author  nipkow 
Mon, 24 Nov 1997 16:43:43 +0100  
changeset 4281  6c6073b13600 
parent 4270  957c887b89b5 
child 4288  3f5e8c4aa84d 
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} 
1238  23 
val term_of : cterm > term 
24 
val cterm_of : Sign.sg > term > cterm 

2671  25 
val ctyp_of_term : cterm > ctyp 
1238  26 
val read_cterm : Sign.sg > string * typ > cterm 
27 
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

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

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

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

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

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

37 
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

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

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

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

42 
datatype deriv_kind = MinDeriv  ThmDeriv  FullDeriv; 
2386  43 
val keep_derivs : deriv_kind ref 
1529  44 
datatype rule = 
2386  45 
MinProof 
4182  46 
 Oracle of string * Sign.sg * object 
47 
 Axiom of string 

2671  48 
 Theorem of string 
49 
 Assume of cterm 

50 
 Implies_intr of cterm 

1529  51 
 Implies_intr_shyps 
52 
 Implies_intr_hyps 

53 
 Implies_elim 

2671  54 
 Forall_intr of cterm 
55 
 Forall_elim of cterm 

56 
 Reflexive of cterm 

1529  57 
 Symmetric 
58 
 Transitive 

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

64 
 Equal_elim 

2671  65 
 Trivial of cterm 
66 
 Lift_rule of cterm * int 

67 
 Assumption of int * Envir.env option 

68 
 Rotate_rule of int * int 

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

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

71 
 Flexflex_rule of Envir.env 

4182  72 
 Class_triv of class 
1529  73 
 VarifyT 
74 
 FreezeT 

2671  75 
 RewriteC of cterm 
76 
 CongC of cterm 

77 
 Rewrite_cterm of cterm 

78 
 Rename_params_rule of string list * int; 

1529  79 

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

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

1160  82 
(*meta theorems*) 
83 
type thm 

84 
exception THM of string * int * thm list 

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

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

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

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

97 
val nprems_of : thm > int 

98 
val concl_of : thm > term 

99 
val cprop_of : thm > cterm 

100 
val extra_shyps : thm > sort list 

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

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

105 
val name_thm : string * thm > thm 
4018  106 
val name_of_thm : thm > string 
1238  107 
val axioms_of : theory > (string * thm) list 
1160  108 

109 
(*meta rules*) 

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

114 
val forall_intr : cterm > thm > thm 

115 
val forall_elim : cterm > thm > thm 

116 
val reflexive : cterm > thm 

117 
val symmetric : thm > thm 

118 
val transitive : thm > thm > thm 

119 
val beta_conversion : cterm > thm 

120 
val extensional : thm > thm 

121 
val abstract_rule : string > cterm > thm > thm 

122 
val combination : thm > thm > thm 

123 
val equal_intr : thm > thm > thm 

124 
val equal_elim : thm > thm > thm 

125 
val implies_intr_hyps : thm > thm 

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

131 
val varifyT : thm > thm 

132 
val freezeT : thm > thm 

133 
val dest_state : thm * int > 

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

145 
(*meta simplification*) 

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

1238  150 
val empty_mss : meta_simpset 
3550  151 
val merge_mss : meta_simpset * meta_simpset > meta_simpset 
1238  152 
val add_simps : meta_simpset * thm list > meta_simpset 
153 
val del_simps : meta_simpset * thm list > meta_simpset 

154 
val mss_of : thm list > meta_simpset 

155 
val add_congs : meta_simpset * thm list > meta_simpset 

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

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

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

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

162 
> meta_simpset 
1238  163 
val add_prems : meta_simpset * thm list > meta_simpset 
164 
val prems_of_mss : meta_simpset > thm list 

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

166 
val mk_rews_of_mss : meta_simpset > thm > thm list 

2509  167 
val set_termless : meta_simpset * (term * term > bool) > meta_simpset 
1238  168 
val trace_simp : bool ref 
169 
val rewrite_cterm : bool * bool > meta_simpset > 

1529  170 
(meta_simpset > thm > thm option) > cterm > thm 
1539  171 

4124  172 
val invoke_oracle : theory > xstring > Sign.sg * object > thm 
250  173 
end; 
0  174 

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

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

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

179 

250  180 
(** certified types **) 
181 

182 
(*certified typs under a signature*) 

183 

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

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

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

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

