author  wenzelm 
Fri, 21 Nov 1997 15:27:43 +0100  
changeset 4270  957c887b89b5 
parent 4254  8ae7ace96c39 
child 4281  6c6073b13600 
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 
1394
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

27 
val read_cterms : Sign.sg > string list * typ list > cterm list 
1238  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 

37 

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

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

2671  45 
 Theorem of string 
46 
 Assume of cterm 

47 
 Implies_intr of cterm 

1529  48 
 Implies_intr_shyps 
49 
 Implies_intr_hyps 

50 
 Implies_elim 

2671  51 
 Forall_intr of cterm 
52 
 Forall_elim of cterm 

53 
 Reflexive of cterm 

1529  54 
 Symmetric 
55 
 Transitive 

2671  56 
 Beta_conversion of cterm 
1529  57 
 Extensional 
2671  58 
 Abstract_rule of string * cterm 
1529  59 
 Combination 
60 
 Equal_intr 

61 
 Equal_elim 

2671  62 
 Trivial of cterm 
63 
 Lift_rule of cterm * int 

64 
 Assumption of int * Envir.env option 

65 
 Rotate_rule of int * int 

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

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

68 
 Flexflex_rule of Envir.env 

4182  69 
 Class_triv of class 
1529  70 
 VarifyT 
71 
 FreezeT 

2671  72 
 RewriteC of cterm 
73 
 CongC of cterm 

74 
 Rewrite_cterm of cterm 

75 
 Rename_params_rule of string list * int; 

1529  76 

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

77 
type deriv (* = rule mtree *) 
1529  78 

1160  79 
(*meta theorems*) 
80 
type thm 

81 
exception THM of string * int * thm list 

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

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

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

89 
val sign_of_thm : thm > Sign.sg 
4254  90 
val transfer_sg : Sign.sg > thm > thm 
3895  91 
val transfer : theory > thm > thm 
1238  92 
val tpairs_of : thm > (term * term) list 
93 
val prems_of : thm > term list 

94 
val nprems_of : thm > int 

95 
val concl_of : thm > term 

96 
val cprop_of : thm > cterm 

97 
val extra_shyps : thm > sort list 

3061  98 
val force_strip_shyps : bool ref (* FIXME tmp (since 1995/08/01) *) 
1238  99 
val strip_shyps : thm > thm 
100 
val implies_intr_shyps: thm > thm 

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

102 
val name_thm : string * thm > thm 
4018  103 
val name_of_thm : thm > string 
1238  104 
val axioms_of : theory > (string * thm) list 
1160  105 

106 
(*meta rules*) 

1238  107 
val assume : cterm > thm 
1416  108 
val compress : thm > thm 
1238  109 
val implies_intr : cterm > thm > thm 
110 
val implies_elim : thm > thm > thm 

111 
val forall_intr : cterm > thm > thm 

112 
val forall_elim : cterm > thm > thm 

113 
val reflexive : cterm > thm 

114 
val symmetric : thm > thm 

115 
val transitive : thm > thm > thm 

116 
val beta_conversion : cterm > thm 

117 
val extensional : thm > thm 

118 
val abstract_rule : string > cterm > thm > thm 

119 
val combination : thm > thm > thm 

120 
val equal_intr : thm > thm > thm 

121 
val equal_elim : thm > thm > thm 

122 
val implies_intr_hyps : thm > thm 

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

128 
val varifyT : thm > thm 

129 
val freezeT : thm > thm 

130 
val dest_state : thm * int > 

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

142 
(*meta simplification*) 

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

1238  147 
val empty_mss : meta_simpset 
3550  148 
val merge_mss : meta_simpset * meta_simpset > meta_simpset 
1238  149 
val add_simps : meta_simpset * thm list > meta_simpset 
150 
val del_simps : meta_simpset * thm list > meta_simpset 

151 
val mss_of : thm list > meta_simpset 

152 
val add_congs : meta_simpset * thm list > meta_simpset 

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

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

