# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260283349 -3600
# Node ID e26e3dac3bf0198c9d9ad229c162cdd828eafeb9
# Parent  7a6aead83647d0d1b66c590a017d527cef618b22
make_inst3

diff -r 7a6aead83647 -r e26e3dac3bf0 Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Tue Dec 08 15:12:55 2009 +0100
+++ b/Quot/Examples/FSet.thy	Tue Dec 08 15:42:29 2009 +0100
@@ -437,9 +437,7 @@
 defer
 apply(tactic {* all_inj_repabs_tac @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
-thm lambda_prs[OF identity_quotient Quotient_fset]
-thm lambda_prs[OF identity_quotient Quotient_fset, simplified]
-apply(simp only: lambda_prs[OF identity_quotient Quotient_fset,simplified])
+apply(tactic {* clean_tac @{context} 1 *}) (* TODO: needs lambda_prs twice *)
 sorry
 
 lemma ttt3: "(\<lambda>x. ((op @) x ((op #) e []))) = (\<lambda>x. ((op #) e x))"
diff -r 7a6aead83647 -r e26e3dac3bf0 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Tue Dec 08 15:12:55 2009 +0100
+++ b/Quot/QuotMain.thy	Tue Dec 08 15:42:29 2009 +0100
@@ -940,6 +940,10 @@
 
 section {* Cleaning of the Theorem *}
 
+(* Since the patterns for the lhs are different; there are 3 different make-insts *)
+(* 1: does  ? \<rightarrow> id *)
+(* 2: does id \<rightarrow> ? *)
+(* 3: does  ? \<rightarrow> ? *)
 ML {*
 fun make_inst lhs t =
   let
@@ -955,12 +959,25 @@
   in (f, Abs ("x", T, mk_abs 0 g)) end;
 *}
 
-(* Since the patterns for the lhs are different; there are 2 different make-insts *)
 ML {*
 fun make_inst2 lhs t =
   let
     val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
-    val _ = tracing "a";
+    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 {*
+fun make_inst3 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
@@ -984,7 +1001,6 @@
        val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
        val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs}
        val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)]
-       val _ = tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te)));
        val ti =
          (let
            val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te
@@ -993,7 +1009,15 @@
            Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
          end handle _ => (* TODO handle only Bind | Error "make_inst" *)
          let
-           val (insp, inst) = make_inst2 (term_of (Thm.lhs_of te)) (term_of ctrm)
+           val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te
+           val _ = tracing ("ts rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ts)));
+           val _ = tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm)));
+           val (insp, inst) = make_inst2 (term_of (Thm.lhs_of ts)) (term_of ctrm)
+         in
+           Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
+         end handle _ => (* TODO handle only Bind | Error "make_inst" *)
+         let
+           val (insp, inst) = make_inst3 (term_of (Thm.lhs_of te)) (term_of ctrm)
            val td = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) te
          in
            MetaSimplifier.rewrite_rule (id_simps_get ctxt) td
@@ -1005,6 +1029,7 @@
                    tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te)));
                    tracing ("ti rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti))))
                else ()
+
      in
        Conv.rewr_conv ti ctrm
      end