src/HOL/Nitpick.thy
changeset 44013 5cfc1c36ae97
parent 42064 f4e53c8630c0
child 44016 51184010c609
     1.1 --- a/src/HOL/Nitpick.thy	Tue Aug 02 10:03:14 2011 +0200
     1.2 +++ b/src/HOL/Nitpick.thy	Tue Aug 02 10:36:50 2011 +0200
     1.3 @@ -82,15 +82,6 @@
     1.4  definition wf' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
     1.5  "wf' r \<equiv> acyclic r \<and> (finite r \<or> unknown)"
     1.6  
     1.7 -axiomatization wf_wfrec :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
     1.8 -
     1.9 -definition wf_wfrec' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
    1.10 -[nitpick_simp]: "wf_wfrec' R F x = F (Recdef.cut (wf_wfrec R F) R x) x"
    1.11 -
    1.12 -definition wfrec' ::  "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
    1.13 -"wfrec' R F x \<equiv> if wf R then wf_wfrec' R F x
    1.14 -                else THE y. wfrec_rel R (%f x. F (Recdef.cut f R x) x) x y"
    1.15 -
    1.16  definition card' :: "('a \<Rightarrow> bool) \<Rightarrow> nat" where
    1.17  "card' A \<equiv> if finite A then length (SOME xs. set xs = A \<and> distinct xs) else 0"
    1.18  
    1.19 @@ -238,14 +229,14 @@
    1.20  setup {* Nitpick_Isar.setup *}
    1.21  
    1.22  hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The
    1.23 -    FunBox PairBox Word prod refl' wf' wf_wfrec wf_wfrec' wfrec' card' setsum'
    1.24 +    FunBox PairBox Word prod refl' wf' card' setsum'
    1.25      fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac
    1.26      one_frac num denom norm_frac frac plus_frac times_frac uminus_frac
    1.27      number_of_frac inverse_frac less_frac less_eq_frac of_frac
    1.28  hide_type (open) iota bisim_iterator fun_box pair_box unsigned_bit signed_bit
    1.29      word
    1.30  hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold
    1.31 -    prod_def refl'_def wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def
    1.32 +    prod_def refl'_def wf'_def card'_def setsum'_def
    1.33      fold_graph'_def The_psimp Eps_psimp unit_case_unfold nat_case_unfold
    1.34      list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
    1.35      zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def