author | wenzelm |
Mon, 27 Jul 2015 11:30:10 +0200 | |
changeset 60795 | c24fa03f4c71 |
parent 60794 | f21f70d24844 |
child 60949 | ccbf9379e355 |
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 |
46320 | 12 |
type type_enc = ATP_Problem_Generate.type_enc |
44492
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44241
diff
changeset
|
13 |
|
50875
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
48132
diff
changeset
|
14 |
exception METIS_RECONSTRUCT of string * string |
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
|
15 |
|
57408 | 16 |
val hol_clause_of_metis : Proof.context -> type_enc -> int Symtab.table -> |
17 |
(string * term) list * (string * term) list -> Metis_Thm.thm -> term |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
18 |
val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a |
57408 | 19 |
val replay_one_inference : Proof.context -> type_enc -> |
20 |
(string * term) list * (string * term) list -> int Symtab.table -> |
|
21 |
Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list -> |
|
22 |
(Metis_Thm.thm * thm) list |
|
23 |
val discharge_skolem_premises : Proof.context -> (thm * term) option list -> thm -> thm |
|
39495
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset
|
24 |
end; |
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset
|
25 |
|
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset
|
26 |
structure Metis_Reconstruct : METIS_RECONSTRUCT = |
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset
|
27 |
struct |
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset
|
28 |
|
43094 | 29 |
open ATP_Problem |
46320 | 30 |
open ATP_Problem_Generate |
31 |
open ATP_Proof_Reconstruct |
|
32 |
open Metis_Generate |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
33 |
|
50875
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
48132
diff
changeset
|
34 |
exception METIS_RECONSTRUCT of string * string |
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
|
35 |
|
57400 | 36 |
val meta_not_not = @{thms not_not[THEN eq_reflection]} |
37 |
||
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset
|
38 |
fun atp_name_of_metis type_enc s = |
57408 | 39 |
(case find_first (fn (_, (f, _)) => f type_enc = s) metis_name_table of |
43104
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
40 |
SOME ((s, _), (_, swap)) => (s, swap) |
57408 | 41 |
| _ => (s, false)) |
42 |
||
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset
|
43 |
fun atp_term_of_metis type_enc (Metis_Term.Fn (s, tms)) = |
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset
|
44 |
let val (s, swap) = atp_name_of_metis type_enc (Metis_Name.toString s) in |
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset
|
45 |
ATerm ((s, []), tms |> map (atp_term_of_metis type_enc) |> swap ? rev) |
43104
81d1b15aa0ae
use ":" for type information (looks good in Metis's output) and handle it in new path finder
blanchet
parents:
43103
diff
changeset
|
46 |
end |
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset
|
47 |
| atp_term_of_metis _ (Metis_Term.Var s) = |
48132
9aa0fad4e864
added type arguments to "ATerm" constructor -- but don't use them yet
blanchet
parents:
46708
diff
changeset
|
48 |
ATerm ((Metis_Name.toString s, []), []) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
49 |
|
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset
|
50 |
fun hol_term_of_metis ctxt type_enc sym_tab = |
57255
488046fdda59
add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents:
55523
diff
changeset
|
51 |
atp_term_of_metis type_enc #> term_of_atp ctxt ATP_Problem.CNF type_enc false sym_tab NONE |
43094 | 52 |
|
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset
|
53 |
fun atp_literal_of_metis type_enc (pos, atom) = |
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset
|
54 |
atom |> Metis_Term.Fn |> atp_term_of_metis type_enc |
44492
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44241
diff
changeset
|
55 |
|> AAtom |> not pos ? mk_anot |
57408 | 56 |
|
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset
|
57 |
fun atp_clause_of_metis _ [] = AAtom (ATerm ((tptp_false, []), [])) |
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset
|
58 |
| atp_clause_of_metis type_enc lits = |
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset
|
59 |
lits |> map (atp_literal_of_metis type_enc) |> mk_aconns AOr |
43136
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset
|
60 |
|
45508 | 61 |
fun polish_hol_terms ctxt (lifted, old_skolems) = |
45569
eb30a5490543
wrap lambdas earlier, to get more control over beta/eta
blanchet
parents:
45511
diff
changeset
|
62 |
map (reveal_lam_lifted lifted #> reveal_old_skolem_terms old_skolems) |
43212 | 63 |
#> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt) |
43184 | 64 |
|
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset
|
65 |
fun hol_clause_of_metis ctxt type_enc sym_tab concealed = |
43159
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43136
diff
changeset
|
66 |
Metis_Thm.clause |
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43136
diff
changeset
|
67 |
#> Metis_LiteralSet.toList |
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset
|
68 |
#> atp_clause_of_metis type_enc |
57255
488046fdda59
add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents:
55523
diff
changeset
|
69 |
#> prop_of_atp ctxt ATP_Problem.CNF type_enc false sym_tab |
45508 | 70 |
#> singleton (polish_hol_terms ctxt concealed) |
43136
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset
|
71 |
|
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset
|
72 |
fun hol_terms_of_metis ctxt type_enc concealed sym_tab fol_tms = |
57408 | 73 |
let |
74 |
val ts = map (hol_term_of_metis ctxt type_enc sym_tab) fol_tms |
|
75 |
val _ = trace_msg ctxt (fn () => " calling type inference:") |
|
76 |
val _ = app (fn t => trace_msg ctxt (fn () => Syntax.string_of_term ctxt t)) ts |
|
77 |
val ts' = ts |> polish_hol_terms ctxt concealed |
|
78 |
val _ = app (fn t => trace_msg ctxt |
|
79 |
(fn () => " final term: " ^ Syntax.string_of_term ctxt t ^ |
|
80 |
" of type " ^ Syntax.string_of_typ ctxt (type_of t))) ts' |
|
81 |
in ts' end |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
82 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
83 |
(* ------------------------------------------------------------------------- *) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
84 |
(* FOL step Inference Rules *) |
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 |
|
43094 | 87 |
fun lookth th_pairs fth = |
88 |
the (AList.lookup (uncurry Metis_Thm.equal) th_pairs fth) |
|
57408 | 89 |
handle Option.Option => raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fth) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
90 |
|
59632 | 91 |
fun cterm_incr_types ctxt idx = |
92 |
Thm.cterm_of ctxt o map_types (Logic.incr_tvar idx) |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
93 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
94 |
(* INFERENCE RULE: AXIOM *) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
95 |
|
43212 | 96 |
(* This causes variables to have an index of 1 by default. See also |
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51998
diff
changeset
|
97 |
"term_of_atp" in "ATP_Proof_Reconstruct". *) |
43212 | 98 |
val axiom_inference = Thm.incr_indexes 1 oo lookth |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
99 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
100 |
(* INFERENCE RULE: ASSUME *) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
101 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
102 |
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
|
103 |
|
59632 | 104 |
fun inst_excluded_middle ctxt i_atom = |
57408 | 105 |
let |
106 |
val th = EXCLUDED_MIDDLE |
|
59582 | 107 |
val [vx] = Term.add_vars (Thm.prop_of th) [] |
57408 | 108 |
in |
60795 | 109 |
infer_instantiate_types ctxt [(vx, Thm.cterm_of ctxt i_atom)] th |
57408 | 110 |
end |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
111 |
|
45508 | 112 |
fun assume_inference ctxt type_enc concealed sym_tab atom = |
59632 | 113 |
inst_excluded_middle ctxt |
57408 | 114 |
(singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) (Metis_Term.Fn atom)) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
115 |
|
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
116 |
(* 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
|
117 |
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
|
118 |
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
|
119 |
can be inferred from terms. *) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
120 |
|
45508 | 121 |
fun inst_inference ctxt type_enc concealed sym_tab th_pairs fsubst th = |
57408 | 122 |
let |
123 |
val i_th = lookth th_pairs th |
|
59582 | 124 |
val i_th_vars = Term.add_vars (Thm.prop_of i_th) [] |
57408 | 125 |
|
126 |
fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars) |
|
127 |
fun subst_translation (x,y) = |
|
128 |
let |
|
129 |
val v = find_var x |
|
130 |
(* We call "polish_hol_terms" below. *) |
|
131 |
val t = hol_term_of_metis ctxt type_enc sym_tab y |
|
132 |
in |
|
59632 | 133 |
SOME (Thm.cterm_of ctxt (Var v), t) |
57408 | 134 |
end |
135 |
handle Option.Option => |
|
136 |
(trace_msg ctxt (fn () => |
|
137 |
"\"find_var\" failed for " ^ x ^ " in " ^ Display.string_of_thm ctxt i_th); |
|
138 |
NONE) |
|
139 |
| TYPE _ => |
|
140 |
(trace_msg ctxt (fn () => |
|
141 |
"\"hol_term_of_metis\" failed for " ^ x ^ " in " ^ Display.string_of_thm ctxt i_th); |
|
142 |
NONE) |
|
143 |
fun remove_typeinst (a, t) = |
|
144 |
let val a = Metis_Name.toString a in |
|
145 |
(case unprefix_and_unascii schematic_var_prefix a of |
|
146 |
SOME b => SOME (b, t) |
|
147 |
| NONE => |
|
148 |
(case unprefix_and_unascii tvar_prefix a of |
|
149 |
SOME _ => NONE (* type instantiations are forbidden *) |
|
150 |
| NONE => SOME (a, t) (* internal Metis var? *))) |
|
151 |
end |
|
152 |
val _ = trace_msg ctxt (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th) |
|
153 |
val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst) |
|
154 |
val (vars, tms) = |
|
155 |
ListPair.unzip (map_filter subst_translation substs) |
|
156 |
||> polish_hol_terms ctxt concealed |
|
59632 | 157 |
val ctm_of = cterm_incr_types ctxt (1 + Thm.maxidx_of i_th) |
57408 | 158 |
val substs' = ListPair.zip (vars, map ctm_of tms) |
159 |
val _ = trace_msg ctxt (fn () => |
|
160 |
cat_lines ("subst_translations:" :: |
|
161 |
(substs' |> map (fn (x, y) => |
|
59582 | 162 |
Syntax.string_of_term ctxt (Thm.term_of x) ^ " |-> " ^ |
163 |
Syntax.string_of_term ctxt (Thm.term_of y))))) |
|
57408 | 164 |
in |
60795 | 165 |
infer_instantiate_types ctxt (map (apfst (dest_Var o Thm.term_of)) substs') i_th |
57408 | 166 |
end |
50875
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
48132
diff
changeset
|
167 |
handle THM (msg, _, _) => raise METIS_RECONSTRUCT ("inst_inference", msg) |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
48132
diff
changeset
|
168 |
| ERROR msg => raise METIS_RECONSTRUCT ("inst_inference", msg) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
169 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
170 |
(* INFERENCE RULE: RESOLVE *) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
171 |
|
43330 | 172 |
(*Increment the indexes of only the type variables*) |
60363 | 173 |
fun incr_type_indexes ctxt inc th = |
57408 | 174 |
let |
175 |
val tvs = Term.add_tvars (Thm.full_prop_of th) [] |
|
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60363
diff
changeset
|
176 |
fun inc_tvar ((a, i), s) = (((a, i), s), Thm.ctyp_of ctxt (TVar ((a, i + inc), s))) |
57408 | 177 |
in |
178 |
Thm.instantiate (map inc_tvar tvs, []) th |
|
179 |
end |
|
43330 | 180 |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
181 |
(* 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
|
182 |
have an index of 1, and the use of RSN would increase this typically to 3. |
43300 | 183 |
Instantiations of those Vars could then fail. *) |
57400 | 184 |
fun resolve_inc_tyvars ctxt tha i thb = |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
185 |
let |
60363 | 186 |
val tha = incr_type_indexes ctxt (1 + Thm.maxidx_of thb) tha |
57400 | 187 |
fun res (tha, thb) = |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58839
diff
changeset
|
188 |
(case Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = true} |
59582 | 189 |
(false, tha, Thm.nprems_of tha) i thb |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
190 |
|> Seq.list_of |> distinct Thm.eq_thm of |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
191 |
[th] => th |
57400 | 192 |
| _ => |
193 |
let |
|
194 |
val thaa'bb' as [(tha', _), (thb', _)] = |
|
195 |
map (`(Local_Defs.unfold ctxt meta_not_not)) [tha, thb] |
|
196 |
in |
|
197 |
if forall Thm.eq_thm_prop thaa'bb' then |
|
198 |
raise THM ("resolve_inc_tyvars: unique result expected", i, [tha, thb]) |
|
199 |
else |
|
200 |
res (tha', thb') |
|
57408 | 201 |
end) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
202 |
in |
57400 | 203 |
res (tha, thb) |
52225
568b2cd65d50
resolve_inc_tyvars: back to old behavior before 0fa3b456a267 where types of equal Vars are *not* unified -- recover last example in src/HOL/Metis_Examples/Clausification.thy;
wenzelm
parents:
52223
diff
changeset
|
204 |
handle TERM z => |
57400 | 205 |
let |
206 |
val ps = [] |
|
59582 | 207 |
|> fold (Term.add_vars o Thm.prop_of) [tha, thb] |
57400 | 208 |
|> AList.group (op =) |
209 |
|> maps (fn ((s, _), T :: Ts) => map (fn T' => (Free (s, T), Free (s, T'))) Ts) |
|
210 |
|> rpair (Envir.empty ~1) |
|
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58839
diff
changeset
|
211 |
|-> fold (Pattern.unify (Context.Proof ctxt)) |
57400 | 212 |
|> Envir.type_env |> Vartab.dest |
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60363
diff
changeset
|
213 |
|> map (fn (x, (S, T)) => ((x, S), Thm.ctyp_of ctxt T)) |
57400 | 214 |
in |
215 |
(* The unifier, which is invoked from "Thm.bicompose", will sometimes refuse to unify |
|
216 |
"?a::?'a" with "?a::?'b" or "?a::nat" and throw a "TERM" exception (with "add_ffpair" as |
|
217 |
first argument). We then perform unification of the types of variables by hand and try |
|
218 |
again. We could do this the first time around but this error occurs seldom and we don't |
|
219 |
want to break existing proofs in subtle ways or slow them down. *) |
|
220 |
if null ps then raise TERM z |
|
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58963
diff
changeset
|
221 |
else res (apply2 (Drule.instantiate_normalize (ps, [])) (tha, thb)) |
57400 | 222 |
end |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
223 |
end |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
224 |
|
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
|
225 |
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
|
226 |
| s_not t = HOLogic.mk_not t |
43195
6dc58b3b73b5
improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents:
43187
diff
changeset
|
227 |
fun simp_not_not (@{const Trueprop} $ t) = @{const Trueprop} $ simp_not_not t |
6dc58b3b73b5
improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents:
43187
diff
changeset
|
228 |
| simp_not_not (@{const Not} $ t) = s_not (simp_not_not t) |
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
|
229 |
| simp_not_not t = t |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
230 |
|
43195
6dc58b3b73b5
improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents:
43187
diff
changeset
|
231 |
val normalize_literal = simp_not_not o Envir.eta_contract |
6dc58b3b73b5
improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents:
43187
diff
changeset
|
232 |
|
43187
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset
|
233 |
(* Find the relative location of an untyped term within a list of terms as a |
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset
|
234 |
1-based index. Returns 0 in case of failure. *) |
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
|
235 |
fun index_of_literal lit haystack = |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
236 |
let |
43195
6dc58b3b73b5
improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents:
43187
diff
changeset
|
237 |
fun match_lit normalize = |
43134
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43130
diff
changeset
|
238 |
HOLogic.dest_Trueprop #> normalize |
43301
8d7fc4a5b502
removed needless function that duplicated standard functionality, with a little unnecessary twist
blanchet
parents:
43300
diff
changeset
|
239 |
#> curry Term.aconv_untyped (lit |> normalize) |
43195
6dc58b3b73b5
improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents:
43187
diff
changeset
|
240 |
in |
6dc58b3b73b5
improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents:
43187
diff
changeset
|
241 |
(case find_index (match_lit I) haystack of |
6dc58b3b73b5
improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents:
43187
diff
changeset
|
242 |
~1 => find_index (match_lit (simp_not_not o Envir.eta_contract)) haystack |
6dc58b3b73b5
improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents:
43187
diff
changeset
|
243 |
| j => j) + 1 |
6dc58b3b73b5
improved correctness of handling of higher-order occurrences of "Not" in new Metis (and probably in old Metis)
blanchet
parents:
43187
diff
changeset
|
244 |
end |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
245 |
|
39893 | 246 |
(* Permute a rule's premises to move the i-th premise to the last position. *) |
247 |
fun make_last i th = |
|
59582 | 248 |
let val n = Thm.nprems_of th in |
54756 | 249 |
if i >= 1 andalso i <= n then Thm.permute_prems (i - 1) 1 th |
250 |
else raise THM ("select_literal", i, [th]) |
|
57408 | 251 |
end |
39893 | 252 |
|
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
|
253 |
(* 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
|
254 |
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
|
255 |
"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
|
256 |
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
|
257 |
necessary. FIXME. *) |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54501
diff
changeset
|
258 |
fun negate_head ctxt th = |
59582 | 259 |
if exists (fn t => t aconv @{prop "~ False"}) (Thm.prems_of th) then |
42349
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
42348
diff
changeset
|
260 |
(th RS @{thm select_FalseI}) |
54756 | 261 |
|> fold (rewrite_rule ctxt o single) @{thms not_atomize_select atomize_not_select} |
42349
721e85fd2db3
make 48170228f562 work also with "HO_Reas" examples
blanchet
parents:
42348
diff
changeset
|
262 |
else |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54501
diff
changeset
|
263 |
th |> fold (rewrite_rule ctxt o single) @{thms not_atomize atomize_not} |
39893 | 264 |
|
265 |
(* Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *) |
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54501
diff
changeset
|
266 |
fun select_literal ctxt = negate_head ctxt oo make_last |
39893 | 267 |
|
45508 | 268 |
fun resolve_inference ctxt type_enc concealed sym_tab th_pairs atom th1 th2 = |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
269 |
let |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58963
diff
changeset
|
270 |
val (i_th1, i_th2) = apply2 (lookth th_pairs) (th1, th2) |
43187
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset
|
271 |
val _ = trace_msg ctxt (fn () => |
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset
|
272 |
" isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1 ^ "\n\ |
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset
|
273 |
\ 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
|
274 |
in |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
275 |
(* Trivial cases where one operand is type info *) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
276 |
if Thm.eq_thm (TrueI, i_th1) then |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
277 |
i_th2 |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
278 |
else if Thm.eq_thm (TrueI, i_th2) then |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
279 |
i_th1 |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
280 |
else |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
281 |
let |
43187
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset
|
282 |
val i_atom = |
54756 | 283 |
singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) (Metis_Term.Fn atom) |
284 |
val _ = trace_msg ctxt (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atom) |
|
43187
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset
|
285 |
in |
59582 | 286 |
(case index_of_literal (s_not i_atom) (Thm.prems_of i_th1) of |
54756 | 287 |
0 => (trace_msg ctxt (fn () => "Failed to find literal in \"th1\""); i_th1) |
43187
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset
|
288 |
| j1 => |
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset
|
289 |
(trace_msg ctxt (fn () => " index th1: " ^ string_of_int j1); |
59582 | 290 |
(case index_of_literal i_atom (Thm.prems_of i_th2) of |
54756 | 291 |
0 => (trace_msg ctxt (fn () => "Failed to find literal in \"th2\""); i_th2) |
43187
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset
|
292 |
| j2 => |
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset
|
293 |
(trace_msg ctxt (fn () => " index th2: " ^ string_of_int j2); |
57400 | 294 |
resolve_inc_tyvars ctxt (select_literal ctxt j1 i_th1) j2 i_th2 |
57408 | 295 |
handle TERM (s, _) => raise METIS_RECONSTRUCT ("resolve_inference", s))))) |
43187
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset
|
296 |
end |
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset
|
297 |
end |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
298 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
299 |
(* INFERENCE RULE: REFL *) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
300 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
301 |
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
|
302 |
|
59632 | 303 |
val refl_x = Thm.cterm_of @{context} (Var (hd (Term.add_vars (Thm.prop_of REFL_THM) []))); |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
304 |
val refl_idx = 1 + Thm.maxidx_of REFL_THM; |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
305 |
|
45508 | 306 |
fun refl_inference ctxt type_enc concealed sym_tab t = |
43094 | 307 |
let |
54756 | 308 |
val i_t = singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) t |
43094 | 309 |
val _ = trace_msg ctxt (fn () => " term: " ^ Syntax.string_of_term ctxt i_t) |
59632 | 310 |
val c_t = cterm_incr_types ctxt refl_idx i_t |
60795 | 311 |
in infer_instantiate_types ctxt [(dest_Var (Thm.term_of refl_x), c_t)] REFL_THM end |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
312 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
313 |
(* INFERENCE RULE: EQUALITY *) |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
314 |
|
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
315 |
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
|
316 |
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
|
317 |
|
45508 | 318 |
fun equality_inference ctxt type_enc concealed sym_tab (pos, atom) fp fr = |
42361 | 319 |
let val thy = Proof_Context.theory_of ctxt |
43187
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset
|
320 |
val m_tm = Metis_Term.Fn atom |
54756 | 321 |
val [i_atom, i_tm] = hol_terms_of_metis ctxt type_enc concealed sym_tab [m_tm, fr] |
58070 | 322 |
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
|
323 |
fun replace_item_list lx 0 (_::ls) = lx::ls |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
324 |
| replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls |
43205 | 325 |
fun path_finder_fail tm ps t = |
50875
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
48132
diff
changeset
|
326 |
raise METIS_RECONSTRUCT ("equality_inference (path_finder)", |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
48132
diff
changeset
|
327 |
"path = " ^ space_implode " " (map string_of_int ps) ^ |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
48132
diff
changeset
|
328 |
" isa-term: " ^ Syntax.string_of_term ctxt tm ^ |
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
48132
diff
changeset
|
329 |
(case t of |
54756 | 330 |
SOME t => " fol-term: " ^ Metis_Term.toString t |
331 |
| NONE => "")) |
|
43212 | 332 |
fun path_finder tm [] _ = (tm, Bound 0) |
333 |
| path_finder tm (p :: ps) (t as Metis_Term.Fn (s, ts)) = |
|
43177 | 334 |
let |
43268
c0eaa8b9bff5
removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
blanchet
parents:
43262
diff
changeset
|
335 |
val s = s |> Metis_Name.toString |
45511
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
336 |
|> perhaps (try (unprefix_and_unascii const_prefix |
46392
676a4b4b6e73
implemented partial application aliases (for SPASS mainly)
blanchet
parents:
46320
diff
changeset
|
337 |
#> the #> unmangled_const_name #> hd)) |
43177 | 338 |
in |
339 |
if s = metis_predicator orelse s = predicator_name orelse |
|
44492
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44241
diff
changeset
|
340 |
s = metis_systematic_type_tag orelse s = metis_ad_hoc_type_tag |
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44241
diff
changeset
|
341 |
orelse s = type_tag_name then |
43212 | 342 |
path_finder tm ps (nth ts p) |
43177 | 343 |
else if s = metis_app_op orelse s = app_op_name then |
43130
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
344 |
let |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
345 |
val (tm1, tm2) = dest_comb tm |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
346 |
val p' = p - (length ts - 2) |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
347 |
in |
54756 | 348 |
if p' = 0 then path_finder tm1 ps (nth ts p) ||> (fn y => y $ tm2) |
349 |
else path_finder tm2 ps (nth ts p) ||> (fn y => tm1 $ y) |
|
43130
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
350 |
end |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
351 |
else |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
352 |
let |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
353 |
val (tm1, args) = strip_comb tm |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
354 |
val adjustment = length ts - length args |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
355 |
val p' = if adjustment > p then p else p - adjustment |
54756 | 356 |
val tm_p = nth args p' |
43278 | 357 |
handle General.Subscript => path_finder_fail tm (p :: ps) (SOME t) |
43130
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
358 |
val _ = trace_msg ctxt (fn () => |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
359 |
"path_finder: " ^ string_of_int p ^ " " ^ |
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
360 |
Syntax.string_of_term ctxt tm_p) |
43212 | 361 |
val (r, t) = path_finder tm_p ps (nth ts p) |
43130
d73fc2e55308
implemented missing hAPP and ti cases of new path finder
blanchet
parents:
43128
diff
changeset
|
362 |
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
|
363 |
end |
43212 | 364 |
| path_finder tm ps t = path_finder_fail tm ps (SOME t) |
365 |
val (tm_subst, body) = path_finder i_atom fp m_tm |
|
39498
e8aef7ea9cbb
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet
parents:
39497
diff
changeset
|
366 |
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
|
367 |
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
|
368 |
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
|
369 |
val _ = trace_msg ctxt (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst) |
54501 | 370 |
val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill-typed but gives right max*) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
371 |
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
|
372 |
val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst') |
59632 | 373 |
val eq_terms = |
374 |
map (apply2 (Thm.cterm_of ctxt)) |
|
375 |
(ListPair.zip (Misc_Legacy.term_vars (Thm.prop_of subst'), [tm_abs, tm_subst, i_tm])) |
|
57408 | 376 |
in |
60795 | 377 |
infer_instantiate_types ctxt (map (apfst (dest_Var o Thm.term_of)) eq_terms) subst' |
57408 | 378 |
end |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
379 |
|
43094 | 380 |
val factor = Seq.hd o distinct_subgoals_tac |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
381 |
|
45508 | 382 |
fun one_step ctxt type_enc concealed sym_tab th_pairs p = |
57408 | 383 |
(case p of |
43186 | 384 |
(fol_th, Metis_Proof.Axiom _) => axiom_inference th_pairs fol_th |> factor |
54756 | 385 |
| (_, Metis_Proof.Assume f_atom) => assume_inference ctxt type_enc concealed sym_tab f_atom |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
386 |
| (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) => |
54756 | 387 |
inst_inference ctxt type_enc concealed sym_tab th_pairs f_subst f_th1 |> factor |
43187
95bd1ef1331a
make resolution replay more robust, in case Metis distinguishes between two literals that are merged in Isabelle (e.g. because they carry more or less type annotations in Metis)
blanchet
parents:
43186
diff
changeset
|
388 |
| (_, Metis_Proof.Resolve(f_atom, f_th1, f_th2)) => |
54756 | 389 |
resolve_inference ctxt type_enc concealed sym_tab th_pairs f_atom f_th1 f_th2 |> factor |
390 |
| (_, Metis_Proof.Refl f_tm) => refl_inference ctxt type_enc concealed sym_tab f_tm |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
391 |
| (_, Metis_Proof.Equality (f_lit, f_p, f_r)) => |
57408 | 392 |
equality_inference ctxt type_enc concealed sym_tab f_lit f_p f_r) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
393 |
|
60363 | 394 |
fun flexflex_first_order ctxt th = |
54756 | 395 |
(case Thm.tpairs_of th of |
396 |
[] => th |
|
397 |
| pairs => |
|
59617 | 398 |
let |
60363 | 399 |
val thy = Proof_Context.theory_of ctxt |
59617 | 400 |
val (tyenv, tenv) = fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty) |
401 |
||
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60363
diff
changeset
|
402 |
fun mkT (v, (S, T)) = ((v, S), Thm.ctyp_of ctxt T) |
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60363
diff
changeset
|
403 |
fun mk (v, (T, t)) = ((v, Envir.subst_type tyenv T), Thm.cterm_of ctxt t) |
59617 | 404 |
|
405 |
val instsT = Vartab.fold (cons o mkT) tyenv [] |
|
406 |
val insts = Vartab.fold (cons o mk) tenv [] |
|
407 |
in |
|
408 |
Thm.instantiate (instsT, insts) th |
|
409 |
end |
|
410 |
handle THM _ => th) |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
411 |
|
43268
c0eaa8b9bff5
removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
blanchet
parents:
43262
diff
changeset
|
412 |
fun is_metis_literal_genuine (_, (s, _)) = |
c0eaa8b9bff5
removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
blanchet
parents:
43262
diff
changeset
|
413 |
not (String.isPrefix class_prefix (Metis_Name.toString s)) |
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
|
414 |
fun is_isabelle_literal_genuine t = |
54756 | 415 |
(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
|
416 |
|
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
|
417 |
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
|
418 |
|
42333 | 419 |
(* Seldomly needed hack. A Metis clause is represented as a set, so duplicate |
420 |
disjuncts are impossible. In the Isabelle proof, in spite of efforts to |
|
421 |
eliminate them, duplicates sometimes appear with slightly different (but |
|
422 |
unifiable) types. *) |
|
423 |
fun resynchronize ctxt fol_th th = |
|
424 |
let |
|
425 |
val num_metis_lits = |
|
54756 | 426 |
count is_metis_literal_genuine (Metis_LiteralSet.toList (Metis_Thm.clause fol_th)) |
59582 | 427 |
val num_isabelle_lits = count is_isabelle_literal_genuine (Thm.prems_of th) |
42333 | 428 |
in |
429 |
if num_metis_lits >= num_isabelle_lits then |
|
430 |
th |
|
431 |
else |
|
432 |
let |
|
59582 | 433 |
val (prems0, concl) = th |> Thm.prop_of |> Logic.strip_horn |
54756 | 434 |
val prems = prems0 |> map normalize_literal |> distinct Term.aconv_untyped |
42333 | 435 |
val goal = Logic.list_implies (prems, concl) |
54984
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
54756
diff
changeset
|
436 |
val ctxt' = fold Thm.declare_hyps (#hyps (Thm.crep_thm th)) ctxt |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58957
diff
changeset
|
437 |
val tac = |
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58957
diff
changeset
|
438 |
cut_tac th 1 THEN |
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58957
diff
changeset
|
439 |
rewrite_goals_tac ctxt' meta_not_not THEN |
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58957
diff
changeset
|
440 |
ALLGOALS (assume_tac ctxt') |
42333 | 441 |
in |
442 |
if length prems = length prems0 then |
|
50875
bfb626265782
less brutal Metis failure -- the brutality was accidentally introduced by df8ae0590be2
blanchet
parents:
48132
diff
changeset
|
443 |
raise METIS_RECONSTRUCT ("resynchronize", "Out of sync") |
42333 | 444 |
else |
54984
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
54756
diff
changeset
|
445 |
Goal.prove ctxt' [] [] goal (K tac) |
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
54756
diff
changeset
|
446 |
|> resynchronize ctxt' fol_th |
42333 | 447 |
end |
448 |
end |
|
449 |
||
45508 | 450 |
fun replay_one_inference ctxt type_enc concealed sym_tab (fol_th, inf) |
44492
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44241
diff
changeset
|
451 |
th_pairs = |
59582 | 452 |
if not (null th_pairs) andalso Thm.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
|
453 |
(* 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
|
454 |
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
|
455 |
benefice of the doubt. *) |
43094 | 456 |
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
|
457 |
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
|
458 |
let |
54756 | 459 |
val _ = trace_msg ctxt (fn () => "=============================================") |
460 |
val _ = trace_msg ctxt (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th) |
|
461 |
val _ = trace_msg ctxt (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf) |
|
45508 | 462 |
val th = one_step ctxt type_enc concealed sym_tab th_pairs (fol_th, inf) |
60363 | 463 |
|> flexflex_first_order ctxt |
54756 | 464 |
|> resynchronize ctxt fol_th |
465 |
val _ = trace_msg ctxt (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th) |
|
466 |
val _ = trace_msg ctxt (fn () => "=============================================") |
|
467 |
in |
|
468 |
(fol_th, th) :: th_pairs |
|
469 |
end |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39495
diff
changeset
|
470 |
|
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
|
471 |
(* 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
|
472 |
one of the premises. Unfortunately, this sometimes yields "Variable |
51701
1e29891759c4
tuned exceptions -- avoid composing error messages in low-level situations;
wenzelm
parents:
50875
diff
changeset
|
473 |
has two distinct types" errors. To avoid this, we instantiate the |
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
|
474 |
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
|
475 |
?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
|
476 |
where the nonvariables are goal parameters. *) |
59632 | 477 |
fun unify_first_prem_with_concl ctxt i th = |
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
|
478 |
let |
59582 | 479 |
val goal = Logic.get_goal (Thm.prop_of th) i |> Envir.beta_eta_contract |
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
|
480 |
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
|
481 |
val concl = goal |> Logic.strip_assums_concl |
54756 | 482 |
|
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
|
483 |
fun pair_untyped_aconv (t1, t2) (u1, u2) = |
43301
8d7fc4a5b502
removed needless function that duplicated standard functionality, with a little unnecessary twist
blanchet
parents:
43300
diff
changeset
|
484 |
Term.aconv_untyped (t1, u1) andalso Term.aconv_untyped (t2, u2) |
54756 | 485 |
|
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
|
486 |
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
|
487 |
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
|
488 |
else tp :: map (apsnd (subst_atomic [tp])) inst |
54756 | 489 |
|
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
|
490 |
fun is_flex t = |
54756 | 491 |
(case strip_comb t of |
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
|
492 |
(Var _, args) => forall is_Bound args |
54756 | 493 |
| _ => false) |
494 |
||
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
|
495 |
fun unify_flex flex rigid = |
54756 | 496 |
(case strip_comb flex of |
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
|
497 |
(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
|
498 |
add_terms (Var z, |
44241 | 499 |
fold_rev absdummy (take (length args) (binder_types T)) rigid) |
54756 | 500 |
| _ => I) |
501 |
||
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
|
502 |
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
|
503 |
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
|
504 |
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
|
505 |
else I |
54756 | 506 |
|
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
|
507 |
fun unify_terms (t, u) = |
54756 | 508 |
(case (t, u) of |
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
|
509 |
(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
|
510 |
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
|
511 |
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
|
512 |
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
|
513 |
| (_ $ _, _) => 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
|
514 |
| (_, _ $ _) => 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
|
515 |
| (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
|
516 |
| (_, Var _) => add_terms (u, t) |
54756 | 517 |
| _ => I) |
518 |
||
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
|
519 |
val t_inst = |
59632 | 520 |
[] |> try (unify_terms (prem, concl) #> map (apply2 (Thm.cterm_of ctxt))) |
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
|
521 |
|> the_default [] (* FIXME *) |
54756 | 522 |
in |
60795 | 523 |
infer_instantiate_types ctxt (map (apfst (dest_Var o Thm.term_of)) t_inst) th |
54756 | 524 |
end |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
525 |
|
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
526 |
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
|
527 |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset
|
528 |
fun copy_prems_tac ctxt [] ns i = |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset
|
529 |
if forall (curry (op =) 1) ns then all_tac else copy_prems_tac ctxt (rev ns) [] i |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset
|
530 |
| copy_prems_tac ctxt (1 :: ms) ns i = rotate_tac 1 i THEN copy_prems_tac ctxt ms (1 :: ns) i |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset
|
531 |
| copy_prems_tac ctxt (m :: ms) ns i = |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset
|
532 |
eresolve_tac ctxt [copy_prem] i THEN copy_prems_tac ctxt ms (m div 2 :: (m + 1) div 2 :: ns) i |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
533 |
|
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
|
534 |
(* 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
|
535 |
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
|
536 |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset
|
537 |
fun instantiate_forall_tac ctxt t i st = |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
538 |
let |
59582 | 539 |
val params = Logic.strip_params (Logic.get_goal (Thm.prop_of st) i) |> rev |
54756 | 540 |
|
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
541 |
fun repair (t as (Var ((s, _), _))) = |
40258
2c0d8fe36c21
make handling of parameters more robust, by querying the goal
blanchet
parents:
40221
diff
changeset
|
542 |
(case find_index (fn (s', _) => s' = s) params of |
54756 | 543 |
~1 => t |
544 |
| j => Bound j) |
|
40261
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset
|
545 |
| repair (t $ u) = |
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset
|
546 |
(case (repair t, repair u) of |
54756 | 547 |
(t as Bound j, u as Bound k) => |
548 |
(* This is a trick to repair the discrepancy between the fully skolemized term that MESON |
|
549 |
gives us (where existentials were pulled out) and the reality. *) |
|
550 |
if k > j then t else t $ u |
|
551 |
| (t, u) => t $ u) |
|
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
552 |
| repair t = t |
54756 | 553 |
|
44241 | 554 |
val t' = t |> repair |> fold (absdummy o snd) params |
54756 | 555 |
|
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
556 |
fun do_instantiate th = |
59582 | 557 |
(case Term.add_vars (Thm.prop_of th) [] |
54756 | 558 |
|> filter_out ((Meson_Clausify.is_zapped_var_name orf is_metis_fresh_variable) o fst |
559 |
o fst) of |
|
42270 | 560 |
[] => 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
|
561 |
| [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
|
562 |
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
|
563 |
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
|
564 |
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
|
565 |
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
|
566 |
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
|
567 |
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
|
568 |
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
|
569 |
Envir.Envir {maxidx = Vartab.fold (Integer.max o snd o fst) tyenv 0, |
54756 | 570 |
tenv = Vartab.empty, tyenv = tyenv} |
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
|
571 |
val ty_inst = |
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60363
diff
changeset
|
572 |
Vartab.fold (fn (x, (S, T)) => cons (((x, S), Thm.ctyp_of ctxt T))) |
59582 | 573 |
tyenv [] |
59632 | 574 |
val t_inst = [apply2 (Thm.cterm_of ctxt o Envir.norm_term env) (Var var, t')] |
54756 | 575 |
in |
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60363
diff
changeset
|
576 |
Drule.instantiate_normalize (ty_inst, map (apfst (dest_Var o Thm.term_of)) t_inst) th |
54756 | 577 |
end |
578 |
| _ => 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
|
579 |
in |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset
|
580 |
(DETERM (eresolve_tac ctxt @{thms allE} i THEN rotate_tac ~1 i) THEN PRIMITIVE do_instantiate) st |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
581 |
end |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
582 |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset
|
583 |
fun fix_exists_tac ctxt t = eresolve_tac ctxt [exE] THEN' rename_tac [t |> dest_Var |> fst |> fst] |
40261
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset
|
584 |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset
|
585 |
fun release_quantifier_tac ctxt (skolem, t) = |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset
|
586 |
(if skolem then fix_exists_tac ctxt else instantiate_forall_tac ctxt) t |
40261
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset
|
587 |
|
40258
2c0d8fe36c21
make handling of parameters more robust, by querying the goal
blanchet
parents:
40221
diff
changeset
|
588 |
fun release_clusters_tac _ _ _ [] = K all_tac |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset
|
589 |
| release_clusters_tac ctxt ax_counts substs ((ax_no, cluster_no) :: clusters) = |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
590 |
let |
54756 | 591 |
val cluster_of_var = Meson_Clausify.cluster_of_zapped_var_name o fst o fst o dest_Var |
40261
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset
|
592 |
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
|
593 |
val cluster_substs = |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
594 |
substs |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
595 |
|> map_filter (fn (ax_no', (_, (_, tsubst))) => |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
596 |
if ax_no' = ax_no then |
40261
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset
|
597 |
tsubst |> map (apfst cluster_of_var) |
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset
|
598 |
|> filter (in_right_cluster o fst) |
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset
|
599 |
|> map (apfst snd) |
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset
|
600 |
|> SOME |
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset
|
601 |
else |
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40259
diff
changeset
|
602 |
NONE) |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
603 |
fun do_cluster_subst cluster_subst = |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset
|
604 |
map (release_quantifier_tac ctxt) cluster_subst @ [rotate_tac 1] |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
605 |
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
|
606 |
in |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
607 |
rotate_tac first_prem |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
608 |
THEN' (EVERY' (maps do_cluster_subst cluster_substs)) |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
609 |
THEN' rotate_tac (~ first_prem - length cluster_substs) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset
|
610 |
THEN' release_clusters_tac ctxt ax_counts substs clusters |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
611 |
end |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
612 |
|
40264
b91e2e16d994
fixed order of quantifier instantiation in new Skolemizer
blanchet
parents:
40261
diff
changeset
|
613 |
fun cluster_key ((ax_no, (cluster_no, index_no)), skolem) = |
b91e2e16d994
fixed order of quantifier instantiation in new Skolemizer
blanchet
parents:
40261
diff
changeset
|
614 |
(ax_no, (cluster_no, (skolem, index_no))) |
b91e2e16d994
fixed order of quantifier instantiation in new Skolemizer
blanchet
parents:
40261
diff
changeset
|
615 |
fun cluster_ord p = |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58963
diff
changeset
|
616 |
prod_ord int_ord (prod_ord int_ord (prod_ord bool_ord int_ord)) (apply2 cluster_key p) |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
617 |
|
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
618 |
val tysubst_ord = |
54756 | 619 |
list_ord (prod_ord Term_Ord.fast_indexname_ord (prod_ord Term_Ord.sort_ord Term_Ord.typ_ord)) |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
620 |
|
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
621 |
structure Int_Tysubst_Table = |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
622 |
Table(type key = int * (indexname * (sort * typ)) list |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
623 |
val ord = prod_ord int_ord tysubst_ord) |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
624 |
|
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
625 |
structure Int_Pair_Graph = |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
626 |
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
|
627 |
|
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
|
628 |
fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (axiom_no, index_no) |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58963
diff
changeset
|
629 |
fun shuffle_ord p = prod_ord int_ord int_ord (apply2 shuffle_key p) |
40258
2c0d8fe36c21
make handling of parameters more robust, by querying the goal
blanchet
parents:
40221
diff
changeset
|
630 |
|
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
631 |
(* 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
|
632 |
"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
|
633 |
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
|
634 |
must be eliminated first. *) |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
635 |
fun discharge_skolem_premises ctxt axioms prems_imp_false = |
59582 | 636 |
if Thm.prop_of prems_imp_false aconv @{prop False} then |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
637 |
prems_imp_false |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
638 |
else |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
639 |
let |
42361 | 640 |
val thy = Proof_Context.theory_of ctxt |
57408 | 641 |
|
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
642 |
fun match_term p = |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
643 |
let |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
644 |
val (tyenv, tenv) = |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
645 |
Pattern.first_order_match thy p (Vartab.empty, Vartab.empty) |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
646 |
val tsubst = |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
647 |
tenv |> Vartab.dest |
42099
447fa058ab22
avoid evil "export_without_context", which breaks if there are local "fixes"
blanchet
parents:
42098
diff
changeset
|
648 |
|> 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
|
649 |
|> sort (cluster_ord |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58963
diff
changeset
|
650 |
o apply2 (Meson_Clausify.cluster_of_zapped_var_name |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
651 |
o fst o fst)) |
60781 | 652 |
|> map (fn (xi, (T, t)) => apply2 (Envir.subst_term_types tyenv) (Var (xi, T), t)) |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
653 |
val tysubst = tyenv |> Vartab.dest |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
654 |
in (tysubst, tsubst) end |
57408 | 655 |
|
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51951
diff
changeset
|
656 |
fun subst_info_of_prem subgoal_no prem = |
57408 | 657 |
(case prem of |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
658 |
_ $ (Const (@{const_name Meson.skolem}, _) $ (_ $ t $ num)) => |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
659 |
let val ax_no = HOLogic.dest_nat num in |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
660 |
(ax_no, (subgoal_no, |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
661 |
match_term (nth axioms ax_no |> the |> snd, t))) |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
662 |
end |
57408 | 663 |
| _ => raise TERM ("discharge_skolem_premises: Malformed premise", [prem])) |
664 |
||
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
665 |
fun cluster_of_var_name skolem s = |
57408 | 666 |
(case try Meson_Clausify.cluster_of_zapped_var_name s of |
42098
f978caf60bbe
more robust handling of variables in new Skolemizer
blanchet
parents:
41491
diff
changeset
|
667 |
NONE => NONE |
f978caf60bbe
more robust handling of variables in new Skolemizer
blanchet
parents:
41491
diff
changeset
|
668 |
| SOME ((ax_no, (cluster_no, _)), skolem') => |
57408 | 669 |
if skolem' = skolem andalso cluster_no > 0 then SOME (ax_no, cluster_no) else NONE) |
670 |
||
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
671 |
fun clusters_in_term skolem t = |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
672 |
Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst) |
57408 | 673 |
|
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51951
diff
changeset
|
674 |
fun deps_of_term_subst (var, t) = |
57408 | 675 |
(case clusters_in_term false var of |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
676 |
[] => NONE |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
677 |
| [(ax_no, cluster_no)] => |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
678 |
SOME ((ax_no, cluster_no), |
57408 | 679 |
clusters_in_term true t |> cluster_no > 1 ? cons (ax_no, cluster_no - 1)) |
680 |
| _ => raise TERM ("discharge_skolem_premises: Expected Var", [var])) |
|
681 |
||
59582 | 682 |
val prems = Logic.strip_imp_prems (Thm.prop_of prems_imp_false) |
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51951
diff
changeset
|
683 |
val substs = prems |> map2 subst_info_of_prem (1 upto length prems) |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58963
diff
changeset
|
684 |
|> sort (int_ord o apply2 fst) |
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51951
diff
changeset
|
685 |
val depss = maps (map_filter deps_of_term_subst o snd o snd o snd) substs |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
686 |
val clusters = maps (op ::) depss |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
687 |
val ordered_clusters = |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
688 |
Int_Pair_Graph.empty |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
689 |
|> fold Int_Pair_Graph.default_node (map (rpair ()) clusters) |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
690 |
|> fold Int_Pair_Graph.add_deps_acyclic depss |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
691 |
|> Int_Pair_Graph.topological_order |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
692 |
handle Int_Pair_Graph.CYCLES _ => |
55523
9429e7b5b827
removed final periods in messages for proof methods
blanchet
parents:
55234
diff
changeset
|
693 |
error "Cannot replay Metis proof in Isabelle without \"Hilbert_Choice\"" |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
694 |
val ax_counts = |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
695 |
Int_Tysubst_Table.empty |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
696 |
|> fold (fn (ax_no, (_, (tysubst, _))) => |
43262 | 697 |
Int_Tysubst_Table.map_default ((ax_no, tysubst), 0) |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
698 |
(Integer.add 1)) substs |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
699 |
|> 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
|
700 |
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
|
701 |
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
|
702 |
|> 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
|
703 |
| (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
|
704 |
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
|
705 |
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
|
706 |
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
|
707 |
SOME t |
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset
|
708 |
else |
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset
|
709 |
NONE) |
0e5d1e5e1177
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
blanchet
parents:
42337
diff
changeset
|
710 |
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
|
711 |
[] |> 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
|
712 |
|> 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
|
713 |
|> 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
|
714 |
|> 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
|
715 |
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
|
716 |
|> sort shuffle_ord |> map (fst o snd) |
57408 | 717 |
|
42270 | 718 |
(* for debugging only: |
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51951
diff
changeset
|
719 |
fun string_of_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) = |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
720 |
"ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^ |
51929 | 721 |
"; tysubst: " ^ @{make_string} tysubst ^ "; tsubst: {" ^ |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
722 |
commas (map ((fn (s, t) => s ^ " |-> " ^ t) |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58963
diff
changeset
|
723 |
o apply2 (Syntax.string_of_term ctxt)) tsubst) ^ "}" |
51929 | 724 |
val _ = tracing ("ORDERED CLUSTERS: " ^ @{make_string} ordered_clusters) |
725 |
val _ = tracing ("AXIOM COUNTS: " ^ @{make_string} ax_counts) |
|
726 |
val _ = tracing ("OUTER PARAMS: " ^ @{make_string} outer_param_names) |
|
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
727 |
val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^ |
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51951
diff
changeset
|
728 |
cat_lines (map string_of_subst_info substs)) |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
729 |
*) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset
|
730 |
val ctxt' = fold Thm.declare_hyps (#hyps (Thm.crep_thm prems_imp_false)) ctxt |
57408 | 731 |
|
58839 | 732 |
fun cut_and_ex_tac axiom = |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset
|
733 |
cut_tac axiom 1 THEN TRY (REPEAT_ALL_NEW (eresolve_tac ctxt' @{thms exE}) 1) |
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51951
diff
changeset
|
734 |
fun rotation_of_subgoal i = |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
735 |
find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
736 |
in |
54984
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
54756
diff
changeset
|
737 |
Goal.prove ctxt' [] [] @{prop False} |
57408 | 738 |
(K (DETERM (EVERY (map (cut_and_ex_tac o fst o the o nth axioms o fst o fst) ax_counts) |
739 |
THEN rename_tac outer_param_names 1 |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset
|
740 |
THEN copy_prems_tac ctxt' (map snd ax_counts) [] 1) |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset
|
741 |
THEN release_clusters_tac ctxt' ax_counts substs ordered_clusters 1 |
58957 | 742 |
THEN match_tac ctxt' [prems_imp_false] 1 |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset
|
743 |
THEN ALLGOALS (fn i => resolve_tac ctxt' @{thms Meson.skolem_COMBK_I} i |
57408 | 744 |
THEN rotate_tac (rotation_of_subgoal i) i |
59632 | 745 |
THEN PRIMITIVE (unify_first_prem_with_concl ctxt' i) |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58957
diff
changeset
|
746 |
THEN assume_tac ctxt' i |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58839
diff
changeset
|
747 |
THEN flexflex_tac ctxt'))) |
54984
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
54756
diff
changeset
|
748 |
handle ERROR msg => |
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
54756
diff
changeset
|
749 |
cat_error msg |
55523
9429e7b5b827
removed final periods in messages for proof methods
blanchet
parents:
55234
diff
changeset
|
750 |
"Cannot replay Metis proof in Isabelle: error when discharging Skolem assumptions" |
39964
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
751 |
end |
8ca95d819c7c
move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet
parents:
39958
diff
changeset
|
752 |
|
39495
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
diff
changeset
|
753 |
end; |