# Theory Decide_Locality

```section ‹Decide Locality of Variables›
theory Decide_Locality
imports "../RefPoint/SM_Semantics"
begin

lemma dom_init_valuation_eq_set[simp]: "dom (init_valuation l) = set l"
unfolding init_valuation_def[abs_def]
by (auto split: if_split_asm)

lemma bind_set_map: "⟦ g`m=m'; ⋀x. x∈m ⟹ f x = f' (g x) ⟧ ⟹ m⤜f = m'⤜f'"
by auto

"f `# m = a' + b' ⟷ (∃ a b. m = a + b ∧ f `# a = a' ∧ f `# b = b')"
using image_mset_union mset_map_split_orig by metis

lemma image_mset_eq_sng_conv:
"image_mset f m = {#y#} ⟷ (∃x. m={#x#} ∧ y = f x)"
by (cases m) auto

(* TODO: Move to general analysis *)
subsection ‹Variables›

text ‹Executions do not change the variables of the state›
abbreviation "ls_vars ls ≡ (dom (local_state.variables ls))"
abbreviation "lc_vars lc ≡ ls_vars (local_config.state lc)"

abbreviation "gs_vars gs ≡ (dom (global_state.variables gs))"
abbreviation "gc_vars gc ≡ gs_vars (global_config.state gc)"

lemma la_ex_pres_ls_vars[simp]:
"la_ex (ls,gs) a = Some (ls',gs') ⟹ ls_vars ls' = ls_vars ls"
by (induction a) (auto split: if_split_asm Option.bind_splits)

lemma la_ex_pres_gs_vars[simp]:
"la_ex (ls,gs) a = Some (ls',gs') ⟹ gs_vars gs' = gs_vars gs"
by (induction a) (auto split: if_split_asm Option.bind_splits)

text ‹We define a program transformation that statically decides whether
variable accesses are local or global›

fun dloc_exp :: "ident set ⇒ exp ⇒ exp" where
"dloc_exp L (e_var x) = (if x∈L then e_localvar x else e_globalvar x)"
| "dloc_exp _ (e_localvar x) = e_localvar x"
| "dloc_exp _ (e_globalvar x) = e_globalvar x"
| "dloc_exp _ (e_const c) = e_const c"
| "dloc_exp L (e_bin bop e1 e2) = e_bin bop (dloc_exp L e1) (dloc_exp L e2)"
| "dloc_exp L (e_un uop e) = e_un uop (dloc_exp L e)"

fun dloc_cmd :: "ident set ⇒ cmd ⇒ cmd" where
"dloc_cmd L (Assign c x e) =
(if x∈L then Assign_local else Assign_global) (dloc_exp L c) x (dloc_exp L e)"
| "dloc_cmd L (Assign_local c x e) = Assign_local (dloc_exp L c) x (dloc_exp L e)"
| "dloc_cmd L (Assign_global c x e) = Assign_global (dloc_exp L c) x (dloc_exp L e)"
| "dloc_cmd L (Test e) = Test (dloc_exp L e)"
| "dloc_cmd L Skip = Skip"
| "dloc_cmd L (Seq c1 c2) = Seq (dloc_cmd L c1) (dloc_cmd L c2)"
| "dloc_cmd L (Or c1 c2) = Or (dloc_cmd L c1) (dloc_cmd L c2)"
| "dloc_cmd L Break = Break"
| "dloc_cmd L Continue = Continue"
| "dloc_cmd L (Iterate c1 c2) = Iterate (dloc_cmd L c1) (dloc_cmd L c2)"
| "dloc_cmd L Invalid = Invalid"

definition dloc_proc :: "proc_decl ⇒ proc_decl" where
"dloc_proc pd ≡ proc_decl.body_update (dloc_cmd (set (proc_decl.local_vars pd))) pd"

definition dloc :: "program ⇒ program" where
"dloc ≡ program.processes_update (map dloc_proc)"

definition dloc_lc :: "local_config ⇒ local_config" where
"dloc_lc lc ≡ ⦇
local_config.command
= dloc_cmd
(lc_vars lc)
(local_config.command lc),
local_config.state = local_config.state lc⦈"

