# HG changeset patch
# User huffman
# Date 1329737837 -3600
# Node ID d1dcb91a512e08d8da33cd1fac778bd28c7644c9
# Parent  42298c5d33b10f6041b0051cae347596c324af37
use qualified constant names instead of suffixes (from Florian Haftmann)

diff -r 42298c5d33b1 -r d1dcb91a512e src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Sat Feb 18 10:35:45 2012 +0100
+++ b/src/HOL/Code_Numeral.thy	Mon Feb 20 12:37:17 2012 +0100
@@ -71,17 +71,17 @@
 
 end
 
-definition [simp]:
-  "Suc_code_numeral k = of_nat (Suc (nat_of k))"
+definition Suc where [simp]:
+  "Suc k = of_nat (Nat.Suc (nat_of k))"
 
-rep_datatype "0 \<Colon> code_numeral" Suc_code_numeral
+rep_datatype "0 \<Colon> code_numeral" Suc
 proof -
   fix P :: "code_numeral \<Rightarrow> bool"
   fix k :: code_numeral
   assume "P 0" then have init: "P (of_nat 0)" by simp
-  assume "\<And>k. P k \<Longrightarrow> P (Suc_code_numeral k)"
-    then have "\<And>n. P (of_nat n) \<Longrightarrow> P (Suc_code_numeral (of_nat n))" .
-    then have step: "\<And>n. P (of_nat n) \<Longrightarrow> P (of_nat (Suc n))" by simp
+  assume "\<And>k. P k \<Longrightarrow> P (Suc k)"
+    then have "\<And>n. P (of_nat n) \<Longrightarrow> P (Suc (of_nat n))" .
+    then have step: "\<And>n. P (of_nat n) \<Longrightarrow> P (of_nat (Nat.Suc n))" by simp
   from init step have "P (of_nat (nat_of k))"
     by (induct ("nat_of k")) simp_all
   then show "P k" by simp
@@ -91,7 +91,7 @@
 declare code_numeral.induct [case_names nat, induct type: code_numeral]
 
 lemma code_numeral_decr [termination_simp]:
-  "k \<noteq> of_nat 0 \<Longrightarrow> nat_of k - Suc 0 < nat_of k"
+  "k \<noteq> of_nat 0 \<Longrightarrow> nat_of k - Nat.Suc 0 < nat_of k"
   by (cases k) simp
 
 lemma [simp, code]:
@@ -99,7 +99,7 @@
 proof (rule ext)
   fix k
   have "code_numeral_size k = nat_size (nat_of k)"
-    by (induct k rule: code_numeral.induct) (simp_all del: zero_code_numeral_def Suc_code_numeral_def, simp_all)
+    by (induct k rule: code_numeral.induct) (simp_all del: zero_code_numeral_def Suc_def, simp_all)
   also have "nat_size (nat_of k) = nat_of k" by (induct ("nat_of k")) simp_all
   finally show "code_numeral_size k = nat_of k" .
 qed
@@ -109,7 +109,7 @@
 proof (rule ext)
   fix k
   show "size k = nat_of k"
-  by (induct k) (simp_all del: zero_code_numeral_def Suc_code_numeral_def, simp_all)
+  by (induct k) (simp_all del: zero_code_numeral_def Suc_def, simp_all)
 qed
 
 lemmas [code del] = code_numeral.recs code_numeral.cases
@@ -194,15 +194,15 @@
   "of_nat n + of_nat m = of_nat (n + m)"
   by simp
 
-definition subtract_code_numeral :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
-  [simp, code del]: "subtract_code_numeral = op -"
+definition subtract :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
+  [simp]: "subtract = minus"
 
-lemma subtract_code_numeral_code [code nbe]:
-  "subtract_code_numeral (of_nat n) (of_nat m) = of_nat (n - m)"
+lemma subtract_code [code nbe]:
+  "subtract (of_nat n) (of_nat m) = of_nat (n - m)"
   by simp
 
 lemma minus_code_numeral_code [code]:
-  "n - m = subtract_code_numeral n m"
+  "minus = subtract"
   by simp
 
 lemma times_code_numeral_code [code nbe]:
@@ -222,7 +222,7 @@
   by simp
 
 lemma Suc_code_numeral_minus_one:
-  "Suc_code_numeral n - 1 = n"
+  "Suc n - 1 = n"
   by simp
 
 lemma of_nat_code [code]:
