author  wenzelm 
Sun, 22 May 2005 16:51:12 +0200  
changeset 16024  ffe25459c72a 
parent 15797  a63605582573 
child 16135  c66545fe72bf 
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 
10486  7 
theorems, meta rules (including lifting and resolution). 
0  8 
*) 
9 

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

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

16 
val ctyp_of : Sign.sg > typ > ctyp 

17 
val read_ctyp : Sign.sg > string > ctyp 

1160  18 

19 
(*certified terms*) 

20 
type cterm 

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

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

2671  27 
val ctyp_of_term : cterm > ctyp 
1238  28 
val read_cterm : Sign.sg > string * typ > cterm 
1703
e22ad43bab5f
moved dest_cimplies to drule.ML; added adjust_maxidx
clasohm
parents:
1659
diff
changeset

29 
val adjust_maxidx : cterm > cterm 
1238  30 
val read_def_cterm : 
1160  31 
Sign.sg * (indexname > typ option) * (indexname > sort option) > 
32 
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

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

34 
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

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

36 
> cterm list * (indexname * typ)list 
1160  37 

6089  38 
type tag (* = string * string list *) 
1529  39 

1160  40 
(*meta theorems*) 
41 
type thm 

11518  42 
val rep_thm : thm > {sign: Sign.sg, der: bool * Proofterm.proof, maxidx: int, 
2386  43 
shyps: sort list, hyps: term list, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

44 
tpairs: (term * term) list, prop: term} 
11518  45 
val crep_thm : thm > {sign: Sign.sg, der: bool * Proofterm.proof, maxidx: int, 
2386  46 
shyps: sort list, hyps: cterm list, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

47 
tpairs: (cterm * cterm) list, prop: cterm} 
6089  48 
exception THM of string * int * thm list 
49 
type 'a attribute (* = 'a * thm > 'a * thm *) 

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

51 
val sign_of_thm : thm > Sign.sg 
12803  52 
val prop_of : thm > term 
13528  53 
val proof_of : thm > Proofterm.proof 
4254  54 
val transfer_sg : Sign.sg > thm > thm 
3895  55 
val transfer : theory > thm > thm 
1238  56 
val tpairs_of : thm > (term * term) list 
57 
val prems_of : thm > term list 

58 
val nprems_of : thm > int 

59 
val concl_of : thm > term 

60 
val cprop_of : thm > cterm 

61 
val extra_shyps : thm > sort list 

62 
val strip_shyps : thm > thm 

15672  63 
val get_axiom_i : theory > string > thm 
3812  64 
val get_axiom : theory > xstring > thm 
6368  65 
val def_name : string > string 
4847  66 
val get_def : theory > xstring > thm 
1238  67 
val axioms_of : theory > (string * thm) list 
1160  68 

69 
(*meta rules*) 

1238  70 
val assume : cterm > thm 
1416  71 
val compress : thm > thm 
1238  72 
val implies_intr : cterm > thm > thm 
73 
val implies_elim : thm > thm > thm 

74 
val forall_intr : cterm > thm > thm 

75 
val forall_elim : cterm > thm > thm 

76 
val reflexive : cterm > thm 

77 
val symmetric : thm > thm 

78 
val transitive : thm > thm > thm 

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

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

80 
val eta_conversion : cterm > thm 
1238  81 
val abstract_rule : string > cterm > thm > thm 
82 
val combination : thm > thm > thm 

83 
val equal_intr : thm > thm > thm 

84 
val equal_elim : thm > thm > thm 

85 
val implies_intr_hyps : thm > thm 

4270  86 
val flexflex_rule : thm > thm Seq.seq 
1238  87 
val instantiate : 
15797  88 
(ctyp * ctyp) list * (cterm * cterm) list > thm > thm 
1238  89 
val trivial : cterm > thm 
6368  90 
val class_triv : Sign.sg > class > thm 
1238  91 
val varifyT : thm > thm 
15797  92 
val varifyT' : (string * sort) list > thm > thm * ((string * sort) * indexname) list 
1238  93 
val freezeT : thm > thm 
94 
val dest_state : thm * int > 

1160  95 
(term * term) list * term list * term * term 
1238  96 
val lift_rule : (thm * int) > thm > thm 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

97 
val incr_indexes : int > thm > thm 
4270  98 
val assumption : int > thm > thm Seq.seq 
1238  99 
val eq_assumption : int > thm > thm 
2671  100 
val rotate_rule : int > int > thm > thm 
7248
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

101 
val permute_prems : int > int > thm > thm 
1160  102 
val rename_params_rule: string list * int > thm > thm 
1238  103 
val bicompose : bool > bool * thm * int > 
4270  104 
int > thm > thm Seq.seq 
1238  105 
val biresolution : bool > (bool * thm) list > 
4270  106 
int > thm > thm Seq.seq 
15672  107 
val invoke_oracle_i : theory > string > Sign.sg * Object.T > thm 
4999  108 
val invoke_oracle : theory > xstring > Sign.sg * Object.T > thm 
250  109 
end; 
0  110 

6089  111 
signature THM = 
112 
sig 

113 
include BASIC_THM 

15087  114 
val dest_ctyp : ctyp > ctyp list 
10767
8fa4aafa7314
Thm: dest_comb, dest_abs, capply, cabs no longer global;
wenzelm
parents:
10486
diff
changeset

115 
val dest_comb : cterm > cterm * cterm 
8fa4aafa7314
Thm: dest_comb, dest_abs, capply, cabs no longer global;
wenzelm
parents:
10486
diff
changeset

116 
val dest_abs : string option > cterm > cterm * cterm 
8fa4aafa7314
Thm: dest_comb, dest_abs, capply, cabs no longer global;
wenzelm
parents:
10486
diff
changeset

117 
val capply : cterm > cterm > cterm 
8fa4aafa7314
Thm: dest_comb, dest_abs, capply, cabs no longer global;
wenzelm
parents:
10486
diff
changeset

