nominal2: comparison Nominal/FSet.thy

equal deleted inserted replaced

-:900ef226973e
+:d3fe17786640
 quotient_type
 'a fset = "'a list" / "list_eq"
 by (rule list_eq_equivp)
-section {* empty fset, finsert and membership *}
+section {* Empty fset, Finsert and Membership *}
 quotient_definition
 fempty  ("{||}")
 where
 "fempty :: 'a fset"
 "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" is "memb"
 abbreviation
 fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50)
 where
-"x |\<notin>| S \<equiv> \<not>(x |\<in>| S)"
+"x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
 lemma memb_rsp[quot_respect]:
 shows "(op = ===> op \<approx> ===> op =) memb memb"
 by (auto simp add: memb_def)
 by simp
 section {* Augmenting an fset -- @{const finsert} *}
 lemma nil_not_cons:
-shows
+shows "\<not> ([] \<approx> x # xs)"
-"\<not> ([] \<approx> x # xs)"
+and   "\<not> (x # xs \<approx> [])"
-"\<not> (x # xs \<approx> [])"
 by auto
 lemma not_memb_nil:
-"\<not> memb x []"
+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 singleton_list_eq:
 shows "[x] \<approx> [y] \<longleftrightarrow> x = y"
 by (simp add: id_simps) auto
-section {* Union *}
+section {* Unions *}
 quotient_definition
 funion  (infixl "|\<union>|" 65)
 where
 "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 "fcard :: 'a fset \<Rightarrow> nat"
 is
 "fcard_raw"
 lemma fcard_raw_0:
-fixes xs :: "'a list"
+shows "fcard_raw xs = 0 \<longleftrightarrow> xs \<approx> []"
-shows "(fcard_raw xs = 0) = (xs \<approx> [])"
 by (induct xs) (auto simp add: memb_def)
 lemma fcard_raw_gt_0:
 assumes a: "x \<in> set xs"
 shows "0 < fcard_raw xs"
+using a by (induct xs) (auto simp add: memb_def)
+lemma fcard_raw_not_memb:
+shows "\<not> memb x xs \<longleftrightarrow> fcard_raw (x # xs) = Suc (fcard_raw xs)"
+by auto
+lemma fcard_raw_suc:
+assumes a: "fcard_raw xs = Suc n"
+shows "\<exists>x ys. \<not> (memb x ys) \<and> xs \<approx> (x # ys) \<and> fcard_raw ys = n"
 using a
-by (induct xs) (auto simp add: memb_def)
+by (induct xs) (auto simp add: memb_def split: if_splits)
-lemma fcard_raw_not_memb:
-fixes x :: "'a"
-shows "\<not>(memb x xs) \<longleftrightarrow> fcard_raw (x # xs) = Suc (fcard_raw xs)"
-by auto
-lemma fcard_raw_suc:
-fixes xs :: "'a list"
-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)
-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
-next
-case False
-then show ?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
 lemma singleton_fcard_1:
-shows "set xs = {x} \<Longrightarrow> fcard_raw xs = Suc 0"
+shows "set xs = {x} \<Longrightarrow> fcard_raw xs = 1"
-apply (induct xs)
+by (induct xs) (auto simp add: memb_def subset_insert)
-apply simp_all
-apply auto
-apply (subgoal_tac "set xs = {x}")
-apply simp
-apply (simp add: memb_def)
-apply auto
-apply (subgoal_tac "set xs = {}")
-apply simp
-by (metis memb_def subset_empty subset_insert)
 lemma fcard_raw_1:
-fixes a :: "'a list"
 shows "fcard_raw xs = 1 \<longleftrightarrow> (\<exists>x. xs \<approx> [x])"
 apply (auto dest!: fcard_raw_suc)
 apply (simp add: fcard_raw_0)
 apply (rule_tac x="x" in exI)
 apply simp
 apply (subgoal_tac "set xs = {x}")
