Adjust Lemmas

jvanbruegge · Feb 13, 2021 · d4d09ee · d4d09ee
1 parent 60fdf1f
commit d4d09ee
Show file tree

Hide file tree

Showing 3 changed files with 127 additions and 35 deletions.
diff --git a/Defs.thy b/Defs.thy
@@ -164,7 +164,7 @@ nominal_function (default "case_sum (\<lambda>x. Inl undefined) (\<lambda>x. Inr
 | "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)"
+| "subst_term_type (Case e alts) \<tau> a = Case (subst_term_type e \<tau> a) (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)"