(*<*)theory BigNat imports Main begin(*>*)

text {*
  Hardware-Plattformen haben ein Limit, welches die gr\"o{\ss}te darstellbare Zahl
  ist; dies ist normalerweise durch die Bitl\"ange der verwendeten Register und ALU
  festgelegt. Um mit beliebig gro{\ss}en Zahlen rechnen zu k\"onnen, m\"ussen
  die entsprechenden arithmetischen Operationen erweitert werden, um auf
  abstrakten Datentypen, welche Zahlen beliebiger Gr\"o{\ss}e repr\"asentieren,
  arbeiten zu k\"onnen.

  Wir werden im folgenden eine Implementation f\"ur BigNat, einen abstrakten 
  Datentypen zur Darstellung von nat\"urlichen Zahlen beliebiger Gr\"o{\ss}e,
  erstellen und verifizieren.

  \section*{Darstellung}

  Ein BigNat wird als Liste von nat\"urlichen Zahlen innerhalb eines von
  der Zielmaschine unterst\"utzten Bereichs dargestellt. In unserem Fall
  sind das alle nat\"urlichen Zahlen im Bereich [0, Basis-1] (den Sonderfall,
  dass die Basis 1 ist, k\"onnen wir f\"ur diese Aufgabe ignorieren). In Isabelle 
  selbst sind nat\"urliche Zahlen von beliebiger Gr\"o{\ss}e.*}

types bigNat = "nat list"

text {* Definieren Sie jetzt zwei Funktionen: @{text valid}, welche einen Wert f\"ur
  die Basis nimmt und pr\"uft, ob der gegebene BigNat daf\"ur g\"ultig ist, und 
  @{text val}, welches mittels eines BigNats und seiner Basis die entsprechend 
  dargestellte Zahl zur\"uckgibt. Beachten Sie: wenn die Basis nicht gr\"o{\ss}er
  als 1 ist, darf die Zahl auch nicht in dieser Basis g\"ultig sein. *}

consts 
  valid :: "nat \<Rightarrow> bigNat \<Rightarrow> bool"
  val :: "nat \<Rightarrow> bigNat \<Rightarrow> nat"

text {*
  \section*{Addition}

  Definieren Sie jetzt eine Funktion @{text add}, welche zwei BigNats mit der selben
  Basis addiert. Stellen Sie sicher, dass ihr Algorihmus die G\"ultigkeit der 
  BigNat-Darstellung beibeh\"alt. Beweisen Sie danach mittels @{text val} und
  @{text valid}, dass der Algorithmus das korrekte Resultat berechnet und die
  G\"ultigkeit der Darstellung beibeh\"alt.*}

consts
  add :: "nat \<Rightarrow> bigNat \<Rightarrow> bigNat \<Rightarrow> bigNat"

lemma add_valid: "\<lbrakk>valid d ns; valid d ms\<rbrakk> \<Longrightarrow> valid d (add d ns ms)"
oops

text {* Eventuell brauchen Sie in folgenden Lemma die Voraussetzungen 
  @{term "valid d ns"} und @{term "valid d ms"} *}

lemma add_val: "val d (add d ns ms) = val d ns + val d ms"
oops

text {* 
  \section*{Multiplikation}

  Jetzt sollen Sie analog zur Addition auch noch die Multiplikation definieren
  und die entsprechenden Lemmas f\"ur @{text valid} und @{text val} zeigen.
  Erinnern Sie sich an die normale Papiermultiplikation, die Sie in der
  Schule gelernt haben, vergessen Sie dabei aber das Shiften um eine Stelle nicht!*}

consts
  mult :: "nat \<Rightarrow> bigNat \<Rightarrow> bigNat \<Rightarrow> bigNat"

lemma mult_valid: "\<lbrakk>valid d ns; valid d ms\<rbrakk> \<Longrightarrow> valid d (mult d ns ms)"
oops

text {* Auch hier k\"onnte wieder die Forderung nach g\"ultigen Zahlen n\"otig sein *}

lemma mult_val: "val d (mult d ns ms) = val d ns * val d ms"
oops

text {*
  \section*{Hinweise}

  Machen sie sich Gedanken, ob Sie die Zahldarstellung in ``big endian'' oder 
  ``little endian'' machen m\"ochten, mit einer der beiden ist deutlich angenehmer
  zu arbeiten als mit der anderen.

  Versuchen Sie ihre Beweise in einem m\"oglichst klaren Isar-Skript darzustellen. 

  Verwenden Sie f\"ur ihre Definitionen die Funktionen @{text div} und @{text mod},
  die sich in Isabelle wie erwartet verhalten; z.B. wird die Aussage
  @{term "d \<le> b \<longrightarrow> b mod d + d * (b div d) = b"} f\"ur nat\"urliche Zahlen
  durch einfache Anwendung des Simplifiers gel\"ost.

  Folgende Aussagen werden in den Beweisen wahrscheinlich zur L\"osung ben\"otigt
  werden, sie sind hier mit einem Beweis angegeben. Sie m\"ussen sie also nur noch 
  an die ben\"otigte Stelle kopieren (oder Sie beweisen sie selbst). *}

lemma less_sqr_div_less: "m < d * d \<Longrightarrow> m div d < (d::nat)"
(*<*)proof(rule ccontr)
  assume m:"m < d * d" and "\<not> m div d < d"
  hence "d \<le> m div d" by simp
  hence le:"d * d \<le> d * (m div d)" by simp
  have "d * (m div d) \<le> m" by (simp add: mult_div_cancel)
  with le have "d * d \<le> m" by(rule le_trans)
  with m show False by simp
qed(*>*)

lemma less_less_add_div_less:
  "\<lbrakk>a < d; b < d\<rbrakk> \<Longrightarrow> (a + b) div d < (d::nat)"
(*<*)proof -
  assume a: "a < d" "b < d"
  { assume "d = 0" with a have ?thesis by simp }
  moreover
  { assume "d = 1" with a have ?thesis by simp }
  moreover
  { from a have "a + b < 2 * d" by simp
    also assume "2 \<le> d" then have "2 * d \<le> d * d" by simp
    finally have "a + b < d * d" .
    then have "(a + b) div d  < d" by (rule less_sqr_div_less)
  }
  ultimately show ?thesis by arith
qed(*>*)

lemma less_less_less_add_div_less:
  "\<lbrakk>a < d; b < d; c < d\<rbrakk> \<Longrightarrow> (a + b + c) div d < (d::nat)"
(*<*)proof -
  assume a: "a < d" "b < d" "c < d"
  { assume "d = 0" with a have ?thesis by simp }
  moreover
  { assume "d = 1" with a have ?thesis by simp }
  moreover
  { assume "d = 2" with a have ?thesis by(cases a,auto) }
  moreover
  { from a have "a + b + c < 3 * d" by simp
    also assume "3 \<le> d" then have "3 * d \<le> d * d" by simp
    finally have "a + b + c < d * d" .
    then have "(a + b + c) div d  < d" by (rule less_sqr_div_less)
  }
  ultimately show ?thesis by arith
qed(*>*)

lemma le_le_le_add_mult_div_Suc_le: 
  "\<lbrakk>a \<le> d; b \<le> d; c \<le> d\<rbrakk> \<Longrightarrow> (a * b + c) div (Suc d) \<le> d"
(*<*)proof -
  assume a:"a \<le> d" and b:"b \<le> d" and c:"c \<le> d"
  then have d:"a * b + c \<le> d * d + d" 
    by (auto intro: add_le_mono mult_le_mono)
  then have e:"d * d + d = d * (Suc d)" by clarsimp
  from d have f:"(a * b + c) div (Suc d) \<le> (d * Suc d) div (Suc d)" 
    by (auto simp:e intro:div_le_mono)
  have "(d * Suc d) div (Suc d) = d" by (simp only:div_mult_self_is_m)
  with f show ?thesis by simp
qed(*>*)

lemma less_less_less_add_mult_div_less: 
  "\<lbrakk>a < d; b < d; c < d\<rbrakk> \<Longrightarrow> (a * b + c) div d < (d::nat)"
(*<*)proof(cases d)
  case 0
  assume "a < d" "d = 0"
  thus ?thesis by simp
next
  case (Suc d')
  assume "d = Suc d'" "a < d" "b < d" "c < d"
  thus ?thesis
    by(fastsimp intro:less_Suc_eq_le[THEN iffD2] le_le_le_add_mult_div_Suc_le
                dest:less_Suc_eq_le[THEN iffD1])
qed(*>*)

text {* An einigen Stellen werden Sie dem Simplifier mit einem der folgenden Lemmas
  auf die Spr\"unge helfen m\"ussen:
  \begin{center}
  @{text "add_mult_distrib:"}~@{thm add_mult_distrib[no_vars]}\\
  @{text "add_mult_distrib2:"}~@{thm add_mult_distrib2[no_vars]}
  \end{center}
  *}

(*<*)end(*>*)