# Theory Nitpick

Up to index of Isabelle/HOL-Proofs

theory Nitpick
imports Sledgehammer
(*  Title:      HOL/Nitpick.thy    Author:     Jasmin Blanchette, TU Muenchen    Copyright   2008, 2009, 2010Nitpick: Yet another counterexample generator for Isabelle/HOL.*)header {* Nitpick: Yet Another Counterexample Generator for Isabelle/HOL *}theory Nitpickimports Hilbert_Choice List Map Quotient Record Sledgehammerkeywords "nitpick" :: diag and "nitpick_params" :: thy_declbegintypedecl bisim_iteratoraxiomatization unknown :: 'a           and is_unknown :: "'a => bool"           and bisim :: "bisim_iterator => 'a => 'a => bool"           and bisim_iterator_max :: bisim_iterator           and Quot :: "'a => 'b"           and safe_The :: "('a => bool) => 'a"datatype ('a, 'b) fun_box = FunBox "('a => 'b)"datatype ('a, 'b) pair_box = PairBox 'a 'btypedecl unsigned_bittypedecl signed_bitdatatype 'a word = Word "('a set)"text {*Alternative definitions.*}lemma Ex1_unfold [nitpick_unfold, no_atp]:"Ex1 P ≡ ∃x. {x. P x} = {x}"apply (rule eq_reflection)apply (simp add: Ex1_def set_eq_iff)apply (rule iffI) apply (erule exE) apply (erule conjE) apply (rule_tac x = x in exI) apply (rule allI) apply (rename_tac y) apply (erule_tac x = y in allE)by autolemma rtrancl_unfold [nitpick_unfold, no_atp]: "r⇧* ≡ (r⇧+)⇧="  by (simp only: rtrancl_trancl_reflcl)lemma rtranclp_unfold [nitpick_unfold, no_atp]:"rtranclp r a b ≡ (a = b ∨ tranclp r a b)"by (rule eq_reflection) (auto dest: rtranclpD)lemma tranclp_unfold [nitpick_unfold, no_atp]:"tranclp r a b ≡ (a, b) ∈ trancl {(x, y). r x y}"by (simp add: trancl_def)lemma [nitpick_simp, no_atp]:"of_nat n = (if n = 0 then 0 else 1 + of_nat (n - 1))"by (cases n) autodefinition prod :: "'a set => 'b set => ('a × 'b) set" where"prod A B = {(a, b). a ∈ A ∧ b ∈ B}"definition refl' :: "('a × 'a) set => bool" where"refl' r ≡ ∀x. (x, x) ∈ r"definition wf' :: "('a × 'a) set => bool" where"wf' r ≡ acyclic r ∧ (finite r ∨ unknown)"definition card' :: "'a set => nat" where"card' A ≡ if finite A then length (SOME xs. set xs = A ∧ distinct xs) else 0"definition setsum' :: "('a => 'b::comm_monoid_add) => 'a set => 'b" where"setsum' f A ≡ if finite A then listsum (map f (SOME xs. set xs = A ∧ distinct xs)) else 0"inductive fold_graph' :: "('a => 'b => 'b) => 'b => 'a set => 'b => bool" where"fold_graph' f z {} z" |"[|x ∈ A; fold_graph' f z (A - {x}) y|] ==> fold_graph' f z A (f x y)"text {*The following lemmas are not strictly necessary but they help the\textit{specialize} optimization.*}lemma The_psimp [nitpick_psimp, no_atp]:  "P = (op =) x ==> The P = x"  by autolemma Eps_psimp [nitpick_psimp, no_atp]:"[|P x; ¬ P y; Eps P = y|] ==> Eps P = x"apply (cases "P (Eps P)") apply autoapply (erule contrapos_np)by (rule someI)lemma unit_case_unfold [nitpick_unfold, no_atp]:"unit_case x u ≡ x"apply (subgoal_tac "u = ()") apply (simp only: unit.cases)by simpdeclare unit.cases [nitpick_simp del]lemma nat_case_unfold [nitpick_unfold, no_atp]:"nat_case x f n ≡ if n = 0 then x else f (n - 1)"apply (rule eq_reflection)by (cases n) autodeclare nat.cases [nitpick_simp del]lemma list_size_simp [nitpick_simp, no_atp]:"list_size f xs = (if xs = [] then 0                   else Suc (f (hd xs) + list_size f (tl xs)))""size xs = (if xs = [] then 0 else Suc (size (tl xs)))"by (cases xs) autotext {*Auxiliary definitions used to provide an alternative representation for@{text rat} and @{text real}.*}function nat_gcd :: "nat => nat => nat" where[simp del]: "nat_gcd x y = (if y = 0 then x else nat_gcd y (x mod y))"by autoterminationapply (relation "measure (λ(x, y). x + y + (if y > x then 1 else 0))") apply auto apply (metis mod_less_divisor xt1(9))by (metis mod_mod_trivial mod_self nat_neq_iff xt1(10))definition nat_lcm :: "nat => nat => nat" where"nat_lcm x y = x * y div (nat_gcd x y)"definition int_gcd :: "int => int => int" where"int_gcd x y = int (nat_gcd (nat (abs x)) (nat (abs y)))"definition int_lcm :: "int => int => int" where"int_lcm x y = int (nat_lcm (nat (abs x)) (nat (abs y)))"definition Frac :: "int × int => bool" where"Frac ≡ λ(a, b). b > 0 ∧ int_gcd a b = 1"axiomatization Abs_Frac :: "int × int => 'a"           and Rep_Frac :: "'a => int × int"definition zero_frac :: 'a where"zero_frac ≡ Abs_Frac (0, 1)"definition one_frac :: 'a where"one_frac ≡ Abs_Frac (1, 1)"definition num :: "'a => int" where"num ≡ fst o Rep_Frac"definition denom :: "'a => int" where"denom ≡ snd o Rep_Frac"function norm_frac :: "int => int => int × int" where[simp del]: "norm_frac a b = (if b < 0 then norm_frac (- a) (- b)                              else if a = 0 ∨ b = 0 then (0, 1)                              else let c = int_gcd a b in (a div c, b div c))"by pat_completeness autotermination by (relation "measure (λ(_, b). if b < 0 then 1 else 0)") autodefinition frac :: "int => int => 'a" where"frac a b ≡ Abs_Frac (norm_frac a b)"definition plus_frac :: "'a => 'a => 'a" where[nitpick_simp]:"plus_frac q r = (let d = int_lcm (denom q) (denom r) in                    frac (num q * (d div denom q) + num r * (d div denom r)) d)"definition times_frac :: "'a => 'a => 'a" where[nitpick_simp]:"times_frac q r = frac (num q * num r) (denom q * denom r)"definition uminus_frac :: "'a => 'a" where"uminus_frac q ≡ Abs_Frac (- num q, denom q)"definition number_of_frac :: "int => 'a" where"number_of_frac n ≡ Abs_Frac (n, 1)"definition inverse_frac :: "'a => 'a" where"inverse_frac q ≡ frac (denom q) (num q)"definition less_frac :: "'a => 'a => bool" where[nitpick_simp]:"less_frac q r <-> num (plus_frac q (uminus_frac r)) < 0"definition less_eq_frac :: "'a => 'a => bool" where[nitpick_simp]:"less_eq_frac q r <-> num (plus_frac q (uminus_frac r)) ≤ 0"definition of_frac :: "'a => 'b::{inverse,ring_1}" where"of_frac q ≡ of_int (num q) / of_int (denom q)"ML_file "Tools/Nitpick/kodkod.ML"ML_file "Tools/Nitpick/kodkod_sat.ML"ML_file "Tools/Nitpick/nitpick_util.ML"ML_file "Tools/Nitpick/nitpick_hol.ML"ML_file "Tools/Nitpick/nitpick_mono.ML"ML_file "Tools/Nitpick/nitpick_preproc.ML"ML_file "Tools/Nitpick/nitpick_scope.ML"ML_file "Tools/Nitpick/nitpick_peephole.ML"ML_file "Tools/Nitpick/nitpick_rep.ML"ML_file "Tools/Nitpick/nitpick_nut.ML"ML_file "Tools/Nitpick/nitpick_kodkod.ML"ML_file "Tools/Nitpick/nitpick_model.ML"ML_file "Tools/Nitpick/nitpick.ML"ML_file "Tools/Nitpick/nitpick_isar.ML"ML_file "Tools/Nitpick/nitpick_tests.ML"setup {*  Nitpick_Isar.setup #>  Nitpick_HOL.register_ersatz_global    [(@{const_name card}, @{const_name card'}),     (@{const_name setsum}, @{const_name setsum'}),     (@{const_name fold_graph}, @{const_name fold_graph'}),     (@{const_name wf}, @{const_name wf'})]*}hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The    FunBox PairBox Word prod refl' wf' card' setsum'    fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac    one_frac num denom norm_frac frac plus_frac times_frac uminus_frac    number_of_frac inverse_frac less_frac less_eq_frac of_frachide_type (open) bisim_iterator fun_box pair_box unsigned_bit signed_bit wordhide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold    prod_def refl'_def wf'_def card'_def setsum'_def    fold_graph'_def The_psimp Eps_psimp unit_case_unfold nat_case_unfold    list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def    zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def    plus_frac_def times_frac_def uminus_frac_def number_of_frac_def    inverse_frac_def less_frac_def less_eq_frac_def of_frac_defend