definition dloc_gc :: "global_config ⇒ global_config" where
"dloc_gc gc ≡ ⦇
global_config.processes = image_mset dloc_lc (global_config.processes gc),
global_config.state = global_config.state gc
⦈"

lemma dloc_rel_init: "dloc_gc (init_gc prog) = init_gc (dloc prog)"
unfolding dloc_gc_def init_gc_def dloc_lc_def[abs_def] init_pc_def[abs_def]
dloc_def dloc_proc_def[abs_def]
apply (auto simp: image_mset.compositionality)
apply (fo_rule fun_cong arg_cong)+
apply (auto)
done

fun dloc_a :: "ident set ⇒ action ⇒ action" where
"dloc_a L ((AAssign c x e)) = ((if x∈L then AAssign_local else AAssign_global)
(dloc_exp L c) x (dloc_exp L e))"
| "dloc_a L ((AAssign_local c x e)) = (AAssign_local (dloc_exp L c) x (dloc_exp L e))"
| "dloc_a L ((AAssign_global c x e)) = (AAssign_global (dloc_exp L c) x (dloc_exp L e))"
| "dloc_a L ((ATest e)) = (ATest (dloc_exp L e))"

fun dloc_ai :: "ident set ⇒ action+brk_ctd ⇒ action+brk_ctd" where
"dloc_ai L (Inr x) = Inr x"
| "dloc_ai L (Inl x) = Inl (dloc_a L x)"

lemma dloc_ai_conv:
"Inr b = dloc_ai L y ⟷ y=Inr b"
"Inl a = dloc_ai L y ⟷ (∃aa. y=Inl aa ∧ a=dloc_a L aa)"
apply (cases y, auto) []
apply (cases y, auto) []
done

lemma dloc_eq_skip_conv[simp]:
"Skip=dloc_cmd L c ⟷ c=Skip"
"dloc_cmd L c=Skip ⟷ c=Skip"
by ((case_tac c, auto) [])+

