author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 24827  646bdc51eb7d 
child 24937  340523598914 
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 

24854  13 
val multi_base_blacklist: string list 
24669  14 
val skolem_thm: thm > thm list 
15 
val cnf_rules_pairs: (string * thm) list > (thm * (string * int)) list 

16 
val cnf_rules_of_ths: thm list > thm list 

17 
val neg_clausify: thm list > thm list 

18 
val expand_defs_tac: thm > tactic 

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

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

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

22 
val simpset_rules_of: Proof.context > (string * thm) list (*FIXME DELETE*) 
21505  23 
val atpset_rules_of: Proof.context > (string * thm) list 
24669  24 
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

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

28 

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

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

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

34 

20445  35 

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

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

38 
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

39 
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

40 

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

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

42 
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

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

45 
case concl_of th of (*conclusion variable*) 
24669  46 
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

47 
Thm.instantiate ([], [(cterm_of HOL.thy v, cfalse)]) th 
24669  48 
 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

49 
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

50 
 _ => th; 
15997  51 

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

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

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

54 

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

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

57 
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

58 
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

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

60 
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

61 
 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

62 
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

63 
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

64 

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

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

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

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

70 
(*Existential: declare a Skolem function, then insert into body and continue*) 
24785  71 
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

72 
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

73 
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

74 
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