@@ -242,27 +242,27 @@
   "nat_of_aux i n = nat_of i + n"
 
 lemma nat_of_aux_code [code]:
-  "nat_of_aux i n = (if i = 0 then n else nat_of_aux (i - 1) (Suc n))"
+  "nat_of_aux i n = (if i = 0 then n else nat_of_aux (i - 1) (Nat.Suc n))"
   by (auto simp add: nat_of_aux_def code_numeral_not_eq_zero)
 
 lemma nat_of_code [code]:
   "nat_of i = nat_of_aux i 0"
   by (simp add: nat_of_aux_def)
 
-definition div_mod_code_numeral :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<times> code_numeral" where
-  [code del]: "div_mod_code_numeral n m = (n div m, n mod m)"
+definition div_mod :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<times> code_numeral" where
+  [code del]: "div_mod n m = (n div m, n mod m)"
 
 lemma [code]:
-  "div_mod_code_numeral n m = (if m = 0 then (0, n) else (n div m, n mod m))"
-  unfolding div_mod_code_numeral_def by auto
+  "div_mod n m = (if m = 0 then (0, n) else (n div m, n mod m))"
+  unfolding div_mod_def by auto
 
 lemma [code]:
-  "n div m = fst (div_mod_code_numeral n m)"
-  unfolding div_mod_code_numeral_def by simp
+  "n div m = fst (div_mod n m)"
+  unfolding div_mod_def by simp
 
 lemma [code]:
-  "n mod m = snd (div_mod_code_numeral n m)"
-  unfolding div_mod_code_numeral_def by simp
+  "n mod m = snd (div_mod n m)"
+  unfolding div_mod_def by simp
 
 definition int_of :: "code_numeral \<Rightarrow> int" where
   "int_of = Nat.of_nat o nat_of"
@@ -280,18 +280,20 @@
   then show ?thesis by (auto simp add: int_of_def mult_ac)
 qed
 
-hide_const (open) of_nat nat_of int_of
 
-subsubsection {* Lazy Evaluation of an indexed function *}
+text {* Lazy Evaluation of an indexed function *}
 
-function iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a Predicate.pred"
+function iterate_upto :: "(code_numeral \<Rightarrow> 'a) \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<Rightarrow> 'a Predicate.pred"
 where
-  "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))"
+  "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))"
 by pat_completeness auto
 
 termination by (relation "measure (%(f, n, m). Code_Numeral.nat_of (m + 1 - n))") auto
 
-hide_const (open) iterate_upto
+hide_const (open) of_nat nat_of Suc  subtract int_of iterate_upto
+
 
 subsection {* Code generator setup *}
 
@@ -316,28 +318,28 @@
 code_reserved SML Int int
 code_reserved Eval Integer
 
-code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
+code_const "plus \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   (SML "Int.+/ ((_),/ (_))")
   (OCaml "Big'_int.add'_big'_int")
   (Haskell infixl 6 "+")
   (Scala infixl 7 "+")
   (Eval infixl 8 "+")
 
-code_const "subtract_code_numeral \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
+code_const "Code_Numeral.subtract \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   (SML "Int.max/ (_/ -/ _,/ 0 : int)")
   (OCaml "Big'_int.max'_big'_int/ (Big'_int.sub'_big'_int/ _/ _)/ Big'_int.zero'_big'_int")
   (Haskell "max/ (_/ -/ _)/ (0 :: Integer)")
   (Scala "!(_/ -/ _).max(0)")
   (Eval "Integer.max/ (_/ -/ _)/ 0")
 
-code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
+code_const "times \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   (SML "Int.*/ ((_),/ (_))")
   (OCaml "Big'_int.mult'_big'_int")
   (Haskell infixl 7 "*")
   (Scala infixl 8 "*")
   (Eval infixl 8 "*")
 
-code_const div_mod_code_numeral
+code_const Code_Numeral.div_mod
   (SML "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (Int.div (n, m), Int.mod (n, m)))")
   (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)")
   (Haskell "divMod")
@@ -351,18 +353,27 @@
   (Scala infixl 5 "==")
   (Eval "!((_ : int) = _)")
 
-code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
+code_const "less_eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   (SML "Int.<=/ ((_),/ (_))")
   (OCaml "Big'_int.le'_big'_int")
   (Haskell infix 4 "<=")
   (Scala infixl 4 "<=")
   (Eval infixl 6 "<=")
 
