author  paulson 
Wed, 18 Aug 1999 10:54:44 +0200  
changeset 7248  322151fe6f02 
parent 7070  893e5a8a8d46 
child 7264  d55cd903c93d 
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 
1529  7 
theorems, meta rules (including resolution and simplification). 
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} 
1238  24 
val term_of : cterm > term 
25 
val cterm_of : Sign.sg > term > cterm 

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

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

29 
val dest_comb : cterm > cterm * cterm 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

30 
val dest_abs : cterm > cterm * cterm 
1703
e22ad43bab5f
moved dest_cimplies to drule.ML; added adjust_maxidx
clasohm
parents:
1659
diff
changeset

31 
val adjust_maxidx : cterm > cterm 
1516
96286c4e32de
removed mk_prop; added capply; simplified dest_abs
clasohm
parents:
1503
diff
changeset

32 
val capply : cterm > cterm > cterm 
1517  33 
val cabs : cterm > cterm > cterm 
1238  34 
val read_def_cterm : 
1160  35 
Sign.sg * (indexname > typ option) * (indexname > sort option) > 
36 
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

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

38 
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

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

40 
> cterm list * (indexname * typ)list 
1160  41 

2671  42 
(*proof terms [must DUPLICATE declaration as a specification]*) 
1597
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

43 
datatype deriv_kind = MinDeriv  ThmDeriv  FullDeriv; 
6089  44 
type tag (* = string * string list *) 
2386  45 
val keep_derivs : deriv_kind ref 
1529  46 
datatype rule = 
2386  47 
MinProof 
4999  48 
 Oracle of string * Sign.sg * Object.T 
6089  49 
 Axiom of string * tag list 
50 
 Theorem of string * tag list 

2671  51 
 Assume of cterm 
52 
 Implies_intr of cterm 

1529  53 
 Implies_intr_shyps 
54 
 Implies_intr_hyps 

55 
 Implies_elim 

2671  56 
 Forall_intr of cterm 
57 
 Forall_elim of cterm 

58 
 Reflexive of cterm 

1529  59 
 Symmetric 
60 
 Transitive 

2671  61 
 Beta_conversion of cterm 
1529  62 
 Extensional 
2671  63 
 Abstract_rule of string * cterm 
1529  64 
 Combination 
65 
 Equal_intr 

66 
 Equal_elim 

2671  67 
 Trivial of cterm 
68 
 Lift_rule of cterm * int 

69 
 Assumption of int * Envir.env option 

70 
 Rotate_rule of int * int 

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

71 
 Permute_prems of int * int 
2671  72 
 Instantiate of (indexname * ctyp) list * (cterm * cterm) list 
73 
 Bicompose of bool * bool * int * int * Envir.env 

74 
 Flexflex_rule of Envir.env 

4182  75 
 Class_triv of class 
6786  76 
 VarifyT of string list 
1529  77 
 FreezeT 
2671  78 
 RewriteC of cterm 
79 
 CongC of cterm 

80 
 Rewrite_cterm of cterm 

81 
 Rename_params_rule of string list * int; 

6089  82 
type deriv (* = rule mtree *) 
1529  83 

1160  84 
(*meta theorems*) 
85 
type thm 

1529  86 
val rep_thm : thm > {sign: Sign.sg, der: deriv, maxidx: int, 
2386  87 
shyps: sort list, hyps: term list, 
88 
prop: term} 

1529  89 
val crep_thm : thm > {sign: Sign.sg, der: deriv, maxidx: int, 
2386  90 
shyps: sort list, hyps: cterm list, 
91 
prop: cterm} 

6089  92 
exception THM of string * int * thm list 
93 
type 'a attribute (* = 'a * thm > 'a * thm *) 

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

95 
val sign_of_thm : thm > Sign.sg 
4254  96 
val transfer_sg : Sign.sg > thm > thm 
3895  97 
val transfer : theory > thm > thm 
1238  98 
val tpairs_of : thm > (term * term) list 
99 
val prems_of : thm > term list 

100 
val nprems_of : thm > int 

101 
val concl_of : thm > term 

102 
val cprop_of : thm > cterm 

103 
val extra_shyps : thm > sort list 

3061  104 
val force_strip_shyps : bool ref (* FIXME tmp (since 1995/08/01) *) 
1238  105 
val strip_shyps : thm > thm 
106 
val implies_intr_shyps: thm > thm 

3812  107 
val get_axiom : theory > xstring > thm 
6368  108 
val def_name : string > string 
4847  109 
val get_def : theory > xstring > thm 
1238  110 
val axioms_of : theory > (string * thm) list 
1160  111 

112 
(*meta rules*) 

1238  113 
val assume : cterm > thm 
1416  114 
val compress : thm > thm 
1238  115 
val implies_intr : cterm > thm > thm 
116 
val implies_elim : thm > thm > thm 

117 
val forall_intr : cterm > thm > thm 

118 
val forall_elim : cterm > thm > thm 

119 
val reflexive : cterm > thm 

120 
val symmetric : thm > thm 

121 
val transitive : thm > thm > thm 

122 
val beta_conversion : cterm > thm 

123 
val extensional : thm > thm 

124 
val abstract_rule : string > cterm > thm > thm 

125 
val combination : thm > thm > thm 

126 
val equal_intr : thm > thm > thm 

127 
val equal_elim : thm > thm > thm 

128 
val implies_intr_hyps : thm > thm 

4270  129 
val flexflex_rule : thm > thm Seq.seq 
1238  130 
val instantiate : 
1160  131 
(indexname * ctyp) list * (cterm * cterm) list > thm > thm 
1238  132 
val trivial : cterm > thm 
6368  133 
val class_triv : Sign.sg > class > thm 
1238  134 
val varifyT : thm > thm 
6786  135 
val varifyT' : string list > thm > thm 
1238  136 
val freezeT : thm > thm 
137 
val dest_state : thm * int > 

1160  138 
(term * term) list * term list * term * term 
1238  139 
val lift_rule : (thm * int) > thm > thm 
4270  140 
val assumption : int > thm > thm Seq.seq 
1238  141 
val eq_assumption : int > thm > thm 
2671  142 
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

143 
val permute_prems : int > int > thm > thm 
1160  144 
val rename_params_rule: string list * int > thm > thm 
1238  145 
val bicompose : bool > bool * thm * int > 
4270  146 
int > thm > thm Seq.seq 
1238  147 
val biresolution : bool > (bool * thm) list > 
4270  148 
int > thm > thm Seq.seq 
1160  149 

