Add data types (#13)

Author: jvanbruegge

Defs.thy

@@ -1,5 +1,5 @@
 theory Defs
-  imports Syntax Nominal2_Lemmas
+  imports Syntax Nominal2_Lemmas "HOL-Library.Adhoc_Overloading"
 begin
 
 nominal_function isin :: "binder \<Rightarrow> \<Gamma> \<Rightarrow> bool" (infixr "\<in>" 80) where
@@ -27,28 +27,49 @@ proof goal_cases
 qed (auto simp: eqvt_def isin_graph_aux_def)
 nominal_termination (eqvt) by lexicographic_order
 
-nominal_function
-is_value :: "term => bool"
-where
-"is_value (Var x) = False"
+nominal_function head_ctor :: "term \<Rightarrow> bool" where
+  "head_ctor (Var _) = False"
+| "head_ctor (Lam _ _ _) = False"
+| "head_ctor (TyLam _ _ _) = False"
+| "head_ctor (App e1 e2) = head_ctor e1"
+| "head_ctor (TApp e _) = head_ctor e"
+| "head_ctor (Ctor _) = True"
+| "head_ctor (Let _ _ _ _) = False"
+proof goal_cases
+  case (3 P x)
+  then show ?case by (cases x rule: term.exhaust)
+qed (auto simp: eqvt_def head_ctor_graph_aux_def)
+nominal_termination (eqvt) by lexicographic_order
+
+nominal_function is_value :: "term => bool" where
+  "is_value (Var x) = False"
 | "is_value (\<lambda> x : \<tau> . 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"
+| "is_value (\<Lambda> a : k . e) = is_value e"
+| "is_value (App e1 e2) = head_ctor e1"
+| "is_value (TApp e \<tau>) = head_ctor e"
+| "is_value (Ctor _) = True"
 | "is_value (Let x \<tau> e1 e2) = False"
-  apply (auto simp: eqvt_def is_value_graph_aux_def)
-  using term.exhaust by blast
+proof goal_cases
+  case (3 P x)
+  then show ?case by (cases x rule: term.exhaust)
+next
+  case (17 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
+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" ("_[_'/_]" [1000,0,0] 1000) where
-  "(Var y)[e/x]  = (if x = y then e else Var y)"
-| "(App e1 e2)[e/x] = App e1[e/x] e2[e/x]"
-| "(TyApp e1 \<tau>)[e/x] = TyApp e1[e/x] \<tau>"
-| "Unit[_/_] = Unit"
-| "atom y \<sharp> (e, x) \<Longrightarrow> (\<lambda> y:\<tau>. e2)[e/x] = (\<lambda> y:\<tau>. e2[e/x])"
-| "atom y \<sharp> (e, x) \<Longrightarrow> (\<Lambda> y:k. e2)[e/x] = (\<Lambda> y:k. e2[e/x])"
-| "atom y \<sharp> (e, x) \<Longrightarrow> (Let y \<tau> e1 e2)[e/x] = (Let y \<tau> e1[e/x] e2[e/x])"
+nominal_function subst_term :: "term => term \<Rightarrow> var => term" 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"
+| "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)"
 proof (goal_cases)
   case (3 P x)
   then obtain t e y where P: "x = (t, e, y)" by (metis prod.exhaust)
@@ -68,12 +89,12 @@ next
 qed (auto simp: eqvt_def subst_term_graph_aux_def)
 nominal_termination (eqvt) by lexicographic_order
 
-nominal_function subst_type :: "\<tau> \<Rightarrow> \<tau> \<Rightarrow> tyvar \<Rightarrow> \<tau>" ("_[_'/_]" [1000,0,0] 1000) where
-  "TyUnit[_/_] = TyUnit"
-| "(TyVar b)[\<tau>/a] = (if a=b then \<tau> else TyVar b)"
-| "(\<tau>1 \<rightarrow> \<tau>2)[\<tau>/a] = (\<tau>1[\<tau>/a] \<rightarrow> \<tau>2[\<tau>/a])"
-| "(TyConApp \<tau>1 \<tau>2)[\<tau>/a] = TyConApp \<tau>1[\<tau>/a] \<tau>2[\<tau>/a]"
-| "atom b \<sharp> (\<tau>, a) \<Longrightarrow> (\<forall> b:k. \<sigma>)[\<tau>/a] = (\<forall>b:k. \<sigma>[\<tau>/a])"
+nominal_function subst_type :: "\<tau> \<Rightarrow> \<tau> \<Rightarrow> tyvar \<Rightarrow> \<tau>" where
+  "subst_type (TyData T) _ _ = TyData T"
+| "subst_type (TyVar b) \<tau> a = (if a=b then \<tau> else TyVar b)"
+| "subst_type TyArrow _ _ = TyArrow"
+| "subst_type (TyApp \<tau>1 \<tau>2) \<tau> a = TyApp (subst_type \<tau>1 \<tau> a) (subst_type \<tau>2 \<tau> a)"
+| "atom b \<sharp> (\<tau>, a) \<Longrightarrow> subst_type (\<forall> b:k. \<sigma>) \<tau> a = (\<forall>b:k. subst_type \<sigma> \<tau> a)"
 proof goal_cases
   case (3 P x)
   then obtain t \<tau> a where P: "x = (t, \<tau>, a)" by (metis prod.exhaust)
@@ -87,14 +108,14 @@ 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" ("_[_'/_]" [1000,0,0] 1000) where
+nominal_function subst_term_type :: "term \<Rightarrow> \<tau> \<Rightarrow> tyvar \<Rightarrow> term" where
   "subst_term_type (Var x) _ _ = Var x"
-| "subst_term_type Unit _ _ = Unit"
-| "subst_term_type (App e1 e2) \<tau> a = App e1[\<tau>/a] e2[\<tau>/a]"
-| "subst_term_type (TyApp e \<tau>2) \<tau> a = TyApp e[\<tau>/a] \<tau>2[\<tau>/a]"
-| "atom y \<sharp> (\<tau>, a) \<Longrightarrow> subst_term_type (\<lambda> y:\<tau>'. e2) \<tau> a = (\<lambda> y:\<tau>'[\<tau>/a]. e2[\<tau>/a])"
-| "atom b \<sharp> (\<tau>, a) \<Longrightarrow> subst_term_type (\<Lambda> b:k. e2) \<tau> a = (\<Lambda> b:k. e2[\<tau>/a])"
-| "atom y \<sharp> (\<tau>, a) \<Longrightarrow> subst_term_type (Let y \<tau>' e1 e2) \<tau> a = Let y \<tau>'[\<tau>/a] e1[\<tau>/a] e2[\<tau>/a]"
+| "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)"
+| "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)"
 proof goal_cases
   case (3 P x)
   then obtain t \<tau> a where P: "x = (t, \<tau>, a)" by (metis prod.exhaust)
@@ -114,9 +135,9 @@ next
 qed (auto simp: eqvt_def subst_term_type_graph_aux_def)
 nominal_termination (eqvt) by lexicographic_order
 
-nominal_function subst_context :: "\<Gamma> \<Rightarrow> \<tau> \<Rightarrow> tyvar \<Rightarrow> \<Gamma>" ("_[_'/_]" [1000,0,0] 1000) where
+nominal_function subst_context :: "\<Gamma> \<Rightarrow> \<tau> \<Rightarrow> tyvar \<Rightarrow> \<Gamma>" where
   "subst_context [] _ _ = []"
-| "subst_context (BVar x \<tau> # \<Gamma>) \<tau>' a = BVar x \<tau>[\<tau>'/a] # subst_context \<Gamma> \<tau>' a"
+| "subst_context (BVar x \<tau> # \<Gamma>) \<tau>' a = BVar x (subst_type \<tau> \<tau>' a) # subst_context \<Gamma> \<tau>' a"
 | "subst_context (BTyVar b k # \<Gamma>) \<tau>' a = (if a = b then subst_context \<Gamma> \<tau>' a else  BTyVar b k # subst_context \<Gamma> \<tau>' a)"
 proof goal_cases
   case (3 P x)
@@ -129,4 +150,10 @@ proof goal_cases
 qed (auto simp: eqvt_def subst_context_graph_aux_def)
 nominal_termination (eqvt) by lexicographic_order
 
+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
+
 end

Determinancy.thy

@@ -2,27 +2,36 @@ theory Determinancy
   imports Typing Typing_Lemmas
 begin
 
-lemma unique_ty: "\<lbrakk> \<Gamma> \<turnstile>\<^sub>t\<^sub>y \<tau> : k1 ; \<Gamma> \<turnstile>\<^sub>t\<^sub>y \<tau> : k2 \<rbrakk> \<Longrightarrow> k1 = k2"
+lemma unique_ty: "\<lbrakk> \<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : k1 ; \<Gamma> , \<Delta> \<turnstile>\<^sub>t\<^sub>y \<tau> : k2 \<rbrakk> \<Longrightarrow> k1 = k2"
 proof (nominal_induct \<tau> arbitrary: k1 k2 rule: \<tau>.strong_induct)
   case (TyVar x)
   then show ?case using isin_split isin_same(1) by blast
 next
-  case (TyConApp \<tau>1 \<tau>2)
+  case (TyData x)
+  then show ?case using axiom_isin_split axiom_isin_same(1) axioms_valid(2)[OF TyData(2)] by blast
+next
+  case (TyApp \<tau>1 \<tau>2)
   then show ?case by fastforce
 next
   case (TyForall x1 x2a x3)
   then show ?case by (metis Ty_Forall_Inv_2)
 qed auto
 
-lemma unique_tm: "\<lbrakk> \<Gamma> \<turnstile> e : \<tau>1 ; \<Gamma> \<turnstile> e : \<tau>2 \<rbrakk> \<Longrightarrow> \<tau>1 = \<tau>2"
+lemma unique_tm: "\<lbrakk> \<Gamma> , \<Delta> \<turnstile> e : \<tau>1 ; \<Gamma> , \<Delta> \<turnstile> e : \<tau>2 \<rbrakk> \<Longrightarrow> \<tau>1 = \<tau>2"
 proof (nominal_induct e avoiding: \<Gamma> \<tau>1 \<tau>2 rule: term.strong_induct)
   case (Var x)
   then show ?case using isin_split isin_same(2) by blast
 next
-  case (TyApp e1 \<tau>)
-  obtain a1 k1 \<sigma>1 where 1: "\<Gamma> \<turnstile> e1 : \<forall> a1:k1. \<sigma>1" "\<tau>1 = \<sigma>1[\<tau>/a1]" by (cases rule: Tm.cases[OF TyApp(2)]) auto
-  obtain a2 k2 \<sigma>2 where 2: "\<Gamma> \<turnstile> e1 : \<forall> a2:k2. \<sigma>2" "\<tau>2 = \<sigma>2[\<tau>/a2]" by (cases rule: Tm.cases[OF TyApp(3)]) auto
-  show ?case using TyApp(1)[OF 1(1) 2(1)] subst_type_same 1(2) 2(2) by simp
+  case (App e1 e2)
+  then show ?case by fastforce
+next
+  case (TApp e1 \<tau>)
+  obtain a1 k1 \<sigma>1 where 1: "\<Gamma> , \<Delta> \<turnstile> e1 : \<forall> a1:k1. \<sigma>1" "\<tau>1 = \<sigma>1[\<tau>/a1]" by (cases rule: Tm.cases[OF TApp(2)]) auto
+  obtain a2 k2 \<sigma>2 where 2: "\<Gamma> , \<Delta> \<turnstile> e1 : \<forall> a2:k2. \<sigma>2" "\<tau>2 = \<sigma>2[\<tau>/a2]" by (cases rule: Tm.cases[OF TApp(3)]) auto
+  show ?case using TApp(1)[OF 1(1) 2(1)] subst_type_same 1(2) 2(2) by simp
+next
+  case (Ctor x)
+  then show ?case using axiom_isin_split axiom_isin_same(2) axioms_valid(3)[OF Ctor(2)] by blast
 next
   case (Lam x \<tau> e)
   then show ?case by (metis T_Abs_Inv)
@@ -32,6 +41,6 @@ next
 next
   case (Let x \<tau> e1 e2)
   then show ?case using T_Let_Inv by blast
-qed fastforce+
+qed
 
 end

Lemmas.thy

@@ -82,6 +82,7 @@ lemma subst_type_same: "[[atom a]]lst. e = [[atom a']]lst. e' \<Longrightarrow>
   by (metis Abs1_eq_iff(3) flip_commute subst_type_var_name)
 lemma subst_term_type_same: "[[atom a]]lst. e = [[atom a']]lst. e' \<Longrightarrow> subst_term_type e \<tau> a = subst_term_type e' \<tau> a'"
   by (metis Abs1_eq_iff(3) flip_commute subst_term_type_var_name)
+lemmas subst_same = subst_term_same subst_type_same subst_term_type_same
 
 (* atom x \<sharp> \<Gamma> \<Longrightarrow> \<not>isin (B x _) \<Gamma> *)
 lemma fresh_not_isin_tyvar: "atom a \<sharp> \<Gamma> \<Longrightarrow> \<not>isin (BTyVar a k) \<Gamma>"
@@ -134,4 +135,7 @@ lemmas subst_subst = subst_subst_term subst_subst_type subst_subst_term_type sub
 lemma fv_supp_subset: "fv_\<tau> \<tau> \<subseteq> supp \<tau>"
   by (induction \<tau> rule: \<tau>.induct) (auto simp: \<tau>.supp \<tau>.fv_defs)
 
+lemma head_ctor_is_value: "head_ctor e \<Longrightarrow> is_value e"
+  by (induction e rule: term.induct) auto
+
 end

Semantics.thy

@@ -6,15 +6,18 @@ no_notation HOL.implies (infixr "\<longrightarrow>" 25)
 
 inductive Step :: "term \<Rightarrow> term \<Rightarrow> bool" ("_ \<longrightarrow> _" 25) where
 
-  ST_BetaI: "App (\<lambda> x : \<tau> . e) e2 \<longrightarrow> e[e2/x]"
+  ST_Beta: "App (\<lambda> x : \<tau> . e) e2 \<longrightarrow> e[e2/x]"
 
-| ST_AppI: "e1 \<longrightarrow> e2 \<Longrightarrow> App e1 e \<longrightarrow> App e2 e"
+| ST_TBeta: "is_value e \<Longrightarrow> TApp (\<Lambda> a : k . e) \<tau> \<longrightarrow> e[\<tau>/a]"
 
-| ST_SubstI: "Let x \<tau> e1 e2 \<longrightarrow> e2[e1/x]"
+| ST_TAbs: "e \<longrightarrow> e' \<Longrightarrow> (\<Lambda> a:k. e) \<longrightarrow> (\<Lambda> a:k. e')"
 
-| ST_BetaTI: "TyApp (\<Lambda> a : k . e) \<tau> \<longrightarrow> e[\<tau>/a]"
+| ST_App: "e1 \<longrightarrow> e1' \<Longrightarrow> App e1 e2 \<longrightarrow> App e1' e2"
+
+| ST_TApp: "e \<longrightarrow> e' \<Longrightarrow> TApp e \<tau> \<longrightarrow> TApp e' \<tau>"
+
+| ST_Let: "Let x \<tau> e1 e2 \<longrightarrow> e2[e1/x]"
 
-| ST_AppTI: "e1 \<longrightarrow> e2 \<Longrightarrow> TyApp e1 \<tau> \<longrightarrow> TyApp e2 \<tau>"
 equivariance Step
 nominal_inductive Step .
 
@@ -29,47 +32,112 @@ definition stuck :: "term \<Rightarrow> bool" where
   "stuck e \<equiv> \<not>is_value e \<and> beta_nf e"
 
 lemma value_beta_nf: "is_value v \<Longrightarrow> beta_nf v"
-  apply (cases v rule: term.exhaust)
-  using Step.cases beta_nf_def by fastforce+
+proof (induction v rule: term.induct)
+  case (App e1 e2)
+  show ?case
+  proof (rule ccontr)
+    assume "\<not>beta_nf (App e1 e2)"
+    then obtain e' where "App e1 e2 \<longrightarrow> e'" using beta_nf_def by blast
+    then show "False" using App head_ctor_is_value beta_nf_def by cases auto
+  qed
+next
+  case (TApp e \<tau>)
+  show ?case
+  proof (rule ccontr)
+    assume "\<not>beta_nf (TApp e \<tau>)"
+    then obtain e' where "TApp e \<tau> \<longrightarrow> e'" using beta_nf_def by blast
+    then show "False" using TApp head_ctor_is_value beta_nf_def by cases auto
+  qed
+next
+  case (Ctor D)
+  then show ?case using Step.cases beta_nf_def by fastforce
+next
+  case (Lam x \<tau> e)
+  then show ?case using Step.cases beta_nf_def by fastforce
+next
+  case (TyLam a k e)
+  show ?case
+  proof (rule ccontr)
+    assume "\<not>beta_nf (\<Lambda> a:k. e)"
+    then obtain e' where "(\<Lambda> a:k. e) \<longrightarrow> e'" using beta_nf_def by blast
+    then show "False"
+    proof cases
+      case (ST_TAbs e2 e2' b)
+      obtain c::tyvar where c:"atom c \<sharp> (a, e, b, e2)" by (rule obtain_fresh)
+      then obtain e3 where 1: "[[atom b]]lst. e2 = [[atom c]]lst. e3" by (metis Abs_lst_rename fresh_PairD(2))
+      then have 2: "e = (c \<leftrightarrow> a) \<bullet> e3" using ST_TAbs(1) c by (metis Abs_rename_body)
+      from 1 have "e3 = (b \<leftrightarrow> c) \<bullet> e2" using Abs_rename_body by blast
+      then have "e3 \<longrightarrow> (b \<leftrightarrow> c) \<bullet> e2'" using ST_TAbs(3) Step.eqvt by blast
+      then have "e \<longrightarrow> (c \<leftrightarrow> a) \<bullet> (b \<leftrightarrow> c) \<bullet> e2'" using 2 Step.eqvt by blast
+      then show ?thesis using TyLam beta_nf_def by auto
+    qed
+  qed
+qed auto
 
 lemma Step_deterministic: "\<lbrakk> e \<longrightarrow> e1 ; e \<longrightarrow> e2 \<rbrakk> \<Longrightarrow> e1 = e2"
 proof (induction e e1 arbitrary: e2 rule: Step.induct)
-  case (ST_BetaI v x \<tau> e)
+  case (ST_Beta v x \<tau> e)
   then show ?case
   proof cases
-    case (ST_BetaI y e')
+    case (ST_Beta y e')
     then show ?thesis using subst_term_same by blast
   next
-    case (ST_AppI e')
+    case (ST_App e')
     then show ?thesis using Step.cases by fastforce
   qed
 next
-  case (ST_AppI e1 e2 e)
-  from ST_AppI(3) show ?case
-    apply cases
-    using ST_AppI Step.cases value_beta_nf beta_nf_def by fastforce+
+  case outer: (ST_TAbs e e' a k)
+  from outer(3) show ?case
+  proof cases
+    case (ST_TAbs e3 e3' b)
+    obtain c::tyvar where "atom c \<sharp> (a, e, b, e3, e', e3')" by (rule obtain_fresh)
+    then have c: "atom c \<sharp> (a, e, b, e3)" "atom c \<sharp> e'" "atom c \<sharp> e3'" by auto
+    then obtain e4 where 1: "[[atom b]]lst. e3 = [[atom c]]lst. e4" by (metis Abs_lst_rename fresh_PairD(2))
+    then have 2: "e = (c \<leftrightarrow> a) \<bullet> e4" using ST_TAbs(1) c by (metis Abs_rename_body)
+    from 1 have 3: "e4 = (b \<leftrightarrow> c) \<bullet> e3" using c by (metis Abs_rename_body)
+
+    have x1: "(\<Lambda> a : k . e') = (\<Lambda> c : k . (a \<leftrightarrow> c) \<bullet> e')" using c(2) Abs_lst_rename by fastforce
+    have x2: "(\<Lambda> b : k . e3') = (\<Lambda> c : k. (b \<leftrightarrow> c) \<bullet> e3')" using c(3) Abs_lst_rename by fastforce
+
+    let ?e4' = "(c \<leftrightarrow> a) \<bullet> (b \<leftrightarrow> c) \<bullet> e3'"
+    from 3 have "e4 \<longrightarrow> (b \<leftrightarrow> c) \<bullet> e3'" using Step.eqvt ST_TAbs(3) by blast
+    then have "e \<longrightarrow> ?e4'" using Step.eqvt 2 by blast
+    then have "e' = ?e4'" using outer(2) by blast
+    then have "(a \<leftrightarrow> c) \<bullet> e' = (b \<leftrightarrow> c) \<bullet> e3'" by (simp add: flip_commute)
+    then show ?thesis using x1 x2 ST_TAbs(2) by argo
+  qed
 next
-  case (ST_SubstI v x e)
+  case (ST_App e1 e2 e)
+  from ST_App(3) show ?case
+  proof cases
+    case (ST_Beta x \<tau> e)
+    then show ?thesis using ST_App.hyps beta_nf_def is_value.simps(2) value_beta_nf by blast
+  next
+    case (ST_App e2)
+    then show ?thesis by (simp add: ST_App.IH)
+  qed
+next
+  case (ST_Let v x e)
   then show ?case
   proof cases
-    case (ST_SubstI x e)
+    case (ST_Let x e)
     then show ?thesis using subst_term_same by blast
   qed
 next
-  case (ST_BetaTI a e \<tau>)
-  then show ?case
+  case (ST_TBeta a e \<tau>)
+  from ST_TBeta(2) show ?case
   proof cases
-    case (ST_BetaTI b e')
+    case (ST_TBeta b e')
     then show ?thesis using subst_term_type_same by blast
   next
-    case (ST_AppTI e2)
-    then show ?thesis using is_value.simps(3) value_beta_nf beta_nf_def by blast
+    case (ST_TApp e2)
+    then show ?thesis using is_value.simps(3) value_beta_nf beta_nf_def ST_TBeta(1) by blast
   qed
 next
-  case (ST_AppTI e1 e2 \<tau>)
-  from ST_AppTI(3) show ?case
+  case (ST_TApp e1 e2 \<tau>)
+  from ST_TApp(3) show ?case
     apply cases
-    using ST_AppTI value_beta_nf beta_nf_def by auto
+    using ST_TApp value_beta_nf beta_nf_def by auto
 qed
 
 end