WIP

Defs.thy

@@ -42,15 +42,13 @@ proof goal_cases
 qed (auto simp: eqvt_def head_ctor_graph_aux_def)
 nominal_termination (eqvt) by lexicographic_order
 
-nominal_function head_data :: "\<tau> \<Rightarrow> data_name option" where
+nominal_function head_data :: "\<tau> \<Rightarrow> (data_name * \<tau> list) option" where
   "head_data (TyVar _) = None"
-| "head_data (TyData T) = Some T"
+| "head_data (TyData T) = Some (T, [])"
 | "head_data TyArrow = None"
-| "head_data (TyApp (TyData T) _) = Some T"
-| "head_data (TyApp (TyVar _) _) = None"
-| "head_data (TyApp TyArrow _) = None"
-| "head_data (TyApp (TyApp _ _) _) = None"
-| "head_data (TyApp (TyForall _ _ _) _) = None"
+| "head_data (TyApp \<tau>1 \<tau>2) = (case head_data \<tau>1 of
+    Some (T, xs) \<Rightarrow> Some (T, xs @ [\<tau>2])
+  | None \<Rightarrow> None)"
 | "head_data (TyForall _ _ _) = None"
 proof goal_cases
   case (3 P x)
@@ -59,7 +57,7 @@ proof goal_cases
     case (TyApp \<tau>1 \<tau>2)
     then show ?thesis using 3 by (cases \<tau>1 rule: \<tau>.exhaust) auto
   qed
-qed (auto simp: eqvt_def head_data_graph_aux_def)
+qed (auto simp: eqvt_def head_data_graph_aux_def split!: option.splits)
 nominal_termination (eqvt) by lexicographic_order
 
 nominal_function set_alt_list :: "alt_list \<Rightarrow> alt set" where
@@ -76,23 +74,23 @@ nominal_function ctor_data_app :: "\<tau> \<Rightarrow> (data_name * tyvar list)
 | "ctor_data_app (TyData T) = Some (T, [])"
 | "ctor_data_app TyArrow = None"
 | "ctor_data_app (TyApp \<tau>1 (TyVar a)) = (case ctor_data_app \<tau>1 of
