nominal2: comparison Nominal/FSet.thy

equal deleted inserted replaced

-:9746421224a3
+:3a7155fce1da
 theory FSet
 imports Quotient_List
 begin
-text {* Definition of the equivalence relation over lists *}
+text {*
+The type of finite sets is created by a quotient construction
+over lists. The definition of the equivalence:
+*}
 fun
 list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)
 where
-"list_eq xs ys = (set xs = set ys)"
+"list_eq xs ys \<longleftrightarrow> set xs = set ys"
 lemma list_eq_equivp:
 shows "equivp list_eq"
 unfolding equivp_reflp_symp_transp
 unfolding reflp_def symp_def transp_def
 Definitions for membership, sublist, cardinality,
 intersection, difference and respectful fold over
 lists.
 *}
-definition
+fun
-"memb x xs \<equiv> x \<in> set xs"
+memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
+where
-definition
+"memb x xs \<longleftrightarrow> x \<in> set xs"
-"sub_list xs ys \<equiv> set xs \<subseteq> set ys"
+fun
-definition
+sub_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
+where
+"sub_list xs ys \<longleftrightarrow> set xs \<subseteq> set ys"
+fun
+card_list :: "'a list \<Rightarrow> nat"
+where
 "card_list xs = card (set xs)"
-definition
+fun
+inter_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+where
 "inter_list xs ys = [x \<leftarrow> xs. x \<in> set xs \<and> x \<in> set ys]"
-definition
+fun
-"diff_list xs ys \<equiv> [x \<leftarrow> xs. x \<notin> set ys]"
+diff_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+where
+"diff_list xs ys = [x \<leftarrow> xs. x \<notin> set ys]"
 definition
 rsp_fold
 where
 "rsp_fold f \<equiv> \<forall>u v w. (f u (f v w) = f v (f u w))"
 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) append append"
 by simp
 lemma sub_list_rsp [quot_respect]:
 shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
-by (auto simp add: sub_list_def)
+by simp
 lemma memb_rsp [quot_respect]:
 shows "(op = ===> op \<approx> ===> op =) memb memb"
-by (auto simp add: memb_def)
+by simp
 lemma nil_rsp [quot_respect]:
 shows "(op \<approx>) Nil Nil"
 by simp
 "(op \<approx> ===> op =) set set"
 by auto
 lemma inter_list_rsp [quot_respect]:
 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) inter_list inter_list"
-by (simp add: inter_list_def)
+by simp
 lemma removeAll_rsp [quot_respect]:
 shows "(op = ===> op \<approx> ===> op \<approx>) removeAll removeAll"
 by simp
 lemma diff_list_rsp [quot_respect]:
 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) diff_list diff_list"
-by (simp add: diff_list_def)
+by simp
 lemma card_list_rsp [quot_respect]:
 shows "(op \<approx> ===> op =) card_list card_list"
-by (simp add: card_list_def)
+by simp
 lemma filter_rsp [quot_respect]:
 shows "(op = ===> op \<approx> ===> op \<approx>) filter filter"
 by simp
 instance
 proof
 fix x y z :: "'a fset"
 show "x |\<subset>| y \<longleftrightarrow> x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x"
 unfolding less_fset_def
-by (descending) (auto simp add: sub_list_def)
+by (descending) (auto)
-show "x |\<subseteq>| x"  by (descending) (simp add: sub_list_def)
+show "x |\<subseteq>| x"  by (descending) (simp)
-show "{||} |\<subseteq>| x" by (descending) (simp add: sub_list_def)
+show "{||} |\<subseteq>| x" by (descending) (simp)
-show "x |\<subseteq>| x |\<union>| y" by (descending) (simp add: sub_list_def)
+show "x |\<subseteq>| x |\<union>| y" by (descending) (simp)
-show "y |\<subseteq>| x |\<union>| y" by (descending) (simp add: sub_list_def)
+show "y |\<subseteq>| x |\<union>| y" by (descending) (simp)
-show "x |\<inter>| y |\<subseteq>| x"
+show "x |\<inter>| y |\<subseteq>| x" by (descending) (auto)
-by (descending) (auto simp add: inter_list_def sub_list_def memb_def)
+show "x |\<inter>| y |\<subseteq>| y" by (descending) (auto)
-show "x |\<inter>| y |\<subseteq>| y"
-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) (auto simp add: inter_list_def)
+by (descending) (auto)
 next
 fix x y z :: "'a fset"
 assume a: "x |\<subseteq>| y"
 assume b: "y |\<subseteq>| z"
