author  wenzelm 
Sun, 01 Mar 2009 23:36:12 +0100  
changeset 30190  479806475f3c 
parent 29579  cb520b766e00 
child 30280  eb98b49ef835 
permissions  rwrr 
15347  1 
(* Author: Jia Meng, Cambridge University Computer Laboratory 
2 

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

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

15997  6 
signature RES_AXIOMS = 
21505  7 
sig 
27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

8 
val cnf_axiom: theory > thm > thm list 
24669  9 
val pairname: thm > string * thm 
27184  10 
val multi_base_blacklist: string list 
25243  11 
val bad_for_atp: thm > bool 
25761  12 
val type_has_empty_sort: typ > bool 
27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

13 
val cnf_rules_pairs: theory > (string * thm) list > (thm * (string * int)) list 
24669  14 
val neg_clausify: thm list > thm list 
15 
val expand_defs_tac: thm > tactic 

24827  16 
val combinators: thm > thm 
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

17 
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

18 
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

19 
val simpset_rules_of: Proof.context > (string * thm) list (*FIXME DELETE*) 
21505  20 
val atpset_rules_of: Proof.context > (string * thm) list 
25256
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset

21 
val suppress_endtheory: bool ref (*for emergency use where endtheory causes problems*) 
24669  22 
val setup: theory > theory 
21505  23 
end; 
19196
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset

24 

24669  25 
structure ResAxioms: RES_AXIOMS = 
15997  26 
struct 
15347  27 

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

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

30 

25761  31 
fun type_has_empty_sort (TFree (_, [])) = true 
32 
 type_has_empty_sort (TVar (_, [])) = true 

33 
 type_has_empty_sort (Type (_, Ts)) = exists type_has_empty_sort Ts 

34 
 type_has_empty_sort _ = false; 

27184  35 

28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

36 

15997  37 
(**** Transformation of Elimination Rules into FirstOrder Formulas****) 
15347  38 

29064  39 
val cfalse = cterm_of @{theory HOL} HOLogic.false_const; 
40 
val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const); 

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

41 

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

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

43 
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

44 
conclusion variable to False.*) 
16009  45 
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

46 
case concl_of th of (*conclusion variable*) 
24669  47 
Const("Trueprop",_) $ (v as Var(_,Type("bool",[]))) => 
29064  48 
Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th 
24669  49 
 v as Var(_, Type("prop",[])) => 
29064  50 
Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th 
21430
77651b6d9d6c
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents:
21290
diff
changeset

51 
 _ => th; 
15997  52 

24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

53 
(*To enforce singlethreading*) 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

54 
exception Clausify_failure of theory; 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

55 

28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

56 

16009  57 
(**** SKOLEMIZATION BY INFERENCE (lcp) ****) 
58 

24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

59 
fun rhs_extra_types lhsT rhs = 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

60 
let val lhs_vars = Term.add_tfreesT lhsT [] 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

61 
fun add_new_TFrees (TFree v) = 
24821
cc55041ca8ba
skolem_cache: ignore internal theorems  major speedup;
wenzelm
parents:
24785
diff
changeset

62 
if member (op =) lhs_vars v then I else insert (op =) (TFree v) 
cc55041ca8ba
skolem_cache: ignore internal theorems  major speedup;
wenzelm
parents:
24785
diff
changeset

63 
 add_new_TFrees _ = I 
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

64 
val rhs_consts = fold_aterms (fn Const c => insert (op =) c  _ => I) rhs [] 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

