--- a/FSet.thy	Wed Oct 28 10:17:07 2009 +0100
+++ b/FSet.thy	Wed Oct 28 10:29:00 2009 +0100
@@ -274,23 +274,25 @@
   apply(auto intro: list_eq.intros)
   done
 
+lemma fun_rel_id:
+  "op = ===> op = \<equiv> op ="
+  apply (rule eq_reflection)
+  apply (rule ext)
+  apply (rule ext)
+  apply (simp)
+  apply (auto)
+  apply (rule ext)
+  apply (simp)
+  done
+
 lemma ho_map_rsp:
   "op = ===> op = ===> op \<approx> ===> op \<approx> map map"
-  apply (simp add: FUN_REL.simps)
-  apply (rule allI)
-  apply (rule allI)
-  apply (rule impI)
-  apply (rule allI)
-  apply (rule allI)
-  apply (rule impI)
-  sorry (* apply (auto simp add: map_rsp[of "xa" "ya"]) *)
+  by (simp add: fun_rel_id map_rsp)
 
 lemma map_append :
   "(map f ((a::'a list) @ b)) \<approx>
   ((map f a) ::'a list) @ (map f b)"
- apply simp
- apply (rule list_eq_refl)
- done
+ by simp (rule list_eq_refl)
 
 thm list.induct
 lemma list_induct_hol4:
@@ -531,7 +533,6 @@
 *}
 *)
 
-(* These do not work without proper definitions to rewrite back *)
 local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *}
 local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *}
 local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *}
@@ -554,28 +555,5 @@
   val cv = cterm_of @{theory} ((term_of @{cpat "REP_fset"}) $ v)
 *}
 
-ML {*
-  Toplevel.program (fn () =>
-    MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} (
-      Drule.instantiate' [] [NONE, SOME (cv)] @{thm leqi4_lift}
-    )
-  )
-*}
-
-
-
-(*prove aaa: {* (Thm.term_of cgoal2) *}
-  apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
-  apply (atomize(full))
-  apply (tactic {* transconv_fset_tac' @{context} 1 *})
-  done*)
-
-(*
-datatype obj1 =
-  OVAR1 "string"
-| OBJ1 "(string * (string \<Rightarrow> obj1)) list"
-| INVOKE1 "obj1 \<Rightarrow> string"
-| UPDATE1 "obj1 \<Rightarrow> string \<Rightarrow> (string \<Rightarrow> obj1)"
-*)
 
 end