Commit ab2b2058 authored by DAILLER Sylvain's avatar DAILLER Sylvain

Merge branch 'issue_288' into 'master'

Issue 288

Closes #288

See merge request !111
parents fb4cb734 acb16638
......@@ -1273,9 +1273,8 @@ ISABELLELIBS_REAL = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/r
ISABELLELIBS_NUMBER_FILES = Divisibility Gcd Parity Prime Coprime
ISABELLELIBS_NUMBER = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/number/, $(ISABELLELIBS_NUMBER_FILES)))
# broken
# ISABELLELIBS_SET_FILES = Set Fset
# ISABELLELIBS_SET = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/set/, $(ISABELLELIBS_SET_FILES)))
ISABELLELIBS_SET_FILES = Set Fset
ISABELLELIBS_SET = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/set/, $(ISABELLELIBS_SET_FILES)))
ISABELLELIBS_MAP_FILES = Map Const Occ MapPermut MapInjection
ISABELLELIBS_MAP = $(addsuffix .xml, $(addprefix $(GENERATED_PREFIX_ISABELLE)/map/, $(ISABELLELIBS_MAP_FILES)))
......@@ -1300,8 +1299,8 @@ drivers/isabelle-realizations.aux: Makefile
echo 'theory real.'"$$f"' meta "realized_theory" "real.'"$$f"'", "" end'; done; \
for f in $(ISABELLELIBS_NUMBER_FILES); do \
echo 'theory number.'"$$f"' meta "realized_theory" "number.'"$$f"'", "" end'; done; \
# for f in $(ISABELLELIBS_SET_FILES); do \
# echo 'theory set.'"$$f"' meta "realized_theory" "set.'"$$f"'", "" end'; done; \
for f in $(ISABELLELIBS_SET_FILES); do \
echo 'theory set.'"$$f"' meta "realized_theory" "set.'"$$f"'", "" end'; done; \
for f in $(ISABELLELIBS_MAP_FILES); do \
echo 'theory map.'"$$f"' meta "realized_theory" "map.'"$$f"'", "" end'; done; \
for f in $(ISABELLELIBS_LIST_FILES); do \
......
theory Why3
imports
Why3_Map
(* broken Why3_Set *)
Why3_Set
Why3_List
Why3_Int
Why3_Bool
......
......@@ -10,6 +10,9 @@ section {* Potentially infinite sets *}
definition complement :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where
"complement S v = Not (S v)"
definition mapi :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool)" where
"mapi f s x = Set.member x (image f (Collect s))"
why3_open "set/Set.xml"
constants
empty = bot
......@@ -19,41 +22,30 @@ why3_open "set/Set.xml"
inter = inf
diff = minus
complement = complement
choose = Eps
pick = Eps
all = top
map = mapi
why3_vc add_spec by (auto simp add: mem_def)
why3_vc diff_def by simp
why3_vc diff_def by (simp add: mem_def)
why3_vc diff_spec by (simp add: mem_def)
why3_vc inter_def by simp
why3_vc inter_def by (simp add: mem_def)
why3_vc is_empty_empty by (simp add: const_def mem_def set.Set.is_empty_def)
why3_vc union_def by simp
why3_vc union_def by (simp add: mem_def)
why3_vc add_remove
using assms
by (simp add: fun_upd_idem_iff mem_def)
why3_vc inter_spec by (simp add: mem_def)
why3_vc remove_add by auto
why3_vc union_spec
by (simp add: mem_def)
why3_vc choose_spec
why3_vc pick_def
using assms
by (auto simp add: mem_def is_empty_def intro: someI_ex)
why3_vc remove_spec
by (simp add: mem_def)
why3_vc subset_diff
by (simp add: diff_spec subset_def)
by (simp add: mem_def diff_def subset_def)
why3_vc subset_refl
by (simp add: subset_def)
......@@ -63,15 +55,49 @@ why3_vc subset_trans
by (simp add: subset_def)
why3_vc subset_remove
by (simp add: remove_spec subset_def)
by (simp add: mem_def remove_def subset_def)
why3_vc complement_def
by (simp add: complement_def)
by (simp add: mem_def complement_def)
why3_vc extensionality
using assms
by (auto simp add: infix_eqeq_def mem_def)
why3_vc map_def by (simp add: mem_def mapi_def image_iff)
why3_vc mem_map
using assms
by (meson facts.map_def mem_def)
why3_vc mem_singleton
by (metis assms const_def fun_upd_other mem_def)
why3_vc empty_is_empty
using assms
by (meson extensionality infix_eqeq_def is_empty_empty set.Set.is_empty_def)
why3_vc subset_inter_1
by (simp add: set.Set.subset_def mem_def)
why3_vc subset_inter_2
by (simp add: set.Set.subset_def mem_def)
why3_vc subset_union_1
by (simp add: set.Set.subset_def mem_def)
why3_vc subset_union_2
by (simp add: set.Set.subset_def mem_def)
why3_vc disjoint_diff_eq
by (smt diff_def disjoint_def extensionality infix_eqeq_def mem_def)
why3_vc disjoint_diff_s2
by (simp add: disjoint_def mem_def)
why3_vc disjoint_inter_empty
by (simp add: disjoint_def mem_def set.Set.is_empty_def)
why3_end
......@@ -86,6 +112,9 @@ definition fchoose :: "'a fset \<Rightarrow> 'a" where
definition is_empty :: "'a fset \<Rightarrow> bool" where
"is_empty S = (S = fempty)"
definition filter :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a fset" where
"filter S p = ffilter p S"
why3_open "set/Fset.xml"
constants
mem = fmember
......@@ -97,13 +126,13 @@ why3_open "set/Fset.xml"
diff = minus
choose = fchoose
all = top
infix_eqeq = HOL.eq
subset = fsubset_eq
is_empty = is_empty
pick = fchoose
filter = filter
map = fimage
types
set = fset
fset = fset
why3_vc add_spec by simp
why3_vc add_def by auto
why3_vc add_remove
using assms
......@@ -111,35 +140,39 @@ why3_vc add_remove
why3_vc remove_add by (simp add: fremove_def)
why3_vc empty_def by (simp add: is_empty_def)
why3_vc map_def by auto
why3_vc inter_spec by simp
why3_vc mem_map by (simp add: assms)
why3_vc union_spec by simp
why3_vc inter_def by simp
why3_vc remove_spec by (auto simp add: fremove_def)
why3_vc union_def by simp
why3_vc subset_diff by auto
why3_vc remove_def by (auto simp add: fremove_def)
why3_vc subset_refl by simp
why3_vc diff_def by auto
why3_vc subset_trans
why3_vc pick_def
using assms
by simp
by (auto simp add: fchoose_def is_empty_def intro: someI_ex)
why3_vc subset_remove by (auto simp add: fremove_def)
why3_vc subset_diff by (simp add: Fset.subset_def)
why3_vc subset_eq
using assms fcard_seteq by fastforce
why3_vc subset_refl by (simp add: Fset.subset_def)
why3_vc subset_spec by auto
why3_vc subset_trans
using assms
by (simp add: Fset.subset_def)
why3_vc infix_eqeq_spec
by (simp add: fset_eq_iff)
why3_vc subset_remove by (auto simp add: Fset.subset_def fremove_def)
why3_vc subset_eq
using assms fcard_seteq
by (metis Fset.subset_def eq_imp_le fsubsetI of_nat_eq_iff)
why3_vc extensionality
using assms
by simp
by (simp add: Fset.infix_eqeq_def fset_eqI)
why3_vc cardinal1
proof (cases s rule: fset_strong_cases)
......@@ -161,36 +194,76 @@ next
qed
qed
why3_vc cardinal_add
using assms
by (simp add: fcard_finsert_disjoint)
why3_vc cardinal_add by (auto simp add: fcard_finsert_if finsert_absorb)
why3_vc cardinal_empty by (simp add: is_empty_def)
why3_vc cardinal_nonneg by simp
why3_vc cardinal_remove
proof -
from assms
have "1 \<le> fcard s"
by (cases s rule: fset_strong_cases)
(auto simp add: fcard_finsert_disjoint)
with assms show ?thesis
by (simp add: fremove_def)
qed
lemma cardinal_remove_in:
"x |\<in>| s \<longrightarrow> int (fcard (fremove x s)) = int (fcard s) - 1"
by (smt cardinal_add(2) fminus_finsert_absorb fremove_def set_finsert)
lemma cardinal_remove_out:
"x |\<notin>| s \<longrightarrow> int (fcard (fremove x s)) = int (fcard s)"
by (simp add: fremove_def)
why3_vc cardinal_remove by (auto simp add: cardinal_remove_out cardinal_remove_in)
why3_vc cardinal_subset
using assms
by (simp add: fcard_mono)
by (simp add: Fset.subset_def fcard_mono fsubsetI)
why3_vc diff_spec by simp
why3_vc filter_def by (simp add: Why3_Set.filter_def)
why3_vc choose_spec
using assms
by (auto simp add: fchoose_def is_empty_def intro: someI_ex)
why3_vc cardinal_map
apply (simp add: fcard_def card_def)
by (metis card_def card_image_le finite_fset)
why3_vc cardinal_diff
by (smt fcard_funion_fsubset fcard_mono finter_lower1 fminus_finter2 inf.idem inf_commute int_ops(6) of_nat_mono)
why3_vc mem_singleton
using assms by auto
why3_vc subset_filter
by (simp add: Fset.subset_def Why3_Set.filter_def)
why3_vc cardinal_union
by (smt fcard_funion_finter of_nat_add)
why3_vc empty_is_empty
by (meson Fset.is_empty_def assms bot.extremum_uniqueI fsubsetI)
why3_vc is_empty_empty
by (simp add: cardinal_empty)
why3_vc subset_inter_1
by (simp add: Fset.subset_def)
why3_vc subset_inter_2
by (simp add: Fset.subset_def)
why3_vc subset_union_1
by (simp add: Fset.subset_def)
why3_vc subset_union_2
by (simp add: Fset.subset_def)
why3_vc cardinal_filter
using cardinal_subset subset_filter by blast
why3_vc disjoint_diff_eq
by (smt Fset.disjoint_def Fset.facts.diff_def fsubsetI fsubset_antisym)
why3_vc disjoint_diff_s2
by (simp add: Fset.facts.disjoint_diff_eq)
why3_vc disjoint_inter_empty
by (metis Fset.facts.disjoint_diff_eq Fset.facts.empty_is_empty Fset.facts.is_empty_empty fminus_disjoint fminus_triv)
why3_vc is_empty_spec
by (simp add: Why3_Set.is_empty_def)
why3_vc cardinal_inter_disjoint
by (meson Fset.facts.disjoint_inter_empty assms cardinal_empty)
why3_end
......
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