# HG changeset patch
# User huffman
# Date 1234818501 28800
# Node ID 922b931fd2ebe73856389f04acc7cb0c82b45098
# Parent  31069b8d39df175ae4665cc32db21ce206b55018
datatype num = One | Dig0 num | Dig1 num

diff -r 31069b8d39df -r 922b931fd2eb src/HOL/ex/Numeral.thy
--- a/src/HOL/ex/Numeral.thy	Mon Feb 16 12:53:59 2009 -0800
+++ b/src/HOL/ex/Numeral.thy	Mon Feb 16 13:08:21 2009 -0800
@@ -11,243 +11,107 @@
 
 subsection {* The @{text num} type *}
 
+datatype num = One | Dig0 num | Dig1 num
+
+text {* Increment function for type @{typ num} *}
+
+primrec
+  inc :: "num \<Rightarrow> num"
+where
+  "inc One = Dig0 One"
+| "inc (Dig0 x) = Dig1 x"
+| "inc (Dig1 x) = Dig0 (inc x)"
+
+text {* Converting between type @{typ num} and type @{typ nat} *}
+
+primrec
+  nat_of_num :: "num \<Rightarrow> nat"
+where
+  "nat_of_num One = Suc 0"
+| "nat_of_num (Dig0 x) = nat_of_num x + nat_of_num x"
+| "nat_of_num (Dig1 x) = Suc (nat_of_num x + nat_of_num x)"
+
+primrec
+  num_of_nat :: "nat \<Rightarrow> num"
+where
+  "num_of_nat 0 = One"
+| "num_of_nat (Suc n) = (if 0 < n then inc (num_of_nat n) else One)"
+
+lemma nat_of_num_gt_0: "0 < nat_of_num x"
+  by (induct x) simp_all
+
+lemma nat_of_num_neq_0: " nat_of_num x \<noteq> 0"
+  by (induct x) simp_all
+
+lemma nat_of_num_inc: "nat_of_num (inc x) = Suc (nat_of_num x)"
+  by (induct x) simp_all
+
+lemma num_of_nat_double:
+  "0 < n \<Longrightarrow> num_of_nat (n + n) = Dig0 (num_of_nat n)"
+  by (induct n) simp_all
+
 text {*
-  We construct @{text num} as a copy of strictly positive
+  Type @{typ num} is isomorphic to the strictly positive
   natural numbers.
 *}
 
-typedef (open) num = "\<lambda>n\<Colon>nat. n > 0"
-  morphisms nat_of_num num_of_nat_abs
-  by (auto simp add: mem_def)
-
-text {*
-  A totalized abstraction function.  It is not entirely clear
-  whether this is really useful.
-*}
-
-definition num_of_nat :: "nat \<Rightarrow> num" where
-  "num_of_nat n = (if n = 0 then num_of_nat_abs 1 else num_of_nat_abs n)"
+lemma nat_of_num_inverse: "num_of_nat (nat_of_num x) = x"
+  by (induct x) (simp_all add: num_of_nat_double nat_of_num_gt_0)
 
-lemma num_cases [case_names nat, cases type: num]:
-  assumes "(\<And>n\<Colon>nat. m = num_of_nat n \<Longrightarrow> 0 < n \<Longrightarrow> P)"
-  shows P
-apply (rule num_of_nat_abs_cases)
-apply (unfold mem_def)
-using assms unfolding num_of_nat_def
-apply auto
-done
-
-lemma num_of_nat_zero: "num_of_nat 0 = num_of_nat 1"
-  by (simp add: num_of_nat_def)
-
-lemma num_of_nat_inverse: "nat_of_num (num_of_nat n) = (if n = 0 then 1 else n)"
-  apply (simp add: num_of_nat_def)
-  apply (subst num_of_nat_abs_inverse)
-  apply (auto simp add: mem_def num_of_nat_abs_inverse)
-  done
-
-lemma num_of_nat_inject:
-  "num_of_nat m = num_of_nat n \<longleftrightarrow> m = n \<or> (m = 0 \<or> m = 1) \<and> (n = 0 \<or> n = 1)"
-by (auto simp add: num_of_nat_def num_of_nat_abs_inject [unfolded mem_def])
-
-lemma nat_of_num_gt_0: "0 < nat_of_num x"
-  using nat_of_num [of x, unfolded mem_def] .
+lemma num_of_nat_inverse: "0 < n \<Longrightarrow> nat_of_num (num_of_nat n) = n"
+  by (induct n) (simp_all add: nat_of_num_inc)
 
 lemma num_eq_iff: "x = y \<longleftrightarrow> nat_of_num x = nat_of_num y"
   apply safe
