author  paulson 
Thu, 11 Oct 2007 15:59:31 +0200  
changeset 24958  ff15f76741bd 
parent 24940  8f9dea697b8d 
child 24974  a2f15968a6f2 
permissions  rwrr 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

1 
(* Title: HOL/Tools/metis_tools.ML 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

2 
Author: Kong W. Susanto and Lawrence C. Paulson, CU Computer Laboratory 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

3 
Copyright Cambridge University 2007 
23447  4 

5 
HOL setup for the Metis prover (version 2.0 from 2007). 

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

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

7 

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

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

9 
sig 
24309
01f3e1a43c24
turned type_lits into configuration option (with attribute);
wenzelm
parents:
24300
diff
changeset

10 
val type_lits: bool Config.T 
24319  11 
val metis_tac: Proof.context > thm list > int > tactic 
12 
val metisF_tac: Proof.context > thm list > int > tactic 

13 
val metisH_tac: Proof.context > thm list > int > tactic 

14 
val setup: theory > theory 

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

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

16 

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

17 
structure MetisTools: METIS_TOOLS = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

19 

24424  20 
structure Recon = ResReconstruct; 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

21 

24309
01f3e1a43c24
turned type_lits into configuration option (with attribute);
wenzelm
parents:
24300
diff
changeset

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

23 

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

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

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

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

27 
val EXCLUDED_MIDDLE' = read_instantiate [("R","False")] notE; 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

28 
val EXCLUDED_MIDDLE = rotate_prems 1 EXCLUDED_MIDDLE'; 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

29 
val REFL_THM = incr_indexes 2 (Meson.make_meta_clause refl); (*Rename from 0,1*) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

30 
val subst_em = zero_var_indexes (subst RS EXCLUDED_MIDDLE); 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

31 
val ssubst_em = read_instantiate [("t","?s"),("s","?t")] (sym RS subst_em); 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

32 

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

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

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

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

36 

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

37 
(* match untyped terms*) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

38 
fun untyped_aconv (Const(a,_)) (Const(b,_)) = (a=b) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

39 
 untyped_aconv (Free(a,_)) (Free(b,_)) = (a=b) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

40 
 untyped_aconv (Var((a,_),_)) (Var((b,_),_)) = (a=b) (*the index is ignored!*) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

41 
 untyped_aconv (Bound i) (Bound j) = (i=j) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

42 
 untyped_aconv (Abs(a,_,t)) (Abs(b,_,u)) = (a=b) andalso untyped_aconv t u 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

43 
 untyped_aconv (t1$t2) (u1$u2) = untyped_aconv t1 u1 andalso untyped_aconv t2 u2 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

45 

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

46 
(* Finding the relative location of an untyped term within a list of terms *) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

47 
fun get_index lit = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

48 
let val lit = Envir.eta_contract lit 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

49 
fun get n [] = raise Empty 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

50 
 get n (x::xs) = if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x)) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

51 
then n else get (n+1) xs 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

52 
in get 1 end; 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

53 

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

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

55 
(* HOL to FOL (Isabelle to Metis) *) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

57 

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

58 
fun fn_isa_to_met "equal" = "=" 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

60 

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

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

62 

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

63 
fun hol_type_to_fol (ResClause.AtomV x) = Metis.Term.Var x 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

64 
 hol_type_to_fol (ResClause.AtomF x) = Metis.Term.Fn(x,[]) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

65 
 hol_type_to_fol (ResClause.Comp(tc,tps)) = Metis.Term.Fn(tc, map hol_type_to_fol tps); 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

66 

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

67 
(*These two functions insert type literals before the real literals. That is the 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

68 
opposite order from TPTP linkup, but maybe OK.*) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

69 

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

70 
fun hol_term_to_fol_FO tm = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

71 
case ResHolClause.strip_comb tm of 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

72 
(ResHolClause.CombConst(c,_,tys), tms) => 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

73 
let val tyargs = map hol_type_to_fol tys 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

74 
val args = map hol_term_to_fol_FO tms 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

75 
in Metis.Term.Fn (c, tyargs @ args) end 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

76 
 (ResHolClause.CombVar(v,_), []) => Metis.Term.Var v 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

77 
 _ => error "hol_term_to_fol_FO"; 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

78 

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

79 
fun hol_term_to_fol_HO (ResHolClause.CombVar(a, ty)) = Metis.Term.Var a 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

80 
 hol_term_to_fol_HO (ResHolClause.CombConst(a, ty, tylist)) = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

81 
Metis.Term.Fn(fn_isa_to_met a, map hol_type_to_fol tylist) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

82 
 hol_term_to_fol_HO (ResHolClause.CombApp(tm1,tm2)) = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

83 
Metis.Term.Fn(".", map hol_term_to_fol_HO [tm1,tm2]); 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

84 

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

