author  blanchet 
Thu, 02 Sep 2010 13:45:23 +0200  
changeset 39038  dfea12cc5f5a 
parent 39037  5146d640aa4a 
child 39112  611e41ef07c3 
permissions  rwrr 
35826  1 
(* Title: HOL/Tools/Sledgehammer/metis_tactics.ML 
38027  2 
Author: Kong W. Susanto, Cambridge University Computer Laboratory 
3 
Author: Lawrence C. Paulson, Cambridge University Computer Laboratory 

4 
Author: Jasmin Blanchette, TU Muenchen 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

5 
Copyright Cambridge University 2007 
23447  6 

29266  7 
HOL setup for the Metis prover. 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

8 
*) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

9 

35826  10 
signature METIS_TACTICS = 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

11 
sig 
32955  12 
val trace: bool Unsynchronized.ref 
24309
01f3e1a43c24
turned type_lits into configuration option (with attribute);
wenzelm
parents:
24300
diff
changeset

13 
val type_lits: bool Config.T 
24319  14 
val metis_tac: Proof.context > thm list > int > tactic 
15 
val metisF_tac: Proof.context > thm list > int > tactic 

32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fullytyped version of metis
paulson
parents:
32530
diff
changeset

16 
val metisFT_tac: Proof.context > thm list > int > tactic 
24319  17 
val setup: theory > theory 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

18 
end 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

19 

35826  20 
structure Metis_Tactics : METIS_TACTICS = 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

21 
struct 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

22 

37578
9367cb36b1c4
renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
blanchet
parents:
37577
diff
changeset

23 
open Metis_Clauses 
35826  24 

32956  25 
val trace = Unsynchronized.ref false; 
35826  26 
fun trace_msg msg = if !trace then tracing (msg ()) else (); 
32955  27 

36001  28 
val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true); 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

29 

35826  30 
datatype mode = FO  HO  FT (* firstorder, higherorder, fullytyped *) 
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fullytyped version of metis
paulson
parents:
32530
diff
changeset

31 

32956  32 
(*  *) 
33 
(* Useful Theorems *) 

34 
(*  *) 

33689
d0a9ce721e0c
properly inlined @{lemma} antiqutations  might also reduce proof terms a bit;
wenzelm
parents:
33339
diff
changeset

35 
val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)} 
36945  36 
val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp} 
33689
d0a9ce721e0c
properly inlined @{lemma} antiqutations  might also reduce proof terms a bit;
wenzelm
parents:
33339
diff
changeset

37 
val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp} 
d0a9ce721e0c
properly inlined @{lemma} antiqutations  might also reduce proof terms a bit;
wenzelm
parents:
33339
diff
changeset

38 
val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp} 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

39 

32956  40 
(*  *) 
41 
(* Useful Functions *) 

42 
(*  *) 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

43 

37417
0714ece49081
A function called "untyped_aconv" shouldn't look at the bound names!
blanchet
parents:
37410
diff
changeset

44 
(* Match untyped terms. *) 
0714ece49081
A function called "untyped_aconv" shouldn't look at the bound names!
blanchet
parents:
37410
diff
changeset

45 
fun untyped_aconv (Const (a, _)) (Const(b, _)) = (a = b) 
0714ece49081
A function called "untyped_aconv" shouldn't look at the bound names!
blanchet
parents:
37410
diff
changeset

46 
 untyped_aconv (Free (a, _)) (Free (b, _)) = (a = b) 
0714ece49081
A function called "untyped_aconv" shouldn't look at the bound names!
blanchet
parents:
37410
diff
changeset

47 
 untyped_aconv (Var ((a, _), _)) (Var ((b, _), _)) = 
0714ece49081
A function called "untyped_aconv" shouldn't look at the bound names!
blanchet
parents:
37410
diff
changeset

48 
(a = b) (* The index is ignored, for some reason. *) 
0714ece49081
A function called "untyped_aconv" shouldn't look at the bound names!
blanchet
parents:
37410
diff
changeset

49 
 untyped_aconv (Bound i) (Bound j) = (i = j) 
0714ece49081
A function called "untyped_aconv" shouldn't look at the bound names!
blanchet
parents:
37410
diff
changeset

50 
 untyped_aconv (Abs (_, _, t)) (Abs (_, _, u)) = untyped_aconv t u 
0714ece49081
A function called "untyped_aconv" shouldn't look at the bound names!
blanchet
parents:
37410
diff
changeset

51 
 untyped_aconv (t1 $ t2) (u1 $ u2) = 
0714ece49081
A function called "untyped_aconv" shouldn't look at the bound names!
blanchet
parents:
37410
diff
changeset

52 
untyped_aconv t1 u1 andalso untyped_aconv t2 u2 
0714ece49081
A function called "untyped_aconv" shouldn't look at the bound names!
blanchet
parents:
37410
diff
changeset

53 
 untyped_aconv _ _ = false 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

54 

32956  55 
(* Finding the relative location of an untyped term within a list of terms *) 
56 
fun get_index lit = 

57 
let val lit = Envir.eta_contract lit 

37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset

58 
fun get _ [] = raise Empty 
32956  59 
 get n (x::xs) = if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x)) 
60 
then n else get (n+1) xs 

61 
in get 1 end; 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

62 

32956  63 
(*  *) 
64 
(* HOL to FOL (Isabelle to Metis) *) 

65 
(*  *) 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

66 

38614  67 
fun fn_isa_to_met_sublevel "equal" = "=" (* FIXME: "c_fequal" *) 
38606
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

68 
 fn_isa_to_met_sublevel x = x 
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

69 
fun fn_isa_to_met_toplevel "equal" = "=" 
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

70 
 fn_isa_to_met_toplevel x = x 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

71 

32956  72 
fun metis_lit b c args = (b, (c, args)); 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

73 

37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset

74 
fun metis_term_from_combtyp (CombTVar (s, _)) = Metis.Term.Var s 
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset

75 
 metis_term_from_combtyp (CombTFree (s, _)) = Metis.Term.Fn (s, []) 
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset

76 
 metis_term_from_combtyp (CombType ((s, _), tps)) = 
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset

77 
Metis.Term.Fn (s, map metis_term_from_combtyp tps); 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

78 

32956  79 
(*These two functions insert type literals before the real literals. That is the 
80 
opposite order from TPTP linkup, but maybe OK.*) 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

81 

32956  82 
fun hol_term_to_fol_FO tm = 
35865  83 
case strip_combterm_comb tm of 
36170
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset

84 
(CombConst ((c, _), _, tys), tms) => 
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset

85 
let val tyargs = map metis_term_from_combtyp tys 
32956  86 
val args = map hol_term_to_fol_FO tms 
87 
in Metis.Term.Fn (c, tyargs @ args) end 

36170
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset

88 
 (CombVar ((v, _), _), []) => Metis.Term.Var v 
