
diff -r 1eeacabe5ffe -r 325d6e9a7515 QuotMain.thy
--- a/QuotMain.thy	Tue Dec 01 19:18:43 2009 +0100
+++ b/QuotMain.thy	Wed Dec 02 07:21:10 2009 +0100
@@ -798,7 +798,7 @@
 using a by simp
 
 ML {*
-val lambda_res_tac =
+val lambda_rsp_tac =
   SUBGOAL (fn (goal, i) =>
     case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
        (_ $ (Abs _) $ (Abs _)) => rtac @{thm FUN_REL_I} i
@@ -806,7 +806,7 @@
 *}
 
 ML {*
-val weak_lambda_res_tac =
+val weak_lambda_rsp_tac =
   SUBGOAL (fn (goal, i) =>
     case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
        (_ $ _ $ (Abs _)) => rtac @{thm FUN_REL_I} i
@@ -868,7 +868,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_rsp_tac
  3) remove Ball/Bex from the right hand side
  4) use user-supplied RSP theorems
  5) remove rep_abs from the right side
@@ -891,22 +891,23 @@
 
 lemma quot_true_dests:
   shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P"
-  and   QT_appL: "QUOT_TRUE (A B) \<Longrightarrow> QUOT_TRUE A"
-  and   QT_appR: "QUOT_TRUE (A B) \<Longrightarrow> QUOT_TRUE B"
+  and   QT_ex:  "QUOT_TRUE (Ex P) \<Longrightarrow> QUOT_TRUE P"
   and   QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE  (P x))"
-apply(simp_all add: QUOT_TRUE_def)
+  and   QT_ext: "(\<And>x. QUOT_TRUE (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (QUOT_TRUE a \<Longrightarrow> f = g)"
+apply(simp_all add: QUOT_TRUE_def ext)
 done
 
-lemma QUOT_TRUE_i: "(QUOT_TRUE a \<Longrightarrow> P) \<Longrightarrow> P"
+lemma QUOT_TRUE_i: "(QUOT_TRUE (a :: bool) \<Longrightarrow> P) \<Longrightarrow> P"
 by (simp add: QUOT_TRUE_def)
 
