# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1271361363 -7200
# Node ID d3fe17786640075f6b075f7f5939e1b0728e9bbd
# Parent  900ef226973e89d75c6fb36c28a7b3fc80ed5e80
some tuning of proofs

diff -r 900ef226973e -r d3fe17786640 Nominal/FSet.thy
--- a/Nominal/FSet.thy	Thu Apr 15 16:01:28 2010 +0200
+++ b/Nominal/FSet.thy	Thu Apr 15 21:56:03 2010 +0200
@@ -23,7 +23,7 @@
   '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  ("{||}")
@@ -55,7 +55,7 @@
 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"
@@ -72,13 +72,12 @@
 section {* Augmenting an fset -- @{const finsert} *}
 
 lemma nil_not_cons:
-  shows
-  "\<not> ([] \<approx> x # xs)"
-  "\<not> (x # xs \<approx> [])"
+  shows "\<not> ([] \<approx> x # xs)"
+  and   "\<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:
@@ -103,7 +102,7 @@
   shows "[x] \<approx> [y] \<longleftrightarrow> x = y"
   by (simp add: id_simps) auto
 
-section {* Union *}
+section {* Unions *}
 
 quotient_definition
   funion  (infixl "|\<union>|" 65)
@@ -126,77 +125,41 @@
   "fcard_raw"
 
 lemma fcard_raw_0:
-  fixes xs :: "'a list"
-  shows "(fcard_raw xs = 0) = (xs \<approx> [])"
+  shows "fcard_raw xs = 0 \<longleftrightarrow> 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)
+  using a by (induct xs) (auto simp add: memb_def)
 
 lemma fcard_raw_not_memb:
-  fixes x :: "'a"
-  shows "\<not>(memb x xs) \<longleftrightarrow> 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"
-  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
+  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 split: if_splits)
 
 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 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)
+  shows "set xs = {x} \<Longrightarrow> fcard_raw xs = 1"
+  by (induct xs) (auto simp add: memb_def 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:
@@ -212,7 +175,7 @@
   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)
 
 
@@ -268,6 +231,8 @@
   apply (auto simp add: memb_def)
   done
 
+section {* deletion *}
+
 fun
   delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"
 where
@@ -279,7 +244,7 @@
   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]:
@@ -287,11 +252,11 @@
   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:
@@ -509,14 +474,15 @@
   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"
@@ -529,16 +495,16 @@
 text {* funion *}
 
 lemma funion_simps[simp]:
-  "{||} |\<union>| S = S"
-  "finsert x S |\<union>| T = finsert x (S |\<union>| T)"
+  shows "{||} |\<union>| S = S"
+  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 *}