author | kleing |
Sat, 30 Apr 2005 14:18:36 +0200 | |
changeset 15900 | d6156cb8dc2e |
parent 15874 | 6236cc88d4b8 |
child 15977 | aa6744dd998e |
permissions | -rw-r--r-- |
10805 | 1 |
(* Title: Pure/tactic.ML |
0 | 2 |
ID: $Id$ |
10805 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1991 University of Cambridge |
5 |
||
10805 | 6 |
Tactics. |
0 | 7 |
*) |
8 |
||
11774 | 9 |
signature BASIC_TACTIC = |
10 |
sig |
|
10805 | 11 |
val ares_tac : thm list -> int -> tactic |
12 |
val assume_tac : int -> tactic |
|
13 |
val atac : int ->tactic |
|
10817 | 14 |
val bimatch_from_nets_tac: |
1501 | 15 |
(int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic |
10805 | 16 |
val bimatch_tac : (bool*thm)list -> int -> tactic |
10817 | 17 |
val biresolution_from_nets_tac: |
10805 | 18 |
('a list -> (bool * thm) list) -> |
19 |
bool -> 'a Net.net * 'a Net.net -> int -> tactic |
|
10817 | 20 |
val biresolve_from_nets_tac: |
1501 | 21 |
(int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic |
10805 | 22 |
val biresolve_tac : (bool*thm)list -> int -> tactic |
23 |
val build_net : thm list -> (int*thm) Net.net |
|
1501 | 24 |
val build_netpair: (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> |
25 |
(bool*thm)list -> (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net |
|
10817 | 26 |
val compose_inst_tac : (string*string)list -> (bool*thm*int) -> |
3409
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
27 |
int -> tactic |
10817 | 28 |
val compose_tac : (bool * thm * int) -> int -> tactic |
10805 | 29 |
val cut_facts_tac : thm list -> int -> tactic |
13650
31bd2a8cdbe2
fixing the cut_tac method to work when there are no instantiations and the
paulson
parents:
13559
diff
changeset
|
30 |
val cut_rules_tac : thm list -> int -> tactic |
10817 | 31 |
val cut_inst_tac : (string*string)list -> thm -> int -> tactic |
7491 | 32 |
val datac : thm -> int -> int -> tactic |
10805 | 33 |
val defer_tac : int -> tactic |
34 |
val distinct_subgoals_tac : tactic |
|
35 |
val dmatch_tac : thm list -> int -> tactic |
|
36 |
val dresolve_tac : thm list -> int -> tactic |
|
10817 | 37 |
val dres_inst_tac : (string*string)list -> thm -> int -> tactic |
10805 | 38 |
val dtac : thm -> int ->tactic |
7491 | 39 |
val eatac : thm -> int -> int -> tactic |
10805 | 40 |
val etac : thm -> int ->tactic |
10817 | 41 |
val eq_assume_tac : int -> tactic |
10805 | 42 |
val ematch_tac : thm list -> int -> tactic |
43 |
val eresolve_tac : thm list -> int -> tactic |
|
44 |
val eres_inst_tac : (string*string)list -> thm -> int -> tactic |
|
7491 | 45 |
val fatac : thm -> int -> int -> tactic |
10817 | 46 |
val filter_prems_tac : (term -> bool) -> int -> tactic |
10805 | 47 |
val filter_thms : (term*term->bool) -> int*term*thm list -> thm list |
48 |
val filt_resolve_tac : thm list -> int -> int -> tactic |
|
49 |
val flexflex_tac : tactic |
|
50 |
val fold_goals_tac : thm list -> tactic |
|
51 |
val fold_rule : thm list -> thm -> thm |
|
52 |
val fold_tac : thm list -> tactic |
|
10817 | 53 |
val forward_tac : thm list -> int -> tactic |
10805 | 54 |
val forw_inst_tac : (string*string)list -> thm -> int -> tactic |
55 |
val ftac : thm -> int ->tactic |
|
12320 | 56 |
val insert_tagged_brl : ('a * (bool * thm)) * |
57 |
(('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net) -> |
|
58 |
('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net |
|
59 |
val delete_tagged_brl : (bool * thm) * |
|
60 |
(('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net) -> |
|
61 |
('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net |
|
10805 | 62 |
val is_fact : thm -> bool |
63 |
val lessb : (bool * thm) * (bool * thm) -> bool |
|
64 |
val lift_inst_rule : thm * int * (string*string)list * thm -> thm |
|
65 |
val make_elim : thm -> thm |
|
66 |
val match_from_net_tac : (int*thm) Net.net -> int -> tactic |
|
67 |
val match_tac : thm list -> int -> tactic |
|
68 |
val metacut_tac : thm -> int -> tactic |
|
69 |
val net_bimatch_tac : (bool*thm) list -> int -> tactic |
|
70 |
val net_biresolve_tac : (bool*thm) list -> int -> tactic |
|
71 |
val net_match_tac : thm list -> int -> tactic |
|
72 |
val net_resolve_tac : thm list -> int -> tactic |
|
15696 | 73 |
val norm_hhf_plain : thm -> thm |
12801 | 74 |
val norm_hhf_rule : thm -> thm |
10805 | 75 |
val norm_hhf_tac : int -> tactic |
76 |
val prune_params_tac : tactic |
|
77 |
val rename_params_tac : string list -> int -> tactic |
|
78 |
val rename_tac : string -> int -> tactic |
|
79 |
val rename_last_tac : string -> string list -> int -> tactic |
|
80 |
val resolve_from_net_tac : (int*thm) Net.net -> int -> tactic |
|
81 |
val resolve_tac : thm list -> int -> tactic |
|
10817 | 82 |
val res_inst_tac : (string*string)list -> thm -> int -> tactic |
10444 | 83 |
val rewrite_goal_tac : thm list -> int -> tactic |
3575
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3554
diff
changeset
|
84 |
val rewrite_goals_rule: thm list -> thm -> thm |
10805 | 85 |
val rewrite_rule : thm list -> thm -> thm |
86 |
val rewrite_goals_tac : thm list -> tactic |
|
87 |
val rewrite_tac : thm list -> tactic |
|
88 |
val rewtac : thm -> tactic |
|
89 |
val rotate_tac : int -> int -> tactic |
|
90 |
val rtac : thm -> int -> tactic |
|
91 |
val rule_by_tactic : tactic -> thm -> thm |
|
92 |
val solve_tac : thm list -> int -> tactic |
|
93 |
val subgoal_tac : string -> int -> tactic |
|
94 |
val subgoals_tac : string list -> int -> tactic |
|
95 |
val subgoals_of_brl : bool * thm -> int |
|
96 |
val term_lift_inst_rule : |
|
15797 | 97 |
thm * int * ((indexname * sort) * typ) list * ((indexname * typ) * term) list * thm |
1975
eec67972b1bf
renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents:
1966
diff
changeset
|
98 |
-> thm |
10347 | 99 |
val instantiate_tac : (string * string) list -> tactic |
10805 | 100 |
val thin_tac : string -> int -> tactic |
101 |
val trace_goalno_tac : (int -> tactic) -> int -> tactic |
|
11774 | 102 |
end; |
0 | 103 |
|
11774 | 104 |
signature TACTIC = |
105 |
sig |
|
106 |
include BASIC_TACTIC |
|
11929 | 107 |
val innermost_params: int -> thm -> (string * typ) list |
11774 | 108 |
val untaglist: (int * 'a) list -> 'a list |
109 |
val orderlist: (int * 'a) list -> 'a list |
|
110 |
val rewrite: bool -> thm list -> cterm -> thm |
|
111 |
val simplify: bool -> thm list -> thm -> thm |
|
12139 | 112 |
val conjunction_tac: tactic |
15874
6236cc88d4b8
added smart_conjunction_tac, prove_multi, prove_multi_standard;
wenzelm
parents:
15797
diff
changeset
|
113 |
val smart_conjunction_tac: int -> tactic |
6236cc88d4b8
added smart_conjunction_tac, prove_multi, prove_multi_standard;
wenzelm
parents:
15797
diff
changeset
|
114 |
val prove_multi: Sign.sg -> string list -> term list -> term list -> |
6236cc88d4b8
added smart_conjunction_tac, prove_multi, prove_multi_standard;
wenzelm
parents:
15797
diff
changeset
|
115 |
(thm list -> tactic) -> thm list |
6236cc88d4b8
added smart_conjunction_tac, prove_multi, prove_multi_standard;
wenzelm
parents:
15797
diff
changeset
|
116 |
val prove_multi_standard: Sign.sg -> string list -> term list -> term list -> |
6236cc88d4b8
added smart_conjunction_tac, prove_multi, prove_multi_standard;
wenzelm
parents:
15797
diff
changeset
|
117 |
(thm list -> tactic) -> thm list |
11970 | 118 |
val prove: Sign.sg -> string list -> term list -> term -> (thm list -> tactic) -> thm |
15874
6236cc88d4b8
added smart_conjunction_tac, prove_multi, prove_multi_standard;
wenzelm
parents:
15797
diff
changeset
|
119 |
val prove_standard: Sign.sg -> string list -> term list -> term -> |
6236cc88d4b8
added smart_conjunction_tac, prove_multi, prove_multi_standard;
wenzelm
parents:
15797
diff
changeset
|
120 |
(thm list -> tactic) -> thm |
15442
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15021
diff
changeset
|
121 |
val compose_inst_tac' : (indexname * string) list -> (bool * thm * int) -> |
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15021
diff
changeset
|
122 |
int -> tactic |
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15021
diff
changeset
|
123 |
val lift_inst_rule' : thm * int * (indexname * string) list * thm -> thm |
15464
02cc838b64ca
Added variant of eres_inst_tac that operates on indexnames instead of strings.
berghofe
parents:
15453
diff
changeset
|
124 |
val eres_inst_tac' : (indexname * string) list -> thm -> int -> tactic |
15442
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15021
diff
changeset
|
125 |
val res_inst_tac' : (indexname * string) list -> thm -> int -> tactic |
15797 | 126 |
val instantiate_tac' : (indexname * string) list -> tactic |
11774 | 127 |
end; |
0 | 128 |
|
11774 | 129 |
structure Tactic: TACTIC = |
0 | 130 |
struct |
131 |
||
1501 | 132 |
(*Discover which goal is chosen: SOMEGOAL(trace_goalno_tac tac) *) |
10817 | 133 |
fun trace_goalno_tac tac i st = |
4270 | 134 |
case Seq.pull(tac i st) of |
15531 | 135 |
NONE => Seq.empty |
12262 | 136 |
| seqcell => (tracing ("Subgoal " ^ string_of_int i ^ " selected"); |
10805 | 137 |
Seq.make(fn()=> seqcell)); |
0 | 138 |
|
139 |
(*Makes a rule by applying a tactic to an existing rule*) |
|
1501 | 140 |
fun rule_by_tactic tac rl = |
2688 | 141 |
let val (st, thaw) = freeze_thaw (zero_var_indexes rl) |
4270 | 142 |
in case Seq.pull (tac st) of |
15531 | 143 |
NONE => raise THM("rule_by_tactic", 0, [rl]) |
144 |
| SOME(st',_) => Thm.varifyT (thaw st') |
|
2688 | 145 |
end; |
10817 | 146 |
|
0 | 147 |
(*** Basic tactics ***) |
148 |
||
149 |
(*** The following fail if the goal number is out of range: |
|
150 |
thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *) |
|
151 |
||
152 |
(*Solve subgoal i by assumption*) |
|
153 |
fun assume_tac i = PRIMSEQ (assumption i); |
|
154 |
||
155 |
(*Solve subgoal i by assumption, using no unification*) |
|
156 |
fun eq_assume_tac i = PRIMITIVE (eq_assumption i); |
|
157 |
||
158 |
(** Resolution/matching tactics **) |
|
159 |
||
160 |
(*The composition rule/state: no lifting or var renaming. |
|
161 |
The arg = (bires_flg, orule, m) ; see bicompose for explanation.*) |
|
162 |
fun compose_tac arg i = PRIMSEQ (bicompose false arg i); |
|
163 |
||
164 |
(*Converts a "destruct" rule like P&Q==>P to an "elimination" rule |
|
165 |
like [| P&Q; P==>R |] ==> R *) |
|
166 |
fun make_elim rl = zero_var_indexes (rl RS revcut_rl); |
|
167 |
||
168 |
(*Attack subgoal i by resolution, using flags to indicate elimination rules*) |
|
169 |
fun biresolve_tac brules i = PRIMSEQ (biresolution false brules i); |
|
170 |
||
171 |
(*Resolution: the simple case, works for introduction rules*) |
|
172 |
fun resolve_tac rules = biresolve_tac (map (pair false) rules); |
|
173 |
||
174 |
(*Resolution with elimination rules only*) |
|
175 |
fun eresolve_tac rules = biresolve_tac (map (pair true) rules); |
|
176 |
||
177 |
(*Forward reasoning using destruction rules.*) |
|
178 |
fun forward_tac rls = resolve_tac (map make_elim rls) THEN' assume_tac; |
|
179 |
||
180 |
(*Like forward_tac, but deletes the assumption after use.*) |
|
181 |
fun dresolve_tac rls = eresolve_tac (map make_elim rls); |
|
182 |
||
183 |
(*Shorthand versions: for resolution with a single theorem*) |
|
7491 | 184 |
val atac = assume_tac; |
185 |
fun rtac rl = resolve_tac [rl]; |
|
186 |
fun dtac rl = dresolve_tac [rl]; |
|
1460 | 187 |
fun etac rl = eresolve_tac [rl]; |
7491 | 188 |
fun ftac rl = forward_tac [rl]; |
189 |
fun datac thm j = EVERY' (dtac thm::replicate j atac); |
|
190 |
fun eatac thm j = EVERY' (etac thm::replicate j atac); |
|
191 |
fun fatac thm j = EVERY' (ftac thm::replicate j atac); |
|
0 | 192 |
|
193 |
(*Use an assumption or some rules ... A popular combination!*) |
|
194 |
fun ares_tac rules = assume_tac ORELSE' resolve_tac rules; |
|
195 |
||
5263 | 196 |
fun solve_tac rules = resolve_tac rules THEN_ALL_NEW assume_tac; |
197 |
||
0 | 198 |
(*Matching tactics -- as above, but forbid updating of state*) |
199 |
fun bimatch_tac brules i = PRIMSEQ (biresolution true brules i); |
|
200 |
fun match_tac rules = bimatch_tac (map (pair false) rules); |
|
201 |
fun ematch_tac rules = bimatch_tac (map (pair true) rules); |
|
202 |
fun dmatch_tac rls = ematch_tac (map make_elim rls); |
|
203 |
||
204 |
(*Smash all flex-flex disagreement pairs in the proof state.*) |
|
205 |
val flexflex_tac = PRIMSEQ flexflex_rule; |
|
206 |
||
3409
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
207 |
|
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
208 |
(*Remove duplicate subgoals. By Mark Staples*) |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
209 |
local |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
210 |
fun cterm_aconv (a,b) = #t (rep_cterm a) aconv #t (rep_cterm b); |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
211 |
in |
10817 | 212 |
fun distinct_subgoals_tac state = |
3409
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
213 |
let val (frozth,thawfn) = freeze_thaw state |
10805 | 214 |
val froz_prems = cprems_of frozth |
215 |
val assumed = implies_elim_list frozth (map assume froz_prems) |
|
216 |
val implied = implies_intr_list (gen_distinct cterm_aconv froz_prems) |
|
217 |
assumed; |
|
4270 | 218 |
in Seq.single (thawfn implied) end |
10817 | 219 |
end; |
3409
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
220 |
|
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
221 |
|
11929 | 222 |
(*Determine print names of goal parameters (reversed)*) |
223 |
fun innermost_params i st = |
|
224 |
let val (_, _, Bi, _) = dest_state (st, i) |
|
225 |
in rename_wrt_term Bi (Logic.strip_params Bi) end; |
|
226 |
||
15453 | 227 |
(*params of subgoal i as they are printed*) |
228 |
fun params_of_state st i = |
|
229 |
let val (_, _, Bi, _) = dest_state(st,i) |
|
230 |
val params = Logic.strip_params Bi |
|
231 |
in rev(rename_wrt_term Bi params) end; |
|
232 |
||
233 |
(*read instantiations with respect to subgoal i of proof state st*) |
|
234 |
fun read_insts_in_state (st, i, sinsts, rule) = |
|
235 |
let val {sign,...} = rep_thm st |
|
236 |
and params = params_of_state st i |
|
237 |
and rts = types_sorts rule and (types,sorts) = types_sorts st |
|
15531 | 238 |
fun types'(a,~1) = (case assoc(params,a) of NONE => types(a,~1) | sm => sm) |
15453 | 239 |
| types'(ixn) = types ixn; |
15671 | 240 |
val used = Drule.add_used rule (Drule.add_used st []); |
15453 | 241 |
in read_insts sign rts (types',sorts) used sinsts end; |
242 |
||
0 | 243 |
(*Lift and instantiate a rule wrt the given state and subgoal number *) |
15442
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15021
diff
changeset
|
244 |
fun lift_inst_rule' (st, i, sinsts, rule) = |
15453 | 245 |
let val (Tinsts,insts) = read_insts_in_state (st, i, sinsts, rule) |
246 |
and {maxidx,...} = rep_thm st |
|
247 |
and params = params_of_state st i |
|
0 | 248 |
val paramTs = map #2 params |
249 |
and inc = maxidx+1 |
|
250 |
fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs---> incr_tvar inc T) |
|
251 |
| liftvar t = raise TERM("Variable expected", [t]); |
|
10817 | 252 |
fun liftterm t = list_abs_free (params, |
10805 | 253 |
Logic.incr_indexes(paramTs,inc) t) |
0 | 254 |
(*Lifts instantiation pair over params*) |
230 | 255 |
fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct) |
15797 | 256 |
val lifttvar = pairself (ctyp_fun (incr_tvar inc)) |
8129
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
7596
diff
changeset
|
257 |
in Drule.instantiate (map lifttvar Tinsts, map liftpair insts) |
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
7596
diff
changeset
|
258 |
(lift_rule (st,i) rule) |
0 | 259 |
end; |
260 |
||
15442
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15021
diff
changeset
|
261 |
fun lift_inst_rule (st, i, sinsts, rule) = lift_inst_rule' |
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15021
diff
changeset
|
262 |
(st, i, map (apfst Syntax.indexname) sinsts, rule); |
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15021
diff
changeset
|
263 |
|
3984 | 264 |
(* |
265 |
Like lift_inst_rule but takes terms, not strings, where the terms may contain |
|
266 |
Bounds referring to parameters of the subgoal. |
|
267 |
||
268 |
insts: [...,(vj,tj),...] |
|
269 |
||
270 |
The tj may contain references to parameters of subgoal i of the state st |
|
271 |
in the form of Bound k, i.e. the tj may be subterms of the subgoal. |
|
272 |
To saturate the lose bound vars, the tj are enclosed in abstractions |
|
273 |
corresponding to the parameters of subgoal i, thus turning them into |
|
274 |
functions. At the same time, the types of the vj are lifted. |
|
275 |
||
276 |
NB: the types in insts must be correctly instantiated already, |
|
277 |
i.e. Tinsts is not applied to insts. |
|
278 |
*) |
|
1975
eec67972b1bf
renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents:
1966
diff
changeset
|
279 |
fun term_lift_inst_rule (st, i, Tinsts, insts, rule) = |
1966 | 280 |
let val {maxidx,sign,...} = rep_thm st |
15453 | 281 |
val paramTs = map #2 (params_of_state st i) |
1966 | 282 |
and inc = maxidx+1 |
1975
eec67972b1bf
renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents:
1966
diff
changeset
|
283 |
fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> incr_tvar inc T) |
eec67972b1bf
renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents:
1966
diff
changeset
|
284 |
(*lift only Var, not term, which must be lifted already*) |
eec67972b1bf
renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents:
1966
diff
changeset
|
285 |
fun liftpair (v,t) = (cterm_of sign (liftvar v), cterm_of sign t) |
15797 | 286 |
fun liftTpair (((a, i), S), T) = |
287 |
(ctyp_of sign (TVar ((a, i + inc), S)), |
|
288 |
ctyp_of sign (incr_tvar inc T)) |
|
8129
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
7596
diff
changeset
|
289 |
in Drule.instantiate (map liftTpair Tinsts, map liftpair insts) |
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
7596
diff
changeset
|
290 |
(lift_rule (st,i) rule) |
1966 | 291 |
end; |
0 | 292 |
|
293 |
(*** Resolve after lifting and instantation; may refer to parameters of the |
|
294 |
subgoal. Fails if "i" is out of range. ***) |
|
295 |
||
296 |
(*compose version: arguments are as for bicompose.*) |
|
15442
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15021
diff
changeset
|
297 |
fun gen_compose_inst_tac instf sinsts (bires_flg, rule, nsubgoal) i st = |
8977
dd8bc754a072
res_inst_tac, etc., no longer print the "dest_state" message when the selected
paulson
parents:
8129
diff
changeset
|
298 |
if i > nprems_of st then no_tac st |
dd8bc754a072
res_inst_tac, etc., no longer print the "dest_state" message when the selected
paulson
parents:
8129
diff
changeset
|
299 |
else st |> |
15442
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15021
diff
changeset
|
300 |
(compose_tac (bires_flg, instf (st, i, sinsts, rule), nsubgoal) i |
12262 | 301 |
handle TERM (msg,_) => (warning msg; no_tac) |
302 |
| THM (msg,_,_) => (warning msg; no_tac)); |
|
0 | 303 |
|
15442
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15021
diff
changeset
|
304 |
val compose_inst_tac = gen_compose_inst_tac lift_inst_rule; |
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15021
diff
changeset
|
305 |
val compose_inst_tac' = gen_compose_inst_tac lift_inst_rule'; |
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15021
diff
changeset
|
306 |
|
761 | 307 |
(*"Resolve" version. Note: res_inst_tac cannot behave sensibly if the |
308 |
terms that are substituted contain (term or type) unknowns from the |
|
309 |
goal, because it is unable to instantiate goal unknowns at the same time. |
|
310 |
||
2029 | 311 |
The type checker is instructed not to freeze flexible type vars that |
952
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset
|
312 |
were introduced during type inference and still remain in the term at the |
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset
|
313 |
end. This increases flexibility but can introduce schematic type vars in |
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset
|
314 |
goals. |
761 | 315 |
*) |
0 | 316 |
fun res_inst_tac sinsts rule i = |
317 |
compose_inst_tac sinsts (false, rule, nprems_of rule) i; |
|
318 |
||
15442
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15021
diff
changeset
|
319 |
fun res_inst_tac' sinsts rule i = |
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15021
diff
changeset
|
320 |
compose_inst_tac' sinsts (false, rule, nprems_of rule) i; |
3b75e1b22ff1
Added variants of instantiation functions that operate on pairs of type
berghofe
parents:
15021
diff
changeset
|
321 |
|
1501 | 322 |
(*eresolve elimination version*) |
0 | 323 |
fun eres_inst_tac sinsts rule i = |
324 |
compose_inst_tac sinsts (true, rule, nprems_of rule) i; |
|
325 |
||
15464
02cc838b64ca
Added variant of eres_inst_tac that operates on indexnames instead of strings.
berghofe
parents:
15453
diff
changeset
|
326 |
fun eres_inst_tac' sinsts rule i = |
02cc838b64ca
Added variant of eres_inst_tac that operates on indexnames instead of strings.
berghofe
parents:
15453
diff
changeset
|
327 |
compose_inst_tac' sinsts (true, rule, nprems_of rule) i; |
02cc838b64ca
Added variant of eres_inst_tac that operates on indexnames instead of strings.
berghofe
parents:
15453
diff
changeset
|
328 |
|
270
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset
|
329 |
(*For forw_inst_tac and dres_inst_tac. Preserve Var indexes of rl; |
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset
|
330 |
increment revcut_rl instead.*) |
10817 | 331 |
fun make_elim_preserve rl = |
270
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset
|
332 |
let val {maxidx,...} = rep_thm rl |
6390 | 333 |
fun cvar ixn = cterm_of (Theory.sign_of ProtoPure.thy) (Var(ixn,propT)); |
10817 | 334 |
val revcut_rl' = |
10805 | 335 |
instantiate ([], [(cvar("V",0), cvar("V",maxidx+1)), |
336 |
(cvar("W",0), cvar("W",maxidx+1))]) revcut_rl |
|
0 | 337 |
val arg = (false, rl, nprems_of rl) |
4270 | 338 |
val [th] = Seq.list_of (bicompose false arg 1 revcut_rl') |
0 | 339 |
in th end |
340 |
handle Bind => raise THM("make_elim_preserve", 1, [rl]); |
|
341 |
||
270
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset
|
342 |
(*instantiate and cut -- for a FACT, anyway...*) |
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset
|
343 |
fun cut_inst_tac sinsts rule = res_inst_tac sinsts (make_elim_preserve rule); |
0 | 344 |
|
270
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset
|
345 |
(*forward tactic applies a RULE to an assumption without deleting it*) |
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset
|
346 |
fun forw_inst_tac sinsts rule = cut_inst_tac sinsts rule THEN' assume_tac; |
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset
|
347 |
|
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset
|
348 |
(*dresolve tactic applies a RULE to replace an assumption*) |
0 | 349 |
fun dres_inst_tac sinsts rule = eres_inst_tac sinsts (make_elim_preserve rule); |
350 |
||
10347 | 351 |
(*instantiate variables in the whole state*) |
352 |
val instantiate_tac = PRIMITIVE o read_instantiate; |
|
353 |
||
15797 | 354 |
val instantiate_tac' = PRIMITIVE o Drule.read_instantiate'; |
355 |
||
1951 | 356 |
(*Deletion of an assumption*) |
357 |
fun thin_tac s = eres_inst_tac [("V",s)] thin_rl; |
|
358 |
||
270
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset
|
359 |
(*** Applications of cut_rl ***) |
0 | 360 |
|
361 |
(*Used by metacut_tac*) |
|
362 |
fun bires_cut_tac arg i = |
|
1460 | 363 |
resolve_tac [cut_rl] i THEN biresolve_tac arg (i+1) ; |
0 | 364 |
|
365 |
(*The conclusion of the rule gets assumed in subgoal i, |
|
366 |
while subgoal i+1,... are the premises of the rule.*) |
|
367 |
fun metacut_tac rule = bires_cut_tac [(false,rule)]; |
|
368 |
||
369 |
(*Recognizes theorems that are not rules, but simple propositions*) |
|
370 |
fun is_fact rl = |
|
371 |
case prems_of rl of |
|
10805 | 372 |
[] => true | _::_ => false; |
0 | 373 |
|
13650
31bd2a8cdbe2
fixing the cut_tac method to work when there are no instantiations and the
paulson
parents:
13559
diff
changeset
|
374 |
(*"Cut" a list of rules into the goal. Their premises will become new |
31bd2a8cdbe2
fixing the cut_tac method to work when there are no instantiations and the
paulson
parents:
13559
diff
changeset
|
375 |
subgoals.*) |
31bd2a8cdbe2
fixing the cut_tac method to work when there are no instantiations and the
paulson
parents:
13559
diff
changeset
|
376 |
fun cut_rules_tac ths i = EVERY (map (fn th => metacut_tac th i) ths); |
31bd2a8cdbe2
fixing the cut_tac method to work when there are no instantiations and the
paulson
parents:
13559
diff
changeset
|
377 |
|
31bd2a8cdbe2
fixing the cut_tac method to work when there are no instantiations and the
paulson
parents:
13559
diff
changeset
|
378 |
(*As above, but inserts only facts (unconditional theorems); |
31bd2a8cdbe2
fixing the cut_tac method to work when there are no instantiations and the
paulson
parents:
13559
diff
changeset
|
379 |
generates no additional subgoals. *) |
15570 | 380 |
fun cut_facts_tac ths = cut_rules_tac (List.filter is_fact ths); |
0 | 381 |
|
382 |
(*Introduce the given proposition as a lemma and subgoal*) |
|
12847
afa356dbcb15
fixed subgoal_tac; fails on non-existent subgoal;
wenzelm
parents:
12801
diff
changeset
|
383 |
fun subgoal_tac sprop = |
afa356dbcb15
fixed subgoal_tac; fails on non-existent subgoal;
wenzelm
parents:
12801
diff
changeset
|
384 |
DETERM o res_inst_tac [("psi", sprop)] cut_rl THEN' SUBGOAL (fn (prop, _) => |
afa356dbcb15
fixed subgoal_tac; fails on non-existent subgoal;
wenzelm
parents:
12801
diff
changeset
|
385 |
let val concl' = Logic.strip_assums_concl prop in |
4178
e64ff1c1bc70
subgoal_tac displays a warning if the new subgoal has type variables
paulson
parents:
3991
diff
changeset
|
386 |
if null (term_tvars concl') then () |
e64ff1c1bc70
subgoal_tac displays a warning if the new subgoal has type variables
paulson
parents:
3991
diff
changeset
|
387 |
else warning"Type variables in new subgoal: add a type constraint?"; |
12847
afa356dbcb15
fixed subgoal_tac; fails on non-existent subgoal;
wenzelm
parents:
12801
diff
changeset
|
388 |
all_tac |
afa356dbcb15
fixed subgoal_tac; fails on non-existent subgoal;
wenzelm
parents:
12801
diff
changeset
|
389 |
end); |
0 | 390 |
|
439 | 391 |
(*Introduce a list of lemmas and subgoals*) |
392 |
fun subgoals_tac sprops = EVERY' (map subgoal_tac sprops); |
|
393 |
||
0 | 394 |
|
395 |
(**** Indexing and filtering of theorems ****) |
|
396 |
||
397 |
(*Returns the list of potentially resolvable theorems for the goal "prem", |
|
10805 | 398 |
using the predicate could(subgoal,concl). |
0 | 399 |
Resulting list is no longer than "limit"*) |
400 |
fun filter_thms could (limit, prem, ths) = |
|
401 |
let val pb = Logic.strip_assums_concl prem; (*delete assumptions*) |
|
402 |
fun filtr (limit, []) = [] |
|
10805 | 403 |
| filtr (limit, th::ths) = |
404 |
if limit=0 then [] |
|
405 |
else if could(pb, concl_of th) then th :: filtr(limit-1, ths) |
|
406 |
else filtr(limit,ths) |
|
0 | 407 |
in filtr(limit,ths) end; |
408 |
||
409 |
||
410 |
(*** biresolution and resolution using nets ***) |
|
411 |
||
412 |
(** To preserve the order of the rules, tag them with increasing integers **) |
|
413 |
||
414 |
(*insert tags*) |
|
415 |
fun taglist k [] = [] |
|
416 |
| taglist k (x::xs) = (k,x) :: taglist (k+1) xs; |
|
417 |
||
418 |
(*remove tags and suppress duplicates -- list is assumed sorted!*) |
|
419 |
fun untaglist [] = [] |
|
420 |
| untaglist [(k:int,x)] = [x] |
|
421 |
| untaglist ((k,x) :: (rest as (k',x')::_)) = |
|
422 |
if k=k' then untaglist rest |
|
423 |
else x :: untaglist rest; |
|
424 |
||
425 |
(*return list elements in original order*) |
|
10817 | 426 |
fun orderlist kbrls = untaglist (sort (int_ord o pairself fst) kbrls); |
0 | 427 |
|
428 |
(*insert one tagged brl into the pair of nets*) |
|
12320 | 429 |
fun insert_tagged_brl (kbrl as (k, (eres, th)), (inet, enet)) = |
430 |
if eres then |
|
431 |
(case try Thm.major_prem_of th of |
|
15531 | 432 |
SOME prem => (inet, Net.insert_term ((prem, kbrl), enet, K false)) |
433 |
| NONE => error "insert_tagged_brl: elimination rule with no premises") |
|
12320 | 434 |
else (Net.insert_term ((concl_of th, kbrl), inet, K false), enet); |
0 | 435 |
|
436 |
(*build a pair of nets for biresolution*) |
|
10817 | 437 |
fun build_netpair netpair brls = |
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
438 |
foldr insert_tagged_brl netpair (taglist 1 brls); |
0 | 439 |
|
12320 | 440 |
(*delete one kbrl from the pair of nets*) |
1801 | 441 |
local |
13105
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
12847
diff
changeset
|
442 |
fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Drule.eq_thm_prop (th, th') |
1801 | 443 |
in |
12320 | 444 |
fun delete_tagged_brl (brl as (eres, th), (inet, enet)) = |
13925 | 445 |
(if eres then |
12320 | 446 |
(case try Thm.major_prem_of th of |
15531 | 447 |
SOME prem => (inet, Net.delete_term ((prem, ((), brl)), enet, eq_kbrl)) |
448 |
| NONE => (inet, enet)) (*no major premise: ignore*) |
|
13925 | 449 |
else (Net.delete_term ((Thm.concl_of th, ((), brl)), inet, eq_kbrl), enet)) |
450 |
handle Net.DELETE => (inet,enet); |
|
1801 | 451 |
end; |
452 |
||
453 |
||
10817 | 454 |
(*biresolution using a pair of nets rather than rules. |
3706
e57b5902822f
Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents:
3575
diff
changeset
|
455 |
function "order" must sort and possibly filter the list of brls. |
e57b5902822f
Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents:
3575
diff
changeset
|
456 |
boolean "match" indicates matching or unification.*) |
e57b5902822f
Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents:
3575
diff
changeset
|
457 |
fun biresolution_from_nets_tac order match (inet,enet) = |
0 | 458 |
SUBGOAL |
459 |
(fn (prem,i) => |
|
460 |
let val hyps = Logic.strip_assums_hyp prem |
|
10817 | 461 |
and concl = Logic.strip_assums_concl prem |
0 | 462 |
val kbrls = Net.unify_term inet concl @ |
2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2580
diff
changeset
|
463 |
List.concat (map (Net.unify_term enet) hyps) |
3706
e57b5902822f
Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents:
3575
diff
changeset
|
464 |
in PRIMSEQ (biresolution match (order kbrls) i) end); |
0 | 465 |
|
3706
e57b5902822f
Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents:
3575
diff
changeset
|
466 |
(*versions taking pre-built nets. No filtering of brls*) |
e57b5902822f
Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents:
3575
diff
changeset
|
467 |
val biresolve_from_nets_tac = biresolution_from_nets_tac orderlist false; |
e57b5902822f
Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents:
3575
diff
changeset
|
468 |
val bimatch_from_nets_tac = biresolution_from_nets_tac orderlist true; |
0 | 469 |
|
470 |
(*fast versions using nets internally*) |
|
670 | 471 |
val net_biresolve_tac = |
472 |
biresolve_from_nets_tac o build_netpair(Net.empty,Net.empty); |
|
473 |
||
474 |
val net_bimatch_tac = |
|
475 |
bimatch_from_nets_tac o build_netpair(Net.empty,Net.empty); |
|
0 | 476 |
|
477 |
(*** Simpler version for resolve_tac -- only one net, and no hyps ***) |
|
478 |
||
479 |
(*insert one tagged rl into the net*) |
|
480 |
fun insert_krl (krl as (k,th), net) = |
|
481 |
Net.insert_term ((concl_of th, krl), net, K false); |
|
482 |
||
483 |
(*build a net of rules for resolution*) |
|
10817 | 484 |
fun build_net rls = |
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
485 |
foldr insert_krl Net.empty (taglist 1 rls); |
0 | 486 |
|
487 |
(*resolution using a net rather than rules; pred supports filt_resolve_tac*) |
|
488 |
fun filt_resolution_from_net_tac match pred net = |
|
489 |
SUBGOAL |
|
490 |
(fn (prem,i) => |
|
491 |
let val krls = Net.unify_term net (Logic.strip_assums_concl prem) |
|
10817 | 492 |
in |
493 |
if pred krls |
|
0 | 494 |
then PRIMSEQ |
10805 | 495 |
(biresolution match (map (pair false) (orderlist krls)) i) |
0 | 496 |
else no_tac |
497 |
end); |
|
498 |
||
499 |
(*Resolve the subgoal using the rules (making a net) unless too flexible, |
|
500 |
which means more than maxr rules are unifiable. *) |
|
10817 | 501 |
fun filt_resolve_tac rules maxr = |
0 | 502 |
let fun pred krls = length krls <= maxr |
503 |
in filt_resolution_from_net_tac false pred (build_net rules) end; |
|
504 |
||
505 |
(*versions taking pre-built nets*) |
|
506 |
val resolve_from_net_tac = filt_resolution_from_net_tac false (K true); |
|
507 |
val match_from_net_tac = filt_resolution_from_net_tac true (K true); |
|
508 |
||
509 |
(*fast versions using nets internally*) |
|
510 |
val net_resolve_tac = resolve_from_net_tac o build_net; |
|
511 |
val net_match_tac = match_from_net_tac o build_net; |
|
512 |
||
513 |
||
514 |
(*** For Natural Deduction using (bires_flg, rule) pairs ***) |
|
515 |
||
516 |
(*The number of new subgoals produced by the brule*) |
|
1077
c2df11ae8b55
Renamed insert_kbrl to insert_tagged_brl and exported it. Now
lcp
parents:
952
diff
changeset
|
517 |
fun subgoals_of_brl (true,rule) = nprems_of rule - 1 |
c2df11ae8b55
Renamed insert_kbrl to insert_tagged_brl and exported it. Now
lcp
parents:
952
diff
changeset
|
518 |
| subgoals_of_brl (false,rule) = nprems_of rule; |
0 | 519 |
|
520 |
(*Less-than test: for sorting to minimize number of new subgoals*) |
|
521 |
fun lessb (brl1,brl2) = subgoals_of_brl brl1 < subgoals_of_brl brl2; |
|
522 |
||
523 |
||
524 |
(*** Meta-Rewriting Tactics ***) |
|
525 |
||
3575
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3554
diff
changeset
|
526 |
val simple_prover = |
15021 | 527 |
SINGLE o (fn ss => ALLGOALS (resolve_tac (MetaSimplifier.prems_of_ss ss))); |
3575
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3554
diff
changeset
|
528 |
|
11768
48bc55f43774
unified rewrite/rewrite_cterm/simplify interface;
wenzelm
parents:
11762
diff
changeset
|
529 |
val rewrite = MetaSimplifier.rewrite_aux simple_prover; |
48bc55f43774
unified rewrite/rewrite_cterm/simplify interface;
wenzelm
parents:
11762
diff
changeset
|
530 |
val simplify = MetaSimplifier.simplify_aux simple_prover; |
48bc55f43774
unified rewrite/rewrite_cterm/simplify interface;
wenzelm
parents:
11762
diff
changeset
|
531 |
val rewrite_rule = simplify true; |
10415
e6d7b77a0574
moved rewriting functions from Drule to MetaSimplifier
berghofe
parents:
10347
diff
changeset
|
532 |
val rewrite_goals_rule = MetaSimplifier.rewrite_goals_rule_aux simple_prover; |
3575
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3554
diff
changeset
|
533 |
|
10444 | 534 |
fun rewrite_goal_tac rews = |
15021 | 535 |
MetaSimplifier.asm_rewrite_goal_tac (true, false, false) (K no_tac) |
536 |
(MetaSimplifier.empty_ss addsimps rews); |
|
10444 | 537 |
|
69
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
538 |
(*Rewrite throughout proof state. *) |
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
539 |
fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs); |
0 | 540 |
|
541 |
(*Rewrite subgoals only, not main goal. *) |
|
69
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
542 |
fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs); |
1460 | 543 |
fun rewtac def = rewrite_goals_tac [def]; |
0 | 544 |
|
15696 | 545 |
fun norm_hhf_plain th = |
546 |
if Drule.is_norm_hhf (prop_of th) then th |
|
547 |
else rewrite_rule [Drule.norm_hhf_eq] th; |
|
548 |
||
12801 | 549 |
fun norm_hhf_rule th = |
15696 | 550 |
th |> norm_hhf_plain |> Drule.gen_all; |
10817 | 551 |
|
12782 | 552 |
val norm_hhf_tac = |
553 |
rtac Drule.asm_rl (*cheap approximation -- thanks to builtin Logic.flatten_params*) |
|
554 |
THEN' SUBGOAL (fn (t, i) => |
|
12801 | 555 |
if Drule.is_norm_hhf t then all_tac |
12782 | 556 |
else rewrite_goal_tac [Drule.norm_hhf_eq] i); |
10805 | 557 |
|
0 | 558 |
|
1501 | 559 |
(*** for folding definitions, handling critical pairs ***) |
69
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
560 |
|
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
561 |
(*The depth of nesting in a term*) |
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
562 |
fun term_depth (Abs(a,T,t)) = 1 + term_depth t |
2145 | 563 |
| term_depth (f$t) = 1 + Int.max(term_depth f, term_depth t) |
69
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
564 |
| term_depth _ = 0; |
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
565 |
|
12801 | 566 |
val lhs_of_thm = #1 o Logic.dest_equals o prop_of; |
69
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
567 |
|
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
568 |
(*folding should handle critical pairs! E.g. K == Inl(0), S == Inr(Inl(0)) |
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
569 |
Returns longest lhs first to avoid folding its subexpressions.*) |
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
570 |
fun sort_lhs_depths defs = |
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
571 |
let val keylist = make_keylist (term_depth o lhs_of_thm) defs |
4438 | 572 |
val keys = distinct (sort (rev_order o int_ord) (map #2 keylist)) |
69
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
573 |
in map (keyfilter keylist) keys end; |
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
574 |
|
7596 | 575 |
val rev_defs = sort_lhs_depths o map symmetric; |
69
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
576 |
|
15570 | 577 |
fun fold_rule defs thm = Library.foldl (fn (th, ds) => rewrite_rule ds th) (thm, rev_defs defs); |
7596 | 578 |
fun fold_tac defs = EVERY (map rewrite_tac (rev_defs defs)); |
579 |
fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs)); |
|
69
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
580 |
|
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
581 |
|
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
582 |
(*** Renaming of parameters in a subgoal |
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
583 |
Names may contain letters, digits or primes and must be |
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
584 |
separated by blanks ***) |
0 | 585 |
|
586 |
(*Calling this will generate the warning "Same as previous level" since |
|
587 |
it affects nothing but the names of bound variables!*) |
|
9535 | 588 |
fun rename_params_tac xs i = |
14673 | 589 |
case Library.find_first (not o Syntax.is_identifier) xs of |
15531 | 590 |
SOME x => error ("Not an identifier: " ^ x) |
591 |
| NONE => |
|
13559
51c3ac47d127
added checking so that (rename_tac "x y") is rejected, since
paulson
parents:
13105
diff
changeset
|
592 |
(if !Logic.auto_rename |
51c3ac47d127
added checking so that (rename_tac "x y") is rejected, since
paulson
parents:
13105
diff
changeset
|
593 |
then (warning "Resetting Logic.auto_rename"; |
51c3ac47d127
added checking so that (rename_tac "x y") is rejected, since
paulson
parents:
13105
diff
changeset
|
594 |
Logic.auto_rename := false) |
51c3ac47d127
added checking so that (rename_tac "x y") is rejected, since
paulson
parents:
13105
diff
changeset
|
595 |
else (); PRIMITIVE (rename_params_rule (xs, i))); |
9535 | 596 |
|
10817 | 597 |
fun rename_tac str i = |
598 |
let val cs = Symbol.explode str in |
|
4693 | 599 |
case #2 (take_prefix (Symbol.is_letdig orf Symbol.is_blank) cs) of |
9535 | 600 |
[] => rename_params_tac (scanwords Symbol.is_letdig cs) i |
0 | 601 |
| c::_ => error ("Illegal character: " ^ c) |
602 |
end; |
|
603 |
||
1501 | 604 |
(*Rename recent parameters using names generated from a and the suffixes, |
605 |
provided the string a, which represents a term, is an identifier. *) |
|
10817 | 606 |
fun rename_last_tac a sufs i = |
0 | 607 |
let val names = map (curry op^ a) sufs |
608 |
in if Syntax.is_identifier a |
|
609 |
then PRIMITIVE (rename_params_rule (names,i)) |
|
610 |
else all_tac |
|
611 |
end; |
|
612 |
||
2043 | 613 |
(*Prunes all redundant parameters from the proof state by rewriting. |
614 |
DOES NOT rewrite main goal, where quantification over an unused bound |
|
615 |
variable is sometimes done to avoid the need for cut_facts_tac.*) |
|
616 |
val prune_params_tac = rewrite_goals_tac [triv_forall_equality]; |
|
0 | 617 |
|
1501 | 618 |
(*rotate_tac n i: rotate the assumptions of subgoal i by n positions, from |
619 |
right to left if n is positive, and from left to right if n is negative.*) |
|
2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2580
diff
changeset
|
620 |
fun rotate_tac 0 i = all_tac |
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2580
diff
changeset
|
621 |
| rotate_tac k i = PRIMITIVE (rotate_rule k i); |
1209 | 622 |
|
7248
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
6979
diff
changeset
|
623 |
(*Rotates the given subgoal to be the last.*) |
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
6979
diff
changeset
|
624 |
fun defer_tac i = PRIMITIVE (permute_prems (i-1) 1); |
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
6979
diff
changeset
|
625 |
|
5974 | 626 |
(* remove premises that do not satisfy p; fails if all prems satisfy p *) |
627 |
fun filter_prems_tac p = |
|
15531 | 628 |
let fun Then NONE tac = SOME tac |
629 |
| Then (SOME tac) tac' = SOME(tac THEN' tac'); |
|
5974 | 630 |
fun thins ((tac,n),H) = |
631 |
if p H then (tac,n+1) |
|
632 |
else (Then tac (rotate_tac n THEN' etac thin_rl),0); |
|
633 |
in SUBGOAL(fn (subg,n) => |
|
634 |
let val Hs = Logic.strip_assums_hyp subg |
|
15570 | 635 |
in case fst(Library.foldl thins ((NONE,0),Hs)) of |
15531 | 636 |
NONE => no_tac | SOME tac => tac n |
5974 | 637 |
end) |
638 |
end; |
|
639 |
||
11961
e5911a25d094
prove: primitive goal interface for internal use;
wenzelm
parents:
11929
diff
changeset
|
640 |
|
12139 | 641 |
(*meta-level conjunction*) |
642 |
val conj_tac = SUBGOAL (fn (Const ("all", _) $ Abs (_, _, Const ("==>", _) $ |
|
643 |
(Const ("==>", _) $ _ $ (Const ("==>", _) $ _ $ Bound 0)) $ Bound 0), i) => |
|
644 |
(fn st => |
|
645 |
compose_tac (false, Drule.incr_indexes_wrt [] [] [] [st] Drule.conj_intr_thm, 2) i st) |
|
646 |
| _ => no_tac); |
|
647 |
||
648 |
val conjunction_tac = ALLGOALS (REPEAT_ALL_NEW conj_tac); |
|
649 |
||
15874
6236cc88d4b8
added smart_conjunction_tac, prove_multi, prove_multi_standard;
wenzelm
parents:
15797
diff
changeset
|
650 |
fun smart_conjunction_tac 0 = assume_tac 1 |
6236cc88d4b8
added smart_conjunction_tac, prove_multi, prove_multi_standard;
wenzelm
parents:
15797
diff
changeset
|
651 |
| smart_conjunction_tac _ = TRY conjunction_tac; |
6236cc88d4b8
added smart_conjunction_tac, prove_multi, prove_multi_standard;
wenzelm
parents:
15797
diff
changeset
|
652 |
|
12139 | 653 |
|
654 |
||
15874
6236cc88d4b8
added smart_conjunction_tac, prove_multi, prove_multi_standard;
wenzelm
parents:
15797
diff
changeset
|
655 |
(** minimal goal interface for programmed proofs *) |
11961
e5911a25d094
prove: primitive goal interface for internal use;
wenzelm
parents:
11929
diff
changeset
|
656 |
|
15874
6236cc88d4b8
added smart_conjunction_tac, prove_multi, prove_multi_standard;
wenzelm
parents:
15797
diff
changeset
|
657 |
fun prove_multi sign xs asms props tac = |
11961
e5911a25d094
prove: primitive goal interface for internal use;
wenzelm
parents:
11929
diff
changeset
|
658 |
let |
15874
6236cc88d4b8
added smart_conjunction_tac, prove_multi, prove_multi_standard;
wenzelm
parents:
15797
diff
changeset
|
659 |
val prop = Logic.mk_conjunction_list props; |
11961
e5911a25d094
prove: primitive goal interface for internal use;
wenzelm
parents:
11929
diff
changeset
|
660 |
val statement = Logic.list_implies (asms, prop); |
e5911a25d094
prove: primitive goal interface for internal use;
wenzelm
parents:
11929
diff
changeset
|
661 |
val frees = map Term.dest_Free (Term.term_frees statement); |
11970 | 662 |
val fixed_frees = filter_out (fn (x, _) => x mem_string xs) frees; |
15797 | 663 |
val fixed_tfrees = foldr Term.add_typ_tfrees [] (map #2 fixed_frees); |
15570 | 664 |
val params = List.mapPartial (fn x => Option.map (pair x) (assoc_string (frees, x))) xs; |
11961
e5911a25d094
prove: primitive goal interface for internal use;
wenzelm
parents:
11929
diff
changeset
|
665 |
|
12212 | 666 |
fun err msg = raise ERROR_MESSAGE |
667 |
(msg ^ "\nThe error(s) above occurred for the goal statement:\n" ^ |
|
668 |
Sign.string_of_term sign (Term.list_all_free (params, statement))); |
|
11961
e5911a25d094
prove: primitive goal interface for internal use;
wenzelm
parents:
11929
diff
changeset
|
669 |
|
12170 | 670 |
fun cert_safe t = Thm.cterm_of sign (Envir.beta_norm t) |
11961
e5911a25d094
prove: primitive goal interface for internal use;
wenzelm
parents:
11929
diff
changeset
|
671 |
handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg; |
e5911a25d094
prove: primitive goal interface for internal use;
wenzelm
parents:
11929
diff
changeset
|
672 |
|
e5911a25d094
prove: primitive goal interface for internal use;
wenzelm
parents:
11929
diff
changeset
|
673 |
val _ = cert_safe statement; |
11974 | 674 |
val _ = Term.no_dummy_patterns statement handle TERM (msg, _) => err msg; |
11961
e5911a25d094
prove: primitive goal interface for internal use;
wenzelm
parents:
11929
diff
changeset
|
675 |
|
11974 | 676 |
val cparams = map (cert_safe o Free) params; |
11961
e5911a25d094
prove: primitive goal interface for internal use;
wenzelm
parents:
11929
diff
changeset
|
677 |
val casms = map cert_safe asms; |
12801 | 678 |
val prems = map (norm_hhf_rule o Thm.assume) casms; |
11961
e5911a25d094
prove: primitive goal interface for internal use;
wenzelm
parents:
11929
diff
changeset
|
679 |
val goal = Drule.mk_triv_goal (cert_safe prop); |
e5911a25d094
prove: primitive goal interface for internal use;
wenzelm
parents:
11929
diff
changeset
|
680 |
|
e5911a25d094
prove: primitive goal interface for internal use;
wenzelm
parents:
11929
diff
changeset
|
681 |
val goal' = |
15531 | 682 |
(case Seq.pull (tac prems goal) of SOME (goal', _) => goal' | _ => err "Tactic failed."); |
11961
e5911a25d094
prove: primitive goal interface for internal use;
wenzelm
parents:
11929
diff
changeset
|
683 |
val ngoals = Thm.nprems_of goal'; |
15874
6236cc88d4b8
added smart_conjunction_tac, prove_multi, prove_multi_standard;
wenzelm
parents:
15797
diff
changeset
|
684 |
val _ = conditional (ngoals <> 0) (fn () => |
6236cc88d4b8
added smart_conjunction_tac, prove_multi, prove_multi_standard;
wenzelm
parents:
15797
diff
changeset
|
685 |
err ("Proof failed.\n" ^ |
6236cc88d4b8
added smart_conjunction_tac, prove_multi, prove_multi_standard;
wenzelm
parents:
15797
diff
changeset
|
686 |
Pretty.string_of (Pretty.chunks (Display.pretty_goals ngoals goal')) ^ |
6236cc88d4b8
added smart_conjunction_tac, prove_multi, prove_multi_standard;
wenzelm
parents:
15797
diff
changeset
|
687 |
("\n" ^ string_of_int ngoals ^ " unsolved goal(s)!"))); |
6236cc88d4b8
added smart_conjunction_tac, prove_multi, prove_multi_standard;
wenzelm
parents:
15797
diff
changeset
|
688 |
|
11961
e5911a25d094
prove: primitive goal interface for internal use;
wenzelm
parents:
11929
diff
changeset
|
689 |
val raw_result = goal' RS Drule.rev_triv_goal; |
12801 | 690 |
val prop' = prop_of raw_result; |
15874
6236cc88d4b8
added smart_conjunction_tac, prove_multi, prove_multi_standard;
wenzelm
parents:
15797
diff
changeset
|
691 |
val _ = conditional (not (Pattern.matches (Sign.tsig_of sign) (prop, prop'))) (fn () => |
6236cc88d4b8
added smart_conjunction_tac, prove_multi, prove_multi_standard;
wenzelm
parents:
15797
diff
changeset
|
692 |
err ("Proved a different theorem: " ^ Sign.string_of_term sign prop')); |
11961
e5911a25d094
prove: primitive goal interface for internal use;
wenzelm
parents:
11929
diff
changeset
|
693 |
in |
15874
6236cc88d4b8
added smart_conjunction_tac, prove_multi, prove_multi_standard;
wenzelm
parents:
15797
diff
changeset
|
694 |
Drule.conj_elim_precise (length props) raw_result |
6236cc88d4b8
added smart_conjunction_tac, prove_multi, prove_multi_standard;
wenzelm
parents:
15797
diff
changeset
|
695 |
|> map (fn res => res |
11961
e5911a25d094
prove: primitive goal interface for internal use;
wenzelm
parents:
11929
diff
changeset
|
696 |
|> Drule.implies_intr_list casms |
11974 | 697 |
|> Drule.forall_intr_list cparams |
12801 | 698 |
|> norm_hhf_rule |
12498 | 699 |
|> (#1 o Thm.varifyT' fixed_tfrees) |
15874
6236cc88d4b8
added smart_conjunction_tac, prove_multi, prove_multi_standard;
wenzelm
parents:
15797
diff
changeset
|
700 |
|> Drule.zero_var_indexes) |
11961
e5911a25d094
prove: primitive goal interface for internal use;
wenzelm
parents:
11929
diff
changeset
|
701 |
end; |
e5911a25d094
prove: primitive goal interface for internal use;
wenzelm
parents:
11929
diff
changeset
|
702 |
|
15874
6236cc88d4b8
added smart_conjunction_tac, prove_multi, prove_multi_standard;
wenzelm
parents:
15797
diff
changeset
|
703 |
fun prove_multi_standard sign xs asms prop tac = |
6236cc88d4b8
added smart_conjunction_tac, prove_multi, prove_multi_standard;
wenzelm
parents:
15797
diff
changeset
|
704 |
map Drule.standard (prove_multi sign xs asms prop tac); |
6236cc88d4b8
added smart_conjunction_tac, prove_multi, prove_multi_standard;
wenzelm
parents:
15797
diff
changeset
|
705 |
|
6236cc88d4b8
added smart_conjunction_tac, prove_multi, prove_multi_standard;
wenzelm
parents:
15797
diff
changeset
|
706 |
fun prove sign xs asms prop tac = hd (prove_multi sign xs asms [prop] tac); |
11970 | 707 |
fun prove_standard sign xs asms prop tac = Drule.standard (prove sign xs asms prop tac); |
708 |
||
0 | 709 |
end; |
1501 | 710 |
|
11774 | 711 |
structure BasicTactic: BASIC_TACTIC = Tactic; |
712 |
open BasicTactic; |