6 Martin Coen's tactic for substitution in the hypotheses |
6 Martin Coen's tactic for substitution in the hypotheses |
7 *) |
7 *) |
8 |
8 |
9 signature HYPSUBST_DATA = |
9 signature HYPSUBST_DATA = |
10 sig |
10 sig |
11 val dest_eq: term -> term*term |
11 val dest_eq : term -> term*term |
12 val imp_intr: thm (* (P ==> Q) ==> P-->Q *) |
12 val imp_intr : thm (* (P ==> Q) ==> P-->Q *) |
13 val rev_cut_eq: thm (* [| a=b; a=b ==> R |] ==> R *) |
13 val rev_mp : thm (* [| P; P-->Q |] ==> Q *) |
14 val rev_mp: thm (* [| P; P-->Q |] ==> Q *) |
14 val subst : thm (* [| a=b; P(a) |] ==> P(b) *) |
15 val subst: thm (* [| a=b; P(a) |] ==> P(b) *) |
15 val sym : thm (* a=b ==> b=a *) |
16 val sym: thm (* a=b ==> b=a *) |
|
17 end; |
16 end; |
18 |
17 |
19 signature HYPSUBST = |
18 signature HYPSUBST = |
20 sig |
19 sig |
21 val bound_hyp_subst_tac : int -> tactic |
20 val bound_hyp_subst_tac : int -> tactic |
22 val hyp_subst_tac : int -> tactic |
21 val hyp_subst_tac : int -> tactic |
23 (*exported purely for debugging purposes*) |
22 (*exported purely for debugging purposes*) |
24 val eq_var : bool -> term -> term * thm |
23 val eq_var : bool -> term -> int * thm |
25 val inspect_pair : bool -> term * term -> term * thm |
24 val inspect_pair : bool -> term * term -> thm |
26 val liftvar : int -> typ list -> term |
|
27 end; |
25 end; |
28 |
26 |
29 functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST = |
27 functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST = |
30 struct |
28 struct |
31 |
29 |
32 local open Data in |
30 local open Data in |
33 |
31 |
34 fun REPEATN 0 tac = all_tac |
32 fun REPEATN 0 tac = all_tac |
35 | REPEATN n tac = Tactic(fn state => |
33 | REPEATN n tac = Tactic(fn state => |
36 tapply(tac THEN REPEATN (n-1) tac, state)); |
34 tapply(tac THEN REPEATN (n-1) tac, state)); |
37 |
|
38 local |
|
39 val T = case #1 (types_sorts rev_cut_eq) ("a",0) of |
|
40 Some T => T |
|
41 | None => error"No such variable in rev_cut_eq" |
|
42 in |
|
43 fun liftvar inc paramTs = Var(("a",inc), paramTs ---> incr_tvar inc T); |
|
44 end; |
|
45 |
35 |
46 exception EQ_VAR; |
36 exception EQ_VAR; |
47 |
37 |
48 fun loose (i,t) = 0 mem add_loose_bnos(t,i,[]); |
38 fun loose (i,t) = 0 mem add_loose_bnos(t,i,[]); |
49 |
39 |
53 It's not safe to substitute for a variable free in the premises, |
43 It's not safe to substitute for a variable free in the premises, |
54 but how could we check for this?*) |
44 but how could we check for this?*) |
55 fun inspect_pair bnd (t,u) = |
45 fun inspect_pair bnd (t,u) = |
56 case (Pattern.eta_contract t, Pattern.eta_contract u) of |
46 case (Pattern.eta_contract t, Pattern.eta_contract u) of |
57 (Bound i, _) => if loose(i,u) then raise Match |
47 (Bound i, _) => if loose(i,u) then raise Match |
58 else (t, asm_rl) |
48 else sym (*eliminates t*) |
59 | (_, Bound i) => if loose(i,t) then raise Match |
49 | (_, Bound i) => if loose(i,t) then raise Match |
60 else (u, sym) |
50 else asm_rl (*eliminates u*) |
61 | (Free _, _) => if bnd orelse Logic.occs(t,u) then raise Match |
51 | (Free _, _) => if bnd orelse Logic.occs(t,u) then raise Match |
62 else (t, asm_rl) |
52 else sym (*eliminates t*) |
63 | (_, Free _) => if bnd orelse Logic.occs(u,t) then raise Match |
53 | (_, Free _) => if bnd orelse Logic.occs(u,t) then raise Match |
64 else (u, sym) |
54 else asm_rl (*eliminates u*) |
65 | _ => raise Match; |
55 | _ => raise Match; |
66 |
56 |
67 (* Extracts the name of the variable on the left (resp. right) of an equality |
57 (*Locates a substitutable variable on the left (resp. right) of an equality |
68 assumption. Returns the rule asm_rl (resp. sym). *) |
58 assumption. Returns the number of intervening assumptions, paried with |
69 fun eq_var bnd (Const("all",_) $ Abs(_,_,t)) = eq_var bnd t |
59 the rule asm_rl (resp. sym). *) |
70 | eq_var bnd (Const("==>",_) $ A $ B) = |
60 fun eq_var bnd = |
71 (inspect_pair bnd (dest_eq A) |
61 let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t |
72 (*Match comes from inspect_pair or dest_eq*) |
62 | eq_var_aux k (Const("==>",_) $ A $ B) = |
73 handle Match => eq_var bnd B) |
63 ((k, inspect_pair bnd (dest_eq A)) |
74 | eq_var bnd _ = raise EQ_VAR; |
64 (*Exception Match comes from inspect_pair or dest_eq*) |
75 |
65 handle Match => eq_var_aux (k+1) B) |
76 (*Lift and instantiate a rule wrt the given state and subgoal number *) |
66 | eq_var_aux k _ = raise EQ_VAR |
77 fun lift_instpair (state, i, t, rule) = |
67 in eq_var_aux 0 end; |
78 let val {maxidx,sign,...} = rep_thm state |
|
79 val (_, _, Bi, _) = dest_state(state,i) |
|
80 val params = Logic.strip_params Bi |
|
81 val var = liftvar (maxidx+1) (map #2 params) |
|
82 and u = Unify.rlist_abs(rev params, t) |
|
83 and cterm = cterm_of sign |
|
84 in cterm_instantiate [(cterm var, cterm u)] (lift_rule (state,i) rule) |
|
85 end; |
|
86 |
|
87 fun eres_instpair_tac t rule i = STATE (fn state => |
|
88 compose_tac (true, lift_instpair (state, i, t, rule), |
|
89 length(prems_of rule)) i); |
|
90 |
|
91 val ssubst = sym RS subst; |
|
92 |
68 |
93 (*Select a suitable equality assumption and substitute throughout the subgoal |
69 (*Select a suitable equality assumption and substitute throughout the subgoal |
94 Replaces only Bound variables if bnd is true*) |
70 Replaces only Bound variables if bnd is true*) |
95 fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state => |
71 fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state => |
96 let val (_,_,Bi,_) = dest_state(state,i) |
72 let val (_,_,Bi,_) = dest_state(state,i) |
97 val n = length(Logic.strip_assums_hyp Bi) - 1 |
73 val n = length(Logic.strip_assums_hyp Bi) - 1 |
98 val (t,symopt) = eq_var bnd Bi |
74 val (k,symopt) = eq_var bnd Bi |
99 in eres_instpair_tac t (symopt RS rev_cut_eq) i THEN |
75 in |
100 REPEATN n (etac rev_mp i) THEN |
76 EVERY [REPEATN k (etac rev_mp i), |
101 etac ssubst i THEN REPEATN n (rtac imp_intr i) |
77 etac revcut_rl i, |
|
78 REPEATN (n-k) (etac rev_mp i), |
|
79 etac (symopt RS subst) i, |
|
80 REPEATN n (rtac imp_intr i)] |
102 end |
81 end |
103 handle THM _ => no_tac | EQ_VAR => no_tac)); |
82 handle THM _ => no_tac | EQ_VAR => no_tac)); |
104 |
83 |
105 (*Substitutes for Free or Bound variables*) |
84 (*Substitutes for Free or Bound variables*) |
106 val hyp_subst_tac = gen_hyp_subst_tac false; |
85 val hyp_subst_tac = gen_hyp_subst_tac false; |