(* Title: HOL/Nitpick_Examples/Manual_Nits.thy
Author: Jasmin Blanchette, TU Muenchen
Copyright 2009-2014
Examples from the Nitpick manual.
*)
section \<open>Examples from the Nitpick Manual\<close>
(* 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 \<open>2. First Steps\<close>
nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
subsection \<open>2.1. Propositional Logic\<close>
lemma "P \ Q"
nitpick [expect = genuine]
apply auto
nitpick [expect = genuine] 1
nitpick [expect = genuine] 2
oops
subsection \<open>2.2. Type Variables\<close>
lemma "x \ A \ (THE y. y \ A) \ A"
nitpick [verbose, expect = genuine]
oops
subsection \<open>2.3. Constants\<close>
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 \<open>2.4. Skolemization\<close>
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 \<open>2.5. Natural Numbers and Integers\<close>
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 \<open>2.6. Inductive Datatypes\<close>
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 \<open>2.7. Typedefs, Records, Rationals, and Reals\<close>
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 \<open>
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
\<close>
declaration \<open>
Nitpick_Model.register_term_postprocessor \<^typ>\<open>my_int\<close> my_int_postproc
\<close>
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 \<open>2.8. Inductive and Coinductive Predicates\<close>
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 \<open>2.9. Coinductive Datatypes\<close>
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 \<open>2.10. Boxing\<close>
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\<^sub>1 where
"subst\<^sub>1 \ (Var j) = \ j" |
"subst\<^sub>1 \ (Lam t) =
Lam (subst\<^sub>1 (\<lambda>n. case n of 0 \<Rightarrow> Var 0 | Suc m \<Rightarrow> lift (\<sigma> m) 1) t)" |
"subst\<^sub>1 \ (App t u) = App (subst\<^sub>1 \ t) (subst\<^sub>1 \ u)"
lemma "\ loose t 0 \ subst\<^sub>1 \ t = t"
nitpick [verbose, expect = genuine]
nitpick [eval = "subst\<^sub>1 \ t", expect = genuine]
(* nitpick [dont_box, expect = unknown] *)
oops
primrec subst\<^sub>2 where
"subst\<^sub>2 \ (Var j) = \ j" |
"subst\<^sub>2 \ (Lam t) =
Lam (subst\<^sub>2 (\<lambda>n. case n of 0 \<Rightarrow> Var 0 | Suc m \<Rightarrow> lift (\<sigma> m) 0) t)" |
"subst\<^sub>2 \ (App t u) = App (subst\<^sub>2 \ t) (subst\<^sub>2 \ u)"
lemma "\ loose t 0 \ subst\<^sub>2 \ t = t"
nitpick [card = 1-5, expect = none]
sorry
subsection \<open>2.11. Scope Monotonicity\<close>
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 \<open>2.12. Inductive Properties\<close>
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 \<open>3. Case Studies\<close>
nitpick_params [max_potential = 0]
subsection \<open>3.1. A Context-Free Grammar\<close>
datatype alphabet = a | b
inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where
"[] \ S\<^sub>1"
| "w \ A\<^sub>1 \ b # w \ S\<^sub>1"
| "w \ B\<^sub>1 \ a # w \ S\<^sub>1"
| "w \ S\<^sub>1 \ a # w \ A\<^sub>1"
| "w \ S\<^sub>1 \ b # w \ S\<^sub>1"
| "\v \ B\<^sub>1; v \ B\<^sub>1\ \ a # v @ w \ B\<^sub>1"
theorem S\<^sub>1_sound:
"w \ S\<^sub>1 \ length [x \ w. x = a] = length [x \ w. x = b]"
nitpick [expect = genuine]
oops
inductive_set S\<^sub>2 and A\<^sub>2 and B\<^sub>2 where
"[] \ S\<^sub>2"
| "w \ A\<^sub>2 \ b # w \ S\<^sub>2"
| "w \ B\<^sub>2 \ a # w \ S\<^sub>2"
| "w \ S\<^sub>2 \ a # w \ A\<^sub>2"
| "w \ S\<^sub>2 \ b # w \ B\<^sub>2"
| "\v \ B\<^sub>2; v \ B\<^sub>2\ \ a # v @ w \ B\<^sub>2"
theorem S\<^sub>2_sound:
"w \ S\<^sub>2 \ length [x \ w. x = a] = length [x \ w. x = b]"
nitpick [expect = genuine]
oops
inductive_set S\<^sub>3 and A\<^sub>3 and B\<^sub>3 where
"[] \ S\<^sub>3"
| "w \ A\<^sub>3 \ b # w \ S\<^sub>3"
| "w \ B\<^sub>3 \ a # w \ S\<^sub>3"
| "w \ S\<^sub>3 \ a # w \ A\<^sub>3"
| "w \ S\<^sub>3 \ b # w \ B\<^sub>3"
| "\v \ B\<^sub>3; w \ B\<^sub>3\ \ a # v @ w \ B\<^sub>3"
theorem S\<^sub>3_sound:
"w \ S\<^sub>3 \ length [x \ w. x = a] = length [x \ w. x = b]"
nitpick [card = 1-5, expect = none]
sorry
theorem S\<^sub>3_complete:
"length [x \ w. x = a] = length [x \ w. x = b] \ w \ S\<^sub>3"
nitpick [expect = genuine]
oops
inductive_set S\<^sub>4 and A\<^sub>4 and B\<^sub>4 where
"[] \ S\<^sub>4"
| "w \ A\<^sub>4 \ b # w \ S\<^sub>4"
| "w \ B\<^sub>4 \ a # w \ S\<^sub>4"
| "w \ S\<^sub>4 \ a # w \ A\<^sub>4"
| "\v \ A\<^sub>4; w \ A\<^sub>4\ \ b # v @ w \ A\<^sub>4"
| "w \ S\<^sub>4 \ b # w \ B\<^sub>4"
| "\v \ B\<^sub>4; w \ B\<^sub>4\ \ a # v @ w \ B\<^sub>4"
theorem S\<^sub>4_sound:
"w \ S\<^sub>4 \ length [x \ w. x = a] = length [x \ w. x = b]"
nitpick [card = 1-5, expect = none]
sorry
theorem S\<^sub>4_complete:
"length [x \ w. x = a] = length [x \ w. x = b] \ w \ S\<^sub>4"
nitpick [card = 1-5, expect = none]
sorry
theorem S\<^sub>4_A\<^sub>4_B\<^sub>4_sound_and_complete:
"w \ S\<^sub>4 \ length [x \ w. x = a] = length [x \ w. x = b]"
"w \ A\<^sub>4 \ length [x \ w. x = a] = length [x \ w. x = b] + 1"
"w \ B\<^sub>4 \ length [x \ w. x = b] = length [x \ w. x = a] + 1"
nitpick [card = 1-5, expect = none]
sorry
subsection \<open>3.2. AA Trees\<close>
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\<^sub>1 _) = t\<^sub>1"
primrec right where
"right \ = \" |
"right (N _ _ _ t\<^sub>2) = t\<^sub>2"
fun wf where
"wf \ = True" |
"wf (N _ k t u) =
(if t = \<Lambda> then
k = 1 \<and> (u = \<Lambda> \<or> (level u = 1 \<and> left u = \<Lambda> \<and> right u = \<Lambda>))
else
wf t \<and> wf u \<and> u \<noteq> \<Lambda> \<and> level t < k \<and> level u \<le> k \<and> level (right u) < k)"
fun skew where
"skew \ = \" |
"skew (N x k t u) =
(if t \<noteq> \<Lambda> \<and> 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 \<noteq> \<Lambda> \<and> 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\<^sub>1 where
"insort\<^sub>1 \ x = N x 1 \ \" |
"insort\<^sub>1 (N y k t u) x =
\<^cancel>\<open>(split \<circ> skew)\<close> (N y k (if x < y then insort\<^sub>1 t x else t)
(if x > y then insort\<^sub>1 u x else u))"
theorem wf_insort\<^sub>1: "wf t \<Longrightarrow> wf (insort\<^sub>1 t x)"
nitpick [expect = genuine]
oops
theorem wf_insort\<^sub>1_nat: "wf t \<Longrightarrow> wf (insort\<^sub>1 t (x::nat))"
nitpick [eval = "insort\<^sub>1 t x", expect = genuine]
oops
primrec insort\<^sub>2 where
"insort\<^sub>2 \ x = N x 1 \ \" |
"insort\<^sub>2 (N y k t u) x =
(split \<circ> skew) (N y k (if x < y then insort\<^sub>2 t x else t)
(if x > y then insort\<^sub>2 u x else u))"
theorem wf_insort\<^sub>2: "wf t \<Longrightarrow> wf (insort\<^sub>2 t x)"
nitpick [card = 1-5, expect = none]
sorry
theorem dataset_insort\<^sub>2: "dataset (insort\<^sub>2 t x) = {x} \<union> dataset t"
nitpick [card = 1-5, expect = none]
sorry
end
¤ Dauer der Verarbeitung: 0.18 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