38695
e85ce10cef1a
revert this idea of automatically invoking "metisFT" when "metis" fails;
blanchet
parents:
38652
diff
changeset

89 
 _ => raise Fail "nonfirstorder combterm" 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

90 

38099
e3bb96b83807
fix Meson's definition of firstorderness to prevent errors later on elsewhere (e.g. in Metis)
blanchet
parents:
38097
diff
changeset

91 
fun hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) = 
38606
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

92 
Metis.Term.Fn (fn_isa_to_met_sublevel a, map metis_term_from_combtyp tylist) 
38099
e3bb96b83807
fix Meson's definition of firstorderness to prevent errors later on elsewhere (e.g. in Metis)
blanchet
parents:
38097
diff
changeset

93 
 hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis.Term.Var s 
35865  94 
 hol_term_to_fol_HO (CombApp (tm1, tm2)) = 
32994  95 
Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]); 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

96 

32956  97 
(*The fullytyped translation, to avoid type errors*) 
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset

98 
fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, metis_term_from_combtyp ty]); 
32956  99 

36170
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset

100 
fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis.Term.Var s, ty) 
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset

101 
 hol_term_to_fol_FT (CombConst((a, _), ty, _)) = 
38606
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

102 
wrap_type (Metis.Term.Fn(fn_isa_to_met_sublevel a, []), ty) 
35865  103 
 hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) = 
32956  104 
wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]), 
37994
b04307085a09
make TPTP generator accept full firstorder formulas
blanchet
parents:
37992
diff
changeset

105 
combtyp_of tm) 
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fullytyped version of metis
paulson
parents:
32530
diff
changeset

106 

37923  107 
fun hol_literal_to_fol FO (FOLLiteral (pos, tm)) = 
36170
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset

108 
let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm 
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset

109 
val tylits = if p = "equal" then [] else map metis_term_from_combtyp tys 
32956  110 
val lits = map hol_term_to_fol_FO tms 
38606
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

111 
in metis_lit pos (fn_isa_to_met_toplevel p) (tylits @ lits) end 
37923  112 
 hol_literal_to_fol HO (FOLLiteral (pos, tm)) = 
35865  113 
(case strip_combterm_comb tm of 
36170
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset

114 
(CombConst(("equal", _), _, _), tms) => 
37923  115 
metis_lit pos "=" (map hol_term_to_fol_HO tms) 
116 
 _ => metis_lit pos "{}" [hol_term_to_fol_HO tm]) (*hBOOL*) 

117 
 hol_literal_to_fol FT (FOLLiteral (pos, tm)) = 

35865  118 
(case strip_combterm_comb tm of 
36170
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset

119 
(CombConst(("equal", _), _, _), tms) => 
37923  120 
metis_lit pos "=" (map hol_term_to_fol_FT tms) 
121 
 _ => metis_lit pos "{}" [hol_term_to_fol_FT tm]) (*hBOOL*); 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

122 

37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

123 
fun literals_of_hol_term thy mode t = 
35865  124 
let val (lits, types_sorts) = literals_of_term thy t 
32956  125 
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

126 

32956  127 
(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*) 
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset

128 
fun metis_of_type_literals pos (TyLitVar ((s, _), (s', _))) = 
36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36401
diff
changeset

129 
metis_lit pos s [Metis.Term.Var s'] 
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset

130 
 metis_of_type_literals pos (TyLitFree ((s, _), (s', _))) = 
36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36401
diff
changeset

131 
metis_lit pos s [Metis.Term.Fn (s',[])] 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

132 

32994  133 
fun default_sort _ (TVar _) = false 
33035  134 
 default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1))); 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

135 

32956  136 
fun metis_of_tfree tf = 
36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36401
diff
changeset

137 
Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_type_literals true tf)); 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

138 

37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

139 
fun hol_thm_to_fol is_conjecture ctxt mode j skolems th = 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

140 
let 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

141 
val thy = ProofContext.theory_of ctxt 
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

142 
val (skolems, (mlits, types_sorts)) = 
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

143 
th > prop_of > conceal_skolem_terms j skolems 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

144 
> (HOLogic.dest_Trueprop #> literals_of_hol_term thy mode) 
32956  145 
in 
146 
if is_conjecture then 

36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36401
diff
changeset

147 
(Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), 
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

148 
type_literals_for_types types_sorts, skolems) 
32956  149 
else 
36966
adc11fb3f3aa
generate proper arity declarations for TFrees for SPASS's DFG format;
blanchet
parents:
36945
diff
changeset

150 
let val tylits = filter_out (default_sort ctxt) types_sorts 
adc11fb3f3aa
generate proper arity declarations for TFrees for SPASS's DFG format;
blanchet
parents:
36945
diff
changeset

151 
> type_literals_for_types 
32956  152 
val mtylits = if Config.get ctxt type_lits 
36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36401
diff
changeset

153 
then map (metis_of_type_literals false) tylits else [] 
32956  154 
in 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

155 
(Metis.Thm.axiom (Metis.LiteralSet.fromList(mtylits @ mlits)), [], 
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

156 
skolems) 
32956  157 
end 
158 
end; 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

159 

32956  160 
(* ARITY CLAUSE *) 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

161 

37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset

162 
fun m_arity_cls (TConsLit ((c, _), (t, _), args)) = 
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset

163 
metis_lit true c [Metis.Term.Fn(t, map (Metis.Term.Var o fst) args)] 
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset

164 
 m_arity_cls (TVarLit ((c, _), (s, _))) = 
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset

165 
metis_lit false c [Metis.Term.Var s] 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

166 

32956  167 
(*TrueI is returned as the Isabelle counterpart because there isn't any.*) 
35865  168 
fun arity_cls (ArityClause {conclLit, premLits, ...}) = 
32956  169 
(TrueI, 
170 
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

171 

32956  172 
(* CLASSREL CLAUSE *) 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

173 

37925  174 
fun m_class_rel_cls (subclass, _) (superclass, _) = 
32956  175 
[metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]]; 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

176 

37925  177 
fun class_rel_cls (ClassRelClause {subclass, superclass, ...}) = 
178 
(TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_class_rel_cls subclass superclass))); 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

179 

32956  180 
(*  *) 
181 
(* FOL to HOL (Metis to Isabelle) *) 

182 
(*  *) 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

183 

32956  184 
datatype term_or_type = Term of Term.term  Type of Term.typ; 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

185 

32956  186 
fun terms_of [] = [] 
187 
 terms_of (Term t :: tts) = t :: terms_of tts 

188 
 terms_of (Type _ :: tts) = terms_of tts; 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

189 

32956  190 
fun types_of [] = [] 
32994  191 
 types_of (Term (Term.Var ((a,idx), _)) :: tts) = 
32956  192 
if String.isPrefix "_" a then 
193 
(*Variable generated by Metis, which might have been a type variable.*) 

32994  194 
TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts 
32956  195 
else types_of tts 
196 
 types_of (Term _ :: tts) = types_of tts 

197 
 types_of (Type T :: tts) = T :: types_of tts; 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

198 

32956  199 
fun apply_list rator nargs rands = 
200 
let val trands = terms_of rands 

201 
in if length trands = nargs then Term (list_comb(rator, trands)) 

37402
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

202 
else raise Fail 
32956  203 
("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^ 
204 
" expected " ^ Int.toString nargs ^ 

205 
" received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands)) 

206 
end; 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

207 

24500  208 
fun infer_types ctxt = 
209 
Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt); 

25713  210 

32956  211 
(*We use 1 rather than 0 because variable references in clauses may otherwise conflict 
212 
with variable constraints in the goal...at least, type inference often fails otherwise. 

213 
SEE ALSO axiom_inf below.*) 

214 
fun mk_var (w,T) = Term.Var((w,1), T); 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

215 

32956  216 
(*include the default sort, if available*) 
217 
fun mk_tfree ctxt w = 

218 
let val ww = "'" ^ w 

33035  219 
in TFree(ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1))) end; 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

220 

32956  221 
(*Remove the "apply" operator from an HO term*) 
222 
fun strip_happ args (Metis.Term.Fn(".",[t,u])) = strip_happ (u::args) t 

223 
 strip_happ args x = (x, args); 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

224 

36967
3c804030474b
fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably
blanchet
parents:
36966
diff
changeset

225 
fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS) 
3c804030474b
fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably
blanchet
parents:
36966
diff
changeset

