nominal2: comparison Nominal/FSet.thy

equal deleted inserted replaced

-:37480540c1af
+:63dd459dbc0d
 lemma nil_not_cons:
 shows
 "\<not>[] \<approx> x # xs"
 "\<not>x # xs \<approx> []"
 by auto
+lemma not_memb_nil:
+"\<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 fcard_raw_suc:
 fixes xs :: "'a list"
 fixes n :: "nat"
 assumes c: "fcard_raw xs = Suc n"
-shows "\<exists>a ys. ~(memb a ys) \<and> xs \<approx> (a # ys)"
+shows "\<exists>a ys. ~(memb a ys) \<and> xs \<approx> (a # ys) \<and> fcard_raw ys = n"
+unfolding memb_def
 using c
-apply(induct xs)
+proof (induct xs)
+case Nil
+then show ?case by simp
+next
+case (Cons a xs)
+have f1: "fcard_raw xs = Suc n \<Longrightarrow> \<exists>a ys. a \<notin> set ys \<and> xs \<approx> a # ys \<and> fcard_raw ys = n" by fact
+have f2: "fcard_raw (a # xs) = Suc n" by fact
+then show ?case proof (cases "a \<in> set xs")
+case True
+then show ?thesis using f1 f2 apply -
+apply (simp add: memb_def)
+apply clarify
+by metis
+case False
+then have ?thesis using f1 f2 apply -
+apply (rule_tac x="a" in exI)
+apply (rule_tac x="xs" in exI)
+apply (simp add: memb_def)
+done
+qed
+qed
+qed
+lemma singleton_fcard_1: "set a = {b} \<Longrightarrow> fcard_raw a = Suc 0"
+apply (induct a)
+apply simp_all
+apply auto
+apply (subgoal_tac "set a2 = {b}")
 apply simp
-apply (auto)
+apply (simp add: memb_def)
-apply (metis memb_def)
+apply auto
+apply (subgoal_tac "set a2 = {}")
+apply simp
+by (metis memb_def subset_empty subset_insert)
+lemma fcard_raw_1:
+fixes a :: "'a list"
+shows "(fcard_raw a = 1) = (\<exists>b. a \<approx> [b])"
+apply auto
+apply (drule fcard_raw_suc)
+apply clarify
+apply (simp add: fcard_raw_0)
+apply (rule_tac x="aa" in exI)
+apply simp
+apply (subgoal_tac "set a = {b}")
+apply (erule singleton_fcard_1)
+apply auto
 done
 lemma fcard_raw_delete_one:
 "fcard_raw ([x \<leftarrow> xs. x \<noteq> y]) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
 by (induct xs) (auto dest: fcard_raw_gt_0 simp add: memb_def)
 lemma map_append:
 "(map f (a @ b)) \<approx> (map f a) @ (map f b)"
 by simp