-lemma QUOT_TRUE_imp: "QUOT_TRUE a \<Longrightarrow> QUOT_TRUE b"
+lemma QUOT_TRUE_imp: "QUOT_TRUE a"
 by (simp add: QUOT_TRUE_def)
 
 ML {*
 fun quot_true_tac ctxt fnctn =
-  SUBGOAL (fn (gl, i) =>
+  CSUBGOAL (fn (cgl, i) =>
   let
+    val gl = term_of cgl;
     val thy = ProofContext.theory_of ctxt;
     fun find_fun trm =
       case trm of
@@ -916,20 +917,27 @@
     case find_first find_fun (Logic.strip_assums_hyp gl) of
       SOME (_ $ (_ $ x)) =>
         let
+          val thm' = Thm.lift_rule cgl @{thm QUOT_TRUE_imp}
+          val ps = Logic.strip_params (Thm.concl_of thm');
           val fx = fnctn x;
-          val ctrm1 = cterm_of thy x;
-          val cty1 = ctyp_of thy (fastype_of x);
-          val ctrm2 = cterm_of thy fx;
-          val cty2 = ctyp_of thy (fastype_of fx);
-          val thm = Drule.instantiate' [SOME cty1, SOME cty2] [SOME ctrm1, SOME ctrm2] @{thm QUOT_TRUE_imp}
+          val (_ $ (_ $ fx')) = Logic.strip_assums_concl (prop_of thm');
+            val insts = [(fx', fx)]
+            |> map (fn (t, u) => (cterm_of thy (Term.head_of t), cterm_of thy (Term.list_abs (ps, u))));
+          val thm_i = Drule.cterm_instantiate insts thm'
+          val thm_j = Thm.forall_elim_vars 1 thm_i
         in
-          dtac thm i
+          dtac thm_j i
         end
     | NONE => error "quot_true_tac!"
     | _ => error "quot_true_tac!!"
   end)
 *}
 
+
+ML {* fun dest_comb (f $ a) = (f, a) *}
+ML {* fun dest_bcomb ((_ $ l) $ r) = (l, r) *}
+ML {* fun unlam (Abs a) = snd (Term.dest_abs a) *}
+
 ML {*
 fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 =
   (FIRST' [
@@ -938,7 +946,7 @@
     DT ctxt "1" (resolve_tac trans2),
 
     (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) 
-    NDT ctxt "2" (lambda_res_tac),
+    NDT ctxt "2" (lambda_rsp_tac),
 
     (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
     NDT ctxt "3" (rtac @{thm ball_rsp}),
@@ -987,11 +995,69 @@
 *}
 
 ML {*
+fun inj_repabs_tac' ctxt rty quot_thms rel_refl trans2 =
+  (FIRST' [
+    (* "cong" rule of the of the relation / transitivity*)
+    (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *)
+    DT ctxt "1" (resolve_tac trans2),
+
+    (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
+    NDT ctxt "2" (lambda_rsp_tac THEN' quot_true_tac ctxt unlam),
+
+    (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
+    NDT ctxt "3" (rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}),
+
+    (* R2 is always equality *)
+    (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *)
+    NDT ctxt "4" (ball_rsp_tac THEN' quot_true_tac ctxt unlam),
+
+    (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
+    NDT ctxt "5" (rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}),
+
+    (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *)
+    NDT ctxt "6" (bex_rsp_tac THEN' dtac @{thm QT_ext}),
+
+    (* respectfulness of constants *)
+    NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt)),
+
+    (* reflexivity of operators arising from Cong_tac *)
+    NDT ctxt "8" (rtac @{thm refl}),
+
+    (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
+    (* observe ---> *) 
+    NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP} ctxt 
+                  THEN' (RANGE [SOLVES' (quotient_tac ctxt quot_thms)]))),
+
+    (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP   provided type of t needs lifting *)
+    NDT ctxt "A" (APPLY_RSP_TAC rty ctxt THEN' 
+                (RANGE [SOLVES' (quotient_tac ctxt quot_thms), SOLVES' (quotient_tac ctxt quot_thms),
+                        quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
+
+    (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong   provided type of t does not need lifting *)
+    (* merge with previous tactic *)
+    NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN'
+                (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
+
+    (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
+    NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam),
+    
+    (* reflexivity of the basic relations *)
+    (* R \<dots> \<dots> *)
+    NDT ctxt "D" (resolve_tac rel_refl),
+
+    (* resolving with R x y assumptions *)
+    NDT ctxt "E" (atac),
+
+    (* (op =) ===> (op =)  \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *)
+    (* global simplification *)
+    NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))])
+*}
+
+ML {*
 fun all_inj_repabs_tac ctxt rty quot_thms rel_refl trans2 =
   REPEAT_ALL_NEW (inj_repabs_tac ctxt rty quot_thms rel_refl trans2)
 *}
 
-
 section {* Cleaning of the theorem *}
 
 
@@ -1206,14 +1272,12 @@
     let
       val rthm' = atomize_thm rthm
       val rule = procedure_inst context (prop_of rthm') (term_of concl)
+      val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb concl))] @{thm QUOT_TRUE_i}
     in
-      EVERY1 [rtac rule, rtac rthm']
+      EVERY1 [rtac rule, rtac rthm'] THEN RANGE [(fn _ => all_tac), rtac thm] 1
     end) lthy
 *}
 
-thm EQUIV_REFL
-thm equiv_trans2
-
 ML {*
 (* FIXME/TODO should only get as arguments the rthm like procedure_tac *)
 fun lift_tac lthy rthm rel_eqv rty quot defs =
@@ -1225,12 +1289,13 @@
       val rule = procedure_inst context (prop_of rthm') (term_of concl)
       val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv
       val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) rel_eqv
+      val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb concl))] @{thm QUOT_TRUE_i}
     in
       EVERY1
        [rtac rule,
         RANGE [rtac rthm',
                regularize_tac lthy rel_eqv,
-               all_inj_repabs_tac lthy rty quot rel_refl trans2,
+               rtac thm THEN' all_inj_repabs_tac lthy rty quot rel_refl trans2,
                clean_tac lthy quot defs]]
     end) lthy
 *}




