147 fun add_if_not_inlist [] xs newlist = newlist |
147 fun add_if_not_inlist [] xs newlist = newlist |
148 | add_if_not_inlist (y::ys) xs newlist = if (not (inlist y xs)) then |
148 | add_if_not_inlist (y::ys) xs newlist = if (not (inlist y xs)) then |
149 add_if_not_inlist ys xs (y::newlist) |
149 add_if_not_inlist ys xs (y::newlist) |
150 else add_if_not_inlist ys xs (newlist) |
150 else add_if_not_inlist ys xs (newlist) |
151 |
151 |
152 (* |
|
153 fun is_alpha_space_neg_eq_colon ch = (ch = "~") orelse (is_alpha ch) orelse ( ch = " ")orelse ( ch = ";") orelse( ch = "=") |
|
154 |
|
155 (* replace | by ; here *) |
|
156 fun change_or [] = [] |
|
157 | change_or (x::xs) = if x = "|" |
|
158 then |
|
159 [";"]@(change_or xs) |
|
160 else (x::(change_or xs)) |
|
161 |
|
162 |
|
163 fun clause_lit_string t = let val termstr = (Sign.string_of_term Mainsign ) t |
|
164 val exp_term = explode termstr |
|
165 val colon_term = change_or exp_term |
|
166 in |
|
167 implode(List.filter is_alpha_space_neg_eq_colon colon_term) |
|
168 end |
|
169 |
|
170 fun get_clause_lits thm = clause_lit_string (prop_of thm) |
|
171 *) |
|
172 |
|
173 |
|
174 fun onestr [] str = str |
152 fun onestr [] str = str |
175 | onestr (x::xs) str = onestr xs (str^(concat x)) |
153 | onestr (x::xs) str = onestr xs (str^(concat x)) |
176 |
154 |
177 fun thmstrings [] str = str |
155 fun thmstrings [] str = str |
178 | thmstrings (x::xs) str = thmstrings xs (str^(string_of_thm x)) |
156 | thmstrings (x::xs) str = thmstrings xs (str^(string_of_thm x)) |
179 |
157 |
180 fun onelist [] newlist = newlist |
158 fun onelist [] newlist = newlist |
181 | onelist (x::xs) newlist = onelist xs (newlist@x) |
159 | onelist (x::xs) newlist = onelist xs (newlist@x) |
182 |
160 |
183 |
161 |
184 (**** Code to support ordinary resolution, rather than Model Elimination ****) |
|
185 |
|
186 (*Convert a list of clauses (disjunctions) to meta-level clauses (==>), |
|
187 with no contrapositives, for ordinary resolution.*) |
|
188 |
|
189 (*raises exception if no rules apply -- unlike RL*) |
|
190 fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls)) |
|
191 | tryres (th, []) = raise THM("tryres", 0, [th]); |
|
192 |
162 |
193 val prop_of = #prop o rep_thm; |
163 val prop_of = #prop o rep_thm; |
194 |
164 |
195 |
165 |
196 (*For ordinary resolution. *) |
|
197 val resolution_clause_rules = [disj_assoc, make_neg_rule', make_pos_rule']; |
|
198 (*Use "theorem naming" to label the clauses*) |
|
199 fun name_thms label = |
|
200 let fun name1 (th, (k,ths)) = |
|
201 (k-1, Thm.name_thm (label ^ string_of_int k, th) :: ths) |
|
202 |
|
203 in fn ths => #2 (foldr name1 (length ths, []) ths) end; |
|
204 |
|
205 (*Find an all-negative support clause*) |
|
206 fun is_negative th = forall (not o #1) (literals (prop_of th)); |
|
207 |
|
208 val neg_clauses = List.filter is_negative; |
|
209 |
|
210 |
|
211 |
|
212 (*True if the given type contains bool anywhere*) |
|
213 fun has_bool (Type("bool",_)) = true |
|
214 | has_bool (Type(_, Ts)) = exists has_bool Ts |
|
215 | has_bool _ = false; |
|
216 |
|
217 |
|
218 (*Create a meta-level Horn clause*) |
|
219 fun make_horn crules th = make_horn crules (tryres(th,crules)) |
|
220 handle THM _ => th; |
|
221 |
|
222 |
|
223 (*Raises an exception if any Vars in the theorem mention type bool. That would mean |
|
224 they are higher-order, and in addition, they could cause make_horn to loop!*) |
|
225 fun check_no_bool th = |
|
226 if exists (has_bool o fastype_of) (term_vars (#prop (rep_thm th))) |
|
227 then raise THM ("check_no_bool", 0, [th]) else th; |
|
228 |
|
229 |
|
230 (*Rules to convert the head literal into a negated assumption. If the head |
|
231 literal is already negated, then using notEfalse instead of notEfalse' |
|
232 prevents a double negation.*) |
|
233 val notEfalse = read_instantiate [("R","False")] notE; |
|
234 val notEfalse' = rotate_prems 1 notEfalse; |
|
235 |
|
236 fun negated_asm_of_head th = |
|
237 th RS notEfalse handle THM _ => th RS notEfalse'; |
|
238 |
|
239 (*Converting one clause*) |
|
240 fun make_meta_clause th = |
|
241 negated_asm_of_head (make_horn resolution_clause_rules (check_no_bool th)); |
|
242 |
|
243 fun make_meta_clauses ths = |
|
244 name_thms "MClause#" |
|
245 (gen_distinct Drule.eq_thm_prop (map make_meta_clause ths)); |
|
246 |
|
247 (*Permute a rule's premises to move the i-th premise to the last position.*) |
|
248 fun make_last i th = |
|
249 let val n = nprems_of th |
|
250 in if 1 <= i andalso i <= n |
|
251 then Thm.permute_prems (i-1) 1 th |
|
252 else raise THM("select_literal", i, [th]) |
|
253 end; |
|
254 |
|
255 (*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing |
|
256 double-negations.*) |
|
257 val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection]; |
|
258 |
|
259 (*Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*) |
|
260 fun select_literal i cl = negate_head (make_last i cl); |
|
261 |
166 |
262 fun get_axioms_used proof_steps thmstring = let |
167 fun get_axioms_used proof_steps thmstring = let |
263 val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr"))) |
168 val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr"))) |
264 val _ = TextIO.output (outfile, thmstring) |
169 val _ = TextIO.output (outfile, thmstring) |
265 |
170 |