# HG changeset patch # User haftmann # Date 1276007839 -7200 # Node ID 3581483cca6c96fcc7b343d1800bda2f5f203879 # Parent f076ca61dc0067ad2bec16b9d59f525f13a66eef qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications diff -r f076ca61dc00 -r 3581483cca6c NEWS --- 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) diff -r f076ca61dc00 -r 3581483cca6c src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- 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 = diff -r f076ca61dc00 -r 3581483cca6c src/HOL/Import/HOL/num.imp --- 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 diff -r f076ca61dc00 -r 3581483cca6c src/HOL/Import/HOL/pair.imp --- 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" diff -r f076ca61dc00 -r 3581483cca6c src/HOL/Import/HOLLight/hollight.imp --- 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" diff -r f076ca61dc00 -r 3581483cca6c src/HOL/Nat.thy --- 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 \ 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 = (\n. f n \ 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 f m < f n) \ f(m)+k \ f(m+k)" diff -r f076ca61dc00 -r 3581483cca6c src/HOL/Product_Type.thy --- 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 \ 'b \ 'c) \ 'a \ 'b \ 'c" - -local defs - curry_def: "curry == (%c x y. c (Pair x y))" +definition curry :: "('a \ 'b \ 'c) \ 'a \ 'b \ 'c" where + "curry = (\c x y. c (x, y))" lemma curry_conv [simp, code]: "curry f a b = f (a, b)" by (simp add: curry_def) diff -r f076ca61dc00 -r 3581483cca6c src/HOL/Set.thy --- 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 \") and supset_eq ("(_/ \ _)" [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 \ ('a \ bool) \ bool" where + "Ball A P \ (\x. x \ A \ 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 \ ('a \ bool) \ bool" where + "Bex A P \ (\x. x \ A \ P x)" -- "bounded existential quantifiers" syntax "_Ball" :: "pttrn => 'a set => bool => bool" ("(3ALL _:_./ _)" [0, 0, 10] 10) diff -r f076ca61dc00 -r 3581483cca6c src/HOL/Tools/Function/measure_functions.ML --- 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 diff -r f076ca61dc00 -r 3581483cca6c src/HOL/Tools/Function/sum_tree.ML --- 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 diff -r f076ca61dc00 -r 3581483cca6c src/HOL/Tools/Function/termination.ML --- 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) diff -r f076ca61dc00 -r 3581483cca6c src/HOL/Tools/hologic.ML --- 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";