author  berghofe 
Tue, 07 Nov 2000 17:52:12 +0100  
changeset 10416  5b33e732e459 
parent 10348  a5653826379e 
child 10486  7b07dd104a1a 
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} 
9461  24 
val sign_of_cterm : cterm > Sign.sg 
1238  25 
val term_of : cterm > term 
26 
val cterm_of : Sign.sg > term > cterm 

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

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

30 
val dest_comb : cterm > cterm * cterm 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

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

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

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

39 
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

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

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

2671  43 
(*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

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

2671  52 
 Assume of cterm 
53 
 Implies_intr of cterm 

1529  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 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

62 
 Eta_conversion of cterm 
1529  63 
 Extensional 
2671  64 
 Abstract_rule of string * cterm 
1529  65 
 Combination 
66 
 Equal_intr 

67 
 Equal_elim 

2671  68 
 Trivial of cterm 
69 
 Lift_rule of cterm * int 

70 
 Assumption of int * Envir.env option 

71 
 Rotate_rule of int * int 

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

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

75 
 Flexflex_rule of Envir.env 

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

81 
 Rewrite_cterm of cterm 

82 
 Rename_params_rule of string list * int; 

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

1160  85 
(*meta theorems*) 
86 
type thm 

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

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

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

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

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

101 
val nprems_of : thm > int 

102 
val concl_of : thm > term 

103 
val cprop_of : thm > cterm 

104 
val extra_shyps : thm > sort list 

105 
val strip_shyps : thm > thm 

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

111 
(*meta rules*) 

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

116 
val forall_intr : cterm > thm > thm 

117 
val forall_elim : cterm > thm > thm 

118 
val reflexive : cterm > thm 

119 
val symmetric : thm > thm 

120 
val transitive : thm > thm > thm 

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

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

122 
val eta_conversion : cterm > thm 
1238  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 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

140 
val incr_indexes : int > thm > thm 
4270  141 
val assumption : int > thm > thm Seq.seq 
1238  142 
val eq_assumption : int > thm > thm 
2671  143 
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

144 
val permute_prems : int > int > thm > thm 
1160  145 
val rename_params_rule: string list * int > thm > thm 
1238  146 
val bicompose : bool > bool * thm * int > 
4270  147 
int > thm > thm Seq.seq 
1238  148 
val biresolution : bool > (bool * thm) list > 
4270  149 
int > thm > thm Seq.seq 
4999  150 
val invoke_oracle : theory > xstring > Sign.sg * Object.T > thm 
250  151 
end; 
0  152 

6089  153 
signature THM = 
154 
sig 

155 
include BASIC_THM 

8299  156 
val major_prem_of : thm > term 
7534  157 
val no_prems : thm > bool 
6089  158 
val no_attributes : 'a > 'a * 'b attribute list 
159 
val apply_attributes : ('a * thm) * 'a attribute list > ('a * thm) 

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

161 
val get_name_tags : thm > string * tag list 

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

163 
val name_of_thm : thm > string 

164 
val tags_of_thm : thm > tag list 

165 
val name_thm : string * thm > thm 

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

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

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

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

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

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

171 
val cterm_incr_indexes : int > cterm > cterm 
6089  172 
end; 
173 

3550  174 
structure Thm: THM = 
0  175 
struct 
250  176 

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

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

178 

250  179 
(** certified types **) 
180 

181 
(*certified typs under a signature*) 

182 

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

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

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

185 
fun rep_ctyp (Ctyp {sign_ref, T}) = {sign = Sign.deref sign_ref, T = T}; 
250  186 
fun typ_of (Ctyp {T, ...}) = T; 
187 

188 
fun ctyp_of sign T = 

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

189 
Ctyp {sign_ref = Sign.self_ref sign, T = Sign.certify_typ sign T}; 
250  190 

191 
fun read_ctyp sign s = 

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

192 
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

193 

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

194 

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

195 

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

197 

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

199 

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

200 
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

201 

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

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

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

204 

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

207 
maxidx = maxidx}; 

208 

9461  209 
fun sign_of_cterm (Cterm {sign_ref, ...}) = Sign.deref sign_ref; 
210 

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

212 

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

213 
fun ctyp_of_term (Cterm {sign_ref, T, ...}) = Ctyp {sign_ref = sign_ref, T = T}; 
2671  214 

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

217 
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

218 
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

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

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

223 

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

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

225 

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

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

227 
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

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

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

230 
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

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

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

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

234 
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

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

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

237 

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

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

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

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

241 
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

242 
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

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

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

245 

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

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

249 
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

250 

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

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

252 
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

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

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

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

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

258 
 capply _ _ = raise CTERM "capply: first arg is not a function" 
250  259 

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

260 
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

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

265 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

284 

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

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

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

287 

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

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

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

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

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

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

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

294 

2509  295 

296 

574  297 
(** read cterms **) (*exception ERROR*) 
250  298 

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

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

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

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

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

307 

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

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

309 
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

310 
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

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

312 

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

313 
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

314 

250  315 

316 

1529  317 
(*** Derivations ***) 
318 

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

321 

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

324 
datatype rule = 

2386  325 
MinProof (*for building minimal proof terms*) 
4999  326 
 Oracle of string * Sign.sg * Object.T (*oracles*) 
1529  327 
(*Axioms/theorems*) 
6089  328 
 Axiom of string * tag list 
329 
 Theorem of string * tag list 

1529  330 
(*primitive inferences and compound versions of them*) 
2386  331 
 Assume of cterm 
332 
 Implies_intr of cterm 

1529  333 
 Implies_intr_hyps 
334 
 Implies_elim 

2386  335 
 Forall_intr of cterm 
336 
 Forall_elim of cterm 

337 
 Reflexive of cterm 

1529  338 
 Symmetric 
339 
 Transitive 

2386  340 
 Beta_conversion of cterm 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

341 
 Eta_conversion of cterm 
1529  342 
 Extensional 
2386  343 
 Abstract_rule of string * cterm 
1529  344 
 Combination 
345 
 Equal_intr 

346 
 Equal_elim 

347 
(*derived rules for tactical proof*) 

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

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

351 
 Lift_rule of cterm * int 

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

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

354 
 Permute_prems of int * int 
2386  355 
 Instantiate of (indexname * ctyp) list * (cterm * cterm) list 
356 
 Bicompose of bool * bool * int * int * Envir.env 

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

1529  358 
(*other derived rules*) 
4182  359 
 Class_triv of class 
6786  360 
 VarifyT of string list 
1529  361 
 FreezeT 
362 
(*for the simplifier*) 

2386  363 
 RewriteC of cterm 
364 
 CongC of cterm 

365 
 Rewrite_cterm of cterm 

1529  366 
(*Logical identities, recorded since they are part of the proof process*) 
2386  367 
 Rename_params_rule of string list * int; 
1529  368 

369 

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

370 
type deriv = rule mtree; 
1529  371 

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

372 
datatype deriv_kind = MinDeriv  ThmDeriv  FullDeriv; 
1529  373 

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

374 
val keep_derivs = ref MinDeriv; 
1529  375 

9501  376 
local 
1529  377 

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

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

379 
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

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

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

382 
(case der of 
2386  383 
Join (Oracle _, _) => der :: squash_derivs ders 
384 
 Join (Theorem _, [der']) => if !keep_derivs=ThmDeriv 

385 
then der :: squash_derivs ders 

386 
else squash_derivs (der'::ders) 

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

388 
then der :: squash_derivs ders 

389 
else squash_derivs ders 

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

391 
 _ => der :: squash_derivs ders); 

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

392 

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

394 
val min_infer = Join (MinProof, []); 
1529  395 

396 
(*Make a minimal inference*) 

397 
fun make_min_infer [] = min_infer 

398 
 make_min_infer [der] = der 

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

399 
 make_min_infer ders = Join (MinProof, ders); 
1529  400 

9501  401 
fun is_oracle (Oracle _) = true 
402 
 is_oracle _ = false; 

403 

404 
in 

405 

406 
fun infer_derivs (rl, []: (bool * deriv) list) = (is_oracle rl, Join (rl, [])) 

1529  407 
 infer_derivs (rl, ders) = 
9501  408 
(is_oracle rl orelse exists #1 ders, 
409 
if !keep_derivs=FullDeriv then Join (rl, map #2 ders) 

410 
else make_min_infer (squash_derivs (map #2 ders))); 

411 

412 
end; 

1529  413 

414 

2509  415 

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

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

417 

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

419 
{sign_ref: Sign.sg_ref, (*mutable reference to signature*) 
9501  420 
der: bool * deriv, (*derivation*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

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

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

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

424 
prop: term}; (*conclusion*) 
0  425 

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

426 
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

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

428 
shyps = shyps, hyps = hyps, prop = prop}; 
0  429 

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

431 
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

432 
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

433 
in {sign = Sign.deref sign_ref, der = der, maxidx = maxidx, shyps = shyps, 
1529  434 
hyps = map (ctermf ~1) hyps, 
435 
prop = ctermf maxidx prop} 

1517  436 
end; 
437 

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

438 
(*errors involving theorems*) 
0  439 
exception THM of string * int * thm list; 
440 

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

443 

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

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

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

447 

3994  448 
fun eq_thm (th1, th2) = 
449 
let 

9031  450 
val {sign = sg1, shyps = shyps1, hyps = hyps1, prop = prop1, maxidx = _, der = _} = 
451 
rep_thm th1; 

452 
val {sign = sg2, shyps = shyps2, hyps = hyps2, prop = prop2, maxidx = _, der = _} = 

453 
rep_thm th2; 

3994  454 
in 
9031  455 
Sign.joinable (sg1, sg2) andalso 
3994  456 
eq_set_sort (shyps1, shyps2) andalso 
457 
aconvs (hyps1, hyps2) andalso 

458 
prop1 aconv prop2 

459 
end; 

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

460 

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

461 
fun sign_of_thm (Thm {sign_ref, ...}) = Sign.deref sign_ref; 
0  462 

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

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

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

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

466 
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

467 

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

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

471 
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

472 
val sign = Sign.deref sign_ref; 
3895  473 
in 
4254  474 
if Sign.eq_sg (sign, sign') then thm 
475 
else if Sign.subsig (sign, sign') then 

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

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

479 
end; 

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

480 

6390  481 
val transfer = transfer_sg o Theory.sign_of; 
4254  482 

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

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

484 
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

485 

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

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

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

488 
Logic.strip_imp_prems (Logic.skip_flexpairs prop); 
0  489 

490 
(*counts premises in a rule*) 

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

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

492 
Logic.count_prems (Logic.skip_flexpairs prop, 0); 
0  493 

8299  494 
fun major_prem_of thm = 
495 
(case prems_of thm of 

496 
prem :: _ => prem 

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

498 

7534  499 
fun no_prems thm = nprems_of thm = 0; 
500 

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

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

502 
fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop; 
0  503 

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

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

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

506 
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

507 

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

508 

0  509 

1238  510 
(** sort contexts of theorems **) 
511 

512 
(* basic utils *) 

513 

2163  514 
(*accumulate sorts suppressing duplicates; these are coded low levelly 
1238  515 
to improve efficiency a bit*) 
516 

517 
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

518 
 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

519 
 add_typ_sorts (TVar (_, S), Ss) = ins_sort(S,Ss) 
1238  520 
and add_typs_sorts ([], Ss) = Ss 
521 
 add_typs_sorts (T :: Ts, Ss) = add_typs_sorts (Ts, add_typ_sorts (T, Ss)); 

522 

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

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

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

526 
 add_term_sorts (Bound _, Ss) = Ss 

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

527 
 add_term_sorts (Abs (_,T,t), Ss) = add_term_sorts (t, add_typ_sorts (T,Ss)) 
1238  528 
 add_term_sorts (t $ u, Ss) = add_term_sorts (t, add_term_sorts (u, Ss)); 
529 

530 
fun add_terms_sorts ([], Ss) = Ss 

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

531 
 add_terms_sorts (t::ts, Ss) = add_terms_sorts (ts, add_term_sorts (t,Ss)); 
1238  532 

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

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

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

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

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

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

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

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

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

541 

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

544 

545 
fun add_thms_shyps ([], Ss) = Ss 

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

7642  547 
add_thms_shyps (ths, union_sort (shyps, Ss)); 
1238  548 

549 

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

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

7642  552 
Term.rems_sort (shyps, add_thm_sorts (th, [])); 
1238  553 

554 

555 
(* fix_shyps *) 

556 

7642  557 
fun all_sorts_nonempty sign_ref = is_some (Sign.univ_witness (Sign.deref sign_ref)); 
558 

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

562 
{sign_ref = sign_ref, 

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

564 
maxidx = maxidx, 

565 
shyps = 

566 
if all_sorts_nonempty sign_ref then [] 

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

568 
hyps = hyps, prop = prop} 

1238  569 

570 

7642  571 
(* strip_shyps *) 
1238  572 

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

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

576 
let 

577 
val sign = Sign.deref sign_ref; 

1238  578 

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

581 
val witnessed_shyps = Sign.witness_sorts sign present_sorts extra_shyps; 

582 
in 

583 
Thm {sign_ref = sign_ref, der = der, maxidx = maxidx, 

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

585 
hyps = hyps, prop = prop} 

586 
end; 

1238  587 

588 

589 

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

591 

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

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

594 
let 
4847  595 
val name = Sign.intern (Theory.sign_of theory) Theory.axiomK raw_name; 
596 

597 
fun get_ax [] = None 

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

601 
Some t => 

602 
Some (fix_shyps [] [] 

603 
(Thm {sign_ref = Sign.self_ref sign, 

6089  604 
der = infer_derivs (Axiom (name, []), []), 
4847  605 
maxidx = maxidx_of_term t, 
606 
shyps = [], 

607 
hyps = [], 

608 
prop = t})) 

609 
 None => get_ax thys) 

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

611 
in 
4847  612 
(case get_ax (theory :: Theory.ancestors_of theory) of 
613 
Some thm => thm 

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

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

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

616 

6368  617 
fun def_name name = name ^ "_def"; 
618 
fun get_def thy = get_axiom thy o def_name; 

4847  619 

1529  620 

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

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

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

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

625 

6089  626 

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

628 

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

9501  630 
(case #2 der of 
6089  631 
Join (Theorem x, _) => x 
632 
 Join (Axiom x, _) => x 

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

4018  634 

9501  635 
fun put_name_tags x (Thm {sign_ref, der = (ora, der), maxidx, shyps, hyps, prop}) = 
6089  636 
let 
637 
val der' = 

638 
(case der of 

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

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

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

642 
in 

9501  643 
Thm {sign_ref = sign_ref, der = (ora, der'), maxidx = maxidx, 
6089  644 
shyps = shyps, hyps = hyps, prop = prop} 
645 
end; 

646 

647 
val name_of_thm = #1 o get_name_tags; 

648 
val tags_of_thm = #2 o get_name_tags; 

649 

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

0  651 

652 

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

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

655 
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

656 
Thm {sign_ref = sign_ref, 
2386  657 
der = der, (*No derivation recorded!*) 
658 
maxidx = maxidx, 

659 
shyps = shyps, 

660 
hyps = map Term.compress_term hyps, 

661 
prop = Term.compress_term prop}; 

564  662 

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

663 

2509  664 

1529  665 
(*** Meta rules ***) 
0  666 

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

669 
recurrence.*) 

8291  670 
fun nodup_vars (thm as Thm{sign_ref, der, maxidx, shyps, hyps, prop}) s = 
8296  671 
Thm {sign_ref = sign_ref, 
2386  672 
der = der, 
673 
maxidx = maxidx_of_term prop, 

674 
shyps = shyps, 

675 
hyps = hyps, 

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

678 

8291  679 

1220  680 
(** 'primitive' rules **) 
681 

682 
(*discharge all assumptions t from ts*) 

0  683 
val disch = gen_rem (op aconv); 
684 

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

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

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

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

693 
else Thm{sign_ref = sign_ref, 
5344  694 
der = infer_derivs (Assume ct, []), 
2386  695 
maxidx = ~1, 
696 
shyps = add_term_sorts(prop,[]), 

697 
hyps = [prop], 

698 
prop = prop} 

0  699 
end; 
700 

1220  701 
(*Implication introduction 
3529  702 
[A] 
703 
: 

704 
B 

1220  705 
 
706 
A ==> B 

707 
*) 

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

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

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

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

713 
Thm{sign_ref = Sign.merge_refs (sign_ref,sign_refA), 
2386  714 
der = infer_derivs (Implies_intr cA, [der]), 
715 
maxidx = Int.max(maxidxA, maxidx), 

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

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

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

721 
end; 

722 

1529  723 

1220  724 
(*Implication elimination 
725 
A ==> B A 

726 
 

727 
B 

728 
*) 

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

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

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

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

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

737 
Thm{sign_ref= merge_thm_sgs(thAB,thA), 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

738 
der = infer_derivs (Implies_elim, [der,derA]), 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

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

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

742 
prop = B} 
250  743 
else err("major premise") 
744 
 _ => err("major premise") 

0  745 
end; 
250  746 

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

749 
 

750 
!!x.A 

751 
*) 

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

752 
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

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

755 
(Thm{sign_ref = sign_ref, 
2386  756 
der = infer_derivs (Forall_intr cx, [der]), 
757 
maxidx = maxidx, 

758 
shyps = [], 

759 
hyps = hyps, 

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

0  761 
in case x of 
250  762 
Free(a,T) => 
763 
if exists (apl(x, Logic.occs)) hyps 

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

765 
else result(a,T) 

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

768 
end; 

769 

1220  770 
(*Forall elimination 
771 
!!x.A 

772 
 

773 
A[t/x] 

774 
*) 

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

775 
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

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

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

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

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

782 
(Thm{sign_ref= Sign.merge_refs(sign_ref,sign_reft), 
2386  783 
der = infer_derivs (Forall_elim ct, [der]), 
784 
maxidx = Int.max(maxidx, maxt), 

785 
shyps = [], 

786 
hyps = hyps, 

787 
prop = betapply(A,t)}) 

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

8291  789 
then nodup_vars thm "forall_elim" 
2386  790 
else thm (*no new Vars: no expensive check!*) 
791 
end 

2147  792 
 _ => raise THM("forall_elim: not quantified", 0, [th]) 
0  793 
end 
794 
handle TERM _ => 

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

797 

1220  798 
(* Equality *) 
0  799 

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

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

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

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

804 
der = infer_derivs (Reflexive ct, []), 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

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

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

808 
prop = Logic.mk_equals(t,t)} 
0  809 
end; 
810 

811 
(*The symmetry rule 

1220  812 
t==u 
813 
 

814 
u==t 

815 
*) 

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

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

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

820 
Thm{sign_ref = sign_ref, 
2386  821 
der = infer_derivs (Symmetric, [der]), 
822 
maxidx = maxidx, 

823 
shyps = shyps, 

824 
hyps = hyps, 

825 
prop = eq$u$t} 

0  826 
 _ => raise THM("symmetric", 0, [th]); 
827 

828 
(*The transitive rule 

1220  829 
t1==u u==t2 
830 
 

831 
t1==t2 

832 
*) 

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

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

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

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

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

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

841 
Thm{sign_ref= merge_thm_sgs(th1,th2), 
2386  842 
der = infer_derivs (Transitive, [der1, der2]), 
2147  843 
maxidx = Int.max(max1,max2), 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

846 
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

847 
in if max1 >= 0 andalso max2 >= 0 
8291  848 
then nodup_vars thm "transitive" 
2147  849 
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

850 
end 
0  851 
 _ => err"premises" 
852 
end; 

853 

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

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

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

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

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

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

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

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

861 
der = infer_derivs (Beta_conversion ct, []), 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

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

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

865 
prop = Logic.mk_equals (t, if full then Envir.norm_term (Envir.empty 0) t 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

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

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

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

870 

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

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

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

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

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

875 
der = infer_derivs (Eta_conversion ct, []), 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

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

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

879 
prop = Logic.mk_equals (t, Pattern.eta_contract t)} 
0  880 
end; 
881 

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

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

885 
f == g 

886 
*) 

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

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

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

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

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

896 
 Var _ => 

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

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

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

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

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

904 
shyps = shyps, 

905 
hyps = hyps, 

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

909 

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

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

1220  912 
t == u 
913 
 

914 
%x.t == %x.u 

915 
*) 

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

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

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

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

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

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

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

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

925 
shyps = add_typ_sorts (T, shyps), 
2386  926 
hyps = hyps, 
927 
prop = Logic.mk_equals(Abs(a, T, abstract_over (x,t)), 

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

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

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

933 
else result T 

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

936 
end; 

937 

938 
(*The combination rule 

3529  939 
f == g t == u 
940 
 

941 
f(t) == g(u) 

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

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

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

951 
if T1 <> tT then 
2386  952 
raise THM("combination: types", 0, [th1,th2]) 
953 
else () 

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

955 
[th1,th2])) 

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

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

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

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

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

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

964 
shyps = union_sort(shyps1,shyps2), 

965 
hyps = union_term(hyps1,hyps2), 

966 
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

967 
in if max1 >= 0 andalso max2 >= 0 
8291  968 
then nodup_vars thm "combination" 
2386  969 
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

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

973 

974 

975 
(* Equality introduction 

3529  976 
A ==> B B ==> A 
977 
 

978 
A == B 

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

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

2386  988 
if A aconv A' andalso B aconv B' 
989 
then 

990 
(*no fix_shyps*) 

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

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

994 
shyps = union_sort(shyps1,shyps2), 

995 
hyps = union_term(hyps1,hyps2), 

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

997 
else err"not equal" 

1529  998 
 _ => err"premises" 
999 
end; 

1000 

1001 

1002 
(*The equal propositions rule 

3529  1003 
A == B A 
1529  1004 
 
1005 
B 

1006 
*) 

1007 
fun equal_elim th1 th2 = 

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

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

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

1011 
in case prop1 of 

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

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

1014 
fix_shyps [th1, th2] [] 

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

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

1018 
shyps = [], 

1019 
hyps = union_term(hyps1,hyps2), 

1020 
prop = B}) 

1529  1021 
 _ => err"major premise" 
1022 
end; 

0  1023 

1220  1024 

1025 

0  1026 
(**** Derived rules ****) 
1027 

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

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

1032 
(Thm{sign_ref = sign_ref, 
2386  1033 
der = infer_derivs (Implies_intr_hyps, [der]), 
1034 
maxidx = maxidx, 

1035 
shyps = shyps, 

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

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

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

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

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

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

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

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

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

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

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

1057 
shyps = [], 

1058 
hyps = hyps, 

1059 
prop = newprop}) 

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

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

1066 
(*Instantiation of Vars 

1220  1067 
A 
1068 
 

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

1070 
*) 

0  1071 

6928  1072 
local 
1073 

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

1076 

6928  1077 
fun prt_typing sg_ref t T = 
1078 
let val sg = Sign.deref sg_ref in 

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

1080 
end; 

1081 

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

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

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

1087 
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

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

1091 
Pretty.fbrk, prt_typing sign_ref_merged t T, 

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

0  1093 
end; 
1094 

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

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

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

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

6928  1099 
in 
1100 

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

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

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

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

1106 
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

1107 
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

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

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

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

1112 
(Thm{sign_ref = newsign_ref, 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

1113 
der = infer_derivs (Instantiate(vcTs,ctpairs), [der]), 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

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

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

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]) 

8291  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)} 
8291  1171 
in nodup_vars thm "varifyT" end 
1172 
(* this nodup_vars check can be removed if thms are guaranteed not to contain 

1173 
duplicate TVars with different 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 

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

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

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

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

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

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

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

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

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

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

1232 

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

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

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

1239 
(Thm{sign_ref = sign_ref, 
2386  1240 
der = infer_derivs (Assumption (i, Some env), [der]), 
1241 
maxidx = maxidx, 

1242 
shyps = [], 

1243 
hyps = hyps, 

1244 
prop = 

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

1246 
Logic.rule_of (tpairs, Bs, C) 

1247 
else (*normalize the new rule fully*) 

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

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

1251 
(Seq.mapp newth 

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

1252 
(Unify.unifiers(Sign.deref sign_ref,Envir.empty maxidx, (t,u)::tpairs)) 
250  1253 
(addprfs apairs))) 
0  1254 
in addprfs (Logic.assum_pairs Bi) end; 
1255 

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

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

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

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

1263 
(Thm{sign_ref = sign_ref, 
2386  1264 
der = infer_derivs (Assumption (i,None), [der]), 
1265 
maxidx = maxidx, 

1266 
shyps = [], 

1267 
hyps = hyps, 

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

0  1269 
else raise THM("eq_assumption", 0, [state]) 
1270 
end; 

1271 

1272 

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

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

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

1277 
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

1278 
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

1279 
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

1280 
and concl = Logic.strip_imp_concl rest 
2671  1281 
val n = length asms 
1282 
fun rot m = if 0=m orelse m=n then Bi 

1283 
else if 0<m andalso m<n 

1284 
then list_all 

1285 
(params, 

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

1287 
List.take(asms, m), 

1288 
concl)) 

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

1289 
else raise THM("rotate_rule", k, [state]) 
7264  1290 
in (*no fix_shyps*) 
1291 
Thm{sign_ref = sign_ref, 

2671  1292 
der = infer_derivs (Rotate_rule (k,i), [der]), 
1293 
maxidx = maxidx, 

1294 
shyps = shyps, 

1295 
hyps = hyps, 

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

1297 
end; 

1298 

1299 

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

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

1301 
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

1302 
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

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

1304 
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

1305 
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

1306 
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

1307 
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

1308 
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

1309 
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

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

1311 
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

1312 
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

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

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

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

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

1317 
else raise THM("permute_prems:k", k, [rl]) 
7264  1318 
in (*no fix_shyps*) 
1319 
Thm{sign_ref = sign_ref, 

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

1320 
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

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

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

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

1324 
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

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

1326 

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

1327 

0  1328 
(** User renaming of parameters in a subgoal **) 
1329 

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

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

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

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

1334 
fun rename_params_rule (cs, i) state = 

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

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

1338 
val short = length iparams  length cs 

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

1341 
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

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

1346 
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

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

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

1349 
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

1350 
state) 
1220  1351 
 [] => fix_shyps [state] [] 