blanchet@40139
|
1 |
(* Title: HOL/Tools/Metis/metis_reconstruct.ML
|
blanchet@39735
|
2 |
Author: Kong W. Susanto, Cambridge University Computer Laboratory
|
blanchet@39735
|
3 |
Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
|
blanchet@39735
|
4 |
Author: Jasmin Blanchette, TU Muenchen
|
blanchet@39735
|
5 |
Copyright Cambridge University 2007
|
blanchet@39735
|
6 |
|
blanchet@39735
|
7 |
Proof reconstruction for Metis.
|
blanchet@39735
|
8 |
*)
|
blanchet@39735
|
9 |
|
blanchet@39735
|
10 |
signature METIS_RECONSTRUCT =
|
blanchet@39735
|
11 |
sig
|
blanchet@43521
|
12 |
exception METIS of string * string
|
blanchet@43521
|
13 |
|
blanchet@44000
|
14 |
val hol_clause_from_metis :
|
blanchet@44025
|
15 |
Proof.context -> int Symtab.table -> (string * term) list -> Metis_Thm.thm
|
blanchet@44025
|
16 |
-> term
|
blanchet@39737
|
17 |
val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
|
blanchet@43975
|
18 |
val untyped_aconv : term * term -> bool
|
blanchet@39737
|
19 |
val replay_one_inference :
|
blanchet@44053
|
20 |
Proof.context -> (string * term) list -> int Symtab.table
|
blanchet@39737
|
21 |
-> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list
|
blanchet@39737
|
22 |
-> (Metis_Thm.thm * thm) list
|
blanchet@40145
|
23 |
val discharge_skolem_premises :
|
blanchet@40145
|
24 |
Proof.context -> (thm * term) option list -> thm -> thm
|
blanchet@39735
|
25 |
end;
|
blanchet@39735
|
26 |
|
blanchet@39735
|
27 |
structure Metis_Reconstruct : METIS_RECONSTRUCT =
|
blanchet@39735
|
28 |
struct
|
blanchet@39735
|
29 |
|
blanchet@43935
|
30 |
open ATP_Problem
|
blanchet@43926
|
31 |
open ATP_Translate
|
blanchet@43935
|
32 |
open ATP_Reconstruct
|
blanchet@39737
|
33 |
open Metis_Translate
|
blanchet@39737
|
34 |
|
blanchet@43521
|
35 |
exception METIS of string * string
|
blanchet@43521
|
36 |
|
blanchet@39738
|
37 |
datatype term_or_type = SomeTerm of term | SomeType of typ
|
blanchet@39737
|
38 |
|
blanchet@39737
|
39 |
fun terms_of [] = []
|
blanchet@39738
|
40 |
| terms_of (SomeTerm t :: tts) = t :: terms_of tts
|
blanchet@39738
|
41 |
| terms_of (SomeType _ :: tts) = terms_of tts;
|
blanchet@39737
|
42 |
|
blanchet@39737
|
43 |
fun types_of [] = []
|
blanchet@43976
|
44 |
| types_of (SomeTerm (Var ((a, idx), _)) :: tts) =
|
blanchet@43976
|
45 |
types_of tts
|
blanchet@43976
|
46 |
|> (if String.isPrefix metis_generated_var_prefix a then
|
blanchet@43976
|
47 |
(* Variable generated by Metis, which might have been a type
|
blanchet@43976
|
48 |
variable. *)
|
blanchet@43976
|
49 |
cons (TVar (("'" ^ a, idx), HOLogic.typeS))
|
blanchet@43976
|
50 |
else
|
blanchet@43976
|
51 |
I)
|
blanchet@39738
|
52 |
| types_of (SomeTerm _ :: tts) = types_of tts
|
blanchet@43976
|
53 |
| types_of (SomeType T :: tts) = T :: types_of tts
|
blanchet@39737
|
54 |
|
blanchet@43935
|
55 |
fun atp_name_from_metis s =
|
blanchet@43945
|
56 |
case find_first (fn (_, (s', _)) => s' = s) metis_name_table of
|
blanchet@43945
|
57 |
SOME ((s, _), (_, swap)) => (s, swap)
|
blanchet@43945
|
58 |
| _ => (s, false)
|
blanchet@43935
|
59 |
fun atp_term_from_metis (Metis_Term.Fn (s, tms)) =
|
blanchet@43945
|
60 |
let val (s, swap) = atp_name_from_metis s in
|
blanchet@43945
|
61 |
ATerm (s, tms |> map atp_term_from_metis |> swap ? rev)
|
blanchet@43945
|
62 |
end
|
blanchet@43935
|
63 |
| atp_term_from_metis (Metis_Term.Var s) = ATerm (s, [])
|
blanchet@39737
|
64 |
|
blanchet@44053
|
65 |
fun hol_term_from_metis ctxt sym_tab =
|
blanchet@44053
|
66 |
atp_term_from_metis #> term_from_atp ctxt false sym_tab NONE
|
blanchet@43935
|
67 |
|
blanchet@43977
|
68 |
fun atp_literal_from_metis (pos, atom) =
|
blanchet@43977
|
69 |
atom |> Metis_Term.Fn |> atp_term_from_metis |> AAtom |> not pos ? mk_anot
|
blanchet@43977
|
70 |
fun atp_clause_from_metis [] = AAtom (ATerm (tptp_false, []))
|
blanchet@43977
|
71 |
| atp_clause_from_metis lits =
|
blanchet@43977
|
72 |
lits |> map atp_literal_from_metis |> mk_aconns AOr
|
blanchet@43977
|
73 |
|
blanchet@44025
|
74 |
fun reveal_old_skolems_and_infer_types ctxt old_skolems =
|
blanchet@44025
|
75 |
map (reveal_old_skolem_terms old_skolems)
|
blanchet@44053
|
76 |
#> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
|
blanchet@44025
|
77 |
|
blanchet@44025
|
78 |
fun hol_clause_from_metis ctxt sym_tab old_skolems =
|
blanchet@44000
|
79 |
Metis_Thm.clause
|
blanchet@44000
|
80 |
#> Metis_LiteralSet.toList
|
blanchet@44000
|
81 |
#> atp_clause_from_metis
|
blanchet@44000
|
82 |
#> prop_from_atp ctxt false sym_tab
|
blanchet@44025
|
83 |
#> singleton (reveal_old_skolems_and_infer_types ctxt old_skolems)
|
blanchet@43977
|
84 |
|
blanchet@44053
|
85 |
fun hol_terms_from_metis ctxt old_skolems sym_tab fol_tms =
|
blanchet@44053
|
86 |
let val ts = map (hol_term_from_metis ctxt sym_tab) fol_tms
|
blanchet@40159
|
87 |
val _ = trace_msg ctxt (fn () => " calling type inference:")
|
blanchet@40159
|
88 |
val _ = app (fn t => trace_msg ctxt
|
blanchet@40159
|
89 |
(fn () => Syntax.string_of_term ctxt t)) ts
|
blanchet@44025
|
90 |
val ts' =
|
blanchet@44025
|
91 |
ts |> reveal_old_skolems_and_infer_types ctxt old_skolems
|
blanchet@40159
|
92 |
val _ = app (fn t => trace_msg ctxt
|
blanchet@39737
|
93 |
(fn () => " final term: " ^ Syntax.string_of_term ctxt t ^
|
blanchet@43969
|
94 |
" of type " ^ Syntax.string_of_typ ctxt (type_of t)))
|
blanchet@39737
|
95 |
ts'
|
blanchet@39737
|
96 |
in ts' end;
|
blanchet@39737
|
97 |
|
blanchet@39737
|
98 |
(* ------------------------------------------------------------------------- *)
|
blanchet@39737
|
99 |
(* FOL step Inference Rules *)
|
blanchet@39737
|
100 |
(* ------------------------------------------------------------------------- *)
|
blanchet@39737
|
101 |
|
blanchet@39737
|
102 |
(*for debugging only*)
|
blanchet@39737
|
103 |
(*
|
blanchet@40159
|
104 |
fun print_thpair ctxt (fth,th) =
|
blanchet@40159
|
105 |
(trace_msg ctxt (fn () => "=============================================");
|
blanchet@40159
|
106 |
trace_msg ctxt (fn () => "Metis: " ^ Metis_Thm.toString fth);
|
blanchet@40159
|
107 |
trace_msg ctxt (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
|
blanchet@39737
|
108 |
*)
|
blanchet@39737
|
109 |
|
blanchet@43935
|
110 |
fun lookth th_pairs fth =
|
blanchet@43935
|
111 |
the (AList.lookup (uncurry Metis_Thm.equal) th_pairs fth)
|
blanchet@39737
|
112 |
handle Option.Option =>
|
blanchet@39737
|
113 |
raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fth)
|
blanchet@39737
|
114 |
|
blanchet@39737
|
115 |
fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx));
|
blanchet@39737
|
116 |
|
blanchet@39737
|
117 |
(* INFERENCE RULE: AXIOM *)
|
blanchet@39737
|
118 |
|
blanchet@44053
|
119 |
(* This causes variables to have an index of 1 by default. See also
|
blanchet@44053
|
120 |
"term_from_atp" in "ATP_Reconstruct". *)
|
blanchet@44053
|
121 |
val axiom_inference = Thm.incr_indexes 1 oo lookth
|
blanchet@39737
|
122 |
|
blanchet@39737
|
123 |
(* INFERENCE RULE: ASSUME *)
|
blanchet@39737
|
124 |
|
blanchet@39737
|
125 |
val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
|
blanchet@39737
|
126 |
|
blanchet@44028
|
127 |
fun inst_excluded_middle thy i_atom =
|
blanchet@39737
|
128 |
let val th = EXCLUDED_MIDDLE
|
blanchet@39737
|
129 |
val [vx] = Term.add_vars (prop_of th) []
|
blanchet@44028
|
130 |
val substs = [(cterm_of thy (Var vx), cterm_of thy i_atom)]
|
blanchet@39737
|
131 |
in cterm_instantiate substs th end;
|
blanchet@39737
|
132 |
|
blanchet@44053
|
133 |
fun assume_inference ctxt old_skolems sym_tab atom =
|
blanchet@39737
|
134 |
inst_excluded_middle
|
wenzelm@43232
|
135 |
(Proof_Context.theory_of ctxt)
|
blanchet@44053
|
136 |
(singleton (hol_terms_from_metis ctxt old_skolems sym_tab)
|
blanchet@44028
|
137 |
(Metis_Term.Fn atom))
|
blanchet@39737
|
138 |
|
blanchet@39738
|
139 |
(* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
|
blanchet@39737
|
140 |
to reconstruct them admits new possibilities of errors, e.g. concerning
|
blanchet@39737
|
141 |
sorts. Instead we try to arrange that new TVars are distinct and that types
|
blanchet@39738
|
142 |
can be inferred from terms. *)
|
blanchet@39737
|
143 |
|
blanchet@44053
|
144 |
fun inst_inference ctxt old_skolems sym_tab th_pairs fsubst th =
|
wenzelm@43232
|
145 |
let val thy = Proof_Context.theory_of ctxt
|
blanchet@43935
|
146 |
val i_th = lookth th_pairs th
|
blanchet@39737
|
147 |
val i_th_vars = Term.add_vars (prop_of i_th) []
|
blanchet@39737
|
148 |
fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
|
blanchet@39737
|
149 |
fun subst_translation (x,y) =
|
blanchet@39738
|
150 |
let val v = find_var x
|
blanchet@44025
|
151 |
(* We call "reveal_old_skolems_and_infer_types" below. *)
|
blanchet@44053
|
152 |
val t = hol_term_from_metis ctxt sym_tab y
|
blanchet@39738
|
153 |
in SOME (cterm_of thy (Var v), t) end
|
blanchet@39738
|
154 |
handle Option.Option =>
|
blanchet@40159
|
155 |
(trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^
|
blanchet@40159
|
156 |
" in " ^ Display.string_of_thm ctxt i_th);
|
blanchet@39738
|
157 |
NONE)
|
blanchet@39738
|
158 |
| TYPE _ =>
|
blanchet@40159
|
159 |
(trace_msg ctxt (fn () => "\"hol_term_from_metis\" failed for " ^ x ^
|
blanchet@40159
|
160 |
" in " ^ Display.string_of_thm ctxt i_th);
|
blanchet@39738
|
161 |
NONE)
|
blanchet@39737
|
162 |
fun remove_typeinst (a, t) =
|
blanchet@39737
|
163 |
case strip_prefix_and_unascii schematic_var_prefix a of
|
blanchet@39737
|
164 |
SOME b => SOME (b, t)
|
blanchet@39737
|
165 |
| NONE => case strip_prefix_and_unascii tvar_prefix a of
|
blanchet@39737
|
166 |
SOME _ => NONE (*type instantiations are forbidden!*)
|
blanchet@39737
|
167 |
| NONE => SOME (a,t) (*internal Metis var?*)
|
blanchet@40159
|
168 |
val _ = trace_msg ctxt (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
|
blanchet@39737
|
169 |
val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
|
blanchet@44025
|
170 |
val (vars, tms) =
|
blanchet@44025
|
171 |
ListPair.unzip (map_filter subst_translation substs)
|
blanchet@44025
|
172 |
||> reveal_old_skolems_and_infer_types ctxt old_skolems
|
blanchet@39737
|
173 |
val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
|
blanchet@39737
|
174 |
val substs' = ListPair.zip (vars, map ctm_of tms)
|
blanchet@40159
|
175 |
val _ = trace_msg ctxt (fn () =>
|
blanchet@39737
|
176 |
cat_lines ("subst_translations:" ::
|
blanchet@39737
|
177 |
(substs' |> map (fn (x, y) =>
|
blanchet@39737
|
178 |
Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
|
blanchet@39737
|
179 |
Syntax.string_of_term ctxt (term_of y)))));
|
blanchet@39737
|
180 |
in cterm_instantiate substs' i_th end
|
blanchet@44027
|
181 |
handle THM (msg, _, _) => raise METIS ("inst_inference", msg)
|
blanchet@44027
|
182 |
| ERROR msg => raise METIS ("inst_inference", msg)
|
blanchet@39737
|
183 |
|
blanchet@39737
|
184 |
(* INFERENCE RULE: RESOLVE *)
|
blanchet@39737
|
185 |
|
blanchet@39737
|
186 |
(* Like RSN, but we rename apart only the type variables. Vars here typically
|
blanchet@39737
|
187 |
have an index of 1, and the use of RSN would increase this typically to 3.
|
blanchet@43976
|
188 |
Instantiations of those Vars could then fail. See comment on "make_var". *)
|
blanchet@39737
|
189 |
fun resolve_inc_tyvars thy tha i thb =
|
blanchet@39737
|
190 |
let
|
blanchet@39737
|
191 |
val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
|
blanchet@39737
|
192 |
fun aux tha thb =
|
blanchet@39737
|
193 |
case Thm.bicompose false (false, tha, nprems_of tha) i thb
|
blanchet@39737
|
194 |
|> Seq.list_of |> distinct Thm.eq_thm of
|
blanchet@39737
|
195 |
[th] => th
|
blanchet@39737
|
196 |
| _ => raise THM ("resolve_inc_tyvars: unique result expected", i,
|
blanchet@39737
|
197 |
[tha, thb])
|
blanchet@39737
|
198 |
in
|
blanchet@39737
|
199 |
aux tha thb
|
blanchet@39737
|
200 |
handle TERM z =>
|
blanchet@39737
|
201 |
(* The unifier, which is invoked from "Thm.bicompose", will sometimes
|
blanchet@39737
|
202 |
refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a
|
blanchet@39737
|
203 |
"TERM" exception (with "add_ffpair" as first argument). We then
|
blanchet@39737
|
204 |
perform unification of the types of variables by hand and try
|
blanchet@39737
|
205 |
again. We could do this the first time around but this error
|
blanchet@39737
|
206 |
occurs seldom and we don't want to break existing proofs in subtle
|
blanchet@39737
|
207 |
ways or slow them down needlessly. *)
|
blanchet@39737
|
208 |
case [] |> fold (Term.add_vars o prop_of) [tha, thb]
|
blanchet@39737
|
209 |
|> AList.group (op =)
|
blanchet@39737
|
210 |
|> maps (fn ((s, _), T :: Ts) =>
|
blanchet@39737
|
211 |
map (fn T' => (Free (s, T), Free (s, T'))) Ts)
|
blanchet@39737
|
212 |
|> rpair (Envir.empty ~1)
|
blanchet@39737
|
213 |
|-> fold (Pattern.unify thy)
|
blanchet@39737
|
214 |
|> Envir.type_env |> Vartab.dest
|
blanchet@39737
|
215 |
|> map (fn (x, (S, T)) =>
|
blanchet@39737
|
216 |
pairself (ctyp_of thy) (TVar (x, S), T)) of
|
blanchet@39737
|
217 |
[] => raise TERM z
|
blanchet@39737
|
218 |
| ps => aux (instantiate (ps, []) tha) (instantiate (ps, []) thb)
|
blanchet@39737
|
219 |
end
|
blanchet@39737
|
220 |
|
blanchet@40462
|
221 |
fun s_not (@{const Not} $ t) = t
|
blanchet@40462
|
222 |
| s_not t = HOLogic.mk_not t
|
blanchet@44036
|
223 |
fun simp_not_not (@{const Trueprop} $ t) = @{const Trueprop} $ simp_not_not t
|
blanchet@44036
|
224 |
| simp_not_not (@{const Not} $ t) = s_not (simp_not_not t)
|
blanchet@40462
|
225 |
| simp_not_not t = t
|
blanchet@39737
|
226 |
|
blanchet@39737
|
227 |
(* Match untyped terms. *)
|
blanchet@43975
|
228 |
fun untyped_aconv (Const (a, _), Const(b, _)) = (a = b)
|
blanchet@43975
|
229 |
| untyped_aconv (Free (a, _), Free (b, _)) = (a = b)
|
blanchet@43975
|
230 |
| untyped_aconv (Var ((a, _), _), Var ((b, _), _)) = (a = b)
|
blanchet@43975
|
231 |
| untyped_aconv (Bound i, Bound j) = (i = j)
|
blanchet@43975
|
232 |
| untyped_aconv (Abs (_, _, t), Abs (_, _, u)) = untyped_aconv (t, u)
|
blanchet@43975
|
233 |
| untyped_aconv (t1 $ t2, u1 $ u2) =
|
blanchet@43975
|
234 |
untyped_aconv (t1, u1) andalso untyped_aconv (t2, u2)
|
blanchet@43975
|
235 |
| untyped_aconv _ = false
|
blanchet@39737
|
236 |
|
blanchet@44036
|
237 |
val normalize_literal = simp_not_not o Envir.eta_contract
|
blanchet@44036
|
238 |
|
blanchet@44028
|
239 |
(* Find the relative location of an untyped term within a list of terms as a
|
blanchet@44028
|
240 |
1-based index. Returns 0 in case of failure. *)
|
blanchet@40462
|
241 |
fun index_of_literal lit haystack =
|
blanchet@39737
|
242 |
let
|
blanchet@44036
|
243 |
fun match_lit normalize =
|
blanchet@43975
|
244 |
HOLogic.dest_Trueprop #> normalize
|
blanchet@43975
|
245 |
#> curry untyped_aconv (lit |> normalize)
|
blanchet@44036
|
246 |
in
|
blanchet@44036
|
247 |
(case find_index (match_lit I) haystack of
|
blanchet@44036
|
248 |
~1 => find_index (match_lit (simp_not_not o Envir.eta_contract)) haystack
|
blanchet@44036
|
249 |
| j => j) + 1
|
blanchet@44036
|
250 |
end
|
blanchet@39737
|
251 |
|
blanchet@40074
|
252 |
(* Permute a rule's premises to move the i-th premise to the last position. *)
|
blanchet@40074
|
253 |
fun make_last i th =
|
blanchet@40074
|
254 |
let val n = nprems_of th
|
blanchet@40074
|
255 |
in if 1 <= i andalso i <= n
|
blanchet@40074
|
256 |
then Thm.permute_prems (i-1) 1 th
|
blanchet@40074
|
257 |
else raise THM("select_literal", i, [th])
|
blanchet@40074
|
258 |
end;
|
blanchet@40074
|
259 |
|
blanchet@43219
|
260 |
(* Maps a rule that ends "... ==> P ==> False" to "... ==> ~ P" while avoiding
|
blanchet@43220
|
261 |
to create double negations. The "select" wrapper is a trick to ensure that
|
blanchet@43220
|
262 |
"P ==> ~ False ==> False" is rewritten to "P ==> False", not to "~ P". We
|
blanchet@43220
|
263 |
don't use this trick in general because it makes the proof object uglier than
|
blanchet@43220
|
264 |
necessary. FIXME. *)
|
blanchet@43220
|
265 |
fun negate_head th =
|
blanchet@43220
|
266 |
if exists (fn t => t aconv @{prop "~ False"}) (prems_of th) then
|
blanchet@43220
|
267 |
(th RS @{thm select_FalseI})
|
blanchet@43220
|
268 |
|> fold (rewrite_rule o single)
|
blanchet@43220
|
269 |
@{thms not_atomize_select atomize_not_select}
|
blanchet@43220
|
270 |
else
|
blanchet@43220
|
271 |
th |> fold (rewrite_rule o single) @{thms not_atomize atomize_not}
|
blanchet@40074
|
272 |
|
blanchet@40074
|
273 |
(* Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
|
blanchet@43219
|
274 |
val select_literal = negate_head oo make_last
|
blanchet@40074
|
275 |
|
blanchet@44053
|
276 |
fun resolve_inference ctxt old_skolems sym_tab th_pairs atom th1 th2 =
|
blanchet@39737
|
277 |
let
|
blanchet@43935
|
278 |
val (i_th1, i_th2) = pairself (lookth th_pairs) (th1, th2)
|
blanchet@44028
|
279 |
val _ = trace_msg ctxt (fn () =>
|
blanchet@44028
|
280 |
" isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1 ^ "\n\
|
blanchet@44028
|
281 |
\ isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
|
blanchet@39737
|
282 |
in
|
blanchet@39737
|
283 |
(* Trivial cases where one operand is type info *)
|
blanchet@39737
|
284 |
if Thm.eq_thm (TrueI, i_th1) then
|
blanchet@39737
|
285 |
i_th2
|
blanchet@39737
|
286 |
else if Thm.eq_thm (TrueI, i_th2) then
|
blanchet@39737
|
287 |
i_th1
|
blanchet@39737
|
288 |
else
|
blanchet@39737
|
289 |
let
|
blanchet@44028
|
290 |
val thy = Proof_Context.theory_of ctxt
|
blanchet@44028
|
291 |
val i_atom =
|
blanchet@44053
|
292 |
singleton (hol_terms_from_metis ctxt old_skolems sym_tab)
|
blanchet@44028
|
293 |
(Metis_Term.Fn atom)
|
blanchet@44028
|
294 |
val _ = trace_msg ctxt (fn () =>
|
blanchet@44028
|
295 |
" atom: " ^ Syntax.string_of_term ctxt i_atom)
|
blanchet@44028
|
296 |
in
|
blanchet@44028
|
297 |
case index_of_literal (s_not i_atom) (prems_of i_th1) of
|
blanchet@44028
|
298 |
0 =>
|
blanchet@44028
|
299 |
(trace_msg ctxt (fn () => "Failed to find literal in \"th1\"");
|
blanchet@44028
|
300 |
i_th1)
|
blanchet@44028
|
301 |
| j1 =>
|
blanchet@44028
|
302 |
(trace_msg ctxt (fn () => " index th1: " ^ string_of_int j1);
|
blanchet@44028
|
303 |
case index_of_literal i_atom (prems_of i_th2) of
|
blanchet@44028
|
304 |
0 =>
|
blanchet@44028
|
305 |
(trace_msg ctxt (fn () => "Failed to find literal in \"th2\"");
|
blanchet@44028
|
306 |
i_th2)
|
blanchet@44028
|
307 |
| j2 =>
|
blanchet@44028
|
308 |
(trace_msg ctxt (fn () => " index th2: " ^ string_of_int j2);
|
blanchet@44028
|
309 |
resolve_inc_tyvars thy (select_literal j1 i_th1) j2 i_th2
|
blanchet@44028
|
310 |
handle TERM (s, _) => raise METIS ("resolve_inference", s)))
|
blanchet@44028
|
311 |
end
|
blanchet@44028
|
312 |
end
|
blanchet@39737
|
313 |
|
blanchet@39737
|
314 |
(* INFERENCE RULE: REFL *)
|
blanchet@39737
|
315 |
|
blanchet@39737
|
316 |
val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
|
blanchet@39737
|
317 |
|
blanchet@39737
|
318 |
val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
|
blanchet@39737
|
319 |
val refl_idx = 1 + Thm.maxidx_of REFL_THM;
|
blanchet@39737
|
320 |
|
blanchet@44053
|
321 |
fun refl_inference ctxt old_skolems sym_tab t =
|
blanchet@43935
|
322 |
let
|
blanchet@43935
|
323 |
val thy = Proof_Context.theory_of ctxt
|
blanchet@44053
|
324 |
val i_t = singleton (hol_terms_from_metis ctxt old_skolems sym_tab) t
|
blanchet@43935
|
325 |
val _ = trace_msg ctxt (fn () => " term: " ^ Syntax.string_of_term ctxt i_t)
|
blanchet@43935
|
326 |
val c_t = cterm_incr_types thy refl_idx i_t
|
blanchet@43935
|
327 |
in cterm_instantiate [(refl_x, c_t)] REFL_THM end
|
blanchet@39737
|
328 |
|
blanchet@39737
|
329 |
(* INFERENCE RULE: EQUALITY *)
|
blanchet@39737
|
330 |
|
blanchet@39737
|
331 |
val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
|
blanchet@39737
|
332 |
val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
|
blanchet@39737
|
333 |
|
blanchet@44053
|
334 |
fun equality_inference ctxt old_skolems sym_tab (pos, atom) fp fr =
|
wenzelm@43232
|
335 |
let val thy = Proof_Context.theory_of ctxt
|
blanchet@44028
|
336 |
val m_tm = Metis_Term.Fn atom
|
blanchet@44028
|
337 |
val [i_atom, i_tm] =
|
blanchet@44053
|
338 |
hol_terms_from_metis ctxt old_skolems sym_tab [m_tm, fr]
|
blanchet@40159
|
339 |
val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos)
|
blanchet@39737
|
340 |
fun replace_item_list lx 0 (_::ls) = lx::ls
|
blanchet@39737
|
341 |
| replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
|
blanchet@44046
|
342 |
fun path_finder_fail tm ps t =
|
blanchet@44050
|
343 |
raise METIS ("equality_inference (path_finder)",
|
blanchet@44050
|
344 |
"path = " ^ space_implode " " (map string_of_int ps) ^
|
blanchet@44050
|
345 |
" isa-term: " ^ Syntax.string_of_term ctxt tm ^
|
blanchet@44050
|
346 |
(case t of
|
blanchet@44050
|
347 |
SOME t => " fol-term: " ^ Metis_Term.toString t
|
blanchet@44050
|
348 |
| NONE => ""))
|
blanchet@44053
|
349 |
fun path_finder tm [] _ = (tm, Bound 0)
|
blanchet@44053
|
350 |
| path_finder tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
|
blanchet@44018
|
351 |
let
|
blanchet@44018
|
352 |
val s = s |> perhaps (try (strip_prefix_and_unascii const_prefix
|
blanchet@44018
|
353 |
#> the #> unmangled_const_name))
|
blanchet@44018
|
354 |
in
|
blanchet@44018
|
355 |
if s = metis_predicator orelse s = predicator_name orelse
|
blanchet@44018
|
356 |
s = metis_type_tag orelse s = type_tag_name then
|
blanchet@44053
|
357 |
path_finder tm ps (nth ts p)
|
blanchet@44018
|
358 |
else if s = metis_app_op orelse s = app_op_name then
|
blanchet@43971
|
359 |
let
|
blanchet@43971
|
360 |
val (tm1, tm2) = dest_comb tm
|
blanchet@43971
|
361 |
val p' = p - (length ts - 2)
|
blanchet@43971
|
362 |
in
|
blanchet@43971
|
363 |
if p' = 0 then
|
blanchet@44053
|
364 |
path_finder tm1 ps (nth ts p) ||> (fn y => y $ tm2)
|
blanchet@43971
|
365 |
else
|
blanchet@44053
|
366 |
path_finder tm2 ps (nth ts p) ||> (fn y => tm1 $ y)
|
blanchet@43971
|
367 |
end
|
blanchet@43971
|
368 |
else
|
blanchet@43971
|
369 |
let
|
blanchet@43971
|
370 |
val (tm1, args) = strip_comb tm
|
blanchet@43971
|
371 |
val adjustment = length ts - length args
|
blanchet@43971
|
372 |
val p' = if adjustment > p then p else p - adjustment
|
blanchet@44046
|
373 |
val tm_p =
|
blanchet@44046
|
374 |
nth args p'
|
blanchet@44046
|
375 |
handle Subscript => path_finder_fail tm (p :: ps) (SOME t)
|
blanchet@43971
|
376 |
val _ = trace_msg ctxt (fn () =>
|
blanchet@43971
|
377 |
"path_finder: " ^ string_of_int p ^ " " ^
|
blanchet@43971
|
378 |
Syntax.string_of_term ctxt tm_p)
|
blanchet@44053
|
379 |
val (r, t) = path_finder tm_p ps (nth ts p)
|
blanchet@43971
|
380 |
in (r, list_comb (tm1, replace_item_list t p' args)) end
|
blanchet@43971
|
381 |
end
|
blanchet@44053
|
382 |
| path_finder tm ps t = path_finder_fail tm ps (SOME t)
|
blanchet@44053
|
383 |
val (tm_subst, body) = path_finder i_atom fp m_tm
|
blanchet@39738
|
384 |
val tm_abs = Abs ("x", type_of tm_subst, body)
|
blanchet@40159
|
385 |
val _ = trace_msg ctxt (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
|
blanchet@40159
|
386 |
val _ = trace_msg ctxt (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
|
blanchet@40159
|
387 |
val _ = trace_msg ctxt (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
|
blanchet@39737
|
388 |
val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill typed but gives right max*)
|
blanchet@39737
|
389 |
val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
|
blanchet@40159
|
390 |
val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
|
blanchet@39737
|
391 |
val eq_terms = map (pairself (cterm_of thy))
|
blanchet@39737
|
392 |
(ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
|
blanchet@39737
|
393 |
in cterm_instantiate eq_terms subst' end;
|
blanchet@39737
|
394 |
|
blanchet@43935
|
395 |
val factor = Seq.hd o distinct_subgoals_tac
|
blanchet@39737
|
396 |
|
blanchet@44053
|
397 |
fun one_step ctxt old_skolems sym_tab th_pairs p =
|
blanchet@39737
|
398 |
case p of
|
blanchet@44027
|
399 |
(fol_th, Metis_Proof.Axiom _) => axiom_inference th_pairs fol_th |> factor
|
blanchet@44028
|
400 |
| (_, Metis_Proof.Assume f_atom) =>
|
blanchet@44053
|
401 |
assume_inference ctxt old_skolems sym_tab f_atom
|
blanchet@39737
|
402 |
| (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
|
blanchet@44053
|
403 |
inst_inference ctxt old_skolems sym_tab th_pairs f_subst f_th1
|
blanchet@44027
|
404 |
|> factor
|
blanchet@44028
|
405 |
| (_, Metis_Proof.Resolve(f_atom, f_th1, f_th2)) =>
|
blanchet@44053
|
406 |
resolve_inference ctxt old_skolems sym_tab th_pairs f_atom f_th1 f_th2
|
blanchet@43935
|
407 |
|> factor
|
blanchet@44027
|
408 |
| (_, Metis_Proof.Refl f_tm) =>
|
blanchet@44053
|
409 |
refl_inference ctxt old_skolems sym_tab f_tm
|
blanchet@39737
|
410 |
| (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
|
blanchet@44053
|
411 |
equality_inference ctxt old_skolems sym_tab f_lit f_p f_r
|
blanchet@39737
|
412 |
|
blanchet@40074
|
413 |
fun flexflex_first_order th =
|
blanchet@40074
|
414 |
case Thm.tpairs_of th of
|
blanchet@40074
|
415 |
[] => th
|
blanchet@40074
|
416 |
| pairs =>
|
blanchet@40074
|
417 |
let val thy = theory_of_thm th
|
blanchet@40074
|
418 |
val (_, tenv) =
|
blanchet@40074
|
419 |
fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
|
blanchet@40074
|
420 |
val t_pairs = map Meson.term_pair_of (Vartab.dest tenv)
|
blanchet@40074
|
421 |
val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
|
blanchet@40074
|
422 |
in th' end
|
blanchet@40074
|
423 |
handle THM _ => th;
|
blanchet@39737
|
424 |
|
blanchet@40076
|
425 |
fun is_metis_literal_genuine (_, (s, _)) = not (String.isPrefix class_prefix s)
|
blanchet@40076
|
426 |
fun is_isabelle_literal_genuine t =
|
blanchet@40134
|
427 |
case t of _ $ (Const (@{const_name Meson.skolem}, _) $ _) => false | _ => true
|
blanchet@40076
|
428 |
|
blanchet@40076
|
429 |
fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0
|
blanchet@40076
|
430 |
|
blanchet@43204
|
431 |
(* Seldomly needed hack. A Metis clause is represented as a set, so duplicate
|
blanchet@43204
|
432 |
disjuncts are impossible. In the Isabelle proof, in spite of efforts to
|
blanchet@43204
|
433 |
eliminate them, duplicates sometimes appear with slightly different (but
|
blanchet@43204
|
434 |
unifiable) types. *)
|
blanchet@43204
|
435 |
fun resynchronize ctxt fol_th th =
|
blanchet@43204
|
436 |
let
|
blanchet@43204
|
437 |
val num_metis_lits =
|
blanchet@43204
|
438 |
count is_metis_literal_genuine
|
blanchet@43204
|
439 |
(Metis_LiteralSet.toList (Metis_Thm.clause fol_th))
|
blanchet@43204
|
440 |
val num_isabelle_lits = count is_isabelle_literal_genuine (prems_of th)
|
blanchet@43204
|
441 |
in
|
blanchet@43204
|
442 |
if num_metis_lits >= num_isabelle_lits then
|
blanchet@43204
|
443 |
th
|
blanchet@43204
|
444 |
else
|
blanchet@43204
|
445 |
let
|
blanchet@43204
|
446 |
val (prems0, concl) = th |> prop_of |> Logic.strip_horn
|
blanchet@44036
|
447 |
val prems = prems0 |> map normalize_literal
|
blanchet@44036
|
448 |
|> distinct untyped_aconv
|
blanchet@43204
|
449 |
val goal = Logic.list_implies (prems, concl)
|
blanchet@44036
|
450 |
val tac = cut_rules_tac [th] 1
|
blanchet@44036
|
451 |
THEN rewrite_goals_tac @{thms not_not [THEN eq_reflection]}
|
blanchet@44036
|
452 |
THEN ALLGOALS assume_tac
|
blanchet@43204
|
453 |
in
|
blanchet@43204
|
454 |
if length prems = length prems0 then
|
blanchet@43521
|
455 |
raise METIS ("resynchronize", "Out of sync")
|
blanchet@43204
|
456 |
else
|
blanchet@44036
|
457 |
Goal.prove ctxt [] [] goal (K tac)
|
blanchet@43204
|
458 |
|> resynchronize ctxt fol_th
|
blanchet@43204
|
459 |
end
|
blanchet@43204
|
460 |
end
|
blanchet@43204
|
461 |
|
blanchet@44053
|
462 |
fun replay_one_inference ctxt old_skolems sym_tab (fol_th, inf) th_pairs =
|
blanchet@43935
|
463 |
if not (null th_pairs) andalso
|
blanchet@43935
|
464 |
prop_of (snd (hd th_pairs)) aconv @{prop False} then
|
blanchet@41110
|
465 |
(* Isabelle sometimes identifies literals (premises) that are distinct in
|
blanchet@41110
|
466 |
Metis (e.g., because of type variables). We give the Isabelle proof the
|
blanchet@41110
|
467 |
benefice of the doubt. *)
|
blanchet@43935
|
468 |
th_pairs
|
blanchet@41110
|
469 |
else
|
blanchet@41110
|
470 |
let
|
blanchet@41110
|
471 |
val _ = trace_msg ctxt
|
blanchet@41110
|
472 |
(fn () => "=============================================")
|
blanchet@41110
|
473 |
val _ = trace_msg ctxt
|
blanchet@41110
|
474 |
(fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
|
blanchet@41110
|
475 |
val _ = trace_msg ctxt
|
blanchet@41110
|
476 |
(fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
|
blanchet@44053
|
477 |
val th = one_step ctxt old_skolems sym_tab th_pairs (fol_th, inf)
|
blanchet@41110
|
478 |
|> flexflex_first_order
|
blanchet@43204
|
479 |
|> resynchronize ctxt fol_th
|
blanchet@41110
|
480 |
val _ = trace_msg ctxt
|
blanchet@41110
|
481 |
(fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
|
blanchet@41110
|
482 |
val _ = trace_msg ctxt
|
blanchet@41110
|
483 |
(fn () => "=============================================")
|
blanchet@43935
|
484 |
in (fol_th, th) :: th_pairs end
|
blanchet@39737
|
485 |
|
blanchet@43213
|
486 |
(* It is normally sufficient to apply "assume_tac" to unify the conclusion with
|
blanchet@43213
|
487 |
one of the premises. Unfortunately, this sometimes yields "Variable
|
blanchet@43213
|
488 |
?SK_a_b_c_x has two distinct types" errors. To avoid this, we instantiate the
|
blanchet@43213
|
489 |
variables before applying "assume_tac". Typical constraints are of the form
|
blanchet@43213
|
490 |
?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,
|
blanchet@43213
|
491 |
where the nonvariables are goal parameters. *)
|
blanchet@43213
|
492 |
fun unify_first_prem_with_concl thy i th =
|
blanchet@43213
|
493 |
let
|
blanchet@43213
|
494 |
val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract
|
blanchet@43213
|
495 |
val prem = goal |> Logic.strip_assums_hyp |> hd
|
blanchet@43213
|
496 |
val concl = goal |> Logic.strip_assums_concl
|
blanchet@43213
|
497 |
fun pair_untyped_aconv (t1, t2) (u1, u2) =
|
blanchet@43975
|
498 |
untyped_aconv (t1, u1) andalso untyped_aconv (t2, u2)
|
blanchet@43213
|
499 |
fun add_terms tp inst =
|
blanchet@43213
|
500 |
if exists (pair_untyped_aconv tp) inst then inst
|
blanchet@43213
|
501 |
else tp :: map (apsnd (subst_atomic [tp])) inst
|
blanchet@43213
|
502 |
fun is_flex t =
|
blanchet@43213
|
503 |
case strip_comb t of
|
blanchet@43213
|
504 |
(Var _, args) => forall is_Bound args
|
blanchet@43213
|
505 |
| _ => false
|
blanchet@43213
|
506 |
fun unify_flex flex rigid =
|
blanchet@43213
|
507 |
case strip_comb flex of
|
blanchet@43213
|
508 |
(Var (z as (_, T)), args) =>
|
blanchet@43213
|
509 |
add_terms (Var z,
|
blanchet@43213
|
510 |
fold_rev (curry absdummy) (take (length args) (binder_types T)) rigid)
|
blanchet@43213
|
511 |
| _ => I
|
blanchet@43213
|
512 |
fun unify_potential_flex comb atom =
|
blanchet@43213
|
513 |
if is_flex comb then unify_flex comb atom
|
blanchet@43213
|
514 |
else if is_Var atom then add_terms (atom, comb)
|
blanchet@43213
|
515 |
else I
|
blanchet@43213
|
516 |
fun unify_terms (t, u) =
|
blanchet@43213
|
517 |
case (t, u) of
|
blanchet@43213
|
518 |
(t1 $ t2, u1 $ u2) =>
|
blanchet@43213
|
519 |
if is_flex t then unify_flex t u
|
blanchet@43213
|
520 |
else if is_flex u then unify_flex u t
|
blanchet@43213
|
521 |
else fold unify_terms [(t1, u1), (t2, u2)]
|
blanchet@43213
|
522 |
| (_ $ _, _) => unify_potential_flex t u
|
blanchet@43213
|
523 |
| (_, _ $ _) => unify_potential_flex u t
|
blanchet@43213
|
524 |
| (Var _, _) => add_terms (t, u)
|
blanchet@43213
|
525 |
| (_, Var _) => add_terms (u, t)
|
blanchet@43213
|
526 |
| _ => I
|
blanchet@43215
|
527 |
val t_inst =
|
blanchet@43215
|
528 |
[] |> try (unify_terms (prem, concl) #> map (pairself (cterm_of thy)))
|
blanchet@43215
|
529 |
|> the_default [] (* FIXME *)
|
blanchet@43213
|
530 |
in th |> cterm_instantiate t_inst end
|
blanchet@40145
|
531 |
|
blanchet@40145
|
532 |
val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast}
|
blanchet@40145
|
533 |
|
blanchet@40145
|
534 |
fun copy_prems_tac [] ns i =
|
blanchet@40145
|
535 |
if forall (curry (op =) 1) ns then all_tac else copy_prems_tac (rev ns) [] i
|
blanchet@40145
|
536 |
| copy_prems_tac (1 :: ms) ns i =
|
blanchet@40145
|
537 |
rotate_tac 1 i THEN copy_prems_tac ms (1 :: ns) i
|
blanchet@40145
|
538 |
| copy_prems_tac (m :: ms) ns i =
|
blanchet@40145
|
539 |
etac copy_prem i THEN copy_prems_tac ms (m div 2 :: (m + 1) div 2 :: ns) i
|
blanchet@40145
|
540 |
|
blanchet@43135
|
541 |
(* Metis generates variables of the form _nnn. *)
|
blanchet@43135
|
542 |
val is_metis_fresh_variable = String.isPrefix "_"
|
blanchet@43135
|
543 |
|
blanchet@40501
|
544 |
fun instantiate_forall_tac thy t i st =
|
blanchet@40145
|
545 |
let
|
blanchet@40501
|
546 |
val params = Logic.strip_params (Logic.get_goal (prop_of st) i) |> rev
|
blanchet@40145
|
547 |
fun repair (t as (Var ((s, _), _))) =
|
blanchet@40501
|
548 |
(case find_index (fn (s', _) => s' = s) params of
|
blanchet@40145
|
549 |
~1 => t
|
blanchet@40145
|
550 |
| j => Bound j)
|
blanchet@40504
|
551 |
| repair (t $ u) =
|
blanchet@40504
|
552 |
(case (repair t, repair u) of
|
blanchet@40504
|
553 |
(t as Bound j, u as Bound k) =>
|
blanchet@40504
|
554 |
(* This is a rather subtle trick to repair the discrepancy between
|
blanchet@40504
|
555 |
the fully skolemized term that MESON gives us (where existentials
|
blanchet@40504
|
556 |
were pulled out) and the reality. *)
|
blanchet@40504
|
557 |
if k > j then t else t $ u
|
blanchet@40504
|
558 |
| (t, u) => t $ u)
|
blanchet@40145
|
559 |
| repair t = t
|
blanchet@40145
|
560 |
val t' = t |> repair |> fold (curry absdummy) (map snd params)
|
blanchet@40145
|
561 |
fun do_instantiate th =
|
blanchet@43134
|
562 |
case Term.add_vars (prop_of th) []
|
blanchet@43135
|
563 |
|> filter_out ((Meson_Clausify.is_zapped_var_name orf
|
blanchet@43135
|
564 |
is_metis_fresh_variable) o fst o fst) of
|
blanchet@43134
|
565 |
[] => th
|
blanchet@43135
|
566 |
| [var as (_, T)] =>
|
blanchet@43135
|
567 |
let
|
blanchet@43135
|
568 |
val var_binder_Ts = T |> binder_types |> take (length params) |> rev
|
blanchet@43135
|
569 |
val var_body_T = T |> funpow (length params) range_type
|
blanchet@43135
|
570 |
val tyenv =
|
blanchet@43135
|
571 |
Vartab.empty |> Type.raw_unifys (fastype_of t :: map snd params,
|
blanchet@43135
|
572 |
var_body_T :: var_binder_Ts)
|
blanchet@43135
|
573 |
val env =
|
blanchet@43135
|
574 |
Envir.Envir {maxidx = Vartab.fold (Integer.max o snd o fst) tyenv 0,
|
blanchet@43135
|
575 |
tenv = Vartab.empty, tyenv = tyenv}
|
blanchet@43135
|
576 |
val ty_inst =
|
blanchet@43135
|
577 |
Vartab.fold (fn (x, (S, T)) =>
|
blanchet@43135
|
578 |
cons (pairself (ctyp_of thy) (TVar (x, S), T)))
|
blanchet@43135
|
579 |
tyenv []
|
blanchet@43135
|
580 |
val t_inst =
|
blanchet@43135
|
581 |
[pairself (cterm_of thy o Envir.norm_term env) (Var var, t')]
|
blanchet@43213
|
582 |
in th |> instantiate (ty_inst, t_inst) end
|
blanchet@43135
|
583 |
| _ => raise Fail "expected a single non-zapped, non-Metis Var"
|
blanchet@40145
|
584 |
in
|
blanchet@43135
|
585 |
(DETERM (etac @{thm allE} i THEN rotate_tac ~1 i)
|
blanchet@40501
|
586 |
THEN PRIMITIVE do_instantiate) st
|
blanchet@40145
|
587 |
end
|
blanchet@40145
|
588 |
|
blanchet@41383
|
589 |
fun fix_exists_tac t =
|
blanchet@44003
|
590 |
etac @{thm exE} THEN' rename_tac [t |> dest_Var |> fst |> fst]
|
blanchet@40504
|
591 |
|
blanchet@40504
|
592 |
fun release_quantifier_tac thy (skolem, t) =
|
blanchet@41383
|
593 |
(if skolem then fix_exists_tac else instantiate_forall_tac thy) t
|
blanchet@40504
|
594 |
|
blanchet@40501
|
595 |
fun release_clusters_tac _ _ _ [] = K all_tac
|
blanchet@40501
|
596 |
| release_clusters_tac thy ax_counts substs
|
blanchet@40145
|
597 |
((ax_no, cluster_no) :: clusters) =
|
blanchet@40145
|
598 |
let
|
blanchet@40504
|
599 |
val cluster_of_var =
|
blanchet@40504
|
600 |
Meson_Clausify.cluster_of_zapped_var_name o fst o fst o dest_Var
|
blanchet@40504
|
601 |
fun in_right_cluster ((_, (cluster_no', _)), _) = cluster_no' = cluster_no
|
blanchet@40145
|
602 |
val cluster_substs =
|
blanchet@40145
|
603 |
substs
|
blanchet@40145
|
604 |
|> map_filter (fn (ax_no', (_, (_, tsubst))) =>
|
blanchet@40145
|
605 |
if ax_no' = ax_no then
|
blanchet@40504
|
606 |
tsubst |> map (apfst cluster_of_var)
|
blanchet@40504
|
607 |
|> filter (in_right_cluster o fst)
|
blanchet@40504
|
608 |
|> map (apfst snd)
|
blanchet@40504
|
609 |
|> SOME
|
blanchet@40504
|
610 |
else
|
blanchet@40504
|
611 |
NONE)
|
blanchet@40145
|
612 |
fun do_cluster_subst cluster_subst =
|
blanchet@40504
|
613 |
map (release_quantifier_tac thy) cluster_subst @ [rotate_tac 1]
|
blanchet@40145
|
614 |
val first_prem = find_index (fn (ax_no', _) => ax_no' = ax_no) substs
|
blanchet@40145
|
615 |
in
|
blanchet@40145
|
616 |
rotate_tac first_prem
|
blanchet@40145
|
617 |
THEN' (EVERY' (maps do_cluster_subst cluster_substs))
|
blanchet@40145
|
618 |
THEN' rotate_tac (~ first_prem - length cluster_substs)
|
blanchet@40501
|
619 |
THEN' release_clusters_tac thy ax_counts substs clusters
|
blanchet@40145
|
620 |
end
|
blanchet@40145
|
621 |
|
blanchet@40507
|
622 |
fun cluster_key ((ax_no, (cluster_no, index_no)), skolem) =
|
blanchet@40507
|
623 |
(ax_no, (cluster_no, (skolem, index_no)))
|
blanchet@40507
|
624 |
fun cluster_ord p =
|
blanchet@40507
|
625 |
prod_ord int_ord (prod_ord int_ord (prod_ord bool_ord int_ord))
|
blanchet@40507
|
626 |
(pairself cluster_key p)
|
blanchet@40145
|
627 |
|
blanchet@40145
|
628 |
val tysubst_ord =
|
blanchet@40145
|
629 |
list_ord (prod_ord Term_Ord.fast_indexname_ord
|
blanchet@40145
|
630 |
(prod_ord Term_Ord.sort_ord Term_Ord.typ_ord))
|
blanchet@40145
|
631 |
|
blanchet@40145
|
632 |
structure Int_Tysubst_Table =
|
blanchet@40145
|
633 |
Table(type key = int * (indexname * (sort * typ)) list
|
blanchet@40145
|
634 |
val ord = prod_ord int_ord tysubst_ord)
|
blanchet@40145
|
635 |
|
blanchet@40145
|
636 |
structure Int_Pair_Graph =
|
blanchet@40145
|
637 |
Graph(type key = int * int val ord = prod_ord int_ord int_ord)
|
blanchet@40145
|
638 |
|
blanchet@43135
|
639 |
fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (axiom_no, index_no)
|
blanchet@40501
|
640 |
fun shuffle_ord p = prod_ord int_ord int_ord (pairself shuffle_key p)
|
blanchet@40501
|
641 |
|
blanchet@40145
|
642 |
(* Attempts to derive the theorem "False" from a theorem of the form
|
blanchet@40145
|
643 |
"P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the
|
blanchet@40145
|
644 |
specified axioms. The axioms have leading "All" and "Ex" quantifiers, which
|
blanchet@40145
|
645 |
must be eliminated first. *)
|
blanchet@40145
|
646 |
fun discharge_skolem_premises ctxt axioms prems_imp_false =
|
blanchet@40145
|
647 |
if prop_of prems_imp_false aconv @{prop False} then
|
blanchet@40145
|
648 |
prems_imp_false
|
blanchet@40145
|
649 |
else
|
blanchet@40145
|
650 |
let
|
wenzelm@43232
|
651 |
val thy = Proof_Context.theory_of ctxt
|
blanchet@40145
|
652 |
fun match_term p =
|
blanchet@40145
|
653 |
let
|
blanchet@40145
|
654 |
val (tyenv, tenv) =
|
blanchet@40145
|
655 |
Pattern.first_order_match thy p (Vartab.empty, Vartab.empty)
|
blanchet@40145
|
656 |
val tsubst =
|
blanchet@40145
|
657 |
tenv |> Vartab.dest
|
blanchet@42963
|
658 |
|> filter (Meson_Clausify.is_zapped_var_name o fst o fst)
|
blanchet@40145
|
659 |
|> sort (cluster_ord
|
blanchet@40145
|
660 |
o pairself (Meson_Clausify.cluster_of_zapped_var_name
|
blanchet@40145
|
661 |
o fst o fst))
|
blanchet@40145
|
662 |
|> map (Meson.term_pair_of
|
blanchet@40145
|
663 |
#> pairself (Envir.subst_term_types tyenv))
|
blanchet@40145
|
664 |
val tysubst = tyenv |> Vartab.dest
|
blanchet@40145
|
665 |
in (tysubst, tsubst) end
|
blanchet@40145
|
666 |
fun subst_info_for_prem subgoal_no prem =
|
blanchet@40145
|
667 |
case prem of
|
blanchet@40145
|
668 |
_ $ (Const (@{const_name Meson.skolem}, _) $ (_ $ t $ num)) =>
|
blanchet@40145
|
669 |
let val ax_no = HOLogic.dest_nat num in
|
blanchet@40145
|
670 |
(ax_no, (subgoal_no,
|
blanchet@40145
|
671 |
match_term (nth axioms ax_no |> the |> snd, t)))
|
blanchet@40145
|
672 |
end
|
blanchet@40145
|
673 |
| _ => raise TERM ("discharge_skolem_premises: Malformed premise",
|
blanchet@40145
|
674 |
[prem])
|
blanchet@40145
|
675 |
fun cluster_of_var_name skolem s =
|
blanchet@42962
|
676 |
case try Meson_Clausify.cluster_of_zapped_var_name s of
|
blanchet@42962
|
677 |
NONE => NONE
|
blanchet@42962
|
678 |
| SOME ((ax_no, (cluster_no, _)), skolem') =>
|
blanchet@40145
|
679 |
if skolem' = skolem andalso cluster_no > 0 then
|
blanchet@40145
|
680 |
SOME (ax_no, cluster_no)
|
blanchet@40145
|
681 |
else
|
blanchet@40145
|
682 |
NONE
|
blanchet@40145
|
683 |
fun clusters_in_term skolem t =
|
blanchet@40145
|
684 |
Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst)
|
blanchet@40145
|
685 |
fun deps_for_term_subst (var, t) =
|
blanchet@40145
|
686 |
case clusters_in_term false var of
|
blanchet@40145
|
687 |
[] => NONE
|
blanchet@40145
|
688 |
| [(ax_no, cluster_no)] =>
|
blanchet@40145
|
689 |
SOME ((ax_no, cluster_no),
|
blanchet@40145
|
690 |
clusters_in_term true t
|
blanchet@40145
|
691 |
|> cluster_no > 1 ? cons (ax_no, cluster_no - 1))
|
blanchet@40145
|
692 |
| _ => raise TERM ("discharge_skolem_premises: Expected Var", [var])
|
blanchet@40145
|
693 |
val prems = Logic.strip_imp_prems (prop_of prems_imp_false)
|
blanchet@40145
|
694 |
val substs = prems |> map2 subst_info_for_prem (1 upto length prems)
|
blanchet@40145
|
695 |
|> sort (int_ord o pairself fst)
|
blanchet@40145
|
696 |
val depss = maps (map_filter deps_for_term_subst o snd o snd o snd) substs
|
blanchet@40145
|
697 |
val clusters = maps (op ::) depss
|
blanchet@40145
|
698 |
val ordered_clusters =
|
blanchet@40145
|
699 |
Int_Pair_Graph.empty
|
blanchet@40145
|
700 |
|> fold Int_Pair_Graph.default_node (map (rpair ()) clusters)
|
blanchet@40145
|
701 |
|> fold Int_Pair_Graph.add_deps_acyclic depss
|
blanchet@40145
|
702 |
|> Int_Pair_Graph.topological_order
|
blanchet@40145
|
703 |
handle Int_Pair_Graph.CYCLES _ =>
|
blanchet@40399
|
704 |
error "Cannot replay Metis proof in Isabelle without \
|
blanchet@40399
|
705 |
\\"Hilbert_Choice\"."
|
blanchet@40145
|
706 |
val ax_counts =
|
blanchet@40145
|
707 |
Int_Tysubst_Table.empty
|
blanchet@40145
|
708 |
|> fold (fn (ax_no, (_, (tysubst, _))) =>
|
blanchet@44100
|
709 |
Int_Tysubst_Table.map_default ((ax_no, [](*###*)), 0)
|
blanchet@40145
|
710 |
(Integer.add 1)) substs
|
blanchet@40145
|
711 |
|> Int_Tysubst_Table.dest
|
blanchet@43210
|
712 |
val needed_axiom_props =
|
blanchet@43210
|
713 |
0 upto length axioms - 1 ~~ axioms
|
blanchet@43210
|
714 |
|> map_filter (fn (_, NONE) => NONE
|
blanchet@43210
|
715 |
| (ax_no, SOME (_, t)) =>
|
blanchet@43210
|
716 |
if exists (fn ((ax_no', _), n) =>
|
blanchet@43210
|
717 |
ax_no' = ax_no andalso n > 0)
|
blanchet@43210
|
718 |
ax_counts then
|
blanchet@43210
|
719 |
SOME t
|
blanchet@43210
|
720 |
else
|
blanchet@43210
|
721 |
NONE)
|
blanchet@43210
|
722 |
val outer_param_names =
|
blanchet@43210
|
723 |
[] |> fold Term.add_var_names needed_axiom_props
|
blanchet@43210
|
724 |
|> filter (Meson_Clausify.is_zapped_var_name o fst)
|
blanchet@43210
|
725 |
|> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst))
|
blanchet@43210
|
726 |
|> filter (fn (((_, (cluster_no, _)), skolem), _) =>
|
blanchet@43210
|
727 |
cluster_no = 0 andalso skolem)
|
blanchet@43210
|
728 |
|> sort shuffle_ord |> map (fst o snd)
|
blanchet@43134
|
729 |
(* for debugging only:
|
blanchet@40145
|
730 |
fun string_for_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) =
|
blanchet@40145
|
731 |
"ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^
|
blanchet@40145
|
732 |
"; tysubst: " ^ PolyML.makestring tysubst ^ "; tsubst: {" ^
|
blanchet@40145
|
733 |
commas (map ((fn (s, t) => s ^ " |-> " ^ t)
|
blanchet@40145
|
734 |
o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}"
|
blanchet@40507
|
735 |
val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters)
|
blanchet@40507
|
736 |
val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts)
|
blanchet@43210
|
737 |
val _ = tracing ("OUTER PARAMS: " ^ PolyML.makestring outer_param_names)
|
blanchet@40145
|
738 |
val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
|
blanchet@40145
|
739 |
cat_lines (map string_for_subst_info substs))
|
blanchet@40145
|
740 |
*)
|
blanchet@43135
|
741 |
fun cut_and_ex_tac axiom =
|
blanchet@43135
|
742 |
cut_rules_tac [axiom] 1
|
blanchet@43135
|
743 |
THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
|
blanchet@40145
|
744 |
fun rotation_for_subgoal i =
|
blanchet@40145
|
745 |
find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs
|
blanchet@40145
|
746 |
in
|
blanchet@40145
|
747 |
Goal.prove ctxt [] [] @{prop False}
|
blanchet@43135
|
748 |
(K (DETERM (EVERY (map (cut_and_ex_tac o fst o the o nth axioms o fst
|
blanchet@43135
|
749 |
o fst) ax_counts)
|
blanchet@43135
|
750 |
THEN rename_tac outer_param_names 1
|
blanchet@43135
|
751 |
THEN copy_prems_tac (map snd ax_counts) [] 1)
|
blanchet@40501
|
752 |
THEN release_clusters_tac thy ax_counts substs ordered_clusters 1
|
blanchet@40145
|
753 |
THEN match_tac [prems_imp_false] 1
|
blanchet@40145
|
754 |
THEN ALLGOALS (fn i =>
|
blanchet@40145
|
755 |
rtac @{thm Meson.skolem_COMBK_I} i
|
blanchet@40145
|
756 |
THEN rotate_tac (rotation_for_subgoal i) i
|
blanchet@43213
|
757 |
THEN PRIMITIVE (unify_first_prem_with_concl thy i)
|
blanchet@43135
|
758 |
THEN assume_tac i
|
blanchet@43134
|
759 |
THEN flexflex_tac)))
|
blanchet@40399
|
760 |
handle ERROR _ =>
|
blanchet@40399
|
761 |
error ("Cannot replay Metis proof in Isabelle:\n\
|
blanchet@40399
|
762 |
\Error when discharging Skolem assumptions.")
|
blanchet@40145
|
763 |
end
|
blanchet@40145
|
764 |
|
blanchet@39735
|
765 |
end;
|