Theory SmallStep

(*  Title:      SmallStep.thy
    Author:     Peter Gammie
*)

section ‹A small-step (reduction) operational semantics for PCF›
(*<*)

theory SmallStep
imports
  OpSem
begin

(*>*)
text‹

A small-step semantics allows us to express more things, like the
progress of well-typed programs.

FIXME adjust: This relation is non-deterministic, but only ‹β›-reduces terms where the argument is a value. Moreover if we
start with a closed term then our values are also closed. So while in
general (i.e., for open terms) our substitution operation is wrong and
this relation is too big, we show that things work out if we start
reducing from a closed term (i.e., a program).

FIXME following Tolmach @{url
"https://www.cis.upenn.edu/~bcpierce/sf/current/Norm.html"} we make
this relation deterministic. Eases the normalization proof.

›

inductive
  reduction :: "db ⇒ db ⇒ bool" (‹_ →⇩v _› [50, 50] 50)
where
  betaN: "DBApp (DBAbsN u) v →⇩v u<v/0>"
| betaV: "val v ⟹ DBApp (DBAbsV u) v →⇩v u<v/0>"
| "f →⇩v f' ⟹ DBApp f x →⇩v DBApp f' x"
| "⟦f = DBAbsV u; x →⇩v x'⟧ ⟹ DBApp f x →⇩v DBApp f x'"
| "DBFix f →⇩v f<DBFix f/0>"
| "DBCond DBtt t e →⇩v t"
| "DBCond DBff t e →⇩v e"
| "DBSucc (DBNum n) →⇩v DBNum (Suc n)"
| "DBPred (DBNum (Suc n)) →⇩v DBNum n"
| "DBIsZero (DBNum 0) →⇩v DBtt"
| "0 < n ⟹ DBIsZero (DBNum n) →⇩v DBff"

abbreviation ― ‹The transitive, reflexive closure of the reduction relation.›
  reduction_trc :: "db ⇒ db ⇒ bool" (‹_ →⇩v⇧* _› [100, 100] 100)
where
  "reduction_trc ≡ rtranclp reduction"

declare reduction.intros[intro!]

inductive_cases reduction_inv:
  "DBVar v →⇩v t'"
  "DBApp f x →⇩v t'"
  "DBAbsN u →⇩v t'"
  "DBAbsV u →⇩v t'"
  "DBFix f →⇩v t'"
  "DBCond i t e →⇩v t'"
  "DBff →⇩v t'"
  "DBtt →⇩v t'"
  "DBNum n →⇩v t'"
  "DBSucc n →⇩v t'"
  "DBPred n →⇩v t'"
  "DBIsZero n →⇩v t'"

lemma reduction_val:
  assumes "val v"
  assumes "v →⇩v v'"
  shows False
using assms by (auto elim: val.cases reduction_inv)

lemma reduction_deterministic:
  assumes "t →⇩v t'"
  assumes "t →⇩v t''"
  shows "t'' = t'"
using assms by (induct arbitrary: t'') (blast dest: reduction_val elim: reduction_inv)+


subsubsection‹ Reduction is consistent with evaluation ›

lemma reduction_eval:
  assumes "t →⇩v t'"
  assumes "t' ⇓ v"
  shows "t ⇓ v"
using assms by (induct arbitrary: v) (auto elim!: evalOP_inv val.cases intro: eval_val)

lemma reduction_trc_eval:
  assumes "t →⇩v⇧* t'"
  assumes "t' ⇓ v"
  shows "t ⇓ v"
using assms by induct (auto simp: reduction_eval)

theorem reduction_trc_val_eval:
  assumes "t →⇩v⇧* v"
  assumes "val v"
  shows "t ⇓ v"
using assms by (induct rule: converse_rtranclp_induct) (auto intro: eval_val reduction_trc_eval)

text‹

We show the converse (of sorts) using the frame stack machinery of the
next section.

›

(*<*)

end
(*>*)