author  wenzelm 
Tue, 31 May 2005 11:53:26 +0200  
changeset 16135  c66545fe72bf 
parent 16024  ffe25459c72a 
child 16287  7a03b4b4df67 
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 
16135  51 
val eq_thms : thm list * thm list > bool 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

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

59 
val nprems_of : thm > int 

60 
val concl_of : thm > term 

61 
val cprop_of : thm > cterm 

62 
val extra_shyps : thm > sort list 

63 
val strip_shyps : thm > thm 

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

70 
(*meta rules*) 

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

75 
val forall_intr : cterm > thm > thm 

76 
val forall_elim : cterm > thm > thm 

77 
val reflexive : cterm > thm 

78 
val symmetric : thm > thm 

79 
val transitive : thm > thm > thm 

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

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

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

84 
val equal_intr : thm > thm > thm 

85 
val equal_elim : thm > thm > thm 

86 
val implies_intr_hyps : thm > thm 

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

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

98 
val incr_indexes : int > thm > thm 
4270  99 
val assumption : int > thm > thm Seq.seq 
1238  100 
val eq_assumption : int > thm > thm 
2671  101 
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

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

6089  112 
signature THM = 
113 
sig 

114 
include BASIC_THM 

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

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

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

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

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

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

125 
val get_name_tags : thm > string * tag list 

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

127 
val name_of_thm : thm > string 

128 
val tags_of_thm : thm > tag list 

129 
val name_thm : string * thm > thm 

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

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

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

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

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

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

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

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

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

143 

250  144 
(** certified types **) 
145 

146 
(*certified typs under a signature*) 

147 

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

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

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

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

153 
fun ctyp_of sign T = 

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

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

156 
fun read_ctyp sign s = 

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

158 

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

161 
 dest_ctyp ct = [ct]; 

162 

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

163 

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

164 

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

166 

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

168 

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

169 
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

170 

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

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

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

173 

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

176 
maxidx = maxidx}; 

177 

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

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

181 

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

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

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

14828  186 
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

187 
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

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

189 

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

190 

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

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

192 

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

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

194 
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

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

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

197 
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

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

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

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

201 
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

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

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

204 

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

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

206 
fun dest_abs a (Cterm {sign_ref, T as Type("fun",[_,S]), maxidx, t=Abs(x,ty,M)}) = 
15570  207 
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

208 
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

209 
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

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

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

212 

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

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

216 
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

217 

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

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

219 
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

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

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

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

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

228 
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

229 
(Cterm {t=t2, sign_ref=sign_ref2, T=T2, maxidx=maxidx2}) = 
15797  230 
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

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

232 
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

233 

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

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

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

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

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

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

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

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

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

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

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

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

247 
let val T = Envir.typ_subst_TVars Tinsts T 

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

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

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

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

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

254 
end; 

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

255 

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

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

257 
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

258 

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

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

260 
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

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

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

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

264 
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

265 

2509  266 

267 

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

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

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

271 
fun read_def_cterms (sign, types, sorts) used freeze sTs = 
250  272 
let 
8608  273 
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

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

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

278 

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

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

280 
fun read_def_cterm args used freeze aT = 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

281 
let val ([ct],tye) = read_def_cterms args used freeze [aT] 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

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

283 

15531  284 
fun read_cterm sign = #1 o read_def_cterm (sign, K NONE, K NONE) [] true; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

285 

250  286 

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

289 

2509  290 

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

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

292 

11518  293 
structure Pt = Proofterm; 
294 

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

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

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

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

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

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

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

16024  304 
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

305 

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

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

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

308 

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

309 
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

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

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

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

314 
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

315 
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

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

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

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

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

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

327 

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

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

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

331 

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

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

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

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

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

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

345 

16135  346 
val eq_thms = Library.equal_lists eq_thm; 
347 

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

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

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

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

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

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

355 
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

356 

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

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

360 
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

