--- a/Quot/QuotMain.thy Tue Dec 08 16:35:40 2009 +0100
+++ b/Quot/QuotMain.thy Tue Dec 08 16:36:01 2009 +0100
@@ -810,6 +810,18 @@
*}
ML {*
+fun equals_rsp_tac R ctxt =
+ let
+ val t = domain_type (fastype_of R);
+ val thy = ProofContext.theory_of ctxt
+ val thm = Drule.instantiate' [SOME (ctyp_of thy t)] [SOME (cterm_of thy R)] @{thm equals_rsp}
+ in
+ rtac thm THEN' RANGE [quotient_tac ctxt]
+ end
+ handle THM _ => K no_tac | TYPE _ => K no_tac | TERM _ => K no_tac
+*}
+
+ML {*
fun rep_abs_rsp_tac ctxt =
SUBGOAL (fn (goal, i) =>
case (bare_concl goal) of
@@ -829,7 +841,7 @@
*}
ML {*
-fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) =>
+fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) =>
(case (bare_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 _))
@@ -864,11 +876,12 @@
(Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
=> rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]
+| Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) => (rtac @{thm refl} ORELSE'
+ (equals_rsp_tac R ctxt THEN' RANGE [
+ quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]))
+
(* reflexivity of operators arising from Cong_tac *)
-| 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)])*)
+| Const (@{const_name "op ="},_) $ _ $ _ => rtac @{thm refl}
(* respectfulness of constants; in particular of a simple relation *)
| _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *)
@@ -884,17 +897,13 @@
*}
ML {*
-fun inj_repabs_step_tac ctxt rel_refl trans2 =
+fun inj_repabs_step_tac ctxt rel_refl =
(FIRST' [
- NDT ctxt "0" (inj_repabs_tac_match ctxt trans2),
+ NDT ctxt "0" (inj_repabs_tac_match ctxt),
(* R (t $ \<dots>) (t' $ \<dots>) ----> apply_rsp provided type of t needs lifting *)
NDT ctxt "A" (apply_rsp_tac ctxt THEN'
RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)]),
-
- (* TODO/FIXME: I had to move this after the apply_rsp_tac - is this right *)
- NDT ctxt "B" (resolve_tac trans2 THEN'
- RANGE [quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]),
(* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *)
(* merge with previous tactic *)
@@ -917,9 +926,8 @@
fun inj_repabs_tac ctxt =
let
val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt)
- val trans2 = map (OF1 @{thm equals_rsp}) (quotient_rules_get ctxt)
in
- inj_repabs_step_tac ctxt rel_refl trans2
+ inj_repabs_step_tac ctxt rel_refl
end
fun all_inj_repabs_tac ctxt =
@@ -928,6 +936,10 @@
section {* Cleaning of the Theorem *}
+(* Since the patterns for the lhs are different; there are 3 different make-insts *)
+(* 1: does ? \<rightarrow> id *)
+(* 2: does id \<rightarrow> ? *)
+(* 3: does ? \<rightarrow> ? *)
ML {*
fun make_inst lhs t =
let
@@ -943,12 +955,25 @@
in (f, Abs ("x", T, mk_abs 0 g)) end;
*}
-(* Since the patterns for the lhs are different; there are 2 different make-insts *)
ML {*
fun make_inst2 lhs t =
let
val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
- val _ = tracing "a";
+ val _ $ (Abs (_, _, (_ $ g))) = t;
+ fun mk_abs i t =
+ if incr_boundvars i u aconv t then Bound i
+ else (case t of
+ t1 $ t2 => mk_abs i t1 $ mk_abs i t2
+ | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t')
+ | Bound j => if i = j then error "make_inst" else t
+ | _ => t);
+ in (f, Abs ("x", T, mk_abs 0 g)) end;
+*}
+
+ML {*
+fun make_inst3 lhs t =
+ let
+ val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
val _ $ (Abs (_, _, (_ $ g))) = t;
fun mk_abs i t =
if incr_boundvars i u aconv t then Bound i
@@ -972,7 +997,6 @@
val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs}
val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)]
- val _ = tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te)));
val ti =
(let
val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te
@@ -981,7 +1005,15 @@
Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
end handle _ => (* TODO handle only Bind | Error "make_inst" *)
let
- val (insp, inst) = make_inst2 (term_of (Thm.lhs_of te)) (term_of ctrm)
+ val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te
+ val _ = tracing ("ts rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ts)));
+ val _ = tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm)));
+ val (insp, inst) = make_inst2 (term_of (Thm.lhs_of ts)) (term_of ctrm)
+ in
+ Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
+ end handle _ => (* TODO handle only Bind | Error "make_inst" *)
+ let
+ val (insp, inst) = make_inst3 (term_of (Thm.lhs_of te)) (term_of ctrm)
val td = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) te
in
MetaSimplifier.rewrite_rule (id_simps_get ctxt) td
@@ -993,6 +1025,7 @@
tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te)));
tracing ("ti rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti))))
else ()
+
in
Conv.rewr_conv ti ctrm
end