# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1271223243 -7200
# Node ID 509a0ccc4f322d62c1e3517697a82149313858e0
# Parent  de28a91eaca3a238a319a41aa81b5ced88bcd5d6
tuned

diff -r de28a91eaca3 -r 509a0ccc4f32 Nominal/FSet.thy
--- a/Nominal/FSet.thy	Tue Apr 13 15:59:53 2010 +0200
+++ b/Nominal/FSet.thy	Wed Apr 14 07:34:03 2010 +0200
@@ -119,13 +119,9 @@
   "fcard_raw"
 
 lemma fcard_raw_0:
-  fixes a :: "'a list"
-  shows "(fcard_raw a = 0) = (a \<approx> [])"
-  apply (induct a)
-  apply auto
-  apply (drule memb_absorb)
-  apply (auto simp add: nil_not_cons)
-  done
+  fixes xs :: "'a list"
+  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"
@@ -136,14 +132,14 @@
 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)
@@ -169,28 +165,29 @@
     qed
   qed
 
-lemma singleton_fcard_1: "set a = {b} \<Longrightarrow> fcard_raw a = Suc 0"
-  apply (induct a)
+lemma singleton_fcard_1: 
+  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
@@ -200,13 +197,13 @@
   by (induct xs) (auto dest: fcard_raw_gt_0 simp add: memb_def)
 
 lemma fcard_raw_rsp_aux:
-  assumes a: "a \<approx> b"
-  shows "fcard_raw a = fcard_raw b"
+  assumes a: "xs \<approx> ys"
+  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
@@ -224,12 +221,12 @@
  "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)"
-  by (induct l) (simp_all add: not_memb_nil memb_cons_iff)
+  "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 *}
 
@@ -247,20 +244,20 @@
   by (auto simp add: map_rsp_aux)
 
 lemma cons_left_comm:
-  "x # y # A \<approx> y # x # A"
-  by (auto simp add: id_simps)
+  "x # y # xs \<approx> y # x # xs"
+  by auto
 
 lemma cons_left_idem:
-  "x # x # A \<approx> x # A"
-  by (auto simp add: id_simps)
+  "x # x # xs \<approx> x # xs"
+  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)))"
-  apply (induct X)
+  "(xs = []) \<or> (\<exists>x ys. ((x \<notin> set ys) \<and> (xs \<approx> x # ys)))"
+  apply (induct xs)
   apply (simp)
   apply (rule disjI2)
   apply (erule disjE)
@@ -268,12 +265,12 @@
   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="a # Y" in exI)
+  apply (rule_tac x="x" in exI)
+  apply (rule_tac x="a # ys" in exI)
   apply (auto)
   done
 
@@ -284,24 +281,24 @@
 | "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)"
-  by (induct A arbitrary: x a) (auto simp add: memb_def)
+  "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 [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)"
-  by (induct A) (auto simp add: memb_def)
+  "\<not> memb x (delete_raw xs x)"
+  by (induct xs) (auto simp add: memb_def)
 
 lemma not_memb_delete_raw_ident:
-  "\<not> memb b A \<Longrightarrow> delete_raw A b = A"
-  by (induct A) (auto simp add: memb_def)
+  "\<not> memb x xs \<Longrightarrow> delete_raw xs x = xs"
+  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)"
-  by (induct X) (auto simp add: memb_def)
+  "xs = [] \<or> (\<exists>x. memb x xs \<and> xs \<approx> x # delete_raw xs x)"
+  by (induct xs) (auto simp add: memb_def)
 
 lemma fdelete_raw_filter:
   "delete_raw xs y = [x \<leftarrow> xs. x \<noteq> y]"
@@ -356,9 +353,11 @@
   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)
@@ -427,13 +426,9 @@
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
   by (auto)
 
-lemma set_cong: "(set x = set y) = (x \<approx> y)"
-  apply rule
-  apply simp_all
-  apply (induct x y rule: list_induct2')
-  apply simp_all
-  apply auto
-  done
+lemma set_cong: 
+  shows "(set x = set y) = (x \<approx> y)"
+  by auto
 
 lemma inj_map_eq_iff:
   "inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)"
@@ -515,7 +510,9 @@
 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"