GD.thy

theory GD
imports Pure
begin

text \<open>The following theory development formalizes Grounded Arithmetic.\<close>

named_theorems auto "Unconditionally applied lemmas of shape simp \<Longrightarrow> comp"
named_theorems cond "Conditionally applied if P can be solved: P \<Longrightarrow> simp \<Longrightarrow> comp"
named_theorems cases "Tag for cases lemmas used by cases tactic."
named_theorems induct "Tag for induction lemmas used by induct tactic."

section \<open>Axiomatization of truth in GD\<close>

typedecl o

judgment
  Trueprop :: \<open>o \<Rightarrow> prop\<close>  (\<open>_\<close> 5)

axiomatization
  disj :: \<open>o \<Rightarrow> o \<Rightarrow> o\<close>  (infixr \<open>\<or>\<close> 30) and
  not :: \<open>o \<Rightarrow> o\<close> (\<open>\<not> _\<close> [40] 40)
where
  disjI1: \<open>P \<Longrightarrow> P \<or> Q\<close> and
  disjI2: \<open>Q \<Longrightarrow> P \<or> Q\<close> and
  disjI3: \<open>\<lbrakk>\<not>P; \<not>Q\<rbrakk> \<Longrightarrow> \<not>(P \<or> Q)\<close> and
  disjE1: \<open>\<lbrakk>P \<or> Q; P \<Longrightarrow> R; Q \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R\<close> and
  disjE2: \<open>\<not>(P \<or> Q) \<Longrightarrow> \<not>P\<close> and
  disjE3: \<open>\<not>(P \<or> Q) \<Longrightarrow> \<not>Q\<close> and
  dNegI: \<open>P \<Longrightarrow> (\<not>\<not>P)\<close> and
  dNegE: \<open>(\<not>\<not>P) \<Longrightarrow> P\<close> and
  exF: \<open>\<lbrakk>P; \<not>P\<rbrakk> \<Longrightarrow> Q\<close>

section \<open>Axiomatization of naturals in GD\<close>

typedecl num

axiomatization
  eq :: \<open>'a \<Rightarrow> 'a \<Rightarrow> o\<close>  (infixl \<open>=\<close> 45)
where
  eqSubst: \<open>\<lbrakk>a = b; Q a\<rbrakk> \<Longrightarrow> Q b\<close> and
  eqSym: \<open>a = b \<Longrightarrow> b = a\<close> and
  eq_reflection: \<open>x = y \<Longrightarrow> x \<equiv> y\<close>

lemma eq_trans: "a = b \<Longrightarrow> b = c \<Longrightarrow> a = c"
by (rule eqSubst[where a="b" and b="c"], assumption)

definition neq :: \<open>num \<Rightarrow> num \<Rightarrow> o\<close> (infixl \<open>\<noteq>\<close> 45)
  where \<open>a \<noteq> b \<equiv> \<not> (a = b)\<close>
definition bJudg :: \<open>o \<Rightarrow> o\<close> (\<open>_ B\<close> [21] 20)
  where \<open>(p B) \<equiv> (p \<or> \<not>p)\<close>
definition isNat :: \<open>num \<Rightarrow> o\<close> (\<open>_ N\<close> [21] 20)
where "x N \<equiv> x = x"
definition conj :: \<open>o \<Rightarrow> o \<Rightarrow> o\<close> (infixl \<open>\<and>\<close> 35)
  where \<open>p \<and> q \<equiv> \<not>(\<not>p \<or> \<not>q)\<close>
definition impl :: \<open>o \<Rightarrow> o \<Rightarrow> o\<close> (infixr \<open>\<longrightarrow>\<close> 25)
  where \<open>p \<longrightarrow> q \<equiv> \<not>p \<or> q\<close>
definition iff :: \<open>o \<Rightarrow> o \<Rightarrow> o\<close> (infixl \<open>\<longleftrightarrow>\<close> 25)
  where \<open>p \<longleftrightarrow> q \<equiv> (p \<longrightarrow> q) \<and> (q \<longrightarrow> p)\<close>

axiomatization
where
  iff_reflection: "p \<longleftrightarrow> q \<Longrightarrow> p \<equiv> q"

lemma conjE1:
  assumes p_and_q: "p \<and> q"
  shows "p"
apply (rule dNegE)
apply (rule disjE2[where Q="\<not>q"])
apply (fold conj_def)
apply (rule p_and_q)
done

lemma conjE2:
  assumes p_and_q: "p \<and> q"
  shows "q"
apply (rule dNegE)
apply (rule disjE3[where P="\<not>p"])
apply (fold conj_def)
apply (rule p_and_q)
done

lemma conjI [auto]:
  assumes p: "p"
  assumes q: "q"
  shows "p \<and> q"
apply (unfold conj_def)
apply (rule disjI3)
apply (rule dNegI)
apply (rule p)
apply (rule dNegI)
apply (rule q)
done

axiomatization
  zero :: \<open>num\<close>                        and
  suc :: \<open>num \<Rightarrow> num\<close>     (\<open>S(_)\<close> [800]) and
  pred :: \<open>num \<Rightarrow> num\<close>    (\<open>P(_)\<close> [800])
where
  nat0: \<open>zero N\<close> and
  sucInj: \<open>S a = S b \<Longrightarrow> a = b\<close> and
  sucCong: \<open>a = b \<Longrightarrow> S a = S b\<close> and
  predCong: \<open>a = b \<Longrightarrow> P a = P b\<close> and
  eqBool: \<open>\<lbrakk>a N; b N\<rbrakk> \<Longrightarrow> (a = b) B\<close> and
  eqBoolB: \<open>\<lbrakk>x B; y B\<rbrakk> \<Longrightarrow> (x = y) B\<close> and
  sucNonZero: \<open>a N \<Longrightarrow> S a \<noteq> zero\<close> and
  predSucInv: \<open>a N \<Longrightarrow> P(S(a)) = a\<close> and
  pred0: \<open>P(zero) = zero\<close> and
  ind [case_names HQ Base Step]:
           "\<lbrakk>a N; Q zero; \<And>x. x N \<Longrightarrow> Q x \<Longrightarrow> Q S(x)\<rbrakk> \<Longrightarrow> Q a"

definition True
  where \<open>True \<equiv> zero = zero\<close>
definition False
  where \<open>False \<equiv> S(zero) = zero\<close>

lemma zeroRefl [auto]: "zero = zero"
apply (fold isNat_def)
apply (rule nat0)
done

lemma natS [auto]:
  assumes a_nat: "a N"
  shows "S a N"
apply (unfold isNat_def)
apply (rule sucCong)
apply (fold isNat_def)
apply (rule a_nat)
done

lemma natSI:
  assumes a_nat: "S(a) N"
  shows "a N"
apply (unfold isNat_def)
apply (rule sucInj)
apply (fold isNat_def)
apply (rule a_nat)
done

lemma natP [auto]:
  assumes a_nat: "a N"
  shows "P a N"
apply (unfold isNat_def)
apply (rule predCong)
apply (fold isNat_def)
apply (rule a_nat)
done

lemma implI:
  assumes a_bool: "a B"
  assumes a_deduce_b: "a \<Longrightarrow> b"
  shows "a \<longrightarrow> b"
proof (unfold impl_def, rule disjE1[where P="a" and Q="\<not>a"])
  show "a \<or> \<not>a" by (fold GD.bJudg_def, rule a_bool)
  next
    show "a \<Longrightarrow> \<not>a \<or> b" by (rule disjI2, rule a_deduce_b, assumption)
  next
    show "\<not>a \<Longrightarrow> \<not>a \<or> b" by (rule disjI1, assumption)
qed

lemma implE:
  assumes H1: "a \<longrightarrow> b"
  assumes H2: "a"
  shows "b"
proof (rule disjE1[where P="\<not>a" and Q="b"])
  show "\<not>a \<or> b"
    apply (fold impl_def)
    apply (rule H1)
    done
  next
    assume not_a: "\<not>a"
    show "b"
    apply (rule exF[where P="a"])
    apply (rule H2)
    apply (rule not_a)
    done
  next
    show "b \<Longrightarrow> b"
    apply (assumption)
    done
qed

lemma iffE1: "a \<longleftrightarrow> b \<Longrightarrow> a \<longrightarrow> b"
apply (rule conjE1)
apply (unfold iff_def)
apply (assumption)
done

lemma iffE2: "a \<longleftrightarrow> b \<Longrightarrow> b \<longrightarrow> a"
apply (rule conjE2)
apply (unfold iff_def)
apply (assumption)
done

lemma iffI:
  assumes a_bool: "a B"
  assumes b_bool: "b B"
  assumes a_deduce_b: "a \<Longrightarrow> b"
  assumes b_deduce_a: "b \<Longrightarrow> a"
  shows "a \<longleftrightarrow> b"
unfolding iff_def
apply (rule conjI)
apply (rule implI, rule a_bool, rule a_deduce_b, assumption)
apply (rule implI, rule b_bool, rule b_deduce_a, assumption)
done

lemma grounded_contradiction:
  assumes p_bool: \<open>p B\<close>
  assumes notp_q: \<open>\<not>p \<Longrightarrow> q\<close>
  assumes notp_notq: \<open>\<not>p \<Longrightarrow> \<not>q\<close>
  shows \<open>p\<close>
proof (rule disjE1[where P="p" and Q="\<not>p"])
  show "p \<or> \<not>p"
    using p_bool unfolding GD.bJudg_def .
  show "p \<Longrightarrow> p" by assumption
  show "\<not>p \<Longrightarrow> p"
  proof -
    assume not_p: "\<not>p"
    have q: "q" using notp_q[OF not_p] .
    have not_q: "\<not>q" using notp_notq[OF not_p] .
    from q and not_q show "p"
      by (rule exF)
  qed
qed

syntax
  "_gd_num" :: "num_token \<Rightarrow> num"    ("_")

ML_file "peano_numerals.ML"

parse_translation \<open>
  [(@{syntax_const "_gd_num"}, Peano_Syntax.parse_gd_numeral)]
\<close>

lemma contradiction:
  assumes p_bool: "p B"
  assumes contr: "\<not>p \<Longrightarrow> False"
  shows "p"
apply (rule grounded_contradiction[where q="False"])
apply (rule p_bool)
proof -
  assume not_p: "\<not>p"
  show "False"
    apply (rule contr)
    apply (rule not_p)
    done
  show "\<not>False"
    apply (unfold False_def)
    apply (fold neq_def)
    apply (rule sucNonZero)
    apply (rule nat0)
    done
qed

(* Entailment reduces to almost the same as object-level implication \<longrightarrow>.
 * The difference is that the \<longrightarrow> introduction rule requires 'a' to be
 * proven boolean first ('a B'), while entailment does not. It is a
 * direct object-level mirroring of the meta-level a \<Longrightarrow> b.
 * Meta-level just means that it is of type prop \<Rightarrow> prop \<Rightarrow> prop,
 * while entailment mirrors this at the object level, that is, it's
 * of type o \<Rightarrow> o \<Rightarrow> o.
 * With entailment, GD can reason about deducability at the object level,
 * which adds a lot of expressive power.
 *)
axiomatization
  entails :: "o \<Rightarrow> o \<Rightarrow> o"    (infixr "\<turnstile>" 10)
where
  entailsI: "\<lbrakk>a \<Longrightarrow> b\<rbrakk> \<Longrightarrow> (a \<turnstile> b)" and
  entailsE: "\<lbrakk>a \<turnstile> b; a\<rbrakk> \<Longrightarrow> b"

axiomatization
  forall :: "(num \<Rightarrow> o) \<Rightarrow> o"  (binder "\<forall>" [8] 9) and
  exists :: "(num \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>" [8] 9)
where
  forallI: "\<lbrakk>\<And>x. x N \<Longrightarrow> Q x\<rbrakk> \<Longrightarrow> \<forall>x. Q x" and
  forallE: "\<lbrakk>\<forall>c'. Q c'; a N\<rbrakk> \<Longrightarrow> Q a" and
  existsI: "\<lbrakk>a N; Q a\<rbrakk> \<Longrightarrow> \<exists>x. Q x" and
  existsE: "\<lbrakk>\<exists>i. Q i; \<And>a. a N \<Longrightarrow> Q a \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
  (*
  forAllNeg: "\<lbrakk>\<not>(\<forall>x. Q x); (Q x) B\<rbrakk> \<Longrightarrow> \<exists>x. \<not>(Q x)" and
  existsNeg: "\<lbrakk>\<not>(\<exists>x. Q x); (Q x) B\<rbrakk> \<Longrightarrow> \<forall>x. \<not>(Q x)" and
   *)

section \<open>Axiomatization of conditional evaluation in GD\<close>

consts
  cond :: \<open>o \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (\<open>if _ then _ else _\<close> [25, 24, 24] 24)

axiomatization where
  condI1: \<open>\<lbrakk>c; a N\<rbrakk> \<Longrightarrow> (if c then a else b) = a\<close> and
  condI2: \<open>\<lbrakk>\<not>c; b N\<rbrakk> \<Longrightarrow> (if c then a else b) = b\<close> and
  condT: \<open>\<lbrakk>c B; a N; b N\<rbrakk> \<Longrightarrow> if c then a else b N\<close> and
  condI1B: \<open>\<lbrakk>c; d B\<rbrakk> \<Longrightarrow> (if c then d else e) = d\<close> and
  condI2B: \<open>\<lbrakk>\<not>c; e B\<rbrakk> \<Longrightarrow> (if c then d else e) = e\<close> and
  condTB: \<open>\<lbrakk>c B; d B; e B\<rbrakk> \<Longrightarrow> if c then d else e B\<close>

lemma condI1BEq:
  assumes c_holds: "c"
  assumes d_bool: "d B"
  assumes a_eq_d: "a = d"
  shows "(if c then a else b) = d"
apply (rule eqSubst[where a="d" and b="a"])
apply (rule eqSym)
apply (rule a_eq_d)
apply (rule condI1B)
apply (rule c_holds)
apply (rule d_bool)
done

lemma condI2BEq:
  assumes not_c: "\<not>c"
  assumes d_bool: "d B"
  assumes a_eq_d: "b = d"
  shows "(if c then a else b) = d"
apply (rule eqSubst[where a="d" and b="b"])
apply (rule eqSym)
apply (rule a_eq_d)
apply (rule condI2B)
apply (rule not_c)
apply (rule d_bool)
done

lemma condI3B:
  shows "a B \<Longrightarrow> c B \<Longrightarrow> (if c then a else a) = a"
apply (rule disjE1[where P="c" and Q="\<not>c"])
apply (fold GD.bJudg_def, simp)
apply (rule condI1B, simp+)
apply (rule condI2B, simp+)
done

lemma condI3BEq:
  assumes a_bool: "a B"
  assumes c_bool: "c B"
  assumes d_eq_a: "d = a"
  assumes e_eq_a: "e = a"
  shows "(if c then d else e) = a"
apply (rule disjE1[where P="c" and Q="\<not>c"])
apply (fold GD.bJudg_def)
apply (rule c_bool)
apply (rule eqSubst[where a="a" and b="d"])
apply (rule eqSym)
apply (rule d_eq_a)
apply (rule condI1B)
apply (assumption)
apply (rule a_bool)
apply (rule eqSubst[where a="a" and b="e"])
apply (rule eqSym)
apply (rule e_eq_a)
apply (rule condI2B)
apply (assumption)
apply (rule a_bool)
done

lemma condI1Eq:
  assumes c_holds: "c"
  assumes d_nat: "d N"
  assumes a_eq_d: "a = d"
  shows "(if c then a else b) = d"
apply (rule eqSubst[where a="d" and b="a"])
apply (rule eqSym)
apply (rule a_eq_d)
apply (rule condI1)
apply (rule c_holds)
apply (rule d_nat)
done

lemma condI2Eq:
  assumes not_c: "\<not>c"
  assumes d_nat: "d N"
  assumes a_eq_d: "b = d"
  shows "(if c then a else b) = d"
apply (rule eqSubst[where a="d" and b="b"])
apply (rule eqSym)
apply (rule a_eq_d)
apply (rule condI2)
apply (rule not_c)
apply (rule d_nat)
done

lemma condI3:
  shows "a N \<Longrightarrow> c B \<Longrightarrow> (if c then a else a) = a"
apply (rule disjE1[where P="c" and Q="\<not>c"])
apply (fold GD.bJudg_def, simp)
apply (rule condI1, simp+)
apply (rule condI2, simp+)
done

lemma condI3Eq:
  assumes a_nat: "a N"
  assumes c_bool: "c B"
  assumes d_eq_a: "c \<Longrightarrow> d = a"
  assumes e_eq_a: "\<not> c \<Longrightarrow> e = a"
  shows "(if c then d else e) = a"
apply (rule disjE1[where P="c" and Q="\<not>c"])
apply (fold GD.bJudg_def)
apply (rule c_bool)
apply (rule eqSubst[where a="a" and b="d"])
apply (rule eqSym)
apply (rule d_eq_a)
apply (assumption)
apply (rule condI1)
apply (assumption)
apply (rule a_nat)
apply (rule eqSubst[where a="a" and b="e"])
apply (rule eqSym)
apply (rule e_eq_a)
apply (assumption)
apply (rule condI2)
apply (assumption)
apply (rule a_nat)
done

ML_file "gd_auto.ML"
ML_file "gd_subst.ML"

section \<open>Definitional Mechanism in GD\<close>

axiomatization
  def :: \<open>'a \<Rightarrow> 'a \<Rightarrow> o\<close> (infix \<open>:=\<close> 10)
where
  defE: \<open>\<lbrakk>a := b; Q b\<rbrakk> \<Longrightarrow> Q a\<close> and
  defI: \<open>\<lbrakk>a := b; Q a\<rbrakk> \<Longrightarrow> Q b\<close>

ML_file "gd_simp.ML"

lemmas [simp] = predSucInv neq_def pred0 condI1 condI1B condI2 condI2B condI3B condI3 
lemmas [auto] = nat0 sucNonZero predSucInv pred0 eqBool eqBoolB disjI3 dNegI

lemma [simp]: "(a = a) \<equiv> (a N)"
  unfolding isNat_def by (rule Pure.reflexive)

ML_file \<open>unfold_def.ML\<close>

section \<open>Deductions of non-elementary inference rules.\<close>

lemma true [auto]: "True"
  unfolding True_def by auto

lemma true_bool [auto]: "True B"
  unfolding bJudg_def by (rule disjI1, rule true)

lemma bool_refl: "a B \<Longrightarrow> a = a"
apply (rule eqSubst[where a="(if True then a else a)" and b="a"])
apply (rule condI1B, simp)
apply (rule condI1BEq, simp)
apply (rule condTB, simp)
apply (rule eqSym)
apply (rule condI1B, simp)
done

lemma eq_impl_term: "a = b \<Longrightarrow> a N"
apply (rule entailsE[where a="a=b"])
apply (unfold isNat_def)
apply (subst "a=b", assumption)
apply (rule entailsI, simp)
done

lemma [simp]: "a B \<Longrightarrow> (a = a) \<longleftrightarrow> True"
by (rule iffI, simp, rule bool_refl)

lemma [simp]: "\<not>c \<Longrightarrow> b N \<Longrightarrow> d N \<Longrightarrow> (if c then a else b) = d \<longleftrightarrow> b = d"
by (rule iffI, simp+)

lemma [simp]: "c \<Longrightarrow> a N \<Longrightarrow> d N \<Longrightarrow> (if c then a else b) = d \<longleftrightarrow> a = d"
by (rule iffI, simp+)

lemma [simp]: "\<not>c \<Longrightarrow> b B \<Longrightarrow> d B \<Longrightarrow> (if c then a else b) = d \<longleftrightarrow> b = d"
by (rule iffI, simp+)

lemma [simp]: "c \<Longrightarrow> a B \<Longrightarrow> d B \<Longrightarrow> (if c then a else b) = d \<longleftrightarrow> a = d"
by (rule iffI, simp+)

lemma [simp]: "c \<Longrightarrow> (if c then True else b) = True"
by simp

lemma [simp]: "\<not>c \<Longrightarrow> (if c then a else True) = True"
by simp

lemma [cond]: "a \<Longrightarrow> a B"
  unfolding bJudg_def by (rule disjI1, simp)

