扩大偏函数的域

Question

对不准确的标题表示歉意。

我定义了一个计算fixed-points的函数，比如

function (domintros) "fix" :: "(env ⇒ env) ⇒ env ⇒ env"
where
  "fix f m n = (if f m n = m n then m n else fix f (f m) n)"
by pat_completeness blast

其中 type_synonym env = char list ⇀ val 只是一个通常的（显式）部分函数（映射）。

我设法证明了在某些条件下终止，但现在我想证明以下引理，它似乎很简单：

lemma fix_dom_iter [intro]:
  assumes "fix_dom (f, m, n)"
  shows "fix_dom (f, f m, n)"
oops

但只是表面上的，因为我找不到如何证明它。似乎没有 fix.p* 定理可以满足我的要求。

困难的情况显然是~(f m n = m n)。

任何指针。如何证明引理？它甚至可以证明吗？

编辑：

我认为 fix.domintros 应该是等价而不是蕴涵。那样的话，我就能够证明我想要什么，而且它实际上应该是可靠的。问题是，这是否适用于任何类型的偏函数。

Answer 1

不幸的是你的引理不成立。考虑以下输入变体，我将环境更改为仅从 bool 到 bool 的函数。

type_synonym env = "bool ⇒ bool"
function (domintros) "fix" :: "(env ⇒ env) ⇒ env ⇒ env"
where
  "fix f m n = (if f m n = m n then m n else fix f (f m) n)"
by pat_completeness blast

我也定义了对应的可执行偏函数

partial_function (tailrec) "fix2" :: "(env ⇒ env) ⇒ env ⇒ env"
where
  [code]: "fix2 f m n = (if f m n = m n then m n else fix2 f (f m) n)"

现在 f、m 和 n 的以下见证表明您的说法是不正确的。

definition "f m = (if m True = m False then Not else Not o m)"  
definition "m n = True" 
definition "n = False"

fix_dom (f,m,n)确实成立。

lemma "fix_dom (f,m,n)" unfolding f_def[abs_def] m_def[abs_def] n_def
  by (auto intro: fix.domintros)

但是，fix_dom (f,f m,n) 不成立，因为可以通过非终止计算观察到。

value (code) "fix2 f (f m) n"

扩大偏函数的域

Widening the domain of a partial function

isabelle