189 
fun ctyp_of sign T = 

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

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

192 
fun read_ctyp sign s = 

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.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

194 

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

195 

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

196 

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

198 

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

200 

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

201 
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

202 

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

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

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

205 

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

207 

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

208 
fun ctyp_of_term (Cterm {sign_ref, T, ...}) = Ctyp {sign_ref = sign_ref, T = T}; 
2671  209 

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

212 
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

213 
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

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

215 

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

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

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

218 

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

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

220 

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

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

222 
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

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

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

225 
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

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

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

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

229 
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

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

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

232 

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

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

234 
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

235 
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

236 
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

237 
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

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

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

240 

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

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

244 
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

245 

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

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

247 
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

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

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

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

252 
 capply _ _ = raise CTERM "capply: first arg is not a function" 
250  253 

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

254 
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

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

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

259 

2509  260 

261 

574  262 
(** read cterms **) (*exception ERROR*) 
250  263 

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

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

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

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

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

269 
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

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

271 
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

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

273 
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

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

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

278 

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

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

280 
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

281 
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

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

283 

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

284 
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

285 

1394
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

286 
(*read a list of terms, matching them against a list of expected types. 
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

287 
NO disambiguation of alternative parses via typechecking  it is just 
4281
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

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

289 

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

290 
Why not? In any case, this function is not used at all. 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

291 

3789  292 
fun read_cterms sg (bs, Ts) = 
1394
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

293 
let 
3789  294 
val {tsig, syn, ...} = Sign.rep_sg sg; 
2979  295 
fun read (b, T) = 
296 
(case Syntax.read syn T b of 

297 
[t] => t 

298 
 _ => error ("Error or ambiguity in parsing of " ^ b)); 

299 

3789  300 
val prt = setmp Syntax.show_brackets true (Sign.pretty_term sg); 
301 
val prT = Sign.pretty_typ sg; 

2979  302 
val (us, _) = 
3789  303 
(* FIXME Sign.infer_types!? *) 
304 
Type.infer_types prt prT tsig (Sign.const_type sg) (K None) (K None) 

305 
(Sign.intern_const sg) (Sign.intern_tycons sg) (Sign.intern_sort sg) 

306 
[] true (map (Sign.certify_typ sg) Ts) (ListPair.map read (bs, Ts)); 

307 
in map (cterm_of sg) us end 

2979  308 
handle TYPE (msg, _, _) => error msg 
1394
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

309 
 TERM (msg, _) => error msg; 
4281
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

310 
*) 
250  311 

312 

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

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

316 
executed in ML.*) 

317 
datatype rule = 

2386  318 
MinProof (*for building minimal proof terms*) 
4182  319 
 Oracle of string * Sign.sg * object (*oracles*) 
1529  320 
(*Axioms/theorems*) 
4182  321 
 Axiom of string 
2386  322 
 Theorem of string 
1529  323 
(*primitive inferences and compound versions of them*) 
2386  324 
 Assume of cterm 
325 
 Implies_intr of cterm 

1529  326 
 Implies_intr_shyps 
327 
 Implies_intr_hyps 

328 
 Implies_elim 

2386  329 
 Forall_intr of cterm 
330 
 Forall_elim of cterm 

331 
 Reflexive of cterm 

1529  332 
 Symmetric 
333 
 Transitive 

2386  334 
 Beta_conversion of cterm 
1529  335 
 Extensional 
2386  336 
 Abstract_rule of string * cterm 
1529  337 
 Combination 
338 
 Equal_intr 

339 
 Equal_elim 

340 
(*derived rules for tactical proof*) 

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

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

344 
 Lift_rule of cterm * int 

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

2671  346 
 Rotate_rule of int * int 
2386  347 
 Instantiate of (indexname * ctyp) list * (cterm * cterm) list 
348 
 Bicompose of bool * bool * int * int * Envir.env 

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

1529  350 
(*other derived rules*) 
4182  351 
 Class_triv of class 
1529  352 
 VarifyT 
353 
 FreezeT 

354 
(*for the simplifier*) 

2386  355 
 RewriteC of cterm 
356 
 CongC of cterm 

357 
 Rewrite_cterm of cterm 

1529  358 
(*Logical identities, recorded since they are part of the proof process*) 
2386  359 
 Rename_params_rule of string list * int; 
1529  360 

361 

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

