(* 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, 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 \<^Type>‹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›