Add higher kinded types (#9)

Author: jvanbruegge

Defs.thy

@@ -5,9 +5,9 @@ begin
 nominal_function isin :: "binder \<Rightarrow> \<Gamma> \<Rightarrow> bool" (infixr "\<in>" 80) where
   "isin _ [] = False"
 | "isin (BVar x t) (BVar y t'#xs) = (if x = y then t = t' else isin (BVar x t) xs)"
-| "isin (BVar x t) (BTyVar a#xs) = isin (BVar x t) xs"
-| "isin (BTyVar a) (BVar x t#xs) = isin (BTyVar a) xs"
-| "isin (BTyVar a) (BTyVar b#xs) = (if a = b then True else isin (BTyVar a) xs)"
+| "isin (BVar x t) (BTyVar _ _#xs) = isin (BVar x t) xs"
+| "isin (BTyVar a k) (BVar _ _#xs) = isin (BTyVar a k) xs"
+| "isin (BTyVar a k1) (BTyVar b k2#xs) = (if a = b then k1 = k2 else isin (BTyVar a k1) xs)"
 proof goal_cases
   case (3 P x)
   then obtain t ys where P: "x = (t, ys)" by (metis prod.exhaust)
@@ -32,7 +32,7 @@ is_value :: "term => bool"
 where
 "is_value (Var x) = False"
 | "is_value (\<lambda> x : \<tau> . e) = True"
-| "is_value (\<Lambda> a . e) = True"
+| "is_value (\<Lambda> a : k . e) = True"
 | "is_value (App e1 e2) = False"
 | "is_value (TyApp e \<tau>) = False"
 | "is_value Unit = True"
@@ -45,7 +45,7 @@ nominal_termination (eqvt) by lexicographic_order
 nominal_function subst_term :: "term => var => term => term" where
   "subst_term e x (Var y) = (if x=y then e else Var y)"
 | "atom y \<sharp> (e, x) \<Longrightarrow> subst_term e x (\<lambda> y : \<tau> . e2) = (Lam y \<tau> (subst_term e x e2))"
-| "atom y \<sharp> (e, x) \<Longrightarrow> subst_term e x (\<Lambda> y . e2) = (\<Lambda> y . subst_term e x e2)"
+| "atom y \<sharp> (e, x) \<Longrightarrow> subst_term e x (\<Lambda> y : k . e2) = (\<Lambda> y : k . subst_term e x e2)"
 | "subst_term e x (App e1 e2) = (App (subst_term e x e1) (subst_term e x e2))"
 | "subst_term e x (TyApp e1 \<tau>) = (TyApp (subst_term e x e1) \<tau>)"
 | "subst_term _ _ Unit = Unit"
@@ -73,25 +73,26 @@ nominal_function subst_type :: "\<tau> \<Rightarrow> tyvar \<Rightarrow> \<tau>
   "subst_type _ _ TyUnit = TyUnit"
 | "subst_type \<tau> a (TyVar b) = (if a=b then \<tau> else TyVar b)"
 | "subst_type \<tau> a (TyArrow \<tau>1 \<tau>2) = TyArrow (subst_type \<tau> a \<tau>1) (subst_type \<tau> a \<tau>2)"
-| "atom b \<sharp> (\<tau>, a) \<Longrightarrow> subst_type \<tau> a (TyForall b \<sigma>) = TyForall b (subst_type \<tau> a \<sigma>)"
+| "subst_type \<tau> a (TyConApp \<tau>1 \<tau>2) = TyConApp (subst_type \<tau> a \<tau>1) (subst_type \<tau> a \<tau>2)"
+| "atom b \<sharp> (\<tau>, a) \<Longrightarrow> subst_type \<tau> a (TyForall b k \<sigma>) = TyForall b k (subst_type \<tau> a \<sigma>)"
 proof goal_cases
   case (3 P x)
   then obtain \<tau> a t where P: "x = (\<tau>, a, t)" by (metis prod.exhaust)
   then show ?case
     apply (cases t rule: \<tau>.strong_exhaust[of _ _ "(\<tau>, a)"])
        apply (auto simp: 3)
-    using 3(4) P fresh_star_def by blast
+    using 3(5) P fresh_star_def by blast
 next
-  case (13 b \<tau> a \<sigma> b' \<tau>' a' \<sigma>')
-  then show ?case using Abs_sumC[OF 13(5) 13(6) 13(1) 13(2)] by fastforce
+  case (18 b \<tau> a k \<sigma> b' \<tau>' a' k' \<sigma>')
+  then show ?case using Abs_sumC[OF 18(5) 18(6) 18(1) 18(2)] by fastforce
 qed (auto simp: eqvt_def subst_type_graph_aux_def)
 nominal_termination (eqvt) by lexicographic_order
 
 nominal_function subst_term_type :: "\<tau> \<Rightarrow> tyvar \<Rightarrow> term \<Rightarrow> term" where
   "subst_term_type _ _ (Var x) = Var x"
 | "subst_term_type _ _ Unit = Unit"
 | "atom y \<sharp> (\<tau>, a) \<Longrightarrow> subst_term_type \<tau> a (\<lambda> y : \<tau>' . e2) = (Lam y (subst_type \<tau> a \<tau>') (subst_term_type \<tau> a e2))"
-| "atom b \<sharp> (\<tau>, a) \<Longrightarrow> subst_term_type \<tau> a (\<Lambda> b . e2) = (TyLam b (subst_term_type \<tau> a e2))"
+| "atom b \<sharp> (\<tau>, a) \<Longrightarrow> subst_term_type \<tau> a (\<Lambda> b : k . e2) = (TyLam b k (subst_term_type \<tau> a e2))"
 | "subst_term_type \<tau> a (App e1 e2) = App (subst_term_type \<tau> a e1) (subst_term_type \<tau> a e2)"
 | "subst_term_type \<tau> a (TyApp e \<tau>2) = TyApp (subst_term_type \<tau> a e) (subst_type \<tau> a \<tau>2)"
 | "atom y \<sharp> (\<tau>, a) \<Longrightarrow> subst_term_type \<tau> a (Let y \<tau>' e1 e2) = Let y (subst_type \<tau> a \<tau>') (subst_term_type \<tau> a e1) (subst_term_type \<tau> a e2)"

Lemmas.thy

@@ -17,7 +17,14 @@ proof (nominal_induct e avoiding: c x e' rule: term.strong_induct)
   then show ?case by (smt flip_fresh_fresh fresh_Pair fresh_at_base(2) list.set(1) list.set(2) no_vars_in_ty singletonD subst_term.simps(7) term.fresh(7) term.perm_simps(7))
 qed (auto simp: flip_fresh_fresh fresh_at_base)
 lemma subst_type_var_name: "atom c \<sharp> \<sigma> \<Longrightarrow> subst_type \<tau> a \<sigma> = subst_type \<tau> c ((a \<leftrightarrow> c) \<bullet> \<sigma>)"
-  by (nominal_induct \<sigma> avoiding: c a \<tau> rule: \<tau>.strong_induct) (auto simp: fresh_at_base)
+proof (nominal_induct \<sigma> avoiding: c a \<tau> rule: \<tau>.strong_induct)
+  case (TyForall b k \<sigma>)
+  then have 1: "atom c \<sharp> \<sigma>" by (simp add: fresh_at_base)
+  have "subst_type \<tau> a \<sigma> = subst_type \<tau> c ((a \<leftrightarrow> c) \<bullet> \<sigma>)" by (rule TyForall(4)[OF 1])
+  then show ?case
+    by (smt TyForall.hyps(1) TyForall.hyps(2) TyForall.hyps(3) \<tau>.perm_simps(5) flip_fresh_fresh fresh_Pair fresh_at_base(2) no_tyvars_in_kinds subst_type.simps(5))
+qed (auto simp: fresh_at_base)
+
 lemma subst_term_type_var_name: "atom c \<sharp> e \<Longrightarrow> subst_term_type \<tau> a e = subst_term_type \<tau> c ((a \<leftrightarrow> c) \<bullet> e)"
 proof (nominal_induct e avoiding: c a \<tau> rule: term.strong_induct)
   case (Lam x \<tau>1 e)
@@ -38,7 +45,7 @@ lemma subst_term_type_same: "[[atom a]]lst. e = [[atom a']]lst. e' \<Longrightar
   by (metis Abs1_eq_iff(3) flip_commute subst_term_type_var_name)
 
 (* atom x \<sharp> \<Gamma> \<Longrightarrow> \<not>isin (B x _) \<Gamma> *)
-lemma fresh_not_isin_tyvar: "atom a \<sharp> \<Gamma> \<Longrightarrow> \<not>isin (BTyVar a) \<Gamma>"
+lemma fresh_not_isin_tyvar: "atom a \<sharp> \<Gamma> \<Longrightarrow> \<not>isin (BTyVar a k) \<Gamma>"
   apply (induction \<Gamma>) apply simp
   by (metis binder.fresh(2) binder.strong_exhaust fresh_Cons fresh_at_base(2) isin.simps(4) isin.simps(5))
 lemma fresh_not_isin_var: "atom x \<sharp> \<Gamma> \<Longrightarrow> \<not>isin (BVar x \<tau>) \<Gamma>"
@@ -57,7 +64,7 @@ qed auto
 
 lemma fresh_subst_type_same: "atom a \<sharp> \<sigma> \<Longrightarrow> subst_type \<tau> a \<sigma> = \<sigma>"
 proof (induction \<tau> a \<sigma> rule: subst_type.induct)
-  case (4 b \<tau> a \<sigma>)
+  case (5 b \<tau> a k \<sigma>)
   then show ?case
     using fresh_Pair fresh_at_base(2) fresh_def list.set(1) list.set(2) subst_type.simps(4) by fastforce
 qed auto
@@ -79,8 +86,7 @@ case (TyVar x)
   then show ?case using fresh_at_base(2) fresh_subst_type_same by auto
 next
   case (TyForall x1 x2a)
-  then show ?case
-    by (smt flip_at_simps(1) flip_at_simps(2) flip_commute fresh_Pair fresh_subst_type fresh_subst_type_same subst_type.eqvt subst_type.simps(4) subst_type_var_name)
+  then show ?case using fresh_subst_type subst_type_var_name by auto
 qed (auto simp: fresh_subst_type)
 
 end

Semantics.thy

@@ -12,7 +12,7 @@ inductive Step :: "term \<Rightarrow> term \<Rightarrow> bool" ("_ \<longrightar
 
 | ST_SubstI: "Let x \<tau> v e \<longrightarrow> subst_term v x e"
 
-| ST_BetaTI: "TyApp (\<Lambda> a . e) \<tau> \<longrightarrow> subst_term_type \<tau> a e"
+| ST_BetaTI: "TyApp (\<Lambda> a : k . e) \<tau> \<longrightarrow> subst_term_type \<tau> a e"
 
 | ST_AppTI: "e1 \<longrightarrow> e2 \<Longrightarrow> TyApp e1 \<tau> \<longrightarrow> TyApp e2 \<tau>"
 equivariance Step