author  nipkow 
Thu, 10 Oct 2002 19:02:23 +0200  
changeset 13642  a3d97348ceb6 
parent 13629  a46362d2b19b 
child 13658  c9ad3e64ddcf 
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, 
45 
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, 
48 
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 
6089  133 
end; 
134 

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

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

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

139 

250  140 
(** certified types **) 
141 

142 
(*certified typs under a signature*) 

143 

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

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

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

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

149 
fun ctyp_of sign T = 

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

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

152 
fun read_ctyp sign s = 

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

153 
Ctyp {sign_ref = Sign.self_ref sign, T = Sign.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

154 

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 

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

158 

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

160 

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

161 
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

162 

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

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

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

165 

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

168 
maxidx = maxidx}; 

169 

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

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

173 

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

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

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

178 
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

179 
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

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

181 

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

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

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

184 

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

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

186 

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

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

188 
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

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

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

191 
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

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

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

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

195 
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

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

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

198 

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

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

200 
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

201 
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

202 
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

203 
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

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

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

206 

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

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

210 
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

211 

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

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

213 
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

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

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

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

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

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

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

221 
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

222 
(Cterm {t=t2, sign_ref=sign_ref2, T=T2, maxidx=maxidx2}) = 
8291  223 
Cterm {t=Sign.nodup_vars (absfree(a,ty,t2)), sign_ref=Sign.merge_refs(sign_ref1,sign_ref2), 
2147  224 
T = ty > T2, maxidx=Int.max(maxidx1, maxidx2)} 
1517  225 
 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

226 

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

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

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

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

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

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

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

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

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

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

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

237 
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

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

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

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

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

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

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

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

245 

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

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

247 
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

248 

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

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

250 
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

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

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

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

254 
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

255 

2509  256 

257 

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

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

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

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

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

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

268 

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

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

270 
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

271 
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

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

273 

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

274 
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

275 

250  276 

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

279 

2509  280 

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

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

282 

11518  283 
structure Pt = Proofterm; 
284 

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

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

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

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

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

291 
prop: term}; (*conclusion*) 
0  292 

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

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

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

295 
shyps = shyps, hyps = hyps, prop = prop}; 
0  296 

