diff -r 42b90994ac77 -r 89d772dae4d4 Quot/Examples/FSet3.thy
--- a/Quot/Examples/FSet3.thy	Fri Jan 08 15:02:12 2010 +0100
+++ b/Quot/Examples/FSet3.thy	Fri Jan 08 19:46:22 2010 +0100
@@ -77,32 +77,28 @@
 
 text {* raw section *}
 
-lemma nil_not_cons: 
-  shows "\<not>[] \<approx> x # xs" 
-by auto
+lemma nil_not_cons:
+  shows "\<not>[] \<approx> x # xs"
+  by auto
 
 lemma memb_cons_iff:
   shows "memb x (y # xs) = (x = y \<or> memb x xs)"
-by (induct xs) (auto simp add: memb_def)
+  by (induct xs) (auto simp add: memb_def)
 
 lemma memb_consI1:
   shows "memb x (x # xs)"
-by (simp add: memb_def)
+  by (simp add: memb_def)
 
-lemma memb_consI2: 
+lemma memb_consI2:
   shows "memb x xs \<Longrightarrow> memb x (y # xs)"
   by (simp add: memb_def)
 
 lemma memb_absorb:
-  shows "memb x xs \<Longrightarrow> (x # xs) \<approx> xs"
-by (induct xs) (auto simp add: memb_def)
+  shows "memb x xs \<Longrightarrow> x # xs \<approx> xs"
+  by (induct xs) (auto simp add: memb_def id_simps)
 
 text {* lifted section *}
 
-lemma fempty_not_finsert[simp]:
-  shows "{||} \<noteq> finsert x S"
-by (lifting nil_not_cons)
-
 lemma fin_finsert_iff[simp]:
   "x |\<in>| finsert y S = (x = y \<or> x |\<in>| S)"
 by (lifting memb_cons_iff) 
@@ -112,9 +108,10 @@
   and   finsertI2: "x |\<in>| S \<Longrightarrow> x |\<in>| finsert y S"
   by (lifting memb_consI1, lifting memb_consI2)
 
+
 lemma finsert_absorb [simp]: 
   shows "x |\<in>| S \<Longrightarrow> finsert x S = S"
-by (lifting memb_absorb)
+  by (lifting memb_absorb)
 
 
 section {* Singletons *}
@@ -123,18 +120,22 @@
 
 lemma singleton_list_eq:
   shows "[x] \<approx> [y] \<longleftrightarrow> x = y"
-by auto
+  by (simp add: id_simps) auto
 
 text {* lifted section *}
 
+lemma fempty_not_finsert[simp]:
+  shows "{||} \<noteq> finsert x S"
+  by (lifting nil_not_cons)
+
 lemma fsingleton_eq[simp]:
   shows "{|x|} = {|y|} \<longleftrightarrow> x = y"
-by (lifting singleton_list_eq)
+  by (lifting singleton_list_eq)
 
 section {* Union *}
 
 quotient_definition
-   "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" (infixl "|\<union>|" 65)
+  "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" (infixl "|\<union>|" 65)
 as
   "op @"
 
@@ -244,21 +245,21 @@
 (* concat.simps(1) and concat.simps(2) contain the    *)
 (* type variables ?'a1.0 (which are turned into frees *)
 (* 'a_1                                               *)
-lemma concat1: 
+lemma concat1:
   shows "concat [] \<approx> []"
-by (simp)
+by (simp add: id_simps)
 
-lemma concat2: 
-  shows "concat (x # xs) \<approx>  x @ concat xs"
-by (simp)
+lemma concat2:
+  shows "concat (x # xs) \<approx> x @ concat xs"
+by (simp add: id_simps)
 
 lemma concat_rsp[quot_respect]:
   shows "(list_rel op \<approx> OO op \<approx> OO list_rel op \<approx> ===> op \<approx>) concat concat"
 sorry
 
 lemma nil_rsp2[quot_respect]: "(list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) [] []"
-apply (metis FSet3.nil_rsp list_rel.simps(1) pred_comp.intros)
-done
+  apply (metis FSet3.nil_rsp list_rel.simps(1) pred_comp.intros)
+  done
 
 lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B"
   apply (rule eq_reflection)
@@ -350,22 +351,25 @@
 apply(rule refl)
 done
 
+(* Should be true *)
+
+lemma insert_rsp2[quot_respect]:
+  "(op \<approx> ===> list_rel op \<approx> OO op \<approx> OO list_rel op \<approx> ===> list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) op # op #"
+apply auto
+apply (simp add: set_in_eq)
+sorry
+
+lemma append_rsp[quot_respect]:
+  "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
+  by (auto)
+
 lemma fconcat_insert:
   shows "fconcat (finsert x S) = x |\<union>| fconcat S"
 apply(lifting concat2)
-apply(injection)
-(* The Relation is wrong to apply rep_abs_rsp *)
-thm rep_abs_rsp[of "(op \<approx> ===> op =)"]
-defer
-apply (simp only: finsert_def[simplified id_simps])
-apply (simp only: fconcat_def[simplified id_simps])
 apply(cleaning)
-(* finsert_def doesn't get folded, since rep-abs types are incorrect *)
-apply(simp add: comp_def)
-apply (simp add: fconcat_def[simplified id_simps])
+apply (simp add: finsert_def fconcat_def comp_def)
 apply cleaning
-(* The Relation is wrong again. *)
-sorry
+done
 
 text {* raw section *}
 
@@ -493,13 +497,13 @@
   "a \<in> set A \<Longrightarrow> a # A \<approx> A"
 by auto
 
-lemma cons_left_comm: 
-  "x #y # A \<approx> y # x # A"
-by auto
+lemma cons_left_comm:
+  "x # y # A \<approx> y # x # A"
+by (auto simp add: id_simps)
 
-lemma cons_left_idem: 
+lemma cons_left_idem:
   "x # x # A \<approx> x # A"
-by auto
+by (auto simp add: id_simps)
 
 lemma finite_set_raw_strong_cases:
   "(X = []) \<or> (\<exists>a Y. ((a \<notin> set Y) \<and> (X \<approx> a # Y)))"
@@ -593,10 +597,6 @@
 apply(auto)
 sorry
 
-lemma append_rsp[quot_respect]:
-  "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
-by auto
-
 primrec
   inter_raw
 where