section \<open>Solutions for Session 10\<close>

theory Solutions10
  imports Demo10
begin

subsection \<open>Exercise 1\<close>

text \<open>
Given the data type
\<close>
datatype 'a btree = Empty | Node 'a "'a btree" "'a btree"
text \<open>
Define notation that allows you to write for example

  \<open><<>,1,<<3>,2,<>>>\<close>

instead of

  \<open>Node 1 Empty (Node 2 (Node 3 Empty Empty) Empty)\<close>

In the output you may further compress the representation to

  \<open><1,<<3>,2>>\<close>
\<close>
notation Empty ("<>")

nonterminal elts

syntax
  "" :: "logic \<Rightarrow> elts" ("_")
  "_elts" :: "logic \<Rightarrow> elts \<Rightarrow> elts" ("_,_")

syntax
  "_btree" :: "elts \<Rightarrow> 'a btree" ("<_>")

translations
  "<<>,x,<>>" \<rightharpoonup> "CONST Node x <> <>"
  "<<>,x,<y>>" \<rightharpoonup> "CONST Node x <> <y>"
  "<<x>,y,<>>" \<rightharpoonup> "CONST Node y <x> <>"
  "<<>,x>" \<rightharpoonup> "CONST Node x <> <>"
  "<x,<>>" \<rightharpoonup> "CONST Node x <> <>"

  "<<x>,y,<z>>" \<rightleftharpoons> "CONST Node y <x> <z>"
  "<x,<y>>" \<rightleftharpoons> "CONST Node x <> <y>"
  "<<x>,y>" \<rightleftharpoons> "CONST Node y <x> <>"
  "<x>" \<rightleftharpoons> "CONST Node x <> <>"


term "<<3,<>>,1,<<>,4>>"
term "<<>,1,<<<6>,3>,2,<<>,4,<5>>>>"

lemma
  "<1,<<<6>,3>,2,<4,<5>>>> = <<>,1,<(<<<>,6,<>>,3,<>>),2,<<>,4,<<>,5,<>>>>>" ..

term "Node 1 (Node 4 (Node 5 <> <>) <>) (Node 2 <> (Node 3 <> <>))"

term "<<B>,A,<C,<D>>>"


subsection \<open>Exercise 2\<close>

text \<open>
Write a @{class to_string} instance for @{typ nat}.
\<close>

definition digit :: "nat \<Rightarrow> char"
  where
    "digit n =
      (if n = 0 then CHR ''0''
      else if n = 1 then CHR ''1''
      else if n = 2 then CHR ''2''
      else if n = 3 then CHR ''3''
      else if n = 4 then CHR ''4''
      else if n = 5 then CHR ''5''
      else if n = 6 then CHR ''6''
      else if n = 7 then CHR ''7''
      else if n = 8 then CHR ''8''
      else if n = 9 then CHR ''9''
      else CHR ''X'')"

fun append_nat :: "nat \<Rightarrow> STRING \<Rightarrow> STRING"
  where
    "append_nat n acc =
      (let d = n div 10 in
      if d = 0 then digit (n mod 10) : acc
      else append_nat d (digit (n mod 10) : acc))"

value "append_nat 13 []"

instantiation nat :: to_string
begin

fun to_string_nat :: "nat \<Rightarrow> STRING"
  where
    "to_string_nat n = append_nat n []"

instance ..

end

value "show (CHR ''c'', 1340::nat, ''heya!'')"


subsection \<open>Exercise 3\<close>

text \<open>
Given the inductive definition of \<open>LT_nat\<close> below, prove that it coincides with
@{term "(\<^bold><) :: nat \<Rightarrow> nat \<Rightarrow> bool"}.
\<close>
inductive LT_nat :: "nat \<Rightarrow> nat \<Rightarrow> bool"
  where
    [simp]: "LT_nat 0 (Suc y)"
  | "LT_nat x y \<Longrightarrow> LT_nat (Suc x) (Suc y)"

lemma LT_0 [simp]:
  "LT_nat x 0 = False"
proof
  assume "LT_nat x 0"
  then show False by (cases)
qed simp

lemma LET_Suc_iff [simp]:
  "LT_nat (Suc x) (Suc y) \<longleftrightarrow> LT_nat x y"
  by (auto intro: LT_nat.intros elim: LT_nat.cases)

lemma LT_nat_LT_conv [simp]:
  "x \<^bold>< y \<longleftrightarrow> LT_nat x y"
proof
  assume "x \<^bold>< y"
  then have "x \<^bold>\<le> y" and "x \<noteq> y" by (auto simp: LT_def)
  then show "LT_nat x y"
  proof (induction x y rule: LEQ_nat.induct)
    case (1 y)
    then obtain n where "y = Suc n" by (cases y) auto
    then show ?case by simp
  qed auto
next
  assume "LT_nat x y"
  then show "x \<^bold>< y"
    by (induction) (auto simp: LT_def)
qed

end