Prove soundness

Author: jvanbruegge

Lemmas.thy

@@ -61,7 +61,7 @@ lemma subst_context_var_name: "atom c \<sharp> \<Gamma> \<Longrightarrow> subst_
 proof (induction \<Gamma> \<tau> a rule: subst_context.induct)
   case (3 b k \<Gamma> \<tau>' a)
   then have 1: "\<Gamma>[\<tau>'/a] = ((a \<leftrightarrow> c) \<bullet> \<Gamma>)[\<tau>'/c]" by (auto simp: fresh_Cons)
-  have 2: "b \<noteq> c" using 3 binder.fresh(2) fresh_Cons fresh_at_base(2) by blast 
+  have 2: "b \<noteq> c" using 3 binder.fresh(2) fresh_Cons fresh_at_base(2) by blast
   then show ?case
   proof (cases "a = b")
     case True

Soundness.thy

@@ -257,7 +257,7 @@ proof (nominal_induct e avoiding: \<tau> a \<sigma> \<Gamma>' \<Gamma> rule: ter
   then show ?case using Tm_Var[OF 1] Var isin_subst_var by auto
 next
   case (App e1 e2)
-  obtain \<tau>1 where P: "\<Gamma>' @ BTyVar a k # \<Gamma> \<turnstile> e1 : \<tau>1 \<rightarrow> \<tau>" "\<Gamma>' @ BTyVar a k # \<Gamma> \<turnstile> e2 : \<tau>1" by (cases rule: Tm.cases[OF App(3)]) auto 
+  obtain \<tau>1 where P: "\<Gamma>' @ BTyVar a k # \<Gamma> \<turnstile> e1 : \<tau>1 \<rightarrow> \<tau>" "\<Gamma>' @ BTyVar a k # \<Gamma> \<turnstile> e2 : \<tau>1" by (cases rule: Tm.cases[OF App(3)]) auto
   have 1: "\<Gamma>'[\<sigma>/a] @ \<Gamma> \<turnstile> e1[\<sigma>/a] : \<tau>1[\<sigma>/a] \<rightarrow> \<tau>[\<sigma>/a]" using App(1)[OF P(1) App(4)] by simp
   have 2: "\<Gamma>'[\<sigma>/a] @ \<Gamma> \<turnstile> e2[\<sigma>/a] : \<tau>1[\<sigma>/a]" by (rule App(2)[OF P(2) App(4)])
   show ?case using Tm_App[OF 1 2] by simp
@@ -286,7 +286,7 @@ next
   case (TyLam b k2 \<sigma>2)
   have 1: "atom b \<sharp> \<Gamma>' @ BTyVar a k # \<Gamma>" using fresh_Cons fresh_append TyLam(2,4,5) by force
   obtain \<sigma>'::\<tau> where P: "BTyVar b k2 # \<Gamma>' @ BTyVar a k # \<Gamma> \<turnstile> \<sigma>2 : \<sigma>'" "\<tau> = (\<forall> b : k2 . \<sigma>')" by (rule T_AbsT_Inv[OF TyLam.prems(1) 1 TyLam(1)])
-  then have 2: "BTyVar b k2 # \<Gamma>'[\<sigma>/a] @ \<Gamma> \<turnstile> \<sigma>2[\<sigma>/a] : \<sigma>'[\<sigma>/a]" using TyLam(6)[of "BTyVar b k2 # \<Gamma>'"] TyLam(2,8) by force 
+  then have 2: "BTyVar b k2 # \<Gamma>'[\<sigma>/a] @ \<Gamma> \<turnstile> \<sigma>2[\<sigma>/a] : \<sigma>'[\<sigma>/a]" using TyLam(6)[of "BTyVar b k2 # \<Gamma>'"] TyLam(2,8) by force
   show ?case using Tm_TAbs[OF 2] TyLam(2,3) P(2) by simp
 next
   case (Let x \<tau>1 e1 e2)
@@ -352,4 +352,60 @@ next
   show ?case using Tm_Let[OF 2 3] Let(3,5) by simp
 qed
 
+theorem preservation:
+  fixes e e'::"term"
+  assumes "[] \<turnstile> e : \<tau>" "e \<longrightarrow> e'"
+  shows "[] \<turnstile> e' : \<tau>"
+using assms beta_nf_def value_beta_nf proof (nominal_induct "[]::\<Gamma>" e \<tau> arbitrary: e' rule: Tm_strong_induct)
+  case (App e1 e2 \<tau>1 \<tau>2)
+  from App(5) show ?case
+  proof cases
+    case (ST_BetaI x \<tau> e)
+    then show ?thesis by (metis App.hyps(1) App.hyps(3) T_Abs_Inv \<tau>.eq_iff(3) append_Nil fresh_Nil substitution)
+  next
+    case (ST_AppI e2')
+    then show ?thesis using App.hyps(2,3,6) Tm_App value_beta_nf by blast
+  qed
+next
+  case (TApp a k e \<sigma> \<tau>)
+  from TApp(4) show ?case
+  proof cases
+    case (ST_BetaTI b k2 e2)
+    obtain c::tyvar where "atom c \<sharp> (a, b, e2, \<sigma>)" using obtain_fresh by blast
+    then have c: "atom c \<sharp> a" "atom c \<sharp> b" "atom c \<sharp> e2" "atom c \<sharp> \<sigma>" by auto
+    obtain \<sigma>2 where c1: "(\<forall> a:k. \<sigma>) = (\<forall> c:k. \<sigma>2)" using Abs_lst_rename[OF c(4)] by auto
+    have same: "k = k2" using TApp(1) forall_ty_lam ST_BetaTI(1) by fastforce
+    obtain e2' where c2: "(\<Lambda> b:k2. e2) = (\<Lambda> c:k. e2')" using Abs_lst_rename[OF c(3)] same by auto
+    have 1: "[] \<turnstile> (\<Lambda> c:k. e2') : \<forall> c:k. \<sigma>2" using TApp(1) ST_BetaTI(1) c2 c1 by simp
+    have 2: "[BTyVar c k] \<turnstile> e2' : \<sigma>2"
+    proof (cases rule: Tm.cases[OF 1])
+      case (4 d _ _ e \<sigma>)
+      have x1: "(d \<leftrightarrow> c) \<bullet> e = e2'" using Abs_rename_body[of d e c e2'] 4(2) by simp
+      have x2: "(d \<leftrightarrow> c) \<bullet> \<sigma> = \<sigma>2" using Abs_rename_body[of d \<sigma> c \<sigma>2] 4(3) by simp
+      show ?thesis
+        by (metis "1" Abs1_eq_iff(3) T_AbsT_Inv \<tau>.eq_iff(5) fresh_Nil fresh_in_context_ty typing_regularity)
+    qed auto
+    then show ?thesis
+      by (metis TApp.hyps(3) \<tau>.eq_iff(5) append_Nil c1 c2 local.ST_BetaTI(2) subst_context.simps(1) subst_term_type_same subst_type_same term.eq_iff(6) type_substitution(3))
+  next
+    case (ST_AppTI e2)
+    then show ?thesis using TApp(2,3) Tm_TApp beta_nf_def value_beta_nf by blast
+  qed
+next
+  case (Let e1 e2 \<tau>1 \<tau>2 x)
+  from Let(4) show ?case
+  proof cases
+    case (ST_SubstI x e2)
+    then show ?thesis
+      by (metis Let.hyps(1,3,4) Step.ST_SubstI Step_deterministic append.left_neutral substitution)
+  qed
+qed auto
+
+lemma multi_preservation: "\<lbrakk> e \<longrightarrow>* e' ; [] \<turnstile> e : \<tau> \<rbrakk> \<Longrightarrow> [] \<turnstile> e' : \<tau>"
+  by (induction e e' rule: Steps.induct) (auto simp: preservation)
+
+corollary soundness: "\<lbrakk> [] \<turnstile> e : \<tau> ; e \<longrightarrow>* e' \<rbrakk> \<Longrightarrow> \<not>(stuck e')"
+  unfolding stuck_def beta_nf_def
+  using progress multi_preservation by blast
+
 end

Typing_Lemmas.thy

@@ -28,7 +28,7 @@ proof (cases rule: Tm.cases[OF a])
     then have 1: "atom x \<sharp> BVar x' \<tau>1' # \<Gamma>'" using b by (simp add: 2 fresh_Cons)
     have 3: "((x' \<leftrightarrow> x) \<bullet> (BVar x' \<tau>1 # \<Gamma>)) \<turnstile> (x' \<leftrightarrow> x) \<bullet> e' : \<tau>2" by (metis "2"(1) "2"(2) "2"(4) Tm.eqvt flip_fresh_fresh no_vars_in_ty term.eq_iff(5))
     have "((x' \<leftrightarrow> x) \<bullet> (BVar x' \<tau>1) # ((x' \<leftrightarrow> x) \<bullet> \<Gamma>)) = BVar x \<tau>1#\<Gamma>"
-      by (metis "1" "2"(1) "2"(4) CtxE(2) binder.perm_simps(1) context_valid_tm flip_at_simps(1) flip_fresh_fresh fresh_Cons no_vars_in_ty) 
+      by (metis "1" "2"(1) "2"(4) CtxE(2) binder.perm_simps(1) context_valid_tm flip_at_simps(1) flip_fresh_fresh fresh_Cons no_vars_in_ty)
     then show ?thesis using 1 2 3 swap that by auto
   qed
 qed simp_all
@@ -97,7 +97,7 @@ proof (cases rule: Ty.cases[OF a])
   then obtain c::tyvar where "atom c \<sharp> (a, \<sigma>, a2, \<sigma>2, \<Gamma>)" using obtain_fresh by blast
   then have c: "atom c \<sharp> a" "atom c \<sharp> \<sigma>" "atom c \<sharp> a2" "atom c \<sharp> \<sigma>2" "atom c \<sharp> \<Gamma>" by auto
   obtain \<sigma>' where P: "(a2 \<leftrightarrow> c) \<bullet> (\<forall> a2:k. \<sigma>2) = (\<forall> c:k. \<sigma>')" using flip_fresh_fresh by force
-  then have 1: "(a2 \<leftrightarrow> c) \<bullet> \<sigma>2 = \<sigma>'" by (simp add: Abs1_eq_iff(3)) 
+  then have 1: "(a2 \<leftrightarrow> c) \<bullet> \<sigma>2 = \<sigma>'" by (simp add: Abs1_eq_iff(3))
   have 2: "(a2 \<leftrightarrow> c) \<bullet> \<Gamma> = \<Gamma>" by (metis "5"(1) "5"(4) CtxE(1) c(5) context_valid_ty flip_def swap_fresh_fresh)
   have 3: "((a2 \<leftrightarrow> c) \<bullet> BTyVar a2 k) = BTyVar c k" using P by auto
   have "(a2 \<leftrightarrow> c) \<bullet> (BTyVar a2 k # \<Gamma> \<turnstile>\<^sub>t\<^sub>y \<sigma>2 : \<star>)" using 5 by auto
@@ -164,7 +164,7 @@ proof (induction \<Gamma>')
   then show ?case
   proof (cases rule: Ctx.cases[OF Cons(3)])
     case (2 \<Gamma>2 c k3)
-    then have "BTyVar a k = bndr \<or> BTyVar a k \<in> (\<Gamma>' @ BTyVar b k2 # \<Gamma>)" by (metis Cons.prems(1) Cons_eq_append_conv isin.simps(5) list.inject) 
+    then have "BTyVar a k = bndr \<or> BTyVar a k \<in> (\<Gamma>' @ BTyVar b k2 # \<Gamma>)" by (metis Cons.prems(1) Cons_eq_append_conv isin.simps(5) list.inject)
     then show ?thesis
     proof
       assume a: "BTyVar a k = bndr"