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