--- a/FSet.thy	Tue Nov 24 19:09:29 2009 +0100
+++ b/FSet.thy	Tue Nov 24 20:13:16 2009 +0100
@@ -355,9 +355,15 @@
           (quotient_tac quot);
         val gc = Drule.strip_imp_concl (cprop_of lpi);
         val t = Goal.prove_internal [] gc (fn _ => tac 1)
-        val _ = tracing (Syntax.string_of_term @{context} (prop_of t))
+        val ts = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t
+        val te = @{thm eq_reflection} OF [ts]
+        val _ = tracing (Syntax.string_of_term @{context} (term_of ctrm));
+        val _ = tracing (Syntax.string_of_term @{context} (term_of (Thm.lhs_of te)));
+        val insts = matching_prs (ProofContext.theory_of ctxt) (term_of ctrm) (term_of (Thm.lhs_of te));
+        val ti = Drule.instantiate insts te;
+        val _ = tracing (Syntax.string_of_term @{context} (term_of (cprop_of ti)));
       in
-        Conv.rewr_conv (eq_reflection OF [t]) ctrm
+        Conv.rewr_conv (eq_reflection OF [ti]) ctrm
       end
   | _ $ _ => Conv.comb_conv (lambda_prs_conv ctxt quot) ctrm
   | Abs _ => Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt ctrm
@@ -365,10 +371,6 @@
 *}
 
 ML {*
-  lambda_prs_conv @{context} quot
-*}
-
-ML {*
 fun lambda_prs_tac ctxt quot = CSUBGOAL (fn (goal, i) =>
   CONVERSION
     (Conv.params_conv ~1 (fn ctxt =>
@@ -377,31 +379,52 @@
 *}
 
 ML {*
-lambda_prs_conv @{context} quot 
-@{cterm "((ABS_fset ---> id) ---> id) (\<lambda>x\<Colon>'a list \<Rightarrow> bool. id ((f ((REP_fset ---> id) x) ((REP_fset ---> id) x))))"}
+val ctrm = @{cterm "((ABS_fset ---> id) ---> id) (\<lambda>x. id ((REP_fset ---> id) x))"}
+val pat =  @{cpat  "((ABS_fset ---> id) ---> id) (\<lambda>x. ?f ((REP_fset ---> id) x))"}
 *}
 
+ML {* matching_prs @{theory} (term_of pat) (term_of ctrm); *}
+
 ML {*
-@{cterm "((ABS_fset ---> id) ---> id)
-          (\<lambda>P.
-              All ((REP_fset ---> id)
-                    (\<lambda>list.
+  lambda_prs_conv @{context} quot ctrm
+*}
+
+
+ML {* 
+val t = @{thm LAMBDA_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT] IDENTITY_QUOTIENT]}
+val te = @{thm eq_reflection} OF [t]
+val ts = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] te
+val tl = Thm.lhs_of ts
+ *}
+
+ML {* val inst = matching_prs @{theory} (term_of tl) (term_of ctrm); *}
+
+ML {* val trm = @{cterm "(((ABS_fset ---> id) ---> id) (\<lambda>(P\<Colon>('a list \<Rightarrow> bool)).
+              All ((REP_fset ---> id) (\<lambda>(list\<Colon>('a list)).
                         (ABS_fset ---> id) ((REP_fset ---> id) P) (REP_fset (ABS_fset [])) \<longrightarrow>
-                        (\<forall>a. All ((REP_fset ---> id)
-                                      (\<lambda>list.
-                                          (ABS_fset ---> id) ((REP_fset ---> id) P) (REP_fset (ABS_fset list)) \<longrightarrow>
-                                          (ABS_fset ---> id) ((REP_fset ---> id) P)
-                                           (REP_fset (ABS_fset (a # REP_fset (ABS_fset list))))))) \<longrightarrow>
-                        (ABS_fset ---> id) ((REP_fset ---> id) P) (REP_fset (ABS_fset list)))))"}
+               True \<longrightarrow> (ABS_fset ---> id) ((REP_fset ---> id) P) (REP_fset (ABS_fset list))))))"} *}
 
+ML {*
+  lambda_prs_conv @{context} quot trm
 *}
 
 
+
+(*ML {* val trm = @{cterm "(((ABS_fset ---> id) ---> id) (\<lambda>(?P\<Colon>('a list \<Rightarrow> bool)). (g (id P)"} *} *)
+
+
+
 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
 apply(tactic {* procedure_tac @{thm list.induct} @{context} 1 *})
 apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *})
 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *})
 apply(tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *})
+apply(tactic {* lambda_prs_tac @{context} quot 1 *})
+
+
+ML_prf {* Subgoal.focus @{context} 1 (#goal (Isar.goal ())) *}
+
+apply (tactic {* lift_tac_fset @{context} @{thm list.induct} 1 *})
 
 
 thm LAMBDA_PRS
@@ -438,7 +461,7 @@
     (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"} *}*)
 
 
-
+*)
 ML {* lift_thm_g_fset @{context} @{thm map_append} @{term "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"} *}
 
 
@@ -448,7 +471,7 @@
 ML {* lift_thm_fset @{context} @{thm map_append} *}
 
 
-
+(*
 apply(tactic {* procedure_tac @{thm m1} @{context} 1 *})
 apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *})
 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *})
@@ -458,7 +481,7 @@
 ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *}
 apply(tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1*})
 apply(tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
-
+*)