author  berghofe 
Thu, 29 Jul 2004 17:45:21 +0200  
changeset 15087  666f89fbb860 
parent 14828  15d12761ba54 
child 15264  a881ad2e9edc 
permissions  rwrr 
250  1 
(* Title: Pure/thm.ML 
0  2 
ID: $Id$ 
250  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

4 
Copyright 1994 University of Cambridge 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

5 

1160  6 
The core of Isabelle's Meta Logic: certified types and terms, meta 
10486  7 
theorems, meta rules (including lifting and resolution). 
0  8 
*) 
9 

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

13 
type ctyp 
1238  14 
val rep_ctyp : ctyp > {sign: Sign.sg, T: typ} 
15 
val typ_of : ctyp > typ 

16 
val ctyp_of : Sign.sg > typ > ctyp 

17 
val read_ctyp : Sign.sg > string > ctyp 

1160  18 

19 
(*certified terms*) 

20 
type cterm 

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

21 
exception CTERM of string 
4270  22 
val rep_cterm : cterm > {sign: Sign.sg, t: term, T: typ, maxidx: int} 
4288  23 
val crep_cterm : cterm > {sign: Sign.sg, t: term, T: ctyp, maxidx: int} 
9461  24 
val sign_of_cterm : cterm > Sign.sg 
1238  25 
val term_of : cterm > term 
26 
val cterm_of : Sign.sg > term > cterm 

2671  27 
val ctyp_of_term : cterm > ctyp 
1238  28 
val read_cterm : Sign.sg > string * typ > cterm 
29 
val cterm_fun : (term > term) > (cterm > cterm) 

1703
e22ad43bab5f
moved dest_cimplies to drule.ML; added adjust_maxidx
clasohm
parents:
1659
diff
changeset

30 
val adjust_maxidx : cterm > cterm 
1238  31 
val read_def_cterm : 
1160  32 
Sign.sg * (indexname > typ option) * (indexname > sort option) > 
33 
string list > bool > string * typ > cterm * (indexname * typ) list 

4281
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

34 
val read_def_cterms : 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

35 
Sign.sg * (indexname > typ option) * (indexname > sort option) > 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

36 
string list > bool > (string * typ)list 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

37 
> cterm list * (indexname * typ)list 
1160  38 

6089  39 
type tag (* = string * string list *) 
1529  40 

1160  41 
(*meta theorems*) 
42 
type thm 

11518  43 
val rep_thm : thm > {sign: Sign.sg, der: bool * Proofterm.proof, maxidx: int, 
2386  44 
shyps: sort list, hyps: term list, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

45 
tpairs: (term * term) list, prop: term} 
11518  46 
val crep_thm : thm > {sign: Sign.sg, der: bool * Proofterm.proof, maxidx: int, 
2386  47 
shyps: sort list, hyps: cterm list, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

48 
tpairs: (cterm * cterm) list, prop: cterm} 
6089  49 
exception THM of string * int * thm list 
50 
type 'a attribute (* = 'a * thm > 'a * thm *) 

3994  51 
val eq_thm : thm * thm > bool 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

52 
val sign_of_thm : thm > Sign.sg 
12803  53 
val prop_of : thm > term 
13528  54 
val proof_of : thm > Proofterm.proof 
4254  55 
val transfer_sg : Sign.sg > thm > thm 
3895  56 
val transfer : theory > thm > thm 
1238  57 
val tpairs_of : thm > (term * term) list 
58 
val prems_of : thm > term list 

59 
val nprems_of : thm > int 

60 
val concl_of : thm > term 

61 
val cprop_of : thm > cterm 

62 
val extra_shyps : thm > sort list 

63 
val strip_shyps : thm > thm 

3812  64 
val get_axiom : theory > xstring > thm 
6368  65 
val def_name : string > string 
4847  66 
val get_def : theory > xstring > thm 
1238  67 
val axioms_of : theory > (string * thm) list 
1160  68 

69 
(*meta rules*) 

1238  70 
val assume : cterm > thm 
1416  71 
val compress : thm > thm 
1238  72 
val implies_intr : cterm > thm > thm 
73 
val implies_elim : thm > thm > thm 

74 
val forall_intr : cterm > thm > thm 

75 
val forall_elim : cterm > thm > thm 

76 
val reflexive : cterm > thm 

77 
val symmetric : thm > thm 

78 
val transitive : thm > thm > thm 

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

79 
val beta_conversion : bool > cterm > thm 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

80 
val eta_conversion : cterm > thm 
1238  81 
val abstract_rule : string > cterm > thm > thm 
82 
val combination : thm > thm > thm 

83 
val equal_intr : thm > thm > thm 

84 
val equal_elim : thm > thm > thm 

85 
val implies_intr_hyps : thm > thm 

4270  86 
val flexflex_rule : thm > thm Seq.seq 
1238  87 
val instantiate : 
1160  88 
(indexname * ctyp) list * (cterm * cterm) list > thm > thm 
1238  89 
val trivial : cterm > thm 
6368  90 
val class_triv : Sign.sg > class > thm 
1238  91 
val varifyT : thm > thm 
12500  92 
val varifyT' : string list > thm > thm * (string * indexname) list 
1238  93 
val freezeT : thm > thm 
94 
val dest_state : thm * int > 

1160  95 
(term * term) list * term list * term * term 
1238  96 
val lift_rule : (thm * int) > thm > thm 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

97 
val incr_indexes : int > thm > thm 
4270  98 
val assumption : int > thm > thm Seq.seq 
1238  99 
val eq_assumption : int > thm > thm 
2671  100 
val rotate_rule : int > int > thm > thm 
7248
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

101 
val permute_prems : int > int > thm > thm 
1160  102 
val rename_params_rule: string list * int > thm > thm 
1238  103 
val bicompose : bool > bool * thm * int > 
4270  104 
int > thm > thm Seq.seq 
1238  105 
val biresolution : bool > (bool * thm) list > 
4270  106 
int > thm > thm Seq.seq 
4999  107 
val invoke_oracle : theory > xstring > Sign.sg * Object.T > thm 
250  108 
end; 
0  109 

6089  110 
signature THM = 
111 
sig 

112 
include BASIC_THM 

15087  113 
val dest_ctyp : ctyp > ctyp list 
10767
8fa4aafa7314
Thm: dest_comb, dest_abs, capply, cabs no longer global;
wenzelm
parents:
10486
diff
changeset

114 
val dest_comb : cterm > cterm * cterm 
8fa4aafa7314
Thm: dest_comb, dest_abs, capply, cabs no longer global;
wenzelm
parents:
10486
diff
changeset

115 
val dest_abs : string option > cterm > cterm * cterm 
8fa4aafa7314
Thm: dest_comb, dest_abs, capply, cabs no longer global;
wenzelm
parents:
10486
diff
changeset

116 
val capply : cterm > cterm > cterm 
8fa4aafa7314
Thm: dest_comb, dest_abs, capply, cabs no longer global;
wenzelm
parents:
10486
diff
changeset

