Quelle  BTVSubst.thy

(*<*)
theory BTVSubst
  imports Syntax
begin
  (*>*)
chapter ‹Basic Type Variable Substitution›

section ‹Class›

class has_subst_b = fs +
  fixes subst_b :: "'a::fs ==> bv ==> b ==> 'a::fs" (‹_[_::=_]_b› [1000,50,50] 1000)

assumes fresh_subst_if:  "j ♯ (t[i::=x]_b ) ⟷ (atom i ♯ t ∧ j ♯ t) ∨ (j ♯ x ∧ (j ♯ t ∨ j = atom i))" 
  and    forget_subst[simp]:  "atom a ♯ tm ==> tm[a::=x]_b = tm"
  and    subst_id[simp]:      "tm[a::=(B_var a)]_b = tm"
  and    eqvt[simp,eqvt]:          "(p::perm) ∙ (subst_b t1 x1 v ) = (subst_b (p ∙t1) (p ∙x1) (p ∙v) )"
  and    flip_subst[simp]:    "atom bv ♯ c ==> ((bv ↔ z) ∙ c) = c[z::=B_var bv]_b"
  and    flip_subst_subst[simp]: "atom bv ♯ c ==> ((bv ↔ z) ∙ c)[bv::=v]_b = c[z::=v]_b"
begin

lemmas flip_subst_b = flip_subst_subst

lemma subst_b_simple_commute:
  fixes x::bv
  assumes "atom x ♯ c" 
  shows "(c[z::=B_var x]_b)[x::=b]_b = c[z::=b]_b" 
proof - 
  have "(c[z::=B_var x]_b)[x::=b]_b = (( x ↔ z) ∙ c)[x::=b]_b" using flip_subst assms by simp
  thus ?thesis using flip_subst_subst assms by simp
qed

lemma subst_b_flip_eq_one:
  fixes z1::bv and z2::bv and x1::bv and x2::bv  
  assumes "[[atom z1]]lst. c1 = [[atom z2]]lst. c2" 
    and "atom x1 ♯ (z1,z2,c1,c2)"
  shows "(c1[z1::=B_var x1]_b) = (c2[z2::=B_var x1]_b)"
proof -  
  have "(c1[z1::=B_var x1]_b) = (x1 ↔ z1) ∙ c1" using assms flip_subst by auto
  moreover have  "(c2[z2::=B_var x1]_b) = (x1 ↔ z2) ∙ c2" using assms flip_subst 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_b_flip_eq_two:
  fixes z1::bv and z2::bv and x1::bv and x2::bv  
  assumes "[[atom z1]]lst. c1 = [[atom z2]]lst. c2" 
  shows "(c1[z1::=b]_b) = (c2[z2::=b]_b)"
proof -
  obtain x::bv where *:"atom x ♯ (z1,z2,c1,c2)" using obtain_fresh by metis
  hence "(c1[z1::=B_var x]_b) = (c2[z2::=B_var x]_b)" using subst_b_flip_eq_one[OF assms, of x] by metis
  hence "(c1[z1::=B_var x]_b)[x::=b]_b = (c2[z2::=B_var x]_b)[x::=b]_b" by auto
  thus ?thesis using subst_b_simple_commute * fresh_prod4 by metis
qed

lemma subst_b_fresh_x:
  fixes tm::"'a::fs" and x::x
  shows "atom x ♯ tm = atom x ♯ tm[bv::=b']_b"
  using fresh_subst_if[of "atom x" tm bv b'] using x_fresh_b by auto

lemma subst_b_x_flip[simp]:
  fixes x'::x and x::x and bv::bv 
  shows "((x' ↔ x) ∙ tm)[bv::=b']_b = (x' ↔ x) ∙ (tm[bv::=b']_b)"
proof - 
  have "(x' ↔ x) ∙ bv = bv" using pure_supp flip_fresh_fresh by force
  moreover have "(x' ↔ x) ∙ b' = b'" using x_fresh_b flip_fresh_fresh by auto
  ultimately show ?thesis using eqvt by simp
qed

end

section ‹Base Type›

nominal_function subst_bb :: "b ==> bv ==> b ==> b" where
  "subst_bb (B_var bv2) bv1 b = (if bv1 = bv2 then b else (B_var bv2))"
| "subst_bb B_int bv1 b = B_int"
| "subst_bb B_bool bv1 b = B_bool"
| "subst_bb (B_id s) bv1 b = B_id s "
| "subst_bb (B_pair b1 b2) bv1 b = B_pair (subst_bb b1 bv1 b) (subst_bb b2 bv1 b)"
| "subst_bb B_unit bv1 b = B_unit "
| "subst_bb B_bitvec bv1 b = B_bitvec "
| "subst_bb (B_app s b2) bv1 b = B_app s (subst_bb b2 bv1 b)"
                      apply (simp add: eqvt_def subst_bb_graph_aux_def )
                      apply (simp add: eqvt_def subst_bb_graph_aux_def )
  by (auto,meson b.strong_exhaust)
nominal_termination (eqvt) by lexicographic_order

abbreviation 
  subst_bb_abbrev :: "b ==> bv ==> b ==> b" (‹_[_::=_]_bb› [1000,50,50] 1000)
  where 
    "b[bv::=b']_bb ≡ subst_bb b bv b' " 

instantiation b :: has_subst_b
begin
definition "subst_b = subst_bb"

instance proof
  fix j::atom and i::bv and  x::b and t::b
  show  "j ♯ subst_b t i x = (atom i ♯ t ∧ j ♯ t ∨ j ♯ x ∧ (j ♯ t ∨ j = atom i))"
  proof (induct t rule: b.induct)
    case (B_id x)
    then show ?case using subst_bb.simps fresh_def pure_fresh subst_b_b_def by auto
  next
    case (B_var x)
    then show ?case using subst_bb.simps fresh_def pure_fresh subst_b_b_def by auto
  next
    case (B_app x1 x2)
    then show ?case using subst_bb.simps fresh_def pure_fresh subst_b_b_def by auto
  qed(auto simp add: subst_bb.simps fresh_def pure_fresh subst_b_b_def)+

  fix a::bv and tm::b and x::b
  show "atom a ♯ tm ==> tm[a::=x]_b = tm"
    by (induct tm rule: b.induct, auto simp add: fresh_at_base subst_bb.simps subst_b_b_def)

  fix a::bv and tm::b
  show "subst_b tm a (B_var a) = tm" using subst_bb.simps  subst_b_b_def 
    by (induct tm rule: b.induct, auto simp add: fresh_at_base subst_bb.simps subst_b_b_def)

  fix p::perm and x1::bv and v::b and t1::b
  show "p ∙ subst_b t1 x1 v = subst_b (p ∙ t1) (p ∙ x1) (p ∙ v)" 
    by (induct tm rule: b.induct, auto simp add: fresh_at_base subst_bb.simps subst_b_b_def)

  fix  bv::bv and c::b and z::bv
  show "atom bv ♯ c ==> ((bv ↔ z) ∙ c) = c[z::=B_var bv]_b"
    by (induct c rule: b.induct,  (auto simp add: fresh_at_base subst_bb.simps subst_b_b_def permute_pure pure_supp )+)

  fix bv::bv and c::b and z::bv and v::b
  show "atom bv ♯ c ==> ((bv ↔ z) ∙ c)[bv::=v]_b = c[z::=v]_b"
    by (induct c rule: b.induct,  (auto simp add: fresh_at_base subst_bb.simps subst_b_b_def permute_pure pure_supp )+)
qed
end

lemma subst_bb_inject:
  assumes "b1 = b2[bv::=b]_bb" and "b2 ≠ B_var bv" 
  shows 
    "b1 = B_int ==> b2 = B_int" and 
    "b1 = B_bool ==> b2 = B_bool" and 
    "b1 = B_unit ==> b2 = B_unit" and 
    "b1 = B_bitvec ==> b2 = B_bitvec" and 
    "b1 = B_pair b11 b12 ==> (∃b11' b12' . b11 = b11'[bv::=b]_bb ∧ b12 = b12'[bv::=b]_bb ∧ b2 = B_pair b11' b12')" and
    "b1 = B_var bv' ==> b2 = B_var bv'" and
    "b1 = B_id tyid ==> b2 = B_id tyid" and
    "b1 = B_app tyid b11 ==> (∃b11'. b11= b11'[bv::=b]_bb ∧ b2 = B_app tyid b11')"
  using assms by(nominal_induct b2 rule:b.strong_induct,auto+)

lemma flip_b_subst4:
  fixes b1::b and bv1::bv and c::bv and b::b
  assumes "atom c ♯ (b1,bv1)" 
  shows "b1[bv1::=b]_bb = ((bv1 ↔ c) ∙ b1)[c ::= b]_bb" 
  using assms proof(nominal_induct b1 rule: b.strong_induct)
  case B_int
  then show ?case using subst_bb.simps b.perm_simps by auto
next
  case B_bool
  then show ?case using subst_bb.simps b.perm_simps by auto
next
  case (B_id x)
  hence "atom bv1 ♯ x ∧ atom c ♯ x" using fresh_def  pure_supp by auto
  hence "((bv1 ↔ c) ∙ B_id x) = B_id x" using fresh_Pair b.fresh(3) flip_fresh_fresh b.perm_simps fresh_def pure_supp by metis
  then show ?case using subst_bb.simps by simp
next
  case (B_pair x1 x2)
  hence "x1[bv1::=b]_bb = ((bv1 ↔ c) ∙ x1)[c::=b]_bb" using  b.perm_simps(4) b.fresh(4) fresh_Pair  by metis
  moreover have  "x2[bv1::=b]_bb = ((bv1 ↔ c) ∙ x2)[c::=b]_bb" using  b.perm_simps(4) b.fresh(4) fresh_Pair B_pair by metis
  ultimately  show ?case using subst_bb.simps(5) b.perm_simps(4) b.fresh(4) fresh_Pair by auto
next
  case B_unit
  then show ?case using subst_bb.simps b.perm_simps by auto
next
  case B_bitvec
  then show ?case using subst_bb.simps b.perm_simps by auto
next
  case (B_var x)
  then show ?case proof(cases "x=bv1")
    case True
    then show ?thesis using B_var subst_bb.simps b.perm_simps by simp
  next
    case False
    moreover have "x≠c" using B_var b.fresh fresh_def supp_at_base fresh_Pair by fastforce
    ultimately show ?thesis using B_var subst_bb.simps(1) b.perm_simps(7) by simp
  qed
next
  case (B_app x1 x2)
  hence "x2[bv1::=b]_bb = ((bv1 ↔ c) ∙ x2)[c::=b]_bb" using  b.perm_simps b.fresh fresh_Pair  by metis 
  thus ?case using subst_bb.simps b.perm_simps b.fresh fresh_Pair B_app 
    by (simp add: permute_pure)
qed

lemma subst_bb_flip_sym:
  fixes b1::b and b2::b
  assumes "atom c ♯ b" and "atom c ♯ (bv1,bv2, b1, b2)" and "(bv1 ↔ c) ∙ b1 = (bv2 ↔ c) ∙ b2" 
  shows "b1[bv1::=b]_bb = b2[bv2::=b]_bb"
  using assms  flip_b_subst4[of c b1 bv1 b]   flip_b_subst4[of c b2 bv2 b] fresh_prod4 fresh_Pair by simp

section ‹Value›

nominal_function subst_vb :: "v ==> bv ==> b ==> v" where
  "subst_vb (V_lit l) x v = V_lit l"
| "subst_vb (V_var y) x v = V_var y"
| "subst_vb (V_cons tyid c v') x v = V_cons tyid c (subst_vb v' x v)"
| "subst_vb (V_consp tyid c b v') x v = V_consp tyid c (subst_bb b x v) (subst_vb v' x v)"
| "subst_vb (V_pair v1 v2) x v = V_pair (subst_vb v1 x v ) (subst_vb v2 x v )"
                   apply (simp add: eqvt_def subst_vb_graph_aux_def)
                  apply auto
  using v.strong_exhaust by meson
nominal_termination (eqvt) by lexicographic_order

abbreviation 
  subst_vb_abbrev :: "v ==> bv ==> b ==> v" (‹_[_::=_]_vb› [1000,50,50] 500)
  where 
    "e[bv::=b]_vb ≡ subst_vb e bv b" 

instantiation v :: has_subst_b
begin
definition "subst_b = subst_vb"

instance proof
  fix j::atom and i::bv and  x::b and t::v
  show  "j ♯ subst_b t i x = (atom i ♯ t ∧ j ♯ t ∨ j ♯ x ∧ (j ♯ t ∨ j = atom i))"
  proof (induct t rule: v.induct)
    case (V_lit l)
    have "j ♯ subst_b (V_lit l) i x = j ♯ (V_lit l)"  using subst_vb.simps fresh_def pure_fresh 
        subst_b_v_def v.supp  v.fresh has_subst_b_class.fresh_subst_if subst_b_b_def subst_b_v_def by auto
    also have "... = True" using fresh_at_base v.fresh l.fresh supp_l_empty fresh_def by metis      
    moreover have "(atom i ♯ (V_lit l) ∧ j ♯ (V_lit l) ∨ j ♯ x ∧ (j ♯ (V_lit l) ∨ j = atom i)) = True" using fresh_at_base v.fresh l.fresh supp_l_empty fresh_def by metis
    ultimately show ?case by simp
  next
    case (V_var y)
    then show ?case using  subst_b_v_def subst_vb.simps pure_fresh by force   
  next
    case (V_pair x1a x2a)
    then show ?case using subst_b_v_def subst_vb.simps by auto  
  next
    case (V_cons x1a x2a x3)       
    then show ?case using V_cons subst_b_v_def subst_vb.simps pure_fresh by force
  next
    case (V_consp x1a x2a x3 x4)
    then show ?case using  subst_b_v_def subst_vb.simps pure_fresh  has_subst_b_class.fresh_subst_if subst_b_b_def subst_b_v_def by fastforce
  qed

  fix a::bv and tm::v and x::b
  show "atom a ♯ tm ==> subst_b tm a x = tm"
    apply(induct tm rule: v.induct)
        apply(auto simp add: fresh_at_base subst_vb.simps subst_b_v_def)
    using has_subst_b_class.fresh_subst_if  subst_b_b_def e.fresh 
    using has_subst_b_class.forget_subst by fastforce

  fix a::bv and tm::v
  show "subst_b tm a (B_var a) = tm" using subst_bb.simps  subst_b_b_def 
    apply (induct tm rule: v.induct)
        apply(auto simp add: fresh_at_base subst_vb.simps subst_b_v_def)
    using has_subst_b_class.fresh_subst_if  subst_b_b_def e.fresh 
    using has_subst_b_class.subst_id by metis

  fix p::perm and x1::bv and v::b and t1::v
  show "p ∙ subst_b t1 x1 v = subst_b (p ∙ t1) (p ∙ x1) (p ∙ v)" 
    apply(induct tm rule: v.induct)
        apply(auto simp add: fresh_at_base subst_bb.simps subst_b_b_def )
    using has_subst_b_class.eqvt  subst_b_b_def e.fresh 
    using has_subst_b_class.eqvt 
    by (simp add: subst_b_v_def)+

  fix  bv::bv and c::v and z::bv
  show "atom bv ♯ c ==> ((bv ↔ z) ∙ c) = c[z::=B_var bv]_b"
    apply (induct c rule: v.induct,  (auto simp add: fresh_at_base  subst_vb.simps subst_b_v_def permute_pure pure_supp )+)
     apply (metis flip_fresh_fresh flip_l_eq permute_flip_cancel2)
    using  fresh_at_base flip_fresh_fresh[of bv  x z] 
    apply (simp add: flip_fresh_fresh)
    using subst_b_b_def by argo

  fix bv::bv and c::v and z::bv and v::b
  show "atom bv ♯ c ==> ((bv ↔ z) ∙ c)[bv::=v]_b = c[z::=v]_b"
    apply (induct c rule: v.induct,  (auto simp add: fresh_at_base  subst_vb.simps subst_b_v_def permute_pure pure_supp )+)
     apply (metis flip_fresh_fresh flip_l_eq permute_flip_cancel2)
    using  fresh_at_base flip_fresh_fresh[of bv  x z] 
    apply (simp add: flip_fresh_fresh)
    using     subst_b_b_def  flip_subst_subst by fastforce

qed
end

section ‹Constraints Expressions›

nominal_function subst_ceb :: "ce ==> bv ==> b ==> ce" where
  "subst_ceb ( (CE_val v') ) bv b = ( CE_val (subst_vb v' bv b) )"
| "subst_ceb ( (CE_op opp v1 v2) ) bv b = ( (CE_op opp (subst_ceb v1 bv b)(subst_ceb v2 bv b)) )"
| "subst_ceb ( (CE_fst v')) bv b = CE_fst (subst_ceb v' bv b)"
| "subst_ceb ( (CE_snd v')) bv b = CE_snd (subst_ceb v' bv b)"
| "subst_ceb ( (CE_len v')) bv b = CE_len (subst_ceb v' bv b)"
| "subst_ceb ( CE_concat v1 v2) bv b = CE_concat (subst_ceb v1 bv b) (subst_ceb v2 bv b)"
                      apply (simp add: eqvt_def subst_ceb_graph_aux_def)
                      apply auto
  by (meson ce.strong_exhaust)
nominal_termination (eqvt) by lexicographic_order

abbreviation 
  subst_ceb_abbrev :: "ce ==> bv ==> b ==> ce" (‹_[_::=_]_ceb› [1000,50,50] 500)
  where 
    "ce[bv::=b]_ceb ≡ subst_ceb ce bv b" 

instantiation ce :: has_subst_b
begin
definition "subst_b = subst_ceb"

instance proof
  fix j::atom and i::bv and  x::b and t::ce
  show  "j ♯ subst_b t i x = (atom i ♯ t ∧ j ♯ t ∨ j ♯ x ∧ (j ♯ t ∨ j = atom i))"
  proof (induct t rule: ce.induct)
    case (CE_val v)
    then show ?case using subst_ceb.simps fresh_def pure_fresh subst_b_ce_def ce.supp v.supp  ce.fresh has_subst_b_class.fresh_subst_if subst_b_b_def subst_b_v_def
      by metis
  next
    case (CE_op opp v1 v2)    

    have "(j ♯ v1[i::=x]_ceb ∧ j ♯ v2[i::=x]_ceb) = ((atom i ♯ v1 ∧ atom i ♯ v2) ∧ j ♯ v1 ∧ j ♯ v2 ∨ j ♯ x ∧ (j ♯ v1 ∧ j ♯ v2 ∨ j = atom i))"
      using has_subst_b_class.fresh_subst_if subst_b_v_def 
      using CE_op.hyps(1) CE_op.hyps(2) subst_b_ce_def by auto

    thus ?case  unfolding subst_ceb.simps subst_b_ce_def ce.fresh 
      using fresh_def pure_fresh opp.fresh subst_b_v_def  opp.exhaust fresh_e_opp_all
      by (metis (full_types))      
  next
    case (CE_concat x1a x2)
    then show ?case  using subst_ceb.simps  subst_b_ce_def e.supp v.supp  has_subst_b_class.fresh_subst_if subst_b_v_def  ce.fresh by force
  next
    case (CE_fst x)
    then show ?case using subst_ceb.simps  subst_b_ce_def e.supp v.supp  has_subst_b_class.fresh_subst_if subst_b_v_def  ce.fresh by metis

  next
    case (CE_snd x)
    then show ?case using subst_ceb.simps  subst_b_ce_def e.supp v.supp  has_subst_b_class.fresh_subst_if subst_b_v_def  ce.fresh by metis
  next
    case (CE_len x)
    then show ?case using subst_ceb.simps  subst_b_ce_def e.supp v.supp  has_subst_b_class.fresh_subst_if subst_b_v_def  ce.fresh by metis
  qed

  fix a::bv and tm::ce and x::b
  show "atom a ♯ tm ==> subst_b tm a x = tm"
    apply(induct tm rule: ce.induct)
         apply( auto simp add: fresh_at_base subst_ceb.simps subst_b_ce_def)
    using has_subst_b_class.fresh_subst_if  subst_b_b_def e.fresh 
    using has_subst_b_class.forget_subst subst_b_v_def apply metis+
    done

  fix a::bv and tm::ce
  show "subst_b tm a (B_var a) = tm" using subst_bb.simps  subst_b_b_def 
    apply (induct tm rule: ce.induct)
         apply(auto simp add: fresh_at_base subst_ceb.simps subst_b_ce_def)
    using has_subst_b_class.fresh_subst_if  subst_b_b_def e.fresh 
    using has_subst_b_class.subst_id subst_b_v_def apply metis+
    done

  fix p::perm and x1::bv and v::b and t1::ce
  show "p ∙ subst_b t1 x1 v = subst_b (p ∙ t1) (p ∙ x1) (p ∙ v)" 
    apply(induct tm rule: ce.induct)
         apply( auto simp add: fresh_at_base subst_bb.simps subst_b_b_def )
    using has_subst_b_class.eqvt  subst_b_b_def ce.fresh 
    using has_subst_b_class.eqvt 
    by (simp add: subst_b_ce_def)+

  fix  bv::bv and c::ce and z::bv
  show "atom bv ♯ c ==> ((bv ↔ z) ∙ c) = c[z::=B_var bv]_b"
    apply (induct c rule: ce.induct,  (auto simp add: fresh_at_base  subst_ceb.simps subst_b_ce_def permute_pure pure_supp )+)
    using  flip_fresh_fresh flip_l_eq permute_flip_cancel2 has_subst_b_class.flip_subst subst_b_v_def apply metis
    using  flip_fresh_fresh flip_l_eq permute_flip_cancel2 has_subst_b_class.flip_subst subst_b_v_def 
    by (simp add: flip_fresh_fresh fresh_opp_all)  

  fix bv::bv and c::ce and z::bv and v::b
  show "atom bv ♯ c ==> ((bv ↔ z) ∙ c)[bv::=v]_b = c[z::=v]_b"
  proof (induct c rule: ce.induct)
    case (CE_val x)
    then show ?case using flip_subst_subst subst_b_v_def subst_ceb.simps  using subst_b_ce_def by fastforce
  next
    case (CE_op x1a x2 x3)
    then show ?case unfolding subst_ceb.simps subst_b_ce_def ce.perm_simps using flip_subst_subst subst_b_v_def  opp.perm_simps opp.strong_exhaust 
      by (metis (full_types) ce.fresh(2))
  next
    case (CE_concat x1a x2)
    then show ?case using flip_subst_subst subst_b_v_def subst_ceb.simps  using subst_b_ce_def by fastforce
  next
    case (CE_fst x)
    then show ?case using flip_subst_subst subst_b_v_def subst_ceb.simps  using subst_b_ce_def by fastforce
  next
    case (CE_snd x)
    then show ?case using flip_subst_subst subst_b_v_def subst_ceb.simps  using subst_b_ce_def by fastforce
  next
    case (CE_len x)
    then show ?case using flip_subst_subst subst_b_v_def subst_ceb.simps  using subst_b_ce_def by fastforce
  qed
qed
end

section ‹Constraints›

nominal_function subst_cb :: "c ==> bv ==> b ==> c" where
  "subst_cb (C_true) x v = C_true"
|  "subst_cb (C_false) x v = C_false"
|  "subst_cb (C_conj c1 c2) x v = C_conj (subst_cb c1 x v ) (subst_cb c2 x v )"
|  "subst_cb (C_disj c1 c2) x v = C_disj (subst_cb c1 x v ) (subst_cb c2 x v )"
|  "subst_cb (C_imp c1 c2) x v = C_imp (subst_cb c1 x v ) (subst_cb c2 x v )"
|  "subst_cb (C_eq e1 e2) x v = C_eq (subst_ceb e1 x v ) (subst_ceb e2 x v )"
|  "subst_cb (C_not c) x v = C_not (subst_cb c x v )"
                      apply (simp add: eqvt_def subst_cb_graph_aux_def)
                      apply auto 
  using c.strong_exhaust apply metis
  done
nominal_termination (eqvt)  by lexicographic_order

abbreviation 
  subst_cb_abbrev :: "c ==> bv ==> b ==> c" (‹_[_::=_]_cb› [1000,50,50] 500)
  where 
    "c[bv::=b]_cb ≡ subst_cb c bv b" 

instantiation c :: has_subst_b
begin
definition "subst_b = subst_cb"

instance proof
  fix j::atom and i::bv and  x::b and t::c
  show  "j ♯ subst_b t i x = (atom i ♯ t ∧ j ♯ t ∨ j ♯ x ∧ (j ♯ t ∨ j = atom i))"
    by (induct t rule: c.induct, unfold subst_cb.simps subst_b_c_def c.fresh,
        (metis has_subst_b_class.fresh_subst_if subst_b_ce_def c.fresh)+
        )

  fix a::bv and tm::c and x::b
  show "atom a ♯ tm ==> subst_b tm a x = tm"
    by(induct tm rule: c.induct, unfold subst_cb.simps subst_b_c_def c.fresh,
        (metis has_subst_b_class.forget_subst subst_b_ce_def)+)

  fix a::bv and tm::c
  show "subst_b tm a (B_var a) = tm" using subst_bb.simps  subst_b_c_def 
    by(induct tm rule: c.induct, unfold subst_cb.simps subst_b_c_def c.fresh,
        (metis has_subst_b_class.subst_id subst_b_ce_def)+)

  fix p::perm and x1::bv and v::b and t1::c
  show "p ∙ subst_b t1 x1 v = subst_b (p ∙ t1) (p ∙ x1) (p ∙ v)" 
    apply(induct tm rule: c.induct,unfold subst_cb.simps subst_b_c_def c.fresh)
    by( auto simp add: fresh_at_base subst_bb.simps subst_b_b_def )

  fix  bv::bv and c::c and z::bv
  show "atom bv ♯ c ==> ((bv ↔ z) ∙ c) = c[z::=B_var bv]_b"
    apply (induct c rule: c.induct,  (auto simp add: fresh_at_base  subst_cb.simps subst_b_c_def permute_pure pure_supp )+)
    using  flip_fresh_fresh flip_l_eq permute_flip_cancel2 has_subst_b_class.flip_subst subst_b_ce_def apply metis
    using  flip_fresh_fresh flip_l_eq permute_flip_cancel2 has_subst_b_class.flip_subst subst_b_ce_def 
    apply (metis opp.perm_simps(2) opp.strong_exhaust)+
    done

  fix bv::bv and c::c and z::bv and v::b
  show "atom bv ♯ c ==> ((bv ↔ z) ∙ c)[bv::=v]_b = c[z::=v]_b"
    apply (induct c rule: c.induct,  (auto simp add: fresh_at_base  subst_cb.simps subst_b_c_def permute_pure pure_supp )+)
    using flip_fresh_fresh flip_l_eq permute_flip_cancel2 has_subst_b_class.flip_subst subst_b_ce_def 
    using flip_subst_subst apply fastforce
    using  flip_fresh_fresh flip_l_eq permute_flip_cancel2 has_subst_b_class.flip_subst subst_b_ce_def 
      opp.perm_simps(2) opp.strong_exhaust 
  proof -
    fix x1a :: ce and x2 :: ce
    assume a1: "atom bv ♯ x2"
    then have "((bv ↔ z) ∙ x2)[bv::=v]_b = x2[z::=v]_b"
      by (metis flip_subst_subst) (* 0.0 ms *)
    then show "x2[z::=B_var bv]_b[bv::=v]_ceb = x2[z::=v]_ceb"
      using a1 by (simp add: subst_b_ce_def) (* 0.0 ms *)
  qed

qed
end

section ‹Types›

nominal_function subst_tb :: "τ ==> bv ==> b ==> τ" where
  "subst_tb ({ z : b2 | c }) bv1 b1 = { z : b2[bv1::=b1]_bb | c[bv1::=b1]_cb }"
proof(goal_cases)
  case 1
  then show ?case using eqvt_def subst_tb_graph_aux_def by force
next
  case (2 x y)
  then show ?case by auto
next
  case (3 P x)
  then show ?case using eqvt_def subst_tb_graph_aux_def τ.strong_exhaust 
    by (metis b_of.cases prod_cases3)
next
  case (4 z' b2' c' bv1' b1' z b2 c bv1 b1)
  show ?case unfolding τ.eq_iff proof
    have *:"[[atom z']]lst. c' = [[atom z]]lst. c" using  τ.eq_iff 4 by auto
    show "[[atom z']]lst. c'[bv1'::=b1']_cb = [[atom z]]lst. c[bv1::=b1]_cb" 
    proof(subst Abs1_eq_iff_all(3),rule,rule,rule)
      fix ca::x
      assume "atom ca ♯ z" and 1:"atom ca ♯ (z', z, c'[bv1'::=b1']_cb, c[bv1::=b1]_cb)" 
      hence 2:"atom ca ♯ (c',c)" using fresh_subst_if subst_b_c_def fresh_Pair fresh_prod4 fresh_at_base subst_b_fresh_x by metis
      hence "(z' ↔ ca) ∙ c' = (z ↔ ca) ∙ c"  using 1 2 * Abs1_eq_iff_all(3) by auto
      hence "((z' ↔ ca) ∙ c')[bv1'::=b1']_cb = ((z ↔ ca) ∙ c)[bv1'::=b1']_cb" by auto      
      hence "(z' ↔ ca) ∙ c'[(z' ↔ ca) ∙ bv1'::=(z' ↔ ca) ∙ b1']_cb = (z ↔ ca) ∙ c[(z ↔ ca) ∙ bv1'::=(z ↔ ca) ∙ b1']_cb" by auto  
      thus "(z' ↔ ca) ∙ c'[bv1'::=b1']_cb = (z ↔ ca) ∙ c[bv1::=b1]_cb" using  4  flip_x_b_cancel by simp
    qed
    show "b2'[bv1'::=b1']_bb = b2[bv1::=b1]_bb" using 4 by simp
  qed
qed

nominal_termination (eqvt) by lexicographic_order

abbreviation 
  subst_tb_abbrev :: "τ ==> bv ==> b ==> τ" (‹_[_::=_]_\τ_b› [1000,50,50] 1000)
  where 
    "t[bv::=b']_\<tau>_b ≡ subst_tb t bv b' " 

instantiation τ :: has_subst_b
begin
definition "subst_b = subst_tb"

instance proof
  fix j::atom and i::bv and  x::b and t::τ
  show  "j ♯ subst_b t i x = (atom i ♯ t ∧ j ♯ t ∨ j ♯ x ∧ (j ♯ t ∨ j = atom i))"
  proof (nominal_induct t avoiding: i x j rule: τ.strong_induct)
    case (T_refined_type z b c)
    then show ?case
      unfolding subst_b_τ_def  subst_tb.simps τ.fresh
      using fresh_subst_if[of j b i x ] subst_b_b_def subst_b_c_def
      by (metis has_subst_b_class.fresh_subst_if list.distinct(1) list.set_cases not_self_fresh set_ConsD)
  qed

  fix a::bv and tm::τ and x::b
  show "atom a ♯ tm ==> subst_b tm a x = tm"
  proof (nominal_induct tm avoiding: a x rule: τ.strong_induct)
    case (T_refined_type xx bb cc )
    moreover hence "atom a ♯ bb ∧ atom a ♯ cc" using τ.fresh by auto
    ultimately show   ?case  
      unfolding  subst_b_τ_def subst_tb.simps 
      using forget_subst subst_b_b_def subst_b_c_def forget_subst τ.fresh by metis
  qed

  fix a::bv and tm::τ
  show "subst_b tm a (B_var a) = tm" 
  proof (nominal_induct tm rule: τ.strong_induct)
    case (T_refined_type xx bb cc)
    thus  ?case  
      unfolding  subst_b_τ_def subst_tb.simps 
      using subst_id subst_b_b_def subst_b_c_def by metis
  qed

  fix p::perm and x1::bv and v::b and t1::τ
  show "p ∙ subst_b t1 x1 v = subst_b (p ∙ t1) (p ∙ x1) (p ∙ v) " 
    by (induct tm rule: τ.induct, auto simp add: fresh_at_base subst_tb.simps subst_b_τ_def subst_bb.simps subst_b_b_def)

  fix  bv::bv and c::τ and z::bv
  show "atom bv ♯ c ==> ((bv ↔ z) ∙ c) = c[z::=B_var bv]_b"
    apply (induct c rule: τ.induct,  (auto simp add: fresh_at_base  subst_ceb.simps subst_b_ce_def permute_pure pure_supp )+)
    using  flip_fresh_fresh permute_flip_cancel2 has_subst_b_class.flip_subst subst_b_c_def  subst_b_b_def 
    by (simp add: flip_fresh_fresh subst_b_τ_def)

  fix bv::bv and c::τ and z::bv and v::b
  show "atom bv ♯ c ==> ((bv ↔ z) ∙ c)[bv::=v]_b = c[z::=v]_b"
  proof (induct c rule: τ.induct)
    case (T_refined_type x1a x2a x3a)
    hence "atom bv ♯ x2a ∧ atom bv ♯ x3a ∧ atom bv ♯ x1a" using fresh_at_base τ.fresh by simp
    then show ?case 
      unfolding subst_tb.simps subst_b_τ_def τ.perm_simps 
      using fresh_at_base flip_fresh_fresh[of bv x1a z] flip_subst_subst subst_b_b_def  subst_b_c_def T_refined_type 
    proof -
      have "atom z ♯ x1a"
        by (metis b.fresh(7) fresh_at_base(2) x_fresh_b) (* 0.0 ms *)
      then show "{ (bv ↔ z) ∙ x1a : ((bv ↔ z) ∙ x2a)[bv::=v]_bb | ((bv ↔ z) ∙ x3a)[bv::=v]_cb } = { x1a : x2a[z::=v]_bb | x3a[z::=v]_cb }"
        by (metis ‹[atom bv ♯ x1a; atom z ♯ x1a] ==> (bv ↔ z) ∙ x1a = x1a› ‹atom bv ♯ x2a ∧ atom bv ♯ x3a ∧ atom bv ♯ x1a› flip_subst_subst subst_b_b_def subst_b_c_def) (* 78 ms *)
    qed 
  qed

qed
end

lemma subst_bb_commute [simp]:
  "atom j ♯ A ==> (subst_bb (subst_bb A i t ) j u ) = subst_bb A i (subst_bb t j u) "
  by (nominal_induct A avoiding: i j t u rule: b.strong_induct) (auto simp: fresh_at_base)

lemma subst_vb_commute [simp]:
  "atom j ♯ A ==> (subst_vb (subst_vb A i t )) j u = subst_vb A i (subst_bb t j u ) "
  by (nominal_induct A avoiding: i j t u rule: v.strong_induct) (auto simp: fresh_at_base)

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

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

lemma subst_tb_commute [simp]:
  "atom j ♯ A ==> (subst_tb (subst_tb A i t )) j u = subst_tb A i (subst_bb t j u ) "
proof (nominal_induct A avoiding: i j t u rule: τ.strong_induct)
  case (T_refined_type z b c)
  then show ?case using subst_tb.simps subst_bb_commute subst_cb_commute by simp
qed

section ‹Expressions›

nominal_function subst_eb :: "e ==> bv ==> b ==> e" where
  "subst_eb ( (AE_val v')) bv b = ( AE_val (subst_vb v' bv b))"
| "subst_eb ( (AE_app f v') ) bv b = ( (AE_app f (subst_vb v' bv b)) )"                
| "subst_eb ( (AE_appP f b' v') ) bv b = ( (AE_appP f (b'[bv::=b]_bb) (subst_vb v' bv b)))"   
| "subst_eb ( (AE_op opp v1 v2) ) bv b = ( (AE_op opp (subst_vb v1 bv b) (subst_vb v2 bv b)) )"
| "subst_eb ( (AE_fst v')) bv b = AE_fst (subst_vb v' bv b)"
| "subst_eb ( (AE_snd v')) bv b = AE_snd (subst_vb v' bv b)"
| "subst_eb ( (AE_mvar u)) bv b = AE_mvar u"
| "subst_eb ( (AE_len v')) bv b = AE_len (subst_vb v' bv b)"
| "subst_eb ( AE_concat v1 v2) bv b = AE_concat (subst_vb v1 bv b) (subst_vb v2 bv b)"
| "subst_eb ( AE_split v1 v2) bv b = AE_split (subst_vb v1 bv b) (subst_vb v2 bv b)"
                      apply (simp add: eqvt_def subst_eb_graph_aux_def)
                      apply auto
  by (meson e.strong_exhaust)
nominal_termination (eqvt) by lexicographic_order

abbreviation 
  subst_eb_abbrev :: "e ==> bv ==> b ==> e" (‹_[_::=_]_eb› [1000,50,50] 500)
  where 
    "e[bv::=b]_eb ≡ subst_eb e bv b" 

instantiation e :: has_subst_b
begin
definition "subst_b = subst_eb"

instance proof
  fix j::atom and i::bv and  x::b and t::e
  show  "j ♯ subst_b t i x = (atom i ♯ t ∧ j ♯ t ∨ j ♯ x ∧ (j ♯ t ∨ j = atom i))"
  proof (induct t rule: e.induct)
    case (AE_val v)
    then show ?case using subst_eb.simps fresh_def pure_fresh subst_b_e_def e.supp v.supp  
        e.fresh has_subst_b_class.fresh_subst_if subst_b_e_def subst_b_v_def
      by metis
  next
    case (AE_app f v)
    then show ?case using subst_eb.simps fresh_def pure_fresh subst_b_e_def 
        e.supp v.supp  has_subst_b_class.fresh_subst_if subst_b_v_def 
      by (metis (mono_tags, opaque_lifting) e.fresh(2))
  next
    case (AE_appP f b' v)
    then show ?case unfolding subst_eb.simps   subst_b_e_def e.fresh using
        fresh_def pure_fresh subst_b_e_def e.supp v.supp
        e.fresh has_subst_b_class.fresh_subst_if subst_b_b_def subst_vb_def   by (metis subst_b_v_def)
  next
    case (AE_op opp v1 v2)
    then show ?case unfolding subst_eb.simps   subst_b_e_def e.fresh using
        fresh_def pure_fresh subst_b_e_def e.supp v.supp fresh_e_opp_all
        e.fresh has_subst_b_class.fresh_subst_if subst_b_b_def subst_vb_def   by (metis subst_b_v_def)  
  next
    case (AE_concat x1a x2)
    then show ?case using subst_eb.simps fresh_def pure_fresh subst_b_e_def e.supp v.supp  
        has_subst_b_class.fresh_subst_if subst_b_v_def 
      by (metis subst_vb.simps(5))
  next
    case (AE_split x1a x2)
    then show ?case using subst_eb.simps fresh_def pure_fresh subst_b_e_def e.supp v.supp  
        has_subst_b_class.fresh_subst_if subst_b_v_def 
      by (metis subst_vb.simps(5))
  next
    case (AE_fst x)
    then show ?case using subst_eb.simps fresh_def pure_fresh subst_b_e_def e.supp v.supp  has_subst_b_class.fresh_subst_if subst_b_v_def  by metis
  next
    case (AE_snd x)
    then show ?case using subst_eb.simps fresh_def pure_fresh subst_b_e_def e.supp v.supp using  has_subst_b_class.fresh_subst_if subst_b_v_def  by metis
  next
    case (AE_mvar x)
    then show ?case using subst_eb.simps fresh_def pure_fresh subst_b_e_def e.supp v.supp  by auto
  next
    case (AE_len x)
    then show ?case using subst_eb.simps fresh_def pure_fresh subst_b_e_def e.supp v.supp   using  has_subst_b_class.fresh_subst_if subst_b_v_def  by metis
  qed

  fix a::bv and tm::e and x::b
  show "atom a ♯ tm ==> subst_b tm a x = tm"
    apply(induct tm rule: e.induct)
             apply( auto simp add: fresh_at_base subst_eb.simps subst_b_e_def)
    using has_subst_b_class.fresh_subst_if  subst_b_b_def e.fresh 
    using has_subst_b_class.forget_subst subst_b_v_def apply metis+
    done

  fix a::bv and tm::e
  show "subst_b tm a (B_var a) = tm" using subst_bb.simps  subst_b_b_def 
    apply (induct tm rule: e.induct)
             apply(auto simp add: fresh_at_base subst_eb.simps subst_b_e_def)
    using has_subst_b_class.fresh_subst_if  subst_b_b_def e.fresh 
    using has_subst_b_class.subst_id subst_b_v_def apply metis+
    done

  fix p::perm and x1::bv and v::b and t1::e
  show "p ∙ subst_b t1 x1 v = subst_b (p ∙ t1) (p ∙ x1) (p ∙ v)" 
    apply(induct tm rule: e.induct)
             apply( auto simp add: fresh_at_base subst_bb.simps subst_b_b_def )
    using has_subst_b_class.eqvt  subst_b_b_def e.fresh 
    using has_subst_b_class.eqvt 
    by (simp add: subst_b_e_def)+

  fix  bv::bv and c::e and z::bv
  show "atom bv ♯ c ==> ((bv ↔ z) ∙ c) = c[z::=B_var bv]_b"
    apply (induct c rule: e.induct)
             apply(auto simp add: fresh_at_base  subst_eb.simps subst_b_e_def subst_b_v_def  permute_pure pure_supp )
    using  flip_fresh_fresh permute_flip_cancel2 has_subst_b_class.flip_subst subst_b_v_def  subst_b_b_def 
      flip_fresh_fresh subst_b_τ_def apply metis
    apply (metis (full_types) opp.perm_simps  opp.strong_exhaust)
    done

  fix bv::bv and c::e and z::bv and v::b
  show "atom bv ♯ c ==> ((bv ↔ z) ∙ c)[bv::=v]_b = c[z::=v]_b"
    apply (induct c rule: e.induct)
             apply(auto simp add: fresh_at_base  subst_eb.simps subst_b_e_def subst_b_v_def  permute_pure pure_supp )
    using  flip_fresh_fresh permute_flip_cancel2 has_subst_b_class.flip_subst subst_b_v_def  subst_b_b_def 
      flip_fresh_fresh subst_b_τ_def apply simp

    apply (metis (full_types) opp.perm_simps  opp.strong_exhaust)
    done
qed
end

section ‹Statements›

nominal_function (default "case_sum (λx. Inl undefined) (case_sum (λx. Inl undefined) (λx. Inr undefined))")
  subst_sb :: "s ==> bv ==> b ==> s"
  and subst_branchb :: "branch_s ==> bv ==> b ==> branch_s" 
  and subst_branchlb :: "branch_list ==> bv ==> b ==> branch_list"
  where
    "subst_sb (AS_val v') bv b = (AS_val (subst_vb v' bv b))"
  | "subst_sb (AS_let y e s) bv b = (AS_let y (e[bv::=b]_eb) (subst_sb s bv b ))"  
  | "subst_sb (AS_let2 y t s1 s2) bv b = (AS_let2 y (subst_tb t bv b) (subst_sb s1 bv b ) (subst_sb s2 bv b))"  
  | "subst_sb (AS_match v' cs) bv b = AS_match (subst_vb v' bv b) (subst_branchlb cs bv b)"
  | "subst_sb (AS_assign y v') bv b = AS_assign y (subst_vb v' bv b)"
  | "subst_sb (AS_if v' s1 s2) bv b = (AS_if (subst_vb v' bv b) (subst_sb s1 bv b ) (subst_sb s2 bv b ) )"  
  | "subst_sb (AS_var u τ v' s) bv b = AS_var u (subst_tb τ bv b) (subst_vb v' bv b) (subst_sb s bv b )"
  | "subst_sb (AS_while s1 s2) bv b = AS_while (subst_sb s1 bv b ) (subst_sb s2 bv b )"
  | "subst_sb (AS_seq s1 s2) bv b = AS_seq (subst_sb s1 bv b ) (subst_sb s2 bv b )"
  | "subst_sb (AS_assert c s) bv b = AS_assert (subst_cb c bv b ) (subst_sb s bv b )"

| "subst_branchb (AS_branch dc x1 s') bv b = AS_branch dc x1 (subst_sb s' bv b)"

| "subst_branchlb (AS_final sb) bv b = AS_final (subst_branchb sb bv b )"
| "subst_branchlb (AS_cons sb ssb) bv b = AS_cons (subst_branchb sb bv b) (subst_branchlb ssb bv b)"

                      apply (simp add: eqvt_def subst_sb_subst_branchb_subst_branchlb_graph_aux_def )                    
                      apply (auto,metis s_branch_s_branch_list.exhaust s_branch_s_branch_list.exhaust(2) old.sum.exhaust surj_pair)

proof(goal_cases)

  have eqvt_at_proj: "∧ s xa va . eqvt_at subst_sb_subst_branchb_subst_branchlb_sumC (Inl (s, xa, va)) ==>
           eqvt_at (λa. projl (subst_sb_subst_branchb_subst_branchlb_sumC (Inl a))) (s, xa, va)"
    apply(simp only: eqvt_at_def)
    apply(rule)
    apply(subst Projl_permute)
     apply(thin_tac _)+
     apply(simp add: subst_sb_subst_branchb_subst_branchlb_sumC_def)
     apply(simp add: THE_default_def)
     apply(case_tac "Ex1 (subst_sb_subst_branchb_subst_branchlb_graph (Inl (s,xa,va)))")
      apply simp
      apply(auto)[1]
      apply(erule_tac x="x" in allE)
      apply simp
      apply(cases rule: subst_sb_subst_branchb_subst_branchlb_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 y s bv b ya sa c)
    moreover have  "atom y ♯ (bv, b) ∧ atom ya ♯ (bv, b)" using x_fresh_b x_fresh_bv fresh_Pair by simp  
    ultimately show ?case 
      using eqvt_triple eqvt_at_proj by metis
  next
    case (2 y s1 s2 bv b ya s2a c)
    moreover have  "atom y ♯ (bv, b) ∧ atom ya ♯ (bv, b)" using x_fresh_b x_fresh_bv   fresh_Pair by simp
    ultimately show ?case 
      using eqvt_triple eqvt_at_proj by metis
  next
    case (3 u s bv b ua sa c)
    moreover have  "atom u ♯ (bv, b) ∧ atom ua ♯ (bv, b)" using x_fresh_b x_fresh_bv   fresh_Pair by simp
    ultimately show ?case using eqvt_triple eqvt_at_proj by metis
  next
    case (4 x1 s' bv b x1a s'a c)
    moreover have  "atom x1 ♯ (bv, b) ∧ atom x1a ♯ (bv, b)" using x_fresh_b x_fresh_bv   fresh_Pair by simp
    ultimately show ?case using eqvt_triple eqvt_at_proj by metis
  }
qed

nominal_termination (eqvt) by lexicographic_order

abbreviation 
  subst_sb_abbrev :: "s ==> bv ==> b ==> s" (‹_[_::=_]_sb› [1000,50,50] 1000)
  where 
    "b[bv::=b']_sb ≡ subst_sb b bv b'" 

lemma fresh_subst_sb_if [simp]: 
  "(j ♯ (subst_sb A i x )) = ((atom i ♯ A ∧ j ♯ A) ∨ (j ♯ x ∧ (j ♯ A ∨ j = atom i)))" and
  "(j ♯ (subst_branchb B i x )) = ((atom i ♯ B ∧ j ♯ B) ∨ (j ♯ x ∧ (j ♯ B ∨ j = atom i)))"  and
  "(j ♯ (subst_branchlb C i x )) = ((atom i ♯ C ∧ j ♯ C) ∨ (j ♯ x ∧ (j ♯ C ∨ j = atom i)))"  
proof (nominal_induct A and B and C avoiding: i x rule: s_branch_s_branch_list.strong_induct)
  case (AS_branch x1 x2 x3)
  have " (j ♯ subst_branchb (AS_branch x1 x2 x3) i x ) = (j ♯ (AS_branch x1 x2 (subst_sb x3 i x)))" by auto
  also have "... = ((j ♯ x3[i::=x]_sb ∨ j ∈ set [atom x2]) ∧ j ♯ x1)" using s_branch_s_branch_list.fresh by auto
  also have "... = ((atom i ♯ AS_branch x1 x2 x3 ∧ j ♯ AS_branch x1 x2 x3) ∨ j ♯ x ∧ (j ♯ AS_branch x1 x2 x3 ∨ j = atom i))"  
    using subst_branchb.simps(1) s_branch_s_branch_list.fresh(1)  fresh_at_base has_subst_b_class.fresh_subst_if list.distinct list.set_cases set_ConsD subst_b_τ_def 
      v.fresh AS_branch
  proof -
    have f1: "∀cs b. atom (b::bv) ♯ (cs::char list)" using pure_fresh by auto

    then have "j ♯ x ∧ atom i = j ⟶ ((j ♯ x3[i::=x]_sb ∨ j ∈ set [atom x2]) ∧ j ♯ x1) = (atom i ♯ AS_branch x1 x2 x3 ∧ j ♯ AS_branch x1 x2 x3 ∨ j ♯ x ∧ (j ♯ AS_branch x1 x2 x3 ∨ j = atom i))"
      by (metis (full_types) AS_branch.hyps(3))
    then have "j ♯ x ⟶ ((j ♯ x3[i::=x]_sb ∨ j ∈ set [atom x2]) ∧ j ♯ x1) = (atom i ♯ AS_branch x1 x2 x3 ∧ j ♯ AS_branch x1 x2 x3 ∨ j ♯ x ∧ (j ♯ AS_branch x1 x2 x3 ∨ j = atom i))"
      using  AS_branch.hyps s_branch_s_branch_list.fresh by metis
    moreover
    { assume "¬ j ♯ x"
      have ?thesis
        using f1 AS_branch.hyps(2) AS_branch.hyps(3) by force  }
    ultimately show ?thesis
      by satx 
  qed   
  finally show ?case by auto  
next
  case (AS_cons cs css i x)
  show ?case 
    unfolding subst_branchlb.simps s_branch_s_branch_list.fresh 
    using AS_cons by auto
next
  case (AS_val xx)
  then show ?case using  subst_sb.simps(1) s_branch_s_branch_list.fresh has_subst_b_class.fresh_subst_if subst_b_b_def subst_b_v_def by metis
next
  case (AS_let x1 x2 x3)
  then show ?case using subst_sb.simps s_branch_s_branch_list.fresh  fresh_at_base has_subst_b_class.fresh_subst_if list.distinct list.set_cases set_ConsD subst_b_e_def 
    by fastforce
next
  case (AS_let2 x1 x2 x3 x4)
  then show ?case using subst_sb.simps s_branch_s_branch_list.fresh  fresh_at_base has_subst_b_class.fresh_subst_if list.distinct list.set_cases set_ConsD subst_b_τ_def
    by fastforce
next
  case (AS_if x1 x2 x3)
  then show ?case unfolding   subst_sb.simps s_branch_s_branch_list.fresh using
      has_subst_b_class.fresh_subst_if  subst_b_v_def   by metis
next
  case (AS_var u t v s)

  have "(((atom i ♯ s ∧ j ♯ s ∨ j ♯ x ∧ (j ♯ s ∨ j = atom i)) ∨ j ∈ set [atom u]) ∧ j ♯ t[i::=x]_\<tau>_b ∧ j ♯ v[i::=x]_vb) =
          (((atom i ♯ s ∧ j ♯ s ∨ j ♯ x ∧ (j ♯ s ∨ j = atom i)) ∨ j ∈ set [atom u]) ∧
                    ((atom i ♯ t ∧ j ♯ t ∨ j ♯ x ∧ (j ♯ t ∨ j = atom i))) ∧
                    ((atom i ♯ v ∧ j ♯ v ∨ j ♯ x ∧ (j ♯ v ∨ j = atom i))))" 
    using    has_subst_b_class.fresh_subst_if  subst_b_v_def  subst_b_τ_def by metis
  also have "... = (((atom i ♯ s ∨ atom i ∈ set [atom u]) ∧ atom i ♯ t ∧ atom i ♯ v) ∧
               (j ♯ s ∨ j ∈ set [atom u]) ∧ j ♯ t ∧ j ♯ v ∨ j ♯ x ∧ ((j ♯ s ∨ j ∈ set [atom u]) ∧ j ♯ t ∧ j ♯ v ∨ j = atom i))" 
    using u_fresh_b by auto
  finally show ?case using  subst_sb.simps s_branch_s_branch_list.fresh AS_var 
    by simp
next
  case (AS_assign u v )
  then show ?case unfolding   subst_sb.simps s_branch_s_branch_list.fresh using
      has_subst_b_class.fresh_subst_if  subst_b_v_def by force
next
  case (AS_match v cs)
  have " j ♯ (AS_match v cs)[i::=x]_sb = j ♯ (AS_match (subst_vb v i x) (subst_branchlb cs i x ))" using subst_sb.simps by auto
  also have "... = (j ♯ (subst_vb v i x) ∧ j ♯ (subst_branchlb cs i x ))" using s_branch_s_branch_list.fresh by simp
  also have "... = (j ♯ (subst_vb v i x) ∧ ((atom i ♯ cs ∧ j ♯ cs) ∨ j ♯ x ∧ (j ♯ cs ∨ j = atom i)))" using  AS_match[of i x] by auto
  also have "... = (atom i ♯ AS_match v cs ∧ j ♯ AS_match v cs ∨ j ♯ x ∧ (j ♯ AS_match v cs ∨ j = atom i))" 
    by (metis (no_types) s_branch_s_branch_list.fresh has_subst_b_class.fresh_subst_if subst_b_v_def) (* 93 ms *)  
  finally show ?case by auto
next
  case (AS_while x1 x2)
  then show ?case by auto
next
  case (AS_seq x1 x2)
  then show ?case by auto
next
  case (AS_assert x1 x2)
  then show ?case unfolding subst_sb.simps  s_branch_s_branch_list.fresh 
    using  fresh_at_base has_subst_b_class.fresh_subst_if list.distinct list.set_cases set_ConsD subst_b_e_def 
    by (metis subst_b_c_def)   
qed(auto+)

lemma 
  forget_subst_sb[simp]: "atom a ♯ A ==> subst_sb A a x = A" and
  forget_subst_branchb [simp]: "atom a ♯ B ==> subst_branchb B a x = B" and 
  forget_subst_branchlb[simp]: "atom a ♯ C ==> subst_branchlb C a x = C"
proof (nominal_induct A and B and C avoiding: a x rule: s_branch_s_branch_list.strong_induct)
  case (AS_let x1 x2 x3)
  then show ?case using subst_sb.simps s_branch_s_branch_list.fresh subst_b_e_def has_subst_b_class.forget_subst subst_b_v_def by force
next
  case (AS_let2 x1 x2 x3 x4)
  then show ?case using subst_sb.simps s_branch_s_branch_list.fresh subst_b_e_def has_subst_b_class.forget_subst subst_b_τ_def by force
next
  case (AS_var x1 x2 x3 x4)
  then show ?case using subst_sb.simps s_branch_s_branch_list.fresh subst_b_e_def has_subst_b_class.forget_subst subst_b_v_def  using subst_b_τ_def 
  proof -
    have f1: "(atom a ♯ x4 ∨ atom a ∈ set [atom x1]) ∧ atom a ♯ x2 ∧ atom a ♯ x3"
      using AS_var.prems s_branch_s_branch_list.fresh  by simp
    then have "atom a ♯ x4"
      by (metis (no_types) "Nominal-Utils.fresh_star_singleton" AS_var.hyps(1) empty_set fresh_star_def list.simps(15) not_self_fresh) (* 46 ms *)
    then show ?thesis
      using f1 by (metis AS_var.hyps(3) has_subst_b_class.forget_subst subst_b_τ_def subst_b_v_def subst_sb.simps(7)) (* 62 ms *)
  qed
next
  case (AS_branch x1 x2 x3)
  then show ?case using subst_sb.simps s_branch_s_branch_list.fresh subst_b_e_def has_subst_b_class.forget_subst subst_b_v_def by force
next
  case (AS_cons x1 x2 x3 x4)
  then show ?case using subst_sb.simps s_branch_s_branch_list.fresh subst_b_e_def has_subst_b_class.forget_subst subst_b_v_def by force
next
  case (AS_val x)
  then show ?case using subst_sb.simps s_branch_s_branch_list.fresh subst_b_e_def has_subst_b_class.forget_subst subst_b_v_def by force
next
  case (AS_if x1 x2 x3)
  then show ?case using subst_sb.simps s_branch_s_branch_list.fresh subst_b_e_def has_subst_b_class.forget_subst subst_b_v_def by force
next
  case (AS_assign x1 x2)
  then show ?case using subst_sb.simps s_branch_s_branch_list.fresh subst_b_e_def has_subst_b_class.forget_subst subst_b_v_def by force
next
  case (AS_match x1 x2)
  then show ?case using subst_sb.simps s_branch_s_branch_list.fresh subst_b_e_def has_subst_b_class.forget_subst subst_b_v_def by force
next
  case (AS_while x1 x2)
  then show ?case using subst_sb.simps s_branch_s_branch_list.fresh subst_b_e_def has_subst_b_class.forget_subst subst_b_v_def by force
next
  case (AS_seq x1 x2)
  then show ?case using subst_sb.simps s_branch_s_branch_list.fresh subst_b_e_def has_subst_b_class.forget_subst subst_b_v_def by force
next
  case (AS_assert c s)
  then show ?case unfolding  subst_sb.simps using
      s_branch_s_branch_list.fresh subst_b_e_def has_subst_b_class.forget_subst subst_b_v_def  subst_b_c_def subst_cb.simps  by force
qed(auto+)

lemma   subst_sb_id: "subst_sb A a (B_var a) = A" and
  subst_branchb_id [simp]: "subst_branchb B a (B_var a) = B" and
  subst_branchlb_id: "subst_branchlb C a (B_var a) = C"
proof(nominal_induct A and B and C avoiding: a  rule: s_branch_s_branch_list.strong_induct)
  case (AS_branch x1 x2 x3)
  then show ?case  using subst_sb.simps s_branch_s_branch_list.fresh subst_b_τ_def has_subst_b_class.subst_id subst_b_v_def 
    by simp
next
  case (AS_cons x1 x2 )
  then show ?case  using subst_sb.simps s_branch_s_branch_list.fresh subst_b_τ_def has_subst_b_class.subst_id subst_b_v_def by simp
next
  case (AS_val x)
  then show ?case  using subst_sb.simps s_branch_s_branch_list.fresh subst_b_τ_def has_subst_b_class.subst_id subst_b_v_def by metis
next
  case (AS_if x1 x2 x3)
  then show ?case  using subst_sb.simps s_branch_s_branch_list.fresh subst_b_τ_def has_subst_b_class.subst_id subst_b_v_def by metis
next
  case (AS_assign x1 x2)
  then show ?case  using subst_sb.simps s_branch_s_branch_list.fresh subst_b_τ_def has_subst_b_class.subst_id subst_b_v_def by metis
next
  case (AS_match x1 x2)
  then show ?case  using subst_sb.simps s_branch_s_branch_list.fresh subst_b_τ_def has_subst_b_class.subst_id subst_b_v_def by metis
next
  case (AS_while x1 x2)
  then show ?case  using subst_sb.simps s_branch_s_branch_list.fresh subst_b_τ_def has_subst_b_class.subst_id subst_b_v_def by metis
next
  case (AS_seq x1 x2)
  then show ?case  using subst_sb.simps s_branch_s_branch_list.fresh subst_b_τ_def has_subst_b_class.subst_id subst_b_v_def by metis
next
  case (AS_let x1 x2 x3)
  then show ?case using subst_sb.simps s_branch_s_branch_list.fresh subst_b_e_def has_subst_b_class.subst_id by metis
next
  case (AS_let2 x1 x2 x3 x4)
  then show ?case using subst_sb.simps s_branch_s_branch_list.fresh subst_b_τ_def has_subst_b_class.subst_id by metis
next
  case (AS_var x1 x2 x3 x4)
  then show ?case using subst_sb.simps s_branch_s_branch_list.fresh subst_b_τ_def has_subst_b_class.subst_id subst_b_v_def by metis
next
  case (AS_assert c s )
  then show ?case unfolding subst_sb.simps using s_branch_s_branch_list.fresh subst_b_c_def has_subst_b_class.subst_id by metis
qed (auto)

lemma flip_subst_s:
  fixes  bv::bv and s::s and cs::branch_s and z::bv
  shows   "atom bv ♯ s ==> ((bv ↔ z) ∙ s) = s[z::=B_var bv]_sb"  and
    "atom bv ♯ cs ==> ((bv ↔ z) ∙ cs) = subst_branchb cs z (B_var bv) " and
    "atom bv ♯ css ==> ((bv ↔ z) ∙ css) = subst_branchlb css z (B_var bv) "

proof(nominal_induct s and cs and css  rule: s_branch_s_branch_list.strong_induct)
  case (AS_branch x1 x2 x3)
  hence "((bv ↔ z) ∙ x1) = x1"  using pure_fresh fresh_at_base flip_fresh_fresh  by metis
  moreover have "((bv ↔ z) ∙ x2) = x2" using  fresh_at_base flip_fresh_fresh[of bv x2 z] AS_branch  by auto
  ultimately show ?case unfolding  s_branch_s_branch_list.perm_simps subst_branchb.simps using s_branch_s_branch_list.fresh(1) AS_branch by auto
next
  case (AS_cons x1 x2 )
  hence "((bv ↔ z) ∙ x1) = subst_branchb x1 z (B_var bv)"  using pure_fresh fresh_at_base flip_fresh_fresh  s_branch_s_branch_list.fresh(13)  by metis
  moreover have "((bv ↔ z) ∙ x2) = subst_branchlb x2 z (B_var bv)" using  fresh_at_base flip_fresh_fresh[of bv x2 z] AS_cons s_branch_s_branch_list.fresh by metis
  ultimately show ?case unfolding  s_branch_s_branch_list.perm_simps subst_branchb.simps using s_branch_s_branch_list.fresh(1) AS_cons by auto
next
  case (AS_val x)
  then show ?case unfolding  s_branch_s_branch_list.perm_simps subst_branchb.simps using flip_subst subst_b_v_def by simp
next
  case (AS_let x1 x2 x3)
  moreover hence "((bv ↔ z) ∙ x1) = x1" using fresh_at_base flip_fresh_fresh[of bv x1 z]  by auto
  ultimately show ?case 
    unfolding  s_branch_s_branch_list.perm_simps subst_sb.simps 
    using flip_subst subst_b_e_def s_branch_s_branch_list.fresh by auto 
next
  case (AS_let2 x1 x2 x3 x4)
  moreover hence "((bv ↔ z) ∙ x1) = x1" using fresh_at_base flip_fresh_fresh[of bv x1 z]  by auto
  ultimately show ?case 
    unfolding  s_branch_s_branch_list.perm_simps subst_sb.simps 
    using flip_subst s_branch_s_branch_list.fresh(5) subst_b_τ_def by auto
next
  case (AS_if x1 x2 x3) 
  thus ?case 
    unfolding  s_branch_s_branch_list.perm_simps subst_sb.simps 
    using flip_subst subst_b_e_def subst_b_v_def s_branch_s_branch_list.fresh by auto
next
  case (AS_var x1 x2 x3 x4)
  thus ?case 
    unfolding  s_branch_s_branch_list.perm_simps subst_sb.simps 
    using flip_subst subst_b_e_def subst_b_v_def subst_b_τ_def s_branch_s_branch_list.fresh fresh_at_base flip_fresh_fresh[of bv x1 z] by auto
next
  case (AS_assign x1 x2)
  thus ?case 
    unfolding  s_branch_s_branch_list.perm_simps subst_sb.simps 
    using flip_subst subst_b_e_def subst_b_v_def s_branch_s_branch_list.fresh fresh_at_base flip_fresh_fresh[of bv x1 z] by auto
next
  case (AS_match x1 x2)
  thus ?case 
    unfolding  s_branch_s_branch_list.perm_simps subst_sb.simps 
    using flip_subst subst_b_e_def subst_b_v_def s_branch_s_branch_list.fresh by auto
next
  case (AS_while x1 x2)
  thus ?case 
    unfolding  s_branch_s_branch_list.perm_simps subst_sb.simps 
    using flip_subst subst_b_e_def subst_b_v_def s_branch_s_branch_list.fresh by auto
next
  case (AS_seq x1 x2)
  thus ?case 
    unfolding  s_branch_s_branch_list.perm_simps subst_sb.simps 
    using flip_subst subst_b_e_def subst_b_v_def s_branch_s_branch_list.fresh by auto
next
  case (AS_assert x1 x2)
  thus ?case 
    unfolding  s_branch_s_branch_list.perm_simps subst_sb.simps 
    using flip_subst subst_b_c_def subst_b_v_def s_branch_s_branch_list.fresh by simp
qed(auto)

lemma flip_subst_subst_s:
  fixes  bv::bv and s::s and cs::branch_s and z::bv
  shows   "atom bv ♯ s ==> ((bv ↔ z) ∙ s)[bv::=v]_sb = s[z::=v]_sb"    and
    "atom bv ♯ cs ==> subst_branchb ((bv ↔ z) ∙ cs) bv v = subst_branchb cs z v" and
    "atom bv ♯ css ==> subst_branchlb ((bv ↔ z) ∙ css) bv v = subst_branchlb css z v " 
proof(nominal_induct s  and cs and css rule: s_branch_s_branch_list.strong_induct)
  case (AS_branch x1 x2 x3)
  hence "((bv ↔ z) ∙ x1) = x1"  using pure_fresh fresh_at_base flip_fresh_fresh  by metis
  moreover have "((bv ↔ z) ∙ x2) = x2" using  fresh_at_base flip_fresh_fresh[of bv x2 z] AS_branch  by auto
  ultimately show ?case unfolding  s_branch_s_branch_list.perm_simps subst_branchb.simps using s_branch_s_branch_list.fresh(1) AS_branch by auto
next
  case (AS_cons x1 x2 )
  thus ?case 
    unfolding  s_branch_s_branch_list.perm_simps subst_branchlb.simps
    using s_branch_s_branch_list.fresh(1) AS_cons by auto

next
  case (AS_val x)
  then show ?case unfolding  s_branch_s_branch_list.perm_simps subst_branchb.simps using flip_subst subst_b_v_def by simp
next
  case (AS_let x1 x2 x3)
  moreover hence "((bv ↔ z) ∙ x1) = x1" using fresh_at_base flip_fresh_fresh[of bv x1 z]  by auto
  ultimately show ?case 
    unfolding  s_branch_s_branch_list.perm_simps subst_sb.simps 
    using flip_subst_subst subst_b_e_def s_branch_s_branch_list.fresh by force
next
  case (AS_let2 x1 x2 x3 x4)
  moreover hence "((bv ↔ z) ∙ x1) = x1" using fresh_at_base flip_fresh_fresh[of bv x1 z]  by auto
  ultimately show ?case 
    unfolding  s_branch_s_branch_list.perm_simps subst_sb.simps 
    using flip_subst s_branch_s_branch_list.fresh(5) subst_b_τ_def by auto
next
  case (AS_if x1 x2 x3) 
  thus ?case 
    unfolding  s_branch_s_branch_list.perm_simps subst_sb.simps 
    using flip_subst subst_b_e_def subst_b_v_def s_branch_s_branch_list.fresh by auto
next
  case (AS_var x1 x2 x3 x4)
  thus ?case 
    unfolding  s_branch_s_branch_list.perm_simps subst_sb.simps 
    using flip_subst subst_b_e_def subst_b_v_def subst_b_τ_def s_branch_s_branch_list.fresh fresh_at_base flip_fresh_fresh[of bv x1 z] by auto
next
  case (AS_assign x1 x2)
  thus ?case 
    unfolding  s_branch_s_branch_list.perm_simps subst_sb.simps 
    using flip_subst subst_b_e_def subst_b_v_def s_branch_s_branch_list.fresh fresh_at_base flip_fresh_fresh[of bv x1 z] by auto
next
  case (AS_match x1 x2)
  thus ?case 
    unfolding  s_branch_s_branch_list.perm_simps subst_sb.simps 
    using flip_subst subst_b_e_def subst_b_v_def s_branch_s_branch_list.fresh by auto
next
  case (AS_while x1 x2)
  thus ?case 
    unfolding  s_branch_s_branch_list.perm_simps subst_sb.simps 
    using flip_subst subst_b_e_def subst_b_v_def s_branch_s_branch_list.fresh by auto
next
  case (AS_seq x1 x2)
  thus ?case 
    unfolding  s_branch_s_branch_list.perm_simps subst_sb.simps 
    using flip_subst subst_b_e_def subst_b_v_def s_branch_s_branch_list.fresh by auto
next
  case (AS_assert x1 x2)
  thus ?case 
    unfolding  s_branch_s_branch_list.perm_simps subst_sb.simps 
    using flip_subst subst_b_e_def subst_b_c_def s_branch_s_branch_list.fresh by auto
qed(auto)

instantiation s :: has_subst_b
begin
definition "subst_b = (λs bv b. subst_sb s bv b)"

instance proof
  fix j::atom and i::bv and  x::b and t::s
  show  "j ♯ subst_b t i x = ((atom i ♯ t ∧ j ♯ t) ∨ (j ♯ x ∧ (j ♯ t ∨ j = atom i)))" 
    using fresh_subst_sb_if subst_b_s_def by metis

  fix a::bv and tm::s and x::b
  show "atom a ♯ tm ==> subst_b tm a x = tm" using subst_b_s_def forget_subst_sb by metis

  fix a::bv and tm::s
  show "subst_b tm a (B_var a) = tm" using subst_b_s_def  subst_sb_id   by metis

  fix p::perm and x1::bv and v::b and t1::s
  show "p ∙ subst_b t1 x1 v = subst_b (p ∙ t1) (p ∙ x1) (p ∙ v)" using subst_b_s_def subst_sb_subst_branchb_subst_branchlb.eqvt by metis

  fix  bv::bv and c::s and z::bv
  show "atom bv ♯ c ==> ((bv ↔ z) ∙ c) = c[z::=B_var bv]_b"
    using subst_b_s_def flip_subst_s by metis

  fix bv::bv and c::s and z::bv and v::b
  show "atom bv ♯ c ==> ((bv ↔ z) ∙ c)[bv::=v]_b = c[z::=v]_b"
    using flip_subst_subst_s subst_b_s_def by metis
qed
end

section ‹Function Type›

nominal_function subst_ft_b :: "fun_typ ==> bv ==> b ==> fun_typ" where
  "subst_ft_b ( AF_fun_typ z b c t (s::s)) x v = AF_fun_typ z (subst_bb b x v) (subst_cb c x v) t[x::=v]_\<tau>_b s[x::=v]_sb"
     apply(simp add: eqvt_def subst_ft_b_graph_aux_def )
    apply(simp add:fun_typ.strong_exhaust,auto )
  apply(rule_tac y=a and c="(a,b)" in fun_typ.strong_exhaust)
  apply (auto simp: eqvt_at_def fresh_star_def fresh_Pair fresh_at_base)
  done

nominal_termination (eqvt) by lexicographic_order

nominal_function subst_ftq_b :: "fun_typ_q ==> bv ==> b ==> fun_typ_q" where
  "atom bv ♯ (x,v) ==> subst_ftq_b (AF_fun_typ_some bv ft) x v = (AF_fun_typ_some bv (subst_ft_b ft x v))" 
|  "subst_ftq_b (AF_fun_typ_none ft) x v = (AF_fun_typ_none (subst_ft_b ft x v))" 
       apply(simp add: eqvt_def subst_ftq_b_graph_aux_def )
      apply(simp add:fun_typ_q.strong_exhaust,auto )
  apply(rule_tac y=a and c="(aa,b)" in fun_typ_q.strong_exhaust)
  by (auto simp: eqvt_at_def fresh_star_def fresh_Pair fresh_at_base)
nominal_termination (eqvt) by lexicographic_order

instantiation fun_typ :: has_subst_b
begin
definition "subst_b = subst_ft_b"

text ‹Note: Using just simp in the second apply unpacks and gives a single goal
  auto gives 43 non-intuitive goals. These goals are easier to solve
  tedious, however they that it clear if a mistake is made in the definition of the function.
  example, I saw that one of the goals was
  through with metis and the next wasn't.
  turned out the definition of the function itself was wrong›

instance proof
  fix j::atom and i::bv and  x::b and t::fun_typ
  show  "j ♯ subst_b 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(auto simp add: subst_b_fun_typ_def )       
    by(metis fresh_subst_if subst_b_s_def subst_b_τ_def subst_b_b_def subst_b_c_def)+

  fix a::bv and tm::fun_typ and x::b
  show "atom a ♯ tm ==> subst_b tm a x = tm"
    apply (nominal_induct tm avoiding: a x rule: fun_typ.strong_induct)
    apply(simp add: subst_b_fun_typ_def Abs1_eq_iff')
    using subst_b_b_def  subst_b_fun_typ_def subst_b_τ_def subst_b_c_def subst_b_s_def
      forget_subst fresh_at_base list.set_cases neq_Nil_conv set_ConsD
      subst_ft_b.simps  by metis

  fix a::bv and tm::fun_typ
  show "subst_b tm a (B_var a) = tm" 
    apply (nominal_induct tm rule: fun_typ.strong_induct)
    apply(simp add: subst_b_fun_typ_def Abs1_eq_iff',auto)
    using subst_b_b_def  subst_b_fun_typ_def subst_b_τ_def subst_b_c_def subst_b_s_def
      forget_subst fresh_at_base list.set_cases neq_Nil_conv set_ConsD
      subst_ft_b.simps 
    by (metis has_subst_b_class.subst_id)+

  fix p::perm and x1::bv and v::b and t1::fun_typ
  show "p ∙ subst_b t1 x1 v = subst_b (p ∙ t1) (p ∙ x1) (p ∙ v) " 
    apply (nominal_induct t1 avoiding: x1 v rule: fun_typ.strong_induct)
    by(auto simp add: subst_b_fun_typ_def Abs1_eq_iff' fun_typ.perm_simps)

  fix  bv::bv and c::fun_typ and z::bv
  show "atom bv ♯ c ==> ((bv ↔ z) ∙ c) = c[z::=B_var bv]_b"
    apply (nominal_induct c avoiding: z bv rule: fun_typ.strong_induct)
    by(auto simp add: subst_b_fun_typ_def Abs1_eq_iff' fun_typ.perm_simps subst_b_b_def subst_b_c_def  subst_b_τ_def  subst_b_s_def)

  fix bv::bv and c::fun_typ and z::bv and v::b
  show "atom bv ♯ c ==> ((bv ↔ z) ∙ c)[bv::=v]_b = c[z::=v]_b"
    apply (nominal_induct c avoiding:  bv v z rule: fun_typ.strong_induct)
    apply(auto simp add: subst_b_fun_typ_def Abs1_eq_iff' fun_typ.perm_simps subst_b_b_def subst_b_c_def  subst_b_τ_def  subst_b_s_def flip_subst_subst flip_subst)
    using  subst_b_fun_typ_def Abs1_eq_iff' fun_typ.perm_simps subst_b_b_def subst_b_c_def  subst_b_τ_def  subst_b_s_def flip_subst_subst flip_subst 
    using flip_subst_s(1) flip_subst_subst_s(1) by auto
qed
end

instantiation fun_typ_q :: has_subst_b
begin
definition "subst_b = subst_ftq_b"

instance proof
  fix j::atom and i::bv and  x::b and t::fun_typ_q
  show  "j ♯ subst_b t i x = (atom i ♯ t ∧ j ♯ t ∨ j ♯ x ∧ (j ♯ t ∨ j = atom i))"
    apply (nominal_induct t avoiding: i x j rule: fun_typ_q.strong_induct,auto simp add: subst_b_fun_typ_q_def subst_ftq_b.simps)
    using  fresh_subst_if subst_b_fun_typ_q_def subst_b_s_def subst_b_τ_def subst_b_b_def subst_b_c_def subst_b_fun_typ_def apply metis+
    done

  fix a::bv and t::fun_typ_q and x::b
  show "atom a ♯ t ==> subst_b t a x = t"
    apply (nominal_induct t avoiding: a x  rule: fun_typ_q.strong_induct)
     apply(auto simp add: subst_b_fun_typ_q_def subst_ftq_b.simps Abs1_eq_iff') 
    using  forget_subst subst_b_fun_typ_q_def subst_b_s_def subst_b_τ_def subst_b_b_def subst_b_c_def subst_b_fun_typ_def eqvt by metis+

  fix p::perm and x1::bv and v::b and t::fun_typ_q
  show "p ∙ subst_b t x1 v = subst_b (p ∙ t) (p ∙ x1) (p ∙ v) " 
    apply (nominal_induct t avoiding: x1 v  rule: fun_typ_q.strong_induct)
    by(auto simp add: subst_b_fun_typ_q_def subst_ftq_b.simps Abs1_eq_iff') 

  fix a::bv and tm::fun_typ_q
  show "subst_b tm a (B_var a) = tm" 
    apply (nominal_induct tm avoiding: a rule: fun_typ_q.strong_induct)
     apply(auto simp add: subst_b_fun_typ_q_def subst_ftq_b.simps Abs1_eq_iff')
    using subst_id subst_b_b_def  subst_b_fun_typ_def subst_b_τ_def subst_b_c_def subst_b_s_def
      forget_subst fresh_at_base list.set_cases neq_Nil_conv set_ConsD
      subst_ft_b.simps by metis+

  fix  bv::bv and c::fun_typ_q and z::bv
  show "atom bv ♯ c ==> ((bv ↔ z) ∙ c) = c[z::=B_var bv]_b"
    apply (nominal_induct c avoiding: z bv  rule: fun_typ_q.strong_induct)
     apply(auto simp add: subst_b_fun_typ_q_def subst_ftq_b.simps Abs1_eq_iff') 
    using  forget_subst subst_b_fun_typ_q_def subst_b_s_def subst_b_τ_def subst_b_b_def subst_b_c_def subst_b_fun_typ_def eqvt by metis+

  fix bv::bv and c::fun_typ_q and z::bv and v::b
  show "atom bv ♯ c ==> ((bv ↔ z) ∙ c)[bv::=v]_b = c[z::=v]_b"
    apply (nominal_induct c avoiding: z v bv  rule: fun_typ_q.strong_induct)
     apply(auto simp add: subst_b_fun_typ_q_def subst_ftq_b.simps Abs1_eq_iff') 
    using  flip_subst flip_subst_subst forget_subst subst_b_fun_typ_q_def subst_b_s_def subst_b_τ_def subst_b_b_def subst_b_c_def subst_b_fun_typ_def eqvt by metis+

qed
end

section ‹Contexts›

subsection ‹Immutable Variables›
nominal_function subst_gb :: "Γ ==> bv ==> b ==> Γ" where
  "subst_gb GNil _ _ = GNil"
| "subst_gb ((y,b',c)#_\<Gamma>Γ) bv b = ((y,b'[bv::=b]_bb,c[bv::=b]_cb)#_\<Gamma> (subst_gb Γ bv b))"
       apply (simp add: eqvt_def subst_gb_graph_aux_def )+
     apply auto
  apply (insert Γ.exhaust neq_GNil_conv, force)
  done
nominal_termination (eqvt) by lexicographic_order

abbreviation 
  subst_gb_abbrev :: "Γ ==> bv ==> b ==> Γ" (‹_[_::=_]_\Γ_b› [1000,50,50] 1000)
  where 
    "g[bv::=b']_\<Gamma>_b ≡ subst_gb g bv b'" 

instantiation Γ :: has_subst_b
begin
definition "subst_b = subst_gb"

instance proof
  fix j::atom and i::bv and  x::b and t::Γ
  show  "j ♯ subst_b t i x = (atom i ♯ t ∧ j ♯ t ∨ j ♯ x ∧ (j ♯ t ∨ j = atom i))"
  proof(induct t rule: Γ_induct)
    case GNil
    then show ?case using fresh_GNil  subst_gb.simps  fresh_def pure_fresh subst_b_Γ_def has_subst_b_class.fresh_subst_if fresh_GNil fresh_GCons by metis
  next
    case (GCons x' b' c' Γ')
    have *: "atom i ♯ x' " using  fresh_at_base by simp

    have "j ♯ subst_b ((x', b', c') #_\<Gamma> Γ') i x = j ♯ ((x', b'[i::=x]_bb, c'[i::=x]_cb) #_\<Gamma> (subst_b Γ' i x))" using subst_gb.simps  subst_b_Γ_def by auto
    also have "... = (j ♯ ((x', b'[i::=x]_bb, c'[i::=x]_cb)) ∧ (j ♯ (subst_b Γ' i x)))" using fresh_GCons by auto
    also have "... = (((j ♯ x') ∧ (j ♯ b'[i::=x]_bb) ∧ (j ♯ c'[i::=x]_cb)) ∧ (j ♯ (subst_b Γ' i x)))"  by auto
    also have "... = (((j ♯ x') ∧ ((atom i ♯ b' ∧ j ♯ b' ∨ j ♯ x ∧ (j ♯ b' ∨ j = atom i))) ∧
                                   ((atom i ♯ c' ∧ j ♯ c' ∨ j ♯ x ∧ (j ♯ c' ∨ j = atom i))) ∧
                                   ((atom i ♯ Γ' ∧ j ♯ Γ' ∨ j ♯ x ∧ (j ♯ Γ' ∨ j = atom i)))))" 
      using fresh_subst_if[of j b' i x] fresh_subst_if[of j c' i x] GCons subst_b_b_def  subst_b_c_def  by simp
    also have "... = ((atom i ♯ (x', b', c') #_\<Gamma> Γ' ∧ j ♯ (x', b', c') #_\<Gamma> Γ') ∨ (j ♯ x ∧ (j ♯ (x', b', c') #_\<Gamma> Γ' ∨ j = atom i)))" using * fresh_GCons fresh_prod3 by metis

    finally show ?case  by auto
  qed

  fix a::bv and tm::Γ and x::b
  show "atom a ♯ tm ==> subst_b tm a x = tm"
  proof (induct tm rule: Γ_induct)
    case GNil
    then show ?case using  subst_gb.simps subst_b_Γ_def by auto
  next
    case (GCons x' b' c' Γ')
    have *:"b'[a::=x]_bb = b' ∧ c'[a::=x]_cb = c'" using GCons fresh_GCons[of "atom a"] fresh_prod3[of "atom a"] has_subst_b_class.forget_subst  subst_b_b_def subst_b_c_def by metis
    have "subst_b ((x', b', c') #_\<Gamma> Γ') a x = ((x', b'[a::=x]_bb, c'[a::=x]_cb) #_\<Gamma> (subst_b Γ' a x))" using  subst_b_Γ_def subst_gb.simps by auto
    also have "... = ((x', b', c') #_\<Gamma> Γ')" using * GCons  fresh_GCons[of "atom a"]  by auto 
    finally show ?case using   has_subst_b_class.forget_subst fresh_GCons fresh_prod3 GCons subst_b_Γ_def has_subst_b_class.forget_subst[of a b' x] fresh_prod3[of "atom a"] by argo
  qed

  fix a::bv and tm::Γ
  show "subst_b tm a (B_var a) = tm"
  proof(induct tm rule: Γ_induct)
    case GNil
    then show ?case using  subst_gb.simps subst_b_Γ_def by auto
  next
    case (GCons x' b' c' Γ')
    then show ?case using    has_subst_b_class.subst_id  subst_b_Γ_def subst_b_b_def subst_b_c_def subst_gb.simps by metis
  qed

  fix p::perm and x1::bv and v::b and t1::Γ
  show "p ∙ subst_b t1 x1 v = subst_b (p ∙ t1) (p ∙ x1) (p ∙ v)" 
  proof (induct tm rule: Γ_induct)
    case GNil
    then show ?case using subst_b_Γ_def subst_gb.simps by simp
  next
    case (GCons x' b' c' Γ')
    then show ?case using subst_b_Γ_def subst_gb.simps has_subst_b_class.eqvt by argo
  qed

  fix  bv::bv and c::Γ and z::bv
  show "atom bv ♯ c ==> ((bv ↔ z) ∙ c) = c[z::=B_var bv]_b"
  proof (induct c rule: Γ_induct)
    case GNil
    then show ?case using subst_b_Γ_def subst_gb.simps by auto
  next
    case (GCons x b c Γ')   
    have *:"(bv ↔ z) ∙ (x, b, c) = (x, (bv ↔ z) ∙ b, (bv ↔ z) ∙ c)" using flip_bv_x_cancel by auto
    then show ?case 
      unfolding subst_gb.simps subst_b_Γ_def permute_Γ.simps  * 
      using GCons subst_b_Γ_def subst_gb.simps flip_subst subst_b_b_def subst_b_c_def fresh_GCons by auto
  qed

  fix bv::bv and c::Γ and z::bv and v::b
  show "atom bv ♯ c ==> ((bv ↔ z) ∙ c)[bv::=v]_b = c[z::=v]_b"
  proof (induct c rule: Γ_induct)
    case GNil
    then show ?case using subst_b_Γ_def subst_gb.simps by auto
  next
    case (GCons x b c Γ')   
    have *:"(bv ↔ z) ∙ (x, b, c) = (x, (bv ↔ z) ∙ b, (bv ↔ z) ∙ c)" using flip_bv_x_cancel by auto
    then show ?case 
      unfolding subst_gb.simps subst_b_Γ_def permute_Γ.simps  * 
      using GCons subst_b_Γ_def subst_gb.simps flip_subst subst_b_b_def subst_b_c_def fresh_GCons by auto
  qed
qed
end

lemma subst_b_base_for_lit:
  "(base_for_lit l)[bv::=b]_bb = base_for_lit l"
  using base_for_lit.simps l.strong_exhaust 
  by (metis subst_bb.simps(2) subst_bb.simps(3) subst_bb.simps(6) subst_bb.simps(7))

lemma subst_b_lookup:
  assumes "Some (b, c) = lookup Γ x"
  shows " Some (b[bv::=b']_bb, c[bv::=b']_cb) = lookup Γ[bv::=b']_\<Gamma>_b x"
  using assms by(induct Γ rule: Γ_induct, auto)

lemma subst_g_b_x_fresh:
  fixes x::x and b::b and Γ::Γ and bv::bv
  assumes "atom x ♯ Γ"
  shows  "atom x ♯ Γ[bv::=b]_\<Gamma>_b"
  using subst_b_fresh_x subst_b_Γ_def assms by metis

subsection ‹Mutable Variables›

nominal_function subst_db :: "Δ ==> bv ==> b ==> Δ" where
  "subst_db []_\<Delta> _ _ = []_\<Delta>"
| "subst_db ((u,t) #_\<Delta> Δ) bv b = ((u,t[bv::=b]_\<tau>_b) #_\<Delta> (subst_db Δ bv b))"
       apply (simp add: eqvt_def subst_db_graph_aux_def,auto )
  using list.exhaust delete_aux.elims
  using neq_DNil_conv by fastforce
nominal_termination (eqvt) by lexicographic_order

abbreviation 
  subst_db_abbrev :: "Δ ==> bv ==> b ==> Δ" (‹_[_::=_]_\Δ_b› [1000,50,50] 1000)
  where 
    "Δ[bv::=b]_\<Delta>_b ≡ subst_db Δ bv b" 

instantiation Δ :: has_subst_b
begin
definition "subst_b = subst_db"

instance proof
  fix j::atom and i::bv and  x::b and t::Δ
  show  "j ♯ subst_b t i x = (atom i ♯ t ∧ j ♯ t ∨ j ♯ x ∧ (j ♯ t ∨ j = atom i))"
  proof(induct t rule: Δ_induct)
    case DNil
    then show ?case using fresh_DNil  subst_db.simps  fresh_def pure_fresh subst_b_Δ_def has_subst_b_class.fresh_subst_if fresh_DNil fresh_DCons by metis
  next
    case (DCons u t Γ')
    have "j ♯ subst_b ((u, t) #_\<Delta> Γ') i x = j ♯ ((u, t[i::=x]_\<tau>_b) #_\<Delta> (subst_b Γ' i x))" using subst_db.simps  subst_b_Δ_def by auto
    also have "... = (j ♯ ((u, t[i::=x]_\<tau>_b)) ∧ (j ♯ (subst_b Γ' i x)))" using fresh_DCons by auto
    also have "... = (((j ♯ u) ∧ (j ♯ t[i::=x]_\<tau>_b)) ∧ (j ♯ (subst_b Γ' i x)))"  by auto
    also have "... = ((j ♯ u) ∧ ((atom i ♯ t ∧ j ♯ t) ∨ (j ♯ x ∧ (j ♯ t ∨ j = atom i))) ∧ (atom i ♯ Γ' ∧ j ♯ Γ' ∨ j ♯ x ∧ (j ♯ Γ' ∨ j = atom i)))" 
      using has_subst_b_class.fresh_subst_if[of j t i x] subst_b_τ_def DCons  subst_b_Δ_def by auto
    also have "... = (atom i ♯ (u, t) #_\<Delta> Γ' ∧ j ♯ (u, t) #_\<Delta> Γ' ∨ j ♯ x ∧ (j ♯ (u, t) #_\<Delta> Γ' ∨ j = atom i))" 
      using DCons subst_db.simps(2)  has_subst_b_class.fresh_subst_if fresh_DCons subst_b_Δ_def  pure_fresh fresh_at_base by auto
    finally show ?case  by auto
  qed

  fix a::bv and tm::Δ and x::b
  show "atom a ♯ tm ==> subst_b tm a x = tm"
  proof (induct tm rule: Δ_induct)
    case DNil
    then show ?case using  subst_db.simps subst_b_Δ_def by auto
  next
    case (DCons u t Γ')
    have *:"t[a::=x]_\<tau>_b = t" using DCons fresh_DCons[of "atom a"] fresh_prod2[of "atom a"] has_subst_b_class.forget_subst  subst_b_τ_def by metis
    have "subst_b ((u,t) #_\<Delta> Γ') a x = ((u,t[a::=x]_\<tau>_b) #_\<Delta> (subst_b Γ' a x))" using  subst_b_Δ_def subst_db.simps by auto
    also have "... = ((u, t) #_\<Delta> Γ')" using * DCons  fresh_DCons[of "atom a"]  by auto 
    finally show ?case using   
        has_subst_b_class.forget_subst fresh_DCons fresh_prod3 
        DCons subst_b_Δ_def has_subst_b_class.forget_subst[of a t x] fresh_prod3[of "atom a"] by argo
  qed

  fix a::bv and tm::Δ
  show "subst_b tm a (B_var a) = tm"
  proof(induct tm rule: Δ_induct)
    case DNil
    then show ?case using  subst_db.simps subst_b_Δ_def by auto
  next
    case (DCons u t  Γ')
    then show ?case using    has_subst_b_class.subst_id  subst_b_Δ_def subst_b_τ_def subst_db.simps by metis
  qed

  fix p::perm and x1::bv and v::b and t1::Δ
  show "p ∙ subst_b t1 x1 v = subst_b (p ∙ t1) (p ∙ x1) (p ∙ v)" 
  proof (induct tm rule: Δ_induct)
    case DNil
    then show ?case using subst_b_Δ_def subst_db.simps by simp
  next
    case (DCons x' b' Γ')
    then show ?case  by argo
  qed

  fix  bv::bv and c::Δ and z::bv
  show "atom bv ♯ c ==> ((bv ↔ z) ∙ c) = c[z::=B_var bv]_b"
  proof (induct c rule: Δ_induct)
    case DNil
    then show ?case using subst_b_Δ_def subst_db.simps by auto
  next
    case (DCons u t')
    then show ?case 
      unfolding subst_db.simps subst_b_Δ_def permute_Δ.simps  
      using DCons subst_b_Δ_def subst_db.simps flip_subst subst_b_τ_def flip_fresh_fresh fresh_at_base fresh_DCons flip_bv_u_cancel by simp
  qed

  fix bv::bv and c::Δ and z::bv and v::b
  show "atom bv ♯ c ==> ((bv ↔ z) ∙ c)[bv::=v]_b = c[z::=v]_b"
  proof (induct c rule: Δ_induct)
    case DNil
    then show ?case using subst_b_Δ_def subst_db.simps by auto
  next
    case (DCons u t')
    then show ?case 
      unfolding subst_db.simps subst_b_Δ_def permute_Δ.simps  
      using DCons subst_b_Δ_def subst_db.simps flip_subst subst_b_τ_def flip_fresh_fresh fresh_at_base fresh_DCons flip_bv_u_cancel by simp
  qed
qed
end

lemma subst_d_b_member:
  assumes "(u, τ) ∈ setD Δ" 
  shows  "(u, τ[bv::=b]_\<tau>_b) ∈ setD Δ[bv::=b]_\<Delta>_b" 
  using assms  by (induct Δ,auto)

lemmas ms_fresh_all = e.fresh s_branch_s_branch_list.fresh τ.fresh c.fresh ce.fresh v.fresh l.fresh fresh_at_base opp.fresh pure_fresh ms_fresh

lemmas fresh_intros[intro] = fresh_GNil x_not_in_b_set x_not_in_u_atoms x_fresh_b u_not_in_x_atoms bv_not_in_x_atoms u_not_in_b_atoms

lemmas subst_b_simps = subst_tb.simps subst_cb.simps subst_ceb.simps subst_vb.simps subst_bb.simps  subst_eb.simps subst_branchb.simps subst_sb.simps

lemma subst_d_b_x_fresh:
  fixes x::x and b::b and Δ::Δ and bv::bv
  assumes "atom x ♯ Δ"
  shows  "atom x ♯ Δ[bv::=b]_\<Delta>_b"
  using subst_b_fresh_x subst_b_Δ_def assms by metis

lemma subst_b_fresh_x:
  fixes  x::x
  shows "atom x ♯ v ==> atom x ♯ v[bv::=b']_vb" and
    "atom x ♯ ce ==> atom x ♯ ce[bv::=b']_ceb" and
    "atom x ♯ e ==> atom x ♯ e[bv::=b']_eb" and
    "atom x ♯ c ==> atom x ♯ c[bv::=b']_cb" and
    "atom x ♯ t ==> atom x ♯ t[bv::=b']_\<tau>_b" and
    "atom x ♯ d ==> atom x ♯ d[bv::=b']_\<Delta>_b" and
    "atom x ♯ g ==> atom x ♯ g[bv::=b']_\<Gamma>_b" and
    "atom x ♯ s ==> atom x ♯ s[bv::=b']_sb"
  using fresh_subst_if x_fresh_b subst_b_v_def subst_b_ce_def subst_b_e_def subst_b_c_def subst_b_τ_def subst_b_s_def subst_g_b_x_fresh subst_d_b_x_fresh 
  by metis+

lemma subst_b_fresh_u_cls:
  fixes tm::"'a::has_subst_b" and x::u
  shows "atom x ♯ tm = atom x ♯ tm[bv::=b']_b"
  using fresh_subst_if[of "atom x" tm bv b'] using u_fresh_b by auto

lemma subst_g_b_u_fresh:
  fixes x::u and b::b and Γ::Γ and bv::bv
  assumes "atom x ♯ Γ"
  shows  "atom x ♯ Γ[bv::=b]_\<Gamma>_b"
  using subst_b_fresh_u_cls subst_b_Γ_def assms by metis

lemma subst_d_b_u_fresh:
  fixes x::u and b::b and Γ::Δ and bv::bv
  assumes "atom x ♯ Γ"
  shows  "atom x ♯ Γ[bv::=b]_\<Delta>_b"
  using subst_b_fresh_u_cls subst_b_Δ_def assms by metis

lemma subst_b_fresh_u:
  fixes  x::u
  shows "atom x ♯ v ==> atom x ♯ v[bv::=b']_vb" and
    "atom x ♯ ce ==> atom x ♯ ce[bv::=b']_ceb" and
    "atom x ♯ e ==> atom x ♯ e[bv::=b']_eb" and
    "atom x ♯ c ==> atom x ♯ c[bv::=b']_cb" and
    "atom x ♯ t ==> atom x ♯ t[bv::=b']_\<tau>_b" and
    "atom x ♯ d ==> atom x ♯ d[bv::=b']_\<Delta>_b" and
    "atom x ♯ g ==> atom x ♯ g[bv::=b']_\<Gamma>_b" and
    "atom x ♯ s ==> atom x ♯ s[bv::=b']_sb"
  using fresh_subst_if u_fresh_b subst_b_v_def subst_b_ce_def subst_b_e_def subst_b_c_def subst_b_τ_def subst_b_s_def subst_g_b_u_fresh subst_d_b_u_fresh 
  by metis+

lemma subst_db_u_fresh:
  fixes u::u and b::b and D::Δ
  assumes "atom u ♯ D"
  shows  "atom u ♯ D[bv::=b]_\<Delta>_b"
  using assms proof(induct D rule: Δ_induct)
  case DNil
  then show ?case by auto
next
  case (DCons u' t' D')
  then show ?case using subst_db.simps fresh_def fresh_DCons fresh_subst_if subst_b_τ_def 
    by (metis fresh_Pair u_not_in_b_atoms)
qed

lemma flip_bt_subst4:
  fixes t::τ and bv::bv 
  assumes "atom bv ♯ t" 
  shows "t[bv'::=b]_\<tau>_b = ((bv' ↔ bv) ∙ t)[bv::=b]_\<tau>_b" 
  using flip_subst_subst[OF assms,of bv' b] 
  by (simp add: flip_commute subst_b_τ_def)

lemma subst_bt_flip_sym:
  fixes t1::τ and t2::τ
  assumes "atom bv ♯ b" and "atom bv ♯ (bv1, bv2, t1, t2)" and "(bv1 ↔ bv) ∙ t1 = (bv2 ↔ bv) ∙ t2"
  shows " t1[bv1::=b]_\<tau>_b = t2[bv2::=b]_\<tau>_b"
  using assms  flip_bt_subst4[of bv t1 bv1 b ]   flip_bt_subst4 fresh_prod4 fresh_Pair by metis

end