118 
val cabs : cterm > cterm > cterm 
8299  119 
val major_prem_of : thm > term 
7534  120 
val no_prems : thm > bool 
6089  121 
val no_attributes : 'a > 'a * 'b attribute list 
122 
val apply_attributes : ('a * thm) * 'a attribute list > ('a * thm) 

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

124 
val get_name_tags : thm > string * tag list 

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

126 
val name_of_thm : thm > string 

127 
val tags_of_thm : thm > tag list 

128 
val name_thm : string * thm > thm 

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

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

130 
val cterm_match : cterm * cterm > 
15797  131 
(ctyp * ctyp) list * (cterm * cterm) list 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

132 
val cterm_first_order_match : cterm * cterm > 
15797  133 
(ctyp * ctyp) list * (cterm * cterm) list 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

134 
val cterm_incr_indexes : int > cterm > cterm 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

135 
val terms_of_tpairs : (term * term) list > term list 
6089  136 
end; 
137 

3550  138 
structure Thm: THM = 
0  139 
struct 
250  140 

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

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

142 

250  143 
(** certified types **) 
144 

145 
(*certified typs under a signature*) 

146 

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

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

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

149 
fun rep_ctyp (Ctyp {sign_ref, T}) = {sign = Sign.deref sign_ref, T = T}; 
250  150 
fun typ_of (Ctyp {T, ...}) = T; 
151 

152 
fun ctyp_of sign T = 

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

153 
Ctyp {sign_ref = Sign.self_ref sign, T = Sign.certify_typ sign T}; 
250  154 

155 
fun read_ctyp sign s = 

15531  156 
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

157 

15087  158 
fun dest_ctyp (Ctyp {sign_ref, T = Type (s, Ts)}) = 
159 
map (fn T => Ctyp {sign_ref = sign_ref, T = T}) Ts 

160 
 dest_ctyp ct = [ct]; 

161 

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

162 

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

163 

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

165 

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

167 

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

168 
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

169 

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

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

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

172 

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

175 
maxidx = maxidx}; 

176 

9461  177 
fun sign_of_cterm (Cterm {sign_ref, ...}) = Sign.deref sign_ref; 
178 

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

180 

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

181 
fun ctyp_of_term (Cterm {sign_ref, T, ...}) = Ctyp {sign_ref = sign_ref, T = T}; 
2671  182 

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

14828  185 
let val (t, T, maxidx) = Sign.certify_term (Sign.pp sign) sign tm 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

186 
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

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

188 

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

189 

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

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

191 

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

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

193 
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

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

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

196 
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

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

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

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

200 
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

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

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

203 

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

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

205 
fun dest_abs a (Cterm {sign_ref, T as Type("fun",[_,S]), maxidx, t=Abs(x,ty,M)}) = 
15570  206 
let val (y,N) = variant_abs (getOpt (a,x),ty,M) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

207 
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

208 
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

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

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

211 

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

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

215 
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

216 

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

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

218 
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

219 
(Cterm {t=x, sign_ref=sign_ref2, T, maxidx=maxidx2}) = 
8291  220 
if T = dty then 
15797  221 
Cterm{t = f $ x, 
15087  222 
sign_ref=Sign.merge_refs(sign_ref1,sign_ref2), T=rty, 
8291  223 
maxidx=Int.max(maxidx1, maxidx2)} 
1516
96286c4e32de
removed mk_prop; added capply; simplified dest_abs
clasohm
parents:
1503
diff
changeset

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

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

15264
a881ad2e9edc
Changed function cabs to also allow abstraction over Vars.
berghofe
parents:
15087
diff
changeset

227 
fun cabs (Cterm {t=t1, sign_ref=sign_ref1, T=T1, maxidx=maxidx1}) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

228 
(Cterm {t=t2, sign_ref=sign_ref2, T=T2, maxidx=maxidx2}) = 
15797  229 
Cterm {t = lambda t1 t2, sign_ref = Sign.merge_refs (sign_ref1,sign_ref2), 
15264
a881ad2e9edc
Changed function cabs to also allow abstraction over Vars.
berghofe
parents:
15087
diff
changeset

230 
T = T1 > T2, maxidx=Int.max(maxidx1, maxidx2)} 
a881ad2e9edc
Changed function cabs to also allow abstraction over Vars.
berghofe
parents:
15087
diff
changeset

231 
handle TERM _ => raise CTERM "cabs: first arg is not a variable"; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

232 

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

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

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

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

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

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

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

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

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

241 
val maxidx = Int.max (maxidx1, maxidx2); 
15797  242 
fun mk_cTinsts (ixn, (S, T)) = 
243 
(Ctyp {sign_ref = sign_ref, T = TVar (ixn, S)}, 

244 
Ctyp {sign_ref = sign_ref, T = T}); 

245 
fun mk_ctinsts (ixn, (T, t)) = 

246 
let val T = Envir.typ_subst_TVars Tinsts T 

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

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

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

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

250 
end; 
15797  251 
in (map mk_cTinsts (Vartab.dest Tinsts), 
252 
map mk_ctinsts (Vartab.dest tinsts)) 

253 
end; 

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

254 

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

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

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

257 

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

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

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

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

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

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

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

264 

2509  265 

266 

574  267 
(** read cterms **) (*exception ERROR*) 
250  268 

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

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

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

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

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

277 

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

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

279 
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

280 
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

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

282 

15531  283 
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

284 

250  285 

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

288 

2509  289 

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

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

291 

11518  292 
structure Pt = Proofterm; 
293 

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

295 
{sign_ref: Sign.sg_ref, (*mutable reference to signature*) 
11518  296 
der: bool * Pt.proof, (*derivation*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

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

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

299 
hyps: term list, (*hypotheses*) 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

300 
tpairs: (term * term) list, (*flexflex pairs*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

301 
prop: term}; (*conclusion*) 
0  302 

16024  303 
fun terms_of_tpairs tpairs = List.concat (map (fn (t, u) => [t, u]) tpairs); 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

304 

c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

305 
fun attach_tpairs tpairs prop = 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

306 
Logic.list_implies (map Logic.mk_equals tpairs, prop); 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

307 

c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

308 
fun rep_thm (Thm {sign_ref, der, maxidx, shyps, hyps, tpairs, prop}) = 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

309 
{sign = Sign.deref sign_ref, der = der, maxidx = maxidx, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

310 
shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}; 
0  311 

1529  312 
(*Version of rep_thm returning cterms instead of terms*) 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

313 
fun crep_thm (Thm {sign_ref, der, maxidx, shyps, hyps, tpairs, prop}) = 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

314 
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

315 
in {sign = Sign.deref sign_ref, der = der, maxidx = maxidx, shyps = shyps, 
1529  316 
hyps = map (ctermf ~1) hyps, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

317 
tpairs = map (pairself (ctermf maxidx)) tpairs, 
1529  318 
prop = ctermf maxidx prop} 
1517  319 
end; 
320 

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

321 
(*errors involving theorems*) 
0  322 
exception THM of string * int * thm list; 
323 

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

326 

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

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

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

330 

3994  331 
fun eq_thm (th1, th2) = 
332 
let 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

333 
val {sign = sg1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1, prop = prop1, ...} = 
9031  334 
rep_thm th1; 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

335 
val {sign = sg2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...} = 
9031  336 
rep_thm th2; 
3994  337 
in 
9031  338 
Sign.joinable (sg1, sg2) andalso 
14791  339 
Sorts.eq_set_sort (shyps1, shyps2) andalso 
3994  340 
aconvs (hyps1, hyps2) andalso 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

341 
aconvs (terms_of_tpairs tpairs1, terms_of_tpairs tpairs2) andalso 
3994  342 
prop1 aconv prop2 
343 
end; 

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

344 

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

345 
fun sign_of_thm (Thm {sign_ref, ...}) = Sign.deref sign_ref; 
12803  346 
fun prop_of (Thm {prop, ...}) = prop; 
13528  347 
fun proof_of (Thm {der = (_, proof), ...}) = proof; 
0  348 

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

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

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

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

352 
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

353 

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

354 
(*transfer thm to super theory (nondestructive)*) 
4254  355 
fun transfer_sg sign' thm = 
3895  356 
let 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

357 
val Thm {sign_ref, der, maxidx, shyps, hyps, tpairs, prop} = thm; 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

358 
val sign = Sign.deref sign_ref; 
3895  359 
in 
4254  360 
if Sign.eq_sg (sign, sign') then thm 
361 
else if Sign.subsig (sign, sign') then 

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

362 
Thm {sign_ref = Sign.self_ref sign', der = der, maxidx = maxidx, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

363 
shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop} 
3895  364 
else raise THM ("transfer: not a super theory", 0, [thm]) 
365 
end; 

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

366 

6390  367 
val transfer = transfer_sg o Theory.sign_of; 
4254  368 

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

369 
(*maps objectrule to tpairs*) 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

370 
fun tpairs_of (Thm {tpairs, ...}) = tpairs; 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

371 

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

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

373 
fun prems_of (Thm {prop, ...}) = 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

374 
Logic.strip_imp_prems prop; 
0  375 

376 
(*counts premises in a rule*) 

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

377 
fun nprems_of (Thm {prop, ...}) = 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

378 
Logic.count_prems (prop, 0); 
0  379 

8299  380 
fun major_prem_of thm = 
381 
(case prems_of thm of 

11692  382 
prem :: _ => Logic.strip_assums_concl prem 
8299  383 
 [] => raise THM ("major_prem_of: rule with no premises", 0, [thm])); 
384 

7534  385 
fun no_prems thm = nprems_of thm = 0; 
386 

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

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

388 
fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop; 
0  389 

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

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

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

392 
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

393 

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

394 

0  395 

1238  396 
(** sort contexts of theorems **) 
397 

398 
(* basic utils *) 

399 

2163  400 
(*accumulate sorts suppressing duplicates; these are coded low levelly 
1238  401 
to improve efficiency a bit*) 
402 

403 
fun add_typ_sorts (Type (_, Ts), Ss) = add_typs_sorts (Ts, Ss) 

14791  404 
 add_typ_sorts (TFree (_, S), Ss) = Sorts.ins_sort(S,Ss) 
405 
 add_typ_sorts (TVar (_, S), Ss) = Sorts.ins_sort(S,Ss) 

1238  406 
and add_typs_sorts ([], Ss) = Ss 
407 
 add_typs_sorts (T :: Ts, Ss) = add_typs_sorts (Ts, add_typ_sorts (T, Ss)); 

408 

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

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

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

412 
 add_term_sorts (Bound _, Ss) = Ss 

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

413 
 add_term_sorts (Abs (_,T,t), Ss) = add_term_sorts (t, add_typ_sorts (T,Ss)) 
1238  414 
 add_term_sorts (t $ u, Ss) = add_term_sorts (t, add_term_sorts (u, Ss)); 
415 

416 
fun add_terms_sorts ([], Ss) = Ss 

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

417 
 add_terms_sorts (t::ts, Ss) = add_terms_sorts (ts, add_term_sorts (t,Ss)); 
1238  418 

15797  419 
fun env_codT (Envir.Envir {iTs, ...}) = map (snd o snd) (Vartab.dest iTs); 
1258  420 

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

421 
fun add_env_sorts (Envir.Envir {iTs, asol, ...}, Ss) = 
15797  422 
Vartab.foldl (add_term_sorts o swap o apsnd (snd o snd)) 
423 
(Vartab.foldl (add_typ_sorts o swap o apsnd (snd o snd)) (Ss, iTs), asol); 

1258  424 

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

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

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

427 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

428 
fun add_thm_sorts (Thm {hyps, tpairs, prop, ...}, Ss) = 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

429 
add_terms_sorts (hyps @ terms_of_tpairs tpairs, add_term_sorts (prop, Ss)); 
1238  430 

431 
fun add_thms_shyps ([], Ss) = Ss 

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

14791  433 
add_thms_shyps (ths, Sorts.union_sort (shyps, Ss)); 
1238  434 

435 

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

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

14791  438 
Sorts.rems_sort (shyps, add_thm_sorts (th, [])); 
1238  439 

440 

441 
(* fix_shyps *) 

442 

15570  443 
fun all_sorts_nonempty sign_ref = isSome (Sign.universal_witness (Sign.deref sign_ref)); 
7642  444 

1238  445 
(*preserve sort contexts of rule premises and substituted types*) 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

446 
fun fix_shyps thms Ts (thm as Thm {sign_ref, der, maxidx, hyps, tpairs, prop, ...}) = 
7642  447 
Thm 
448 
{sign_ref = sign_ref, 

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

450 
maxidx = maxidx, 

451 
shyps = 

452 
if all_sorts_nonempty sign_ref then [] 

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

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

454 
hyps = hyps, tpairs = tpairs, prop = prop} 
1238  455 

456 

7642  457 
(* strip_shyps *) 
1238  458 

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

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

461 
 strip_shyps (thm as Thm {sign_ref, der, maxidx, shyps, hyps, tpairs, prop}) = 
7642  462 
let 
463 
val sign = Sign.deref sign_ref; 

1238  464 

7642  465 
val present_sorts = add_thm_sorts (thm, []); 
14791  466 
val extra_shyps = Sorts.rems_sort (shyps, present_sorts); 
7642  467 
val witnessed_shyps = Sign.witness_sorts sign present_sorts extra_shyps; 
468 
in 

469 
Thm {sign_ref = sign_ref, der = der, maxidx = maxidx, 

14791  470 
shyps = Sorts.rems_sort (shyps, map #2 witnessed_shyps), 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

471 
hyps = hyps, tpairs = tpairs, prop = prop} 
7642  472 
end; 
1238  473 

474 

475 

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

477 

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

478 
(*look up the named axiom in the theory*) 
15672  479 
fun get_axiom_i theory name = 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

480 
let 
15531  481 
fun get_ax [] = NONE 
1529  482 
 get_ax (thy :: thys) = 
4847  483 
let val {sign, axioms, ...} = Theory.rep_theory thy in 
484 
(case Symtab.lookup (axioms, name) of 

15531  485 
SOME t => 
486 
SOME (fix_shyps [] [] 

4847  487 
(Thm {sign_ref = Sign.self_ref sign, 
11518  488 
der = Pt.infer_derivs' I 
489 
(false, Pt.axm_proof name t), 

4847  490 
maxidx = maxidx_of_term t, 
491 
shyps = [], 

492 
hyps = [], 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

493 
tpairs = [], 
4847  494 
prop = t})) 
15531  495 
 NONE => get_ax thys) 
1529  496 
end; 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

497 
in 
4847  498 
(case get_ax (theory :: Theory.ancestors_of theory) of 
15531  499 
SOME thm => thm 
500 
 NONE => raise THEORY ("No axiom " ^ quote name, [theory])) 

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

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

502 

15672  503 
fun get_axiom thy = get_axiom_i thy o Sign.intern (Theory.sign_of thy) Theory.axiomK; 
504 

6368  505 
fun def_name name = name ^ "_def"; 
506 
fun get_def thy = get_axiom thy o def_name; 

4847  507 

1529  508 

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

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

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

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

513 

6089  514 

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

516 

12923  517 
fun get_name_tags (Thm {hyps, prop, der = (_, prf), ...}) = 
518 
Pt.get_name_tags hyps prop prf; 

4018  519 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

520 
fun put_name_tags x (Thm {sign_ref, der = (ora, prf), maxidx, 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

521 
shyps, hyps, tpairs = [], prop}) = Thm {sign_ref = sign_ref, 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

522 
der = (ora, Pt.thm_proof (Sign.deref sign_ref) x hyps prop prf), 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

523 
maxidx = maxidx, shyps = shyps, hyps = hyps, tpairs = [], prop = prop} 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

524 
 put_name_tags _ thm = 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

525 
raise THM ("put_name_tags: unsolved flexflex constraints", 0, [thm]); 
6089  526 

527 
val name_of_thm = #1 o get_name_tags; 

528 
val tags_of_thm = #2 o get_name_tags; 

529 

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

0  531 

532 

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

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

535 
fun compress (Thm {sign_ref, der, maxidx, shyps, hyps, tpairs, prop}) = 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

536 
Thm {sign_ref = sign_ref, 
2386  537 
der = der, (*No derivation recorded!*) 
538 
maxidx = maxidx, 

539 
shyps = shyps, 

540 
hyps = map Term.compress_term hyps, 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

541 
tpairs = map (pairself Term.compress_term) tpairs, 
2386  542 
prop = Term.compress_term prop}; 
564  543 

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

544 

2509  545 

1529  546 
(*** Meta rules ***) 
0  547 

1220  548 
(** 'primitive' rules **) 
549 

550 
(*discharge all assumptions t from ts*) 

0  551 
val disch = gen_rem (op aconv); 
552 

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

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

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

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

561 
else Thm{sign_ref = sign_ref, 
11518  562 
der = Pt.infer_derivs' I (false, Pt.Hyp prop), 
2386  563 
maxidx = ~1, 
564 
shyps = add_term_sorts(prop,[]), 

565 
hyps = [prop], 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

566 
tpairs = [], 
2386  567 
prop = prop} 
0  568 
end; 
569 

1220  570 
(*Implication introduction 
3529  571 
[A] 
572 
: 

573 
B 

1220  574 
 
575 
A ==> B 

576 
*) 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

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

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

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

582 
Thm{sign_ref = Sign.merge_refs (sign_ref,sign_refA), 
11518  583 
der = Pt.infer_derivs' (Pt.implies_intr_proof A) der, 
2386  584 
maxidx = Int.max(maxidxA, maxidx), 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

585 
shyps = add_term_sorts (A, shyps), 
2386  586 
hyps = disch(hyps,A), 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

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

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

591 
end; 

592 

1529  593 

1220  594 
(*Implication elimination 
595 
A ==> B A 

596 
 

597 
B 

598 
*) 

0  599 
fun implies_elim thAB thA : thm = 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

600 
let val Thm{maxidx=maxA, der=derA, hyps=hypsA, shyps=shypsA, tpairs=tpairsA, prop=propA, ...} = thA 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

601 
and Thm{der, maxidx, hyps, shyps, tpairs, prop, ...} = thAB; 
250  602 
fun err(a) = raise THM("implies_elim: "^a, 0, [thAB,thA]) 
0  603 
in case prop of 
250  604 
imp$A$B => 
605 
if imp=implies andalso A aconv propA 

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

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

607 
Thm{sign_ref= merge_thm_sgs(thAB,thA), 
11612  608 
der = Pt.infer_derivs (curry Pt.%%) der derA, 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

609 
maxidx = Int.max(maxA,maxidx), 
14791  610 
shyps = Sorts.union_sort (shypsA, shyps), 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

611 
hyps = union_term(hypsA,hyps), (*dups suppressed*) 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

612 
tpairs = tpairsA @ tpairs, 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

613 
prop = B} 
250  614 
else err("major premise") 
615 
 _ => err("major premise") 

0  616 
end; 
250  617 

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

620 
 

621 
!!x.A 

622 
*) 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

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

624 
let val x = term_of cx; 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

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

626 
(Thm{sign_ref = sign_ref, 
11518  627 
der = Pt.infer_derivs' (Pt.forall_intr_proof x a) der, 
2386  628 
maxidx = maxidx, 
629 
shyps = [], 

630 
hyps = hyps, 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

631 
tpairs = tpairs, 
2386  632 
prop = all(T) $ Abs(a, T, abstract_over (x,prop))}) 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

633 
fun check_occs x ts = 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

634 
if exists (apl(x, Logic.occs)) ts 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

635 
then raise THM("forall_intr: variable free in assumptions", 0, [th]) 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

636 
else () 
0  637 
in case x of 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

638 
Free(a,T) => (check_occs x (hyps @ terms_of_tpairs tpairs); result a T) 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

639 
 Var((a,_),T) => (check_occs x (terms_of_tpairs tpairs); result a T) 
0  640 
 _ => raise THM("forall_intr: not a variable", 0, [th]) 
641 
end; 

642 

1220  643 
(*Forall elimination 
644 
!!x.A 

645 
 

646 
A[t/x] 

647 
*) 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

648 
fun forall_elim ct (th as Thm{sign_ref,der,maxidx,hyps,tpairs,prop,...}) : thm = 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

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

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

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

655 
(Thm{sign_ref= Sign.merge_refs(sign_ref,sign_reft), 
15531  656 
der = Pt.infer_derivs' (Pt.% o rpair (SOME t)) der, 
2386  657 
maxidx = Int.max(maxidx, maxt), 
658 
shyps = [], 

659 
hyps = hyps, 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

660 
tpairs = tpairs, 
2386  661 
prop = betapply(A,t)}) 
2147  662 
 _ => raise THM("forall_elim: not quantified", 0, [th]) 
0  663 
end 
664 
handle TERM _ => 

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

667 

1220  668 
(* Equality *) 
0  669 

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

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

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

673 
in Thm{sign_ref= sign_ref, 
11518  674 
der = Pt.infer_derivs' I (false, Pt.reflexive), 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

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

677 
maxidx = maxidx, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

678 
tpairs = [], 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

679 
prop = Logic.mk_equals(t,t)} 
0  680 
end; 
681 

682 
(*The symmetry rule 

1220  683 
t==u 
684 
 

685 
u==t 

686 
*) 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

687 
fun symmetric (th as Thm{sign_ref,der,maxidx,shyps,hyps,tpairs,prop}) = 
0  688 
case prop of 
11518  689 
(eq as Const("==", Type (_, [T, _]))) $ t $ u => 
1238  690 
(*no fix_shyps*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

691 
Thm{sign_ref = sign_ref, 
11518  692 
der = Pt.infer_derivs' Pt.symmetric der, 
2386  693 
maxidx = maxidx, 
694 
shyps = shyps, 

695 
hyps = hyps, 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

696 
tpairs = tpairs, 
2386  697 
prop = eq$u$t} 
0  698 
 _ => raise THM("symmetric", 0, [th]); 
699 

700 
(*The transitive rule 

1220  701 
t1==u u==t2 
702 
 

703 
t1==t2 

704 
*) 

0  705 
fun transitive th1 th2 = 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

706 
let val Thm{der=der1, maxidx=max1, hyps=hyps1, shyps=shyps1, tpairs=tpairs1, prop=prop1,...} = th1 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

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

11518  710 
((eq as Const("==", Type (_, [T, _]))) $ t1 $ u, Const("==",_) $ u' $ t2) => 
1634  711 
if not (u aconv u') then err"middle term" 
15797  712 
else 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

713 
Thm{sign_ref= merge_thm_sgs(th1,th2), 
11518  714 
der = Pt.infer_derivs (Pt.transitive u T) der1 der2, 
2147  715 
maxidx = Int.max(max1,max2), 
14791  716 
shyps = Sorts.union_sort (shyps1, shyps2), 
2386  717 
hyps = union_term(hyps1,hyps2), 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

718 
tpairs = tpairs1 @ tpairs2, 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

719 
prop = eq$t1$t2} 
0  720 
 _ => err"premises" 
721 
end; 

722 

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

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

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

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

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

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

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

729 
{sign_ref = sign_ref, 
11518  730 
der = Pt.infer_derivs' I (false, Pt.reflexive), 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

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

733 
hyps = [], 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

734 
tpairs = [], 
10486  735 
prop = Logic.mk_equals (t, if full then Envir.beta_norm t 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

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

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

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

740 

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

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

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

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

744 
{sign_ref = sign_ref, 
11518  745 
der = Pt.infer_derivs' I (false, Pt.reflexive), 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

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

748 
hyps = [], 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

749 
tpairs = [], 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

750 
prop = Logic.mk_equals (t, Pattern.eta_contract t)} 
0  751 
end; 
752 

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

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

1220  755 
t == u 
756 
 

757 
%x.t == %x.u 

758 
*) 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

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

760 
let val x = term_of cx; 
250  761 
val (t,u) = Logic.dest_equals prop 
762 
handle TERM _ => 

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

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

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

765 
Thm{sign_ref = sign_ref, 
11518  766 
der = Pt.infer_derivs' (Pt.abstract_rule x a) der, 
2386  767 
maxidx = maxidx, 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

768 
shyps = add_typ_sorts (T, shyps), 
2386  769 
hyps = hyps, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

770 
tpairs = tpairs, 
2386  771 
prop = Logic.mk_equals(Abs(a, T, abstract_over (x,t)), 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

772 
Abs(a, T, abstract_over (x,u)))} 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

773 
fun check_occs x ts = 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

774 
if exists (apl(x, Logic.occs)) ts 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

775 
then raise THM("abstract_rule: variable free in assumptions", 0, [th]) 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

776 
else () 
0  777 
in case x of 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

778 
Free(_,T) => (check_occs x (hyps @ terms_of_tpairs tpairs); result T) 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

779 
 Var(_,T) => (check_occs x (terms_of_tpairs tpairs); result T) 
0  780 
 _ => raise THM("abstract_rule: not a variable", 0, [th]) 
781 
end; 

782 

783 
(*The combination rule 

3529  784 
f == g t == u 
785 
 

786 
f(t) == g(u) 

1220  787 
*) 
0  788 
fun combination th1 th2 = 
1529  789 
let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

790 
tpairs=tpairs1, prop=prop1,...} = th1 
1529  791 
and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

792 
tpairs=tpairs2, prop=prop2,...} = th2 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

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

796 
if T1 <> tT then 
2386  797 
raise THM("combination: types", 0, [th1,th2]) 
798 
else () 

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

800 
[th1,th2])) 

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

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

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

803 
Const ("==", Type ("fun", [tT, _])) $ t $ u) => 
15797  804 
(chktypes fT tT; 
805 
(*no fix_shyps*) 

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

806 
Thm{sign_ref = merge_thm_sgs(th1,th2), 
11518  807 
der = Pt.infer_derivs 
808 
(Pt.combination f g t u fT) der1 der2, 

2386  809 
maxidx = Int.max(max1,max2), 
14791  810 
shyps = Sorts.union_sort(shyps1,shyps2), 
2386  811 
hyps = union_term(hyps1,hyps2), 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

812 
tpairs = tpairs1 @ tpairs2, 
15797  813 
prop = Logic.mk_equals(f$t, g$u)}) 
0  814 
 _ => raise THM("combination: premises", 0, [th1,th2]) 
815 
end; 

816 

817 

818 
(* Equality introduction 

3529  819 
A ==> B B ==> A 
820 
 

821 
A == B 

1220  822 
*) 
0  823 
fun equal_intr th1 th2 = 
11518  824 
let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

825 
tpairs=tpairs1, prop=prop1,...} = th1 
1529  826 
and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

827 
tpairs=tpairs2, prop=prop2,...} = th2; 
1529  828 
fun err(msg) = raise THM("equal_intr: "^msg, 0, [th1,th2]) 
829 
in case (prop1,prop2) of 

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

2386  831 
if A aconv A' andalso B aconv B' 
832 
then 

833 
(*no fix_shyps*) 

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

834 
Thm{sign_ref = merge_thm_sgs(th1,th2), 
11518  835 
der = Pt.infer_derivs (Pt.equal_intr A B) der1 der2, 
2386  836 
maxidx = Int.max(max1,max2), 
14791  837 
shyps = Sorts.union_sort(shyps1,shyps2), 
2386  838 
hyps = union_term(hyps1,hyps2), 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

839 
tpairs = tpairs1 @ tpairs2, 
2386  840 
prop = Logic.mk_equals(A,B)} 
841 
else err"not equal" 

1529  842 
 _ => err"premises" 
843 
end; 

844 

845 

846 
(*The equal propositions rule 

3529  847 
A == B A 
1529  848 
 
849 
B 

850 
*) 

851 
fun equal_elim th1 th2 = 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

852 
let val Thm{der=der1, maxidx=max1, hyps=hyps1, tpairs=tpairs1, prop=prop1,...} = th1 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

853 
and Thm{der=der2, maxidx=max2, hyps=hyps2, tpairs=tpairs2, prop=prop2,...} = th2; 
1529  854 
fun err(msg) = raise THM("equal_elim: "^msg, 0, [th1,th2]) 
855 
in case prop1 of 

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

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

858 
fix_shyps [th1, th2] [] 

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

859 
(Thm{sign_ref= merge_thm_sgs(th1,th2), 
11518  860 
der = Pt.infer_derivs (Pt.equal_elim A B) der1 der2, 
2386  861 
maxidx = Int.max(max1,max2), 
862 
shyps = [], 

863 
hyps = union_term(hyps1,hyps2), 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

864 
tpairs = tpairs1 @ tpairs2, 
2386  865 
prop = B}) 
1529  866 
 _ => err"major premise" 
867 
end; 

0  868 

1220  869 

870 

0  871 
(**** Derived rules ****) 
872 

1503  873 
(*Discharge all hypotheses. Need not verify cterms or call fix_shyps. 
0  874 
Repeated hypotheses are discharged only once; fold cannot do this*) 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

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

877 
(Thm{sign_ref = sign_ref, 
11518  878 
der = Pt.infer_derivs' (Pt.implies_intr_proof A) der, 
2386  879 
maxidx = maxidx, 
880 
shyps = shyps, 

1529  881 
hyps = disch(As,A), 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

882 
tpairs = tpairs, 
2386  883 
prop = implies$A$prop}) 
0  884 
 implies_intr_hyps th = th; 
885 

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

250  887 
Instantiates the theorem and deletes trivial tpairs. 
0  888 
Resulting sequence may contain multiple elements if the tpairs are 
889 
not all flexflex. *) 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

890 
fun flexflex_rule (th as Thm{sign_ref, der, maxidx, hyps, tpairs, prop, ...}) = 
250  891 
let fun newthm env = 
1529  892 
if Envir.is_empty env then th 
893 
else 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

894 
let val ntpairs = map (pairself (Envir.norm_term env)) tpairs; 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

895 
val newprop = Envir.norm_term env prop; 
250  896 
(*Remove trivial tpairs, of the form t=t*) 
15570  897 
val distpairs = List.filter (not o op aconv) ntpairs 
1220  898 
in fix_shyps [th] (env_codT env) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

899 
(Thm{sign_ref = sign_ref, 
11518  900 
der = Pt.infer_derivs' (Pt.norm_proof' env) der, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

901 
maxidx = maxidx_of_terms (newprop :: 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

902 
terms_of_tpairs distpairs), 
2386  903 
shyps = [], 
904 
hyps = hyps, 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

905 
tpairs = distpairs, 
2386  906 
prop = newprop}) 
250  907 
end; 
4270  908 
in Seq.map newthm 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

909 
(Unify.smash_unifiers(Sign.deref sign_ref, Envir.empty maxidx, tpairs)) 
0  910 
end; 
911 

912 
(*Instantiation of Vars 

1220  913 
A 
914 
 

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

916 
*) 

0  917 

6928  918 
local 
919 

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

922 

6928  923 
fun prt_typing sg_ref t T = 
924 
let val sg = Sign.deref sg_ref in 

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

926 
end; 

927 

15797  928 
fun prt_type sg_ref T = Sign.pretty_typ (Sign.deref sg_ref) T; 
929 

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

931 
fun add_ctpair ((ct,cu), (sign_ref,tpairs)) = 
6928  932 
let 
933 
val Cterm {sign_ref=sign_reft, t=t, T= T, ...} = ct 

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

935 
val sign_ref_merged = Sign.merge_refs (sign_ref, Sign.merge_refs (sign_reft, sign_refu)); 

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

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

939 
Pretty.fbrk, prt_typing sign_ref_merged t T, 

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

0  941 
end; 
942 

15797  943 
fun add_ctyp ((Ctyp {T = T as TVar (_, S), sign_ref = sign_refT}, 
944 
Ctyp {T = U, sign_ref = sign_refU}), (sign_ref, vTs)) = 

945 
let 

946 
val sign_ref_merged = Sign.merge_refs 

947 
(sign_ref, Sign.merge_refs (sign_refT, sign_refU)); 

948 
val sign = Sign.deref sign_ref_merged 

949 
in 

950 
if Type.of_sort (Sign.tsig_of sign) (U, S) then 

951 
(sign_ref_merged, (T, U) :: vTs) 

952 
else raise TYPE ("Type not of sort " ^ 

953 
Sign.string_of_sort sign S, [U], []) 

954 
end 

955 
 add_ctyp ((Ctyp {T, sign_ref}, _), _) = 

956 
raise TYPE (Pretty.string_of (Pretty.block 

957 
[Pretty.str "instantiate: not a type variable", 

958 
Pretty.fbrk, prt_type sign_ref T]), [T], []); 

0  959 

6928  960 
in 
961 

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

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

964 
No longer normalizes the new theorem! *) 
1529  965 
fun instantiate ([], []) th = th 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