361 
val sign = Sign.deref sign_ref; 
3895  362 
in 
4254  363 
if Sign.eq_sg (sign, sign') then thm 
364 
else if Sign.subsig (sign, sign') then 

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

365 
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

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

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

369 

6390  370 
val transfer = transfer_sg o Theory.sign_of; 
4254  371 

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

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

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

374 

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

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

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

377 
Logic.strip_imp_prems prop; 
0  378 

379 
(*counts premises in a rule*) 

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

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

381 
Logic.count_prems (prop, 0); 
0  382 

8299  383 
fun major_prem_of thm = 
384 
(case prems_of thm of 

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

7534  388 
fun no_prems thm = nprems_of thm = 0; 
389 

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

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

391 
fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop; 
0  392 

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

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

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

395 
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

396 

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

397 

0  398 

1238  399 
(** sort contexts of theorems **) 
400 

401 
(* basic utils *) 

402 

2163  403 
(*accumulate sorts suppressing duplicates; these are coded low levelly 
1238  404 
to improve efficiency a bit*) 
405 

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

14791  407 
 add_typ_sorts (TFree (_, S), Ss) = Sorts.ins_sort(S,Ss) 
408 
 add_typ_sorts (TVar (_, S), Ss) = Sorts.ins_sort(S,Ss) 

1238  409 
and add_typs_sorts ([], Ss) = Ss 
410 
 add_typs_sorts (T :: Ts, Ss) = add_typs_sorts (Ts, add_typ_sorts (T, Ss)); 

411 

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

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

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

415 
 add_term_sorts (Bound _, Ss) = Ss 

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

416 
 add_term_sorts (Abs (_,T,t), Ss) = add_term_sorts (t, add_typ_sorts (T,Ss)) 
1238  417 
 add_term_sorts (t $ u, Ss) = add_term_sorts (t, add_term_sorts (u, Ss)); 
418 

419 
fun add_terms_sorts ([], Ss) = Ss 

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

420 
 add_terms_sorts (t::ts, Ss) = add_terms_sorts (ts, add_term_sorts (t,Ss)); 
1238  421 

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

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

424 
fun add_env_sorts (Envir.Envir {iTs, asol, ...}, Ss) = 
15797  425 
Vartab.foldl (add_term_sorts o swap o apsnd (snd o snd)) 
426 
(Vartab.foldl (add_typ_sorts o swap o apsnd (snd o snd)) (Ss, iTs), asol); 

1258  427 

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

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

429 
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

430 

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

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

432 
add_terms_sorts (hyps @ terms_of_tpairs tpairs, add_term_sorts (prop, Ss)); 
1238  433 

434 
fun add_thms_shyps ([], Ss) = Ss 

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

14791  436 
add_thms_shyps (ths, Sorts.union_sort (shyps, Ss)); 
1238  437 

438 

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

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

14791  441 
Sorts.rems_sort (shyps, add_thm_sorts (th, [])); 
1238  442 

443 

444 
(* fix_shyps *) 

445 

15570  446 
fun all_sorts_nonempty sign_ref = isSome (Sign.universal_witness (Sign.deref sign_ref)); 
7642  447 

1238  448 
(*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

449 
fun fix_shyps thms Ts (thm as Thm {sign_ref, der, maxidx, hyps, tpairs, prop, ...}) = 
7642  450 
Thm 
451 
{sign_ref = sign_ref, 

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

453 
maxidx = maxidx, 

454 
shyps = 

455 
if all_sorts_nonempty sign_ref then [] 

456 
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

457 
hyps = hyps, tpairs = tpairs, prop = prop} 
1238  458 

459 

7642  460 
(* strip_shyps *) 
1238  461 

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

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

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

1238  467 

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

472 
Thm {sign_ref = sign_ref, der = der, maxidx = maxidx, 

14791  473 
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

474 
hyps = hyps, tpairs = tpairs, prop = prop} 
7642  475 
end; 
1238  476 

477 

478 

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

480 

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

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

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

15531  488 
SOME t => 
489 
SOME (fix_shyps [] [] 

4847  490 
(Thm {sign_ref = Sign.self_ref sign, 
11518  491 
der = Pt.infer_derivs' I 
492 
(false, Pt.axm_proof name t), 

4847  493 
maxidx = maxidx_of_term t, 
494 
shyps = [], 

495 
hyps = [], 

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

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

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

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

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

505 

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

6368  508 
fun def_name name = name ^ "_def"; 
509 
fun get_def thy = get_axiom thy o def_name; 

4847  510 

1529  511 

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

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

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

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

516 

6089  517 

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

519 

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

4018  522 

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

523 
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

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

525 
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

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

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

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

530 
val name_of_thm = #1 o get_name_tags; 

531 
val tags_of_thm = #2 o get_name_tags; 

532 

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

0  534 

535 

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

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

538 
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

539 
Thm {sign_ref = sign_ref, 
2386  540 
der = der, (*No derivation recorded!*) 
541 
maxidx = maxidx, 

542 
shyps = shyps, 

543 
hyps = map Term.compress_term hyps, 

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

544 
tpairs = map (pairself Term.compress_term) tpairs, 
2386  545 
prop = Term.compress_term prop}; 
564  546 

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

547 

2509  548 

1529  549 
(*** Meta rules ***) 
0  550 

1220  551 
(** 'primitive' rules **) 
552 

553 
(*discharge all assumptions t from ts*) 

0  554 
val disch = gen_rem (op aconv); 
555 

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

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

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

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

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

568 
hyps = [prop], 

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

569 
tpairs = [], 
2386  570 
prop = prop} 
0  571 
end; 
572 

1220  573 
(*Implication introduction 
3529  574 
[A] 
575 
: 

576 
B 

1220  577 
 
578 
A ==> B 

579 
*) 

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

580 
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

581 
let val Cterm {sign_ref=sign_refA, t=A, T, maxidx=maxidxA} = cA 
0  582 
in if T<>propT then 
250  583 
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

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

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

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

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

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

594 
end; 

595 

1529  596 

1220  597 
(*Implication elimination 
598 
A ==> B A 

599 
 

600 
B 

601 
*) 

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

603 
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

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

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

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

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

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

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

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

616 
prop = B} 
250  617 
else err("major premise") 
618 
 _ => err("major premise") 

0  619 
end; 
250  620 

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

623 
 

624 
!!x.A 

625 
*) 

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

626 
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

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

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

629 
(Thm{sign_ref = sign_ref, 
11518  630 
der = Pt.infer_derivs' (Pt.forall_intr_proof x a) der, 
2386  631 
maxidx = maxidx, 
632 
shyps = [], 

633 
hyps = hyps, 

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

634 
tpairs = tpairs, 
2386  635 
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

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

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

638 
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

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

641 
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

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

645 

1220  646 
(*Forall elimination 
647 
!!x.A 

648 
 

649 
A[t/x] 

650 
*) 

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

651 
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

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

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

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

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

662 
hyps = hyps, 

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

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

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

670 

1220  671 
(* Equality *) 
0  672 

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

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

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

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

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

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

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

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

682 
prop = Logic.mk_equals(t,t)} 
0  683 
end; 
684 

685 
(*The symmetry rule 

1220  686 
t==u 
687 
 

688 
u==t 

689 
*) 

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

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

694 
Thm{sign_ref = sign_ref, 
11518  695 
der = Pt.infer_derivs' Pt.symmetric der, 
2386  696 
maxidx = maxidx, 
697 
shyps = shyps, 

698 
hyps = hyps, 

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

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

703 
(*The transitive rule 

1220  704 
t1==u u==t2 
705 
 

706 
t1==t2 

707 
*) 

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

709 
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

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

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

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

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

722 
prop = eq$t1$t2} 
0  723 
 _ => err"premises" 
724 
end; 

725 

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

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

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

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

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

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

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

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

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

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

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

737 
tpairs = [], 
10486  738 
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

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

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

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

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

743 

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

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

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

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

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

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

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

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

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

753 
prop = Logic.mk_equals (t, Pattern.eta_contract t)} 
0  754 
end; 
755 

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

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

1220  758 
t == u 
759 
 

760 
%x.t == %x.u 

761 
*) 

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

762 
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

763 
let val x = term_of cx; 
250  764 
val (t,u) = Logic.dest_equals prop 
765 
handle TERM _ => 

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

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

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

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

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

773 
tpairs = tpairs, 
2386  774 
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

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

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

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

778 
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

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

781 
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

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

785 

786 
(*The combination rule 

3529  787 
f == g t == u 
788 
 

789 
f(t) == g(u) 

1220  790 
*) 
0  791 
fun combination th1 th2 = 
1529  792 
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

793 
tpairs=tpairs1, prop=prop1,...} = th1 
1529  794 
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

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

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

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

799 
if T1 <> tT then 
2386  800 
raise THM("combination: types", 0, [th1,th2]) 
801 
else () 

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

803 
[th1,th2])) 

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

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

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