156 
> meta_simpset 
2509  157 
val del_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 
1238  160 
val add_prems : meta_simpset * thm list > meta_simpset 
161 
val prems_of_mss : meta_simpset > thm list 

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

163 
val mk_rews_of_mss : meta_simpset > thm > thm list 

2509  164 
val set_termless : meta_simpset * (term * term > bool) > meta_simpset 
1238  165 
val trace_simp : bool ref 
166 
val rewrite_cterm : bool * bool > meta_simpset > 

1529  167 
(meta_simpset > thm > thm option) > cterm > thm 
1539  168 

4124  169 
val invoke_oracle : theory > xstring > Sign.sg * object > thm 
250  170 
end; 
0  171 

3550  172 
structure Thm: THM = 
0  173 
struct 
250  174 

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

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

176 

250  177 
(** certified types **) 
178 

179 
(*certified typs under a signature*) 

180 

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

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

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

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

186 
fun ctyp_of sign T = 

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

187 
Ctyp {sign_ref = Sign.self_ref sign, T = Sign.certify_typ sign T}; 
250  188 

189 
fun read_ctyp sign s = 

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

191 

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

192 

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

193 

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

195 

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

197 

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

198 
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

199 

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

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

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

202 

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

204 

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

205 
fun ctyp_of_term (Cterm {sign_ref, T, ...}) = Ctyp {sign_ref = sign_ref, T = T}; 
2671  206 

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

209 
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

210 
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

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

212 

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

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

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

215 

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

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

217 

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

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

219 
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

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

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

222 
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

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

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

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

226 
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

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

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

229 

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

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

231 
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

232 
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

233 
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

234 
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

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

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

237 

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

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

241 
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

242 

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

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

244 
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

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

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

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

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

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

251 
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

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

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

256 

2509  257 

258 

574  259 
(** read cterms **) (*exception ERROR*) 
250  260 

261 
(*read term, infer types, certify term*) 

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

262 
fun read_def_cterm (sign, types, sorts) used freeze (a, T) = 
250  263 
let 
574  264 
val T' = Sign.certify_typ sign T 
265 
handle TYPE (msg, _, _) => error msg; 

623  266 
val ts = Syntax.read (#syn (Sign.rep_sg sign)) T' a; 
4251  267 
val (t', tye) = Sign.infer_types sign types sorts used freeze (ts, T'); 
574  268 
val ct = cterm_of sign t' 
2979  269 
handle TYPE (msg, _, _) => error msg 
2386  270 
 TERM (msg, _) => error msg; 
250  271 
in (ct, tye) end; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

272 

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

273 
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

274 

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

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

276 
NO disambiguation of alternative parses via typechecking  it is just 
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

277 
not practical.*) 
3789  278 
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

279 
let 
3789  280 
val {tsig, syn, ...} = Sign.rep_sg sg; 
2979  281 
fun read (b, T) = 
282 
(case Syntax.read syn T b of 

283 
[t] => t 

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

285 

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

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

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

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

293 
in map (cterm_of sg) us end 

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

295 
 TERM (msg, _) => error msg; 
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

296 

250  297 

298 

1529  299 
(*** Derivations ***) 
300 

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

302 
executed in ML.*) 

303 
datatype rule = 

2386  304 
MinProof (*for building minimal proof terms*) 
4182  305 
 Oracle of string * Sign.sg * object (*oracles*) 
1529  306 
(*Axioms/theorems*) 
4182  307 
 Axiom of string 
2386  308 
 Theorem of string 
1529  309 
(*primitive inferences and compound versions of them*) 
2386  310 
 Assume of cterm 
311 
 Implies_intr of cterm 

1529  312 
 Implies_intr_shyps 
313 
 Implies_intr_hyps 

314 
 Implies_elim 

2386  315 
 Forall_intr of cterm 
316 
 Forall_elim of cterm 

317 
 Reflexive of cterm 

1529  318 
 Symmetric 
319 
 Transitive 

2386  320 
 Beta_conversion of cterm 
1529  321 
 Extensional 
