author  wenzelm 
Mon, 09 Nov 1998 15:42:08 +0100  
changeset 5840  e2d2b896c717 
parent 5624  4813dd0fe6e5 
child 6089  4d2d5556b4f9 
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 

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

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

16 
val ctyp_of : Sign.sg > typ > ctyp 

17 
val read_ctyp : Sign.sg > string > ctyp 

1160  18 

19 
(*certified terms*) 

20 
type cterm 

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

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

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

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

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

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

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

32 
val capply : cterm > cterm > cterm 
1517  33 
val cabs : cterm > cterm > cterm 
1238  34 
val read_def_cterm : 
1160  35 
Sign.sg * (indexname > typ option) * (indexname > sort option) > 
36 
string list > bool > string * typ > cterm * (indexname * typ) list 

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

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

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

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

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

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

43 
datatype deriv_kind = MinDeriv  ThmDeriv  FullDeriv; 
2386  44 
val keep_derivs : deriv_kind ref 
1529  45 
datatype rule = 
2386  46 
MinProof 
4999  47 
 Oracle of string * Sign.sg * Object.T 
4182  48 
 Axiom of string 
2671  49 
 Theorem of string 
50 
 Assume of cterm 

51 
 Implies_intr of cterm 

1529  52 
 Implies_intr_shyps 
53 
 Implies_intr_hyps 

54 
 Implies_elim 

2671  55 
 Forall_intr of cterm 
56 
 Forall_elim of cterm 

57 
 Reflexive of cterm 

1529  58 
 Symmetric 
59 
 Transitive 

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

65 
 Equal_elim 

2671  66 
 Trivial of cterm 
67 
 Lift_rule of cterm * int 

68 
 Assumption of int * Envir.env option 

69 
 Rotate_rule of int * int 

70 
 Instantiate of (indexname * ctyp) list * (cterm * cterm) list 

71 
 Bicompose of bool * bool * int * int * Envir.env 

72 
 Flexflex_rule of Envir.env 

4182  73 
 Class_triv of class 
1529  74 
 VarifyT 
75 
 FreezeT 

2671  76 
 RewriteC of cterm 
77 
 CongC of cterm 

78 
 Rewrite_cterm of cterm 

79 
 Rename_params_rule of string list * int; 

1529  80 

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

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

1160  83 
(*meta theorems*) 
84 
type thm 

85 
exception THM of string * int * thm list 

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

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

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

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

98 
val nprems_of : thm > int 

99 
val concl_of : thm > term 

100 
val cprop_of : thm > cterm 

101 
val extra_shyps : thm > sort list 

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

3812  105 
val get_axiom : theory > xstring > thm 
4847  106 
val get_def : theory > xstring > thm 
1597
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

107 
val name_thm : string * thm > thm 
4018  108 
val name_of_thm : thm > string 
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 

121 
val beta_conversion : cterm > thm 

122 
val extensional : thm > thm 

123 
val abstract_rule : string > cterm > thm > thm 

124 
val combination : thm > thm > thm 

125 
val equal_intr : thm > thm > thm 

126 
val equal_elim : thm > thm > thm 

127 
val implies_intr_hyps : thm > thm 

4270  128 
val flexflex_rule : thm > thm Seq.seq 
1238  129 
val instantiate : 
1160  130 
(indexname * ctyp) list * (cterm * cterm) list > thm > thm 
1238  131 
val trivial : cterm > thm 
132 
val class_triv : theory > class > thm 

133 
val varifyT : thm > thm 

134 
val freezeT : thm > thm 

135 
val dest_state : thm * int > 

1160  136 
(term * term) list * term list * term * term 
1238  137 
val lift_rule : (thm * int) > thm > thm 
4270  138 
val assumption : int > thm > thm Seq.seq 
1238  139 
val eq_assumption : int > thm > thm 
2671  140 
val rotate_rule : int > int > thm > thm 
1160  141 
val rename_params_rule: string list * int > thm > thm 
1238  142 
val bicompose : bool > bool * thm * int > 
4270  143 
int > thm > thm Seq.seq 
1238  144 
val biresolution : bool > (bool * thm) list > 
4270  145 
int > thm > thm Seq.seq 
1160  146 

147 
(*meta simplification*) 

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

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

156 
val mss_of : thm list > meta_simpset 

157 
val add_congs : meta_simpset * thm list > meta_simpset 

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

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

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

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

164 
> meta_simpset 
1238  165 
val add_prems : meta_simpset * thm list > meta_simpset 
166 
val prems_of_mss : meta_simpset > thm list 

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

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

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

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