226 

38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38748
diff
changeset

227 
fun smart_invert_const "fequal" = @{const_name HOL.eq} 
38606
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

228 
 smart_invert_const s = invert_const s 
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

229 

37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset

230 
fun hol_type_from_metis_term _ (Metis.Term.Var v) = 
38748  231 
(case strip_prefix_and_unascii tvar_prefix v of 
35865  232 
SOME w => make_tvar w 
233 
 NONE => make_tvar v) 

37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset

234 
 hol_type_from_metis_term ctxt (Metis.Term.Fn(x, tys)) = 
38748  235 
(case strip_prefix_and_unascii type_const_prefix x of 
38606
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

236 
SOME tc => Term.Type (smart_invert_const tc, 
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset

237 
map (hol_type_from_metis_term ctxt) tys) 
32956  238 
 NONE => 
38748  239 
case strip_prefix_and_unascii tfree_prefix x of 
32956  240 
SOME tf => mk_tfree ctxt tf 
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset

241 
 NONE => raise Fail ("hol_type_from_metis_term: " ^ x)); 
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fullytyped version of metis
paulson
parents:
32530
diff
changeset

242 

32956  243 
(*Maps metis terms to isabelle terms*) 
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset

244 
fun hol_term_from_metis_PT ctxt fol_tm = 
32956  245 
let val thy = ProofContext.theory_of ctxt 
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset

246 
val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^ 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

247 
Metis.Term.toString fol_tm) 
32956  248 
fun tm_to_tt (Metis.Term.Var v) = 
38748  249 
(case strip_prefix_and_unascii tvar_prefix v of 
35865  250 
SOME w => Type (make_tvar w) 
32956  251 
 NONE => 
38748  252 
case strip_prefix_and_unascii schematic_var_prefix v of 
32956  253 
SOME w => Term (mk_var (w, HOLogic.typeT)) 
254 
 NONE => Term (mk_var (v, HOLogic.typeT)) ) 

255 
(*Var from Metis with a name like _nnn; possibly a type variable*) 

256 
 tm_to_tt (Metis.Term.Fn ("{}", [arg])) = tm_to_tt arg (*hBOOL*) 

257 
 tm_to_tt (t as Metis.Term.Fn (".",_)) = 

258 
let val (rator,rands) = strip_happ [] t 

259 
in case rator of 

260 
Metis.Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands) 

261 
 _ => case tm_to_tt rator of 

262 
Term t => Term (list_comb(t, terms_of (map tm_to_tt rands))) 

37402
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

263 
 _ => raise Fail "tm_to_tt: HO application" 
32956  264 
end 
265 
 tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args) 

266 
and applic_to_tt ("=",ts) = 

38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38748
diff
changeset

267 
Term (list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), terms_of (map tm_to_tt ts))) 
32956  268 
 applic_to_tt (a,ts) = 
38748  269 
case strip_prefix_and_unascii const_prefix a of 
32956  270 
SOME b => 
38606
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

271 
let val c = smart_invert_const b 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36556
diff
changeset

272 
val ntypes = num_type_args thy c 
32956  273 
val nterms = length ts  ntypes 
274 
val tts = map tm_to_tt ts 

275 
val tys = types_of (List.take(tts,ntypes)) 

36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36556
diff
changeset

276 
in if length tys = ntypes then 
32956  277 
apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes)) 
37402
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

278 
else 
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

279 
raise Fail ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^ 
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

280 
" but gets " ^ Int.toString (length tys) ^ 
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

281 
" type arguments\n" ^ 
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

282 
cat_lines (map (Syntax.string_of_typ ctxt) tys) ^ 
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

283 
" the terms are \n" ^ 
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

284 
cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts))) 
32956  285 
end 
286 
 NONE => (*Not a constant. Is it a type constructor?*) 

38748  287 
case strip_prefix_and_unascii type_const_prefix a of 
33227  288 
SOME b => 
38606
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

289 
Type (Term.Type (smart_invert_const b, types_of (map tm_to_tt ts))) 
32956  290 
 NONE => (*Maybe a TFree. Should then check that ts=[].*) 
38748  291 
case strip_prefix_and_unascii tfree_prefix a of 
32956  292 
SOME b => Type (mk_tfree ctxt b) 
293 
 NONE => (*a fixed variable? They are Skolem functions.*) 

38748  294 
case strip_prefix_and_unascii fixed_var_prefix a of 
32956  295 
SOME b => 
296 
let val opr = Term.Free(b, HOLogic.typeT) 

297 
in apply_list opr (length ts) (map tm_to_tt ts) end 

37402
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

298 
 NONE => raise Fail ("unexpected metis function: " ^ a) 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

299 
in 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

300 
case tm_to_tt fol_tm of 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

301 
Term t => t 
37402
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

302 
 _ => raise Fail "fol_tm_to_tt: Term expected" 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

303 
end 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

304 

32956  305 
(*Maps fullytyped metis terms to isabelle terms*) 
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset

306 
fun hol_term_from_metis_FT ctxt fol_tm = 
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset

307 
let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^ 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

308 
Metis.Term.toString fol_tm) 
32994  309 
fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) = 
38748  310 
(case strip_prefix_and_unascii schematic_var_prefix v of 
32956  311 
SOME w => mk_var(w, dummyT) 
312 
 NONE => mk_var(v, dummyT)) 

32994  313 
 cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) = 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38748
diff
changeset