2386  322 
 Abstract_rule of string * cterm 
1529  323 
 Combination 
324 
 Equal_intr 

325 
 Equal_elim 

326 
(*derived rules for tactical proof*) 

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

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

330 
 Lift_rule of cterm * int 

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

2671  332 
 Rotate_rule of int * int 
2386  333 
 Instantiate of (indexname * ctyp) list * (cterm * cterm) list 
334 
 Bicompose of bool * bool * int * int * Envir.env 

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

1529  336 
(*other derived rules*) 
4182  337 
 Class_triv of class 
1529  338 
 VarifyT 
339 
 FreezeT 

340 
(*for the simplifier*) 

2386  341 
 RewriteC of cterm 
342 
 CongC of cterm 

343 
 Rewrite_cterm of cterm 

1529  344 
(*Logical identities, recorded since they are part of the proof process*) 
2386  345 
 Rename_params_rule of string list * int; 
1529  346 

347 

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

348 
type deriv = rule mtree; 
1529  349 

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

350 
datatype deriv_kind = MinDeriv  ThmDeriv  FullDeriv; 
1529  351 

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

352 
val keep_derivs = ref MinDeriv; 
1529  353 

354 

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

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

356 
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

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

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

359 
(case der of 
2386  360 
Join (Oracle _, _) => der :: squash_derivs ders 
361 
 Join (Theorem _, [der']) => if !keep_derivs=ThmDeriv 

362 
then der :: squash_derivs ders 

363 
else squash_derivs (der'::ders) 

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

365 
then der :: squash_derivs ders 

366 
else squash_derivs ders 

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

368 
 _ => der :: squash_derivs ders); 

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

369 

1529  370 

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

372 
val min_infer = Join (MinProof, []); 
1529  373 

374 
(*Make a minimal inference*) 

375 
fun make_min_infer [] = min_infer 

376 
 make_min_infer [der] = der 

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

377 
 make_min_infer ders = Join (MinProof, ders); 
1529  378 

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

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

381 
if !keep_derivs=FullDeriv then Join (rl, ders) 
1529  382 
else make_min_infer (squash_derivs ders); 
383 

384 

2509  385 

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

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

387 

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

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

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

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

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

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

394 
prop: term}; (*conclusion*) 
0  395 

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

396 
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

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

398 
shyps = shyps, hyps = hyps, prop = prop}; 
0  399 

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

401 
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

402 
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

403 
in {sign = Sign.deref sign_ref, der = der, maxidx = maxidx, shyps = shyps, 
1529  404 
hyps = map (ctermf ~1) hyps, 
405 
prop = ctermf maxidx prop} 

1517  406 
end; 
407 

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

408 
(*errors involving theorems*) 
0  409 
exception THM of string * int * thm list; 
410 

3994  411 
(*equality of theorems uses equality of signatures and the 
412 
aconvertible test for terms*) 

413 
fun eq_thm (th1, th2) = 

414 
let 

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

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

417 
in 

418 
Sign.eq_sg (sg1, sg2) andalso 

419 
eq_set_sort (shyps1, shyps2) andalso 

420 
aconvs (hyps1, hyps2) andalso 

421 
prop1 aconv prop2 

422 
end; 

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

423 

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

424 
fun sign_of_thm (Thm {sign_ref, ...}) = Sign.deref sign_ref; 
0  425 

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

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

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

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

429 
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

430 

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

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

434 
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

435 
val sign = Sign.deref sign_ref; 
3895  436 
in 
4254  437 
if Sign.eq_sg (sign, sign') then thm 
438 
else if Sign.subsig (sign, sign') then 

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

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

442 
end; 

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

443 

4254  444 
val transfer = transfer_sg o sign_of; 
445 

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

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

447 
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

448 

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

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

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

451 
Logic.strip_imp_prems (Logic.skip_flexpairs prop); 
0  452 

453 
(*counts premises in a rule*) 

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

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

455 
Logic.count_prems (Logic.skip_flexpairs prop, 0); 
0  456 

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

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

458 
fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop; 
0  459 

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

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

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

462 
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

463 

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

464 

0  465 

1238  466 
(** sort contexts of theorems **) 
467 

468 
(* basic utils *) 

469 

2163  470 
(*accumulate sorts suppressing duplicates; these are coded low levelly 
1238  471 
to improve efficiency a bit*) 
472 

473 
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

474 
 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

475 
 add_typ_sorts (TVar (_, S), Ss) = ins_sort(S,Ss) 
1238  476 
and add_typs_sorts ([], Ss) = Ss 
477 
 add_typs_sorts (T :: Ts, Ss) = add_typs_sorts (Ts, add_typ_sorts (T, Ss)); 

478 

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

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

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

482 
 add_term_sorts (Bound _, Ss) = Ss 

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

483 
 add_term_sorts (Abs (_,T,t), Ss) = add_term_sorts (t, add_typ_sorts (T,Ss)) 
1238  484 
 add_term_sorts (t $ u, Ss) = add_term_sorts (t, add_term_sorts (u, Ss)); 
485 

486 
fun add_terms_sorts ([], Ss) = Ss 

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

487 
 add_terms_sorts (t::ts, Ss) = add_terms_sorts (ts, add_term_sorts (t,Ss)); 
1238  488 

1258  489 
fun env_codT (Envir.Envir {iTs, ...}) = map snd iTs; 
490 

491 
fun add_env_sorts (env, Ss) = 

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

493 
add_typs_sorts (env_codT env, Ss)); 

494 

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

497 

498 
fun add_thms_shyps ([], Ss) = Ss 

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

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

500 
add_thms_shyps (ths, union_sort(shyps,Ss)); 
1238  501 

502 

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

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

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

506 

507 

508 
(* fix_shyps *) 

509 

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

511 
fun fix_shyps thms Ts thm = 

512 
let 

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

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

516 
in 

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

517 
Thm {sign_ref = sign_ref, 
2386  518 
der = der, (*No new derivation, as other rules call this*) 
519 
maxidx = maxidx, 

520 
shyps = shyps, hyps = hyps, prop = prop} 

1238  521 
end; 
522 

523 

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

525 

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

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

529 
fun strip_shyps thm = 

530 
let 

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

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

533 
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

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

536 
Thm {sign_ref = sign_ref, der = der, maxidx = maxidx, 
2386  537 
shyps = 
538 
(if eq_set_sort (shyps',sorts) orelse 

539 
not (!force_strip_shyps) then shyps' 

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

1238  547 
end; 
548 

549 

550 
(* implies_intr_shyps *) 

551 

552 
(*discharge all extra sort hypotheses*) 

553 
fun implies_intr_shyps thm = 

554 
(case extra_shyps thm of 

555 
[] => thm 

556 
 xshyps => 

557 
let 

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

558 
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

559 
val shyps' = ins_sort (logicS, shyps \\ xshyps); 
1238  560 
val used_names = foldr add_term_tfree_names (prop :: hyps, []); 
561 
val names = 

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

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

564 

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

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

568 
Thm {sign_ref = sign_ref, 
2386  569 
der = infer_derivs (Implies_intr_shyps, [der]), 
570 
maxidx = maxidx, 

571 
shyps = shyps', 

572 
hyps = hyps, 

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

1238  574 
end); 
575 

576 

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

578 

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

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

581 
let 
3994  582 
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

583 
fun get_ax [] = raise Match 
1529  584 
 get_ax (thy :: thys) = 
3994  585 
let val {sign, axioms, parents, ...} = rep_theory thy 
586 
in case Symtab.lookup (axioms, name) of 

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

588 
(Thm {sign_ref = Sign.self_ref sign, 
4182  589 
der = infer_derivs (Axiom name, []), 
2386  590 
maxidx = maxidx_of_term t, 
591 
shyps = [], 

592 
hyps = [], 

593 
prop = t}) 

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

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

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

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

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

600 

1529  601 

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

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

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

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

606 

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

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

610 
Join (Theorem _, _) => th 

611 
 Join (Axiom _, _) => th 

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

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

614 

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

616 
(case der of 

617 
Join (Theorem name, _) => name 

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

621 

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

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

624 
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

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

628 
shyps = shyps, 

629 
hyps = map Term.compress_term hyps, 

630 
prop = Term.compress_term prop}; 

564  631 

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

632 

2509  633 

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

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

638 
recurrence.*) 

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

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

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

644 
shyps = shyps, 

645 
hyps = hyps, 

646 
prop = prop}) 

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

648 

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

651 
(*discharge all assumptions t from ts*) 

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

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

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

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

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

662 
else Thm{sign_ref = sign_ref, 
2386  663 
der = infer_derivs (Assume ct, []), 
664 
maxidx = ~1, 

665 
shyps = add_term_sorts(prop,[]), 

666 
hyps = [prop], 

667 
prop = prop} 

0  668 
end; 
669 

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

673 
B 

1220  674 
 
675 
A ==> B 

676 
*) 

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

677 
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

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

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

685 
shyps = [], 

686 
hyps = disch(hyps,A), 

687 
prop = implies$A$prop}) 

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