806 
Const ("==", Type ("fun", [tT, _])) $ t $ u) => 
15797  807 
(chktypes fT tT; 
808 
(*no fix_shyps*) 

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

809 
Thm{sign_ref = merge_thm_sgs(th1,th2), 
11518  810 
der = Pt.infer_derivs 
811 
(Pt.combination f g t u fT) der1 der2, 

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

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

819 

820 

821 
(* Equality introduction 

3529  822 
A ==> B B ==> A 
823 
 

824 
A == B 

1220  825 
*) 
0  826 
fun equal_intr th1 th2 = 
11518  827 
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

828 
tpairs=tpairs1, prop=prop1,...} = th1 
1529  829 
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

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

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

2386  834 
if A aconv A' andalso B aconv B' 
835 
then 

836 
(*no fix_shyps*) 

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

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

842 
tpairs = tpairs1 @ tpairs2, 
2386  843 
prop = Logic.mk_equals(A,B)} 
844 
else err"not equal" 

1529  845 
 _ => err"premises" 
846 
end; 

847 

848 

849 
(*The equal propositions rule 

3529  850 
A == B A 
1529  851 
 
852 
B 

853 
*) 

854 
fun equal_elim th1 th2 = 

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

855 
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

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

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

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

861 
fix_shyps [th1, th2] [] 

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

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

