theory week06A_demo_soln imports Main begin -- ----------------------------------------------------------------------- -- {* a recursive data type: *} datatype ('a,'b) tree = Tip | Node "('a,'b) tree" 'b "('a,'b) tree" print_theorems -- {* distincteness of constructors automatic: *} lemma "Tip ~= Node l x r" by simp -- {* case sytax, case distinction manual *} lemma "(1::nat) \ (case t of Tip \ 1 | Node l x r \ x+1)" apply(case_tac t) apply auto done -- {* partial cases and dummy patterns: *} term "case t of Node _ b _ => b" -- {* partial case maps to 'undefined': *} lemma "(case Tip of Node _ _ _ => 0) = undefined" by simp -- {* nested case and default pattern: *} term "case t of Node (Node _ _ _) x Tip => 0 | _ => 1" -- {* inifinitely branching: *} datatype 'a inftree = Tp | Nd 'a "nat \ 'a inftree" -- {* mutually recursive *} datatype ty = Integer | Real | RefT ref and ref = Class | Array ty -- ----------------------------------------------------------------- -- {* primitive recursion *} primrec app :: "'a list => 'a list => 'a list" where "app Nil ys = ys" | "app (Cons x xs) ys = Cons x (app xs ys)" print_theorems primrec rv :: "'a list => 'a list" where "rv [] = []" | "rv (x#xs) = app (rv xs) [x]" -- {* on trees *} primrec mirror :: "('a,'b) tree => ('a,'b) tree" where "mirror Tip = Tip" | "mirror (Node l x r) = Node (mirror r) x (mirror l)" print_theorems -- {* mutual recursion *} primrec has_int :: "ty \ bool" and has_int_ref :: "ref \ bool" where "has_int Integer = True" | "has_int Real = False" | "has_int (RefT T) = has_int_ref T" | "has_int_ref Class = False" | "has_int_ref (Array T) = has_int T" -- ------------------------------------------------------------------ -- {* structural induction *} -- {* discovering lemmas needed to prove a theorem *} lemma app_nil: "app xs [] = xs" apply (induct xs) apply auto done lemma app_app: "app (app xs ys) zs = app xs (app ys zs)" apply (induct xs) apply auto done lemma rv_app: "rv (app xs ys) = app (rv ys) (rv xs)" apply (induct xs arbitrary: ys) apply (simp add: app_nil) apply (auto simp: app_app) done theorem rv_rv: "rv (rv xs) = xs" apply (induct xs) apply (auto simp: rv_app) done -- {* induction heuristics *} primrec itrev :: "'a list \ 'a list \ 'a list" where "itrev [] ys = ys" | "itrev (x#xs) ys = itrev xs (x#ys)" lemma itrev_rev_app: "itrev xs ys = rev xs @ ys" apply (induct xs arbitrary: ys) apply auto done lemma "itrev xs [] = rev xs" apply (induct xs) apply simp apply (clarsimp simp: itrev_rev_app) done -- ------------------------------------------------------------------ primrec lsum :: "nat list \ nat" where "lsum [] = 0" | "lsum (x#xs) = x + lsum xs" lemma lsum_app: "lsum (xs @ ys) = lsum xs + lsum ys" by (induct xs arbitrary: ys, auto) lemma "2 * lsum [0 ..< Suc n] = n * (n + 1)" apply (induct n) apply (auto simp: lsum_app) done lemma "lsum (replicate n a) = n * a" apply (induct n) apply simp apply simp done -- {* tail recursive version: *} primrec lsumT :: "nat list \ nat \ nat" where "lsumT [] s = s" | "lsumT (x#xs) s = lsumT xs (x + s)" lemma lsumT_gen: "lsumT xs s = lsum xs + s" by (induct xs arbitrary: s, auto) lemma lsum_correct: "lsumT xs 0 = lsum xs" by (simp add: lsumT_gen) end