690 
end; 

691 

1529  692 

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

695 
 

696 
B 

697 
*) 

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

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

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

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

709 
shyps = [], 

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

711 
prop = B}) 

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

0  714 
end; 
250  715 

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

718 
 

719 
!!x.A 

720 
*) 

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

721 
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

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

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

727 
shyps = [], 

728 
hyps = hyps, 

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

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

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

734 
else result(a,T) 

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

737 
end; 

738 

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

741 
 

742 
A[t/x] 

743 
*) 

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

744 
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

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

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

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

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

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

754 
shyps = [], 

755 
hyps = hyps, 

756 
prop = betapply(A,t)}) 

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

758 
then nodup_Vars thm "forall_elim" 

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

760 
end 

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

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

766 

1220  767 
(* Equality *) 
0  768 

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

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

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

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

776 
hyps = [], 

777 
maxidx = maxidx, 

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

0  779 
end; 
780 

781 
(*The symmetry rule 

1220  782 
t==u 
783 
 

784 
u==t 

785 
*) 

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

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

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

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

793 
shyps = shyps, 

794 
hyps = hyps, 

795 
prop = eq$u$t} 

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

798 
(*The transitive rule 

1220  799 
t1==u u==t2 
800 
 

801 
t1==t2 

802 
*) 

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

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

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

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

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

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