lemma [cond]: "\<not>a \<Longrightarrow> a B"
  unfolding bJudg_def by (rule disjI2, simp)

lemma if_trueI [auto]: "c \<Longrightarrow> if c then True else False"
  by simp

lemma [auto]: "True = True"
  by simp

lemma not_false [auto]: "\<not>False"
proof (unfold False_def)
  show "\<not>(S(0) = 0)"
  proof -
    have "S(0) \<noteq> 0" by (rule sucNonZero) (rule nat0)
    then show ?thesis by (unfold neq_def)
  qed
qed

lemma false_bool [auto]: "False B"
proof (unfold bJudg_def)
  show "False \<or> \<not>False"
  proof -
    have "\<not>False" by (rule not_false)
    then show ?thesis by (rule disjI2[where Q="\<not>False" and P="False"])
  qed
qed

lemma disj_comm:
  assumes q_or_r: "Q \<or> R"
  shows "R \<or> Q"
proof (rule disjE1[where P="Q" and Q="R" and R="R \<or> Q"])
  show "Q \<or> R" by (rule q_or_r)
  show "Q \<Longrightarrow> R \<or> Q"
    proof -
      assume Q
      then show "R \<or> Q" by (rule disjI2[where Q="Q" and P="R"])
    qed
  show "R \<Longrightarrow> R \<or> Q"
    proof -
      assume R
      then show "R \<or> Q" by (rule disjI1[where P="R" and Q="Q"])
    qed
qed

lemma not_bool [auto]:
  assumes a_bool: "a B"
  shows "(\<not>a) B"
apply (unfold GD.bJudg_def)
apply (rule disjE1[where P="\<not>a" and Q="a"])
apply (rule disj_comm)
apply (fold GD.bJudg_def)
apply (rule a_bool)
apply (unfold GD.bJudg_def)
apply (rule disjI1)
apply (assumption)
apply (rule disjI2)
apply (rule dNegI)
apply (assumption)
done

lemma neq_sym:
  assumes a_nat: "a N"
  assumes b_nat: "b N"
  assumes ab_neq: "a \<noteq> b"
  shows "b \<noteq> a"
proof (unfold neq_def, rule grounded_contradiction[where q="a=b"])
  show "(\<not>(b=a)) B"
    apply (auto)
    apply (rule b_nat)
    apply (rule a_nat)
    done
  next
    assume H: "\<not> \<not> b = a"
    show "a = b"
    apply (rule eqSym)
    apply (rule dNegE)
    apply (rule H)
    done
  next
    assume H: "\<not> \<not> b = a"
    show "\<not> a = b"
    apply (fold neq_def)
    apply (rule ab_neq)
    done
qed

lemma neq_bool [auto]: "a N \<Longrightarrow> b N \<Longrightarrow> (a \<noteq> b) B"
by simp

lemma sucNotEqual [auto]: "a N \<Longrightarrow> a \<noteq> S(a)"
proof (rule ind[where a="a"], simp)
  show "0 \<noteq> S(0)"
    by (rule neq_sym, simp)
  show "\<And>x. x N \<Longrightarrow> (x\<noteq>S(x)) \<Longrightarrow> (S(x) \<noteq> S(S(x)))"
    proof -
      fix x
      assume x_neq_s: "x \<noteq> S(x)"
      show "x N \<Longrightarrow> S(x) \<noteq> S(S(x))"
      proof (rule grounded_contradiction[where q="False"], simp)
        assume H: "\<not> (S x \<noteq> S(S x))"
        have eq_suc: "x = S(x)"
          apply (rule sucInj)
          apply (rule dNegE)
          apply (fold neq_def)
          apply (rule H)
          done
        then show "False"
          apply (rule exF)
          apply (fold neq_def)
          apply (rule x_neq_s)
          done
        show "\<not> False"
        by simp
      qed
    qed
qed

section \<open>Definitions of basic arithmetic functions\<close>

(* Use the recursion mechanism to define the standard arithmetic functions to
 * be available in a global context.
 * Axiomatizing them simply means that the fact that they are defined with the
 * given definitions are axioms.
 * User-defined functions should be in locales,
 * not in axiomatization blocks.
 *)

(*
recdef add :: "num \<Rightarrow> num \<Rightarrow> num" where
  "add x y := if y = 0 then x else S(add x P(y))"
*)

axiomatization
  add   :: "num \<Rightarrow> num \<Rightarrow> num"  (infixl "+" 60) and
  sub   :: "num \<Rightarrow> num \<Rightarrow> num"  (infixl "-" 60) and
  mult  :: "num \<Rightarrow> num \<Rightarrow> num"  (infixl "*" 70) and
  div   :: "num \<Rightarrow> num \<Rightarrow> num"                  and
  less  :: "num \<Rightarrow> num \<Rightarrow> num"  (infix "<" 50)  and
  leq   :: "num \<Rightarrow> num \<Rightarrow> num"  (infix "\<le>" 50) and
  omega :: "'a"
where
  add_def:   "add x y  := if y = 0 then x else S(add x (P y))"       and
  sub_def:   "sub x y  := if y = 0 then x else P(sub x (P y))"       and
  mult_def:  "mult x y := if y = 0 then 0 else (x + mult x (P y))"   and
  leq_def:   "leq x y  := if x = 0 then 1
                          else if y = 0 then 0
                          else (leq (P x) (P y))"                    and
  less_def:  "less x y := if y = 0 then 0
                          else if x = 0 then 1
                          else (less (P x) (P y))"                   and
  div_def:   "div x y  := if x < y = 1 then 0 else S(div (x - y) y)" and
  omega_def: "omega    := omega"

definition greater :: "num \<Rightarrow> num \<Rightarrow> num" (infix ">" 50) where
  "greater x y \<equiv> 1 - (x \<le> y)"

definition geq :: "num \<Rightarrow> num \<Rightarrow> num" (infix "\<ge>" 50) where
  "geq x y \<equiv> 1 - (x < y)"

lemma less_0_false [simp, auto]: "(x < 0) = 0"
apply (rule defE[OF less_def])
apply (rule condI1)
apply (rule zeroRefl)
apply (rule nat0)
done

lemma add_terminates [auto]:
  assumes x_nat: \<open>x N\<close>
  assumes y_nat: \<open>y N\<close>
  shows \<open>add x y N\<close>
proof (rule ind[where a=y])
  show "y N" by (rule y_nat)
  show "add x 0 N"
    proof (rule defE[OF add_def])
      show "if (0 = 0) then x else S(add x P(0)) N"
        apply (rule eqSubst[where a="x"])
        apply (rule eqSym)
        apply (rule condI1)
        apply (rule zeroRefl)
        apply (rule x_nat)
        apply (rule x_nat)
        done
    qed
  show ind_step: "\<And>a. a N \<Longrightarrow> ((x + a) N) \<Longrightarrow> ((x + S(a)) N)"
    proof (rule defE[OF add_def])
      fix a
      assume a_nat: "a N" and BC: "add x a N"
      show "if (S(a) = 0) then x else S(add x P(S(a))) N"
        proof (rule condT)
          show "S(a) = 0 B"
            apply (rule eqBool)
            apply (rule natS)
            apply (rule a_nat)
            apply (rule nat0)
            done
          show "x N" by (rule x_nat)
          show "S(add x P(S(a))) N"
            apply (rule GD.natS)
            apply (rule eqSubst[where a="x+a"])
            apply (rule eqSubst[where a="a" and b="P(S(a))"])
            apply (rule eqSym)
            apply (rule predSucInv)
            apply (rule a_nat)
            apply (fold isNat_def)
            apply (rule BC)
            apply (rule BC)
            done
        qed
    qed
qed

lemma cases_bool:
  assumes q_bool: "q B"
  assumes H: "q \<Longrightarrow> p"
  assumes H1: "\<not>q \<Longrightarrow> p"
  shows "p"
apply (rule disjE1[where P="q" and Q="\<not>q"])
apply (fold bJudg_def)
apply (rule q_bool)
apply (rule H)
apply (assumption)
apply (rule H1)
apply (assumption)
done

(*
declare [[simp_trace = true, simp_trace_depth_limit = 8]]
 *)

lemma [auto]: "c B \<Longrightarrow> if c then True else True"
  by simp

lemma [auto]: "c B \<Longrightarrow> \<not> (if c then False else False)"
  by simp

lemma mult_terminates [auto]:
  shows \<open>x N \<Longrightarrow> y N \<Longrightarrow> mult x y N\<close>
proof (rule ind[where a=y])
  show "y N \<Longrightarrow> y N" by simp
  show "x N \<Longrightarrow> mult x 0 N"
    by (unfold_def mult_def, simp)
  fix a
  show "a N \<Longrightarrow> x N \<Longrightarrow> mult x a N \<Longrightarrow> mult x (S a) N"
    by (unfold_def mult_def, rule condT, simp+)
qed

lemma [auto]: "x N \<Longrightarrow> \<not> S(x) = 0"
  by (fold neq_def, auto)

lemma add_zero [simp, auto]:
  assumes a_nat: "a N"
  shows "a + 0 = a"
apply (unfold_def add_def)
apply (rule condI1)
apply (rule zeroRefl)
apply (rule a_nat)
done

lemma zero_add [simp, auto]:
  shows "a N \<Longrightarrow> 0 + a = a"
proof (rule ind[where a="a"], simp)
  fix x
  assume hyp: "0 + x = x"
  show "a N \<Longrightarrow> x N \<Longrightarrow> 0 + S x = S x"
    by (unfold_def add_def, simp add: hyp)
qed

lemma add_succ [auto]:
  shows "a N \<Longrightarrow> b N \<Longrightarrow> a + S b = S (a + b)"
apply (rule eqSym)
apply (unfold_def add_def)
apply (rule eqSym)
apply (simp)+
done
lemma mult_zero [simp, auto]: shows "a * 0 = 0" by (unfold_def mult_def, rule condI1, auto)

lemma zero_mult [simp, auto]:
  shows "a N \<Longrightarrow> 0 * a = 0"
proof (rule ind[where a="a"], auto)
  fix x
  assume hyp: "0 * x = 0"
  show "a N \<Longrightarrow> x N \<Longrightarrow> 0 * S x = 0"
    by (unfold_def mult_def, simp add: hyp)
qed

lemma mult_one [simp, auto]:
  shows "a N \<Longrightarrow> a * 1 = a"
by (unfold_def mult_def, simp)

lemma plus_one_suc [simp, auto]:
  shows "a N \<Longrightarrow> 1 + a = S a"
proof (rule ind[where a="a"], auto)
  fix x
  assume hyp: "1+x = S x"
  show "a N \<Longrightarrow> x N \<Longrightarrow> 1+(S x) = S S x"
    by (unfold_def add_def, simp add: hyp)
qed

lemma one_plus_suc [simp, auto]:
  shows "a N \<Longrightarrow> a + 1 = S a"
by (unfold_def add_def, simp)

lemma [auto]: "x N \<Longrightarrow> x = x"
by (fold isNat_def)

lemma one_mult [simp, auto]:
  shows "a N \<Longrightarrow> 1 * a = a"
proof (rule ind[where a="a"], auto)
  fix x
  assume hyp: "1*x = x"
  show "a N \<Longrightarrow> x N \<Longrightarrow> 1*(S x) = S x"
    by (unfold_def mult_def, simp add: hyp)
qed

lemma zero_leq_true [simp, auto]:
  assumes x_nat: "x N"
  shows "0 \<le> x = 1"
by (unfold_def leq_def, rule condI1Eq, auto)

lemma leq_terminates [auto]:
  shows "x N \<Longrightarrow> y N \<Longrightarrow> x \<le> y N"
proof -
  have H: "y N \<Longrightarrow> \<forall>x. x\<le>y N"
  proof (rule ind[where a="y"], simp)
    show "\<forall>x'. x' \<le> 0 N"
      apply (rule forallI)
      apply (rule defE[OF leq_def])
      apply (rule condT)
      apply (rule eqBool)
      apply (assumption)
      apply (rule nat0)
      apply (rule natS)
      apply (rule nat0)
      apply (rule eqSubst[where a="0"])
      apply (rule eqSym)
      apply (rule condI1)
      apply (rule zeroRefl)
      apply (rule nat0)+
      done
    show "\<And>x. x N \<Longrightarrow> (\<forall>xa. xa \<le> x N) \<Longrightarrow> (\<forall>xa. xa \<le> S(x) N)"
      proof -
        fix x
        assume H: "\<forall>xa. xa \<le> x N"
        show "x N \<Longrightarrow> \<forall>xa. xa \<le> S(x) N"
          proof (rule forallI)
            fix xa
            show "x N \<Longrightarrow> xa N \<Longrightarrow> xa \<le> S(x) N"
              apply (rule defE[OF leq_def])
              apply (rule condT)
              apply (rule eqBool)
              apply (assumption)
              apply (rule nat0)+
              apply (rule natS, rule nat0)
              apply (rule condT)
              apply (rule eqBool)
              apply (rule natS, assumption)
              apply (rule nat0)+
              apply (rule eqSubst[where a="x" and b="P S x"])
              apply (rule eqSym, rule predSucInv, assumption)
              apply (rule forallE[where a="P xa"])
              apply (rule H)
              apply (rule natP, assumption)
              done
          qed
      qed
  qed
  then show "x N \<Longrightarrow> y N \<Longrightarrow> x \<le> y N"
    by (rule forallE)
qed

lemma less_terminates [auto]:
  shows "x N \<Longrightarrow> y N \<Longrightarrow> x < y N"
proof -
  have q: "y N \<Longrightarrow> \<forall>x. x < y N"
  proof (rule ind[where a="y"], simp)
    show "\<forall>x. x < 0 N"
      by (rule forallI, simp)
    show "\<And>x. x N \<Longrightarrow> (\<forall>xa. xa < x N) \<Longrightarrow> (\<forall>xa. xa < S x N)"
      proof (rule forallI)+
        fix x y
        assume hyp: "\<forall>xa. xa < x N"
        show "x N \<Longrightarrow> y N \<Longrightarrow> y < S x N"
          apply (unfold_def less_def)
          apply (rule condT)
          apply (simp+)
          apply (rule condT)
          apply (simp+)
          apply (rule forallE[where a="P y"])
          apply (rule hyp)
          apply (simp)
          done
      qed
  qed
  show "x N \<Longrightarrow> y N \<Longrightarrow> x < y N"
    by (rule forallE[where a="x"], rule q, simp)
qed

lemma leq_refl [simp, auto]:
  shows "x N \<Longrightarrow> (x \<le> x) = 1"
proof (rule ind[where a="x"], simp)
  show "\<And>x. x N \<Longrightarrow> (x \<le> x = 1) \<Longrightarrow> (S(x) \<le> S(x) = 1)"
  proof -
    fix x
    assume x_refl: "x \<le> x = 1"
    show "x N \<Longrightarrow> ((S(x)) \<le> S(x)) = 1"
      apply (unfold_def leq_def)
      apply (simp add: x_refl)+
      done
  qed
qed

lemma pred_leq [simp, auto]:
  assumes z_nat: "z N"
  shows "P(z) \<le> z = 1"
proof (rule ind[where a="z"])
  show "z N" by (rule z_nat)
  show "((P(0)) \<le> 0) = 1"
    by (unfold_def leq_def, simp)
  show "\<And>x. x N \<Longrightarrow> ((P(x))\<le>x = 1) \<Longrightarrow> (((P(S(x)))\<le>S(x)) = 1)"
    proof -
      fix x
      assume ind_hyp: "((P(x)) \<le> x) = 1"
      show "x N \<Longrightarrow> ((P(S(x))) \<le> (S(x))) = 1"
        apply (unfold_def leq_def)
        apply (rule condI3Eq)
        apply (simp add: ind_hyp)+
        done
    qed
qed

lemma leq_suc [simp, auto]:
  shows "x N \<Longrightarrow> x \<le> S(x) = 1"
apply (rule ind[where a="x"])
proof (auto)
  fix x
  assume hyp: "x \<le> S x = 1"
  show "x N \<Longrightarrow> S x \<le> S S x = 1"
    by (unfold_def leq_def, simp add: hyp)
qed

lemma less_suc [simp, auto]:
  shows "x N \<Longrightarrow> x < S(x) = 1"
apply (rule ind[where a="x"], simp)
apply (unfold_def less_def, simp)+
done

lemma [auto]: "x N \<Longrightarrow> \<not> 0 = S x"
apply (fold neq_def)
apply (rule neq_sym)
apply (simp)
done

lemma leq_0:
  shows "x N \<Longrightarrow> x \<le> 0 = 1 \<Longrightarrow> x = 0"
proof (rule grounded_contradiction[where q="False"])
  show "x N \<Longrightarrow> x = 0 B" by (simp)
  show "x N \<Longrightarrow> x \<le> 0 = 1 \<Longrightarrow> \<not> x = 0 \<Longrightarrow> False"
    apply (rule exF[where P="x \<le> 0 = 1"])
    apply (simp)
    apply (rule eqSubst[where a="0" and b="x \<le> 0"])
    apply (unfold_def leq_def)
    apply (simp+)
    done
  show "\<not>False" by (simp)
qed

lemma leq_monotone_suc [simp]:
  shows "x N \<Longrightarrow> y N \<Longrightarrow> x \<le> y = 1 \<Longrightarrow> S x \<le> S y = 1"
by (unfold_def leq_def, simp)

lemma num_cases:
  shows "x N \<Longrightarrow> x = 0 \<or> (\<exists>y. x = S y)"
proof (rule ind[where a="x"], simp)
  show "0 = 0 \<or> (\<exists>y. 0 = S y)" by (rule disjI1, simp)
  show "\<And>x. x N \<Longrightarrow> x=0 \<or> (\<exists>y. x = S y) \<Longrightarrow> S x = 0 \<or> (\<exists>y. S x = S y)"
    proof -
      fix x
      show "x N \<Longrightarrow> S x = 0 \<or> (\<exists>y. S x = S y)"
        apply (rule disjI2)
        apply (rule existsI[where a="x"])
        apply (simp)
        done
    qed
qed

lemma num_nonzero [auto]:
  "x N \<Longrightarrow> \<not> x = 0 \<Longrightarrow> \<exists>y. x = S(y)"
proof -
  have "x N \<Longrightarrow> x = 0 \<or> (\<exists>y. x = S y)"
    by (rule num_cases, simp)
  then show "x N \<Longrightarrow> \<not> x = 0 \<Longrightarrow> \<exists>y. x = S(y)"
    apply (rule disjE1, simp)
    apply (rule exF[where P="x=0"], simp)
    done
qed

lemma leq_nz_monotone:
  shows "ya N \<Longrightarrow> \<not> xa = 0 \<Longrightarrow> xa \<le> ya = 1 \<Longrightarrow> ya \<noteq> 0"
proof (rule grounded_contradiction[where q="xa \<le> 0 = 1"])
  show "ya N \<Longrightarrow> ya \<noteq> 0 B" by (simp)
  show "\<not> ya \<noteq> 0 \<Longrightarrow> xa \<le> ya = 1 \<Longrightarrow> xa \<le> 0 = 1"
    proof -
      assume H: "\<not> ya \<noteq> 0"
      have ya_nz: "ya = 0" by (rule dNegE, fold neq_def, rule H)
      show "xa \<le> ya = 1 \<Longrightarrow> xa \<le> 0 = 1"
        apply (rule eqSubst[where a="ya" and b="0"])
        apply (rule ya_nz)
        apply (rule eqSubst[where a="1" and b="S ya"])
        apply (rule sucCong)
        apply (rule eqSym)
        apply (rule ya_nz)
        apply (simp)
        done
    qed
  show "\<not> xa = 0 \<Longrightarrow> \<not> xa \<le> 0 = 1"
    apply (rule eqSubst[where a="0" and b="xa \<le> 0"])
    apply (rule eqSym)
    apply (unfold_def leq_def)
    apply (simp)
    done
qed

lemma leq_0_if_nz [auto]:
  shows "\<not> x = 0 \<Longrightarrow> x \<le> 0 = 0"
by (unfold_def leq_def, simp)

lemma leq_suc_eq:
  shows "x N \<Longrightarrow> y N \<Longrightarrow> x \<le> y = S x \<le> S y"
by (unfold_def leq_def, simp)

