--- a/FIXME-TODO	Fri Dec 04 09:18:46 2009 +0100
+++ b/FIXME-TODO	Fri Dec 04 09:25:27 2009 +0100
@@ -16,6 +16,9 @@
 
 
 
+- Handle theorems that include Ball/Bex
+
+
 
 
 

--- a/LFex.thy	Fri Dec 04 09:18:46 2009 +0100
+++ b/LFex.thy	Fri Dec 04 09:25:27 2009 +0100
@@ -270,7 +270,8 @@
 ML_prf {* PolyML.profiling 1 *}
 ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *}
 *)
-apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac' @{context} rel_refl trans2 1 *})
+(*apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *})*)
 done
 
 (* Does not work:
@@ -297,10 +298,7 @@
   \<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2);
   \<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)\<rbrakk>
   \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm"
-apply(tactic {* procedure_tac @{context} @{thm kind_ty_trm.induct} 1 *})
-apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *})
-apply(tactic {* clean_tac @{context} 1 *})
+apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} @{thms alpha_EQUIVs} 1 *})
 done
 
 print_quotients

--- a/LamEx.thy	Fri Dec 04 09:18:46 2009 +0100
+++ b/LamEx.thy	Fri Dec 04 09:25:27 2009 +0100
@@ -308,7 +308,7 @@
 lemma perm_prs2: "(id ---> option_map ABS_lam) ((id ---> option_map REP_lam) ([b].(s::lam))) = [b].s"
 sorry
 
-lemma real_alpha:
+lemma real_alpha_lift:
   "\<lbrakk>t = [(a, b)] \<bullet> s; a \<sharp> [b].s\<rbrakk> \<Longrightarrow> Lam a t = Lam b s"
 apply (tactic {* procedure_tac @{context} @{thm real_alpha_pre} 1 *})
 prefer 2
@@ -338,6 +338,7 @@
 apply (tactic {* clean_tac @{context} 1 *})
 apply (simp only: perm_prs)
 (*apply (tactic {* regularize_tac @{context} 1 *})*)
+sorry
 
 done
 

--- a/QuotMain.thy	Fri Dec 04 09:18:46 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 09:25:27 2009 +0100
@@ -739,7 +739,6 @@
      resolve_tac (quotient_rules_get ctxt)])
 *}
 
-
 lemma FUN_REL_I:
   assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
   shows "(R1 ===> R2) f g"
@@ -965,14 +964,71 @@
   REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2)
 *}
 
+(* A faster version *)
+
+ML {*
+fun inj_repabs_tac_fast ctxt quot_thms trans2 = SUBGOAL (fn (goal, i) =>
+(case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
+  ((Const (@{const_name FUN_REL}, _) $ _ $ _) $ (Abs _) $ (Abs _))
+      => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam
+| (Const (@{const_name "op ="},_) $
+    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
+      => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
+| (Const (@{const_name FUN_REL}, _) $ _ $ _) $
+    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
+      => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam
+| Const (@{const_name "op ="},_) $
+    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
+      => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
+| (Const (@{const_name FUN_REL}, _) $ _ $ _) $
+    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
+      => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam
+| Const (@{const_name "op ="},_) $ _ $ _ => 
+    rtac @{thm refl} ORELSE'
+    (resolve_tac trans2 THEN' RANGE [
+      quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])
+| _ $ _ $ _ =>
+    instantiate_tac @{thm REP_ABS_RSP} ctxt THEN' RANGE [SOLVES' (quotient_tac ctxt quot_thms)]
+) i)
+*}
+
+ML {*
+fun inj_repabs_tac' ctxt quot_thms rel_refl trans2 =
+  (FIRST' [
+    inj_repabs_tac_fast ctxt quot_thms trans2,
+    NDT ctxt "A" (APPLY_RSP_TAC 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)])),
+    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)])),
+    NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam),
+    NDT ctxt "E" (atac),
+    NDT ctxt "D" (resolve_tac rel_refl),
+    NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt)),
+    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 quot_thms rel_refl trans2 =
+  REPEAT_ALL_NEW (inj_repabs_tac' ctxt quot_thms rel_refl trans2)
+*}
+
+
+
 section {* Cleaning of the theorem *}
 
 
 (* TODO: This is slow *)
+(*
 ML {*
 fun allex_prs_tac ctxt =
   (EqSubst.eqsubst_tac ctxt [0] @{thms all_prs ex_prs}) THEN' (quotient_tac ctxt)
 *}
+*)
 
 ML {*
 fun make_inst lhs t =
@@ -1233,7 +1289,7 @@
        [rtac rule,
         RANGE [rtac rthm',
                regularize_tac lthy rel_eqv,
-               rtac thm THEN' all_inj_repabs_tac lthy rel_refl trans2,
+               rtac thm THEN' all_inj_repabs_tac' lthy rel_refl trans2,
                clean_tac lthy]]
     end) lthy
 *}