author  haftmann 
Sun, 11 Jan 2009 14:18:16 +0100  
changeset 29439  83601bdadae8 
parent 29378  2821c2c5270d 
child 29509  1ff0f3f08a7b 
permissions  rwrr 
29358  1 
(* Title: Pure/Isar/ML 
24218  2 
Author: Florian Haftmann, TU Muenchen 
3 

29358  4 
Type classes derived from primitive axclasses and locales  interfaces 
24218  5 
*) 
6 

7 
signature CLASS = 

8 
sig 

29358  9 
include CLASS_TARGET 
29439  10 
(*FIXME the split into class_target.ML, theory_target.ML and 
11 
class.ML is artificial*) 

29358  12 

26247  13 
val class: bstring > class list > Element.context_i list 
29378  14 
> theory > string * local_theory 
26247  15 
val class_cmd: bstring > xstring list > Element.context list 
29378  16 
> theory > string * local_theory 
29358  17 
val prove_subclass: tactic > class > local_theory > local_theory 
18 
val subclass: class > local_theory > Proof.state 

19 
val subclass_cmd: xstring > local_theory > Proof.state 

24218  20 
end; 
21 

22 
structure Class : CLASS = 

23 
struct 

24 

29358  25 
open Class_Target; 
28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

26 

29358  27 
(** rule calculation **) 
24589  28 

28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

29 
fun calculate_axiom thy sups base_sort assm_axiom param_map class = 
29360  30 
case Old_Locale.intros thy class 
28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

31 
of (_, []) => assm_axiom 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

32 
 (_, [intro]) => 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

33 
let 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

34 
fun instantiate thy sort = Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o pair (Name.aT, 0)) 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

35 
(base_sort, sort)], map (fn (v, (c, ty)) => pairself (Thm.cterm_of thy) 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

36 
(Var ((v, 0), map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty), 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

37 
Const (c, map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty))) param_map); 
29358  38 
val axiom_premises = map_filter (fst o rules thy) sups 
28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

39 
@ the_list assm_axiom; 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

40 
in intro 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

41 
> instantiate thy [class] 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

42 
> (fn thm => thm OF axiom_premises) 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

43 
> Drule.standard' 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

44 
> Thm.close_derivation 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

45 
> SOME 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

46 
end; 
25024  47 

29439  48 
fun raw_morphism thy class param_map some_axiom = 
49 
let 

50 
val ctxt = ProofContext.init thy; 

51 
val some_wit = case some_axiom 

52 
of SOME axiom => SOME (Element.prove_witness ctxt 

53 
(Logic.unvarify (Thm.prop_of axiom)) 

54 
(ALLGOALS (ProofContext.fact_tac [axiom]))) 

55 
 NONE => NONE; 

56 
val instT = Symtab.empty > Symtab.update ("'a", TFree ("'a", [class])); 

57 
val inst = Symtab.make ((map o apsnd) Const param_map); 

58 
in case some_wit 

59 
of SOME wit => Element.inst_morphism thy (instT, inst) 

60 
$> Morphism.binding_morphism (Binding.add_prefix false (class_prefix class)) 

61 
$> Element.satisfy_morphism [wit] 

62 
 NONE => Element.inst_morphism thy (instT, inst) 

63 
$> Morphism.binding_morphism (Binding.add_prefix false (class_prefix class)) 

64 
end; 

65 

66 
fun calculate_rules thy morph sups base_sort param_map axiom class = 

25062  67 
let 
25711  68 
fun instantiate thy sort = Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o pair (Name.aT, 0)) 
69 
(base_sort, sort)], map (fn (v, (c, ty)) => pairself (Thm.cterm_of thy) 

70 
(Var ((v, 0), map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty), 

71 
Const (c, map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty))) param_map); 

72 
val defs = these_defs thy sups; 

29360  73 
val assm_intro = Old_Locale.intros thy class 
28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

74 
> fst 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

75 
> map (instantiate thy base_sort) 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

76 
> map (MetaSimplifier.rewrite_rule defs) 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

77 
> map Thm.close_derivation 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

