28 bisim :: "bisim_iterator \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
28 bisim :: "bisim_iterator \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
29 bisim_iterator_max :: bisim_iterator |
29 bisim_iterator_max :: bisim_iterator |
30 Quot :: "'a \<Rightarrow> 'b" |
30 Quot :: "'a \<Rightarrow> 'b" |
31 safe_The :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" |
31 safe_The :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" |
32 |
32 |
33 text {* |
33 text \<open> |
34 Alternative definitions. |
34 Alternative definitions. |
35 *} |
35 \<close> |
36 |
36 |
37 lemma Ex1_unfold[nitpick_unfold]: "Ex1 P \<equiv> \<exists>x. {x. P x} = {x}" |
37 lemma Ex1_unfold[nitpick_unfold]: "Ex1 P \<equiv> \<exists>x. {x. P x} = {x}" |
38 apply (rule eq_reflection) |
38 apply (rule eq_reflection) |
39 apply (simp add: Ex1_def set_eq_iff) |
39 apply (simp add: Ex1_def set_eq_iff) |
40 apply (rule iffI) |
40 apply (rule iffI) |
77 |
77 |
78 inductive fold_graph' :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool" where |
78 inductive fold_graph' :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool" where |
79 "fold_graph' f z {} z" | |
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)" |
80 "\<lbrakk>x \<in> A; fold_graph' f z (A - {x}) y\<rbrakk> \<Longrightarrow> fold_graph' f z A (f x y)" |
81 |
81 |
82 text {* |
82 text \<open> |
83 The following lemmas are not strictly necessary but they help the |
83 The following lemmas are not strictly necessary but they help the |
84 \textit{specialize} optimization. |
84 \textit{specialize} optimization. |
85 *} |
85 \<close> |
86 |
86 |
87 lemma The_psimp[nitpick_psimp]: "P = (op =) x \<Longrightarrow> The P = x" |
87 lemma The_psimp[nitpick_psimp]: "P = (op =) x \<Longrightarrow> The P = x" |
88 by auto |
88 by auto |
89 |
89 |
90 lemma Eps_psimp[nitpick_psimp]: |
90 lemma Eps_psimp[nitpick_psimp]: |
112 lemma size_list_simp[nitpick_simp]: |
112 lemma size_list_simp[nitpick_simp]: |
113 "size_list f xs = (if xs = [] then 0 else Suc (f (hd xs) + size_list f (tl xs)))" |
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)))" |
114 "size xs = (if xs = [] then 0 else Suc (size (tl xs)))" |
115 by (cases xs) auto |
115 by (cases xs) auto |
116 |
116 |
117 text {* |
117 text \<open> |
118 Auxiliary definitions used to provide an alternative representation for |
118 Auxiliary definitions used to provide an alternative representation for |
119 @{text rat} and @{text real}. |
119 @{text rat} and @{text real}. |
120 *} |
120 \<close> |
121 |
121 |
122 function nat_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
122 function 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))" |
123 "nat_gcd x y = (if y = 0 then x else nat_gcd y (x mod y))" |
124 by auto |
124 by auto |
125 termination |
125 termination |
218 ML_file "Tools/Nitpick/nitpick_model.ML" |
218 ML_file "Tools/Nitpick/nitpick_model.ML" |
219 ML_file "Tools/Nitpick/nitpick.ML" |
219 ML_file "Tools/Nitpick/nitpick.ML" |
220 ML_file "Tools/Nitpick/nitpick_commands.ML" |
220 ML_file "Tools/Nitpick/nitpick_commands.ML" |
221 ML_file "Tools/Nitpick/nitpick_tests.ML" |
221 ML_file "Tools/Nitpick/nitpick_tests.ML" |
222 |
222 |
223 setup {* |
223 setup \<open> |
224 Nitpick_HOL.register_ersatz_global |
224 Nitpick_HOL.register_ersatz_global |
225 [(@{const_name card}, @{const_name card'}), |
225 [(@{const_name card}, @{const_name card'}), |
226 (@{const_name setsum}, @{const_name setsum'}), |
226 (@{const_name setsum}, @{const_name setsum'}), |
227 (@{const_name fold_graph}, @{const_name fold_graph'}), |
227 (@{const_name fold_graph}, @{const_name fold_graph'}), |
228 (@{const_name wf}, @{const_name wf'}), |
228 (@{const_name wf}, @{const_name wf'}), |
229 (@{const_name wf_wfrec}, @{const_name wf_wfrec'}), |
229 (@{const_name wf_wfrec}, @{const_name wf_wfrec'}), |
230 (@{const_name wfrec}, @{const_name wfrec'})] |
230 (@{const_name wfrec}, @{const_name wfrec'})] |
231 *} |
231 \<close> |
232 |
232 |
233 hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The FunBox PairBox Word prod |
233 hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The FunBox PairBox Word prod |
234 refl' wf' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac |
234 refl' wf' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac |
235 zero_frac one_frac num denom norm_frac frac plus_frac times_frac uminus_frac number_of_frac |
235 zero_frac one_frac num denom norm_frac frac plus_frac times_frac uminus_frac number_of_frac |
236 inverse_frac less_frac less_eq_frac of_frac wf_wfrec wf_wfrec wfrec' |
236 inverse_frac less_frac less_eq_frac of_frac wf_wfrec wf_wfrec wfrec' |