Theory BTVSubst
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" ("_[_::=_]⇩b⇩b" [1000,50,50] 1000)
where
"b[bv::=b']⇩b⇩b ≡ 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]⇩b⇩b" 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]⇩b⇩b ∧ b12 = b12'[bv::=b]⇩b⇩b ∧ 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]⇩b⇩b ∧ 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]⇩b⇩b = ((bv1 ↔ c) ∙ b1)[c ::= b]⇩b⇩b"
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]⇩b⇩b = ((bv1 ↔ c) ∙ x1)[c::=b]⇩b⇩b" using b.perm_simps(4) b.fresh(4) fresh_Pair by metis
moreover have "x2[bv1::=b]⇩b⇩b = ((bv1 ↔ c) ∙ x2)[c::=b]⇩b⇩b" 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]⇩b⇩b = ((bv1 ↔ c) ∙ x2)[c::=b]⇩b⇩b" 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]⇩b⇩b = b2[bv2::=b]⇩b⇩b"
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" ("_[_::=_]⇩v⇩b" [1000,50,50] 500)
where
"e[bv::=b]⇩v⇩b ≡ 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" ("_[_::=_]⇩c⇩e⇩b" [1000,50,50] 500)
where
"ce[bv::=b]⇩c⇩e⇩b ≡ 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]⇩c⇩e⇩b ∧ j ♯ v2[i::=x]⇩c⇩e⇩b) = ((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" ("_[_::=_]⇩c⇩b" [1000,50,50] 500)
where
"c[bv::=b]⇩c⇩b ≡ 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)
then show "x2[z::=B_var bv]⇩b[bv::=v]⇩c⇩e⇩b = x2[z::=v]⇩c⇩e⇩b"
using a1 by (simp add: subst_b_ce_def)
qed
qed
end
section ‹Types›
nominal_function subst_tb :: "τ ⇒ bv ⇒ b ⇒ τ" where
"subst_tb (⦃ z : b2 | c ⦄) bv1 b1 = ⦃ z : b2[bv1::=b1]⇩b⇩b | c[bv1::=b1]⇩c⇩b ⦄"
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']⇩c⇩b = [[atom z]]lst. c[bv1::=b1]⇩c⇩b"
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']⇩c⇩b, c[bv1::=b1]⇩c⇩b)"
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']⇩c⇩b = ((z ↔ ca) ∙ c)[bv1'::=b1']⇩c⇩b" by auto
hence "(z' ↔ ca) ∙ c'[(z' ↔ ca) ∙ bv1'::=(z' ↔ ca) ∙ b1']⇩c⇩b = (z ↔ ca) ∙ c[(z ↔ ca) ∙ bv1'::=(z ↔ ca) ∙ b1']⇩c⇩b" by auto
thus "(z' ↔ ca) ∙ c'[bv1'::=b1']⇩c⇩b = (z ↔ ca) ∙ c[bv1::=b1]⇩c⇩b" using 4 flip_x_b_cancel by simp
qed
show "b2'[bv1'::=b1']⇩b⇩b = b2[bv1::=b1]⇩b⇩b" 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']⇩τ⇩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)
then show "⦃ (bv ↔ z) ∙ x1a : ((bv ↔ z) ∙ x2a)[bv::=v]⇩b⇩b | ((bv ↔ z) ∙ x3a)[bv::=v]⇩c⇩b ⦄ = ⦃ x1a : x2a[z::=v]⇩b⇩b | x3a[z::=v]⇩c⇩b ⦄"
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)
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]⇩b⇩b) (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" ("_[_::=_]⇩e⇩b" [1000,50,50] 500)
where
"e[bv::=b]⇩e⇩b ≡ 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]⇩e⇩b) (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" ("_[_::=_]⇩s⇩b" [1000,50,50] 1000)
where
"b[bv::=b']⇩s⇩b ≡ 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]⇩s⇩b ∨ 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]⇩s⇩b ∨ 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]⇩s⇩b ∨ 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]⇩τ⇩b ∧ j ♯ v[i::=x]⇩v⇩b) =
(((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]⇩s⇩b = 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)
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)
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))
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]⇩s⇩b" 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]⇩s⇩b = s[z::=v]⇩s⇩b" 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]⇩τ⇩b s[x::=v]⇩s⇩b"
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
whereas auto gives 43 non-intuitive goals. These goals are easier to solve
and tedious, however they that it clear if a mistake is made in the definition of the function.
For example, I saw that one of the goals was
going through with metis and the next wasn't.
It 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)#⇩ΓΓ) bv b = ((y,b'[bv::=b]⇩b⇩b,c[bv::=b]⇩c⇩b)#⇩Γ (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']⇩Γ⇩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') #⇩Γ Γ') i x = j ♯ ((x', b'[i::=x]⇩b⇩b, c'[i::=x]⇩c⇩b) #⇩Γ (subst_b Γ' i x))" using subst_gb.simps subst_b_Γ_def by auto
also have "... = (j ♯ ((x', b'[i::=x]⇩b⇩b, c'[i::=x]⇩c⇩b)) ∧ (j ♯ (subst_b Γ' i x)))" using fresh_GCons by auto
also have "... = (((j ♯ x') ∧ (j ♯ b'[i::=x]⇩b⇩b) ∧ (j ♯ c'[i::=x]⇩c⇩b)) ∧ (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') #⇩Γ Γ' ∧ j ♯ (x', b', c') #⇩Γ Γ') ∨ (j ♯ x ∧ (j ♯ (x', b', c') #⇩Γ Γ' ∨ 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]⇩b⇩b = b' ∧ c'[a::=x]⇩c⇩b = 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') #⇩Γ Γ') a x = ((x', b'[a::=x]⇩b⇩b, c'[a::=x]⇩c⇩b) #⇩Γ (subst_b Γ' a x))" using subst_b_Γ_def subst_gb.simps by auto
also have "... = ((x', b', c') #⇩Γ Γ')" 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]⇩b⇩b = 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']⇩b⇩b, c[bv::=b']⇩c⇩b) = lookup Γ[bv::=b']⇩Γ⇩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]⇩Γ⇩b"
using subst_b_fresh_x subst_b_Γ_def assms by metis
subsection ‹Mutable Variables›
nominal_function subst_db :: "Δ ⇒ bv ⇒ b ⇒ Δ" where
"subst_db []⇩Δ _ _ = []⇩Δ"
| "subst_db ((u,t) #⇩Δ Δ) bv b = ((u,t[bv::=b]⇩τ⇩b) #⇩Δ (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]⇩Δ⇩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) #⇩Δ Γ') i x = j ♯ ((u, t[i::=x]⇩τ⇩b) #⇩Δ (subst_b Γ' i x))" using subst_db.simps subst_b_Δ_def by auto
also have "... = (j ♯ ((u, t[i::=x]⇩τ⇩b)) ∧ (j ♯ (subst_b Γ' i x)))" using fresh_DCons by auto
also have "... = (((j ♯ u) ∧ (j ♯ t[i::=x]⇩τ⇩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) #⇩Δ Γ' ∧ j ♯ (u, t) #⇩Δ Γ' ∨ j ♯ x ∧ (j ♯ (u, t) #⇩Δ Γ' ∨ 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]⇩τ⇩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) #⇩Δ Γ') a x = ((u,t[a::=x]⇩τ⇩b) #⇩Δ (subst_b Γ' a x))" using subst_b_Δ_def subst_db.simps by auto
also have "... = ((u, t) #⇩Δ Γ')" 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]⇩τ⇩b) ∈ setD Δ[bv::=b]⇩Δ⇩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]⇩Δ⇩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']⇩v⇩b" and
"atom x ♯ ce ⟹ atom x ♯ ce[bv::=b']⇩c⇩e⇩b" and
"atom x ♯ e ⟹ atom x ♯ e[bv::=b']⇩e⇩b" and
"atom x ♯ c ⟹ atom x ♯ c[bv::=b']⇩c⇩b" and
"atom x ♯ t ⟹ atom x ♯ t[bv::=b']⇩τ⇩b" and
"atom x ♯ d ⟹ atom x ♯ d[bv::=b']⇩Δ⇩b" and
"atom x ♯ g ⟹ atom x ♯ g[bv::=b']⇩Γ⇩b" and
"atom x ♯ s ⟹ atom x ♯ s[bv::=b']⇩s⇩b"
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]⇩Γ⇩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]⇩Δ⇩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']⇩v⇩b" and
"atom x ♯ ce ⟹ atom x ♯ ce[bv::=b']⇩c⇩e⇩b" and
"atom x ♯ e ⟹ atom x ♯ e[bv::=b']⇩e⇩b" and
"atom x ♯ c ⟹ atom x ♯ c[bv::=b']⇩c⇩b" and
"atom x ♯ t ⟹ atom x ♯ t[bv::=b']⇩τ⇩b" and
"atom x ♯ d ⟹ atom x ♯ d[bv::=b']⇩Δ⇩b" and
"atom x ♯ g ⟹ atom x ♯ g[bv::=b']⇩Γ⇩b" and
"atom x ♯ s ⟹ atom x ♯ s[bv::=b']⇩s⇩b"
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]⇩Δ⇩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]⇩τ⇩b = ((bv' ↔ bv) ∙ t)[bv::=b]⇩τ⇩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]⇩τ⇩b = t2[bv2::=b]⇩τ⇩b"
using assms flip_bt_subst4[of bv t1 bv1 b ] flip_bt_subst4 fresh_prod4 fresh_Pair by metis
end