author  paulson 
Thu, 04 Oct 2007 12:32:58 +0200  
changeset 24827  646bdc51eb7d 
parent 24821  cc55041ca8ba 
child 24854  0ebcd575d3c6 
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 
24669  10 
val cnf_axiom: thm > thm list 
11 
val meta_cnf_axiom: thm > thm list 

12 
val pairname: thm > string * thm 

13 
val skolem_thm: thm > thm list 

14 
val cnf_rules_pairs: (string * thm) list > (thm * (string * int)) list 

15 
val cnf_rules_of_ths: thm list > thm list 

16 
val neg_clausify: thm list > thm list 

17 
val expand_defs_tac: thm > tactic 

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

19 
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

20 
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

21 
val simpset_rules_of: Proof.context > (string * thm) list (*FIXME DELETE*) 
21505  22 
val atpset_rules_of: Proof.context > (string * thm) list 
24669  23 
val meson_method_setup: theory > theory 
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

24 
val clause_cache_endtheory: theory > theory option 
24669  25 
val setup: theory > theory 
21505  26 
end; 
19196
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset

27 

24669  28 
structure ResAxioms: RES_AXIOMS = 
15997  29 
struct 
15347  30 

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

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

33 

20445  34 

15997  35 
(**** Transformation of Elimination Rules into FirstOrder Formulas****) 
15347  36 

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

37 
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

38 
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

39 

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

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

41 
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

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

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

46 
Thm.instantiate ([], [(cterm_of HOL.thy v, cfalse)]) th 
24669  47 
 v as Var(_, Type("prop",[])) => 
21430
77651b6d9d6c
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents:
21290
diff
changeset

48 
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

49 
 _ => th; 
15997  50 

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

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

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

53 

16009  54 
(**** SKOLEMIZATION BY INFERENCE (lcp) ****) 
55 

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

56 
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

57 
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

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

59 
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

60 
 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

61 
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

62 
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

63 

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

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

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

66 
fun declare_skofuns s th thy = 
21071  67 
let val nref = ref 0 
68 
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

69 
(*Existential: declare a Skolem function, then insert into body and continue*) 
24785  70 
let val cname = "sko_" ^ s ^ "_" ^ Int.toString (inc nref) 
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

71 
val args0 = term_frees xtp (*get the formal parameter list*) 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

72 
val Ts = map type_of args0 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

73 
val extraTs = rhs_extra_types (Ts > T) xtp 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

74 
val _ = if null extraTs then () else 
24785  75 
warning ("Skolemization: extra type vars: " ^ 
76 
commas_quote (map (Sign.string_of_typ thy) extraTs)); 

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

77 
val argsx = map (fn T => Free(gensym"vsk", T)) extraTs 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

78 
val args = argsx @ args0 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

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

80 
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

81 
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

82 
(*Forms a lambdaabstraction over the formal parameters*) 
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

83 
val _ = Output.debug (fn () => "declaring the constant " ^ cname) 
24771
6c7e94742afa
skofuns/absfuns: explicit markup as internal consts;
wenzelm
parents:
24742
diff
changeset

84 
val thy' = 
6c7e94742afa
skofuns/absfuns: explicit markup as internal consts;
wenzelm
parents:
24742
diff
changeset

85 
Sign.add_consts_authentic [Markup.property_internal] [(cname, cT, NoSyn)] thy 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

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

87 
val cdef = cname ^ "_def" 
24821
cc55041ca8ba
skolem_cache: ignore internal theorems  major speedup;
wenzelm
parents:
24785
diff
changeset

88 
val thy'' = Theory.add_defs_i true false [(cdef, equals cT $ c $ rhs)] thy' 
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

89 
handle ERROR _ => raise Clausify_failure thy' 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

90 
in dec_sko (subst_bound (list_comb(c,args), p)) 
24821
cc55041ca8ba
skolem_cache: ignore internal theorems  major speedup;
wenzelm
parents:
24785
diff
changeset

91 
(thy'', Thm.get_axiom_i thy'' (Sign.full_name thy'' cdef) :: axs) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

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

93 
 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

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

95 
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

96 
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

97 
 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

98 
 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

99 
 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

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

102 

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

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

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

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

106 
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

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

108 
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

109 
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

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

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

112 
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

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

114 
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

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

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

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

