author  wenzelm 
Tue, 14 Mar 2006 16:29:38 +0100  
changeset 19261  9f8e56d1dbf6 
parent 18939  18e2a2676d80 
child 20912  380663e636a8 
permissions  rwrr 
11897  1 
(* Title: Pure/Isar/object_logic.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

4 

5 
Specifics about common objectlogics. 

6 
*) 

7 

8 
signature OBJECT_LOGIC = 

9 
sig 

10 
val add_judgment: bstring * string * mixfix > theory > theory 

11 
val add_judgment_i: bstring * typ * mixfix > theory > theory 

16449  12 
val judgment_name: theory > string 
13 
val is_judgment: theory > term > bool 

14 
val drop_judgment: theory > term > term 

15 
val fixed_judgment: theory > string > term 

18121  16 
val ensure_propT: theory > term > term 
19261  17 
val is_elim: thm > bool 
18728  18 
val declare_atomize: attribute 
19 
val declare_rulify: attribute 

16449  20 
val atomize_term: theory > term > term 
18783  21 
val atomize_cterm: cterm > thm 
14743  22 
val atomize_thm: thm > thm 
11897  23 
val atomize_tac: int > tactic 
12829  24 
val full_atomize_tac: int > tactic 
11897  25 
val atomize_goal: int > thm > thm 
18807  26 
val rulify_term: theory > term > term 
27 
val rulify_tac: int > tactic 

11897  28 
val rulify: thm > thm 
29 
val rulify_no_asm: thm > thm 

18728  30 
val rule_format: attribute 
31 
val rule_format_no_asm: attribute 

11897  32 
end; 
33 

34 
structure ObjectLogic: OBJECT_LOGIC = 

35 
struct 

36 

37 

18825  38 
(** theory data **) 
11897  39 

16449  40 
structure ObjectLogicData = TheoryDataFun 
41 
(struct 

18563  42 
val name = "Pure/object_logic"; 
11897  43 
type T = string option * (thm list * thm list); 
44 

15531  45 
val empty = (NONE, ([], [Drule.norm_hhf_eq])); 
11897  46 
val copy = I; 
16449  47 
val extend = I; 
11897  48 

15531  49 
fun merge_judgment (SOME x, SOME y) = 
50 
if x = y then SOME x else error "Attempt to merge different objectlogics" 

15973  51 
 merge_judgment (j1, j2) = if is_some j1 then j1 else j2; 
11897  52 

16449  53 
fun merge _ ((judgment1, (atomize1, rulify1)), (judgment2, (atomize2, rulify2))) = 
11897  54 
(merge_judgment (judgment1, judgment2), 
55 
(Drule.merge_rules (atomize1, atomize2), Drule.merge_rules (rulify1, rulify2))); 

56 

57 
fun print _ _ = (); 

16449  58 
end); 
11897  59 

18708  60 
val _ = Context.add_setup ObjectLogicData.init; 
15801  61 

11897  62 

63 

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

65 

18825  66 
(* add judgment *) 
11897  67 

68 
local 

69 

15531  70 
fun new_judgment name (NONE, rules) = (SOME name, rules) 
71 
 new_judgment _ (SOME _, _) = error "Attempt to redeclare objectlogic judgment"; 

11897  72 

16449  73 
fun gen_add_judgment add_consts (bname, T, mx) thy = 
74 
let val c = Sign.full_name thy (Syntax.const_name bname mx) in 

14226  75 
thy 
16449  76 
> add_consts [(bname, T, mx)] 
77 
> (fn thy' => Theory.add_finals_i false [(Const (c, Sign.the_const_type thy' c))] thy') 

78 
> ObjectLogicData.map (new_judgment c) 

14226  79 
end; 
11897  80 

81 
in 

82 

83 
val add_judgment = gen_add_judgment Theory.add_consts; 

84 
val add_judgment_i = gen_add_judgment Theory.add_consts_i; 

85 

86 
end; 

87 

88 

89 
(* term operations *) 

90 

16449  91 
fun judgment_name thy = 
92 
(case ObjectLogicData.get thy of 

15531  93 
(SOME name, _) => name 
11897  94 
 _ => raise TERM ("Unknown objectlogic judgment", [])); 
95 

16449  96 
fun is_judgment thy (Const (c, _) $ _) = c = judgment_name thy 
11897  97 
 is_judgment _ _ = false; 
98 

16449  99 
fun drop_judgment thy (Abs (x, T, t)) = Abs (x, T, drop_judgment thy t) 
100 
 drop_judgment thy (tm as (Const (c, _) $ t)) = 

101 
if (c = judgment_name thy handle TERM _ => false) then t else tm 

