author | wenzelm |
Fri, 09 Jul 1999 18:54:55 +0200 | |
changeset 6955 | 9e2d97ef55d2 |
parent 6556 | daa00919502b |
child 6967 | a3c163ed1e04 |
permissions | -rw-r--r-- |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
1 |
(* Title: Provers/classical.ML |
0 | 2 |
ID: $Id$ |
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1992 University of Cambridge |
|
5 |
||
6 |
Theorem prover for classical reasoning, including predicate calculus, set |
|
7 |
theory, etc. |
|
8 |
||
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
9 |
Rules must be classified as intr, elim, safe, hazardous (unsafe). |
0 | 10 |
|
11 |
A rule is unsafe unless it can be applied blindly without harmful results. |
|
12 |
For a rule to be safe, its premises and conclusion should be logically |
|
13 |
equivalent. There should be no variables in the premises that are not in |
|
14 |
the conclusion. |
|
15 |
*) |
|
16 |
||
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
17 |
(*higher precedence than := facilitates use of references*) |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
18 |
infix 4 addSIs addSEs addSDs addIs addEs addDs delrules |
4651 | 19 |
addSWrapper delSWrapper addWrapper delWrapper |
5523 | 20 |
addSbefore addSaltern addbefore addaltern |
21 |
addD2 addE2 addSD2 addSE2; |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
22 |
|
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
23 |
|
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
24 |
(*should be a type abbreviation in signature CLASSICAL*) |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
25 |
type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net; |
4651 | 26 |
type wrapper = (int -> tactic) -> (int -> tactic); |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
27 |
|
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
28 |
signature CLASET_THY_DATA = |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
29 |
sig |
5001 | 30 |
val clasetN: string |
31 |
val clasetK: Object.kind |
|
32 |
exception ClasetData of Object.T ref |
|
4854 | 33 |
val setup: (theory -> theory) list |
6556 | 34 |
val fix_methods: Object.T * (Object.T -> Object.T) * (Object.T -> Object.T) * |
5001 | 35 |
(Object.T * Object.T -> Object.T) * (Sign.sg -> Object.T -> unit) -> unit |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
36 |
end; |
2868
17a23a62f82a
New DEEPEN allows giving an upper bound for deepen_tac
paulson
parents:
2813
diff
changeset
|
37 |
|
0 | 38 |
signature CLASSICAL_DATA = |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
39 |
sig |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
40 |
val mp : thm (* [| P-->Q; P |] ==> Q *) |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
41 |
val not_elim : thm (* [| ~P; P |] ==> R *) |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
42 |
val classical : thm (* (~P ==> P) ==> P *) |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
43 |
val sizef : thm -> int (* size function for BEST_FIRST *) |
0 | 44 |
val hyp_subst_tacs: (int -> tactic) list |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
45 |
end; |
0 | 46 |
|
5841 | 47 |
signature BASIC_CLASSICAL = |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
48 |
sig |
0 | 49 |
type claset |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
50 |
val empty_cs: claset |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
51 |
val print_cs: claset -> unit |
4380 | 52 |
val print_claset: theory -> unit |
4653 | 53 |
val rep_cs: (* BLAST_DATA in blast.ML dependent on this *) |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
54 |
claset -> {safeIs: thm list, safeEs: thm list, |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
55 |
hazIs: thm list, hazEs: thm list, |
6955 | 56 |
xtraIs: thm list, xtraEs: thm list, |
4651 | 57 |
swrappers: (string * wrapper) list, |
58 |
uwrappers: (string * wrapper) list, |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
59 |
safe0_netpair: netpair, safep_netpair: netpair, |
6955 | 60 |
haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: netpair} |
1711 | 61 |
val merge_cs : claset * claset -> claset |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
62 |
val addDs : claset * thm list -> claset |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
63 |
val addEs : claset * thm list -> claset |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
64 |
val addIs : claset * thm list -> claset |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
65 |
val addSDs : claset * thm list -> claset |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
66 |
val addSEs : claset * thm list -> claset |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
67 |
val addSIs : claset * thm list -> claset |
1800 | 68 |
val delrules : claset * thm list -> claset |
4651 | 69 |
val addSWrapper : claset * (string * wrapper) -> claset |
70 |
val delSWrapper : claset * string -> claset |
|
71 |
val addWrapper : claset * (string * wrapper) -> claset |
|
72 |
val delWrapper : claset * string -> claset |
|
73 |
val addSbefore : claset * (string * (int -> tactic)) -> claset |
|
74 |
val addSaltern : claset * (string * (int -> tactic)) -> claset |
|
75 |
val addbefore : claset * (string * (int -> tactic)) -> claset |
|
76 |
val addaltern : claset * (string * (int -> tactic)) -> claset |
|
5523 | 77 |
val addD2 : claset * (string * thm) -> claset |
78 |
val addE2 : claset * (string * thm) -> claset |
|
79 |
val addSD2 : claset * (string * thm) -> claset |
|
80 |
val addSE2 : claset * (string * thm) -> claset |
|
4765 | 81 |
val appSWrappers : claset -> wrapper |
4651 | 82 |
val appWrappers : claset -> wrapper |
5927 | 83 |
val trace_rules : bool ref |
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
84 |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
85 |
val claset_ref_of_sg: Sign.sg -> claset ref |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
86 |
val claset_ref_of: theory -> claset ref |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
87 |
val claset_of_sg: Sign.sg -> claset |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
88 |
val claset_of: theory -> claset |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
89 |
val CLASET: (claset -> tactic) -> tactic |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
90 |
val CLASET': (claset -> 'a -> tactic) -> 'a -> tactic |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
91 |
val claset: unit -> claset |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
92 |
val claset_ref: unit -> claset ref |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
93 |
|
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
94 |
val fast_tac : claset -> int -> tactic |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
95 |
val slow_tac : claset -> int -> tactic |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
96 |
val weight_ASTAR : int ref |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
97 |
val astar_tac : claset -> int -> tactic |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
98 |
val slow_astar_tac : claset -> int -> tactic |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
99 |
val best_tac : claset -> int -> tactic |
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
100 |
val slow_best_tac : claset -> int -> tactic |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
101 |
val depth_tac : claset -> int -> int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
102 |
val deepen_tac : claset -> int -> int -> tactic |
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
103 |
|
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
104 |
val contr_tac : int -> tactic |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
105 |
val dup_elim : thm -> thm |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
106 |
val dup_intr : thm -> thm |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
107 |
val dup_step_tac : claset -> int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
108 |
val eq_mp_tac : int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
109 |
val haz_step_tac : claset -> int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
110 |
val joinrules : thm list * thm list -> (bool * thm) list |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
111 |
val mp_tac : int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
112 |
val safe_tac : claset -> tactic |
5757 | 113 |
val safe_steps_tac : claset -> int -> tactic |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
114 |
val safe_step_tac : claset -> int -> tactic |
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
115 |
val clarify_tac : claset -> int -> tactic |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
116 |
val clarify_step_tac : claset -> int -> tactic |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
117 |
val step_tac : claset -> int -> tactic |
2630 | 118 |
val slow_step_tac : claset -> int -> tactic |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
119 |
val swap : thm (* ~P ==> (~Q ==> P) ==> Q *) |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
120 |
val swapify : thm list -> thm list |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
121 |
val swap_res_tac : thm list -> int -> tactic |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
122 |
val inst_step_tac : claset -> int -> tactic |
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
123 |
val inst0_step_tac : claset -> int -> tactic |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
124 |
val instp_step_tac : claset -> int -> tactic |
1724 | 125 |
|
126 |
val AddDs : thm list -> unit |
|
127 |
val AddEs : thm list -> unit |
|
128 |
val AddIs : thm list -> unit |
|
129 |
val AddSDs : thm list -> unit |
|
130 |
val AddSEs : thm list -> unit |
|
131 |
val AddSIs : thm list -> unit |
|
6955 | 132 |
val AddXDs : thm list -> unit |
133 |
val AddXEs : thm list -> unit |
|
134 |
val AddXIs : thm list -> unit |
|
1807 | 135 |
val Delrules : thm list -> unit |
3727
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset
|
136 |
val Safe_tac : tactic |
1814 | 137 |
val Safe_step_tac : int -> tactic |
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
138 |
val Clarify_tac : int -> tactic |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
139 |
val Clarify_step_tac : int -> tactic |
1800 | 140 |
val Step_tac : int -> tactic |
1724 | 141 |
val Fast_tac : int -> tactic |
1800 | 142 |
val Best_tac : int -> tactic |
2066 | 143 |
val Slow_tac : int -> tactic |
144 |
val Slow_best_tac : int -> tactic |
|
1800 | 145 |
val Deepen_tac : int -> int -> tactic |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
146 |
end; |
1724 | 147 |
|
5841 | 148 |
signature CLASSICAL = |
149 |
sig |
|
150 |
include BASIC_CLASSICAL |
|
151 |
val print_local_claset: Proof.context -> unit |
|
152 |
val get_local_claset: Proof.context -> claset |
|
153 |
val put_local_claset: claset -> Proof.context -> Proof.context |
|
154 |
val safe_dest_global: theory attribute |
|
155 |
val safe_elim_global: theory attribute |
|
156 |
val safe_intro_global: theory attribute |
|
6955 | 157 |
val haz_dest_global: theory attribute |
158 |
val haz_elim_global: theory attribute |
|
159 |
val haz_intro_global: theory attribute |
|
160 |
val xtra_dest_global: theory attribute |
|
161 |
val xtra_elim_global: theory attribute |
|
162 |
val xtra_intro_global: theory attribute |
|
5885 | 163 |
val delrule_global: theory attribute |
6955 | 164 |
val safe_dest_local: Proof.context attribute |
165 |
val safe_elim_local: Proof.context attribute |
|
166 |
val safe_intro_local: Proof.context attribute |
|
5885 | 167 |
val haz_dest_local: Proof.context attribute |
168 |
val haz_elim_local: Proof.context attribute |
|
169 |
val haz_intro_local: Proof.context attribute |
|
6955 | 170 |
val xtra_dest_local: Proof.context attribute |
171 |
val xtra_elim_local: Proof.context attribute |
|
172 |
val xtra_intro_local: Proof.context attribute |
|
5885 | 173 |
val delrule_local: Proof.context attribute |
5927 | 174 |
val cla_modifiers: (Args.T list -> (Proof.context attribute * Args.T list)) list |
175 |
val cla_method: (claset -> tactic) -> Args.src -> Proof.context -> Proof.method |
|
176 |
val cla_method': (claset -> int -> tactic) -> Args.src -> Proof.context -> Proof.method |
|
6096 | 177 |
val single_tac: claset -> thm list -> int -> tactic |
5841 | 178 |
val setup: (theory -> theory) list |
179 |
end; |
|
180 |
||
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
181 |
structure ClasetThyData: CLASET_THY_DATA = |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
182 |
struct |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
183 |
|
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
184 |
(* data kind claset -- forward declaration *) |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
185 |
|
5001 | 186 |
val clasetN = "Provers/claset"; |
187 |
val clasetK = Object.kind clasetN; |
|
188 |
exception ClasetData of Object.T ref; |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
189 |
|
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
190 |
local |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
191 |
fun undef _ = raise Match; |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
192 |
|
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
193 |
val empty_ref = ref ERROR; |
6556 | 194 |
val copy_fn = ref (undef: Object.T -> Object.T); |
5001 | 195 |
val prep_ext_fn = ref (undef: Object.T -> Object.T); |
196 |
val merge_fn = ref (undef: Object.T * Object.T -> Object.T); |
|
197 |
val print_fn = ref (undef: Sign.sg -> Object.T -> unit); |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
198 |
|
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
199 |
val empty = ClasetData empty_ref; |
6556 | 200 |
fun copy exn = ! copy_fn exn; |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
201 |
fun prep_ext exn = ! prep_ext_fn exn; |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
202 |
fun merge exn = ! merge_fn exn; |
4259 | 203 |
fun print sg exn = ! print_fn sg exn; |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
204 |
in |
6556 | 205 |
val setup = [Theory.init_data clasetK (empty, copy, prep_ext, merge, print)]; |
206 |
fun fix_methods (e, cp, ext, mrg, prt) = |
|
207 |
(empty_ref := e; copy_fn := cp; prep_ext_fn := ext; merge_fn := mrg; print_fn := prt); |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
208 |
end; |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
209 |
|
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
210 |
|
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
211 |
end; |
0 | 212 |
|
213 |
||
5927 | 214 |
functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = |
0 | 215 |
struct |
216 |
||
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
217 |
local open ClasetThyData Data in |
0 | 218 |
|
1800 | 219 |
(*** Useful tactics for classical reasoning ***) |
0 | 220 |
|
1524 | 221 |
val imp_elim = (*cannot use bind_thm within a structure!*) |
222 |
store_thm ("imp_elim", make_elim mp); |
|
0 | 223 |
|
4392 | 224 |
(*Prove goal that assumes both P and ~P. |
225 |
No backtracking if it finds an equal assumption. Perhaps should call |
|
226 |
ematch_tac instead of eresolve_tac, but then cannot prove ZF/cantor.*) |
|
227 |
val contr_tac = eresolve_tac [not_elim] THEN' |
|
228 |
(eq_assume_tac ORELSE' assume_tac); |
|
0 | 229 |
|
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
230 |
(*Finds P-->Q and P in the assumptions, replaces implication by Q. |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
231 |
Could do the same thing for P<->Q and P... *) |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
232 |
fun mp_tac i = eresolve_tac [not_elim, imp_elim] i THEN assume_tac i; |
0 | 233 |
|
234 |
(*Like mp_tac but instantiates no variables*) |
|
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
235 |
fun eq_mp_tac i = ematch_tac [not_elim, imp_elim] i THEN eq_assume_tac i; |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
236 |
|
1524 | 237 |
val swap = |
238 |
store_thm ("swap", rule_by_tactic (etac thin_rl 1) (not_elim RS classical)); |
|
0 | 239 |
|
240 |
(*Creates rules to eliminate ~A, from rules to introduce A*) |
|
241 |
fun swapify intrs = intrs RLN (2, [swap]); |
|
242 |
||
243 |
(*Uses introduction rules in the normal way, or on negated assumptions, |
|
244 |
trying rules in order. *) |
|
245 |
fun swap_res_tac rls = |
|
54 | 246 |
let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2,swap)) :: brls |
247 |
in assume_tac ORELSE' |
|
248 |
contr_tac ORELSE' |
|
249 |
biresolve_tac (foldr addrl (rls,[])) |
|
0 | 250 |
end; |
251 |
||
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
252 |
(*Duplication of hazardous rules, for complete provers*) |
2689
6d3d893453de
dup_intr & dup_elim no longer call standard -- this
paulson
parents:
2630
diff
changeset
|
253 |
fun dup_intr th = zero_var_indexes (th RS classical); |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
254 |
|
4646 | 255 |
fun dup_elim th = |
256 |
th RSN (2, revcut_rl) |> assumption 2 |> Seq.hd |> |
|
257 |
rule_by_tactic (TRYALL (etac revcut_rl)) |
|
258 |
handle _ => error ("Bad format for elimination rule\n" ^ string_of_thm th); |
|
0 | 259 |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
260 |
|
1800 | 261 |
(**** Classical rule sets ****) |
0 | 262 |
|
263 |
datatype claset = |
|
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
264 |
CS of {safeIs : thm list, (*safe introduction rules*) |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
265 |
safeEs : thm list, (*safe elimination rules*) |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
266 |
hazIs : thm list, (*unsafe introduction rules*) |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
267 |
hazEs : thm list, (*unsafe elimination rules*) |
6955 | 268 |
xtraIs : thm list, (*extra introduction rules*) |
269 |
xtraEs : thm list, (*extra elimination rules*) |
|
4651 | 270 |
swrappers : (string * wrapper) list, (*for transf. safe_step_tac*) |
271 |
uwrappers : (string * wrapper) list, (*for transforming step_tac*) |
|
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
272 |
safe0_netpair : netpair, (*nets for trivial cases*) |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
273 |
safep_netpair : netpair, (*nets for >0 subgoals*) |
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
274 |
haz_netpair : netpair, (*nets for unsafe rules*) |
6955 | 275 |
dup_netpair : netpair, (*nets for duplication*) |
276 |
xtra_netpair : netpair}; (*nets for extra rules*) |
|
0 | 277 |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
278 |
(*Desired invariants are |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
279 |
safe0_netpair = build safe0_brls, |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
280 |
safep_netpair = build safep_brls, |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
281 |
haz_netpair = build (joinrules(hazIs, hazEs)), |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
282 |
dup_netpair = build (joinrules(map dup_intr hazIs, |
6955 | 283 |
map dup_elim hazEs)), |
284 |
xtra_netpair = build (joinrules(xtraIs, xtraEs))} |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
285 |
|
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
286 |
where build = build_netpair(Net.empty,Net.empty), |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
287 |
safe0_brls contains all brules that solve the subgoal, and |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
288 |
safep_brls contains all brules that generate 1 or more new subgoals. |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
289 |
The theorem lists are largely comments, though they are used in merge_cs and print_cs. |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
290 |
Nets must be built incrementally, to save space and time. |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
291 |
*) |
0 | 292 |
|
6502 | 293 |
val empty_netpair = (Net.empty, Net.empty); |
294 |
||
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
295 |
val empty_cs = |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
296 |
CS{safeIs = [], |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
297 |
safeEs = [], |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
298 |
hazIs = [], |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
299 |
hazEs = [], |
6955 | 300 |
xtraIs = [], |
301 |
xtraEs = [], |
|
4651 | 302 |
swrappers = [], |
303 |
uwrappers = [], |
|
6502 | 304 |
safe0_netpair = empty_netpair, |
305 |
safep_netpair = empty_netpair, |
|
306 |
haz_netpair = empty_netpair, |
|
6955 | 307 |
dup_netpair = empty_netpair, |
308 |
xtra_netpair = empty_netpair}; |
|
0 | 309 |
|
6955 | 310 |
fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...}) = |
3546 | 311 |
let val pretty_thms = map Display.pretty_thm in |
312 |
Pretty.writeln (Pretty.big_list "safe introduction rules:" (pretty_thms safeIs)); |
|
4624 | 313 |
Pretty.writeln (Pretty.big_list "unsafe introduction rules:" (pretty_thms hazIs)); |
6955 | 314 |
Pretty.writeln (Pretty.big_list "extra introduction rules:" (pretty_thms xtraIs)); |
4625 | 315 |
Pretty.writeln (Pretty.big_list "safe elimination rules:" (pretty_thms safeEs)); |
6955 | 316 |
Pretty.writeln (Pretty.big_list "unsafe elimination rules:" (pretty_thms hazEs)); |
317 |
Pretty.writeln (Pretty.big_list "extra elimination rules:" (pretty_thms xtraEs)) |
|
3546 | 318 |
end; |
0 | 319 |
|
4653 | 320 |
fun rep_cs (CS args) = args; |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
321 |
|
4651 | 322 |
local |
323 |
fun calc_wrap l tac = foldr (fn ((name,tacf),w) => tacf w) (l, tac); |
|
324 |
in |
|
325 |
fun appSWrappers (CS{swrappers,...}) = calc_wrap swrappers; |
|
326 |
fun appWrappers (CS{uwrappers,...}) = calc_wrap uwrappers; |
|
327 |
end; |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
328 |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
329 |
|
1800 | 330 |
(*** Adding (un)safe introduction or elimination rules. |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
331 |
|
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
332 |
In case of overlap, new rules are tried BEFORE old ones!! |
1800 | 333 |
***) |
0 | 334 |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
335 |
(*For use with biresolve_tac. Combines intr rules with swap to handle negated |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
336 |
assumptions. Pairs elim rules with true. *) |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
337 |
fun joinrules (intrs,elims) = |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
338 |
(map (pair true) (elims @ swapify intrs) @ |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
339 |
map (pair false) intrs); |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
340 |
|
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
341 |
(*Priority: prefer rules with fewest subgoals, |
1231 | 342 |
then rules added most recently (preferring the head of the list).*) |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
343 |
fun tag_brls k [] = [] |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
344 |
| tag_brls k (brl::brls) = |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
345 |
(1000000*subgoals_of_brl brl + k, brl) :: |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
346 |
tag_brls (k+1) brls; |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
347 |
|
1800 | 348 |
fun insert_tagged_list kbrls netpr = foldr insert_tagged_brl (kbrls, netpr); |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
349 |
|
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
350 |
(*Insert into netpair that already has nI intr rules and nE elim rules. |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
351 |
Count the intr rules double (to account for swapify). Negate to give the |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
352 |
new insertions the lowest priority.*) |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
353 |
fun insert (nI,nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules; |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
354 |
|
1800 | 355 |
fun delete_tagged_list brls netpr = foldr delete_tagged_brl (brls, netpr); |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
356 |
|
1800 | 357 |
val delete = delete_tagged_list o joinrules; |
358 |
||
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
359 |
val mem_thm = gen_mem eq_thm |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
360 |
and rem_thm = gen_rem eq_thm; |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
361 |
|
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
362 |
(*Warn if the rule is already present ELSEWHERE in the claset. The addition |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
363 |
is still allowed.*) |
6955 | 364 |
fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...}) = |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
365 |
if mem_thm (th, safeIs) then |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
366 |
warning ("Rule already in claset as Safe Intr\n" ^ string_of_thm th) |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
367 |
else if mem_thm (th, safeEs) then |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
368 |
warning ("Rule already in claset as Safe Elim\n" ^ string_of_thm th) |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
369 |
else if mem_thm (th, hazIs) then |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
370 |
warning ("Rule already in claset as unsafe Intr\n" ^ string_of_thm th) |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
371 |
else if mem_thm (th, hazEs) then |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
372 |
warning ("Rule already in claset as unsafe Elim\n" ^ string_of_thm th) |
6955 | 373 |
else if mem_thm (th, xtraIs) then |
374 |
warning ("Rule already in claset as extra Intr\n" ^ string_of_thm th) |
|
375 |
else if mem_thm (th, xtraEs) then |
|
376 |
warning ("Rule already in claset as extra Elim\n" ^ string_of_thm th) |
|
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
377 |
else (); |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
378 |
|
1800 | 379 |
(*** Safe rules ***) |
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
380 |
|
6955 | 381 |
fun addSI (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, |
382 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, |
|
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
383 |
th) = |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
384 |
if mem_thm (th, safeIs) then |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
385 |
(warning ("Ignoring duplicate Safe Intr\n" ^ string_of_thm th); |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
386 |
cs) |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
387 |
else |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
388 |
let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
389 |
partition (fn rl => nprems_of rl=0) [th] |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
390 |
val nI = length safeIs + 1 |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
391 |
and nE = length safeEs |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
392 |
in warn_dup th cs; |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
393 |
CS{safeIs = th::safeIs, |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
394 |
safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
395 |
safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
396 |
safeEs = safeEs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
397 |
hazIs = hazIs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
398 |
hazEs = hazEs, |
6955 | 399 |
xtraIs = xtraIs, |
400 |
xtraEs = xtraEs, |
|
4651 | 401 |
swrappers = swrappers, |
402 |
uwrappers = uwrappers, |
|
2630 | 403 |
haz_netpair = haz_netpair, |
6955 | 404 |
dup_netpair = dup_netpair, |
405 |
xtra_netpair = xtra_netpair} |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
406 |
end; |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
407 |
|
6955 | 408 |
fun addSE (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, |
409 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, |
|
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
410 |
th) = |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
411 |
if mem_thm (th, safeEs) then |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
412 |
(warning ("Ignoring duplicate Safe Elim\n" ^ string_of_thm th); |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
413 |
cs) |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
414 |
else |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
415 |
let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
416 |
partition (fn rl => nprems_of rl=1) [th] |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
417 |
val nI = length safeIs |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
418 |
and nE = length safeEs + 1 |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
419 |
in warn_dup th cs; |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
420 |
CS{safeEs = th::safeEs, |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
421 |
safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
422 |
safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
423 |
safeIs = safeIs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
424 |
hazIs = hazIs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
425 |
hazEs = hazEs, |
6955 | 426 |
xtraIs = xtraIs, |
427 |
xtraEs = xtraEs, |
|
4651 | 428 |
swrappers = swrappers, |
429 |
uwrappers = uwrappers, |
|
2630 | 430 |
haz_netpair = haz_netpair, |
6955 | 431 |
dup_netpair = dup_netpair, |
432 |
xtra_netpair = xtra_netpair} |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
433 |
end; |
0 | 434 |
|
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
435 |
fun rev_foldl f (e, l) = foldl f (e, rev l); |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
436 |
|
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
437 |
val op addSIs = rev_foldl addSI; |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
438 |
val op addSEs = rev_foldl addSE; |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
439 |
|
0 | 440 |
fun cs addSDs ths = cs addSEs (map make_elim ths); |
441 |
||
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
442 |
|
1800 | 443 |
(*** Hazardous (unsafe) rules ***) |
0 | 444 |
|
6955 | 445 |
fun addI (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, |
446 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, |
|
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
447 |
th)= |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
448 |
if mem_thm (th, hazIs) then |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
449 |
(warning ("Ignoring duplicate unsafe Intr\n" ^ string_of_thm th); |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
450 |
cs) |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
451 |
else |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
452 |
let val nI = length hazIs + 1 |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
453 |
and nE = length hazEs |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
454 |
in warn_dup th cs; |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
455 |
CS{hazIs = th::hazIs, |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
456 |
haz_netpair = insert (nI,nE) ([th], []) haz_netpair, |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
457 |
dup_netpair = insert (nI,nE) (map dup_intr [th], []) dup_netpair, |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
458 |
safeIs = safeIs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
459 |
safeEs = safeEs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
460 |
hazEs = hazEs, |
6955 | 461 |
xtraIs = xtraIs, |
462 |
xtraEs = xtraEs, |
|
4651 | 463 |
swrappers = swrappers, |
464 |
uwrappers = uwrappers, |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
465 |
safe0_netpair = safe0_netpair, |
6955 | 466 |
safep_netpair = safep_netpair, |
467 |
xtra_netpair = xtra_netpair} |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
468 |
end; |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
469 |
|
6955 | 470 |
fun addE (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, |
471 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, |
|
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
472 |
th) = |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
473 |
if mem_thm (th, hazEs) then |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
474 |
(warning ("Ignoring duplicate unsafe Elim\n" ^ string_of_thm th); |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
475 |
cs) |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
476 |
else |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
477 |
let val nI = length hazIs |
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
478 |
and nE = length hazEs + 1 |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
479 |
in warn_dup th cs; |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
480 |
CS{hazEs = th::hazEs, |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
481 |
haz_netpair = insert (nI,nE) ([], [th]) haz_netpair, |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
482 |
dup_netpair = insert (nI,nE) ([], map dup_elim [th]) dup_netpair, |
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
483 |
safeIs = safeIs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
484 |
safeEs = safeEs, |
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
485 |
hazIs = hazIs, |
6955 | 486 |
xtraIs = xtraIs, |
487 |
xtraEs = xtraEs, |
|
4651 | 488 |
swrappers = swrappers, |
489 |
uwrappers = uwrappers, |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
490 |
safe0_netpair = safe0_netpair, |
6955 | 491 |
safep_netpair = safep_netpair, |
492 |
xtra_netpair = xtra_netpair} |
|
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
493 |
end; |
0 | 494 |
|
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
495 |
val op addIs = rev_foldl addI; |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
496 |
val op addEs = rev_foldl addE; |
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
497 |
|
0 | 498 |
fun cs addDs ths = cs addEs (map make_elim ths); |
499 |
||
1073
b3f190995bc9
Recoded addSIs, etc., so that nets are built incrementally
lcp
parents:
1010
diff
changeset
|
500 |
|
6955 | 501 |
(*** Extra (single step) rules ***) |
502 |
||
503 |
fun addXI (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, |
|
504 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, |
|
505 |
th)= |
|
506 |
if mem_thm (th, xtraIs) then |
|
507 |
(warning ("Ignoring duplicate extra Intr\n" ^ string_of_thm th); |
|
508 |
cs) |
|
509 |
else |
|
510 |
let val nI = length xtraIs + 1 |
|
511 |
and nE = length xtraEs |
|
512 |
in warn_dup th cs; |
|
513 |
CS{xtraIs = th::xtraIs, |
|
514 |
xtra_netpair = insert (nI,nE) ([th], []) xtra_netpair, |
|
515 |
safeIs = safeIs, |
|
516 |
safeEs = safeEs, |
|
517 |
hazIs = hazIs, |
|
518 |
hazEs = hazEs, |
|
519 |
xtraEs = xtraEs, |
|
520 |
swrappers = swrappers, |
|
521 |
uwrappers = uwrappers, |
|
522 |
safe0_netpair = safe0_netpair, |
|
523 |
safep_netpair = safep_netpair, |
|
524 |
haz_netpair = haz_netpair, |
|
525 |
dup_netpair = dup_netpair} |
|
526 |
end; |
|
527 |
||
528 |
fun addXE (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, |
|
529 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, |
|
530 |
th) = |
|
531 |
if mem_thm (th, xtraEs) then |
|
532 |
(warning ("Ignoring duplicate extra Elim\n" ^ string_of_thm th); |
|
533 |
cs) |
|
534 |
else |
|
535 |
let val nI = length xtraIs |
|
536 |
and nE = length xtraEs + 1 |
|
537 |
in warn_dup th cs; |
|
538 |
CS{xtraEs = th::xtraEs, |
|
539 |
xtra_netpair = insert (nI,nE) ([], [th]) xtra_netpair, |
|
540 |
safeIs = safeIs, |
|
541 |
safeEs = safeEs, |
|
542 |
hazIs = hazIs, |
|
543 |
hazEs = hazEs, |
|
544 |
xtraIs = xtraIs, |
|
545 |
swrappers = swrappers, |
|
546 |
uwrappers = uwrappers, |
|
547 |
safe0_netpair = safe0_netpair, |
|
548 |
safep_netpair = safep_netpair, |
|
549 |
haz_netpair = haz_netpair, |
|
550 |
dup_netpair = dup_netpair} |
|
551 |
end; |
|
552 |
||
553 |
infix 4 addXIs addXEs addXDs; |
|
554 |
||
555 |
val op addXIs = rev_foldl addXI; |
|
556 |
val op addXEs = rev_foldl addXE; |
|
557 |
||
558 |
fun cs addXDs ths = cs addXEs (map make_elim ths); |
|
559 |
||
560 |
||
1800 | 561 |
(*** Deletion of rules |
562 |
Working out what to delete, requires repeating much of the code used |
|
563 |
to insert. |
|
1927
6f97cb16e453
New classical reasoner: warns of, and ignores, redundant rules.
paulson
parents:
1814
diff
changeset
|
564 |
Separate functions delSI, etc., are not exported; instead delrules |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
565 |
searches in all the lists and chooses the relevant delXX functions. |
1800 | 566 |
***) |
567 |
||
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
568 |
fun delSI th |
6955 | 569 |
(cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, |
570 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
|
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
571 |
if mem_thm (th, safeIs) then |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
572 |
let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=0) [th] |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
573 |
in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair, |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
574 |
safep_netpair = delete (safep_rls, []) safep_netpair, |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
575 |
safeIs = rem_thm (safeIs,th), |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
576 |
safeEs = safeEs, |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
577 |
hazIs = hazIs, |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
578 |
hazEs = hazEs, |
6955 | 579 |
xtraIs = xtraIs, |
580 |
xtraEs = xtraEs, |
|
4651 | 581 |
swrappers = swrappers, |
582 |
uwrappers = uwrappers, |
|
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
583 |
haz_netpair = haz_netpair, |
6955 | 584 |
dup_netpair = dup_netpair, |
585 |
xtra_netpair = xtra_netpair} |
|
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
586 |
end |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
587 |
else cs; |
1800 | 588 |
|
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
589 |
fun delSE th |
6955 | 590 |
(cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, |
591 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
|
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
592 |
if mem_thm (th, safeEs) then |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
593 |
let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=1) [th] |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
594 |
in CS{safe0_netpair = delete ([], safe0_rls) safe0_netpair, |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
595 |
safep_netpair = delete ([], safep_rls) safep_netpair, |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
596 |
safeIs = safeIs, |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
597 |
safeEs = rem_thm (safeEs,th), |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
598 |
hazIs = hazIs, |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
599 |
hazEs = hazEs, |
6955 | 600 |
xtraIs = xtraIs, |
601 |
xtraEs = xtraEs, |
|
4651 | 602 |
swrappers = swrappers, |
603 |
uwrappers = uwrappers, |
|
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
604 |
haz_netpair = haz_netpair, |
6955 | 605 |
dup_netpair = dup_netpair, |
606 |
xtra_netpair = xtra_netpair} |
|
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
607 |
end |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
608 |
else cs; |
1800 | 609 |
|
610 |
||
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
611 |
fun delI th |
6955 | 612 |
(cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, |
613 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
|
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
614 |
if mem_thm (th, hazIs) then |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
615 |
CS{haz_netpair = delete ([th], []) haz_netpair, |
1800 | 616 |
dup_netpair = delete ([dup_intr th], []) dup_netpair, |
617 |
safeIs = safeIs, |
|
618 |
safeEs = safeEs, |
|
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
619 |
hazIs = rem_thm (hazIs,th), |
1800 | 620 |
hazEs = hazEs, |
6955 | 621 |
xtraIs = xtraIs, |
622 |
xtraEs = xtraEs, |
|
4651 | 623 |
swrappers = swrappers, |
624 |
uwrappers = uwrappers, |
|
1800 | 625 |
safe0_netpair = safe0_netpair, |
6955 | 626 |
safep_netpair = safep_netpair, |
627 |
xtra_netpair = xtra_netpair} |
|
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
628 |
else cs; |
1800 | 629 |
|
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
630 |
fun delE th |
6955 | 631 |
(cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, |
632 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
|
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
633 |
if mem_thm (th, hazEs) then |
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
634 |
CS{haz_netpair = delete ([], [th]) haz_netpair, |
1800 | 635 |
dup_netpair = delete ([], [dup_elim th]) dup_netpair, |
636 |
safeIs = safeIs, |
|
637 |
safeEs = safeEs, |
|
638 |
hazIs = hazIs, |
|
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
639 |
hazEs = rem_thm (hazEs,th), |
6955 | 640 |
xtraIs = xtraIs, |
641 |
xtraEs = xtraEs, |
|
642 |
swrappers = swrappers, |
|
643 |
uwrappers = uwrappers, |
|
644 |
safe0_netpair = safe0_netpair, |
|
645 |
safep_netpair = safep_netpair, |
|
646 |
xtra_netpair = xtra_netpair} |
|
647 |
else cs; |
|
648 |
||
649 |
||
650 |
fun delXI th |
|
651 |
(cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, |
|
652 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
|
653 |
if mem_thm (th, xtraIs) then |
|
654 |
CS{xtra_netpair = delete ([th], []) xtra_netpair, |
|
655 |
safeIs = safeIs, |
|
656 |
safeEs = safeEs, |
|
657 |
hazIs = hazIs, |
|
658 |
hazEs = hazEs, |
|
659 |
xtraIs = rem_thm (xtraIs,th), |
|
660 |
xtraEs = xtraEs, |
|
4651 | 661 |
swrappers = swrappers, |
662 |
uwrappers = uwrappers, |
|
1800 | 663 |
safe0_netpair = safe0_netpair, |
6955 | 664 |
safep_netpair = safep_netpair, |
665 |
haz_netpair = haz_netpair, |
|
666 |
dup_netpair = dup_netpair} |
|
667 |
else cs; |
|
668 |
||
669 |
fun delXE th |
|
670 |
(cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, |
|
671 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
|
672 |
if mem_thm (th, xtraEs) then |
|
673 |
CS{xtra_netpair = delete ([], [th]) xtra_netpair, |
|
674 |
safeIs = safeIs, |
|
675 |
safeEs = safeEs, |
|
676 |
hazIs = hazIs, |
|
677 |
hazEs = hazEs, |
|
678 |
xtraIs = xtraIs, |
|
679 |
xtraEs = rem_thm (xtraEs,th), |
|
680 |
swrappers = swrappers, |
|
681 |
uwrappers = uwrappers, |
|
682 |
safe0_netpair = safe0_netpair, |
|
683 |
safep_netpair = safep_netpair, |
|
684 |
haz_netpair = haz_netpair, |
|
685 |
dup_netpair = dup_netpair} |
|
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
686 |
else cs; |
1800 | 687 |
|
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
688 |
(*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*) |
6955 | 689 |
fun delrule (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...}, th) = |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
690 |
if mem_thm (th, safeIs) orelse mem_thm (th, safeEs) orelse |
6955 | 691 |
mem_thm (th, hazIs) orelse mem_thm (th, hazEs) orelse |
692 |
mem_thm (th, xtraIs) orelse mem_thm (th, xtraEs) |
|
693 |
then delSI th (delSE th (delI th (delE th (delXI th (delXE th cs))))) |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
694 |
else (warning ("Rule not in claset\n" ^ (string_of_thm th)); |
2813
cc4c816dafdc
delrules now deletes ALL occurrences of a rule, since it may appear in any of
paulson
parents:
2689
diff
changeset
|
695 |
cs); |
1800 | 696 |
|
697 |
val op delrules = foldl delrule; |
|
698 |
||
699 |
||
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
700 |
(*** Modifying the wrapper tacticals ***) |
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
701 |
fun update_swrappers |
6955 | 702 |
(CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, |
703 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) f = |
|
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
704 |
CS{safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, |
6955 | 705 |
xtraIs = xtraIs, xtraEs = xtraEs, |
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
706 |
swrappers = f swrappers, uwrappers = uwrappers, |
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
707 |
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, |
6955 | 708 |
haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair}; |
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
709 |
|
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
710 |
fun update_uwrappers |
6955 | 711 |
(CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, |
712 |
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) f = |
|
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
713 |
CS{safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, |
6955 | 714 |
xtraIs = xtraIs, xtraEs = xtraEs, |
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
715 |
swrappers = swrappers, uwrappers = f uwrappers, |
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
716 |
safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, |
6955 | 717 |
haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair}; |
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
718 |
|
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
719 |
|
4651 | 720 |
(*Add/replace a safe wrapper*) |
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
721 |
fun cs addSWrapper new_swrapper = update_swrappers cs (fn swrappers => |
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
722 |
(case assoc_string (swrappers,(fst new_swrapper)) of None =>() |
4651 | 723 |
| Some x => warning("overwriting safe wrapper "^fst new_swrapper); |
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
724 |
overwrite (swrappers, new_swrapper))); |
4651 | 725 |
|
726 |
(*Add/replace an unsafe wrapper*) |
|
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
727 |
fun cs addWrapper new_uwrapper = update_uwrappers cs (fn uwrappers => |
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
728 |
(case assoc_string (uwrappers,(fst new_uwrapper)) of None =>() |
4651 | 729 |
| Some x => warning ("overwriting unsafe wrapper "^fst new_uwrapper); |
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
730 |
overwrite (uwrappers, new_uwrapper))); |
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
731 |
|
4651 | 732 |
(*Remove a safe wrapper*) |
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
733 |
fun cs delSWrapper name = update_swrappers cs (fn swrappers => |
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
734 |
let val (del,rest) = partition (fn (n,_) => n=name) swrappers |
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
735 |
in if null del then (warning ("No such safe wrapper in claset: "^ name); |
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
736 |
swrappers) else rest end); |
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
737 |
|
4651 | 738 |
(*Remove an unsafe wrapper*) |
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
739 |
fun cs delWrapper name = update_uwrappers cs (fn uwrappers => |
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
740 |
let val (del,rest) = partition (fn (n,_) => n=name) uwrappers |
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
741 |
in if null del then (warning ("No such unsafe wrapper in claset: " ^ name); |
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
742 |
uwrappers) else rest end); |
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
743 |
|
2630 | 744 |
(*compose a safe tactic sequentially before/alternatively after safe_step_tac*) |
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
745 |
fun cs addSbefore (name, tac1) = |
5523 | 746 |
cs addSWrapper (name, fn tac2 => tac1 ORELSE' tac2); |
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
747 |
fun cs addSaltern (name, tac2) = |
5523 | 748 |
cs addSWrapper (name, fn tac1 => tac1 ORELSE' tac2); |
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
749 |
|
2630 | 750 |
(*compose a tactic sequentially before/alternatively after the step tactic*) |
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
751 |
fun cs addbefore (name, tac1) = |
5523 | 752 |
cs addWrapper (name, fn tac2 => tac1 APPEND' tac2); |
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
753 |
fun cs addaltern (name, tac2) = |
5523 | 754 |
cs addWrapper (name, fn tac1 => tac1 APPEND' tac2); |
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
755 |
|
5523 | 756 |
fun cs addD2 (name, thm) = |
757 |
cs addaltern (name, dtac thm THEN' atac); |
|
758 |
fun cs addE2 (name, thm) = |
|
759 |
cs addaltern (name, etac thm THEN' atac); |
|
760 |
fun cs addSD2 (name, thm) = |
|
761 |
cs addSaltern (name, dmatch_tac [thm] THEN' eq_assume_tac); |
|
762 |
fun cs addSE2 (name, thm) = |
|
763 |
cs addSaltern (name, ematch_tac [thm] THEN' eq_assume_tac); |
|
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
764 |
|
1711 | 765 |
(*Merge works by adding all new rules of the 2nd claset into the 1st claset. |
766 |
Merging the term nets may look more efficient, but the rather delicate |
|
767 |
treatment of priority might get muddled up.*) |
|
768 |
fun merge_cs |
|
6955 | 769 |
(cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...}, |
4765 | 770 |
CS{safeIs=safeIs2, safeEs=safeEs2, hazIs=hazIs2, hazEs=hazEs2, |
6955 | 771 |
xtraIs=xtraIs2, xtraEs=xtraEs2, swrappers, uwrappers, ...}) = |
1711 | 772 |
let val safeIs' = gen_rems eq_thm (safeIs2,safeIs) |
773 |
val safeEs' = gen_rems eq_thm (safeEs2,safeEs) |
|
2630 | 774 |
val hazIs' = gen_rems eq_thm ( hazIs2, hazIs) |
775 |
val hazEs' = gen_rems eq_thm ( hazEs2, hazEs) |
|
6955 | 776 |
val xtraIs' = gen_rems eq_thm (xtraIs2, xtraIs) |
777 |
val xtraEs' = gen_rems eq_thm (xtraEs2, xtraEs) |
|
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
778 |
val cs1 = cs addSIs safeIs' |
4765 | 779 |
addSEs safeEs' |
780 |
addIs hazIs' |
|
781 |
addEs hazEs' |
|
6955 | 782 |
addXIs xtraIs' |
783 |
addXEs xtraEs' |
|
4767
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
784 |
val cs2 = update_swrappers cs1 (fn ws => merge_alists ws swrappers); |
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
785 |
val cs3 = update_uwrappers cs2 (fn ws => merge_alists ws uwrappers); |
b9f3468c6ee2
introduced functions for updating the wrapper lists
oheimb
parents:
4765
diff
changeset
|
786 |
in cs3 |
1711 | 787 |
end; |
788 |
||
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
789 |
|
1800 | 790 |
(**** Simple tactics for theorem proving ****) |
0 | 791 |
|
792 |
(*Attack subgoals using safe inferences -- matching, not resolution*) |
|
2630 | 793 |
fun safe_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = |
4651 | 794 |
appSWrappers cs (FIRST' [ |
2630 | 795 |
eq_assume_tac, |
796 |
eq_mp_tac, |
|
797 |
bimatch_from_nets_tac safe0_netpair, |
|
798 |
FIRST' hyp_subst_tacs, |
|
799 |
bimatch_from_nets_tac safep_netpair]); |
|
0 | 800 |
|
5757 | 801 |
(*Repeatedly attack a subgoal using safe inferences -- it's deterministic!*) |
802 |
fun safe_steps_tac cs = REPEAT_DETERM1 o |
|
803 |
(fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i)); |
|
804 |
||
0 | 805 |
(*Repeatedly attack subgoals using safe inferences -- it's deterministic!*) |
5757 | 806 |
fun safe_tac cs = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac cs)); |
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
807 |
|
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
808 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
809 |
(*** Clarify_tac: do safe steps without causing branching ***) |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
810 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
811 |
fun nsubgoalsP n (k,brl) = (subgoals_of_brl brl = n); |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
812 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
813 |
(*version of bimatch_from_nets_tac that only applies rules that |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
814 |
create precisely n subgoals.*) |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
815 |
fun n_bimatch_from_nets_tac n = |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
816 |
biresolution_from_nets_tac (orderlist o filter (nsubgoalsP n)) true; |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
817 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
818 |
fun eq_contr_tac i = ematch_tac [not_elim] i THEN eq_assume_tac i; |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
819 |
val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac; |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
820 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
821 |
(*Two-way branching is allowed only if one of the branches immediately closes*) |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
822 |
fun bimatch2_tac netpair i = |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
823 |
n_bimatch_from_nets_tac 2 netpair i THEN |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
824 |
(eq_assume_contr_tac i ORELSE eq_assume_contr_tac (i+1)); |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
825 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
826 |
(*Attack subgoals using safe inferences -- matching, not resolution*) |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
827 |
fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = |
4651 | 828 |
appSWrappers cs (FIRST' [ |
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
829 |
eq_assume_contr_tac, |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
830 |
bimatch_from_nets_tac safe0_netpair, |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
831 |
FIRST' hyp_subst_tacs, |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
832 |
n_bimatch_from_nets_tac 1 safep_netpair, |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
833 |
bimatch2_tac safep_netpair]); |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
834 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
835 |
fun clarify_tac cs = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac cs 1)); |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
836 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
837 |
|
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
838 |
(*** Unsafe steps instantiate variables or lose information ***) |
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
839 |
|
4066 | 840 |
(*Backtracking is allowed among the various these unsafe ways of |
841 |
proving a subgoal. *) |
|
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
842 |
fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) = |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
843 |
assume_tac APPEND' |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
844 |
contr_tac APPEND' |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
845 |
biresolve_from_nets_tac safe0_netpair; |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
846 |
|
4066 | 847 |
(*These unsafe steps could generate more subgoals.*) |
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
848 |
fun instp_step_tac (CS{safep_netpair,...}) = |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
849 |
biresolve_from_nets_tac safep_netpair; |
0 | 850 |
|
851 |
(*These steps could instantiate variables and are therefore unsafe.*) |
|
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
852 |
fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs; |
0 | 853 |
|
982
4fe0b642b7d5
Addition of wrappers for integration with the simplifier.
lcp
parents:
747
diff
changeset
|
854 |
fun haz_step_tac (CS{haz_netpair,...}) = |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
855 |
biresolve_from_nets_tac haz_netpair; |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
856 |
|
0 | 857 |
(*Single step for the prover. FAILS unless it makes progress. *) |
5523 | 858 |
fun step_tac cs i = safe_tac cs ORELSE appWrappers cs |
859 |
(inst_step_tac cs ORELSE' haz_step_tac cs) i; |
|
0 | 860 |
|
861 |
(*Using a "safe" rule to instantiate variables is unsafe. This tactic |
|
862 |
allows backtracking from "safe" rules to "unsafe" rules here.*) |
|
5523 | 863 |
fun slow_step_tac cs i = safe_tac cs ORELSE appWrappers cs |
864 |
(inst_step_tac cs APPEND' haz_step_tac cs) i; |
|
0 | 865 |
|
1800 | 866 |
(**** The following tactics all fail unless they solve one goal ****) |
0 | 867 |
|
868 |
(*Dumb but fast*) |
|
869 |
fun fast_tac cs = SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1)); |
|
870 |
||
871 |
(*Slower but smarter than fast_tac*) |
|
872 |
fun best_tac cs = |
|
873 |
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1)); |
|
874 |
||
875 |
fun slow_tac cs = SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1)); |
|
876 |
||
877 |
fun slow_best_tac cs = |
|
878 |
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1)); |
|
879 |
||
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
880 |
|
1800 | 881 |
(***ASTAR with weight weight_ASTAR, by Norbert Voelker*) |
1587
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
882 |
val weight_ASTAR = ref 5; |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
883 |
|
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
884 |
fun astar_tac cs = |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
885 |
SELECT_GOAL ( ASTAR (has_fewer_prems 1 |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
886 |
, fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level)) |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
887 |
(step_tac cs 1)); |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
888 |
|
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
889 |
fun slow_astar_tac cs = |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
890 |
SELECT_GOAL ( ASTAR (has_fewer_prems 1 |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
891 |
, fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level)) |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
892 |
(slow_step_tac cs 1)); |
e7d8a4957bac
Now provides astar versions (thanks to Norbert Voelker)
paulson
parents:
1524
diff
changeset
|
893 |
|
1800 | 894 |
(**** Complete tactic, loosely based upon LeanTaP. This tactic is the outcome |
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
895 |
of much experimentation! Changing APPEND to ORELSE below would prove |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
896 |
easy theorems faster, but loses completeness -- and many of the harder |
1800 | 897 |
theorems such as 43. ****) |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
898 |
|
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
899 |
(*Non-deterministic! Could always expand the first unsafe connective. |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
900 |
That's hard to implement and did not perform better in experiments, due to |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
901 |
greater search depth required.*) |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
902 |
fun dup_step_tac (cs as (CS{dup_netpair,...})) = |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
903 |
biresolve_from_nets_tac dup_netpair; |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
904 |
|
5523 | 905 |
(*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*) |
5757 | 906 |
local |
907 |
fun slow_step_tac' cs = appWrappers cs |
|
908 |
(instp_step_tac cs APPEND' dup_step_tac cs); |
|
909 |
in fun depth_tac cs m i state = SELECT_GOAL |
|
910 |
(safe_steps_tac cs 1 THEN_ELSE |
|
911 |
(DEPTH_SOLVE (depth_tac cs m 1), |
|
912 |
inst0_step_tac cs 1 APPEND COND (K (m=0)) no_tac |
|
913 |
(slow_step_tac' cs 1 THEN DEPTH_SOLVE (depth_tac cs (m-1) 1)) |
|
914 |
)) i state; |
|
915 |
end; |
|
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
916 |
|
2173 | 917 |
(*Search, with depth bound m. |
918 |
This is the "entry point", which does safe inferences first.*) |
|
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
919 |
fun safe_depth_tac cs m = |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
920 |
SUBGOAL |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
921 |
(fn (prem,i) => |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
922 |
let val deti = |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
923 |
(*No Vars in the goal? No need to backtrack between goals.*) |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
924 |
case term_vars prem of |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
925 |
[] => DETERM |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
926 |
| _::_ => I |
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
927 |
in SELECT_GOAL (TRY (safe_tac cs) THEN |
747
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
928 |
DEPTH_SOLVE (deti (depth_tac cs m 1))) i |
bdc066781063
deepen_tac: modified due to outcome of experiments. Its
lcp
parents:
681
diff
changeset
|
929 |
end); |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
930 |
|
2868
17a23a62f82a
New DEEPEN allows giving an upper bound for deepen_tac
paulson
parents:
2813
diff
changeset
|
931 |
fun deepen_tac cs = DEEPEN (2,10) (safe_depth_tac cs); |
681
9b02474744ca
Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp
parents:
469
diff
changeset
|
932 |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
933 |
|
1724 | 934 |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
935 |
(** claset theory data **) |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
936 |
|
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
937 |
(* init data kind claset *) |
1724 | 938 |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
939 |
exception CSData of claset ref; |
1724 | 940 |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
941 |
local |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
942 |
val empty = CSData (ref empty_cs); |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
943 |
|
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
944 |
(*create new references*) |
6556 | 945 |
fun copy (ClasetData (ref (CSData (ref cs)))) = |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
946 |
ClasetData (ref (CSData (ref cs))); |
6556 | 947 |
val prep_ext = copy; |
1724 | 948 |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
949 |
fun merge (ClasetData (ref (CSData (ref cs1))), ClasetData (ref (CSData (ref cs2)))) = |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
950 |
ClasetData (ref (CSData (ref (merge_cs (cs1, cs2))))); |
1724 | 951 |
|
4259 | 952 |
fun print (_: Sign.sg) (ClasetData (ref (CSData (ref cs)))) = print_cs cs; |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
953 |
in |
6556 | 954 |
val _ = fix_methods (empty, copy, prep_ext, merge, print); |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
955 |
end; |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
956 |
|
1724 | 957 |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
958 |
(* access claset *) |
1724 | 959 |
|
5001 | 960 |
val print_claset = Theory.print_data clasetK; |
4380 | 961 |
|
5001 | 962 |
val claset_ref_of_sg = Sign.get_data clasetK (fn ClasetData (ref (CSData r)) => r); |
1807 | 963 |
|
6391 | 964 |
val claset_ref_of = claset_ref_of_sg o Theory.sign_of; |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
965 |
val claset_of_sg = ! o claset_ref_of_sg; |
6391 | 966 |
val claset_of = claset_of_sg o Theory.sign_of; |
1800 | 967 |
|
6391 | 968 |
fun CLASET tacf state = tacf (claset_of_sg (Thm.sign_of_thm state)) state; |
969 |
fun CLASET' tacf i state = tacf (claset_of_sg (Thm.sign_of_thm state)) i state; |
|
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
970 |
|
5028 | 971 |
val claset = claset_of o Context.the_context; |
6391 | 972 |
val claset_ref = claset_ref_of_sg o Theory.sign_of o Context.the_context; |
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
973 |
|
3705
76f3b2803982
Addition of clarify_tac, clarify_step_tac, Clarify_tac, Clarify_step_tac
paulson
parents:
3546
diff
changeset
|
974 |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
975 |
(* change claset *) |
1800 | 976 |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
977 |
fun change_claset f x = claset_ref () := (f (claset (), x)); |
1724 | 978 |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
979 |
val AddDs = change_claset (op addDs); |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
980 |
val AddEs = change_claset (op addEs); |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
981 |
val AddIs = change_claset (op addIs); |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
982 |
val AddSDs = change_claset (op addSDs); |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
983 |
val AddSEs = change_claset (op addSEs); |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
984 |
val AddSIs = change_claset (op addSIs); |
6955 | 985 |
val AddXDs = change_claset (op addXDs); |
986 |
val AddXEs = change_claset (op addXEs); |
|
987 |
val AddXIs = change_claset (op addXIs); |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
988 |
val Delrules = change_claset (op delrules); |
3727
ed63c05d7992
Added Safe_tac; all other default claset tactics now dereference "claset"
paulson
parents:
3705
diff
changeset
|
989 |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
990 |
|
5841 | 991 |
(* proof data kind 'Provers/claset' *) |
992 |
||
993 |
structure LocalClasetArgs = |
|
994 |
struct |
|
995 |
val name = "Provers/claset"; |
|
996 |
type T = claset; |
|
997 |
val init = claset_of; |
|
998 |
fun print _ cs = print_cs cs; |
|
999 |
end; |
|
1000 |
||
1001 |
structure LocalClaset = ProofDataFun(LocalClasetArgs); |
|
1002 |
val print_local_claset = LocalClaset.print; |
|
1003 |
val get_local_claset = LocalClaset.get; |
|
1004 |
val put_local_claset = LocalClaset.put; |
|
1005 |
||
1006 |
||
5885 | 1007 |
(* attributes *) |
1008 |
||
1009 |
fun change_global_cs f (thy, th) = |
|
1010 |
let val r = claset_ref_of thy |
|
6096 | 1011 |
in r := f (! r, [th]); (thy, th) end; |
5885 | 1012 |
|
1013 |
fun change_local_cs f (ctxt, th) = |
|
6096 | 1014 |
let val cs = f (get_local_claset ctxt, [th]) |
5885 | 1015 |
in (put_local_claset cs ctxt, th) end; |
1016 |
||
1017 |
val safe_dest_global = change_global_cs (op addSDs); |
|
1018 |
val safe_elim_global = change_global_cs (op addSEs); |
|
1019 |
val safe_intro_global = change_global_cs (op addSIs); |
|
6955 | 1020 |
val haz_dest_global = change_global_cs (op addDs); |
1021 |
val haz_elim_global = change_global_cs (op addEs); |
|
1022 |
val haz_intro_global = change_global_cs (op addIs); |
|
1023 |
val xtra_dest_global = change_global_cs (op addXDs); |
|
1024 |
val xtra_elim_global = change_global_cs (op addXEs); |
|
1025 |
val xtra_intro_global = change_global_cs (op addXIs); |
|
5885 | 1026 |
val delrule_global = change_global_cs (op delrules); |
1027 |
||
6955 | 1028 |
val safe_dest_local = change_local_cs (op addSDs); |
1029 |
val safe_elim_local = change_local_cs (op addSEs); |
|
1030 |
val safe_intro_local = change_local_cs (op addSIs); |
|
5885 | 1031 |
val haz_dest_local = change_local_cs (op addDs); |
1032 |
val haz_elim_local = change_local_cs (op addEs); |
|
1033 |
val haz_intro_local = change_local_cs (op addIs); |
|
6955 | 1034 |
val xtra_dest_local = change_local_cs (op addXDs); |
1035 |
val xtra_elim_local = change_local_cs (op addXEs); |
|
1036 |
val xtra_intro_local = change_local_cs (op addXIs); |
|
5885 | 1037 |
val delrule_local = change_local_cs (op delrules); |
1038 |
||
1039 |
||
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
1040 |
(* tactics referring to the implicit claset *) |
1800 | 1041 |
|
4079
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
1042 |
(*the abstraction over the proof state delays the dereferencing*) |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
1043 |
fun Safe_tac st = safe_tac (claset()) st; |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
1044 |
fun Safe_step_tac i st = safe_step_tac (claset()) i st; |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
1045 |
fun Clarify_step_tac i st = clarify_step_tac (claset()) i st; |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
1046 |
fun Clarify_tac i st = clarify_tac (claset()) i st; |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
1047 |
fun Step_tac i st = step_tac (claset()) i st; |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
1048 |
fun Fast_tac i st = fast_tac (claset()) i st; |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
1049 |
fun Best_tac i st = best_tac (claset()) i st; |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
1050 |
fun Slow_tac i st = slow_tac (claset()) i st; |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
1051 |
fun Slow_best_tac i st = slow_best_tac (claset()) i st; |
9df5e4f22d96
new implicit claset mechanism based on Sign.sg anytype data;
wenzelm
parents:
4066
diff
changeset
|
1052 |
fun Deepen_tac m = deepen_tac (claset()) m; |
2066 | 1053 |
|
1800 | 1054 |
|
0 | 1055 |
end; |
5841 | 1056 |
|
1057 |
||
1058 |
||
5885 | 1059 |
(** concrete syntax of attributes **) |
5841 | 1060 |
|
1061 |
(* add / del rules *) |
|
1062 |
||
1063 |
val introN = "intro"; |
|
1064 |
val elimN = "elim"; |
|
1065 |
val destN = "dest"; |
|
1066 |
val delN = "del"; |
|
5885 | 1067 |
val delruleN = "delrule"; |
5841 | 1068 |
|
5885 | 1069 |
val bang = Args.$$$ "!"; |
6955 | 1070 |
val bbang = Args.$$$ "!!"; |
5841 | 1071 |
|
6955 | 1072 |
fun cla_att change xtra haz safe = Attrib.syntax |
1073 |
(Scan.lift ((bbang >> K xtra || bang >> K haz || Scan.succeed safe) >> change)); |
|
5841 | 1074 |
|
6955 | 1075 |
fun cla_attr f g h = (cla_att change_global_cs f g h, cla_att change_local_cs f g h); |
5885 | 1076 |
val del_attr = (Attrib.no_args delrule_global, Attrib.no_args delrule_local); |
5841 | 1077 |
|
1078 |
||
1079 |
(* setup_attrs *) |
|
1080 |
||
1081 |
val setup_attrs = Attrib.add_attributes |
|
6955 | 1082 |
[(destN, cla_attr (op addXDs) (op addDs) (op addSDs), "destruction rule"), |
1083 |
(elimN, cla_attr (op addXEs) (op addEs) (op addSEs), "elimination rule"), |
|
1084 |
(introN, cla_attr (op addXIs) (op addIs) (op addSIs), "introduction rule"), |
|
5885 | 1085 |
(delruleN, del_attr, "delete rule")]; |
5841 | 1086 |
|
1087 |
||
1088 |
||
5885 | 1089 |
(** single rule proof method **) |
5841 | 1090 |
|
1091 |
(* utils *) |
|
1092 |
||
1093 |
fun resolve_from_seq_tac rq i st = Seq.flat (Seq.map (fn r => rtac r i st) rq); |
|
1094 |
fun order_rules xs = map snd (Tactic.orderlist xs); |
|
1095 |
||
1096 |
fun find_rules concl nets = |
|
1097 |
let fun rules_of (inet, _) = order_rules (Net.unify_term inet concl) |
|
1098 |
in flat (map rules_of nets) end; |
|
1099 |
||
1100 |
fun find_erules [] _ = [] |
|
6955 | 1101 |
| find_erules (fact :: _) nets = |
5841 | 1102 |
let |
6502 | 1103 |
fun may_unify net = Net.unify_term net o Logic.strip_assums_concl o #prop o Thm.rep_thm; |
6955 | 1104 |
fun erules_of (_, enet) = order_rules (may_unify enet fact); |
6502 | 1105 |
in flat (map erules_of nets) end; |
5841 | 1106 |
|
1107 |
||
1108 |
(* trace rules *) |
|
1109 |
||
1110 |
val trace_rules = ref false; |
|
1111 |
||
1112 |
fun print_rules rules i = |
|
1113 |
if not (! trace_rules) then () |
|
1114 |
else |
|
1115 |
Pretty.writeln (Pretty.big_list ("trying standard rule(s) on goal #" ^ string_of_int i ^ ":") |
|
1116 |
(map Display.pretty_thm rules)); |
|
1117 |
||
1118 |
||
1119 |
(* single_tac *) |
|
1120 |
||
6502 | 1121 |
val imp_elim_netpair = insert (0, 0) ([], [imp_elim]) empty_netpair; |
1122 |
val not_elim_netpair = insert (0, 0) ([], [Data.not_elim]) empty_netpair; |
|
1123 |
||
6096 | 1124 |
fun single_tac cs facts = |
5841 | 1125 |
let |
6955 | 1126 |
val CS {safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair, ...} = cs; |
6502 | 1127 |
val nets = [imp_elim_netpair, safe0_netpair, safep_netpair, |
6955 | 1128 |
not_elim_netpair, haz_netpair, dup_netpair, xtra_netpair]; |
6492 | 1129 |
val erules = find_erules facts nets; |
5841 | 1130 |
|
1131 |
val tac = SUBGOAL (fn (goal, i) => |
|
1132 |
let |
|
1133 |
val irules = find_rules (Logic.strip_assums_concl goal) nets; |
|
1134 |
val rules = erules @ irules; |
|
1135 |
val ruleq = Method.forward_chain facts rules; |
|
1136 |
in |
|
1137 |
print_rules rules i; |
|
1138 |
fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq) end); |
|
1139 |
in tac end; |
|
1140 |
||
1141 |
val single = Method.METHOD (FIRSTGOAL o (fn facts => CLASET' (fn cs => single_tac cs facts))); |
|
1142 |
||
1143 |
||
1144 |
||
6502 | 1145 |
(** more proof methods **) |
1146 |
||
1147 |
(* contradiction *) |
|
1148 |
||
1149 |
(* FIXME |
|
1150 |
val contradiction = Method.METHOD (fn facts => |
|
1151 |
Method.FINISHED (ALLGOALS (Method.same_tac facts THEN' (contr_tac ORELSE' assume_tac)))); |
|
1152 |
*) |
|
1153 |
||
1154 |
val contradiction = Method.METHOD (fn facts => FIRSTGOAL (Method.same_tac facts THEN' contr_tac)); |
|
1155 |
||
1156 |
||
1157 |
(* automatic methods *) |
|
5841 | 1158 |
|
5927 | 1159 |
val cla_modifiers = |
6955 | 1160 |
[Args.$$$ destN -- bbang >> K xtra_dest_local, |
1161 |
Args.$$$ destN -- bang >> K haz_dest_local, |
|
5927 | 1162 |
Args.$$$ destN >> K safe_dest_local, |
6955 | 1163 |
Args.$$$ elimN -- bbang >> K xtra_elim_local, |
5927 | 1164 |
Args.$$$ elimN -- bang >> K haz_elim_local, |
1165 |
Args.$$$ elimN >> K safe_elim_local, |
|
6955 | 1166 |
Args.$$$ introN -- bbang >> K xtra_intro_local, |
5927 | 1167 |
Args.$$$ introN -- bang >> K haz_intro_local, |
1168 |
Args.$$$ introN >> K safe_intro_local, |
|
1169 |
Args.$$$ delN >> K delrule_local]; |
|
1170 |
||
1171 |
val cla_args = Method.only_sectioned_args cla_modifiers; |
|
5841 | 1172 |
|
5885 | 1173 |
fun cla_meth tac ctxt = Method.METHOD0 (tac (get_local_claset ctxt)); |
1174 |
fun cla_meth' tac ctxt = Method.METHOD0 (FIRSTGOAL (tac (get_local_claset ctxt))); |
|
5841 | 1175 |
|
5885 | 1176 |
val cla_method = cla_args o cla_meth; |
1177 |
val cla_method' = cla_args o cla_meth'; |
|
5841 | 1178 |
|
1179 |
||
1180 |
||
1181 |
(** setup_methods **) |
|
1182 |
||
1183 |
val setup_methods = Method.add_methods |
|
1184 |
[("single", Method.no_args single, "apply standard rule (single step)"), |
|
1185 |
("default", Method.no_args single, "apply standard rule (single step)"), |
|
6502 | 1186 |
("contradiction", Method.no_args contradiction, "proof by contradiction"), |
5885 | 1187 |
("safe_tac", cla_method safe_tac, "safe_tac"), |
1188 |
("safe_step", cla_method' safe_step_tac, "step_tac"), |
|
1189 |
("fast", cla_method' fast_tac, "fast_tac"), |
|
1190 |
("best", cla_method' best_tac, "best_tac"), |
|
1191 |
("slow", cla_method' slow_tac, "slow_tac"), |
|
1192 |
("slow_best", cla_method' slow_best_tac, "slow_best_tac")]; |
|
5841 | 1193 |
|
1194 |
||
1195 |
||
1196 |
(** theory setup **) |
|
1197 |
||
1198 |
(* FIXME claset theory data *) |
|
1199 |
||
1200 |
val setup = [LocalClaset.init, setup_attrs, setup_methods]; |
|
1201 |
||
1202 |
||
1203 |
end; |