author  berghofe 
Fri, 10 Mar 2000 14:58:25 +0100  
changeset 8407  d522ad1809e9 
parent 8299  52d9f64841d6 
child 8608  3759be3d1ebf 
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_hyps 
54 
 Implies_elim 

2671  55 
 Forall_intr of cterm 
56 
 Forall_elim of cterm 

57 
 Reflexive of cterm 

1529  58 
 Symmetric 
59 
 Transitive 

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

65 
 Equal_elim 

2671  66 
 Trivial of cterm 
67 
 Lift_rule of cterm * int 

68 
 Assumption of int * Envir.env option 

69 
 Rotate_rule of int * int 

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

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

73 
 Flexflex_rule of Envir.env 

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

79 
 Rewrite_cterm of cterm 

80 
 Rename_params_rule of string list * int; 

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

1160  83 
(*meta theorems*) 
84 
type thm 

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

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

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

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

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

99 
val nprems_of : thm > int 

100 
val concl_of : thm > term 

101 
val cprop_of : thm > cterm 

102 
val extra_shyps : thm > sort list 

103 
val strip_shyps : thm > thm 

3812  104 
val get_axiom : theory > xstring > thm 
6368  105 
val def_name : string > string 
4847  106 
val get_def : theory > xstring > thm 
1238  107 
val axioms_of : theory > (string * thm) list 
1160  108 

109 
(*meta rules*) 

1238  110 
val assume : cterm > thm 
1416  111 
val compress : thm > thm 
1238  112 
val implies_intr : cterm > thm > thm 
113 
val implies_elim : thm > thm > thm 

114 
val forall_intr : cterm > thm > thm 

115 
val forall_elim : cterm > thm > thm 

116 
val reflexive : cterm > thm 

117 
val symmetric : thm > thm 

118 
val transitive : thm > thm > thm 

119 
val beta_conversion : cterm > thm 

120 
val extensional : thm > thm 

121 
val abstract_rule : string > cterm > thm > thm 

122 
val combination : thm > thm > thm 

123 
val equal_intr : thm > thm > thm 

124 
val equal_elim : thm > thm > thm 

125 
val implies_intr_hyps : thm > thm 

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

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

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

147 
(*meta simplification*) 

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

1238  152 
val empty_mss : meta_simpset 
6899  153 
val clear_mss : meta_simpset > meta_simpset 
3550  154 
val merge_mss : meta_simpset * meta_simpset > meta_simpset 
1238  155 
val add_simps : meta_simpset * thm list > meta_simpset 
156 
val del_simps : meta_simpset * thm list > meta_simpset 

157 
val mss_of : thm list > meta_simpset 

158 
val add_congs : meta_simpset * thm list > meta_simpset 

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

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

162 
> meta_simpset 
2509  163 
val del_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 
1238  166 
val add_prems : meta_simpset * thm list > meta_simpset 
167 
val prems_of_mss : meta_simpset > thm list 

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

4679  169 
val set_mk_sym : meta_simpset * (thm > thm option) > meta_simpset 
170 
val set_mk_eq_True : meta_simpset * (thm > thm option) > meta_simpset 

2509  171 
val set_termless : meta_simpset * (term * term > bool) > meta_simpset 
1238  172 
val trace_simp : bool ref 
7921  173 
val debug_simp : bool ref 
4713  174 
val rewrite_cterm : bool * bool * bool > meta_simpset > 
1529  175 
(meta_simpset > thm > thm option) > cterm > thm 
1539  176 

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

6089  180 
signature THM = 
181 
sig 

182 
include BASIC_THM 

