在 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⟹ [[原子 x]]lst.(T， t( = [[atom xa]]lst.(塔，塔(⟹ 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