-apply (erule singleton_fcard_1)
+apply (drule 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)"
+shows "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 fcard_raw_rsp_aux:
 assumes a: "xs \<approx> ys"
 shows "fcard_raw xs = fcard_raw ys"
 apply(simp add: fcard_raw_delete_one)
 apply(metis Suc_pred'[OF fcard_raw_gt_0] fcard_raw_delete_one memb_def)
 done
 lemma fcard_raw_rsp[quot_respect]:
-"(op \<approx> ===> op =) fcard_raw fcard_raw"
+shows "(op \<approx> ===> op =) fcard_raw fcard_raw"
 by (simp add: fcard_raw_rsp_aux)
 section {* fmap and fset comprehension *}
 apply (rule_tac x="x" in exI)
 apply (rule_tac x="a # ys" in exI)
 apply (auto simp add: memb_def)
 done
+section {* deletion *}
 fun
 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 memb_delete_raw:
 "memb x (delete_raw xs y) = (memb x xs \<and> x \<noteq> y)"
 by (induct xs arbitrary: x y) (auto simp add: memb_def)
 lemma delete_raw_rsp:
-"l \<approx> r \<Longrightarrow> delete_raw l x \<approx> delete_raw r x"
+"xs \<approx> ys \<Longrightarrow> delete_raw xs x \<approx> delete_raw ys x"
 by (simp add: memb_def[symmetric] memb_delete_raw)
 lemma [quot_respect]:
 "(op \<approx> ===> op = ===> op \<approx>) delete_raw delete_raw"
 by (simp add: memb_def[symmetric] memb_delete_raw)
 lemma memb_delete_raw_ident:
-"\<not> memb x (delete_raw xs x)"
+shows "\<not> memb x (delete_raw xs x)"
 by (induct xs) (auto simp add: memb_def)
 lemma not_memb_delete_raw_ident:
-"\<not> memb x xs \<Longrightarrow> delete_raw xs x = xs"
+shows "\<not> memb x xs \<Longrightarrow> delete_raw xs x = xs"
 by (induct xs) (auto simp add: memb_def)
 lemma fset_raw_delete_raw_cases:
 "xs = [] \<or> (\<exists>x. memb x xs \<and> xs \<approx> x # delete_raw xs x)"
 by (induct xs) (auto simp add: memb_def)
 lemma fcard_0: "(fcard S = 0) = (S = {||})"
 by (lifting fcard_raw_0)
 lemma fcard_1:
-fixes S::"'b fset"
 shows "(fcard S = 1) = (\<exists>x. S = {|x|})"
 by (lifting fcard_raw_1)
-lemma fcard_gt_0: "x \<in> fset_to_set S \<Longrightarrow> 0 < fcard S"
+lemma fcard_gt_0:
+shows "x \<in> fset_to_set S \<Longrightarrow> 0 < fcard S"
 by (lifting fcard_raw_gt_0)
-lemma fcard_not_fin: "(x |\<notin>| S) = (fcard (finsert x S) = Suc (fcard S))"
+lemma fcard_not_fin:
+shows "(x |\<notin>| S) = (fcard (finsert x S) = Suc (fcard S))"
 by (lifting fcard_raw_not_memb)
 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)
 by (lifting fcard_raw_delete)
 text {* funion *}
 lemma funion_simps[simp]:
-"{||} |\<union>| S = S"
+shows "{||} |\<union>| S = S"
-"finsert x S |\<union>| T = finsert x (S |\<union>| T)"
+and   "finsert x S |\<union>| T = finsert x (S |\<union>| T)"
 by (lifting append.simps)
 lemma funion_sym:
-"S |\<union>| T = T |\<union>| S"
+shows "S |\<union>| T = T |\<union>| S"
 by (lifting funion_sym_pre)
 lemma funion_assoc:
-"S |\<union>| T |\<union>| U = S |\<union>| (T |\<union>| U)"
+shows "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:

changeset 1860	d3fe17786640
parent 1826	faa7e6033f2e
child 1878	c22947214948