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 -> (meta_simpset -> tactic) -> meta_simpset -> int -> tactic |
13 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 biresolve_from_nets_tac: |
19 val biresolve_from_nets_tac: |
20 (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic |
20 (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic |
21 val biresolve_tac: (bool*thm)list -> int -> tactic |
21 val biresolve_tac : (bool*thm)list -> int -> tactic |
22 val build_net: thm list -> (int*thm) Net.net |
22 val build_net : thm list -> (int*thm) Net.net |
23 val build_netpair: (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> |
23 val build_netpair: (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> |
24 (bool*thm)list -> (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net |
24 (bool*thm)list -> (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net |
25 val compose_inst_tac: (string*string)list -> (bool*thm*int) -> int -> tactic |
25 val compose_inst_tac : (string*string)list -> (bool*thm*int) -> |
26 val compose_tac: (bool * thm * int) -> int -> tactic |
26 int -> tactic |
27 val cut_facts_tac: thm list -> int -> tactic |
27 val compose_tac : (bool * thm * int) -> int -> tactic |
28 val cut_inst_tac: (string*string)list -> thm -> int -> tactic |
28 val cut_facts_tac : thm list -> int -> tactic |
29 val defer_tac : int -> tactic |
29 val cut_inst_tac : (string*string)list -> thm -> int -> tactic |
30 val dmatch_tac: thm list -> int -> tactic |
30 val defer_tac : int -> tactic |
31 val dresolve_tac: thm list -> int -> tactic |
31 val distinct_subgoals_tac : tactic |
32 val dres_inst_tac: (string*string)list -> thm -> int -> tactic |
32 val dmatch_tac : thm list -> int -> tactic |
33 val dtac: thm -> int ->tactic |
33 val dresolve_tac : thm list -> int -> tactic |
34 val etac: thm -> int ->tactic |
34 val dres_inst_tac : (string*string)list -> thm -> int -> tactic |
35 val eq_assume_tac: int -> tactic |
35 val dtac : thm -> int ->tactic |
36 val ematch_tac: thm list -> int -> tactic |
36 val etac : thm -> int ->tactic |
37 val eresolve_tac: thm list -> int -> tactic |
37 val eq_assume_tac : int -> tactic |
38 val eres_inst_tac: (string*string)list -> thm -> int -> tactic |
38 val ematch_tac : thm list -> int -> tactic |
39 val filter_thms: (term*term->bool) -> int*term*thm list -> thm list |
39 val eresolve_tac : thm list -> int -> tactic |
40 val filt_resolve_tac: thm list -> int -> int -> tactic |
40 val eres_inst_tac : (string*string)list -> thm -> int -> tactic |
41 val flexflex_tac: tactic |
41 val filter_thms : (term*term->bool) -> int*term*thm list -> thm list |
42 val fold_goals_tac: thm list -> tactic |
42 val filt_resolve_tac : thm list -> int -> int -> tactic |
43 val fold_tac: thm list -> tactic |
43 val flexflex_tac : tactic |
44 val forward_tac: thm list -> int -> tactic |
44 val fold_goals_tac : thm list -> tactic |
45 val forw_inst_tac: (string*string)list -> thm -> int -> tactic |
45 val fold_tac : thm list -> tactic |
46 val freeze_thaw: thm -> thm * (thm -> thm) |
46 val forward_tac : thm list -> int -> tactic |
47 val insert_tagged_brl: ('a*(bool*thm)) * |
47 val forw_inst_tac : (string*string)list -> thm -> int -> tactic |
48 (('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net) -> |
48 val freeze_thaw : thm -> thm * (thm -> thm) |
49 ('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net |
49 val insert_tagged_brl : ('a*(bool*thm)) * |
50 val delete_tagged_brl: (bool*thm) * |
50 (('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net) -> |
51 ((int*(bool*thm))Net.net * (int*(bool*thm))Net.net) -> |
51 ('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net |
|
52 val delete_tagged_brl : (bool*thm) * |
|
53 ((int*(bool*thm))Net.net * (int*(bool*thm))Net.net) -> |
52 (int*(bool*thm))Net.net * (int*(bool*thm))Net.net |
54 (int*(bool*thm))Net.net * (int*(bool*thm))Net.net |
53 val is_fact: thm -> bool |
55 val is_fact : thm -> bool |
54 val lessb: (bool * thm) * (bool * thm) -> bool |
56 val lessb : (bool * thm) * (bool * thm) -> bool |
55 val lift_inst_rule: thm * int * (string*string)list * thm -> thm |
57 val lift_inst_rule : thm * int * (string*string)list * thm -> thm |
56 val make_elim: thm -> thm |
58 val make_elim : thm -> thm |
57 val match_from_net_tac: (int*thm) Net.net -> int -> tactic |
59 val match_from_net_tac : (int*thm) Net.net -> int -> tactic |
58 val match_tac: thm list -> int -> tactic |
60 val match_tac : thm list -> int -> tactic |
59 val metacut_tac: thm -> int -> tactic |
61 val metacut_tac : thm -> int -> tactic |
60 val net_bimatch_tac: (bool*thm) list -> int -> tactic |
62 val net_bimatch_tac : (bool*thm) list -> int -> tactic |
61 val net_biresolve_tac: (bool*thm) list -> int -> tactic |
63 val net_biresolve_tac : (bool*thm) list -> int -> tactic |
62 val net_match_tac: thm list -> int -> tactic |
64 val net_match_tac : thm list -> int -> tactic |
63 val net_resolve_tac: thm list -> int -> tactic |
65 val net_resolve_tac : thm list -> int -> tactic |
64 val orderlist: (int * 'a) list -> 'a list |
66 val orderlist : (int * 'a) list -> 'a list |
65 val PRIMITIVE: (thm -> thm) -> tactic |
67 val PRIMITIVE : (thm -> thm) -> tactic |
66 val PRIMSEQ: (thm -> thm Sequence.seq) -> tactic |
68 val PRIMSEQ : (thm -> thm Sequence.seq) -> tactic |
67 val prune_params_tac: tactic |
69 val prune_params_tac : tactic |
68 val rename_tac: string -> int -> tactic |
70 val rename_tac : string -> int -> tactic |
69 val rename_last_tac: string -> string list -> int -> tactic |
71 val rename_last_tac : string -> string list -> int -> tactic |
70 val resolve_from_net_tac: (int*thm) Net.net -> int -> tactic |
72 val resolve_from_net_tac : (int*thm) Net.net -> int -> tactic |
71 val resolve_tac: thm list -> int -> tactic |
73 val resolve_tac : thm list -> int -> tactic |
72 val res_inst_tac: (string*string)list -> thm -> int -> tactic |
74 val res_inst_tac : (string*string)list -> thm -> int -> tactic |
73 val rewrite_goals_tac: thm list -> tactic |
75 val rewrite_goals_tac : thm list -> tactic |
74 val rewrite_tac: thm list -> tactic |
76 val rewrite_tac : thm list -> tactic |
75 val rewtac: thm -> tactic |
77 val rewtac : thm -> tactic |
76 val rotate_tac: int -> int -> tactic |
78 val rotate_tac : int -> int -> tactic |
77 val rtac: thm -> int -> tactic |
79 val rtac : thm -> int -> tactic |
78 val rule_by_tactic: tactic -> thm -> thm |
80 val rule_by_tactic : tactic -> thm -> thm |
79 val subgoal_tac: string -> int -> tactic |
81 val subgoal_tac : string -> int -> tactic |
80 val subgoals_tac: string list -> int -> tactic |
82 val subgoals_tac : string list -> int -> tactic |
81 val subgoals_of_brl: bool * thm -> int |
83 val subgoals_of_brl : bool * thm -> int |
82 val term_lift_inst_rule: |
84 val term_lift_inst_rule : |
83 thm * int * (indexname*typ)list * ((indexname*typ)*term)list * thm |
85 thm * int * (indexname*typ)list * ((indexname*typ)*term)list * thm |
84 -> thm |
86 -> thm |
85 val thin_tac: string -> int -> tactic |
87 val thin_tac : string -> int -> tactic |
86 val trace_goalno_tac: (int -> tactic) -> int -> tactic |
88 val trace_goalno_tac : (int -> tactic) -> int -> tactic |
87 end; |
89 end; |
88 |
90 |
89 |
91 |
90 structure Tactic : TACTIC = |
92 structure Tactic : TACTIC = |
91 struct |
93 struct |
97 | seqcell => (prs("Subgoal " ^ string_of_int i ^ " selected\n"); |
99 | seqcell => (prs("Subgoal " ^ string_of_int i ^ " selected\n"); |
98 Sequence.seqof(fn()=> seqcell)); |
100 Sequence.seqof(fn()=> seqcell)); |
99 |
101 |
100 |
102 |
101 (*Convert all Vars in a theorem to Frees. Also return a function for |
103 (*Convert all Vars in a theorem to Frees. Also return a function for |
102 reversing that operation. DOES NOT WORK FOR TYPE VARIABLES.*) |
104 reversing that operation. DOES NOT WORK FOR TYPE VARIABLES. |
103 local |
105 Similar code in type/freeze_thaw*) |
104 fun string_of (a,0) = a |
106 fun freeze_thaw th = |
105 | string_of (a,i) = a ^ "_" ^ string_of_int i; |
107 let val fth = freezeT th |
106 in |
108 val {prop,sign,...} = rep_thm fth |
107 fun freeze_thaw th = |
109 val used = add_term_names (prop, []) |
108 let val fth = freezeT th |
110 and vars = term_vars prop |
109 val vary = variant (add_term_names (#prop(rep_thm fth), [])) |
111 fun newName (Var(ix,_), (pairs,used)) = |
110 val {prop,sign,...} = rep_thm fth |
112 let val v = variant used (string_of_indexname ix) |
111 fun mk_inst (Var(v,T)) = |
113 in ((ix,v)::pairs, v::used) end; |
112 (cterm_of sign (Var(v,T)), |
114 val (alist, _) = foldr newName (vars, ([], used)) |
113 cterm_of sign (Free(vary (string_of v), T))) |
115 fun mk_inst (Var(v,T)) = |
114 val insts = map mk_inst (term_vars prop) |
116 (cterm_of sign (Var(v,T)), |
115 fun thaw th' = |
117 cterm_of sign (Free(the (assoc(alist,v)), T))) |
116 th' |> forall_intr_list (map #2 insts) |
118 val insts = map mk_inst vars |
117 |> forall_elim_list (map #1 insts) |
119 fun thaw th' = |
118 in (instantiate ([],insts) fth, thaw) end; |
120 th' |> forall_intr_list (map #2 insts) |
119 end; |
121 |> forall_elim_list (map #1 insts) |
|
122 in (instantiate ([],insts) fth, thaw) end; |
120 |
123 |
121 |
124 |
122 (*Rotates the given subgoal to be the last. Useful when re-playing |
125 (*Rotates the given subgoal to be the last. Useful when re-playing |
123 an old proof script, when the proof of an early subgoal fails. |
126 an old proof script, when the proof of an early subgoal fails. |
124 DOES NOT WORK FOR TYPE VARIABLES.*) |
127 DOES NOT WORK FOR TYPE VARIABLES.*) |
199 fun ematch_tac rules = bimatch_tac (map (pair true) rules); |
202 fun ematch_tac rules = bimatch_tac (map (pair true) rules); |
200 fun dmatch_tac rls = ematch_tac (map make_elim rls); |
203 fun dmatch_tac rls = ematch_tac (map make_elim rls); |
201 |
204 |
202 (*Smash all flex-flex disagreement pairs in the proof state.*) |
205 (*Smash all flex-flex disagreement pairs in the proof state.*) |
203 val flexflex_tac = PRIMSEQ flexflex_rule; |
206 val flexflex_tac = PRIMSEQ flexflex_rule; |
|
207 |
|
208 |
|
209 (*Remove duplicate subgoals. By Mark Staples*) |
|
210 local |
|
211 fun cterm_aconv (a,b) = #t (rep_cterm a) aconv #t (rep_cterm b); |
|
212 in |
|
213 fun distinct_subgoals_tac state = |
|
214 let val (frozth,thawfn) = freeze_thaw state |
|
215 val froz_prems = cprems_of frozth |
|
216 val assumed = implies_elim_list frozth (map assume froz_prems) |
|
217 val implied = implies_intr_list (gen_distinct cterm_aconv froz_prems) |
|
218 assumed; |
|
219 in Sequence.single (thawfn implied) end |
|
220 end; |
|
221 |
204 |
222 |
205 (*Lift and instantiate a rule wrt the given state and subgoal number *) |
223 (*Lift and instantiate a rule wrt the given state and subgoal number *) |
206 fun lift_inst_rule (st, i, sinsts, rule) = |
224 fun lift_inst_rule (st, i, sinsts, rule) = |
207 let val {maxidx,sign,...} = rep_thm st |
225 let val {maxidx,sign,...} = rep_thm st |
208 val (_, _, Bi, _) = dest_state(st,i) |
226 val (_, _, Bi, _) = dest_state(st,i) |