Quelle  Pattern.thy

section ‹Simply-typed lambda-calculus with let and tuple patterns›

theory Pattern
imports "HOL-Nominal.Nominal"
begin

atom_decl name

nominal_datatype ty =
    Atom nat
  | Arrow ty ty  (infixr ‹→› 200)
  | TupleT ty ty  (infixr ‹⊗› 210)

lemma fresh_type [simp]: "(a::name) ♯ (T::ty)"
  by (induct T rule: ty.induct) (simp_all add: fresh_nat)

lemma supp_type [simp]: "supp (T::ty) = ({} :: name set)"
  by (induct T rule: ty.induct) (simp_all add: ty.supp supp_nat)

lemma perm_type: "(pi::name prm) ∙ (T::ty) = T"
  by (induct T rule: ty.induct) (simp_all add: perm_nat_def)

nominal_datatype trm =
    Var name
  | Tuple trm trm  (‹(1'⟨_,/ _'⟩)›)
  | Abs ty "«name¬trm"
  | App trm trm  (infixl ‹⋅› 200)
  | Let ty trm btrm
and btrm =
    Base trm
  | Bind ty "«name¬btrm"

abbreviation
  Abs_syn :: "name ==> ty ==> trm ==> trm"  (‹(3λ_:_./ _)› [0, 0, 10] 10) 
where
  "λx:T. t ≡ Abs T x t"

datatype pat =
    PVar name ty
  | PTuple pat pat  (‹(1'⟨⟨_,/ _'⟩⟩)›)

(* FIXME: The following should be done automatically by the nominal package *)
overloading pat_perm ≡ "perm :: name prm ==> pat ==> pat" (unchecked)
begin

primrec pat_perm
where
  "pat_perm pi (PVar x ty) = PVar (pi ∙ x) (pi ∙ ty)"
| "pat_perm pi ⟨⟨p, q⟩⟩ = ⟨⟨pat_perm pi p, pat_perm pi q⟩⟩"

end

declare pat_perm.simps [eqvt]

lemma supp_PVar [simp]: "((supp (PVar x T))::name set) = supp x"
  by (simp add: supp_def perm_fresh_fresh)

lemma supp_PTuple [simp]: "((supp ⟨⟨p, q⟩⟩)::name set) = supp p ∪ supp q"
  by (simp add: supp_def Collect_disj_eq del: disj_not1)

instance pat :: pt_name
proof
  fix x :: pat
  show "([]::(name × _) list) ∙ x = x"
    by (induct x) simp_all
  fix pi1 pi2 :: "(name × name) list"
  show "(pi1 @ pi2) ∙ x = pi1 ∙ pi2 ∙ x"
    by (induct x) (simp_all add: pt_name2)
  assume "pi1 ≜ pi2"
  then show "pi1 ∙ x = pi2 ∙ x"
    by (induct x) (simp_all add: pt_name3)
qed

instance pat :: fs_name
proof
  fix x :: pat
  show "finite (supp x::name set)"
    by (induct x) (simp_all add: fin_supp)
qed

(* the following function cannot be defined using nominal_primrec, *)
(* since variable parameters are currently not allowed.            *)
primrec abs_pat :: "pat ==> btrm ==> btrm" (‹(3λ[_]./ _)› [0, 10] 10)
where
  "(λ[PVar x T]. t) = Bind T x t"
| "(λ[⟨⟨p, q⟩⟩]. t) = (λ[p]. λ[q]. t)"

lemma abs_pat_eqvt [eqvt]:
  "(pi :: name prm) ∙ (λ[p]. t) = (λ[pi ∙ p]. (pi ∙ t))"
  by (induct p arbitrary: t) simp_all

lemma abs_pat_fresh [simp]:
  "(x::name) ♯ (λ[p]. t) = (x ∈ supp p ∨ x ♯ t)"
  by (induct p arbitrary: t) (simp_all add: abs_fresh supp_atm)

lemma abs_pat_alpha:
  assumes fresh: "((pi::name prm) ∙ supp p::name set) ♯* t"
  and pi: "set pi ⊆ supp p × pi ∙ supp p"
  shows "(λ[p]. t) = (λ[pi ∙ p]. pi ∙ t)"
proof -
  note pt_name_inst at_name_inst pi
  moreover have "(supp p::name set) ♯* (λ[p]. t)"
    by (simp add: fresh_star_def)
  moreover from fresh
  have "(pi ∙ supp p::name set) ♯* (λ[p]. t)"
    by (simp add: fresh_star_def)
  ultimately have "pi ∙ (λ[p]. t) = (λ[p]. t)"
    by (rule pt_freshs_freshs)
  then show ?thesis by (simp add: eqvts)
qed

primrec pat_vars :: "pat ==> name list"
where
  "pat_vars (PVar x T) = [x]"
| "pat_vars ⟨⟨p, q⟩⟩ = pat_vars q @ pat_vars p"

lemma pat_vars_eqvt [eqvt]:
  "(pi :: name prm) ∙ (pat_vars p) = pat_vars (pi ∙ p)"
  by (induct p rule: pat.induct) (simp_all add: eqvts)

lemma set_pat_vars_supp: "set (pat_vars p) = supp p"
  by (induct p) (auto simp add: supp_atm)

lemma distinct_eqvt [eqvt]:
  "(pi :: name prm) ∙ (distinct (xs::name list)) = distinct (pi ∙ xs)"
  by (induct xs) (simp_all add: eqvts)

primrec pat_type :: "pat ==> ty"
where
  "pat_type (PVar x T) = T"
| "pat_type ⟨⟨p, q⟩⟩ = pat_type p ⊗ pat_type q"

lemma pat_type_eqvt [eqvt]:
  "(pi :: name prm) ∙ (pat_type p) = pat_type (pi ∙ p)"
  by (induct p) simp_all

lemma pat_type_perm_eq: "pat_type ((pi :: name prm) ∙ p) = pat_type p"
  by (induct p) (simp_all add: perm_type)

type_synonym ctx = "(name × ty) list"

inductive
  ptyping :: "pat ==> ty ==> ctx ==> bool"  (‹⊨ _ : _ ==> _› [60, 60, 60] 60)
where
  PVar: "⊨ PVar x T : T ==> [(x, T)]"