-show "x |\<subseteq>| z" using a b
+show "x |\<subseteq>| z" using a b by (descending) (simp)
-by (descending) (simp add: sub_list_def)
 next
 fix x y :: "'a fset"
 assume a: "x |\<subseteq>| y"
 assume b: "y |\<subseteq>| x"
-show "x = y" using a b
+show "x = y" using a b by (descending) (auto)
-by (descending) (unfold sub_list_def list_eq.simps, blast)
 next
 fix x y z :: "'a fset"
 assume a: "y |\<subseteq>| x"
 assume b: "z |\<subseteq>| x"
-show "y |\<union>| z |\<subseteq>| x" using a b
+show "y |\<union>| z |\<subseteq>| x" using a b by (descending) (simp)
-by (descending) (simp add: sub_list_def)
 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
+show "x |\<subseteq>| y |\<inter>| z" using a b by (descending) (auto)
-by (descending) (auto simp add: inter_list_def sub_list_def memb_def)
 qed
 end
 shows "fset (remove_fset x xs) = fset xs - {x}"
 by (descending) (simp)
 lemma inter_fset [simp]:
 shows "fset (xs |\<inter>| ys) = fset xs \<inter> fset ys"
-by (descending) (auto simp add: inter_list_def)
+by (descending) (auto)
 lemma union_fset [simp]:
 shows "fset (xs |\<union>| ys) = fset xs \<union> fset ys"
 by (lifting set_append)
 lemma minus_fset [simp]:
 shows "fset (xs - ys) = fset xs - fset ys"
-by (descending) (auto simp add: diff_list_def)
+by (descending) (auto)
 subsection {* in_fset *}
 lemma in_fset:
 shows "x |\<in>| S \<longleftrightarrow> x \<in> fset S"
-by (descending) (simp add: memb_def)
+by (descending) (simp)
 lemma notin_fset:
 shows "x |\<notin>| S \<longleftrightarrow> x \<notin> fset S"
 by (simp add: in_fset)
 shows "x |\<notin>| {||}"
 by (simp add: in_fset)
 lemma fset_eq_iff:
 shows "S = T \<longleftrightarrow> (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
-by (descending) (auto simp add: memb_def)
+by (descending) (auto)
 lemma none_in_empty_fset:
 shows "(\<forall>x. x |\<notin>| S) \<longleftrightarrow> S = {||}"
-by (descending) (simp add: memb_def)
+by (descending) (simp)
 subsection {* insert_fset *}
 lemma in_insert_fset_iff [simp]:
 shows "x |\<in>| insert_fset y S \<longleftrightarrow> x = y \<or> x |\<in>| S"
-by (descending) (simp add: memb_def)
+by (descending) (simp)
 lemma
 shows insert_fsetI1: "x |\<in>| insert_fset x S"
 and   insert_fsetI2: "x |\<in>| S \<Longrightarrow> x |\<in>| insert_fset y S"
 by simp_all
 lemma insert_absorb_fset [simp]:
 shows "x |\<in>| S \<Longrightarrow> insert_fset x S = S"
-by (descending) (auto simp add: memb_def)
+by (descending) (auto)
 lemma empty_not_insert_fset[simp]:
 shows "{||} \<noteq> insert_fset x S"
 and   "insert_fset x S \<noteq> {||}"
 by (descending, simp)+
 (* FIXME: is this a useful lemma ? *)
 lemma in_fset_mdef:
 shows "x |\<in>| F \<longleftrightarrow> x |\<notin>| (F - {|x|}) \<and> F = insert_fset x (F - {|x|})"