362 
type deriv = rule mtree; 
1529  363 

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

364 
datatype deriv_kind = MinDeriv  ThmDeriv  FullDeriv; 
1529  365 

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

366 
val keep_derivs = ref MinDeriv; 
1529  367 

368 

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

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

370 
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

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

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

373 
(case der of 
2386  374 
Join (Oracle _, _) => der :: squash_derivs ders 
375 
 Join (Theorem _, [der']) => if !keep_derivs=ThmDeriv 

376 
then der :: squash_derivs ders 

377 
else squash_derivs (der'::ders) 

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

379 
then der :: squash_derivs ders 

380 
else squash_derivs ders 

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

382 
 _ => der :: squash_derivs ders); 

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

383 

1529  384 

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

386 
val min_infer = Join (MinProof, []); 
1529  387 

388 
(*Make a minimal inference*) 

389 
fun make_min_infer [] = min_infer 

390 
 make_min_infer [der] = der 

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

391 
 make_min_infer ders = Join (MinProof, ders); 
1529  392 

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

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

395 
if !keep_derivs=FullDeriv then Join (rl, ders) 
1529  396 
else make_min_infer (squash_derivs ders); 
397 

398 

2509  399 

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

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

401 

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

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

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

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

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

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

408 
prop: term}; (*conclusion*) 
0  409 

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

410 
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

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

412 
shyps = shyps, hyps = hyps, prop = prop}; 
0  413 

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

415 
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

416 
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

417 
in {sign = Sign.deref sign_ref, der = der, maxidx = maxidx, shyps = shyps, 
1529  418 
hyps = map (ctermf ~1) hyps, 
419 
prop = ctermf maxidx prop} 

1517  420 
end; 
421 

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

422 
(*errors involving theorems*) 
0  423 
exception THM of string * int * thm list; 
424 

3994  425 
(*equality of theorems uses equality of signatures and the 
426 
aconvertible test for terms*) 

427 
fun eq_thm (th1, th2) = 

428 
let 

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

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

431 
in 

432 
Sign.eq_sg (sg1, sg2) andalso 

433 
eq_set_sort (shyps1, shyps2) andalso 

434 
aconvs (hyps1, hyps2) andalso 

435 
prop1 aconv prop2 

436 
end; 

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

437 

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

438 
fun sign_of_thm (Thm {sign_ref, ...}) = Sign.deref sign_ref; 
0  439 

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

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

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

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

443 
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

444 

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

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

448 
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

449 
val sign = Sign.deref sign_ref; 
3895  450 
in 
4254  451 
if Sign.eq_sg (sign, sign') then thm 
452 
else if Sign.subsig (sign, sign') then 

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

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

456 
end; 

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

457 

4254  458 
val transfer = transfer_sg o sign_of; 
459 

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

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

461 
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

462 

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

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

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

465 
Logic.strip_imp_prems (Logic.skip_flexpairs prop); 
0  466 

467 
(*counts premises in a rule*) 

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

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

469 
Logic.count_prems (Logic.skip_flexpairs prop, 0); 
0  470 

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

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

472 
fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop; 
0  473 

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

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

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

476 
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

477 

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

478 

0  479 

1238  480 
(** sort contexts of theorems **) 
481 

482 
(* basic utils *) 

483 

2163  484 
(*accumulate sorts suppressing duplicates; these are coded low levelly 
1238  485 
to improve efficiency a bit*) 
486 

487 
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

488 
 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

489 
 add_typ_sorts (TVar (_, S), Ss) = ins_sort(S,Ss) 
1238  490 
and add_typs_sorts ([], Ss) = Ss 
491 
 add_typs_sorts (T :: Ts, Ss) = add_typs_sorts (Ts, add_typ_sorts (T, Ss)); 

492 

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

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

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

496 
 add_term_sorts (Bound _, Ss) = Ss 

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

497 
 add_term_sorts (Abs (_,T,t), Ss) = add_term_sorts (t, add_typ_sorts (T,Ss)) 
1238  498 
 add_term_sorts (t $ u, Ss) = add_term_sorts (t, add_term_sorts (u, Ss)); 
499 

500 
fun add_terms_sorts ([], Ss) = Ss 

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

501 
 add_terms_sorts (t::ts, Ss) = add_terms_sorts (ts, add_term_sorts (t,Ss)); 
1238  502 

1258  503 
fun env_codT (Envir.Envir {iTs, ...}) = map snd iTs; 
504 

505 
fun add_env_sorts (env, Ss) = 

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

507 
add_typs_sorts (env_codT env, Ss)); 

508 

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

511 

512 
fun add_thms_shyps ([], Ss) = Ss 

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

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

514 
add_thms_shyps (ths, union_sort(shyps,Ss)); 
1238  515 

516 

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

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

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

520 

521 

522 
(* fix_shyps *) 

523 

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

525 
fun fix_shyps thms Ts 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, hyps, prop, ...} = thm; 
1238  528 
val shyps = 
529 
add_thm_sorts (thm, add_typs_sorts (Ts, add_thms_shyps (thms, []))); 

530 
in 

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

531 
Thm {sign_ref = sign_ref, 
2386  532 
der = der, (*No new derivation, as other rules call this*) 
533 
maxidx = maxidx, 

534 
shyps = shyps, hyps = hyps, prop = prop} 

1238  535 
end; 
536 

537 

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

539 

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

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

543 
fun strip_shyps thm = 

544 
let 

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

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

547 
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

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

550 
Thm {sign_ref = sign_ref, der = der, maxidx = maxidx, 
2386  551 
shyps = 
552 
(if eq_set_sort (shyps',sorts) orelse 

553 
not (!force_strip_shyps) then shyps' 

3061  554 
else (* FIXME tmp (since 1995/08/01) *) 
2386  555 
(warning ("Removed sort hypotheses: " ^ 
2962  556 
commas (map Sorts.str_of_sort (shyps' \\ sorts))); 
2386  557 
warning "Let's hope these sorts are nonempty!"; 
1238  558 
sorts)), 
1529  559 
hyps = hyps, 
560 
prop = prop} 

1238  561 
end; 
562 

563 

564 
(* implies_intr_shyps *) 

565 

566 
(*discharge all extra sort hypotheses*) 

567 
fun implies_intr_shyps thm = 

568 
(case extra_shyps thm of 

569 
[] => thm 

570 
 xshyps => 

571 
let 

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

572 
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

573 
val shyps' = ins_sort (logicS, shyps \\ xshyps); 
1238  574 
val used_names = foldr add_term_tfree_names (prop :: hyps, []); 
575 
val names = 

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

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

578 

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

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

582 
Thm {sign_ref = sign_ref, 
2386  583 
der = infer_derivs (Implies_intr_shyps, [der]), 
584 
maxidx = maxidx, 

585 
shyps = shyps', 

586 
hyps = hyps, 

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

1238  588 
end); 
589 

590 

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

592 

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

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

595 
let 
3994  596 
val name = Sign.intern (sign_of theory) Theory.axiomK raw_name; 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

597 
fun get_ax [] = raise Match 
1529  598 
 get_ax (thy :: thys) = 
3994  599 
let val {sign, axioms, parents, ...} = rep_theory thy 
600 
in case Symtab.lookup (axioms, name) of 

2386  601 
Some t => fix_shyps [] [] 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

602 
(Thm {sign_ref = Sign.self_ref sign, 
4182  603 
der = infer_derivs (Axiom name, []), 
2386  604 
maxidx = maxidx_of_term t, 
605 
shyps = [], 

606 
hyps = [], 

607 
prop = t}) 

608 
 None => get_ax parents handle Match => get_ax thys 

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

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

611 
get_ax [theory] handle Match 
3994  612 
=> raise THEORY ("No axiom " ^ quote name, [theory]) 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

614 

1529  615 

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

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

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

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

620 

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

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

624 
Join (Theorem _, _) => th 

625 
 Join (Axiom _, _) => th 

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

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

628 

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

630 
(case der of 

631 
Join (Theorem name, _) => name 

4182  632 
 Join (Axiom name, _) => name 
4018  633 
 _ => ""); 
0  634 

635 

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

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

638 
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

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

642 
shyps = shyps, 

643 
hyps = map Term.compress_term hyps, 

644 
prop = Term.compress_term prop}; 

564  645 

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

646 

2509  647 

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

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

652 
recurrence.*) 

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

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

655 
Thm {sign_ref = sign_ref, 
2386  656 
der = der, 
657 
maxidx = maxidx_of_term prop, 

658 
shyps = shyps, 

659 
hyps = hyps, 

660 
prop = prop}) 

2147  661 
handle TYPE(msg,Ts,ts) => raise TYPE(s^": "^msg,Ts,ts); 
1495
b8b54847c77f
Added check for duplicate vars with distinct types/sorts (nodup_Vars)
nipkow
parents:
1493
diff
changeset

662 

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

665 
(*discharge all assumptions t from ts*) 

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

1220  668 
(*The assumption rule AA in a theory*) 
250  669 
fun assume ct : thm = 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

670 
let val Cterm {sign_ref, t=prop, T, maxidx} = ct 
250  671 
in if T<>propT then 
672 
raise THM("assume: assumptions must have type prop", 0, []) 

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

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

676 
else Thm{sign_ref = sign_ref, 
2386  677 
der = infer_derivs (Assume ct, []), 
678 
maxidx = ~1, 

679 
shyps = add_term_sorts(prop,[]), 

680 
hyps = [prop], 

681 
prop = prop} 

0  682 
end; 
683 

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

687 
B 

1220  688 
 
689 
A ==> B 

690 
*) 

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

691 
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

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

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

699 
shyps = [], 

700 
hyps = disch(hyps,A), 

701 
prop = implies$A$prop}) 

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

