author  paulson 
Thu, 19 Apr 2007 18:23:11 +0200  
changeset 22731  abfdccaed085 
parent 22724  3002683a6e0f 
child 22846  fb79144af9a3 
permissions  rwrr 
15347  1 
(* Author: Jia Meng, Cambridge University Computer Laboratory 
2 
ID: $Id$ 

3 
Copyright 2004 University of Cambridge 

4 

20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

5 
Transformation of axiom rules (elim/intro/etc) into CNF forms. 
15347  6 
*) 
7 

15997  8 
signature RES_AXIOMS = 
21505  9 
sig 
10 
val trace_abs: bool ref 

11 
val cnf_axiom : string * thm > thm list 

21071  12 
val cnf_name : string > thm list 
15997  13 
val meta_cnf_axiom : thm > thm list 
21505  14 
val pairname : thm > string * thm 
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

15 
val skolem_thm : thm > thm list 
21505  16 
val cnf_rules_pairs : (string * thm) list > (thm * (string * int)) list 
18708  17 
val meson_method_setup : theory > theory 
18 
val setup : theory > theory 

22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

19 
val assume_abstract_list: string > thm list > thm list 
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

20 
val neg_conjecture_clauses: thm > int > thm list * (string * typ) list 
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

21 
val claset_rules_of: Proof.context > (string * thm) list (*FIXME DELETE*) 
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

22 
val simpset_rules_of: Proof.context > (string * thm) list (*FIXME DELETE*) 
21505  23 
val atpset_rules_of: Proof.context > (string * thm) list 
24 
end; 

19196
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset

25 

21900  26 
structure ResAxioms = 
15997  27 
struct 
15347  28 

20996  29 
(*For running the comparison between combinators and abstractions. 
30 
CANNOT be a ref, as the setting is used while Isabelle is built. 

22644
f10465ee7aa2
Fixed the treatment of TVars in conjecture clauses (they are deleted, not frozen)
paulson
parents:
22596
diff
changeset

31 
Currently TRUE: the combinator code cannot be used with proof reconstruction 
f10465ee7aa2
Fixed the treatment of TVars in conjecture clauses (they are deleted, not frozen)
paulson
parents:
22596
diff
changeset

32 
because it is not performed by inference!!*) 
21900  33 
val abstract_lambdas = true; 
20419  34 

35 
val trace_abs = ref false; 

18000
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

36 

20902  37 
(* FIXME legacy *) 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

38 
fun freeze_thm th = #1 (Drule.freeze_thaw th); 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

39 

20902  40 
val lhs_of = #1 o Logic.dest_equals o Thm.prop_of; 
41 
val rhs_of = #2 o Logic.dest_equals o Thm.prop_of; 

20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

42 

4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

43 

20445  44 
(*Store definitions of abstraction functions, ensuring that identical righthand 
45 
sides are denoted by the same functions and thereby reducing the need for 

46 
extensionality in proofs. 

47 
FIXME! Store in theory data!!*) 

20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

48 

20867
e7b92a48e22b
Refinements to abstraction. Seeding with combinators K, I and B.
paulson
parents:
20863
diff
changeset

49 
(*Populate the abstraction cache with common combinators.*) 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

50 
fun seed th net = 
20902  51 
let val (_,ct) = Thm.dest_abs NONE (Drule.rhs_of th) 
20867
e7b92a48e22b
Refinements to abstraction. Seeding with combinators K, I and B.
paulson
parents:
20863
diff
changeset

52 
val t = Logic.legacy_varify (term_of ct) 
22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
22345
diff
changeset

53 
in Net.insert_term Thm.eq_thm (t, th) net end; 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

54 

4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

55 
val abstraction_cache = ref 
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21102
diff
changeset

56 
(seed (thm"ATP_Linkup.I_simp") 
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21102
diff
changeset

57 
(seed (thm"ATP_Linkup.B_simp") 
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21102
diff
changeset

58 
(seed (thm"ATP_Linkup.K_simp") Net.empty))); 
20867
e7b92a48e22b
Refinements to abstraction. Seeding with combinators K, I and B.
paulson
parents:
20863
diff
changeset

59 

20445  60 

15997  61 
(**** Transformation of Elimination Rules into FirstOrder Formulas****) 
15347  62 

21430
77651b6d9d6c
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents:
21290
diff
changeset

63 
val cfalse = cterm_of HOL.thy HOLogic.false_const; 
77651b6d9d6c
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents:
21290
diff
changeset

64 
val ctp_false = cterm_of HOL.thy (HOLogic.mk_Trueprop HOLogic.false_const); 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

65 

21430
77651b6d9d6c
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents:
21290
diff
changeset

66 
(*Converts an elimrule into an equivalent theorem that does not have the 
77651b6d9d6c
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents:
21290
diff
changeset

67 
predicate variable. Leaves other theorems unchanged. We simply instantiate the 
77651b6d9d6c
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents:
21290
diff
changeset

68 
conclusion variable to False.*) 
16009  69 
fun transform_elim th = 
21430
77651b6d9d6c
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents:
21290
diff
changeset

70 
case concl_of th of (*conclusion variable*) 
77651b6d9d6c
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents:
21290
diff
changeset

71 
Const("Trueprop",_) $ (v as Var(_,Type("bool",[]))) => 
77651b6d9d6c
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents:
21290
diff
changeset

72 
Thm.instantiate ([], [(cterm_of HOL.thy v, cfalse)]) th 
77651b6d9d6c
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents:
21290
diff
changeset

73 
 v as Var(_, Type("prop",[])) => 
77651b6d9d6c
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents:
21290
diff
changeset

74 
Thm.instantiate ([], [(cterm_of HOL.thy v, ctp_false)]) th 
77651b6d9d6c
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents:
21290
diff
changeset

75 
 _ => th; 
15997  76 

77 
(**** Transformation of Clasets and Simpsets into FirstOrder Axioms ****) 

78 

21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21102
diff
changeset

