theory week06A_demo imports Main begin -- ----------------------------------------------------------------------- -- {* a recursive data type: *} datatype ('a,'b) tree = Tip | Node "('a,'b) tree" 'b "('a,'b) tree" print_theorems -- {* distinctness 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 *} theorem rv_rv: "rv (rv xs) = xs" apply (induct xs) oops -- {* induction heuristics *} primrec itrev :: "'a list \ 'a list \ 'a list" where "itrev [] ys = ys" | "itrev (x#xs) ys = itrev xs (x#ys)" lemma "itrev xs [] = rev xs" oops -- ------------------------------------------------------------------ primrec lsum :: "nat list \ nat" where "lsum [] = 0" | "lsum (x#xs) = x + lsum xs" lemma "2 * lsum [0 ..< Suc n] = n * (n + 1)" oops lemma "lsum (replicate n a) = n * a" oops -- {* tail recursive version: *} primrec lsumT :: "nat list \ nat \ nat" where "lsumT [] s = ?" lemma lsum_correct: "lsumT xs 0 = lsum xs" oops end