314 
Const (@{const_name HOL.eq}, HOLogic.typeT) 
32956  315 
 cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) = 
38748  316 
(case strip_prefix_and_unascii const_prefix x of 
38606
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

317 
SOME c => Const (smart_invert_const c, dummyT) 
32956  318 
 NONE => (*Not a constant. Is it a fixed variable??*) 
38748  319 
case strip_prefix_and_unascii fixed_var_prefix x of 
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset

320 
SOME v => Free (v, hol_type_from_metis_term ctxt ty) 
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset

321 
 NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x)) 
32956  322 
 cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) = 
323 
cvt tm1 $ cvt tm2 

324 
 cvt (Metis.Term.Fn (".",[tm1,tm2])) = (*untyped application*) 

325 
cvt tm1 $ cvt tm2 

326 
 cvt (Metis.Term.Fn ("{}", [arg])) = cvt arg (*hBOOL*) 

327 
 cvt (Metis.Term.Fn ("=", [tm1,tm2])) = 

38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38748
diff
changeset

328 
list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), map cvt [tm1,tm2]) 
32956  329 
 cvt (t as Metis.Term.Fn (x, [])) = 
38748  330 
(case strip_prefix_and_unascii const_prefix x of 
38606
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

331 
SOME c => Const (smart_invert_const c, dummyT) 
32956  332 
 NONE => (*Not a constant. Is it a fixed variable??*) 
38748  333 
case strip_prefix_and_unascii fixed_var_prefix x of 
32956  334 
SOME v => Free (v, dummyT) 
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset

335 
 NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x); 
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset

336 
hol_term_from_metis_PT ctxt t)) 
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset

337 
 cvt t = (trace_msg (fn () => "hol_term_from_metis_FT bad term: " ^ Metis.Term.toString t); 
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset

338 
hol_term_from_metis_PT ctxt t) 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

339 
in fol_tm > cvt end 
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fullytyped version of metis
paulson
parents:
32530
diff
changeset

340 

37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset

341 
fun hol_term_from_metis FT = hol_term_from_metis_FT 
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset

342 
 hol_term_from_metis _ = hol_term_from_metis_PT 
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fullytyped version of metis
paulson
parents:
32530
diff
changeset

343 

37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

344 
fun hol_terms_from_fol ctxt mode skolems fol_tms = 
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset

345 
let val ts = map (hol_term_from_metis mode ctxt) fol_tms 
32956  346 
val _ = trace_msg (fn () => " calling type inference:") 
347 
val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts 

37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

348 
val ts' = ts > map (reveal_skolem_terms skolems) > infer_types ctxt 
32956  349 
val _ = app (fn t => trace_msg 
350 
(fn () => " final term: " ^ Syntax.string_of_term ctxt t ^ 

351 
" of type " ^ Syntax.string_of_typ ctxt (type_of t))) 

352 
ts' 

353 
in ts' end; 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

354 

35865  355 
fun mk_not (Const (@{const_name Not}, _) $ b) = b 
32956  356 
 mk_not b = HOLogic.mk_not b; 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

357 

32956  358 
val metis_eq = Metis.Term.Fn ("=", []); 
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fullytyped version of metis
paulson
parents:
32530
diff
changeset

359 

32956  360 
(*  *) 
361 
(* FOL step Inference Rules *) 

362 
(*  *) 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

363 

32956  364 
(*for debugging only*) 
365 
fun print_thpair (fth,th) = 

366 
(trace_msg (fn () => "============================================="); 

367 
trace_msg (fn () => "Metis: " ^ Metis.Thm.toString fth); 

368 
trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th)); 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

369 

32956  370 
fun lookth thpairs (fth : Metis.Thm.thm) = 
33035  371 
the (AList.lookup (uncurry Metis.Thm.equal) thpairs fth) 
37402
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

372 
handle Option => 
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

373 
raise Fail ("Failed to find a Metis theorem " ^ Metis.Thm.toString fth); 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

374 

32956  375 
fun is_TrueI th = Thm.eq_thm(TrueI,th); 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

376 

32956  377 
fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx)); 
24974  378 

32956  379 
fun inst_excluded_middle thy i_atm = 
380 
let val th = EXCLUDED_MIDDLE 

381 
val [vx] = Term.add_vars (prop_of th) [] 

382 
val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)] 

383 
in cterm_instantiate substs th end; 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

384 

32956  385 
(* INFERENCE RULE: AXIOM *) 
36945  386 
fun axiom_inf thpairs th = Thm.incr_indexes 1 (lookth thpairs th); 
32956  387 
(*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*) 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

388 

32956  389 
(* INFERENCE RULE: ASSUME *) 
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

390 
fun assume_inf ctxt mode skolems atm = 
32956  391 
inst_excluded_middle 
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

392 
(ProofContext.theory_of ctxt) 
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

393 
(singleton (hol_terms_from_fol ctxt mode skolems) (Metis.Term.Fn atm)) 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

394 

32956  395 
(* INFERENCE RULE: INSTANTIATE (Subst). Type instantiations are ignored. Trying to reconstruct 
396 
them admits new possibilities of errors, e.g. concerning sorts. Instead we try to arrange 

397 
that new TVars are distinct and that types can be inferred from terms.*) 

37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

398 
fun inst_inf ctxt mode skolems thpairs fsubst th = 
32956  399 
let val thy = ProofContext.theory_of ctxt 
400 
val i_th = lookth thpairs th 

401 
val i_th_vars = Term.add_vars (prop_of i_th) [] 

33035  402 
fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars) 
32956  403 
fun subst_translation (x,y) = 
404 
let val v = find_var x 

37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

405 
(* We call "reveal_skolem_terms" and "infer_types" below. *) 
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset

406 
val t = hol_term_from_metis mode ctxt y 
32956  407 
in SOME (cterm_of thy (Var v), t) end 
408 
handle Option => 

409 
(trace_msg (fn() => "List.find failed for the variable " ^ x ^ 

410 
" in " ^ Display.string_of_thm ctxt i_th); 

411 
NONE) 

412 
fun remove_typeinst (a, t) = 

38748  413 
case strip_prefix_and_unascii schematic_var_prefix a of 
32956  414 
SOME b => SOME (b, t) 
38748  415 
 NONE => case strip_prefix_and_unascii tvar_prefix a of 
32956  416 
SOME _ => NONE (*type instantiations are forbidden!*) 
38748  417 
 NONE => SOME (a,t) (*internal Metis var?*) 
32956  418 
val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th) 
419 
val substs = map_filter remove_typeinst (Metis.Subst.toList fsubst) 

420 
val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs) 

37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

421 
val tms = rawtms > map (reveal_skolem_terms skolems) > infer_types ctxt 
32956  422 
val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th) 
423 
val substs' = ListPair.zip (vars, map ctm_of tms) 

