src/HOL/Nitpick.thy
 changeset 55017 2df6ad1dbd66 parent 54555 e8c5e95d338b child 55082 e60036c1c248
```     1.1 --- a/src/HOL/Nitpick.thy	Thu Jan 16 15:47:33 2014 +0100
1.2 +++ b/src/HOL/Nitpick.thy	Thu Jan 16 16:20:17 2014 +0100
1.3 @@ -8,7 +8,7 @@
1.4  header {* Nitpick: Yet Another Counterexample Generator for Isabelle/HOL *}
1.5
1.6  theory Nitpick
1.7 -imports Map Record Sledgehammer
1.8 +imports Map Record Sledgehammer Wfrec
1.9  keywords "nitpick" :: diag and "nitpick_params" :: thy_decl
1.10  begin
1.11
1.12 @@ -197,6 +197,15 @@
1.13  definition of_frac :: "'a \<Rightarrow> 'b\<Colon>{inverse,ring_1}" where
1.14  "of_frac q \<equiv> of_int (num q) / of_int (denom q)"
1.15
1.16 +axiomatization wf_wfrec :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
1.17 +
1.18 +definition wf_wfrec' :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
1.19 +[nitpick_simp]: "wf_wfrec' R F x = F (cut (wf_wfrec R F) R x) x"
1.20 +
1.21 +definition wfrec' ::  "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
1.22 +"wfrec' R F x \<equiv> if wf R then wf_wfrec' R F x
1.23 +                else THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
1.24 +
1.25  ML_file "Tools/Nitpick/kodkod.ML"
1.26  ML_file "Tools/Nitpick/kodkod_sat.ML"
1.27  ML_file "Tools/Nitpick/nitpick_util.ML"
1.28 @@ -218,14 +227,17 @@
1.29      [(@{const_name card}, @{const_name card'}),
1.30       (@{const_name setsum}, @{const_name setsum'}),
1.31       (@{const_name fold_graph}, @{const_name fold_graph'}),
1.32 -     (@{const_name wf}, @{const_name wf'})]
1.33 +     (@{const_name wf}, @{const_name wf'}),
1.34 +     (@{const_name wf_wfrec}, @{const_name wf_wfrec'}),
1.35 +     (@{const_name wfrec}, @{const_name wfrec'})]
1.36  *}
1.37
1.38  hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The
1.39      FunBox PairBox Word prod refl' wf' card' setsum'
1.40      fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac
1.41      one_frac num denom norm_frac frac plus_frac times_frac uminus_frac
1.42 -    number_of_frac inverse_frac less_frac less_eq_frac of_frac
1.43 +    number_of_frac inverse_frac less_frac less_eq_frac of_frac wf_wfrec wf_wfrec
1.44 +    wfrec'
1.45  hide_type (open) bisim_iterator fun_box pair_box unsigned_bit signed_bit word
1.46  hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold
1.47      prod_def refl'_def wf'_def card'_def setsum'_def
1.48 @@ -233,6 +245,7 @@
1.49      list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
1.50      zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def
1.51      plus_frac_def times_frac_def uminus_frac_def number_of_frac_def
1.52 -    inverse_frac_def less_frac_def less_eq_frac_def of_frac_def
1.53 +    inverse_frac_def less_frac_def less_eq_frac_def of_frac_def wf_wfrec'_def
1.54 +    wfrec'_def
1.55
1.56  end
```