nominal2: comparison Nominal/FSet.thy

equal deleted inserted replaced

-:509a0ccc4f32
+:4465723e35e7
 using a
 by (induct xs) (auto simp add: memb_def)
 lemma fcard_raw_not_memb:
 fixes x :: "'a"
-fixes xs :: "'a list"
 shows "\<not>(memb x xs) \<longleftrightarrow> (fcard_raw (x # xs) = Suc (fcard_raw xs))"
 by auto
 lemma fcard_raw_suc:
 fixes xs :: "'a list"
-fixes n :: "nat"
 assumes c: "fcard_raw xs = Suc n"
 shows "\<exists>x ys. \<not>(memb x ys) \<and> xs \<approx> (x # ys) \<and> fcard_raw ys = n"
 unfolding memb_def
 using c
 proof (induct xs)
 "memb x (xs @ ys) = (memb x xs \<or> memb x ys)"
 by (induct xs) (simp_all add: not_memb_nil memb_cons_iff)
 text {* raw section *}
-lemma map_rsp_aux:
-assumes a: "a \<approx> b"
-shows "map f a \<approx> map f b"
-using a
-apply(induct a arbitrary: b)
-apply(auto)
-apply(metis rev_image_eqI)
-done
 lemma map_rsp[quot_respect]:
 shows "(op = ===> op \<approx> ===> op \<approx>) map map"
-by (auto simp add: map_rsp_aux)
+by auto
 lemma cons_left_comm:
 "x # y # xs \<approx> y # x # xs"
 by auto
 lemma none_mem_nil:
 "(\<forall>x. x \<notin> set xs) = (xs \<approx> [])"
 by simp
 lemma fset_raw_strong_cases:
-"(xs = []) \<or> (\<exists>x ys. ((x \<notin> set ys) \<and> (xs \<approx> x # ys)))"
+"(xs = []) \<or> (\<exists>x ys. ((\<not> memb x ys) \<and> (xs \<approx> x # ys)))"
 apply (induct xs)
 apply (simp)
 apply (rule disjI2)
 apply (erule disjE)
 apply (rule_tac x="a" in exI)
 apply (rule_tac x="[]" in exI)
-apply (simp)
+apply (simp add: memb_def)
 apply (erule exE)+
 apply (case_tac "x = a")
 apply (rule_tac x="a" in exI)
 apply (rule_tac x="ys" in exI)
 apply (simp)
 apply (rule_tac x="x" in exI)
 apply (rule_tac x="a # ys" in exI)
-apply (auto)
+apply (auto simp add: memb_def)
 done
 fun
 delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"
 where
 lemma finter_raw_empty:
 "finter_raw l [] = []"
 by (induct l) (simp_all add: not_memb_nil)
 lemma memb_finter_raw:
-"memb e (finter_raw l r) = (memb e l \<and> memb e r)"
+"memb x (finter_raw xs ys) = (memb x xs \<and> memb x ys)"
-apply (induct l)
+apply (induct xs)
 apply (simp add: not_memb_nil)
 apply (simp add: finter_raw.simps)
 apply (simp add: memb_cons_iff)
 apply auto
 done
 where
 "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 is "finter_raw"
 lemma funion_sym_pre:
-"a @ b \<approx> b @ a"
+"xs @ ys \<approx> ys @ xs"
 by auto
 lemma append_rsp[quot_respect]:
 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
-by (auto)
+by auto
 lemma set_cong:
 shows "(set x = set y) = (x \<approx> y)"
 by auto
 "{||} \<noteq> finsert x S"
 "finsert x S \<noteq> {||}"
 by (lifting nil_not_cons)
 lemma finsert_left_comm:
-"finsert a (finsert b S) = finsert b (finsert a S)"
+"finsert x (finsert y S) = finsert y (finsert x S)"
 by (lifting cons_left_comm)
 lemma finsert_left_idem:
-"finsert a (finsert a S) = finsert a S"
+"finsert x (finsert x S) = finsert x S"
 by (lifting cons_left_idem)
 lemma fsingleton_eq[simp]:
 shows "{|x|} = {|y|} \<longleftrightarrow> x = y"
 by (lifting singleton_list_eq)
 lemma fset_to_set_simps[simp]:
 "fset_to_set {||} = ({} :: 'a set)"
 "fset_to_set (finsert (h :: 'a) t) = insert h (fset_to_set t)"
 by (lifting set.simps)
