--- a/QuotMain.thy	Fri Nov 27 18:38:44 2009 +0100
+++ b/QuotMain.thy	Sat Nov 28 02:54:24 2009 +0100
@@ -717,7 +717,8 @@
 *)
 
 ML {*
-fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} =>
+fun instantiate_tac thm = 
+  Subgoal.FOCUS (fn {concl, ...} =>
   let
     val pat = Drule.strip_imp_concl (cprop_of thm)
     val insts = Thm.match (pat, concl)
@@ -739,13 +740,17 @@
      CHANGED o (simp_tac (HOL_ss addsimps @{thms id_simps}))])
 *}
 
+lemma FUN_REL_I:
+  assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
+  shows "(R1 ===> R2) f g"
+using a by (simp add: FUN_REL.simps)
+
 ML {*
-fun LAMBDA_RES_TAC ctxt i st =
-  (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
-    (_ $ (_ $ (Abs(_, _, _)) $ (Abs(_, _, _)))) =>
-      (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
-      (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
-  | _ => fn _ => no_tac) i st
+val LAMBDA_RES_TAC =
+  SUBGOAL (fn (goal, i) =>
+    case goal of
+       (_ $ (_ $ (Abs _) $ (Abs _))) => rtac @{thm FUN_REL_I} i
+     | _ => no_tac)
 *}
 
 ML {*
@@ -815,7 +820,7 @@
 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
   (FIRST' [
     resolve_tac trans2,
-    LAMBDA_RES_TAC ctxt,
+    LAMBDA_RES_TAC,
     rtac @{thm RES_FORALL_RSP},
     ball_rsp_tac ctxt,
     rtac @{thm RES_EXISTS_RSP},
@@ -834,6 +839,9 @@
     WEAK_LAMBDA_RES_TAC ctxt,
     CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))
     ])
+
+fun all_r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
+  REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms)
 *}
 
 (*
@@ -841,7 +849,7 @@
 we try:
 
  1) theorems 'trans2' from the appropriate QUOT_TYPE
- 2) remove lambdas from both sides (LAMBDA_RES_TAC)
+ 2) remove lambdas from both sides: LAMBDA_RES_TAC
  3) remove Ball/Bex from the right hand side
  4) use user-supplied RSP theorems
  5) remove rep_abs from the right side
@@ -849,44 +857,96 @@
  7) split applications of lifted type (apply_rsp)
  8) split applications of non-lifted type (cong_tac)
  9) apply extentionality
-10) reflexivity of the relation
-11) assumption
+ A) reflexivity of the relation
+ B) assumption
     (Lambdas under respects may have left us some assumptions)
-12) proving obvious higher order equalities by simplifying fun_rel
+ C) proving obvious higher order equalities by simplifying fun_rel
     (not sure if it is still needed?)
-13) unfolding lambda on one side
-14) simplifying (= ===> =) for simpler respectfulness
+ D) unfolding lambda on one side
+ E) simplifying (= ===> =) for simpler respectfulness
 
 *)
 
 ML {*
 fun r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms =
-  REPEAT_ALL_NEW (FIRST' [
+  (FIRST' [
     (K (print_tac "start")) THEN' (K no_tac), 
+  
+    (* "cong" rule of the of the relation    *)
+    (* \<lbrakk>a \<approx> c; b \<approx> d\<rbrakk> \<Longrightarrow> (a \<approx> b) = (c \<approx> d) *)
     DT ctxt "1" (resolve_tac trans2),
-    DT ctxt "2" (LAMBDA_RES_TAC ctxt),
+
+    (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) 
+    DT ctxt "2" (LAMBDA_RES_TAC),
+
+    (* R (Ball\<dots>) (Ball\<dots>) \<Longrightarrow> R (\<dots>) (\<dots>) *)
     DT ctxt "3" (rtac @{thm RES_FORALL_RSP}),
+
     DT ctxt "4" (ball_rsp_tac ctxt),
     DT ctxt "5" (rtac @{thm RES_EXISTS_RSP}),
     DT ctxt "6" (bex_rsp_tac ctxt),
+
+    (* respectfulness of ops *)
     DT ctxt "7" (resolve_tac rsp_thms),
+
+    (* reflexivity of operators arising from Cong_tac *)
     DT ctxt "8" (rtac @{thm refl}),
+
+    (* R (\<dots>) (Rep (Abs \<dots>)) \<Longrightarrow> R (\<dots>) (\<dots>) *)
+    (* observe ---> *) 
     DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt 
                   THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))),
+
+    (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> APPLY_RSP   provided type of t needs lifting *)
     DT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' 
                 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))),
+
+    (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> Cong provided R = (op =) and t does not need lifting *)
     DT ctxt "B" (Cong_Tac.cong_tac @{thm cong}),
+
+    (* = (\<lambda>x\<dots>) (\<lambda>x\<dots>) \<Longrightarrow> = (\<dots>) (\<dots>) *)
     DT ctxt "C" (rtac @{thm ext}),
+    
+    (* reflexivity of the basic relations *)
     DT ctxt "D" (resolve_tac rel_refl),
+
+    (* resolving with R x y assumptions *)
     DT ctxt "E" (atac),
+
     DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),
     DT ctxt "G" (WEAK_LAMBDA_RES_TAC ctxt),
     DT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))
     ])
+
+fun all_r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms =
+  REPEAT_ALL_NEW (r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms)
 *}
 
+ML {*
+fun get_inj_repabs_tac ctxt rel lhs rhs =
+let
+  val _ = tracing "input"
+  val _ = tracing ("rel: " ^ Syntax.string_of_term ctxt rel)
+  val _ = tracing ("lhs: " ^ Syntax.string_of_term ctxt lhs)
+  val _ = tracing ("rhs: " ^ Syntax.string_of_term ctxt rhs)
+in  
+  case (rel, lhs, rhs) of
+    (_, l, Const _ $ (Const _ $ r)) (* FIXME: not right_match *)
+      => rtac @{thm REP_ABS_RSP(1)}
+  | (_, Const (@{const_name "Ball"}, _) $ _, 
+        Const (@{const_name "Ball"}, _) $ _)
+      => rtac @{thm RES_FORALL_RSP}
+  | _ => K no_tac
+end
+*}
 
-
+ML {* 
+fun inj_repabs_tac ctxt =
+  SUBGOAL (fn (goal, i) =>
+     (case (HOLogic.dest_Trueprop goal) of
+        (rel $ lhs $ rhs) => get_inj_repabs_tac ctxt rel lhs rhs
+      | _ => K no_tac) i)
+*}
 
 section {* Cleaning of the theorem *}