header {* Unconstrained Fixpoint Evaluation of @{text wfrec} Is Inconsistent *} 

theory Wfrec_Codegen_Inconsistency 
imports Main
begin


consts_code
  "wfrec"   ("\<module>wfrec?")
attach {*
  fun wfrec f x = f (wfrec f) x;
*}

definition
  "F f x = (case x of 
     0 \<Rightarrow> True
   | Suc 0 \<Rightarrow> False
   | Suc (Suc n) \<Rightarrow> (f 0 = f (Suc 0)))" 

definition "f = wfrec {} F"

lemma LFalse: "f 2 = False" by evaluation

lemma wfrec_empty: "wfrec {} H a = H (\<lambda>x. undefined) a" 
proof -
  from wfrec[OF wf_empty]
  have "wfrec {} H a = H (cut (wfrec {} H) {} a) a" .
  also have "\<dots> = H (\<lambda>x. undefined) a"
    unfolding cut_def by simp
  finally show ?thesis . 
qed

lemma LTrue: "f 2 = True"
  unfolding f_def
  unfolding wfrec_empty
  by (simp add: F_def)

lemma "False"
  by (fold LFalse) (simp add: LTrue)

end