424 
val _ = trace_msg (fn () => 

425 
cat_lines ("subst_translations:" :: 

426 
(substs' > map (fn (x, y) => 

427 
Syntax.string_of_term ctxt (term_of x) ^ " > " ^ 

428 
Syntax.string_of_term ctxt (term_of y))))); 

37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

429 
in cterm_instantiate substs' i_th end 
38695
e85ce10cef1a
revert this idea of automatically invoking "metisFT" when "metis" fails;
blanchet
parents:
38652
diff
changeset

430 
handle THM (msg, _, _) => 
e85ce10cef1a
revert this idea of automatically invoking "metisFT" when "metis" fails;
blanchet
parents:
38652
diff
changeset

431 
error ("Cannot replay Metis proof in Isabelle:\n" ^ msg) 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

432 

32956  433 
(* INFERENCE RULE: RESOLVE *) 
25713  434 

32956  435 
(*Like RSN, but we rename apart only the type variables. Vars here typically have an index 
436 
of 1, and the use of RSN would increase this typically to 3. Instantiations of those Vars 

437 
could then fail. See comment on mk_var.*) 

438 
fun resolve_inc_tyvars(tha,i,thb) = 

37548
6a7a9261b9ad
make sure "metisFT" is tried upon "metis" failure in "resolve_inc_tyvars"
blanchet
parents:
37538
diff
changeset

439 
let 
6a7a9261b9ad
make sure "metisFT" is tried upon "metis" failure in "resolve_inc_tyvars"
blanchet
parents:
37538
diff
changeset

440 
val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha 
32956  441 
val ths = Seq.list_of (Thm.bicompose false (false,tha,nprems_of tha) i thb) 
442 
in 

443 
case distinct Thm.eq_thm ths of 

444 
[th] => th 

445 
 _ => raise THM ("resolve_inc_tyvars: unique result expected", i, [tha,thb]) 

37548
6a7a9261b9ad
make sure "metisFT" is tried upon "metis" failure in "resolve_inc_tyvars"
blanchet
parents:
37538
diff
changeset

446 
end 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

447 

37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

448 
fun resolve_inf ctxt mode skolems thpairs atm th1 th2 = 
32956  449 
let 
450 
val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2 

451 
val _ = trace_msg (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1) 

452 
val _ = trace_msg (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2) 

453 
in 

454 
if is_TrueI i_th1 then i_th2 (*Trivial cases where one operand is type info*) 

455 
else if is_TrueI i_th2 then i_th1 

456 
else 

457 
let 

37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

458 
val i_atm = singleton (hol_terms_from_fol ctxt mode skolems) 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

459 
(Metis.Term.Fn atm) 
32956  460 
val _ = trace_msg (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm) 
461 
val prems_th1 = prems_of i_th1 

462 
val prems_th2 = prems_of i_th2 

463 
val index_th1 = get_index (mk_not i_atm) prems_th1 

37402
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

464 
handle Empty => raise Fail "Failed to find literal in th1" 
32956  465 
val _ = trace_msg (fn () => " index_th1: " ^ Int.toString index_th1) 
466 
val index_th2 = get_index i_atm prems_th2 

37402
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

467 
handle Empty => raise Fail "Failed to find literal in th2" 
32956  468 
val _ = trace_msg (fn () => " index_th2: " ^ Int.toString index_th2) 
469 
in resolve_inc_tyvars (Meson.select_literal index_th1 i_th1, index_th2, i_th2) end 

470 
end; 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

471 

32956  472 
(* INFERENCE RULE: REFL *) 
473 
val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) []))); 

474 
val refl_idx = 1 + Thm.maxidx_of REFL_THM; 

25713  475 

37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

476 
fun refl_inf ctxt mode skolems t = 
32956  477 
let val thy = ProofContext.theory_of ctxt 
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

478 
val i_t = singleton (hol_terms_from_fol ctxt mode skolems) t 
32956  479 
val _ = trace_msg (fn () => " term: " ^ Syntax.string_of_term ctxt i_t) 
480 
val c_t = cterm_incr_types thy refl_idx i_t 

481 
in cterm_instantiate [(refl_x, c_t)] REFL_THM end; 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

482 

38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38748
diff
changeset

483 
fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0 (*equality has no type arguments*) 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36556
diff
changeset

484 
 get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0) 
32994  485 
 get_ty_arg_size _ _ = 0; 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

486 

32956  487 
(* INFERENCE RULE: EQUALITY *) 
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

488 
fun equality_inf ctxt mode skolems (pos, atm) fp fr = 
32956  489 
let val thy = ProofContext.theory_of ctxt 
490 
val m_tm = Metis.Term.Fn atm 

37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

491 
val [i_atm,i_tm] = hol_terms_from_fol ctxt mode skolems [m_tm, fr] 
32956  492 
val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos) 
32994  493 
fun replace_item_list lx 0 (_::ls) = lx::ls 
32956  494 
 replace_item_list lx i (l::ls) = l :: replace_item_list lx (i1) ls 
495 
fun path_finder_FO tm [] = (tm, Term.Bound 0) 

496 
 path_finder_FO tm (p::ps) = 

35865  497 
let val (tm1,args) = strip_comb tm 
32956  498 
val adjustment = get_ty_arg_size thy tm1 
499 
val p' = if adjustment > p then p else padjustment 

500 
val tm_p = List.nth(args,p') 

38695
e85ce10cef1a
revert this idea of automatically invoking "metisFT" when "metis" fails;
blanchet
parents:
38652
diff
changeset

501 
handle Subscript => 
e85ce10cef1a
revert this idea of automatically invoking "metisFT" when "metis" fails;
blanchet
parents:
38652
diff
changeset

502 
error ("Cannot replay Metis proof in Isabelle:\n" ^ 
e85ce10cef1a
revert this idea of automatically invoking "metisFT" when "metis" fails;
blanchet
parents:
38652
diff
changeset

503 
"equality_inf: " ^ Int.toString p ^ " adj " ^ 
e85ce10cef1a
revert this idea of automatically invoking "metisFT" when "metis" fails;
blanchet
parents:
38652
diff
changeset

504 
Int.toString adjustment ^ " term " ^ 
e85ce10cef1a
revert this idea of automatically invoking "metisFT" when "metis" fails;
blanchet
parents:
38652
diff
changeset

505 
Syntax.string_of_term ctxt tm) 
32956  506 
val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^ 
507 
" " ^ Syntax.string_of_term ctxt tm_p) 

508 
val (r,t) = path_finder_FO tm_p ps 

509 
in 

510 
(r, list_comb (tm1, replace_item_list t p' args)) 

511 
end 

512 
fun path_finder_HO tm [] = (tm, Term.Bound 0) 

513 
 path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps) 

32994  514 
 path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps) 
37402
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

515 
 path_finder_HO tm ps = 
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