85 
fun hol_literal_to_fol true (ResHolClause.Literal (pol, tm)) = (*firstorder*) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

86 
let val (ResHolClause.CombConst(p,_,tys), tms) = ResHolClause.strip_comb tm 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

87 
val tylits = if p = "equal" then [] else map hol_type_to_fol tys 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

88 
val lits = map hol_term_to_fol_FO tms 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

89 
in metis_lit pol (fn_isa_to_met p) (tylits @ lits) end 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

90 
 hol_literal_to_fol false (ResHolClause.Literal (pol, tm)) = (*higherorder*) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

91 
case ResHolClause.strip_comb tm of 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

92 
(ResHolClause.CombConst("equal",_,_), tms) => 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

93 
metis_lit pol "=" (map hol_term_to_fol_HO tms) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

94 
 _ => metis_lit pol "{}" [hol_term_to_fol_HO tm]; 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

95 

24319  96 
fun literals_of_hol_thm thy isFO t = 
97 
let val (lits, types_sorts) = ResHolClause.literals_of_term thy t 

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

98 
in (map (hol_literal_to_fol isFO) lits, types_sorts) end; 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

99 

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

100 
(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*) 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

101 
fun metis_of_typeLit pos (ResClause.LTVar (s,x)) = metis_lit pos s [Metis.Term.Var x] 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

102 
 metis_of_typeLit pos (ResClause.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])]; 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

103 

24940  104 
fun default_sort ctxt (TVar _) = false 
105 
 default_sort ctxt (TFree(x,s)) = (s = Option.getOpt (Variable.def_sort ctxt (x,~1), [])); 

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

106 

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

107 
fun metis_of_tfree tf = 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

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

109 

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

110 
fun hol_thm_to_fol is_conjecture ctxt isFO th = 
24319  111 
let val thy = ProofContext.theory_of ctxt 
112 
val (mlits, types_sorts) = 

113 
(literals_of_hol_thm thy isFO o HOLogic.dest_Trueprop o prop_of) th 

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

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

115 
if is_conjecture then 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

116 
(Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), ResClause.add_typs types_sorts) 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

117 
else 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

118 
let val tylits = ResClause.add_typs 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

119 
(filter (not o default_sort ctxt) types_sorts) 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

120 
val mtylits = if Config.get ctxt type_lits 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

121 
then map (metis_of_typeLit false) tylits else [] 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

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

123 
(Metis.Thm.axiom (Metis.LiteralSet.fromList(mtylits @ mlits)), []) 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

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

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

126 

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

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

128 

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

129 
fun m_arity_cls (ResClause.TConsLit (c,t,args)) = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

130 
metis_lit true (ResClause.make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)] 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

131 
 m_arity_cls (ResClause.TVarLit (c,str)) = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

132 
metis_lit false (ResClause.make_type_class c) [Metis.Term.Var str]; 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

133 

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

134 
(*TrueI is returned as the Isabelle counterpart because there isn't any.*) 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

135 
fun arity_cls (ResClause.ArityClause{conclLit,premLits,...}) = 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

136 
(TrueI, 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

137 
Metis.Thm.axiom (Metis.LiteralSet.fromList (map m_arity_cls (conclLit :: premLits)))); 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

138 

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

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

140 

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

141 
fun m_classrel_cls subclass superclass = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

142 
[metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]]; 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

143 

24309
01f3e1a43c24
turned type_lits into configuration option (with attribute);
wenzelm
parents:
24300
diff
changeset

144 
fun classrel_cls (ResClause.ClassrelClause {axiom_name,subclass,superclass,...}) = 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

145 
(TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass))); 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

146 

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

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

148 
(* FOL to HOL (Metis to Isabelle) *) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

150 

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

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

152 

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

153 
fun terms_of [] = [] 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

154 
 terms_of (Term t :: tts) = t :: terms_of tts 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

155 
 terms_of (Type _ :: tts) = terms_of tts; 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

156 

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

157 
fun types_of [] = [] 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

158 
 types_of (Term (Term.Var((a,idx), T)) :: tts) = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

159 
if String.isPrefix "_" a then 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

160 
(*Variable generated by Metis, which might have been a type variable.*) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

161 
TVar(("'" ^ a, idx), HOLogic.typeS) :: types_of tts 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

163 
 types_of (Term _ :: tts) = types_of tts 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

164 
 types_of (Type T :: tts) = T :: types_of tts; 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

165 

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

166 
fun apply_list rator nargs rands = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

167 
let val trands = terms_of rands 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

168 
in if length trands = nargs then Term (list_comb(rator, trands)) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

169 
else error ("apply_list: wrong number of arguments: " ^ Display.raw_string_of_term rator ^ 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

171 
Int.toString nargs ^ " received " ^ commas (map Display.raw_string_of_term trands)) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

173 

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

