section \Solutions for Session 10\ theory Solutions10 imports Demo10 begin subsection \Exercise 1\ text \ Given the data type \ datatype 'a btree = Empty | Node 'a "'a btree" "'a btree" text \ Define notation that allows you to write for example \<<>,1,<<3>,2,<>>>\ instead of \Node 1 Empty (Node 2 (Node 3 Empty Empty) Empty)\ In the output you may further compress the representation to \<1,<<3>,2>>\ \ notation Empty ("<>") nonterminal elts syntax "" :: "logic \ elts" ("_") "_elts" :: "logic \ elts \ elts" ("_,_") syntax "_btree" :: "elts \ 'a btree" ("<_>") translations "<<>,x,<>>" \ "CONST Node x <> <>" "<<>,x,>" \ "CONST Node x <> " "<,y,<>>" \ "CONST Node y <>" "<<>,x>" \ "CONST Node x <> <>" ">" \ "CONST Node x <> <>" "<,y,>" \ "CONST Node y " ">" \ "CONST Node x <> " "<,y>" \ "CONST Node y <>" "" \ "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 "<,A,>>" subsection \Exercise 2\ text \ Write a @{class to_string} instance for @{typ nat}. \ definition digit :: "nat \ 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 \ STRING \ 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 \ STRING" where "to_string_nat n = append_nat n []" instance .. end value "show (CHR ''c'', 1340::nat, ''heya!'')" subsection \Exercise 3\ text \ Given the inductive definition of \LT_nat\ below, prove that it coincides with @{term "(\<^bold><) :: nat \ nat \ bool"}. \ inductive LT_nat :: "nat \ nat \ bool" where [simp]: "LT_nat 0 (Suc y)" | "LT_nat x y \ 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) \ LT_nat x y" by (auto intro: LT_nat.intros elim: LT_nat.cases) lemma LT_nat_LT_conv [simp]: "x \<^bold>< y \ LT_nat x y" proof assume "x \<^bold>< y" then have "x \<^bold>\ y" and "x \ 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