author  berghofe 
Fri, 31 Aug 2001 16:13:00 +0200  
changeset 11518  5f2616a1c10a 
parent 10767  8fa4aafa7314 
child 11563  e172cbed431d 
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, 
45 
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, 
48 
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 
4254  53 
val transfer_sg : Sign.sg > thm > thm 
3895  54 
val transfer : theory > thm > thm 
1238  55 
val tpairs_of : thm > (term * term) list 
56 
val prems_of : thm > term list 

57 
val nprems_of : thm > int 

58 
val concl_of : thm > term 

59 
val cprop_of : thm > cterm 

60 
val extra_shyps : thm > sort list 

61 
val strip_shyps : thm > thm 

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

67 
(*meta rules*) 

1238  68 
val assume : cterm > thm 
1416  69 
val compress : thm > thm 
1238  70 
val implies_intr : cterm > thm > thm 
71 
val implies_elim : thm > thm > thm 

72 
val forall_intr : cterm > thm > thm 

73 
val forall_elim : cterm > thm > thm 

74 
val reflexive : cterm > thm 

75 
val symmetric : thm > thm 

76 
val transitive : thm > thm > thm 

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

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

78 
val eta_conversion : cterm > thm 
1238  79 
val abstract_rule : string > cterm > thm > thm 
80 
val combination : thm > thm > thm 

81 
val equal_intr : thm > thm > thm 

82 
val equal_elim : thm > thm > thm 

83 
val implies_intr_hyps : thm > thm 

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

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

95 
val incr_indexes : int > thm > thm 
4270  96 
val assumption : int > thm > thm Seq.seq 
1238  97 
val eq_assumption : int > thm > thm 
2671  98 
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

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

6089  108 
signature THM = 
109 
sig 

110 
include BASIC_THM 

10767
8fa4aafa7314
Thm: dest_comb, dest_abs, capply, cabs no longer global;
wenzelm
parents:
10486
diff
changeset

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

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

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

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

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

120 
val get_name_tags : thm > string * tag list 

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

122 
val name_of_thm : thm > string 

123 
val tags_of_thm : thm > tag list 

124 
val name_thm : string * thm > thm 

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

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

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

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

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

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

130 
val cterm_incr_indexes : int > cterm > cterm 
6089  131 
end; 
132 

3550  133 
structure Thm: THM = 
0  134 
struct 
250  135 

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

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

137 

250  138 
(** certified types **) 
139 

140 
(*certified typs under a signature*) 

141 

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

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

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

144 
fun rep_ctyp (Ctyp {sign_ref, T}) = {sign = Sign.deref sign_ref, T = T}; 
250  145 
fun typ_of (Ctyp {T, ...}) = T; 
146 

147 
fun ctyp_of sign T = 

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

148 
Ctyp {sign_ref = Sign.self_ref sign, T = Sign.certify_typ sign T}; 
250  149 

150 
fun read_ctyp sign s = 

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

151 
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

152 

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

153 

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

154 

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

156 

250  157 
(*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

158 

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

159 
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

160 

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

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

162 
{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

163 

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

166 
maxidx = maxidx}; 

167 

9461  168 
fun sign_of_cterm (Cterm {sign_ref, ...}) = Sign.deref sign_ref; 
169 

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

171 

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

172 
fun ctyp_of_term (Cterm {sign_ref, T, ...}) = Ctyp {sign_ref = sign_ref, T = T}; 
2671  173 

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

176 
let val (t, T, maxidx) = Sign.certify_term sign tm 

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

177 
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

178 
end; 
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 cterm_fun f (Cterm {sign_ref, t, ...}) = cterm_of (Sign.deref sign_ref) (f t); 
250  181 

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

182 

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

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

184 

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

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

186 
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

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

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

189 
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

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

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

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

193 
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

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

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

196 

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

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

198 
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

199 
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

200 
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

201 
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

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

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

204 

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

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

208 
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

209 

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

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

211 
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

212 
(Cterm {t=x, sign_ref=sign_ref2, T, maxidx=maxidx2}) = 
8291  213 
if T = dty then 
214 
Cterm{t=Sign.nodup_vars (f$x), sign_ref=Sign.merge_refs(sign_ref1,sign_ref2), T=rty, 

215 
maxidx=Int.max(maxidx1, maxidx2)} 

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

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

217 
 capply _ _ = raise CTERM "capply: first arg is not a function" 
250  218 

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

219 
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

220 
(Cterm {t=t2, sign_ref=sign_ref2, T=T2, maxidx=maxidx2}) = 
8291  221 
Cterm {t=Sign.nodup_vars (absfree(a,ty,t2)), sign_ref=Sign.merge_refs(sign_ref1,sign_ref2), 
2147  222 
T = ty > T2, maxidx=Int.max(maxidx1, maxidx2)} 
1517  223 
 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

224 

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

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

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

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

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

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

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

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

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

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

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

235 
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

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

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

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

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

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

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

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

243 

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

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

245 
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

246 

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

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

248 
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

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

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

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

252 
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

253 

2509  254 

255 

574  256 
(** read cterms **) (*exception ERROR*) 
250  257 

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

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

259 
fun read_def_cterms (sign, types, sorts) used freeze sTs = 
250  260 
let 
8608  261 
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

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

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

266 

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

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

268 
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

269 
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

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

271 

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

272 
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

273 

250  274 

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

277 

2509  278 

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

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

280 

11518  281 
structure Pt = Proofterm; 
282 

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

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

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

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

288 
hyps: term list, (*hypotheses*) 
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

289 
prop: term}; (*conclusion*) 
0  290 

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

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

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