78 
> try the_single; 
25711  79 
val fixate = Thm.instantiate 
80 
(map (pairself (Thm.ctyp_of thy)) [(TVar ((Name.aT, 0), []), TFree (Name.aT, base_sort)), 

81 
(TVar ((Name.aT, 0), base_sort), TFree (Name.aT, base_sort))], []) 

25618  82 
val of_class_sups = if null sups 
25711  83 
then map (fixate o Thm.class_triv thy) base_sort 
29358  84 
else map (fixate o snd o rules thy) sups; 
29360  85 
val locale_dests = map Drule.standard' (Old_Locale.dests thy class); 
25711  86 
val num_trivs = case length locale_dests 
87 
of 0 => if is_none axiom then 0 else 1 

88 
 n => n; 

89 
val pred_trivs = if num_trivs = 0 then [] 

90 
else the axiom 

91 
> Thm.prop_of 

92 
> (map_types o map_atyps o K) (TFree (Name.aT, base_sort)) 

93 
> (Thm.assume o Thm.cterm_of thy) 

94 
> replicate num_trivs; 

28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

95 
val axclass_intro = (#intro o AxClass.get_info thy) class; 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

96 
val of_class = (fixate axclass_intro OF of_class_sups OF locale_dests OF pred_trivs) 
25711  97 
> Drule.standard' 
26628
63306cb94313
replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
wenzelm
parents:
26596
diff
changeset

98 
> Thm.close_derivation; 
28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

99 
in (assm_intro, of_class) end; 
24218  100 

28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

101 
fun note_assm_intro class assm_intro thy = 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

102 
thy 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

103 
> Sign.sticky_prefix (class_prefix class ^ "_" ^ AxClass.axiomsN) 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

104 
> PureThy.store_thm (AxClass.introN, assm_intro) 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

105 
> snd 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

106 
> Sign.restore_naming thy; 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

107 

24218  108 

29358  109 
(** define classes **) 
24218  110 

111 
local 

112 

26247  113 
fun gen_class_spec prep_class process_expr thy raw_supclasses raw_elems = 
24218  114 
let 
24748  115 
val supclasses = map (prep_class thy) raw_supclasses; 
116 
val supsort = Sign.minimize_sort thy supclasses; 

25618  117 
val sups = filter (is_class thy) supsort; 
26995  118 
val supparam_names = map fst (these_params thy sups); 
119 
val _ = if has_duplicates (op =) supparam_names 

120 
then error ("Duplicate parameter(s) in superclasses: " 

121 
^ (commas o map quote o duplicates (op =)) supparam_names) 

122 
else (); 

25618  123 
val base_sort = if null sups then supsort else 
26167  124 
foldr1 (Sorts.inter_sort (Sign.classes_of thy)) 
29358  125 
(map (base_sort thy) sups); 
29360  126 
val suplocales = map Old_Locale.Locale sups; 
127 
val supexpr = Old_Locale.Merge suplocales; 

128 
val supparams = (map fst o Old_Locale.parameters_of_expr thy) supexpr; 

129 
val mergeexpr = Old_Locale.Merge suplocales; 

24748  130 
val constrain = Element.Constrains ((map o apsnd o map_atyps) 
26167  131 
(K (TFree (Name.aT, base_sort))) supparams); 
25683  132 
fun fork_syn (Element.Fixes xs) = 
29006  133 
fold_map (fn (c, ty, syn) => cons (Binding.base_name c, syn) #> pair (c, ty, NoSyn)) xs 
25683  134 
#>> Element.Fixes 
135 
 fork_syn x = pair x; 

136 
fun fork_syntax elems = 

137 
let 

138 
val (elems', global_syntax) = fold_map fork_syn elems []; 

26247  139 
in (constrain :: elems', global_syntax) end; 
25683  140 
val (elems, global_syntax) = 
141 
ProofContext.init thy 

29360  142 
> Old_Locale.cert_expr supexpr [constrain] 
25683  143 
> snd 
29358  144 
> begin sups base_sort 
29360  145 
> process_expr Old_Locale.empty raw_elems 
25683  146 
> fst 
147 
> fork_syntax 

148 
in (((sups, supparams), (supsort, base_sort, mergeexpr)), (elems, global_syntax)) end; 

24748  149 

29360  150 
val read_class_spec = gen_class_spec Sign.intern_class Old_Locale.read_expr; 
151 
val check_class_spec = gen_class_spec (K I) Old_Locale.cert_expr; 

24748  152 

28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

153 
fun add_consts bname class base_sort sups supparams global_syntax thy = 
24968
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

154 
let 
25683  155 
val supconsts = map fst supparams 
26518  156 
> AList.make (snd o the o AList.lookup (op =) (these_params thy sups)) 
25683  157 
> (map o apsnd o apsnd o map_atyps o K o TFree) (Name.aT, [class]); 
29360  158 
val all_params = map fst (Old_Locale.parameters_of thy class); 
28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

159 
val raw_params = (snd o chop (length supparams)) all_params; 
25683  160 
fun add_const (v, raw_ty) thy = 
161 
let 

28965  162 
val c = Sign.full_bname thy v; 
25683  163 
val ty = map_atyps (K (TFree (Name.aT, base_sort))) raw_ty; 
164 
val ty0 = Type.strip_sorts ty; 

165 
val ty' = map_atyps (K (TFree (Name.aT, [class]))) ty0; 

166 
val syn = (the_default NoSyn o AList.lookup (op =) global_syntax) v; 

167 
in 

168 
thy 

28965  169 
> Sign.declare_const [] ((Binding.name v, ty0), syn) 
25683  170 
> snd 
171 
> pair ((v, ty), (c, ty')) 

172 
end; 

28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

173 
in 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

174 
thy 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

175 
> Sign.add_path (Logic.const_of_class bname) 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

176 
> fold_map add_const raw_params 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

177 
> Sign.restore_naming thy 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

178 
> (fn params => pair (supconsts @ (map o apfst) fst params, params)) 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

179 
end; 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

180 

238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

181 
fun adjungate_axclass bname class base_sort sups supsort supparams global_syntax thy = 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

182 
let 
25683  183 
fun globalize param_map = map_aterms 
184 
(fn Free (v, ty) => Const ((fst o the o AList.lookup (op =) param_map) v, ty) 

185 
 t => t); 

29360  186 
val raw_pred = Old_Locale.intros thy class 
25683  187 
> fst 
188 
> map (Logic.unvarify o Logic.strip_imp_concl o Thm.prop_of); 

189 
fun get_axiom thy = case (#axioms o AxClass.get_info thy) class 

190 
of [] => NONE 

191 
 [thm] => SOME thm; 

24968
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

192 
in 
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

193 
thy 
28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

194 
> add_consts bname class base_sort sups supparams global_syntax 
25683  195 
> (fn (param_map, params) => AxClass.define_class (bname, supsort) 
26518  196 
(map (fst o snd) params) 
28965  197 
[((Binding.name (bname ^ "_" ^ AxClass.axiomsN), []), map (globalize param_map) raw_pred)] 
25683  198 
#> snd 
199 
#> `get_axiom 

200 
#> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params 

28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

201 
#> pair (map (Const o snd) param_map, param_map, params, assm_axiom))) 
24968
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

202 
end; 
f9bafc868847
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24949
diff
changeset

203 

26518  204 
fun gen_class prep_spec bname raw_supclasses raw_elems thy = 
24748  205 
let 
28965  206 
val class = Sign.full_bname thy bname; 
25683  207 
val (((sups, supparams), (supsort, base_sort, mergeexpr)), (elems, global_syntax)) = 
26247  208 
prep_spec thy raw_supclasses raw_elems; 
28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

209 
val supconsts = map (apsnd fst o snd) (these_params thy sups); 
24218  210 
in 
211 
thy 

29360  212 
> Old_Locale.add_locale "" bname mergeexpr elems 
25038  213 
> snd 
25311  214 
> ProofContext.theory_of 
26518  215 
> adjungate_axclass bname class base_sort sups supsort supparams global_syntax 
28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

216 
> (fn (inst, param_map, params, assm_axiom) => 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

217 
`(fn thy => calculate_axiom thy sups base_sort assm_axiom param_map class) 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

218 
#> (fn axiom => 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

219 
prove_class_interpretation class inst 
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

220 
(supconsts @ map (pair class o fst o snd) params) (the_list axiom) [] 
29439  221 
#> `(fn thy => raw_morphism thy class param_map axiom) 
222 
#> (fn morph => 

223 
`(fn thy => calculate_rules thy morph sups base_sort param_map axiom class) 

28715
238f9966c80e
class morphism stemming from locale interpretation
haftmann
parents:
28674
diff
changeset

224 
#> (fn (assm_intro, of_class) => 
29358  225 
register class sups params base_sort inst 
29439  226 
morph axiom assm_intro of_class 
227 
#> fold (note_assm_intro class) (the_list assm_intro))))) 

29378  228 
> TheoryTarget.init (SOME class) 
25038  229 
> pair class 
24218  230 
end; 
231 

232 
in 

233 

26518  234 
val class_cmd = gen_class read_class_spec; 
235 
val class = gen_class check_class_spec; 

24218  236 

237 
end; (*local*) 

238 

239 

29358  240 
(** subclass relations **) 
25462  241 

29358  242 
local 
25462  243 

29358  244 
fun gen_subclass prep_class do_proof raw_sup lthy = 
25462  245 
let 
29358  246 
val thy = ProofContext.theory_of lthy; 
247 
val sup = prep_class thy raw_sup; 

248 
val sub = case TheoryTarget.peek lthy 

249 
of {is_class = false, ...} => error "Not a class context" 

250 
 {target, ...} => target; 

251 
val _ = if Sign.subsort thy ([sup], [sub]) 

252 
then error ("Class " ^ Syntax.string_of_sort lthy [sup] 

253 
^ " is subclass of class " ^ Syntax.string_of_sort lthy [sub]) 

254 
else (); 

255 
val sub_params = map fst (these_params thy [sub]); 

256 
val sup_params = map fst (these_params thy [sup]); 

257 
val err_params = subtract (op =) sub_params sup_params; 

258 
val _ = if null err_params then [] else 

259 
error ("Class " ^ Syntax.string_of_sort lthy [sub] ^ " lacks parameter(s) " ^ 

260 
commas_quote err_params ^ " of " ^ Syntax.string_of_sort lthy [sup]); 

261 
val sublocale_prop = 

29360  262 
Old_Locale.global_asms_of thy sup 
29358  263 
> maps snd 
264 
> try the_single 

265 
> Option.map (ObjectLogic.ensure_propT thy); 

266 
fun after_qed some_thm = 

267 
LocalTheory.theory (prove_subclass_relation (sub, sup) some_thm) 

268 
#> (TheoryTarget.init (SOME sub) o ProofContext.theory_of); 

26238  269 
in 
29358  270 
do_proof after_qed sublocale_prop lthy 
25485  271 
end; 
272 

29358  273 
fun user_proof after_qed NONE = 
274 
Proof.theorem_i NONE (K (after_qed NONE)) [[]] 

275 
 user_proof after_qed (SOME prop) = 

276 
Proof.theorem_i NONE (after_qed o try the_single o the_single) [[(prop, [])]]; 

25485  277 

29358  278 
fun tactic_proof tac after_qed NONE lthy = 
279 
after_qed NONE lthy 

280 
 tactic_proof tac after_qed (SOME prop) lthy = 

281 
after_qed (SOME (Goal.prove (LocalTheory.target_of lthy) [] [] prop 

282 
(K tac))) lthy; 

28666  283 

29358  284 
in 
28666  285 

29358  286 
val subclass = gen_subclass (K I) user_proof; 
287 
fun prove_subclass tac = gen_subclass (K I) (tactic_proof tac); 

288 
val subclass_cmd = gen_subclass Sign.read_class user_proof; 

25462  289 

29358  290 
end; (*local*) 
291 

25603  292 

24218  293 
end; 
25683  294 