author | paulson |
Mon, 07 Sep 2009 13:19:09 +0100 | |
changeset 32532 | a0a54a51b15b |
parent 32530 | 1beb4275eb64 |
child 32535 | b4d49a4f4436 |
permissions | -rw-r--r-- |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/metis_tools.ML |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
2 |
Author: Kong W. Susanto and Lawrence C. Paulson, CU Computer Laboratory |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
3 |
Copyright Cambridge University 2007 |
23447 | 4 |
|
29266 | 5 |
HOL setup for the Metis prover. |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
6 |
*) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
7 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
8 |
signature METIS_TOOLS = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
9 |
sig |
24309
01f3e1a43c24
turned type_lits into configuration option (with attribute);
wenzelm
parents:
24300
diff
changeset
|
10 |
val type_lits: bool Config.T |
24319 | 11 |
val metis_tac: Proof.context -> thm list -> int -> tactic |
12 |
val metisF_tac: Proof.context -> thm list -> int -> tactic |
|
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
13 |
val metisFT_tac: Proof.context -> thm list -> int -> tactic |
24319 | 14 |
val setup: theory -> theory |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
15 |
end |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
16 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
17 |
structure MetisTools: METIS_TOOLS = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
18 |
struct |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
19 |
|
24424 | 20 |
structure Recon = ResReconstruct; |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
21 |
|
24309
01f3e1a43c24
turned type_lits into configuration option (with attribute);
wenzelm
parents:
24300
diff
changeset
|
22 |
val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" true; |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
23 |
|
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
24 |
datatype mode = FO | HO | FT (*first-order, higher-order, fully-typed*) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
25 |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
26 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
27 |
(* Useful Theorems *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
28 |
(* ------------------------------------------------------------------------- *) |
27239 | 29 |
val EXCLUDED_MIDDLE = rotate_prems 1 (read_instantiate @{context} [(("R", 0), "False")] notE); |
27230 | 30 |
val REFL_THM = incr_indexes 2 (Meson.make_meta_clause refl); (*Rename from 0,1*) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
31 |
val subst_em = zero_var_indexes (subst RS EXCLUDED_MIDDLE); |
27239 | 32 |
val ssubst_em = read_instantiate @{context} [(("t", 0), "?s"), (("s", 0), "?t")] (sym RS subst_em); |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
33 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
34 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
35 |
(* Useful Functions *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
36 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
37 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
38 |
(* match untyped terms*) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
39 |
fun untyped_aconv (Const(a,_)) (Const(b,_)) = (a=b) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
40 |
| untyped_aconv (Free(a,_)) (Free(b,_)) = (a=b) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
41 |
| untyped_aconv (Var((a,_),_)) (Var((b,_),_)) = (a=b) (*the index is ignored!*) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
42 |
| untyped_aconv (Bound i) (Bound j) = (i=j) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
43 |
| untyped_aconv (Abs(a,_,t)) (Abs(b,_,u)) = (a=b) andalso untyped_aconv t u |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
44 |
| untyped_aconv (t1$t2) (u1$u2) = untyped_aconv t1 u1 andalso untyped_aconv t2 u2 |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
45 |
| untyped_aconv _ _ = false; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
46 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
47 |
(* Finding the relative location of an untyped term within a list of terms *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
48 |
fun get_index lit = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
49 |
let val lit = Envir.eta_contract lit |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
50 |
fun get n [] = raise Empty |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
51 |
| get n (x::xs) = if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x)) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
52 |
then n else get (n+1) xs |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
53 |
in get 1 end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
54 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
55 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
56 |
(* HOL to FOL (Isabelle to Metis) *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
57 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
58 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
59 |
fun fn_isa_to_met "equal" = "=" |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
60 |
| fn_isa_to_met x = x; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
61 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
62 |
fun metis_lit b c args = (b, (c, args)); |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
63 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
64 |
fun hol_type_to_fol (ResClause.AtomV x) = Metis.Term.Var x |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
65 |
| hol_type_to_fol (ResClause.AtomF x) = Metis.Term.Fn(x,[]) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
66 |
| hol_type_to_fol (ResClause.Comp(tc,tps)) = Metis.Term.Fn(tc, map hol_type_to_fol tps); |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
67 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
68 |
(*These two functions insert type literals before the real literals. That is the |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
69 |
opposite order from TPTP linkup, but maybe OK.*) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
70 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
71 |
fun hol_term_to_fol_FO tm = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
72 |
case ResHolClause.strip_comb tm of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
73 |
(ResHolClause.CombConst(c,_,tys), tms) => |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
74 |
let val tyargs = map hol_type_to_fol tys |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
75 |
val args = map hol_term_to_fol_FO tms |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
76 |
in Metis.Term.Fn (c, tyargs @ args) end |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
77 |
| (ResHolClause.CombVar(v,_), []) => Metis.Term.Var v |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
78 |
| _ => error "hol_term_to_fol_FO"; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
79 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
80 |
fun hol_term_to_fol_HO (ResHolClause.CombVar(a, ty)) = Metis.Term.Var a |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
81 |
| hol_term_to_fol_HO (ResHolClause.CombConst(a, ty, tylist)) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
82 |
Metis.Term.Fn(fn_isa_to_met a, map hol_type_to_fol tylist) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
83 |
| hol_term_to_fol_HO (ResHolClause.CombApp(tm1,tm2)) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
84 |
Metis.Term.Fn(".", map hol_term_to_fol_HO [tm1,tm2]); |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
85 |
|
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
86 |
(*The fully-typed translation, to avoid type errors*) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
87 |
fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, hol_type_to_fol ty]); |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
88 |
|
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
89 |
fun hol_term_to_fol_FT (ResHolClause.CombVar(a, ty)) = |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
90 |
wrap_type (Metis.Term.Var a, ty) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
91 |
| hol_term_to_fol_FT (ResHolClause.CombConst(a, ty, _)) = |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
92 |
wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
93 |
| hol_term_to_fol_FT (tm as ResHolClause.CombApp(tm1,tm2)) = |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
94 |
wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]), |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
95 |
ResHolClause.type_of_combterm tm); |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
96 |
|
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
97 |
fun hol_literal_to_fol FO (ResHolClause.Literal (pol, tm)) = |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
98 |
let val (ResHolClause.CombConst(p,_,tys), tms) = ResHolClause.strip_comb tm |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
99 |
val tylits = if p = "equal" then [] else map hol_type_to_fol tys |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
100 |
val lits = map hol_term_to_fol_FO tms |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
101 |
in metis_lit pol (fn_isa_to_met p) (tylits @ lits) end |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
102 |
| hol_literal_to_fol HO (ResHolClause.Literal (pol, tm)) = |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
103 |
(case ResHolClause.strip_comb tm of |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
104 |
(ResHolClause.CombConst("equal",_,_), tms) => |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
105 |
metis_lit pol "=" (map hol_term_to_fol_HO tms) |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
106 |
| _ => metis_lit pol "{}" [hol_term_to_fol_HO tm]) (*hBOOL*) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
107 |
| hol_literal_to_fol FT (ResHolClause.Literal (pol, tm)) = |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
108 |
(case ResHolClause.strip_comb tm of |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
109 |
(ResHolClause.CombConst("equal",_,_), tms) => |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
110 |
metis_lit pol "=" (map hol_term_to_fol_FT tms) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
111 |
| _ => metis_lit pol "{}" [hol_term_to_fol_FT tm]) (*hBOOL*); |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
112 |
|
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
113 |
fun literals_of_hol_thm thy mode t = |
24319 | 114 |
let val (lits, types_sorts) = ResHolClause.literals_of_term thy t |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
115 |
in (map (hol_literal_to_fol mode) lits, types_sorts) end; |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
116 |
|
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset
|
117 |
(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*) |
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset
|
118 |
fun metis_of_typeLit pos (ResClause.LTVar (s,x)) = metis_lit pos s [Metis.Term.Var x] |
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset
|
119 |
| metis_of_typeLit pos (ResClause.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])]; |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
120 |
|
24940 | 121 |
fun default_sort ctxt (TVar _) = false |
122 |
| default_sort ctxt (TFree(x,s)) = (s = Option.getOpt (Variable.def_sort ctxt (x,~1), [])); |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
123 |
|
25713 | 124 |
fun metis_of_tfree tf = |
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset
|
125 |
Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_typeLit true tf)); |
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset
|
126 |
|
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
127 |
fun hol_thm_to_fol is_conjecture ctxt mode th = |
24319 | 128 |
let val thy = ProofContext.theory_of ctxt |
129 |
val (mlits, types_sorts) = |
|
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
130 |
(literals_of_hol_thm thy mode o HOLogic.dest_Trueprop o prop_of) th |
25713 | 131 |
in |
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset
|
132 |
if is_conjecture then |
25713 | 133 |
(Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), ResClause.add_typs types_sorts) |
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset
|
134 |
else |
25713 | 135 |
let val tylits = ResClause.add_typs |
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset
|
136 |
(filter (not o default_sort ctxt) types_sorts) |
25713 | 137 |
val mtylits = if Config.get ctxt type_lits |
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset
|
138 |
then map (metis_of_typeLit false) tylits else [] |
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset
|
139 |
in |
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset
|
140 |
(Metis.Thm.axiom (Metis.LiteralSet.fromList(mtylits @ mlits)), []) |
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset
|
141 |
end |
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset
|
142 |
end; |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
143 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
144 |
(* ARITY CLAUSE *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
145 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
146 |
fun m_arity_cls (ResClause.TConsLit (c,t,args)) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
147 |
metis_lit true (ResClause.make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)] |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
148 |
| m_arity_cls (ResClause.TVarLit (c,str)) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
149 |
metis_lit false (ResClause.make_type_class c) [Metis.Term.Var str]; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
150 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
151 |
(*TrueI is returned as the Isabelle counterpart because there isn't any.*) |
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset
|
152 |
fun arity_cls (ResClause.ArityClause{conclLit,premLits,...}) = |
25713 | 153 |
(TrueI, |
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset
|
154 |
Metis.Thm.axiom (Metis.LiteralSet.fromList (map m_arity_cls (conclLit :: premLits)))); |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
155 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
156 |
(* CLASSREL CLAUSE *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
157 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
158 |
fun m_classrel_cls subclass superclass = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
159 |
[metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]]; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
160 |
|
24309
01f3e1a43c24
turned type_lits into configuration option (with attribute);
wenzelm
parents:
24300
diff
changeset
|
161 |
fun classrel_cls (ResClause.ClassrelClause {axiom_name,subclass,superclass,...}) = |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
162 |
(TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass))); |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
163 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
164 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
165 |
(* FOL to HOL (Metis to Isabelle) *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
166 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
167 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
168 |
datatype term_or_type = Term of Term.term | Type of Term.typ; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
169 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
170 |
fun terms_of [] = [] |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
171 |
| terms_of (Term t :: tts) = t :: terms_of tts |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
172 |
| terms_of (Type _ :: tts) = terms_of tts; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
173 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
174 |
fun types_of [] = [] |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
175 |
| types_of (Term (Term.Var((a,idx), T)) :: tts) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
176 |
if String.isPrefix "_" a then |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
177 |
(*Variable generated by Metis, which might have been a type variable.*) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
178 |
TVar(("'" ^ a, idx), HOLogic.typeS) :: types_of tts |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
179 |
else types_of tts |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
180 |
| types_of (Term _ :: tts) = types_of tts |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
181 |
| types_of (Type T :: tts) = T :: types_of tts; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
182 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
183 |
fun apply_list rator nargs rands = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
184 |
let val trands = terms_of rands |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
185 |
in if length trands = nargs then Term (list_comb(rator, trands)) |
26423
8408edac8f6b
removed Display.raw_string_of_XXX (use regular Sign.string_of_XXX);
wenzelm
parents:
25761
diff
changeset
|
186 |
else error |
26957 | 187 |
("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^ |
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26931
diff
changeset
|
188 |
" expected " ^ Int.toString nargs ^ |
26957 | 189 |
" received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands)) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
190 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
191 |
|
24500 | 192 |
fun infer_types ctxt = |
193 |
Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt); |
|
25713 | 194 |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
195 |
(*We use 1 rather than 0 because variable references in clauses may otherwise conflict |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
196 |
with variable constraints in the goal...at least, type inference often fails otherwise. |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
197 |
SEE ALSO axiom_inf below.*) |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
198 |
fun mk_var (w,T) = Term.Var((w,1), T); |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
199 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
200 |
(*include the default sort, if available*) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
201 |
fun mk_tfree ctxt w = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
202 |
let val ww = "'" ^ w |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
203 |
in TFree(ww, getOpt (Variable.def_sort ctxt (ww,~1), HOLogic.typeS)) end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
204 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
205 |
(*Remove the "apply" operator from an HO term*) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
206 |
fun strip_happ args (Metis.Term.Fn(".",[t,u])) = strip_happ (u::args) t |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
207 |
| strip_happ args x = (x, args); |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
208 |
|
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
209 |
fun fol_type_to_isa ctxt (Metis.Term.Var v) = |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
210 |
(case Recon.strip_prefix ResClause.tvar_prefix v of |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
211 |
SOME w => Recon.make_tvar w |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
212 |
| NONE => Recon.make_tvar v) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
213 |
| fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) = |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
214 |
(case Recon.strip_prefix ResClause.tconst_prefix x of |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
215 |
SOME tc => Term.Type (Recon.invert_type_const tc, map (fol_type_to_isa ctxt) tys) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
216 |
| NONE => |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
217 |
case Recon.strip_prefix ResClause.tfree_prefix x of |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
218 |
SOME tf => mk_tfree ctxt tf |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
219 |
| NONE => error ("fol_type_to_isa: " ^ x)); |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
220 |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
221 |
(*Maps metis terms to isabelle terms*) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
222 |
fun fol_term_to_hol_RAW ctxt fol_tm = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
223 |
let val thy = ProofContext.theory_of ctxt |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
224 |
val _ = Output.debug (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
225 |
fun tm_to_tt (Metis.Term.Var v) = |
24424 | 226 |
(case Recon.strip_prefix ResClause.tvar_prefix v of |
227 |
SOME w => Type (Recon.make_tvar w) |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
228 |
| NONE => |
24424 | 229 |
case Recon.strip_prefix ResClause.schematic_var_prefix v of |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
230 |
SOME w => Term (mk_var (w, HOLogic.typeT)) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
231 |
| NONE => Term (mk_var (v, HOLogic.typeT)) ) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
232 |
(*Var from Metis with a name like _nnn; possibly a type variable*) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
233 |
| tm_to_tt (Metis.Term.Fn ("{}", [arg])) = tm_to_tt arg (*hBOOL*) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
234 |
| tm_to_tt (t as Metis.Term.Fn (".",_)) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
235 |
let val (rator,rands) = strip_happ [] t |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
236 |
in case rator of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
237 |
Metis.Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
238 |
| _ => case tm_to_tt rator of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
239 |
Term t => Term (list_comb(t, terms_of (map tm_to_tt rands))) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
240 |
| _ => error "tm_to_tt: HO application" |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
241 |
end |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
242 |
| tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
243 |
and applic_to_tt ("=",ts) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
244 |
Term (list_comb(Const ("op =", HOLogic.typeT), terms_of (map tm_to_tt ts))) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
245 |
| applic_to_tt (a,ts) = |
24424 | 246 |
case Recon.strip_prefix ResClause.const_prefix a of |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
247 |
SOME b => |
24424 | 248 |
let val c = Recon.invert_const b |
249 |
val ntypes = Recon.num_typargs thy c |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
250 |
val nterms = length ts - ntypes |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
251 |
val tts = map tm_to_tt ts |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
252 |
val tys = types_of (List.take(tts,ntypes)) |
24424 | 253 |
val ntyargs = Recon.num_typargs thy c |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
254 |
in if length tys = ntyargs then |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
255 |
apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes)) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
256 |
else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^ |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
257 |
" but gets " ^ Int.toString (length tys) ^ |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
258 |
" type arguments\n" ^ |
26931 | 259 |
cat_lines (map (Syntax.string_of_typ ctxt) tys) ^ |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
260 |
" the terms are \n" ^ |
26931 | 261 |
cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts))) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
262 |
end |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
263 |
| NONE => (*Not a constant. Is it a type constructor?*) |
24424 | 264 |
case Recon.strip_prefix ResClause.tconst_prefix a of |
265 |
SOME b => Type (Term.Type(Recon.invert_type_const b, types_of (map tm_to_tt ts))) |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
266 |
| NONE => (*Maybe a TFree. Should then check that ts=[].*) |
24424 | 267 |
case Recon.strip_prefix ResClause.tfree_prefix a of |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
268 |
SOME b => Type (mk_tfree ctxt b) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
269 |
| NONE => (*a fixed variable? They are Skolem functions.*) |
24424 | 270 |
case Recon.strip_prefix ResClause.fixed_var_prefix a of |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
271 |
SOME b => |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
272 |
let val opr = Term.Free(b, HOLogic.typeT) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
273 |
in apply_list opr (length ts) (map tm_to_tt ts) end |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
274 |
| NONE => error ("unexpected metis function: " ^ a) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
275 |
in case tm_to_tt fol_tm of Term t => t | _ => error "fol_tm_to_tt: Term expected" end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
276 |
|
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
277 |
(*Maps fully-typed metis terms to isabelle terms*) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
278 |
fun fol_term_to_hol_FT ctxt fol_tm = |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
279 |
let val _ = Output.debug (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
280 |
fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, ty])) = |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
281 |
(case Recon.strip_prefix ResClause.schematic_var_prefix v of |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
282 |
SOME w => mk_var(w, dummyT) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
283 |
| NONE => mk_var(v, dummyT)) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
284 |
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) = |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
285 |
(case Recon.strip_prefix ResClause.const_prefix x of |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
286 |
SOME c => Const (Recon.invert_const c, dummyT) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
287 |
| NONE => (*Not a constant. Is it a fixed variable??*) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
288 |
case Recon.strip_prefix ResClause.fixed_var_prefix x of |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
289 |
SOME v => Free (v, fol_type_to_isa ctxt ty) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
290 |
| NONE => if x = "=" then Const ("op =", HOLogic.typeT) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
291 |
else error ("fol_term_to_hol_FT bad constant: " ^ x)) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
292 |
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) = |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
293 |
cvt tm1 $ cvt tm2 |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
294 |
| cvt (Metis.Term.Fn (".",[tm1,tm2])) = (*untyped application*) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
295 |
cvt tm1 $ cvt tm2 |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
296 |
| cvt (Metis.Term.Fn ("{}", [arg])) = cvt arg (*hBOOL*) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
297 |
| cvt (Metis.Term.Fn ("=", [tm1,tm2])) = |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
298 |
list_comb(Const ("op =", HOLogic.typeT), map cvt [tm1,tm2]) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
299 |
| cvt (t as Metis.Term.Fn (x, [])) = |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
300 |
(case Recon.strip_prefix ResClause.const_prefix x of |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
301 |
SOME c => Const (Recon.invert_const c, dummyT) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
302 |
| NONE => (*Not a constant. Is it a fixed variable??*) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
303 |
case Recon.strip_prefix ResClause.fixed_var_prefix x of |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
304 |
SOME v => Free (v, dummyT) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
305 |
| NONE => (Output.debug (fn () => "fol_term_to_hol_FT bad const: " ^ x); fol_term_to_hol_RAW ctxt t)) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
306 |
| cvt t = (Output.debug (fn () => "fol_term_to_hol_FT bad term: " ^ Metis.Term.toString t); fol_term_to_hol_RAW ctxt t) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
307 |
in cvt fol_tm end; |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
308 |
|
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
309 |
fun fol_term_to_hol ctxt FO = fol_term_to_hol_RAW ctxt |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
310 |
| fol_term_to_hol ctxt HO = fol_term_to_hol_RAW ctxt |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
311 |
| fol_term_to_hol ctxt FT = fol_term_to_hol_FT ctxt; |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
312 |
|
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
313 |
fun fol_terms_to_hol ctxt mode fol_tms = |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
314 |
let val ts = map (fol_term_to_hol ctxt mode) fol_tms |
24494
dc387e3999ec
replaced ProofContext.infer_types by general Syntax.check_terms;
wenzelm
parents:
24424
diff
changeset
|
315 |
val _ = Output.debug (fn () => " calling type inference:") |
24920 | 316 |
val _ = app (fn t => Output.debug (fn () => Syntax.string_of_term ctxt t)) ts |
24500 | 317 |
val ts' = infer_types ctxt ts; |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
318 |
val _ = app (fn t => Output.debug |
24920 | 319 |
(fn () => " final term: " ^ Syntax.string_of_term ctxt t ^ |
320 |
" of type " ^ Syntax.string_of_typ ctxt (type_of t))) |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
321 |
ts' |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
322 |
in ts' end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
323 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
324 |
fun mk_not (Const ("Not", _) $ b) = b |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
325 |
| mk_not b = HOLogic.mk_not b; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
326 |
|
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
327 |
val metis_eq = Metis.Term.Fn ("=", []); |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
328 |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
329 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
330 |
(* FOL step Inference Rules *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
331 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
332 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
333 |
(*for debugging only*) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
334 |
fun print_thpair (fth,th) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
335 |
(Output.debug (fn () => "============================================="); |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
336 |
Output.debug (fn () => "Metis: " ^ Metis.Thm.toString fth); |
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32010
diff
changeset
|
337 |
Output.debug (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th)); |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
338 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
339 |
fun lookth thpairs (fth : Metis.Thm.thm) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
340 |
valOf (AList.lookup (uncurry Metis.Thm.equal) thpairs fth) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
341 |
handle Option => error ("Failed to find a Metis theorem " ^ Metis.Thm.toString fth); |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
342 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
343 |
fun is_TrueI th = Thm.eq_thm(TrueI,th); |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
344 |
|
24974 | 345 |
fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx)); |
346 |
||
29266 | 347 |
fun inst_excluded_middle thy i_atm = |
348 |
let val th = EXCLUDED_MIDDLE |
|
349 |
val [vx] = Term.add_vars (prop_of th) [] |
|
350 |
val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)] |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
351 |
in cterm_instantiate substs th end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
352 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
353 |
(* INFERENCE RULE: AXIOM *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
354 |
fun axiom_inf ctxt thpairs th = incr_indexes 1 (lookth thpairs th); |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
355 |
(*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
356 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
357 |
(* INFERENCE RULE: ASSUME *) |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
358 |
fun assume_inf ctxt mode atm = |
29266 | 359 |
inst_excluded_middle |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
360 |
(ProofContext.theory_of ctxt) |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
361 |
(singleton (fol_terms_to_hol ctxt mode) (Metis.Term.Fn atm)); |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
362 |
|
26561 | 363 |
(* INFERENCE RULE: INSTANTIATE (Subst). Type instantiations are ignored. Trying to reconstruct |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
364 |
them admits new possibilities of errors, e.g. concerning sorts. Instead we try to arrange |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
365 |
that new TVars are distinct and that types can be inferred from terms.*) |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
366 |
fun inst_inf ctxt mode thpairs fsubst th = |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
367 |
let val thy = ProofContext.theory_of ctxt |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
368 |
val i_th = lookth thpairs th |
29266 | 369 |
val i_th_vars = Term.add_vars (prop_of i_th) [] |
370 |
fun find_var x = valOf (List.find (fn ((a,_),_) => a=x) i_th_vars) |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
371 |
fun subst_translation (x,y) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
372 |
let val v = find_var x |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
373 |
val t = fol_term_to_hol ctxt mode y (*we call infer_types below*) |
29266 | 374 |
in SOME (cterm_of thy (Var v), t) end |
25713 | 375 |
handle Option => |
376 |
(Output.debug (fn() => "List.find failed for the variable " ^ x ^ |
|
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32010
diff
changeset
|
377 |
" in " ^ Display.string_of_thm ctxt i_th); |
25713 | 378 |
NONE) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
379 |
fun remove_typeinst (a, t) = |
24424 | 380 |
case Recon.strip_prefix ResClause.schematic_var_prefix a of |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
381 |
SOME b => SOME (b, t) |
24424 | 382 |
| NONE => case Recon.strip_prefix ResClause.tvar_prefix a of |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
383 |
SOME _ => NONE (*type instantiations are forbidden!*) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
384 |
| NONE => SOME (a,t) (*internal Metis var?*) |
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32010
diff
changeset
|
385 |
val _ = Output.debug (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
386 |
val substs = List.mapPartial remove_typeinst (Metis.Subst.toList fsubst) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
387 |
val (vars,rawtms) = ListPair.unzip (List.mapPartial subst_translation substs) |
24500 | 388 |
val tms = infer_types ctxt rawtms; |
24974 | 389 |
val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
390 |
val substs' = ListPair.zip (vars, map ctm_of tms) |
32432
64f30bdd3ba1
modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents:
32262
diff
changeset
|
391 |
val _ = Output.debug (fn () => |
64f30bdd3ba1
modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents:
32262
diff
changeset
|
392 |
cat_lines ("subst_translations:" :: |
64f30bdd3ba1
modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents:
32262
diff
changeset
|
393 |
(substs' |> map (fn (x, y) => |
64f30bdd3ba1
modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents:
32262
diff
changeset
|
394 |
Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^ |
64f30bdd3ba1
modernized messages -- eliminated ctyp/cterm operations;
wenzelm
parents:
32262
diff
changeset
|
395 |
Syntax.string_of_term ctxt (term_of y))))); |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
396 |
in cterm_instantiate substs' i_th |
28528
0cf2749e8ef7
The result of the equality inference rule no longer undergoes factoring.
paulson
parents:
28262
diff
changeset
|
397 |
handle THM (msg, _, _) => error ("metis error (inst_inf): " ^ msg) |
0cf2749e8ef7
The result of the equality inference rule no longer undergoes factoring.
paulson
parents:
28262
diff
changeset
|
398 |
end; |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
399 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
400 |
(* INFERENCE RULE: RESOLVE *) |
25713 | 401 |
|
24424 | 402 |
(*Like RSN, but we rename apart only the type variables. Vars here typically have an index |
403 |
of 1, and the use of RSN would increase this typically to 3. Instantiations of those Vars |
|
404 |
could then fail. See comment on mk_var.*) |
|
405 |
fun resolve_inc_tyvars(tha,i,thb) = |
|
406 |
let val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha |
|
31945 | 407 |
val ths = Seq.list_of (Thm.bicompose false (false,tha,nprems_of tha) i thb) |
25713 | 408 |
in |
24424 | 409 |
case distinct Thm.eq_thm ths of |
410 |
[th] => th |
|
411 |
| _ => raise THM ("resolve_inc_tyvars: unique result expected", i, [tha,thb]) |
|
412 |
end; |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
413 |
|
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
414 |
fun resolve_inf ctxt mode thpairs atm th1 th2 = |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
415 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
416 |
val thy = ProofContext.theory_of ctxt |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
417 |
val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2 |
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32010
diff
changeset
|
418 |
val _ = Output.debug (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1) |
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32010
diff
changeset
|
419 |
val _ = Output.debug (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
420 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
421 |
if is_TrueI i_th1 then i_th2 (*Trivial cases where one operand is type info*) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
422 |
else if is_TrueI i_th2 then i_th1 |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
423 |
else |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
424 |
let |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
425 |
val i_atm = singleton (fol_terms_to_hol ctxt mode) (Metis.Term.Fn atm) |
24920 | 426 |
val _ = Output.debug (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
427 |
val prems_th1 = prems_of i_th1 |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
428 |
val prems_th2 = prems_of i_th2 |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
429 |
val index_th1 = get_index (mk_not i_atm) prems_th1 |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
430 |
handle Empty => error "Failed to find literal in th1" |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
431 |
val _ = Output.debug (fn () => " index_th1: " ^ Int.toString index_th1) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
432 |
val index_th2 = get_index i_atm prems_th2 |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
433 |
handle Empty => error "Failed to find literal in th2" |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
434 |
val _ = Output.debug (fn () => " index_th2: " ^ Int.toString index_th2) |
24424 | 435 |
in resolve_inc_tyvars (Meson.select_literal index_th1 i_th1, index_th2, i_th2) end |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
436 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
437 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
438 |
(* INFERENCE RULE: REFL *) |
32010 | 439 |
val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) []))); |
24974 | 440 |
val refl_idx = 1 + Thm.maxidx_of REFL_THM; |
25713 | 441 |
|
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
442 |
fun refl_inf ctxt mode t = |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
443 |
let val thy = ProofContext.theory_of ctxt |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
444 |
val i_t = singleton (fol_terms_to_hol ctxt mode) t |
24974 | 445 |
val _ = Output.debug (fn () => " term: " ^ Syntax.string_of_term ctxt i_t) |
446 |
val c_t = cterm_incr_types thy refl_idx i_t |
|
447 |
in cterm_instantiate [(refl_x, c_t)] REFL_THM end; |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
448 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
449 |
fun get_ty_arg_size thy (Const("op =",_)) = 0 (*equality has no type arguments*) |
24424 | 450 |
| get_ty_arg_size thy (Const(c,_)) = (Recon.num_typargs thy c handle TYPE _ => 0) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
451 |
| get_ty_arg_size thy _ = 0; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
452 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
453 |
(* INFERENCE RULE: EQUALITY *) |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
454 |
fun equality_inf ctxt mode thpairs (pos,atm) fp fr = |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
455 |
let val thy = ProofContext.theory_of ctxt |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
456 |
val m_tm = Metis.Term.Fn atm |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
457 |
val [i_atm,i_tm] = fol_terms_to_hol ctxt mode [m_tm, fr] |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
458 |
val _ = Output.debug (fn () => "sign of the literal: " ^ Bool.toString pos) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
459 |
fun replace_item_list lx 0 (l::ls) = lx::ls |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
460 |
| replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
461 |
fun path_finder_FO tm [] = (tm, Term.Bound 0) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
462 |
| path_finder_FO tm (p::ps) = |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
463 |
let val (tm1,args) = Term.strip_comb tm |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
464 |
val adjustment = get_ty_arg_size thy tm1 |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
465 |
val p' = if adjustment > p then p else p-adjustment |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
466 |
val tm_p = List.nth(args,p') |
24920 | 467 |
handle Subscript => error ("equality_inf: " ^ Int.toString p ^ " adj " ^ |
468 |
Int.toString adjustment ^ " term " ^ Syntax.string_of_term ctxt tm) |
|
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
469 |
val _ = Output.debug (fn () => "path_finder: " ^ Int.toString p ^ |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
470 |
" " ^ Syntax.string_of_term ctxt tm_p) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
471 |
val (r,t) = path_finder_FO tm_p ps |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
472 |
in |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
473 |
(r, list_comb (tm1, replace_item_list t p' args)) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
474 |
end |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
475 |
fun path_finder_HO tm [] = (tm, Term.Bound 0) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
476 |
| path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
477 |
| path_finder_HO (t$u) (p::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps) |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
478 |
fun path_finder_FT tm [] _ = (tm, Term.Bound 0) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
479 |
| path_finder_FT tm (0::ps) (Metis.Term.Fn ("ti", [t1,t2])) = |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
480 |
path_finder_FT tm ps t1 |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
481 |
| path_finder_FT (t$u) (0::ps) (Metis.Term.Fn (".", [t1,t2])) = |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
482 |
(fn(x,y) => (x, y$u)) (path_finder_FT t ps t1) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
483 |
| path_finder_FT (t$u) (1::ps) (Metis.Term.Fn (".", [t1,t2])) = |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
484 |
(fn(x,y) => (x, t$y)) (path_finder_FT u ps t2) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
485 |
| path_finder_FT tm ps t = error ("equality_inf, path_finder_FT: path = " ^ |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
486 |
space_implode " " (map Int.toString ps) ^ |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
487 |
" isa-term: " ^ Syntax.string_of_term ctxt tm ^ |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
488 |
" fol-term: " ^ Metis.Term.toString t) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
489 |
fun path_finder FO tm ps _ = path_finder_FO tm ps |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
490 |
| path_finder HO (tm as Const("op =",_) $ _ $ _) (p::ps) _ = |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
491 |
(*equality: not curried, as other predicates are*) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
492 |
if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
493 |
else path_finder_HO tm (p::ps) (*1 selects second operand*) |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
494 |
| path_finder HO tm (p::ps) (Metis.Term.Fn ("{}", [t1])) = |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
495 |
path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*) |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
496 |
| path_finder FT (tm as Const("op =",_) $ _ $ _) (p::ps) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
497 |
(Metis.Term.Fn ("=", [t1,t2])) = |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
498 |
(*equality: not curried, as other predicates are*) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
499 |
if p=0 then path_finder_FT tm (0::1::ps) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
500 |
(Metis.Term.Fn (".", [Metis.Term.Fn (".", [metis_eq,t1]), t2])) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
501 |
(*select first operand*) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
502 |
else path_finder_FT tm (p::ps) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
503 |
(Metis.Term.Fn (".", [metis_eq,t2])) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
504 |
(*1 selects second operand*) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
505 |
| path_finder FT tm (p::ps) (Metis.Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1 |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
506 |
(*if not equality, ignore head to skip the hBOOL predicate*) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
507 |
| path_finder FT tm ps t = path_finder_FT tm ps t (*really an error case!*) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
508 |
fun path_finder_lit ((nt as Term.Const ("Not", _)) $ tm_a) idx = |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
509 |
let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
510 |
in (tm, nt $ tm_rslt) end |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
511 |
| path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
512 |
val (tm_subst, body) = path_finder_lit i_atm fp |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
513 |
val tm_abs = Term.Abs("x", Term.type_of tm_subst, body) |
24920 | 514 |
val _ = Output.debug (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs) |
515 |
val _ = Output.debug (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm) |
|
516 |
val _ = Output.debug (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst) |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
517 |
val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill typed but gives right max*) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
518 |
val subst' = incr_indexes (imax+1) (if pos then subst_em else ssubst_em) |
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32010
diff
changeset
|
519 |
val _ = Output.debug (fn () => "subst' " ^ Display.string_of_thm ctxt subst') |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
520 |
val eq_terms = map (pairself (cterm_of thy)) |
29266 | 521 |
(ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm])) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
522 |
in cterm_instantiate eq_terms subst' end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
523 |
|
28528
0cf2749e8ef7
The result of the equality inference rule no longer undergoes factoring.
paulson
parents:
28262
diff
changeset
|
524 |
val factor = Seq.hd o distinct_subgoals_tac; |
0cf2749e8ef7
The result of the equality inference rule no longer undergoes factoring.
paulson
parents:
28262
diff
changeset
|
525 |
|
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
526 |
fun step ctxt mode thpairs (fol_th, Metis.Proof.Axiom _) = |
28528
0cf2749e8ef7
The result of the equality inference rule no longer undergoes factoring.
paulson
parents:
28262
diff
changeset
|
527 |
factor (axiom_inf ctxt thpairs fol_th) |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
528 |
| step ctxt mode thpairs (_, Metis.Proof.Assume f_atm) = |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
529 |
assume_inf ctxt mode f_atm |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
530 |
| step ctxt mode thpairs (_, Metis.Proof.Subst(f_subst, f_th1)) = |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
531 |
factor (inst_inf ctxt mode thpairs f_subst f_th1) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
532 |
| step ctxt mode thpairs (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2)) = |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
533 |
factor (resolve_inf ctxt mode thpairs f_atm f_th1 f_th2) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
534 |
| step ctxt mode thpairs (_, Metis.Proof.Refl f_tm) = |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
535 |
refl_inf ctxt mode f_tm |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
536 |
| step ctxt mode thpairs (_, Metis.Proof.Equality(f_lit, f_p, f_r)) = |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
537 |
equality_inf ctxt mode thpairs f_lit f_p f_r; |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
538 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
539 |
fun real_literal (b, (c, _)) = not (String.isPrefix ResClause.class_prefix c); |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
540 |
|
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
541 |
fun translate mode _ thpairs [] = thpairs |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
542 |
| translate mode ctxt thpairs ((fol_th, inf) :: infpairs) = |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
543 |
let val _ = Output.debug (fn () => "=============================================") |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
544 |
val _ = Output.debug (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
545 |
val _ = Output.debug (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf) |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
546 |
val th = Meson.flexflex_first_order (step ctxt mode thpairs (fol_th, inf)) |
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32010
diff
changeset
|
547 |
val _ = Output.debug (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
548 |
val _ = Output.debug (fn () => "=============================================") |
24424 | 549 |
val n_metis_lits = length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th))) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
550 |
in |
24424 | 551 |
if nprems_of th = n_metis_lits then () |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
552 |
else error "Metis: proof reconstruction has gone wrong"; |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
553 |
translate mode ctxt ((fol_th, th) :: thpairs) infpairs |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
554 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
555 |
|
24855 | 556 |
(*Determining which axiom clauses are actually used*) |
25713 | 557 |
fun used_axioms axioms (th, Metis.Proof.Axiom _) = SOME (lookth axioms th) |
24855 | 558 |
| used_axioms axioms _ = NONE; |
559 |
||
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
560 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
561 |
(* Translation of HO Clauses *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
562 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
563 |
|
27178
c8ddb3000743
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27153
diff
changeset
|
564 |
fun cnf_th thy th = hd (ResAxioms.cnf_axiom thy th); |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
565 |
|
32010 | 566 |
val equal_imp_fequal' = cnf_th @{theory} @{thm equal_imp_fequal}; |
567 |
val fequal_imp_equal' = cnf_th @{theory} @{thm fequal_imp_equal}; |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
568 |
|
32010 | 569 |
val comb_I = cnf_th @{theory} ResHolClause.comb_I; |
570 |
val comb_K = cnf_th @{theory} ResHolClause.comb_K; |
|
571 |
val comb_B = cnf_th @{theory} ResHolClause.comb_B; |
|
572 |
val comb_C = cnf_th @{theory} ResHolClause.comb_C; |
|
573 |
val comb_S = cnf_th @{theory} ResHolClause.comb_S; |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
574 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
575 |
fun type_ext thy tms = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
576 |
let val subs = ResAtp.tfree_classes_of_terms tms |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
577 |
val supers = ResAtp.tvar_classes_of_terms tms |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
578 |
and tycons = ResAtp.type_consts_of_terms thy tms |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
579 |
val arity_clauses = ResClause.make_arity_clauses thy tycons supers |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
580 |
val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
581 |
val classrel_clauses = ResClause.make_classrel_clauses thy subs supers' |
24309
01f3e1a43c24
turned type_lits into configuration option (with attribute);
wenzelm
parents:
24300
diff
changeset
|
582 |
in map classrel_cls classrel_clauses @ map arity_cls arity_clauses |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
583 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
584 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
585 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
586 |
(* Logic maps manage the interface between HOL and first-order logic. *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
587 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
588 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
589 |
type logic_map = |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
590 |
{axioms : (Metis.Thm.thm * Thm.thm) list, |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
591 |
tfrees : ResClause.type_literal list}; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
592 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
593 |
fun const_in_metis c (pol,(pred,tm_list)) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
594 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
595 |
fun in_mterm (Metis.Term.Var nm) = false |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
596 |
| in_mterm (Metis.Term.Fn (".", tm_list)) = exists in_mterm tm_list |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
597 |
| in_mterm (Metis.Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
598 |
in c=pred orelse exists in_mterm tm_list end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
599 |
|
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset
|
600 |
(*Extract TFree constraints from context to include as conjecture clauses*) |
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset
|
601 |
fun init_tfrees ctxt = |
24940 | 602 |
let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts |
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset
|
603 |
in ResClause.add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end; |
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset
|
604 |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
605 |
(*transform isabelle type / arity clause to metis clause *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
606 |
fun add_type_thm [] lmap = lmap |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
607 |
| add_type_thm ((ith, mth) :: cls) {axioms, tfrees} = |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
608 |
add_type_thm cls {axioms = (mth, ith) :: axioms, |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
609 |
tfrees = tfrees} |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
610 |
|
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset
|
611 |
(*Insert non-logical axioms corresponding to all accumulated TFrees*) |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
612 |
fun add_tfrees {axioms, tfrees} : logic_map = |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
613 |
{axioms = (map (fn tf => (metis_of_tfree tf, TrueI)) (distinct op= tfrees)) @ axioms, |
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset
|
614 |
tfrees = tfrees}; |
25713 | 615 |
|
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
616 |
fun string_of_mode FO = "FO" |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
617 |
| string_of_mode HO = "HO" |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
618 |
| string_of_mode FT = "FT" |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
619 |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
620 |
(* Function to generate metis clauses, including comb and type clauses *) |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
621 |
fun build_map mode0 ctxt cls ths = |
24958 | 622 |
let val thy = ProofContext.theory_of ctxt |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
623 |
(*The modes FO and FT are sticky. HO can be downgraded to FO.*) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
624 |
fun set_mode FO = FO |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
625 |
| set_mode HO = if forall (Meson.is_fol_term thy o prop_of) (cls@ths) then FO else HO |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
626 |
| set_mode FT = FT |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
627 |
val mode = set_mode mode0 |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
628 |
(*transform isabelle clause to metis clause *) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
629 |
fun add_thm is_conjecture (ith, {axioms, tfrees}) : logic_map = |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
630 |
let val (mth, tfree_lits) = hol_thm_to_fol is_conjecture ctxt mode ith |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
631 |
in |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
632 |
{axioms = (mth, Meson.make_meta_clause ith) :: axioms, |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
633 |
tfrees = tfree_lits union tfrees} |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
634 |
end; |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
635 |
val lmap0 = List.foldl (add_thm true) |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
636 |
{axioms = [], tfrees = init_tfrees ctxt} cls |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
637 |
val lmap = List.foldl (add_thm false) (add_tfrees lmap0) ths |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
638 |
val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
639 |
fun used c = exists (Metis.LiteralSet.exists (const_in_metis c)) clause_lists |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
640 |
(*Now check for the existence of certain combinators*) |
24827 | 641 |
val thI = if used "c_COMBI" then [comb_I] else [] |
642 |
val thK = if used "c_COMBK" then [comb_K] else [] |
|
643 |
val thB = if used "c_COMBB" then [comb_B] else [] |
|
644 |
val thC = if used "c_COMBC" then [comb_C] else [] |
|
645 |
val thS = if used "c_COMBS" then [comb_S] else [] |
|
646 |
val thEQ = if used "c_fequal" then [fequal_imp_equal', equal_imp_fequal'] else [] |
|
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
647 |
val lmap' = if mode=FO then lmap |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
648 |
else List.foldl (add_thm false) lmap (thEQ @ thS @ thC @ thB @ thK @ thI) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
649 |
in |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
650 |
(mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap') |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
651 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
652 |
|
25724
31e7bd574eb9
made refute non-critical (seems to work after avoiding floating point random numbers);
wenzelm
parents:
25713
diff
changeset
|
653 |
fun refute cls = |
31e7bd574eb9
made refute non-critical (seems to work after avoiding floating point random numbers);
wenzelm
parents:
25713
diff
changeset
|
654 |
Metis.Resolution.loop (Metis.Resolution.new Metis.Resolution.default cls); |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
655 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
656 |
fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const); |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
657 |
|
24855 | 658 |
fun common_thm ths1 ths2 = exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2); |
659 |
||
28233
f14f34194f63
The metis method now fails in the usual manner, rather than raising an exception,
paulson
parents:
28175
diff
changeset
|
660 |
exception METIS of string; |
f14f34194f63
The metis method now fails in the usual manner, rather than raising an exception,
paulson
parents:
28175
diff
changeset
|
661 |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
662 |
(* Main function to start metis prove and reconstruction *) |
24855 | 663 |
fun FOL_SOLVE mode ctxt cls ths0 = |
27178
c8ddb3000743
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27153
diff
changeset
|
664 |
let val thy = ProofContext.theory_of ctxt |
27865
27a8ad9612a3
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents:
27239
diff
changeset
|
665 |
val th_cls_pairs = map (fn th => (Thm.get_name_hint th, ResAxioms.cnf_axiom thy th)) ths0 |
24855 | 666 |
val ths = List.concat (map #2 th_cls_pairs) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
667 |
val _ = Output.debug (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") |
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32010
diff
changeset
|
668 |
val _ = app (fn th => Output.debug (fn () => Display.string_of_thm ctxt th)) cls |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
669 |
val _ = Output.debug (fn () => "THEOREM CLAUSES") |
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32010
diff
changeset
|
670 |
val _ = app (fn th => Output.debug (fn () => Display.string_of_thm ctxt th)) ths |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
671 |
val (mode, {axioms,tfrees}) = build_map mode ctxt cls ths |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
672 |
val _ = if null tfrees then () |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
673 |
else (Output.debug (fn () => "TFREE CLAUSES"); |
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset
|
674 |
app (fn tf => Output.debug (fn _ => ResClause.tptp_of_typeLit true tf)) tfrees) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
675 |
val _ = Output.debug (fn () => "CLAUSES GIVEN TO METIS") |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
676 |
val thms = map #1 axioms |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
677 |
val _ = app (fn th => Output.debug (fn () => Metis.Thm.toString th)) thms |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
678 |
val _ = Output.debug (fn () => "mode = " ^ string_of_mode mode) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
679 |
val _ = Output.debug (fn () => "START METIS PROVE PROCESS") |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
680 |
in |
28700
fb92b1d1b285
The metis method no longer fails because the theorem is too trivial
paulson
parents:
28528
diff
changeset
|
681 |
case List.filter (is_false o prop_of) cls of |
fb92b1d1b285
The metis method no longer fails because the theorem is too trivial
paulson
parents:
28528
diff
changeset
|
682 |
false_th::_ => [false_th RS @{thm FalseE}] |
fb92b1d1b285
The metis method no longer fails because the theorem is too trivial
paulson
parents:
28528
diff
changeset
|
683 |
| [] => |
25713 | 684 |
case refute thms of |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
685 |
Metis.Resolution.Contradiction mth => |
28233
f14f34194f63
The metis method now fails in the usual manner, rather than raising an exception,
paulson
parents:
28175
diff
changeset
|
686 |
let val _ = Output.debug (fn () => "METIS RECONSTRUCTION START: " ^ |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
687 |
Metis.Thm.toString mth) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
688 |
val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
689 |
(*add constraints arising from converting goal to clause form*) |
24855 | 690 |
val proof = Metis.Proof.proof mth |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
691 |
val result = translate mode ctxt' axioms proof |
24855 | 692 |
and used = List.mapPartial (used_axioms axioms) proof |
693 |
val _ = Output.debug (fn () => "METIS COMPLETED...clauses actually used:") |
|
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32010
diff
changeset
|
694 |
val _ = app (fn th => Output.debug (fn () => Display.string_of_thm ctxt th)) used |
24855 | 695 |
val unused = filter (fn (a,cls) => not (common_thm used cls)) th_cls_pairs |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
696 |
in |
24855 | 697 |
if null unused then () |
30362 | 698 |
else warning ("Metis: unused theorems " ^ commas_quote (map #1 unused)); |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
699 |
case result of |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
700 |
(_,ith)::_ => |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
701 |
(Output.debug (fn () => "success: " ^ Display.string_of_thm ctxt ith); |
28233
f14f34194f63
The metis method now fails in the usual manner, rather than raising an exception,
paulson
parents:
28175
diff
changeset
|
702 |
[ith]) |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
703 |
| _ => (Output.debug (fn () => "Metis: no result"); |
28233
f14f34194f63
The metis method now fails in the usual manner, rather than raising an exception,
paulson
parents:
28175
diff
changeset
|
704 |
[]) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
705 |
end |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
706 |
| Metis.Resolution.Satisfiable _ => |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
707 |
(Output.debug (fn () => "Metis: No first-order proof with the lemmas supplied"); |
28233
f14f34194f63
The metis method now fails in the usual manner, rather than raising an exception,
paulson
parents:
28175
diff
changeset
|
708 |
[]) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
709 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
710 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
711 |
fun metis_general_tac mode ctxt ths i st0 = |
24041
d5845b7c1a24
metis_tac: proper context (ProofContext.init it *not* sufficient);
wenzelm
parents:
23447
diff
changeset
|
712 |
let val _ = Output.debug (fn () => |
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32010
diff
changeset
|
713 |
"Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths)) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
714 |
in |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
715 |
if exists_type ResAxioms.type_has_empty_sort (prop_of st0) |
28233
f14f34194f63
The metis method now fails in the usual manner, rather than raising an exception,
paulson
parents:
28175
diff
changeset
|
716 |
then (warning "Proof state contains the empty sort"; Seq.empty) |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
717 |
else |
32262 | 718 |
(Meson.MESON ResAxioms.neg_clausify |
719 |
(fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i |
|
28233
f14f34194f63
The metis method now fails in the usual manner, rather than raising an exception,
paulson
parents:
28175
diff
changeset
|
720 |
THEN ResAxioms.expand_defs_tac st0) st0 |
f14f34194f63
The metis method now fails in the usual manner, rather than raising an exception,
paulson
parents:
28175
diff
changeset
|
721 |
end |
f14f34194f63
The metis method now fails in the usual manner, rather than raising an exception,
paulson
parents:
28175
diff
changeset
|
722 |
handle METIS s => (warning ("Metis: " ^ s); Seq.empty); |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
723 |
|
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
724 |
val metis_tac = metis_general_tac HO; |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
725 |
val metisF_tac = metis_general_tac FO; |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
726 |
val metisFT_tac = metis_general_tac FO; |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
727 |
|
30515 | 728 |
fun method name mode comment = Method.setup name (Attrib.thms >> (fn ths => fn ctxt => |
729 |
SIMPLE_METHOD' (CHANGED_PROP o metis_general_tac mode ctxt ths))) comment; |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
730 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
731 |
val setup = |
24309
01f3e1a43c24
turned type_lits into configuration option (with attribute);
wenzelm
parents:
24300
diff
changeset
|
732 |
type_lits_setup #> |
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
733 |
method @{binding metis} HO "METIS for FOL & HOL problems" #> |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
734 |
method @{binding metisF} FO "METIS for FOL problems" #> |
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents:
32530
diff
changeset
|
735 |
method @{binding metisFT} FT "METIS With-fully typed translation" #> |
30515 | 736 |
Method.setup @{binding finish_clausify} |
737 |
(Scan.succeed (K (SIMPLE_METHOD (ResAxioms.expand_defs_tac refl)))) |
|
738 |
"cleanup after conversion to clauses"; |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
739 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
740 |
end; |