refined overloading target

--- a/src/HOL/Relation_Power.thy	Tue Jan 08 10:24:34 2008 +0100
+++ b/src/HOL/Relation_Power.thy	Tue Jan 08 11:37:27 2008 +0100
@@ -14,20 +14,33 @@
   set :: (type) power ..
       --{* only type @{typ "('a * 'a) set"} should be in class @{text power}!*}
 
-(*R^n = R O ... O R, the n-fold composition of R*)
-primrec (unchecked relpow)
-  "R^0 = Id"
-  "R^(Suc n) = R O (R^n)"
+overloading
+  relpow \<equiv> "power \<Colon> ('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a \<times> 'a) set"  (unchecked)
+begin
+
+text {* @{text "R ^ n = R O ... O R"}, the n-fold composition of @{text R} *}
 
+primrec relpow where
+  "(R \<Colon> ('a \<times> 'a) set)  ^ 0 = Id"
+  | "(R \<Colon> ('a \<times> 'a) set) ^ Suc n = R O (R ^ n)"
+
+end
 
 instance
   "fun" :: (type, type) power ..
       --{* only type @{typ "'a => 'a"} should be in class @{text power}!*}
 
-(*f^n = f o ... o f, the n-fold composition of f*)
-primrec (unchecked funpow)
-  "f^0 = id"
-  "f^(Suc n) = f o (f^n)"
+overloading
+  funpow \<equiv> "power \<Colon>  ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" (unchecked)
+begin
+
+text {* @{text "f ^ n = f o ... o f"}, the n-fold composition of @{text f} *}
+
+primrec funpow where
+  "(f \<Colon> 'a \<Rightarrow> 'a) ^ 0 = id"
+  | "(f \<Colon> 'a \<Rightarrow> 'a) ^ Suc n = f o (f ^ n)"
+
+end
 
 text{*WARNING: due to the limits of Isabelle's type classes, exponentiation on
 functions and relations has too general a domain, namely @{typ "('a * 'b)set"}
@@ -39,17 +52,14 @@
   Circumvent this problem for code generation:
 *}
 
-definition
-  funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
+primrec
+  fun_pow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
 where
-  funpow_def: "funpow n f = f ^ n"
+  "fun_pow 0 f = id"
+  | "fun_pow (Suc n) f = f o fun_pow n f"
 
-lemmas [code inline] = funpow_def [symmetric]
-
-lemma [code func]:
-  "funpow 0 f = id"
-  "funpow (Suc n) f = f o funpow n f"
-  unfolding funpow_def by simp_all
+lemma funpow_fun_pow [code inline]: "f ^ n = fun_pow n f"
+  unfolding funpow_def fun_pow_def ..
 
 lemma funpow_add: "f ^ (m+n) = f^m o f^n"
   by (induct m) simp_all

--- a/src/Pure/Isar/isar_syn.ML	Tue Jan 08 10:24:34 2008 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Tue Jan 08 11:37:27 2008 +0100
@@ -463,7 +463,7 @@
 
 val _ =
   OuterSyntax.command "overloading" "overloaded definitions" K.thy_decl
-   (Scan.repeat1 (P.xname --| P.$$$ "::" -- P.typ --| P.$$$ "is" -- P.name --
+   (Scan.repeat1 (P.name --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.term --
       Scan.optional (P.$$$ "(" |-- (P.$$$ "unchecked" >> K false) --| P.$$$ ")") true)
         --| P.begin
    >> (fn operations => Toplevel.print o

--- a/src/Pure/Isar/overloading.ML	Tue Jan 08 10:24:34 2008 +0100
+++ b/src/Pure/Isar/overloading.ML	Tue Jan 08 11:37:27 2008 +0100
@@ -7,7 +7,7 @@
 
 signature OVERLOADING =
 sig
-  val init: ((string * typ) * (string * bool)) list -> theory -> local_theory
+  val init: (string * (string * typ) * bool) list -> theory -> local_theory
   val conclude: local_theory -> local_theory
   val declare: string * typ -> theory -> term * theory
   val confirm: string -> local_theory -> local_theory
@@ -75,12 +75,11 @@
 fun init overloading thy =
   let
     val _ = if null overloading then error "At least one parameter must be given" else ();
-    fun declare ((_, ty), (v, _ )) = Variable.declare_term (Free (v, ty));
   in
     thy
     |> ProofContext.init
-    |> OverloadingData.put overloading
-    |> fold declare overloading
+    |> OverloadingData.put (map (fn (v, c_ty, checked) => (c_ty, (v, checked))) overloading)
+    |> fold (fn (v, (_, ty), _) => Variable.declare_term (Free (v, ty))) overloading
     |> Context.proof_map (
         Syntax.add_term_check 0 "overloading" term_check
         #> Syntax.add_term_uncheck 0 "overloading" term_uncheck)
@@ -101,8 +100,8 @@
     val thy = ProofContext.theory_of lthy;
     val overloading = get_overloading lthy;
     fun pr_operation ((c, ty), (v, _)) =
-      (Pretty.block o Pretty.breaks) [Pretty.str (Sign.extern_const thy c), Pretty.str "::",
-        Sign.pretty_typ thy ty, Pretty.str "as", Pretty.str v];
+      (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==",
+        Pretty.str (Sign.extern_const thy c), Pretty.str "::", Sign.pretty_typ thy ty];
   in
     (Pretty.block o Pretty.fbreaks)
       (Pretty.str "overloading" :: map pr_operation overloading)