author  berghofe 
Mon, 21 Oct 2002 17:04:47 +0200  
changeset 13658  c9ad3e64ddcf 
parent 13642  a3d97348ceb6 
child 14791  23e51b22c710 
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 
29 
val cterm_fun : (term > term) > (cterm > cterm) 

1703
e22ad43bab5f
moved dest_cimplies to drule.ML; added adjust_maxidx
clasohm
parents:
1659
diff
changeset

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

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

35 
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

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

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

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

1160  41 
(*meta theorems*) 
42 
type thm 

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

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

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

3994  51 
val eq_thm : thm * thm > 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 

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

69 
(*meta rules*) 

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

74 
val forall_intr : cterm > thm > thm 

75 
val forall_elim : cterm > thm > thm 

76 
val reflexive : cterm > thm 

77 
val symmetric : thm > thm 

78 
val transitive : thm > thm > thm 

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

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

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

83 
val equal_intr : thm > thm > thm 

84 
val equal_elim : thm > thm > thm 

85 
val implies_intr_hyps : thm > thm 

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

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

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

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

6089  110 
signature THM = 
111 
sig 

112 
include BASIC_THM 

10767
8fa4aafa7314
Thm: dest_comb, dest_abs, capply, cabs no longer global;
wenzelm
parents:
10486
diff
changeset

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

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

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

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

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

122 
val get_name_tags : thm > string * tag list 

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

124 
val name_of_thm : thm > string 

125 
val tags_of_thm : thm > tag list 

126 
val name_thm : string * thm > thm 

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

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

128 
val cterm_match : cterm * cterm > 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

129 
(indexname * ctyp) list * (cterm * cterm) list 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

130 
val cterm_first_order_match : cterm * cterm > 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

131 
(indexname * ctyp) list * (cterm * cterm) list 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

133 
val terms_of_tpairs : (term * term) list > term list 
6089  134 
end; 
135 

3550  136 
structure Thm: THM = 
0  137 
struct 
250  138 

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

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

140 

250  141 
(** certified types **) 
142 

143 
(*certified typs under a signature*) 

144 

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

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

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

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

150 
fun ctyp_of sign T = 

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

151 
Ctyp {sign_ref = Sign.self_ref sign, T = Sign.certify_typ sign T}; 
250  152 

153 
fun read_ctyp sign s = 

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

155 

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

156 

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

157 

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

159 

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

161 

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

162 
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

163 

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

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

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

166 

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

169 
maxidx = maxidx}; 

170 

9461  171 
fun sign_of_cterm (Cterm {sign_ref, ...}) = Sign.deref sign_ref; 
172 

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

174 

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

175 
fun ctyp_of_term (Cterm {sign_ref, T, ...}) = Ctyp {sign_ref = sign_ref, T = T}; 
2671  176 

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

179 
let val (t, T, maxidx) = Sign.certify_term sign tm 

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

180 
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

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

182 

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

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

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

185 

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

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

187 

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

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

189 
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

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

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

192 
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

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

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

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

196 
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

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

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

199 

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

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

201 
fun dest_abs a (Cterm {sign_ref, T as Type("fun",[_,S]), maxidx, t=Abs(x,ty,M)}) = 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

203 
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

204 
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

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

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

207 

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

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

211 
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

212 

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

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

214 
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

215 
(Cterm {t=x, sign_ref=sign_ref2, T, maxidx=maxidx2}) = 
8291  216 
if T = dty then 
217 
Cterm{t=Sign.nodup_vars (f$x), sign_ref=Sign.merge_refs(sign_ref1,sign_ref2), T=rty, 

218 
maxidx=Int.max(maxidx1, maxidx2)} 

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

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

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

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

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

223 
(Cterm {t=t2, sign_ref=sign_ref2, T=T2, maxidx=maxidx2}) = 
8291  224 
Cterm {t=Sign.nodup_vars (absfree(a,ty,t2)), sign_ref=Sign.merge_refs(sign_ref1,sign_ref2), 
2147  225 
T = ty > T2, maxidx=Int.max(maxidx1, maxidx2)} 
1517  226 
 cabs _ _ = raise CTERM "cabs: first arg is not a free variable"; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

227 

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

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

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

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

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

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

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

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

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

236 
val maxidx = Int.max (maxidx1, maxidx2); 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

237 
val vars = map dest_Var (term_vars t1); 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

