Quelle  IVSubst.thy

(*<*)
theory IVSubst
  imports  Syntax
begin
  (*>*)

chapter ‹Immutable Variable Substitution›

text ‹Substitution involving immutable variables. We define a class and instances for all
  the term forms›

section ‹Class›

class has_subst_v = fs +
  fixes subst_v :: "'a::fs ==> x ==> v ==> 'a::fs"   (‹_[_::=_]_v› [1000,50,50] 1000)
  assumes fresh_subst_v_if:  "y ♯ (subst_v a x v) ⟷ (atom x ♯ a ∧ y ♯ a) ∨ (y ♯ v ∧ (y ♯ a ∨ y = atom x))" 
    and    forget_subst_v[simp]:  "atom x ♯ a ==> subst_v a x v = a"
    and    subst_v_id[simp]:      "subst_v a x (V_var x) = a"
    and    eqvt[simp,eqvt]:       "(p::perm) ∙ (subst_v a x v) = (subst_v (p ∙ a) (p ∙x) (p ∙v))"
    and    flip_subst_v[simp]:    "atom x ♯ c ==> ((x ↔ z) ∙ c) = c[z::=[x]^v]_v"
    and    subst_v_simple_commute[simp]: "atom x ♯ c ==>(c[z::=[x]^v]_v)[x::=b]_v = c[z::=b]_v" 
begin

lemma subst_v_flip_eq_one:
  fixes z1::x and z2::x and x1::x and x2::x  
  assumes "[[atom z1]]lst. c1 = [[atom z2]]lst. c2" 
    and "atom x1 ♯ (z1,z2,c1,c2)"
  shows "(c1[z1::=[x1]^v]_v) = (c2[z2::=[x1]^v]_v)"
proof -  
  have "(c1[z1::=[x1]^v]_v) = (x1 ↔ z1) ∙ c1" using assms flip_subst_v by auto
  moreover have  "(c2[z2::=[x1]^v]_v) = (x1 ↔ z2) ∙ c2" using assms flip_subst_v by auto
  ultimately show ?thesis using Abs1_eq_iff_all(3)[of z1 c1 z2 c2 z1]  assms 
    by (metis Abs1_eq_iff_fresh(3) flip_commute)
qed

lemma subst_v_flip_eq_two:
  fixes z1::x and z2::x and x1::x and x2::x 
  assumes "[[atom z1]]lst. c1 = [[atom z2]]lst. c2" 
  shows "(c1[z1::=b]_v) = (c2[z2::=b]_v)"
proof -
  obtain x::x where *:"atom x ♯ (z1,z2,c1,c2)" using obtain_fresh by metis
  hence "(c1[z1::=[x]^v]_v) = (c2[z2::=[x]^v]_v)" using subst_v_flip_eq_one[OF assms, of x] by metis
  hence "(c1[z1::=[x]^v]_v)[x::=b]_v = (c2[z2::=[x]^v]_v)[x::=b]_v" by auto
  thus ?thesis using subst_v_simple_commute * fresh_prod4 by metis
qed

lemma subst_v_flip_eq_three:
  assumes "[[atom z1]]lst. c1 = [[atom z1']]lst. c1'"  and "atom x ♯ c1" and "atom x' ♯ (x,z1,z1', c1, c1')"
  shows   "(x ↔ x') ∙ (c1[z1::=[x]^v]_v) = c1'[z1'::=[x']^v]_v" 
