54 nominal_datatype sig_ass =

    55     TC_ass "ident" "kind"

    56   | C_ass "ident" "ty"

    58 types Sig = "sig_ass list"

    59 types Ctx = "(name \<times> ty) list"

    60 types Subst = "(name \<times> trm) list"

    61 

    62 inductive

    63     sig_valid  :: "Sig \<Rightarrow> bool" ("\<turnstile> _ sig" [60] 60)

    64 and ctx_valid  :: "Sig \<Rightarrow> Ctx \<Rightarrow> bool" ("_ \<turnstile> _ ctx" [60,60] 60)

    65 and trm_valid  :: "Sig \<Rightarrow> Ctx \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow> bool" ("_,_ \<turnstile> _ : _" [60,60,60,60] 60)

    66 and ty_valid   :: "Sig \<Rightarrow> Ctx \<Rightarrow> ty \<Rightarrow> kind \<Rightarrow> bool" ("_,_ \<turnstile> _ : _" [60,60,60,60] 60)

    67 and kind_valid :: "Sig \<Rightarrow> Ctx \<Rightarrow> kind \<Rightarrow> bool" ("_,_ \<turnstile> _ : Kind" [60,60,60] 60)

    68 and trm_equiv  :: "Sig \<Rightarrow> Ctx \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow> bool" ("_,_ \<turnstile> _ = _ : _" [60,60,60,60,60] 60)

    69 and ty_equiv   :: "Sig \<Rightarrow> Ctx \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> kind \<Rightarrow> bool" ("_,_ \<turnstile> _ = _ : _" [60,60,60,60,60] 60)

    70 and kind_equiv :: "Sig \<Rightarrow> Ctx \<Rightarrow> kind \<Rightarrow> kind \<Rightarrow> bool" ("_,_ \<turnstile> _ = _ : Kind" [60,60,60,60] 60)

    71 where

    72 (* Signatures *)

    73   s1: "\<turnstile> [] sig"

    74 | s2: "\<lbrakk>\<turnstile> \<Sigma> sig; \<Sigma>,[] \<turnstile> K : Kind; atom a\<sharp>\<Sigma>\<rbrakk> \<Longrightarrow> \<turnstile> (TC_ass a K)#\<Sigma> sig"

    75 | s3: "\<lbrakk>\<turnstile> \<Sigma> sig; \<Sigma>,[] \<turnstile> A : Type; atom c\<sharp>\<Sigma>\<rbrakk> \<Longrightarrow> \<turnstile> (C_ass c A)#\<Sigma> sig"

    76 

    77 (* Contexts *)

    78 | c1: "\<turnstile> \<Sigma> sig \<Longrightarrow> \<Sigma> \<turnstile> [] ctx"

    79 | c2: "\<lbrakk>\<Sigma> \<turnstile> \<Gamma>  ctx; \<Sigma>,\<Gamma> \<turnstile> A : Type; atom x\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> \<Sigma> \<turnstile> (x,A)#\<Gamma> ctx"

    80 

    81 (* Typing Terms *)

    82 | t1: "\<lbrakk>\<Sigma> \<turnstile> \<Gamma>  ctx; (x,A) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> (Var x) : A"

    83 | t2: "\<lbrakk>\<Sigma> \<turnstile> \<Gamma>  ctx; C_ass c A \<in> set \<Sigma>\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> (Const c) : A"

    84 | t3: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> M1 : \<Pi>[x:A2].A1; \<Sigma>,\<Gamma> \<turnstile> M2 : A2; atom x\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> (App M1 M2) : A1"

    85 | t4: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> A1 : Type; \<Sigma>,(x,A1)#\<Gamma> \<turnstile> M2 : A2; atom x\<sharp>(\<Gamma>,A1)\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> (Lam [x:A1].M2) : \<Pi>[x:A1].A2"

    86 | t5: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> M : A; \<Sigma>,\<Gamma> \<turnstile> A = B : Type\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> M : B "

    87 

    88 (* Typing Types *)

    89 | f1: "\<lbrakk>\<Sigma> \<turnstile> \<Gamma>  ctx; TC_ass a K \<in> set \<Sigma>\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> (TConst a) : K"

    90 | f2: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> A : \<Pi>[x:B].K; \<Sigma>,\<Gamma> \<turnstile> M : B; atom x\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> (TApp A M) : K"

    91 | f3: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> A1 : Type; \<Sigma>,(x,A1)#\<Gamma> \<turnstile> A2 : Type; atom x\<sharp>(\<Gamma>,A1)\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> (\<Pi>[x:A1].A2) : Type"

    92 | f4: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> A : K; \<Sigma>,\<Gamma> \<turnstile> K = L : Kind\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> A : L"

    93 

    94 (* Typing Kinds *)

    95 | k1: "\<Sigma> \<turnstile> \<Gamma> ctx \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> Type : Kind"

    96 | k2: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> A : Type; \<Sigma>,(x,A)#\<Gamma> \<turnstile> K : Kind; atom x\<sharp>(\<Gamma>,A)\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> (\<Pi>[x:A].K) : Kind"

    97 

    98 (* Simultaneous Congruence for Terms *)

    99 | q1: "\<lbrakk>\<Sigma> \<turnstile> \<Gamma>  ctx; (x,A) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> (Var x) = (Var x) : A"

   100 | q2: "\<lbrakk>\<Sigma> \<turnstile> \<Gamma>  ctx; C_ass c A \<in> set \<Sigma>\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> (Const c) = (Const c): A"

   101 | q3: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> M1 = N1 : \<Pi>[x:A2].A1; \<Sigma>,\<Gamma> \<turnstile> M2 = N2 : A2; atom x\<sharp>\<Gamma>\<rbrakk> 

   102        \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> (App M1 M2) = (App N1 N2) : A1"

   103 | q4: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> A1' = A1 : Type; \<Sigma>,\<Gamma> \<turnstile> A1'' = A1 : Type; \<Sigma>,\<Gamma> \<turnstile> A1 : Type;

   104         \<Sigma>,(x,A1)#\<Gamma> \<turnstile> M2 = N2 : A2; atom x\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> (Lam [x:A1'].M2) = (Lam [x:A1''].N2) : \<Pi>[x:A1].A2"

   105 

   106 (* Extensionality *)

   107 | ex: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> M : \<Pi>[x:A1].A2; \<Sigma>,\<Gamma> \<turnstile> N : \<Pi>[x:A1].A2; \<Sigma>,\<Gamma> \<turnstile> A1 : Type;

   108         \<Sigma>,(x,A1)#\<Gamma> \<turnstile> App M (Var x) = App N (Var x) : A2; atom x\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> M = N : \<Pi>[x:A1].A2"

   109 

   110 (* Parallel Conversion *)

   111 | pc: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> A1 : Type; \<Sigma>,(x,A1)#\<Gamma> \<turnstile> M2 = N2 : A2; \<Sigma>,\<Gamma> \<turnstile> M1 = N1 : A1; atom x\<sharp>\<Gamma>\<rbrakk> 

   112        \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> App (Lam [x:A1].M2) M1 = N2 : A2"

   113 

   114 (* Equivalence *)

   115 | e1: "\<Sigma>,\<Gamma> \<turnstile> M = N : A \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> N = M : (A::ty)"

   116 | e2: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> M = N : A; \<Sigma>,\<Gamma> \<turnstile> N = P : A\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> M = P : (A::ty)"

   117 (*| e3: "\<Sigma>,\<Gamma> \<turnstile> M : A \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> M = M : (A::ty)"*)

   118 

   119 (* Type conversion *)

   120 | tc: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> M = N : A; \<Sigma>,\<Gamma> \<turnstile> A = B : Type\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> M = N : B"

   121 

   122 (* Types Conruence *)

   123 | ft1: "\<lbrakk>\<Sigma> \<turnstile> \<Gamma>  ctx; TC_ass a K \<in> set \<Sigma>\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> (TConst a) = (TConst a) : K"

   124 | ft2: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> A = B : \<Pi>[x:C].K; \<Sigma>,\<Gamma> \<turnstile> M = N : C; atom x\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> (TApp A M) = (TApp B N) : K"

   125 | ft3: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> A1 = B1 : Type; \<Sigma>,\<Gamma> \<turnstile> A1 : Type; \<Sigma>,(x,A1)#\<Gamma> \<turnstile> A2 = B2 : Type; atom x\<sharp>\<Gamma>\<rbrakk> 

   126        \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> \<Pi>[x:A1].A2 = \<Pi>[x:B1].B2 : Type"

   127 

   128 (* Types Equivalence *)

   129 | fe1: "\<Sigma>,\<Gamma> \<turnstile> A = (B::ty) : (K::kind) \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> B = A : K"

   130 | fe2: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> A = B : K; \<Sigma>,\<Gamma> \<turnstile> B = C : K\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> A = C : (K::kind)"

   131 (*| fe3: "\<Sigma>,\<Gamma> \<turnstile> A : K \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> A = A : (K::kind)"*)

   132 

   133 (* Kind Conversion *)

   134 | kc: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> A = B : K; \<Sigma>,\<Gamma> \<turnstile> K = L : Kind\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> A = B : (L::kind)"

   135 

   136 (* Kind Congruence *)

   137 | kc1: "\<Sigma> \<turnstile> \<Gamma> ctx \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> Type = Type : Kind"

   138 | kc2: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> A = B : Type; \<Sigma>,\<Gamma> \<turnstile> A : Type; \<Sigma>,(x,A)#\<Gamma> \<turnstile> K = L : Kind; atom x\<sharp>\<Gamma>\<rbrakk> 

   139         \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> \<Pi>[x:A].K = \<Pi>[x:B].L : Kind"

   140 

   141 (* Kind Equivalence *)

   142 | ke1: "\<Sigma>,\<Gamma> \<turnstile> K = L : Kind \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> L = K : Kind"

   143 | ke2: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> K = L : Kind; \<Sigma>,\<Gamma> \<turnstile> L = L' : Kind\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> K = L' : Kind"

   144 (*| ke3: "\<Sigma>,\<Gamma> \<turnstile> K : Kind \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> K = K : Kind"*)

   145 

   146 (* type extensionality - needed in order to get the soundness theorem through*)

   147 | tex: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> A : \<Pi>[x:C].K; \<Sigma>,\<Gamma> \<turnstile> B : \<Pi>[x:C].K; \<Sigma>,\<Gamma> \<turnstile> C : Type; 

   148          \<Sigma>,(x,C)#\<Gamma> \<turnstile> TApp A (Var x) = TApp B (Var x) : K; atom x\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> A = B : \<Pi>[x:C].K"

   149 

   150 thm sig_valid_ctx_valid_trm_valid_ty_valid_kind_valid_trm_equiv_ty_equiv_kind_equiv_def

   151 thm sig_valid_def

   152 thm trm_valid_def

   153 thm ty_valid_def

   154 thm kind_valid_def

   155 thm trm_equiv_def

   156 thm kind_equiv_def

   157 thm ty_equiv_def