Quelle Manual_Nits.thy Sprache: Isabelle

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

quality88%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.