Theory SM_Variables

section ‹Accessed Variables›
theory SM_Variables
imports "../Refine/SM_Pid"
begin

  subsection "Expressions"

  primrec udvars_of_exp :: "exp ⇒ ident set" where
      "udvars_of_exp (e_var x) = {x}"
    | "udvars_of_exp (e_localvar x) = {}"
    | "udvars_of_exp (e_globalvar x) = {}"
    | "udvars_of_exp (e_const c) = {}"
    | "udvars_of_exp (e_bin bop e1 e2) = (udvars_of_exp e1) ∪ (udvars_of_exp e2)"
    | "udvars_of_exp (e_un uop e) = (udvars_of_exp e)"

  primrec lvars_of_exp :: "exp ⇒ ident set" where
      "lvars_of_exp (e_var x) = {}"
    | "lvars_of_exp (e_localvar x) = {x}"
    | "lvars_of_exp (e_globalvar x) = {}"
    | "lvars_of_exp (e_const c) = {}"
    | "lvars_of_exp (e_bin bop e1 e2) = (lvars_of_exp e1) ∪ (lvars_of_exp e2)"
    | "lvars_of_exp (e_un uop e) = (lvars_of_exp e)"
      
  primrec gvars_of_exp :: "exp ⇒ ident set" where
      "gvars_of_exp (e_var x) = {}"
    | "gvars_of_exp (e_localvar x) = {}"
    | "gvars_of_exp (e_globalvar x) = {x}"
    | "gvars_of_exp (e_const c) = {}"
    | "gvars_of_exp (e_bin bop e1 e2) = (gvars_of_exp e1) ∪ (gvars_of_exp e2)"
    | "gvars_of_exp (e_un uop e) = (gvars_of_exp e)"

  subsection "Commands"
  primrec join_cmd_exp :: "'a ⇒ ('a ⇒ 'a ⇒ 'a) ⇒ (exp ⇒ 'a) ⇒ cmd ⇒ 'a" where  
    "join_cmd_exp z join f (Assign c x e) = join (f c) (f e)"
  | "join_cmd_exp z join f (Assign_local c x e) = join (f c) (f e)"
  | "join_cmd_exp z join f (Assign_global c x e) = join (f c) (f e)"
  | "join_cmd_exp z join f (Test e) = f e"
  | "join_cmd_exp z join f (Skip) = z"
  | "join_cmd_exp z join f (Seq c1 c2) 
      = join (join_cmd_exp z join f c1) (join_cmd_exp z join f c2)"
  | "join_cmd_exp z join f (Or c1 c2) 
      = join (join_cmd_exp z join f c1) (join_cmd_exp z join f c2)"
  | "join_cmd_exp z join f (Break) = z"
  | "join_cmd_exp z join f (Continue) = z"
  | "join_cmd_exp z join f (Iterate c1 c2) 
      = join (join_cmd_exp z join f c1) (join_cmd_exp z join f c2)"
  | "join_cmd_exp z join f (Invalid) = z"

  abbreviation "union_cmd_exp ≡ join_cmd_exp {} (∪)"
  abbreviation "all_cmd_exp ≡ join_cmd_exp True (∧)"
  abbreviation "ex_cmd_exp ≡ join_cmd_exp False (∨)"

  abbreviation "ud_rvars_of_cmd == union_cmd_exp udvars_of_exp"
  abbreviation "g_rvars_of_cmd == union_cmd_exp gvars_of_exp"
  abbreviation "l_rvars_of_cmd == union_cmd_exp lvars_of_exp"

  primrec ud_wvars_of_cmd :: "cmd ⇒ ident set" where  
    "ud_wvars_of_cmd (Assign c x e) = {x}"
  | "ud_wvars_of_cmd (Assign_local c x e) = {}"
  | "ud_wvars_of_cmd (Assign_global c x e) = {}"
  | "ud_wvars_of_cmd (Test e) = {}"
  | "ud_wvars_of_cmd (Skip) = {}"
  | "ud_wvars_of_cmd (Seq c1 c2) = (ud_wvars_of_cmd c1 ∪ ud_wvars_of_cmd c2)"
  | "ud_wvars_of_cmd (Or c1 c2) = (ud_wvars_of_cmd c1 ∪ ud_wvars_of_cmd c2)"
  | "ud_wvars_of_cmd (Break) = {}"
  | "ud_wvars_of_cmd (Continue) = {}"
  | "ud_wvars_of_cmd (Iterate c1 c2) = (ud_wvars_of_cmd c1 ∪ ud_wvars_of_cmd c2)"
  | "ud_wvars_of_cmd (Invalid) = {}"

  primrec l_wvars_of_cmd :: "cmd ⇒ ident set" where  
    "l_wvars_of_cmd (Assign c x e) = {}"
  | "l_wvars_of_cmd (Assign_local c x e) = {x}"
  | "l_wvars_of_cmd (Assign_global c x e) = {}"
  | "l_wvars_of_cmd (Test e) = {}"
  | "l_wvars_of_cmd (Skip) = {}"
  | "l_wvars_of_cmd (Seq c1 c2) = (l_wvars_of_cmd c1 ∪ l_wvars_of_cmd c2)"
  | "l_wvars_of_cmd (Or c1 c2) = (l_wvars_of_cmd c1 ∪ l_wvars_of_cmd c2)"
  | "l_wvars_of_cmd (Break) = {}"
  | "l_wvars_of_cmd (Continue) = {}"
  | "l_wvars_of_cmd (Iterate c1 c2) = (l_wvars_of_cmd c1 ∪ l_wvars_of_cmd c2)"
  | "l_wvars_of_cmd (Invalid) = {}"

  primrec g_wvars_of_cmd :: "cmd ⇒ ident set" where  
    "g_wvars_of_cmd (Assign c x e) = {}"
  | "g_wvars_of_cmd (Assign_local c x e) = {}"
  | "g_wvars_of_cmd (Assign_global c x e) = {x}"
  | "g_wvars_of_cmd (Test e) = {}"
  | "g_wvars_of_cmd (Skip) = {}"
  | "g_wvars_of_cmd (Seq c1 c2) = (g_wvars_of_cmd c1 ∪ g_wvars_of_cmd c2)"
  | "g_wvars_of_cmd (Or c1 c2) = (g_wvars_of_cmd c1 ∪ g_wvars_of_cmd c2)"
  | "g_wvars_of_cmd (Break) = {}"
  | "g_wvars_of_cmd (Continue) = {}"
  | "g_wvars_of_cmd (Iterate c1 c2) = (g_wvars_of_cmd c1 ∪ g_wvars_of_cmd c2)"
  | "g_wvars_of_cmd (Invalid) = {}"


  definition "udvars_of_cmd c ≡ ud_rvars_of_cmd c ∪ ud_wvars_of_cmd c"
  definition "lvars_of_cmd c ≡ l_rvars_of_cmd c ∪ l_wvars_of_cmd c"
  definition "gvars_of_cmd c ≡ g_rvars_of_cmd c ∪ g_wvars_of_cmd c"

  fun read_globals :: "action ⇒ ident set" where
    "read_globals (AAssign c _ e) = gvars_of_exp c ∪ udvars_of_exp c ∪
      gvars_of_exp e ∪ udvars_of_exp e"
  | "read_globals (AAssign_local c _ e) = gvars_of_exp c ∪ udvars_of_exp c ∪
      gvars_of_exp e ∪ udvars_of_exp e"
  | "read_globals (AAssign_global c _ e) = gvars_of_exp c ∪ udvars_of_exp c ∪
      gvars_of_exp e ∪ udvars_of_exp e"
  | "read_globals (ATest e) = gvars_of_exp e ∪ udvars_of_exp e"
  | "read_globals (ASkip) = {}"

  fun write_globals :: "action ⇒ ident set" where
    "write_globals (AAssign _ x _) = {x}"
  | "write_globals (AAssign_local _ _ _) = {}"
  | "write_globals (AAssign_global _ x _) = {x}"
  | "write_globals (ATest e) = {}"
  | "write_globals (ASkip) = {}"

  abbreviation "rw_globals a ≡ read_globals a ∪ write_globals a"

  definition eq_on :: "ident set ⇒ valuation ⇒ valuation ⇒ bool"
    where "eq_on X s1 s2 ≡ ∀x∈X. s1 x = s2 x"

  lemma eq_onD: "⟦eq_on X s1 s2; x∈X⟧ ⟹ s1 x = s2 x"
    unfolding eq_on_def by auto  
    
  lemma 
    eq_on_refl[simp]: "eq_on X s s" and
    eq_on_sym: "eq_on X s1 s2 ⟹ eq_on X s2 s1" and
    eq_on_sym_eq: "eq_on X s1 s2 ⟷ eq_on X s2 s1" and
    eq_on_trans[trans]: "⟦eq_on Xa s1 s2; eq_on Xb s2 s3⟧ 
      ⟹ eq_on (Xa∩Xb) s1 s3" and
    eq_on_UNIV_eq[simp]: "eq_on UNIV s1 s2 ⟷ s1=s2"  
    unfolding eq_on_def by auto

  lemma eq_on_join: "⟦eq_on X s s'; eq_on Y s s'⟧ ⟹ eq_on (X∪Y) s s'"
    unfolding eq_on_def by auto

  abbreviation ls_eq_on :: "ident set ⇒ local_state ⇒ local_state ⇒ bool"
    where "ls_eq_on X ls1 ls2 ≡ 
      eq_on X (local_state.variables ls1) (local_state.variables ls2)"  

  abbreviation gs_eq_on :: "ident set ⇒ global_state ⇒ global_state ⇒ bool"
    where "gs_eq_on X ls1 ls2 ≡ 
      eq_on X (global_state.variables ls1) (global_state.variables ls2)"  

  lemma eval_dep_vars:
    assumes "gs_eq_on X gs gs'"    
    assumes "udvars_of_exp e ⊆ X" "gvars_of_exp e ⊆ X"
    shows "eval_exp e (ls,gs) = eval_exp e (ls,gs')"
    using assms
    apply (induction e)
    apply (auto split: option.splits simp: eq_on_def)
    done    

  lemma en_dep_read:
    assumes "gs_eq_on X gs gs'"
    assumes "read_globals a ⊆ X"
    shows "la_en' (ls,gs) a = la_en' (ls,gs') a"
    using assms
    apply (cases a)
    apply (auto 
      simp: la_en'_def eval_dep_vars 
      split: Option.bind_splits)
    done

  lemma ex_mod_limit: 
    assumes "la_ex' (ls,gs) a = (ls',gs')"
    shows "gs_eq_on (-write_globals a) gs gs'"
    using assms
    apply (cases a)
    apply (auto 
      simp: la_ex'_def eval_dep_vars eq_on_def 
      split: option.splits Option.bind_splits)
    apply (auto split: if_split_asm)
    done    

  lemma ex_dep_pres:
    assumes "gs_eq_on X gs1 gs2"
    assumes "read_globals a ⊆ X"
    assumes "la_ex' (ls,gs1) a = (ls1',gs1')"
    assumes "la_ex' (ls,gs2) a = (ls2',gs2')"
    shows "ls1'=ls2' ∧ gs_eq_on X gs1' gs2'"
    using assms
    apply (cases a)
    apply (auto 
      simp: la_ex'_def eval_dep_vars eq_on_def
      split: Option.bind_splits option.splits bool.splits if_split_asm)
    done


  lemma ex_swap_global:
    assumes DJ:
      "write_globals a1 ∩ read_globals a2 = {}"
      "write_globals a2 ∩ read_globals a1 = {}"
      "write_globals a1 ∩ write_globals a2 = {}"
    assumes EXA: 
      "la_ex' (ls1,gs) a1 = (ls1a, gsa)"
      "la_ex' (ls2, gsa) a2 = (ls2a, gsa')"
    assumes EXB:
      "la_ex' (ls2,gs) a2 = (ls2b, gsb)"
      "la_ex' (ls1, gsb) a1 = (ls1b, gsb')"
    shows "ls1a=ls1b" "ls2a=ls2b" "gsa'=gsb'"
  proof -
    from ex_dep_pres[OF ex_mod_limit[OF EXB(1)] _ EXA(1) EXB(2)] DJ
    have "ls1a = ls1b" and E1: "gs_eq_on (- write_globals a2) gsa gsb'"
      by auto
    thus [simp]: "ls1a=ls1b" by simp
      
    from 
      ex_dep_pres[OF 
        ex_mod_limit[OF EXA(1), THEN eq_on_sym] _ EXA(2) EXB(1)
      ] DJ
    have "ls2a = ls2b" and E2: "gs_eq_on (- write_globals a1) gsa' gsb"
      by auto
    thus [simp]: "ls2a=ls2b" by simp

    from DJ have [simp]: "- write_globals a1 ∪ - write_globals a2 = UNIV" 
      by auto

    from eq_on_trans[OF E2 ex_mod_limit[OF EXB(2)]]
    have "gs_eq_on (- write_globals a1) gsa' gsb'" by simp
    also from eq_on_trans[OF ex_mod_limit[OF EXA(2), THEN eq_on_sym] E1]
    have "gs_eq_on (- write_globals a2) gsa' gsb'" by simp
    finally (eq_on_join) have "gs_eq_on UNIV gsa' gsb'" by simp
    thus "gsa' = gsb'" 
      apply (cases gsa', cases gsb')
      apply simp
      done
  qed

  lemma ex_pres_en:
    assumes EX: "la_ex' (ls1,gs) a1 = (ls1',gs')"
    assumes DJ: "write_globals a1 ∩ read_globals a2 = {}"
    shows "la_en' (ls2,gs') a2 = la_en' (ls2,gs) a2"
    using en_dep_read[OF ex_mod_limit[OF EX], of a2] DJ by auto



end