lemma suc_pred_inv [simp, auto]:
  shows "x N \<Longrightarrow> \<not> x = 0 \<Longrightarrow> S P x = x"
proof -
  have "x N \<Longrightarrow> \<not> x = 0 \<Longrightarrow> \<exists>u. x = S(u)" by (simp)
  then show "x N \<Longrightarrow> \<not> x = 0 \<Longrightarrow> S P x = x"
    proof (rule existsE)
      fix a
      show "a N \<Longrightarrow> x = S a \<Longrightarrow> S P x = x"
        by (simp)
    qed
qed

lemma cases_nat_2:
  shows "x N \<Longrightarrow> (x = 0 \<Longrightarrow> Q 0) \<Longrightarrow> (\<And>y. y N \<Longrightarrow> x = S(y) \<Longrightarrow> Q S(y)) \<Longrightarrow> Q x"
apply (rule disjE1[where P="x = 0" and Q="\<not> x = 0"])
apply (fold bJudg_def, simp)
apply (subst "0 = x", assumption)
apply (rule existsE[where Q="\<lambda>c. x = S(c)"])
apply (rule num_nonzero)
proof -
  fix a
  show "(\<And>y. y N \<Longrightarrow> x = S y \<Longrightarrow> Q (S y)) \<Longrightarrow> a N \<Longrightarrow> x = S a \<Longrightarrow> Q x"
   by (subst "S a = x", assumption)
qed

lemma cases_nat:
  assumes x_z: "x = 0 \<Longrightarrow> Q 0"
  assumes x_nz: "\<not> x = 0 \<Longrightarrow> Q x"
  shows "x N \<Longrightarrow> Q x"
apply (rule disjE1[where P="x = 0" and Q="\<not> x = 0"])
apply (fold bJudg_def)
apply (simp+)
apply (rule x_z, simp)+
apply (rule x_nz, simp)+
done

lemma leq_monotone_pred [simp]:
  assumes x_nat: "x N"
  assumes y_nat: "y N"
  assumes H: "x \<le> y = 1"
  shows "P x \<le> P y = 1"
proof (rule cases_nat[where x="x"])
  show "x N" by (rule x_nat)
  show "x = 0 \<Longrightarrow> P 0 \<le> P y = 1"
    apply (rule eqSubst[where a="0" and b="P 0"])
    apply (rule eqSym)
    apply (auto)
    apply (rule y_nat)
    done
  show "\<not> x = 0 \<Longrightarrow> P x \<le> P y = 1"
  proof (rule cases_nat[where x="y"])
    show "y N" by (rule y_nat)
    show "\<not> x = 0 \<Longrightarrow> y = 0 \<Longrightarrow> P x \<le> P 0 = 1"
      apply (rule exF[where P="x \<le> y = 1"])
      apply (rule H)
      apply (rule eqSubst[where a="0" and b="x \<le> y"])
      apply (rule eqSym)
      apply (simp+)
      done
    show "\<not> x = 0 \<Longrightarrow> \<not> y = 0 \<Longrightarrow> P x \<le> P y = 1"
    proof -
      assume x_nz: "\<not> x = 0"
      assume y_nz: "\<not> y = 0"
      have H1: "P x \<le> P y = S P x \<le> S P y"
        apply (rule leq_suc_eq)
        apply (simp)
        apply (rule x_nat)
        apply (simp)
        apply (rule y_nat)
        done
      have H2: "x N \<Longrightarrow> y N \<Longrightarrow> P x \<le> P y = x \<le> y"
        apply (subst "S P x = x", simp)
        apply (rule x_nz)
        apply (subst "S P y = y", simp)
        apply (rule y_nz)
        apply (subst "P x = P S P x", simp)
        apply (rule H1)
        done
      show ?thesis
        apply (subst "x \<le> y = 1")
        apply (rule H)
        apply (rule H2)
        apply (rule x_nat)
        apply (rule y_nat)
        done
    qed
  qed
qed

lemma [auto]: "x N \<Longrightarrow> y N \<Longrightarrow> S x \<le> S y = x \<le> y"
apply (rule eqSym)
apply (unfold_def leq_def)
apply (rule eqSym, simp)
done

lemma suc_leq_mono: "x N \<Longrightarrow> y N \<Longrightarrow> S x \<le> S y = 1 \<Longrightarrow> x \<le> y = 1"
apply (rule eqSubst[where b="x \<le> y" and a="S x \<le> S y"])
apply (auto)
done

lemma [auto]:
  assumes p_bool: "p B"
  assumes q_bool: "q B"
  shows "p \<or> q B"
apply (unfold bJudg_def)
apply (rule cases_bool[where q="p"])
apply (rule p_bool)
apply (rule disjI1)
apply (rule disjI1)
apply (assumption)
apply (rule cases_bool[where q="q"])
apply (rule q_bool)
apply (rule disjI1)
apply (rule disjI2)
apply (assumption)
apply (rule disjI2)
apply (auto)
done

lemma [auto]: "p B \<Longrightarrow> q B \<Longrightarrow> (p \<longrightarrow> q) B"
unfolding impl_def by simp

lemma leq_trans:
  assumes x_nat: "x N"
  assumes y_nat: "y N"
  assumes z_nat: "z N"
  assumes x_leq_y: "x \<le> y = 1"
  assumes y_leq_z: "y \<le> z = 1"
  shows "x \<le> z = 1"
proof -
  have quantized: "\<forall>x y. (x \<le> y = 1) \<longrightarrow> (y \<le> z = 1) \<longrightarrow> (x \<le> z = 1)"
  proof (rule ind[where a="z"])
  show "z N" by (rule z_nat)
  show "\<forall>x y. x \<le> y = 1 \<longrightarrow>
    y \<le> 0 = 1 \<longrightarrow> x \<le> 0 = 1"
    apply (rule forallI)+
    proof (rule implI, simp)+
      fix xa ya
      assume xa_nat: "xa N"
      assume ya_nat: "ya N"
      assume H: "ya \<le> 0 = 1"
      assume H1: "xa \<le> ya = 1"
      have ya_zero: "ya = 0" by (rule leq_0, rule ya_nat, rule H)
      show "xa \<le> 0 = 1"
        apply (rule eqSubst[where a="ya" and b="0"])
        apply (rule eqSubst[where a="1" and b="S(ya)"])
        apply (rule sucCong)
        apply (rule eqSym)
        apply (rule ya_zero)+
        apply (rule eqSubst[where a="1" and b="S(ya)"])
        apply (simp add: ya_zero)
        apply (rule H1)
        done
    qed
  show "\<And>x. x N \<Longrightarrow> (\<forall>xa y. xa \<le> y = 1 \<longrightarrow> y \<le> x = 1 \<longrightarrow> xa \<le> x = 1) \<Longrightarrow>
     (\<forall>xa y. xa \<le> y = 1 \<longrightarrow> y \<le> S x = 1 \<longrightarrow> xa \<le> S x = 1)"
    proof -
      fix x
      show "x N \<Longrightarrow> \<forall>xa y. xa \<le> y = 1 \<longrightarrow> y \<le> x = 1 \<longrightarrow> xa \<le> x = 1 \<Longrightarrow>
            \<forall>xa y. xa \<le> y = 1 \<longrightarrow> y \<le> S x = 1 \<longrightarrow> xa \<le> S x = 1"
        proof -
          assume hyp: "\<forall>xa y. xa \<le> y = 1 \<longrightarrow> y \<le> x = 1 \<longrightarrow> xa \<le> x = 1"
          show "x N \<Longrightarrow> \<forall>xa y. xa \<le> y = 1 \<longrightarrow> y \<le> S x = 1 \<longrightarrow> xa \<le> S x = 1"
            apply (rule forallI)+
            proof (rule implI, simp)+
              fix xa ya
              assume xa_leq_ya: "xa \<le> ya = 1"
              assume ya_leq_sx: "ya \<le> S x = 1"
              show "x N \<Longrightarrow> xa N \<Longrightarrow> ya N \<Longrightarrow> xa \<le> S x = 1"
                apply (unfold_def leq_def)
                apply (rule condI3Eq)
                apply (simp+)
                apply (rule implE[where a="(P ya) \<le> x = 1"])
                apply (rule implE[where a="(P xa) \<le> (P ya) = 1"])
                apply (rule forallE[where Q="\<lambda>a. (P xa) \<le> a = 1 \<longrightarrow> a \<le> x = 1 \<longrightarrow> (P xa) \<le> x = 1"])
                apply (rule forallE[where Q="\<lambda>a. (\<forall>c'. a \<le> c' = 1 \<longrightarrow> c' \<le> x = 1 \<longrightarrow> a \<le> x = 1)"])
                apply (rule hyp, simp)
                apply (rule leq_monotone_pred, simp)
                apply (rule xa_leq_ya)
                apply (rule suc_leq_mono)
                apply (simp)
                apply (rule eqSubst[where a="ya" and b="S P ya"])
                apply (rule eqSym)
                apply (rule suc_pred_inv, simp)
                apply (fold neq_def)
                apply (rule leq_nz_monotone[where xa="xa"])
                apply (simp+)
                apply (rule xa_leq_ya)
                apply (rule ya_leq_sx)
                done
           qed
        qed
     qed
  qed
  then have "\<forall>y. (x \<le> y = 1) \<longrightarrow> (y \<le> z = 1) \<longrightarrow> (x \<le> z = 1)"
    apply (rule forallE)
    apply (rule x_nat)
    done
  then have "(x \<le> y = 1) \<longrightarrow> (y \<le> z = 1) \<longrightarrow> (x \<le> z = 1)"
    apply (rule forallE)
    apply (rule y_nat)
    done
  then have "(y \<le> z = 1) \<longrightarrow> (x \<le> z = 1)"
    apply (rule implE)
    apply (rule x_leq_y)
    done
  then show ?thesis
    apply (rule implE)
    apply (rule y_leq_z)
    done
qed

lemma zero_less_true [simp, auto]: "a N \<Longrightarrow> 0 < S(a) = 1"
by (unfold_def less_def, simp)

lemma sub_0 [simp, auto]: "x N \<Longrightarrow> x - 0 = x"
by (unfold_def sub_def, simp)

lemma zero_div [simp, auto]: "x N \<Longrightarrow> div 0 S(x) = 0"
by (unfold_def div_def, simp)

lemma div_1 [simp, auto]:
  assumes x_nat: "x N"
  shows "x N \<Longrightarrow> div x 1 = x"
proof (rule ind, simp)
  fix xa
  assume ind_h: "div xa 1 = xa"
  show "xa N \<Longrightarrow> div S(xa) 1 = S(xa)"
    apply (unfold_def div_def)
    apply (rule eqSubst[where a="xa" and b="div ((S(xa))-1) 1"])
    apply (rule eqSubst[where a="xa" and b="(S(xa))-1"])
    apply (unfold_def sub_def)
    apply (simp+)
    apply (rule eqSym)
    apply (rule ind_h)
    apply (rule condI2)
    apply (rule eqSubst[where a="0" and b="S xa < 1"])
    apply (rule eqSym)
    apply (unfold_def less_def)
    apply (simp+)
    done
qed

lemma neq_monotone_suc:
  shows "x N \<Longrightarrow> y N \<Longrightarrow> \<not> x = y \<Longrightarrow> \<not> S x = S y"
apply (rule grounded_contradiction[where q="x = y"])
apply (simp)
apply (rule sucInj)
apply (rule dNegE)
apply (simp)
done

lemma neq_monotone_pred:
  assumes x_nat: "x N"
  assumes y_nat: "y N"
  assumes x_nz: "\<not> x = 0"
  assumes y_nz: "\<not> y = 0"
  assumes x_neq_y: "\<not> x = y"
  shows "\<not> P x = P y"
proof (rule GD.grounded_contradiction[where q="x = y"])
  show "\<not> P x = P y B" by (auto, rule x_nat, rule y_nat)
  show "\<not>\<not> P x = P y \<Longrightarrow> x = y"
    proof -
      assume H: "\<not> \<not> P x = P y"
      then have H2: "P x = P y"
        by (rule dNegE)
      then have H3: "S P x = S P y"
        by (rule sucCong)
      show ?thesis
        apply (rule eqSubst[where a="S P x" and b="x"])
        apply (rule suc_pred_inv)
        apply (rule x_nat)
        apply (rule x_nz)
        apply (rule eqSubst[where a="S P y" and b="y"])
        apply (rule suc_pred_inv)
        apply (rule y_nat)
        apply (rule y_nz)
        apply (rule H3)
        done
    qed
  show "\<not>\<not> P x = P y \<Longrightarrow> \<not> x = y" by (rule x_neq_y)
qed

lemma less_is_leq_neq:
  assumes x_nat: "x N"
  assumes y_nat: "y N"
  assumes x_leq_y: "x \<le> y = 1"
  assumes x_neq_y: "\<not> x = y"
  shows "x N \<Longrightarrow> y N \<Longrightarrow> x < y = 1"
proof -
  have "\<forall>x. x \<le> y = 1 \<longrightarrow> \<not> x = y \<longrightarrow> x < y = 1"
  proof (rule ind[where a="y"])
    show "y N" by (rule y_nat)
    show "\<forall>x. x \<le> 0 = 1 \<longrightarrow> \<not> x = 0 \<longrightarrow> x < 0 = 1"
      apply (rule forallI)+
      proof (rule implI, simp)+
        fix x
        assume x_nat: "x N"
        assume x_leq_0: "x \<le> 0 = 1"
        assume x_nz: "\<not> x = 0"
        show "x N \<Longrightarrow> x \<le> 0 = 1 \<Longrightarrow> \<not>x = 0 \<Longrightarrow> x < 0 = 1"
          apply (rule exF[where P="x = 0"])
          apply (rule leq_0)
          apply (simp)
          done
      qed
    show "\<And>x. x N \<Longrightarrow> (\<forall>xa. xa \<le> x = 1 \<longrightarrow> \<not> xa = x \<longrightarrow> xa < x = 1) \<Longrightarrow>
     (\<forall>xa. xa \<le> S x = 1 \<longrightarrow> \<not> xa = S x \<longrightarrow> xa < S x = 1)"
      apply (rule forallI)+
      proof (rule implI, simp)+
        fix x xa
        assume hyp: "\<forall>xa. xa \<le> x = 1 \<longrightarrow> \<not> xa = x \<longrightarrow> xa < x = 1"
        assume xa_leq_sx: "xa \<le> S x = 1"
        assume xa_neq_sx: "\<not> xa = S x"
        have H: "x N \<Longrightarrow> xa N \<Longrightarrow> P xa \<le> P S x = 1"
          by (rule leq_monotone_pred, simp, rule xa_leq_sx)
        have p_xa_leq_x: "xa N \<Longrightarrow> x N \<Longrightarrow> P xa \<le> x = 1"
          by (rule eqSubst[where a="P S x" and b="x"], simp, rule H)
        show "x N \<Longrightarrow> xa N \<Longrightarrow> xa < S x = 1 "
          apply (unfold_def less_def)
          apply (rule condI2Eq)
          apply (fold neq_def)
          apply (simp)
          apply (rule cases_nat[where x="xa"], simp+)
          proof -
            show "xa N \<Longrightarrow> xa N" by assumption
            assume xa_nz: "\<not> xa = 0"
            have H2: "xa N \<Longrightarrow> x N \<Longrightarrow> \<not> P xa = P S x"
              apply (rule neq_monotone_pred, simp)
              apply (rule xa_nz, simp)
              apply (rule xa_neq_sx)
              done
            have pxa_neq_x: "x N \<Longrightarrow> xa N \<Longrightarrow> \<not> P xa = x"
              apply (rule eqSubst[where a="P S x" and b="x"])
              apply (simp)
              apply (rule H2, simp)
              done
            have "xa N \<Longrightarrow> P xa \<le> x = 1 \<longrightarrow> \<not> P xa = x \<longrightarrow> P xa < x = 1"
              apply (rule forallE[where a="P xa"])
              apply (rule hyp)
              apply (rule natP, simp)
              done
            then have "x N \<Longrightarrow> xa N \<Longrightarrow> \<not> P xa = x \<longrightarrow> P xa < x = 1"
              apply (rule implE, simp)
              apply (rule p_xa_leq_x, simp)
              done
            then show "x N \<Longrightarrow> xa N \<Longrightarrow> P xa < x = 1"
              apply (rule implE, simp)
              apply (rule pxa_neq_x, simp)
              done
        qed
      qed
  qed
  then have "x \<le> y = 1 \<longrightarrow> \<not> x = y \<longrightarrow> x < y = 1"
    apply (rule forallE)
    apply (rule x_nat)
    done
  then have "\<not> x = y \<longrightarrow> x < y = 1"
    apply (rule implE)
    apply (rule x_leq_y)
    done
  then show "x < y = 1"
    apply (rule implE)
    apply (rule x_neq_y)
    done
qed

lemma x_less_1_is_0:
  assumes x_nat: "x N"
  assumes H: "x < 1 = 1"
  shows "x = 0"
proof (rule grounded_contradiction[where q="x < 1 = 0"])
  show "x = 0 B"
    by (rule eqBool, rule x_nat, auto)
  show "\<not> x = 0 \<Longrightarrow> x < 1 = 0"
    apply (unfold_def less_def)
    apply (rule condI2Eq)
    apply (fold neq_def)
    apply (auto)
    apply (rule condI2Eq)
    apply (unfold neq_def)
    apply (auto)
    apply (rule eqSubst[where a="0" and b="P S 0"])
    apply (rule eqSym)
    apply (auto)
    done
  show "\<not> x = 0 \<Longrightarrow> \<not> x < 1 = 0"
      apply (rule eqSubst[where a="1" and b="x < 1"])
      apply (rule eqSym)
      apply (rule H)
      apply (fold neq_def)
      apply (auto)
      done
qed

lemma le_monotone_suc [simp]:
  shows "x < y = 1 \<Longrightarrow> x N \<Longrightarrow> y N \<Longrightarrow> S x < S y = 1"
by (unfold_def less_def, simp)

lemma [simp]:
  shows "x < y = 0 \<Longrightarrow> x N \<Longrightarrow> y N \<Longrightarrow> S x < S y = 0"
by (unfold_def less_def, simp)

lemma le_monotone_pred:
  assumes x_nat: "x N"
  assumes x_nz: "\<not> x = 0"
  assumes y_nat: "y N"
  assumes x_le_y: "x < y = 1"
  shows "x N \<Longrightarrow> y N \<Longrightarrow> \<not> x = 0 \<Longrightarrow> x < y = 1 \<Longrightarrow> P x < P y = 1"
