--- a/QuotMain.thy Fri Dec 04 12:21:15 2009 +0100
+++ b/QuotMain.thy Fri Dec 04 14:11:03 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
*}