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

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

theory SmallStep
imports
  OpSem
begin

(*>*)
text‹

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

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

  following Tolmach @{url
 https://www.cis.upenn.edu/~bcpierce/sf/current/Norm.html"} we make
  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‹

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

 ›

(*<*)

end
(*>*)