1529  297 
(*Version of rep_thm returning cterms instead of terms*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

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

299 
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

300 
in {sign = Sign.deref sign_ref, der = der, maxidx = maxidx, shyps = shyps, 
1529  301 
hyps = map (ctermf ~1) hyps, 
302 
prop = ctermf maxidx prop} 

1517  303 
end; 
304 

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

305 
(*errors involving theorems*) 
0  306 
exception THM of string * int * thm list; 
307 

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

310 

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

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

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

314 

3994  315 
fun eq_thm (th1, th2) = 
316 
let 

11518  317 
val {sign = sg1, shyps = shyps1, hyps = hyps1, prop = prop1, ...} = 
9031  318 
rep_thm th1; 
11518  319 
val {sign = sg2, shyps = shyps2, hyps = hyps2, prop = prop2, ...} = 
9031  320 
rep_thm th2; 
3994  321 
in 
9031  322 
Sign.joinable (sg1, sg2) andalso 
3994  323 
eq_set_sort (shyps1, shyps2) andalso 
324 
aconvs (hyps1, hyps2) andalso 

325 
prop1 aconv prop2 

326 
end; 

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

327 

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

328 
fun sign_of_thm (Thm {sign_ref, ...}) = Sign.deref sign_ref; 
12803  329 
fun prop_of (Thm {prop, ...}) = prop; 
13528  330 
fun proof_of (Thm {der = (_, proof), ...}) = proof; 
0  331 

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

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

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

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

335 
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

336 

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

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

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

341 
val sign = Sign.deref sign_ref; 
3895  342 
in 
4254  343 
if Sign.eq_sg (sign, sign') then thm 
344 
else if Sign.subsig (sign, sign') then 

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

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

348 
end; 

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

349 

6390  350 
val transfer = transfer_sg o Theory.sign_of; 
4254  351 

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

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

353 
fun tpairs_of (Thm {prop, ...}) = #1 (Logic.strip_flexpairs prop); 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

354 

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

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

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

357 
Logic.strip_imp_prems (Logic.skip_flexpairs prop); 
0  358 

359 
(*counts premises in a rule*) 

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

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

361 
Logic.count_prems (Logic.skip_flexpairs prop, 0); 
0  362 

8299  363 
fun major_prem_of thm = 
364 
(case prems_of thm of 

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

7534  368 
fun no_prems thm = nprems_of thm = 0; 
369 

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

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

371 
fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop; 
0  372 

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

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

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

375 
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

376 

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

377 

0  378 

1238  379 
(** sort contexts of theorems **) 
380 

381 
(* basic utils *) 

382 

2163  383 
(*accumulate sorts suppressing duplicates; these are coded low levelly 
1238  384 
to improve efficiency a bit*) 
385 

386 
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

387 
 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

388 
 add_typ_sorts (TVar (_, S), Ss) = ins_sort(S,Ss) 
1238  389 
and add_typs_sorts ([], Ss) = Ss 
390 
 add_typs_sorts (T :: Ts, Ss) = add_typs_sorts (Ts, add_typ_sorts (T, Ss)); 

391 

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

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

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

395 
 add_term_sorts (Bound _, Ss) = Ss 

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

396 
 add_term_sorts (Abs (_,T,t), Ss) = add_term_sorts (t, add_typ_sorts (T,Ss)) 
1238  397 
 add_term_sorts (t $ u, Ss) = add_term_sorts (t, add_term_sorts (u, Ss)); 
398 

399 
fun add_terms_sorts ([], Ss) = Ss 

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

400 
 add_terms_sorts (t::ts, Ss) = add_terms_sorts (ts, add_term_sorts (t,Ss)); 
1238  401 

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

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

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

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

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

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

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

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

409 
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

410 

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

413 

414 
fun add_thms_shyps ([], Ss) = Ss 

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

7642  416 
add_thms_shyps (ths, union_sort (shyps, Ss)); 
1238  417 

418 

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

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

7642  421 
Term.rems_sort (shyps, add_thm_sorts (th, [])); 
1238  422 

423 

424 
(* fix_shyps *) 

425 

7642  426 
fun all_sorts_nonempty sign_ref = is_some (Sign.univ_witness (Sign.deref sign_ref)); 
427 

1238  428 
(*preserve sort contexts of rule premises and substituted types*) 
7642  429 
fun fix_shyps thms Ts (thm as Thm {sign_ref, der, maxidx, hyps, prop, ...}) = 
430 
Thm 

431 
{sign_ref = sign_ref, 

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

433 
maxidx = maxidx, 

434 
shyps = 

435 
if all_sorts_nonempty sign_ref then [] 

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

437 
hyps = hyps, prop = prop} 

1238  438 

439 

7642  440 
(* strip_shyps *) 
1238  441 

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

444 
 strip_shyps (thm as Thm {sign_ref, der, maxidx, shyps, hyps, prop}) = 

445 
let 

446 
val sign = Sign.deref sign_ref; 

1238  447 

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

450 
val witnessed_shyps = Sign.witness_sorts sign present_sorts extra_shyps; 

451 
in 

452 
Thm {sign_ref = sign_ref, der = der, maxidx = maxidx, 

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

454 
hyps = hyps, prop = prop} 

455 
end; 

1238  456 

457 

458 

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

460 

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

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

463 
let 
4847  464 
val name = Sign.intern (Theory.sign_of theory) Theory.axiomK raw_name; 
465 

466 
fun get_ax [] = None 

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

470 
Some t => 

471 
Some (fix_shyps [] [] 

472 
(Thm {sign_ref = Sign.self_ref sign, 

11518  473 
der = Pt.infer_derivs' I 
474 
(false, Pt.axm_proof name t), 

4847  475 
maxidx = maxidx_of_term t, 
476 
shyps = [], 

477 
hyps = [], 

478 
prop = t})) 

479 
 None => get_ax thys) 

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

481 
in 
4847  482 
(case get_ax (theory :: Theory.ancestors_of theory) of 
483 
Some thm => thm 

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

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

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

486 

6368  487 
fun def_name name = name ^ "_def"; 
488 
fun get_def thy = get_axiom thy o def_name; 

4847  489 

1529  490 

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

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

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

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

495 

6089  496 

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

498 

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

4018  501 

11518  502 
fun put_name_tags x (Thm {sign_ref, der = (ora, prf), maxidx, shyps, hyps, prop}) = 
503 
Thm {sign_ref = sign_ref, 

504 
der = (ora, Pt.thm_proof (Sign.deref sign_ref) x hyps prop prf), 

505 
maxidx = maxidx, shyps = shyps, hyps = hyps, prop = prop}; 

6089  506 

507 
val name_of_thm = #1 o get_name_tags; 

508 
val tags_of_thm = #2 o get_name_tags; 

509 

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

0  511 

512 

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

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

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

516 
Thm {sign_ref = sign_ref, 
2386  517 
der = der, (*No derivation recorded!*) 
518 
maxidx = maxidx, 

519 
shyps = shyps, 

520 
hyps = map Term.compress_term hyps, 

521 
prop = Term.compress_term prop}; 

564  522 

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

523 

2509  524 

1529  525 
(*** Meta rules ***) 
0  526 

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

529 
recurrence.*) 

8291  530 
fun nodup_vars (thm as Thm{sign_ref, der, maxidx, shyps, hyps, prop}) s = 
8296  531 
Thm {sign_ref = sign_ref, 
2386  532 
der = der, 
533 
maxidx = maxidx_of_term prop, 

534 
shyps = shyps, 

535 
hyps = hyps, 

8296  536 
prop = Sign.nodup_vars prop} 
2147  537 
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

538 

8291  539 

1220  540 
(** 'primitive' rules **) 
541 

542 
(*discharge all assumptions t from ts*) 

0  543 
val disch = gen_rem (op aconv); 
544 

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

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

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

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

553 
else Thm{sign_ref = sign_ref, 
11518  554 
der = Pt.infer_derivs' I (false, Pt.Hyp prop), 
2386  555 
maxidx = ~1, 
556 
shyps = add_term_sorts(prop,[]), 

557 
hyps = [prop], 

558 
prop = prop} 

0  559 
end; 
560 

1220  561 
(*Implication introduction 
3529  562 
[A] 
563 
: 

564 
B 

1220  565 
 
566 
A ==> B 

567 
*) 

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

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

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

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

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

576 
shyps = add_term_sorts (A, shyps), 
2386  577 
hyps = disch(hyps,A), 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

581 
end; 

582 

1529  583 

1220  584 
(*Implication elimination 
585 
A ==> B A 

586 
 

587 
B 

588 
*) 

0  589 
fun implies_elim thAB thA : thm = 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

590 
let val Thm{maxidx=maxA, der=derA, hyps=hypsA, shyps=shypsA, prop=propA, ...} = thA 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

591 
and Thm{der, maxidx, hyps, shyps, prop, ...} = thAB; 
250  592 
fun err(a) = raise THM("implies_elim: "^a, 0, [thAB,thA]) 
0  593 
in case prop of 
250  594 
imp$A$B => 
595 
if imp=implies andalso A aconv propA 

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

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

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

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

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

601 
hyps = union_term(hypsA,hyps), (*dups suppressed*) 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

602 
prop = B} 
250  603 
else err("major premise") 
604 
 _ => err("major premise") 

0  605 
end; 
250  606 

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

609 
 

610 
!!x.A 

611 
*) 

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

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

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

615 
(Thm{sign_ref = sign_ref, 
11518  616 
der = Pt.infer_derivs' (Pt.forall_intr_proof x a) der, 
2386  617 
maxidx = maxidx, 
618 
shyps = [], 

619 
hyps = hyps, 

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

0  621 
in case x of 
250  622 
Free(a,T) => 
623 
if exists (apl(x, Logic.occs)) hyps 

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

625 
else result(a,T) 

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

628 
end; 

629 

1220  630 
(*Forall elimination 
631 
!!x.A 

632 
 

633 
A[t/x] 

634 
*) 

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

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

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

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

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

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

642 
(Thm{sign_ref= Sign.merge_refs(sign_ref,sign_reft), 
11612  643 
der = Pt.infer_derivs' (Pt.% o rpair (Some t)) der, 
2386  644 
maxidx = Int.max(maxidx, maxt), 
645 
shyps = [], 

646 
hyps = hyps, 

647 
prop = betapply(A,t)}) 

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

8291  649 
then nodup_vars thm "forall_elim" 
2386  650 
else thm (*no new Vars: no expensive check!*) 
651 
end 

2147  652 
 _ => raise THM("forall_elim: not quantified", 0, [th]) 
0  653 
end 
654 
handle TERM _ => 

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

657 

1220  658 
(* Equality *) 
0  659 

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

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

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

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

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

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

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

668 
prop = Logic.mk_equals(t,t)} 
0  669 
end; 
670 

671 
(*The symmetry rule 

1220  672 
t==u 
673 
 

674 
u==t 

675 
*) 

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

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

680 
Thm{sign_ref = sign_ref, 
11518  681 
der = Pt.infer_derivs' Pt.symmetric der, 
2386  682 
maxidx = maxidx, 
683 
shyps = shyps, 

684 
hyps = hyps, 

685 
prop = eq$u$t} 

0  686 
 _ => raise THM("symmetric", 0, [th]); 
687 

688 
(*The transitive rule 

1220  689 
t1==u u==t2 
690 
 

691 
t1==t2 

692 
*) 

0  693 
fun transitive th1 th2 = 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

694 
let val Thm{der=der1, maxidx=max1, hyps=hyps1, shyps=shyps1, prop=prop1,...} = th1 
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

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

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

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

704 
shyps = union_sort (shyps1, shyps2), 
2386  705 
hyps = union_term(hyps1,hyps2), 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

706 
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

707 
in if max1 >= 0 andalso max2 >= 0 
8291  708 
then nodup_vars thm "transitive" 
2147  709 
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

710 
end 
0  711 
 _ => err"premises" 
712 
end; 

713 

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

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

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

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

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

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

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

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

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

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

724 
hyps = [], 
10486  725 
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

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

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

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

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

730 

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

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

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

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

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

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

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

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

739 
prop = Logic.mk_equals (t, Pattern.eta_contract t)} 
0  740 
end; 
741 

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

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

1220  744 
t == u 
745 
 

746 
%x.t == %x.u 

747 
*) 

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

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

