# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260891600 -3600
# Node ID 17d06b5ec197b51c4844b582748a767fe59cc1e8
# Parent  670131bcba4ad8795b3e5bbd76ffe654950d23bf
lambda_prs & solve_quotient_assum cleaned.

diff -r 670131bcba4a -r 17d06b5ec197 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Tue Dec 15 15:38:17 2009 +0100
+++ b/Quot/QuotMain.thy	Tue Dec 15 16:40:00 2009 +0100
@@ -437,13 +437,10 @@
 *}
 
 ML {*
-fun solve_quotient_assums ctxt thm =
-let 
-  val goal = hd (Drule.strip_imp_prems (cprop_of thm)) 
-in
-  thm OF [Goal.prove_internal [] goal (fn _ => quotient_tac ctxt 1)]
-end
-handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing"
+fun solve_quotient_assum ctxt thm =
+  case Seq.pull (quotient_tac ctxt 1 thm) of
+    SOME (t, _) => t
+  | _ => error "solve_quotient_assum failed. Maybe a quotient_thm is missing"
 *}
 
 
@@ -859,9 +856,6 @@
 fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt)
 *}
 
-(* Since the patterns for the lhs are different; there are 2 different make-insts *)
-(* 1: does  ? \<rightarrow> id *)
-(* 2: does  ? \<rightarrow> non-id *)
 ML {* 
 fun mk_abs u i t =
   if incr_boundvars i u aconv t then Bound i
@@ -873,24 +867,27 @@
 
 fun make_inst lhs t =
 let
-  val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
-  val _ $ (Abs (_, _, g)) = t;
-in 
-  (f, Abs ("x", T, mk_abs u 0 g)) 
+  val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
+  val _ $ (Abs (_, _, (_ $ g))) = t;
+in
+  (f, Abs ("x", T, mk_abs u 0 g))
 end
 
-fun make_inst2 lhs t =
+fun make_inst_id lhs t =
 let
-  val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
-  val _ $ (Abs (_, _, (_ $ g))) = t;
-in 
-  (f, Abs ("x", T, mk_abs u 0 g)) 
+  val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
+  val _ $ (Abs (_, _, g)) = t;
+in
+  (f, Abs ("x", T, mk_abs u 0 g))
 end
 *}
 
 ML {*
-(* FIXME / TODO this needs to be clarified *)
-
+(* Simplifies a redex using the 'lambda_prs' theorem. *)
+(* First instantiates the types and known subterms. *)
+(* Then solves the quotient assumptions to get Rep2 and Abs1 *)
+(* Finally instantiates the function f using make_inst *)
+(* If Rep2 is identity then the pattern is simpler and make_inst_id is used *)
 fun lambda_prs_simple_conv ctxt ctrm =
   case (term_of ctrm) of
    (Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) =>
@@ -901,36 +898,11 @@
        val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
        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 ti =
-         (let
-           val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te
-           val (insp, inst) = make_inst (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 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_inst2 (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
-         end)
-       val _ = if not (Term.is_Const a2 andalso fst (dest_Const a2) = @{const_name "id"}) then
-                  (tracing "lambda_prs";
-                   tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm)));
-                   tracing ("lpi rule:\n" ^ (Syntax.string_of_term ctxt (prop_of lpi)));
-                   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 ()
-
+       val te = @{thm eq_reflection} OF [solve_quotient_assum ctxt (solve_quotient_assum ctxt lpi)]
+       val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te
+       val make_inst = if ty_c = ty_d then make_inst_id else make_inst
+       val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm)
+       val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
      in
        Conv.rewr_conv ti ctrm
      end