150 
(*meta simplification*) 

3550  151 
exception SIMPLIFIER of string * thm 
1160  152 
type meta_simpset 
3550  153 
val dest_mss : meta_simpset > 
154 
{simps: thm list, congs: thm list, procs: (string * cterm list) list} 

1238  155 
val empty_mss : meta_simpset 
6899  156 
val clear_mss : meta_simpset > meta_simpset 
3550  157 
val merge_mss : meta_simpset * meta_simpset > meta_simpset 
1238  158 
val add_simps : meta_simpset * thm list > meta_simpset 
159 
val del_simps : meta_simpset * thm list > meta_simpset 

160 
val mss_of : thm list > meta_simpset 

161 
val add_congs : meta_simpset * thm list > meta_simpset 

2626  162 
val del_congs : meta_simpset * thm list > meta_simpset 
2509  163 
val add_simprocs : meta_simpset * 
3577
9715b6e3ec5f
added prems argument to simplification procedures;
wenzelm
parents:
3565
diff
changeset

164 
(string * cterm list * (Sign.sg > thm list > term > thm option) * stamp) list 
9715b6e3ec5f
added prems argument to simplification procedures;
wenzelm
parents:
3565
diff
changeset

165 
> meta_simpset 
2509  166 
val del_simprocs : meta_simpset * 
3577
9715b6e3ec5f
added prems argument to simplification procedures;
wenzelm
parents:
3565
diff
changeset

167 
(string * cterm list * (Sign.sg > thm list > term > thm option) * stamp) list 
9715b6e3ec5f
added prems argument to simplification procedures;
wenzelm
parents:
3565
diff
changeset

168 
> meta_simpset 
1238  169 
val add_prems : meta_simpset * thm list > meta_simpset 
170 
val prems_of_mss : meta_simpset > thm list 

171 
val set_mk_rews : meta_simpset * (thm > thm list) > meta_simpset 

4679  172 
val set_mk_sym : meta_simpset * (thm > thm option) > meta_simpset 
173 
val set_mk_eq_True : meta_simpset * (thm > thm option) > meta_simpset 

2509  174 
val set_termless : meta_simpset * (term * term > bool) > meta_simpset 
1238  175 
val trace_simp : bool ref 
4713  176 
val rewrite_cterm : bool * bool * bool > meta_simpset > 
1529  177 
(meta_simpset > thm > thm option) > cterm > thm 
1539  178 

4999  179 
val invoke_oracle : theory > xstring > Sign.sg * Object.T > thm 
250  180 
end; 
0  181 

6089  182 
signature THM = 
183 
sig 

184 
include BASIC_THM 

185 
val no_attributes : 'a > 'a * 'b attribute list 

