13 |
13 |
14 val hol_clause_from_metis : |
14 val hol_clause_from_metis : |
15 Proof.context -> int Symtab.table -> (string * term) list -> Metis_Thm.thm |
15 Proof.context -> int Symtab.table -> (string * term) list -> Metis_Thm.thm |
16 -> term |
16 -> term |
17 val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a |
17 val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a |
18 val metis_aconv_untyped : term * term -> bool |
|
19 val replay_one_inference : |
18 val replay_one_inference : |
20 Proof.context -> (string * term) list -> int Symtab.table |
19 Proof.context -> (string * term) list -> int Symtab.table |
21 -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list |
20 -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list |
22 -> (Metis_Thm.thm * thm) list |
21 -> (Metis_Thm.thm * thm) list |
23 val discharge_skolem_premises : |
22 val discharge_skolem_premises : |
207 | s_not t = HOLogic.mk_not t |
206 | s_not t = HOLogic.mk_not t |
208 fun simp_not_not (@{const Trueprop} $ t) = @{const Trueprop} $ simp_not_not t |
207 fun simp_not_not (@{const Trueprop} $ t) = @{const Trueprop} $ simp_not_not t |
209 | simp_not_not (@{const Not} $ t) = s_not (simp_not_not t) |
208 | simp_not_not (@{const Not} $ t) = s_not (simp_not_not t) |
210 | simp_not_not t = t |
209 | simp_not_not t = t |
211 |
210 |
212 (* Match untyped terms. *) |
|
213 fun metis_aconv_untyped (Const (a, _), Const(b, _)) = (a = b) |
|
214 | metis_aconv_untyped (Free (a, _), Free (b, _)) = (a = b) |
|
215 | metis_aconv_untyped (Var ((a, _), _), Var ((b, _), _)) = |
|
216 a = b (* ignore variable numbers *) |
|
217 | metis_aconv_untyped (Bound i, Bound j) = (i = j) |
|
218 | metis_aconv_untyped (Abs (_, _, t), Abs (_, _, u)) = |
|
219 metis_aconv_untyped (t, u) |
|
220 | metis_aconv_untyped (t1 $ t2, u1 $ u2) = |
|
221 metis_aconv_untyped (t1, u1) andalso metis_aconv_untyped (t2, u2) |
|
222 | metis_aconv_untyped _ = false |
|
223 |
|
224 val normalize_literal = simp_not_not o Envir.eta_contract |
211 val normalize_literal = simp_not_not o Envir.eta_contract |
225 |
212 |
226 (* Find the relative location of an untyped term within a list of terms as a |
213 (* Find the relative location of an untyped term within a list of terms as a |
227 1-based index. Returns 0 in case of failure. *) |
214 1-based index. Returns 0 in case of failure. *) |
228 fun index_of_literal lit haystack = |
215 fun index_of_literal lit haystack = |
229 let |
216 let |
230 fun match_lit normalize = |
217 fun match_lit normalize = |
231 HOLogic.dest_Trueprop #> normalize |
218 HOLogic.dest_Trueprop #> normalize |
232 #> curry metis_aconv_untyped (lit |> normalize) |
219 #> curry Term.aconv_untyped (lit |> normalize) |
233 in |
220 in |
234 (case find_index (match_lit I) haystack of |
221 (case find_index (match_lit I) haystack of |
235 ~1 => find_index (match_lit (simp_not_not o Envir.eta_contract)) haystack |
222 ~1 => find_index (match_lit (simp_not_not o Envir.eta_contract)) haystack |
236 | j => j) + 1 |
223 | j => j) + 1 |
237 end |
224 end |
432 th |
419 th |
433 else |
420 else |
434 let |
421 let |
435 val (prems0, concl) = th |> prop_of |> Logic.strip_horn |
422 val (prems0, concl) = th |> prop_of |> Logic.strip_horn |
436 val prems = prems0 |> map normalize_literal |
423 val prems = prems0 |> map normalize_literal |
437 |> distinct metis_aconv_untyped |
424 |> distinct Term.aconv_untyped |
438 val goal = Logic.list_implies (prems, concl) |
425 val goal = Logic.list_implies (prems, concl) |
439 val tac = cut_rules_tac [th] 1 |
426 val tac = cut_rules_tac [th] 1 |
440 THEN rewrite_goals_tac @{thms not_not [THEN eq_reflection]} |
427 THEN rewrite_goals_tac @{thms not_not [THEN eq_reflection]} |
441 THEN ALLGOALS assume_tac |
428 THEN ALLGOALS assume_tac |
442 in |
429 in |
482 let |
469 let |
483 val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract |
470 val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract |
484 val prem = goal |> Logic.strip_assums_hyp |> hd |
471 val prem = goal |> Logic.strip_assums_hyp |> hd |
485 val concl = goal |> Logic.strip_assums_concl |
472 val concl = goal |> Logic.strip_assums_concl |
486 fun pair_untyped_aconv (t1, t2) (u1, u2) = |
473 fun pair_untyped_aconv (t1, t2) (u1, u2) = |
487 metis_aconv_untyped (t1, u1) andalso metis_aconv_untyped (t2, u2) |
474 Term.aconv_untyped (t1, u1) andalso Term.aconv_untyped (t2, u2) |
488 fun add_terms tp inst = |
475 fun add_terms tp inst = |
489 if exists (pair_untyped_aconv tp) inst then inst |
476 if exists (pair_untyped_aconv tp) inst then inst |
490 else tp :: map (apsnd (subst_atomic [tp])) inst |
477 else tp :: map (apsnd (subst_atomic [tp])) inst |
491 fun is_flex t = |
478 fun is_flex t = |
492 case strip_comb t of |
479 case strip_comb t of |