author  wenzelm 
Sun, 30 Sep 2007 16:20:33 +0200  
changeset 24771  6c7e94742afa 
parent 24742  73b8b42a36b6 
child 24785  197e4df96fd4 
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 

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

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

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 

20902  34 
val lhs_of = #1 o Logic.dest_equals o Thm.prop_of; 
35 
val rhs_of = #2 o Logic.dest_equals o Thm.prop_of; 

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

36 

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

37 

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

40 
extensionality in proofs. 

41 
FIXME! Store in theory data!!*) 

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

42 

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

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

44 
fun seed th net = 
22902
ac833b4bb7ee
moved some Drule operations to Thm (see more_thm.ML);
wenzelm
parents:
22846
diff
changeset

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

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

47 
in Net.insert_term Thm.eq_thm (t, th) net end; 
24669  48 

49 
val abstraction_cache = ref 

50 
(seed (thm"ATP_Linkup.I_simp") 

51 
(seed (thm"ATP_Linkup.B_simp") 

52 
(seed (thm"ATP_Linkup.K_simp") Net.empty))); 

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

53 

20445  54 

15997  55 
(**** Transformation of Elimination Rules into FirstOrder Formulas****) 
15347  56 

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

57 
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

58 
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

59 

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

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

61 
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

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

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

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

68 
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

69 
 _ => th; 
15997  70 

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

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

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

73 

16009  74 
(**** SKOLEMIZATION BY INFERENCE (lcp) ****) 
75 

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

76 
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

77 
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

78 
fun add_new_TFrees (TFree v) = 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

79 
if member (op =) lhs_vars v then I else insert (op =) (TFree v) 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

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

81 
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

82 
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

83 

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

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

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

86 
fun declare_skofuns s th thy = 
21071  87 
let val nref = ref 0 
88 
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

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