238 
fun mk_cTinsts (ixn, T) = (ixn, Ctyp {sign_ref = sign_ref, T = T}); 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

239 
fun mk_ctinsts (ixn, t) = 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

240 
let val T = typ_subst_TVars Tinsts (the (assoc (vars, ixn))) 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

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

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

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

245 
in (map mk_cTinsts Tinsts, map mk_ctinsts tinsts) end; 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

246 

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

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

248 
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

249 

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

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

251 
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

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

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

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

255 
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

256 

2509  257 

258 

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

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

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

262 
fun read_def_cterms (sign, types, sorts) used freeze sTs = 
250  263 
let 
8608  264 
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

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

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

269 

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

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

271 
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

272 
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

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

274 

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

275 
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

276 

250  277 

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

280 

2509  281 

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

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

283 

11518  284 
structure Pt = Proofterm; 
285 

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

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

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

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

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

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

293 
prop: term}; (*conclusion*) 
0  294 

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

295 
fun terms_of_tpairs tpairs = flat (map (op @ o pairself single) tpairs); 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

296 

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

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

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

299 

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

300 
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

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

302 
shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}; 
0  303 

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

305 
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

306 
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

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

309 
tpairs = map (pairself (ctermf maxidx)) tpairs, 
1529  310 
prop = ctermf maxidx prop} 
1517  311 
end; 
312 

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

313 
(*errors involving theorems*) 
0  314 
exception THM of string * int * thm list; 
315 

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

318 

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

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

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

322 

3994  323 
fun eq_thm (th1, th2) = 
324 
let 

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

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

327 
val {sign = sg2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...} = 
9031  328 
rep_thm th2; 
3994  329 
in 
9031  330 
Sign.joinable (sg1, sg2) andalso 
3994  331 
eq_set_sort (shyps1, shyps2) andalso 
332 
aconvs (hyps1, hyps2) andalso 

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

333 
aconvs (terms_of_tpairs tpairs1, terms_of_tpairs tpairs2) andalso 
3994  334 
prop1 aconv prop2 
335 
end; 

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

336 

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

337 
fun sign_of_thm (Thm {sign_ref, ...}) = Sign.deref sign_ref; 
12803  338 
fun prop_of (Thm {prop, ...}) = prop; 
13528  339 
fun proof_of (Thm {der = (_, proof), ...}) = proof; 
0  340 

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

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

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

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

344 
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

345 

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

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

349 
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