11897  102 
 drop_judgment _ tm = tm; 
103 

16449  104 
fun fixed_judgment thy x = 
11897  105 
let (*be robust wrt. lowlevel errors*) 
16449  106 
val c = judgment_name thy; 
14854  107 
val aT = TFree ("'a", []); 
11897  108 
val T = 
18939  109 
the_default (aT > propT) (Sign.const_type thy c) 
11897  110 
> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S)); 
111 
val U = Term.domain_type T handle Match => aT; 

112 
in Const (c, T) $ Free (x, U) end; 

113 

18121  114 
fun ensure_propT thy t = 
13376  115 
let val T = Term.fastype_of t 
16449  116 
in if T = propT then t else Const (judgment_name thy, T > propT) $ t end; 
13376  117 

11897  118 

19261  119 
(* elimination rules *) 
120 

121 
fun is_elim rule = 

122 
let 

123 
val thy = Thm.theory_of_thm rule; 

124 
val concl = Thm.concl_of rule; 

125 
in 

126 
Term.is_Var (drop_judgment thy concl) andalso 

127 
exists (fn prem => concl aconv Logic.strip_assums_concl prem) (Thm.prems_of rule) 

128 
end; 

129 

130 

11897  131 

132 
(** treatment of metalevel connectives **) 

133 

134 
(* maintain rules *) 

135 

16449  136 
val get_atomize = #1 o #2 o ObjectLogicData.get; 
137 
val get_rulify = #2 o #2 o ObjectLogicData.get; 

11897  138 

18728  139 
val declare_atomize = 
140 
Thm.declaration_attribute (Context.map_theory o ObjectLogicData.map o 

141 
Library.apsnd o Library.apfst o Drule.add_rule); 

11897  142 

18728  143 
val declare_rulify = 
144 
Thm.declaration_attribute (Context.map_theory o ObjectLogicData.map o 

145 
Library.apsnd o Library.apsnd o Drule.add_rule); 

11897  146 

147 

148 
(* atomize *) 

149 

15001
fb2141a9f8c0
Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
skalberg
parents:
14981
diff
changeset

150 
fun rewrite_prems_tac rews i = PRIMITIVE (Drule.fconv_rule 
fb2141a9f8c0
Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
skalberg
parents:
14981
diff
changeset

151 
(Drule.goals_conv (Library.equal i) 
18254  152 
(Drule.forall_conv ~1 
15001
fb2141a9f8c0
Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
skalberg
parents:
14981
diff
changeset

153 
(Drule.goals_conv (K true) (Tactic.rewrite true rews))))); 
11897  154 

16449  155 
fun atomize_term thy = 
156 
drop_judgment thy o MetaSimplifier.rewrite_term thy (get_atomize thy) []; 

12729  157 

18783  158 
fun atomize_cterm ct = Tactic.rewrite true (get_atomize (Thm.theory_of_cterm ct)) ct; 
17902  159 
fun atomize_thm th = rewrite_rule (get_atomize (Thm.theory_of_thm th)) th; 
14743  160 

11897  161 
fun atomize_tac i st = 
12807  162 
if Logic.has_meta_prems (Thm.prop_of st) i then 
16449  163 
(rewrite_prems_tac (get_atomize (Thm.theory_of_thm st)) i) st 
11897  164 
else all_tac st; 
165 

12829  166 
fun full_atomize_tac i st = 
16449  167 
rewrite_goal_tac (get_atomize (Thm.theory_of_thm st)) i st; 
12829  168 

11897  169 
fun atomize_goal i st = 
15531  170 
(case Seq.pull (atomize_tac i st) of NONE => st  SOME (st', _) => st'); 
11897  171 

172 

173 
(* rulify *) 

174 

18807  175 
fun rulify_term thy = MetaSimplifier.rewrite_term thy (get_rulify thy) []; 
176 
fun rulify_tac i st = rewrite_goal_tac (get_rulify (Thm.theory_of_thm st)) i st; 

177 

11897  178 
fun gen_rulify full thm = 
16449  179 
Tactic.simplify full (get_rulify (Thm.theory_of_thm thm)) thm 
12725  180 
> Drule.gen_all > Drule.strip_shyps_warning > Drule.zero_var_indexes; 
11897  181 

182 
val rulify = gen_rulify true; 

183 
val rulify_no_asm = gen_rulify false; 

184 

18728  185 
fun rule_format x = Thm.rule_attribute (fn _ => rulify) x; 
186 
fun rule_format_no_asm x = Thm.rule_attribute (fn _ => rulify_no_asm) x; 

11897  187 

188 
end; 