293 
shyps = shyps, hyps = hyps, prop = prop}; 
0  294 

1529  295 
(*Version of rep_thm returning cterms instead of terms*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

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

297 
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

298 
in {sign = Sign.deref sign_ref, der = der, maxidx = maxidx, shyps = shyps, 
1529  299 
hyps = map (ctermf ~1) hyps, 
300 
prop = ctermf maxidx prop} 

1517  301 
end; 
302 

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

303 
(*errors involving theorems*) 
0  304 
exception THM of string * int * thm list; 
305 

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

308 

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

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

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

312 

3994  313 
fun eq_thm (th1, th2) = 
314 
let 

11518  315 
val {sign = sg1, shyps = shyps1, hyps = hyps1, prop = prop1, ...} = 
9031  316 
rep_thm th1; 
11518  317 
val {sign = sg2, shyps = shyps2, hyps = hyps2, prop = prop2, ...} = 
9031  318 
rep_thm th2; 
3994  319 
in 
9031  320 
Sign.joinable (sg1, sg2) andalso 
3994  321 
eq_set_sort (shyps1, shyps2) andalso 
322 
aconvs (hyps1, hyps2) andalso 

323 
prop1 aconv prop2 

324 
end; 

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

325 

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

326 
fun sign_of_thm (Thm {sign_ref, ...}) = Sign.deref sign_ref; 
0  327 

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

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

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

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

331 
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

332 

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

333 
(*transfer thm to super theory (nondestructive)*) 
4254  334 
fun transfer_sg sign' thm = 
3895  335 
let 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

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

337 
val sign = Sign.deref sign_ref; 
3895  338 
in 
4254  339 
if Sign.eq_sg (sign, sign') then thm 
340 
else if Sign.subsig (sign, sign') then 

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

341 
Thm {sign_ref = Sign.self_ref sign', der = der, maxidx = maxidx, 
3895  342 
shyps = shyps, hyps = hyps, prop = prop} 
343 
else raise THM ("transfer: not a super theory", 0, [thm]) 

344 
end; 

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

345 

6390  346 
val transfer = transfer_sg o Theory.sign_of; 
4254  347 

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

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

349 
fun tpairs_of (Thm {prop, ...}) = #1 (Logic.strip_flexpairs prop); 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

350 

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

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

352 
fun prems_of (Thm {prop, ...}) = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

353 
Logic.strip_imp_prems (Logic.skip_flexpairs prop); 
0  354 

355 
(*counts premises in a rule*) 

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

356 
fun nprems_of (Thm {prop, ...}) = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

357 
Logic.count_prems (Logic.skip_flexpairs prop, 0); 
0  358 

8299  359 
fun major_prem_of thm = 
360 
(case prems_of thm of 

361 
prem :: _ => prem 

362 
 [] => raise THM ("major_prem_of: rule with no premises", 0, [thm])); 

363 

7534  364 
fun no_prems thm = nprems_of thm = 0; 
365 

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

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

367 
fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop; 
0  368 

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

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

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

371 
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

372 

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

373 

0  374 

1238  375 
(** sort contexts of theorems **) 
376 

377 
(* basic utils *) 

378 

2163  379 
(*accumulate sorts suppressing duplicates; these are coded low levelly 
1238  380 
to improve efficiency a bit*) 
381 

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

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

383 
 add_typ_sorts (TFree (_, S), Ss) = ins_sort(S,Ss) 
8b365a3a6ed1
Changed some mem, ins and union calls to be monomorphic
paulson
parents:
2163
diff
changeset

384 
 add_typ_sorts (TVar (_, S), Ss) = ins_sort(S,Ss) 
1238  385 
and add_typs_sorts ([], Ss) = Ss 
386 
 add_typs_sorts (T :: Ts, Ss) = add_typs_sorts (Ts, add_typ_sorts (T, Ss)); 

387 

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

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

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

391 
 add_term_sorts (Bound _, Ss) = Ss 

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

392 
 add_term_sorts (Abs (_,T,t), Ss) = add_term_sorts (t, add_typ_sorts (T,Ss)) 
1238  393 
 add_term_sorts (t $ u, Ss) = add_term_sorts (t, add_term_sorts (u, Ss)); 
394 

395 
fun add_terms_sorts ([], Ss) = Ss 

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

396 
 add_terms_sorts (t::ts, Ss) = add_terms_sorts (ts, add_term_sorts (t,Ss)); 
1238  397 

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

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

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

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

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

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

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

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

405 
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

406 

1238  407 
fun add_thm_sorts (Thm {hyps, prop, ...}, Ss) = 
408 
add_terms_sorts (hyps, add_term_sorts (prop, Ss)); 

409 

410 
fun add_thms_shyps ([], Ss) = Ss 

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

7642  412 
add_thms_shyps (ths, union_sort (shyps, Ss)); 
1238  413 

414 

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

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

7642  417 
Term.rems_sort (shyps, add_thm_sorts (th, [])); 
1238  418 

419 

420 
(* fix_shyps *) 

421 

7642  422 
fun all_sorts_nonempty sign_ref = is_some (Sign.univ_witness (Sign.deref sign_ref)); 
423 

1238  424 
(*preserve sort contexts of rule premises and substituted types*) 
7642  425 
fun fix_shyps thms Ts (thm as Thm {sign_ref, der, maxidx, hyps, prop, ...}) = 
426 
Thm 

427 
{sign_ref = sign_ref, 

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

429 
maxidx = maxidx, 

430 
shyps = 

431 
if all_sorts_nonempty sign_ref then [] 

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

433 
hyps = hyps, prop = prop} 

1238  434 

435 

7642  436 
(* strip_shyps *) 
1238  437 

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

440 
 strip_shyps (thm as Thm {sign_ref, der, maxidx, shyps, hyps, prop}) = 

441 
let 

442 
val sign = Sign.deref sign_ref; 

1238  443 

7642  444 
val present_sorts = add_thm_sorts (thm, []); 
445 
val extra_shyps = Term.rems_sort (shyps, present_sorts); 

446 
val witnessed_shyps = Sign.witness_sorts sign present_sorts extra_shyps; 

447 
in 

448 
Thm {sign_ref = sign_ref, der = der, maxidx = maxidx, 

449 
shyps = Term.rems_sort (shyps, map #2 witnessed_shyps), 

450 
hyps = hyps, prop = prop} 

451 
end; 

1238  452 

453 

454 

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

456 

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

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

459 
let 
4847  460 
val name = Sign.intern (Theory.sign_of theory) Theory.axiomK raw_name; 
461 

462 
fun get_ax [] = None 

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

466 
Some t => 

467 
Some (fix_shyps [] [] 

468 
(Thm {sign_ref = Sign.self_ref sign, 

11518  469 
der = Pt.infer_derivs' I 
470 
(false, Pt.axm_proof name t), 

4847  471 
maxidx = maxidx_of_term t, 
472 
shyps = [], 

473 
hyps = [], 

474 
prop = t})) 

475 
 None => get_ax thys) 

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

477 
in 
4847  478 
(case get_ax (theory :: Theory.ancestors_of theory) of 
479 
Some thm => thm 

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

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

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

482 

6368  483 
fun def_name name = name ^ "_def"; 
484 
fun get_def thy = get_axiom thy o def_name; 

4847  485 

1529  486 

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

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

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

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

491 

6089  492 

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

494 

11518  495 
fun get_name_tags (Thm {prop, der = (_, prf), ...}) = Pt.get_name_tags prop prf; 
4018  496 

11518  497 
fun put_name_tags x (Thm {sign_ref, der = (ora, prf), maxidx, shyps, hyps, prop}) = 
498 
Thm {sign_ref = sign_ref, 

499 
der = (ora, Pt.thm_proof (Sign.deref sign_ref) x hyps prop prf), 

500 
maxidx = maxidx, shyps = shyps, hyps = hyps, prop = prop}; 

6089  501 

502 
val name_of_thm = #1 o get_name_tags; 

503 
val tags_of_thm = #2 o get_name_tags; 

504 

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

0  506 

507 

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

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

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

511 
Thm {sign_ref = sign_ref, 
2386  512 
der = der, (*No derivation recorded!*) 
513 
maxidx = maxidx, 

514 
shyps = shyps, 

515 
hyps = map Term.compress_term hyps, 

516 
prop = Term.compress_term prop}; 

564  517 

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

518 

2509  519 

1529  520 
(*** Meta rules ***) 
0  521 

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

524 
recurrence.*) 

8291  525 
fun nodup_vars (thm as Thm{sign_ref, der, maxidx, shyps, hyps, prop}) s = 
8296  526 
Thm {sign_ref = sign_ref, 
2386  527 
der = der, 
528 
maxidx = maxidx_of_term prop, 

529 
shyps = shyps, 

530 
hyps = hyps, 

8296  531 
prop = Sign.nodup_vars prop} 
2147  532 
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

533 

8291  534 

1220  535 
(** 'primitive' rules **) 
536 

537 
(*discharge all assumptions t from ts*) 

0  538 
val disch = gen_rem (op aconv); 
539 

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

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

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

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

548 
else Thm{sign_ref = sign_ref, 
11518  549 
der = Pt.infer_derivs' I (false, Pt.Hyp prop), 
2386  550 
maxidx = ~1, 
551 
shyps = add_term_sorts(prop,[]), 

552 
hyps = [prop], 

553 
prop = prop} 

0  554 
end; 
555 

1220  556 
(*Implication introduction 
3529  557 
[A] 
558 
: 

559 
B 

1220  560 
 
561 
A ==> B 

562 
*) 

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

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

564 
let val Cterm {sign_ref=sign_refA, t=A, T, maxidx=maxidxA} = cA 
0  565 
in if T<>propT then 
250  566 
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

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

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

571 
shyps = add_term_sorts (A, shyps), 
2386  572 
hyps = disch(hyps,A), 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

576 
end; 

577 

1529  578 

1220  579 
(*Implication elimination 
580 
A ==> B A 

581 
 

582 
B 

583 
*) 

0  584 
fun implies_elim thAB thA : thm = 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

585 
let val Thm{maxidx=maxA, der=derA, hyps=hypsA, shyps=shypsA, prop=propA, ...} = thA 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

586 
and Thm{der, maxidx, hyps, shyps, prop, ...} = thAB; 
250  587 
fun err(a) = raise THM("implies_elim: "^a, 0, [thAB,thA]) 
0  588 
in case prop of 
250  589 
imp$A$B => 
590 
if imp=implies andalso A aconv propA 

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

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

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

594 
maxidx = Int.max(maxA,maxidx), 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

595 
shyps = union_sort (shypsA, shyps), 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

596 
hyps = union_term(hypsA,hyps), (*dups suppressed*) 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

597 
prop = B} 
250  598 
else err("major premise") 
599 
 _ => err("major premise") 

0  600 
end; 
250  601 

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

604 
 

605 
!!x.A 

606 
*) 

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

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

608 
let val x = term_of cx; 
1238  609 
fun result(a,T) = fix_shyps [th] [] 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

610 
(Thm{sign_ref = sign_ref, 
11518  611 
der = Pt.infer_derivs' (Pt.forall_intr_proof x a) der, 
2386  612 
maxidx = maxidx, 
613 
shyps = [], 

614 
hyps = hyps, 

615 
prop = all(T) $ Abs(a, T, abstract_over (x,prop))}) 

0  616 
in case x of 
250  617 
Free(a,T) => 
618 
if exists (apl(x, Logic.occs)) hyps 

619 
then raise THM("forall_intr: variable free in assumptions", 0, [th]) 

620 
else result(a,T) 

0  621 
 Var((a,_),T) => result(a,T) 
622 
 _ => raise THM("forall_intr: not a variable", 0, [th]) 

623 
end; 

624 

1220  625 
(*Forall elimination 
626 
!!x.A 

627 
 

628 
A[t/x] 

629 
*) 

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

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

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

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

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

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

637 
(Thm{sign_ref= Sign.merge_refs(sign_ref,sign_reft), 
11518  638 
der = Pt.infer_derivs' (Pt.%% o rpair (Some t)) der, 
2386  639 
maxidx = Int.max(maxidx, maxt), 
640 
shyps = [], 

641 
hyps = hyps, 

642 
prop = betapply(A,t)}) 

643 
in if maxt >= 0 andalso maxidx >= 0 

8291  644 
then nodup_vars thm "forall_elim" 
2386  645 
else thm (*no new Vars: no expensive check!*) 
646 
end 

2147  647 
 _ => raise THM("forall_elim: not quantified", 0, [th]) 
0  648 
end 
649 
handle TERM _ => 

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

652 

1220  653 
(* Equality *) 
0  654 

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

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

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

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

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

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

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

663 
prop = Logic.mk_equals(t,t)} 
0  664 
end; 
665 