65 
in fold (#2 #> Term.fold_atyps add_new_TFrees) rhs_consts [] end; 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

66 

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

67 
(*Traverse a theorem, declaring Skolem function definitions. String s is the suggested 
27174
c2c484480f40
declare_skofuns/skolem: canonical argument order;
wenzelm
parents:
26939
diff
changeset

68 
prefix for the Skolem constant.*) 
c2c484480f40
declare_skofuns/skolem: canonical argument order;
wenzelm
parents:
26939
diff
changeset

69 
fun declare_skofuns s th = 
c2c484480f40
declare_skofuns/skolem: canonical argument order;
wenzelm
parents:
26939
diff
changeset

70 
let 
c2c484480f40
declare_skofuns/skolem: canonical argument order;
wenzelm
parents:
26939
diff
changeset

71 
val nref = ref 0 
c2c484480f40
declare_skofuns/skolem: canonical argument order;
wenzelm
parents:
26939
diff
changeset

72 
fun dec_sko (Const ("Ex",_) $ (xtp as Abs (_, T, p))) (axs, thy) = 
c2c484480f40
declare_skofuns/skolem: canonical argument order;
wenzelm
parents:
26939
diff
changeset

73 
(*Existential: declare a Skolem function, then insert into body and continue*) 
c2c484480f40
declare_skofuns/skolem: canonical argument order;
wenzelm
parents:
26939
diff
changeset

74 
let 
c2c484480f40
declare_skofuns/skolem: canonical argument order;
wenzelm
parents:
26939
diff
changeset

75 
val cname = "sko_" ^ s ^ "_" ^ Int.toString (inc nref) 
29265
5b4247055bd7
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents:
29064
diff
changeset

76 
val args0 = OldTerm.term_frees xtp (*get the formal parameter list*) 
27174
c2c484480f40
declare_skofuns/skolem: canonical argument order;
wenzelm
parents:
26939
diff
changeset

77 
val Ts = map type_of args0 
c2c484480f40
declare_skofuns/skolem: canonical argument order;
wenzelm
parents:
26939
diff
changeset

78 
val extraTs = rhs_extra_types (Ts > T) xtp 
c2c484480f40
declare_skofuns/skolem: canonical argument order;
wenzelm
parents:
26939
diff
changeset

79 
val argsx = map (fn T => Free (gensym "vsk", T)) extraTs 
c2c484480f40
declare_skofuns/skolem: canonical argument order;
wenzelm
parents:
26939
diff
changeset

80 
val args = argsx @ args0 
c2c484480f40
declare_skofuns/skolem: canonical argument order;
wenzelm
parents:
26939
diff
changeset

81 
val cT = extraTs > Ts > T 
c2c484480f40
declare_skofuns/skolem: canonical argument order;
wenzelm
parents:
26939
diff
changeset

82 
val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp) 
c2c484480f40
declare_skofuns/skolem: canonical argument order;
wenzelm
parents:
26939
diff
changeset

