--- a/FSet.thy	Tue Dec 01 18:22:48 2009 +0100
+++ b/FSet.thy	Tue Dec 01 18:41:01 2009 +0100
@@ -12,12 +12,6 @@
 | "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys"
 | "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3"
 
-lemma
-  "(list_eq ===> (list_eq ===> (op =))) (list_eq) (list_eq)"
-apply(simp add: FUN_REL.simps)
-apply(rule allI | rule impI)+
-sorry
-
 lemma list_eq_refl:
   shows "xs \<approx> xs"
   by (induct xs) (auto intro: list_eq.intros)
@@ -297,6 +291,24 @@
   apply (auto simp add: memb_rsp rsp_fold_def)
 done
 
+lemma list_eq_rsp[quot_rsp]:
+  "(op \<approx> ===> op \<approx> ===> op =) (op \<approx>) (op \<approx>)"
+apply(simp add: FUN_REL.simps)
+apply(auto)
+apply(blast intro: list_eq.intros)
+apply(blast intro: list_eq.intros)
+done
+
+lemma list_eq_rsp2[quot_rsp]:
+  "(op \<approx> ===> op =) (op \<approx>) (op \<approx>)"
+apply(simp add: FUN_REL.simps)
+apply(rule allI)+
+apply(rule impI)
+apply(simp add: expand_fun_eq)
+apply(rule allI)
+apply(blast intro: list_eq.intros)
+done
+
 print_quotients
 
 ML {* val qty = @{typ "'a fset"} *}
@@ -310,6 +322,7 @@
 
 thm m1
 
+
 lemma "IN x EMPTY = False"
 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *})
 apply(tactic {* regularize_tac @{context}  [rel_eqv] 1 *})
@@ -344,6 +357,51 @@
 done
 
 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
+apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
+ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
+apply(tactic {* procedure_tac @{context} @{thm map_append} 1 *})
+apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
+prefer 2
+apply(tactic {* clean_tac @{context} [quot] defs 1 *})
+apply(tactic {* inj_repabs_tac_fset @{context} 1*})
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*})
+ 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*})
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*})
+back 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*})
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
+
 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *})
 done
 

--- a/QuotMain.thy	Tue Dec 01 18:22:48 2009 +0100
+++ b/QuotMain.thy	Tue Dec 01 18:41:01 2009 +0100
@@ -5,6 +5,59 @@
      ("quotient_def.ML")
 begin
 
+thm LAMBDA_PRS
+
+ML {*
+let
+   val parser = Args.context -- Scan.lift Args.name_source
+   fun term_pat (ctxt, str) =
+      str |> ProofContext.read_term_pattern ctxt
+          |> ML_Syntax.print_term
+          |> ML_Syntax.atomic
+in
+   ML_Antiquote.inline "term_pat" (parser >> term_pat)
+end
+*}
+
+ML {*
+fun make_inst lhs t =
+  let
+    val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
+    val _ $ (Abs (_, _, g)) = t;
+    fun mk_abs i t =
+      if incr_boundvars i u aconv t then Bound i
+      else (case t of
+        t1 $ t2 => mk_abs i t1 $ mk_abs i t2
+      | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t')
+      | Bound j => if i = j then error "make_inst" else t
+      | _ => t);
+  in (f, Abs ("x", T, mk_abs 0 g)) end;
+*}
+
+ML {* 
+  val trm1 = @{term_pat "(P::(nat\<Rightarrow>bool)\<Rightarrow>bool) (\<lambda>(x::nat). (?f ((g::nat\<Rightarrow>nat) x)))"}; 
+  val trm2 = @{term_pat "(P::(nat\<Rightarrow>bool)\<Rightarrow>bool) (\<lambda>(x::nat). (h (g x) ((g::nat\<Rightarrow>nat) x)))"}
+*}
+
+ML {*
+fun test trm =
+  case trm of
+  (_ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u))) => (1,f)
+  | (_ $ (Abs (_, _, (f as (Var (_, _)) $ u)))) => (2,f)
+  | (_ $ (Abs (_, _, (f $ u)))) => (3,f)
+*}
+
+ML {* test trm1 *}
+
+ML {*
+ make_inst trm1 trm2
+  |> pairself (Syntax.string_of_term @{context})
+  |> pairself writeln
+*}
+
+
+
+
 locale QUOT_TYPE =
   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"