src/Pure/Isar/class.ML
changeset 25485 33840a854e63
parent 25462 dad0291cb76a
child 25502 9200b36280c0
     1.1 --- a/src/Pure/Isar/class.ML	Wed Nov 28 09:01:40 2007 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Wed Nov 28 09:01:42 2007 +0100
     1.3 @@ -12,35 +12,42 @@
     1.4      -> string list -> theory -> string * Proof.context
     1.5    val class_cmd: bstring -> xstring list -> Element.context Locale.element list
     1.6      -> xstring list -> theory -> string * Proof.context
     1.7 -  val is_class: theory -> class -> bool
     1.8 -  val these_params: theory -> sort -> (string * (string * typ)) list
     1.9 +
    1.10    val init: class -> theory -> Proof.context
    1.11 -  val add_logical_const: string -> Markup.property list
    1.12 +  val logical_const: string -> Markup.property list
    1.13      -> (string * mixfix) * term -> theory -> theory
    1.14 -  val add_syntactic_const: string -> Syntax.mode -> Markup.property list
    1.15 +  val syntactic_const: string -> Syntax.mode -> Markup.property list
    1.16      -> (string * mixfix) * term -> theory -> theory
    1.17    val refresh_syntax: class -> Proof.context -> Proof.context
    1.18 +
    1.19    val intro_classes_tac: thm list -> tactic
    1.20    val default_intro_classes_tac: thm list -> tactic
    1.21    val prove_subclass: class * class -> thm list -> Proof.context
    1.22      -> theory -> theory
    1.23 +
    1.24 +  val class_prefix: string -> string
    1.25 +  val is_class: theory -> class -> bool
    1.26 +  val these_params: theory -> sort -> (string * (string * typ)) list
    1.27    val print_classes: theory -> unit
    1.28 -  val class_prefix: string -> string
    1.29  
    1.30    (*instances*)
    1.31 -  val declare_overloaded: string * typ * mixfix -> theory -> term * theory
    1.32 -  val define_overloaded: string -> string * term -> theory -> thm * theory
    1.33 -  val unoverload: theory -> conv
    1.34 -  val overload: theory -> conv
    1.35 +  val init_instantiation: arity list -> theory -> local_theory
    1.36 +  val instantiation_instance: (local_theory -> local_theory) -> local_theory -> Proof.state
    1.37 +  val prove_instantiation_instance: (Proof.context -> tactic) -> local_theory -> local_theory
    1.38 +  val conclude_instantiation: local_theory -> local_theory
    1.39 +
    1.40 +  val overloaded_const: string * typ * mixfix -> theory -> term * theory
    1.41 +  val overloaded_def: string -> string * term -> theory -> thm * theory
    1.42 +  val instantiation_param: Proof.context -> string -> string option
    1.43 +  val confirm_declaration: string -> local_theory -> local_theory
    1.44 +
    1.45 +  val unoverload: theory -> thm -> thm
    1.46 +  val overload: theory -> thm -> thm
    1.47 +  val unoverload_conv: theory -> conv
    1.48 +  val overload_conv: theory -> conv
    1.49    val unoverload_const: theory -> string * typ -> string
    1.50 -  val inst_const: theory -> string * string -> string
    1.51 -  val param_const: theory -> string -> (string * string) option
    1.52 -  val instantiation: arity list -> theory -> local_theory
    1.53 -  val proof_instantiation: (local_theory -> local_theory) -> local_theory -> Proof.state
    1.54 -  val prove_instantiation: (Proof.context -> tactic) -> local_theory -> local_theory
    1.55 -  val conclude_instantiation: local_theory -> local_theory
    1.56 -  val end_instantiation: local_theory -> Proof.context
    1.57 -  val instantiation_const: Proof.context -> string -> string option
    1.58 +  val param_of_inst: theory -> string * string -> string
    1.59 +  val inst_of_param: theory -> string -> (string * string) option
    1.60  
    1.61    (*old axclass layer*)
    1.62    val axclass_cmd: bstring * xstring list
    1.63 @@ -109,7 +116,7 @@
    1.64    end;
    1.65  
    1.66  
    1.67 -(** axclass command **)
    1.68 +(** primitive axclass and instance commands **)
    1.69  
    1.70  fun axclass_cmd (class, raw_superclasses) raw_specs thy =
    1.71    let
    1.72 @@ -175,26 +182,27 @@
    1.73  fun inst thy (c, tyco) =
    1.74    (the o Symtab.lookup ((the o Symtab.lookup (fst (InstData.get thy))) c)) tyco;
    1.75  
    1.76 -val inst_const = fst oo inst;
    1.77 +val param_of_inst = fst oo inst;
    1.78  
    1.79  fun inst_thms thy = (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst)
    1.80    (InstData.get thy) [];
    1.81  
    1.82 -val param_const = Symtab.lookup o snd o InstData.get;
    1.83 +val inst_of_param = Symtab.lookup o snd o InstData.get;
    1.84  
    1.85  fun add_inst (c, tyco) inst = (InstData.map o apfst
    1.86        o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst))
    1.87    #> (InstData.map o apsnd) (Symtab.update_new (fst inst, (c, tyco)));
    1.88  
    1.89 -fun unoverload thy = MetaSimplifier.rewrite true (inst_thms thy);
    1.90 -fun overload thy = MetaSimplifier.rewrite true (map Thm.symmetric (inst_thms thy));
    1.91 +fun unoverload thy = MetaSimplifier.simplify true (inst_thms thy);
    1.92 +fun overload thy = MetaSimplifier.simplify true (map Thm.symmetric (inst_thms thy));
    1.93 +
    1.94 +fun unoverload_conv thy = MetaSimplifier.rewrite true (inst_thms thy);
    1.95 +fun overload_conv thy = MetaSimplifier.rewrite true (map Thm.symmetric (inst_thms thy));
    1.96  
    1.97  fun unoverload_const thy (c_ty as (c, _)) =
    1.98    case AxClass.class_of_param thy c
    1.99     of SOME class => (case inst_tyco thy c_ty
   1.100 -       of SOME tyco => (case try (inst thy) (c, tyco)
   1.101 -             of SOME (c, _) => c
   1.102 -              | NONE => c)
   1.103 +       of SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
   1.104          | NONE => c)
   1.105      | NONE => c;
   1.106  
   1.107 @@ -205,18 +213,20 @@
   1.108    PureThy.note_thmss_i kind [((name, []), [([thm], [])])]
   1.109    #>> (fn [(_, [thm])] => thm);
   1.110  
   1.111 -fun declare_overloaded (c, ty, mx) thy =
   1.112 +fun overloaded_const (c, ty, mx) thy =
   1.113    let
   1.114 +    val _ = if mx <> NoSyn then
   1.115 +      error ("Illegal mixfix syntax for constant to be instantiated " ^ quote c)
   1.116 +      else ()
   1.117      val SOME class = AxClass.class_of_param thy c;
   1.118      val SOME tyco = inst_tyco thy (c, ty);
   1.119 -    val name_inst = NameSpace.base class ^ "_" ^ NameSpace.base tyco ^ "_inst";
   1.120 +    val name_inst = AxClass.instance_name (tyco, class) ^ "_inst";
   1.121      val c' = NameSpace.base c;
   1.122      val ty' = Type.strip_sorts ty;
   1.123    in
   1.124      thy
   1.125      |> Sign.sticky_prefix name_inst
   1.126      |> Sign.no_base_names
   1.127 -    |> Sign.notation true Syntax.mode_default [(Const (c, ty), mx)]
   1.128      |> Sign.declare_const [] (c', ty', NoSyn)
   1.129      |-> (fn const' as Const (c'', _) => Thm.add_def true
   1.130            (Thm.def_name c', Logic.mk_equals (Const (c, ty'), const'))
   1.131 @@ -228,22 +238,18 @@
   1.132      #> pair (Const (c, ty))))
   1.133    end;
   1.134  
   1.135 -fun define_overloaded name (c, t) thy =
   1.136 +fun overloaded_def name (c, t) thy =
   1.137    let
   1.138      val ty = Term.fastype_of t;
   1.139      val SOME tyco = inst_tyco thy (c, ty);
   1.140      val (c', eq) = inst thy (c, tyco);
   1.141 -    val [Type (_, tys)] = Sign.const_typargs thy (c, ty);
   1.142 -    val eq' = eq
   1.143 -      |> Drule.instantiate' (map (SOME o Thm.ctyp_of thy) tys) [];
   1.144 -          (*FIXME proper recover_sort mechanism*)
   1.145      val prop = Logic.mk_equals (Const (c', ty), t);
   1.146 -    val name' = if name = "" then
   1.147 -      Thm.def_name (NameSpace.base c ^ "_" ^ NameSpace.base tyco) else name;
   1.148 +    val name' = Thm.def_name_optional
   1.149 +      (NameSpace.base c ^ "_" ^ NameSpace.base tyco) name;
   1.150    in
   1.151      thy
   1.152      |> Thm.add_def false (name', prop)
   1.153 -    |>> (fn thm => Thm.transitive eq' thm)
   1.154 +    |>> (fn thm =>  Drule.transitive_thm OF [eq, thm])
   1.155    end;
   1.156  
   1.157  
   1.158 @@ -911,9 +917,9 @@
   1.159  end; (*local*)
   1.160  
   1.161  
   1.162 -(* definition in class target *)
   1.163 +(* class target *)
   1.164  
   1.165 -fun add_logical_const class pos ((c, mx), dict) thy =
   1.166 +fun logical_const class pos ((c, mx), dict) thy =
   1.167    let
   1.168      val prfx = class_prefix class;
   1.169      val thy' = thy |> Sign.add_path prfx;
   1.170 @@ -928,7 +934,7 @@
   1.171    in
   1.172      thy'
   1.173      |> Sign.declare_const pos (c, ty'', mx) |> snd
   1.174 -    |> Thm.add_def false (c, def_eq)    (* FIXME PureThy.add_defs_i *)
   1.175 +    |> Thm.add_def false (c, def_eq)
   1.176      |>> Thm.symmetric
   1.177      |-> (fn def => class_interpretation class [def] [Thm.prop_of def]
   1.178            #> register_operation class (c', (dict', SOME (Thm.varifyT def))))
   1.179 @@ -936,10 +942,7 @@
   1.180      |> Sign.add_const_constraint (c', SOME ty')
   1.181    end;
   1.182  
   1.183 -
   1.184 -(* abbreviation in class target *)
   1.185 -
   1.186 -fun add_syntactic_const class prmode pos ((c, mx), rhs) thy =
   1.187 +fun syntactic_const class prmode pos ((c, mx), rhs) thy =
   1.188    let
   1.189      val prfx = class_prefix class;
   1.190      val thy' = thy |> Sign.add_path prfx;
   1.191 @@ -974,51 +977,26 @@
   1.192    fun init _ = Instantiation { arities = [], params = [] };
   1.193  );
   1.194  
   1.195 -fun mk_instantiation (arities, params) = Instantiation {
   1.196 -    arities = arities, params = params
   1.197 -  };
   1.198 +fun mk_instantiation (arities, params) =
   1.199 +  Instantiation { arities = arities, params = params };
   1.200 +fun get_instantiation ctxt = case Instantiation.get ctxt
   1.201 + of Instantiation data => data;
   1.202  fun map_instantiation f (Instantiation { arities, params }) =
   1.203    mk_instantiation (f (arities, params));
   1.204  
   1.205 -fun the_instantiation ctxt = case Instantiation.get ctxt
   1.206 - of Instantiation { arities = [], ... } => error "No instantiation target"
   1.207 -  | Instantiation data => data;
   1.208 +fun the_instantiation ctxt = case get_instantiation ctxt
   1.209 + of { arities = [], ... } => error "No instantiation target"
   1.210 +  | data => data;
   1.211  
   1.212 -fun init_instantiation arities ctxt =
   1.213 -  let
   1.214 -    val thy = ProofContext.theory_of ctxt;
   1.215 -    val _ = if null arities then error "At least one arity must be given" else ();
   1.216 -    val _ = case (duplicates (op =) o map #1) arities
   1.217 -     of [] => ()
   1.218 -      | dupl_tycos => error ("Type constructors occur more than once in arities: "
   1.219 -          ^ commas_quote dupl_tycos);
   1.220 -    val ty_insts = map (fn (tyco, sorts, _) =>
   1.221 -        (tyco, Type (tyco, map TFree (Name.names Name.context Name.aT sorts))))
   1.222 -      arities;
   1.223 -    val ty_inst = the o AList.lookup (op =) ty_insts;
   1.224 -    fun type_name "*" = "prod"
   1.225 -      | type_name "+" = "sum"
   1.226 -      | type_name s = NameSpace.base s; (*FIXME*)
   1.227 -    fun get_param tyco sorts (param, (c, ty)) =
   1.228 -      ((unoverload_const thy (c, ty), tyco),
   1.229 -        (param ^ "_" ^ type_name tyco,
   1.230 -          map_atyps (K (ty_inst tyco)) ty));
   1.231 -    fun get_params (tyco, sorts, sort) =
   1.232 -      map (get_param tyco sorts) (these_params thy sort)
   1.233 -    val params = maps get_params arities;
   1.234 -  in
   1.235 -    ctxt
   1.236 -    |> Instantiation.put (mk_instantiation (arities, params))
   1.237 -    |> fold (Variable.declare_term o Logic.mk_type o snd) ty_insts
   1.238 -    |> fold (Variable.declare_term o Free o snd) params
   1.239 -  end;
   1.240 +val instantiation_params = #params o get_instantiation;
   1.241  
   1.242 -val instantiation_params = #params o the_instantiation;
   1.243 -
   1.244 -fun instantiation_const ctxt v = instantiation_params ctxt
   1.245 +fun instantiation_param ctxt v = instantiation_params ctxt
   1.246    |> find_first (fn (_, (v', _)) => v = v')
   1.247    |> Option.map (fst o fst);
   1.248  
   1.249 +fun confirm_declaration c = (Instantiation.map o map_instantiation o apsnd)
   1.250 +  (filter_out (fn (_, (c', _)) => c' = c));
   1.251 +
   1.252  
   1.253  (* syntax *)
   1.254  
   1.255 @@ -1057,21 +1035,58 @@
   1.256  
   1.257  (* target *)
   1.258  
   1.259 -fun instantiation arities =
   1.260 -  ProofContext.init
   1.261 -  #> init_instantiation arities
   1.262 -  #> fold ProofContext.add_arity arities
   1.263 -  #> Context.proof_map (
   1.264 -      Syntax.add_term_check 0 "instance" inst_term_check
   1.265 -      #> Syntax.add_term_uncheck 0 "instance" inst_term_uncheck);
   1.266 +val sanatize_name = (*FIXME*)
   1.267 +  let
   1.268 +    fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse s = "'";
   1.269 +    val is_junk = not o is_valid andf Symbol.is_regular;
   1.270 +    val junk = Scan.many is_junk;
   1.271 +    val scan_valids = Symbol.scanner "Malformed input"
   1.272 +      ((junk |--
   1.273 +        (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode)
   1.274 +        --| junk))
   1.275 +      -- Scan.repeat ((Scan.many1 is_valid >> implode) --| junk) >> op ::);
   1.276 +  in
   1.277 +    explode #> scan_valids #> implode
   1.278 +  end;
   1.279 +
   1.280  
   1.281 -fun gen_proof_instantiation do_proof after_qed lthy =
   1.282 +fun init_instantiation arities thy =
   1.283    let
   1.284 -    (*FIXME should work on fresh context but continue local theory afterwards*)
   1.285 +    val _ = if null arities then error "At least one arity must be given" else ();
   1.286 +    val _ = case (duplicates (op =) o map #1) arities
   1.287 +     of [] => ()
   1.288 +      | dupl_tycos => error ("Type constructors occur more than once in arities: "
   1.289 +          ^ commas_quote dupl_tycos);
   1.290 +    val ty_insts = map (fn (tyco, sorts, _) =>
   1.291 +        (tyco, Type (tyco, map TFree (Name.names Name.context Name.aT sorts))))
   1.292 +      arities;
   1.293 +    val ty_inst = the o AList.lookup (op =) ty_insts;
   1.294 +    fun type_name "*" = "prod"
   1.295 +      | type_name "+" = "sum"
   1.296 +      | type_name s = sanatize_name (NameSpace.base s); (*FIXME*)
   1.297 +    fun get_param tyco sorts (param, (c, ty)) =
   1.298 +      ((unoverload_const thy (c, ty), tyco),
   1.299 +        (param ^ "_" ^ type_name tyco,
   1.300 +          map_atyps (K (ty_inst tyco)) ty));
   1.301 +    fun get_params (tyco, sorts, sort) =
   1.302 +      map (get_param tyco sorts) (these_params thy sort)
   1.303 +    val params = maps get_params arities;
   1.304 +  in
   1.305 +    thy
   1.306 +    |> ProofContext.init
   1.307 +    |> Instantiation.put (mk_instantiation (arities, params))
   1.308 +    |> fold (Variable.declare_term o Logic.mk_type o snd) ty_insts
   1.309 +    |> fold ProofContext.add_arity arities
   1.310 +    |> Context.proof_map (
   1.311 +        Syntax.add_term_check 0 "instance" inst_term_check
   1.312 +        #> Syntax.add_term_uncheck 0 "instance" inst_term_uncheck)
   1.313 +  end;
   1.314 +
   1.315 +fun gen_instantiation_instance do_proof after_qed lthy =
   1.316 +  let
   1.317      val ctxt = LocalTheory.target_of lthy;
   1.318      val arities = (#arities o the_instantiation) ctxt;
   1.319 -    val arities_proof = maps
   1.320 -      (Logic.mk_arities o Sign.cert_arity (ProofContext.theory_of ctxt)) arities;
   1.321 +    val arities_proof = maps Logic.mk_arities arities;
   1.322      fun after_qed' results =
   1.323        LocalTheory.theory (fold (AxClass.add_arity o Thm.varifyT) results)
   1.324        #> after_qed;
   1.325 @@ -1080,16 +1095,16 @@
   1.326      |> do_proof after_qed' arities_proof
   1.327    end;
   1.328  
   1.329 -val proof_instantiation = gen_proof_instantiation (fn after_qed => fn ts =>
   1.330 +val instantiation_instance = gen_instantiation_instance (fn after_qed => fn ts =>
   1.331    Proof.theorem_i NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts));
   1.332  
   1.333 -fun prove_instantiation tac = gen_proof_instantiation (fn after_qed =>
   1.334 +fun prove_instantiation_instance tac = gen_instantiation_instance (fn after_qed =>
   1.335    fn ts => fn lthy => after_qed (Goal.prove_multi lthy [] [] ts
   1.336      (fn {context, ...} => tac context)) lthy) I;
   1.337  
   1.338  fun conclude_instantiation lthy =
   1.339    let
   1.340 -    val arities = (#arities o the_instantiation) lthy;
   1.341 +    val { arities, params } = the_instantiation lthy;
   1.342      val thy = ProofContext.theory_of lthy;
   1.343      (*val _ = map (fn (tyco, sorts, sort) =>
   1.344        if Sign.of_sort thy
   1.345 @@ -1101,20 +1116,21 @@
   1.346      val missing_params = arities
   1.347        |> maps (fn (tyco, _, sort) => params_of sort |> map (rpair tyco))
   1.348        |> filter_out (can (inst thy) o apfst fst);
   1.349 -    fun declare_missing ((c, ty), tyco) thy =
   1.350 +    fun declare_missing ((c, ty0), tyco) thy =
   1.351 +    (*fun declare_missing ((c, tyco), (_, ty)) thy =*)
   1.352        let
   1.353          val SOME class = AxClass.class_of_param thy c;
   1.354 -        val name_inst = NameSpace.base class ^ "_" ^ NameSpace.base tyco ^ "_inst";
   1.355 +        val name_inst = AxClass.instance_name (tyco, class) ^ "_inst";
   1.356 +        val c' = NameSpace.base c;
   1.357          val vs = Name.names Name.context Name.aT (replicate (Sign.arity_number thy tyco) []);
   1.358 -        val ty' = map_atyps (fn _ => Type (tyco, map TFree vs)) ty;
   1.359 -        val c' = NameSpace.base c;
   1.360 +        val ty = map_atyps (fn _ => Type (tyco, map TFree vs)) ty0;
   1.361        in
   1.362          thy
   1.363          |> Sign.sticky_prefix name_inst
   1.364          |> Sign.no_base_names
   1.365 -        |> Sign.declare_const [] (c', ty', NoSyn)
   1.366 +        |> Sign.declare_const [] (c', ty, NoSyn)
   1.367          |-> (fn const' as Const (c'', _) => Thm.add_def true
   1.368 -              (Thm.def_name c', Logic.mk_equals (const', Const (c, ty')))
   1.369 +              (Thm.def_name c', Logic.mk_equals (const', Const (c, ty)))
   1.370          #>> Thm.varifyT
   1.371          #-> (fn thm => add_inst (c, tyco) (c'', Thm.symmetric thm)
   1.372          #> primitive_note Thm.internalK (c', thm)
   1.373 @@ -1126,6 +1142,4 @@
   1.374      |> LocalTheory.theory (fold declare_missing missing_params)
   1.375    end;
   1.376  
   1.377 -val end_instantiation = conclude_instantiation #> LocalTheory.target_of;
   1.378 -
   1.379  end;