83 
(*Forms a lambdaabstraction over the formal parameters*) 
28110  84 
val (c, thy') = 
28965  85 
Sign.declare_const [Markup.property_internal] ((Binding.name cname, cT), NoSyn) thy 
27174
c2c484480f40
declare_skofuns/skolem: canonical argument order;
wenzelm
parents:
26939
diff
changeset

86 
val cdef = cname ^ "_def" 
29579  87 
val thy'' = Theory.add_defs_i true false [(Binding.name cdef, Logic.mk_equals (c, rhs))] thy' 
28965  88 
val ax = Thm.axiom thy'' (Sign.full_bname thy'' cdef) 
27174
c2c484480f40
declare_skofuns/skolem: canonical argument order;
wenzelm
parents:
26939
diff
changeset

89 
in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end 
c2c484480f40
declare_skofuns/skolem: canonical argument order;
wenzelm
parents:
26939
diff
changeset

90 
 dec_sko (Const ("All", _) $ (xtp as Abs (a, T, p))) thx = 
c2c484480f40
declare_skofuns/skolem: canonical argument order;
wenzelm
parents:
26939
diff
changeset

91 
(*Universal quant: insert a free variable into body and continue*) 
29270
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29265
diff
changeset

92 
let val fname = Name.variant (OldTerm.add_term_names (p, [])) a 
27174
c2c484480f40
declare_skofuns/skolem: canonical argument order;
wenzelm
parents:
26939
diff
changeset

93 
in dec_sko (subst_bound (Free (fname, T), p)) thx end 
c2c484480f40
declare_skofuns/skolem: canonical argument order;
wenzelm
parents:
26939
diff
changeset

94 
 dec_sko (Const ("op &", _) $ p $ q) thx = dec_sko q (dec_sko p thx) 
c2c484480f40
declare_skofuns/skolem: canonical argument order;
wenzelm
parents:
26939
diff
changeset

95 
 dec_sko (Const ("op ", _) $ p $ q) thx = dec_sko q (dec_sko p thx) 
c2c484480f40
declare_skofuns/skolem: canonical argument order;
wenzelm
parents:
26939
diff
changeset

96 
 dec_sko (Const ("Trueprop", _) $ p) thx = dec_sko p thx 
c2c484480f40
declare_skofuns/skolem: canonical argument order;
wenzelm
parents:
26939
diff
changeset

97 
 dec_sko t thx = thx (*Do nothing otherwise*) 
c2c484480f40
declare_skofuns/skolem: canonical argument order;
wenzelm
parents:
26939
diff
changeset

98 
in fn thy => dec_sko (Thm.prop_of th) ([], thy) end; 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

99 

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

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

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

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

103 
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

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

105 
let val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*) 
29265
5b4247055bd7
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents:
29064
diff
changeset

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

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

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

109 
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

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

111 
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

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

113 
(*Forms a lambdaabstraction over the formal parameters*) 
27330  114 
val def = Logic.mk_equals (c, rhs) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

115 
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

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

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

118 
 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

119 
(*Universal quant: insert a free variable into body and continue*) 
29270
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29265
diff
changeset

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

121 
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

122 
 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

123 
 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

124 
 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

125 
 dec_sko t defs = defs (*Do nothing otherwise*) 
20419  126 
in dec_sko (prop_of th) [] end; 
127 

128 

24827  129 
(**** REPLACING ABSTRACTIONS BY COMBINATORS ****) 
20419  130 

131 
(*Returns the vars of a theorem*) 

132 
fun vars_of_thm th = 

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

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

136 
local 

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

138 
val cx = hd (vars_of_thm fun_cong'); 

139 
val ty = typ_of (ctyp_of_term cx); 

20445  140 
val thy = theory_of_thm fun_cong; 
20419  141 
fun mkvar a = cterm_of thy (Var((a,0),ty)); 
142 
in 

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

144 
end; 

145 

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

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

147 
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

148 
fun strip_lambdas 0 th = th 
24669  149 
 strip_lambdas n th = 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

150 
case prop_of th of 
24669  151 
_ $ (Const ("op =", _) $ _ $ Abs (x,_,_)) => 
152 
strip_lambdas (n1) (freeze_thm (th RS xfun_cong x)) 

153 
 _ => th; 

20419  154 

24669  155 
val lambda_free = not o Term.has_abs; 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

156 

24669  157 
val monomorphic = not o Term.exists_type (Term.exists_subtype Term.is_TVar); 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

158 

29265
5b4247055bd7
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents:
29064
diff
changeset

159 
val [f_B,g_B] = map (cterm_of (the_context ())) (OldTerm.term_vars (prop_of @{thm abs_B})); 
5b4247055bd7
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents:
29064
diff
changeset

160 
val [g_C,f_C] = map (cterm_of (the_context ())) (OldTerm.term_vars (prop_of @{thm abs_C})); 
5b4247055bd7
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents:
29064
diff
changeset

161 
val [f_S,g_S] = map (cterm_of (the_context ())) (OldTerm.term_vars (prop_of @{thm abs_S})); 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

162 

24827  163 
(*FIXME: requires more use of cterm constructors*) 
164 
fun abstract ct = 

28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

165 
let 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

166 
val thy = theory_of_cterm ct 
25256
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset

167 
val Abs(x,_,body) = term_of ct 
24827  168 
val Type("fun",[xT,bodyT]) = typ_of (ctyp_of_term ct) 
169 
val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT 

27184  170 
fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] @{thm abs_K} 
24827  171 
in 
172 
case body of 