117 
val cabs : cterm > cterm > cterm 
8299  118 
val major_prem_of : thm > term 
7534  119 
val no_prems : thm > bool 
6089  120 
val no_attributes : 'a > 'a * 'b attribute list 
121 
val apply_attributes : ('a * thm) * 'a attribute list > ('a * thm) 

122 
val applys_attributes : ('a * thm list) * 'a attribute list > ('a * thm list) 

123 
val get_name_tags : thm > string * tag list 

124 
val put_name_tags : string * tag list > thm > thm 

125 
val name_of_thm : thm > string 

126 
val tags_of_thm : thm > tag list 

127 
val name_thm : string * thm > thm 

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

128 
val rename_boundvars : term > term > thm > thm 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

129 
val cterm_match : cterm * cterm > 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

130 
(indexname * ctyp) list * (cterm * cterm) list 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

131 
val cterm_first_order_match : cterm * cterm > 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

132 
(indexname * ctyp) list * (cterm * cterm) list 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

133 
val cterm_incr_indexes : int > cterm > cterm 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

134 
val terms_of_tpairs : (term * term) list > term list 
6089  135 
end; 
136 

3550  137 
structure Thm: THM = 
0  138 
struct 
250  139 

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

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

141 

250  142 
(** certified types **) 
143 

144 
(*certified typs under a signature*) 

145 

3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

146 
datatype ctyp = Ctyp of {sign_ref: Sign.sg_ref, T: typ}; 
250  147 

3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

148 
fun rep_ctyp (Ctyp {sign_ref, T}) = {sign = Sign.deref sign_ref, T = T}; 
250  149 
fun typ_of (Ctyp {T, ...}) = T; 
150 

151 
fun ctyp_of sign T = 

3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

152 
Ctyp {sign_ref = Sign.self_ref sign, T = Sign.certify_typ sign T}; 
250  153 

154 
fun read_ctyp sign s = 

3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

155 
Ctyp {sign_ref = Sign.self_ref sign, T = Sign.read_typ (sign, K None) s}; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

156 

15087  157 
fun dest_ctyp (Ctyp {sign_ref, T = Type (s, Ts)}) = 
158 
map (fn T => Ctyp {sign_ref = sign_ref, T = T}) Ts 

159 
 dest_ctyp ct = [ct]; 

160 

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

161 

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

162 

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

164 

250  165 
(*certified terms under a signature, with checked typ and maxidx of Vars*) 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

166 

3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

167 
datatype cterm = Cterm of {sign_ref: Sign.sg_ref, t: term, T: typ, maxidx: int}; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

168 

3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

169 
fun rep_cterm (Cterm {sign_ref, t, T, maxidx}) = 
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

170 
{sign = Sign.deref sign_ref, t = t, T = T, maxidx = maxidx}; 
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

171 

4288  172 
fun crep_cterm (Cterm {sign_ref, t, T, maxidx}) = 
173 
{sign = Sign.deref sign_ref, t = t, T = Ctyp {sign_ref = sign_ref, T = T}, 

174 
maxidx = maxidx}; 

175 

9461  176 
fun sign_of_cterm (Cterm {sign_ref, ...}) = Sign.deref sign_ref; 
177 

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

179 

3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

180 
fun ctyp_of_term (Cterm {sign_ref, T, ...}) = Ctyp {sign_ref = sign_ref, T = T}; 
2671  181 

250  182 
(*create a cterm by checking a "raw" term with respect to a signature*) 
183 
fun cterm_of sign tm = 

14828  184 
let val (t, T, maxidx) = Sign.certify_term (Sign.pp sign) sign tm 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

185 
in Cterm {sign_ref = Sign.self_ref sign, t = t, T = T, maxidx = maxidx} 
1394
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

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

187 

3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

188 
fun cterm_fun f (Cterm {sign_ref, t, ...}) = cterm_of (Sign.deref sign_ref) (f t); 
250  189 

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

190 

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

191 
exception CTERM of string; 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

192 

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

193 
(*Destruct application in cterms*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

194 
fun dest_comb (Cterm {sign_ref, T, maxidx, t = A $ B}) = 
1493
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

195 
let val typeA = fastype_of A; 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

196 
val typeB = 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

197 
case typeA of Type("fun",[S,T]) => S 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

198 
 _ => error "Function type expected in dest_comb"; 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

199 
in 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

200 
(Cterm {sign_ref=sign_ref, maxidx=maxidx, t=A, T=typeA}, 
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

201 
Cterm {sign_ref=sign_ref, maxidx=maxidx, t=B, T=typeB}) 
1493
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

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

203 
 dest_comb _ = raise CTERM "dest_comb"; 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

204 

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

205 
(*Destruct abstraction in cterms*) 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

206 
fun dest_abs a (Cterm {sign_ref, T as Type("fun",[_,S]), maxidx, t=Abs(x,ty,M)}) = 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

207 
let val (y,N) = variant_abs (if_none a x,ty,M) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

208 
in (Cterm {sign_ref = sign_ref, T = ty, maxidx = 0, t = Free(y,ty)}, 
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

209 
Cterm {sign_ref = sign_ref, T = S, maxidx = maxidx, t = N}) 
1493
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

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

211 
 dest_abs _ _ = raise CTERM "dest_abs"; 
1493
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

212 

2147  213 
(*Makes maxidx precise: it is often too big*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

214 
fun adjust_maxidx (ct as Cterm {sign_ref, T, t, maxidx, ...}) = 
2147  215 
if maxidx = ~1 then ct 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

216 
else Cterm {sign_ref = sign_ref, T = T, maxidx = maxidx_of_term t, t = t}; 
1703
e22ad43bab5f
moved dest_cimplies to drule.ML; added adjust_maxidx
clasohm
parents:
1659
diff
changeset

217 

1516
96286c4e32de
removed mk_prop; added capply; simplified dest_abs
clasohm
parents:
1503
diff
changeset

218 
(*Form cterm out of a function and an argument*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

219 
fun capply (Cterm {t=f, sign_ref=sign_ref1, T=Type("fun",[dty,rty]), maxidx=maxidx1}) 
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

220 
(Cterm {t=x, sign_ref=sign_ref2, T, maxidx=maxidx2}) = 
8291  221 
if T = dty then 
15087  222 
Cterm{t = if maxidx1 >= 0 andalso maxidx2 >= 0 then Sign.nodup_vars (f $ x) 
223 
else f $ x, (*no new Vars: no expensive check!*) 

224 
sign_ref=Sign.merge_refs(sign_ref1,sign_ref2), T=rty, 

8291  225 
maxidx=Int.max(maxidx1, maxidx2)} 
1516
96286c4e32de
removed mk_prop; added capply; simplified dest_abs
clasohm
parents:
1503
diff
changeset

226 
else raise CTERM "capply: types don't agree" 
96286c4e32de
removed mk_prop; added capply; simplified dest_abs
clasohm
parents:
1503
diff
changeset

227 
 capply _ _ = raise CTERM "capply: first arg is not a function" 
250  228 

3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

229 
fun cabs (Cterm {t=Free(a,ty), sign_ref=sign_ref1, T=T1, maxidx=maxidx1}) 
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

230 
(Cterm {t=t2, sign_ref=sign_ref2, T=T2, maxidx=maxidx2}) = 
8291  231 
Cterm {t=Sign.nodup_vars (absfree(a,ty,t2)), sign_ref=Sign.merge_refs(sign_ref1,sign_ref2), 
2147  232 
T = ty > T2, maxidx=Int.max(maxidx1, maxidx2)} 
1517  233 
 cabs _ _ = raise CTERM "cabs: first arg is not a free variable"; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

234 

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

235 
(*Matching of cterms*) 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

236 
fun gen_cterm_match mtch 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

237 
(Cterm {sign_ref = sign_ref1, maxidx = maxidx1, t = t1, ...}, 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

238 
Cterm {sign_ref = sign_ref2, maxidx = maxidx2, t = t2, ...}) = 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

240 
val sign_ref = Sign.merge_refs (sign_ref1, sign_ref2); 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

241 
val tsig = Sign.tsig_of (Sign.deref sign_ref); 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

242 
val (Tinsts, tinsts) = mtch tsig (t1, t2); 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

243 
val maxidx = Int.max (maxidx1, maxidx2); 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

244 
val vars = map dest_Var (term_vars t1); 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

245 
fun mk_cTinsts (ixn, T) = (ixn, Ctyp {sign_ref = sign_ref, T = T}); 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

246 
fun mk_ctinsts (ixn, t) = 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

247 
let val T = typ_subst_TVars Tinsts (the (assoc (vars, ixn))) 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

249 
(Cterm {sign_ref = sign_ref, maxidx = maxidx, T = T, t = Var (ixn, T)}, 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

250 
Cterm {sign_ref = sign_ref, maxidx = maxidx, T = T, t = t}) 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

252 
in (map mk_cTinsts Tinsts, map mk_ctinsts tinsts) end; 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

253 

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

254 
val cterm_match = gen_cterm_match Pattern.match; 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

255 
val cterm_first_order_match = gen_cterm_match Pattern.first_order_match; 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

256 

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

257 
(*Incrementing indexes*) 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

258 
fun cterm_incr_indexes i (ct as Cterm {sign_ref, maxidx, t, T}) = 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

259 
if i < 0 then raise CTERM "negative increment" else 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

260 
if i = 0 then ct else 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

261 
Cterm {sign_ref = sign_ref, maxidx = maxidx + i, 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

262 
t = Logic.incr_indexes ([], i) t, T = Term.incr_tvar i T}; 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

263 

2509  264 

265 

574  266 
(** read cterms **) (*exception ERROR*) 
250  267 

4281
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

268 
(*read terms, infer types, certify terms*) 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

269 
fun read_def_cterms (sign, types, sorts) used freeze sTs = 
250  270 
let 
8608  271 
val (ts', tye) = Sign.read_def_terms (sign, types, sorts) used freeze sTs; 
4281
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

272 
val cts = map (cterm_of sign) ts' 
2979  273 
handle TYPE (msg, _, _) => error msg 
2386  274 
 TERM (msg, _) => error msg; 
4281
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

275 
in (cts, tye) end; 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

276 

6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

277 
(*read term, infer types, certify term*) 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

278 
fun read_def_cterm args used freeze aT = 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

279 
let val ([ct],tye) = read_def_cterms args used freeze [aT] 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

280 
in (ct,tye) end; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

281 

949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

282 
fun read_cterm sign = #1 o read_def_cterm (sign, K None, K None) [] true; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

283 

250  284 

6089  285 
(*tags provide additional comment, apart from the axiom/theorem name*) 
286 
type tag = string * string list; 

287 

2509  288 

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

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

290 

11518  291 
structure Pt = Proofterm; 
292 

0  293 
datatype thm = Thm of 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

294 
{sign_ref: Sign.sg_ref, (*mutable reference to signature*) 
11518  295 
der: bool * Pt.proof, (*derivation*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

296 
maxidx: int, (*maximum index of any Var or TVar*) 
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

297 
shyps: sort list, (*sort hypotheses*) 
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

298 
hyps: term list, (*hypotheses*) 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

299 
tpairs: (term * term) list, (*flexflex pairs*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

300 
prop: term}; (*conclusion*) 
0  301 

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

302 
fun terms_of_tpairs tpairs = flat (map (op @ o pairself single) tpairs); 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

303 

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

304 
fun attach_tpairs tpairs prop = 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

305 
Logic.list_implies (map Logic.mk_equals tpairs, prop); 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

306 

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

307 
fun rep_thm (Thm {sign_ref, der, maxidx, shyps, hyps, tpairs, prop}) = 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

308 
{sign = Sign.deref sign_ref, der = der, maxidx = maxidx, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

309 
shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}; 
0  310 

1529  311 
(*Version of rep_thm returning cterms instead of terms*) 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

312 
fun crep_thm (Thm {sign_ref, der, maxidx, shyps, hyps, tpairs, prop}) = 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

313 
let fun ctermf max t = Cterm{sign_ref=sign_ref, t=t, T=propT, maxidx=max}; 
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

314 
in {sign = Sign.deref sign_ref, der = der, maxidx = maxidx, shyps = shyps, 
1529  315 
hyps = map (ctermf ~1) hyps, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

316 
tpairs = map (pairself (ctermf maxidx)) tpairs, 
1529  317 
prop = ctermf maxidx prop} 
1517  318 
end; 
319 

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

320 
(*errors involving theorems*) 
0  321 
exception THM of string * int * thm list; 
322 

6089  323 
(*attributes subsume any kind of rules or addXXXs modifiers*) 
324 
type 'a attribute = 'a * thm > 'a * thm; 

325 

326 
fun no_attributes x = (x, []); 

327 
fun apply_attributes (x_th, atts) = Library.apply atts x_th; 

328 
fun applys_attributes (x_ths, atts) = foldl_map (Library.apply atts) x_ths; 

329 

3994  330 
fun eq_thm (th1, th2) = 
331 
let 

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

332 
val {sign = sg1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1, prop = prop1, ...} = 
9031  333 
rep_thm th1; 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

334 
val {sign = sg2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...} = 
9031  335 
rep_thm th2; 
3994  336 
in 
9031  337 
Sign.joinable (sg1, sg2) andalso 
14791  338 
Sorts.eq_set_sort (shyps1, shyps2) andalso 
3994  339 
aconvs (hyps1, hyps2) andalso 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

340 
aconvs (terms_of_tpairs tpairs1, terms_of_tpairs tpairs2) andalso 
3994  341 
prop1 aconv prop2 
342 
end; 

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

343 

3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

344 
fun sign_of_thm (Thm {sign_ref, ...}) = Sign.deref sign_ref; 
12803  345 
fun prop_of (Thm {prop, ...}) = prop; 
13528  346 
fun proof_of (Thm {der = (_, proof), ...}) = proof; 
0  347 

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

348 
(*merge signatures of two theorems; raise exception if incompatible*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

349 
fun merge_thm_sgs 
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

350 
(th1 as Thm {sign_ref = sgr1, ...}, th2 as Thm {sign_ref = sgr2, ...}) = 
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

351 
Sign.merge_refs (sgr1, sgr2) handle TERM (msg, _) => raise THM (msg, 0, [th1, th2]); 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

352 

3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

353 
(*transfer thm to super theory (nondestructive)*) 
4254  354 
fun transfer_sg sign' thm = 
3895  355 
let 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

356 
val Thm {sign_ref, der, maxidx, shyps, hyps, tpairs, prop} = thm; 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

357 
val sign = Sign.deref sign_ref; 
3895  358 
in 
4254  359 
if Sign.eq_sg (sign, sign') then thm 
360 
else if Sign.subsig (sign, sign') then 

3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

361 
Thm {sign_ref = Sign.self_ref sign', der = der, maxidx = maxidx, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

362 
shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop} 
3895  363 
else raise THM ("transfer: not a super theory", 0, [thm]) 
364 
end; 

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

365 

6390  366 
val transfer = transfer_sg o Theory.sign_of; 
4254  367 

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

368 
(*maps objectrule to tpairs*) 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

369 
fun tpairs_of (Thm {tpairs, ...}) = tpairs; 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

370 

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

371 
(*maps objectrule to premises*) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

372 
fun prems_of (Thm {prop, ...}) = 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

373 
Logic.strip_imp_prems prop; 
0  374 

375 
(*counts premises in a rule*) 

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

376 
fun nprems_of (Thm {prop, ...}) = 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

377 
Logic.count_prems (prop, 0); 
0  378 

8299  379 
fun major_prem_of thm = 
380 
(case prems_of thm of 

11692  381 
prem :: _ => Logic.strip_assums_concl prem 
8299  382 
 [] => raise THM ("major_prem_of: rule with no premises", 0, [thm])); 
383 

7534  384 
fun no_prems thm = nprems_of thm = 0; 
385 

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

386 
(*maps objectrule to conclusion*) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

387 
fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop; 
0  388 

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

389 
(*the statement of any thm is a cterm*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

390 
fun cprop_of (Thm {sign_ref, maxidx, prop, ...}) = 
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

391 
Cterm {sign_ref = sign_ref, maxidx = maxidx, T = propT, t = prop}; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

392 

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

393 

0  394 

1238  395 
(** sort contexts of theorems **) 
396 

397 
(* basic utils *) 

398 

2163  399 
(*accumulate sorts suppressing duplicates; these are coded low levelly 
1238  400 
to improve efficiency a bit*) 
401 

402 
fun add_typ_sorts (Type (_, Ts), Ss) = add_typs_sorts (Ts, Ss) 

14791  403 
 add_typ_sorts (TFree (_, S), Ss) = Sorts.ins_sort(S,Ss) 
404 
 add_typ_sorts (TVar (_, S), Ss) = Sorts.ins_sort(S,Ss) 

1238  405 
and add_typs_sorts ([], Ss) = Ss 
406 
 add_typs_sorts (T :: Ts, Ss) = add_typs_sorts (Ts, add_typ_sorts (T, Ss)); 

407 

408 
fun add_term_sorts (Const (_, T), Ss) = add_typ_sorts (T, Ss) 

409 
 add_term_sorts (Free (_, T), Ss) = add_typ_sorts (T, Ss) 

410 
 add_term_sorts (Var (_, T), Ss) = add_typ_sorts (T, Ss) 

411 
 add_term_sorts (Bound _, Ss) = Ss 

2177
8b365a3a6ed1
Changed some mem, ins and union calls to be monomorphic
paulson
parents:
2163
diff
changeset

412 
 add_term_sorts (Abs (_,T,t), Ss) = add_term_sorts (t, add_typ_sorts (T,Ss)) 
1238  413 
 add_term_sorts (t $ u, Ss) = add_term_sorts (t, add_term_sorts (u, Ss)); 
414 

415 
fun add_terms_sorts ([], Ss) = Ss 

2177
8b365a3a6ed1
Changed some mem, ins and union calls to be monomorphic
paulson
parents:
2163
diff
changeset

416 
 add_terms_sorts (t::ts, Ss) = add_terms_sorts (ts, add_term_sorts (t,Ss)); 
1238  417 

8407
d522ad1809e9
Envir now uses Vartab instead of association lists.
berghofe
parents:
8299
diff
changeset

418 
fun env_codT (Envir.Envir {iTs, ...}) = map snd (Vartab.dest iTs); 
1258  419 

8407
d522ad1809e9
Envir now uses Vartab instead of association lists.
berghofe
parents:
8299
diff
changeset

420 
fun add_env_sorts (Envir.Envir {iTs, asol, ...}, Ss) = 
d522ad1809e9
Envir now uses Vartab instead of association lists.
berghofe
parents:
8299
diff
changeset

421 
Vartab.foldl (add_term_sorts o swap o apsnd snd) 
d522ad1809e9
Envir now uses Vartab instead of association lists.
berghofe
parents:
8299
diff
changeset

422 
(Vartab.foldl (add_typ_sorts o swap o apsnd snd) (Ss, iTs), asol); 
1258  423 

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

424 
fun add_insts_sorts ((iTs, is), Ss) = 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

425 
add_typs_sorts (map snd iTs, add_terms_sorts (map snd is, Ss)); 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

426 

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

427 
fun add_thm_sorts (Thm {hyps, tpairs, prop, ...}, Ss) = 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

428 
add_terms_sorts (hyps @ terms_of_tpairs tpairs, add_term_sorts (prop, Ss)); 
1238  429 

430 
fun add_thms_shyps ([], Ss) = Ss 

431 
 add_thms_shyps (Thm {shyps, ...} :: ths, Ss) = 

14791  432 
add_thms_shyps (ths, Sorts.union_sort (shyps, Ss)); 
1238  433 

434 

435 
(*get 'dangling' sort constraints of a thm*) 

436 
fun extra_shyps (th as Thm {shyps, ...}) = 

14791  437 
Sorts.rems_sort (shyps, add_thm_sorts (th, [])); 
1238  438 

439 

440 
(* fix_shyps *) 

441 

14791  442 
fun all_sorts_nonempty sign_ref = is_some (Sign.universal_witness (Sign.deref sign_ref)); 
7642  443 

1238  444 
(*preserve sort contexts of rule premises and substituted types*) 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

445 
fun fix_shyps thms Ts (thm as Thm {sign_ref, der, maxidx, hyps, tpairs, prop, ...}) = 
7642  446 
Thm 
447 
{sign_ref = sign_ref, 

448 
der = der, (*no new derivation, as other rules call this*) 

449 
maxidx = maxidx, 

450 
shyps = 

451 
if all_sorts_nonempty sign_ref then [] 

452 
else add_thm_sorts (thm, add_typs_sorts (Ts, add_thms_shyps (thms, []))), 

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

453 
hyps = hyps, tpairs = tpairs, prop = prop} 
1238  454 

455 

7642  456 
(* strip_shyps *) 
1238  457 

7642  458 
(*remove extra sorts that are nonempty by virtue of type signature information*) 
459 
fun strip_shyps (thm as Thm {shyps = [], ...}) = thm 

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

460 
 strip_shyps (thm as Thm {sign_ref, der, maxidx, shyps, hyps, tpairs, prop}) = 
7642  461 
let 
462 
val sign = Sign.deref sign_ref; 

1238  463 

7642  464 
val present_sorts = add_thm_sorts (thm, []); 
14791  465 
val extra_shyps = Sorts.rems_sort (shyps, present_sorts); 
7642  466 
val witnessed_shyps = Sign.witness_sorts sign present_sorts extra_shyps; 
467 
in 

468 
Thm {sign_ref = sign_ref, der = der, maxidx = maxidx, 

14791  469 
shyps = Sorts.rems_sort (shyps, map #2 witnessed_shyps), 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

470 
hyps = hyps, tpairs = tpairs, prop = prop} 
7642  471 
end; 
1238  472 

473 

474 

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

476 

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

477 
(*look up the named axiom in the theory*) 
3812  478 
fun get_axiom theory raw_name = 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

479 
let 
4847  480 
val name = Sign.intern (Theory.sign_of theory) Theory.axiomK raw_name; 
481 

482 
fun get_ax [] = None 

1529  483 
 get_ax (thy :: thys) = 
4847  484 
let val {sign, axioms, ...} = Theory.rep_theory thy in 
485 
(case Symtab.lookup (axioms, name) of 

486 
Some t => 

487 
Some (fix_shyps [] [] 

488 
(Thm {sign_ref = Sign.self_ref sign, 

11518  489 
der = Pt.infer_derivs' I 
490 
(false, Pt.axm_proof name t), 

4847  491 
maxidx = maxidx_of_term t, 
492 
shyps = [], 

493 
hyps = [], 

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

494 
tpairs = [], 
4847  495 
prop = t})) 
496 
 None => get_ax thys) 

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

498 
in 
4847  499 
(case get_ax (theory :: Theory.ancestors_of theory) of 
500 
Some thm => thm 

501 
 None => raise THEORY ("No axiom " ^ quote name, [theory])) 

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

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

503 

6368  504 
fun def_name name = name ^ "_def"; 
505 
fun get_def thy = get_axiom thy o def_name; 

4847  506 

1529  507 

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

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

509 
fun axioms_of thy = 
df8f91c0e57c
improved axioms_of: returns thms as the manual says;
wenzelm
parents:
721
diff
changeset

510 
map (fn (s, _) => (s, get_axiom thy s)) 
6390  511 
(Symtab.dest (#axioms (Theory.rep_theory thy))); 
776
df8f91c0e57c
improved axioms_of: returns thms as the manual says;
wenzelm
parents:
721
diff
changeset

512 

6089  513 

514 
(* name and tags  make proof objects more readable *) 

515 

12923  516 
fun get_name_tags (Thm {hyps, prop, der = (_, prf), ...}) = 
517 
Pt.get_name_tags hyps prop prf; 

4018  518 

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

519 
fun put_name_tags x (Thm {sign_ref, der = (ora, prf), maxidx, 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

520 
shyps, hyps, tpairs = [], prop}) = Thm {sign_ref = sign_ref, 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

521 
der = (ora, Pt.thm_proof (Sign.deref sign_ref) x hyps prop prf), 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

522 
maxidx = maxidx, shyps = shyps, hyps = hyps, tpairs = [], prop = prop} 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

523 
 put_name_tags _ thm = 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

524 
raise THM ("put_name_tags: unsolved flexflex constraints", 0, [thm]); 
6089  525 

526 
val name_of_thm = #1 o get_name_tags; 

527 
val tags_of_thm = #2 o get_name_tags; 

528 

529 
fun name_thm (name, thm) = put_name_tags (name, tags_of_thm thm) thm; 

0  530 

531 

1529  532 
(*Compression of theorems  a separate rule, not integrated with the others, 
533 
as it could be slow.*) 

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

534 
fun compress (Thm {sign_ref, der, maxidx, shyps, hyps, tpairs, prop}) = 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

535 
Thm {sign_ref = sign_ref, 
2386  536 
der = der, (*No derivation recorded!*) 
537 
maxidx = maxidx, 

538 
shyps = shyps, 

539 
hyps = map Term.compress_term hyps, 

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

540 
tpairs = map (pairself Term.compress_term) tpairs, 
2386  541 
prop = Term.compress_term prop}; 
564  542 

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

543 

2509  544 

1529  545 
(*** Meta rules ***) 
0  546 

2147  547 
(*Check that term does not contain same var with different typing/sorting. 
548 
If this check must be made, recalculate maxidx in hope of preventing its 

549 
recurrence.*) 

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

550 
fun nodup_vars (thm as Thm{sign_ref, der, maxidx, shyps, hyps, tpairs, prop}) s = 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

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

552 
val prop' = attach_tpairs tpairs prop; 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

553 
val _ = Sign.nodup_vars prop' 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

554 
in Thm {sign_ref = sign_ref, 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

555 
der = der, 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

556 
maxidx = maxidx_of_term prop', 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

557 
shyps = shyps, 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

558 
hyps = hyps, 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

559 
tpairs = tpairs, 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

560 
prop = prop} 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

561 
end handle TYPE(msg,Ts,ts) => raise TYPE(s^": "^msg,Ts,ts); 
1495
b8b54847c77f
Added check for duplicate vars with distinct types/sorts (nodup_Vars)
nipkow
parents:
1493
diff
changeset

562 

8291  563 

1220  564 
(** 'primitive' rules **) 
565 

566 
(*discharge all assumptions t from ts*) 

0  567 
val disch = gen_rem (op aconv); 
568 

1220  569 
(*The assumption rule AA in a theory*) 
5344  570 
fun assume raw_ct : thm = 
571 
let val ct as Cterm {sign_ref, t=prop, T, maxidx} = adjust_maxidx raw_ct 

250  572 
in if T<>propT then 
573 
raise THM("assume: assumptions must have type prop", 0, []) 

0  574 
else if maxidx <> ~1 then 
250  575 
raise THM("assume: assumptions may not contain scheme variables", 
576 
maxidx, []) 

3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

577 
else Thm{sign_ref = sign_ref, 
11518  578 
der = Pt.infer_derivs' I (false, Pt.Hyp prop), 
2386  579 
maxidx = ~1, 
580 
shyps = add_term_sorts(prop,[]), 

581 
hyps = [prop], 

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

582 
tpairs = [], 
2386  583 
prop = prop} 
0  584 
end; 
585 

1220  586 
(*Implication introduction 
3529  587 
[A] 
588 
: 

589 
B 

1220  590 
 
591 
A ==> B 

592 
*) 

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

593 
fun implies_intr cA (thB as Thm{sign_ref,der,maxidx,hyps,shyps,tpairs,prop}) : thm = 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

594 
let val Cterm {sign_ref=sign_refA, t=A, T, maxidx=maxidxA} = cA 
0  595 
in if T<>propT then 
250  596 
raise THM("implies_intr: assumptions must have type prop", 0, [thB]) 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

598 
Thm{sign_ref = Sign.merge_refs (sign_ref,sign_refA), 
11518  599 
der = Pt.infer_derivs' (Pt.implies_intr_proof A) der, 
2386  600 
maxidx = Int.max(maxidxA, maxidx), 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

601 
shyps = add_term_sorts (A, shyps), 
2386  602 
hyps = disch(hyps,A), 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

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

604 
prop = implies$A$prop} 
0  605 
handle TERM _ => 
606 
raise THM("implies_intr: incompatible signatures", 0, [thB]) 

607 
end; 

608 

1529  609 

1220  610 
(*Implication elimination 
611 
A ==> B A 

612 
 

613 
B 

614 
*) 

0  615 
fun implies_elim thAB thA : thm = 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

616 
let val Thm{maxidx=maxA, der=derA, hyps=hypsA, shyps=shypsA, tpairs=tpairsA, prop=propA, ...} = thA 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

617 
and Thm{der, maxidx, hyps, shyps, tpairs, prop, ...} = thAB; 
250  618 
fun err(a) = raise THM("implies_elim: "^a, 0, [thAB,thA]) 
0  619 
in case prop of 
250  620 
imp$A$B => 
621 
if imp=implies andalso A aconv propA 

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

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

623 
Thm{sign_ref= merge_thm_sgs(thAB,thA), 
11612  624 
der = Pt.infer_derivs (curry Pt.%%) der derA, 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

625 
maxidx = Int.max(maxA,maxidx), 
14791  626 
shyps = Sorts.union_sort (shypsA, shyps), 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

627 
hyps = union_term(hypsA,hyps), (*dups suppressed*) 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

628 
tpairs = tpairsA @ tpairs, 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

629 
prop = B} 
250  630 
else err("major premise") 
631 
 _ => err("major premise") 

0  632 
end; 
250  633 

1220  634 
(*Forall introduction. The Free or Var x must not be free in the hypotheses. 
635 
A 

636 
 

637 
!!x.A 

638 
*) 

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

639 
fun forall_intr cx (th as Thm{sign_ref,der,maxidx,hyps,tpairs,prop,...}) = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

640 
let val x = term_of cx; 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

641 
fun result a T = fix_shyps [th] [] 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

642 
(Thm{sign_ref = sign_ref, 
11518  643 
der = Pt.infer_derivs' (Pt.forall_intr_proof x a) der, 
2386  644 
maxidx = maxidx, 
645 
shyps = [], 

646 
hyps = hyps, 

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

647 
tpairs = tpairs, 
2386  648 
prop = all(T) $ Abs(a, T, abstract_over (x,prop))}) 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

649 
fun check_occs x ts = 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

650 
if exists (apl(x, Logic.occs)) ts 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

651 
then raise THM("forall_intr: variable free in assumptions", 0, [th]) 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

652 
else () 
0  653 
in case x of 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

654 
Free(a,T) => (check_occs x (hyps @ terms_of_tpairs tpairs); result a T) 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

655 
 Var((a,_),T) => (check_occs x (terms_of_tpairs tpairs); result a T) 
0  656 
 _ => raise THM("forall_intr: not a variable", 0, [th]) 
657 
end; 

658 

1220  659 
(*Forall elimination 
660 
!!x.A 

661 
 

662 
A[t/x] 

663 
*) 

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

664 
fun forall_elim ct (th as Thm{sign_ref,der,maxidx,hyps,tpairs,prop,...}) : thm = 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

665 
let val Cterm {sign_ref=sign_reft, t, T, maxidx=maxt} = ct 
0  666 
in case prop of 
2386  667 
Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A => 
668 
if T<>qary then 

669 
raise THM("forall_elim: type mismatch", 0, [th]) 

670 
else let val thm = fix_shyps [th] [] 

3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

671 
(Thm{sign_ref= Sign.merge_refs(sign_ref,sign_reft), 
11612  672 
der = Pt.infer_derivs' (Pt.% o rpair (Some t)) der, 
2386  673 
maxidx = Int.max(maxidx, maxt), 
674 
shyps = [], 

675 
hyps = hyps, 

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

676 
tpairs = tpairs, 
2386  677 
prop = betapply(A,t)}) 
678 
in if maxt >= 0 andalso maxidx >= 0 

8291  679 
then nodup_vars thm "forall_elim" 
2386  680 
else thm (*no new Vars: no expensive check!*) 
681 
end 

2147  682 
 _ => raise THM("forall_elim: not quantified", 0, [th]) 
0  683 
end 
684 
handle TERM _ => 

250  685 
raise THM("forall_elim: incompatible signatures", 0, [th]); 
0  686 

687 

1220  688 
(* Equality *) 
0  689 

690 
(*The reflexivity rule: maps t to the theorem t==t *) 

250  691 
fun reflexive ct = 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

692 
let val Cterm {sign_ref, t, T, maxidx} = ct 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

693 
in Thm{sign_ref= sign_ref, 
11518  694 
der = Pt.infer_derivs' I (false, Pt.reflexive), 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

695 
shyps = add_term_sorts (t, []), 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

696 
hyps = [], 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

698 
tpairs = [], 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

699 
prop = Logic.mk_equals(t,t)} 
0  700 
end; 
701 

702 
(*The symmetry rule 

1220  703 
t==u 
704 
 

705 
u==t 

706 
*) 

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

707 
fun symmetric (th as Thm{sign_ref,der,maxidx,shyps,hyps,tpairs,prop}) = 
0  708 
case prop of 
11518  709 
(eq as Const("==", Type (_, [T, _]))) $ t $ u => 
1238  710 
(*no fix_shyps*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

711 
Thm{sign_ref = sign_ref, 
11518  712 
der = Pt.infer_derivs' Pt.symmetric der, 
2386  713 
maxidx = maxidx, 
714 
shyps = shyps, 

715 
hyps = hyps, 

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

716 
tpairs = tpairs, 
2386  717 
prop = eq$u$t} 
0  718 
 _ => raise THM("symmetric", 0, [th]); 
719 

720 
(*The transitive rule 

1220  721 
t1==u u==t2 
722 
 

723 
t1==t2 

724 
*) 

0  725 
fun transitive th1 th2 = 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

726 
let val Thm{der=der1, maxidx=max1, hyps=hyps1, shyps=shyps1, tpairs=tpairs1, prop=prop1,...} = th1 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

727 
and Thm{der=der2, maxidx=max2, hyps=hyps2, shyps=shyps2, tpairs=tpairs2, prop=prop2,...} = th2; 
0  728 
fun err(msg) = raise THM("transitive: "^msg, 0, [th1,th2]) 
729 
in case (prop1,prop2) of 

11518  730 
((eq as Const("==", Type (_, [T, _]))) $ t1 $ u, Const("==",_) $ u' $ t2) => 
1634  731 
if not (u aconv u') then err"middle term" 
732 
else let val thm = 

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

733 
Thm{sign_ref= merge_thm_sgs(th1,th2), 
11518  734 
der = Pt.infer_derivs (Pt.transitive u T) der1 der2, 
2147  735 
maxidx = Int.max(max1,max2), 
14791  736 
shyps = Sorts.union_sort (shyps1, shyps2), 
2386  737 
hyps = union_term(hyps1,hyps2), 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

738 
tpairs = tpairs1 @ tpairs2, 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

739 
prop = eq$t1$t2} 
2139
2c59b204b540
Only calls nodup_Vars if really necessary. We get a speedup of nearly 6%
paulson
parents:
2047
diff
changeset

740 
in if max1 >= 0 andalso max2 >= 0 
8291  741 
then nodup_vars thm "transitive" 
2147  742 
else thm (*no new Vars: no expensive check!*) 
2139
2c59b204b540
Only calls nodup_Vars if really necessary. We get a speedup of nearly 6%
paulson
parents:
2047
diff
changeset

743 
end 
0  744 
 _ => err"premises" 
745 
end; 

746 

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

747 
(*Betaconversion: maps (%x.t)(u) to the theorem (%x.t)(u) == t[u/x] 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

749 
*) 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

750 
fun beta_conversion full ct = 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

751 
let val Cterm {sign_ref, t, T, maxidx} = ct 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

752 
in Thm 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

753 
{sign_ref = sign_ref, 
11518  754 
der = Pt.infer_derivs' I (false, Pt.reflexive), 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

755 
maxidx = maxidx, 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

756 
shyps = add_term_sorts (t, []), 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

757 
hyps = [], 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

758 
tpairs = [], 
10486  759 
prop = Logic.mk_equals (t, if full then Envir.beta_norm t 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

760 
else case t of 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

761 
Abs(_, _, bodt) $ u => subst_bound (u, bodt) 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

762 
 _ => raise THM ("beta_conversion: not a redex", 0, []))} 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

764 

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

765 
fun eta_conversion ct = 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

766 
let val Cterm {sign_ref, t, T, maxidx} = ct 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

767 
in Thm 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

768 
{sign_ref = sign_ref, 
11518  769 
der = Pt.infer_derivs' I (false, Pt.reflexive), 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

770 
maxidx = maxidx, 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

771 
shyps = add_term_sorts (t, []), 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

772 
hyps = [], 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

773 
tpairs = [], 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

774 
prop = Logic.mk_equals (t, Pattern.eta_contract t)} 
0  775 
end; 
776 

777 
(*The abstraction rule. The Free or Var x must not be free in the hypotheses. 

778 
The bound variable will be named "a" (since x will be something like x320) 

1220  779 
t == u 
780 
 

781 
%x.t == %x.u 

782 
*) 

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

783 
fun abstract_rule a cx (th as Thm{sign_ref,der,maxidx,hyps,shyps,tpairs,prop}) = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

784 
let val x = term_of cx; 
250  785 
val (t,u) = Logic.dest_equals prop 
786 
handle TERM _ => 

787 
raise THM("abstract_rule: premise not an equality", 0, [th]) 

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

788 
fun result T = 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

789 
Thm{sign_ref = sign_ref, 
11518  790 
der = Pt.infer_derivs' (Pt.abstract_rule x a) der, 
2386  791 
maxidx = maxidx, 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

792 
shyps = add_typ_sorts (T, shyps), 
2386  793 
hyps = hyps, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

794 
tpairs = tpairs, 
2386  795 
prop = Logic.mk_equals(Abs(a, T, abstract_over (x,t)), 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

796 
Abs(a, T, abstract_over (x,u)))} 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

797 
fun check_occs x ts = 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

798 
if exists (apl(x, Logic.occs)) ts 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

799 
then raise THM("abstract_rule: variable free in assumptions", 0, [th]) 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

800 
else () 
0  801 
in case x of 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

802 
Free(_,T) => (check_occs x (hyps @ terms_of_tpairs tpairs); result T) 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

803 
 Var(_,T) => (check_occs x (terms_of_tpairs tpairs); result T) 
0  804 
 _ => raise THM("abstract_rule: not a variable", 0, [th]) 
805 
end; 

806 

807 
(*The combination rule 

3529  808 
f == g t == u 
809 
 

810 
f(t) == g(u) 

1220  811 
*) 
0  812 
fun combination th1 th2 = 
1529  813 
let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

814 
tpairs=tpairs1, prop=prop1,...} = th1 
1529  815 
and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

816 
tpairs=tpairs2, prop=prop2,...} = th2 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

817 
fun chktypes fT tT = 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

818 
(case fT of 
2386  819 
Type("fun",[T1,T2]) => 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

820 
if T1 <> tT then 
2386  821 
raise THM("combination: types", 0, [th1,th2]) 
822 
else () 

823 
 _ => raise THM("combination: not function type", 0, 

824 
[th1,th2])) 

1495
b8b54847c77f
Added check for duplicate vars with distinct types/sorts (nodup_Vars)
nipkow
parents:
1493
diff
changeset

825 
in case (prop1,prop2) of 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

826 
(Const ("==", Type ("fun", [fT, _])) $ f $ g, 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

827 
Const ("==", Type ("fun", [tT, _])) $ t $ u) => 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

828 
let val _ = chktypes fT tT 
2386  829 
val thm = (*no fix_shyps*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

830 
Thm{sign_ref = merge_thm_sgs(th1,th2), 
11518  831 
der = Pt.infer_derivs 
832 
(Pt.combination f g t u fT) der1 der2, 

2386  833 
maxidx = Int.max(max1,max2), 
14791  834 
shyps = Sorts.union_sort(shyps1,shyps2), 
2386  835 
hyps = union_term(hyps1,hyps2), 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

836 
tpairs = tpairs1 @ tpairs2, 
2386  837 
prop = Logic.mk_equals(f$t, g$u)} 
2139
2c59b204b540
Only calls nodup_Vars if really necessary. We get a speedup of nearly 6%
paulson
parents:
2047
diff
changeset

838 
in if max1 >= 0 andalso max2 >= 0 
8291  839 
then nodup_vars thm "combination" 
2386  840 
else thm (*no new Vars: no expensive check!*) 
2139
2c59b204b540
Only calls nodup_Vars if really necessary. We get a speedup of nearly 6%
paulson
parents:
2047
diff
changeset

841 
end 
0  842 
 _ => raise THM("combination: premises", 0, [th1,th2]) 
843 
end; 

844 

845 

846 
(* Equality introduction 

3529  847 
A ==> B B ==> A 
848 
 

849 
A == B 

1220  850 
*) 
0  851 
fun equal_intr th1 th2 = 
11518  852 
let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

853 
tpairs=tpairs1, prop=prop1,...} = th1 
1529  854 
and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

855 
tpairs=tpairs2, prop=prop2,...} = th2; 
1529  856 
fun err(msg) = raise THM("equal_intr: "^msg, 0, [th1,th2]) 
857 
in case (prop1,prop2) of 

858 
(Const("==>",_) $ A $ B, Const("==>",_) $ B' $ A') => 

2386  859 
if A aconv A' andalso B aconv B' 
860 
then 

861 
(*no fix_shyps*) 

3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

862 
Thm{sign_ref = merge_thm_sgs(th1,th2), 
11518  863 
der = Pt.infer_derivs (Pt.equal_intr A B) der1 der2, 
2386  864 
maxidx = Int.max(max1,max2), 
14791  865 
shyps = Sorts.union_sort(shyps1,shyps2), 
2386  866 
hyps = union_term(hyps1,hyps2), 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

867 
tpairs = tpairs1 @ tpairs2, 
2386  868 
prop = Logic.mk_equals(A,B)} 
869 
else err"not equal" 

1529  870 
 _ => err"premises" 
871 
end; 

872 

873 

874 
(*The equal propositions rule 

3529  875 
A == B A 
1529  876 
 
877 
B 

878 
*) 

879 
fun equal_elim th1 th2 = 

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

880 
let val Thm{der=der1, maxidx=max1, hyps=hyps1, tpairs=tpairs1, prop=prop1,...} = th1 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

881 
and Thm{der=der2, maxidx=max2, hyps=hyps2, tpairs=tpairs2, prop=prop2,...} = th2; 
1529  882 
fun err(msg) = raise THM("equal_elim: "^msg, 0, [th1,th2]) 
883 
in case prop1 of 

884 
Const("==",_) $ A $ B => 

885 
if not (prop2 aconv A) then err"not equal" else 

886 
fix_shyps [th1, th2] [] 

3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

887 
(Thm{sign_ref= merge_thm_sgs(th1,th2), 
11518  888 
der = Pt.infer_derivs (Pt.equal_elim A B) der1 der2, 
2386  889 
maxidx = Int.max(max1,max2), 
890 
shyps = [], 

891 
hyps = union_term(hyps1,hyps2), 

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

892 
tpairs = tpairs1 @ tpairs2, 
2386  893 
prop = B}) 
1529  894 
 _ => err"major premise" 
895 
end; 

0  896 

1220  897 

898 

0  899 
(**** Derived rules ****) 
900 

1503  901 
(*Discharge all hypotheses. Need not verify cterms or call fix_shyps. 
0  902 
Repeated hypotheses are discharged only once; fold cannot do this*) 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

903 
fun implies_intr_hyps (Thm{sign_ref, der, maxidx, shyps, hyps=A::As, tpairs, prop}) = 
1238  904 
implies_intr_hyps (*no fix_shyps*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

905 
(Thm{sign_ref = sign_ref, 
11518  906 
der = Pt.infer_derivs' (Pt.implies_intr_proof A) der, 
2386  907 
maxidx = maxidx, 
908 
shyps = shyps, 

1529  909 
hyps = disch(As,A), 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

910 
tpairs = tpairs, 
2386  911 
prop = implies$A$prop}) 
0  912 
 implies_intr_hyps th = th; 
913 

914 
(*Smash" unifies the list of term pairs leaving no flexflex pairs. 

250  915 
Instantiates the theorem and deletes trivial tpairs. 
0  916 
Resulting sequence may contain multiple elements if the tpairs are 
917 
not all flexflex. *) 

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

918 
fun flexflex_rule (th as Thm{sign_ref, der, maxidx, hyps, tpairs, prop, ...}) = 
250  919 
let fun newthm env = 
1529  920 
if Envir.is_empty env then th 
921 
else 

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

922 
let val ntpairs = map (pairself (Envir.norm_term env)) tpairs; 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

923 
val newprop = Envir.norm_term env prop; 
250  924 
(*Remove trivial tpairs, of the form t=t*) 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

925 
val distpairs = filter (not o op aconv) ntpairs 
1220  926 
in fix_shyps [th] (env_codT env) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

927 
(Thm{sign_ref = sign_ref, 
11518  928 
der = Pt.infer_derivs' (Pt.norm_proof' env) der, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

929 
maxidx = maxidx_of_terms (newprop :: 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

930 
terms_of_tpairs distpairs), 
2386  931 
shyps = [], 
932 
hyps = hyps, 

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

933 
tpairs = distpairs, 
2386  934 
prop = newprop}) 
250  935 
end; 
4270  936 
in Seq.map newthm 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

937 
(Unify.smash_unifiers(Sign.deref sign_ref, Envir.empty maxidx, tpairs)) 
0  938 
end; 
939 

940 
(*Instantiation of Vars 

1220  941 
A 
942 
 

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

944 
*) 

0  945 

6928  946 
local 
947 

0  948 
(*Check that all the terms are Vars and are distinct*) 
949 
fun instl_ok ts = forall is_Var ts andalso null(findrep ts); 

950 

6928  951 
fun prt_typing sg_ref t T = 
952 
let val sg = Sign.deref sg_ref in 

953 
Pretty.block [Sign.pretty_term sg t, Pretty.str " ::", Pretty.brk 1, Sign.pretty_typ sg T] 

954 
end; 

955 

0  956 
(*For instantiate: process pair of cterms, merge theories*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

957 
fun add_ctpair ((ct,cu), (sign_ref,tpairs)) = 
6928  958 
let 
959 
val Cterm {sign_ref=sign_reft, t=t, T= T, ...} = ct 

960 
and Cterm {sign_ref=sign_refu, t=u, T= U, ...} = cu; 

961 
val sign_ref_merged = Sign.merge_refs (sign_ref, Sign.merge_refs (sign_reft, sign_refu)); 

3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

962 
in 
6928  963 
if T=U then (sign_ref_merged, (t,u)::tpairs) 
964 
else raise TYPE (Pretty.string_of (Pretty.block [Pretty.str "instantiate: type conflict", 

965 
Pretty.fbrk, prt_typing sign_ref_merged t T, 

966 
Pretty.fbrk, prt_typing sign_ref_merged u U]), [T,U], [t,u]) 

0  967 
end; 
968 

3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

969 
fun add_ctyp ((v,ctyp), (sign_ref',vTs)) = 
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

970 
let val Ctyp {T,sign_ref} = ctyp 
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

971 
in (Sign.merge_refs(sign_ref,sign_ref'), (v,T)::vTs) end; 
0  972 

6928  973 
in 
974 

0  975 
(*Lefttoright replacements: ctpairs = [...,(vi,ti),...]. 
976 
Instantiates distinct Vars by terms of same type. 

8129
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8066
diff
changeset

977 
No longer normalizes the new theorem! *) 
1529  978 
fun instantiate ([], []) th = th 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

979 
 instantiate (vcTs,ctpairs) (th as Thm{sign_ref,der,maxidx,hyps,shyps,tpairs=dpairs,prop}) = 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

980 
let val (newsign_ref,tpairs) = foldr add_ctpair (ctpairs, (sign_ref,[])); 
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

981 
val (newsign_ref,vTs) = foldr add_ctyp (vcTs, (newsign_ref,[])); 
14828  982 
fun subst t = 
983 
subst_atomic tpairs (Sign.inst_term_tvars (Sign.deref newsign_ref) vTs t); 

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

984 
val newprop = subst prop; 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

985 
val newdpairs = map (pairself subst) dpairs; 
1220  986 
val newth = 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

987 
(Thm{sign_ref = newsign_ref, 
11518  988 
der = Pt.infer_derivs' (Pt.instantiate vTs tpairs) der, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

989 
maxidx = maxidx_of_terms (newprop :: 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

990 
terms_of_tpairs newdpairs), 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

991 
shyps = add_insts_sorts ((vTs, tpairs), shyps), 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

993 
tpairs = newdpairs, 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

994 
prop = newprop}) 
250  995 
in if not(instl_ok(map #1 tpairs)) 
193  996 
then raise THM("instantiate: variables not distinct", 0, [th]) 
997 
else if not(null(findrep(map #1 vTs))) 

998 
then raise THM("instantiate: type variables not distinct", 0, [th]) 

8291  999 
else nodup_vars newth "instantiate" 
0  1000 
end 
6928  1001 
handle TERM _ => raise THM("instantiate: incompatible signatures", 0, [th]) 
1002 
 TYPE (msg, _, _) => raise THM (msg, 0, [th]); 

1003 

1004 
end; 

1005 

0  1006 

1007 
(*The trivial implication A==>A, justified by assume and forall rules. 

1008 
A can contain Vars, not so for assume! *) 

250  1009 
fun trivial ct : thm = 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

1010 
let val Cterm {sign_ref, t=A, T, maxidx} = ct 
250  1011 
in if T<>propT then 
1012 
raise THM("trivial: the term must have type prop", 0, []) 

1238  1013 
else fix_shyps [] [] 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

1014 
(Thm{sign_ref = sign_ref, 
11518  1015 
der = Pt.infer_derivs' I (false, Pt.AbsP ("H", None, Pt.PBound 0)), 
2386  1016 
maxidx = maxidx, 
1017 
shyps = [], 

1018 
hyps = [], 

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

1019 
tpairs = [], 
2386  1020 
prop = implies$A$A}) 
0  1021 
end; 
1022 

1503  1023 
(*Axiomscheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" *) 
6368  1024 
fun class_triv sign c = 
1025 
let val Cterm {sign_ref, t, maxidx, ...} = 

1026 
cterm_of sign (Logic.mk_inclass (TVar (("'a", 0), [c]), c)) 

1027 
handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []); 

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

1028 
in 
1238  1029 
fix_shyps [] [] 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

1030 
(Thm {sign_ref = sign_ref, 
11518  1031 
der = Pt.infer_derivs' I 
1032 
(false, Pt.PAxm ("ProtoPure.class_triv:" ^ c, t, Some [])), 

2386  1033 
maxidx = maxidx, 
1034 
shyps = [], 

1035 
hyps = [], 

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

1036 
tpairs = [], 
2386  1037 
prop = t}) 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

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

1039 

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

1040 

6786  1041 
(* Replace all TFrees not fixed or in the hyps by new TVars *) 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1042 
fun varifyT' fixed (Thm{sign_ref,der,maxidx,shyps,hyps,tpairs,prop}) = 
12500  1043 
let 
1044 
val tfrees = foldr add_term_tfree_names (hyps, fixed); 

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

1045 
val prop1 = attach_tpairs tpairs prop; 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1046 
val (prop2, al) = Type.varify (prop1, tfrees); 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1047 
val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2) 
1634  1048 
in let val thm = (*no fix_shyps*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

1049 
Thm{sign_ref = sign_ref, 
11518  1050 
der = Pt.infer_derivs' (Pt.varify_proof prop tfrees) der, 
2386  1051 
maxidx = Int.max(0,maxidx), 
1052 
shyps = shyps, 

1053 
hyps = hyps, 

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

1054 
tpairs = rev (map Logic.dest_equals ts), 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1055 
prop = prop3} 
12500  1056 
in (nodup_vars thm "varifyT", al) end 
8291  1057 
(* this nodup_vars check can be removed if thms are guaranteed not to contain 
1058 
duplicate TVars with different sorts *) 

0  1059 
end; 
1060 

12500  1061 
val varifyT = #1 o varifyT' []; 
6786  1062 

0  1063 
(* Replace all TVars by new TFrees *) 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1064 
fun freezeT(Thm{sign_ref,der,maxidx,shyps,hyps,tpairs,prop}) = 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

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

1066 
val prop1 = attach_tpairs tpairs prop; 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1067 
val (prop2, _) = Type.freeze_thaw prop1; 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1068 
val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2) 
1238  1069 
in (*no fix_shyps*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

1070 
Thm{sign_ref = sign_ref, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1071 
der = Pt.infer_derivs' (Pt.freezeT prop1) der, 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1072 
maxidx = maxidx_of_term prop2, 
2386  1073 
shyps = shyps, 
1074 
hyps = hyps, 

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

1075 
tpairs = rev (map Logic.dest_equals ts), 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1076 
prop = prop3} 
1220  1077 
end; 
0  1078 

1079 

1080 
(*** Inference rules for tactics ***) 

1081 

1082 
(*Destruct proof state into constraints, other goals, goal(i), rest *) 

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

1083 
fun dest_state (state as Thm{prop,tpairs,...}, i) = 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1084 
(case Logic.strip_prems(i, [], prop) of 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1085 
(B::rBs, C) => (tpairs, rev rBs, B, C) 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1086 
 _ => raise THM("dest_state", i, [state])) 
0  1087 
handle TERM _ => raise THM("dest_state", i, [state]); 
1088 

309  1089 
(*Increment variables and parameters of orule as required for 
0  1090 
resolution with goal i of state. *) 
1091 
fun lift_rule (state, i) orule = 

3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

1092 
let val Thm{shyps=sshyps, prop=sprop, maxidx=smax, sign_ref=ssign_ref,...} = state 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1093 
val (Bi::_, _) = Logic.strip_prems(i, [], sprop) 
1529  1094 
handle TERM _ => raise THM("lift_rule", i, [orule,state]) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

1095 
val ct_Bi = Cterm {sign_ref=ssign_ref, maxidx=smax, T=propT, t=Bi} 
1529  1096 
val (lift_abs,lift_all) = Logic.lift_fns(Bi,smax+1) 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1097 
val (Thm{sign_ref, der, maxidx,shyps,hyps,tpairs,prop}) = orule 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1098 
val (As, B) = Logic.strip_horn prop 
1238  1099 
in (*no fix_shyps*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

1100 
Thm{sign_ref = merge_thm_sgs(state,orule), 
11518  1101 
der = Pt.infer_derivs' (Pt.lift_proof Bi (smax+1) prop) der, 
2386  1102 
maxidx = maxidx+smax+1, 
14791  1103 
shyps = Sorts.union_sort(sshyps,shyps), 
1104 
hyps = hyps, 

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

1105 
tpairs = map (pairself lift_abs) tpairs, 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1106 
prop = Logic.list_implies (map lift_all As, lift_all B)} 
0  1107 
end; 
1108 

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

1109 
fun incr_indexes i (thm as Thm {sign_ref, der, maxidx, shyps, hyps, tpairs, prop}) = 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

1110 
if i < 0 then raise THM ("negative increment", 0, [thm]) else 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

1111 
if i = 0 then thm else 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

1112 
Thm {sign_ref = sign_ref, 
11518  1113 
der = Pt.infer_derivs' (Pt.map_proof_terms 
1114 
(Logic.incr_indexes ([], i)) (incr_tvar i)) der, 

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

1115 
maxidx = maxidx + i, 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

1116 
shyps = shyps, 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

1118 
tpairs = map (pairself (Logic.incr_indexes ([], i))) tpairs, 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

1119 
prop = Logic.incr_indexes ([], i) prop}; 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

1120 

0  1121 
(*Solve subgoal Bi of proof state B1...Bn/C by assumption. *) 
1122 
fun assumption i state = 

3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

1123 
let val Thm{sign_ref,der,maxidx,hyps,prop,...} = state; 
0  1124 
val (tpairs, Bs, Bi, C) = dest_state(state,i) 
11518  1125 
fun newth n (env as Envir.Envir{maxidx, ...}, tpairs) = 
1220  1126 
fix_shyps [state] (env_codT env) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

1127 
(Thm{sign_ref = sign_ref, 
11518  1128 
der = Pt.infer_derivs' 
1129 
((if Envir.is_empty env then I else (Pt.norm_proof' env)) o 

1130 
Pt.assumption_proof Bs Bi n) der, 

2386  1131 
maxidx = maxidx, 
1132 
shyps = [], 

1133 
hyps = hyps, 

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

1134 
tpairs = if Envir.is_empty env then tpairs else 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1135 
map (pairself (Envir.norm_term env)) tpairs, 
2386  1136 
prop = 
1137 
if Envir.is_empty env then (*avoid wasted normalizations*) 

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

1138 
Logic.list_implies (Bs, C) 
2386  1139 
else (*normalize the new rule fully*) 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1140 
Envir.norm_term env (Logic.list_implies (Bs, C))}); 
11518  1141 
fun addprfs [] _ = Seq.empty 
1142 
 addprfs ((t,u)::apairs) n = Seq.make (fn()=> Seq.pull 

1143 
(Seq.mapp (newth n) 

3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

1144 
(Unify.unifiers(Sign.deref sign_ref,Envir.empty maxidx, (t,u)::tpairs)) 
11518  1145 
(addprfs apairs (n+1)))) 
1146 
in addprfs (Logic.assum_pairs Bi) 1 end; 

0  1147 

250  1148 
(*Solve subgoal Bi of proof state B1...Bn/C by assumption. 
0  1149 
Checks if Bi's conclusion is alphaconvertible to one of its assumptions*) 
1150 
fun eq_assumption i state = 

3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

1151 
let val Thm{sign_ref,der,maxidx,hyps,prop,...} = state; 
0  1152 
val (tpairs, Bs, Bi, C) = dest_state(state,i) 
11518  1153 
in (case find_index (op aconv) (Logic.assum_pairs Bi) of 
1154 
(~1) => raise THM("eq_assumption", 0, [state]) 

1155 
 n => fix_shyps [state] [] 

1156 
(Thm{sign_ref = sign_ref, 

1157 
der = Pt.infer_derivs' 

1158 
(Pt.assumption_proof Bs Bi (n+1)) der, 

1159 
maxidx = maxidx, 

1160 
shyps = [], 

1161 
hyps = hyps, 

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

1162 
tpairs = tpairs, 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1163 
prop = Logic.list_implies (Bs, C)})) 
0  1164 
end; 
1165 

1166 

2671  1167 
(*For rotate_tac: fast rotation of assumptions of subgoal i*) 
1168 
fun rotate_rule k i state = 

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

1169 
let val Thm{sign_ref,der,maxidx,hyps,prop,shyps,...} = state; 
2671  1170 
val (tpairs, Bs, Bi, C) = dest_state(state,i) 
8066
54d37e491ac2
SOUNDNESS BUG FIX for rotate_rule. The original code did not expect
paulson
parents:
7921
diff
changeset

1171 
val params = Term.strip_all_vars Bi 
54d37e491ac2
SOUNDNESS BUG FIX for rotate_rule. The original code did not expect
paulson
parents:
7921
diff
changeset

1172 
and rest = Term.strip_all_body Bi 
54d37e491ac2
SOUNDNESS BUG FIX for rotate_rule. The original code did not expect
paulson
parents:
7921
diff
changeset

1173 
val asms = Logic.strip_imp_prems rest 
54d37e491ac2
SOUNDNESS BUG FIX for rotate_rule. The original code did not expect
paulson
parents:
7921
diff
changeset

1174 
and concl = Logic.strip_imp_concl rest 
2671  1175 
val n = length asms 
11563  1176 
val m = if k<0 then n+k else k 
1177 
val Bi' = if 0=m orelse m=n then Bi 

2671  1178 
else if 0<m andalso m<n 
13629  1179 
then let val (ps,qs) = splitAt(m,asms) 
1180 
in list_all(params, Logic.list_implies(qs @ ps, concl)) 

1181 
end 

7248
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1182 
else raise THM("rotate_rule", k, [state]) 
7264  1183 
in (*no fix_shyps*) 
1184 
Thm{sign_ref = sign_ref, 

11563  1185 
der = Pt.infer_derivs' (Pt.rotate_proof Bs Bi m) der, 
2671  1186 
maxidx = maxidx, 
1187 
shyps = shyps, 

1188 
hyps = hyps, 

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

1189 
tpairs = tpairs, 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1190 
prop = Logic.list_implies (Bs @ [Bi'], C)} 
2671  1191 
end; 
1192 

1193 

7248
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1194 
(*Rotates a rule's premises to the left by k, leaving the first j premises 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1195 
unchanged. Does nothing if k=0 or if k equals nj, where n is the 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1196 
number of premises. Useful with etac and underlies tactic/defer_tac*) 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1197 
fun permute_prems j k rl = 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1198 
let val Thm{sign_ref,der,maxidx,hyps,tpairs,prop,shyps} = rl 
7248
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1199 
val prems = Logic.strip_imp_prems prop 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1200 
and concl = Logic.strip_imp_concl prop 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1201 
val moved_prems = List.drop(prems, j) 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1202 
and fixed_prems = List.take(prems, j) 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1203 
handle Subscript => raise THM("permute_prems:j", j, [rl]) 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1204 
val n_j = length moved_prems 
11563  1205 
val m = if k<0 then n_j + k else k 
1206 
val prop' = if 0 = m orelse m = n_j then prop 

7248
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1207 
else if 0<m andalso m<n_j 
13629  1208 
then let val (ps,qs) = splitAt(m,moved_prems) 
1209 
in Logic.list_implies(fixed_prems @ qs @ ps, concl) end 

7248
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1210 
else raise THM("permute_prems:k", k, [rl]) 
7264  1211 
in (*no fix_shyps*) 
1212 
Thm{sign_ref = sign_ref, 

11563  1213 
der = Pt.infer_derivs' (Pt.permute_prems_prf prems j m) der, 
7248
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1214 
maxidx = maxidx, 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1215 
shyps = shyps, 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

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

1217 
tpairs = tpairs, 
11563  1218 
prop = prop'} 
7248
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1219 
end; 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1220 

322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1221 

0  1222 
(** User renaming of parameters in a subgoal **) 
1223 

1224 
(*Calls error rather than raising an exception because it is intended 

1225 
for toplevel use  exception handling would not make sense here. 

1226 
The names in cs, if distinct, are used for the innermost parameters; 

1227 
preceding parameters may be renamed to make all params distinct.*) 

1228 
fun rename_params_rule (cs, i) state = 

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

1229 
let val Thm{sign_ref,der,maxidx,hyps,shyps,...} = state 
0  1230 
val (tpairs, Bs, Bi, C) = dest_state(state,i) 
1231 
val iparams = map #1 (Logic.strip_params Bi) 

1232 
val short = length iparams  length cs 

250  1233 
val newnames = 
1234 
if short<0 then error"More names than abstractions!" 

1235 
else variantlist(take (short,iparams), cs) @ cs 

3037
99ed078e6ae7
rename_params_rule used to check if the new name clashed with a free name in
nipkow
parents:
3012
diff
changeset

1236 
val freenames = map (#1 o dest_Free) (term_frees Bi) 
0  1237 
val newBi = Logic.list_rename_params (newnames, Bi) 
250  1238 
in 
0  1239 
case findrep cs of 
3565
c64410e701fb
Now rename_params_rule merely issues warningsand does nothingif the
paulson
parents:
3558
diff
changeset

1240 
c::_ => (warning ("Can't rename. Bound variables not distinct: " ^ c); 
c64410e701fb
Now rename_params_rule merely issues warningsand does nothingif the
paulson
parents:
3558
diff
changeset

1241 
state) 
1576
af8f43f742a0
Added some optimized versions of functions dealing with sets
berghofe
parents:
1569
diff
changeset

1242 
 [] => (case cs inter_string freenames of 
3565
c64410e701fb
Now rename_params_rule merely issues warningsand does nothingif the
paulson
parents:
3558
diff
changeset

1243 
a::_ => (warning ("Can't rename. Bound/Free variable clash: " ^ a); 
c64410e701fb
Now rename_params_rule merely issues warningsand does nothingif the
paulson
parents:
3558
diff
changeset

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

1245 
 [] => Thm{sign_ref = sign_ref, 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1246 
der = der, 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1247 
maxidx = maxidx, 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1248 
shyps = shyps, 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1249 
hyps = hyps, 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1250 
tpairs = tpairs, 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1251 
prop = Logic.list_implies (Bs @ [newBi], C)}) 
0  1252 
end; 
1253 

12982  1254 

0  1255 
(*** Preservation of bound variable names ***) 
1256 

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

1257 
fun rename_boundvars pat obj (thm as Thm {sign_ref, der, maxidx, hyps, shyps, tpairs, prop}) = 
12982  1258 
(case Term.rename_abs pat obj prop of 
1259 
None => thm 

1260 
 Some prop' => Thm 

1261 
{sign_ref = sign_ref, 

1262 
der = der, 

1263 
maxidx = maxidx, 

1264 
hyps = hyps, 

1265 
shyps = shyps, 

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

1266 
tpairs = tpairs, 
12982  1267 
prop = prop'}); 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

1268 

0  1269 

250  1270 
(* strip_apply f A(,B) strips off all assumptions/parameters from A 
0  1271 
introduced by lifting over B, and applies f to remaining part of A*) 
1272 
fun strip_apply f = 

1273 
let fun strip(Const("==>",_)$ A1 $ B1, 

250  1274 
Const("==>",_)$ _ $ B2) = implies $ A1 $ strip(B1,B2) 
1275 
 strip((c as Const("all",_)) $ Abs(a,T,t1), 

1276 
Const("all",_) $ Abs(_,_,t2)) = c$Abs(a,T,strip(t1,t2)) 

1277 
 strip(A,_) = f A 

0  1278 
in strip end; 
1279 

1280 
(*Use the alist to rename all bound variables and some unknowns in a term 

1281 
dpairs = current disagreement pairs; tpairs = permanent ones (flexflex); 

1282 
Preserves unknowns in tpairs and on lhs of dpairs. *) 

1283 
fun rename_bvs([],_,_,_) = I 

1284 
 rename_bvs(al,dpairs,tpairs,B) = 

250  1285 
let val vars = foldr add_term_vars 
1286 
(map fst dpairs @ map fst tpairs @ map snd tpairs, []) 

1287 
(*unknowns appearing elsewhere be preserved!*) 

1288 
val vids = map (#1 o #1 o dest_Var) vars; 

1289 
fun rename(t as Var((x,i),T)) = 

1290 
(case assoc(al,x) of 

1576
af8f43f742a0
Added some optimized versions of functions dealing with sets
berghofe
parents:
1569
diff
changeset

1291 
Some(y) => if x mem_string vids orelse y mem_string vids then t 
250  1292 
else Var((y,i),T) 
1293 
 None=> t) 

0  1294 
 rename(Abs(x,T,t)) = 
9721  1295 
Abs(if_none(assoc_string(al,x)) x, T, rename t) 
0  1296 
 rename(f$t) = rename f $ rename t 
1297 
 rename(t) = t; 

250  1298 
fun strip_ren Ai = strip_apply rename (Ai,B) 
0  1299 
in strip_ren end; 
1300 

1301 
(*Function to rename bounds/unknowns in the argument, lifted over B*) 

1302 
fun rename_bvars(dpairs, tpairs, B) = 

12982  1303 
rename_bvs(foldr Term.match_bvars (dpairs,[]), dpairs, tpairs, B); 
0  1304 

1305 

1306 
(*** RESOLUTION ***) 

1307 

721
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1308 
(** Lifting optimizations **) 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1309 

0  1310 
(*strip off pairs of assumptions/parameters in parallel  they are 
1311 
identical because of lifting*) 

250  1312 
fun strip_assums2 (Const("==>", _) $ _ $ B1, 
1313 
Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2) 

0  1314 
 strip_assums2 (Const("all",_)$Abs(a,T,t1), 
250  1315 
Const("all",_)$Abs(_,_,t2)) = 
0  1316 
let val (B1,B2) = strip_assums2 (t1,t2) 
1317 
in (Abs(a,T,B1), Abs(a,T,B2)) end 

1318 
 strip_assums2 BB = BB; 

1319 

1320 

721
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1321 
(*Faster normalization: skip assumptions that were lifted over*) 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1322 
fun norm_term_skip env 0 t = Envir.norm_term env t 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1323 
 norm_term_skip env n (Const("all",_)$Abs(a,T,t)) = 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1324 
let val Envir.Envir{iTs, ...} = env 
8407
d522ad1809e9
Envir now uses Vartab instead of association lists.
berghofe
parents:
8299
diff
changeset

1325 
val T' = typ_subst_TVars_Vartab iTs T 
1238  1326 
(*Must instantiate types of parameters because they are flattened; 
721
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1327 
this could be a NEW parameter*) 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1328 
in all T' $ Abs(a, T', norm_term_skip env n t) end 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1329 
 norm_term_skip env n (Const("==>", _) $ A $ B) = 
1238  1330 
implies $ A $ norm_term_skip env (n1) B 
721
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
