src/HOL/Nominal/Examples/Pattern.thy
author wenzelm
Mon Aug 31 21:01:21 2015 +0200 (2015-08-31)
changeset 61069 aefe89038dd2
parent 60580 7e741e22d7fc
child 61166 5976fe402824
permissions -rw-r--r--
prefer symbols;
     1 section {* Simply-typed lambda-calculus with let and tuple patterns *}
     2 
     3 theory Pattern
     4 imports "../Nominal"
     5 begin
     6 
     7 no_syntax
     8   "_Map" :: "maplets => 'a \<rightharpoonup> 'b"  ("(1[_])")
     9 
    10 atom_decl name
    11 
    12 nominal_datatype ty =
    13     Atom nat
    14   | Arrow ty ty  (infixr "\<rightarrow>" 200)
    15   | TupleT ty ty  (infixr "\<otimes>" 210)
    16 
    17 lemma fresh_type [simp]: "(a::name) \<sharp> (T::ty)"
    18   by (induct T rule: ty.induct) (simp_all add: fresh_nat)
    19 
    20 lemma supp_type [simp]: "supp (T::ty) = ({} :: name set)"
    21   by (induct T rule: ty.induct) (simp_all add: ty.supp supp_nat)
    22 
    23 lemma perm_type: "(pi::name prm) \<bullet> (T::ty) = T"
    24   by (induct T rule: ty.induct) (simp_all add: perm_nat_def)
    25 
    26 nominal_datatype trm =
    27     Var name
    28   | Tuple trm trm  ("(1'\<langle>_,/ _'\<rangle>)")
    29   | Abs ty "\<guillemotleft>name\<guillemotright>trm"
    30   | App trm trm  (infixl "\<cdot>" 200)
    31   | Let ty trm btrm
    32 and btrm =
    33     Base trm
    34   | Bind ty "\<guillemotleft>name\<guillemotright>btrm"
    35 
    36 abbreviation
    37   Abs_syn :: "name \<Rightarrow> ty \<Rightarrow> trm \<Rightarrow> trm"  ("(3\<lambda>_:_./ _)" [0, 0, 10] 10) 
    38 where
    39   "\<lambda>x:T. t \<equiv> Abs T x t"
    40 
    41 datatype pat =
    42     PVar name ty
    43   | PTuple pat pat  ("(1'\<langle>\<langle>_,/ _'\<rangle>\<rangle>)")
    44 
    45 (* FIXME: The following should be done automatically by the nominal package *)
    46 overloading pat_perm \<equiv> "perm :: name prm \<Rightarrow> pat \<Rightarrow> pat" (unchecked)
    47 begin
    48 
    49 primrec pat_perm
    50 where
    51   "pat_perm pi (PVar x ty) = PVar (pi \<bullet> x) (pi \<bullet> ty)"
    52 | "pat_perm pi \<langle>\<langle>p, q\<rangle>\<rangle> = \<langle>\<langle>pat_perm pi p, pat_perm pi q\<rangle>\<rangle>"
    53 
    54 end
    55 
    56 declare pat_perm.simps [eqvt]
    57 
    58 lemma supp_PVar [simp]: "((supp (PVar x T))::name set) = supp x"
    59   by (simp add: supp_def perm_fresh_fresh)
    60 
    61 lemma supp_PTuple [simp]: "((supp \<langle>\<langle>p, q\<rangle>\<rangle>)::name set) = supp p \<union> supp q"
    62   by (simp add: supp_def Collect_disj_eq del: disj_not1)
    63 
    64 instance pat :: pt_name
    65 proof (default, goals)
    66   case (1 x)
    67   show ?case by (induct x) simp_all
    68 next
    69   case (2 _ _ x)
    70   show ?case by (induct x) (simp_all add: pt_name2)
    71 next
    72   case (3 _ _ x)
    73   then show ?case by (induct x) (simp_all add: pt_name3)
    74 qed
    75 
    76 instance pat :: fs_name
    77 proof (default, goals)
    78   case (1 x)
    79   show ?case by (induct x) (simp_all add: fin_supp)
    80 qed
    81 
    82 (* the following function cannot be defined using nominal_primrec, *)
    83 (* since variable parameters are currently not allowed.            *)
    84 primrec abs_pat :: "pat \<Rightarrow> btrm \<Rightarrow> btrm" ("(3\<lambda>[_]./ _)" [0, 10] 10)
    85 where
    86   "(\<lambda>[PVar x T]. t) = Bind T x t"
    87 | "(\<lambda>[\<langle>\<langle>p, q\<rangle>\<rangle>]. t) = (\<lambda>[p]. \<lambda>[q]. t)"
    88 
    89 lemma abs_pat_eqvt [eqvt]:
    90   "(pi :: name prm) \<bullet> (\<lambda>[p]. t) = (\<lambda>[pi \<bullet> p]. (pi \<bullet> t))"
    91   by (induct p arbitrary: t) simp_all
    92 
    93 lemma abs_pat_fresh [simp]:
    94   "(x::name) \<sharp> (\<lambda>[p]. t) = (x \<in> supp p \<or> x \<sharp> t)"
    95   by (induct p arbitrary: t) (simp_all add: abs_fresh supp_atm)
    96 
    97 lemma abs_pat_alpha:
    98   assumes fresh: "((pi::name prm) \<bullet> supp p::name set) \<sharp>* t"
    99   and pi: "set pi \<subseteq> supp p \<times> pi \<bullet> supp p"
   100   shows "(\<lambda>[p]. t) = (\<lambda>[pi \<bullet> p]. pi \<bullet> t)"
   101 proof -
   102   note pt_name_inst at_name_inst pi
   103   moreover have "(supp p::name set) \<sharp>* (\<lambda>[p]. t)"
   104     by (simp add: fresh_star_def)
   105   moreover from fresh
   106   have "(pi \<bullet> supp p::name set) \<sharp>* (\<lambda>[p]. t)"
   107     by (simp add: fresh_star_def)
   108   ultimately have "pi \<bullet> (\<lambda>[p]. t) = (\<lambda>[p]. t)"
   109     by (rule pt_freshs_freshs)
   110   then show ?thesis by (simp add: eqvts)
   111 qed
   112 
   113 primrec pat_vars :: "pat \<Rightarrow> name list"
   114 where
   115   "pat_vars (PVar x T) = [x]"
   116 | "pat_vars \<langle>\<langle>p, q\<rangle>\<rangle> = pat_vars q @ pat_vars p"
   117 
   118 lemma pat_vars_eqvt [eqvt]:
   119   "(pi :: name prm) \<bullet> (pat_vars p) = pat_vars (pi \<bullet> p)"
   120   by (induct p rule: pat.induct) (simp_all add: eqvts)
   121 
   122 lemma set_pat_vars_supp: "set (pat_vars p) = supp p"
   123   by (induct p) (auto simp add: supp_atm)
   124 
   125 lemma distinct_eqvt [eqvt]:
   126   "(pi :: name prm) \<bullet> (distinct (xs::name list)) = distinct (pi \<bullet> xs)"
   127   by (induct xs) (simp_all add: eqvts)
   128 
   129 primrec pat_type :: "pat \<Rightarrow> ty"
   130 where
   131   "pat_type (PVar x T) = T"
   132 | "pat_type \<langle>\<langle>p, q\<rangle>\<rangle> = pat_type p \<otimes> pat_type q"
   133 
   134 lemma pat_type_eqvt [eqvt]:
   135   "(pi :: name prm) \<bullet> (pat_type p) = pat_type (pi \<bullet> p)"
   136   by (induct p) simp_all
   137 
   138 lemma pat_type_perm_eq: "pat_type ((pi :: name prm) \<bullet> p) = pat_type p"
   139   by (induct p) (simp_all add: perm_type)
   140 
   141 type_synonym ctx = "(name \<times> ty) list"
   142 
   143 inductive
   144   ptyping :: "pat \<Rightarrow> ty \<Rightarrow> ctx \<Rightarrow> bool"  ("\<turnstile> _ : _ \<Rightarrow> _" [60, 60, 60] 60)
   145 where
   146   PVar: "\<turnstile> PVar x T : T \<Rightarrow> [(x, T)]"
   147 | PTuple: "\<turnstile> p : T \<Rightarrow> \<Delta>\<^sub>1 \<Longrightarrow> \<turnstile> q : U \<Rightarrow> \<Delta>\<^sub>2 \<Longrightarrow> \<turnstile> \<langle>\<langle>p, q\<rangle>\<rangle> : T \<otimes> U \<Rightarrow> \<Delta>\<^sub>2 @ \<Delta>\<^sub>1"
   148 
   149 lemma pat_vars_ptyping:
   150   assumes "\<turnstile> p : T \<Rightarrow> \<Delta>"
   151   shows "pat_vars p = map fst \<Delta>" using assms
   152   by induct simp_all
   153 
   154 inductive
   155   valid :: "ctx \<Rightarrow> bool"
   156 where
   157   Nil [intro!]: "valid []"
   158 | Cons [intro!]: "valid \<Gamma> \<Longrightarrow> x \<sharp> \<Gamma> \<Longrightarrow> valid ((x, T) # \<Gamma>)"
   159 
   160 inductive_cases validE[elim!]: "valid ((x, T) # \<Gamma>)"
   161 
   162 lemma fresh_ctxt_set_eq: "((x::name) \<sharp> (\<Gamma>::ctx)) = (x \<notin> fst ` set \<Gamma>)"
   163   by (induct \<Gamma>) (auto simp add: fresh_list_nil fresh_list_cons fresh_prod fresh_atm)
   164 
   165 lemma valid_distinct: "valid \<Gamma> = distinct (map fst \<Gamma>)"
   166   by (induct \<Gamma>) (auto simp add: fresh_ctxt_set_eq [symmetric])
   167 
   168 abbreviation
   169   "sub_ctx" :: "ctx \<Rightarrow> ctx \<Rightarrow> bool" ("_ \<sqsubseteq> _") 
   170 where
   171   "\<Gamma>\<^sub>1 \<sqsubseteq> \<Gamma>\<^sub>2 \<equiv> \<forall>x. x \<in> set \<Gamma>\<^sub>1 \<longrightarrow> x \<in> set \<Gamma>\<^sub>2"
   172 
   173 abbreviation
   174   Let_syn :: "pat \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm"  ("(LET (_ =/ _)/ IN (_))" 10)
   175 where
   176   "LET p = t IN u \<equiv> Let (pat_type p) t (\<lambda>[p]. Base u)"
   177 
   178 inductive typing :: "ctx \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60, 60, 60] 60)
   179 where
   180   Var [intro]: "valid \<Gamma> \<Longrightarrow> (x, T) \<in> set \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
   181 | Tuple [intro]: "\<Gamma> \<turnstile> t : T \<Longrightarrow> \<Gamma> \<turnstile> u : U \<Longrightarrow> \<Gamma> \<turnstile> \<langle>t, u\<rangle> : T \<otimes> U"
   182 | Abs [intro]: "(x, T) # \<Gamma> \<turnstile> t : U \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda>x:T. t) : T \<rightarrow> U"
   183 | App [intro]: "\<Gamma> \<turnstile> t : T \<rightarrow> U \<Longrightarrow> \<Gamma> \<turnstile> u : T \<Longrightarrow> \<Gamma> \<turnstile> t \<cdot> u : U"
   184 | Let: "((supp p)::name set) \<sharp>* t \<Longrightarrow>
   185     \<Gamma> \<turnstile> t : T \<Longrightarrow> \<turnstile> p : T \<Rightarrow> \<Delta> \<Longrightarrow> \<Delta> @ \<Gamma> \<turnstile> u : U \<Longrightarrow>
   186     \<Gamma> \<turnstile> (LET p = t IN u) : U"
   187 
   188 equivariance ptyping
   189 
   190 equivariance valid
   191 
   192 equivariance typing
   193 
   194 lemma valid_typing:
   195   assumes "\<Gamma> \<turnstile> t : T"
   196   shows "valid \<Gamma>" using assms
   197   by induct auto
   198 
   199 lemma pat_var:
   200   assumes "\<turnstile> p : T \<Rightarrow> \<Delta>"
   201   shows "(supp p::name set) = supp \<Delta>" using assms
   202   by induct (auto simp add: supp_list_nil supp_list_cons supp_prod supp_list_append)
   203 
   204 lemma valid_app_fresh:
   205   assumes "valid (\<Delta> @ \<Gamma>)" and "(x::name) \<in> supp \<Delta>"
   206   shows "x \<sharp> \<Gamma>" using assms
   207   by (induct \<Delta>)
   208     (auto simp add: supp_list_nil supp_list_cons supp_prod supp_atm fresh_list_append)
   209 
   210 lemma pat_freshs:
   211   assumes "\<turnstile> p : T \<Rightarrow> \<Delta>"
   212   shows "(supp p::name set) \<sharp>* c = (supp \<Delta>::name set) \<sharp>* c" using assms
   213   by (auto simp add: fresh_star_def pat_var)
   214 
   215 lemma valid_app_mono:
   216   assumes "valid (\<Delta> @ \<Gamma>\<^sub>1)" and "(supp \<Delta>::name set) \<sharp>* \<Gamma>\<^sub>2" and "valid \<Gamma>\<^sub>2" and "\<Gamma>\<^sub>1 \<sqsubseteq> \<Gamma>\<^sub>2"
   217   shows "valid (\<Delta> @ \<Gamma>\<^sub>2)" using assms
   218   by (induct \<Delta>)
   219     (auto simp add: supp_list_cons fresh_star_Un_elim supp_prod
   220        fresh_list_append supp_atm fresh_star_insert_elim fresh_star_empty_elim)
   221 
   222 nominal_inductive2 typing
   223 avoids
   224   Abs: "{x}"
   225 | Let: "(supp p)::name set"
   226   by (auto simp add: fresh_star_def abs_fresh fin_supp pat_var
   227     dest!: valid_typing valid_app_fresh)
   228 
   229 lemma better_T_Let [intro]:
   230   assumes t: "\<Gamma> \<turnstile> t : T" and p: "\<turnstile> p : T \<Rightarrow> \<Delta>" and u: "\<Delta> @ \<Gamma> \<turnstile> u : U"
   231   shows "\<Gamma> \<turnstile> (LET p = t IN u) : U"
   232 proof -
   233   obtain pi::"name prm" where pi: "(pi \<bullet> (supp p::name set)) \<sharp>* (t, Base u, \<Gamma>)"
   234     and pi': "set pi \<subseteq> supp p \<times> (pi \<bullet> supp p)"
   235     by (rule at_set_avoiding [OF at_name_inst fin_supp fin_supp])
   236   from p u have p_fresh: "(supp p::name set) \<sharp>* \<Gamma>"
   237     by (auto simp add: fresh_star_def pat_var dest!: valid_typing valid_app_fresh)
   238   from pi have p_fresh': "(pi \<bullet> (supp p::name set)) \<sharp>* \<Gamma>"
   239     by (simp add: fresh_star_prod_elim)
   240   from pi have p_fresh'': "(pi \<bullet> (supp p::name set)) \<sharp>* Base u"
   241     by (simp add: fresh_star_prod_elim)
   242   from pi have "(supp (pi \<bullet> p)::name set) \<sharp>* t"
   243     by (simp add: fresh_star_prod_elim eqvts)
   244   moreover note t
   245   moreover from p have "pi \<bullet> (\<turnstile> p : T \<Rightarrow> \<Delta>)" by (rule perm_boolI)
   246   then have "\<turnstile> (pi \<bullet> p) : T \<Rightarrow> (pi \<bullet> \<Delta>)" by (simp add: eqvts perm_type)
   247   moreover from u have "pi \<bullet> (\<Delta> @ \<Gamma> \<turnstile> u : U)" by (rule perm_boolI)
   248   with pt_freshs_freshs [OF pt_name_inst at_name_inst pi' p_fresh p_fresh']
   249   have "(pi \<bullet> \<Delta>) @ \<Gamma> \<turnstile> (pi \<bullet> u) : U" by (simp add: eqvts perm_type)
   250   ultimately have "\<Gamma> \<turnstile> (LET (pi \<bullet> p) = t IN (pi \<bullet> u)) : U"
   251     by (rule Let)
   252   then show ?thesis by (simp add: abs_pat_alpha [OF p_fresh'' pi'] pat_type_perm_eq)
   253 qed
   254 
   255 lemma weakening: 
   256   assumes "\<Gamma>\<^sub>1 \<turnstile> t : T" and "valid \<Gamma>\<^sub>2" and "\<Gamma>\<^sub>1 \<sqsubseteq> \<Gamma>\<^sub>2"
   257   shows "\<Gamma>\<^sub>2 \<turnstile> t : T" using assms
   258   apply (nominal_induct \<Gamma>\<^sub>1 t T avoiding: \<Gamma>\<^sub>2 rule: typing.strong_induct)
   259   apply auto
   260   apply (drule_tac x="(x, T) # \<Gamma>\<^sub>2" in meta_spec)
   261   apply (auto intro: valid_typing)
   262   apply (drule_tac x="\<Gamma>\<^sub>2" in meta_spec)
   263   apply (drule_tac x="\<Delta> @ \<Gamma>\<^sub>2" in meta_spec)
   264   apply (auto intro: valid_typing)
   265   apply (rule typing.Let)
   266   apply assumption+
   267   apply (drule meta_mp)
   268   apply (rule valid_app_mono)
   269   apply (rule valid_typing)
   270   apply assumption
   271   apply (auto simp add: pat_freshs)
   272   done
   273 
   274 inductive
   275   match :: "pat \<Rightarrow> trm \<Rightarrow> (name \<times> trm) list \<Rightarrow> bool"  ("\<turnstile> _ \<rhd> _ \<Rightarrow> _" [50, 50, 50] 50)
   276 where
   277   PVar: "\<turnstile> PVar x T \<rhd> t \<Rightarrow> [(x, t)]"
   278 | 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>'"
   279 
   280 fun
   281   lookup :: "(name \<times> trm) list \<Rightarrow> name \<Rightarrow> trm"   
   282 where
   283   "lookup [] x = Var x"
   284 | "lookup ((y, e) # \<theta>) x = (if x = y then e else lookup \<theta> x)"
   285 
   286 lemma lookup_eqvt[eqvt]:
   287   fixes pi :: "name prm"
   288   and   \<theta> :: "(name \<times> trm) list"
   289   and   X :: "name"
   290   shows "pi \<bullet> (lookup \<theta> X) = lookup (pi \<bullet> \<theta>) (pi \<bullet> X)"
   291   by (induct \<theta>) (auto simp add: eqvts)
   292  
   293 nominal_primrec
   294   psubst :: "(name \<times> trm) list \<Rightarrow> trm \<Rightarrow> trm"  ("_\<lparr>_\<rparr>" [95,0] 210)
   295   and psubstb :: "(name \<times> trm) list \<Rightarrow> btrm \<Rightarrow> btrm"  ("_\<lparr>_\<rparr>\<^sub>b" [95,0] 210)
   296 where
   297   "\<theta>\<lparr>Var x\<rparr> = (lookup \<theta> x)"
   298 | "\<theta>\<lparr>t \<cdot> u\<rparr> = \<theta>\<lparr>t\<rparr> \<cdot> \<theta>\<lparr>u\<rparr>"
   299 | "\<theta>\<lparr>\<langle>t, u\<rangle>\<rparr> = \<langle>\<theta>\<lparr>t\<rparr>, \<theta>\<lparr>u\<rparr>\<rangle>"
   300 | "\<theta>\<lparr>Let T t u\<rparr> = Let T (\<theta>\<lparr>t\<rparr>) (\<theta>\<lparr>u\<rparr>\<^sub>b)"
   301 | "x \<sharp> \<theta> \<Longrightarrow> \<theta>\<lparr>\<lambda>x:T. t\<rparr> = (\<lambda>x:T. \<theta>\<lparr>t\<rparr>)"
   302 | "\<theta>\<lparr>Base t\<rparr>\<^sub>b = Base (\<theta>\<lparr>t\<rparr>)"
   303 | "x \<sharp> \<theta> \<Longrightarrow> \<theta>\<lparr>Bind T x t\<rparr>\<^sub>b = Bind T x (\<theta>\<lparr>t\<rparr>\<^sub>b)"
   304   apply finite_guess+
   305   apply (simp add: abs_fresh | fresh_guess)+
   306   done
   307 
   308 lemma lookup_fresh:
   309   "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"
   310   apply (induct \<theta>)
   311   apply (simp_all add: split_paired_all fresh_atm)
   312   apply (case_tac "x = y")
   313   apply (auto simp add: fresh_atm)
   314   done
   315 
   316 lemma psubst_fresh:
   317   assumes "x \<in> set (map fst \<theta>)" and "\<forall>(y, t)\<in>set \<theta>. x \<sharp> t"
   318   shows "x \<sharp> \<theta>\<lparr>t\<rparr>" and "x \<sharp> \<theta>\<lparr>t'\<rparr>\<^sub>b" using assms
   319   apply (nominal_induct t and t' avoiding: \<theta> rule: trm_btrm.strong_inducts)
   320   apply simp
   321   apply (rule lookup_fresh)
   322   apply (rule impI)
   323   apply (simp_all add: abs_fresh)
   324   done
   325 
   326 lemma psubst_eqvt[eqvt]:
   327   fixes pi :: "name prm" 
   328   shows "pi \<bullet> (\<theta>\<lparr>t\<rparr>) = (pi \<bullet> \<theta>)\<lparr>pi \<bullet> t\<rparr>"
   329   and "pi \<bullet> (\<theta>\<lparr>t'\<rparr>\<^sub>b) = (pi \<bullet> \<theta>)\<lparr>pi \<bullet> t'\<rparr>\<^sub>b"
   330   by (nominal_induct t and t' avoiding: \<theta> rule: trm_btrm.strong_inducts)
   331     (simp_all add: eqvts fresh_bij)
   332 
   333 abbreviation 
   334   subst :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_[_\<mapsto>_]" [100,0,0] 100)
   335 where 
   336   "t[x\<mapsto>t'] \<equiv> [(x,t')]\<lparr>t\<rparr>"
   337 
   338 abbreviation 
   339   substb :: "btrm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> btrm" ("_[_\<mapsto>_]\<^sub>b" [100,0,0] 100)
   340 where 
   341   "t[x\<mapsto>t']\<^sub>b \<equiv> [(x,t')]\<lparr>t\<rparr>\<^sub>b"
   342 
   343 lemma lookup_forget:
   344   "(supp (map fst \<theta>)::name set) \<sharp>* x \<Longrightarrow> lookup \<theta> x = Var x"
   345   by (induct \<theta>) (auto simp add: split_paired_all fresh_star_def fresh_atm supp_list_cons supp_atm)
   346 
   347 lemma supp_fst: "(x::name) \<in> supp (map fst (\<theta>::(name \<times> trm) list)) \<Longrightarrow> x \<in> supp \<theta>"
   348   by (induct \<theta>) (auto simp add: supp_list_nil supp_list_cons supp_prod)
   349 
   350 lemma psubst_forget:
   351   "(supp (map fst \<theta>)::name set) \<sharp>* t \<Longrightarrow> \<theta>\<lparr>t\<rparr> = t"
   352   "(supp (map fst \<theta>)::name set) \<sharp>* t' \<Longrightarrow> \<theta>\<lparr>t'\<rparr>\<^sub>b = t'"
   353   apply (nominal_induct t and t' avoiding: \<theta> rule: trm_btrm.strong_inducts)
   354   apply (auto simp add: fresh_star_def lookup_forget abs_fresh)
   355   apply (drule_tac x=\<theta> in meta_spec)
   356   apply (drule meta_mp)
   357   apply (rule ballI)
   358   apply (drule_tac x=x in bspec)
   359   apply assumption
   360   apply (drule supp_fst)
   361   apply (auto simp add: fresh_def)
   362   apply (drule_tac x=\<theta> in meta_spec)
   363   apply (drule meta_mp)
   364   apply (rule ballI)
   365   apply (drule_tac x=x in bspec)
   366   apply assumption
   367   apply (drule supp_fst)
   368   apply (auto simp add: fresh_def)
   369   done
   370 
   371 lemma psubst_nil: "[]\<lparr>t\<rparr> = t" "[]\<lparr>t'\<rparr>\<^sub>b = t'"
   372   by (induct t and t' rule: trm_btrm.inducts) (simp_all add: fresh_list_nil)
   373 
   374 lemma psubst_cons:
   375   assumes "(supp (map fst \<theta>)::name set) \<sharp>* u"
   376   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"
   377   using assms
   378   by (nominal_induct t and t' avoiding: x u \<theta> rule: trm_btrm.strong_inducts)
   379     (simp_all add: fresh_list_nil fresh_list_cons psubst_forget)
   380 
   381 lemma psubst_append:
   382   "(supp (map fst (\<theta>\<^sub>1 @ \<theta>\<^sub>2))::name set) \<sharp>* map snd (\<theta>\<^sub>1 @ \<theta>\<^sub>2) \<Longrightarrow> (\<theta>\<^sub>1 @ \<theta>\<^sub>2)\<lparr>t\<rparr> = \<theta>\<^sub>2\<lparr>\<theta>\<^sub>1\<lparr>t\<rparr>\<rparr>"
   383   by (induct \<theta>\<^sub>1 arbitrary: t)
   384     (simp_all add: psubst_nil split_paired_all supp_list_cons psubst_cons fresh_star_def
   385       fresh_list_cons fresh_list_append supp_list_append)
   386 
   387 lemma abs_pat_psubst [simp]:
   388   "(supp p::name set) \<sharp>* \<theta> \<Longrightarrow> \<theta>\<lparr>\<lambda>[p]. t\<rparr>\<^sub>b = (\<lambda>[p]. \<theta>\<lparr>t\<rparr>\<^sub>b)"
   389   by (induct p arbitrary: t) (auto simp add: fresh_star_def supp_atm)
   390 
   391 lemma valid_insert:
   392   assumes "valid (\<Delta> @ [(x, T)] @ \<Gamma>)"
   393   shows "valid (\<Delta> @ \<Gamma>)" using assms
   394   by (induct \<Delta>)
   395     (auto simp add: fresh_list_append fresh_list_cons)
   396 
   397 lemma fresh_set: 
   398   shows "y \<sharp> xs = (\<forall>x\<in>set xs. y \<sharp> x)"
   399   by (induct xs) (simp_all add: fresh_list_nil fresh_list_cons)
   400 
   401 lemma context_unique:
   402   assumes "valid \<Gamma>"
   403   and "(x, T) \<in> set \<Gamma>"
   404   and "(x, U) \<in> set \<Gamma>"
   405   shows "T = U" using assms
   406   by induct (auto simp add: fresh_set fresh_prod fresh_atm)
   407 
   408 lemma subst_type_aux:
   409   assumes a: "\<Delta> @ [(x, U)] @ \<Gamma> \<turnstile> t : T"
   410   and b: "\<Gamma> \<turnstile> u : U"
   411   shows "\<Delta> @ \<Gamma> \<turnstile> t[x\<mapsto>u] : T" using a b
   412 proof (nominal_induct \<Gamma>'\<equiv>"\<Delta> @ [(x, U)] @ \<Gamma>" t T avoiding: x u \<Delta> rule: typing.strong_induct)
   413   case (Var y T x u \<Delta>)
   414   from `valid (\<Delta> @ [(x, U)] @ \<Gamma>)`
   415   have valid: "valid (\<Delta> @ \<Gamma>)" by (rule valid_insert)
   416   show "\<Delta> @ \<Gamma> \<turnstile> Var y[x\<mapsto>u] : T"
   417   proof cases
   418     assume eq: "x = y"
   419     from Var eq have "T = U" by (auto intro: context_unique)
   420     with Var eq valid show "\<Delta> @ \<Gamma> \<turnstile> Var y[x\<mapsto>u] : T" by (auto intro: weakening)
   421   next
   422     assume ineq: "x \<noteq> y"
   423     from Var ineq have "(y, T) \<in> set (\<Delta> @ \<Gamma>)" by simp
   424     then show "\<Delta> @ \<Gamma> \<turnstile> Var y[x\<mapsto>u] : T" using ineq valid by auto
   425   qed
   426 next
   427   case (Tuple t\<^sub>1 T\<^sub>1 t\<^sub>2 T\<^sub>2)
   428   from refl `\<Gamma> \<turnstile> u : U`
   429   have "\<Delta> @ \<Gamma> \<turnstile> t\<^sub>1[x\<mapsto>u] : T\<^sub>1" by (rule Tuple)
   430   moreover from refl `\<Gamma> \<turnstile> u : U`
   431   have "\<Delta> @ \<Gamma> \<turnstile> t\<^sub>2[x\<mapsto>u] : T\<^sub>2" by (rule Tuple)
   432   ultimately have "\<Delta> @ \<Gamma> \<turnstile> \<langle>t\<^sub>1[x\<mapsto>u], t\<^sub>2[x\<mapsto>u]\<rangle> : T\<^sub>1 \<otimes> T\<^sub>2" ..
   433   then show ?case by simp
   434 next
   435   case (Let p t T \<Delta>' s S)
   436   from refl `\<Gamma> \<turnstile> u : U`
   437   have "\<Delta> @ \<Gamma> \<turnstile> t[x\<mapsto>u] : T" by (rule Let)
   438   moreover note `\<turnstile> p : T \<Rightarrow> \<Delta>'`
   439   moreover have "\<Delta>' @ (\<Delta> @ [(x, U)] @ \<Gamma>) = (\<Delta>' @ \<Delta>) @ [(x, U)] @ \<Gamma>" by simp
   440   then have "(\<Delta>' @ \<Delta>) @ \<Gamma> \<turnstile> s[x\<mapsto>u] : S" using `\<Gamma> \<turnstile> u : U` by (rule Let)
   441   then have "\<Delta>' @ \<Delta> @ \<Gamma> \<turnstile> s[x\<mapsto>u] : S" by simp
   442   ultimately have "\<Delta> @ \<Gamma> \<turnstile> (LET p = t[x\<mapsto>u] IN s[x\<mapsto>u]) : S"
   443     by (rule better_T_Let)
   444   moreover from Let have "(supp p::name set) \<sharp>* [(x, u)]"
   445     by (simp add: fresh_star_def fresh_list_nil fresh_list_cons)
   446   ultimately show ?case by simp
   447 next
   448   case (Abs y T t S)
   449   have "(y, T) # \<Delta> @ [(x, U)] @ \<Gamma> = ((y, T) # \<Delta>) @ [(x, U)] @ \<Gamma>"
   450     by simp
   451   then have "((y, T) # \<Delta>) @ \<Gamma> \<turnstile> t[x\<mapsto>u] : S" using `\<Gamma> \<turnstile> u : U` by (rule Abs)
   452   then have "(y, T) # \<Delta> @ \<Gamma> \<turnstile> t[x\<mapsto>u] : S" by simp
   453   then have "\<Delta> @ \<Gamma> \<turnstile> (\<lambda>y:T. t[x\<mapsto>u]) : T \<rightarrow> S"
   454     by (rule typing.Abs)
   455   moreover from Abs have "y \<sharp> [(x, u)]"
   456     by (simp add: fresh_list_nil fresh_list_cons)
   457   ultimately show ?case by simp
   458 next
   459   case (App t\<^sub>1 T S t\<^sub>2)
   460   from refl `\<Gamma> \<turnstile> u : U`
   461   have "\<Delta> @ \<Gamma> \<turnstile> t\<^sub>1[x\<mapsto>u] : T \<rightarrow> S" by (rule App)
   462   moreover from refl `\<Gamma> \<turnstile> u : U`
   463   have "\<Delta> @ \<Gamma> \<turnstile> t\<^sub>2[x\<mapsto>u] : T" by (rule App)
   464   ultimately have "\<Delta> @ \<Gamma> \<turnstile> (t\<^sub>1[x\<mapsto>u]) \<cdot> (t\<^sub>2[x\<mapsto>u]) : S"
   465     by (rule typing.App)
   466   then show ?case by simp
   467 qed
   468 
   469 lemmas subst_type = subst_type_aux [of "[]", simplified]
   470 
   471 lemma match_supp_fst:
   472   assumes "\<turnstile> p \<rhd> u \<Rightarrow> \<theta>" shows "(supp (map fst \<theta>)::name set) = supp p" using assms
   473   by induct (simp_all add: supp_list_nil supp_list_cons supp_list_append)
   474 
   475 lemma match_supp_snd:
   476   assumes "\<turnstile> p \<rhd> u \<Rightarrow> \<theta>" shows "(supp (map snd \<theta>)::name set) = supp u" using assms
   477   by induct (simp_all add: supp_list_nil supp_list_cons supp_list_append trm.supp)
   478 
   479 lemma match_fresh: "\<turnstile> p \<rhd> u \<Rightarrow> \<theta> \<Longrightarrow> (supp p::name set) \<sharp>* u \<Longrightarrow>
   480   (supp (map fst \<theta>)::name set) \<sharp>* map snd \<theta>"
   481   by (simp add: fresh_star_def fresh_def match_supp_fst match_supp_snd)
   482 
   483 lemma match_type_aux:
   484   assumes "\<turnstile> p : U \<Rightarrow> \<Delta>"
   485   and "\<Gamma>\<^sub>2 \<turnstile> u : U"
   486   and "\<Gamma>\<^sub>1 @ \<Delta> @ \<Gamma>\<^sub>2 \<turnstile> t : T"
   487   and "\<turnstile> p \<rhd> u \<Rightarrow> \<theta>"
   488   and "(supp p::name set) \<sharp>* u"
   489   shows "\<Gamma>\<^sub>1 @ \<Gamma>\<^sub>2 \<turnstile> \<theta>\<lparr>t\<rparr> : T" using assms
   490 proof (induct arbitrary: \<Gamma>\<^sub>1 \<Gamma>\<^sub>2 t u T \<theta>)
   491   case (PVar x U)
   492   from `\<Gamma>\<^sub>1 @ [(x, U)] @ \<Gamma>\<^sub>2 \<turnstile> t : T` `\<Gamma>\<^sub>2 \<turnstile> u : U`
   493   have "\<Gamma>\<^sub>1 @ \<Gamma>\<^sub>2 \<turnstile> t[x\<mapsto>u] : T" by (rule subst_type_aux)
   494   moreover from `\<turnstile> PVar x U \<rhd> u \<Rightarrow> \<theta>` have "\<theta> = [(x, u)]"
   495     by cases simp_all
   496   ultimately show ?case by simp
   497 next
   498   case (PTuple p S \<Delta>\<^sub>1 q U \<Delta>\<^sub>2)
   499   from `\<turnstile> \<langle>\<langle>p, q\<rangle>\<rangle> \<rhd> u \<Rightarrow> \<theta>` obtain u\<^sub>1 u\<^sub>2 \<theta>\<^sub>1 \<theta>\<^sub>2
   500     where u: "u = \<langle>u\<^sub>1, u\<^sub>2\<rangle>" and \<theta>: "\<theta> = \<theta>\<^sub>1 @ \<theta>\<^sub>2"
   501     and p: "\<turnstile> p \<rhd> u\<^sub>1 \<Rightarrow> \<theta>\<^sub>1" and q: "\<turnstile> q \<rhd> u\<^sub>2 \<Rightarrow> \<theta>\<^sub>2"
   502     by cases simp_all
   503   with PTuple have "\<Gamma>\<^sub>2 \<turnstile> \<langle>u\<^sub>1, u\<^sub>2\<rangle> : S \<otimes> U" by simp
   504   then obtain u\<^sub>1: "\<Gamma>\<^sub>2 \<turnstile> u\<^sub>1 : S" and u\<^sub>2: "\<Gamma>\<^sub>2 \<turnstile> u\<^sub>2 : U"
   505     by cases (simp_all add: ty.inject trm.inject)
   506   note u\<^sub>1
   507   moreover from `\<Gamma>\<^sub>1 @ (\<Delta>\<^sub>2 @ \<Delta>\<^sub>1) @ \<Gamma>\<^sub>2 \<turnstile> t : T`
   508   have "(\<Gamma>\<^sub>1 @ \<Delta>\<^sub>2) @ \<Delta>\<^sub>1 @ \<Gamma>\<^sub>2 \<turnstile> t : T" by simp
   509   moreover note p
   510   moreover from `supp \<langle>\<langle>p, q\<rangle>\<rangle> \<sharp>* u` and u
   511   have "(supp p::name set) \<sharp>* u\<^sub>1" by (simp add: fresh_star_def)
   512   ultimately have \<theta>\<^sub>1: "(\<Gamma>\<^sub>1 @ \<Delta>\<^sub>2) @ \<Gamma>\<^sub>2 \<turnstile> \<theta>\<^sub>1\<lparr>t\<rparr> : T"
   513     by (rule PTuple)
   514   note u\<^sub>2
   515   moreover from \<theta>\<^sub>1
   516   have "\<Gamma>\<^sub>1 @ \<Delta>\<^sub>2 @ \<Gamma>\<^sub>2 \<turnstile> \<theta>\<^sub>1\<lparr>t\<rparr> : T" by simp
   517   moreover note q
   518   moreover from `supp \<langle>\<langle>p, q\<rangle>\<rangle> \<sharp>* u` and u
   519   have "(supp q::name set) \<sharp>* u\<^sub>2" by (simp add: fresh_star_def)
   520   ultimately have "\<Gamma>\<^sub>1 @ \<Gamma>\<^sub>2 \<turnstile> \<theta>\<^sub>2\<lparr>\<theta>\<^sub>1\<lparr>t\<rparr>\<rparr> : T"
   521     by (rule PTuple)
   522   moreover from `\<turnstile> \<langle>\<langle>p, q\<rangle>\<rangle> \<rhd> u \<Rightarrow> \<theta>` `supp \<langle>\<langle>p, q\<rangle>\<rangle> \<sharp>* u`
   523   have "(supp (map fst \<theta>)::name set) \<sharp>* map snd \<theta>"
   524     by (rule match_fresh)
   525   ultimately show ?case using \<theta> by (simp add: psubst_append)
   526 qed
   527 
   528 lemmas match_type = match_type_aux [where \<Gamma>\<^sub>1="[]", simplified]
   529 
   530 inductive eval :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<longmapsto> _" [60,60] 60)
   531 where
   532   TupleL: "t \<longmapsto> t' \<Longrightarrow> \<langle>t, u\<rangle> \<longmapsto> \<langle>t', u\<rangle>"
   533 | TupleR: "u \<longmapsto> u' \<Longrightarrow> \<langle>t, u\<rangle> \<longmapsto> \<langle>t, u'\<rangle>"
   534 | Abs: "t \<longmapsto> t' \<Longrightarrow> (\<lambda>x:T. t) \<longmapsto> (\<lambda>x:T. t')"
   535 | AppL: "t \<longmapsto> t' \<Longrightarrow> t \<cdot> u \<longmapsto> t' \<cdot> u"
   536 | AppR: "u \<longmapsto> u' \<Longrightarrow> t \<cdot> u \<longmapsto> t \<cdot> u'"
   537 | Beta: "x \<sharp> u \<Longrightarrow> (\<lambda>x:T. t) \<cdot> u \<longmapsto> t[x\<mapsto>u]"
   538 | Let: "((supp p)::name set) \<sharp>* t \<Longrightarrow> distinct (pat_vars p) \<Longrightarrow>
   539     \<turnstile> p \<rhd> t \<Rightarrow> \<theta> \<Longrightarrow> (LET p = t IN u) \<longmapsto> \<theta>\<lparr>u\<rparr>"
   540 
   541 equivariance match
   542 
   543 equivariance eval
   544 
   545 lemma match_vars:
   546   assumes "\<turnstile> p \<rhd> t \<Rightarrow> \<theta>" and "x \<in> supp p"
   547   shows "x \<in> set (map fst \<theta>)" using assms
   548   by induct (auto simp add: supp_atm)
   549 
   550 lemma match_fresh_mono:
   551   assumes "\<turnstile> p \<rhd> t \<Rightarrow> \<theta>" and "(x::name) \<sharp> t"
   552   shows "\<forall>(y, t)\<in>set \<theta>. x \<sharp> t" using assms
   553   by induct auto
   554 
   555 nominal_inductive2 eval
   556 avoids
   557   Abs: "{x}"
   558 | Beta: "{x}"
   559 | Let: "(supp p)::name set"
   560   apply (simp_all add: fresh_star_def abs_fresh fin_supp)
   561   apply (rule psubst_fresh)
   562   apply simp
   563   apply simp
   564   apply (rule ballI)
   565   apply (rule psubst_fresh)
   566   apply (rule match_vars)
   567   apply assumption+
   568   apply (rule match_fresh_mono)
   569   apply auto
   570   done
   571 
   572 lemma typing_case_Abs:
   573   assumes ty: "\<Gamma> \<turnstile> (\<lambda>x:T. t) : S"
   574   and fresh: "x \<sharp> \<Gamma>"
   575   and R: "\<And>U. S = T \<rightarrow> U \<Longrightarrow> (x, T) # \<Gamma> \<turnstile> t : U \<Longrightarrow> P"
   576   shows P using ty
   577 proof cases
   578   case (Abs x' T' t' U)
   579   obtain y::name where y: "y \<sharp> (x, \<Gamma>, \<lambda>x':T'. t')"
   580     by (rule exists_fresh) (auto intro: fin_supp)
   581   from `(\<lambda>x:T. t) = (\<lambda>x':T'. t')` [symmetric]
   582   have x: "x \<sharp> (\<lambda>x':T'. t')" by (simp add: abs_fresh)
   583   have x': "x' \<sharp> (\<lambda>x':T'. t')" by (simp add: abs_fresh)
   584   from `(x', T') # \<Gamma> \<turnstile> t' : U` have x'': "x' \<sharp> \<Gamma>"
   585     by (auto dest: valid_typing)
   586   have "(\<lambda>x:T. t) = (\<lambda>x':T'. t')" by fact
   587   also from x x' y have "\<dots> = [(x, y)] \<bullet> [(x', y)] \<bullet> (\<lambda>x':T'. t')"
   588     by (simp only: perm_fresh_fresh fresh_prod)
   589   also have "\<dots> = (\<lambda>x:T'. [(x, y)] \<bullet> [(x', y)] \<bullet> t')"
   590     by (simp add: swap_simps perm_fresh_fresh)
   591   finally have "(\<lambda>x:T. t) = (\<lambda>x:T'. [(x, y)] \<bullet> [(x', y)] \<bullet> t')" .
   592   then have T: "T = T'" and t: "[(x, y)] \<bullet> [(x', y)] \<bullet> t' = t"
   593     by (simp_all add: trm.inject alpha)
   594   from Abs T have "S = T \<rightarrow> U" by simp
   595   moreover from `(x', T') # \<Gamma> \<turnstile> t' : U`
   596   have "[(x, y)] \<bullet> [(x', y)] \<bullet> ((x', T') # \<Gamma> \<turnstile> t' : U)"
   597     by (simp add: perm_bool)
   598   with T t y x'' fresh have "(x, T) # \<Gamma> \<turnstile> t : U"
   599     by (simp add: eqvts swap_simps perm_fresh_fresh fresh_prod)
   600   ultimately show ?thesis by (rule R)
   601 qed simp_all
   602 
   603 nominal_primrec ty_size :: "ty \<Rightarrow> nat"
   604 where
   605   "ty_size (Atom n) = 0"
   606 | "ty_size (T \<rightarrow> U) = ty_size T + ty_size U + 1"
   607 | "ty_size (T \<otimes> U) = ty_size T + ty_size U + 1"
   608   by (rule TrueI)+
   609 
   610 lemma bind_tuple_ineq:
   611   "ty_size (pat_type p) < ty_size U \<Longrightarrow> Bind U x t \<noteq> (\<lambda>[p]. u)"
   612   by (induct p arbitrary: U x t u) (auto simp add: btrm.inject)
   613 
   614 lemma valid_appD: assumes "valid (\<Gamma> @ \<Delta>)"
   615   shows "valid \<Gamma>" "valid \<Delta>" using assms
   616   by (induct \<Gamma>'\<equiv>"\<Gamma> @ \<Delta>" arbitrary: \<Gamma> \<Delta>)
   617     (auto simp add: Cons_eq_append_conv fresh_list_append)
   618 
   619 lemma valid_app_freshs: assumes "valid (\<Gamma> @ \<Delta>)"
   620   shows "(supp \<Gamma>::name set) \<sharp>* \<Delta>" "(supp \<Delta>::name set) \<sharp>* \<Gamma>" using assms
   621   by (induct \<Gamma>'\<equiv>"\<Gamma> @ \<Delta>" arbitrary: \<Gamma> \<Delta>)
   622     (auto simp add: Cons_eq_append_conv fresh_star_def
   623      fresh_list_nil fresh_list_cons supp_list_nil supp_list_cons fresh_list_append
   624      supp_prod fresh_prod supp_atm fresh_atm
   625      dest: notE [OF iffD1 [OF fresh_def]])
   626 
   627 lemma perm_mem_left: "(x::name) \<in> ((pi::name prm) \<bullet> A) \<Longrightarrow> (rev pi \<bullet> x) \<in> A"
   628   by (drule perm_boolI [of _ "rev pi"]) (simp add: eqvts perm_pi_simp)
   629 
   630 lemma perm_mem_right: "(rev (pi::name prm) \<bullet> (x::name)) \<in> A \<Longrightarrow> x \<in> (pi \<bullet> A)"
   631   by (drule perm_boolI [of _ pi]) (simp add: eqvts perm_pi_simp)
   632 
   633 lemma perm_cases:
   634   assumes pi: "set pi \<subseteq> A \<times> A"
   635   shows "((pi::name prm) \<bullet> B) \<subseteq> A \<union> B"
   636 proof
   637   fix x assume "x \<in> pi \<bullet> B"
   638   then show "x \<in> A \<union> B" using pi
   639     apply (induct pi arbitrary: x B rule: rev_induct)
   640     apply simp
   641     apply (simp add: split_paired_all supp_eqvt)
   642     apply (drule perm_mem_left)
   643     apply (simp add: calc_atm split: split_if_asm)
   644     apply (auto dest: perm_mem_right)
   645     done
   646 qed
   647 
   648 lemma abs_pat_alpha':
   649   assumes eq: "(\<lambda>[p]. t) = (\<lambda>[q]. u)"
   650   and ty: "pat_type p = pat_type q"
   651   and pv: "distinct (pat_vars p)"
   652   and qv: "distinct (pat_vars q)"
   653   shows "\<exists>pi::name prm. p = pi \<bullet> q \<and> t = pi \<bullet> u \<and>
   654     set pi \<subseteq> (supp p \<union> supp q) \<times> (supp p \<union> supp q)"
   655   using assms
   656 proof (induct p arbitrary: q t u)
   657   case (PVar x T)
   658   note PVar' = this
   659   show ?case
   660   proof (cases q)
   661     case (PVar x' T')
   662     with `(\<lambda>[PVar x T]. t) = (\<lambda>[q]. u)`
   663     have "x = x' \<and> t = u \<or> x \<noteq> x' \<and> t = [(x, x')] \<bullet> u \<and> x \<sharp> u"
   664       by (simp add: btrm.inject alpha)
   665     then show ?thesis
   666     proof
   667       assume "x = x' \<and> t = u"
   668       with PVar PVar' have "PVar x T = ([]::name prm) \<bullet> q \<and>
   669         t = ([]::name prm) \<bullet> u \<and>
   670         set ([]::name prm) \<subseteq> (supp (PVar x T) \<union> supp q) \<times>
   671           (supp (PVar x T) \<union> supp q)" by simp
   672       then show ?thesis ..
   673     next
   674       assume "x \<noteq> x' \<and> t = [(x, x')] \<bullet> u \<and> x \<sharp> u"
   675       with PVar PVar' have "PVar x T = [(x, x')] \<bullet> q \<and>
   676         t = [(x, x')] \<bullet> u \<and>
   677         set [(x, x')] \<subseteq> (supp (PVar x T) \<union> supp q) \<times>
   678           (supp (PVar x T) \<union> supp q)"
   679         by (simp add: perm_swap swap_simps supp_atm perm_type)
   680       then show ?thesis ..
   681     qed
   682   next
   683     case (PTuple p\<^sub>1 p\<^sub>2)
   684     with PVar have "ty_size (pat_type p\<^sub>1) < ty_size T" by simp
   685     then have "Bind T x t \<noteq> (\<lambda>[p\<^sub>1]. \<lambda>[p\<^sub>2]. u)"
   686       by (rule bind_tuple_ineq)
   687     moreover from PTuple PVar
   688     have "Bind T x t = (\<lambda>[p\<^sub>1]. \<lambda>[p\<^sub>2]. u)" by simp
   689     ultimately show ?thesis ..
   690   qed
   691 next
   692   case (PTuple p\<^sub>1 p\<^sub>2)
   693   note PTuple' = this
   694   show ?case
   695   proof (cases q)
   696     case (PVar x T)
   697     with PTuple have "ty_size (pat_type p\<^sub>1) < ty_size T" by auto
   698     then have "Bind T x u \<noteq> (\<lambda>[p\<^sub>1]. \<lambda>[p\<^sub>2]. t)"
   699       by (rule bind_tuple_ineq)
   700     moreover from PTuple PVar
   701     have "Bind T x u = (\<lambda>[p\<^sub>1]. \<lambda>[p\<^sub>2]. t)" by simp
   702     ultimately show ?thesis ..
   703   next
   704     case (PTuple p\<^sub>1' p\<^sub>2')
   705     with PTuple' have "(\<lambda>[p\<^sub>1]. \<lambda>[p\<^sub>2]. t) = (\<lambda>[p\<^sub>1']. \<lambda>[p\<^sub>2']. u)" by simp
   706     moreover from PTuple PTuple' have "pat_type p\<^sub>1 = pat_type p\<^sub>1'"
   707       by (simp add: ty.inject)
   708     moreover from PTuple' have "distinct (pat_vars p\<^sub>1)" by simp
   709     moreover from PTuple PTuple' have "distinct (pat_vars p\<^sub>1')" by simp
   710     ultimately have "\<exists>pi::name prm. p\<^sub>1 = pi \<bullet> p\<^sub>1' \<and>
   711       (\<lambda>[p\<^sub>2]. t) = pi \<bullet> (\<lambda>[p\<^sub>2']. u) \<and>
   712       set pi \<subseteq> (supp p\<^sub>1 \<union> supp p\<^sub>1') \<times> (supp p\<^sub>1 \<union> supp p\<^sub>1')"
   713       by (rule PTuple')
   714     then obtain pi::"name prm" where
   715       "p\<^sub>1 = pi \<bullet> p\<^sub>1'" "(\<lambda>[p\<^sub>2]. t) = pi \<bullet> (\<lambda>[p\<^sub>2']. u)" and
   716       pi: "set pi \<subseteq> (supp p\<^sub>1 \<union> supp p\<^sub>1') \<times> (supp p\<^sub>1 \<union> supp p\<^sub>1')" by auto
   717     from `(\<lambda>[p\<^sub>2]. t) = pi \<bullet> (\<lambda>[p\<^sub>2']. u)`
   718     have "(\<lambda>[p\<^sub>2]. t) = (\<lambda>[pi \<bullet> p\<^sub>2']. pi \<bullet> u)"
   719       by (simp add: eqvts)
   720     moreover from PTuple PTuple' have "pat_type p\<^sub>2 = pat_type (pi \<bullet> p\<^sub>2')"
   721       by (simp add: ty.inject pat_type_perm_eq)
   722     moreover from PTuple' have "distinct (pat_vars p\<^sub>2)" by simp
   723     moreover from PTuple PTuple' have "distinct (pat_vars (pi \<bullet> p\<^sub>2'))"
   724       by (simp add: pat_vars_eqvt [symmetric] distinct_eqvt [symmetric])
   725     ultimately have "\<exists>pi'::name prm. p\<^sub>2 = pi' \<bullet> pi \<bullet> p\<^sub>2' \<and>
   726       t = pi' \<bullet> pi \<bullet> u \<and>
   727       set pi' \<subseteq> (supp p\<^sub>2 \<union> supp (pi \<bullet> p\<^sub>2')) \<times> (supp p\<^sub>2 \<union> supp (pi \<bullet> p\<^sub>2'))"
   728       by (rule PTuple')
   729     then obtain pi'::"name prm" where
   730       "p\<^sub>2 = pi' \<bullet> pi \<bullet> p\<^sub>2'" "t = pi' \<bullet> pi \<bullet> u" and
   731       pi': "set pi' \<subseteq> (supp p\<^sub>2 \<union> supp (pi \<bullet> p\<^sub>2')) \<times>
   732         (supp p\<^sub>2 \<union> supp (pi \<bullet> p\<^sub>2'))" by auto
   733     from PTuple PTuple' have "pi \<bullet> distinct (pat_vars \<langle>\<langle>p\<^sub>1', p\<^sub>2'\<rangle>\<rangle>)" by simp
   734     then have "distinct (pat_vars \<langle>\<langle>pi \<bullet> p\<^sub>1', pi \<bullet> p\<^sub>2'\<rangle>\<rangle>)" by (simp only: eqvts)
   735     with `p\<^sub>1 = pi \<bullet> p\<^sub>1'` PTuple'
   736     have fresh: "(supp p\<^sub>2 \<union> supp (pi \<bullet> p\<^sub>2') :: name set) \<sharp>* p\<^sub>1"
   737       by (auto simp add: set_pat_vars_supp fresh_star_def fresh_def eqvts)
   738     from `p\<^sub>1 = pi \<bullet> p\<^sub>1'` have "pi' \<bullet> (p\<^sub>1 = pi \<bullet> p\<^sub>1')" by (rule perm_boolI)
   739     with pt_freshs_freshs [OF pt_name_inst at_name_inst pi' fresh fresh]
   740     have "p\<^sub>1 = pi' \<bullet> pi \<bullet> p\<^sub>1'" by (simp add: eqvts)
   741     with `p\<^sub>2 = pi' \<bullet> pi \<bullet> p\<^sub>2'` have "\<langle>\<langle>p\<^sub>1, p\<^sub>2\<rangle>\<rangle> = (pi' @ pi) \<bullet> \<langle>\<langle>p\<^sub>1', p\<^sub>2'\<rangle>\<rangle>"
   742       by (simp add: pt_name2)
   743     moreover
   744     have "((supp p\<^sub>2 \<union> (pi \<bullet> supp p\<^sub>2')) \<times> (supp p\<^sub>2 \<union> (pi \<bullet> supp p\<^sub>2'))::(name \<times> name) set) \<subseteq>
   745       (supp p\<^sub>2 \<union> (supp p\<^sub>1 \<union> supp p\<^sub>1' \<union> supp p\<^sub>2')) \<times> (supp p\<^sub>2 \<union> (supp p\<^sub>1 \<union> supp p\<^sub>1' \<union> supp p\<^sub>2'))"
   746       by (rule subset_refl Sigma_mono Un_mono perm_cases [OF pi])+
   747     with pi' have "set pi' \<subseteq> \<dots>" by (simp add: supp_eqvt [symmetric])
   748     with pi have "set (pi' @ pi) \<subseteq> (supp \<langle>\<langle>p\<^sub>1, p\<^sub>2\<rangle>\<rangle> \<union> supp \<langle>\<langle>p\<^sub>1', p\<^sub>2'\<rangle>\<rangle>) \<times>
   749       (supp \<langle>\<langle>p\<^sub>1, p\<^sub>2\<rangle>\<rangle> \<union> supp \<langle>\<langle>p\<^sub>1', p\<^sub>2'\<rangle>\<rangle>)"
   750       by (simp add: Sigma_Un_distrib1 Sigma_Un_distrib2 Un_ac) blast
   751     moreover note `t = pi' \<bullet> pi \<bullet> u`
   752     ultimately have "\<langle>\<langle>p\<^sub>1, p\<^sub>2\<rangle>\<rangle> = (pi' @ pi) \<bullet> q \<and> t = (pi' @ pi) \<bullet> u \<and>
   753       set (pi' @ pi) \<subseteq> (supp \<langle>\<langle>p\<^sub>1, p\<^sub>2\<rangle>\<rangle> \<union> supp q) \<times>
   754         (supp \<langle>\<langle>p\<^sub>1, p\<^sub>2\<rangle>\<rangle> \<union> supp q)" using PTuple
   755       by (simp add: pt_name2)
   756     then show ?thesis ..
   757   qed
   758 qed
   759 
   760 lemma typing_case_Let:
   761   assumes ty: "\<Gamma> \<turnstile> (LET p = t IN u) : U"
   762   and fresh: "(supp p::name set) \<sharp>* \<Gamma>"
   763   and distinct: "distinct (pat_vars p)"
   764   and R: "\<And>T \<Delta>. \<Gamma> \<turnstile> t : T \<Longrightarrow> \<turnstile> p : T \<Rightarrow> \<Delta> \<Longrightarrow> \<Delta> @ \<Gamma> \<turnstile> u : U \<Longrightarrow> P"
   765   shows P using ty
   766 proof cases
   767   case (Let p' t' T \<Delta> u')
   768   then have "(supp \<Delta>::name set) \<sharp>* \<Gamma>"
   769     by (auto intro: valid_typing valid_app_freshs)
   770   with Let have "(supp p'::name set) \<sharp>* \<Gamma>"
   771     by (simp add: pat_var)
   772   with fresh have fresh': "(supp p \<union> supp p' :: name set) \<sharp>* \<Gamma>"
   773     by (auto simp add: fresh_star_def)
   774   from Let have "(\<lambda>[p]. Base u) = (\<lambda>[p']. Base u')"
   775     by (simp add: trm.inject)
   776   moreover from Let have "pat_type p = pat_type p'"
   777     by (simp add: trm.inject)
   778   moreover note distinct
   779   moreover from `\<Delta> @ \<Gamma> \<turnstile> u' : U` have "valid (\<Delta> @ \<Gamma>)"
   780     by (rule valid_typing)
   781   then have "valid \<Delta>" by (rule valid_appD)
   782   with `\<turnstile> p' : T \<Rightarrow> \<Delta>` have "distinct (pat_vars p')"
   783     by (simp add: valid_distinct pat_vars_ptyping)
   784   ultimately have "\<exists>pi::name prm. p = pi \<bullet> p' \<and> Base u = pi \<bullet> Base u' \<and>
   785     set pi \<subseteq> (supp p \<union> supp p') \<times> (supp p \<union> supp p')"
   786     by (rule abs_pat_alpha')
   787   then obtain pi::"name prm" where pi: "p = pi \<bullet> p'" "u = pi \<bullet> u'"
   788     and pi': "set pi \<subseteq> (supp p \<union> supp p') \<times> (supp p \<union> supp p')"
   789     by (auto simp add: btrm.inject)
   790   from Let have "\<Gamma> \<turnstile> t : T" by (simp add: trm.inject)
   791   moreover from `\<turnstile> p' : T \<Rightarrow> \<Delta>` have "\<turnstile> (pi \<bullet> p') : (pi \<bullet> T) \<Rightarrow> (pi \<bullet> \<Delta>)"
   792     by (simp add: ptyping.eqvt)
   793   with pi have "\<turnstile> p : T \<Rightarrow> (pi \<bullet> \<Delta>)" by (simp add: perm_type)
   794   moreover from Let
   795   have "(pi \<bullet> \<Delta>) @ (pi \<bullet> \<Gamma>) \<turnstile> (pi \<bullet> u') : (pi \<bullet> U)"
   796     by (simp add: append_eqvt [symmetric] typing.eqvt)
   797   with pi have "(pi \<bullet> \<Delta>) @ \<Gamma> \<turnstile> u : U"
   798     by (simp add: perm_type pt_freshs_freshs
   799       [OF pt_name_inst at_name_inst pi' fresh' fresh'])
   800   ultimately show ?thesis by (rule R)
   801 qed simp_all
   802 
   803 lemma preservation:
   804   assumes "t \<longmapsto> t'" and "\<Gamma> \<turnstile> t : T"
   805   shows "\<Gamma> \<turnstile> t' : T" using assms
   806 proof (nominal_induct avoiding: \<Gamma> T rule: eval.strong_induct)
   807   case (TupleL t t' u)
   808   from `\<Gamma> \<turnstile> \<langle>t, u\<rangle> : T` obtain T\<^sub>1 T\<^sub>2
   809     where "T = T\<^sub>1 \<otimes> T\<^sub>2" "\<Gamma> \<turnstile> t : T\<^sub>1" "\<Gamma> \<turnstile> u : T\<^sub>2"
   810     by cases (simp_all add: trm.inject)
   811   from `\<Gamma> \<turnstile> t : T\<^sub>1` have "\<Gamma> \<turnstile> t' : T\<^sub>1" by (rule TupleL)
   812   then have "\<Gamma> \<turnstile> \<langle>t', u\<rangle> : T\<^sub>1 \<otimes> T\<^sub>2" using `\<Gamma> \<turnstile> u : T\<^sub>2`
   813     by (rule Tuple)
   814   with `T = T\<^sub>1 \<otimes> T\<^sub>2` show ?case by simp
   815 next
   816   case (TupleR u u' t)
   817   from `\<Gamma> \<turnstile> \<langle>t, u\<rangle> : T` obtain T\<^sub>1 T\<^sub>2
   818     where "T = T\<^sub>1 \<otimes> T\<^sub>2" "\<Gamma> \<turnstile> t : T\<^sub>1" "\<Gamma> \<turnstile> u : T\<^sub>2"
   819     by cases (simp_all add: trm.inject)
   820   from `\<Gamma> \<turnstile> u : T\<^sub>2` have "\<Gamma> \<turnstile> u' : T\<^sub>2" by (rule TupleR)
   821   with `\<Gamma> \<turnstile> t : T\<^sub>1` have "\<Gamma> \<turnstile> \<langle>t, u'\<rangle> : T\<^sub>1 \<otimes> T\<^sub>2"
   822     by (rule Tuple)
   823   with `T = T\<^sub>1 \<otimes> T\<^sub>2` show ?case by simp
   824 next
   825   case (Abs t t' x S)
   826   from `\<Gamma> \<turnstile> (\<lambda>x:S. t) : T` `x \<sharp> \<Gamma>` obtain U where
   827     T: "T = S \<rightarrow> U" and U: "(x, S) # \<Gamma> \<turnstile> t : U"
   828     by (rule typing_case_Abs)
   829   from U have "(x, S) # \<Gamma> \<turnstile> t' : U" by (rule Abs)
   830   then have "\<Gamma> \<turnstile> (\<lambda>x:S. t') : S \<rightarrow> U"
   831     by (rule typing.Abs)
   832   with T show ?case by simp
   833 next
   834   case (Beta x u S t)
   835   from `\<Gamma> \<turnstile> (\<lambda>x:S. t) \<cdot> u : T` `x \<sharp> \<Gamma>`
   836   obtain "(x, S) # \<Gamma> \<turnstile> t : T" and "\<Gamma> \<turnstile> u : S"
   837     by cases (auto simp add: trm.inject ty.inject elim: typing_case_Abs)
   838   then show ?case by (rule subst_type)
   839 next
   840   case (Let p t \<theta> u)
   841   from `\<Gamma> \<turnstile> (LET p = t IN u) : T` `supp p \<sharp>* \<Gamma>` `distinct (pat_vars p)`
   842   obtain U \<Delta> where "\<turnstile> p : U \<Rightarrow> \<Delta>" "\<Gamma> \<turnstile> t : U" "\<Delta> @ \<Gamma> \<turnstile> u : T"
   843     by (rule typing_case_Let)
   844   then show ?case using `\<turnstile> p \<rhd> t \<Rightarrow> \<theta>` `supp p \<sharp>* t`
   845     by (rule match_type)
   846 next
   847   case (AppL t t' u)
   848   from `\<Gamma> \<turnstile> t \<cdot> u : T` obtain U where
   849     t: "\<Gamma> \<turnstile> t : U \<rightarrow> T" and u: "\<Gamma> \<turnstile> u : U"
   850     by cases (auto simp add: trm.inject)
   851   from t have "\<Gamma> \<turnstile> t' : U \<rightarrow> T" by (rule AppL)
   852   then show ?case using u by (rule typing.App)
   853 next
   854   case (AppR u u' t)
   855   from `\<Gamma> \<turnstile> t \<cdot> u : T` obtain U where
   856     t: "\<Gamma> \<turnstile> t : U \<rightarrow> T" and u: "\<Gamma> \<turnstile> u : U"
   857     by cases (auto simp add: trm.inject)
   858   from u have "\<Gamma> \<turnstile> u' : U" by (rule AppR)
   859   with t show ?case by (rule typing.App)
   860 qed
   861 
   862 end