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