theory Demo4 imports Main begin datatype 'a tree = Leaf 'a | Node "'a tree list" fun f and g where "f (Leaf x) = [x]" | "f (Node lst) = g lst" | "g [] = []" | "g (t1 # ts) = (f t1) @ g ts" thm f_g.induct (*and 'a nlist = One "'a tree" | More "'a tree" "'a tree nlist"*) section{* How to simplify *} text{* No assumption: *} lemma "ys @ [] = []" proof simp oops (* abandon proof *) text{* Simple assumption: *} lemma "xs = [] \ xs @ ys = ys @ xs @ ys" proof (simp) oops; text{* Simplification in assumption: *} lemma "\ xs @ zs = ys @ xs; [] @ xs = [] @ [] \ \ ys = zs" proof(simp) qed; lemma assumes H1:"xs @ zs = ys @ xs" and H2:"[] @ xs = [] @ []" shows "ys = zs" using H1 and H2 proof (simp) qed; text{* This assumption would lead to nontermination. (Note that ALL binds stronger than ==>) *} lemma "\ x. f x = g x \ g x = f x \ f [] = f [] @ []" (* Would diverge: proof(simp) *) proof(simp (no_asm)) qed thm distrib_right distrib_left right_diff_distrib text{* Using additional rules: *} lemma "(a+b)*(a-b) = a*a - b*(b\int)" proof (simp add: distrib_right distrib_left right_diff_distrib) qed text{* Giving a lemma the simp-attribute: *} declare distrib_right distrib_left right_diff_distrib [simp] subsection{* Rewriting with definitions *} (* Old syntax; still works constdefs exor \ "bool \ bool => bool" "exor x y == x & y | ~x & ~y" nand :: "bool => bool => bool" "nand x y == ~(x & y)"; *) definition exor :: "bool \ bool \ bool" where "exor x y \ x \ y | \x \ \y" definition nand :: "bool => bool => bool" where "nand x y \ \(x & y)"; text{* Unfolding + simplification: *} lemma "exor x x = nand x (\x)" proof(unfold exor_def nand_def) show "(x \ x \ \ x \ \ x) = (\ (x \ \ x))" proof(simp) qed qed text{* Just simplification: *} lemma "exor x x = nand x (\x)" proof(simp add: exor_def nand_def) qed subsection{* Case distinctions *} text{* Automatic: *} lemma "(A \ B) = (if A then B else False)" proof(simp) qed lemma "if A then B else C" proof(simp) oops text{* By hand (for case): *} lemma "x = (case x of 0 \ n | Suc y \ y+y)" proof(simp split: nat.split) oops; subsection {* Arithmetic *} text{* A bit of linear arithmetic (no multiplication) is automatic: *} lemma "\(x::nat) \ y+z; z+x < y \ \ x < y" proof(simp) qed subsection{* Tracing: *} lemma "rev[x] = []" proof(simp) oops subsection{* Auto *} text{* Method ``auto'' can be modified almost like ``simp'': instead of ``add'' use ``simp add'': *} lemma "(\ u::nat. x=y+u) \ a*(b+c)+y \ x + a*b+a*c" proof(auto simp add: add_mult_distrib2) qed end