749 
let val x = term_of cx; 
250  750 
val (t,u) = Logic.dest_equals prop 
751 
handle TERM _ => 

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

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

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

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

757 
shyps = add_typ_sorts (T, shyps), 
2386  758 
hyps = hyps, 
759 
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

760 
Abs(a, T, abstract_over (x,u)))} 
0  761 
in case x of 
250  762 
Free(_,T) => 
763 
if exists (apl(x, Logic.occs)) hyps 

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

765 
else result T 

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

768 
end; 

769 

770 
(*The combination rule 

3529  771 
f == g t == u 
772 
 

773 
f(t) == g(u) 

1220  774 
*) 
0  775 
fun combination th1 th2 = 
1529  776 
let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1, 
2386  777 
prop=prop1,...} = th1 
1529  778 
and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, 
2386  779 
prop=prop2,...} = th2 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

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

783 
if T1 <> tT then 
2386  784 
raise THM("combination: types", 0, [th1,th2]) 
785 
else () 

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

787 
[th1,th2])) 

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

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

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

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

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

793 
Thm{sign_ref = merge_thm_sgs(th1,th2), 
11518  794 
der = Pt.infer_derivs 
795 
(Pt.combination f g t u fT) der1 der2, 

2386  796 
maxidx = Int.max(max1,max2), 
797 
shyps = union_sort(shyps1,shyps2), 

798 
hyps = union_term(hyps1,hyps2), 

799 
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

800 
in if max1 >= 0 andalso max2 >= 0 
8291  801 
then nodup_vars thm "combination" 
2386  802 
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

803 
end 
0  804 
 _ => raise THM("combination: premises", 0, [th1,th2]) 
805 
end; 

806 

807 

808 
(* Equality introduction 

3529  809 
A ==> B B ==> A 
810 
 

811 
A == B 

1220  812 
*) 
0  813 
fun equal_intr th1 th2 = 
11518  814 
let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1, 
2386  815 
prop=prop1,...} = th1 
1529  816 
and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, 
2386  817 
prop=prop2,...} = th2; 
1529  818 
fun err(msg) = raise THM("equal_intr: "^msg, 0, [th1,th2]) 
819 
in case (prop1,prop2) of 

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