8299  183 
val major_prem_of : thm > term 
7534  184 
val no_prems : thm > bool 
6089  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}) = 
8291  273 
if T = dty then 
274 
Cterm{t=Sign.nodup_vars (f$x), sign_ref=Sign.merge_refs(sign_ref1,sign_ref2), T=rty, 

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

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

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

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

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

279 
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

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

284 

2509  285 

286 

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

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

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

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

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

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

294 
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

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

296 
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

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

298 
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

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

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

303 

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

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

305 
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

306 
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

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

308 

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

309 
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

310 

250  311 

312 

1529  313 
(*** Derivations ***) 
314 

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

317 

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

320 
datatype rule = 

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

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

1529  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 

8299  481 
fun major_prem_of thm = 
482 
(case prems_of thm of 

483 
prem :: _ => prem 

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

485 

7534  486 
fun no_prems thm = nprems_of thm = 0; 
487 

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

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

489 
fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop; 
0  490 

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

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

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

493 
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

494 

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

495 

0  496 

1238  497 
(** sort contexts of theorems **) 
498 

499 
(* basic utils *) 

500 

2163  501 
(*accumulate sorts suppressing duplicates; these are coded low levelly 
1238  502 
to improve efficiency a bit*) 
503 

504 
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

505 
 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

506 
 add_typ_sorts (TVar (_, S), Ss) = ins_sort(S,Ss) 
1238  507 
and add_typs_sorts ([], Ss) = Ss 
508 
 add_typs_sorts (T :: Ts, Ss) = add_typs_sorts (Ts, add_typ_sorts (T, Ss)); 

509 

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

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

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

513 
 add_term_sorts (Bound _, Ss) = Ss 

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

514 
 add_term_sorts (Abs (_,T,t), Ss) = add_term_sorts (t, add_typ_sorts (T,Ss)) 
1238  515 
 add_term_sorts (t $ u, Ss) = add_term_sorts (t, add_term_sorts (u, Ss)); 
516 

517 
fun add_terms_sorts ([], Ss) = Ss 

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

518 
 add_terms_sorts (t::ts, Ss) = add_terms_sorts (ts, add_term_sorts (t,Ss)); 
1238  519 

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

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

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

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

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

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

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

528 

529 
fun add_thms_shyps ([], Ss) = Ss 

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

7642  531 
add_thms_shyps (ths, union_sort (shyps, Ss)); 
1238  532 

533 

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

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

7642  536 
Term.rems_sort (shyps, add_thm_sorts (th, [])); 
1238  537 

538 

539 
(* fix_shyps *) 

540 

7642  541 
fun all_sorts_nonempty sign_ref = is_some (Sign.univ_witness (Sign.deref sign_ref)); 
542 

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

546 
{sign_ref = sign_ref, 

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

548 
maxidx = maxidx, 

549 
shyps = 

550 
if all_sorts_nonempty sign_ref then [] 

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

552 
hyps = hyps, prop = prop} 

1238  553 

554 

7642  555 
(* strip_shyps *) 
1238  556 

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

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

560 
let 

561 
val sign = Sign.deref sign_ref; 

1238  562 

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

565 
val witnessed_shyps = Sign.witness_sorts sign present_sorts extra_shyps; 

566 
in 

567 
Thm {sign_ref = sign_ref, der = der, maxidx = maxidx, 

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

569 
hyps = hyps, prop = prop} 

570 
end; 

1238  571 

572 

573 

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

575 

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

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

578 
let 
4847  579 
val name = Sign.intern (Theory.sign_of theory) Theory.axiomK raw_name; 
580 

581 
fun get_ax [] = None 

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

585 
Some t => 

586 
Some (fix_shyps [] [] 

587 
(Thm {sign_ref = Sign.self_ref sign, 

6089  588 
der = infer_derivs (Axiom (name, []), []), 
4847  589 
maxidx = maxidx_of_term t, 
590 
shyps = [], 

591 
hyps = [], 

592 
prop = t})) 

593 
 None => get_ax thys) 

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

595 
in 
4847  596 
(case get_ax (theory :: Theory.ancestors_of theory) of 
597 
Some thm => thm 

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

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

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

600 

6368  601 
fun def_name name = name ^ "_def"; 
602 
fun get_def thy = get_axiom thy o def_name; 

4847  603 

1529  604 

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

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

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

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

609 

6089  610 

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

612 

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

4018  614 
(case der of 
6089  615 
Join (Theorem x, _) => x 
616 
 Join (Axiom x, _) => x 

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

4018  618 

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

621 
val der' = 

622 
(case der of 

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

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

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

626 
in 

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

628 
shyps = shyps, hyps = hyps, prop = prop} 

629 
end; 

630 

631 
val name_of_thm = #1 o get_name_tags; 

632 
val tags_of_thm = #2 o get_name_tags; 

633 

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

0  635 

636 

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

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

639 
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

640 
Thm {sign_ref = sign_ref, 
2386  641 
der = der, (*No derivation recorded!*) 
642 
maxidx = maxidx, 

643 
shyps = shyps, 

644 
hyps = map Term.compress_term hyps, 

645 
prop = Term.compress_term prop}; 

564  646 

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

647 

2509  648 

1529  649 
(*** Meta rules ***) 
0  650 

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

653 
recurrence.*) 

8291  654 
fun nodup_vars (thm as Thm{sign_ref, der, maxidx, shyps, hyps, prop}) s = 
8296  655 
Thm {sign_ref = sign_ref, 
2386  656 
der = der, 
657 
maxidx = maxidx_of_term prop, 

658 
shyps = shyps, 

659 
hyps = hyps, 

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

662 

8291  663 

1220  664 
(** 'primitive' rules **) 
665 

666 
(*discharge all assumptions t from ts*) 

0  667 
val disch = gen_rem (op aconv); 
668 

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

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

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

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

677 
else Thm{sign_ref = sign_ref, 
5344  678 
der = infer_derivs (Assume ct, []), 
2386  679 
maxidx = ~1, 
680 
shyps = add_term_sorts(prop,[]), 

681 
hyps = [prop], 

682 
prop = prop} 

0  683 
end; 
684 

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

688 
B 

1220  689 
 
690 
A ==> B 

691 
*) 

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

692 
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

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

697 
(Thm{sign_ref = Sign.merge_refs (sign_ref,sign_refA), 
2386  698 
der = infer_derivs (Implies_intr cA, [der]), 
699 
maxidx = Int.max(maxidxA, maxidx), 

700 
shyps = [], 

701 
hyps = disch(hyps,A), 

702 
prop = implies$A$prop}) 

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

705 
end; 

706 

1529  707 

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

710 
 

711 
B 

712 
*) 

0  713 
fun implies_elim thAB thA : thm = 
1529  714 
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

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

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

721 
(Thm{sign_ref= merge_thm_sgs(thAB,thA), 
2386  722 
der = infer_derivs (Implies_elim, [der,derA]), 
723 
maxidx = Int.max(maxA,maxidx), 

724 
shyps = [], 

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

726 
prop = B}) 

250  727 
else err("major premise") 
728 
 _ => err("major premise") 

0  729 
end; 
250  730 

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

733 
 

734 
!!x.A 

735 
*) 

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

