author | blanchet |
Fri, 17 Sep 2010 00:35:19 +0200 | |
changeset 39498 | e8aef7ea9cbb |
parent 39497 | fa16349939b7 |
child 39550 | f97fa74c388e |
permissions | -rw-r--r-- |
39495
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/Sledgehammer/metis_reconstruct.ML |
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset
|
2 |
Author: Kong W. Susanto, Cambridge University Computer Laboratory |
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset
|
3 |
Author: Lawrence C. Paulson, Cambridge University Computer Laboratory |
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset
|
4 |
Author: Jasmin Blanchette, TU Muenchen |
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset
|
5 |
Copyright Cambridge University 2007 |
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset
|
6 |
|
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset
|
7 |
Proof reconstruction for Metis. |
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset
|
8 |
*) |
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset
|
9 |
|
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset
|
10 |
signature METIS_RECONSTRUCT = |
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset
|
11 |
sig |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
12 |
type mode = Metis_Translate.mode |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
13 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
14 |
val trace: bool Unsynchronized.ref |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
15 |
val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
16 |
val replay_one_inference : |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
17 |
Proof.context -> mode -> (string * term) list |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
18 |
-> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
19 |
-> (Metis_Thm.thm * thm) list |
39495
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset
|
20 |
end; |
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset
|
21 |
|
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset
|
22 |
structure Metis_Reconstruct : METIS_RECONSTRUCT = |
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset
|
23 |
struct |
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset
|
24 |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
25 |
open Metis_Translate |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
26 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
27 |
val trace = Unsynchronized.ref false |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
28 |
fun trace_msg msg = if !trace then tracing (msg ()) else () |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
29 |
|
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
30 |
datatype term_or_type = SomeTerm of term | SomeType of typ |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
31 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
32 |
fun terms_of [] = [] |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
33 |
| terms_of (SomeTerm t :: tts) = t :: terms_of tts |
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
34 |
| terms_of (SomeType _ :: tts) = terms_of tts; |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
35 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
36 |
fun types_of [] = [] |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
37 |
| types_of (SomeTerm (Var ((a,idx), _)) :: tts) = |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
38 |
if String.isPrefix "_" a then |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
39 |
(*Variable generated by Metis, which might have been a type variable.*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
40 |
TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
41 |
else types_of tts |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
42 |
| types_of (SomeTerm _ :: tts) = types_of tts |
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
43 |
| types_of (SomeType T :: tts) = T :: types_of tts; |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
44 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
45 |
fun apply_list rator nargs rands = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
46 |
let val trands = terms_of rands |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
47 |
in if length trands = nargs then SomeTerm (list_comb(rator, trands)) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
48 |
else raise Fail |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
49 |
("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^ |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
50 |
" expected " ^ Int.toString nargs ^ |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
51 |
" received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands)) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
52 |
end; |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
53 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
54 |
fun infer_types ctxt = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
55 |
Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt); |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
56 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
57 |
(*We use 1 rather than 0 because variable references in clauses may otherwise conflict |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
58 |
with variable constraints in the goal...at least, type inference often fails otherwise. |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
59 |
SEE ALSO axiom_inf below.*) |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
60 |
fun mk_var (w, T) = Var ((w, 1), T) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
61 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
62 |
(*include the default sort, if available*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
63 |
fun mk_tfree ctxt w = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
64 |
let val ww = "'" ^ w |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
65 |
in TFree(ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1))) end; |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
66 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
67 |
(*Remove the "apply" operator from an HO term*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
68 |
fun strip_happ args (Metis_Term.Fn(".",[t,u])) = strip_happ (u::args) t |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
69 |
| strip_happ args x = (x, args); |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
70 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
71 |
fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
72 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
73 |
fun smart_invert_const "fequal" = @{const_name HOL.eq} |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
74 |
| smart_invert_const s = invert_const s |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
75 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
76 |
fun hol_type_from_metis_term _ (Metis_Term.Var v) = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
77 |
(case strip_prefix_and_unascii tvar_prefix v of |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
78 |
SOME w => make_tvar w |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
79 |
| NONE => make_tvar v) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
80 |
| hol_type_from_metis_term ctxt (Metis_Term.Fn(x, tys)) = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
81 |
(case strip_prefix_and_unascii type_const_prefix x of |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
82 |
SOME tc => Type (smart_invert_const tc, |
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
83 |
map (hol_type_from_metis_term ctxt) tys) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
84 |
| NONE => |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
85 |
case strip_prefix_and_unascii tfree_prefix x of |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
86 |
SOME tf => mk_tfree ctxt tf |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
87 |
| NONE => raise Fail ("hol_type_from_metis_term: " ^ x)); |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
88 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
89 |
(*Maps metis terms to isabelle terms*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
90 |
fun hol_term_from_metis_PT ctxt fol_tm = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
91 |
let val thy = ProofContext.theory_of ctxt |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
92 |
val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^ |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
93 |
Metis_Term.toString fol_tm) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
94 |
fun tm_to_tt (Metis_Term.Var v) = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
95 |
(case strip_prefix_and_unascii tvar_prefix v of |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
96 |
SOME w => SomeType (make_tvar w) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
97 |
| NONE => |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
98 |
case strip_prefix_and_unascii schematic_var_prefix v of |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
99 |
SOME w => SomeTerm (mk_var (w, HOLogic.typeT)) |
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
100 |
| NONE => SomeTerm (mk_var (v, HOLogic.typeT)) ) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
101 |
(*Var from Metis with a name like _nnn; possibly a type variable*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
102 |
| tm_to_tt (Metis_Term.Fn ("{}", [arg])) = tm_to_tt arg (*hBOOL*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
103 |
| tm_to_tt (t as Metis_Term.Fn (".",_)) = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
104 |
let val (rator,rands) = strip_happ [] t |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
105 |
in case rator of |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
106 |
Metis_Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
107 |
| _ => case tm_to_tt rator of |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
108 |
SomeTerm t => SomeTerm (list_comb(t, terms_of (map tm_to_tt rands))) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
109 |
| _ => raise Fail "tm_to_tt: HO application" |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
110 |
end |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
111 |
| tm_to_tt (Metis_Term.Fn (fname, args)) = applic_to_tt (fname,args) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
112 |
and applic_to_tt ("=",ts) = |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
113 |
SomeTerm (list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), terms_of (map tm_to_tt ts))) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
114 |
| applic_to_tt (a,ts) = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
115 |
case strip_prefix_and_unascii const_prefix a of |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
116 |
SOME b => |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
117 |
let val c = smart_invert_const b |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
118 |
val ntypes = num_type_args thy c |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
119 |
val nterms = length ts - ntypes |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
120 |
val tts = map tm_to_tt ts |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
121 |
val tys = types_of (List.take(tts,ntypes)) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
122 |
in if length tys = ntypes then |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
123 |
apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes)) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
124 |
else |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
125 |
raise Fail ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^ |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
126 |
" but gets " ^ Int.toString (length tys) ^ |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
127 |
" type arguments\n" ^ |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
128 |
cat_lines (map (Syntax.string_of_typ ctxt) tys) ^ |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
129 |
" the terms are \n" ^ |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
130 |
cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts))) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
131 |
end |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
132 |
| NONE => (*Not a constant. Is it a type constructor?*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
133 |
case strip_prefix_and_unascii type_const_prefix a of |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
134 |
SOME b => |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
135 |
SomeType (Type (smart_invert_const b, types_of (map tm_to_tt ts))) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
136 |
| NONE => (*Maybe a TFree. Should then check that ts=[].*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
137 |
case strip_prefix_and_unascii tfree_prefix a of |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
138 |
SOME b => SomeType (mk_tfree ctxt b) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
139 |
| NONE => (*a fixed variable? They are Skolem functions.*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
140 |
case strip_prefix_and_unascii fixed_var_prefix a of |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
141 |
SOME b => |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
142 |
let val opr = Free (b, HOLogic.typeT) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
143 |
in apply_list opr (length ts) (map tm_to_tt ts) end |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
144 |
| NONE => raise Fail ("unexpected metis function: " ^ a) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
145 |
in |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
146 |
case tm_to_tt fol_tm of |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
147 |
SomeTerm t => t |
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
148 |
| SomeType T => raise TYPE ("fol_tm_to_tt: Term expected", [T], []) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
149 |
end |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
150 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
151 |
(*Maps fully-typed metis terms to isabelle terms*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
152 |
fun hol_term_from_metis_FT ctxt fol_tm = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
153 |
let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^ |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
154 |
Metis_Term.toString fol_tm) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
155 |
fun cvt (Metis_Term.Fn ("ti", [Metis_Term.Var v, _])) = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
156 |
(case strip_prefix_and_unascii schematic_var_prefix v of |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
157 |
SOME w => mk_var(w, dummyT) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
158 |
| NONE => mk_var(v, dummyT)) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
159 |
| cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn ("=",[]), _])) = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
160 |
Const (@{const_name HOL.eq}, HOLogic.typeT) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
161 |
| cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (x,[]), ty])) = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
162 |
(case strip_prefix_and_unascii const_prefix x of |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
163 |
SOME c => Const (smart_invert_const c, dummyT) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
164 |
| NONE => (*Not a constant. Is it a fixed variable??*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
165 |
case strip_prefix_and_unascii fixed_var_prefix x of |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
166 |
SOME v => Free (v, hol_type_from_metis_term ctxt ty) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
167 |
| NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x)) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
168 |
| cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (".",[tm1,tm2]), _])) = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
169 |
cvt tm1 $ cvt tm2 |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
170 |
| cvt (Metis_Term.Fn (".",[tm1,tm2])) = (*untyped application*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
171 |
cvt tm1 $ cvt tm2 |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
172 |
| cvt (Metis_Term.Fn ("{}", [arg])) = cvt arg (*hBOOL*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
173 |
| cvt (Metis_Term.Fn ("=", [tm1,tm2])) = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
174 |
list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), map cvt [tm1,tm2]) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
175 |
| cvt (t as Metis_Term.Fn (x, [])) = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
176 |
(case strip_prefix_and_unascii const_prefix x of |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
177 |
SOME c => Const (smart_invert_const c, dummyT) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
178 |
| NONE => (*Not a constant. Is it a fixed variable??*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
179 |
case strip_prefix_and_unascii fixed_var_prefix x of |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
180 |
SOME v => Free (v, dummyT) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
181 |
| NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x); |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
182 |
hol_term_from_metis_PT ctxt t)) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
183 |
| cvt t = (trace_msg (fn () => "hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t); |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
184 |
hol_term_from_metis_PT ctxt t) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
185 |
in fol_tm |> cvt end |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
186 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
187 |
fun hol_term_from_metis FT = hol_term_from_metis_FT |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
188 |
| hol_term_from_metis _ = hol_term_from_metis_PT |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
189 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
190 |
fun hol_terms_from_fol ctxt mode skolems fol_tms = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
191 |
let val ts = map (hol_term_from_metis mode ctxt) fol_tms |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
192 |
val _ = trace_msg (fn () => " calling type inference:") |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
193 |
val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
194 |
val ts' = ts |> map (reveal_skolem_terms skolems) |> infer_types ctxt |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
195 |
val _ = app (fn t => trace_msg |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
196 |
(fn () => " final term: " ^ Syntax.string_of_term ctxt t ^ |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
197 |
" of type " ^ Syntax.string_of_typ ctxt (type_of t))) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
198 |
ts' |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
199 |
in ts' end; |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
200 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
201 |
(* ------------------------------------------------------------------------- *) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
202 |
(* FOL step Inference Rules *) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
203 |
(* ------------------------------------------------------------------------- *) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
204 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
205 |
(*for debugging only*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
206 |
(* |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
207 |
fun print_thpair (fth,th) = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
208 |
(trace_msg (fn () => "============================================="); |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
209 |
trace_msg (fn () => "Metis: " ^ Metis_Thm.toString fth); |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
210 |
trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th)); |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
211 |
*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
212 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
213 |
fun lookth thpairs (fth : Metis_Thm.thm) = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
214 |
the (AList.lookup (uncurry Metis_Thm.equal) thpairs fth) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
215 |
handle Option.Option => |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
216 |
raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fth) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
217 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
218 |
fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx)); |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
219 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
220 |
(* INFERENCE RULE: AXIOM *) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
221 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
222 |
fun axiom_inf thpairs th = Thm.incr_indexes 1 (lookth thpairs th); |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
223 |
(*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
224 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
225 |
(* INFERENCE RULE: ASSUME *) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
226 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
227 |
val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)} |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
228 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
229 |
fun inst_excluded_middle thy i_atm = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
230 |
let val th = EXCLUDED_MIDDLE |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
231 |
val [vx] = Term.add_vars (prop_of th) [] |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
232 |
val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)] |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
233 |
in cterm_instantiate substs th end; |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
234 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
235 |
fun assume_inf ctxt mode skolems atm = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
236 |
inst_excluded_middle |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
237 |
(ProofContext.theory_of ctxt) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
238 |
(singleton (hol_terms_from_fol ctxt mode skolems) (Metis_Term.Fn atm)) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
239 |
|
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
240 |
(* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
241 |
to reconstruct them admits new possibilities of errors, e.g. concerning |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
242 |
sorts. Instead we try to arrange that new TVars are distinct and that types |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
243 |
can be inferred from terms. *) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
244 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
245 |
fun inst_inf ctxt mode skolems thpairs fsubst th = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
246 |
let val thy = ProofContext.theory_of ctxt |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
247 |
val i_th = lookth thpairs th |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
248 |
val i_th_vars = Term.add_vars (prop_of i_th) [] |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
249 |
fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
250 |
fun subst_translation (x,y) = |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
251 |
let val v = find_var x |
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
252 |
(* We call "reveal_skolem_terms" and "infer_types" below. *) |
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
253 |
val t = hol_term_from_metis mode ctxt y |
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
254 |
in SOME (cterm_of thy (Var v), t) end |
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
255 |
handle Option.Option => |
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
256 |
(trace_msg (fn () => "\"find_var\" failed for " ^ x ^ |
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
257 |
" in " ^ Display.string_of_thm ctxt i_th); |
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
258 |
NONE) |
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
259 |
| TYPE _ => |
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
260 |
(trace_msg (fn () => "\"hol_term_from_metis\" failed for " ^ x ^ |
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
261 |
" in " ^ Display.string_of_thm ctxt i_th); |
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
262 |
NONE) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
263 |
fun remove_typeinst (a, t) = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
264 |
case strip_prefix_and_unascii schematic_var_prefix a of |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
265 |
SOME b => SOME (b, t) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
266 |
| NONE => case strip_prefix_and_unascii tvar_prefix a of |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
267 |
SOME _ => NONE (*type instantiations are forbidden!*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
268 |
| NONE => SOME (a,t) (*internal Metis var?*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
269 |
val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
270 |
val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
271 |
val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
272 |
val tms = rawtms |> map (reveal_skolem_terms skolems) |> infer_types ctxt |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
273 |
val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
274 |
val substs' = ListPair.zip (vars, map ctm_of tms) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
275 |
val _ = trace_msg (fn () => |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
276 |
cat_lines ("subst_translations:" :: |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
277 |
(substs' |> map (fn (x, y) => |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
278 |
Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^ |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
279 |
Syntax.string_of_term ctxt (term_of y))))); |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
280 |
in cterm_instantiate substs' i_th end |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
281 |
handle THM (msg, _, _) => |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
282 |
error ("Cannot replay Metis proof in Isabelle:\n" ^ msg) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
283 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
284 |
(* INFERENCE RULE: RESOLVE *) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
285 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
286 |
(* Like RSN, but we rename apart only the type variables. Vars here typically |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
287 |
have an index of 1, and the use of RSN would increase this typically to 3. |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
288 |
Instantiations of those Vars could then fail. See comment on "mk_var". *) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
289 |
fun resolve_inc_tyvars thy tha i thb = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
290 |
let |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
291 |
val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
292 |
fun aux tha thb = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
293 |
case Thm.bicompose false (false, tha, nprems_of tha) i thb |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
294 |
|> Seq.list_of |> distinct Thm.eq_thm of |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
295 |
[th] => th |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
296 |
| _ => raise THM ("resolve_inc_tyvars: unique result expected", i, |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
297 |
[tha, thb]) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
298 |
in |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
299 |
aux tha thb |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
300 |
handle TERM z => |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
301 |
(* The unifier, which is invoked from "Thm.bicompose", will sometimes |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
302 |
refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
303 |
"TERM" exception (with "add_ffpair" as first argument). We then |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
304 |
perform unification of the types of variables by hand and try |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
305 |
again. We could do this the first time around but this error |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
306 |
occurs seldom and we don't want to break existing proofs in subtle |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
307 |
ways or slow them down needlessly. *) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
308 |
case [] |> fold (Term.add_vars o prop_of) [tha, thb] |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
309 |
|> AList.group (op =) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
310 |
|> maps (fn ((s, _), T :: Ts) => |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
311 |
map (fn T' => (Free (s, T), Free (s, T'))) Ts) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
312 |
|> rpair (Envir.empty ~1) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
313 |
|-> fold (Pattern.unify thy) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
314 |
|> Envir.type_env |> Vartab.dest |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
315 |
|> map (fn (x, (S, T)) => |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
316 |
pairself (ctyp_of thy) (TVar (x, S), T)) of |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
317 |
[] => raise TERM z |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
318 |
| ps => aux (instantiate (ps, []) tha) (instantiate (ps, []) thb) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
319 |
end |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
320 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
321 |
fun mk_not (Const (@{const_name Not}, _) $ b) = b |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
322 |
| mk_not b = HOLogic.mk_not b |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
323 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
324 |
(* Match untyped terms. *) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
325 |
fun untyped_aconv (Const (a, _)) (Const(b, _)) = (a = b) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
326 |
| untyped_aconv (Free (a, _)) (Free (b, _)) = (a = b) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
327 |
| untyped_aconv (Var ((a, _), _)) (Var ((b, _), _)) = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
328 |
(a = b) (* The index is ignored, for some reason. *) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
329 |
| untyped_aconv (Bound i) (Bound j) = (i = j) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
330 |
| untyped_aconv (Abs (_, _, t)) (Abs (_, _, u)) = untyped_aconv t u |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
331 |
| untyped_aconv (t1 $ t2) (u1 $ u2) = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
332 |
untyped_aconv t1 u1 andalso untyped_aconv t2 u2 |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
333 |
| untyped_aconv _ _ = false |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
334 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
335 |
(* Finding the relative location of an untyped term within a list of terms *) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
336 |
fun literal_index lit = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
337 |
let |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
338 |
val lit = Envir.eta_contract lit |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
339 |
fun get _ [] = raise Empty |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
340 |
| get n (x :: xs) = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
341 |
if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x)) then |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
342 |
n |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
343 |
else |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
344 |
get (n+1) xs |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
345 |
in get 1 end |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
346 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
347 |
fun resolve_inf ctxt mode skolems thpairs atm th1 th2 = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
348 |
let |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
349 |
val thy = ProofContext.theory_of ctxt |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
350 |
val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2 |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
351 |
val _ = trace_msg (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
352 |
val _ = trace_msg (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
353 |
in |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
354 |
(* Trivial cases where one operand is type info *) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
355 |
if Thm.eq_thm (TrueI, i_th1) then |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
356 |
i_th2 |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
357 |
else if Thm.eq_thm (TrueI, i_th2) then |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
358 |
i_th1 |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
359 |
else |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
360 |
let |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
361 |
val i_atm = singleton (hol_terms_from_fol ctxt mode skolems) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
362 |
(Metis_Term.Fn atm) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
363 |
val _ = trace_msg (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
364 |
val prems_th1 = prems_of i_th1 |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
365 |
val prems_th2 = prems_of i_th2 |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
366 |
val index_th1 = literal_index (mk_not i_atm) prems_th1 |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
367 |
handle Empty => raise Fail "Failed to find literal in th1" |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
368 |
val _ = trace_msg (fn () => " index_th1: " ^ Int.toString index_th1) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
369 |
val index_th2 = literal_index i_atm prems_th2 |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
370 |
handle Empty => raise Fail "Failed to find literal in th2" |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
371 |
val _ = trace_msg (fn () => " index_th2: " ^ Int.toString index_th2) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
372 |
in |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
373 |
resolve_inc_tyvars thy (Meson.select_literal index_th1 i_th1) index_th2 |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
374 |
i_th2 |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
375 |
end |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
376 |
end; |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
377 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
378 |
(* INFERENCE RULE: REFL *) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
379 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
380 |
val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp} |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
381 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
382 |
val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) []))); |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
383 |
val refl_idx = 1 + Thm.maxidx_of REFL_THM; |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
384 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
385 |
fun refl_inf ctxt mode skolems t = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
386 |
let val thy = ProofContext.theory_of ctxt |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
387 |
val i_t = singleton (hol_terms_from_fol ctxt mode skolems) t |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
388 |
val _ = trace_msg (fn () => " term: " ^ Syntax.string_of_term ctxt i_t) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
389 |
val c_t = cterm_incr_types thy refl_idx i_t |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
390 |
in cterm_instantiate [(refl_x, c_t)] REFL_THM end; |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
391 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
392 |
(* INFERENCE RULE: EQUALITY *) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
393 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
394 |
val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp} |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
395 |
val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp} |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
396 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
397 |
val metis_eq = Metis_Term.Fn ("=", []); |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
398 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
399 |
fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0 (*equality has no type arguments*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
400 |
| get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
401 |
| get_ty_arg_size _ _ = 0; |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
402 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
403 |
fun equality_inf ctxt mode skolems (pos, atm) fp fr = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
404 |
let val thy = ProofContext.theory_of ctxt |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
405 |
val m_tm = Metis_Term.Fn atm |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
406 |
val [i_atm,i_tm] = hol_terms_from_fol ctxt mode skolems [m_tm, fr] |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
407 |
val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
408 |
fun replace_item_list lx 0 (_::ls) = lx::ls |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
409 |
| replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
410 |
fun path_finder_FO tm [] = (tm, Bound 0) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
411 |
| path_finder_FO tm (p::ps) = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
412 |
let val (tm1,args) = strip_comb tm |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
413 |
val adjustment = get_ty_arg_size thy tm1 |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
414 |
val p' = if adjustment > p then p else p-adjustment |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
415 |
val tm_p = List.nth(args,p') |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
416 |
handle Subscript => |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
417 |
error ("Cannot replay Metis proof in Isabelle:\n" ^ |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
418 |
"equality_inf: " ^ Int.toString p ^ " adj " ^ |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
419 |
Int.toString adjustment ^ " term " ^ |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
420 |
Syntax.string_of_term ctxt tm) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
421 |
val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^ |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
422 |
" " ^ Syntax.string_of_term ctxt tm_p) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
423 |
val (r,t) = path_finder_FO tm_p ps |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
424 |
in |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
425 |
(r, list_comb (tm1, replace_item_list t p' args)) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
426 |
end |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
427 |
fun path_finder_HO tm [] = (tm, Bound 0) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
428 |
| path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
429 |
| path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
430 |
| path_finder_HO tm ps = |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
431 |
raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^ |
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
432 |
"equality_inf, path_finder_HO: path = " ^ |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
433 |
space_implode " " (map Int.toString ps) ^ |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
434 |
" isa-term: " ^ Syntax.string_of_term ctxt tm) |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
435 |
fun path_finder_FT tm [] _ = (tm, Bound 0) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
436 |
| path_finder_FT tm (0::ps) (Metis_Term.Fn ("ti", [t1, _])) = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
437 |
path_finder_FT tm ps t1 |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
438 |
| path_finder_FT (t$u) (0::ps) (Metis_Term.Fn (".", [t1, _])) = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
439 |
(fn(x,y) => (x, y$u)) (path_finder_FT t ps t1) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
440 |
| path_finder_FT (t$u) (1::ps) (Metis_Term.Fn (".", [_, t2])) = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
441 |
(fn(x,y) => (x, t$y)) (path_finder_FT u ps t2) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
442 |
| path_finder_FT tm ps t = |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
443 |
raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^ |
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
444 |
"equality_inf, path_finder_FT: path = " ^ |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
445 |
space_implode " " (map Int.toString ps) ^ |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
446 |
" isa-term: " ^ Syntax.string_of_term ctxt tm ^ |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
447 |
" fol-term: " ^ Metis_Term.toString t) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
448 |
fun path_finder FO tm ps _ = path_finder_FO tm ps |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
449 |
| path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (p::ps) _ = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
450 |
(*equality: not curried, as other predicates are*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
451 |
if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
452 |
else path_finder_HO tm (p::ps) (*1 selects second operand*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
453 |
| path_finder HO tm (_ :: ps) (Metis_Term.Fn ("{}", [_])) = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
454 |
path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
455 |
| path_finder FT (tm as Const(@{const_name HOL.eq}, _) $ _ $ _) (p::ps) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
456 |
(Metis_Term.Fn ("=", [t1,t2])) = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
457 |
(*equality: not curried, as other predicates are*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
458 |
if p=0 then path_finder_FT tm (0::1::ps) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
459 |
(Metis_Term.Fn (".", [Metis_Term.Fn (".", [metis_eq,t1]), t2])) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
460 |
(*select first operand*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
461 |
else path_finder_FT tm (p::ps) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
462 |
(Metis_Term.Fn (".", [metis_eq,t2])) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
463 |
(*1 selects second operand*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
464 |
| path_finder FT tm (_ :: ps) (Metis_Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1 |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
465 |
(*if not equality, ignore head to skip the hBOOL predicate*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
466 |
| path_finder FT tm ps t = path_finder_FT tm ps t (*really an error case!*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
467 |
fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
468 |
let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
469 |
in (tm, nt $ tm_rslt) end |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
470 |
| path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
471 |
val (tm_subst, body) = path_finder_lit i_atm fp |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
472 |
val tm_abs = Abs ("x", type_of tm_subst, body) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
473 |
val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
474 |
val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
475 |
val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
476 |
val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill typed but gives right max*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
477 |
val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
478 |
val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst') |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
479 |
val eq_terms = map (pairself (cterm_of thy)) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
480 |
(ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm])) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
481 |
in cterm_instantiate eq_terms subst' end; |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
482 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
483 |
val factor = Seq.hd o distinct_subgoals_tac; |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
484 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
485 |
fun step ctxt mode skolems thpairs p = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
486 |
case p of |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
487 |
(fol_th, Metis_Proof.Axiom _) => factor (axiom_inf thpairs fol_th) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
488 |
| (_, Metis_Proof.Assume f_atm) => assume_inf ctxt mode skolems f_atm |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
489 |
| (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) => |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
490 |
factor (inst_inf ctxt mode skolems thpairs f_subst f_th1) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
491 |
| (_, Metis_Proof.Resolve(f_atm, f_th1, f_th2)) => |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
492 |
factor (resolve_inf ctxt mode skolems thpairs f_atm f_th1 f_th2) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
493 |
| (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode skolems f_tm |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
494 |
| (_, Metis_Proof.Equality (f_lit, f_p, f_r)) => |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
495 |
equality_inf ctxt mode skolems f_lit f_p f_r |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
496 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
497 |
fun is_real_literal (_, (c, _)) = not (String.isPrefix class_prefix c) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
498 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
499 |
fun replay_one_inference ctxt mode skolems (fol_th, inf) thpairs = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
500 |
let |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
501 |
val _ = trace_msg (fn () => "=============================================") |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
502 |
val _ = trace_msg (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
503 |
val _ = trace_msg (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
504 |
val th = Meson.flexflex_first_order (step ctxt mode skolems |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
505 |
thpairs (fol_th, inf)) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
506 |
val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
507 |
val _ = trace_msg (fn () => "=============================================") |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
508 |
val n_metis_lits = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
509 |
length (filter is_real_literal (Metis_LiteralSet.toList (Metis_Thm.clause fol_th))) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
510 |
val _ = if nprems_of th = n_metis_lits then () |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
511 |
else error "Cannot replay Metis proof in Isabelle: Out of sync." |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
512 |
in (fol_th, th) :: thpairs end |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
513 |
|
39495
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset
|
514 |
end; |