+thm memb_def[symmetric, THEN meta_eq_to_obj_eq]
 lemma in_fset_to_set:
-"x \<in> fset_to_set xs \<equiv> x |\<in>| xs"
+"x \<in> fset_to_set S \<equiv> x |\<in>| S"
 by (lifting memb_def[symmetric])
 lemma none_fin_fempty:
-"(\<forall>a. a \<notin> fset_to_set A) = (A = {||})"
+"(\<forall>x. x \<notin> fset_to_set S) = (S = {||})"
 by (lifting none_mem_nil)
 lemma fset_cong:
-"(fset_to_set x = fset_to_set y) = (x = y)"
+"(fset_to_set S = fset_to_set T) = (S = T)"
 by (lifting set_cong)
 text {* fcard *}
 lemma fcard_fempty [simp]:
 lemma fcard_finsert_if [simp]:
 shows "fcard (finsert x S) = (if x |\<in>| S then fcard S else Suc (fcard S))"
 by (lifting fcard_raw_cons)
-lemma fcard_0: "(fcard a = 0) = (a = {||})"
+lemma fcard_0: "(fcard S = 0) = (S = {||})"
 by (lifting fcard_raw_0)
 lemma fcard_1:
-fixes xs::"'b fset"
+fixes S::"'b fset"
-shows "(fcard xs = 1) = (\<exists>x. xs = {|x|})"
+shows "(fcard S = 1) = (\<exists>x. S = {|x|})"
 by (lifting fcard_raw_1)
-lemma fcard_gt_0: "x \<in> fset_to_set xs \<Longrightarrow> 0 < fcard xs"
+lemma fcard_gt_0: "x \<in> fset_to_set S \<Longrightarrow> 0 < fcard S"
 by (lifting fcard_raw_gt_0)
-lemma fcard_not_fin: "(x |\<notin>| xs) = (fcard (finsert x xs) = Suc (fcard xs))"
+lemma fcard_not_fin: "(x |\<notin>| S) = (fcard (finsert x S) = Suc (fcard S))"
 by (lifting fcard_raw_not_memb)
-lemma fcard_suc: "fcard xs = Suc n \<Longrightarrow> \<exists>a ys. a |\<notin>| ys \<and> xs = finsert a ys \<and> fcard ys = n"
+lemma fcard_suc: "fcard S = Suc n \<Longrightarrow> \<exists>x T. x |\<notin>| T \<and> S = finsert x T \<and> fcard T = n"
 by (lifting fcard_raw_suc)
 lemma fcard_delete:
-"fcard (fdelete xs y) = (if y |\<in>| xs then fcard xs - 1 else fcard xs)"
+"fcard (fdelete S y) = (if y |\<in>| S then fcard S - 1 else fcard S)"
 by (lifting fcard_raw_delete)
 text {* funion *}
 lemma funion_simps[simp]:
-"{||} |\<union>| ys = ys"
+"{||} |\<union>| S = S"
-"finsert x xs |\<union>| ys = finsert x (xs |\<union>| ys)"
+"finsert x S |\<union>| T = finsert x (S |\<union>| T)"
 by (lifting append.simps)
 lemma funion_sym:
-"a |\<union>| b = b |\<union>| a"
+"S |\<union>| T = T |\<union>| S"
 by (lifting funion_sym_pre)
 lemma funion_assoc:
-"x |\<union>| xa |\<union>| xb = x |\<union>| (xa |\<union>| xb)"
+"S |\<union>| T |\<union>| U = S |\<union>| (T |\<union>| U)"
 by (lifting append_assoc)
 section {* Induction and Cases rules for finite sets *}
 lemma fset_strong_cases:
-"X = {||} \<or> (\<exists>a Y. a \<notin> fset_to_set Y \<and> X = finsert a Y)"
+"S = {||} \<or> (\<exists>x T. x |\<notin>| T \<and> S = finsert x T)"
 by (lifting fset_raw_strong_cases)
 lemma fset_exhaust[case_names fempty finsert, cases type: fset]:
 shows "\<lbrakk>S = {||} \<Longrightarrow> P; \<And>x S'. S = finsert x S' \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
 by (lifting list.exhaust)
 text {* fmap *}
 lemma fmap_simps[simp]:
 "fmap (f :: 'a \<Rightarrow> 'b) {||} = {||}"
