(*
 * 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₁ c₂) = redex c₁" |
"redex (Cond b c₁ c₂) = (Cond b c₁ c₂)" |
"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₁ c₂) = redex c₁" |
"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
 , or @{term "(Throw,Normal s)"} in case the program was started in
  @{term "Normal"} state and terminated abruptly. Explicit abrupt states are removed
  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₁ c₂) = (atom_com c₁ ∧ atom_com c₂)" | 
  "atom_com (Cond b c₁ c₂) = (atom_com c₁ ∧ atom_com c₂)" | 
  "atom_com (While b c) = atom_com c" | 
 (* Change to  atom_com (Call p) = atom_com (\<Theta> 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₁ c₂) = (atom_com c₁ ∧ atom_com c₂)" | 
  "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₁,s) → (c₁',s')
        ==>
        Γ ⊨(Seq c₁ c₂,s) → (Seq c₁' c₂, s')"
| SeqSkip: "Γ ⊨(Seq Skip c₂,s) → (c₂, s)"
| SeqThrow: "Γ ⊨(Seq Throw c₂,Normal s) → (Throw, Normal s)"

| CondTrue:  "s∈b ==> Γ ⊨(Cond b c₁ c₂,Normal s) → (c₁,Normal s)"
| CondFalse: "s∉b ==> Γ ⊨(Cond b c₁ c₂,Normal s) → (c₂,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₁,s) → (c₁',s')]
          ==>
          Γ ⊨(Catch c₁ c₂,s) → (Catch c₁' c₂,s')"

| CatchSkip: "Γ ⊨(Catch Skip c₂,s) → (Skip,s)"
| CatchThrow: "Γ ⊨(Catch Throw c₂,Normal s) → (c₂,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
 . It is the intention that ‹∃cfg. Γ ⊨ (c, s) → cfg) ∨ final (c, s) ∨ blocked Γ c s›, but
  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₁) c₂) (Normal s) = (s ∉ b)"
| "blocked Γ (Catch (Await b c₁) c₂) (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 →ⁿⁿ 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₁→^* cfg₂"
  shows "∧ c₁ s c₁' s'. [cfg₁ = (c₁,s);cfg₂=(c₁',s')]
          ==> Γ ⊨(Seq c₁ c₂,s) →^* (Seq c₁' c₂, s')"
using steps
proof (induct rule: converse_rtranclp_induct [case_names Refl Trans])
  case Refl
  thus ?case
    by simp
next
  case (Trans cfg₁ cfg'')
  have step: "Γ ⊨ cfg₁ → cfg''" by fact
  have steps: "Γ ⊨ cfg'' →^* cfg₂" by fact
  have cfg₁: "cfg₁ = (c₁, s)" and cfg₂: "cfg₂ = (c₁', s')"  by fact+
  obtain c₁'' s'' where cfg'': "cfg''=(c₁'',s'')"
    by (cases cfg'') auto
  from step cfg₁ cfg'' 
  have "Γ ⊨ (c₁,s) → (c₁'',s'')"
    by simp
  hence "Γ ⊨ (Seq c₁ c₂,s) → (Seq c₁'' c₂,s'')"
    by (rule step.Seq)
  also from Trans.hyps (3) [OF cfg'' cfg₂]
  have "Γ ⊨ (Seq c₁'' c₂, s'') →^* (Seq c₁' c₂, s')" .
  finally show ?case .
qed


lemma CatchSteps: 
  assumes steps: "Γ ⊨cfg₁→^* cfg₂"
  shows "∧ c₁ s c₁' s'. [cfg₁ = (c₁,s); cfg₂=(c₁',s')]
          ==> Γ ⊨(Catch c₁ c₂,s) →^* (Catch c₁' c₂, s')"
using steps
proof (induct rule: converse_rtranclp_induct [case_names Refl Trans])
  case Refl
  thus ?case
    by simp
next
  case (Trans cfg₁ cfg'')
  have step: "Γ ⊨ cfg₁ → cfg''" by fact
  have steps: "Γ ⊨ cfg'' →^* cfg₂" by fact
  have cfg₁: "cfg₁ = (c₁, s)" and cfg₂: "cfg₂ = (c₁', s')"  by fact+
  obtain c₁'' s'' where cfg'': "cfg''=(c₁'',s'')"
    by (cases cfg'') auto
  from step cfg₁ cfg'' 
  have s: "Γ ⊨ (c₁,s) → (c₁'',s'')"
    by simp
  hence "Γ ⊨ (Catch c₁ c₂,s) → (Catch c₁'' c₂,s'')"
    by (rule step.Catch)
  also from Trans.hyps (3) [OF cfg'' cfg₂]
  have "Γ ⊨ (Catch c₁'' c₂, s'') →^* (Catch c₁' c₂, s')" .
  finally show ?case .      
qed


lemma steps_Fault: "Γ ⊨ (c, Fault f) →^* (Skip, Fault f)"
proof (induct c)
  case (Seq c₁ c₂)
  have steps_c₁: "Γ ⊨ (c₁, Fault f) →^* (Skip, Fault f)" by fact
  have steps_c₂: "Γ ⊨ (c₂, Fault f) →^* (Skip, Fault f)" by fact
  from SeqSteps [OF steps_c₁ refl refl]
  have "Γ ⊨ (Seq c₁ c₂, Fault f) →^* (Seq Skip c₂, Fault f)".
  also
  have "Γ ⊨ (Seq Skip c₂, Fault f) → (c₂, Fault f)" by (rule SeqSkip)
  also note steps_c₂
  finally show ?case by simp
next
  case (Catch c₁ c₂)
  have steps_c₁: "Γ ⊨ (c₁, Fault f) →^* (Skip, Fault f)" by fact
  from CatchSteps [OF steps_c₁ refl refl]
  have "Γ ⊨ (Catch c₁ c₂, Fault f) →^* (Catch Skip c₂, Fault f)".
  also
  have "Γ ⊨ (Catch Skip c₂, 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₁ c₂)
  have steps_c₁: "Γ ⊨ (c₁, Stuck) →^* (Skip, Stuck)" by fact
  have steps_c₂: "Γ ⊨ (c₂, Stuck) →^* (Skip, Stuck)" by fact
  from SeqSteps [OF steps_c₁ refl refl]
  have "Γ ⊨ (Seq c₁ c₂, Stuck) →^* (Seq Skip c₂, Stuck)".
  also
  have "Γ ⊨ (Seq Skip c₂, Stuck) → (c₂, Stuck)" by (rule SeqSkip)
  also note steps_c₂
  finally show ?case by simp
next
  case (Catch c₁ c₂)
  have steps_c₁: "Γ ⊨ (c₁, Stuck) →^* (Skip, Stuck)" by fact
  from CatchSteps [OF steps_c₁ refl refl]
  have "Γ ⊨ (Catch c₁ c₂, Stuck) →^* (Catch Skip c₂, Stuck)" .
  also
  have "Γ ⊨ (Catch Skip c₂, 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