# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259383398 -3600
# Node ID 1c245f6911ddae9b97aa475c5d449983f24786c2
# Parent  9c33c0809733f8eb40c947fc3e6e51658de44cb4# Parent  5b298c42f6c8cdfa016e1e632416a7361c8fb529
Merged and tested that all works.

diff -r 9c33c0809733 -r 1c245f6911dd FSet.thy
--- a/FSet.thy	Sat Nov 28 05:29:30 2009 +0100
+++ b/FSet.thy	Sat Nov 28 05:43:18 2009 +0100
@@ -307,8 +307,7 @@
 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] rsp_thms defs *}
 
 lemma "IN x EMPTY = False"
-apply (tactic {* lift_tac_fset @{context} @{thm m1} 1 *})
-done
+by (tactic {* lift_tac_fset @{context} @{thm m1} 1 *})
 
 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)"
 by (tactic {* lift_tac_fset @{context} @{thm m2} 1 *})
diff -r 9c33c0809733 -r 1c245f6911dd IntEx.thy
--- a/IntEx.thy	Sat Nov 28 05:29:30 2009 +0100
+++ b/IntEx.thy	Sat Nov 28 05:43:18 2009 +0100
@@ -147,8 +147,6 @@
 ML {* fun all_r_mk_comb_tac_intex lthy = all_r_mk_comb_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
 
 
-lemma cheat: "P" sorry
-
 lemma "PLUS a b = PLUS b a"
 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
@@ -178,7 +176,7 @@
 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
-apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
 done
 
 lemma plus_assoc_pre:
@@ -236,49 +234,3 @@
 done
 
 
-(*
-
-ML {*
-fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
-  (REPEAT1 o FIRST1) 
-    [(K (print_tac "start")) THEN' (K no_tac), 
-     DT ctxt "1" (rtac trans_thm),
-     DT ctxt "2" (LAMBDA_RES_TAC ctxt),
-     DT ctxt "3" (ball_rsp_tac ctxt),
-     DT ctxt "4" (bex_rsp_tac ctxt),
-     DT ctxt "5" (FIRST' (map rtac rsp_thms)),
-     DT ctxt "6" (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
-     DT ctxt "7" (rtac refl),
-     DT ctxt "8" (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
-     DT ctxt "9" (Cong_Tac.cong_tac @{thm cong}),
-     DT ctxt "A" (rtac @{thm ext}),
-     DT ctxt "B" (rtac reflex_thm),
-     DT ctxt "C" (atac),
-     DT ctxt "D" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),
-     DT ctxt "E" (WEAK_LAMBDA_RES_TAC ctxt),
-     DT ctxt "F" (CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))]
-*}
-
-ML {* 
-inj_repabs_trm @{context} (reg_atrm, aqtrm) 
-  |> Syntax.check_term @{context}
-*}
-
-
-ML {* val my_goal = cterm_of @{theory} (mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm)) *}
-ML {* val yr_goal = cterm_of @{theory} (build_repabs_goal @{context} (@{thm testtest} OF [arthm]) consts rty qty) *}
-
-prove {* mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) *}
-apply(tactic {* ObjectLogic.full_atomize_tac 1 *})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *})
-done
-
-ML {*
-inj_repabs_trm @{context} (reg_atrm, aqtrm)  
-|> Syntax.string_of_term @{context}
-|> writeln
-*}
-
-*)
-
-
diff -r 9c33c0809733 -r 1c245f6911dd QuotMain.thy
--- a/QuotMain.thy	Sat Nov 28 05:29:30 2009 +0100
+++ b/QuotMain.thy	Sat Nov 28 05:43:18 2009 +0100
@@ -812,22 +812,19 @@
 
 ML {*
 val LAMBDA_RES_TAC =
-  SUBGOAL (fn (goal, i) =>
-    case goal of
-       (_ $ (_ $ (Abs _) $ (Abs _))) => rtac @{thm FUN_REL_I} i
+  Subgoal.FOCUS (fn {concl, ...} =>
+    case (term_of concl) of
+       (_ $ (_ $ (Abs _) $ (Abs _))) => rtac @{thm FUN_REL_I} 1
      | _ => no_tac)
 *}
 
 ML {*
-fun WEAK_LAMBDA_RES_TAC ctxt i st =
-  (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
-    (_ $ (_ $ _ $ (Abs(_, _, _)))) =>
-      (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
-      (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
-  | (_ $ (_ $ (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 WEAK_LAMBDA_RES_TAC =
+  Subgoal.FOCUS (fn {concl, ...} =>
+    case (term_of concl) of
+       (_ $ (_ $ _ $ (Abs _))) => rtac @{thm FUN_REL_I} 1
+     | (_ $ (_ $ (Abs _) $ _)) => rtac @{thm FUN_REL_I} 1
+     | _ => no_tac)
 *}
 
 ML {* (* Legacy *)
@@ -839,48 +836,44 @@
 
 *}
 
-(* Doesn't work *)
 ML {*
-fun APPLY_RSP_TAC rty = Subgoal.FOCUS (fn {concl, ...} =>
-  let
-    val (_ $ (R $ (f $ _) $ (_ $ _))) = term_of concl;
-    val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP});
-    val insts = Thm.match (pat, concl)
-  in
-    if needs_lift rty (type_of f) then rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1
-    else no_tac
-  end
-  handle _ => no_tac)
-*}
-
-
-
-ML {*
-val ball_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
-  let
-    val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $
-                 (Const (@{const_name Ball}, _) $ _)) = term_of concl
-  in
-    ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
-    THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
-    THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN'
-    (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
-  end
-  handle _ => no_tac)
+fun APPLY_RSP_TAC rty = 
+  Subgoal.FOCUS (fn {concl, ...} =>
+    case (term_of concl) of
+       (_ $ (R $ (f $ _) $ (_ $ _))) =>
+          let
+            val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP});
+            val insts = Thm.match (pat, concl)
+          in
+            if needs_lift rty (fastype_of f) 
+            then rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1
+            else no_tac
+          end
+     | _ => no_tac)
 *}
 
 ML {*
-val bex_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
-  let
-    val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $
-                 (Const (@{const_name Bex}, _) $ _)) = term_of concl
-  in
-    ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
-    THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
-    THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN'
-    (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
-  end
-  handle _ => no_tac)
+val ball_rsp_tac = 
+  Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
+     case (term_of concl) of
+        (_ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _))) =>
+            ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
+            THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
+            THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN'
+            (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
+      |_ => no_tac)
+*}
+
+ML {*
+val bex_rsp_tac = 
+  Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
+     case (term_of concl) of
+        (_ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _))) =>
+            ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
+            THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
+            THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN'
+            (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
+      | _ => no_tac)
 *}
 
 ML {*
@@ -890,16 +883,16 @@
 ML {*
 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
   (FIRST' [resolve_tac trans2,
-           LAMBDA_RES_TAC,
+           LAMBDA_RES_TAC ctxt,
            rtac @{thm RES_FORALL_RSP},
            ball_rsp_tac ctxt,
            rtac @{thm RES_EXISTS_RSP},
            bex_rsp_tac ctxt,
            resolve_tac rsp_thms,
            rtac @{thm refl},
-           (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN'
+           (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' 
               (RANGE [SOLVES' (quotient_tac quot_thms)])),
-           (APPLY_RSP_TAC rty ctxt THEN'
+           (APPLY_RSP_TAC rty ctxt THEN' 
               (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)])),
            Cong_Tac.cong_tac @{thm cong},
            rtac @{thm ext},
@@ -946,7 +939,7 @@
     DT ctxt "1" (resolve_tac trans2),
 
     (* (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),
+    DT ctxt "2" (LAMBDA_RES_TAC ctxt),
 
     (* R (Ball\<dots>) (Ball\<dots>) \<Longrightarrow> R (\<dots>) (\<dots>) *)
     DT ctxt "3" (rtac @{thm RES_FORALL_RSP}),
@@ -963,11 +956,11 @@
 
     (* R (\<dots>) (Rep (Abs \<dots>)) \<Longrightarrow> R (\<dots>) (\<dots>) *)
     (* observe ---> *) 
-    DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt
+    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'
+    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 *)