(* Title: HOL/Nitpick_Examples/Manual_Nits.thy Author: Jasmin Blanchette, TU Muenchen Copyright 2009-2014 Examples from the Nitpick manual. *) section ‹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 HOL.Real "HOL-Library.Quotient_Product" begin section ‹2. First Steps› nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240] subsection ‹2.1. Propositional Logic› lemma "P ⟷ Q" nitpick [expect = genuine] apply auto nitpick [expect = genuine] 1 nitpick [expect = genuine] 2 oops subsection ‹2.2. Type Variables› lemma "x ∈ A ⟹ (THE y. y ∈ A) ∈ A" nitpick [verbose, expect = genuine] oops subsection ‹2.3. Constants› lemma "x ∈ A ⟹ (THE y. y ∈ A) ∈ A" nitpick [show_consts, expect = genuine] nitpick [dont_specialize, show_consts, expect = genuine] oops lemma "∃!x. x ∈ A ⟹ (THE y. y ∈ A) ∈ A" nitpick [expect = none] nitpick [card 'a = 1-50, expect = none] (* sledgehammer *) by (metis the_equality) subsection ‹2.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 ‹2.5. Natural Numbers and Integers› lemma "⟦i ≤ j; n ≤ (m::int)⟧ ⟹ i * n + j * m ≤ i * m + j * n" nitpick [expect = genuine] nitpick [binary_ints, bits = 16, expect = genuine] oops lemma "∀n. Suc n ≠ n ⟹ P" nitpick [card nat = 100, expect = potential] oops lemma "P Suc" nitpick [expect = none] oops lemma "P ((+)::nat⇒nat⇒nat)" nitpick [card nat = 1, expect = genuine] nitpick [card nat = 2, expect = none] oops subsection ‹2.6. Inductive Datatypes› lemma "hd (xs @ [y, y]) = hd xs" nitpick [expect = genuine] nitpick [show_consts, show_types, expect = genuine] oops lemma "⟦length xs = 1; length ys = 1⟧ ⟹ xs = ys" nitpick [show_types, expect = genuine] oops subsection ‹2.7. Typedefs, Records, Rationals, and Reals› definition "three = {0::nat, 1, 2}" typedef three = three unfolding three_def 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 "⟦A ∈ X; B ∈ X⟧ ⟹ c ∈ X" nitpick [show_types, 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 fun_eq_iff) 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 unfolding add_raw_def by auto lemma "add x y = add x x" nitpick [show_types, 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_types] oops record point = Xcoord :: int Ycoord :: int lemma "Xcoord (p::point) = Xcoord (q::point)" nitpick [show_types, expect = genuine] oops lemma "4 * x + 3 * (y::real) ≠ 1 / 2" nitpick [show_types, expect = genuine] oops subsection ‹2.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 = (λn. n ∈ {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 = 4, show_consts, expect = genuine] oops subsection ‹2.9. Coinductive Datatypes› codatatype 'a llist = LNil | LCons 'a "'a llist" primcorec iterates where "iterates f a = LCons a (iterates f (f a))" 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_types, expect = quasi_genuine] nitpick [card = 1-5, expect = none] sorry subsection ‹2.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⇩_{1}where "subst⇩_{1}σ (Var j) = σ j" | "subst⇩_{1}σ (Lam t) = Lam (subst⇩_{1}(λn. case n of 0 ⇒ Var 0 | Suc m ⇒ lift (σ m) 1) t)" | "subst⇩_{1}σ (App t u) = App (subst⇩_{1}σ t) (subst⇩_{1}σ u)" lemma "¬ loose t 0 ⟹ subst⇩_{1}σ t = t" nitpick [verbose, expect = genuine] nitpick [eval = "subst⇩_{1}σ t", expect = genuine] (* nitpick [dont_box, expect = unknown] *) oops primrec subst⇩_{2}where "subst⇩_{2}σ (Var j) = σ j" | "subst⇩_{2}σ (Lam t) = Lam (subst⇩_{2}(λn. case n of 0 ⇒ Var 0 | Suc m ⇒ lift (σ m) 0) t)" | "subst⇩_{2}σ (App t u) = App (subst⇩_{2}σ t) (subst⇩_{2}σ u)" lemma "¬ loose t 0 ⟹ subst⇩_{2}σ t = t" nitpick [card = 1-5, expect = none] sorry subsection ‹2.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 ‹2.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+ section ‹3. Case Studies› nitpick_params [max_potential = 0] subsection ‹3.1. A Context-Free Grammar› datatype alphabet = a | b inductive_set S⇩_{1}and A⇩_{1}and B⇩_{1}where "[] ∈ S⇩_{1}" | "w ∈ A⇩_{1}⟹ b # w ∈ S⇩_{1}" | "w ∈ B⇩_{1}⟹ a # w ∈ S⇩_{1}" | "w ∈ S⇩_{1}⟹ a # w ∈ A⇩_{1}" | "w ∈ S⇩_{1}⟹ b # w ∈ S⇩_{1}" | "⟦v ∈ B⇩_{1}; v ∈ B⇩_{1}⟧ ⟹ a # v @ w ∈ B⇩_{1}" theorem S⇩_{1}_sound: "w ∈ S⇩_{1}⟶ length [x ← w. x = a] = length [x ← w. x = b]" nitpick [expect = genuine] oops inductive_set S⇩_{2}and A⇩_{2}and B⇩_{2}where "[] ∈ S⇩_{2}" | "w ∈ A⇩_{2}⟹ b # w ∈ S⇩_{2}" | "w ∈ B⇩_{2}⟹ a # w ∈ S⇩_{2}" | "w ∈ S⇩_{2}⟹ a # w ∈ A⇩_{2}" | "w ∈ S⇩_{2}⟹ b # w ∈ B⇩_{2}" | "⟦v ∈ B⇩_{2}; v ∈ B⇩_{2}⟧ ⟹ a # v @ w ∈ B⇩_{2}" theorem S⇩_{2}_sound: "w ∈ S⇩_{2}⟶ length [x ← w. x = a] = length [x ← w. x = b]" nitpick [expect = genuine] oops inductive_set S⇩_{3}and A⇩_{3}and B⇩_{3}where "[] ∈ S⇩_{3}" | "w ∈ A⇩_{3}⟹ b # w ∈ S⇩_{3}" | "w ∈ B⇩_{3}⟹ a # w ∈ S⇩_{3}" | "w ∈ S⇩_{3}⟹ a # w ∈ A⇩_{3}" | "w ∈ S⇩_{3}⟹ b # w ∈ B⇩_{3}" | "⟦v ∈ B⇩_{3}; w ∈ B⇩_{3}⟧ ⟹ a # v @ w ∈ B⇩_{3}" theorem S⇩_{3}_sound: "w ∈ S⇩_{3}⟶ length [x ← w. x = a] = length [x ← w. x = b]" nitpick [card = 1-5, expect = none] sorry theorem S⇩_{3}_complete: "length [x ← w. x = a] = length [x ← w. x = b] ⟶ w ∈ S⇩_{3}" nitpick [expect = genuine] oops inductive_set S⇩_{4}and A⇩_{4}and B⇩_{4}where "[] ∈ S⇩_{4}" | "w ∈ A⇩_{4}⟹ b # w ∈ S⇩_{4}" | "w ∈ B⇩_{4}⟹ a # w ∈ S⇩_{4}" | "w ∈ S⇩_{4}⟹ a # w ∈ A⇩_{4}" | "⟦v ∈ A⇩_{4}; w ∈ A⇩_{4}⟧ ⟹ b # v @ w ∈ A⇩_{4}" | "w ∈ S⇩_{4}⟹ b # w ∈ B⇩_{4}" | "⟦v ∈ B⇩_{4}; w ∈ B⇩_{4}⟧ ⟹ a # v @ w ∈ B⇩_{4}" theorem S⇩_{4}_sound: "w ∈ S⇩_{4}⟶ length [x ← w. x = a] = length [x ← w. x = b]" nitpick [card = 1-5, expect = none] sorry theorem S⇩_{4}_complete: "length [x ← w. x = a] = length [x ← w. x = b] ⟶ w ∈ S⇩_{4}" nitpick [card = 1-5, expect = none] sorry theorem S⇩_{4}_A⇩_{4}_B⇩_{4}_sound_and_complete: "w ∈ S⇩_{4}⟷ length [x ← w. x = a] = length [x ← w. x = b]" "w ∈ A⇩_{4}⟷ length [x ← w. x = a] = length [x ← w. x = b] + 1" "w ∈ B⇩_{4}⟷ length [x ← w. x = b] = length [x ← w. x = a] + 1" nitpick [card = 1-5, expect = none] sorry subsection ‹3.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⇩_{1}_) = t⇩_{1}" primrec right where "right Λ = Λ" | "right (N _ _ _ t⇩_{2}) = t⇩_{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⇩_{1}where "insort⇩_{1}Λ x = N x 1 Λ Λ" | "insort⇩_{1}(N y k t u) x = ⌦‹(split ∘ skew)› (N y k (if x < y then insort⇩_{1}t x else t) (if x > y then insort⇩_{1}u x else u))" theorem wf_insort⇩_{1}: "wf t ⟹ wf (insort⇩_{1}t x)" nitpick [expect = genuine] oops theorem wf_insort⇩_{1}_nat: "wf t ⟹ wf (insort⇩_{1}t (x::nat))" nitpick [eval = "insort⇩_{1}t x", expect = genuine] oops primrec insort⇩_{2}where "insort⇩_{2}Λ x = N x 1 Λ Λ" | "insort⇩_{2}(N y k t u) x = (split ∘ skew) (N y k (if x < y then insort⇩_{2}t x else t) (if x > y then insort⇩_{2}u x else u))" theorem wf_insort⇩_{2}: "wf t ⟹ wf (insort⇩_{2}t x)" nitpick [card = 1-5, expect = none] sorry theorem dataset_insort⇩_{2}: "dataset (insort⇩_{2}t x) = {x} ∪ dataset t" nitpick [card = 1-5, expect = none] sorry end