174 
(*Instantiate constant c with the supplied types, but if they don't match its declared 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

175 
sort constraints, replace by a general type.*) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

176 
fun const_of ctxt (c,Ts) = Const (c, dummyT) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

177 

24500  178 
fun infer_types ctxt = 
179 
Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt); 

180 

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

181 
(*We use 1 rather than 0 because variable references in clauses may otherwise conflict 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

182 
with variable constraints in the goal...at least, type inference often fails otherwise. 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

183 
SEE ALSO axiom_inf below.*) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

184 
fun mk_var w = Term.Var((w,1), HOLogic.typeT); 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

185 

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

186 
(*include the default sort, if available*) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

187 
fun mk_tfree ctxt w = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

188 
let val ww = "'" ^ w 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

190 

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

191 
(*Remove the "apply" operator from an HO term*) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

192 
fun strip_happ args (Metis.Term.Fn(".",[t,u])) = strip_happ (u::args) t 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

193 
 strip_happ args x = (x, args); 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

194 

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

195 
(*Maps metis terms to isabelle terms*) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

196 
fun fol_term_to_hol_RAW ctxt fol_tm = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

197 
let val thy = ProofContext.theory_of ctxt 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

198 
val _ = Output.debug (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

199 
fun tm_to_tt (Metis.Term.Var v) = 
24424  200 
(case Recon.strip_prefix ResClause.tvar_prefix v of 
201 
SOME w => Type (Recon.make_tvar w) 

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

202 
 NONE => 
24424  203 
case Recon.strip_prefix ResClause.schematic_var_prefix v of 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

204 
SOME w => Term (mk_var w) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

205 
 NONE => Term (mk_var v) ) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

206 
(*Var from Metis with a name like _nnn; possibly a type variable*) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

207 
 tm_to_tt (Metis.Term.Fn ("{}", [arg])) = tm_to_tt arg (*hBOOL*) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

208 
 tm_to_tt (t as Metis.Term.Fn (".",_)) = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

209 
let val (rator,rands) = strip_happ [] t 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

210 
in case rator of 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

211 
Metis.Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

212 
 _ => case tm_to_tt rator of 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

213 
Term t => Term (list_comb(t, terms_of (map tm_to_tt rands))) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

214 
 _ => error "tm_to_tt: HO application" 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

216 
 tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

217 
and applic_to_tt ("=",ts) = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

218 
Term (list_comb(Const ("op =", HOLogic.typeT), terms_of (map tm_to_tt ts))) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

219 
 applic_to_tt (a,ts) = 
24424  220 
case Recon.strip_prefix ResClause.const_prefix a of 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

221 
SOME b => 
24424  222 
let val c = Recon.invert_const b 
223 
val ntypes = Recon.num_typargs thy c 

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

224 
val nterms = length ts  ntypes 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

225 
val tts = map tm_to_tt ts 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

226 
val tys = types_of (List.take(tts,ntypes)) 
24424  227 
val ntyargs = Recon.num_typargs thy c 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

228 
in if length tys = ntyargs then 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

229 
apply_list (const_of ctxt (c, tys)) nterms (List.drop(tts,ntypes)) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

230 
else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^ 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

231 
" but gets " ^ Int.toString (length tys) ^ 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

232 
" type arguments\n" ^ 
24920  233 
space_implode "\n" (map (Syntax.string_of_typ ctxt) tys) ^ 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

234 
" the terms are \n" ^ 
24920  235 
space_implode "\n" (map (Syntax.string_of_term ctxt) (terms_of tts))) 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

237 
 NONE => (*Not a constant. Is it a type constructor?*) 
24424  238 
case Recon.strip_prefix ResClause.tconst_prefix a of 
239 
SOME b => Type (Term.Type(Recon.invert_type_const b, types_of (map tm_to_tt ts))) 

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

240 
 NONE => (*Maybe a TFree. Should then check that ts=[].*) 
24424  241 
case Recon.strip_prefix ResClause.tfree_prefix a of 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

242 
SOME b => Type (mk_tfree ctxt b) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

243 
 NONE => (*a fixed variable? They are Skolem functions.*) 
24424  244 
case Recon.strip_prefix ResClause.fixed_var_prefix a of 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

245 
SOME b => 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

246 
let val opr = Term.Free(b, HOLogic.typeT) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

247 
in apply_list opr (length ts) (map tm_to_tt ts) end 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

248 
 NONE => error ("unexpected metis function: " ^ a) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

249 
in case tm_to_tt fol_tm of Term t => t  _ => error "fol_tm_to_tt: Term expected" end; 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

250 

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

251 
fun fol_terms_to_hol ctxt fol_tms = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

252 
let val ts = map (fol_term_to_hol_RAW ctxt) fol_tms 
24494
dc387e3999ec
replaced ProofContext.infer_types by general Syntax.check_terms;
wenzelm
parents:
24424
diff
changeset

