author  wenzelm 
Tue, 06 Aug 2019 16:15:22 +0200  
changeset 70657  1004333b76aa 
parent 70572  35dd9212bf29 
child 74694  e098fa45bfe0 
permissions  rwrr 
11897  1 
(* Title: Pure/Isar/object_logic.ML 
2 
Author: Markus Wenzel, TU Muenchen 

3 

4 
Specifics about common objectlogics. 

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 
14 
val is_judgment: Proof.context > term > bool 

15 
val drop_judgment: Proof.context > term > term 

16 
val fixed_judgment: Proof.context > string > term 

17 
val ensure_propT: Proof.context > term > term 

18 
val dest_judgment: Proof.context > cterm > cterm 

19 
val judgment_conv: Proof.context > conv > conv 

70170  20 
val is_propositional: Proof.context > typ > bool 
59970  21 
val elim_concl: Proof.context > thm > term option 
18728  22 
val declare_atomize: attribute 
23 
val declare_rulify: attribute 

59970  24 
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

25 
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

26 
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

27 
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

28 
val full_atomize_tac: Proof.context > int > tactic 
59970  29 
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

30 
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

31 
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

32 
val rulify_no_asm: Proof.context > thm > thm 
18728  33 
val rule_format: attribute 
34 
val rule_format_no_asm: attribute 

11897  35 
end; 
36 

35625  37 
structure Object_Logic: OBJECT_LOGIC = 
11897  38 
struct 
39 

59970  40 
(** context data **) 
11897  41 

25497  42 
datatype data = Data of 
43 
{base_sort: sort option, 

44 
judgment: string option, 

45 
atomize_rulify: thm list * thm list}; 

46 

47 
fun make_data (base_sort, judgment, atomize_rulify) = 

48 
Data {base_sort = base_sort, judgment = judgment, atomize_rulify = atomize_rulify}; 

11897  49 

59970  50 
structure Data = Generic_Data 
22846  51 
( 
25497  52 
type T = data; 
53 
val empty = make_data (NONE, NONE, ([], [])); 

16449  54 
val extend = I; 
11897  55 

25497  56 
fun merge_opt eq (SOME x, SOME y) = 
57 
if eq (x, y) then SOME x else error "Attempt to merge different objectlogics" 

41493  58 
 merge_opt _ data = merge_options data; 
11897  59 

33522  60 
fun merge 
25497  61 
(Data {base_sort = base_sort1, judgment = judgment1, atomize_rulify = (atomize1, rulify1)}, 
62 
Data {base_sort = base_sort2, judgment = judgment2, atomize_rulify = (atomize2, rulify2)}) = 

63 
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

64 
(Thm.merge_thms (atomize1, atomize2), Thm.merge_thms (rulify1, rulify2))); 
22846  65 
); 
15801  66 

37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36610
diff
changeset

67 
fun map_data f = Data.map (fn (Data {base_sort, judgment, atomize_rulify}) => 
25497  68 
make_data (f (base_sort, judgment, atomize_rulify))); 
69 

59970  70 
fun get_data ctxt = Data.get (Context.Proof ctxt) > (fn Data args => args); 
25497  71 

11897  72 

73 

74 
(** generic treatment of judgments  with a single argument only **) 

75 

25497  76 
(* base_sort *) 
77 

78 
val get_base_sort = #base_sort o get_data; 

79 

59970  80 
fun add_base_sort S = 
81 
(Context.theory_map o map_data) (fn (base_sort, judgment, atomize_rulify) => 

82 
if is_some base_sort then error "Attempt to redeclare objectlogic base sort" 

83 
else (SOME S, judgment, atomize_rulify)); 

25497  84 

85 

18825  86 
(* add judgment *) 
11897  87 

88 
local 

89 

30344
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
29606
diff
changeset

90 
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

91 
let 
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61246
diff
changeset

92 
val c = Sign.full_name thy b; 
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61246
diff
changeset

93 
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

94 
val T' = Logic.unvarifyT_global (Sign.the_const_type thy' c); 
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' 
15865e0c5598
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
wenzelm
parents:
61246
diff
changeset

97 
> Theory.add_deps_global "" (Theory.const_dep thy' (c, T')) [] 
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 objectlogic 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 objectlogic judgment", [])); 
117 

59970  118 
fun is_judgment ctxt (Const (c, _) $ _) = c = judgment_name ctxt 
11897  119 
 is_judgment _ _ = false; 
120 

59970  121 
fun drop_judgment ctxt (Abs (x, T, t)) = Abs (x, T, drop_judgment ctxt t) 
122 
 drop_judgment ctxt (tm as (Const (c, _) $ t)) = 

123 
if (c = judgment_name ctxt handle TERM _ => false) then t else tm 

11897  124 
 drop_judgment _ tm = tm; 
125 

59970  126 
fun fixed_judgment ctxt x = 
11897  127 
let (*be robust wrt. lowlevel errors*) 
59970  128 
val c = judgment_name ctxt; 
70572  129 
val aT = Term.aT []; 
11897  130 
val T = 
59970  131 
the_default (aT > propT) (Sign.const_type (Proof_Context.theory_of ctxt) c) 
60443  132 
> Term.map_type_tvar (fn ((a, _), S) => TFree (a, S)); 
11897  133 
val U = Term.domain_type T handle Match => aT; 
134 
in Const (c, T) $ Free (x, U) end; 