| PTuple: "⊨ p : T ==> Δ🪙1 ==> ⊨ q : U ==> Δ🪙2 ==> ⊨ ⟨⟨p, q⟩⟩ : T ⊗ U ==> Δ🪙2 @ Δ🪙1"

lemma pat_vars_ptyping:
  assumes "⊨ p : T ==> Δ"
  shows "pat_vars p = map fst Δ" using assms
  by induct simp_all

inductive
  valid :: "ctx ==> bool"
where
  Nil [intro!]: "valid []"
| Cons [intro!]: "valid Γ ==> x ♯ Γ ==> valid ((x, T) # Γ)"

inductive_cases validE[elim!]: "valid ((x, T) # Γ)"

lemma fresh_ctxt_set_eq: "((x::name) ♯ (Γ::ctx)) = (x ∉ fst ` set Γ)"
  by (induct Γ) (auto simp add: fresh_list_nil fresh_list_cons fresh_prod fresh_atm)

lemma valid_distinct: "valid Γ = distinct (map fst Γ)"
  by (induct Γ) (auto simp add: fresh_ctxt_set_eq [symmetric])

abbreviation
  "sub_ctx" :: "ctx ==> ctx ==> bool" (‹_ ⊑ _›) 
where
  "Γ🪙1 ⊑ Γ🪙2 ≡ ∀x. x ∈ set Γ🪙1 ⟶ x ∈ set Γ🪙2"

abbreviation
  Let_syn :: "pat ==> trm ==> trm ==> trm"  (‹(LET (_ =/ _)/ IN (_))› 10)
where
  "LET p = t IN u ≡ Let (pat_type p) t (λ[p]. Base u)"

inductive typing :: "ctx ==> trm ==> ty ==> bool" (‹_ ⊨ _ : _› [60, 60, 60] 60)
where
  Var [intro]: "valid Γ ==> (x, T) ∈ set Γ ==> Γ ⊨ Var x : T"
| Tuple [intro]: "Γ ⊨ t : T ==> Γ ⊨ u : U ==> Γ ⊨ ⟨t, u⟩ : T ⊗ U"
| Abs [intro]: "(x, T) # Γ ⊨ t : U ==> Γ ⊨ (λx:T. t) : T → U"
| App [intro]: "Γ ⊨ t : T → U ==> Γ ⊨ u : T ==> Γ ⊨ t ⋅ u : U"
| Let: "((supp p)::name set) ♯* t ==>
    Γ ⊨ t : T ==> ⊨ p : T ==> Δ ==> Δ @ Γ ⊨ u : U ==>
    Γ ⊨ (LET p = t IN u) : U"

equivariance ptyping

equivariance valid

equivariance typing

lemma valid_typing:
  assumes "Γ ⊨ t : T"
  shows "valid Γ" using assms
  by induct auto

lemma pat_var:
  assumes "⊨ p : T ==> Δ"
  shows "(supp p::name set) = supp Δ" using assms
  by induct (auto simp add: supp_list_nil supp_list_cons supp_prod supp_list_append)

lemma valid_app_fresh:
  assumes "valid (Δ @ Γ)" and "(x::name) ∈ supp Δ"
  shows "x ♯ Γ" using assms
  by (induct Δ)
    (auto simp add: supp_list_nil supp_list_cons supp_prod supp_atm fresh_list_append)

lemma pat_freshs:
  assumes "⊨ p : T ==> Δ"
  shows "(supp p::name set) ♯* c = (supp Δ::name set) ♯* c" using assms
  by (auto simp add: fresh_star_def pat_var)

lemma valid_app_mono:
  assumes "valid (Δ @ Γ🪙1)" and "(supp Δ::name set) ♯* Γ🪙2" and "valid Γ🪙2" and "Γ🪙1 ⊑ Γ🪙2"
  shows "valid (Δ @ Γ🪙2)" using assms
  by (induct Δ)
    (auto simp add: supp_list_cons fresh_star_Un_elim supp_prod
       fresh_list_append supp_atm fresh_star_insert_elim fresh_star_empty_elim)

nominal_inductive2 typing
avoids
  Abs: "{x}"
| Let: "(supp p)::name set"
  by (auto simp add: fresh_star_def abs_fresh fin_supp pat_var
    dest!: valid_typing valid_app_fresh)

lemma better_T_Let [intro]:
  assumes t: "Γ ⊨ t : T" and p: "⊨ p : T ==> Δ" and u: "Δ @ Γ ⊨ u : U"
  shows "Γ ⊨ (LET p = t IN u) : U"