118 
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

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

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

121 
 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

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

123 
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

124 
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

125 
 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

126 
 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

127 
 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

128 
 dec_sko t defs = defs (*Do nothing otherwise*) 
20419  129 
in dec_sko (prop_of th) [] end; 
130 

131 

24827  132 
(**** REPLACING ABSTRACTIONS BY COMBINATORS ****) 
20419  133 

134 
(*Returns the vars of a theorem*) 

135 
fun vars_of_thm th = 

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

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

139 
local 

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

141 
val cx = hd (vars_of_thm fun_cong'); 

142 
val ty = typ_of (ctyp_of_term cx); 

20445  143 
val thy = theory_of_thm fun_cong; 
20419  144 
fun mkvar a = cterm_of thy (Var((a,0),ty)); 
145 
in 

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

147 
end; 

148 

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

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

150 
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

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

153 
case prop_of th of 
24669  154 
_ $ (Const ("op =", _) $ _ $ Abs (x,_,_)) => 
155 
strip_lambdas (n1) (freeze_thm (th RS xfun_cong x)) 

156 
 _ => th; 

20419  157 

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

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

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

160 
in if (t aconv Envir.eta_contract t) then () 
20419  161 
else error ("Eta redex in term: " ^ string_of_cterm ct) 
162 
end; 

163 

24669  164 
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

165 

24669  166 
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

167 

24827  168 
val abs_S = @{thm"abs_S"}; 
169 
val abs_K = @{thm"abs_K"}; 

170 
val abs_I = @{thm"abs_I"}; 

171 
val abs_B = @{thm"abs_B"}; 

172 
val abs_C = @{thm"abs_C"}; 

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

173 

24827  174 
val [f_B,g_B] = map (cterm_of @{theory}) (term_vars (prop_of abs_B)); 
175 
val [g_C,f_C] = map (cterm_of @{theory}) (term_vars (prop_of abs_C)); 

176 
val [f_S,g_S] = map (cterm_of @{theory}) (term_vars (prop_of abs_S)); 

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

177 

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

180 
let val Abs(x,_,body) = term_of ct 

181 
val thy = theory_of_cterm ct 

182 
val Type("fun",[xT,bodyT]) = typ_of (ctyp_of_term ct) 

183 
val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT 

184 
fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] abs_K 

185 
in 

186 
case body of 

187 
Const _ => makeK() 

188 
 Free _ => makeK() 

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

190 
 Bound 0 => instantiate' [SOME cxT] [] abs_I (*identity: I*) 

191 
 rator$rand => 

192 
if loose_bvar1 (rator,0) then (*C or S*) 

193 
if loose_bvar1 (rand,0) then (*S*) 

194 
let val crator = cterm_of thy (Abs(x,xT,rator)) 

195 
val crand = cterm_of thy (Abs(x,xT,rand)) 

196 
val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] abs_S 

197 
val (_,rhs) = Thm.dest_equals (cprop_of abs_S') 

198 
in 

199 
Thm.transitive abs_S' (Conv.binop_conv abstract rhs) 

200 
end 

201 
else (*C*) 

202 
let val crator = cterm_of thy (Abs(x,xT,rator)) 

203 
val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] abs_C 

204 
val (_,rhs) = Thm.dest_equals (cprop_of abs_C') 

205 
in 

206 
Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs) 

207 
end 

208 
else if loose_bvar1 (rand,0) then (*B or eta*) 

209 
if rand = Bound 0 then eta_conversion ct 

210 
else (*B*) 

211 
let val crand = cterm_of thy (Abs(x,xT,rand)) 

212 
val abs_B' = cterm_instantiate [(f_B, cterm_of thy rator),(g_B,crand)] abs_B 

