src/Pure/Isar/class_target.ML
changeset 31635 8623244a50d5
parent 31599 97b4d289c646
child 31697 fd841fc9ee9e
     1.1 --- a/src/Pure/Isar/class_target.ML	Sun Jun 14 17:20:19 2009 +0200
     1.2 +++ b/src/Pure/Isar/class_target.ML	Sun Jun 14 17:20:19 2009 +0200
     1.3 @@ -10,8 +10,6 @@
     1.4    val register: class -> class list -> ((string * typ) * (string * typ)) list
     1.5      -> sort -> morphism -> thm option -> thm option -> thm
     1.6      -> theory -> theory
     1.7 -  val register_subclass: class * class -> morphism option -> Element.witness option
     1.8 -    -> morphism -> theory -> theory
     1.9  
    1.10    val is_class: theory -> class -> bool
    1.11    val base_sort: theory -> class -> sort
    1.12 @@ -46,8 +44,16 @@
    1.13    val instantiation_param: local_theory -> binding -> string option
    1.14    val confirm_declaration: binding -> local_theory -> local_theory
    1.15    val pretty_instantiation: local_theory -> Pretty.T
    1.16 +  val instance_arity_cmd: xstring * xstring list * xstring -> theory -> Proof.state
    1.17    val type_name: string -> string
    1.18  
    1.19 +  (*subclasses*)
    1.20 +  val register_subclass: class * class -> morphism option -> Element.witness option
    1.21 +    -> morphism -> theory -> theory
    1.22 +  val classrel: class * class -> theory -> Proof.state
    1.23 +  val classrel_cmd: xstring * xstring -> theory -> Proof.state
    1.24 +
    1.25 +  (*tactics*)
    1.26    val intro_classes_tac: thm list -> tactic
    1.27    val default_intro_tac: Proof.context -> thm list -> tactic
    1.28  
    1.29 @@ -55,58 +61,11 @@
    1.30    val axclass_cmd: binding * xstring list
    1.31      -> (Attrib.binding * string list) list
    1.32      -> theory -> class * theory
    1.33 -  val classrel_cmd: xstring * xstring -> theory -> Proof.state
    1.34 -  val instance_arity: (theory -> theory) -> arity -> theory -> Proof.state
    1.35 -  val instance_arity_cmd: xstring * xstring list * xstring -> theory -> Proof.state
    1.36  end;
    1.37  
    1.38  structure Class_Target : CLASS_TARGET =
    1.39  struct
    1.40  
    1.41 -(** primitive axclass and instance commands **)
    1.42 -
    1.43 -fun axclass_cmd (class, raw_superclasses) raw_specs thy =
    1.44 -  let
    1.45 -    val ctxt = ProofContext.init thy;
    1.46 -    val superclasses = map (Sign.read_class thy) raw_superclasses;
    1.47 -    val name_atts = map ((apsnd o map) (Attrib.attribute thy) o fst)
    1.48 -      raw_specs;
    1.49 -    val axiomss = ProofContext.read_propp (ctxt, map (map (rpair []) o snd)
    1.50 -          raw_specs)
    1.51 -      |> snd
    1.52 -      |> (map o map) fst;
    1.53 -  in
    1.54 -    AxClass.define_class (class, superclasses) []
    1.55 -      (name_atts ~~ axiomss) thy
    1.56 -  end;
    1.57 -
    1.58 -local
    1.59 -
    1.60 -fun gen_instance mk_prop add_thm after_qed insts thy =
    1.61 -  let
    1.62 -    fun after_qed' results =
    1.63 -      ProofContext.theory ((fold o fold) add_thm results #> after_qed);
    1.64 -  in
    1.65 -    thy
    1.66 -    |> ProofContext.init
    1.67 -    |> Proof.theorem_i NONE after_qed' ((map (fn t => [(t, [])])
    1.68 -        o mk_prop thy) insts)
    1.69 -  end;
    1.70 -
    1.71 -in
    1.72 -
    1.73 -val instance_arity =
    1.74 -  gen_instance (Logic.mk_arities oo Sign.cert_arity) AxClass.add_arity;
    1.75 -val instance_arity_cmd =
    1.76 -  gen_instance (Logic.mk_arities oo Sign.read_arity) AxClass.add_arity I;
    1.77 -val classrel =
    1.78 -  gen_instance (single oo (Logic.mk_classrel oo AxClass.cert_classrel)) AxClass.add_classrel I;
    1.79 -val classrel_cmd =
    1.80 -  gen_instance (single oo (Logic.mk_classrel oo AxClass.read_classrel)) AxClass.add_classrel I;
    1.81 -
    1.82 -end; (*local*)
    1.83 -
    1.84 -
    1.85  (** class data **)
    1.86  
    1.87  datatype class_data = ClassData of {
    1.88 @@ -276,7 +235,7 @@
    1.89        [Option.map (Drule.standard' o Element.conclude_witness) some_wit,
    1.90          (fst o rules thy) sub];
    1.91      val tac = EVERY (map (TRYALL o Tactic.rtac) intros);
    1.92 -    val classrel = Goal.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
    1.93 +    val classrel = SkipProof.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
    1.94        (K tac);
    1.95      val diff_sort = Sign.complete_sort thy [sup]
    1.96        |> subtract (op =) (Sign.complete_sort thy [sub])
    1.97 @@ -403,6 +362,30 @@
    1.98    end;
    1.99  
   1.100  
   1.101 +(* simple subclasses *)
   1.102 +
   1.103 +local
   1.104 +
   1.105 +fun gen_classrel mk_prop classrel thy =
   1.106 +  let
   1.107 +    fun after_qed results =
   1.108 +      ProofContext.theory ((fold o fold) AxClass.add_classrel results);
   1.109 +  in
   1.110 +    thy
   1.111 +    |> ProofContext.init
   1.112 +    |> Proof.theorem_i NONE after_qed [[(mk_prop thy classrel, [])]]
   1.113 +  end;
   1.114 +
   1.115 +in
   1.116 +
   1.117 +val classrel =
   1.118 +  gen_classrel (Logic.mk_classrel oo AxClass.cert_classrel);
   1.119 +val classrel_cmd =
   1.120 +  gen_classrel (Logic.mk_classrel oo AxClass.read_classrel);
   1.121 +
   1.122 +end; (*local*)
   1.123 +
   1.124 +
   1.125  (** instantiation target **)
   1.126  
   1.127  (* bookkeeping *)
   1.128 @@ -593,6 +576,20 @@
   1.129    end;
   1.130  
   1.131  
   1.132 +(* simplified instantiation interface with no class parameter *)
   1.133 +
   1.134 +fun instance_arity_cmd arities thy =
   1.135 +  let
   1.136 +    fun after_qed results = ProofContext.theory
   1.137 +      ((fold o fold) AxClass.add_arity results);
   1.138 +  in
   1.139 +    thy
   1.140 +    |> ProofContext.init
   1.141 +    |> Proof.theorem_i NONE after_qed ((map (fn t => [(t, [])])
   1.142 +        o Logic.mk_arities o Sign.read_arity thy) arities)
   1.143 +  end;
   1.144 +
   1.145 +
   1.146  (** tactics and methods **)
   1.147  
   1.148  fun intro_classes_tac facts st =
   1.149 @@ -620,5 +617,24 @@
   1.150    Method.setup (Binding.name "default") (Attrib.thms >> (METHOD oo default_tac))
   1.151      "apply some intro/elim rule"));
   1.152  
   1.153 +
   1.154 +(** old axclass command **)
   1.155 +
   1.156 +fun axclass_cmd (class, raw_superclasses) raw_specs thy =
   1.157 +  let
   1.158 +    val _ = Output.legacy_feature "command \"axclass\" deprecated; use \"class\" instead.";
   1.159 +    val ctxt = ProofContext.init thy;
   1.160 +    val superclasses = map (Sign.read_class thy) raw_superclasses;
   1.161 +    val name_atts = map ((apsnd o map) (Attrib.attribute thy) o fst)
   1.162 +      raw_specs;
   1.163 +    val axiomss = ProofContext.read_propp (ctxt, map (map (rpair []) o snd)
   1.164 +          raw_specs)
   1.165 +      |> snd
   1.166 +      |> (map o map) fst;
   1.167 +  in
   1.168 +    AxClass.define_class (class, superclasses) []
   1.169 +      (name_atts ~~ axiomss) thy
   1.170 +  end;
   1.171 +
   1.172  end;
   1.173