author  blanchet 
Tue, 31 May 2011 16:38:36 +0200  
changeset 43086  4dce7f2bb59f 
parent 43085  0a2f5b86bdd7 
child 43087  b870759ce0f3 
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 
37577
5379f41a1322
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
blanchet
parents:
37575
diff
changeset

13 

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

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

15 

40157  16 
type metis_problem = 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

17 
{axioms: (Metis_Thm.thm * thm) list, 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

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

19 
old_skolems: (string * term) list} 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

20 

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

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

22 
val new_skolem_const_prefix : string 
37618
fa57a87f92a0
get rid of Skolem cache by performing CNFconversion after fact selection
blanchet
parents:
37616
diff
changeset

23 
val num_type_args: theory > string > int 
40259
c0e34371c2e2
prevent type errors because of inconsistent skolem Var types by giving fresh indices to Skolems
blanchet
parents:
40157
diff
changeset

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

25 
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

26 
val string_of_mode : mode > string 
40157  27 
val prepare_metis_problem : 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

28 
mode > Proof.context > bool > thm list > thm list list 
40157  29 
> mode * metis_problem 
24310  30 
end 
15347  31 

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

32 
structure Metis_Translate : METIS_TRANSLATE = 
15347  33 
struct 
34 

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

35 
open ATP_Translate 
15347  36 

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

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

38 

37618
fa57a87f92a0
get rid of Skolem cache by performing CNFconversion after fact selection
blanchet
parents:
37616
diff
changeset

39 
(* The number of type arguments of a constant, zero if it's monomorphic. For 
fa57a87f92a0
get rid of Skolem cache by performing CNFconversion after fact selection
blanchet
parents:
37616
diff
changeset

40 
(instances of) Skolem pseudoconstants, this information is encoded in the 
fa57a87f92a0
get rid of Skolem cache by performing CNFconversion after fact selection
blanchet
parents:
37616
diff
changeset

41 
constant name. *) 
fa57a87f92a0
get rid of Skolem cache by performing CNFconversion after fact selection
blanchet
parents:
37616
diff
changeset

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

43 
if String.isPrefix skolem_const_prefix s then 
39499  44 
s > space_explode Long_Name.separator > List.last > Int.fromString > the 
37618
fa57a87f92a0
get rid of Skolem cache by performing CNFconversion after fact selection
blanchet
parents:
37616
diff
changeset

45 
else 
fa57a87f92a0
get rid of Skolem cache by performing CNFconversion after fact selection
blanchet
parents:
37616
diff
changeset

46 
(s, Sign.the_const_type thy s) > Sign.const_typargs thy > length 
17150
ce2a1aeb42aa
DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents:
16976
diff
changeset

47 

40259
c0e34371c2e2
prevent type errors because of inconsistent skolem Var types by giving fresh indices to Skolems
blanchet
parents:
40157
diff
changeset

48 
fun new_skolem_var_name_from_const s = 
40145
04a05b2a7a36
no need to encode theorem number twice in skolem names
blanchet
parents:
39962
diff
changeset

49 
let val ss = s > space_explode Long_Name.separator in 
40259
c0e34371c2e2
prevent type errors because of inconsistent skolem Var types by giving fresh indices to Skolems
blanchet
parents:
40157
diff
changeset

50 
nth ss (length ss  2) 
40145
04a05b2a7a36
no need to encode theorem number twice in skolem names
blanchet
parents:
39962
diff
changeset

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

52 

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

53 
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

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

55 
(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

56 

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

57 
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

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

59 
 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

60 
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

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

62 
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

63 
((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

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

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

66 

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

67 
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

68 
old_skolem_const_prefix ^ Long_Name.separator ^ 
41491  69 
(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

70 

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

71 
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

72 
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

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

74 
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

75 
(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

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

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

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

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

80 
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

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

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

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

84 
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

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

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

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

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

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

90 
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

91 
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

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

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

94 
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

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

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

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

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

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

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

101 

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

102 
fun reveal_old_skolem_terms old_skolems = 
37632  103 
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

104 
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

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

108 
t 

109 
 t => t) 

110 

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

111 

39497
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 
(* HOL to FOL (Isabelle to Metis) *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

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

115 

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

116 
datatype mode = FO  HO  FT (* firstorder, higherorder, fullytyped *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

117 

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

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

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

120 
 string_of_mode FT = "FT" 
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 

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

131 
fun fn_isa_to_met_toplevel "equal" = "=" 
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)) = 
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)) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

159 
Metis_Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]); 
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)) = 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
40259
diff
changeset

170 
tag_with_type (Metis_Term.Fn (".", map hol_term_to_fol_FT [tm1, tm2])) 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
40259
diff
changeset

171 
(combtyp_of tm) 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

172 

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

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

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

177 
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

178 
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

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

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

181 
(CombConst(("equal", _), _, _), tms) => 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

182 
metis_lit pos "=" (map hol_term_to_fol_HO tms) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

183 
 _ => metis_lit pos "{}" [hol_term_to_fol_HO tm]) (*hBOOL*) 
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43003
diff
changeset

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

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

186 
(CombConst(("equal", _), _, _), tms) => 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

