From e0499546a2ddfc5a3bc88522503994f770084c51 Mon Sep 17 00:00:00 2001 From: Claude Marche Date: Tue, 5 Dec 2017 09:26:25 +0100 Subject: [PATCH] update Isabelle realizations after changes in int.Exponentiation --- lib/isabelle/Why3_Int.thy | 13 +++++++------ lib/isabelle/Why3_Real.thy.2016-1 | 4 +++- lib/isabelle/Why3_Real.thy.2017 | 4 +++- 3 files changed, 13 insertions(+), 8 deletions(-) diff --git a/lib/isabelle/Why3_Int.thy b/lib/isabelle/Why3_Int.thy index 169e21a54..773e74da9 100644 --- a/lib/isabelle/Why3_Int.thy +++ b/lib/isabelle/Why3_Int.thy @@ -154,7 +154,7 @@ why3_vc Mod_mult using assms by (simp add: emod_def add.commute) why3_vc Mod_bound using assms by (simp_all add: emod_def) why3_vc Div_unique using assms - proof - + proof - have h0: "y \ 0" using assms by auto have h1: "x = y * (x ediv y) + (x emod y)" using h0 Div_mod by blast have h2: "0 \ x emod y \ x emod y < y" using assms H1 h0 Mod_bound zabs_def @@ -166,16 +166,16 @@ why3_vc Div_unique using assms assume a:"q < x ediv y" have h5: "x ediv y \ q + 1" using a by linarith have h6: "y * (x ediv y) >= y * (q + 1)" by (metis H1 h5 le_less mult_left_mono) - have h7: "y * (x ediv y) >= q * y + y" by (metis Comm1 Mul_distr_l h6 monoid_mult_class.mult.right_neutral) + have h7: "y * (x ediv y) >= q * y + y" by (metis Comm1 Mul_distr_l h6 monoid_mult_class.mult.right_neutral) thus "x ediv y = q" using H3 h1 h2 h7 by linarith next assume a:"\ q < x ediv y" - show "x ediv y = q" + show "x ediv y = q" proof (cases "x ediv y < q") assume b:"x ediv y < q" have h5: "x ediv y \ q - 1" using b by linarith have h6: "y * (x ediv y) <= y * (q - 1)" by (metis H1 h5 le_less mult_left_mono) - have h7: "y * (x ediv y) <= q * y - y" by (metis Comm1 h6 int_distrib(4) monoid_mult_class.mult.right_neutral) + have h7: "y * (x ediv y) <= q * y - y" by (metis Comm1 h6 int_distrib(4) monoid_mult_class.mult.right_neutral) thus "x ediv y = q" using H2 h3 h7 by linarith next assume b:"\ x ediv y < q" @@ -320,7 +320,9 @@ why3_vc Power_sum using assms by (simp add: nat_add_distrib power_add) why3_vc Power_mult using assms by (simp add: nat_mult_distrib power_mult) -why3_vc Power_mult2 by (simp add: power_mult_distrib) +why3_vc Power_comm1 by (simp add: power_mult_distrib) + +why3_vc Power_comm2 by (simp add: power_mult_distrib) why3_vc Power_non_neg using assms by simp @@ -329,4 +331,3 @@ why3_vc Power_monotonic using assms by (simp add: power_increasing) why3_end end - diff --git a/lib/isabelle/Why3_Real.thy.2016-1 b/lib/isabelle/Why3_Real.thy.2016-1 index c625cd54c..d13d57385 100644 --- a/lib/isabelle/Why3_Real.thy.2016-1 +++ b/lib/isabelle/Why3_Real.thy.2016-1 @@ -285,7 +285,9 @@ why3_vc Power_mult using assms by (simp add: nat_mult_distrib power_mult) -why3_vc Power_mult2 by (simp only:Power.comm_monoid_mult_class.power_mult_distrib) +why3_vc Power_comm1 by simp + +why3_vc Power_comm2 by (simp add: semiring_normalization_rules(30)) why3_vc Power_s_alt proof - diff --git a/lib/isabelle/Why3_Real.thy.2017 b/lib/isabelle/Why3_Real.thy.2017 index a397a8e80..4d24586ba 100644 --- a/lib/isabelle/Why3_Real.thy.2017 +++ b/lib/isabelle/Why3_Real.thy.2017 @@ -288,7 +288,9 @@ why3_vc Power_mult using assms by (simp add: nat_mult_distrib power_mult) -why3_vc Power_mult2 by (simp only:Power.comm_monoid_mult_class.power_mult_distrib) +why3_vc Power_comm1 by simp + +why3_vc Power_comm2 by (simp add: semiring_normalization_rules(30)) why3_vc Power_s_alt proof - -- GitLab