3550  178 
structure Thm: THM = 
0  179 
struct 
250  180 

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

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

182 

250  183 
(** certified types **) 
184 

185 
(*certified typs under a signature*) 

186 

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

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

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

189 
fun rep_ctyp (Ctyp {sign_ref, T}) = {sign = Sign.deref sign_ref, T = T}; 
250  190 
fun typ_of (Ctyp {T, ...}) = T; 
191 

192 
fun ctyp_of sign T = 

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

193 
Ctyp {sign_ref = Sign.self_ref sign, T = Sign.certify_typ sign T}; 
250  194 

195 
fun read_ctyp sign s = 

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

196 
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

197 

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

198 

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

199 

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

201 

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

203 

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

204 
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

205 

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

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

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

208 

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

211 
maxidx = maxidx}; 

212 

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

214 

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

215 
fun ctyp_of_term (Cterm {sign_ref, T, ...}) = Ctyp {sign_ref = sign_ref, T = T}; 
2671  216 

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

219 
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

220 
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

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

222 

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

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

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

225 

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

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

227 

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

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

229 
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

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

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

232 
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

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

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

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

236 
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

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

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

239 

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

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

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

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

243 
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

244 
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

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

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

247 

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

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

251 
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

252 

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

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

254 
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

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

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

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

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

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

261 
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

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

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

266 

2509  267 

268 

574  269 
(** read cterms **) (*exception ERROR*) 
250  270 

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

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

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

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

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

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

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

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

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

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

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

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

285 

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

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

287 
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

288 
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

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

290 

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

291 
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

292 

250  293 

294 

1529  295 
(*** Derivations ***) 
296 

297 
(*Names of rules in derivations. Includes logically trivial rules, if 

298 
executed in ML.*) 

299 
datatype rule = 

2386  300 
MinProof (*for building minimal proof terms*) 
4999  301 
 Oracle of string * Sign.sg * Object.T (*oracles*) 
1529  302 
(*Axioms/theorems*) 
4182  303 
 Axiom of string 
2386  304 
 Theorem of string 
1529  305 
(*primitive inferences and compound versions of them*) 
2386  306 
 Assume of cterm 
307 
 Implies_intr of cterm 

1529  308 
 Implies_intr_shyps 
309 
 Implies_intr_hyps 

310 
 Implies_elim 

2386  311 
 Forall_intr of cterm 
312 
 Forall_elim of cterm 

313 
 Reflexive of cterm 

1529  314 
 Symmetric 
315 
 Transitive 

2386  316 
 Beta_conversion of cterm 
1529  317 
 Extensional 
2386  318 
 Abstract_rule of string * cterm 
1529  319 
 Combination 
320 
 Equal_intr 

321 
 Equal_elim 

322 
(*derived rules for tactical proof*) 

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

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

326 
 Lift_rule of cterm * int 

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

2671  328 
 Rotate_rule of int * int 
2386  329 
 Instantiate of (indexname * ctyp) list * (cterm * cterm) list 
330 
 Bicompose of bool * bool * int * int * Envir.env 

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

1529  332 
(*other derived rules*) 
4182  333 
 Class_triv of class 
1529  334 
 VarifyT 
335 
 FreezeT 

336 
(*for the simplifier*) 

2386  337 
 RewriteC of cterm 
338 
 CongC of cterm 

339 
 Rewrite_cterm of cterm 

1529  340 
(*Logical identities, recorded since they are part of the proof process*) 
2386  341 
 Rename_params_rule of string list * int; 
1529  342 

343 

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

344 
type deriv = rule mtree; 
1529  345 

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

346 
datatype deriv_kind = MinDeriv  ThmDeriv  FullDeriv; 
1529  347 

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

348 
val keep_derivs = ref MinDeriv; 
1529  349 

350 

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

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

352 
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

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

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

