Remove is_value from small step relation (#8)

Author: jvanbruegge

Semantics.thy

@@ -5,19 +5,16 @@ begin
 no_notation HOL.implies (infixr "\<longrightarrow>" 25)
 
 inductive Step :: "term \<Rightarrow> term \<Rightarrow> bool" ("_ \<longrightarrow> _" 25) where
-  ST_BetaI: "\<lbrakk> is_value v \<rbrakk> \<Longrightarrow> App (\<lambda> x : \<tau> . e) v \<longrightarrow> subst_term v x e"
 
-| ST_AppI: "\<lbrakk> e1 \<longrightarrow> e2 \<rbrakk> \<Longrightarrow> App e1 e \<longrightarrow> App e2 e"
+  ST_BetaI: "App (\<lambda> x : \<tau> . e) v \<longrightarrow> subst_term v x e"
 
-| ST_App2I: "\<lbrakk> is_value v ; e1 \<longrightarrow> e2 \<rbrakk> \<Longrightarrow> App v e1 \<longrightarrow> App v e2"
+| ST_AppI: "e1 \<longrightarrow> e2 \<Longrightarrow> App e1 e \<longrightarrow> App e2 e"
 
-| ST_SubstI: "\<lbrakk> is_value v \<rbrakk> \<Longrightarrow> Let x \<tau> v e \<longrightarrow> subst_term v x e"
-
-| ST_LetI: "\<lbrakk> e1 \<longrightarrow> e2 \<rbrakk> \<Longrightarrow> Let x \<tau> e1 e \<longrightarrow> Let x \<tau> e2 e"
+| 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_AppTI: "\<lbrakk> e1 \<longrightarrow> e2 \<rbrakk> \<Longrightarrow> TyApp e1 \<tau> \<longrightarrow> TyApp e2 \<tau>"
+| ST_AppTI: "e1 \<longrightarrow> e2 \<Longrightarrow> TyApp e1 \<tau> \<longrightarrow> TyApp e2 \<tau>"
 equivariance Step
 nominal_inductive Step .
 
@@ -38,44 +35,26 @@ lemma value_beta_nf: "is_value v \<Longrightarrow> beta_nf v"
 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)
-  from ST_BetaI(2) show ?case
+  then show ?case
   proof cases
     case (ST_BetaI y e')
     then show ?thesis using subst_term_same by blast
   next
     case (ST_AppI e')
     then show ?thesis using Step.cases by fastforce
-  next
-    case (ST_App2I e')
-    then show ?thesis using ST_BetaI value_beta_nf beta_nf_def by blast
   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+
-next
-  case (ST_App2I v e1 e2)
-  from ST_App2I(4) show ?case
-    apply cases
-    using ST_App2I.hyps(2) value_beta_nf beta_nf_def apply blast
-    using ST_App2I.hyps(1) value_beta_nf beta_nf_def apply blast
-    using ST_App2I value_beta_nf beta_nf_def by auto
 next
   case (ST_SubstI v x e)
-  from ST_SubstI(2) show ?case
+  then show ?case
   proof cases
     case (ST_SubstI x e)
     then show ?thesis using subst_term_same by blast
-  next
-    case (ST_LetI e2 x e)
-    then show ?thesis using ST_SubstI.hyps value_beta_nf beta_nf_def by blast
   qed
-next
-  case (ST_LetI t1 t2 x \<tau> e)
-  from ST_LetI(3) show ?case
-    apply cases
-    using ST_LetI value_beta_nf beta_nf_def by auto
 next
   case (ST_BetaTI a e \<tau>)
   then show ?case

Soundness.thy

@@ -24,7 +24,7 @@ case (T_AppI e1 \<tau>1 \<tau>2 e2)
       then show ?thesis by simp
     next
       assume "\<exists>e2'. Step e2 e2'"
-      then show ?thesis using ST_App2I \<open>is_value e1\<close> by blast
+      then show ?thesis using ST_BetaI T_AppI.hyps(1) \<open>is_value e1\<close> fun_ty_lam by blast 
     qed
   next
     assume "\<exists>e1'. Step e1 e1'"
@@ -34,7 +34,7 @@ case (T_AppI e1 \<tau>1 \<tau>2 e2)
   qed
 next
   case (T_LetI x e1 \<tau>1 e2 \<tau>2)
-  then show ?case using ST_SubstI ST_LetI by blast
+  then show ?case using ST_SubstI by blast
 next
   case (T_AppTI e a \<sigma> \<tau>)
   from T_AppTI(2) show ?case
@@ -281,9 +281,6 @@ next
   next
     case (ST_AppI e2)
     then show ?thesis using T_AppI T.T_AppI by blast
-  next
-    case (ST_App2I e2)
-    then show ?thesis using T_AppI T.T_AppI by blast
   qed
 next
   case (T_LetI x e1 \<tau>1 e2 \<tau>2)
@@ -302,21 +299,6 @@ next
       then have "[BVar y \<tau>1] \<turnstile> e : \<tau>2" using T.eqvt by (metis T_AbsI T_Abs_Inv T_LetI.hyps(3) T_LetI.hyps(4) \<tau>.eq_iff(3) fresh_Nil local.ST_SubstI(1) term.eq_iff(5))
       then show ?thesis using T_LetI ST_SubstI substitution by auto
     qed
-  next
-    case (ST_LetI e1' x' e2')
-
-    have "atom x' \<sharp> e1'" using T_LetI.hyps(6) fresh_Nil fresh_term_var local.ST_LetI(3) by blast
-    then have 1: "atom x' \<sharp> ([], e1')" using fresh_Pair fresh_Nil by auto
-
-    have swap: "(x \<leftrightarrow> x') \<bullet> e2' = e2"
-      by (metis Abs1_eq_iff(3) Nominal2_Base.swap_self add_flip_cancel flip_def local.ST_LetI(1) permute_flip_cancel permute_plus)
-
-    have "(x \<leftrightarrow> x') \<bullet> ([BVar x \<tau>1] \<turnstile> e2 : \<tau>2)" by (simp add: T_LetI.hyps(4))
-    then have "((x \<leftrightarrow> x') \<bullet> [BVar x \<tau>1]) \<turnstile> e2' : \<tau>2" by (metis (full_types) T.eqvt T_LetI.hyps(4) flip_commute flip_fresh_fresh local.swap no_vars_in_ty permute_flip_cancel2)
-    then have 2: "[BVar x' \<tau>1] \<turnstile> e2' : \<tau>2" by (simp add: flip_fresh_fresh)
-    have 3: "[] \<turnstile>\<^sub>t\<^sub>y \<tau>1" by (simp add: T_LetI.hyps(3))
-
-    show ?thesis using ST_LetI(2) T.T_LetI[OF 1 3 2 T_LetI(6)[OF ST_LetI(3)]] by simp
   qed
 next
   case (T_AppTI e a \<sigma> \<tau>)