173 
Const _ => makeK() 

174 
 Free _ => makeK() 

175 
 Var _ => makeK() (*though Var isn't expected*) 

27184  176 
 Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*) 
24827  177 
 rator$rand => 
27184  178 
if loose_bvar1 (rator,0) then (*C or S*) 
27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

179 
if loose_bvar1 (rand,0) then (*S*) 
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

180 
let val crator = cterm_of thy (Abs(x,xT,rator)) 
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

181 
val crand = cterm_of thy (Abs(x,xT,rand)) 
27184  182 
val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S} 
183 
val (_,rhs) = Thm.dest_equals (cprop_of abs_S') 

27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

184 
in 
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

185 
Thm.transitive abs_S' (Conv.binop_conv abstract rhs) 
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

186 
end 
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

187 
else (*C*) 
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

188 
let val crator = cterm_of thy (Abs(x,xT,rator)) 
27184  189 
val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] @{thm abs_C} 
190 
val (_,rhs) = Thm.dest_equals (cprop_of abs_C') 

27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

191 
in 
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

192 
Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs) 
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

193 
end 
27184  194 
else if loose_bvar1 (rand,0) then (*B or eta*) 
27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

195 
if rand = Bound 0 then eta_conversion ct 
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

196 
else (*B*) 
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

197 
let val crand = cterm_of thy (Abs(x,xT,rand)) 
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

198 
val crator = cterm_of thy rator 
27184  199 
val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B} 
200 
val (_,rhs) = Thm.dest_equals (cprop_of abs_B') 

27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

201 
in 
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

202 
Thm.transitive abs_B' (Conv.arg_conv abstract rhs) 
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

203 
end 
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

204 
else makeK() 
24827  205 
 _ => error "abstract: Bad term" 
206 
end; 

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

207 

20419  208 
(*Traverse a theorem, declaring abstraction function definitions. String s is the suggested 
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

209 
prefix for the constants.*) 
24827  210 
fun combinators_aux ct = 
211 
if lambda_free (term_of ct) then reflexive ct 

212 
else 

213 
case term_of ct of 

214 
Abs _ => 

27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

215 
let val (cv,cta) = Thm.dest_abs NONE ct 
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

216 
val (v,Tv) = (dest_Free o term_of) cv 
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

217 
val u_th = combinators_aux cta 
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

218 
val cu = Thm.rhs_of u_th 
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

219 
val comb_eq = abstract (Thm.cabs cv cu) 
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

220 
in transitive (abstract_rule v cv u_th) comb_eq end 
24827  221 
 t1 $ t2 => 
27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

222 
let val (ct1,ct2) = Thm.dest_comb ct 
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

223 
in combination (combinators_aux ct1) (combinators_aux ct2) end; 
27184  224 

24827  225 
fun combinators th = 
27184  226 
if lambda_free (prop_of th) then th 
24827  227 
else 
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

228 
let val th = Drule.eta_contraction_rule th 
27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

229 
val eqth = combinators_aux (cprop_of th) 
25256
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset

230 
in equal_elim eqth th end 
27184  231 
handle THM (msg,_,_) => 
26928  232 
(warning ("Error in the combinator translation of " ^ Display.string_of_thm th); 
25256
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset

233 
warning (" Exception message: " ^ msg); 
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset

234 
TrueI); (*A type variable of sort {} will cause make abstraction fail.*) 
16009  235 

236 
(*cterms are used throughout for efficiency*) 

29064  237 
val cTrueprop = Thm.cterm_of @{theory HOL} HOLogic.Trueprop; 
16009  238 

239 
(*cterm version of mk_cTrueprop*) 

240 
fun c_mkTrueprop A = Thm.capply cTrueprop A; 

241 

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

243 
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

244 
fun c_variant_abs_multi (ct0, vars) = 
16009  245 
let val (cv,ct) = Thm.dest_abs NONE ct0 
246 
in c_variant_abs_multi (ct, cv::vars) end 

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

248 

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

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

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

251 
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

252 
fun skolem_of_def def = 
22902
ac833b4bb7ee
moved some Drule operations to Thm (see more_thm.ML);
wenzelm
parents:
22846
diff
changeset

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

255 
val (chilbert,cabs) = Thm.dest_comb ch 
26627
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26618
diff
changeset

256 
val thy = Thm.theory_of_cterm chilbert 
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26618
diff
changeset

257 
val t = Thm.term_of chilbert 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

258 
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

259 
 _ => raise THM ("skolem_of_def: expected Eps", 0, [def]) 
22596  260 
val cex = Thm.cterm_of thy (HOLogic.exists_const T) 
16009  261 
val ex_tm = c_mkTrueprop (Thm.capply cex cabs) 
262 
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

263 
fun tacf [prem] = rewrite_goals_tac [def] THEN rtac (prem RS someI_ex) 1 
23352  264 
in Goal.prove_internal [ex_tm] conc tacf 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

265 
> forall_intr_list frees 
26653  266 
> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*) 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

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