516 
raise Fail ("equality_inf, path_finder_HO: path = " ^ 
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

517 
space_implode " " (map Int.toString ps) ^ 
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

518 
" isaterm: " ^ Syntax.string_of_term ctxt tm) 
32956  519 
fun path_finder_FT tm [] _ = (tm, Term.Bound 0) 
32994  520 
 path_finder_FT tm (0::ps) (Metis.Term.Fn ("ti", [t1, _])) = 
32956  521 
path_finder_FT tm ps t1 
32994  522 
 path_finder_FT (t$u) (0::ps) (Metis.Term.Fn (".", [t1, _])) = 
32956  523 
(fn(x,y) => (x, y$u)) (path_finder_FT t ps t1) 
32994  524 
 path_finder_FT (t$u) (1::ps) (Metis.Term.Fn (".", [_, t2])) = 
32956  525 
(fn(x,y) => (x, t$y)) (path_finder_FT u ps t2) 
37402
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

526 
 path_finder_FT tm ps t = 
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

527 
raise Fail ("equality_inf, path_finder_FT: path = " ^ 
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

528 
space_implode " " (map Int.toString ps) ^ 
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

529 
" isaterm: " ^ Syntax.string_of_term ctxt tm ^ 
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

530 
" folterm: " ^ Metis.Term.toString t) 
32956  531 
fun path_finder FO tm ps _ = path_finder_FO tm ps 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38748
diff
changeset

532 
 path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (p::ps) _ = 
32956  533 
(*equality: not curried, as other predicates are*) 
534 
if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*) 

535 
else path_finder_HO tm (p::ps) (*1 selects second operand*) 

32994  536 
 path_finder HO tm (_ :: ps) (Metis.Term.Fn ("{}", [_])) = 
32956  537 
path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*) 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38748
diff
changeset

538 
 path_finder FT (tm as Const(@{const_name HOL.eq}, _) $ _ $ _) (p::ps) 
32956  539 
(Metis.Term.Fn ("=", [t1,t2])) = 
540 
(*equality: not curried, as other predicates are*) 

541 
if p=0 then path_finder_FT tm (0::1::ps) 

542 
(Metis.Term.Fn (".", [Metis.Term.Fn (".", [metis_eq,t1]), t2])) 

543 
(*select first operand*) 

544 
else path_finder_FT tm (p::ps) 

545 
(Metis.Term.Fn (".", [metis_eq,t2])) 

546 
(*1 selects second operand*) 

32994  547 
 path_finder FT tm (_ :: ps) (Metis.Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1 
32956  548 
(*if not equality, ignore head to skip the hBOOL predicate*) 
549 
 path_finder FT tm ps t = path_finder_FT tm ps t (*really an error case!*) 

35865  550 
fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx = 
32956  551 
let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm 
552 
in (tm, nt $ tm_rslt) end 

553 
 path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm 

554 
val (tm_subst, body) = path_finder_lit i_atm fp 

555 
val tm_abs = Term.Abs("x", Term.type_of tm_subst, body) 

556 
val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs) 

557 
val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm) 

558 
val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst) 

559 
val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill typed but gives right max*) 

36945  560 
val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em) 
32956  561 
val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst') 
562 
val eq_terms = map (pairself (cterm_of thy)) 

33227  563 
(ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm])) 
32956  564 
in cterm_instantiate eq_terms subst' end; 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

565 

32956  566 
val factor = Seq.hd o distinct_subgoals_tac; 
28528
0cf2749e8ef7
The result of the equality inference rule no longer undergoes factoring.
paulson
parents:
28262
diff
changeset

567 

37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

568 
fun step ctxt mode skolems thpairs p = 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

569 
case p of 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

570 
(fol_th, Metis.Proof.Axiom _) => factor (axiom_inf thpairs fol_th) 
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

571 
 (_, Metis.Proof.Assume f_atm) => assume_inf ctxt mode skolems f_atm 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

572 
 (_, Metis.Proof.Subst (f_subst, f_th1)) => 
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

573 
factor (inst_inf ctxt mode skolems thpairs f_subst f_th1) 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

574 
 (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2)) => 
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

575 
factor (resolve_inf ctxt mode skolems thpairs f_atm f_th1 f_th2) 
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

576 
 (_, Metis.Proof.Refl f_tm) => refl_inf ctxt mode skolems f_tm 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

577 
 (_, Metis.Proof.Equality (f_lit, f_p, f_r)) => 
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

578 
equality_inf ctxt mode skolems f_lit f_p f_r 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

579 

35865  580 
fun real_literal (_, (c, _)) = not (String.isPrefix class_prefix c); 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

581 

38280  582 
fun translate_one ctxt mode skolems (fol_th, inf) thpairs = 
583 
let 

584 
val _ = trace_msg (fn () => "=============================================") 

585 
val _ = trace_msg (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th) 

586 
val _ = trace_msg (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf) 

587 
val th = Meson.flexflex_first_order (step ctxt mode skolems 

588 
thpairs (fol_th, inf)) 

589 
val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th) 

590 
val _ = trace_msg (fn () => "=============================================") 

591 
val n_metis_lits = 

592 
length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th))) 

38695
e85ce10cef1a
revert this idea of automatically invoking "metisFT" when "metis" fails;
blanchet
parents:
38652
diff
changeset

593 
val _ = if nprems_of th = n_metis_lits then () 
e85ce10cef1a
revert this idea of automatically invoking "metisFT" when "metis" fails;
blanchet
parents:
38652
diff
changeset

594 
else error "Cannot replay Metis proof in Isabelle." 
38280  595 
in (fol_th, th) :: thpairs end 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

596 

32956  597 
(*Determining which axiom clauses are actually used*) 
598 
fun used_axioms axioms (th, Metis.Proof.Axiom _) = SOME (lookth axioms th) 

32994  599 
 used_axioms _ _ = NONE; 
24855  600 

32956  601 
(*  *) 
602 
(* Translation of HO Clauses *) 

603 
(*  *) 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

604 

32956  605 
fun type_ext thy tms = 
35865  606 
let val subs = tfree_classes_of_terms tms 
607 
val supers = tvar_classes_of_terms tms 

608 
and tycons = type_consts_of_terms thy tms 