736 
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

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

739 
(Thm{sign_ref = sign_ref, 
2386  740 
der = infer_derivs (Forall_intr cx, [der]), 
741 
maxidx = maxidx, 

742 
shyps = [], 

743 
hyps = hyps, 

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

0  745 
in case x of 
250  746 
Free(a,T) => 
747 
if exists (apl(x, Logic.occs)) hyps 

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

749 
else result(a,T) 

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

752 
end; 

753 

1220  754 
(*Forall elimination 
755 
!!x.A 

756 
 

757 
A[t/x] 

758 
*) 

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

759 
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

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

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

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

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

766 
(Thm{sign_ref= Sign.merge_refs(sign_ref,sign_reft), 
2386  767 
der = infer_derivs (Forall_elim ct, [der]), 
768 
maxidx = Int.max(maxidx, maxt), 

769 
shyps = [], 

770 
hyps = hyps, 

771 
prop = betapply(A,t)}) 

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

8291  773 
then nodup_vars thm "forall_elim" 
2386  774 
else thm (*no new Vars: no expensive check!*) 
775 
end 

2147  776 
 _ => raise THM("forall_elim: not quantified", 0, [th]) 
0  777 
end 
778 
handle TERM _ => 

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

781 

1220  782 
(* Equality *) 
0  783 

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

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

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

788 
(Thm{sign_ref= sign_ref, 
2386  789 
der = infer_derivs (Reflexive ct, []), 
790 
shyps = [], 

791 
hyps = [], 

792 
maxidx = maxidx, 

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

0  794 
end; 
795 

796 
(*The symmetry rule 

1220  797 
t==u 
798 
 

799 
u==t 

800 
*) 

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

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

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

805 
Thm{sign_ref = sign_ref, 
2386  806 
der = infer_derivs (Symmetric, [der]), 
807 
maxidx = maxidx, 

808 
shyps = shyps, 

809 
hyps = hyps, 

810 
prop = eq$u$t} 

0  811 
 _ => raise THM("symmetric", 0, [th]); 
812 

813 
(*The transitive rule 

1220  814 
t1==u u==t2 
815 
 

816 
t1==t2 

817 
*) 

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

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

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

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

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

827 
(Thm{sign_ref= merge_thm_sgs(th1,th2), 
2386  828 
der = infer_derivs (Transitive, [der1, der2]), 
2147  829 
maxidx = Int.max(max1,max2), 
2386  830 
shyps = [], 
831 
hyps = union_term(hyps1,hyps2), 

832 
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

833 
in if max1 >= 0 andalso max2 >= 0 
8291  834 
then nodup_vars thm "transitive" 
2147  835 
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

836 
end 
0  837 
 _ => err"premises" 
838 
end; 

839 

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

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

845 
(Thm{sign_ref = sign_ref, 
2386  846 
der = infer_derivs (Beta_conversion ct, []), 
847 
maxidx = maxidx, 

848 
shyps = [], 

849 
hyps = [], 

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

250  851 
 _ => raise THM("beta_conversion: not a redex", 0, []) 
0  852 
end; 
853 

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

1220  855 
f(x) == g(x) 
856 
 

857 
f == g 

858 
*) 

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

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

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

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

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

868 
 Var _ => 

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

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

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

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

873 
Thm{sign_ref = sign_ref, 
2386  874 
der = infer_derivs (Extensional, [der]), 
875 
maxidx = maxidx, 

876 
shyps = shyps, 

877 
hyps = hyps, 

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

881 

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

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

1220  884 
t == u 
885 
 

886 
%x.t == %x.u 

887 
*) 

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

888 
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

889 
let val x = term_of cx; 
250  890 
val (t,u) = Logic.dest_equals prop 
891 
handle TERM _ => 

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

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

894 
(Thm{sign_ref = sign_ref, 
2386  895 
der = infer_derivs (Abstract_rule (a,cx), [der]), 
896 
maxidx = maxidx, 

897 
shyps = [], 

898 
hyps = hyps, 

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

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

0  901 
in case x of 
250  902 
Free(_,T) => 
903 
if exists (apl(x, Logic.occs)) hyps 

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

905 
else result T 

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

908 
end; 

909 

910 
(*The combination rule 

3529  911 
f == g t == u 
912 
 

913 
f(t) == g(u) 

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

920 
fun chktypes (f,t) = 
2386  921 
(case fastype_of f of 
922 
Type("fun",[T1,T2]) => 

923 
if T1 <> fastype_of t then 

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

925 
else () 

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

927 
[th1,th2])) 

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

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

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

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

935 
shyps = union_sort(shyps1,shyps2), 

936 
hyps = union_term(hyps1,hyps2), 

937 
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

938 
in if max1 >= 0 andalso max2 >= 0 
8291  939 
then nodup_vars thm "combination" 
2386  940 
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

941 
end 
0  942 
 _ => raise THM("combination: premises", 0, [th1,th2]) 
943 
end; 

944 

945 

946 
(* Equality introduction 

3529  947 
A ==> B B ==> A 
948 
 

949 
A == B 

1220  950 
*) 
0  951 
fun equal_intr th1 th2 = 
1529  952 
let val Thm{der=der1,maxidx=max1, shyps=shyps1, hyps=hyps1, 
2386  953 
prop=prop1,...} = th1 
1529  954 
and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, 
2386  955 
prop=prop2,...} = th2; 
1529  956 
fun err(msg) = raise THM("equal_intr: "^msg, 0, [th1,th2]) 
957 
in case (prop1,prop2) of 

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

2386  959 
if A aconv A' andalso B aconv B' 
960 
then 

961 
(*no fix_shyps*) 

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

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

965 
shyps = union_sort(shyps1,shyps2), 

966 
hyps = union_term(hyps1,hyps2), 

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

968 
else err"not equal" 

1529  969 
 _ => err"premises" 
970 
end; 

971 

972 

973 
(*The equal propositions rule 

3529  974 
A == B A 
1529  975 
 
976 
B 

977 
*) 

978 
fun equal_elim th1 th2 = 

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

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

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

982 
in case prop1 of 

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

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

985 
fix_shyps [th1, th2] [] 

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

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

989 
shyps = [], 

990 
hyps = union_term(hyps1,hyps2), 

991 
prop = B}) 

1529  992 
 _ => err"major premise" 
993 
end; 

0  994 

1220  995 

996 

0  997 
(**** Derived rules ****) 
998 

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

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

1003 
(Thm{sign_ref = sign_ref, 
2386  1004 
der = infer_derivs (Implies_intr_hyps, [der]), 
1005 
maxidx = maxidx, 

1006 
shyps = shyps, 

1529  1007 
hyps = disch(As,A), 
2386  1008 
prop = implies$A$prop}) 
0  1009 
 implies_intr_hyps th = th; 
1010 

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

250  1012 
Instantiates the theorem and deletes trivial tpairs. 
0  1013 
Resulting sequence may contain multiple elements if the tpairs are 
1014 
not all flexflex. *) 

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

1015 
fun flexflex_rule (th as Thm{sign_ref, der, maxidx, hyps, prop,...}) = 
250  1016 
let fun newthm env = 
1529  1017 
if Envir.is_empty env then th 
1018 
else 

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

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

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

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

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

1025 
(Thm{sign_ref = sign_ref, 
2386  1026 
der = infer_derivs (Flexflex_rule env, [der]), 
1027 
maxidx = maxidx_of_term newprop, 

1028 
shyps = [], 

1029 
hyps = hyps, 

1030 
prop = newprop}) 

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

1034 
(Unify.smash_unifiers(Sign.deref sign_ref, Envir.empty maxidx, tpairs)) 
0  1035 
end; 
1036 

1037 
(*Instantiation of Vars 

1220  1038 
A 
1039 
 

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

1041 
*) 

0  1042 

6928  1043 
local 
1044 

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

1047 

6928  1048 
fun prt_typing sg_ref t T = 
1049 
let val sg = Sign.deref sg_ref in 

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

1051 
end; 

1052 

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

1054 
fun add_ctpair ((ct,cu), (sign_ref,tpairs)) = 
6928  1055 
let 
1056 
val Cterm {sign_ref=sign_reft, t=t, T= T, ...} = ct 

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

1058 
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

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

1062 
Pretty.fbrk, prt_typing sign_ref_merged t T, 

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

0  1064 
end; 
1065 

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

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

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

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

6928  1070 
in 
1071 

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

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

1074 
No longer normalizes the new theorem! *) 
1529  1075 
fun instantiate ([], []) th = th 
8129
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8066
diff
changeset

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

1077 
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

1078 
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

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

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

1081 
(Sign.tsig_of (Sign.deref newsign_ref),vTs) prop) 
1220  1082 
val newth = 
1083 
fix_shyps [th] (map snd vTs) 

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

1084 
(Thm{sign_ref = newsign_ref, 
2386  1085 
der = infer_derivs (Instantiate(vcTs,ctpairs), [der]), 
1086 
maxidx = maxidx_of_term newprop, 

1087 
shyps = [], 

1088 
hyps = hyps, 

1089 
prop = newprop}) 

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

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

8291  1094 
else nodup_vars newth "instantiate" 
0  1095 
end 
6928  1096 
handle TERM _ => raise THM("instantiate: incompatible signatures", 0, [th]) 
1097 
 TYPE (msg, _, _) => raise THM (msg, 0, [th]); 

1098 

1099 
end; 

1100 

0  1101 

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

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

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

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

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

1109 
(Thm{sign_ref = sign_ref, 
2386  1110 
der = infer_derivs (Trivial ct, []), 
1111 
maxidx = maxidx, 

1112 
shyps = [], 

1113 
hyps = [], 

1114 
prop = implies$A$A}) 

0  1115 
end; 
1116 

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

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

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

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

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

1124 
(Thm {sign_ref = sign_ref, 
4182  1125 
der = infer_derivs (Class_triv c, []), 
2386  1126 
maxidx = maxidx, 
1127 
shyps = [], 

1128 
hyps = [], 

1129 
prop = t}) 

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

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

1131 

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

1132 

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

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

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

1137 
Thm{sign_ref = sign_ref, 
6786  1138 
der = infer_derivs (VarifyT fixed, [der]), 
2386  1139 
maxidx = Int.max(0,maxidx), 
1140 
shyps = shyps, 

1141 
hyps = hyps, 

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

1145 
duplicate TVars with different sorts *) 

0  1146 
end; 
1147 

6786  1148 
val varifyT = varifyT' []; 
1149 

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

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

1154 
Thm{sign_ref = sign_ref, 
2386  1155 
der = infer_derivs (FreezeT, [der]), 
1156 
maxidx = maxidx_of_term prop', 

1157 
shyps = shyps, 

1158 
hyps = hyps, 

1529  1159 
prop = prop'} 
1220  1160 
end; 
0  1161 

1162 

1163 
(*** Inference rules for tactics ***) 

1164 

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

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

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

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

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

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

1171 
end 

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

1173 

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

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

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

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

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

1185 
Thm{sign_ref = merge_thm_sgs(state,orule), 
2386  1186 
der = infer_derivs (Lift_rule(ct_Bi, i), [der]), 
1187 
maxidx = maxidx+smax+1, 

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

1188 
shyps=union_sort(sshyps,shyps), 
2386  1189 
hyps=hyps, 
1529  1190 
prop = Logic.rule_of (map (pairself lift_abs) tpairs, 
2386  1191 
map lift_all As, 
1192 
lift_all B)} 

0  1193 
end; 
1194 

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

1196 
fun assumption i state = 

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

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

1201 
(Thm{sign_ref = sign_ref, 
2386  1202 
der = infer_derivs (Assumption (i, Some env), [der]), 
1203 
maxidx = maxidx, 

1204 
shyps = [], 

1205 
hyps = hyps, 

1206 
prop = 

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

1208 
Logic.rule_of (tpairs, Bs, C) 

1209 
else (*normalize the new rule fully*) 

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

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

1213 
(Seq.mapp newth 

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

1214 
(Unify.unifiers(Sign.deref sign_ref,Envir.empty maxidx, (t,u)::tpairs)) 
250  1215 
(addprfs apairs))) 
0  1216 
in addprfs (Logic.assum_pairs Bi) end; 
1217 

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

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

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

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

1225 
(Thm{sign_ref = sign_ref, 
2386  1226 
der = infer_derivs (Assumption (i,None), [der]), 
1227 
maxidx = maxidx, 

1228 
shyps = [], 

1229 
hyps = hyps, 

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

0  1231 
else raise THM("eq_assumption", 0, [state]) 
1232 
end; 

1233 

1234 

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

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

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

1239 
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

1240 
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

1241 
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

1242 
and concl = Logic.strip_imp_concl rest 
2671  1243 
val n = length asms 
1244 
fun rot m = if 0=m orelse m=n then Bi 

1245 
else if 0<m andalso m<n 

1246 
then list_all 

1247 
(params, 

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

1249 
List.take(asms, m), 

1250 
concl)) 

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

1251 
else raise THM("rotate_rule", k, [state]) 
7264  1252 
in (*no fix_shyps*) 
1253 
Thm{sign_ref = sign_ref, 

2671  1254 
der = infer_derivs (Rotate_rule (k,i), [der]), 
1255 
maxidx = maxidx, 

1256 
shyps = shyps, 

1257 
hyps = hyps, 

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

1259 
end; 

1260 

1261 

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

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

1263 
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

1264 
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

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

1266 
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

1267 
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

1268 
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

1269 
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

1270 
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

1271 
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

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

1273 
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

1274 
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

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

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

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

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

1279 
else raise THM("permute_prems:k", k, [rl]) 
7264  1280 
in (*no fix_shyps*) 
1281 
Thm{sign_ref = sign_ref, 

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

1282 
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

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

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

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

1286 
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

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

1288 

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

1289 

0  1290 
(** User renaming of parameters in a subgoal **) 
1291 

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

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

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

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

1296 
fun rename_params_rule (cs, i) state = 

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

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

1300 
val short = length iparams  length cs 

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

1303 
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

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

1308 
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

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

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

1311 
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

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

1314 
(Thm{sign_ref = sign_ref, 
2386  1315 
der = infer_derivs (Rename_params_rule(cs,i), [der]), 
1316 
maxidx = maxidx, 

1317 
shyps = [], 

1318 
hyps = hyps, 

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

0  1320 
end; 
1321 

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

1323 

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

1327 
match_bvs(s, t, if x="" orelse y="" then al 
1238  1328 
else (x,y)::al) 
0  1329 
 match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al)) 
1330 
 match_bvs(_,_,al) = al; 

1331 

1332 
(* strip abstractions created by parameters *) 

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

1334 

1335 

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

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

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

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

1343 
 strip(A,_) = f A 

0  1344 
in strip end; 
1345 

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

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

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

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

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

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

1353 
(*unknowns appearing elsewhere be preserved!*) 

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

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

1356 
(case assoc(al,x) of 

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

1357 
Some(y) => if x mem_string vids orelse y mem_string vids then t 
250 