79 
(*Transfer a theorem into theory ATP_Linkup.thy if it is not already 
15359
8bad1f42fec0
new CLAUSIFY attribute for proof reconstruction with lemmas
paulson
parents:
15347
diff
changeset

80 
inside that theory  because it's needed for Skolemization *) 
8bad1f42fec0
new CLAUSIFY attribute for proof reconstruction with lemmas
paulson
parents:
15347
diff
changeset

81 

21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21102
diff
changeset

82 
(*This will refer to the final version of theory ATP_Linkup.*) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

83 
val recon_thy_ref = Theory.self_ref (the_context ()); 
15359
8bad1f42fec0
new CLAUSIFY attribute for proof reconstruction with lemmas
paulson
parents:
15347
diff
changeset

84 

21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21102
diff
changeset

85 
(*If called while ATP_Linkup is being created, it will transfer to the 
16563  86 
current version. If called afterward, it will transfer to the final version.*) 
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21102
diff
changeset

87 
fun transfer_to_ATP_Linkup th = 
16563  88 
transfer (Theory.deref recon_thy_ref) th handle THM _ => th; 
15347  89 

20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

90 

16009  91 
(**** SKOLEMIZATION BY INFERENCE (lcp) ****) 
92 

18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

93 
(*Traverse a theorem, declaring Skolem function definitions. String s is the suggested 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

94 
prefix for the Skolem constant. Result is a new theory*) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

95 
fun declare_skofuns s th thy = 
21071  96 
let val nref = ref 0 
97 
fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (thy, axs) = 

20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

98 
(*Existential: declare a Skolem function, then insert into body and continue*) 
22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

99 
let val cname = Name.internal ("sko_" ^ s ^ "_" ^ Int.toString (inc nref)) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

100 
val args = term_frees xtp (*get the formal parameter list*) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

101 
val Ts = map type_of args 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

102 
val cT = Ts > T 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

103 
val c = Const (Sign.full_name thy cname, cT) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

104 
val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

105 
(*Forms a lambdaabstraction over the formal parameters*) 
20783  106 
val thy' = Sign.add_consts_authentic [(cname, cT, NoSyn)] thy 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

107 
(*Theory is augmented with the constant, then its def*) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

108 
val cdef = cname ^ "_def" 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

109 
val thy'' = Theory.add_defs_i false false [(cdef, equals cT $ c $ rhs)] thy' 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

110 
in dec_sko (subst_bound (list_comb(c,args), p)) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

111 
(thy'', get_axiom thy'' cdef :: axs) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

112 
end 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

113 
 dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) thx = 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

114 
(*Universal quant: insert a free variable into body and continue*) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

115 
let val fname = Name.variant (add_term_names (p,[])) a 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

116 
in dec_sko (subst_bound (Free(fname,T), p)) thx end 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

117 
 dec_sko (Const ("op &", _) $ p $ q) thx = dec_sko q (dec_sko p thx) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

118 
 dec_sko (Const ("op ", _) $ p $ q) thx = dec_sko q (dec_sko p thx) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

119 
 dec_sko (Const ("Trueprop", _) $ p) thx = dec_sko p thx 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

120 
 dec_sko t thx = thx (*Do nothing otherwise*) 
20419  121 
in dec_sko (prop_of th) (thy,[]) end; 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

122 

89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

123 
(*Traverse a theorem, accumulating Skolem function definitions.*) 
22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

124 
fun assume_skofuns s th = 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

125 
let val sko_count = ref 0 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

126 
fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs = 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

127 
(*Existential: declare a Skolem function, then insert into body and continue*) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

128 
let val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

129 
val args = term_frees xtp \\ skos (*the formal parameters*) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

130 
val Ts = map type_of args 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

131 
val cT = Ts > T 
22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

132 
val id = "sko_" ^ s ^ "_" ^ Int.toString (inc sko_count) 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

133 
val c = Free (id, cT) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

134 
val rhs = list_abs_free (map dest_Free args, 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

135 
HOLogic.choice_const T $ xtp) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

136 
(*Forms a lambdaabstraction over the formal parameters*) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

137 
val def = equals cT $ c $ rhs 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

138 
in dec_sko (subst_bound (list_comb(c,args), p)) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

139 
(def :: defs) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

140 
end 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

141 
 dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) defs = 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

142 
(*Universal quant: insert a free variable into body and continue*) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

143 
let val fname = Name.variant (add_term_names (p,[])) a 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

144 
in dec_sko (subst_bound (Free(fname,T), p)) defs end 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

145 
 dec_sko (Const ("op &", _) $ p $ q) defs = dec_sko q (dec_sko p defs) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

146 
 dec_sko (Const ("op ", _) $ p $ q) defs = dec_sko q (dec_sko p defs) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

147 
 dec_sko (Const ("Trueprop", _) $ p) defs = dec_sko p defs 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

148 
 dec_sko t defs = defs (*Do nothing otherwise*) 
20419  149 
in dec_sko (prop_of th) [] end; 
150 

151 

152 
(**** REPLACING ABSTRACTIONS BY FUNCTION DEFINITIONS ****) 

153 

154 
(*Returns the vars of a theorem*) 

155 
fun vars_of_thm th = 

22691  156 
map (Thm.cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []); 
20419  157 

158 
(*Make a version of fun_cong with a given variable name*) 

159 
local 

160 
val fun_cong' = fun_cong RS asm_rl; (*renumber f, g to prevent clashes with (a,0)*) 

