8 signature AX_CLASS = |
8 signature AX_CLASS = |
9 sig |
9 sig |
10 val quiet_mode: bool ref |
10 val quiet_mode: bool ref |
11 val print_axclasses: theory -> unit |
11 val print_axclasses: theory -> unit |
12 val get_info: theory -> string -> {super_classes: class list, intro: thm, axioms: thm list} |
12 val get_info: theory -> string -> {super_classes: class list, intro: thm, axioms: thm list} |
13 val add_axclass: bstring * xstring list -> ((bstring * string) * Attrib.src list) list |
13 val add_axclass: bstring * xstring list -> ((bstring * string) * Attrib.src list) list -> |
14 -> theory -> theory * {intro: thm, axioms: thm list} |
14 theory -> theory * {intro: thm, axioms: thm list} |
15 val add_axclass_i: bstring * class list -> ((bstring * term) * theory attribute list) list |
15 val add_axclass_i: bstring * class list -> ((bstring * term) * theory attribute list) list -> |
16 -> theory -> theory * {intro: thm, axioms: thm list} |
16 theory -> theory * {intro: thm, axioms: thm list} |
17 val add_classrel_thms: thm list -> theory -> theory |
17 val add_classrel_thms: thm list -> theory -> theory |
18 val add_arity_thms: thm list -> theory -> theory |
18 val add_arity_thms: thm list -> theory -> theory |
19 val add_inst_subclass: xstring * xstring -> tactic -> theory -> theory |
19 val add_inst_subclass: xstring * xstring -> tactic -> theory -> theory |
20 val add_inst_subclass_i: class * class -> tactic -> theory -> theory |
20 val add_inst_subclass_i: class * class -> tactic -> theory -> theory |
21 val add_inst_arity: xstring * string list * string -> tactic -> theory -> theory |
21 val add_inst_arity: xstring * string list * string -> tactic -> theory -> theory |
22 val add_inst_arity_i: string * sort list * sort -> tactic -> theory -> theory |
22 val add_inst_arity_i: string * sort list * sort -> tactic -> theory -> theory |
23 val instance_subclass_proof: xstring * xstring -> (theory -> theory) |
23 val instance_subclass: xstring * xstring -> theory -> Proof.state |
24 -> bool -> theory -> ProofHistory.T |
24 val instance_subclass_i: class * class -> theory -> Proof.state |
25 val instance_subclass_proof_i: class * class -> (theory -> theory) |
25 val instance_arity: xstring * string list * string -> theory -> Proof.state |
26 -> bool -> theory -> ProofHistory.T |
26 val instance_arity_i: string * sort list * sort -> theory -> Proof.state |
27 val instance_arity_proof: xstring * string list * string -> (theory -> theory) |
|
28 -> bool -> theory -> ProofHistory.T |
|
29 val instance_arity_proof_i: string * sort list * sort -> (theory -> theory) |
|
30 -> bool -> theory -> ProofHistory.T |
|
31 val intro_classes_tac: thm list -> tactic |
27 val intro_classes_tac: thm list -> tactic |
32 val default_intro_classes_tac: thm list -> tactic |
28 val default_intro_classes_tac: thm list -> tactic |
33 |
|
34 (*legacy interfaces*) |
29 (*legacy interfaces*) |
35 val axclass_tac: thm list -> tactic |
30 val axclass_tac: thm list -> tactic |
36 val add_inst_subclass_x: xstring * xstring -> string list -> thm list |
31 val add_inst_subclass_x: xstring * xstring -> string list -> thm list |
37 -> tactic option -> theory -> theory |
32 -> tactic option -> theory -> theory |
38 val add_inst_arity_x: xstring * string list * string -> string list |
33 val add_inst_arity_x: xstring * string list * string -> string list |
315 |
310 |
316 (* instance declarations -- Isar proof *) |
311 (* instance declarations -- Isar proof *) |
317 |
312 |
318 local |
313 local |
319 |
314 |
320 fun inst_proof mk_prop add_thms inst after_qed int theory = |
315 fun gen_instance mk_prop add_thms inst thy = thy |
321 theory |
316 |> ProofContext.init |
322 |> IsarThy.multi_theorem_i Drule.internalK (K after_qed) ProofContext.export_standard |
317 |> Proof.theorem_i Drule.internalK (K (fold add_thms)) NONE ("", []) |
323 ("", [fn (thy, th) => (add_thms [th] thy, th)]) [] |
318 (map (fn t => (("", []), [(t, ([], []))])) (mk_prop thy inst)); |
324 (map (fn t => (("", []), [(t, ([], []))])) (mk_prop theory inst)) int; |
|
325 |
319 |
326 in |
320 in |
327 |
321 |
328 val instance_subclass_proof = |
322 val instance_subclass = |
329 inst_proof (single oo (mk_classrel oo read_classrel)) add_classrel_thms; |
323 gen_instance (single oo (mk_classrel oo read_classrel)) add_classrel_thms; |
330 val instance_subclass_proof_i = |
324 val instance_subclass_i = |
331 inst_proof (single oo (mk_classrel oo cert_classrel)) add_classrel_thms; |
325 gen_instance (single oo (mk_classrel oo cert_classrel)) add_classrel_thms; |
332 val instance_arity_proof = inst_proof (mk_arities oo read_arity) add_arity_thms; |
326 val instance_arity = gen_instance (mk_arities oo read_arity) add_arity_thms; |
333 val instance_arity_proof_i = inst_proof (mk_arities oo cert_arity) add_arity_thms; |
327 val instance_arity_i = gen_instance (mk_arities oo cert_arity) add_arity_thms; |
334 |
328 |
335 end; |
329 end; |
336 |
330 |
337 |
331 |
338 (* tactics and methods *) |
332 (* tactics and methods *) |
362 |
356 |
363 val axclassP = |
357 val axclassP = |
364 OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl |
358 OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl |
365 ((P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- |
359 ((P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- |
366 P.!!! (P.list1 P.xname)) []) -- Scan.repeat P.spec_name |
360 P.!!! (P.list1 P.xname)) []) -- Scan.repeat P.spec_name |
367 >> (fn (cls, axs) => Toplevel.theory (#1 o add_axclass cls axs))); |
361 >> (Toplevel.theory o (#1 oo uncurry add_axclass))); |
368 |
362 |
369 val instanceP = |
363 val instanceP = |
370 OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal |
364 OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal |
371 ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.xname) |
365 ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> instance_subclass || |
372 >> (fn i => instance_subclass_proof i I) || |
366 P.xname -- (P.$$$ "::" |-- P.!!! P.arity) >> (instance_arity o P.triple2)) |
373 (P.xname -- (P.$$$ "::" |-- P.arity) >> P.triple2) |
367 >> (Toplevel.print oo Toplevel.theory_to_proof)); |
374 >> (fn i => instance_arity_proof i I)) |
|
375 >> (Toplevel.print oo Toplevel.theory_to_proof)); |
|
376 |
368 |
377 val _ = OuterSyntax.add_parsers [axclassP, instanceP]; |
369 val _ = OuterSyntax.add_parsers [axclassP, instanceP]; |
378 |
370 |
379 end; |
371 end; |
380 |
372 |