--- a/FSet.thy	Wed Oct 28 01:49:31 2009 +0100
+++ b/FSet.thy	Wed Oct 28 10:17:07 2009 +0100
@@ -94,12 +94,7 @@
 lemma card1_0:
   fixes a :: "'a list"
   shows "(card1 a = 0) = (a = [])"
-  apply (induct a)
-   apply (simp)
-  apply (simp_all)
-   apply meson
-  apply (simp_all)
-  done
+  by (induct a) auto
 
 lemma not_mem_card1:
   fixes x :: "'a"
@@ -107,16 +102,12 @@
   shows "~(x memb xs) \<Longrightarrow> card1 (x # xs) = Suc (card1 xs)"
   by simp
 
-
 lemma mem_cons:
   fixes x :: "'a"
   fixes xs :: "'a list"
   assumes a : "x memb xs"
   shows "x # xs \<approx> xs"
-  using a
-  apply (induct xs)
-  apply (auto intro: list_eq.intros)
-  done
+  using a by (induct xs) (auto intro: list_eq.intros )
 
 lemma card1_suc:
   fixes xs :: "'a list"
@@ -177,30 +168,18 @@
 thm fmap_def
 
 
-
+ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *}
+ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *}
 
-ML {*
+(* ML {*
   val consts = [@{const_name "Nil"}, @{const_name "Cons"},
                 @{const_name "membship"}, @{const_name "card1"},
                 @{const_name "append"}, @{const_name "fold1"},
                 @{const_name "map"}];
-*}
-
-ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *}
+*} *)
 
-ML {*
-fun add_lower_defs ctxt defs =
-  let
-    val defs_pre_sym = map symmetric defs
-    val defs_atom = map atomize_thm defs_pre_sym
-    val defs_all = flat (map (add_lower_defs_aux ctxt) defs_atom)
-  in
-    map Thm.varifyT defs_all
-  end
-*}
 ML {* val fset_defs_sym = add_lower_defs @{context} fset_defs *}
 
-
 lemma memb_rsp:
   fixes z
   assumes a: "list_eq x y"
@@ -209,22 +188,16 @@
 
 lemma ho_memb_rsp:
   "(op = ===> (op \<approx> ===> op =)) (op memb) (op memb)"
-  apply (simp add: FUN_REL.simps)
-  apply (metis memb_rsp)
-  done
+  by (simp add: memb_rsp)
 
 lemma card1_rsp:
   fixes a b :: "'a list"
   assumes e: "a \<approx> b"
   shows "card1 a = card1 b"
-  using e apply induct
-  apply (simp_all add:memb_rsp)
-  done
+  using e by induct (simp_all add:memb_rsp)
 
 lemma ho_card1_rsp: "op \<approx> ===> op = card1 card1"
-  apply (simp add: FUN_REL.simps)
-  apply (metis card1_rsp)
-  done
+  by (simp add: card1_rsp)
 
 lemma cons_rsp:
   fixes z
@@ -234,27 +207,64 @@
 
 lemma ho_cons_rsp:
   "op = ===> op \<approx> ===> op \<approx> op # op #"
-  apply (simp add: FUN_REL.simps)
-  apply (metis cons_rsp)
-  done
+  by (simp add: cons_rsp)
 
 lemma append_rsp_fst:
   assumes a : "list_eq l1 l2"
-  shows "list_eq (l1 @ s) (l2 @ s)"
+  shows "(l1 @ s) \<approx> (l2 @ s)"
   using a
-  apply(induct)
-  apply(auto intro: list_eq.intros)
-  apply(rule list_eq_refl)
-done
+  by (induct) (auto intro: list_eq.intros list_eq_refl)
+
+lemma append_end:
+  shows "(e # l) \<approx> (l @ [e])"
+  apply (induct l)
+  apply (auto intro: list_eq.intros list_eq_refl)
+  done
+
+lemma rev_rsp:
+  shows "a \<approx> rev a"
+  apply (induct a)
+  apply simp
+  apply (rule list_eq_refl)
+  apply simp_all
+  apply (rule list_eq.intros(6))
+  prefer 2
+  apply (rule append_rsp_fst)
+  apply assumption
+  apply (rule append_end)
+  done
 
-(* Need stronger induction... *)
-lemma "(a @ b) \<approx> (b @ a)"
-  apply(induct a)
-  sorry
+lemma append_sym_rsp:
+  shows "(a @ b) \<approx> (b @ a)"
+  apply (rule list_eq.intros(6))
+  apply (rule append_rsp_fst)
+  apply (rule rev_rsp)
+  apply (rule list_eq.intros(6))
+  apply (rule rev_rsp)
+  apply (simp)
+  apply (rule append_rsp_fst)
+  apply (rule list_eq.intros(3))
+  apply (rule rev_rsp)
+  done
+
+lemma append_rsp:
+  assumes a : "list_eq l1 r1"
+  assumes b : "list_eq l2 r2 "
+  shows "(l1 @ l2) \<approx> (r1 @ r2)"
+  apply (rule list_eq.intros(6))
+  apply (rule append_rsp_fst)
+  using a apply (assumption)
+  apply (rule list_eq.intros(6))
+  apply (rule append_sym_rsp)
+  apply (rule list_eq.intros(6))
+  apply (rule append_rsp_fst)
+  using b apply (assumption)
+  apply (rule append_sym_rsp)
+  done
 
 lemma ho_append_rsp:
   "op \<approx> ===> op \<approx> ===> op \<approx> op @ op @"
-sorry
+  by (simp add: append_rsp)
 
 lemma map_rsp:
   assumes a: "a \<approx> b"

--- a/QuotMain.thy	Wed Oct 28 01:49:31 2009 +0100
+++ b/QuotMain.thy	Wed Oct 28 10:17:07 2009 +0100
@@ -810,9 +810,8 @@
     val defs_pre_sym = map symmetric defs
     val defs_atom = map atomize_thm defs_pre_sym
     val defs_all = flat (map (add_lower_defs_aux ctxt) defs_atom)
-    val defs_sym = map (fn t => eq_reflection OF [t]) defs_all
   in
-    map Thm.varifyT defs_sym
+    map Thm.varifyT defs_all
   end
 *}