author | wenzelm |
Fri, 03 Sep 2021 18:57:33 +0200 | |
changeset 74220 | c49134ee16c1 |
parent 74200 | 17090e27aae9 |
child 74230 | d637611b41bd |
permissions | -rw-r--r-- |
22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/more_thm.ML |
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
3 |
|
22907 | 4 |
Further operations on type ctyp/cterm/thm, outside the inference kernel. |
22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
5 |
*) |
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
6 |
|
23169 | 7 |
infix aconvc; |
8 |
||
32842 | 9 |
signature BASIC_THM = |
10 |
sig |
|
11 |
include BASIC_THM |
|
61268 | 12 |
val show_consts: bool Config.T |
13 |
val show_hyps: bool Config.T |
|
14 |
val show_tags: bool Config.T |
|
32842 | 15 |
structure Ctermtab: TABLE |
16 |
structure Thmtab: TABLE |
|
17 |
val aconvc: cterm * cterm -> bool |
|
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
43780
diff
changeset
|
18 |
type attribute = Context.generic * thm -> Context.generic option * thm option |
32842 | 19 |
end; |
20 |
||
22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
21 |
signature THM = |
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
22 |
sig |
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
23 |
include THM |
32842 | 24 |
structure Ctermtab: TABLE |
25 |
structure Thmtab: TABLE |
|
60952
762cb38a3147
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60951
diff
changeset
|
26 |
val eq_ctyp: ctyp * ctyp -> bool |
24948 | 27 |
val aconvc: cterm * cterm -> bool |
60952
762cb38a3147
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60951
diff
changeset
|
28 |
val add_tvars: thm -> ctyp list -> ctyp list |
60818 | 29 |
val add_frees: thm -> cterm list -> cterm list |
30 |
val add_vars: thm -> cterm list -> cterm list |
|
70159 | 31 |
val dest_funT: ctyp -> ctyp * ctyp |
70152 | 32 |
val strip_type: ctyp -> ctyp list * ctyp |
60938 | 33 |
val all_name: Proof.context -> string * cterm -> cterm -> cterm |
34 |
val all: Proof.context -> cterm -> cterm -> cterm |
|
22907 | 35 |
val mk_binop: cterm -> cterm -> cterm -> cterm |
36 |
val dest_binop: cterm -> cterm * cterm |
|
37 |
val dest_implies: cterm -> cterm * cterm |
|
38 |
val dest_equals: cterm -> cterm * cterm |
|
39 |
val dest_equals_lhs: cterm -> cterm |
|
40 |
val dest_equals_rhs: cterm -> cterm |
|
41 |
val lhs_of: thm -> cterm |
|
42 |
val rhs_of: thm -> cterm |
|
70586 | 43 |
val fast_term_ord: cterm ord |
44 |
val term_ord: cterm ord |
|
45 |
val thm_ord: thm ord |
|
32842 | 46 |
val cterm_cache: (cterm -> 'a) -> cterm -> 'a |
47 |
val thm_cache: (thm -> 'a) -> thm -> 'a |
|
23599 | 48 |
val is_reflexive: thm -> bool |
22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
49 |
val eq_thm: thm * thm -> bool |
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
50 |
val eq_thm_prop: thm * thm -> bool |
52683
fb028440473e
more official Thm.eq_thm_strict, without demanding ML equality type;
wenzelm
parents:
51316
diff
changeset
|
51 |
val eq_thm_strict: thm * thm -> bool |
60817 | 52 |
val equiv_thm: theory -> thm * thm -> bool |
31944 | 53 |
val class_triv: theory -> class -> thm |
54 |
val of_sort: ctyp * sort -> thm list |
|
24048
a12b4faff474
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23599
diff
changeset
|
55 |
val is_dummy: thm -> bool |
a12b4faff474
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23599
diff
changeset
|
56 |
val add_thm: thm -> thm list -> thm list |
a12b4faff474
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23599
diff
changeset
|
57 |
val del_thm: thm -> thm list -> thm list |
a12b4faff474
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23599
diff
changeset
|
58 |
val merge_thms: thm list * thm list -> thm list |
74152 | 59 |
val item_net: thm Item_Net.T |
60 |
val item_net_intro: thm Item_Net.T |
|
61 |
val item_net_elim: thm Item_Net.T |
|
54984
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset
|
62 |
val declare_hyps: cterm -> Proof.context -> Proof.context |
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset
|
63 |
val assume_hyps: cterm -> Proof.context -> thm * Proof.context |
54993
625370769fc0
check_hyps for attribute application (still inactive, due to non-compliant tools);
wenzelm
parents:
54984
diff
changeset
|
64 |
val unchecked_hyps: Proof.context -> Proof.context |
625370769fc0
check_hyps for attribute application (still inactive, due to non-compliant tools);
wenzelm
parents:
54984
diff
changeset
|
65 |
val restore_hyps: Proof.context -> Proof.context -> Proof.context |
55633 | 66 |
val undeclared_hyps: Context.generic -> thm -> term list |
54993
625370769fc0
check_hyps for attribute application (still inactive, due to non-compliant tools);
wenzelm
parents:
54984
diff
changeset
|
67 |
val check_hyps: Context.generic -> thm -> thm |
61508 | 68 |
val declare_term_sorts: term -> Proof.context -> Proof.context |
61509
358dfae15d83
print thm wrt. local shyps (from full proof context);
wenzelm
parents:
61508
diff
changeset
|
69 |
val extra_shyps': Proof.context -> thm -> sort list |
61508 | 70 |
val check_shyps: Proof.context -> thm -> thm |
71 |
val weaken_sorts': Proof.context -> cterm -> cterm |
|
27866
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
72 |
val elim_implies: thm -> thm -> thm |
61339 | 73 |
val forall_intr_name: string * cterm -> thm -> thm |
27866
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
74 |
val forall_elim_var: int -> thm -> thm |
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
75 |
val forall_elim_vars: int -> thm -> thm |
67698
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
76 |
val instantiate_frees: ((string * sort) * ctyp) list * ((string * typ) * cterm) list -> thm -> thm |
60801 | 77 |
val instantiate': ctyp option list -> cterm option list -> thm -> thm |
35985
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset
|
78 |
val forall_intr_frees: thm -> thm |
60825 | 79 |
val unvarify_global: theory -> thm -> thm |
80 |
val unvarify_axiom: theory -> string -> thm |
|
59969
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
81 |
val rename_params_rule: string list * int -> thm -> thm |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
82 |
val rename_boundvars: term -> term -> thm -> thm |
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
40238
diff
changeset
|
83 |
val add_axiom: Proof.context -> binding * term -> theory -> (string * thm) * theory |
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
40238
diff
changeset
|
84 |
val add_axiom_global: binding * term -> theory -> (string * thm) * theory |
61261
ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
61059
diff
changeset
|
85 |
val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> (string * thm) * theory |
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
40238
diff
changeset
|
86 |
val add_def_global: bool -> bool -> binding * term -> theory -> (string * thm) * theory |
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
43780
diff
changeset
|
87 |
type attribute = Context.generic * thm -> Context.generic option * thm option |
30210 | 88 |
type binding = binding * attribute list |
46830 | 89 |
val tag_rule: string * string -> thm -> thm |
27866
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
90 |
val untag_rule: string -> thm -> thm |
61852 | 91 |
val is_free_dummy: thm -> bool |
92 |
val tag_free_dummy: thm -> thm |
|
30342 | 93 |
val def_name: string -> string |
94 |
val def_name_optional: string -> string -> string |
|
35238 | 95 |
val def_binding: Binding.binding -> Binding.binding |
30433
ce5138c92ca7
added def_binding_optional -- robust version of def_name_optional for bindings;
wenzelm
parents:
30342
diff
changeset
|
96 |
val def_binding_optional: Binding.binding -> Binding.binding -> Binding.binding |
62093 | 97 |
val make_def_binding: bool -> Binding.binding -> Binding.binding |
27866
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
98 |
val has_name_hint: thm -> bool |
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
99 |
val get_name_hint: thm -> string |
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
100 |
val put_name_hint: string -> thm -> thm |
22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
101 |
val theoremK: string |
42473 | 102 |
val legacy_get_kind: thm -> string |
27866
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
103 |
val kind_rule: string -> thm -> thm |
61853
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
104 |
val rule_attribute: thm list -> (Context.generic -> thm -> thm) -> attribute |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
105 |
val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
106 |
val mixed_attribute: (Context.generic * thm -> Context.generic * thm) -> attribute |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
107 |
val apply_attribute: attribute -> thm -> Context.generic -> thm * Context.generic |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
108 |
val attribute_declaration: attribute -> thm -> Context.generic -> Context.generic |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
109 |
val theory_attributes: attribute list -> thm -> theory -> thm * theory |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
110 |
val proof_attributes: attribute list -> thm -> Proof.context -> thm * Proof.context |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
111 |
val no_attributes: 'a -> 'a * 'b list |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
112 |
val simple_fact: 'a -> ('a * 'b list) list |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
113 |
val tag: string * string -> attribute |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
114 |
val untag: string -> attribute |
27866
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
115 |
val kind: string -> attribute |
67671
857da80611ab
support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes;
wenzelm
parents:
67649
diff
changeset
|
116 |
val register_proofs: thm list lazy -> theory -> theory |
64574
1134e4d5e5b7
consolidate nested thms with persistent result, for improved performance;
wenzelm
parents:
64568
diff
changeset
|
117 |
val consolidate_theory: theory -> unit |
71023
35a8e15b7e03
more robust Thm.expose_theory -- ensure that PIDE export happens in the proper theory context;
wenzelm
parents:
71018
diff
changeset
|
118 |
val expose_theory: theory -> unit |
61268 | 119 |
val show_consts: bool Config.T |
120 |
val show_hyps: bool Config.T |
|
121 |
val show_tags: bool Config.T |
|
122 |
val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool} -> thm -> Pretty.T |
|
123 |
val pretty_thm: Proof.context -> thm -> Pretty.T |
|
124 |
val pretty_thm_item: Proof.context -> thm -> Pretty.T |
|
125 |
val pretty_thm_global: theory -> thm -> Pretty.T |
|
126 |
val string_of_thm: Proof.context -> thm -> string |
|
127 |
val string_of_thm_global: theory -> thm -> string |
|
22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
128 |
end; |
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
129 |
|
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
130 |
structure Thm: THM = |
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
131 |
struct |
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
132 |
|
22695
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset
|
133 |
(** basic operations **) |
22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
134 |
|
60952
762cb38a3147
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60951
diff
changeset
|
135 |
(* collecting ctyps and cterms *) |
23491 | 136 |
|
60952
762cb38a3147
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60951
diff
changeset
|
137 |
val eq_ctyp = op = o apply2 Thm.typ_of; |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58001
diff
changeset
|
138 |
val op aconvc = op aconv o apply2 Thm.term_of; |
23491 | 139 |
|
60952
762cb38a3147
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60951
diff
changeset
|
140 |
val add_tvars = Thm.fold_atomic_ctyps (fn a => is_TVar (Thm.typ_of a) ? insert eq_ctyp a); |
60818 | 141 |
val add_frees = Thm.fold_atomic_cterms (fn a => is_Free (Thm.term_of a) ? insert (op aconvc) a); |
142 |
val add_vars = Thm.fold_atomic_cterms (fn a => is_Var (Thm.term_of a) ? insert (op aconvc) a); |
|
23491 | 143 |
|
144 |
||
70155 | 145 |
(* ctyp operations *) |
70152 | 146 |
|
70159 | 147 |
fun dest_funT cT = |
70155 | 148 |
(case Thm.typ_of cT of |
149 |
Type ("fun", _) => let val [A, B] = Thm.dest_ctyp cT in (A, B) end |
|
70159 | 150 |
| T => raise TYPE ("dest_funT", [T], [])); |
70152 | 151 |
|
152 |
(* ctyp version of strip_type: maps [T1,...,Tn]--->T to ([T1,T2,...,Tn], T) *) |
|
153 |
fun strip_type cT = |
|
154 |
(case Thm.typ_of cT of |
|
155 |
Type ("fun", _) => |
|
156 |
let |
|
70159 | 157 |
val (cT1, cT2) = dest_funT cT; |
70152 | 158 |
val (cTs, cT') = strip_type cT2 |
159 |
in (cT1 :: cTs, cT') end |
|
160 |
| _ => ([], cT)); |
|
161 |
||
162 |
||
70155 | 163 |
(* cterm operations *) |
22907 | 164 |
|
60938 | 165 |
fun all_name ctxt (x, t) A = |
32198 | 166 |
let |
59586 | 167 |
val T = Thm.typ_of_cterm t; |
60938 | 168 |
val all_const = Thm.cterm_of ctxt (Const ("Pure.all", (T --> propT) --> propT)); |
169 |
in Thm.apply all_const (Thm.lambda_name (x, t) A) end; |
|
32198 | 170 |
|
60938 | 171 |
fun all ctxt t A = all_name ctxt ("", t) A; |
32198 | 172 |
|
46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
45382
diff
changeset
|
173 |
fun mk_binop c a b = Thm.apply (Thm.apply c a) b; |
22907 | 174 |
fun dest_binop ct = (Thm.dest_arg1 ct, Thm.dest_arg ct); |
175 |
||
176 |
fun dest_implies ct = |
|
177 |
(case Thm.term_of ct of |
|
56245 | 178 |
Const ("Pure.imp", _) $ _ $ _ => dest_binop ct |
22907 | 179 |
| _ => raise TERM ("dest_implies", [Thm.term_of ct])); |
180 |
||
181 |
fun dest_equals ct = |
|
182 |
(case Thm.term_of ct of |
|
56245 | 183 |
Const ("Pure.eq", _) $ _ $ _ => dest_binop ct |
22907 | 184 |
| _ => raise TERM ("dest_equals", [Thm.term_of ct])); |
185 |
||
186 |
fun dest_equals_lhs ct = |
|
187 |
(case Thm.term_of ct of |
|
56245 | 188 |
Const ("Pure.eq", _) $ _ $ _ => Thm.dest_arg1 ct |
22907 | 189 |
| _ => raise TERM ("dest_equals_lhs", [Thm.term_of ct])); |
190 |
||
191 |
fun dest_equals_rhs ct = |
|
192 |
(case Thm.term_of ct of |
|
56245 | 193 |
Const ("Pure.eq", _) $ _ $ _ => Thm.dest_arg ct |
22907 | 194 |
| _ => raise TERM ("dest_equals_rhs", [Thm.term_of ct])); |
195 |
||
196 |
val lhs_of = dest_equals_lhs o Thm.cprop_of; |
|
197 |
val rhs_of = dest_equals_rhs o Thm.cprop_of; |
|
198 |
||
199 |
||
67559 | 200 |
(* certified term order *) |
201 |
||
202 |
val fast_term_ord = Term_Ord.fast_term_ord o apply2 Thm.term_of; |
|
203 |
val term_ord = Term_Ord.term_ord o apply2 Thm.term_of; |
|
204 |
||
205 |
||
22907 | 206 |
(* thm order: ignores theory context! *) |
22682 | 207 |
|
70464 | 208 |
val thm_ord = |
209 |
Term_Ord.fast_term_ord o apply2 Thm.prop_of |
|
73860 | 210 |
||| list_ord (prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord) o apply2 Thm.tpairs_of |
211 |
||| list_ord Term_Ord.fast_term_ord o apply2 Thm.hyps_of |
|
212 |
||| list_ord Term_Ord.sort_ord o apply2 Thm.shyps_of; |
|
22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
213 |
|
22682 | 214 |
|
32842 | 215 |
(* tables and caches *) |
216 |
||
67559 | 217 |
structure Ctermtab = Table(type key = cterm val ord = fast_term_ord); |
32842 | 218 |
structure Thmtab = Table(type key = thm val ord = thm_ord); |
219 |
||
220 |
fun cterm_cache f = Cache.create Ctermtab.empty Ctermtab.lookup Ctermtab.update f; |
|
221 |
fun thm_cache f = Cache.create Thmtab.empty Thmtab.lookup Thmtab.update f; |
|
222 |
||
223 |
||
22682 | 224 |
(* equality *) |
225 |
||
23599 | 226 |
fun is_reflexive th = op aconv (Logic.dest_equals (Thm.prop_of th)) |
227 |
handle TERM _ => false; |
|
228 |
||
55547
384bfd19ee61
subtle change of semantics of Thm.eq_thm, e.g. relevant for merge of src/HOL/Tools/Predicate_Compile/core_data.ML (cf. HOL-IMP);
wenzelm
parents:
54996
diff
changeset
|
229 |
val eq_thm = is_equal o thm_ord; |
22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
230 |
|
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58001
diff
changeset
|
231 |
val eq_thm_prop = op aconv o apply2 Thm.full_prop_of; |
22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
232 |
|
52683
fb028440473e
more official Thm.eq_thm_strict, without demanding ML equality type;
wenzelm
parents:
51316
diff
changeset
|
233 |
fun eq_thm_strict ths = |
55547
384bfd19ee61
subtle change of semantics of Thm.eq_thm, e.g. relevant for merge of src/HOL/Tools/Predicate_Compile/core_data.ML (cf. HOL-IMP);
wenzelm
parents:
54996
diff
changeset
|
234 |
eq_thm ths andalso |
65458 | 235 |
Context.eq_thy_id (apply2 Thm.theory_id ths) andalso |
61040 | 236 |
op = (apply2 Thm.maxidx_of ths) andalso |
237 |
op = (apply2 Thm.get_tags ths); |
|
52683
fb028440473e
more official Thm.eq_thm_strict, without demanding ML equality type;
wenzelm
parents:
51316
diff
changeset
|
238 |
|
22682 | 239 |
|
240 |
(* pattern equivalence *) |
|
241 |
||
60817 | 242 |
fun equiv_thm thy ths = |
243 |
Pattern.equiv thy (apply2 (Thm.full_prop_of o Thm.transfer thy) ths); |
|
22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
244 |
|
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
245 |
|
31904
a86896359ca4
renamed Drule.sort_triv to Thm.sort_triv (cf. more_thm.ML);
wenzelm
parents:
31177
diff
changeset
|
246 |
(* type classes and sorts *) |
a86896359ca4
renamed Drule.sort_triv to Thm.sort_triv (cf. more_thm.ML);
wenzelm
parents:
31177
diff
changeset
|
247 |
|
31944 | 248 |
fun class_triv thy c = |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59616
diff
changeset
|
249 |
Thm.of_class (Thm.global_ctyp_of thy (TVar ((Name.aT, 0), [c])), c); |
31944 | 250 |
|
251 |
fun of_sort (T, S) = map (fn c => Thm.of_class (T, c)) S; |
|
28621
a60164e8fff0
added check_shyps, which reject pending sort hypotheses;
wenzelm
parents:
28116
diff
changeset
|
252 |
|
a60164e8fff0
added check_shyps, which reject pending sort hypotheses;
wenzelm
parents:
28116
diff
changeset
|
253 |
|
22695
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset
|
254 |
(* misc operations *) |
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset
|
255 |
|
24048
a12b4faff474
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23599
diff
changeset
|
256 |
fun is_dummy thm = |
a12b4faff474
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23599
diff
changeset
|
257 |
(case try Logic.dest_term (Thm.concl_of thm) of |
a12b4faff474
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23599
diff
changeset
|
258 |
NONE => false |
58001
934d85f14d1d
more general dummy: may contain "parked arguments", for example;
wenzelm
parents:
56245
diff
changeset
|
259 |
| SOME t => Term.is_dummy_pattern (Term.head_of t)); |
24048
a12b4faff474
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23599
diff
changeset
|
260 |
|
22695
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset
|
261 |
|
30564 | 262 |
(* collections of theorems in canonical order *) |
24048
a12b4faff474
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23599
diff
changeset
|
263 |
|
a12b4faff474
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23599
diff
changeset
|
264 |
val add_thm = update eq_thm_prop; |
a12b4faff474
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23599
diff
changeset
|
265 |
val del_thm = remove eq_thm_prop; |
a12b4faff474
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23599
diff
changeset
|
266 |
val merge_thms = merge eq_thm_prop; |
a12b4faff474
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23599
diff
changeset
|
267 |
|
74152 | 268 |
val item_net = Item_Net.init eq_thm_prop (single o Thm.full_prop_of); |
269 |
val item_net_intro = Item_Net.init eq_thm_prop (single o Thm.concl_of); |
|
270 |
val item_net_elim = Item_Net.init eq_thm_prop (single o Thm.major_prem_of); |
|
30560 | 271 |
|
272 |
||
22682 | 273 |
|
61508 | 274 |
(** declared hyps and sort hyps **) |
54984
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset
|
275 |
|
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset
|
276 |
structure Hyps = Proof_Data |
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset
|
277 |
( |
61508 | 278 |
type T = {checked_hyps: bool, hyps: Termtab.set, shyps: sort Ord_List.T}; |
279 |
fun init _ : T = {checked_hyps = true, hyps = Termtab.empty, shyps = []}; |
|
54984
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset
|
280 |
); |
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset
|
281 |
|
61508 | 282 |
fun map_hyps f = Hyps.map (fn {checked_hyps, hyps, shyps} => |
283 |
let val (checked_hyps', hyps', shyps') = f (checked_hyps, hyps, shyps) |
|
284 |
in {checked_hyps = checked_hyps', hyps = hyps', shyps = shyps'} end); |
|
285 |
||
286 |
||
287 |
(* hyps *) |
|
288 |
||
289 |
fun declare_hyps raw_ct ctxt = ctxt |> map_hyps (fn (checked_hyps, hyps, shyps) => |
|
290 |
let |
|
291 |
val ct = Thm.transfer_cterm (Proof_Context.theory_of ctxt) raw_ct; |
|
292 |
val hyps' = Termtab.update (Thm.term_of ct, ()) hyps; |
|
293 |
in (checked_hyps, hyps', shyps) end); |
|
54984
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset
|
294 |
|
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset
|
295 |
fun assume_hyps ct ctxt = (Thm.assume ct, declare_hyps ct ctxt); |
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset
|
296 |
|
61508 | 297 |
val unchecked_hyps = map_hyps (fn (_, hyps, shyps) => (false, hyps, shyps)); |
298 |
||
299 |
fun restore_hyps ctxt = |
|
300 |
map_hyps (fn (_, hyps, shyps) => (#checked_hyps (Hyps.get ctxt), hyps, shyps)); |
|
54993
625370769fc0
check_hyps for attribute application (still inactive, due to non-compliant tools);
wenzelm
parents:
54984
diff
changeset
|
301 |
|
55633 | 302 |
fun undeclared_hyps context th = |
303 |
Thm.hyps_of th |
|
304 |
|> filter_out |
|
305 |
(case context of |
|
306 |
Context.Theory _ => K false |
|
307 |
| Context.Proof ctxt => |
|
308 |
(case Hyps.get ctxt of |
|
61508 | 309 |
{checked_hyps = false, ...} => K true |
310 |
| {hyps, ...} => Termtab.defined hyps)); |
|
55633 | 311 |
|
54993
625370769fc0
check_hyps for attribute application (still inactive, due to non-compliant tools);
wenzelm
parents:
54984
diff
changeset
|
312 |
fun check_hyps context th = |
55633 | 313 |
(case undeclared_hyps context th of |
314 |
[] => th |
|
315 |
| undeclared => |
|
61263 | 316 |
error (Pretty.string_of (Pretty.big_list "Undeclared hyps:" |
317 |
(map (Pretty.item o single o Syntax.pretty_term (Syntax.init_pretty context)) undeclared)))); |
|
54984
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset
|
318 |
|
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset
|
319 |
|
61508 | 320 |
(* shyps *) |
321 |
||
322 |
fun declare_term_sorts t = |
|
323 |
map_hyps (fn (checked_hyps, hyps, shyps) => |
|
324 |
(checked_hyps, hyps, Sorts.insert_term t shyps)); |
|
325 |
||
61509
358dfae15d83
print thm wrt. local shyps (from full proof context);
wenzelm
parents:
61508
diff
changeset
|
326 |
fun extra_shyps' ctxt th = |
358dfae15d83
print thm wrt. local shyps (from full proof context);
wenzelm
parents:
61508
diff
changeset
|
327 |
Sorts.subtract (#shyps (Hyps.get ctxt)) (Thm.extra_shyps th); |
358dfae15d83
print thm wrt. local shyps (from full proof context);
wenzelm
parents:
61508
diff
changeset
|
328 |
|
61508 | 329 |
fun check_shyps ctxt raw_th = |
330 |
let |
|
331 |
val th = Thm.strip_shyps raw_th; |
|
61509
358dfae15d83
print thm wrt. local shyps (from full proof context);
wenzelm
parents:
61508
diff
changeset
|
332 |
val extra_shyps = extra_shyps' ctxt th; |
61508 | 333 |
in |
61509
358dfae15d83
print thm wrt. local shyps (from full proof context);
wenzelm
parents:
61508
diff
changeset
|
334 |
if null extra_shyps then th |
61508 | 335 |
else error (Pretty.string_of (Pretty.block (Pretty.str "Pending sort hypotheses:" :: |
61509
358dfae15d83
print thm wrt. local shyps (from full proof context);
wenzelm
parents:
61508
diff
changeset
|
336 |
Pretty.brk 1 :: Pretty.commas (map (Syntax.pretty_sort ctxt) extra_shyps)))) |
61508 | 337 |
end; |
338 |
||
339 |
val weaken_sorts' = Thm.weaken_sorts o #shyps o Hyps.get; |
|
340 |
||
341 |
||
54984
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset
|
342 |
|
24980
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
343 |
(** basic derived rules **) |
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
344 |
|
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
345 |
(*Elimination of implication |
67721 | 346 |
A A \<Longrightarrow> B |
24980
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
347 |
------------ |
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
348 |
B |
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
349 |
*) |
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
350 |
fun elim_implies thA thAB = Thm.implies_elim thAB thA; |
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
351 |
|
26653 | 352 |
|
61339 | 353 |
(* forall_intr_name *) |
354 |
||
355 |
fun forall_intr_name (a, x) th = |
|
356 |
let |
|
357 |
val th' = Thm.forall_intr x th; |
|
358 |
val prop' = (case Thm.prop_of th' of all $ Abs (_, T, b) => all $ Abs (a, T, b)); |
|
359 |
in Thm.renamed_prop prop' th' end; |
|
360 |
||
361 |
||
26653 | 362 |
(* forall_elim_var(s) *) |
363 |
||
364 |
local |
|
365 |
||
60951
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset
|
366 |
fun dest_all ct = |
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset
|
367 |
(case Thm.term_of ct of |
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset
|
368 |
Const ("Pure.all", _) $ Abs (a, _, _) => |
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset
|
369 |
let val (x, ct') = Thm.dest_abs NONE (Thm.dest_arg ct) |
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset
|
370 |
in SOME ((a, Thm.ctyp_of_cterm x), ct') end |
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset
|
371 |
| _ => NONE); |
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset
|
372 |
|
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset
|
373 |
fun dest_all_list ct = |
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset
|
374 |
(case dest_all ct of |
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset
|
375 |
NONE => [] |
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset
|
376 |
| SOME (v, ct') => v :: dest_all_list ct'); |
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset
|
377 |
|
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset
|
378 |
fun forall_elim_vars_list vars i th = |
26653 | 379 |
let |
60950 | 380 |
val used = |
381 |
(Thm.fold_terms o Term.fold_aterms) |
|
382 |
(fn Var ((x, j), _) => if i = j then insert (op =) x else I | _ => I) th []; |
|
60951
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset
|
383 |
val vars' = (Name.variant_list used (map #1 vars), vars) |
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset
|
384 |
|> ListPair.map (fn (x, (_, T)) => Thm.var ((x, i), T)); |
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset
|
385 |
in fold Thm.forall_elim vars' th end; |
26653 | 386 |
|
387 |
in |
|
388 |
||
60950 | 389 |
fun forall_elim_vars i th = |
60951
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset
|
390 |
forall_elim_vars_list (dest_all_list (Thm.cprop_of th)) i th; |
26653 | 391 |
|
33697 | 392 |
fun forall_elim_var i th = |
60950 | 393 |
let |
394 |
val vars = |
|
60951
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset
|
395 |
(case dest_all (Thm.cprop_of th) of |
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset
|
396 |
SOME (v, _) => [v] |
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset
|
397 |
| NONE => raise THM ("forall_elim_var", i, [th])); |
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset
|
398 |
in forall_elim_vars_list vars i th end; |
26653 | 399 |
|
400 |
end; |
|
401 |
||
402 |
||
67698
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
403 |
(* instantiate frees *) |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
404 |
|
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
405 |
fun instantiate_frees ([], []) th = th |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
406 |
| instantiate_frees (instT, inst) th = |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
407 |
let |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
408 |
val idx = Thm.maxidx_of th + 1; |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
409 |
fun index ((a, A), b) = (((a, idx), A), b); |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
410 |
val insts = (map index instT, map index inst); |
74200
17090e27aae9
more scalable data structure (but: rarely used with > 5 arguments);
wenzelm
parents:
74152
diff
changeset
|
411 |
val tfrees = fold (Symtab.insert_set o #1 o #1) instT Symtab.empty; |
17090e27aae9
more scalable data structure (but: rarely used with > 5 arguments);
wenzelm
parents:
74152
diff
changeset
|
412 |
val frees = fold (Symtab.insert_set o #1 o #1) inst Symtab.empty; |
67698
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
413 |
|
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
414 |
val hyps = Thm.chyps_of th; |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
415 |
val inst_cterm = |
74200
17090e27aae9
more scalable data structure (but: rarely used with > 5 arguments);
wenzelm
parents:
74152
diff
changeset
|
416 |
Thm.generalize_cterm (tfrees, frees) idx #> |
67698
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
417 |
Thm.instantiate_cterm insts; |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
418 |
in |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
419 |
th |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
420 |
|> fold_rev Thm.implies_intr hyps |
74200
17090e27aae9
more scalable data structure (but: rarely used with > 5 arguments);
wenzelm
parents:
74152
diff
changeset
|
421 |
|> Thm.generalize (tfrees, frees) idx |
67698
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
422 |
|> Thm.instantiate insts |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
423 |
|> fold (elim_implies o Thm.assume o inst_cterm) hyps |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
424 |
end; |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
425 |
|
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
426 |
|
60801 | 427 |
(* instantiate by left-to-right occurrence of variables *) |
428 |
||
429 |
fun instantiate' cTs cts thm = |
|
430 |
let |
|
431 |
fun err msg = |
|
432 |
raise TYPE ("instantiate': " ^ msg, |
|
433 |
map_filter (Option.map Thm.typ_of) cTs, |
|
434 |
map_filter (Option.map Thm.term_of) cts); |
|
435 |
||
436 |
fun zip_vars xs ys = |
|
437 |
zip_options xs ys handle ListPair.UnequalLengths => |
|
438 |
err "more instantiations than variables in thm"; |
|
439 |
||
440 |
val thm' = |
|
441 |
Thm.instantiate ((zip_vars (rev (Thm.fold_terms Term.add_tvars thm [])) cTs), []) thm; |
|
442 |
val thm'' = |
|
443 |
Thm.instantiate ([], zip_vars (rev (Thm.fold_terms Term.add_vars thm' [])) cts) thm'; |
|
444 |
in thm'' end; |
|
445 |
||
446 |
||
35985
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset
|
447 |
(* forall_intr_frees: generalization over all suitable Free variables *) |
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset
|
448 |
|
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset
|
449 |
fun forall_intr_frees th = |
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset
|
450 |
let |
61041 | 451 |
val fixed = |
452 |
fold Term.add_frees (Thm.terms_of_tpairs (Thm.tpairs_of th) @ Thm.hyps_of th) []; |
|
60821 | 453 |
val frees = |
454 |
Thm.fold_atomic_cterms (fn a => |
|
455 |
(case Thm.term_of a of |
|
456 |
Free v => not (member (op =) fixed v) ? insert (op aconvc) a |
|
457 |
| _ => I)) th []; |
|
458 |
in fold Thm.forall_intr frees th end; |
|
35985
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset
|
459 |
|
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset
|
460 |
|
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35715
diff
changeset
|
461 |
(* unvarify_global: global schematic variables *) |
26653 | 462 |
|
60825 | 463 |
fun unvarify_global thy th = |
24980
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
464 |
let |
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
465 |
val prop = Thm.full_prop_of th; |
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35715
diff
changeset
|
466 |
val _ = map Logic.unvarify_global (prop :: Thm.hyps_of th) |
24980
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
467 |
handle TERM (msg, _) => raise THM (msg, 0, [th]); |
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
468 |
|
32279 | 469 |
val instT = rev (Term.add_tvars prop []) |> map (fn v as ((a, _), S) => (v, TFree (a, S))); |
74220
c49134ee16c1
more scalable data structure (but: rarely used many arguments);
wenzelm
parents:
74200
diff
changeset
|
470 |
val instantiateT = Term_Subst.instantiateT (Term_Subst.TVars.table instT); |
24980
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
471 |
val inst = rev (Term.add_vars prop []) |> map (fn ((a, i), T) => |
74220
c49134ee16c1
more scalable data structure (but: rarely used many arguments);
wenzelm
parents:
74200
diff
changeset
|
472 |
let val T' = instantiateT T |
60805 | 473 |
in (((a, i), T'), Thm.global_cterm_of thy (Free ((a, T')))) end); |
474 |
in Thm.instantiate (map (apsnd (Thm.global_ctyp_of thy)) instT, inst) th end; |
|
24980
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
475 |
|
60825 | 476 |
fun unvarify_axiom thy = unvarify_global thy o Thm.axiom thy; |
477 |
||
26653 | 478 |
|
59969
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
479 |
(* user renaming of parameters in a subgoal *) |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
480 |
|
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
481 |
(*The names, if distinct, are used for the innermost parameters of subgoal i; |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
482 |
preceding parameters may be renamed to make all parameters distinct.*) |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
483 |
fun rename_params_rule (names, i) st = |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
484 |
let |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
485 |
val (_, Bs, Bi, C) = Thm.dest_state (st, i); |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
486 |
val params = map #1 (Logic.strip_params Bi); |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
487 |
val short = length params - length names; |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
488 |
val names' = |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
489 |
if short < 0 then error "More names than parameters in subgoal!" |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
490 |
else Name.variant_list names (take short params) @ names; |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
491 |
val free_names = Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) Bi []; |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
492 |
val Bi' = Logic.list_rename_params names' Bi; |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
493 |
in |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
494 |
(case duplicates (op =) names of |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
495 |
a :: _ => (warning ("Can't rename. Bound variables not distinct: " ^ a); st) |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
496 |
| [] => |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
497 |
(case inter (op =) names free_names of |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
498 |
a :: _ => (warning ("Can't rename. Bound/Free variable clash: " ^ a); st) |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
499 |
| [] => Thm.renamed_prop (Logic.list_implies (Bs @ [Bi'], C)) st)) |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
500 |
end; |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
501 |
|
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
502 |
|
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
503 |
(* preservation of bound variable names *) |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
504 |
|
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
505 |
fun rename_boundvars pat obj th = |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
506 |
(case Term.rename_abs pat obj (Thm.prop_of th) of |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
507 |
NONE => th |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
508 |
| SOME prop' => Thm.renamed_prop prop' th); |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
509 |
|
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
510 |
|
24980
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
511 |
|
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
512 |
(** specification primitives **) |
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
513 |
|
30342 | 514 |
(* rules *) |
515 |
||
35855
e7d004b89ca8
add_axiom: axiomatize "unconstrained" version, with explicit of_class premises;
wenzelm
parents:
35853
diff
changeset
|
516 |
fun stripped_sorts thy t = |
e7d004b89ca8
add_axiom: axiomatize "unconstrained" version, with explicit of_class premises;
wenzelm
parents:
35853
diff
changeset
|
517 |
let |
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60367
diff
changeset
|
518 |
val tfrees = rev (Term.add_tfrees t []); |
70922
539dfd4c166b
more conservative type names, e.g. relevant for Isabelle/MMT export;
wenzelm
parents:
70915
diff
changeset
|
519 |
val tfrees' = map (fn a => (a, [])) (Name.variant_list [] (map #1 tfrees)); |
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60367
diff
changeset
|
520 |
val recover = |
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60367
diff
changeset
|
521 |
map2 (fn (a', S') => fn (a, S) => (((a', 0), S'), Thm.global_ctyp_of thy (TVar ((a, 0), S)))) |
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60367
diff
changeset
|
522 |
tfrees' tfrees; |
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60367
diff
changeset
|
523 |
val strip = map (apply2 TFree) (tfrees ~~ tfrees'); |
35855
e7d004b89ca8
add_axiom: axiomatize "unconstrained" version, with explicit of_class premises;
wenzelm
parents:
35853
diff
changeset
|
524 |
val t' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip))) t; |
e7d004b89ca8
add_axiom: axiomatize "unconstrained" version, with explicit of_class premises;
wenzelm
parents:
35853
diff
changeset
|
525 |
in (strip, recover, t') end; |
e7d004b89ca8
add_axiom: axiomatize "unconstrained" version, with explicit of_class premises;
wenzelm
parents:
35853
diff
changeset
|
526 |
|
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
40238
diff
changeset
|
527 |
fun add_axiom ctxt (b, prop) thy = |
24980
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
528 |
let |
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
40238
diff
changeset
|
529 |
val _ = Sign.no_vars ctxt prop; |
35855
e7d004b89ca8
add_axiom: axiomatize "unconstrained" version, with explicit of_class premises;
wenzelm
parents:
35853
diff
changeset
|
530 |
val (strip, recover, prop') = stripped_sorts thy prop; |
e7d004b89ca8
add_axiom: axiomatize "unconstrained" version, with explicit of_class premises;
wenzelm
parents:
35853
diff
changeset
|
531 |
val constraints = map (fn (TFree (_, S), T) => (T, S)) strip; |
60367 | 532 |
val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of ctxt T, S)) strip; |
36106
19deea200358
Thm.add_axiom/add_def: return internal name of foundational axiom;
wenzelm
parents:
35988
diff
changeset
|
533 |
|
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
40238
diff
changeset
|
534 |
val thy' = thy |
51316
dfe469293eb4
discontinued empty name bindings in 'axiomatization';
wenzelm
parents:
49062
diff
changeset
|
535 |
|> Theory.add_axiom ctxt (b, Logic.list_implies (maps Logic.mk_of_sort constraints, prop')); |
dfe469293eb4
discontinued empty name bindings in 'axiomatization';
wenzelm
parents:
49062
diff
changeset
|
536 |
val axm_name = Sign.full_name thy' b; |
36106
19deea200358
Thm.add_axiom/add_def: return internal name of foundational axiom;
wenzelm
parents:
35988
diff
changeset
|
537 |
val axm' = Thm.axiom thy' axm_name; |
35988
76ca601c941e
disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
wenzelm
parents:
35985
diff
changeset
|
538 |
val thm = |
76ca601c941e
disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
wenzelm
parents:
35985
diff
changeset
|
539 |
Thm.instantiate (recover, []) axm' |
60825 | 540 |
|> unvarify_global thy' |
35988
76ca601c941e
disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
wenzelm
parents:
35985
diff
changeset
|
541 |
|> fold elim_implies of_sorts; |
36106
19deea200358
Thm.add_axiom/add_def: return internal name of foundational axiom;
wenzelm
parents:
35988
diff
changeset
|
542 |
in ((axm_name, thm), thy') end; |
24980
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
543 |
|
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
40238
diff
changeset
|
544 |
fun add_axiom_global arg thy = add_axiom (Syntax.init_pretty_global thy) arg thy; |
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
40238
diff
changeset
|
545 |
|
61261
ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
61059
diff
changeset
|
546 |
fun add_def (context as (ctxt, _)) unchecked overloaded (b, prop) thy = |
24980
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
547 |
let |
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
40238
diff
changeset
|
548 |
val _ = Sign.no_vars ctxt prop; |
60367 | 549 |
val prems = map (Thm.cterm_of ctxt) (Logic.strip_imp_prems prop); |
35988
76ca601c941e
disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
wenzelm
parents:
35985
diff
changeset
|
550 |
val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop); |
36106
19deea200358
Thm.add_axiom/add_def: return internal name of foundational axiom;
wenzelm
parents:
35988
diff
changeset
|
551 |
|
61261
ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
61059
diff
changeset
|
552 |
val thy' = Theory.add_def context unchecked overloaded (b, concl') thy; |
36106
19deea200358
Thm.add_axiom/add_def: return internal name of foundational axiom;
wenzelm
parents:
35988
diff
changeset
|
553 |
val axm_name = Sign.full_name thy' b; |
19deea200358
Thm.add_axiom/add_def: return internal name of foundational axiom;
wenzelm
parents:
35988
diff
changeset
|
554 |
val axm' = Thm.axiom thy' axm_name; |
35988
76ca601c941e
disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
wenzelm
parents:
35985
diff
changeset
|
555 |
val thm = |
76ca601c941e
disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
wenzelm
parents:
35985
diff
changeset
|
556 |
Thm.instantiate (recover, []) axm' |
60825 | 557 |
|> unvarify_global thy' |
35988
76ca601c941e
disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
wenzelm
parents:
35985
diff
changeset
|
558 |
|> fold_rev Thm.implies_intr prems; |
36106
19deea200358
Thm.add_axiom/add_def: return internal name of foundational axiom;
wenzelm
parents:
35988
diff
changeset
|
559 |
in ((axm_name, thm), thy') end; |
24980
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
560 |
|
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
40238
diff
changeset
|
561 |
fun add_def_global unchecked overloaded arg thy = |
61262
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61261
diff
changeset
|
562 |
add_def (Defs.global_context thy) unchecked overloaded arg thy; |
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
40238
diff
changeset
|
563 |
|
27866
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
564 |
|
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
565 |
|
70443 | 566 |
(** theorem tags **) |
27866
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
567 |
|
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
568 |
(* add / delete tags *) |
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
569 |
|
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
570 |
fun tag_rule tg = Thm.map_tags (insert (op =) tg); |
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
571 |
fun untag_rule s = Thm.map_tags (filter_out (fn (s', _) => s = s')); |
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
572 |
|
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
573 |
|
61852 | 574 |
(* free dummy thm -- for abstract closure *) |
575 |
||
576 |
val free_dummyN = "free_dummy"; |
|
577 |
fun is_free_dummy thm = Properties.defined (Thm.get_tags thm) free_dummyN; |
|
578 |
val tag_free_dummy = tag_rule (free_dummyN, ""); |
|
579 |
||
580 |
||
30342 | 581 |
(* def_name *) |
582 |
||
583 |
fun def_name c = c ^ "_def"; |
|
584 |
||
585 |
fun def_name_optional c "" = def_name c |
|
586 |
| def_name_optional _ name = name; |
|
587 |
||
63041
cb495c4807b3
clarified def binding position: reset for implicit/derived binding, keep for explicit binding;
wenzelm
parents:
62093
diff
changeset
|
588 |
val def_binding = Binding.map_name def_name #> Binding.reset_pos; |
cb495c4807b3
clarified def binding position: reset for implicit/derived binding, keep for explicit binding;
wenzelm
parents:
62093
diff
changeset
|
589 |
fun def_binding_optional b name = if Binding.is_empty name then def_binding b else name; |
cb495c4807b3
clarified def binding position: reset for implicit/derived binding, keep for explicit binding;
wenzelm
parents:
62093
diff
changeset
|
590 |
fun make_def_binding cond b = if cond then def_binding b else Binding.empty; |
62093 | 591 |
|
30342 | 592 |
|
27866
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
593 |
(* unofficial theorem names *) |
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
594 |
|
68036
4c9e79aeadf0
tuned -- avoid spurious exception trace for "the";
wenzelm
parents:
67778
diff
changeset
|
595 |
fun has_name_hint thm = AList.defined (op =) (Thm.get_tags thm) Markup.nameN; |
27866
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
596 |
fun the_name_hint thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.nameN); |
68036
4c9e79aeadf0
tuned -- avoid spurious exception trace for "the";
wenzelm
parents:
67778
diff
changeset
|
597 |
fun get_name_hint thm = if has_name_hint thm then the_name_hint thm else "??.unknown"; |
27866
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
598 |
|
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
599 |
fun put_name_hint name = untag_rule Markup.nameN #> tag_rule (Markup.nameN, name); |
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
600 |
|
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
601 |
|
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
602 |
(* theorem kinds *) |
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
603 |
|
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
604 |
val theoremK = "theorem"; |
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
605 |
|
42473 | 606 |
fun legacy_get_kind thm = the_default "" (Properties.get (Thm.get_tags thm) Markup.kindN); |
27866
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
607 |
|
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
608 |
fun kind_rule k = tag_rule (Markup.kindN, k) o untag_rule Markup.kindN; |
61853
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
609 |
|
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
610 |
|
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
611 |
|
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
612 |
(** attributes **) |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
613 |
|
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
614 |
(*attributes subsume any kind of rules or context modifiers*) |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
615 |
type attribute = Context.generic * thm -> Context.generic option * thm option; |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
616 |
|
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
617 |
type binding = binding * attribute list; |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
618 |
|
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
619 |
fun rule_attribute ths f (x, th) = |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
620 |
(NONE, |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
621 |
(case find_first is_free_dummy (th :: ths) of |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
622 |
SOME th' => SOME th' |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
623 |
| NONE => SOME (f x th))); |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
624 |
|
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
625 |
fun declaration_attribute f (x, th) = |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
626 |
(if is_free_dummy th then NONE else SOME (f th x), NONE); |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
627 |
|
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
628 |
fun mixed_attribute f (x, th) = |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
629 |
let val (x', th') = f (x, th) in (SOME x', SOME th') end; |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
630 |
|
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
631 |
fun apply_attribute (att: attribute) th x = |
67649 | 632 |
let val (x', th') = att (x, check_hyps x (Thm.transfer'' x th)) |
61853
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
633 |
in (the_default th th', the_default x x') end; |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
634 |
|
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
635 |
fun attribute_declaration att th x = #2 (apply_attribute att th x); |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
636 |
|
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
637 |
fun apply_attributes mk dest = |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
638 |
let |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
639 |
fun app [] th x = (th, x) |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
640 |
| app (att :: atts) th x = apply_attribute att th (mk x) ||> dest |-> app atts; |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
641 |
in app end; |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
642 |
|
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
643 |
val theory_attributes = apply_attributes Context.Theory Context.the_theory; |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
644 |
val proof_attributes = apply_attributes Context.Proof Context.the_proof; |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
645 |
|
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
646 |
fun no_attributes x = (x, []); |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
647 |
fun simple_fact x = [(x, [])]; |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
648 |
|
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
649 |
fun tag tg = rule_attribute [] (K (tag_rule tg)); |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
650 |
fun untag s = rule_attribute [] (K (untag_rule s)); |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
651 |
fun kind k = rule_attribute [] (K (k <> "" ? kind_rule k)); |
27866
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
652 |
|
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
653 |
|
70443 | 654 |
|
655 |
(** forked proofs **) |
|
49010 | 656 |
|
49062
7e31dfd99ce7
discontinued complicated/unreliable notion of recent proofs within context;
wenzelm
parents:
49058
diff
changeset
|
657 |
structure Proofs = Theory_Data |
49010 | 658 |
( |
72048
d3b8c8b2d1fc
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
71088
diff
changeset
|
659 |
type T = thm list lazy Inttab.table; |
d3b8c8b2d1fc
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
71088
diff
changeset
|
660 |
val empty = Inttab.empty; |
d3b8c8b2d1fc
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
71088
diff
changeset
|
661 |
val extend = I; |
d3b8c8b2d1fc
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
71088
diff
changeset
|
662 |
val merge = Inttab.merge (K true); |
49010 | 663 |
); |
664 |
||
72048
d3b8c8b2d1fc
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
71088
diff
changeset
|
665 |
fun reset_proofs thy = |
d3b8c8b2d1fc
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
71088
diff
changeset
|
666 |
if Inttab.is_empty (Proofs.get thy) then NONE |
d3b8c8b2d1fc
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
71088
diff
changeset
|
667 |
else SOME (Proofs.put Inttab.empty thy); |
d3b8c8b2d1fc
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
71088
diff
changeset
|
668 |
|
d3b8c8b2d1fc
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
71088
diff
changeset
|
669 |
val _ = Theory.setup (Theory.at_begin reset_proofs); |
61059 | 670 |
|
72048
d3b8c8b2d1fc
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
71088
diff
changeset
|
671 |
fun register_proofs ths thy = |
d3b8c8b2d1fc
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
71088
diff
changeset
|
672 |
let val entry = (serial (), Lazy.map_finished (map Thm.trim_context) ths) |
d3b8c8b2d1fc
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
71088
diff
changeset
|
673 |
in (Proofs.map o Inttab.update) entry thy end; |
d3b8c8b2d1fc
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
71088
diff
changeset
|
674 |
|
d3b8c8b2d1fc
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
71088
diff
changeset
|
675 |
fun force_proofs thy = |
d3b8c8b2d1fc
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
71088
diff
changeset
|
676 |
Proofs.get thy |> Inttab.dest |> maps (map (Thm.transfer thy) o Lazy.force o #2); |
71023
35a8e15b7e03
more robust Thm.expose_theory -- ensure that PIDE export happens in the proper theory context;
wenzelm
parents:
71018
diff
changeset
|
677 |
|
35a8e15b7e03
more robust Thm.expose_theory -- ensure that PIDE export happens in the proper theory context;
wenzelm
parents:
71018
diff
changeset
|
678 |
val consolidate_theory = Thm.consolidate o force_proofs; |
35a8e15b7e03
more robust Thm.expose_theory -- ensure that PIDE export happens in the proper theory context;
wenzelm
parents:
71018
diff
changeset
|
679 |
|
35a8e15b7e03
more robust Thm.expose_theory -- ensure that PIDE export happens in the proper theory context;
wenzelm
parents:
71018
diff
changeset
|
680 |
fun expose_theory thy = |
35a8e15b7e03
more robust Thm.expose_theory -- ensure that PIDE export happens in the proper theory context;
wenzelm
parents:
71018
diff
changeset
|
681 |
if Proofterm.export_enabled () |
35a8e15b7e03
more robust Thm.expose_theory -- ensure that PIDE export happens in the proper theory context;
wenzelm
parents:
71018
diff
changeset
|
682 |
then Thm.expose_proofs thy (force_proofs thy) else (); |
49010 | 683 |
|
684 |
||
61268 | 685 |
|
686 |
(** print theorems **) |
|
687 |
||
688 |
(* options *) |
|
689 |
||
69575 | 690 |
val show_consts = Config.declare_option_bool ("show_consts", \<^here>); |
691 |
val show_hyps = Config.declare_bool ("show_hyps", \<^here>) (K false); |
|
692 |
val show_tags = Config.declare_bool ("show_tags", \<^here>) (K false); |
|
61268 | 693 |
|
694 |
||
695 |
(* pretty_thm etc. *) |
|
696 |
||
697 |
fun pretty_tag (name, arg) = Pretty.strs [name, quote arg]; |
|
698 |
val pretty_tags = Pretty.list "[" "]" o map pretty_tag; |
|
699 |
||
700 |
fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps'} raw_th = |
|
701 |
let |
|
702 |
val show_tags = Config.get ctxt show_tags; |
|
703 |
val show_hyps = Config.get ctxt show_hyps; |
|
704 |
||
705 |
val th = raw_th |
|
67649 | 706 |
|> perhaps (try (Thm.transfer' ctxt)) |
61268 | 707 |
|> perhaps (try Thm.strip_shyps); |
708 |
||
709 |
val hyps = if show_hyps then Thm.hyps_of th else undeclared_hyps (Context.Proof ctxt) th; |
|
61509
358dfae15d83
print thm wrt. local shyps (from full proof context);
wenzelm
parents:
61508
diff
changeset
|
710 |
val extra_shyps = extra_shyps' ctxt th; |
61268 | 711 |
val tags = Thm.get_tags th; |
712 |
val tpairs = Thm.tpairs_of th; |
|
713 |
||
714 |
val q = if quote then Pretty.quote else I; |
|
715 |
val prt_term = q o Syntax.pretty_term ctxt; |
|
716 |
||
717 |
||
718 |
val hlen = length extra_shyps + length hyps + length tpairs; |
|
719 |
val hsymbs = |
|
720 |
if hlen = 0 then [] |
|
721 |
else if show_hyps orelse show_hyps' then |
|
722 |
[Pretty.brk 2, Pretty.list "[" "]" |
|
70443 | 723 |
(map (q o Syntax.pretty_flexpair ctxt) tpairs @ map prt_term hyps @ |
61268 | 724 |
map (Syntax.pretty_sort ctxt) extra_shyps)] |
725 |
else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")]; |
|
726 |
val tsymbs = |
|
727 |
if null tags orelse not show_tags then [] |
|
728 |
else [Pretty.brk 1, pretty_tags tags]; |
|
729 |
in Pretty.block (prt_term (Thm.prop_of th) :: (hsymbs @ tsymbs)) end; |
|
730 |
||
731 |
fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true}; |
|
732 |
fun pretty_thm_item ctxt th = Pretty.item [pretty_thm ctxt th]; |
|
733 |
||
734 |
fun pretty_thm_global thy = |
|
735 |
pretty_thm_raw (Syntax.init_pretty_global thy) {quote = false, show_hyps = false}; |
|
736 |
||
737 |
val string_of_thm = Pretty.string_of oo pretty_thm; |
|
738 |
val string_of_thm_global = Pretty.string_of oo pretty_thm_global; |
|
739 |
||
740 |
||
22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
741 |
open Thm; |
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
742 |
|
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
743 |
end; |
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
744 |
|
32842 | 745 |
structure Basic_Thm: BASIC_THM = Thm; |
746 |
open Basic_Thm; |