From 0ee5101d59561a30509b1939fb34568513019d8c Mon Sep 17 00:00:00 2001 From: Wolfgang Jeltsch Date: Wed, 29 Dec 2021 13:33:58 +0200 Subject: [PATCH 1/7] Add the skeleton of the next-generation usage example --- src/Equivalence_Reasoner-Usage_Example.thy | 10 ++++++++++ src/ROOT | 1 + 2 files changed, 11 insertions(+) create mode 100644 src/Equivalence_Reasoner-Usage_Example.thy diff --git a/src/Equivalence_Reasoner-Usage_Example.thy b/src/Equivalence_Reasoner-Usage_Example.thy new file mode 100644 index 0000000..23f617d --- /dev/null +++ b/src/Equivalence_Reasoner-Usage_Example.thy @@ -0,0 +1,10 @@ +text_raw \\appendix\ + +section \Usage Example\ + +theory "Equivalence_Reasoner-Usage_Example" +imports + Equivalence_Reasoner +begin + +end diff --git a/src/ROOT b/src/ROOT index aeb52e2..e36310a 100644 --- a/src/ROOT +++ b/src/ROOT @@ -7,5 +7,6 @@ session Equivalence_Reasoner = HOL + "HOL-Eisbach" theories Equivalence_Reasoner + "Equivalence_Reasoner-Usage_Example" document_files "root.tex" From 5a42e72f9f69433adebaf53bf87998b919d60da3 Mon Sep 17 00:00:00 2001 From: Wolfgang Jeltsch Date: Wed, 29 Dec 2021 13:48:17 +0200 Subject: [PATCH 2/7] =?UTF-8?q?Add=20code=20of=20subsection=20=E2=80=9CExt?= =?UTF-8?q?ended=20Reals=E2=80=9D?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Equivalence_Reasoner-Usage_Example.thy | 89 ++++++++++++++++++++++ 1 file changed, 89 insertions(+) diff --git a/src/Equivalence_Reasoner-Usage_Example.thy b/src/Equivalence_Reasoner-Usage_Example.thy index 23f617d..d5a3bf4 100644 --- a/src/Equivalence_Reasoner-Usage_Example.thy +++ b/src/Equivalence_Reasoner-Usage_Example.thy @@ -5,6 +5,95 @@ section \Usage Example\ theory "Equivalence_Reasoner-Usage_Example" imports Equivalence_Reasoner + "HOL-Library.Extended_Nonnegative_Real" begin +subsection \Extended Reals\ + +setup_lifting type_definition_ennreal + +function extended_exp :: "ereal \ ennreal" where + "extended_exp (-\) = 0" | + "extended_exp x = exp x" for x :: real | + "extended_exp \ = \" + by (erule ereal_cases, simp_all) + termination by standard+ + +function extended_ln :: "ennreal \ ereal" where + "extended_ln 0 = -\" | + "extended_ln x = ln x" if "x > 0" for x :: real | + "extended_ln \ = \" + by (rule ennreal_cases, force, simp_all) + termination by standard+ + +lemma extended_exp_of_sum: + assumes "x \ \" and "y \ \" + shows "extended_exp (x + y) = extended_exp x * extended_exp y" + using assms + by + (cases x rule: extended_exp.cases; cases y rule: extended_exp.cases) + (simp_all add: exp_add ennreal_mult) + +lemma extended_ln_of_product: + assumes "x \ \" and "y \ \" + shows "extended_ln (x * y) = extended_ln x + extended_ln y" + using assms + by + (cases x rule: extended_ln.cases; cases y rule: extended_ln.cases) + (simp_all add: ln_mult ennreal_mult [symmetric]) + +lemma extended_ln_after_extended_exp: + shows "extended_ln (extended_exp x) = x" + by (cases x rule: extended_exp.cases) (simp_all del: infinity_ennreal_def) + +lemma extended_exp_after_extended_ln: + shows "extended_exp (extended_ln x) = x" + by (cases x rule: extended_ln.cases) (simp_all del: infinity_ennreal_def) + +lemma extended_exp_surjectivity: + shows "surj extended_exp" + using extended_exp_after_extended_ln + by (rule surjI) + +lemma extended_ln_surjectivity: + shows "surj extended_ln" + using extended_ln_after_extended_exp + by (rule surjI) + +lemma extended_exp_monotonicity: + shows "mono extended_exp" +proof + fix x y :: ereal + assume "x \ y" + then show "extended_exp x \ extended_exp y" + by (cases x rule: extended_exp.cases; cases y rule: extended_exp.cases) simp_all +qed + +lemma extended_ln_monotonicity: + shows "mono extended_ln" +proof + fix x y :: ennreal + assume "x \ y" + then show "extended_ln x \ extended_ln y" + by + (cases x rule: extended_ln.cases; cases y rule: extended_ln.cases) + ( + (simp_all del: infinity_ennreal_def)[7], + metis ennreal_less_top infinity_ennreal_def not_le, + simp + ) +qed + +lemma extended_exp_continuity: + shows "continuous_on UNIV extended_exp" + by + (rule continuous_onI_mono) + (simp add: extended_exp_surjectivity, rule extended_exp_monotonicity [THEN monoD]) + +lemma extended_ln_continuity: + shows "continuous_on UNIV extended_ln" + by + (rule continuous_onI_mono) + (simp add: extended_ln_surjectivity, rule extended_ln_monotonicity [THEN monoD]) + end From f0f75281e1f03be53c444ee557b2e46490860522 Mon Sep 17 00:00:00 2001 From: Wolfgang Jeltsch Date: Wed, 29 Dec 2021 14:43:38 +0200 Subject: [PATCH 3/7] =?UTF-8?q?Add=20code=20of=20subsection=20=E2=80=9CPos?= =?UTF-8?q?itive=20Reals=E2=80=9D?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Equivalence_Reasoner-Usage_Example.thy | 90 ++++++++++++++++++++++ 1 file changed, 90 insertions(+) diff --git a/src/Equivalence_Reasoner-Usage_Example.thy b/src/Equivalence_Reasoner-Usage_Example.thy index d5a3bf4..5d2c01e 100644 --- a/src/Equivalence_Reasoner-Usage_Example.thy +++ b/src/Equivalence_Reasoner-Usage_Example.thy @@ -96,4 +96,94 @@ lemma extended_ln_continuity: (rule continuous_onI_mono) (simp add: extended_ln_surjectivity, rule extended_ln_monotonicity [THEN monoD]) +subsection \Positive Reals\ + +typedef positive_real = "{x :: real. x > 0}" + using zero_less_one + by blast + +setup_lifting type_definition_positive_real + +instantiation positive_real :: comm_semiring +begin + +lift_definition plus_positive_real :: "positive_real \ positive_real \ positive_real" + is "(+)" + using add_pos_pos . + +lift_definition times_positive_real :: "positive_real \ positive_real \ positive_real" + is "(*)" + using mult_pos_pos . + +instance by (standard; transfer) (simp_all add: algebra_simps) + +end + +instantiation positive_real :: comm_monoid_mult +begin + +lift_definition one_positive_real :: positive_real + is 1 + using zero_less_one . + +instance by (standard; transfer) simp + +end + +instantiation positive_real :: inverse +begin + +lift_definition divide_positive_real :: "positive_real \ positive_real \ positive_real" + is "(/)" + using divide_pos_pos . + +lift_definition inverse_positive_real :: "positive_real \ positive_real" + is inverse + using positive_imp_inverse_positive . + +instance .. + +end + +instantiation positive_real :: unbounded_dense_linorder +begin + +lift_definition less_eq_positive_real :: "positive_real \ positive_real \ bool" + is "(\)" . + +lift_definition less_positive_real :: "positive_real \ positive_real \ bool" + is "(<)" . + +instance proof ((standard; transfer), unfold bex_simps(6)) + show "\z > 0. x < z \ z < y" if "x > 0" and "x < y" for x y :: real + proof + show "(x + y) / 2 > 0 \ x < (x + y) / 2 \ (x + y) / 2 < y" + using that + by simp + qed +next + show "\y > 0. y > x" if "x > 0" for x :: real + using gt_ex and that + by (iprover intro: less_trans) +next + show "\y > 0. y < x" if "x > 0" for x :: real + using dense [OF that] . +qed auto + +end + +lift_definition extended_non_negative_real :: "positive_real \ ennreal" + is ennreal . + +lemma extended_non_negative_real_is_finite: + shows "extended_non_negative_real x \ \" + by transfer simp + +lemma extended_non_negative_real_of_product: + shows " + extended_non_negative_real (x * y) + = + extended_non_negative_real x * extended_non_negative_real y" + by transfer (simp only: ennreal_mult) + end From 07240ad94210f12f1ca2185dc61bc89cb0c9d700 Mon Sep 17 00:00:00 2001 From: Wolfgang Jeltsch Date: Wed, 29 Dec 2021 14:50:47 +0200 Subject: [PATCH 4/7] =?UTF-8?q?Add=20code=20of=20subsection=20=E2=80=9CSeq?= =?UTF-8?q?uences=20of=20Positive=20Reals=E2=80=9D?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Equivalence_Reasoner-Usage_Example.thy | 118 ++++++++++++++++++++- src/ROOT | 1 + 2 files changed, 118 insertions(+), 1 deletion(-) diff --git a/src/Equivalence_Reasoner-Usage_Example.thy b/src/Equivalence_Reasoner-Usage_Example.thy index 5d2c01e..1a3c7c3 100644 --- a/src/Equivalence_Reasoner-Usage_Example.thy +++ b/src/Equivalence_Reasoner-Usage_Example.thy @@ -5,7 +5,7 @@ section \Usage Example\ theory "Equivalence_Reasoner-Usage_Example" imports Equivalence_Reasoner - "HOL-Library.Extended_Nonnegative_Real" + "HOL-Analysis.Extended_Real_Limits" begin subsection \Extended Reals\ @@ -186,4 +186,120 @@ lemma extended_non_negative_real_of_product: extended_non_negative_real x * extended_non_negative_real y" by transfer (simp only: ennreal_mult) +subsection \Sequences of Positive Reals\ + +typedef sequence = "UNIV :: (nat \ positive_real) set" + by simp + +setup_lifting type_definition_sequence + +instantiation sequence :: comm_semiring +begin + +lift_definition plus_sequence :: "sequence \ sequence \ sequence" + is "\X Y. \i. X i + Y i" . + +lift_definition times_sequence :: "sequence \ sequence \ sequence" + is "\X Y. \i. X i * Y i" . + +instance by (standard; transfer) (simp_all add: algebra_simps) + +end + +instantiation sequence :: comm_monoid_mult +begin + +lift_definition one_sequence :: sequence + is "\_. 1" . + +instance by (standard; transfer) simp + +end + +instantiation sequence :: inverse +begin + +lift_definition divide_sequence :: "sequence \ sequence \ sequence" + is "\X Y. \i. X i / Y i" . + +lift_definition inverse_sequence :: "sequence \ sequence" + is "\X. \i. inverse (X i)" . + +instance .. + +end + +instantiation sequence :: dense_order +begin + +lift_definition less_eq_sequence :: "sequence \ sequence \ bool" + is "(\)" . + +lift_definition less_sequence :: "sequence \ sequence \ bool" + is "(<)" . + +instance proof (standard; transfer) + show "\Z > X. Z < Y" if "X < Y" for X Y Z :: "nat \ positive_real" + proof - + from \X < Y\ obtain i where "X i < Y i" + by (metis leD le_funI leI) + then obtain z where "X i < z" and "z < Y i" + using dense + by blast + with \X < Y\ have "X < X(i := z)" and "X(i := z) < Y" + by (auto simp add: less_le_not_le le_fun_def) + then show ?thesis + by iprover + qed +qed (simp_all add: less_le_not_le) + +end + +lift_definition limit_superior :: "sequence \ ennreal" + is "\X. limsup (\i. extended_non_negative_real (X i))" . + +lemma limit_superior_of_product: + assumes "limit_superior X \ \" and "limit_superior Y \ \" + shows "limit_superior (X * Y) \ limit_superior X * limit_superior Y" +proof - + note Limsup_after_extended_ln = + Limsup_compose_continuous_mono [OF extended_ln_continuity extended_ln_monotonicity] + have raw_thesis: + "limsup (\i. X i * Y i) \ limsup X * limsup Y" + if "\i. X i \ \" and "\i. Y i \ \" and "limsup X \ \" and "limsup Y \ \" + for X Y :: "nat \ ennreal" + proof - + from that(3-4) have "extended_ln (limsup X) \ \" and "extended_ln (limsup Y) \ \" + by (metis extended_exp_after_extended_ln extended_exp.simps(3))+ + then have 1: "limsup (\i. extended_ln (X i)) \ \" and 2: "limsup (\i. extended_ln (Y i)) \ \" + by (simp_all add: Limsup_after_extended_ln) + have "limsup (\i. X i * Y i) = extended_exp (extended_ln (limsup (\i. X i * Y i)))" + by (simp only: extended_exp_after_extended_ln) + also have "\ = extended_exp (limsup (\i. extended_ln (X i * Y i)))" + by (simp_all add: Limsup_after_extended_ln) + also have "\ = extended_exp (limsup (\i. extended_ln (X i) + extended_ln (Y i)))" + using extended_ln_of_product and that(1-2) + by simp + also have "\ \ extended_exp (limsup (\i. extended_ln (X i)) + limsup (\i. extended_ln (Y i)))" + using ereal_limsup_add_mono + by (rule extended_exp_monotonicity [THEN monoD]) + also have "\ = + extended_exp (limsup (\i. extended_ln (X i))) * extended_exp (limsup (\i. extended_ln (Y i)))" + using extended_exp_of_sum and 1 2 + by simp + also have "\ = extended_exp (extended_ln (limsup X)) * extended_exp (extended_ln (limsup Y))" + by (simp_all add: Limsup_after_extended_ln) + also have "\ = limsup X * limsup Y" + by (simp only: extended_exp_after_extended_ln) + finally show ?thesis . + qed + from assms show ?thesis + by + transfer + (auto + simp only: extended_non_negative_real_of_product extended_non_negative_real_is_finite + intro: raw_thesis + ) +qed + end diff --git a/src/ROOT b/src/ROOT index e36310a..6fa1a65 100644 --- a/src/ROOT +++ b/src/ROOT @@ -5,6 +5,7 @@ session Equivalence_Reasoner = HOL + \An Automated Equivalence Reasoner for Isabelle/HOL.\ sessions "HOL-Eisbach" + "HOL-Analysis" theories Equivalence_Reasoner "Equivalence_Reasoner-Usage_Example" From 45b0f3edb1a1d88c6e9154f92399963d92105087 Mon Sep 17 00:00:00 2001 From: Wolfgang Jeltsch Date: Wed, 29 Dec 2021 14:57:18 +0200 Subject: [PATCH 5/7] =?UTF-8?q?Add=20code=20of=20subsection=20=E2=80=9CAsy?= =?UTF-8?q?mptotic=20Bounds=E2=80=9D?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Equivalence_Reasoner-Usage_Example.thy | 48 ++++++++++++++++++++++ 1 file changed, 48 insertions(+) diff --git a/src/Equivalence_Reasoner-Usage_Example.thy b/src/Equivalence_Reasoner-Usage_Example.thy index 1a3c7c3..be81fb3 100644 --- a/src/Equivalence_Reasoner-Usage_Example.thy +++ b/src/Equivalence_Reasoner-Usage_Example.thy @@ -302,4 +302,52 @@ proof - ) qed +subsection \Asymptotic Bounds\ + +definition asymptotically_bounded_above_by :: "sequence \ sequence \ bool" (infix \\\ 50) where + "X \ Y \ limit_superior (X / Y) \ 1" + +lemma asymptotically_bounded_above_by_reflexivity [iff]: + shows "X \ X" +proof - + have "limit_superior (X / X) \ 1" for X :: sequence + proof - + have "limit_superior (X / X) = limit_superior 1" + by (transfer, transfer) (simp add: less_le) + also have "\ = 1" + by (transfer, transfer) (simp add: Limsup_const) + also have "\ \ 1" + using order.refl . + finally show ?thesis . + qed + then show ?thesis + unfolding asymptotically_bounded_above_by_def . +qed + +lemma asymptotically_bounded_above_by_transitivity [trans]: + assumes "X \ Y" and "Y \ Z" + shows "X \ Z" +proof - + have raw_thesis: + "limit_superior (X / Z) \ 1" + if "limit_superior (X / Y) \ 1" and "limit_superior (Y / Z) \ 1" + for X Y Z :: sequence + proof - + have "limit_superior (X / Z) = limit_superior ((X / Y) * (Y / Z))" + by (transfer, transfer) (simp add: less_le) + also have "\ \ limit_superior (X / Y) * limit_superior (Y / Z)" + by ( + rule limit_superior_of_product, unfold infinity_ennreal_def; + rule neq_top_trans, use that in simp_all + ) + also have "\ \ 1" + using mult_mono and that + by fastforce + finally show ?thesis . + qed + from assms show ?thesis + unfolding asymptotically_bounded_above_by_def + by (fact raw_thesis) +qed + end From 1a6c13d9312ab42f7f0d99810e190d77e5d59620 Mon Sep 17 00:00:00 2001 From: Wolfgang Jeltsch Date: Wed, 5 Jan 2022 21:24:47 +0200 Subject: [PATCH 6/7] Add changelog entry --- CHANGELOG.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index cd1e81c..af2bb7a 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,3 +4,5 @@ Start – version 0.0.0.0 * Document the usage of the next-generation equivalence reasoner * Implement the next-generation equivalence reasoner + + * Add an example of using the next-generation equivalence reasoner From f9a0ebd0777341b6b50e23c225cc9fd5e2ccca4e Mon Sep 17 00:00:00 2001 From: Wolfgang Jeltsch Date: Sun, 16 Jul 2023 20:10:36 +0300 Subject: [PATCH 7/7] Improve the layout of the `imports` clause This complements #71. --- src/Equivalence_Reasoner-Usage_Example.thy | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Equivalence_Reasoner-Usage_Example.thy b/src/Equivalence_Reasoner-Usage_Example.thy index be81fb3..61377af 100644 --- a/src/Equivalence_Reasoner-Usage_Example.thy +++ b/src/Equivalence_Reasoner-Usage_Example.thy @@ -3,9 +3,9 @@ text_raw \\appendix\ section \Usage Example\ theory "Equivalence_Reasoner-Usage_Example" -imports - Equivalence_Reasoner - "HOL-Analysis.Extended_Real_Limits" + imports + Equivalence_Reasoner + "HOL-Analysis.Extended_Real_Limits" begin subsection \Extended Reals\