2386  821 
if A aconv A' andalso B aconv B' 
822 
then 

823 
(*no fix_shyps*) 

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

824 
Thm{sign_ref = merge_thm_sgs(th1,th2), 
11518  825 
der = Pt.infer_derivs (Pt.equal_intr A B) der1 der2, 
2386  826 
maxidx = Int.max(max1,max2), 
827 
shyps = union_sort(shyps1,shyps2), 

828 
hyps = union_term(hyps1,hyps2), 

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

830 
else err"not equal" 

1529  831 
 _ => err"premises" 
832 
end; 

833 

834 

835 
(*The equal propositions rule 

3529  836 
A == B A 
1529  837 
 
838 
B 

839 
*) 

840 
fun equal_elim th1 th2 = 

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

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

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

844 
in case prop1 of 

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

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

847 
fix_shyps [th1, th2] [] 

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

848 
(Thm{sign_ref= merge_thm_sgs(th1,th2), 
11518  849 
der = Pt.infer_derivs (Pt.equal_elim A B) der1 der2, 
2386  850 
maxidx = Int.max(max1,max2), 
851 
shyps = [], 

852 
hyps = union_term(hyps1,hyps2), 

853 
prop = B}) 

1529  854 
 _ => err"major premise" 
855 
end; 

0  856 

1220  857 

858 

0  859 
(**** Derived rules ****) 
860 

1503  861 
(*Discharge all hypotheses. Need not verify cterms or call fix_shyps. 
0  862 
Repeated hypotheses are discharged only once; fold cannot do this*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

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

865 
(Thm{sign_ref = sign_ref, 
11518  866 
der = Pt.infer_derivs' (Pt.implies_intr_proof A) der, 
2386  867 
maxidx = maxidx, 
868 
shyps = shyps, 

1529  869 
hyps = disch(As,A), 
2386  870 
prop = implies$A$prop}) 
0  871 
 implies_intr_hyps th = th; 
872 

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

250  874 
Instantiates the theorem and deletes trivial tpairs. 
0  875 
Resulting sequence may contain multiple elements if the tpairs are 
876 
not all flexflex. *) 

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

877 
fun flexflex_rule (th as Thm{sign_ref, der, maxidx, hyps, prop,...}) = 
250  878 
let fun newthm env = 
1529  879 
if Envir.is_empty env then th 
880 
else 

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

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

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

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

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

887 
(Thm{sign_ref = sign_ref, 
11518  888 
der = Pt.infer_derivs' (Pt.norm_proof' env) der, 
2386  889 
maxidx = maxidx_of_term newprop, 
890 
shyps = [], 

891 
hyps = hyps, 

892 
prop = newprop}) 

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

