nominal2: comparison Nominal/FSet.thy

equal deleted inserted replaced

-:d73fa7a3e04b
+:c9deccd12476
 quotient_type
 'a fset = "'a list" / "list_eq"
 by (rule list_eq_equivp)
 text {*
-Definitions of membership, sublist, cardinality,
+Definitions of membership, sublist, cardinality, intersection,
-intersection etc over lists
+difference and respectful fold over lists
 *}
 definition
-memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
-where
 "memb x xs \<equiv> x \<in> set xs"
 definition
-sub_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
-where
 "sub_list xs ys \<equiv> set xs \<subseteq> set ys"
 definition
-card_list :: "'a list \<Rightarrow> nat"
-where
 "card_list xs = card (set xs)"
-primrec
-finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
-where
-"finter_raw [] ys = []"
-| "finter_raw (x # xs) ys =
-(if x \<in> set ys then x # (finter_raw xs ys) else finter_raw xs ys)"
 definition
-diff_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+"inter_list xs ys = [x \<leftarrow> xs. x \<in> set xs \<and> x \<in> set ys]"
-where
+definition
 "diff_list xs ys \<equiv> [x \<leftarrow> xs. x\<notin>set ys]"
 definition
 rsp_fold
 where
-"rsp_fold f = (\<forall>u v w. (f u (f v w) = f v (f u w)))"
+"rsp_fold f \<equiv> \<forall>u v w. (f u (f v w) = f v (f u w))"
 primrec
 ffold_raw :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"
 where
 "ffold_raw f z [] = z"
 | "ffold_raw f z (a # xs) =
 (if (rsp_fold f) then
 if a \<in> set xs then ffold_raw f z xs
 else f a (ffold_raw f z xs)
 else z)"
-lemma set_finter_raw[simp]:
-shows "set (finter_raw xs ys) = set xs \<inter> set ys"
-by (induct xs) (auto simp add: memb_def)
-lemma set_diff_list[simp]:
-shows "set (diff_list xs ys) = (set xs - set ys)"
-by (auto simp add: diff_list_def)
 section {* Quotient composition lemmas *}
 lemma list_all2_refl1:
 using a c pred_compI by simp
 qed
 qed
-text {* Respectfulness *}
+subsection {* Respectfulness lemmas for list operations *}
-lemma append_rsp[quot_respect]:
+lemma list_equiv_rsp [quot_respect]:
+shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
+by auto
+lemma append_rsp [quot_respect]:
 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) append append"
 by simp
-lemma sub_list_rsp[quot_respect]:
+lemma sub_list_rsp [quot_respect]:
 shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
 by (auto simp add: sub_list_def)
-lemma memb_rsp[quot_respect]:
+lemma memb_rsp [quot_respect]:
 shows "(op = ===> op \<approx> ===> op =) memb memb"
 by (auto simp add: memb_def)
-lemma nil_rsp[quot_respect]:
+lemma nil_rsp [quot_respect]:
 shows "(op \<approx>) Nil Nil"
 by simp
-lemma cons_rsp[quot_respect]:
+lemma cons_rsp [quot_respect]:
 shows "(op = ===> op \<approx> ===> op \<approx>) Cons Cons"
 by simp
-lemma map_rsp[quot_respect]:
+lemma map_rsp [quot_respect]:
 shows "(op = ===> op \<approx> ===> op \<approx>) map map"
 by auto
-lemma set_rsp[quot_respect]:
+lemma set_rsp [quot_respect]:
 "(op \<approx> ===> op =) set set"
 by auto
-lemma list_equiv_rsp[quot_respect]:
+lemma inter_list_rsp [quot_respect]:
-shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
+shows "(op \<approx> ===> op \<approx> ===> op \<approx>) inter_list inter_list"
-by auto
+by (simp add: inter_list_def)
-lemma finter_raw_rsp[quot_respect]:
+lemma removeAll_rsp [quot_respect]:
-shows "(op \<approx> ===> op \<approx> ===> op \<approx>) finter_raw finter_raw"
-by simp
-lemma removeAll_rsp[quot_respect]:
 shows "(op = ===> op \<approx> ===> op \<approx>) removeAll removeAll"
 by simp
-lemma diff_list_rsp[quot_respect]:
+lemma diff_list_rsp [quot_respect]:
 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) diff_list diff_list"
-by simp
+by (simp add: diff_list_def)
-lemma card_list_rsp[quot_respect]:
+lemma card_list_rsp [quot_respect]:
 shows "(op \<approx> ===> op =) card_list card_list"
 by (simp add: card_list_def)
+lemma filter_rsp [quot_respect]:
+shows "(op = ===> op \<approx> ===> op \<approx>) filter filter"
+by simp
 lemma memb_commute_ffold_raw:
 "rsp_fold f \<Longrightarrow> h \<in> set b \<Longrightarrow> ffold_raw f z b = f h (ffold_raw f z (removeAll h b))"
 apply (induct b)
 apply (auto simp add: rsp_fold_def)
 apply(auto)
 apply(drule meta_mp)
 apply(blast)
 by (metis List.set.simps(2) emptyE ffold_raw.simps(2) in_listsp_conv_set listsp.simps mem_def)
-lemma ffold_raw_rsp[quot_respect]:
+lemma ffold_raw_rsp [quot_respect]:
 shows "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw"
 unfolding fun_rel_def
 by(auto intro: ffold_raw_rsp_pre)
 lemma concat_rsp_pre:
 have "ya \<in> set y'" using b h by simp
 then have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" using c by (rule list_all2_find_element)
 then show ?thesis using f i by auto
 qed