666 
(*The symmetry rule 

1220  667 
t==u 
668 
 

669 
u==t 

670 
*) 

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

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

675 
Thm{sign_ref = sign_ref, 
11518  676 
der = Pt.infer_derivs' Pt.symmetric der, 
2386  677 
maxidx = maxidx, 
678 
shyps = shyps, 

679 
hyps = hyps, 

680 
prop = eq$u$t} 

0  681 
 _ => raise THM("symmetric", 0, [th]); 
682 

683 
(*The transitive rule 

1220  684 
t1==u u==t2 
685 
 

686 
t1==t2 

687 
*) 

0  688 
fun transitive th1 th2 = 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

689 
let val Thm{der=der1, maxidx=max1, hyps=hyps1, shyps=shyps1, prop=prop1,...} = th1 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

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

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

696 
Thm{sign_ref= merge_thm_sgs(th1,th2), 
11518  697 
der = Pt.infer_derivs (Pt.transitive u T) der1 der2, 
2147  698 
maxidx = Int.max(max1,max2), 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

699 
shyps = union_sort (shyps1, shyps2), 
2386  700 
hyps = union_term(hyps1,hyps2), 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

701 
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

702 
in if max1 >= 0 andalso max2 >= 0 
8291  703 
then nodup_vars thm "transitive" 
2147  704 
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

705 
end 
0  706 
 _ => err"premises" 
707 
end; 

708 

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

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

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

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

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

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

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

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

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

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

719 
hyps = [], 
10486  720 
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

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

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

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

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

725 

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

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

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

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

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

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

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

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

734 
prop = Logic.mk_equals (t, Pattern.eta_contract t)} 
0  735 
end; 
736 

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

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

