author | wenzelm |
Fri, 28 Dec 2018 16:58:27 +0100 | |
changeset 69524 | fa94f2b2a877 |
parent 68036 | 4c9e79aeadf0 |
child 69575 | f77cc54f6d47 |
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 |
|
60938 | 31 |
val all_name: Proof.context -> string * cterm -> cterm -> cterm |
32 |
val all: Proof.context -> cterm -> cterm -> cterm |
|
22907 | 33 |
val mk_binop: cterm -> cterm -> cterm -> cterm |
34 |
val dest_binop: cterm -> cterm * cterm |
|
35 |
val dest_implies: cterm -> cterm * cterm |
|
36 |
val dest_equals: cterm -> cterm * cterm |
|
37 |
val dest_equals_lhs: cterm -> cterm |
|
38 |
val dest_equals_rhs: cterm -> cterm |
|
39 |
val lhs_of: thm -> cterm |
|
40 |
val rhs_of: thm -> cterm |
|
67559 | 41 |
val fast_term_ord: cterm * cterm -> order |
42 |
val term_ord: cterm * cterm -> order |
|
22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
43 |
val thm_ord: thm * thm -> order |
32842 | 44 |
val cterm_cache: (cterm -> 'a) -> cterm -> 'a |
45 |
val thm_cache: (thm -> 'a) -> thm -> 'a |
|
23599 | 46 |
val is_reflexive: thm -> bool |
22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
47 |
val eq_thm: thm * thm -> bool |
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
48 |
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
|
49 |
val eq_thm_strict: thm * thm -> bool |
60817 | 50 |
val equiv_thm: theory -> thm * thm -> bool |
31944 | 51 |
val class_triv: theory -> class -> thm |
52 |
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
|
53 |
val is_dummy: thm -> bool |
22695
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset
|
54 |
val plain_prop_of: thm -> term |
24048
a12b4faff474
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23599
diff
changeset
|
55 |
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
|
56 |
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
|
57 |
val merge_thms: thm list * thm list -> thm list |
33453 | 58 |
val full_rules: thm Item_Net.T |
30560 | 59 |
val intro_rules: thm Item_Net.T |
60 |
val elim_rules: thm Item_Net.T |
|
54984
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset
|
61 |
val declare_hyps: cterm -> Proof.context -> Proof.context |
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset
|
62 |
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
|
63 |
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
|
64 |
val restore_hyps: Proof.context -> Proof.context -> Proof.context |
55633 | 65 |
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
|
66 |
val check_hyps: Context.generic -> thm -> thm |
61508 | 67 |
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
|
68 |
val extra_shyps': Proof.context -> thm -> sort list |
61508 | 69 |
val check_shyps: Proof.context -> thm -> thm |
70 |
val weaken_sorts': Proof.context -> cterm -> cterm |
|
27866
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
71 |
val elim_implies: thm -> thm -> thm |
61339 | 72 |
val forall_intr_name: string * cterm -> thm -> thm |
27866
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
73 |
val forall_elim_var: int -> thm -> thm |
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
74 |
val forall_elim_vars: int -> thm -> thm |
67698
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
75 |
val instantiate_frees: ((string * sort) * ctyp) list * ((string * typ) * cterm) list -> thm -> thm |
60801 | 76 |
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
|
77 |
val forall_intr_frees: thm -> thm |
60825 | 78 |
val unvarify_global: theory -> thm -> thm |
79 |
val unvarify_axiom: theory -> string -> thm |
|
27866
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
80 |
val close_derivation: thm -> 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 |
61268 | 118 |
val show_consts_raw: Config.raw |
119 |
val show_consts: bool Config.T |
|
120 |
val show_hyps_raw: Config.raw |
|
121 |
val show_hyps: bool Config.T |
|
122 |
val show_tags_raw: Config.raw |
|
123 |
val show_tags: bool Config.T |
|
124 |
val pretty_flexpair: Proof.context -> term * term -> Pretty.T |
|
125 |
val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool} -> thm -> Pretty.T |
|
126 |
val pretty_thm: Proof.context -> thm -> Pretty.T |
|
127 |
val pretty_thm_item: Proof.context -> thm -> Pretty.T |
|
128 |
val pretty_thm_global: theory -> thm -> Pretty.T |
|
129 |
val string_of_thm: Proof.context -> thm -> string |
|
130 |
val string_of_thm_global: theory -> thm -> string |
|
22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
131 |
end; |
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
132 |
|
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
133 |
structure Thm: THM = |
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
134 |
struct |
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
135 |
|
22695
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset
|
136 |
(** basic operations **) |
22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
137 |
|
60952
762cb38a3147
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60951
diff
changeset
|
138 |
(* collecting ctyps and cterms *) |
23491 | 139 |
|
60952
762cb38a3147
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60951
diff
changeset
|
140 |
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
|
141 |
val op aconvc = op aconv o apply2 Thm.term_of; |
23491 | 142 |
|
60952
762cb38a3147
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60951
diff
changeset
|
143 |
val add_tvars = Thm.fold_atomic_ctyps (fn a => is_TVar (Thm.typ_of a) ? insert eq_ctyp a); |
60818 | 144 |
val add_frees = Thm.fold_atomic_cterms (fn a => is_Free (Thm.term_of a) ? insert (op aconvc) a); |
145 |
val add_vars = Thm.fold_atomic_cterms (fn a => is_Var (Thm.term_of a) ? insert (op aconvc) a); |
|
23491 | 146 |
|
147 |
||
22907 | 148 |
(* cterm constructors and destructors *) |
149 |
||
60938 | 150 |
fun all_name ctxt (x, t) A = |
32198 | 151 |
let |
59586 | 152 |
val T = Thm.typ_of_cterm t; |
60938 | 153 |
val all_const = Thm.cterm_of ctxt (Const ("Pure.all", (T --> propT) --> propT)); |
154 |
in Thm.apply all_const (Thm.lambda_name (x, t) A) end; |
|
32198 | 155 |
|
60938 | 156 |
fun all ctxt t A = all_name ctxt ("", t) A; |
32198 | 157 |
|
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
|
158 |
fun mk_binop c a b = Thm.apply (Thm.apply c a) b; |
22907 | 159 |
fun dest_binop ct = (Thm.dest_arg1 ct, Thm.dest_arg ct); |
160 |
||
161 |
fun dest_implies ct = |
|
162 |
(case Thm.term_of ct of |
|
56245 | 163 |
Const ("Pure.imp", _) $ _ $ _ => dest_binop ct |
22907 | 164 |
| _ => raise TERM ("dest_implies", [Thm.term_of ct])); |
165 |
||
166 |
fun dest_equals ct = |
|
167 |
(case Thm.term_of ct of |
|
56245 | 168 |
Const ("Pure.eq", _) $ _ $ _ => dest_binop ct |
22907 | 169 |
| _ => raise TERM ("dest_equals", [Thm.term_of ct])); |
170 |
||
171 |
fun dest_equals_lhs ct = |
|
172 |
(case Thm.term_of ct of |
|
56245 | 173 |
Const ("Pure.eq", _) $ _ $ _ => Thm.dest_arg1 ct |
22907 | 174 |
| _ => raise TERM ("dest_equals_lhs", [Thm.term_of ct])); |
175 |
||
176 |
fun dest_equals_rhs ct = |
|
177 |
(case Thm.term_of ct of |
|
56245 | 178 |
Const ("Pure.eq", _) $ _ $ _ => Thm.dest_arg ct |
22907 | 179 |
| _ => raise TERM ("dest_equals_rhs", [Thm.term_of ct])); |
180 |
||
181 |
val lhs_of = dest_equals_lhs o Thm.cprop_of; |
|
182 |
val rhs_of = dest_equals_rhs o Thm.cprop_of; |
|
183 |
||
184 |
||
67559 | 185 |
(* certified term order *) |
186 |
||
187 |
val fast_term_ord = Term_Ord.fast_term_ord o apply2 Thm.term_of; |
|
188 |
val term_ord = Term_Ord.term_ord o apply2 Thm.term_of; |
|
189 |
||
190 |
||
22907 | 191 |
(* thm order: ignores theory context! *) |
22682 | 192 |
|
61039 | 193 |
fun thm_ord ths = |
194 |
(case Term_Ord.fast_term_ord (apply2 Thm.prop_of ths) of |
|
195 |
EQUAL => |
|
196 |
(case |
|
197 |
list_ord (prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord) |
|
198 |
(apply2 Thm.tpairs_of ths) |
|
199 |
of |
|
200 |
EQUAL => |
|
201 |
(case list_ord Term_Ord.fast_term_ord (apply2 Thm.hyps_of ths) of |
|
202 |
EQUAL => list_ord Term_Ord.sort_ord (apply2 Thm.shyps_of ths) |
|
203 |
| ord => ord) |
|
204 |
| ord => ord) |
|
205 |
| ord => ord); |
|
22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
206 |
|
22682 | 207 |
|
32842 | 208 |
(* tables and caches *) |
209 |
||
67559 | 210 |
structure Ctermtab = Table(type key = cterm val ord = fast_term_ord); |
32842 | 211 |
structure Thmtab = Table(type key = thm val ord = thm_ord); |
212 |
||
213 |
fun cterm_cache f = Cache.create Ctermtab.empty Ctermtab.lookup Ctermtab.update f; |
|
214 |
fun thm_cache f = Cache.create Thmtab.empty Thmtab.lookup Thmtab.update f; |
|
215 |
||
216 |
||
22682 | 217 |
(* equality *) |
218 |
||
23599 | 219 |
fun is_reflexive th = op aconv (Logic.dest_equals (Thm.prop_of th)) |
220 |
handle TERM _ => false; |
|
221 |
||
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
|
222 |
val eq_thm = is_equal o thm_ord; |
22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
223 |
|
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58001
diff
changeset
|
224 |
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
|
225 |
|
52683
fb028440473e
more official Thm.eq_thm_strict, without demanding ML equality type;
wenzelm
parents:
51316
diff
changeset
|
226 |
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
|
227 |
eq_thm ths andalso |
65458 | 228 |
Context.eq_thy_id (apply2 Thm.theory_id ths) andalso |
61040 | 229 |
op = (apply2 Thm.maxidx_of ths) andalso |
230 |
op = (apply2 Thm.get_tags ths); |
|
52683
fb028440473e
more official Thm.eq_thm_strict, without demanding ML equality type;
wenzelm
parents:
51316
diff
changeset
|
231 |
|
22682 | 232 |
|
233 |
(* pattern equivalence *) |
|
234 |
||
60817 | 235 |
fun equiv_thm thy ths = |
236 |
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
|
237 |
|
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
238 |
|
31904
a86896359ca4
renamed Drule.sort_triv to Thm.sort_triv (cf. more_thm.ML);
wenzelm
parents:
31177
diff
changeset
|
239 |
(* type classes and sorts *) |
a86896359ca4
renamed Drule.sort_triv to Thm.sort_triv (cf. more_thm.ML);
wenzelm
parents:
31177
diff
changeset
|
240 |
|
31944 | 241 |
fun class_triv thy c = |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59616
diff
changeset
|
242 |
Thm.of_class (Thm.global_ctyp_of thy (TVar ((Name.aT, 0), [c])), c); |
31944 | 243 |
|
244 |
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
|
245 |
|
a60164e8fff0
added check_shyps, which reject pending sort hypotheses;
wenzelm
parents:
28116
diff
changeset
|
246 |
|
22695
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset
|
247 |
(* misc operations *) |
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset
|
248 |
|
24048
a12b4faff474
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23599
diff
changeset
|
249 |
fun is_dummy thm = |
a12b4faff474
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23599
diff
changeset
|
250 |
(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
|
251 |
NONE => false |
58001
934d85f14d1d
more general dummy: may contain "parked arguments", for example;
wenzelm
parents:
56245
diff
changeset
|
252 |
| 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
|
253 |
|
22695
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset
|
254 |
fun plain_prop_of raw_thm = |
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset
|
255 |
let |
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset
|
256 |
val thm = Thm.strip_shyps raw_thm; |
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset
|
257 |
fun err msg = raise THM ("plain_prop_of: " ^ msg, 0, [thm]); |
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset
|
258 |
in |
61039 | 259 |
if not (null (Thm.hyps_of thm)) then |
22695
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset
|
260 |
err "theorem may not contain hypotheses" |
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset
|
261 |
else if not (null (Thm.extra_shyps thm)) then |
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset
|
262 |
err "theorem may not contain sort hypotheses" |
61039 | 263 |
else if not (null (Thm.tpairs_of thm)) then |
22695
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset
|
264 |
err "theorem may not contain flex-flex pairs" |
61039 | 265 |
else Thm.prop_of thm |
22695
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset
|
266 |
end; |
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset
|
267 |
|
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset
|
268 |
|
30564 | 269 |
(* 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
|
270 |
|
a12b4faff474
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23599
diff
changeset
|
271 |
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
|
272 |
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
|
273 |
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
|
274 |
|
33453 | 275 |
val full_rules = Item_Net.init eq_thm_prop (single o Thm.full_prop_of); |
33373 | 276 |
val intro_rules = Item_Net.init eq_thm_prop (single o Thm.concl_of); |
277 |
val elim_rules = Item_Net.init eq_thm_prop (single o Thm.major_prem_of); |
|
30560 | 278 |
|
279 |
||
22682 | 280 |
|
61508 | 281 |
(** declared hyps and sort hyps **) |
54984
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset
|
282 |
|
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset
|
283 |
structure Hyps = Proof_Data |
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset
|
284 |
( |
61508 | 285 |
type T = {checked_hyps: bool, hyps: Termtab.set, shyps: sort Ord_List.T}; |
286 |
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
|
287 |
); |
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset
|
288 |
|
61508 | 289 |
fun map_hyps f = Hyps.map (fn {checked_hyps, hyps, shyps} => |
290 |
let val (checked_hyps', hyps', shyps') = f (checked_hyps, hyps, shyps) |
|
291 |
in {checked_hyps = checked_hyps', hyps = hyps', shyps = shyps'} end); |
|
292 |
||
293 |
||
294 |
(* hyps *) |
|
295 |
||
296 |
fun declare_hyps raw_ct ctxt = ctxt |> map_hyps (fn (checked_hyps, hyps, shyps) => |
|
297 |
let |
|
298 |
val ct = Thm.transfer_cterm (Proof_Context.theory_of ctxt) raw_ct; |
|
299 |
val hyps' = Termtab.update (Thm.term_of ct, ()) hyps; |
|
300 |
in (checked_hyps, hyps', shyps) end); |
|
54984
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset
|
301 |
|
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset
|
302 |
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
|
303 |
|
61508 | 304 |
val unchecked_hyps = map_hyps (fn (_, hyps, shyps) => (false, hyps, shyps)); |
305 |
||
306 |
fun restore_hyps ctxt = |
|
307 |
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
|
308 |
|
55633 | 309 |
fun undeclared_hyps context th = |
310 |
Thm.hyps_of th |
|
311 |
|> filter_out |
|
312 |
(case context of |
|
313 |
Context.Theory _ => K false |
|
314 |
| Context.Proof ctxt => |
|
315 |
(case Hyps.get ctxt of |
|
61508 | 316 |
{checked_hyps = false, ...} => K true |
317 |
| {hyps, ...} => Termtab.defined hyps)); |
|
55633 | 318 |
|
54993
625370769fc0
check_hyps for attribute application (still inactive, due to non-compliant tools);
wenzelm
parents:
54984
diff
changeset
|
319 |
fun check_hyps context th = |
55633 | 320 |
(case undeclared_hyps context th of |
321 |
[] => th |
|
322 |
| undeclared => |
|
61263 | 323 |
error (Pretty.string_of (Pretty.big_list "Undeclared hyps:" |
324 |
(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
|
325 |
|
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset
|
326 |
|
61508 | 327 |
(* shyps *) |
328 |
||
329 |
fun declare_term_sorts t = |
|
330 |
map_hyps (fn (checked_hyps, hyps, shyps) => |
|
331 |
(checked_hyps, hyps, Sorts.insert_term t shyps)); |
|
332 |
||
61509
358dfae15d83
print thm wrt. local shyps (from full proof context);
wenzelm
parents:
61508
diff
changeset
|
333 |
fun extra_shyps' ctxt th = |
358dfae15d83
print thm wrt. local shyps (from full proof context);
wenzelm
parents:
61508
diff
changeset
|
334 |
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
|
335 |
|
61508 | 336 |
fun check_shyps ctxt raw_th = |
337 |
let |
|
338 |
val th = Thm.strip_shyps raw_th; |
|
61509
358dfae15d83
print thm wrt. local shyps (from full proof context);
wenzelm
parents:
61508
diff
changeset
|
339 |
val extra_shyps = extra_shyps' ctxt th; |
61508 | 340 |
in |
61509
358dfae15d83
print thm wrt. local shyps (from full proof context);
wenzelm
parents:
61508
diff
changeset
|
341 |
if null extra_shyps then th |
61508 | 342 |
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
|
343 |
Pretty.brk 1 :: Pretty.commas (map (Syntax.pretty_sort ctxt) extra_shyps)))) |
61508 | 344 |
end; |
345 |
||
346 |
val weaken_sorts' = Thm.weaken_sorts o #shyps o Hyps.get; |
|
347 |
||
348 |
||
54984
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset
|
349 |
|
24980
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
350 |
(** basic derived rules **) |
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
351 |
|
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
352 |
(*Elimination of implication |
67721 | 353 |
A A \<Longrightarrow> B |
24980
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
354 |
------------ |
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
355 |
B |
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
356 |
*) |
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
357 |
fun elim_implies thA thAB = Thm.implies_elim thAB thA; |
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
358 |
|
26653 | 359 |
|
61339 | 360 |
(* forall_intr_name *) |
361 |
||
362 |
fun forall_intr_name (a, x) th = |
|
363 |
let |
|
364 |
val th' = Thm.forall_intr x th; |
|
365 |
val prop' = (case Thm.prop_of th' of all $ Abs (_, T, b) => all $ Abs (a, T, b)); |
|
366 |
in Thm.renamed_prop prop' th' end; |
|
367 |
||
368 |
||
26653 | 369 |
(* forall_elim_var(s) *) |
370 |
||
371 |
local |
|
372 |
||
60951
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset
|
373 |
fun dest_all ct = |
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset
|
374 |
(case Thm.term_of ct of |
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset
|
375 |
Const ("Pure.all", _) $ Abs (a, _, _) => |
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset
|
376 |
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
|
377 |
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
|
378 |
| _ => NONE); |
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset
|
379 |
|
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset
|
380 |
fun dest_all_list ct = |
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset
|
381 |
(case dest_all ct of |
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset
|
382 |
NONE => [] |
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset
|
383 |
| 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
|
384 |
|
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset
|
385 |
fun forall_elim_vars_list vars i th = |
26653 | 386 |
let |
60950 | 387 |
val used = |
388 |
(Thm.fold_terms o Term.fold_aterms) |
|
389 |
(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
|
390 |
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
|
391 |
|> 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
|
392 |
in fold Thm.forall_elim vars' th end; |
26653 | 393 |
|
394 |
in |
|
395 |
||
60950 | 396 |
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
|
397 |
forall_elim_vars_list (dest_all_list (Thm.cprop_of th)) i th; |
26653 | 398 |
|
33697 | 399 |
fun forall_elim_var i th = |
60950 | 400 |
let |
401 |
val vars = |
|
60951
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset
|
402 |
(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
|
403 |
SOME (v, _) => [v] |
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset
|
404 |
| 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
|
405 |
in forall_elim_vars_list vars i th end; |
26653 | 406 |
|
407 |
end; |
|
408 |
||
409 |
||
67698
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
410 |
(* instantiate frees *) |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
411 |
|
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
412 |
fun instantiate_frees ([], []) th = th |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
413 |
| instantiate_frees (instT, inst) th = |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
414 |
let |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
415 |
val idx = Thm.maxidx_of th + 1; |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
416 |
fun index ((a, A), b) = (((a, idx), A), b); |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
417 |
val insts = (map index instT, map index inst); |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
418 |
val frees = (map (#1 o #1) instT, map (#1 o #1) inst); |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
419 |
|
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
420 |
val hyps = Thm.chyps_of th; |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
421 |
val inst_cterm = |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
422 |
Thm.generalize_cterm frees idx #> |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
423 |
Thm.instantiate_cterm insts; |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
424 |
in |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
425 |
th |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
426 |
|> fold_rev Thm.implies_intr hyps |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
427 |
|> Thm.generalize frees idx |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
428 |
|> Thm.instantiate insts |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
429 |
|> 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
|
430 |
end; |
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
431 |
|
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset
|
432 |
|
60801 | 433 |
(* instantiate by left-to-right occurrence of variables *) |
434 |
||
435 |
fun instantiate' cTs cts thm = |
|
436 |
let |
|
437 |
fun err msg = |
|
438 |
raise TYPE ("instantiate': " ^ msg, |
|
439 |
map_filter (Option.map Thm.typ_of) cTs, |
|
440 |
map_filter (Option.map Thm.term_of) cts); |
|
441 |
||
442 |
fun zip_vars xs ys = |
|
443 |
zip_options xs ys handle ListPair.UnequalLengths => |
|
444 |
err "more instantiations than variables in thm"; |
|
445 |
||
446 |
val thm' = |
|
447 |
Thm.instantiate ((zip_vars (rev (Thm.fold_terms Term.add_tvars thm [])) cTs), []) thm; |
|
448 |
val thm'' = |
|
449 |
Thm.instantiate ([], zip_vars (rev (Thm.fold_terms Term.add_vars thm' [])) cts) thm'; |
|
450 |
in thm'' end; |
|
451 |
||
452 |
||
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
|
453 |
(* 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
|
454 |
|
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
|
455 |
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
|
456 |
let |
61041 | 457 |
val fixed = |
458 |
fold Term.add_frees (Thm.terms_of_tpairs (Thm.tpairs_of th) @ Thm.hyps_of th) []; |
|
60821 | 459 |
val frees = |
460 |
Thm.fold_atomic_cterms (fn a => |
|
461 |
(case Thm.term_of a of |
|
462 |
Free v => not (member (op =) fixed v) ? insert (op aconvc) a |
|
463 |
| _ => I)) th []; |
|
464 |
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
|
465 |
|
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
|
466 |
|
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
|
467 |
(* unvarify_global: global schematic variables *) |
26653 | 468 |
|
60825 | 469 |
fun unvarify_global thy th = |
24980
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
470 |
let |
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
471 |
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
|
472 |
val _ = map Logic.unvarify_global (prop :: Thm.hyps_of th) |
24980
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
473 |
handle TERM (msg, _) => raise THM (msg, 0, [th]); |
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
474 |
|
32279 | 475 |
val instT = rev (Term.add_tvars prop []) |> map (fn v as ((a, _), S) => (v, TFree (a, S))); |
24980
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
476 |
val inst = rev (Term.add_vars prop []) |> map (fn ((a, i), T) => |
32279 | 477 |
let val T' = Term_Subst.instantiateT instT T |
60805 | 478 |
in (((a, i), T'), Thm.global_cterm_of thy (Free ((a, T')))) end); |
479 |
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
|
480 |
|
60825 | 481 |
fun unvarify_axiom thy = unvarify_global thy o Thm.axiom thy; |
482 |
||
26653 | 483 |
|
484 |
(* close_derivation *) |
|
485 |
||
26628
63306cb94313
replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
wenzelm
parents:
25518
diff
changeset
|
486 |
fun close_derivation thm = |
64568
a504a3dec35a
more careful derivation_closed / close_derivation;
wenzelm
parents:
64556
diff
changeset
|
487 |
if Thm.derivation_closed thm then thm else Thm.name_derivation "" thm; |
26628
63306cb94313
replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
wenzelm
parents:
25518
diff
changeset
|
488 |
|
24980
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
489 |
|
59969
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
490 |
(* user renaming of parameters in a subgoal *) |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
491 |
|
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
492 |
(*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
|
493 |
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
|
494 |
fun rename_params_rule (names, i) st = |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
495 |
let |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
496 |
val (_, Bs, Bi, C) = Thm.dest_state (st, i); |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
497 |
val params = map #1 (Logic.strip_params Bi); |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
498 |
val short = length params - length names; |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
499 |
val names' = |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
500 |
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
|
501 |
else Name.variant_list names (take short params) @ names; |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
502 |
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
|
503 |
val Bi' = Logic.list_rename_params names' Bi; |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
504 |
in |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
505 |
(case duplicates (op =) names of |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
506 |
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
|
507 |
| [] => |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
508 |
(case inter (op =) names free_names of |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
509 |
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
|
510 |
| [] => 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
|
511 |
end; |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
512 |
|
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
513 |
|
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
514 |
(* preservation of bound variable names *) |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
515 |
|
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
516 |
fun rename_boundvars pat obj th = |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
517 |
(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
|
518 |
NONE => th |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
519 |
| SOME prop' => Thm.renamed_prop prop' th); |
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
520 |
|
bcccad156236
explicitly checked alpha conversion -- actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset
|
521 |
|
24980
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
522 |
|
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
523 |
(** specification primitives **) |
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
524 |
|
30342 | 525 |
(* rules *) |
526 |
||
35855
e7d004b89ca8
add_axiom: axiomatize "unconstrained" version, with explicit of_class premises;
wenzelm
parents:
35853
diff
changeset
|
527 |
fun stripped_sorts thy t = |
e7d004b89ca8
add_axiom: axiomatize "unconstrained" version, with explicit of_class premises;
wenzelm
parents:
35853
diff
changeset
|
528 |
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
|
529 |
val tfrees = rev (Term.add_tfrees t []); |
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
|
530 |
val tfrees' = map (fn a => (a, [])) (Name.invent Name.context Name.aT (length 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
|
531 |
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
|
532 |
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
|
533 |
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
|
534 |
val strip = map (apply2 TFree) (tfrees ~~ tfrees'); |
35855
e7d004b89ca8
add_axiom: axiomatize "unconstrained" version, with explicit of_class premises;
wenzelm
parents:
35853
diff
changeset
|
535 |
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
|
536 |
in (strip, recover, t') end; |
e7d004b89ca8
add_axiom: axiomatize "unconstrained" version, with explicit of_class premises;
wenzelm
parents:
35853
diff
changeset
|
537 |
|
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
40238
diff
changeset
|
538 |
fun add_axiom ctxt (b, prop) thy = |
24980
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
539 |
let |
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
40238
diff
changeset
|
540 |
val _ = Sign.no_vars ctxt prop; |
35855
e7d004b89ca8
add_axiom: axiomatize "unconstrained" version, with explicit of_class premises;
wenzelm
parents:
35853
diff
changeset
|
541 |
val (strip, recover, prop') = stripped_sorts thy prop; |
e7d004b89ca8
add_axiom: axiomatize "unconstrained" version, with explicit of_class premises;
wenzelm
parents:
35853
diff
changeset
|
542 |
val constraints = map (fn (TFree (_, S), T) => (T, S)) strip; |
60367 | 543 |
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
|
544 |
|
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
40238
diff
changeset
|
545 |
val thy' = thy |
51316
dfe469293eb4
discontinued empty name bindings in 'axiomatization';
wenzelm
parents:
49062
diff
changeset
|
546 |
|> 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
|
547 |
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
|
548 |
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
|
549 |
val thm = |
76ca601c941e
disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
wenzelm
parents:
35985
diff
changeset
|
550 |
Thm.instantiate (recover, []) axm' |
60825 | 551 |
|> unvarify_global thy' |
35988
76ca601c941e
disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
wenzelm
parents:
35985
diff
changeset
|
552 |
|> fold elim_implies of_sorts; |
36106
19deea200358
Thm.add_axiom/add_def: return internal name of foundational axiom;
wenzelm
parents:
35988
diff
changeset
|
553 |
in ((axm_name, thm), thy') end; |
24980
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
554 |
|
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
40238
diff
changeset
|
555 |
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
|
556 |
|
61261
ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
61059
diff
changeset
|
557 |
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
|
558 |
let |
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
40238
diff
changeset
|
559 |
val _ = Sign.no_vars ctxt prop; |
60367 | 560 |
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
|
561 |
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
|
562 |
|
61261
ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
61059
diff
changeset
|
563 |
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
|
564 |
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
|
565 |
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
|
566 |
val thm = |
76ca601c941e
disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
wenzelm
parents:
35985
diff
changeset
|
567 |
Thm.instantiate (recover, []) axm' |
60825 | 568 |
|> unvarify_global thy' |
35988
76ca601c941e
disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
wenzelm
parents:
35985
diff
changeset
|
569 |
|> fold_rev Thm.implies_intr prems; |
36106
19deea200358
Thm.add_axiom/add_def: return internal name of foundational axiom;
wenzelm
parents:
35988
diff
changeset
|
570 |
in ((axm_name, thm), thy') end; |
24980
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset
|
571 |
|
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
40238
diff
changeset
|
572 |
fun add_def_global unchecked overloaded arg thy = |
61262
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61261
diff
changeset
|
573 |
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
|
574 |
|
27866
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
575 |
|
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
576 |
|
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
577 |
(*** theorem tags ***) |
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
578 |
|
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
579 |
(* add / delete tags *) |
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
580 |
|
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
581 |
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
|
582 |
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
|
583 |
|
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
584 |
|
61852 | 585 |
(* free dummy thm -- for abstract closure *) |
586 |
||
587 |
val free_dummyN = "free_dummy"; |
|
588 |
fun is_free_dummy thm = Properties.defined (Thm.get_tags thm) free_dummyN; |
|
589 |
val tag_free_dummy = tag_rule (free_dummyN, ""); |
|
590 |
||
591 |
||
30342 | 592 |
(* def_name *) |
593 |
||
594 |
fun def_name c = c ^ "_def"; |
|
595 |
||
596 |
fun def_name_optional c "" = def_name c |
|
597 |
| def_name_optional _ name = name; |
|
598 |
||
63041
cb495c4807b3
clarified def binding position: reset for implicit/derived binding, keep for explicit binding;
wenzelm
parents:
62093
diff
changeset
|
599 |
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
|
600 |
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
|
601 |
fun make_def_binding cond b = if cond then def_binding b else Binding.empty; |
62093 | 602 |
|
30342 | 603 |
|
27866
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
604 |
(* unofficial theorem names *) |
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
605 |
|
68036
4c9e79aeadf0
tuned -- avoid spurious exception trace for "the";
wenzelm
parents:
67778
diff
changeset
|
606 |
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
|
607 |
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
|
608 |
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
|
609 |
|
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
610 |
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
|
611 |
|
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
612 |
|
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
613 |
(* theorem kinds *) |
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
614 |
|
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
615 |
val theoremK = "theorem"; |
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
616 |
|
42473 | 617 |
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
|
618 |
|
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
619 |
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
|
620 |
|
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 |
|
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 |
|
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 |
(** 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
|
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 |
(*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
|
626 |
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
|
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 |
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
|
629 |
|
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 |
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
|
631 |
(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
|
632 |
(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
|
633 |
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
|
634 |
| 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
|
635 |
|
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 |
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
|
637 |
(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
|
638 |
|
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 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
|
640 |
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
|
641 |
|
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 |
fun apply_attribute (att: attribute) th x = |
67649 | 643 |
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
|
644 |
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
|
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 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
|
647 |
|
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 |
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
|
649 |
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
|
650 |
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
|
651 |
| 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
|
652 |
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
|
653 |
|
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
|
654 |
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
|
655 |
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
|
656 |
|
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
|
657 |
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
|
658 |
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
|
659 |
|
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
|
660 |
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
|
661 |
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
|
662 |
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
|
663 |
|
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset
|
664 |
|
49011
9c68e43502ce
some support for registering forked proofs within Proof.state, using its bottom context;
wenzelm
parents:
49010
diff
changeset
|
665 |
(* forked proofs *) |
49010 | 666 |
|
49062
7e31dfd99ce7
discontinued complicated/unreliable notion of recent proofs within context;
wenzelm
parents:
49058
diff
changeset
|
667 |
structure Proofs = Theory_Data |
49010 | 668 |
( |
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
|
669 |
type T = thm list lazy list; |
49062
7e31dfd99ce7
discontinued complicated/unreliable notion of recent proofs within context;
wenzelm
parents:
49058
diff
changeset
|
670 |
val empty = []; |
49010 | 671 |
fun extend _ = empty; |
672 |
fun merge _ = empty; |
|
673 |
); |
|
674 |
||
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
|
675 |
fun register_proofs ths = |
857da80611ab
support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes;
wenzelm
parents:
67649
diff
changeset
|
676 |
(Proofs.map o cons) (Lazy.map_finished (map Thm.trim_context) ths); |
61059 | 677 |
|
64574
1134e4d5e5b7
consolidate nested thms with persistent result, for improved performance;
wenzelm
parents:
64568
diff
changeset
|
678 |
fun consolidate_theory thy = |
67778
a25f9076a0b3
eliminated somewhat pointless parallelism (from 857da80611ab): usually hundreds of tasks with < 1ms each, also note that the enclosing join_theory happens within theory graph parallelism;
wenzelm
parents:
67725
diff
changeset
|
679 |
rev (Proofs.get thy) |
a25f9076a0b3
eliminated somewhat pointless parallelism (from 857da80611ab): usually hundreds of tasks with < 1ms each, also note that the enclosing join_theory happens within theory graph parallelism;
wenzelm
parents:
67725
diff
changeset
|
680 |
|> maps (map (Thm.transfer thy) o Lazy.force) |
a25f9076a0b3
eliminated somewhat pointless parallelism (from 857da80611ab): usually hundreds of tasks with < 1ms each, also note that the enclosing join_theory happens within theory graph parallelism;
wenzelm
parents:
67725
diff
changeset
|
681 |
|> Thm.consolidate; |
49010 | 682 |
|
683 |
||
61268 | 684 |
|
685 |
(** print theorems **) |
|
686 |
||
687 |
(* options *) |
|
688 |
||
64556 | 689 |
val show_consts_raw = Config.declare_option ("show_consts", \<^here>); |
61268 | 690 |
val show_consts = Config.bool show_consts_raw; |
691 |
||
64556 | 692 |
val show_hyps_raw = Config.declare ("show_hyps", \<^here>) (fn _ => Config.Bool false); |
61268 | 693 |
val show_hyps = Config.bool show_hyps_raw; |
694 |
||
64556 | 695 |
val show_tags_raw = Config.declare ("show_tags", \<^here>) (fn _ => Config.Bool false); |
61268 | 696 |
val show_tags = Config.bool show_tags_raw; |
697 |
||
698 |
||
699 |
(* pretty_thm etc. *) |
|
700 |
||
701 |
fun pretty_tag (name, arg) = Pretty.strs [name, quote arg]; |
|
702 |
val pretty_tags = Pretty.list "[" "]" o map pretty_tag; |
|
703 |
||
704 |
fun pretty_flexpair ctxt (t, u) = Pretty.block |
|
67725 | 705 |
[Syntax.pretty_term ctxt t, Pretty.str " \<equiv>\<^sup>?", Pretty.brk 1, Syntax.pretty_term ctxt u]; |
61268 | 706 |
|
707 |
fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps'} raw_th = |
|
708 |
let |
|
709 |
val show_tags = Config.get ctxt show_tags; |
|
710 |
val show_hyps = Config.get ctxt show_hyps; |
|
711 |
||
712 |
val th = raw_th |
|
67649 | 713 |
|> perhaps (try (Thm.transfer' ctxt)) |
61268 | 714 |
|> perhaps (try Thm.strip_shyps); |
715 |
||
716 |
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
|
717 |
val extra_shyps = extra_shyps' ctxt th; |
61268 | 718 |
val tags = Thm.get_tags th; |
719 |
val tpairs = Thm.tpairs_of th; |
|
720 |
||
721 |
val q = if quote then Pretty.quote else I; |
|
722 |
val prt_term = q o Syntax.pretty_term ctxt; |
|
723 |
||
724 |
||
725 |
val hlen = length extra_shyps + length hyps + length tpairs; |
|
726 |
val hsymbs = |
|
727 |
if hlen = 0 then [] |
|
728 |
else if show_hyps orelse show_hyps' then |
|
729 |
[Pretty.brk 2, Pretty.list "[" "]" |
|
730 |
(map (q o pretty_flexpair ctxt) tpairs @ map prt_term hyps @ |
|
731 |
map (Syntax.pretty_sort ctxt) extra_shyps)] |
|
732 |
else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")]; |
|
733 |
val tsymbs = |
|
734 |
if null tags orelse not show_tags then [] |
|
735 |
else [Pretty.brk 1, pretty_tags tags]; |
|
736 |
in Pretty.block (prt_term (Thm.prop_of th) :: (hsymbs @ tsymbs)) end; |
|
737 |
||
738 |
fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true}; |
|
739 |
fun pretty_thm_item ctxt th = Pretty.item [pretty_thm ctxt th]; |
|
740 |
||
741 |
fun pretty_thm_global thy = |
|
742 |
pretty_thm_raw (Syntax.init_pretty_global thy) {quote = false, show_hyps = false}; |
|
743 |
||
744 |
val string_of_thm = Pretty.string_of oo pretty_thm; |
|
745 |
val string_of_thm_global = Pretty.string_of oo pretty_thm_global; |
|
746 |
||
747 |
||
22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
748 |
open Thm; |
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
749 |
|
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
750 |
end; |
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset
|
751 |
|
32842 | 752 |
structure Basic_Thm: BASIC_THM = Thm; |
753 |
open Basic_Thm; |