253 
val _ = Output.debug (fn () => " calling type inference:") 
24920  254 
val _ = app (fn t => Output.debug (fn () => Syntax.string_of_term ctxt t)) ts 
24500  255 
val ts' = infer_types ctxt ts; 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

256 
val _ = app (fn t => Output.debug 
24920  257 
(fn () => " final term: " ^ Syntax.string_of_term ctxt t ^ 
258 
" of type " ^ Syntax.string_of_typ ctxt (type_of t))) 

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

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

260 
in ts' end; 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

261 

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

262 
fun mk_not (Const ("Not", _) $ b) = b 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

263 
 mk_not b = HOLogic.mk_not b; 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

264 

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

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

266 
(* FOL step Inference Rules *) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

268 

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

269 
(*for debugging only*) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

270 
fun print_thpair (fth,th) = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

271 
(Output.debug (fn () => "============================================="); 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

272 
Output.debug (fn () => "Metis: " ^ Metis.Thm.toString fth); 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

273 
Output.debug (fn () => "Isabelle: " ^ string_of_thm th)); 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

274 

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

275 
fun lookth thpairs (fth : Metis.Thm.thm) = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

276 
valOf (AList.lookup (uncurry Metis.Thm.equal) thpairs fth) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

277 
handle Option => error ("Failed to find a Metis theorem " ^ Metis.Thm.toString fth); 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

278 

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

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

280 

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

281 
fun inst_excluded_middle th thy i_atm = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

282 
let val vx = hd (term_vars (prop_of th)) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

283 
val substs = [(cterm_of thy vx, cterm_of thy i_atm)] 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

284 
in cterm_instantiate substs th end; 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

285 

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

286 
(* INFERENCE RULE: AXIOM *) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

287 
fun axiom_inf ctxt thpairs th = incr_indexes 1 (lookth thpairs th); 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

