1section \<open>Simply-typed lambda-calculus with let and tuple patterns\<close> 2 3theory Pattern 4imports "HOL-Nominal.Nominal" 5begin 6 7no_syntax 8 "_Map" :: "maplets => 'a \<rightharpoonup> 'b" ("(1[_])") 9 10atom_decl name 11 12nominal_datatype ty = 13 Atom nat 14 | Arrow ty ty (infixr "\<rightarrow>" 200) 15 | TupleT ty ty (infixr "\<otimes>" 210) 16 17lemma fresh_type [simp]: "(a::name) \<sharp> (T::ty)" 18 by (induct T rule: ty.induct) (simp_all add: fresh_nat) 19 20lemma supp_type [simp]: "supp (T::ty) = ({} :: name set)" 21 by (induct T rule: ty.induct) (simp_all add: ty.supp supp_nat) 22 23lemma perm_type: "(pi::name prm) \<bullet> (T::ty) = T" 24 by (induct T rule: ty.induct) (simp_all add: perm_nat_def) 25 26nominal_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 32and btrm = 33 Base trm 34 | Bind ty "\<guillemotleft>name\<guillemotright>btrm" 35 36abbreviation 37 Abs_syn :: "name \<Rightarrow> ty \<Rightarrow> trm \<Rightarrow> trm" ("(3\<lambda>_:_./ _)" [0, 0, 10] 10) 38where 39 "\<lambda>x:T. t \<equiv> Abs T x t" 40 41datatype 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 *) 46overloading pat_perm \<equiv> "perm :: name prm \<Rightarrow> pat \<Rightarrow> pat" (unchecked) 47begin 48 49primrec pat_perm 50where 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 54end 55 56declare pat_perm.simps [eqvt] 57 58lemma supp_PVar [simp]: "((supp (PVar x T))::name set) = supp x" 59 by (simp add: supp_def perm_fresh_fresh) 60 61lemma 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 64instance pat :: pt_name 65proof (standard, goal_cases) 66 case (1 x) 67 show ?case by (induct x) simp_all 68next 69 case (2 _ _ x) 70 show ?case by (induct x) (simp_all add: pt_name2) 71next 72 case (3 _ _ x) 73 then show ?case by (induct x) (simp_all add: pt_name3) 74qed 75 76instance pat :: fs_name 77proof (standard, goal_cases) 78 case (1 x) 79 show ?case by (induct x) (simp_all add: fin_supp) 80qed 81 82(* the following function cannot be defined using nominal_primrec, *) 83(* since variable parameters are currently not allowed. *) 84primrec abs_pat :: "pat \<Rightarrow> btrm \<Rightarrow> btrm" ("(3\<lambda>[_]./ _)" [0, 10] 10) 85where 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 89lemma 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 93lemma 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 97lemma 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)" 101proof - 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) 111qed 112 113primrec pat_vars :: "pat \<Rightarrow> name list" 114where 115 "pat_vars (PVar x T) = [x]" 116| "pat_vars \<langle>\<langle>p, q\<rangle>\<rangle> = pat_vars q @ pat_vars p" 117 118lemma 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 122lemma set_pat_vars_supp: "set (pat_vars p) = supp p" 123 by (induct p) (auto simp add: supp_atm) 124 125lemma 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 129primrec pat_type :: "pat \<Rightarrow> ty" 130where 131 "pat_type (PVar x T) = T" 132| "pat_type \<langle>\<langle>p, q\<rangle>\<rangle> = pat_type p \<otimes> pat_type q" 133 134lemma pat_type_eqvt [eqvt]: 135 "(pi :: name prm) \<bullet> (pat_type p) = pat_type (pi \<bullet> p)" 136 by (induct p) simp_all 137 138lemma pat_type_perm_eq: "pat_type ((pi :: name prm) \<bullet> p) = pat_type p" 139 by (induct p) (simp_all add: perm_type) 140 141type_synonym ctx = "(name \<times> ty) list" 142 143inductive 144 ptyping :: "pat \<Rightarrow> ty \<Rightarrow> ctx \<Rightarrow> bool" ("\<turnstile> _ : _ \<Rightarrow> _" [60, 60, 60] 60) 145where 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 149lemma 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 154inductive 155 valid :: "ctx \<Rightarrow> bool" 156where 157 Nil [intro!]: "valid []" 158| Cons [intro!]: "valid \<Gamma> \<Longrightarrow> x \<sharp> \<Gamma> \<Longrightarrow> valid ((x, T) # \<Gamma>)" 159 160inductive_cases validE[elim!]: "valid ((x, T) # \<Gamma>)" 161 162lemma 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 165lemma valid_distinct: "valid \<Gamma> = distinct (map fst \<Gamma>)" 166 by (induct \<Gamma>) (auto simp add: fresh_ctxt_set_eq [symmetric]) 167 168abbreviation 169 "sub_ctx" :: "ctx \<Rightarrow> ctx \<Rightarrow> bool" ("_ \<sqsubseteq> _") 170where 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 173abbreviation 174 Let_syn :: "pat \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm" ("(LET (_ =/ _)/ IN (_))" 10) 175where 176 "LET p = t IN u \<equiv> Let (pat_type p) t (\<lambda>[p]. Base u)" 177 178inductive typing :: "ctx \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60, 60, 60] 60) 179where 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 188equivariance ptyping 189 190equivariance valid 191 192equivariance typing 193 194lemma valid_typing: 195 assumes "\<Gamma> \<turnstile> t : T" 196 shows "valid \<Gamma>" using assms 197 by induct auto 198 199lemma 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 204lemma 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 210lemma 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 215lemma 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 222nominal_inductive2 typing 223avoids 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 229lemma 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" 232proof - 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) 253qed 254 255lemma 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 274inductive 275 match :: "pat \<Rightarrow> trm \<Rightarrow> (name \<times> trm) list \<Rightarrow> bool" ("\<turnstile> _ \<rhd> _ \<Rightarrow> _" [50, 50, 50] 50) 276where 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 280fun 281 lookup :: "(name \<times> trm) list \<Rightarrow> name \<Rightarrow> trm" 282where 283 "lookup [] x = Var x" 284| "lookup ((y, e) # \<theta>) x = (if x = y then e else lookup \<theta> x)" 285 286lemma 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 293nominal_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) 296where 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 308lemma 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 316lemma 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 326lemma 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 333abbreviation 334 subst :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_[_\<mapsto>_]" [100,0,0] 100) 335where 336 "t[x\<mapsto>t'] \<equiv> [(x,t')]\<lparr>t\<rparr>" 337 338abbreviation 339 substb :: "btrm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> btrm" ("_[_\<mapsto>_]\<^sub>b" [100,0,0] 100) 340where 341 "t[x\<mapsto>t']\<^sub>b \<equiv> [(x,t')]\<lparr>t\<rparr>\<^sub>b" 342 343lemma 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 347lemma 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 350lemma 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 371lemma 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 374lemma 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 381lemma 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 387lemma 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 391lemma 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 397lemma 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 401lemma 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 408lemma 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 412proof (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 \<open>valid (\<Delta> @ [(x, U)] @ \<Gamma>)\<close> 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 426next 427 case (Tuple t\<^sub>1 T\<^sub>1 t\<^sub>2 T\<^sub>2) 428 from refl \<open>\<Gamma> \<turnstile> u : U\<close> 429 have "\<Delta> @ \<Gamma> \<turnstile> t\<^sub>1[x\<mapsto>u] : T\<^sub>1" by (rule Tuple) 430 moreover from refl \<open>\<Gamma> \<turnstile> u : U\<close> 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 434next 435 case (Let p t T \<Delta>' s S) 436 from refl \<open>\<Gamma> \<turnstile> u : U\<close> 437 have "\<Delta> @ \<Gamma> \<turnstile> t[x\<mapsto>u] : T" by (rule Let) 438 moreover note \<open>\<turnstile> p : T \<Rightarrow> \<Delta>'\<close> 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 \<open>\<Gamma> \<turnstile> u : U\<close> 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 447next 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 \<open>\<Gamma> \<turnstile> u : U\<close> 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 458next 459 case (App t\<^sub>1 T S t\<^sub>2) 460 from refl \<open>\<Gamma> \<turnstile> u : U\<close> 461 have "\<Delta> @ \<Gamma> \<turnstile> t\<^sub>1[x\<mapsto>u] : T \<rightarrow> S" by (rule App) 462 moreover from refl \<open>\<Gamma> \<turnstile> u : U\<close> 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 467qed 468 469lemmas subst_type = subst_type_aux [of "[]", simplified] 470 471lemma 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 475lemma 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 479lemma 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 483lemma 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 490proof (induct arbitrary: \<Gamma>\<^sub>1 \<Gamma>\<^sub>2 t u T \<theta>) 491 case (PVar x U) 492 from \<open>\<Gamma>\<^sub>1 @ [(x, U)] @ \<Gamma>\<^sub>2 \<turnstile> t : T\<close> \<open>\<Gamma>\<^sub>2 \<turnstile> u : U\<close> 493 have "\<Gamma>\<^sub>1 @ \<Gamma>\<^sub>2 \<turnstile> t[x\<mapsto>u] : T" by (rule subst_type_aux) 494 moreover from \<open>\<turnstile> PVar x U \<rhd> u \<Rightarrow> \<theta>\<close> have "\<theta> = [(x, u)]" 495 by cases simp_all 496 ultimately show ?case by simp 497next 498 case (PTuple p S \<Delta>\<^sub>1 q U \<Delta>\<^sub>2) 499 from \<open>\<turnstile> \<langle>\<langle>p, q\<rangle>\<rangle> \<rhd> u \<Rightarrow> \<theta>\<close> 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 \<open>\<Gamma>\<^sub>1 @ (\<Delta>\<^sub>2 @ \<Delta>\<^sub>1) @ \<Gamma>\<^sub>2 \<turnstile> t : T\<close> 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 \<open>supp \<langle>\<langle>p, q\<rangle>\<rangle> \<sharp>* u\<close> 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 \<open>supp \<langle>\<langle>p, q\<rangle>\<rangle> \<sharp>* u\<close> 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 \<open>\<turnstile> \<langle>\<langle>p, q\<rangle>\<rangle> \<rhd> u \<Rightarrow> \<theta>\<close> \<open>supp \<langle>\<langle>p, q\<rangle>\<rangle> \<sharp>* u\<close> 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) 526qed 527 528lemmas match_type = match_type_aux [where \<Gamma>\<^sub>1="[]", simplified] 529 530inductive eval :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<longmapsto> _" [60,60] 60) 531where 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 541equivariance match 542 543equivariance eval 544 545lemma 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 550lemma 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 555nominal_inductive2 eval 556avoids 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 572lemma 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 577proof 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 \<open>(\<lambda>x:T. t) = (\<lambda>x':T'. t')\<close> [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 \<open>(x', T') # \<Gamma> \<turnstile> t' : U\<close> 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 \<open>(x', T') # \<Gamma> \<turnstile> t' : U\<close> 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) 601qed simp_all 602 603nominal_primrec ty_size :: "ty \<Rightarrow> nat" 604where 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 610lemma 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 614lemma 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 619lemma 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 627lemma 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 630lemma 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 633lemma perm_cases: 634 assumes pi: "set pi \<subseteq> A \<times> A" 635 shows "((pi::name prm) \<bullet> B) \<subseteq> A \<union> B" 636proof 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: if_split_asm) 644 apply (auto dest: perm_mem_right) 645 done 646qed 647 648lemma 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 656proof (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 \<open>(\<lambda>[PVar x T]. t) = (\<lambda>[q]. u)\<close> 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 691next 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 \<open>(\<lambda>[p\<^sub>2]. t) = pi \<bullet> (\<lambda>[p\<^sub>2']. u)\<close> 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 \<open>p\<^sub>1 = pi \<bullet> p\<^sub>1'\<close> 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 \<open>p\<^sub>1 = pi \<bullet> p\<^sub>1'\<close> 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 \<open>p\<^sub>2 = pi' \<bullet> pi \<bullet> p\<^sub>2'\<close> 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 \<open>t = pi' \<bullet> pi \<bullet> u\<close> 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 758qed 759 760lemma 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 766proof 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 \<open>\<Delta> @ \<Gamma> \<turnstile> u' : U\<close> have "valid (\<Delta> @ \<Gamma>)" 780 by (rule valid_typing) 781 then have "valid \<Delta>" by (rule valid_appD) 782 with \<open>\<turnstile> p' : T \<Rightarrow> \<Delta>\<close> 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 \<open>\<turnstile> p' : T \<Rightarrow> \<Delta>\<close> 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) 801qed simp_all 802 803lemma preservation: 804 assumes "t \<longmapsto> t'" and "\<Gamma> \<turnstile> t : T" 805 shows "\<Gamma> \<turnstile> t' : T" using assms 806proof (nominal_induct avoiding: \<Gamma> T rule: eval.strong_induct) 807 case (TupleL t t' u) 808 from \<open>\<Gamma> \<turnstile> \<langle>t, u\<rangle> : T\<close> 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 \<open>\<Gamma> \<turnstile> t : T\<^sub>1\<close> 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 \<open>\<Gamma> \<turnstile> u : T\<^sub>2\<close> 813 by (rule Tuple) 814 with \<open>T = T\<^sub>1 \<otimes> T\<^sub>2\<close> show ?case by simp 815next 816 case (TupleR u u' t) 817 from \<open>\<Gamma> \<turnstile> \<langle>t, u\<rangle> : T\<close> 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 \<open>\<Gamma> \<turnstile> u : T\<^sub>2\<close> have "\<Gamma> \<turnstile> u' : T\<^sub>2" by (rule TupleR) 821 with \<open>\<Gamma> \<turnstile> t : T\<^sub>1\<close> have "\<Gamma> \<turnstile> \<langle>t, u'\<rangle> : T\<^sub>1 \<otimes> T\<^sub>2" 822 by (rule Tuple) 823 with \<open>T = T\<^sub>1 \<otimes> T\<^sub>2\<close> show ?case by simp 824next 825 case (Abs t t' x S) 826 from \<open>\<Gamma> \<turnstile> (\<lambda>x:S. t) : T\<close> \<open>x \<sharp> \<Gamma>\<close> 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 833next 834 case (Beta x u S t) 835 from \<open>\<Gamma> \<turnstile> (\<lambda>x:S. t) \<cdot> u : T\<close> \<open>x \<sharp> \<Gamma>\<close> 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) 839next 840 case (Let p t \<theta> u) 841 from \<open>\<Gamma> \<turnstile> (LET p = t IN u) : T\<close> \<open>supp p \<sharp>* \<Gamma>\<close> \<open>distinct (pat_vars p)\<close> 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 \<open>\<turnstile> p \<rhd> t \<Rightarrow> \<theta>\<close> \<open>supp p \<sharp>* t\<close> 845 by (rule match_type) 846next 847 case (AppL t t' u) 848 from \<open>\<Gamma> \<turnstile> t \<cdot> u : T\<close> 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) 853next 854 case (AppR u u' t) 855 from \<open>\<Gamma> \<turnstile> t \<cdot> u : T\<close> 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) 860qed 861 862end 863