author | blanchet |
Wed, 01 Jun 2011 10:29:43 +0200 | |
changeset 43134 | 0c82e00ba63e |
parent 43130 | d73fc2e55308 |
child 43135 | 8c32a0160b0d |
permissions | -rw-r--r-- |
39958 | 1 |
(* Title: HOL/Tools/Metis/metis_reconstruct.ML |
39495
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 |
|
42650
552eae49f97d
reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
blanchet
parents:
42616
diff
changeset
|
14 |
exception METIS of string * string |
552eae49f97d
reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
blanchet
parents:
42616
diff
changeset
|
15 |
|
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
16 |
val trace : bool Config.T |
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
17 |
val trace_msg : Proof.context -> (unit -> string) -> unit |
40665
1a65f0c74827
added "verbose" option to Metis to shut up its warnings if necessary
blanchet
parents:
40264
diff
changeset
|
18 |
val verbose : bool Config.T |
1a65f0c74827
added "verbose" option to Metis to shut up its warnings if necessary
blanchet
parents:
40264
diff
changeset
|
19 |
val verbose_warning : Proof.context -> string -> unit |
43128 | 20 |
val hol_term_from_metis : |
21 |
mode -> int Symtab.table -> Proof.context -> Metis_Term.term -> term |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
22 |
val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a |
43134
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43130
diff
changeset
|
23 |
val untyped_aconv : term * term -> bool |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
24 |
val replay_one_inference : |
43094 | 25 |
Proof.context -> mode -> (string * term) list -> int Symtab.table |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
26 |
-> 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
|
27 |
-> (Metis_Thm.thm * thm) list |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
28 |
val discharge_skolem_premises : |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
29 |
Proof.context -> (thm * term) option list -> thm -> thm |
39495
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset
|
30 |
end; |
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset
|
31 |
|
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset
|
32 |
structure Metis_Reconstruct : METIS_RECONSTRUCT = |
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset
|
33 |
struct |
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset
|
34 |
|
43094 | 35 |
open ATP_Problem |
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
42650
diff
changeset
|
36 |
open ATP_Translate |
43094 | 37 |
open ATP_Reconstruct |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
38 |
open Metis_Translate |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
39 |
|
42650
552eae49f97d
reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
blanchet
parents:
42616
diff
changeset
|
40 |
exception METIS of string * string |
552eae49f97d
reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
blanchet
parents:
42616
diff
changeset
|
41 |
|
42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42570
diff
changeset
|
42 |
val trace = Attrib.setup_config_bool @{binding metis_trace} (K false) |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42570
diff
changeset
|
43 |
val verbose = Attrib.setup_config_bool @{binding metis_verbose} (K true) |
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
44 |
|
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
45 |
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else () |
40665
1a65f0c74827
added "verbose" option to Metis to shut up its warnings if necessary
blanchet
parents:
40264
diff
changeset
|
46 |
fun verbose_warning ctxt msg = |
42650
552eae49f97d
reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
blanchet
parents:
42616
diff
changeset
|
47 |
if Config.get ctxt verbose then warning ("Metis: " ^ msg) else () |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
48 |
|
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
49 |
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
|
50 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
51 |
fun terms_of [] = [] |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
52 |
| 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
|
53 |
| terms_of (SomeType _ :: tts) = terms_of tts; |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
54 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
55 |
fun types_of [] = [] |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
56 |
| types_of (SomeTerm (Var ((a,idx), _)) :: tts) = |
42098
f978caf60bbe
more robust handling of variables in new Skolemizer
blanchet
parents:
41491
diff
changeset
|
57 |
if String.isPrefix metis_generated_var_prefix a then |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
58 |
(*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
|
59 |
TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
60 |
else types_of tts |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
61 |
| 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
|
62 |
| 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
|
63 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
64 |
fun apply_list rator nargs rands = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
65 |
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
|
66 |
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
|
67 |
else raise Fail |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
68 |
("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^ |
41491 | 69 |
" expected " ^ string_of_int nargs ^ |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
70 |
" 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
|
71 |
end; |
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 infer_types ctxt = |
42361 | 74 |
Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt); |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
75 |
|
43094 | 76 |
(* We use 1 rather than 0 because variable references in clauses may otherwise |
77 |
conflict with variable constraints in the goal...at least, type inference |
|
78 |
often fails otherwise. 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
|
79 |
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
|
80 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
81 |
(*include the default sort, if available*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
82 |
fun mk_tfree ctxt w = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
83 |
let val ww = "'" ^ w |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
84 |
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
|
85 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
86 |
(*Remove the "apply" operator from an HO term*) |
43094 | 87 |
fun strip_happ args (Metis_Term.Fn (".", [t, u])) = strip_happ (u :: args) t |
88 |
| strip_happ args x = (x, args) |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
89 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
90 |
fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
91 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
92 |
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
|
93 |
(case strip_prefix_and_unascii tvar_prefix v of |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
94 |
SOME w => make_tvar w |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
95 |
| NONE => make_tvar v) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
96 |
| 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
|
97 |
(case strip_prefix_and_unascii type_const_prefix x of |
41140
9c68004b8c9d
added Sledgehammer support for higher-order propositional reasoning
blanchet
parents:
41139
diff
changeset
|
98 |
SOME tc => Type (invert_const tc, |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
99 |
map (hol_type_from_metis_term ctxt) tys) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
100 |
| NONE => |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
101 |
case strip_prefix_and_unascii tfree_prefix x of |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
102 |
SOME tf => mk_tfree ctxt tf |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
103 |
| NONE => raise Fail ("hol_type_from_metis_term: " ^ x)); |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
104 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
105 |
(*Maps metis terms to isabelle terms*) |
42341
5a00af7f4978
removed obsolete Skolem counter in new Skolemizer
blanchet
parents:
42339
diff
changeset
|
106 |
fun hol_term_from_metis_PT ctxt fol_tm = |
42361 | 107 |
let val thy = Proof_Context.theory_of ctxt |
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
108 |
val _ = trace_msg ctxt (fn () => "hol_term_from_metis_PT: " ^ |
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
109 |
Metis_Term.toString fol_tm) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
110 |
fun tm_to_tt (Metis_Term.Var v) = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
111 |
(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
|
112 |
SOME w => SomeType (make_tvar w) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
113 |
| NONE => |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
114 |
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
|
115 |
SOME w => SomeTerm (mk_var (w, HOLogic.typeT)) |
42270 | 116 |
| NONE => SomeTerm (mk_var (v, HOLogic.typeT))) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
117 |
(*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
|
118 |
| tm_to_tt (Metis_Term.Fn ("{}", [arg])) = tm_to_tt arg (*hBOOL*) |
43094 | 119 |
| tm_to_tt (t as Metis_Term.Fn (".", _)) = |
120 |
let val (rator,rands) = strip_happ [] t in |
|
121 |
case rator of |
|
122 |
Metis_Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands) |
|
123 |
| _ => case tm_to_tt rator of |
|
124 |
SomeTerm t => SomeTerm (list_comb(t, terms_of (map tm_to_tt rands))) |
|
125 |
| _ => raise Fail "tm_to_tt: HO application" |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
126 |
end |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
127 |
| 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
|
128 |
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
|
129 |
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
|
130 |
| applic_to_tt (a,ts) = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
131 |
case strip_prefix_and_unascii const_prefix a of |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
132 |
SOME b => |
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39550
diff
changeset
|
133 |
let |
42570
77f94ac04f32
cleanup proxification/unproxification and make sure that "num_atp_type_args" is called on the proxy in the reconstruction code, since "c_fequal" has one type arg but the unproxified equal has 0
blanchet
parents:
42364
diff
changeset
|
134 |
val c = b |> invert_const |> unproxify_const |
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39550
diff
changeset
|
135 |
val ntypes = num_type_args thy c |
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39550
diff
changeset
|
136 |
val nterms = length ts - ntypes |
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39550
diff
changeset
|
137 |
val tts = map tm_to_tt ts |
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39550
diff
changeset
|
138 |
val tys = types_of (List.take(tts,ntypes)) |
39939
6e9aff5ee9b5
paramify new skolems just like old ones (cf. reveal_old_skolem_terms)
blanchet
parents:
39896
diff
changeset
|
139 |
val t = |
6e9aff5ee9b5
paramify new skolems just like old ones (cf. reveal_old_skolem_terms)
blanchet
parents:
39896
diff
changeset
|
140 |
if String.isPrefix new_skolem_const_prefix c then |
42341
5a00af7f4978
removed obsolete Skolem counter in new Skolemizer
blanchet
parents:
42339
diff
changeset
|
141 |
Var ((new_skolem_var_name_from_const c, 1), |
39939
6e9aff5ee9b5
paramify new skolems just like old ones (cf. reveal_old_skolem_terms)
blanchet
parents:
39896
diff
changeset
|
142 |
Type_Infer.paramify_vars (tl tys ---> hd tys)) |
6e9aff5ee9b5
paramify new skolems just like old ones (cf. reveal_old_skolem_terms)
blanchet
parents:
39896
diff
changeset
|
143 |
else |
6e9aff5ee9b5
paramify new skolems just like old ones (cf. reveal_old_skolem_terms)
blanchet
parents:
39896
diff
changeset
|
144 |
Const (c, dummyT) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
145 |
in if length tys = ntypes then |
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39550
diff
changeset
|
146 |
apply_list t nterms (List.drop(tts,ntypes)) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
147 |
else |
41491 | 148 |
raise Fail ("Constant " ^ c ^ " expects " ^ string_of_int ntypes ^ |
149 |
" but gets " ^ string_of_int (length tys) ^ |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
150 |
" type arguments\n" ^ |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
151 |
cat_lines (map (Syntax.string_of_typ ctxt) tys) ^ |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
152 |
" the terms are \n" ^ |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
153 |
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
|
154 |
end |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
155 |
| NONE => (*Not a constant. Is it a type constructor?*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
156 |
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
|
157 |
SOME b => |
41140
9c68004b8c9d
added Sledgehammer support for higher-order propositional reasoning
blanchet
parents:
41139
diff
changeset
|
158 |
SomeType (Type (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
|
159 |
| NONE => (*Maybe a TFree. Should then check that ts=[].*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
160 |
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
|
161 |
SOME b => SomeType (mk_tfree ctxt b) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
162 |
| NONE => (*a fixed variable? They are Skolem functions.*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
163 |
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
|
164 |
SOME b => |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
165 |
let val opr = Free (b, HOLogic.typeT) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
166 |
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
|
167 |
| NONE => raise Fail ("unexpected metis function: " ^ a) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
168 |
in |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
169 |
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
|
170 |
SomeTerm t => t |
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
171 |
| 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
|
172 |
end |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
173 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
174 |
(*Maps fully-typed metis terms to isabelle terms*) |
42341
5a00af7f4978
removed obsolete Skolem counter in new Skolemizer
blanchet
parents:
42339
diff
changeset
|
175 |
fun hol_term_from_metis_FT ctxt fol_tm = |
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
176 |
let val _ = trace_msg ctxt (fn () => "hol_term_from_metis_FT: " ^ |
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
177 |
Metis_Term.toString fol_tm) |
42337 | 178 |
fun do_const c = |
42570
77f94ac04f32
cleanup proxification/unproxification and make sure that "num_atp_type_args" is called on the proxy in the reconstruction code, since "c_fequal" has one type arg but the unproxified equal has 0
blanchet
parents:
42364
diff
changeset
|
179 |
let val c = c |> invert_const |> unproxify_const in |
42337 | 180 |
if String.isPrefix new_skolem_const_prefix c then |
181 |
Var ((new_skolem_var_name_from_const c, 1), dummyT) |
|
182 |
else |
|
183 |
Const (c, dummyT) |
|
184 |
end |
|
43104
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
185 |
fun cvt (Metis_Term.Fn (":", [Metis_Term.Var v, _])) = |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
186 |
(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
|
187 |
SOME w => mk_var(w, dummyT) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
188 |
| NONE => mk_var(v, dummyT)) |
43104
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
189 |
| cvt (Metis_Term.Fn (":", [Metis_Term.Fn ("=",[]), _])) = |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
190 |
Const (@{const_name HOL.eq}, HOLogic.typeT) |
43104
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
191 |
| cvt (Metis_Term.Fn (":", [Metis_Term.Fn (x,[]), ty])) = |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
192 |
(case strip_prefix_and_unascii const_prefix x of |
42337 | 193 |
SOME c => do_const c |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
194 |
| NONE => (*Not a constant. Is it a fixed variable??*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
195 |
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
|
196 |
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
|
197 |
| NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x)) |
43104
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
198 |
| cvt (Metis_Term.Fn (":", [Metis_Term.Fn (".", [tm1,tm2]), _])) = |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
199 |
cvt tm1 $ cvt tm2 |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
200 |
| cvt (Metis_Term.Fn (".",[tm1,tm2])) = (*untyped application*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
201 |
cvt tm1 $ cvt tm2 |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
202 |
| cvt (Metis_Term.Fn ("{}", [arg])) = cvt arg (*hBOOL*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
203 |
| cvt (Metis_Term.Fn ("=", [tm1,tm2])) = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
204 |
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
|
205 |
| cvt (t as Metis_Term.Fn (x, [])) = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
206 |
(case strip_prefix_and_unascii const_prefix x of |
42337 | 207 |
SOME c => do_const c |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
208 |
| NONE => (*Not a constant. Is it a fixed variable??*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
209 |
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
|
210 |
SOME v => Free (v, dummyT) |
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
211 |
| NONE => (trace_msg ctxt (fn () => |
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
212 |
"hol_term_from_metis_FT bad const: " ^ x); |
42341
5a00af7f4978
removed obsolete Skolem counter in new Skolemizer
blanchet
parents:
42339
diff
changeset
|
213 |
hol_term_from_metis_PT ctxt t)) |
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
214 |
| cvt t = (trace_msg ctxt (fn () => |
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
215 |
"hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t); |
42341
5a00af7f4978
removed obsolete Skolem counter in new Skolemizer
blanchet
parents:
42339
diff
changeset
|
216 |
hol_term_from_metis_PT ctxt t) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
217 |
in fol_tm |> cvt end |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
218 |
|
43094 | 219 |
fun atp_name_from_metis s = |
43104
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
220 |
case find_first (fn (_, (s', _)) => s' = s) metis_name_table of |
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
221 |
SOME ((s, _), (_, swap)) => (s, swap) |
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
222 |
| _ => (s, false) |
43094 | 223 |
fun atp_term_from_metis (Metis_Term.Fn (s, tms)) = |
43104
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
224 |
let val (s, swap) = atp_name_from_metis s in |
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
225 |
ATerm (s, tms |> map atp_term_from_metis |> swap ? rev) |
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
226 |
end |
43094 | 227 |
| atp_term_from_metis (Metis_Term.Var s) = ATerm (s, []) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
228 |
|
43103 | 229 |
fun hol_term_from_metis_MX sym_tab ctxt = |
43094 | 230 |
let val thy = Proof_Context.theory_of ctxt in |
43103 | 231 |
atp_term_from_metis #> term_from_atp thy false sym_tab [] |
232 |
(* FIXME ### tfrees instead of []? *) NONE |
|
43094 | 233 |
end |
234 |
||
235 |
fun hol_term_from_metis FO _ = hol_term_from_metis_PT |
|
236 |
| hol_term_from_metis HO _ = hol_term_from_metis_PT |
|
237 |
| hol_term_from_metis FT _ = hol_term_from_metis_FT |
|
43103 | 238 |
| hol_term_from_metis MX sym_tab = hol_term_from_metis_MX sym_tab |
43094 | 239 |
|
240 |
fun hol_terms_from_metis ctxt mode old_skolems sym_tab fol_tms = |
|
241 |
let val ts = map (hol_term_from_metis mode sym_tab ctxt) fol_tms |
|
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
242 |
val _ = trace_msg ctxt (fn () => " calling type inference:") |
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
243 |
val _ = app (fn t => trace_msg ctxt |
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
244 |
(fn () => Syntax.string_of_term ctxt t)) ts |
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39550
diff
changeset
|
245 |
val ts' = ts |> map (reveal_old_skolem_terms old_skolems) |
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39550
diff
changeset
|
246 |
|> infer_types ctxt |
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
247 |
val _ = app (fn t => trace_msg ctxt |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
248 |
(fn () => " final term: " ^ Syntax.string_of_term ctxt t ^ |
43128 | 249 |
" of type " ^ Syntax.string_of_typ ctxt (type_of t))) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
250 |
ts' |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
251 |
in ts' end; |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
252 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
253 |
(* ------------------------------------------------------------------------- *) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
254 |
(* FOL step Inference Rules *) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
255 |
(* ------------------------------------------------------------------------- *) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
256 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
257 |
(*for debugging only*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
258 |
(* |
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
259 |
fun print_thpair ctxt (fth,th) = |
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
260 |
(trace_msg ctxt (fn () => "============================================="); |
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
261 |
trace_msg ctxt (fn () => "Metis: " ^ Metis_Thm.toString fth); |
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
262 |
trace_msg ctxt (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th)); |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
263 |
*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
264 |
|
43094 | 265 |
fun lookth th_pairs fth = |
266 |
the (AList.lookup (uncurry Metis_Thm.equal) th_pairs fth) |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
267 |
handle Option.Option => |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
268 |
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
|
269 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
270 |
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
|
271 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
272 |
(* INFERENCE RULE: AXIOM *) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
273 |
|
43094 | 274 |
(* This causes variables to have an index of 1 by default. See also "mk_var" |
275 |
above. *) |
|
276 |
fun axiom_inf th_pairs th = Thm.incr_indexes 1 (lookth th_pairs th) |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
277 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
278 |
(* INFERENCE RULE: ASSUME *) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
279 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
280 |
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
|
281 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
282 |
fun inst_excluded_middle thy i_atm = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
283 |
let val th = EXCLUDED_MIDDLE |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
284 |
val [vx] = Term.add_vars (prop_of th) [] |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
285 |
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
|
286 |
in cterm_instantiate substs th end; |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
287 |
|
43094 | 288 |
fun assume_inf ctxt mode old_skolems sym_tab atm = |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
289 |
inst_excluded_middle |
42361 | 290 |
(Proof_Context.theory_of ctxt) |
43094 | 291 |
(singleton (hol_terms_from_metis ctxt mode old_skolems sym_tab) |
40259
c0e34371c2e2
prevent type errors because of inconsistent skolem Var types by giving fresh indices to Skolems
blanchet
parents:
40258
diff
changeset
|
292 |
(Metis_Term.Fn atm)) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
293 |
|
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
294 |
(* 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
|
295 |
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
|
296 |
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
|
297 |
can be inferred from terms. *) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
298 |
|
43094 | 299 |
fun inst_inf ctxt mode old_skolems sym_tab th_pairs fsubst th = |
42361 | 300 |
let val thy = Proof_Context.theory_of ctxt |
43094 | 301 |
val i_th = lookth th_pairs th |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
302 |
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
|
303 |
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
|
304 |
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
|
305 |
let val v = find_var x |
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39550
diff
changeset
|
306 |
(* We call "reveal_old_skolem_terms" and "infer_types" below. *) |
43094 | 307 |
val t = hol_term_from_metis mode sym_tab ctxt y |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
308 |
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
|
309 |
handle Option.Option => |
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
310 |
(trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^ |
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
311 |
" in " ^ Display.string_of_thm ctxt i_th); |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
312 |
NONE) |
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
313 |
| TYPE _ => |
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
314 |
(trace_msg ctxt (fn () => "\"hol_term_from_metis\" failed for " ^ x ^ |
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
315 |
" in " ^ Display.string_of_thm ctxt i_th); |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
316 |
NONE) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
317 |
fun remove_typeinst (a, t) = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
318 |
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
|
319 |
SOME b => SOME (b, t) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
320 |
| 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
|
321 |
SOME _ => NONE (*type instantiations are forbidden!*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
322 |
| NONE => SOME (a,t) (*internal Metis var?*) |
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
323 |
val _ = trace_msg ctxt (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
324 |
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
|
325 |
val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs) |
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39550
diff
changeset
|
326 |
val tms = rawtms |> map (reveal_old_skolem_terms old_skolems) |
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39550
diff
changeset
|
327 |
|> infer_types ctxt |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
328 |
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
|
329 |
val substs' = ListPair.zip (vars, map ctm_of tms) |
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
330 |
val _ = trace_msg ctxt (fn () => |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
331 |
cat_lines ("subst_translations:" :: |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
332 |
(substs' |> map (fn (x, y) => |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
333 |
Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^ |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
334 |
Syntax.string_of_term ctxt (term_of y))))); |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
335 |
in cterm_instantiate substs' i_th end |
42650
552eae49f97d
reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
blanchet
parents:
42616
diff
changeset
|
336 |
handle THM (msg, _, _) => raise METIS ("inst_inf", msg) |
552eae49f97d
reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
blanchet
parents:
42616
diff
changeset
|
337 |
| ERROR msg => raise METIS ("inst_inf", msg) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
338 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
339 |
(* INFERENCE RULE: RESOLVE *) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
340 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
341 |
(* 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
|
342 |
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
|
343 |
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
|
344 |
fun resolve_inc_tyvars thy tha i thb = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
345 |
let |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
346 |
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
|
347 |
fun aux tha thb = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
348 |
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
|
349 |
|> Seq.list_of |> distinct Thm.eq_thm of |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
350 |
[th] => th |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
351 |
| _ => raise THM ("resolve_inc_tyvars: unique result expected", i, |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
352 |
[tha, thb]) |
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 |
aux tha thb |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
355 |
handle TERM z => |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
356 |
(* 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
|
357 |
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
|
358 |
"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
|
359 |
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
|
360 |
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
|
361 |
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
|
362 |
ways or slow them down needlessly. *) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
363 |
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
|
364 |
|> AList.group (op =) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
365 |
|> maps (fn ((s, _), T :: Ts) => |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
366 |
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
|
367 |
|> rpair (Envir.empty ~1) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
368 |
|-> fold (Pattern.unify thy) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
369 |
|> Envir.type_env |> Vartab.dest |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
370 |
|> map (fn (x, (S, T)) => |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
371 |
pairself (ctyp_of thy) (TVar (x, S), T)) of |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
372 |
[] => raise TERM z |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
373 |
| ps => aux (instantiate (ps, []) tha) (instantiate (ps, []) thb) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
374 |
end |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
375 |
|
40221
d10b68c6e6d4
do not let Metis be confused by higher-order reasoning leading to literals of the form "~ ~ p", which are really the same as "p"
blanchet
parents:
40158
diff
changeset
|
376 |
fun s_not (@{const Not} $ t) = t |
d10b68c6e6d4
do not let Metis be confused by higher-order reasoning leading to literals of the form "~ ~ p", which are really the same as "p"
blanchet
parents:
40158
diff
changeset
|
377 |
| s_not t = HOLogic.mk_not t |
d10b68c6e6d4
do not let Metis be confused by higher-order reasoning leading to literals of the form "~ ~ p", which are really the same as "p"
blanchet
parents:
40158
diff
changeset
|
378 |
fun simp_not_not (@{const Not} $ t) = s_not (simp_not_not t) |
d10b68c6e6d4
do not let Metis be confused by higher-order reasoning leading to literals of the form "~ ~ p", which are really the same as "p"
blanchet
parents:
40158
diff
changeset
|
379 |
| simp_not_not t = t |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
380 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
381 |
(* Match untyped terms. *) |
43134
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43130
diff
changeset
|
382 |
fun untyped_aconv (Const (a, _), Const(b, _)) = (a = b) |
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43130
diff
changeset
|
383 |
| untyped_aconv (Free (a, _), Free (b, _)) = (a = b) |
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43130
diff
changeset
|
384 |
| untyped_aconv (Var ((a, _), _), Var ((b, _), _)) = (a = b) |
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43130
diff
changeset
|
385 |
| untyped_aconv (Bound i, Bound j) = (i = j) |
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43130
diff
changeset
|
386 |
| untyped_aconv (Abs (_, _, t), Abs (_, _, u)) = untyped_aconv (t, u) |
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43130
diff
changeset
|
387 |
| untyped_aconv (t1 $ t2, u1 $ u2) = |
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43130
diff
changeset
|
388 |
untyped_aconv (t1, u1) andalso untyped_aconv (t2, u2) |
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43130
diff
changeset
|
389 |
| untyped_aconv _ = false |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
390 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
391 |
(* Finding the relative location of an untyped term within a list of terms *) |
40221
d10b68c6e6d4
do not let Metis be confused by higher-order reasoning leading to literals of the form "~ ~ p", which are really the same as "p"
blanchet
parents:
40158
diff
changeset
|
392 |
fun index_of_literal lit haystack = |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
393 |
let |
40221
d10b68c6e6d4
do not let Metis be confused by higher-order reasoning leading to literals of the form "~ ~ p", which are really the same as "p"
blanchet
parents:
40158
diff
changeset
|
394 |
val normalize = simp_not_not o Envir.eta_contract |
d10b68c6e6d4
do not let Metis be confused by higher-order reasoning leading to literals of the form "~ ~ p", which are really the same as "p"
blanchet
parents:
40158
diff
changeset
|
395 |
val match_lit = |
43134
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43130
diff
changeset
|
396 |
HOLogic.dest_Trueprop #> normalize |
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43130
diff
changeset
|
397 |
#> curry untyped_aconv (lit |> normalize) |
40221
d10b68c6e6d4
do not let Metis be confused by higher-order reasoning leading to literals of the form "~ ~ p", which are really the same as "p"
blanchet
parents:
40158
diff
changeset
|
398 |
in case find_index match_lit haystack of ~1 => raise Empty | n => n + 1 end |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
399 |
|
39893 | 400 |
(* Permute a rule's premises to move the i-th premise to the last position. *) |
401 |
fun make_last i th = |
|
402 |
let val n = nprems_of th |
|
403 |
in if 1 <= i andalso i <= n |
|
404 |
then Thm.permute_prems (i-1) 1 th |
|
405 |
else raise THM("select_literal", i, [th]) |
|
406 |
end; |
|
407 |
||
42348
187354e22c7d
improve on 0b05cc14c2cb: make sure that a literal variable "?foo" isn't accidentally renamed "?Q", which might be enough to confuse the new Skolemizer (cf. "Clausify.thy" example)
blanchet
parents:
42344
diff
changeset
|
408 |
(* Maps a rule that ends "... ==> P ==> False" to "... ==> ~ P" while avoiding |
42349
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
42348
diff
changeset
|
409 |
to create double negations. The "select" wrapper is a trick to ensure that |
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
42348
diff
changeset
|
410 |
"P ==> ~ False ==> False" is rewritten to "P ==> False", not to "~ P". We |
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
42348
diff
changeset
|
411 |
don't use this trick in general because it makes the proof object uglier than |
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
42348
diff
changeset
|
412 |
necessary. FIXME. *) |
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
42348
diff
changeset
|
413 |
fun negate_head th = |
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
42348
diff
changeset
|
414 |
if exists (fn t => t aconv @{prop "~ False"}) (prems_of th) then |
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
42348
diff
changeset
|
415 |
(th RS @{thm select_FalseI}) |
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
42348
diff
changeset
|
416 |
|> fold (rewrite_rule o single) |
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
42348
diff
changeset
|
417 |
@{thms not_atomize_select atomize_not_select} |
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
42348
diff
changeset
|
418 |
else |
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
42348
diff
changeset
|
419 |
th |> fold (rewrite_rule o single) @{thms not_atomize atomize_not} |
39893 | 420 |
|
421 |
(* Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *) |
|
42348
187354e22c7d
improve on 0b05cc14c2cb: make sure that a literal variable "?foo" isn't accidentally renamed "?Q", which might be enough to confuse the new Skolemizer (cf. "Clausify.thy" example)
blanchet
parents:
42344
diff
changeset
|
422 |
val select_literal = negate_head oo make_last |
39893 | 423 |
|
43094 | 424 |
fun resolve_inf ctxt mode old_skolems sym_tab th_pairs atm th1 th2 = |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
425 |
let |
42361 | 426 |
val thy = Proof_Context.theory_of ctxt |
43094 | 427 |
val (i_th1, i_th2) = pairself (lookth th_pairs) (th1, th2) |
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
428 |
val _ = trace_msg ctxt (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1) |
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
429 |
val _ = trace_msg ctxt (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
430 |
in |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
431 |
(* Trivial cases where one operand is type info *) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
432 |
if Thm.eq_thm (TrueI, i_th1) then |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
433 |
i_th2 |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
434 |
else if Thm.eq_thm (TrueI, i_th2) then |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
435 |
i_th1 |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
436 |
else |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
437 |
let |
40221
d10b68c6e6d4
do not let Metis be confused by higher-order reasoning leading to literals of the form "~ ~ p", which are really the same as "p"
blanchet
parents:
40158
diff
changeset
|
438 |
val i_atm = |
43094 | 439 |
singleton (hol_terms_from_metis ctxt mode old_skolems sym_tab) |
40221
d10b68c6e6d4
do not let Metis be confused by higher-order reasoning leading to literals of the form "~ ~ p", which are really the same as "p"
blanchet
parents:
40158
diff
changeset
|
440 |
(Metis_Term.Fn atm) |
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
441 |
val _ = trace_msg ctxt (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
442 |
val prems_th1 = prems_of i_th1 |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
443 |
val prems_th2 = prems_of i_th2 |
40221
d10b68c6e6d4
do not let Metis be confused by higher-order reasoning leading to literals of the form "~ ~ p", which are really the same as "p"
blanchet
parents:
40158
diff
changeset
|
444 |
val index_th1 = |
d10b68c6e6d4
do not let Metis be confused by higher-order reasoning leading to literals of the form "~ ~ p", which are really the same as "p"
blanchet
parents:
40158
diff
changeset
|
445 |
index_of_literal (s_not i_atm) prems_th1 |
d10b68c6e6d4
do not let Metis be confused by higher-order reasoning leading to literals of the form "~ ~ p", which are really the same as "p"
blanchet
parents:
40158
diff
changeset
|
446 |
handle Empty => raise Fail "Failed to find literal in th1" |
41491 | 447 |
val _ = trace_msg ctxt (fn () => " index_th1: " ^ string_of_int index_th1) |
40221
d10b68c6e6d4
do not let Metis be confused by higher-order reasoning leading to literals of the form "~ ~ p", which are really the same as "p"
blanchet
parents:
40158
diff
changeset
|
448 |
val index_th2 = |
d10b68c6e6d4
do not let Metis be confused by higher-order reasoning leading to literals of the form "~ ~ p", which are really the same as "p"
blanchet
parents:
40158
diff
changeset
|
449 |
index_of_literal i_atm prems_th2 |
d10b68c6e6d4
do not let Metis be confused by higher-order reasoning leading to literals of the form "~ ~ p", which are really the same as "p"
blanchet
parents:
40158
diff
changeset
|
450 |
handle Empty => raise Fail "Failed to find literal in th2" |
41491 | 451 |
val _ = trace_msg ctxt (fn () => " index_th2: " ^ string_of_int index_th2) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
452 |
in |
42348
187354e22c7d
improve on 0b05cc14c2cb: make sure that a literal variable "?foo" isn't accidentally renamed "?Q", which might be enough to confuse the new Skolemizer (cf. "Clausify.thy" example)
blanchet
parents:
42344
diff
changeset
|
453 |
resolve_inc_tyvars thy (select_literal index_th1 i_th1) index_th2 i_th2 |
42650
552eae49f97d
reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
blanchet
parents:
42616
diff
changeset
|
454 |
handle TERM (s, _) => raise METIS ("resolve_inf", s) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
455 |
end |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
456 |
end; |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
457 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
458 |
(* INFERENCE RULE: REFL *) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
459 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
460 |
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
|
461 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
462 |
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
|
463 |
val refl_idx = 1 + Thm.maxidx_of REFL_THM; |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
464 |
|
43094 | 465 |
fun refl_inf ctxt mode old_skolems sym_tab t = |
466 |
let |
|
467 |
val thy = Proof_Context.theory_of ctxt |
|
468 |
val i_t = singleton (hol_terms_from_metis ctxt mode old_skolems sym_tab) t |
|
469 |
val _ = trace_msg ctxt (fn () => " term: " ^ Syntax.string_of_term ctxt i_t) |
|
470 |
val c_t = cterm_incr_types thy refl_idx i_t |
|
471 |
in cterm_instantiate [(refl_x, c_t)] REFL_THM end |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
472 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
473 |
(* INFERENCE RULE: EQUALITY *) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
474 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
475 |
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
|
476 |
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
|
477 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
478 |
val metis_eq = Metis_Term.Fn ("=", []); |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
479 |
|
43093 | 480 |
(* Equality has no type arguments *) |
481 |
fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0 |
|
482 |
| get_ty_arg_size thy (Const (s, _)) = |
|
483 |
(num_type_args thy s handle TYPE _ => 0) |
|
484 |
| get_ty_arg_size _ _ = 0 |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
485 |
|
43094 | 486 |
fun equality_inf ctxt mode old_skolems sym_tab (pos, atm) fp fr = |
42361 | 487 |
let val thy = Proof_Context.theory_of ctxt |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
488 |
val m_tm = Metis_Term.Fn atm |
43094 | 489 |
val [i_atm, i_tm] = |
490 |
hol_terms_from_metis ctxt mode old_skolems sym_tab [m_tm, fr] |
|
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
491 |
val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
492 |
fun replace_item_list lx 0 (_::ls) = lx::ls |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
493 |
| replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls |
43104
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
494 |
fun path_finder_fail mode tm ps t = |
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
495 |
raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^ |
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
496 |
"equality_inf, path_finder_" ^ string_of_mode mode ^ |
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
497 |
": path = " ^ space_implode " " (map string_of_int ps) ^ |
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
498 |
" isa-term: " ^ Syntax.string_of_term ctxt tm ^ |
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
499 |
(case t of |
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
500 |
SOME t => " fol-term: " ^ Metis_Term.toString t |
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
501 |
| NONE => "")) |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
502 |
fun path_finder_FO tm [] = (tm, Bound 0) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
503 |
| path_finder_FO tm (p::ps) = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
504 |
let val (tm1,args) = strip_comb tm |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
505 |
val adjustment = get_ty_arg_size thy tm1 |
43094 | 506 |
val p' = if adjustment > p then p else p - adjustment |
42364 | 507 |
val tm_p = nth args p' |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
508 |
handle Subscript => |
42650
552eae49f97d
reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
blanchet
parents:
42616
diff
changeset
|
509 |
raise METIS ("equality_inf", |
552eae49f97d
reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
blanchet
parents:
42616
diff
changeset
|
510 |
string_of_int p ^ " adj " ^ |
552eae49f97d
reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
blanchet
parents:
42616
diff
changeset
|
511 |
string_of_int adjustment ^ " term " ^ |
552eae49f97d
reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
blanchet
parents:
42616
diff
changeset
|
512 |
Syntax.string_of_term ctxt tm) |
41491 | 513 |
val _ = trace_msg ctxt (fn () => "path_finder: " ^ string_of_int p ^ |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
514 |
" " ^ Syntax.string_of_term ctxt tm_p) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
515 |
val (r,t) = path_finder_FO tm_p ps |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
516 |
in |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
517 |
(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
|
518 |
end |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
519 |
fun path_finder_HO tm [] = (tm, Bound 0) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
520 |
| 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
|
521 |
| path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps) |
43104
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
522 |
| path_finder_HO tm ps = path_finder_fail HO tm ps NONE |
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
523 |
fun path_finder_FT tm [] _ = (tm, Bound 0) |
43104
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
524 |
| path_finder_FT tm (0::ps) (Metis_Term.Fn (":", [t1, _])) = |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
525 |
path_finder_FT tm ps t1 |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
526 |
| 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
|
527 |
(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
|
528 |
| 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
|
529 |
(fn(x,y) => (x, t$y)) (path_finder_FT u ps t2) |
43104
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
530 |
| path_finder_FT tm ps t = path_finder_fail FT tm ps (SOME t) |
43103 | 531 |
fun path_finder_MX tm [] _ = (tm, Bound 0) |
532 |
| path_finder_MX tm (p :: ps) (t as Metis_Term.Fn (s, ts)) = |
|
43130
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
533 |
let val s = s |> unmangled_const_name in |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
534 |
if s = metis_type_tag orelse s = prefixed_type_tag_name then |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
535 |
path_finder_MX tm ps (nth ts p) |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
536 |
else if s = metis_app_op orelse s = prefixed_app_op_name then |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
537 |
let |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
538 |
val (tm1, tm2) = dest_comb tm |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
539 |
val p' = p - (length ts - 2) |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
540 |
in |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
541 |
if p' = 0 then |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
542 |
path_finder_MX tm1 ps (nth ts p) ||> (fn y => y $ tm2) |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
543 |
else |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
544 |
path_finder_MX tm2 ps (nth ts p) ||> (fn y => tm1 $ y) |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
545 |
end |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
546 |
else |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
547 |
let |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
548 |
val (tm1, args) = strip_comb tm |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
549 |
val adjustment = length ts - length args |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
550 |
val p' = if adjustment > p then p else p - adjustment |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
551 |
val tm_p = nth args p' |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
552 |
handle Subscript => |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
553 |
path_finder_fail MX tm (p :: ps) (SOME t) |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
554 |
val _ = trace_msg ctxt (fn () => |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
555 |
"path_finder: " ^ string_of_int p ^ " " ^ |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
556 |
Syntax.string_of_term ctxt tm_p) |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
557 |
val (r, t) = path_finder_MX tm_p ps (nth ts p) |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
558 |
in (r, list_comb (tm1, replace_item_list t p' args)) end |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
559 |
end |
43104
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
560 |
| path_finder_MX tm ps t = path_finder_fail MX tm ps (SOME t) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
561 |
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
|
562 |
| 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
|
563 |
(*equality: not curried, as other predicates are*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
564 |
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
|
565 |
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
|
566 |
| path_finder HO tm (_ :: ps) (Metis_Term.Fn ("{}", [_])) = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
567 |
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
|
568 |
| 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
|
569 |
(Metis_Term.Fn ("=", [t1,t2])) = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
570 |
(*equality: not curried, as other predicates are*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
571 |
if p=0 then path_finder_FT tm (0::1::ps) |
43094 | 572 |
(Metis_Term.Fn (metis_app_op, [Metis_Term.Fn (metis_app_op, [metis_eq,t1]), t2])) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
573 |
(*select first operand*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
574 |
else path_finder_FT tm (p::ps) |
43094 | 575 |
(Metis_Term.Fn (metis_app_op, [metis_eq, t2])) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
576 |
(*1 selects second operand*) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
577 |
| 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
|
578 |
(*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
|
579 |
| path_finder FT tm ps t = path_finder_FT tm ps t (*really an error case!*) |
43103 | 580 |
| path_finder MX tm ps t = path_finder_MX tm ps t |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
581 |
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
|
582 |
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
|
583 |
in (tm, nt $ tm_rslt) end |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
584 |
| 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
|
585 |
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
|
586 |
val tm_abs = Abs ("x", type_of tm_subst, body) |
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
587 |
val _ = trace_msg ctxt (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs) |
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
588 |
val _ = trace_msg ctxt (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm) |
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
589 |
val _ = trace_msg ctxt (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
590 |
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
|
591 |
val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em) |
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
592 |
val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst') |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
593 |
val eq_terms = map (pairself (cterm_of thy)) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
594 |
(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
|
595 |
in cterm_instantiate eq_terms subst' end; |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
596 |
|
43094 | 597 |
val factor = Seq.hd o distinct_subgoals_tac |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
598 |
|
43094 | 599 |
fun one_step ctxt mode old_skolems sym_tab th_pairs p = |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
600 |
case p of |
43094 | 601 |
(fol_th, Metis_Proof.Axiom _) => axiom_inf th_pairs fol_th |> factor |
602 |
| (_, Metis_Proof.Assume f_atm) => |
|
603 |
assume_inf ctxt mode old_skolems sym_tab f_atm |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
604 |
| (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) => |
43094 | 605 |
inst_inf ctxt mode old_skolems sym_tab th_pairs f_subst f_th1 |> factor |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
606 |
| (_, Metis_Proof.Resolve(f_atm, f_th1, f_th2)) => |
43094 | 607 |
resolve_inf ctxt mode old_skolems sym_tab th_pairs f_atm f_th1 f_th2 |
608 |
|> factor |
|
609 |
| (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode old_skolems sym_tab f_tm |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
610 |
| (_, Metis_Proof.Equality (f_lit, f_p, f_r)) => |
43094 | 611 |
equality_inf ctxt mode old_skolems sym_tab f_lit f_p f_r |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
612 |
|
39893 | 613 |
fun flexflex_first_order th = |
614 |
case Thm.tpairs_of th of |
|
615 |
[] => th |
|
616 |
| pairs => |
|
617 |
let val thy = theory_of_thm th |
|
618 |
val (_, tenv) = |
|
619 |
fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty) |
|
620 |
val t_pairs = map Meson.term_pair_of (Vartab.dest tenv) |
|
621 |
val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th |
|
622 |
in th' end |
|
623 |
handle THM _ => th; |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
624 |
|
39895
a91a84b1dfdd
reintroduced code that keeps track of whether the Isabelle and Metis proofs are in sync -- generalized to work with the new skolemizer
blanchet
parents:
39893
diff
changeset
|
625 |
fun is_metis_literal_genuine (_, (s, _)) = not (String.isPrefix class_prefix s) |
a91a84b1dfdd
reintroduced code that keeps track of whether the Isabelle and Metis proofs are in sync -- generalized to work with the new skolemizer
blanchet
parents:
39893
diff
changeset
|
626 |
fun is_isabelle_literal_genuine t = |
39953
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39946
diff
changeset
|
627 |
case t of _ $ (Const (@{const_name Meson.skolem}, _) $ _) => false | _ => true |
39895
a91a84b1dfdd
reintroduced code that keeps track of whether the Isabelle and Metis proofs are in sync -- generalized to work with the new skolemizer
blanchet
parents:
39893
diff
changeset
|
628 |
|
a91a84b1dfdd
reintroduced code that keeps track of whether the Isabelle and Metis proofs are in sync -- generalized to work with the new skolemizer
blanchet
parents:
39893
diff
changeset
|
629 |
fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0 |
a91a84b1dfdd
reintroduced code that keeps track of whether the Isabelle and Metis proofs are in sync -- generalized to work with the new skolemizer
blanchet
parents:
39893
diff
changeset
|
630 |
|
42333 | 631 |
(* Seldomly needed hack. A Metis clause is represented as a set, so duplicate |
632 |
disjuncts are impossible. In the Isabelle proof, in spite of efforts to |
|
633 |
eliminate them, duplicates sometimes appear with slightly different (but |
|
634 |
unifiable) types. *) |
|
635 |
fun resynchronize ctxt fol_th th = |
|
636 |
let |
|
637 |
val num_metis_lits = |
|
638 |
count is_metis_literal_genuine |
|
639 |
(Metis_LiteralSet.toList (Metis_Thm.clause fol_th)) |
|
640 |
val num_isabelle_lits = count is_isabelle_literal_genuine (prems_of th) |
|
641 |
in |
|
642 |
if num_metis_lits >= num_isabelle_lits then |
|
643 |
th |
|
644 |
else |
|
645 |
let |
|
646 |
val (prems0, concl) = th |> prop_of |> Logic.strip_horn |
|
43134
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43130
diff
changeset
|
647 |
val prems = prems0 |> distinct untyped_aconv |
42333 | 648 |
val goal = Logic.list_implies (prems, concl) |
649 |
in |
|
650 |
if length prems = length prems0 then |
|
42650
552eae49f97d
reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
blanchet
parents:
42616
diff
changeset
|
651 |
raise METIS ("resynchronize", "Out of sync") |
42333 | 652 |
else |
653 |
Goal.prove ctxt [] [] goal (K (cut_rules_tac [th] 1 |
|
654 |
THEN ALLGOALS assume_tac)) |
|
655 |
|> resynchronize ctxt fol_th |
|
656 |
end |
|
657 |
end |
|
658 |
||
43094 | 659 |
fun replay_one_inference ctxt mode old_skolems sym_tab (fol_th, inf) th_pairs = |
660 |
if not (null th_pairs) andalso |
|
661 |
prop_of (snd (hd th_pairs)) aconv @{prop False} then |
|
40868
177cd660abb7
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents:
40724
diff
changeset
|
662 |
(* Isabelle sometimes identifies literals (premises) that are distinct in |
177cd660abb7
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents:
40724
diff
changeset
|
663 |
Metis (e.g., because of type variables). We give the Isabelle proof the |
177cd660abb7
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents:
40724
diff
changeset
|
664 |
benefice of the doubt. *) |
43094 | 665 |
th_pairs |
40868
177cd660abb7
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents:
40724
diff
changeset
|
666 |
else |
177cd660abb7
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents:
40724
diff
changeset
|
667 |
let |
177cd660abb7
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents:
40724
diff
changeset
|
668 |
val _ = trace_msg ctxt |
177cd660abb7
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents:
40724
diff
changeset
|
669 |
(fn () => "=============================================") |
177cd660abb7
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents:
40724
diff
changeset
|
670 |
val _ = trace_msg ctxt |
177cd660abb7
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents:
40724
diff
changeset
|
671 |
(fn () => "METIS THM: " ^ Metis_Thm.toString fol_th) |
177cd660abb7
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents:
40724
diff
changeset
|
672 |
val _ = trace_msg ctxt |
177cd660abb7
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents:
40724
diff
changeset
|
673 |
(fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf) |
43094 | 674 |
val th = one_step ctxt mode old_skolems sym_tab th_pairs (fol_th, inf) |
40868
177cd660abb7
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents:
40724
diff
changeset
|
675 |
|> flexflex_first_order |
42333 | 676 |
|> resynchronize ctxt fol_th |
40868
177cd660abb7
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents:
40724
diff
changeset
|
677 |
val _ = trace_msg ctxt |
177cd660abb7
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents:
40724
diff
changeset
|
678 |
(fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th) |
177cd660abb7
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents:
40724
diff
changeset
|
679 |
val _ = trace_msg ctxt |
177cd660abb7
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
blanchet
parents:
40724
diff
changeset
|
680 |
(fn () => "=============================================") |
43094 | 681 |
in (fol_th, th) :: th_pairs end |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
682 |
|
42342
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
683 |
(* It is normally sufficient to apply "assume_tac" to unify the conclusion with |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
684 |
one of the premises. Unfortunately, this sometimes yields "Variable |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
685 |
?SK_a_b_c_x has two distinct types" errors. To avoid this, we instantiate the |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
686 |
variables before applying "assume_tac". Typical constraints are of the form |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
687 |
?SK_a_b_c_x SK_d_e_f_y ... SK_a_b_c_x ... SK_g_h_i_z =?= SK_a_b_c_x, |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
688 |
where the nonvariables are goal parameters. *) |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
689 |
fun unify_first_prem_with_concl thy i th = |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
690 |
let |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
691 |
val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
692 |
val prem = goal |> Logic.strip_assums_hyp |> hd |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
693 |
val concl = goal |> Logic.strip_assums_concl |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
694 |
fun pair_untyped_aconv (t1, t2) (u1, u2) = |
43134
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43130
diff
changeset
|
695 |
untyped_aconv (t1, u1) andalso untyped_aconv (t2, u2) |
42342
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
696 |
fun add_terms tp inst = |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
697 |
if exists (pair_untyped_aconv tp) inst then inst |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
698 |
else tp :: map (apsnd (subst_atomic [tp])) inst |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
699 |
fun is_flex t = |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
700 |
case strip_comb t of |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
701 |
(Var _, args) => forall is_Bound args |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
702 |
| _ => false |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
703 |
fun unify_flex flex rigid = |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
704 |
case strip_comb flex of |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
705 |
(Var (z as (_, T)), args) => |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
706 |
add_terms (Var z, |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
707 |
fold_rev (curry absdummy) (take (length args) (binder_types T)) rigid) |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
708 |
| _ => I |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
709 |
fun unify_potential_flex comb atom = |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
710 |
if is_flex comb then unify_flex comb atom |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
711 |
else if is_Var atom then add_terms (atom, comb) |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
712 |
else I |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
713 |
fun unify_terms (t, u) = |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
714 |
case (t, u) of |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
715 |
(t1 $ t2, u1 $ u2) => |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
716 |
if is_flex t then unify_flex t u |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
717 |
else if is_flex u then unify_flex u t |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
718 |
else fold unify_terms [(t1, u1), (t2, u2)] |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
719 |
| (_ $ _, _) => unify_potential_flex t u |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
720 |
| (_, _ $ _) => unify_potential_flex u t |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
721 |
| (Var _, _) => add_terms (t, u) |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
722 |
| (_, Var _) => add_terms (u, t) |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
723 |
| _ => I |
42344
4a58173ffb99
"unify_first_prem_with_concl" (cf. 9ceb585c097a) sometimes throws an exception, but it is very rarely needed -- catch the exception for now
blanchet
parents:
42342
diff
changeset
|
724 |
val t_inst = |
4a58173ffb99
"unify_first_prem_with_concl" (cf. 9ceb585c097a) sometimes throws an exception, but it is very rarely needed -- catch the exception for now
blanchet
parents:
42342
diff
changeset
|
725 |
[] |> try (unify_terms (prem, concl) #> map (pairself (cterm_of thy))) |
4a58173ffb99
"unify_first_prem_with_concl" (cf. 9ceb585c097a) sometimes throws an exception, but it is very rarely needed -- catch the exception for now
blanchet
parents:
42342
diff
changeset
|
726 |
|> the_default [] (* FIXME *) |
42342
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
727 |
in th |> cterm_instantiate t_inst end |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
728 |
|
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
729 |
val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast} |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
730 |
|
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
731 |
fun copy_prems_tac [] ns i = |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
732 |
if forall (curry (op =) 1) ns then all_tac else copy_prems_tac (rev ns) [] i |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
733 |
| copy_prems_tac (1 :: ms) ns i = |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
734 |
rotate_tac 1 i THEN copy_prems_tac ms (1 :: ns) i |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
735 |
| copy_prems_tac (m :: ms) ns i = |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
736 |
etac copy_prem i THEN copy_prems_tac ms (m div 2 :: (m + 1) div 2 :: ns) i |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
737 |
|
42271
7d08265f181d
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset
|
738 |
(* Metis generates variables of the form _nnn. *) |
7d08265f181d
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset
|
739 |
val is_metis_fresh_variable = String.isPrefix "_" |
7d08265f181d
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset
|
740 |
|
40258
2c0d8fe36c21
make handling of parameters more robust, by querying the goal
blanchet
parents:
40221
diff
changeset
|
741 |
fun instantiate_forall_tac thy t i st = |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
742 |
let |
40258
2c0d8fe36c21
make handling of parameters more robust, by querying the goal
blanchet
parents:
40221
diff
changeset
|
743 |
val params = Logic.strip_params (Logic.get_goal (prop_of st) i) |> rev |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
744 |
fun repair (t as (Var ((s, _), _))) = |
40258
2c0d8fe36c21
make handling of parameters more robust, by querying the goal
blanchet
parents:
40221
diff
changeset
|
745 |
(case find_index (fn (s', _) => s' = s) params of |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
746 |
~1 => t |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
747 |
| j => Bound j) |
40261
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset
|
748 |
| repair (t $ u) = |
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset
|
749 |
(case (repair t, repair u) of |
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset
|
750 |
(t as Bound j, u as Bound k) => |
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset
|
751 |
(* This is a rather subtle trick to repair the discrepancy between |
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset
|
752 |
the fully skolemized term that MESON gives us (where existentials |
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset
|
753 |
were pulled out) and the reality. *) |
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset
|
754 |
if k > j then t else t $ u |
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset
|
755 |
| (t, u) => t $ u) |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
756 |
| repair t = t |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
757 |
val t' = t |> repair |> fold (curry absdummy) (map snd params) |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
758 |
fun do_instantiate th = |
42270 | 759 |
case Term.add_vars (prop_of th) [] |
42271
7d08265f181d
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset
|
760 |
|> filter_out ((Meson_Clausify.is_zapped_var_name orf |
7d08265f181d
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset
|
761 |
is_metis_fresh_variable) o fst o fst) of |
42270 | 762 |
[] => th |
42271
7d08265f181d
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset
|
763 |
| [var as (_, T)] => |
7d08265f181d
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset
|
764 |
let |
7d08265f181d
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset
|
765 |
val var_binder_Ts = T |> binder_types |> take (length params) |> rev |
7d08265f181d
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset
|
766 |
val var_body_T = T |> funpow (length params) range_type |
7d08265f181d
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset
|
767 |
val tyenv = |
7d08265f181d
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset
|
768 |
Vartab.empty |> Type.raw_unifys (fastype_of t :: map snd params, |
7d08265f181d
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset
|
769 |
var_body_T :: var_binder_Ts) |
7d08265f181d
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset
|
770 |
val env = |
7d08265f181d
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset
|
771 |
Envir.Envir {maxidx = Vartab.fold (Integer.max o snd o fst) tyenv 0, |
7d08265f181d
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset
|
772 |
tenv = Vartab.empty, tyenv = tyenv} |
7d08265f181d
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset
|
773 |
val ty_inst = |
7d08265f181d
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset
|
774 |
Vartab.fold (fn (x, (S, T)) => |
7d08265f181d
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset
|
775 |
cons (pairself (ctyp_of thy) (TVar (x, S), T))) |
7d08265f181d
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset
|
776 |
tyenv [] |
7d08265f181d
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset
|
777 |
val t_inst = |
7d08265f181d
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset
|
778 |
[pairself (cterm_of thy o Envir.norm_term env) (Var var, t')] |
42342
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
779 |
in th |> instantiate (ty_inst, t_inst) end |
42271
7d08265f181d
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset
|
780 |
| _ => raise Fail "expected a single non-zapped, non-Metis Var" |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
781 |
in |
42271
7d08265f181d
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset
|
782 |
(DETERM (etac @{thm allE} i THEN rotate_tac ~1 i) |
40258
2c0d8fe36c21
make handling of parameters more robust, by querying the goal
blanchet
parents:
40221
diff
changeset
|
783 |
THEN PRIMITIVE do_instantiate) st |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
784 |
end |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
785 |
|
41135 | 786 |
fun fix_exists_tac t = |
40261
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset
|
787 |
etac @{thm exE} |
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset
|
788 |
THEN' rename_tac [t |> dest_Var |> fst |> fst] |
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset
|
789 |
|
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset
|
790 |
fun release_quantifier_tac thy (skolem, t) = |
41135 | 791 |
(if skolem then fix_exists_tac else instantiate_forall_tac thy) t |
40261
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset
|
792 |
|
40258
2c0d8fe36c21
make handling of parameters more robust, by querying the goal
blanchet
parents:
40221
diff
changeset
|
793 |
fun release_clusters_tac _ _ _ [] = K all_tac |
2c0d8fe36c21
make handling of parameters more robust, by querying the goal
blanchet
parents:
40221
diff
changeset
|
794 |
| release_clusters_tac thy ax_counts substs |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
795 |
((ax_no, cluster_no) :: clusters) = |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
796 |
let |
40261
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset
|
797 |
val cluster_of_var = |
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset
|
798 |
Meson_Clausify.cluster_of_zapped_var_name o fst o fst o dest_Var |
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset
|
799 |
fun in_right_cluster ((_, (cluster_no', _)), _) = cluster_no' = cluster_no |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
800 |
val cluster_substs = |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
801 |
substs |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
802 |
|> map_filter (fn (ax_no', (_, (_, tsubst))) => |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
803 |
if ax_no' = ax_no then |
40261
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset
|
804 |
tsubst |> map (apfst cluster_of_var) |
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset
|
805 |
|> filter (in_right_cluster o fst) |
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset
|
806 |
|> map (apfst snd) |
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset
|
807 |
|> SOME |
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset
|
808 |
else |
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset
|
809 |
NONE) |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
810 |
fun do_cluster_subst cluster_subst = |
40261
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset
|
811 |
map (release_quantifier_tac thy) cluster_subst @ [rotate_tac 1] |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
812 |
val first_prem = find_index (fn (ax_no', _) => ax_no' = ax_no) substs |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
813 |
in |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
814 |
rotate_tac first_prem |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
815 |
THEN' (EVERY' (maps do_cluster_subst cluster_substs)) |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
816 |
THEN' rotate_tac (~ first_prem - length cluster_substs) |
40258
2c0d8fe36c21
make handling of parameters more robust, by querying the goal
blanchet
parents:
40221
diff
changeset
|
817 |
THEN' release_clusters_tac thy ax_counts substs clusters |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
818 |
end |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
819 |
|
40264
b91e2e16d994
fixed order of quantifier instantiation in new Skolemizer
blanchet
parents:
40261
diff
changeset
|
820 |
fun cluster_key ((ax_no, (cluster_no, index_no)), skolem) = |
b91e2e16d994
fixed order of quantifier instantiation in new Skolemizer
blanchet
parents:
40261
diff
changeset
|
821 |
(ax_no, (cluster_no, (skolem, index_no))) |
b91e2e16d994
fixed order of quantifier instantiation in new Skolemizer
blanchet
parents:
40261
diff
changeset
|
822 |
fun cluster_ord p = |
b91e2e16d994
fixed order of quantifier instantiation in new Skolemizer
blanchet
parents:
40261
diff
changeset
|
823 |
prod_ord int_ord (prod_ord int_ord (prod_ord bool_ord int_ord)) |
b91e2e16d994
fixed order of quantifier instantiation in new Skolemizer
blanchet
parents:
40261
diff
changeset
|
824 |
(pairself cluster_key p) |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
825 |
|
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
826 |
val tysubst_ord = |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
827 |
list_ord (prod_ord Term_Ord.fast_indexname_ord |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
828 |
(prod_ord Term_Ord.sort_ord Term_Ord.typ_ord)) |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
829 |
|
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
830 |
structure Int_Tysubst_Table = |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
831 |
Table(type key = int * (indexname * (sort * typ)) list |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
832 |
val ord = prod_ord int_ord tysubst_ord) |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
833 |
|
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
834 |
structure Int_Pair_Graph = |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
835 |
Graph(type key = int * int val ord = prod_ord int_ord int_ord) |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
836 |
|
42271
7d08265f181d
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset
|
837 |
fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (axiom_no, index_no) |
40258
2c0d8fe36c21
make handling of parameters more robust, by querying the goal
blanchet
parents:
40221
diff
changeset
|
838 |
fun shuffle_ord p = prod_ord int_ord int_ord (pairself shuffle_key p) |
2c0d8fe36c21
make handling of parameters more robust, by querying the goal
blanchet
parents:
40221
diff
changeset
|
839 |
|
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
840 |
(* Attempts to derive the theorem "False" from a theorem of the form |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
841 |
"P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
842 |
specified axioms. The axioms have leading "All" and "Ex" quantifiers, which |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
843 |
must be eliminated first. *) |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
844 |
fun discharge_skolem_premises ctxt axioms prems_imp_false = |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
845 |
if prop_of prems_imp_false aconv @{prop False} then |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
846 |
prems_imp_false |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
847 |
else |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
848 |
let |
42361 | 849 |
val thy = Proof_Context.theory_of ctxt |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
850 |
fun match_term p = |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
851 |
let |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
852 |
val (tyenv, tenv) = |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
853 |
Pattern.first_order_match thy p (Vartab.empty, Vartab.empty) |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
854 |
val tsubst = |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
855 |
tenv |> Vartab.dest |
42099
447fa058ab22
avoid evil "export_without_context", which breaks if there are local "fixes"
blanchet
parents:
42098
diff
changeset
|
856 |
|> filter (Meson_Clausify.is_zapped_var_name o fst o fst) |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
857 |
|> sort (cluster_ord |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
858 |
o pairself (Meson_Clausify.cluster_of_zapped_var_name |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
859 |
o fst o fst)) |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
860 |
|> map (Meson.term_pair_of |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
861 |
#> pairself (Envir.subst_term_types tyenv)) |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
862 |
val tysubst = tyenv |> Vartab.dest |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
863 |
in (tysubst, tsubst) end |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
864 |
fun subst_info_for_prem subgoal_no prem = |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
865 |
case prem of |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
866 |
_ $ (Const (@{const_name Meson.skolem}, _) $ (_ $ t $ num)) => |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
867 |
let val ax_no = HOLogic.dest_nat num in |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
868 |
(ax_no, (subgoal_no, |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
869 |
match_term (nth axioms ax_no |> the |> snd, t))) |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
870 |
end |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
871 |
| _ => raise TERM ("discharge_skolem_premises: Malformed premise", |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
872 |
[prem]) |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
873 |
fun cluster_of_var_name skolem s = |
42098
f978caf60bbe
more robust handling of variables in new Skolemizer
blanchet
parents:
41491
diff
changeset
|
874 |
case try Meson_Clausify.cluster_of_zapped_var_name s of |
f978caf60bbe
more robust handling of variables in new Skolemizer
blanchet
parents:
41491
diff
changeset
|
875 |
NONE => NONE |
f978caf60bbe
more robust handling of variables in new Skolemizer
blanchet
parents:
41491
diff
changeset
|
876 |
| SOME ((ax_no, (cluster_no, _)), skolem') => |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
877 |
if skolem' = skolem andalso cluster_no > 0 then |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
878 |
SOME (ax_no, cluster_no) |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
879 |
else |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
880 |
NONE |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
881 |
fun clusters_in_term skolem t = |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
882 |
Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst) |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
883 |
fun deps_for_term_subst (var, t) = |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
884 |
case clusters_in_term false var of |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
885 |
[] => NONE |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
886 |
| [(ax_no, cluster_no)] => |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
887 |
SOME ((ax_no, cluster_no), |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
888 |
clusters_in_term true t |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
889 |
|> cluster_no > 1 ? cons (ax_no, cluster_no - 1)) |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
890 |
| _ => raise TERM ("discharge_skolem_premises: Expected Var", [var]) |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
891 |
val prems = Logic.strip_imp_prems (prop_of prems_imp_false) |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
892 |
val substs = prems |> map2 subst_info_for_prem (1 upto length prems) |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
893 |
|> sort (int_ord o pairself fst) |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
894 |
val depss = maps (map_filter deps_for_term_subst o snd o snd o snd) substs |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
895 |
val clusters = maps (op ::) depss |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
896 |
val ordered_clusters = |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
897 |
Int_Pair_Graph.empty |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
898 |
|> fold Int_Pair_Graph.default_node (map (rpair ()) clusters) |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
899 |
|> fold Int_Pair_Graph.add_deps_acyclic depss |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
900 |
|> Int_Pair_Graph.topological_order |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
901 |
handle Int_Pair_Graph.CYCLES _ => |
40158 | 902 |
error "Cannot replay Metis proof in Isabelle without \ |
903 |
\\"Hilbert_Choice\"." |
|
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
904 |
val ax_counts = |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
905 |
Int_Tysubst_Table.empty |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
906 |
|> fold (fn (ax_no, (_, (tysubst, _))) => |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
907 |
Int_Tysubst_Table.map_default ((ax_no, tysubst), 0) |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
908 |
(Integer.add 1)) substs |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
909 |
|> Int_Tysubst_Table.dest |
42339
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset
|
910 |
val needed_axiom_props = |
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset
|
911 |
0 upto length axioms - 1 ~~ axioms |
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset
|
912 |
|> map_filter (fn (_, NONE) => NONE |
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset
|
913 |
| (ax_no, SOME (_, t)) => |
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset
|
914 |
if exists (fn ((ax_no', _), n) => |
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset
|
915 |
ax_no' = ax_no andalso n > 0) |
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset
|
916 |
ax_counts then |
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset
|
917 |
SOME t |
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset
|
918 |
else |
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset
|
919 |
NONE) |
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset
|
920 |
val outer_param_names = |
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset
|
921 |
[] |> fold Term.add_var_names needed_axiom_props |
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset
|
922 |
|> filter (Meson_Clausify.is_zapped_var_name o fst) |
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset
|
923 |
|> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst)) |
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset
|
924 |
|> filter (fn (((_, (cluster_no, _)), skolem), _) => |
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset
|
925 |
cluster_no = 0 andalso skolem) |
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset
|
926 |
|> sort shuffle_ord |> map (fst o snd) |
42270 | 927 |
(* for debugging only: |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
928 |
fun string_for_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) = |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
929 |
"ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^ |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
930 |
"; tysubst: " ^ PolyML.makestring tysubst ^ "; tsubst: {" ^ |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
931 |
commas (map ((fn (s, t) => s ^ " |-> " ^ t) |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
932 |
o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}" |
40264
b91e2e16d994
fixed order of quantifier instantiation in new Skolemizer
blanchet
parents:
40261
diff
changeset
|
933 |
val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters) |
b91e2e16d994
fixed order of quantifier instantiation in new Skolemizer
blanchet
parents:
40261
diff
changeset
|
934 |
val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts) |
42339
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset
|
935 |
val _ = tracing ("OUTER PARAMS: " ^ PolyML.makestring outer_param_names) |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
936 |
val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^ |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
937 |
cat_lines (map string_for_subst_info substs)) |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
938 |
*) |
42271
7d08265f181d
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset
|
939 |
fun cut_and_ex_tac axiom = |
7d08265f181d
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset
|
940 |
cut_rules_tac [axiom] 1 |
7d08265f181d
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset
|
941 |
THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1) |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
942 |
fun rotation_for_subgoal i = |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
943 |
find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
944 |
in |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
945 |
Goal.prove ctxt [] [] @{prop False} |
42271
7d08265f181d
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset
|
946 |
(K (DETERM (EVERY (map (cut_and_ex_tac o fst o the o nth axioms o fst |
7d08265f181d
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset
|
947 |
o fst) ax_counts) |
7d08265f181d
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset
|
948 |
THEN rename_tac outer_param_names 1 |
7d08265f181d
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset
|
949 |
THEN copy_prems_tac (map snd ax_counts) [] 1) |
40258
2c0d8fe36c21
make handling of parameters more robust, by querying the goal
blanchet
parents:
40221
diff
changeset
|
950 |
THEN release_clusters_tac thy ax_counts substs ordered_clusters 1 |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
951 |
THEN match_tac [prems_imp_false] 1 |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
952 |
THEN ALLGOALS (fn i => |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
953 |
rtac @{thm Meson.skolem_COMBK_I} i |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
954 |
THEN rotate_tac (rotation_for_subgoal i) i |
42342
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42341
diff
changeset
|
955 |
THEN PRIMITIVE (unify_first_prem_with_concl thy i) |
42271
7d08265f181d
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
blanchet
parents:
42270
diff
changeset
|
956 |
THEN assume_tac i |
42270 | 957 |
THEN flexflex_tac))) |
40158 | 958 |
handle ERROR _ => |
959 |
error ("Cannot replay Metis proof in Isabelle:\n\ |
|
960 |
\Error when discharging Skolem assumptions.") |
|
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
961 |
end |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
962 |
|
39495
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset
|
963 |
end; |