diff -r 7b74d77a61aa -r d5fce1ead432 Quot/Examples/FSet3.thy
--- a/Quot/Examples/FSet3.thy	Fri Dec 11 17:03:52 2009 +0100
+++ b/Quot/Examples/FSet3.thy	Fri Dec 11 19:19:24 2009 +0100
@@ -2,82 +2,89 @@
 imports "../QuotMain" List
 begin
 
-definition
+fun
   list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)
 where
-  "list_eq x y = (\<forall>e. e mem x = e mem y)"
-
-lemma list_eq_reflp:
-  shows "xs \<approx> xs"
-  by (metis list_eq_def)
+  "list_eq xs ys = (\<forall>e. (e \<in> set xs) = (e \<in> set ys))"
 
 lemma list_eq_equivp:
   shows "equivp list_eq"
-  unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
-  apply (auto intro: list_eq_def)
-  apply (metis list_eq_def)
-  apply (metis list_eq_def)
-  sorry
+unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
+by auto
 
 quotient fset = "'a list" / "list_eq"
   by (rule list_eq_equivp)
 
-lemma not_nil_equiv_cons: "\<not>[] \<approx> a # A" sorry
+lemma not_nil_equiv_cons: 
+  "\<not>[] \<approx> a # A" 
+by auto
 
-(* The 2 lemmas below are different from the ones in QuotList *)
 lemma nil_rsp[quot_respect]:
   shows "[] \<approx> []"
-by (rule list_eq_reflp)
+  by simp
 
-lemma cons_rsp[quot_respect]: (* Better then the one from QuotList *)
-  " (op = ===> op \<approx> ===> op \<approx>) op # op #"
-  sorry
+lemma cons_rsp[quot_respect]: 
+  shows "(op = ===> op \<approx> ===> op \<approx>) op # op #"
+  by simp
 
+(*
 lemma mem_rsp[quot_respect]:
   "(op = ===> op \<approx> ===> op =) (op mem) (op mem)"
-  sorry
+*)
+
 
-lemma no_mem_nil: "(\<forall>a. \<not>(a mem A)) = (A = [])"
-sorry
+lemma no_mem_nil: 
+  "(\<forall>a. \<not>(a \<in> set A)) = (A = [])"
+by (induct A) (auto)
 
-lemma none_mem_nil: "(\<forall>a. \<not>(a mem A)) = (A \<approx> [])"
-sorry
+lemma none_mem_nil: 
+  "(\<forall>a. \<not>(a \<in> set A)) = (A \<approx> [])"
+by simp
 
-lemma mem_cons: "a mem A \<Longrightarrow> a # A \<approx> A"
-sorry
+lemma mem_cons: 
+  "a \<in> set A \<Longrightarrow> a # A \<approx> A"
+by auto
 
-lemma cons_left_comm: "x # y # A \<approx> y # x # A"
-sorry
+lemma cons_left_comm: 
+  "x #y # A \<approx> y # x # A"
+by auto
 
-lemma cons_left_idem: "x # x # A \<approx> x # A"
-sorry
+lemma cons_left_idem: 
+  "x # x # A \<approx> x # A"
+by auto
 
 lemma finite_set_raw_strong_cases:
   "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a mem Y) \<and> (X \<approx> a # Y)))"
   apply (induct X)
-  apply (simp)
+  apply (auto)
   sorry
 
-primrec
+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))"
 
+(* 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
+*)
 
 lemma mem_delete_raw_ident:
-  "\<not>(MEM a (A delete_raw a))"
-sorry
+  "\<not>(a \<in> set (delete_raw A a))"
+by (induct A) (auto)
 
 lemma not_mem_delete_raw_ident:
-  "\<not>(b mem A) \<Longrightarrow> (delete_raw A b = A)"
-sorry
+  "b \<notin> set A \<Longrightarrow> (delete_raw A b = A)"
+by (induct A) (auto)
 
 lemma delete_raw_RSP:
   "A \<approx> B \<Longrightarrow> delete_raw A a \<approx> delete_raw B a"
+apply(induct A arbitrary: B a)
+apply(auto)
 sorry
 
 lemma cons_delete_raw:
@@ -115,9 +122,11 @@
   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)
 apply(metis mem_delete_raw)
