author  wenzelm 
Wed, 29 May 2013 18:25:11 +0200  
changeset 52223  5bb6ae8acb87 
parent 52222  0fa3b456a267 
child 52470  dedd7952a62c 
permissions  rwrr 
250  1 
(* Title: Pure/thm.ML 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29003
diff
changeset

3 
Author: Makarius 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

4 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

5 
The very core of Isabelle's Meta Logic: certified types and terms, 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

6 
derivations, theorems, framework rules (including lifting and 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

7 
resolution), oracles. 
0  8 
*) 
9 

6089  10 
signature BASIC_THM = 
1503  11 
sig 
1160  12 
(*certified types*) 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

13 
type ctyp 
16656  14 
val rep_ctyp: ctyp > 
26631
d6b6c74a8bcf
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26424
diff
changeset

15 
{thy_ref: theory_ref, 
16656  16 
T: typ, 
20512  17 
maxidx: int, 
39687  18 
sorts: sort Ord_List.T} 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

19 
val theory_of_ctyp: ctyp > theory 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

20 
val typ_of: ctyp > typ 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

21 
val ctyp_of: theory > typ > ctyp 
1160  22 

23 
(*certified terms*) 

24 
type cterm 

22584  25 
exception CTERM of string * cterm list 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

26 
val rep_cterm: cterm > 
26631
d6b6c74a8bcf
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26424
diff
changeset

27 
{thy_ref: theory_ref, 
16656  28 
t: term, 
29 
T: typ, 

30 
maxidx: int, 

39687  31 
sorts: sort Ord_List.T} 
28354  32 
val crep_cterm: cterm > 
39687  33 
{thy_ref: theory_ref, t: term, T: ctyp, maxidx: int, sorts: sort Ord_List.T} 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

34 
val theory_of_cterm: cterm > theory 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

35 
val term_of: cterm > term 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

36 
val cterm_of: theory > term > cterm 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

37 
val ctyp_of_term: cterm > ctyp 
1160  38 

28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

39 
(*theorems*) 
1160  40 
type thm 
23601  41 
type conv = cterm > thm 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

42 
val rep_thm: thm > 
26631
d6b6c74a8bcf
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26424
diff
changeset

43 
{thy_ref: theory_ref, 
28017  44 
tags: Properties.T, 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

45 
maxidx: int, 
39687  46 
shyps: sort Ord_List.T, 
47 
hyps: term Ord_List.T, 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

48 
tpairs: (term * term) list, 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

49 
prop: term} 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

50 
val crep_thm: thm > 
26631
d6b6c74a8bcf
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26424
diff
changeset

51 
{thy_ref: theory_ref, 
28017  52 
tags: Properties.T, 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

53 
maxidx: int, 
39687  54 
shyps: sort Ord_List.T, 
55 
hyps: cterm Ord_List.T, 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

56 
tpairs: (cterm * cterm) list, 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

57 
prop: cterm} 
6089  58 
exception THM of string * int * thm list 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

59 
val theory_of_thm: thm > theory 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

60 
val prop_of: thm > term 
16656  61 
val concl_of: thm > term 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

62 
val prems_of: thm > term list 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

63 
val nprems_of: thm > int 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

64 
val cprop_of: thm > cterm 
18145  65 
val cprem_of: thm > int > cterm 
250  66 
end; 
0  67 

6089  68 
signature THM = 
69 
sig 

70 
include BASIC_THM 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

71 
val dest_ctyp: ctyp > ctyp list 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

72 
val dest_comb: cterm > cterm * cterm 
22909  73 
val dest_fun: cterm > cterm 
20580
6fb75df09253
added dest_arg, i.e. a tuned version of #2 o dest_comb;
wenzelm
parents:
20548
diff
changeset

74 
val dest_arg: cterm > cterm 
22909  75 
val dest_fun2: cterm > cterm 
76 
val dest_arg1: cterm > cterm 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

77 
val dest_abs: string option > cterm > cterm * cterm 
46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
46475
diff
changeset

78 
val apply: cterm > cterm > cterm 
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
46475
diff
changeset

79 
val lambda_name: string * cterm > cterm > cterm 
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
46475
diff
changeset

80 
val lambda: cterm > cterm > cterm 
31945  81 
val adjust_maxidx_cterm: int > cterm > cterm 
82 
val incr_indexes_cterm: int > cterm > cterm 

83 
val match: cterm * cterm > (ctyp * ctyp) list * (cterm * cterm) list 

84 
val first_order_match: cterm * cterm > (ctyp * ctyp) list * (cterm * cterm) list 

31947
7daee3bed3af
clarified strip_shyps: proper type witnesses for present sorts;
wenzelm
parents:
31945
diff
changeset

85 
val fold_terms: (term > 'a > 'a) > thm > 'a > 'a 
16945  86 
val terms_of_tpairs: (term * term) list > term list 
31945  87 
val full_prop_of: thm > term 
19881  88 
val maxidx_of: thm > int 
19910  89 
val maxidx_thm: thm > int > int 
19881  90 
val hyps_of: thm > term list 
38709  91 
val tpairs_of: thm > (term * term) list 
31945  92 
val no_prems: thm > bool 
93 
val major_prem_of: thm > term 

38709  94 
val transfer: theory > thm > thm 
95 
val weaken: cterm > thm > thm 

96 
val weaken_sorts: sort list > cterm > cterm 

97 
val extra_shyps: thm > sort list 

44333
cc53ce50f738
reverted to join_bodies/join_proofs based on fold_body_thms to regain performance (escpecially of HOLProofs)  see also aa9c1e9ef2ce and 4e2abb045eac;
wenzelm
parents:
44331
diff
changeset

98 
val proof_bodies_of: thm list > proof_body list 
32725  99 
val proof_body_of: thm > proof_body 
100 
val proof_of: thm > proof 

44331  101 
val join_proofs: thm list > unit 
50126
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
49008
diff
changeset

102 
val peek_status: thm > {oracle: bool, unfinished: bool, failed: bool} 
32725  103 
val future: thm future > cterm > thm 
36744
6e1f3d609a68
renamed Thm.get_name > Thm.derivation_name and Thm.put_name > Thm.name_derivation, to emphasize the true nature of these operations;
wenzelm
parents:
36742
diff
changeset

104 
val derivation_name: thm > string 
6e1f3d609a68
renamed Thm.get_name > Thm.derivation_name and Thm.put_name > Thm.name_derivation, to emphasize the true nature of these operations;
wenzelm
parents:
36742
diff
changeset

105 
val name_derivation: string > thm > thm 
28675
fb68c0767004
renamed get_axiom_i to axiom, removed obsolete get_axiom;
wenzelm
parents:
28648
diff
changeset

106 
val axiom: theory > string > thm 
fb68c0767004
renamed get_axiom_i to axiom, removed obsolete get_axiom;
wenzelm
parents:
28648
diff
changeset

107 
val axioms_of: theory > (string * thm) list 
28017  108 
val get_tags: thm > Properties.T 
109 
val map_tags: (Properties.T > Properties.T) > thm > thm 

23781
ab793a6ddf9f
Added function norm_proof for normalizing the proof term
berghofe
parents:
23657
diff
changeset

110 
val norm_proof: thm > thm 
20261  111 
val adjust_maxidx_thm: int > thm > thm 
38709  112 
(*meta rules*) 
113 
val assume: cterm > thm 

114 
val implies_intr: cterm > thm > thm 

115 
val implies_elim: thm > thm > thm 

116 
val forall_intr: cterm > thm > thm 

117 
val forall_elim: cterm > thm > thm 

118 
val reflexive: cterm > thm 

119 
val symmetric: thm > thm 

120 
val transitive: thm > thm > thm 

121 
val beta_conversion: bool > conv 

122 
val eta_conversion: conv 

123 
val eta_long_conversion: conv 

124 
val abstract_rule: string > cterm > thm > thm 

125 
val combination: thm > thm > thm 

126 
val equal_intr: thm > thm > thm 

127 
val equal_elim: thm > thm > thm 

128 
val flexflex_rule: thm > thm Seq.seq 

129 
val generalize: string list * string list > int > thm > thm 

130 
val instantiate: (ctyp * ctyp) list * (cterm * cterm) list > thm > thm 

131 
val instantiate_cterm: (ctyp * ctyp) list * (cterm * cterm) list > cterm > cterm 

132 
val trivial: cterm > thm 

36330
0584e203960e
renamed Drule.unconstrainTs to Thm.unconstrain_allTs to accomdate the version by krauss/schropp;
wenzelm
parents:
35986
diff
changeset

133 
val of_class: ctyp * class > thm 
36614
b6c031ad3690
minor tuning of Thm.strip_shyps  no longer pervasive;
wenzelm
parents:
36613
diff
changeset

134 
val strip_shyps: thm > thm 
36768
46be86127972
just one version of Thm.unconstrainT, which affects all variables;
wenzelm
parents:
36744
diff
changeset

135 
val unconstrainT: thm > thm 
38709  136 
val varifyT_global': (string * sort) list > thm > ((string * sort) * indexname) list * thm 
137 
val varifyT_global: thm > thm 

36615
88756a5a92fc
renamed Thm.freezeT to Thm.legacy_freezeT  it is based on Type.legacy_freeze;
wenzelm
parents:
36614
diff
changeset

138 
val legacy_freezeT: thm > thm 
38709  139 
val lift_rule: cterm > thm > thm 
140 
val incr_indexes: int > thm > thm 

31945  141 
val assumption: int > thm > thm Seq.seq 
142 
val eq_assumption: int > thm > thm 

143 
val rotate_rule: int > int > thm > thm 

144 
val permute_prems: int > int > thm > thm 

145 
val rename_params_rule: string list * int > thm > thm 

38709  146 
val rename_boundvars: term > term > thm > thm 
52223
5bb6ae8acb87
tuned signature  more explicit flags for lowlevel Thm.bicompose;
wenzelm
parents:
52222
diff
changeset

147 
val bicompose: {flatten: bool, match: bool, incremented: bool} > 
5bb6ae8acb87
tuned signature  more explicit flags for lowlevel Thm.bicompose;
wenzelm
parents:
52222
diff
changeset

148 
bool * thm * int > int > thm > thm Seq.seq 
31945  149 
val biresolution: bool > (bool * thm) list > int > thm > thm Seq.seq 
50301  150 
val extern_oracles: Proof.context > (Markup.T * xstring) list 
30288
a32700e45ab3
Thm.add_oracle interface: replaced old bstring by binding;
wenzelm
parents:
29636
diff
changeset

151 
val add_oracle: binding * ('a > cterm) > theory > (string * ('a > thm)) * theory 
6089  152 
end; 
153 

32590
95f4f08f950f
replaced opaque signature matching by plain old abstype (again, cf. ac4498f95d1c)  this recovers pretty printing in SML/NJ and Poly/ML 5.3;
wenzelm
parents:
32198
diff
changeset

154 
structure Thm: THM = 
0  155 
struct 
250  156 

387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

157 
(*** Certified terms and types ***) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

158 

250  159 
(** certified types **) 
160 