609 
val (supers', arity_clauses) = make_arity_clauses thy tycons supers 

37925  610 
val class_rel_clauses = make_class_rel_clauses thy subs supers' 
611 
in map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses 

32956  612 
end; 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

613 

32956  614 
(*  *) 
615 
(* Logic maps manage the interface between HOL and firstorder logic. *) 

616 
(*  *) 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

617 

32956  618 
type logic_map = 
35865  619 
{axioms: (Metis.Thm.thm * thm) list, 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

620 
tfrees: type_literal list, 
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

621 
skolems: (string * term) list} 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

622 

32994  623 
fun const_in_metis c (pred, tm_list) = 
32956  624 
let 
32994  625 
fun in_mterm (Metis.Term.Var _) = false 
32956  626 
 in_mterm (Metis.Term.Fn (".", tm_list)) = exists in_mterm tm_list 
627 
 in_mterm (Metis.Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list 

32994  628 
in c = pred orelse exists in_mterm tm_list end; 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

629 

32956  630 
(*Extract TFree constraints from context to include as conjecture clauses*) 
631 
fun init_tfrees ctxt = 

36966
adc11fb3f3aa
generate proper arity declarations for TFrees for SPASS's DFG format;
blanchet
parents:
36945
diff
changeset

632 
let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts in 
adc11fb3f3aa
generate proper arity declarations for TFrees for SPASS's DFG format;
blanchet
parents:
36945
diff
changeset

633 
Vartab.fold add (#2 (Variable.constraints_of ctxt)) [] 
adc11fb3f3aa
generate proper arity declarations for TFrees for SPASS's DFG format;
blanchet
parents:
36945
diff
changeset

634 
> type_literals_for_types 
36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36401
diff
changeset

635 
end; 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

636 

32956  637 
(*transform isabelle type / arity clause to metis clause *) 
638 
fun add_type_thm [] lmap = lmap 

37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

639 
 add_type_thm ((ith, mth) :: cls) {axioms, tfrees, skolems} = 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

640 
add_type_thm cls {axioms = (mth, ith) :: axioms, tfrees = tfrees, 
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

641 
skolems = skolems} 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

642 

32956  643 
(*Insert nonlogical axioms corresponding to all accumulated TFrees*) 
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

644 
fun add_tfrees {axioms, tfrees, skolems} : logic_map = 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

645 
{axioms = map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @ 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

646 
axioms, 
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

647 
tfrees = tfrees, skolems = skolems} 
25713  648 

32956  649 
fun string_of_mode FO = "FO" 
650 
 string_of_mode HO = "HO" 

651 
 string_of_mode FT = "FT" 

32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fullytyped version of metis
paulson
parents:
32530
diff
changeset

652 

37479
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37417
diff
changeset

653 
val helpers = 
38606
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

654 
[("c_COMBI", (false, map (`I) @{thms COMBI_def})), 
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

655 
("c_COMBK", (false, map (`I) @{thms COMBK_def})), 
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

656 
("c_COMBB", (false, map (`I) @{thms COMBB_def})), 
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

657 
("c_COMBC", (false, map (`I) @{thms COMBC_def})), 
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

658 
("c_COMBS", (false, map (`I) @{thms COMBS_def})), 
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

659 
("c_fequal", (false, map (rpair @{thm equal_imp_equal}) 
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

660 
@{thms fequal_imp_equal equal_imp_fequal})), 
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

661 
("c_True", (true, map (`I) @{thms True_or_False})), 
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

662 
("c_False", (true, map (`I) @{thms True_or_False})), 
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

663 
("c_If", (true, map (`I) @{thms if_True if_False True_or_False}))] 
37479
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37417
diff
changeset

664 

38100
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38099
diff
changeset

665 
fun is_quasi_fol_clause thy = 
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

666 
Meson.is_fol_term thy o snd o conceal_skolem_terms ~1 [] o prop_of 
37623
295f3a9b44b6
move functions not needed by Metis out of "Metis_Clauses"
blanchet
parents:
37619
diff
changeset

667 

32956  668 
(* Function to generate metis clauses, including comb and type clauses *) 
669 
fun build_map mode0 ctxt cls ths = 

670 
let val thy = ProofContext.theory_of ctxt 

671 
(*The modes FO and FT are sticky. HO can be downgraded to FO.*) 

672 
fun set_mode FO = FO 

37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

673 
 set_mode HO = 
37623
295f3a9b44b6
move functions not needed by Metis out of "Metis_Clauses"
blanchet
parents:
37619
diff
changeset

674 
if forall (is_quasi_fol_clause thy) (cls @ ths) then FO else HO 
32956  675 
 set_mode FT = FT 
676 
val mode = set_mode mode0 

677 
(*transform isabelle clause to metis clause *) 

38606
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

678 
fun add_thm is_conjecture (metis_ith, isa_ith) {axioms, tfrees, skolems} 
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

679 
: logic_map = 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

680 
let 
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

681 
val (mth, tfree_lits, skolems) = 
38606
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

682 
hol_thm_to_fol is_conjecture ctxt mode (length axioms) skolems 
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

683 
metis_ith 
32956  684 
in 
38606
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

685 
{axioms = (mth, Meson.make_meta_clause isa_ith) :: axioms, 
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

686 
tfrees = union (op =) tfree_lits tfrees, skolems = skolems} 
32956  687 
end; 
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

688 
val lmap = {axioms = [], tfrees = init_tfrees ctxt, skolems = []} 
38606
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

689 
> fold (add_thm true o `I) cls 
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset

690 
> add_tfrees 
38606
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

691 
> fold (add_thm false o `I) ths 
32956  692 
val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap) 
37479
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37417
diff
changeset

693 
fun is_used c = 
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37417
diff
changeset

694 
exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

695 
val lmap = 
37479
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37417
diff
changeset

696 
if mode = FO then 
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37417
diff
changeset

697 
lmap 
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37417
diff
changeset

698 
else 
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37417
diff
changeset

699 
let 
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37417
diff
changeset

700 
val helper_ths = 
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37417
diff
changeset

701 
helpers > filter (is_used o fst) 
38606
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

702 
> maps (fn (c, (needs_full_types, thms)) => 
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

703 
if not (is_used c) orelse 
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

704 
needs_full_types andalso mode <> FT then 
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

705 
[] 
37479
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37417
diff
changeset

706 
else 
38606
3003ddbd46d9
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer  otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents:
38433
diff
changeset

707 
thms) 
37479
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37417
diff
changeset

708 
in lmap > fold (add_thm false) helper_ths end 
37410
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37402
diff
changeset

709 
in (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap) end 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

710 

32956  711 
fun refute cls = 
712 
Metis.Resolution.loop (Metis.Resolution.new Metis.Resolution.default cls); 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

713 

32956  714 
fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const); 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

715 

32956  716 
fun common_thm ths1 ths2 = exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2); 
24855  717 

37573  718 

37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

719 
(* Main function to start Metis proof and reconstruction *) 
32956  720 
fun FOL_SOLVE mode ctxt cls ths0 = 
721 
let val thy = ProofContext.theory_of ctxt 

35826  722 
val th_cls_pairs = 
38016  723 
map (fn th => (Thm.get_name_hint th, Clausifier.cnf_axiom thy th)) ths0 
32956  724 
val ths = maps #2 th_cls_pairs 
725 
val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") 

726 
val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls 

727 
val _ = trace_msg (fn () => "THEOREM CLAUSES") 

728 
val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) ths 

37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

