author  wenzelm 
Fri, 17 Jun 2005 18:33:34 +0200  
changeset 16449  d0dc9a301e37 
parent 15973  5fd94d84470f 
child 17902  7b35ce796a4d 
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 

16 
val assert_propT: theory > term > term 

11897  17 
val declare_atomize: theory attribute 
18 
val declare_rulify: theory attribute 

16449  19 
val atomize_term: theory > term > term 
14743  20 
val atomize_thm: thm > thm 
16449  21 
val atomize_rule: theory > cterm > thm 
11897  22 
val atomize_tac: int > tactic 
12829  23 
val full_atomize_tac: int > tactic 
11897  24 
val atomize_goal: int > thm > thm 
25 
val rulify: thm > thm 

26 
val rulify_no_asm: thm > thm 

27 
val rule_format: 'a attribute 

28 
val rule_format_no_asm: 'a attribute 

29 
end; 

30 

31 
structure ObjectLogic: OBJECT_LOGIC = 

32 
struct 

33 

34 

35 
(** objectlogic theory data **) 

36 

37 
(* data kind 'Pure/objectlogic' *) 

38 

16449  39 
structure ObjectLogicData = TheoryDataFun 
40 
(struct 

11897  41 
val name = "Pure/objectlogic"; 
42 
type T = string option * (thm list * thm list); 

43 

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

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

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

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

55 

56 
fun print _ _ = (); 

16449  57 
end); 
11897  58 

15801  59 
val _ = Context.add_setup [ObjectLogicData.init]; 
60 

11897  61 

62 

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

64 

65 
(* add_judgment(_i) *) 

66 

67 
local 

68 

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

11897  71 

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

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

77 
> ObjectLogicData.map (new_judgment c) 

14226  78 
end; 
11897  79 

80 
in 

81 

82 
val add_judgment = gen_add_judgment Theory.add_consts; 

83 
val add_judgment_i = gen_add_judgment Theory.add_consts_i; 

84 

85 
end; 

86 

87 

88 
(* term operations *) 

89 

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

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

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

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

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

11897  101 
 drop_judgment _ tm = tm; 
102 

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

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

112 

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

11897  117 

118 

119 
(** treatment of metalevel connectives **) 

120 

121 
(* maintain rules *) 

122 

16449  123 
val get_atomize = #1 o #2 o ObjectLogicData.get; 
124 
val get_rulify = #2 o #2 o ObjectLogicData.get; 

11897  125 

12371  126 
val add_atomize = ObjectLogicData.map o Library.apsnd o Library.apfst o Drule.add_rule; 
127 
val add_rulify = ObjectLogicData.map o Library.apsnd o Library.apsnd o Drule.add_rule; 

11897  128 

12371  129 
fun declare_atomize (thy, th) = (add_atomize th thy, th); 
130 
fun declare_rulify (thy, th) = (add_rulify th thy, th); 

11897  131 

132 

133 
(* atomize *) 

134 

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

135 
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

136 
(Drule.goals_conv (Library.equal i) 
fb2141a9f8c0
Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
skalberg
parents:
14981
diff
changeset

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

138 
(Drule.goals_conv (K true) (Tactic.rewrite true rews))))); 
11897  139 

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

12729  142 

16449  143 
fun atomize_rule thy = Tactic.rewrite true (get_atomize thy); 
13376  144 

16449  145 
(*convert a naturaldeduction rule into an objectlevel formula*) 
14743  146 
fun atomize_thm th = 
16449  147 
rewrite_rule (get_atomize (Thm.theory_of_thm th)) th; 
14743  148 

11897  149 
fun atomize_tac i st = 
12807  150 
if Logic.has_meta_prems (Thm.prop_of st) i then 
16449  151 
(rewrite_prems_tac (get_atomize (Thm.theory_of_thm st)) i) st 
11897  152 
else all_tac st; 
153 

12829  154 
fun full_atomize_tac i st = 
16449  155 
rewrite_goal_tac (get_atomize (Thm.theory_of_thm st)) i st; 
12829  156 

11897  157 
fun atomize_goal i st = 
15531  158 
(case Seq.pull (atomize_tac i st) of NONE => st  SOME (st', _) => st'); 
11897  159 

160 

161 
(* rulify *) 

162 

163 
fun gen_rulify full thm = 

16449  164 
Tactic.simplify full (get_rulify (Thm.theory_of_thm thm)) thm 
12725  165 
> Drule.gen_all > Drule.strip_shyps_warning > Drule.zero_var_indexes; 
11897  166 

167 
val rulify = gen_rulify true; 

168 
val rulify_no_asm = gen_rulify false; 

169 

170 
fun rule_format x = Drule.rule_attribute (fn _ => rulify) x; 

171 
fun rule_format_no_asm x = Drule.rule_attribute (fn _ => rulify_no_asm) x; 

172 

173 

174 
end; 