proof -
  have "atom x' ♯ c1[z1::=[x]^v]_v" using assms fresh_subst_v_if by simp
  hence "(x ↔ x') ∙ (c1[z1::=[x]^v]_v) = c1[z1::=[x]^v]_v[x::=[x']^v]_v" using flip_subst_v[of x' "c1[z1::=[x]^v]_v" x] flip_commute by metis
  also have "... = c1[z1::=[x']^v]_v" using subst_v_simple_commute fresh_prod4 assms by auto
  also have "... = c1'[z1'::=[x']^v]_v" using subst_v_flip_eq_one[of z1 c1 z1' c1' x'] using  assms by auto
  finally show ?thesis by auto
qed

end

section ‹Values›

nominal_function 
  subst_vv :: "v ==> x ==> v ==> v" where
  "subst_vv (V_lit l) x v = V_lit l"
| "subst_vv (V_var y) x v = (if x = y then v else V_var y)"
| "subst_vv (V_cons tyid c v') x v = V_cons tyid c (subst_vv v' x v)"
| "subst_vv (V_consp tyid c b v') x v = V_consp tyid c b (subst_vv v' x v)"
| "subst_vv (V_pair v1 v2) x v = V_pair (subst_vv v1 x v ) (subst_vv v2 x v )"
  by(auto simp: eqvt_def subst_vv_graph_aux_def, metis v.strong_exhaust)
nominal_termination (eqvt) by lexicographic_order

abbreviation 
  subst_vv_abbrev :: "v ==> x ==> v ==> v" (‹_[_::=_]_vv› [1000,50,50] 1000)
  where 
    "v[x::=v']_vv ≡ subst_vv v x v'" 

lemma fresh_subst_vv_if [simp]:
  "j ♯ t[i::=x]_vv = ((atom i ♯ t ∧ j ♯ t) ∨ (j ♯ x ∧ (j ♯ t ∨ j = atom i)))"
  using supp_l_empty apply (induct t rule: v.induct,auto simp add: subst_vv.simps fresh_def, auto)
  by (simp add: supp_at_base |metis b.supp supp_b_empty  )+

lemma forget_subst_vv [simp]: "atom a ♯ tm ==> tm[a::=x]_vv = tm"
  by (induct tm rule: v.induct) (simp_all add: fresh_at_base)

lemma subst_vv_id [simp]: "tm[a::=V_var a]_vv = tm"
  by (induct tm rule: v.induct) simp_all

lemma subst_vv_commute [simp]:
  "atom j ♯ tm ==> tm[i::=t]_vv[j::=u]_vv = tm[i::=t[j::=u]_vv]_vv "
  by (induct tm rule: v.induct) (auto simp: fresh_Pair)

lemma subst_vv_commute_full [simp]:
  "atom j ♯ t ==> atom i ♯ u ==> i ≠ j ==> tm[i::=t]_vv[j::=u]_vv = tm[j::=u]_vv[i::=t]_vv"
  by (induct tm rule: v.induct) auto

lemma subst_vv_var_flip[simp]:
  fixes v::v
  assumes "atom y ♯ v"
  shows "(y ↔ x) ∙ v = v [x::=V_var y]_vv"
  using assms apply(induct v rule:v.induct)
      apply auto
  using  l.fresh l.perm_simps l.strong_exhaust supp_l_empty permute_pure permute_list.simps fresh_def flip_fresh_fresh apply fastforce
  using permute_pure apply blast+
  done

instantiation v :: has_subst_v
begin

definition 
  "subst_v = subst_vv"

instance proof
  fix j::atom and i::x and  x::v and t::v
  show  "(j ♯ subst_v t i x) = ((atom i ♯ t ∧ j ♯ t) ∨ (j ♯ x ∧ (j ♯ t ∨ j = atom i)))"
    using fresh_subst_vv_if[of j t i x] subst_v_v_def by metis

  fix a::x and tm::v and x::v
  show "atom a ♯ tm ==> subst_v tm a x = tm"
    using forget_subst_vv subst_v_v_def by simp

  fix a::x and tm::v
  show "subst_v tm a (V_var a) = tm" using subst_vv_id  subst_v_v_def by simp

  fix p::perm and x1::x and v::v and t1::v
  show "p ∙ subst_v t1 x1 v = subst_v (p ∙ t1) (p ∙ x1) (p ∙ v)" 
    using   subst_v_v_def by simp

  fix x::x and c::v and z::x
  show "atom x ♯ c ==> ((x ↔ z) ∙ c) = c[z::=[x]^v]_v"
    using  subst_v_v_def by simp

  fix x::x and c::v and z::x
  show  "atom x ♯ c ==> c[z::=[x]^v]_v[x::=v]_v = c[z::=v]_v"
    using  subst_v_v_def by simp
qed

end

section ‹Expressions›

nominal_function subst_ev :: "e ==> x ==> v ==> e" where
  "subst_ev ( (AE_val v') ) x v = ( (AE_val (subst_vv v' x v)) )"
| "subst_ev ( (AE_app f v') ) x v = ( (AE_app f (subst_vv v' x v )) )"                
| "subst_ev ( (AE_appP f b v') ) x v = ( (AE_appP f b (subst_vv v' x v )) )"   
| "subst_ev ( (AE_op opp v1 v2) ) x v = ( (AE_op opp (subst_vv v1 x v ) (subst_vv v2 x v )) )"
| "subst_ev [#1 v']^e x v = [#1 (subst_vv v' x v )]^e"
| "subst_ev [#2 v']^e x v = [#2 (subst_vv v' x v )]^e"
| "subst_ev ( (AE_mvar u)) x v = AE_mvar u"
| "subst_ev [| v' |]^e x v = [| (subst_vv v' x v ) |]^e"
| "subst_ev ( AE_concat v1 v2) x v = AE_concat (subst_vv v1 x v ) (subst_vv v2 x v )"
| "subst_ev ( AE_split v1 v2) x v = AE_split (subst_vv v1 x v ) (subst_vv v2 x v )"
  by(simp add: eqvt_def subst_ev_graph_aux_def,auto)(meson e.strong_exhaust)

nominal_termination (eqvt) by lexicographic_order

abbreviation 
  subst_ev_abbrev :: "e ==> x ==> v ==> e" (‹_[_::=_]_ev› [1000,50,50] 500)
  where 
    "e[x::=v']_ev ≡ subst_ev e x v' " 

lemma size_subst_ev [simp]: "size ( subst_ev A i x) = size A"
  apply (nominal_induct A avoiding: i x rule: e.strong_induct) 
  by auto

lemma forget_subst_ev [simp]: "atom a ♯ A ==> subst_ev A a x = A"
  apply (nominal_induct A avoiding: a x rule: e.strong_induct) 
  by (auto simp: fresh_at_base)

lemma subst_ev_id [simp]: "subst_ev A a (V_var a) = A"
  by (nominal_induct A avoiding: a rule: e.strong_induct) (auto simp: fresh_at_base)

lemma fresh_subst_ev_if [simp]:
  "j ♯ (subst_ev A i x ) = ((atom i ♯ A ∧ j ♯ A) ∨ (j ♯ x ∧ (j ♯ A ∨ j = atom i)))"
  apply (induct A rule: e.induct)
  unfolding subst_ev.simps fresh_subst_vv_if apply auto+
  using pure_fresh fresh_opp_all apply metis+
  done

lemma subst_ev_commute [simp]:
  "atom j ♯ A ==> (A[i::=t]_ev)[j::=u]_ev = A[i::=t[j::=u]_vv]_ev"
  by (nominal_induct A avoiding: i j t u rule: e.strong_induct) (auto simp: fresh_at_base)

lemma subst_ev_var_flip[simp]:
  fixes e::e and y::x and x::x
  assumes "atom y ♯ e"
  shows "(y ↔ x) ∙ e = e [x::=V_var y]_ev"
  using assms apply(nominal_induct e rule:e.strong_induct)
           apply (simp add: subst_v_v_def)  
          apply (metis (mono_tags, lifting) b.eq_iff b.perm_simps e.fresh e.perm_simps flip_b_id subst_ev.simps subst_vv_var_flip)
         apply (metis (mono_tags, lifting) b.eq_iff b.perm_simps e.fresh e.perm_simps flip_b_id subst_ev.simps subst_vv_var_flip)
  subgoal for x
    apply (rule_tac y=x in  opp.strong_exhaust)
    using  subst_vv_var_flip flip_def by (simp add: flip_def permute_pure)+
  using  subst_vv_var_flip flip_def by (simp add: flip_def permute_pure)+

lemma subst_ev_flip:
  fixes e::e and ea::e and c::x
  assumes "atom c ♯ (e, ea)" and "atom c ♯ (x, xa, e, ea)" and "(x ↔ c) ∙ e = (xa ↔ c) ∙ ea" 
  shows "e[x::=v']_ev = ea[xa::=v']_ev"
proof -
  have "e[x::=v']_ev = (e[x::=V_var c]_ev)[c::=v']_ev" using subst_ev_commute assms by simp
  also have "... = ((c ↔ x) ∙ e)[c::=v']_ev" using subst_ev_var_flip assms by simp
  also have "... = ((c ↔ xa) ∙ ea)[c::=v']_ev" using assms flip_commute by metis
  also have "... = ea[xa::=v']_ev"  using subst_ev_var_flip assms  by simp
  finally show ?thesis by auto
qed

lemma subst_ev_var[simp]:
  "(AE_val (V_var x))[x::=[z]^v]_ev = AE_val (V_var z)"
  by auto

instantiation e :: has_subst_v
begin

definition 
  "subst_v = subst_ev"

instance proof
  fix j::atom and i::x and  x::v and t::e
  show  "(j ♯ subst_v t i x) = ((atom i ♯ t ∧ j ♯ t) ∨ (j ♯ x ∧ (j ♯ t ∨ j = atom i)))"
    using fresh_subst_ev_if[of j t i x] subst_v_e_def by metis

  fix a::x and tm::e and x::v
  show "atom a ♯ tm ==> subst_v tm a x = tm"
    using forget_subst_ev subst_v_e_def by simp

  fix a::x and tm::e
  show "subst_v tm a (V_var a) = tm" using subst_ev_id  subst_v_e_def by simp

  fix p::perm and x1::x and v::v and t1::e
  show "p ∙ subst_v t1 x1 v = subst_v (p ∙ t1) (p ∙ x1) (p ∙ v)" 
    using subst_ev_commute  subst_v_e_def by simp

  fix x::x and c::e and z::x
  show "atom x ♯ c ==> ((x ↔ z) ∙ c) = c[z::=[x]^v]_v"
    using  subst_v_e_def by simp

  fix x::x and c::e and z::x
  show  "atom x ♯ c ==> c[z::=[x]^v]_v[x::=v]_v = c[z::=v]_v"
    using  subst_v_e_def by simp
qed
end

lemma subst_ev_commute_full:
  fixes e::e and w::v and v::v
  assumes "atom z ♯ v" and "atom x ♯ w" and "x ≠ z"
  shows "subst_ev (e[z::=w]_ev) x v = subst_ev (e[x::=v]_ev) z w" 
  using assms by(nominal_induct e rule: e.strong_induct,simp+)

lemma subst_ev_v_flip1[simp]:
  fixes e::e
  assumes "atom z1 ♯ (z,e)" and "atom z1' ♯ (z,e)"
  shows"(z1 ↔ z1') ∙ e[z::=v]_ev = e[z::= ((z1 ↔ z1') ∙ v)]_ev"
  using assms proof(nominal_induct e rule:e.strong_induct)
qed  (simp add: flip_def fresh_Pair swap_fresh_fresh)+

section ‹Expressions in Constraints›

nominal_function subst_cev :: "ce ==> x ==> v ==> ce" where
  "subst_cev ( (CE_val v') ) x v = ( (CE_val (subst_vv v' x v )) )" 
| "subst_cev ( (CE_op opp v1 v2) ) x v = ( (CE_op opp (subst_cev v1 x v ) (subst_cev v2 x v )) )"
| "subst_cev ( (CE_fst v')) x v = CE_fst (subst_cev v' x v )"
| "subst_cev ( (CE_snd v')) x v = CE_snd (subst_cev v' x v )"
| "subst_cev ( (CE_len v')) x v = CE_len (subst_cev v' x v )"
| "subst_cev ( CE_concat v1 v2) x v = CE_concat (subst_cev v1 x v ) (subst_cev v2 x v )"
                      apply (simp add: eqvt_def subst_cev_graph_aux_def,auto)
  by (meson ce.strong_exhaust)

nominal_termination (eqvt) by lexicographic_order

abbreviation 
  subst_cev_abbrev :: "ce ==> x ==> v ==> ce" (‹_[_::=_]_cev› [1000,50,50] 500)
  where 
    "e[x::=v']_cev ≡ subst_cev e x v'" 

lemma size_subst_cev [simp]: "size ( subst_cev A i x ) = size A"
  by (nominal_induct A avoiding: i x rule: ce.strong_induct,auto) 

lemma forget_subst_cev [simp]: "atom a ♯ A ==> subst_cev A a x = A"
  by (nominal_induct A avoiding: a x rule: ce.strong_induct, auto simp: fresh_at_base)

lemma subst_cev_id [simp]: "subst_cev A a (V_var a) = A"
  by (nominal_induct A avoiding: a rule: ce.strong_induct) (auto simp: fresh_at_base)

lemma fresh_subst_cev_if [simp]:
  "j ♯ (subst_cev A i x ) = ((atom i ♯ A ∧ j ♯ A) ∨ (j ♯ x ∧ (j ♯ A ∨ j = atom i)))"
proof(nominal_induct A avoiding: i x rule: ce.strong_induct)
  case (CE_op opp v1 v2)
  then show ?case  using fresh_subst_vv_if subst_ev.simps e.supp pure_fresh opp.fresh 
      fresh_e_opp 
    using fresh_opp_all by auto
qed(auto)+

lemma subst_cev_commute [simp]:
  "atom j ♯ A ==> (subst_cev (subst_cev A i t ) j u) = subst_cev A i (subst_vv t j u )"
  by (nominal_induct A avoiding: i j t u rule: ce.strong_induct) (auto simp: fresh_at_base)

lemma subst_cev_var_flip[simp]:
  fixes e::ce and y::x and x::x
  assumes "atom y ♯ e"
  shows "(y ↔ x) ∙ e = e [x::=V_var y]_cev"
  using assms proof(nominal_induct e rule:ce.strong_induct)
  case (CE_val v)
  then show ?case using subst_vv_var_flip by auto
next
  case (CE_op opp v1 v2)
  hence yf: "atom y ♯ v1 ∧ atom y ♯ v2" using ce.fresh by blast
  have " (y ↔ x) ∙ (CE_op opp v1 v2 ) = CE_op ((y ↔ x) ∙ opp) ( (y ↔ x) ∙ v1 ) ( (y ↔ x) ∙ v2)" 
    using opp.perm_simps ce.perm_simps permute_pure ce.fresh opp.strong_exhaust by presburger
  also have "... = CE_op ((y ↔ x) ∙ opp) (v1[x::=V_var y]_cev) (v2 [x::=V_var y]_cev)" using yf 
    by (simp add: CE_op.hyps(1) CE_op.hyps(2))
  finally show ?case using subst_cev.simps  opp.perm_simps  opp.strong_exhaust 
    by (metis (full_types))
qed( (auto simp add: permute_pure subst_vv_var_flip)+)

lemma subst_cev_flip:
  fixes e::ce and ea::ce and c::x
  assumes "atom c ♯ (e, ea)" and "atom c ♯ (x, xa, e, ea)" and "(x ↔ c) ∙ e = (xa ↔ c) ∙ ea" 
  shows "e[x::=v']_cev = ea[xa::=v']_cev"
proof -
  have "e[x::=v']_cev = (e[x::=V_var c]_cev)[c::=v']_cev" using subst_ev_commute assms by simp
  also have "... = ((c ↔ x) ∙ e)[c::=v']_cev" using subst_ev_var_flip assms by simp
  also have "... = ((c ↔ xa) ∙ ea)[c::=v']_cev" using assms flip_commute by metis
  also have "... = ea[xa::=v']_cev"  using subst_ev_var_flip assms  by simp
  finally show ?thesis by auto
qed

lemma subst_cev_var[simp]:
  fixes z::x and x::x
  shows  "[[x]^v]^ce [x::=[z]^v]_cev = [[z]^v]^ce"
  by auto

instantiation ce :: has_subst_v
begin

definition 
  "subst_v = subst_cev"

instance proof
  fix j::atom and i::x and  x::v and t::ce
  show  "(j ♯ subst_v t i x) = ((atom i ♯ t ∧ j ♯ t) ∨ (j ♯ x ∧ (j ♯ t ∨ j = atom i)))"
    using fresh_subst_cev_if[of j t i x] subst_v_ce_def by metis

  fix a::x and tm::ce and x::v
  show "atom a ♯ tm ==> subst_v tm a x = tm"
    using forget_subst_cev subst_v_ce_def by simp

  fix a::x and tm::ce
  show "subst_v tm a (V_var a) = tm" using subst_cev_id  subst_v_ce_def by simp

  fix p::perm and x1::x and v::v and t1::ce
  show "p ∙ subst_v t1 x1 v = subst_v (p ∙ t1) (p ∙ x1) (p ∙ v)" 
    using subst_cev_commute  subst_v_ce_def by simp

  fix x::x and c::ce and z::x 
  show "atom x ♯ c ==> ((x ↔ z) ∙ c) = c [z::=V_var x]_v"
    using  subst_v_ce_def by simp

  fix x::x and c::ce and z::x
  show  "atom x ♯ c ==> c [z::=V_var x]_v[x::=v]_v = c[z::=v]_v"
    using  subst_v_ce_def by simp
qed

end

lemma subst_cev_commute_full:
  fixes e::ce and w::v and v::v
  assumes "atom z ♯ v" and "atom x ♯ w" and "x ≠ z"
  shows "subst_cev (e[z::=w]_cev) x v = subst_cev (e[x::=v]_cev) z w " 
  using assms by(nominal_induct e rule: ce.strong_induct,simp+)


lemma subst_cev_v_flip1[simp]:
  fixes e::ce
  assumes "atom z1 ♯ (z,e)" and "atom z1' ♯ (z,e)"
  shows"(z1 ↔ z1') ∙ e[z::=v]_cev = e[z::= ((z1 ↔ z1') ∙ v)]_cev"
  using assms apply(nominal_induct e rule:ce.strong_induct)
  by (simp add: flip_def fresh_Pair swap_fresh_fresh)+

section ‹Constraints›

nominal_function subst_cv :: "c ==> x ==> v ==> c" where
  "subst_cv (C_true) x v = C_true"
|  "subst_cv (C_false) x v = C_false"
|  "subst_cv (C_conj c1 c2) x v = C_conj (subst_cv c1 x v ) (subst_cv c2 x v )"
|  "subst_cv (C_disj c1 c2) x v = C_disj (subst_cv c1 x v ) (subst_cv c2 x v )"
|  "subst_cv (C_imp c1 c2) x v = C_imp (subst_cv c1 x v ) (subst_cv c2 x v )"
|  "subst_cv (e1 == e2) x v = ((subst_cev e1 x v ) == (subst_cev e2 x v ))"
|  "subst_cv (C_not c) x v = C_not (subst_cv c x v )"
                      apply (simp add: eqvt_def subst_cv_graph_aux_def,auto)
  using c.strong_exhaust by metis
nominal_termination (eqvt)  by lexicographic_order

abbreviation 
  subst_cv_abbrev :: "c ==> x ==> v ==> c" (‹_[_::=_]_cv› [1000,50,50] 1000)
  where 
    "c[x::=v']_cv ≡ subst_cv c x v'" 

lemma size_subst_cv [simp]: "size ( subst_cv A i x ) = size A"
  by (nominal_induct A avoiding: i x rule: c.strong_induct,auto) 

lemma forget_subst_cv [simp]: "atom a ♯ A ==> subst_cv A a x = A"
  by (nominal_induct A avoiding: a x rule: c.strong_induct, auto simp: fresh_at_base)

lemma subst_cv_id [simp]: "subst_cv A a (V_var a) = A"
  by (nominal_induct A avoiding: a rule: c.strong_induct) (auto simp: fresh_at_base)

lemma fresh_subst_cv_if [simp]:
  "j ♯ (subst_cv A i x ) ⟷ (atom i ♯ A ∧ j ♯ A) ∨ (j ♯ x ∧ (j ♯ A ∨ j = atom i))"
  by (nominal_induct A avoiding: i x rule: c.strong_induct, (auto simp add: pure_fresh)+)

lemma subst_cv_commute [simp]:
  "atom j ♯ A ==> (subst_cv (subst_cv A i t ) j u ) = subst_cv A i (subst_vv t j u )"
  by (nominal_induct A avoiding: i j t u rule: c.strong_induct) (auto simp: fresh_at_base)

lemma let_s_size [simp]: "size s ≤ size (AS_let x e s)"
  apply (nominal_induct s avoiding: e x rule: s_branch_s_branch_list.strong_induct(1)) 
              apply auto
  done

lemma subst_cv_var_flip[simp]:
  fixes c::c
  assumes "atom y ♯ c"
  shows "(y ↔ x) ∙ c = c[x::=V_var y]_cv"
  using assms by(nominal_induct c rule:c.strong_induct,(simp add: flip_subst_v subst_v_ce_def)+)

instantiation c :: has_subst_v
begin

definition 
  "subst_v = subst_cv"

instance proof
  fix j::atom and i::x and  x::v and t::c
  show  "(j ♯ subst_v t i x) = ((atom i ♯ t ∧ j ♯ t) ∨ (j ♯ x ∧ (j ♯ t ∨ j = atom i)))"
    using fresh_subst_cv_if[of j t i x] subst_v_c_def by metis

  fix a::x and tm::c and x::v
  show "atom a ♯ tm ==> subst_v tm a x = tm"
    using forget_subst_cv subst_v_c_def by simp

  fix a::x and tm::c
  show "subst_v tm a (V_var a) = tm" using subst_cv_id  subst_v_c_def by simp

  fix p::perm and x1::x and v::v and t1::c
  show "p ∙ subst_v t1 x1 v = subst_v (p ∙ t1) (p ∙ x1) (p ∙ v)" 
    using subst_cv_commute  subst_v_c_def by simp

  fix x::x and c::c and z::x
  show "atom x ♯ c ==> ((x ↔ z) ∙ c) = c[z::=[x]^v]_v"
    using subst_cv_var_flip subst_v_c_def by simp

  fix x::x and c::c and z::x
  show  "atom x ♯ c ==> c[z::=[x]^v]_v[x::=v]_v = c[z::=v]_v"
    using subst_cv_var_flip subst_v_c_def by simp
qed

end

lemma subst_cv_var_flip1[simp]:
  fixes c::c
  assumes "atom y ♯ c"
  shows "(x ↔ y) ∙ c = c[x::=V_var y]_cv"
  using subst_cv_var_flip flip_commute 
  by (metis assms)

lemma subst_cv_v_flip3[simp]:
  fixes c::c
  assumes "atom z1 ♯ c" and "atom z1' ♯ c"
  shows"(z1 ↔ z1') ∙ c[z::=[z1]^v]_cv = c[z::=[z1']^v]_cv"
proof - 
  consider "z1' = z" | "z1 = z" | "atom z1 ♯ z ∧ atom z1' ♯ z" by force
  then show ?thesis proof(cases)
    case 1
    then show ?thesis using 1 assms by auto
  next
    case 2
    then show ?thesis using 2 assms by auto
  next
    case 3
    then show ?thesis using assms by auto
  qed
qed

lemma subst_cv_v_flip[simp]:
  fixes c::c
  assumes "atom x ♯ c"
  shows "((x ↔ z) ∙ c)[x::=v]_cv = c [z::=v]_cv"
  using assms subst_v_c_def by auto

lemma subst_cv_commute_full:
  fixes c::c
  assumes "atom z ♯ v" and "atom x ♯ w" and "x≠z"
  shows "(c[z::=w]_cv)[x::=v]_cv = (c[x::=v]_cv)[z::=w]_cv" 
  using assms proof(nominal_induct c rule: c.strong_induct)
  case (C_eq e1 e2)
  then show ?case using subst_cev_commute_full by simp
qed(force+)

lemma subst_cv_eq[simp]:
  assumes  "atom z1 ♯ e1" 
  shows "(CE_val (V_var z1) == e1 )[z1::=[x]^v]_cv = (CE_val (V_var x) == e1 )" (is "?A = ?B")
proof -
  have "?A = (((CE_val (V_var z1))[z1::=[x]^v]_cev) == e1)" using subst_cv.simps assms by simp
  thus ?thesis by simp
qed

section ‹Variable Context›

text ‹The idea of this substitution is to remove x from the context. We really want to add the condition
  x is fresh in v but this causes problems with proofs.›

nominal_function subst_gv :: "Γ ==> x ==> v ==> Γ" where
  "subst_gv GNil x v = GNil"
| "subst_gv ((y,b,c) #_\<Gamma> Γ) x v = (if x = y then Γ else ((y,b,c[x::=v]_cv)#_\<Gamma> (subst_gv Γ x v )))"
proof(goal_cases)
  case 1
  then show ?case  by(simp add: eqvt_def subst_gv_graph_aux_def )
next
  case (3 P x)
  then show ?case by (metis neq_GNil_conv prod_cases3)
qed(fast+)
nominal_termination (eqvt) by lexicographic_order

abbreviation 
  subst_gv_abbrev :: "Γ ==> x ==> v ==> Γ" (‹_[_::=_]_\Γ_v› [1000,50,50] 1000)
  where 
    "g[x::=v]_\<Gamma>_v ≡ subst_gv g x v" 

lemma size_subst_gv [simp]: "size ( subst_gv G i x ) ≤ size G"
  by (induct G,auto) 

lemma forget_subst_gv [simp]: "atom a ♯ G ==> subst_gv G a x = G"
  apply (induct G ,auto) 
  using fresh_GCons fresh_PairD(1) not_self_fresh apply blast
   apply (simp add: fresh_GCons)+
  done

lemma fresh_subst_gv: "atom a ♯ G ==> atom a ♯ v ==> atom a ♯ subst_gv G x v"
proof(induct G)
  case GNil
  then show ?case by auto
next
  case (GCons xbc G)
  obtain x' and b' and c' where xbc: "xbc = (x',b',c')" using prod_cases3 by blast
  show ?case proof(cases "x=x'")
    case True
    have "atom a ♯ G" using GCons fresh_GCons by blast
    thus ?thesis using subst_gv.simps(2)[of  x' b' c' G] GCons xbc True by presburger
  next
    case False
    then show ?thesis using subst_gv.simps(2)[of  x' b' c' G] GCons xbc False fresh_GCons by simp
  qed
qed

lemma subst_gv_flip: 
  fixes x::x and xa::x and z::x and c::c and b::b and Γ::Γ
  assumes "atom xa ♯ ((x, b, c[z::=[x]^v]_cv) #_\<Gamma> Γ)"  and "atom xa ♯ Γ" and "atom x ♯ Γ" and "atom x ♯ (z, c)" and "atom xa ♯ (z, c)"
  shows "(x ↔ xa) ∙ ((x, b, c[z::=[x]^v]_cv) #_\<Gamma> Γ) = (xa, b, c[z::=V_var xa]_cv) #_\<Gamma> Γ"
proof -
  have  "(x ↔ xa) ∙ ((x, b, c[z::=[x]^v]_cv) #_\<Gamma> Γ) = (( (x ↔ xa) ∙ x, b, (x ↔ xa) ∙ c[z::=[x]^v]_cv) #_\<Gamma> ((x ↔ xa) ∙ Γ))" 
    using subst Cons_eqvt flip_fresh_fresh using G_cons_flip by simp
  also have "... = ((xa, b, (x ↔ xa) ∙ c[z::=[x]^v]_cv) #_\<Gamma> ((x ↔ xa) ∙ Γ))" using assms by fastforce
  also have "... = ((xa, b, c[z::=V_var xa]_cv) #_\<Gamma> ((x ↔ xa) ∙ Γ))" using assms subst_cv_var_flip by fastforce
  also have "... = ((xa, b, c[z::=V_var xa]_cv) #_\<Gamma> Γ)"  using assms flip_fresh_fresh by blast 
  finally show ?thesis by simp
qed

section ‹Types›

nominal_function subst_tv :: "τ ==> x ==> v ==> τ" where
  "atom z ♯ (x,v) ==> subst_tv { z : b | c } x v = { z : b | c[x::=v]_cv }"
     apply (simp add: eqvt_def subst_tv_graph_aux_def )
    apply auto
  subgoal for P a aa b
    apply(rule_tac y=a and c="(aa,b)" in τ.strong_exhaust)
    by (auto simp: eqvt_at_def fresh_star_def fresh_Pair fresh_at_base) 
  apply (auto simp: eqvt_at_def fresh_star_def fresh_Pair fresh_at_base)
proof -
  fix z :: x and c :: c and za :: x and xa :: x and va :: v and ca :: c and cb :: x
  assume a1: "atom za ♯ va"  and  a2: "atom z ♯ va" and a3: "∀cb. atom cb ♯ c ∧ atom cb ♯ ca ⟶ cb ≠ z ∧ cb ≠ za ⟶ c[z::=V_var cb]_cv = ca[za::=V_var cb]_cv"
  assume a4: "atom cb ♯ c" and a5: "atom cb ♯ ca" and a6: "cb ≠ z" and a7: "cb ≠ za" and "atom cb ♯ va" and a8: "za ≠ xa" and a9: "z ≠ xa"
  assume a10:"cb ≠ xa"
  note assms = a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 

  have "c[z::=V_var cb]_cv = ca[za::=V_var cb]_cv" using assms  by auto
  hence "c[z::=V_var cb]_cv[xa::=va]_cv = ca[za::=V_var cb]_cv[xa::=va]_cv" by simp
  moreover have "c[z::=V_var cb]_cv[xa::=va]_cv = c[xa::=va]_cv[z::=V_var cb]_cv" using   subst_cv_commute_full[of z va xa "V_var cb" ]  assms fresh_def v.supp by fastforce
  moreover  have "ca[za::=V_var cb]_cv[xa::=va]_cv = ca[xa::=va]_cv[za::=V_var cb]_cv" 
    using   subst_cv_commute_full[of za va xa "V_var cb" ]  assms fresh_def v.supp by fastforce

  ultimately show "c[xa::=va]_cv[z::=V_var cb]_cv = ca[xa::=va]_cv[za::=V_var cb]_cv" by simp
qed

nominal_termination (eqvt) by lexicographic_order

abbreviation 
  subst_tv_abbrev :: "τ ==> x ==> v ==> τ" (‹_[_::=_]_\τ_v› [1000,50,50] 1000)
  where 
    "t[x::=v]_\<tau>_v ≡ subst_tv t x v" 

lemma size_subst_tv [simp]: "size ( subst_tv A i x ) = size A"
proof (nominal_induct A avoiding: i x  rule: τ.strong_induct)
  case (T_refined_type x' b' c')
  then show ?case by auto
qed

lemma forget_subst_tv [simp]: "atom a ♯ A ==> subst_tv A a x = A"
  apply (nominal_induct A avoiding: a x rule: τ.strong_induct) 
  apply(auto simp: fresh_at_base)
  done

lemma subst_tv_id [simp]: "subst_tv A a (V_var a) = A"
  by (nominal_induct A avoiding: a rule: τ.strong_induct) (auto simp: fresh_at_base)

lemma fresh_subst_tv_if [simp]:
  "j ♯ (subst_tv A i x ) ⟷ (atom i ♯ A ∧ j ♯ A) ∨ (j ♯ x ∧ (j ♯ A ∨ j = atom i))"
  apply (nominal_induct A avoiding: i x rule: τ.strong_induct)
  using fresh_def supp_b_empty x_fresh_b by auto

lemma subst_tv_commute [simp]:
  "atom y ♯ τ ==> (τ[x::= t]_\<tau>_v)[y::=v]_\<tau>_v = τ[x::= t[y::=v]_vv]_\<tau>_v "
  by (nominal_induct τ avoiding: x y t v rule: τ.strong_induct) (auto simp: fresh_at_base)

lemma subst_tv_var_flip [simp]:
  fixes x::x and xa::x and τ::τ
  assumes "atom xa ♯ τ"
  shows "(x ↔ xa) ∙ τ = τ[x::=V_var xa]_\<tau>_v"
proof - 
  obtain z::x and b and c where zbc: "atom z ♯ (x,xa, V_var xa) ∧ τ = { z : b | c }" 
    using obtain_fresh_z   by (metis prod.inject subst_tv.cases)
  hence "atom xa ∉ supp c - { atom z }" using τ.supp[of z b c] fresh_def supp_b_empty assms 
    by  auto
  moreover have "xa ≠ z" using zbc fresh_prod3 by force
  ultimately have xaf: "atom xa ♯ c" using fresh_def by auto
  have "(x ↔ xa) ∙ τ = { z : b | (x ↔ xa) ∙ c }" 
    by (metis τ.perm_simps empty_iff flip_at_base_simps(3) flip_fresh_fresh fresh_PairD(1) fresh_PairD(2) fresh_def not_self_fresh supp_b_empty v.fresh(2) zbc)
  also have "... = { z : b | c[x::=V_var xa]_cv }"  using subst_cv_v_flip xaf  
    by (metis permute_flip_cancel permute_flip_cancel2 subst_cv_var_flip)
  finally show ?thesis using subst_tv.simps zbc 
    using fresh_PairD(1) not_self_fresh by force
qed

instantiation τ :: has_subst_v
begin

definition 
  "subst_v = subst_tv"

instance proof
  fix j::atom and i::x and  x::v and t::τ
  show  "(j ♯ subst_v t i x) = ((atom i ♯ t ∧ j ♯ t) ∨ (j ♯ x ∧ (j ♯ t ∨ j = atom i)))"

  proof(nominal_induct t avoiding: i x rule:τ.strong_induct)
    case (T_refined_type z b c)
    hence " j ♯ { z : b | c }[i::=x]_v = j ♯ { z : b | c[i::=x]_cv }" using subst_tv.simps subst_v_τ_def fresh_Pair by simp
    also have "... = (atom i ♯ { z : b | c } ∧ j ♯ { z : b | c } ∨ j ♯ x ∧ (j ♯ { z : b | c } ∨ j = atom i))" 
      unfolding τ.fresh using subst_v_c_def fresh_subst_v_if 
      using T_refined_type.hyps(1) T_refined_type.hyps(2) x_fresh_b by auto
    finally show ?case by auto
  qed

  fix a::x and tm::τ and x::v
  show "atom a ♯ tm ==> subst_v tm a x = tm"
    apply(nominal_induct tm avoiding: a x rule:τ.strong_induct)
    using subst_v_c_def forget_subst_v subst_tv.simps subst_v_τ_def fresh_Pair by simp

  fix a::x and tm::τ
  show "subst_v tm a (V_var a) = tm"     
    apply(nominal_induct tm avoiding: a rule:τ.strong_induct)
    using subst_v_c_def forget_subst_v subst_tv.simps subst_v_τ_def fresh_Pair by simp

  fix p::perm and x1::x and v::v and t1::τ
  show "p ∙ subst_v t1 x1 v = subst_v (p ∙ t1) (p ∙ x1) (p ∙ v)" 
    apply(nominal_induct tm avoiding: a x rule:τ.strong_induct)
    using subst_v_c_def forget_subst_v subst_tv.simps subst_v_τ_def fresh_Pair by simp

  fix x::x and c::τ and z::x
  show "atom x ♯ c ==> ((x ↔ z) ∙ c) = c[z::=[x]^v]_v" 
    apply(nominal_induct c avoiding: z x rule:τ.strong_induct)
    using subst_v_c_def flip_subst_v subst_tv.simps subst_v_τ_def fresh_Pair by auto

  fix x::x and c::τ and z::x
  show  "atom x ♯ c ==> c[z::=[x]^v]_v[x::=v]_v = c[z::=v]_v"
    apply(nominal_induct c avoiding:  x v z rule:τ.strong_induct)
    using subst_v_c_def  subst_tv.simps subst_v_τ_def fresh_Pair 
    by (metis flip_commute subst_tv_commute subst_tv_var_flip subst_v_τ_def subst_vv.simps(2))
qed

end

lemma subst_tv_commute_full:
  fixes c::τ
  assumes "atom z ♯ v" and "atom x ♯ w" and "x≠z"
  shows "(c[z::=w]_\<tau>_v)[x::=v]_\<tau>_v = (c[x::=v]_\<tau>_v)[z::=w]_\<tau>_v" 
  using assms proof(nominal_induct c avoiding: x v z w rule: τ.strong_induct)
  case (T_refined_type x1a x2a x3a)
  then show ?case using subst_cv_commute_full by simp
qed

lemma type_eq_subst_eq:
  fixes v::v and c1::c
  assumes "{ z1 : b1 | c1 } = { z2 : b2 | c2 }"
  shows "c1[z1::=v]_cv = c2[z2::=v]_cv"
  using subst_v_flip_eq_two[of z1 c1 z2 c2 v] τ.eq_iff assms subst_v_c_def by simp

text ‹Extract constraint from a type. We cannot just project out the constraint as this would
  alpha-equivalent types give different answers ›

nominal_function c_of :: "τ ==> x ==> c" where
  "atom z ♯ x ==> c_of (T_refined_type z b c) x = c[z::=[x]^v]_cv"
proof(goal_cases)
  case 1
  then show ?case using eqvt_def c_of_graph_aux_def by force
next
  case (2 x y)
  then show ?case using eqvt_def c_of_graph_aux_def by force
next
  case (3 P x)
  then obtain x1::τ and x2::x where *:"x = (x1,x2)" by force
  obtain z' and b' and c' where "x1 = { z' : b' | c' } ∧ atom z' ♯ x2" using obtain_fresh_z by metis
  then show ?case  using 3 * by auto
next
  case (4 z1 x1 b1 c1 z2 x2 b2 c2)
  then show ?case using subst_v_flip_eq_two τ.eq_iff   by (metis prod.inject type_eq_subst_eq)
qed

nominal_termination (eqvt) by lexicographic_order

lemma c_of_eq:
  shows  "c_of { x : b | c } x = c"
proof(nominal_induct "{ x : b | c }" avoiding: x rule: τ.strong_induct)
  case (T_refined_type x' c') 
  moreover hence "c_of { x' : b | c' } x = c'[x'::=V_var x]_cv" using c_of.simps by auto
  moreover have "{ x' : b | c' } = { x : b | c }" using T_refined_type  τ.eq_iff by metis
  moreover have "c'[x'::=V_var x]_cv = c" using  T_refined_type Abs1_eq_iff flip_subst_v subst_v_c_def 
    by (metis subst_cv_id)
  ultimately show ?case by auto
qed

lemma obtain_fresh_z_c_of:
  fixes t::"'b::fs"
  obtains z  where "atom z ♯ t ∧ τ = { z : b_of τ | c_of τ z }"
proof - 
  obtain z and c where "atom z ♯ t ∧ τ = { z : b_of τ | c }" using obtain_fresh_z2 by metis
  moreover hence "c = c_of τ z" using c_of.simps using c_of_eq by metis
  ultimately show ?thesis 
    using that by auto
qed

lemma c_of_fresh:
  fixes x::x
  assumes  "atom x ♯ (t,z)" 
  shows "atom x ♯ c_of t z" 
proof -
  obtain z' and c' where z:"t = { z' : b_of t | c' } ∧ atom z' ♯ (x,z)" using obtain_fresh_z_c_of by metis
  hence *:"c_of t z = c'[z'::=V_var z]_cv" using c_of.simps fresh_Pair by metis
  have "(atom x ♯ c' ∨ atom x ∈ set [atom z']) ∧ atom x ♯ b_of t" using τ.fresh assms z fresh_Pair by metis
  hence "atom x ♯ c'" using fresh_Pair z fresh_at_base(2) by fastforce
  moreover have "atom x ♯ V_var z" using assms fresh_Pair v.fresh by metis
  ultimately show ?thesis using assms fresh_subst_v_if[of "atom x" c' z' "V_var z"] subst_v_c_def * by metis
qed

lemma c_of_switch:
  fixes z::x
  assumes "atom z ♯ t" 
  shows "(c_of t z)[z::=V_var x]_cv = c_of t x"
proof -  
  obtain z' and c' where z:"t = { z' : b_of t | c' } ∧ atom z' ♯ (x,z)" using obtain_fresh_z_c_of by metis
  hence "(atom z ♯ c' ∨ atom z ∈ set [atom z']) ∧ atom z ♯ b_of t" using τ.fresh[of "atom z" z' "b_of t" c'] assms by metis
  moreover have " atom z ∉ set [atom z']" using z fresh_Pair by force
  ultimately have  **:"atom z ♯ c'" using fresh_Pair z fresh_at_base(2) by metis

  have "(c_of t z)[z::=V_var x]_cv = c'[z'::=V_var z]_cv[z::=V_var x]_cv"  using c_of.simps fresh_Pair  z by metis
  also have "... = c'[z'::=V_var x]_cv"  using subst_v_simple_commute subst_v_c_def assms c_of.simps z  ** by metis
  finally show ?thesis using c_of.simps[of z' x "b_of t" c']  fresh_Pair z by metis
qed

lemma type_eq_subst_eq1:
  fixes v::v and c1::c
  assumes "{ z1 : b1 | c1 } = ({ z2 : b2 | c2 })" and "atom z1 ♯ c2" 
  shows "c1[z1::=v]_cv = c2[z2::=v]_cv" and "b1=b2" and " c1 = (z1 ↔ z2) ∙ c2"
proof -
  show "c1[z1::=v]_cv = c2[z2::=v]_cv" using type_eq_subst_eq assms by blast
  show "b1=b2" using τ.eq_iff assms by blast
  have "z1 = z2 ∧ c1 = c2 ∨ z1 ≠ z2 ∧ c1 = (z1 ↔ z2) ∙ c2 ∧ atom z1 ♯ c2" 
    using τ.eq_iff Abs1_eq_iff[of z1 c1 z2 c2] assms by blast 
  thus  "c1 = (z1 ↔ z2) ∙ c2" by auto
qed

lemma type_eq_subst_eq2:
  fixes v::v and c1::c
  assumes "{ z1 : b1 | c1 } = ({ z2 : b2 | c2 })" 
  shows "c1[z1::=v]_cv = c2[z2::=v]_cv" and "b1=b2" and "[[atom z1]]lst. c1 = [[atom z2]]lst. c2"
proof -
  show "c1[z1::=v]_cv = c2[z2::=v]_cv" using type_eq_subst_eq assms by blast
  show "b1=b2" using τ.eq_iff assms by blast
  show  "[[atom z1]]lst. c1 = [[atom z2]]lst. c2" 
    using τ.eq_iff assms by auto
qed

lemma type_eq_subst_eq3:
  fixes v::v and c1::c
  assumes "{ z1 : b1 | c1 } = ({ z2 : b2 | c2 })" and "atom z1 ♯ c2" 
  shows "c1 = c2[z2::=V_var z1]_cv" and "b1=b2"
  using type_eq_subst_eq1 assms  subst_v_c_def 
  by (metis subst_cv_var_flip)+

lemma type_eq_flip:
  assumes "atom x ♯ c"
  shows "{ z : b | c } = { x : b | (x ↔ z ) ∙ c }"
  using τ.eq_iff Abs1_eq_iff assms 
  by (metis (no_types, lifting) flip_fresh_fresh)

lemma c_of_true:
  "c_of { z' : B_bool | TRUE } x = C_true"
proof(nominal_induct "{ z' : B_bool | TRUE }" avoiding: x rule:τ.strong_induct)
  case (T_refined_type x1a x3a)
  hence "{ z' : B_bool | TRUE } = { x1a : B_bool | x3a }" using τ.eq_iff by metis
  then show ?case using subst_cv.simps c_of.simps T_refined_type 
      type_eq_subst_eq3 
    by (metis type_eq_subst_eq)
qed

lemma type_eq_subst:
  assumes "atom x ♯ c"
  shows "{ z : b | c } = { x : b | c[z::=[x]^v]_cv }"
  using τ.eq_iff Abs1_eq_iff assms 
  using subst_cv_var_flip type_eq_flip by auto

lemma type_e_subst_fresh:
  fixes x::x and z::x
  assumes "atom z ♯ (x,v)" and "atom x ♯ e" 
  shows "{ z : b | CE_val (V_var z) == e }[x::=v]_\<tau>_v = { z : b | CE_val (V_var z) == e }"
  using assms subst_tv.simps subst_cv.simps forget_subst_cev by simp

lemma type_v_subst_fresh:
  fixes x::x and z::x
  assumes "atom z ♯ (x,v)" and "atom x ♯ v'" 
  shows "{ z : b | CE_val (V_var z) == CE_val v' }[x::=v]_\<tau>_v = { z : b | CE_val (V_var z) == CE_val v' }"
  using assms subst_tv.simps subst_cv.simps  by simp

lemma subst_tbase_eq:
  "b_of τ = b_of τ[x::=v]_\<tau>_v"
proof -
  obtain z and b and c where zbc: "τ = { z:b|c} ∧ atom z ♯ (x,v)" using τ.exhaust
    by (metis prod.inject subst_tv.cases)
  hence "b_of { z:b|c} = b_of { z:b|c}[x::=v]_\<tau>_v" using subst_tv.simps by simp
  thus ?thesis using zbc by blast
qed

lemma subst_tv_if:
  assumes "atom z1 ♯ (x,v)" and "atom z' ♯ (x,v)" 
  shows "{ z1 : b | CE_val (v'[x::=v]_vv) == CE_val (V_lit l) IMP (c'[x::=v]_cv)[z'::=[z1]^v]_cv } =
         { z1 : b | CE_val v' == CE_val (V_lit l) IMP c'[z'::=[z1]^v]_cv }[x::=v]_\<tau>_v" 
  using subst_cv_commute_full[of z' v x "V_var z1" c']  subst_tv.simps subst_vv.simps(1) subst_ev.simps  subst_cv.simps assms 
  by simp

lemma subst_tv_tid:
  assumes "atom za ♯ (x,v)"
  shows "{ za : B_id tid | TRUE } = { za : B_id tid | TRUE }[x::=v]_\<tau>_v"
  using assms subst_tv.simps subst_cv.simps by presburger


lemma b_of_subst:
  "b_of (τ[x::=v]_\<tau>_v) = b_of τ"
proof -
  obtain z b c where *:"τ = { z : b | c } ∧ atom z ♯ (x,v)" using obtain_fresh_z by metis
  thus ?thesis  using subst_tv.simps * by auto 
qed

lemma subst_tv_flip:
  assumes "τ'[x::=v]_\<tau>_v = τ" and "atom x ♯ (v,τ)" and "atom x' ♯ (v,τ)"
  shows "((x' ↔ x) ∙ τ')[x'::=v]_\<tau>_v = τ"
proof -
  have "(x' ↔ x) ∙ v = v ∧ (x' ↔ x) ∙ τ = τ" using assms flip_fresh_fresh by auto
  thus ?thesis using subst_tv.eqvt[of  "(x' ↔ x)"  τ' x v ] assms by auto
qed

lemma subst_cv_true:
  "{ z : B_id tid | TRUE } = { z : B_id tid | TRUE }[x::=v]_\<tau>_v" 
proof -
  obtain za::x where "atom za ♯ (x,v)" using obtain_fresh by auto
  hence "{ z : B_id tid | TRUE } = { za: B_id tid | TRUE }" using τ.eq_iff Abs1_eq_iff by fastforce
  moreover have  "{ za : B_id tid | TRUE } = { za : B_id tid | TRUE }[x::=v]_\<tau>_v"  
    using subst_cv.simps subst_tv.simps  by (simp add: ‹atom za ♯ (x, v)›)
  ultimately show ?thesis by argo
qed

lemma t_eq_supp:
  assumes "({ z : b | c }) = ({ z1 : b1 | c1 })"
  shows "supp c - { atom z } = supp c1 - { atom z1 }"
proof - 
  have "supp c - { atom z } ∪ supp b = supp c1 - { atom z1 } ∪ supp b1" using τ.supp assms
    by (metis list.set(1) list.simps(15) sup_bot.right_neutral supp_b_empty)
  moreover have "supp b = supp b1" using assms  τ.eq_iff by simp
  moreover have "atom z1 ∉ supp b1 ∧ atom z ∉ supp b" using  supp_b_empty by simp
  ultimately show ?thesis
    by (metis τ.eq_iff τ.supp assms b.supp(1) list.set(1) list.set(2) sup_bot.right_neutral)
qed

lemma fresh_t_eq: 
  fixes x::x
  assumes  "({ z : b | c }) = ({ zz : b | cc })" and "atom x ♯ c" and "x ≠ zz"
  shows "atom x ♯ cc"
proof - 
  have "supp c - { atom z } ∪ supp b = supp cc - { atom zz } ∪ supp b" using τ.supp assms
    by (metis list.set(1) list.simps(15) sup_bot.right_neutral supp_b_empty)
  moreover have "atom x ∉ supp c" using assms fresh_def by blast
  ultimately have "atom x ∉ supp cc - { atom zz } ∪ supp b" by force
  hence "atom x ∉ supp cc" using assms by simp
  thus ?thesis using fresh_def by auto
qed

section ‹Mutable Variable Context›

nominal_function subst_dv :: "Δ ==> x ==> v ==> Δ" where
  "subst_dv DNil x v = DNil"
| "subst_dv ((u,t) #_\<Delta> Δ) x v = ((u,t[x::=v]_\<tau>_v) #_\<Delta> (subst_dv Δ x v ))"
       apply (simp add: eqvt_def subst_dv_graph_aux_def,auto )
  using delete_aux.elims by (metis Δ.exhaust surj_pair)
nominal_termination (eqvt) by lexicographic_order

abbreviation 
  subst_dv_abbrev :: "Δ ==> x ==> v ==> Δ" (‹_[_::=_]_\Δ_v› [1000,50,50] 1000)
  where 
    "Δ[x::=v]_\<Delta>_v ≡ subst_dv Δ x v " 

nominal_function dmap :: "(u*τ ==> u*τ) ==> Δ ==> Δ" where
  "dmap f DNil = DNil"
| "dmap f ((u,t)#_\<Delta>Δ) = (f (u,t) #_\<Delta> (dmap f Δ ))"
       apply (simp add: eqvt_def dmap_graph_aux_def,auto )
  using delete_aux.elims by (metis Δ.exhaust surj_pair)
nominal_termination (eqvt) by lexicographic_order

lemma subst_dv_iff:
  "Δ[x::=v]_\<Delta>_v = dmap (λ(u,t). (u, t[x::=v]_\<tau>_v)) Δ"
  by(induct Δ, auto)

lemma size_subst_dv [simp]: "size ( subst_dv G i x) ≤ size G"
  by (induct G,auto) 

lemma forget_subst_dv [simp]: "atom a ♯ G ==> subst_dv G a x = G"
  apply (induct G ,auto) 
  using fresh_DCons fresh_PairD(1) not_self_fresh apply fastforce
  apply (simp add: fresh_DCons)+
  done

lemma subst_dv_member:
  assumes "(u,τ) ∈ setD Δ"
  shows  "(u, τ[x::=v]_\<tau>_v) ∈ setD (Δ[x::=v]_\<Delta>_v)"
  using assms  by(induct Δ rule: Δ_induct,auto)

lemma fresh_subst_dv:
  fixes x::x
  assumes "atom xa ♯ Δ" and "atom xa ♯ v"
  shows "atom xa ♯Δ[x::=v]_\<Delta>_v" 
  using assms proof(induct Δ rule:Δ_induct)
  case DNil
  then show ?case by auto
next
  case (DCons u t  Δ)
  then show ?case using subst_dv.simps  subst_v_τ_def fresh_DCons fresh_Pair by simp
qed

lemma fresh_subst_dv_if:
  fixes j::atom and i::x and  x::v and t::Δ
  assumes "j ♯ t ∧ j ♯ x" 
  shows  "(j ♯ subst_dv t i x)"
  using assms proof(induct t rule: Δ_induct)
  case DNil
  then show ?case using subst_gv.simps fresh_GNil by auto
next
  case (DCons u' t'  D')
  then show ?case unfolding subst_dv.simps using fresh_DCons fresh_subst_tv_if fresh_Pair by metis
qed

section ‹Statements›

text ‹ Using ideas from proofs at top of AFP/Launchbury/Substitution.thy.
 Subproofs borrowed from there; hence the apply style proofs. ›

nominal_function (default "case_sum (λx. Inl undefined) (case_sum (λx. Inl undefined) (λx. Inr undefined))")
  subst_sv :: "s ==> x ==> v ==> s"
  and subst_branchv :: "branch_s ==> x ==> v ==> branch_s" 
  and subst_branchlv :: "branch_list ==> x ==> v ==> branch_list" where
  "subst_sv ( (AS_val v') ) x v = (AS_val (subst_vv v' x v ))"
| "atom y ♯ (x,v) ==> subst_sv (AS_let y e s) x v = (AS_let y (e[x::=v]_ev) (subst_sv s x v ))"  
| "atom y ♯ (x,v) ==> subst_sv (AS_let2 y t s1 s2) x v = (AS_let2 y (t[x::=v]_\<tau>_v) (subst_sv s1 x v ) (subst_sv s2 x v ))"  
| " subst_sv (AS_match v' cs) x v = AS_match (v'[x::=v]_vv) (subst_branchlv cs x v )"
| "subst_sv (AS_assign y v') x v = AS_assign y (subst_vv v' x v )"
| "subst_sv ( (AS_if v' s1 s2) ) x v = (AS_if (subst_vv v' x v ) (subst_sv s1 x v ) (subst_sv s2 x v ) )"  
| "atom u ♯ (x,v) ==> subst_sv (AS_var u τ v' s) x v = AS_var u (subst_tv τ x v ) (subst_vv v' x v ) (subst_sv s x v ) "
| "subst_sv (AS_while s1 s2) x v = AS_while (subst_sv s1 x v ) (subst_sv s2 x v )"
| "subst_sv (AS_seq s1 s2) x v = AS_seq (subst_sv s1 x v ) (subst_sv s2 x v )" 
| "subst_sv (AS_assert c s) x v = AS_assert (subst_cv c x v) (subst_sv s x v)"
| "atom x1 ♯ (x,v) ==> subst_branchv (AS_branch dc x1 s1 ) x v = AS_branch dc x1 (subst_sv s1 x v )" 

| "subst_branchlv (AS_final cs) x v = AS_final (subst_branchv cs x v )"
| "subst_branchlv (AS_cons cs css) x v = AS_cons (subst_branchv cs x v ) (subst_branchlv css x v )"
                      apply (auto,simp add: eqvt_def subst_sv_subst_branchv_subst_branchlv_graph_aux_def )
proof(goal_cases)

  have eqvt_at_proj: "∧ s xa va . eqvt_at subst_sv_subst_branchv_subst_branchlv_sumC (Inl (s, xa, va)) ==>
           eqvt_at (λa. projl (subst_sv_subst_branchv_subst_branchlv_sumC (Inl a))) (s, xa, va)"
    apply(simp add: eqvt_at_def)
    apply(rule)
    apply(subst Projl_permute)
     apply(thin_tac _)+
     apply (simp add: subst_sv_subst_branchv_subst_branchlv_sumC_def)
     apply (simp add: THE_default_def)
     apply (case_tac "Ex1 (subst_sv_subst_branchv_subst_branchlv_graph (Inl (s,xa,va)))")
      apply simp
      apply(auto)[1]
      apply (erule_tac x="x" in allE)
      apply simp
      apply(cases rule: subst_sv_subst_branchv_subst_branchlv_graph.cases)    
                   apply(assumption)
                  apply(rule_tac x="Sum_Type.projl x" in exI,clarify,rule the1_equality,blast,simp (no_asm) only: sum.sel)+
        apply blast +

    apply(simp)+      
    done

  {
    case (1 P x')    
    then show ?case proof(cases x')
      case (Inl a) thus P 
      proof(cases a)
        case (fields aa bb cc)
        thus P using Inl 1 s_branch_s_branch_list.strong_exhaust fresh_star_insert by metis
      qed
    next
      case (Inr b) thus P
      proof(cases b)
        case (Inl a) thus P proof(cases a)
          case (fields aa bb cc)
          then show ?thesis  using Inr Inl 1 s_branch_s_branch_list.strong_exhaust fresh_star_insert by metis
        qed
      next
        case Inr2: (Inr b) thus P proof(cases b)
          case (fields aa bb cc)
          then show ?thesis  using Inr Inr2 1 s_branch_s_branch_list.strong_exhaust fresh_star_insert by metis
        qed
      qed
    qed
  next
    case (2 y s ya xa va sa c)
    thus ?case using eqvt_triple eqvt_at_proj by blast
  next
    case (3 y s2 ya xa va s1a s2a c)
    thus ?case using eqvt_triple eqvt_at_proj by blast
  next
    case (4 u xa va s ua sa c)
    moreover have "atom u ♯ (xa, va) ∧ atom ua ♯ (xa, va)" 
      using fresh_Pair u_fresh_xv by auto
    ultimately show ?case using eqvt_triple[of u xa va ua s sa]  subst_sv_def eqvt_at_proj by metis
  next
    case (5 x1 s1 x1a xa va s1a c)
    thus ?case using eqvt_triple eqvt_at_proj by blast
  }
qed
nominal_termination (eqvt) by lexicographic_order

abbreviation 
  subst_sv_abbrev :: "s ==> x ==> v ==> s" (‹_[_::=_]_sv› [1000,50,50] 1000)
  where 
    "s[x::=v]_sv ≡ subst_sv s x v" 

abbreviation 
  subst_branchv_abbrev :: "branch_s ==> x ==> v ==> branch_s" (‹_[_::=_]_sv› [1000,50,50] 1000)
  where 
    "s[x::=v]_sv ≡ subst_branchv s x v" 

lemma size_subst_sv [simp]:  "size (subst_sv A i x ) = size A" and  "size (subst_branchv B i x ) = size B"  and  "size (subst_branchlv C i x ) = size C"
  by(nominal_induct A and B and C avoiding: i x rule: s_branch_s_branch_list.strong_induct,auto)

lemma forget_subst_sv [simp]: shows  "atom a ♯ A ==> subst_sv A a x = A" and "atom a ♯ B ==> subst_branchv B a x = B" and "atom a ♯ C ==> subst_branchlv C a x = C"
  by (nominal_induct A and B and C avoiding: a x rule: s_branch_s_branch_list.strong_induct,auto simp: fresh_at_base)

lemma subst_sv_id [simp]: "subst_sv A a (V_var a) = A" and "subst_branchv B a (V_var a) = B" and  "subst_branchlv C a (V_var a) = C"
proof(nominal_induct A and B and C avoiding: a  rule: s_branch_s_branch_list.strong_induct) 
  case (AS_let x option e s)
  then show ?case 
    by (metis (no_types, lifting) fresh_Pair not_None_eq subst_ev_id subst_sv.simps(2) subst_sv.simps(3) subst_tv_id v.fresh(2))
next
  case (AS_match v branch_s)
  then show ?case using fresh_Pair not_None_eq subst_ev_id subst_sv.simps subst_sv.simps subst_tv_id v.fresh subst_vv_id
    by metis 
qed(auto)+ 

lemma fresh_subst_sv_if_rl:
  shows 
    "(atom x ♯ s ∧ j ♯ s) ∨ (j ♯ v ∧ (j ♯ s ∨ j = atom x)) ==> j ♯ (subst_sv s x v )" and
    "(atom x ♯ cs ∧ j ♯ cs) ∨ (j ♯ v ∧ (j ♯ cs ∨ j = atom x)) ==> j ♯ (subst_branchv cs x v)" and
    "(atom x ♯ css ∧ j ♯ css) ∨ (j ♯ v ∧ (j ♯ css ∨ j = atom x)) ==> j ♯ (subst_branchlv css x v )" 
    apply(nominal_induct s and cs and css avoiding: v x rule: s_branch_s_branch_list.strong_induct)
  using pure_fresh by force+

lemma fresh_subst_sv_if_lr:
  shows  "j ♯ (subst_sv s x v) ==> (atom x ♯ s ∧ j ♯ s) ∨ (j ♯ v ∧ (j ♯ s ∨ j = atom x))" and
    "j ♯ (subst_branchv cs x v) ==> (atom x ♯ cs ∧ j ♯ cs) ∨ (j ♯ v ∧ (j ♯ cs ∨ j = atom x))" and       
    "j ♯ (subst_branchlv css x v ) ==> (atom x ♯ css ∧ j ♯ css) ∨ (j ♯ v ∧ (j ♯ css ∨ j = atom x))"
proof(nominal_induct s and cs and css avoiding: v x rule: s_branch_s_branch_list.strong_induct)
  case (AS_branch list x s )
  then show ?case using s_branch_s_branch_list.fresh fresh_Pair list.distinct(1) list.set_cases pure_fresh set_ConsD subst_branchv.simps by metis
next
  case (AS_let y e s')
  thus ?case proof(cases "atom x ♯ (AS_let y e s')")
    case True
    hence "subst_sv (AS_let y e s') x v = (AS_let y e s')" using forget_subst_sv by simp
    hence "j ♯ (AS_let y e s')" using AS_let by argo
    then show ?thesis using True by blast
  next
    case False
    have "subst_sv (AS_let y e s') x v = AS_let y (e[x::=v]_ev) (s'[x::=v]_sv)" using subst_sv.simps(2) AS_let by force
    hence "((j ♯ s'[x::=v]_sv ∨ j ∈ set [atom y]) ∧ j ♯ None ∧ j ♯ e[x::=v]_ev)" using s_branch_s_branch_list.fresh AS_let 
      by (simp add: fresh_None)
    then show ?thesis using  AS_let  fresh_None fresh_subst_ev_if list.discI list.set_cases s_branch_s_branch_list.fresh set_ConsD 
      by metis
  qed
next
  case (AS_let2 y τ s1 s2)
  thus ?case proof(cases "atom x ♯ (AS_let2 y τ s1 s2)")
    case True
    hence "subst_sv (AS_let2 y τ s1 s2) x v = (AS_let2 y τ s1 s2)" using forget_subst_sv by simp
    hence "j ♯ (AS_let2 y τ s1 s2)" using AS_let2 by argo
    then show ?thesis using True by blast
  next
    case False
    have "subst_sv (AS_let2 y τ s1 s2) x v = AS_let2 y (τ[x::=v]_\<tau>_v) (s1[x::=v]_sv) (s2[x::=v]_sv)" using subst_sv.simps AS_let2 by force
    then show ?thesis using  AS_let2
        fresh_subst_tv_if list.discI list.set_cases s_branch_s_branch_list.fresh(4) set_ConsD by auto
  qed
qed(auto)+

lemma fresh_subst_sv_if[simp]:
  fixes x::x and v::v
  shows "j ♯ (subst_sv s x v) ⟷ (atom x ♯ s ∧ j ♯ s) ∨ (j ♯ v ∧ (j ♯ s ∨ j = atom x))" and
    "j ♯ (subst_branchv cs x v) ⟷ (atom x ♯ cs ∧ j ♯ cs) ∨ (j ♯ v ∧ (j ♯ cs ∨ j = atom x))"
  using fresh_subst_sv_if_lr fresh_subst_sv_if_rl by metis+

lemma subst_sv_commute [simp]:
  fixes A::s and t::v and j::x and i::x
  shows  "atom j ♯ A ==> (subst_sv (subst_sv A i t) j u ) = subst_sv A i (subst_vv t j u )" and
    "atom j ♯ B ==> (subst_branchv (subst_branchv B i t ) j u ) = subst_branchv B i (subst_vv t j u )" and
    "atom j ♯ C ==> (subst_branchlv (subst_branchlv C i t) j u ) = subst_branchlv C i (subst_vv t j u ) "
    apply(nominal_induct A and B and C avoiding: i j t u rule: s_branch_s_branch_list.strong_induct) 
  by(auto simp: fresh_at_base)

lemma c_eq_perm:
  assumes "( (atom z) ⇌ (atom z') ) ∙ c = c'" and "atom z' ♯ c"
  shows "{ z : b | c } = { z' : b | c' }"
  using τ.eq_iff Abs1_eq_iff(3) 
  by (metis Nominal2_Base.swap_commute assms(1) assms(2) flip_def swap_fresh_fresh)

lemma subst_sv_flip:
  fixes s::s and sa::s and v'::v
  assumes "atom c ♯ (s, sa)" and "atom c ♯ (v',x, xa, s, sa)" "atom x ♯ v'" and "atom xa ♯ v'" and "(x ↔ c) ∙ s = (xa ↔ c) ∙ sa" 
  shows "s[x::=v']_sv = sa[xa::=v']_sv"
proof - 
  have "atom x ♯ (s[x::=v']_sv)" and xafr: "atom xa ♯ (sa[xa::=v']_sv)" 
    and  "atom c ♯ ( s[x::=v']_sv, sa[xa::=v']_sv)" using assms using  fresh_subst_sv_if assms  by( blast+ ,force)

  hence "s[x::=v']_sv = (x ↔ c) ∙ (s[x::=v']_sv)"  by (simp add: flip_fresh_fresh fresh_Pair)
  also have " ... = ((x ↔ c) ∙ s)[ ((x ↔ c) ∙ x) ::= ((x ↔ c) ∙ v') ]_sv" using subst_sv_subst_branchv_subst_branchlv.eqvt  by blast
  also have "... = ((xa ↔ c) ∙ sa)[ ((x ↔ c) ∙ x) ::= ((x ↔ c) ∙ v') ]_sv" using assms by presburger
  also have "... = ((xa ↔ c) ∙ sa)[ ((xa ↔ c) ∙ xa) ::= ((xa ↔ c) ∙ v') ]_sv" using assms 
    by (metis flip_at_simps(1) flip_fresh_fresh fresh_PairD(1))
  also have "... = (xa ↔ c) ∙ (sa[xa::=v']_sv)" using subst_sv_subst_branchv_subst_branchlv.eqvt  by presburger
  also have "... = sa[xa::=v']_sv" using xafr assms by (simp add: flip_fresh_fresh fresh_Pair)
  finally show ?thesis by simp
qed

lemma if_type_eq:
  fixes Γ::Γ and v::v and z1::x
  assumes "atom z1' ♯ (v, ca, (x, b, c) #_\<Gamma> Γ, (CE_val v == CE_val (V_lit ll) IMP ca[za::=[z1]^v]_cv ))" and "atom z1 ♯ v" 
    and "atom z1 ♯ (za,ca)" and "atom z1' ♯ (za,ca)"
  shows "({ z1' : ba | CE_val v == CE_val (V_lit ll) IMP ca[za::=[z1']^v]_cv }) = { z1 : ba | CE_val v == CE_val (V_lit ll) IMP ca[za::=[z1]^v]_cv }"
proof -
  have "atom z1' ♯ (CE_val v == CE_val (V_lit ll) IMP ca[za::=[z1]^v]_cv )" using assms fresh_prod4 by blast
  moreover hence "(CE_val v == CE_val (V_lit ll) IMP ca[za::=[z1']^v]_cv) = (z1' ↔ z1) ∙ (CE_val v == CE_val (V_lit ll) IMP ca[za::=[z1]^v]_cv )"
  proof -
    have "(z1' ↔ z1) ∙ (CE_val v == CE_val (V_lit ll) IMP ca[za::=[z1]^v]_cv ) = ( (z1' ↔ z1) ∙ (CE_val v == CE_val (V_lit ll)) IMP ((z1' ↔ z1) ∙ ca[za::=[z1]^v]_cv ))"
      by auto
    also have "... = ((CE_val v == CE_val (V_lit ll)) IMP ((z1' ↔ z1) ∙ ca[za::=[z1]^v]_cv ))"
      using ‹atom z1 ♯ v› assms 
      by (metis (mono_tags) ‹atom z1' ♯ (CE_val v == CE_val (V_lit ll) IMP ca[za::=[z1]^v]_cv )› c.fresh(6) c.fresh(7) ce.fresh(1) flip_at_simps(2) flip_fresh_fresh fresh_at_base_permute_iff fresh_def supp_l_empty v.fresh(1))
    also have "... = ((CE_val v == CE_val (V_lit ll)) IMP (ca[za::=[z1']^v]_cv ))"
      using assms   by fastforce
    finally show ?thesis by auto
  qed
  ultimately show ?thesis    
    using τ.eq_iff Abs1_eq_iff(3)[of z1' "CE_val v == CE_val (V_lit ll) IMP ca[za::=[z1']^v]_cv" 
        z1 "CE_val v == CE_val (V_lit ll) IMP ca[za::=[z1]^v]_cv"] by blast
qed 

lemma subst_sv_var_flip:
  fixes x::x and s::s and z::x
  shows "atom x ♯ s ==> ((x ↔ z) ∙ s) = s[z::=[x]^v]_sv" and 
    "atom x ♯ cs ==> ((x ↔ z) ∙ cs) = subst_branchv cs z [x]^v" and
    "atom x ♯ css ==> ((x ↔ z) ∙ css) = subst_branchlv css z [x]^v"
    apply(nominal_induct s and cs and css avoiding: z x rule: s_branch_s_branch_list.strong_induct)
  using [[simproc del: alpha_lst]]
              apply (auto  ) (* This unpacks subst, perm *)
  using  subst_tv_var_flip  flip_fresh_fresh v.fresh s_branch_s_branch_list.fresh 
    subst_v_τ_def subst_v_v_def subst_vv_var_flip subst_v_e_def subst_ev_var_flip pure_fresh   apply auto 
     defer 1 (* Sometimes defering hard goals to the end makes it easier to finish *)
  using x_fresh_u   apply blast (* Next two involve u and flipping with x *)
    defer 1
  using x_fresh_u   apply blast
   defer 1
  using x_fresh_u Abs1_eq_iff'(3) flip_fresh_fresh 
   apply (simp add: subst_v_c_def)
  using x_fresh_u Abs1_eq_iff'(3) flip_fresh_fresh  
  by (simp add: flip_fresh_fresh)

instantiation s :: has_subst_v
begin

definition 
  "subst_v = subst_sv"

instance proof
  fix j::atom and i::x and  x::v and t::s
  show  "(j ♯ subst_v t i x) = ((atom i ♯ t ∧ j ♯ t) ∨ (j ♯ x ∧ (j ♯ t ∨ j = atom i)))"
    using fresh_subst_sv_if subst_v_s_def by auto

  fix a::x and tm::s and x::v
  show "atom a ♯ tm ==> subst_v tm a x = tm"
    using forget_subst_sv subst_v_s_def by simp

  fix a::x and tm::s
  show "subst_v tm a (V_var a) = tm" using subst_sv_id  subst_v_s_def by simp

  fix p::perm and x1::x and v::v and t1::s
  show "p ∙ subst_v t1 x1 v = subst_v (p ∙ t1) (p ∙ x1) (p ∙ v)" 
    using subst_sv_commute  subst_v_s_def by simp

  fix x::x and c::s and z::x
  show "atom x ♯ c ==> ((x ↔ z) ∙ c) = c[z::=[x]^v]_v"
    using subst_sv_var_flip subst_v_s_def by simp

  fix x::x and c::s and z::x
  show  "atom x ♯ c ==> c[z::=[x]^v]_v[x::=v]_v = c[z::=v]_v"
    using subst_sv_var_flip subst_v_s_def by simp
qed
end

section ‹Type Definition›

nominal_function subst_ft_v :: "fun_typ ==> x ==> v ==> fun_typ" where
  "atom z ♯ (x,v) ==> subst_ft_v ( AF_fun_typ z b c t (s::s)) x v = AF_fun_typ z b c[x::=v]_cv t[x::=v]_\<tau>_v s[x::=v]_sv"
     apply(simp add: eqvt_def subst_ft_v_graph_aux_def )
    apply(simp add:fun_typ.strong_exhaust )
   apply(auto) 
    apply(rule_tac y=a and c="(aa,b)" in fun_typ.strong_exhaust)
    apply (auto simp: eqvt_at_def fresh_star_def fresh_Pair fresh_at_base)

proof(goal_cases)
  case (1 z xa va c t s za ca ta sa cb)
  hence  "c[z::=[ cb ]^v]_cv = ca[za::=[ cb ]^v]_cv" 
    by (metis flip_commute subst_cv_var_flip)
  hence  "c[z::=[ cb ]^v]_cv[xa::=va]_cv = ca[za::=[ cb ]^v]_cv[xa::=va]_cv" by auto
  then show ?case using subst_cv_commute atom_eq_iff fresh_atom fresh_atom_at_base subst_cv_commute_full v.fresh 
    using 1 subst_cv_var_flip  flip_commute by metis
next
  case (2 z xa va c t s za ca ta sa cb)
  hence  "t[z::=[ cb ]^v]_\<tau>_v = ta[za::=[ cb ]^v]_\<tau>_v" by metis
  hence  "t[z::=[ cb ]^v]_\<tau>_v[xa::=va]_\<tau>_v = ta[za::=[ cb ]^v]_\<tau>_v[xa::=va]_\<tau>_v" by auto
  then show ?case using subst_tv_commute_full 2 
    by (metis atom_eq_iff fresh_atom fresh_atom_at_base v.fresh(2))
qed

nominal_termination (eqvt) by lexicographic_order

nominal_function subst_ftq_v :: "fun_typ_q ==> x ==> v ==> fun_typ_q" where
  "atom bv ♯ (x,v) ==> subst_ftq_v (AF_fun_typ_some bv ft) x v = (AF_fun_typ_some bv (subst_ft_v ft x v))" 
|  "subst_ftq_v (AF_fun_typ_none ft) x v = (AF_fun_typ_none (subst_ft_v ft x v))" 
       apply(simp add: eqvt_def subst_ftq_v_graph_aux_def )
      apply(simp add:fun_typ_q.strong_exhaust )
     apply(auto) 
   apply(rule_tac y=a and c="(aa,b)" in fun_typ_q.strong_exhaust)
    apply (auto simp: eqvt_at_def fresh_star_def fresh_Pair fresh_at_base)
proof(goal_cases)
  case (1 bv ft bva fta xa va c)
  then show ?case using subst_ft_v.simps  by (simp add: flip_fresh_fresh)
qed
nominal_termination (eqvt) by lexicographic_order

lemma size_subst_ft[simp]:  "size (subst_ft_v A x v) = size A" 
  by(nominal_induct A  avoiding: x v rule: fun_typ.strong_induct,auto)

lemma forget_subst_ft [simp]: shows  "atom x ♯ A ==> subst_ft_v A x a = A" 
  by (nominal_induct A  avoiding: a x rule: fun_typ.strong_induct,auto simp: fresh_at_base)

lemma subst_ft_id [simp]: "subst_ft_v A a (V_var a) = A"
  by(nominal_induct A  avoiding: a  rule: fun_typ.strong_induct,auto) 

instantiation fun_typ :: has_subst_v
begin

definition 
  "subst_v = subst_ft_v"

instance proof

  fix j::atom and i::x and  x::v and t::fun_typ
  show  "(j ♯ subst_v t i x) = ((atom i ♯ t ∧ j ♯ t) ∨ (j ♯ x ∧ (j ♯ t ∨ j = atom i)))"
    apply(nominal_induct t avoiding: i x rule:fun_typ.strong_induct)
    apply(simp only: subst_v_fun_typ_def subst_ft_v.simps )
    using fun_typ.fresh fresh_subst_v_if apply simp
    by auto

  fix a::x and tm::fun_typ and x::v
  show "atom a ♯ tm ==> subst_v tm a x = tm"
  proof(nominal_induct tm avoiding: a x rule:fun_typ.strong_induct)
    case (AF_fun_typ x1a x2a x3a x4a x5a)
    then show ?case unfolding subst_ft_v.simps subst_v_fun_typ_def fun_typ.fresh  using forget_subst_v subst_ft_v.simps subst_v_c_def forget_subst_sv subst_v_τ_def by fastforce
  qed

  fix a::x and tm::fun_typ
  show "subst_v tm a (V_var a) = tm" 
  proof(nominal_induct tm avoiding: a x rule:fun_typ.strong_induct)
    case (AF_fun_typ x1a x2a x3a x4a x5a)
    then show ?case unfolding subst_ft_v.simps subst_v_fun_typ_def fun_typ.fresh  using forget_subst_v subst_ft_v.simps subst_v_c_def forget_subst_sv subst_v_τ_def by fastforce
  qed

  fix p::perm and x1::x and v::v and t1::fun_typ
  show "p ∙ subst_v t1 x1 v = subst_v (p ∙ t1) (p ∙ x1) (p ∙ v)" 
  proof(nominal_induct t1 avoiding: x1 v rule:fun_typ.strong_induct)
    case (AF_fun_typ x1a x2a x3a x4a x5a)
    then show ?case unfolding subst_ft_v.simps subst_v_fun_typ_def fun_typ.fresh  using forget_subst_v subst_ft_v.simps subst_v_c_def forget_subst_sv subst_v_τ_def by fastforce
  qed

  fix x::x and c::fun_typ and z::x
  show "atom x ♯ c ==> ((x ↔ z) ∙ c) = c[z::=[x]^v]_v"
    apply(nominal_induct c avoiding: x z rule:fun_typ.strong_induct)
    by (auto simp add: subst_v_c_def subst_v_s_def subst_v_τ_def subst_v_fun_typ_def)

  fix x::x and c::fun_typ and z::x
  show  "atom x ♯ c ==> c[z::=[x]^v]_v[x::=v]_v = c[z::=v]_v"
    apply(nominal_induct c avoiding: z x v rule:fun_typ.strong_induct)
    apply auto
    by (auto simp add: subst_v_c_def subst_v_s_def subst_v_τ_def subst_v_fun_typ_def )
qed
end

instantiation fun_typ_q :: has_subst_v
begin

definition 
  "subst_v = subst_ftq_v"

instance proof
  fix j::atom and i::x and  x::v and t::fun_typ_q
  show  "(j ♯ subst_v t i x) = ((atom i ♯ t ∧ j ♯ t) ∨ (j ♯ x ∧ (j ♯ t ∨ j = atom i)))"
    apply(nominal_induct t avoiding: i x rule:fun_typ_q.strong_induct,auto)
                   apply(auto simp add: subst_v_fun_typ_def subst_v_s_def subst_v_τ_def subst_v_fun_typ_q_def fresh_subst_v_if )    
    by (metis (no_types) fresh_subst_v_if subst_v_fun_typ_def)+

  fix i::x and t::fun_typ_q and x::v
  show "atom i ♯ t ==> subst_v t i x = t"
    apply(nominal_induct t avoiding: i x rule:fun_typ_q.strong_induct,auto)
    by(auto simp add: subst_v_fun_typ_def subst_v_s_def subst_v_τ_def subst_v_fun_typ_q_def fresh_subst_v_if )    

  fix i::x and t::fun_typ_q
  show "subst_v t i (V_var i) = t" using subst_cv_id  subst_v_fun_typ_def  
    apply(nominal_induct t avoiding: i x rule:fun_typ_q.strong_induct,auto)
    by(auto simp add: subst_v_fun_typ_def subst_v_s_def subst_v_τ_def subst_v_fun_typ_q_def fresh_subst_v_if )  

  fix p::perm and x1::x and v::v and t1::fun_typ_q
  show "p ∙ subst_v t1 x1 v = subst_v (p ∙ t1) (p ∙ x1) (p ∙ v)" 
    apply(nominal_induct t1 avoiding: v x1 rule:fun_typ_q.strong_induct,auto)
    by(auto simp add: subst_v_fun_typ_def subst_v_s_def subst_v_τ_def subst_v_fun_typ_q_def fresh_subst_v_if )  

  fix x::x and c::fun_typ_q and z::x
  show "atom x ♯ c ==> ((x ↔ z) ∙ c) = c[z::=[x]^v]_v"
    apply(nominal_induct c avoiding: x z rule:fun_typ_q.strong_induct,auto)
    by(auto simp add: subst_v_fun_typ_def subst_v_s_def subst_v_τ_def subst_v_fun_typ_q_def fresh_subst_v_if )  

  fix x::x and c::fun_typ_q and z::x
  show  "atom x ♯ c ==> c[z::=[x]^v]_v[x::=v]_v = c[z::=v]_v"
    apply(nominal_induct c avoiding: z x v rule:fun_typ_q.strong_induct,auto)
     apply(auto simp add: subst_v_fun_typ_def subst_v_s_def subst_v_τ_def subst_v_fun_typ_q_def fresh_subst_v_if )  
    by (metis subst_v_fun_typ_def flip_bv_x_cancel subst_ft_v.eqvt subst_v_simple_commute v.perm_simps )+
qed

end

section ‹Variable Context›

lemma subst_dv_fst_eq:
  "fst ` setD (Δ[x::=v]<sub>\</sub><Delta><sub>v</sub>) = fst ` setD Δ" 
  by(induct Δ rule: Δ_induct,simp,force)

lemma subst_gv_member_iff:
  fixes x'::x and x::x and v::v and c'::c
  assumes "(x',b',c') ∈ toSet Γ" and "atom x ∉ atom_dom Γ" 
  shows "(x',b',c'[x::=v]_cv) ∈ toSet Γ[x::=v]_\<Gamma>_v"
proof -
  have "x' ≠ x" using assms fresh_dom_free2 by metis
  then show ?thesis  using assms proof(induct Γ rule: Γ_induct)
    case GNil
    then show ?case by auto
  next
    case (GCons x1 b1 c1 Γ')
    show ?case proof(cases "(x',b',c') = (x1,b1,c1)")
      case True
      hence "((x1, b1, c1) #_\<Gamma> Γ')[x::=v]_\<Gamma>_v = ((x1, b1, c1[x::=v]_cv) #_\<Gamma> (Γ'[x::=v]_\<Gamma>_v))"  using subst_gv.simps  ‹x'≠x› by auto
      then show ?thesis using True by auto
    next
      case False
      have "x1≠x" using fresh_def fresh_GCons fresh_Pair supp_at_base GCons fresh_dom_free2 by auto
      hence "(x', b', c') ∈ toSet Γ'" using GCons False toSet.simps by auto
      moreover have "atom x ∉ atom_dom Γ'" using fresh_GCons GCons dom.simps toSet.simps by simp
      ultimately have  "(x', b', c'[x::=v]_cv) ∈ toSet Γ'[x::=v]_\<Gamma>_v" using GCons by auto
      hence "(x', b', c'[x::=v]_cv) ∈ toSet ((x1, b1, c1[x::=v]_cv) #_\<Gamma> (Γ'[x::=v]_\<Gamma>_v))" by auto
      then show ?thesis using subst_gv.simps ‹x1≠x› by auto
    qed
  qed
qed

lemma fresh_subst_gv_if:
  fixes j::atom and i::x and  x::v and t::Γ
  assumes "j ♯ t ∧ j ♯ x" 
  shows  "(j ♯ subst_gv t i x)"
  using assms proof(induct t rule: Γ_induct)
  case GNil
  then show ?case using subst_gv.simps fresh_GNil by auto
next
  case (GCons x' b' c' Γ')
  then show ?case unfolding subst_gv.simps using fresh_GCons fresh_subst_cv_if by auto
qed

section ‹Lookup›

lemma set_GConsD: "y ∈ toSet (x #_\<Gamma> xs) ==> y=x ∨ y ∈ toSet xs"
  by auto

lemma  subst_g_assoc_cons:
  assumes "x ≠ x'"
  shows "(((x', b', c') #_\<Gamma> Γ')[x::=v]_\<Gamma>_v @ G) = ((x', b', c'[x::=v]_cv) #_\<Gamma> ((Γ'[x::=v]_\<Gamma>_v) @ G))"
  using subst_gv.simps append_g.simps assms by auto

end