896 
(Unify.smash_unifiers(Sign.deref sign_ref, Envir.empty maxidx, tpairs)) 
0  897 
end; 
898 

899 
(*Instantiation of Vars 

1220  900 
A 
901 
 

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

903 
*) 

0  904 

6928  905 
local 
906 

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

909 

6928  910 
fun prt_typing sg_ref t T = 
911 
let val sg = Sign.deref sg_ref in 

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

913 
end; 

914 

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

916 
fun add_ctpair ((ct,cu), (sign_ref,tpairs)) = 
6928  917 
let 
918 
val Cterm {sign_ref=sign_reft, t=t, T= T, ...} = ct 

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

920 
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

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

924 
Pretty.fbrk, prt_typing sign_ref_merged t T, 

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

0  926 
end; 
927 

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

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

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

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

6928  932 
in 
933 

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

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

936 
No longer normalizes the new theorem! *) 
1529  937 
fun instantiate ([], []) th = th 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

939 
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

940 
val (newsign_ref,vTs) = foldr add_ctyp (vcTs, (newsign_ref,[])); 
8129
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8066
diff
changeset

941 
val newprop = subst_atomic tpairs 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8066
diff
changeset

942 
(Type.inst_term_tvars 
29e239c7b8c2
Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents:
8066
diff
changeset

943 
(Sign.tsig_of (Sign.deref newsign_ref),vTs) prop) 
1220  944 
val newth = 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

