qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications

--- a/NEWS	Tue Jun 08 07:45:39 2010 +0200
+++ b/NEWS	Tue Jun 08 16:37:19 2010 +0200
@@ -4,6 +4,21 @@
 New in this Isabelle version
 ----------------------------
 
+*** HOL ***
+
+* Some previously unqualified names have been qualified:
+
+  types
+    nat ~> Nat.nat
+    + ~> Sum_Type.+
+
+  constants
+    Ball ~> Set.Ball
+    Bex ~> Set.Bex
+    Suc ~> Nat.Suc
+    curry ~> Product_Type.curry
+
+INCOMPATIBILITY.
 
 
 New in Isabelle2009-2 (June 2010)

--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Jun 08 07:45:39 2010 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Jun 08 16:37:19 2010 +0200
@@ -2964,7 +2964,7 @@
 fun rz rT = Const(@{const_name Groups.zero},rT);
 
 fun dest_nat t = case t of
-  Const ("Suc",_)$t' => 1 + dest_nat t'
+  Const (@{const_name Suc}, _) $ t' => 1 + dest_nat t'
 | _ => (snd o HOLogic.dest_number) t;
 
 fun num_of_term m t = 

--- a/src/HOL/Import/HOL/num.imp	Tue Jun 08 07:45:39 2010 +0200
+++ b/src/HOL/Import/HOL/num.imp	Tue Jun 08 16:37:19 2010 +0200
@@ -3,10 +3,10 @@
 import_segment "hol4"
 
 type_maps
-  "num" > "nat"
+  "num" > "Nat.nat"
 
 const_maps
-  "SUC" > "Suc"
+  "SUC" > "Nat.Suc"
   "0" > "0" :: "nat"
 
 thm_maps

--- a/src/HOL/Import/HOL/pair.imp	Tue Jun 08 07:45:39 2010 +0200
+++ b/src/HOL/Import/HOL/pair.imp	Tue Jun 08 16:37:19 2010 +0200
@@ -16,7 +16,7 @@
   "RPROD" > "HOL4Base.pair.RPROD"
   "LEX" > "HOL4Base.pair.LEX"
   "FST" > "fst"
-  "CURRY" > "curry"
+  "CURRY" > "Product_Type.curry"
   "," > "Pair"
   "##" > "prod_fun"
 

--- a/src/HOL/Import/HOLLight/hollight.imp	Tue Jun 08 07:45:39 2010 +0200
+++ b/src/HOL/Import/HOLLight/hollight.imp	Tue Jun 08 16:37:19 2010 +0200
@@ -8,7 +8,7 @@
   "real" > "HOLLight.hollight.real"
   "prod" > "*"
   "option" > "HOLLight.hollight.option"
-  "num" > "nat"
+  "num" > "Nat.nat"
   "nadd" > "HOLLight.hollight.nadd"
   "list" > "HOLLight.hollight.list"
   "int" > "HOLLight.hollight.int"
@@ -128,7 +128,7 @@
   "TL" > "HOLLight.hollight.TL"
   "T" > "True"
   "SURJ" > "HOLLight.hollight.SURJ"
-  "SUC" > "Suc"
+  "SUC" > "Nat.Suc"
   "SUBSET" > "HOLLight.hollight.SUBSET"
   "SOME" > "HOLLight.hollight.SOME"
   "SND" > "snd"

--- a/src/HOL/Nat.thy	Tue Jun 08 07:45:39 2010 +0200
+++ b/src/HOL/Nat.thy	Tue Jun 08 16:37:19 2010 +0200
@@ -39,16 +39,11 @@
     Zero_RepI: "Nat Zero_Rep"
   | Suc_RepI: "Nat i \<Longrightarrow> Nat (Suc_Rep i)"
 
-global
-
-typedef (open Nat)
-  nat = Nat
+typedef (open Nat) nat = Nat
   by (rule exI, unfold mem_def, rule Nat.Zero_RepI)
 
 definition Suc :: "nat => nat" where
