--- a/Nominal/FSet.thy Fri Oct 15 14:11:23 2010 +0100
+++ b/Nominal/FSet.thy Fri Oct 15 15:47:20 2010 +0100
@@ -48,13 +48,6 @@
where
"fcard_raw xs = card (set xs)"
-(*
-definition
- finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
-where
- "finter_raw xs ys \<equiv> [x \<leftarrow> xs. x\<notin>set ys]"
-*)
-
primrec
finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
where
@@ -62,11 +55,12 @@
| "finter_raw (x # xs) ys =
(if x \<in> set ys then x # (finter_raw xs ys) else finter_raw xs ys)"
-primrec
+
+definition
fminus_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
where
- "fminus_raw ys [] = ys"
-| "fminus_raw ys (x # xs) = fminus_raw (removeAll x ys) xs"
+ "fminus_raw xs ys \<equiv> [x \<leftarrow> xs. x\<notin>set ys]"
+
definition
rsp_fold
@@ -91,8 +85,7 @@
lemma set_fminus_raw[simp]:
shows "set (fminus_raw xs ys) = (set xs - set ys)"
- by (induct ys arbitrary: xs) (auto)
-
+ by (auto simp add: fminus_raw_def)
section {* Quotient composition lemmas *}
@@ -405,11 +398,13 @@
end
-section {* Finsert and Membership *}
+
+section {* Definitions for fsets *}
+
quotient_definition
"finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-is "Cons"
+ is "Cons"
syntax
"@Finset" :: "args => 'a fset" ("{|(_)|}")
@@ -432,13 +427,11 @@
quotient_definition
"fcard :: 'a fset \<Rightarrow> nat"
-is
- fcard_raw
+ is fcard_raw
quotient_definition
"fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
-is
- map
+ is map
quotient_definition
"fdelete :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
@@ -450,19 +443,18 @@
quotient_definition
"ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b"
- is "ffold_raw"
+ is ffold_raw
quotient_definition
"fconcat :: ('a fset) fset \<Rightarrow> 'a fset"
-is
- "concat"
+ is concat
quotient_definition
"ffilter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-is
- "filter"
+ is filter
-text {* Compositional Respectfullness and Preservation *}
+
+subsection {* Compositional Respectfulness and Preservation *}
lemma [quot_respect]: "(list_all2 op \<approx> OOO op \<approx>) [] []"
by (fact compose_list_refl)
@@ -545,58 +537,9 @@
by (rule pred_compI) (rule a', rule d')
qed
-text {* Raw theorems. Finsert, memb, singleron, sub_list *}
-
-lemma nil_not_cons:
- shows "\<not> ([] \<approx> x # xs)"
- and "\<not> (x # xs \<approx> [])"
- by auto
-
-lemma no_memb_nil:
- "(\<forall>x. \<not> memb x xs) = (xs = [])"
- by (simp add: memb_def)
-
-lemma memb_consI1:
- shows "memb x (x # xs)"
- by (simp add: memb_def)
-
-lemma memb_consI2:
- shows "memb x xs \<Longrightarrow> memb x (y # xs)"
- by (simp add: memb_def)
-
-lemma singleton_list_eq:
- shows "[x] \<approx> [y] \<longleftrightarrow> x = y"
- by (simp)
-
-lemma sub_list_cons:
- "sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)"
- by (auto simp add: memb_def sub_list_def)
-
-lemma fminus_raw_red:
- "fminus_raw (x # xs) ys = (if x \<in> set ys then fminus_raw xs ys else x # (fminus_raw xs ys))"
- by (induct ys arbitrary: xs x) (simp_all)
-
-text {* Cardinality of finite sets *}
-
-(* used in memb_card_not_0 *)
-lemma fcard_raw_0:
- shows "fcard_raw xs = 0 \<longleftrightarrow> xs \<approx> []"
- unfolding fcard_raw_def
- by (induct xs) (auto)
-
-(* used in list_eq2_equiv *)
-lemma memb_card_not_0:
- assumes a: "memb a A"
- shows "\<not>(fcard_raw A = 0)"
-proof -
- have "\<not>(\<forall>x. \<not> memb x A)" using a by auto
- then have "\<not>A \<approx> []" by (simp add: memb_def)
- then show ?thesis using fcard_raw_0[of A] by simp
-qed
-
-section {* ? *}
+section {* Cases *}
lemma fset_raw_strong_cases:
@@ -609,7 +552,8 @@
case (Cons a xs)
have a: "\<lbrakk>xs = [] \<Longrightarrow> thesis; \<And>x ys. \<lbrakk>\<not> memb x ys; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis" by fact
have b: "\<And>x' ys'. \<lbrakk>\<not> memb x' ys'; a # xs \<approx> x' # ys'\<rbrakk> \<Longrightarrow> thesis" by fact
- have c: "xs = [] \<Longrightarrow> thesis" by (metis no_memb_nil singleton_list_eq b)
+ have c: "xs = [] \<Longrightarrow> thesis" using b unfolding memb_def
+ by (metis in_set_conv_nth less_zeroE list.size(3) list_eq.simps member_set)
have "\<And>x ys. \<lbrakk>\<not> memb x ys; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis"
proof -
fix x :: 'a
@@ -632,24 +576,6 @@
then show thesis using a c by blast
qed
-section {* deletion *}
-
-
-lemma fset_raw_removeAll_cases:
- "xs = [] \<or> (\<exists>x. memb x xs \<and> xs \<approx> x # removeAll x xs)"
- by (induct xs) (auto simp add: memb_def)
-
-lemma fremoveAll_filter:
- "removeAll y xs = [x \<leftarrow> xs. x \<noteq> y]"
- by (induct xs) simp_all
-
-lemma fcard_raw_delete:
- "fcard_raw (removeAll y xs) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
- by (auto simp add: fcard_raw_def memb_def)
-
-lemma inj_map_eq_iff:
- "inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)"
- by (simp add: set_eq_iff[symmetric] inj_image_eq_iff)
text {* alternate formulation with a different decomposition principle
and a proof of equivalence *}
@@ -702,8 +628,8 @@
proof (induct n arbitrary: l r)
case 0
have "fcard_raw l = 0" by fact
- then have "\<forall>x. \<not> memb x l" using memb_card_not_0[of _ l] by auto
- then have z: "l = []" using no_memb_nil by auto
+ then have "\<forall>x. \<not> memb x l" unfolding fcard_raw_def memb_def by auto
+ then have z: "l = []" unfolding memb_def by auto
then have "r = []" using `l \<approx> r` by simp
then show ?case using z list_eq2_refl by simp
next
@@ -718,7 +644,7 @@
then obtain a where e: "memb a l" by auto
then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b
unfolding memb_def by auto
- have f: "fcard_raw (removeAll a l) = m" using fcard_raw_delete[of a l] e d by simp
+ have f: "fcard_raw (removeAll a l) = m" using e d by (simp add: fcard_raw_def memb_def)
have g: "removeAll a l \<approx> removeAll a r" using removeAll_rsp b by simp
have "list_eq2 (removeAll a l) (removeAll a r)" by (rule Suc.hyps[OF f g])
then have h: "list_eq2 (a # removeAll a l) (a # removeAll a r)" by (rule list_eq2.intros(5))
@@ -731,35 +657,59 @@
then show "l \<approx> r \<Longrightarrow> list_eq2 l r" by blast
qed
-text {* Lifted theorems *}
+
+section {* Lifted theorems *}
+
+
+subsection {* fin *}
-lemma not_fin_fnil: "x |\<notin>| {||}"
+lemma not_fin_fnil:
+ shows "x |\<notin>| {||}"
+ by (descending) (simp add: memb_def)
+
+lemma fin_set:
+ shows "x |\<in>| S \<longleftrightarrow> x \<in> fset S"
by (descending) (simp add: memb_def)
+lemma fnotin_set:
+ shows "x |\<notin>| S \<longleftrightarrow> x \<notin> fset S"
+ by (descending) (simp add: memb_def)
+
+lemma fset_eq_iff:
+ shows "S = T \<longleftrightarrow> (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
+ by (descending) (auto simp add: memb_def)
+
+lemma none_fin_fempty:
+ shows "(\<forall>x. x |\<notin>| S) \<longleftrightarrow> S = {||}"
+ by (descending) (simp add: memb_def)
+
+
+subsection {* finsert *}
+
lemma fin_finsert_iff[simp]:
- "x |\<in>| finsert y S \<longleftrightarrow> x = y \<or> x |\<in>| S"
+ shows "x |\<in>| finsert y S \<longleftrightarrow> x = y \<or> x |\<in>| S"
by (descending) (simp add: memb_def)
lemma
shows finsertI1: "x |\<in>| finsert x S"
and finsertI2: "x |\<in>| S \<Longrightarrow> x |\<in>| finsert y S"
- by (lifting memb_consI1 memb_consI2)
+ by (descending, simp add: memb_def)+
lemma finsert_absorb[simp]:
shows "x |\<in>| S \<Longrightarrow> finsert x S = S"
by (descending) (auto simp add: memb_def)
lemma fempty_not_finsert[simp]:
- "{||} \<noteq> finsert x S"
- "finsert x S \<noteq> {||}"
- by (lifting nil_not_cons)
+ shows "{||} \<noteq> finsert x S"
+ and "finsert x S \<noteq> {||}"
+ by (descending, simp)+
lemma finsert_left_comm:
- "finsert x (finsert y S) = finsert y (finsert x S)"
+ shows "finsert x (finsert y S) = finsert y (finsert x S)"
by (descending) (auto)
lemma finsert_left_idem:
- "finsert x (finsert x S) = finsert x S"
+ shows "finsert x (finsert x S) = finsert x S"
by (descending) (auto)
lemma fsingleton_eq[simp]:
@@ -767,27 +717,199 @@
by (descending) (auto)
-text {* fset *}
+(* FIXME: is this in any case a useful lemma *)
+lemma fin_mdef:
+ shows "x |\<in>| F \<longleftrightarrow> x |\<notin>| (F - {|x|}) \<and> F = finsert x (F - {|x|})"
+ by (descending) (auto simp add: memb_def fminus_raw_def)
+
+
+subsection {* fset *}
lemma fset_simps[simp]:
"fset {||} = ({} :: 'a set)"
"fset (finsert (x :: 'a) S) = insert x (fset S)"
by (lifting set.simps)
-lemma fin_fset:
- "x \<in> fset S \<longleftrightarrow> x |\<in>| S"
- by (lifting memb_def[symmetric])
+lemma finite_fset [simp]:
+ shows "finite (fset S)"
+ by (descending) (simp)
+
+lemma fset_cong:
+ shows "fset S = fset T \<longleftrightarrow> S = T"
+ by (descending) (simp)
+
+lemma ffilter_set [simp]:
+ shows "fset (ffilter P xs) = P \<inter> fset xs"
+ by (descending) (auto simp add: mem_def)
+
+lemma fdelete_set [simp]:
+ shows "fset (fdelete x xs) = fset xs - {x}"
+ by (descending) (simp)
+
+lemma finter_set [simp]:
+ shows "fset (xs |\<inter>| ys) = fset xs \<inter> fset ys"
+ by (lifting set_finter_raw)
+
+lemma funion_set [simp]:
+ shows "fset (xs |\<union>| ys) = fset xs \<union> fset ys"
+ by (lifting set_append)
+
+lemma fminus_set [simp]:
+ shows "fset (xs - ys) = fset xs - fset ys"
+ by (lifting set_fminus_raw)
+
+
+subsection {* funion *}
+
+lemmas [simp] =
+ sup_bot_left[where 'a="'a fset", standard]
+ sup_bot_right[where 'a="'a fset", standard]
+
+lemma funion_finsert[simp]:
+ shows "finsert x S |\<union>| T = finsert x (S |\<union>| T)"
+ by (lifting append.simps(2))
+
+lemma singleton_funion_left:
+ shows "{|a|} |\<union>| S = finsert a S"
+ by simp
-lemma none_fin_fempty:
- "(\<forall>x. x |\<notin>| S) \<longleftrightarrow> S = {||}"
+lemma singleton_funion_right:
+ shows "S |\<union>| {|a|} = finsert a S"
+ by (subst sup.commute) simp
+
+lemma fin_funion:
+ shows "x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"
+ by (descending) (simp add: memb_def)
+
+
+subsection {* fminus *}
+
+lemma fminus_fin:
+ shows "x |\<in>| (xs - ys) \<longleftrightarrow> x |\<in>| xs \<and> x |\<notin>| ys"
+ by (descending) (simp add: memb_def)
+
+lemma fminus_red:
+ shows "finsert x xs - ys = (if x |\<in>| ys then xs - ys else finsert x (xs - ys))"
+ by (descending) (auto simp add: memb_def)
+
+lemma fminus_red_fin[simp]:
+ shows "x |\<in>| ys \<Longrightarrow> finsert x xs - ys = xs - ys"
+ by (simp add: fminus_red)
+
+lemma fminus_red_fnotin[simp]:
+ shows "x |\<notin>| ys \<Longrightarrow> finsert x xs - ys = finsert x (xs - ys)"
+ by (simp add: fminus_red)
+
+lemma fin_fminus_fnotin:
+ shows "x |\<in>| F - S \<Longrightarrow> x |\<notin>| S"
+ unfolding fin_set fminus_set
+ by blast
+
+lemma fin_fnotin_fminus:
+ shows "x |\<in>| S \<Longrightarrow> x |\<notin>| F - S"
+ unfolding fin_set fminus_set
+ by blast
+
+
+section {* fdelete *}
+
+lemma fin_fdelete:
+ shows "x |\<in>| fdelete y S \<longleftrightarrow> x |\<in>| S \<and> x \<noteq> y"
by (descending) (simp add: memb_def)
-lemma fset_cong:
- "S = T \<longleftrightarrow> fset S = fset T"
- by (lifting list_eq.simps)
+lemma fnotin_fdelete:
+ shows "x |\<notin>| fdelete x S"
+ by (descending) (simp add: memb_def)
+
+lemma fnotin_fdelete_ident:
+ shows "x |\<notin>| S \<Longrightarrow> fdelete x S = S"
+ by (descending) (simp add: memb_def)
+
+lemma fset_fdelete_cases:
+ shows "S = {||} \<or> (\<exists>x. x |\<in>| S \<and> S = finsert x (fdelete x S))"
+ by (descending) (auto simp add: memb_def insert_absorb)
+
+
+section {* finter *}
+
+lemma finter_empty_l:
+ shows "{||} |\<inter>| S = {||}"
+ by simp
+
+lemma finter_empty_r:
+ shows "S |\<inter>| {||} = {||}"
+ by simp
+
+lemma finter_finsert:
+ shows "finsert x S |\<inter>| T = (if x |\<in>| T then finsert x (S |\<inter>| T) else S |\<inter>| T)"
+ by (descending) (simp add: memb_def)
+
+lemma fin_finter:
+ shows "x |\<in>| (S |\<inter>| T) \<longleftrightarrow> x |\<in>| S \<and> x |\<in>| T"
+ by (descending) (simp add: memb_def)
-section {* fcard *}
+subsection {* fsubset *}
+
+lemma fsubseteq_set:
+ shows "xs |\<subseteq>| ys \<longleftrightarrow> fset xs \<subseteq> fset ys"
+ by (descending) (simp add: sub_list_def)
+
+lemma fsubset_set:
+ shows "xs |\<subset>| ys \<longleftrightarrow> fset xs \<subset> fset ys"
+ unfolding less_fset_def
+ by (descending) (auto simp add: sub_list_def)
+
+lemma fsubseteq_finsert:
+ shows "(finsert x xs) |\<subseteq>| ys \<longleftrightarrow> x |\<in>| ys \<and> xs |\<subseteq>| ys"
+ by (descending) (simp add: sub_list_def memb_def)
+
+lemma fsubset_fin:
+ shows "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)"
+ by (descending) (auto simp add: sub_list_def memb_def)
+
+(* FIXME: no type ord *)
+(*
+lemma fsubset_finsert:
+ shows "(finsert x xs) |\<subset>| ys \<longleftrightarrow> x |\<in>| ys \<and> xs |\<subset>| ys"
+ by (descending) (simp add: sub_list_def memb_def)
+*)
+
+lemma fsubseteq_fempty:
+ shows "xs |\<subseteq>| {||} \<longleftrightarrow> xs = {||}"
+ by (descending) (simp add: sub_list_def)
+
+(* also problem with ord *)
+lemma not_fsubset_fnil:
+ shows "\<not> xs |\<subset>| {||}"
+ by (metis fset_simps(1) fsubset_set not_psubset_empty)
+
+
+section {* fmap *}
+
+lemma fmap_simps [simp]:
+ shows "fmap f {||} = {||}"
+ and "fmap f (finsert x S) = finsert (f x) (fmap f S)"
+ by (descending, simp)+
+
+lemma fmap_set_image [simp]:
+ shows "fset (fmap f S) = f ` (fset S)"
+ by (descending) (simp)
+
+lemma inj_fmap_eq_iff:
+ shows "inj f \<Longrightarrow> fmap f S = fmap f T \<longleftrightarrow> S = T"
+ by (descending) (metis inj_vimage_image_eq list_eq.simps set_map)
+
+lemma fmap_funion:
+ shows "fmap f (S |\<union>| T) = fmap f S |\<union>| fmap f T"
+ by (descending) (simp)
+
+
+subsection {* fcard *}
+
+lemma fcard_set:
+ shows "fcard xs = card (fset xs)"
+ by (lifting fcard_raw_def)
lemma fcard_finsert_if [simp]:
shows "fcard (finsert x S) = (if x |\<in>| S then fcard S else Suc (fcard S))"
@@ -816,7 +938,7 @@
lemma fcard_suc:
shows "fcard S = Suc n \<Longrightarrow> \<exists>x T. x |\<notin>| T \<and> S = finsert x T \<and> fcard T = n"
apply(descending)
- apply(simp add: fcard_raw_def memb_def)
+ apply(auto simp add: fcard_raw_def memb_def)
apply(drule card_eq_SucD)
apply(auto)
apply(rule_tac x="b" in exI)
@@ -825,8 +947,8 @@
done
lemma fcard_delete:
- "fcard (fdelete y S) = (if y |\<in>| S then fcard S - 1 else fcard S)"
- by (lifting fcard_raw_delete)
+ shows "fcard (fdelete y S) = (if y |\<in>| S then fcard S - 1 else fcard S)"
+ by (descending) (simp add: fcard_raw_def memb_def)
lemma fcard_suc_memb:
shows "fcard A = Suc n \<Longrightarrow> \<exists>a. a |\<in>| A"
@@ -840,24 +962,135 @@
shows "a |\<in>| A \<Longrightarrow> fcard A \<noteq> 0"
by (descending) (auto simp add: fcard_raw_def memb_def)
+lemma fcard_mono:
+ shows "xs |\<subseteq>| ys \<Longrightarrow> fcard xs \<le> fcard ys"
+ unfolding fcard_set fsubseteq_set
+ by (simp add: card_mono[OF finite_fset])
-section {* funion *}
+lemma fcard_fsubset_eq:
+ shows "xs |\<subseteq>| ys \<Longrightarrow> fcard ys \<le> fcard xs \<Longrightarrow> xs = ys"
+ unfolding fcard_set fsubseteq_set
+ by (auto dest: card_seteq[OF finite_fset] simp add: fset_cong)
+
+lemma psubset_fcard_mono:
+ shows "xs |\<subset>| ys \<Longrightarrow> fcard xs < fcard ys"
+ unfolding fcard_set fsubset_set
+ by (rule psubset_card_mono[OF finite_fset])
+
+lemma fcard_funion_finter:
+ shows "fcard xs + fcard ys = fcard (xs |\<union>| ys) + fcard (xs |\<inter>| ys)"
+ unfolding fcard_set funion_set finter_set
+ by (rule card_Un_Int[OF finite_fset finite_fset])
+
+lemma fcard_funion_disjoint:
+ shows "xs |\<inter>| ys = {||} \<Longrightarrow> fcard (xs |\<union>| ys) = fcard xs + fcard ys"
+ unfolding fcard_set funion_set
+ apply (rule card_Un_disjoint[OF finite_fset finite_fset])
+ by (metis finter_set fset_simps(1))
+
+lemma fcard_delete1_less:
+ shows "x |\<in>| xs \<Longrightarrow> fcard (fdelete x xs) < fcard xs"
+ unfolding fcard_set fin_set fdelete_set
+ by (rule card_Diff1_less[OF finite_fset])
-lemmas [simp] =
- sup_bot_left[where 'a="'a fset", standard]
- sup_bot_right[where 'a="'a fset", standard]
+lemma fcard_delete2_less:
+ shows "x |\<in>| xs \<Longrightarrow> y |\<in>| xs \<Longrightarrow> fcard (fdelete y (fdelete x xs)) < fcard xs"
+ unfolding fcard_set fdelete_set fin_set
+ by (rule card_Diff2_less[OF finite_fset])
+
+lemma fcard_delete1_le:
+ shows "fcard (fdelete x xs) \<le> fcard xs"
+ unfolding fdelete_set fcard_set
+ by (rule card_Diff1_le[OF finite_fset])
+
+lemma fcard_psubset:
+ shows "ys |\<subseteq>| xs \<Longrightarrow> fcard ys < fcard xs \<Longrightarrow> ys |\<subset>| xs"
+ unfolding fcard_set fsubseteq_set fsubset_set
+ by (rule card_psubset[OF finite_fset])
+
+lemma fcard_fmap_le:
+ shows "fcard (fmap f xs) \<le> fcard xs"
+ unfolding fcard_set fmap_set_image
+ by (rule card_image_le[OF finite_fset])
+
+lemma fcard_fminus_finsert[simp]:
+ assumes "a |\<in>| A" and "a |\<notin>| B"
+ shows "fcard (A - finsert a B) = fcard (A - B) - 1"
+ using assms
+ unfolding fin_set fcard_set fminus_set
+ by (simp add: card_Diff_insert[OF finite_fset])
+
+lemma fcard_fminus_fsubset:
+ assumes "B |\<subseteq>| A"
+ shows "fcard (A - B) = fcard A - fcard B"
+ using assms
+ unfolding fsubseteq_set fcard_set fminus_set
+ by (rule card_Diff_subset[OF finite_fset])
-lemma funion_finsert[simp]:
- shows "finsert x S |\<union>| T = finsert x (S |\<union>| T)"
- by (lifting append.simps(2))
+lemma fcard_fminus_subset_finter:
+ shows "fcard (A - B) = fcard A - fcard (A |\<inter>| B)"
+ unfolding finter_set fcard_set fminus_set
+ by (rule card_Diff_subset_Int) (simp)
+
+
+section {* fconcat *}
+
+lemma fconcat_fempty:
+ shows "fconcat {||} = {||}"
+ by (lifting concat.simps(1))
+
+lemma fconcat_finsert:
+ shows "fconcat (finsert x S) = x |\<union>| fconcat S"
+ by (lifting concat.simps(2))
+
+lemma fconcat_finter:
+ shows "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys"
+ by (lifting concat_append)
+
+
+section {* ffilter *}
+
+lemma subseteq_filter:
+ shows "ffilter P xs <= ffilter Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)"
+ by (descending) (auto simp add: memb_def sub_list_def)
+
+lemma eq_ffilter:
+ shows "(ffilter P xs = ffilter Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)"
+ by (descending) (auto simp add: memb_def)
-lemma singleton_union_left:
- shows "{|a|} |\<union>| S = finsert a S"
- by simp
+lemma subset_ffilter:
+ shows "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> ffilter P xs < ffilter Q xs"
+ unfolding less_fset_def by (auto simp add: subseteq_filter eq_ffilter)
+
+
+subsection {* ffold *}
+
+lemma ffold_nil:
+ shows "ffold f z {||} = z"
+ by (descending) (simp)
+
+lemma ffold_finsert: "ffold f z (finsert a A) =
+ (if rsp_fold f then if a |\<in>| A then ffold f z A else f a (ffold f z A) else z)"
+ by (descending) (simp add: memb_def)
-lemma singleton_union_right:
- shows "S |\<union>| {|a|} = finsert a S"
- by (subst sup.commute) simp
+lemma fin_commute_ffold:
+ "\<lbrakk>rsp_fold f; h |\<in>| b\<rbrakk> \<Longrightarrow> ffold f z b = f h (ffold f z (fdelete h b))"
+ by (descending) (simp add: memb_def memb_commute_ffold_raw)
+
+
+subsection {* Choice in fsets *}
+
+lemma fset_choice:
+ assumes a: "\<forall>x. x |\<in>| A \<longrightarrow> (\<exists>y. P x y)"
+ shows "\<exists>f. \<forall>x. x |\<in>| A \<longrightarrow> P x (f x)"
+ using a
+ apply(descending)
+ using finite_set_choice
+ by (auto simp add: memb_def Ball_def)
+
+
+(* FIXME: is that in any way useful *)
+
section {* Induction and Cases rules for fsets *}
@@ -917,160 +1150,6 @@
qed
-section {* fmap *}
-
-lemma fmap_simps[simp]:
- fixes f::"'a \<Rightarrow> 'b"
- shows "fmap f {||} = {||}"
- and "fmap f (finsert x S) = finsert (f x) (fmap f S)"
- by (lifting map.simps)
-
-lemma fmap_set_image:
- "fset (fmap f S) = f ` (fset S)"
- by (induct S) simp_all
-
-lemma inj_fmap_eq_iff:
- "inj f \<Longrightarrow> fmap f S = fmap f T \<longleftrightarrow> S = T"
- by (lifting inj_map_eq_iff)
-
-lemma fmap_funion:
- shows "fmap f (S |\<union>| T) = fmap f S |\<union>| fmap f T"
- by (descending) (simp)
-
-lemma fin_funion:
- shows "x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"
- by (descending) (simp add: memb_def)
-
-section {* fset *}
-
-lemma fin_set:
- shows "x |\<in>| xs \<longleftrightarrow> x \<in> fset xs"
- by (lifting memb_def)
-
-lemma fnotin_set:
- shows "x |\<notin>| xs \<longleftrightarrow> x \<notin> fset xs"
- by (simp add: fin_set)
-
-lemma fcard_set:
- shows "fcard xs = card (fset xs)"
- by (lifting fcard_raw_def)
-
-lemma fsubseteq_set:
- shows "xs |\<subseteq>| ys \<longleftrightarrow> fset xs \<subseteq> fset ys"
- by (lifting sub_list_def)
-
-lemma fsubset_set:
- shows "xs |\<subset>| ys \<longleftrightarrow> fset xs \<subset> fset ys"
- unfolding less_fset_def
- by (descending) (auto simp add: sub_list_def)
-
-lemma ffilter_set [simp]:
- shows "fset (ffilter P xs) = P \<inter> fset xs"
- by (descending) (auto simp add: mem_def)
-
-lemma fdelete_set [simp]:
- shows "fset (fdelete x xs) = fset xs - {x}"
- by (lifting set_removeAll)
-
-lemma finter_set [simp]:
- shows "fset (xs |\<inter>| ys) = fset xs \<inter> fset ys"
- by (lifting set_finter_raw)
-
-lemma funion_set [simp]:
- shows "fset (xs |\<union>| ys) = fset xs \<union> fset ys"
- by (lifting set_append)
-
-lemma fminus_set [simp]:
- shows "fset (xs - ys) = fset xs - fset ys"
- by (lifting set_fminus_raw)
-
-
-
-section {* ffold *}
-
-lemma ffold_nil:
- shows "ffold f z {||} = z"
- by (lifting ffold_raw.simps(1)[where 'a="'b" and 'b="'a"])
-
-lemma ffold_finsert: "ffold f z (finsert a A) =
- (if rsp_fold f then if a |\<in>| A then ffold f z A else f a (ffold f z A) else z)"
- by (descending) (simp add: memb_def)
-
-lemma fin_commute_ffold:
- "\<lbrakk>rsp_fold f; h |\<in>| b\<rbrakk> \<Longrightarrow> ffold f z b = f h (ffold f z (fdelete h b))"
- by (descending) (simp add: memb_def memb_commute_ffold_raw)
-
-
-
-section {* fdelete *}
-
-lemma fin_fdelete:
- shows "x |\<in>| fdelete y S \<longleftrightarrow> x |\<in>| S \<and> x \<noteq> y"
- by (descending) (simp add: memb_def)
-
-lemma fnotin_fdelete:
- shows "x |\<notin>| fdelete x S"
- by (descending) (simp add: memb_def)
-
-lemma fnotin_fdelete_ident:
- shows "x |\<notin>| S \<Longrightarrow> fdelete x S = S"
- by (descending) (simp add: memb_def)
-
-lemma fset_fdelete_cases:
- shows "S = {||} \<or> (\<exists>x. x |\<in>| S \<and> S = finsert x (fdelete x S))"
- by (lifting fset_raw_removeAll_cases)
-
-
-section {* finter *}
-
-lemma finter_empty_l:
- shows "{||} |\<inter>| S = {||}"
- by simp
-
-lemma finter_empty_r:
- shows "S |\<inter>| {||} = {||}"
- by simp
-
-lemma finter_finsert:
- shows "finsert x S |\<inter>| T = (if x |\<in>| T then finsert x (S |\<inter>| T) else S |\<inter>| T)"
- by (descending) (simp add: memb_def)
-
-lemma fin_finter:
- shows "x |\<in>| (S |\<inter>| T) \<longleftrightarrow> x |\<in>| S \<and> x |\<in>| T"
- by (descending) (simp add: memb_def)
-
-lemma fsubset_finsert:
- shows "finsert x xs |\<subseteq>| ys \<longleftrightarrow> x |\<in>| ys \<and> xs |\<subseteq>| ys"
- by (lifting sub_list_cons)
-
-lemma
- shows "xs |\<subseteq>| ys \<equiv> \<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys"
- by (descending) (auto simp add: sub_list_def memb_def)
-
-lemma fsubset_fin:
- shows "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)"
- by (descending) (auto simp add: sub_list_def memb_def)
-
-lemma fminus_fin:
- shows "x |\<in>| xs - ys \<longleftrightarrow> x |\<in>| xs \<and> x |\<notin>| ys"
- by (descending) (simp add: memb_def)
-
-lemma fminus_red:
- shows "finsert x xs - ys = (if x |\<in>| ys then xs - ys else finsert x (xs - ys))"
- by (descending) (auto simp add: memb_def)
-
-lemma fminus_red_fin[simp]:
- shows "x |\<in>| ys \<Longrightarrow> finsert x xs - ys = xs - ys"
- by (simp add: fminus_red)
-
-lemma fminus_red_fnotin[simp]:
- shows "x |\<notin>| ys \<Longrightarrow> finsert x xs - ys = finsert x (xs - ys)"
- by (simp add: fminus_red)
-
-lemma fset_eq_iff:
- shows "S = T \<longleftrightarrow> (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
- by (descending) (auto simp add: memb_def)
-
(* We cannot write it as "assumes .. shows" since Isabelle changes
the quantifiers to schematic variables and reintroduces them in
a different order *)
@@ -1097,143 +1176,12 @@
by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]])
-section {* fconcat *}
-
-lemma fconcat_empty:
- shows "fconcat {||} = {||}"
- by (lifting concat.simps(1))
-
-lemma fconcat_insert:
- shows "fconcat (finsert x S) = x |\<union>| fconcat S"
- by (lifting concat.simps(2))
-
-lemma
- shows "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys"
- by (lifting concat_append)
-
-
-section {* ffilter *}
-
-lemma subseteq_filter:
- shows "ffilter P xs <= ffilter Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)"
- by (descending) (auto simp add: memb_def sub_list_def)
-
-lemma eq_ffilter:
- shows "(ffilter P xs = ffilter Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)"
- by (descending) (auto simp add: memb_def)
-
-lemma subset_ffilter:
- shows "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> ffilter P xs < ffilter Q xs"
- unfolding less_fset_def by (auto simp add: subseteq_filter eq_ffilter)
-
section {* lemmas transferred from Finite_Set theory *}
text {* finiteness for finite sets holds *}
-lemma finite_fset [simp]:
- shows "finite (fset S)"
- by (induct S) auto
-
-lemma fset_choice:
- shows "\<forall>x. x |\<in>| A \<longrightarrow> (\<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. x |\<in>| A \<longrightarrow> P x (f x)"
- apply(descending)
- apply(simp add: memb_def)
- apply(rule finite_set_choice[simplified Ball_def])
- apply(simp_all)
- done
-
-lemma fsubseteq_fempty:
- shows "xs |\<subseteq>| {||} \<longleftrightarrow> xs = {||}"
- by (metis finter_empty_r le_iff_inf)
-
-lemma not_fsubset_fnil:
- shows "\<not> xs |\<subset>| {||}"
- by (metis fset_simps(1) fsubset_set not_psubset_empty)
-
-lemma fcard_mono:
- shows "xs |\<subseteq>| ys \<Longrightarrow> fcard xs \<le> fcard ys"
- unfolding fcard_set fsubseteq_set
- by (rule card_mono[OF finite_fset])
-
-lemma fcard_fseteq:
- shows "xs |\<subseteq>| ys \<Longrightarrow> fcard ys \<le> fcard xs \<Longrightarrow> xs = ys"
- unfolding fcard_set fsubseteq_set
- by (simp add: card_seteq[OF finite_fset] fset_cong)
-
-lemma psubset_fcard_mono:
- shows "xs |\<subset>| ys \<Longrightarrow> fcard xs < fcard ys"
- unfolding fcard_set fsubset_set
- by (rule psubset_card_mono[OF finite_fset])
-
-lemma fcard_funion_finter:
- shows "fcard xs + fcard ys = fcard (xs |\<union>| ys) + fcard (xs |\<inter>| ys)"
- unfolding fcard_set funion_set finter_set
- by (rule card_Un_Int[OF finite_fset finite_fset])
-
-lemma fcard_funion_disjoint:
- shows "xs |\<inter>| ys = {||} \<Longrightarrow> fcard (xs |\<union>| ys) = fcard xs + fcard ys"
- unfolding fcard_set funion_set
- apply (rule card_Un_disjoint[OF finite_fset finite_fset])
- by (metis finter_set fset_simps(1))
-
-lemma fcard_delete1_less:
- shows "x |\<in>| xs \<Longrightarrow> fcard (fdelete x xs) < fcard xs"
- unfolding fcard_set fin_set fdelete_set
- by (rule card_Diff1_less[OF finite_fset])
-lemma fcard_delete2_less:
- shows "x |\<in>| xs \<Longrightarrow> y |\<in>| xs \<Longrightarrow> fcard (fdelete y (fdelete x xs)) < fcard xs"
- unfolding fcard_set fdelete_set fin_set
- by (rule card_Diff2_less[OF finite_fset])
-lemma fcard_delete1_le:
- shows "fcard (fdelete x xs) \<le> fcard xs"
- unfolding fdelete_set fcard_set
- by (rule card_Diff1_le[OF finite_fset])
-
-lemma fcard_psubset:
- shows "ys |\<subseteq>| xs \<Longrightarrow> fcard ys < fcard xs \<Longrightarrow> ys |\<subset>| xs"
- unfolding fcard_set fsubseteq_set fsubset_set
- by (rule card_psubset[OF finite_fset])
-
-lemma fcard_fmap_le:
- shows "fcard (fmap f xs) \<le> fcard xs"
- unfolding fcard_set fmap_set_image
- by (rule card_image_le[OF finite_fset])
-
-lemma fin_fminus_fnotin:
- shows "x |\<in>| F - S \<Longrightarrow> x |\<notin>| S"
- unfolding fin_set fminus_set
- by blast
-
-lemma fin_fnotin_fminus:
- shows "x |\<in>| S \<Longrightarrow> x |\<notin>| F - S"
- unfolding fin_set fminus_set
- by blast
-
-lemma fin_mdef:
- shows "x |\<in>| F \<longleftrightarrow> x |\<notin>| (F - {|x|}) \<and> F = finsert x (F - {|x|})"
- unfolding fin_set fset_simps fset_cong fminus_set
- by blast
-
-lemma fcard_fminus_finsert[simp]:
- assumes "a |\<in>| A" and "a |\<notin>| B"
- shows "fcard (A - finsert a B) = fcard (A - B) - 1"
- using assms
- unfolding fin_set fcard_set fminus_set
- by (simp add: card_Diff_insert[OF finite_fset])
-
-lemma fcard_fminus_fsubset:
- assumes "B |\<subseteq>| A"
- shows "fcard (A - B) = fcard A - fcard B"
- using assms
- unfolding fsubseteq_set fcard_set fminus_set
- by (rule card_Diff_subset[OF finite_fset])
-
-lemma fcard_fminus_subset_finter:
- shows "fcard (A - B) = fcard A - fcard (A |\<inter>| B)"
- unfolding finter_set fcard_set fminus_set
- by (rule card_Diff_subset_Int) (simp)
lemma list_all2_refl: