src/HOL/Wfrec.thy
changeset 55017 2df6ad1dbd66
parent 55016 9fc7e7753d86
child 55210 d1e3b708d74b
     1.1 --- a/src/HOL/Wfrec.thy	Thu Jan 16 15:47:33 2014 +0100
     1.2 +++ b/src/HOL/Wfrec.thy	Thu Jan 16 16:20:17 2014 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  header {* Well-Founded Recursion Combinator *}
     1.5  
     1.6  theory Wfrec
     1.7 -imports Main
     1.8 +imports Wellfounded
     1.9  begin
    1.10  
    1.11  inductive
    1.12 @@ -74,26 +74,6 @@
    1.13  done
    1.14  
    1.15  
    1.16 -subsection {* Nitpick setup *}
    1.17 -
    1.18 -axiomatization wf_wfrec :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    1.19 -
    1.20 -definition wf_wfrec' :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
    1.21 -[nitpick_simp]: "wf_wfrec' R F x = F (cut (wf_wfrec R F) R x) x"
    1.22 -
    1.23 -definition wfrec' ::  "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
    1.24 -"wfrec' R F x \<equiv> if wf R then wf_wfrec' R F x
    1.25 -                else THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
    1.26 -
    1.27 -setup {*
    1.28 -  Nitpick_HOL.register_ersatz_global
    1.29 -    [(@{const_name wf_wfrec}, @{const_name wf_wfrec'}),
    1.30 -     (@{const_name wfrec}, @{const_name wfrec'})]
    1.31 -*}
    1.32 -
    1.33 -hide_const (open) wf_wfrec wf_wfrec' wfrec'
    1.34 -hide_fact (open) wf_wfrec'_def wfrec'_def
    1.35 -
    1.36  subsection {* Wellfoundedness of @{text same_fst} *}
    1.37  
    1.38  definition