-done
+done*)
+sorry
+
 
 lemma mem_card_raw_not_0:
   "a mem A \<Longrightarrow> \<not>(card_raw A = 0)"
@@ -174,13 +183,12 @@
 
 lemma fold_rsp[quot_respect]:
   "(op = ===> op = ===> op \<approx> ===> op =) fold_raw fold_raw"
-  apply (auto)
-  apply (case_tac "rsp_fold x")
+apply(auto)
 sorry
 
 lemma append_rsp[quot_respect]:
   "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
-  sorry
+by auto
 
 primrec
   inter_raw
@@ -199,44 +207,61 @@
 
 (* LIFTING DEFS *)
 
+
+section {* Constants on the Quotient Type *} 
+
 quotient_def
-  "Empty :: 'a fset" as "[]::'a list"
+  "fempty :: 'a fset" 
+  as "[]::'a list"
 
 quotient_def
-  "Insert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" as "op #"
+  "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" 
+  as "op #"
 
 quotient_def
-  "In :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" as "op mem"
+  "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<in>f _" [50, 51] 50)
+  as "\<lambda>x X. x \<in> set X"
 
-quotient_def
-  "Card :: 'a fset \<Rightarrow> nat" as "card_raw"
+abbreviation
+  fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<notin>f _" [50, 51] 50)
+where
+  "a \<notin>f S \<equiv> \<not>(a \<in>f S)"
 
 quotient_def
-  "Delete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" as "delete_raw"
+  "fcard :: 'a fset \<Rightarrow> nat" 
+  as "card_raw"
 
 quotient_def
-  "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" as "op @"
+  "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" 
+  as "delete_raw"
+
+quotient_def
+  "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<in>f _" [50, 51] 50)
+  as "op @"
 
 quotient_def
-  "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" as "inter_raw"
+  "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70)
+  as "inter_raw"
 
 quotient_def
-  "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" as "fold_raw"
+  "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" 
+  as "fold_raw"
 
 quotient_def
-  "fset_to_set :: 'a fset \<Rightarrow> 'a set" as "set"
+  "fset_to_set :: 'a fset \<Rightarrow> 'a set" 
+  as "set"
 
 
-(* LIFTING THMS *)
+section {* Lifted Theorems *}
 
 thm list.cases (* ??? *)
 
 thm cons_left_comm
-lemma "Insert a (Insert b x) = Insert b (Insert a x)"
+lemma "finsert a (finsert b S) = finsert b (finsert a S)"
 by (lifting cons_left_comm)
 
 thm cons_left_idem
-lemma "Insert a (Insert a x) = Insert a x"
+lemma "finsert a (finsert a S) = finsert a S"
 by (lifting cons_left_idem)
 
 (* thm MEM:
@@ -248,14 +273,16 @@
 thm card_raw.simps
 thm not_mem_card_raw
 thm card_raw_suc
-lemma "Card x = Suc n \<Longrightarrow> (\<exists>a b. \<not> In a b & x = Insert a b)"
-by (lifting card_raw_suc)
+
+lemma "fcard X = Suc n \<Longrightarrow> (\<exists>a S. a \<notin>f S & X = finsert a S)"
+(*by (lifting card_raw_suc)*)
+sorry
 
 thm card_raw_cons_gt_0
 thm mem_card_raw_not_0
 thm not_nil_equiv_cons
 thm delete_raw.simps
-thm mem_delete_raw
+(*thm mem_delete_raw*)
 thm card_raw_delete_raw
 thm cons_delete_raw
 thm mem_cons_delete_raw
@@ -268,7 +295,7 @@
 thm list2set_thm
 thm list_eq_def
 thm list.induct
-lemma "\<lbrakk>P Empty; \<And>a x. P x \<Longrightarrow> P (Insert a x)\<rbrakk> \<Longrightarrow> P l"
+lemma "\<lbrakk>P fempty; \<And>a x. P x \<Longrightarrow> P (finsert a x)\<rbrakk> \<Longrightarrow> P l"
 by (lifting list.induct)
 
 (* We also have map and some properties of it in FSet *)
@@ -287,7 +314,7 @@
   apply (auto)
   sorry
 
-lemma "fset_case (f1::'t) f2 (Insert a xa) = f2 a xa"
+lemma "fset_case (f1::'t) f2 (finsert a xa) = f2 a xa"
 apply (lifting list.cases(2))
 done