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