(* Title: HOL/Nitpick_Examples/Manual_Nits.thy Author: Jasmin Blanchette, TU Muenchen Copyright 2009, 2010 Examples from the Nitpick manual. *) header {* Examples from the Nitpick Manual *} (* The "expect" arguments to Nitpick in this theory and the other example theories are there so that the example can also serve as a regression test suite. *) theory Manual_Nits imports Main Quotient_Product RealDef begin chapter {* 3. First Steps *} nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s] subsection {* 3.1. Propositional Logic *} lemma "P \ Q" nitpick [expect = genuine] apply auto nitpick [expect = genuine] 1 nitpick [expect = genuine] 2 oops subsection {* 3.2. Type Variables *} lemma "P x \ P (THE y. P y)" nitpick [verbose, expect = genuine] oops subsection {* 3.3. Constants *} lemma "P x \ P (THE y. P y)" nitpick [show_consts, expect = genuine] nitpick [full_descrs, show_consts, expect = genuine] nitpick [dont_specialize, full_descrs, show_consts, expect = genuine] oops lemma "\!x. P x \ P (THE y. P y)" nitpick [expect = none] nitpick [card 'a = 1\50, expect = none] (* sledgehammer *) apply (metis the_equality) done subsection {* 3.4. Skolemization *} lemma "\g. \x. g (f x) = x \ \y. \x. y = f x" nitpick [expect = genuine] oops lemma "\x. \f. f x = x" nitpick [expect = genuine] oops lemma "refl r \ sym r" nitpick [expect = genuine] oops subsection {* 3.5. Natural Numbers and Integers *} lemma "\i \ j; n \ (m\int)\ \ i * n + j * m \ i * m + j * n" nitpick [expect = genuine] oops lemma "\n. Suc n \ n \ P" nitpick [card nat = 100, check_potential, expect = genuine] oops lemma "P Suc" nitpick [expect = none] oops lemma "P (op +\nat\nat\nat)" nitpick [card nat = 1, expect = genuine] nitpick [card nat = 2, expect = none] oops subsection {* 3.6. Inductive Datatypes *} lemma "hd (xs @ [y, y]) = hd xs" nitpick [expect = genuine] nitpick [show_consts, show_datatypes, expect = genuine] oops lemma "\length xs = 1; length ys = 1\ \ xs = ys" nitpick [show_datatypes, expect = genuine] oops subsection {* 3.7. Typedefs, Records, Rationals, and Reals *} typedef three = "{0\nat, 1, 2}" by blast definition A :: three where "A \ Abs_three 0" definition B :: three where "B \ Abs_three 1" definition C :: three where "C \ Abs_three 2" lemma "\P A; P B\ \ P x" nitpick [show_datatypes, expect = genuine] oops fun my_int_rel where "my_int_rel (x, y) (u, v) = (x + v = u + y)" quotient_type my_int = "nat \ nat" / my_int_rel by (auto simp add: equivp_def expand_fun_eq) definition add_raw where "add_raw \ \(x, y) (u, v). (x + (u\nat), y + (v\nat))" quotient_definition "add\my_int \ my_int \ my_int" is add_raw lemma "add x y = add x x" nitpick [show_datatypes, expect = genuine] oops ML {* fun my_int_postproc _ _ _ T (Const _ $ (Const _ $ t1 $ t2)) = HOLogic.mk_number T (snd (HOLogic.dest_number t1) - snd (HOLogic.dest_number t2)) | my_int_postproc _ _ _ _ t = t *} declaration {* Nitpick_Model.register_term_postprocessor @{typ my_int} my_int_postproc *} lemma "add x y = add x x" nitpick [show_datatypes] oops record point = Xcoord :: int Ycoord :: int lemma "Xcoord (p\point) = Xcoord (q\point)" nitpick [show_datatypes, expect = genuine] oops lemma "4 * x + 3 * (y\real) \ 1 / 2" nitpick [show_datatypes, expect = genuine] oops subsection {* 3.8. Inductive and Coinductive Predicates *} inductive even where "even 0" | "even n \ even (Suc (Suc n))" lemma "\n. even n \ even (Suc n)" nitpick [card nat = 50, unary_ints, verbose, expect = potential] oops lemma "\n \ 49. even n \ even (Suc n)" nitpick [card nat = 50, unary_ints, expect = genuine] oops inductive even' where "even' (0\nat)" | "even' 2" | "\even' m; even' n\ \ even' (m + n)" lemma "\n \ {0, 2, 4, 6, 8}. \ even' n" nitpick [card nat = 10, unary_ints, verbose, show_consts, expect = genuine] oops lemma "even' (n - 2) \ even' n" nitpick [card nat = 10, show_consts, expect = genuine] oops coinductive nats where "nats (x\nat) \ nats x" lemma "nats = {0, 1, 2, 3, 4}" nitpick [card nat = 10, show_consts, expect = genuine] oops inductive odd where "odd 1" | "\odd m; even n\ \ odd (m + n)" lemma "odd n \ odd (n - 2)" nitpick [card nat = 10, show_consts, expect = genuine] oops subsection {* 3.9. Coinductive Datatypes *} (* Lazy lists are defined in Andreas Lochbihler's "Coinductive" AFP entry. Since we cannot rely on its presence, we expediently provide our own axiomatization. The examples also work unchanged with Lochbihler's "Coinductive_List" theory. *) typedef 'a llist = "UNIV\('a list + (nat \ 'a)) set" by auto definition LNil where "LNil = Abs_llist (Inl [])" definition LCons where "LCons y ys = Abs_llist (case Rep_llist ys of Inl ys' \ Inl (y # ys') | Inr f \ Inr (\n. case n of 0 \ y | Suc m \ f m))" axiomatization iterates :: "('a \ 'a) \ 'a \ 'a llist" lemma iterates_def [nitpick_simp]: "iterates f a = LCons a (iterates f (f a))" sorry declaration {* Nitpick_HOL.register_codatatype @{typ "'a llist"} "" (map dest_Const [@{term LNil}, @{term LCons}]) *} lemma "xs \ LCons a xs" nitpick [expect = genuine] oops lemma "\xs = LCons a xs; ys = iterates (\b. a) b\ \ xs = ys" nitpick [verbose, expect = genuine] oops lemma "\xs = LCons a xs; ys = LCons a ys\ \ xs = ys" nitpick [bisim_depth = -1, show_datatypes, expect = quasi_genuine] nitpick [card = 1\5, expect = none] sorry subsection {* 3.10. Boxing *} datatype tm = Var nat | Lam tm | App tm tm primrec lift where "lift (Var j) k = Var (if j < k then j else j + 1)" | "lift (Lam t) k = Lam (lift t (k + 1))" | "lift (App t u) k = App (lift t k) (lift u k)" primrec loose where "loose (Var j) k = (j \ k)" | "loose (Lam t) k = loose t (Suc k)" | "loose (App t u) k = (loose t k \ loose u k)" primrec subst\<^isub>1 where "subst\<^isub>1 \ (Var j) = \ j" | "subst\<^isub>1 \ (Lam t) = Lam (subst\<^isub>1 (\n. case n of 0 \ Var 0 | Suc m \ lift (\ m) 1) t)" | "subst\<^isub>1 \ (App t u) = App (subst\<^isub>1 \ t) (subst\<^isub>1 \ u)" lemma "\ loose t 0 \ subst\<^isub>1 \ t = t" nitpick [verbose, expect = genuine] nitpick [eval = "subst\<^isub>1 \ t", expect = genuine] (* nitpick [dont_box, expect = unknown] *) oops primrec subst\<^isub>2 where "subst\<^isub>2 \ (Var j) = \ j" | "subst\<^isub>2 \ (Lam t) = Lam (subst\<^isub>2 (\n. case n of 0 \ Var 0 | Suc m \ lift (\ m) 0) t)" | "subst\<^isub>2 \ (App t u) = App (subst\<^isub>2 \ t) (subst\<^isub>2 \ u)" lemma "\ loose t 0 \ subst\<^isub>2 \ t = t" nitpick [card = 1\5, expect = none] sorry subsection {* 3.11. Scope Monotonicity *} lemma "length xs = length ys \ rev (zip xs ys) = zip xs (rev ys)" nitpick [verbose, expect = genuine] oops lemma "\g. \x\'b. g (f x) = x \ \y\'a. \x. y = f x" nitpick [mono, expect = none] nitpick [expect = genuine] oops subsection {* 3.12. Inductive Properties *} inductive_set reach where "(4\nat) \ reach" | "n \ reach \ n < 4 \ 3 * n + 1 \ reach" | "n \ reach \ n + 2 \ reach" lemma "n \ reach \ 2 dvd n" (* nitpick *) apply (induct set: reach) apply auto nitpick [card = 1\4, bits = 1\4, expect = none] apply (thin_tac "n \ reach") nitpick [expect = genuine] oops lemma "n \ reach \ 2 dvd n \ n \ 0" (* nitpick *) apply (induct set: reach) apply auto nitpick [card = 1\4, bits = 1\4, expect = none] apply (thin_tac "n \ reach") nitpick [expect = genuine] oops lemma "n \ reach \ 2 dvd n \ n \ 4" by (induct set: reach) arith+ datatype 'a bin_tree = Leaf 'a | Branch "'a bin_tree" "'a bin_tree" primrec labels where "labels (Leaf a) = {a}" | "labels (Branch t u) = labels t \ labels u" primrec swap where "swap (Leaf c) a b = (if c = a then Leaf b else if c = b then Leaf a else Leaf c)" | "swap (Branch t u) a b = Branch (swap t a b) (swap u a b)" lemma "{a, b} \ labels t \ labels (swap t a b) = labels t" (* nitpick *) proof (induct t) case Leaf thus ?case by simp next case (Branch t u) thus ?case (* nitpick *) nitpick [non_std, show_all, expect = genuine] oops lemma "labels (swap t a b) = (if a \ labels t then if b \ labels t then labels t else (labels t - {a}) \ {b} else if b \ labels t then (labels t - {b}) \ {a} else labels t)" (* nitpick *) proof (induct t) case Leaf thus ?case by simp next case (Branch t u) thus ?case nitpick [non_std, card = 1\4, expect = none] by auto qed section {* 4. Case Studies *} nitpick_params [max_potential = 0] subsection {* 4.1. A Context-Free Grammar *} datatype alphabet = a | b inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where "[] \ S\<^isub>1" | "w \ A\<^isub>1 \ b # w \ S\<^isub>1" | "w \ B\<^isub>1 \ a # w \ S\<^isub>1" | "w \ S\<^isub>1 \ a # w \ A\<^isub>1" | "w \ S\<^isub>1 \ b # w \ S\<^isub>1" | "\v \ B\<^isub>1; v \ B\<^isub>1\ \ a # v @ w \ B\<^isub>1" theorem S\<^isub>1_sound: "w \ S\<^isub>1 \ length [x \ w. x = a] = length [x \ w. x = b]" nitpick [expect = genuine] oops inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where "[] \ S\<^isub>2" | "w \ A\<^isub>2 \ b # w \ S\<^isub>2" | "w \ B\<^isub>2 \ a # w \ S\<^isub>2" | "w \ S\<^isub>2 \ a # w \ A\<^isub>2" | "w \ S\<^isub>2 \ b # w \ B\<^isub>2" | "\v \ B\<^isub>2; v \ B\<^isub>2\ \ a # v @ w \ B\<^isub>2" theorem S\<^isub>2_sound: "w \ S\<^isub>2 \ length [x \ w. x = a] = length [x \ w. x = b]" nitpick [expect = genuine] oops inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where "[] \ S\<^isub>3" | "w \ A\<^isub>3 \ b # w \ S\<^isub>3" | "w \ B\<^isub>3 \ a # w \ S\<^isub>3" | "w \ S\<^isub>3 \ a # w \ A\<^isub>3" | "w \ S\<^isub>3 \ b # w \ B\<^isub>3" | "\v \ B\<^isub>3; w \ B\<^isub>3\ \ a # v @ w \ B\<^isub>3" theorem S\<^isub>3_sound: "w \ S\<^isub>3 \ length [x \ w. x = a] = length [x \ w. x = b]" nitpick [card = 1\5, expect = none] sorry theorem S\<^isub>3_complete: "length [x \ w. x = a] = length [x \ w. x = b] \ w \ S\<^isub>3" nitpick [expect = genuine] oops inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where "[] \ S\<^isub>4" | "w \ A\<^isub>4 \ b # w \ S\<^isub>4" | "w \ B\<^isub>4 \ a # w \ S\<^isub>4" | "w \ S\<^isub>4 \ a # w \ A\<^isub>4" | "\v \ A\<^isub>4; w \ A\<^isub>4\ \ b # v @ w \ A\<^isub>4" | "w \ S\<^isub>4 \ b # w \ B\<^isub>4" | "\v \ B\<^isub>4; w \ B\<^isub>4\ \ a # v @ w \ B\<^isub>4" theorem S\<^isub>4_sound: "w \ S\<^isub>4 \ length [x \ w. x = a] = length [x \ w. x = b]" nitpick [card = 1\5, expect = none] sorry theorem S\<^isub>4_complete: "length [x \ w. x = a] = length [x \ w. x = b] \ w \ S\<^isub>4" nitpick [card = 1\5, expect = none] sorry theorem S\<^isub>4_A\<^isub>4_B\<^isub>4_sound_and_complete: "w \ S\<^isub>4 \ length [x \ w. x = a] = length [x \ w. x = b]" "w \ A\<^isub>4 \ length [x \ w. x = a] = length [x \ w. x = b] + 1" "w \ B\<^isub>4 \ length [x \ w. x = b] = length [x \ w. x = a] + 1" nitpick [card = 1\5, expect = none] sorry subsection {* 4.2. AA Trees *} datatype 'a aa_tree = \ | N "'a\linorder" nat "'a aa_tree" "'a aa_tree" primrec data where "data \ = undefined" | "data (N x _ _ _) = x" primrec dataset where "dataset \ = {}" | "dataset (N x _ t u) = {x} \ dataset t \ dataset u" primrec level where "level \ = 0" | "level (N _ k _ _) = k" primrec left where "left \ = \" | "left (N _ _ t\<^isub>1 _) = t\<^isub>1" primrec right where "right \ = \" | "right (N _ _ _ t\<^isub>2) = t\<^isub>2" fun wf where "wf \ = True" | "wf (N _ k t u) = (if t = \ then k = 1 \ (u = \ \ (level u = 1 \ left u = \ \ right u = \)) else wf t \ wf u \ u \ \ \ level t < k \ level u \ k \ level (right u) < k)" fun skew where "skew \ = \" | "skew (N x k t u) = (if t \ \ \ k = level t then N (data t) k (left t) (N x k (right t) u) else N x k t u)" fun split where "split \ = \" | "split (N x k t u) = (if u \ \ \ k = level (right u) then N (data u) (Suc k) (N x k t (left u)) (right u) else N x k t u)" theorem dataset_skew_split: "dataset (skew t) = dataset t" "dataset (split t) = dataset t" nitpick [card = 1\5, expect = none] sorry theorem wf_skew_split: "wf t \ skew t = t" "wf t \ split t = t" nitpick [card = 1\5, expect = none] sorry primrec insort\<^isub>1 where "insort\<^isub>1 \ x = N x 1 \ \" | "insort\<^isub>1 (N y k t u) x = (* (split \ skew) *) (N y k (if x < y then insort\<^isub>1 t x else t) (if x > y then insort\<^isub>1 u x else u))" theorem wf_insort\<^isub>1: "wf t \ wf (insort\<^isub>1 t x)" nitpick [expect = genuine] oops theorem wf_insort\<^isub>1_nat: "wf t \ wf (insort\<^isub>1 t (x\nat))" nitpick [eval = "insort\<^isub>1 t x", expect = genuine] oops primrec insort\<^isub>2 where "insort\<^isub>2 \ x = N x 1 \ \" | "insort\<^isub>2 (N y k t u) x = (split \ skew) (N y k (if x < y then insort\<^isub>2 t x else t) (if x > y then insort\<^isub>2 u x else u))" theorem wf_insort\<^isub>2: "wf t \ wf (insort\<^isub>2 t x)" nitpick [card = 1\5, expect = none] sorry theorem dataset_insort\<^isub>2: "dataset (insort\<^isub>2 t x) = {x} \ dataset t" nitpick [card = 1\5, expect = none] sorry end