866 
hyps = union_term(hyps1,hyps2), 

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

867 
tpairs = tpairs1 @ tpairs2, 
2386  868 
prop = B}) 
1529  869 
 _ => err"major premise" 
870 
end; 

0  871 

1220  872 

873 

0  874 
(**** Derived rules ****) 
875 

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

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

880 
(Thm{sign_ref = sign_ref, 
11518  881 
der = Pt.infer_derivs' (Pt.implies_intr_proof A) der, 
2386  882 
maxidx = maxidx, 
883 
shyps = shyps, 

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

885 
tpairs = tpairs, 
2386  886 
prop = implies$A$prop}) 
0  887 
 implies_intr_hyps th = th; 
888 

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

250  890 
Instantiates the theorem and deletes trivial tpairs. 
0  891 
Resulting sequence may contain multiple elements if the tpairs are 
892 
not all flexflex. *) 

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

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

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

897 
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

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

902 
(Thm{sign_ref = sign_ref, 
11518  903 
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

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

905 
terms_of_tpairs distpairs), 
2386  906 
shyps = [], 
907 
hyps = hyps, 

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

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

912 
(Unify.smash_unifiers(Sign.deref sign_ref, Envir.empty maxidx, tpairs)) 
0  913 
end; 
914 

915 
(*Instantiation of Vars 

1220  916 
A 
917 
 

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

919 
*) 

0  920 

6928  921 
local 
922 

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

925 

6928  926 
fun prt_typing sg_ref t T = 
927 
let val sg = Sign.deref sg_ref in 

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

929 
end; 

930 

15797  931 
fun prt_type sg_ref T = Sign.pretty_typ (Sign.deref sg_ref) T; 
932 

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

934 
fun add_ctpair ((ct,cu), (sign_ref,tpairs)) = 
6928  935 
let 
936 
val Cterm {sign_ref=sign_reft, t=t, T= T, ...} = ct 

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

938 
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

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

942 
Pretty.fbrk, prt_typing sign_ref_merged t T, 

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

0  944 
end; 
945 

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

948 
let 

949 
val sign_ref_merged = Sign.merge_refs 

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

951 
val sign = Sign.deref sign_ref_merged 

952 
in 

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

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

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

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

957 
end 

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

959 
raise TYPE (Pretty.string_of (Pretty.block 

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

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

0  962 

6928  963 
in 
964 

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

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

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

969 
 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

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

971 
val (newsign_ref,vTs) = foldr add_ctyp (newsign_ref,[]) vcTs; 
14828  972 
fun subst t = 
15797  973 
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

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

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

977 
(Thm{sign_ref = newsign_ref, 
11518  978 
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

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

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

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

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

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

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

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

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

993 

994 
end; 

995 

0  996 

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

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

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

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

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

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

1008 
hyps = [], 

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

1009 
tpairs = [], 
2386  1010 
prop = implies$A$A}) 
0  1011 
end; 
1012 

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

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

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

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

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

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

1025 
hyps = [], 

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

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

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

1029 

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

1030 

6786  1031 
(* 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

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

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

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

1037 
val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2) 
15797  1038 
in (*no fix_shyps*) 
1039 
(Thm{sign_ref = sign_ref, 

11518  1040 
der = Pt.infer_derivs' (Pt.varify_proof prop tfrees) der, 
2386  1041 
maxidx = Int.max(0,maxidx), 
1042 
shyps = shyps, 

1043 
hyps = hyps, 

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

1044 
tpairs = rev (map Logic.dest_equals ts), 
15797  1045 
prop = prop3}, al) 
0  1046 
end; 
1047 

12500  1048 
val varifyT = #1 o varifyT' []; 
6786  1049 

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

1051 
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

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

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

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

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

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

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

1059 
maxidx = maxidx_of_term prop2, 
2386  1060 
shyps = shyps, 
1061 
hyps = hyps, 

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

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

1063 
prop = prop3} 
1220  1064 
end; 
0  1065 

1066 

1067 
(*** Inference rules for tactics ***) 

1068 

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

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

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

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

1073 
 _ => raise THM("dest_state", i, [state])) 
0  1074 
handle TERM _ => raise THM("dest_state", i, [state]); 
1075 

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

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

1079 
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

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

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

1084 
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

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

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

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

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

1093 
prop = Logic.list_implies (map lift_all As, lift_all B)} 
0  1094 
end; 
1095 

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