-by (descending) (auto simp add: memb_def diff_list_def)
+by (descending) (auto)
 subsection {* union_fset *}
 lemmas [simp] =
 shows "S |\<union>| {|a|} = insert_fset a S"
 by (subst sup.commute) simp
 lemma in_union_fset:
 shows "x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"
-by (descending) (simp add: memb_def)
+by (descending) (simp)
 subsection {* minus_fset *}
 lemma minus_in_fset:
 shows "x |\<in>| (xs - ys) \<longleftrightarrow> x |\<in>| xs \<and> x |\<notin>| ys"
-by (descending) (simp add: diff_list_def memb_def)
+by (descending) (simp)
 lemma minus_insert_fset:
 shows "insert_fset x xs - ys = (if x |\<in>| ys then xs - ys else insert_fset x (xs - ys))"
-by (descending) (auto simp add: diff_list_def memb_def)
+by (descending) (auto)
 lemma minus_insert_in_fset[simp]:
 shows "x |\<in>| ys \<Longrightarrow> insert_fset x xs - ys = xs - ys"
 by (simp add: minus_insert_fset)
 subsection {* remove_fset *}
 lemma in_remove_fset:
 shows "x |\<in>| remove_fset y S \<longleftrightarrow> x |\<in>| S \<and> x \<noteq> y"
-by (descending) (simp add: memb_def)
+by (descending) (simp)
 lemma notin_remove_fset:
 shows "x |\<notin>| remove_fset x S"
-by (descending) (simp add: memb_def)
+by (descending) (simp)
 lemma notin_remove_ident_fset:
 shows "x |\<notin>| S \<Longrightarrow> remove_fset x S = S"
-by (descending) (simp add: memb_def)
+by (descending) (simp)
 lemma remove_fset_cases:
 shows "S = {||} \<or> (\<exists>x. x |\<in>| S \<and> S = insert_fset x (remove_fset x S))"
-by (descending) (auto simp add: memb_def insert_absorb)
+by (descending) (auto simp add: insert_absorb)
 subsection {* inter_fset *}
 lemma inter_empty_fset_l:
 shows "S |\<inter>| {||} = {||}"
 by simp
 lemma inter_insert_fset:
 shows "insert_fset x S |\<inter>| T = (if x |\<in>| T then insert_fset x (S |\<inter>| T) else S |\<inter>| T)"
-by (descending) (auto simp add: inter_list_def memb_def)
+by (descending) (auto)
 lemma in_inter_fset:
 shows "x |\<in>| (S |\<inter>| T) \<longleftrightarrow> x |\<in>| S \<and> x |\<in>| T"
-by (descending) (simp add: inter_list_def memb_def)
+by (descending) (simp)
 subsection {* subset_fset and psubset_fset *}
 lemma subset_fset:
 shows "xs |\<subseteq>| ys \<longleftrightarrow> fset xs \<subseteq> fset ys"
-by (descending) (simp add: sub_list_def)
+by (descending) (simp)
 lemma psubset_fset:
 shows "xs |\<subset>| ys \<longleftrightarrow> fset xs \<subset> fset ys"
 unfolding less_fset_def
-by (descending) (auto simp add: sub_list_def)
+by (descending) (auto)
 lemma subset_insert_fset:
 shows "(insert_fset x xs) |\<subseteq>| ys \<longleftrightarrow> x |\<in>| ys \<and> xs |\<subseteq>| ys"
-by (descending) (simp add: sub_list_def memb_def)
+by (descending) (simp)
 lemma subset_in_fset:
 shows "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)"
-by (descending) (auto simp add: sub_list_def memb_def)
+by (descending) (auto)
 lemma subset_empty_fset:
 shows "xs |\<subseteq>| {||} \<longleftrightarrow> xs = {||}"
-by (descending) (simp add: sub_list_def)
+by (descending) (simp)
 lemma not_psubset_empty_fset:
 shows "\<not> xs |\<subset>| {||}"
 by (metis fset_simps(1) psubset_fset not_psubset_empty)
 subsection {* card_fset *}
 lemma card_fset:
 shows "card_fset xs = card (fset xs)"