-  apply (drule arg_cong [where f=num_of_nat_abs])
+  apply (drule arg_cong [where f=num_of_nat])
   apply (simp add: nat_of_num_inverse)
   done
 
-
-lemma split_num_all:
-  "(\<And>m. PROP P m) \<equiv> (\<And>n. PROP P (num_of_nat n))"
-proof
-  fix n
-  assume "\<And>m\<Colon>num. PROP P m"
-  then show "PROP P (num_of_nat n)" .
-next
-  fix m
-  have nat_of_num: "\<And>m. nat_of_num m \<noteq> 0"
-    using nat_of_num by (auto simp add: mem_def)
-  have nat_of_num_inverse: "\<And>m. num_of_nat (nat_of_num m) = m"
-    by (auto simp add: num_of_nat_def nat_of_num_inverse nat_of_num)
-  assume "\<And>n. PROP P (num_of_nat n)"
-  then have "PROP P (num_of_nat (nat_of_num m))" .
-  then show "PROP P m" unfolding nat_of_num_inverse .
-qed
-
-
-subsection {* Digit representation for @{typ num} *}
-
 instantiation num :: "semiring"
 begin
 
-definition One :: num where
-  one_num_def [code del]: "One = num_of_nat 1"
-
 definition plus_num :: "num \<Rightarrow> num \<Rightarrow> num" where
   [code del]: "m + n = num_of_nat (nat_of_num m + nat_of_num n)"
 
 definition times_num :: "num \<Rightarrow> num \<Rightarrow> num" where
   [code del]: "m * n = num_of_nat (nat_of_num m * nat_of_num n)"
 
-definition Dig0 :: "num \<Rightarrow> num" where
-  [code del]: "Dig0 n = n + n"
+lemma nat_of_num_add: "nat_of_num (x + y) = nat_of_num x + nat_of_num y"
+  unfolding plus_num_def
+  by (intro num_of_nat_inverse add_pos_pos nat_of_num_gt_0)
 
-definition Dig1 :: "num \<Rightarrow> num" where
-  [code del]: "Dig1 n = n + n + One"
+lemma nat_of_num_mult: "nat_of_num (x * y) = nat_of_num x * nat_of_num y"
+  unfolding times_num_def
+  by (intro num_of_nat_inverse mult_pos_pos nat_of_num_gt_0)
 
 instance proof
-qed (simp_all add: one_num_def plus_num_def times_num_def
-  split_num_all num_of_nat_inverse num_of_nat_zero add_ac mult_ac nat_distrib)
+qed (simp_all add: num_eq_iff nat_of_num_add nat_of_num_mult nat_distrib)
 
 end
 
-text {*
-  The following proofs seem horribly complicated.
-  Any room for simplification!?
-*}
-
-lemma nat_dig_cases [case_names 0 1 dig0 dig1]:
-  fixes n :: nat
-  assumes "n = 0 \<Longrightarrow> P"
-  and "n = 1 \<Longrightarrow> P"
-  and "\<And>m. m > 0 \<Longrightarrow> n = m + m \<Longrightarrow> P"
-  and "\<And>m. m > 0 \<Longrightarrow> n = Suc (m + m) \<Longrightarrow> P"
-  shows P
-using assms proof (induct n)
-  case 0 then show ?case by simp
-next
-  case (Suc n)
-  show P proof (rule Suc.hyps)
-    assume "n = 0"
-    then have "Suc n = 1" by simp
-    then show P by (rule Suc.prems(2))
-  next
-    assume "n = 1"
-    have "1 > (0\<Colon>nat)" by simp
-    moreover from `n = 1` have "Suc n = 1 + 1" by simp
-    ultimately show P by (rule Suc.prems(3))
-  next
-    fix m
-    assume "0 < m" and "n = m + m"
-    note `0 < m`
-    moreover from `n = m + m` have "Suc n = Suc (m + m)" by simp
-    ultimately show P by (rule Suc.prems(4))
+lemma num_induct [case_names One inc]:
+  fixes P :: "num \<Rightarrow> bool"
+  assumes One: "P One"
+    and inc: "\<And>x. P x \<Longrightarrow> P (inc x)"
+  shows "P x"
+proof -
+  obtain n where n: "Suc n = nat_of_num x"
+    by (cases "nat_of_num x", simp_all add: nat_of_num_neq_0)
+  have "P (num_of_nat (Suc n))"
+  proof (induct n)
+    case 0 show ?case using One by simp
   next