350 
val sign = Sign.deref sign_ref; 
3895  351 
in 
4254  352 
if Sign.eq_sg (sign, sign') then thm 
353 
else if Sign.subsig (sign, sign') then 

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

354 
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

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

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

358 

6390  359 
val transfer = transfer_sg o Theory.sign_of; 
4254  360 

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

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

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

363 

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

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

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

366 
Logic.strip_imp_prems prop; 
0  367 

368 
(*counts premises in a rule*) 

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

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

370 
Logic.count_prems (prop, 0); 
0  371 

8299  372 
fun major_prem_of thm = 
373 
(case prems_of thm of 

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

7534  377 
fun no_prems thm = nprems_of thm = 0; 
378 

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

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

380 
fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop; 
0  381 

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

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

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

384 
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

385 

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

386 

0  387 

1238  388 
(** sort contexts of theorems **) 
389 

390 
(* basic utils *) 

391 

2163  392 
(*accumulate sorts suppressing duplicates; these are coded low levelly 
1238  393 
to improve efficiency a bit*) 
394 

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

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

396 
 add_typ_sorts (TFree (_, S), Ss) = ins_sort(S,Ss) 
8b365a3a6ed1
Changed some mem, ins and union calls to be monomorphic
paulson
parents:
2163
diff
changeset

397 
 add_typ_sorts (TVar (_, S), Ss) = ins_sort(S,Ss) 
1238  398 
and add_typs_sorts ([], Ss) = Ss 
399 
 add_typs_sorts (T :: Ts, Ss) = add_typs_sorts (Ts, add_typ_sorts (T, Ss)); 

400 

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

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

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

404 
 add_term_sorts (Bound _, Ss) = Ss 

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

405 
 add_term_sorts (Abs (_,T,t), Ss) = add_term_sorts (t, add_typ_sorts (T,Ss)) 
1238  406 
 add_term_sorts (t $ u, Ss) = add_term_sorts (t, add_term_sorts (u, Ss)); 
407 

408 
fun add_terms_sorts ([], Ss) = Ss 

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

409 
 add_terms_sorts (t::ts, Ss) = add_terms_sorts (ts, add_term_sorts (t,Ss)); 
1238  410 

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

411 
fun env_codT (Envir.Envir {iTs, ...}) = map snd (Vartab.dest iTs); 
1258  412 

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

413 
fun add_env_sorts (Envir.Envir {iTs, asol, ...}, Ss) = 
d522ad1809e9
Envir now uses Vartab instead of association lists.
berghofe
parents:
8299
diff
changeset

414 
Vartab.foldl (add_term_sorts o swap o apsnd snd) 
d522ad1809e9
Envir now uses Vartab instead of association lists.
berghofe
parents:
8299
diff
changeset

415 
(Vartab.foldl (add_typ_sorts o swap o apsnd snd) (Ss, iTs), asol); 
1258  416 

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

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

418 
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

419 

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

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

421 
add_terms_sorts (hyps @ terms_of_tpairs tpairs, add_term_sorts (prop, Ss)); 
1238  422 

423 
fun add_thms_shyps ([], Ss) = Ss 

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

7642  425 
add_thms_shyps (ths, union_sort (shyps, Ss)); 
1238  426 

427 

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

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

7642  430 
Term.rems_sort (shyps, add_thm_sorts (th, [])); 
1238  431 

432 

433 
(* fix_shyps *) 

434 

7642  435 
fun all_sorts_nonempty sign_ref = is_some (Sign.univ_witness (Sign.deref sign_ref)); 
436 

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

438 
fun fix_shyps thms Ts (thm as Thm {sign_ref, der, maxidx, hyps, tpairs, prop, ...}) = 
7642  439 
Thm 
440 
{sign_ref = sign_ref, 

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

442 
maxidx = maxidx, 

443 
shyps = 

444 
if all_sorts_nonempty sign_ref then [] 

445 
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

446 
hyps = hyps, tpairs = tpairs, prop = prop} 
1238  447 

448 

7642  449 
(* strip_shyps *) 
1238  450 

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

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

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

1238  456 

7642  457 
val present_sorts = add_thm_sorts (thm, []); 
458 
val extra_shyps = Term.rems_sort (shyps, present_sorts); 

459 
val witnessed_shyps = Sign.witness_sorts sign present_sorts extra_shyps; 

460 
in 

461 
Thm {sign_ref = sign_ref, der = der, maxidx = maxidx, 

462 
shyps = Term.rems_sort (shyps, map #2 witnessed_shyps), 

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

463 
hyps = hyps, tpairs = tpairs, prop = prop} 
7642  464 
end; 
1238  465 

466 

467 

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

469 

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

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

472 
let 
4847  473 
val name = Sign.intern (Theory.sign_of theory) Theory.axiomK raw_name; 
474 

475 
fun get_ax [] = None 

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

479 
Some t => 

480 
Some (fix_shyps [] [] 

481 
(Thm {sign_ref = Sign.self_ref sign, 

11518  482 
der = Pt.infer_derivs' I 
483 
(false, Pt.axm_proof name t), 

4847  484 
maxidx = maxidx_of_term t, 
485 
shyps = [], 

486 
hyps = [], 

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

487 
tpairs = [], 
4847  488 
prop = t})) 
489 
 None => get_ax thys) 

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

491 
in 
4847  492 
(case get_ax (theory :: Theory.ancestors_of theory) of 
493 
Some thm => thm 

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

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

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

496 

6368  497 
fun def_name name = name ^ "_def"; 
498 
fun get_def thy = get_axiom thy o def_name; 

4847  499 

1529  500 

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

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

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

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

505 

6089  506 

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

508 

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

4018  511 

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

512 
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

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

514 
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

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

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

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

519 
val name_of_thm = #1 o get_name_tags; 

520 
val tags_of_thm = #2 o get_name_tags; 

521 

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

0  523 

524 

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

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

527 
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

528 
Thm {sign_ref = sign_ref, 
2386  529 
der = der, (*No derivation recorded!*) 
530 
maxidx = maxidx, 

531 
shyps = shyps, 

532 
hyps = map Term.compress_term hyps, 

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

533 
tpairs = map (pairself Term.compress_term) tpairs, 
2386  534 
prop = Term.compress_term prop}; 
564  535 

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

536 

2509  537 

1529  538 
(*** Meta rules ***) 
0  539 

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

542 
recurrence.*) 

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

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

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

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

546 
val _ = Sign.nodup_vars prop' 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

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

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

549 
maxidx = maxidx_of_term prop', 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

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

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

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

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

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

555 

8291  556 

1220  557 
(** 'primitive' rules **) 
558 

559 
(*discharge all assumptions t from ts*) 

0  560 
val disch = gen_rem (op aconv); 
561 

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

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

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

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

570 
else Thm{sign_ref = sign_ref, 
11518  571 
der = Pt.infer_derivs' I (false, Pt.Hyp prop), 
2386  572 
maxidx = ~1, 
573 
shyps = add_term_sorts(prop,[]), 

574 
hyps = [prop], 

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

575 
tpairs = [], 
2386  576 
prop = prop} 
0  577 
end; 
578 

1220  579 
(*Implication introduction 
3529  580 
[A] 
581 
: 

582 
B 

1220  583 
 
584 
A ==> B 

585 
*) 

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

586 
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

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

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

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

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

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

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

600 
end; 

601 

1529  602 

1220  603 
(*Implication elimination 
604 
A ==> B A 

605 
 

606 
B 

607 
*) 

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

609 
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

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

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

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

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

618 
maxidx = Int.max(maxA,maxidx), 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

619 
shyps = union_sort (shypsA, shyps), 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

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

622 
prop = B} 
250  623 
else err("major premise") 
624 
 _ => err("major premise") 

0  625 
end; 
250  626 

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

629 
 

630 
!!x.A 

631 
*) 

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

632 
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

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

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

635 
(Thm{sign_ref = sign_ref, 
11518  636 
der = Pt.infer_derivs' (Pt.forall_intr_proof x a) der, 
2386  637 
maxidx = maxidx, 
638 
shyps = [], 

639 
hyps = hyps, 

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

640 
tpairs = tpairs, 
2386  641 
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

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

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

644 
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

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

647 
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

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

651 

1220  652 
(*Forall elimination 
653 
!!x.A 

654 
 

655 
A[t/x] 

656 
*) 

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

657 
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

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

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

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

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

664 
(Thm{sign_ref= Sign.merge_refs(sign_ref,sign_reft), 
11612  665 
der = Pt.infer_derivs' (Pt.% o rpair (Some t)) der, 
2386  666 
maxidx = Int.max(maxidx, maxt), 
667 
shyps = [], 

668 
hyps = hyps, 

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

669 
tpairs = tpairs, 
2386  670 
prop = betapply(A,t)}) 
671 
in if maxt >= 0 andalso maxidx >= 0 

8291  672 
then nodup_vars thm "forall_elim" 
2386  673 
else thm (*no new Vars: no expensive check!*) 
674 
end 

2147  675 
 _ => raise THM("forall_elim: not quantified", 0, [th]) 
0  676 
end 
677 
handle TERM _ => 

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

680 

1220  681 
(* Equality *) 
0  682 

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

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

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

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

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

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

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

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

692 
prop = Logic.mk_equals(t,t)} 
0  693 
end; 
694 

695 
(*The symmetry rule 

1220  696 
t==u 
697 
 

698 
u==t 

699 
*) 

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

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

704 
Thm{sign_ref = sign_ref, 
11518  705 
der = Pt.infer_derivs' Pt.symmetric der, 
2386  706 
maxidx = maxidx, 
707 
shyps = shyps, 

708 
hyps = hyps, 

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

709 
tpairs = tpairs, 
2386  710 
prop = eq$u$t} 
0  711 
 _ => raise THM("symmetric", 0, [th]); 
712 

713 
(*The transitive rule 

1220  714 
t1==u u==t2 
715 
 

716 
t1==t2 

717 
*) 

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

719 
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

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

11518  723 
((eq as Const("==", Type (_, [T, _]))) $ t1 $ u, Const("==",_) $ u' $ t2) => 
1634  724 
if not (u aconv u') then err"middle term" 
725 
else let val thm = 

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

726 
Thm{sign_ref= merge_thm_sgs(th1,th2), 
11518  727 
der = Pt.infer_derivs (Pt.transitive u T) der1 der2, 
2147  728 
maxidx = Int.max(max1,max2), 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

729 
shyps = union_sort (shyps1, shyps2), 
2386  730 
hyps = union_term(hyps1,hyps2), 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

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

732 
prop = eq$t1$t2} 
2139
2c59b204b540
Only calls nodup_Vars if really necessary. We get a speedup of nearly 6%
paulson
parents:
2047
diff
changeset

733 
in if max1 >= 0 andalso max2 >= 0 
8291  734 
then nodup_vars thm "transitive" 
2147  735 
else thm (*no new Vars: no expensive check!*) 
2139
2c59b204b540
Only calls nodup_Vars if really necessary. We get a speedup of nearly 6%
paulson
parents:
2047
diff
changeset

736 
end 
0  737 
 _ => err"premises" 
738 
end; 

739 

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

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

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

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

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

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

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

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

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

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

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

751 
tpairs = [], 
10486  752 
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

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

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

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

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

757 

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

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

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

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

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

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

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

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

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

767 
prop = Logic.mk_equals (t, Pattern.eta_contract t)} 
0  768 
end; 
769 

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

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

1220  772 
t == u 
773 
 

774 
%x.t == %x.u 

775 
*) 

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

776 
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

777 
let val x = term_of cx; 
250  778 
val (t,u) = Logic.dest_equals prop 
779 
handle TERM _ => 

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

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

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

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

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

787 
tpairs = tpairs, 
2386  788 
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

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

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

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

792 
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

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

795 
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

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

799 

800 
(*The combination rule 

3529  801 
f == g t == u 
802 
 

803 
f(t) == g(u) 

1220  804 
*) 
0  805 
fun combination th1 th2 = 
1529  806 
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

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

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

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

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

813 
if T1 <> tT then 
2386  814 
raise THM("combination: types", 0, [th1,th2]) 
815 
else () 

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

817 
[th1,th2])) 

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

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

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

