explicit constants for overloaded definitions
authorhaftmann
Fri Aug 17 13:58:58 2007 +0200 (2007-08-17)
changeset 2430469d40a562ba4
parent 24303 32b67bdf2c3a
child 24305 b1df9e31cda1
explicit constants for overloaded definitions
src/HOL/Relation_Power.thy
src/Pure/Isar/class.ML
     1.1 --- a/src/HOL/Relation_Power.thy	Fri Aug 17 13:58:57 2007 +0200
     1.2 +++ b/src/HOL/Relation_Power.thy	Fri Aug 17 13:58:58 2007 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4        --{* only type @{typ "('a * 'a) set"} should be in class @{text power}!*}
     1.5  
     1.6  (*R^n = R O ... O R, the n-fold composition of R*)
     1.7 -primrec (relpow)
     1.8 +primrec (unchecked relpow)
     1.9    "R^0 = Id"
    1.10    "R^(Suc n) = R O (R^n)"
    1.11  
    1.12 @@ -25,7 +25,7 @@
    1.13        --{* only type @{typ "'a => 'a"} should be in class @{text power}!*}
    1.14  
    1.15  (*f^n = f o ... o f, the n-fold composition of f*)
    1.16 -primrec (funpow)
    1.17 +primrec (unchecked funpow)
    1.18    "f^0 = id"
    1.19    "f^(Suc n) = f o (f^n)"
    1.20  
     2.1 --- a/src/Pure/Isar/class.ML	Fri Aug 17 13:58:57 2007 +0200
     2.2 +++ b/src/Pure/Isar/class.ML	Fri Aug 17 13:58:58 2007 +0200
     2.3 @@ -33,6 +33,10 @@
     2.4    val add_const_in_class: string -> (string * term) * Syntax.mixfix
     2.5      -> theory -> theory
     2.6  
     2.7 +  val unoverload: theory -> thm -> thm
     2.8 +  val overload: theory -> thm -> thm
     2.9 +  val inst_const: theory -> string * string -> string
    2.10 +
    2.11    val print_classes: theory -> unit
    2.12    val intro_classes_tac: thm list -> tactic
    2.13    val default_intro_classes_tac: thm list -> tactic
    2.14 @@ -122,6 +126,67 @@
    2.15    end;
    2.16  
    2.17  
    2.18 +(* explicit constants for overloaded definitions *)
    2.19 +
    2.20 +structure InstData = TheoryDataFun
    2.21 +(
    2.22 +  type T = (string * thm) Symtab.table Symtab.table;
    2.23 +    (*constant name ~> type constructor ~> (constant name, equation)*)
    2.24 +  val empty = Symtab.empty;
    2.25 +  val copy = I;
    2.26 +  val extend = I;
    2.27 +  fun merge _ = Symtab.join (K (Symtab.merge (K true)));
    2.28 +);
    2.29 +
    2.30 +fun inst_thms f thy =
    2.31 +  Symtab.fold (Symtab.fold (cons o f o snd o snd) o snd) (InstData.get thy) [];
    2.32 +fun add_inst (c, tyco) inst = (InstData.map o Symtab.map_default (c, Symtab.empty))
    2.33 +  (Symtab.update_new (tyco, inst));
    2.34 +
    2.35 +fun unoverload thy thm = MetaSimplifier.rewrite_rule (inst_thms I thy) thm;
    2.36 +fun overload thy thm = MetaSimplifier.rewrite_rule (inst_thms symmetric thy) thm;
    2.37 +
    2.38 +fun inst_const thy (c, tyco) =
    2.39 +  (fst o the o Symtab.lookup ((the o Symtab.lookup (InstData.get thy)) c)) tyco;
    2.40 +
    2.41 +fun add_inst_def (class, tyco) (c, ty) thy =
    2.42 +  let
    2.43 +    val tyco_base = NameSpace.base tyco;
    2.44 +    val name_inst = NameSpace.base class ^ "_" ^ tyco_base ^ "_inst";
    2.45 +    val c_inst_base = NameSpace.base c ^ "_" ^ tyco_base;
    2.46 +  in
    2.47 +    thy
    2.48 +    |> Sign.sticky_prefix name_inst
    2.49 +    |> Sign.add_consts_i [(c_inst_base, ty, Syntax.NoSyn)]
    2.50 +    |> `(fn thy => Sign.full_name thy c_inst_base)
    2.51 +    |-> (fn c_inst => PureThy.add_defs_i true
    2.52 +          [((Thm.def_name c_inst_base, Logic.mk_equals (Const (c_inst, ty), Const (c, ty))), [])]
    2.53 +    #-> (fn [def] => add_inst (c, tyco) (c_inst, symmetric def))
    2.54 +    #> Sign.restore_naming thy)
    2.55 +  end;
    2.56 +
    2.57 +fun add_inst_def' (class, tyco) (c, ty) thy =
    2.58 +  if case Symtab.lookup (InstData.get thy) c
    2.59 +   of NONE => true
    2.60 +    | SOME tab => is_none (Symtab.lookup tab tyco)
    2.61 +  then add_inst_def (class, tyco) (c, Logic.unvarifyT ty) thy
    2.62 +  else thy;
    2.63 +
    2.64 +fun add_def ((class, tyco), ((name, prop), atts)) thy =
    2.65 +  let
    2.66 +    val ((lhs as Const (c, ty), args), rhs) = (apfst Term.strip_comb o Logic.dest_equals) prop;
    2.67 +    fun add_inst' def ([], (Const (c_inst, ty))) =
    2.68 +          if forall (fn TFree_ => true | _ => false) (Sign.const_typargs thy (c_inst, ty))
    2.69 +          then add_inst (c, tyco) (c_inst, def)
    2.70 +          else add_inst_def (class, tyco) (c, ty)
    2.71 +      | add_inst' _ t = add_inst_def (class, tyco) (c, ty);
    2.72 +  in
    2.73 +    thy
    2.74 +    |> PureThy.add_defs_i true [((name, prop), map (Attrib.attribute thy) atts)]
    2.75 +    |-> (fn [def] => add_inst' def (args, rhs) #> pair def)
    2.76 +  end;
    2.77 +
    2.78 +
    2.79  (* instances with implicit parameter handling *)
    2.80  
    2.81  local
    2.82 @@ -154,7 +219,7 @@
    2.83          val cs = (these o Option.map snd o try (AxClass.params_of_class theory)) class;
    2.84          val subst_ty = map_type_tfree (K ty);
    2.85        in
    2.86 -        map (fn (c, ty) => (c, ((tyco, class), subst_ty ty))) cs
    2.87 +        map (fn (c, ty) => (c, ((class, tyco), subst_ty ty))) cs
    2.88        end;
    2.89      fun get_consts_sort (tyco, asorts, sort) =
    2.90        let
    2.91 @@ -171,7 +236,7 @@
    2.92            let
    2.93              val (c, (inst, ((name_opt, t), atts))) = read_def thy_read raw_def;
    2.94              val ty = Consts.instance (Sign.consts_of thy_read) (c, inst);
    2.95 -            val ((tyco, class), ty') = case AList.lookup (op =) cs c
    2.96 +            val ((class, tyco), ty') = case AList.lookup (op =) cs c
    2.97               of NONE => error ("illegal definition for constant " ^ quote c)
    2.98                | SOME class_ty => class_ty;
    2.99              val name = case name_opt
   2.100 @@ -184,7 +249,7 @@
   2.101                | SOME norm => map_types norm t
   2.102            in (((class, tyco), ((name, t'), atts)), AList.delete (op =) c cs) end;
   2.103        in fold_map read defs cs end;
   2.104 -    val (defs, _) = read_defs raw_defs cs
   2.105 +    val (defs, other_cs) = read_defs raw_defs cs
   2.106        (fold Sign.primitive_arity arities (Theory.copy theory));
   2.107      fun get_remove_contraint c thy =
   2.108        let
   2.109 @@ -194,18 +259,14 @@
   2.110          |> Sign.add_const_constraint_i (c, NONE)
   2.111          |> pair (c, Logic.unvarifyT ty)
   2.112        end;
   2.113 -    fun add_defs defs thy =
   2.114 -      thy
   2.115 -      |> PureThy.add_defs_i true (map ((apsnd o map) (Attrib.attribute thy) o snd) defs)
   2.116 -      |-> (fn thms => pair (map fst defs ~~ thms));
   2.117 -    fun after_qed cs defs thy =
   2.118 -      thy
   2.119 -      |> fold Sign.add_const_constraint_i (map (apsnd SOME) cs)
   2.120 -      |> fold (Code.add_func false o snd) defs;
   2.121 +    fun after_qed cs defs =
   2.122 +      fold Sign.add_const_constraint_i (map (apsnd SOME) cs)
   2.123 +      #> fold (Code.add_func false) defs;
   2.124    in
   2.125      theory
   2.126      |> fold_map get_remove_contraint (map fst cs |> distinct (op =))
   2.127 -    ||>> add_defs defs
   2.128 +    ||>> fold_map add_def defs
   2.129 +    ||> fold (fn (c, ((class, tyco), ty)) => add_inst_def' (class, tyco) (c, ty)) other_cs
   2.130      |-> (fn (cs, defs) => do_proof (after_qed cs defs) arities)
   2.131    end;
   2.132