theory Scratch
  imports Main
begin

lemma aux: "(x::nat) = 0 \<or> x = 1 \<or>
         (\<exists>a b. (a, b) = (SOME (a', b'). 0 < a' \<and> 0 < b' \<and> a' + b' = a + b) \<and> 0 < a \<and> 0 < b \<and> x = a + b)"
proof (cases "x=0 \<or> x=1")
  case True
  then show ?thesis by auto
next
  case False
  have "(\<exists>a b. (a, b) = (SOME (a', b'). 0 < a' \<and> 0 < b' \<and> a' + b' = x) \<and> 0 < a \<and> 0 < b \<and> x = a + b)"
    apply (rule someI2_ex)
    apply auto
    by (metis False Suc_eq_plus1_left add.right_neutral neq0_conv old.nat.exhaust zero_less_one)
  with False show ?thesis
    by auto
qed

function f :: "nat \<Rightarrow> nat" where
   f0: "f 0 = 0"
| f1: "f 1 = 0"
| fplus_raw: "
   (a,b) = (SOME (a',b'). a' > 0 \<and> b' > 0 \<and> a'+b' = a+b) \<Longrightarrow> 
    a > 0 \<Longrightarrow> b > 0 \<Longrightarrow>
   f (a + b) = f a + f b"
        apply (atomize_elim, rule aux)
       apply auto
  by (metis add_diff_cancel_left' prod.sel(1))

termination by lexicographic_order

lemma fplus[simp]: "a > 0 \<Longrightarrow> b > 0 \<Longrightarrow> f (a + b) = f a + f b"
proof (induction "a+b" arbitrary: a b rule: full_nat_induct)
  case 1
  obtain a' b' :: nat where a'b': "(a',b') = (SOME (a', b'). 0 < a' \<and> 0 < b' \<and> a' + b' = a + b)"
    apply atomize_elim by (smt surj_pair)
  have "let (a',b') = \<dots> in (0 < a' \<and> 0 < b' \<and> a' + b' = a + b)"
    apply (rule someI2_ex)
    using "1.prems" by auto
  with a'b' have "0 < a'" and "0 < b'" and ab: "a' + b' = a + b"
    by auto
  then have "f (a' + b') = f a' + f b'"
    apply (rule_tac fplus_raw)
    using ab a'b' by auto
  with ab have fab: "f (a + b) = f a' + f b'"
    by simp
  consider (less) "a' < a" | (same) "a' = a" | (more) "a' > a"
    using nat_neq_iff by blast
  then have "f a' + f b' = f a + f b"
  proof cases
    case less
    then have "f a + f b = f (a' + (a-a')) + f b"
      by auto
    also have "\<dots> = f a' + f (a-a') + f b"
      apply (subst "1.hyps"[rule_format])
      using \<open>0 < a'\<close> "1.prems"(2) less by auto
    also have "\<dots> = f a' + f ((a-a') + b)"
      apply (subst "1.hyps"[rule_format])
      using "1.prems"(2) less \<open>0 < a'\<close> by auto
    also have "(a-a') + b = b'"
      using ab less by linarith
    finally show ?thesis by simp
  next
    case more
    then have less: "b' < b"
      using ab by linarith
    then have "f a + f b = f a + f ((b-b') + b')"
      by auto
    also have "\<dots> = f a + f (b-b') + f b'"
      apply (subst "1.hyps"[rule_format])
      using \<open>0 < b'\<close> "1.prems"(1) less by auto
    also have "\<dots> = f (a + (b-b')) + f b'"
      apply (subst "1.hyps"[rule_format])
      using less "1.prems" \<open>0 < b'\<close> by auto
    also have "a + (b-b') = a'"
      using ab less by linarith
    finally show ?thesis by simp
  next
    case same
    then show ?thesis
      using ab by auto
  qed
  with fab show ?case
    by simp
qed