author  blanchet 
Tue, 31 May 2011 16:38:36 +0200  
changeset 43103  35962353e36b 
parent 43102  9a42899ec169 
child 43104  81d1b15aa0ae 
permissions  rwrr 
39958  1 
(* Title: HOL/Tools/Metis/metis_translate.ML 
38027  2 
Author: Jia Meng, Cambridge University Computer Laboratory and NICTA 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

3 
Author: Kong W. Susanto, Cambridge University Computer Laboratory 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

4 
Author: Lawrence C. Paulson, Cambridge University Computer Laboratory 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36378
diff
changeset

5 
Author: Jasmin Blanchette, TU Muenchen 
15347  6 

39494
bf7dd4902321
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents:
39355
diff
changeset

7 
Translation of HOL to FOL for Metis. 
15347  8 
*) 
9 

39494
bf7dd4902321
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents:
39355
diff
changeset

10 
signature METIS_TRANSLATE = 
24310  11 
sig 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43003
diff
changeset

12 
type type_literal = ATP_Translate.type_literal 
43102  13 
type type_sys = ATP_Translate.type_sys 
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset

14 

43103  15 
datatype mode = FO  HO  FT  MX 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43003
diff
changeset

16 

40157  17 
type metis_problem = 
43094  18 
{axioms : (Metis_Thm.thm * thm) list, 
19 
tfrees : type_literal list, 

20 
old_skolems : (string * term) list} 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

21 

43094  22 
val metis_equal : string 
23 
val metis_predicator : string 

24 
val metis_app_op : string 

42098
f978caf60bbe
more robust handling of variables in new Skolemizer
blanchet
parents:
41491
diff
changeset

25 
val metis_generated_var_prefix : string 
43094  26 
val metis_name_table : ((string * int) * string) list 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

27 
val reveal_old_skolem_terms : (string * term) list > term > term 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

28 
val string_of_mode : mode > string 
40157  29 
val prepare_metis_problem : 
43102  30 
Proof.context > mode > type_sys option > thm list > thm list 
43094  31 
> mode * int Symtab.table * metis_problem 
24310  32 
end 
15347  33 

39494
bf7dd4902321
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents:
39355
diff
changeset

34 
structure Metis_Translate : METIS_TRANSLATE = 
15347  35 
struct 
36 

43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

37 
open ATP_Problem 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43003
diff
changeset

38 
open ATP_Translate 
15347  39 

43094  40 
val metis_equal = "=" 
41 
val metis_predicator = "{}" 

42 
val metis_app_op = "." 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43003
diff
changeset

43 
val metis_generated_var_prefix = "_" 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

44 

43094  45 
val metis_name_table = 
46 
[((tptp_equal, 2), metis_equal), 

47 
((tptp_old_equal, 2), metis_equal), 

43096  48 
((const_prefix ^ predicator_name, 1), metis_predicator), 
49 
((const_prefix ^ app_op_name, 2), metis_app_op)] 

43094  50 

40145
04a05b2a7a36
no need to encode theorem number twice in skolem names
blanchet
parents:
39962
diff
changeset

51 
fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos) 
04a05b2a7a36
no need to encode theorem number twice in skolem names
blanchet
parents:
39962
diff
changeset

52 
 predicate_of thy (t, pos) = 
04a05b2a7a36
no need to encode theorem number twice in skolem names
blanchet
parents:
39962
diff
changeset

53 
(combterm_from_term thy [] (Envir.eta_contract t), pos) 
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset

54 

40145
04a05b2a7a36
no need to encode theorem number twice in skolem names
blanchet
parents:
39962
diff
changeset

55 
fun literals_of_term1 args thy (@{const Trueprop} $ P) = 
04a05b2a7a36
no need to encode theorem number twice in skolem names
blanchet
parents:
39962
diff
changeset

56 
literals_of_term1 args thy P 
04a05b2a7a36
no need to encode theorem number twice in skolem names
blanchet
parents:
39962
diff
changeset

57 
 literals_of_term1 args thy (@{const HOL.disj} $ P $ Q) = 
04a05b2a7a36
no need to encode theorem number twice in skolem names
blanchet
parents:
39962
diff
changeset

58 
literals_of_term1 (literals_of_term1 args thy P) thy Q 
04a05b2a7a36
no need to encode theorem number twice in skolem names
blanchet
parents:
39962
diff
changeset

59 
 literals_of_term1 (lits, ts) thy P = 
