在 Isabelle 中使用多个绑定定义函数

Question

考虑以下简化的 lambda 演算，其特点是绑定变量可以出现在绑定类型上：

theory Example
  imports "Nominal2.Nominal2" 
begin


atom_decl vrs

nominal_datatype ty = 
    Top

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

nominal_function
  fv :: "trm ⇒ vrs set"
where
  "fv (Var x) = {x}"
| "fv (Abs x t T) = (fv t) - {x}"
  using [[simproc del: alpha_lst]]  
  subgoal by(simp add: fv_graph_aux_def eqvt_def eqvt_at_def)
  subgoal by simp
  subgoal for P x
    apply(rule trm.strong_exhaust[of x P]) 
    by( simp_all add: fresh_star_def fresh_Pair)
                apply simp_all
  subgoal for x T t xa Ta ta  
    sorry

end

我一直无法显示上一个目标：

eqvt_at fv_sumC T ⟹ eqvt_at fv_sumC Ta ⟹ [[atom x]]lst. (T, t) = [[atom xa]]lst. (Ta, ta) ⟹ fv_sumC T - {x} = fv_sumC Ta - {xa}

尽管我努力了一天。

解决方案

subgoal for x T t xa Ta ta  
  proof -
    assume 1: "[[atom x]]lst. (t, T) = [[atom xa]]lst. (ta, Ta)"
          " eqvt_at fv_sumC t" " eqvt_at fv_sumC ta"
    then have 2: "[[atom x]]lst. t = [[atom xa]]lst. ta"
      by(auto simp add: Abs1_eq_iff'(3) fresh_Pair)      
    show "removeAll x (fv_sumC t) = removeAll xa (fv_sumC ta)"
      apply(rule Abs_lst1_fcb2'[OF 2, of _ "[]"])
         apply (simp add: fresh_removeAll)
        apply (simp add: fresh_star_list(3))
      using 1 Abs_lst1_fcb2' unfolding eqvt_at_def
      by auto
  qed

Answer 1

很高兴您能够找到解决方案。尽管如此，我还是想详细说明一下我之前的评论。特别是，我想强调 nominal_datatype 已经自动提供了一个非常相似的功能：它是功能 fv_trm。该函数实际上等同于您问题中的函数 fv 。这是证明这一点的理论的粗略草图（需要完善证明）：

theory Scratch
  imports "Nominal2.Nominal2"
begin

atom_decl vrs

nominal_datatype ty = 
  Top

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

lemma supp_ty: "supp (ty::ty) = {}"
  by (metis (full_types) ty.strong_exhaust ty.supp)

lemmas fv_trm = trm.fv_defs[unfolded supp_ty supp_at_base, simplified]

lemma dom_fv_trm: 
  "a ∈ fv_trm x ⟹ a ∈ {a. sort_of a = Sort ''Scratch.vrs'' []}"
  apply(induction rule: trm.induct)
  unfolding fv_trm 
  by auto

lemma inj_on_Abs_vrs: "inj_on Abs_vrs (fv_trm x)"
  using dom_fv_trm by (simp add: Abs_vrs_inject inj_on_def)

definition fv where "fv x = Abs_vrs ` fv_trm x"

lemma fv_Var: "fv (Var x) = {x}"
  unfolding fv_def fv_trm using Rep_vrs_inverse atom_vrs_def by auto

(*I leave it to you to work out the details, 
but Sledgehammer already finds something sensible*)
lemma fv_Abs: "fv (Abs x t T) = fv t - {x}"
  using inj_on_Abs_vrs
  unfolding fv_def fv_trm 
  sorry

end

在 Isabelle 中使用多个绑定定义函数

Defining function with several bindings in Isabelle

isabelle