+lemma memb_append:
+"memb e (append l r) = (memb e l \<or> memb e r)"
+by (induct l) (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"
 lemma none_mem_nil:
 "(\<forall>a. a \<notin> set A) = (A \<approx> [])"
 by simp
-lemma finite_set_raw_strong_cases:
+lemma fset_raw_strong_cases:
 "(X = []) \<or> (\<exists>a Y. ((a \<notin> set Y) \<and> (X \<approx> a # Y)))"
 apply (induct X)
 apply (simp)
 apply (rule disjI2)
 apply (erule disjE)
 delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"
 where
 "delete_raw [] x = []"
 | "delete_raw (a # A) x = (if (a = x) then delete_raw A x else a # (delete_raw A x))"
-lemma mem_delete_raw:
+lemma memb_delete_raw:
-"x \<in> set (delete_raw A a) = (x \<in> set A \<and> \<not>(x = a))"
+"memb x (delete_raw A a) = (memb x A \<and> x \<noteq> a)"
-by (induct A arbitrary: x a) (auto)
+by (induct A arbitrary: x a) (auto simp add: memb_def)
-lemma mem_delete_raw_ident:
+lemma [quot_respect]:
-"\<not>(a \<in> set (delete_raw A a))"
+"(op \<approx> ===> op = ===> op \<approx>) delete_raw delete_raw"
-by (induct A) (auto)
+by (simp add: memb_def[symmetric] memb_delete_raw)
-lemma not_mem_delete_raw_ident:
+lemma memb_delete_raw_ident:
-"b \<notin> set A \<Longrightarrow> (delete_raw A b = A)"
+"\<not> memb a (delete_raw A a)"
-by (induct A) (auto)
+by (induct A) (auto simp add: memb_def)
-lemma finite_set_raw_delete_raw_cases:
+lemma not_memb_delete_raw_ident:
-"X = [] \<or> (\<exists>a. a mem X \<and> X \<approx> a # delete_raw X a)"
+"\<not> memb b A \<Longrightarrow> delete_raw A b = A"
-by (induct X) (auto)
+by (induct A) (auto simp add: memb_def)
-lemma list2set_thm:
+lemma fset_raw_delete_raw_cases:
-shows "set [] = {}"
+"X = [] \<or> (\<exists>a. memb a X \<and> X \<approx> a # delete_raw X a)"
-and "set (h # t) = insert h (set t)"
+by (induct X) (auto simp add: memb_def)
-by (auto)
+lemma fdelete_raw_filter:
-lemma list2set_rsp[quot_respect]:
+"delete_raw xs y = [x \<leftarrow> xs. x \<noteq> y]"
+by (induct xs) simp_all
+lemma fcard_raw_delete:
+"fcard_raw (delete_raw xs y) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
+by (simp add: fdelete_raw_filter fcard_raw_delete_one)
+lemma set_rsp[quot_respect]:
 "(op \<approx> ===> op =) set set"
 by auto
 definition
 rsp_fold
 where
 "rsp_fold f = (\<forall>u v w. (f u (f v w) = f v (f u w)))"
 primrec
-fold_raw :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"
+ffold_raw :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"
 where
-"fold_raw f z [] = z"
+"ffold_raw f z [] = z"
-| "fold_raw f z (a # A) =
+| "ffold_raw f z (a # A) =
 (if (rsp_fold f) then
-if a mem A then fold_raw f z A
+if memb a A then ffold_raw f z A
-else f a (fold_raw f z A)
+else f a (ffold_raw f z A)
 else z)"
+lemma memb_commute_ffold_raw:
+"rsp_fold f \<Longrightarrow> memb h b \<Longrightarrow> ffold_raw f z b = f h (ffold_raw f z (delete_raw b h))"
+apply (induct b)
+apply (simp add: not_memb_nil)
+apply (simp add: ffold_raw.simps)
+apply (rule conjI)
+apply (rule_tac [!] impI)
+apply (rule_tac [!] conjI)
+apply (rule_tac [!] impI)
+apply (simp_all add: memb_delete_raw)
+apply (simp add: memb_cons_iff)
+apply (simp add: not_memb_delete_raw_ident)
+apply (simp add: memb_cons_iff rsp_fold_def)
+done
+primrec
+finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+where
+"finter_raw [] l = []"
+| "finter_raw (h # t) l =
+(if memb h l then h # (finter_raw t l) else finter_raw t l)"
+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)"
+apply (induct l)
+apply (simp add: not_memb_nil)
+apply (simp add: finter_raw.simps)
+apply (simp add: memb_cons_iff)
+apply auto
+done
+lemma [quot_respect]:
+"(op \<approx> ===> op \<approx> ===> op \<approx>) finter_raw finter_raw"
+by (simp add: memb_def[symmetric] memb_finter_raw)
 section {* Constants on the Quotient Type *}
 quotient_definition
 "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset"
 is "delete_raw"
 quotient_definition
 "fset_to_set :: 'a fset \<Rightarrow> 'a set"
 is "set"
+quotient_definition
+"ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b"
+is "ffold_raw"
+quotient_definition
+finter (infix "|\<inter>|" 50)
+where
+"finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+is "finter_raw"
 lemma funion_sym_pre:
 "a @ b \<approx> b @ a"
 by auto
 shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
 by auto
 section {* lifted part *}
+lemma not_fin_fnil: "x |\<notin>| {||}"
+by (lifting not_memb_nil)
 lemma fin_finsert_iff[simp]:
 "x |\<in>| finsert y S = (x = y \<or> x |\<in>| S)"
 by (lifting memb_cons_iff)
 by (lifting singleton_list_eq)
 text {* fset_to_set *}
 lemma fset_to_set_simps[simp]:
-"fset_to_set {||} = {}"
+"fset_to_set {||} = ({} :: 'a set)"
-"fset_to_set (finsert (h :: 'b) t) = insert h (fset_to_set t)"
+"fset_to_set (finsert (h :: 'a) t) = insert h (fset_to_set t)"
-by (lifting list2set_thm)
+by (lifting set.simps)
 lemma in_fset_to_set:
 "x \<in> fset_to_set xs \<equiv> x |\<in>| xs"
 by (lifting memb_def[symmetric])
-lemma none_in_fempty:
+lemma none_fin_fempty:
 "(\<forall>a. a \<notin> fset_to_set A) = (A = {||})"
 by (lifting none_mem_nil)
 lemma fset_cong:
 "(fset_to_set x = fset_to_set y) = (x = y)"
 by (lifting fcard_raw_cons)
 lemma fcard_0: "(fcard a = 0) = (a = {||})"
 by (lifting fcard_raw_0)
+lemma fcard_1: "(fcard a = 1) = (\<exists>b. a = {|b|})"
+by (lifting fcard_raw_1)
 lemma fcard_gt_0: "x \<in> fset_to_set xs \<Longrightarrow> 0 < fcard xs"
 by (lifting fcard_raw_gt_0)
-lemma fcard_not_memb: "(x |\<notin>| xs) = (fcard (finsert x xs) = Suc (fcard xs))"
+lemma fcard_not_fin: "(x |\<notin>| xs) = (fcard (finsert x xs) = Suc (fcard xs))"
 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"
+lemma fcard_suc: "fcard xs = Suc n \<Longrightarrow> \<exists>a ys. a |\<notin>| ys \<and> xs = finsert a ys \<and> fcard ys = n"
 by (lifting fcard_raw_suc)
+lemma fcard_delete:
+"fcard (fdelete xs y) = (if y |\<in>| xs then fcard xs - 1 else fcard xs)"
+by (lifting fcard_raw_delete)
 text {* funion *}
 lemma funion_simps[simp]:
 "{||} |\<union>| ys = ys"
 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)"