-code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
+code_const "less \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   (SML "Int.</ ((_),/ (_))")
   (OCaml "Big'_int.lt'_big'_int")
   (Haskell infix 4 "<")
   (Scala infixl 4 "<")
   (Eval infixl 6 "<")
 
+code_modulename SML
+  Code_Numeral Arith
+
+code_modulename OCaml
+  Code_Numeral Arith
+
+code_modulename Haskell
+  Code_Numeral Arith
+
 end
diff -r 42298c5d33b1 -r d1dcb91a512e src/HOL/Library/Code_Natural.thy
--- a/src/HOL/Library/Code_Natural.thy	Sat Feb 18 10:35:45 2012 +0100
+++ b/src/HOL/Library/Code_Natural.thy	Mon Feb 20 12:37:17 2012 +0100
@@ -3,7 +3,7 @@
 *)
 
 theory Code_Natural
-imports Main
+imports "../Main"
 begin
 
 section {* Alternative representation of @{typ code_numeral} for @{text Haskell} and @{text Scala} *}
@@ -125,7 +125,7 @@
   (Haskell infixl 7 "*")
   (Scala infixl 8 "*")
 
-code_const div_mod_code_numeral
+code_const Code_Numeral.div_mod
   (Haskell "divMod")
   (Scala infixl 8 "/%")
 
diff -r 42298c5d33b1 -r d1dcb91a512e src/HOL/Nitpick_Examples/Typedef_Nits.thy
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Sat Feb 18 10:35:45 2012 +0100
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Mon Feb 20 12:37:17 2012 +0100
@@ -153,7 +153,7 @@
 
 lemma "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))"
 nitpick [expect = none]
-by (rule Suc_def)
+by (rule Nat.Suc_def)
 
 lemma "Suc n = Abs_Nat (Suc_Rep (Suc_Rep (Rep_Nat n)))"
 nitpick [expect = genuine]
diff -r 42298c5d33b1 -r d1dcb91a512e src/HOL/Quickcheck.thy
--- a/src/HOL/Quickcheck.thy	Sat Feb 18 10:35:45 2012 +0100
+++ b/src/HOL/Quickcheck.thy	Mon Feb 20 12:37:17 2012 +0100
@@ -139,7 +139,7 @@
 primrec random_aux_set
 where
   "random_aux_set 0 j = collapse (Random.select_weight [(1, Pair valterm_emptyset)])"
-| "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))))])"
+| "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))))])"
 
 lemma [code]:
   "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))))])"
@@ -149,7 +149,7 @@
   show ?case by (subst select_weight_drop_zero[symmetric])
     (simp add: filter.simps random_aux_set.simps[simplified])
 next
-  case (Suc_code_numeral i)
+  case (Suc i)
   show ?case by (simp only: random_aux_set.simps(2)[of "i"] Suc_code_numeral_minus_one)
 qed
 
@@ -164,7 +164,7 @@
 lemma random_aux_rec:
   fixes random_aux :: "code_numeral \<Rightarrow> 'a"
   assumes "random_aux 0 = rhs 0"
-    and "\<And>k. random_aux (Suc_code_numeral k) = rhs (Suc_code_numeral k)"
+    and "\<And>k. random_aux (Code_Numeral.Suc k) = rhs (Code_Numeral.Suc k)"
   shows "random_aux k = rhs k"
   using assms by (rule code_numeral.induct)
 
diff -r 42298c5d33b1 -r d1dcb91a512e src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Sat Feb 18 10:35:45 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Feb 20 12:37:17 2012 +0100
@@ -100,7 +100,7 @@
     fun subst_v t' = map_aterms (fn t as Free (w, _) => if v = w then t' else t | t => t);
     val t_rhs = lambda t_k proto_t_rhs;
     val eqs0 = [subst_v @{term "0::code_numeral"} eq,
-      subst_v (@{term "Suc_code_numeral"} $ t_k) eq];
+      subst_v (@{const Code_Numeral.Suc} $ t_k) eq];
     val eqs1 = map (Pattern.rewrite_term thy rew_ts []) eqs0;
     val ((_, (_, eqs2)), lthy') = Primrec.add_primrec_simple
       [((Binding.conceal (Binding.name random_aux), T), NoSyn)] eqs1 lthy;