-  Suc_def: "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))"
-
-local
+  "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))"
 
 instantiation nat :: zero
 begin
@@ -1457,8 +1452,7 @@
 end
 
 lemma mono_iff_le_Suc: "mono f = (\<forall>n. f n \<le> f (Suc n))"
-unfolding mono_def
-by (auto intro:lift_Suc_mono_le[of f])
+  unfolding mono_def by (auto intro: lift_Suc_mono_le [of f])
 
 lemma mono_nat_linear_lb:
   "(!!m n::nat. m<n \<Longrightarrow> f m < f n) \<Longrightarrow> f(m)+k \<le> f(m+k)"

--- a/src/HOL/Product_Type.thy	Tue Jun 08 07:45:39 2010 +0200
+++ b/src/HOL/Product_Type.thy	Tue Jun 08 16:37:19 2010 +0200
@@ -788,11 +788,8 @@
 
 subsubsection {* Derived operations *}
 
-global consts
-  curry    :: "('a \<times> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c"
-
-local defs
-  curry_def:    "curry == (%c x y. c (Pair x y))"
+definition curry    :: "('a \<times> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c" where
+  "curry = (\<lambda>c x y. c (x, y))"
 
 lemma curry_conv [simp, code]: "curry f a b = f (a, b)"
   by (simp add: curry_def)

--- a/src/HOL/Set.thy	Tue Jun 08 07:45:39 2010 +0200
+++ b/src/HOL/Set.thy	Tue Jun 08 16:37:19 2010 +0200
@@ -151,17 +151,11 @@
   supset_eq  ("op \<supseteq>") and
   supset_eq  ("(_/ \<supseteq> _)" [50, 51] 50)
 
-global
-
-consts
-  Ball          :: "'a set => ('a => bool) => bool"      -- "bounded universal quantifiers"
-  Bex           :: "'a set => ('a => bool) => bool"      -- "bounded existential quantifiers"
+definition Ball :: "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "Ball A P \<longleftrightarrow> (\<forall>x. x \<in> A \<longrightarrow> P x)"   -- "bounded universal quantifiers"
 
-local
-
-defs
-  Ball_def:     "Ball A P       == ALL x. x:A --> P(x)"
-  Bex_def:      "Bex A P        == EX x. x:A & P(x)"
+definition Bex :: "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "Bex A P \<longleftrightarrow> (\<exists>x. x \<in> A \<and> P x)"   -- "bounded existential quantifiers"
 
 syntax
   "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3ALL _:_./ _)" [0, 0, 10] 10)

--- a/src/HOL/Tools/Function/measure_functions.ML	Tue Jun 08 07:45:39 2010 +0200
+++ b/src/HOL/Tools/Function/measure_functions.ML	Tue Jun 08 16:37:19 2010 +0200
@@ -39,17 +39,17 @@
 fun constant_0 T = Abs ("x", T, HOLogic.zero)
 fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero)
 
-fun mk_funorder_funs (Type ("+", [fT, sT])) =
+fun mk_funorder_funs (Type (@{type_name "+"}, [fT, sT])) =
   map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT)
   @ map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT)
   | mk_funorder_funs T = [ constant_1 T ]
 
-fun mk_ext_base_funs ctxt (Type ("+", [fT, sT])) =
+fun mk_ext_base_funs ctxt (Type (@{type_name "+"}, [fT, sT])) =
     map_product (SumTree.mk_sumcase fT sT HOLogic.natT)
       (mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT)
   | mk_ext_base_funs ctxt T = find_measures ctxt T
 
-fun mk_all_measure_funs ctxt (T as Type ("+", _)) =
+fun mk_all_measure_funs ctxt (T as Type (@{type_name "+"}, _)) =
     mk_ext_base_funs ctxt T @ mk_funorder_funs T
   | mk_all_measure_funs ctxt T = find_measures ctxt T
 