288 
(*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

289 

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

290 
(* INFERENCE RULE: ASSUME *) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

291 
fun assume_inf ctxt atm = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

293 
(ProofContext.theory_of ctxt) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

294 
(singleton (fol_terms_to_hol ctxt) (Metis.Term.Fn atm)); 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

295 

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

296 
(* INFERENCE RULE: INSTANTIATE. Type instantiations are ignored. Attempting to reconstruct 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

297 
them admits new possibilities of errors, e.g. concerning sorts. Instead we try to arrange 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

298 
that new TVars are distinct and that types can be inferred from terms.*) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

299 
fun inst_inf ctxt thpairs fsubst th = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

300 
let val thy = ProofContext.theory_of ctxt 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

301 
val i_th = lookth thpairs th 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

302 
val i_th_vars = term_vars (prop_of i_th) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

303 
fun find_var x = valOf (List.find (fn Term.Var((a,_),_) => a=x) i_th_vars) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

304 
fun subst_translation (x,y) = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

305 
let val v = find_var x 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

306 
val t = fol_term_to_hol_RAW ctxt y 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

307 
in SOME (cterm_of thy v, t) end 
24827  308 
handle Option => 
309 
(Output.debug (fn() => "List.find failed for the variable " ^ x ^ 

310 
" in " ^ string_of_thm i_th); 

311 
NONE) 

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

312 
fun remove_typeinst (a, t) = 
24424  313 
case Recon.strip_prefix ResClause.schematic_var_prefix a of 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

314 
SOME b => SOME (b, t) 
24424  315 
 NONE => case Recon.strip_prefix ResClause.tvar_prefix a of 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

316 
SOME _ => NONE (*type instantiations are forbidden!*) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

317 
 NONE => SOME (a,t) (*internal Metis var?*) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

318 
val _ = Output.debug (fn () => " isa th: " ^ string_of_thm i_th) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

319 
val substs = List.mapPartial remove_typeinst (Metis.Subst.toList fsubst) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

320 
val (vars,rawtms) = ListPair.unzip (List.mapPartial subst_translation substs) 
24500  321 
val tms = infer_types ctxt rawtms; 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

322 
val ctm_of = cterm_of thy o (map_types o Logic.incr_tvar) (1 + Thm.maxidx_of i_th) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

323 
val substs' = ListPair.zip (vars, map ctm_of tms) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

324 
val _ = Output.debug (fn() => "subst_translations:") 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

325 
val _ = app (fn (x,y) => Output.debug (fn () => string_of_cterm x ^ " > " ^ 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

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

328 
in cterm_instantiate substs' i_th end; 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

329 

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

330 
(* INFERENCE RULE: RESOLVE *) 
24424  331 

332 
(*Like RSN, but we rename apart only the type variables. Vars here typically have an index 

333 
of 1, and the use of RSN would increase this typically to 3. Instantiations of those Vars 

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

335 
fun resolve_inc_tyvars(tha,i,thb) = 

336 
let val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha 

337 
val ths = Seq.list_of (bicompose false (false,tha,nprems_of tha) i thb) 

338 
in 

339 
case distinct Thm.eq_thm ths of 

340 
[th] => th 

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

342 
end; 

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

343 

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

344 
fun resolve_inf ctxt thpairs atm th1 th2 = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

346 
val thy = ProofContext.theory_of ctxt 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

347 
val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

348 
val _ = Output.debug (fn () => " isa th1 (pos): " ^ string_of_thm i_th1) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

349 
val _ = Output.debug (fn () => " isa th2 (neg): " ^ string_of_thm i_th2) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

351 
if is_TrueI i_th1 then i_th2 (*Trivial cases where one operand is type info*) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

352 
else if is_TrueI i_th2 then i_th1 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

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

355 
val i_atm = singleton (fol_terms_to_hol ctxt) (Metis.Term.Fn atm) 
24920  356 
val _ = Output.debug (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm) 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

357 
val prems_th1 = prems_of i_th1 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

358 
val prems_th2 = prems_of i_th2 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

359 
val index_th1 = get_index (mk_not i_atm) prems_th1 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

360 
handle Empty => error "Failed to find literal in th1" 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

361 
val _ = Output.debug (fn () => " index_th1: " ^ Int.toString index_th1) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

362 
val index_th2 = get_index i_atm prems_th2 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

363 
handle Empty => error "Failed to find literal in th2" 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

364 
val _ = Output.debug (fn () => " index_th2: " ^ Int.toString index_th2) 
24424  365 
in resolve_inc_tyvars (Meson.select_literal index_th1 i_th1, index_th2, i_th2) end 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

367 

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

368 
(* INFERENCE RULE: REFL *) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

369 
fun refl_inf ctxt lit = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

370 
let val thy = ProofContext.theory_of ctxt 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

371 
val v_x = hd (term_vars (prop_of REFL_THM)) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

372 
val i_lit = singleton (fol_terms_to_hol ctxt) lit 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

373 
in cterm_instantiate [(cterm_of thy v_x, cterm_of thy i_lit)] REFL_THM end; 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

374 

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

375 
fun get_ty_arg_size thy (Const("op =",_)) = 0 (*equality has no type arguments*) 
24424  376 
 get_ty_arg_size thy (Const(c,_)) = (Recon.num_typargs thy c handle TYPE _ => 0) 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

377 
 get_ty_arg_size thy _ = 0; 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

378 

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

379 
(* INFERENCE RULE: EQUALITY *) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

380 
fun equality_inf ctxt isFO thpairs (pos,atm) fp fr = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

381 
let val thy = ProofContext.theory_of ctxt 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

382 
val [i_atm,i_tm] = fol_terms_to_hol ctxt [Metis.Term.Fn atm, fr] 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

383 
val _ = Output.debug (fn () => "sign of the literal: " ^ Bool.toString pos) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

384 
fun replace_item_list lx 0 (l::ls) = lx::ls 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

385 
 replace_item_list lx i (l::ls) = l :: replace_item_list lx (i1) ls 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

386 
fun path_finder_FO tm (p::ps) = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

387 
let val (tm1,args) = Term.strip_comb tm 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

388 
val adjustment = get_ty_arg_size thy tm1 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

389 
val p' = if adjustment > p then p else padjustment 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

390 
val tm_p = List.nth(args,p') 
24920  391 
handle Subscript => error ("equality_inf: " ^ Int.toString p ^ " adj " ^ 
392 
Int.toString adjustment ^ " term " ^ Syntax.string_of_term ctxt tm) 

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

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

394 
Output.debug (fn () => "path_finder: " ^ Int.toString p ^ 
24920  395 
" " ^ Syntax.string_of_term ctxt tm_p); 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

396 
if null ps (*FIXME: why not use patternmatching and avoid repetition*) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

397 
then (tm_p, list_comb (tm1, replace_item_list (Term.Bound 0) p' args)) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

398 
else let val (r,t) = path_finder_FO tm_p ps 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

399 
in (r, list_comb (tm1, replace_item_list t p' args)) end 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

401 
fun path_finder_HO tm [] = (tm, Term.Bound 0) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

402 
 path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

403 
 path_finder_HO (t$u) (p::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

404 
fun path_finder true tm ps = path_finder_FO tm ps 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

405 
 path_finder false (tm as Const("op =",_) $ _ $ _) (p::ps) = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

406 
(*equality: not curried, as other predicates are*) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

407 
if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

408 
else path_finder_HO tm (p::ps) (*1 selects second operand*) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

409 
 path_finder false tm (p::ps) = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

410 
path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

411 
fun path_finder_lit ((nt as Term.Const ("Not", _)) $ tm_a) idx = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

412 
let val (tm, tm_rslt) = path_finder isFO tm_a idx 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

413 
in (tm, nt $ tm_rslt) end 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

414 
 path_finder_lit tm_a idx = path_finder isFO tm_a idx 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

415 
val (tm_subst, body) = path_finder_lit i_atm fp 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

416 
val tm_abs = Term.Abs("x", Term.type_of tm_subst, body) 
24920  417 
val _ = Output.debug (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs) 
418 
val _ = Output.debug (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm) 

419 
val _ = Output.debug (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst) 

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

420 
val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill typed but gives right max*) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

421 
val subst' = incr_indexes (imax+1) (if pos then subst_em else ssubst_em) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

422 
val _ = Output.debug (fn () => "subst' " ^ string_of_thm subst') 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

423 
val eq_terms = map (pairself (cterm_of thy)) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

424 
(ListPair.zip (term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm])) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

425 
in cterm_instantiate eq_terms subst' end; 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

426 

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

427 
fun step ctxt isFO thpairs (fol_th, Metis.Proof.Axiom _) = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

428 
axiom_inf ctxt thpairs fol_th 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

429 
 step ctxt isFO thpairs (_, Metis.Proof.Assume f_atm) = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

431 
 step ctxt isFO thpairs (_, Metis.Proof.Subst(f_subst, f_th1)) = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

432 
inst_inf ctxt thpairs f_subst f_th1 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

433 
 step ctxt isFO thpairs (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2)) = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

434 
resolve_inf ctxt thpairs f_atm f_th1 f_th2 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

435 
 step ctxt isFO thpairs (_, Metis.Proof.Refl f_tm) = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

437 
 step ctxt isFO thpairs (_, Metis.Proof.Equality(f_lit, f_p, f_r)) = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

438 
equality_inf ctxt isFO thpairs f_lit f_p f_r; 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

439 

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

440 
val factor = Seq.hd o distinct_subgoals_tac; 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

441 

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

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

443 

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

444 
fun translate isFO _ thpairs [] = thpairs 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

445 
 translate isFO ctxt thpairs ((fol_th, inf) :: infpairs) = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

446 
let val _ = Output.debug (fn () => "=============================================") 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

447 
val _ = Output.debug (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

448 
val _ = Output.debug (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

449 
val th = Meson.flexflex_first_order (factor (step ctxt isFO thpairs (fol_th, inf))) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

450 
val _ = Output.debug (fn () => "ISABELLE THM: " ^ string_of_thm th) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

451 
val _ = Output.debug (fn () => "=============================================") 
24424  452 
val n_metis_lits = length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th))) 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

453 
in 
24424  454 
if nprems_of th = n_metis_lits then () 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

455 
else error "Metis: proof reconstruction has gone wrong"; 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

456 
translate isFO ctxt ((fol_th, th) :: thpairs) infpairs 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

458 

24855  459 
(*Determining which axiom clauses are actually used*) 
460 
fun used_axioms axioms (th, Metis.Proof.Axiom _) = SOME (lookth axioms th) 

461 
 used_axioms axioms _ = NONE; 

462 

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

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

464 
(* Translation of HO Clauses *) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

466 

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

467 
fun cnf_th th = hd (ResAxioms.cnf_axiom th); 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

468 

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

469 
val equal_imp_fequal' = cnf_th (thm"equal_imp_fequal"); 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

470 
val fequal_imp_equal' = cnf_th (thm"fequal_imp_equal"); 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

471 

24827  472 
val comb_I = cnf_th ResHolClause.comb_I; 
473 
val comb_K = cnf_th ResHolClause.comb_K; 

474 
val comb_B = cnf_th ResHolClause.comb_B; 

475 
val comb_C = cnf_th ResHolClause.comb_C; 

476 
val comb_S = cnf_th ResHolClause.comb_S; 

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

477 

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

478 
fun type_ext thy tms = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

479 
let val subs = ResAtp.tfree_classes_of_terms tms 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

480 
val supers = ResAtp.tvar_classes_of_terms tms 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

481 
and tycons = ResAtp.type_consts_of_terms thy tms 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

482 
val arity_clauses = ResClause.make_arity_clauses thy tycons supers 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

483 
val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

484 
val classrel_clauses = ResClause.make_classrel_clauses thy subs supers' 
24309
01f3e1a43c24
turned type_lits into configuration option (with attribute);
wenzelm
parents:
24300
diff
changeset

485 
in map classrel_cls classrel_clauses @ map arity_cls arity_clauses 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

487 

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

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

489 
(* Logic maps manage the interface between HOL and firstorder logic. *) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

491 

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

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

493 
{isFO : bool, 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

494 
axioms : (Metis.Thm.thm * Thm.thm) list, 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

495 
tfrees : ResClause.type_literal list}; 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

496 

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

497 
fun const_in_metis c (pol,(pred,tm_list)) = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

499 
fun in_mterm (Metis.Term.Var nm) = false 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

500 
 in_mterm (Metis.Term.Fn (".", tm_list)) = exists in_mterm tm_list 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

501 
 in_mterm (Metis.Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

503 

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

504 
(*Extract TFree constraints from context to include as conjecture clauses*) 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

505 
fun init_tfrees ctxt = 
24940  506 
let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

507 
in ResClause.add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end; 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

508 

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

509 
(*transform isabelle clause to metis clause *) 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

510 
fun add_thm is_conjecture ctxt (ith, {isFO, axioms, tfrees}) : logic_map = 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

511 
let val (mth, tfree_lits) = hol_thm_to_fol is_conjecture ctxt isFO ith 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

513 
{isFO = isFO, 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

514 
axioms = (mth, Meson.make_meta_clause ith) :: axioms, 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

515 
tfrees = tfree_lits union tfrees} 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

517 

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

518 
(*transform isabelle type / arity clause to metis clause *) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

519 
fun add_type_thm [] lmap = lmap 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

520 
 add_type_thm ((ith, mth) :: cls) {isFO, axioms, tfrees} = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

521 
add_type_thm cls {isFO = isFO, 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

522 
axioms = (mth, ith) :: axioms, 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

524 

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

525 
(*Insert nonlogical axioms corresponding to all accumulated TFrees*) 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

526 
fun add_tfrees {isFO, axioms, tfrees} : logic_map = 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

527 
{isFO = isFO, 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

528 
axioms = (map (fn tf => (metis_of_tfree tf, TrueI)) (distinct op= tfrees)) @ axioms, 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

529 
tfrees = tfrees}; 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

530 

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

531 
(* Function to generate metis clauses, including comb and type clauses *) 
24958  532 
fun build_map mode ctxt cls ths = 
533 
let val thy = ProofContext.theory_of ctxt 

534 
val all_thms_FO = forall (Meson.is_fol_term thy o prop_of) 

535 
val isFO = (mode = ResAtp.Fol) orelse 

536 
(mode <> ResAtp.Hol andalso all_thms_FO (cls @ ths)) 

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

537 
val lmap0 = foldl (add_thm true ctxt) 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

538 
{isFO = isFO, axioms = [], tfrees = init_tfrees ctxt} cls 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

539 
val lmap = foldl (add_thm false ctxt) (add_tfrees lmap0) ths 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

540 
val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

541 
fun used c = exists (Metis.LiteralSet.exists (const_in_metis c)) clause_lists 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

542 
(*Now check for the existence of certain combinators*) 
24827  543 
val thI = if used "c_COMBI" then [comb_I] else [] 
544 
val thK = if used "c_COMBK" then [comb_K] else [] 

545 
val thB = if used "c_COMBB" then [comb_B] else [] 

546 
val thC = if used "c_COMBC" then [comb_C] else [] 

547 
val thS = if used "c_COMBS" then [comb_S] else [] 

548 
val thEQ = if used "c_fequal" then [fequal_imp_equal', equal_imp_fequal'] else [] 

549 
val lmap' = if isFO then lmap 

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

550 
else foldl (add_thm false ctxt) lmap (thEQ @ thS @ thC @ thB @ thK @ thI) 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

552 
add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap' 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

554 

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

555 
fun refute cls = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

556 
Metis.Resolution.loop (Metis.Resolution.new Metis.Resolution.default cls); 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

557 

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

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

559 

24855  560 
fun common_thm ths1 ths2 = exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2); 
561 

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

562 
(* Main function to start metis prove and reconstruction *) 
24855  563 
fun FOL_SOLVE mode ctxt cls ths0 = 
24958  564 
let val th_cls_pairs = map (fn th => (PureThy.get_name_hint th, ResAxioms.cnf_axiom th)) ths0 
24855  565 
val ths = List.concat (map #2 th_cls_pairs) 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

566 
val _ = if exists(is_false o prop_of) cls then error "problem contains the empty clause" 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

568 
val _ = Output.debug (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

569 
val _ = app (fn th => Output.debug (fn () => string_of_thm th)) cls 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

570 
val _ = Output.debug (fn () => "THEOREM CLAUSES") 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

571 
val _ = app (fn th => Output.debug (fn () => string_of_thm th)) ths 
24958  572 
val {isFO,axioms,tfrees} = build_map mode ctxt cls ths 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

573 
val _ = if null tfrees then () 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

574 
else (Output.debug (fn () => "TFREE CLAUSES"); 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

575 
app (fn tf => Output.debug (fn _ => ResClause.tptp_of_typeLit true tf)) tfrees) 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

576 
val _ = Output.debug (fn () => "CLAUSES GIVEN TO METIS") 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

577 
val thms = map #1 axioms 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

578 
val _ = app (fn th => Output.debug (fn () => Metis.Thm.toString th)) thms 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

579 
val _ = if isFO 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

580 
then Output.debug (fn () => "goal is firstorder") 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

581 
else Output.debug (fn () => "goal is higherorder") 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

582 
val _ = Output.debug (fn () => "START METIS PROVE PROCESS") 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

584 
case refute thms of 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

585 
Metis.Resolution.Contradiction mth => 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

586 
let val _ = Output.debug (fn () => "METIS RECONSTRUCTION START: " ^ 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

587 
Metis.Thm.toString mth) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

588 
val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

589 
(*add constraints arising from converting goal to clause form*) 
24855  590 
val proof = Metis.Proof.proof mth 
591 
val result = translate isFO ctxt' axioms proof 

592 
and used = List.mapPartial (used_axioms axioms) proof 

593 
val _ = Output.debug (fn () => "METIS COMPLETED...clauses actually used:") 

594 
val _ = app (fn th => Output.debug (fn () => string_of_thm th)) used 

595 
val unused = filter (fn (a,cls) => not (common_thm used cls)) th_cls_pairs 

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

596 
in 
24855  597 
if null unused then () 
598 
else warning ("Unused theorems: " ^ commas (map #1 unused)); 

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

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

600 
(_,ith)::_ => (Output.debug (fn () => "success: " ^ string_of_thm ith); ith) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

601 
 _ => error "METIS: no result" 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

603 
 Metis.Resolution.Satisfiable _ => error "Metis finds the theorem to be invalid" 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

605 

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

606 
fun metis_general_tac mode ctxt ths i st0 = 
24041
d5845b7c1a24
metis_tac: proper context (ProofContext.init it *not* sufficient);
wenzelm
parents:
23447
diff
changeset

607 
let val _ = Output.debug (fn () => 
d5845b7c1a24
metis_tac: proper context (ProofContext.init it *not* sufficient);
wenzelm
parents:
23447
diff
changeset

608 
"Metis called with theorems " ^ cat_lines (map string_of_thm ths)) 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

609 
in 
24855  610 
(Meson.MESON ResAxioms.neg_clausify (fn cls => rtac (FOL_SOLVE mode ctxt cls ths) 1) i 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

611 
THEN ResAxioms.expand_defs_tac st0) st0 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

613 

24041
d5845b7c1a24
metis_tac: proper context (ProofContext.init it *not* sufficient);
wenzelm
parents:
23447
diff
changeset

614 
val metis_tac = metis_general_tac ResAtp.Auto; 
d5845b7c1a24
metis_tac: proper context (ProofContext.init it *not* sufficient);
wenzelm
parents:
23447
diff
changeset

615 
val metisF_tac = metis_general_tac ResAtp.Fol; 
d5845b7c1a24
metis_tac: proper context (ProofContext.init it *not* sufficient);
wenzelm
parents:
23447
diff
changeset

616 
val metisH_tac = metis_general_tac ResAtp.Hol; 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

617 

24041
d5845b7c1a24
metis_tac: proper context (ProofContext.init it *not* sufficient);
wenzelm
parents:
23447
diff
changeset

618 
fun method mode = Method.thms_ctxt_args (fn ths => fn ctxt => 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

619 
Method.SIMPLE_METHOD' 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

620 
(setmp ResHolClause.typ_level ResHolClause.T_CONST (*constanttyped*) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

621 
(setmp ResHolClause.minimize_applies false (*avoid this optimization*) 
24041
d5845b7c1a24
metis_tac: proper context (ProofContext.init it *not* sufficient);
wenzelm
parents:
23447
diff
changeset

622 
(CHANGED_PROP o metis_general_tac mode ctxt ths)))); 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

623 

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

624 
val setup = 
24309
01f3e1a43c24
turned type_lits into configuration option (with attribute);
wenzelm
parents:
24300
diff
changeset

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

626 
Method.add_methods 
24041
d5845b7c1a24
metis_tac: proper context (ProofContext.init it *not* sufficient);
wenzelm
parents:
23447
diff
changeset

627 
[("metis", method ResAtp.Auto, "METIS for FOL & HOL problems"), 
d5845b7c1a24
metis_tac: proper context (ProofContext.init it *not* sufficient);
wenzelm
parents:
23447
diff
changeset

628 
("metisF", method ResAtp.Fol, "METIS for FOL problems"), 
d5845b7c1a24
metis_tac: proper context (ProofContext.init it *not* sufficient);
wenzelm
parents:
23447
diff
changeset

629 
("metisH", method ResAtp.Hol, "METIS for HOL problems"), 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

631 
Method.no_args (Method.SIMPLE_METHOD' (K (ResAxioms.expand_defs_tac refl))), 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

632 
"cleanup after conversion to clauses")]; 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

633 

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

634 
end; 