1096 
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

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

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

1099 
Thm {sign_ref = sign_ref, 
11518  1100 
der = Pt.infer_derivs' (Pt.map_proof_terms 
1101 
(Logic.incr_indexes ([], i)) (incr_tvar i)) der, 

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

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

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

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

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

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

1107 

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

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

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

1114 
(Thm{sign_ref = sign_ref, 
11518  1115 
der = Pt.infer_derivs' 
1116 
((if Envir.is_empty env then I else (Pt.norm_proof' env)) o 

1117 
Pt.assumption_proof Bs Bi n) der, 

2386  1118 
maxidx = maxidx, 
1119 
shyps = [], 

1120 
hyps = hyps, 

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

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

1122 
map (pairself (Envir.norm_term env)) tpairs, 
2386  1123 
prop = 
1124 
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

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

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

1130 
(Seq.mapp (newth n) 

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

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

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

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

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

1143 
(Thm{sign_ref = sign_ref, 

1144 
der = Pt.infer_derivs' 

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

1146 
maxidx = maxidx, 

1147 
shyps = [], 

1148 
hyps = hyps, 

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

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

1150 
prop = Logic.list_implies (Bs, C)})) 
0  1151 
end; 
1152 

1153 

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

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

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

1158 
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

1159 
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

1160 
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

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

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

1168 
end 

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

1169 
else raise THM("rotate_rule", k, [state]) 
7264  1170 
in (*no fix_shyps*) 
1171 
Thm{sign_ref = sign_ref, 

11563  1172 
der = Pt.infer_derivs' (Pt.rotate_proof Bs Bi m) der, 
2671  1173 
maxidx = maxidx, 
1174 
shyps = shyps, 

1175 
hyps = hyps, 

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

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

1177 
prop = Logic.list_implies (Bs @ [Bi'], C)} 
2671  1178 
end; 
1179 

1180 

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

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

1182 
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

1183 
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

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

1185 
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

1186 
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

1187 
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

1188 
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

1189 
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

1190 
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

1191 
val n_j = length moved_prems 
11563  1192 
val m = if k<0 then n_j + k else k 
1193 
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

1194 
else if 0<m andalso m<n_j 
13629  1195 
then let val (ps,qs) = splitAt(m,moved_prems) 
1196 
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

1197 
else raise THM("permute_prems:k", k, [rl]) 
7264  1198 
in (*no fix_shyps*) 
1199 
Thm{sign_ref = sign_ref, 

11563  1200 
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

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

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

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

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

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

1207 

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

1208 

0  1209 
(** User renaming of parameters in a subgoal **) 
1210 

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

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

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

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

1215 
fun rename_params_rule (cs, i) state = 

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

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

1219 
val short = length iparams  length cs 

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

15570  1222 
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

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

1227 
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

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

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

1230 
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

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

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

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

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

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

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

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

1238 
prop = Logic.list_implies (Bs @ [newBi], C)}) 
0  1239 
end; 
1240 

12982  1241 

0  1242 
(*** Preservation of bound variable names ***) 
1243 

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

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

12982  1248 
{sign_ref = sign_ref, 
1249 
der = der, 

1250 
maxidx = maxidx, 

1251 
hyps = hyps, 

1252 
shyps = shyps, 

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

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

1255 

0  1256 

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

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

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

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

1264 
 strip(A,_) = f A 

0  1265 
in strip end; 
1266 

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

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

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

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

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

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

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

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

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

1277 
(case assoc(al,x) of 

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

250  1285 
fun strip_ren Ai = strip_apply rename (Ai,B) 
0  1286 
in strip_ren end; 
1287 

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

1289 
fun rename_bvars(dpairs, tpairs, B) = 

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

1290 
rename_bvs(foldr Term.match_bvars [] dpairs, dpairs, tpairs, B); 
0  1291 

1292 

1293 
(*** RESOLUTION ***) 

1294 

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

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

1296 

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

250  1299 
fun strip_assums2 (Const("==>", _) $ _ $ B1, 
1300 
Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2) 

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

1305 
 strip_assums2 BB = BB; 

1306 

1307 

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

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

1309 
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

1310 
 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

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

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

1315 
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

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

1318 
 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

1319 

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

1320 

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

1325 
If eres_flg then simultaneously proves A1 by assumption. 

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

4270  1329 
local exception COMPOSE 
0  1330 
in 
250 