817 
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

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

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

824 

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

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

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

833 
shyps = [], 

834 
hyps = [], 

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

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

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

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

842 
f == g 

843 
*) 

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

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

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

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

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

853 
 Var _ => 

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

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

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

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

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

861 
shyps = shyps, 

862 
hyps = hyps, 

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

866 

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

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

1220  869 
t == u 
870 
 

871 
%x.t == %x.u 

872 
*) 

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

873 
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

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

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

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

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

882 
shyps = [], 

883 
hyps = hyps, 

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

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

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

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

890 
else result T 

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

893 
end; 

894 

895 
(*The combination rule 

3529  896 
f == g t == u 
897 
 

898 
f(t) == g(u) 

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

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

908 
if T1 <> fastype_of t then 

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

910 
else () 

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

912 
[th1,th2])) 

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

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

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

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

920 
shyps = union_sort(shyps1,shyps2), 

921 
hyps = union_term(hyps1,hyps2), 

922 
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

923 
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

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

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

929 

930 

931 
(* Equality introduction 

3529  932 
A ==> B B ==> A 
933 
 

934 
A == B 

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

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

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

946 
(*no fix_shyps*) 

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

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

950 
shyps = union_sort(shyps1,shyps2), 

951 
hyps = union_term(hyps1,hyps2), 

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

953 
else err"not equal" 

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

956 

957 

958 
(*The equal propositions rule 

3529  959 
A == B A 
1529  960 
 
961 
B 

962 
*) 

963 
fun equal_elim th1 th2 = 

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

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

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

967 
in case prop1 of 

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

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

970 
fix_shyps [th1, th2] [] 

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

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

974 
shyps = [], 

975 
hyps = union_term(hyps1,hyps2), 

976 
prop = B}) 

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