945 
(Thm{sign_ref = newsign_ref, 
11518  946 
der = Pt.infer_derivs' (Pt.instantiate vTs tpairs) der, 
10416
5b33e732e459
 Moved rewriting functions to meta_simplifier.ML
berghofe
parents:
10348
diff
changeset

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

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

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

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

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

8291  955 
else nodup_vars newth "instantiate" 
0  956 
end 
6928  957 
handle TERM _ => raise THM("instantiate: incompatible signatures", 0, [th]) 
958 
 TYPE (msg, _, _) => raise THM (msg, 0, [th]); 

959 

960 
end; 

961 

0  962 

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

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

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

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

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

970 
(Thm{sign_ref = sign_ref, 
11518  971 
der = Pt.infer_derivs' I (false, Pt.AbsP ("H", None, Pt.PBound 0)), 
2386  972 
maxidx = maxidx, 
973 
shyps = [], 

974 
hyps = [], 

975 
prop = implies$A$A}) 

0  976 
end; 
977 

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

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

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

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

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

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

2386  988 
maxidx = maxidx, 
989 
shyps = [], 

990 
hyps = [], 

991 
prop = t}) 

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

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

993 

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

994 

6786  995 
(* Replace all TFrees not fixed or in the hyps by new TVars *) 
996 
fun varifyT' fixed (Thm{sign_ref,der,maxidx,shyps,hyps,prop}) = 

12500  997 
let 
998 
val tfrees = foldr add_term_tfree_names (hyps, fixed); 

