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