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: xstring * xstring -> theory -> Proof.state |
23 val instance_subclass: xstring * xstring -> theory -> Proof.state |
24 val instance_subclass_i: class * class -> theory -> Proof.state |
24 val instance_subclass_i: class * class -> theory -> Proof.state |
25 val instance_arity: xstring * string list * string -> theory -> Proof.state |
25 val instance_arity: (theory -> theory) -> xstring * string list * string -> theory -> Proof.state |
26 val instance_arity_i: string * sort list * sort -> theory -> Proof.state |
26 val instance_arity_i: (theory -> theory) -> string * sort list * sort -> theory -> Proof.state |
27 val read_arity: theory -> xstring * string list * string -> arity |
27 val read_arity: theory -> xstring * string list * string -> arity |
28 val cert_arity: theory -> string * sort list * sort -> arity |
28 val cert_arity: theory -> string * sort list * sort -> arity |
29 val intro_classes_tac: thm list -> tactic |
29 val intro_classes_tac: thm list -> tactic |
30 val default_intro_classes_tac: thm list -> tactic |
30 val default_intro_classes_tac: thm list -> tactic |
31 end; |
31 end; |
301 |
301 |
302 (* instance declarations -- Isar proof *) |
302 (* instance declarations -- Isar proof *) |
303 |
303 |
304 local |
304 local |
305 |
305 |
306 fun gen_instance mk_prop add_thms inst thy = thy |
306 fun gen_instance mk_prop add_thms after_qed inst thy = |
|
307 thy |
307 |> ProofContext.init |
308 |> ProofContext.init |
308 |> Proof.theorem_i Drule.internalK NONE (fold add_thms) NONE ("", []) |
309 |> Proof.theorem_i Drule.internalK NONE (after_qed oo fold add_thms) NONE ("", []) |
309 (map (fn t => (("", []), [(t, ([], []))])) (mk_prop thy inst)); |
310 (map (fn t => (("", []), [(t, ([], []))])) (mk_prop thy inst)); |
310 |
311 |
311 in |
312 in |
312 |
313 |
313 val instance_subclass = |
314 val instance_subclass = |
314 gen_instance (single oo (mk_classrel oo read_classrel)) add_classrel_thms; |
315 gen_instance (single oo (mk_classrel oo read_classrel)) add_classrel_thms I; |
315 val instance_subclass_i = |
316 val instance_subclass_i = |
316 gen_instance (single oo (mk_classrel oo cert_classrel)) add_classrel_thms; |
317 gen_instance (single oo (mk_classrel oo cert_classrel)) add_classrel_thms I; |
317 val instance_arity = gen_instance (mk_arities oo read_arity) add_arity_thms; |
318 val instance_arity = |
318 val instance_arity_i = gen_instance (mk_arities oo cert_arity) add_arity_thms; |
319 gen_instance (mk_arities oo read_arity) add_arity_thms; |
|
320 val instance_arity_i = |
|
321 gen_instance (mk_arities oo cert_arity) add_arity_thms; |
319 |
322 |
320 end; |
323 end; |
321 |
324 |
322 |
325 |
323 (* tactics and methods *) |
326 (* tactics and methods *) |
352 >> (Toplevel.theory o (snd oo uncurry add_axclass))); |
355 >> (Toplevel.theory o (snd oo uncurry add_axclass))); |
353 |
356 |
354 val instanceP = |
357 val instanceP = |
355 OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal |
358 OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal |
356 ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> instance_subclass || |
359 ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> instance_subclass || |
357 P.xname -- (P.$$$ "::" |-- P.!!! P.arity) >> (instance_arity o P.triple2)) |
360 P.xname -- (P.$$$ "::" |-- P.!!! P.arity) >> (instance_arity I o P.triple2)) |
358 >> (Toplevel.print oo Toplevel.theory_to_proof)); |
361 >> (Toplevel.print oo Toplevel.theory_to_proof)); |
359 |
362 |
360 val _ = OuterSyntax.add_parsers [axclassP, instanceP]; |
363 val _ = OuterSyntax.add_parsers [axclassP, instanceP]; |
361 |
364 |
362 end; |
365 end; |