wenzelm@22362
|
1 |
(* Title: Pure/more_thm.ML
|
wenzelm@22362
|
2 |
Author: Makarius
|
wenzelm@22362
|
3 |
|
wenzelm@22907
|
4 |
Further operations on type ctyp/cterm/thm, outside the inference kernel.
|
wenzelm@22362
|
5 |
*)
|
wenzelm@22362
|
6 |
|
wenzelm@23169
|
7 |
infix aconvc;
|
wenzelm@23169
|
8 |
|
wenzelm@32846
|
9 |
signature BASIC_THM =
|
wenzelm@32846
|
10 |
sig
|
wenzelm@32846
|
11 |
include BASIC_THM
|
wenzelm@32846
|
12 |
structure Ctermtab: TABLE
|
wenzelm@32846
|
13 |
structure Thmtab: TABLE
|
wenzelm@32846
|
14 |
val aconvc: cterm * cterm -> bool
|
wenzelm@46246
|
15 |
type attribute = Context.generic * thm -> Context.generic option * thm option
|
wenzelm@32846
|
16 |
end;
|
wenzelm@32846
|
17 |
|
wenzelm@22362
|
18 |
signature THM =
|
wenzelm@22362
|
19 |
sig
|
wenzelm@22362
|
20 |
include THM
|
wenzelm@32846
|
21 |
structure Ctermtab: TABLE
|
wenzelm@32846
|
22 |
structure Thmtab: TABLE
|
wenzelm@24948
|
23 |
val aconvc: cterm * cterm -> bool
|
wenzelm@23491
|
24 |
val add_cterm_frees: cterm -> cterm list -> cterm list
|
wenzelm@32204
|
25 |
val all_name: string * cterm -> cterm -> cterm
|
wenzelm@32204
|
26 |
val all: cterm -> cterm -> cterm
|
wenzelm@22907
|
27 |
val mk_binop: cterm -> cterm -> cterm -> cterm
|
wenzelm@22907
|
28 |
val dest_binop: cterm -> cterm * cterm
|
wenzelm@22907
|
29 |
val dest_implies: cterm -> cterm * cterm
|
wenzelm@22907
|
30 |
val dest_equals: cterm -> cterm * cterm
|
wenzelm@22907
|
31 |
val dest_equals_lhs: cterm -> cterm
|
wenzelm@22907
|
32 |
val dest_equals_rhs: cterm -> cterm
|
wenzelm@22907
|
33 |
val lhs_of: thm -> cterm
|
wenzelm@22907
|
34 |
val rhs_of: thm -> cterm
|
wenzelm@22362
|
35 |
val thm_ord: thm * thm -> order
|
wenzelm@32846
|
36 |
val cterm_cache: (cterm -> 'a) -> cterm -> 'a
|
wenzelm@32846
|
37 |
val thm_cache: (thm -> 'a) -> thm -> 'a
|
wenzelm@23599
|
38 |
val is_reflexive: thm -> bool
|
wenzelm@22362
|
39 |
val eq_thm: thm * thm -> bool
|
wenzelm@22362
|
40 |
val eq_thm_thy: thm * thm -> bool
|
wenzelm@22362
|
41 |
val eq_thm_prop: thm * thm -> bool
|
wenzelm@22362
|
42 |
val equiv_thm: thm * thm -> bool
|
wenzelm@31944
|
43 |
val class_triv: theory -> class -> thm
|
wenzelm@31944
|
44 |
val of_sort: ctyp * sort -> thm list
|
wenzelm@28621
|
45 |
val check_shyps: sort list -> thm -> thm
|
wenzelm@24048
|
46 |
val is_dummy: thm -> bool
|
wenzelm@22695
|
47 |
val plain_prop_of: thm -> term
|
wenzelm@24048
|
48 |
val add_thm: thm -> thm list -> thm list
|
wenzelm@24048
|
49 |
val del_thm: thm -> thm list -> thm list
|
wenzelm@24048
|
50 |
val merge_thms: thm list * thm list -> thm list
|
wenzelm@33459
|
51 |
val full_rules: thm Item_Net.T
|
wenzelm@30562
|
52 |
val intro_rules: thm Item_Net.T
|
wenzelm@30562
|
53 |
val elim_rules: thm Item_Net.T
|
wenzelm@27866
|
54 |
val elim_implies: thm -> thm -> thm
|
wenzelm@27866
|
55 |
val forall_elim_var: int -> thm -> thm
|
wenzelm@27866
|
56 |
val forall_elim_vars: int -> thm -> thm
|
wenzelm@32282
|
57 |
val certify_inst: theory ->
|
wenzelm@32282
|
58 |
((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
|
wenzelm@32282
|
59 |
(ctyp * ctyp) list * (cterm * cterm) list
|
wenzelm@32282
|
60 |
val certify_instantiate:
|
wenzelm@32282
|
61 |
((indexname * sort) * typ) list * ((indexname * typ) * term) list -> thm -> thm
|
wenzelm@35986
|
62 |
val forall_intr_frees: thm -> thm
|
wenzelm@35845
|
63 |
val unvarify_global: thm -> thm
|
wenzelm@27866
|
64 |
val close_derivation: thm -> thm
|
wenzelm@43246
|
65 |
val add_axiom: Proof.context -> binding * term -> theory -> (string * thm) * theory
|
wenzelm@43246
|
66 |
val add_axiom_global: binding * term -> theory -> (string * thm) * theory
|
wenzelm@43246
|
67 |
val add_def: Proof.context -> bool -> bool -> binding * term -> theory -> (string * thm) * theory
|
wenzelm@43246
|
68 |
val add_def_global: bool -> bool -> binding * term -> theory -> (string * thm) * theory
|
wenzelm@46246
|
69 |
type attribute = Context.generic * thm -> Context.generic option * thm option
|
wenzelm@30214
|
70 |
type binding = binding * attribute list
|
wenzelm@30214
|
71 |
val empty_binding: binding
|
wenzelm@27866
|
72 |
val rule_attribute: (Context.generic -> thm -> thm) -> attribute
|
wenzelm@27866
|
73 |
val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute
|
wenzelm@46246
|
74 |
val mixed_attribute: (Context.generic * thm -> Context.generic * thm) -> attribute
|
wenzelm@47659
|
75 |
val apply_attribute: attribute -> thm -> Context.generic -> thm * Context.generic
|
wenzelm@46246
|
76 |
val attribute_declaration: attribute -> thm -> Context.generic -> Context.generic
|
wenzelm@47659
|
77 |
val theory_attributes: attribute list -> thm -> theory -> thm * theory
|
wenzelm@47659
|
78 |
val proof_attributes: attribute list -> thm -> Proof.context -> thm * Proof.context
|
wenzelm@27866
|
79 |
val no_attributes: 'a -> 'a * 'b list
|
wenzelm@27866
|
80 |
val simple_fact: 'a -> ('a * 'b list) list
|
wenzelm@47703
|
81 |
val tag_rule: string * string -> thm -> thm
|
wenzelm@27866
|
82 |
val untag_rule: string -> thm -> thm
|
wenzelm@47703
|
83 |
val tag: string * string -> attribute
|
wenzelm@27866
|
84 |
val untag: string -> attribute
|
wenzelm@30348
|
85 |
val def_name: string -> string
|
wenzelm@30348
|
86 |
val def_name_optional: string -> string -> string
|
wenzelm@35238
|
87 |
val def_binding: Binding.binding -> Binding.binding
|
wenzelm@30447
|
88 |
val def_binding_optional: Binding.binding -> Binding.binding -> Binding.binding
|
wenzelm@27866
|
89 |
val has_name_hint: thm -> bool
|
wenzelm@27866
|
90 |
val get_name_hint: thm -> string
|
wenzelm@27866
|
91 |
val put_name_hint: string -> thm -> thm
|
wenzelm@22362
|
92 |
val theoremK: string
|
wenzelm@22362
|
93 |
val lemmaK: string
|
wenzelm@22362
|
94 |
val corollaryK: string
|
wenzelm@43344
|
95 |
val legacy_get_kind: thm -> string
|
wenzelm@27866
|
96 |
val kind_rule: string -> thm -> thm
|
wenzelm@27866
|
97 |
val kind: string -> attribute
|
wenzelm@50077
|
98 |
val register_proofs: thm list -> theory -> theory
|
wenzelm@50026
|
99 |
val join_theory_proofs: theory -> unit
|
wenzelm@22362
|
100 |
end;
|
wenzelm@22362
|
101 |
|
wenzelm@22362
|
102 |
structure Thm: THM =
|
wenzelm@22362
|
103 |
struct
|
wenzelm@22362
|
104 |
|
wenzelm@22695
|
105 |
(** basic operations **)
|
wenzelm@22362
|
106 |
|
wenzelm@23491
|
107 |
(* collecting cterms *)
|
wenzelm@23491
|
108 |
|
wenzelm@23491
|
109 |
val op aconvc = op aconv o pairself Thm.term_of;
|
wenzelm@23491
|
110 |
|
wenzelm@23491
|
111 |
fun add_cterm_frees ct =
|
wenzelm@23491
|
112 |
let
|
wenzelm@23491
|
113 |
val cert = Thm.cterm_of (Thm.theory_of_cterm ct);
|
wenzelm@23491
|
114 |
val t = Thm.term_of ct;
|
wenzelm@23491
|
115 |
in Term.fold_aterms (fn v as Free _ => insert (op aconvc) (cert v) | _ => I) t end;
|
wenzelm@23491
|
116 |
|
wenzelm@23491
|
117 |
|
wenzelm@22907
|
118 |
(* cterm constructors and destructors *)
|
wenzelm@22907
|
119 |
|
wenzelm@32204
|
120 |
fun all_name (x, t) A =
|
wenzelm@32204
|
121 |
let
|
wenzelm@32204
|
122 |
val cert = Thm.cterm_of (Thm.theory_of_cterm t);
|
wenzelm@32204
|
123 |
val T = #T (Thm.rep_cterm t);
|
wenzelm@47368
|
124 |
in Thm.apply (cert (Const ("all", (T --> propT) --> propT))) (Thm.lambda_name (x, t) A) end;
|
wenzelm@32204
|
125 |
|
wenzelm@32204
|
126 |
fun all t A = all_name ("", t) A;
|
wenzelm@32204
|
127 |
|
wenzelm@47368
|
128 |
fun mk_binop c a b = Thm.apply (Thm.apply c a) b;
|
wenzelm@22907
|
129 |
fun dest_binop ct = (Thm.dest_arg1 ct, Thm.dest_arg ct);
|
wenzelm@22907
|
130 |
|
wenzelm@22907
|
131 |
fun dest_implies ct =
|
wenzelm@22907
|
132 |
(case Thm.term_of ct of
|
wenzelm@22907
|
133 |
Const ("==>", _) $ _ $ _ => dest_binop ct
|
wenzelm@22907
|
134 |
| _ => raise TERM ("dest_implies", [Thm.term_of ct]));
|
wenzelm@22907
|
135 |
|
wenzelm@22907
|
136 |
fun dest_equals ct =
|
wenzelm@22907
|
137 |
(case Thm.term_of ct of
|
wenzelm@22907
|
138 |
Const ("==", _) $ _ $ _ => dest_binop ct
|
wenzelm@22907
|
139 |
| _ => raise TERM ("dest_equals", [Thm.term_of ct]));
|
wenzelm@22907
|
140 |
|
wenzelm@22907
|
141 |
fun dest_equals_lhs ct =
|
wenzelm@22907
|
142 |
(case Thm.term_of ct of
|
wenzelm@22907
|
143 |
Const ("==", _) $ _ $ _ => Thm.dest_arg1 ct
|
wenzelm@22907
|
144 |
| _ => raise TERM ("dest_equals_lhs", [Thm.term_of ct]));
|
wenzelm@22907
|
145 |
|
wenzelm@22907
|
146 |
fun dest_equals_rhs ct =
|
wenzelm@22907
|
147 |
(case Thm.term_of ct of
|
wenzelm@22907
|
148 |
Const ("==", _) $ _ $ _ => Thm.dest_arg ct
|
wenzelm@22907
|
149 |
| _ => raise TERM ("dest_equals_rhs", [Thm.term_of ct]));
|
wenzelm@22907
|
150 |
|
wenzelm@22907
|
151 |
val lhs_of = dest_equals_lhs o Thm.cprop_of;
|
wenzelm@22907
|
152 |
val rhs_of = dest_equals_rhs o Thm.cprop_of;
|
wenzelm@22907
|
153 |
|
wenzelm@22907
|
154 |
|
wenzelm@22907
|
155 |
(* thm order: ignores theory context! *)
|
wenzelm@22682
|
156 |
|
wenzelm@22362
|
157 |
fun thm_ord (th1, th2) =
|
wenzelm@22362
|
158 |
let
|
wenzelm@22362
|
159 |
val {shyps = shyps1, hyps = hyps1, tpairs = tpairs1, prop = prop1, ...} = Thm.rep_thm th1;
|
wenzelm@22362
|
160 |
val {shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...} = Thm.rep_thm th2;
|
wenzelm@22362
|
161 |
in
|
wenzelm@35408
|
162 |
(case Term_Ord.fast_term_ord (prop1, prop2) of
|
wenzelm@22362
|
163 |
EQUAL =>
|
wenzelm@35408
|
164 |
(case list_ord (prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord) (tpairs1, tpairs2) of
|
wenzelm@22362
|
165 |
EQUAL =>
|
wenzelm@35408
|
166 |
(case list_ord Term_Ord.fast_term_ord (hyps1, hyps2) of
|
wenzelm@35408
|
167 |
EQUAL => list_ord Term_Ord.sort_ord (shyps1, shyps2)
|
wenzelm@22362
|
168 |
| ord => ord)
|
wenzelm@22362
|
169 |
| ord => ord)
|
wenzelm@22362
|
170 |
| ord => ord)
|
wenzelm@22362
|
171 |
end;
|
wenzelm@22362
|
172 |
|
wenzelm@22682
|
173 |
|
wenzelm@32846
|
174 |
(* tables and caches *)
|
wenzelm@32846
|
175 |
|
wenzelm@35408
|
176 |
structure Ctermtab = Table(type key = cterm val ord = Term_Ord.fast_term_ord o pairself Thm.term_of);
|
wenzelm@32846
|
177 |
structure Thmtab = Table(type key = thm val ord = thm_ord);
|
wenzelm@32846
|
178 |
|
wenzelm@32846
|
179 |
fun cterm_cache f = Cache.create Ctermtab.empty Ctermtab.lookup Ctermtab.update f;
|
wenzelm@32846
|
180 |
fun thm_cache f = Cache.create Thmtab.empty Thmtab.lookup Thmtab.update f;
|
wenzelm@32846
|
181 |
|
wenzelm@32846
|
182 |
|
wenzelm@22682
|
183 |
(* equality *)
|
wenzelm@22682
|
184 |
|
wenzelm@23599
|
185 |
fun is_reflexive th = op aconv (Logic.dest_equals (Thm.prop_of th))
|
wenzelm@23599
|
186 |
handle TERM _ => false;
|
wenzelm@23599
|
187 |
|
wenzelm@22362
|
188 |
fun eq_thm ths =
|
wenzelm@22362
|
189 |
Context.joinable (pairself Thm.theory_of_thm ths) andalso
|
wenzelm@26653
|
190 |
is_equal (thm_ord ths);
|
wenzelm@22362
|
191 |
|
wenzelm@26665
|
192 |
val eq_thm_thy = Theory.eq_thy o pairself Thm.theory_of_thm;
|
wenzelm@22362
|
193 |
val eq_thm_prop = op aconv o pairself Thm.full_prop_of;
|
wenzelm@22362
|
194 |
|
wenzelm@22682
|
195 |
|
wenzelm@22682
|
196 |
(* pattern equivalence *)
|
wenzelm@22682
|
197 |
|
wenzelm@22362
|
198 |
fun equiv_thm ths =
|
wenzelm@22362
|
199 |
Pattern.equiv (Theory.merge (pairself Thm.theory_of_thm ths)) (pairself Thm.full_prop_of ths);
|
wenzelm@22362
|
200 |
|
wenzelm@22362
|
201 |
|
wenzelm@31915
|
202 |
(* type classes and sorts *)
|
wenzelm@31915
|
203 |
|
wenzelm@31944
|
204 |
fun class_triv thy c =
|
wenzelm@31944
|
205 |
Thm.of_class (Thm.ctyp_of thy (TVar ((Name.aT, 0), [c])), c);
|
wenzelm@31944
|
206 |
|
wenzelm@31944
|
207 |
fun of_sort (T, S) = map (fn c => Thm.of_class (T, c)) S;
|
wenzelm@28621
|
208 |
|
wenzelm@28621
|
209 |
fun check_shyps sorts raw_th =
|
wenzelm@28621
|
210 |
let
|
wenzelm@28621
|
211 |
val th = Thm.strip_shyps raw_th;
|
wenzelm@28621
|
212 |
val prt_sort = Syntax.pretty_sort_global (Thm.theory_of_thm th);
|
wenzelm@28621
|
213 |
val pending = Sorts.subtract sorts (Thm.extra_shyps th);
|
wenzelm@28621
|
214 |
in
|
wenzelm@28621
|
215 |
if null pending then th
|
wenzelm@28621
|
216 |
else error (Pretty.string_of (Pretty.block (Pretty.str "Pending sort hypotheses:" ::
|
wenzelm@28621
|
217 |
Pretty.brk 1 :: Pretty.commas (map prt_sort pending))))
|
wenzelm@28621
|
218 |
end;
|
wenzelm@28621
|
219 |
|
wenzelm@28621
|
220 |
|
wenzelm@22695
|
221 |
(* misc operations *)
|
wenzelm@22695
|
222 |
|
wenzelm@24048
|
223 |
fun is_dummy thm =
|
wenzelm@24048
|
224 |
(case try Logic.dest_term (Thm.concl_of thm) of
|
wenzelm@24048
|
225 |
NONE => false
|
wenzelm@24048
|
226 |
| SOME t => Term.is_dummy_pattern t);
|
wenzelm@24048
|
227 |
|
wenzelm@22695
|
228 |
fun plain_prop_of raw_thm =
|
wenzelm@22695
|
229 |
let
|
wenzelm@22695
|
230 |
val thm = Thm.strip_shyps raw_thm;
|
wenzelm@22695
|
231 |
fun err msg = raise THM ("plain_prop_of: " ^ msg, 0, [thm]);
|
wenzelm@22695
|
232 |
val {hyps, prop, tpairs, ...} = Thm.rep_thm thm;
|
wenzelm@22695
|
233 |
in
|
wenzelm@22695
|
234 |
if not (null hyps) then
|
wenzelm@22695
|
235 |
err "theorem may not contain hypotheses"
|
wenzelm@22695
|
236 |
else if not (null (Thm.extra_shyps thm)) then
|
wenzelm@22695
|
237 |
err "theorem may not contain sort hypotheses"
|
wenzelm@22695
|
238 |
else if not (null tpairs) then
|
wenzelm@22695
|
239 |
err "theorem may not contain flex-flex pairs"
|
wenzelm@22695
|
240 |
else prop
|
wenzelm@22695
|
241 |
end;
|
wenzelm@22695
|
242 |
|
wenzelm@22695
|
243 |
|
wenzelm@30564
|
244 |
(* collections of theorems in canonical order *)
|
wenzelm@24048
|
245 |
|
wenzelm@24048
|
246 |
val add_thm = update eq_thm_prop;
|
wenzelm@24048
|
247 |
val del_thm = remove eq_thm_prop;
|
wenzelm@24048
|
248 |
val merge_thms = merge eq_thm_prop;
|
wenzelm@24048
|
249 |
|
wenzelm@33459
|
250 |
val full_rules = Item_Net.init eq_thm_prop (single o Thm.full_prop_of);
|
wenzelm@33373
|
251 |
val intro_rules = Item_Net.init eq_thm_prop (single o Thm.concl_of);
|
wenzelm@33373
|
252 |
val elim_rules = Item_Net.init eq_thm_prop (single o Thm.major_prem_of);
|
wenzelm@30562
|
253 |
|
wenzelm@30562
|
254 |
|
wenzelm@22682
|
255 |
|
wenzelm@24980
|
256 |
(** basic derived rules **)
|
wenzelm@24980
|
257 |
|
wenzelm@24980
|
258 |
(*Elimination of implication
|
wenzelm@24980
|
259 |
A A ==> B
|
wenzelm@24980
|
260 |
------------
|
wenzelm@24980
|
261 |
B
|
wenzelm@24980
|
262 |
*)
|
wenzelm@24980
|
263 |
fun elim_implies thA thAB = Thm.implies_elim thAB thA;
|
wenzelm@24980
|
264 |
|
wenzelm@26653
|
265 |
|
wenzelm@26653
|
266 |
(* forall_elim_var(s) *)
|
wenzelm@26653
|
267 |
|
wenzelm@26653
|
268 |
local
|
wenzelm@26653
|
269 |
|
wenzelm@26653
|
270 |
fun forall_elim_vars_aux strip_vars i th =
|
wenzelm@26653
|
271 |
let
|
wenzelm@26653
|
272 |
val thy = Thm.theory_of_thm th;
|
wenzelm@26653
|
273 |
val {tpairs, prop, ...} = Thm.rep_thm th;
|
wenzelm@26653
|
274 |
val add_used = Term.fold_aterms
|
wenzelm@26653
|
275 |
(fn Var ((x, j), _) => if i = j then insert (op =) x else I | _ => I);
|
wenzelm@26653
|
276 |
val used = fold (fn (t, u) => add_used t o add_used u) tpairs (add_used prop []);
|
wenzelm@26653
|
277 |
val vars = strip_vars prop;
|
wenzelm@26653
|
278 |
val cvars = (Name.variant_list used (map #1 vars), vars)
|
wenzelm@26653
|
279 |
|> ListPair.map (fn (x, (_, T)) => Thm.cterm_of thy (Var ((x, i), T)));
|
wenzelm@26653
|
280 |
in fold Thm.forall_elim cvars th end;
|
wenzelm@26653
|
281 |
|
wenzelm@26653
|
282 |
in
|
wenzelm@26653
|
283 |
|
wenzelm@26653
|
284 |
val forall_elim_vars = forall_elim_vars_aux Term.strip_all_vars;
|
wenzelm@26653
|
285 |
|
wenzelm@33697
|
286 |
fun forall_elim_var i th =
|
wenzelm@33697
|
287 |
forall_elim_vars_aux
|
wenzelm@33697
|
288 |
(fn Const ("all", _) $ Abs (a, T, _) => [(a, T)]
|
wenzelm@33697
|
289 |
| _ => raise THM ("forall_elim_vars", i, [th])) i th;
|
wenzelm@26653
|
290 |
|
wenzelm@26653
|
291 |
end;
|
wenzelm@26653
|
292 |
|
wenzelm@26653
|
293 |
|
wenzelm@32282
|
294 |
(* certify_instantiate *)
|
wenzelm@32282
|
295 |
|
wenzelm@32282
|
296 |
fun certify_inst thy (instT, inst) =
|
wenzelm@32282
|
297 |
(map (fn (v, T) => (Thm.ctyp_of thy (TVar v), Thm.ctyp_of thy T)) instT,
|
wenzelm@32282
|
298 |
map (fn (v, t) => (Thm.cterm_of thy (Var v), Thm.cterm_of thy t)) inst);
|
wenzelm@32282
|
299 |
|
wenzelm@32282
|
300 |
fun certify_instantiate insts th =
|
wenzelm@32282
|
301 |
Thm.instantiate (certify_inst (Thm.theory_of_thm th) insts) th;
|
wenzelm@32282
|
302 |
|
wenzelm@32282
|
303 |
|
wenzelm@35986
|
304 |
(* forall_intr_frees: generalization over all suitable Free variables *)
|
wenzelm@35986
|
305 |
|
wenzelm@35986
|
306 |
fun forall_intr_frees th =
|
wenzelm@35986
|
307 |
let
|
wenzelm@35986
|
308 |
val thy = Thm.theory_of_thm th;
|
wenzelm@35986
|
309 |
val {prop, hyps, tpairs, ...} = Thm.rep_thm th;
|
wenzelm@35986
|
310 |
val fixed = fold Term.add_frees (Thm.terms_of_tpairs tpairs @ hyps) [];
|
wenzelm@35986
|
311 |
val frees = Term.fold_aterms (fn Free v =>
|
wenzelm@35986
|
312 |
if member (op =) fixed v then I else insert (op =) v | _ => I) prop [];
|
wenzelm@35986
|
313 |
in fold (Thm.forall_intr o Thm.cterm_of thy o Free) frees th end;
|
wenzelm@35986
|
314 |
|
wenzelm@35986
|
315 |
|
wenzelm@35845
|
316 |
(* unvarify_global: global schematic variables *)
|
wenzelm@26653
|
317 |
|
wenzelm@35845
|
318 |
fun unvarify_global th =
|
wenzelm@24980
|
319 |
let
|
wenzelm@24980
|
320 |
val prop = Thm.full_prop_of th;
|
wenzelm@35845
|
321 |
val _ = map Logic.unvarify_global (prop :: Thm.hyps_of th)
|
wenzelm@24980
|
322 |
handle TERM (msg, _) => raise THM (msg, 0, [th]);
|
wenzelm@24980
|
323 |
|
wenzelm@32282
|
324 |
val instT = rev (Term.add_tvars prop []) |> map (fn v as ((a, _), S) => (v, TFree (a, S)));
|
wenzelm@24980
|
325 |
val inst = rev (Term.add_vars prop []) |> map (fn ((a, i), T) =>
|
wenzelm@32282
|
326 |
let val T' = Term_Subst.instantiateT instT T
|
wenzelm@32282
|
327 |
in (((a, i), T'), Free ((a, T'))) end);
|
wenzelm@32282
|
328 |
in certify_instantiate (instT, inst) th end;
|
wenzelm@24980
|
329 |
|
wenzelm@26653
|
330 |
|
wenzelm@26653
|
331 |
(* close_derivation *)
|
wenzelm@26653
|
332 |
|
wenzelm@26628
|
333 |
fun close_derivation thm =
|
wenzelm@36753
|
334 |
if Thm.derivation_name thm = "" then Thm.name_derivation "" thm
|
wenzelm@26628
|
335 |
else thm;
|
wenzelm@26628
|
336 |
|
wenzelm@24980
|
337 |
|
wenzelm@24980
|
338 |
|
wenzelm@24980
|
339 |
(** specification primitives **)
|
wenzelm@24980
|
340 |
|
wenzelm@30348
|
341 |
(* rules *)
|
wenzelm@30348
|
342 |
|
wenzelm@35855
|
343 |
fun stripped_sorts thy t =
|
wenzelm@35855
|
344 |
let
|
wenzelm@35855
|
345 |
val tfrees = rev (map TFree (Term.add_tfrees t []));
|
wenzelm@44211
|
346 |
val tfrees' = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT (length tfrees));
|
wenzelm@35855
|
347 |
val strip = tfrees ~~ tfrees';
|
wenzelm@35855
|
348 |
val recover = map (pairself (Thm.ctyp_of thy o Logic.varifyT_global) o swap) strip;
|
wenzelm@35855
|
349 |
val t' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip))) t;
|
wenzelm@35855
|
350 |
in (strip, recover, t') end;
|
wenzelm@35855
|
351 |
|
wenzelm@43246
|
352 |
fun add_axiom ctxt (b, prop) thy =
|
wenzelm@24980
|
353 |
let
|
wenzelm@43246
|
354 |
val _ = Sign.no_vars ctxt prop;
|
wenzelm@35855
|
355 |
val (strip, recover, prop') = stripped_sorts thy prop;
|
wenzelm@35855
|
356 |
val constraints = map (fn (TFree (_, S), T) => (T, S)) strip;
|
wenzelm@35855
|
357 |
val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of thy T, S)) strip;
|
wenzelm@36106
|
358 |
|
wenzelm@43246
|
359 |
val thy' = thy
|
wenzelm@52453
|
360 |
|> Theory.add_axiom ctxt (b, Logic.list_implies (maps Logic.mk_of_sort constraints, prop'));
|
wenzelm@52453
|
361 |
val axm_name = Sign.full_name thy' b;
|
wenzelm@36106
|
362 |
val axm' = Thm.axiom thy' axm_name;
|
wenzelm@35989
|
363 |
val thm =
|
wenzelm@35989
|
364 |
Thm.instantiate (recover, []) axm'
|
wenzelm@35989
|
365 |
|> unvarify_global
|
wenzelm@35989
|
366 |
|> fold elim_implies of_sorts;
|
wenzelm@36106
|
367 |
in ((axm_name, thm), thy') end;
|
wenzelm@24980
|
368 |
|
wenzelm@43246
|
369 |
fun add_axiom_global arg thy = add_axiom (Syntax.init_pretty_global thy) arg thy;
|
wenzelm@43246
|
370 |
|
wenzelm@43246
|
371 |
fun add_def ctxt unchecked overloaded (b, prop) thy =
|
wenzelm@24980
|
372 |
let
|
wenzelm@43246
|
373 |
val _ = Sign.no_vars ctxt prop;
|
wenzelm@35989
|
374 |
val prems = map (Thm.cterm_of thy) (Logic.strip_imp_prems prop);
|
wenzelm@35989
|
375 |
val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop);
|
wenzelm@36106
|
376 |
|
wenzelm@43246
|
377 |
val thy' = Theory.add_def ctxt unchecked overloaded (b, concl') thy;
|
wenzelm@36106
|
378 |
val axm_name = Sign.full_name thy' b;
|
wenzelm@36106
|
379 |
val axm' = Thm.axiom thy' axm_name;
|
wenzelm@35989
|
380 |
val thm =
|
wenzelm@35989
|
381 |
Thm.instantiate (recover, []) axm'
|
wenzelm@35989
|
382 |
|> unvarify_global
|
wenzelm@35989
|
383 |
|> fold_rev Thm.implies_intr prems;
|
wenzelm@36106
|
384 |
in ((axm_name, thm), thy') end;
|
wenzelm@24980
|
385 |
|
wenzelm@43246
|
386 |
fun add_def_global unchecked overloaded arg thy =
|
wenzelm@43246
|
387 |
add_def (Syntax.init_pretty_global thy) unchecked overloaded arg thy;
|
wenzelm@43246
|
388 |
|
wenzelm@27866
|
389 |
|
wenzelm@27866
|
390 |
|
wenzelm@27866
|
391 |
(** attributes **)
|
wenzelm@27866
|
392 |
|
wenzelm@40494
|
393 |
(*attributes subsume any kind of rules or context modifiers*)
|
wenzelm@46246
|
394 |
type attribute = Context.generic * thm -> Context.generic option * thm option;
|
wenzelm@40494
|
395 |
|
wenzelm@30214
|
396 |
type binding = binding * attribute list;
|
wenzelm@30214
|
397 |
val empty_binding: binding = (Binding.empty, []);
|
wenzelm@30214
|
398 |
|
wenzelm@46246
|
399 |
fun rule_attribute f (x, th) = (NONE, SOME (f x th));
|
wenzelm@46246
|
400 |
fun declaration_attribute f (x, th) = (SOME (f th x), NONE);
|
wenzelm@46246
|
401 |
fun mixed_attribute f (x, th) = let val (x', th') = f (x, th) in (SOME x', SOME th') end;
|
wenzelm@46246
|
402 |
|
wenzelm@47659
|
403 |
fun apply_attribute (att: attribute) th x =
|
wenzelm@46246
|
404 |
let val (x', th') = att (x, th)
|
wenzelm@47659
|
405 |
in (the_default th th', the_default x x') end;
|
wenzelm@46246
|
406 |
|
wenzelm@47659
|
407 |
fun attribute_declaration att th x = #2 (apply_attribute att th x);
|
wenzelm@27866
|
408 |
|
wenzelm@27866
|
409 |
fun apply_attributes mk dest =
|
wenzelm@27866
|
410 |
let
|
wenzelm@47659
|
411 |
fun app [] th x = (th, x)
|
wenzelm@47659
|
412 |
| app (att :: atts) th x = apply_attribute att th (mk x) ||> dest |-> app atts;
|
wenzelm@27866
|
413 |
in app end;
|
wenzelm@27866
|
414 |
|
wenzelm@27866
|
415 |
val theory_attributes = apply_attributes Context.Theory Context.the_theory;
|
wenzelm@27866
|
416 |
val proof_attributes = apply_attributes Context.Proof Context.the_proof;
|
wenzelm@27866
|
417 |
|
wenzelm@27866
|
418 |
fun no_attributes x = (x, []);
|
wenzelm@27866
|
419 |
fun simple_fact x = [(x, [])];
|
wenzelm@27866
|
420 |
|
wenzelm@27866
|
421 |
|
wenzelm@27866
|
422 |
|
wenzelm@27866
|
423 |
(*** theorem tags ***)
|
wenzelm@27866
|
424 |
|
wenzelm@27866
|
425 |
(* add / delete tags *)
|
wenzelm@27866
|
426 |
|
wenzelm@27866
|
427 |
fun tag_rule tg = Thm.map_tags (insert (op =) tg);
|
wenzelm@27866
|
428 |
fun untag_rule s = Thm.map_tags (filter_out (fn (s', _) => s = s'));
|
wenzelm@27866
|
429 |
|
wenzelm@46246
|
430 |
fun tag tg = rule_attribute (K (tag_rule tg));
|
wenzelm@46246
|
431 |
fun untag s = rule_attribute (K (untag_rule s));
|
wenzelm@27866
|
432 |
|
wenzelm@27866
|
433 |
|
wenzelm@30348
|
434 |
(* def_name *)
|
wenzelm@30348
|
435 |
|
wenzelm@30348
|
436 |
fun def_name c = c ^ "_def";
|
wenzelm@30348
|
437 |
|
wenzelm@30348
|
438 |
fun def_name_optional c "" = def_name c
|
wenzelm@30348
|
439 |
| def_name_optional _ name = name;
|
wenzelm@30348
|
440 |
|
wenzelm@35238
|
441 |
val def_binding = Binding.map_name def_name;
|
wenzelm@35238
|
442 |
|
wenzelm@30447
|
443 |
fun def_binding_optional b name =
|
wenzelm@35238
|
444 |
if Binding.is_empty name then def_binding b else name;
|
wenzelm@30447
|
445 |
|
wenzelm@30348
|
446 |
|
wenzelm@27866
|
447 |
(* unofficial theorem names *)
|
wenzelm@27866
|
448 |
|
wenzelm@27866
|
449 |
fun the_name_hint thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.nameN);
|
wenzelm@27866
|
450 |
|
wenzelm@27866
|
451 |
val has_name_hint = can the_name_hint;
|
wenzelm@27866
|
452 |
val get_name_hint = the_default "??.unknown" o try the_name_hint;
|
wenzelm@27866
|
453 |
|
wenzelm@27866
|
454 |
fun put_name_hint name = untag_rule Markup.nameN #> tag_rule (Markup.nameN, name);
|
wenzelm@27866
|
455 |
|
wenzelm@27866
|
456 |
|
wenzelm@27866
|
457 |
(* theorem kinds *)
|
wenzelm@27866
|
458 |
|
wenzelm@27866
|
459 |
val theoremK = "theorem";
|
wenzelm@27866
|
460 |
val lemmaK = "lemma";
|
wenzelm@27866
|
461 |
val corollaryK = "corollary";
|
wenzelm@27866
|
462 |
|
wenzelm@43344
|
463 |
fun legacy_get_kind thm = the_default "" (Properties.get (Thm.get_tags thm) Markup.kindN);
|
wenzelm@27866
|
464 |
|
wenzelm@27866
|
465 |
fun kind_rule k = tag_rule (Markup.kindN, k) o untag_rule Markup.kindN;
|
wenzelm@46246
|
466 |
fun kind k = rule_attribute (K (k <> "" ? kind_rule k));
|
wenzelm@27866
|
467 |
|
wenzelm@27866
|
468 |
|
wenzelm@50026
|
469 |
(* forked proofs *)
|
wenzelm@50025
|
470 |
|
wenzelm@50077
|
471 |
structure Proofs = Theory_Data
|
wenzelm@50025
|
472 |
(
|
wenzelm@50077
|
473 |
type T = thm list;
|
wenzelm@50077
|
474 |
val empty = [];
|
wenzelm@50025
|
475 |
fun extend _ = empty;
|
wenzelm@50025
|
476 |
fun merge _ = empty;
|
wenzelm@50025
|
477 |
);
|
wenzelm@50025
|
478 |
|
wenzelm@50077
|
479 |
fun register_proofs more_thms = Proofs.map (fn thms => fold cons more_thms thms);
|
wenzelm@50077
|
480 |
val join_theory_proofs = Thm.join_proofs o rev o Proofs.get;
|
wenzelm@50025
|
481 |
|
wenzelm@50025
|
482 |
|
wenzelm@22362
|
483 |
open Thm;
|
wenzelm@22362
|
484 |
|
wenzelm@22362
|
485 |
end;
|
wenzelm@22362
|
486 |
|
wenzelm@32846
|
487 |
structure Basic_Thm: BASIC_THM = Thm;
|
wenzelm@32846
|
488 |
open Basic_Thm;
|
wenzelm@23170
|
489 |
|