一些选项，让和原因重写器不简化的情况

Question

在 Isabelle 中，我必须遵循以下证明状态：

proof (prove)
using this:
  find (λc. length c = 1) f = Some [l]

goal (1 subgoal):
 1. fst (units_propagate f) = fst (units_propagate (update_formula f (atom_of l) (is_pos l)))

如果您将假设与一些简化相结合，我很确定这是真的。为了说明这一点，我可以使用 HOL-Library 重写

units_propagate f

调用。重写：

apply(rewrite at "units_propagate f" units_propagate.simps)
===========================================================
proof (prove)
goal (1 subgoal):
 1. find (λc. length c = 1) f = Some [l] ⟹
    fst (case find (λc. length c = 1) f of None ⇒ (f, Map.empty)
         | Some [l] ⇒
             let (f', e) = units_propagate (update_formula f (atom_of l) (is_pos l))
             in (f', e(atom_of l ↦ is_pos l))) =
    fst (units_propagate (update_formula f (atom_of l) (is_pos l)))

现在我很确定，如果你使用这个假设，

case of

表达式将简化为只有

Some

的情况。然后，使用

fst

允许只保留元组的第一个元素，导致以下证明状态（假设的，因为我无法产生）：

proof (prove)
goal (1 subgoal):
 1. find (λc. length c = 1) f = Some [l] ⟹
    fst (units_propagate (update_formula f (atom_of l) (is_pos l))) =
    fst (units_propagate (update_formula f (atom_of l) (is_pos l)))

很明显这是相等的。因为我可以写下这些步骤，所以我希望 simp 的调用应该能够解决它。但它不能。使用

try

，经过比较长的时间后，发现如下调用：

by (metis (no_types, lifting) case_prod_unfold fst_conv list.simps(4) list.simps(5) option.simps(5)) 

那行得通。但这很痛苦，我不明白。有人可以阐明为什么这很困难吗？

我怀疑伊莎贝尔在将

= Some [l]

假设与简化

l

表达式的过程中创建的

case of

统一起来时遇到了麻烦。但我不知道如何向伊莎贝尔表明应该合并这两个变量。如果重要，这里是

units_propagate

的完整定义：

function (sequential) units_propagate :: "'a formula ⇒ 'a formula × 'a env" where
"units_propagate f =
  (case find (λc. length c = 1) f of
      Some [l] ⇒ 
        let (f', e) = units_propagate (update_formula f (atom_of l) (is_pos l)) in
        (f', e(atom_of l ↦ is_pos l))
    | None ⇒ (f, Map.empty)
)"
  by(simp_all)
termination
  apply(relation "measure size_formula")
   apply(simp)
  using update_formula_decreases_units_propagate by auto

编辑：好的，在盯着

metis

调用之后，我设法将其分解为以下证明脚本以供检查：

    apply(simp only: case_prod_unfold)
    apply(simp only: option.simps)
    apply(simp only: list.simps)
    apply(meson fstI)
    done

事实上，它似乎一层一层地剥离所有数据类型。但我觉得通常情况下，isabelle 可以顺利完成我的数据类型分层。但这里似乎很难。有人可以解释为什么吗？有没有一种方法可以让 isabelle 更轻松地重组我的功能？