-by (lifting card_list_def)
+by (descending) (simp)
 lemma card_insert_fset_iff [simp]:
 shows "card_fset (insert_fset x S) = (if x |\<in>| S then card_fset S else Suc (card_fset S))"
-by (descending) (auto simp add: card_list_def memb_def insert_absorb)
+by (descending) (simp add: insert_absorb)
 lemma card_fset_0[simp]:
 shows "card_fset S = 0 \<longleftrightarrow> S = {||}"
-by (descending) (simp add: card_list_def)
+by (descending) (simp)
 lemma card_empty_fset[simp]:
 shows "card_fset {||} = 0"
 by (simp add: card_fset)
 lemma card_fset_1:
 shows "card_fset S = 1 \<longleftrightarrow> (\<exists>x. S = {|x|})"
-by (descending) (auto simp add: card_list_def card_Suc_eq)
+by (descending) (auto simp add: card_Suc_eq)
 lemma card_fset_gt_0:
 shows "x \<in> fset S \<Longrightarrow> 0 < card_fset S"
-by (descending) (auto simp add: card_list_def card_gt_0_iff)
+by (descending) (auto simp add: card_gt_0_iff)
 lemma card_notin_fset:
 shows "(x |\<notin>| S) = (card_fset (insert_fset x S) = Suc (card_fset S))"
 by simp
 lemma card_fset_Suc:
 shows "card_fset S = Suc n \<Longrightarrow> \<exists>x T. x |\<notin>| T \<and> S = insert_fset x T \<and> card_fset T = n"
 apply(descending)
-apply(auto simp add: card_list_def memb_def dest!: card_eq_SucD)
+apply(auto dest!: card_eq_SucD)
 by (metis Diff_insert_absorb set_removeAll)
 lemma card_remove_fset_iff [simp]:
 shows "card_fset (remove_fset y S) = (if y |\<in>| S then card_fset S - 1 else card_fset S)"
-by (descending) (simp add: card_list_def memb_def)
+by (descending) (simp)
 lemma card_Suc_exists_in_fset:
 shows "card_fset S = Suc n \<Longrightarrow> \<exists>a. a |\<in>| S"
 by (drule card_fset_Suc) (auto)
 lemma in_card_fset_not_0:
 shows "a |\<in>| A \<Longrightarrow> card_fset A \<noteq> 0"
-by (descending) (auto simp add: card_list_def memb_def)
+by (descending) (auto)
 lemma card_fset_mono:
 shows "xs |\<subseteq>| ys \<Longrightarrow> card_fset xs \<le> card_fset ys"
 unfolding card_fset psubset_fset
-by (simp add:  card_mono subset_fset)
+by (simp add: card_mono subset_fset)
 lemma card_subset_fset_eq:
 shows "xs |\<subseteq>| ys \<Longrightarrow> card_fset ys \<le> card_fset xs \<Longrightarrow> xs = ys"
 unfolding card_fset subset_fset
 by (auto dest: card_seteq[OF finite_fset] simp add: fset_cong)
 subsection {* filter_fset *}
 lemma subset_filter_fset:
 shows "filter_fset P xs |\<subseteq>| filter_fset Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)"
-by  (descending) (auto simp add: memb_def sub_list_def)
+by  (descending) (auto)
 lemma eq_filter_fset:
 shows "(filter_fset P xs = filter_fset Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)"
-by (descending) (auto simp add: memb_def)
+by (descending) (auto)
 lemma psubset_filter_fset:
 shows "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow>
 filter_fset P xs |\<subset>| filter_fset Q xs"
 unfolding less_fset_def by (auto simp add: subset_filter_fset eq_filter_fset)
 shows "fold_fset f z {||} = z"
 by (descending) (simp)
 lemma fold_insert_fset: "fold_fset f z (insert_fset a A) =
 (if rsp_fold f then if a |\<in>| A then fold_fset f z A else f a (fold_fset f z A) else z)"
