Theory SmallStep

(*
 * Copyright 2016, Data61, CSIRO
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(DATA61_BSD)
 *)
section ‹COMPLX small-step semantics›
theory SmallStep
imports Language
begin

text ‹The procedure environment›
type_synonym ('s,'p,'f) body = "'p ⇒ ('s,'p,'f) com option"

text ‹State types›
datatype ('s,'f) xstate = Normal 's | Fault 'f | Stuck

lemma rtrancl_mono_proof[mono]:
   "(⋀a b. x a b ⟶ y a b) ⟹ rtranclp x a b ⟶ rtranclp y a b"
   apply (rule impI, rotate_tac, induct rule: rtranclp.induct)
    apply simp_all
   apply (metis rtranclp.intros)
   done


primrec redex:: "('s,'p,'f)com ⇒ ('s,'p,'f)com"
where
"redex Skip = Skip" |
"redex (Basic f) = (Basic f)" |
"redex (Spec r) = (Spec r)" |
"redex (Seq c⇩1 c⇩2) = redex c⇩1" |
"redex (Cond b c⇩1 c⇩2) = (Cond b c⇩1 c⇩2)" |
"redex (While b c) = (While b c)" |
"redex (Call p) = (Call p)" |
"redex (DynCom d) = (DynCom d)" |
"redex (Guard f b c) = (Guard f b c)" |
"redex (Throw) = Throw" |
"redex (Catch c⇩1 c⇩2) = redex c⇩1" |
"redex (Await b c) = Await b c" |
"redex (Parallel cs) = Parallel cs"

subsection ‹Small-Step Computation: ‹Γ ⊢(c, s) → (c', s')››

text ‹The final configuration is either of the form ‹(Skip,_)› for normal
termination, or @{term "(Throw,Normal s)"} in case the program was started in 
a @{term "Normal"} state and terminated abruptly. Explicit abrupt states are removed
from the language definition and thus do not need to be propogated.›

type_synonym ('s,'p,'f) config = "('s,'p,'f)com  × ('s,'f) xstate"

definition final:: "('s,'p,'f) config ⇒ bool" where
"final cfg = (fst cfg=Skip ∨ (fst cfg=Throw ∧ (∃s. snd cfg=Normal s)))"

primrec atom_com :: "⌦‹('s,'p,'f) body ⇒› ('s, 'p, 'f) com ⇒ bool" where
  "atom_com Skip = True" | 
  "atom_com (Basic f) = True" | 
  "atom_com (Spec r) = True" | 
  "atom_com (Seq  c⇩1 c⇩2) = (atom_com c⇩1 ∧ atom_com c⇩2)" | 
  "atom_com (Cond b c⇩1 c⇩2) = (atom_com c⇩1 ∧ atom_com c⇩2)" | 
  "atom_com (While b c) = atom_com c" | 
 (* Change to  atom_com (Call p) = atom_com (Θ p)
  Butow do we pass function body from step? *)
  "atom_com (Call p) = False" |
  "atom_com (DynCom f) = (∀s::'s. atom_com (f s))" | 
  "atom_com (Guard f g c) = atom_com c" | 
  "atom_com Throw = True" | 
  "atom_com (Catch c⇩1 c⇩2) = (atom_com c⇩1 ∧ atom_com c⇩2)" | 
  "atom_com (Parallel cs) = False" | 
  "atom_com (Await b c) = False"


inductive
      "step"::"[('s,'p,'f) body, ('s,'p,'f) config,('s,'p,'f) config] ⇒ bool"
                                (‹_⊢ (_ →/ _)› [81,81,81] 100)
  and "step_rtrancl" :: "[('s,'p,'f) body, ('s,'p,'f) config,('s,'p,'f) config] ⇒ bool"
                                (‹_ ⊢ (_ →⇧*/ _)› [81,81,81] 100)
  for Γ::"('s,'p,'f) body"
where
  "Γ ⊢ a →⇧* b ≡ (step Γ)⇧*⇧* a b"
| Basic: "Γ ⊢(Basic f,Normal s) → (Skip,Normal (f s))"

| Spec: "(s,t) ∈ r ⟹ Γ ⊢(Spec r,Normal s) → (Skip,Normal t)"
| SpecStuck: "∀t. (s,t) ∉ r ⟹ Γ ⊢(Spec r,Normal s) → (Skip,Stuck)"

| Guard: "s∈g ⟹ Γ ⊢(Guard f g c,Normal s) → (c,Normal s)"
  
| GuardFault: "s∉g ⟹ Γ ⊢(Guard f g c,Normal s) → (Skip,Fault f)"


| Seq: "Γ ⊢(c⇩1,s) → (c⇩1',s')
        ⟹ 
        Γ ⊢(Seq c⇩1 c⇩2,s) → (Seq c⇩1' c⇩2, s')"
| SeqSkip: "Γ ⊢(Seq Skip c⇩2,s) → (c⇩2, s)"
| SeqThrow: "Γ ⊢(Seq Throw c⇩2,Normal s) → (Throw, Normal s)"

| CondTrue:  "s∈b ⟹ Γ ⊢(Cond b c⇩1 c⇩2,Normal s) → (c⇩1,Normal s)"
| CondFalse: "s∉b ⟹ Γ ⊢(Cond b c⇩1 c⇩2,Normal s) → (c⇩2,Normal s)"

| WhileTrue: "⟦s∈b⟧ 
              ⟹ 
              Γ ⊢(While b c,Normal s) → (Seq c (While b c),Normal s)"

| WhileFalse: "⟦s∉b⟧ 
               ⟹ 
               Γ ⊢(While b c,Normal s) → (Skip,Normal s)"

| Call: "Γ p=Some b ⟹
         Γ ⊢(Call p,Normal s) → (b,Normal s)"

| CallUndefined: "Γ p=None ⟹
         Γ ⊢(Call p,Normal s) → (Skip,Stuck)"

| DynCom: "Γ ⊢(DynCom c,Normal s) → (c s,Normal s)"

| Catch: "⟦Γ ⊢(c⇩1,s) → (c⇩1',s')⟧
          ⟹
          Γ ⊢(Catch c⇩1 c⇩2,s) → (Catch c⇩1' c⇩2,s')"

| CatchSkip: "Γ ⊢(Catch Skip c⇩2,s) → (Skip,s)"
| CatchThrow: "Γ ⊢(Catch Throw c⇩2,Normal s) → (c⇩2,Normal s)"

| FaultProp:  "⟦c≠Skip; redex c = c⟧ ⟹ Γ ⊢(c,Fault f) → (Skip,Fault f)"
| StuckProp:  "⟦c≠Skip; redex c = c⟧ ⟹ Γ ⊢(c,Stuck) → (Skip,Stuck)"


| Parallel: "⟦  i < length cs; Γ ⊢ (cs!i, s) → (c', s') ⟧ 
            ⟹ Γ ⊢ (Parallel cs, s) → (Parallel (cs[i := c']), s')"

| ParSkip: "⟦ ∀c ∈ set cs. c = Skip ⟧ ⟹ Γ ⊢ (Parallel cs, s) → (Skip, s)"
(* If exception is thrown, the parallel execution may either abort
   immediately (rule ParThrow) or keep executing (rule Parallel) *)
| ParThrow: "⟦ Throw ∈ set cs ⟧ ⟹ Γ ⊢ (Parallel cs, s) → (Throw, s)"


| Await: "⟦ s ∈ b; Γ ⊢ (c, Normal s) →⇧* (c', Normal s');
           atom_com c; c' = Skip ∨ c' = Throw ⟧ 
          ⟹ Γ ⊢ (Await b c, Normal s) → (c', Normal s')"
| AwaitStuck: 
         "⟦ s ∈ b; Γ ⊢ (c, Normal s) →⇧* (c', Stuck) ;
           atom_com c⟧
          ⟹ Γ ⊢ (Await b c, Normal s) → (Skip, Stuck)" 
| AwaitFault: 
         "⟦ s ∈ b; Γ ⊢ (c, Normal s) →⇧* (c', Fault f) ;
           atom_com c⟧
          ⟹ Γ ⊢ (Await b c, Normal s) → (Skip, Fault f)" 
| AwaitNonAtom: 
         " ¬ atom_com c
          ⟹ Γ ⊢ (Await b c, Normal s) → (Skip, Stuck)"


lemmas step_induct = step.induct [of _ "(c,s)" "(c',s')", split_format (complete), case_names
Basic Spec SpecStuck Guard GuardFault Seq SeqSkip SeqThrow CondTrue CondFalse
WhileTrue WhileFalse Call CallUndefined DynCom Catch CatchThrow CatchSkip
FaultProp StuckProp Parallel ParSkip Await, induct set]

text ‹The execution of a command is blocked if it cannot make progress, but is not in a final
state. It is the intention that ‹∃cfg. Γ ⊢ (c, s) → cfg) ∨ final (c, s) ∨ blocked Γ c s›, but
we do not prove this.›

function(sequential) blocked :: "('s,'p,'f) body ⇒ ('s,'p,'f) com ⇒ ('s,'f)xstate ⇒ bool" where
  "blocked Γ (Seq (Await b c⇩1) c⇩2) (Normal s) = (s ∉ b)"
| "blocked Γ (Catch (Await b c⇩1) c⇩2) (Normal s) = (s ∉ b)"
| "blocked Γ (Await b c) (Normal s) = (s ∉ b ∨ (∀c' s'. Γ ⊢ (c, Normal s) →⇧* (c', Normal s') ⟶ ¬ final (c', Normal s')))"
| "blocked Γ (Parallel cs) (Normal s) = (∀t ∈ set cs. blocked Γ t (Normal s) ∨ final (t, Normal s))"
| "blocked Γ _ _ = False"
by (pat_completeness, auto)

inductive_cases step_elim_cases [cases set]:
 "Γ ⊢(Skip,s) → u"
 "Γ ⊢(Guard f g c,s) → u"
 "Γ ⊢(Basic f,s) → u"
 "Γ ⊢(Spec r,s) → u"
 "Γ ⊢(Seq c1 c2,s) → u"
 "Γ ⊢(Cond b c1 c2,s) → u"
 "Γ ⊢(While b c,s) → u"
 "Γ ⊢(Call p,s) → u"
 "Γ ⊢(DynCom c,s) → u"
 "Γ ⊢(Throw,s) → u"
 "Γ ⊢(Catch c1 c2,s) → u"
 "Γ ⊢(Parallel cs,s) → u"
 "Γ ⊢(Await b e,s) → u"


inductive_cases step_Normal_elim_cases [cases set]:
 "Γ ⊢(Skip,Normal s) → u"
 "Γ ⊢(Guard f g c,Normal s) → u"
 "Γ ⊢(Basic f,Normal s) → u"
 "Γ ⊢(Spec r,Normal s) → u"
 "Γ ⊢(Seq c1 c2,Normal s) → u"
 "Γ ⊢(Cond b c1 c2,Normal s) → u"
 "Γ ⊢(While b c,Normal s) → u"
 "Γ ⊢(Call p,Normal s) → u"
 "Γ ⊢(DynCom c,Normal s) → u"
 "Γ ⊢(Throw,Normal s) → u"
 "Γ ⊢(Catch c1 c2,Normal s) → u"
 "Γ ⊢(Parallel cs,Normal s) → u"
 "Γ ⊢(Await b e,Normal s) → u"


abbreviation 
 "step_trancl" :: "[('s,'p,'f) body, ('s,'p,'f) config,('s,'p,'f) config] ⇒ bool"
                                (‹_⊢ (_ →⇧+/ _)› [81,81,81] 100)
 where
  "Γ ⊢cf0 →⇧+ cf1 ≡ (CONST step Γ)⇧+⇧+ cf0 cf1"

abbreviation 
 "step_n_trancl" :: "[('s,'p,'f) body, ('s,'p,'f) config,nat,('s,'p,'f) config] ⇒ bool"
                                (‹_⊢ (_ →⇧n_/ _)› [81,81,81,81] 100)
 where
  "Γ ⊢cf0 →⇧nn cf1 ≡ (CONST step Γ ^^ n) cf0 cf1"

lemma no_step_final: 
  assumes step: "Γ ⊢(c,s) → (c',s')"
  shows "final (c,s) ⟹ P"
using step
by induct (auto simp add: final_def)

lemma no_step_final':
  assumes step: "Γ ⊢cfg → cfg'"
  shows "final cfg ⟹ P"
using step
  by (cases cfg, cases cfg') (auto intro: no_step_final)

lemma no_steps_final:
"Γ ⊢ v →⇧* w ⟹ final v ⟹ w = v"
  apply (cases v)
  apply simp
  apply  (erule converse_rtranclpE)
   apply simp
   apply (erule (1) no_step_final')
 done

lemma step_Fault: 
  assumes step: "Γ ⊢ (c, s) → (c', s')"
  shows "⋀f. s=Fault f ⟹ s'=Fault f"
using step

by (induct) auto

lemma step_Stuck: 
  assumes step: "Γ ⊢ (c, s) → (c', s')"
  shows "⋀f. s=Stuck ⟹ s'=Stuck"
using step
by (induct) auto

lemma SeqSteps: 
  assumes steps: "Γ ⊢cfg⇩1→⇧* cfg⇩2"
  shows "⋀ c⇩1 s c⇩1' s'. ⟦cfg⇩1 = (c⇩1,s);cfg⇩2=(c⇩1',s')⟧
          ⟹ Γ ⊢(Seq c⇩1 c⇩2,s) →⇧* (Seq c⇩1' c⇩2, s')"
using steps
proof (induct rule: converse_rtranclp_induct [case_names Refl Trans])
  case Refl
  thus ?case
    by simp
next
  case (Trans cfg⇩1 cfg'')
  have step: "Γ ⊢ cfg⇩1 → cfg''" by fact
  have steps: "Γ ⊢ cfg'' →⇧* cfg⇩2" by fact
  have cfg⇩1: "cfg⇩1 = (c⇩1, s)" and cfg⇩2: "cfg⇩2 = (c⇩1', s')"  by fact+
  obtain c⇩1'' s'' where cfg'': "cfg''=(c⇩1'',s'')"
    by (cases cfg'') auto
  from step cfg⇩1 cfg'' 
  have "Γ ⊢ (c⇩1,s) → (c⇩1'',s'')"
    by simp
  hence "Γ ⊢ (Seq c⇩1 c⇩2,s) → (Seq c⇩1'' c⇩2,s'')"
    by (rule step.Seq)
  also from Trans.hyps (3) [OF cfg'' cfg⇩2]
  have "Γ ⊢ (Seq c⇩1'' c⇩2, s'') →⇧* (Seq c⇩1' c⇩2, s')" .
  finally show ?case .
qed


lemma CatchSteps: 
  assumes steps: "Γ ⊢cfg⇩1→⇧* cfg⇩2"
  shows "⋀ c⇩1 s c⇩1' s'. ⟦cfg⇩1 = (c⇩1,s); cfg⇩2=(c⇩1',s')⟧
          ⟹ Γ ⊢(Catch c⇩1 c⇩2,s) →⇧* (Catch c⇩1' c⇩2, s')"
using steps
proof (induct rule: converse_rtranclp_induct [case_names Refl Trans])
  case Refl
  thus ?case
    by simp
next
  case (Trans cfg⇩1 cfg'')
  have step: "Γ ⊢ cfg⇩1 → cfg''" by fact
  have steps: "Γ ⊢ cfg'' →⇧* cfg⇩2" by fact
  have cfg⇩1: "cfg⇩1 = (c⇩1, s)" and cfg⇩2: "cfg⇩2 = (c⇩1', s')"  by fact+
  obtain c⇩1'' s'' where cfg'': "cfg''=(c⇩1'',s'')"
    by (cases cfg'') auto
  from step cfg⇩1 cfg'' 
  have s: "Γ ⊢ (c⇩1,s) → (c⇩1'',s'')"
    by simp
  hence "Γ ⊢ (Catch c⇩1 c⇩2,s) → (Catch c⇩1'' c⇩2,s'')"
    by (rule step.Catch)
  also from Trans.hyps (3) [OF cfg'' cfg⇩2]
  have "Γ ⊢ (Catch c⇩1'' c⇩2, s'') →⇧* (Catch c⇩1' c⇩2, s')" .
  finally show ?case .      
qed


lemma steps_Fault: "Γ ⊢ (c, Fault f) →⇧* (Skip, Fault f)"
proof (induct c)
  case (Seq c⇩1 c⇩2)
  have steps_c⇩1: "Γ ⊢ (c⇩1, Fault f) →⇧* (Skip, Fault f)" by fact
  have steps_c⇩2: "Γ ⊢ (c⇩2, Fault f) →⇧* (Skip, Fault f)" by fact
  from SeqSteps [OF steps_c⇩1 refl refl]
  have "Γ ⊢ (Seq c⇩1 c⇩2, Fault f) →⇧* (Seq Skip c⇩2, Fault f)".
  also
  have "Γ ⊢ (Seq Skip c⇩2, Fault f) → (c⇩2, Fault f)" by (rule SeqSkip)
  also note steps_c⇩2
  finally show ?case by simp
next
  case (Catch c⇩1 c⇩2)
  have steps_c⇩1: "Γ ⊢ (c⇩1, Fault f) →⇧* (Skip, Fault f)" by fact
  from CatchSteps [OF steps_c⇩1 refl refl]
  have "Γ ⊢ (Catch c⇩1 c⇩2, Fault f) →⇧* (Catch Skip c⇩2, Fault f)".
  also
  have "Γ ⊢ (Catch Skip c⇩2, Fault f) → (Skip, Fault f)" by (rule CatchSkip) 
  finally show ?case by simp
qed (fastforce intro: step.intros)+

lemma steps_Stuck: "Γ ⊢ (c, Stuck) →⇧* (Skip, Stuck)"
proof (induct c)
  case (Seq c⇩1 c⇩2)
  have steps_c⇩1: "Γ ⊢ (c⇩1, Stuck) →⇧* (Skip, Stuck)" by fact
  have steps_c⇩2: "Γ ⊢ (c⇩2, Stuck) →⇧* (Skip, Stuck)" by fact
  from SeqSteps [OF steps_c⇩1 refl refl]
  have "Γ ⊢ (Seq c⇩1 c⇩2, Stuck) →⇧* (Seq Skip c⇩2, Stuck)".
  also
  have "Γ ⊢ (Seq Skip c⇩2, Stuck) → (c⇩2, Stuck)" by (rule SeqSkip)
  also note steps_c⇩2
  finally show ?case by simp
next
  case (Catch c⇩1 c⇩2)
  have steps_c⇩1: "Γ ⊢ (c⇩1, Stuck) →⇧* (Skip, Stuck)" by fact
  from CatchSteps [OF steps_c⇩1 refl refl]
  have "Γ ⊢ (Catch c⇩1 c⇩2, Stuck) →⇧* (Catch Skip c⇩2, Stuck)" .
  also
  have "Γ ⊢ (Catch Skip c⇩2, Stuck) → (Skip, Stuck)" by (rule CatchSkip) 
  finally show ?case by simp
qed (fastforce intro: step.intros)+

lemma step_Fault_prop: 
  assumes step: "Γ ⊢ (c, s) → (c', s')"
  shows "⋀f. s=Fault f ⟹ s'=Fault f"
using step
by (induct) auto

lemma step_Stuck_prop: 
  assumes step: "Γ ⊢ (c, s) → (c', s')"
  shows "s=Stuck ⟹ s'=Stuck"
using step
by (induct) auto

lemma steps_Fault_prop: 
  assumes step: "Γ ⊢ (c, s) →⇧* (c', s')"
  shows "s=Fault f ⟹ s'=Fault f"
using step
proof (induct rule: converse_rtranclp_induct2 [case_names Refl Trans])
  case Refl thus ?case by simp
next
  case (Trans c s c'' s'')
  thus ?case
    by (auto intro: step_Fault_prop)
qed

lemma steps_Stuck_prop: 
  assumes step: "Γ ⊢ (c, s) →⇧* (c', s')"
  shows "s=Stuck ⟹ s'=Stuck"
using step
proof (induct rule: converse_rtranclp_induct2 [case_names Refl Trans])
  case Refl thus ?case by simp
next
  case (Trans c s c'' s'')
  thus ?case
    by (auto intro: step_Stuck_prop)
qed

end