268 
end; 
16009  269 

24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

270 

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

271 
(*Converts an Isabelle theorem (intro, elim or simp format, even higherorder) into NNF.*) 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24854
diff
changeset

272 
fun to_nnf th ctxt0 = 
27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

273 
let val th1 = th > transform_elim > zero_var_indexes 
27184  274 
val ((_,[th2]),ctxt) = Variable.import_thms true [th1] ctxt0 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24854
diff
changeset

275 
val th3 = th2 > Conv.fconv_rule ObjectLogic.atomize > Meson.make_nnf > strip_lambdas ~1 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24854
diff
changeset

276 
in (th3, ctxt) end; 
16009  277 

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

278 
(*Generate Skolem functions for a theorem supplied in nnf*) 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24854
diff
changeset

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

280 
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

281 

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

283 
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

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

286 

25007  287 

27184  288 
(*** Blacklisting (duplicated in ResAtp?) ***) 
25007  289 

290 
val max_lambda_nesting = 3; 

27184  291 

25007  292 
fun excessive_lambdas (f$t, k) = excessive_lambdas (f,k) orelse excessive_lambdas (t,k) 
293 
 excessive_lambdas (Abs(_,_,t), k) = k=0 orelse excessive_lambdas (t,k1) 

294 
 excessive_lambdas _ = false; 

295 

296 
fun is_formula_type T = (T = HOLogic.boolT orelse T = propT); 

297 

