Commit f2df0ef6 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

update Isabelle realizations after changes in int.Exponentiation

parent 67d281ae
...@@ -154,7 +154,7 @@ why3_vc Mod_mult using assms by (simp add: emod_def add.commute) ...@@ -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 Mod_bound using assms by (simp_all add: emod_def)
why3_vc Div_unique using assms why3_vc Div_unique using assms
proof - proof -
have h0: "y \<noteq> 0" using assms by auto have h0: "y \<noteq> 0" using assms by auto
have h1: "x = y * (x ediv y) + (x emod y)" using h0 Div_mod by blast have h1: "x = y * (x ediv y) + (x emod y)" using h0 Div_mod by blast
have h2: "0 \<le> x emod y \<and> x emod y < y" using assms H1 h0 Mod_bound zabs_def have h2: "0 \<le> x emod y \<and> x emod y < y" using assms H1 h0 Mod_bound zabs_def
...@@ -166,16 +166,16 @@ why3_vc Div_unique using assms ...@@ -166,16 +166,16 @@ why3_vc Div_unique using assms
assume a:"q < x ediv y" assume a:"q < x ediv y"
have h5: "x ediv y \<ge> q + 1" using a by linarith have h5: "x ediv y \<ge> 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 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 thus "x ediv y = q" using H3 h1 h2 h7 by linarith
next next
assume a:"\<not> q < x ediv y" assume a:"\<not> q < x ediv y"
show "x ediv y = q" show "x ediv y = q"
proof (cases "x ediv y < q") proof (cases "x ediv y < q")
assume b:"x ediv y < q" assume b:"x ediv y < q"
have h5: "x ediv y \<le> q - 1" using b by linarith have h5: "x ediv y \<le> 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 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 thus "x ediv y = q" using H2 h3 h7 by linarith
next next
assume b:"\<not> x ediv y < q" assume b:"\<not> x ediv y < q"
...@@ -320,7 +320,9 @@ why3_vc Power_sum using assms by (simp add: nat_add_distrib power_add) ...@@ -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_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 why3_vc Power_non_neg using assms by simp
...@@ -329,4 +331,3 @@ why3_vc Power_monotonic using assms by (simp add: power_increasing) ...@@ -329,4 +331,3 @@ why3_vc Power_monotonic using assms by (simp add: power_increasing)
why3_end why3_end
end end
...@@ -285,7 +285,9 @@ why3_vc Power_mult ...@@ -285,7 +285,9 @@ why3_vc Power_mult
using assms using assms
by (simp add: nat_mult_distrib power_mult) 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 why3_vc Power_s_alt
proof - proof -
......
...@@ -288,7 +288,9 @@ why3_vc Power_mult ...@@ -288,7 +288,9 @@ why3_vc Power_mult
using assms using assms
by (simp add: nat_mult_distrib power_mult) 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 why3_vc Power_s_alt
proof - proof -
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment