Evaluate under type lambdas to match Haskell

Author: jvanbruegge

Defs.thy

@@ -27,34 +27,39 @@ proof goal_cases
 qed (auto simp: eqvt_def isin_graph_aux_def)
 nominal_termination (eqvt) by lexicographic_order
 
-nominal_function head_ctor :: "term \<Rightarrow> bool"
-  and is_value :: "term => bool" where
+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 \<and> is_value e2)"
+| "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
 
-| "is_value (Var x) = False"
+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) = (head_ctor e1 \<and> is_value e2)"
+| "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"
 proof goal_cases
   case (3 P x)
-  then show ?case
-  proof (cases x)
-    case (Inl a)
-    then show ?thesis using 3(1-7) by (cases a rule: term.exhaust) auto
-  next
-    case (Inr b)
-    then show ?thesis using 3(8-14) by (cases b rule: term.exhaust) auto
-  qed
-qed (auto simp: eqvt_def head_ctor_is_value_graph_aux_def)
+  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" where

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: "TApp (\<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> TApp e1 \<tau> \<longrightarrow> TApp e2 \<tau>"
 equivariance Step
 nominal_inductive Step .
 
@@ -53,47 +56,88 @@ next
   then show ?case using Step.cases beta_nf_def by fastforce
 next
   case (TyLam a k e)
-  then show ?case using Step.cases beta_nf_def by fastforce
+  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_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_SubstI v x e)
+  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

Typing_Lemmas.thy

@@ -4,6 +4,9 @@ begin
 
 no_notation Set.member  ("(_/ : _)" [51, 51] 50)
 
+lemma fun_ty_val: "\<lbrakk> \<Gamma> , \<Delta> \<turnstile> e : \<tau>1 \<rightarrow> \<tau>2 ; is_value e \<rbrakk> \<Longrightarrow> (\<exists>x e'. e = (\<lambda>x:\<tau>1. e')) \<or> head_ctor e"
+  by (induction \<Gamma> \<Delta> e "\<tau>1 \<rightarrow> \<tau>2" rule: Tm.induct) auto
+
 lemma context_cons_valid[elim]: "(\<Delta>::\<Delta>) \<turnstile> bndr # \<Gamma> \<Longrightarrow> (\<Delta> \<turnstile> \<Gamma> \<Longrightarrow> P) \<Longrightarrow> P"
   by (cases rule: Ctx.cases) (auto simp: context_valid(1))