Add syntax and substitution for case expressions

Author: jvanbruegge

Defs.thy

@@ -35,9 +35,10 @@ nominal_function head_ctor :: "term \<Rightarrow> bool" where
 | "head_ctor (TApp e _) = head_ctor e"
 | "head_ctor (Ctor _) = True"
 | "head_ctor (Let _ _ _ _) = False"
+| "head_ctor (Case _ _) = False"
 proof goal_cases
   case (3 P x)
-  then show ?case by (cases x rule: term.exhaust)
+  then show ?case by (cases x rule: term_alts.exhaust(1))
 qed (auto simp: eqvt_def head_ctor_graph_aux_def)
 nominal_termination (eqvt) by lexicographic_order
 
@@ -49,44 +50,92 @@ nominal_function is_value :: "term => bool" where
 | "is_value (TApp e \<tau>) = head_ctor e"
 | "is_value (Ctor _) = True"
 | "is_value (Let x \<tau> e1 e2) = False"
+| "is_value (Case _ _) = False"
 proof goal_cases
   case (3 P x)
-  then show ?case by (cases x rule: term.exhaust)
+  then show ?case by (cases x rule: term_alts.exhaust(1))
 next
-  case (17 a k e a' k' e')
+  case (19 a k e a' k' e')
   obtain c::tyvar where c: "atom c \<sharp> (a, e, a', e')" by (rule obtain_fresh)
   have 1: "is_value_sumC e' = (a' \<leftrightarrow> c) \<bullet> is_value_sumC e'" using permute_boolE permute_boolI by blast
   have 2: "is_value_sumC e = (a \<leftrightarrow> c) \<bullet> is_value_sumC e" using permute_boolE permute_boolI by blast
-  from c have "(a \<leftrightarrow> c) \<bullet> e = (a' \<leftrightarrow> c) \<bullet> e'" using 17(5) by simp
-  then show ?case using 1 2 17(1,2) eqvt_at_def by metis
+  from c have "(a \<leftrightarrow> c) \<bullet> e = (a' \<leftrightarrow> c) \<bullet> e'" using 19(5) by simp
+  then show ?case using 1 2 19(1,2) eqvt_at_def by metis
 qed (auto simp: eqvt_def is_value_graph_aux_def)
 nominal_termination (eqvt) by lexicographic_order
 
-nominal_function subst_term :: "term => term \<Rightarrow> var => term" where
+nominal_function (default "case_sum (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)")
+  subst_term :: "term => term \<Rightarrow> var => term" and
+  subst_alts :: "alts \<Rightarrow> term \<Rightarrow> var \<Rightarrow> alts" where
   "subst_term (Var y) e x  = (if x = y then e else Var y)"
 | "subst_term (App e1 e2) e x = App (subst_term e1 e x) (subst_term e2 e x)"
 | "subst_term (TApp e1 \<tau>) e x = TApp (subst_term e1 e x) \<tau>"
 | "subst_term (Ctor D) _ _ = Ctor D"
+| "subst_term (Case t alts) e x = Case (subst_term t e x) (subst_alts alts e x)"
 | "atom y \<sharp> (e, x) \<Longrightarrow> subst_term (\<lambda> y:\<tau>. e2) e x = (\<lambda> y:\<tau>. subst_term e2 e x)"
 | "atom y \<sharp> (e, x) \<Longrightarrow> subst_term (\<Lambda> y:k. e2) e x = (\<Lambda> y:k. subst_term e2 e x)"
 | "atom y \<sharp> (e, x) \<Longrightarrow> subst_term (Let y \<tau> e1 e2) e x = Let y \<tau> (subst_term e1 e x) (subst_term e2 e x)"
+
+| "subst_alts ANil _ _ = ANil"
+| "set (map atom tys @ map atom vals) \<sharp>* (e, x) \<Longrightarrow> subst_alts (Alt D tys vals t) e x = Alt D tys vals (subst_term t e x)"
 proof (goal_cases)
+  (* this is adapted and simplified from here: https://www.joachim-breitner.de/thesis/isa/Substitution.thy *)
+  have eqvt_at_subst_term: "\<And>e y z . eqvt_at subst_term_subst_alts_sumC (Inl (e, y, z)) \<Longrightarrow> eqvt_at (\<lambda>(a, b, c). subst_term a b c) (e, y, z)"
+    apply (simp add: eqvt_at_def subst_term_def)
+    apply rule
+    apply (subst Projl_permute)
+     apply (simp add: subst_term_subst_alts_sumC_def)
+     apply (simp add: THE_default_def)
+     apply (case_tac "Ex1 (subst_term_subst_alts_graph (Inl (e, y, z)))")
+      apply(auto)[2]
+      apply (erule_tac x="x" in allE)
+      apply simp
+      apply(cases rule: subst_term_subst_alts_graph.cases)
+               apply(assumption)
+              apply blast+
+    apply simp
+    done
+
+{
   case (3 P x)
-  then obtain t e y where P: "x = (t, e, y)" by (metis prod.exhaust)
   then show ?case
-    apply (cases t rule: term.strong_exhaust[of _ _ "(e, y)"])
-          apply (auto simp: 3)
-    using 3(5-7) P fresh_star_def by blast+
+  proof (cases x)
+    case (Inl a)
+    then obtain t e y where P: "a = (t, e, y)" by (metis prod.exhaust)
+    then show ?thesis using Inl 3(1-5)
+    proof (cases t rule: term_alts.strong_exhaust(1)[of _ _ "(e, y)"])
+      case Lam
+      then show ?thesis using 3(6) fresh_star_def Inl P by blast
+    next
+      case TyLam
+      then show ?thesis using 3(7) fresh_star_def Inl P by blast
+    next
+      case Let
+      then show ?thesis using 3(8) fresh_star_def Inl P by blast
+    qed auto
+  next
+    case (Inr b)
+    then obtain xs e y where P: "b = (xs, e, y)" by (metis prod.exhaust)
+    then show ?thesis using Inr 3(9,10) by (cases xs rule: term_alts.strong_exhaust(2)[of _ _ "(e, y)"]) auto
+  qed
+next
+  case (44 y e x \<tau> e2 y' e' x' \<tau>' e2')
+  have "(\<lambda> y : \<tau> . subst_term e2 e x) = (\<lambda> y' : \<tau>' . subst_term e2' e' x')" using Abs_sumC[OF 44(5,6) eqvt_at_subst_term[OF 44(1)] eqvt_at_subst_term[OF 44(2)]] 44(7) by fastforce
+  then show ?case by (auto simp: Abs_fresh_iff meta_eq_to_obj_eq[OF subst_term_def, symmetric, unfolded fun_eq_iff])
 next
-  case (26 y e x \<tau> e2 y' e' x' \<tau>' e2')
-  then show ?case using Abs_sumC[OF 26(5,6,1,2)] by fastforce
+  case (49 y e x k e2 y' e' x' k' e2')
+  have "(\<Lambda> y : k . subst_term e2 e x) = (\<Lambda> y' : k' . subst_term e2' e' x')" using Abs_sumC[OF 49(5,6) eqvt_at_subst_term[OF 49(1)] eqvt_at_subst_term[OF 49(2)]] 49(7) by fastforce
+  then show ?case by (auto simp: Abs_fresh_iff meta_eq_to_obj_eq[OF subst_term_def, symmetric, unfolded fun_eq_iff])
 next
-  case (29 y e x k e2 y' e' x' k' e2')
-  then show ?case using Abs_sumC[OF 29(5,6,1,2)] by fastforce
+  case (53 y e x \<tau> e1 e2 y' e' x' \<tau>' e1' e2')
+  have "Let y \<tau> (subst_term e1 e x) (subst_term e2 e x) = Let y' \<tau>' (subst_term e1' e' x') (subst_term e2' e' x')"
+    using Abs_sumC[OF 53(9,10) eqvt_at_subst_term[OF 53(2)] eqvt_at_subst_term[OF 53(4)]] 53(11) by fastforce
+  then show ?case by (auto simp: Abs_fresh_iff meta_eq_to_obj_eq[OF subst_term_def, symmetric, unfolded fun_eq_iff])
 next
-  case (31 y e x \<tau> e1 e2 y' e' x' \<tau>' e1' e2')
-  then show ?case using Abs_sumC[OF 31(9,10,2,4)] by fastforce
-qed (auto simp: eqvt_def subst_term_graph_aux_def)
+  case (58 tys vals e x D t tys' vals' e' x' D' t')
+  have "Alt D tys vals (subst_term t e x) = Alt D' tys' vals' (subst_term t' e' x')" using Abs_sumC_star[OF 58(5,6) eqvt_at_subst_term[OF 58(1)] eqvt_at_subst_term[OF 58(2)]] 58(7) by fastforce
+  then show ?case by (auto simp: Abs_fresh_iff meta_eq_to_obj_eq[OF subst_term_def, symmetric, unfolded fun_eq_iff])
+} qed (auto simp: eqvt_def subst_term_subst_alts_graph_aux_def)
 nominal_termination (eqvt) by lexicographic_order
 
 nominal_function subst_type :: "\<tau> \<Rightarrow> \<tau> \<Rightarrow> tyvar \<Rightarrow> \<tau>" where
@@ -108,31 +157,77 @@ next
 qed (auto simp: eqvt_def subst_type_graph_aux_def)
 nominal_termination (eqvt) by lexicographic_order
 
-nominal_function subst_term_type :: "term \<Rightarrow> \<tau> \<Rightarrow> tyvar \<Rightarrow> term" where
+nominal_function (default "case_sum (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)")
+  subst_term_type :: "term \<Rightarrow> \<tau> \<Rightarrow> tyvar \<Rightarrow> term" and
+  subst_alts_type :: "alts \<Rightarrow> \<tau> \<Rightarrow> tyvar \<Rightarrow> alts"  where
   "subst_term_type (Var x) _ _ = Var x"
 | "subst_term_type (Ctor D) _ _ = Ctor D"
 | "subst_term_type (App e1 e2) \<tau> a = App (subst_term_type e1 \<tau> a) (subst_term_type e2 \<tau> a)"
 | "subst_term_type (TApp e \<tau>2) \<tau> a = TApp (subst_term_type e \<tau> a) (subst_type \<tau>2 \<tau> a)"
+| "subst_term_type (Case D alts) \<tau> a = Case D (subst_alts_type alts \<tau> a)"
 | "atom y \<sharp> (\<tau>, a) \<Longrightarrow> subst_term_type (\<lambda> y:\<tau>'. e2) \<tau> a = (\<lambda> y:(subst_type \<tau>' \<tau> a). subst_term_type e2 \<tau> a)"
 | "atom b \<sharp> (\<tau>, a) \<Longrightarrow> subst_term_type (\<Lambda> b:k. e2) \<tau> a = (\<Lambda> b:k. subst_term_type e2 \<tau> a)"
 | "atom y \<sharp> (\<tau>, a) \<Longrightarrow> subst_term_type (Let y \<tau>' e1 e2) \<tau> a = Let y (subst_type \<tau>' \<tau> a) (subst_term_type e1 \<tau> a) (subst_term_type e2 \<tau> a)"
+
+| "subst_alts_type ANil _ _ = ANil"
+| "set (map atom tys @ map atom vals) \<sharp>* (\<tau>, a) \<Longrightarrow> subst_alts_type (Alt D tys vals e) \<tau> a = Alt D tys vals (subst_term_type e \<tau> a)"
 proof goal_cases
+  (* this is adapted and simplified from here: https://www.joachim-breitner.de/thesis/isa/Substitution.thy *)
+  have eqvt_at_subst_term_type: "\<And>e y z . eqvt_at subst_term_type_subst_alts_type_sumC (Inl (e, y, z)) \<Longrightarrow> eqvt_at (\<lambda>(a, b, c). subst_term_type a b c) (e, y, z)"
+    apply (simp add: eqvt_at_def subst_term_type_def)
+    apply rule
+    apply (subst Projl_permute)
+     apply (simp add: subst_term_type_subst_alts_type_sumC_def)
+     apply (simp add: THE_default_def)
+     apply (case_tac "Ex1 (subst_term_type_subst_alts_type_graph (Inl (e, y, z)))")
+      apply(auto)[2]
+      apply (erule_tac x="x" in allE)
+      apply simp
+      apply(cases rule: subst_term_type_subst_alts_type_graph.cases)
+               apply(assumption)
+              apply blast+
+    apply simp
+    done
+{
   case (3 P x)
-  then obtain t \<tau> a where P: "x = (t, \<tau>, a)" by (metis prod.exhaust)
   then show ?case
-    apply (cases t rule: term.strong_exhaust[of _ _ "(\<tau>, a)"])
-    using 3 P apply auto[4]
-    using 3(5,6,7) P fresh_star_def by blast+
+  proof (cases x)
+    case (Inl a)
+    then obtain t \<tau> c where P: "a = (t, \<tau>, c)" by (metis prod.exhaust)
+    then show ?thesis using 3 Inl
+    proof (cases t rule: term_alts.strong_exhaust(1)[of _ _ "(\<tau>, c)"])
+      case Lam
+      then show ?thesis using 3(6) Inl P fresh_star_insert by blast
+    next
+      case TyLam
+      then show ?thesis using 3(7) Inl P fresh_star_insert by blast
+    next
+      case Let
+      then show ?thesis using 3(8) Inl P fresh_star_insert by blast
+    qed auto
+  next
+    case (Inr b)
+    then obtain xs \<tau> c where P: "b = (xs, \<tau>, c)" by (metis prod.exhaust)
+    then show ?thesis using 3 Inr by (cases xs rule: term_alts.strong_exhaust(2)[of _ _ "(\<tau>, c)"]) auto
+  qed
+next
+  case (44 y \<tau> a \<tau>2 e2 y' \<tau>' a' \<tau>2' e2')
+  have "(\<lambda> y : (subst_type \<tau>2 \<tau> a) . subst_term_type e2 \<tau> a) = (\<lambda> y' : (subst_type \<tau>2' \<tau>' a') . subst_term_type e2' \<tau>' a')" using Abs_sumC[OF 44(5,6) eqvt_at_subst_term_type[OF 44(1)] eqvt_at_subst_term_type[OF 44(2)]] 44(7) by fastforce
+  then show ?case by (auto simp: Abs_fresh_iff meta_eq_to_obj_eq[OF subst_term_type_def, symmetric, unfolded fun_eq_iff])
 next
-  case (26 y \<tau> a \<tau>1 e2 y' \<tau>' a' \<tau>1' e2')
-  then show ?case using Abs_sumC[OF 26(5,6,1,2)] by fastforce
+  case (49 b \<tau> a k e2 b' \<tau>' a' k' e2')
+  have "(\<Lambda> b : k . subst_term_type e2 \<tau> a) = (\<Lambda> b' : k' . subst_term_type e2' \<tau>' a')" using Abs_sumC[OF 49(5,6) eqvt_at_subst_term_type[OF 49(1)] eqvt_at_subst_term_type[OF 49(2)]] 49(7) by fastforce
+  then show ?case by (auto simp: Abs_fresh_iff meta_eq_to_obj_eq[OF subst_term_type_def, symmetric, unfolded fun_eq_iff])
 next
-  case (29 b \<tau> a k e2 b' \<tau>' a' k' e2')
-  then show ?case using Abs_sumC[OF 29(5,6,1,2)] by fastforce
+  case (53 y \<tau> a \<tau>2 e1 e2 y' \<tau>' a' \<tau>2' e1' e2')
+  have "Let y (subst_type \<tau>2 \<tau> a) (subst_term_type e1 \<tau> a) (subst_term_type e2 \<tau> a) = Let y' (subst_type \<tau>2' \<tau>' a') (subst_term_type e1' \<tau>' a') (subst_term_type e2' \<tau>' a')"
+    using Abs_sumC[OF 53(9,10) eqvt_at_subst_term_type[OF 53(2)]  eqvt_at_subst_term_type[OF 53(4)]] 53(11) by fastforce
+  then show ?case by (auto simp: Abs_fresh_iff meta_eq_to_obj_eq[OF subst_term_type_def, symmetric, unfolded fun_eq_iff])
 next
-  case (31 y \<tau> a \<tau>1 e1 e2 y' \<tau>' a' \<tau>1' e1' e2')
-  then show ?case using Abs_sumC[OF 31(9,10,2,4)] by fastforce
-qed (auto simp: eqvt_def subst_term_type_graph_aux_def)
+  case (58 tys vals \<tau> a D e tys' vals' \<tau>' a' D' e')
+  have "Alt D tys vals (subst_term_type e \<tau> a) = Alt D' tys' vals' (subst_term_type e' \<tau>' a')" using Abs_sumC_star[OF 58(5,6) eqvt_at_subst_term_type[OF 58(1)] eqvt_at_subst_term_type[OF 58(2)]] 58(7) by fastforce
+  then show ?case by (auto simp: Abs_fresh_iff meta_eq_to_obj_eq[OF subst_term_type_def, symmetric, unfolded fun_eq_iff])
+} qed (auto simp: eqvt_def subst_term_type_subst_alts_type_graph_aux_def)
 nominal_termination (eqvt) by lexicographic_order
 
 nominal_function subst_context :: "\<Gamma> \<Rightarrow> \<tau> \<Rightarrow> tyvar \<Rightarrow> \<Gamma>" where
@@ -154,6 +249,6 @@ no_notation inverse_divide (infixl "'/" 70)
 consts subst :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a" ("_[_'/_]" [1000,0,0] 1000)
 
 adhoc_overloading
-  subst subst_term subst_type subst_term_type subst_context
+  subst subst_term subst_alts subst_type subst_term_type subst_alts_type subst_context
 
 end

Nominal2_Lemmas.thy

@@ -62,6 +62,22 @@ proof -
   show ?thesis using 1 2 3 equal by argo
 qed
 
+lemma Abs_sumC_star:
+  fixes ys ys'::"atom list" and x::"'a::fs" and e::"'b::fs" and e2 e2'::"'c::fs" and f::"'c \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'd::fs"
+  assumes fresh: "set ys \<sharp>* (e, x)" "set ys' \<sharp>* (e', x')"
+  and eqvt_at: "eqvt_at (\<lambda>(a, b, c). f a b c) (e2, e, x)" "eqvt_at (\<lambda>(a, b, c). f a b c) (e2', e', x')"
+  and equal: "[ys]lst. e2 = [ys']lst. e2'" "e = e'" "x = x'"
+shows "[ys]lst. f e2 e x = [ys']lst. f e2' e x"
+proof -
+  have 1: "set ys \<sharp>* ([ys]lst. f e2 e x)" using Abs_fresh_star(3) by blast
+  have 2: "\<And>p. supp p \<sharp>* (e, x) \<Longrightarrow> p \<bullet> ([ys]lst. f e2 e x) = [p \<bullet> ys]lst. f (p \<bullet> e2) e x"
+    using eqvt_at(1) by (simp add: eqvt_at_def, simp add: fresh_star_Pair perm_supp_eq)
+  have 3: "\<And>p. supp p \<sharp>* (e, x) \<Longrightarrow> p \<bullet> ([ys']lst. f e2' e x) = [p \<bullet> ys']lst. f (p \<bullet> e2') e x"
+    using eqvt_at(2) equal(2,3) by (simp add: eqvt_at_def, simp add: fresh_star_Pair perm_supp_eq)
+
+  show ?thesis using Abs_lst_fcb2[where f="\<lambda>a b _. [a]lst. f b e x", OF equal(1) 1 fresh(1)] fresh(2) equal(2,3) 2 3 by argo
+qed
+
 lemma Abs_fresh_var:
   fixes y::"'a::at" and e ::"'b::fs"
   obtains c::"'a" and e'::"'b" where "([[atom y]]lst. e = [[atom c]]lst. e') \<and> atom y \<sharp> [[atom c]]lst. e'"
@@ -79,4 +95,7 @@ lemma Abs_rename_body:
   shows "(a \<leftrightarrow> b) \<bullet> e1 = e2"
   by (metis Abs1_eq_iff'(3) Nominal2_Base.swap_self assms flip_commute flip_def fresh_star_zero supp_perm_eq_test)
 
+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
+
 end

Syntax.thy

@@ -30,6 +30,10 @@ nominal_datatype "term" =
  | Lam x::"var" "\<tau>" e::"term" binds x in e  ("\<lambda> _ : _ . _" 50)
  | TyLam a::"tyvar" "\<kappa>" e::"term" binds a in e ("\<Lambda> _ : _ . _" 50)
  | Let x::"var" "\<tau>" "term" e2::"term" binds x in e2
+ | Case "term" alts
+and alts =
+  ANil
+| Alt "ctor_name" tys::"tyvar list" terms::"var list" e::"term" binds tys terms in e
 
 nominal_datatype "binder" =
   BVar "var" "\<tau>"