theory week05B_demo imports Main begin \ \ ----------------------------------------------------------------\ text \a recursive data type: \ datatype ('a,'b) tree = Tip | Node "('a,'b) tree" 'b "('a,'b) tree" print_theorems text \ distinctness of constructors automatic: \ lemma "Tip ~= Node l x r" by simp text \ case syntax, case distinction manual \ lemma "(1::nat) \ (case t of Tip \ 1 | Node l x r \ x+1)" apply(case_tac t) apply auto done text \ partial cases and dummy patterns: \ term "case t of Node _ b _ => b" text \ partial case maps to 'undefined': \ lemma "(case Tip of Node _ _ _ => 0) = undefined" by simp text \ nested case and default pattern: \ term "case t of Node (Node _ _ _) x Tip => 0 | _ => 1" text \ infinitely branching: \ datatype 'a inftree = Tp | Nd 'a "nat \ 'a inftree" text \ mutually recursive \ datatype ty = Integer | Real | RefT ref and ref = Class | Array ty \ \ ----------------------------------------------------------------\ text \ 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]" text \ 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 text \ 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" \ \ ----------------------------------------------------------------\ text \ structural induction \ text \ discovering lemmas needed to prove a theorem \ theorem rv_rv: "rv (rv xs) = xs" apply (induct xs) oops text \ 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 text \ tail recursive version: \ primrec lsumT :: "nat list \ nat \ nat" where "lsumT [] s = ?" lemma lsum_correct: "lsumT xs 0 = lsum xs" oops end