author  wenzelm 
Thu, 15 Dec 2016 15:08:18 +0100  
changeset 64570  a2e7862e7dd5 
parent 64568  a504a3dec35a 
child 64571  07bbdb2079db 
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, 
59589  6 
derivations, theorems, inference rules (including lifting and 
28321
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 = 
59589  11 
sig 
59582  12 
type ctyp 
13 
type cterm 

14 
exception CTERM of string * cterm list 

15 
type thm 

16 
type conv = cterm > thm 

17 
exception THM of string * int * thm list 

18 
end; 

19 

20 
signature THM = 

21 
sig 

22 
include BASIC_THM 

1160  23 
(*certified types*) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

24 
val typ_of: ctyp > typ 
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59591
diff
changeset

25 
val global_ctyp_of: theory > typ > ctyp 
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59591
diff
changeset

26 
val ctyp_of: Proof.context > typ > ctyp 
59582  27 
val dest_ctyp: ctyp > ctyp list 
1160  28 
(*certified terms*) 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

29 
val term_of: cterm > term 
59586  30 
val typ_of_cterm: cterm > typ 
31 
val ctyp_of_cterm: cterm > ctyp 

32 
val maxidx_of_cterm: cterm > int 

59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59591
diff
changeset

33 
val global_cterm_of: theory > term > cterm 
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59591
diff
changeset

34 
val cterm_of: Proof.context > term > cterm 
59969
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59917
diff
changeset

35 
val renamed_term: term > cterm > cterm 
59582  36 
val dest_comb: cterm > cterm * cterm 
37 
val dest_fun: cterm > cterm 

38 
val dest_arg: cterm > cterm 

39 
val dest_fun2: cterm > cterm 

40 
val dest_arg1: cterm > cterm 

41 
val dest_abs: string option > cterm > cterm * cterm 

60952
762cb38a3147
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60951
diff
changeset

42 
val rename_tvar: indexname > ctyp > ctyp 
60951
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60949
diff
changeset

43 
val var: indexname * ctyp > cterm 
59582  44 
val apply: cterm > cterm > cterm 
45 
val lambda_name: string * cterm > cterm > cterm 

46 
val lambda: cterm > cterm > cterm 

47 
val adjust_maxidx_cterm: int > cterm > cterm 

48 
val incr_indexes_cterm: int > cterm > cterm 

60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60638
diff
changeset

49 
val match: cterm * cterm > 
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60638
diff
changeset

50 
((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list 
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60638
diff
changeset

51 
val first_order_match: cterm * cterm > 
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60638
diff
changeset

52 
((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

53 
(*theorems*) 
59582  54 
val fold_terms: (term > 'a > 'a) > thm > 'a > 'a 
60952
762cb38a3147
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60951
diff
changeset

55 
val fold_atomic_ctyps: (ctyp > 'a > 'a) > thm > 'a > 'a 
60818  56 
val fold_atomic_cterms: (cterm > 'a > 'a) > thm > 'a > 'a 
59582  57 
val terms_of_tpairs: (term * term) list > term list 
58 
val full_prop_of: thm > term 

60948  59 
val theory_id_of_thm: thm > Context.theory_id 
60638  60 
val theory_name_of_thm: thm > string 
59582  61 
val maxidx_of: thm > int 
62 
val maxidx_thm: thm > int > int 

61039  63 
val shyps_of: thm > sort Ord_List.T 
59582  64 
val hyps_of: thm > term list 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

65 
val prop_of: thm > term 
59582  66 
val tpairs_of: thm > (term * term) list 
16656  67 
val concl_of: thm > term 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
16352
diff
changeset

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

69 
val nprems_of: thm > int 
59582  70 
val no_prems: thm > bool 
71 
val major_prem_of: thm > term 

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

72 
val cprop_of: thm > cterm 
18145  73 
val cprem_of: thm > int > cterm 
60949  74 
val chyps_of: thm > cterm list 
61051  75 
exception CONTEXT of string * ctyp list * cterm list * thm list * Context.generic option 
76 
val theory_of_cterm: cterm > theory 

77 
val theory_of_thm: thm > theory 

78 
val trim_context_cterm: cterm > cterm 

61048  79 
val trim_context: thm > thm 
61051  80 
val transfer_cterm: theory > cterm > cterm 
38709  81 
val transfer: theory > thm > thm 
59969
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59917
diff
changeset

82 
val renamed_prop: term > thm > thm 
38709  83 
val weaken: cterm > thm > thm 
84 
val weaken_sorts: sort list > cterm > cterm 

85 
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

86 
val proof_bodies_of: thm list > proof_body list 
32725  87 
val proof_body_of: thm > proof_body 
88 
val proof_of: thm > proof 

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

90 
val peek_status: thm > {oracle: bool, unfinished: bool, failed: bool} 
32725  91 
val future: thm future > cterm > thm 
64568
a504a3dec35a
more careful derivation_closed / close_derivation;
wenzelm
parents:
63858
diff
changeset

92 
val derivation_closed: thm > bool 
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

93 
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

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

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

96 
val axioms_of: theory > (string * thm) list 
28017  97 
val get_tags: thm > Properties.T 
98 
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

99 
val norm_proof: thm > thm 
20261  100 
val adjust_maxidx_thm: int > thm > thm 
59589  101 
(*inference rules*) 
38709  102 
val assume: cterm > thm 
103 
val implies_intr: cterm > thm > thm 

104 
val implies_elim: thm > thm > thm 

105 
val forall_intr: cterm > thm > thm 

106 
val forall_elim: cterm > thm > thm 

107 
val reflexive: cterm > thm 

108 
val symmetric: thm > thm 

109 
val transitive: thm > thm > thm 

110 
val beta_conversion: bool > conv 

111 
val eta_conversion: conv 

112 
val eta_long_conversion: conv 

113 
val abstract_rule: string > cterm > thm > thm 

114 
val combination: thm > thm > thm 

115 
val equal_intr: thm > thm > thm 

116 
val equal_elim: thm > thm > thm 

58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58946
diff
changeset

117 
val flexflex_rule: Proof.context option > thm > thm Seq.seq 
38709  118 
val generalize: string list * string list > int > thm > thm 
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60638
diff
changeset

119 
val instantiate: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list > 
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60638
diff
changeset

120 
thm > thm 
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60638
diff
changeset

121 
val instantiate_cterm: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list > 
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60638
diff
changeset

122 
cterm > cterm 
38709  123 
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

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

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

126 
val unconstrainT: thm > thm 
38709  127 
val varifyT_global': (string * sort) list > thm > ((string * sort) * indexname) list * thm 
128 
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

129 
val legacy_freezeT: thm > thm 
59969
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59917
diff
changeset

130 
val dest_state: thm * int > (term * term) list * term list * term * term 
38709  131 
val lift_rule: cterm > thm > thm 
132 
val incr_indexes: int > thm > thm 

58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58946
diff
changeset

133 
val assumption: Proof.context option > int > thm > thm Seq.seq 
31945  134 
val eq_assumption: int > thm > thm 
135 
val rotate_rule: int > int > thm > thm 

136 
val permute_prems: int > int > thm > thm 

58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58946
diff
changeset

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

138 
bool * thm * int > int > thm > thm Seq.seq 
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58946
diff
changeset

139 
val biresolution: Proof.context option > bool > (bool * thm) list > int > thm > thm Seq.seq 
59589  140 
(*oracles*) 
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
59884
diff
changeset

141 
val extern_oracles: bool > Proof.context > (Markup.T * xstring) list 
30288
a32700e45ab3
Thm.add_oracle interface: replaced old bstring by binding;
wenzelm
parents:
29636
diff
changeset

142 
val add_oracle: binding * ('a > cterm) > theory > (string * ('a > thm)) * theory 
6089  143 
end; 
144 

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

145 
structure Thm: THM = 
0  146 
struct 
250  147 

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

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

149 

250  150 
(** certified types **) 
151 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

152 
abstype ctyp = Ctyp of {cert: Context.certificate, T: typ, maxidx: int, 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

153 
with 
250  154 

155 
fun typ_of (Ctyp {T, ...}) = T; 

156 

59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59591
diff
changeset

157 
fun global_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

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

159 
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

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

161 
val sorts = Sorts.insert_typ T []; 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

162 
in Ctyp {cert = Context.Certificate thy, T = T, maxidx = maxidx, sorts = sorts} end; 
250  163 

59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59591
diff
changeset

164 
val ctyp_of = global_ctyp_of o Proof_Context.theory_of; 
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59591
diff
changeset

165 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

166 
fun dest_ctyp (Ctyp {cert, T = Type (_, Ts), maxidx, sorts}) = 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

167 
map (fn T => Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = sorts}) Ts 
16679  168 
 dest_ctyp cT = raise TYPE ("dest_ctyp", [typ_of cT], []); 
15087  169 

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

170 

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

171 

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

173 

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

174 
(*certified terms with checked typ, maxidx, and sorts*) 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

175 
abstype cterm = 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

176 
Cterm of {cert: Context.certificate, t: term, T: typ, maxidx: int, 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

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

178 

22584  179 
exception CTERM of string * cterm list; 
16679  180 

250  181 
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

182 

59586  183 
fun typ_of_cterm (Cterm {T, ...}) = T; 
184 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

185 
fun ctyp_of_cterm (Cterm {cert, T, maxidx, sorts, ...}) = 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

186 
Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = sorts}; 
2671  187 

59586  188 
fun maxidx_of_cterm (Cterm {maxidx, ...}) = maxidx; 
189 

59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59591
diff
changeset

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

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

193 
val sorts = Sorts.insert_term t []; 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

194 
in Cterm {cert = Context.Certificate 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

195 

59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59591
diff
changeset

196 
val cterm_of = global_cterm_of o Proof_Context.theory_of; 
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59591
diff
changeset

197 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

198 
fun join_certificate0 (Cterm {cert = cert1, ...}, Cterm {cert = cert2, ...}) = 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

199 
Context.join_certificate (cert1, cert2); 
60315  200 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

201 
fun renamed_term t' (Cterm {cert, t, T, maxidx, sorts}) = 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

202 
if t aconv t' then Cterm {cert = cert, t = t', T = T, maxidx = maxidx, sorts = sorts} 
59969
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59917
diff
changeset

203 
else raise TERM ("renamed_term: terms disagree", [t, t']); 
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59917
diff
changeset

204 

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

205 

22909  206 
(* destructors *) 
207 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

208 
fun dest_comb (Cterm {t = c $ a, T, cert, maxidx, sorts}) = 
22909  209 
let val A = Term.argument_type_of c 0 in 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

210 
(Cterm {t = c, T = A > T, cert = cert, maxidx = maxidx, sorts = sorts}, 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

211 
Cterm {t = a, T = A, cert = cert, maxidx = maxidx, sorts = sorts}) 
1493
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

212 
end 
22584  213 
 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

214 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

215 
fun dest_fun (Cterm {t = c $ _, T, cert, maxidx, sorts}) = 
22909  216 
let val A = Term.argument_type_of c 0 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

217 
in Cterm {t = c, T = A > T, cert = cert, maxidx = maxidx, sorts = sorts} end 
22909  218 
 dest_fun ct = raise CTERM ("dest_fun", [ct]); 
219 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

220 
fun dest_arg (Cterm {t = c $ a, T = _, cert, maxidx, sorts}) = 
22909  221 
let val A = Term.argument_type_of c 0 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

222 
in Cterm {t = a, T = A, cert = cert, maxidx = maxidx, sorts = sorts} end 
22584  223 
 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

224 

22909  225 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

226 
fun dest_fun2 (Cterm {t = c $ _ $ _, T, cert, maxidx, sorts}) = 
22909  227 
let 
228 
val A = Term.argument_type_of c 0; 

229 
val B = Term.argument_type_of c 1; 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

230 
in Cterm {t = c, T = A > B > T, cert = cert, maxidx = maxidx, sorts = sorts} end 
22909  231 
 dest_fun2 ct = raise CTERM ("dest_fun2", [ct]); 
232 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

233 
fun dest_arg1 (Cterm {t = c $ a $ _, T = _, cert, maxidx, sorts}) = 
22909  234 
let val A = Term.argument_type_of c 0 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

235 
in Cterm {t = a, T = A, cert = cert, maxidx = maxidx, sorts = sorts} end 
22909  236 
 dest_arg1 ct = raise CTERM ("dest_arg1", [ct]); 
20673  237 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

238 
fun dest_abs a (Cterm {t = Abs (x, T, t), T = Type ("fun", [_, U]), cert, maxidx, sorts}) = 
18944  239 
let val (y', t') = Term.dest_abs (the_default x a, T, t) in 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

240 
(Cterm {t = Free (y', T), T = T, cert = cert, maxidx = maxidx, sorts = sorts}, 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

241 
Cterm {t = t', T = U, cert = cert, maxidx = maxidx, sorts = sorts}) 
1493
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

242 
end 
22584  243 
 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

244 

22909  245 

246 
(* constructors *) 

247 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

248 
fun rename_tvar (a, i) (Ctyp {cert, T, maxidx, sorts}) = 
60952
762cb38a3147
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60951
diff
changeset

249 
let 
762cb38a3147
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60951
diff
changeset

250 
val S = 
762cb38a3147
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60951
diff
changeset

251 
(case T of 
762cb38a3147
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60951
diff
changeset

252 
TFree (_, S) => S 
762cb38a3147
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60951
diff
changeset

253 
 TVar (_, S) => S 
762cb38a3147
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60951
diff
changeset

254 
 _ => raise TYPE ("rename_tvar: no variable", [T], [])); 
762cb38a3147
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60951
diff
changeset

255 
val _ = if i < 0 then raise TYPE ("rename_tvar: bad index", [TVar ((a, i), S)], []) else (); 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

256 
in Ctyp {cert = cert, T = TVar ((a, i), S), maxidx = Int.max (i, maxidx), sorts = sorts} end; 
60952
762cb38a3147
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60951
diff
changeset

257 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

258 
fun var ((x, i), Ctyp {cert, T, maxidx, sorts}) = 
60951
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60949
diff
changeset

259 
if i < 0 then raise TERM ("var: bad index", [Var ((x, i), T)]) 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

260 
else Cterm {cert = cert, t = Var ((x, i), T), T = T, maxidx = Int.max (i, maxidx), sorts = sorts}; 
60951
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60949
diff
changeset

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 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

266 
Cterm {cert = join_certificate0 (cf, cx), 
16656  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 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

278 
Cterm {cert = join_certificate0 (ct1, ct2), 
16656  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 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

289 
fun adjust_maxidx_cterm i (ct as Cterm {cert, t, T, maxidx, sorts}) = 
20580
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 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

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

293 
else 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

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

295 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

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

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

299 
else Cterm {cert = cert, t = Logic.incr_indexes ([], [], i) t, 
22909  300 
T = Logic.incr_tvar i T, maxidx = maxidx + i, sorts = sorts}; 
301 

302 

2509  303 

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

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

305 

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

306 
abstype thm = Thm of 
40124  307 
deriv * (*derivation*) 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

308 
{cert: Context.certificate, (*background theory certificate*) 
40124  309 
tags: Properties.T, (*additional annotations/comments*) 
310 
maxidx: int, (*maximum index of any Var or TVar*) 

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

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

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

314 
prop: term} (*conclusion*) 

28624  315 
and deriv = Deriv of 
39687  316 
{promises: (serial * thm future) Ord_List.T, 
37309  317 
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

318 
with 
0  319 

23601  320 
type conv = cterm > thm; 
321 

16725  322 
(*errors involving theorems*) 
323 
exception THM of string * int * thm list; 

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

324 

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

325 
fun rep_thm (Thm (_, args)) = args; 
0  326 

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

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

328 
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

329 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

330 
fun fold_atomic_ctyps f (th as Thm (_, {cert, maxidx, shyps, ...})) = 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

331 
let fun ctyp T = Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = shyps} 
60952
762cb38a3147
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60951
diff
changeset

332 
in (fold_terms o fold_types o fold_atyps) (f o ctyp) th end; 
762cb38a3147
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60951
diff
changeset

333 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

334 
fun fold_atomic_cterms f (th as Thm (_, {cert, maxidx, shyps, ...})) = 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

335 
let fun cterm t T = Cterm {cert = cert, t = t, T = T, maxidx = maxidx, sorts = shyps} in 
60818  336 
(fold_terms o fold_aterms) 
337 
(fn t as Const (_, T) => f (cterm t T) 

338 
 t as Free (_, T) => f (cterm t T) 

339 
 t as Var (_, T) => f (cterm t T) 

340 
 _ => I) th 

341 
end; 

342 

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

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

18944  346 
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

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

349 
fun attach_tpairs tpairs prop = 

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

351 

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

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

39687  354 
val union_hyps = Ord_List.union Term_Ord.fast_term_ord; 
355 
val insert_hyps = Ord_List.insert Term_Ord.fast_term_ord; 

356 
val remove_hyps = Ord_List.remove Term_Ord.fast_term_ord; 

22365  357 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

358 
fun join_certificate1 (Cterm {cert = cert1, ...}, Thm (_, {cert = cert2, ...})) = 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

359 
Context.join_certificate (cert1, cert2); 
16945  360 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

361 
fun join_certificate2 (Thm (_, {cert = cert1, ...}), Thm (_, {cert = cert2, ...})) = 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

362 
Context.join_certificate (cert1, cert2); 
16945  363 

0  364 

22365  365 
(* basic components *) 
16135  366 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

367 
val cert_of = #cert o rep_thm; 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

368 
val theory_id_of_thm = Context.certificate_theory_id o cert_of; 
60948  369 
val theory_name_of_thm = Context.theory_id_name o theory_id_of_thm; 
61050  370 

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

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

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

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

376 
val tpairs_of = #tpairs o rep_thm; 
0  377 

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

378 
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

379 
val prems_of = Logic.strip_imp_prems o prop_of; 
21576  380 
val nprems_of = Logic.count_prems o prop_of; 
19305  381 
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

382 

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

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

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

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

386 
 [] => 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

387 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

388 
fun cprop_of (Thm (_, {cert, maxidx, shyps, prop, ...})) = 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

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

390 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

391 
fun cprem_of (th as Thm (_, {cert, maxidx, shyps, prop, ...})) i = 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

392 
Cterm {cert = cert, maxidx = maxidx, T = propT, sorts = shyps, 
18145  393 
t = Logic.nth_prem (i, prop) handle TERM _ => raise THM ("cprem_of", i, [th])}; 
18035  394 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

395 
fun chyps_of (Thm (_, {cert, shyps, hyps, ...})) = 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

396 
map (fn t => Cterm {cert = cert, maxidx = ~1, T = propT, sorts = shyps, t = t}) hyps; 
60949  397 

61051  398 

399 
(* implicit theory context *) 

400 

401 
exception CONTEXT of string * ctyp list * cterm list * thm list * Context.generic option; 

402 

403 
fun theory_of_cterm (ct as Cterm {cert, ...}) = 

404 
Context.certificate_theory cert 

405 
handle ERROR msg => raise CONTEXT (msg, [], [ct], [], NONE); 

406 

407 
fun theory_of_thm th = 

408 
Context.certificate_theory (cert_of th) 

409 
handle ERROR msg => raise CONTEXT (msg, [], [], [th], NONE); 

410 

411 
fun trim_context_cterm ct = 

412 
(case ct of 

413 
Cterm {cert = Context.Certificate_Id _, ...} => ct 

414 
 Cterm {cert = Context.Certificate thy, t, T, maxidx, sorts} => 

415 
Cterm {cert = Context.Certificate_Id (Context.theory_id thy), 

416 
t = t, T = T, maxidx = maxidx, sorts = sorts}); 

417 

61048  418 
fun trim_context th = 
419 
(case th of 

420 
Thm (_, {cert = Context.Certificate_Id _, ...}) => th 

421 
 Thm (der, {cert = Context.Certificate thy, tags, maxidx, shyps, hyps, tpairs, prop}) => 

422 
Thm (der, 

423 
{cert = Context.Certificate_Id (Context.theory_id thy), 

424 
tags = tags, maxidx = maxidx, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop})); 

425 

61051  426 
fun transfer_cterm thy' ct = 
3895  427 
let 
61051  428 
val Cterm {cert, t, T, maxidx, sorts} = ct; 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

429 
val _ = 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

430 
Context.subthy_id (Context.certificate_theory_id cert, Context.theory_id thy') orelse 
61051  431 
raise CONTEXT ("Cannot transfer: not a super theory", [], [ct], [], 
432 
SOME (Context.Theory thy')); 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

433 
val cert' = Context.join_certificate (Context.Certificate thy', cert); 
3895  434 
in 
61051  435 
if Context.eq_certificate (cert, cert') then ct 
436 
else Cterm {cert = cert', t = t, T = T, maxidx = maxidx, sorts = sorts} 

437 
end; 

438 

439 
fun transfer thy' th = 

440 
let 

441 
val Thm (der, {cert, tags, maxidx, shyps, hyps, tpairs, prop}) = th; 

442 
val _ = 

443 
Context.subthy_id (Context.certificate_theory_id cert, Context.theory_id thy') orelse 

444 
raise CONTEXT ("Cannot transfer: not a super theory", [], [], [th], 

445 
SOME (Context.Theory thy')); 

446 
val cert' = Context.join_certificate (Context.Certificate thy', cert); 

447 
in 

448 
if Context.eq_certificate (cert, cert') then th 

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

450 
Thm (der, 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

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

452 
tags = tags, 
16945  453 
maxidx = maxidx, 
454 
shyps = shyps, 

455 
hyps = hyps, 

456 
tpairs = tpairs, 

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

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

459 

61051  460 

461 
(* matching *) 

462 

463 
local 

464 

465 
fun gen_match match 

466 
(ct1 as Cterm {t = t1, sorts = sorts1, ...}, 

467 
ct2 as Cterm {t = t2, sorts = sorts2, maxidx = maxidx2, ...}) = 

468 
let 

469 
val cert = join_certificate0 (ct1, ct2); 

470 
val thy = Context.certificate_theory cert 

471 
handle ERROR msg => raise CONTEXT (msg, [], [ct1, ct2], [], NONE); 

472 
val (Tinsts, tinsts) = match thy (t1, t2) (Vartab.empty, Vartab.empty); 

473 
val sorts = Sorts.union sorts1 sorts2; 

474 
fun mk_cTinst ((a, i), (S, T)) = 

475 
(((a, i), S), Ctyp {T = T, cert = cert, maxidx = maxidx2, sorts = sorts}); 

476 
fun mk_ctinst ((x, i), (U, t)) = 

477 
let val T = Envir.subst_type Tinsts U in 

478 
(((x, i), T), Cterm {t = t, T = T, cert = cert, maxidx = maxidx2, sorts = sorts}) 

479 
end; 

480 
in (Vartab.fold (cons o mk_cTinst) Tinsts [], Vartab.fold (cons o mk_ctinst) tinsts []) end; 

481 

482 
in 

483 

484 
val match = gen_match Pattern.match; 

485 
val first_order_match = gen_match Pattern.first_order_match; 

486 

487 
end; 

488 

489 

59969
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59917
diff
changeset

490 
(*implicit alphaconversion*) 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

491 
fun renamed_prop prop' (Thm (der, {cert, tags, maxidx, shyps, hyps, tpairs, prop})) = 
59969
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59917
diff
changeset

492 
if prop aconv prop' then 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

493 
Thm (der, {cert = cert, tags = tags, maxidx = maxidx, shyps = shyps, 
59969
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59917
diff
changeset

494 
hyps = hyps, tpairs = tpairs, prop = prop'}) 
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59917
diff
changeset

495 
else raise TERM ("renamed_prop: props disagree", [prop, prop']); 
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59917
diff
changeset

496 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

497 
fun make_context ths NONE cert = 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

498 
(Context.Theory (Context.certificate_theory cert) 
61051  499 
handle ERROR msg => raise CONTEXT (msg, [], [], ths, NONE)) 
61045
c7a7f063704a
clarified exceptions: avoid interference of formal context failure with regular rule application failure (which is routinely handled in userspace);
wenzelm
parents:
61044
diff
changeset

500 
 make_context ths (SOME ctxt) cert = 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

501 
let 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

502 
val thy_id = Context.certificate_theory_id cert; 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

503 
val thy_id' = Context.theory_id (Proof_Context.theory_of ctxt); 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

504 
in 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

505 
if Context.subthy_id (thy_id, thy_id') then Context.Proof ctxt 
61051  506 
else raise CONTEXT ("Bad context", [], [], ths, SOME (Context.Proof ctxt)) 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

507 
end; 
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58946
diff
changeset

508 

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

511 
let 

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

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

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

517 
else if maxidxA <> ~1 then 

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

519 
else 

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

520 
Thm (der, 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

521 
{cert = join_certificate1 (ct, th), 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

522 
tags = tags, 
16945  523 
maxidx = maxidx, 
524 
shyps = Sorts.union sorts shyps, 

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

527 
prop = prop}) 
16945  528 
end; 
16656  529 

28624  530 
fun weaken_sorts raw_sorts ct = 
531 
let 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

532 
val Cterm {cert, t, T, maxidx, sorts} = ct; 
61050  533 
val thy = theory_of_cterm ct; 
28624  534 
val more_sorts = Sorts.make (map (Sign.certify_sort thy) raw_sorts); 
535 
val sorts' = Sorts.union sorts more_sorts; 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

536 
in Cterm {cert = cert, t = t, T = T, maxidx = maxidx, sorts = sorts'} end; 
28624  537 

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

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

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

541 

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

542 

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

543 

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

545 

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

546 
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

547 
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

548 

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

550 

28330  551 

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

553 

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

554 
fun promise_ord ((i, _), (j, _)) = int_ord (j, i); 
28330  555 

52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

556 
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

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

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

559 
let 
39687  560 
val ps = Ord_List.union promise_ord ps1 ps2; 
44334  561 
val oras = Proofterm.unions_oracles [oras1, oras2]; 
562 
val thms = Proofterm.unions_thms [thms1, thms2]; 

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

563 
val prf = 
52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

564 
(case ! Proofterm.proofs of 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

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

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

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

568 
 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

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

570 

52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

571 
fun deriv_rule1 f = deriv_rule2 (K f) empty_deriv; 
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

572 
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

573 

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

574 
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

575 
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

576 

1238  577 

32725  578 
(* fulfilled proofs *) 
579 

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

582 

583 
fun join_promises [] = () 

584 
 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

585 
and join_promises_of thms = join_promises (Ord_List.make promise_ord (maps raw_promises_of thms)); 
32725  586 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

587 
fun fulfill_body (th as Thm (Deriv {promises, body}, _)) = 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

588 
Proofterm.fulfill_norm_proof (theory_of_thm th) (fulfill_promises promises) body 
44331  589 
and fulfill_promises promises = 
590 
map fst promises ~~ map fulfill_body (Future.joins (map snd promises)); 

32725  591 

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

592 
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

593 
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

594 
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

595 
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

596 
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

597 
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

598 

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

599 
val proof_body_of = singleton proof_bodies_of; 
44331  600 
val proof_of = Proofterm.proof_of o proof_body_of; 
32725  601 

64570
a2e7862e7dd5
back to full Proofterm.join_bodies, which was lost in 2011 (4e2abb045eac, cc53ce50f738);
wenzelm
parents:
64568
diff
changeset

602 
val join_proofs = Proofterm.join_bodies o proof_bodies_of; 
32725  603 

604 

605 
(* derivation status *) 

606 

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

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

610 
val bodies = body :: 

44331  611 
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

612 
val {oracle, unfinished, failed} = Proofterm.peek_status bodies; 
32725  613 
in 
614 
{oracle = oracle, 

615 
unfinished = unfinished orelse exists is_none ps, 

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

617 
end; 

618 

619 

620 
(* future rule *) 

621 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

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

624 
fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]); 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

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

626 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

627 
val _ = Context.eq_certificate (cert, orig_cert) orelse err "bad theory"; 
32725  628 
val _ = prop aconv orig_prop orelse err "bad prop"; 
629 
val _ = null tpairs orelse err "bad tpairs"; 

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

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

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

44331  633 
val _ = join_promises promises; 
32725  634 
in thm end; 
635 

636 
fun future future_thm ct = 

637 
let 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

638 
val Cterm {cert = cert, t = prop, T, maxidx, sorts} = ct; 
32725  639 
val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]); 
640 

61050  641 
val thy = theory_of_cterm ct; 
32725  642 
val i = serial (); 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

643 
val future = future_thm > Future.map (future_result i cert sorts prop); 
32725  644 
in 
37309  645 
Thm (make_deriv [(i, future)] [] [] (Proofterm.promise_proof thy i prop), 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

646 
{cert = cert, 
32725  647 
tags = [], 
648 
maxidx = maxidx, 

649 
shyps = sorts, 

650 
hyps = [], 

651 
tpairs = [], 

652 
prop = prop}) 

653 
end; 

654 

655 

656 
(* closed derivations with official name *) 

657 

41699  658 
(*nondeterministic, depends on unknown promises*) 
64568
a504a3dec35a
more careful derivation_closed / close_derivation;
wenzelm
parents:
63858
diff
changeset

659 
fun derivation_closed (Thm (Deriv {body, ...}, _)) = 
a504a3dec35a
more careful derivation_closed / close_derivation;
wenzelm
parents:
63858
diff
changeset

660 
Proofterm.compact_proof (Proofterm.proof_of body); 
a504a3dec35a
more careful derivation_closed / close_derivation;
wenzelm
parents:
63858
diff
changeset

661 

a504a3dec35a
more careful derivation_closed / close_derivation;
wenzelm
parents:
63858
diff
changeset

662 
(*nondeterministic, depends on unknown promises*) 
37297  663 
fun derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) = 
37309  664 
Proofterm.get_name shyps hyps prop (Proofterm.proof_of body); 
32725  665 

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

666 
fun name_derivation name (thm as Thm (der, args)) = 
32725  667 
let 
668 
val Deriv {promises, body} = der; 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

669 
val {shyps, hyps, prop, tpairs, ...} = args; 
32725  670 
val _ = null tpairs orelse raise THM ("put_name: unsolved flexflex constraints", 0, [thm]); 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

671 
val thy = theory_of_thm thm; 
32725  672 

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

673 
val ps = map (apsnd (Future.map fulfill_body)) promises; 
37309  674 
val (pthm, proof) = Proofterm.thm_proof thy name shyps hyps prop ps body; 
32725  675 
val der' = make_deriv [] [] [pthm] proof; 
676 
in Thm (der', args) end; 

677 

678 

1238  679 

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

681 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

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

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

684 
fun get_ax thy = 
59884  685 
Name_Space.lookup (Theory.axiom_table thy) name 
686 
> 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

687 
let 
52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

688 
val der = deriv_rule0 (Proofterm.axm_proof name prop); 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

689 
val cert = Context.Certificate thy; 
24143
90a9a6fe0d01
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23781
diff
changeset

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

691 
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

692 
in 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

693 
Thm (der, {cert = cert, tags = [], 
28321
9f4499bf9384
type thm: fully internal derivation, no longer exported;
wenzelm
parents:
28290
diff
changeset

694 
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

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

696 
in 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

697 
(case get_first get_ax (Theory.nodes_of thy0) of 
15531  698 
SOME thm => thm 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

699 
 NONE => raise THEORY ("No axiom " ^ quote name, [thy0])) 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

701 

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

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

703 
fun axioms_of thy = 
56025  704 
map (fn (name, _) => (name, axiom thy name)) (Theory.axioms_of thy); 
776
df8f91c0e57c
improved axioms_of: returns thms as the manual says;
wenzelm
parents:
721
diff
changeset

705 

6089  706 

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

707 
(* tags *) 
6089  708 

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

709 
val get_tags = #tags o rep_thm; 
6089  710 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

711 
fun map_tags f (Thm (der, {cert, tags, maxidx, shyps, hyps, tpairs, prop})) = 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

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

713 
shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}); 
0  714 

715 

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

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

717 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

718 
fun norm_proof (th as Thm (der, args)) = 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

719 
Thm (deriv_rule1 (Proofterm.rew_proof (theory_of_thm th)) der, args); 
23781
ab793a6ddf9f
Added function norm_proof for normalizing the proof term
berghofe
parents:
23657
diff
changeset

720 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

721 
fun adjust_maxidx_thm i (th as Thm (der, {cert, tags, maxidx, shyps, hyps, tpairs, prop})) = 
20261  722 
if maxidx = i then th 
723 
else if maxidx < i then 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

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

725 
hyps = hyps, tpairs = tpairs, prop = prop}) 
20261  726 
else 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

727 
Thm (der, {maxidx = Int.max (maxidx_tpairs tpairs (maxidx_of_term prop), i), 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

728 
cert = cert, tags = tags, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}); 
564  729 

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

730 

2509  731 

1529  732 
(*** Meta rules ***) 
0  733 

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

734 
(** primitive rules **) 
0  735 

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

737 
fun assume raw_ct = 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

738 
let val Cterm {cert, 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

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

741 
else if maxidx <> ~1 then 
19230  742 
raise THM ("assume: variables", maxidx, []) 
52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

743 
else Thm (deriv_rule0 (Proofterm.Hyp prop), 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

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

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

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

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

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

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

750 
prop = prop}) 
0  751 
end; 
752 

1220  753 
(*Implication introduction 
3529  754 
[A] 
755 
: 

756 
B 

1220  757 
 
758 
A ==> B 

759 
*) 

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

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

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

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

764 
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

765 
else 
52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

766 
Thm (deriv_rule1 (Proofterm.implies_intr_proof A) der, 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

767 
{cert = join_certificate1 (ct, th), 
52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

768 
tags = [], 
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

769 
maxidx = Int.max (maxidxA, maxidx), 
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

770 
shyps = Sorts.union sorts shyps, 
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

771 
hyps = remove_hyps A hyps, 
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

772 
tpairs = tpairs, 
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

773 
prop = Logic.mk_implies (A, prop)}); 
0  774 

1529  775 

1220  776 
(*Implication elimination 
777 
A ==> B A 

778 
 

779 
B 

780 
*) 

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

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

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

783 
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

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

785 
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

786 
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

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

788 
case prop of 
56245  789 
Const ("Pure.imp", _) $ A $ B => 
20512  790 
if A aconv propA then 
52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

791 
Thm (deriv_rule2 (curry Proofterm.%%) der derA, 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

792 
{cert = join_certificate2 (thAB, thA), 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

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

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

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

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

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

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

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

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

801 
end; 
250  802 

1220  803 
(*Forall introduction. The Free or Var x must not be free in the hypotheses. 
16656  804 
[x] 
805 
: 

806 
A 

807 
 

808 
!!x. A 

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

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

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

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

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

814 
fun result a = 
52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

815 
Thm (deriv_rule1 (Proofterm.forall_intr_proof x a) der, 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

816 
{cert = join_certificate1 (ct, th), 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

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

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

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

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

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

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

824 
if exists (fn t => Logic.occs (x, t)) ts then 
21798  825 
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

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

827 
in 
52788  828 
(case x of 
21798  829 
Free (a, _) => (check_occs a x hyps; check_occs a x (terms_of_tpairs tpairs); result a) 
830 
 Var ((a, _), _) => (check_occs a x (terms_of_tpairs tpairs); result a) 

52788  831 
 _ => raise THM ("forall_intr: not a variable", 0, [th])) 
0  832 
end; 
833 

1220  834 
(*Forall elimination 
16656  835 
!!x. A 
1220  836 
 
837 
A[t/x] 

838 
*) 

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

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

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

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

842 
(case prop of 
56245  843 
Const ("Pure.all", Type ("fun", [Type ("fun", [qary, _]), _])) $ A => 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

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

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

846 
else 
52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

847 
Thm (deriv_rule1 (Proofterm.% o rpair (SOME t)) der, 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

848 
{cert = join_certificate1 (ct, th), 
52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

849 
tags = [], 
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

850 
maxidx = Int.max (maxidx, maxt), 
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

851 
shyps = Sorts.union sorts shyps, 
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

852 
hyps = hyps, 
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

853 
tpairs = tpairs, 
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

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

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

857 

1220  858 
(* Equality *) 
0  859 

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

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

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

862 
*) 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

863 
fun reflexive (Cterm {cert, t, T = _, maxidx, sorts}) = 
52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

864 
Thm (deriv_rule0 Proofterm.reflexive, 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

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

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

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

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

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

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

871 
prop = Logic.mk_equals (t, t)}); 
0  872 

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

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

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

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

876 
u == t 
1220  877 
*) 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

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

879 
(case prop of 
56245  880 
(eq as Const ("Pure.eq", _)) $ t $ u => 
52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

881 
Thm (deriv_rule1 Proofterm.symmetric der, 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

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

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

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

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

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

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

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

889 
 _ => raise THM ("symmetric", 0, [th])); 
0  890 

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

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

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

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

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

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

898 
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

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

900 
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

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

902 
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

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

904 
case (prop1, prop2) of 
56245  905 
((eq as Const ("Pure.eq", Type (_, [T, _]))) $ t1 $ u, Const ("Pure.eq", _) $ u' $ t2) => 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

906 
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

907 
else 
52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

908 
Thm (deriv_rule2 (Proofterm.transitive u T) der1 der2, 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

909 
{cert = join_certificate2 (th1, th2), 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

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

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

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

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

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

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

916 
 _ => err "premises" 
0  917 
end; 
918 

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

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

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

922 
*) 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

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

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

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

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

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

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

929 
in 
52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

930 
Thm (deriv_rule0 Proofterm.reflexive, 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

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

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

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

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

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

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

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

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

939 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

940 
fun eta_conversion (Cterm {cert, t, T = _, maxidx, sorts}) = 
52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

941 
Thm (deriv_rule0 Proofterm.reflexive, 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

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

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

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

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

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

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

948 
prop = Logic.mk_equals (t, Envir.eta_contract t)}); 
0  949 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

950 
fun eta_long_conversion (Cterm {cert, t, T = _, maxidx, sorts}) = 
52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

951 
Thm (deriv_rule0 Proofterm.reflexive, 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

952 
{cert = cert, 
23493  953 
tags = [], 
954 
maxidx = maxidx, 

955 
shyps = sorts, 

956 
hyps = [], 

957 
tpairs = [], 

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

0  960 
(*The abstraction rule. The Free or Var x must not be free in the hypotheses. 
961 
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

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

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

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

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

967 
(Cterm {t = x, T, sorts, ...}) 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

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

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

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

971 
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

972 
val result = 
52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

973 
Thm (deriv_rule1 (Proofterm.abstract_rule x a) der, 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

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

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

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

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

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

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

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

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

983 
if exists (fn t => Logic.occs (x, t)) ts then 
21798  984 
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

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

986 
in 
52788  987 
(case x of 
21798  988 
Free (a, _) => (check_occs a x hyps; check_occs a x (terms_of_tpairs tpairs); result) 
989 
 Var ((a, _), _) => (check_occs a x (terms_of_tpairs tpairs); result) 

52788  990 
 _ => raise THM ("abstract_rule: not a variable", 0, [th])) 
0  991 
end; 
992 

993 
(*The combination rule 

3529  994 
f == g t == u 
995 
 

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

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

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

1000 
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

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

1002 
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

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

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

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

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

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

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

1010 
 _ => 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

1011 
in 
52788  1012 
(case (prop1, prop2) of 
56245  1013 
(Const ("Pure.eq", Type ("fun", [fT, _])) $ f $ g, 
1014 
Const ("Pure.eq", Type ("fun", [tT, _])) $ t $ u) => 

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

1015 
(chktypes fT tT; 
52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

1016 
Thm (deriv_rule2 (Proofterm.combination f g t u fT) der1 der2, 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1017 
{cert = join_certificate2 (th1, th2), 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

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

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

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

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

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

1023 
prop = Logic.mk_equals (f $ t, g $ u)})) 
52788  1024 
 _ => raise THM ("combination: premises", 0, [th1, th2])) 
0  1025 
end; 
1026 

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

1027 
(*Equality introduction 
3529  1028 
A ==> B B ==> A 
1029 
 

1030 
A == B 

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

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

1034 
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

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

1036 
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

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

1038 
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

1039 
in 
52788  1040 
(case (prop1, prop2) of 
56245  1041 
(Const("Pure.imp", _) $ A $ B, Const("Pure.imp", _) $ B' $ A') => 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1042 
if A aconv A' andalso B aconv B' then 
52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

1043 
Thm (deriv_rule2 (Proofterm.equal_intr A B) der1 der2, 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1044 
{cert = join_certificate2 (th1, th2), 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

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

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

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

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

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

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

1051 
else err "not equal" 
52788  1052 
 _ => err "premises") 
1529  1053 
end; 
1054 

1055 
(*The equal propositions rule 

3529  1056 
A == B A 
1529  1057 
 
1058 
B 

1059 
*) 

1060 
fun equal_elim th1 th2 = 

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

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

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

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

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

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

1066 
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

1067 
in 
52788  1068 
(case prop1 of 
56245  1069 
Const ("Pure.eq", _) $ A $ B => 
16601
ee8eefade568
more efficient treatment of shyps and hyps (use ordered lists);
wenzelm
parents:
16425
diff
changeset

1070 
if prop2 aconv A then 
52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

1071 
Thm (deriv_rule2 (Proofterm.equal_elim A B) der1 der2, 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1072 
{cert = join_certificate2 (th1, th2), 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21576
diff
changeset

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

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

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

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

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

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

1079 
else err "not equal" 
52789  1080 
 _ => err "major premise") 
1529  1081 
end; 
0  1082 

1220  1083 

1084 

0  1085 
(**** Derived rules ****) 
1086 

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

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

1088 
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

1089 
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

1090 
flexflex.*) 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1091 
fun flexflex_rule opt_ctxt (th as Thm (der, {cert, maxidx, shyps, hyps, tpairs, prop, ...})) = 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1092 
Unify.smash_unifiers (make_context [th] opt_ctxt cert) tpairs (Envir.empty maxidx) 
52788  1093 
> Seq.map (fn env => 
1094 
if Envir.is_empty env then th 

1095 
else 

1096 
let 

59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58950
diff
changeset

1097 
val tpairs' = tpairs > map (apply2 (Envir.norm_term env)) 
52788  1098 
(*remove trivial tpairs, of the form t==t*) 
1099 
> filter_out (op aconv); 

1100 
val der' = deriv_rule1 (Proofterm.norm_proof' env) der; 

1101 
val prop' = Envir.norm_term env prop; 

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

1103 
val shyps = Envir.insert_sorts env shyps; 

1104 
in 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1105 
Thm (der', {cert = cert, tags = [], maxidx = maxidx, 
52788  1106 
shyps = shyps, hyps = hyps, tpairs = tpairs', prop = prop'}) 
1107 
end); 

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

1108 

0  1109 

19910  1110 
(*Generalization of fixed variables 
1111 
A 

1112 
 

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

1114 
*) 

1115 

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

1117 
 generalize (tfrees, frees) idx th = 

1118 
let 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1119 
val Thm (der, {cert, maxidx, shyps, hyps, tpairs, prop, ...}) = th; 
19910  1120 
val _ = idx <= maxidx andalso raise THM ("generalize: bad index", idx, [th]); 
1121 

33697  1122 
val bad_type = 
1123 
if null tfrees then K false 

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

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

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

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

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

1130 
 bad_term (Bound _) = false; 

1131 
val _ = exists bad_term hyps andalso 

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

1133 

31977  1134 
val gen = Term_Subst.generalize (tfrees, frees) idx; 
19910  1135 
val prop' = gen prop; 
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58950
diff
changeset

1136 
val tpairs' = map (apply2 gen) tpairs; 
19910  1137 
val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop'); 
1138 
in 

52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

1139 
Thm (deriv_rule1 (Proofterm.generalize (tfrees, frees) idx) der, 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

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

1141 
tags = [], 
19910  1142 
maxidx = maxidx', 
1143 
shyps = shyps, 

1144 
hyps = hyps, 

1145 
tpairs = tpairs', 

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

1146 
prop = prop'}) 
19910  1147 
end; 
1148 

1149 

22584  1150 
(*Instantiation of schematic variables 
16656  1151 
A 
1152 
 

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

1220  1154 
*) 
0  1155 

6928  1156 
local 
1157 

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

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

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

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1161 
fun add_inst (v as (_, T), cu) (cert, sorts) = 
6928  1162 
let 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1163 
val Cterm {t = u, T = U, cert = cert2, sorts = sorts_u, maxidx = maxidx_u, ...} = cu; 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1164 
val cert' = Context.join_certificate (cert, cert2); 
16884
1678a796b6b2
tuned instantiate (avoid subst_atomic, subst_atomic_types);
wenzelm
parents:
16847
diff
changeset

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

1166 
in 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1167 
if T = U then ((v, (u, maxidx_u)), (cert', sorts')) 
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60638
diff
changeset

1168 
else 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1169 
let 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1170 
val msg = 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1171 
(case cert' of 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1172 
Context.Certificate thy' => 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1173 
Pretty.string_of (Pretty.block 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1174 
[Pretty.str "instantiate: type conflict", 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1175 
Pretty.fbrk, pretty_typing thy' (Var v) T, 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1176 
Pretty.fbrk, pretty_typing thy' u U]) 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1177 
 Context.Certificate_Id _ => "instantiate: type conflict"); 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1178 
in raise TYPE (msg, [T, U], [Var v, u]) end 
0  1179 
end; 
1180 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1181 
fun add_instT (v as (_, S), cU) (cert, sorts) = 
16656  1182 
let 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1183 
val Ctyp {T = U, cert = cert2, sorts = sorts_U, maxidx = maxidx_U, ...} = cU; 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1184 
val cert' = Context.join_certificate (cert, cert2); 
61051  1185 
val thy' = Context.certificate_theory cert' 
1186 
handle ERROR msg => raise CONTEXT (msg, [cU], [], [], NONE); 

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

1187 
val sorts' = Sorts.union sorts_U sorts; 
16656  1188 
in 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1189 
if Sign.of_sort thy' (U, S) then ((v, (U, maxidx_U)), (cert', sorts')) 
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60638
diff
changeset

1190 
else raise TYPE ("Type not of sort " ^ Syntax.string_of_sort_global thy' S, [U], []) 
16656  1191 
end; 
0  1192 

6928  1193 
in 
1194 

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

1195 
(*Lefttoright replacements: ctpairs = [..., (vi, ti), ...]. 
0  1196 
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

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

1199 
 instantiate (instT, inst) th = 
16656  1200 
let 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1201 
val Thm (der, {cert, hyps, shyps, tpairs, prop, ...}) = th; 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1202 
val (inst', (instT', (cert', shyps'))) = 
61051  1203 
(cert, shyps) > fold_map add_inst inst > fold_map add_instT instT 
61053  1204 
handle CONTEXT (msg, cTs, cts, ths, context) => 
1205 
raise CONTEXT (msg, cTs, cts, th :: ths, context); 

31977  1206 
val subst = Term_Subst.instantiate_maxidx (instT', inst'); 
20512  1207 
val (prop', maxidx1) = subst prop ~1; 
1208 
val (tpairs', maxidx') = 

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

16656  1210 
in 
52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

1211 
Thm (deriv_rule1 
37309  1212 
(fn d => Proofterm.instantiate (map (apsnd #1) instT', map (apsnd #1) inst') d) der, 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

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

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

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

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

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

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

1219 
prop = prop'}) 
16656  1220 
end 
1221 
handle TYPE (msg, _, _) => raise THM (msg, 0, [th]); 

6928  1222 

22584  1223 
fun instantiate_cterm ([], []) ct = ct 
1224 
 instantiate_cterm (instT, inst) ct = 

1225 
let 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1226 
val Cterm {cert, t, T, sorts, ...} = ct; 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1227 
val (inst', (instT', (cert', sorts'))) = 
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1228 
(cert, sorts) > fold_map add_inst inst > fold_map add_instT instT; 
31977  1229 
val subst = Term_Subst.instantiate_maxidx (instT', inst'); 
1230 
val substT = Term_Subst.instantiateT_maxidx instT'; 

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

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1233 
in Cterm {cert = cert', t = t', T = T', sorts = sorts', maxidx = maxidx'} end 
22584  1234 
handle TYPE (msg, _, _) => raise CTERM (msg, [ct]); 
1235 

6928  1236 
end; 
1237 

0  1238 

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

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

1240 
A can contain Vars, not so for assume!*) 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

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

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

1243 
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

1244 
else 
52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

1245 
Thm (deriv_rule0 (Proofterm.AbsP ("H", NONE, Proofterm.PBound 0)), 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

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

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

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

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

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

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

1252 
prop = Logic.mk_implies (A, A)}); 
0  1253 

31944  1254 
(*Axiomscheme reflecting signature contents 
1255 
T :: c 

1256 
 

1257 
OFCLASS(T, c_class) 

1258 
*) 

1259 
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

1260 
let 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1261 
val Ctyp {cert, T, ...} = cT; 
61051  1262 
val thy = Context.certificate_theory cert 
1263 
handle ERROR msg => raise CONTEXT (msg, [cT], [], [], NONE); 

31903  1264 
val c = Sign.certify_class thy raw_c; 
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59591
diff
changeset

1265 
val Cterm {t = prop, maxidx, sorts, ...} = global_cterm_of thy (Logic.mk_of_class (T, c)); 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

1266 
in 
31944  1267 
if Sign.of_sort thy (T, [c]) then 
52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

1268 
Thm (deriv_rule0 (Proofterm.OfClass (T, c)), 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1269 
{cert = cert, 
31944  1270 
tags = [], 
1271 
maxidx = maxidx, 

1272 
shyps = sorts, 

1273 
hyps = [], 

1274 
tpairs = [], 

1275 
prop = prop}) 

1276 
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

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

1278 

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

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

1280 
fun strip_shyps (thm as Thm (_, {shyps = [], ...})) = thm 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

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

1282 
let 
61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1283 
val thy = theory_of_thm thm; 
36621
2fd4e2c76636
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
wenzelm
parents:
36619
diff
changeset

1284 
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

1285 

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

1286 
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

1287 
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

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

1289 
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

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

1291 
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

1292 
in 
37309  1293 
Thm (deriv_rule_unconditional 
1294 
(Proofterm.strip_shyps_proof algebra present witnessed extra') der, 

61044
b7af255dd200
more abstract theory certificate, which is not necessarily the full theory;
wenzelm
parents:
61042
diff
changeset

1295 
{cert = cert, tags = tags, maxidx = maxidx, 
36614
b6c031ad3690
minor tuning of Thm.strip_shyps  no longer pervasive;
wenzelm
parents:
36613
diff
changeset

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

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

1298 

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

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

1300 
fun unconstrainT (thm as Thm (der, args)) = 
19505
0b345cf953c4
added unconstrainT;
w 