90 
let val cname = Name.internal ("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

91 
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

92 
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

93 
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

94 
val _ = if null extraTs then () else 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

95 
warning ("Skolemization: extra type vars: " ^ 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

96 
commas_quote (map (Sign.string_of_typ thy) extraTs)); 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

97 
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

98 
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

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

100 
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

101 
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

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

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

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

105 
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

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

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

108 
val thy'' = Theory.add_defs_i false 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

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

110 
in dec_sko (subst_bound (list_comb(c,args), p)) 
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

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

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

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

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

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

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

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

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

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

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

122 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

151 

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

153 

154 
(*Returns the vars of a theorem*) 

155 
fun vars_of_thm th = 

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

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

159 
local 

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

161 
val cx = hd (vars_of_thm fun_cong'); 

162 
val ty = typ_of (ctyp_of_term cx); 

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

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

167 
end; 

168 

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

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

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

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

173 
case prop_of th of 
24669  174 
_ $ (Const ("op =", _) $ _ $ Abs (x,_,_)) => 
175 
strip_lambdas (n1) (freeze_thm (th RS xfun_cong x)) 

176 
 _ => th; 

20419  177 

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

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

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

183 

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

186 
let val th1 = combination cf (reflexive x) 

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

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

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

191 
fun list_combination cf [] = cf 

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

193 

194 
fun list_cabs ([] , t) = t 

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

196 

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

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

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

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

202 

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

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

206 

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

208 

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

210 

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

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

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

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

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

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

216 

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

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

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

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

220 

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

221 

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

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

223 

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

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

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

226 
fun match_rhs thy t th = 
24669  227 
let val _ = Output.debug (fn()=> "match_rhs: " ^ string_of_cterm (cterm_of thy t) ^ 
24215  228 
" against\n" ^ string_of_thm th); 
20867
e7b92a48e22b
Refinements to abstraction. Seeding with combinators K, I and B.
paulson
parents:
20863
diff
changeset

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

230 
val term_insts = map Meson.term_pair_of (Vartab.dest tenv) 
24669  231 
val ct_pairs = if subthy (theory_of_thm th, thy) andalso 
232 
forall lambda_free (map #2 term_insts) 

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

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

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

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

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

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

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

239 

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

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

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

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

244 
fun abstract thy ct = 
20445  245 
if lambda_free (term_of ct) then (transfer thy (reflexive ct), []) 
246 
else 

247 
case term_of ct of 

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

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

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

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

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

252 
val (vs,Tvs) = ListPair.unzip (map (dest_Free o term_of) cvs) 
24215  253 
val _ = Output.debug (fn()=>"Nested lambda: " ^ string_of_cterm cta); 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

254 
val (u'_th,defs) = abstract thy cta 
24215  255 
val _ = Output.debug (fn()=>"Returned " ^ string_of_thm u'_th); 
22902
ac833b4bb7ee
moved some Drule operations to Thm (see more_thm.ML);
wenzelm
parents:
22846
diff
changeset

256 
val cu' = Thm.rhs_of u'_th 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

257 
val u' = term_of cu' 
24669  258 
val abs_v_u = fold_rev (lambda o term_of) cvs u' 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

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

260 
val args = term_frees abs_v_u 
24215  261 
val _ = Output.debug (fn()=>Int.toString (length args) ^ " arguments"); 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

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

263 
(*Forms a lambdaabstraction over the formal parameters*) 
24215  264 
val _ = Output.debug (fn()=>"Looking up " ^ string_of_cterm cu'); 
20969
341808e0b7f2
Abstraction reuse code now checks that the abstraction function can be used in the current
paulson
parents:
20902
diff
changeset

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

266 
val (ax,ax',thy) = 
24669  267 
case List.mapPartial (match_rhs thy abs_v_u) 
20969
341808e0b7f2
Abstraction reuse code now checks that the abstraction function can be used in the current
paulson
parents:
20902
diff
changeset

268 
(Net.match_term (!abstraction_cache) u') of 
24669  269 
(ax,ax')::_ => 
24215  270 
(Output.debug (fn()=>"Reusing axiom " ^ string_of_thm ax); 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

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

272 
 [] => 
24215  273 
let val _ = Output.debug (fn()=>"Lookup was empty"); 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

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

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

276 
val c = Const (Sign.full_name thy cname, cT) 
24771
6c7e94742afa
skofuns/absfuns: explicit markup as internal consts;
wenzelm
parents:
24742
diff
changeset

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

278 
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

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

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

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

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

283 
[(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

284 
handle ERROR _ => raise Clausify_failure thy 
24215  285 
val _ = Output.debug (fn()=> "Definition is " ^ string_of_thm (get_axiom thy cdef)); 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

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

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

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

289 
val (_,ax') = Option.valOf (match_rhs thy abs_v_u ax) 
24215  290 
val _ = Output.debug (fn()=> "Declaring: " ^ string_of_thm ax ^ "\n" ^ 
291 
"Instance: " ^ string_of_thm ax'); 

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

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

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

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

296 
in (ax,ax',thy) end 
24215  297 
in Output.debug (fn()=>"Lookup result: " ^ string_of_thm ax'); 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

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

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

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

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

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

303 
in (combination th1 th2, defs1@defs2) end 
24215  304 
val _ = Output.debug (fn()=>"declare_absfuns, Abstracting: " ^ string_of_thm th); 
20419  305 
val (eqth,defs) = abstract (theory_of_thm th) (cprop_of th) 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

306 
val ths = equal_elim eqth th :: map (strip_lambdas ~1 o mk_object_eq o freeze_thm) defs 
24215  307 
val _ = Output.debug (fn()=>"declare_absfuns, Result: " ^ string_of_thm (hd ths)); 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

308 
in (theory_of_thm eqth, map Drule.eta_contraction_rule ths) end; 
20419  309 

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

311 

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

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

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

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

315 

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

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

317 
fun assume_absfuns s th = 
20445  318 
let val thy = theory_of_thm th 
319 
val cterm = cterm_of thy 

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

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

321 
fun abstract ct = 
20445  322 
if lambda_free (term_of ct) then (reflexive ct, []) 
323 
else 

324 
case term_of ct of 

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

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

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

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

329 
val (u'_th,defs) = abstract cta 
22902
ac833b4bb7ee
moved some Drule operations to Thm (see more_thm.ML);
wenzelm
parents:
22846
diff
changeset

330 
val cu' = Thm.rhs_of u'_th 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

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

332 
(*Could use Thm.cabs instead of lambda to work at level of cterms*) 
24669  333 
val abs_v_u = fold_rev (lambda o term_of) cvs (term_of cu') 
20525
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset

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

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

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

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

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

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

340 
val (ax,ax') = 
24669  341 
case List.mapPartial (match_rhs thy abs_v_u) 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

342 
(Net.match_term (!abstraction_cache) u') of 
24669  343 
(ax,ax')::_ => 
24215  344 
(Output.debug (fn()=>"Reusing axiom " ^ string_of_thm ax); 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

359 
in (ax,ax') end 
24215  360 
in Output.debug (fn()=>"Lookup result: " ^ string_of_thm ax'); 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

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

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

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

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

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

366 
in (combination t1' t2', defs1@defs2) end 
24215  367 
val _ = Output.debug (fn()=>"assume_absfuns, Abstracting: " ^ string_of_thm th); 
20525
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset

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

369 
val ths = equal_elim eqth th :: map (strip_lambdas ~1 o mk_object_eq o freeze_thm) defs 
24215  370 
val _ = Output.debug (fn()=>"assume_absfuns, Result: " ^ string_of_thm (hd ths)); 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

371 
in map Drule.eta_contraction_rule ths end; 
20419  372 

16009  373 

374 
(*cterms are used throughout for efficiency*) 

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

375 
val cTrueprop = Thm.cterm_of HOL.thy HOLogic.Trueprop; 
16009  376 

377 
(*cterm version of mk_cTrueprop*) 

378 
fun c_mkTrueprop A = Thm.capply cTrueprop A; 

379 

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

381 
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

382 
fun c_variant_abs_multi (ct0, vars) = 
16009  383 
let val (cv,ct) = Thm.dest_abs NONE ct0 
384 
in c_variant_abs_multi (ct, cv::vars) end 

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

386 

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

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

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

389 
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

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

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

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

395 
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

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

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

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

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

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

405 
end; 
16009  406 

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

407 

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

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

409 
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

410 

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

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

412 
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

413 
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

414 
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

415 
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

416 
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

417 

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

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

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

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

421 
> transform_elim > zero_var_indexes > freeze_thm 
24300  422 
> Conv.fconv_rule ObjectLogic.atomize > Meson.make_nnf > strip_lambdas ~1; 
16009  423 

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

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

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

426 
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

427 

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

429 
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

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

431 
 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

432 

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

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

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

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

436 
> tap (fn ths => assert_lambda_free ths "assume_abstract: lambdas") 
20445  437 

20419  438 
(*Replace lambdas by assumed function definitions in the theorems*) 
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

439 
fun assume_abstract_list s ths = List.concat (map (assume_abstract s) ths); 
20419  440 

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

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

442 
fun declare_abstract s (thy, []) = (thy, []) 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

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

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

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

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

448 
> Drule.eta_contraction_rule > transfer thy > declare_absfuns s 
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

449 
handle Clausify_failure thy_e => (thy_e,[]) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

450 
val _ = assert_lambda_free th_defs "declare_abstract: lambdas" 
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

451 
val (thy'', ths') = declare_abstract (s^"'") (thy', ths) 
20419  452 
in (thy'', th_defs @ ths') end; 
453 

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

455 
fun flatten_name s = space_implode "_X" (NameSpace.explode s); 
21071  456 

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

457 
fun fake_name th = 
24669  458 
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

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

460 

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

461 
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

462 
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

463 
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

464 

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

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

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

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

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

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

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

471 

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

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

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

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

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

477 
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

478 
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

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

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

482 
val _ = Output.debug (fn () => Int.toString (length cnfs) ^ " clauses yielded") 
22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset

483 
val (thy'',cnfs') = declare_abstract s (thy',cnfs) 
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

484 
in (map Goal.close_result (Meson.finish_cnf cnfs'), thy'') end 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

485 
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

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

487 
(try to_nnf th); 
16009  488 

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

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

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

493 
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

494 
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

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

497 
fun merge _ (tab1, tab2) : T = Thmtab.merge (K true) (tab1, tab2); 
22846  498 
); 
22516  499 

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

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

501 
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

502 
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

503 
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

504 
NONE => 
22471  505 
(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

506 
NONE => ([th],thy) 
24669  507 
 SOME (cls,thy') => 
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

508 
(Output.debug (fn () => "skolem_cache_thm: " ^ Int.toString (length cls) ^ 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

509 
" clauses inserted into cache: " ^ 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

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

512 

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

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

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

517 
case Thmtab.lookup (ThmCache.get thy) th of 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

518 
NONE => (Output.debug (fn () => "cnf_axiom: " ^ 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

519 
map Goal.close_result (skolem_thm th)) 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

520 
 SOME cls => cls 
22516  521 
end; 
15347  522 

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

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

524 

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

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

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

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

531 
in 
22130  532 
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

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

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

535 
end; 
15347  536 

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

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

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

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

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

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

544 

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

547 

24042  548 
fun atpset_rules_of ctxt = map pairname (ResAtpset.get ctxt); 
20774  549 

15347  550 

22471  551 
(**** Translate a set of theorems into CNF ****) 
15347  552 

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

555 
 cnf_rules ((name,th) :: ths) err_list = 
19894  556 
let val (ts,es) = cnf_rules ths err_list 
22471  557 
in (cnf_axiom th :: ts,es) handle _ => (ts, (th::es)) end; 
15347  558 

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

561 

19894  562 
fun cnf_rules_pairs_aux pairs [] = pairs 
563 
 cnf_rules_pairs_aux pairs ((name,th)::ths) = 

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

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

567 

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

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

569 
fun cnf_rules_pairs l = cnf_rules_pairs_aux [] (rev l); 
19353  570 

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

571 

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

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

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

575 

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

576 
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

577 

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

578 
fun skolem_cache th thy = #2 (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

579 

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

580 
fun skolem_cache_all thy = fold skolem_cache (map #2 (PureThy.all_thms_of thy)) thy; 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

581 

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

582 
fun skolem_cache_new thy = fold skolem_cache (map #2 (PureThy.thms_of thy)) thy; 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset

583 

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

21071  586 

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

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

588 
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

589 
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

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

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

592 
end; 
16563  593 

594 
(*** meson proof methods ***) 

595 

22516  596 
fun cnf_rules_of_ths ths = List.concat (map cnf_axiom ths); 
16563  597 

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

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

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

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

601 

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

602 
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

603 
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

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

605 

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

608 
of llabs_ and sko_ functions. *) 

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

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

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

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

612 
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

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

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

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

617 
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

618 
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

619 
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

620 
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

621 
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

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

623 

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

624 

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

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

626 
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

627 
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

628 

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

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

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

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

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

635 

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

637 

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

638 
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

639 

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

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

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

642 

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

643 

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

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

645 

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

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

649 
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

650 
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

651 

24300  652 
val neg_clausify = 
653 
filter no_tvars o Meson.finish_cnf o assume_abstract_list "subgoal" o Meson.make_clauses; 

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

654 

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

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

656 
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

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

660 

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

662 
leading !!bound universal variables, to express generality. *) 
24669  663 
val neg_clausify_tac = 
664 
neg_skolemize_tac THEN' 

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

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

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

667 
let val ts = Logic.strip_assums_hyp prop 
24669  668 
in EVERY1 
669 
[METAHYPS 

670 
(fn hyps => 

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

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

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

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

675 

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

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

677 

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

678 
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

679 

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

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

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

683 

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

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

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

688 

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

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

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

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

692 

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

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

695 
"conversion of goal to conjecture clauses")]; 
24669  696 

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

697 
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

698 

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

699 
end; 