apply (rule grounded_contradiction[where q="x < y = 1"])
apply (simp)
apply (unfold_def less_def)
apply (rule cases_nat[where x="y"])
apply (rule eqSubst[where a="0" and b="(if 0 = 0 then 0 else
  if x = 0 then 1 else (P x < P 0))"])
apply (simp+)
done

lemma le_suc_implies_leq:
  assumes x_le_sy: "x < S y = 1"
  shows "x N \<Longrightarrow> y N \<Longrightarrow> x \<le> y = 1"
proof -
  have "x N \<Longrightarrow> y N \<Longrightarrow> \<forall>x. x < S y = 1 \<longrightarrow> x \<le> y = 1"
  proof (rule ind[where a="y"], auto)
    show "x N \<Longrightarrow> y N \<Longrightarrow> \<forall>x. x < 1 = 1 \<longrightarrow> x \<le> 0 = 1"
      apply (rule forallI)+
      proof (rule implI, simp)+
        fix x
        assume x_le_sy: "x < 1 = 1"
        show "x N \<Longrightarrow> x \<le> 0 = 1"
          apply (unfold_def leq_def)
          apply (rule condI1)
          apply (rule x_less_1_is_0)
          apply (auto)
          apply (rule x_le_sy)
          apply (auto)
          done
      qed
    show "\<And>x. x N \<Longrightarrow> (\<forall>xa. xa < S x = 1 \<longrightarrow> xa \<le> x = 1) \<Longrightarrow>
     (\<forall>xa. xa < S S x = 1 \<longrightarrow> xa \<le> S x = 1)"
      apply (rule forallI)+
      proof (rule implI, simp)+
        fix x xa
        assume x_nat: "x N"
        assume xa_nat: "xa N"
        assume hyp: "\<forall>xa. xa < S x = 1 \<longrightarrow> xa \<le> x = 1"
        have hyp_inst: "P xa < S x = 1 \<longrightarrow> P xa \<le> x = 1"
          apply (rule forallE[where a="P xa"])
          apply (rule hyp)
          apply (auto)
          apply (rule xa_nat)
          done
        assume xa_le_ssx: "xa < S S x = 1"
        show "x N \<Longrightarrow> xa N \<Longrightarrow> xa \<le> S x = 1"
          apply (unfold_def leq_def)
          apply (rule cases_nat[where x="xa"])
          apply (rule condI1)
          apply (simp+)
          apply (rule implE[where a="P xa < S x = 1"])
          apply (rule hyp_inst)
          apply (rule eqSubst[where a="P S S x" and b = "S x"])
          apply (simp)
          apply (rule le_monotone_pred)
          apply (rule xa_nat)
          apply (simp add: xa_le_ssx)+
          done
      qed
  qed
  then have "x N \<Longrightarrow> y N \<Longrightarrow> x < S y = 1 \<longrightarrow> x \<le> y = 1"
    by (rule forallE, simp)
  then show "x N \<Longrightarrow> y N \<Longrightarrow> x \<le> y = 1"
    apply (rule implE, simp)
    apply (rule x_le_sy)
    done
qed

lemma leq_suc_not_leq_implies_eq:
  assumes x_nat: "x N"
  assumes y_nat: "y N"
  assumes x_ge_y: "\<not> x \<le> y = 1"
  assumes x_le_sy: "x \<le> S y = 1"
  shows "x = S y"
proof (rule contradiction)
  show "x = S(y) B" by (rule eqBool, rule x_nat, rule natS, rule y_nat)
  show "\<not> x = S(y) \<Longrightarrow> False"
    proof -
      assume x_neq_sy: "\<not> x = S y"
      have H: "x < S y = 1"
        apply (rule less_is_leq_neq)
        apply (rule x_nat)
        apply (rule natS)
        apply (rule y_nat)
        apply (rule x_le_sy)
        apply (rule x_neq_sy)
        apply (rule x_nat)
        apply (simp, rule y_nat)
        done
      have H4: "x \<le> y = 1"
        apply (rule le_suc_implies_leq)
        apply (rule H)
        apply (rule x_nat, rule y_nat)
        done
      show "False"
        apply (rule exF[where P="x \<le> y = 1"])
        apply (rule H4)
        apply (rule x_ge_y)
        done
    qed
qed

lemma strong_induction [consumes 1, case_names HQ Base Step]:
  shows "a N \<Longrightarrow> Q 0 \<Longrightarrow> (\<And>x. x N \<Longrightarrow> (\<And>y. y N \<Longrightarrow> y\<le>x = 1 \<Longrightarrow> Q y) \<Longrightarrow> (Q S(x))) \<Longrightarrow> Q a"
proof -
  have q: "a N \<Longrightarrow> Q 0 \<Longrightarrow> (\<And>x. x N \<Longrightarrow> (\<And>y. y N \<Longrightarrow> y\<le>x = 1 \<Longrightarrow> Q y) \<Longrightarrow> (Q S(x))) \<Longrightarrow>
           \<forall>x. (x \<le> a = 1) \<longrightarrow> Q x"
    apply (rule ind[where a="a"], assumption)
    apply (rule forallI implI)+
    apply (rule eqBool, rule leq_terminates, assumption)
    apply (rule nat0, rule natS, rule nat0)
    proof -
      fix x
      show "x N \<Longrightarrow> x \<le> 0 = 1 \<Longrightarrow> Q 0 \<Longrightarrow> Q x"
        apply (rule eqSubst[where a="0" and b="x"], rule eqSym)
        apply (rule leq_0, assumption+)
        done
      show "a N \<Longrightarrow> x N \<Longrightarrow>
            Q 0 \<Longrightarrow>
            (\<And>x. x N \<Longrightarrow> (\<And>y. y N \<Longrightarrow> y \<le> x = 1 \<Longrightarrow> Q y) \<Longrightarrow> Q (S x)) \<Longrightarrow>
            \<forall>xa. xa \<le> x = 1 \<longrightarrow> Q xa \<Longrightarrow>
            \<forall>xa. xa \<le> (S x) = 1 \<longrightarrow> Q xa"
        apply (rule forallI implI)+
        apply (rule eqBool, rule leq_terminates, assumption)
        apply (rule natS, assumption)
        apply (rule natS, rule nat0)
        proof -
          fix xa
          assume xa_nat: "xa N"
          assume hyp: "\<forall>x'. x' \<le> x = 1 \<longrightarrow> Q x'"
          assume step: "(\<And>x. x N \<Longrightarrow> (\<And>y. y N \<Longrightarrow> y \<le> x = 1 \<Longrightarrow> Q y) \<Longrightarrow> Q (S x))"
          assume xa_leq_sx: "xa \<le> S x = 1"
          have H: "xa \<le> x = 1 \<longrightarrow> Q xa"
            by (rule forallE[where a="xa"], rule hyp, rule xa_nat)
          show "x N \<Longrightarrow> Q xa"
            apply (rule disjE1[where P="xa \<le> x = 1" and Q="\<not> xa \<le> x = 1"])
            apply (fold GD.bJudg_def)
            apply (rule eqBool)
            apply (rule leq_terminates)
            apply (rule xa_nat, assumption)
            apply (rule natS, rule nat0)
            apply (rule implE[where a="xa \<le> x = 1"])
            apply (rule H)
            apply (assumption)
            proof -
              assume xa_not_leq_x: "\<not> xa \<le> x = 1"
              have xa_eq_sx: "x N \<Longrightarrow> xa = S x"
                apply (rule leq_suc_not_leq_implies_eq)
                apply (rule xa_nat, assumption)
                apply (rule xa_not_leq_x)
                apply (rule xa_leq_sx)
                done
              have q_sx: "x N \<Longrightarrow> Q S(x)"
                apply (rule step)
                apply (assumption)
                apply (rule implE)
                apply (rule forallE)
                apply (rule hyp, assumption+)
                done
              show "x N \<Longrightarrow> Q xa"
                apply (rule eqSubst[where a="S x" and b="xa"])
                apply (rule eqSym)
                apply (rule xa_eq_sx, assumption)
                apply (rule q_sx, assumption)
                done
            qed
        qed
    qed
    assume step: "(\<And>x. x N \<Longrightarrow> (\<And>y. y N \<Longrightarrow> y\<le>x = 1 \<Longrightarrow> Q y) \<Longrightarrow> (Q S(x)))"
    show "a N \<Longrightarrow> Q 0 \<Longrightarrow> Q a"
      apply (rule implE[where a="a \<le> a = 1"])
      apply (rule forallE[where Q="\<lambda>x. (x \<le> a = 1) \<longrightarrow> Q x"])
      apply (rule q)
      apply (assumption+)
      apply (rule step)
      apply (assumption+)
      apply (rule leq_refl)
      apply (assumption)
      done
qed

lemma sub_terminates [auto]:
  assumes x_nat: "x N"
  assumes y_nat: "y N"
  shows "x - y N"
proof (rule ind[where a=y])
  show habeas_quid_cond: "y N" by (rule y_nat)
  show base_case: "x - 0 N"
    apply (unfold_def sub_def)
    apply (rule eqSubst[where a="x"])
    apply (rule eqSym)
    apply (rule condI1)
    apply (rule zeroRefl)
    apply (rule x_nat)
    apply (rule x_nat)
    done
  show ind_step: "\<And>a. a N \<Longrightarrow> ((x - a) N) \<Longrightarrow> ((x - S(a)) N)"
    proof (unfold_def sub_def)
      fix a
      assume HQ: "a N" and BC: "x - a N"
      show "if (S(a) = 0) then x else P(x - P(S(a))) N"
        proof (rule GD.condT)
          show "S(a) = 0 B"
            apply (rule GD.eqBool)
            apply (rule GD.natS)
            apply (rule HQ)
            apply (rule GD.nat0)
            done
          show "x N" by (rule x_nat)
          show "P(x - P(S(a))) N"
            apply (rule natP)
            apply (rule eqSubst[where a="x-a"])
            apply (rule eqSubst[where a="a" and b="P(S(a))"])
            apply (rule eqSym)
            apply (rule predSucInv)
            apply (rule HQ)
            apply (fold isNat_def)
            apply (rule BC)+
            done
        qed
    qed
qed

lemma sub_nz_leq_pred [simp]:
  assumes x_nat: "x N"
  assumes y_nat: "y N"
  shows "(S x) - (S y) \<le> x = 1"
proof -
  have "\<forall>x. (S x) - (S y) \<le> x = 1"
  proof (rule ind[where a="y"])
    show "y N" by (rule y_nat)
    show "\<forall>x. S x - 1 \<le> x = 1"
      proof (rule forallI)
        fix x
        assume x_nat: "x N"
        show "S x - 1 \<le> x = 1"
          apply (rule eqSubst[where a="x" and b="S x - 1"])
          apply (rule eqSym)
          apply (unfold_def sub_def)
          apply (rule condI2Eq)
          apply (fold neq_def)
          apply (auto)
          apply (rule x_nat)
          apply (rule eqSubst[where a="0" and b="P S 0"])
          apply (rule eqSym)
          apply (auto)
          apply (rule eqSubst[where a="S x" and b="S x - 0"])
          apply (rule eqSym)
          apply (auto)
          apply (rule x_nat)
          apply (auto)
          apply (rule x_nat)
          apply (auto)
          apply (rule x_nat)
          done
      qed
    show "\<And>x. x N \<Longrightarrow> (\<forall>xa. S xa - S x \<le> xa = 1) \<Longrightarrow> (\<forall>xa. S xa - S S x \<le> xa = 1)"
      proof (rule forallI)+
        fix x xa
        assume x_nat: "x N" and xa_nat: "xa N"
        assume hyp: "\<forall>xa. S xa - S x \<le> xa = 1"
        then have H: "S xa - S x \<le> xa = 1"
          apply (rule forallE)
          apply (rule xa_nat)
          done
        have H2: "P(S xa - S x) \<le> xa = 1"
          apply (rule leq_trans[where y="S xa - S x"])
          apply (auto)
          apply (rule xa_nat)
          apply (rule x_nat)
          apply (auto)
          apply (rule xa_nat)
          apply (rule x_nat)
          apply (rule xa_nat)
          apply (auto)
          apply (rule xa_nat)
          apply (rule x_nat)
          apply (rule H)
          done
        show "S xa - S S x \<le> xa = 1"
          apply (unfold_def sub_def)
          apply (rule eqSubst[where a="P(S xa - S x)" and b="(if S S x = zero then S xa else P(S xa - P S S x))"])
          apply (rule eqSym)
          apply (rule condI2Eq)
          apply (fold neq_def)
          apply (auto)
          apply (rule x_nat)
          apply (auto)
          apply (rule xa_nat)
          apply (rule x_nat)
          apply (rule eqSubst[where a="S x" and b="P S S x"])
          apply (rule eqSym)
          apply (auto)
          apply (rule x_nat)
          apply (fold isNat_def)
          apply (auto)
          apply (rule xa_nat)
          apply (rule x_nat)
          apply (rule H2)
          done
      qed
  qed
  then show ?thesis
    apply (rule forallE)
    apply (rule x_nat)
    done
qed

lemma div_terminates [auto]:
  shows "x N \<Longrightarrow> y N \<Longrightarrow> div x S(y) N"
apply (rule strong_induction[where a="x"], assumption)
apply (unfold_def div_def, simp)
proof -
  fix x
  assume hyp: "\<And>ya. ya N \<Longrightarrow> ya \<le> x = 1 \<Longrightarrow> (div ya (S y) N)"
  show "x N \<Longrightarrow> y N \<Longrightarrow> div (S x) (S y) N"
    apply (unfold_def div_def)
    apply (rule condT, simp)
    apply (rule hyp, simp+)
    done
qed

axiomatization cpair :: "num \<Rightarrow> num \<Rightarrow> num" where
  cpair_def: "cpair x y := if y = 0 then div (x * S(x)) 2
                           else cpair x P(y) + x + y + 2"

nonterminal cpair_args

syntax
  "_cpair"      :: "num \<Rightarrow> cpair_args \<Rightarrow> num"        ("\<langle>_,_\<rangle>")
  "_cpair_arg"  :: "num \<Rightarrow> cpair_args"               ("_")
  "_cpair_args" :: "num \<Rightarrow> cpair_args \<Rightarrow> cpair_args" ("_,_")
translations
  "\<langle>x, y\<rangle>" == "CONST cpair x y"
  "_cpair x (_cpair_args y z)" == "_cpair x (_cpair_arg (_cpair y z))"

ML_file "gd_induct.ML"
ML_file "gd_cases.ML"

lemma [simp]: "x N \<Longrightarrow> \<langle>x, 0\<rangle> = div (x * S(x)) 2"
  by (unfold_def cpair_def, simp)

lemma cpair_terminates [auto]: "x N \<Longrightarrow> y N \<Longrightarrow> \<langle>x, y\<rangle> N"
apply (induct y, simp)
apply (unfold_def cpair_def, simp)+
done

lemma cpair_suc [auto]: "x N \<Longrightarrow> y N \<Longrightarrow> \<langle>x, S(y)\<rangle> = \<langle>x, y\<rangle> + x + S(y) + 2"
apply (rule eqSym)
apply (unfold_def cpair_def)
apply (rule eqSym)
apply (simp)
done

axiomatization
  cpx :: "num \<Rightarrow> num" and
  cpy :: "num \<Rightarrow> num"
where
  cpx_def: "cpx x := if x = 0 then 0
                     else if cpx (P x) = 0 then S(cpy P(x))
                     else P(cpx (P x))" and
  cpy_def: "cpy x := if cpx (P x) = 0 then 0
                     else S(cpy (P x))"

lemma [simp]: "cpx 0 = 0"
by (unfold_def cpx_def, simp)

lemma [simp]: "cpy 0 = 0"
by (unfold_def cpy_def, simp)

lemma cpx_cpy_terminate: "x N \<Longrightarrow> (cpx x N) \<and> (cpy x N)"
apply (induct x, simp)
apply (unfold_def cpx_def, simp)
apply (subst rule: condI2)
apply (rule condT, simp)
apply (rule conjE1, simp)
apply (rule conjE2, simp)
apply (rule conjE1, simp)
apply (rule condT, simp)
apply (rule conjE1, simp)
apply (rule conjE2, simp)
apply (rule conjE1, simp)
apply (unfold_def cpy_def, simp)
apply (rule condT, simp)
apply (rule conjE1, simp)
apply (rule conjE2, simp)
done

lemma cpx_terminates [auto]: "x N \<Longrightarrow> cpx x N"
by (rule conjE1, rule cpx_cpy_terminate, assumption)

lemma cpy_terminates [auto]: "x N \<Longrightarrow> cpy x N"
by (rule conjE2, rule cpx_cpy_terminate, assumption)

lemma cpx_suc: "x N \<Longrightarrow> cpx (S x) = (if cpx x = 0 then S(cpy x)
                           else P(cpx x))"
apply (rule eqSym)
apply (unfold_def cpx_def)
apply (rule eqSym)
apply (simp)
apply (rule condI2Eq, simp)
apply (rule condT, simp)+
done

lemma cpy_suc: "x N \<Longrightarrow> cpy (S x) = (if cpx x = 0 then 0
                           else S(cpy x))"
apply (rule eqSym)
apply (unfold_def cpy_def)
apply (rule eqSym)
apply (simp)
apply (rule condT, simp)+
done

lemma "cpx \<langle>0,0\<rangle> = 0"
by simp

lemma "cpy \<langle>0,0\<rangle> = 0"
by simp

lemma cpx_proj [simp]: "a N \<Longrightarrow> b N \<Longrightarrow> cpx \<langle>a, b\<rangle> = a"
sorry

lemma cpy_proj [simp]: "a N \<Longrightarrow> b N \<Longrightarrow> cpy \<langle>a, b\<rangle> = b"
sorry

lemma cpair_inj:
  assumes eq: "\<langle>a, b\<rangle> = \<langle>c, d\<rangle>"
  shows "a N \<Longrightarrow> b N \<Longrightarrow> c N \<Longrightarrow> d N \<Longrightarrow> a = c \<and> b = d"
proof -
  have H: "a N \<Longrightarrow> b N \<Longrightarrow> cpx \<langle>a, b\<rangle> = cpx \<langle>c, d\<rangle>"
    by (rule eqSubst[OF eq], simp)
  have a_eq_c: "a N \<Longrightarrow> b N \<Longrightarrow> c N \<Longrightarrow> d N \<Longrightarrow> a = c"
    apply (rule eqSubst[where a="cpx \<langle>a, b\<rangle>" and b="a"], simp)
    apply (rule eqSubst[where a="cpx \<langle>c, d\<rangle>" and b="c"], simp)
    apply (rule H, simp)
    done
  have H2: "a N \<Longrightarrow> b N \<Longrightarrow> cpy \<langle>a, b\<rangle> = cpy \<langle>c, d\<rangle>"
    by (rule eqSubst[OF eq], simp)
  have b_eq_d: "a N \<Longrightarrow> b N \<Longrightarrow> c N \<Longrightarrow> d N \<Longrightarrow> b = d"
    apply (rule eqSubst[where a="cpy \<langle>a, b\<rangle>" and b="b"])
    apply (rule cpy_proj, assumption+)
    apply (rule eqSubst[where a="cpy \<langle>c, d\<rangle>" and b="d"])
    apply (rule cpy_proj, assumption+)
    apply (rule H2, assumption+)
    done
  show "a N \<Longrightarrow> b N \<Longrightarrow> c N \<Longrightarrow> d N \<Longrightarrow> a = c \<and> b = d"
    apply (rule conjI)
    apply (rule a_eq_c)
    apply (simp)
    apply (rule b_eq_d)
    apply (simp)
    done
qed

lemma cpair_inj_l:
  assumes eq: "\<langle>a, b\<rangle> = \<langle>c, d\<rangle>"
  shows "a N \<Longrightarrow> b N \<Longrightarrow> c N \<Longrightarrow> d N \<Longrightarrow> a = c"
apply (rule conjE1[where q="b=d"])
apply (rule cpair_inj)
apply (rule eq)
apply (simp)
done

lemma cpair_inj_r:
  assumes eq: "\<langle>a, b\<rangle> = \<langle>c, d\<rangle>"
  shows "a N \<Longrightarrow> b N \<Longrightarrow> c N \<Longrightarrow> d N \<Longrightarrow> b = d"
apply (rule conjE2[where p="a=c"])
apply (rule cpair_inj)
apply (rule eq)
apply (simp)
done

lemma [auto]:
  "\<not>a \<or> \<not>b \<Longrightarrow> \<not> (a \<and> b)"
unfolding conj_def
by (rule dNegI, assumption)

lemma [auto]:
  "a N \<Longrightarrow> b N \<Longrightarrow> c N \<Longrightarrow> d N \<Longrightarrow> \<not> a = c \<or> \<not> b = d \<Longrightarrow> \<not> \<langle>a, b\<rangle> = \<langle>c, d\<rangle>"
apply (rule grounded_contradiction[where q="\<not>(a=c \<and> b=d)"], simp)
apply (rule cpair_inj_l[where b="b" and d="d"])
apply (rule dNegE, simp)
apply (rule cpair_inj_r[where a="a" and c="c"])
apply (rule dNegE, simp)
done

lemma if_leq_not_greater:
  assumes a_le_b: "a \<le> b = 1"
  shows "a > b = 0"
apply (unfold greater_def)
apply (rule eqSubst[where a="1" and b="a \<le> b"])
apply (rule eqSym)
apply (rule a_le_b)
apply (unfold_def sub_def)
apply (rule condI2Eq)
apply (fold neq_def)
apply (auto)
apply (rule eqSubst[where a="0" and b="P S 0"])
apply (rule eqSym)
apply (auto)
apply (rule eqSubst[where a="1" and b="1 - 0"])
apply (rule eqSym)
apply (auto)
done

lemma if_less_not_geq:
  assumes a_less_b: "a < b = 1"
  shows "a \<ge> b = 0"