1220  739 
t == u 
740 
 

741 
%x.t == %x.u 

742 
*) 

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

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

744 
let val x = term_of cx; 
250  745 
val (t,u) = Logic.dest_equals prop 
746 
handle TERM _ => 

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

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

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

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

752 
shyps = add_typ_sorts (T, shyps), 
2386  753 
hyps = hyps, 
754 
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

755 
Abs(a, T, abstract_over (x,u)))} 
0  756 
in case x of 
250  757 
Free(_,T) => 
758 
if exists (apl(x, Logic.occs)) hyps 

759 
then raise THM("abstract_rule: variable free in assumptions", 0, [th]) 

760 
else result T 

0  761 
 Var(_,T) => result T 
762 
 _ => raise THM("abstract_rule: not a variable", 0, [th]) 

763 
end; 

764 

765 
(*The combination rule 

3529  766 
f == g t == u 
767 
 

768 
f(t) == g(u) 

1220  769 
*) 
0  770 
fun combination th1 th2 = 
1529  771 
let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1, 
2386  772 
prop=prop1,...} = th1 
1529  773 
and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, 
2386  774 
prop=prop2,...} = th2 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

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

778 
if T1 <> tT then 
2386  779 
raise THM("combination: types", 0, [th1,th2]) 
780 
else () 

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

782 
[th1,th2])) 

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

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

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

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

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