161 
val cx = hd (vars_of_thm fun_cong'); 

162 
val ty = typ_of (ctyp_of_term cx); 

20445  163 
val thy = theory_of_thm fun_cong; 
20419  164 
fun mkvar a = cterm_of thy (Var((a,0),ty)); 
165 
in 

166 
fun xfun_cong x = Thm.instantiate ([], [(cx, mkvar x)]) fun_cong' 

167 
end; 

168 

20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

169 
(*Removes the lambdas from an equation of the form t = (%x. u). A nonnegative n, 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

170 
serves as an upper bound on how many to remove.*) 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

171 
fun strip_lambdas 0 th = th 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

172 
 strip_lambdas n th = 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

173 
case prop_of th of 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

174 
_ $ (Const ("op =", _) $ _ $ Abs (x,_,_)) => 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

175 
strip_lambdas (n1) (freeze_thm (th RS xfun_cong x)) 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

176 
 _ => th; 
20419  177 

20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

178 
(*Convert meta to objectequality. Fails for theorems like split_comp_eq, 
20419  179 
where some types have the empty sort.*) 
22218  180 
val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq"; 
181 
fun mk_object_eq th = th RS meta_eq_to_obj_eq 

20419  182 
handle THM _ => error ("Theorem contains empty sort: " ^ string_of_thm th); 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

183 

20419  184 
(*Apply a function definition to an argument, betareducing the result.*) 
185 
fun beta_comb cf x = 

186 
let val th1 = combination cf (reflexive x) 

20902  187 
val th2 = beta_conversion false (Drule.rhs_of th1) 
20419  188 
in transitive th1 th2 end; 
189 

190 
(*Apply a function definition to arguments, betareducing along the way.*) 

191 
fun list_combination cf [] = cf 

192 
 list_combination cf (x::xs) = list_combination (beta_comb cf x) xs; 

193 

194 
fun list_cabs ([] , t) = t 

195 
 list_cabs (v::vars, t) = Thm.cabs v (list_cabs(vars,t)); 

196 

20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

197 
fun assert_eta_free ct = 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

198 
let val t = term_of ct 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

199 
in if (t aconv Envir.eta_contract t) then () 
20419  200 
else error ("Eta redex in term: " ^ string_of_cterm ct) 
201 
end; 

202 

20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

203 
fun eq_absdef (th1, th2) = 
20445  204 
Context.joinable (theory_of_thm th1, theory_of_thm th2) andalso 
205 
rhs_of th1 aconv rhs_of th2; 

206 

207 
fun lambda_free (Abs _) = false 

208 
 lambda_free (t $ u) = lambda_free t andalso lambda_free u 

209 
 lambda_free _ = true; 

20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

210 

d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

211 
fun monomorphic t = 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

212 
Term.fold_types (Term.fold_atyps (fn TVar _ => K false  _ => I)) t true; 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

213 

20710
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

214 
fun dest_abs_list ct = 
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

215 
let val (cv,ct') = Thm.dest_abs NONE ct 
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

216 
val (cvs,cu) = dest_abs_list ct' 
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

217 
in (cv::cvs, cu) end 
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

218 
handle CTERM _ => ([],ct); 
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

219 

384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

220 
fun lambda_list [] u = u 
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

221 
 lambda_list (v::vs) u = lambda v (lambda_list vs u); 
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

222 

384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

223 
fun abstract_rule_list [] [] th = th 
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

224 
 abstract_rule_list (v::vs) (ct::cts) th = abstract_rule v ct (abstract_rule_list vs cts th) 
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

225 
 abstract_rule_list _ _ th = raise THM ("abstract_rule_list", 0, [th]); 
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

226 

20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

227 

4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

228 
val Envir.Envir {asol = tenv0, iTs = tyenv0, ...} = Envir.empty 0 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

229 

20969
341808e0b7f2
Abstraction reuse code now checks that the abstraction function can be used in the current
paulson
parents:
20902
diff
changeset

230 
(*Does an existing abstraction definition have an RHS that matches the one we need now? 
341808e0b7f2
Abstraction reuse code now checks that the abstraction function can be used in the current
paulson
parents:
20902
diff
changeset

231 
thy is the current theory, which must extend that of theorem th.*) 
341808e0b7f2
Abstraction reuse code now checks that the abstraction function can be used in the current
paulson
parents:
20902
diff
changeset

232 
fun match_rhs thy t th = 
341808e0b7f2
Abstraction reuse code now checks that the abstraction function can be used in the current
paulson
parents:
20902
diff
changeset

233 
let val _ = if !trace_abs then warning ("match_rhs: " ^ string_of_cterm (cterm_of thy t) ^ 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

234 
" against\n" ^ string_of_thm th) else (); 
20867
e7b92a48e22b
Refinements to abstraction. Seeding with combinators K, I and B.
paulson
parents:
20863
diff
changeset

235 
val (tyenv,tenv) = Pattern.first_order_match thy (rhs_of th, t) (tyenv0,tenv0) 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

236 
val term_insts = map Meson.term_pair_of (Vartab.dest tenv) 
20969
341808e0b7f2
Abstraction reuse code now checks that the abstraction function can be used in the current
paulson
parents:
20902
diff
changeset

237 
val ct_pairs = if subthy (theory_of_thm th, thy) andalso 
341808e0b7f2
Abstraction reuse code now checks that the abstraction function can be used in the current
paulson
parents:
20902
diff
changeset

238 
forall lambda_free (map #2 term_insts) 
341808e0b7f2
Abstraction reuse code now checks that the abstraction function can be used in the current
paulson
parents:
20902
diff
changeset

239 
then map (pairself (cterm_of thy)) term_insts 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

240 
else raise Pattern.MATCH (*Cannot allow lambdas in the instantiation*) 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

241 
fun ctyp2 (ixn, (S, T)) = (ctyp_of thy (TVar (ixn, S)), ctyp_of thy T) 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

242 
val th' = cterm_instantiate ct_pairs th 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

243 
in SOME (th, instantiate (map ctyp2 (Vartab.dest tyenv), []) th') end 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

244 
handle _ => NONE; 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

245 

20419  246 
(*Traverse a theorem, declaring abstraction function definitions. String s is the suggested 
247 
prefix for the constants. Resulting theory is returned in the first theorem. *) 

22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

248 
fun declare_absfuns s th = 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

249 
let val nref = ref 0 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

250 
fun abstract thy ct = 
20445  251 
if lambda_free (term_of ct) then (transfer thy (reflexive ct), []) 
252 
else 

253 
case term_of ct of 

20710
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

254 
Abs _ => 
22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

255 
let val cname = Name.internal ("llabs_" ^ s ^ "_" ^ Int.toString (inc nref)) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

256 
val _ = assert_eta_free ct; 
20710
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

257 
val (cvs,cta) = dest_abs_list ct 
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

258 
val (vs,Tvs) = ListPair.unzip (map (dest_Free o term_of) cvs) 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

259 
val _ = if !trace_abs then warning ("Nested lambda: " ^ string_of_cterm cta) else (); 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

260 
val (u'_th,defs) = abstract thy cta 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

261 
val _ = if !trace_abs then warning ("Returned " ^ string_of_thm u'_th) else (); 
20902  262 
val cu' = Drule.rhs_of u'_th 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

263 
val u' = term_of cu' 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

264 
val abs_v_u = lambda_list (map term_of cvs) u' 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

265 
(*get the formal parameters: ALL variables free in the term*) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

266 
val args = term_frees abs_v_u 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

267 
val _ = if !trace_abs then warning (Int.toString (length args) ^ " arguments") else (); 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

268 
val rhs = list_abs_free (map dest_Free args, abs_v_u) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

269 
(*Forms a lambdaabstraction over the formal parameters*) 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

270 
val _ = if !trace_abs then warning ("Looking up " ^ string_of_cterm cu') else (); 
20969
341808e0b7f2
Abstraction reuse code now checks that the abstraction function can be used in the current
paulson
parents:
20902
diff
changeset

271 
val thy = theory_of_thm u'_th 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

272 
val (ax,ax',thy) = 
20969
341808e0b7f2
Abstraction reuse code now checks that the abstraction function can be used in the current
paulson
parents:
20902
diff
changeset

273 
case List.mapPartial (match_rhs thy abs_v_u) 
341808e0b7f2
Abstraction reuse code now checks that the abstraction function can be used in the current
paulson
parents:
20902
diff
changeset

274 
(Net.match_term (!abstraction_cache) u') of 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

275 
(ax,ax')::_ => 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

276 
(if !trace_abs then warning ("Reusing axiom " ^ string_of_thm ax) else (); 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

277 
(ax,ax',thy)) 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

278 
 [] => 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

279 
let val _ = if !trace_abs then warning "Lookup was empty" else (); 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

280 
val Ts = map type_of args 
20710
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

281 
val cT = Ts > (Tvs > typ_of (ctyp_of_term cu')) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

282 
val c = Const (Sign.full_name thy cname, cT) 
20783  283 
val thy = Sign.add_consts_authentic [(cname, cT, NoSyn)] thy 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

284 
(*Theory is augmented with the constant, 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

285 
then its definition*) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

286 
val cdef = cname ^ "_def" 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

287 
val thy = Theory.add_defs_i false false 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

288 
[(cdef, equals cT $ c $ rhs)] thy 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

289 
val _ = if !trace_abs then (warning ("Definition is " ^ 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

290 
string_of_thm (get_axiom thy cdef))) 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

291 
else (); 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

292 
val ax = get_axiom thy cdef > freeze_thm 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

293 
> mk_object_eq > strip_lambdas (length args) 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

294 
> mk_meta_eq > Meson.generalize 
20969
341808e0b7f2
Abstraction reuse code now checks that the abstraction function can be used in the current
paulson
parents:
20902
diff
changeset

295 
val (_,ax') = Option.valOf (match_rhs thy abs_v_u ax) 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

296 
val _ = if !trace_abs then 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

297 
(warning ("Declaring: " ^ string_of_thm ax); 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

298 
warning ("Instance: " ^ string_of_thm ax')) 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

299 
else (); 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

300 
val _ = abstraction_cache := Net.insert_term eq_absdef 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

301 
((Logic.varify u'), ax) (!abstraction_cache) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

302 
handle Net.INSERT => 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

303 
raise THM ("declare_absfuns: INSERT", 0, [th,u'_th,ax]) 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

304 
in (ax,ax',thy) end 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

305 
in if !trace_abs then warning ("Lookup result: " ^ string_of_thm ax') else (); 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

306 
(transitive (abstract_rule_list vs cvs u'_th) (symmetric ax'), ax::defs) end 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

307 
 (t1$t2) => 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

308 
let val (ct1,ct2) = Thm.dest_comb ct 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

309 
val (th1,defs1) = abstract thy ct1 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

310 
val (th2,defs2) = abstract (theory_of_thm th1) ct2 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

311 
in (combination th1 th2, defs1@defs2) end 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

312 
val _ = if !trace_abs then warning ("declare_absfuns, Abstracting: " ^ string_of_thm th) else (); 
20419  313 
val (eqth,defs) = abstract (theory_of_thm th) (cprop_of th) 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

314 
val ths = equal_elim eqth th :: map (strip_lambdas ~1 o mk_object_eq o freeze_thm) defs 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

315 
val _ = if !trace_abs then warning ("declare_absfuns, Result: " ^ string_of_thm (hd ths)) else (); 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

316 
in (theory_of_thm eqth, map Drule.eta_contraction_rule ths) end; 
20419  317 

20902  318 
fun name_of def = try (#1 o dest_Free o lhs_of) def; 
20567
93ae490fe02c
Bug fix to prevent exception dest_Free from escaping
paulson
parents:
20525
diff
changeset

319 

20525
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset

320 
(*A name is valid provided it isn't the name of a defined abstraction.*) 
20567
93ae490fe02c
Bug fix to prevent exception dest_Free from escaping
paulson
parents:
20525
diff
changeset

321 
fun valid_name defs (Free(x,T)) = not (x mem_string (List.mapPartial name_of defs)) 
20525
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset

322 
 valid_name defs _ = false; 
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset

323 

22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

324 
(*s is the theorem name (hint) or the word "subgoal"*) 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

325 
fun assume_absfuns s th = 
20445  326 
let val thy = theory_of_thm th 
327 
val cterm = cterm_of thy 

22724
3002683a6e0f
Fixes for proof reconstruction, especially involving abstractions and definitions
paulson
parents:
22691
diff
changeset

328 
val abs_count = ref 0 
20525
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset

329 
fun abstract ct = 
20445  330 
if lambda_free (term_of ct) then (reflexive ct, []) 
331 
else 

332 
case term_of ct of 

20419  333 
Abs (_,T,u) => 
20710
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

334 
let val _ = assert_eta_free ct; 
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

335 
val (cvs,cta) = dest_abs_list ct 
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

336 
val (vs,Tvs) = ListPair.unzip (map (dest_Free o term_of) cvs) 
20525
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset

337 
val (u'_th,defs) = abstract cta 
20902  338 
val cu' = Drule.rhs_of u'_th 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

339 
val u' = term_of cu' 
20710
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

340 
(*Could use Thm.cabs instead of lambda to work at level of cterms*) 
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

341 
val abs_v_u = lambda_list (map term_of cvs) (term_of cu') 
20525
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset

342 
(*get the formal parameters: free variables not present in the defs 
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset

343 
(to avoid taking abstraction function names as parameters) *) 
20710
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

344 
val args = filter (valid_name defs) (term_frees abs_v_u) 
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

345 
val crhs = list_cabs (map cterm args, cterm abs_v_u) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

346 
(*Forms a lambdaabstraction over the formal parameters*) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

347 
val rhs = term_of crhs 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

348 
val (ax,ax') = 
20969
341808e0b7f2
Abstraction reuse code now checks that the abstraction function can be used in the current
paulson
parents:
20902
diff
changeset

349 
case List.mapPartial (match_rhs thy abs_v_u) 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

350 
(Net.match_term (!abstraction_cache) u') of 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

351 
(ax,ax')::_ => 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

352 
(if !trace_abs then warning ("Reusing axiom " ^ string_of_thm ax) else (); 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

353 
(ax,ax')) 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

354 
 [] => 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

355 
let val Ts = map type_of args 
20710
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

356 
val const_ty = Ts > (Tvs > typ_of (ctyp_of_term cu')) 
22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

357 
val id = "llabs_" ^ s ^ "_" ^ Int.toString (inc abs_count) 
22724
3002683a6e0f
Fixes for proof reconstruction, especially involving abstractions and definitions
paulson
parents:
22691
diff
changeset

358 
val c = Free (id, const_ty) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

359 
val ax = assume (Thm.capply (cterm (equals const_ty $ c)) crhs) 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

360 
> mk_object_eq > strip_lambdas (length args) 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

361 
> mk_meta_eq > Meson.generalize 
20969
341808e0b7f2
Abstraction reuse code now checks that the abstraction function can be used in the current
paulson
parents:
20902
diff
changeset

362 
val (_,ax') = Option.valOf (match_rhs thy abs_v_u ax) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

363 
val _ = abstraction_cache := Net.insert_term eq_absdef (rhs,ax) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

364 
(!abstraction_cache) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

365 
handle Net.INSERT => 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

366 
raise THM ("assume_absfuns: INSERT", 0, [th,u'_th,ax]) 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

367 
in (ax,ax') end 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

368 
in if !trace_abs then warning ("Lookup result: " ^ string_of_thm ax') else (); 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

369 
(transitive (abstract_rule_list vs cvs u'_th) (symmetric ax'), ax::defs) end 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

370 
 (t1$t2) => 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

371 
let val (ct1,ct2) = Thm.dest_comb ct 
20525
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset

372 
val (t1',defs1) = abstract ct1 
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset

373 
val (t2',defs2) = abstract ct2 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

374 
in (combination t1' t2', defs1@defs2) end 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

375 
val _ = if !trace_abs then warning ("assume_absfuns, Abstracting: " ^ string_of_thm th) else (); 
20525
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset

376 
val (eqth,defs) = abstract (cprop_of th) 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

377 
val ths = equal_elim eqth th :: map (strip_lambdas ~1 o mk_object_eq o freeze_thm) defs 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

378 
val _ = if !trace_abs then warning ("assume_absfuns, Result: " ^ string_of_thm (hd ths)) else (); 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

379 
in map Drule.eta_contraction_rule ths end; 
20419  380 

16009  381 

382 
(*cterms are used throughout for efficiency*) 

18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

383 
val cTrueprop = Thm.cterm_of HOL.thy HOLogic.Trueprop; 
16009  384 

385 
(*cterm version of mk_cTrueprop*) 

386 
fun c_mkTrueprop A = Thm.capply cTrueprop A; 

387 

388 
(*Given an abstraction over n variables, replace the bound variables by free 

389 
ones. Return the body, along with the list of free variables.*) 

20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

390 
fun c_variant_abs_multi (ct0, vars) = 
16009  391 
let val (cv,ct) = Thm.dest_abs NONE ct0 
392 
in c_variant_abs_multi (ct, cv::vars) end 

393 
handle CTERM _ => (ct0, rev vars); 

394 

20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

395 
(*Given the definition of a Skolem function, return a theorem to replace 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

396 
an existential formula by a use of that function. 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

397 
Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

398 
fun skolem_of_def def = 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

399 
let val (c,rhs) = Drule.dest_equals (cprop_of (freeze_thm def)) 
16009  400 
val (ch, frees) = c_variant_abs_multi (rhs, []) 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

401 
val (chilbert,cabs) = Thm.dest_comb ch 
22596  402 
val {thy,t, ...} = rep_cterm chilbert 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

403 
val T = case t of Const ("Hilbert_Choice.Eps", Type("fun",[_,T])) => T 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

404 
 _ => raise THM ("skolem_of_def: expected Eps", 0, [def]) 
22596  405 
val cex = Thm.cterm_of thy (HOLogic.exists_const T) 
16009  406 
val ex_tm = c_mkTrueprop (Thm.capply cex cabs) 
407 
and conc = c_mkTrueprop (Drule.beta_conv cabs (Drule.list_comb(c,frees))); 

18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

408 
fun tacf [prem] = rewrite_goals_tac [def] THEN rtac (prem RS someI_ex) 1 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

409 
in Goal.prove_raw [ex_tm] conc tacf 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

410 
> forall_intr_list frees 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

411 
> forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

412 
> Thm.varifyT 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

413 
end; 
16009  414 

20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

415 
(*Converts an Isabelle theorem (intro, elim or simp format, even higherorder) into NNF.*) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

416 
fun to_nnf th = 
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
21102
diff
changeset

417 
th > transfer_to_ATP_Linkup 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

418 
> transform_elim > zero_var_indexes > freeze_thm 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

419 
> ObjectLogic.atomize_thm > make_nnf > strip_lambdas ~1; 
16009  420 

18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

421 
(*Generate Skolem functions for a theorem supplied in nnf*) 
22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

422 
fun skolem_of_nnf s th = 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

423 
map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th); 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

424 

20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

425 
fun assert_lambda_free ths msg = 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

426 
case filter (not o lambda_free o prop_of) ths of 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

427 
[] => () 
22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

428 
 ths' => error (msg ^ "\n" ^ cat_lines (map string_of_thm ths')); 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset

429 

22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

430 
fun assume_abstract s th = 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset

431 
if lambda_free (prop_of th) then [th] 
22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

432 
else th > Drule.eta_contraction_rule > assume_absfuns s 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset

433 
> tap (fn ths => assert_lambda_free ths "assume_abstract: lambdas") 
20445  434 

20419  435 
(*Replace lambdas by assumed function definitions in the theorems*) 
22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

436 
fun assume_abstract_list s ths = 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

437 
if abstract_lambdas then List.concat (map (assume_abstract s) ths) 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

438 
else map Drule.eta_contraction_rule ths; 
20419  439 

440 
(*Replace lambdas by declared function definitions in the theorems*) 

22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

441 
fun declare_abstract' s (thy, []) = (thy, []) 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

442 
 declare_abstract' s (thy, th::ths) = 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

443 
let val (thy', th_defs) = 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset

444 
if lambda_free (prop_of th) then (thy, [th]) 
20445  445 
else 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

446 
th > zero_var_indexes > freeze_thm 
22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

447 
> Drule.eta_contraction_rule > transfer thy > declare_absfuns s 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

448 
val _ = assert_lambda_free th_defs "declare_abstract: lambdas" 
22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

449 
val (thy'', ths') = declare_abstract' s (thy', ths) 
20419  450 
in (thy'', th_defs @ ths') end; 
451 

22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

452 
fun declare_abstract s (thy, ths) = 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

453 
if abstract_lambdas then declare_abstract' s (thy, ths) 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

454 
else (thy, map Drule.eta_contraction_rule ths); 
20419  455 

21071  456 
(*Keep the full complexity of the original name*) 
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
21646
diff
changeset

457 
fun flatten_name s = space_implode "_X" (NameSpace.explode s); 
21071  458 

22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

459 
fun fake_name th = 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

460 
if PureThy.has_name_hint th then flatten_name (PureThy.get_name_hint th) 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

461 
else gensym "unknown_thm_"; 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

462 

abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

463 
(*Skolemize a named theorem, with Skolem functions as additional premises.*) 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

464 
fun skolem_thm th = 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

465 
let val nnfth = to_nnf th and s = fake_name th 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

466 
in Meson.make_cnf (skolem_of_nnf s nnfth) nnfth > assume_abstract_list s > Meson.finish_cnf 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

467 
end 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

468 
handle THM _ => []; 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

469 

18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

470 
(*Declare Skolem functions for a theorem, supplied in nnf and with its name. 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

471 
It returns a modified theory, unless skolemization fails.*) 
22471  472 
fun skolem thy th = 
22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

473 
Option.map 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

474 
(fn (nnfth, s) => 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

475 
let val _ = Output.debug (fn () => "skolemizing " ^ s ^ ": ") 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

476 
val (thy',defs) = declare_skofuns s nnfth thy 
20419  477 
val cnfs = Meson.make_cnf (map skolem_of_def defs) nnfth 
22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

478 
val (thy'',cnfs') = declare_abstract s (thy',cnfs) 
22345
85f76b341893
Improved handling of situation when theorem in cache disagrees with theorem supplied: new clauses
paulson
parents:
22218
diff
changeset

479 
in (map Goal.close_result (Meson.finish_cnf cnfs'), thy'') 
20419  480 
end) 
22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

481 
(SOME (to_nnf th, fake_name th) handle THM _ => NONE); 
16009  482 

22516  483 
structure ThmCache = TheoryDataFun 
484 
(struct 

485 
val name = "ATP/thm_cache"; 

486 
type T = (thm list) Thmtab.table ref; 

487 
val empty : T = ref Thmtab.empty; 

488 
fun copy (ref tab) : T = ref tab; 

489 
val extend = copy; 

490 
fun merge _ (ref tab1, ref tab2) : T = ref (Thmtab.merge (K true) (tab1, tab2)); 

491 
fun print _ _ = (); 

492 
end); 

493 

494 
(*The cache prevents repeated clausification of a theorem, and also repeated declaration of 

495 
Skolem functions. The global one holds theorems proved prior to this point. Theory data 

496 
holds the remaining ones.*) 

497 
val global_clause_cache = ref (Thmtab.empty : (thm list) Thmtab.table); 

498 

18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

499 
(*Populate the clause cache using the supplied theorem. Return the clausal form 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

500 
and modified theory.*) 
22516  501 
fun skolem_cache_thm clause_cache th thy = 
22471  502 
case Thmtab.lookup (!clause_cache) th of 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

503 
NONE => 
22471  504 
(case skolem thy (Thm.transfer thy th) of 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

505 
NONE => ([th],thy) 
22345
85f76b341893
Improved handling of situation when theorem in cache disagrees with theorem supplied: new clauses
paulson
parents:
22218
diff
changeset

506 
 SOME (cls,thy') => 
22471  507 
(if null cls 
508 
then warning ("skolem_cache: empty clause set for " ^ string_of_thm th) 

20473
7ef72f030679
Using Drule.local_standard to reduce the space usage
paulson
parents:
20461
diff
changeset

509 
else (); 
22471  510 
change clause_cache (Thmtab.update (th, cls)); 
22345
85f76b341893
Improved handling of situation when theorem in cache disagrees with theorem supplied: new clauses
paulson
parents:
22218
diff
changeset

511 
(cls,thy'))) 
22471  512 
 SOME cls => (cls,thy); 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

513 

d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

514 
(*Exported function to convert Isabelle theorems into axiom clauses*) 
22471  515 
fun cnf_axiom th = 
22516  516 
let val cache = ThmCache.get (Thm.theory_of_thm th) 
517 
handle ERROR _ => global_clause_cache 

518 
val in_cache = if cache = global_clause_cache then NONE else Thmtab.lookup (!cache) th 

519 
in 

520 
case in_cache of 

521 
NONE => 

522 
(case Thmtab.lookup (!global_clause_cache) th of 

523 
NONE => 

524 
let val cls = map Goal.close_result (skolem_thm th) 

22724
3002683a6e0f
Fixes for proof reconstruction, especially involving abstractions and definitions
paulson
parents:
22691
diff
changeset

525 
in Output.debug (fn () => Int.toString (length cls) ^ " clauses inserted into cache: " ^ 
3002683a6e0f
Fixes for proof reconstruction, especially involving abstractions and definitions
paulson
parents:
22691
diff
changeset

526 
(if PureThy.has_name_hint th then PureThy.get_name_hint th 
3002683a6e0f
Fixes for proof reconstruction, especially involving abstractions and definitions
paulson
parents:
22691
diff
changeset

527 
else string_of_thm th)); 
22516  528 
change cache (Thmtab.update (th, cls)); cls 
529 
end 

530 
 SOME cls => cls) 

531 
 SOME cls => cls 

532 
end; 

15347  533 

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21602
diff
changeset

534 
fun pairname th = (PureThy.get_name_hint th, th); 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

535 

15872  536 
(**** Extract and Clausify theorems from a theory's claset and simpset ****) 
15347  537 

17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

538 
fun rules_of_claset cs = 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

539 
let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs 
19175  540 
val intros = safeIs @ hazIs 
18532  541 
val elims = map Classical.classical_rule (safeEs @ hazEs) 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

542 
in 
22130  543 
Output.debug (fn () => "rules_of_claset intros: " ^ Int.toString(length intros) ^ 
17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

544 
" elims: " ^ Int.toString(length elims)); 
20017
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

545 
map pairname (intros @ elims) 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

546 
end; 
15347  547 

17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

548 
fun rules_of_simpset ss = 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

549 
let val ({rules,...}, _) = rep_ss ss 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

550 
val simps = Net.entries rules 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

551 
in 
22130  552 
Output.debug (fn () => "rules_of_simpset: " ^ Int.toString(length simps)); 
553 
map (fn r => (#name r, #thm r)) simps 

17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

554 
end; 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

555 

21505  556 
fun claset_rules_of ctxt = rules_of_claset (local_claset_of ctxt); 
557 
fun simpset_rules_of ctxt = rules_of_simpset (local_simpset_of ctxt); 

19196
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset

558 

21505  559 
fun atpset_rules_of ctxt = map pairname (ResAtpset.get_atpset ctxt); 
20774  560 

15347  561 

22471  562 
(**** Translate a set of theorems into CNF ****) 
15347  563 

19894  564 
(* classical rules: works for both FOL and HOL *) 
565 
fun cnf_rules [] err_list = ([],err_list) 

20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

566 
 cnf_rules ((name,th) :: ths) err_list = 
19894  567 
let val (ts,es) = cnf_rules ths err_list 
22471  568 
in (cnf_axiom th :: ts,es) handle _ => (ts, (th::es)) end; 
15347  569 

19894  570 
fun pair_name_cls k (n, []) = [] 
571 
 pair_name_cls k (n, cls::clss) = (cls, (n,k)) :: pair_name_cls (k+1) (n, clss) 

20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

572 

19894  573 
fun cnf_rules_pairs_aux pairs [] = pairs 
574 
 cnf_rules_pairs_aux pairs ((name,th)::ths) = 

22471  575 
let val pairs' = (pair_name_cls 0 (name, cnf_axiom th)) @ pairs 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

576 
handle THM _ => pairs  ResClause.CLAUSE _ => pairs 
19894  577 
in cnf_rules_pairs_aux pairs' ths end; 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

578 

21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21254
diff
changeset

579 
(*The combination of rev and tail recursion preserves the original order*) 
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21254
diff
changeset

580 
fun cnf_rules_pairs l = cnf_rules_pairs_aux [] (rev l); 
19353  581 

19196
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset

582 

18198
95330fc0ea8d
 combined common CNF functions used by HOL and FOL axioms, the difference between conversion of HOL and FOL theorems only comes in when theorems are converted to ResClause.clause or ResHolClause.clause format.
mengj
parents:
18144
diff
changeset

583 
(**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****) 
15347  584 

20419  585 
(*Setup function: takes a theory and installs ALL known theorems into the clause cache*) 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset

586 

22516  587 
fun skolem_cache clause_cache th thy = #2 (skolem_cache_thm clause_cache th thy); 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset

588 

22516  589 
(*The cache can be kept smaller by inspecting the prop of each thm. Can ignore all that are 
590 
lambda_free, but then the individual theory caches become much bigger.*) 

21071  591 

22516  592 
fun clause_cache_setup thy = 
593 
fold (skolem_cache global_clause_cache) (map #2 (PureThy.all_thms_of thy)) thy; 

20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

594 

16563  595 

596 
(*** meson proof methods ***) 

597 

22516  598 
fun cnf_rules_of_ths ths = List.concat (map cnf_axiom ths); 
16563  599 

22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

600 
(*Expand all new*definitions of abstraction or Skolem functions in a proof state.*) 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

601 
fun is_absko (Const ("==", _) $ Free (a,_) $ u) = String.isPrefix "llabs_" a orelse String.isPrefix "sko_" a 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

602 
 is_absko _ = false; 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

603 

abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

604 
fun is_okdef xs (Const ("==", _) $ t $ u) = (*Definition of Free, not in certain terms*) 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

605 
is_Free t andalso not (member (op aconv) xs t) 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

606 
 is_okdef _ _ = false 
22724
3002683a6e0f
Fixes for proof reconstruction, especially involving abstractions and definitions
paulson
parents:
22691
diff
changeset

607 

22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

608 
fun expand_defs_tac st0 st = 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

609 
let val hyps0 = #hyps (rep_thm st0) 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

610 
val hyps = #hyps (crep_thm st) 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

611 
val newhyps = filter_out (member (op aconv) hyps0 o Thm.term_of) hyps 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

612 
val defs = filter (is_absko o Thm.term_of) newhyps 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

613 
val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs)) 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

614 
(map Thm.term_of hyps) 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

615 
val fixed = term_frees (concl_of st) @ 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

616 
foldl (gen_union (op aconv)) [] (map term_frees remaining_hyps) 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

617 
in Output.debug (fn _ => "expand_defs_tac: " ^ string_of_thm st); 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

618 
Output.debug (fn _ => " st0: " ^ string_of_thm st0); 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

619 
Output.debug (fn _ => " defs: " ^ commas (map string_of_cterm defs)); 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

620 
Seq.of_list [LocalDefs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

621 
end; 
22724
3002683a6e0f
Fixes for proof reconstruction, especially involving abstractions and definitions
paulson
parents:
22691
diff
changeset

622 

22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

623 

abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

624 
fun meson_general_tac ths i st0 = 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

625 
let val _ = Output.debug (fn () => "Meson called: " ^ cat_lines (map string_of_thm ths)) 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

626 
in (Meson.meson_claset_tac (cnf_rules_of_ths ths) HOL_cs i THEN expand_defs_tac st0) st0 end; 
22724
3002683a6e0f
Fixes for proof reconstruction, especially involving abstractions and definitions
paulson
parents:
22691
diff
changeset

627 

21588  628 
val meson_method_setup = Method.add_methods 
629 
[("meson", Method.thms_args (fn ths => 

22724
3002683a6e0f
Fixes for proof reconstruction, especially involving abstractions and definitions
paulson
parents:
22691
diff
changeset

630 
Method.SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ths)), 
21588  631 
"MESON resolution proof procedure")]; 
15347  632 

21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21096
diff
changeset

633 
(** Attribute for converting a theorem into clauses **) 
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

634 

22471  635 
fun meta_cnf_axiom th = map Meson.make_meta_clause (cnf_axiom th); 
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

636 

21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21096
diff
changeset

637 
fun clausify_rule (th,i) = List.nth (meta_cnf_axiom th, i) 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21096
diff
changeset

638 

7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21096
diff
changeset

639 
val clausify = Attrib.syntax (Scan.lift Args.nat 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21096
diff
changeset

640 
>> (fn i => Thm.rule_attribute (fn _ => fn th => clausify_rule (th, i)))); 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21096
diff
changeset

641 

21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

642 

0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

643 
(*** Converting a subgoal into negated conjecture clauses. ***) 
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

644 

0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

645 
val neg_skolemize_tac = EVERY' [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac]; 
22471  646 

647 
(*finish_cnf removes tautologies and functional reflexivity axioms, but by calling Thm.varifyT 

22644
f10465ee7aa2
Fixed the treatment of TVars in conjecture clauses (they are deleted, not frozen)
paulson
parents:
22596
diff
changeset

648 
it can introduce TVars, which are useless in conjecture clauses.*) 
f10465ee7aa2
Fixed the treatment of TVars in conjecture clauses (they are deleted, not frozen)
paulson
parents:
22596
diff
changeset

649 
val no_tvars = null o term_tvars o prop_of; 
f10465ee7aa2
Fixed the treatment of TVars in conjecture clauses (they are deleted, not frozen)
paulson
parents:
22596
diff
changeset

650 

22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

651 
val neg_clausify = filter no_tvars o Meson.finish_cnf o assume_abstract_list "subgoal" o make_clauses; 
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

652 

0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

653 
fun neg_conjecture_clauses st0 n = 
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

654 
let val st = Seq.hd (neg_skolemize_tac n st0) 
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

655 
val (params,_,_) = strip_context (Logic.nth_prem (n, Thm.prop_of st)) 
22516  656 
in (neg_clausify (Option.valOf (metahyps_thms n st)), params) end 
657 
handle Option => raise ERROR "unable to Skolemize subgoal"; 

21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

658 

0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

659 
(*Conversion of a subgoal to conjecture clauses. Each clause has 
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

660 
leading !!bound universal variables, to express generality. *) 
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

661 
val neg_clausify_tac = 
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

662 
neg_skolemize_tac THEN' 
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

663 
SUBGOAL 
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

664 
(fn (prop,_) => 
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

665 
let val ts = Logic.strip_assums_hyp prop 
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

666 
in EVERY1 
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

667 
[METAHYPS 
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

668 
(fn hyps => 
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

669 
(Method.insert_tac 
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

670 
(map forall_intr_vars (neg_clausify hyps)) 1)), 
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

671 
REPEAT_DETERM_N (length ts) o (etac thin_rl)] 
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

672 
end); 
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

673 

21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21096
diff
changeset

674 
(** The Skolemization attribute **) 
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

675 

0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

676 
fun conj2_rule (th1,th2) = conjI OF [th1,th2]; 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

677 

20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset

678 
(*Conjoin a list of theorems to form a single theorem*) 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset

679 
fun conj_rule [] = TrueI 
20445  680 
 conj_rule ths = foldr1 conj2_rule ths; 
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

681 

20419  682 
fun skolem_attr (Context.Theory thy, th) = 
22516  683 
let val (cls, thy') = skolem_cache_thm (ThmCache.get thy) th thy 
18728  684 
in (Context.Theory thy', conj_rule cls) end 
22724
3002683a6e0f
Fixes for proof reconstruction, especially involving abstractions and definitions
paulson
parents:
22691
diff
changeset

685 
 skolem_attr (context, th) = (context, th) 
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

686 

0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

687 
val setup_attrs = Attrib.add_attributes 
21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21096
diff
changeset

688 
[("skolem", Attrib.no_args skolem_attr, "skolemization of a theorem"), 
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

689 
("clausify", clausify, "conversion of theorem to clauses")]; 
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

690 

0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

691 
val setup_methods = Method.add_methods 
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

692 
[("neg_clausify", Method.no_args (Method.SIMPLE_METHOD' neg_clausify_tac), 
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

693 
"conversion of goal to conjecture clauses")]; 
21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21096
diff
changeset

694 

22516  695 
val setup = clause_cache_setup #> ThmCache.init #> setup_attrs #> setup_methods; 
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

696 

20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

697 
end; 