966 
 instantiate (vcTs,ctpairs) (th as Thm{sign_ref,der,maxidx,hyps,shyps,tpairs=dpairs,prop}) = 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

967 
let val (newsign_ref,tpairs) = foldr add_ctpair (sign_ref,[]) ctpairs; 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

968 
val (newsign_ref,vTs) = foldr add_ctyp (newsign_ref,[]) vcTs; 
14828  969 
fun subst t = 
15797  970 
subst_atomic tpairs (map_term_types (typ_subst_atomic vTs) t); 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

971 
val newprop = subst prop; 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

972 
val newdpairs = map (pairself subst) dpairs; 
1220  973 
val newth = 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

974 
(Thm{sign_ref = newsign_ref, 
11518  975 
der = Pt.infer_derivs' (Pt.instantiate vTs tpairs) der, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

976 
maxidx = maxidx_of_terms (newprop :: 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

977 
terms_of_tpairs newdpairs), 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

979 
hyps = hyps, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

980 
tpairs = newdpairs, 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

981 
prop = newprop}) 
250  982 
in if not(instl_ok(map #1 tpairs)) 
193  983 
then raise THM("instantiate: variables not distinct", 0, [th]) 
984 
else if not(null(findrep(map #1 vTs))) 

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

15797  986 
else newth 
0  987 
end 
6928  988 
handle TERM _ => raise THM("instantiate: incompatible signatures", 0, [th]) 
989 
 TYPE (msg, _, _) => raise THM (msg, 0, [th]); 

990 

991 
end; 

992 

0  993 

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

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

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

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

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

1001 
(Thm{sign_ref = sign_ref, 
15531  1002 
der = Pt.infer_derivs' I (false, Pt.AbsP ("H", NONE, Pt.PBound 0)), 
2386  1003 
maxidx = maxidx, 
1004 
shyps = [], 

1005 
hyps = [], 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1006 
tpairs = [], 
2386  1007 
prop = implies$A$A}) 
0  1008 
end; 
1009 

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

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

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

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

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

1017 
(Thm {sign_ref = sign_ref, 
11518  1018 
der = Pt.infer_derivs' I 
15531  1019 
(false, Pt.PAxm ("ProtoPure.class_triv:" ^ c, t, SOME [])), 
2386  1020 
maxidx = maxidx, 
1021 
shyps = [], 

1022 
hyps = [], 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1023 
tpairs = [], 
2386  1024 
prop = t}) 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

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

1026 

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

1027 

6786  1028 
(* Replace all TFrees not fixed or in the hyps by new TVars *) 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1029 
fun varifyT' fixed (Thm{sign_ref,der,maxidx,shyps,hyps,tpairs,prop}) = 
12500  1030 
let 
15797  1031 
val tfrees = foldr add_term_tfrees fixed hyps; 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1032 
val prop1 = attach_tpairs tpairs prop; 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1033 
val (prop2, al) = Type.varify (prop1, tfrees); 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1034 
val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2) 
15797  1035 
in (*no fix_shyps*) 
1036 
(Thm{sign_ref = sign_ref, 

11518  1037 
der = Pt.infer_derivs' (Pt.varify_proof prop tfrees) der, 
2386  1038 
maxidx = Int.max(0,maxidx), 
1039 
shyps = shyps, 

1040 
hyps = hyps, 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1041 
tpairs = rev (map Logic.dest_equals ts), 
15797  1042 
prop = prop3}, al) 
0  1043 
end; 
1044 

12500  1045 
val varifyT = #1 o varifyT' []; 
6786  1046 

0  1047 
(* Replace all TVars by new TFrees *) 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1048 
fun freezeT(Thm{sign_ref,der,maxidx,shyps,hyps,tpairs,prop}) = 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1049 
let 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1050 
val prop1 = attach_tpairs tpairs prop; 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1051 
val (prop2, _) = Type.freeze_thaw prop1; 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1052 
val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2) 
1238  1053 
in (*no fix_shyps*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

1054 
Thm{sign_ref = sign_ref, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1055 
der = Pt.infer_derivs' (Pt.freezeT prop1) der, 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1056 
maxidx = maxidx_of_term prop2, 
2386  1057 
shyps = shyps, 
1058 
hyps = hyps, 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1059 
tpairs = rev (map Logic.dest_equals ts), 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1060 
prop = prop3} 
1220  1061 
end; 
0  1062 

1063 

1064 
(*** Inference rules for tactics ***) 

1065 

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

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1067 
fun dest_state (state as Thm{prop,tpairs,...}, i) = 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1068 
(case Logic.strip_prems(i, [], prop) of 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1069 
(B::rBs, C) => (tpairs, rev rBs, B, C) 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1070 
 _ => raise THM("dest_state", i, [state])) 
0  1071 
handle TERM _ => raise THM("dest_state", i, [state]); 
1072 

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

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

1076 
let val Thm{shyps=sshyps, prop=sprop, maxidx=smax, sign_ref=ssign_ref,...} = state 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1077 
val (Bi::_, _) = Logic.strip_prems(i, [], sprop) 
1529  1078 
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

1079 
val ct_Bi = Cterm {sign_ref=ssign_ref, maxidx=smax, T=propT, t=Bi} 
1529  1080 
val (lift_abs,lift_all) = Logic.lift_fns(Bi,smax+1) 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1081 
val (Thm{sign_ref, der, maxidx,shyps,hyps,tpairs,prop}) = orule 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1082 
val (As, B) = Logic.strip_horn prop 
1238  1083 
in (*no fix_shyps*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

1084 
Thm{sign_ref = merge_thm_sgs(state,orule), 
11518  1085 
der = Pt.infer_derivs' (Pt.lift_proof Bi (smax+1) prop) der, 
2386  1086 
maxidx = maxidx+smax+1, 
14791  1087 
shyps = Sorts.union_sort(sshyps,shyps), 
1088 
hyps = hyps, 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1089 
tpairs = map (pairself lift_abs) tpairs, 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1090 
prop = Logic.list_implies (map lift_all As, lift_all B)} 
0  1091 
end; 
1092 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

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

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

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

1096 
Thm {sign_ref = sign_ref, 
11518  1097 
der = Pt.infer_derivs' (Pt.map_proof_terms 
1098 
(Logic.incr_indexes ([], i)) (incr_tvar i)) der, 

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

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

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

1101 
hyps = hyps, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1102 
tpairs = map (pairself (Logic.incr_indexes ([], i))) tpairs, 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

1104 

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

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

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

1111 
(Thm{sign_ref = sign_ref, 
11518  1112 
der = Pt.infer_derivs' 
1113 
((if Envir.is_empty env then I else (Pt.norm_proof' env)) o 

1114 
Pt.assumption_proof Bs Bi n) der, 

2386  1115 
maxidx = maxidx, 
1116 
shyps = [], 

1117 
hyps = hyps, 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1118 
tpairs = if Envir.is_empty env then tpairs else 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1119 
map (pairself (Envir.norm_term env)) tpairs, 
2386  1120 
prop = 
1121 
if Envir.is_empty env then (*avoid wasted normalizations*) 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1122 
Logic.list_implies (Bs, C) 
2386  1123 
else (*normalize the new rule fully*) 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1124 
Envir.norm_term env (Logic.list_implies (Bs, C))}); 
11518  1125 
fun addprfs [] _ = Seq.empty 
1126 
 addprfs ((t,u)::apairs) n = Seq.make (fn()=> Seq.pull 

1127 
(Seq.mapp (newth n) 

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

1128 
(Unify.unifiers(Sign.deref sign_ref,Envir.empty maxidx, (t,u)::tpairs)) 
11518  1129 
(addprfs apairs (n+1)))) 
15454  1130 
in addprfs (Logic.assum_pairs (~1,Bi)) 1 end; 
0  1131 

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

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

1135 
let val Thm{sign_ref,der,maxidx,hyps,prop,...} = state; 
0  1136 
val (tpairs, Bs, Bi, C) = dest_state(state,i) 
15454  1137 
in (case find_index (op aconv) (Logic.assum_pairs (~1,Bi)) of 
11518  1138 
(~1) => raise THM("eq_assumption", 0, [state]) 
1139 
 n => fix_shyps [state] [] 

1140 
(Thm{sign_ref = sign_ref, 

1141 
der = Pt.infer_derivs' 

1142 
(Pt.assumption_proof Bs Bi (n+1)) der, 

1143 
maxidx = maxidx, 

1144 
shyps = [], 

1145 
hyps = hyps, 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1146 
tpairs = tpairs, 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1147 
prop = Logic.list_implies (Bs, C)})) 
0  1148 
end; 
1149 

1150 

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

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1153 
let val Thm{sign_ref,der,maxidx,hyps,prop,shyps,...} = state; 
2671  1154 
val (tpairs, Bs, Bi, C) = dest_state(state,i) 
8066
54d37e491ac2
SOUNDNESS BUG FIX for rotate_rule. The original code did not expect
paulson
parents:
7921
diff
changeset

1155 
val params = Term.strip_all_vars Bi 
54d37e491ac2
SOUNDNESS BUG FIX for rotate_rule. The original code did not expect
paulson
parents:
7921
diff
changeset

1156 
and rest = Term.strip_all_body Bi 
54d37e491ac2
SOUNDNESS BUG FIX for rotate_rule. The original code did not expect
paulson
parents:
7921
diff
changeset

1157 
val asms = Logic.strip_imp_prems rest 
54d37e491ac2
SOUNDNESS BUG FIX for rotate_rule. The original code did not expect
paulson
parents:
7921
diff
changeset

1158 
and concl = Logic.strip_imp_concl rest 
2671  1159 
val n = length asms 
11563  1160 
val m = if k<0 then n+k else k 
1161 
val Bi' = if 0=m orelse m=n then Bi 

2671  1162 
else if 0<m andalso m<n 
13629  1163 
then let val (ps,qs) = splitAt(m,asms) 
1164 
in list_all(params, Logic.list_implies(qs @ ps, concl)) 

1165 
end 

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

1166 
else raise THM("rotate_rule", k, [state]) 
7264  1167 
in (*no fix_shyps*) 
1168 
Thm{sign_ref = sign_ref, 

11563  1169 
der = Pt.infer_derivs' (Pt.rotate_proof Bs Bi m) der, 
2671  1170 
maxidx = maxidx, 
1171 
shyps = shyps, 

1172 
hyps = hyps, 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1173 
tpairs = tpairs, 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1174 
prop = Logic.list_implies (Bs @ [Bi'], C)} 
2671  1175 
end; 
1176 

1177 

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

1178 
(*Rotates a rule's premises to the left by k, leaving the first j premises 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1179 
unchanged. Does nothing if k=0 or if k equals nj, where n is the 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1180 
number of premises. Useful with etac and underlies tactic/defer_tac*) 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1181 
fun permute_prems j k rl = 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1182 
let val Thm{sign_ref,der,maxidx,hyps,tpairs,prop,shyps} = rl 
7248
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1183 
val prems = Logic.strip_imp_prems prop 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1184 
and concl = Logic.strip_imp_concl prop 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1185 
val moved_prems = List.drop(prems, j) 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1186 
and fixed_prems = List.take(prems, j) 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1187 
handle Subscript => raise THM("permute_prems:j", j, [rl]) 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

1188 
val n_j = length moved_prems 
11563  1189 
val m = if k<0 then n_j + k else k 
1190 
val prop' = if 0 = m orelse m = n_j then prop 

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

1191 
else if 0<m andalso m<n_j 
13629  1192 
then let val (ps,qs) = splitAt(m,moved_prems) 
1193 
in Logic.list_implies(fixed_prems @ qs @ ps, concl) end 

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

1194 
else raise THM("permute_prems:k", k, [rl]) 
7264  1195 
in (*no fix_shyps*) 
1196 
Thm{sign_ref = sign_ref, 

11563  1197 
der = Pt.infer_derivs' (Pt.permute_prems_prf prems j m) der, 
7248
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

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

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

1200 
hyps = hyps, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1201 
tpairs = tpairs, 
11563  1202 
prop = prop'} 
7248
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

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

1204 

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

1205 

0  1206 
(** User renaming of parameters in a subgoal **) 
1207 

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

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

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

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

1212 
fun rename_params_rule (cs, i) state = 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

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

1216 
val short = length iparams  length cs 

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

15570  1219 
else variantlist(Library.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

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

1224 
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

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

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

1227 
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

1228 
state) 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1229 
 [] => Thm{sign_ref = sign_ref, 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1230 
der = der, 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1231 
maxidx = maxidx, 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1232 
shyps = shyps, 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1233 
hyps = hyps, 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1234 
tpairs = tpairs, 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1235 
prop = Logic.list_implies (Bs @ [newBi], C)}) 
0  1236 
end; 
1237 

12982  1238 

0  1239 
(*** Preservation of bound variable names ***) 
1240 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1241 
fun rename_boundvars pat obj (thm as Thm {sign_ref, der, maxidx, hyps, shyps, tpairs, prop}) = 
12982  1242 
(case Term.rename_abs pat obj prop of 
15531  1243 
NONE => thm 
1244 
 SOME prop' => Thm 

12982  1245 
{sign_ref = sign_ref, 
1246 
der = der, 

1247 
maxidx = maxidx, 

1248 
hyps = hyps, 

1249 
shyps = shyps, 

13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

1250 
tpairs = tpairs, 
12982  1251 
prop = prop'}); 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

1252 

0  1253 

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

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

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

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

1261 
 strip(A,_) = f A 

0  1262 
in strip end; 
1263 

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

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

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

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

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

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

1269 
let val vars = foldr add_term_vars [] 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

1270 
(map fst dpairs @ map fst tpairs @ map snd tpairs) 
250  1271 
(*unknowns appearing elsewhere be preserved!*) 
1272 
val vids = map (#1 o #1 o dest_Var) vars; 

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

1274 
(case assoc(al,x) of 

15531  1275 
SOME(y) => if x mem_string vids orelse y mem_string vids then t 
250  1276 
else Var((y,i),T) 
15531  1277 
 NONE=> t) 
0  1278 
 rename(Abs(x,T,t)) = 
15570  1279 
Abs(getOpt(assoc_string(al,x),x), T, rename t) 
0  1280 
 rename(f$t) = rename f $ rename t 
1281 
 rename(t) = t; 

250  1282 
fun strip_ren Ai = strip_apply rename (Ai,B) 
0  1283 
in strip_ren end; 
1284 

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

1286 
fun rename_bvars(dpairs, tpairs, B) = 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

1287 
rename_bvs(foldr Term.match_bvars [] dpairs, dpairs, tpairs, B); 
0  1288 

1289 

1290 
(*** RESOLUTION ***) 

1291 

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

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

1293 

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

250  1296 
fun strip_assums2 (Const("==>", _) $ _ $ B1, 
1297 
Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2) 

0  1298 
 strip_assums2 (Const("all",_)$Abs(a,T,t1), 
250  1299 
Const("all",_)$Abs(_,_,t2)) = 
0  1300 
let val (B1,B2) = strip_assums2 (t1,t2) 
1301 
in (Abs(a,T,B1), Abs(a,T,B2)) end 

1302 
 strip_assums2 BB = BB; 

1303 

1304 

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

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

1306 
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

1307 
 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

1308 
let val Envir.Envir{iTs, ...} = env 
15797  1309 
val T' = Envir.typ_subst_TVars iTs T 
1238  1310 
(*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

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

1312 
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

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

1315 
 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

1316 

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

1317 

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

1322 
If eres_flg then simultaneously proves A1 by assumption. 

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

4270  1326 
local exception COMPOSE 
0  1327 
in 
250  1328 
fun bicompose_aux match (state, (stpairs, Bs, Bi, C), lifted) 
0  1329 
(eres_flg, orule, nsubgoal) = 
1529  1330 
let val Thm{der=sder, maxidx=smax, shyps=sshyps, hyps=shyps, ...} = state 