-"fmap f (finsert x xs) = finsert (f x) (fmap f xs)"
+"fmap f (finsert x S) = finsert (f x) (fmap f S)"
 by (lifting map.simps)
 lemma fmap_set_image:
-"fset_to_set (fmap f fs) = f ` (fset_to_set fs)"
+"fset_to_set (fmap f S) = f ` (fset_to_set S)"
-apply (induct fs)
+by (induct S) (simp_all)
-apply (simp_all)
-done
 lemma inj_fmap_eq_iff:
-"inj f \<Longrightarrow> (fmap f l = fmap f m) = (l = m)"
+"inj f \<Longrightarrow> (fmap f S = fmap f T) = (S = T)"
 by (lifting inj_map_eq_iff)
-lemma fmap_funion: "fmap f (a |\<union>| b) = fmap f a |\<union>| fmap f b"
+lemma fmap_funion: "fmap f (S |\<union>| T) = fmap f S |\<union>| fmap f T"
 by (lifting map_append)
 lemma fin_funion:
-"(e |\<in>| l |\<union>| r) = (e |\<in>| l \<or> e |\<in>| r)"
+"x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"
 by (lifting memb_append)
 text {* ffold *}
 lemma ffold_nil: "ffold f z {||} = z"
 "\<lbrakk>rsp_fold f; h |\<in>| b\<rbrakk> \<Longrightarrow> ffold f z b = f h (ffold f z (fdelete b h))"
 by (lifting memb_commute_ffold_raw)
 text {* fdelete *}
-lemma fin_fdelete: "(x |\<in>| fdelete A a) = (x |\<in>| A \<and> x \<noteq> a)"
+lemma fin_fdelete:
+shows "x |\<in>| fdelete S y \<longleftrightarrow> x |\<in>| S \<and> x \<noteq> y"
 by (lifting memb_delete_raw)
-lemma fin_fdelete_ident: "a |\<notin>| fdelete A a"
+lemma fin_fdelete_ident:
+shows "x |\<notin>| fdelete S x"
 by (lifting memb_delete_raw_ident)
-lemma not_memb_fdelete_ident: "b |\<notin>| A \<Longrightarrow> fdelete A b = A"
+lemma not_memb_fdelete_ident:
+shows "x |\<notin>| S \<Longrightarrow> fdelete S x = S"
 by (lifting not_memb_delete_raw_ident)
 lemma fset_fdelete_cases:
-"X = {||} \<or> (\<exists>a. a |\<in>| X \<and> X = finsert a (fdelete X a))"
+shows "S = {||} \<or> (\<exists>x. x |\<in>| S \<and> S = finsert x (fdelete S x))"
 by (lifting fset_raw_delete_raw_cases)
 text {* inter *}
-lemma finter_empty_l: "({||} |\<inter>| r) = {||}"
+lemma finter_empty_l: "({||} |\<inter>| S) = {||}"
 by (lifting finter_raw.simps(1))
-lemma finter_empty_r: "(l |\<inter>| {||}) = {||}"
+lemma finter_empty_r: "(S |\<inter>| {||}) = {||}"
 by (lifting finter_raw_empty)
 lemma finter_finsert:
-"(finsert h t |\<inter>| l) = (if h |\<in>| l then finsert h (t |\<inter>| l) else t |\<inter>| l)"
+"finsert x S |\<inter>| T = (if x |\<in>| T then finsert x (S |\<inter>| T) else S |\<inter>| T)"
 by (lifting finter_raw.simps(2))
 lemma fin_finter:
-"(e |\<in>| (l |\<inter>| r)) = (e |\<in>| l \<and> e |\<in>| r)"
+"x |\<in>| (S |\<inter>| T) \<longleftrightarrow> x |\<in>| S \<and> x |\<in>| T"
 by (lifting memb_finter_raw)
 lemma expand_fset_eq:
-"(xs = ys) = (\<forall>x. (x |\<in>| xs) = (x |\<in>| ys))"
+"(S = T) = (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
 by (lifting list_eq.simps[simplified memb_def[symmetric]])
 ML {*
 fun dest_fsetT (Type ("FSet.fset", [T])) = T

changeset 1822	4465723e35e7
parent 1821	509a0ccc4f32
child 1823	91ba55dba5e0