04a05b2a7a36
no need to encode theorem number twice in skolem names
blanchet
parents:
39962
diff
changeset

60 
let val ((pred, ts'), pol) = predicate_of thy (P, true) in 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43003
diff
changeset

61 
((pol, pred) :: lits, union (op =) ts ts') 
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset

62 
end 
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset

63 
val literals_of_term = literals_of_term1 ([], []) 
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset

64 

39896
13b3a2ba9ea7
encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents:
39890
diff
changeset

65 
fun old_skolem_const_name i j num_T_args = 
13b3a2ba9ea7
encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents:
39890
diff
changeset

66 
old_skolem_const_prefix ^ Long_Name.separator ^ 
41491  67 
(space_implode Long_Name.separator (map string_of_int [i, j, num_T_args])) 
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset

68 

39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

69 
fun conceal_old_skolem_terms i old_skolems t = 
39953
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39946
diff
changeset

70 
if exists_Const (curry (op =) @{const_name Meson.skolem} o fst) t then 
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset

71 
let 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

72 
fun aux old_skolems 
39953
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39946
diff
changeset

73 
(t as (Const (@{const_name Meson.skolem}, Type (_, [_, T])) $ _)) = 
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset

74 
let 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

75 
val (old_skolems, s) = 
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset

76 
if i = ~1 then 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

77 
(old_skolems, @{const_name undefined}) 
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

78 
else case AList.find (op aconv) old_skolems t of 
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

79 
s :: _ => (old_skolems, s) 
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset

80 
 [] => 
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset

81 
let 
39896
13b3a2ba9ea7
encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents:
39890
diff
changeset

82 
val s = old_skolem_const_name i (length old_skolems) 
13b3a2ba9ea7
encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents:
39890
diff
changeset

83 
(length (Term.add_tvarsT T [])) 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

84 
in ((s, t) :: old_skolems, s) end 
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

85 
in (old_skolems, Const (s, T)) end 
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

86 
 aux old_skolems (t1 $ t2) = 
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset

87 
let 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

88 
val (old_skolems, t1) = aux old_skolems t1 
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

89 
val (old_skolems, t2) = aux old_skolems t2 
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

90 
in (old_skolems, t1 $ t2) end 
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

91 
 aux old_skolems (Abs (s, T, t')) = 
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

92 
let val (old_skolems, t') = aux old_skolems t' in 
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

93 
(old_skolems, Abs (s, T, t')) 
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset

94 
end 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

95 
 aux old_skolems t = (old_skolems, t) 
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

96 
in aux old_skolems t end 
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset

97 
else 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

98 
(old_skolems, t) 
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset

99 

39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

100 
fun reveal_old_skolem_terms old_skolems = 
37632  101 
map_aterms (fn t as Const (s, _) => 
39896
13b3a2ba9ea7
encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents:
39890
diff
changeset

102 
if String.isPrefix old_skolem_const_prefix s then 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

103 
AList.lookup (op =) old_skolems s > the 
37632  104 
> map_types Type_Infer.paramify_vars 
105 
else 

106 
t 

107 
 t => t) 

108 

37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset

109 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

110 
(*  *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

111 
(* HOL to FOL (Isabelle to Metis) *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

112 
(*  *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

113 

43103  114 
(* firstorder, higherorder, fullytyped, mode X (fleXible) *) 
115 
datatype mode = FO  HO  FT  MX 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

116 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

117 
fun string_of_mode FO = "FO" 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

118 
 string_of_mode HO = "HO" 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

119 
 string_of_mode FT = "FT" 
43103  120 
 string_of_mode MX = "MX" 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

121 

42745
b817c6f91a98
reenabled equality proxy in Metis for higherorder reasoning
blanchet
parents:
42727
diff
changeset

122 
fun fn_isa_to_met_sublevel "equal" = "c_fequal" 
41139
cb1cbae54dbf
add Metis support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

123 
 fn_isa_to_met_sublevel "c_False" = "c_fFalse" 
cb1cbae54dbf
add Metis support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

124 
 fn_isa_to_met_sublevel "c_True" = "c_fTrue" 
cb1cbae54dbf
add Metis support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

125 
 fn_isa_to_met_sublevel "c_Not" = "c_fNot" 
cb1cbae54dbf
add Metis support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

126 
 fn_isa_to_met_sublevel "c_conj" = "c_fconj" 
cb1cbae54dbf
add Metis support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

127 
 fn_isa_to_met_sublevel "c_disj" = "c_fdisj" 
cb1cbae54dbf
add Metis support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

128 
 fn_isa_to_met_sublevel "c_implies" = "c_fimplies" 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

129 
 fn_isa_to_met_sublevel x = x 
42758
865ce93ce025
handle equality proxy in a more backwardcompatible way
blanchet
parents:
42745
diff
changeset

130 

43094  131 
fun fn_isa_to_met_toplevel "equal" = metis_equal 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

132 
 fn_isa_to_met_toplevel x = x 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

133 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

134 
fun metis_lit b c args = (b, (c, args)); 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

135 

42562  136 
fun metis_term_from_typ (Type (s, Ts)) = 
137 
Metis_Term.Fn (make_fixed_type_const s, map metis_term_from_typ Ts) 

138 
 metis_term_from_typ (TFree (s, _)) = 

139 
Metis_Term.Fn (make_fixed_type_var s, []) 

140 
 metis_term_from_typ (TVar (x, _)) = 

141 
Metis_Term.Var (make_schematic_type_var x) 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

142 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

143 
(*These two functions insert type literals before the real literals. That is the 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

144 
opposite order from TPTP linkup, but maybe OK.*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

145 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

146 
fun hol_term_to_fol_FO tm = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

147 
case strip_combterm_comb tm of 
42562  148 
(CombConst ((c, _), _, Ts), tms) => 
149 
let val tyargs = map metis_term_from_typ Ts 

150 
val args = map hol_term_to_fol_FO tms 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

151 
in Metis_Term.Fn (c, tyargs @ args) end 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

152 
 (CombVar ((v, _), _), []) => Metis_Term.Var v 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

153 
 _ => raise Fail "nonfirstorder combterm" 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

154 

42562  155 
fun hol_term_to_fol_HO (CombConst ((a, _), _, Ts)) = 
43094  156 
Metis_Term.Fn (fn_isa_to_met_sublevel a, map metis_term_from_typ Ts) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

157 
 hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis_Term.Var s 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

158 
 hol_term_to_fol_HO (CombApp (tm1, tm2)) = 
43094  159 
Metis_Term.Fn (metis_app_op, map hol_term_to_fol_HO [tm1, tm2]) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

160 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

161 
(*The fullytyped translation, to avoid type errors*) 
42562  162 
fun tag_with_type tm T = 
163 
Metis_Term.Fn (type_tag_name, [tm, metis_term_from_typ T]) 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

164 

41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
40259
diff
changeset

165 
fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
40259
diff
changeset

166 
tag_with_type (Metis_Term.Var s) ty 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
40259
diff
changeset

167 
 hol_term_to_fol_FT (CombConst ((a, _), ty, _)) = 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
40259
diff
changeset

168 
tag_with_type (Metis_Term.Fn (fn_isa_to_met_sublevel a, [])) ty 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
40259
diff
changeset

169 
 hol_term_to_fol_FT (tm as CombApp (tm1,tm2)) = 
43094  170 
tag_with_type 
171 
(Metis_Term.Fn (metis_app_op, map hol_term_to_fol_FT [tm1, tm2])) 

172 
(combtyp_of tm) 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

173 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43003
diff
changeset

174 
fun hol_literal_to_fol FO (pos, tm) = 
42562  175 
let 
176 
val (CombConst((p, _), _, Ts), tms) = strip_combterm_comb tm 

177 
val tylits = if p = "equal" then [] else map metis_term_from_typ Ts 

178 
val lits = map hol_term_to_fol_FO tms 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

179 
in metis_lit pos (fn_isa_to_met_toplevel p) (tylits @ lits) end 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43003
diff
changeset

180 
 hol_literal_to_fol HO (pos, tm) = 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

181 
(case strip_combterm_comb tm of 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

182 
(CombConst(("equal", _), _, _), tms) => 
43094  183 
metis_lit pos metis_equal (map hol_term_to_fol_HO tms) 
184 
 _ => metis_lit pos metis_predicator [hol_term_to_fol_HO tm]) 

43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43003
diff
changeset

185 
 hol_literal_to_fol FT (pos, tm) = 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

186 
(case strip_combterm_comb tm of 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

187 
(CombConst(("equal", _), _, _), tms) => 
43094  188 
metis_lit pos metis_equal (map hol_term_to_fol_FT tms) 
189 
 _ => metis_lit pos metis_predicator [hol_term_to_fol_FT tm]) 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

190 

40145
04a05b2a7a36
no need to encode theorem number twice in skolem names
blanchet
parents:
39962
diff
changeset

191 
fun literals_of_hol_term thy mode t = 
04a05b2a7a36
no need to encode theorem number twice in skolem names
blanchet
parents:
39962
diff
changeset

192 
let val (lits, types_sorts) = literals_of_term thy t in 
04a05b2a7a36
no need to encode theorem number twice in skolem names
blanchet
parents:
39962
diff
changeset

193 
(map (hol_literal_to_fol mode) lits, types_sorts) 
04a05b2a7a36
no need to encode theorem number twice in skolem names
blanchet
parents:
39962
diff
changeset

194 
end 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

195 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

196 
(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

197 
fun metis_of_type_literals pos (TyLitVar ((s, _), (s', _))) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

198 
metis_lit pos s [Metis_Term.Var s'] 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

199 
 metis_of_type_literals pos (TyLitFree ((s, _), (s', _))) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

200 
metis_lit pos s [Metis_Term.Fn (s',[])] 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

201 

42352  202 
fun has_default_sort _ (TVar _) = false 
203 
 has_default_sort ctxt (TFree (x, s)) = 

204 
(s = the_default [] (Variable.def_sort ctxt (x, ~1))); 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

205 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

206 
fun metis_of_tfree tf = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

207 
Metis_Thm.axiom (Metis_LiteralSet.singleton (metis_of_type_literals true tf)); 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

208 

43090  209 
fun hol_thm_to_fol is_conjecture ctxt mode j old_skolems th = 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

210 
let 
42361  211 
val thy = Proof_Context.theory_of ctxt 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

212 
val (old_skolems, (mlits, types_sorts)) = 
39888  213 
th > prop_of > Logic.strip_imp_concl 
214 
> conceal_old_skolem_terms j old_skolems 

40145
04a05b2a7a36
no need to encode theorem number twice in skolem names
blanchet
parents:
39962
diff
changeset

215 
> (HOLogic.dest_Trueprop #> literals_of_hol_term thy mode) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

216 
in 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

217 
if is_conjecture then 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

218 
(Metis_Thm.axiom (Metis_LiteralSet.fromList mlits), 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43003
diff
changeset

219 
raw_type_literals_for_types types_sorts, old_skolems) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

220 
else 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

221 
let 
42352  222 
val tylits = types_sorts > filter_out (has_default_sort ctxt) 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43003
diff
changeset

223 
> raw_type_literals_for_types 
43090  224 
val mtylits = map (metis_of_type_literals false) tylits 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

225 
in 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

226 
(Metis_Thm.axiom (Metis_LiteralSet.fromList(mtylits @ mlits)), [], 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

227 
old_skolems) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

228 
end 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

229 
end; 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

230 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

231 
(*  *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

232 
(* Logic maps manage the interface between HOL and firstorder logic. *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

233 
(*  *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

234 

40157  235 
type metis_problem = 
43094  236 
{axioms : (Metis_Thm.thm * thm) list, 
237 
tfrees : type_literal list, 

238 
old_skolems : (string * term) list} 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

239 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

240 
fun is_quasi_fol_clause thy = 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

241 
Meson.is_fol_term thy o snd o conceal_old_skolem_terms ~1 [] o prop_of 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

242 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

243 
(*Extract TFree constraints from context to include as conjecture clauses*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

244 
fun init_tfrees ctxt = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

245 
let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts in 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

246 
Vartab.fold add (#2 (Variable.constraints_of ctxt)) [] 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43003
diff
changeset

247 
> raw_type_literals_for_types 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

248 
end; 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

249 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

250 
fun const_in_metis c (pred, tm_list) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

251 
let 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

252 
fun in_mterm (Metis_Term.Var _) = false 
41156  253 
 in_mterm (Metis_Term.Fn (nm, tm_list)) = 
254 
c = nm orelse exists in_mterm tm_list 

255 
in c = pred orelse exists in_mterm tm_list end 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

256 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

257 
(* ARITY CLAUSE *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

258 
fun m_arity_cls (TConsLit ((c, _), (t, _), args)) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

259 
metis_lit true c [Metis_Term.Fn(t, map (Metis_Term.Var o fst) args)] 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

260 
 m_arity_cls (TVarLit ((c, _), (s, _))) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

261 
metis_lit false c [Metis_Term.Var s] 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

262 
(*TrueI is returned as the Isabelle counterpart because there isn't any.*) 
43086  263 
fun arity_cls ({prem_lits, concl_lits, ...} : arity_clause) = 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

264 
(TrueI, 
42895  265 
Metis_Thm.axiom (Metis_LiteralSet.fromList 
266 
(map m_arity_cls (concl_lits :: prem_lits)))); 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

267 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

268 
(* CLASSREL CLAUSE *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

269 
fun m_class_rel_cls (subclass, _) (superclass, _) = 
43091  270 
[metis_lit false subclass [Metis_Term.Var "T"], 
271 
metis_lit true superclass [Metis_Term.Var "T"]] 

43086  272 
fun class_rel_cls ({subclass, superclass, ...} : class_rel_clause) = 
43091  273 
(TrueI, m_class_rel_cls subclass superclass 
274 
> Metis_LiteralSet.fromList > Metis_Thm.axiom) 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

275 

fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

276 
fun type_ext thy tms = 
43091  277 
let 
278 
val subs = tfree_classes_of_terms tms 

279 
val supers = tvar_classes_of_terms tms 

280 
val tycons = type_consts_of_terms thy tms 

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

282 
val class_rel_clauses = make_class_rel_clauses thy subs supers' 

283 
in map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses end 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

284 

43094  285 
fun metis_name_from_atp s ary = 
286 
AList.lookup (op =) metis_name_table (s, ary) > the_default s 

43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

287 
fun metis_term_from_atp (ATerm (s, tms)) = 
43094  288 
if is_tptp_variable s then 
289 
Metis_Term.Var s 

290 
else 

291 
Metis_Term.Fn (metis_name_from_atp s (length tms), 

292 
map metis_term_from_atp tms) 

43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

293 
fun metis_atom_from_atp (AAtom (ATerm (s, tms))) = 
43094  294 
(metis_name_from_atp s (length tms), map metis_term_from_atp tms) 
43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

295 
 metis_atom_from_atp _ = raise Fail "not CNF  expected atom" 
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

296 
fun metis_literal_from_atp (AConn (ANot, [phi])) = 
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

297 
(false, metis_atom_from_atp phi) 
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

298 
 metis_literal_from_atp phi = (true, metis_atom_from_atp phi) 
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

299 
fun metis_literals_from_atp (AConn (AOr, [phi1, phi2])) = 
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

300 
uncurry (union (op =)) (pairself metis_literals_from_atp (phi1, phi2)) 
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

301 
 metis_literals_from_atp phi = [metis_literal_from_atp phi] 
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

302 
fun metis_axiom_from_atp clauses (Formula (ident, _, phi, _, _)) = 
43098
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43096
diff
changeset

303 
(phi > metis_literals_from_atp > Metis_LiteralSet.fromList 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43096
diff
changeset

304 
> Metis_Thm.axiom, 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43096
diff
changeset

305 
case try (unprefix conjecture_prefix) ident of 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43096
diff
changeset

306 
SOME s => Meson.make_meta_clause (nth clauses (the (Int.fromString s))) 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43096
diff
changeset

307 
 NONE => TrueI) 
43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

308 
 metis_axiom_from_atp _ _ = raise Fail "not CNF  expected formula" 
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

309 

43100  310 
val default_type_sys = Preds (Polymorphic, Nonmonotonic_Types, Light) 
311 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

312 
(* Function to generate metis clauses, including comb and type clauses *) 
43103  313 
fun prepare_metis_problem ctxt MX type_sys conj_clauses fact_clauses = 
43091  314 
let 
43100  315 
val type_sys = type_sys > the_default default_type_sys 
43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

316 
val explicit_apply = NONE 
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

317 
val clauses = conj_clauses @ fact_clauses 
43094  318 
val (atp_problem, _, _, _, _, _, sym_tab) = 
43098
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43096
diff
changeset

319 
prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply 
e88e974c4846
proper handling of type variable classes in new Metis
blanchet
parents:
43096
diff
changeset

320 
false false (map prop_of clauses) @{prop False} [] 
43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

321 
val axioms = 
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

322 
atp_problem 
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

323 
> maps (map_filter (try (metis_axiom_from_atp clauses)) o snd) 
43094  324 
in 
43103  325 
(MX, sym_tab, 
43094  326 
{axioms = axioms, tfrees = [], old_skolems = [] (* FIXME ### *)}) 
327 
end 

43100  328 
 prepare_metis_problem ctxt mode _ conj_clauses fact_clauses = 
43087
b870759ce0f3
added new metis mode, with no implementation yet
blanchet
parents:
43086
diff
changeset

329 
let 
b870759ce0f3
added new metis mode, with no implementation yet
blanchet
parents:
43086
diff
changeset

330 
val thy = Proof_Context.theory_of ctxt 
b870759ce0f3
added new metis mode, with no implementation yet
blanchet
parents:
43086
diff
changeset

331 
(* The modes FO and FT are sticky. HO can be downgraded to FO. *) 
b870759ce0f3
added new metis mode, with no implementation yet
blanchet
parents:
43086
diff
changeset

332 
val mode = 
b870759ce0f3
added new metis mode, with no implementation yet
blanchet
parents:
43086
diff
changeset

333 
if mode = HO andalso 
43091  334 
forall (forall (is_quasi_fol_clause thy)) 
43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

335 
[conj_clauses, fact_clauses] then 
43087
b870759ce0f3
added new metis mode, with no implementation yet
blanchet
parents:
43086
diff
changeset

336 
FO 
b870759ce0f3
added new metis mode, with no implementation yet
blanchet
parents:
43086
diff
changeset

337 
else 
b870759ce0f3
added new metis mode, with no implementation yet
blanchet
parents:
43086
diff
changeset

338 
mode 
41139
cb1cbae54dbf
add Metis support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

339 
fun add_thm is_conjecture (isa_ith, metis_ith) 
40157  340 
{axioms, tfrees, old_skolems} : metis_problem = 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

341 
let 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

342 
val (mth, tfree_lits, old_skolems) = 
43090  343 
hol_thm_to_fol is_conjecture ctxt mode (length axioms) old_skolems 
344 
metis_ith 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

345 
in 
43091  346 
{axioms = (mth, isa_ith) :: axioms, 
347 
tfrees = union (op =) tfree_lits tfrees, old_skolems = old_skolems} 

39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

348 
end; 
43091  349 
fun add_type_thm (ith, mth) {axioms, tfrees, old_skolems} = 
350 
{axioms = (mth, ith) :: axioms, tfrees = tfrees, 

351 
old_skolems = old_skolems} 

352 
fun add_tfrees {axioms, tfrees, old_skolems} = 

353 
{axioms = 

354 
map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @ axioms, 

355 
tfrees = tfrees, old_skolems = old_skolems} 

356 
val problem = 

357 
{axioms = [], tfrees = init_tfrees ctxt, old_skolems = []} 

358 
> fold (add_thm true o `Meson.make_meta_clause) conj_clauses 

359 
> add_tfrees 

43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

360 
> fold (add_thm false o `Meson.make_meta_clause) fact_clauses 
43091  361 
val clause_lists = map (Metis_Thm.clause o #1) (#axioms problem) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

362 
fun is_used c = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

363 
exists (Metis_LiteralSet.exists (const_in_metis c o #2)) clause_lists 
43091  364 
val problem = 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

365 
if mode = FO then 
43091  366 
problem 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

367 
else 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

368 
let 
41156  369 
val fdefs = @{thms fFalse_def fTrue_def fNot_def fconj_def fdisj_def 
370 
fimplies_def fequal_def} 

41139
cb1cbae54dbf
add Metis support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

371 
val prepare_helper = 
cb1cbae54dbf
add Metis support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

372 
zero_var_indexes 
cb1cbae54dbf
add Metis support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

373 
#> `(Meson.make_meta_clause 
cb1cbae54dbf
add Metis support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

374 
#> rewrite_rule (map safe_mk_meta_eq fdefs)) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

375 
val helper_ths = 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43003
diff
changeset

376 
helper_table 
42561
23ddc4e3d19c
have properly typeinstantiated helper facts (combinators and If)
blanchet
parents:
42544
diff
changeset

377 
> filter (is_used o prefix const_prefix o fst) 
42894
ce269ee43800
further improvements to "poly_{preds,tags}_{bang,query}"  better solution to the combinator problem + make sure type assumptions can be discharged
blanchet
parents:
42893
diff
changeset

378 
> maps (fn (_, (needs_full_types, thms)) => 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41139
diff
changeset

379 
if needs_full_types andalso mode <> FT then [] 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41139
diff
changeset

380 
else map prepare_helper thms) 
43091  381 
in problem > fold (add_thm false) helper_ths end 
43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset

382 
val type_ths = type_ext thy (map prop_of (conj_clauses @ fact_clauses)) 
43094  383 
in (mode, Symtab.empty, fold add_type_thm type_ths problem) end 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

384 

15347  385 
end; 