-    fix m
-    assume "0 < m" and "n = Suc (m + m)"
-    have "0 < Suc m" by simp
-    moreover from `n = Suc (m + m)` have "Suc n = Suc m + Suc m" by simp
-    ultimately show P by (rule Suc.prems(3))
-  qed
-qed
-
-lemma num_induct_raw:
-  fixes n :: nat
-  assumes not0: "n > 0"
-  assumes "P 1"
-  and "\<And>n. n > 0 \<Longrightarrow> P n \<Longrightarrow> P (n + n)"
-  and "\<And>n. n > 0 \<Longrightarrow> P n \<Longrightarrow> P (Suc (n + n))"
-  shows "P n"
-using not0 proof (induct n rule: less_induct)
-  case (less n)
-  show "P n" proof (cases n rule: nat_dig_cases)
-    case 0 then show ?thesis using less by simp
-  next
-    case 1 then show ?thesis using assms by simp
-  next
-    case (dig0 m)
-    then show ?thesis apply simp
-      apply (rule assms(3)) apply assumption
-      apply (rule less)
-      apply simp_all
-    done
-  next
-    case (dig1 m)
-    then show ?thesis apply simp
-      apply (rule assms(4)) apply assumption
-      apply (rule less)
-      apply simp_all
-    done
+    case (Suc n)
+    then have "P (inc (num_of_nat (Suc n)))" by (rule inc)
+    then show "P (num_of_nat (Suc (Suc n)))" by simp
   qed