0  979 

1220  980 

981 

0  982 
(**** Derived rules ****) 
983 

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

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

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

991 
shyps = shyps, 

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

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

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

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

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

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

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

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

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

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

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

1013 
shyps = [], 

1014 
hyps = hyps, 

1015 
prop = newprop}) 

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

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

1022 
(*Instantiation of Vars 

1220  1023 
A 
1024 
 

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

1026 
*) 

0  1027 

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

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

1030 

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

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

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

1033 
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

1034 
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

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

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

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

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

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

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

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

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

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

1046 
Instantiates distinct Vars by terms of same type. 

1047 
Normalizes the new theorem! *) 

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

1049 
 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

1050 
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

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

1054 
(subst_atomic tpairs 

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

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

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

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

1061 
shyps = [], 

1062 
hyps = hyps, 

1063 
prop = newprop}) 

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

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

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

0  1074 

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

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

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

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

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

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

1085 
shyps = [], 

1086 
hyps = [], 

1087 
prop = implies$A$A}) 

0  1088 
end; 
1089 

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

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

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

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

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

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

1102 
hyps = [], 

1103 
prop = t}) 

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

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

1105 

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

1106 

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

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

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

1114 
shyps = shyps, 

1115 
hyps = hyps, 

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

0  1120 
end; 
1121 

1122 
(* Replace all TVars by new TFrees *) 

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

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

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

1129 
shyps = shyps, 

1130 
hyps = hyps, 

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

1134 

1135 
(*** Inference rules for tactics ***) 

1136 

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

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

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

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

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

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

1143 
end 

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

1145 

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

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

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

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

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

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

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

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

0  1165 
end; 
1166 

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

1168 
fun assumption i state = 

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

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

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

1176 
shyps = [], 

1177 
hyps = hyps, 

1178 
prop = 

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

1180 
Logic.rule_of (tpairs, Bs, C) 

1181 
else (*normalize the new rule fully*) 

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

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

1185 
(Seq.mapp newth 

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

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

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

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

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

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

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

1200 
shyps = [], 

1201 
hyps = hyps, 

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

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

1205 

1206 

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

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

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

1212 
and asms = Logic.strip_assums_hyp Bi 

1213 
and concl = Logic.strip_assums_concl Bi 

1214 
val n = length asms 

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

1216 
else if 0<m andalso m<n 

1217 
then list_all 

1218 
(params, 

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

1220 
List.take(asms, m), 

1221 
concl)) 

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

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

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

1226 
shyps = shyps, 

1227 
hyps = hyps, 

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

1229 
end; 

1230 

1231 

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

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

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

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

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

1238 
fun rename_params_rule (cs, i) state = 

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

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

1242 
val short = length iparams  length cs 

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

1245 
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

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

1250 
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

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

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

1253 
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

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

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

1259 
shyps = [], 

1260 
hyps = hyps, 

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

0  1262 
end; 
1263 

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

1265 

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

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

1273 

1274 
(* strip abstractions created by parameters *) 

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

1276 

1277 

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

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

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

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

1285 
 strip(A,_) = f A 

0  1286 
in strip end; 
1287 

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

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

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

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

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

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

1295 
(*unknowns appearing elsewhere be preserved!*) 

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

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

1298 
(case assoc(al,x) of 

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

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

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

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

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

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

1311 
fun rename_bvars(dpairs, tpairs, B) = 

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

1314 

1315 
(*** RESOLUTION ***) 

1316 

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

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

1318 

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

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

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

1327 
 strip_assums2 BB = BB; 

1328 

1329 

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

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

1331 
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

1332 
 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

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

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

1337 
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

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

1340 
 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

1341 

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

1342 

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

1347 
If eres_flg then simultaneously proves A1 by assumption. 

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

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

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