nominal2: comparison Nominal/FSet.thy

equal deleted inserted replaced

-:693562f03eee
+:c848f93807b9
 qed
 lemma Quotient_fset_list:
 shows "Quotient (list_all2 op \<approx>) (map abs_fset) (map rep_fset)"
 by (fact list_quotient[OF Quotient_fset])
-(*
-lemma set_in_eq: "(\<forall>e. ((e \<in> xs) \<longleftrightarrow> (e \<in> ys))) \<equiv> xs = ys"
-by (rule eq_reflection) auto
-*)
 lemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"
 unfolding list_eq.simps
 by (simp only: set_map)
 then show "(list_all2 op \<approx> OOO op \<approx>) r s"
 using a c pred_compI by simp
 qed
 qed
+lemma set_finter_raw[simp]:
+"set (finter_raw xs ys) = set xs \<inter> set ys"
+by (induct xs) (auto simp add: memb_def)
+lemma set_fminus_raw[simp]:
+"set (fminus_raw xs ys) = (set xs - set ys)"
+by (induct ys arbitrary: xs) (auto)
 text {* Respectfullness *}
 lemma append_rsp[quot_respect]:
 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) append append"
 by (simp)
-(*
+lemma sub_list_rsp[quot_respect]:
-lemma append_rsp_unfolded:
-"\<lbrakk>x \<approx> y; v \<approx> w\<rbrakk> \<Longrightarrow> x @ v \<approx> y @ w"
-by auto
-*)
-lemma [quot_respect]:
 shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
 by (auto simp add: sub_list_def)
 lemma memb_rsp[quot_respect]:
 shows "(op = ===> op \<approx> ===> op =) memb memb"
 by (auto simp add: memb_def)
 lemma nil_rsp[quot_respect]:
-shows "[] \<approx> []"
+shows "(op \<approx>) Nil Nil"
 by simp
 lemma cons_rsp[quot_respect]:
 shows "(op = ===> op \<approx> ===> op \<approx>) Cons Cons"
 by simp
 lemma list_equiv_rsp[quot_respect]:
 shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
 by auto
+lemma finter_raw_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 fminus_raw_rsp[quot_respect]:
+shows "(op \<approx> ===> op \<approx> ===> op \<approx>) fminus_raw fminus_raw"
+by simp
+lemma fcard_raw_rsp[quot_respect]:
+shows "(op \<approx> ===> op =) fcard_raw fcard_raw"
+by (simp add: fcard_raw_def)
 lemma not_memb_nil:
 shows "\<not> memb x []"
 by (simp add: memb_def)
 lemma memb_cons_iff:
 shows "memb x (y # xs) = (x = y \<or> memb x xs)"
 by (induct xs) (auto simp add: memb_def)
-lemma set_finter_raw[simp]:
-"set (finter_raw xs ys) = set xs \<inter> set ys"
-by (induct xs) (auto simp add: memb_def)
-lemma [quot_respect]:
-shows "(op \<approx> ===> op \<approx> ===> op \<approx>) finter_raw finter_raw"
-by (simp)
-(*
-lemma memb_removeAll:
-"memb x (removeAll y xs) \<longleftrightarrow> memb x xs \<and> x \<noteq> y"
-by (induct xs arbitrary: x y) (auto simp add: memb_def)
-*)
-lemma [quot_respect]:
-shows "(op = ===> op \<approx> ===> op \<approx>) removeAll removeAll"
-by (simp)
-lemma set_fminus_raw[simp]:
-"set (fminus_raw xs ys) = (set xs - set ys)"
-by (induct ys arbitrary: xs) (auto)
-lemma [quot_respect]:
-shows "(op \<approx> ===> op \<approx> ===> op \<approx>) fminus_raw fminus_raw"
-by simp
-lemma fcard_raw_rsp[quot_respect]:
-shows "(op \<approx> ===> op =) fcard_raw fcard_raw"
-by (simp add: fcard_raw_def)
 lemma memb_absorb:
 shows "memb x xs \<Longrightarrow> x # xs \<approx> xs"
 by (induct xs) (auto simp add: memb_def)
 lemma none_memb_nil:
 "(\<forall>x. \<not> memb x xs) = (xs \<approx> [])"
 by (simp add: memb_def)
-lemma not_memb_removeAll_ident:
-shows "\<not> memb x xs \<Longrightarrow> removeAll x xs = xs"
-by (induct xs) (auto simp add: memb_def)
 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 [quot_respect]:
+lemma ffold_raw_rsp[quot_respect]:
 shows "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw"
 unfolding fun_rel_def
 apply(auto intro: ffold_raw_rsp_pre)
 done
 qed
 section {* deletion *}
-lemma memb_removeAll_ident:
-shows "\<not> memb x (removeAll x xs)"
-by (induct xs) (auto simp add: memb_def)
 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)
 apply (simp_all)
 apply (case_tac "memb a A")
 apply (auto simp add: memb_def)[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 not_memb_removeAll_ident)
+apply (auto simp add: list_eq2_refl memb_def)
 done
 lemma memb_delete_list_eq2:
 assumes a: "memb e r"
 shows "list_eq2 (e # removeAll e r) r"
 using a cons_delete_list_eq2[of e r]
 by simp
-lemma removeAll_rsp:
-"xs \<approx> ys \<Longrightarrow> removeAll x xs \<approx> removeAll x ys"
-by (simp add: memb_def[symmetric])
 lemma list_eq2_equiv:
 "(l \<approx> r) \<longleftrightarrow> (list_eq2 l r)"
 proof
 show "list_eq2 l r \<Longrightarrow> l \<approx> r" by (induct rule: list_eq2.induct) auto
 	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
 have f: "fcard_raw (removeAll a l) = m" using fcard_raw_delete[of a l] e d by simp
-have g: "removeAll a l \<approx> removeAll a r" using removeAll_rsp[OF b] by simp
+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))
 have i: "list_eq2 l (a # removeAll a l)"
 by (rule list_eq2.intros(3)[OF memb_delete_list_eq2[OF e]])
 have "list_eq2 l (a # removeAll a r)" by (rule list_eq2.intros(6)[OF i h])
 lemma fin_fdelete:
 shows "x |\<in>| fdelete y S \<longleftrightarrow> x |\<in>| S \<and> x \<noteq> y"
 by (descending) (simp add: memb_def)
-lemma fin_fdelete_ident:
+lemma fnotin_fdelete:
 shows "x |\<notin>| fdelete x S"
-by (lifting memb_removeAll_ident)
+by (descending) (simp add: memb_def)
-lemma not_memb_fdelete_ident:
+lemma fnotin_fdelete_ident:
 shows "x |\<notin>| S \<Longrightarrow> fdelete x S = S"
-by (lifting not_memb_removeAll_ident)
+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)

changeset 2525	c848f93807b9
parent 2524	693562f03eee
child 2528	9bde8a508594