Consider the following simplified lambda-calculus with the peculiarity that bound variables can occur on the bound type:
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
I have been unable to show the last goal:
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}
despite my efforts of a day.
Solution
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
I am glad that you were able to work out the solution. Nonetheless, I would still like to elaborate on the comment that I previously made. In particular, I would like to emphasize that nominal_datatype already provides a very similar function automatically: it is the function fv_trm. This function is, effectively, equivalent to the function fv in your question. Here is a rough sketch (the proof will need to be refined) of a theory that demonstrates this:
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