author | wenzelm |
Mon, 06 Oct 1997 18:22:22 +0200 | |
changeset 3776 | 38f8ec304b95 |
parent 3706 | e57b5902822f |
child 3984 | 8fc76a487616 |
permissions | -rw-r--r-- |
3575
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3554
diff
changeset
|
1 |
(* Title: Pure/tactic.ML |
0 | 2 |
ID: $Id$ |
1460 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1991 University of Cambridge |
5 |
||
6 |
Tactics |
|
7 |
*) |
|
8 |
||
9 |
signature TACTIC = |
|
1501 | 10 |
sig |
3409
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
11 |
val ares_tac : thm list -> int -> tactic |
0 | 12 |
val asm_rewrite_goal_tac: |
214
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
191
diff
changeset
|
13 |
bool*bool -> (meta_simpset -> tactic) -> meta_simpset -> int -> tactic |
3409
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
14 |
val assume_tac : int -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
15 |
val atac : int ->tactic |
670 | 16 |
val bimatch_from_nets_tac: |
1501 | 17 |
(int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic |
3409
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
18 |
val bimatch_tac : (bool*thm)list -> int -> tactic |
3706
e57b5902822f
Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents:
3575
diff
changeset
|
19 |
val biresolution_from_nets_tac: |
e57b5902822f
Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents:
3575
diff
changeset
|
20 |
('a list -> (bool * thm) list) -> |
e57b5902822f
Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents:
3575
diff
changeset
|
21 |
bool -> 'a Net.net * 'a Net.net -> int -> tactic |
670 | 22 |
val biresolve_from_nets_tac: |
1501 | 23 |
(int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic |
3409
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
24 |
val biresolve_tac : (bool*thm)list -> int -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
25 |
val build_net : thm list -> (int*thm) Net.net |
1501 | 26 |
val build_netpair: (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> |
27 |
(bool*thm)list -> (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net |
|
3409
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
28 |
val compose_inst_tac : (string*string)list -> (bool*thm*int) -> |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
29 |
int -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
30 |
val compose_tac : (bool * thm * int) -> int -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
31 |
val cut_facts_tac : thm list -> int -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
32 |
val cut_inst_tac : (string*string)list -> thm -> int -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
33 |
val defer_tac : int -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
34 |
val distinct_subgoals_tac : tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
35 |
val dmatch_tac : thm list -> int -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
36 |
val dresolve_tac : thm list -> int -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
37 |
val dres_inst_tac : (string*string)list -> thm -> int -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
38 |
val dtac : thm -> int ->tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
39 |
val etac : thm -> int ->tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
40 |
val eq_assume_tac : int -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
41 |
val ematch_tac : thm list -> int -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
42 |
val eresolve_tac : thm list -> int -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
43 |
val eres_inst_tac : (string*string)list -> thm -> int -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
44 |
val filter_thms : (term*term->bool) -> int*term*thm list -> thm list |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
45 |
val filt_resolve_tac : thm list -> int -> int -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
46 |
val flexflex_tac : tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
47 |
val fold_goals_tac : thm list -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
48 |
val fold_tac : thm list -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
49 |
val forward_tac : thm list -> int -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
50 |
val forw_inst_tac : (string*string)list -> thm -> int -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
51 |
val freeze_thaw : thm -> thm * (thm -> thm) |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
52 |
val insert_tagged_brl : ('a*(bool*thm)) * |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
53 |
(('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net) -> |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
54 |
('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
55 |
val delete_tagged_brl : (bool*thm) * |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
56 |
((int*(bool*thm))Net.net * (int*(bool*thm))Net.net) -> |
1801 | 57 |
(int*(bool*thm))Net.net * (int*(bool*thm))Net.net |
3409
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
58 |
val is_fact : thm -> bool |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
59 |
val lessb : (bool * thm) * (bool * thm) -> bool |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
60 |
val lift_inst_rule : thm * int * (string*string)list * thm -> thm |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
61 |
val make_elim : thm -> thm |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
62 |
val match_from_net_tac : (int*thm) Net.net -> int -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
63 |
val match_tac : thm list -> int -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
64 |
val metacut_tac : thm -> int -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
65 |
val net_bimatch_tac : (bool*thm) list -> int -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
66 |
val net_biresolve_tac : (bool*thm) list -> int -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
67 |
val net_match_tac : thm list -> int -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
68 |
val net_resolve_tac : thm list -> int -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
69 |
val orderlist : (int * 'a) list -> 'a list |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
70 |
val PRIMITIVE : (thm -> thm) -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
71 |
val PRIMSEQ : (thm -> thm Sequence.seq) -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
72 |
val prune_params_tac : tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
73 |
val rename_tac : string -> int -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
74 |
val rename_last_tac : string -> string list -> int -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
75 |
val resolve_from_net_tac : (int*thm) Net.net -> int -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
76 |
val resolve_tac : thm list -> int -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
77 |
val res_inst_tac : (string*string)list -> thm -> int -> tactic |
3575
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3554
diff
changeset
|
78 |
val rewrite_goals_rule: thm list -> thm -> thm |
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3554
diff
changeset
|
79 |
val rewrite_rule : thm list -> thm -> thm |
3409
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
80 |
val rewrite_goals_tac : thm list -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
81 |
val rewrite_tac : thm list -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
82 |
val rewtac : thm -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
83 |
val rotate_tac : int -> int -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
84 |
val rtac : thm -> int -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
85 |
val rule_by_tactic : tactic -> thm -> thm |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
86 |
val subgoal_tac : string -> int -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
87 |
val subgoals_tac : string list -> int -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
88 |
val subgoals_of_brl : bool * thm -> int |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
89 |
val term_lift_inst_rule : |
1975
eec67972b1bf
renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents:
1966
diff
changeset
|
90 |
thm * int * (indexname*typ)list * ((indexname*typ)*term)list * thm |
eec67972b1bf
renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents:
1966
diff
changeset
|
91 |
-> thm |
3409
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
92 |
val thin_tac : string -> int -> tactic |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
93 |
val trace_goalno_tac : (int -> tactic) -> int -> tactic |
1501 | 94 |
end; |
0 | 95 |
|
96 |
||
1501 | 97 |
structure Tactic : TACTIC = |
0 | 98 |
struct |
99 |
||
1501 | 100 |
(*Discover which goal is chosen: SOMEGOAL(trace_goalno_tac tac) *) |
101 |
fun trace_goalno_tac tac i st = |
|
102 |
case Sequence.pull(tac i st) of |
|
1460 | 103 |
None => Sequence.null |
0 | 104 |
| seqcell => (prs("Subgoal " ^ string_of_int i ^ " selected\n"); |
1501 | 105 |
Sequence.seqof(fn()=> seqcell)); |
0 | 106 |
|
107 |
||
2029 | 108 |
(*Convert all Vars in a theorem to Frees. Also return a function for |
3409
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
109 |
reversing that operation. DOES NOT WORK FOR TYPE VARIABLES. |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
110 |
Similar code in type/freeze_thaw*) |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
111 |
fun freeze_thaw th = |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
112 |
let val fth = freezeT th |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
113 |
val {prop,sign,...} = rep_thm fth |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
114 |
val used = add_term_names (prop, []) |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
115 |
and vars = term_vars prop |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
116 |
fun newName (Var(ix,_), (pairs,used)) = |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
117 |
let val v = variant used (string_of_indexname ix) |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
118 |
in ((ix,v)::pairs, v::used) end; |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
119 |
val (alist, _) = foldr newName (vars, ([], used)) |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
120 |
fun mk_inst (Var(v,T)) = |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
121 |
(cterm_of sign (Var(v,T)), |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
122 |
cterm_of sign (Free(the (assoc(alist,v)), T))) |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
123 |
val insts = map mk_inst vars |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
124 |
fun thaw th' = |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
125 |
th' |> forall_intr_list (map #2 insts) |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
126 |
|> forall_elim_list (map #1 insts) |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
127 |
in (instantiate ([],insts) fth, thaw) end; |
2029 | 128 |
|
129 |
||
130 |
(*Rotates the given subgoal to be the last. Useful when re-playing |
|
131 |
an old proof script, when the proof of an early subgoal fails. |
|
132 |
DOES NOT WORK FOR TYPE VARIABLES.*) |
|
133 |
fun defer_tac i state = |
|
134 |
let val (state',thaw) = freeze_thaw state |
|
135 |
val hyps = Drule.strip_imp_prems (adjust_maxidx (cprop_of state')) |
|
2580
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2228
diff
changeset
|
136 |
val hyp::hyps' = List.drop(hyps, i-1) |
2029 | 137 |
in implies_intr hyp (implies_elim_list state' (map assume hyps)) |
2580
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2228
diff
changeset
|
138 |
|> implies_intr_list (List.take(hyps, i-1) @ hyps') |
2029 | 139 |
|> thaw |
140 |
|> Sequence.single |
|
141 |
end |
|
142 |
handle _ => Sequence.null; |
|
143 |
||
0 | 144 |
|
145 |
(*Makes a rule by applying a tactic to an existing rule*) |
|
1501 | 146 |
fun rule_by_tactic tac rl = |
2688 | 147 |
let val (st, thaw) = freeze_thaw (zero_var_indexes rl) |
148 |
in case Sequence.pull (tac st) of |
|
1460 | 149 |
None => raise THM("rule_by_tactic", 0, [rl]) |
2688 | 150 |
| Some(st',_) => Thm.varifyT (thaw st') |
151 |
end; |
|
0 | 152 |
|
153 |
(*** Basic tactics ***) |
|
154 |
||
155 |
(*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*) |
|
1501 | 156 |
fun PRIMSEQ thmfun st = thmfun st handle THM _ => Sequence.null; |
0 | 157 |
|
158 |
(*Makes a tactic whose effect on a state is given by thmfun: thm->thm.*) |
|
159 |
fun PRIMITIVE thmfun = PRIMSEQ (Sequence.single o thmfun); |
|
160 |
||
161 |
(*** The following fail if the goal number is out of range: |
|
162 |
thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *) |
|
163 |
||
164 |
(*Solve subgoal i by assumption*) |
|
165 |
fun assume_tac i = PRIMSEQ (assumption i); |
|
166 |
||
167 |
(*Solve subgoal i by assumption, using no unification*) |
|
168 |
fun eq_assume_tac i = PRIMITIVE (eq_assumption i); |
|
169 |
||
170 |
(** Resolution/matching tactics **) |
|
171 |
||
172 |
(*The composition rule/state: no lifting or var renaming. |
|
173 |
The arg = (bires_flg, orule, m) ; see bicompose for explanation.*) |
|
174 |
fun compose_tac arg i = PRIMSEQ (bicompose false arg i); |
|
175 |
||
176 |
(*Converts a "destruct" rule like P&Q==>P to an "elimination" rule |
|
177 |
like [| P&Q; P==>R |] ==> R *) |
|
178 |
fun make_elim rl = zero_var_indexes (rl RS revcut_rl); |
|
179 |
||
180 |
(*Attack subgoal i by resolution, using flags to indicate elimination rules*) |
|
181 |
fun biresolve_tac brules i = PRIMSEQ (biresolution false brules i); |
|
182 |
||
183 |
(*Resolution: the simple case, works for introduction rules*) |
|
184 |
fun resolve_tac rules = biresolve_tac (map (pair false) rules); |
|
185 |
||
186 |
(*Resolution with elimination rules only*) |
|
187 |
fun eresolve_tac rules = biresolve_tac (map (pair true) rules); |
|
188 |
||
189 |
(*Forward reasoning using destruction rules.*) |
|
190 |
fun forward_tac rls = resolve_tac (map make_elim rls) THEN' assume_tac; |
|
191 |
||
192 |
(*Like forward_tac, but deletes the assumption after use.*) |
|
193 |
fun dresolve_tac rls = eresolve_tac (map make_elim rls); |
|
194 |
||
195 |
(*Shorthand versions: for resolution with a single theorem*) |
|
1460 | 196 |
fun rtac rl = resolve_tac [rl]; |
197 |
fun etac rl = eresolve_tac [rl]; |
|
198 |
fun dtac rl = dresolve_tac [rl]; |
|
0 | 199 |
val atac = assume_tac; |
200 |
||
201 |
(*Use an assumption or some rules ... A popular combination!*) |
|
202 |
fun ares_tac rules = assume_tac ORELSE' resolve_tac rules; |
|
203 |
||
204 |
(*Matching tactics -- as above, but forbid updating of state*) |
|
205 |
fun bimatch_tac brules i = PRIMSEQ (biresolution true brules i); |
|
206 |
fun match_tac rules = bimatch_tac (map (pair false) rules); |
|
207 |
fun ematch_tac rules = bimatch_tac (map (pair true) rules); |
|
208 |
fun dmatch_tac rls = ematch_tac (map make_elim rls); |
|
209 |
||
210 |
(*Smash all flex-flex disagreement pairs in the proof state.*) |
|
211 |
val flexflex_tac = PRIMSEQ flexflex_rule; |
|
212 |
||
3409
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
213 |
|
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
214 |
(*Remove duplicate subgoals. By Mark Staples*) |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
215 |
local |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
216 |
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
|
217 |
in |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
218 |
fun distinct_subgoals_tac state = |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
219 |
let val (frozth,thawfn) = freeze_thaw state |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
220 |
val froz_prems = cprems_of frozth |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
221 |
val assumed = implies_elim_list frozth (map assume froz_prems) |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
222 |
val implied = implies_intr_list (gen_distinct cterm_aconv froz_prems) |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
223 |
assumed; |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
224 |
in Sequence.single (thawfn implied) end |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
225 |
end; |
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
226 |
|
c0466958df5d
Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents:
2814
diff
changeset
|
227 |
|
0 | 228 |
(*Lift and instantiate a rule wrt the given state and subgoal number *) |
1501 | 229 |
fun lift_inst_rule (st, i, sinsts, rule) = |
230 |
let val {maxidx,sign,...} = rep_thm st |
|
231 |
val (_, _, Bi, _) = dest_state(st,i) |
|
1460 | 232 |
val params = Logic.strip_params Bi (*params of subgoal i*) |
0 | 233 |
val params = rev(rename_wrt_term Bi params) (*as they are printed*) |
234 |
val paramTs = map #2 params |
|
235 |
and inc = maxidx+1 |
|
236 |
fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs---> incr_tvar inc T) |
|
237 |
| liftvar t = raise TERM("Variable expected", [t]); |
|
238 |
fun liftterm t = list_abs_free (params, |
|
1460 | 239 |
Logic.incr_indexes(paramTs,inc) t) |
0 | 240 |
(*Lifts instantiation pair over params*) |
230 | 241 |
fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct) |
0 | 242 |
fun lifttvar((a,i),ctyp) = |
1460 | 243 |
let val {T,sign} = rep_ctyp ctyp |
244 |
in ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end |
|
1501 | 245 |
val rts = types_sorts rule and (types,sorts) = types_sorts st |
0 | 246 |
fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm) |
247 |
| types'(ixn) = types ixn; |
|
949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
947
diff
changeset
|
248 |
val used = add_term_tvarnames |
1501 | 249 |
(#prop(rep_thm st) $ #prop(rep_thm rule),[]) |
949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
947
diff
changeset
|
250 |
val (Tinsts,insts) = read_insts sign rts (types',sorts) used sinsts |
0 | 251 |
in instantiate (map lifttvar Tinsts, map liftpair insts) |
1501 | 252 |
(lift_rule (st,i) rule) |
0 | 253 |
end; |
254 |
||
1966 | 255 |
(*Like lift_inst_rule but takes cterms, not strings. |
256 |
The cterms must be functions of the parameters of the subgoal, |
|
257 |
i.e. they are assumed to be lifted already! |
|
258 |
Also: types of Vars must be fully instantiated already *) |
|
1975
eec67972b1bf
renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents:
1966
diff
changeset
|
259 |
fun term_lift_inst_rule (st, i, Tinsts, insts, rule) = |
1966 | 260 |
let val {maxidx,sign,...} = rep_thm st |
261 |
val (_, _, Bi, _) = dest_state(st,i) |
|
262 |
val params = Logic.strip_params Bi (*params of subgoal i*) |
|
263 |
val paramTs = map #2 params |
|
264 |
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
|
265 |
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
|
266 |
(*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
|
267 |
fun liftpair (v,t) = (cterm_of sign (liftvar v), cterm_of sign t) |
eec67972b1bf
renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents:
1966
diff
changeset
|
268 |
fun liftTpair((a,i),T) = ((a,i+inc), ctyp_of sign (incr_tvar inc T)) |
eec67972b1bf
renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents:
1966
diff
changeset
|
269 |
in instantiate (map liftTpair Tinsts, map liftpair insts) |
1966 | 270 |
(lift_rule (st,i) rule) |
271 |
end; |
|
0 | 272 |
|
273 |
(*** Resolve after lifting and instantation; may refer to parameters of the |
|
274 |
subgoal. Fails if "i" is out of range. ***) |
|
275 |
||
276 |
(*compose version: arguments are as for bicompose.*) |
|
3538 | 277 |
fun compose_inst_tac sinsts (bires_flg, rule, nsubgoal) i st = st |> |
278 |
(compose_tac (bires_flg, lift_inst_rule (st, i, sinsts, rule), nsubgoal) i |
|
279 |
handle TERM (msg,_) => (writeln msg; no_tac) |
|
280 |
| THM (msg,_,_) => (writeln msg; no_tac)); |
|
0 | 281 |
|
761 | 282 |
(*"Resolve" version. Note: res_inst_tac cannot behave sensibly if the |
283 |
terms that are substituted contain (term or type) unknowns from the |
|
284 |
goal, because it is unable to instantiate goal unknowns at the same time. |
|
285 |
||
2029 | 286 |
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
|
287 |
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
|
288 |
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
|
289 |
goals. |
761 | 290 |
*) |
0 | 291 |
fun res_inst_tac sinsts rule i = |
292 |
compose_inst_tac sinsts (false, rule, nprems_of rule) i; |
|
293 |
||
1501 | 294 |
(*eresolve elimination version*) |
0 | 295 |
fun eres_inst_tac sinsts rule i = |
296 |
compose_inst_tac sinsts (true, rule, nprems_of rule) i; |
|
297 |
||
270
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset
|
298 |
(*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
|
299 |
increment revcut_rl instead.*) |
0 | 300 |
fun make_elim_preserve rl = |
270
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset
|
301 |
let val {maxidx,...} = rep_thm rl |
922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
761
diff
changeset
|
302 |
fun cvar ixn = cterm_of Sign.proto_pure (Var(ixn,propT)); |
270
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset
|
303 |
val revcut_rl' = |
1460 | 304 |
instantiate ([], [(cvar("V",0), cvar("V",maxidx+1)), |
305 |
(cvar("W",0), cvar("W",maxidx+1))]) revcut_rl |
|
0 | 306 |
val arg = (false, rl, nprems_of rl) |
307 |
val [th] = Sequence.list_of_s (bicompose false arg 1 revcut_rl') |
|
308 |
in th end |
|
309 |
handle Bind => raise THM("make_elim_preserve", 1, [rl]); |
|
310 |
||
270
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset
|
311 |
(*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
|
312 |
fun cut_inst_tac sinsts rule = res_inst_tac sinsts (make_elim_preserve rule); |
0 | 313 |
|
270
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset
|
314 |
(*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
|
315 |
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
|
316 |
|
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset
|
317 |
(*dresolve tactic applies a RULE to replace an assumption*) |
0 | 318 |
fun dres_inst_tac sinsts rule = eres_inst_tac sinsts (make_elim_preserve rule); |
319 |
||
1951 | 320 |
(*Deletion of an assumption*) |
321 |
fun thin_tac s = eres_inst_tac [("V",s)] thin_rl; |
|
322 |
||
270
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset
|
323 |
(*** Applications of cut_rl ***) |
0 | 324 |
|
325 |
(*Used by metacut_tac*) |
|
326 |
fun bires_cut_tac arg i = |
|
1460 | 327 |
resolve_tac [cut_rl] i THEN biresolve_tac arg (i+1) ; |
0 | 328 |
|
329 |
(*The conclusion of the rule gets assumed in subgoal i, |
|
330 |
while subgoal i+1,... are the premises of the rule.*) |
|
331 |
fun metacut_tac rule = bires_cut_tac [(false,rule)]; |
|
332 |
||
333 |
(*Recognizes theorems that are not rules, but simple propositions*) |
|
334 |
fun is_fact rl = |
|
335 |
case prems_of rl of |
|
1460 | 336 |
[] => true | _::_ => false; |
0 | 337 |
|
338 |
(*"Cut" all facts from theorem list into the goal as assumptions. *) |
|
339 |
fun cut_facts_tac ths i = |
|
340 |
EVERY (map (fn th => metacut_tac th i) (filter is_fact ths)); |
|
341 |
||
342 |
(*Introduce the given proposition as a lemma and subgoal*) |
|
343 |
fun subgoal_tac sprop = res_inst_tac [("psi", sprop)] cut_rl; |
|
344 |
||
439 | 345 |
(*Introduce a list of lemmas and subgoals*) |
346 |
fun subgoals_tac sprops = EVERY' (map subgoal_tac sprops); |
|
347 |
||
0 | 348 |
|
349 |
(**** Indexing and filtering of theorems ****) |
|
350 |
||
351 |
(*Returns the list of potentially resolvable theorems for the goal "prem", |
|
1460 | 352 |
using the predicate could(subgoal,concl). |
0 | 353 |
Resulting list is no longer than "limit"*) |
354 |
fun filter_thms could (limit, prem, ths) = |
|
355 |
let val pb = Logic.strip_assums_concl prem; (*delete assumptions*) |
|
356 |
fun filtr (limit, []) = [] |
|
1460 | 357 |
| filtr (limit, th::ths) = |
358 |
if limit=0 then [] |
|
359 |
else if could(pb, concl_of th) then th :: filtr(limit-1, ths) |
|
360 |
else filtr(limit,ths) |
|
0 | 361 |
in filtr(limit,ths) end; |
362 |
||
363 |
||
364 |
(*** biresolution and resolution using nets ***) |
|
365 |
||
366 |
(** To preserve the order of the rules, tag them with increasing integers **) |
|
367 |
||
368 |
(*insert tags*) |
|
369 |
fun taglist k [] = [] |
|
370 |
| taglist k (x::xs) = (k,x) :: taglist (k+1) xs; |
|
371 |
||
372 |
(*remove tags and suppress duplicates -- list is assumed sorted!*) |
|
373 |
fun untaglist [] = [] |
|
374 |
| untaglist [(k:int,x)] = [x] |
|
375 |
| untaglist ((k,x) :: (rest as (k',x')::_)) = |
|
376 |
if k=k' then untaglist rest |
|
377 |
else x :: untaglist rest; |
|
378 |
||
379 |
(*return list elements in original order*) |
|
2228
f381c1a98209
Eta-expansion of a function definition, for value polymorphism
paulson
parents:
2145
diff
changeset
|
380 |
fun orderlist kbrls = untaglist (sort (fn(x,y)=> #1 x < #1 y) kbrls); |
0 | 381 |
|
382 |
(*insert one tagged brl into the pair of nets*) |
|
1077
c2df11ae8b55
Renamed insert_kbrl to insert_tagged_brl and exported it. Now
lcp
parents:
952
diff
changeset
|
383 |
fun insert_tagged_brl (kbrl as (k,(eres,th)), (inet,enet)) = |
0 | 384 |
if eres then |
1460 | 385 |
case prems_of th of |
386 |
prem::_ => (inet, Net.insert_term ((prem,kbrl), enet, K false)) |
|
387 |
| [] => error"insert_tagged_brl: elimination rule with no premises" |
|
0 | 388 |
else (Net.insert_term ((concl_of th, kbrl), inet, K false), enet); |
389 |
||
390 |
(*build a pair of nets for biresolution*) |
|
670 | 391 |
fun build_netpair netpair brls = |
1077
c2df11ae8b55
Renamed insert_kbrl to insert_tagged_brl and exported it. Now
lcp
parents:
952
diff
changeset
|
392 |
foldr insert_tagged_brl (taglist 1 brls, netpair); |
0 | 393 |
|
1801 | 394 |
(*delete one kbrl from the pair of nets; |
395 |
we don't know the value of k, so we use 0 and ignore it in the comparison*) |
|
396 |
local |
|
397 |
fun eq_kbrl ((k,(eres,th)), (k',(eres',th'))) = eq_thm (th,th') |
|
398 |
in |
|
399 |
fun delete_tagged_brl (brl as (eres,th), (inet,enet)) = |
|
400 |
if eres then |
|
401 |
case prems_of th of |
|
402 |
prem::_ => (inet, Net.delete_term ((prem, (0,brl)), enet, eq_kbrl)) |
|
2814
a318f7f3a65c
delete_tagged_brl just ignores non-elimination rules instead of complaining
paulson
parents:
2688
diff
changeset
|
403 |
| [] => (inet,enet) (*no major premise: ignore*) |
1801 | 404 |
else (Net.delete_term ((concl_of th, (0,brl)), inet, eq_kbrl), enet); |
405 |
end; |
|
406 |
||
407 |
||
3706
e57b5902822f
Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents:
3575
diff
changeset
|
408 |
(*biresolution using a pair of nets rather than rules. |
e57b5902822f
Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents:
3575
diff
changeset
|
409 |
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
|
410 |
boolean "match" indicates matching or unification.*) |
e57b5902822f
Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents:
3575
diff
changeset
|
411 |
fun biresolution_from_nets_tac order match (inet,enet) = |
0 | 412 |
SUBGOAL |
413 |
(fn (prem,i) => |
|
414 |
let val hyps = Logic.strip_assums_hyp prem |
|
415 |
and concl = Logic.strip_assums_concl prem |
|
416 |
val kbrls = Net.unify_term inet concl @ |
|
2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2580
diff
changeset
|
417 |
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
|
418 |
in PRIMSEQ (biresolution match (order kbrls) i) end); |
0 | 419 |
|
3706
e57b5902822f
Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents:
3575
diff
changeset
|
420 |
(*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
|
421 |
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
|
422 |
val bimatch_from_nets_tac = biresolution_from_nets_tac orderlist true; |
0 | 423 |
|
424 |
(*fast versions using nets internally*) |
|
670 | 425 |
val net_biresolve_tac = |
426 |
biresolve_from_nets_tac o build_netpair(Net.empty,Net.empty); |
|
427 |
||
428 |
val net_bimatch_tac = |
|
429 |
bimatch_from_nets_tac o build_netpair(Net.empty,Net.empty); |
|
0 | 430 |
|
431 |
(*** Simpler version for resolve_tac -- only one net, and no hyps ***) |
|
432 |
||
433 |
(*insert one tagged rl into the net*) |
|
434 |
fun insert_krl (krl as (k,th), net) = |
|
435 |
Net.insert_term ((concl_of th, krl), net, K false); |
|
436 |
||
437 |
(*build a net of rules for resolution*) |
|
438 |
fun build_net rls = |
|
439 |
foldr insert_krl (taglist 1 rls, Net.empty); |
|
440 |
||
441 |
(*resolution using a net rather than rules; pred supports filt_resolve_tac*) |
|
442 |
fun filt_resolution_from_net_tac match pred net = |
|
443 |
SUBGOAL |
|
444 |
(fn (prem,i) => |
|
445 |
let val krls = Net.unify_term net (Logic.strip_assums_concl prem) |
|
446 |
in |
|
1460 | 447 |
if pred krls |
0 | 448 |
then PRIMSEQ |
1460 | 449 |
(biresolution match (map (pair false) (orderlist krls)) i) |
0 | 450 |
else no_tac |
451 |
end); |
|
452 |
||
453 |
(*Resolve the subgoal using the rules (making a net) unless too flexible, |
|
454 |
which means more than maxr rules are unifiable. *) |
|
455 |
fun filt_resolve_tac rules maxr = |
|
456 |
let fun pred krls = length krls <= maxr |
|
457 |
in filt_resolution_from_net_tac false pred (build_net rules) end; |
|
458 |
||
459 |
(*versions taking pre-built nets*) |
|
460 |
val resolve_from_net_tac = filt_resolution_from_net_tac false (K true); |
|
461 |
val match_from_net_tac = filt_resolution_from_net_tac true (K true); |
|
462 |
||
463 |
(*fast versions using nets internally*) |
|
464 |
val net_resolve_tac = resolve_from_net_tac o build_net; |
|
465 |
val net_match_tac = match_from_net_tac o build_net; |
|
466 |
||
467 |
||
468 |
(*** For Natural Deduction using (bires_flg, rule) pairs ***) |
|
469 |
||
470 |
(*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
|
471 |
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
|
472 |
| subgoals_of_brl (false,rule) = nprems_of rule; |
0 | 473 |
|
474 |
(*Less-than test: for sorting to minimize number of new subgoals*) |
|
475 |
fun lessb (brl1,brl2) = subgoals_of_brl brl1 < subgoals_of_brl brl2; |
|
476 |
||
477 |
||
478 |
(*** Meta-Rewriting Tactics ***) |
|
479 |
||
480 |
fun result1 tacf mss thm = |
|
3554 | 481 |
apsome fst (Sequence.pull (tacf mss thm)); |
0 | 482 |
|
3575
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3554
diff
changeset
|
483 |
val simple_prover = |
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3554
diff
changeset
|
484 |
result1 (fn mss => ALLGOALS (resolve_tac (prems_of_mss mss))); |
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3554
diff
changeset
|
485 |
|
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3554
diff
changeset
|
486 |
val rewrite_rule = Drule.rewrite_rule_aux simple_prover; |
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3554
diff
changeset
|
487 |
val rewrite_goals_rule = Drule.rewrite_goals_rule_aux simple_prover; |
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3554
diff
changeset
|
488 |
|
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3554
diff
changeset
|
489 |
|
2145 | 490 |
(*Rewrite subgoal i only. SELECT_GOAL avoids inefficiencies in goals_conv.*) |
491 |
fun asm_rewrite_goal_tac mode prover_tac mss = |
|
492 |
SELECT_GOAL |
|
493 |
(PRIMITIVE |
|
494 |
(rewrite_goal_rule mode (result1 prover_tac) mss 1)); |
|
0 | 495 |
|
69
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
496 |
(*Rewrite throughout proof state. *) |
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
497 |
fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs); |
0 | 498 |
|
499 |
(*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
|
500 |
fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs); |
0 | 501 |
|
1460 | 502 |
fun rewtac def = rewrite_goals_tac [def]; |
0 | 503 |
|
504 |
||
1501 | 505 |
(*** 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
|
506 |
|
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
507 |
(*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
|
508 |
fun term_depth (Abs(a,T,t)) = 1 + term_depth t |
2145 | 509 |
| 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
|
510 |
| term_depth _ = 0; |
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
511 |
|
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
512 |
val lhs_of_thm = #1 o Logic.dest_equals o #prop o rep_thm; |
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
513 |
|
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
514 |
(*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
|
515 |
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
|
516 |
fun sort_lhs_depths defs = |
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
517 |
let val keylist = make_keylist (term_depth o lhs_of_thm) defs |
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
518 |
val keys = distinct (sort op> (map #2 keylist)) |
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
519 |
in map (keyfilter keylist) keys end; |
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
520 |
|
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
521 |
fun fold_tac defs = EVERY |
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
522 |
(map rewrite_tac (sort_lhs_depths (map symmetric defs))); |
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
523 |
|
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
524 |
fun fold_goals_tac defs = EVERY |
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
525 |
(map rewrite_goals_tac (sort_lhs_depths (map symmetric defs))); |
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
526 |
|
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
527 |
|
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
528 |
(*** Renaming of parameters in a subgoal |
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset
|
529 |
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
|
530 |
separated by blanks ***) |
0 | 531 |
|
532 |
(*Calling this will generate the warning "Same as previous level" since |
|
533 |
it affects nothing but the names of bound variables!*) |
|
534 |
fun rename_tac str i = |
|
535 |
let val cs = explode str |
|
536 |
in |
|
537 |
if !Logic.auto_rename |
|
538 |
then (writeln"Note: setting Logic.auto_rename := false"; |
|
1460 | 539 |
Logic.auto_rename := false) |
0 | 540 |
else (); |
541 |
case #2 (take_prefix (is_letdig orf is_blank) cs) of |
|
542 |
[] => PRIMITIVE (rename_params_rule (scanwords is_letdig cs, i)) |
|
543 |
| c::_ => error ("Illegal character: " ^ c) |
|
544 |
end; |
|
545 |
||
1501 | 546 |
(*Rename recent parameters using names generated from a and the suffixes, |
547 |
provided the string a, which represents a term, is an identifier. *) |
|
0 | 548 |
fun rename_last_tac a sufs i = |
549 |
let val names = map (curry op^ a) sufs |
|
550 |
in if Syntax.is_identifier a |
|
551 |
then PRIMITIVE (rename_params_rule (names,i)) |
|
552 |
else all_tac |
|
553 |
end; |
|
554 |
||
2043 | 555 |
(*Prunes all redundant parameters from the proof state by rewriting. |
556 |
DOES NOT rewrite main goal, where quantification over an unused bound |
|
557 |
variable is sometimes done to avoid the need for cut_facts_tac.*) |
|
558 |
val prune_params_tac = rewrite_goals_tac [triv_forall_equality]; |
|
0 | 559 |
|
1501 | 560 |
(*rotate_tac n i: rotate the assumptions of subgoal i by n positions, from |
561 |
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
|
562 |
fun rotate_tac 0 i = all_tac |
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2580
diff
changeset
|
563 |
| rotate_tac k i = PRIMITIVE (rotate_rule k i); |
1209 | 564 |
|
0 | 565 |
end; |
1501 | 566 |
|
567 |
open Tactic; |