1(* Title: HOL/Nitpick.thy 2 Author: Jasmin Blanchette, TU Muenchen 3 Copyright 2008, 2009, 2010 4 5Nitpick: Yet another counterexample generator for Isabelle/HOL. 6*) 7 8section \<open>Nitpick: Yet Another Counterexample Generator for Isabelle/HOL\<close> 9 10theory Nitpick 11imports Record GCD 12keywords 13 "nitpick" :: diag and 14 "nitpick_params" :: thy_decl 15begin 16 17datatype (plugins only: extraction) (dead 'a, dead 'b) fun_box = FunBox "'a \<Rightarrow> 'b" 18datatype (plugins only: extraction) (dead 'a, dead 'b) pair_box = PairBox 'a 'b 19datatype (plugins only: extraction) (dead 'a) word = Word "'a set" 20 21typedecl bisim_iterator 22typedecl unsigned_bit 23typedecl signed_bit 24 25consts 26 unknown :: 'a 27 is_unknown :: "'a \<Rightarrow> bool" 28 bisim :: "bisim_iterator \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 29 bisim_iterator_max :: bisim_iterator 30 Quot :: "'a \<Rightarrow> 'b" 31 safe_The :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" 32 33text \<open> 34Alternative definitions. 35\<close> 36 37lemma Ex1_unfold[nitpick_unfold]: "Ex1 P \<equiv> \<exists>x. {x. P x} = {x}" 38 apply (rule eq_reflection) 39 apply (simp add: Ex1_def set_eq_iff) 40 apply (rule iffI) 41 apply (erule exE) 42 apply (erule conjE) 43 apply (rule_tac x = x in exI) 44 apply (rule allI) 45 apply (rename_tac y) 46 apply (erule_tac x = y in allE) 47 by auto 48 49lemma rtrancl_unfold[nitpick_unfold]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>=" 50 by (simp only: rtrancl_trancl_reflcl) 51 52lemma rtranclp_unfold[nitpick_unfold]: "rtranclp r a b \<equiv> (a = b \<or> tranclp r a b)" 53 by (rule eq_reflection) (auto dest: rtranclpD) 54 55lemma tranclp_unfold[nitpick_unfold]: 56 "tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}" 57 by (simp add: trancl_def) 58 59lemma [nitpick_simp]: 60 "of_nat n = (if n = 0 then 0 else 1 + of_nat (n - 1))" 61 by (cases n) auto 62 63definition prod :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where 64 "prod A B = {(a, b). a \<in> A \<and> b \<in> B}" 65 66definition refl' :: "('a \<times> 'a) set \<Rightarrow> bool" where 67 "refl' r \<equiv> \<forall>x. (x, x) \<in> r" 68 69definition wf' :: "('a \<times> 'a) set \<Rightarrow> bool" where 70 "wf' r \<equiv> acyclic r \<and> (finite r \<or> unknown)" 71 72definition card' :: "'a set \<Rightarrow> nat" where 73 "card' A \<equiv> if finite A then length (SOME xs. set xs = A \<and> distinct xs) else 0" 74 75definition sum' :: "('a \<Rightarrow> 'b::comm_monoid_add) \<Rightarrow> 'a set \<Rightarrow> 'b" where 76 "sum' f A \<equiv> if finite A then sum_list (map f (SOME xs. set xs = A \<and> distinct xs)) else 0" 77 78inductive fold_graph' :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool" where 79 "fold_graph' f z {} z" | 80 "\<lbrakk>x \<in> A; fold_graph' f z (A - {x}) y\<rbrakk> \<Longrightarrow> fold_graph' f z A (f x y)" 81 82text \<open> 83The following lemmas are not strictly necessary but they help the 84\textit{specialize} optimization. 85\<close> 86 87lemma The_psimp[nitpick_psimp]: "P = (=) x \<Longrightarrow> The P = x" 88 by auto 89 90lemma Eps_psimp[nitpick_psimp]: 91 "\<lbrakk>P x; \<not> P y; Eps P = y\<rbrakk> \<Longrightarrow> Eps P = x" 92 apply (cases "P (Eps P)") 93 apply auto 94 apply (erule contrapos_np) 95 by (rule someI) 96 97lemma case_unit_unfold[nitpick_unfold]: 98 "case_unit x u \<equiv> x" 99 apply (subgoal_tac "u = ()") 100 apply (simp only: unit.case) 101 by simp 102 103declare unit.case[nitpick_simp del] 104 105lemma case_nat_unfold[nitpick_unfold]: 106 "case_nat x f n \<equiv> if n = 0 then x else f (n - 1)" 107 apply (rule eq_reflection) 108 by (cases n) auto 109 110declare nat.case[nitpick_simp del] 111 112lemma size_list_simp[nitpick_simp]: 113 "size_list f xs = (if xs = [] then 0 else Suc (f (hd xs) + size_list f (tl xs)))" 114 "size xs = (if xs = [] then 0 else Suc (size (tl xs)))" 115 by (cases xs) auto 116 117text \<open> 118Auxiliary definitions used to provide an alternative representation for 119\<open>rat\<close> and \<open>real\<close>. 120\<close> 121 122fun nat_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where 123 "nat_gcd x y = (if y = 0 then x else nat_gcd y (x mod y))" 124 125declare nat_gcd.simps [simp del] 126 127definition nat_lcm :: "nat \<Rightarrow> nat \<Rightarrow> nat" where 128 "nat_lcm x y = x * y div (nat_gcd x y)" 129 130lemma gcd_eq_nitpick_gcd [nitpick_unfold]: 131 "gcd x y = Nitpick.nat_gcd x y" 132 by (induct x y rule: nat_gcd.induct) 133 (simp add: gcd_nat.simps Nitpick.nat_gcd.simps) 134 135lemma lcm_eq_nitpick_lcm [nitpick_unfold]: 136 "lcm x y = Nitpick.nat_lcm x y" 137 by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd) 138 139definition Frac :: "int \<times> int \<Rightarrow> bool" where 140 "Frac \<equiv> \<lambda>(a, b). b > 0 \<and> coprime a b" 141 142consts 143 Abs_Frac :: "int \<times> int \<Rightarrow> 'a" 144 Rep_Frac :: "'a \<Rightarrow> int \<times> int" 145 146definition zero_frac :: 'a where 147 "zero_frac \<equiv> Abs_Frac (0, 1)" 148 149definition one_frac :: 'a where 150 "one_frac \<equiv> Abs_Frac (1, 1)" 151 152definition num :: "'a \<Rightarrow> int" where 153 "num \<equiv> fst \<circ> Rep_Frac" 154 155definition denom :: "'a \<Rightarrow> int" where 156 "denom \<equiv> snd \<circ> Rep_Frac" 157 158function norm_frac :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where 159 "norm_frac a b = 160 (if b < 0 then norm_frac (- a) (- b) 161 else if a = 0 \<or> b = 0 then (0, 1) 162 else let c = gcd a b in (a div c, b div c))" 163 by pat_completeness auto 164 termination by (relation "measure (\<lambda>(_, b). if b < 0 then 1 else 0)") auto 165 166declare norm_frac.simps[simp del] 167 168definition frac :: "int \<Rightarrow> int \<Rightarrow> 'a" where 169 "frac a b \<equiv> Abs_Frac (norm_frac a b)" 170 171definition plus_frac :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where 172 [nitpick_simp]: "plus_frac q r = (let d = lcm (denom q) (denom r) in 173 frac (num q * (d div denom q) + num r * (d div denom r)) d)" 174 175definition times_frac :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where 176 [nitpick_simp]: "times_frac q r = frac (num q * num r) (denom q * denom r)" 177 178definition uminus_frac :: "'a \<Rightarrow> 'a" where 179 "uminus_frac q \<equiv> Abs_Frac (- num q, denom q)" 180 181definition number_of_frac :: "int \<Rightarrow> 'a" where 182 "number_of_frac n \<equiv> Abs_Frac (n, 1)" 183 184definition inverse_frac :: "'a \<Rightarrow> 'a" where 185 "inverse_frac q \<equiv> frac (denom q) (num q)" 186 187definition less_frac :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where 188 [nitpick_simp]: "less_frac q r \<longleftrightarrow> num (plus_frac q (uminus_frac r)) < 0" 189 190definition less_eq_frac :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where 191 [nitpick_simp]: "less_eq_frac q r \<longleftrightarrow> num (plus_frac q (uminus_frac r)) \<le> 0" 192 193definition of_frac :: "'a \<Rightarrow> 'b::{inverse,ring_1}" where 194 "of_frac q \<equiv> of_int (num q) / of_int (denom q)" 195 196axiomatization wf_wfrec :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" 197 198definition wf_wfrec' :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where 199 [nitpick_simp]: "wf_wfrec' R F x = F (cut (wf_wfrec R F) R x) x" 200 201definition wfrec' :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where 202 "wfrec' R F x \<equiv> if wf R then wf_wfrec' R F x else THE y. wfrec_rel R (\<lambda>f x. F (cut f R x) x) x y" 203 204ML_file \<open>Tools/Nitpick/kodkod.ML\<close> 205ML_file \<open>Tools/Nitpick/kodkod_sat.ML\<close> 206ML_file \<open>Tools/Nitpick/nitpick_util.ML\<close> 207ML_file \<open>Tools/Nitpick/nitpick_hol.ML\<close> 208ML_file \<open>Tools/Nitpick/nitpick_mono.ML\<close> 209ML_file \<open>Tools/Nitpick/nitpick_preproc.ML\<close> 210ML_file \<open>Tools/Nitpick/nitpick_scope.ML\<close> 211ML_file \<open>Tools/Nitpick/nitpick_peephole.ML\<close> 212ML_file \<open>Tools/Nitpick/nitpick_rep.ML\<close> 213ML_file \<open>Tools/Nitpick/nitpick_nut.ML\<close> 214ML_file \<open>Tools/Nitpick/nitpick_kodkod.ML\<close> 215ML_file \<open>Tools/Nitpick/nitpick_model.ML\<close> 216ML_file \<open>Tools/Nitpick/nitpick.ML\<close> 217ML_file \<open>Tools/Nitpick/nitpick_commands.ML\<close> 218ML_file \<open>Tools/Nitpick/nitpick_tests.ML\<close> 219 220setup \<open> 221 Nitpick_HOL.register_ersatz_global 222 [(\<^const_name>\<open>card\<close>, \<^const_name>\<open>card'\<close>), 223 (\<^const_name>\<open>sum\<close>, \<^const_name>\<open>sum'\<close>), 224 (\<^const_name>\<open>fold_graph\<close>, \<^const_name>\<open>fold_graph'\<close>), 225 (\<^const_name>\<open>wf\<close>, \<^const_name>\<open>wf'\<close>), 226 (\<^const_name>\<open>wf_wfrec\<close>, \<^const_name>\<open>wf_wfrec'\<close>), 227 (\<^const_name>\<open>wfrec\<close>, \<^const_name>\<open>wfrec'\<close>)] 228\<close> 229 230hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The FunBox PairBox Word prod 231 refl' wf' card' sum' fold_graph' nat_gcd nat_lcm Frac Abs_Frac Rep_Frac 232 zero_frac one_frac num denom norm_frac frac plus_frac times_frac uminus_frac number_of_frac 233 inverse_frac less_frac less_eq_frac of_frac wf_wfrec wf_wfrec wfrec' 234 235hide_type (open) bisim_iterator fun_box pair_box unsigned_bit signed_bit word 236 237hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold prod_def refl'_def wf'_def 238 card'_def sum'_def The_psimp Eps_psimp case_unit_unfold case_nat_unfold 239 size_list_simp nat_lcm_def Frac_def zero_frac_def one_frac_def 240 num_def denom_def frac_def plus_frac_def times_frac_def uminus_frac_def 241 number_of_frac_def inverse_frac_def less_frac_def less_eq_frac_def of_frac_def wf_wfrec'_def 242 wfrec'_def 243 244end 245