theory Numeral
  imports Main
begin

typedef num = \<open>{n::nat. n > 0}\<close> morphisms nat_of_num Num
  by auto

setup_lifting type_definition_num

lift_definition One :: num
  is \<open>Suc 0\<close>
  by simp

lift_definition Bit0 :: \<open>num \<Rightarrow> num\<close>
  is \<open>\<lambda>n. Suc (Suc 0) * n\<close>
  by simp

lift_definition Bit1 :: \<open>num \<Rightarrow> num\<close>
  is \<open>\<lambda>n. Suc (Suc (Suc 0) * n)\<close>
  by simp

free_constructors case_num for One | Bit0 | Bit1
proof -
  fix m n :: num
  show \<open>Bit0 n = Bit0 m \<longleftrightarrow> n = m\<close>
    by transfer auto
  show \<open>Bit1 n = Bit1 m \<longleftrightarrow> n = m\<close>
    by transfer auto
  show \<open>One \<noteq> Bit0 n\<close>
    by transfer auto
  show \<open>One \<noteq> Bit1 n\<close>
    by transfer auto
  show \<open>Bit0 m \<noteq> Bit1 n\<close>
    by transfer arith
  show P if \<open>n = One \<Longrightarrow> P\<close> \<open>\<And>m. n = Bit0 m \<Longrightarrow> P\<close> \<open>\<And>m. n = Bit1 m \<Longrightarrow> P\<close> for P
  using that proof (transfer fixing: P)
    fix n :: nat
    assume \<open>n > 0\<close>
      and One: \<open>n = Suc 0 \<Longrightarrow> P\<close>
      and Bit0: \<open>\<And>m. 0 < m \<Longrightarrow> n = Suc (Suc 0) * m \<Longrightarrow> P\<close>
      and Bit1: \<open>\<And>m. 0 < m \<Longrightarrow> n = Suc (Suc (Suc 0) * m) \<Longrightarrow> P\<close>
    consider \<open>n = Suc 0\<close> | \<open>even n\<close> | \<open>n > 2 \<and> odd n\<close>
      by (cases \<open>even n\<close>; cases \<open>n = Suc 0\<close>) (auto elim: oddE)
    then show P
    proof cases
      case 1
      with One show P
        by simp
    next
      case 2
      with \<open>n > 0\<close> Bit0 [of \<open>n div 2\<close>] show P
        by (simp flip: numeral_2_eq_2)
    next
      case 3
      with Bit1 [of \<open>n div 2\<close>] show P
        by (simp flip: numeral_2_eq_2)
    qed
  qed
qed

context
  includes lifting_syntax
begin

lemma num_induct [case_names One Bit0 Bit1, induct type: num]:
  \<open>P n\<close>
  if One: \<open>P One\<close>
  and Bit0: \<open>\<And>n. P n \<Longrightarrow> P (Bit0 n)\<close>
  and Bit1: \<open>\<And>n. P n \<Longrightarrow> P (Bit1 n)\<close>
proof -
  define Q where \<open>Q n = P (Num n)\<close> for n
  have [transfer_rule]: \<open>(pcr_num ===> (\<longleftrightarrow>)) Q P\<close>
  proof
    fix m and n
    assume \<open>pcr_num n m\<close>
    then have \<open>n = nat_of_num m\<close>
      by (auto simp add: pcr_num_def cr_num_def)
    then show \<open>Q n \<longleftrightarrow> P m\<close>
      by (simp add: Q_def nat_of_num_inverse)
  qed
  show ?thesis
  proof transfer
    fix n :: nat
    assume \<open>n > 0\<close>
    moreover from One have \<open>Q (Suc 0)\<close>
      by transfer
    moreover from Bit0 have \<open>\<And>n. n > 0 \<Longrightarrow> Q n \<Longrightarrow> Q (Suc (Suc 0) * n)\<close>
      by transfer
    moreover from Bit1 have \<open>\<And>n. n > 0 \<Longrightarrow> Q n \<Longrightarrow> Q (Suc (Suc (Suc 0) * n))\<close>
      by transfer
    ultimately show \<open>Q n\<close>
    proof (induction n rule: nat_bit_induct)
      case zero
      then show ?case by simp
    next
      case (even n)
      then show ?case by (simp add: mult_2)
    next
      case (odd n)
      then show ?case
        by (cases \<open>n = 0\<close>) (simp_all add: mult_2)
    qed
  qed
qed

end

primrec inc :: \<open>num \<Rightarrow> num\<close>
  where
    \<open>inc One = Bit0 One\<close>
  | \<open>inc (Bit0 x) = Bit1 x\<close>
  | \<open>inc (Bit1 x) = Bit0 (inc x)\<close>

end