1 (* Title: Pure/tactic.ML |
1 (* Title: Pure/tactic.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1991 University of Cambridge |
4 Copyright 1991 University of Cambridge |
5 |
5 |
6 Tactics |
6 Tactics. |
7 *) |
7 *) |
8 |
8 |
9 signature TACTIC = |
9 signature TACTIC = |
10 sig |
10 sig |
11 val ares_tac : thm list -> int -> tactic |
11 val ares_tac : thm list -> int -> tactic |
12 val asm_rewrite_goal_tac: |
12 val asm_rewrite_goal_tac: |
13 bool*bool*bool -> (meta_simpset -> tactic) -> meta_simpset -> int -> tactic |
13 bool*bool*bool -> (meta_simpset -> tactic) -> meta_simpset -> int -> tactic |
14 val assume_tac : int -> tactic |
14 val assume_tac : int -> tactic |
15 val atac : int ->tactic |
15 val atac : int ->tactic |
16 val bimatch_from_nets_tac: |
16 val bimatch_from_nets_tac: |
17 (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic |
17 (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic |
18 val bimatch_tac : (bool*thm)list -> int -> tactic |
18 val bimatch_tac : (bool*thm)list -> int -> tactic |
19 val biresolution_from_nets_tac: |
19 val biresolution_from_nets_tac: |
20 ('a list -> (bool * thm) list) -> |
20 ('a list -> (bool * thm) list) -> |
21 bool -> 'a Net.net * 'a Net.net -> int -> tactic |
21 bool -> 'a Net.net * 'a Net.net -> int -> tactic |
22 val biresolve_from_nets_tac: |
22 val biresolve_from_nets_tac: |
23 (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic |
23 (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic |
24 val biresolve_tac : (bool*thm)list -> int -> tactic |
24 val biresolve_tac : (bool*thm)list -> int -> tactic |
25 val build_net : thm list -> (int*thm) Net.net |
25 val build_net : thm list -> (int*thm) Net.net |
26 val build_netpair: (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> |
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 |
27 (bool*thm)list -> (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net |
28 val compose_inst_tac : (string*string)list -> (bool*thm*int) -> |
28 val compose_inst_tac : (string*string)list -> (bool*thm*int) -> |
29 int -> tactic |
29 int -> tactic |
30 val compose_tac : (bool * thm * int) -> int -> tactic |
30 val compose_tac : (bool * thm * int) -> int -> tactic |
31 val cut_facts_tac : thm list -> int -> tactic |
31 val cut_facts_tac : thm list -> int -> tactic |
32 val cut_inst_tac : (string*string)list -> thm -> int -> tactic |
32 val cut_inst_tac : (string*string)list -> thm -> int -> tactic |
33 val datac : thm -> int -> int -> tactic |
33 val datac : thm -> int -> int -> tactic |
34 val defer_tac : int -> tactic |
34 val defer_tac : int -> tactic |
35 val distinct_subgoals_tac : tactic |
35 val distinct_subgoals_tac : tactic |
36 val dmatch_tac : thm list -> int -> tactic |
36 val dmatch_tac : thm list -> int -> tactic |
37 val dresolve_tac : thm list -> int -> tactic |
37 val dresolve_tac : thm list -> int -> tactic |
38 val dres_inst_tac : (string*string)list -> thm -> int -> tactic |
38 val dres_inst_tac : (string*string)list -> thm -> int -> tactic |
39 val dtac : thm -> int ->tactic |
39 val dtac : thm -> int ->tactic |
40 val eatac : thm -> int -> int -> tactic |
40 val eatac : thm -> int -> int -> tactic |
41 val etac : thm -> int ->tactic |
41 val etac : thm -> int ->tactic |
42 val eq_assume_tac : int -> tactic |
42 val eq_assume_tac : int -> tactic |
43 val ematch_tac : thm list -> int -> tactic |
43 val ematch_tac : thm list -> int -> tactic |
44 val eresolve_tac : thm list -> int -> tactic |
44 val eresolve_tac : thm list -> int -> tactic |
45 val eres_inst_tac : (string*string)list -> thm -> int -> tactic |
45 val eres_inst_tac : (string*string)list -> thm -> int -> tactic |
46 val fatac : thm -> int -> int -> tactic |
46 val fatac : thm -> int -> int -> tactic |
47 val filter_prems_tac : (term -> bool) -> int -> tactic |
47 val filter_prems_tac : (term -> bool) -> int -> tactic |
48 val filter_thms : (term*term->bool) -> int*term*thm list -> thm list |
48 val filter_thms : (term*term->bool) -> int*term*thm list -> thm list |
49 val filt_resolve_tac : thm list -> int -> int -> tactic |
49 val filt_resolve_tac : thm list -> int -> int -> tactic |
50 val flexflex_tac : tactic |
50 val flexflex_tac : tactic |
51 val fold_goals_tac : thm list -> tactic |
51 val fold_goals_tac : thm list -> tactic |
52 val fold_rule : thm list -> thm -> thm |
52 val fold_rule : thm list -> thm -> thm |
53 val fold_tac : thm list -> tactic |
53 val fold_tac : thm list -> tactic |
54 val forward_tac : thm list -> int -> tactic |
54 val forward_tac : thm list -> int -> tactic |
55 val forw_inst_tac : (string*string)list -> thm -> int -> tactic |
55 val forw_inst_tac : (string*string)list -> thm -> int -> tactic |
56 val ftac : thm -> int ->tactic |
56 val ftac : thm -> int ->tactic |
57 val insert_tagged_brl : ('a*(bool*thm)) * |
57 val insert_tagged_brl : ('a*(bool*thm)) * |
58 (('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net) -> |
58 (('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net) -> |
59 ('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net |
59 ('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net |
60 val delete_tagged_brl : (bool*thm) * |
60 val delete_tagged_brl : (bool*thm) * |
61 ((int*(bool*thm))Net.net * (int*(bool*thm))Net.net) -> |
61 ((int*(bool*thm))Net.net * (int*(bool*thm))Net.net) -> |
62 (int*(bool*thm))Net.net * (int*(bool*thm))Net.net |
62 (int*(bool*thm))Net.net * (int*(bool*thm))Net.net |
63 val is_fact : thm -> bool |
63 val is_fact : thm -> bool |
64 val lessb : (bool * thm) * (bool * thm) -> bool |
64 val lessb : (bool * thm) * (bool * thm) -> bool |
65 val lift_inst_rule : thm * int * (string*string)list * thm -> thm |
65 val lift_inst_rule : thm * int * (string*string)list * thm -> thm |
66 val make_elim : thm -> thm |
66 val make_elim : thm -> thm |
67 val match_from_net_tac : (int*thm) Net.net -> int -> tactic |
67 val match_from_net_tac : (int*thm) Net.net -> int -> tactic |
68 val match_tac : thm list -> int -> tactic |
68 val match_tac : thm list -> int -> tactic |
69 val metacut_tac : thm -> int -> tactic |
69 val metacut_tac : thm -> int -> tactic |
70 val net_bimatch_tac : (bool*thm) list -> int -> tactic |
70 val net_bimatch_tac : (bool*thm) list -> int -> tactic |
71 val net_biresolve_tac : (bool*thm) list -> int -> tactic |
71 val net_biresolve_tac : (bool*thm) list -> int -> tactic |
72 val net_match_tac : thm list -> int -> tactic |
72 val net_match_tac : thm list -> int -> tactic |
73 val net_resolve_tac : thm list -> int -> tactic |
73 val net_resolve_tac : thm list -> int -> tactic |
74 val orderlist : (int * 'a) list -> 'a list |
74 val norm_hhf : thm -> thm |
75 val PRIMITIVE : (thm -> thm) -> tactic |
75 val norm_hhf_tac : int -> tactic |
76 val PRIMSEQ : (thm -> thm Seq.seq) -> tactic |
76 val orderlist : (int * 'a) list -> 'a list |
77 val prune_params_tac : tactic |
77 val PRIMITIVE : (thm -> thm) -> tactic |
78 val rename_params_tac : string list -> int -> tactic |
78 val PRIMSEQ : (thm -> thm Seq.seq) -> tactic |
79 val rename_tac : string -> int -> tactic |
79 val prune_params_tac : tactic |
80 val rename_last_tac : string -> string list -> int -> tactic |
80 val rename_params_tac : string list -> int -> tactic |
81 val resolve_from_net_tac : (int*thm) Net.net -> int -> tactic |
81 val rename_tac : string -> int -> tactic |
82 val resolve_tac : thm list -> int -> tactic |
82 val rename_last_tac : string -> string list -> int -> tactic |
83 val res_inst_tac : (string*string)list -> thm -> int -> tactic |
83 val resolve_from_net_tac : (int*thm) Net.net -> int -> tactic |
|
84 val resolve_tac : thm list -> int -> tactic |
|
85 val res_inst_tac : (string*string)list -> thm -> int -> tactic |
84 val rewrite_goal_tac : thm list -> int -> tactic |
86 val rewrite_goal_tac : thm list -> int -> tactic |
85 val rewrite_goals_rule: thm list -> thm -> thm |
87 val rewrite_goals_rule: thm list -> thm -> thm |
86 val rewrite_rule : thm list -> thm -> thm |
88 val rewrite_rule : thm list -> thm -> thm |
87 val rewrite_goals_tac : thm list -> tactic |
89 val rewrite_goals_tac : thm list -> tactic |
88 val rewrite_tac : thm list -> tactic |
90 val rewrite_tac : thm list -> tactic |
89 val rewtac : thm -> tactic |
91 val rewtac : thm -> tactic |
90 val rotate_tac : int -> int -> tactic |
92 val rotate_tac : int -> int -> tactic |
91 val rtac : thm -> int -> tactic |
93 val rtac : thm -> int -> tactic |
92 val rule_by_tactic : tactic -> thm -> thm |
94 val rule_by_tactic : tactic -> thm -> thm |
93 val solve_tac : thm list -> int -> tactic |
95 val solve_tac : thm list -> int -> tactic |
94 val subgoal_tac : string -> int -> tactic |
96 val subgoal_tac : string -> int -> tactic |
95 val subgoals_tac : string list -> int -> tactic |
97 val subgoals_tac : string list -> int -> tactic |
96 val subgoals_of_brl : bool * thm -> int |
98 val subgoals_of_brl : bool * thm -> int |
97 val term_lift_inst_rule : |
99 val term_lift_inst_rule : |
98 thm * int * (indexname*typ)list * ((indexname*typ)*term)list * thm |
100 thm * int * (indexname*typ)list * ((indexname*typ)*term)list * thm |
99 -> thm |
101 -> thm |
100 val instantiate_tac : (string * string) list -> tactic |
102 val instantiate_tac : (string * string) list -> tactic |
101 val thin_tac : string -> int -> tactic |
103 val thin_tac : string -> int -> tactic |
102 val trace_goalno_tac : (int -> tactic) -> int -> tactic |
104 val trace_goalno_tac : (int -> tactic) -> int -> tactic |
103 end; |
105 end; |
104 |
106 |
105 |
107 |
106 structure Tactic : TACTIC = |
108 structure Tactic : TACTIC = |
107 struct |
109 struct |
108 |
110 |
109 (*Discover which goal is chosen: SOMEGOAL(trace_goalno_tac tac) *) |
111 (*Discover which goal is chosen: SOMEGOAL(trace_goalno_tac tac) *) |
110 fun trace_goalno_tac tac i st = |
112 fun trace_goalno_tac tac i st = |
111 case Seq.pull(tac i st) of |
113 case Seq.pull(tac i st) of |
112 None => Seq.empty |
114 None => Seq.empty |
113 | seqcell => (writeln ("Subgoal " ^ string_of_int i ^ " selected"); |
115 | seqcell => (writeln ("Subgoal " ^ string_of_int i ^ " selected"); |
114 Seq.make(fn()=> seqcell)); |
116 Seq.make(fn()=> seqcell)); |
115 |
117 |
116 (*Makes a rule by applying a tactic to an existing rule*) |
118 (*Makes a rule by applying a tactic to an existing rule*) |
117 fun rule_by_tactic tac rl = |
119 fun rule_by_tactic tac rl = |
118 let val (st, thaw) = freeze_thaw (zero_var_indexes rl) |
120 let val (st, thaw) = freeze_thaw (zero_var_indexes rl) |
119 in case Seq.pull (tac st) of |
121 in case Seq.pull (tac st) of |
120 None => raise THM("rule_by_tactic", 0, [rl]) |
122 None => raise THM("rule_by_tactic", 0, [rl]) |
121 | Some(st',_) => Thm.varifyT (thaw st') |
123 | Some(st',_) => Thm.varifyT (thaw st') |
122 end; |
124 end; |
123 |
125 |
124 (*** Basic tactics ***) |
126 (*** Basic tactics ***) |
125 |
127 |
192 local |
194 local |
193 fun cterm_aconv (a,b) = #t (rep_cterm a) aconv #t (rep_cterm b); |
195 fun cterm_aconv (a,b) = #t (rep_cterm a) aconv #t (rep_cterm b); |
194 in |
196 in |
195 fun distinct_subgoals_tac state = |
197 fun distinct_subgoals_tac state = |
196 let val (frozth,thawfn) = freeze_thaw state |
198 let val (frozth,thawfn) = freeze_thaw state |
197 val froz_prems = cprems_of frozth |
199 val froz_prems = cprems_of frozth |
198 val assumed = implies_elim_list frozth (map assume froz_prems) |
200 val assumed = implies_elim_list frozth (map assume froz_prems) |
199 val implied = implies_intr_list (gen_distinct cterm_aconv froz_prems) |
201 val implied = implies_intr_list (gen_distinct cterm_aconv froz_prems) |
200 assumed; |
202 assumed; |
201 in Seq.single (thawfn implied) end |
203 in Seq.single (thawfn implied) end |
202 end; |
204 end; |
203 |
205 |
204 |
206 |
205 (*Lift and instantiate a rule wrt the given state and subgoal number *) |
207 (*Lift and instantiate a rule wrt the given state and subgoal number *) |
206 fun lift_inst_rule (st, i, sinsts, rule) = |
208 fun lift_inst_rule (st, i, sinsts, rule) = |
207 let val {maxidx,sign,...} = rep_thm st |
209 let val {maxidx,sign,...} = rep_thm st |
208 val (_, _, Bi, _) = dest_state(st,i) |
210 val (_, _, Bi, _) = dest_state(st,i) |
209 val params = Logic.strip_params Bi (*params of subgoal i*) |
211 val params = Logic.strip_params Bi (*params of subgoal i*) |
210 val params = rev(rename_wrt_term Bi params) (*as they are printed*) |
212 val params = rev(rename_wrt_term Bi params) (*as they are printed*) |
211 val paramTs = map #2 params |
213 val paramTs = map #2 params |
212 and inc = maxidx+1 |
214 and inc = maxidx+1 |
213 fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs---> incr_tvar inc T) |
215 fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs---> incr_tvar inc T) |
214 | liftvar t = raise TERM("Variable expected", [t]); |
216 | liftvar t = raise TERM("Variable expected", [t]); |
215 fun liftterm t = list_abs_free (params, |
217 fun liftterm t = list_abs_free (params, |
216 Logic.incr_indexes(paramTs,inc) t) |
218 Logic.incr_indexes(paramTs,inc) t) |
217 (*Lifts instantiation pair over params*) |
219 (*Lifts instantiation pair over params*) |
218 fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct) |
220 fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct) |
219 fun lifttvar((a,i),ctyp) = |
221 fun lifttvar((a,i),ctyp) = |
220 let val {T,sign} = rep_ctyp ctyp |
222 let val {T,sign} = rep_ctyp ctyp |
221 in ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end |
223 in ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end |
222 val rts = types_sorts rule and (types,sorts) = types_sorts st |
224 val rts = types_sorts rule and (types,sorts) = types_sorts st |
223 fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm) |
225 fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm) |
224 | types'(ixn) = types ixn; |
226 | types'(ixn) = types ixn; |
225 val used = add_term_tvarnames |
227 val used = add_term_tvarnames |
226 (#prop(rep_thm st) $ #prop(rep_thm rule),[]) |
228 (#prop(rep_thm st) $ #prop(rep_thm rule),[]) |