Prove determinancy of typing and kinding

Author: jvanbruegge

Determinancy.thy

@@ -0,0 +1,37 @@
+theory Determinancy
+  imports Typing Typing_Lemmas
+begin
+
+lemma unique_ty: "\<lbrakk> \<Gamma> \<turnstile>\<^sub>t\<^sub>y \<tau> : k1 ; \<Gamma> \<turnstile>\<^sub>t\<^sub>y \<tau> : k2 \<rbrakk> \<Longrightarrow> k1 = k2"
+proof (nominal_induct \<tau> arbitrary: k1 k2 rule: \<tau>.strong_induct)
+  case (TyVar x)
+  then show ?case using isin_split isin_same(1) by blast
+next
+  case (TyConApp \<tau>1 \<tau>2)
+  then show ?case by fastforce
+next
+  case (TyForall x1 x2a x3)
+  then show ?case by (metis Ty_Forall_Inv_2)
+qed auto
+
+lemma unique_tm: "\<lbrakk> \<Gamma> \<turnstile> e : \<tau>1 ; \<Gamma> \<turnstile> e : \<tau>2 \<rbrakk> \<Longrightarrow> \<tau>1 = \<tau>2"
+proof (nominal_induct e avoiding: \<Gamma> \<tau>1 \<tau>2 rule: term.strong_induct)
+  case (Var x)
+  then show ?case using isin_split isin_same(2) by blast
+next
+  case (TyApp e1 \<tau>)
+  obtain a1 k1 \<sigma>1 where 1: "\<Gamma> \<turnstile> e1 : \<forall> a1:k1. \<sigma>1" "\<tau>1 = \<sigma>1[\<tau>/a1]" by (cases rule: Tm.cases[OF TyApp(2)]) auto 
+  obtain a2 k2 \<sigma>2 where 2: "\<Gamma> \<turnstile> e1 : \<forall> a2:k2. \<sigma>2" "\<tau>2 = \<sigma>2[\<tau>/a2]" by (cases rule: Tm.cases[OF TyApp(3)]) auto 
+  show ?case using TyApp(1)[OF 1(1) 2(1)] subst_type_same 1(2) 2(2) by simp
+next
+  case (Lam x \<tau> e)
+  then show ?case by (metis T_Abs_Inv)
+next
+  case (TyLam a k e)
+  then show ?case by (metis T_AbsT_Inv)
+next
+  case (Let x \<tau> e1 e2)
+  then show ?case using T_Let_Inv by blast
+qed fastforce+
+
+end

ROOT

@@ -2,3 +2,4 @@ session Lambda = HOL + sessions "HOL-Eisbach" Nominal2
 theories
     Confluence
     Soundness
+    Determinancy

Typing_Lemmas.thy

@@ -182,13 +182,20 @@ qed simp
 lemma context_split_valid: "\<turnstile> \<Gamma>' @ \<Gamma> \<Longrightarrow> \<turnstile> \<Gamma>"
   by (induction \<Gamma>') (auto simp: Ctx_Empty)
 
-lemma isin_split: "\<lbrakk> BVar x \<tau> \<in> \<Gamma> ; \<turnstile> \<Gamma> \<rbrakk> \<Longrightarrow> \<exists>\<Gamma>1 \<Gamma>2. \<Gamma> = \<Gamma>1 @ BVar x \<tau> # \<Gamma>2"
+lemma isin_split: "\<lbrakk> b \<in> \<Gamma> ; \<turnstile> \<Gamma> \<rbrakk> \<Longrightarrow> \<exists>\<Gamma>1 \<Gamma>2. \<Gamma> = \<Gamma>1 @ b # \<Gamma>2"
 proof (induction \<Gamma>)
   case (Cons bndr \<Gamma>)
   then show ?case
-  proof (cases "bndr = BVar x \<tau>")
+  proof (cases "bndr = b")
     case False
-    then have "BVar x \<tau> \<in> \<Gamma>" using Cons(2) by (cases bndr rule: binder.exhaust) auto
+    then have "b \<in> \<Gamma>"
+    proof (cases bndr rule: binder.exhaust)
+      case (BVar x \<tau>)
+      then show ?thesis using False Cons by (cases b rule: binder.exhaust) auto
+    next
+      case (BTyVar a k)
+      then show ?thesis using False Cons by (cases b rule: binder.exhaust) auto
+    qed
     then show ?thesis by (metis Cons.IH Cons.prems(2) Cons_eq_appendI context_cons_valid)
   qed blast
 qed auto