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
```