820 
Const ("==", Type ("fun", [tT, _])) $ t $ u) => 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

821 
let val _ = chktypes fT tT 
2386  822 
val thm = (*no fix_shyps*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

823 
Thm{sign_ref = merge_thm_sgs(th1,th2), 
11518  824 
der = Pt.infer_derivs 
825 
(Pt.combination f g t u fT) der1 der2, 

2386  826 
maxidx = Int.max(max1,max2), 
827 
shyps = union_sort(shyps1,shyps2), 

828 
hyps = union_term(hyps1,hyps2), 

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

829 
tpairs = tpairs1 @ tpairs2, 
2386  830 
prop = Logic.mk_equals(f$t, g$u)} 
2139
2c59b204b540
Only calls nodup_Vars if really necessary. We get a speedup of nearly 6%
paulson
parents:
2047
diff
changeset

831 
in if max1 >= 0 andalso max2 >= 0 
8291  832 
then nodup_vars thm "combination" 
2386  833 
else thm (*no new Vars: no expensive check!*) 
2139
2c59b204b540
Only calls nodup_Vars if really necessary. We get a speedup of nearly 6%
paulson
parents:
2047
diff
changeset

834 
end 
0  835 
 _ => raise THM("combination: premises", 0, [th1,th2]) 
836 
end; 

837 

838 

839 
(* Equality introduction 

3529  840 
A ==> B B ==> A 
841 
 

842 
A == B 

1220  843 
*) 
0  844 
fun equal_intr th1 th2 = 
11518  845 
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

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

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

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

2386  852 
if A aconv A' andalso B aconv B' 
853 
then 

854 
(*no fix_shyps*) 

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

855 
Thm{sign_ref = merge_thm_sgs(th1,th2), 
11518  856 
der = Pt.infer_derivs (Pt.equal_intr A B) der1 der2, 
2386  857 
maxidx = Int.max(max1,max2), 
858 
shyps = union_sort(shyps1,shyps2), 

859 
hyps = union_term(hyps1,hyps2), 

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

860 
tpairs = tpairs1 @ tpairs2, 
2386  861 
prop = Logic.mk_equals(A,B)} 
862 
else err"not equal" 

1529  863 
 _ => err"premises" 
864 
end; 

865 

866 

867 
(*The equal propositions rule 

3529  868 
A == B A 
1529  869 
 
870 
B 

871 
*) 

872 
fun equal_elim th1 th2 = 

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

873 
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

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

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

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

879 
fix_shyps [th1, th2] [] 

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

880 
(Thm{sign_ref= merge_thm_sgs(th1,th2), 
11518  881 
der = Pt.infer_derivs (Pt.equal_elim A B) der1 der2, 
2386  882 
maxidx = Int.max(max1,max2), 
883 
shyps = [], 

884 
hyps = union_term(hyps1,hyps2), 

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

885 
tpairs = tpairs1 @ tpairs2, 
2386  886 
prop = B}) 
1529  887 
 _ => err"major premise" 
888 
end; 

0  889 

1220  890 

891 

0  892 
(**** Derived rules ****) 
893 

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

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

898 
(Thm{sign_ref = sign_ref, 
11518  899 
der = Pt.infer_derivs' (Pt.implies_intr_proof A) der, 
2386  900 
maxidx = maxidx, 
901 
shyps = shyps, 

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

903 
tpairs = tpairs, 
2386  904 
prop = implies$A$prop}) 
0  905 
 implies_intr_hyps th = th; 
906 

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

250  908 
Instantiates the theorem and deletes trivial tpairs. 
0  909 
Resulting sequence may contain multiple elements if the tpairs are 
910 
not all flexflex. *) 

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