788 
Thm{sign_ref = merge_thm_sgs(th1,th2), 
11518  789 
der = Pt.infer_derivs 
790 
(Pt.combination f g t u fT) der1 der2, 

2386  791 
maxidx = Int.max(max1,max2), 
792 
shyps = union_sort(shyps1,shyps2), 

793 
hyps = union_term(hyps1,hyps2), 

794 
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

795 
in if max1 >= 0 andalso max2 >= 0 
8291  796 
then nodup_vars thm "combination" 
2386  797 
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

798 
end 
0  799 
 _ => raise THM("combination: premises", 0, [th1,th2]) 
800 
end; 

801 

802 

803 
(* Equality introduction 

3529  804 
A ==> B B ==> A 
805 
 

806 
A == B 

1220  807 
*) 
0  808 
fun equal_intr th1 th2 = 
11518  809 
let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1, 
2386  810 
prop=prop1,...} = th1 
1529  811 
and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, 
2386  812 
prop=prop2,...} = th2; 
1529  813 
fun err(msg) = raise THM("equal_intr: "^msg, 0, [th1,th2]) 
814 
in case (prop1,prop2) of 

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

2386  816 
if A aconv A' andalso B aconv B' 
817 
then 

818 
(*no fix_shyps*) 

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

819 
Thm{sign_ref = merge_thm_sgs(th1,th2), 
11518  820 
der = Pt.infer_derivs (Pt.equal_intr A B) der1 der2, 
2386  821 
maxidx = Int.max(max1,max2), 
822 
shyps = union_sort(shyps1,shyps2), 

823 
hyps = union_term(hyps1,hyps2), 

824 
prop = Logic.mk_equals(A,B)} 

825 
else err"not equal" 

1529  826 
 _ => err"premises" 
827 
end; 

828 

829 

830 
(*The equal propositions rule 

3529  831 
A == B A 
1529  832 
 
833 
B 

834 
*) 

835 
fun equal_elim th1 th2 = 

836 
let val Thm{der=der1, maxidx=max1, hyps=hyps1, prop=prop1,...} = th1 

837 
and Thm{der=der2, maxidx=max2, hyps=hyps2, prop=prop2,...} = th2; 

838 
fun err(msg) = raise THM("equal_elim: "^msg, 0, [th1,th2]) 

839 
in case prop1 of 

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

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

842 
fix_shyps [th1, th2] [] 

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

843 
(Thm{sign_ref= merge_thm_sgs(th1,th2), 
11518  844 
der = Pt.infer_derivs (Pt.equal_elim A B) der1 der2, 
2386  845 
maxidx = Int.max(max1,max2), 
846 
shyps = [], 

847 
hyps = union_term(hyps1,hyps2), 

848 
prop = B}) 

1529  849 
 _ => err"major premise" 
850 
end; 

0  851 

1220  852 

853 

0  854 
(**** Derived rules ****) 
855 

1503  856 
(*Discharge all hypotheses. Need not verify cterms or call fix_shyps. 
0  857 
Repeated hypotheses are discharged only once; fold cannot do this*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

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

860 
(Thm{sign_ref = sign_ref, 
11518  861 
der = Pt.infer_derivs' (Pt.implies_intr_proof A) der, 
2386  862 
maxidx = maxidx, 
863 
shyps = shyps, 

1529  864 
hyps = disch(As,A), 
2386  865 
prop = implies$A$prop}) 
0  866 
 implies_intr_hyps th = th; 
867 

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

250  869 
Instantiates the theorem and deletes trivial tpairs. 
0  870 
Resulting sequence may contain multiple elements if the tpairs are 
871 
not all flexflex. *) 

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

872 
fun flexflex_rule (th as Thm{sign_ref, der, maxidx, hyps, prop,...}) = 
250  873 
let fun newthm env = 
1529  874 
if Envir.is_empty env then th 
875 
else 

250  876 
let val (tpairs,horn) = 
877 
Logic.strip_flexpairs (Envir.norm_term env prop) 

878 
(*Remove trivial tpairs, of the form t=t*) 

879 
val distpairs = filter (not o op aconv) tpairs 

880 
val newprop = Logic.list_flexpairs(distpairs, horn) 

1220  881 
in fix_shyps [th] (env_codT env) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

882 
(Thm{sign_ref = sign_ref, 
11518  883 
der = Pt.infer_derivs' (Pt.norm_proof' env) der, 
2386  884 
maxidx = maxidx_of_term newprop, 
885 
shyps = [], 

886 
hyps = hyps, 

887 
prop = newprop}) 

250  888 
end; 
0  889 
val (tpairs,_) = Logic.strip_flexpairs prop 
4270  890 
in Seq.map newthm 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

891 
(Unify.smash_unifiers(Sign.deref sign_ref, Envir.empty maxidx, tpairs)) 
0  892 
end; 
893 

894 
(*Instantiation of Vars 

1220  895 
A 
896 
 

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

898 
*) 

0  899 

6928  900 
local 
901 

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

904 

6928  905 
fun prt_typing sg_ref t T = 
906 
let val sg = Sign.deref sg_ref in 

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

908 
end; 

909 

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

911 
fun add_ctpair ((ct,cu), (sign_ref,tpairs)) = 
6928  912 
let 
913 
val Cterm {sign_ref=sign_reft, t=t, T= T, ...} = ct 

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

915 
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

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

919 
Pretty.fbrk, prt_typing sign_ref_merged t T, 

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

0  921 
end; 
922 

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

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

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

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

6928  927 
in 
928 

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

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

931 
No longer normalizes the new theorem! *) 
1529  932 
fun instantiate ([], []) th = th 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

934 
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

935 
val (newsign_ref,vTs) = foldr add_ctyp (vcTs, (newsign_ref,[])); 
8129
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8066
diff
changeset

936 
val newprop = subst_atomic tpairs 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8066
diff
changeset

