Added Pattern.thy to Nominal/Examples.
authorberghofe
Mon Oct 26 14:53:33 2009 +0100 (2009-10-26)
changeset 3318982a40677c1f8
parent 33176 d6936fd7cda8
child 33190 4705b7323a7d
Added Pattern.thy to Nominal/Examples.
src/HOL/IsaMakefile
src/HOL/Nominal/Examples/Nominal_Examples.thy
src/HOL/Nominal/Examples/Pattern.thy
     1.1 --- a/src/HOL/IsaMakefile	Mon Oct 26 09:03:57 2009 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Mon Oct 26 14:53:33 2009 +0100
     1.3 @@ -1054,6 +1054,7 @@
     1.4    Nominal/Examples/Lam_Funs.thy \
     1.5    Nominal/Examples/Lambda_mu.thy \
     1.6    Nominal/Examples/LocalWeakening.thy \
     1.7 +  Nominal/Examples/Pattern.thy \
     1.8    Nominal/Examples/ROOT.ML \
     1.9    Nominal/Examples/SN.thy \
    1.10    Nominal/Examples/SOS.thy \
     2.1 --- a/src/HOL/Nominal/Examples/Nominal_Examples.thy	Mon Oct 26 09:03:57 2009 +0100
     2.2 +++ b/src/HOL/Nominal/Examples/Nominal_Examples.thy	Mon Oct 26 14:53:33 2009 +0100
     2.3 @@ -20,6 +20,7 @@
     2.4    Contexts
     2.5    Standardization
     2.6    W
     2.7 +  Pattern
     2.8  begin
     2.9  
    2.10  end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Nominal/Examples/Pattern.thy	Mon Oct 26 14:53:33 2009 +0100
     3.3 @@ -0,0 +1,865 @@
     3.4 +header {* Simply-typed lambda-calculus with let and tuple patterns *}
     3.5 +
     3.6 +theory Pattern
     3.7 +imports Nominal
     3.8 +begin
     3.9 +
    3.10 +no_syntax
    3.11 +  "_Map" :: "maplets => 'a ~=> 'b"  ("(1[_])")
    3.12 +
    3.13 +atom_decl name
    3.14 +
    3.15 +nominal_datatype ty =
    3.16 +    Atom nat
    3.17 +  | Arrow ty ty  (infixr "\<rightarrow>" 200)
    3.18 +  | TupleT ty ty  (infixr "\<otimes>" 210)
    3.19 +
    3.20 +lemma fresh_type [simp]: "(a::name) \<sharp> (T::ty)"
    3.21 +  by (induct T rule: ty.induct) (simp_all add: fresh_nat)
    3.22 +
    3.23 +lemma supp_type [simp]: "supp (T::ty) = ({} :: name set)"
    3.24 +  by (induct T rule: ty.induct) (simp_all add: ty.supp supp_nat)
    3.25 +
    3.26 +lemma perm_type: "(pi::name prm) \<bullet> (T::ty) = T"
    3.27 +  by (induct T rule: ty.induct) (simp_all add: perm_nat_def)
    3.28 +
    3.29 +nominal_datatype trm =
    3.30 +    Var name
    3.31 +  | Tuple trm trm  ("(1'\<langle>_,/ _'\<rangle>)")
    3.32 +  | Abs ty "\<guillemotleft>name\<guillemotright>trm"
    3.33 +  | App trm trm  (infixl "\<cdot>" 200)
    3.34 +  | Let ty trm btrm
    3.35 +and btrm =
    3.36 +    Base trm
    3.37 +  | Bind ty "\<guillemotleft>name\<guillemotright>btrm"
    3.38 +
    3.39 +abbreviation
    3.40 +  Abs_syn :: "name \<Rightarrow> ty \<Rightarrow> trm \<Rightarrow> trm"  ("(3\<lambda>_:_./ _)" [0, 0, 10] 10) 
    3.41 +where
    3.42 +  "\<lambda>x:T. t \<equiv> Abs T x t"
    3.43 +
    3.44 +datatype pat =
    3.45 +    PVar name ty
    3.46 +  | PTuple pat pat  ("(1'\<langle>\<langle>_,/ _'\<rangle>\<rangle>)")
    3.47 +
    3.48 +(* FIXME: The following should be done automatically by the nominal package *)
    3.49 +overloading pat_perm \<equiv> "perm :: name prm \<Rightarrow> pat \<Rightarrow> pat" (unchecked)
    3.50 +begin
    3.51 +
    3.52 +primrec pat_perm
    3.53 +where
    3.54 +  "pat_perm pi (PVar x ty) = PVar (pi \<bullet> x) (pi \<bullet> ty)"
    3.55 +| "pat_perm pi \<langle>\<langle>p, q\<rangle>\<rangle> = \<langle>\<langle>pat_perm pi p, pat_perm pi q\<rangle>\<rangle>"
    3.56 +
    3.57 +end
    3.58 +
    3.59 +declare pat_perm.simps [eqvt]
    3.60 +
    3.61 +lemma supp_PVar [simp]: "((supp (PVar x T))::name set) = supp x"
    3.62 +  by (simp add: supp_def perm_fresh_fresh)
    3.63 +
    3.64 +lemma supp_PTuple [simp]: "((supp \<langle>\<langle>p, q\<rangle>\<rangle>)::name set) = supp p \<union> supp q"
    3.65 +  by (simp add: supp_def Collect_disj_eq del: disj_not1)
    3.66 +
    3.67 +instance pat :: pt_name
    3.68 +proof intro_classes
    3.69 +  case goal1
    3.70 +  show ?case by (induct x) simp_all
    3.71 +next
    3.72 +  case goal2
    3.73 +  show ?case by (induct x) (simp_all add: pt_name2)
    3.74 +next
    3.75 +  case goal3
    3.76 +  then show ?case by (induct x) (simp_all add: pt_name3)
    3.77 +qed
    3.78 +
    3.79 +instance pat :: fs_name
    3.80 +proof intro_classes
    3.81 +  case goal1
    3.82 +  show ?case by (induct x) (simp_all add: fin_supp)
    3.83 +qed
    3.84 +
    3.85 +(* the following function cannot be defined using nominal_primrec, *)
    3.86 +(* since variable parameters are currently not allowed.            *)
    3.87 +primrec abs_pat :: "pat \<Rightarrow> btrm \<Rightarrow> btrm" ("(3\<lambda>[_]./ _)" [0, 10] 10)
    3.88 +where
    3.89 +  "(\<lambda>[PVar x T]. t) = Bind T x t"
    3.90 +| "(\<lambda>[\<langle>\<langle>p, q\<rangle>\<rangle>]. t) = (\<lambda>[p]. \<lambda>[q]. t)"
    3.91 +
    3.92 +lemma abs_pat_eqvt [eqvt]:
    3.93 +  "(pi :: name prm) \<bullet> (\<lambda>[p]. t) = (\<lambda>[pi \<bullet> p]. (pi \<bullet> t))"
    3.94 +  by (induct p arbitrary: t) simp_all
    3.95 +
    3.96 +lemma abs_pat_fresh [simp]:
    3.97 +  "(x::name) \<sharp> (\<lambda>[p]. t) = (x \<in> supp p \<or> x \<sharp> t)"
    3.98 +  by (induct p arbitrary: t) (simp_all add: abs_fresh supp_atm)
    3.99 +
   3.100 +lemma abs_pat_alpha:
   3.101 +  assumes fresh: "((pi::name prm) \<bullet> supp p::name set) \<sharp>* t"
   3.102 +  and pi: "set pi \<subseteq> supp p \<times> pi \<bullet> supp p"
   3.103 +  shows "(\<lambda>[p]. t) = (\<lambda>[pi \<bullet> p]. pi \<bullet> t)"
   3.104 +proof -
   3.105 +  note pt_name_inst at_name_inst pi
   3.106 +  moreover have "(supp p::name set) \<sharp>* (\<lambda>[p]. t)"
   3.107 +    by (simp add: fresh_star_def)
   3.108 +  moreover from fresh
   3.109 +  have "(pi \<bullet> supp p::name set) \<sharp>* (\<lambda>[p]. t)"
   3.110 +    by (simp add: fresh_star_def)
   3.111 +  ultimately have "pi \<bullet> (\<lambda>[p]. t) = (\<lambda>[p]. t)"
   3.112 +    by (rule pt_freshs_freshs)
   3.113 +  then show ?thesis by (simp add: eqvts)
   3.114 +qed
   3.115 +
   3.116 +primrec pat_vars :: "pat \<Rightarrow> name list"
   3.117 +where
   3.118 +  "pat_vars (PVar x T) = [x]"
   3.119 +| "pat_vars \<langle>\<langle>p, q\<rangle>\<rangle> = pat_vars q @ pat_vars p"
   3.120 +
   3.121 +lemma pat_vars_eqvt [eqvt]:
   3.122 +  "(pi :: name prm) \<bullet> (pat_vars p) = pat_vars (pi \<bullet> p)"
   3.123 +  by (induct p rule: pat.induct) (simp_all add: eqvts)
   3.124 +
   3.125 +lemma set_pat_vars_supp: "set (pat_vars p) = supp p"
   3.126 +  by (induct p) (auto simp add: supp_atm)
   3.127 +
   3.128 +lemma distinct_eqvt [eqvt]:
   3.129 +  "(pi :: name prm) \<bullet> (distinct (xs::name list)) = distinct (pi \<bullet> xs)"
   3.130 +  by (induct xs) (simp_all add: eqvts)
   3.131 +
   3.132 +primrec pat_type :: "pat \<Rightarrow> ty"
   3.133 +where
   3.134 +  "pat_type (PVar x T) = T"
   3.135 +| "pat_type \<langle>\<langle>p, q\<rangle>\<rangle> = pat_type p \<otimes> pat_type q"
   3.136 +
   3.137 +lemma pat_type_eqvt [eqvt]:
   3.138 +  "(pi :: name prm) \<bullet> (pat_type p) = pat_type (pi \<bullet> p)"
   3.139 +  by (induct p) simp_all
   3.140 +
   3.141 +lemma pat_type_perm_eq: "pat_type ((pi :: name prm) \<bullet> p) = pat_type p"
   3.142 +  by (induct p) (simp_all add: perm_type)
   3.143 +
   3.144 +types ctx = "(name \<times> ty) list"
   3.145 +
   3.146 +inductive
   3.147 +  ptyping :: "pat \<Rightarrow> ty \<Rightarrow> ctx \<Rightarrow> bool"  ("\<turnstile> _ : _ \<Rightarrow> _" [60, 60, 60] 60)
   3.148 +where
   3.149 +  PVar: "\<turnstile> PVar x T : T \<Rightarrow> [(x, T)]"
   3.150 +| PTuple: "\<turnstile> p : T \<Rightarrow> \<Delta>\<^isub>1 \<Longrightarrow> \<turnstile> q : U \<Rightarrow> \<Delta>\<^isub>2 \<Longrightarrow> \<turnstile> \<langle>\<langle>p, q\<rangle>\<rangle> : T \<otimes> U \<Rightarrow> \<Delta>\<^isub>2 @ \<Delta>\<^isub>1"
   3.151 +
   3.152 +lemma pat_vars_ptyping:
   3.153 +  assumes "\<turnstile> p : T \<Rightarrow> \<Delta>"
   3.154 +  shows "pat_vars p = map fst \<Delta>" using assms
   3.155 +  by induct simp_all
   3.156 +
   3.157 +inductive
   3.158 +  valid :: "ctx \<Rightarrow> bool"
   3.159 +where
   3.160 +  Nil [intro!]: "valid []"
   3.161 +| Cons [intro!]: "valid \<Gamma> \<Longrightarrow> x \<sharp> \<Gamma> \<Longrightarrow> valid ((x, T) # \<Gamma>)"
   3.162 +
   3.163 +inductive_cases validE[elim!]: "valid ((x, T) # \<Gamma>)"
   3.164 +
   3.165 +lemma fresh_ctxt_set_eq: "((x::name) \<sharp> (\<Gamma>::ctx)) = (x \<notin> fst ` set \<Gamma>)"
   3.166 +  by (induct \<Gamma>) (auto simp add: fresh_list_nil fresh_list_cons fresh_prod fresh_atm)
   3.167 +
   3.168 +lemma valid_distinct: "valid \<Gamma> = distinct (map fst \<Gamma>)"
   3.169 +  by (induct \<Gamma>) (auto simp add: fresh_ctxt_set_eq [symmetric])
   3.170 +
   3.171 +abbreviation
   3.172 +  "sub_ctx" :: "ctx \<Rightarrow> ctx \<Rightarrow> bool" ("_ \<sqsubseteq> _") 
   3.173 +where
   3.174 +  "\<Gamma>\<^isub>1 \<sqsubseteq> \<Gamma>\<^isub>2 \<equiv> \<forall>x. x \<in> set \<Gamma>\<^isub>1 \<longrightarrow> x \<in> set \<Gamma>\<^isub>2"
   3.175 +
   3.176 +abbreviation
   3.177 +  Let_syn :: "pat \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm"  ("(LET (_ =/ _)/ IN (_))" 10)
   3.178 +where
   3.179 +  "LET p = t IN u \<equiv> Let (pat_type p) t (\<lambda>[p]. Base u)"
   3.180 +
   3.181 +inductive typing :: "ctx \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60, 60, 60] 60)
   3.182 +where
   3.183 +  Var [intro]: "valid \<Gamma> \<Longrightarrow> (x, T) \<in> set \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
   3.184 +| Tuple [intro]: "\<Gamma> \<turnstile> t : T \<Longrightarrow> \<Gamma> \<turnstile> u : U \<Longrightarrow> \<Gamma> \<turnstile> \<langle>t, u\<rangle> : T \<otimes> U"
   3.185 +| Abs [intro]: "(x, T) # \<Gamma> \<turnstile> t : U \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda>x:T. t) : T \<rightarrow> U"
   3.186 +| App [intro]: "\<Gamma> \<turnstile> t : T \<rightarrow> U \<Longrightarrow> \<Gamma> \<turnstile> u : T \<Longrightarrow> \<Gamma> \<turnstile> t \<cdot> u : U"
   3.187 +| Let: "((supp p)::name set) \<sharp>* t \<Longrightarrow>
   3.188 +    \<Gamma> \<turnstile> t : T \<Longrightarrow> \<turnstile> p : T \<Rightarrow> \<Delta> \<Longrightarrow> \<Delta> @ \<Gamma> \<turnstile> u : U \<Longrightarrow>
   3.189 +    \<Gamma> \<turnstile> (LET p = t IN u) : U"
   3.190 +
   3.191 +equivariance ptyping
   3.192 +
   3.193 +equivariance valid
   3.194 +
   3.195 +equivariance typing
   3.196 +
   3.197 +lemma valid_typing:
   3.198 +  assumes "\<Gamma> \<turnstile> t : T"
   3.199 +  shows "valid \<Gamma>" using assms
   3.200 +  by induct auto
   3.201 +
   3.202 +lemma pat_var:
   3.203 +  assumes "\<turnstile> p : T \<Rightarrow> \<Delta>"
   3.204 +  shows "(supp p::name set) = supp \<Delta>" using assms
   3.205 +  by induct (auto simp add: supp_list_nil supp_list_cons supp_prod supp_list_append)
   3.206 +
   3.207 +lemma valid_app_fresh:
   3.208 +  assumes "valid (\<Delta> @ \<Gamma>)" and "(x::name) \<in> supp \<Delta>"
   3.209 +  shows "x \<sharp> \<Gamma>" using assms
   3.210 +  by (induct \<Delta>)
   3.211 +    (auto simp add: supp_list_nil supp_list_cons supp_prod supp_atm fresh_list_append)
   3.212 +
   3.213 +lemma pat_freshs:
   3.214 +  assumes "\<turnstile> p : T \<Rightarrow> \<Delta>"
   3.215 +  shows "(supp p::name set) \<sharp>* c = (supp \<Delta>::name set) \<sharp>* c" using assms
   3.216 +  by (auto simp add: fresh_star_def pat_var)
   3.217 +
   3.218 +lemma valid_app_mono:
   3.219 +  assumes "valid (\<Delta> @ \<Gamma>\<^isub>1)" and "(supp \<Delta>::name set) \<sharp>* \<Gamma>\<^isub>2" and "valid \<Gamma>\<^isub>2" and "\<Gamma>\<^isub>1 \<sqsubseteq> \<Gamma>\<^isub>2"
   3.220 +  shows "valid (\<Delta> @ \<Gamma>\<^isub>2)" using assms
   3.221 +  by (induct \<Delta>)
   3.222 +    (auto simp add: supp_list_cons fresh_star_Un_elim supp_prod
   3.223 +       fresh_list_append supp_atm fresh_star_insert_elim fresh_star_empty_elim)
   3.224 +
   3.225 +nominal_inductive2 typing
   3.226 +avoids
   3.227 +  Abs: "{x}"
   3.228 +| Let: "(supp p)::name set"
   3.229 +  by (auto simp add: fresh_star_def abs_fresh fin_supp pat_var
   3.230 +    dest!: valid_typing valid_app_fresh)
   3.231 +
   3.232 +lemma better_T_Let [intro]:
   3.233 +  assumes t: "\<Gamma> \<turnstile> t : T" and p: "\<turnstile> p : T \<Rightarrow> \<Delta>" and u: "\<Delta> @ \<Gamma> \<turnstile> u : U"
   3.234 +  shows "\<Gamma> \<turnstile> (LET p = t IN u) : U"
   3.235 +proof -
   3.236 +  obtain pi::"name prm" where pi: "(pi \<bullet> (supp p::name set)) \<sharp>* (t, Base u, \<Gamma>)"
   3.237 +    and pi': "set pi \<subseteq> supp p \<times> (pi \<bullet> supp p)"
   3.238 +    by (rule at_set_avoiding [OF at_name_inst fin_supp fin_supp])
   3.239 +  from p u have p_fresh: "(supp p::name set) \<sharp>* \<Gamma>"
   3.240 +    by (auto simp add: fresh_star_def pat_var dest!: valid_typing valid_app_fresh)
   3.241 +  from pi have p_fresh': "(pi \<bullet> (supp p::name set)) \<sharp>* \<Gamma>"
   3.242 +    by (simp add: fresh_star_prod_elim)
   3.243 +  from pi have p_fresh'': "(pi \<bullet> (supp p::name set)) \<sharp>* Base u"
   3.244 +    by (simp add: fresh_star_prod_elim)
   3.245 +  from pi have "(supp (pi \<bullet> p)::name set) \<sharp>* t"
   3.246 +    by (simp add: fresh_star_prod_elim eqvts)
   3.247 +  moreover note t
   3.248 +  moreover from p have "pi \<bullet> (\<turnstile> p : T \<Rightarrow> \<Delta>)" by (rule perm_boolI)
   3.249 +  then have "\<turnstile> (pi \<bullet> p) : T \<Rightarrow> (pi \<bullet> \<Delta>)" by (simp add: eqvts perm_type)
   3.250 +  moreover from u have "pi \<bullet> (\<Delta> @ \<Gamma> \<turnstile> u : U)" by (rule perm_boolI)
   3.251 +  with pt_freshs_freshs [OF pt_name_inst at_name_inst pi' p_fresh p_fresh']
   3.252 +  have "(pi \<bullet> \<Delta>) @ \<Gamma> \<turnstile> (pi \<bullet> u) : U" by (simp add: eqvts perm_type)
   3.253 +  ultimately have "\<Gamma> \<turnstile> (LET (pi \<bullet> p) = t IN (pi \<bullet> u)) : U"
   3.254 +    by (rule Let)
   3.255 +  then show ?thesis by (simp add: abs_pat_alpha [OF p_fresh'' pi'] pat_type_perm_eq)
   3.256 +qed
   3.257 +
   3.258 +lemma weakening: 
   3.259 +  assumes "\<Gamma>\<^isub>1 \<turnstile> t : T" and "valid \<Gamma>\<^isub>2" and "\<Gamma>\<^isub>1 \<sqsubseteq> \<Gamma>\<^isub>2"
   3.260 +  shows "\<Gamma>\<^isub>2 \<turnstile> t : T" using assms
   3.261 +  apply (nominal_induct \<Gamma>\<^isub>1 t T avoiding: \<Gamma>\<^isub>2 rule: typing.strong_induct)
   3.262 +  apply auto
   3.263 +  apply (drule_tac x="(x, T) # \<Gamma>\<^isub>2" in meta_spec)
   3.264 +  apply (auto intro: valid_typing)
   3.265 +  apply (drule_tac x="\<Gamma>\<^isub>2" in meta_spec)
   3.266 +  apply (drule_tac x="\<Delta> @ \<Gamma>\<^isub>2" in meta_spec)
   3.267 +  apply (auto intro: valid_typing)
   3.268 +  apply (rule typing.Let)
   3.269 +  apply assumption+
   3.270 +  apply (drule meta_mp)
   3.271 +  apply (rule valid_app_mono)
   3.272 +  apply (rule valid_typing)
   3.273 +  apply assumption
   3.274 +  apply (auto simp add: pat_freshs)
   3.275 +  done
   3.276 +
   3.277 +inductive
   3.278 +  match :: "pat \<Rightarrow> trm \<Rightarrow> (name \<times> trm) list \<Rightarrow> bool"  ("\<turnstile> _ \<rhd> _ \<Rightarrow> _" [50, 50, 50] 50)
   3.279 +where
   3.280 +  PVar: "\<turnstile> PVar x T \<rhd> t \<Rightarrow> [(x, t)]"
   3.281 +| PProd: "\<turnstile> p \<rhd> t \<Rightarrow> \<theta> \<Longrightarrow> \<turnstile> q \<rhd> u \<Rightarrow> \<theta>' \<Longrightarrow> \<turnstile> \<langle>\<langle>p, q\<rangle>\<rangle> \<rhd> \<langle>t, u\<rangle> \<Rightarrow> \<theta> @ \<theta>'"
   3.282 +
   3.283 +fun
   3.284 +  lookup :: "(name \<times> trm) list \<Rightarrow> name \<Rightarrow> trm"   
   3.285 +where
   3.286 +  "lookup [] x = Var x"
   3.287 +| "lookup ((y, e) # \<theta>) x = (if x = y then e else lookup \<theta> x)"
   3.288 +
   3.289 +lemma lookup_eqvt[eqvt]:
   3.290 +  fixes pi :: "name prm"
   3.291 +  and   \<theta> :: "(name \<times> trm) list"
   3.292 +  and   X :: "name"
   3.293 +  shows "pi \<bullet> (lookup \<theta> X) = lookup (pi \<bullet> \<theta>) (pi \<bullet> X)"
   3.294 +  by (induct \<theta>) (auto simp add: eqvts)
   3.295 + 
   3.296 +nominal_primrec
   3.297 +  psubst :: "(name \<times> trm) list \<Rightarrow> trm \<Rightarrow> trm"  ("_\<lparr>_\<rparr>" [95,0] 210)
   3.298 +  and psubstb :: "(name \<times> trm) list \<Rightarrow> btrm \<Rightarrow> btrm"  ("_\<lparr>_\<rparr>\<^sub>b" [95,0] 210)
   3.299 +where
   3.300 +  "\<theta>\<lparr>Var x\<rparr> = (lookup \<theta> x)"
   3.301 +| "\<theta>\<lparr>t \<cdot> u\<rparr> = \<theta>\<lparr>t\<rparr> \<cdot> \<theta>\<lparr>u\<rparr>"
   3.302 +| "\<theta>\<lparr>\<langle>t, u\<rangle>\<rparr> = \<langle>\<theta>\<lparr>t\<rparr>, \<theta>\<lparr>u\<rparr>\<rangle>"
   3.303 +| "\<theta>\<lparr>Let T t u\<rparr> = Let T (\<theta>\<lparr>t\<rparr>) (\<theta>\<lparr>u\<rparr>\<^sub>b)"
   3.304 +| "x \<sharp> \<theta> \<Longrightarrow> \<theta>\<lparr>\<lambda>x:T. t\<rparr> = (\<lambda>x:T. \<theta>\<lparr>t\<rparr>)"
   3.305 +| "\<theta>\<lparr>Base t\<rparr>\<^sub>b = Base (\<theta>\<lparr>t\<rparr>)"
   3.306 +| "x \<sharp> \<theta> \<Longrightarrow> \<theta>\<lparr>Bind T x t\<rparr>\<^sub>b = Bind T x (\<theta>\<lparr>t\<rparr>\<^sub>b)"
   3.307 +  apply finite_guess+
   3.308 +  apply (simp add: abs_fresh | fresh_guess)+
   3.309 +  done
   3.310 +
   3.311 +lemma lookup_fresh:
   3.312 +  "x = y \<longrightarrow> x \<in> set (map fst \<theta>) \<Longrightarrow> \<forall>(y, t)\<in>set \<theta>. x \<sharp> t \<Longrightarrow> x \<sharp> lookup \<theta> y"
   3.313 +  apply (induct \<theta>)
   3.314 +  apply (simp_all add: split_paired_all fresh_atm)
   3.315 +  apply (case_tac "x = y")
   3.316 +  apply (auto simp add: fresh_atm)
   3.317 +  done
   3.318 +
   3.319 +lemma psubst_fresh:
   3.320 +  assumes "x \<in> set (map fst \<theta>)" and "\<forall>(y, t)\<in>set \<theta>. x \<sharp> t"
   3.321 +  shows "x \<sharp> \<theta>\<lparr>t\<rparr>" and "x \<sharp> \<theta>\<lparr>t'\<rparr>\<^sub>b" using assms
   3.322 +  apply (nominal_induct t and t' avoiding: \<theta> rule: trm_btrm.strong_inducts)
   3.323 +  apply simp
   3.324 +  apply (rule lookup_fresh)
   3.325 +  apply (rule impI)
   3.326 +  apply (simp_all add: abs_fresh)
   3.327 +  done
   3.328 +
   3.329 +lemma psubst_eqvt[eqvt]:
   3.330 +  fixes pi :: "name prm" 
   3.331 +  shows "pi \<bullet> (\<theta>\<lparr>t\<rparr>) = (pi \<bullet> \<theta>)\<lparr>pi \<bullet> t\<rparr>"
   3.332 +  and "pi \<bullet> (\<theta>\<lparr>t'\<rparr>\<^sub>b) = (pi \<bullet> \<theta>)\<lparr>pi \<bullet> t'\<rparr>\<^sub>b"
   3.333 +  by (nominal_induct t and t' avoiding: \<theta> rule: trm_btrm.strong_inducts)
   3.334 +    (simp_all add: eqvts fresh_bij)
   3.335 +
   3.336 +abbreviation 
   3.337 +  subst :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_[_\<mapsto>_]" [100,0,0] 100)
   3.338 +where 
   3.339 +  "t[x\<mapsto>t'] \<equiv> [(x,t')]\<lparr>t\<rparr>"
   3.340 +
   3.341 +abbreviation 
   3.342 +  substb :: "btrm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> btrm" ("_[_\<mapsto>_]\<^sub>b" [100,0,0] 100)
   3.343 +where 
   3.344 +  "t[x\<mapsto>t']\<^sub>b \<equiv> [(x,t')]\<lparr>t\<rparr>\<^sub>b"
   3.345 +
   3.346 +lemma lookup_forget:
   3.347 +  "(supp (map fst \<theta>)::name set) \<sharp>* x \<Longrightarrow> lookup \<theta> x = Var x"
   3.348 +  by (induct \<theta>) (auto simp add: split_paired_all fresh_star_def fresh_atm supp_list_cons supp_atm)
   3.349 +
   3.350 +lemma supp_fst: "(x::name) \<in> supp (map fst (\<theta>::(name \<times> trm) list)) \<Longrightarrow> x \<in> supp \<theta>"
   3.351 +  by (induct \<theta>) (auto simp add: supp_list_nil supp_list_cons supp_prod)
   3.352 +
   3.353 +lemma psubst_forget:
   3.354 +  "(supp (map fst \<theta>)::name set) \<sharp>* t \<Longrightarrow> \<theta>\<lparr>t\<rparr> = t"
   3.355 +  "(supp (map fst \<theta>)::name set) \<sharp>* t' \<Longrightarrow> \<theta>\<lparr>t'\<rparr>\<^sub>b = t'"
   3.356 +  apply (nominal_induct t and t' avoiding: \<theta> rule: trm_btrm.strong_inducts)
   3.357 +  apply (auto simp add: fresh_star_def lookup_forget abs_fresh)
   3.358 +  apply (drule_tac x=\<theta> in meta_spec)
   3.359 +  apply (drule meta_mp)
   3.360 +  apply (rule ballI)
   3.361 +  apply (drule_tac x=x in bspec)
   3.362 +  apply assumption
   3.363 +  apply (drule supp_fst)
   3.364 +  apply (auto simp add: fresh_def)
   3.365 +  apply (drule_tac x=\<theta> in meta_spec)
   3.366 +  apply (drule meta_mp)
   3.367 +  apply (rule ballI)
   3.368 +  apply (drule_tac x=x in bspec)
   3.369 +  apply assumption
   3.370 +  apply (drule supp_fst)
   3.371 +  apply (auto simp add: fresh_def)
   3.372 +  done
   3.373 +
   3.374 +lemma psubst_nil: "[]\<lparr>t\<rparr> = t" "[]\<lparr>t'\<rparr>\<^sub>b = t'"
   3.375 +  by (induct t and t' rule: trm_btrm.inducts) (simp_all add: fresh_list_nil)
   3.376 +
   3.377 +lemma psubst_cons:
   3.378 +  assumes "(supp (map fst \<theta>)::name set) \<sharp>* u"
   3.379 +  shows "((x, u) # \<theta>)\<lparr>t\<rparr> = \<theta>\<lparr>t[x\<mapsto>u]\<rparr>" and "((x, u) # \<theta>)\<lparr>t'\<rparr>\<^sub>b = \<theta>\<lparr>t'[x\<mapsto>u]\<^sub>b\<rparr>\<^sub>b"
   3.380 +  using assms
   3.381 +  by (nominal_induct t and t' avoiding: x u \<theta> rule: trm_btrm.strong_inducts)
   3.382 +    (simp_all add: fresh_list_nil fresh_list_cons psubst_forget)
   3.383 +
   3.384 +lemma psubst_append:
   3.385 +  "(supp (map fst (\<theta>\<^isub>1 @ \<theta>\<^isub>2))::name set) \<sharp>* map snd (\<theta>\<^isub>1 @ \<theta>\<^isub>2) \<Longrightarrow> (\<theta>\<^isub>1 @ \<theta>\<^isub>2)\<lparr>t\<rparr> = \<theta>\<^isub>2\<lparr>\<theta>\<^isub>1\<lparr>t\<rparr>\<rparr>"
   3.386 +  by (induct \<theta>\<^isub>1 arbitrary: t)
   3.387 +    (simp_all add: psubst_nil split_paired_all supp_list_cons psubst_cons fresh_star_def
   3.388 +      fresh_list_cons fresh_list_append supp_list_append)
   3.389 +
   3.390 +lemma abs_pat_psubst [simp]:
   3.391 +  "(supp p::name set) \<sharp>* \<theta> \<Longrightarrow> \<theta>\<lparr>\<lambda>[p]. t\<rparr>\<^sub>b = (\<lambda>[p]. \<theta>\<lparr>t\<rparr>\<^sub>b)"
   3.392 +  by (induct p arbitrary: t) (auto simp add: fresh_star_def supp_atm)
   3.393 +
   3.394 +lemma valid_insert:
   3.395 +  assumes "valid (\<Delta> @ [(x, T)] @ \<Gamma>)"
   3.396 +  shows "valid (\<Delta> @ \<Gamma>)" using assms
   3.397 +  by (induct \<Delta>)
   3.398 +    (auto simp add: fresh_list_append fresh_list_cons)
   3.399 +
   3.400 +lemma fresh_set: 
   3.401 +  shows "y \<sharp> xs = (\<forall>x\<in>set xs. y \<sharp> x)"
   3.402 +  by (induct xs) (simp_all add: fresh_list_nil fresh_list_cons)
   3.403 +
   3.404 +lemma context_unique:
   3.405 +  assumes "valid \<Gamma>"
   3.406 +  and "(x, T) \<in> set \<Gamma>"
   3.407 +  and "(x, U) \<in> set \<Gamma>"
   3.408 +  shows "T = U" using assms
   3.409 +  by induct (auto simp add: fresh_set fresh_prod fresh_atm)
   3.410 +
   3.411 +lemma subst_type_aux:
   3.412 +  assumes a: "\<Delta> @ [(x, U)] @ \<Gamma> \<turnstile> t : T"
   3.413 +  and b: "\<Gamma> \<turnstile> u : U"
   3.414 +  shows "\<Delta> @ \<Gamma> \<turnstile> t[x\<mapsto>u] : T" using a b
   3.415 +proof (nominal_induct \<Gamma>'\<equiv>"\<Delta> @ [(x, U)] @ \<Gamma>" t T avoiding: x u \<Delta> rule: typing.strong_induct)
   3.416 +  case (Var \<Gamma>' y T x u \<Delta>)
   3.417 +  then have a1: "valid (\<Delta> @ [(x, U)] @ \<Gamma>)" 
   3.418 +       and  a2: "(y, T) \<in> set (\<Delta> @ [(x, U)] @ \<Gamma>)" 
   3.419 +       and  a3: "\<Gamma> \<turnstile> u : U" by simp_all
   3.420 +  from a1 have a4: "valid (\<Delta> @ \<Gamma>)" by (rule valid_insert)
   3.421 +  show "\<Delta> @ \<Gamma> \<turnstile> Var y[x\<mapsto>u] : T"
   3.422 +  proof cases
   3.423 +    assume eq: "x = y"
   3.424 +    from a1 a2 have "T = U" using eq by (auto intro: context_unique)
   3.425 +    with a3 show "\<Delta> @ \<Gamma> \<turnstile> Var y[x\<mapsto>u] : T" using eq a4 by (auto intro: weakening)
   3.426 +  next
   3.427 +    assume ineq: "x \<noteq> y"
   3.428 +    from a2 have "(y, T) \<in> set (\<Delta> @ \<Gamma>)" using ineq by simp
   3.429 +    then show "\<Delta> @ \<Gamma> \<turnstile> Var y[x\<mapsto>u] : T" using ineq a4 by auto
   3.430 +  qed
   3.431 +next
   3.432 +  case (Tuple \<Gamma>' t\<^isub>1 T\<^isub>1 t\<^isub>2 T\<^isub>2)
   3.433 +  from `\<Gamma> \<turnstile> u : U` `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>`
   3.434 +  have "\<Delta> @ \<Gamma> \<turnstile> t\<^isub>1[x\<mapsto>u] : T\<^isub>1" by (rule Tuple)
   3.435 +  moreover from `\<Gamma> \<turnstile> u : U` `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>`
   3.436 +  have "\<Delta> @ \<Gamma> \<turnstile> t\<^isub>2[x\<mapsto>u] : T\<^isub>2" by (rule Tuple)
   3.437 +  ultimately have "\<Delta> @ \<Gamma> \<turnstile> \<langle>t\<^isub>1[x\<mapsto>u], t\<^isub>2[x\<mapsto>u]\<rangle> : T\<^isub>1 \<otimes> T\<^isub>2" ..
   3.438 +  then show ?case by simp
   3.439 +next
   3.440 +  case (Let p t \<Gamma>' T \<Delta>' s S)
   3.441 +  from `\<Gamma> \<turnstile> u : U` `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>`
   3.442 +  have "\<Delta> @ \<Gamma> \<turnstile> t[x\<mapsto>u] : T" by (rule Let)
   3.443 +  moreover note `\<turnstile> p : T \<Rightarrow> \<Delta>'`
   3.444 +  moreover from `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>`
   3.445 +  have "\<Delta>' @ \<Gamma>' = (\<Delta>' @ \<Delta>) @ [(x, U)] @ \<Gamma>" by simp
   3.446 +  with `\<Gamma> \<turnstile> u : U` have "(\<Delta>' @ \<Delta>) @ \<Gamma> \<turnstile> s[x\<mapsto>u] : S" by (rule Let)
   3.447 +  then have "\<Delta>' @ \<Delta> @ \<Gamma> \<turnstile> s[x\<mapsto>u] : S" by simp
   3.448 +  ultimately have "\<Delta> @ \<Gamma> \<turnstile> (LET p = t[x\<mapsto>u] IN s[x\<mapsto>u]) : S"
   3.449 +    by (rule better_T_Let)
   3.450 +  moreover from Let have "(supp p::name set) \<sharp>* [(x, u)]"
   3.451 +    by (simp add: fresh_star_def fresh_list_nil fresh_list_cons)
   3.452 +  ultimately show ?case by simp
   3.453 +next
   3.454 +  case (Abs y T \<Gamma>' t S)
   3.455 +  from `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>` have "(y, T) # \<Gamma>' = ((y, T) # \<Delta>) @ [(x, U)] @ \<Gamma>"
   3.456 +    by simp
   3.457 +  with `\<Gamma> \<turnstile> u : U` have "((y, T) # \<Delta>) @ \<Gamma> \<turnstile> t[x\<mapsto>u] : S" by (rule Abs)
   3.458 +  then have "(y, T) # \<Delta> @ \<Gamma> \<turnstile> t[x\<mapsto>u] : S" by simp
   3.459 +  then have "\<Delta> @ \<Gamma> \<turnstile> (\<lambda>y:T. t[x\<mapsto>u]) : T \<rightarrow> S"
   3.460 +    by (rule typing.Abs)
   3.461 +  moreover from Abs have "y \<sharp> [(x, u)]"
   3.462 +    by (simp add: fresh_list_nil fresh_list_cons)
   3.463 +  ultimately show ?case by simp
   3.464 +next
   3.465 +  case (App \<Gamma>' t\<^isub>1 T S t\<^isub>2)
   3.466 +  from `\<Gamma> \<turnstile> u : U` `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>`
   3.467 +  have "\<Delta> @ \<Gamma> \<turnstile> t\<^isub>1[x\<mapsto>u] : T \<rightarrow> S" by (rule App)
   3.468 +  moreover from `\<Gamma> \<turnstile> u : U` `\<Gamma>' = \<Delta> @ [(x, U)] @ \<Gamma>`
   3.469 +  have "\<Delta> @ \<Gamma> \<turnstile> t\<^isub>2[x\<mapsto>u] : T" by (rule App)
   3.470 +  ultimately have "\<Delta> @ \<Gamma> \<turnstile> (t\<^isub>1[x\<mapsto>u]) \<cdot> (t\<^isub>2[x\<mapsto>u]) : S"
   3.471 +    by (rule typing.App)
   3.472 +  then show ?case by simp
   3.473 +qed
   3.474 +
   3.475 +lemmas subst_type = subst_type_aux [of "[]", simplified]
   3.476 +
   3.477 +lemma match_supp_fst:
   3.478 +  assumes "\<turnstile> p \<rhd> u \<Rightarrow> \<theta>" shows "(supp (map fst \<theta>)::name set) = supp p" using assms
   3.479 +  by induct (simp_all add: supp_list_nil supp_list_cons supp_list_append)
   3.480 +
   3.481 +lemma match_supp_snd:
   3.482 +  assumes "\<turnstile> p \<rhd> u \<Rightarrow> \<theta>" shows "(supp (map snd \<theta>)::name set) = supp u" using assms
   3.483 +  by induct (simp_all add: supp_list_nil supp_list_cons supp_list_append trm.supp)
   3.484 +
   3.485 +lemma match_fresh: "\<turnstile> p \<rhd> u \<Rightarrow> \<theta> \<Longrightarrow> (supp p::name set) \<sharp>* u \<Longrightarrow>
   3.486 +  (supp (map fst \<theta>)::name set) \<sharp>* map snd \<theta>"
   3.487 +  by (simp add: fresh_star_def fresh_def match_supp_fst match_supp_snd)
   3.488 +
   3.489 +lemma match_type_aux:
   3.490 +  assumes "\<turnstile> p : U \<Rightarrow> \<Delta>"
   3.491 +  and "\<Gamma>\<^isub>2 \<turnstile> u : U"
   3.492 +  and "\<Gamma>\<^isub>1 @ \<Delta> @ \<Gamma>\<^isub>2 \<turnstile> t : T"
   3.493 +  and "\<turnstile> p \<rhd> u \<Rightarrow> \<theta>"
   3.494 +  and "(supp p::name set) \<sharp>* u"
   3.495 +  shows "\<Gamma>\<^isub>1 @ \<Gamma>\<^isub>2 \<turnstile> \<theta>\<lparr>t\<rparr> : T" using assms
   3.496 +proof (induct arbitrary: \<Gamma>\<^isub>1 \<Gamma>\<^isub>2 t u T \<theta>)
   3.497 +  case (PVar x U)
   3.498 +  from `\<Gamma>\<^isub>1 @ [(x, U)] @ \<Gamma>\<^isub>2 \<turnstile> t : T` `\<Gamma>\<^isub>2 \<turnstile> u : U`
   3.499 +  have "\<Gamma>\<^isub>1 @ \<Gamma>\<^isub>2 \<turnstile> t[x\<mapsto>u] : T" by (rule subst_type_aux)
   3.500 +  moreover from `\<turnstile> PVar x U \<rhd> u \<Rightarrow> \<theta>` have "\<theta> = [(x, u)]"
   3.501 +    by cases simp_all
   3.502 +  ultimately show ?case by simp
   3.503 +next
   3.504 +  case (PTuple p S \<Delta>\<^isub>1 q U \<Delta>\<^isub>2)
   3.505 +  from `\<turnstile> \<langle>\<langle>p, q\<rangle>\<rangle> \<rhd> u \<Rightarrow> \<theta>` obtain u\<^isub>1 u\<^isub>2 \<theta>\<^isub>1 \<theta>\<^isub>2
   3.506 +    where u: "u = \<langle>u\<^isub>1, u\<^isub>2\<rangle>" and \<theta>: "\<theta> = \<theta>\<^isub>1 @ \<theta>\<^isub>2"
   3.507 +    and p: "\<turnstile> p \<rhd> u\<^isub>1 \<Rightarrow> \<theta>\<^isub>1" and q: "\<turnstile> q \<rhd> u\<^isub>2 \<Rightarrow> \<theta>\<^isub>2"
   3.508 +    by cases simp_all
   3.509 +  with PTuple have "\<Gamma>\<^isub>2 \<turnstile> \<langle>u\<^isub>1, u\<^isub>2\<rangle> : S \<otimes> U" by simp
   3.510 +  then obtain u\<^isub>1: "\<Gamma>\<^isub>2 \<turnstile> u\<^isub>1 : S" and u\<^isub>2: "\<Gamma>\<^isub>2 \<turnstile> u\<^isub>2 : U"
   3.511 +    by cases (simp_all add: ty.inject trm.inject)
   3.512 +  note u\<^isub>1
   3.513 +  moreover from `\<Gamma>\<^isub>1 @ (\<Delta>\<^isub>2 @ \<Delta>\<^isub>1) @ \<Gamma>\<^isub>2 \<turnstile> t : T`
   3.514 +  have "(\<Gamma>\<^isub>1 @ \<Delta>\<^isub>2) @ \<Delta>\<^isub>1 @ \<Gamma>\<^isub>2 \<turnstile> t : T" by simp
   3.515 +  moreover note p
   3.516 +  moreover from `supp \<langle>\<langle>p, q\<rangle>\<rangle> \<sharp>* u` and u
   3.517 +  have "(supp p::name set) \<sharp>* u\<^isub>1" by (simp add: fresh_star_def)
   3.518 +  ultimately have \<theta>\<^isub>1: "(\<Gamma>\<^isub>1 @ \<Delta>\<^isub>2) @ \<Gamma>\<^isub>2 \<turnstile> \<theta>\<^isub>1\<lparr>t\<rparr> : T"
   3.519 +    by (rule PTuple)
   3.520 +  note u\<^isub>2
   3.521 +  moreover from \<theta>\<^isub>1
   3.522 +  have "\<Gamma>\<^isub>1 @ \<Delta>\<^isub>2 @ \<Gamma>\<^isub>2 \<turnstile> \<theta>\<^isub>1\<lparr>t\<rparr> : T" by simp
   3.523 +  moreover note q
   3.524 +  moreover from `supp \<langle>\<langle>p, q\<rangle>\<rangle> \<sharp>* u` and u
   3.525 +  have "(supp q::name set) \<sharp>* u\<^isub>2" by (simp add: fresh_star_def)
   3.526 +  ultimately have "\<Gamma>\<^isub>1 @ \<Gamma>\<^isub>2 \<turnstile> \<theta>\<^isub>2\<lparr>\<theta>\<^isub>1\<lparr>t\<rparr>\<rparr> : T"
   3.527 +    by (rule PTuple)
   3.528 +  moreover from `\<turnstile> \<langle>\<langle>p, q\<rangle>\<rangle> \<rhd> u \<Rightarrow> \<theta>` `supp \<langle>\<langle>p, q\<rangle>\<rangle> \<sharp>* u`
   3.529 +  have "(supp (map fst \<theta>)::name set) \<sharp>* map snd \<theta>"
   3.530 +    by (rule match_fresh)
   3.531 +  ultimately show ?case using \<theta> by (simp add: psubst_append)
   3.532 +qed
   3.533 +
   3.534 +lemmas match_type = match_type_aux [where \<Gamma>\<^isub>1="[]", simplified]
   3.535 +
   3.536 +inductive eval :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<longmapsto> _" [60,60] 60)
   3.537 +where
   3.538 +  TupleL: "t \<longmapsto> t' \<Longrightarrow> \<langle>t, u\<rangle> \<longmapsto> \<langle>t', u\<rangle>"
   3.539 +| TupleR: "u \<longmapsto> u' \<Longrightarrow> \<langle>t, u\<rangle> \<longmapsto> \<langle>t, u'\<rangle>"
   3.540 +| Abs: "t \<longmapsto> t' \<Longrightarrow> (\<lambda>x:T. t) \<longmapsto> (\<lambda>x:T. t')"
   3.541 +| AppL: "t \<longmapsto> t' \<Longrightarrow> t \<cdot> u \<longmapsto> t' \<cdot> u"
   3.542 +| AppR: "u \<longmapsto> u' \<Longrightarrow> t \<cdot> u \<longmapsto> t \<cdot> u'"
   3.543 +| Beta: "x \<sharp> u \<Longrightarrow> (\<lambda>x:T. t) \<cdot> u \<longmapsto> t[x\<mapsto>u]"
   3.544 +| Let: "((supp p)::name set) \<sharp>* t \<Longrightarrow> distinct (pat_vars p) \<Longrightarrow>
   3.545 +    \<turnstile> p \<rhd> t \<Rightarrow> \<theta> \<Longrightarrow> (LET p = t IN u) \<longmapsto> \<theta>\<lparr>u\<rparr>"
   3.546 +
   3.547 +equivariance match
   3.548 +
   3.549 +equivariance eval
   3.550 +
   3.551 +lemma match_vars:
   3.552 +  assumes "\<turnstile> p \<rhd> t \<Rightarrow> \<theta>" and "x \<in> supp p"
   3.553 +  shows "x \<in> set (map fst \<theta>)" using assms
   3.554 +  by induct (auto simp add: supp_atm)
   3.555 +
   3.556 +lemma match_fresh_mono:
   3.557 +  assumes "\<turnstile> p \<rhd> t \<Rightarrow> \<theta>" and "(x::name) \<sharp> t"
   3.558 +  shows "\<forall>(y, t)\<in>set \<theta>. x \<sharp> t" using assms
   3.559 +  by induct auto
   3.560 +
   3.561 +nominal_inductive2 eval
   3.562 +avoids
   3.563 +  Abs: "{x}"
   3.564 +| Beta: "{x}"
   3.565 +| Let: "(supp p)::name set"
   3.566 +  apply (simp_all add: fresh_star_def abs_fresh fin_supp)
   3.567 +  apply (rule psubst_fresh)
   3.568 +  apply simp
   3.569 +  apply simp
   3.570 +  apply (rule ballI)
   3.571 +  apply (rule psubst_fresh)
   3.572 +  apply (rule match_vars)
   3.573 +  apply assumption+
   3.574 +  apply (rule match_fresh_mono)
   3.575 +  apply auto
   3.576 +  done
   3.577 +
   3.578 +lemma typing_case_Abs:
   3.579 +  assumes ty: "\<Gamma> \<turnstile> (\<lambda>x:T. t) : S"
   3.580 +  and fresh: "x \<sharp> \<Gamma>"
   3.581 +  and R: "\<And>U. S = T \<rightarrow> U \<Longrightarrow> (x, T) # \<Gamma> \<turnstile> t : U \<Longrightarrow> P"
   3.582 +  shows P using ty
   3.583 +proof cases
   3.584 +  case (Abs x' T' \<Gamma>' t' U)
   3.585 +  obtain y::name where y: "y \<sharp> (x, \<Gamma>, \<lambda>x':T'. t')"
   3.586 +    by (rule exists_fresh) (auto intro: fin_supp)
   3.587 +  from `(\<lambda>x:T. t) = (\<lambda>x':T'. t')` [symmetric]
   3.588 +  have x: "x \<sharp> (\<lambda>x':T'. t')" by (simp add: abs_fresh)
   3.589 +  have x': "x' \<sharp> (\<lambda>x':T'. t')" by (simp add: abs_fresh)
   3.590 +  from `(x', T') # \<Gamma>' \<turnstile> t' : U` have x'': "x' \<sharp> \<Gamma>'"
   3.591 +    by (auto dest: valid_typing)
   3.592 +  have "(\<lambda>x:T. t) = (\<lambda>x':T'. t')" by fact
   3.593 +  also from x x' y have "\<dots> = [(x, y)] \<bullet> [(x', y)] \<bullet> (\<lambda>x':T'. t')"
   3.594 +    by (simp only: perm_fresh_fresh fresh_prod)
   3.595 +  also have "\<dots> = (\<lambda>x:T'. [(x, y)] \<bullet> [(x', y)] \<bullet> t')"
   3.596 +    by (simp add: swap_simps perm_fresh_fresh)
   3.597 +  finally have "(\<lambda>x:T. t) = (\<lambda>x:T'. [(x, y)] \<bullet> [(x', y)] \<bullet> t')" .
   3.598 +  then have T: "T = T'" and t: "[(x, y)] \<bullet> [(x', y)] \<bullet> t' = t"
   3.599 +    by (simp_all add: trm.inject alpha)
   3.600 +  from Abs T have "S = T \<rightarrow> U" by simp
   3.601 +  moreover from `(x', T') # \<Gamma>' \<turnstile> t' : U`
   3.602 +  have "[(x, y)] \<bullet> [(x', y)] \<bullet> ((x', T') # \<Gamma>' \<turnstile> t' : U)"
   3.603 +    by (simp add: perm_bool)
   3.604 +  with T t y `\<Gamma> = \<Gamma>'` x'' fresh have "(x, T) # \<Gamma> \<turnstile> t : U"
   3.605 +    by (simp add: eqvts swap_simps perm_fresh_fresh fresh_prod)
   3.606 +  ultimately show ?thesis by (rule R)
   3.607 +qed simp_all
   3.608 +
   3.609 +nominal_primrec ty_size :: "ty \<Rightarrow> nat"
   3.610 +where
   3.611 +  "ty_size (Atom n) = 0"
   3.612 +| "ty_size (T \<rightarrow> U) = ty_size T + ty_size U + 1"
   3.613 +| "ty_size (T \<otimes> U) = ty_size T + ty_size U + 1"
   3.614 +  by (rule TrueI)+
   3.615 +
   3.616 +lemma bind_tuple_ineq:
   3.617 +  "ty_size (pat_type p) < ty_size U \<Longrightarrow> Bind U x t \<noteq> (\<lambda>[p]. u)"
   3.618 +  by (induct p arbitrary: U x t u) (auto simp add: btrm.inject)
   3.619 +
   3.620 +lemma valid_appD: assumes "valid (\<Gamma> @ \<Delta>)"
   3.621 +  shows "valid \<Gamma>" "valid \<Delta>" using assms
   3.622 +  by (induct \<Gamma>'\<equiv>"\<Gamma> @ \<Delta>" arbitrary: \<Gamma> \<Delta>)
   3.623 +    (auto simp add: Cons_eq_append_conv fresh_list_append)
   3.624 +
   3.625 +lemma valid_app_freshs: assumes "valid (\<Gamma> @ \<Delta>)"
   3.626 +  shows "(supp \<Gamma>::name set) \<sharp>* \<Delta>" "(supp \<Delta>::name set) \<sharp>* \<Gamma>" using assms
   3.627 +  by (induct \<Gamma>'\<equiv>"\<Gamma> @ \<Delta>" arbitrary: \<Gamma> \<Delta>)
   3.628 +    (auto simp add: Cons_eq_append_conv fresh_star_def
   3.629 +     fresh_list_nil fresh_list_cons supp_list_nil supp_list_cons fresh_list_append
   3.630 +     supp_prod fresh_prod supp_atm fresh_atm
   3.631 +     dest: notE [OF iffD1 [OF fresh_def [THEN meta_eq_to_obj_eq]]])
   3.632 +
   3.633 +lemma perm_mem_left: "(x::name) \<in> ((pi::name prm) \<bullet> A) \<Longrightarrow> (rev pi \<bullet> x) \<in> A"
   3.634 +  by (drule perm_boolI [of _ "rev pi"]) (simp add: eqvts perm_pi_simp)
   3.635 +
   3.636 +lemma perm_mem_right: "(rev (pi::name prm) \<bullet> (x::name)) \<in> A \<Longrightarrow> x \<in> (pi \<bullet> A)"
   3.637 +  by (drule perm_boolI [of _ pi]) (simp add: eqvts perm_pi_simp)
   3.638 +
   3.639 +lemma perm_cases:
   3.640 +  assumes pi: "set pi \<subseteq> A \<times> A"
   3.641 +  shows "((pi::name prm) \<bullet> B) \<subseteq> A \<union> B"
   3.642 +proof
   3.643 +  fix x assume "x \<in> pi \<bullet> B"
   3.644 +  then show "x \<in> A \<union> B" using pi
   3.645 +    apply (induct pi arbitrary: x B rule: rev_induct)
   3.646 +    apply simp
   3.647 +    apply (simp add: split_paired_all supp_eqvt)
   3.648 +    apply (drule perm_mem_left)
   3.649 +    apply (simp add: calc_atm split: split_if_asm)
   3.650 +    apply (auto dest: perm_mem_right)
   3.651 +    done
   3.652 +qed
   3.653 +
   3.654 +lemma abs_pat_alpha':
   3.655 +  assumes eq: "(\<lambda>[p]. t) = (\<lambda>[q]. u)"
   3.656 +  and ty: "pat_type p = pat_type q"
   3.657 +  and pv: "distinct (pat_vars p)"
   3.658 +  and qv: "distinct (pat_vars q)"
   3.659 +  shows "\<exists>pi::name prm. p = pi \<bullet> q \<and> t = pi \<bullet> u \<and>
   3.660 +    set pi \<subseteq> (supp p \<union> supp q) \<times> (supp p \<union> supp q)"
   3.661 +  using assms
   3.662 +proof (induct p arbitrary: q t u \<Delta>)
   3.663 +  case (PVar x T)
   3.664 +  note PVar' = this
   3.665 +  show ?case
   3.666 +  proof (cases q)
   3.667 +    case (PVar x' T')
   3.668 +    with `(\<lambda>[PVar x T]. t) = (\<lambda>[q]. u)`
   3.669 +    have "x = x' \<and> t = u \<or> x \<noteq> x' \<and> t = [(x, x')] \<bullet> u \<and> x \<sharp> u"
   3.670 +      by (simp add: btrm.inject alpha)
   3.671 +    then show ?thesis
   3.672 +    proof
   3.673 +      assume "x = x' \<and> t = u"
   3.674 +      with PVar PVar' have "PVar x T = ([]::name prm) \<bullet> q \<and>
   3.675 +	t = ([]::name prm) \<bullet> u \<and>
   3.676 +	set ([]::name prm) \<subseteq> (supp (PVar x T) \<union> supp q) \<times>
   3.677 +          (supp (PVar x T) \<union> supp q)" by simp
   3.678 +      then show ?thesis ..
   3.679 +    next
   3.680 +      assume "x \<noteq> x' \<and> t = [(x, x')] \<bullet> u \<and> x \<sharp> u"
   3.681 +      with PVar PVar' have "PVar x T = [(x, x')] \<bullet> q \<and>
   3.682 +	t = [(x, x')] \<bullet> u \<and>
   3.683 +	set [(x, x')] \<subseteq> (supp (PVar x T) \<union> supp q) \<times>
   3.684 +          (supp (PVar x T) \<union> supp q)"
   3.685 +	by (simp add: perm_swap swap_simps supp_atm perm_type)
   3.686 +      then show ?thesis ..
   3.687 +    qed
   3.688 +  next
   3.689 +    case (PTuple p\<^isub>1 p\<^isub>2)
   3.690 +    with PVar have "ty_size (pat_type p\<^isub>1) < ty_size T" by simp
   3.691 +    then have "Bind T x t \<noteq> (\<lambda>[p\<^isub>1]. \<lambda>[p\<^isub>2]. u)"
   3.692 +      by (rule bind_tuple_ineq)
   3.693 +    moreover from PTuple PVar
   3.694 +    have "Bind T x t = (\<lambda>[p\<^isub>1]. \<lambda>[p\<^isub>2]. u)" by simp
   3.695 +    ultimately show ?thesis ..
   3.696 +  qed
   3.697 +next
   3.698 +  case (PTuple p\<^isub>1 p\<^isub>2)
   3.699 +  note PTuple' = this
   3.700 +  show ?case
   3.701 +  proof (cases q)
   3.702 +    case (PVar x T)
   3.703 +    with PTuple have "ty_size (pat_type p\<^isub>1) < ty_size T" by auto
   3.704 +    then have "Bind T x u \<noteq> (\<lambda>[p\<^isub>1]. \<lambda>[p\<^isub>2]. t)"
   3.705 +      by (rule bind_tuple_ineq)
   3.706 +    moreover from PTuple PVar
   3.707 +    have "Bind T x u = (\<lambda>[p\<^isub>1]. \<lambda>[p\<^isub>2]. t)" by simp
   3.708 +    ultimately show ?thesis ..
   3.709 +  next
   3.710 +    case (PTuple p\<^isub>1' p\<^isub>2')
   3.711 +    with PTuple' have "(\<lambda>[p\<^isub>1]. \<lambda>[p\<^isub>2]. t) = (\<lambda>[p\<^isub>1']. \<lambda>[p\<^isub>2']. u)" by simp
   3.712 +    moreover from PTuple PTuple' have "pat_type p\<^isub>1 = pat_type p\<^isub>1'"
   3.713 +      by (simp add: ty.inject)
   3.714 +    moreover from PTuple' have "distinct (pat_vars p\<^isub>1)" by simp
   3.715 +    moreover from PTuple PTuple' have "distinct (pat_vars p\<^isub>1')" by simp
   3.716 +    ultimately have "\<exists>pi::name prm. p\<^isub>1 = pi \<bullet> p\<^isub>1' \<and>
   3.717 +      (\<lambda>[p\<^isub>2]. t) = pi \<bullet> (\<lambda>[p\<^isub>2']. u) \<and>
   3.718 +      set pi \<subseteq> (supp p\<^isub>1 \<union> supp p\<^isub>1') \<times> (supp p\<^isub>1 \<union> supp p\<^isub>1')"
   3.719 +      by (rule PTuple')
   3.720 +    then obtain pi::"name prm" where
   3.721 +      "p\<^isub>1 = pi \<bullet> p\<^isub>1'" "(\<lambda>[p\<^isub>2]. t) = pi \<bullet> (\<lambda>[p\<^isub>2']. u)" and
   3.722 +      pi: "set pi \<subseteq> (supp p\<^isub>1 \<union> supp p\<^isub>1') \<times> (supp p\<^isub>1 \<union> supp p\<^isub>1')" by auto
   3.723 +    from `(\<lambda>[p\<^isub>2]. t) = pi \<bullet> (\<lambda>[p\<^isub>2']. u)`
   3.724 +    have "(\<lambda>[p\<^isub>2]. t) = (\<lambda>[pi \<bullet> p\<^isub>2']. pi \<bullet> u)"
   3.725 +      by (simp add: eqvts)
   3.726 +    moreover from PTuple PTuple' have "pat_type p\<^isub>2 = pat_type (pi \<bullet> p\<^isub>2')"
   3.727 +      by (simp add: ty.inject pat_type_perm_eq)
   3.728 +    moreover from PTuple' have "distinct (pat_vars p\<^isub>2)" by simp
   3.729 +    moreover from PTuple PTuple' have "distinct (pat_vars (pi \<bullet> p\<^isub>2'))"
   3.730 +      by (simp add: pat_vars_eqvt [symmetric] distinct_eqvt [symmetric])
   3.731 +    ultimately have "\<exists>pi'::name prm. p\<^isub>2 = pi' \<bullet> pi \<bullet> p\<^isub>2' \<and>
   3.732 +      t = pi' \<bullet> pi \<bullet> u \<and>
   3.733 +      set pi' \<subseteq> (supp p\<^isub>2 \<union> supp (pi \<bullet> p\<^isub>2')) \<times> (supp p\<^isub>2 \<union> supp (pi \<bullet> p\<^isub>2'))"
   3.734 +      by (rule PTuple')
   3.735 +    then obtain pi'::"name prm" where
   3.736 +      "p\<^isub>2 = pi' \<bullet> pi \<bullet> p\<^isub>2'" "t = pi' \<bullet> pi \<bullet> u" and
   3.737 +      pi': "set pi' \<subseteq> (supp p\<^isub>2 \<union> supp (pi \<bullet> p\<^isub>2')) \<times>
   3.738 +        (supp p\<^isub>2 \<union> supp (pi \<bullet> p\<^isub>2'))" by auto
   3.739 +    from PTuple PTuple' have "pi \<bullet> distinct (pat_vars \<langle>\<langle>p\<^isub>1', p\<^isub>2'\<rangle>\<rangle>)" by simp
   3.740 +    then have "distinct (pat_vars \<langle>\<langle>pi \<bullet> p\<^isub>1', pi \<bullet> p\<^isub>2'\<rangle>\<rangle>)" by (simp only: eqvts)
   3.741 +    with `p\<^isub>1 = pi \<bullet> p\<^isub>1'` PTuple'
   3.742 +    have fresh: "(supp p\<^isub>2 \<union> supp (pi \<bullet> p\<^isub>2') :: name set) \<sharp>* p\<^isub>1"
   3.743 +      by (auto simp add: set_pat_vars_supp fresh_star_def fresh_def eqvts)
   3.744 +    from `p\<^isub>1 = pi \<bullet> p\<^isub>1'` have "pi' \<bullet> (p\<^isub>1 = pi \<bullet> p\<^isub>1')" by (rule perm_boolI)
   3.745 +    with pt_freshs_freshs [OF pt_name_inst at_name_inst pi' fresh fresh]
   3.746 +    have "p\<^isub>1 = pi' \<bullet> pi \<bullet> p\<^isub>1'" by (simp add: eqvts)
   3.747 +    with `p\<^isub>2 = pi' \<bullet> pi \<bullet> p\<^isub>2'` have "\<langle>\<langle>p\<^isub>1, p\<^isub>2\<rangle>\<rangle> = (pi' @ pi) \<bullet> \<langle>\<langle>p\<^isub>1', p\<^isub>2'\<rangle>\<rangle>"
   3.748 +      by (simp add: pt_name2)
   3.749 +    moreover
   3.750 +    have "((supp p\<^isub>2 \<union> (pi \<bullet> supp p\<^isub>2')) \<times> (supp p\<^isub>2 \<union> (pi \<bullet> supp p\<^isub>2'))::(name \<times> name) set) \<subseteq>
   3.751 +      (supp p\<^isub>2 \<union> (supp p\<^isub>1 \<union> supp p\<^isub>1' \<union> supp p\<^isub>2')) \<times> (supp p\<^isub>2 \<union> (supp p\<^isub>1 \<union> supp p\<^isub>1' \<union> supp p\<^isub>2'))"
   3.752 +      by (rule subset_refl Sigma_mono Un_mono perm_cases [OF pi])+
   3.753 +    with pi' have "set pi' \<subseteq> \<dots>" by (simp add: supp_eqvt [symmetric])
   3.754 +    with pi have "set (pi' @ pi) \<subseteq> (supp \<langle>\<langle>p\<^isub>1, p\<^isub>2\<rangle>\<rangle> \<union> supp \<langle>\<langle>p\<^isub>1', p\<^isub>2'\<rangle>\<rangle>) \<times>
   3.755 +      (supp \<langle>\<langle>p\<^isub>1, p\<^isub>2\<rangle>\<rangle> \<union> supp \<langle>\<langle>p\<^isub>1', p\<^isub>2'\<rangle>\<rangle>)"
   3.756 +      by (simp add: Sigma_Un_distrib1 Sigma_Un_distrib2 Un_ac) blast
   3.757 +    moreover note `t = pi' \<bullet> pi \<bullet> u`
   3.758 +    ultimately have "\<langle>\<langle>p\<^isub>1, p\<^isub>2\<rangle>\<rangle> = (pi' @ pi) \<bullet> q \<and> t = (pi' @ pi) \<bullet> u \<and>
   3.759 +      set (pi' @ pi) \<subseteq> (supp \<langle>\<langle>p\<^isub>1, p\<^isub>2\<rangle>\<rangle> \<union> supp q) \<times>
   3.760 +        (supp \<langle>\<langle>p\<^isub>1, p\<^isub>2\<rangle>\<rangle> \<union> supp q)" using PTuple
   3.761 +      by (simp add: pt_name2)
   3.762 +    then show ?thesis ..
   3.763 +  qed
   3.764 +qed
   3.765 +
   3.766 +lemma typing_case_Let:
   3.767 +  assumes ty: "\<Gamma> \<turnstile> (LET p = t IN u) : U"
   3.768 +  and fresh: "(supp p::name set) \<sharp>* \<Gamma>"
   3.769 +  and distinct: "distinct (pat_vars p)"
   3.770 +  and R: "\<And>T \<Delta>. \<Gamma> \<turnstile> t : T \<Longrightarrow> \<turnstile> p : T \<Rightarrow> \<Delta> \<Longrightarrow> \<Delta> @ \<Gamma> \<turnstile> u : U \<Longrightarrow> P"
   3.771 +  shows P using ty
   3.772 +proof cases
   3.773 +  case (Let p' t' \<Gamma>' T \<Delta> u' U')
   3.774 +  then have "(supp \<Delta>::name set) \<sharp>* \<Gamma>"
   3.775 +    by (auto intro: valid_typing valid_app_freshs)
   3.776 +  with Let have "(supp p'::name set) \<sharp>* \<Gamma>"
   3.777 +    by (simp add: pat_var)
   3.778 +  with fresh have fresh': "(supp p \<union> supp p' :: name set) \<sharp>* \<Gamma>"
   3.779 +    by (auto simp add: fresh_star_def)
   3.780 +  from Let have "(\<lambda>[p]. Base u) = (\<lambda>[p']. Base u')"
   3.781 +    by (simp add: trm.inject)
   3.782 +  moreover from Let have "pat_type p = pat_type p'"
   3.783 +    by (simp add: trm.inject)
   3.784 +  moreover note distinct
   3.785 +  moreover from `\<Delta> @ \<Gamma>' \<turnstile> u' : U'` have "valid (\<Delta> @ \<Gamma>')"
   3.786 +    by (rule valid_typing)
   3.787 +  then have "valid \<Delta>" by (rule valid_appD)
   3.788 +  with `\<turnstile> p' : T \<Rightarrow> \<Delta>` have "distinct (pat_vars p')"
   3.789 +    by (simp add: valid_distinct pat_vars_ptyping)
   3.790 +  ultimately have "\<exists>pi::name prm. p = pi \<bullet> p' \<and> Base u = pi \<bullet> Base u' \<and>
   3.791 +    set pi \<subseteq> (supp p \<union> supp p') \<times> (supp p \<union> supp p')"
   3.792 +    by (rule abs_pat_alpha')
   3.793 +  then obtain pi::"name prm" where pi: "p = pi \<bullet> p'" "u = pi \<bullet> u'"
   3.794 +    and pi': "set pi \<subseteq> (supp p \<union> supp p') \<times> (supp p \<union> supp p')"
   3.795 +    by (auto simp add: btrm.inject)
   3.796 +  from Let have "\<Gamma> \<turnstile> t : T" by (simp add: trm.inject)
   3.797 +  moreover from `\<turnstile> p' : T \<Rightarrow> \<Delta>` have "\<turnstile> (pi \<bullet> p') : (pi \<bullet> T) \<Rightarrow> (pi \<bullet> \<Delta>)"
   3.798 +    by (simp add: ptyping.eqvt)
   3.799 +  with pi have "\<turnstile> p : T \<Rightarrow> (pi \<bullet> \<Delta>)" by (simp add: perm_type)
   3.800 +  moreover from Let
   3.801 +  have "(pi \<bullet> \<Delta>) @ (pi \<bullet> \<Gamma>) \<turnstile> (pi \<bullet> u') : (pi \<bullet> U)"
   3.802 +    by (simp add: append_eqvt [symmetric] typing.eqvt)
   3.803 +  with pi have "(pi \<bullet> \<Delta>) @ \<Gamma> \<turnstile> u : U"
   3.804 +    by (simp add: perm_type pt_freshs_freshs
   3.805 +      [OF pt_name_inst at_name_inst pi' fresh' fresh'])
   3.806 +  ultimately show ?thesis by (rule R)
   3.807 +qed simp_all
   3.808 +
   3.809 +lemma preservation:
   3.810 +  assumes "t \<longmapsto> t'" and "\<Gamma> \<turnstile> t : T"
   3.811 +  shows "\<Gamma> \<turnstile> t' : T" using assms
   3.812 +proof (nominal_induct avoiding: \<Gamma> T rule: eval.strong_induct)
   3.813 +  case (TupleL t t' u)
   3.814 +  from `\<Gamma> \<turnstile> \<langle>t, u\<rangle> : T` obtain T\<^isub>1 T\<^isub>2
   3.815 +    where "T = T\<^isub>1 \<otimes> T\<^isub>2" "\<Gamma> \<turnstile> t : T\<^isub>1" "\<Gamma> \<turnstile> u : T\<^isub>2"
   3.816 +    by cases (simp_all add: trm.inject)
   3.817 +  from `\<Gamma> \<turnstile> t : T\<^isub>1` have "\<Gamma> \<turnstile> t' : T\<^isub>1" by (rule TupleL)
   3.818 +  then have "\<Gamma> \<turnstile> \<langle>t', u\<rangle> : T\<^isub>1 \<otimes> T\<^isub>2" using `\<Gamma> \<turnstile> u : T\<^isub>2`
   3.819 +    by (rule Tuple)
   3.820 +  with `T = T\<^isub>1 \<otimes> T\<^isub>2` show ?case by simp
   3.821 +next
   3.822 +  case (TupleR u u' t)
   3.823 +  from `\<Gamma> \<turnstile> \<langle>t, u\<rangle> : T` obtain T\<^isub>1 T\<^isub>2
   3.824 +    where "T = T\<^isub>1 \<otimes> T\<^isub>2" "\<Gamma> \<turnstile> t : T\<^isub>1" "\<Gamma> \<turnstile> u : T\<^isub>2"
   3.825 +    by cases (simp_all add: trm.inject)
   3.826 +  from `\<Gamma> \<turnstile> u : T\<^isub>2` have "\<Gamma> \<turnstile> u' : T\<^isub>2" by (rule TupleR)
   3.827 +  with `\<Gamma> \<turnstile> t : T\<^isub>1` have "\<Gamma> \<turnstile> \<langle>t, u'\<rangle> : T\<^isub>1 \<otimes> T\<^isub>2"
   3.828 +    by (rule Tuple)
   3.829 +  with `T = T\<^isub>1 \<otimes> T\<^isub>2` show ?case by simp
   3.830 +next
   3.831 +  case (Abs t t' x S)
   3.832 +  from `\<Gamma> \<turnstile> (\<lambda>x:S. t) : T` `x \<sharp> \<Gamma>` obtain U where
   3.833 +    T: "T = S \<rightarrow> U" and U: "(x, S) # \<Gamma> \<turnstile> t : U"
   3.834 +    by (rule typing_case_Abs)
   3.835 +  from U have "(x, S) # \<Gamma> \<turnstile> t' : U" by (rule Abs)
   3.836 +  then have "\<Gamma> \<turnstile> (\<lambda>x:S. t') : S \<rightarrow> U"
   3.837 +    by (rule typing.Abs)
   3.838 +  with T show ?case by simp
   3.839 +next
   3.840 +  case (Beta x u S t)
   3.841 +  from `\<Gamma> \<turnstile> (\<lambda>x:S. t) \<cdot> u : T` `x \<sharp> \<Gamma>`
   3.842 +  obtain "(x, S) # \<Gamma> \<turnstile> t : T" and "\<Gamma> \<turnstile> u : S"
   3.843 +    by cases (auto simp add: trm.inject ty.inject elim: typing_case_Abs)
   3.844 +  then show ?case by (rule subst_type)
   3.845 +next
   3.846 +  case (Let p t \<theta> u)
   3.847 +  from `\<Gamma> \<turnstile> (LET p = t IN u) : T` `supp p \<sharp>* \<Gamma>` `distinct (pat_vars p)`
   3.848 +  obtain U \<Delta> where "\<turnstile> p : U \<Rightarrow> \<Delta>" "\<Gamma> \<turnstile> t : U" "\<Delta> @ \<Gamma> \<turnstile> u : T"
   3.849 +    by (rule typing_case_Let)
   3.850 +  then show ?case using `\<turnstile> p \<rhd> t \<Rightarrow> \<theta>` `supp p \<sharp>* t`
   3.851 +    by (rule match_type)
   3.852 +next
   3.853 +  case (AppL t t' u)
   3.854 +  from `\<Gamma> \<turnstile> t \<cdot> u : T` obtain U where
   3.855 +    t: "\<Gamma> \<turnstile> t : U \<rightarrow> T" and u: "\<Gamma> \<turnstile> u : U"
   3.856 +    by cases (auto simp add: trm.inject)
   3.857 +  from t have "\<Gamma> \<turnstile> t' : U \<rightarrow> T" by (rule AppL)
   3.858 +  then show ?case using u by (rule typing.App)
   3.859 +next
   3.860 +  case (AppR u u' t)
   3.861 +  from `\<Gamma> \<turnstile> t \<cdot> u : T` obtain U where
   3.862 +    t: "\<Gamma> \<turnstile> t : U \<rightarrow> T" and u: "\<Gamma> \<turnstile> u : U"
   3.863 +    by cases (auto simp add: trm.inject)
   3.864 +  from u have "\<Gamma> \<turnstile> u' : U" by (rule AppR)
   3.865 +  with t show ?case by (rule typing.App)
   3.866 +qed
   3.867 +
   3.868 +end