apply (unfold geq_def)
apply (rule eqSubst[where a="1" and b="a < b"])
apply (rule eqSym)
apply (rule a_less_b)
apply (unfold_def sub_def)
apply (rule condI2Eq)
apply (fold neq_def)
apply (auto)
apply (rule eqSubst[where a="0" and b="P S 0"])
apply (rule eqSym)
apply (auto)
apply (rule eqSubst[where a="1" and b="1 - 0"])
apply (rule eqSym)
apply (auto)
done

lemma leq_monotone_add [auto, simp]:
  assumes x_nat: "x N"
  assumes y_nat: "y N"
  shows "x \<le> y + x = 1"
proof (rule ind[where a="x"])
  show "x N" by (rule x_nat)
  show "0 \<le> y + 0 = 1" by (auto, rule y_nat)
  show "\<And>x. x N \<Longrightarrow> x \<le> y + x = 1 \<Longrightarrow> S x \<le> y + S x = 1"
    proof -
      fix xa
      assume xa_nat: "xa N" and hyp: "xa \<le> y + xa = 1"
      show "S xa \<le> y + S xa = 1"
        apply (unfold_def leq_def)
        apply (rule condI2Eq)
        apply (fold neq_def)
        apply (auto)
        apply (rule xa_nat)
        apply (auto)
        apply (rule condI2Eq)
        apply (fold neq_def)
        apply (rule eqSubst[where a="S(y + xa)" and b="y + S xa"])
        apply (unfold_def add_def)
        apply (rule eqSym)
        apply (rule condI2Eq)
        apply (fold neq_def)
        apply (auto)
        apply (rule xa_nat)
        apply (auto)
        apply (rule y_nat)
        apply (rule xa_nat)
        apply (rule eqSubst[where a="xa" and b="P S xa"])
        apply (rule eqSym)
        apply (rule predSucInv)
        apply (rule xa_nat)
        apply (fold isNat_def)
        apply (auto)
        apply (rule y_nat)
        apply (rule xa_nat)
        apply (auto)
        apply (rule y_nat)
        apply (rule xa_nat)
        apply (auto)
        apply (rule eqSubst[where a="xa" and b="P S xa"])
        apply (rule eqSym)
        apply (rule predSucInv)
        apply (rule xa_nat)
        apply (rule eqSubst[where a="S (y + xa)" and b="y + S xa"])
        apply (unfold_def add_def)
        apply (rule eqSym)
        apply (rule condI2Eq)
        apply (fold neq_def)
        apply (auto)
        apply (rule xa_nat)
        apply (auto)
        apply (rule y_nat)
        apply (rule xa_nat)
        apply (rule eqSubst[where a="xa" and b="P S xa"])
        apply (rule eqSym)
        apply (rule predSucInv)
        apply (rule xa_nat)
        apply (fold isNat_def)
        apply (auto)
        apply (rule y_nat)
        apply (rule xa_nat)
        apply (rule eqSubst[where a="y + xa" and b="P S (y + xa)"])
        apply (rule eqSym)
        apply (auto)
        apply (rule y_nat)
        apply (rule xa_nat)
        apply (rule hyp)
        done
    qed
qed

lemma add_suc_comm:
  shows "x N \<Longrightarrow> y N \<Longrightarrow> y + S(x) = S(y) + x"
proof (rule ind[where a="x"], simp+)
  fix xa
  assume hyp: "y + S xa = S y + xa"
  show "x N \<Longrightarrow> y N \<Longrightarrow> xa N \<Longrightarrow> y + S S xa = S y + S xa"
    apply (rule eqSubst[where a="S(y + S(xa))" and b="y + S S xa"])
    apply (unfold_def add_def)
    apply (simp)
    apply (rule eqSubst[where a="S xa" and b="P S S xa"])
    apply (rule eqSym)
    apply (simp add: hyp)+
    apply (unfold_def add_def)
    apply (simp)
    done
qed

lemma add_comm [auto]:
  shows "x N \<Longrightarrow> y N \<Longrightarrow> x + y = y + x"
apply (rule ind[where a="y"], simp)
apply (rule eqSubst[where a="x" and b="x + 0"])
apply (rule eqSym)
apply (auto)
apply (rule eqSym)
proof (auto)
  fix xa
  assume hyp: "x + xa = xa + x"
  show "x N \<Longrightarrow> xa N \<Longrightarrow> x + S xa = S xa + x"
    apply (rule eqSym)
    apply (unfold_def add_def)
    apply (rule eqSym)
    apply (simp add: hyp)
    apply (rule eqSubst[where a="xa + S x" and b="S xa + x"])
    apply (rule add_suc_comm, simp)
    apply (unfold_def add_def)
    apply (simp)
    done
qed

lemma leq_monotone_add_r [simp]:
  "x \<le> y = 1 \<Longrightarrow> x N \<Longrightarrow> y N \<Longrightarrow> z N \<Longrightarrow> x \<le> y + z = 1"
apply (rule leq_trans[where y="y"], simp)
apply (rule eqSubst[where a="z + y" and b="y + z"], simp)
done

lemma leq_monotone_add_l [simp]:
  "x \<le> z = 1 \<Longrightarrow> x N \<Longrightarrow> y N \<Longrightarrow> z N \<Longrightarrow> x \<le> y + z = 1"
apply (rule leq_trans[where y="z"], simp)
done

lemma neq_monotone_add:
  assumes x_nat: "x N"
  assumes y_nat: "y N"
  assumes x_nz: "\<not> x = 0"
  shows "x N \<Longrightarrow> y N \<Longrightarrow> \<not> y = x + y"
proof -
  have H1: "x N \<Longrightarrow> y N \<Longrightarrow> (\<And>xa. xa N \<Longrightarrow> \<not> (y = S(xa) + y))"
    proof -
      fix xa
      show "x N \<Longrightarrow> y N \<Longrightarrow> xa N \<Longrightarrow> \<not> (y = S(xa) + y)"
        proof (rule ind[where a="y"], simp+)
          fix z
          assume hyp: "\<not> z = S xa + z"
          show "xa N \<Longrightarrow> z N \<Longrightarrow> \<not> S z = S xa + S z"
            apply (rule eqSubst[where a="S(S xa + z)" and b="S xa + S z"])
            apply (unfold_def add_def)
            apply (simp)
            apply (rule neq_monotone_suc)
            apply (simp)
            apply (rule hyp)
            done
        qed
    qed
  have "\<exists>p. x = S(p)" by (auto, rule x_nat, rule x_nz)
  then show "x N \<Longrightarrow> y N \<Longrightarrow> \<not> y = x + y"
    apply (rule existsE)
    proof -
      fix a
      assume a_pred: "x = S a"
      show "a N \<Longrightarrow> x N \<Longrightarrow> y N \<Longrightarrow> \<not> y = x + y"
        apply (rule eqSubst[where a="S a" and b="x"])
        apply (rule eqSym)
        apply (rule a_pred)
        apply (rule H1)
        apply (simp)
        done
    qed
qed

lemma swap_add:
  shows "x N \<Longrightarrow> y N \<Longrightarrow> Q(y + x) \<Longrightarrow> Q (x + y)"
  by (rule eqSubst[where a="y+x" and b="x+y"], simp)

lemma nz_monotone_leq:
  assumes x_nat: "x N"
  assumes y_nat: "y N"
  assumes H: "S(x) \<le> y = 1"
  shows "\<not> y = 0"
apply (rule grounded_contradiction[where q="S(x) = 0"])
apply (auto)
apply (rule y_nat)
apply (rule leq_0)
apply (rule natS)
apply (rule x_nat)
apply (rule eqSubst[where a="y" and b="0" and Q="\<lambda>c. S x \<le> c = 1"])
apply (rule dNegE)
apply (assumption)
apply (rule H)
apply (fold neq_def)
apply (auto)
apply (rule x_nat)
done

lemma sub_pred_suc:
  assumes H: "S(z) = x - S(y)"
  shows "x N \<Longrightarrow> y N \<Longrightarrow> z N \<Longrightarrow> x - y = S(S(z))"
proof -
  have unf: "x N \<Longrightarrow> y N \<Longrightarrow> x - S(y) = P(x - y)"
    apply (rule eqSym)
    apply (unfold_def sub_def)
    apply (simp+)
    done
  have x_neq_y: "x N \<Longrightarrow> y N \<Longrightarrow> z N \<Longrightarrow> \<not> x - y = 0"
    apply (rule nz_monotone_leq[where x="z"])
    apply (simp add: H unf)+
    done
  have H1: "x N \<Longrightarrow> y N \<Longrightarrow> P(x - y) = S(z)"
    apply (rule eqSubst[where a="x - S(y)" and b="P(x - y)"])
    apply (simp add: H unf)+
    done
  show "x N \<Longrightarrow> y N \<Longrightarrow> z N \<Longrightarrow> x - y = S(S(z))"
    apply (rule eqSubst[where b="x - y" and a="S P (x - y)"], simp)
    apply (rule x_neq_y)
    apply (simp add: H1)+
    done
qed

lemma sub_suc_pred:
  assumes H: "x - y = S(z)"
  shows "x N \<Longrightarrow> y N \<Longrightarrow> z N \<Longrightarrow> x - S(y) = z"
apply (rule implE[where a="x-y=(S z)"])
apply (induct y, simp)
apply (rule implI, simp)
apply (subst "S(z) = x")
apply (unfold_def sub_def, simp)
proof (rule implI, simp)
  fix xa
  show "x - y = S(z)" by (rule H)
  assume h: "x - S xa = S z"
  show "xa N \<Longrightarrow> x N \<Longrightarrow> z N \<Longrightarrow> x - S(S xa) = z"
    apply (unfold_def sub_def)
    apply (simp add: h)
    done
qed

lemma sub_monotone_lhs:
  assumes H: "S(x) - y = S(z)"
  shows "x N \<Longrightarrow> y N \<Longrightarrow> z N \<Longrightarrow> x - y = z"
proof -
  have "x N \<Longrightarrow> y N \<Longrightarrow> \<forall>z. S(x) - y = S(z) \<longrightarrow> x - y = z"
    apply (rule ind[where a="y"], simp)
    apply (rule forallI)
    apply (rule implI, simp)
    apply (subst "x = x - 0")
    apply (rule eqSym, simp)
    apply (rule sucInj, rule eqSym, simp)
    apply (rule forallI)+
    proof (rule implI, simp)+
      fix xa za
      assume hyp: "\<forall>z. S x - xa = S z \<longrightarrow> x - xa = z"
      assume H1: "S x - S xa = S za"
      show "x N \<Longrightarrow> y N \<Longrightarrow> xa N \<Longrightarrow> za N \<Longrightarrow> x - S xa = za"
        apply (rule sub_suc_pred)
        apply (rule implE[where a="S x - xa = S(S za)"])
        apply (rule forallE, rule hyp, simp)
        apply (rule sub_pred_suc)
        apply (simp add: H1)
        done
    qed
  then have "x N \<Longrightarrow> y N \<Longrightarrow> z N \<Longrightarrow> S(x) - y = S(z) \<longrightarrow> x - y = z"
    by (rule forallE, simp)
  then show "x N \<Longrightarrow> y N \<Longrightarrow> z N \<Longrightarrow> x - y = z"
    apply (rule implE, simp)
    apply (rule H)
    done
qed

lemma sub_eq_0_imp_leq:
  assumes H: "a - b = 0"
  shows "a N \<Longrightarrow> b N \<Longrightarrow> a \<le> b = 1"
proof -
  have "a N \<Longrightarrow> b N \<Longrightarrow> \<forall>a. a - b = 0 \<longrightarrow> a \<le> b = 1"
  proof (induct b)
    show "\<forall>a. a - 0 = 0 \<longrightarrow> a \<le> 0 = 1"
      proof (rule forallI, rule implI, simp)
        fix aa
        assume aa_nat: "aa N" and hyp: "aa - 0 = 0"
        have a_zero: "aa = 0"
          apply (rule eqSubst[where a="aa-0" and b="aa"])
          apply (auto)
          apply (rule aa_nat)
          apply (rule hyp)
          done
        show "aa \<le> 0 = 1"
          apply (rule eqSubst[where a="0" and b="aa"])
          apply (rule eqSym)
          apply (rule a_zero)
          apply (auto)
          done
      qed
    show "\<And>x. x N \<Longrightarrow> (\<forall>a. a - x = 0 \<longrightarrow> a \<le> x = 1) \<Longrightarrow>
     (\<forall>a. a - S x = 0 \<longrightarrow> a \<le> S x = 1)"
      proof (rule forallI, rule implI, simp)
        fix xa aa
        assume hyp: "\<forall>a. a - xa = 0 \<longrightarrow> a \<le> xa = 1"
        assume H1: "aa - S xa = 0"
        show "xa N \<Longrightarrow> aa N \<Longrightarrow> aa \<le> S xa = 1"
          apply (rule cases_nat[where x="aa-xa"])
          apply (rule leq_trans[where y="xa"])
          apply (simp)
          apply (rule implE[where a="aa - xa = 0"])
          apply (rule forallE[where a="aa"])
          apply (rule hyp, simp)
          apply (rule cases_nat[where x="aa"])
          apply (simp)
          apply (rule existsE[where Q="\<lambda>c. aa = S(c)"])
          apply (simp)
          proof -
            show "aa N \<Longrightarrow> aa N" by (simp)
            show "aa N \<Longrightarrow> xa N \<Longrightarrow> aa - xa N" by (simp)
            fix a
            assume aa_sub_xa_nz: "\<not> aa - xa = 0" and aa_nz: "\<not> aa = 0" and aa_eq_sa: "aa = S a"
            show "aa N \<Longrightarrow> xa N \<Longrightarrow> a N \<Longrightarrow> aa \<le> S xa = 1"
              apply (rule eqSubst[where a="S a" and b="aa"])
              apply (rule eqSym)
              apply (rule aa_eq_sa)
              apply (rule leq_monotone_suc, simp)
              apply (rule implE[where a="a - xa = 0"])
              apply (rule forallE[where a="a"])
              apply (rule hyp, simp)
              apply (rule sub_monotone_lhs)
              apply (subst "aa = S a")
              apply (rule aa_eq_sa)
              apply (subst "S P (aa - xa) = aa - xa", simp)
              apply (rule aa_sub_xa_nz)
              apply (rule sucCong)
              apply (subst "aa - S(xa) = P(aa - xa)")
              apply (rule eqSym)
              apply (unfold_def sub_def)
              apply (simp)
              apply (rule H1, simp)
              done
          qed
      qed
  qed
  then have "a N \<Longrightarrow> b N \<Longrightarrow> a - b = 0 \<longrightarrow> a \<le> b = 1"
    apply (rule forallE, simp)
    done
  then show "a N \<Longrightarrow> b N \<Longrightarrow> a \<le> b = 1"
    apply (rule implE, simp)
    apply (rule H)
    done
qed

lemma less_monotone_pred:
  shows "x N \<Longrightarrow> y N \<Longrightarrow> S x < S y = 1 \<Longrightarrow> x < y = 1"
proof (rule grounded_contradiction[where q="x < y = 1"], simp)
  have H1: "x N \<Longrightarrow> y N \<Longrightarrow> S(x) < S(y) = x < y"
    apply (rule eqSym)
    apply (unfold_def less_def)
    apply (simp)
    done
  show "x N \<Longrightarrow> y N \<Longrightarrow> S x < S y = 1 \<Longrightarrow> x < y = 1"
    apply (rule eqSubst[where a="S(x) < S(y)" and b="1"])
    apply (simp)
    apply (rule eqSym)
    apply (rule H1, simp)
    done
qed

lemma less_trans:
  assumes x_nat: "x N"
  assumes y_nat: "y N"
  assumes z_nat: "z N"
  assumes x_le_y: "x < y = 1"
  assumes y_le_z: "y < z = 1"
  shows "x < z = 1"
proof -
  have quantized: "\<forall>x y. (x < y = 1) \<longrightarrow> (y < z = 1) \<longrightarrow> (x < z = 1)"
    proof (rule ind[where a="z"])
    show "z N" by (rule z_nat)
    show "\<forall>x y. x < y = 1 \<longrightarrow>
      y < 0 = 1 \<longrightarrow> x < 0 = 1"
      apply (rule forallI)+
      proof (rule implI, simp)+
        fix x y
        show "y < 0 = 1 \<Longrightarrow> x < 0 = 1"
          apply (rule exF[where P="y < 0 = 1"], simp)
          apply (subst "0 = y < 0")
          done
      qed
    show "\<And>x. x N \<Longrightarrow> (\<forall>xa y. xa < y = 1 \<longrightarrow> y < x = 1 \<longrightarrow> xa < x = 1) \<Longrightarrow>
      (\<forall>xa y. xa < y = 1 \<longrightarrow> y < S x = 1 \<longrightarrow> xa < S x = 1)"
      proof -
        fix x
        show "x N \<Longrightarrow> \<forall>xa y. xa < y = 1 \<longrightarrow> y < x = 1 \<longrightarrow> xa < x = 1 \<Longrightarrow>
              \<forall>xa y. xa < y = 1 \<longrightarrow> y < S x = 1 \<longrightarrow> xa < S x = 1"
          proof -
            assume hyp: "\<forall>xa y. xa < y = 1 \<longrightarrow> y < x = 1 \<longrightarrow> xa < x = 1"
            show "x N \<Longrightarrow> \<forall>xa y. xa < y = 1 \<longrightarrow> y < S x = 1 \<longrightarrow> xa < S x = 1"
              apply (rule forallI)+
              proof (rule implI, simp)+
                fix xa ya
                assume xa_le_ya: "xa < ya = 1"
                assume ya_le_sx: "ya < S x = 1"
                show "x N \<Longrightarrow> xa N \<Longrightarrow> ya N \<Longrightarrow> xa < S x = 1"
                  apply (rule cases_nat[where x="xa"])
                  apply (simp)
                  apply (unfold_def less_def)
                  apply (simp)
                  proof -
                    assume xa_nz: "\<not> xa = 0"
                    have ya_nz: "ya N \<Longrightarrow> \<not> ya = 0"
                      apply (rule grounded_contradiction[where q="xa < ya = 1"])
                      apply (simp)
                      apply (rule xa_le_ya)
                      apply (rule eqSubst[where a="0" and b="xa < ya"])
                      apply (rule eqSym)
                      apply (rule eqSubst[where a="0" and b="ya"])
                      apply (rule eqSym)
                      apply (rule dNegE)
                      apply (auto)
                      done
                    have H: "x N \<Longrightarrow> ya N \<Longrightarrow> P(ya) < P(S x) = 1"
                      apply (rule less_monotone_pred)
                      apply (rule natP, assumption, simp+)
                      apply (rule eqSubst[where a="ya" and b="S P ya"])
                      apply (rule eqSym, simp)
                      apply (rule ya_nz, simp+)
                      apply (rule ya_le_sx)
                      done
                    have H2: "x N \<Longrightarrow> ya N \<Longrightarrow> P(ya) < x = 1"
                      apply (rule eqSubst[where a="P S x" and b="x"])
                      apply (auto)
                      apply (rule H, simp)
                      done
                    have H3: "xa N \<Longrightarrow> ya N \<Longrightarrow> P(xa) < P(ya) = 1"
                      apply (rule less_monotone_pred)
                      apply (rule natP, assumption)+
                      apply (rule eqSubst[where a="xa" and b="S P xa"])
                      apply (rule eqSym)
                      apply (auto)
                      apply (rule xa_nz)
                      apply (rule eqSubst[where a="ya" and b="S P ya"])
                      apply (rule eqSym, simp)
                      apply (rule ya_nz, simp)
                      apply (rule xa_le_ya)
                      done
                    have H4: "xa N \<Longrightarrow> ya N \<Longrightarrow> P xa < P ya = 1 \<longrightarrow> P ya < x = 1 \<longrightarrow> P xa < x = 1"
                      apply (rule forallE[where a="P ya"])
                      apply (rule forallE[where a="P xa"])
                      apply (rule hyp, simp)
                      done
                    then have H5: "xa N \<Longrightarrow> ya N \<Longrightarrow> P ya < x = 1 \<longrightarrow> P xa < x = 1"
                      apply (rule implE, simp)
                      apply (rule H3, simp)
                      done
                    then show "xa N \<Longrightarrow> ya N \<Longrightarrow> x N \<Longrightarrow> P xa < x = 1"
                      apply (rule implE, simp)
                      apply (rule H2, simp)
                      done
                  qed
            qed
          qed
      qed
    qed
    then have "\<forall>y. (x < y = 1) \<longrightarrow> (y < z = 1) \<longrightarrow> (x < z = 1)"
      apply (rule forallE)
      apply (rule x_nat)
      done
    then have "(x < y = 1) \<longrightarrow> (y < z = 1) \<longrightarrow> (x < z = 1)"
      apply (rule forallE)
      apply (rule y_nat)
      done
    then have "(y < z = 1) \<longrightarrow> (x < z = 1)"
      apply (rule implE)
      apply (rule x_le_y)
      done
    then show ?thesis
      apply (rule implE)
      apply (rule y_le_z)
      done
