Theory Progress

subsection‹Progress›

theory Progress
  imports TypePreservation
begin
  
text‹We say that a term $t$ is in \emph{weak-head-normal} form when one of the following conditions are met:
  \begin{enumerate}
    \item $t$ is a value,
    \item there exists $\alpha$ and $v$ such that $t = \mu:\tau.[\alpha]\ v$ with $\alpha \in fcv(v)$
          whenever $\alpha = 0$.
  \end{enumerate}›
  
fun (sequential) is_nf :: "trm ⇒ bool" where
  "is_nf (μ U: (<β> v)) = (is_val v ∧ (β = 0 ⟶ 0 ∈ fmv_trm v 0))" |
  "is_nf v = is_val v"
  
lemma progress':
  "Γ, Δ ⊢⇩T t : T ⟹ lambda_closed t ⟹ (∀ s. ¬(t ⇢ s)) ⟹ is_nf t"
  "Γ, Δ ⊢⇩C c ⟹ lambda_closedC c  ⟹ (∀ β t. c = (<β> t) ⟶ (∀ d. ¬(t ⇢ d)) ⟶ is_nf t)"                            
proof (induct rule: typing_trm_typing_cmd.inducts)
  case (app Γ Δ t T1 T2 s)
  then show ?case
    by -(erule type_arrow_elim; force)  
next
  case (activate Γ Δ T c)
  then show ?case
    proof(cases c)
      case (MVar α t)
      then show ?thesis
        using activate by (case_tac t; force)
    qed
qed force+

theorem progress:
  assumes "Γ, Δ ⊢⇩T t : T" "lambda_closed t"
  shows   "is_nf t ∨ (∃ s. t ⇢ s)"
using assms by (fastforce intro: progress')
    
end