1 (* Title: Pure/thm.ML |
1 (* Title: Pure/thm.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1994 University of Cambridge |
4 Copyright 1994 University of Cambridge |
5 |
5 |
6 The core of Isabelle's Meta Logic: certified types and terms, meta |
6 The very core of Isabelle's Meta Logic: certified types and terms, |
7 theorems, meta rules (including lifting and resolution). |
7 meta theorems, meta rules (including lifting and resolution). |
8 *) |
8 *) |
9 |
9 |
10 signature BASIC_THM = |
10 signature BASIC_THM = |
11 sig |
11 sig |
12 (*certified types*) |
12 (*certified types*) |
13 type ctyp |
13 type ctyp |
14 val rep_ctyp : ctyp -> {sign: Sign.sg, T: typ} |
14 val rep_ctyp: ctyp -> {thy: theory, sign: theory, T: typ} |
15 val typ_of : ctyp -> typ |
15 val theory_of_ctyp: ctyp -> theory |
16 val ctyp_of : Sign.sg -> typ -> ctyp |
16 val typ_of: ctyp -> typ |
17 val read_ctyp : Sign.sg -> string -> ctyp |
17 val ctyp_of: theory -> typ -> ctyp |
|
18 val read_ctyp: theory -> string -> ctyp |
18 |
19 |
19 (*certified terms*) |
20 (*certified terms*) |
20 type cterm |
21 type cterm |
21 exception CTERM of string |
22 exception CTERM of string |
22 val rep_cterm : cterm -> {sign: Sign.sg, t: term, T: typ, maxidx: int} |
23 val rep_cterm: cterm -> {thy: theory, sign: theory, t: term, T: typ, maxidx: int} |
23 val crep_cterm : cterm -> {sign: Sign.sg, t: term, T: ctyp, maxidx: int} |
24 val crep_cterm: cterm -> {thy: theory, sign: theory, t: term, T: ctyp, maxidx: int} |
24 val sign_of_cterm : cterm -> Sign.sg |
25 val theory_of_cterm: cterm -> theory |
25 val term_of : cterm -> term |
26 val sign_of_cterm: cterm -> theory (*obsolete*) |
26 val cterm_of : Sign.sg -> term -> cterm |
27 val term_of: cterm -> term |
27 val ctyp_of_term : cterm -> ctyp |
28 val cterm_of: theory -> term -> cterm |
28 val read_cterm : Sign.sg -> string * typ -> cterm |
29 val ctyp_of_term: cterm -> ctyp |
29 val adjust_maxidx : cterm -> cterm |
30 val read_cterm: theory -> string * typ -> cterm |
30 val read_def_cterm : |
31 val adjust_maxidx: cterm -> cterm |
31 Sign.sg * (indexname -> typ option) * (indexname -> sort option) -> |
32 val read_def_cterm: |
|
33 theory * (indexname -> typ option) * (indexname -> sort option) -> |
32 string list -> bool -> string * typ -> cterm * (indexname * typ) list |
34 string list -> bool -> string * typ -> cterm * (indexname * typ) list |
33 val read_def_cterms : |
35 val read_def_cterms: |
34 Sign.sg * (indexname -> typ option) * (indexname -> sort option) -> |
36 theory * (indexname -> typ option) * (indexname -> sort option) -> |
35 string list -> bool -> (string * typ)list |
37 string list -> bool -> (string * typ)list |
36 -> cterm list * (indexname * typ)list |
38 -> cterm list * (indexname * typ)list |
37 |
39 |
38 type tag (* = string * string list *) |
40 type tag (* = string * string list *) |
39 |
41 |
40 (*meta theorems*) |
42 (*meta theorems*) |
41 type thm |
43 type thm |
42 val rep_thm : thm -> {sign: Sign.sg, der: bool * Proofterm.proof, maxidx: int, |
44 val rep_thm: thm -> |
43 shyps: sort list, hyps: term list, |
45 {thy: theory, sign: theory, |
44 tpairs: (term * term) list, prop: term} |
46 der: bool * Proofterm.proof, |
45 val crep_thm : thm -> {sign: Sign.sg, der: bool * Proofterm.proof, maxidx: int, |
47 maxidx: int, |
46 shyps: sort list, hyps: cterm list, |
48 shyps: sort list, |
47 tpairs: (cterm * cterm) list, prop: cterm} |
49 hyps: term list, |
|
50 tpairs: (term * term) list, |
|
51 prop: term} |
|
52 val crep_thm: thm -> |
|
53 {thy: theory, sign: theory, |
|
54 der: bool * Proofterm.proof, |
|
55 maxidx: int, |
|
56 shyps: sort list, |
|
57 hyps: cterm list, |
|
58 tpairs: (cterm * cterm) list, |
|
59 prop: cterm} |
48 exception THM of string * int * thm list |
60 exception THM of string * int * thm list |
49 type 'a attribute (* = 'a * thm -> 'a * thm *) |
61 type 'a attribute (* = 'a * thm -> 'a * thm *) |
50 val eq_thm : thm * thm -> bool |
62 val eq_thm: thm * thm -> bool |
51 val eq_thms : thm list * thm list -> bool |
63 val eq_thms: thm list * thm list -> bool |
52 val sign_of_thm : thm -> Sign.sg |
64 val theory_of_thm: thm -> theory |
53 val prop_of : thm -> term |
65 val sign_of_thm: thm -> theory (*obsolete*) |
54 val proof_of : thm -> Proofterm.proof |
66 val prop_of: thm -> term |
55 val transfer_sg : Sign.sg -> thm -> thm |
67 val proof_of: thm -> Proofterm.proof |
56 val transfer : theory -> thm -> thm |
68 val transfer: theory -> thm -> thm |
57 val tpairs_of : thm -> (term * term) list |
69 val tpairs_of: thm -> (term * term) list |
58 val prems_of : thm -> term list |
70 val prems_of: thm -> term list |
59 val nprems_of : thm -> int |
71 val nprems_of: thm -> int |
60 val concl_of : thm -> term |
72 val concl_of: thm -> term |
61 val cprop_of : thm -> cterm |
73 val cprop_of: thm -> cterm |
62 val extra_shyps : thm -> sort list |
74 val extra_shyps: thm -> sort list |
63 val strip_shyps : thm -> thm |
75 val strip_shyps: thm -> thm |
64 val get_axiom_i : theory -> string -> thm |
76 val get_axiom_i: theory -> string -> thm |
65 val get_axiom : theory -> xstring -> thm |
77 val get_axiom: theory -> xstring -> thm |
66 val def_name : string -> string |
78 val def_name: string -> string |
67 val get_def : theory -> xstring -> thm |
79 val get_def: theory -> xstring -> thm |
68 val axioms_of : theory -> (string * thm) list |
80 val axioms_of: theory -> (string * thm) list |
69 |
81 |
70 (*meta rules*) |
82 (*meta rules*) |
71 val assume : cterm -> thm |
83 val assume: cterm -> thm |
72 val compress : thm -> thm |
84 val compress: thm -> thm |
73 val implies_intr : cterm -> thm -> thm |
85 val implies_intr: cterm -> thm -> thm |
74 val implies_elim : thm -> thm -> thm |
86 val implies_elim: thm -> thm -> thm |
75 val forall_intr : cterm -> thm -> thm |
87 val forall_intr: cterm -> thm -> thm |
76 val forall_elim : cterm -> thm -> thm |
88 val forall_elim: cterm -> thm -> thm |
77 val reflexive : cterm -> thm |
89 val reflexive: cterm -> thm |
78 val symmetric : thm -> thm |
90 val symmetric: thm -> thm |
79 val transitive : thm -> thm -> thm |
91 val transitive: thm -> thm -> thm |
80 val beta_conversion : bool -> cterm -> thm |
92 val beta_conversion: bool -> cterm -> thm |
81 val eta_conversion : cterm -> thm |
93 val eta_conversion: cterm -> thm |
82 val abstract_rule : string -> cterm -> thm -> thm |
94 val abstract_rule: string -> cterm -> thm -> thm |
83 val combination : thm -> thm -> thm |
95 val combination: thm -> thm -> thm |
84 val equal_intr : thm -> thm -> thm |
96 val equal_intr: thm -> thm -> thm |
85 val equal_elim : thm -> thm -> thm |
97 val equal_elim: thm -> thm -> thm |
86 val implies_intr_hyps : thm -> thm |
98 val implies_intr_hyps: thm -> thm |
87 val flexflex_rule : thm -> thm Seq.seq |
99 val flexflex_rule: thm -> thm Seq.seq |
88 val instantiate : |
100 val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm |
89 (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm |
101 val trivial: cterm -> thm |
90 val trivial : cterm -> thm |
102 val class_triv: theory -> class -> thm |
91 val class_triv : Sign.sg -> class -> thm |
103 val varifyT: thm -> thm |
92 val varifyT : thm -> thm |
104 val varifyT': (string * sort) list -> thm -> thm * ((string * sort) * indexname) list |
93 val varifyT' : (string * sort) list -> thm -> thm * ((string * sort) * indexname) list |
105 val freezeT: thm -> thm |
94 val freezeT : thm -> thm |
106 val dest_state: thm * int -> (term * term) list * term list * term * term |
95 val dest_state : thm * int -> |
107 val lift_rule: (thm * int) -> thm -> thm |
96 (term * term) list * term list * term * term |
108 val incr_indexes: int -> thm -> thm |
97 val lift_rule : (thm * int) -> thm -> thm |
109 val assumption: int -> thm -> thm Seq.seq |
98 val incr_indexes : int -> thm -> thm |
110 val eq_assumption: int -> thm -> thm |
99 val assumption : int -> thm -> thm Seq.seq |
111 val rotate_rule: int -> int -> thm -> thm |
100 val eq_assumption : int -> thm -> thm |
112 val permute_prems: int -> int -> thm -> thm |
101 val rotate_rule : int -> int -> thm -> thm |
|
102 val permute_prems : int -> int -> thm -> thm |
|
103 val rename_params_rule: string list * int -> thm -> thm |
113 val rename_params_rule: string list * int -> thm -> thm |
104 val bicompose : bool -> bool * thm * int -> |
114 val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq |
105 int -> thm -> thm Seq.seq |
115 val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq |
106 val biresolution : bool -> (bool * thm) list -> |
116 val invoke_oracle: theory -> xstring -> theory * Object.T -> thm |
107 int -> thm -> thm Seq.seq |
117 val invoke_oracle_i: theory -> string -> theory * Object.T -> thm |
108 val invoke_oracle_i : theory -> string -> Sign.sg * Object.T -> thm |
|
109 val invoke_oracle : theory -> xstring -> Sign.sg * Object.T -> thm |
|
110 end; |
118 end; |
111 |
119 |
112 signature THM = |
120 signature THM = |
113 sig |
121 sig |
114 include BASIC_THM |
122 include BASIC_THM |
115 val dest_ctyp : ctyp -> ctyp list |
123 val dest_ctyp: ctyp -> ctyp list |
116 val dest_comb : cterm -> cterm * cterm |
124 val dest_comb: cterm -> cterm * cterm |
117 val dest_abs : string option -> cterm -> cterm * cterm |
125 val dest_abs: string option -> cterm -> cterm * cterm |
118 val capply : cterm -> cterm -> cterm |
126 val capply: cterm -> cterm -> cterm |
119 val cabs : cterm -> cterm -> cterm |
127 val cabs: cterm -> cterm -> cterm |
120 val major_prem_of : thm -> term |
128 val major_prem_of: thm -> term |
121 val no_prems : thm -> bool |
129 val no_prems: thm -> bool |
122 val no_attributes : 'a -> 'a * 'b attribute list |
130 val no_attributes: 'a -> 'a * 'b attribute list |
123 val apply_attributes : ('a * thm) * 'a attribute list -> ('a * thm) |
131 val apply_attributes: ('a * thm) * 'a attribute list -> ('a * thm) |
124 val applys_attributes : ('a * thm list) * 'a attribute list -> ('a * thm list) |
132 val applys_attributes: ('a * thm list) * 'a attribute list -> ('a * thm list) |
125 val get_name_tags : thm -> string * tag list |
133 val get_name_tags: thm -> string * tag list |
126 val put_name_tags : string * tag list -> thm -> thm |
134 val put_name_tags: string * tag list -> thm -> thm |
127 val name_of_thm : thm -> string |
135 val name_of_thm: thm -> string |
128 val tags_of_thm : thm -> tag list |
136 val tags_of_thm: thm -> tag list |
129 val name_thm : string * thm -> thm |
137 val name_thm: string * thm -> thm |
130 val rename_boundvars : term -> term -> thm -> thm |
138 val rename_boundvars: term -> term -> thm -> thm |
131 val cterm_match : cterm * cterm -> |
139 val cterm_match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list |
132 (ctyp * ctyp) list * (cterm * cterm) list |
140 val cterm_first_order_match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list |
133 val cterm_first_order_match : cterm * cterm -> |
141 val cterm_incr_indexes: int -> cterm -> cterm |
134 (ctyp * ctyp) list * (cterm * cterm) list |
142 val terms_of_tpairs: (term * term) list -> term list |
135 val cterm_incr_indexes : int -> cterm -> cterm |
|
136 val terms_of_tpairs : (term * term) list -> term list |
|
137 end; |
143 end; |
138 |
144 |
139 structure Thm: THM = |
145 structure Thm: THM = |
140 struct |
146 struct |
141 |
147 |
142 (*** Certified terms and types ***) |
148 (*** Certified terms and types ***) |
143 |
149 |
144 (** certified types **) |
150 (** certified types **) |
145 |
151 |
146 (*certified typs under a signature*) |
152 datatype ctyp = Ctyp of {thy_ref: theory_ref, T: typ}; |
147 |
153 |
148 datatype ctyp = Ctyp of {sign_ref: Sign.sg_ref, T: typ}; |
154 fun rep_ctyp (Ctyp {thy_ref, T}) = |
149 |
155 let val thy = Theory.deref thy_ref |
150 fun rep_ctyp (Ctyp {sign_ref, T}) = {sign = Sign.deref sign_ref, T = T}; |
156 in {thy = thy, sign = thy, T = T} end; |
|
157 |
|
158 val theory_of_ctyp = #thy o rep_ctyp; |
|
159 |
151 fun typ_of (Ctyp {T, ...}) = T; |
160 fun typ_of (Ctyp {T, ...}) = T; |
152 |
161 |
153 fun ctyp_of sign T = |
162 fun ctyp_of thy T = |
154 Ctyp {sign_ref = Sign.self_ref sign, T = Sign.certify_typ sign T}; |
163 Ctyp {thy_ref = Theory.self_ref thy, T = Sign.certify_typ thy T}; |
155 |
164 |
156 fun read_ctyp sign s = |
165 fun read_ctyp thy s = |
157 Ctyp {sign_ref = Sign.self_ref sign, T = Sign.read_typ (sign, K NONE) s}; |
166 Ctyp {thy_ref = Theory.self_ref thy, T = Sign.read_typ (thy, K NONE) s}; |
158 |
167 |
159 fun dest_ctyp (Ctyp {sign_ref, T = Type (s, Ts)}) = |
168 fun dest_ctyp (Ctyp {thy_ref, T = Type (s, Ts)}) = |
160 map (fn T => Ctyp {sign_ref = sign_ref, T = T}) Ts |
169 map (fn T => Ctyp {thy_ref = thy_ref, T = T}) Ts |
161 | dest_ctyp ct = [ct]; |
170 | dest_ctyp ct = [ct]; |
162 |
171 |
163 |
172 |
164 |
173 |
165 (** certified terms **) |
174 (** certified terms **) |
166 |
175 |
167 (*certified terms under a signature, with checked typ and maxidx of Vars*) |
176 (*certified terms with checked typ and maxidx of Vars/TVars*) |
168 |
177 |
169 datatype cterm = Cterm of {sign_ref: Sign.sg_ref, t: term, T: typ, maxidx: int}; |
178 datatype cterm = Cterm of {thy_ref: theory_ref, t: term, T: typ, maxidx: int}; |
170 |
179 |
171 fun rep_cterm (Cterm {sign_ref, t, T, maxidx}) = |
180 fun rep_cterm (Cterm {thy_ref, t, T, maxidx}) = |
172 {sign = Sign.deref sign_ref, t = t, T = T, maxidx = maxidx}; |
181 let val thy = Theory.deref thy_ref |
173 |
182 in {thy = thy, sign = thy, t = t, T = T, maxidx = maxidx} end; |
174 fun crep_cterm (Cterm {sign_ref, t, T, maxidx}) = |
183 |
175 {sign = Sign.deref sign_ref, t = t, T = Ctyp {sign_ref = sign_ref, T = T}, |
184 fun crep_cterm (Cterm {thy_ref, t, T, maxidx}) = |
176 maxidx = maxidx}; |
185 let val thy = Theory.deref thy_ref in |
177 |
186 {thy = thy, sign = thy, t = t, T = Ctyp {thy_ref = thy_ref, T = T}, maxidx = maxidx} |
178 fun sign_of_cterm (Cterm {sign_ref, ...}) = Sign.deref sign_ref; |
187 end; |
|
188 |
|
189 fun theory_of_cterm (Cterm {thy_ref, ...}) = Theory.deref thy_ref; |
|
190 val sign_of_cterm = theory_of_cterm; |
179 |
191 |
180 fun term_of (Cterm {t, ...}) = t; |
192 fun term_of (Cterm {t, ...}) = t; |
181 |
193 |
182 fun ctyp_of_term (Cterm {sign_ref, T, ...}) = Ctyp {sign_ref = sign_ref, T = T}; |
194 fun ctyp_of_term (Cterm {thy_ref, T, ...}) = Ctyp {thy_ref = thy_ref, T = T}; |
183 |
195 |
184 (*create a cterm by checking a "raw" term with respect to a signature*) |
196 fun cterm_of thy tm = |
185 fun cterm_of sign tm = |
197 let val (t, T, maxidx) = Sign.certify_term (Sign.pp thy) thy tm |
186 let val (t, T, maxidx) = Sign.certify_term (Sign.pp sign) sign tm |
198 in Cterm {thy_ref = Theory.self_ref thy, t = t, T = T, maxidx = maxidx} |
187 in Cterm {sign_ref = Sign.self_ref sign, t = t, T = T, maxidx = maxidx} |
|
188 end; |
199 end; |
189 |
200 |
190 |
201 |
191 exception CTERM of string; |
202 exception CTERM of string; |
192 |
203 |
193 (*Destruct application in cterms*) |
204 (*Destruct application in cterms*) |
194 fun dest_comb (Cterm {sign_ref, T, maxidx, t = A $ B}) = |
205 fun dest_comb (Cterm {thy_ref, T, maxidx, t = A $ B}) = |
195 let val typeA = fastype_of A; |
206 let val typeA = fastype_of A; |
196 val typeB = |
207 val typeB = |
197 case typeA of Type("fun",[S,T]) => S |
208 case typeA of Type("fun",[S,T]) => S |
198 | _ => error "Function type expected in dest_comb"; |
209 | _ => error "Function type expected in dest_comb"; |
199 in |
210 in |
200 (Cterm {sign_ref=sign_ref, maxidx=maxidx, t=A, T=typeA}, |
211 (Cterm {thy_ref=thy_ref, maxidx=maxidx, t=A, T=typeA}, |
201 Cterm {sign_ref=sign_ref, maxidx=maxidx, t=B, T=typeB}) |
212 Cterm {thy_ref=thy_ref, maxidx=maxidx, t=B, T=typeB}) |
202 end |
213 end |
203 | dest_comb _ = raise CTERM "dest_comb"; |
214 | dest_comb _ = raise CTERM "dest_comb"; |
204 |
215 |
205 (*Destruct abstraction in cterms*) |
216 (*Destruct abstraction in cterms*) |
206 fun dest_abs a (Cterm {sign_ref, T as Type("fun",[_,S]), maxidx, t=Abs(x,ty,M)}) = |
217 fun dest_abs a (Cterm {thy_ref, T as Type("fun",[_,S]), maxidx, t=Abs(x,ty,M)}) = |
207 let val (y,N) = variant_abs (getOpt (a,x),ty,M) |
218 let val (y,N) = variant_abs (if_none a x, ty, M) |
208 in (Cterm {sign_ref = sign_ref, T = ty, maxidx = 0, t = Free(y,ty)}, |
219 in (Cterm {thy_ref = thy_ref, T = ty, maxidx = 0, t = Free(y,ty)}, |
209 Cterm {sign_ref = sign_ref, T = S, maxidx = maxidx, t = N}) |
220 Cterm {thy_ref = thy_ref, T = S, maxidx = maxidx, t = N}) |
210 end |
221 end |
211 | dest_abs _ _ = raise CTERM "dest_abs"; |
222 | dest_abs _ _ = raise CTERM "dest_abs"; |
212 |
223 |
213 (*Makes maxidx precise: it is often too big*) |
224 (*Makes maxidx precise: it is often too big*) |
214 fun adjust_maxidx (ct as Cterm {sign_ref, T, t, maxidx, ...}) = |
225 fun adjust_maxidx (ct as Cterm {thy_ref, T, t, maxidx, ...}) = |
215 if maxidx = ~1 then ct |
226 if maxidx = ~1 then ct |
216 else Cterm {sign_ref = sign_ref, T = T, maxidx = maxidx_of_term t, t = t}; |
227 else Cterm {thy_ref = thy_ref, T = T, maxidx = maxidx_of_term t, t = t}; |
217 |
228 |
218 (*Form cterm out of a function and an argument*) |
229 (*Form cterm out of a function and an argument*) |
219 fun capply (Cterm {t=f, sign_ref=sign_ref1, T=Type("fun",[dty,rty]), maxidx=maxidx1}) |
230 fun capply (Cterm {t=f, thy_ref=thy_ref1, T=Type("fun",[dty,rty]), maxidx=maxidx1}) |
220 (Cterm {t=x, sign_ref=sign_ref2, T, maxidx=maxidx2}) = |
231 (Cterm {t=x, thy_ref=thy_ref2, T, maxidx=maxidx2}) = |
221 if T = dty then |
232 if T = dty then |
222 Cterm{t = f $ x, |
233 Cterm{t = f $ x, |
223 sign_ref=Sign.merge_refs(sign_ref1,sign_ref2), T=rty, |
234 thy_ref=Theory.merge_refs(thy_ref1,thy_ref2), T=rty, |
224 maxidx=Int.max(maxidx1, maxidx2)} |
235 maxidx=Int.max(maxidx1, maxidx2)} |
225 else raise CTERM "capply: types don't agree" |
236 else raise CTERM "capply: types don't agree" |
226 | capply _ _ = raise CTERM "capply: first arg is not a function" |
237 | capply _ _ = raise CTERM "capply: first arg is not a function" |
227 |
238 |
228 fun cabs (Cterm {t=t1, sign_ref=sign_ref1, T=T1, maxidx=maxidx1}) |
239 fun cabs (Cterm {t=t1, thy_ref=thy_ref1, T=T1, maxidx=maxidx1}) |
229 (Cterm {t=t2, sign_ref=sign_ref2, T=T2, maxidx=maxidx2}) = |
240 (Cterm {t=t2, thy_ref=thy_ref2, T=T2, maxidx=maxidx2}) = |
230 Cterm {t = lambda t1 t2, sign_ref = Sign.merge_refs (sign_ref1,sign_ref2), |
241 Cterm {t = lambda t1 t2, thy_ref = Theory.merge_refs (thy_ref1,thy_ref2), |
231 T = T1 --> T2, maxidx=Int.max(maxidx1, maxidx2)} |
242 T = T1 --> T2, maxidx=Int.max(maxidx1, maxidx2)} |
232 handle TERM _ => raise CTERM "cabs: first arg is not a variable"; |
243 handle TERM _ => raise CTERM "cabs: first arg is not a variable"; |
233 |
244 |
234 (*Matching of cterms*) |
245 (*Matching of cterms*) |
235 fun gen_cterm_match mtch |
246 fun gen_cterm_match mtch |
236 (Cterm {sign_ref = sign_ref1, maxidx = maxidx1, t = t1, ...}, |
247 (Cterm {thy_ref = thy_ref1, maxidx = maxidx1, t = t1, ...}, |
237 Cterm {sign_ref = sign_ref2, maxidx = maxidx2, t = t2, ...}) = |
248 Cterm {thy_ref = thy_ref2, maxidx = maxidx2, t = t2, ...}) = |
238 let |
249 let |
239 val sign_ref = Sign.merge_refs (sign_ref1, sign_ref2); |
250 val thy_ref = Theory.merge_refs (thy_ref1, thy_ref2); |
240 val tsig = Sign.tsig_of (Sign.deref sign_ref); |
251 val tsig = Sign.tsig_of (Theory.deref thy_ref); |
241 val (Tinsts, tinsts) = mtch tsig (t1, t2); |
252 val (Tinsts, tinsts) = mtch tsig (t1, t2); |
242 val maxidx = Int.max (maxidx1, maxidx2); |
253 val maxidx = Int.max (maxidx1, maxidx2); |
243 fun mk_cTinsts (ixn, (S, T)) = |
254 fun mk_cTinsts (ixn, (S, T)) = |
244 (Ctyp {sign_ref = sign_ref, T = TVar (ixn, S)}, |
255 (Ctyp {thy_ref = thy_ref, T = TVar (ixn, S)}, |
245 Ctyp {sign_ref = sign_ref, T = T}); |
256 Ctyp {thy_ref = thy_ref, T = T}); |
246 fun mk_ctinsts (ixn, (T, t)) = |
257 fun mk_ctinsts (ixn, (T, t)) = |
247 let val T = Envir.typ_subst_TVars Tinsts T |
258 let val T = Envir.typ_subst_TVars Tinsts T |
248 in |
259 in |
249 (Cterm {sign_ref = sign_ref, maxidx = maxidx, T = T, t = Var (ixn, T)}, |
260 (Cterm {thy_ref = thy_ref, maxidx = maxidx, T = T, t = Var (ixn, T)}, |
250 Cterm {sign_ref = sign_ref, maxidx = maxidx, T = T, t = t}) |
261 Cterm {thy_ref = thy_ref, maxidx = maxidx, T = T, t = t}) |
251 end; |
262 end; |
252 in (map mk_cTinsts (Vartab.dest Tinsts), |
263 in (map mk_cTinsts (Vartab.dest Tinsts), |
253 map mk_ctinsts (Vartab.dest tinsts)) |
264 map mk_ctinsts (Vartab.dest tinsts)) |
254 end; |
265 end; |
255 |
266 |
256 val cterm_match = gen_cterm_match Pattern.match; |
267 val cterm_match = gen_cterm_match Pattern.match; |
257 val cterm_first_order_match = gen_cterm_match Pattern.first_order_match; |
268 val cterm_first_order_match = gen_cterm_match Pattern.first_order_match; |
258 |
269 |
259 (*Incrementing indexes*) |
270 (*Incrementing indexes*) |
260 fun cterm_incr_indexes i (ct as Cterm {sign_ref, maxidx, t, T}) = |
271 fun cterm_incr_indexes i (ct as Cterm {thy_ref, maxidx, t, T}) = |
261 if i < 0 then raise CTERM "negative increment" else |
272 if i < 0 then raise CTERM "negative increment" else |
262 if i = 0 then ct else |
273 if i = 0 then ct else |
263 Cterm {sign_ref = sign_ref, maxidx = maxidx + i, |
274 Cterm {thy_ref = thy_ref, maxidx = maxidx + i, |
264 t = Logic.incr_indexes ([], i) t, T = Term.incr_tvar i T}; |
275 t = Logic.incr_indexes ([], i) t, T = Term.incr_tvar i T}; |
265 |
276 |
266 |
277 |
267 |
278 |
268 (** read cterms **) (*exception ERROR*) |
279 (** read cterms **) (*exception ERROR*) |
269 |
280 |
270 (*read terms, infer types, certify terms*) |
281 (*read terms, infer types, certify terms*) |
271 fun read_def_cterms (sign, types, sorts) used freeze sTs = |
282 fun read_def_cterms (thy, types, sorts) used freeze sTs = |
272 let |
283 let |
273 val (ts', tye) = Sign.read_def_terms (sign, types, sorts) used freeze sTs; |
284 val (ts', tye) = Sign.read_def_terms (thy, types, sorts) used freeze sTs; |
274 val cts = map (cterm_of sign) ts' |
285 val cts = map (cterm_of thy) ts' |
275 handle TYPE (msg, _, _) => error msg |
286 handle TYPE (msg, _, _) => error msg |
276 | TERM (msg, _) => error msg; |
287 | TERM (msg, _) => error msg; |
277 in (cts, tye) end; |
288 in (cts, tye) end; |
278 |
289 |
279 (*read term, infer types, certify term*) |
290 (*read term, infer types, certify term*) |
280 fun read_def_cterm args used freeze aT = |
291 fun read_def_cterm args used freeze aT = |
281 let val ([ct],tye) = read_def_cterms args used freeze [aT] |
292 let val ([ct],tye) = read_def_cterms args used freeze [aT] |
282 in (ct,tye) end; |
293 in (ct,tye) end; |
283 |
294 |
284 fun read_cterm sign = #1 o read_def_cterm (sign, K NONE, K NONE) [] true; |
295 fun read_cterm thy = #1 o read_def_cterm (thy, K NONE, K NONE) [] true; |
285 |
296 |
286 |
297 |
287 (*tags provide additional comment, apart from the axiom/theorem name*) |
298 (*tags provide additional comment, apart from the axiom/theorem name*) |
288 type tag = string * string list; |
299 type tag = string * string list; |
289 |
300 |
304 fun terms_of_tpairs tpairs = List.concat (map (fn (t, u) => [t, u]) tpairs); |
315 fun terms_of_tpairs tpairs = List.concat (map (fn (t, u) => [t, u]) tpairs); |
305 |
316 |
306 fun attach_tpairs tpairs prop = |
317 fun attach_tpairs tpairs prop = |
307 Logic.list_implies (map Logic.mk_equals tpairs, prop); |
318 Logic.list_implies (map Logic.mk_equals tpairs, prop); |
308 |
319 |
309 fun rep_thm (Thm {sign_ref, der, maxidx, shyps, hyps, tpairs, prop}) = |
320 fun rep_thm (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = |
310 {sign = Sign.deref sign_ref, der = der, maxidx = maxidx, |
321 let val thy = Theory.deref thy_ref in |
311 shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}; |
322 {thy = thy, sign = thy, der = der, maxidx = maxidx, |
312 |
323 shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop} |
313 (*Version of rep_thm returning cterms instead of terms*) |
324 end; |
314 fun crep_thm (Thm {sign_ref, der, maxidx, shyps, hyps, tpairs, prop}) = |
325 |
315 let fun ctermf max t = Cterm{sign_ref=sign_ref, t=t, T=propT, maxidx=max}; |
326 (*version of rep_thm returning cterms instead of terms*) |
316 in {sign = Sign.deref sign_ref, der = der, maxidx = maxidx, shyps = shyps, |
327 fun crep_thm (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = |
317 hyps = map (ctermf ~1) hyps, |
328 let |
318 tpairs = map (pairself (ctermf maxidx)) tpairs, |
329 val thy = Theory.deref thy_ref; |
319 prop = ctermf maxidx prop} |
330 fun cterm max t = Cterm {thy_ref = thy_ref, t = t, T = propT, maxidx = max}; |
|
331 in |
|
332 {thy = thy, sign = thy, der = der, maxidx = maxidx, shyps = shyps, |
|
333 hyps = map (cterm ~1) hyps, |
|
334 tpairs = map (pairself (cterm maxidx)) tpairs, |
|
335 prop = cterm maxidx prop} |
320 end; |
336 end; |
321 |
337 |
322 (*errors involving theorems*) |
338 (*errors involving theorems*) |
323 exception THM of string * int * thm list; |
339 exception THM of string * int * thm list; |
324 |
340 |
325 (*attributes subsume any kind of rules or addXXXs modifiers*) |
341 (*attributes subsume any kind of rules or context modifiers*) |
326 type 'a attribute = 'a * thm -> 'a * thm; |
342 type 'a attribute = 'a * thm -> 'a * thm; |
327 |
343 |
328 fun no_attributes x = (x, []); |
344 fun no_attributes x = (x, []); |
329 fun apply_attributes (x_th, atts) = Library.apply atts x_th; |
345 fun apply_attributes (x_th, atts) = Library.apply atts x_th; |
330 fun applys_attributes (x_ths, atts) = foldl_map (Library.apply atts) x_ths; |
346 fun applys_attributes (x_ths, atts) = foldl_map (Library.apply atts) x_ths; |
331 |
347 |
332 fun eq_thm (th1, th2) = |
348 fun eq_thm (th1, th2) = |
333 let |
349 let |
334 val {sign = sg1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1, prop = prop1, ...} = |
350 val {thy = thy1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1, prop = prop1, ...} = |
335 rep_thm th1; |
351 rep_thm th1; |
336 val {sign = sg2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...} = |
352 val {thy = thy2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...} = |
337 rep_thm th2; |
353 rep_thm th2; |
338 in |
354 in |
339 Sign.joinable (sg1, sg2) andalso |
355 (subthy (thy1, thy2) orelse subthy (thy2, thy1)) andalso |
340 Sorts.eq_set_sort (shyps1, shyps2) andalso |
356 Sorts.eq_set_sort (shyps1, shyps2) andalso |
341 aconvs (hyps1, hyps2) andalso |
357 aconvs (hyps1, hyps2) andalso |
342 aconvs (terms_of_tpairs tpairs1, terms_of_tpairs tpairs2) andalso |
358 aconvs (terms_of_tpairs tpairs1, terms_of_tpairs tpairs2) andalso |
343 prop1 aconv prop2 |
359 prop1 aconv prop2 |
344 end; |
360 end; |
345 |
361 |
346 val eq_thms = Library.equal_lists eq_thm; |
362 val eq_thms = Library.equal_lists eq_thm; |
347 |
363 |
348 fun sign_of_thm (Thm {sign_ref, ...}) = Sign.deref sign_ref; |
364 fun theory_of_thm (Thm {thy_ref, ...}) = Theory.deref thy_ref; |
|
365 val sign_of_thm = theory_of_thm; |
|
366 |
349 fun prop_of (Thm {prop, ...}) = prop; |
367 fun prop_of (Thm {prop, ...}) = prop; |
350 fun proof_of (Thm {der = (_, proof), ...}) = proof; |
368 fun proof_of (Thm {der = (_, proof), ...}) = proof; |
351 |
369 |
352 (*merge signatures of two theorems; raise exception if incompatible*) |
370 (*merge theories of two theorems; raise exception if incompatible*) |
353 fun merge_thm_sgs |
371 fun merge_thm_thys |
354 (th1 as Thm {sign_ref = sgr1, ...}, th2 as Thm {sign_ref = sgr2, ...}) = |
372 (th1 as Thm {thy_ref = r1, ...}, th2 as Thm {thy_ref = r2, ...}) = |
355 Sign.merge_refs (sgr1, sgr2) handle TERM (msg, _) => raise THM (msg, 0, [th1, th2]); |
373 Theory.merge_refs (r1, r2) handle TERM (msg, _) => raise THM (msg, 0, [th1, th2]); |
356 |
374 |
357 (*transfer thm to super theory (non-destructive)*) |
375 (*transfer thm to super theory (non-destructive)*) |
358 fun transfer_sg sign' thm = |
376 fun transfer thy' thm = |
359 let |
377 let |
360 val Thm {sign_ref, der, maxidx, shyps, hyps, tpairs, prop} = thm; |
378 val Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop} = thm; |
361 val sign = Sign.deref sign_ref; |
379 val thy = Theory.deref thy_ref; |
362 in |
380 in |
363 if Sign.eq_sg (sign, sign') then thm |
381 if eq_thy (thy, thy') then thm |
364 else if Sign.subsig (sign, sign') then |
382 else if subthy (thy, thy') then |
365 Thm {sign_ref = Sign.self_ref sign', der = der, maxidx = maxidx, |
383 Thm {thy_ref = Theory.self_ref thy', der = der, maxidx = maxidx, |
366 shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop} |
384 shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop} |
367 else raise THM ("transfer: not a super theory", 0, [thm]) |
385 else raise THM ("transfer: not a super theory", 0, [thm]) |
368 end; |
386 end; |
369 |
|
370 val transfer = transfer_sg o Theory.sign_of; |
|
371 |
387 |
372 (*maps object-rule to tpairs*) |
388 (*maps object-rule to tpairs*) |
373 fun tpairs_of (Thm {tpairs, ...}) = tpairs; |
389 fun tpairs_of (Thm {tpairs, ...}) = tpairs; |
374 |
390 |
375 (*maps object-rule to premises*) |
391 (*maps object-rule to premises*) |
922 local |
932 local |
923 |
933 |
924 (*Check that all the terms are Vars and are distinct*) |
934 (*Check that all the terms are Vars and are distinct*) |
925 fun instl_ok ts = forall is_Var ts andalso null(findrep ts); |
935 fun instl_ok ts = forall is_Var ts andalso null(findrep ts); |
926 |
936 |
927 fun prt_typing sg_ref t T = |
937 fun pretty_typing thy t T = |
928 let val sg = Sign.deref sg_ref in |
938 Pretty.block [Sign.pretty_term thy t, Pretty.str " ::", Pretty.brk 1, Sign.pretty_typ thy T]; |
929 Pretty.block [Sign.pretty_term sg t, Pretty.str " ::", Pretty.brk 1, Sign.pretty_typ sg T] |
|
930 end; |
|
931 |
|
932 fun prt_type sg_ref T = Sign.pretty_typ (Sign.deref sg_ref) T; |
|
933 |
939 |
934 (*For instantiate: process pair of cterms, merge theories*) |
940 (*For instantiate: process pair of cterms, merge theories*) |
935 fun add_ctpair ((ct,cu), (sign_ref,tpairs)) = |
941 fun add_ctpair ((ct,cu), (thy_ref,tpairs)) = |
936 let |
942 let |
937 val Cterm {sign_ref=sign_reft, t=t, T= T, ...} = ct |
943 val Cterm {thy_ref=thy_reft, t=t, T= T, ...} = ct |
938 and Cterm {sign_ref=sign_refu, t=u, T= U, ...} = cu; |
944 and Cterm {thy_ref=thy_refu, t=u, T= U, ...} = cu; |
939 val sign_ref_merged = Sign.merge_refs (sign_ref, Sign.merge_refs (sign_reft, sign_refu)); |
945 val thy_ref_merged = Theory.merge_refs (thy_ref, Theory.merge_refs (thy_reft, thy_refu)); |
|
946 val thy_merged = Theory.deref thy_ref_merged; |
940 in |
947 in |
941 if T=U then (sign_ref_merged, (t,u)::tpairs) |
948 if T=U then (thy_ref_merged, (t,u)::tpairs) |
942 else raise TYPE (Pretty.string_of (Pretty.block [Pretty.str "instantiate: type conflict", |
949 else raise TYPE (Pretty.string_of (Pretty.block [Pretty.str "instantiate: type conflict", |
943 Pretty.fbrk, prt_typing sign_ref_merged t T, |
950 Pretty.fbrk, pretty_typing thy_merged t T, |
944 Pretty.fbrk, prt_typing sign_ref_merged u U]), [T,U], [t,u]) |
951 Pretty.fbrk, pretty_typing thy_merged u U]), [T,U], [t,u]) |
945 end; |
952 end; |
946 |
953 |
947 fun add_ctyp ((Ctyp {T = T as TVar (_, S), sign_ref = sign_refT}, |
954 fun add_ctyp ((Ctyp {T = T as TVar (_, S), thy_ref = thy_refT}, |
948 Ctyp {T = U, sign_ref = sign_refU}), (sign_ref, vTs)) = |
955 Ctyp {T = U, thy_ref = thy_refU}), (thy_ref, vTs)) = |
949 let |
956 let |
950 val sign_ref_merged = Sign.merge_refs |
957 val thy_ref_merged = Theory.merge_refs |
951 (sign_ref, Sign.merge_refs (sign_refT, sign_refU)); |
958 (thy_ref, Theory.merge_refs (thy_refT, thy_refU)); |
952 val sign = Sign.deref sign_ref_merged |
959 val thy_merged = Theory.deref thy_ref_merged |
953 in |
960 in |
954 if Type.of_sort (Sign.tsig_of sign) (U, S) then |
961 if Type.of_sort (Sign.tsig_of thy_merged) (U, S) then |
955 (sign_ref_merged, (T, U) :: vTs) |
962 (thy_ref_merged, (T, U) :: vTs) |
956 else raise TYPE ("Type not of sort " ^ |
963 else raise TYPE ("Type not of sort " ^ |
957 Sign.string_of_sort sign S, [U], []) |
964 Sign.string_of_sort thy_merged S, [U], []) |
958 end |
965 end |
959 | add_ctyp ((Ctyp {T, sign_ref}, _), _) = |
966 | add_ctyp ((Ctyp {T, thy_ref}, _), _) = |
960 raise TYPE (Pretty.string_of (Pretty.block |
967 raise TYPE (Pretty.string_of (Pretty.block |
961 [Pretty.str "instantiate: not a type variable", |
968 [Pretty.str "instantiate: not a type variable", |
962 Pretty.fbrk, prt_type sign_ref T]), [T], []); |
969 Pretty.fbrk, Sign.pretty_typ (Theory.deref thy_ref) T]), [T], []); |
963 |
970 |
964 in |
971 in |
965 |
972 |
966 (*Left-to-right replacements: ctpairs = [...,(vi,ti),...]. |
973 (*Left-to-right replacements: ctpairs = [...,(vi,ti),...]. |
967 Instantiates distinct Vars by terms of same type. |
974 Instantiates distinct Vars by terms of same type. |
968 No longer normalizes the new theorem! *) |
975 No longer normalizes the new theorem! *) |
969 fun instantiate ([], []) th = th |
976 fun instantiate ([], []) th = th |
970 | instantiate (vcTs,ctpairs) (th as Thm{sign_ref,der,maxidx,hyps,shyps,tpairs=dpairs,prop}) = |
977 | instantiate (vcTs,ctpairs) (th as Thm{thy_ref,der,maxidx,hyps,shyps,tpairs=dpairs,prop}) = |
971 let val (newsign_ref,tpairs) = foldr add_ctpair (sign_ref,[]) ctpairs; |
978 let val (newthy_ref,tpairs) = foldr add_ctpair (thy_ref,[]) ctpairs; |
972 val (newsign_ref,vTs) = foldr add_ctyp (newsign_ref,[]) vcTs; |
979 val (newthy_ref,vTs) = foldr add_ctyp (newthy_ref,[]) vcTs; |
973 fun subst t = |
980 fun subst t = |
974 subst_atomic tpairs (map_term_types (typ_subst_atomic vTs) t); |
981 subst_atomic tpairs (map_term_types (typ_subst_atomic vTs) t); |
975 val newprop = subst prop; |
982 val newprop = subst prop; |
976 val newdpairs = map (pairself subst) dpairs; |
983 val newdpairs = map (pairself subst) dpairs; |
977 val newth = |
984 val newth = |
978 (Thm{sign_ref = newsign_ref, |
985 (Thm{thy_ref = newthy_ref, |
979 der = Pt.infer_derivs' (Pt.instantiate vTs tpairs) der, |
986 der = Pt.infer_derivs' (Pt.instantiate vTs tpairs) der, |
980 maxidx = maxidx_of_terms (newprop :: |
987 maxidx = maxidx_of_terms (newprop :: |
981 terms_of_tpairs newdpairs), |
988 terms_of_tpairs newdpairs), |
982 shyps = add_insts_sorts ((vTs, tpairs), shyps), |
989 shyps = add_insts_sorts ((vTs, tpairs), shyps), |
983 hyps = hyps, |
990 hyps = hyps, |
984 tpairs = newdpairs, |
991 tpairs = newdpairs, |
985 prop = newprop}) |
992 prop = newprop}) |
986 in if not(instl_ok(map #1 tpairs)) |
993 in if not(instl_ok(map #1 tpairs)) |
987 then raise THM("instantiate: variables not distinct", 0, [th]) |
994 then raise THM("instantiate: variables not distinct", 0, [th]) |
988 else if not(null(findrep(map #1 vTs))) |
995 else if not(null(findrep(map #1 vTs))) |
989 then raise THM("instantiate: type variables not distinct", 0, [th]) |
996 then raise THM("instantiate: type variables not distinct", 0, [th]) |
990 else newth |
997 else newth |
991 end |
998 end |
992 handle TERM _ => raise THM("instantiate: incompatible signatures", 0, [th]) |
999 handle TERM _ => raise THM("instantiate: incompatible theories", 0, [th]) |
993 | TYPE (msg, _, _) => raise THM (msg, 0, [th]); |
1000 | TYPE (msg, _, _) => raise THM (msg, 0, [th]); |
994 |
1001 |
995 end; |
1002 end; |
996 |
1003 |
997 |
1004 |
998 (*The trivial implication A==>A, justified by assume and forall rules. |
1005 (*The trivial implication A==>A, justified by assume and forall rules. |
999 A can contain Vars, not so for assume! *) |
1006 A can contain Vars, not so for assume! *) |
1000 fun trivial ct : thm = |
1007 fun trivial ct : thm = |
1001 let val Cterm {sign_ref, t=A, T, maxidx} = ct |
1008 let val Cterm {thy_ref, t=A, T, maxidx} = ct |
1002 in if T<>propT then |
1009 in if T<>propT then |
1003 raise THM("trivial: the term must have type prop", 0, []) |
1010 raise THM("trivial: the term must have type prop", 0, []) |
1004 else fix_shyps [] [] |
1011 else fix_shyps [] [] |
1005 (Thm{sign_ref = sign_ref, |
1012 (Thm{thy_ref = thy_ref, |
1006 der = Pt.infer_derivs' I (false, Pt.AbsP ("H", NONE, Pt.PBound 0)), |
1013 der = Pt.infer_derivs' I (false, Pt.AbsP ("H", NONE, Pt.PBound 0)), |
1007 maxidx = maxidx, |
1014 maxidx = maxidx, |
1008 shyps = [], |
1015 shyps = [], |
1009 hyps = [], |
1016 hyps = [], |
1010 tpairs = [], |
1017 tpairs = [], |
1011 prop = implies$A$A}) |
1018 prop = implies$A$A}) |
1012 end; |
1019 end; |
1013 |
1020 |
1014 (*Axiom-scheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" *) |
1021 (*Axiom-scheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" *) |
1015 fun class_triv sign c = |
1022 fun class_triv thy c = |
1016 let val Cterm {sign_ref, t, maxidx, ...} = |
1023 let val Cterm {thy_ref, t, maxidx, ...} = |
1017 cterm_of sign (Logic.mk_inclass (TVar (("'a", 0), [c]), c)) |
1024 cterm_of thy (Logic.mk_inclass (TVar (("'a", 0), [c]), c)) |
1018 handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []); |
1025 handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []); |
1019 in |
1026 in |
1020 fix_shyps [] [] |
1027 fix_shyps [] [] |
1021 (Thm {sign_ref = sign_ref, |
1028 (Thm {thy_ref = thy_ref, |
1022 der = Pt.infer_derivs' I |
1029 der = Pt.infer_derivs' I |
1023 (false, Pt.PAxm ("ProtoPure.class_triv:" ^ c, t, SOME [])), |
1030 (false, Pt.PAxm ("ProtoPure.class_triv:" ^ c, t, SOME [])), |
1024 maxidx = maxidx, |
1031 maxidx = maxidx, |
1025 shyps = [], |
1032 shyps = [], |
1026 hyps = [], |
1033 hyps = [], |
1027 tpairs = [], |
1034 tpairs = [], |
1028 prop = t}) |
1035 prop = t}) |
1029 end; |
1036 end; |
1030 |
1037 |
1031 |
1038 |
1032 (* Replace all TFrees not fixed or in the hyps by new TVars *) |
1039 (* Replace all TFrees not fixed or in the hyps by new TVars *) |
1033 fun varifyT' fixed (Thm{sign_ref,der,maxidx,shyps,hyps,tpairs,prop}) = |
1040 fun varifyT' fixed (Thm{thy_ref,der,maxidx,shyps,hyps,tpairs,prop}) = |
1034 let |
1041 let |
1035 val tfrees = foldr add_term_tfrees fixed hyps; |
1042 val tfrees = foldr add_term_tfrees fixed hyps; |
1036 val prop1 = attach_tpairs tpairs prop; |
1043 val prop1 = attach_tpairs tpairs prop; |
1037 val (prop2, al) = Type.varify (prop1, tfrees); |
1044 val (prop2, al) = Type.varify (prop1, tfrees); |
1038 val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2) |
1045 val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2) |
1039 in (*no fix_shyps*) |
1046 in (*no fix_shyps*) |
1040 (Thm{sign_ref = sign_ref, |
1047 (Thm{thy_ref = thy_ref, |
1041 der = Pt.infer_derivs' (Pt.varify_proof prop tfrees) der, |
1048 der = Pt.infer_derivs' (Pt.varify_proof prop tfrees) der, |
1042 maxidx = Int.max(0,maxidx), |
1049 maxidx = Int.max(0,maxidx), |
1043 shyps = shyps, |
1050 shyps = shyps, |
1044 hyps = hyps, |
1051 hyps = hyps, |
1045 tpairs = rev (map Logic.dest_equals ts), |
1052 tpairs = rev (map Logic.dest_equals ts), |
1046 prop = prop3}, al) |
1053 prop = prop3}, al) |
1047 end; |
1054 end; |
1048 |
1055 |
1049 val varifyT = #1 o varifyT' []; |
1056 val varifyT = #1 o varifyT' []; |
1050 |
1057 |
1051 (* Replace all TVars by new TFrees *) |
1058 (* Replace all TVars by new TFrees *) |
1052 fun freezeT(Thm{sign_ref,der,maxidx,shyps,hyps,tpairs,prop}) = |
1059 fun freezeT(Thm{thy_ref,der,maxidx,shyps,hyps,tpairs,prop}) = |
1053 let |
1060 let |
1054 val prop1 = attach_tpairs tpairs prop; |
1061 val prop1 = attach_tpairs tpairs prop; |
1055 val prop2 = Type.freeze prop1; |
1062 val prop2 = Type.freeze prop1; |
1056 val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2) |
1063 val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2) |
1057 in (*no fix_shyps*) |
1064 in (*no fix_shyps*) |
1058 Thm{sign_ref = sign_ref, |
1065 Thm{thy_ref = thy_ref, |
1059 der = Pt.infer_derivs' (Pt.freezeT prop1) der, |
1066 der = Pt.infer_derivs' (Pt.freezeT prop1) der, |
1060 maxidx = maxidx_of_term prop2, |
1067 maxidx = maxidx_of_term prop2, |
1061 shyps = shyps, |
1068 shyps = shyps, |
1062 hyps = hyps, |
1069 hyps = hyps, |
1063 tpairs = rev (map Logic.dest_equals ts), |
1070 tpairs = rev (map Logic.dest_equals ts), |
1075 handle TERM _ => raise THM("dest_state", i, [state]); |
1082 handle TERM _ => raise THM("dest_state", i, [state]); |
1076 |
1083 |
1077 (*Increment variables and parameters of orule as required for |
1084 (*Increment variables and parameters of orule as required for |
1078 resolution with goal i of state. *) |
1085 resolution with goal i of state. *) |
1079 fun lift_rule (state, i) orule = |
1086 fun lift_rule (state, i) orule = |
1080 let val Thm{shyps=sshyps, prop=sprop, maxidx=smax, sign_ref=ssign_ref,...} = state |
1087 let val Thm{shyps=sshyps, prop=sprop, maxidx=smax, thy_ref=sthy_ref,...} = state |
1081 val (Bi::_, _) = Logic.strip_prems(i, [], sprop) |
1088 val (Bi::_, _) = Logic.strip_prems(i, [], sprop) |
1082 handle TERM _ => raise THM("lift_rule", i, [orule,state]) |
1089 handle TERM _ => raise THM("lift_rule", i, [orule,state]) |
1083 val ct_Bi = Cterm {sign_ref=ssign_ref, maxidx=smax, T=propT, t=Bi} |
1090 val ct_Bi = Cterm {thy_ref=sthy_ref, maxidx=smax, T=propT, t=Bi} |
1084 val (lift_abs,lift_all) = Logic.lift_fns(Bi,smax+1) |
1091 val (lift_abs,lift_all) = Logic.lift_fns(Bi,smax+1) |
1085 val (Thm{sign_ref, der, maxidx,shyps,hyps,tpairs,prop}) = orule |
1092 val (Thm{thy_ref, der, maxidx,shyps,hyps,tpairs,prop}) = orule |
1086 val (As, B) = Logic.strip_horn prop |
1093 val (As, B) = Logic.strip_horn prop |
1087 in (*no fix_shyps*) |
1094 in (*no fix_shyps*) |
1088 Thm{sign_ref = merge_thm_sgs(state,orule), |
1095 Thm{thy_ref = merge_thm_thys(state,orule), |
1089 der = Pt.infer_derivs' (Pt.lift_proof Bi (smax+1) prop) der, |
1096 der = Pt.infer_derivs' (Pt.lift_proof Bi (smax+1) prop) der, |
1090 maxidx = maxidx+smax+1, |
1097 maxidx = maxidx+smax+1, |
1091 shyps = Sorts.union_sort(sshyps,shyps), |
1098 shyps = Sorts.union_sort(sshyps,shyps), |
1092 hyps = hyps, |
1099 hyps = hyps, |
1093 tpairs = map (pairself lift_abs) tpairs, |
1100 tpairs = map (pairself lift_abs) tpairs, |
1094 prop = Logic.list_implies (map lift_all As, lift_all B)} |
1101 prop = Logic.list_implies (map lift_all As, lift_all B)} |
1095 end; |
1102 end; |
1096 |
1103 |
1097 fun incr_indexes i (thm as Thm {sign_ref, der, maxidx, shyps, hyps, tpairs, prop}) = |
1104 fun incr_indexes i (thm as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) = |
1098 if i < 0 then raise THM ("negative increment", 0, [thm]) else |
1105 if i < 0 then raise THM ("negative increment", 0, [thm]) else |
1099 if i = 0 then thm else |
1106 if i = 0 then thm else |
1100 Thm {sign_ref = sign_ref, |
1107 Thm {thy_ref = thy_ref, |
1101 der = Pt.infer_derivs' (Pt.map_proof_terms |
1108 der = Pt.infer_derivs' (Pt.map_proof_terms |
1102 (Logic.incr_indexes ([], i)) (incr_tvar i)) der, |
1109 (Logic.incr_indexes ([], i)) (incr_tvar i)) der, |
1103 maxidx = maxidx + i, |
1110 maxidx = maxidx + i, |
1104 shyps = shyps, |
1111 shyps = shyps, |
1105 hyps = hyps, |
1112 hyps = hyps, |
1106 tpairs = map (pairself (Logic.incr_indexes ([], i))) tpairs, |
1113 tpairs = map (pairself (Logic.incr_indexes ([], i))) tpairs, |
1107 prop = Logic.incr_indexes ([], i) prop}; |
1114 prop = Logic.incr_indexes ([], i) prop}; |
1108 |
1115 |
1109 (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *) |
1116 (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *) |
1110 fun assumption i state = |
1117 fun assumption i state = |
1111 let val Thm{sign_ref,der,maxidx,hyps,prop,...} = state; |
1118 let val Thm{thy_ref,der,maxidx,hyps,prop,...} = state; |
1112 val (tpairs, Bs, Bi, C) = dest_state(state,i) |
1119 val (tpairs, Bs, Bi, C) = dest_state(state,i) |
1113 fun newth n (env as Envir.Envir{maxidx, ...}, tpairs) = |
1120 fun newth n (env as Envir.Envir{maxidx, ...}, tpairs) = |
1114 fix_shyps [state] (env_codT env) |
1121 fix_shyps [state] (env_codT env) |
1115 (Thm{sign_ref = sign_ref, |
1122 (Thm{thy_ref = thy_ref, |
1116 der = Pt.infer_derivs' |
1123 der = Pt.infer_derivs' |
1117 ((if Envir.is_empty env then I else (Pt.norm_proof' env)) o |
1124 ((if Envir.is_empty env then I else (Pt.norm_proof' env)) o |
1118 Pt.assumption_proof Bs Bi n) der, |
1125 Pt.assumption_proof Bs Bi n) der, |
1119 maxidx = maxidx, |
1126 maxidx = maxidx, |
1120 shyps = [], |
1127 shyps = [], |
1121 hyps = hyps, |
1128 hyps = hyps, |
1122 tpairs = if Envir.is_empty env then tpairs else |
1129 tpairs = if Envir.is_empty env then tpairs else |
1123 map (pairself (Envir.norm_term env)) tpairs, |
1130 map (pairself (Envir.norm_term env)) tpairs, |
1124 prop = |
1131 prop = |
1125 if Envir.is_empty env then (*avoid wasted normalizations*) |
1132 if Envir.is_empty env then (*avoid wasted normalizations*) |
1126 Logic.list_implies (Bs, C) |
1133 Logic.list_implies (Bs, C) |
1127 else (*normalize the new rule fully*) |
1134 else (*normalize the new rule fully*) |
1128 Envir.norm_term env (Logic.list_implies (Bs, C))}); |
1135 Envir.norm_term env (Logic.list_implies (Bs, C))}); |
1129 fun addprfs [] _ = Seq.empty |
1136 fun addprfs [] _ = Seq.empty |
1130 | addprfs ((t,u)::apairs) n = Seq.make (fn()=> Seq.pull |
1137 | addprfs ((t,u)::apairs) n = Seq.make (fn()=> Seq.pull |
1131 (Seq.mapp (newth n) |
1138 (Seq.mapp (newth n) |
1132 (Unify.unifiers(Sign.deref sign_ref,Envir.empty maxidx, (t,u)::tpairs)) |
1139 (Unify.unifiers(Theory.deref thy_ref,Envir.empty maxidx, (t,u)::tpairs)) |
1133 (addprfs apairs (n+1)))) |
1140 (addprfs apairs (n+1)))) |
1134 in addprfs (Logic.assum_pairs (~1,Bi)) 1 end; |
1141 in addprfs (Logic.assum_pairs (~1,Bi)) 1 end; |
1135 |
1142 |
1136 (*Solve subgoal Bi of proof state B1...Bn/C by assumption. |
1143 (*Solve subgoal Bi of proof state B1...Bn/C by assumption. |
1137 Checks if Bi's conclusion is alpha-convertible to one of its assumptions*) |
1144 Checks if Bi's conclusion is alpha-convertible to one of its assumptions*) |
1138 fun eq_assumption i state = |
1145 fun eq_assumption i state = |
1139 let val Thm{sign_ref,der,maxidx,hyps,prop,...} = state; |
1146 let val Thm{thy_ref,der,maxidx,hyps,prop,...} = state; |
1140 val (tpairs, Bs, Bi, C) = dest_state(state,i) |
1147 val (tpairs, Bs, Bi, C) = dest_state(state,i) |
1141 in (case find_index (op aconv) (Logic.assum_pairs (~1,Bi)) of |
1148 in (case find_index (op aconv) (Logic.assum_pairs (~1,Bi)) of |
1142 (~1) => raise THM("eq_assumption", 0, [state]) |
1149 (~1) => raise THM("eq_assumption", 0, [state]) |
1143 | n => fix_shyps [state] [] |
1150 | n => fix_shyps [state] [] |
1144 (Thm{sign_ref = sign_ref, |
1151 (Thm{thy_ref = thy_ref, |
1145 der = Pt.infer_derivs' |
1152 der = Pt.infer_derivs' |
1146 (Pt.assumption_proof Bs Bi (n+1)) der, |
1153 (Pt.assumption_proof Bs Bi (n+1)) der, |
1147 maxidx = maxidx, |
1154 maxidx = maxidx, |
1148 shyps = [], |
1155 shyps = [], |
1149 hyps = hyps, |
1156 hyps = hyps, |
1152 end; |
1159 end; |
1153 |
1160 |
1154 |
1161 |
1155 (*For rotate_tac: fast rotation of assumptions of subgoal i*) |
1162 (*For rotate_tac: fast rotation of assumptions of subgoal i*) |
1156 fun rotate_rule k i state = |
1163 fun rotate_rule k i state = |
1157 let val Thm{sign_ref,der,maxidx,hyps,prop,shyps,...} = state; |
1164 let val Thm{thy_ref,der,maxidx,hyps,prop,shyps,...} = state; |
1158 val (tpairs, Bs, Bi, C) = dest_state(state,i) |
1165 val (tpairs, Bs, Bi, C) = dest_state(state,i) |
1159 val params = Term.strip_all_vars Bi |
1166 val params = Term.strip_all_vars Bi |
1160 and rest = Term.strip_all_body Bi |
1167 and rest = Term.strip_all_body Bi |
1161 val asms = Logic.strip_imp_prems rest |
1168 val asms = Logic.strip_imp_prems rest |
1162 and concl = Logic.strip_imp_concl rest |
1169 and concl = Logic.strip_imp_concl rest |
1163 val n = length asms |
1170 val n = length asms |
1164 val m = if k<0 then n+k else k |
1171 val m = if k<0 then n+k else k |
1165 val Bi' = if 0=m orelse m=n then Bi |
1172 val Bi' = if 0=m orelse m=n then Bi |
1166 else if 0<m andalso m<n |
1173 else if 0<m andalso m<n |
1167 then let val (ps,qs) = splitAt(m,asms) |
1174 then let val (ps,qs) = splitAt(m,asms) |
1168 in list_all(params, Logic.list_implies(qs @ ps, concl)) |
1175 in list_all(params, Logic.list_implies(qs @ ps, concl)) |
1169 end |
1176 end |
1170 else raise THM("rotate_rule", k, [state]) |
1177 else raise THM("rotate_rule", k, [state]) |
1171 in (*no fix_shyps*) |
1178 in (*no fix_shyps*) |
1172 Thm{sign_ref = sign_ref, |
1179 Thm{thy_ref = thy_ref, |
1173 der = Pt.infer_derivs' (Pt.rotate_proof Bs Bi m) der, |
1180 der = Pt.infer_derivs' (Pt.rotate_proof Bs Bi m) der, |
1174 maxidx = maxidx, |
1181 maxidx = maxidx, |
1175 shyps = shyps, |
1182 shyps = shyps, |
1176 hyps = hyps, |
1183 hyps = hyps, |
1177 tpairs = tpairs, |
1184 tpairs = tpairs, |
1178 prop = Logic.list_implies (Bs @ [Bi'], C)} |
1185 prop = Logic.list_implies (Bs @ [Bi'], C)} |
1179 end; |
1186 end; |
1180 |
1187 |
1181 |
1188 |
1182 (*Rotates a rule's premises to the left by k, leaving the first j premises |
1189 (*Rotates a rule's premises to the left by k, leaving the first j premises |
1183 unchanged. Does nothing if k=0 or if k equals n-j, where n is the |
1190 unchanged. Does nothing if k=0 or if k equals n-j, where n is the |
1184 number of premises. Useful with etac and underlies tactic/defer_tac*) |
1191 number of premises. Useful with etac and underlies tactic/defer_tac*) |
1185 fun permute_prems j k rl = |
1192 fun permute_prems j k rl = |
1186 let val Thm{sign_ref,der,maxidx,hyps,tpairs,prop,shyps} = rl |
1193 let val Thm{thy_ref,der,maxidx,hyps,tpairs,prop,shyps} = rl |
1187 val prems = Logic.strip_imp_prems prop |
1194 val prems = Logic.strip_imp_prems prop |
1188 and concl = Logic.strip_imp_concl prop |
1195 and concl = Logic.strip_imp_concl prop |
1189 val moved_prems = List.drop(prems, j) |
1196 val moved_prems = List.drop(prems, j) |
1190 and fixed_prems = List.take(prems, j) |
1197 and fixed_prems = List.take(prems, j) |
1191 handle Subscript => raise THM("permute_prems:j", j, [rl]) |
1198 handle Subscript => raise THM("permute_prems:j", j, [rl]) |
1192 val n_j = length moved_prems |
1199 val n_j = length moved_prems |
1193 val m = if k<0 then n_j + k else k |
1200 val m = if k<0 then n_j + k else k |
1194 val prop' = if 0 = m orelse m = n_j then prop |
1201 val prop' = if 0 = m orelse m = n_j then prop |
1195 else if 0<m andalso m<n_j |
1202 else if 0<m andalso m<n_j |
1196 then let val (ps,qs) = splitAt(m,moved_prems) |
1203 then let val (ps,qs) = splitAt(m,moved_prems) |
1197 in Logic.list_implies(fixed_prems @ qs @ ps, concl) end |
1204 in Logic.list_implies(fixed_prems @ qs @ ps, concl) end |
1198 else raise THM("permute_prems:k", k, [rl]) |
1205 else raise THM("permute_prems:k", k, [rl]) |
1199 in (*no fix_shyps*) |
1206 in (*no fix_shyps*) |
1200 Thm{sign_ref = sign_ref, |
1207 Thm{thy_ref = thy_ref, |
1201 der = Pt.infer_derivs' (Pt.permute_prems_prf prems j m) der, |
1208 der = Pt.infer_derivs' (Pt.permute_prems_prf prems j m) der, |
1202 maxidx = maxidx, |
1209 maxidx = maxidx, |
1203 shyps = shyps, |
1210 shyps = shyps, |
1204 hyps = hyps, |
1211 hyps = hyps, |
1205 tpairs = tpairs, |
1212 tpairs = tpairs, |
1206 prop = prop'} |
1213 prop = prop'} |
1207 end; |
1214 end; |
1208 |
1215 |
1209 |
1216 |
1210 (** User renaming of parameters in a subgoal **) |
1217 (** User renaming of parameters in a subgoal **) |
1211 |
1218 |
1212 (*Calls error rather than raising an exception because it is intended |
1219 (*Calls error rather than raising an exception because it is intended |
1213 for top-level use -- exception handling would not make sense here. |
1220 for top-level use -- exception handling would not make sense here. |
1214 The names in cs, if distinct, are used for the innermost parameters; |
1221 The names in cs, if distinct, are used for the innermost parameters; |
1215 preceding parameters may be renamed to make all params distinct.*) |
1222 preceding parameters may be renamed to make all params distinct.*) |
1216 fun rename_params_rule (cs, i) state = |
1223 fun rename_params_rule (cs, i) state = |
1217 let val Thm{sign_ref,der,maxidx,hyps,shyps,...} = state |
1224 let val Thm{thy_ref,der,maxidx,hyps,shyps,...} = state |
1218 val (tpairs, Bs, Bi, C) = dest_state(state,i) |
1225 val (tpairs, Bs, Bi, C) = dest_state(state,i) |
1219 val iparams = map #1 (Logic.strip_params Bi) |
1226 val iparams = map #1 (Logic.strip_params Bi) |
1220 val short = length iparams - length cs |
1227 val short = length iparams - length cs |
1221 val newnames = |
1228 val newnames = |
1222 if short<0 then error"More names than abstractions!" |
1229 if short<0 then error"More names than abstractions!" |
1223 else variantlist(Library.take (short,iparams), cs) @ cs |
1230 else variantlist(Library.take (short,iparams), cs) @ cs |
1224 val freenames = map (#1 o dest_Free) (term_frees Bi) |
1231 val freenames = map (#1 o dest_Free) (term_frees Bi) |
1225 val newBi = Logic.list_rename_params (newnames, Bi) |
1232 val newBi = Logic.list_rename_params (newnames, Bi) |
1226 in |
1233 in |
1227 case findrep cs of |
1234 case findrep cs of |
1228 c::_ => (warning ("Can't rename. Bound variables not distinct: " ^ c); |
1235 c::_ => (warning ("Can't rename. Bound variables not distinct: " ^ c); |
1229 state) |
1236 state) |
1230 | [] => (case cs inter_string freenames of |
1237 | [] => (case cs inter_string freenames of |
1231 a::_ => (warning ("Can't rename. Bound/Free variable clash: " ^ a); |
1238 a::_ => (warning ("Can't rename. Bound/Free variable clash: " ^ a); |
1232 state) |
1239 state) |
1233 | [] => Thm{sign_ref = sign_ref, |
1240 | [] => Thm{thy_ref = thy_ref, |
1234 der = der, |
1241 der = der, |
1235 maxidx = maxidx, |
1242 maxidx = maxidx, |
1236 shyps = shyps, |
1243 shyps = shyps, |
1237 hyps = hyps, |
1244 hyps = hyps, |
1238 tpairs = tpairs, |
1245 tpairs = tpairs, |