999 
val (prop', al) = Type.varify (prop, tfrees); 

1634  1000 
in let val thm = (*no fix_shyps*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

1001 
Thm{sign_ref = sign_ref, 
11518  1002 
der = Pt.infer_derivs' (Pt.varify_proof prop tfrees) der, 
2386  1003 
maxidx = Int.max(0,maxidx), 
1004 
shyps = shyps, 

1005 
hyps = hyps, 

12500  1006 
prop = prop'} 
1007 
in (nodup_vars thm "varifyT", al) end 

8291  1008 
(* this nodup_vars check can be removed if thms are guaranteed not to contain 
1009 
duplicate TVars with different sorts *) 

0  1010 
end; 
1011 

12500  1012 
val varifyT = #1 o varifyT' []; 
6786  1013 

0  1014 
(* Replace all TVars by new TFrees *) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

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

1018 
Thm{sign_ref = sign_ref, 
11518  1019 
der = Pt.infer_derivs' (Pt.freezeT prop) der, 
2386  1020 
maxidx = maxidx_of_term prop', 
1021 
shyps = shyps, 

1022 
hyps = hyps, 

1529  1023 
prop = prop'} 
1220  1024 
end; 
0  1025 

1026 

1027 
(*** Inference rules for tactics ***) 

1028 

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

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

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

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

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

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

1035 
end 

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

1037 

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

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

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

1044 
val ct_Bi = Cterm {sign_ref=ssign_ref, maxidx=smax, T=propT, t=Bi} 
1529  1045 
val (lift_abs,lift_all) = Logic.lift_fns(Bi,smax+1) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

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

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

1052 
shyps=union_sort(sshyps,shyps), 
2386  1053 
hyps=hyps, 
1529  1054 
prop = Logic.rule_of (map (pairself lift_abs) tpairs, 
2386  1055 
map lift_all As, 
1056 
lift_all B)} 

0  1057 
end; 
1058 

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

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

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

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

1062 
Thm {sign_ref = sign_ref, 
11518  1063 
der = Pt.infer_derivs' (Pt.map_proof_terms 
1064 
(Logic.incr_indexes ([], i)) (incr_tvar i)) der, 

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

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

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

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

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

1069 

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

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

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

1076 
(Thm{sign_ref = sign_ref, 
11518  1077 
der = Pt.infer_derivs' 
1078 
((if Envir.is_empty env then I else (Pt.norm_proof' env)) o 

1079 
Pt.assumption_proof Bs Bi n) der, 

2386  1080 
maxidx = maxidx, 
1081 
shyps = [], 

1082 
hyps = hyps, 

1083 
prop = 

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

1085 
Logic.rule_of (tpairs, Bs, C) 

1086 
else (*normalize the new rule fully*) 

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

11518  1088 
fun addprfs [] _ = Seq.empty 
1089 
 addprfs ((t,u)::apairs) n = Seq.make (fn()=> Seq.pull 

1090 
(Seq.mapp (newth n) 

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

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

0  1094 

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

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

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

1102 
 n => fix_shyps [state] [] 

1103 
(Thm{sign_ref = sign_ref, 

1104 
der = Pt.infer_derivs' 

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

1106 
maxidx = maxidx, 

1107 
shyps = [], 

1108 
hyps = hyps, 

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

0  1110 
end; 
1111 

1112 

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

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

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

1117 
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

1118 
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

1119 
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

1120 
and concl = Logic.strip_imp_concl rest 
2671  1121 
val n = length asms 
11563  1122 
val m = if k<0 then n+k else k 
1123 
val Bi' = if 0=m orelse m=n then Bi 

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

1127 
end 

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

1128 
else raise THM("rotate_rule", k, [state]) 
7264  1129 
in (*no fix_shyps*) 
1130 
Thm{sign_ref = sign_ref, 

11563  1131 
der = Pt.infer_derivs' (Pt.rotate_proof Bs Bi m) der, 
2671  1132 
maxidx = maxidx, 
1133 
shyps = shyps, 

1134 
hyps = hyps, 

11563  1135 
prop = Logic.rule_of (tpairs, Bs @ [Bi'], C)} 
2671  1136 
end; 
1137 

1138 

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

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

1140 
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

1141 
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

1142 
fun permute_prems j k rl = 
322151fe6f02
new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents:
7070
diff
changeset

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

1144 
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

1145 
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

1146 
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

1147 
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

1148 
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

1149 
val n_j = length moved_prems 
11563  1150 
val m = if k<0 then n_j + k else k 
1151 
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

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

1155 
else raise THM("permute_prems:k", k, [rl]) 
7264  1156 
in (*no fix_shyps*) 
1157 
Thm{sign_ref = sign_ref, 

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

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

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

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

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

1164 

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

1165 

0  1166 
(** User renaming of parameters in a subgoal **) 
1167 

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

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

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

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

1172 
fun rename_params_rule (cs, i) state = 

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

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

1176 
val short = length iparams  length cs 

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

1179 
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

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

1184 
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

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

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

1187 
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

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

1190 
(Thm{sign_ref = sign_ref, 
11518  1191 
der = der, 
2386  1192 
maxidx = maxidx, 
1193 
shyps = [], 

1194 
hyps = hyps, 

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

0  1196 
end; 
1197 

12982  1198 

0  1199 
(*** Preservation of bound variable names ***) 
1200 

12982  1201 
fun rename_boundvars pat obj (thm as Thm {sign_ref, der, maxidx, hyps, shyps, prop}) = 
1202 
(case Term.rename_abs pat obj prop of 

1203 
None => thm 

1204 
 Some prop' => Thm 

1205 
{sign_ref = sign_ref, 

1206 
der = der, 

1207 
maxidx = maxidx, 

1208 
hyps = hyps, 

1209 
shyps = shyps, 

1210 
prop = prop'}); 

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

1211 

0  1212 

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

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

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

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

1220 
 strip(A,_) = f A 

0  1221 
in strip end; 
1222 

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

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

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

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

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

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

1230 
(*unknowns appearing elsewhere be preserved!*) 

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

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

1233 
(case assoc(al,x) of 

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

1234 
Some(y) => if x mem_string vids orelse y mem_string vids then t 
250  1235 
else Var((y,i),T) 
1236 
 None=> t) 

0  1237 
 rename(Abs(x,T,t)) = 
9721  1238 
Abs(if_none(assoc_string(al,x)) x, T, rename t) 
0  1239 
 rename(f$t) = rename f $ rename t 
1240 
 rename(t) = t; 

250  1241 
fun strip_ren Ai = strip_apply rename (Ai,B) 
0  1242 
in strip_ren end; 
1243 

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

1245 
fun rename_bvars(dpairs, tpairs, B) = 

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

1248 

1249 
(*** RESOLUTION ***) 

1250 

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

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

1252 

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

250  1255 
fun strip_assums2 (Const("==>", _) $ _ $ B1, 
1256 
Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2) 

0  1257 
 strip_assums2 (Const("all",_)$Abs(a,T,t1), 
250  1258 
Const("all",_)$Abs(_,_,t2)) = 
0  1259 
let val (B1,B2) = strip_assums2 (t1,t2) 
1260 
in (Abs(a,T,B1), Abs(a,T,B2)) end 

1261 
 strip_assums2 BB = BB; 

1262 

1263 

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

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

1265 
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

1266 
 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

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

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

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

1271 
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

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

1274 
 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

1275 

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

1276 

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

1281 
If eres_flg then simultaneously proves A1 by assumption. 

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

4270  1285 
local exception COMPOSE 
0  1286 
in 
250  1287 
fun bicompose_aux match (state, (stpairs, Bs, Bi, C), lifted) 
0  1288 
(eres_flg, orule, nsubgoal) = 
1529  1289 
let val Thm{der=sder, maxidx=smax, shyps=sshyps, hyps=shyps, ...} = state 
1290 
and Thm{der=rder, maxidx=rmax, shyps=rshyps, hyps=rhyps, 

2386  1291 
prop=rprop,...} = orule 
1529  1292 
(*How many hyps to skip over during normalization*) 
1238  1293 
and nlift = Logic.count_prems(strip_all_body Bi, 
1294 
if eres_flg then ~1 else 0) 

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

1295 
val sign_ref = merge_thm_sgs(state,orule); 
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

1296 
val sign = Sign.deref sign_ref; 
0  1297 
(** Add new theorem with prop = '[ Bs; As ] ==> C' to thq **) 
11518  1298 
fun addth A (As, oldAs, rder', n) ((env as Envir.Envir {maxidx, ...}, tpairs), thq) = 
250  1299 
let val normt = Envir.norm_term env; 
1300 
(*perform minimal copying here by examining env*) 

1301 
val normp = 

1302 
if Envir.is_empty env then (tpairs, Bs @ As, C) 

1303 
else 

1304 
let val ntps = map (pairself normt) tpairs 

2147  1305 
in if Envir.above (smax, env) then 
1238  1306 
(*no assignments in state; normalize the rule only*) 
1307 
if lifted 

1308 
then (ntps, Bs @ map (norm_term_skip env nlift) As, C) 

1309 
else (ntps, Bs @ map normt As, C) 

1529  1310 
else if match then raise COMPOSE 
250  1311 
else (*normalize the new rule fully*) 
1312 
(ntps, map normt (Bs @ As), normt C) 

1313 
end 

1258  1314 
val th = (*tuned fix_shyps*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3895
diff
changeset

1315 
Thm{sign_ref = sign_ref, 
11518  1316 
der = Pt.infer_derivs 
1317 
((if Envir.is_empty env then I 

1318 
else if Envir.above (smax, env) then 

1319 
(fn f => fn der => f (Pt.norm_proof' env der)) 

1320 
else 

1321 
curry op oo (Pt.norm_proof' env)) 

1322 
(Pt.bicompose_proof Bs oldAs As A n)) rder' sder, 

2386  1323 
maxidx = maxidx, 
1324 
shyps = add_env_sorts (env, union_sort(rshyps,sshyps)), 

1325 
hyps = union_term(rhyps,shyps), 

1326 
prop = Logic.rule_of normp} 

11518  1327 
in Seq.cons(th, thq) end handle COMPOSE => thq; 
0  1328 
val (rtpairs,rhorn) = Logic.strip_flexpairs(rprop); 
1329 
val (rAs,B) = Logic.strip_prems(nsubgoal, [], rhorn) 

1330 
handle TERM _ => raise THM("bicompose: rule", 0, [orule,state]); 

1331 
(*Modify assumptions, deleting nth if n>0 for eresolution*) 

1332 
fun newAs(As0, n, dpairs, tpairs) = 

11518  1333 
let val (As1, rder') = 
1334 
if !Logic.auto_rename orelse not lifted then (As0, rder) 

1335 
else (map (rename_bvars(dpairs,tpairs,B)) As0, 

1336 
Pt.infer_derivs' (Pt.map_proof_terms 

1337 
(rename_bvars (dpairs, tpairs, Bound 0)) I) rder); 

1338 
in (map (Logic.flatten_params n) As1, As1, rder', n) 

250  1339 
handle TERM _ => 
1340 
raise THM("bicompose: 1st premise", 0, [orule]) 

0  1341 
end; 
2147  1342 
val env = Envir.empty(Int.max(rmax,smax)); 
0  1343 
val BBi = if lifted then strip_assums2(B,Bi) else (B,Bi); 
1344 
val dpairs = BBi :: (rtpairs@stpairs); 

1345 
(*elimresolution: try each assumption in turn. Initially n=1*) 

11518  1346 
fun tryasms (_, _, _, []) = Seq.empty 
1347 
 tryasms (A, As, n, (t,u)::apairs) = 

4270 