qed

lemma sub_less:
  shows "x N \<Longrightarrow> y N \<Longrightarrow> S(x) - S(y) < S(x) = 1"
apply (rule ind[where a="y"])
apply (simp)
apply (rule eqSubst[where a="P(S(x) - 0)" and b="S(x) - 1"])
apply (unfold_def sub_def)
proof (simp+)
  fix xa
  assume hyp: "S x - S xa < S x = 1"
  show "x N \<Longrightarrow> xa N \<Longrightarrow> S x - S S xa < S x = 1"
    apply (rule eqSubst[where b="S x - S S xa" and a="P(S(x) - S(xa))"])
    apply (unfold_def sub_def, simp+)
    apply (rule cases_nat[where x="S(x) - S(xa)"], simp+)
    apply (rule less_monotone_pred)
    apply (rule natP, rule sub_terminates)
    apply (rule natS, assumption)+
    apply (rule eqSubst[where a="S x - S xa" and b="S P (S x - S xa)"], simp)
    apply (rule less_trans[where y="S x"], simp)
    apply (rule hyp, simp)
    done
qed

lemma less_not_refl [simp]:
  shows "x N \<Longrightarrow> x < x = 0"
apply (rule ind[where a="x"], simp)
apply (unfold_def less_def, simp)
done

lemma [simp]: "x N \<Longrightarrow> 0 - x = 0"
apply (induct x, simp)
apply (unfold_def sub_def, simp)
done

lemma unfold_sub: "a N \<Longrightarrow> b N \<Longrightarrow> a - (S b) = P(a - b)"
apply (rule eqSym, unfold_def sub_def, rule eqSym)
apply (simp)
done

lemma [simp]: "a N \<Longrightarrow> a - 1 = P(a)"
by (unfold_def sub_def, simp)

lemma sub_mono_suc: "a N \<Longrightarrow> b N \<Longrightarrow> S a - S b = a - b"
apply (induct b, simp+)
apply (rule eqSym, unfold_def sub_def, rule eqSym, simp)
apply (simp add: unfold_sub)
done

lemma fold_sub: "a N \<Longrightarrow> b N \<Longrightarrow> P(S(a) - b) = (S a) - (S b)"
by (rule eqSym, rule unfold_sub, simp)

lemma sub_distr_pred: "a N \<Longrightarrow> b N \<Longrightarrow> P(a - b) = P(a) - b"
apply (induct a, simp+)
apply (simp add: fold_sub sub_mono_suc)
done

lemma [simp]: "a N \<Longrightarrow> a - a = 0"
apply (induct a, simp)
apply (unfold_def sub_def)
apply (simp add: sub_distr_pred)
done

lemma div_x_x_1 [auto, simp]:
  shows "x N \<Longrightarrow> div (S x) (S x) = 1"
by (unfold_def div_def, simp)

lemma cpair_1_0_1 [simp, auto]: "\<langle>1, 0\<rangle> = 1"
  unfolding cpair_def by (simp)

lemma sub_eq_self_imp_zero:
  assumes x_nat: "x N"
  assumes y_nat: "y N"
  assumes H: "S(y) - x = S(y)"
  shows "x = 0"
proof (rule grounded_contradiction[where q="S(y) < S(y) = 1"])
  show "x = 0 B" by (auto, rule x_nat)
  assume x_nz: "\<not> x = 0"
  have H1: "S(y) - x < S(y) = 1"
    apply (rule existsE[where Q="\<lambda>c. x = S(c)"])
    apply (auto)
    apply (rule x_nat)
    apply (rule x_nz)
    proof -
      fix a
      assume a_nat: "a N" and x_p: "x = S a"
      show "S y - x < S y = 1 "
        apply (rule eqSubst[where a="S a" and b="x"])
        apply (rule eqSym)
        apply (rule x_p)
        apply (rule sub_less)
        apply (rule y_nat)
        apply (rule a_nat)
        done
    qed
  show "S(y) < S(y) = 1"
    apply (rule eqSubst[where a="S(y) - x" and b="S(y)" and Q="\<lambda>c. c < S(y) = 1"])
    apply (rule H)
    apply (rule H1)
    done
  show "\<not> S(y) < S(y) = 1"
    apply (rule eqSubst[where a="0" and b= "S y < S y"])
    apply (rule eqSym)
    apply (rule less_not_refl)
    apply (rule natS)
    apply (rule y_nat)
    apply (fold neq_def)
    apply (auto)
    done
qed

lemma div_nz:
  assumes x_geq_y: "x \<ge> S(y) = 1"
  shows "x N \<Longrightarrow> y N \<Longrightarrow> \<not> div x S(y) = 0"
apply (rule eqSubst[where a="S(div (x - S y) S(y))" and b="div x S(y)"])
apply (unfold_def div_def)
apply (rule eqSym)
apply (rule condI2)
apply (rule eqSubst[where a="0" and b="x < S y"])
apply (rule eqSym)
apply (rule sub_eq_self_imp_zero[where y="0"])
apply (simp)
apply (fold geq_def)
apply (rule x_geq_y)
apply (simp)
done

lemma [auto]:
  assumes p_bool: "p B"
  assumes q_bool: "q B"
  shows "p \<and> q B"
apply (unfold conj_def)
apply (auto)
apply (rule p_bool)
apply (rule q_bool)
done

lemma notE_impl: "\<not> a \<Longrightarrow> a \<longrightarrow> b"
apply (unfold impl_def)
apply (rule disjI1)
apply (assumption)
done

lemma [auto]:
  "a N \<Longrightarrow> b N \<Longrightarrow> \<not> (a = b) \<Longrightarrow> \<not> (S a = S b)"
apply (rule grounded_contradiction[where q="a = b"], simp)
apply (rule sucInj)
apply (rule dNegE, simp)
done

lemma [simp]:
  "\<not>a \<Longrightarrow> b B \<Longrightarrow> a \<or> b \<longleftrightarrow> b"
apply (rule iffI, simp)
apply (rule grounded_contradiction[where q="\<not>(a \<or> b)"], simp)
apply (rule disjI2, simp)
done

lemma [simp]:
  "\<not>b \<Longrightarrow> a B \<Longrightarrow> a \<or> b \<longleftrightarrow> a"
apply (rule iffI, simp)
apply (rule grounded_contradiction[where q="\<not>(a \<or> b)"], simp)
apply (rule disjI1, simp)
done

lemma [auto]: "y N \<Longrightarrow> x = 0 \<Longrightarrow> y - x = y"
by (simp)

lemma [auto]: "a N \<Longrightarrow> b N \<Longrightarrow> a \<le> b = 0 \<Longrightarrow> S a \<le> S b = 0"
by (unfold_def leq_def, simp)

lemma gr_mono_suc [auto]: "a N \<Longrightarrow> b N \<Longrightarrow> a > b = 1 \<Longrightarrow> S a > S b = 1"
unfolding greater_def
apply (simp)
apply (rule sub_eq_self_imp_zero[where y="0"])
apply (simp)
done

lemma [simp]: "a N \<Longrightarrow> S a > 0 = 1"
unfolding greater_def by simp

lemma [simp]: "a < b = 1 \<Longrightarrow> a N \<Longrightarrow> b N \<Longrightarrow> \<not> a = b \<longleftrightarrow> True"
apply (rule iffI, simp)
apply (rule grounded_contradiction[where q="a < a = 1"], simp)
apply (subst "a < b = a < a")
apply (subst "a = b")
apply (rule dNegE, simp+)
done

lemma [simp]: "a N \<Longrightarrow> a > a = 0"
unfolding greater_def by simp

lemma [simp]: "a > b = 1 \<Longrightarrow> a N \<Longrightarrow> b N \<Longrightarrow> \<not> a = b \<longleftrightarrow> True"
apply (rule iffI, simp)
apply (rule grounded_contradiction[where q="a > a = 1"], simp)
apply (subst "a > b = a > a")
apply (subst "a = b")
apply (rule dNegE)
apply (simp+)
done

lemma le_less_trans:
  "a N \<Longrightarrow> b N \<Longrightarrow> c N \<Longrightarrow> a \<le> b = 1 \<Longrightarrow> b < c = 1 \<Longrightarrow> a < c = 1"
apply (cases bool: "a=b", simp)
apply (subst "b=a")
apply (rule less_trans[where y="b"], simp)
apply (rule less_is_leq_neq, simp)
done

lemma less_le_trans: "a N \<Longrightarrow> b N \<Longrightarrow> c N \<Longrightarrow> a < b = 1 \<Longrightarrow> b \<le> c = 1 \<Longrightarrow> a < c = 1"
apply (cases bool: "b = c", simp)
apply (subst "b = c")
apply (rule less_trans[where y="b"], simp)
apply (rule less_is_leq_neq, simp)
done

lemma neg_conjI1: "\<not>a \<Longrightarrow> \<not>(a \<and> b)"
  unfolding conj_def by (rule dNegI, rule disjI1, simp)

lemma neg_conjI2: "\<not>b \<Longrightarrow> \<not>(a \<and> b)"
  unfolding conj_def by (rule dNegI, rule disjI2, simp)

lemma [cond]: "((c B) \<and> (a N) \<and> (b N)) \<Longrightarrow> if c then a else b N"
apply (rule condT)
apply (rule conjE1, rule conjE1, simp)
apply (rule conjE2, rule conjE1, simp)
apply (rule conjE2, simp)
done

lemma [cond]: "((c B) \<and> (a B) \<and> (b B)) \<Longrightarrow> if c then a else b B"
apply (rule condTB)
apply (rule conjE1, rule conjE1, simp)
apply (rule conjE2, rule conjE1, simp)
apply (rule conjE2, simp)
done

lemma suc_nz: "\<not> x = 0 \<Longrightarrow> x N \<Longrightarrow> Q (S (P x)) \<Longrightarrow> Q x"
by simp

lemma [simp]: "x N \<Longrightarrow> y N \<Longrightarrow> x < x + S(y) = 1"
apply (unfold_def add_def, simp)
apply (rule le_less_trans[where b="x+y"], simp+)
done

lemma add_assoc: "a N \<Longrightarrow> b N \<Longrightarrow> c N \<Longrightarrow> a + b + c = a + (b + c)"
apply (induct c, simp+)
apply (unfold_def add_def, simp)
apply (rule eqSym)
apply (unfold_def add_def, simp)
done

lemma and_assoc: "(a \<and> b \<and> c) \<Longrightarrow> (a \<and> (b \<and> c))"
apply (rule conjE1, rule conjE2, simp)
apply (rule conjE1, rule conjE1, simp)
apply (rule conjE2, rule conjE1, simp)
apply (rule conjE2, rule conjE2, simp)
done

lemma gr_mono_pred:
  "a N \<Longrightarrow> b N \<Longrightarrow> \<not> a = 0 \<Longrightarrow> \<not> b = 0 \<Longrightarrow> P a > P b = 1 \<Longrightarrow> a > b = 1"
apply (rule suc_nz[where x="a"], simp)
apply (rule suc_nz[where x="b"], simp)
done

lemma not_le_mono_suc [simp]:
  "a N \<Longrightarrow> b N \<Longrightarrow> a < b = 0 \<Longrightarrow> S a < S b = 0"
by (unfold_def less_def, simp)

lemma geq_mono_suc [simp]: "a N \<Longrightarrow> b N \<Longrightarrow> a \<ge> b = 1 \<Longrightarrow> S a \<ge> S b = 1"
apply (unfold geq_def, simp)
apply (rule not_le_mono_suc, simp)
apply (rule sub_eq_self_imp_zero[where y="0"], simp)
done

lemma geq_mono_pred:
  "a N \<Longrightarrow> b N \<Longrightarrow> \<not> a = 0 \<Longrightarrow> \<not> b = 0 \<Longrightarrow> P a \<ge> P b = 1 \<Longrightarrow> a \<ge> b = 1"
apply (rule suc_nz[where x="a"], simp)
apply (rule suc_nz[where x="b"], simp)
apply (rule geq_mono_suc, simp)
done

lemma cpair_strict_mono_r [simp]:
  "x N \<Longrightarrow> y N \<Longrightarrow> (S y) < \<langle>x, (S y)\<rangle> = 1"
proof (induct y)
  case Base
    show "x N \<Longrightarrow> y N \<Longrightarrow> 1 < \<langle>x,1\<rangle> = 1"
      apply (rule less_le_trans[where b="2"], simp)
      apply (unfold_def cpair_def, simp)
      done
next
  case (Step xa)
  show "x N \<Longrightarrow> y N \<Longrightarrow> xa N \<Longrightarrow> S xa < \<langle>x, (S xa)\<rangle> = 1 \<Longrightarrow> S S xa < \<langle>x, (S S xa)\<rangle> = 1"
    apply (unfold_def cpair_def, simp)
    apply (rule less_le_trans[where b="S S xa + 2"])
    apply (simp add: add_assoc)+
    done
qed

lemma sum_0_summands_0: "a N \<Longrightarrow> b N \<Longrightarrow> a + b = 0 \<Longrightarrow> a = 0 \<and> b = 0"
apply (rule implE[where a="a+b=0"])
apply (unfold_def add_def)
apply (cases bool: "b = 0", simp+)
apply (rule implI, simp+)+
apply (rule exF[where P="S(a + P b) = 0"], simp)+
done

lemma [simp]: "a N \<Longrightarrow> b N \<Longrightarrow> c N \<Longrightarrow> b = c \<Longrightarrow> \<langle>a,b\<rangle> = \<langle>a,c\<rangle> \<longleftrightarrow> True"
by (rule iffI, simp+)

lemma [simp]: "a N \<Longrightarrow> b N \<Longrightarrow> c N \<Longrightarrow> \<not> b = c \<Longrightarrow> \<langle>a,b\<rangle> = \<langle>a,c\<rangle> \<longleftrightarrow> False"
apply (rule iffI, simp)
apply (rule exF[where P="b=c"])
apply (rule conjE2[where p="a=a"])
apply (rule cpair_inj, simp)
apply (rule contradiction, simp)
done

lemma [simp]: "\<not> a = 0 \<Longrightarrow> a N \<Longrightarrow> b N \<Longrightarrow> \<not> a + b = 0 \<longleftrightarrow> True"
apply (rule iffI, simp)
apply (rule grounded_contradiction[where q="a = 0"], simp)
apply (rule conjE1[where q="b=0"], rule sum_0_summands_0, simp, rule dNegE, simp)
done

lemma [simp]: "\<not> b = 0 \<Longrightarrow> a N \<Longrightarrow> b N \<Longrightarrow> \<not> a + b = 0 \<longleftrightarrow> True"
apply (rule iffI, simp)
apply (rule grounded_contradiction[where q="b = 0"], simp)
apply (rule conjE2, rule sum_0_summands_0, simp, rule dNegE, simp)
done

lemma noteq_sym: "\<not> a = b \<Longrightarrow> a N \<Longrightarrow> b N \<Longrightarrow> \<not> b = a"
apply (fold neq_def)
apply (rule neq_sym)
apply (simp)
done

lemma [simp]: "x N \<Longrightarrow> y N \<Longrightarrow> P(S x + y) = x + y"
apply (induct y, simp+)
apply (rule eqSym, unfold_def add_def, rule eqSym, simp)
apply (unfold_def add_def, simp)
proof -
  fix xa
  show "x N \<Longrightarrow> y N \<Longrightarrow> xa N \<Longrightarrow> P(S x + xa) = x + xa \<Longrightarrow> S x + xa = S(x + xa)"
  apply (subst "P(S x + xa) = x+xa")
  apply (subst rule: suc_pred_inv, simp)
  done
qed

lemma [auto]: "b N \<Longrightarrow> \<not> b = 0 \<Longrightarrow> 0 < b = 1"
by (unfold_def less_def, simp)

lemma [simp]: "\<not> b = 0 \<Longrightarrow> a N \<Longrightarrow> b N \<Longrightarrow> a < a + b = 1"
apply (induct a, simp+)
apply (unfold_def less_def, simp+)
done

lemma [simp]:
  shows "\<not> y = 0 \<Longrightarrow> x N \<Longrightarrow> y N \<Longrightarrow> y < \<langle>x, y\<rangle> = 1"
by (rule suc_nz[where x="y"], simp, rule cpair_strict_mono_r, simp)

lemma less_impl_leq [simp]: "x < y = 1 \<Longrightarrow> x N \<Longrightarrow> y N \<Longrightarrow> x \<le> y = 1"
proof -
  have H: "y N \<Longrightarrow> \<forall>x. x < y = 1 \<longrightarrow> x \<le> y = 1"
    proof (induct y)
      case Base
        show ?case
          apply (rule forallI, rule implI, simp+)
          done
    next
      case (Step x)
        show "y N \<Longrightarrow> x N \<Longrightarrow>
              \<forall>xa. xa < x = 1 \<longrightarrow> xa \<le> x = 1 \<Longrightarrow>
              \<forall>xa. xa < S x = 1 \<longrightarrow> xa \<le> S x = 1 "
          apply (rule forallI)
          proof -
            fix xaa
            show "y N \<Longrightarrow> x N \<Longrightarrow> \<forall>xaa. xaa < x = 1 \<longrightarrow> xaa \<le> x = 1 \<Longrightarrow>
                  xaa N \<Longrightarrow> xaa < S x = 1 \<longrightarrow> xaa \<le> S x = 1"
              apply (unfold_def less_def, simp)
              apply (cases bool: "xaa = 0", simp+)
              apply (rule implI, simp+)+
              apply (unfold_def leq_def, simp)
              apply (rule implE[where a="P xaa < x = 1"])
              apply (rule forallE[where a="P xaa"], simp)
              done
          qed
    qed
  show "x N \<Longrightarrow> y N \<Longrightarrow> x < y = 1 \<Longrightarrow> x \<le> y = 1"
    apply (rule implE[where a="x < y = 1"], rule forallE[where a="x"])
    apply (rule H, simp)
    done
qed

lemma cpair_mono_r [simp]:
  "x N \<Longrightarrow> y N \<Longrightarrow> y \<le> \<langle>x, y\<rangle> = 1"
by (cases bool: "y = 0", simp+)

lemma cpair_le_2 [simp]:
  "a \<le> c = 1 \<Longrightarrow> \<not> c = 0 \<Longrightarrow> a N \<Longrightarrow> b N \<Longrightarrow> c N \<Longrightarrow> a < \<langle>b,c\<rangle> = 1"
by (rule le_less_trans[where b="c"], simp+)

lemma leq_mono_add_l [simp]:
  "b \<le> c = 1 \<Longrightarrow> a N \<Longrightarrow> b N \<Longrightarrow> c N \<Longrightarrow> a + b \<le> a + c = 1"
apply (induct a, simp+)
apply (unfold_def leq_def, simp)
done

lemma leq_mono_add_r [simp]:
  "b \<le> c = 1 \<Longrightarrow> a N \<Longrightarrow> b N \<Longrightarrow> c N \<Longrightarrow> b + a \<le> c + a = 1"
apply (induct a, simp+)
apply (unfold_def add_def, simp)+
done

lemma less_mono_add_l [simp]:
  "b < c = 1 \<Longrightarrow> a N \<Longrightarrow> b N \<Longrightarrow> c N \<Longrightarrow> a + b < a + c = 1"
apply (induct a, simp+)
apply (unfold_def less_def, simp)
done

lemma less_mono_add_r [simp]:
  "b < c = 1 \<Longrightarrow> a N \<Longrightarrow> b N \<Longrightarrow> c N \<Longrightarrow> b + a < c + a = 1"