32590
95f4f08f950f
replaced opaque signature matching by plain old abstype (again, cf. ac4498f95d1c)  this recovers pretty printing in SML/NJ and Poly/ML 5.3;
wenzelm
parents:
32198
diff
changeset

161 
abstype ctyp = Ctyp of 
20512  162 
{thy_ref: theory_ref, 
163 
T: typ, 

164 
maxidx: int, 

39687  165 
sorts: sort Ord_List.T} 
32590
95f4f08f950f
replaced opaque signature matching by plain old abstype (again, cf. ac4498f95d1c)  this recovers pretty printing in SML/NJ and Poly/ML 5.3;
wenzelm
parents:
32198
diff
changeset

166 
with 
250  167 

26631
d6b6c74a8bcf
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26424
diff
changeset

168 
fun rep_ctyp (Ctyp args) = args; 
16656  169 
fun theory_of_ctyp (Ctyp {thy_ref, ...}) = Theory.deref thy_ref; 
250  170 
fun typ_of (Ctyp {T, ...}) = T; 
171 

16656  172 
fun ctyp_of thy raw_T = 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

173 
let 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

174 
val T = Sign.certify_typ thy raw_T; 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

175 
val maxidx = Term.maxidx_of_typ T; 
26640
92e6d3ec91bd
simplified handling of sorts, removed unnecessary universal witness;
wenzelm
parents:
26631
diff
changeset

176 
val sorts = Sorts.insert_typ T []; 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

177 
in Ctyp {thy_ref = Theory.check_thy thy, T = T, maxidx = maxidx, sorts = sorts} end; 
250  178 

32784  179 
fun dest_ctyp (Ctyp {thy_ref, T = Type (_, Ts), maxidx, sorts}) = 
20512  180 
map (fn T => Ctyp {thy_ref = thy_ref, T = T, maxidx = maxidx, sorts = sorts}) Ts 
16679  181 
 dest_ctyp cT = raise TYPE ("dest_ctyp", [typ_of cT], []); 
15087  182 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

183 

4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

184 

250  185 
(** certified terms **) 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

186 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

187 
(*certified terms with checked typ, maxidx, and sorts*) 
32590
95f4f08f950f
replaced opaque signature matching by plain old abstype (again, cf. ac4498f95d1c)  this recovers pretty printing in SML/NJ and Poly/ML 5.3;
wenzelm
parents:
32198
diff
changeset

188 
abstype cterm = Cterm of 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

189 
{thy_ref: theory_ref, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

190 
t: term, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

191 
T: typ, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

192 
maxidx: int, 
39687  193 
sorts: sort Ord_List.T} 
32590
95f4f08f950f
replaced opaque signature matching by plain old abstype (again, cf. ac4498f95d1c)  this recovers pretty printing in SML/NJ and Poly/ML 5.3;
wenzelm
parents:
32198
diff
changeset

194 
with 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

195 

22584  196 
exception CTERM of string * cterm list; 
16679  197 

26631
d6b6c74a8bcf
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26424
diff
changeset

198 
fun rep_cterm (Cterm args) = args; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

199 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

200 
fun crep_cterm (Cterm {thy_ref, t, T, maxidx, sorts}) = 
26631
d6b6c74a8bcf
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26424
diff
changeset

201 
{thy_ref = thy_ref, t = t, maxidx = maxidx, sorts = sorts, 
d6b6c74a8bcf
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26424
diff
changeset

202 
T = Ctyp {thy_ref = thy_ref, T = T, maxidx = maxidx, sorts = sorts}}; 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

203 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

204 
fun theory_of_cterm (Cterm {thy_ref, ...}) = Theory.deref thy_ref; 
250  205 
fun term_of (Cterm {t, ...}) = t; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

206 

20512  207 
fun ctyp_of_term (Cterm {thy_ref, T, maxidx, sorts, ...}) = 
208 
Ctyp {thy_ref = thy_ref, T = T, maxidx = maxidx, sorts = sorts}; 

2671  209 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

210 
fun cterm_of thy tm = 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

211 
let 
18969  212 
val (t, T, maxidx) = Sign.certify_term thy tm; 
26640
92e6d3ec91bd
simplified handling of sorts, removed unnecessary universal witness;
wenzelm
parents:
26631
diff
changeset

213 
val sorts = Sorts.insert_term t []; 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

