Theory Phi_Semantics_Framework.Phi_SemFrame_ex

theory Phi_SemFrame_ex
imports Phi_Semantics_Framework
begin

declare [[typedef_overloaded]]

datatype 'ret eval_stat = Normal ‹'ret φarg› | Abnm ABNM | Crash

declare [[typedef_overloaded = false]]

lemma eval_stat_forall:
  ‹All P ⟷ (∀ret. P (Normal ret)) ∧ (∀e. P (Abnm e)) ∧ P Crash›
  by (metis eval_stat.exhaust)

lemma eval_stat_ex:
  ‹Ex P ⟷ (∃ret. P (Normal ret)) ∨ (∃e. P (Abnm e)) ∨ P Crash›
  by (metis eval_stat.exhaust)

definition Transition_of' :: ‹'ret proc ⇒ 'ret eval_stat ⇒ resource rel›
  where ‹Transition_of' f = (λx. (case x of Normal v ⇒ { (s,s'). Success v s' ∈ f s ∧ s ∈ RES.SPACE }
                                          | Abnm e ⇒ { (s,s'). Abnormal e s' ∈ f s ∧ s ∈ RES.SPACE }
                                          | Crash ⇒ { (s,s'). Invalid ∈ f s ∧ s = s' ∧ s ∈ RES.SPACE }))›

definition Valid_Transition :: ‹('ret eval_stat ⇒ 'a rel) ⇒ bool›
  where ‹Valid_Transition tr ⟷ tr Crash = {}›




end