apply (induct a, simp+)
apply (unfold_def add_def, simp)+
done

lemma [simp]: "a N \<Longrightarrow> b N \<Longrightarrow> \<not> S(a) * S(b) = 0"
by (unfold_def mult_def, simp)

lemma zero_not_less_impl_zero: "a N \<Longrightarrow> 0 < a = 0 \<Longrightarrow> a = 0"
apply (rule grounded_contradiction[where q="0 < S(P a) = 0"], simp)
apply (simp)
apply (subst "1 = 0 < S P a", rule eqSym)
apply (rule zero_less_true, simp)
done

lemma zero_not_less_zero [simp]: "a = 0 \<Longrightarrow> 0 < a = 0"
by simp

lemma [simp]: "x N \<Longrightarrow> S x \<ge> 0 = 1"
by (unfold geq_def, simp)

lemma le_impl_ge: "a N \<Longrightarrow> b N \<Longrightarrow> a \<le> b = 1 \<Longrightarrow> b \<ge> a = 1"
proof -
  have H:"a N \<Longrightarrow> b N \<Longrightarrow> \<forall>a. a \<le> b = 1 \<longrightarrow> b \<ge> a = 1"
    proof (induct b)
      case Base
        show ?case
          apply (rule forallI, rule implI, simp)
          apply (unfold geq_def, simp)
          apply (rule zero_not_less_zero)
          apply (rule leq_0, simp)
          done
    next
      case (Step x)
        show "a N \<Longrightarrow> b N \<Longrightarrow> x N \<Longrightarrow>
              \<forall>a. a \<le> x = 1 \<longrightarrow> x \<ge> a = 1 \<Longrightarrow>
              \<forall>a. a \<le> S x = 1 \<longrightarrow> S x \<ge> a = 1"
          apply (rule forallI)
          proof -
            fix aa
            show "b N \<Longrightarrow> x N \<Longrightarrow> aa N \<Longrightarrow> \<forall>a. a \<le> x = 1 \<longrightarrow> x \<ge> a = 1 \<Longrightarrow>
                  aa \<le> S x = 1 \<longrightarrow> S x \<ge> aa = 1"
              apply (unfold_def leq_def, simp)
              apply (cases bool: "aa = 0", simp+)
              apply (rule implI, simp+)
              apply (rule implI, simp)
              apply (rule geq_mono_pred, simp+)
              apply (rule implE[where a="P aa \<le> x = 1"])
              apply (rule forallE[where a="P aa"], simp)
              done
          qed
    qed
  show "a \<le> b = 1 \<Longrightarrow> a N \<Longrightarrow> b N \<Longrightarrow> b \<ge> a = 1"
    apply (rule implE[where a="a \<le> b = 1"])
    apply (rule forallE[where a="a"])
    apply (rule H, simp)
    done
qed

lemma [auto]: "a N \<Longrightarrow> b N \<Longrightarrow> a \<ge> b N"
unfolding geq_def by simp

lemma [simp]: "a N \<Longrightarrow> 0 \<ge> S a = 0"
unfolding geq_def by simp

lemma ge_impl_le: "a N \<Longrightarrow> b N \<Longrightarrow> a \<ge> b = 1 \<Longrightarrow> b \<le> a = 1"
proof -
  have H:"a N \<Longrightarrow> b N \<Longrightarrow> \<forall>a. a \<ge> b = 1 \<longrightarrow> b \<le> a = 1"
    proof (induct b)
      case Base
        show ?case
          by (rule forallI, rule implI, simp)
    next
      case (Step x)
        show "a N \<Longrightarrow> b N \<Longrightarrow> x N \<Longrightarrow>
              \<forall>a. a \<ge> x = 1 \<longrightarrow> x \<le> a = 1 \<Longrightarrow>
              \<forall>a. a \<ge> S x = 1 \<longrightarrow> S x \<le> a = 1"
          apply (rule forallI)
          proof -
            fix aa
            show "b N \<Longrightarrow> x N \<Longrightarrow> aa N \<Longrightarrow> \<forall>a. a \<ge> x = 1 \<longrightarrow> x \<le> a = 1 \<Longrightarrow>
                  aa \<ge> S x = 1 \<longrightarrow> S x \<le> aa = 1"
              apply (unfold_def leq_def, simp)
              apply (cases bool: "aa = 0", simp+)
              apply (rule implI, simp+)
              apply (unfold geq_def)
              apply (unfold_def less_def, simp, fold geq_def)
              apply (rule implI, simp)
              apply (rule implE[where a="P aa \<ge> x = 1"])
              apply (rule forallE[where a="P aa"], simp)
              done
          qed
    qed
  show "a \<ge> b = 1 \<Longrightarrow> a N \<Longrightarrow> b N \<Longrightarrow> b \<le> a = 1"
    apply (rule implE[where a="a \<ge> b = 1"])
    apply (rule forallE[where a="a"])
    apply (rule H, simp)
    done
qed

lemma [simp]: "a N \<Longrightarrow> b N \<Longrightarrow> c N \<Longrightarrow> a \<le> b = 1 \<Longrightarrow> a - c \<le> b - c = 1"
apply (induct c, simp+)
apply (unfold_def sub_def, simp+)+
done

lemma leq_mono_div [simp]:
  "a N \<Longrightarrow> b N \<Longrightarrow> c N \<Longrightarrow> a \<le> b = 1 \<Longrightarrow> div a (S c) \<le> div b (S c) = 1"
apply (rule implE[where a="a\<le>b=1"])
apply (rule forallE[where a="b"])
apply (induct strong a, simp)
apply (rule forallI)
apply (rule implI, simp+)
apply (rule forallI)
apply (rule implI, simp)
proof -
  fix x b'
  assume step: "(\<And>y. y N \<Longrightarrow>
      y \<le> x = 1 \<Longrightarrow>
      \<forall>c'. y \<le> c' = 1 \<longrightarrow> div y (S c) \<le> div c' (S c) = 1)"
  show "a N \<Longrightarrow> b N \<Longrightarrow> b' N \<Longrightarrow> c N \<Longrightarrow> x N \<Longrightarrow> a \<le> b = 1 \<Longrightarrow>
     S x \<le> b' = 1 \<Longrightarrow> div (S x) (S c) \<le> div b' (S c) = 1"
    apply (unfold_def div_def)
    apply (cases bool: "b' < S c = 1", simp+)
    apply (unfold_def div_def)
    apply (cases bool: "S x < S c = 1", simp+)
    apply (rule grounded_contradiction[where q="S x < S c = 1"], simp)
    apply (rule le_less_trans[where b="b'"], simp+)
    apply (rule ge_impl_le, simp)
    apply (unfold_def div_def)
    apply (cases bool: "S x < S c = 1", simp+)
    apply (rule le_impl_ge, simp)
    apply (rule leq_monotone_suc, simp)
    apply (rule implE)
    apply (rule forallE[where a="b' - S c"])
    apply (rule step, simp+)
    done
qed

lemma leq_mono_mult_r [simp]:
  "a \<le> b = 1 \<Longrightarrow> a N \<Longrightarrow> b N \<Longrightarrow> c N \<Longrightarrow> a * c \<le> b * c = 1"
apply (induct c, simp+)
apply (unfold_def mult_def, simp)+
proof -
  fix x
  show "a \<le> b = 1 \<Longrightarrow> a N \<Longrightarrow> b N \<Longrightarrow> x N \<Longrightarrow> a * x \<le> b * x = 1 \<Longrightarrow>
        a + a * x \<le> b + b * x = 1"
    by (rule leq_trans[where y="a + b*x"], simp+)
qed

lemma leq_mono_mult_l [simp]:
  "a \<le> b = 1 \<Longrightarrow> a N \<Longrightarrow> b N \<Longrightarrow> c N \<Longrightarrow> c * a \<le> c * b = 1"
apply (rule implE[where a="a\<le>b=1"])
apply (rule forallE[where a="b"])
apply (induct a, simp)
apply (rule forallI, rule implI, simp+)
proof (rule forallI)
  fix a b
  show "\<forall>b. a \<le> b = 1 \<longrightarrow> c * a \<le> c * b = 1 \<Longrightarrow>
        a N \<Longrightarrow> b N \<Longrightarrow> c N \<Longrightarrow> S a \<le> b = 1 \<longrightarrow> c * (S a) \<le> c * b = 1"
    apply (cases bool: "b=0", simp)
    apply (rule implI, simp)
    apply (rule exF[where P="S a = 0"], simp)
    apply (rule leq_0, simp)
    apply (unfold_def leq_def, simp)
    apply (rule implI, simp)
    apply (unfold_def mult_def, simp)+
    apply (rule leq_mono_add_l)
    apply (rule implE[where a="a\<le>P b=1"])
    apply (rule forallE[where a="P b"], simp)
    done
qed

lemma [simp]:
  "a < b = 1 \<Longrightarrow> a N \<Longrightarrow> b N \<Longrightarrow> c N \<Longrightarrow> a < b + c = 1"
apply (induct c, simp+)
apply (unfold_def add_def, simp)
proof -
  fix x
  show "a < b = 1 \<Longrightarrow> a N \<Longrightarrow> b N \<Longrightarrow> x N \<Longrightarrow> a < b + x = 1 \<Longrightarrow> a < S(b + x) = 1"
    by (rule less_le_trans[where b="b+x"], simp)
qed

lemma [simp]: "a N \<Longrightarrow> b N \<Longrightarrow> a \<le> a + b = 1"
by (induct b, simp+)

lemma [simp]: "a N \<Longrightarrow> b N \<Longrightarrow> a + b < a = 0"
apply (induct a, simp)
apply (rule swap_add, simp)
apply (unfold_def add_def, simp)
apply (rule swap_add, simp+)
done

lemma [simp]: "a N \<Longrightarrow> b N \<Longrightarrow> a + b \<ge> a = 1"
by (unfold geq_def, simp)

lemma [simp]: "a N \<Longrightarrow> b N \<Longrightarrow> a * S(b) < a = 0"
by (unfold_def mult_def, simp)

lemma [simp]: "a N \<Longrightarrow> b N \<Longrightarrow> a + b - b = a"
apply (induct b, simp+)
apply (unfold_def add_def, simp add: sub_mono_suc)
done

lemma [simp]: "a N \<Longrightarrow> b N \<Longrightarrow> a + b - a = b"
by (rule swap_add, simp+)

lemma mult_div_inv: "a N \<Longrightarrow> b N \<Longrightarrow> div ((S a) * b) (S a) = b"
apply (induct b, simp+)
apply (unfold_def div_def, simp)
apply (unfold_def mult_def, simp)
done

lemma [simp]:
  "x N \<Longrightarrow> y N \<Longrightarrow> S S x < \<langle>(S S x), y\<rangle> = 1"
apply (induct y)
apply (unfold_def cpair_def, simp)
apply (rule less_le_trans[where b="div (2 * (S S S x)) 2"], simp)
apply (simp add: mult_div_inv)
apply (rule leq_mono_div, simp+)
apply (unfold_def cpair_def, simp)
done

lemma pred_inj_if_nz:
  "a N \<Longrightarrow> b N \<Longrightarrow> \<not> a = 0 \<Longrightarrow> \<not> b = 0 \<Longrightarrow> P a = P b \<Longrightarrow> a = b"
apply (rule suc_nz[where x="a"], assumption+)
apply (rule suc_nz[where x="b"], assumption+)
apply (simp)
done

lemma cpair_strict_mono_l [simp]:
  "\<not> x = 0 \<Longrightarrow> \<not> x = 1 \<Longrightarrow> x N \<Longrightarrow> y N \<Longrightarrow> x < \<langle>x, y\<rangle> = 1"
apply (rule suc_nz[where x="x"], simp)
apply (rule suc_nz[where x="P(x)"])
apply (rule grounded_contradiction[where q="x=1"], simp)
apply (rule pred_inj_if_nz, simp+)
apply (rule dNegE, simp+)
done

lemma cpair_mono_l [simp]:
  "x N \<Longrightarrow> y N \<Longrightarrow> x \<le> \<langle>x,y\<rangle> = 1"
apply (cases bool: "x=0", simp+)
apply (cases bool: "x=1", simp+)
apply (induct y, simp+)
done

lemma [simp]:
  "a \<le> b = 1 \<Longrightarrow> \<not> b = 0 \<Longrightarrow> \<not> b = 1 \<Longrightarrow> a N \<Longrightarrow> b N \<Longrightarrow> c N \<Longrightarrow> a < \<langle>b,c\<rangle> = 1"
by (rule le_less_trans[where b="b"], simp+)

lemma cpair_of_nz_nz_l: "a N \<Longrightarrow> b N \<Longrightarrow> \<not> a = 0 \<Longrightarrow> \<not> \<langle>a,b\<rangle> = 0"
apply (unfold_def cpair_def)
apply (cases bool: "b=0", simp+)
apply (unfold_def mult_def, simp)
apply (rule swap_add, simp)
apply (unfold_def mult_def, simp)
apply (unfold_def div_def)
apply (rule suc_nz[where x="a"], simp)
apply (unfold_def add_def, simp)
apply (unfold_def less_def, simp)
apply (rule suc_nz[where x="a"], simp)
apply (rule swap_add, simp)
apply (unfold_def add_def, simp+)
done

lemma [simp]: "a N \<Longrightarrow> b N \<Longrightarrow> \<not> a = 0 \<Longrightarrow> \<langle>a,b\<rangle> = 0 \<longleftrightarrow> False"
apply (rule iffI, simp)
apply (rule exF[where P="\<langle>a,b\<rangle> = 0"], simp)
apply (rule cpair_of_nz_nz_l, simp)
apply (rule contradiction, simp)
done

lemma cpair_of_nz_nz_r: "a N \<Longrightarrow> b N \<Longrightarrow> \<not> b = 0 \<Longrightarrow> \<not> \<langle>a,b\<rangle> = 0"
by (unfold_def cpair_def, simp)

lemma [simp]: "a N \<Longrightarrow> b N \<Longrightarrow> \<not> b = 0 \<Longrightarrow> \<langle>a,b\<rangle> = 0 \<longleftrightarrow> False"
apply (rule iffI, simp)
apply (rule exF[where P="\<langle>a,b\<rangle> = 0"], simp)
apply (rule cpair_of_nz_nz_r, simp)
apply (rule contradiction, simp)
done

lemma [simp]: "a < b = 1 \<Longrightarrow> a N \<Longrightarrow> b N \<Longrightarrow> b > a = 1"
proof -
  have H:"a N \<Longrightarrow> b N \<Longrightarrow> \<forall>a. a < b = 1 \<longrightarrow> b > a = 1"
    proof (induct b)
      case Base
        show ?case
        apply (simp, rule forallI, rule implI, simp)
        apply (rule exF[where P="0=1"], simp)
        done
    next
      case (Step x)
        show "a N \<Longrightarrow> b N \<Longrightarrow> x N \<Longrightarrow>
              \<forall>a. a < x = 1 \<longrightarrow> x > a = 1 \<Longrightarrow>
              \<forall>a. a < S x = 1 \<longrightarrow> S x > a = 1"
          apply (rule forallI)
          proof -
            fix aa
            show "b N \<Longrightarrow> x N \<Longrightarrow> aa N \<Longrightarrow> \<forall>a. a < x = 1 \<longrightarrow> x > a = 1 \<Longrightarrow>
                  aa < S x = 1 \<longrightarrow> S x > aa = 1"
              apply (unfold_def less_def, simp)
              apply (cases bool: "aa=0", simp+)
              apply (rule implI, simp+)
              apply (rule implI, simp)
              apply (rule gr_mono_pred, simp+)
              apply (rule implE[where a="P aa < x = 1"])
              apply (rule forallE[where a="P aa"], simp)
              done
          qed
    qed
  show "a < b = 1 \<Longrightarrow> a N \<Longrightarrow> b N \<Longrightarrow> b > a = 1"
    apply (rule implE[where a="a < b = 1"])
    apply (rule forallE[where a="a"])
    apply (rule H, simp)
    done
qed

lemma [auto]: "a = b \<Longrightarrow> cpx a = cpx b"
by (simp, rule eq_impl_term[where b="a"], rule eqSym, assumption)

lemma [auto]: "a = b \<Longrightarrow> cpy a = cpy b"
by (simp, rule eq_impl_term[where b="a"], rule eqSym, assumption)

axiomatization
  cpi' :: "num \<Rightarrow> num \<Rightarrow> num"
