src/HOL/Nitpick.thy
changeset 57992 2371bff894f9
parent 57242 25aff3b8d550
child 58152 6fe60a9a5bad
     1.1 --- a/src/HOL/Nitpick.thy	Tue Aug 19 09:34:30 2014 +0200
     1.2 +++ b/src/HOL/Nitpick.thy	Tue Aug 19 09:34:41 2014 +0200
     1.3 @@ -14,109 +14,105 @@
     1.4    "nitpick_params" :: thy_decl
     1.5  begin
     1.6  
     1.7 -typedecl bisim_iterator
     1.8 +datatype ('a, 'b) fun_box = FunBox "'a \<Rightarrow> 'b"
     1.9 +datatype ('a, 'b) pair_box = PairBox 'a 'b
    1.10 +datatype 'a word = Word "'a set"
    1.11  
    1.12 -axiomatization unknown :: 'a
    1.13 -           and is_unknown :: "'a \<Rightarrow> bool"
    1.14 -           and bisim :: "bisim_iterator \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.15 -           and bisim_iterator_max :: bisim_iterator
    1.16 -           and Quot :: "'a \<Rightarrow> 'b"
    1.17 -           and safe_The :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
    1.18 -
    1.19 -datatype ('a, 'b) fun_box = FunBox "('a \<Rightarrow> 'b)"
    1.20 -datatype ('a, 'b) pair_box = PairBox 'a 'b
    1.21 -
    1.22 +typedecl bisim_iterator
    1.23  typedecl unsigned_bit
    1.24  typedecl signed_bit
    1.25  
    1.26 -datatype 'a word = Word "('a set)"
    1.27 +consts
    1.28 +  unknown :: 'a
    1.29 +  is_unknown :: "'a \<Rightarrow> bool"
    1.30 +  bisim :: "bisim_iterator \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.31 +  bisim_iterator_max :: bisim_iterator
    1.32 +  Quot :: "'a \<Rightarrow> 'b"
    1.33 +  safe_The :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
    1.34  
    1.35  text {*
    1.36  Alternative definitions.
    1.37  *}
    1.38  
    1.39 -lemma Ex1_unfold [nitpick_unfold]:
    1.40 -"Ex1 P \<equiv> \<exists>x. {x. P x} = {x}"
    1.41 -apply (rule eq_reflection)
    1.42 -apply (simp add: Ex1_def set_eq_iff)
    1.43 -apply (rule iffI)
    1.44 - apply (erule exE)
    1.45 - apply (erule conjE)
    1.46 - apply (rule_tac x = x in exI)
    1.47 - apply (rule allI)
    1.48 - apply (rename_tac y)
    1.49 - apply (erule_tac x = y in allE)
    1.50 -by auto
    1.51 +lemma Ex1_unfold[nitpick_unfold]: "Ex1 P \<equiv> \<exists>x. {x. P x} = {x}"
    1.52 +  apply (rule eq_reflection)
    1.53 +  apply (simp add: Ex1_def set_eq_iff)
    1.54 +  apply (rule iffI)
    1.55 +   apply (erule exE)
    1.56 +   apply (erule conjE)
    1.57 +   apply (rule_tac x = x in exI)
    1.58 +   apply (rule allI)
    1.59 +   apply (rename_tac y)
    1.60 +   apply (erule_tac x = y in allE)
    1.61 +  by auto
    1.62  
    1.63 -lemma rtrancl_unfold [nitpick_unfold]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>="
    1.64 +lemma rtrancl_unfold[nitpick_unfold]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>="
    1.65    by (simp only: rtrancl_trancl_reflcl)
    1.66  
    1.67 -lemma rtranclp_unfold [nitpick_unfold]:
    1.68 -"rtranclp r a b \<equiv> (a = b \<or> tranclp r a b)"
    1.69 -by (rule eq_reflection) (auto dest: rtranclpD)
    1.70 +lemma rtranclp_unfold[nitpick_unfold]: "rtranclp r a b \<equiv> (a = b \<or> tranclp r a b)"
    1.71 +  by (rule eq_reflection) (auto dest: rtranclpD)
    1.72  
    1.73 -lemma tranclp_unfold [nitpick_unfold]:
    1.74 -"tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}"
    1.75 -by (simp add: trancl_def)
    1.76 +lemma tranclp_unfold[nitpick_unfold]:
    1.77 +  "tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}"
    1.78 +  by (simp add: trancl_def)
    1.79  
    1.80  lemma [nitpick_simp]:
    1.81 -"of_nat n = (if n = 0 then 0 else 1 + of_nat (n - 1))"
    1.82 -by (cases n) auto
    1.83 +  "of_nat n = (if n = 0 then 0 else 1 + of_nat (n - 1))"
    1.84 +  by (cases n) auto
    1.85  
    1.86  definition prod :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
    1.87 -"prod A B = {(a, b). a \<in> A \<and> b \<in> B}"
    1.88 +  "prod A B = {(a, b). a \<in> A \<and> b \<in> B}"
    1.89  
    1.90  definition refl' :: "('a \<times> 'a) set \<Rightarrow> bool" where
    1.91 -"refl' r \<equiv> \<forall>x. (x, x) \<in> r"
    1.92 +  "refl' r \<equiv> \<forall>x. (x, x) \<in> r"
    1.93  
    1.94  definition wf' :: "('a \<times> 'a) set \<Rightarrow> bool" where
    1.95 -"wf' r \<equiv> acyclic r \<and> (finite r \<or> unknown)"
    1.96 +  "wf' r \<equiv> acyclic r \<and> (finite r \<or> unknown)"
    1.97  
    1.98  definition card' :: "'a set \<Rightarrow> nat" where
    1.99 -"card' A \<equiv> if finite A then length (SOME xs. set xs = A \<and> distinct xs) else 0"
   1.100 +  "card' A \<equiv> if finite A then length (SOME xs. set xs = A \<and> distinct xs) else 0"
   1.101  
   1.102  definition setsum' :: "('a \<Rightarrow> 'b\<Colon>comm_monoid_add) \<Rightarrow> 'a set \<Rightarrow> 'b" where
   1.103 -"setsum' f A \<equiv> if finite A then listsum (map f (SOME xs. set xs = A \<and> distinct xs)) else 0"
   1.104 +  "setsum' f A \<equiv> if finite A then listsum (map f (SOME xs. set xs = A \<and> distinct xs)) else 0"
   1.105  
   1.106  inductive fold_graph' :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool" where
   1.107 -"fold_graph' f z {} z" |
   1.108 -"\<lbrakk>x \<in> A; fold_graph' f z (A - {x}) y\<rbrakk> \<Longrightarrow> fold_graph' f z A (f x y)"
   1.109 +  "fold_graph' f z {} z" |
   1.110 +  "\<lbrakk>x \<in> A; fold_graph' f z (A - {x}) y\<rbrakk> \<Longrightarrow> fold_graph' f z A (f x y)"
   1.111  
   1.112  text {*
   1.113  The following lemmas are not strictly necessary but they help the
   1.114  \textit{specialize} optimization.
   1.115  *}
   1.116  
   1.117 -lemma The_psimp [nitpick_psimp]:
   1.118 -  "P = (op =) x \<Longrightarrow> The P = x"
   1.119 +lemma The_psimp[nitpick_psimp]: "P = (op =) x \<Longrightarrow> The P = x"
   1.120    by auto
   1.121  
   1.122 -lemma Eps_psimp [nitpick_psimp]:
   1.123 -"\<lbrakk>P x; \<not> P y; Eps P = y\<rbrakk> \<Longrightarrow> Eps P = x"
   1.124 -apply (cases "P (Eps P)")
   1.125 - apply auto
   1.126 -apply (erule contrapos_np)
   1.127 -by (rule someI)
   1.128 +lemma Eps_psimp[nitpick_psimp]:
   1.129 +  "\<lbrakk>P x; \<not> P y; Eps P = y\<rbrakk> \<Longrightarrow> Eps P = x"
   1.130 +  apply (cases "P (Eps P)")
   1.131 +   apply auto
   1.132 +  apply (erule contrapos_np)
   1.133 +  by (rule someI)
   1.134  
   1.135 -lemma case_unit_unfold [nitpick_unfold]:
   1.136 -"case_unit x u \<equiv> x"
   1.137 -apply (subgoal_tac "u = ()")
   1.138 - apply (simp only: unit.case)
   1.139 -by simp
   1.140 +lemma case_unit_unfold[nitpick_unfold]:
   1.141 +  "case_unit x u \<equiv> x"
   1.142 +  apply (subgoal_tac "u = ()")
   1.143 +   apply (simp only: unit.case)
   1.144 +  by simp
   1.145  
   1.146 -declare unit.case [nitpick_simp del]
   1.147 +declare unit.case[nitpick_simp del]
   1.148  
   1.149 -lemma case_nat_unfold [nitpick_unfold]:
   1.150 -"case_nat x f n \<equiv> if n = 0 then x else f (n - 1)"
   1.151 -apply (rule eq_reflection)
   1.152 -by (cases n) auto
   1.153 +lemma case_nat_unfold[nitpick_unfold]:
   1.154 +  "case_nat x f n \<equiv> if n = 0 then x else f (n - 1)"
   1.155 +  apply (rule eq_reflection)
   1.156 +  by (cases n) auto
   1.157  
   1.158 -declare nat.case [nitpick_simp del]
   1.159 +declare nat.case[nitpick_simp del]
   1.160  
   1.161 -lemma size_list_simp [nitpick_simp]:
   1.162 -"size_list f xs = (if xs = [] then 0 else Suc (f (hd xs) + size_list f (tl xs)))"
   1.163 -"size xs = (if xs = [] then 0 else Suc (size (tl xs)))"
   1.164 -by (cases xs) auto
   1.165 +lemma size_list_simp[nitpick_simp]:
   1.166 +  "size_list f xs = (if xs = [] then 0 else Suc (f (hd xs) + size_list f (tl xs)))"
   1.167 +  "size xs = (if xs = [] then 0 else Suc (size (tl xs)))"
   1.168 +  by (cases xs) auto
   1.169  
   1.170  text {*
   1.171  Auxiliary definitions used to provide an alternative representation for
   1.172 @@ -124,89 +120,89 @@
   1.173  *}
   1.174  
   1.175  function nat_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
   1.176 -[simp del]: "nat_gcd x y = (if y = 0 then x else nat_gcd y (x mod y))"
   1.177 -by auto
   1.178 -termination
   1.179 -apply (relation "measure (\<lambda>(x, y). x + y + (if y > x then 1 else 0))")
   1.180 - apply auto
   1.181 - apply (metis mod_less_divisor xt1(9))
   1.182 -by (metis mod_mod_trivial mod_self nat_neq_iff xt1(10))
   1.183 +  "nat_gcd x y = (if y = 0 then x else nat_gcd y (x mod y))"
   1.184 +  by auto
   1.185 +  termination
   1.186 +  apply (relation "measure (\<lambda>(x, y). x + y + (if y > x then 1 else 0))")
   1.187 +   apply auto
   1.188 +   apply (metis mod_less_divisor xt1(9))
   1.189 +  by (metis mod_mod_trivial mod_self nat_neq_iff xt1(10))
   1.190 +
   1.191 +declare nat_gcd.simps[simp del]
   1.192  
   1.193  definition nat_lcm :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
   1.194 -"nat_lcm x y = x * y div (nat_gcd x y)"
   1.195 +  "nat_lcm x y = x * y div (nat_gcd x y)"
   1.196  
   1.197  definition int_gcd :: "int \<Rightarrow> int \<Rightarrow> int" where
   1.198 -"int_gcd x y = int (nat_gcd (nat (abs x)) (nat (abs y)))"
   1.199 +  "int_gcd x y = int (nat_gcd (nat (abs x)) (nat (abs y)))"
   1.200  
   1.201  definition int_lcm :: "int \<Rightarrow> int \<Rightarrow> int" where
   1.202 -"int_lcm x y = int (nat_lcm (nat (abs x)) (nat (abs y)))"
   1.203 +  "int_lcm x y = int (nat_lcm (nat (abs x)) (nat (abs y)))"
   1.204  
   1.205  definition Frac :: "int \<times> int \<Rightarrow> bool" where
   1.206 -"Frac \<equiv> \<lambda>(a, b). b > 0 \<and> int_gcd a b = 1"
   1.207 +  "Frac \<equiv> \<lambda>(a, b). b > 0 \<and> int_gcd a b = 1"
   1.208  
   1.209 -axiomatization
   1.210 -  Abs_Frac :: "int \<times> int \<Rightarrow> 'a" and
   1.211 +consts
   1.212 +  Abs_Frac :: "int \<times> int \<Rightarrow> 'a"
   1.213    Rep_Frac :: "'a \<Rightarrow> int \<times> int"
   1.214  
   1.215  definition zero_frac :: 'a where
   1.216 -"zero_frac \<equiv> Abs_Frac (0, 1)"
   1.217 +  "zero_frac \<equiv> Abs_Frac (0, 1)"
   1.218  
   1.219  definition one_frac :: 'a where
   1.220 -"one_frac \<equiv> Abs_Frac (1, 1)"
   1.221 +  "one_frac \<equiv> Abs_Frac (1, 1)"
   1.222  
   1.223  definition num :: "'a \<Rightarrow> int" where
   1.224 -"num \<equiv> fst o Rep_Frac"
   1.225 +  "num \<equiv> fst o Rep_Frac"
   1.226  
   1.227  definition denom :: "'a \<Rightarrow> int" where
   1.228 -"denom \<equiv> snd o Rep_Frac"
   1.229 +  "denom \<equiv> snd o Rep_Frac"
   1.230  
   1.231  function norm_frac :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
   1.232 -[simp del]: "norm_frac a b = (if b < 0 then norm_frac (- a) (- b)
   1.233 -                              else if a = 0 \<or> b = 0 then (0, 1)
   1.234 -                              else let c = int_gcd a b in (a div c, b div c))"
   1.235 -by pat_completeness auto
   1.236 -termination by (relation "measure (\<lambda>(_, b). if b < 0 then 1 else 0)") auto
   1.237 +  "norm_frac a b =
   1.238 +    (if b < 0 then norm_frac (- a) (- b)
   1.239 +     else if a = 0 \<or> b = 0 then (0, 1)
   1.240 +     else let c = int_gcd a b in (a div c, b div c))"
   1.241 +  by pat_completeness auto
   1.242 +  termination by (relation "measure (\<lambda>(_, b). if b < 0 then 1 else 0)") auto
   1.243 +
   1.244 +declare norm_frac.simps[simp del]
   1.245  
   1.246  definition frac :: "int \<Rightarrow> int \<Rightarrow> 'a" where
   1.247 -"frac a b \<equiv> Abs_Frac (norm_frac a b)"
   1.248 +  "frac a b \<equiv> Abs_Frac (norm_frac a b)"
   1.249  
   1.250  definition plus_frac :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
   1.251 -[nitpick_simp]:
   1.252 -"plus_frac q r = (let d = int_lcm (denom q) (denom r) in
   1.253 -                    frac (num q * (d div denom q) + num r * (d div denom r)) d)"
   1.254 +  [nitpick_simp]: "plus_frac q r = (let d = int_lcm (denom q) (denom r) in
   1.255 +    frac (num q * (d div denom q) + num r * (d div denom r)) d)"
   1.256  
   1.257  definition times_frac :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
   1.258 -[nitpick_simp]:
   1.259 -"times_frac q r = frac (num q * num r) (denom q * denom r)"
   1.260 +  [nitpick_simp]: "times_frac q r = frac (num q * num r) (denom q * denom r)"
   1.261  
   1.262  definition uminus_frac :: "'a \<Rightarrow> 'a" where
   1.263 -"uminus_frac q \<equiv> Abs_Frac (- num q, denom q)"
   1.264 +  "uminus_frac q \<equiv> Abs_Frac (- num q, denom q)"
   1.265  
   1.266  definition number_of_frac :: "int \<Rightarrow> 'a" where
   1.267 -"number_of_frac n \<equiv> Abs_Frac (n, 1)"
   1.268 +  "number_of_frac n \<equiv> Abs_Frac (n, 1)"
   1.269  
   1.270  definition inverse_frac :: "'a \<Rightarrow> 'a" where
   1.271 -"inverse_frac q \<equiv> frac (denom q) (num q)"
   1.272 +  "inverse_frac q \<equiv> frac (denom q) (num q)"
   1.273  
   1.274  definition less_frac :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
   1.275 -[nitpick_simp]:
   1.276 -"less_frac q r \<longleftrightarrow> num (plus_frac q (uminus_frac r)) < 0"
   1.277 +  [nitpick_simp]: "less_frac q r \<longleftrightarrow> num (plus_frac q (uminus_frac r)) < 0"
   1.278  
   1.279  definition less_eq_frac :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
   1.280 -[nitpick_simp]:
   1.281 -"less_eq_frac q r \<longleftrightarrow> num (plus_frac q (uminus_frac r)) \<le> 0"
   1.282 +  [nitpick_simp]: "less_eq_frac q r \<longleftrightarrow> num (plus_frac q (uminus_frac r)) \<le> 0"
   1.283  
   1.284  definition of_frac :: "'a \<Rightarrow> 'b\<Colon>{inverse,ring_1}" where
   1.285 -"of_frac q \<equiv> of_int (num q) / of_int (denom q)"
   1.286 +  "of_frac q \<equiv> of_int (num q) / of_int (denom q)"
   1.287  
   1.288  axiomatization wf_wfrec :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
   1.289  
   1.290  definition wf_wfrec' :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
   1.291 -[nitpick_simp]: "wf_wfrec' R F x = F (cut (wf_wfrec R F) R x) x"
   1.292 +  [nitpick_simp]: "wf_wfrec' R F x = F (cut (wf_wfrec R F) R x) x"
   1.293  
   1.294  definition wfrec' ::  "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
   1.295 -"wfrec' R F x \<equiv> if wf R then wf_wfrec' R F x
   1.296 -                else THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
   1.297 +  "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"
   1.298  
   1.299  ML_file "Tools/Nitpick/kodkod.ML"
   1.300  ML_file "Tools/Nitpick/kodkod_sat.ML"
   1.301 @@ -234,20 +230,18 @@
   1.302       (@{const_name wfrec}, @{const_name wfrec'})]
   1.303  *}
   1.304  
   1.305 -hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The
   1.306 -    FunBox PairBox Word prod refl' wf' card' setsum'
   1.307 -    fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac
   1.308 -    one_frac num denom norm_frac frac plus_frac times_frac uminus_frac
   1.309 -    number_of_frac inverse_frac less_frac less_eq_frac of_frac wf_wfrec wf_wfrec
   1.310 -    wfrec'
   1.311 +hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The FunBox PairBox Word prod
   1.312 +  refl' wf' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac
   1.313 +  zero_frac one_frac num denom norm_frac frac plus_frac times_frac uminus_frac number_of_frac
   1.314 +  inverse_frac less_frac less_eq_frac of_frac wf_wfrec wf_wfrec wfrec'
   1.315 +
   1.316  hide_type (open) bisim_iterator fun_box pair_box unsigned_bit signed_bit word
   1.317 -hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold
   1.318 -    prod_def refl'_def wf'_def card'_def setsum'_def
   1.319 -    fold_graph'_def The_psimp Eps_psimp case_unit_unfold case_nat_unfold
   1.320 -    size_list_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
   1.321 -    zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def
   1.322 -    plus_frac_def times_frac_def uminus_frac_def number_of_frac_def
   1.323 -    inverse_frac_def less_frac_def less_eq_frac_def of_frac_def wf_wfrec'_def
   1.324 -    wfrec'_def
   1.325 +
   1.326 +hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold prod_def refl'_def wf'_def
   1.327 +  card'_def setsum'_def fold_graph'_def The_psimp Eps_psimp case_unit_unfold case_nat_unfold
   1.328 +  size_list_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def
   1.329 +  num_def denom_def norm_frac_def frac_def plus_frac_def times_frac_def uminus_frac_def
   1.330 +  number_of_frac_def inverse_frac_def less_frac_def less_eq_frac_def of_frac_def wf_wfrec'_def
   1.331 +  wfrec'_def
   1.332  
   1.333  end