证明两个绑定相等的名义伊莎贝尔

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用户可以通过两种方式提供帮助：

1. 如果你知道Nominal Isabelle，有可能做到这一点吗
2. 否则，x在规则T_Abs中的两次出现对于辅助是相等的，还是它们是具有不同恒等式的有界变量

Answer 1

1. 如果你知道Nominal Isabelle，有可能做到这一点吗

不幸的是，不可能证明你试图证明的定理。这里有一个反例(证明是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

2. 否则，规则T_Abs中出现的两个x是否等于辅助变量还是它们是不同的绑定变量身份

我相信您的思路是正确的，希望上面的例子能澄清您可能存在的任何困惑。一般来说，你可以将Abs x t1 = Abs y t2的含义解释为(λx. t1)和(λy. t2)的α等价。当然，在x和y不相等的情况下，(λx. t1)和(λy. t2)可以是α等价的。