213 
val (_,rhs) = Thm.dest_equals (cprop_of abs_B') 

214 
in 

215 
Thm.transitive abs_B' (Conv.arg_conv abstract rhs) 

216 
end 

217 
else makeK() 

218 
 _ => error "abstract: Bad term" 

219 
end; 

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

220 

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

24827  223 
fun combinators_aux ct = 
224 
if lambda_free (term_of ct) then reflexive ct 

225 
else 

226 
case term_of ct of 

227 
Abs _ => 

228 
let val _ = assert_eta_free ct; 

229 
val (cv,cta) = Thm.dest_abs NONE ct 

230 
val (v,Tv) = (dest_Free o term_of) cv 

231 
val _ = Output.debug (fn()=>" recursion: " ^ string_of_cterm cta); 

232 
val u_th = combinators_aux cta 

233 
val _ = Output.debug (fn()=>" returned " ^ string_of_thm u_th); 

234 
val cu = Thm.rhs_of u_th 

235 
val comb_eq = abstract (Thm.cabs cv cu) 

236 
in Output.debug (fn()=>" abstraction result: " ^ string_of_thm comb_eq); 

237 
(transitive (abstract_rule v cv u_th) comb_eq) end 

238 
 t1 $ t2 => 

239 
let val (ct1,ct2) = Thm.dest_comb ct 

240 
in combination (combinators_aux ct1) (combinators_aux ct2) end; 

241 

242 
fun combinators th = 

243 
if lambda_free (prop_of th) then th 

244 
else 

245 
let val _ = Output.debug (fn()=>"Conversion to combinators: " ^ string_of_thm th); 

246 
val th = Drule.eta_contraction_rule th 

247 
val eqth = combinators_aux (cprop_of th) 

248 
val _ = Output.debug (fn()=>"Conversion result: " ^ string_of_thm eqth); 

249 
in equal_elim eqth th end; 

16009  250 

251 
(*cterms are used throughout for efficiency*) 

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

252 
val cTrueprop = Thm.cterm_of HOL.thy HOLogic.Trueprop; 
16009  253 

254 
(*cterm version of mk_cTrueprop*) 

255 
fun c_mkTrueprop A = Thm.capply cTrueprop A; 

256 

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

258 
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

259 
fun c_variant_abs_multi (ct0, vars) = 
16009  260 
let val (cv,ct) = Thm.dest_abs NONE ct0 
261 
in c_variant_abs_multi (ct, cv::vars) end 

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

263 

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

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

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

266 
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

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

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

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

272 
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

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

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

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

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

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

282 
end; 
16009  283 

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

284 

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

285 
(*This will refer to the final version of theory ATP_Linkup.*) 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

286 
val atp_linkup_thy_ref = Theory.check_thy @{theory} 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

287 

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

288 
(*Transfer a theorem into theory ATP_Linkup.thy if it is not already 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

289 
inside that theory  because it's needed for Skolemization. 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

290 
If called while ATP_Linkup is being created, it will transfer to the 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

291 
current version. If called afterward, it will transfer to the final version.*) 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

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

293 
transfer (Theory.deref atp_linkup_thy_ref) th handle THM _ => th; 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

294 

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

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

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

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

298 
> transform_elim > zero_var_indexes > freeze_thm 
24300  299 
> Conv.fconv_rule ObjectLogic.atomize > Meson.make_nnf > strip_lambdas ~1; 
16009  300 

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

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

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

303 
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

304 

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

306 
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

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

308 
 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

309 

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

311 
fun flatten_name s = space_implode "_X" (NameSpace.explode s); 
21071  312 

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

313 
fun fake_name th = 
24669  314 
if PureThy.has_name_hint th then flatten_name (PureThy.get_name_hint th) 
22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

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

316 

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

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

318 
if PureThy.has_name_hint th then PureThy.get_name_hint th 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

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

320 

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

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

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

323 
let val nnfth = to_nnf th and s = fake_name th 
24827  324 
in Meson.make_cnf (skolem_of_nnf s nnfth) nnfth > map combinators > Meson.finish_cnf 
22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

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

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

327 

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

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

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

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

332 
(fn nnfth => 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

333 
let val _ = Output.debug (fn () => "skolemizing " ^ name_or_string th ^ ": ") 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

334 
val _ = Output.debug (fn () => string_of_thm nnfth) 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

335 
val s = fake_name th 
22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

336 
val (thy',defs) = declare_skofuns s nnfth thy 
20419  337 
val cnfs = Meson.make_cnf (map skolem_of_def defs) nnfth 
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

338 
val _ = Output.debug (fn () => Int.toString (length cnfs) ^ " clauses yielded") 
24827  339 
val cnfs' = map combinators cnfs 
340 
in (map Goal.close_result (Meson.finish_cnf cnfs'), thy') end 

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

341 
handle Clausify_failure thy_e => ([],thy_e) 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

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

343 
(try to_nnf th); 
16009  344 

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

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

346 
Skolem functions.*) 
22516  347 
structure ThmCache = TheoryDataFun 
22846  348 
( 
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

349 
type T = (thm list) Thmtab.table; 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

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

351 
fun copy tab : T = tab; 
22516  352 
val extend = copy; 
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

353 
fun merge _ (tab1, tab2) : T = Thmtab.merge (K true) (tab1, tab2); 
22846  354 
); 
22516  355 

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

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

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

358 
fun skolem_cache_thm th thy = 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

359 
case Thmtab.lookup (ThmCache.get thy) th of 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

360 
NONE => 
22471  361 
(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

362 
NONE => ([th],thy) 
24669  363 
 SOME (cls,thy') => 
24785  364 
(Output.debug (fn () => "skolem_cache_thm: " ^ Int.toString (length cls) ^ 
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

365 
" clauses inserted into cache: " ^ name_or_string th); 
24821
cc55041ca8ba
skolem_cache: ignore internal theorems  major speedup;
wenzelm
parents:
24785
diff
changeset

366 
(cls, ThmCache.map (Thmtab.update (th,cls)) thy'))) 
22471  367 
 SOME cls => (cls,thy); 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

368 

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

369 
(*Exported function to convert Isabelle theorems into axiom clauses*) 
22471  370 
fun cnf_axiom th = 
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

371 
let val thy = Theory.merge (Theory.deref atp_linkup_thy_ref, Thm.theory_of_thm th) 
22516  372 
in 
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

373 
case Thmtab.lookup (ThmCache.get thy) th of 
24821
cc55041ca8ba
skolem_cache: ignore internal theorems  major speedup;
wenzelm
parents:
24785
diff
changeset

374 
NONE => (Output.debug (fn () => "cnf_axiom: " ^ name_or_string th); 
cc55041ca8ba
skolem_cache: ignore internal theorems  major speedup;
wenzelm
parents:
24785
diff
changeset

375 
map Goal.close_result (skolem_thm th)) 
cc55041ca8ba
skolem_cache: ignore internal theorems  major speedup;
wenzelm
parents:
24785
diff
changeset

376 
 SOME cls => cls 
22516  377 
end; 
15347  378 

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

379 
fun pairname th = (PureThy.get_name_hint th, th); 
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 

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

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

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

387 
in 
22130  388 
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

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

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

391 
end; 
15347  392 

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

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

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

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

396 
in 
22130  397 
Output.debug (fn () => "rules_of_simpset: " ^ Int.toString(length simps)); 
398 
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

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

400 

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

403 

24042  404 
fun atpset_rules_of ctxt = map pairname (ResAtpset.get ctxt); 
20774  405 

15347  406 

22471  407 
(**** Translate a set of theorems into CNF ****) 
15347  408 

19894  409 
(* classical rules: works for both FOL and HOL *) 
410 
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

411 
 cnf_rules ((name,th) :: ths) err_list = 
19894  412 
let val (ts,es) = cnf_rules ths err_list 
22471  413 
in (cnf_axiom th :: ts,es) handle _ => (ts, (th::es)) end; 
15347  414 

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

417 

19894  418 
fun cnf_rules_pairs_aux pairs [] = pairs 
419 
 cnf_rules_pairs_aux pairs ((name,th)::ths) = 

22471  420 
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

421 
handle THM _ => pairs  ResClause.CLAUSE _ => pairs 
19894  422 
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

423 

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

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

425 
fun cnf_rules_pairs l = cnf_rules_pairs_aux [] (rev l); 
19353  426 

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

427 

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

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

20419  430 
(*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

431 

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

432 
val mark_skolemized = Sign.add_consts_i [("ResAxioms_endtheory", HOLogic.boolT, NoSyn)]; 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

433 

24827  434 
val max_lambda_nesting = 3; 
435 

436 
fun excessive_lambdas (f$t, k) = excessive_lambdas (f,k) orelse excessive_lambdas (t,k) 

437 
 excessive_lambdas (Abs(_,_,t), k) = k=0 orelse excessive_lambdas (t,k1) 

438 
 excessive_lambdas _ = false; 

439 

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

441 

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

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

444 
 excessive_lambdas_fm Ts t = 

445 
if is_formula_type (fastype_of1 (Ts, t)) 

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

447 
else excessive_lambdas (t, max_lambda_nesting); 

448 

449 
fun too_complex t = 

450 
Meson.too_many_clauses t orelse excessive_lambdas_fm [] t; 

451 

24821
cc55041ca8ba
skolem_cache: ignore internal theorems  major speedup;
wenzelm
parents:
24785
diff
changeset

452 
fun skolem_cache th thy = 
24827  453 
if PureThy.is_internal th orelse too_complex (prop_of th) then thy 
24821
cc55041ca8ba
skolem_cache: ignore internal theorems  major speedup;
wenzelm
parents:
24785
diff
changeset

454 
else #2 (skolem_cache_thm th thy); 
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

455 

24821
cc55041ca8ba
skolem_cache: ignore internal theorems  major speedup;
wenzelm
parents:
24785
diff
changeset

456 
val skolem_cache_theorems_of = Symtab.fold (fold skolem_cache o snd) o #2 o PureThy.theorems_of; 
cc55041ca8ba
skolem_cache: ignore internal theorems  major speedup;
wenzelm
parents:
24785
diff
changeset

457 
fun skolem_cache_node thy = skolem_cache_theorems_of thy thy; 
cc55041ca8ba
skolem_cache: ignore internal theorems  major speedup;
wenzelm
parents:
24785
diff
changeset

458 
fun skolem_cache_all thy = fold skolem_cache_theorems_of (thy :: Theory.ancestors_of thy) thy; 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset

459 

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

21071  462 

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

463 
(*The new constant is a hack to prevent multiple execution*) 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

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

465 
let val _ = Output.debug (fn () => "RexAxioms end theory action: " ^ Context.str_of_thy thy) 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

466 
in 
24821
cc55041ca8ba
skolem_cache: ignore internal theorems  major speedup;
wenzelm
parents:
24785
diff
changeset

467 
Option.map skolem_cache_node (try mark_skolemized thy) 
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

468 
end; 
16563  469 

470 
(*** meson proof methods ***) 

471 

22516  472 
fun cnf_rules_of_ths ths = List.concat (map cnf_axiom ths); 
16563  473 

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

474 
(*Expand all new*definitions of abstraction or Skolem functions in a proof state.*) 
24827  475 
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

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

477 

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

478 
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

479 
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

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

481 

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

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

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

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

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

488 
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

489 
val defs = filter (is_absko o Thm.term_of) newhyps 
24669  490 
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

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

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

493 
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

494 
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

495 
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

496 
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

497 
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

498 
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 = 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

502 
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

503 
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

504 

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

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

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

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

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

511 

22471  512 
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

513 

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

514 
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

515 

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

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

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

518 

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

519 

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

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

521 

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

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

525 
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

526 
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

527 

24300  528 
val neg_clausify = 
24827  529 
filter no_tvars o Meson.finish_cnf o map combinators o Meson.make_clauses; 
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

530 

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

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

532 
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

533 
val (params,_,_) = strip_context (Logic.nth_prem (n, Thm.prop_of st)) 
22516  534 
in (neg_clausify (Option.valOf (metahyps_thms n st)), params) end 
535 
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

536 

24669  537 
(*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

538 
leading !!bound universal variables, to express generality. *) 
24669  539 
val neg_clausify_tac = 
540 
neg_skolemize_tac THEN' 

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

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

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

543 
let val ts = Logic.strip_assums_hyp prop 
24669  544 
in EVERY1 
545 
[METAHYPS 

546 
(fn hyps => 

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

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

548 
(map forall_intr_vars (neg_clausify hyps)) 1)), 
24669  549 
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

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

551 

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

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

553 

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

554 
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

555 

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

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

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

559 

20419  560 
fun skolem_attr (Context.Theory thy, th) = 
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

561 
let val (cls, thy') = skolem_cache_thm th thy 
18728  562 
in (Context.Theory thy', conj_rule cls) end 
22724
3002683a6e0f
Fixes for proof reconstruction, especially involving abstractions and definitions
paulson
parents:
22691
diff
changeset

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

564 

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

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

566 
[("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

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

568 

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

569 
val setup_methods = Method.add_methods 
24669  570 
[("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

571 
"conversion of goal to conjecture clauses")]; 
24669  572 

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

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

574 

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

575 
end; 