214 
in Cterm {thy_ref = Theory.check_thy thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

215 

32784  216 
fun merge_thys0 (Cterm {thy_ref = r1, ...}) (Cterm {thy_ref = r2, ...}) = 
23601  217 
Theory.merge_refs (r1, r2); 
16656  218 

20580
6fb75df09253
added dest_arg, i.e. a tuned version of #2 o dest_comb;
wenzelm
parents:
20548
diff
changeset

219 

22909  220 
(* destructors *) 
221 

32784  222 
fun dest_comb (Cterm {t = c $ a, T, thy_ref, maxidx, sorts}) = 
22909  223 
let val A = Term.argument_type_of c 0 in 
224 
(Cterm {t = c, T = A > T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts}, 

225 
Cterm {t = a, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts}) 

1493
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

226 
end 
22584  227 
 dest_comb ct = raise CTERM ("dest_comb", [ct]); 
1493
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

228 

32784  229 
fun dest_fun (Cterm {t = c $ _, T, thy_ref, maxidx, sorts}) = 
22909  230 
let val A = Term.argument_type_of c 0 
231 
in Cterm {t = c, T = A > T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end 

232 
 dest_fun ct = raise CTERM ("dest_fun", [ct]); 

233 

32784  234 
fun dest_arg (Cterm {t = c $ a, T = _, thy_ref, maxidx, sorts}) = 
22909  235 
let val A = Term.argument_type_of c 0 
236 
in Cterm {t = a, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end 

22584  237 
 dest_arg ct = raise CTERM ("dest_arg", [ct]); 
20580
6fb75df09253
added dest_arg, i.e. a tuned version of #2 o dest_comb;
wenzelm
parents:
20548
diff
changeset

238 

22909  239 

32784  240 
fun dest_fun2 (Cterm {t = c $ _ $ _, T, thy_ref, maxidx, sorts}) = 
22909  241 
let 
242 
val A = Term.argument_type_of c 0; 

243 
val B = Term.argument_type_of c 1; 

244 
in Cterm {t = c, T = A > B > T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end 

245 
 dest_fun2 ct = raise CTERM ("dest_fun2", [ct]); 

246 

247 
fun dest_arg1 (Cterm {t = c $ a $ _, T = _, thy_ref, maxidx, sorts}) = 

248 
let val A = Term.argument_type_of c 0 

249 
in Cterm {t = a, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end 

250 
 dest_arg1 ct = raise CTERM ("dest_arg1", [ct]); 

20673  251 

32784  252 
fun dest_abs a (Cterm {t = Abs (x, T, t), T = Type ("fun", [_, U]), thy_ref, maxidx, sorts}) = 
18944  253 
let val (y', t') = Term.dest_abs (the_default x a, T, t) in 
16679  254 
(Cterm {t = Free (y', T), T = T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts}, 
255 
Cterm {t = t', T = U, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts}) 

1493
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

256 
end 
22584  257 
 dest_abs _ ct = raise CTERM ("dest_abs", [ct]); 
1493
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

258 

22909  259 

260 
(* constructors *) 

261 

46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
46475
diff
changeset

262 
fun apply 
16656  263 
(cf as Cterm {t = f, T = Type ("fun", [dty, rty]), maxidx = maxidx1, sorts = sorts1, ...}) 
264 
(cx as Cterm {t = x, T, maxidx = maxidx2, sorts = sorts2, ...}) = 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

265 
if T = dty then 
16656  266 
Cterm {thy_ref = merge_thys0 cf cx, 
267 
t = f $ x, 

268 
T = rty, 

269 
maxidx = Int.max (maxidx1, maxidx2), 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

270 
sorts = Sorts.union sorts1 sorts2} 
46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
46475
diff
changeset

271 
else raise CTERM ("apply: types don't agree", [cf, cx]) 
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
46475
diff
changeset

272 
 apply cf cx = raise CTERM ("apply: first arg is not a function", [cf, cx]); 
250  273 

46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
46475
diff
changeset

274 
fun lambda_name 
32198  275 
(x, ct1 as Cterm {t = t1, T = T1, maxidx = maxidx1, sorts = sorts1, ...}) 
16656  276 
(ct2 as Cterm {t = t2, T = T2, maxidx = maxidx2, sorts = sorts2, ...}) = 
32198  277 
let val t = Term.lambda_name (x, t1) t2 in 
16656  278 
Cterm {thy_ref = merge_thys0 ct1 ct2, 
279 
t = t, T = T1 > T2, 

280 
maxidx = Int.max (maxidx1, maxidx2), 

281 
sorts = Sorts.union sorts1 sorts2} 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

282 
end; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

283 

46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
46475
diff
changeset

284 
fun lambda t u = lambda_name ("", t) u; 
32198  285 

20580
6fb75df09253
added dest_arg, i.e. a tuned version of #2 o dest_comb;
wenzelm
parents:
20548
diff
changeset

286 

22909  287 
(* indexes *) 
288 

20580
6fb75df09253
added dest_arg, i.e. a tuned version of #2 o dest_comb;
wenzelm
parents:
20548
diff
changeset

289 
fun adjust_maxidx_cterm i (ct as Cterm {thy_ref, t, T, maxidx, sorts}) = 
6fb75df09253
added dest_arg, i.e. a tuned version of #2 o dest_comb;
wenzelm
parents:
20548
diff
changeset

290 
if maxidx = i then ct 
6fb75df09253
added dest_arg, i.e. a tuned version of #2 o dest_comb;
wenzelm
parents:
20548
diff
changeset

291 
else if maxidx < i then 
6fb75df09253
added dest_arg, i.e. a tuned version of #2 o dest_comb;
wenzelm
parents:
20548
diff
changeset

292 
Cterm {maxidx = i, thy_ref = thy_ref, t = t, T = T, sorts = sorts} 
6fb75df09253
added dest_arg, i.e. a tuned version of #2 o dest_comb;
wenzelm
parents:
20548
diff
changeset

293 
else 
6fb75df09253
added dest_arg, i.e. a tuned version of #2 o dest_comb;
wenzelm
parents:
20548
diff
changeset

294 
Cterm {maxidx = Int.max (maxidx_of_term t, i), thy_ref = thy_ref, t = t, T = T, sorts = sorts}; 
6fb75df09253
added dest_arg, i.e. a tuned version of #2 o dest_comb;
wenzelm
parents:
20548
diff
changeset

295 

22909  296 
fun incr_indexes_cterm i (ct as Cterm {thy_ref, t, T, maxidx, sorts}) = 
297 
if i < 0 then raise CTERM ("negative increment", [ct]) 

298 
else if i = 0 then ct 

299 
else Cterm {thy_ref = thy_ref, t = Logic.incr_indexes ([], i) t, 

300 
T = Logic.incr_tvar i T, maxidx = maxidx + i, sorts = sorts}; 

301 

302 

303 
(* matching *) 

304 

305 
local 

306 

307 
fun gen_match match 

20512  308 
(ct1 as Cterm {t = t1, sorts = sorts1, ...}, 
20815  309 
ct2 as Cterm {t = t2, sorts = sorts2, maxidx = maxidx2, ...}) = 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

310 
let 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

311 
val thy = Theory.deref (merge_thys0 ct1 ct2); 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

312 
val (Tinsts, tinsts) = match thy (t1, t2) (Vartab.empty, Vartab.empty); 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

313 
val sorts = Sorts.union sorts1 sorts2; 
20512  314 
fun mk_cTinst ((a, i), (S, T)) = 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

315 
(Ctyp {T = TVar ((a, i), S), thy_ref = Theory.check_thy thy, maxidx = i, sorts = sorts}, 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

316 
Ctyp {T = T, thy_ref = Theory.check_thy thy, maxidx = maxidx2, sorts = sorts}); 
20512  317 
fun mk_ctinst ((x, i), (T, t)) = 
32035  318 
let val T = Envir.subst_type Tinsts T in 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

319 
(Cterm {t = Var ((x, i), T), T = T, thy_ref = Theory.check_thy thy, 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

320 
maxidx = i, sorts = sorts}, 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

321 
Cterm {t = t, T = T, thy_ref = Theory.check_thy thy, maxidx = maxidx2, sorts = sorts}) 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

322 
end; 
16656  323 
in (Vartab.fold (cons o mk_cTinst) Tinsts [], Vartab.fold (cons o mk_ctinst) tinsts []) end; 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

324 

22909  325 
in 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

326 

22909  327 
val match = gen_match Pattern.match; 
328 
val first_order_match = gen_match Pattern.first_order_match; 

329 

330 
end; 

10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

331 

2509  332 

333 

28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

334 
(*** Derivations and Theorems ***) 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

335 

32590
95f4f08f950f
replaced opaque signature matching by plain old abstype (again, cf. ac4498f95d1c)  this recovers pretty printing in SML/NJ and Poly/ML 5.3;
wenzelm
parents:
32198
diff
changeset

336 
abstype thm = Thm of 
40124  337 
deriv * (*derivation*) 
338 
{thy_ref: theory_ref, (*dynamic reference to theory*) 

339 
tags: Properties.T, (*additional annotations/comments*) 

340 
maxidx: int, (*maximum index of any Var or TVar*) 

341 
shyps: sort Ord_List.T, (*sort hypotheses*) 

342 
hyps: term Ord_List.T, (*hypotheses*) 

343 
tpairs: (term * term) list, (*flexflex pairs*) 

344 
prop: term} (*conclusion*) 

28624  345 
and deriv = Deriv of 
39687  346 
{promises: (serial * thm future) Ord_List.T, 
37309  347 
body: Proofterm.proof_body} 
32590
95f4f08f950f
replaced opaque signature matching by plain old abstype (again, cf. ac4498f95d1c)  this recovers pretty printing in SML/NJ and Poly/ML 5.3;
wenzelm
parents:
32198
diff
changeset

348 
with 
0  349 

23601  350 
type conv = cterm > thm; 
351 

16725  352 
(*errors involving theorems*) 
353 
exception THM of string * int * thm list; 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

354 

28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

355 
fun rep_thm (Thm (_, args)) = args; 
0  356 

28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

357 
fun crep_thm (Thm (_, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) = 
26631
d6b6c74a8bcf
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26424
diff
changeset

358 
let fun cterm max t = Cterm {thy_ref = thy_ref, t = t, T = propT, maxidx = max, sorts = shyps} in 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

359 
{thy_ref = thy_ref, tags = tags, maxidx = maxidx, shyps = shyps, 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

360 
hyps = map (cterm ~1) hyps, 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

361 
tpairs = map (pairself (cterm maxidx)) tpairs, 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

362 
prop = cterm maxidx prop} 
1517  363 
end; 
364 

31947
7daee3bed3af
clarified strip_shyps: proper type witnesses for present sorts;
wenzelm
parents:
31945
diff
changeset

365 
fun fold_terms f (Thm (_, {tpairs, prop, hyps, ...})) = 
7daee3bed3af
clarified strip_shyps: proper type witnesses for present sorts;
wenzelm
parents:
31945
diff
changeset

366 
fold (fn (t, u) => f t #> f u) tpairs #> f prop #> fold f hyps; 
7daee3bed3af
clarified strip_shyps: proper type witnesses for present sorts;
wenzelm
parents:
31945
diff
changeset

367 

16725  368 
fun terms_of_tpairs tpairs = fold_rev (fn (t, u) => cons t o cons u) tpairs []; 
369 

370 
fun eq_tpairs ((t, u), (t', u')) = t aconv t' andalso u aconv u'; 

18944  371 
fun union_tpairs ts us = Library.merge eq_tpairs (ts, us); 
16884
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

372 
val maxidx_tpairs = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u); 
16725  373 

374 
fun attach_tpairs tpairs prop = 

375 
Logic.list_implies (map Logic.mk_equals tpairs, prop); 

376 

28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

377 
fun full_prop_of (Thm (_, {tpairs, prop, ...})) = attach_tpairs tpairs prop; 
16945  378 

39687  379 
val union_hyps = Ord_List.union Term_Ord.fast_term_ord; 
380 
val insert_hyps = Ord_List.insert Term_Ord.fast_term_ord; 

381 
val remove_hyps = Ord_List.remove Term_Ord.fast_term_ord; 

22365  382 

16945  383 

24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

384 
(* merge theories of cterms/thms  trivial absorption only *) 
16945  385 

32784  386 
fun merge_thys1 (Cterm {thy_ref = r1, ...}) (Thm (_, {thy_ref = r2, ...})) = 
23601  387 
Theory.merge_refs (r1, r2); 
16945  388 

32784  389 
fun merge_thys2 (Thm (_, {thy_ref = r1, ...})) (Thm (_, {thy_ref = r2, ...})) = 
23601  390 
Theory.merge_refs (r1, r2); 
16945  391 

0  392 

22365  393 
(* basic components *) 
16135  394 

28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

395 
val theory_of_thm = Theory.deref o #thy_ref o rep_thm; 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

396 
val maxidx_of = #maxidx o rep_thm; 
19910  397 
fun maxidx_thm th i = Int.max (maxidx_of th, i); 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

398 
val hyps_of = #hyps o rep_thm; 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

399 
val prop_of = #prop o rep_thm; 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

400 
val tpairs_of = #tpairs o rep_thm; 
0  401 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

402 
val concl_of = Logic.strip_imp_concl o prop_of; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

403 
val prems_of = Logic.strip_imp_prems o prop_of; 
21576  404 
val nprems_of = Logic.count_prems o prop_of; 
19305  405 
fun no_prems th = nprems_of th = 0; 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

406 

ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

407 
fun major_prem_of th = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

408 
(case prems_of th of 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

409 
prem :: _ => Logic.strip_assums_concl prem 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

410 
 [] => raise THM ("major_prem_of: rule with no premises", 0, [th])); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

411 

ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

412 
(*the statement of any thm is a cterm*) 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

413 
fun cprop_of (Thm (_, {thy_ref, maxidx, shyps, prop, ...})) = 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

414 
Cterm {thy_ref = thy_ref, maxidx = maxidx, T = propT, t = prop, sorts = shyps}; 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

415 

28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

416 
fun cprem_of (th as Thm (_, {thy_ref, maxidx, shyps, prop, ...})) i = 
18035  417 
Cterm {thy_ref = thy_ref, maxidx = maxidx, T = propT, sorts = shyps, 
18145  418 
t = Logic.nth_prem (i, prop) handle TERM _ => raise THM ("cprem_of", i, [th])}; 
18035  419 

16656  420 
(*explicit transfer to a super theory*) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

421 
fun transfer thy' thm = 
3895  422 
let 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

423 
val Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop}) = thm; 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

424 
val thy = Theory.deref thy_ref; 
26665  425 
val _ = Theory.subthy (thy, thy') orelse raise THM ("transfer: not a super theory", 0, [thm]); 
426 
val is_eq = Theory.eq_thy (thy, thy'); 

24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

427 
val _ = Theory.check_thy thy; 
3895  428 
in 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

429 
if is_eq then thm 
16945  430 
else 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

431 
Thm (der, 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

432 
{thy_ref = Theory.check_thy thy', 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

433 
tags = tags, 
16945  434 
maxidx = maxidx, 
435 
shyps = shyps, 

436 
hyps = hyps, 

437 
tpairs = tpairs, 

28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

438 
prop = prop}) 
3895  439 
end; 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

440 

16945  441 
(*explicit weakening: maps  B to A  B*) 
442 
fun weaken raw_ct th = 

443 
let 

20261  444 
val ct as Cterm {t = A, T, sorts, maxidx = maxidxA, ...} = adjust_maxidx_cterm ~1 raw_ct; 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

445 
val Thm (der, {tags, maxidx, shyps, hyps, tpairs, prop, ...}) = th; 
16945  446 
in 
447 
if T <> propT then 

448 
raise THM ("weaken: assumptions must have type prop", 0, []) 

449 
else if maxidxA <> ~1 then 

450 
raise THM ("weaken: assumptions may not contain schematic variables", maxidxA, []) 

451 
else 

28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

452 
Thm (der, 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

453 
{thy_ref = merge_thys1 ct th, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

454 
tags = tags, 
16945  455 
maxidx = maxidx, 
456 
shyps = Sorts.union sorts shyps, 

28354  457 
hyps = insert_hyps A hyps, 
16945  458 
tpairs = tpairs, 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

459 
prop = prop}) 
16945  460 
end; 
16656  461 

28624  462 
fun weaken_sorts raw_sorts ct = 
463 
let 

464 
val Cterm {thy_ref, t, T, maxidx, sorts} = ct; 

465 
val thy = Theory.deref thy_ref; 

466 
val more_sorts = Sorts.make (map (Sign.certify_sort thy) raw_sorts); 

467 
val sorts' = Sorts.union sorts more_sorts; 

468 
in Cterm {thy_ref = Theory.check_thy thy, t = t, T = T, maxidx = maxidx, sorts = sorts'} end; 

469 

16656  470 
(*dangling sort constraints of a thm*) 
31947
7daee3bed3af
clarified strip_shyps: proper type witnesses for present sorts;
wenzelm
parents:
31945
diff
changeset

471 
fun extra_shyps (th as Thm (_, {shyps, ...})) = 
7daee3bed3af
clarified strip_shyps: proper type witnesses for present sorts;
wenzelm
parents:
31945
diff
changeset

472 
Sorts.subtract (fold_terms Sorts.insert_term th []) shyps; 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

473 

9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

474 

9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

475 

32725  476 
(** derivations and promised proofs **) 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

477 

32059
7991cdf10a54
support for arbitrarity nested future proofs  replaced crude order by explicit normalization (which might loop for bad dependencies);
wenzelm
parents:
32035
diff
changeset

478 
fun make_deriv promises oracles thms proof = 
7991cdf10a54
support for arbitrarity nested future proofs  replaced crude order by explicit normalization (which might loop for bad dependencies);
wenzelm
parents:
32035
diff
changeset

479 
Deriv {promises = promises, body = PBody {oracles = oracles, thms = thms, proof = proof}}; 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

480 

37309  481 
val empty_deriv = make_deriv [] [] [] Proofterm.MinProof; 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

482 

28330  483 

28354  484 
(* inference rules *) 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

485 

28378
60cc0359363d
promise: include check into future body, i.e. joined results are always valid;
wenzelm
parents:
28364
diff
changeset

486 
fun promise_ord ((i, _), (j, _)) = int_ord (j, i); 
28330  487 

28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

488 
fun deriv_rule2 f 
32059
7991cdf10a54
support for arbitrarity nested future proofs  replaced crude order by explicit normalization (which might loop for bad dependencies);
wenzelm
parents:
32035
diff
changeset

489 
(Deriv {promises = ps1, body = PBody {oracles = oras1, thms = thms1, proof = prf1}}) 
7991cdf10a54
support for arbitrarity nested future proofs  replaced crude order by explicit normalization (which might loop for bad dependencies);
wenzelm
parents:
32035
diff
changeset

490 
(Deriv {promises = ps2, body = PBody {oracles = oras2, thms = thms2, proof = prf2}}) = 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

491 
let 
39687  492 
val ps = Ord_List.union promise_ord ps1 ps2; 
44334  493 
val oras = Proofterm.unions_oracles [oras1, oras2]; 
494 
val thms = Proofterm.unions_thms [thms1, thms2]; 

28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

495 
val prf = 
37309  496 
(case ! Proofterm.proofs of 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

497 
2 => f prf1 prf2 
28804
5d3b1df16353
refined notion of derivation, consiting of promises and proof_body;
wenzelm
parents:
28675
diff
changeset

498 
 1 => MinProof 
5d3b1df16353
refined notion of derivation, consiting of promises and proof_body;
wenzelm
parents:
28675
diff
changeset

499 
 0 => MinProof 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

500 
 i => error ("Illegal level of detail for proof objects: " ^ string_of_int i)); 
32059
7991cdf10a54
support for arbitrarity nested future proofs  replaced crude order by explicit normalization (which might loop for bad dependencies);
wenzelm
parents:
32035
diff
changeset

501 
in make_deriv ps oras thms prf end; 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

502 

9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

503 
fun deriv_rule1 f = deriv_rule2 (K f) empty_deriv; 
32059
7991cdf10a54
support for arbitrarity nested future proofs  replaced crude order by explicit normalization (which might loop for bad dependencies);
wenzelm
parents:
32035
diff
changeset

504 
fun deriv_rule0 prf = deriv_rule1 I (make_deriv [] [] [] prf); 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

505 

36621
2fd4e2c76636
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
wenzelm
parents:
36619
diff
changeset

506 
fun deriv_rule_unconditional f (Deriv {promises, body = PBody {oracles, thms, proof}}) = 
2fd4e2c76636
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
wenzelm
parents:
36619
diff
changeset

507 
make_deriv promises oracles thms (f proof); 
2fd4e2c76636
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
wenzelm
parents:
36619
diff
changeset

508 

1238  509 

32725  510 
(* fulfilled proofs *) 
511 

44331  512 
fun raw_body_of (Thm (Deriv {body, ...}, _)) = body; 
513 
fun raw_promises_of (Thm (Deriv {promises, ...}, _)) = promises; 

514 

515 
fun join_promises [] = () 

516 
 join_promises promises = join_promises_of (Future.joins (map snd promises)) 

49008
a3cdb49c22cc
proper merge of promises to avoid exponential blowup in pathologic situations (e.g. lack of PThm wrapping);
wenzelm
parents:
48263
diff
changeset

517 
and join_promises_of thms = join_promises (Ord_List.make promise_ord (maps raw_promises_of thms)); 
32725  518 

519 
fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) = 

44331  520 
Proofterm.fulfill_norm_proof (Theory.deref thy_ref) (fulfill_promises promises) body 
521 
and fulfill_promises promises = 

522 
map fst promises ~~ map fulfill_body (Future.joins (map snd promises)); 

32725  523 

44333
cc53ce50f738
reverted to join_bodies/join_proofs based on fold_body_thms to regain performance (escpecially of HOLProofs)  see also aa9c1e9ef2ce and 4e2abb045eac;
wenzelm
parents:
44331
diff
changeset

524 
fun proof_bodies_of thms = 
cc53ce50f738
reverted to join_bodies/join_proofs based on fold_body_thms to regain performance (escpecially of HOLProofs)  see also aa9c1e9ef2ce and 4e2abb045eac;
wenzelm
parents:
44331
diff
changeset

525 
let 
cc53ce50f738
reverted to join_bodies/join_proofs based on fold_body_thms to regain performance (escpecially of HOLProofs)  see also aa9c1e9ef2ce and 4e2abb045eac;
wenzelm
parents:
44331
diff
changeset

526 
val _ = join_promises_of thms; 
cc53ce50f738
reverted to join_bodies/join_proofs based on fold_body_thms to regain performance (escpecially of HOLProofs)  see also aa9c1e9ef2ce and 4e2abb045eac;
wenzelm
parents:
44331
diff
changeset

527 
val bodies = map fulfill_body thms; 
cc53ce50f738
reverted to join_bodies/join_proofs based on fold_body_thms to regain performance (escpecially of HOLProofs)  see also aa9c1e9ef2ce and 4e2abb045eac;
wenzelm
parents:
44331
diff
changeset

528 
val _ = Proofterm.join_bodies bodies; 
cc53ce50f738
reverted to join_bodies/join_proofs based on fold_body_thms to regain performance (escpecially of HOLProofs)  see also aa9c1e9ef2ce and 4e2abb045eac;
wenzelm
parents:
44331
diff
changeset

529 
in bodies end; 
cc53ce50f738
reverted to join_bodies/join_proofs based on fold_body_thms to regain performance (escpecially of HOLProofs)  see also aa9c1e9ef2ce and 4e2abb045eac;
wenzelm
parents:
44331
diff
changeset

530 

cc53ce50f738
reverted to join_bodies/join_proofs based on fold_body_thms to regain performance (escpecially of HOLProofs)  see also aa9c1e9ef2ce and 4e2abb045eac;
wenzelm
parents:
44331
diff
changeset

531 
val proof_body_of = singleton proof_bodies_of; 
44331  532 
val proof_of = Proofterm.proof_of o proof_body_of; 
32725  533 

44333
cc53ce50f738
reverted to join_bodies/join_proofs based on fold_body_thms to regain performance (escpecially of HOLProofs)  see also aa9c1e9ef2ce and 4e2abb045eac;
wenzelm
parents:
44331
diff
changeset

534 
val join_proofs = ignore o proof_bodies_of; 
32725  535 

536 

537 
(* derivation status *) 

538 

50126
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
49008
diff
changeset

539 
fun peek_status (Thm (Deriv {promises, body}, _)) = 
32725  540 
let 
541 
val ps = map (Future.peek o snd) promises; 

542 
val bodies = body :: 

44331  543 
map_filter (fn SOME (Exn.Res th) => SOME (raw_body_of th)  _ => NONE) ps; 
50126
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
49008
diff
changeset

544 
val {oracle, unfinished, failed} = Proofterm.peek_status bodies; 
32725  545 
in 
546 
{oracle = oracle, 

547 
unfinished = unfinished orelse exists is_none ps, 

548 
failed = failed orelse exists (fn SOME (Exn.Exn _) => true  _ => false) ps} 

549 
end; 

550 

551 

552 
(* future rule *) 

553 

36613
f3157c288aca
simplified primitive Thm.future: more direct theory check, do not hardwire strip_shyps here;
wenzelm
parents:
36330
diff
changeset

554 
fun future_result i orig_thy orig_shyps orig_prop thm = 
32725  555 
let 
36613
f3157c288aca
simplified primitive Thm.future: more direct theory check, do not hardwire strip_shyps here;
wenzelm
parents:
36330
diff
changeset

556 
fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]); 
f3157c288aca
simplified primitive Thm.future: more direct theory check, do not hardwire strip_shyps here;
wenzelm
parents:
36330
diff
changeset

557 
val Thm (Deriv {promises, ...}, {thy_ref, shyps, hyps, tpairs, prop, ...}) = thm; 
f3157c288aca
simplified primitive Thm.future: more direct theory check, do not hardwire strip_shyps here;
wenzelm
parents:
36330
diff
changeset

558 

f3157c288aca
simplified primitive Thm.future: more direct theory check, do not hardwire strip_shyps here;
wenzelm
parents:
36330
diff
changeset

559 
val _ = Theory.eq_thy (Theory.deref thy_ref, orig_thy) orelse err "bad theory"; 
32725  560 
val _ = Theory.check_thy orig_thy; 
561 
val _ = prop aconv orig_prop orelse err "bad prop"; 

562 
val _ = null tpairs orelse err "bad tpairs"; 

563 
val _ = null hyps orelse err "bad hyps"; 

564 
val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps"; 

565 
val _ = forall (fn (j, _) => i <> j) promises orelse err "bad dependencies"; 

44331  566 
val _ = join_promises promises; 
32725  567 
in thm end; 
568 

569 
fun future future_thm ct = 

570 
let 

571 
val Cterm {thy_ref = thy_ref, t = prop, T, maxidx, sorts} = ct; 

572 
val thy = Context.reject_draft (Theory.deref thy_ref); 

573 
val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]); 

574 

575 
val i = serial (); 

576 
val future = future_thm > Future.map (future_result i thy sorts prop); 

577 
in 

37309  578 
Thm (make_deriv [(i, future)] [] [] (Proofterm.promise_proof thy i prop), 
32725  579 
{thy_ref = thy_ref, 
580 
tags = [], 

581 
maxidx = maxidx, 

582 
shyps = sorts, 

583 
hyps = [], 

584 
tpairs = [], 

585 
prop = prop}) 

586 
end; 

587 

588 

589 
(* closed derivations with official name *) 

590 

41699  591 
(*nondeterministic, depends on unknown promises*) 
37297  592 
fun derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) = 
37309  593 
Proofterm.get_name shyps hyps prop (Proofterm.proof_of body); 
32725  594 

36744
6e1f3d609a68
renamed Thm.get_name > Thm.derivation_name and Thm.put_name > Thm.name_derivation, to emphasize the true nature of these operations;
wenzelm
parents:
36742
diff
changeset

595 
fun name_derivation name (thm as Thm (der, args)) = 
32725  596 
let 
597 
val Deriv {promises, body} = der; 

36882
f33760bb8ca0
conditionally unconstrain thm proofs  loosely based on the version by krauss/schropp;
wenzelm
parents:
36770
diff
changeset

598 
val {thy_ref, shyps, hyps, prop, tpairs, ...} = args; 
32725  599 
val _ = null tpairs orelse raise THM ("put_name: unsolved flexflex constraints", 0, [thm]); 
600 

41700
f33d5a00c25d
thm_proof: visible fulfill_body only, without joining nested thms  retain proof irrelevance, which is important for parallel performance;
wenzelm
parents:
41699
diff
changeset

601 
val ps = map (apsnd (Future.map fulfill_body)) promises; 
32725  602 
val thy = Theory.deref thy_ref; 
37309  603 
val (pthm, proof) = Proofterm.thm_proof thy name shyps hyps prop ps body; 
32725  604 
val der' = make_deriv [] [] [pthm] proof; 
605 
val _ = Theory.check_thy thy; 

606 
in Thm (der', args) end; 

607 

608 

1238  609 

1529  610 
(** Axioms **) 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

611 

28675
fb68c0767004
renamed get_axiom_i to axiom, removed obsolete get_axiom;
wenzelm
parents:
28648
diff
changeset

612 
fun axiom theory name = 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

613 
let 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

614 
fun get_ax thy = 
22685  615 
Symtab.lookup (Theory.axiom_table thy) name 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

616 
> Option.map (fn prop => 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

617 
let 
37309  618 
val der = deriv_rule0 (Proofterm.axm_proof name prop); 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

619 
val maxidx = maxidx_of_term prop; 
26640
92e6d3ec91bd
simplified handling of sorts, removed unnecessary universal witness;
wenzelm
parents:
26631
diff
changeset

620 
val shyps = Sorts.insert_term prop []; 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

621 
in 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

622 
Thm (der, {thy_ref = Theory.check_thy thy, tags = [], 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

623 
maxidx = maxidx, shyps = shyps, hyps = [], tpairs = [], prop = prop}) 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

624 
end); 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

625 
in 
42425  626 
(case get_first get_ax (Theory.nodes_of theory) of 
15531  627 
SOME thm => thm 
628 
 NONE => raise THEORY ("No axiom " ^ quote name, [theory])) 

387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

629 
end; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

630 

776
df8f91c0e57c
improved axioms_of: returns thms as the manual says;
wenzelm
parents:
721
diff
changeset

631 
(*return additional axioms of this theory node*) 
df8f91c0e57c
improved axioms_of: returns thms as the manual says;
wenzelm
parents:
721
diff
changeset

632 
fun axioms_of thy = 
28675
fb68c0767004
renamed get_axiom_i to axiom, removed obsolete get_axiom;
wenzelm
parents:
28648
diff
changeset

633 
map (fn s => (s, axiom thy s)) (Symtab.keys (Theory.axiom_table thy)); 
776
df8f91c0e57c
improved axioms_of: returns thms as the manual says;
wenzelm
parents:
721
diff
changeset

634 

6089  635 

28804
5d3b1df16353
refined notion of derivation, consiting of promises and proof_body;
wenzelm
parents:
28675
diff
changeset

636 
(* tags *) 
6089  637 

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

638 
val get_tags = #tags o rep_thm; 
6089  639 

28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

640 
fun map_tags f (Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) = 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

641 
Thm (der, {thy_ref = thy_ref, tags = f tags, maxidx = maxidx, 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

642 
shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}); 
0  643 

644 

43795
ca5896a836ba
recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck;
wenzelm
parents:
43761
diff
changeset

645 
(* technical adjustments *) 
ca5896a836ba
recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck;
wenzelm
parents:
43761
diff
changeset

646 

28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

647 
fun norm_proof (Thm (der, args as {thy_ref, ...})) = 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

648 
let 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

649 
val thy = Theory.deref thy_ref; 
37309  650 
val der' = deriv_rule1 (Proofterm.rew_proof thy) der; 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

651 
val _ = Theory.check_thy thy; 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

652 
in Thm (der', args) end; 
23781
ab793a6ddf9f
Added function norm_proof for normalizing the proof term
berghofe
parents:
23657
diff
changeset

653 

28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

654 
fun adjust_maxidx_thm i (th as Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) = 
20261  655 
if maxidx = i then th 
656 
else if maxidx < i then 

28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

657 
Thm (der, {maxidx = i, thy_ref = thy_ref, tags = tags, shyps = shyps, 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

658 
hyps = hyps, tpairs = tpairs, prop = prop}) 
20261  659 
else 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

660 
Thm (der, {maxidx = Int.max (maxidx_tpairs tpairs (maxidx_of_term prop), i), thy_ref = thy_ref, 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

661 
tags = tags, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}); 
564  662 

387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

663 

2509  664 

1529  665 
(*** Meta rules ***) 
0  666 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

667 
(** primitive rules **) 
0  668 

16656  669 
(*The assumption rule A  A*) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

670 
fun assume raw_ct = 
20261  671 
let val Cterm {thy_ref, t = prop, T, maxidx, sorts} = adjust_maxidx_cterm ~1 raw_ct in 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

672 
if T <> propT then 
19230  673 
raise THM ("assume: prop", 0, []) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

674 
else if maxidx <> ~1 then 
19230  675 
raise THM ("assume: variables", maxidx, []) 
37309  676 
else Thm (deriv_rule0 (Proofterm.Hyp prop), 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

677 
{thy_ref = thy_ref, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

678 
tags = [], 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

679 
maxidx = ~1, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

680 
shyps = sorts, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

681 
hyps = [prop], 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

682 
tpairs = [], 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

683 
prop = prop}) 
0  684 
end; 
685 

1220  686 
(*Implication introduction 
3529  687 
[A] 
688 
: 

689 
B 

1220  690 
 
691 
A ==> B 

692 
*) 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

693 
fun implies_intr 
16679  694 
(ct as Cterm {t = A, T, maxidx = maxidxA, sorts, ...}) 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

695 
(th as Thm (der, {maxidx, hyps, shyps, tpairs, prop, ...})) = 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

696 
if T <> propT then 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

697 
raise THM ("implies_intr: assumptions must have type prop", 0, [th]) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

698 
else 
37309  699 
Thm (deriv_rule1 (Proofterm.implies_intr_proof A) der, 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

700 
{thy_ref = merge_thys1 ct th, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

701 
tags = [], 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

702 
maxidx = Int.max (maxidxA, maxidx), 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

703 
shyps = Sorts.union sorts shyps, 
28354  704 
hyps = remove_hyps A hyps, 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

705 
tpairs = tpairs, 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

706 
prop = Logic.mk_implies (A, prop)}); 
0  707 

1529  708 

1220  709 
(*Implication elimination 
710 
A ==> B A 

711 
 

712 
B 

713 
*) 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

714 
fun implies_elim thAB thA = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

715 
let 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

716 
val Thm (derA, {maxidx = maxA, hyps = hypsA, shyps = shypsA, tpairs = tpairsA, 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

717 
prop = propA, ...}) = thA 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

718 
and Thm (der, {maxidx, hyps, shyps, tpairs, prop, ...}) = thAB; 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

719 
fun err () = raise THM ("implies_elim: major premise", 0, [thAB, thA]); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

720 
in 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

721 
case prop of 
20512  722 
Const ("==>", _) $ A $ B => 
723 
if A aconv propA then 

37309  724 
Thm (deriv_rule2 (curry Proofterm.%%) der derA, 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

725 
{thy_ref = merge_thys2 thAB thA, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

726 
tags = [], 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

727 
maxidx = Int.max (maxA, maxidx), 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

728 
shyps = Sorts.union shypsA shyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

729 
hyps = union_hyps hypsA hyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

730 
tpairs = union_tpairs tpairsA tpairs, 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

731 
prop = B}) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

732 
else err () 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

733 
 _ => err () 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

734 
end; 
250  735 

1220  736 
(*Forall introduction. The Free or Var x must not be free in the hypotheses. 
16656  737 
[x] 
738 
: 

739 
A 

740 
 

741 
!!x. A 

1220  742 
*) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

743 
fun forall_intr 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

744 
(ct as Cterm {t = x, T, sorts, ...}) 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

745 
(th as Thm (der, {maxidx, shyps, hyps, tpairs, prop, ...})) = 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

746 
let 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

747 
fun result a = 
37309  748 
Thm (deriv_rule1 (Proofterm.forall_intr_proof x a) der, 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

749 
{thy_ref = merge_thys1 ct th, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

750 
tags = [], 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

751 
maxidx = maxidx, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

752 
shyps = Sorts.union sorts shyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

753 
hyps = hyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

754 
tpairs = tpairs, 
46217
7b19666f0e3d
renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
wenzelm
parents:
45443
diff
changeset

755 
prop = Logic.all_const T $ Abs (a, T, abstract_over (x, prop))}); 
21798  756 
fun check_occs a x ts = 
16847
8fc160b12e73
invoke_oracle: do not keep theory value, but theory_ref;
wenzelm
parents:
16725
diff
changeset

757 
if exists (fn t => Logic.occs (x, t)) ts then 
21798  758 
raise THM ("forall_intr: variable " ^ quote a ^ " free in assumptions", 0, [th]) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

759 
else (); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

760 
in 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

761 
case x of 
21798  762 
Free (a, _) => (check_occs a x hyps; check_occs a x (terms_of_tpairs tpairs); result a) 
763 
 Var ((a, _), _) => (check_occs a x (terms_of_tpairs tpairs); result a) 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

764 
 _ => raise THM ("forall_intr: not a variable", 0, [th]) 
0  765 
end; 
766 

1220  767 
(*Forall elimination 
16656  768 
!!x. A 
1220  769 
 
770 
A[t/x] 

771 
*) 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

772 
fun forall_elim 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

773 
(ct as Cterm {t, T, maxidx = maxt, sorts, ...}) 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

774 
(th as Thm (der, {maxidx, shyps, hyps, tpairs, prop, ...})) = 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

775 
(case prop of 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

776 
Const ("all", Type ("fun", [Type ("fun", [qary, _]), _])) $ A => 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

777 
if T <> qary then 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

778 
raise THM ("forall_elim: type mismatch", 0, [th]) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

779 
else 
37309  780 
Thm (deriv_rule1 (Proofterm.% o rpair (SOME t)) der, 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

781 
{thy_ref = merge_thys1 ct th, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

782 
tags = [], 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

783 
maxidx = Int.max (maxidx, maxt), 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

784 
shyps = Sorts.union sorts shyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

785 
hyps = hyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

786 
tpairs = tpairs, 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

787 
prop = Term.betapply (A, t)}) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

788 
 _ => raise THM ("forall_elim: not quantified", 0, [th])); 
0  789 

790 

1220  791 
(* Equality *) 
0  792 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

793 
(*Reflexivity 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

794 
t == t 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

795 
*) 
32784  796 
fun reflexive (Cterm {thy_ref, t, T = _, maxidx, sorts}) = 
37309  797 
Thm (deriv_rule0 Proofterm.reflexive, 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

798 
{thy_ref = thy_ref, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

799 
tags = [], 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

800 
maxidx = maxidx, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

801 
shyps = sorts, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

802 
hyps = [], 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

803 
tpairs = [], 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

804 
prop = Logic.mk_equals (t, t)}); 
0  805 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

806 
(*Symmetry 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

807 
t == u 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

808 
 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

809 
u == t 
1220  810 
*) 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

811 
fun symmetric (th as Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) = 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

812 
(case prop of 
32784  813 
(eq as Const ("==", _)) $ t $ u => 
37309  814 
Thm (deriv_rule1 Proofterm.symmetric der, 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

815 
{thy_ref = thy_ref, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

816 
tags = [], 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

817 
maxidx = maxidx, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

818 
shyps = shyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

819 
hyps = hyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

820 
tpairs = tpairs, 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

821 
prop = eq $ u $ t}) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

822 
 _ => raise THM ("symmetric", 0, [th])); 
0  823 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

824 
(*Transitivity 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

825 
t1 == u u == t2 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

826 
 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

827 
t1 == t2 
1220  828 
*) 
0  829 
fun transitive th1 th2 = 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

830 
let 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

831 
val Thm (der1, {maxidx = max1, hyps = hyps1, shyps = shyps1, tpairs = tpairs1, 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

832 
prop = prop1, ...}) = th1 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

833 
and Thm (der2, {maxidx = max2, hyps = hyps2, shyps = shyps2, tpairs = tpairs2, 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

834 
prop = prop2, ...}) = th2; 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

835 
fun err msg = raise THM ("transitive: " ^ msg, 0, [th1, th2]); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

836 
in 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

837 
case (prop1, prop2) of 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

838 
((eq as Const ("==", Type (_, [T, _]))) $ t1 $ u, Const ("==", _) $ u' $ t2) => 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

839 
if not (u aconv u') then err "middle term" 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

840 
else 
37309  841 
Thm (deriv_rule2 (Proofterm.transitive u T) der1 der2, 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

842 
{thy_ref = merge_thys2 th1 th2, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

843 
tags = [], 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

844 
maxidx = Int.max (max1, max2), 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

845 
shyps = Sorts.union shyps1 shyps2, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

846 
hyps = union_hyps hyps1 hyps2, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

847 
tpairs = union_tpairs tpairs1 tpairs2, 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

848 
prop = eq $ t1 $ t2}) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

849 
 _ => err "premises" 
0  850 
end; 
851 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

852 
(*Betaconversion 
16656  853 
(%x. t)(u) == t[u/x] 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

854 
fully betareduces the term if full = true 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

855 
*) 
32784  856 
fun beta_conversion full (Cterm {thy_ref, t, T = _, maxidx, sorts}) = 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

857 
let val t' = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

858 
if full then Envir.beta_norm t 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

859 
else 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

860 
(case t of Abs (_, _, bodt) $ u => subst_bound (u, bodt) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

861 
 _ => raise THM ("beta_conversion: not a redex", 0, [])); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

862 
in 
37309  863 
Thm (deriv_rule0 Proofterm.reflexive, 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

864 
{thy_ref = thy_ref, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

865 
tags = [], 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

866 
maxidx = maxidx, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

867 
shyps = sorts, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

868 
hyps = [], 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

869 
tpairs = [], 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

870 
prop = Logic.mk_equals (t, t')}) 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

871 
end; 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

872 

32784  873 
fun eta_conversion (Cterm {thy_ref, t, T = _, maxidx, sorts}) = 
37309  874 
Thm (deriv_rule0 Proofterm.reflexive, 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

875 
{thy_ref = thy_ref, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

876 
tags = [], 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

877 
maxidx = maxidx, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

878 
shyps = sorts, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

879 
hyps = [], 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

880 
tpairs = [], 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

881 
prop = Logic.mk_equals (t, Envir.eta_contract t)}); 
0  882 

32784  883 
fun eta_long_conversion (Cterm {thy_ref, t, T = _, maxidx, sorts}) = 
37309  884 
Thm (deriv_rule0 Proofterm.reflexive, 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

885 
{thy_ref = thy_ref, 
23493  886 
tags = [], 
887 
maxidx = maxidx, 

888 
shyps = sorts, 

889 
hyps = [], 

890 
tpairs = [], 

52131  891 
prop = Logic.mk_equals (t, Envir.eta_long [] t)}); 
23493  892 

0  893 
(*The abstraction rule. The Free or Var x must not be free in the hypotheses. 
894 
The bound variable will be named "a" (since x will be something like x320) 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

895 
t == u 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

896 
 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

897 
%x. t == %x. u 
1220  898 
*) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

899 
fun abstract_rule a 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

900 
(Cterm {t = x, T, sorts, ...}) 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

901 
(th as Thm (der, {thy_ref, maxidx, hyps, shyps, tpairs, prop, ...})) = 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

902 
let 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

903 
val (t, u) = Logic.dest_equals prop 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

904 
handle TERM _ => raise THM ("abstract_rule: premise not an equality", 0, [th]); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

905 
val result = 
37309  906 
Thm (deriv_rule1 (Proofterm.abstract_rule x a) der, 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

907 
{thy_ref = thy_ref, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

908 
tags = [], 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

909 
maxidx = maxidx, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

910 
shyps = Sorts.union sorts shyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

911 
hyps = hyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

912 
tpairs = tpairs, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

913 
prop = Logic.mk_equals 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

914 
(Abs (a, T, abstract_over (x, t)), Abs (a, T, abstract_over (x, u)))}); 
21798  915 
fun check_occs a x ts = 
16847
8fc160b12e73
invoke_oracle: do not keep theory value, but theory_ref;
wenzelm
parents:
16725
diff
changeset

916 
if exists (fn t => Logic.occs (x, t)) ts then 
21798  917 
raise THM ("abstract_rule: variable " ^ quote a ^ " free in assumptions", 0, [th]) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

918 
else (); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

919 
in 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

920 
case x of 
21798  921 
Free (a, _) => (check_occs a x hyps; check_occs a x (terms_of_tpairs tpairs); result) 
922 
 Var ((a, _), _) => (check_occs a x (terms_of_tpairs tpairs); result) 

923 
 _ => raise THM ("abstract_rule: not a variable", 0, [th]) 

0  924 
end; 
925 

926 
(*The combination rule 

3529  927 
f == g t == u 
928 
 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

929 
f t == g u 
1220  930 
*) 
0  931 
fun combination th1 th2 = 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

932 
let 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

933 
val Thm (der1, {maxidx = max1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1, 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

934 
prop = prop1, ...}) = th1 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

935 
and Thm (der2, {maxidx = max2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2, 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

936 
prop = prop2, ...}) = th2; 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

937 
fun chktypes fT tT = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

938 
(case fT of 
32784  939 
Type ("fun", [T1, _]) => 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

940 
if T1 <> tT then 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

941 
raise THM ("combination: types", 0, [th1, th2]) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

942 
else () 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

943 
 _ => raise THM ("combination: not function type", 0, [th1, th2])); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

944 
in 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

945 
case (prop1, prop2) of 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

946 
(Const ("==", Type ("fun", [fT, _])) $ f $ g, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

947 
Const ("==", Type ("fun", [tT, _])) $ t $ u) => 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

948 
(chktypes fT tT; 
37309  949 
Thm (deriv_rule2 (Proofterm.combination f g t u fT) der1 der2, 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

950 
{thy_ref = merge_thys2 th1 th2, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

951 
tags = [], 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

952 
maxidx = Int.max (max1, max2), 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

953 
shyps = Sorts.union shyps1 shyps2, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

954 
hyps = union_hyps hyps1 hyps2, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

955 
tpairs = union_tpairs tpairs1 tpairs2, 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

956 
prop = Logic.mk_equals (f $ t, g $ u)})) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

957 
 _ => raise THM ("combination: premises", 0, [th1, th2]) 
0  958 
end; 
959 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

960 
(*Equality introduction 
3529  961 
A ==> B B ==> A 
962 
 

963 
A == B 

1220  964 
*) 
0  965 
fun equal_intr th1 th2 = 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

966 
let 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

967 
val Thm (der1, {maxidx = max1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1, 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

968 
prop = prop1, ...}) = th1 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

969 
and Thm (der2, {maxidx = max2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2, 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

970 
prop = prop2, ...}) = th2; 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

971 
fun err msg = raise THM ("equal_intr: " ^ msg, 0, [th1, th2]); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

972 
in 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

973 
case (prop1, prop2) of 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

974 
(Const("==>", _) $ A $ B, Const("==>", _) $ B' $ A') => 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

975 
if A aconv A' andalso B aconv B' then 
37309  976 
Thm (deriv_rule2 (Proofterm.equal_intr A B) der1 der2, 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

977 
{thy_ref = merge_thys2 th1 th2, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

978 
tags = [], 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

979 
maxidx = Int.max (max1, max2), 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

980 
shyps = Sorts.union shyps1 shyps2, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

981 
hyps = union_hyps hyps1 hyps2, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

982 
tpairs = union_tpairs tpairs1 tpairs2, 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

983 
prop = Logic.mk_equals (A, B)}) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

984 
else err "not equal" 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

985 
 _ => err "premises" 
1529  986 
end; 
987 

988 
(*The equal propositions rule 

3529  989 
A == B A 
1529  990 
 
991 
B 

992 
*) 

993 
fun equal_elim th1 th2 = 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

994 
let 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

995 
val Thm (der1, {maxidx = max1, shyps = shyps1, hyps = hyps1, 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

996 
tpairs = tpairs1, prop = prop1, ...}) = th1 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

997 
and Thm (der2, {maxidx = max2, shyps = shyps2, hyps = hyps2, 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

998 
tpairs = tpairs2, prop = prop2, ...}) = th2; 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

999 
fun err msg = raise THM ("equal_elim: " ^ msg, 0, [th1, th2]); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1000 
in 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1001 
case prop1 of 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1002 
Const ("==", _) $ A $ B => 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1003 
if prop2 aconv A then 
37309  1004 
Thm (deriv_rule2 (Proofterm.equal_elim A B) der1 der2, 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

1005 
{thy_ref = merge_thys2 th1 th2, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

1006 
tags = [], 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1007 
maxidx = Int.max (max1, max2), 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1008 
shyps = Sorts.union shyps1 shyps2, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1009 
hyps = union_hyps hyps1 hyps2, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1010 
tpairs = union_tpairs tpairs1 tpairs2, 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

1011 
prop = B}) 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1012 
else err "not equal" 
1529  1013 
 _ => err"major premise" 
1014 
end; 

0  1015 

1220  1016 

1017 

0  1018 
(**** Derived rules ****) 
1019 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1020 
(*Smash unifies the list of term pairs leaving no flexflex pairs. 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

1021 
Instantiates the theorem and deletes trivial tpairs. Resulting 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

1022 
sequence may contain multiple elements if the tpairs are not all 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

1023 
flexflex.*) 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

1024 
fun flexflex_rule (th as Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) = 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

1025 
let val thy = Theory.deref thy_ref in 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

1026 
Unify.smash_unifiers thy tpairs (Envir.empty maxidx) 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

1027 
> Seq.map (fn env => 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

1028 
if Envir.is_empty env then th 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

1029 
else 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

1030 
let 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

1031 
val tpairs' = tpairs > map (pairself (Envir.norm_term env)) 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

1032 
(*remove trivial tpairs, of the form t==t*) 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

1033 
> filter_out (op aconv); 
37309  1034 
val der' = deriv_rule1 (Proofterm.norm_proof' env) der; 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

1035 
val prop' = Envir.norm_term env prop; 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

1036 
val maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop'); 
26640
92e6d3ec91bd
simplified handling of sorts, removed unnecessary universal witness;
wenzelm
parents:
26631
diff
changeset

1037 
val shyps = Envir.insert_sorts env shyps; 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

1038 
in 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

1039 
Thm (der', {thy_ref = Theory.check_thy thy, tags = [], maxidx = maxidx, 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

1040 
shyps = shyps, hyps = hyps, tpairs = tpairs', prop = prop'}) 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

1041 
end) 
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

1042 
end; 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1043 

0  1044 

19910  1045 
(*Generalization of fixed variables 
1046 
A 

1047 
 

1048 
A[?'a/'a, ?x/x, ...] 

1049 
*) 

1050 

1051 
fun generalize ([], []) _ th = th 

1052 
 generalize (tfrees, frees) idx th = 

1053 
let 

28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

1054 
val Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...}) = th; 
19910  1055 
val _ = idx <= maxidx andalso raise THM ("generalize: bad index", idx, [th]); 
1056 

33697  1057 
val bad_type = 
1058 
if null tfrees then K false 

1059 
else Term.exists_subtype (fn TFree (a, _) => member (op =) tfrees a  _ => false); 

19910  1060 
fun bad_term (Free (x, T)) = bad_type T orelse member (op =) frees x 
1061 
 bad_term (Var (_, T)) = bad_type T 

1062 
 bad_term (Const (_, T)) = bad_type T 

1063 
 bad_term (Abs (_, T, t)) = bad_type T orelse bad_term t 

1064 
 bad_term (t $ u) = bad_term t orelse bad_term u 

1065 
 bad_term (Bound _) = false; 

1066 
val _ = exists bad_term hyps andalso 

1067 
raise THM ("generalize: variable free in assumptions", 0, [th]); 

1068 

31977  1069 
val gen = Term_Subst.generalize (tfrees, frees) idx; 
19910  1070 
val prop' = gen prop; 
1071 
val tpairs' = map (pairself gen) tpairs; 

1072 
val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop'); 

1073 
in 

37309  1074 
Thm (deriv_rule1 (Proofterm.generalize (tfrees, frees) idx) der, 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

1075 
{thy_ref = thy_ref, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

1076 
tags = [], 
19910  1077 
maxidx = maxidx', 
1078 
shyps = shyps, 

1079 
hyps = hyps, 

1080 
tpairs = tpairs', 

28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

1081 
prop = prop'}) 
19910  1082 
end; 
1083 

1084 

22584  1085 
(*Instantiation of schematic variables 
16656  1086 
A 
1087 
 

1088 
A[t1/v1, ..., tn/vn] 

1220  1089 
*) 
0  1090 

6928  1091 
local 
1092 

26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26832
diff
changeset

1093 
fun pretty_typing thy t T = Pretty.block 
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26832
diff
changeset

1094 
[Syntax.pretty_term_global thy t, Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ_global thy T]; 
15797  1095 

16884
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

1096 
fun add_inst (ct, cu) (thy_ref, sorts) = 
6928  1097 
let 
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26832
diff
changeset

1098 
val Cterm {t = t, T = T, ...} = ct; 
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26832
diff
changeset

1099 
val Cterm {t = u, T = U, sorts = sorts_u, maxidx = maxidx_u, ...} = cu; 
16884
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

1100 
val thy_ref' = Theory.merge_refs (thy_ref, merge_thys0 ct cu); 
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

1101 
val sorts' = Sorts.union sorts_u sorts; 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

1102 
in 
16884
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

1103 
(case t of Var v => 
20512  1104 
if T = U then ((v, (u, maxidx_u)), (thy_ref', sorts')) 
16884
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

1105 
else raise TYPE (Pretty.string_of (Pretty.block 
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

1106 
[Pretty.str "instantiate: type conflict", 
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

1107 
Pretty.fbrk, pretty_typing (Theory.deref thy_ref') t T, 
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

1108 
Pretty.fbrk, pretty_typing (Theory.deref thy_ref') u U]), [T, U], [t, u]) 
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

1109 
 _ => raise TYPE (Pretty.string_of (Pretty.block 
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

1110 
[Pretty.str "instantiate: not a variable", 
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26832
diff
changeset

1111 
Pretty.fbrk, Syntax.pretty_term_global (Theory.deref thy_ref') t]), [], [t])) 
0  1112 
end; 
1113 

16884
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

1114 
fun add_instT (cT, cU) (thy_ref, sorts) = 
16656  1115 
let 
16884
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

1116 
val Ctyp {T, thy_ref = thy_ref1, ...} = cT 
20512  1117 
and Ctyp {T = U, thy_ref = thy_ref2, sorts = sorts_U, maxidx = maxidx_U, ...} = cU; 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

1118 
val thy' = Theory.deref (Theory.merge_refs (thy_ref, Theory.merge_refs (thy_ref1, thy_ref2))); 
16884
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

1119 
val sorts' = Sorts.union sorts_U sorts; 
16656  1120 
in 
16884
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

1121 
(case T of TVar (v as (_, S)) => 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

1122 
if Sign.of_sort thy' (U, S) then ((v, (U, maxidx_U)), (Theory.check_thy thy', sorts')) 
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26832
diff
changeset

1123 
else raise TYPE ("Type not of sort " ^ Syntax.string_of_sort_global thy' S, [U], []) 
16656  1124 
 _ => raise TYPE (Pretty.string_of (Pretty.block 
15797  1125 
[Pretty.str "instantiate: not a type variable", 
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26832
diff
changeset

1126 
Pretty.fbrk, Syntax.pretty_typ_global thy' T]), [T], [])) 
16656  1127 
end; 
0  1128 

6928  1129 
in 
1130 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1131 
(*Lefttoright replacements: ctpairs = [..., (vi, ti), ...]. 
0  1132 
Instantiates distinct Vars by terms of same type. 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1133 
Does NOT normalize the resulting theorem!*) 
1529  1134 
fun instantiate ([], []) th = th 
16884
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

1135 
 instantiate (instT, inst) th = 
16656  1136 
let 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

1137 
val Thm (der, {thy_ref, hyps, shyps, tpairs, prop, ...}) = th; 
16884
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

1138 
val (inst', (instT', (thy_ref', shyps'))) = 
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

1139 
(thy_ref, shyps) > fold_map add_inst inst > fold_map add_instT instT; 
31977  1140 
val subst = Term_Subst.instantiate_maxidx (instT', inst'); 
20512  1141 
val (prop', maxidx1) = subst prop ~1; 
1142 
val (tpairs', maxidx') = 

1143 
fold_map (fn (t, u) => fn i => subst t i >> subst u) tpairs maxidx1; 

16656  1144 
in 
37309  1145 
Thm (deriv_rule1 
1146 
(fn d => Proofterm.instantiate (map (apsnd #1) instT', map (apsnd #1) inst') d) der, 

28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

1147 
{thy_ref = thy_ref', 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

1148 
tags = [], 
20545
4c1068697159
instantiate: omit has_duplicates check, which is irrelevant for soundness;
wenzelm
parents:
20512
diff
changeset

1149 
maxidx = maxidx', 
4c1068697159
instantiate: omit has_duplicates check, which is irrelevant for soundness;
wenzelm
parents:
20512
diff
changeset

1150 
shyps = shyps', 
4c1068697159
instantiate: omit has_duplicates check, which is irrelevant for soundness;
wenzelm
parents:
20512
diff
changeset

1151 
hyps = hyps, 
4c1068697159
instantiate: omit has_duplicates check, which is irrelevant for soundness;
wenzelm
parents:
20512
diff
changeset

1152 
tpairs = tpairs', 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

1153 
prop = prop'}) 
16656  1154 
end 
1155 
handle TYPE (msg, _, _) => raise THM (msg, 0, [th]); 

6928  1156 

22584  1157 
fun instantiate_cterm ([], []) ct = ct 
1158 
 instantiate_cterm (instT, inst) ct = 

1159 
let 

1160 
val Cterm {thy_ref, t, T, sorts, ...} = ct; 

1161 
val (inst', (instT', (thy_ref', sorts'))) = 

1162 
(thy_ref, sorts) > fold_map add_inst inst > fold_map add_instT instT; 

31977  1163 
val subst = Term_Subst.instantiate_maxidx (instT', inst'); 
1164 
val substT = Term_Subst.instantiateT_maxidx instT'; 

22584  1165 
val (t', maxidx1) = subst t ~1; 
1166 
val (T', maxidx') = substT T maxidx1; 

1167 
in Cterm {thy_ref = thy_ref', t = t', T = T', sorts = sorts', maxidx = maxidx'} end 

1168 
handle TYPE (msg, _, _) => raise CTERM (msg, [ct]); 

1169 

6928  1170 
end; 
1171 

0  1172 

16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1173 
(*The trivial implication A ==> A, justified by assume and forall rules. 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1174 
A can contain Vars, not so for assume!*) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1175 
fun trivial (Cterm {thy_ref, t =A, T, maxidx, sorts}) = 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1176 
if T <> propT then 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1177 
raise THM ("trivial: the term must have type prop", 0, []) 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1178 
else 
37309  1179 
Thm (deriv_rule0 (Proofterm.AbsP ("H", NONE, Proofterm.PBound 0)), 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

1180 
{thy_ref = thy_ref, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

1181 
tags = [], 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1182 
maxidx = maxidx, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1183 
shyps = sorts, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1184 
hyps = [], 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1185 
tpairs = [], 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

1186 
prop = Logic.mk_implies (A, A)}); 
0  1187 

31944  1188 
(*Axiomscheme reflecting signature contents 
1189 
T :: c 

1190 
 

1191 
OFCLASS(T, c_class) 

1192 
*) 

1193 
fun of_class (cT, raw_c) = 

24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

1194 
let 
31944  1195 
val Ctyp {thy_ref, T, ...} = cT; 
1196 
val thy = Theory.deref thy_ref; 

31903  1197 
val c = Sign.certify_class thy raw_c; 
31944  1198 
val Cterm {t = prop, maxidx, sorts, ...} = cterm_of thy (Logic.mk_of_class (T, c)); 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

1199 
in 
31944  1200 
if Sign.of_sort thy (T, [c]) then 
37309  1201 
Thm (deriv_rule0 (Proofterm.OfClass (T, c)), 
31944  1202 
{thy_ref = Theory.check_thy thy, 
1203 
tags = [], 

1204 
maxidx = maxidx, 

1205 
shyps = sorts, 

1206 
hyps = [], 

1207 
tpairs = [], 

1208 
prop = prop}) 

1209 
else raise THM ("of_class: type not of class " ^ Syntax.string_of_sort_global thy [c], 0, []) 

399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

1210 
end; 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

1211 

36614
b6c031ad3690
minor tuning of Thm.strip_shyps  no longer pervasive;
wenzelm
parents:
36613
diff
changeset

1212 
(*Remove extra sorts that are witnessed by type signature information*) 
b6c031ad3690
minor tuning of Thm.strip_shyps  no longer pervasive;
wenzelm
parents:
36613
diff
changeset

1213 
fun strip_shyps (thm as Thm (_, {shyps = [], ...})) = thm 
b6c031ad3690
minor tuning of Thm.strip_shyps  no longer pervasive;
wenzelm
parents:
36613
diff
changeset

1214 
 strip_shyps (thm as Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) = 
b6c031ad3690
minor tuning of Thm.strip_shyps  no longer pervasive;
wenzelm
parents:
36613
diff
changeset

1215 
let 
b6c031ad3690
minor tuning of Thm.strip_shyps  no longer pervasive;
wenzelm
parents:
36613
diff
changeset

1216 
val thy = Theory.deref thy_ref; 
36621
2fd4e2c76636
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
wenzelm
parents:
36619
diff
changeset

1217 
val algebra = Sign.classes_of thy; 
2fd4e2c76636
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
wenzelm
parents:
36619
diff
changeset

1218 

2fd4e2c76636
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
wenzelm
parents:
36619
diff
changeset

1219 
val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_fst op =)) thm []; 
36614
b6c031ad3690
minor tuning of Thm.strip_shyps  no longer pervasive;
wenzelm
parents:
36613
diff
changeset

1220 
val extra = fold (Sorts.remove_sort o #2) present shyps; 
b6c031ad3690
minor tuning of Thm.strip_shyps  no longer pervasive;
wenzelm
parents:
36613
diff
changeset

1221 
val witnessed = Sign.witness_sorts thy present extra; 
b6c031ad3690
minor tuning of Thm.strip_shyps  no longer pervasive;
wenzelm
parents:
36613
diff
changeset

1222 
val extra' = fold (Sorts.remove_sort o #2) witnessed extra 
36621
2fd4e2c76636
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
wenzelm
parents:
36619
diff
changeset

1223 
> Sorts.minimal_sorts algebra; 
36614
b6c031ad3690
minor tuning of Thm.strip_shyps  no longer pervasive;
wenzelm
parents:
36613
diff
changeset

1224 
val shyps' = fold (Sorts.insert_sort o #2) present extra'; 
b6c031ad3690
minor tuning of Thm.strip_shyps  no longer pervasive;
wenzelm
parents:
36613
diff
changeset

1225 
in 
37309  1226 
Thm (deriv_rule_unconditional 
1227 
(Proofterm.strip_shyps_proof algebra present witnessed extra') der, 

36621
2fd4e2c76636
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
wenzelm
parents:
36619
diff
changeset

1228 
{thy_ref = Theory.check_thy thy, tags = tags, maxidx = maxidx, 
36614
b6c031ad3690
minor tuning of Thm.strip_shyps  no longer pervasive;
wenzelm
parents:
36613
diff
changeset

1229 
shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop}) 
b6c031ad3690
minor tuning of Thm.strip_shyps  no longer pervasive;
wenzelm
parents:
36613
diff
changeset

1230 
end; 
b6c031ad3690
minor tuning of Thm.strip_shyps  no longer pervasive;
wenzelm
parents:
36613
diff
changeset

1231 

36769
b6b88bf695b3
Thm.unconstrainT based on Logic.unconstrainT  no proofterm yet;
wenzelm
parents:
36768
diff
changeset

1232 
(*Internalize sort constraints of type variables*) 
36883
4ed0d72def50
added Proofterm.unconstrain_thm_proof for Thm.unconstrainT  loosely based on the version by krauss/schropp;
wenzelm
parents:
36882
diff
changeset

1233 
fun unconstrainT (thm as Thm (der, args)) = 
19505  1234 
let 
36883
4ed0d72def50
added Proofterm.unconstrain_thm_proof for Thm.unconstrainT  loosely based on the version by krauss/schropp;
wenzelm
parents:
36882
diff
changeset

1235 
val Deriv {promises, body} = der; 
4ed0d72def50
added Proofterm.unconstrain_thm_proof for Thm.unconstrainT  loosely based on the version by krauss/schropp;
wenzelm
parents:
36882
diff
changeset

1236 
val {thy_ref, shyps, hyps, tpairs, prop, ...} = args; 
4ed0d72def50
added Proofterm.unconstrain_thm_proof for Thm.unconstrainT  loosely based on the version by krauss/schropp;
wenzelm
parents:
36882
diff
changeset

1237 

36769
b6b88bf695b3
Thm.unconstrainT based on Logic.unconstrainT  no proofterm yet;
wenzelm
parents:
36768
diff
changeset

1238 
fun err msg = raise THM ("unconstrainT: " ^ msg, 0, [thm]); 
b6b88bf695b3
Thm.unconstrainT based on Logic.unconstrainT  no proofterm yet;
wenzelm
parents:
36768
diff
changeset

1239 
val _ = null hyps orelse err "illegal hyps"; 
b6b88bf695b3
Thm.unconstrainT based on Logic.unconstrainT  no proofterm yet;
wenzelm
parents:
36768
diff
changeset

1240 
val _ = null tpairs orelse err "unsolved flexflex constraints"; 
b6b88bf695b3
Thm.unconstrainT based on Logic.unconstrainT  no proofterm yet;
wenzelm
parents:
36768
diff
changeset

1241 
val tfrees = rev (Term.add_tfree_names prop []); 
b6b88bf695b3
Thm.unconstrainT based on Logic.unconstrainT  no proofterm yet;
wenzelm
parents:
36768
diff
changeset

1242 
val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees); 
b6b88bf695b3
Thm.unconstrainT based on Logic.unconstrainT  no proofterm yet;
wenzelm
parents:
36768
diff
changeset

1243 

41700
f33d5a00c25d
thm_proof: visible fulfill_body only, without joining nested thms  retain proof irrelevance, which is important for parallel performance;
wenzelm
parents:
41699
diff
changeset

1244 
val ps = map (apsnd (Future.map fulfill_body)) promises; 
36883
4ed0d72def50
added Proofterm.unconstrain_thm_proof for Thm.unconstrainT  loosely based on the version by krauss/schropp;
wenzelm
parents:
36882
diff
changeset

1245 
val thy = Theory.deref thy_ref; 
37309  1246 
val (pthm as (_, (_, prop', _)), proof) = 
1247 
Proofterm.unconstrain_thm_proof thy shyps prop ps body; 

36883
4ed0d72def50
added Proofterm.unconstrain_thm_proof for Thm.unconstrainT  loosely based on the version by krauss/schropp;
wenzelm
parents:
36882
diff
changeset

1248 
val der' = make_deriv [] [] [pthm] proof; 
4ed0d72def50
added Proofterm.unconstrain_thm_proof for Thm.unconstrainT  loosely based on the version by krauss/schropp;
wenzelm
parents:
36882
diff
changeset

1249 
val _ = Theory.check_thy thy; 
19505  1250 
in 
36883
4ed0d72def50
added Proofterm.unconstrain_thm_proof for Thm.unconstrainT  loosely based on the version by krauss/schropp;
wenzelm
parents:
36882
diff
changeset

1251 
Thm (der', 
36769
b6b88bf695b3
Thm.unconstrainT based on Logic.unconstrainT  no proofterm yet;
wenzelm
parents:
36768
diff
changeset

1252 
{thy_ref = thy_ref, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

1253 
tags = [], 
36769
b6b88bf695b3
Thm.unconstrainT based on Logic.unconstrainT  no proofterm yet;
wenzelm
parents:
36768
diff
changeset

1254 
maxidx = maxidx_of_term prop', 
b6b88bf695b3
Thm.unconstrainT based on Logic.unconstrainT  no proofterm yet;
wenzelm
parents:
36768
diff
changeset

1255 
shyps = [[]], (*potentially redundant*) 
36883
4ed0d72def50
added Proofterm.unconstrain_thm_proof for Thm.unconstrainT  loosely based on the version by krauss/schropp;
wenzelm
parents:
36882
diff
changeset

1256 
hyps = [], 
4ed0d72def50
added Proofterm.unconstrain_thm_proof for Thm.unconstrainT  loosely based on the version by krauss/schropp;
wenzelm
parents:
36882
diff
changeset

1257 
tpairs = [], 
36769
b6b88bf695b3
Thm.unconstrainT based on Logic.unconstrainT  no proofterm yet;
wenzelm
parents:
36768
diff
changeset

1258 
prop = prop'}) 
19505  1259 
end; 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

1260 

6786  1261 
(* Replace all TFrees not fixed or in the hyps by new TVars *) 
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35408
diff
changeset

1262 
fun varifyT_global' fixed (Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) = 
12500  1263 
let 
29272  1264 
val tfrees = fold Term.add_tfrees hyps fixed; 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1265 
val prop1 = attach_tpairs tpairs prop; 
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35408
diff
changeset

1266 
val (al, prop2) = Type.varify_global tfrees prop1; 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1267 
val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2); 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1268 
in 
37309  1269 
(al, Thm (deriv_rule1 (Proofterm.varify_proof prop tfrees) der, 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

1270 
{thy_ref = thy_ref, 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

1271 
tags = [], 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1272 
maxidx = Int.max (0, maxidx), 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1273 
shyps = shyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1274 
hyps = hyps, 
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1275 
tpairs = rev (map Logic.dest_equals ts), 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

1276 
prop = prop3})) 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

1277 
end; 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

1278 

35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35408
diff
changeset

1279 
val varifyT_global = #2 o varifyT_global' []; 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

1280 

36615
88756a5a92fc
renamed Thm.freezeT to Thm.legacy_freezeT  it is based on Type.legacy_freeze;
wenzelm
parents:
36614
diff
changeset

1281 
(* Replace all TVars by TFrees that are often new *) 
88756a5a92fc
renamed Thm.freezeT to Thm.legacy_freezeT  it is based on Type.legacy_freeze;
wenzelm
parents:
36614
diff
changeset

1282 
fun legacy_freezeT (Thm (der, {thy_ref, shyps, hyps, tpairs, prop, ...})) = 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

1283 
let 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

1284 
val prop1 = attach_tpairs tpairs prop; 
33832  1285 
val prop2 = Type.legacy_freeze prop1; 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

1286 
val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2); 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

1287 
in 
37309  1288 
Thm (deriv_rule1 (Proofterm.legacy_freezeT prop1) der, 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

1289 
{thy_ref = thy_ref, 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

1290 
tags = [], 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

1291 
maxidx = maxidx_of_term prop2, 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

1292 
shyps = shyps, 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

1293 
hyps = hyps, 
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

1294 
tpairs = rev (map Logic.dest_equals ts), 
18127  1295 
prop = prop3}) 
0  1296 
end; 
1297 

1298 

1299 
(*** Inference rules for tactics ***) 

1300 

1301 
(*Destruct proof state into constraints, other goals, goal(i), rest *) 

28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

1302 
fun dest_state (state as Thm (_, {prop,tpairs,...}), i) = 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1303 
(case Logic.strip_prems(i, [], prop) of 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1304 
(B::rBs, C) => (tpairs, rev rBs, B, C) 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1305 
 _ => raise THM("dest_state", i, [state])) 
0  1306 
handle TERM _ => raise THM("dest_state", i, [state]); 
1307 

46255  1308 
(*Prepare orule for resolution by lifting it over the parameters and 
1309 
assumptions of goal.*) 

18035  1310 
fun lift_rule goal orule = 