298 
(*Don't count nested lambdas at the level of formulas, as they are quantifiers*) 

299 
fun excessive_lambdas_fm Ts (Abs(_,T,t)) = excessive_lambdas_fm (T::Ts) t 

300 
 excessive_lambdas_fm Ts t = 

301 
if is_formula_type (fastype_of1 (Ts, t)) 

302 
then exists (excessive_lambdas_fm Ts) (#2 (strip_comb t)) 

303 
else excessive_lambdas (t, max_lambda_nesting); 

304 

25256
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset

305 
(*The max apply_depth of any metis call in MetisExamples (on 31102007) was 11.*) 
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset

306 
val max_apply_depth = 15; 
27184  307 

25256
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset

308 
fun apply_depth (f$t) = Int.max (apply_depth f, apply_depth t + 1) 
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset

309 
 apply_depth (Abs(_,_,t)) = apply_depth t 
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset

310 
 apply_depth _ = 0; 
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset

311 

27184  312 
fun too_complex t = 
313 
apply_depth t > max_apply_depth orelse 

26562
9d25ef112cf6
* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
paulson
parents:
25761
diff
changeset

314 
Meson.too_many_clauses NONE t orelse 
25256
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset

315 
excessive_lambdas_fm [] t; 
27184  316 

25243  317 
fun is_strange_thm th = 
318 
case head_of (concl_of th) of 

319 
Const (a,_) => (a <> "Trueprop" andalso a <> "==") 

320 
 _ => false; 

321 

27184  322 
fun bad_for_atp th = 
27865
27a8ad9612a3
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents:
27809
diff
changeset

323 
Thm.is_internal th 
27184  324 
orelse too_complex (prop_of th) 
325 
orelse exists_type type_has_empty_sort (prop_of th) 

25761  326 
orelse is_strange_thm th; 
25243  327 

25007  328 
val multi_base_blacklist = 
25256
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset

329 
["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm", 
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset

330 
"cases","ext_cases"]; (*FIXME: put other record thms here, or use the "Internal" marker*) 
25007  331 

21071  332 
(*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

333 
fun flatten_name s = space_implode "_X" (NameSpace.explode s); 
21071  334 

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

335 
fun fake_name th = 
27865
27a8ad9612a3
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents:
27809
diff
changeset

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

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

338 

24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

339 
fun name_or_string th = 
27865
27a8ad9612a3
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents:
27809
diff
changeset

340 
if Thm.has_name_hint th then Thm.get_name_hint th 
26928  341 
else Display.string_of_thm th; 
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

342 

27184  343 
(*Skolemize a named theorem, with Skolem functions as additional premises.*) 
344 
fun skolem_thm (s, th) = 

345 
if member (op =) multi_base_blacklist (Sign.base_name s) orelse bad_for_atp th then [] 

346 
else 

347 
let 

348 
val ctxt0 = Variable.thm_context th 

349 
val (nnfth, ctxt1) = to_nnf th ctxt0 

350 
val (cnfs, ctxt2) = Meson.make_cnf (assume_skolem_of_def s nnfth) nnfth ctxt1 

351 
in cnfs > map combinators > Variable.export ctxt2 ctxt0 > Meson.finish_cnf end 

352 
handle THM _ => []; 

353 

24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

354 
(*The cache prevents repeated clausification of a theorem, and also repeated declaration of 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

355 
Skolem functions.*) 
22516  356 
structure ThmCache = TheoryDataFun 
22846  357 
( 
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

358 
type T = thm list Thmtab.table * unit Symtab.table; 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

359 
val empty = (Thmtab.empty, Symtab.empty); 
26618  360 
val copy = I; 
361 
val extend = I; 

27184  362 
fun merge _ ((cache1, seen1), (cache2, seen2)) : T = 
363 
(Thmtab.merge (K true) (cache1, cache2), Symtab.merge (K true) (seen1, seen2)); 

22846  364 
); 
22516  365 

27184  366 
val lookup_cache = Thmtab.lookup o #1 o ThmCache.get; 
367 
val already_seen = Symtab.defined o #2 o ThmCache.get; 

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

368 

27184  369 
val update_cache = ThmCache.map o apfst o Thmtab.update; 
370 
fun mark_seen name = ThmCache.map (apsnd (Symtab.update (name, ()))); 

25007  371 

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

372 
(*Exported function to convert Isabelle theorems into axiom clauses*) 
27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

373 
fun cnf_axiom thy th0 = 
27184  374 
let val th = Thm.transfer thy th0 in 
375 
case lookup_cache thy th of 

376 
NONE => map Thm.close_derivation (skolem_thm (fake_name th, th)) 

377 
 SOME cls => cls 

22516  378 
end; 
15347  379 

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

380 

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

27865
27a8ad9612a3
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents:
27809
diff
changeset

383 
fun pairname th = (Thm.get_name_hint th, th); 
27184  384 

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

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

386 
let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs 
19175  387 
val intros = safeIs @ hazIs 
18532  388 
val elims = map Classical.classical_rule (safeEs @ hazEs) 
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

389 
in map pairname (intros @ elims) end; 
15347  390 

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

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

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

393 
val simps = Net.entries rules 
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

394 
in map (fn r => (#name r, #thm r)) simps end; 
17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

395 

21505  396 
fun claset_rules_of ctxt = rules_of_claset (local_claset_of ctxt); 
397 
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

398 

24042  399 
fun atpset_rules_of ctxt = map pairname (ResAtpset.get ctxt); 
20774  400 

15347  401 

22471  402 
(**** Translate a set of theorems into CNF ****) 
15347  403 

19894  404 
fun pair_name_cls k (n, []) = [] 
405 
 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

406 

27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

407 
fun cnf_rules_pairs_aux _ pairs [] = pairs 
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

408 
 cnf_rules_pairs_aux thy pairs ((name,th)::ths) = 
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

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

410 
handle THM _ => pairs  ResClause.CLAUSE _ => pairs 
27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

411 
in cnf_rules_pairs_aux thy pairs' ths end; 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

412 

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

413 
(*The combination of rev and tail recursion preserves the original order*) 
27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

414 
fun cnf_rules_pairs thy l = cnf_rules_pairs_aux thy [] (rev l); 
19353  415 

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

416 

27184  417 
(**** Convert all facts of the theory into clauses (ResClause.clause, or ResHolClause.clause) ****) 
15347  418 

28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

419 
local 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

420 

26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

421 
fun skolem_def (name, th) thy = 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

422 
let val ctxt0 = Variable.thm_context th in 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

423 
(case try (to_nnf th) ctxt0 of 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

424 
NONE => (NONE, thy) 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

425 
 SOME (nnfth, ctxt1) => 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

426 
let val (defs, thy') = declare_skofuns (flatten_name name) nnfth thy 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

427 
in (SOME (th, ctxt0, ctxt1, nnfth, defs), thy') end) 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

428 
end; 
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

429 

28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

430 
fun skolem_cnfs (th, ctxt0, ctxt1, nnfth, defs) = 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

431 
let 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

432 
val (cnfs, ctxt2) = Meson.make_cnf (map skolem_of_def defs) nnfth ctxt1; 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

433 
val cnfs' = cnfs 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

434 
> map combinators 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

435 
> Variable.export ctxt2 ctxt0 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

436 
> Meson.finish_cnf 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

437 
> map Thm.close_derivation; 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

438 
in (th, cnfs') end; 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

439 

26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

440 
in 
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

441 

27184  442 
fun saturate_skolem_cache thy = 
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

443 
let 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

444 
val new_facts = (PureThy.facts_of thy, []) > Facts.fold_static (fn (name, ths) => 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

445 
if already_seen thy name then I else cons (name, ths)); 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

446 
val new_thms = (new_facts, []) > fold (fn (name, ths) => 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

447 
if member (op =) multi_base_blacklist (Sign.base_name name) then I 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

448 
else fold_index (fn (i, th) => 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

449 
if bad_for_atp th orelse is_some (lookup_cache thy th) then I 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

450 
else cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths); 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

451 
in 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

452 
if null new_facts then NONE 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

453 
else 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

454 
let 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

455 
val (defs, thy') = thy 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

456 
> fold (mark_seen o #1) new_facts 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

457 
> fold_map skolem_def (sort_distinct (Thm.thm_ord o pairself snd) new_thms) 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

458 
>> map_filter I; 
29368  459 
val cache_entries = Par_List.map skolem_cnfs defs; 
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

460 
in SOME (fold update_cache cache_entries thy') end 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

461 
end; 
27184  462 

28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

463 
end; 
24854  464 

27184  465 
val suppress_endtheory = ref false; 
466 

467 
fun clause_cache_endtheory thy = 

468 
if ! suppress_endtheory then NONE 

469 
else saturate_skolem_cache thy; 

470 

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

471 

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

21071  474 

27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

475 

16563  476 
(*** meson proof methods ***) 
477 

28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

478 
(*Expand all new definitions of abstraction or Skolem functions in a proof state.*) 
24827  479 
fun is_absko (Const ("==", _) $ Free (a,_) $ u) = String.isPrefix "sko_" a 
22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

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

481 

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

482 
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

483 
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

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

485 

24215  486 
(*This function tries to cope with open locales, which introduce hypotheses of the form 
487 
Free == t, conjecture clauses, which introduce various hypotheses, and also definitions 

24827  488 
of sko_ functions. *) 
22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

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

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

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

492 
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

493 
val defs = filter (is_absko o Thm.term_of) newhyps 
24669  494 
val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs)) 
22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

495 
(map Thm.term_of hyps) 
29265
5b4247055bd7
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents:
29064
diff
changeset

496 
val fixed = OldTerm.term_frees (concl_of st) @ 
30190  497 
List.foldl (gen_union (op aconv)) [] (map OldTerm.term_frees remaining_hyps) 
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

498 
in Seq.of_list [LocalDefs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end; 
22724
3002683a6e0f
Fixes for proof reconstruction, especially involving abstractions and definitions
paulson
parents:
22691
diff
changeset

499 

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

500 

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

501 
fun meson_general_tac ths i st0 = 
27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

502 
let 
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

503 
val thy = Thm.theory_of_thm st0 
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

504 
in (Meson.meson_claset_tac (maps (cnf_axiom thy) 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

505 

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

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

508 
Method.SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ths)), 
21588  509 
"MESON resolution proof procedure")]; 
15347  510 

27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

511 

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

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

513 

24300  514 
val neg_skolemize_tac = EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, Meson.skolemize_tac]; 
22471  515 

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

516 
fun neg_clausify sts = 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24854
diff
changeset

517 
sts > Meson.make_clauses > map combinators > Meson.finish_cnf; 
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

518 

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

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

520 
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

521 
val (params,_,_) = strip_context (Logic.nth_prem (n, Thm.prop_of st)) 
27187  522 
in (neg_clausify (the (metahyps_thms n st)), params) end 
523 
handle Option => error "unable to Skolemize subgoal"; 

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

524 

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

526 
leading !!bound universal variables, to express generality. *) 
24669  527 
val neg_clausify_tac = 
528 
neg_skolemize_tac THEN' 

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

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

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

531 
let val ts = Logic.strip_assums_hyp prop 
24669  532 
in EVERY1 
533 
[METAHYPS 

534 
(fn hyps => 

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

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

536 
(map forall_intr_vars (neg_clausify hyps)) 1)), 
24669  537 
REPEAT_DETERM_N (length ts) o (etac thin_rl)] 
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

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

539 

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

540 
val setup_methods = Method.add_methods 
24669  541 
[("neg_clausify", Method.no_args (Method.SIMPLE_METHOD' neg_clausify_tac), 
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

542 
"conversion of goal to conjecture clauses")]; 
24669  543 

27184  544 

545 
(** Attribute for converting a theorem into clauses **) 

546 

27809
a1e409db516b
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27330
diff
changeset

547 
val clausify = Attrib.syntax (Scan.lift OuterParse.nat 
27184  548 
>> (fn i => Thm.rule_attribute (fn context => fn th => 
549 
Meson.make_meta_clause (nth (cnf_axiom (Context.theory_of context) th) i)))); 

550 

551 
val setup_attrs = Attrib.add_attributes 

552 
[("clausify", clausify, "conversion of theorem to clauses")]; 

553 

554 

555 

556 
(** setup **) 

557 

558 
val setup = 

559 
meson_method_setup #> 

560 
setup_methods #> 

561 
setup_attrs #> 

562 
perhaps saturate_skolem_cache #> 

563 
Theory.at_end clause_cache_endtheory; 

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

564 

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

565 
end; 