-    Some (T, s) \<Rightarrow> Some (T, a#s)
+    Some (T, tys) \<Rightarrow> Some (T, a#tys)
   | None \<Rightarrow> None)"
 | "ctor_data_app (TyApp _ (TyData _)) = None"
 | "ctor_data_app (TyApp _ TyArrow) = None"
 | "ctor_data_app (TyApp _ (TyApp _ _)) = None"
 | "ctor_data_app (TyApp _ (TyForall _ _ _)) = None"
 | "ctor_data_app (TyForall _ _ _) = None"
 proof goal_cases
-  case 1
+case 1
   then show ?case by (auto simp: eqvt_def ctor_data_app_graph_aux_def split!: option.splits)
 next
   case (3 P x)
   then show ?case
   proof (cases x rule: \<tau>.exhaust)
     case (TyApp \<tau>1 \<tau>2)
     then show ?thesis using 3 by (cases \<tau>2 rule: \<tau>.exhaust) auto
-  qed (auto simp: 3)
+  qed auto
 qed auto
 nominal_termination (eqvt) by lexicographic_order
 
@@ -112,38 +110,38 @@ nominal_function ctor_type_app :: "\<tau> \<Rightarrow> (data_name * tyvar list)
 | "ctor_type_app (TyForall _ _ _) = None"
 proof goal_cases
   case (3 P x)
-  show ?case using 3(1-3,13)
+  then show ?case
   proof (cases x rule: \<tau>.exhaust)
     case outer: (TyApp \<tau>1 \<tau>2)
-    then show ?thesis using 3(9-12)
+    then show ?thesis using 3
     proof (cases \<tau>1 rule: \<tau>.exhaust)
-      case inner: (TyApp \<tau>1' \<tau>2')
-      then show ?thesis using outer 3(4-8) by (cases \<tau>1' rule: \<tau>.exhaust) blast+
-    qed blast+
-  qed blast+
+      case (TyApp \<sigma>1 \<sigma>2)
+      then show ?thesis using outer 3 by (cases \<sigma>1 rule: \<tau>.exhaust) auto
+    qed auto
+  qed auto
 next
   case (74 a k e \<tau>1 \<tau>2 a k e \<tau>1 \<tau>2)
-  then show ?case by (simp add: 74)
+  then show ?case by presburger
 next
   case (92 a k e \<tau>2 a k e \<tau>2)
-  then show ?case by (simp add: 92)
+  then show ?case by presburger
 qed (auto simp: eqvt_def ctor_type_app_graph_aux_def)
 nominal_termination (eqvt) by lexicographic_order
 
-nominal_function ctor_type_forall :: "\<tau> \<Rightarrow> (data_name * tyvar list) option" where
+nominal_function ctor_type_forall :: "\<tau> \<Rightarrow> (data_name * tyvar list * \<kappa> list) option" where
   "ctor_type_forall (TyVar _) = None"
-| "ctor_type_forall (TyData T) = Some (T, [])"
+| "ctor_type_forall (TyData T) = Some (T, [], [])"
 | "ctor_type_forall TyArrow = None"
-| "ctor_type_forall (TyApp \<tau>1 \<tau>2) = ctor_type_app (TyApp \<tau>1 \<tau>2)"
-| "ctor_type_forall (TyForall a _ e) = (case ctor_type_forall e of
-    Some (T, s) \<Rightarrow> (if a \<in> set s then Some (T, filter (\<lambda>x. x \<noteq> a) s) else None)
-  | None \<Rightarrow> None)"
+| "ctor_type_forall (TyApp \<tau>1 \<tau>2) = (case ctor_type_app (TyApp \<tau>1 \<tau>2) of Some (T, tys) \<Rightarrow> Some (T, tys, []) | None \<Rightarrow> None)"
+| "ctor_type_forall (TyForall a k e) = (case ctor_type_forall e of
+    Some (T, xs, ks) \<Rightarrow> (if a \<in> set xs then Some (T, filter (\<lambda>x. x \<noteq> a) xs, k#ks) else None)
+  | _ \<Rightarrow> None)"
 proof goal_cases
   case 1
   then show ?case by (auto simp: eqvt_def ctor_type_forall_graph_aux_def split!: option.splits list.splits)
 next
   case (3 P x)
-  then show ?case by (cases x rule: \<tau>.exhaust)
+  then show ?case by (cases x rule: \<tau>.exhaust) auto
 next
   case (18 a k e a' k' e')
   obtain c::tyvar where P: "atom c \<sharp> (a, e, a', e', ctor_type_forall_sumC e, ctor_type_forall_sumC e')" by (rule obtain_fresh)
@@ -154,9 +152,10 @@ next
   then show ?case
   proof (cases "ctor_type_forall_sumC e")
     case (Some t)
-    then obtain T s where P1: "t = (T, s)" by fastforce
-    from Some obtain T' s' where P2: "ctor_type_forall_sumC e' = Some (T', s')" using 3 by auto
-    have "T = T'" using "2" P1 P2 Some Some_eqvt option.inject perm_data_name_tyvar by auto
+    then obtain T s ks where P1: "t = (T, s, ks)" by (metis prod.exhaust)
+    from Some obtain T' s' ks' where P2: "ctor_type_forall_sumC e' = Some (T', s', ks')" using 3 by auto
+    then have pairs: "(a \<leftrightarrow> c) \<bullet> (T, s, ks) = (a' \<leftrightarrow> c) \<bullet> (T', s', ks')" using 2 P1 Some Some_eqvt option.inject by simp
+    from pairs have "T = T'" "ks = ks'" by auto
     have same: "(a \<leftrightarrow> c) \<bullet> s = (a' \<leftrightarrow> c) \<bullet> s'" using "2" P1 P2 Some by auto
     have x: "a \<in> set s \<longleftrightarrow> a' \<in> set s'" by (metis flip_at_simps(2) mem_permute_iff permute_flip_cancel same set_eqvt)
     have 4: "atom c \<sharp> s" using c(5) Some P1 fresh_Some fresh_Pair by metis
@@ -167,19 +166,26 @@ next
     also have "... = filter (\<lambda>x. x \<noteq> c) ((a' \<leftrightarrow> c) \<bullet> s')" using same by argo
     also have "... = (a' \<leftrightarrow> c) \<bullet> filter (\<lambda>x. x \<noteq> a') s'" by simp
     also have "... = filter (\<lambda>x. x \<noteq> a') s'" using 6 flip_fresh_fresh by blast
-    finally have 9: "Some (T, filter (\<lambda>x. x \<noteq> a) s) = Some (T', filter (\<lambda>x. x \<noteq> a') s')" using \<open>T = T'\<close> by blast
-    then show ?thesis using Some P1 P2 x by simp
+    finally have 9: "Some (T, filter (\<lambda>x. x \<noteq> a) s, ks) = Some (T', filter (\<lambda>x. x \<noteq> a') s', ks')" using \<open>T = T'\<close> \<open>ks = ks'\<close> by blast
+    then show ?thesis
+    proof (cases "a \<in> set s")
+      case True
+      then show ?thesis using Some P1 P2 x 18(5) 9 by simp
+    next
+      case False
+      then show ?thesis using P1 P2 Some x by force
+    qed  
   qed simp
 qed auto
 nominal_termination (eqvt) by lexicographic_order
 
 (* This function checks if a type has the form \<forall>[a:k]. [\<tau>] \<rightarrow> T [a] *)
-nominal_function ctor_type :: "\<tau> \<Rightarrow> data_name option" where
+nominal_function ctor_type :: "\<tau> \<Rightarrow> (data_name * \<kappa> list) option" where
   "ctor_type (TyVar a) = None"
-| "ctor_type (TyData T) = Some T"
+| "ctor_type (TyData T) = Some (T, [])"
 | "ctor_type TyArrow = None"
-| "ctor_type (TyApp \<tau>1 \<tau>2) = (case ctor_type_app (TyApp \<tau>1 \<tau>2) of Some (T, []) \<Rightarrow> Some T | _ \<Rightarrow> None)"
-| "ctor_type (TyForall a k e) = (case ctor_type_forall (TyForall a k e) of Some (T, []) \<Rightarrow> Some T | _ \<Rightarrow> None)"
+| "ctor_type (TyApp \<tau>1 \<tau>2) = (case ctor_type_app (TyApp \<tau>1 \<tau>2) of Some (T, []) \<Rightarrow> Some (T, []) | _ \<Rightarrow> None)"
+| "ctor_type (TyForall a k e) = (case ctor_type_forall (TyForall a k e) of Some (T, [], ks) \<Rightarrow> Some (T, k#ks) | _ \<Rightarrow> None)"
 proof goal_cases
   case 1
   then show ?case by (auto simp: eqvt_def ctor_type_graph_aux_def split!: option.splits list.splits)
@@ -188,18 +194,34 @@ next
   then show ?case by (cases x rule: \<tau>.exhaust)
 next
   case (18 a k e a' k' e')
-  then show ?case by (simp add: 18)
+  have "(case ctor_type_forall (\<forall> a' : k' . e') of None \<Rightarrow> None | Some (d, [], ks) \<Rightarrow> Some (d, k # ks) | Some (d, t # x, ks) \<Rightarrow> Map.empty x) = (case ctor_type_forall (\<forall> a' : k' . e') of None \<Rightarrow> None | Some (d, [], ks) \<Rightarrow> Some (d, k' # ks) | Some (d, t # x, ks) \<Rightarrow> Map.empty x)"
+    using "18" by fastforce
+  then show ?case
+    by (simp add: "18")
 qed auto
 nominal_termination (eqvt) by lexicographic_order
 
 abbreviation exhaustive :: "alt_list \<Rightarrow> \<Delta> \<Rightarrow> data_name \<Rightarrow> bool" where
   "exhaustive alts \<Delta> T \<equiv>
     (\<nexists>x e. MatchVar x e \<in> set_alt_list alts) \<longrightarrow>
-      (\<forall>D \<tau>.
-          (AxCtor D \<tau> \<in> set \<Delta> \<and> ctor_type \<tau> = Some T) \<longrightarrow>
+      (\<forall>D \<tau> ks.
+          (AxCtor D \<tau> \<in> set \<Delta> \<and> ctor_type \<tau> = Some (T, ks)) \<longrightarrow>
           (\<exists>tys vals e. MatchCtor D tys vals e \<in> set_alt_list alts)
       )"
 
+nominal_function zip_with :: "('a::pt \<Rightarrow> 'b::pt \<Rightarrow> 'c::pt) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" where
+  "zip_with _ [] _ = []"
+| "zip_with _ _ [] = []"
+| "zip_with f (a#as) (b#bs) = f a b # zip_with f as bs"
+proof goal_cases
+  case (3 P x)
+  then show ?case sorry
+qed (auto simp: eqvt_def zip_with_graph_aux_def)
+nominal_termination (eqvt) by lexicographic_order
+
+lemma zip_with_length[simp]: "length (zip_with f as bs) = min (length as) (length bs)"
+  by (induction f as bs rule: zip_with.induct) auto
+
 nominal_function is_value :: "term => bool" where
   "is_value (Var x) = False"
 | "is_value (\<lambda> x : \<tau> . e) = True"

Nominal2_Lemmas.thy

@@ -99,4 +99,7 @@ lemma fresh_filter: "a = b \<or> atom a \<sharp> xs \<Longrightarrow> atom a \<s
 lemma Projl_permute: "\<exists>y. f = Inl y \<Longrightarrow> p \<bullet> projl f = projl (p \<bullet> f)" by auto
 lemma Projr_permute: "\<exists>y. f = Inr y \<Longrightarrow> p \<bullet> projr f = projr (p \<bullet> f)" by auto
 
+lemma pair3_eqvt[simp]: "(a \<leftrightarrow> b) \<bullet> (x, y, z) = ((a \<leftrightarrow> b) \<bullet> x, (a \<leftrightarrow> b) \<bullet> y, (a \<leftrightarrow> b) \<bullet> z)"
+  by (simp split: prod.splits)
+
 end

Semantics.thy

@@ -18,6 +18,8 @@ inductive Step :: "term \<Rightarrow> term \<Rightarrow> bool" ("_ \<longrightar
 
 | ST_Let: "Let x \<tau> e1 e2 \<longrightarrow> e2[e1/x]"
 
+| ST_Case_Cong: "e \<longrightarrow> e' \<Longrightarrow> Case e alts \<longrightarrow> Case e' alts"
+
 equivariance Step
 nominal_inductive Step .
 

Syntax.thy

@@ -78,5 +78,13 @@ lemma perm_ctor_name_var[simp]: "((a::var) \<leftrightarrow> b) \<bullet> (D ::
   using flip_fresh_fresh by force
 lemma perm_ctor_name_tyvar[simp]: "((a::tyvar) \<leftrightarrow> b) \<bullet> (D :: ctor_name) = D"
   using flip_fresh_fresh by force
+lemma perm_kind_var[simp]: "((a::var) \<leftrightarrow> b) \<bullet> (k::\<kappa>) = k"
+  using supp_empty_kinds flip_fresh_fresh fresh_def by blast
+lemma perm_kind_tyvar[simp]: "((a::tyvar) \<leftrightarrow> b) \<bullet> (k::\<kappa>) = k"
+  using supp_empty_kinds flip_fresh_fresh fresh_def by blast
+lemma perm_kind_list_var[simp]: "((a::var) \<leftrightarrow> b) \<bullet> (ks::\<kappa> list) = ks"
+  by (induction ks) auto
+lemma perm_kind_list_tyvar[simp]: "((a::tyvar) \<leftrightarrow> b) \<bullet> (ks::\<kappa> list) = ks"
+  by (induction ks) auto
 
 end

Typing.thy

@@ -12,7 +12,7 @@ inductive Ax :: "\<Delta> \<Rightarrow> bool" ("\<turnstile> _")
 
 | Ax_Data: "\<lbrakk> \<turnstile> \<Delta> ; atom T \<sharp> \<Delta> \<rbrakk> \<Longrightarrow> \<turnstile> AxData T \<kappa> # \<Delta>"
 
-| Ax_Ctor: "\<lbrakk> [] , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : \<star> ; ctor_type \<tau> = Some T ; atom D \<sharp> \<Delta> \<rbrakk> \<Longrightarrow> \<turnstile> AxCtor D \<tau> # \<Delta>"
+| Ax_Ctor: "\<lbrakk> [] , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : \<star> ; ctor_type \<tau> = Some (T, ks, tys) ; atom D \<sharp> \<Delta> \<rbrakk> \<Longrightarrow> \<turnstile> AxCtor D \<tau> # \<Delta>"
 
 (* ------------------------------ *)
 
@@ -36,7 +36,8 @@ inductive Ax :: "\<Delta> \<Rightarrow> bool" ("\<turnstile> _")
 
 equivariance Ax
 
-inductive Tm :: "\<Gamma> \<Rightarrow> \<Delta> \<Rightarrow> term \<Rightarrow> \<tau> \<Rightarrow> bool" ("_ , _ \<turnstile> _ : _" 50) where
+inductive Tm :: "\<Gamma> \<Rightarrow> \<Delta> \<Rightarrow> term \<Rightarrow> \<tau> \<Rightarrow> bool" ("_ , _ \<turnstile> _ : _" 50) and
+          Alts :: "\<Gamma> \<Rightarrow> \<Delta> \<Rightarrow> data_name \<Rightarrow> \<tau> list \<Rightarrow> \<tau> \<Rightarrow> alt_list \<Rightarrow> \<tau> \<Rightarrow> bool" where
   Tm_Var: "\<lbrakk> \<Delta> \<turnstile> \<Gamma> ; BVar x \<tau> \<in> \<Gamma> \<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile> (Var x) : \<tau>"
 
 | Tm_Abs: "BVar x \<tau>1 # \<Gamma> , \<Delta> \<turnstile> e : \<tau>2 \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile> (\<lambda> x : \<tau>1 . e) : (\<tau>1 \<rightarrow> \<tau>2)"
@@ -51,9 +52,16 @@ inductive Tm :: "\<Gamma> \<Rightarrow> \<Delta> \<Rightarrow> term \<Rightarrow
 
 | Tm_Let: "\<lbrakk> \<Gamma> , \<Delta> \<turnstile> e1 : \<tau>1 ; BVar x \<tau>1 # \<Gamma> , \<Delta> \<turnstile> e2 : \<tau>2 \<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile> Let x \<tau>1 e1 e2 : \<tau>2"
 
-| Tm_Case: "\<lbrakk> \<Gamma> , \<Delta> \<turnstile> e : \<tau>1 ; head_data \<tau>1 = Some T ; \<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : \<star> ; exhaustive alts \<Delta> T ;
-    \<forall>m\<in>set_alt_list alts.  True
-  \<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile> Case e alts : \<tau>"
+| Tm_Case: "\<lbrakk> \<Gamma> , \<Delta> \<turnstile> e : \<tau>1 ; head_data \<tau>1 = Some (T, \<sigma>s) ; \<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : \<star> ;
+             exhaustive alts \<Delta> T ; Alts \<Gamma> \<Delta> T \<sigma>s \<tau>1 alts \<tau> \<rbrakk> \<Longrightarrow> \<Gamma> , \<Delta> \<turnstile> Case e alts : \<tau>"
+
+| Alts_Nil: "Alts _ _ _ _ _ ANil _"
+
+| Alts_Var: "\<lbrakk> BVar x \<tau>1#\<Gamma>, \<Delta> \<turnstile> e : \<tau> ; Alts \<Gamma> \<Delta> T \<sigma>s \<tau>1 alts \<tau> \<rbrakk> \<Longrightarrow> Alts \<Gamma> \<Delta> T \<sigma>s \<tau>1 (ACons (MatchVar x e) alts) \<tau>"
+
+| Alts_Ctor: "\<lbrakk> AxCtor K cty \<in> set \<Delta> ; ctor_type cty = Some (T, ks, args) ; length ks = length tys ;
+              length args = length vals ; (zip_with BVar vals args) @ (zip_with BTyVar tys ks) @ \<Gamma>, \<Delta> \<turnstile> e : \<tau> ;  Alts \<Gamma> \<Delta> T \<sigma>s \<tau>1 alts \<tau> 
+              \<rbrakk> \<Longrightarrow> Alts \<Gamma> \<Delta> T \<sigma>s \<tau>1 (ACons (MatchCtor K tys vals e) alts) \<tau>"
 
 equivariance Tm