1(* Title: Pure/axclass.ML 2 Author: Markus Wenzel, TU Muenchen 3 4Type classes defined as predicates, associated with a record of 5parameters. Proven class relations and type arities. 6*) 7 8signature AXCLASS = 9sig 10 type info = {def: thm, intro: thm, axioms: thm list, params: (string * typ) list} 11 val get_info: theory -> class -> info 12 val class_of_param: theory -> string -> class option 13 val instance_name: string * class -> string 14 val param_of_inst: theory -> string * string -> string 15 val inst_of_param: theory -> string -> (string * string) option 16 val unoverload: Proof.context -> thm -> thm 17 val overload: Proof.context -> thm -> thm 18 val unoverload_conv: Proof.context -> conv 19 val overload_conv: Proof.context -> conv 20 val lookup_inst_param: Consts.T -> ((string * string) * 'a) list -> string * typ -> 'a option 21 val unoverload_const: theory -> string * typ -> string 22 val cert_classrel: theory -> class * class -> class * class 23 val read_classrel: theory -> xstring * xstring -> class * class 24 val declare_overloaded: string * typ -> theory -> term * theory 25 val define_overloaded: binding -> string * term -> theory -> thm * theory 26 val add_classrel: thm -> theory -> theory 27 val add_arity: thm -> theory -> theory 28 val prove_classrel: class * class -> (Proof.context -> tactic) -> theory -> theory 29 val prove_arity: string * sort list * sort -> (Proof.context -> tactic) -> theory -> theory 30 val define_class: binding * class list -> string list -> 31 (Thm.binding * term list) list -> theory -> class * theory 32 val classrel_axiomatization: (class * class) list -> theory -> theory 33 val arity_axiomatization: arity -> theory -> theory 34 val class_axiomatization: binding * class list -> theory -> theory 35end; 36 37structure Axclass: AXCLASS = 38struct 39 40(** theory data **) 41 42(* axclass info *) 43 44type info = 45 {def: thm, 46 intro: thm, 47 axioms: thm list, 48 params: (string * typ) list}; 49 50fun make_axclass (def, intro, axioms, params): info = 51 {def = def, intro = intro, axioms = axioms, params = params}; 52 53 54(* class parameters (canonical order) *) 55 56type param = string * class; 57 58fun add_param ctxt ((x, c): param) params = 59 (case AList.lookup (op =) params x of 60 NONE => (x, c) :: params 61 | SOME c' => 62 error ("Duplicate class parameter " ^ quote x ^ " for " ^ Syntax.string_of_sort ctxt [c] ^ 63 (if c = c' then "" else " and " ^ Syntax.string_of_sort ctxt [c']))); 64 65 66(* setup data *) 67 68datatype data = Data of 69 {axclasses: info Symtab.table, 70 params: param list, 71 (*arity theorems with theory name*) 72 inst_params: 73 (string * thm) Symtab.table Symtab.table * 74 (*constant name ~> type constructor ~> (constant name, equation)*) 75 (string * string) Symtab.table (*constant name ~> (constant name, type constructor)*)}; 76 77fun make_data (axclasses, params, inst_params) = 78 Data {axclasses = axclasses, params = params, inst_params = inst_params}; 79 80structure Data = Theory_Data' 81( 82 type T = data; 83 val empty = make_data (Symtab.empty, [], (Symtab.empty, Symtab.empty)); 84 val extend = I; 85 fun merge old_thys 86 (Data {axclasses = axclasses1, params = params1, inst_params = inst_params1}, 87 Data {axclasses = axclasses2, params = params2, inst_params = inst_params2}) = 88 let 89 val old_ctxt = Syntax.init_pretty_global (fst old_thys); 90 91 val axclasses' = Symtab.merge (K true) (axclasses1, axclasses2); 92 val params' = 93 if null params1 then params2 94 else 95 fold_rev (fn p => if member (op =) params1 p then I else add_param old_ctxt p) 96 params2 params1; 97 98 val inst_params' = 99 (Symtab.join (K (Symtab.merge (K true))) (#1 inst_params1, #1 inst_params2), 100 Symtab.merge (K true) (#2 inst_params1, #2 inst_params2)); 101 in make_data (axclasses', params', inst_params') end; 102); 103 104fun map_data f = 105 Data.map (fn Data {axclasses, params, inst_params} => 106 make_data (f (axclasses, params, inst_params))); 107 108fun map_axclasses f = 109 map_data (fn (axclasses, params, inst_params) => 110 (f axclasses, params, inst_params)); 111 112fun map_params f = 113 map_data (fn (axclasses, params, inst_params) => 114 (axclasses, f params, inst_params)); 115 116fun map_inst_params f = 117 map_data (fn (axclasses, params, inst_params) => 118 (axclasses, params, f inst_params)); 119 120val rep_data = Data.get #> (fn Data args => args); 121 122val axclasses_of = #axclasses o rep_data; 123val params_of = #params o rep_data; 124val inst_params_of = #inst_params o rep_data; 125 126 127(* axclasses with parameters *) 128 129fun get_info thy c = 130 (case Symtab.lookup (axclasses_of thy) c of 131 SOME {def, intro, axioms, params} => 132 {def = Thm.transfer thy def, 133 intro = Thm.transfer thy intro, 134 axioms = map (Thm.transfer thy) axioms, 135 params = params} 136 | NONE => error ("No such axclass: " ^ quote c)); 137 138fun all_params_of thy S = 139 let val params = params_of thy; 140 in fold (fn (x, c) => if Sign.subsort thy (S, [c]) then cons x else I) params [] end; 141 142fun class_of_param thy = AList.lookup (op =) (params_of thy); 143 144 145(* maintain instance parameters *) 146 147fun get_inst_param thy (c, tyco) = 148 (case Symtab.lookup (the_default Symtab.empty (Symtab.lookup (#1 (inst_params_of thy)) c)) tyco of 149 SOME (a, th) => (a, Thm.transfer thy th) 150 | NONE => error ("No instance parameter for constant " ^ quote c ^ " on type " ^ quote tyco)); 151 152fun add_inst_param (c, tyco) (a, th) = 153 (map_inst_params o apfst o Symtab.map_default (c, Symtab.empty)) 154 (Symtab.update_new (tyco, (a, Thm.trim_context th))) 155 #> (map_inst_params o apsnd) (Symtab.update_new (a, (c, tyco))); 156 157val inst_of_param = Symtab.lookup o #2 o inst_params_of; 158val param_of_inst = #1 oo get_inst_param; 159 160fun inst_thms ctxt = 161 Symtab.fold 162 (Symtab.fold (cons o #2 o #2) o #2) (#1 (inst_params_of (Proof_Context.theory_of ctxt))) []; 163 164fun get_inst_tyco consts = try (#1 o dest_Type o the_single o Consts.typargs consts); 165 166fun unoverload ctxt = rewrite_rule ctxt (inst_thms ctxt); 167fun overload ctxt = rewrite_rule ctxt (map Thm.symmetric (inst_thms ctxt)); 168 169fun unoverload_conv ctxt = Raw_Simplifier.rewrite ctxt true (inst_thms ctxt); 170fun overload_conv ctxt = Raw_Simplifier.rewrite ctxt true (map Thm.symmetric (inst_thms ctxt)); 171 172fun lookup_inst_param consts params (c, T) = 173 (case get_inst_tyco consts (c, T) of 174 SOME tyco => AList.lookup (op =) params (c, tyco) 175 | NONE => NONE); 176 177fun unoverload_const thy (c_ty as (c, _)) = 178 if is_some (class_of_param thy c) then 179 (case get_inst_tyco (Sign.consts_of thy) c_ty of 180 SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c 181 | NONE => c) 182 else c; 183 184 185 186(** instances **) 187 188val classrel_prefix = "classrel_"; 189val arity_prefix = "arity_"; 190 191fun instance_name (a, c) = Long_Name.base_name c ^ "_" ^ Long_Name.base_name a; 192 193 194(* class relations *) 195 196fun cert_classrel thy raw_rel = 197 let 198 val string_of_sort = Syntax.string_of_sort_global thy; 199 val (c1, c2) = apply2 (Sign.certify_class thy) raw_rel; 200 val _ = Sign.primitive_classrel (c1, c2) thy; 201 val _ = 202 (case subtract (op =) (all_params_of thy [c1]) (all_params_of thy [c2]) of 203 [] => () 204 | xs => raise TYPE ("Class " ^ string_of_sort [c1] ^ " lacks parameter(s) " ^ 205 commas_quote xs ^ " of " ^ string_of_sort [c2], [], [])); 206 in (c1, c2) end; 207 208fun read_classrel thy raw_rel = 209 cert_classrel thy (apply2 (Proof_Context.read_class (Proof_Context.init_global thy)) raw_rel) 210 handle TYPE (msg, _, _) => error msg; 211 212 213(* declaration and definition of instances of overloaded constants *) 214 215fun inst_tyco_of thy (c, T) = 216 (case get_inst_tyco (Sign.consts_of thy) (c, T) of 217 SOME tyco => tyco 218 | NONE => error ("Illegal type for instantiation of class parameter: " ^ 219 quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T))); 220 221fun declare_overloaded (c, T) thy = 222 let 223 val class = 224 (case class_of_param thy c of 225 SOME class => class 226 | NONE => error ("Not a class parameter: " ^ quote c)); 227 val tyco = inst_tyco_of thy (c, T); 228 val name_inst = instance_name (tyco, class) ^ "_inst"; 229 val c' = instance_name (tyco, c); 230 val T' = Type.strip_sorts T; 231 in 232 thy 233 |> Sign.qualified_path true (Binding.name name_inst) 234 |> Sign.declare_const_global ((Binding.name c', T'), NoSyn) 235 |-> (fn const' as Const (c'', _) => 236 Thm.add_def_global false true 237 (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const')) 238 #>> apsnd Thm.varifyT_global 239 #-> (fn (_, thm) => add_inst_param (c, tyco) (c'', thm) 240 #> Global_Theory.add_thm ((Binding.concealed (Binding.name c'), thm), []) 241 #> #2 242 #> pair (Const (c, T)))) 243 ||> Sign.restore_naming thy 244 end; 245 246fun define_overloaded b (c, t) thy = 247 let 248 val T = Term.fastype_of t; 249 val tyco = inst_tyco_of thy (c, T); 250 val (c', eq) = get_inst_param thy (c, tyco); 251 val prop = Logic.mk_equals (Const (c', T), t); 252 val b' = Thm.def_binding_optional (Binding.name (instance_name (tyco, c))) b; 253 in 254 thy 255 |> Thm.add_def_global false false (b', prop) 256 |>> (fn (_, thm) => Drule.transitive_thm OF [eq, thm]) 257 end; 258 259 260(* primitive rules *) 261 262fun add_classrel raw_th thy = 263 let 264 val th = Thm.strip_shyps (Thm.transfer thy raw_th); 265 val prop = Thm.plain_prop_of th; 266 fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]); 267 val rel = Logic.dest_classrel prop handle TERM _ => err (); 268 val (c1, c2) = cert_classrel thy rel handle TYPE _ => err (); 269 val binding = 270 Binding.concealed (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2)))); 271 in thy |> Global_Theory.store_thm (binding, th) |-> Thm.add_classrel end; 272 273fun add_arity raw_th thy = 274 let 275 val th = Thm.strip_shyps (Thm.transfer thy raw_th); 276 val prop = Thm.plain_prop_of th; 277 fun err () = raise THM ("add_arity: malformed type arity", 0, [th]); 278 val arity as (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err (); 279 280 val binding = 281 Binding.concealed (Binding.name (prefix arity_prefix (Logic.name_arity arity))); 282 283 val args = Name.invent_names Name.context Name.aT Ss; 284 val missing_params = 285 Sign.complete_sort thy [c] 286 |> maps (these o Option.map #params o try (get_info thy)) 287 |> filter_out (fn (const, _) => can (get_inst_param thy) (const, t)) 288 |> (map o apsnd o map_atyps) (K (Type (t, map TFree args))); 289 in 290 thy 291 |> Global_Theory.store_thm (binding, th) 292 |-> Thm.add_arity 293 |> fold (#2 oo declare_overloaded) missing_params 294 end; 295 296 297(* tactical proofs *) 298 299fun prove_classrel raw_rel tac thy = 300 let 301 val ctxt = Proof_Context.init_global thy; 302 val (c1, c2) = cert_classrel thy raw_rel; 303 val th = 304 Goal.prove ctxt [] [] (Logic.mk_classrel (c1, c2)) (fn {context, ...} => tac context) 305 handle ERROR msg => 306 cat_error msg ("The error(s) above occurred while trying to prove class relation " ^ 307 quote (Syntax.string_of_classrel ctxt [c1, c2])); 308 in 309 thy |> add_classrel th 310 end; 311 312fun prove_arity raw_arity tac thy = 313 let 314 val ctxt = Proof_Context.init_global thy; 315 val arity = Proof_Context.cert_arity ctxt raw_arity; 316 val props = Logic.mk_arities arity; 317 val ths = 318 Goal.prove_common ctxt NONE [] [] props 319 (fn {context, ...} => Goal.precise_conjunction_tac (length props) 1 THEN tac context) 320 handle ERROR msg => 321 cat_error msg ("The error(s) above occurred while trying to prove type arity " ^ 322 quote (Syntax.string_of_arity ctxt arity)); 323 in 324 thy |> fold add_arity ths 325 end; 326 327 328 329(** class definitions **) 330 331fun split_defined n eq = 332 let 333 val intro = 334 (eq RS Drule.equal_elim_rule2) 335 |> Conjunction.curry_balanced n 336 |> n = 0 ? Thm.eq_assumption 1; 337 val dests = 338 if n = 0 then [] 339 else 340 (eq RS Drule.equal_elim_rule1) 341 |> Balanced_Tree.dest (fn th => 342 (th RS Conjunction.conjunctionD1, th RS Conjunction.conjunctionD2)) n; 343 in (intro, dests) end; 344 345fun define_class (bclass, raw_super) raw_params raw_specs thy = 346 let 347 val ctxt = Syntax.init_pretty_global thy; 348 349 350 (* class *) 351 352 val bconst = Binding.map_name Logic.const_of_class bclass; 353 val class = Sign.full_name thy bclass; 354 val super = Sign.minimize_sort thy (Sign.certify_sort thy raw_super); 355 356 fun check_constraint (a, S) = 357 if Sign.subsort thy (super, S) then () 358 else error ("Sort constraint of type variable " ^ 359 Syntax.string_of_typ (Config.put show_sorts true ctxt) (TFree (a, S)) ^ 360 " needs to be weaker than " ^ Syntax.string_of_sort ctxt super); 361 362 363 (* params *) 364 365 val params = raw_params |> map (fn p => 366 let 367 val T = Sign.the_const_type thy p; 368 val _ = 369 (case Term.add_tvarsT T [] of 370 [((a, _), S)] => check_constraint (a, S) 371 | _ => error ("Exactly one type variable expected in class parameter " ^ quote p)); 372 val T' = Term.map_type_tvar (K (Term.aT [class])) T; 373 in (p, T') end); 374 375 376 (* axioms *) 377 378 fun prep_axiom t = 379 (case Term.add_tfrees t [] of 380 [(a, S)] => check_constraint (a, S) 381 | [] => () 382 | _ => error ("Multiple type variables in class axiom:\n" ^ Syntax.string_of_term ctxt t); 383 t 384 |> Term.map_types (Term.map_atyps (fn TFree _ => Term.aT [] | U => U)) 385 |> Logic.close_form); 386 387 val axiomss = map (map (prep_axiom o Sign.cert_prop thy) o snd) raw_specs; 388 val name_atts = map fst raw_specs; 389 390 391 (* definition *) 392 393 val conjs = Logic.mk_of_sort (Term.aT [], super) @ flat axiomss; 394 val class_eq = 395 Logic.mk_equals (Logic.mk_of_class (Term.aT [], class), Logic.mk_conjunction_balanced conjs); 396 397 val ([def], def_thy) = 398 thy 399 |> Sign.primitive_class (bclass, super) 400 |> Global_Theory.add_defs false [((Thm.def_binding bconst, class_eq), [])]; 401 val (raw_intro, (raw_classrel, raw_axioms)) = 402 split_defined (length conjs) def ||> chop (length super); 403 404 405 (* facts *) 406 407 val class_triv = Thm.class_triv def_thy class; 408 val ([(_, [intro]), (_, classrel), (_, axioms)], facts_thy) = 409 def_thy 410 |> Sign.qualified_path true bconst 411 |> Global_Theory.note_thmss "" 412 [((Binding.name "intro", []), [([Drule.export_without_context raw_intro], [])]), 413 ((Binding.name "super", []), [(map Drule.export_without_context raw_classrel, [])]), 414 ((Binding.name "axioms", []), 415 [(map (fn th => Drule.export_without_context (class_triv RS th)) raw_axioms, [])])] 416 ||> Sign.restore_naming def_thy; 417 418 419 (* result *) 420 421 val axclass = 422 make_axclass 423 (Thm.trim_context def, Thm.trim_context intro, map Thm.trim_context axioms, params); 424 425 val result_thy = 426 facts_thy 427 |> fold (fn th => Thm.add_classrel (class_triv RS th)) classrel 428 |> Sign.qualified_path false bconst 429 |> Global_Theory.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) 430 |> #2 431 |> Sign.restore_naming facts_thy 432 |> map_axclasses (Symtab.update (class, axclass)) 433 |> map_params (fold (fn (x, _) => add_param ctxt (x, class)) params); 434 435 in (class, result_thy) end; 436 437 438 439(** axiomatizations **) 440 441local 442 443(*old-style axioms*) 444fun add_axioms prep mk name add raw_args thy = 445 let 446 val args = prep thy raw_args; 447 val specs = mk args; 448 val names = name args; 449 in 450 thy 451 |> fold_map Thm.add_axiom_global (map Binding.name names ~~ specs) 452 |-> fold (add o Drule.export_without_context o snd) 453 end; 454 455fun class_const_dep c = 456 ((Defs.Const, Logic.const_of_class c), [Term.aT []]); 457 458in 459 460val classrel_axiomatization = 461 add_axioms (map o cert_classrel) (map Logic.mk_classrel) 462 (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel; 463 464val arity_axiomatization = 465 add_axioms (Proof_Context.cert_arity o Proof_Context.init_global) Logic.mk_arities 466 (map (prefix arity_prefix) o Logic.name_arities) add_arity; 467 468fun class_axiomatization (bclass, raw_super) thy = 469 let 470 val class = Sign.full_name thy bclass; 471 val super = map (Sign.certify_class thy) raw_super |> Sign.minimize_sort thy; 472 in 473 thy 474 |> Sign.primitive_class (bclass, super) 475 |> classrel_axiomatization (map (fn c => (class, c)) super) 476 |> Theory.add_deps_global "" (class_const_dep class) (map class_const_dep super) 477 end; 478 479end; 480 481end; 482