355 
(case der of 
2386  356 
Join (Oracle _, _) => der :: squash_derivs ders 
357 
 Join (Theorem _, [der']) => if !keep_derivs=ThmDeriv 

358 
then der :: squash_derivs ders 

359 
else squash_derivs (der'::ders) 

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

361 
then der :: squash_derivs ders 

362 
else squash_derivs ders 

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

364 
 _ => der :: squash_derivs ders); 

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

365 

1529  366 

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

368 
val min_infer = Join (MinProof, []); 
1529  369 

370 
(*Make a minimal inference*) 

371 
fun make_min_infer [] = min_infer 

372 
 make_min_infer [der] = der 

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

373 
 make_min_infer ders = Join (MinProof, ders); 
1529  374 

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

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

377 
if !keep_derivs=FullDeriv then Join (rl, ders) 
1529  378 
else make_min_infer (squash_derivs ders); 
379 

380 

2509  381 

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

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

383 

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

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

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

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

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

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

390 
prop: term}; (*conclusion*) 
0  391 

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

392 
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

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

394 
shyps = shyps, hyps = hyps, prop = prop}; 
0  395 

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

397 
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

398 
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

399 
in {sign = Sign.deref sign_ref, der = der, maxidx = maxidx, shyps = shyps, 
1529  400 
hyps = map (ctermf ~1) hyps, 
401 
prop = ctermf maxidx prop} 

1517  402 
end; 
403 

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

404 
(*errors involving theorems*) 
0  405 
exception THM of string * int * thm list; 
406 

3994  407 
(*equality of theorems uses equality of signatures and the 
408 
aconvertible test for terms*) 

409 
fun eq_thm (th1, th2) = 

410 
let 

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

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

413 
in 

414 
Sign.eq_sg (sg1, sg2) andalso 

415 
eq_set_sort (shyps1, shyps2) andalso 

416 
aconvs (hyps1, hyps2) andalso 

417 
prop1 aconv prop2 

418 
end; 

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

419 

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

420 
fun sign_of_thm (Thm {sign_ref, ...}) = Sign.deref sign_ref; 
0  421 

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

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

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

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

425 
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

426 

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

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

430 
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

431 
val sign = Sign.deref sign_ref; 
3895  432 
in 
4254  433 
if Sign.eq_sg (sign, sign') then thm 
434 
else if Sign.subsig (sign, sign') then 

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

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

438 
end; 

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

439 

4254  440 
val transfer = transfer_sg o sign_of; 
441 

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

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

443 
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

444 

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

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

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

447 
Logic.strip_imp_prems (Logic.skip_flexpairs prop); 
0  448 

449 
(*counts premises in a rule*) 

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

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

451 
Logic.count_prems (Logic.skip_flexpairs prop, 0); 
0  452 

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

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

454 
fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop; 
0  455 

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

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

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

458 
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

459 

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

460 

0  461 

1238  462 
(** sort contexts of theorems **) 
463 

464 
(* basic utils *) 

465 

2163  466 
(*accumulate sorts suppressing duplicates; these are coded low levelly 
1238  467 
to improve efficiency a bit*) 
468 

469 
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

470 
 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

471 
 add_typ_sorts (TVar (_, S), Ss) = ins_sort(S,Ss) 
1238  472 
and add_typs_sorts ([], Ss) = Ss 
473 
 add_typs_sorts (T :: Ts, Ss) = add_typs_sorts (Ts, add_typ_sorts (T, Ss)); 

474 

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

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

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

478 
 add_term_sorts (Bound _, Ss) = Ss 

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

479 
 add_term_sorts (Abs (_,T,t), Ss) = add_term_sorts (t, add_typ_sorts (T,Ss)) 
1238  480 
 add_term_sorts (t $ u, Ss) = add_term_sorts (t, add_term_sorts (u, Ss)); 
481 

482 
fun add_terms_sorts ([], Ss) = Ss 

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

483 
 add_terms_sorts (t::ts, Ss) = add_terms_sorts (ts, add_term_sorts (t,Ss)); 
1238  484 

1258  485 
fun env_codT (Envir.Envir {iTs, ...}) = map snd iTs; 
486 

487 
fun add_env_sorts (env, Ss) = 

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

489 
add_typs_sorts (env_codT env, Ss)); 

490 

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

493 

494 
fun add_thms_shyps ([], Ss) = Ss 

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

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

496 
add_thms_shyps (ths, union_sort(shyps,Ss)); 
1238  497 

498 

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

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

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

502 

503 

504 
(* fix_shyps *) 

505 

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

507 
fun fix_shyps thms Ts thm = 

508 
let 

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

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

512 
in 

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

513 
Thm {sign_ref = sign_ref, 
2386  514 
der = der, (*No new derivation, as other rules call this*) 
515 
maxidx = maxidx, 

516 
shyps = shyps, hyps = hyps, prop = prop} 

1238  517 
end; 
518 

519 

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

521 

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

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

525 
fun strip_shyps thm = 

526 
let 

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

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

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

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

532 
Thm {sign_ref = sign_ref, der = der, maxidx = maxidx, 
2386  533 
shyps = 
534 
(if eq_set_sort (shyps',sorts) orelse 

535 
not (!force_strip_shyps) then shyps' 

3061  536 
else (* FIXME tmp (since 1995/08/01) *) 
2386  537 
(warning ("Removed sort hypotheses: " ^ 
2962  538 
commas (map Sorts.str_of_sort (shyps' \\ sorts))); 
2386  539 
warning "Let's hope these sorts are nonempty!"; 
1238  540 
sorts)), 
1529  541 
hyps = hyps, 
542 
prop = prop} 

1238  543 
end; 
544 

545 

546 
(* implies_intr_shyps *) 

547 

548 
(*discharge all extra sort hypotheses*) 

549 
fun implies_intr_shyps thm = 

550 
(case extra_shyps thm of 

551 
[] => thm 

552 
 xshyps => 

553 
let 

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

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

555 
val shyps' = ins_sort (logicS, shyps \\ xshyps); 
1238  556 
val used_names = foldr add_term_tfree_names (prop :: hyps, []); 
557 
val names = 

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

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

560 

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

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

564 
Thm {sign_ref = sign_ref, 
2386  565 
der = infer_derivs (Implies_intr_shyps, [der]), 
566 
maxidx = maxidx, 

567 
shyps = shyps', 

568 
hyps = hyps, 

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

1238  570 
end); 
571 

572 

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

574 

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

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

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

580 
fun get_ax [] = None 

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

584 
Some t => 

585 
Some (fix_shyps [] [] 

586 
(Thm {sign_ref = Sign.self_ref sign, 

587 
der = infer_derivs (Axiom name, []), 

588 
maxidx = maxidx_of_term t, 

589 
shyps = [], 

590 
hyps = [], 

591 
prop = t})) 

592 
 None => get_ax thys) 

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

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

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

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

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

599 

4847  600 
fun get_def thy name = get_axiom thy (name ^ "_def"); 
601 

1529  602 

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

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

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

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

607 

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

608 
(*Attach a label to a theorem to make proof objects more readable*) 
4018  609 
fun name_thm (name, th as Thm {sign_ref, der, maxidx, shyps, hyps, prop}) = 
610 
(case der of 

611 
Join (Theorem _, _) => th 

612 
 Join (Axiom _, _) => th 

613 
 _ => Thm {sign_ref = sign_ref, der = Join (Theorem name, [der]), 

614 
maxidx = maxidx, shyps = shyps, hyps = hyps, prop = prop}); 

615 

616 
fun name_of_thm (Thm {der, ...}) = 

617 
(case der of 

618 
Join (Theorem name, _) => name 

4182  619 
 Join (Axiom name, _) => name 
4018  620 
 _ => ""); 
0  621 

622 

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

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

625 
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

626 
Thm {sign_ref = sign_ref, 
2386  627 
der = der, (*No derivation recorded!*) 
628 
maxidx = maxidx, 

629 
shyps = shyps, 

630 
hyps = map Term.compress_term hyps, 

631 
prop = Term.compress_term prop}; 

564  632 

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

633 

2509  634 

1529  635 
(*** Meta rules ***) 
0  636 

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

639 
recurrence.*) 

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

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

642 
Thm {sign_ref = sign_ref, 
2386  643 
der = der, 
644 
maxidx = maxidx_of_term prop, 

645 
shyps = shyps, 

646 
hyps = hyps, 

647 
prop = prop}) 

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

649 

1220  650 
(** 'primitive' rules **) 
651 

652 
(*discharge all assumptions t from ts*) 

0  653 
val disch = gen_rem (op aconv); 
654 

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

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

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

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

663 
else Thm{sign_ref = sign_ref, 
5344  664 
der = infer_derivs (Assume ct, []), 
2386  665 
maxidx = ~1, 
666 
shyps = add_term_sorts(prop,[]), 

667 
hyps = [prop], 

668 
prop = prop} 

0  669 
end; 
670 

1220  671 
(*Implication introduction 
3529  672 
[A] 
673 
: 

674 
B 

1220  675 
 
676 
A ==> B 

677 
*) 

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

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

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

683 
(Thm{sign_ref = Sign.merge_refs (sign_ref,sign_refA), 
2386  684 
der = infer_derivs (Implies_intr cA, [der]), 
685 
maxidx = Int.max(maxidxA, maxidx), 

686 
shyps = [], 

687 
hyps = disch(hyps,A), 

688 
prop = implies$A$prop}) 

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

691 
end; 

692 

1529  693 

1220  694 
(*Implication elimination 
695 
A ==> B A 

696 
 

697 
B 

698 
*) 

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

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

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

707 
(Thm{sign_ref= merge_thm_sgs(thAB,thA), 
2386  708 
der = infer_derivs (Implies_elim, [der,derA]), 
709 
maxidx = Int.max(maxA,maxidx), 

710 
shyps = [], 

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

712 
prop = B}) 

250  713 
else err("major premise") 
714 
 _ => err("major premise") 

0  715 
end; 
250  716 

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

719 
 

720 
!!x.A 

721 
*) 

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

722 
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

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

725 
(Thm{sign_ref = sign_ref, 
2386  726 
der = infer_derivs (Forall_intr cx, [der]), 
727 
maxidx = maxidx, 

728 
shyps = [], 

729 
hyps = hyps, 

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

0  731 
in case x of 
250  732 
Free(a,T) => 
733 
if exists (apl(x, Logic.occs)) hyps 

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

735 
else result(a,T) 

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

738 
end; 

739 

1220  740 
(*Forall elimination 
741 
!!x.A 

742 
 

743 
A[t/x] 

744 
*) 

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

745 
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

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

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

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

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

752 
(Thm{sign_ref= Sign.merge_refs(sign_ref,sign_reft), 
2386  753 
der = infer_derivs (Forall_elim ct, [der]), 
754 
maxidx = Int.max(maxidx, maxt), 

755 
shyps = [], 

756 
hyps = hyps, 

757 
prop = betapply(A,t)}) 

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

759 
then nodup_Vars thm "forall_elim" 

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

761 
end 

2147  762 
 _ => raise THM("forall_elim: not quantified", 0, [th]) 
0  763 
end 
764 
handle TERM _ => 

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

767 

1220  768 
(* Equality *) 
0  769 

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

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

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

774 
(Thm{sign_ref= sign_ref, 
2386  775 
der = infer_derivs (Reflexive ct, []), 
776 
shyps = [], 

777 
hyps = [], 

778 
maxidx = maxidx, 

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

0  780 
end; 
781 

782 
(*The symmetry rule 

1220  783 
t==u 
784 
 

785 
u==t 

786 
*) 

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

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

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

791 
Thm{sign_ref = sign_ref, 
2386  792 
der = infer_derivs (Symmetric, [der]), 
793 
maxidx = maxidx, 

794 
shyps = shyps, 

795 
hyps = hyps, 

796 
prop = eq$u$t} 

0  797 
 _ => raise THM("symmetric", 0, [th]); 
798 

799 
(*The transitive rule 

1220  800 
t1==u u==t2 
801 
 

802 
t1==t2 

803 
*) 

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

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

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

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

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

813 
(Thm{sign_ref= merge_thm_sgs(th1,th2), 
2386  814 
der = infer_derivs (Transitive, [der1, der2]), 
2147  815 
maxidx = Int.max(max1,max2), 
2386  816 
shyps = [], 
817 
hyps = union_term(hyps1,hyps2), 

818 
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

819 
in if max1 >= 0 andalso max2 >= 0 
2147  820 
then nodup_Vars thm "transitive" 
821 
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

822 
end 
0  823 
 _ => err"premises" 
824 
end; 

825 

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

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

831 
(Thm{sign_ref = sign_ref, 
2386  832 
der = infer_derivs (Beta_conversion ct, []), 
833 
maxidx = maxidx, 

834 
shyps = [], 

835 
hyps = [], 

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

250  837 
 _ => raise THM("beta_conversion: not a redex", 0, []) 
0  838 
end; 
839 

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

1220  841 
f(x) == g(x) 
842 
 

843 
f == g 

844 
*) 

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

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

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

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

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

854 
 Var _ => 

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

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

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

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

859 
Thm{sign_ref = sign_ref, 
2386  860 
der = infer_derivs (Extensional, [der]), 
861 
maxidx = maxidx, 

862 
shyps = shyps, 

863 
hyps = hyps, 

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

867 

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

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

1220  870 
t == u 
871 
 

872 
%x.t == %x.u 

873 
*) 

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

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

875 
let val x = term_of cx; 
250  876 
val (t,u) = Logic.dest_equals prop 
877 
handle TERM _ => 

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

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

880 
(Thm{sign_ref = sign_ref, 
2386  881 
der = infer_derivs (Abstract_rule (a,cx), [der]), 
882 
maxidx = maxidx, 

883 
shyps = [], 

884 
hyps = hyps, 

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

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

0  887 
in case x of 
250  888 
Free(_,T) => 
889 
if exists (apl(x, Logic.occs)) hyps 

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

891 
else result T 

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

894 
end; 

895 

896 
(*The combination rule 

3529  897 
f == g t == u 
898 
 

899 
f(t) == g(u) 

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

906 
fun chktypes (f,t) = 
2386  907 
(case fastype_of f of 
908 
Type("fun",[T1,T2]) => 

909 
if T1 <> fastype_of t then 

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

911 
else () 

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

913 
[th1,th2])) 

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

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

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

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

921 
shyps = union_sort(shyps1,shyps2), 

922 
hyps = union_term(hyps1,hyps2), 

923 
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

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

925 
then nodup_Vars thm "combination" 
2386  926 
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

927 
end 
0  928 
 _ => raise THM("combination: premises", 0, [th1,th2]) 
929 
end; 

930 

931 

932 
(* Equality introduction 

3529  933 
A ==> B B ==> A 
934 
 

935 
A == B 

1220  936 
*) 
0  937 
fun equal_intr th1 th2 = 
1529  938 
let val Thm{der=der1,maxidx=max1, shyps=shyps1, hyps=hyps1, 
2386  939 
prop=prop1,...} = th1 
1529  940 
and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, 
2386  941 
prop=prop2,...} = th2; 
1529  942 
fun err(msg) = raise THM("equal_intr: "^msg, 0, [th1,th2]) 
943 
in case (prop1,prop2) of 

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

2386  945 
if A aconv A' andalso B aconv B' 
946 
then 

947 
(*no fix_shyps*) 

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

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

951 
shyps = union_sort(shyps1,shyps2), 

952 
hyps = union_term(hyps1,hyps2), 

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

954 
else err"not equal" 

1529  955 
 _ => err"premises" 
956 
end; 

957 

958 

959 
(*The equal propositions rule 

3529  960 
A == B A 
1529  961 
 
962 
B 

963 
*) 

964 
fun equal_elim th1 th2 = 

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

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

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

968 
in case prop1 of 

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

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

971 
fix_shyps [th1, th2] [] 

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

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

975 
shyps = [], 

976 
hyps = union_term(hyps1,hyps2), 

977 
prop = B}) 

1529  978 
 _ => err"major premise" 
979 
end; 

0  980 

1220  981 

982 

0  983 
(**** Derived rules ****) 
984 

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

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

989 
(Thm{sign_ref = sign_ref, 
2386  990 
der = infer_derivs (Implies_intr_hyps, [der]), 
991 
maxidx = maxidx, 

992 
shyps = shyps, 

1529  993 
hyps = disch(As,A), 
2386  994 
prop = implies$A$prop}) 
0  995 
 implies_intr_hyps th = th; 
996 

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

250  998 
Instantiates the theorem and deletes trivial tpairs. 
0  999 
Resulting sequence may contain multiple elements if the tpairs are 
1000 
not all flexflex. *) 

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

1001 
fun flexflex_rule (th as Thm{sign_ref, der, maxidx, hyps, prop,...}) = 
250  1002 
let fun newthm env = 
1529  1003 
if Envir.is_empty env then th 
1004 
else 

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

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

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

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

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

1011 
(Thm{sign_ref = sign_ref, 
2386  1012 
der = infer_derivs (Flexflex_rule env, [der]), 
1013 
maxidx = maxidx_of_term newprop, 

1014 
shyps = [], 

1015 
hyps = hyps, 

1016 
prop = newprop}) 

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

1020 
(Unify.smash_unifiers(Sign.deref sign_ref, Envir.empty maxidx, tpairs)) 
0  1021 
end; 
1022 

1023 
(*Instantiation of Vars 

1220  1024 
A 
1025 
 

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

1027 
*) 

0  1028 

1029 
(*Check that all the terms are Vars and are distinct*) 

1030 
fun instl_ok ts = forall is_Var ts andalso null(findrep ts); 

1031 

1032 
(*For instantiate: process pair of cterms, merge theories*) 

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

1033 
fun add_ctpair ((ct,cu), (sign_ref,tpairs)) = 
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

1034 
let val Cterm {sign_ref=sign_reft, t=t, T= T, ...} = ct 
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

1035 
and Cterm {sign_ref=sign_refu, t=u, T= U, ...} = cu 
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

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

1037 
if T=U then 
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

1038 
(Sign.merge_refs (sign_ref, Sign.merge_refs (sign_reft, sign_refu)), (t,u)::tpairs) 
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

1039 
else raise TYPE("add_ctpair", [T,U], [t,u]) 
0  1040 
end; 
1041 

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

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

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

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

1046 
(*Lefttoright replacements: ctpairs = [...,(vi,ti),...]. 

1047 
Instantiates distinct Vars by terms of same type. 

1048 
Normalizes the new theorem! *) 

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

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

1051 
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

1052 
val (newsign_ref,vTs) = foldr add_ctyp (vcTs, (newsign_ref,[])); 
250  1053 
val newprop = 
1054 
Envir.norm_term (Envir.empty 0) 

1055 
(subst_atomic tpairs 

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

1056 
(Type.inst_term_tvars(Sign.tsig_of (Sign.deref newsign_ref),vTs) prop)) 
1220  1057 
val newth = 
1058 
fix_shyps [th] (map snd vTs) 

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

1059 
(Thm{sign_ref = newsign_ref, 
2386  1060 
der = infer_derivs (Instantiate(vcTs,ctpairs), [der]), 
1061 
maxidx = maxidx_of_term newprop, 

1062 
shyps = [], 

1063 
hyps = hyps, 

1064 
prop = newprop}) 

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

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

2147  1069 
else nodup_Vars newth "instantiate" 
0  1070 
end 
250  1071 
handle TERM _ => 
0  1072 
raise THM("instantiate: incompatible signatures",0,[th]) 
2671  1073 
 TYPE (msg,_,_) => raise THM("instantiate: type conflict: " ^ msg, 
1074 
0, [th]); 

0  1075 

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

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

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

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

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

1083 
(Thm{sign_ref = sign_ref, 
2386  1084 
der = infer_derivs (Trivial ct, []), 
1085 
maxidx = maxidx, 

1086 
shyps = [], 

1087 
hyps = [], 

1088 
prop = implies$A$A}) 

0  1089 
end; 
1090 

1503  1091 
(*Axiomscheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" *) 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

1092 
fun class_triv thy c = 
1529  1093 
let val sign = sign_of thy; 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

1094 
val Cterm {sign_ref, t, maxidx, ...} = 
2386  1095 
cterm_of sign (Logic.mk_inclass (TVar (("'a", 0), [c]), c)) 
1096 
handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []); 

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

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

1099 
(Thm {sign_ref = sign_ref, 
4182  1100 
der = infer_derivs (Class_triv c, []), 
2386  1101 
maxidx = maxidx, 
1102 
shyps = [], 

1103 
hyps = [], 

1104 
prop = t}) 

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

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

1106 

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

1107 

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

1109 
fun varifyT(Thm{sign_ref,der,maxidx,shyps,hyps,prop}) = 
0  1110 
let val tfrees = foldr add_term_tfree_names (hyps,[]) 
1634  1111 
in let val thm = (*no fix_shyps*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

1112 
Thm{sign_ref = sign_ref, 
2386  1113 
der = infer_derivs (VarifyT, [der]), 
1114 
maxidx = Int.max(0,maxidx), 

1115 
shyps = shyps, 

1116 
hyps = hyps, 

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

0  1121 
end; 
1122 

1123 
(* Replace all TVars by new TFrees *) 

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

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

1127 
Thm{sign_ref = sign_ref, 
2386  1128 
der = infer_derivs (FreezeT, [der]), 
1129 
maxidx = maxidx_of_term prop', 

1130 
shyps = shyps, 

1131 
hyps = hyps, 

1529  1132 
prop = prop'} 
1220  1133 
end; 
0  1134 

1135 

1136 
(*** Inference rules for tactics ***) 

1137 

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

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

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

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

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

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

1144 
end 

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

1146 

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

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

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

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

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

1158 
Thm{sign_ref = merge_thm_sgs(state,orule), 
2386  1159 
der = infer_derivs (Lift_rule(ct_Bi, i), [der]), 
1160 
maxidx = maxidx+smax+1, 

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

1161 
shyps=union_sort(sshyps,shyps), 
2386  1162 
hyps=hyps, 
1529  1163 
prop = Logic.rule_of (map (pairself lift_abs) tpairs, 
2386  1164 
map lift_all As, 
1165 
lift_all B)} 

0  1166 
end; 
1167 

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

1169 
fun assumption i state = 

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

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

1174 
(Thm{sign_ref = sign_ref, 
2386  1175 
der = infer_derivs (Assumption (i, Some env), [der]), 
1176 
maxidx = maxidx, 

1177 
shyps = [], 

1178 
hyps = hyps, 

1179 
prop = 

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

1181 
Logic.rule_of (tpairs, Bs, C) 

1182 
else (*normalize the new rule fully*) 

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

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

1186 
(Seq.mapp newth 

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

1187 
(Unify.unifiers(Sign.deref sign_ref,Envir.empty maxidx, (t,u)::tpairs)) 
250  1188 
(addprfs apairs))) 
0  1189 
in addprfs (Logic.assum_pairs Bi) end; 
1190 

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

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

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

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

1198 
(Thm{sign_ref = sign_ref, 
2386  1199 
der = infer_derivs (Assumption (i,None), [der]), 
1200 
maxidx = maxidx, 

1201 
shyps = [], 

1202 
hyps = hyps, 

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

0  1204 
else raise THM("eq_assumption", 0, [state]) 
1205 
end; 

1206 

1207 

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

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

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

1213 
and asms = Logic.strip_assums_hyp Bi 

1214 
and concl = Logic.strip_assums_concl Bi 

1215 
val n = length asms 

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

1217 
else if 0<m andalso m<n 

1218 
then list_all 

1219 
(params, 

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

1221 
List.take(asms, m), 

1222 
concl)) 

1223 
else raise THM("rotate_rule", m, [state]) 

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

1224 
in Thm{sign_ref = sign_ref, 
2671  1225 
der = infer_derivs (Rotate_rule (k,i), [der]), 
1226 
maxidx = maxidx, 

1227 
shyps = shyps, 

1228 
hyps = hyps, 

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

1230 
end; 

1231 

1232 

0  1233 
(** User renaming of parameters in a subgoal **) 
1234 

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

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

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

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

1239 
fun rename_params_rule (cs, i) state = 

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

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

1243 
val short = length iparams  length cs 

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

1246 
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

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

1251 
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

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

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

1254 
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

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

1257 
(Thm{sign_ref = sign_ref, 
2386  1258 
der = infer_derivs (Rename_params_rule(cs,i), [der]), 
1259 
maxidx = maxidx, 

1260 
shyps = [], 

1261 
hyps = hyps, 

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

0  1263 
end; 
1264 

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

1266 

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

1270 
match_bvs(s, t, if x="" orelse y="" then al 
1238  1271 
else (x,y)::al) 
0  1272 
 match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al)) 
1273 
 match_bvs(_,_,al) = al; 

1274 

1275 
(* strip abstractions created by parameters *) 

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

1277 

1278 

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

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

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

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

1286 
 strip(A,_) = f A 

0  1287 
in strip end; 
1288 

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

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

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

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

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

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

1296 
(*unknowns appearing elsewhere be preserved!*) 

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

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

1299 
(case assoc(al,x) of 

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

1300 
Some(y) => if x mem_string vids orelse y mem_string vids then t 
250  1301 
else Var((y,i),T) 
1302 
 None=> t) 

0  1303 
 rename(Abs(x,T,t)) = 
1576
af8f43f742a0
Added some optimized versions of functions dealing with sets
berghofe
parents:
1569
diff
changeset

1304 
Abs(case assoc_string(al,x) of Some(y) => y  None => x, 
250  1305 
T, rename t) 
0  1306 
 rename(f$t) = rename f $ rename t 
1307 
 rename(t) = t; 

250  1308 
fun strip_ren Ai = strip_apply rename (Ai,B) 
0  1309 
in strip_ren end; 
1310 

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

1312 
fun rename_bvars(dpairs, tpairs, B) = 

250  1313 
rename_bvs(foldr match_bvars (dpairs,[]), dpairs, tpairs, B); 
0  1314 

1315 

1316 
(*** RESOLUTION ***) 

1317 

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

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

1319 

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

250  1322 
fun strip_assums2 (Const("==>", _) $ _ $ B1, 
1323 
Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2) 

0  1324 
 strip_assums2 (Const("all",_)$Abs(a,T,t1), 
250  1325 
Const("all",_)$Abs(_,_,t2)) = 
0  1326 
let val (B1,B2) = strip_assums2 (t1,t2) 
1327 
in (Abs(a,T,B1), Abs(a,T,B2)) end 

1328 
 strip_assums2 BB = BB; 

1329 

1330 

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

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

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

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

1334 
let val Envir.Envir{iTs, ...} = env 
1238  1335 
val T' = typ_subst_TVars iTs T 
1336 
(*Must instantiate types of parameters because they are flattened; 

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

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

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

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

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

1342 

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

1343 

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

1348 
If eres_flg then simultaneously proves A1 by assumption. 

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

4270  1352 
local exception COMPOSE 
0  1353 
in 
250  1354 
fun bicompose_aux match (state, (stpairs, Bs, Bi, C), lifted) 
0  1355 
(eres_flg, orule, nsubgoal) = 
1529  1356 
let val Thm{der=sder, maxidx=smax, shyps=sshyps, hyps=shyps, ...} = state 
1357 
and Thm{der=rder, maxidx=rmax, shyps=rshyps, hyps=rhyps, 

2386  1358 
prop=rprop,...} = orule 
1529  1359 
(*How many hyps to skip over during normalization*) 
1238  1360 
a 