704 
end; 

705 

1529  706 

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

709 
 

710 
B 

711 
*) 

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

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

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

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

723 
shyps = [], 

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

725 
prop = B}) 

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

0  728 
end; 
250  729 

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

732 
 

733 
!!x.A 

734 
*) 

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

735 
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

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

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

741 
shyps = [], 

742 
hyps = hyps, 

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

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

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

748 
else result(a,T) 

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

751 
end; 

752 

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

755 
 

756 
A[t/x] 

757 
*) 

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

758 
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

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

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

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

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

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

768 
shyps = [], 

769 
hyps = hyps, 

770 
prop = betapply(A,t)}) 

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

772 
then nodup_Vars thm "forall_elim" 

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

774 
end 

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

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

780 

1220  781 
(* Equality *) 
0  782 

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

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

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

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

790 
hyps = [], 

791 
maxidx = maxidx, 

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

0  793 
end; 
794 

795 
(*The symmetry rule 

1220  796 
t==u 
797 
 

798 
u==t 

799 
*) 

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

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

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

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

807 
shyps = shyps, 

808 
hyps = hyps, 

809 
prop = eq$u$t} 

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

812 
(*The transitive rule 

1220  813 
t1==u u==t2 
814 
 

815 
t1==t2 

816 
*) 

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

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

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

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

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

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

