Attention une mise à jour du serveur va être effectuée le vendredi 16 avril entre 12h et 12h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit 71f2f2b4 authored by Stefan Berghofer's avatar Stefan Berghofer

Streamlined some proofs

parent 9e7b004a
......@@ -32,7 +32,7 @@ lemma nth_eq: "0 \<le> i \<Longrightarrow> nat i < length xs \<Longrightarrow> n
by (induct xs arbitrary: i) (auto simp add: nat_diff_distrib)
why3_vc is_none_spec
by (simp add: is_none_def option.disc_eq_case(1))
by (simp add: is_none_def split: option.split)
why3_end
......@@ -77,7 +77,7 @@ next
qed
why3_vc is_none_spec
by (simp add: NthLength.is_none_def option.disc_eq_case(1))
by (simp add: is_none_def split: option.split)
why3_end
......@@ -87,7 +87,7 @@ section {* Head and tail *}
why3_open "list/HdTl.xml"
why3_vc is_none_spec
by (simp add: HdTl.is_none_def option.disc_eq_case(1))
by (simp add: is_none_def split: option.split)
why3_end
......@@ -113,7 +113,7 @@ why3_vc Nth0_head
by (simp add: hd_def split: list.split)
why3_vc is_none_spec
by (simp add: NthHdTl.is_none_def option.disc_eq_case(1))
by (simp add: is_none_def split: option.split)
why3_end
......@@ -163,7 +163,7 @@ next
qed
why3_vc is_none_spec
by (simp add: NthLengthAppend.is_none_def option.disc_eq_case(1))
by (simp add: is_none_def split: option.split)
why3_end
......
......@@ -91,30 +91,14 @@ proof -
then show ?thesis by (simp add: occ_def)
qed
(* We use occ_append to decompose into {l..<i} {i} {i+1..<j} {j} {j+1..<u} and this complete the
proof
*)
lemma occ_exchange2:
assumes "l \<le> i \<and> i < u \<and> l \<le> j \<and> j < u \<and> i < j"
shows "occ z (m(i := x, j := y)) l u = occ z (m(i := y, j := x)) l u"
proof -
from assms have h1:
"occ z (m (i := x, j := y)) l i + occ z (m (i := x, j := y)) i (i+1) + occ z (m (i := x, j := y)) (i+1) j +
occ z (m (i := x, j := y)) j (j+1) + occ z (m (i := x, j := y)) (j+1) u =
occ z (m (i := x, j := y)) l u"
by (smt occ_append)
from assms have h2:
"occ z (m (i := y, j := x)) l i + occ z (m (i := y, j := x)) i (i+1) + occ z (m (i := y, j := x)) (i+1) j +
occ z (m (i := y, j := x)) j (j+1) + occ z (m (i := y, j := x)) (j+1) u =
occ z (m (i := y, j := x)) l u"
by (smt occ_append)
show ?thesis
by (smt h1 h2 assms facts.set_def occ_bounds(1) occ_eq occ_exists occ_right_add)
qed
lemma vimage_update:
"m(i := x) -` {z} = (if x = z then m -` {z} \<union> {i} else m -` {z} - {i})"
by auto
why3_vc occ_exchange
using assms
by (smt fun_upd_twist occ_exchange2)
by (simp add: occ_def vimage_update insert_Diff_if card_insert)
(auto simp add: Diff_Int_distrib2 card_Diff_subset_Int)
why3_vc occ_left_add
proof -
......
......@@ -30,10 +30,9 @@ why3_vc even_2k by simp
why3_vc odd_2k1 by simp
why3_vc even_mod2
apply (simp add: even_def cmod_def)
by (metis abs_mult abs_mult_sgn abs_numeral mult.assoc mult_zero_right zmod_eq_0_iff)
why3_vc even_mod2
by (auto simp add: even_def cmod_def sgn_if minus_equation_iff [of n])
why3_end
......@@ -42,7 +41,7 @@ section {* Divisibility *}
why3_open "number/Divisibility.xml"
why3_vc divides_def
by (metis ComputerDivision.facts.Div_mod abs_mult add.right_neutral cmod_def dvd_0_left_iff dvd_def mult_zero_right zmod_eq_0_iff)
by (auto simp add: cmod_def sgn_if minus_equation_iff [of n])
why3_vc divides_refl by simp
......@@ -108,7 +107,7 @@ why3_vc even_divides ..
why3_vc odd_divides ..
why3_vc divides_spec
by (metis divides_factorl dvd_div_mult_self)
by (simp add: dvd_def mult.commute)
why3_end
......
......@@ -31,8 +31,7 @@ why3_vc even_2k by simp
why3_vc odd_2k1 by simp
why3_vc even_mod2
apply (simp add: even_def cmod_def)
by (metis abs_mult abs_mult_sgn abs_numeral mult.assoc mult_zero_right zmod_eq_0_iff)
by (auto simp add: even_def cmod_def sgn_if minus_equation_iff [of n])
why3_end
......@@ -42,7 +41,7 @@ section {* Divisibility *}
why3_open "number/Divisibility.xml"
why3_vc divides_def
by (metis ComputerDivision.facts.Div_mod abs_mult add.right_neutral cmod_def dvd_0_left_iff dvd_def mult_zero_right zmod_eq_0_iff)
by (auto simp add: cmod_def sgn_if minus_equation_iff [of n])
why3_vc divides_refl by simp
......@@ -108,7 +107,7 @@ why3_vc even_divides ..
why3_vc odd_divides ..
why3_vc divides_spec
by (metis divides_factorl dvd_div_mult_self)
by (simp add: dvd_def mult.commute)
why3_end
......
......@@ -7,9 +7,6 @@ begin
section {* Potentially infinite sets *}
definition choose_elt :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" where
"choose_elt S = (\<some>x. S x)"
definition complement :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where
"complement S v = Not (S v)"
......@@ -22,7 +19,7 @@ why3_open "set/Set.xml"
inter = inf
diff = minus
complement = complement
choose = choose_elt
choose = Eps
all = top
why3_vc add_spec by (auto simp add: mem_def)
......@@ -49,7 +46,8 @@ why3_vc union_spec
by (simp add: mem_def)
why3_vc choose_spec
by (metis assms choose_elt_def mem_def set.Set.is_empty_def tfl_some)
using assms
by (auto simp add: mem_def is_empty_def intro: someI_ex)
why3_vc remove_spec
by (simp add: mem_def)
......@@ -61,7 +59,8 @@ why3_vc subset_refl
by (simp add: subset_def)
why3_vc subset_trans
by (meson H1 H2 subset_def)
using assms
by (simp add: subset_def)
why3_vc subset_remove
by (simp add: remove_spec subset_def)
......@@ -84,9 +83,6 @@ definition fremove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
definition fchoose :: "'a fset \<Rightarrow> 'a" where
"fchoose S = (\<some>x. x |\<in>| S)"
definition ext_eq :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where
"ext_eq S1 S2 = (S1 = S2)"
definition is_empty :: "'a fset \<Rightarrow> bool" where
"is_empty S = (S = fempty)"
......@@ -101,7 +97,7 @@ why3_open "set/Fset.xml"
diff = minus
choose = fchoose
all = top
infix_eqeq = ext_eq
infix_eqeq = HOL.eq
subset = fsubset_eq
is_empty = is_empty
types
......@@ -134,16 +130,16 @@ why3_vc subset_trans
why3_vc subset_remove by (auto simp add: fremove_def)
why3_vc subset_eq
using assms ext_eq_def fcard_seteq by fastforce
using assms fcard_seteq by fastforce
why3_vc subset_spec by auto
why3_vc infix_eqeq_spec
by (metis ext_eq_def fsubset_antisym subset_spec)
by (simp add: fset_eq_iff)
why3_vc extensionality
using assms
by (auto simp add: ext_eq_def)
by simp
why3_vc cardinal1
proof (cases s rule: fset_strong_cases)
......@@ -191,8 +187,7 @@ why3_vc diff_spec by simp
why3_vc choose_spec
using assms
using Why3_Set.is_empty_def
by (metis (full_types) ex_fin_conv fchoose_def someI_ex)
by (auto simp add: fchoose_def is_empty_def intro: someI_ex)
why3_vc is_empty_spec
by (simp add: Why3_Set.is_empty_def)
......
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