937 
(Type.inst_term_tvars 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8066
diff
changeset

938 
(Sign.tsig_of (Sign.deref newsign_ref),vTs) prop) 
1220  939 
val newth = 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

940 
(Thm{sign_ref = newsign_ref, 
11518  941 
der = Pt.infer_derivs' (Pt.instantiate vTs tpairs) der, 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

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

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

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

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

8291  950 
else nodup_vars newth "instantiate" 
0  951 
end 
6928  952 
handle TERM _ => raise THM("instantiate: incompatible signatures", 0, [th]) 
953 
 TYPE (msg, _, _) => raise THM (msg, 0, [th]); 

954 

955 
end; 

956 

0  957 

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

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

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

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

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

965 
(Thm{sign_ref = sign_ref, 
11518  966 
der = Pt.infer_derivs' I (false, Pt.AbsP ("H", None, Pt.PBound 0)), 
2386  967 
maxidx = maxidx, 
968 
shyps = [], 

969 
hyps = [], 

970 
prop = implies$A$A}) 

0  971 
end; 
972 

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

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

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

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

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

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

2386  983 
maxidx = maxidx, 
984 
shyps = [], 

985 
hyps = [], 

986 
prop = t}) 

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

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

988 

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

989 

6786  990 
(* Replace all TFrees not fixed or in the hyps by new TVars *) 
991 
fun varifyT' fixed (Thm{sign_ref,der,maxidx,shyps,hyps,prop}) = 

992 
let val tfrees = foldr add_term_tfree_names (hyps,fixed) 

