equal
deleted
inserted
replaced
74 done |
74 done |
75 |
75 |
76 |
76 |
77 subsection {* Nitpick setup *} |
77 subsection {* Nitpick setup *} |
78 |
78 |
79 axiomatization wf_wfrec :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
79 axiomatization wf_wfrec :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
80 |
80 |
81 definition wf_wfrec' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where |
81 definition wf_wfrec' :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where |
82 [nitpick_simp]: "wf_wfrec' R F x = F (cut (wf_wfrec R F) R x) x" |
82 [nitpick_simp]: "wf_wfrec' R F x = F (cut (wf_wfrec R F) R x) x" |
83 |
83 |
84 definition wfrec' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where |
84 definition wfrec' :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where |
85 "wfrec' R F x \<equiv> if wf R then wf_wfrec' R F x |
85 "wfrec' R F x \<equiv> if wf R then wf_wfrec' R F x |
86 else THE y. wfrec_rel R (%f x. F (cut f R x) x) x y" |
86 else THE y. wfrec_rel R (%f x. F (cut f R x) x) x y" |
87 |
87 |
88 setup {* |
88 setup {* |
89 Nitpick_HOL.register_ersatz_global |
89 Nitpick_HOL.register_ersatz_global |