187 
metis_lit pos "=" (map hol_term_to_fol_FT tms) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

188 
 _ => metis_lit pos "{}" [hol_term_to_fol_FT tm]) (*hBOOL*); 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

189 

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

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

191 
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

192 
(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

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

194 

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

195 
(*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

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

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

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

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

200 

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

203 
(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

204 

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

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

206 
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

207 

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

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

209 
let 
42361  210 
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

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

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

214 
> (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

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

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

217 
(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

218 
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

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

220 
let 
42352  221 
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

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

223 
val mtylits = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

224 
if type_lits then map (metis_of_type_literals false) tylits else [] 
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 = 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

236 
{axioms: (Metis_Thm.thm * thm) list, 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

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

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 
(*Insert nonlogical axioms corresponding to all accumulated TFrees*) 
40157  251 
fun add_tfrees {axioms, tfrees, old_skolems} : metis_problem = 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

252 
{axioms = map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @ 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

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

254 
tfrees = tfrees, old_skolems = old_skolems} 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

255 

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

256 
(*transform isabelle type / arity clause to metis clause *) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

257 
fun add_type_thm [] lmap = lmap 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

258 
 add_type_thm ((ith, mth) :: cls) {axioms, tfrees, old_skolems} = 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

259 
add_type_thm cls {axioms = (mth, ith) :: axioms, tfrees = tfrees, 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

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

261 

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

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

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

264 
fun in_mterm (Metis_Term.Var _) = false 
41156  265 
 in_mterm (Metis_Term.Fn (nm, tm_list)) = 
266 
c = nm orelse exists in_mterm tm_list 

267 
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

268 

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

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

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

271 
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

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

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

274 
(*TrueI is returned as the Isabelle counterpart because there isn't any.*) 
43086  275 
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

276 
(TrueI, 
42895  277 
Metis_Thm.axiom (Metis_LiteralSet.fromList 
278 
(map m_arity_cls (concl_lits :: prem_lits)))); 

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

279 

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

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

281 
fun m_class_rel_cls (subclass, _) (superclass, _) = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

282 
[metis_lit false subclass [Metis_Term.Var "T"], metis_lit true superclass [Metis_Term.Var "T"]]; 
43086  283 
fun class_rel_cls ({subclass, superclass, ...} : class_rel_clause) = 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

284 
(TrueI, Metis_Thm.axiom (Metis_LiteralSet.fromList (m_class_rel_cls subclass superclass))); 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

285 

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

286 
fun type_ext thy tms = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

287 
let val subs = tfree_classes_of_terms tms 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

288 
val supers = tvar_classes_of_terms tms 
43003  289 
val tycons = type_consts_of_terms thy tms 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

290 
val (supers', arity_clauses) = make_arity_clauses thy tycons supers 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

291 
val class_rel_clauses = make_class_rel_clauses thy subs supers' 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

292 
in map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

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

294 

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

295 
(* Function to generate metis clauses, including comb and type clauses *) 
40157  296 
fun prepare_metis_problem mode0 ctxt type_lits cls thss = 
42361  297 
let val thy = Proof_Context.theory_of ctxt 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

298 
(*The modes FO and FT are sticky. HO can be downgraded to FO.*) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

299 
fun set_mode FO = FO 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

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

301 
if forall (forall (is_quasi_fol_clause thy)) (cls :: thss) then FO 
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

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

303 
 set_mode FT = FT 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

304 
val mode = set_mode mode0 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

305 
(*transform isabelle clause to metis clause *) 
41139
cb1cbae54dbf
add Metis support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

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

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

309 
val (mth, tfree_lits, old_skolems) = 
40145
04a05b2a7a36
no need to encode theorem number twice in skolem names
blanchet
parents:
39962
diff
changeset

310 
hol_thm_to_fol is_conjecture ctxt type_lits mode (length axioms) 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

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

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

313 
{axioms = (mth, isa_ith) :: axioms, 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

314 
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

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

316 
val lmap = {axioms = [], tfrees = init_tfrees ctxt, old_skolems = []} 
41139
cb1cbae54dbf
add Metis support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

317 
> fold (add_thm true o `Meson.make_meta_clause) cls 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

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

319 
> fold (fold (add_thm false o `Meson.make_meta_clause)) thss 
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

320 
val clause_lists = map (Metis_Thm.clause o #1) (#axioms lmap) 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

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

322 
exists (Metis_LiteralSet.exists (const_in_metis c o #2)) clause_lists 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

323 
val lmap = 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

324 
if mode = FO then 
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset

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

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

327 
let 
41156  328 
val fdefs = @{thms fFalse_def fTrue_def fNot_def fconj_def fdisj_def 
329 
fimplies_def fequal_def} 

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

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

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

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

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

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

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

336 
> 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

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

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

339 
else map prepare_helper thms) 
40145
04a05b2a7a36
no need to encode theorem number twice in skolem names
blanchet
parents:
39962
diff
changeset

340 
in lmap > fold (add_thm false) helper_ths end 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

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

342 
(mode, add_type_thm (type_ext thy (maps (map prop_of) (cls :: thss))) lmap) 
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39720
diff
changeset

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

344 

15347  345 
end; 