186 
val apply_attributes : ('a * thm) * 'a attribute list > ('a * thm) 

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

188 
val get_name_tags : thm > string * tag list 

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

190 
val name_of_thm : thm > string 

191 
val tags_of_thm : thm > tag list 

192 
val name_thm : string * thm > thm 

193 
end; 

194 

3550  195 
structure Thm: THM = 
0  196 
struct 
250  197 

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

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

199 

250  200 
(** certified types **) 
201 

202 
(*certified typs under a signature*) 

203 

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

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

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

206 
fun rep_ctyp (Ctyp {sign_ref, T}) = {sign = Sign.deref sign_ref, T = T}; 
250  207 
fun typ_of (Ctyp {T, ...}) = T; 
208 

209 
fun ctyp_of sign T = 

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

210 
Ctyp {sign_ref = Sign.self_ref sign, T = Sign.certify_typ sign T}; 
250  211 

212 
fun read_ctyp sign s = 

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

213 
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

214 

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

215 

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

216 

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

218 

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

220 

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

221 
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

222 

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

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

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

225 

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

228 
maxidx = maxidx}; 

229 

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

231 

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

232 
fun ctyp_of_term (Cterm {sign_ref, T, ...}) = Ctyp {sign_ref = sign_ref, T = T}; 
2671  233 

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

236 
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

237 
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

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

239 

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

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

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

242 

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

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

244 

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

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

246 
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

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

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

249 
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

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

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

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

253 
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

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

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

256 

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

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

258 
fun dest_abs (Cterm {sign_ref, T as Type("fun",[_,S]), maxidx, t=Abs(x,ty,M)}) = 
1516
96286c4e32de
removed mk_prop; added capply; simplified dest_abs
clasohm
parents:
1503
diff
changeset

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

260 
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

261 
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

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

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

264 

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

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

268 
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

269 

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

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

271 
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

272 
(Cterm {t=x, sign_ref=sign_ref2, T, maxidx=maxidx2}) = 
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

273 
if T = dty then Cterm{t=f$x, sign_ref=Sign.merge_refs(sign_ref1,sign_ref2), T=rty, 
2147  274 
maxidx=Int.max(maxidx1, maxidx2)} 
1516
96286c4e32de
removed mk_prop; added capply; simplified dest_abs
clasohm
parents:
1503
diff
changeset

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

276 
 capply _ _ = raise CTERM "capply: first arg is not a function" 
250  277 

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

278 
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

279 
(Cterm {t=t2, sign_ref=sign_ref2, T=T2, maxidx=maxidx2}) = 
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

280 
Cterm {t=absfree(a,ty,t2), sign_ref=Sign.merge_refs(sign_ref1,sign_ref2), 
2147  281 
T = ty > T2, maxidx=Int.max(maxidx1, maxidx2)} 
1517  282 
 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

283 

2509  284 

285 

574  286 
(** read cterms **) (*exception ERROR*) 
250  287 

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

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

289 
fun read_def_cterms (sign, types, sorts) used freeze sTs = 
250  290 
let 
4281
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

291 
val syn = #syn (Sign.rep_sg sign) 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

292 
fun read(s,T) = 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

293 
let val T' = Sign.certify_typ sign T 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

294 
handle TYPE (msg, _, _) => error msg 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

295 
in (Syntax.read syn T' s, T') end 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

296 
val tsTs = map read sTs 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

297 
val (ts',tye) = Sign.infer_types_simult sign types sorts used freeze tsTs; 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

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

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

302 

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

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

304 
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

305 
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

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

307 

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

308 
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

309 

250  310 

311 

1529  312 
(*** Derivations ***) 
313 

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

316 

1529  317 
(*Names of rules in derivations. Includes logically trivial rules, if 
318 
executed in ML.*) 

319 
datatype rule = 

2386  320 
MinProof (*for building minimal proof terms*) 
4999  321 
 Oracle of string * Sign.sg * Object.T (*oracles*) 
1529  322 
(*Axioms/theorems*) 
6089  323 
 Axiom of string * tag list 
324 
 Theorem of string * tag list 

1529  325 
(*primitive inferences and compound versions of them*) 
2386  326 
 Assume of cterm 
327 
 Implies_intr of cterm 

1529  328 
 Implies_intr_shyps 
329 
 Implies_intr_hyps 

330 
 Implies_elim 

2386  331 
 Forall_intr of cterm 
332 
 Forall_elim of cterm 

333 
 Reflexive of cterm 

1529  334 
 Symmetric 
335 
 Transitive 

2386  336 
 Beta_conversion of cterm 
1529  337 
 Extensional 
2386  338 
 Abstract_rule of string * cterm 
1529  339 
 Combination 
340 
 Equal_intr 

341 
 Equal_elim 

342 
(*derived rules for tactical proof*) 

2386  343 
 Trivial of cterm 
344 
(*For lift_rule, the proof state is not a premise. 

345 
Use cterm instead of thm to avoid mutual recursion.*) 

346 
 Lift_rule of cterm * int 

347 
 Assumption of int * Envir.env option (*includes eq_assumption*) 

2671  348 
 Rotate_rule of int * int 
7248
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

349 
 Permute_prems of int * int 
2386  350 
 Instantiate of (indexname * ctyp) list * (cterm * cterm) list 
351 
 Bicompose of bool * bool * int * int * Envir.env 

352 
 Flexflex_rule of Envir.env (*identifies unifier chosen*) 

1529  353 
(*other derived rules*) 
4182  354 
 Class_triv of class 
6786  355 
 VarifyT of string list 
1529  356 
 FreezeT 
357 
(*for the simplifier*) 

2386  358 
 RewriteC of cterm 
359 
 CongC of cterm 

360 
 Rewrite_cterm of cterm 

1529  361 
(*Logical identities, recorded since they are part of the proof process*) 
2386  362 
 Rename_params_rule of string list * int; 
1529  363 

364 

1597
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

365 
type deriv = rule mtree; 
1529  366 

1597
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

367 
datatype deriv_kind = MinDeriv  ThmDeriv  FullDeriv; 
1529  368 

1597
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

369 
val keep_derivs = ref MinDeriv; 
1529  370 

371 

1597
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

372 
(*Build a minimal derivation. Keep oracles; suppress atomic inferences; 
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

373 
retain Theorems or their underlying links; keep anything else*) 
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

374 
fun squash_derivs [] = [] 
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

375 
 squash_derivs (der::ders) = 
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

376 
(case der of 
2386  377 
Join (Oracle _, _) => der :: squash_derivs ders 
378 
 Join (Theorem _, [der']) => if !keep_derivs=ThmDeriv 

379 
then der :: squash_derivs ders 

380 
else squash_derivs (der'::ders) 

381 
 Join (Axiom _, _) => if !keep_derivs=ThmDeriv 

382 
then der :: squash_derivs ders 

383 
else squash_derivs ders 

384 
 Join (_, []) => squash_derivs ders 

385 
 _ => der :: squash_derivs ders); 

1597
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

386 

1529  387 

388 
(*Ensure sharing of the most likely derivation, the empty one!*) 

1597
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

389 
val min_infer = Join (MinProof, []); 
1529  390 

391 
(*Make a minimal inference*) 

392 
fun make_min_infer [] = min_infer 

393 
 make_min_infer [der] = der 

1597
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

394 
 make_min_infer ders = Join (MinProof, ders); 
1529  395 

1597
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

396 
fun infer_derivs (rl, []) = Join (rl, []) 
1529  397 
 infer_derivs (rl, ders) = 
1597
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

398 
if !keep_derivs=FullDeriv then Join (rl, ders) 
1529  399 
else make_min_infer (squash_derivs ders); 
400 

401 

2509  402 

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

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

404 

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

406 
{sign_ref: Sign.sg_ref, (*mutable reference to signature*) 
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

407 
der: deriv, (*derivation*) 
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

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

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

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

411 
prop: term}; (*conclusion*) 
0  412 

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

413 
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

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

415 
shyps = shyps, hyps = hyps, prop = prop}; 
0  416 

1529  417 
(*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

418 
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

419 
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

420 
in {sign = Sign.deref sign_ref, der = der, maxidx = maxidx, shyps = shyps, 
1529  421 
hyps = map (ctermf ~1) hyps, 
422 
prop = ctermf maxidx prop} 

1517  423 
end; 
424 

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

425 
(*errors involving theorems*) 
0  426 
exception THM of string * int * thm list; 
427 

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

430 

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

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

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

434 

3994  435 
(*equality of theorems uses equality of signatures and the 
436 
aconvertible test for terms*) 

437 
fun eq_thm (th1, th2) = 

438 
let 

439 
val {sign = sg1, shyps = shyps1, hyps = hyps1, prop = prop1, ...} = rep_thm th1; 

440 
val {sign = sg2, shyps = shyps2, hyps = hyps2, prop = prop2, ...} = rep_thm th2; 

441 
in 

442 
Sign.eq_sg (sg1, sg2) andalso 

443 
eq_set_sort (shyps1, shyps2) andalso 

444 
aconvs (hyps1, hyps2) andalso 

445 
prop1 aconv prop2 

446 
end; 

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

447 

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

448 
fun sign_of_thm (Thm {sign_ref, ...}) = Sign.deref sign_ref; 
0  449 

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

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

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

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

453 
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

454 

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

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

458 
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

459 
val sign = Sign.deref sign_ref; 
3895  460 
in 
4254  461 
if Sign.eq_sg (sign, sign') then thm 
462 
else if Sign.subsig (sign, sign') then 

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

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

466 
end; 

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

467 

6390  468 
val transfer = transfer_sg o Theory.sign_of; 
4254  469 

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

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

471 
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

472 

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

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

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

475 
Logic.strip_imp_prems (Logic.skip_flexpairs prop); 
0  476 

477 
(*counts premises in a rule*) 

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

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

479 
Logic.count_prems (Logic.skip_flexpairs prop, 0); 
0  480 

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

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

482 
fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop; 
0  483 

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

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

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

486 
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

487 

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

488 

0  489 

1238  490 
(** sort contexts of theorems **) 
491 

492 
(* basic utils *) 

493 

2163  494 
(*accumulate sorts suppressing duplicates; these are coded low levelly 
1238  495 
to improve efficiency a bit*) 
496 

497 
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

498 
 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

499 
 add_typ_sorts (TVar (_, S), Ss) = ins_sort(S,Ss) 
1238  500 
and add_typs_sorts ([], Ss) = Ss 
501 
 add_typs_sorts (T :: Ts, Ss) = add_typs_sorts (Ts, add_typ_sorts (T, Ss)); 

502 

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

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

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

506 
 add_term_sorts (Bound _, Ss) = Ss 

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

507 
 add_term_sorts (Abs (_,T,t), Ss) = add_term_sorts (t, add_typ_sorts (T,Ss)) 
1238  508 
 add_term_sorts (t $ u, Ss) = add_term_sorts (t, add_term_sorts (u, Ss)); 
509 

510 
fun add_terms_sorts ([], Ss) = Ss 

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

511 
 add_terms_sorts (t::ts, Ss) = add_terms_sorts (ts, add_term_sorts (t,Ss)); 
1238  512 

1258  513 
fun env_codT (Envir.Envir {iTs, ...}) = map snd iTs; 
514 

515 
fun add_env_sorts (env, Ss) = 

516 
add_terms_sorts (map snd (Envir.alist_of env), 

517 
add_typs_sorts (env_codT env, Ss)); 

518 

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

521 

522 
fun add_thms_shyps ([], Ss) = Ss 

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

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

524 
add_thms_shyps (ths, union_sort(shyps,Ss)); 
1238  525 

526 

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

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

529 
shyps \\ add_thm_sorts (th, []); 

530 

531 

532 
(* fix_shyps *) 

533 

534 
(*preserve sort contexts of rule premises and substituted types*) 

535 
fun fix_shyps thms Ts thm = 

536 
let 

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

537 
val Thm {sign_ref, der, maxidx, hyps, prop, ...} = thm; 
1238  538 
val shyps = 
539 
add_thm_sorts (thm, add_typs_sorts (Ts, add_thms_shyps (thms, []))); 

540 
in 

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

541 
Thm {sign_ref = sign_ref, 
2386  542 
der = der, (*No new derivation, as other rules call this*) 
543 
maxidx = maxidx, 

544 
shyps = shyps, hyps = hyps, prop = prop} 

1238  545 
end; 
546 

547 

548 
(* strip_shyps *) (* FIXME improve? (e.g. only minimal extra sorts) *) 

549 

3061  550 
val force_strip_shyps = ref true; (* FIXME tmp (since 1995/08/01) *) 
1238  551 

552 
(*remove extra sorts that are known to be syntactically nonempty*) 

553 
fun strip_shyps thm = 

554 
let 

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

555 
val Thm {sign_ref, der, maxidx, shyps, hyps, prop} = thm; 
1238  556 
val sorts = add_thm_sorts (thm, []); 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

557 
val maybe_empty = not o Sign.nonempty_sort (Sign.deref sign_ref) sorts; 
2177
8b365a3a6ed1
Changed some mem, ins and union calls to be monomorphic
paulson
parents:
2163
diff
changeset

558 
val shyps' = filter (fn S => mem_sort(S,sorts) orelse maybe_empty S) shyps; 
1238  559 
in 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

560 
Thm {sign_ref = sign_ref, der = der, maxidx = maxidx, 
2386  561 
shyps = 
562 
(if eq_set_sort (shyps',sorts) orelse 

563 
not (!force_strip_shyps) then shyps' 

3061  564 
else (* FIXME tmp (since 1995/08/01) *) 
2386  565 
(warning ("Removed sort hypotheses: " ^ 
2962  566 
commas (map Sorts.str_of_sort (shyps' \\ sorts))); 
2386  567 
warning "Let's hope these sorts are nonempty!"; 
1238  568 
sorts)), 
1529  569 
hyps = hyps, 
570 
prop = prop} 

1238  571 
end; 
572 

573 

574 
(* implies_intr_shyps *) 

575 

576 
(*discharge all extra sort hypotheses*) 

577 
fun implies_intr_shyps thm = 

578 
(case extra_shyps thm of 

579 
[] => thm 

580 
 xshyps => 

581 
let 

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

582 
val Thm {sign_ref, der, maxidx, shyps, hyps, prop} = thm; 
2182
29e56f003599
Removal of polymorphic equality via mem, subset, eq_set, etc
paulson
parents:
2177
diff
changeset

583 
val shyps' = ins_sort (logicS, shyps \\ xshyps); 
1238  584 
val used_names = foldr add_term_tfree_names (prop :: hyps, []); 
585 
val names = 

586 
tl (variantlist (replicate (length xshyps + 1) "'", used_names)); 

587 
val tfrees = map (TFree o rpair logicS) names; 

588 

589 
fun mk_insort (T, S) = map (Logic.mk_inclass o pair T) S; 

2671  590 
val sort_hyps = List.concat (map2 mk_insort (tfrees, xshyps)); 
1238  591 
in 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

592 
Thm {sign_ref = sign_ref, 
2386  593 
der = infer_derivs (Implies_intr_shyps, [der]), 
594 
maxidx = maxidx, 

595 
shyps = shyps', 

596 
hyps = hyps, 

597 
prop = Logic.list_implies (sort_hyps, prop)} 

1238  598 
end); 
599 

600 

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

602 

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

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

605 
let 
4847  606 
val name = Sign.intern (Theory.sign_of theory) Theory.axiomK raw_name; 
607 

608 
fun get_ax [] = None 

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

612 
Some t => 

613 
Some (fix_shyps [] [] 

614 
(Thm {sign_ref = Sign.self_ref sign, 

6089  615 
der = infer_derivs (Axiom (name, []), []), 
4847  616 
maxidx = maxidx_of_term t, 
617 
shyps = [], 

618 
hyps = [], 

619 
prop = t})) 

620 
 None => get_ax thys) 

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

622 
in 
4847  623 
(case get_ax (theory :: Theory.ancestors_of theory) of 
624 
Some thm => thm 

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

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

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

627 

6368  628 
fun def_name name = name ^ "_def"; 
629 
fun get_def thy = get_axiom thy o def_name; 

4847  630 

1529  631 

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

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

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

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

636 

6089  637 

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

639 

640 
fun get_name_tags (Thm {der, ...}) = 

4018  641 
(case der of 
6089  642 
Join (Theorem x, _) => x 
643 
 Join (Axiom x, _) => x 

644 
 _ => ("", [])); 

4018  645 

6089  646 
fun put_name_tags x (Thm {sign_ref, der, maxidx, shyps, hyps, prop}) = 
647 
let 

648 
val der' = 

649 
(case der of 

650 
Join (Theorem _, ds) => Join (Theorem x, ds) 

651 
 Join (Axiom _, ds) => Join (Axiom x, ds) 

652 
 _ => Join (Theorem x, [der])); 

653 
in 

654 
Thm {sign_ref = sign_ref, der = der', maxidx = maxidx, 

655 
shyps = shyps, hyps = hyps, prop = prop} 

656 
end; 

657 

658 
val name_of_thm = #1 o get_name_tags; 

659 
val tags_of_thm = #2 o get_name_tags; 

660 

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

0  662 

663 

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

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

666 
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

667 
Thm {sign_ref = sign_ref, 
2386  668 
der = der, (*No derivation recorded!*) 
669 
maxidx = maxidx, 

670 
shyps = shyps, 

671 
hyps = map Term.compress_term hyps, 

672 
prop = Term.compress_term prop}; 

564  673 

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

674 

2509  675 

1529  676 
(*** Meta rules ***) 
0  677 

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

680 
recurrence.*) 

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

681 
fun nodup_Vars (thm as Thm{sign_ref, der, maxidx, shyps, hyps, prop}) s = 
2147  682 
(Sign.nodup_Vars prop; 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

683 
Thm {sign_ref = sign_ref, 
2386  684 
der = der, 
685 
maxidx = maxidx_of_term prop, 

686 
shyps = shyps, 

687 
hyps = hyps, 

688 
prop = prop}) 

2147  689 
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

690 

1220  691 
(** 'primitive' rules **) 
692 

693 
(*discharge all assumptions t from ts*) 

0  694 
val disch = gen_rem (op aconv); 
695 

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

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

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

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

704 
else Thm{sign_ref = sign_ref, 
5344  705 
der = infer_derivs (Assume ct, []), 
2386  706 
maxidx = ~1, 
707 
shyps = add_term_sorts(prop,[]), 

708 
hyps = [prop], 

709 
prop = prop} 

0  710 
end; 
711 

1220  712 
(*Implication introduction 
3529  713 
[A] 
714 
: 

715 
B 

1220  716 
 
717 
A ==> B 

718 
*) 

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

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

720 
let val Cterm {sign_ref=sign_refA, t=A, T, maxidx=maxidxA} = cA 
0  721 
in if T<>propT then 
250  722 
raise THM("implies_intr: assumptions must have type prop", 0, [thB]) 
1238  723 
else fix_shyps [thB] [] 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

724 
(Thm{sign_ref = Sign.merge_refs (sign_ref,sign_refA), 
2386  725 
der = infer_derivs (Implies_intr cA, [der]), 
726 
maxidx = Int.max(maxidxA, maxidx), 

727 
shyps = [], 

728 
hyps = disch(hyps,A), 

729 
prop = implies$A$prop}) 

0  730 
handle TERM _ => 
731 
raise THM("implies_intr: incompatible signatures", 0, [thB]) 

732 
end; 

733 

1529  734 

1220  735 
(*Implication elimination 
736 
A ==> B A 

737 
 

738 
B 

739 
*) 

0  740 
fun implies_elim thAB thA : thm = 
1529  741 
let val Thm{maxidx=maxA, der=derA, hyps=hypsA, prop=propA,...} = thA 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

742 
and Thm{sign_ref, der, maxidx, hyps, prop,...} = thAB; 
250  743 
fun err(a) = raise THM("implies_elim: "^a, 0, [thAB,thA]) 
0  744 
in case prop of 
250  745 
imp$A$B => 
746 
if imp=implies andalso A aconv propA 

1220  747 
then fix_shyps [thAB, thA] [] 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

748 
(Thm{sign_ref= merge_thm_sgs(thAB,thA), 
2386  749 
der = infer_derivs (Implies_elim, [der,derA]), 
750 
maxidx = Int.max(maxA,maxidx), 

751 
shyps = [], 

752 
hyps = union_term(hypsA,hyps), (*dups suppressed*) 

753 
prop = B}) 

250  754 
else err("major premise") 
755 
 _ => err("major premise") 

0  756 
end; 
250  757 

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

760 
 

761 
!!x.A 

762 
*) 

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

763 
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

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

766 
(Thm{sign_ref = sign_ref, 
2386  767 
der = infer_derivs (Forall_intr cx, [der]), 
768 
maxidx = maxidx, 

769 
shyps = [], 

770 
hyps = hyps, 

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

0  772 
in case x of 
250  773 
Free(a,T) => 
774 
if exists (apl(x, Logic.occs)) hyps 

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

776 
else result(a,T) 

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

779 
end; 

780 

1220  781 
(*Forall elimination 
782 
!!x.A 

783 
 

784 
A[t/x] 

785 
*) 

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

786 
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

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

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

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

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

793 
(Thm{sign_ref= Sign.merge_refs(sign_ref,sign_reft), 
2386  794 
der = infer_derivs (Forall_elim ct, [der]), 
795 
maxidx = Int.max(maxidx, maxt), 

796 
shyps = [], 

797 
hyps = hyps, 

798 
prop = betapply(A,t)}) 

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

800 
then nodup_Vars thm "forall_elim" 

801 
else thm (*no new Vars: no expensive check!*) 

802 
end 

2147  803 
 _ => raise THM("forall_elim: not quantified", 0, [th]) 
0  804 
end 
805 
handle TERM _ => 

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

808 

1220  809 
(* Equality *) 
0  810 

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

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

813 
let val Cterm {sign_ref, t, T, maxidx} = ct 
1238  814 
in fix_shyps [] [] 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

815 
(Thm{sign_ref= sign_ref, 
2386  816 
der = infer_derivs (Reflexive ct, []), 
817 
shyps = [], 

818 
hyps = [], 

819 
maxidx = maxidx, 

820 
prop = Logic.mk_equals(t,t)}) 

0  821 
end; 
822 

823 
(*The symmetry rule 

1220  824 
t==u 
825 
 

826 
u==t 

827 
*) 

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

828 
fun symmetric (th as Thm{sign_ref,der,maxidx,shyps,hyps,prop}) = 
0  829 
case prop of 
830 
(eq as Const("==",_)) $ t $ u => 

1238  831 
(*no fix_shyps*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

832 
Thm{sign_ref = sign_ref, 
2386  833 
der = infer_derivs (Symmetric, [der]), 
834 
maxidx = maxidx, 

835 
shyps = shyps, 

836 
hyps = hyps, 

837 
prop = eq$u$t} 

0  838 
 _ => raise THM("symmetric", 0, [th]); 
839 

840 
(*The transitive rule 

1220  841 
t1==u u==t2 
842 
 

843 
t1==t2 

844 
*) 

0  845 
fun transitive th1 th2 = 
1529  846 
let val Thm{der=der1, maxidx=max1, hyps=hyps1, prop=prop1,...} = th1 
847 
and Thm{der=der2, maxidx=max2, hyps=hyps2, prop=prop2,...} = th2; 

0  848 
fun err(msg) = raise THM("transitive: "^msg, 0, [th1,th2]) 
849 
in case (prop1,prop2) of 

850 
((eq as Const("==",_)) $ t1 $ u, Const("==",_) $ u' $ t2) => 

1634  851 
if not (u aconv u') then err"middle term" 
852 
else let val thm = 

1220  853 
fix_shyps [th1, th2] [] 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

854 
(Thm{sign_ref= merge_thm_sgs(th1,th2), 
2386  855 
der = infer_derivs (Transitive, [der1, der2]), 
2147  856 
maxidx = Int.max(max1,max2), 
2386  857 
shyps = [], 
858 
hyps = union_term(hyps1,hyps2), 

859 
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

860 
in if max1 >= 0 andalso max2 >= 0 
2147  861 
then nodup_Vars thm "transitive" 
862 
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

863 
end 
0  864 
 _ => err"premises" 
865 
end; 

866 

1160  867 
(*Betaconversion: maps (%x.t)(u) to the theorem (%x.t)(u) == t[u/x] *) 
250  868 
fun beta_conversion ct = 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

869 
let val Cterm {sign_ref, t, T, maxidx} = ct 
0  870 
in case t of 
1238  871 
Abs(_,_,bodt) $ u => fix_shyps [] [] 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

872 
(Thm{sign_ref = sign_ref, 
2386  873 
der = infer_derivs (Beta_conversion ct, []), 
874 
maxidx = maxidx, 

875 
shyps = [], 

876 
hyps = [], 

877 
prop = Logic.mk_equals(t, subst_bound (u,bodt))}) 

250  878 
 _ => raise THM("beta_conversion: not a redex", 0, []) 
0  879 
end; 
880 

881 
(*The extensionality rule (proviso: x not free in f, g, or hypotheses) 

1220  882 
f(x) == g(x) 
883 
 

884 
f == g 

885 
*) 

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

886 
fun extensional (th as Thm{sign_ref, der, maxidx,shyps,hyps,prop}) = 
0  887 
case prop of 
888 
(Const("==",_)) $ (f$x) $ (g$y) => 

250  889 
let fun err(msg) = raise THM("extensional: "^msg, 0, [th]) 
0  890 
in (if x<>y then err"different variables" else 
891 
case y of 

250  892 
Free _ => 
893 
if exists (apl(y, Logic.occs)) (f::g::hyps) 

894 
then err"variable free in hyps or functions" else () 

895 
 Var _ => 

896 
if Logic.occs(y,f) orelse Logic.occs(y,g) 

897 
then err"variable free in functions" else () 

898 
 _ => err"not a variable"); 

1238  899 
(*no fix_shyps*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

900 
Thm{sign_ref = sign_ref, 
2386  901 
der = infer_derivs (Extensional, [der]), 
902 
maxidx = maxidx, 

903 
shyps = shyps, 

904 
hyps = hyps, 

1529  905 
prop = Logic.mk_equals(f,g)} 
0  906 
end 
907 
 _ => raise THM("extensional: premise", 0, [th]); 

908 

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

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

1220  911 
t == u 
912 
 

913 
%x.t == %x.u 

914 
*) 

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

915 
fun abstract_rule a 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

916 
let val x = term_of cx; 
250  917 
val (t,u) = Logic.dest_equals prop 
918 
handle TERM _ => 

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

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

921 
(Thm{sign_ref = sign_ref, 
2386  922 
der = infer_derivs (Abstract_rule (a,cx), [der]), 
923 
maxidx = maxidx, 

924 
shyps = [], 

925 
hyps = hyps, 

926 
prop = Logic.mk_equals(Abs(a, T, abstract_over (x,t)), 

927 
Abs(a, T, abstract_over (x,u)))}) 

0  928 
in case x of 
250  929 
Free(_,T) => 
930 
if exists (apl(x, Logic.occs)) hyps 

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

932 
else result T 

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

935 
end; 

936 

937 
(*The combination rule 

3529  938 
f == g t == u 
939 
 

940 
f(t) == g(u) 

1220  941 
*) 
0  942 
fun combination th1 th2 = 
1529  943 
let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1, 
2386  944 
prop=prop1,...} = th1 
1529  945 
and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, 
2386  946 
prop=prop2,...} = th2 
1836
861e29c7cada
Added typechecking to rule "combination". This corrects a fault
paulson
parents:
1802
diff
changeset

947 
fun chktypes (f,t) = 
2386  948 
(case fastype_of f of 
949 
Type("fun",[T1,T2]) => 

950 
if T1 <> fastype_of t then 

951 
raise THM("combination: types", 0, [th1,th2]) 

952 
else () 

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

954 
[th1,th2])) 

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

955 
in case (prop1,prop2) of 
0  956 
(Const("==",_) $ f $ g, Const("==",_) $ t $ u) => 
1836
861e29c7cada
Added typechecking to rule "combination". This corrects a fault
paulson
parents:
1802
diff
changeset

957 
let val _ = chktypes (f,t) 
2386  958 
val thm = (*no fix_shyps*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

959 
Thm{sign_ref = merge_thm_sgs(th1,th2), 
2386  960 
der = infer_derivs (Combination, [der1, der2]), 
961 
maxidx = Int.max(max1,max2), 

962 
shyps = union_sort(shyps1,shyps2), 

963 
hyps = union_term(hyps1,hyps2), 

964 
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

965 
in if max1 >= 0 andalso max2 >= 0 
2c59b204b540
Only calls nodup_Vars if really necessary. We get a speedup of nearly 6%
paulson
parents:
2047
diff
changeset

966 
then nodup_Vars thm "combination" 
2386  967 
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

968 
end 
0  969 
 _ => raise THM("combination: premises", 0, [th1,th2]) 
970 
end; 

971 

972 

973 
(* Equality introduction 

3529  974 
A ==> B B ==> A 
975 
 

976 
A == B 

1220  977 
*) 
0  978 
fun equal_intr th1 th2 = 
1529  979 
let val Thm{der=der1,maxidx=max1, shyps=shyps1, hyps=hyps1, 
2386  980 
prop=prop1,...} = th1 
1529  981 
and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, 
2386  982 
prop=prop2,...} = th2; 
1529  983 
fun err(msg) = raise THM("equal_intr: "^msg, 0, [th1,th2]) 
984 
in case (prop1,prop2) of 

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

2386  986 
if A aconv A' andalso B aconv B' 
987 
then 

988 
(*no fix_shyps*) 

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

989 
Thm{sign_ref = merge_thm_sgs(th1,th2), 
2386  990 
der = infer_derivs (Equal_intr, [der1, der2]), 
991 
maxidx = Int.max(max1,max2), 

992 
shyps = union_sort(shyps1,shyps2), 

993 
hyps = union_term(hyps1,hyps2), 

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

995 
else err"not equal" 

1529  996 
 _ => err"premises" 
997 
end; 

998 

999 

1000 
(*The equal propositions rule 

3529  1001 
A == B A 
1529  1002 
 
1003 
B 

1004 
*) 

1005 
fun equal_elim th1 th2 = 

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

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

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

1009 
in case prop1 of 

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

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

1012 
fix_shyps [th1, th2] [] 

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

1013 
(Thm{sign_ref= merge_thm_sgs(th1,th2), 
2386  1014 
der = infer_derivs (Equal_elim, [der1, der2]), 
1015 
maxidx = Int.max(max1,max2), 

1016 
shyps = [], 

1017 
hyps = union_term(hyps1,hyps2), 

1018 
prop = B}) 

1529  1019 
 _ => err"major premise" 
1020 
end; 

0  1021 

1220  1022 

1023 

0  1024 
(**** Derived rules ****) 
1025 

1503  1026 
(*Discharge all hypotheses. Need not verify cterms or call fix_shyps. 
0  1027 
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

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

1030 
(Thm{sign_ref = sign_ref, 
2386  1031 
der = infer_derivs (Implies_intr_hyps, [der]), 
1032 
maxidx = maxidx, 

1033 
shyps = shyps, 

1529  1034 
hyps = disch(As,A), 
2386  1035 
prop = implies$A$prop}) 
0  1036 
 implies_intr_hyps th = th; 
1037 

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

250  1039 
Instantiates the theorem and deletes trivial tpairs. 
0  1040 
Resulting sequence may contain multiple elements if the tpairs are 
1041 
not all flexflex. *) 

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

1042 
fun flexflex_rule (th as Thm{sign_ref, der, maxidx, hyps, prop,...}) = 
250  1043 
let fun newthm env = 
1529  1044 
if Envir.is_empty env then th 
1045 
else 

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

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

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

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

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

1052 
(Thm{sign_ref = sign_ref, 
2386  1053 
der = infer_derivs (Flexflex_rule env, [der]), 
1054 
maxidx = maxidx_of_term newprop, 

1055 
shyps = [], 

1056 
hyps = hyps, 

1057 
prop = newprop}) 

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

1061 
(Unify.smash_unifiers(Sign.deref sign_ref, Envir.empty maxidx, tpairs)) 
0  1062 
end; 
1063 

1064 
(*Instantiation of Vars 

1220  1065 
A 
1066 
 

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

1068 
*) 

0  1069 

6928  1070 
local 
1071 

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

1074 

6928  1075 
fun prt_typing sg_ref t T = 
1076 
let val sg = Sign.deref sg_ref in 

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

1078 
end; 

1079 

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

1081 
fun add_ctpair ((ct,cu), (sign_ref,tpairs)) = 
6928  1082 
let 
1083 
val Cterm {sign_ref=sign_reft, t=t, T= T, ...} = ct 

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

1085 
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

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

1089 
Pretty.fbrk, prt_typing sign_ref_merged t T, 

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

0  1091 
end; 
1092 

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

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

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

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

6928  1097 
in 
1098 

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

1101 
Normalizes the new theorem! *) 

1529  1102 
fun instantiate ([], []) th = th 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

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

1104 
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

1105 
val (newsign_ref,vTs) = foldr add_ctyp (vcTs, (newsign_ref,[])); 
250  1106 
val newprop = 
1107 
Envir.norm_term (Envir.empty 0) 

1108 
(subst_atomic tpairs 

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

1109 
(Type.inst_term_tvars(Sign.tsig_of (Sign.deref newsign_ref),vTs) prop)) 
1220  1110 
val newth = 
1111 
fix_shyps [th] (map snd vTs) 

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

1112 
(Thm{sign_ref = newsign_ref, 
2386  1113 
der = infer_derivs (Instantiate(vcTs,ctpairs), [der]), 
1114 
maxidx = maxidx_of_term newprop, 

1115 
shyps = [], 

1116 
hyps = hyps, 

1117 
prop = newprop}) 

250  1118 
in if not(instl_ok(map #1 tpairs)) 
193  1119 
then raise THM("instantiate: variables not distinct", 0, [th]) 
1120 
else if not(null(findrep(map #1 vTs))) 

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

2147  1122 
else nodup_Vars newth "instantiate" 
0  1123 
end 
6928  1124 
handle TERM _ => raise THM("instantiate: incompatible signatures", 0, [th]) 
1125 
 TYPE (msg, _, _) => raise THM (msg, 0, [th]); 

1126 

1127 
end; 

1128 

0  1129 

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

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

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

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

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

1137 
(Thm{sign_ref = sign_ref, 
2386  1138 
der = infer_derivs (Trivial ct, []), 
1139 
maxidx = maxidx, 

1140 
shyps = [], 

1141 
hyps = [], 

1142 
prop = implies$A$A}) 

0  1143 
end; 
1144 

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

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

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

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

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

1152 
(Thm {sign_ref = sign_ref, 
4182  1153 
der = infer_derivs (Class_triv c, []), 
2386  1154 
maxidx = maxidx, 
1155 
shyps = [], 

1156 
hyps = [], 

1157 
prop = t}) 

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

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

1159 

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

1160 

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

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

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

1165 
Thm{sign_ref = sign_ref, 
6786  1166 
der = infer_derivs (VarifyT fixed, [der]), 
2386  1167 
maxidx = Int.max(0,maxidx), 
1168 
shyps = shyps, 

1169 
hyps = hyps, 

1529  1170 
prop = Type.varify(prop,tfrees)} 
2147  1171 
in nodup_Vars thm "varifyT" end 
1634  1172 
(* this nodup_Vars check can be removed if thms are guaranteed not to contain 
1173 
duplicate TVars with differnt sorts *) 

0  1174 
end; 
1175 

6786  1176 
val varifyT = varifyT' []; 
1177 

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

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

1182 
Thm{sign_ref = sign_ref, 
2386  1183 
der = infer_derivs (FreezeT, [der]), 
1184 
maxidx = maxidx_of_term prop', 

1185 
shyps = shyps, 

1186 
hyps = hyps, 

1529  1187 
prop = prop'} 
1220  1188 
end; 
0  1189 

1190 

1191 
(*** Inference rules for tactics ***) 

1192 

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

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

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

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

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

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

1199 
end 

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

1201 

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

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

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

1208 
val ct_Bi = Cterm {sign_ref=ssign_ref, maxidx=smax, T=propT, t=Bi} 
1529  1209 
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

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

1213 
Thm{sign_ref = merge_thm_sgs(state,orule), 
2386  1214 
der = infer_derivs (Lift_rule(ct_Bi, i), [der]), 
1215 
maxidx = maxidx+smax+1, 

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

1216 
shyps=union_sort(sshyps,shyps), 
2386  1217 
hyps=hyps, 
1529  1218 
prop = Logic.rule_of (map (pairself lift_abs) tpairs, 
2386  1219 
map lift_all As, 
1220 
lift_all B)} 

0  1221 
end; 
1222 

1223 
(*Solve subgoal Bi of proof state B1...Bn/C by assumption. *) 

1224 
fun assumption i state = 

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

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

1229 
(Thm{sign_ref = sign_ref, 
2386  1230 
der = infer_derivs (Assumption (i, Some env), [der]), 
1231 
maxidx = maxidx, 

1232 
shyps = [], 

1233 
hyps = hyps, 

1234 
prop = 

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

1236 
Logic.rule_of (tpairs, Bs, C) 

1237 
else (*normalize the new rule fully*) 

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

4270  1239 
fun addprfs [] = Seq.empty 
1240 
 addprfs ((t,u)::apairs) = Seq.make (fn()=> Seq.pull 

1241 
(Seq.mapp newth 

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

1242 
(Unify.unifiers(Sign.deref sign_ref,Envir.empty maxidx, (t,u)::tpairs)) 
250  1243 
(addprfs apairs))) 
0  1244 
in addprfs (Logic.assum_pairs Bi) end; 
1245 

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

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

1249 
let val Thm{sign_ref,der,maxidx,hyps,prop,...} = state; 
0  1250 
val (tpairs, Bs, Bi, C) = dest_state(state,i) 
1251 
in if exists (op aconv) (Logic.assum_pairs Bi) 

1220  1252 
then fix_shyps [state] [] 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

1253 
(Thm{sign_ref = sign_ref, 
2386  1254 
der = infer_derivs (Assumption (i,None), [der]), 
1255 
maxidx = maxidx, 

1256 
shyps = [], 

1257 
hyps = hyps, 

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

0  1259 
else raise THM("eq_assumption", 0, [state]) 
1260 
end; 

1261 

1262 

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

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

1265 
let val Thm{sign_ref,der,maxidx,hyps,prop,shyps} = state; 
2671  1266 
val (tpairs, Bs, Bi, C) = dest_state(state,i) 
1267 
val params = Logic.strip_params Bi 

1268 
and asms = Logic.strip_assums_hyp Bi 

1269 
and concl = Logic.strip_assums_concl Bi 

1270 
val n = length asms 

1271 
fun rot m = if 0=m orelse m=n then Bi 

1272 
else if 0<m andalso m<n 

1273 
then list_all 

1274 
(params, 

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

1276 
List.take(asms, m), 

1277 
concl)) 

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

1278 
else raise THM("rotate_rule", k, [state]) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

1279 
in Thm{sign_ref = sign_ref, 
2671  1280 
der = infer_derivs (Rotate_rule (k,i), [der]), 
1281 
maxidx = maxidx, 

1282 
shyps = shyps, 

1283 
hyps = hyps, 

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

1285 
end; 

1286 

1287 

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

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

1289 
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

1290 
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

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

1292 
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

1293 
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

1294 
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

1295 
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

1296 
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

1297 
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

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

1299 
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

1300 
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

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

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

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

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

1305 
else raise THM("permute_prems:k", k, [rl]) 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1306 
in Thm{sign_ref = sign_ref, 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1307 
der = infer_derivs (Permute_prems (j,k), [der]), 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

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

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

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

1311 
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

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

1313 

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

1314 

0  1315 
(** User renaming of parameters in a subgoal **) 
1316 

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

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

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

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

1321 
fun rename_params_rule (cs, i) state = 

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

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

1325 
val short = length iparams  length cs 

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

1328 
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

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

1333 
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

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

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

1336 
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

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

1339 
(Thm{sign_ref = sign_ref, 
2386  1340 
der = infer_derivs (Rename_params_rule(cs,i), [der]), 
1341 
maxidx = maxidx, 

1342 
shyps = [], 

1343 
hyps = hyps, 

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

0  1345 
end; 
1346 

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

1348 

250  1349 
(*Scan a pair of terms; while they are similar, 
0  1350 
accumulate corresponding bound vars in "al"*) 
1238  1351 
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

1352 
match_bvs(s, t, if x="" orelse y="" then al 
1238  1353 
else (x,y)::al) 
0  1354 
 match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al)) 
1355 
 match_bvs(_,_,al) = al; 

1356 
