1.1 --- a/src/HOL/Code_Numeral.thy	Sat Feb 18 10:35:45 2012 +0100
     1.2 +++ b/src/HOL/Code_Numeral.thy	Mon Feb 20 12:37:17 2012 +0100
     1.3 @@ -71,17 +71,17 @@
     1.4  
     1.5  end
     1.6  
     1.7 -definition [simp]:
     1.8 -  "Suc_code_numeral k = of_nat (Suc (nat_of k))"
     1.9 +definition Suc where [simp]:
    1.10 +  "Suc k = of_nat (Nat.Suc (nat_of k))"
    1.11  
    1.12 -rep_datatype "0 \<Colon> code_numeral" Suc_code_numeral
    1.13 +rep_datatype "0 \<Colon> code_numeral" Suc
    1.14  proof -
    1.15    fix P :: "code_numeral \<Rightarrow> bool"
    1.16    fix k :: code_numeral
    1.17    assume "P 0" then have init: "P (of_nat 0)" by simp
    1.18 -  assume "\<And>k. P k \<Longrightarrow> P (Suc_code_numeral k)"
    1.19 -    then have "\<And>n. P (of_nat n) \<Longrightarrow> P (Suc_code_numeral (of_nat n))" .
    1.20 -    then have step: "\<And>n. P (of_nat n) \<Longrightarrow> P (of_nat (Suc n))" by simp
    1.21 +  assume "\<And>k. P k \<Longrightarrow> P (Suc k)"
    1.22 +    then have "\<And>n. P (of_nat n) \<Longrightarrow> P (Suc (of_nat n))" .
    1.23 +    then have step: "\<And>n. P (of_nat n) \<Longrightarrow> P (of_nat (Nat.Suc n))" by simp
    1.24    from init step have "P (of_nat (nat_of k))"
    1.25      by (induct ("nat_of k")) simp_all
    1.26    then show "P k" by simp
    1.27 @@ -91,7 +91,7 @@
    1.28  declare code_numeral.induct [case_names nat, induct type: code_numeral]
    1.29  
    1.30  lemma code_numeral_decr [termination_simp]:
    1.31 -  "k \<noteq> of_nat 0 \<Longrightarrow> nat_of k - Suc 0 < nat_of k"
    1.32 +  "k \<noteq> of_nat 0 \<Longrightarrow> nat_of k - Nat.Suc 0 < nat_of k"
    1.33    by (cases k) simp
    1.34  
    1.35  lemma [simp, code]:
    1.36 @@ -99,7 +99,7 @@
    1.37  proof (rule ext)
    1.38    fix k
    1.39    have "code_numeral_size k = nat_size (nat_of k)"
    1.40 -    by (induct k rule: code_numeral.induct) (simp_all del: zero_code_numeral_def Suc_code_numeral_def, simp_all)
    1.41 +    by (induct k rule: code_numeral.induct) (simp_all del: zero_code_numeral_def Suc_def, simp_all)
    1.42    also have "nat_size (nat_of k) = nat_of k" by (induct ("nat_of k")) simp_all
    1.43    finally show "code_numeral_size k = nat_of k" .
    1.44  qed
    1.45 @@ -109,7 +109,7 @@
    1.46  proof (rule ext)
    1.47    fix k
    1.48    show "size k = nat_of k"
    1.49 -  by (induct k) (simp_all del: zero_code_numeral_def Suc_code_numeral_def, simp_all)
    1.50 +  by (induct k) (simp_all del: zero_code_numeral_def Suc_def, simp_all)
    1.51  qed
    1.52  
    1.53  lemmas [code del] = code_numeral.recs code_numeral.cases
    1.54 @@ -194,15 +194,15 @@
    1.55    "of_nat n + of_nat m = of_nat (n + m)"
    1.56    by simp
    1.57  
    1.58 -definition subtract_code_numeral :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
    1.59 -  [simp, code del]: "subtract_code_numeral = op -"
    1.60 +definition subtract :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
    1.61 +  [simp]: "subtract = minus"
    1.62  
    1.63 -lemma subtract_code_numeral_code [code nbe]:
    1.64 -  "subtract_code_numeral (of_nat n) (of_nat m) = of_nat (n - m)"
    1.65 +lemma subtract_code [code nbe]:
    1.66 +  "subtract (of_nat n) (of_nat m) = of_nat (n - m)"
    1.67    by simp
    1.68  
    1.69  lemma minus_code_numeral_code [code]:
    1.70 -  "n - m = subtract_code_numeral n m"
    1.71 +  "minus = subtract"
    1.72    by simp
    1.73  
    1.74  lemma times_code_numeral_code [code nbe]:
    1.75 @@ -222,7 +222,7 @@
    1.76    by simp
    1.77  
    1.78  lemma Suc_code_numeral_minus_one:
    1.79 -  "Suc_code_numeral n - 1 = n"
    1.80 +  "Suc n - 1 = n"
    1.81    by simp
    1.82  
    1.83  lemma of_nat_code [code]:
    1.84 @@ -242,27 +242,27 @@
    1.85    "nat_of_aux i n = nat_of i + n"
    1.86  
    1.87  lemma nat_of_aux_code [code]:
    1.88 -  "nat_of_aux i n = (if i = 0 then n else nat_of_aux (i - 1) (Suc n))"
    1.89 +  "nat_of_aux i n = (if i = 0 then n else nat_of_aux (i - 1) (Nat.Suc n))"
    1.90    by (auto simp add: nat_of_aux_def code_numeral_not_eq_zero)
    1.91  
    1.92  lemma nat_of_code [code]:
    1.93    "nat_of i = nat_of_aux i 0"
    1.94    by (simp add: nat_of_aux_def)
    1.95  
    1.96 -definition div_mod_code_numeral :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<times> code_numeral" where
    1.97 -  [code del]: "div_mod_code_numeral n m = (n div m, n mod m)"
    1.98 +definition div_mod :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<times> code_numeral" where
    1.99 +  [code del]: "div_mod n m = (n div m, n mod m)"
   1.100  
   1.101  lemma [code]:
   1.102 -  "div_mod_code_numeral n m = (if m = 0 then (0, n) else (n div m, n mod m))"
   1.103 -  unfolding div_mod_code_numeral_def by auto
   1.104 +  "div_mod n m = (if m = 0 then (0, n) else (n div m, n mod m))"
   1.105 +  unfolding div_mod_def by auto
   1.106  
   1.107  lemma [code]:
   1.108 -  "n div m = fst (div_mod_code_numeral n m)"
   1.109 -  unfolding div_mod_code_numeral_def by simp
   1.110 +  "n div m = fst (div_mod n m)"
   1.111 +  unfolding div_mod_def by simp
   1.112  
   1.113  lemma [code]:
   1.114 -  "n mod m = snd (div_mod_code_numeral n m)"
   1.115 -  unfolding div_mod_code_numeral_def by simp
   1.116 +  "n mod m = snd (div_mod n m)"
   1.117 +  unfolding div_mod_def by simp
   1.118  
   1.119  definition int_of :: "code_numeral \<Rightarrow> int" where
   1.120    "int_of = Nat.of_nat o nat_of"
   1.121 @@ -280,18 +280,20 @@
   1.122    then show ?thesis by (auto simp add: int_of_def mult_ac)
   1.123  qed
   1.124  
   1.125 -hide_const (open) of_nat nat_of int_of
   1.126  
   1.127 -subsubsection {* Lazy Evaluation of an indexed function *}
   1.128 +text {* Lazy Evaluation of an indexed function *}
   1.129  
   1.130 -function iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a Predicate.pred"
   1.131 +function iterate_upto :: "(code_numeral \<Rightarrow> 'a) \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<Rightarrow> 'a Predicate.pred"
   1.132  where
   1.133 -  "iterate_upto f n m = Predicate.Seq (%u. if n > m then Predicate.Empty else Predicate.Insert (f n) (iterate_upto f (n + 1) m))"
   1.134 +  "iterate_upto f n m =
   1.135 +    Predicate.Seq (%u. if n > m then Predicate.Empty
   1.136 +     else Predicate.Insert (f n) (iterate_upto f (n + 1) m))"
   1.137  by pat_completeness auto
   1.138  
   1.139  termination by (relation "measure (%(f, n, m). Code_Numeral.nat_of (m + 1 - n))") auto
   1.140  
   1.141 -hide_const (open) iterate_upto
   1.142 +hide_const (open) of_nat nat_of Suc  subtract int_of iterate_upto
   1.143 +
   1.144  
   1.145  subsection {* Code generator setup *}
   1.146  
   1.147 @@ -316,28 +318,28 @@
   1.148  code_reserved SML Int int
   1.149  code_reserved Eval Integer
   1.150  
   1.151 -code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   1.152 +code_const "plus \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   1.153    (SML "Int.+/ ((_),/ (_))")
   1.154    (OCaml "Big'_int.add'_big'_int")
   1.155    (Haskell infixl 6 "+")
   1.156    (Scala infixl 7 "+")
   1.157    (Eval infixl 8 "+")
   1.158  
   1.159 -code_const "subtract_code_numeral \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   1.160 +code_const "Code_Numeral.subtract \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   1.161    (SML "Int.max/ (_/ -/ _,/ 0 : int)")
   1.162    (OCaml "Big'_int.max'_big'_int/ (Big'_int.sub'_big'_int/ _/ _)/ Big'_int.zero'_big'_int")
   1.163    (Haskell "max/ (_/ -/ _)/ (0 :: Integer)")
   1.164    (Scala "!(_/ -/ _).max(0)")
   1.165    (Eval "Integer.max/ (_/ -/ _)/ 0")
   1.166  
   1.167 -code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   1.168 +code_const "times \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   1.169    (SML "Int.*/ ((_),/ (_))")
   1.170    (OCaml "Big'_int.mult'_big'_int")
   1.171    (Haskell infixl 7 "*")
   1.172    (Scala infixl 8 "*")
   1.173    (Eval infixl 8 "*")
   1.174  
   1.175 -code_const div_mod_code_numeral
   1.176 +code_const Code_Numeral.div_mod
   1.177    (SML "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (Int.div (n, m), Int.mod (n, m)))")
   1.178    (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)")
   1.179    (Haskell "divMod")
   1.180 @@ -351,18 +353,27 @@
   1.181    (Scala infixl 5 "==")
   1.182    (Eval "!((_ : int) = _)")
   1.183  
   1.184 -code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   1.185 +code_const "less_eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   1.186    (SML "Int.<=/ ((_),/ (_))")
   1.187    (OCaml "Big'_int.le'_big'_int")
   1.188    (Haskell infix 4 "<=")
   1.189    (Scala infixl 4 "<=")
   1.190    (Eval infixl 6 "<=")
   1.191  
   1.192 -code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   1.193 +code_const "less \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   1.194    (SML "Int.</ ((_),/ (_))")
   1.195    (OCaml "Big'_int.lt'_big'_int")
   1.196    (Haskell infix 4 "<")
   1.197    (Scala infixl 4 "<")
   1.198    (Eval infixl 6 "<")
   1.199  
   1.200 +code_modulename SML
   1.201 +  Code_Numeral Arith
   1.202 +
   1.203 +code_modulename OCaml
   1.204 +  Code_Numeral Arith
   1.205 +
   1.206 +code_modulename Haskell
   1.207 +  Code_Numeral Arith
   1.208 +
   1.209  end

     2.1 --- a/src/HOL/Library/Code_Natural.thy	Sat Feb 18 10:35:45 2012 +0100
     2.2 +++ b/src/HOL/Library/Code_Natural.thy	Mon Feb 20 12:37:17 2012 +0100
     2.3 @@ -3,7 +3,7 @@
     2.4  *)
     2.5  
     2.6  theory Code_Natural
     2.7 -imports Main
     2.8 +imports "../Main"
     2.9  begin
    2.10  
    2.11  section {* Alternative representation of @{typ code_numeral} for @{text Haskell} and @{text Scala} *}
    2.12 @@ -125,7 +125,7 @@
    2.13    (Haskell infixl 7 "*")
    2.14    (Scala infixl 8 "*")
    2.15  
    2.16 -code_const div_mod_code_numeral
    2.17 +code_const Code_Numeral.div_mod
    2.18    (Haskell "divMod")
    2.19    (Scala infixl 8 "/%")
    2.20  

     3.1 --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Sat Feb 18 10:35:45 2012 +0100
     3.2 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Mon Feb 20 12:37:17 2012 +0100
     3.3 @@ -153,7 +153,7 @@
     3.4  
     3.5  lemma "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))"
     3.6  nitpick [expect = none]
     3.7 -by (rule Suc_def)
     3.8 +by (rule Nat.Suc_def)
     3.9  
    3.10  lemma "Suc n = Abs_Nat (Suc_Rep (Suc_Rep (Rep_Nat n)))"
    3.11  nitpick [expect = genuine]

     4.1 --- a/src/HOL/Quickcheck.thy	Sat Feb 18 10:35:45 2012 +0100
     4.2 +++ b/src/HOL/Quickcheck.thy	Mon Feb 20 12:37:17 2012 +0100
     4.3 @@ -139,7 +139,7 @@
     4.4  primrec random_aux_set
     4.5  where
     4.6    "random_aux_set 0 j = collapse (Random.select_weight [(1, Pair valterm_emptyset)])"
     4.7 -| "random_aux_set (Suc_code_numeral i) j = collapse (Random.select_weight [(1, Pair valterm_emptyset), (Suc_code_numeral i, random j \<circ>\<rightarrow> (%x. random_aux_set i j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])"
     4.8 +| "random_aux_set (Code_Numeral.Suc i) j = collapse (Random.select_weight [(1, Pair valterm_emptyset), (Code_Numeral.Suc i, random j \<circ>\<rightarrow> (%x. random_aux_set i j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])"
     4.9  
    4.10  lemma [code]:
    4.11    "random_aux_set i j = collapse (Random.select_weight [(1, Pair valterm_emptyset), (i, random j \<circ>\<rightarrow> (%x. random_aux_set (i - 1) j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])"
    4.12 @@ -149,7 +149,7 @@
    4.13    show ?case by (subst select_weight_drop_zero[symmetric])
    4.14      (simp add: filter.simps random_aux_set.simps[simplified])
    4.15  next
    4.16 -  case (Suc_code_numeral i)
    4.17 +  case (Suc i)
    4.18    show ?case by (simp only: random_aux_set.simps(2)[of "i"] Suc_code_numeral_minus_one)
    4.19  qed
    4.20  
    4.21 @@ -164,7 +164,7 @@
    4.22  lemma random_aux_rec:
    4.23    fixes random_aux :: "code_numeral \<Rightarrow> 'a"
    4.24    assumes "random_aux 0 = rhs 0"
    4.25 -    and "\<And>k. random_aux (Suc_code_numeral k) = rhs (Suc_code_numeral k)"
    4.26 +    and "\<And>k. random_aux (Code_Numeral.Suc k) = rhs (Code_Numeral.Suc k)"
    4.27    shows "random_aux k = rhs k"
    4.28    using assms by (rule code_numeral.induct)
    4.29  

     5.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Sat Feb 18 10:35:45 2012 +0100
     5.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Feb 20 12:37:17 2012 +0100
     5.3 @@ -100,7 +100,7 @@
     5.4      fun subst_v t' = map_aterms (fn t as Free (w, _) => if v = w then t' else t | t => t);
     5.5      val t_rhs = lambda t_k proto_t_rhs;
     5.6      val eqs0 = [subst_v @{term "0::code_numeral"} eq,
     5.7 -      subst_v (@{term "Suc_code_numeral"} $ t_k) eq];
     5.8 +      subst_v (@{const Code_Numeral.Suc} $ t_k) eq];
     5.9      val eqs1 = map (Pattern.rewrite_term thy rew_ts []) eqs0;
    5.10      val ((_, (_, eqs2)), lthy') = Primrec.add_primrec_simple
    5.11        [((Binding.conceal (Binding.name random_aux), T), NoSyn)] eqs1 lthy;