1(* *) 2(* Formalisation of the chapter on Logical Relations *) 3(* and a Case Study in Equivalence Checking *) 4(* by Karl Crary from the book on Advanced Topics in *) 5(* Types and Programming Languages, MIT Press 2005 *) 6 7(* The formalisation was done by Julien Narboux and *) 8(* Christian Urban. *) 9 10theory Crary 11 imports "HOL-Nominal.Nominal" 12begin 13 14atom_decl name 15 16nominal_datatype ty = 17 TBase 18 | TUnit 19 | Arrow "ty" "ty" ("_\<rightarrow>_" [100,100] 100) 20 21nominal_datatype trm = 22 Unit 23 | Var "name" ("Var _" [100] 100) 24 | Lam "\<guillemotleft>name\<guillemotright>trm" ("Lam [_]._" [100,100] 100) 25 | App "trm" "trm" ("App _ _" [110,110] 100) 26 | Const "nat" 27 28type_synonym Ctxt = "(name\<times>ty) list" 29type_synonym Subst = "(name\<times>trm) list" 30 31 32lemma perm_ty[simp]: 33 fixes T::"ty" 34 and pi::"name prm" 35 shows "pi\<bullet>T = T" 36 by (induct T rule: ty.induct) (simp_all) 37 38lemma fresh_ty[simp]: 39 fixes x::"name" 40 and T::"ty" 41 shows "x\<sharp>T" 42 by (simp add: fresh_def supp_def) 43 44lemma ty_cases: 45 fixes T::ty 46 shows "(\<exists> T\<^sub>1 T\<^sub>2. T=T\<^sub>1\<rightarrow>T\<^sub>2) \<or> T=TUnit \<or> T=TBase" 47by (induct T rule:ty.induct) (auto) 48 49instantiation ty :: size 50begin 51 52nominal_primrec size_ty 53where 54 "size (TBase) = 1" 55| "size (TUnit) = 1" 56| "size (T\<^sub>1\<rightarrow>T\<^sub>2) = size T\<^sub>1 + size T\<^sub>2" 57by (rule TrueI)+ 58 59instance .. 60 61end 62 63lemma ty_size_greater_zero[simp]: 64 fixes T::"ty" 65 shows "size T > 0" 66by (nominal_induct rule: ty.strong_induct) (simp_all) 67 68section \<open>Substitutions\<close> 69 70fun 71 lookup :: "Subst \<Rightarrow> name \<Rightarrow> trm" 72where 73 "lookup [] x = Var x" 74| "lookup ((y,T)#\<theta>) x = (if x=y then T else lookup \<theta> x)" 75 76lemma lookup_eqvt[eqvt]: 77 fixes pi::"name prm" 78 shows "pi\<bullet>(lookup \<theta> x) = lookup (pi\<bullet>\<theta>) (pi\<bullet>x)" 79by (induct \<theta>) (auto simp add: perm_bij) 80 81lemma lookup_fresh: 82 fixes z::"name" 83 assumes a: "z\<sharp>\<theta>" "z\<sharp>x" 84 shows "z\<sharp> lookup \<theta> x" 85using a 86by (induct rule: lookup.induct) 87 (auto simp add: fresh_list_cons) 88 89lemma lookup_fresh': 90 assumes a: "z\<sharp>\<theta>" 91 shows "lookup \<theta> z = Var z" 92using a 93by (induct rule: lookup.induct) 94 (auto simp add: fresh_list_cons fresh_prod fresh_atm) 95 96nominal_primrec 97 psubst :: "Subst \<Rightarrow> trm \<Rightarrow> trm" ("_<_>" [100,100] 130) 98where 99 "\<theta><(Var x)> = (lookup \<theta> x)" 100| "\<theta><(App t\<^sub>1 t\<^sub>2)> = App \<theta><t\<^sub>1> \<theta><t\<^sub>2>" 101| "x\<sharp>\<theta> \<Longrightarrow> \<theta><(Lam [x].t)> = Lam [x].(\<theta><t>)" 102| "\<theta><(Const n)> = Const n" 103| "\<theta><(Unit)> = Unit" 104apply(finite_guess)+ 105apply(rule TrueI)+ 106apply(simp add: abs_fresh)+ 107apply(fresh_guess)+ 108done 109 110abbreviation 111 subst :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_[_::=_]" [100,100,100] 100) 112where 113 "t[x::=t'] \<equiv> ([(x,t')])<t>" 114 115lemma subst[simp]: 116 shows "(Var x)[y::=t'] = (if x=y then t' else (Var x))" 117 and "(App t\<^sub>1 t\<^sub>2)[y::=t'] = App (t\<^sub>1[y::=t']) (t\<^sub>2[y::=t'])" 118 and "x\<sharp>(y,t') \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])" 119 and "Const n[y::=t'] = Const n" 120 and "Unit [y::=t'] = Unit" 121 by (simp_all add: fresh_list_cons fresh_list_nil) 122 123lemma subst_eqvt[eqvt]: 124 fixes pi::"name prm" 125 shows "pi\<bullet>(t[x::=t']) = (pi\<bullet>t)[(pi\<bullet>x)::=(pi\<bullet>t')]" 126 by (nominal_induct t avoiding: x t' rule: trm.strong_induct) 127 (perm_simp add: fresh_bij)+ 128 129lemma subst_rename: 130 fixes c::"name" 131 assumes a: "c\<sharp>t\<^sub>1" 132 shows "t\<^sub>1[a::=t\<^sub>2] = ([(c,a)]\<bullet>t\<^sub>1)[c::=t\<^sub>2]" 133using a 134apply(nominal_induct t\<^sub>1 avoiding: a c t\<^sub>2 rule: trm.strong_induct) 135apply(simp add: trm.inject calc_atm fresh_atm abs_fresh perm_nat_def)+ 136done 137 138lemma fresh_psubst: 139 fixes z::"name" 140 assumes a: "z\<sharp>t" "z\<sharp>\<theta>" 141 shows "z\<sharp>(\<theta><t>)" 142using a 143by (nominal_induct t avoiding: z \<theta> t rule: trm.strong_induct) 144 (auto simp add: abs_fresh lookup_fresh) 145 146lemma fresh_subst'': 147 fixes z::"name" 148 assumes "z\<sharp>t\<^sub>2" 149 shows "z\<sharp>t\<^sub>1[z::=t\<^sub>2]" 150using assms 151by (nominal_induct t\<^sub>1 avoiding: t\<^sub>2 z rule: trm.strong_induct) 152 (auto simp add: abs_fresh fresh_nat fresh_atm) 153 154lemma fresh_subst': 155 fixes z::"name" 156 assumes "z\<sharp>[y].t\<^sub>1" "z\<sharp>t\<^sub>2" 157 shows "z\<sharp>t\<^sub>1[y::=t\<^sub>2]" 158using assms 159by (nominal_induct t\<^sub>1 avoiding: y t\<^sub>2 z rule: trm.strong_induct) 160 (auto simp add: abs_fresh fresh_nat fresh_atm) 161 162lemma fresh_subst: 163 fixes z::"name" 164 assumes a: "z\<sharp>t\<^sub>1" "z\<sharp>t\<^sub>2" 165 shows "z\<sharp>t\<^sub>1[y::=t\<^sub>2]" 166using a 167by (auto simp add: fresh_subst' abs_fresh) 168 169lemma fresh_psubst_simp: 170 assumes "x\<sharp>t" 171 shows "((x,u)#\<theta>)<t> = \<theta><t>" 172using assms 173proof (nominal_induct t avoiding: x u \<theta> rule: trm.strong_induct) 174 case (Lam y t x u) 175 have fs: "y\<sharp>\<theta>" "y\<sharp>x" "y\<sharp>u" by fact+ 176 moreover have "x\<sharp> Lam [y].t" by fact 177 ultimately have "x\<sharp>t" by (simp add: abs_fresh fresh_atm) 178 moreover have ih:"\<And>n T. n\<sharp>t \<Longrightarrow> ((n,T)#\<theta>)<t> = \<theta><t>" by fact 179 ultimately have "((x,u)#\<theta>)<t> = \<theta><t>" by auto 180 moreover have "((x,u)#\<theta>)<Lam [y].t> = Lam [y].(((x,u)#\<theta>)<t>)" using fs 181 by (simp add: fresh_list_cons fresh_prod) 182 moreover have " \<theta><Lam [y].t> = Lam [y]. (\<theta><t>)" using fs by simp 183 ultimately show "((x,u)#\<theta>)<Lam [y].t> = \<theta><Lam [y].t>" by auto 184qed (auto simp add: fresh_atm abs_fresh) 185 186lemma forget: 187 fixes x::"name" 188 assumes a: "x\<sharp>t" 189 shows "t[x::=t'] = t" 190 using a 191by (nominal_induct t avoiding: x t' rule: trm.strong_induct) 192 (auto simp add: fresh_atm abs_fresh) 193 194lemma subst_fun_eq: 195 fixes u::trm 196 assumes h:"[x].t\<^sub>1 = [y].t\<^sub>2" 197 shows "t\<^sub>1[x::=u] = t\<^sub>2[y::=u]" 198proof - 199 { 200 assume "x=y" and "t\<^sub>1=t\<^sub>2" 201 then have ?thesis using h by simp 202 } 203 moreover 204 { 205 assume h1:"x \<noteq> y" and h2:"t\<^sub>1=[(x,y)] \<bullet> t\<^sub>2" and h3:"x \<sharp> t\<^sub>2" 206 then have "([(x,y)] \<bullet> t\<^sub>2)[x::=u] = t\<^sub>2[y::=u]" by (simp add: subst_rename) 207 then have ?thesis using h2 by simp 208 } 209 ultimately show ?thesis using alpha h by blast 210qed 211 212lemma psubst_empty[simp]: 213 shows "[]<t> = t" 214by (nominal_induct t rule: trm.strong_induct) 215 (auto simp add: fresh_list_nil) 216 217lemma psubst_subst_psubst: 218 assumes h:"c\<sharp>\<theta>" 219 shows "\<theta><t>[c::=s] = ((c,s)#\<theta>)<t>" 220 using h 221by (nominal_induct t avoiding: \<theta> c s rule: trm.strong_induct) 222 (auto simp add: fresh_list_cons fresh_atm forget lookup_fresh lookup_fresh' fresh_psubst) 223 224lemma subst_fresh_simp: 225 assumes a: "x\<sharp>\<theta>" 226 shows "\<theta><Var x> = Var x" 227using a 228by (induct \<theta> arbitrary: x) (auto simp add:fresh_list_cons fresh_prod fresh_atm) 229 230lemma psubst_subst_propagate: 231 assumes "x\<sharp>\<theta>" 232 shows "\<theta><t[x::=u]> = \<theta><t>[x::=\<theta><u>]" 233using assms 234proof (nominal_induct t avoiding: x u \<theta> rule: trm.strong_induct) 235 case (Var n x u \<theta>) 236 { assume "x=n" 237 moreover have "x\<sharp>\<theta>" by fact 238 ultimately have "\<theta><Var n[x::=u]> = \<theta><Var n>[x::=\<theta><u>]" using subst_fresh_simp by auto 239 } 240 moreover 241 { assume h:"x\<noteq>n" 242 then have "x\<sharp>Var n" by (auto simp add: fresh_atm) 243 moreover have "x\<sharp>\<theta>" by fact 244 ultimately have "x\<sharp>\<theta><Var n>" using fresh_psubst by blast 245 then have " \<theta><Var n>[x::=\<theta><u>] = \<theta><Var n>" using forget by auto 246 then have "\<theta><Var n[x::=u]> = \<theta><Var n>[x::=\<theta><u>]" using h by auto 247 } 248 ultimately show ?case by auto 249next 250 case (Lam n t x u \<theta>) 251 have fs:"n\<sharp>x" "n\<sharp>u" "n\<sharp>\<theta>" "x\<sharp>\<theta>" by fact+ 252 have ih:"\<And> y s \<theta>. y\<sharp>\<theta> \<Longrightarrow> ((\<theta><(t[y::=s])>) = ((\<theta><t>)[y::=(\<theta><s>)]))" by fact 253 have "\<theta> <(Lam [n].t)[x::=u]> = \<theta><Lam [n]. (t [x::=u])>" using fs by auto 254 then have "\<theta> <(Lam [n].t)[x::=u]> = Lam [n]. \<theta><t [x::=u]>" using fs by auto 255 moreover have "\<theta><t[x::=u]> = \<theta><t>[x::=\<theta><u>]" using ih fs by blast 256 ultimately have "\<theta> <(Lam [n].t)[x::=u]> = Lam [n].(\<theta><t>[x::=\<theta><u>])" by auto 257 moreover have "Lam [n].(\<theta><t>[x::=\<theta><u>]) = (Lam [n].\<theta><t>)[x::=\<theta><u>]" using fs fresh_psubst by auto 258 ultimately have "\<theta><(Lam [n].t)[x::=u]> = (Lam [n].\<theta><t>)[x::=\<theta><u>]" using fs by auto 259 then show "\<theta><(Lam [n].t)[x::=u]> = \<theta><Lam [n].t>[x::=\<theta><u>]" using fs by auto 260qed (auto) 261 262section \<open>Typing\<close> 263 264inductive 265 valid :: "Ctxt \<Rightarrow> bool" 266where 267 v_nil[intro]: "valid []" 268| v_cons[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> valid ((a,T)#\<Gamma>)" 269 270equivariance valid 271 272inductive_cases 273 valid_cons_elim_auto[elim]:"valid ((x,T)#\<Gamma>)" 274 275abbreviation 276 "sub_context" :: "Ctxt \<Rightarrow> Ctxt \<Rightarrow> bool" (" _ \<subseteq> _ " [55,55] 55) 277where 278 "\<Gamma>\<^sub>1 \<subseteq> \<Gamma>\<^sub>2 \<equiv> \<forall>a T. (a,T)\<in>set \<Gamma>\<^sub>1 \<longrightarrow> (a,T)\<in>set \<Gamma>\<^sub>2" 279 280lemma valid_monotonicity[elim]: 281 fixes \<Gamma> \<Gamma>' :: Ctxt 282 assumes a: "\<Gamma> \<subseteq> \<Gamma>'" 283 and b: "x\<sharp>\<Gamma>'" 284 shows "(x,T\<^sub>1)#\<Gamma> \<subseteq> (x,T\<^sub>1)#\<Gamma>'" 285using a b by auto 286 287lemma fresh_context: 288 fixes \<Gamma> :: "Ctxt" 289 and a :: "name" 290 assumes "a\<sharp>\<Gamma>" 291 shows "\<not>(\<exists>\<tau>::ty. (a,\<tau>)\<in>set \<Gamma>)" 292using assms 293by (induct \<Gamma>) 294 (auto simp add: fresh_prod fresh_list_cons fresh_atm) 295 296lemma type_unicity_in_context: 297 assumes a: "valid \<Gamma>" 298 and b: "(x,T\<^sub>1) \<in> set \<Gamma>" 299 and c: "(x,T\<^sub>2) \<in> set \<Gamma>" 300 shows "T\<^sub>1=T\<^sub>2" 301using a b c 302by (induct \<Gamma>) 303 (auto dest!: fresh_context) 304 305inductive 306 typing :: "Ctxt\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [60,60,60] 60) 307where 308 T_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T" 309| T_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> e\<^sub>1 : T\<^sub>1\<rightarrow>T\<^sub>2; \<Gamma> \<turnstile> e\<^sub>2 : T\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App e\<^sub>1 e\<^sub>2 : T\<^sub>2" 310| T_Lam[intro]: "\<lbrakk>x\<sharp>\<Gamma>; (x,T\<^sub>1)#\<Gamma> \<turnstile> t : T\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T\<^sub>1\<rightarrow>T\<^sub>2" 311| T_Const[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n : TBase" 312| T_Unit[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Unit : TUnit" 313 314equivariance typing 315 316nominal_inductive typing 317 by (simp_all add: abs_fresh) 318 319lemma typing_implies_valid: 320 assumes a: "\<Gamma> \<turnstile> t : T" 321 shows "valid \<Gamma>" 322 using a by (induct) (auto) 323 324declare trm.inject [simp add] 325declare ty.inject [simp add] 326 327inductive_cases typing_inv_auto[elim]: 328 "\<Gamma> \<turnstile> Lam [x].t : T" 329 "\<Gamma> \<turnstile> Var x : T" 330 "\<Gamma> \<turnstile> App x y : T" 331 "\<Gamma> \<turnstile> Const n : T" 332 "\<Gamma> \<turnstile> Unit : TUnit" 333 "\<Gamma> \<turnstile> s : TUnit" 334 335declare trm.inject [simp del] 336declare ty.inject [simp del] 337 338 339section \<open>Definitional Equivalence\<close> 340 341inductive 342 def_equiv :: "Ctxt\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ \<equiv> _ : _" [60,60] 60) 343where 344 Q_Refl[intro]: "\<Gamma> \<turnstile> t : T \<Longrightarrow> \<Gamma> \<turnstile> t \<equiv> t : T" 345| Q_Symm[intro]: "\<Gamma> \<turnstile> t \<equiv> s : T \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : T" 346| Q_Trans[intro]: "\<lbrakk>\<Gamma> \<turnstile> s \<equiv> t : T; \<Gamma> \<turnstile> t \<equiv> u : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> u : T" 347| Q_Abs[intro]: "\<lbrakk>x\<sharp>\<Gamma>; (x,T\<^sub>1)#\<Gamma> \<turnstile> s\<^sub>2 \<equiv> t\<^sub>2 : T\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x]. s\<^sub>2 \<equiv> Lam [x]. t\<^sub>2 : T\<^sub>1 \<rightarrow> T\<^sub>2" 348| Q_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> s\<^sub>1 \<equiv> t\<^sub>1 : T\<^sub>1 \<rightarrow> T\<^sub>2 ; \<Gamma> \<turnstile> s\<^sub>2 \<equiv> t\<^sub>2 : T\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App s\<^sub>1 s\<^sub>2 \<equiv> App t\<^sub>1 t\<^sub>2 : T\<^sub>2" 349| Q_Beta[intro]: "\<lbrakk>x\<sharp>(\<Gamma>,s\<^sub>2,t\<^sub>2); (x,T\<^sub>1)#\<Gamma> \<turnstile> s\<^sub>1 \<equiv> t\<^sub>1 : T\<^sub>2 ; \<Gamma> \<turnstile> s\<^sub>2 \<equiv> t\<^sub>2 : T\<^sub>1\<rbrakk> 350 \<Longrightarrow> \<Gamma> \<turnstile> App (Lam [x]. s\<^sub>1) s\<^sub>2 \<equiv> t\<^sub>1[x::=t\<^sub>2] : T\<^sub>2" 351| Q_Ext[intro]: "\<lbrakk>x\<sharp>(\<Gamma>,s,t); (x,T\<^sub>1)#\<Gamma> \<turnstile> App s (Var x) \<equiv> App t (Var x) : T\<^sub>2\<rbrakk> 352 \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : T\<^sub>1 \<rightarrow> T\<^sub>2" 353| Q_Unit[intro]: "\<lbrakk>\<Gamma> \<turnstile> s : TUnit; \<Gamma> \<turnstile> t: TUnit\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : TUnit" 354 355equivariance def_equiv 356 357nominal_inductive def_equiv 358 by (simp_all add: abs_fresh fresh_subst'') 359 360lemma def_equiv_implies_valid: 361 assumes a: "\<Gamma> \<turnstile> t \<equiv> s : T" 362 shows "valid \<Gamma>" 363using a by (induct) (auto elim: typing_implies_valid) 364 365section \<open>Weak Head Reduction\<close> 366 367inductive 368 whr_def :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<leadsto> _" [80,80] 80) 369where 370 QAR_Beta[intro]: "App (Lam [x]. t\<^sub>1) t\<^sub>2 \<leadsto> t\<^sub>1[x::=t\<^sub>2]" 371| QAR_App[intro]: "t\<^sub>1 \<leadsto> t\<^sub>1' \<Longrightarrow> App t\<^sub>1 t\<^sub>2 \<leadsto> App t\<^sub>1' t\<^sub>2" 372 373declare trm.inject [simp add] 374declare ty.inject [simp add] 375 376inductive_cases whr_inv_auto[elim]: 377 "t \<leadsto> t'" 378 "Lam [x].t \<leadsto> t'" 379 "App (Lam [x].t12) t2 \<leadsto> t" 380 "Var x \<leadsto> t" 381 "Const n \<leadsto> t" 382 "App p q \<leadsto> t" 383 "t \<leadsto> Const n" 384 "t \<leadsto> Var x" 385 "t \<leadsto> App p q" 386 387declare trm.inject [simp del] 388declare ty.inject [simp del] 389 390equivariance whr_def 391 392section \<open>Weak Head Normalisation\<close> 393 394abbreviation 395 nf :: "trm \<Rightarrow> bool" ("_ \<leadsto>|" [100] 100) 396where 397 "t\<leadsto>| \<equiv> \<not>(\<exists> u. t \<leadsto> u)" 398 399inductive 400 whn_def :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<Down> _" [80,80] 80) 401where 402 QAN_Reduce[intro]: "\<lbrakk>s \<leadsto> t; t \<Down> u\<rbrakk> \<Longrightarrow> s \<Down> u" 403| QAN_Normal[intro]: "t\<leadsto>| \<Longrightarrow> t \<Down> t" 404 405declare trm.inject[simp] 406 407inductive_cases whn_inv_auto[elim]: "t \<Down> t'" 408 409declare trm.inject[simp del] 410 411equivariance whn_def 412 413lemma red_unicity : 414 assumes a: "x \<leadsto> a" 415 and b: "x \<leadsto> b" 416 shows "a=b" 417 using a b 418apply (induct arbitrary: b) 419apply (erule whr_inv_auto(3)) 420apply (clarify) 421apply (rule subst_fun_eq) 422apply (simp) 423apply (force) 424apply (erule whr_inv_auto(6)) 425apply (blast)+ 426done 427 428lemma nf_unicity : 429 assumes "x \<Down> a" and "x \<Down> b" 430 shows "a=b" 431 using assms 432proof (induct arbitrary: b) 433 case (QAN_Reduce x t a b) 434 have h:"x \<leadsto> t" "t \<Down> a" by fact+ 435 have ih:"\<And>b. t \<Down> b \<Longrightarrow> a = b" by fact 436 have "x \<Down> b" by fact 437 then obtain t' where "x \<leadsto> t'" and hl:"t' \<Down> b" using h by auto 438 then have "t=t'" using h red_unicity by auto 439 then show "a=b" using ih hl by auto 440qed (auto) 441 442 443section \<open>Algorithmic Term Equivalence and Algorithmic Path Equivalence\<close> 444 445inductive 446 alg_equiv :: "Ctxt\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ \<Leftrightarrow> _ : _" [60,60,60,60] 60) 447and 448 alg_path_equiv :: "Ctxt\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ \<leftrightarrow> _ : _" [60,60,60,60] 60) 449where 450 QAT_Base[intro]: "\<lbrakk>s \<Down> p; t \<Down> q; \<Gamma> \<turnstile> p \<leftrightarrow> q : TBase\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : TBase" 451| QAT_Arrow[intro]: "\<lbrakk>x\<sharp>(\<Gamma>,s,t); (x,T\<^sub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^sub>2\<rbrakk> 452 \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^sub>1 \<rightarrow> T\<^sub>2" 453| QAT_One[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : TUnit" 454| QAP_Var[intro]: "\<lbrakk>valid \<Gamma>;(x,T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x \<leftrightarrow> Var x : T" 455| QAP_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> p \<leftrightarrow> q : T\<^sub>1 \<rightarrow> T\<^sub>2; \<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App p s \<leftrightarrow> App q t : T\<^sub>2" 456| QAP_Const[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n \<leftrightarrow> Const n : TBase" 457 458equivariance alg_equiv 459 460nominal_inductive alg_equiv 461 avoids QAT_Arrow: x 462 by simp_all 463 464declare trm.inject [simp add] 465declare ty.inject [simp add] 466 467inductive_cases alg_equiv_inv_auto[elim]: 468 "\<Gamma> \<turnstile> s\<Leftrightarrow>t : TBase" 469 "\<Gamma> \<turnstile> s\<Leftrightarrow>t : T\<^sub>1 \<rightarrow> T\<^sub>2" 470 "\<Gamma> \<turnstile> s\<leftrightarrow>t : TBase" 471 "\<Gamma> \<turnstile> s\<leftrightarrow>t : TUnit" 472 "\<Gamma> \<turnstile> s\<leftrightarrow>t : T\<^sub>1 \<rightarrow> T\<^sub>2" 473 474 "\<Gamma> \<turnstile> Var x \<leftrightarrow> t : T" 475 "\<Gamma> \<turnstile> Var x \<leftrightarrow> t : T'" 476 "\<Gamma> \<turnstile> s \<leftrightarrow> Var x : T" 477 "\<Gamma> \<turnstile> s \<leftrightarrow> Var x : T'" 478 "\<Gamma> \<turnstile> Const n \<leftrightarrow> t : T" 479 "\<Gamma> \<turnstile> s \<leftrightarrow> Const n : T" 480 "\<Gamma> \<turnstile> App p s \<leftrightarrow> t : T" 481 "\<Gamma> \<turnstile> s \<leftrightarrow> App q t : T" 482 "\<Gamma> \<turnstile> Lam[x].s \<leftrightarrow> t : T" 483 "\<Gamma> \<turnstile> t \<leftrightarrow> Lam[x].s : T" 484 485declare trm.inject [simp del] 486declare ty.inject [simp del] 487 488lemma Q_Arrow_strong_inversion: 489 assumes fs: "x\<sharp>\<Gamma>" "x\<sharp>t" "x\<sharp>u" 490 and h: "\<Gamma> \<turnstile> t \<Leftrightarrow> u : T\<^sub>1\<rightarrow>T\<^sub>2" 491 shows "(x,T\<^sub>1)#\<Gamma> \<turnstile> App t (Var x) \<Leftrightarrow> App u (Var x) : T\<^sub>2" 492proof - 493 obtain y where fs2: "y\<sharp>(\<Gamma>,t,u)" and "(y,T\<^sub>1)#\<Gamma> \<turnstile> App t (Var y) \<Leftrightarrow> App u (Var y) : T\<^sub>2" 494 using h by auto 495 then have "([(x,y)]\<bullet>((y,T\<^sub>1)#\<Gamma>)) \<turnstile> [(x,y)]\<bullet> App t (Var y) \<Leftrightarrow> [(x,y)]\<bullet> App u (Var y) : T\<^sub>2" 496 using alg_equiv.eqvt[simplified] by blast 497 then show ?thesis using fs fs2 by (perm_simp) 498qed 499 500(* 501Warning this lemma is false: 502 503lemma algorithmic_type_unicity: 504 shows "\<lbrakk> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T ; \<Gamma> \<turnstile> s \<Leftrightarrow> u : T' \<rbrakk> \<Longrightarrow> T = T'" 505 and "\<lbrakk> \<Gamma> \<turnstile> s \<leftrightarrow> t : T ; \<Gamma> \<turnstile> s \<leftrightarrow> u : T' \<rbrakk> \<Longrightarrow> T = T'" 506 507Here is the counter example : 508\<Gamma> \<turnstile> Const n \<Leftrightarrow> Const n : Tbase and \<Gamma> \<turnstile> Const n \<Leftrightarrow> Const n : TUnit 509*) 510 511lemma algorithmic_path_type_unicity: 512 shows "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<turnstile> s \<leftrightarrow> u : T' \<Longrightarrow> T = T'" 513proof (induct arbitrary: u T' 514 rule: alg_equiv_alg_path_equiv.inducts(2) [of _ _ _ _ _ "%a b c d . True" ]) 515 case (QAP_Var \<Gamma> x T u T') 516 have "\<Gamma> \<turnstile> Var x \<leftrightarrow> u : T'" by fact 517 then have "u=Var x" and "(x,T') \<in> set \<Gamma>" by auto 518 moreover have "valid \<Gamma>" "(x,T) \<in> set \<Gamma>" by fact+ 519 ultimately show "T=T'" using type_unicity_in_context by auto 520next 521 case (QAP_App \<Gamma> p q T\<^sub>1 T\<^sub>2 s t u T\<^sub>2') 522 have ih:"\<And>u T. \<Gamma> \<turnstile> p \<leftrightarrow> u : T \<Longrightarrow> T\<^sub>1\<rightarrow>T\<^sub>2 = T" by fact 523 have "\<Gamma> \<turnstile> App p s \<leftrightarrow> u : T\<^sub>2'" by fact 524 then obtain r t T\<^sub>1' where "u = App r t" "\<Gamma> \<turnstile> p \<leftrightarrow> r : T\<^sub>1' \<rightarrow> T\<^sub>2'" by auto 525 with ih have "T\<^sub>1\<rightarrow>T\<^sub>2 = T\<^sub>1' \<rightarrow> T\<^sub>2'" by auto 526 then show "T\<^sub>2=T\<^sub>2'" using ty.inject by auto 527qed (auto) 528 529lemma alg_path_equiv_implies_valid: 530 shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> valid \<Gamma>" 531 and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> valid \<Gamma>" 532by (induct rule : alg_equiv_alg_path_equiv.inducts) auto 533 534lemma algorithmic_symmetry: 535 shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<turnstile> t \<Leftrightarrow> s : T" 536 and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<turnstile> t \<leftrightarrow> s : T" 537by (induct rule: alg_equiv_alg_path_equiv.inducts) 538 (auto simp add: fresh_prod) 539 540lemma algorithmic_transitivity: 541 shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<turnstile> t \<Leftrightarrow> u : T \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> u : T" 542 and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<turnstile> t \<leftrightarrow> u : T \<Longrightarrow> \<Gamma> \<turnstile> s \<leftrightarrow> u : T" 543proof (nominal_induct \<Gamma> s t T and \<Gamma> s t T avoiding: u rule: alg_equiv_alg_path_equiv.strong_inducts) 544 case (QAT_Base s p t q \<Gamma> u) 545 have "\<Gamma> \<turnstile> t \<Leftrightarrow> u : TBase" by fact 546 then obtain r' q' where b1: "t \<Down> q'" and b2: "u \<Down> r'" and b3: "\<Gamma> \<turnstile> q' \<leftrightarrow> r' : TBase" by auto 547 have ih: "\<Gamma> \<turnstile> q \<leftrightarrow> r' : TBase \<Longrightarrow> \<Gamma> \<turnstile> p \<leftrightarrow> r' : TBase" by fact 548 have "t \<Down> q" by fact 549 with b1 have eq: "q=q'" by (simp add: nf_unicity) 550 with ih b3 have "\<Gamma> \<turnstile> p \<leftrightarrow> r' : TBase" by simp 551 moreover 552 have "s \<Down> p" by fact 553 ultimately show "\<Gamma> \<turnstile> s \<Leftrightarrow> u : TBase" using b2 by auto 554next 555 case (QAT_Arrow x \<Gamma> s t T\<^sub>1 T\<^sub>2 u) 556 have ih:"(x,T\<^sub>1)#\<Gamma> \<turnstile> App t (Var x) \<Leftrightarrow> App u (Var x) : T\<^sub>2 557 \<Longrightarrow> (x,T\<^sub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App u (Var x) : T\<^sub>2" by fact 558 have fs: "x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" "x\<sharp>u" by fact+ 559 have "\<Gamma> \<turnstile> t \<Leftrightarrow> u : T\<^sub>1\<rightarrow>T\<^sub>2" by fact 560 then have "(x,T\<^sub>1)#\<Gamma> \<turnstile> App t (Var x) \<Leftrightarrow> App u (Var x) : T\<^sub>2" using fs 561 by (simp add: Q_Arrow_strong_inversion) 562 with ih have "(x,T\<^sub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App u (Var x) : T\<^sub>2" by simp 563 then show "\<Gamma> \<turnstile> s \<Leftrightarrow> u : T\<^sub>1\<rightarrow>T\<^sub>2" using fs by (auto simp add: fresh_prod) 564next 565 case (QAP_App \<Gamma> p q T\<^sub>1 T\<^sub>2 s t u) 566 have "\<Gamma> \<turnstile> App q t \<leftrightarrow> u : T\<^sub>2" by fact 567 then obtain r T\<^sub>1' v where ha: "\<Gamma> \<turnstile> q \<leftrightarrow> r : T\<^sub>1'\<rightarrow>T\<^sub>2" and hb: "\<Gamma> \<turnstile> t \<Leftrightarrow> v : T\<^sub>1'" and eq: "u = App r v" 568 by auto 569 have ih1: "\<Gamma> \<turnstile> q \<leftrightarrow> r : T\<^sub>1\<rightarrow>T\<^sub>2 \<Longrightarrow> \<Gamma> \<turnstile> p \<leftrightarrow> r : T\<^sub>1\<rightarrow>T\<^sub>2" by fact 570 have ih2:"\<Gamma> \<turnstile> t \<Leftrightarrow> v : T\<^sub>1 \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> v : T\<^sub>1" by fact 571 have "\<Gamma> \<turnstile> p \<leftrightarrow> q : T\<^sub>1\<rightarrow>T\<^sub>2" by fact 572 then have "\<Gamma> \<turnstile> q \<leftrightarrow> p : T\<^sub>1\<rightarrow>T\<^sub>2" by (simp add: algorithmic_symmetry) 573 with ha have "T\<^sub>1'\<rightarrow>T\<^sub>2 = T\<^sub>1\<rightarrow>T\<^sub>2" using algorithmic_path_type_unicity by simp 574 then have "T\<^sub>1' = T\<^sub>1" by (simp add: ty.inject) 575 then have "\<Gamma> \<turnstile> s \<Leftrightarrow> v : T\<^sub>1" "\<Gamma> \<turnstile> p \<leftrightarrow> r : T\<^sub>1\<rightarrow>T\<^sub>2" using ih1 ih2 ha hb by auto 576 then show "\<Gamma> \<turnstile> App p s \<leftrightarrow> u : T\<^sub>2" using eq by auto 577qed (auto) 578 579lemma algorithmic_weak_head_closure: 580 shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> s' \<leadsto> s \<Longrightarrow> t' \<leadsto> t \<Longrightarrow> \<Gamma> \<turnstile> s' \<Leftrightarrow> t' : T" 581apply (nominal_induct \<Gamma> s t T avoiding: s' t' 582 rule: alg_equiv_alg_path_equiv.strong_inducts(1) [of _ _ _ _ "%a b c d e. True"]) 583apply(auto intro!: QAT_Arrow) 584done 585 586lemma algorithmic_monotonicity: 587 shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<subseteq> \<Gamma>' \<Longrightarrow> valid \<Gamma>' \<Longrightarrow> \<Gamma>' \<turnstile> s \<Leftrightarrow> t : T" 588 and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<subseteq> \<Gamma>' \<Longrightarrow> valid \<Gamma>' \<Longrightarrow> \<Gamma>' \<turnstile> s \<leftrightarrow> t : T" 589proof (nominal_induct \<Gamma> s t T and \<Gamma> s t T avoiding: \<Gamma>' rule: alg_equiv_alg_path_equiv.strong_inducts) 590 case (QAT_Arrow x \<Gamma> s t T\<^sub>1 T\<^sub>2 \<Gamma>') 591 have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" "x\<sharp>\<Gamma>'" by fact+ 592 have h2:"\<Gamma> \<subseteq> \<Gamma>'" by fact 593 have ih:"\<And>\<Gamma>'. \<lbrakk>(x,T\<^sub>1)#\<Gamma> \<subseteq> \<Gamma>'; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^sub>2" by fact 594 have "valid \<Gamma>'" by fact 595 then have "valid ((x,T\<^sub>1)#\<Gamma>')" using fs by auto 596 moreover 597 have sub: "(x,T\<^sub>1)#\<Gamma> \<subseteq> (x,T\<^sub>1)#\<Gamma>'" using h2 by auto 598 ultimately have "(x,T\<^sub>1)#\<Gamma>' \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^sub>2" using ih by simp 599 then show "\<Gamma>' \<turnstile> s \<Leftrightarrow> t : T\<^sub>1\<rightarrow>T\<^sub>2" using fs by (auto simp add: fresh_prod) 600qed (auto) 601 602lemma path_equiv_implies_nf: 603 assumes "\<Gamma> \<turnstile> s \<leftrightarrow> t : T" 604 shows "s \<leadsto>|" and "t \<leadsto>|" 605using assms 606by (induct rule: alg_equiv_alg_path_equiv.inducts(2)) (simp, auto) 607 608section \<open>Logical Equivalence\<close> 609 610function log_equiv :: "(Ctxt \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow> bool)" ("_ \<turnstile> _ is _ : _" [60,60,60,60] 60) 611where 612 "\<Gamma> \<turnstile> s is t : TUnit = True" 613 | "\<Gamma> \<turnstile> s is t : TBase = \<Gamma> \<turnstile> s \<Leftrightarrow> t : TBase" 614 | "\<Gamma> \<turnstile> s is t : (T\<^sub>1 \<rightarrow> T\<^sub>2) = 615 (\<forall>\<Gamma>' s' t'. \<Gamma>\<subseteq>\<Gamma>' \<longrightarrow> valid \<Gamma>' \<longrightarrow> \<Gamma>' \<turnstile> s' is t' : T\<^sub>1 \<longrightarrow> (\<Gamma>' \<turnstile> (App s s') is (App t t') : T\<^sub>2))" 616apply (auto simp add: ty.inject) 617apply (subgoal_tac "(\<exists>T\<^sub>1 T\<^sub>2. b=T\<^sub>1 \<rightarrow> T\<^sub>2) \<or> b=TUnit \<or> b=TBase" ) 618apply (force) 619apply (rule ty_cases) 620done 621 622termination by lexicographic_order 623 624lemma logical_monotonicity: 625 fixes \<Gamma> \<Gamma>' :: Ctxt 626 assumes a1: "\<Gamma> \<turnstile> s is t : T" 627 and a2: "\<Gamma> \<subseteq> \<Gamma>'" 628 and a3: "valid \<Gamma>'" 629 shows "\<Gamma>' \<turnstile> s is t : T" 630using a1 a2 a3 631proof (induct arbitrary: \<Gamma>' rule: log_equiv.induct) 632 case (2 \<Gamma> s t \<Gamma>') 633 then show "\<Gamma>' \<turnstile> s is t : TBase" using algorithmic_monotonicity by auto 634next 635 case (3 \<Gamma> s t T\<^sub>1 T\<^sub>2 \<Gamma>') 636 have "\<Gamma> \<turnstile> s is t : T\<^sub>1\<rightarrow>T\<^sub>2" 637 and "\<Gamma> \<subseteq> \<Gamma>'" 638 and "valid \<Gamma>'" by fact+ 639 then show "\<Gamma>' \<turnstile> s is t : T\<^sub>1\<rightarrow>T\<^sub>2" by simp 640qed (auto) 641 642lemma main_lemma: 643 shows "\<Gamma> \<turnstile> s is t : T \<Longrightarrow> valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T" 644 and "\<Gamma> \<turnstile> p \<leftrightarrow> q : T \<Longrightarrow> \<Gamma> \<turnstile> p is q : T" 645proof (nominal_induct T arbitrary: \<Gamma> s t p q rule: ty.strong_induct) 646 case (Arrow T\<^sub>1 T\<^sub>2) 647 { 648 case (1 \<Gamma> s t) 649 have ih1:"\<And>\<Gamma> s t. \<lbrakk>\<Gamma> \<turnstile> s is t : T\<^sub>2; valid \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^sub>2" by fact 650 have ih2:"\<And>\<Gamma> s t. \<Gamma> \<turnstile> s \<leftrightarrow> t : T\<^sub>1 \<Longrightarrow> \<Gamma> \<turnstile> s is t : T\<^sub>1" by fact 651 have h:"\<Gamma> \<turnstile> s is t : T\<^sub>1\<rightarrow>T\<^sub>2" by fact 652 obtain x::name where fs:"x\<sharp>(\<Gamma>,s,t)" by (erule exists_fresh[OF fs_name1]) 653 have "valid \<Gamma>" by fact 654 then have v: "valid ((x,T\<^sub>1)#\<Gamma>)" using fs by auto 655 then have "(x,T\<^sub>1)#\<Gamma> \<turnstile> Var x \<leftrightarrow> Var x : T\<^sub>1" by auto 656 then have "(x,T\<^sub>1)#\<Gamma> \<turnstile> Var x is Var x : T\<^sub>1" using ih2 by auto 657 then have "(x,T\<^sub>1)#\<Gamma> \<turnstile> App s (Var x) is App t (Var x) : T\<^sub>2" using h v by auto 658 then have "(x,T\<^sub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^sub>2" using ih1 v by auto 659 then show "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^sub>1\<rightarrow>T\<^sub>2" using fs by (auto simp add: fresh_prod) 660 next 661 case (2 \<Gamma> p q) 662 have h: "\<Gamma> \<turnstile> p \<leftrightarrow> q : T\<^sub>1\<rightarrow>T\<^sub>2" by fact 663 have ih1:"\<And>\<Gamma> s t. \<Gamma> \<turnstile> s \<leftrightarrow> t : T\<^sub>2 \<Longrightarrow> \<Gamma> \<turnstile> s is t : T\<^sub>2" by fact 664 have ih2:"\<And>\<Gamma> s t. \<lbrakk>\<Gamma> \<turnstile> s is t : T\<^sub>1; valid \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^sub>1" by fact 665 { 666 fix \<Gamma>' s t 667 assume "\<Gamma> \<subseteq> \<Gamma>'" and hl:"\<Gamma>' \<turnstile> s is t : T\<^sub>1" and hk: "valid \<Gamma>'" 668 then have "\<Gamma>' \<turnstile> p \<leftrightarrow> q : T\<^sub>1 \<rightarrow> T\<^sub>2" using h algorithmic_monotonicity by auto 669 moreover have "\<Gamma>' \<turnstile> s \<Leftrightarrow> t : T\<^sub>1" using ih2 hl hk by auto 670 ultimately have "\<Gamma>' \<turnstile> App p s \<leftrightarrow> App q t : T\<^sub>2" by auto 671 then have "\<Gamma>' \<turnstile> App p s is App q t : T\<^sub>2" using ih1 by auto 672 } 673 then show "\<Gamma> \<turnstile> p is q : T\<^sub>1\<rightarrow>T\<^sub>2" by simp 674 } 675next 676 case TBase 677 { case 2 678 have h:"\<Gamma> \<turnstile> s \<leftrightarrow> t : TBase" by fact 679 then have "s \<leadsto>|" and "t \<leadsto>|" using path_equiv_implies_nf by auto 680 then have "s \<Down> s" and "t \<Down> t" by auto 681 then have "\<Gamma> \<turnstile> s \<Leftrightarrow> t : TBase" using h by auto 682 then show "\<Gamma> \<turnstile> s is t : TBase" by auto 683 } 684qed (auto elim: alg_path_equiv_implies_valid) 685 686corollary corollary_main: 687 assumes a: "\<Gamma> \<turnstile> s \<leftrightarrow> t : T" 688 shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T" 689using a main_lemma alg_path_equiv_implies_valid by blast 690 691lemma logical_symmetry: 692 assumes a: "\<Gamma> \<turnstile> s is t : T" 693 shows "\<Gamma> \<turnstile> t is s : T" 694using a 695by (nominal_induct arbitrary: \<Gamma> s t rule: ty.strong_induct) 696 (auto simp add: algorithmic_symmetry) 697 698lemma logical_transitivity: 699 assumes "\<Gamma> \<turnstile> s is t : T" "\<Gamma> \<turnstile> t is u : T" 700 shows "\<Gamma> \<turnstile> s is u : T" 701using assms 702proof (nominal_induct arbitrary: \<Gamma> s t u rule:ty.strong_induct) 703 case TBase 704 then show "\<Gamma> \<turnstile> s is u : TBase" by (auto elim: algorithmic_transitivity) 705next 706 case (Arrow T\<^sub>1 T\<^sub>2 \<Gamma> s t u) 707 have h1:"\<Gamma> \<turnstile> s is t : T\<^sub>1 \<rightarrow> T\<^sub>2" by fact 708 have h2:"\<Gamma> \<turnstile> t is u : T\<^sub>1 \<rightarrow> T\<^sub>2" by fact 709 have ih1:"\<And>\<Gamma> s t u. \<lbrakk>\<Gamma> \<turnstile> s is t : T\<^sub>1; \<Gamma> \<turnstile> t is u : T\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s is u : T\<^sub>1" by fact 710 have ih2:"\<And>\<Gamma> s t u. \<lbrakk>\<Gamma> \<turnstile> s is t : T\<^sub>2; \<Gamma> \<turnstile> t is u : T\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s is u : T\<^sub>2" by fact 711 { 712 fix \<Gamma>' s' u' 713 assume hsub:"\<Gamma> \<subseteq> \<Gamma>'" and hl:"\<Gamma>' \<turnstile> s' is u' : T\<^sub>1" and hk: "valid \<Gamma>'" 714 then have "\<Gamma>' \<turnstile> u' is s' : T\<^sub>1" using logical_symmetry by blast 715 then have "\<Gamma>' \<turnstile> u' is u' : T\<^sub>1" using ih1 hl by blast 716 then have "\<Gamma>' \<turnstile> App t u' is App u u' : T\<^sub>2" using h2 hsub hk by auto 717 moreover have "\<Gamma>' \<turnstile> App s s' is App t u' : T\<^sub>2" using h1 hsub hl hk by auto 718 ultimately have "\<Gamma>' \<turnstile> App s s' is App u u' : T\<^sub>2" using ih2 by blast 719 } 720 then show "\<Gamma> \<turnstile> s is u : T\<^sub>1 \<rightarrow> T\<^sub>2" by auto 721qed (auto) 722 723lemma logical_weak_head_closure: 724 assumes a: "\<Gamma> \<turnstile> s is t : T" 725 and b: "s' \<leadsto> s" 726 and c: "t' \<leadsto> t" 727 shows "\<Gamma> \<turnstile> s' is t' : T" 728using a b c algorithmic_weak_head_closure 729by (nominal_induct arbitrary: \<Gamma> s t s' t' rule: ty.strong_induct) 730 (auto, blast) 731 732lemma logical_weak_head_closure': 733 assumes "\<Gamma> \<turnstile> s is t : T" and "s' \<leadsto> s" 734 shows "\<Gamma> \<turnstile> s' is t : T" 735using assms 736proof (nominal_induct arbitrary: \<Gamma> s t s' rule: ty.strong_induct) 737 case (TBase \<Gamma> s t s') 738 then show ?case by force 739next 740 case (TUnit \<Gamma> s t s') 741 then show ?case by auto 742next 743 case (Arrow T\<^sub>1 T\<^sub>2 \<Gamma> s t s') 744 have h1:"s' \<leadsto> s" by fact 745 have ih:"\<And>\<Gamma> s t s'. \<lbrakk>\<Gamma> \<turnstile> s is t : T\<^sub>2; s' \<leadsto> s\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s' is t : T\<^sub>2" by fact 746 have h2:"\<Gamma> \<turnstile> s is t : T\<^sub>1\<rightarrow>T\<^sub>2" by fact 747 then 748 have hb:"\<forall>\<Gamma>' s' t'. \<Gamma>\<subseteq>\<Gamma>' \<longrightarrow> valid \<Gamma>' \<longrightarrow> \<Gamma>' \<turnstile> s' is t' : T\<^sub>1 \<longrightarrow> (\<Gamma>' \<turnstile> (App s s') is (App t t') : T\<^sub>2)" 749 by auto 750 { 751 fix \<Gamma>' s\<^sub>2 t\<^sub>2 752 assume "\<Gamma> \<subseteq> \<Gamma>'" and "\<Gamma>' \<turnstile> s\<^sub>2 is t\<^sub>2 : T\<^sub>1" and "valid \<Gamma>'" 753 then have "\<Gamma>' \<turnstile> (App s s\<^sub>2) is (App t t\<^sub>2) : T\<^sub>2" using hb by auto 754 moreover have "(App s' s\<^sub>2) \<leadsto> (App s s\<^sub>2)" using h1 by auto 755 ultimately have "\<Gamma>' \<turnstile> App s' s\<^sub>2 is App t t\<^sub>2 : T\<^sub>2" using ih by auto 756 } 757 then show "\<Gamma> \<turnstile> s' is t : T\<^sub>1\<rightarrow>T\<^sub>2" by auto 758qed 759 760abbreviation 761 log_equiv_for_psubsts :: "Ctxt \<Rightarrow> Subst \<Rightarrow> Subst \<Rightarrow> Ctxt \<Rightarrow> bool" ("_ \<turnstile> _ is _ over _" [60,60] 60) 762where 763 "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma> \<equiv> \<forall>x T. (x,T) \<in> set \<Gamma> \<longrightarrow> \<Gamma>' \<turnstile> \<theta><Var x> is \<theta>'<Var x> : T" 764 765lemma logical_pseudo_reflexivity: 766 assumes "\<Gamma>' \<turnstile> t is s over \<Gamma>" 767 shows "\<Gamma>' \<turnstile> s is s over \<Gamma>" 768proof - 769 from assms have "\<Gamma>' \<turnstile> s is t over \<Gamma>" using logical_symmetry by blast 770 with assms show "\<Gamma>' \<turnstile> s is s over \<Gamma>" using logical_transitivity by blast 771qed 772 773lemma logical_subst_monotonicity : 774 fixes \<Gamma> \<Gamma>' \<Gamma>'' :: Ctxt 775 assumes a: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" 776 and b: "\<Gamma>' \<subseteq> \<Gamma>''" 777 and c: "valid \<Gamma>''" 778 shows "\<Gamma>'' \<turnstile> \<theta> is \<theta>' over \<Gamma>" 779using a b c logical_monotonicity by blast 780 781lemma equiv_subst_ext : 782 assumes h1: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" 783 and h2: "\<Gamma>' \<turnstile> s is t : T" 784 and fs: "x\<sharp>\<Gamma>" 785 shows "\<Gamma>' \<turnstile> (x,s)#\<theta> is (x,t)#\<theta>' over (x,T)#\<Gamma>" 786using assms 787proof - 788 { 789 fix y U 790 assume "(y,U) \<in> set ((x,T)#\<Gamma>)" 791 moreover 792 { 793 assume "(y,U) \<in> set [(x,T)]" 794 with h2 have "\<Gamma>' \<turnstile> ((x,s)#\<theta>)<Var y> is ((x,t)#\<theta>')<Var y> : U" by auto 795 } 796 moreover 797 { 798 assume hl:"(y,U) \<in> set \<Gamma>" 799 then have "\<not> y\<sharp>\<Gamma>" by (induct \<Gamma>) (auto simp add: fresh_list_cons fresh_atm fresh_prod) 800 then have hf:"x\<sharp> Var y" using fs by (auto simp add: fresh_atm) 801 then have "((x,s)#\<theta>)<Var y> = \<theta><Var y>" "((x,t)#\<theta>')<Var y> = \<theta>'<Var y>" 802 using fresh_psubst_simp by blast+ 803 moreover have "\<Gamma>' \<turnstile> \<theta><Var y> is \<theta>'<Var y> : U" using h1 hl by auto 804 ultimately have "\<Gamma>' \<turnstile> ((x,s)#\<theta>)<Var y> is ((x,t)#\<theta>')<Var y> : U" by auto 805 } 806 ultimately have "\<Gamma>' \<turnstile> ((x,s)#\<theta>)<Var y> is ((x,t)#\<theta>')<Var y> : U" by auto 807 } 808 then show "\<Gamma>' \<turnstile> (x,s)#\<theta> is (x,t)#\<theta>' over (x,T)#\<Gamma>" by auto 809qed 810 811theorem fundamental_theorem_1: 812 assumes a1: "\<Gamma> \<turnstile> t : T" 813 and a2: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" 814 and a3: "valid \<Gamma>'" 815 shows "\<Gamma>' \<turnstile> \<theta><t> is \<theta>'<t> : T" 816using a1 a2 a3 817proof (nominal_induct \<Gamma> t T avoiding: \<theta> \<theta>' arbitrary: \<Gamma>' rule: typing.strong_induct) 818 case (T_Lam x \<Gamma> T\<^sub>1 t\<^sub>2 T\<^sub>2 \<theta> \<theta>' \<Gamma>') 819 have vc: "x\<sharp>\<theta>" "x\<sharp>\<theta>'" "x\<sharp>\<Gamma>" by fact+ 820 have asm1: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" by fact 821 have ih:"\<And>\<theta> \<theta>' \<Gamma>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over (x,T\<^sub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><t\<^sub>2> is \<theta>'<t\<^sub>2> : T\<^sub>2" by fact 822 show "\<Gamma>' \<turnstile> \<theta><Lam [x].t\<^sub>2> is \<theta>'<Lam [x].t\<^sub>2> : T\<^sub>1\<rightarrow>T\<^sub>2" using vc 823 proof (simp, intro strip) 824 fix \<Gamma>'' s' t' 825 assume sub: "\<Gamma>' \<subseteq> \<Gamma>''" 826 and asm2: "\<Gamma>''\<turnstile> s' is t' : T\<^sub>1" 827 and val: "valid \<Gamma>''" 828 from asm1 val sub have "\<Gamma>'' \<turnstile> \<theta> is \<theta>' over \<Gamma>" using logical_subst_monotonicity by blast 829 with asm2 vc have "\<Gamma>'' \<turnstile> (x,s')#\<theta> is (x,t')#\<theta>' over (x,T\<^sub>1)#\<Gamma>" using equiv_subst_ext by blast 830 with ih val have "\<Gamma>'' \<turnstile> ((x,s')#\<theta>)<t\<^sub>2> is ((x,t')#\<theta>')<t\<^sub>2> : T\<^sub>2" by auto 831 with vc have "\<Gamma>''\<turnstile>\<theta><t\<^sub>2>[x::=s'] is \<theta>'<t\<^sub>2>[x::=t'] : T\<^sub>2" by (simp add: psubst_subst_psubst) 832 moreover 833 have "App (Lam [x].\<theta><t\<^sub>2>) s' \<leadsto> \<theta><t\<^sub>2>[x::=s']" by auto 834 moreover 835 have "App (Lam [x].\<theta>'<t\<^sub>2>) t' \<leadsto> \<theta>'<t\<^sub>2>[x::=t']" by auto 836 ultimately show "\<Gamma>''\<turnstile> App (Lam [x].\<theta><t\<^sub>2>) s' is App (Lam [x].\<theta>'<t\<^sub>2>) t' : T\<^sub>2" 837 using logical_weak_head_closure by auto 838 qed 839qed (auto) 840 841 842theorem fundamental_theorem_2: 843 assumes h1: "\<Gamma> \<turnstile> s \<equiv> t : T" 844 and h2: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" 845 and h3: "valid \<Gamma>'" 846 shows "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T" 847using h1 h2 h3 848proof (nominal_induct \<Gamma> s t T avoiding: \<Gamma>' \<theta> \<theta>' rule: def_equiv.strong_induct) 849 case (Q_Refl \<Gamma> t T \<Gamma>' \<theta> \<theta>') 850 have "\<Gamma> \<turnstile> t : T" 851 and "valid \<Gamma>'" by fact+ 852 moreover 853 have "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" by fact 854 ultimately show "\<Gamma>' \<turnstile> \<theta><t> is \<theta>'<t> : T" using fundamental_theorem_1 by blast 855next 856 case (Q_Symm \<Gamma> t s T \<Gamma>' \<theta> \<theta>') 857 have "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" 858 and "valid \<Gamma>'" by fact+ 859 moreover 860 have ih: "\<And> \<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><t> is \<theta>'<s> : T" by fact 861 ultimately show "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T" using logical_symmetry by blast 862next 863 case (Q_Trans \<Gamma> s t T u \<Gamma>' \<theta> \<theta>') 864 have ih1: "\<And> \<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T" by fact 865 have ih2: "\<And> \<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><t> is \<theta>'<u> : T" by fact 866 have h: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" 867 and v: "valid \<Gamma>'" by fact+ 868 then have "\<Gamma>' \<turnstile> \<theta>' is \<theta>' over \<Gamma>" using logical_pseudo_reflexivity by auto 869 then have "\<Gamma>' \<turnstile> \<theta>'<t> is \<theta>'<u> : T" using ih2 v by auto 870 moreover have "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T" using ih1 h v by auto 871 ultimately show "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<u> : T" using logical_transitivity by blast 872next 873 case (Q_Abs x \<Gamma> T\<^sub>1 s\<^sub>2 t\<^sub>2 T\<^sub>2 \<Gamma>' \<theta> \<theta>') 874 have fs:"x\<sharp>\<Gamma>" by fact 875 have fs2: "x\<sharp>\<theta>" "x\<sharp>\<theta>'" by fact+ 876 have h2: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" 877 and h3: "valid \<Gamma>'" by fact+ 878 have ih:"\<And>\<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over (x,T\<^sub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><s\<^sub>2> is \<theta>'<t\<^sub>2> : T\<^sub>2" by fact 879 { 880 fix \<Gamma>'' s' t' 881 assume "\<Gamma>' \<subseteq> \<Gamma>''" and hl:"\<Gamma>''\<turnstile> s' is t' : T\<^sub>1" and hk: "valid \<Gamma>''" 882 then have "\<Gamma>'' \<turnstile> \<theta> is \<theta>' over \<Gamma>" using h2 logical_subst_monotonicity by blast 883 then have "\<Gamma>'' \<turnstile> (x,s')#\<theta> is (x,t')#\<theta>' over (x,T\<^sub>1)#\<Gamma>" using equiv_subst_ext hl fs by blast 884 then have "\<Gamma>'' \<turnstile> ((x,s')#\<theta>)<s\<^sub>2> is ((x,t')#\<theta>')<t\<^sub>2> : T\<^sub>2" using ih hk by blast 885 then have "\<Gamma>''\<turnstile> \<theta><s\<^sub>2>[x::=s'] is \<theta>'<t\<^sub>2>[x::=t'] : T\<^sub>2" using fs2 psubst_subst_psubst by auto 886 moreover have "App (Lam [x]. \<theta><s\<^sub>2>) s' \<leadsto> \<theta><s\<^sub>2>[x::=s']" 887 and "App (Lam [x].\<theta>'<t\<^sub>2>) t' \<leadsto> \<theta>'<t\<^sub>2>[x::=t']" by auto 888 ultimately have "\<Gamma>'' \<turnstile> App (Lam [x]. \<theta><s\<^sub>2>) s' is App (Lam [x].\<theta>'<t\<^sub>2>) t' : T\<^sub>2" 889 using logical_weak_head_closure by auto 890 } 891 moreover have "valid \<Gamma>'" by fact 892 ultimately have "\<Gamma>' \<turnstile> Lam [x].\<theta><s\<^sub>2> is Lam [x].\<theta>'<t\<^sub>2> : T\<^sub>1\<rightarrow>T\<^sub>2" by auto 893 then show "\<Gamma>' \<turnstile> \<theta><Lam [x].s\<^sub>2> is \<theta>'<Lam [x].t\<^sub>2> : T\<^sub>1\<rightarrow>T\<^sub>2" using fs2 by auto 894next 895 case (Q_App \<Gamma> s\<^sub>1 t\<^sub>1 T\<^sub>1 T\<^sub>2 s\<^sub>2 t\<^sub>2 \<Gamma>' \<theta> \<theta>') 896 then show "\<Gamma>' \<turnstile> \<theta><App s\<^sub>1 s\<^sub>2> is \<theta>'<App t\<^sub>1 t\<^sub>2> : T\<^sub>2" by auto 897next 898 case (Q_Beta x \<Gamma> s\<^sub>2 t\<^sub>2 T\<^sub>1 s12 t12 T\<^sub>2 \<Gamma>' \<theta> \<theta>') 899 have h: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" 900 and h': "valid \<Gamma>'" by fact+ 901 have fs: "x\<sharp>\<Gamma>" by fact 902 have fs2: " x\<sharp>\<theta>" "x\<sharp>\<theta>'" by fact+ 903 have ih1: "\<And>\<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><s\<^sub>2> is \<theta>'<t\<^sub>2> : T\<^sub>1" by fact 904 have ih2: "\<And>\<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over (x,T\<^sub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><s12> is \<theta>'<t12> : T\<^sub>2" by fact 905 have "\<Gamma>' \<turnstile> \<theta><s\<^sub>2> is \<theta>'<t\<^sub>2> : T\<^sub>1" using ih1 h' h by auto 906 then have "\<Gamma>' \<turnstile> (x,\<theta><s\<^sub>2>)#\<theta> is (x,\<theta>'<t\<^sub>2>)#\<theta>' over (x,T\<^sub>1)#\<Gamma>" using equiv_subst_ext h fs by blast 907 then have "\<Gamma>' \<turnstile> ((x,\<theta><s\<^sub>2>)#\<theta>)<s12> is ((x,\<theta>'<t\<^sub>2>)#\<theta>')<t12> : T\<^sub>2" using ih2 h' by auto 908 then have "\<Gamma>' \<turnstile> \<theta><s12>[x::=\<theta><s\<^sub>2>] is \<theta>'<t12>[x::=\<theta>'<t\<^sub>2>] : T\<^sub>2" using fs2 psubst_subst_psubst by auto 909 then have "\<Gamma>' \<turnstile> \<theta><s12>[x::=\<theta><s\<^sub>2>] is \<theta>'<t12[x::=t\<^sub>2]> : T\<^sub>2" using fs2 psubst_subst_propagate by auto 910 moreover have "App (Lam [x].\<theta><s12>) (\<theta><s\<^sub>2>) \<leadsto> \<theta><s12>[x::=\<theta><s\<^sub>2>]" by auto 911 ultimately have "\<Gamma>' \<turnstile> App (Lam [x].\<theta><s12>) (\<theta><s\<^sub>2>) is \<theta>'<t12[x::=t\<^sub>2]> : T\<^sub>2" 912 using logical_weak_head_closure' by auto 913 then show "\<Gamma>' \<turnstile> \<theta><App (Lam [x].s12) s\<^sub>2> is \<theta>'<t12[x::=t\<^sub>2]> : T\<^sub>2" using fs2 by simp 914next 915 case (Q_Ext x \<Gamma> s t T\<^sub>1 T\<^sub>2 \<Gamma>' \<theta> \<theta>') 916 have h2: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" 917 and h2': "valid \<Gamma>'" by fact+ 918 have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact+ 919 have ih:"\<And>\<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over (x,T\<^sub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk> 920 \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><App s (Var x)> is \<theta>'<App t (Var x)> : T\<^sub>2" by fact 921 { 922 fix \<Gamma>'' s' t' 923 assume hsub: "\<Gamma>' \<subseteq> \<Gamma>''" and hl: "\<Gamma>''\<turnstile> s' is t' : T\<^sub>1" and hk: "valid \<Gamma>''" 924 then have "\<Gamma>'' \<turnstile> \<theta> is \<theta>' over \<Gamma>" using h2 logical_subst_monotonicity by blast 925 then have "\<Gamma>'' \<turnstile> (x,s')#\<theta> is (x,t')#\<theta>' over (x,T\<^sub>1)#\<Gamma>" using equiv_subst_ext hl fs by blast 926 then have "\<Gamma>'' \<turnstile> ((x,s')#\<theta>)<App s (Var x)> is ((x,t')#\<theta>')<App t (Var x)> : T\<^sub>2" using ih hk by blast 927 then 928 have "\<Gamma>'' \<turnstile> App (((x,s')#\<theta>)<s>) (((x,s')#\<theta>)<(Var x)>) is App (((x,t')#\<theta>')<t>) (((x,t')#\<theta>')<(Var x)>) : T\<^sub>2" 929 by auto 930 then have "\<Gamma>'' \<turnstile> App ((x,s')#\<theta>)<s> s' is App ((x,t')#\<theta>')<t> t' : T\<^sub>2" by auto 931 then have "\<Gamma>'' \<turnstile> App (\<theta><s>) s' is App (\<theta>'<t>) t' : T\<^sub>2" using fs fresh_psubst_simp by auto 932 } 933 moreover have "valid \<Gamma>'" by fact 934 ultimately show "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T\<^sub>1\<rightarrow>T\<^sub>2" by auto 935next 936 case (Q_Unit \<Gamma> s t \<Gamma>' \<theta> \<theta>') 937 then show "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : TUnit" by auto 938qed 939 940 941theorem completeness: 942 assumes asm: "\<Gamma> \<turnstile> s \<equiv> t : T" 943 shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T" 944proof - 945 have val: "valid \<Gamma>" using def_equiv_implies_valid asm by simp 946 moreover 947 { 948 fix x T 949 assume "(x,T) \<in> set \<Gamma>" "valid \<Gamma>" 950 then have "\<Gamma> \<turnstile> Var x is Var x : T" using main_lemma(2) by blast 951 } 952 ultimately have "\<Gamma> \<turnstile> [] is [] over \<Gamma>" by auto 953 then have "\<Gamma> \<turnstile> []<s> is []<t> : T" using fundamental_theorem_2 val asm by blast 954 then have "\<Gamma> \<turnstile> s is t : T" by simp 955 then show "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T" using main_lemma(1) val by simp 956qed 957 958text \<open>We leave soundness as an exercise - just like Crary in the ATS book :-) \\ 959 @{prop[mode=IfThen] "\<lbrakk>\<Gamma> \<turnstile> s \<Leftrightarrow> t : T; \<Gamma> \<turnstile> t : T; \<Gamma> \<turnstile> s : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : T"} \\ 960 \<^prop>\<open>\<lbrakk>\<Gamma> \<turnstile> s \<leftrightarrow> t : T; \<Gamma> \<turnstile> t : T; \<Gamma> \<turnstile> s : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : T\<close> 961\<close> 962 963end 964 965