Theory SM_Indep

theory SM_Indep
imports 
  "../Refine/SM_Finite_Reachable" 
  Partial_Order_Reduction.Transition_System_Interpreted_Traces
  SM_Variables
begin

context visible_prog
begin
  
  fun ind :: "global_action option ⇒ global_action option ⇒ bool" where
    "ind None None ⟷ True"
  | "ind (Some _) None ⟷ False"
  | "ind None (Some _) ⟷ False"
  | "ind (Some (pid1,c1,a1,c1')) (Some (pid2,c2,a2,c2')) 
    ⟷ 
      pid1≠pid2
    ∧ (write_globals a1 ∩ read_globals a2 = {})
    ∧ (write_globals a2 ∩ read_globals a1 = {})
    ∧ (write_globals a1 ∩ write_globals a2 = {})
    ∧ (¬( Some (pid1,c1,a1,c1')∈jsys.visible 
        ∧ Some (pid2,c2,a2,c2') ∈ jsys.visible))"
  
  lemma ind_symmetric: "ind a b ⟷ ind b a"
    by (cases "(a,b)" rule: ind.cases) auto
  
  lemma ga_ex_swap:
    assumes PIDNE: "pid1≠pid2"
    assumes DJ: 
      "write_globals a1 ∩ read_globals a2 = {}"
      "write_globals a2 ∩ read_globals a1 = {}"
      "write_globals a1 ∩ write_globals a2 = {}"
    shows "ga_ex (Some (pid1,c1,a1,c1')) (ga_ex (Some (pid2,c2,a2,c2')) gc) 
         = ga_ex (Some (pid2,c2,a2,c2')) (ga_ex (Some (pid1,c1,a1,c1')) gc)"
    using PIDNE
    apply (auto 
      simp: ga_ex_def ga_gex_def 
      simp: list_update_swap dest: ex_swap_global[OF DJ]
      split: prod.splits)
    done
  
  corollary ind_swap:
    "ind ga1 ga2 ⟹ ga_ex ga2 (ga_ex ga1 gc) = ga_ex ga1 (ga_ex ga2 gc)"
    apply (cases "(ga1,ga2)" rule: ind.cases)
    apply (auto intro: ga_ex_swap)
    done
  
  
  lemma ind_en: "⟦ind a b; a ∈ ga_en p⟧
         ⟹ (b ∈ ga_en (ga_ex a p)) = (b ∈ ga_en p)"
    apply (cases "(a,b)" rule: ind.cases, simp_all)
    apply (auto 
      simp: ga_ex_def ga_en_def ga_gex_def ga_gen_def ex_pres_en
      split: prod.splits
      )
    done
  
  sublocale jsys: transition_system_traces ga_ex "λ a p. a ∈ ga_en p" ind
    apply unfold_locales
    apply (simp_all add: ind_symmetric ind_en ind_swap)
    done
      
  sublocale jsys: transition_system_interpreted_traces 
    ga_ex "λ a p. a ∈ ga_en p" pid_interp_gc
    ind
    apply unfold_locales
    apply (case_tac "(a,b)" rule: ind.cases)
    apply (auto simp: jsys.visible_def)
    done
  
  end
end