# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259932280 -3600
# Node ID 7ba2fc25c6a3af6ac8fffe833e4a52fa0b76c8d0
# Parent  3f657c4fbefa27e63c2574af502c4b83f0fd22a6# Parent  c7c6ba5ac043c8ce32818dbae5d2819a91df8278
merge

diff -r c7c6ba5ac043 -r 7ba2fc25c6a3 FIXME-TODO
--- a/FIXME-TODO	Fri Dec 04 13:58:23 2009 +0100
+++ b/FIXME-TODO	Fri Dec 04 14:11:20 2009 +0100
@@ -18,7 +18,7 @@
 
 - Handle theorems that include Ball/Bex
 
-
+- Test theorems with abstractions
 
 
 
diff -r c7c6ba5ac043 -r 7ba2fc25c6a3 FSet.thy
--- a/FSet.thy	Fri Dec 04 13:58:23 2009 +0100
+++ b/FSet.thy	Fri Dec 04 14:11:20 2009 +0100
@@ -299,7 +299,7 @@
 lemma "IN x EMPTY = False"
 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
-apply(tactic {* all_inj_repabs_tac' @{context} [rel_refl] [trans2] 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 apply(tactic {* clean_tac @{context} 1*})
 done
 
@@ -327,7 +327,7 @@
 apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})
 done
 
-ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac' lthy [rel_refl] [trans2] *}
+ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}
 
 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *})
diff -r c7c6ba5ac043 -r 7ba2fc25c6a3 LFex.thy
--- a/LFex.thy	Fri Dec 04 13:58:23 2009 +0100
+++ b/LFex.thy	Fri Dec 04 14:11:20 2009 +0100
@@ -260,7 +260,7 @@
 apply - 
 apply(tactic {* lift_tac @{context} @{thm akind_aty_atrm.induct} @{thms alpha_EQUIVs} 1 *})
 (*apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
-apply(tactic {* all_inj_repabs_tac' @{context} rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *})
 apply(tactic {* clean_tac @{context} 1 *})
 *)
 (*apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *})*)
diff -r c7c6ba5ac043 -r 7ba2fc25c6a3 QuotMain.thy
--- a/QuotMain.thy	Fri Dec 04 13:58:23 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 14:11:20 2009 +0100
@@ -956,73 +956,7 @@
 fun unlam t =
   case t of
     (Abs a) => snd (Term.dest_abs a)
-  | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0)))  *}
-
-
-ML {*
-fun inj_repabs_tac ctxt 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> *)
-    NDT ctxt "1" (resolve_tac trans2 THEN' RANGE [
-      quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]),
-
-    (* (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)]))),
-
-    (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP   provided type of t needs lifting *)
-    NDT ctxt "A" (APPLY_RSP_TAC ctxt THEN'
-                (RANGE [SOLVES' (quotient_tac ctxt), SOLVES' (quotient_tac ctxt),
-                        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 FUN_REL_EQ LIST_REL_EQ})))*)
-    ])
-*}
-
-ML {*
-fun all_inj_repabs_tac ctxt rel_refl trans2 =
-  REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2)
+  | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0)))
 *}
 
 ML {*
@@ -1050,58 +984,71 @@
   | _ => no_tac)
 *}
 
-(* A faster version *)
-
 ML {*
-fun inj_repabs_tac_fast ctxt trans2 = SUBGOAL (fn (goal, i) =>
+fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) =>
 (case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
+    (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
   ((Const (@{const_name FUN_REL}, _) $ _ $ _) $ (Abs _) $ (Abs _))
       => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam
+    (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
 | (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}
+    (* (R1 ===> op =) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Ball\<dots>x) = (Ball\<dots>y) *)
 | (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
+    (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
 | 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}
+    (* (R1 ===> op =) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Bex\<dots>x) = (Bex\<dots>y) *)
 | (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 ="},_) $ _ $ _ => 
+    (* reflexivity of operators arising from Cong_tac *)
     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)])
 | _ $ _ $ _ =>
+    (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
+    (* observe ---> *)
     rep_abs_rsp_tac ctxt
 | _ => error "inj_repabs_tac not a relation"
 ) i)
 *}
 
 ML {*
-fun inj_repabs_tac' ctxt rel_refl trans2 =
+fun inj_repabs_tac ctxt rel_refl trans2 =
   (FIRST' [
-    inj_repabs_tac_fast ctxt trans2,
+    inj_repabs_tac_match ctxt trans2,
+    (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP   provided type of t needs lifting *)
     NDT ctxt "A" (APPLY_RSP1_TAC' ctxt THEN'
                 (RANGE [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),
+    (* resolving with R x y assumptions *)
     NDT ctxt "E" (atac),
+    (* reflexivity of the basic relations *)
+    (* R \<dots> \<dots> *)
     NDT ctxt "D" (resolve_tac rel_refl),
+    (* respectfulness of constants *)
     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 FUN_REL_EQ LIST_REL_EQ})))*)
     ])
 *}
 
 ML {*
-fun all_inj_repabs_tac' ctxt rel_refl trans2 =
-  REPEAT_ALL_NEW (inj_repabs_tac' ctxt rel_refl trans2)
+fun all_inj_repabs_tac ctxt rel_refl trans2 =
+  REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2)
 *}
 
 
@@ -1360,7 +1307,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
 *}