831 
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

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

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

838 

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

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

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

847 
shyps = [], 

848 
hyps = [], 

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

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

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

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

856 
f == g 

857 
*) 

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

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

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

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

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

867 
 Var _ => 

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

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

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

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

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

875 
shyps = shyps, 

876 
hyps = hyps, 

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

880 

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

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

1220  883 
t == u 
884 
 

885 
%x.t == %x.u 

886 
*) 

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

887 
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

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

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

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

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

896 
shyps = [], 

897 
hyps = hyps, 

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

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

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

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

904 
else result T 

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

907 
end; 

908 

909 
(*The combination rule 

3529  910 
f == g t == u 
911 
 

912 
f(t) == g(u) 

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

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

922 
if T1 <> fastype_of t then 

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

924 
else () 

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

926 
[th1,th2])) 

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

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

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

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

934 
shyps = union_sort(shyps1,shyps2), 

935 
hyps = union_term(hyps1,hyps2), 

936 
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

937 
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

938 
then nodup_Vars thm "combination" 
2386  939 
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

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

943 

944 

945 
(* Equality introduction 

3529  946 
A ==> B B ==> A 
947 
 

948 
A == B 

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

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

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

960 
(*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 (Equal_intr, [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(A,B)} 

967 
else err"not equal" 

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

970 

971 

972 
(*The equal propositions rule 

3529  973 
A == B A 
1529  974 
 
975 
B 

976 
*) 

977 
fun equal_elim th1 th2 = 

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

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

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

981 
in case prop1 of 

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

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

984 
fix_shyps [th1, th2] [] 

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

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

988 
shyps = [], 

989 
hyps = union_term(hyps1,hyps2), 

990 
prop = B}) 

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

0  993 

1220  994 

995 

0  996 
(**** Derived rules ****) 
997 

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

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

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

1005 
shyps = shyps, 

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

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

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

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

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

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

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

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

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

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

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

1027 
shyps = [], 

1028 
hyps = hyps, 

1029 
prop = newprop}) 

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

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