729 
val (mode, {axioms, tfrees, skolems}) = build_map mode ctxt cls ths 
32956  730 
val _ = if null tfrees then () 
731 
else (trace_msg (fn () => "TFREE CLAUSES"); 

37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset

732 
app (fn TyLitFree ((s, _), (s', _)) => 
37573  733 
trace_msg (fn _ => s ^ "(" ^ s' ^ ")")) tfrees) 
32956  734 
val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS") 
735 
val thms = map #1 axioms 

736 
val _ = app (fn th => trace_msg (fn () => Metis.Thm.toString th)) thms 

737 
val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode) 

738 
val _ = trace_msg (fn () => "START METIS PROVE PROCESS") 

739 
in 

33317  740 
case filter (is_false o prop_of) cls of 
32956  741 
false_th::_ => [false_th RS @{thm FalseE}] 
742 
 [] => 

743 
case refute thms of 

744 
Metis.Resolution.Contradiction mth => 

745 
let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^ 

746 
Metis.Thm.toString mth) 

747 
val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt 

748 
(*add constraints arising from converting goal to clause form*) 

749 
val proof = Metis.Proof.proof mth 

38280  750 
val result = fold (translate_one ctxt' mode skolems) proof axioms 
32956  751 
and used = map_filter (used_axioms axioms) proof 
752 
val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:") 

753 
val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used 

33305  754 
val unused = th_cls_pairs > map_filter (fn (name, cls) => 
755 
if common_thm used cls then NONE else SOME name) 

32956  756 
in 
36383  757 
if not (null cls) andalso not (common_thm used cls) then 
758 
warning "Metis: The assumptions are inconsistent." 

759 
else 

760 
(); 

761 
if not (null unused) then 

36230
43d10a494c91
added warning about inconsistent context to Metis;
blanchet
parents:
36170
diff
changeset

762 
warning ("Metis: Unused theorems: " ^ commas_quote unused 
43d10a494c91
added warning about inconsistent context to Metis;
blanchet
parents:
36170
diff
changeset

763 
^ ".") 
43d10a494c91
added warning about inconsistent context to Metis;
blanchet
parents:
36170
diff
changeset

764 
else 
43d10a494c91
added warning about inconsistent context to Metis;
blanchet
parents:
36170
diff
changeset

765 
(); 
32956  766 
case result of 
767 
(_,ith)::_ => 

36230
43d10a494c91
added warning about inconsistent context to Metis;
blanchet
parents:
36170
diff
changeset

768 
(trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith); 
32956  769 
[ith]) 
38097
5e4ad2df09f3
revert exception throwing in FOL_SOLVE, since they're not caught anyway
blanchet
parents:
38028
diff
changeset

770 
 _ => (trace_msg (fn () => "Metis: No result"); []) 
32956  771 
end 
772 
 Metis.Resolution.Satisfiable _ => 

773 
(trace_msg (fn () => "Metis: No firstorder proof with the lemmas supplied"); 

38097
5e4ad2df09f3
revert exception throwing in FOL_SOLVE, since they're not caught anyway
blanchet
parents:
38028
diff
changeset

774 
[]) 
32956  775 
end; 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

776 

38632
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

777 
(* Extensionalize "th", because that makes sense and that's what Sledgehammer 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

778 
does, but also keep an unextensionalized version of "th" for backward 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

779 
compatibility. *) 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

780 
fun also_extensionalize_theorem th = 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

781 
let val th' = Clausifier.extensionalize_theorem th in 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

782 
if Thm.eq_thm (th, th') then [th] 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

783 
else th :: Meson.make_clauses_unsorted [th'] 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

784 
end 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

785 

38028  786 
val neg_clausify = 
787 
single 

788 
#> Meson.make_clauses_unsorted 

38632
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

789 
#> maps also_extensionalize_theorem 
38028  790 
#> map Clausifier.introduce_combinators_in_theorem 
791 
#> Meson.finish_cnf 

792 

38652
e063be321438
perform etaexpansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38632
diff
changeset

793 
val type_has_top_sort = 
e063be321438
perform etaexpansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38632
diff
changeset

794 
exists_subtype (fn TFree (_, []) => true  TVar (_, []) => true  _ => false) 
e063be321438
perform etaexpansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38632
diff
changeset

795 

37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

796 
fun generic_metis_tac mode ctxt ths i st0 = 
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset

797 
let 
39037
5146d640aa4a
Let MESON take an additional "preskolemization tactic", which can be used to put the goal in definitional CNF
blanchet
parents:
38994
diff
changeset

798 
val thy = ProofContext.theory_of ctxt 
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset

799 
val _ = trace_msg (fn () => 
32956  800 
"Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths)) 
801 
in 

37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37625
diff
changeset

802 
if exists_type type_has_top_sort (prop_of st0) then 
37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

803 
(warning ("Metis: Proof state contains the universal sort {}"); Seq.empty) 
35568
8fbbfc39508f
renamed type_has_empty_sort to type_has_topsort  {} is the full universal sort;
wenzelm
parents:
34087
diff
changeset

804 
else 
39038  805 
Meson.MESON (K all_tac) (* TODO: Try (cnf.cnfx_rewrite_tac ctxt) *) 
39037
5146d640aa4a
Let MESON take an additional "preskolemization tactic", which can be used to put the goal in definitional CNF
blanchet
parents:
38994
diff
changeset

806 
(maps neg_clausify) 
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset

807 
(fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) 
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset

808 
ctxt i st0 
32956  809 
end 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

810 

37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

811 
val metis_tac = generic_metis_tac HO 
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

812 
val metisF_tac = generic_metis_tac FO 
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

813 
val metisFT_tac = generic_metis_tac FT 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

814 

38632
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

815 
(* Whenever "X" has schematic type variables, we treat "using X by metis" as 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

816 
"by (metis X)", to prevent "Subgoal.FOCUS" from freezing the type variables. 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

817 
We don't do it for nonschematic facts "X" because this breaks a few proofs 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

818 
(in the rare and subtle case where a proof relied on extensionality not being 
38994  819 
applied) and brings few benefits. *) 
38632
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

820 
val has_tvar = 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

821 
exists_type (exists_subtype (fn TVar _ => true  _ => false)) o prop_of 
37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

822 
fun method name mode = 
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

823 
Method.setup name (Attrib.thms >> (fn ths => fn ctxt => 
38632
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

824 
METHOD (fn facts => 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

825 
let 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

826 
val (schem_facts, nonschem_facts) = 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

827 
List.partition has_tvar facts 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

828 
in 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

829 
HEADGOAL (Method.insert_tac nonschem_facts THEN' 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

830 
CHANGED_PROP 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

831 
o generic_metis_tac mode ctxt (schem_facts @ ths)) 
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset

832 
end))) 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

833 

32956  834 
val setup = 
37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

835 
type_lits_setup 
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

836 
#> method @{binding metis} HO "Metis for FOL/HOL problems" 
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

837 
#> method @{binding metisF} FO "Metis for FOL problems" 
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

838 
#> method @{binding metisFT} FT 
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

839 
"Metis for FOL/HOL problems with fullytyped translation" 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

840 

028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

841 
end; 