lemma cfg_dloc: "cfg (dloc_cmd L c) da dc' ⟷ (∃c' a. dc'=dloc_cmd L c' ∧ da=dloc_ai L a ∧ cfg c a c')"
proof (safe)
have aux1: "⋀c1 c2 c' S. Seq c1 c2 = dloc_cmd S c'
⟷ (∃c1' c2'. c'=Seq c1' c2' ∧ c1=dloc_cmd S c1' ∧ c2=dloc_cmd S c2')"
by (case_tac "(S,c')" rule: dloc_cmd.cases) auto

assume A: "cfg (dloc_cmd L c) da dc'"
thus "∃c' a. dc'=dloc_cmd L c' ∧ da=dloc_ai L a ∧ cfg c a c'"
proof (induction "dloc_cmd L c" da dc' arbitrary: c)
case Ass thus ?case by (cases c) (auto intro: cfg.intros split: if_split_asm)
next
case (Assl x e) thus ?case by (cases c) (auto intro: cfg.intros intro!: exI split: if_split_asm)
next
case (Assg x e) thus ?case by (cases c) (auto intro: cfg.intros intro!: exI split: if_split_asm)
next
case (Test e) thus ?case by (cases c) (auto intro: cfg.intros intro!: exI split: if_split_asm)
next
case (Seq1 dc2 c) thus ?case
apply (intro exI conjI)
apply (auto intro: cfg.Seq1)
done
next
case (Seq2' dc1 da dc2 c) thus ?case
apply (fastforce intro: cfg.Seq2')
done
next
case (Seq2 dc1 da dc1' dc2 c)
with aux1 obtain c1 c2 where [simp]: "c=Seq c1 c2" "dc1=dloc_cmd L c1" "dc2=dloc_cmd L c2"
by auto
from Seq2.hyps(2) obtain c1' a where
[simp]: "dc1' = dloc_cmd L c1'" "da = dloc_ai L a"
and 1: "cfg c1 a c1'"
by fastforce
from ‹dc1'≠Skip› have "c1'≠Skip" by simp
with cfg.Seq2[OF 1] show ?case by force
next
case (Iterate2' dc1 da dc2 c)
from Iterate2'.hyps(3)
obtain c1 c2 where [simp]: "c = Iterate c1 c2" "dc1 = dloc_cmd L c1" "dc2 = dloc_cmd L c2"
by (cases c) (auto split: if_split_asm)
from Iterate2'.hyps(2) obtain a where
S1: "Inl da = dloc_ai L a"
and 1: "cfg c1 a Skip"
by fastforce
then obtain aa where [simp]: "a=Inl aa" by (cases a) (auto split: if_split_asm)
note [simp] = S1
from cfg.Iterate2'[OF 1[simplified]] show ?case by force
next
case (Iterate2 dc1 da dc1' dc2)
from Iterate2.hyps(4)
obtain c1 c2 where [simp]: "c = Iterate c1 c2" "dc1 = dloc_cmd L c1" "dc2 = dloc_cmd L c2"
by (cases c) (auto split: if_split_asm)
from Iterate2.hyps(2) obtain c1' a where
S1: "dc1' = dloc_cmd L c1'" "Inl da = dloc_ai L a"
and 1: "cfg c1 a c1'"
by fastforce
then obtain aa where [simp]: "a=Inl aa" by (cases a) (auto split: if_split_asm)
note [simp] = S1
from cfg.Iterate2[OF 1[simplified]] ‹dc1' ≠ Skip› show ?case by force
next
case (IterateBrk dc1 dc1' dc2)
from IterateBrk.hyps(3)
obtain c1 c2 where [simp]: "c = Iterate c1 c2" "dc1 = dloc_cmd L c1" "dc2 = dloc_cmd L c2"
by (cases c) (auto split: if_split_asm)
from IterateBrk.hyps(2) obtain c1' a where
S1: "dc1' = dloc_cmd L c1'" and "Inr AIBreak = dloc_ai L a"
and 1: "cfg c1 a c1'"
by fastforce
hence [simp]: "a=Inr AIBreak" by (cases "(L,a)" rule: dloc_ai.cases) simp_all
note [simp] = S1
from cfg.IterateBrk[OF 1[simplified]] show ?case by force
next
case (IterateCtd dc1 dc1' dc2)
from IterateCtd.hyps(3)
obtain c1 c2 where [simp]: "c = Iterate c1 c2" "dc1 = dloc_cmd L c1" "dc2 = dloc_cmd L c2"
by (cases c) (auto split: if_split_asm)
from IterateCtd.hyps(2) obtain c1' a where
S1: "dc1' = dloc_cmd L c1'" and "Inr AIContinue = dloc_ai L a"
and 1: "cfg c1 a c1'"
by fastforce
hence [simp]: "a=Inr AIContinue" by (cases "(L,a)" rule: dloc_ai.cases) simp_all
note [simp] = S1
from cfg.IterateCtd[OF 1[simplified]] show ?case by force
next
case (Or1 dc1 da dc1' dc2) thus ?case
apply (case_tac c, simp_all split: if_split_asm)
apply (fastforce intro: cfg.intros)
done
next
case (Or2 dc2 da dc2' dc1) thus ?case
apply (case_tac c, simp_all split: if_split_asm)
apply (fastforce intro: cfg.intros)
done
apply_end (case_tac c, auto intro: cfg.intros intro!: exI split: if_split_asm) []
apply_end (case_tac c, auto intro: cfg.intros intro!: exI split: if_split_asm) []
apply_end (case_tac ca, auto intro: cfg.intros intro!: exI split: if_split_asm) []
qed
next
fix c' a
assume "cfg c a c'"
thus "cfg (dloc_cmd L c) (dloc_ai L a) (dloc_cmd L c')"
by (induction) (auto intro: cfg.intros)
qed

lemma choose_action_as_map_aux: "
(map_prod (dloc_ai (lc_vars lc)) (dloc_cmd (lc_vars lc)))`{(a, c'). cfg (command lc) a c'}
= {(a, c'). cfg (command (dloc_lc lc)) a c'}"
by (auto simp: dloc_lc_def map_prod_def image_def cfg_dloc)

lemma dloc_lc_state[simp]: "local_config.state (dloc_lc lc) = local_config.state lc"
unfolding dloc_lc_def by simp

lemma dloc_gc_state[simp]: "global_config.state (dloc_gc gc) = global_config.state gc"
unfolding dloc_gc_def by simp

lemma dloc_exp_correct[simp]:
"eval_exp (dloc_exp (ls_vars ls) e) (ls, gs) = eval_exp e (ls,gs)"
by (induction e) (auto split: option.splits)

lemma dloc_la_en_correct[simp]:
"la_en (ls, gs) (dloc_a (ls_vars ls) a) = la_en (ls, gs) a"
by (cases a) auto

lemma dloc_la_ex_correct[simp]:
"la_ex (ls,gs) (dloc_a (ls_vars ls) a) = la_ex (ls,gs) a"
by (cases a) auto

lemma dloc_rel_gstep_succ:
"li.gstep_succ (dloc_gc gc) = map_option dloc_gc ` li.gstep_succ gc"
apply (rule sym)
apply safe

apply (erule li.gstep_succE, simp_all) []
apply (force
intro: li.gstep_succ_fail_cmd li.gstep_succ_fail_en li.gstep_succ_fail_ex
simp: dloc_gc_def cfg_dloc dloc_lc_def) []

apply (force
intro: li.gstep_succ_fail_cmd li.gstep_succ_fail_en li.gstep_succ_fail_ex
simp: dloc_gc_def cfg_dloc dloc_lc_def) []

apply (force intro: li.gstep_succ_fail_en li.gstep_succ_fail_ex
simp: dloc_gc_def cfg_dloc dloc_lc_def) []
apply (force intro: li.gstep_succ_fail_en li.gstep_succ_fail_ex li.gstep_succ_succ
simp: dloc_gc_def cfg_dloc dloc_lc_def) []

apply (erule li.gstep_succE,
clarsimp_all
simp: cfg_dloc dloc_lc_def dloc_ai_conv
) []
apply (force
intro: li.gstep_succ_fail_cmd li.gstep_succ_fail_en li.gstep_succ_fail_ex
simp: dloc_gc_def cfg_dloc dloc_lc_def) []
apply (force intro: li.gstep_succ_fail_en li.gstep_succ_fail_ex
simp: dloc_gc_def cfg_dloc dloc_lc_def) []
apply (auto intro: li.gstep_succ_fail_en li.gstep_succ_fail_ex
simp: dloc_gc_def cfg_dloc dloc_lc_def) []
apply (force intro!: li.gstep_succ_succ image_eqI[rotated]
simp: dloc_gc_def cfg_dloc dloc_lc_def) []

done

lemma dloc_rel_gstep: "(map_option dloc_gc gc, dgc') ∈ li.gstep ⟷
(∃ gc'. dgc'= map_option dloc_gc gc' ∧ (gc, gc') ∈ li.gstep)"
using li.gstep_eq_conv dloc_rel_gstep_succ by auto

lemma dloc_rel_label: "li.label (map_option dloc_gc gc) = li.label gc"
apply (cases gc, simp_all)
done

interpretation dloc_sim: lbisimulation "br (map_option dloc_gc) (λ _. True)"
"li.system_automaton prog" "li.system_automaton (dloc prog)"
for prog
proof -
interpret bisim: lbisimulation "br (map_option dloc_gc) (λ _. True)"
"li.system_automaton' prog" "li.system_automaton' (dloc prog)"
apply unfold_locales
apply (auto simp: build_rel_def li.init_conv simp: dloc_rel_init dloc_rel_gstep dloc_rel_label)
done
interpret bisim: lbisimulation "br (map_option dloc_gc) (λ _. True)"
"li.system_automaton prog" "li.system_automaton (dloc prog)"
unfolding li.system_automaton_alt_def
using bisim.lstutter_extend by this
show "lbisimulation (br (map_option dloc_gc) (λ _. True))
(li.system_automaton prog) (li.system_automaton (dloc prog))"
by unfold_locales
qed

end

```