Theory Manual_Nits

(*  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›

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