-by (descending) (simp add: memb_def)
+by (descending) (simp)
 lemma in_commute_fold_fset:
 "\<lbrakk>rsp_fold f; h |\<in>| b\<rbrakk> \<Longrightarrow> fold_fset f z b = f h (fold_fset f z (remove_fset h b))"
-by (descending) (simp add: memb_def memb_commute_fold_list)
+by (descending) (simp add: memb_commute_fold_list)
 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)
+by (auto simp add: Ball_def)
 section {* Induction and Cases rules for fsets *}
 lemma fset_exhaust [case_names empty_fset insert_fset, cases type: fset]:
 then show thesis by simp
 next
 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" using b unfolding memb_def
+have c: "xs = [] \<Longrightarrow> thesis" using b
-by (metis in_set_conv_nth less_zeroE list.size(3) list_eq.simps member_set)
+apply(simp)
+by (metis List.set.simps(1) emptyE empty_subsetI)
 have "\<And>x ys. \<lbrakk>\<not> memb x ys; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis"
 proof -
 fix x :: 'a
 fix ys :: "'a list"
 assume d:"\<not> memb x ys"
 then have f: "\<not> memb a ys" using d by simp
 have g: "a # xs \<approx> a # ys" using e h by auto
 show thesis using b f g by simp
 next
 assume h: "x \<noteq> a"
-then have f: "\<not> memb x (a # ys)" using d unfolding memb_def by auto
+then have f: "\<not> memb x (a # ys)" using d by auto
 have g: "a # xs \<approx> x # (a # ys)" using e h by auto
-show thesis using b f g by simp
+show thesis using b f g by (simp del: memb.simps)
 qed
 qed
 then show thesis using a c by blast
 qed
 by (induct xs) (auto intro: list_eq2.intros)
 lemma cons_delete_list_eq2:
 shows "(a # (removeAll a A)) \<approx>2 (if memb a A then A else a # A)"
 apply (induct A)
-apply (simp add: memb_def list_eq2_refl)
+apply (simp add: list_eq2_refl)
 apply (case_tac "memb a (aa # A)")
-apply (simp_all only: memb_def)
+apply (simp_all)
 apply (case_tac [!] "a = aa")
 apply (simp_all)
 apply (case_tac "memb a A")
-apply (auto simp add: memb_def)[2]
+apply (auto)[2]
 apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6))
 apply (metis list_eq2.intros(1) list_eq2.intros(5) list_eq2.intros(6))
 apply (auto simp add: list_eq2_refl memb_def)
 done
 have "l \<approx>2 r"
 using a b
 proof (induct n arbitrary: l r)
 case 0
 have "card_list l = 0" by fact
-then have "\<forall>x. \<not> memb x l" unfolding card_list_def memb_def by auto
+then have "\<forall>x. \<not> memb x l" by auto
-then have z: "l = []" unfolding memb_def by auto
+then have z: "l = []" by auto
 then have "r = []" using `l \<approx> r` by simp
 then show ?case using z list_eq2_refl by simp
 next
 case (Suc m)
 have b: "l \<approx> r" by fact
 have d: "card_list l = Suc m" by fact
 then have "\<exists>a. memb a l"
-	apply(simp add: card_list_def memb_def)
+	apply(simp)
 	apply(drule card_eq_SucD)
 	apply(blast)
 	done
 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
+	by auto
-have f: "card_list (removeAll a l) = m" using e d by (simp add: card_list_def memb_def)
+have f: "card_list (removeAll a l) = m" using e d by (simp)
 have g: "removeAll a l \<approx> removeAll a r" using removeAll_rsp b by simp
 have "(removeAll a l) \<approx>2 (removeAll a r)" by (rule Suc.hyps[OF f g])
 then have h: "(a # removeAll a l) \<approx>2 (a # removeAll a r)" by (rule list_eq2.intros(5))
 have i: "l \<approx>2 (a # removeAll a l)"
 by (rule list_eq2.intros(3)[OF memb_delete_list_eq2[OF e]])

changeset 2546	3a7155fce1da
parent 2544	3b24b5d2b68c
child 2547	17b369a73f15