在 Nominal Isabelle 中证明两个绑定相等

Question

考虑 Nominal Isabelle 中具有绑定的以下数据类型：

theory Example
  imports "Nominal2.Nominal2" 
begin

atom_decl vrs

nominal_datatype ty = 
    Tvar   "vrs"
  | Arrow x::vrs T::"ty" binds x in T

nominal_datatype trm = 
    Var   "vrs"
  | Abs   x::"vrs" t::"trm"  binds x in t 

inductive
  typing :: "trm ⇒ ty ⇒ bool" ("_ , _" [60,60] 60) 
where
 T_Abs[intro]: "(Abs x t) , (Arrow x T)"

equivariance typing
nominal_inductive typing done 

lemma 
  assumes "(Abs x t), (Arrow y T)"
  shows "x = y"
  using assms

我想证明关系中出现的两个绑定是相等的。我看到 Isabelle 用户可以通过两种方式提供帮助：

如果你知道 Nominal Isabelle 是否可以这样做？
否则，规则 T_Abs 中两次出现的 x 对助手来说是相等的还是它们是具有不同身份的绑定变量？

Answer 1

If you know Nominal Isabelle is it possible to do this?

很遗憾，无法证明您要证明的定理。这是一个反例（证明是 Sledgehammered）：

theory Scratch
  imports "Nominal2.Nominal2" 
begin

atom_decl vrs

nominal_datatype ty = 
    Tvar   "vrs"
    | Arrow x::vrs T::"ty" binds x in T

nominal_datatype trm = 
    Var   "vrs"
    | Abs   x::"vrs" t::"trm"  binds x in t 

inductive
  typing :: "trm ⇒ ty ⇒ bool" ("_ , _" [60,60] 60) 
where
 T_Abs[intro]: "(Abs x t) , (Arrow x T)"

equivariance typing
nominal_inductive typing . 

abbreviation s where "s ≡ Sort ''Scratch.vrs'' []"
abbreviation v where "v n ≡ Abs_vrs (Atom s n)"

lemma neq: "Abs (v 1) (Var (v 0)), Arrow (v (Suc (Suc 0))) (Tvar (v 0))"
  (is "?a, ?b")
proof-
  have a_def: "Abs (v 1) (Var (v 0)) = Abs (v (Suc (Suc 0))) (Var (v 0))"
    (*Sledgehammered*)
    by simp (smt Abs_vrs_inverse atom.inject flip_at_base_simps(3) fresh_PairD(2) 
        fresh_at_base(2) mem_Collect_eq nat.distinct(1) sort_of.simps trm.fresh(1))
  from typing.simps[of ?a ?b, unfolded this, THEN iffD2] have
    "Abs (v (Suc (Suc 0))) (Var (v 0)) , Arrow (v (Suc (Suc 0))) (Tvar (v 0))"
    by auto
  then show ?thesis unfolding a_def by clarsimp
qed

lemma "∃x y t T. x ≠ y ∧ (Abs x t), (Arrow y T)"
proof(intro exI conjI)
  show "v 1 ≠ v (Suc (Suc 0))" 
    (*Sledgehammered*)
    by (smt Abs_vrs_inverse One_nat_def atom.inject mem_Collect_eq n_not_Suc_n 
        sort_of.simps)
  show "Abs (v 1) (Var (v 0)) , Arrow (v (Suc (Suc 0))) (Tvar (v 0))"
    by (rule neq)
qed

end

Otherwise, are the two occurrences of x in the rule T_Abs equal for the assistant or are they sort of bound variable with different identity?

我相信您的思路是正确的，希望上面的例子能澄清您可能有的任何困惑。通常，您可以将 Abs x t1 = Abs y t2 的含义解释为 (λx. t1) 和 (λy. t2) 的等价字母。当然，(λx. t1) 和 (λy. t2) 可能是 alpha 等效的，但 x 和 y 不相等。

在 Nominal Isabelle 中证明两个绑定相等

Proving two bindings equal in Nominal Isabelle

isabelle