Commit 4dd0cc57 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Adapt Isabelle realizations to new_system/master

This only adapts existing .thy files so that compilation go through.
Modifications may/(should?) be improved as they were mainly application of
sledgehammer.
Compilation should work for both Isabelle2016-1 and Isabelle2017.
parent ba2f367a
...@@ -1503,6 +1503,7 @@ endif ...@@ -1503,6 +1503,7 @@ endif
install-isabelle: $(GENERATED_PREFIX_ISABELLE)/last_build install-isabelle: $(GENERATED_PREFIX_ISABELLE)/last_build
install_local:: install-isabelle
install:: install-isabelle install:: install-isabelle
clean:: clean::
......
...@@ -31,6 +31,9 @@ why3_open "list/Nth.xml" ...@@ -31,6 +31,9 @@ why3_open "list/Nth.xml"
lemma nth_eq: "0 \<le> i \<Longrightarrow> nat i < length xs \<Longrightarrow> nth i xs = Some (xs ! nat i)" lemma nth_eq: "0 \<le> i \<Longrightarrow> nat i < length xs \<Longrightarrow> nth i xs = Some (xs ! nat i)"
by (induct xs arbitrary: i) (auto simp add: nat_diff_distrib) 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))
why3_end why3_end
...@@ -73,6 +76,9 @@ next ...@@ -73,6 +76,9 @@ next
qed simp qed simp
qed qed
why3_vc is_none_spec
by (simp add: NthLength.is_none_def option.disc_eq_case(1))
why3_end why3_end
...@@ -80,6 +86,9 @@ section {* Head and tail *} ...@@ -80,6 +86,9 @@ section {* Head and tail *}
why3_open "list/HdTl.xml" why3_open "list/HdTl.xml"
why3_vc is_none_spec
by (simp add: HdTl.is_none_def option.disc_eq_case(1))
why3_end why3_end
...@@ -103,6 +112,9 @@ why3_vc Nth_tl ...@@ -103,6 +112,9 @@ why3_vc Nth_tl
why3_vc Nth0_head why3_vc Nth0_head
by (simp add: hd_def split: list.split) 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))
why3_end why3_end
...@@ -150,6 +162,9 @@ next ...@@ -150,6 +162,9 @@ next
with assms show ?thesis by (simp add: nth_none_2) with assms show ?thesis by (simp add: nth_none_2)
qed qed
why3_vc is_none_spec
by (simp add: NthLengthAppend.is_none_def option.disc_eq_case(1))
why3_end why3_end
......
...@@ -6,26 +6,25 @@ section {* Generic Maps *} ...@@ -6,26 +6,25 @@ section {* Generic Maps *}
why3_open "map/Map.xml" why3_open "map/Map.xml"
why3_vc Select_eq why3_vc set_def by auto
using assms
by simp
why3_vc Select_neq
using assms
by simp
why3_end why3_end
section {* Constant Maps *} section {* Constant Maps *}
definition abs_const :: "'a \<Rightarrow> ('b \<Rightarrow> 'a)" where
"abs_const v y = v"
why3_open "map/Const.xml" why3_open "map/Const.xml"
constants
const=abs_const
why3_vc Const by simp why3_vc const_def
by (simp add: abs_const_def)
why3_end why3_end
section {* Number of occurrences *} section {* Number of occurrences *}
definition occ :: "'a \<Rightarrow> (int \<Rightarrow> 'a) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int" where definition occ :: "'a \<Rightarrow> (int \<Rightarrow> 'a) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int" where
...@@ -92,8 +91,44 @@ proof - ...@@ -92,8 +91,44 @@ proof -
then show ?thesis by (simp add: occ_def) then show ?thesis by (simp add: occ_def)
qed qed
why3_end (* 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
why3_vc occ_exchange
using assms
by (smt fun_upd_twist occ_exchange2)
why3_vc occ_left_add
proof -
from assms have "{l..<u} = {l} \<union> {l + 1..<u}" by auto
with assms show ?thesis by (simp add: occ_def)
qed
why3_vc occ_left_no_add
proof -
from assms have "{l..<u} = {l} \<union> {l + 1..<u}" by auto
with assms show ?thesis by (simp add: occ_def)
qed
why3_end
why3_open "map/MapPermut.xml" why3_open "map/MapPermut.xml"
......
...@@ -30,6 +30,10 @@ why3_vc even_2k by simp ...@@ -30,6 +30,10 @@ why3_vc even_2k by simp
why3_vc odd_2k1 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_end why3_end
...@@ -37,7 +41,8 @@ section {* Divisibility *} ...@@ -37,7 +41,8 @@ section {* Divisibility *}
why3_open "number/Divisibility.xml" why3_open "number/Divisibility.xml"
why3_vc divides_def by (simp add: dvd_def mult.commute) 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)
why3_vc divides_refl by simp why3_vc divides_refl by simp
...@@ -102,6 +107,9 @@ why3_vc even_divides .. ...@@ -102,6 +107,9 @@ why3_vc even_divides ..
why3_vc odd_divides .. why3_vc odd_divides ..
why3_vc divides_spec
by (metis divides_factorl dvd_div_mult_self)
why3_end why3_end
......
...@@ -30,6 +30,10 @@ why3_vc even_2k by simp ...@@ -30,6 +30,10 @@ why3_vc even_2k by simp
why3_vc odd_2k1 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_end why3_end
...@@ -37,7 +41,8 @@ section {* Divisibility *} ...@@ -37,7 +41,8 @@ section {* Divisibility *}
why3_open "number/Divisibility.xml" why3_open "number/Divisibility.xml"
why3_vc divides_def by (simp add: dvd_def mult.commute) 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)
why3_vc divides_refl by simp why3_vc divides_refl by simp
...@@ -102,6 +107,9 @@ why3_vc even_divides .. ...@@ -102,6 +107,9 @@ why3_vc even_divides ..
why3_vc odd_divides .. why3_vc odd_divides ..
why3_vc divides_spec
by (metis divides_factorl dvd_div_mult_self)
why3_end why3_end
......
...@@ -144,6 +144,8 @@ why3_vc Zero by auto ...@@ -144,6 +144,8 @@ why3_vc Zero by auto
why3_vc Monotonic using assms by auto why3_vc Monotonic using assms by auto
why3_vc Injective using assms by auto
why3_end why3_end
section {* Various truncation functions *} section {* Various truncation functions *}
......
...@@ -147,6 +147,8 @@ why3_vc Zero by auto ...@@ -147,6 +147,8 @@ why3_vc Zero by auto
why3_vc Monotonic using assms by auto why3_vc Monotonic using assms by auto
why3_vc Injective using assms by auto
why3_end why3_end
section {* Various truncation functions *} section {* Various truncation functions *}
......
theory Why3_Set theory Why3_Set
imports Why3_Setup "~~/src/HOL/Library/FSet" imports Why3_Setup Why3_Map "~~/src/HOL/Library/FSet"
begin begin
section {* Potentially infinite sets *} section {* Potentially infinite sets *}
definition choose :: "'a set \<Rightarrow> 'a" where definition choose_elt :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" where
"choose S = (\<some>x. x \<in> S)" "choose_elt S = (\<some>x. S x)"
definition complement :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where
"complement S v = Not (S v)"
why3_open "set/Set.xml" why3_open "set/Set.xml"
constants constants
mem = Set.member
empty = bot empty = bot
add = insert add = insert
remove = Set.remove remove = Set.remove
union = sup union = sup
inter = inf inter = inf
diff = minus diff = minus
choose = choose complement = complement
choose = choose_elt
all = top all = top
types
set = set
why3_vc all_def by simp why3_vc add_spec by (auto simp add: mem_def)
why3_vc add_def1 by simp why3_vc diff_def by simp
why3_vc diff_def1 by simp why3_vc diff_spec by (simp add: mem_def)
why3_vc mem_empty by simp why3_vc inter_def by simp
why3_vc add_remove why3_vc mem_empty by (simp add: const_def mem_def set.Set.is_empty_def)
using assms
by (auto simp add: remove_def)
why3_vc remove_add by (simp add: remove_def) why3_vc union_def by simp
why3_vc choose_def why3_vc add_remove
using assms using assms
by (auto simp add: is_empty_def choose_def intro: someI_ex) by (simp add: fun_upd_idem_iff mem_def)
why3_vc empty_def1 by (simp add: is_empty_def) why3_vc inter_spec by (simp add: mem_def)
why3_vc inter_def1 by simp why3_vc remove_add by auto
why3_vc union_def1 by simp why3_vc union_spec
by (simp add: mem_def)
why3_vc remove_def1 by (auto simp add: remove_def) why3_vc choose_spec
by (metis assms choose_elt_def mem_def set.Set.is_empty_def tfl_some)
why3_vc subset_diff by auto why3_vc remove_spec
by (simp add: mem_def)
why3_vc subset_def by auto why3_vc subset_diff
by (simp add: diff_spec subset_def)
why3_vc subset_refl by simp why3_vc subset_refl
by (simp add: subset_def)
why3_vc subset_trans why3_vc subset_trans
using assms by (meson H1 H2 subset_def)
by simp
why3_vc subset_remove
by (simp add: remove_spec subset_def)
why3_vc subset_remove by (auto simp add: remove_def) why3_vc complement_def
by (simp add: complement_def)
why3_vc extensionality why3_vc extensionality
using assms using assms
by simp by (auto simp add: infix_eqeq_def mem_def)
why3_vc infix_eqeq_def by auto
why3_end why3_end
...@@ -76,6 +81,12 @@ definition fremove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where ...@@ -76,6 +81,12 @@ definition fremove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
definition fchoose :: "'a fset \<Rightarrow> 'a" where definition fchoose :: "'a fset \<Rightarrow> 'a" where
"fchoose S = (\<some>x. x |\<in>| S)" "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)"
why3_open "set/Fset.xml" why3_open "set/Fset.xml"
constants constants
mem = fmember mem = fmember
...@@ -87,14 +98,13 @@ why3_open "set/Fset.xml" ...@@ -87,14 +98,13 @@ why3_open "set/Fset.xml"
diff = minus diff = minus
choose = fchoose choose = fchoose
all = top all = top
infix_eqeq = ext_eq
subset = fsubset_eq
is_empty = is_empty
types types
set = fset set = fset
why3_vc add_def1 by simp why3_vc add_spec by simp
why3_vc diff_def1 by simp
why3_vc mem_empty by simp
why3_vc add_remove why3_vc add_remove
using assms using assms
...@@ -102,22 +112,16 @@ why3_vc add_remove ...@@ -102,22 +112,16 @@ why3_vc add_remove
why3_vc remove_add by (simp add: fremove_def) why3_vc remove_add by (simp add: fremove_def)
why3_vc choose_def why3_vc empty_def by (simp add: is_empty_def)
using assms
by (auto simp add: is_empty_def fchoose_def intro: someI_ex)
why3_vc empty_def1 by (simp add: is_empty_def)
why3_vc inter_def1 by simp why3_vc inter_spec by simp
why3_vc union_def1 by simp why3_vc union_spec by simp
why3_vc remove_def1 by (auto simp add: fremove_def) why3_vc remove_spec by (auto simp add: fremove_def)
why3_vc subset_diff by auto why3_vc subset_diff by auto
why3_vc subset_def by auto
why3_vc subset_refl by simp why3_vc subset_refl by simp
why3_vc subset_trans why3_vc subset_trans
...@@ -126,11 +130,17 @@ why3_vc subset_trans ...@@ -126,11 +130,17 @@ why3_vc subset_trans
why3_vc subset_remove by (auto simp add: fremove_def) why3_vc subset_remove by (auto simp add: fremove_def)
why3_vc subset_eq
using assms ext_eq_def fcard_seteq by fastforce
why3_vc subset_spec by auto
why3_vc infix_eqeq_spec
by (metis ext_eq_def fsubset_antisym subset_spec)
why3_vc extensionality why3_vc extensionality
using assms using assms
by simp by (auto simp add: ext_eq_def)
why3_vc infix_eqeq_def by auto
why3_vc cardinal1 why3_vc cardinal1
proof (cases s rule: fset_strong_cases) proof (cases s rule: fset_strong_cases)
...@@ -174,8 +184,15 @@ why3_vc cardinal_subset ...@@ -174,8 +184,15 @@ why3_vc cardinal_subset
using assms using assms
by (simp add: fcard_mono) by (simp add: fcard_mono)
why3_vc subset_eq why3_vc diff_spec by simp
by (metis H1 H2 fcard_seteq nat_int order_refl)
why3_vc choose_spec
using assms
using Why3_Set.is_empty_def
by (metis (full_types) ex_fin_conv fchoose_def someI_ex)
why3_vc is_empty_spec
by (simp add: Why3_Set.is_empty_def)
why3_end why3_end
......
theory Why3_Set theory Why3_Set
imports imports
Why3_Setup Why3_Setup
Why3_Map
"HOL-Library.FSet" "HOL-Library.FSet"
begin begin
section {* Potentially infinite sets *} section {* Potentially infinite sets *}
definition choose_elt :: "'a set \<Rightarrow> 'a" where definition choose_elt :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" where
"choose_elt S = (\<some>x. x \<in> S)" "choose_elt S = (\<some>x. S x)"
definition complement :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where
"complement S v = Not (S v)"
why3_open "set/Set.xml" why3_open "set/Set.xml"
constants constants
mem = Set.member
empty = bot empty = bot
add = insert add = insert
remove = Set.remove remove = Set.remove
union = sup union = sup
inter = inf inter = inf
diff = minus diff = minus
complement = complement
choose = choose_elt choose = choose_elt
all = top all = top
types
set = set
why3_vc all_def by simp why3_vc add_spec by (auto simp add: mem_def)
why3_vc add_def1 by simp why3_vc diff_def by simp
why3_vc diff_def1 by simp why3_vc diff_spec by (simp add: mem_def)
why3_vc mem_empty by simp why3_vc inter_def by simp
why3_vc add_remove why3_vc mem_empty by (simp add: const_def mem_def set.Set.is_empty_def)
using assms
by (auto simp add: remove_def)
why3_vc remove_add by (simp add: remove_def) why3_vc union_def by simp
why3_vc choose_def why3_vc add_remove
using assms using assms
by (auto simp add: is_empty_def choose_elt_def intro: someI_ex) by (simp add: fun_upd_idem_iff mem_def)
why3_vc empty_def1 by (simp add: is_empty_def) why3_vc inter_spec by (simp add: mem_def)
why3_vc inter_def1 by simp why3_vc remove_add by auto
why3_vc union_def1 by simp why3_vc union_spec
by (simp add: mem_def)
why3_vc remove_def1 by (auto simp add: remove_def) why3_vc choose_spec