author | wenzelm |
Tue, 21 Sep 2021 13:12:14 +0200 | |
changeset 74341 | edf8b141a8c4 |
parent 74340 | e098fa45bfe0 |
child 74344 | 1c2c0380d58b |
permissions | -rw-r--r-- |
11897 | 1 |
(* Title: Pure/Isar/object_logic.ML |
2 |
Author: Markus Wenzel, TU Muenchen |
|
3 |
||
4 |
Specifics about common object-logics. |
|
5 |
*) |
|
6 |
||
7 |
signature OBJECT_LOGIC = |
|
8 |
sig |
|
59970 | 9 |
val get_base_sort: Proof.context -> sort option |
25497 | 10 |
val add_base_sort: sort -> theory -> theory |
30344
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
29606
diff
changeset
|
11 |
val add_judgment: binding * typ * mixfix -> theory -> theory |
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
29606
diff
changeset
|
12 |
val add_judgment_cmd: binding * string * mixfix -> theory -> theory |
59970 | 13 |
val judgment_name: Proof.context -> string |
74341 | 14 |
val judgment_const: Proof.context -> string * typ |
59970 | 15 |
val is_judgment: Proof.context -> term -> bool |
16 |
val drop_judgment: Proof.context -> term -> term |
|
17 |
val fixed_judgment: Proof.context -> string -> term |
|
18 |
val ensure_propT: Proof.context -> term -> term |
|
19 |
val dest_judgment: Proof.context -> cterm -> cterm |
|
20 |
val judgment_conv: Proof.context -> conv -> conv |
|
69988 | 21 |
val is_propositional: Proof.context -> typ -> bool |
59970 | 22 |
val elim_concl: Proof.context -> thm -> term option |
18728 | 23 |
val declare_atomize: attribute |
24 |
val declare_rulify: attribute |
|
59970 | 25 |
val atomize_term: Proof.context -> term -> term |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
26 |
val atomize: Proof.context -> conv |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
27 |
val atomize_prems: Proof.context -> conv |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
28 |
val atomize_prems_tac: Proof.context -> int -> tactic |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
29 |
val full_atomize_tac: Proof.context -> int -> tactic |
59970 | 30 |
val rulify_term: Proof.context -> term -> term |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
31 |
val rulify_tac: Proof.context -> int -> tactic |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
32 |
val rulify: Proof.context -> thm -> thm |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
33 |
val rulify_no_asm: Proof.context -> thm -> thm |
18728 | 34 |
val rule_format: attribute |
35 |
val rule_format_no_asm: attribute |
|
11897 | 36 |
end; |
37 |
||
35625 | 38 |
structure Object_Logic: OBJECT_LOGIC = |
11897 | 39 |
struct |
40 |
||
59970 | 41 |
(** context data **) |
11897 | 42 |
|
25497 | 43 |
datatype data = Data of |
44 |
{base_sort: sort option, |
|
45 |
judgment: string option, |
|
46 |
atomize_rulify: thm list * thm list}; |
|
47 |
||
48 |
fun make_data (base_sort, judgment, atomize_rulify) = |
|
49 |
Data {base_sort = base_sort, judgment = judgment, atomize_rulify = atomize_rulify}; |
|
11897 | 50 |
|
59970 | 51 |
structure Data = Generic_Data |
22846 | 52 |
( |
25497 | 53 |
type T = data; |
54 |
val empty = make_data (NONE, NONE, ([], [])); |
|
16449 | 55 |
val extend = I; |
11897 | 56 |
|
25497 | 57 |
fun merge_opt eq (SOME x, SOME y) = |
58 |
if eq (x, y) then SOME x else error "Attempt to merge different object-logics" |
|
41493 | 59 |
| merge_opt _ data = merge_options data; |
11897 | 60 |
|
33522 | 61 |
fun merge |
25497 | 62 |
(Data {base_sort = base_sort1, judgment = judgment1, atomize_rulify = (atomize1, rulify1)}, |
63 |
Data {base_sort = base_sort2, judgment = judgment2, atomize_rulify = (atomize2, rulify2)}) = |
|
64 |
make_data (merge_opt (op =) (base_sort1, base_sort2), merge_opt (op =) (judgment1, judgment2), |
|
24039
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23602
diff
changeset
|
65 |
(Thm.merge_thms (atomize1, atomize2), Thm.merge_thms (rulify1, rulify2))); |
22846 | 66 |
); |
15801 | 67 |
|
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36610
diff
changeset
|
68 |
fun map_data f = Data.map (fn (Data {base_sort, judgment, atomize_rulify}) => |
25497 | 69 |
make_data (f (base_sort, judgment, atomize_rulify))); |
70 |
||
59970 | 71 |
fun get_data ctxt = Data.get (Context.Proof ctxt) |> (fn Data args => args); |
25497 | 72 |
|
11897 | 73 |
|
74 |
||
75 |
(** generic treatment of judgments -- with a single argument only **) |
|
76 |
||
25497 | 77 |
(* base_sort *) |
78 |
||
79 |
val get_base_sort = #base_sort o get_data; |
|
80 |
||
59970 | 81 |
fun add_base_sort S = |
82 |
(Context.theory_map o map_data) (fn (base_sort, judgment, atomize_rulify) => |
|
83 |
if is_some base_sort then error "Attempt to redeclare object-logic base sort" |
|
84 |
else (SOME S, judgment, atomize_rulify)); |
|
25497 | 85 |
|
86 |
||
18825 | 87 |
(* add judgment *) |
11897 | 88 |
|
89 |
local |
|
90 |
||
30344
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
29606
diff
changeset
|
91 |
fun gen_add_judgment add_consts (b, T, mx) thy = |
61255
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61246
diff
changeset
|
92 |
let |
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61246
diff
changeset
|
93 |
val c = Sign.full_name thy b; |
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61246
diff
changeset
|
94 |
val thy' = thy |> add_consts [(b, T, mx)]; |
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61246
diff
changeset
|
95 |
in |
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61246
diff
changeset
|
96 |
thy' |
74340
e098fa45bfe0
proper Sign.const_typargs via Theory.add_deps_const/Theory.const_dep;
wenzelm
parents:
70471
diff
changeset
|
97 |
|> Theory.add_deps_const c |
59970 | 98 |
|> (Context.theory_map o map_data) (fn (base_sort, judgment, atomize_rulify) => |
25497 | 99 |
if is_some judgment then error "Attempt to redeclare object-logic judgment" |
100 |
else (base_sort, SOME c, atomize_rulify)) |
|
14226 | 101 |
end; |
11897 | 102 |
|
103 |
in |
|
104 |
||
56239 | 105 |
val add_judgment = gen_add_judgment Sign.add_consts; |
106 |
val add_judgment_cmd = gen_add_judgment Sign.add_consts_cmd; |
|
11897 | 107 |
|
108 |
end; |
|
109 |
||
110 |
||
23566
b65692d4adcd
replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;
wenzelm
parents:
23540
diff
changeset
|
111 |
(* judgments *) |
11897 | 112 |
|
59970 | 113 |
fun judgment_name ctxt = |
114 |
(case #judgment (get_data ctxt) of |
|
25497 | 115 |
SOME name => name |
11897 | 116 |
| _ => raise TERM ("Unknown object-logic judgment", [])); |
117 |
||
74341 | 118 |
fun judgment_const ctxt = |
119 |
let |
|
120 |
val thy = Proof_Context.theory_of ctxt; |
|
121 |
val c = judgment_name ctxt; |
|
122 |
val T = Sign.the_const_type thy c; |
|
123 |
in (c, T) end; |
|
124 |
||
59970 | 125 |
fun is_judgment ctxt (Const (c, _) $ _) = c = judgment_name ctxt |
11897 | 126 |
| is_judgment _ _ = false; |
127 |
||
59970 | 128 |
fun drop_judgment ctxt (Abs (x, T, t)) = Abs (x, T, drop_judgment ctxt t) |
129 |
| drop_judgment ctxt (tm as (Const (c, _) $ t)) = |
|
130 |
if (c = judgment_name ctxt handle TERM _ => false) then t else tm |
|
11897 | 131 |
| drop_judgment _ tm = tm; |
132 |
||
59970 | 133 |
fun fixed_judgment ctxt x = |
11897 | 134 |
let (*be robust wrt. low-level errors*) |
59970 | 135 |
val c = judgment_name ctxt; |
70387 | 136 |
val aT = Term.aT []; |
11897 | 137 |
val T = |
59970 | 138 |
the_default (aT --> propT) (Sign.const_type (Proof_Context.theory_of ctxt) c) |
60443 | 139 |
|> Term.map_type_tvar (fn ((a, _), S) => TFree (a, S)); |
11897 | 140 |
val U = Term.domain_type T handle Match => aT; |
141 |
in Const (c, T) $ Free (x, U) end; |
|
142 |
||
59970 | 143 |
fun ensure_propT ctxt t = |
13376 | 144 |
let val T = Term.fastype_of t |
59970 | 145 |
in if T = propT then t else Const (judgment_name ctxt, T --> propT) $ t end; |
13376 | 146 |
|
59970 | 147 |
fun dest_judgment ctxt ct = |
148 |
if is_judgment ctxt (Thm.term_of ct) |
|
23586 | 149 |
then Thm.dest_arg ct |
150 |
else raise CTERM ("dest_judgment", [ct]); |
|
151 |
||
59970 | 152 |
fun judgment_conv ctxt cv ct = |
153 |
if is_judgment ctxt (Thm.term_of ct) |
|
23566
b65692d4adcd
replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;
wenzelm
parents:
23540
diff
changeset
|
154 |
then Conv.arg_conv cv ct |
b65692d4adcd
replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;
wenzelm
parents:
23540
diff
changeset
|
155 |
else raise CTERM ("judgment_conv", [ct]); |
b65692d4adcd
replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;
wenzelm
parents:
23540
diff
changeset
|
156 |
|
69988 | 157 |
fun is_propositional ctxt T = |
158 |
T = propT orelse |
|
159 |
let val x = Free (singleton (Variable.variant_frees ctxt []) ("x", T)) |
|
160 |
in can (fn () => Syntax.check_term ctxt (ensure_propT ctxt x)) () end; |
|
161 |
||
11897 | 162 |
|
19261 | 163 |
(* elimination rules *) |
164 |
||
59970 | 165 |
fun elim_concl ctxt rule = |
19261 | 166 |
let |
167 |
val concl = Thm.concl_of rule; |
|
59970 | 168 |
val C = drop_judgment ctxt concl; |
19261 | 169 |
in |
41581
72a02e3dec7e
clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents:
41493
diff
changeset
|
170 |
if Term.is_Var C andalso |
19261 | 171 |
exists (fn prem => concl aconv Logic.strip_assums_concl prem) (Thm.prems_of rule) |
41581
72a02e3dec7e
clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents:
41493
diff
changeset
|
172 |
then SOME C else NONE |
19261 | 173 |
end; |
174 |
||
175 |
||
11897 | 176 |
|
177 |
(** treatment of meta-level connectives **) |
|
178 |
||
179 |
(* maintain rules *) |
|
180 |
||
70471 | 181 |
fun get_atomize_rulify f ctxt = map (Thm.transfer' ctxt) (f (#atomize_rulify (get_data ctxt))); |
182 |
val get_atomize = get_atomize_rulify #1; |
|
183 |
val get_rulify = get_atomize_rulify #2; |
|
11897 | 184 |
|
25497 | 185 |
fun add_atomize th = map_data (fn (base_sort, judgment, (atomize, rulify)) => |
61092 | 186 |
(base_sort, judgment, (Thm.add_thm (Thm.trim_context th) atomize, rulify))); |
25497 | 187 |
|
188 |
fun add_rulify th = map_data (fn (base_sort, judgment, (atomize, rulify)) => |
|
61092 | 189 |
(base_sort, judgment, (atomize, Thm.add_thm (Thm.trim_context th) rulify))); |
11897 | 190 |
|
59970 | 191 |
val declare_atomize = Thm.declaration_attribute add_atomize; |
192 |
val declare_rulify = Thm.declaration_attribute add_rulify; |
|
22846 | 193 |
|
59970 | 194 |
val _ = Theory.setup (fold (Context.theory_map o add_rulify) Drule.norm_hhf_eqs); |
11897 | 195 |
|
196 |
||
197 |
(* atomize *) |
|
198 |
||
59970 | 199 |
fun atomize_term ctxt = |
200 |
drop_judgment ctxt o |
|
201 |
Raw_Simplifier.rewrite_term (Proof_Context.theory_of ctxt) (get_atomize ctxt) []; |
|
12729 | 202 |
|
59970 | 203 |
fun atomize ctxt = Raw_Simplifier.rewrite ctxt true (get_atomize ctxt); |
14743 | 204 |
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
205 |
fun atomize_prems ctxt ct = |
23602
361e9c3a5e3a
tuned interfaces: atomize, atomize_prems, atomize_prems_tac;
wenzelm
parents:
23586
diff
changeset
|
206 |
if Logic.has_meta_prems (Thm.term_of ct) then |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
207 |
Conv.params_conv ~1 (Conv.prems_conv ~1 o atomize) ctxt ct |
23602
361e9c3a5e3a
tuned interfaces: atomize, atomize_prems, atomize_prems_tac;
wenzelm
parents:
23586
diff
changeset
|
208 |
else Conv.all_conv ct; |
11897 | 209 |
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
210 |
val atomize_prems_tac = CONVERSION o atomize_prems; |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
211 |
val full_atomize_tac = CONVERSION o atomize; |
11897 | 212 |
|
213 |
||
214 |
(* rulify *) |
|
215 |
||
59970 | 216 |
fun rulify_term ctxt = |
217 |
Raw_Simplifier.rewrite_term (Proof_Context.theory_of ctxt) (get_rulify ctxt) []; |
|
218 |
||
219 |
fun rulify_tac ctxt = rewrite_goal_tac ctxt (get_rulify ctxt); |
|
18807 | 220 |
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
221 |
fun gen_rulify full ctxt = |
59970 | 222 |
Conv.fconv_rule (Raw_Simplifier.rewrite ctxt full (get_rulify ctxt)) |
60822 | 223 |
#> Variable.gen_all ctxt |
59647
c6f413b660cf
clarified Drule.gen_all: observe context more carefully;
wenzelm
parents:
56239
diff
changeset
|
224 |
#> Thm.strip_shyps |
c6f413b660cf
clarified Drule.gen_all: observe context more carefully;
wenzelm
parents:
56239
diff
changeset
|
225 |
#> Drule.zero_var_indexes; |
11897 | 226 |
|
227 |
val rulify = gen_rulify true; |
|
228 |
val rulify_no_asm = gen_rulify false; |
|
229 |
||
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:
61255
diff
changeset
|
230 |
val rule_format = Thm.rule_attribute [] (rulify o Context.proof_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:
61255
diff
changeset
|
231 |
val rule_format_no_asm = Thm.rule_attribute [] (rulify_no_asm o Context.proof_of); |
11897 | 232 |
|
233 |
end; |