--- a/src/HOL/Tools/Function/sum_tree.ML	Tue Jun 08 07:45:39 2010 +0200
+++ b/src/HOL/Tools/Function/sum_tree.ML	Tue Jun 08 16:37:19 2010 +0200
@@ -17,7 +17,7 @@
     {left = (fn f => f o left), right = (fn f => f o right), init = I} len i init
 
 (* Sum types *)
-fun mk_sumT LT RT = Type ("+", [LT, RT])
+fun mk_sumT LT RT = Type (@{type_name "+"}, [LT, RT])
 fun mk_sumcase TL TR T l r =
   Const (@{const_name sum.sum_case},
     (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r
@@ -27,18 +27,18 @@
 fun mk_inj ST n i =
   access_top_down
   { init = (ST, I : term -> term),
-    left = (fn (T as Type ("+", [LT, RT]), inj) =>
+    left = (fn (T as Type (@{type_name "+"}, [LT, RT]), inj) =>
       (LT, inj o App (Const (@{const_name Inl}, LT --> T)))),
-    right =(fn (T as Type ("+", [LT, RT]), inj) =>
+    right =(fn (T as Type (@{type_name "+"}, [LT, RT]), inj) =>
       (RT, inj o App (Const (@{const_name Inr}, RT --> T))))} n i
   |> snd
 
 fun mk_proj ST n i =
   access_top_down
   { init = (ST, I : term -> term),
-    left = (fn (T as Type ("+", [LT, RT]), proj) =>
+    left = (fn (T as Type (@{type_name "+"}, [LT, RT]), proj) =>
       (LT, App (Const (@{const_name Sum_Type.Projl}, T --> LT)) o proj)),
-    right =(fn (T as Type ("+", [LT, RT]), proj) =>
+    right =(fn (T as Type (@{type_name "+"}, [LT, RT]), proj) =>
       (RT, App (Const (@{const_name Sum_Type.Projr}, T --> RT)) o proj))} n i
   |> snd
 

--- a/src/HOL/Tools/Function/termination.ML	Tue Jun 08 07:45:39 2010 +0200
+++ b/src/HOL/Tools/Function/termination.ML	Tue Jun 08 16:37:19 2010 +0200
@@ -106,7 +106,7 @@
   end
 
 (* compute list of types for nodes *)
-fun node_types sk T = dest_tree (fn Type ("+", [LT, RT]) => (LT, RT)) sk T |> map snd
+fun node_types sk T = dest_tree (fn Type (@{type_name "+"}, [LT, RT]) => (LT, RT)) sk T |> map snd
 
 (* find index and raw term *)
 fun dest_inj (SLeaf i) trm = (i, trm)

--- a/src/HOL/Tools/hologic.ML	Tue Jun 08 07:45:39 2010 +0200
+++ b/src/HOL/Tools/hologic.ML	Tue Jun 08 16:37:19 2010 +0200
@@ -438,16 +438,16 @@
 
 (* nat *)
 
-val natT = Type ("nat", []);
+val natT = Type ("Nat.nat", []);
 
 val zero = Const ("Groups.zero_class.zero", natT);
 
 fun is_zero (Const ("Groups.zero_class.zero", _)) = true
   | is_zero _ = false;
 
-fun mk_Suc t = Const ("Suc", natT --> natT) $ t;
+fun mk_Suc t = Const ("Nat.Suc", natT --> natT) $ t;
 
-fun dest_Suc (Const ("Suc", _) $ t) = t
+fun dest_Suc (Const ("Nat.Suc", _) $ t) = t
   | dest_Suc t = raise TERM ("dest_Suc", [t]);
 
 val Suc_zero = mk_Suc zero;
@@ -459,7 +459,7 @@
   in if n < 0 then raise TERM ("mk_nat: negative number", []) else mk n end;
 
 fun dest_nat (Const ("Groups.zero_class.zero", _)) = 0
-  | dest_nat (Const ("Suc", _) $ t) = dest_nat t + 1
+  | dest_nat (Const ("Nat.Suc", _) $ t) = dest_nat t + 1
   | dest_nat t = raise TERM ("dest_nat", [t]);
 
 val class_size = "Nat.size";