-by (lifting finite_set_raw_strong_cases)
+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)
 apply simp_all
 apply (induct_tac xa rule: fset_induct)
 apply simp_all
 done
-(* fmap *)
+text {* fmap *}
 lemma fmap_simps[simp]:
 "fmap (f :: 'a \<Rightarrow> 'b) {||} = {||}"
 "fmap f (finsert x xs) = finsert (f x) (fmap f xs)"
 by (lifting map.simps)
 by (lifting inj_map_eq_iff)
 lemma fmap_funion: "fmap f (a |\<union>| b) = fmap f a |\<union>| fmap f b"
 by (lifting map_append)
+lemma fin_funion:
+"(e |\<in>| l |\<union>| r) = (e |\<in>| l \<or> e |\<in>| r)"
+by (lifting memb_append)
+text {* ffold *}
+lemma ffold_nil: "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 (lifting ffold_raw.simps(2)[where 'a="'b" and 'b="'a"])
+lemma fin_commute_ffold:
+"\<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)"
+by (lifting memb_delete_raw)
+lemma fin_fdelete_ident: "a |\<notin>| fdelete A a"
+by (lifting memb_delete_raw_ident)
+lemma not_memb_fdelete_ident: "b |\<notin>| A \<Longrightarrow> fdelete A b = A"
+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))"
+by (lifting fset_raw_delete_raw_cases)
+text {* inter *}
+lemma finter_empty_l: "({||} |\<inter>| r) = {||}"
+by (lifting finter_raw.simps(1))
+lemma finter_empty_r: "(l |\<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)"
+by (lifting finter_raw.simps(2))
+lemma fin_finter:
+"(e |\<in>| (l |\<inter>| r)) = (e |\<in>| l \<and> e |\<in>| r)"
+by (lifting memb_finter_raw)
 ML {*
 fun dest_fsetT (Type ("FSet.fset", [T])) = T
 | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
 *}

changeset 1819	63dd459dbc0d
parent 1817	f20096761790
child 1820	de28a91eaca3