-lemma concat_rsp[quot_respect]:
+lemma concat_rsp [quot_respect]:
 shows "(list_all2 op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"
 proof (rule fun_relI, elim pred_compE)
 fix a b ba bb
 assume a: "list_all2 op \<approx> a ba"
 assume b: "ba \<approx> bb"
 qed
 qed
 then show "concat a \<approx> concat b" by auto
 qed
-lemma [quot_respect]:
-shows "(op = ===> op \<approx> ===> op \<approx>) filter filter"
+subsection {* Finite sets are a bounded, distributive lattice with minus *}
-by auto
 instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}"
 begin
 quotient_definition
-"bot :: 'a fset" is "[] :: 'a list"
+"bot :: 'a fset"
+is "Nil :: 'a list"
 abbreviation
 fempty  ("{||}")
 where
 "{||} \<equiv> bot :: 'a fset"
 quotient_definition
-"less_eq_fset \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> bool)"
+"less_eq_fset :: ('a fset \<Rightarrow> 'a fset \<Rightarrow> bool)"
-is
+is "sub_list :: ('a list \<Rightarrow> 'a list \<Rightarrow> bool)"
-"sub_list \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> bool)"
 abbreviation
 f_subset_eq :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subseteq>|" 50)
 where
 "xs |\<subseteq>| ys \<equiv> xs \<le> ys"
 where
 "xs |\<subset>| ys \<equiv> xs < ys"
 quotient_definition
 "sup :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-is
+is "append :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
-"append :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 abbreviation
 funion (infixl "|\<union>|" 65)
 where
 "xs |\<union>| ys \<equiv> sup xs (ys::'a fset)"
 quotient_definition
 "inf :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-is
+is "inter_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
-"finter_raw :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 abbreviation
 finter (infixl "|\<inter>|" 65)
 where
 "xs |\<inter>| ys \<equiv> inf xs (ys::'a fset)"
 quotient_definition
 "minus :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-is
+is "diff_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
-"diff_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
-lemma append_finter_raw_distrib:
-"x @ (finter_raw y z) \<approx> finter_raw (x @ y) (x @ z)"
-apply (induct x)
-apply (auto)
-done
 instance
 proof
 fix x y z :: "'a fset"
 show "x |\<subset>| y \<longleftrightarrow> x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x"
 show "x |\<subseteq>| x"  by (descending) (simp add: sub_list_def)
 show "{||} |\<subseteq>| x" by (descending) (simp add: sub_list_def)
 show "x |\<subseteq>| x |\<union>| y" by (descending) (simp add: sub_list_def)
 show "y |\<subseteq>| x |\<union>| y" by (descending) (simp add: sub_list_def)
 show "x |\<inter>| y |\<subseteq>| x"
-by (descending) (simp add: sub_list_def memb_def[symmetric])
+by (descending) (auto simp add: inter_list_def sub_list_def memb_def)
 show "x |\<inter>| y |\<subseteq>| y"
-by (descending) (simp add: sub_list_def memb_def[symmetric])
+by (descending) (auto simp add: inter_list_def sub_list_def memb_def)
 show "x |\<union>| (y |\<inter>| z) = x |\<union>| y |\<inter>| (x |\<union>| z)"
-by (descending) (rule append_finter_raw_distrib)
+by (descending) (auto simp add: inter_list_def)
 next
 fix x y z :: "'a fset"
 assume a: "x |\<subseteq>| y"
 assume b: "y |\<subseteq>| z"
 show "x |\<subseteq>| z" using a b
 next
 fix x y z :: "'a fset"
 assume a: "x |\<subseteq>| y"
 assume b: "x |\<subseteq>| z"
 show "x |\<subseteq>| y |\<inter>| z" using a b
-by (descending) (simp add: sub_list_def memb_def[symmetric])
+by (descending) (auto simp add: inter_list_def sub_list_def memb_def)
 qed
 end
-section {* Definitions for fsets *}
+section {* Quotient definitions for fsets *}
 quotient_definition
 "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 is "Cons"
 subsection {* Compositional Respectfulness and Preservation *}
 lemma [quot_respect]: "(list_all2 op \<approx> OOO op \<approx>) [] []"
 by (fact compose_list_refl)
-lemma [quot_preserve]: "(abs_fset \<circ> map f) [] = abs_fset []"
+lemma  [quot_preserve]: "(abs_fset \<circ> map f) [] = abs_fset []"
 by simp
 lemma [quot_respect]:
 shows "(op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) Cons Cons"
 apply auto
 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)
+by (descending) (auto simp add: inter_list_def)
 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_diff_list)
+by (descending) (auto simp add: diff_list_def)
 subsection {* funion *}
 lemmas [simp] =
 subsection {* fminus *}
 lemma fminus_fin:
 shows "x |\<in>| (xs - ys) \<longleftrightarrow> x |\<in>| xs \<and> x |\<notin>| ys"
-by (descending) (simp add: memb_def)
+by (descending) (simp add: diff_list_def 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)
+by (descending) (auto simp add: diff_list_def memb_def)
 lemma fminus_red_fin[simp]:
 shows "x |\<in>| ys \<Longrightarrow> finsert x xs - ys = xs - ys"
 by (simp add: fminus_red)
 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)
+by (descending) (auto simp add: inter_list_def 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)
+by (descending) (simp add: inter_list_def memb_def)
 subsection {* fsubset *}
 lemma fsubseteq_set:

changeset 2538	c9deccd12476
parent 2537	d73fa7a3e04b
child 2539	a8f5611dbd65