-qed
-
-lemma num_of_nat_Suc: "num_of_nat (Suc n) = (if n = 0 then One else num_of_nat n + One)"
-  by (cases n) (auto simp add: one_num_def plus_num_def num_of_nat_inverse)
-
-lemma num_induct [case_names 1 Suc, induct type: num]:
-  fixes P :: "num \<Rightarrow> bool"
-  assumes 1: "P One"
-    and Suc: "\<And>n. P n \<Longrightarrow> P (n + One)"
-  shows "P n"
-proof (cases n)
-  case (nat m) then show ?thesis by (induct m arbitrary: n)
-    (auto simp: num_of_nat_Suc intro: 1 Suc split: split_if_asm)
-qed
-
-rep_datatype One Dig0 Dig1 proof -
-  fix P m
-  assume 1: "P One"
-    and Dig0: "\<And>m. P m \<Longrightarrow> P (Dig0 m)"
-    and Dig1: "\<And>m. P m \<Longrightarrow> P (Dig1 m)"
-  obtain n where "0 < n" and m: "m = num_of_nat n"
-    by (cases m) auto
-  from `0 < n` have "P (num_of_nat n)" proof (induct n rule: num_induct_raw)
-    case 1 from `0 < n` show ?case .
-  next
-    case 2 with 1 show ?case by (simp add: one_num_def)
-  next
-    case (3 n) then have "P (num_of_nat n)" by auto
-    then have "P (Dig0 (num_of_nat n))" by (rule Dig0)
-    with 3 show ?case by (simp add: Dig0_def plus_num_def num_of_nat_inverse)
-  next
-    case (4 n) then have "P (num_of_nat n)" by auto
-    then have "P (Dig1 (num_of_nat n))" by (rule Dig1)
-    with 4 show ?case by (simp add: Dig1_def one_num_def plus_num_def num_of_nat_inverse)
-  qed
-  with m show "P m" by simp
-next
-  fix m n
-  show "Dig0 m = Dig0 n \<longleftrightarrow> m = n"
-    apply (cases m) apply (cases n)
-    by (auto simp add: Dig0_def plus_num_def num_of_nat_inverse num_of_nat_inject)
-next
-  fix m n
-  show "Dig1 m = Dig1 n \<longleftrightarrow> m = n"
-    apply (cases m) apply (cases n)
-    by (auto simp add: Dig1_def plus_num_def num_of_nat_inverse num_of_nat_inject)
-next
-  fix n
-  show "One \<noteq> Dig0 n"
-    apply (cases n)
-    by (auto simp add: Dig0_def one_num_def plus_num_def num_of_nat_inverse num_of_nat_inject)
-next
-  fix n
-  show "One \<noteq> Dig1 n"
-    apply (cases n)
-    by (auto simp add: Dig1_def one_num_def plus_num_def num_of_nat_inverse num_of_nat_inject)
-next
-  fix m n
-  have "\<And>n m. n + n \<noteq> Suc (m + m)"
-  proof -
-    fix n m
-    show "n + n \<noteq> Suc (m + m)"
-    proof (induct m arbitrary: n)
-      case 0 then show ?case by (cases n) simp_all
-    next
-      case (Suc m) then show ?case by (cases n) simp_all
-    qed
-  qed
-  then show "Dig0 n \<noteq> Dig1 m"
-    apply (cases n) apply (cases m)
-    by (auto simp add: Dig0_def Dig1_def one_num_def plus_num_def num_of_nat_inverse num_of_nat_inject)
+  with n show "P x"
+    by (simp add: nat_of_num_inverse)
 qed
 
 text {*
   From now on, there are two possible models for @{typ num}:
-  as positive naturals (rules @{text "num_induct"}, @{text "num_cases"})
+  as positive naturals (rule @{text "num_induct"})
   and as digit representation (rules @{text "num.induct"}, @{text "num.cases"}).
 
   It is not entirely clear in which context it is better to use
@@ -277,6 +141,9 @@
   | "of_num (Dig0 n) = of_num n + of_num n"
   | "of_num (Dig1 n) = of_num n + of_num n + 1"
 
+lemma of_num_inc: "of_num (inc x) = of_num x + 1"
+  by (induct x) (simp_all add: add_ac)
+
 declare of_num.simps [simp del]
 
 end
@@ -354,25 +221,6 @@
   First, addition and multiplication on digits.
 *}
 
-lemma nat_of_num_add: "nat_of_num (x + y) = nat_of_num x + nat_of_num y"
-  unfolding plus_num_def by (simp add: num_of_nat_inverse nat_of_num_gt_0)
-
-lemma nat_of_num_mult: "nat_of_num (x * y) = nat_of_num x * nat_of_num y"
-  unfolding times_num_def by (simp add: num_of_nat_inverse nat_of_num_gt_0)
-
-lemma nat_of_num_One: "nat_of_num One = 1"
-  unfolding one_num_def by (simp add: num_of_nat_inverse)
-
-lemma nat_of_num_Dig0: "nat_of_num (Dig0 x) = nat_of_num x + nat_of_num x"
-  unfolding Dig0_def by (simp add: nat_of_num_add)
-
-lemma nat_of_num_Dig1: "nat_of_num (Dig1 x) = nat_of_num x + nat_of_num x + 1"
-  unfolding Dig1_def by (simp add: nat_of_num_add nat_of_num_One)
-
-lemmas nat_of_num_simps =
-  nat_of_num_One nat_of_num_Dig0 nat_of_num_Dig1
-  nat_of_num_add nat_of_num_mult
-
 lemma Dig_plus [numeral, simp, code]:
   "One + One = Dig0 One"
   "One + Dig0 m = Dig1 m"
@@ -383,7 +231,7 @@
   "Dig1 n + One = Dig0 (n + One)"
   "Dig1 n + Dig0 m = Dig1 (n + m)"
   "Dig1 n + Dig1 m = Dig0 (n + m + One)"
-  by (simp_all add: num_eq_iff nat_of_num_simps)
+  by (simp_all add: num_eq_iff nat_of_num_add)
 
 lemma Dig_times [numeral, simp, code]:
   "One * One = One"
@@ -395,7 +243,8 @@
   "Dig1 n * One = Dig1 n"
   "Dig1 n * Dig0 m = Dig0 (n * Dig0 m + m)"
   "Dig1 n * Dig1 m = Dig1 (n * Dig1 m + m)"