where
  cpi'_def: "cpi' n x := if n = 0 then 0
                         else if n = 1 then x
                         else cpy (cpi' (n-1) x)"

definition cpi :: "num \<Rightarrow> num \<Rightarrow> num" where
  "cpi n x \<equiv> cpx (cpi' n x)"

lemma [simp]: "cpi' 0 a = 0"
  by (unfold_def cpi'_def, simp)

lemma [simp]: "cpi 0 a = 0"
  by (unfold cpi_def, simp)

lemma [auto]: "i N \<Longrightarrow> x N \<Longrightarrow> cpi' i x N"
apply (induct i, simp)
apply (unfold_def cpi'_def, simp)
done

lemma [auto]: "i N \<Longrightarrow> x N \<Longrightarrow> cpi i x N"
unfolding cpi_def by simp

lemma [simp]: "a N \<Longrightarrow> cpi' 1 a = a"
by (unfold_def cpi'_def, simp)

lemma [auto]: "a N \<Longrightarrow> cpi 1 a = cpx a"
unfolding cpi_def by simp

lemma [simp]: "a N \<Longrightarrow> b N \<Longrightarrow> cpi 1 \<langle>a, b\<rangle> = a"
unfolding cpi_def by simp

lemma [simp]: "a N \<Longrightarrow> b N \<Longrightarrow> cpi' 2 \<langle>a, b\<rangle> = b"
by (unfold_def cpi'_def, simp)

lemma [auto]: "a N \<Longrightarrow> cpi' 2 a = cpy a"
by (unfold_def cpi'_def, simp)

lemma [auto]: "a N \<Longrightarrow> cpi 2 a = cpx (cpy a)"
unfolding cpi_def by simp

lemma [simp]: "a N \<Longrightarrow> b N \<Longrightarrow> c N \<Longrightarrow> cpi 2 \<langle>a, b, c\<rangle> = b"
unfolding cpi_def by simp

lemma [simp]: "a N \<Longrightarrow> b N \<Longrightarrow> c N \<Longrightarrow> cpi' 3 \<langle>a, b, c\<rangle> = c"
by (unfold_def cpi'_def, simp)

lemma [auto]: "a N \<Longrightarrow> cpi' 3 a = cpy (cpy a)"
by (unfold_def cpi'_def, simp)

lemma [simp]: "a N \<Longrightarrow> b N \<Longrightarrow> c N \<Longrightarrow> d N \<Longrightarrow> cpi 3 \<langle>a, b, c, d\<rangle> = c"
unfolding cpi_def by simp

lemma [auto]: "a N \<Longrightarrow> cpi 3 a = cpx (cpy (cpy a))"
unfolding cpi_def by simp

lemma [simp]: "a N \<Longrightarrow> b N \<Longrightarrow> c N \<Longrightarrow> d N \<Longrightarrow> cpi' 4 \<langle>a, b, c, d\<rangle> = d"
by (unfold_def cpi'_def, simp)

lemma [auto]: "a N \<Longrightarrow> cpi' 4 a = cpy (cpy (cpy a))"
by (unfold_def cpi'_def, simp)

lemma [auto]: "a N \<Longrightarrow> cpi 4 a = cpx (cpy (cpy (cpy a)))"
unfolding cpi_def by simp

lemma [simp]: "x N \<Longrightarrow> x - 1 = P(x)"
by (unfold_def sub_def, simp)

lemma [simp]: "i N \<Longrightarrow> cpi' i 0 = 0"
apply (induct i, simp)
apply (unfold_def cpi'_def, simp)
done

lemma [simp]: "i N \<Longrightarrow> cpi i 0 = 0"
unfolding cpi_def by simp

lemma cpy_nz_arg_nz: "x N \<Longrightarrow> \<not> cpy x = 0 \<Longrightarrow> \<not> x = 0"
apply (rule grounded_contradiction[where q="cpy x = 0"], simp)
apply (subst "0 = x")
apply (rule eqSym, rule dNegE, assumption)
apply (simp)
done

lemma cpx_nz_arg_nz: "x N \<Longrightarrow> \<not> cpx x = 0 \<Longrightarrow> \<not> x = 0"
apply (rule grounded_contradiction[where q="cpx x = 0"], simp)
apply (subst "0 = x")
apply (rule eqSym, rule dNegE, assumption)
apply (simp)
done

lemma cpy_mono [simp]: "x N \<Longrightarrow> cpy x \<le> x = 1"
apply (induct x)
proof (simp add: cpy_suc)+
  case (Step xa)
    show "x N \<Longrightarrow> xa N \<Longrightarrow> cpy xa \<le> xa = 1 \<Longrightarrow>
      (if cpx xa = 0 then 0 else S(cpy xa)) \<le> (S xa) = 1"
      by (cases bool: "cpx xa = 0", simp+)
qed

lemma cpy_strict_mono [simp]: "x N \<Longrightarrow> cpy (S x) < (S x) = 1"
proof (induct strong x)
  case Base
    from Base show ?case
      by (unfold_def cpy_def, simp)
next
  case (Step xa)
    fix y
    assume hyp: "\<And>y. y N \<Longrightarrow> y\<le>xa = 1 \<Longrightarrow> cpy (S y) < (S y) = 1"
    from Step show ?case
      apply (unfold_def cpy_def, simp)
      apply (cases bool: "cpx (S xa) = 0")
      apply (simp add: cpx_suc)+
      apply (cases bool: "cpx xa = 0")
      apply (simp add: cpx_suc cpy_suc)+
      apply (subst "S P xa = xa", simp)
      apply (rule cpx_nz_arg_nz, simp)
      apply (rule le_monotone_suc)+
      apply (rule hyp, simp)
      done
qed

lemma [simp, auto]: "x N \<Longrightarrow> \<not> x = 0 \<Longrightarrow> cpy x < x = 1"
apply (cases x)
apply (rule exF[where P="x=0"], simp)
apply (rule cpy_strict_mono, simp)
done

lemma [simp]: "i N \<Longrightarrow> x N \<Longrightarrow> cpi' (S S i) (S x) < S x = 1"
proof (induct i)
  case Base
    show "i N \<Longrightarrow> x N \<Longrightarrow> cpi' 2 (S x) < (S x) = 1"
      by (unfold_def cpi'_def, simp)
next
  case (Step xa)
    show "i N \<Longrightarrow> x N \<Longrightarrow> xa N \<Longrightarrow> cpi' (S S xa) (S x) < (S x) = 1 \<Longrightarrow> cpi' (S S S xa) (S x) < (S x) = 1"
      apply (unfold_def cpi'_def, simp)
      apply (rule le_less_trans[where b="cpi' (S S xa) (S x)"], simp+)
      done
qed

lemma cpair_surjective [auto]: "a N \<Longrightarrow> \<exists>b c. a = \<langle>b,c\<rangle>"
sorry

lemma "a N \<Longrightarrow> b N \<Longrightarrow> x = \<langle>a,b\<rangle> \<Longrightarrow> cpx x = a"
by (subst "\<langle>a,b\<rangle> = x", simp)

lemma "a N \<Longrightarrow> b N \<Longrightarrow> x = \<langle>a,b\<rangle> \<Longrightarrow> cpy x = b"
by (subst "\<langle>a,b\<rangle> = x", simp)

lemma [auto]: "x N \<Longrightarrow> x = \<langle>cpx x, cpy x\<rangle>"
apply (rule existsE[where Q="\<lambda>b. x=\<langle>cpx x,b\<rangle>"])
apply (rule existsE[where Q="\<lambda>c. \<exists>i. x=\<langle>c,i\<rangle>"])
apply (simp)
proof -
  fix a
  show "x N \<Longrightarrow> a N \<Longrightarrow> \<exists>i. x = \<langle>a,i\<rangle> \<Longrightarrow> \<exists>i. x = \<langle>cpx x,i\<rangle>"
    apply (subst "a = cpx x")
    apply (rule existsE[where Q="\<lambda>i. x=\<langle>a,i\<rangle>"])
    apply (simp+)
    done
  show "x N \<Longrightarrow> a N \<Longrightarrow> x = \<langle>cpx x,a\<rangle> \<Longrightarrow> x = \<langle>cpx x,cpy x\<rangle>"
    apply (subst "a = cpy x")
    apply (subst "\<langle>cpx x,a\<rangle> = x")
    apply (subst rule: cpy_proj)
    done
qed

lemma cpair_eq_I: "x N \<Longrightarrow> a N \<Longrightarrow> b N \<Longrightarrow> cpx x = a \<Longrightarrow> cpy x = b \<Longrightarrow> x = \<langle>a,b\<rangle>"
by (subst "cpx x = a", subst "cpy x = b")

lemma cp4_reconstr: "x N \<Longrightarrow> a N \<Longrightarrow> b N \<Longrightarrow> c N \<Longrightarrow> d N \<Longrightarrow> cpi 1 x = a \<Longrightarrow> cpi 2 x = b \<Longrightarrow>
       cpi 3 x = c \<Longrightarrow> cpi' 4 x = d \<Longrightarrow>
       x = \<langle>a,b,c,d\<rangle>"
apply (rule cpair_eq_I, simp)
apply (subst "cpi 1 x = cpx x", auto)
apply (rule cpair_eq_I, simp)
apply (subst "cpi 2 x = cpx (cpy x)", auto)
apply (rule cpair_eq_I, simp)
apply (subst "cpi 3 x = cpx (cpy (cpy x))", auto)
apply (subst "cpi' 4 x = cpy (cpy (cpy x))", auto)
done

text "A manual construction of an inductive datatype.
  Later, we want this to be generated automatically from something
  like \<open>declaretype List = Nil | Cons of \<open>nat\<close> \<open>List\<close>\<close>."

type_synonym List = num

definition list_type_tag where
  "list_type_tag \<equiv> 1"

definition list_nil_tag where
  "list_nil_tag \<equiv> 1"

definition list_cons_tag where
  "list_cons_tag \<equiv> 2"

definition Nil :: "List" where
  "Nil \<equiv> \<langle>list_type_tag,list_nil_tag\<rangle>"

definition Cons :: "num \<Rightarrow> List \<Rightarrow> List" where
  "Cons n xs \<equiv> \<langle>list_type_tag,list_cons_tag,n,xs\<rangle>"

axiomatization
  is_list :: "num \<Rightarrow> o" and
  is_cons :: "num \<Rightarrow> o"
where
  is_cons_def: "is_cons x := (cpi 1 x = list_type_tag)
                              \<and> (cpi 2 x = list_cons_tag)
                              \<and> ((cpi 3 x) N)
                              \<and> (is_list (cpi' 4 x))" and
  is_list_def: "is_list x := if x = 0
                               then False
                             else if x = Nil
                               then True
                             else if is_cons x
                               then True
                             else False"

lemma [simp]: "list_type_tag = 1"
unfolding list_type_tag_def by simp

lemma [simp]: "list_nil_tag = 1"
unfolding list_nil_tag_def by simp

lemma [simp]: "list_cons_tag = 2"
unfolding list_cons_tag_def by simp

lemma nil_nat [auto]: "Nil N"
unfolding Nil_def list_type_tag_def by simp

lemma cons_nat [auto]: "n N \<Longrightarrow> xs N \<Longrightarrow> Cons n xs N"
unfolding Cons_def list_type_tag_def by simp

lemma list_cons_term [auto]: "x N \<Longrightarrow> (is_list x B) \<and> (is_cons x B)"
proof (induct strong x)
  case Base
    show "x N \<Longrightarrow> (is_list 0 B) \<and> (is_cons 0 B)"
      apply (unfold_def is_list_def)
      apply (unfold_def is_cons_def)
      apply (unfold_def is_list_def)
      apply (simp)
      done
next
  case (Step xa)
    fix y
    assume hyp: "(\<And>y. y N \<Longrightarrow> y \<le> xa = 1 \<Longrightarrow> (is_list y B) \<and> (is_cons y B))"
    from Step show ?case
      apply (unfold_def is_list_def)
      apply (unfold_def is_cons_def)
      apply (simp)
      apply (rule condTB, simp)+
      apply (rule conjE1, rule hyp, simp, rule le_suc_implies_leq, simp)+
      done
qed

lemma is_list_terminates [auto]: "x N \<Longrightarrow> is_list x B"
by (rule conjE1, rule list_cons_term, simp)

lemma is_cons_terminates [auto]: "x N \<Longrightarrow> is_cons x B"
by (rule conjE2, rule list_cons_term, simp)

lemma [auto]: "\<not> Nil = 0"
unfolding Nil_def by simp

lemma [auto]: "\<not> is_list 0"
by (unfold_def is_list_def, simp)

lemma [auto]: "is_list Nil"
by (unfold_def is_list_def, simp)

lemma [auto]: "n N \<Longrightarrow> xs N \<Longrightarrow> \<not> Nil = Cons n xs"
unfolding Nil_def Cons_def by simp

lemma [auto]: "n N \<Longrightarrow> xs N \<Longrightarrow> \<not> Cons n xs = Nil"
unfolding Nil_def Cons_def by simp

lemma cons_1_tag: "is_cons x \<Longrightarrow> list_type_tag = cpi 1 x"
apply (rule eqSym)
apply (rule conjE1, rule conjE1, rule conjE1)
apply (fold_def is_cons_def, simp)
done

lemma cons_2_2: "is_cons x \<Longrightarrow> list_cons_tag = cpi 2 x"
apply (rule eqSym)
apply (rule conjE2, rule conjE1, rule conjE1)
apply (fold_def is_cons_def, simp)
done

lemma "is_cons x \<Longrightarrow> (cpi 3 x) N"
apply (rule conjE2, rule conjE2)
apply (rule and_assoc, rule conjE1)
apply (fold_def is_cons_def, simp)
done

lemma [cond]: "is_cons x \<Longrightarrow> is_list (cpi' 4 x)"
apply (rule conjE2)
apply (fold_def is_cons_def, simp+)
done

lemma cons_decode [auto]:
  "is_cons x \<Longrightarrow> x N \<Longrightarrow> \<exists>n xs. ((n N) \<and> is_list xs \<and> x = Cons n xs)"
apply (rule existsI[where a="cpi 3 x"], simp+)
apply (rule existsI[where a="cpi' 4 x"], simp+)
apply (unfold Cons_def)
apply (subst rule: cons_1_tag)
apply (subst rule: cons_2_2)
apply (rule cp4_reconstr, simp+)
done

lemma [auto]: "n N \<Longrightarrow> xs N \<Longrightarrow> \<not> 0 = Cons n xs"
unfolding Nil_def Cons_def by simp

lemma [auto]: "n N \<Longrightarrow> xs N \<Longrightarrow> is_list xs \<Longrightarrow> is_cons (Cons n xs)"
unfolding Cons_def by (unfold_def is_cons_def, simp)

lemma cons_is_list [auto]:
  "n N \<Longrightarrow> xs N \<Longrightarrow> is_list xs \<Longrightarrow> is_list (Cons n xs)"
apply (unfold_def is_list_def)
apply (unfold_def is_cons_def)
apply (unfold Cons_def)
apply (simp)
done

lemma
  "n N \<Longrightarrow> m N \<Longrightarrow> xs N \<Longrightarrow> ys N \<Longrightarrow> Cons n xs = Cons m ys \<Longrightarrow> n = m \<and> xs = ys"
unfolding Cons_def
apply (rule cpair_inj)
apply (rule cpair_inj_r, rule cpair_inj_r, simp)
done

lemma list_cases: "x N \<Longrightarrow> is_list x \<Longrightarrow> (x = Nil) \<or> (\<exists>n xs. (n N) \<and> is_list xs \<and> (x = Cons n xs))"
apply (rule implE[where a="is_list x"])
apply (unfold_def is_list_def)
apply (cases bool: "x=Nil", simp+)
apply (rule implI, simp)
apply (rule disjI1, simp)
apply (cases bool: "is_cons x", simp+)
apply (rule implI)
apply (rule condTB, simp)+
apply (simp+)
apply (rule implI, simp)
apply (rule exF[where P="False"], simp)
done

lemma cases_list [case_names _ HQ Nil Cons, cases]: "is_list x \<Longrightarrow>
       (x N) \<Longrightarrow>
       (x = Nil \<Longrightarrow> Q) \<Longrightarrow>
       (\<And>n xs. n N \<Longrightarrow> xs N \<Longrightarrow> is_list xs \<Longrightarrow> x = Cons n xs \<Longrightarrow> Q)
       \<Longrightarrow> Q"
apply (rule disjE1[OF list_cases], simp, assumption)
apply (rule existsE[where Q="\<lambda>n. \<exists>xs. (n N) \<and> is_list xs \<and> x = Cons n xs"])
apply (assumption)
proof -
  fix a
  show "is_list x \<Longrightarrow>
     (x = Nil \<Longrightarrow> Q) \<Longrightarrow>
     (\<And>n xs. n N \<Longrightarrow> xs N \<Longrightarrow> is_list xs \<Longrightarrow> x = Cons n xs \<Longrightarrow> Q) \<Longrightarrow>
     \<exists>n xs. (n N) \<and> is_list xs \<and> x = Cons n xs \<Longrightarrow>
     a N \<Longrightarrow> \<exists>xs. (a N) \<and> is_list xs \<and> x = Cons a xs \<Longrightarrow> Q"
    apply (rule existsE[where Q="\<lambda>xs. (a N) \<and> is_list xs \<and> x = Cons a xs"])
    apply (assumption)
    proof -
      fix aa
      show "
      (\<And>n xs. n N \<Longrightarrow> xs N \<Longrightarrow> is_list xs \<Longrightarrow> x = Cons n xs \<Longrightarrow> Q) \<Longrightarrow>
        aa N \<Longrightarrow> (a N) \<and> is_list aa \<and> x = Cons a aa \<Longrightarrow> Q"
        apply (rule Pure.meta_mp[where P="a N"])
        apply (rule Pure.meta_mp[where P="is_list aa"])
        apply (rule Pure.meta_mp[where P="x = Cons a aa"])
        apply (assumption)
        apply (rule conjE2, simp)
        apply (rule conjE2, rule conjE1, simp)
        apply (rule conjE1, rule conjE1, simp)
        done
    qed
qed

lemma [simp]: "x N \<Longrightarrow> is_list x \<Longrightarrow> x = 0 \<longleftrightarrow> False"
apply (rule iffI, simp+)
apply (rule exF[where P="is_list 0"], simp)
apply (rule exF[where P="False"], simp)
done

lemma [simp]: "xs N \<Longrightarrow> is_list xs \<Longrightarrow> n N \<Longrightarrow> xs < Cons n xs = 1"
unfolding Cons_def by simp

lemma obj_impl: "Q a \<longrightarrow> R a \<Longrightarrow> Q a \<Longrightarrow> R a"
by (rule implE[where a="Q a"], simp)

lemma obj_univ_impl: "\<forall>a. Q a \<longrightarrow> R a \<Longrightarrow> x N \<Longrightarrow> Q x \<Longrightarrow> R x"
apply (rule implE[where a="Q x"])
apply (rule forallE, simp)
done

lemma [case_names _ HQ Nil Cons, induct]:
  "is_list a \<Longrightarrow> a N \<Longrightarrow> Q Nil \<Longrightarrow> (\<And>x xs. x N \<Longrightarrow> xs N \<Longrightarrow> is_list xs \<Longrightarrow> Q xs \<Longrightarrow> Q (Cons x xs))
   \<Longrightarrow> Q a"
apply (rule implE[where a="is_list a"])
apply (induct strong a)
apply (rule implI, simp)
apply (rule exF[where P="is_list 0"], simp)
apply (rule implI, simp)
proof -
  fix xa
  assume hyp: "(\<And>y. y N \<Longrightarrow> y \<le> xa = 1 \<Longrightarrow> is_list y \<longrightarrow> Q y)"
  assume cons: "(\<And>x xs. x N \<Longrightarrow> xs N \<Longrightarrow> is_list xs \<Longrightarrow> Q xs \<Longrightarrow> Q (Cons x xs))"
  show "a N \<Longrightarrow> xa N \<Longrightarrow> is_list S xa \<Longrightarrow> Q Nil \<Longrightarrow>
        Q S xa"
    proof (cases "S xa", simp)
      case Nil
        from Nil show ?case
          by (simp+)
    next
      case (Cons n xs)
        from Cons and cons show ?case
          apply (simp)
          apply (rule cons, simp)
          apply (rule obj_impl)
          apply (rule hyp, simp)
          apply (rule le_suc_implies_leq, simp+)
          done
    qed
qed

(*
 fun sum :: "List \<Rightarrow> num" where
   sum_nil: "sum Nil = 0" and
   sum_cons: "sum (Cons n xs) = n + sum xs"
 *)

axiomatization
  sum :: "List \<Rightarrow> num"
where
  sum_def: "sum x := if x = Nil then 0
                     else if (is_cons x) then (cpi 3 x) + (sum (cpi' 4 x))
                     else omega"

lemma [simp]: "is_list 0 \<Longrightarrow> False"
by (rule exF[where P="is_list 0"], simp)

lemma [auto]: "x N \<Longrightarrow> is_list x \<Longrightarrow> sum x N"
proof (induct x, simp)
  case Nil
  show ?case
    by (unfold_def sum_def, simp add: sum_def)
next
  case (Cons n xs)
  from Cons show ?case
    apply (unfold_def sum_def)
    apply (subst rule: condI2)
    apply (subst rule: condI1)
    apply (unfold Cons_def, simp+)
    apply (unfold_def is_cons_def, simp)
    done
qed

lemma [simp]: "sum Nil = 0"
by (unfold_def sum_def, simp)

lemma [simp]: "n N \<Longrightarrow> xs N \<Longrightarrow> is_list xs \<Longrightarrow> sum (Cons n xs) = n + sum xs"
apply (rule eqSym)
apply (unfold_def sum_def)
apply (unfold_def is_cons_def)
apply (unfold Cons_def Nil_def, simp)
done

lemma "sum (Cons 4 (Cons 3 (Nil))) = 7"
apply (simp)
apply (unfold_def add_def)
apply (unfold_def add_def)
apply (simp)
done

lemma "is_list (Cons 4 (Cons 3 (Nil)))"
by simp

(*
declaretype num =
  Zero
  | Suc of "num"

declaretype list =
  nil
  | cons of "num" "list"
*)

axiomatization
  ack :: "num \<Rightarrow> num \<Rightarrow> num"
where
  ack_def: "ack x y := if x = 0 then y + 1
                       else if y = 0 then ack (P x) 1
                       else ack (P x) (ack x (P y))"

lemma [simp]: "n N \<Longrightarrow> ack 0 n = n + 1"
by (unfold_def ack_def, simp)

lemma "n N \<Longrightarrow> m N \<Longrightarrow> ack m n N"
apply (rule forallE[where a="n"])
apply (induct m)
apply (rule forallI, simp)
apply (rule forallI)
proof -
  fix x z
  show "x N \<Longrightarrow> \<forall>y. ack x y N \<Longrightarrow> z N \<Longrightarrow> ack (S x) z N"
    apply (induct z)
    apply (unfold_def ack_def)
    apply (subst rule: condI2)
    apply (subst rule: condI1)
    apply (rule forallE[where a="1"], simp)
    apply (rule forallE[where a="1"], simp)
    apply (subst rule: condI1)
    apply (rule forallE[where a="1"], simp)
    apply (rule forallE[where a="1"], simp)
    apply (unfold_def ack_def)
    apply (subst rule: condI2, simp)
    apply (subst rule: condI2)
    apply (rule forallE, simp)+
    apply (rule forallI, simp+)
    apply (rule forallE, simp)
    done
qed

lemma "a \<longleftrightarrow> b \<Longrightarrow> (Trueprop a) \<equiv> (Trueprop b)"
apply (rule Pure.equal_intr_rule)
apply (unfold iff_def)
apply (rule implE, rule conjE1, assumption+)
apply (rule implE, rule conjE2, assumption+)
done

lemma "a = b \<Longrightarrow> Q b \<Longrightarrow> Q a"
apply (rule eqSubst[where a="b" and b="a"])
apply (rule eqSym)
apply (assumption+)
done

end (* End of theory *)