proof -
  obtain pi::"name prm" where pi: "(pi ∙ (supp p::name set)) ♯* (t, Base u, Γ)"
    and pi': "set pi ⊆ supp p × (pi ∙ supp p)"
    by (rule at_set_avoiding [OF at_name_inst fin_supp fin_supp])
  from p u have p_fresh: "(supp p::name set) ♯* Γ"
    by (auto simp add: fresh_star_def pat_var dest!: valid_typing valid_app_fresh)
  from pi have p_fresh': "(pi ∙ (supp p::name set)) ♯* Γ"
    by (simp add: fresh_star_prod_elim)
  from pi have p_fresh'': "(pi ∙ (supp p::name set)) ♯* Base u"
    by (simp add: fresh_star_prod_elim)
  from pi have "(supp (pi ∙ p)::name set) ♯* t"
    by (simp add: fresh_star_prod_elim eqvts)
  moreover note t
  moreover from p have "pi ∙ (⊨ p : T ==> Δ)" by (rule perm_boolI)
  then have "⊨ (pi ∙ p) : T ==> (pi ∙ Δ)" by (simp add: eqvts perm_type)
  moreover from u have "pi ∙ (Δ @ Γ ⊨ u : U)" by (rule perm_boolI)
  with pt_freshs_freshs [OF pt_name_inst at_name_inst pi' p_fresh p_fresh']
  have "(pi ∙ Δ) @ Γ ⊨ (pi ∙ u) : U" by (simp add: eqvts perm_type)
  ultimately have "Γ ⊨ (LET (pi ∙ p) = t IN (pi ∙ u)) : U"
    by (rule Let)
  then show ?thesis by (simp add: abs_pat_alpha [OF p_fresh'' pi'] pat_type_perm_eq)
qed

lemma weakening: 
  assumes "Γ🪙1 ⊨ t : T" and "valid Γ🪙2" and "Γ🪙1 ⊑ Γ🪙2"
  shows "Γ🪙2 ⊨ t : T" using assms
proof (nominal_induct Γ🪙1 t T avoiding: Γ🪙2 rule: typing.strong_induct)
  case (Abs x T Γ t U)
  then show ?case
    by (simp add: typing.Abs valid.Cons)
next
  case (Let p t Γ T Δ u U)
  then show ?case
    by (smt (verit, ccfv_threshold) Un_iff pat_freshs set_append typing.simps valid_app_mono valid_typing) 
qed auto

inductive
  match :: "pat ==> trm ==> (name × trm) list ==> bool"  (‹⊨ _ ⊳ _ ==> _› [50, 50, 50] 50)
where
  PVar: "⊨ PVar x T ⊳ t ==> [(x, t)]"
| PProd: "⊨ p ⊳ t ==> θ ==> ⊨ q ⊳ u ==> θ' ==> ⊨ ⟨⟨p, q⟩⟩ ⊳ ⟨t, u⟩ ==> θ @ θ'"

fun
  lookup :: "(name × trm) list ==> name ==> trm"   
where
  "lookup [] x = Var x"
| "lookup ((y, e) # θ) x = (if x = y then e else lookup θ x)"

lemma lookup_eqvt[eqvt]:
  fixes pi :: "name prm"
  and   θ :: "(name × trm) list"
  and   X :: "name"
  shows "pi ∙ (lookup θ X) = lookup (pi ∙ θ) (pi ∙ X)"
  by (induct θ) (auto simp add: eqvts)
 
nominal_primrec
  psubst :: "(name × trm) list ==> trm ==> trm"  (‹_(_)› [95,0] 210)
  and psubstb :: "(name × trm) list ==> btrm ==> btrm"  (‹_(_)🪙b› [95,0] 210)
where
  "θ(Var x) = (lookup θ x)"
| "θ(t ⋅ u) = θ(t) ⋅ θ(u)"
| "θ(⟨t, u⟩) = ⟨θ(t), θ(u)⟩"
| "θ(Let T t u) = Let T (θ(t)) (θ(u)🪙b)"
| "x ♯ θ ==> θ(λx:T. t) = (λx:T. θ(t))"
| "θ(Base t)🪙b = Base (θ(t))"
| "x ♯ θ ==> θ(Bind T x t)🪙b = Bind T x (θ(t)🪙b)"
  by (finite_guess | simp add: abs_fresh | fresh_guess)+

lemma lookup_fresh:
  "x = y ⟶ x ∈ set (map fst θ) ==> ∀(y, t)∈set θ. x ♯ t ==> x ♯ lookup θ y"
  by (induct θ) (use fresh_atm in force)+

lemma psubst_fresh:
  assumes "x ∈ set (map fst θ)" and "∀(y, t)∈set θ. x ♯ t"
  shows "x ♯ θ(t)" and "x ♯ θ(t')🪙b" using assms
proof (nominal_induct t and t' avoiding: θ rule: trm_btrm.strong_inducts)
  case (Var name)
  then show ?case
    by (metis lookup_fresh simps(1))
qed (auto simp: abs_fresh)

lemma psubst_eqvt[eqvt]:
  fixes pi :: "name prm" 
  shows "pi ∙ (θ(t)) = (pi ∙ θ)(pi ∙ t)"
  and "pi ∙ (θ(t')🪙b) = (pi ∙ θ)(pi ∙ t')🪙b"
  by (nominal_induct t and t' avoiding: θ rule: trm_btrm.strong_inducts)
    (simp_all add: eqvts fresh_bij)

abbreviation 
  subst :: "trm ==> name ==> trm ==> trm" (‹_[_↝_]› [100,0,0] 100)
where 
  "t[x↝t'] ≡ [(x,t')](t)"

abbreviation 
  substb :: "btrm ==> name ==> trm ==> btrm" (‹_[_↝_]🪙b› [100,0,0] 100)
where 
  "t[x↝t']🪙b ≡ [(x,t')](t)🪙b"

lemma lookup_forget:
  "(supp (map fst θ)::name set) ♯* x ==> lookup θ x = Var x"
  by (induct θ) (auto simp add: split_paired_all fresh_star_def fresh_atm supp_list_cons supp_atm)

lemma supp_fst: "(x::name) ∈ supp (map fst (θ::(name × trm) list)) ==> x ∈ supp θ"
  by (induct θ) (auto simp add: supp_list_nil supp_list_cons supp_prod)

lemma psubst_forget:
  "(supp (map fst θ)::name set) ♯* t ==> θ(t) = t"
  "(supp (map fst θ)::name set) ♯* t' ==> θ(t')🪙b = t'"
proof (nominal_induct t and t' avoiding: θ rule: trm_btrm.strong_inducts)
  case (Var name)
  then show ?case
    by (simp add: fresh_star_set lookup_forget)
next
  case (Abs ty name trm)
  then show ?case
    apply (simp add: fresh_def)
    by (metis abs_fresh(1) fresh_star_set supp_fst trm.fresh(3))
next
  case (Bind ty name btrm)
  then show ?case
    apply (simp add: fresh_def)
    by (metis abs_fresh(1) btrm.fresh(2) fresh_star_set supp_fst)
qed (auto simp: fresh_star_set)

lemma psubst_nil[simp]: "[](t) = t" "[](t')🪙b = t'"
  by (induct t and t' rule: trm_btrm.inducts) (simp_all add: fresh_list_nil)

lemma psubst_cons:
  assumes "(supp (map fst θ)::name set) ♯* u"
  shows "((x, u) # θ)(t) = θ(t[x↝u])" and "((x, u) # θ)(t')🪙b = θ(t'[x↝u]🪙b)🪙b"
  using assms
  by (nominal_induct t and t' avoiding: x u θ rule: trm_btrm.strong_inducts)
    (simp_all add: fresh_list_nil fresh_list_cons psubst_forget)

lemma psubst_append:
  "(supp (map fst (θ🪙1 @ θ🪙2))::name set) ♯* map snd (θ🪙1 @ θ🪙2) ==> (θ🪙1 @ θ🪙2)(t) = θ🪙2(θ🪙1(t))"
proof (induct θ🪙1 arbitrary: t)
  case Nil
  then show ?case
    by (auto simp: psubst_nil)
next
  case (Cons a θ🪙1)
  then show ?case
  proof (cases a)
    case (Pair a b)
    with Cons show ?thesis
      apply (simp add: supp_list_cons fresh_star_set fresh_list_cons)
      by (metis Un_iff fresh_star_set map_append psubst_cons(1) supp_list_append)
  qed
qed

lemma abs_pat_psubst [simp]:
  "(supp p::name set) ♯* θ ==> θ(λ[p]. t)🪙b = (λ[p]. θ(t)🪙b)"
  by (induct p arbitrary: t) (auto simp add: fresh_star_def supp_atm)

lemma valid_insert:
  assumes "valid (Δ @ [(x, T)] @ Γ)"
  shows "valid (Δ @ Γ)" using assms
  by (induct Δ)
    (auto simp add: fresh_list_append fresh_list_cons)

lemma fresh_set: 
  shows "y ♯ xs = (∀x∈set xs. y ♯ x)"
  by (induct xs) (simp_all add: fresh_list_nil fresh_list_cons)

lemma context_unique:
  assumes "valid Γ"
  and "(x, T) ∈ set Γ"
  and "(x, U) ∈ set Γ"
  shows "T = U" using assms
  by induct (auto simp add: fresh_set fresh_prod fresh_atm)

lemma subst_type_aux:
  assumes a: "Δ @ [(x, U)] @ Γ ⊨ t : T"
  and b: "Γ ⊨ u : U"
  shows "Δ @ Γ ⊨ t[x↝u] : T" using a b
proof (nominal_induct Γ'≡"Δ @ [(x, U)] @ Γ" t T avoiding: x u Δ rule: typing.strong_induct)
  case (Var y T x u Δ)
  from ‹valid (Δ @ [(x, U)] @ Γ)›
  have valid: "valid (Δ @ Γ)" by (rule valid_insert)
  show "Δ @ Γ ⊨ Var y[x↝u] : T"
  proof cases
    assume eq: "x = y"
    from Var eq have "T = U" by (auto intro: context_unique)
    with Var eq valid show "Δ @ Γ ⊨ Var y[x↝u] : T" by (auto intro: weakening)
  next
    assume ineq: "x ≠ y"
    from Var ineq have "(y, T) ∈ set (Δ @ Γ)" by simp
    then show "Δ @ Γ ⊨ Var y[x↝u] : T" using ineq valid by auto
  qed
next
  case (Tuple t🪙1 T🪙1 t🪙2 T🪙2)
  from refl ‹Γ ⊨ u : U›
  have "Δ @ Γ ⊨ t🪙1[x↝u] : T🪙1" by (rule Tuple)
  moreover from refl ‹Γ ⊨ u : U›
  have "Δ @ Γ ⊨ t🪙2[x↝u] : T🪙2" by (rule Tuple)
  ultimately have "Δ @ Γ ⊨ ⟨t🪙1[x↝u], t🪙2[x↝u]⟩ : T🪙1 ⊗ T🪙2" ..
  then show ?case by simp
next
  case (Let p t T Δ' s S)
  from refl ‹Γ ⊨ u : U›
  have "Δ @ Γ ⊨ t[x↝u] : T" by (rule Let)
  moreover note ‹⊨ p : T ==> Δ'›
  moreover have "Δ' @ (Δ @ [(x, U)] @ Γ) = (Δ' @ Δ) @ [(x, U)] @ Γ" by simp
  then have "(Δ' @ Δ) @ Γ ⊨ s[x↝u] : S" using ‹Γ ⊨ u : U› by (rule Let)
  then have "Δ' @ Δ @ Γ ⊨ s[x↝u] : S" by simp
  ultimately have "Δ @ Γ ⊨ (LET p = t[x↝u] IN s[x↝u]) : S"
    by (rule better_T_Let)
  moreover from Let have "(supp p::name set) ♯* [(x, u)]"
    by (simp add: fresh_star_def fresh_list_nil fresh_list_cons)
  ultimately show ?case by simp
next
  case (Abs y T t S)
  have "(y, T) # Δ @ [(x, U)] @ Γ = ((y, T) # Δ) @ [(x, U)] @ Γ"
    by simp
  then have "((y, T) # Δ) @ Γ ⊨ t[x↝u] : S" using ‹Γ ⊨ u : U› by (rule Abs)
  then have "(y, T) # Δ @ Γ ⊨ t[x↝u] : S" by simp
  then have "Δ @ Γ ⊨ (λy:T. t[x↝u]) : T → S"
    by (rule typing.Abs)
  moreover from Abs have "y ♯ [(x, u)]"
    by (simp add: fresh_list_nil fresh_list_cons)
  ultimately show ?case by simp
next
  case (App t🪙1 T S t🪙2)
  from refl ‹Γ ⊨ u : U›
  have "Δ @ Γ ⊨ t🪙1[x↝u] : T → S" by (rule App)
  moreover from refl ‹Γ ⊨ u : U›
  have "Δ @ Γ ⊨ t🪙2[x↝u] : T" by (rule App)
  ultimately have "Δ @ Γ ⊨ (t🪙1[x↝u]) ⋅ (t🪙2[x↝u]) : S"
    by (rule typing.App)
  then show ?case by simp
qed

lemmas subst_type = subst_type_aux [of "[]", simplified]

lemma match_supp_fst:
  assumes "⊨ p ⊳ u ==> θ" shows "(supp (map fst θ)::name set) = supp p" using assms
  by induct (simp_all add: supp_list_nil supp_list_cons supp_list_append)

lemma match_supp_snd:
  assumes "⊨ p ⊳ u ==> θ" shows "(supp (map snd θ)::name set) = supp u" using assms
  by induct (simp_all add: supp_list_nil supp_list_cons supp_list_append trm.supp)

lemma match_fresh: "⊨ p ⊳ u ==> θ ==> (supp p::name set) ♯* u ==>
  (supp (map fst θ)::name set) ♯* map snd θ"
  by (simp add: fresh_star_def fresh_def match_supp_fst match_supp_snd)

lemma match_type_aux:
  assumes "⊨ p : U ==> Δ"
  and "Γ🪙2 ⊨ u : U"
  and "Γ🪙1 @ Δ @ Γ🪙2 ⊨ t : T"
  and "⊨ p ⊳ u ==> θ"
  and "(supp p::name set) ♯* u"
  shows "Γ🪙1 @ Γ🪙2 ⊨ θ(t) : T" using assms
proof (induct arbitrary: Γ🪙1 Γ🪙2 t u T θ)
  case (PVar x U)
  from ‹Γ🪙1 @ [(x, U)] @ Γ🪙2 ⊨ t : T› ‹Γ🪙2 ⊨ u : U›
  have "Γ🪙1 @ Γ🪙2 ⊨ t[x↝u] : T" by (rule subst_type_aux)
  moreover from ‹⊨ PVar x U ⊳ u ==> θ› have "θ = [(x, u)]"
    by cases simp_all
  ultimately show ?case by simp
next
  case (PTuple p S Δ🪙1 q U Δ🪙2)
  from ‹⊨ ⟨⟨p, q⟩⟩ ⊳ u ==> θ› obtain u🪙1 u🪙2 θ🪙1 θ🪙2
    where u: "u = ⟨u🪙1, u🪙2⟩" and θ: "θ = θ🪙1 @ θ🪙2"
    and p: "⊨ p ⊳ u🪙1 ==> θ🪙1" and q: "⊨ q ⊳ u🪙2 ==> θ🪙2"
    by cases simp_all
  with PTuple have "Γ🪙2 ⊨ ⟨u🪙1, u🪙2⟩ : S ⊗ U" by simp
  then obtain u🪙1: "Γ🪙2 ⊨ u🪙1 : S" and u🪙2: "Γ🪙2 ⊨ u🪙2 : U"
    by cases (simp_all add: ty.inject trm.inject)
  note u🪙1
  moreover from ‹Γ🪙1 @ (Δ🪙2 @ Δ🪙1) @ Γ🪙2 ⊨ t : T›
  have "(Γ🪙1 @ Δ🪙2) @ Δ🪙1 @ Γ🪙2 ⊨ t : T" by simp
  moreover note p
  moreover from ‹supp ⟨⟨p, q⟩⟩ ♯* u› and u
  have "(supp p::name set) ♯* u🪙1" by (simp add: fresh_star_def)
  ultimately have θ🪙1: "(Γ🪙1 @ Δ🪙2) @ Γ🪙2 ⊨ θ🪙1(t) : T"
    by (rule PTuple)
  note u🪙2
  moreover from θ🪙1
  have "Γ🪙1 @ Δ🪙2 @ Γ🪙2 ⊨ θ🪙1(t) : T" by simp
  moreover note q
  moreover from ‹supp ⟨⟨p, q⟩⟩ ♯* u› and u
  have "(supp q::name set) ♯* u🪙2" by (simp add: fresh_star_def)
  ultimately have "Γ🪙1 @ Γ🪙2 ⊨ θ🪙2(θ🪙1(t)) : T"
    by (rule PTuple)
  moreover from ‹⊨ ⟨⟨p, q⟩⟩ ⊳ u ==> θ› ‹supp ⟨⟨p, q⟩⟩ ♯* u›
  have "(supp (map fst θ)::name set) ♯* map snd θ"
    by (rule match_fresh)
  ultimately show ?case using θ by (simp add: psubst_append)
qed

lemmas match_type = match_type_aux [where Γ🪙1="[]", simplified]

inductive eval :: "trm ==> trm ==> bool" (‹_ ⟼ _› [60,60] 60)
where
  TupleL: "t ⟼ t' ==> ⟨t, u⟩ ⟼ ⟨t', u⟩"
| TupleR: "u ⟼ u' ==> ⟨t, u⟩ ⟼ ⟨t, u'⟩"
| Abs: "t ⟼ t' ==> (λx:T. t) ⟼ (λx:T. t')"
| AppL: "t ⟼ t' ==> t ⋅ u ⟼ t' ⋅ u"
| AppR: "u ⟼ u' ==> t ⋅ u ⟼ t ⋅ u'"
| Beta: "x ♯ u ==> (λx:T. t) ⋅ u ⟼ t[x↝u]"
| Let: "((supp p)::name set) ♯* t ==> distinct (pat_vars p) ==>
    ⊨ p ⊳ t ==> θ ==> (LET p = t IN u) ⟼ θ(u)"

equivariance match

equivariance eval

lemma match_vars:
  assumes "⊨ p ⊳ t ==> θ" and "x ∈ supp p"
  shows "x ∈ set (map fst θ)" using assms
  by induct (auto simp add: supp_atm)

lemma match_fresh_mono:
  assumes "⊨ p ⊳ t ==> θ" and "(x::name) ♯ t"
  shows "∀(y, t)∈set θ. x ♯ t" using assms
  by induct auto

nominal_inductive2 eval
avoids
  Abs: "{x}"
| Beta: "{x}"
| Let: "(supp p)::name set"
proof (simp_all add: fresh_star_def abs_fresh fin_supp)
  show "x ♯ t[x↝u]" if "x ♯ u" for x t u
    by (simp add: ‹x ♯ u› psubst_fresh(1))
next
  show "∀x∈supp p. (x::name) ♯ θ(u)" 
    if "∀x∈supp p. (x::name) ♯ t" and "⊨ p ⊳ t ==> θ"
    for p t θ u
    by (meson that match_fresh_mono match_vars psubst_fresh(1))
qed

lemma typing_case_Abs:
  assumes ty: "Γ ⊨ (λx:T. t) : S"
  and fresh: "x ♯ Γ"
  and R: "∧U. S = T → U ==> (x, T) # Γ ⊨ t : U ==> P"
  shows P using ty
proof cases
  case (Abs x' T' t' U)
  obtain y::name where y: "y ♯ (x, Γ, λx':T'. t')"
    by (rule exists_fresh) (auto intro: fin_supp)
  from ‹(λx:T. t) = (λx':T'. t')› [symmetric]
  have x: "x ♯ (λx':T'. t')" by (simp add: abs_fresh)
  have x': "x' ♯ (λx':T'. t')" by (simp add: abs_fresh)
  from ‹(x', T') # Γ ⊨ t' : U› have x'': "x' ♯ Γ"
    by (auto dest: valid_typing)
  have "(λx:T. t) = (λx':T'. t')" by fact
  also from x x' y have "… = [(x, y)] ∙ [(x', y)] ∙ (λx':T'. t')"
    by (simp only: perm_fresh_fresh fresh_prod)
  also have "… = (λx:T'. [(x, y)] ∙ [(x', y)] ∙ t')"
    by (simp add: swap_simps perm_fresh_fresh)
  finally have "(λx:T. t) = (λx:T'. [(x, y)] ∙ [(x', y)] ∙ t')" .
  then have T: "T = T'" and t: "[(x, y)] ∙ [(x', y)] ∙ t' = t"
    by (simp_all add: trm.inject alpha)
  from Abs T have "S = T → U" by simp
  moreover from ‹(x', T') # Γ ⊨ t' : U›
  have "[(x, y)] ∙ [(x', y)] ∙ ((x', T') # Γ ⊨ t' : U)"
    by (simp add: perm_bool)
  with T t y x'' fresh have "(x, T) # Γ ⊨ t : U"
    by (simp add: eqvts swap_simps perm_fresh_fresh fresh_prod)
  ultimately show ?thesis by (rule R)
qed simp_all

nominal_primrec ty_size :: "ty ==> nat"
where
  "ty_size (Atom n) = 0"
| "ty_size (T → U) = ty_size T + ty_size U + 1"
| "ty_size (T ⊗ U) = ty_size T + ty_size U + 1"
  by (rule TrueI)+

lemma bind_tuple_ineq:
  "ty_size (pat_type p) < ty_size U ==> Bind U x t ≠ (λ[p]. u)"
  by (induct p arbitrary: U x t u) (auto simp add: btrm.inject)

lemma valid_appD: assumes "valid (Γ @ Δ)"
  shows "valid Γ" "valid Δ" using assms
  by (induct Γ'≡"Γ @ Δ" arbitrary: Γ Δ)
    (auto simp add: Cons_eq_append_conv fresh_list_append)

lemma valid_app_freshs: assumes "valid (Γ @ Δ)"
  shows "(supp Γ::name set) ♯* Δ" "(supp Δ::name set) ♯* Γ" using assms
  by (induct Γ'≡"Γ @ Δ" arbitrary: Γ Δ)
    (auto simp add: Cons_eq_append_conv fresh_star_def
     fresh_list_nil fresh_list_cons supp_list_nil supp_list_cons fresh_list_append
     supp_prod fresh_prod supp_atm fresh_atm
     dest: notE [OF iffD1 [OF fresh_def]])

lemma perm_mem_left: "(x::name) ∈ ((pi::name prm) ∙ A) ==> (rev pi ∙ x) ∈ A"
  by (drule perm_boolI [of _ "rev pi"]) (simp add: eqvts perm_pi_simp)

lemma perm_mem_right: "(rev (pi::name prm) ∙ (x::name)) ∈ A ==> x ∈ (pi ∙ A)"
  by (drule perm_boolI [of _ pi]) (simp add: eqvts perm_pi_simp)

lemma perm_cases:
  assumes pi: "set pi ⊆ A × A"
  shows "((pi::name prm) ∙ B) ⊆ A ∪ B"
proof
  fix x assume "x ∈ pi ∙ B"
  then show "x ∈ A ∪ B" using pi
  proof (induct pi arbitrary: x B rule: rev_induct)
    case Nil
    then show ?case
      by simp
  next
    case (snoc y xs)
    then show ?case
      apply simp
      by (metis SigmaE perm_mem_left perm_pi_simp(2) pt_name2 swap_simps(3))
  qed
qed

lemma abs_pat_alpha':
  assumes eq: "(λ[p]. t) = (λ[q]. u)"
  and ty: "pat_type p = pat_type q"
  and pv: "distinct (pat_vars p)"
  and qv: "distinct (pat_vars q)"
  shows "∃pi::name prm. p = pi ∙ q ∧ t = pi ∙ u ∧
    set pi ⊆ (supp p ∪ supp q) × (supp p ∪ supp q)"
  using assms
proof (induct p arbitrary: q t u)
  case (PVar x T)
  note PVar' = this
  show ?case
  proof (cases q)
    case (PVar x' T')
    with ‹(λ[PVar x T]. t) = (λ[q]. u)›
    have "x = x' ∧ t = u ∨ x ≠ x' ∧ t = [(x, x')] ∙ u ∧ x ♯ u"
      by (simp add: btrm.inject alpha)
    then show ?thesis
    proof
      assume "x = x' ∧ t = u"
      with PVar PVar' have "PVar x T = ([]::name prm) ∙ q ∧
        t = ([]::name prm) ∙ u ∧
        set ([]::name prm) ⊆ (supp (PVar x T) ∪ supp q) ×
          (supp (PVar x T) ∪ supp q)" by simp
      then show ?thesis ..
    next
      assume "x ≠ x' ∧ t = [(x, x')] ∙ u ∧ x ♯ u"
      with PVar PVar' have "PVar x T = [(x, x')] ∙ q ∧
        t = [(x, x')] ∙ u ∧
        set [(x, x')] ⊆ (supp (PVar x T) ∪ supp q) ×
          (supp (PVar x T) ∪ supp q)"
        by (simp add: perm_swap swap_simps supp_atm perm_type)
      then show ?thesis ..
    qed
  next
    case (PTuple p🪙1 p🪙2)
    with PVar have "ty_size (pat_type p🪙1) < ty_size T" by simp
    then have "Bind T x t ≠ (λ[p🪙1]. λ[p🪙2]. u)"
      by (rule bind_tuple_ineq)
    moreover from PTuple PVar
    have "Bind T x t = (λ[p🪙1]. λ[p🪙2]. u)" by simp
    ultimately show ?thesis ..
  qed
next
  case (PTuple p🪙1 p🪙2)
  note PTuple' = this
  show ?case
  proof (cases q)
    case (PVar x T)
    with PTuple have "ty_size (pat_type p🪙1) < ty_size T" by auto
    then have "Bind T x u ≠ (λ[p🪙1]. λ[p🪙2]. t)"
      by (rule bind_tuple_ineq)
    moreover from PTuple PVar
    have "Bind T x u = (λ[p🪙1]. λ[p🪙2]. t)" by simp
    ultimately show ?thesis ..
  next
    case (PTuple p🪙1' p🪙2')
    with PTuple' have "(λ[p🪙1]. λ[p🪙2]. t) = (λ[p🪙1']. λ[p🪙2']. u)" by simp
    moreover from PTuple PTuple' have "pat_type p🪙1 = pat_type p🪙1'"
      by (simp add: ty.inject)
    moreover from PTuple' have "distinct (pat_vars p🪙1)" by simp
    moreover from PTuple PTuple' have "distinct (pat_vars p🪙1')" by simp
    ultimately have "∃pi::name prm. p🪙1 = pi ∙ p🪙1' ∧
      (λ[p🪙2]. t) = pi ∙ (λ[p🪙2']. u) ∧
      set pi ⊆ (supp p🪙1 ∪ supp p🪙1') × (supp p🪙1 ∪ supp p🪙1')"
      by (rule PTuple')
    then obtain pi::"name prm" where
      "p🪙1 = pi ∙ p🪙1'" "(λ[p🪙2]. t) = pi ∙ (λ[p🪙2']. u)" and
      pi: "set pi ⊆ (supp p🪙1 ∪ supp p🪙1') × (supp p🪙1 ∪ supp p🪙1')" by auto
    from ‹(λ[p🪙2]. t) = pi ∙ (λ[p🪙2']. u)›
    have "(λ[p🪙2]. t) = (λ[pi ∙ p🪙2']. pi ∙ u)"
      by (simp add: eqvts)
    moreover from PTuple PTuple' have "pat_type p🪙2 = pat_type (pi ∙ p🪙2')"
      by (simp add: ty.inject pat_type_perm_eq)
    moreover from PTuple' have "distinct (pat_vars p🪙2)" by simp
    moreover from PTuple PTuple' have "distinct (pat_vars (pi ∙ p🪙2'))"
      by (simp add: pat_vars_eqvt [symmetric] distinct_eqvt [symmetric])
    ultimately have "∃pi'::name prm. p🪙2 = pi' ∙ pi ∙ p🪙2' ∧
      t = pi' ∙ pi ∙ u ∧
      set pi' ⊆ (supp p🪙2 ∪ supp (pi ∙ p🪙2')) × (supp p🪙2 ∪ supp (pi ∙ p🪙2'))"
      by (rule PTuple')
    then obtain pi'::"name prm" where
      "p🪙2 = pi' ∙ pi ∙ p🪙2'" "t = pi' ∙ pi ∙ u" and
      pi': "set pi' ⊆ (supp p🪙2 ∪ supp (pi ∙ p🪙2')) ×
        (supp p🪙2 ∪ supp (pi ∙ p🪙2'))" by auto
    from PTuple PTuple' have "pi ∙ distinct (pat_vars ⟨⟨p🪙1', p🪙2'⟩⟩)" by simp
    then have "distinct (pat_vars ⟨⟨pi ∙ p🪙1', pi ∙ p🪙2'⟩⟩)" by (simp only: eqvts)
    with ‹p🪙1 = pi ∙ p🪙1'› PTuple'
    have fresh: "(supp p🪙2 ∪ supp (pi ∙ p🪙2') :: name set) ♯* p🪙1"
      by (auto simp add: set_pat_vars_supp fresh_star_def fresh_def eqvts)
    from ‹p🪙1 = pi ∙ p🪙1'› have "pi' ∙ (p🪙1 = pi ∙ p🪙1')" by (rule perm_boolI)
    with pt_freshs_freshs [OF pt_name_inst at_name_inst pi' fresh fresh]
    have "p🪙1 = pi' ∙ pi ∙ p🪙1'" by (simp add: eqvts)
    with ‹p🪙2 = pi' ∙ pi ∙ p🪙2'› have "⟨⟨p🪙1, p🪙2⟩⟩ = (pi' @ pi) ∙ ⟨⟨p🪙1', p🪙2'⟩⟩"
      by (simp add: pt_name2)
    moreover
    have "((supp p🪙2 ∪ (pi ∙ supp p🪙2')) × (supp p🪙2 ∪ (pi ∙ supp p🪙2'))::(name × name) set) ⊆
      (supp p🪙2 ∪ (supp p🪙1 ∪ supp p🪙1' ∪ supp p🪙2')) × (supp p🪙2 ∪ (supp p🪙1 ∪ supp p🪙1' ∪ supp p🪙2'))"
      by (rule subset_refl Sigma_mono Un_mono perm_cases [OF pi])+
    with pi' have "set pi' ⊆ …" by (simp add: supp_eqvt [symmetric])
    with pi have "set (pi' @ pi) ⊆ (supp ⟨⟨p🪙1, p🪙2⟩⟩ ∪ supp ⟨⟨p🪙1', p🪙2'⟩⟩) ×
      (supp ⟨⟨p🪙1, p🪙2⟩⟩ ∪ supp ⟨⟨p🪙1', p🪙2'⟩⟩)"
      by (simp add: Sigma_Un_distrib1 Sigma_Un_distrib2 Un_ac) blast
    moreover note ‹t = pi' ∙ pi ∙ u›
    ultimately have "⟨⟨p🪙1, p🪙2⟩⟩ = (pi' @ pi) ∙ q ∧ t = (pi' @ pi) ∙ u ∧
      set (pi' @ pi) ⊆ (supp ⟨⟨p🪙1, p🪙2⟩⟩ ∪ supp q) ×
        (supp ⟨⟨p🪙1, p🪙2⟩⟩ ∪ supp q)" using PTuple
      by (simp add: pt_name2)
    then show ?thesis ..
  qed
qed

lemma typing_case_Let:
  assumes ty: "Γ ⊨ (LET p = t IN u) : U"
  and fresh: "(supp p::name set) ♯* Γ"
  and distinct: "distinct (pat_vars p)"
  and R: "∧T Δ. Γ ⊨ t : T ==> ⊨ p : T ==> Δ ==> Δ @ Γ ⊨ u : U ==> P"
  shows P using ty
proof cases
  case (Let p' t' T Δ u')
  then have "(supp Δ::name set) ♯* Γ"
    by (auto intro: valid_typing valid_app_freshs)
  with Let have "(supp p'::name set) ♯* Γ"
    by (simp add: pat_var)
  with fresh have fresh': "(supp p ∪ supp p' :: name set) ♯* Γ"
    by (auto simp add: fresh_star_def)
  from Let have "(λ[p]. Base u) = (λ[p']. Base u')"
    by (simp add: trm.inject)
  moreover from Let have "pat_type p = pat_type p'"
    by (simp add: trm.inject)
  moreover note distinct
  moreover from ‹Δ @ Γ ⊨ u' : U› have "valid (Δ @ Γ)"
    by (rule valid_typing)
  then have "valid Δ" by (rule valid_appD)
  with ‹⊨ p' : T ==> Δ› have "distinct (pat_vars p')"
    by (simp add: valid_distinct pat_vars_ptyping)
  ultimately have "∃pi::name prm. p = pi ∙ p' ∧ Base u = pi ∙ Base u' ∧
    set pi ⊆ (supp p ∪ supp p') × (supp p ∪ supp p')"
    by (rule abs_pat_alpha')
  then obtain pi::"name prm" where pi: "p = pi ∙ p'" "u = pi ∙ u'"
    and pi': "set pi ⊆ (supp p ∪ supp p') × (supp p ∪ supp p')"
    by (auto simp add: btrm.inject)
  from Let have "Γ ⊨ t : T" by (simp add: trm.inject)
  moreover from ‹⊨ p' : T ==> Δ› have "⊨ (pi ∙ p') : (pi ∙ T) ==> (pi ∙ Δ)"
    by (simp add: ptyping.eqvt)
  with pi have "⊨ p : T ==> (pi ∙ Δ)" by (simp add: perm_type)
  moreover from Let
  have "(pi ∙ Δ) @ (pi ∙ Γ) ⊨ (pi ∙ u') : (pi ∙ U)"
    by (simp add: append_eqvt [symmetric] typing.eqvt)
  with pi have "(pi ∙ Δ) @ Γ ⊨ u : U"
    by (simp add: perm_type pt_freshs_freshs
      [OF pt_name_inst at_name_inst pi' fresh' fresh'])
  ultimately show ?thesis by (rule R)
qed simp_all

lemma preservation:
  assumes "t ⟼ t'" and "Γ ⊨ t : T"
  shows "Γ ⊨ t' : T" using assms
proof (nominal_induct avoiding: Γ T rule: eval.strong_induct)
  case (TupleL t t' u)
  from ‹Γ ⊨ ⟨t, u⟩ : T› obtain T🪙1 T🪙2
    where "T = T🪙1 ⊗ T🪙2" "Γ ⊨ t : T🪙1" "Γ ⊨ u : T🪙2"
    by cases (simp_all add: trm.inject)
  from ‹Γ ⊨ t : T🪙1› have "Γ ⊨ t' : T🪙1" by (rule TupleL)
  then have "Γ ⊨ ⟨t', u⟩ : T🪙1 ⊗ T🪙2" using ‹Γ ⊨ u : T🪙2›
    by (rule Tuple)
  with ‹T = T🪙1 ⊗ T🪙2› show ?case by simp
next
  case (TupleR u u' t)
  from ‹Γ ⊨ ⟨t, u⟩ : T› obtain T🪙1 T🪙2
    where "T = T🪙1 ⊗ T🪙2" "Γ ⊨ t : T🪙1" "Γ ⊨ u : T🪙2"
    by cases (simp_all add: trm.inject)
  from ‹Γ ⊨ u : T🪙2› have "Γ ⊨ u' : T🪙2" by (rule TupleR)
  with ‹Γ ⊨ t : T🪙1› have "Γ ⊨ ⟨t, u'⟩ : T🪙1 ⊗ T🪙2"
    by (rule Tuple)
  with ‹T = T🪙1 ⊗ T🪙2› show ?case by simp
next
  case (Abs t t' x S)
  from ‹Γ ⊨ (λx:S. t) : T› ‹x ♯ Γ› obtain U where
    T: "T = S → U" and U: "(x, S) # Γ ⊨ t : U"
    by (rule typing_case_Abs)
  from U have "(x, S) # Γ ⊨ t' : U" by (rule Abs)
  then have "Γ ⊨ (λx:S. t') : S → U"
    by (rule typing.Abs)
  with T show ?case by simp
next
  case (Beta x u S t)
  from ‹Γ ⊨ (λx:S. t) ⋅ u : T› ‹x ♯ Γ›
  obtain "(x, S) # Γ ⊨ t : T" and "Γ ⊨ u : S"
    by cases (auto simp add: trm.inject ty.inject elim: typing_case_Abs)
  then show ?case by (rule subst_type)
next
  case (Let p t θ u)
  from ‹Γ ⊨ (LET p = t IN u) : T› ‹supp p ♯* Γ› ‹distinct (pat_vars p)›
  obtain U Δ where "⊨ p : U ==> Δ" "Γ ⊨ t : U" "Δ @ Γ ⊨ u : T"
    by (rule typing_case_Let)
  then show ?case using ‹⊨ p ⊳ t ==> θ› ‹supp p ♯* t›
    by (rule match_type)
next
  case (AppL t t' u)
  from ‹Γ ⊨ t ⋅ u : T› obtain U where
    t: "Γ ⊨ t : U → T" and u: "Γ ⊨ u : U"
    by cases (auto simp add: trm.inject)
  from t have "Γ ⊨ t' : U → T" by (rule AppL)
  then show ?case using u by (rule typing.App)
next
  case (AppR u u' t)
  from ‹Γ ⊨ t ⋅ u : T› obtain U where
    t: "Γ ⊨ t : U → T" and u: "Γ ⊨ u : U"
    by cases (auto simp add: trm.inject)
  from u have "Γ ⊨ u' : U" by (rule AppR)
  with t show ?case by (rule typing.App)
qed

end