qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
authorhaftmann
Tue Jun 08 16:37:19 2010 +0200 (2010-06-08)
changeset 373873581483cca6c
parent 37385 f076ca61dc00
child 37388 793618618f78
qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
NEWS
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Import/HOL/num.imp
src/HOL/Import/HOL/pair.imp
src/HOL/Import/HOLLight/hollight.imp
src/HOL/Nat.thy
src/HOL/Product_Type.thy
src/HOL/Set.thy
src/HOL/Tools/Function/measure_functions.ML
src/HOL/Tools/Function/sum_tree.ML
src/HOL/Tools/Function/termination.ML
src/HOL/Tools/hologic.ML
     1.1 --- a/NEWS	Tue Jun 08 07:45:39 2010 +0200
     1.2 +++ b/NEWS	Tue Jun 08 16:37:19 2010 +0200
     1.3 @@ -4,6 +4,21 @@
     1.4  New in this Isabelle version
     1.5  ----------------------------
     1.6  
     1.7 +*** HOL ***
     1.8 +
     1.9 +* Some previously unqualified names have been qualified:
    1.10 +
    1.11 +  types
    1.12 +    nat ~> Nat.nat
    1.13 +    + ~> Sum_Type.+
    1.14 +
    1.15 +  constants
    1.16 +    Ball ~> Set.Ball
    1.17 +    Bex ~> Set.Bex
    1.18 +    Suc ~> Nat.Suc
    1.19 +    curry ~> Product_Type.curry
    1.20 +
    1.21 +INCOMPATIBILITY.
    1.22  
    1.23  
    1.24  New in Isabelle2009-2 (June 2010)
     2.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Jun 08 07:45:39 2010 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Jun 08 16:37:19 2010 +0200
     2.3 @@ -2964,7 +2964,7 @@
     2.4  fun rz rT = Const(@{const_name Groups.zero},rT);
     2.5  
     2.6  fun dest_nat t = case t of
     2.7 -  Const ("Suc",_)$t' => 1 + dest_nat t'
     2.8 +  Const (@{const_name Suc}, _) $ t' => 1 + dest_nat t'
     2.9  | _ => (snd o HOLogic.dest_number) t;
    2.10  
    2.11  fun num_of_term m t = 
     3.1 --- a/src/HOL/Import/HOL/num.imp	Tue Jun 08 07:45:39 2010 +0200
     3.2 +++ b/src/HOL/Import/HOL/num.imp	Tue Jun 08 16:37:19 2010 +0200
     3.3 @@ -3,10 +3,10 @@
     3.4  import_segment "hol4"
     3.5  
     3.6  type_maps
     3.7 -  "num" > "nat"
     3.8 +  "num" > "Nat.nat"
     3.9  
    3.10  const_maps
    3.11 -  "SUC" > "Suc"
    3.12 +  "SUC" > "Nat.Suc"
    3.13    "0" > "0" :: "nat"
    3.14  
    3.15  thm_maps
     4.1 --- a/src/HOL/Import/HOL/pair.imp	Tue Jun 08 07:45:39 2010 +0200
     4.2 +++ b/src/HOL/Import/HOL/pair.imp	Tue Jun 08 16:37:19 2010 +0200
     4.3 @@ -16,7 +16,7 @@
     4.4    "RPROD" > "HOL4Base.pair.RPROD"
     4.5    "LEX" > "HOL4Base.pair.LEX"
     4.6    "FST" > "fst"
     4.7 -  "CURRY" > "curry"
     4.8 +  "CURRY" > "Product_Type.curry"
     4.9    "," > "Pair"
    4.10    "##" > "prod_fun"
    4.11  
     5.1 --- a/src/HOL/Import/HOLLight/hollight.imp	Tue Jun 08 07:45:39 2010 +0200
     5.2 +++ b/src/HOL/Import/HOLLight/hollight.imp	Tue Jun 08 16:37:19 2010 +0200
     5.3 @@ -8,7 +8,7 @@
     5.4    "real" > "HOLLight.hollight.real"
     5.5    "prod" > "*"
     5.6    "option" > "HOLLight.hollight.option"
     5.7 -  "num" > "nat"
     5.8 +  "num" > "Nat.nat"
     5.9    "nadd" > "HOLLight.hollight.nadd"
    5.10    "list" > "HOLLight.hollight.list"
    5.11    "int" > "HOLLight.hollight.int"
    5.12 @@ -128,7 +128,7 @@
    5.13    "TL" > "HOLLight.hollight.TL"
    5.14    "T" > "True"
    5.15    "SURJ" > "HOLLight.hollight.SURJ"
    5.16 -  "SUC" > "Suc"
    5.17 +  "SUC" > "Nat.Suc"
    5.18    "SUBSET" > "HOLLight.hollight.SUBSET"
    5.19    "SOME" > "HOLLight.hollight.SOME"
    5.20    "SND" > "snd"
     6.1 --- a/src/HOL/Nat.thy	Tue Jun 08 07:45:39 2010 +0200
     6.2 +++ b/src/HOL/Nat.thy	Tue Jun 08 16:37:19 2010 +0200
     6.3 @@ -39,16 +39,11 @@
     6.4      Zero_RepI: "Nat Zero_Rep"
     6.5    | Suc_RepI: "Nat i \<Longrightarrow> Nat (Suc_Rep i)"
     6.6  
     6.7 -global
     6.8 -
     6.9 -typedef (open Nat)
    6.10 -  nat = Nat
    6.11 +typedef (open Nat) nat = Nat
    6.12    by (rule exI, unfold mem_def, rule Nat.Zero_RepI)
    6.13  
    6.14  definition Suc :: "nat => nat" where
    6.15 -  Suc_def: "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))"
    6.16 -
    6.17 -local
    6.18 +  "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))"
    6.19  
    6.20  instantiation nat :: zero
    6.21  begin
    6.22 @@ -1457,8 +1452,7 @@
    6.23  end
    6.24  
    6.25  lemma mono_iff_le_Suc: "mono f = (\<forall>n. f n \<le> f (Suc n))"
    6.26 -unfolding mono_def
    6.27 -by (auto intro:lift_Suc_mono_le[of f])
    6.28 +  unfolding mono_def by (auto intro: lift_Suc_mono_le [of f])
    6.29  
    6.30  lemma mono_nat_linear_lb:
    6.31    "(!!m n::nat. m<n \<Longrightarrow> f m < f n) \<Longrightarrow> f(m)+k \<le> f(m+k)"
     7.1 --- a/src/HOL/Product_Type.thy	Tue Jun 08 07:45:39 2010 +0200
     7.2 +++ b/src/HOL/Product_Type.thy	Tue Jun 08 16:37:19 2010 +0200
     7.3 @@ -788,11 +788,8 @@
     7.4  
     7.5  subsubsection {* Derived operations *}
     7.6  
     7.7 -global consts
     7.8 -  curry    :: "('a \<times> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c"
     7.9 -
    7.10 -local defs
    7.11 -  curry_def:    "curry == (%c x y. c (Pair x y))"
    7.12 +definition curry    :: "('a \<times> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c" where
    7.13 +  "curry = (\<lambda>c x y. c (x, y))"
    7.14  
    7.15  lemma curry_conv [simp, code]: "curry f a b = f (a, b)"
    7.16    by (simp add: curry_def)
     8.1 --- a/src/HOL/Set.thy	Tue Jun 08 07:45:39 2010 +0200
     8.2 +++ b/src/HOL/Set.thy	Tue Jun 08 16:37:19 2010 +0200
     8.3 @@ -151,17 +151,11 @@
     8.4    supset_eq  ("op \<supseteq>") and
     8.5    supset_eq  ("(_/ \<supseteq> _)" [50, 51] 50)
     8.6  
     8.7 -global
     8.8 -
     8.9 -consts
    8.10 -  Ball          :: "'a set => ('a => bool) => bool"      -- "bounded universal quantifiers"
    8.11 -  Bex           :: "'a set => ('a => bool) => bool"      -- "bounded existential quantifiers"
    8.12 +definition Ball :: "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
    8.13 +  "Ball A P \<longleftrightarrow> (\<forall>x. x \<in> A \<longrightarrow> P x)"   -- "bounded universal quantifiers"
    8.14  
    8.15 -local
    8.16 -
    8.17 -defs
    8.18 -  Ball_def:     "Ball A P       == ALL x. x:A --> P(x)"
    8.19 -  Bex_def:      "Bex A P        == EX x. x:A & P(x)"
    8.20 +definition Bex :: "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
    8.21 +  "Bex A P \<longleftrightarrow> (\<exists>x. x \<in> A \<and> P x)"   -- "bounded existential quantifiers"
    8.22  
    8.23  syntax
    8.24    "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3ALL _:_./ _)" [0, 0, 10] 10)
     9.1 --- a/src/HOL/Tools/Function/measure_functions.ML	Tue Jun 08 07:45:39 2010 +0200
     9.2 +++ b/src/HOL/Tools/Function/measure_functions.ML	Tue Jun 08 16:37:19 2010 +0200
     9.3 @@ -39,17 +39,17 @@
     9.4  fun constant_0 T = Abs ("x", T, HOLogic.zero)
     9.5  fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero)
     9.6  
     9.7 -fun mk_funorder_funs (Type ("+", [fT, sT])) =
     9.8 +fun mk_funorder_funs (Type (@{type_name "+"}, [fT, sT])) =
     9.9    map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT)
    9.10    @ map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT)
    9.11    | mk_funorder_funs T = [ constant_1 T ]
    9.12  
    9.13 -fun mk_ext_base_funs ctxt (Type ("+", [fT, sT])) =
    9.14 +fun mk_ext_base_funs ctxt (Type (@{type_name "+"}, [fT, sT])) =
    9.15      map_product (SumTree.mk_sumcase fT sT HOLogic.natT)
    9.16        (mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT)
    9.17    | mk_ext_base_funs ctxt T = find_measures ctxt T
    9.18  
    9.19 -fun mk_all_measure_funs ctxt (T as Type ("+", _)) =
    9.20 +fun mk_all_measure_funs ctxt (T as Type (@{type_name "+"}, _)) =
    9.21      mk_ext_base_funs ctxt T @ mk_funorder_funs T
    9.22    | mk_all_measure_funs ctxt T = find_measures ctxt T
    9.23  
    10.1 --- a/src/HOL/Tools/Function/sum_tree.ML	Tue Jun 08 07:45:39 2010 +0200
    10.2 +++ b/src/HOL/Tools/Function/sum_tree.ML	Tue Jun 08 16:37:19 2010 +0200
    10.3 @@ -17,7 +17,7 @@
    10.4      {left = (fn f => f o left), right = (fn f => f o right), init = I} len i init
    10.5  
    10.6  (* Sum types *)
    10.7 -fun mk_sumT LT RT = Type ("+", [LT, RT])
    10.8 +fun mk_sumT LT RT = Type (@{type_name "+"}, [LT, RT])
    10.9  fun mk_sumcase TL TR T l r =
   10.10    Const (@{const_name sum.sum_case},
   10.11      (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r
   10.12 @@ -27,18 +27,18 @@
   10.13  fun mk_inj ST n i =
   10.14    access_top_down
   10.15    { init = (ST, I : term -> term),
   10.16 -    left = (fn (T as Type ("+", [LT, RT]), inj) =>
   10.17 +    left = (fn (T as Type (@{type_name "+"}, [LT, RT]), inj) =>
   10.18        (LT, inj o App (Const (@{const_name Inl}, LT --> T)))),
   10.19 -    right =(fn (T as Type ("+", [LT, RT]), inj) =>
   10.20 +    right =(fn (T as Type (@{type_name "+"}, [LT, RT]), inj) =>
   10.21        (RT, inj o App (Const (@{const_name Inr}, RT --> T))))} n i
   10.22    |> snd
   10.23  
   10.24  fun mk_proj ST n i =
   10.25    access_top_down
   10.26    { init = (ST, I : term -> term),
   10.27 -    left = (fn (T as Type ("+", [LT, RT]), proj) =>
   10.28 +    left = (fn (T as Type (@{type_name "+"}, [LT, RT]), proj) =>
   10.29        (LT, App (Const (@{const_name Sum_Type.Projl}, T --> LT)) o proj)),
   10.30 -    right =(fn (T as Type ("+", [LT, RT]), proj) =>
   10.31 +    right =(fn (T as Type (@{type_name "+"}, [LT, RT]), proj) =>
   10.32        (RT, App (Const (@{const_name Sum_Type.Projr}, T --> RT)) o proj))} n i
   10.33    |> snd
   10.34  
    11.1 --- a/src/HOL/Tools/Function/termination.ML	Tue Jun 08 07:45:39 2010 +0200
    11.2 +++ b/src/HOL/Tools/Function/termination.ML	Tue Jun 08 16:37:19 2010 +0200
    11.3 @@ -106,7 +106,7 @@
    11.4    end
    11.5  
    11.6  (* compute list of types for nodes *)
    11.7 -fun node_types sk T = dest_tree (fn Type ("+", [LT, RT]) => (LT, RT)) sk T |> map snd
    11.8 +fun node_types sk T = dest_tree (fn Type (@{type_name "+"}, [LT, RT]) => (LT, RT)) sk T |> map snd
    11.9  
   11.10  (* find index and raw term *)
   11.11  fun dest_inj (SLeaf i) trm = (i, trm)
    12.1 --- a/src/HOL/Tools/hologic.ML	Tue Jun 08 07:45:39 2010 +0200
    12.2 +++ b/src/HOL/Tools/hologic.ML	Tue Jun 08 16:37:19 2010 +0200
    12.3 @@ -438,16 +438,16 @@
    12.4  
    12.5  (* nat *)
    12.6  
    12.7 -val natT = Type ("nat", []);
    12.8 +val natT = Type ("Nat.nat", []);
    12.9  
   12.10  val zero = Const ("Groups.zero_class.zero", natT);
   12.11  
   12.12  fun is_zero (Const ("Groups.zero_class.zero", _)) = true
   12.13    | is_zero _ = false;
   12.14  
   12.15 -fun mk_Suc t = Const ("Suc", natT --> natT) $ t;
   12.16 +fun mk_Suc t = Const ("Nat.Suc", natT --> natT) $ t;
   12.17  
   12.18 -fun dest_Suc (Const ("Suc", _) $ t) = t
   12.19 +fun dest_Suc (Const ("Nat.Suc", _) $ t) = t
   12.20    | dest_Suc t = raise TERM ("dest_Suc", [t]);
   12.21  
   12.22  val Suc_zero = mk_Suc zero;
   12.23 @@ -459,7 +459,7 @@
   12.24    in if n < 0 then raise TERM ("mk_nat: negative number", []) else mk n end;
   12.25  
   12.26  fun dest_nat (Const ("Groups.zero_class.zero", _)) = 0
   12.27 -  | dest_nat (Const ("Suc", _) $ t) = dest_nat t + 1
   12.28 +  | dest_nat (Const ("Nat.Suc", _) $ t) = dest_nat t + 1
   12.29    | dest_nat t = raise TERM ("dest_nat", [t]);
   12.30  
   12.31  val class_size = "Nat.size";