-  by (simp_all add: num_eq_iff nat_of_num_simps left_distrib right_distrib)
+  by (simp_all add: num_eq_iff nat_of_num_add nat_of_num_mult
+                    left_distrib right_distrib)
 
 text {*
   @{const of_num} is a morphism.
@@ -404,7 +253,7 @@
 context semiring_numeral
 begin
 
-abbreviation "Num1 \<equiv> of_num 1"
+abbreviation "Num1 \<equiv> of_num One"
 
 text {*
   Alas, there is still the duplication of @{term 1},
@@ -417,17 +266,32 @@
 
 lemma of_num_plus_one [numeral]:
   "of_num n + 1 = of_num (n + One)"
-  by (rule sym, induct n) (simp_all add: Dig_plus of_num.simps add_ac)
+  by (rule sym, induct n) (simp_all add: of_num.simps add_ac)
 
 lemma of_num_one_plus [numeral]:
   "1 + of_num n = of_num (n + One)"
   unfolding of_num_plus_one [symmetric] add_commute ..
 
+text {* Rules for addition in the One/inc view *}
+
+lemma add_One: "x + One = inc x"
+  by (simp add: num_eq_iff nat_of_num_add nat_of_num_inc)
+
+lemma add_inc: "x + inc y = inc (x + y)"
+  by (simp add: num_eq_iff nat_of_num_add nat_of_num_inc)
+
+text {* Rules for multiplication in the One/inc view *}
+
+lemma mult_One: "x * One = x"
+  by (simp add: num_eq_iff nat_of_num_mult)
+
+lemma mult_inc: "x * inc y = x * y + x"
+  by (simp add: num_eq_iff nat_of_num_mult nat_of_num_add nat_of_num_inc)
+
 lemma of_num_plus [numeral]:
   "of_num m + of_num n = of_num (m + n)"
   by (induct n rule: num_induct)
-    (simp_all add: Dig_plus of_num_one semigroup_add_class.add_assoc [symmetric, of m]
-    add_ac of_num_plus_one [symmetric])
+     (simp_all add: add_One add_inc of_num_one of_num_inc add_ac)
 
 lemma of_num_times_one [numeral]:
   "of_num n * 1 = of_num n"
@@ -437,14 +301,11 @@
   "1 * of_num n = of_num n"
   by simp
 
-lemma times_One [simp]: "m * One = m"
-  by (simp add: num_eq_iff nat_of_num_simps)
-
 lemma of_num_times [numeral]:
   "of_num m * of_num n = of_num (m * n)"
   by (induct n rule: num_induct)
-    (simp_all add: of_num_plus [symmetric]
-    semiring_class.right_distrib right_distrib of_num_one)
+    (simp_all add: of_num_plus [symmetric] mult_One mult_inc
+    semiring_class.right_distrib right_distrib of_num_one of_num_inc)
 
 end
 
@@ -482,11 +343,8 @@
 lemma nat_of_num_of_num: "nat_of_num = of_num"
 proof
   fix n
-  have "of_num n = nat_of_num n" apply (induct n)
-    apply (simp_all add: of_num.simps)
-    using nat_of_num
-    apply (simp_all add: one_num_def plus_num_def Dig0_def Dig1_def num_of_nat_inverse mem_def)
-    done
+  have "of_num n = nat_of_num n"
+    by (induct n) (simp_all add: of_num.simps)
   then show "nat_of_num n = of_num n" by simp
 qed
 
@@ -500,7 +358,7 @@
 lemma of_num_eq_iff [numeral]:
   "of_num m = of_num n \<longleftrightarrow> m = n"
   unfolding of_nat_of_num [symmetric] nat_of_num_of_num [symmetric]
-    of_nat_eq_iff nat_of_num_inject ..
+    of_nat_eq_iff num_eq_iff ..
 
 lemma of_num_eq_one_iff [numeral]:
   "of_num n = 1 \<longleftrightarrow> n = One"
@@ -541,8 +399,7 @@
   [code del]: "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n"
 
 instance proof
-qed (auto simp add: less_eq_num_def less_num_def
-  split_num_all num_of_nat_inverse num_of_nat_inject split: split_if_asm)
+qed (auto simp add: less_eq_num_def less_num_def num_eq_iff)
 
 end