Theory AuxiliaryLemmas

theory AuxiliaryLemmas
imports UnwindingConditions
begin


context Unwinding
begin

(* Main lemma on output step consistency 
 (Lemma 5.4.2 in Heiko Mantel's dissertation)*)
lemma osc_property: 
"⋀s1 s1'. ⟦ osc ur; s1 ∈ S⇘SES⇙; s1' ∈ S⇘SES⇙; α ↿ C⇘𝒱⇙ = []; 
  reachable SES s1; reachable SES s1'; enabled SES s1' α; (s1', s1) ∈ ur ⟧
  ⟹ (∃α'. α' ↿ C⇘𝒱⇙ = [] ∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ enabled SES s1 α')" 
proof (induct α)
  case Nil
  have "[] ↿ C⇘𝒱⇙ = [] ∧
    [] ↿ V⇘𝒱⇙ = [] ↿ V⇘𝒱⇙ ∧ enabled SES s1 []" 
    by (simp add: enabled_def projection_def)
  thus ?case by (rule exI)
next
  case (Cons e1 α1)
  assume osc_true: "osc ur"
  assume s1_in_S: "s1 ∈ S⇘SES⇙"
  assume s1'_in_S: "s1' ∈ S⇘SES⇙"
  assume e1α1_C_empty: "(e1 # α1) ↿ C⇘𝒱⇙ = []"
  assume reachable_s1: "reachable SES s1"
  assume reachable_s1': "reachable SES s1'"
  assume enabled_s1'_e1α1: "enabled SES s1' (e1 # α1)"
  assume unwindingrel_s1'_s1: "(s1', s1) ∈ ur"

  have e1α1_no_c: "∀a ∈ (set (e1 # α1)). a ∈ (E⇘SES⇙ - C⇘𝒱⇙)"
  proof -
    from reachable_s1' obtain β 
      where "s0⇘SES⇙ β⟹⇘SES⇙ s1'"
      by(simp add: reachable_def, auto)
    moreover
    from enabled_s1'_e1α1 obtain s1337
      where "s1' (e1 # α1)⟹⇘SES⇙ s1337"
      by(simp add: enabled_def, auto)
    ultimately have "s0⇘SES⇙ (β @ (e1 # α1))⟹⇘SES⇙ s1337"
      by(rule path_trans)
    hence "β @ (e1 # α1) ∈ Tr⇘(induceES SES)⇙"
      by (simp add: induceES_def possible_traces_def enabled_def)
    with validSES induceES_yields_ES[of "SES"] have "∀a ∈ (set (β @ (e1 # α1))). a ∈ E⇘SES⇙"
      by (simp add: induceES_def ES_valid_def traces_contain_events_def)
    hence "∀ a ∈ (set (e1 # α1)). a ∈ E⇘SES⇙"
      by auto
    with e1α1_C_empty show ?thesis
      by (simp only: projection_def filter_empty_conv, auto)
  qed

  from enabled_s1'_e1α1 obtain s2' where 
    s1'_e1_s2': "s1' e1⟶⇘SES⇙ s2'" 
    by (simp add: enabled_def, split if_split_asm, auto)
  with validSES have s2'_in_S: "s2' ∈ S⇘SES⇙" 
    by (simp add: SES_valid_def correct_transition_relation_def)
  have reachable_s2': "reachable SES s2'"
  proof -
    from reachable_s1' obtain t where 
      path_to_s1': "s0⇘SES⇙ t⟹⇘SES⇙ s1'" 
      by (simp add: reachable_def, auto)
    from s1'_e1_s2' have "s1' [e1]⟹⇘SES⇙ s2'" 
      by simp
    with path_to_s1' have "s0⇘SES⇙ (t @ [e1])⟹⇘SES⇙ s2'" 
      by (simp add: path_trans)
    thus ?thesis by (simp add: reachable_def, rule exI)
  qed
  from s1'_e1_s2' enabled_s1'_e1α1 obtain sn' where 
    "s2' α1⟹⇘SES⇙ sn'" 
    by (simp add: enabled_def, auto)
  hence enabled_s2'_α1: "enabled SES s2' α1" 
    by (simp add: enabled_def)
  from e1α1_no_c have e1_no_c: "e1 ∈ (E⇘SES⇙ - C⇘𝒱⇙)" 
    by simp
  from e1α1_no_c have α1_no_c: "∀a∈(set α1). (a ∈ (E⇘SES⇙ - C⇘𝒱⇙))" 
    by simp
  hence α1_proj_C_empty: "α1 ↿ C⇘𝒱⇙ = []"
    by (simp add: projection_def)
  from osc_true have 
    "⟦ s1 ∈ S⇘SES⇙; s1' ∈ S⇘SES⇙; s2' ∈ S⇘SES⇙; 
      e1 ∈ (E⇘SES⇙ - C⇘𝒱⇙); reachable SES s1; reachable SES s1'; 
      s1' e1⟶⇘SES⇙ s2'; (s1', s1) ∈ ur ⟧ 
     ⟹ (∃s2 ∈ S⇘SES⇙. ∃δ. δ ↿ C⇘𝒱⇙ = []
        ∧ (δ ↿ V⇘𝒱⇙) = ([e1] ↿ V⇘𝒱⇙) ∧ (s1 δ⟹⇘SES⇙ s2 ∧ 
       ((s2', s2) ∈ ur)))"
    by (simp add: osc_def)
  with s1_in_S s1'_in_S e1_no_c reachable_s1 reachable_s1' 
    s2'_in_S s1'_e1_s2' unwindingrel_s1'_s1 
  obtain s2 δ where 
    osc_conclusion: 
      "s2 ∈ S⇘SES⇙ ∧ δ ↿ C⇘𝒱⇙ = [] ∧
      (δ ↿ V⇘𝒱⇙) = ([e1] ↿ V⇘𝒱⇙) ∧ s1 δ⟹⇘SES⇙ s2 ∧ 
      ((s2', s2) ∈ ur)"
    by auto
  hence δ_proj_C_empty: "δ ↿ C⇘𝒱⇙ = []"
    by (simp add: projection_def)
  from osc_conclusion have s2_in_S: "s2 ∈ S⇘SES⇙" 
    by auto
  from osc_conclusion have unwindingrel_s2'_s2: "(s2', s2) ∈ ur" 
    by auto
  have reachable_s2: "reachable SES s2"
  proof -
    from reachable_s1 obtain t where 
      path_to_s1: "s0⇘SES⇙ t⟹⇘SES⇙ s1" 
      by (simp add: reachable_def, auto)
    from osc_conclusion have "s1 δ⟹⇘SES⇙ s2" 
      by auto
    with path_to_s1 have "s0⇘SES⇙ (t @ δ)⟹⇘SES⇙ s2" 
      by (simp add: path_trans)
    thus ?thesis by (simp add: reachable_def, rule exI)
  qed

  from Cons osc_true s2_in_S s2'_in_S α1_proj_C_empty
    reachable_s2 reachable_s2' enabled_s2'_α1 unwindingrel_s2'_s2
  obtain α'' where α''_props:
    "α'' ↿ C⇘𝒱⇙ = [] ∧ α'' ↿ V⇘𝒱⇙ = α1 ↿ V⇘𝒱⇙ ∧ enabled SES s2 α''"
    by auto
  with osc_conclusion have  δα''_props:
    "(δ @ α'') ↿ C⇘𝒱⇙ = [] ∧ 
    (δ @ α'') ↿ V⇘𝒱⇙ = (e1#α1) ↿ V⇘𝒱⇙ ∧ enabled SES s1 (δ @ α'')"
    by (simp add: projection_def enabled_def, auto, simp add: path_trans)
  hence "(δ @ α'') ↿ C⇘𝒱⇙ = []"
    by (simp add: projection_def)
  thus ?case using δα''_props by auto
qed

(* Paths will not bring us out of the domain of states.  *)
lemma path_state_closure: "⟦ s τ⟹⇘SES⇙ s'; s ∈ S⇘SES⇙ ⟧ ⟹ s' ∈ S⇘SES⇙"
  (is "⟦ ?P s τ s'; ?S s SES ⟧ ⟹ ?S s' SES ")
proof (induct τ arbitrary: s s')
  case Nil with validSES show ?case 
    by (auto simp add: SES_valid_def correct_transition_relation_def)
next
  case (Cons e τ) thus ?case
  proof -
    assume path_eτ: "?P s (e # τ) s'" 
    assume induct_hypo: "⋀ s s'. ⟦ ?P s τ s'; ?S s SES ⟧ ⟹ ?S s' SES"
    
    from path_eτ obtain s'' where s_e_s'': "s e⟶⇘SES⇙ s''" 
      by(simp add: path_def, split if_split_asm, auto)
    with validSES have s''_in_S: "?S s'' SES" 
      by (simp add: SES_valid_def correct_transition_relation_def)
    
    from s_e_s'' path_eτ have path_τ: "?P s'' τ s'" by auto
    
    from path_τ s''_in_S show ?case by (rule induct_hypo)
  qed
qed


(* Theorem 5.4.7 split into two parts *)

(* first part *)
theorem En_to_Adm:
"⟦ reachable SES s; En ρ s e⟧ 
⟹ ∃β. ( s0⇘SES⇙ β⟹⇘SES⇙ s ∧ Adm 𝒱 ρ Tr⇘(induceES SES)⇙ β e )" 
proof -
  assume "En ρ s e"
  then obtain β γ s' s'' 
    where "s0⇘SES⇙ β⟹⇘SES⇙ s"
    and   "γ ↿ (ρ 𝒱) = β ↿ (ρ 𝒱)" 
    and   s0_γ_s': "s0⇘SES⇙ γ⟹⇘SES⇙ s'" 
    and   s'_e_s'': "s' e⟶⇘SES⇙ s''"
    by (simp add: En_def, auto)
  moreover 
    from s0_γ_s' s'_e_s'' have "s0⇘SES⇙ (γ @ [e])⟹⇘SES⇙ s''"
      by (rule path_trans_single)
    hence "(γ @ [e]) ∈ Tr⇘(induceES SES)⇙"
      by(simp add: induceES_def possible_traces_def enabled_def)
  ultimately show ?thesis
    by (simp add: Adm_def, auto)
qed

(* second part *)
theorem Adm_to_En:
"⟦ β ∈ Tr⇘(induceES SES)⇙; Adm 𝒱 ρ Tr⇘(induceES SES)⇙ β e ⟧
⟹ ∃s ∈ S⇘SES⇙. (s0⇘SES⇙ β⟹⇘SES⇙ s ∧ En ρ s e)"
proof -
  from validSES have s0_in_S: "s0⇘SES⇙ ∈ S⇘SES⇙"
       by (simp add: SES_valid_def s0_is_state_def) 
  
  assume "β ∈ Tr⇘(induceES SES)⇙"
  then obtain s
    where s0_β_s: "s0⇘SES⇙ β⟹⇘SES⇙ s"
    by (simp add: induceES_def possible_traces_def enabled_def, auto)
  from this have s_in_S: "s ∈ S⇘SES⇙" using s0_in_S
    by (rule path_state_closure)

  assume  "Adm 𝒱 ρ Tr⇘(induceES SES)⇙ β e"
  then obtain γ
    where ργ_is_ρβ: "γ ↿ (ρ 𝒱) = β ↿ (ρ 𝒱)"
    and   "∃s''. s0⇘SES⇙ (γ @ [e])⟹⇘SES⇙ s''"
    by(simp add: Adm_def induceES_def possible_traces_def enabled_def, auto)
  then obtain s''
    where  s0_γe_s'': "s0⇘SES⇙ (γ @ [e])⟹⇘SES⇙ s''"
    by auto
  from this have s''_in_S: "s'' ∈ S⇘SES⇙" using s0_in_S
    by (rule path_state_closure)
  
  from path_split_single[OF s0_γe_s''] obtain s' 
    where s0_γ_s': "s0⇘SES⇙ γ⟹⇘SES⇙ s'"
    and s'_e_s'': "s' e⟶⇘SES⇙ s''"
    by auto

  from path_state_closure[OF s0_γ_s' s0_in_S] have s'_in_S: "s' ∈ S⇘SES⇙". 
  
  from s'_in_S s''_in_S s0_β_s ργ_is_ρβ s0_γ_s' s'_e_s'' s_in_S show ?thesis 
    by (simp add: En_def, auto)
qed


(* It is a common pattern in the unwinding theorem proofs to obtain 
 a state from a given trace in a state event system and deduce some of its
 properties. This can be accomplished with the following lemma: 
*)
lemma state_from_induceES_trace: 
  "⟦  (β @ α) ∈ Tr⇘(induceES SES)⇙ ⟧ 
  ⟹ ∃s ∈ S⇘SES⇙. s0⇘SES⇙ β⟹⇘SES⇙ s ∧ enabled SES s α ∧ reachable SES s"
  proof -
    
    assume βα_in_Tr: "(β @ α) ∈ Tr⇘(induceES SES)⇙"
    then obtain s' where  s0_βα_s':"s0⇘SES⇙ (β @ α)⟹⇘SES⇙ s'" 
      by (simp add: induceES_def possible_traces_def enabled_def, auto)
    
    from path_split[OF s0_βα_s'] obtain s 
      where s0_β_s: "s0⇘SES⇙ β⟹⇘SES⇙ s" 
      and "s α⟹⇘SES⇙ s'"
      by auto    
    hence enabled_s_α: "enabled SES s α"
      by (simp add: enabled_def)
    
    from s0_β_s have reachable_s: "reachable SES s"
      by(simp add: reachable_def, auto)
    
    from validSES have "s0⇘SES⇙ ∈ S⇘SES⇙"
      by (simp add: SES_valid_def s0_is_state_def)
    with s0_β_s have s_in_S: "s ∈ S⇘SES⇙"
      by (rule path_state_closure)
    with s0_β_s enabled_s_α reachable_s show ?thesis
      by auto
  qed

(* Another common pattern in unwinding results: *)
lemma path_split2:"s0⇘SES⇙ (β @ α)⟹⇘SES⇙ s 
  ⟹ ∃s' ∈ S⇘SES⇙. ( s0⇘SES⇙ β⟹⇘SES⇙ s' ∧ s' α⟹⇘SES⇙ s ∧ reachable SES s' )"
proof - 
  assume s0_βα_s: "s0⇘SES⇙ (β @ α)⟹⇘SES⇙ s"

  from path_split[OF s0_βα_s] obtain s' 
    where s0_β_s': "s0⇘SES⇙ β⟹⇘SES⇙ s'"
    and s'_α_s: "s' α⟹⇘SES⇙ s"
    by auto
  hence "reachable SES s'"
    by(simp add: reachable_def, auto)  
  moreover
  have "s' ∈ S⇘SES⇙"
    proof -
      from s0_β_s' validSES path_state_closure show ?thesis
        by (auto simp add: SES_valid_def s0_is_state_def)
    qed

  ultimately show ?thesis using s'_α_s s0_β_s'
    by(auto)
qed 


(* Variant for singleton lists *)
lemma path_split_single2:
  "s0⇘SES⇙ (β @ [x])⟹⇘SES⇙ s
  ⟹ ∃s' ∈ S⇘SES⇙. ( s0⇘SES⇙ β⟹⇘SES⇙ s' ∧ s' x⟶⇘SES⇙ s ∧ reachable SES s' )"
proof - 
  assume s0_βx_s: "s0⇘SES⇙ (β @ [x])⟹⇘SES⇙ s"

  from path_split2[OF s0_βx_s] show ?thesis
    by (auto, split if_split_asm, auto)
qed 

      
lemma modified_view_valid: "isViewOn ⦇V = (V⇘𝒱⇙ ∪ N⇘𝒱⇙), N = {}, C = C⇘𝒱⇙⦈ E⇘SES⇙"
  using validVU 
    unfolding isViewOn_def V_valid_def VC_disjoint_def VN_disjoint_def NC_disjoint_def by auto
    
end

end