135 

59970  136 
fun ensure_propT ctxt t = 
13376  137 
let val T = Term.fastype_of t 
59970  138 
in if T = propT then t else Const (judgment_name ctxt, T > propT) $ t end; 
13376  139 

59970  140 
fun dest_judgment ctxt ct = 
141 
if is_judgment ctxt (Thm.term_of ct) 

23586  142 
then Thm.dest_arg ct 
143 
else raise CTERM ("dest_judgment", [ct]); 

144 

59970  145 
fun judgment_conv ctxt cv ct = 
146 
if is_judgment ctxt (Thm.term_of ct) 

23566
b65692d4adcd
replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;
wenzelm
parents:
23540
diff
changeset

147 
then Conv.arg_conv cv ct 
b65692d4adcd
replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;
wenzelm
parents:
23540
diff
changeset

148 
else raise CTERM ("judgment_conv", [ct]); 
b65692d4adcd
replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;
wenzelm
parents:
23540
diff
changeset

149 

70170  150 
fun is_propositional ctxt T = 
151 
T = propT orelse 

152 
let val x = Free (singleton (Variable.variant_frees ctxt []) ("x", T)) 

153 
in can (fn () => Syntax.check_term ctxt (ensure_propT ctxt x)) () end; 

154 

11897  155 

19261  156 
(* elimination rules *) 
157 

59970  158 
fun elim_concl ctxt rule = 
19261  159 
let 
160 
val concl = Thm.concl_of rule; 

59970  161 
val C = drop_judgment ctxt concl; 
19261  162 
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

163 
if Term.is_Var C andalso 
19261  164 
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

165 
then SOME C else NONE 
19261  166 
end; 
167 

168 

11897  169 

170 
(** treatment of metalevel connectives **) 

171 

172 
(* maintain rules *) 

173 

70657  174 
fun get_atomize_rulify f ctxt = map (Thm.transfer' ctxt) (f (#atomize_rulify (get_data ctxt))); 
175 
val get_atomize = get_atomize_rulify #1; 

176 
val get_rulify = get_atomize_rulify #2; 

11897  177 

25497  178 
fun add_atomize th = map_data (fn (base_sort, judgment, (atomize, rulify)) => 
61092  179 
(base_sort, judgment, (Thm.add_thm (Thm.trim_context th) atomize, rulify))); 
25497  180 

181 
fun add_rulify th = map_data (fn (base_sort, judgment, (atomize, rulify)) => 

61092  182 
(base_sort, judgment, (atomize, Thm.add_thm (Thm.trim_context th) rulify))); 
11897  183 

59970  184 
val declare_atomize = Thm.declaration_attribute add_atomize; 
185 
val declare_rulify = Thm.declaration_attribute add_rulify; 

22846  186 

59970  187 
val _ = Theory.setup (fold (Context.theory_map o add_rulify) Drule.norm_hhf_eqs); 
11897  188 

189 

190 
(* atomize *) 

191 

59970  192 
fun atomize_term ctxt = 
193 
drop_judgment ctxt o 

194 
Raw_Simplifier.rewrite_term (Proof_Context.theory_of ctxt) (get_atomize ctxt) []; 

12729  195 

59970  196 
fun atomize ctxt = Raw_Simplifier.rewrite ctxt true (get_atomize ctxt); 
14743  197 

54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset

198 
fun atomize_prems ctxt ct = 
23602
361e9c3a5e3a
tuned interfaces: atomize, atomize_prems, atomize_prems_tac;
wenzelm
parents:
23586
diff
changeset

199 
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

200 
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

201 
else Conv.all_conv ct; 
11897  202 

54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset

203 
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

204 
val full_atomize_tac = CONVERSION o atomize; 
11897  205 

206 

207 
(* rulify *) 

208 

59970  209 
fun rulify_term ctxt = 
210 
Raw_Simplifier.rewrite_term (Proof_Context.theory_of ctxt) (get_rulify ctxt) []; 

211 

212 
fun rulify_tac ctxt = rewrite_goal_tac ctxt (get_rulify ctxt); 

18807  213 

54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset

214 
fun gen_rulify full ctxt = 
59970  215 
Conv.fconv_rule (Raw_Simplifier.rewrite ctxt full (get_rulify ctxt)) 
60822  216 
#> Variable.gen_all ctxt 
59647
c6f413b660cf
clarified Drule.gen_all: observe context more carefully;
wenzelm
parents:
56239
diff
changeset

217 
#> Thm.strip_shyps 
c6f413b660cf
clarified Drule.gen_all: observe context more carefully;
wenzelm
parents:
56239
diff
changeset

218 
#> Drule.zero_var_indexes; 
11897  219 

220 
val rulify = gen_rulify true; 

221 
val rulify_no_asm = gen_rulify false; 

222 

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

223 
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

224 
val rule_format_no_asm = Thm.rule_attribute [] (rulify_no_asm o Context.proof_of); 
11897  225 

226 
end; 