1634  993 
in let val thm = (*no fix_shyps*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

994 
Thm{sign_ref = sign_ref, 
11518  995 
der = Pt.infer_derivs' (Pt.varify_proof prop tfrees) der, 
2386  996 
maxidx = Int.max(0,maxidx), 
997 
shyps = shyps, 

998 
hyps = hyps, 

1529  999 
prop = Type.varify(prop,tfrees)} 
8291  1000 
in nodup_vars thm "varifyT" end 
1001 
(* this nodup_vars check can be removed if thms are guaranteed not to contain 

1002 
duplicate TVars with different sorts *) 

0  1003 
end; 
1004 

6786  1005 
val varifyT = varifyT' []; 
1006 

0  1007 
(* Replace all TVars by new TFrees *) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

1008 
fun freezeT(Thm{sign_ref,der,maxidx,shyps,hyps,prop}) = 
3410  1009 
let val (prop',_) = Type.freeze_thaw prop 
1238  1010 
in (*no fix_shyps*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

1011 
Thm{sign_ref = sign_ref, 
11518  1012 
der = Pt.infer_derivs' (Pt.freezeT prop) der, 
2386  1013 
maxidx = maxidx_of_term prop', 
1014 
shyps = shyps, 

1015 
hyps = hyps, 

1529  1016 
prop = prop'} 
1220  1017 
end; 
0  1018 

1019 

1020 
(*** Inference rules for tactics ***) 

1021 

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

1023 
fun dest_state (state as Thm{prop,...}, i) = 

1024 
let val (tpairs,horn) = Logic.strip_flexpairs prop 

1025 
in case Logic.strip_prems(i, [], horn) of 

1026 
(B::rBs, C) => (tpairs, rev rBs, B, C) 

1027 
 _ => raise THM("dest_state", i, [state]) 

1028 
end 

1029 
handle TERM _ => raise THM("dest_state", i, [state]); 

1030 

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

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

1034 
let val Thm{shyps=sshyps, prop=sprop, maxidx=smax, sign_ref=ssign_ref,...} = state 
0  1035 
val (Bi::_, _) = Logic.strip_prems(i, [], Logic.skip_flexpairs sprop) 
1529  1036 
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

1037 
val ct_Bi = Cterm {sign_ref=ssign_ref, maxidx=smax, T=propT, t=Bi} 
1529  1038 
val (lift_abs,lift_all) = Logic.lift_fns(Bi,smax+1) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

1039 
val (Thm{sign_ref, der, maxidx,shyps,hyps,prop}) = orule 
0  1040 
val (tpairs,As,B) = Logic.strip_horn prop 
1238  1041 
in (*no fix_shyps*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

1042 
Thm{sign_ref = merge_thm_sgs(state,orule), 
11518  1043 
der = Pt.infer_derivs' (Pt.lift_proof Bi (smax+1) prop) der, 
2386  1044 
maxidx = maxidx+smax+1, 
2177
8b365a3a6ed1
Changed some mem, ins and union calls to be monomorphic
paulson
parents:
2163
diff
changeset

1045 
shyps=union_sort(sshyps,shyps), 
2386  1046 
hyps=hyps, 
1529  1047 
prop = Logic.rule_of (map (pairself lift_abs) tpairs, 
2386  1048 
map lift_all As, 
1049 
lift_all B)} 

0  1050 
end; 
1051 

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

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

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

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

1055 
Thm {sign_ref = sign_ref, 
11518  1056 
der = Pt.infer_derivs' (Pt.map_proof_terms 
1057 
(Logic.incr_indexes ([], i)) (incr_tvar i)) der, 

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

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

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

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

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

1062 

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

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

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

1069 
(Thm{sign_ref = sign_ref, 
11518  1070 
der = Pt.infer_derivs' 
1071 
((if Envir.is_empty env then I else (Pt.norm_proof' env)) o 

1072 
Pt.assumption_proof Bs Bi n) der, 

2386  1073 
maxidx = maxidx, 
1074 
shyps = [], 

1075 
hyps = hyps, 

1076 
prop = 

1077 
if Envir.is_empty env then (*avoid wasted normalizations*) 

1078 
Logic.rule_of (tpairs, Bs, C) 

1079 
else (*normalize the new rule fully*) 

1080 
Envir.norm_term env (Logic.rule_of (tpairs, Bs, C))}); 

11518  1081 
fun addprfs [] _ = Seq.empty 
1082 
 addprfs ((t,u)::apairs) n = Seq.make (fn()=> Seq.pull 

1083 
(Seq.mapp (newth n) 

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

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

0  1087 

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

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

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

1095 
 n => fix_shyps [state] [] 

1096 
(Thm{sign_ref = sign_ref, 

1097 
der = Pt.infer_derivs' 

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

1099 
maxidx = maxidx, 

1100 
shyps = [], 

1101 
hyps = hyps, 

1102 
prop = Logic.rule_of(tpairs, Bs, C)})) 

0  1103 
end; 
1104 

1105 

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

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

1108 
let val Thm{sign_ref,der,maxidx,hyps,prop,shyps} = state; 
2671  1109 
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

1110 
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

1111 
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

1112 
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

1113 
and concl = Logic.strip_imp_concl rest 
2671  1114 
val n = length asms 
1115 
fun rot m = if 0=m orelse m=n then Bi 

1116 
else if 0<m andalso m<n 

1117 
then list_all 

1118 
(params, 

1119 
Logic.list_implies(List.drop(asms, m) @ 

1120 
List.take(asms, m), 

1121 
concl)) 

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

1122 
else raise THM("rotate_rule", k, [state]) 
7264  1123 
in (*no fix_shyps*) 
1124 
Thm{sign_ref = sign_ref, 

11518  1125 
der = Pt.infer_derivs' 
1126 
(Pt.rotate_proof Bs Bi (if k<0 then n+k else k)) der, 

2671  1127 
maxidx = maxidx, 
1128 
shyps = shyps, 

1129 
hyps = hyps, 

1130 
prop = Logic.rule_of(tpairs, Bs@[rot (if k<0 then n+k else k)], C)} 

1131 
end; 

1132 

1133 

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

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

1135 
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

1136 
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

1137 
fun permute_prems j k rl = 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

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

1139 
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

1140 
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

1141 
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

1142 
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

1143 
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

1144 
val n_j = length moved_prems 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1145 
fun rot m = if 0 = m orelse m = n_j then prop 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1146 
else if 0<m andalso m<n_j 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1147 
then Logic.list_implies(fixed_prems @ 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1148 
List.drop(moved_prems, m) @ 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1149 
List.take(moved_prems, m), 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

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

1151 
else raise THM("permute_prems:k", k, [rl]) 
7264  1152 
in (*no fix_shyps*) 
1153 
Thm{sign_ref = sign_ref, 

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

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

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

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

1158 
prop = rot (if k<0 then n_j + k else k)} 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

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

1160 

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

1161 

0  1162 
(** User renaming of parameters in a subgoal **) 
1163 

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

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

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

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

1168 
fun rename_params_rule (cs, i) state = 

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

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

1172 
val short = length iparams  length cs 

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

1175 
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

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

1180 
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

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

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

1183 
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

1184 
state) 
1220  1185 
 [] => fix_shyps [state] [] 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

1186 
(Thm{sign_ref = sign_ref, 
11518  1187 
der = der, 
2386  1188 
maxidx = maxidx, 
1189 
shyps = [], 

1190 
hyps = hyps, 

1191 
prop = Logic.rule_of(tpairs, Bs@[newBi], C)})) 

0  1192 
end; 
1193 

1194 
(*** Preservation of bound variable names ***) 

1195 

250  1196 
(*Scan a pair of terms; while they are similar, 
0  1197 
accumulate corresponding bound vars in "al"*) 
1238  1198 
fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) = 
1195
686e3eb613b9
match_bvs no longer puts a name in the alist if it is null ("")
lcp
parents:
1160
diff
changeset

1199 
match_bvs(s, t, if x="" orelse y="" then al 
1238  1200 
else (x,y)::al) 
0  1201 
 match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al)) 
1202 
 match_bvs(_,_,al) = al; 

1203 

1204 
(* strip abstractions created by parameters *) 

1205 
fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al); 

1206 

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

1207 
fun rename_boundvars pat obj (thm as Thm {sign_ref,der,maxidx,hyps,shyps,prop}) = 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

1208 
let val ren = match_bvs (pat, obj, []) 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

1209 
fun renAbs (Abs (x, T, b)) = 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

1210 
Abs (if_none (assoc_string (ren, x)) x, T, renAbs b) 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

1211 
 renAbs (f $ t) = renAbs f $ renAbs t 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

1212 
 renAbs t = t 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

1213 
in if null ren then thm else Thm 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

1214 
{sign_ref = sign_ref, 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

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

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

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

1219 
prop = renAbs prop} 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

1221 

0  1222 

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

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

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

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

1230 
 strip(A,_) = f A 

0  1231 
in strip end; 
1232 

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

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

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

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

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

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

1240 
(*unknowns appearing elsewhere be preserved!*) 

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

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

1243 
(case assoc(al,x) of 

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

1244 
Some(y) => if x mem_string vids orelse y mem_string vids then t 
250  1245 
else Var((y,i),T) 
1246 
 None=> t) 

0  1247 
 rename(Abs(x,T,t)) = 
9721  1248 
Abs(if_none(assoc_string(al,x)) x, T, rename t) 
0  1249 
 rename(f$t) = rename f $ rename t 
1250 
 rename(t) = t; 

250  1251 
fun strip_ren Ai = strip_apply rename (Ai,B) 
0  1252 
in strip_ren end; 
1253 

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

1255 
fun rename_bvars(dpairs, tpairs, B) = 

250  1256 
rename_bvs(foldr match_bvars (dpairs,[]), dpairs, tpairs, B); 
0  1257 

1258 

1259 
(*** RESOLUTION ***) 

1260 

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

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

1262 

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

250  1265 
fun strip_assums2 (Const("==>", _) $ _ $ B1, 
1266 
Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2) 

0  1267 
 strip_assums2 (Const("all",_)$Abs(a,T,t1), 
250  1268 
Const("all",_)$Abs(_,_,t2)) = 
0  1269 
let val (B1,B2) = strip_assums2 (t1,t2) 
1270 
in (Abs(a,T,B1), Abs(a,T,B2)) end 

1271 
 strip_assums2 BB = BB; 

1272 

1273 

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

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

1275 
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

1276 
 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

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

1278 
val T' = typ_subst_TVars_Vartab iTs T 
1238  1279 
(*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

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

1281 
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

1282 
 norm_term_skip env n (Const("==>", _) $ A $ B) = 
1238  1283 
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
diff
changeset

1284 
 norm_term_skip env n t = error"norm_term_skip: too few assumptions??"; 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1285 

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

1286 

0  1287 
(*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C) 
250  1288 
Unifies B with Bi, replacing subgoal i (1 <= i <= n) 
0  1289 
If match then forbid instantiations in proof state 
1290 
If lifted then shorten the dpair using strip_assums2. 

1291 
If eres_flg then simultaneously proves A1 by assumption. 

250  1292 
nsubgoal is the number of new subgoals (written m above). 
0  1293 
Curried so that resolution calls dest_state only once. 
1294 
*) 

4270  1295 
local exception COMPOSE 
0  1296 
in 
250  1297 
fun bicompose_aux match (state, (stpairs, Bs, Bi, C), lifted) 
0  1298 
(eres_flg, orule, nsubgoal) = 
1529  1299 
let val Thm{der=sder, maxidx=smax, shyps=sshyps, hyps=shyps, ...} = state 
1300 
and Thm{der=rder, maxidx=rmax, shyps=rshyps, hyps=rhyps, 

2386  1301 
prop=rprop,...} = orule 
1529  1302 
(*How many hyps to skip over during normalization*) 
1238  1303 
and nlift = Logic.count_prems(strip_all_body Bi, 
1304 
if eres_flg then ~1 else 0) 

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

1305 
val sign_ref = merge_thm_sgs(state,orule); 
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

1306 
val sign = Sign.deref sign_ref; 
0  1307 
(** Add new theorem with prop = '[ Bs; As ] ==> C' to thq **) 
11518  1308 
fun addth A (As, oldAs, rder', n) ((env as Envir.Envir {maxidx, ...}, tpairs), thq) = 
250  1309 
let val normt = Envir.norm_term env; 
1310 
(*perform minimal copying here by examining env*) 

1311 
val normp = 

1312 
if Envir.is_empty env then (tpairs, Bs @ As, C) 

1313 
else 

1314 
let val ntps = map (pairself normt) tpairs 

2147  1315 
in if Envir.above (smax, env) then 
1238  1316 
(*no assignments in state; normalize the rule only*) 
1317 
if lifted 

1318 
then (ntps, Bs @ map (norm_term_skip env nlift) As, C) 

1319 
else (ntps, Bs @ map normt As, C) 

1529  1320 
else if match then raise COMPOSE 
250  1321 
else (*normalize the new rule fully*) 
1322 
(ntps, map normt (Bs @ As), normt C) 

1323 
end 

1258  1324 
val th = (*tuned fix_shyps*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

1325 
Thm{sign_ref = sign_ref, 
11518  1326 
der = Pt.infer_derivs 
1327 
((if Envir.is_empty env then I 

1328 
else if Envir.above (smax, env) then 

1329 
(fn f => fn der => f (Pt.norm_proof' env der)) 

1330 
else 

1331 
curry op oo (Pt.norm_proof' env)) 

1332 
(Pt.bicompose_proof Bs oldAs As A n)) rder' sder, 

2386  1333 
maxidx = maxidx, 
1334 
shyps = add_env_sorts (env, union_sort(rshyps,sshyps)), 

1335 
hyps = union_term(rhyps,shyps), 

1336 
prop = Logic.rule_of normp} 

11518  1337 
in Seq.cons(th, thq) end handle COMPOSE => thq; 
0  1338 
val (rtpairs,rhorn) = Logic.strip_flexpairs(rprop); 
1339 
val (rAs,B) = Logic.strip_prems(nsubgoal, [], rhorn) 

1340 
handle TERM _ => raise THM("bicompose: rule", 0, [orule,state]); 

1341 
(*Modify assumptions, deleting nth if n>0 for eresolution*) 

1342 
fun newAs(As0, n, dpairs, tpairs) = 

11518  1343 
let val (As1, rder') = 
1344 
if !Logic.auto_rename orelse not lifted then (As0, rder) 

1345 
else (map (rename_bvars(dpairs,tpairs,B)) As0, 

1346 
Pt.infer_derivs' (Pt.map_proof_terms 

1347 
(rename_bvars (dpairs, tpairs, Bound 0)) I) rder); 

1348 
in (map (Logic.flatten_params n) As1, As1, rder', n) 

250  1349 
handle TERM _ => 