75 
val _ = if null extraTs then () else 
24785  76 
warning ("Skolemization: extra type vars: " ^ 
77 
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

78 
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

79 
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

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

81 
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

82 
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

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

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

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

86 
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

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

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

89 
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

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

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

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

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

94 
 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

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

96 
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

97 
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

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

100 
 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

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

103 

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

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

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

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

107 
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

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

109 
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

110 
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

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

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

113 
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

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

115 
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

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

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

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

119 
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

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

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

122 
 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

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

124 
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

125 
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

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

128 
 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

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

132 

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

135 
(*Returns the vars of a theorem*) 

136 
fun vars_of_thm th = 

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

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

140 
local 

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

142 
val cx = hd (vars_of_thm fun_cong'); 

143 
val ty = typ_of (ctyp_of_term cx); 

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

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

148 
end; 

149 

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

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

151 
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

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

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

157 
 _ => th; 

20419  158 

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

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

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

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

164 

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

166 

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

168 

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

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

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

173 
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

174 

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

177 
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

178 

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

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

182 
val thy = theory_of_cterm ct 

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

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

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

186 
in 

187 
case body of 

188 
Const _ => makeK() 

189 
 Free _ => makeK() 

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

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

192 
 rator$rand => 

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

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

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

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

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

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

199 
in 

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

201 
end 

202 
else (*C*) 

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

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

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

206 
in 

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

208 
end 

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

210 
if rand = Bound 0 then eta_conversion ct 

211 
else (*B*) 

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

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

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

215 
in 

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

217 
end 

218 
else makeK() 

219 
 _ => error "abstract: Bad term" 

220 
end; 

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

221 

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

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

226 
else 

227 
case term_of ct of 

228 
Abs _ => 

229 
let val _ = assert_eta_free ct; 

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

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

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

233 
val u_th = combinators_aux cta 

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

235 
val cu = Thm.rhs_of u_th 

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

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

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

239 
 t1 $ t2 => 

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

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

242 

243 
fun combinators th = 

244 
if lambda_free (prop_of th) then th 

245 
else 

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

247 
val th = Drule.eta_contraction_rule th 

248 
val eqth = combinators_aux (cprop_of th) 

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

250 
in equal_elim eqth th end; 

16009  251 

252 
(*cterms are used throughout for efficiency*) 

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

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

255 
(*cterm version of mk_cTrueprop*) 

256 
fun c_mkTrueprop A = Thm.capply cTrueprop A; 

257 

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

259 
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

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

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

264 

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

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

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

267 
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

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

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

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

273 
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

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

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

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

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

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

283 
end; 
16009  284 

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

285 

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

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

287 
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

288 

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

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

290 
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

291 
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

292 
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

293 
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

294 
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

295 

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

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

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

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

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

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

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

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

304 
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

305 

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

307 
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

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

309 
 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

310 

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

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

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

314 
fun fake_name th = 
24669  315 
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

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

317 

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

318 
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

319 
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

320 
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

321 

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

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

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

324 
let val nnfth = to_nnf th and s = fake_name th 
24827  325 
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

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

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

328 

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

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

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

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

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

334 
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

335 
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

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

337 
val (thy',defs) = declare_skofuns s nnfth thy 
20419  338 
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

339 
val _ = Output.debug (fn () => Int.toString (length cnfs) ^ " clauses yielded") 
24827  340 
val cnfs' = map combinators cnfs 
341 
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

342 
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

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

344 
(try to_nnf th); 
16009  345 

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

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

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

350 
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

351 
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

352 
fun copy tab : T = tab; 
22516  353 
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

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

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

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

358 
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

359 
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

360 
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

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

363 
NONE => ([th],thy) 
24669  364 
 SOME (cls,thy') => 
24785  365 
(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

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

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

369 

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

370 
(*Exported function to convert Isabelle theorems into axiom clauses*) 
22471  371 
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

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

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

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

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

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

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

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

381 

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

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

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

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

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

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

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

392 
end; 
15347  393 

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

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

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

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

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

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

401 

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

404 

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

15347  407 

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

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

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

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

418 

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

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

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

424 

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

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

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

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

428 

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

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

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

432 

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

433 
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

434 

24827  435 
val max_lambda_nesting = 3; 
436 

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

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

439 
 excessive_lambdas _ = false; 

440 

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

442 

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

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

445 
 excessive_lambdas_fm Ts t = 

446 
if is_formula_type (fastype_of1 (Ts, t)) 

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

448 
else excessive_lambdas (t, max_lambda_nesting); 

449 

450 
fun too_complex t = 

451 
Meson.too_many_clauses t orelse excessive_lambdas_fm [] t; 

452 

24854  453 
val multi_base_blacklist = 
454 
["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm"]; 

455 

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

456 
fun skolem_cache th thy = 
24827  457 
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

458 
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

459 

24854  460 
fun skolem_cache_list (a,ths) thy = 
461 
if (Sign.base_name a) mem_string multi_base_blacklist then thy 

462 
else fold skolem_cache ths thy; 

463 

464 
val skolem_cache_theorems_of = Symtab.fold skolem_cache_list o #2 o PureThy.theorems_of; 

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

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

466 
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

467 

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

21071  470 

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

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

472 
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

473 
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

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

475 
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

476 
end; 
16563  477 

478 
(*** meson proof methods ***) 

479 

22516  480 
fun cnf_rules_of_ths ths = List.concat (map cnf_axiom ths); 
16563  481 

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

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

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

485 

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

486 
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

487 
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

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

489 

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

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

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

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

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

496 
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

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

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

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

501 
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

502 
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

503 
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

504 
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

505 
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

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

507 

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

508 

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

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

510 
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

511 
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

512 

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

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

515 
Method.SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ths)), 
21588  516 
"MESON resolution proof procedure")]; 
15347  517 

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

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

519 

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

521 

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

522 
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

523 

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

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

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

526 

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

527 

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

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

529 

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

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

533 
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

534 
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

535 

24300  536 
val neg_clausify = 
24827  537 
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

538 

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

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

540 
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

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

544 

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

546 
leading !!bound universal variables, to express generality. *) 
24669  547 
val neg_clausify_tac = 
548 
neg_skolemize_tac THEN' 

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

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

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

551 
let val ts = Logic.strip_assums_hyp prop 
24669  552 
in EVERY1 
553 
[METAHYPS 

554 
(fn hyps => 

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

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

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

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

559 

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

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

561 

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

562 
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

563 

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

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

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

567 

20419  568 
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

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

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

572 

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

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

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

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

576 

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

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

579 
"conversion of goal to conjecture clauses")]; 
24669  580 

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

581 
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

582 

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

583 
end; 