1036 
(*Instantiation of Vars 

1220  1037 
A 
1038 
 

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

1040 
*) 

0  1041 

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

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

1044 

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

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

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

1047 
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

1048 
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

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

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

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

1052 
else raise TYPE("add_ctpair", [T,U], [t,u]) 
0  1053 
end; 
1054 

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

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

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

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

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

1060 
Instantiates distinct Vars by terms of same type. 

1061 
Normalizes the new theorem! *) 

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

1063 
 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

1064 
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

1065 
val (newsign_ref,vTs) = foldr add_ctyp (vcTs, (newsign_ref,[])); 
250  1066 
val newprop = 
1067 
Envir.norm_term (Envir.empty 0) 

1068 
(subst_atomic tpairs 

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

1069 
(Type.inst_term_tvars(Sign.tsig_of (Sign.deref newsign_ref),vTs) prop)) 
1220  1070 
val newth = 
1071 
fix_shyps [th] (map snd vTs) 

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

1072 
(Thm{sign_ref = newsign_ref, 
2386  1073 
der = infer_derivs (Instantiate(vcTs,ctpairs), [der]), 
1074 
maxidx = maxidx_of_term newprop, 

1075 
shyps = [], 

1076 
hyps = hyps, 

1077 
prop = newprop}) 

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

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

2147  1082 
else nodup_Vars newth "instantiate" 
0  1083 
end 
250  1084 
handle TERM _ => 
0  1085 
raise THM("instantiate: incompatible signatures",0,[th]) 
2671  1086 
 TYPE (msg,_,_) => raise THM("instantiate: type conflict: " ^ msg, 
1087 
0, [th]); 

0  1088 

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

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

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

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

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

1096 
(Thm{sign_ref = sign_ref, 
2386  1097 
der = infer_derivs (Trivial ct, []), 
1098 
maxidx = maxidx, 

1099 
shyps = [], 

1100 
hyps = [], 

1101 
prop = implies$A$A}) 

0  1102 
end; 
1103 

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

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

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

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

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

1112 
(Thm {sign_ref = sign_ref, 
4182  1113 
der = infer_derivs (Class_triv c, []), 
2386  1114 
maxidx = maxidx, 
1115 
shyps = [], 

1116 
hyps = [], 

1117 
prop = t}) 

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

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

1119 

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

1120 

