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