如何使用单值关系自动重写目标

Question

单值关系(由Relation理论中的single_valued定义)允许从隶属关系中推导等式。我想知道是否有一种方法可以利用这一点来重写目标中的术语(然后合并这些成员关系)。

作为一个例子，这里有一个目标，如果没有辅助定理，就不能用自动或力来解决:

lemma
  assumes "single_valued A"
  assumes "(a,b) ∈ A" and "(a,b') ∈ A"
  shows "b = b'"
using assms
by (metis single_valued_def)

这里的等式直接存在于目标中，但如果能在假设中重写就更好了。

同样，我在这里讨论的是对的集合，但我有一个更复杂的应用，它是另一种具有类似性质的关系，其中这种假设是常见的，然后我正在寻找一种方法来简化它们。

在我看来，自动方法可以从这样的特性中受益匪浅。

我之前已经写了一些simprocs，在我看来，我们可以在这里使用它们，如果我们可以访问一组假设，一旦simproc被触发，我不知道这是否可能。例如，一旦"(a,b)∈a"触发了simproc，我们是否可以检查是否有任何假设包含"(a，_)∈a"?但这可能太昂贵了……

Answer 1

下面是你想要的一个simproc:

lemma single_valuedD_eq:
  "⟦ single_valued A; (x, a) ∈ A ⟧ ⟹ (x, b) ∈ A ⟷ b = a"
by(auto dest: single_valuedD)
simproc_setup single_valued ("(x, y) ∈ A") = {*
  (fn phi => fn ctxt => fn redex => case term_of redex of
    Const (@{const_name "Set.member"},
         Type (@{type_name fun},
           [Txy as Type (@{type_name prod}, [Tx, Ty]),
            Type (@{type_name fun}, [TA, _])])) $
      (Const (@{const_name "Pair"}, _) $ tx $ ty) $
      tA =>
    let
      val thy = Proof_Context.theory_of ctxt;
      val prems = Simplifier.prems_of ctxt;
      fun mk_stmt t = t |> HOLogic.mk_Trueprop |> Thm.cterm_of thy |> Goal.init
      fun mk_thm tac t =
        case SINGLE (tac 1) (mk_stmt t) of
          SOME thm => SOME (Goal.finish (Syntax.init_pretty_global (Thm.theory_of_thm thm)) thm)
        | NONE => NONE;
      val svA = Const (@{const_name single_valued}, TA --> @{typ bool}) $ tA
      val [z] = Name.invent (Variable.names_of ctxt) "z" 1
      val xzA = 
        Const (@{const_name Set.member}, Txy --> TA --> @{typ bool})
        $ (Const (@{const_name Pair}, Tx --> Ty --> Txy)
           $ tx $ Var ((z, 0), Ty))
        $ tA
    in
      case mk_thm (resolve_tac prems) svA of NONE => NONE
      | SOME thm_svA => case mk_thm (resolve_tac prems) xzA of NONE => NONE
        | SOME thm_xzA => 
          SOME (@{thm single_valuedD_eq[THEN eq_reflection]} OF [thm_svA, thm_xzA])
    end
  | _ => NONE)
*}

当它触发模式(_, _) ∈ _的一个项时，例如(x, y) ∈ A，它检查当前目标中是否存在single_valued A和(x, ?z) ∈ A假设。如果是，它将用它们实例化定理single_valuedD_eq，并将(x, y) ∈ A重写为y = ?z，并且?z被适当地实例化。

下面是一个例子:

lemma
  "⟦ single_valued A; (x, b) ∈ A; (x, c) ∈ A ⟧
  ⟹ map (λy. (x, y) ∈ A) xs = foo"
apply simp
  NEW GOAL:
  1. ⟦single_valued A; b = c; (x, c) ∈ A⟧ ⟹ map (λy. y = c) xs = foo

注意single_valued A必须是目标的假设。仅仅将single_valued A作为规则是不够的。这是因为假设是通过resolve_tac prems而不是完整的简化器调用来查找的。