0  1121 
(* 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

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

1125 
Thm{sign_ref = sign_ref, 
2386  1126 
der = infer_derivs (VarifyT, [der]), 
1127 
maxidx = Int.max(0,maxidx), 

1128 
shyps = shyps, 

1129 
hyps = hyps, 

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

0  1134 
end; 
1135 

1136 
(* Replace all TVars by new TFrees *) 

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

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

1140 
Thm{sign_ref = sign_ref, 
2386  1141 
der = infer_derivs (FreezeT, [der]), 
1142 
maxidx = maxidx_of_term prop', 

1143 
shyps = shyps, 

1144 
hyps = hyps, 

1529  1145 
prop = prop'} 
1220  1146 
end; 
0  1147 

1148 

1149 
(*** Inference rules for tactics ***) 

1150 

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

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

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

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

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

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

1157 
end 

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

1159 

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

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

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

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

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

1171 
Thm{sign_ref = merge_thm_sgs(state,orule), 
2386  1172 
der = infer_derivs (Lift_rule(ct_Bi, i), [der]), 
1173 
maxidx = maxidx+smax+1, 

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

1174 
shyps=union_sort(sshyps,shyps), 
2386  1175 
hyps=hyps, 
1529  1176 
prop = Logic.rule_of (map (pairself lift_abs) tpairs, 
2386  1177 
map lift_all As, 
1178 
lift_all B)} 

0  1179 
end; 
1180 

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

1182 
fun assumption i state = 

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

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

1187 
(Thm{sign_ref = sign_ref, 
2386  1188 
der = infer_derivs (Assumption (i, Some env), [der]), 
1189 
maxidx = maxidx, 

1190 
shyps = [], 

1191 
hyps = hyps, 

1192 
prop = 

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

1194 
Logic.rule_of (tpairs, Bs, C) 

1195 
else (*normalize the new rule fully*) 

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

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

1199 
(Seq.mapp newth 

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

1200 
(Unify.unifiers(Sign.deref sign_ref,Envir.empty maxidx, (t,u)::tpairs)) 
250  1201 
(addprfs apairs))) 
0  1202 
in addprfs (Logic.assum_pairs Bi) end; 
1203 

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

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

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

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

1211 
(Thm{sign_ref = sign_ref, 
2386  1212 
der = infer_derivs (Assumption (i,None), [der]), 
1213 
maxidx = maxidx, 

1214 
shyps = [], 

1215 
hyps = hyps, 

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

0  1217 
else raise THM("eq_assumption", 0, [state]) 
1218 
end; 

1219 

1220 

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

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

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

1226 
and asms = Logic.strip_assums_hyp Bi 

1227 
and concl = Logic.strip_assums_concl Bi 

1228 
val n = length asms 

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

1230 
else if 0<m andalso m<n 

1231 
then list_all 

1232 
(params, 

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

1234 
List.take(asms, m), 

1235 
concl)) 

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

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

1237 
in Thm{sign_ref = sign_ref, 
2671  1238 
der = infer_derivs (Rotate_rule (k,i), [der]), 
1239 
maxidx = maxidx, 

1240 
shyps = shyps, 

1241 
hyps = hyps, 

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

1243 
end; 

1244 

1245 

0  1246 
(** User renaming of parameters in a subgoal **) 
1247 

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

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

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

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

1252 
fun rename_params_rule (cs, i) state = 

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

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

1256 
val short = length iparams  length cs 

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

1259 
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

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

1264 
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

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

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

1267 
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

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

1270 
(Thm{sign_ref = sign_ref, 
2386  1271 
der = infer_derivs (Rename_params_rule(cs,i), [der]), 
1272 
maxidx = maxidx, 

1273 
shyps = [], 

1274 
hyps = hyps, 

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

0  1276 
end; 
1277 

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

1279 

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

1283 
match_bvs(s, t, if x="" orelse y="" then al 
1238  1284 
else (x,y)::al) 
0  1285 
 match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al)) 
1286 
 match_bvs(_,_,al) = al; 

1287 

1288 
(* strip abstractions created by parameters *) 

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

1290 

1291 

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

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

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

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

1299 
 strip(A,_) = f A 

0  1300 
in strip end; 
1301 

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

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

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

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

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

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

1309 
(*unknowns appearing elsewhere be preserved!*) 

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

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

1312 
(case assoc(al,x) of 

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

1313 
Some(y) => if x mem_string vids orelse y mem_string vids then t 
250  1314 
else Var((y,i),T) 
1315 
 None=> t) 

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

1317 
Abs(case assoc_string(al,x) of Some(y) => y  None => x, 
250  1318 
T, rename t) 
0  1319 
 rename(f$t) = rename f $ rename t 
1320 
 rename(t) = t; 

250  1321 
fun strip_ren Ai = strip_apply rename (Ai,B) 
0  1322 
in strip_ren end; 
1323 

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

1325 
fun rename_bvars(dpairs, tpairs, B) = 

250  1326 
rename_bvs(foldr match_bvars (dpairs,[]), dpairs, tpairs, B); 
0  1327 

1328 

1329 
(*** RESOLUTION ***) 

1330 

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

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

1332 

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

250  1335 
fun strip_assums2 (Const("==>", _) $ _ $ B1, 
1336 
Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2) 

0  1337 
 strip_assums2 (Const("all",_)$Abs(a,T,t1), 
250  1338 
Const("all",_)$Abs(_,_,t2)) = 
0  1339 
let val (B1,B2) = strip_assums2 (t1,t2) 
1340 
in (Abs(a,T,B1), Abs(a,T,B2)) end 

1341 
 strip_assums2 BB = BB; 

1342 

1343 

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

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

1345 
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

1346 
 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

1347 
let val Envir.Envir{iTs, ...} = env 
1238  1348 
val T' = typ_subst_TVars iTs T 
1349 
(*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

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

1351 
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

1352 
 norm_term_skip env n (Const("==>", _) $ A $ B) = 
1238  1353 
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

1354 
 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

1355 

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

1356 

0  1357 
(*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C) 
250  1358 
Unifies B with Bi, replacing subgoal i (1 <= i <= n) 
0 