911 
fun flexflex_rule (th as Thm{sign_ref, der, maxidx, hyps, tpairs, prop, ...}) = 
250  912 
let fun newthm env = 
1529  913 
if Envir.is_empty env then th 
914 
else 

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

915 
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

916 
val newprop = Envir.norm_term env prop; 
250  917 
(*Remove trivial tpairs, of the form t=t*) 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

918 
val distpairs = filter (not o op aconv) ntpairs 
1220  919 
in fix_shyps [th] (env_codT env) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

920 
(Thm{sign_ref = sign_ref, 
11518  921 
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

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

923 
terms_of_tpairs distpairs), 
2386  924 
shyps = [], 
925 
hyps = hyps, 

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

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

930 
(Unify.smash_unifiers(Sign.deref sign_ref, Envir.empty maxidx, tpairs)) 
0  931 
end; 
932 

933 
(*Instantiation of Vars 

1220  934 
A 
935 
 

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

937 
*) 

0  938 

6928  939 
local 
940 

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

943 

6928  944 
fun prt_typing sg_ref t T = 
945 
let val sg = Sign.deref sg_ref in 

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

947 
end; 

948 

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

950 
fun add_ctpair ((ct,cu), (sign_ref,tpairs)) = 
6928  951 
let 
952 
val Cterm {sign_ref=sign_reft, t=t, T= T, ...} = ct 

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

954 
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

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

958 
Pretty.fbrk, prt_typing sign_ref_merged t T, 

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

0  960 
end; 
961 

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

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

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

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

6928  966 
in 
967 

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

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

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

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

973 
let val (newsign_ref,tpairs) = foldr add_ctpair (ctpairs, (sign_ref,[])); 
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

974 
val (newsign_ref,vTs) = foldr add_ctyp (vcTs, (newsign_ref,[])); 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

975 
val tsig = Sign.tsig_of (Sign.deref newsign_ref); 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

976 
fun subst t = subst_atomic tpairs (Type.inst_term_tvars (tsig, vTs) t); 
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

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

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

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

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

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

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

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

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

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

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

8291  992 
else nodup_vars newth "instantiate" 
0  993 
end 
6928  994 
handle TERM _ => raise THM("instantiate: incompatible signatures", 0, [th]) 
995 
 TYPE (msg, _, _) => raise THM (msg, 0, [th]); 

996 

997 
end; 

998 

0  999 

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

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

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

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

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

1007 
(Thm{sign_ref = sign_ref, 
11518  1008 
der = Pt.infer_derivs' I (false, Pt.AbsP ("H", None, Pt.PBound 0)), 
2386  1009 
maxidx = maxidx, 
1010 
shyps = [], 

1011 
hyps = [], 

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

1012 
tpairs = [], 
2386  1013 
prop = implies$A$A}) 
0  1014 
end; 
1015 

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

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

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

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

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

1023 
(Thm {sign_ref = sign_ref, 
11518  1024 
der = Pt.infer_derivs' I 
1025 
(false, Pt.PAxm ("ProtoPure.class_triv:" ^ c, t, Some [])), 

2386  1026 
maxidx = maxidx, 
1027 
shyps = [], 

1028 
hyps = [], 

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

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

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

1032 

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

1033 

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

1035 
fun varifyT' fixed (Thm{sign_ref,der,maxidx,shyps,hyps,tpairs,prop}) = 
12500  1036 
let 
1037 
val tfrees = foldr add_term_tfree_names (hyps, fixed); 

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

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

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

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

1042 
Thm{sign_ref = sign_ref, 
11518  1043 
der = Pt.infer_derivs' (Pt.varify_proof prop tfrees) der, 
2386  1044 
maxidx = Int.max(0,maxidx), 
1045 
shyps = shyps, 

1046 
hyps = hyps, 

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

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

1048 
prop = prop3} 
12500  1049 
in (nodup_vars thm "varifyT", al) end 
8291  1050 
(* this nodup_vars check can be removed if thms are guaranteed not to contain 
1051 
duplicate TVars with different sorts *) 

0  1052 
end; 
1053 

12500  1054 
val varifyT = #1 o varifyT' []; 
6786  1055 

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

1057 
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

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

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

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

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

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

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

1065 
maxidx = maxidx_of_term prop2, 
2386  1066 
shyps = shyps, 
1067 
hyps = hyps, 

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

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

1069 
prop = prop3} 
1220  1070 
end; 
0  1071 

1072 

1073 
(*** Inference rules for tactics ***) 

1074 

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

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

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

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

1079 
 _ => raise THM("dest_state", i, [state])) 
0  1080 
handle TERM _ => raise THM("dest_state", i, [state]); 
1081 

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

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

1085 
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

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

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

1090 
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

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

1093 
Thm{sign_ref = merge_thm_sgs(state,orule), 
11518  1094 
der = Pt.infer_derivs' (Pt.lift_proof Bi (smax+1) prop) der, 
2386  1095 
maxidx = maxidx+smax+1, 
2177
8b365a3a6ed1
Changed some mem, ins and union calls to be monomorphic
paulson
parents:
2163
diff
changeset

1096 
shyps=union_sort(sshyps,shyps), 
2386  1097 
hyps=hyps, 
13658
c9ad3e64ddcf
Changed handling of flexflex constraints: now stored in separate
berghofe
parents:
13642
diff
changeset

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

1099 
prop = Logic.list_implies (map lift_all As, lift_all B)} 
0  1100 
end; 
1101 

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

1102 
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

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

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

1105 
Thm {sign_ref = sign_ref, 
11518  1106 
der = Pt.infer_derivs' (Pt.map_proof_terms 
1107 
(Logic.incr_indexes ([], i)) (incr_tvar i)) der, 

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

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

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

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

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

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

1113 

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

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

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

1120 
(Thm{sign_ref = sign_ref, 
11518  1121 
der = Pt.infer_derivs' 
1122 
((if Envir.is_empty env then I else (Pt.norm_proof' env)) o 

1123 
Pt.assumption_proof Bs Bi n) der, 

2386  1124 
maxidx = maxidx, 
1125 
shyps = [], 

1126 
hyps = hyps, 

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

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

1128 
map (pairself (Envir.norm_term env)) tpairs, 
2386  1129 
prop = 
1130 
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

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

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

1136 
(Seq.mapp (newth n) 

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

1137 
(Unify.unifiers(Sign.deref sign_ref,Envir.empty maxidx, (t,u)::tpairs)) 
11518  1138 
(addprfs apairs (n+1)))) 
1139 
in addprfs (Logic.assum_pairs Bi) 1 end; 

0  1140 

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

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

1144 
let val Thm{sign_ref,der,maxidx,hyps,prop,...} = state; 
0  1145 
val (tpairs, Bs, Bi, C) = dest_state(state,i) 
11518  1146 
in (case find_index (op aconv) (Logic.assum_pairs Bi) of 
1147 
(~1) => raise THM("eq_assumption", 0, [state]) 

1148 
 n => fix_shyps [state] [] 

1149 
(Thm{sign_ref = sign_ref, 

1150 
der = Pt.infer_derivs' 

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

1152 
maxidx = maxidx, 

1153 
shyps = [], 

1154 
hyps = hyps, 

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

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

1156 
prop = Logic.list_implies (Bs, C)})) 
0  1157 
end; 
1158 

1159 

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

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

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

1164 
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

1165 
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

1166 
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

1167 
and concl = Logic.strip_imp_concl rest 
2671  1168 
val n = length asms 
11563  1169 
val m = if k<0 then n+k else k 
1170 
val Bi' = if 0=m orelse m=n then Bi 

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

1174 
end 

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

1175 
else raise THM("rotate_rule", k, [state]) 
7264  1176 
in (*no fix_shyps*) 
1177 
Thm{sign_ref = sign_ref, 

11563  1178 
der = Pt.infer_derivs' (Pt.rotate_proof Bs Bi m) der, 
2671  1179 
maxidx = maxidx, 
1180 
shyps = shyps, 

1181 
hyps = hyps, 

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

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

1183 
prop = Logic.list_implies (Bs @ [Bi'], C)} 
2671  1184 
end; 
1185 

1186 

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

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

1188 
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

1189 
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

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

1191 
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

1192 
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

1193 
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

1194 
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

1195 
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

1196 
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

1197 
val n_j = length moved_prems 
11563  1198 
val m = if k<0 then n_j + k else k 
1199 
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

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

1203 
else raise THM("permute_prems:k", k, [rl]) 
7264  1204 
in (*no fix_shyps*) 
1205 
Thm{sign_ref = sign_ref, 

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

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

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

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

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

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

1213 

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

1214 

0  1215 
(** User renaming of parameters in a subgoal **) 
1216 

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

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

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

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

1221 
fun rename_params_rule (cs, i) state = 

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

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

1225 
val short = length iparams  length cs 

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

1228 
else variantlist(take (short,iparams), cs) @ cs 

3037
99ed078e6ae7
rename_params_rule used to check if the new name clashed with a free name in
nipkow
parents:
3012
diff
changeset

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

1233 
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

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

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

1236 
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

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

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

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

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

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

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

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

1244 
prop = Logic.list_implies (Bs @ [newBi], C)}) 
0  1245 
end; 
1246 

12982  1247 

0  1248 
(*** Preservation of bound variable names ***) 
1249 

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

1250 
fun rename_boundvars pat obj (thm as Thm {sign_ref, der, maxidx, hyps, shyps, tpairs, prop}) = 
12982  1251 
(case Term.rename_abs pat obj prop of 
1252 
None => thm 

1253 
 Some prop' => Thm 

1254 
{sign_ref = sign_ref, 

1255 
der = der, 

1256 
maxidx = maxidx, 

1257 
hyps = hyps, 

1258 
shyps = shyps, 

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

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

1261 

0  1262 

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

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

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

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

1270 
 strip(A,_) = f A 

0  1271 
in strip end; 
1272 

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

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

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

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

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

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

1280 
(*unknowns appearing elsewhere be preserved!*) 

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

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

1283 
(case assoc(al,x) of 

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

1284 
Some(y) => if x mem_string vids orelse y mem_string vids then t 
250  1285 
else Var((y,i),T) 
1286 
 None=> t) 

0  1287 
 rename(Abs(x,T,t)) = 
9721  1288 
Abs(if_none(assoc_string(al,x)) x, T, rename t) 
0  1289 
 rename(f$t) = rename f $ rename t 
1290 
 rename(t) = t; 

250  1291 
fun strip_ren Ai = strip_apply rename (Ai,B) 
0  1292 
in strip_ren end; 
1293 

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

1295 
fun rename_bvars(dpairs, tpairs, B) = 

12982  1296 
rename_bvs(foldr Term.match_bvars (dpairs,[]), dpairs, tpairs, B); 
0  1297 

1298 

1299 
(*** RESOLUTION ***) 

1300 

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

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

1302 

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

250  1305 
fun strip_assums2 (Const("==>", _) $ _ $ B1, 
1306 
Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2) 

0  1307 
 strip_assums2 (Const("all",_)$Abs(a,T,t1), 
250  1308 
Const("all",_)$Abs(_,_,t2)) = 
0  1309 
let val (B1,B2) = strip_assums2 (t1,t2) 
1310 
in (Abs(a,T,B1), Abs(a,T,B2)) end 

1311 
 strip_assums2 BB = BB; 

1312 

1313 

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

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

1315 
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

1316 
 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

1317 
let val Envir.Envir{iTs, ...} = env 
8407
d522ad1809e9
Envir now uses Vartab instead of association lists.
berghofe
parents:
8299
diff
changeset

1318 
val T' = typ_subst_TVars_Vartab iTs T 
1238  1319 
(*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

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

1321 
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

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

1324 
 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

1325 

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

1326 

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

1331 
If eres_flg 