nominal2: comparison Nominal/FSet.thy

equal deleted inserted replaced

-:de28a91eaca3
+:509a0ccc4f32
 "fcard :: 'a fset \<Rightarrow> nat"
 is
 "fcard_raw"
 lemma fcard_raw_0:
-fixes a :: "'a list"
+fixes xs :: "'a list"
-shows "(fcard_raw a = 0) = (a \<approx> [])"
+shows "(fcard_raw xs = 0) = (xs \<approx> [])"
-apply (induct a)
+by (induct xs) (auto simp add: memb_def)
-apply auto
-apply (drule memb_absorb)
-apply (auto simp add: nil_not_cons)
-done
 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:
 fixes x :: "'a"
 fixes xs :: "'a list"
-shows "(~(memb x xs)) = (fcard_raw (x # xs) = Suc (fcard_raw xs))"
+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>a ys. ~(memb a ys) \<and> xs \<approx> (a # ys) \<and> fcard_raw ys = 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
 apply (simp add: memb_def)
 done
 qed
 qed
-lemma singleton_fcard_1: "set a = {b} \<Longrightarrow> fcard_raw a = Suc 0"
+lemma singleton_fcard_1:
-apply (induct a)
+shows "set xs = {x} \<Longrightarrow> fcard_raw xs = Suc 0"
+apply (induct xs)
 apply simp_all
 apply auto
-apply (subgoal_tac "set a2 = {b}")
+apply (subgoal_tac "set xs = {x}")
 apply simp
 apply (simp add: memb_def)
 apply auto
-apply (subgoal_tac "set a2 = {}")
+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 a = 1) = (\<exists>b. a \<approx> [b])"
+shows "(fcard_raw xs = 1) = (\<exists>x. xs \<approx> [x])"
 apply auto
 apply (drule fcard_raw_suc)
 apply clarify
 apply (simp add: fcard_raw_0)
-apply (rule_tac x="aa" in exI)
+apply (rule_tac x="x" in exI)
 apply simp
-apply (subgoal_tac "set a = {b}")
+apply (subgoal_tac "set xs = {x}")
 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 fcard_raw_rsp_aux:
-assumes a: "a \<approx> b"
+assumes a: "xs \<approx> ys"
-shows "fcard_raw a = fcard_raw b"
+shows "fcard_raw xs = fcard_raw ys"
 using a
-apply(induct a arbitrary: b)
+apply(induct xs arbitrary: ys)
 apply(auto simp add: memb_def)
 apply(metis)
-apply(drule_tac x="[x \<leftarrow> b. x \<noteq> a1]" in meta_spec)
+apply(drule_tac x="[x \<leftarrow> ys. x \<noteq> a]" in meta_spec)
 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]:
 "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
 is
 "map"
 lemma map_append:
-"(map f (a @ b)) \<approx> (map f a) @ (map f b)"
+"map f (xs @ ys) \<approx> (map f xs) @ (map f ys)"
 by simp
 lemma memb_append:
-"memb e (append l r) = (memb e l \<or> memb e r)"
+"memb x (xs @ ys) = (memb x xs \<or> memb x ys)"
-by (induct l) (simp_all add: not_memb_nil memb_cons_iff)
+by (induct xs) (simp_all add: not_memb_nil memb_cons_iff)
 text {* raw section *}
 lemma map_rsp_aux:
 assumes a: "a \<approx> b"
 lemma map_rsp[quot_respect]:
 shows "(op = ===> op \<approx> ===> op \<approx>) map map"
 by (auto simp add: map_rsp_aux)
 lemma cons_left_comm:
-"x # y # A \<approx> y # x # A"
+"x # y # xs \<approx> y # x # xs"
-by (auto simp add: id_simps)
+by auto
 lemma cons_left_idem:
-"x # x # A \<approx> x # A"
+"x # x # xs \<approx> x # xs"
-by (auto simp add: id_simps)
+by auto
 lemma none_mem_nil:
-"(\<forall>a. a \<notin> set A) = (A \<approx> [])"
+"(\<forall>x. x \<notin> set xs) = (xs \<approx> [])"
 by simp
 lemma fset_raw_strong_cases:
-"(X = []) \<or> (\<exists>a Y. ((a \<notin> set Y) \<and> (X \<approx> a # Y)))"
+"(xs = []) \<or> (\<exists>x ys. ((x \<notin> set ys) \<and> (xs \<approx> x # ys)))"
-apply (induct X)
+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 (erule exE)+
-apply (case_tac "a = aa")
+apply (case_tac "x = a")
 apply (rule_tac x="a" in exI)
-apply (rule_tac x="Y" in exI)
+apply (rule_tac x="ys" in exI)
 apply (simp)
-apply (rule_tac x="aa" in exI)
+apply (rule_tac x="x" in exI)
-apply (rule_tac x="a # Y" in exI)
+apply (rule_tac x="a # ys" in exI)
 apply (auto)
 done
 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 A a) = (memb x A \<and> x \<noteq> a)"
+"memb x (delete_raw xs y) = (memb x xs \<and> x \<noteq> y)"
-by (induct A arbitrary: x a) (auto simp add: memb_def)
+by (induct xs arbitrary: x y) (auto simp add: memb_def)
 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 a (delete_raw A a)"
+"\<not> memb x (delete_raw xs x)"
-by (induct A) (auto simp add: memb_def)
+by (induct xs) (auto simp add: memb_def)
 lemma not_memb_delete_raw_ident:
-"\<not> memb b A \<Longrightarrow> delete_raw A b = A"
+"\<not> memb x xs \<Longrightarrow> delete_raw xs x = xs"
-by (induct A) (auto simp add: memb_def)
+by (induct xs) (auto simp add: memb_def)
 lemma fset_raw_delete_raw_cases:
-"X = [] \<or> (\<exists>a. memb a X \<and> X \<approx> a # delete_raw X a)"
+"xs = [] \<or> (\<exists>x. memb x xs \<and> xs \<approx> x # delete_raw xs x)"
-by (induct X) (auto simp add: memb_def)
+by (induct xs) (auto simp add: memb_def)
 lemma fdelete_raw_filter:
 "delete_raw xs y = [x \<leftarrow> xs. x \<noteq> y]"
 by (induct xs) simp_all
 apply (rule_tac [!] impI)
 apply (rule_tac [!] conjI)
 apply (rule_tac [!] impI)
 apply (simp add: in_set_code memb_cons_iff memb_def)
 apply (metis)
-apply (metis Nitpick.list_size_simp(2) ffold_raw.simps(2) length_Suc_conv memb_absorb memb_cons_iff nil_not_cons(2))
+apply (metis Nitpick.list_size_simp(2) ffold_raw.simps(2)
+length_Suc_conv memb_absorb memb_cons_iff nil_not_cons(2))
 defer
-apply (metis Nitpick.list_size_simp(2) ffold_raw.simps(2) length_Suc_conv memb_absorb memb_cons_iff nil_not_cons(2))
+apply (metis Nitpick.list_size_simp(2) ffold_raw.simps(2)
+length_Suc_conv memb_absorb memb_cons_iff nil_not_cons(2))
 apply (subgoal_tac "ffold_raw f z b = f a1 (ffold_raw f z (delete_raw b a1))")
 apply (simp only:)
 apply (rule_tac f="f a1" in arg_cong)
 apply (subgoal_tac "\<forall>e. memb e a2 = memb e (delete_raw b a1)")
 apply simp
 lemma append_rsp[quot_respect]:
 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
 by (auto)
-lemma set_cong: "(set x = set y) = (x \<approx> y)"
+lemma set_cong:
-apply rule
+shows "(set x = set y) = (x \<approx> y)"
-apply simp_all
+by auto
-apply (induct x y rule: list_induct2')
-apply simp_all
-apply auto
-done
 lemma inj_map_eq_iff:
 "inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)"
 by (simp add: expand_set_eq[symmetric] inj_image_eq_iff)
 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|})"
+lemma fcard_1:
+fixes xs::"'b fset"
+shows "(fcard xs = 1) = (\<exists>x. xs = {|x|})"
 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)

changeset 1821	509a0ccc4f32
parent 1820	de28a91eaca3
child 1822	4465723e35e7