# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260622441 -3600
# Node ID 33cd648df179913428abb9216d8f79fd0a20034c
# Parent  e16523f01908fe7e2d74d745dcb4de396f1e247d# Parent  8d5408322de50529b6f0a52ed7e981d6bc0d01f5
merged

diff -r e16523f01908 -r 33cd648df179 Quot/Examples/FSet3.thy
--- a/Quot/Examples/FSet3.thy	Sat Dec 12 13:53:46 2009 +0100
+++ b/Quot/Examples/FSet3.thy	Sat Dec 12 13:54:01 2009 +0100
@@ -34,11 +34,11 @@
 
 
 lemma no_mem_nil: 
-  "(\<forall>a. \<not>(a \<in> set A)) = (A = [])"
+  "(\<forall>a. a \<notin> set A) = (A = [])"
 by (induct A) (auto)
 
 lemma none_mem_nil: 
-  "(\<forall>a. \<not>(a \<in> set A)) = (A \<approx> [])"
+  "(\<forall>a. a \<notin> set A) = (A \<approx> [])"
 by simp
 
 lemma mem_cons: 
@@ -54,10 +54,23 @@
 by auto
 
 lemma finite_set_raw_strong_cases:
-  "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a mem Y) \<and> (X \<approx> a # Y)))"
+  "(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)
+  apply (rule_tac x="a" in exI)
+  apply (rule_tac x="[]" in exI)
+  apply (simp)
+  apply (erule exE)+
+  apply (case_tac "a = aa")
+  apply (rule_tac x="a" in exI)
+  apply (rule_tac x="Y" in exI)
+  apply (simp)
+  apply (rule_tac x="aa" in exI)
+  apply (rule_tac x="a # Y" in exI)
   apply (auto)
-  sorry
+  done
 
 fun
   delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"
@@ -65,13 +78,9 @@
   "delete_raw [] x = []"
 | "delete_raw (a # A) x = (if (a = x) then delete_raw A x else a # (delete_raw A x))"
 
-(* definitely FALSE
 lemma mem_delete_raw:
-  "x mem (delete_raw A a) = x mem A \<and> \<not>(x = a)"
-apply(induct A arbitrary: x a)
-apply(auto)
-sorry
-*)
+  "x \<in> set (delete_raw A a) = (x \<in> set A \<and> \<not>(x = a))"
+  by (induct A arbitrary: x a) (auto)
 
 lemma mem_delete_raw_ident:
   "\<not>(a \<in> set (delete_raw A a))"
@@ -88,26 +97,22 @@
 sorry
 
 lemma cons_delete_raw:
-  "a # (delete_raw A a) \<approx> (if a mem A then A else (a # A))"
+  "a # (delete_raw A a) \<approx> (if a \<in> set A then A else (a # A))"
 sorry
 
 lemma mem_cons_delete_raw:
-    "a mem A \<Longrightarrow> a # (delete_raw A a) \<approx> A"
-sorry
-
-lemma finite_set_raw_delete_raw_cases1:
-    "X = [] \<or> (\<exists>a. X \<approx> a # delete_raw X a)"
+    "a \<in> set A \<Longrightarrow> a # (delete_raw A a) \<approx> A"
 sorry
 
 lemma finite_set_raw_delete_raw_cases:
     "X = [] \<or> (\<exists>a. a mem X \<and> X \<approx> a # delete_raw X a)"
-sorry
+  by (induct X) (auto)
 
 fun
   card_raw :: "'a list \<Rightarrow> nat"
 where
   card_raw_nil: "card_raw [] = 0"
-| card_raw_cons: "card_raw (x # xs) = (if x mem xs then card_raw xs else Suc (card_raw xs))"
+| card_raw_cons: "card_raw (x # xs) = (if x \<in> set xs then card_raw xs else Suc (card_raw xs))"
 
 lemma not_mem_card_raw:
   fixes x :: "'a"
@@ -116,28 +121,22 @@
   sorry
 
 lemma card_raw_suc:
-  fixes xs :: "'a list"
-  fixes n :: "nat"
   assumes c: "card_raw xs = Suc n"
-  shows "\<exists>a ys. \<not>(a mem ys) \<and> xs \<approx> (a # ys)"
-  using c
-apply(induct xs)
-(*apply(metis mem_delete_raw)
-apply(metis mem_delete_raw)
-done*)
-sorry
+  shows "\<exists>a ys. (a \<notin> set ys) \<and> xs \<approx> (a # ys)"
+  using c apply(induct xs)
+  apply(simp)
+  sorry
 
-
-lemma mem_card_raw_not_0:
-  "a mem A \<Longrightarrow> \<not>(card_raw A = 0)"
-sorry
+lemma mem_card_raw_gt_0:
+  "a \<in> set A \<Longrightarrow> 0 < card_raw A"
+  by (induct A) (auto)
 
 lemma card_raw_cons_gt_0:
   "0 < card_raw (a # A)"
-sorry
+  by (induct A) (auto)
 
 lemma card_raw_delete_raw:
-  "card_raw (delete_raw A a) = (if a mem A then card_raw A - 1 else card_raw A)"
+  "card_raw (delete_raw A a) = (if a \<in> set A then card_raw A - 1 else card_raw A)"
 sorry
 
 lemma card_raw_rsp_aux:
@@ -151,16 +150,16 @@
 
 lemma card_raw_0:
   "(card_raw A = 0) = (A = [])"
-sorry
+  by (induct A) (auto)
 
 lemma list2set_thm:
   shows "set [] = {}"
   and "set (h # t) = insert h (set t)"
-sorry
+  by (auto)
 
 lemma list2set_RSP:
   "A \<approx> B \<Longrightarrow> set A = set B"
-sorry
+  by auto
 
 definition
   rsp_fold
@@ -236,7 +235,7 @@
   as "delete_raw"
 
 quotient_def
-  "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<in>f _" [50, 51] 50)
+  "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<union>f _" [50, 51] 50)
   as "op @"
 
 quotient_def
@@ -268,6 +267,8 @@
   MEM x [] = F
   MEM x (h::t) = (x=h) \/ MEM x t *)
 thm none_mem_nil
+(*lemma "(\<forall>a. a \<notin>f A) = (A = fempty)"*)
+
 thm mem_cons
 thm finite_set_raw_strong_cases
 thm card_raw.simps