# Theory Gen_Cfg_Bisim

```theory Gen_Cfg_Bisim
imports Gen_Scheduler_Refine
begin

(* TODO: Move? *)
(* TODO: we should consistenly use relations here *)

subsection ‹Functional Relations›

definition "build_relp α I x y ≡ y=α x ∧ I x"
abbreviation "brp ≡ build_relp"

lemma brp_right_unique[simp, intro!]: "right_unique (brp α I)"
apply (rule right_uniqueI)
unfolding build_relp_def
by auto

definition "the_brp_α R ≡ (λx. SOME y. R x y)"
abbreviation (input) "the_brp_invar ≡ Domainp"

lemma the_brp[simp]:
assumes "right_unique R"
shows "brp (the_brp_α R) (the_brp_invar R) = R"
apply (rule sym)
apply (intro ext)
unfolding build_relp_def the_brp_α_def
apply auto
apply (metis assms right_uniqueD someI)
by (blast intro: someI)

lemma obtain_brp:
assumes "right_unique R"
obtains α I where "R=brp α I"
using the_brp[OF assms, THEN sym] ..

lemma the_brp_brp[simp]:
"I x ⟹ the_brp_α (brp α I) x = α x"
"the_brp_invar (brp α I) = I"
unfolding the_brp_α_def build_relp_def[abs_def]
by (auto)

lemma brp_comp[simp]: "brp α1 I1 OO brp α2 I2 = brp (α2 o α1) (λx. I1 x ∧ I2 (α1 x))"
unfolding build_relp_def[abs_def] by auto

lemma rel_of_pred_brp[simp]: "rel_of_pred (brp α invar) = br α invar"
unfolding build_relp_def[abs_def] build_rel_def by auto

"rel_option R None c ⟷ c=None"
"rel_option R d None ⟷ d=None"
apply (cases c, auto) []
apply (cases d, auto) []
done

lemma rel_option_Some_conv:
"rel_option R (Some v) d ⟷ (∃w. R v w ∧ d = Some w)"
"rel_option R c (Some w) ⟷ (∃v. R v w ∧ c = Some v)"
apply (cases d, auto)
apply (cases c, auto)
done

lemma rel_mset_plus_conv:
"rel_mset R ({#a#}+m') n ⟷ (∃b n'. n={#b#}+n' ∧ R a b ∧ rel_mset R m' n')"
"rel_mset R m ({#b#}+n') ⟷ (∃a m'. m={#a#}+m' ∧ R a b ∧ rel_mset R m' n')"
apply (metis msed_rel_invL)
apply (metis rel_mset_Plus)
apply (metis msed_rel_invR)
apply (metis rel_mset_Plus)
done

lemma rel_mset_brp:
"rel_mset (brp α I) = brp (image_mset α) (λm. ∀x. x:#m ⟶ I x)"
proof (intro ext iffI)
fix m m'
assume "rel_mset (brp α I) m m'"
thus "brp (image_mset α) (λm. ∀x. x:#m ⟶ I x) m m'"
apply (induction "(brp α I)" _ _ rule: rel_mset_induct)
apply (auto simp: build_relp_def)
done
next
fix m m'
assume "brp (image_mset α) (λm. ∀x. x ∈# m ⟶ I x) m m'"
hence 1: "m' = image_mset α m"
and "∀x. x ∈# m ⟶ I x" by (auto simp: build_relp_def)
from this(2) show "rel_mset (brp α I) m m'"
unfolding 1
apply (induction m)
apply simp
apply (rule rel_mset_Plus)
.
qed

locale Gen_Cfg_Bisim_Pre =
s1: Gen_Scheduler' cstep1 en ex
+ s2: Gen_Scheduler' cstep2 en ex
for rel_c :: "'c ⇒ 'd ⇒ bool"
and cstep1 :: "'c ⇒ 'a ⇒ 'c ⇒ bool"
and cstep2 :: "'d ⇒ 'a ⇒ 'd ⇒ bool"
and en
and ex :: "('ls×'gs) ⇒ 'a ⇒ ('ls×'gs)" +
assumes csim1: "⟦cstep1 c a c'; rel_c c d ⟧ ⟹ ∃d'. rel_c c' d' ∧ cstep2 d a d'"
assumes csim2: "⟦cstep2 d a d'; rel_c c d ⟧ ⟹ ∃c'. rel_c c' d' ∧ cstep1 c a c'"
begin

(* TODO: we should consistenly use relations here *)
definition rel_lc :: "('c,'ls) local_config ⇒ ('d,'ls) local_config ⇒ bool"
where "rel_lc lc ld ≡
rel_c (local_config.command lc) (local_config.command ld)
∧ local_config.state lc = local_config.state ld"

definition rel_gc :: "('c,'ls,'gs)global_config ⇒ ('d,'ls,'gs)global_config ⇒ bool"
where "rel_gc gc gd ≡
rel_mset rel_lc (global_config.processes gc) (global_config.processes gd)
∧ global_config.state gc = global_config.state gd"

lemma gstep_sim1: "⟦(c, c') ∈ s1.gstep; rel_gc c d⟧ ⟹ ∃d'. rel_gc c' d' ∧ (d, d') ∈ s2.gstep"
apply (cases c, simp_all)
apply (erule s1.gstep_succE)
apply (auto
simp: rel_option_Some_conv rel_gc_def rel_lc_def
simp: rel_mset_plus_conv
)
apply (drule (1) csim1, clarsimp)
apply (drule (3) s2.gstep_succI, force)
done

lemma gstep_sim2: "⟦(d, d') ∈ s2.gstep; rel_gc c d⟧ ⟹ ∃c'. rel_gc c' d' ∧ (c, c') ∈ s1.gstep"
apply (cases d, simp_all)
apply (erule s2.gstep_succE)
apply (auto
simp: rel_option_Some_conv rel_gc_def rel_lc_def
simp: rel_mset_plus_conv
)
apply (drule (1) csim2, clarsimp)
apply (drule (1) s1.gstep_succI, simp_all, force)
done

lemma left_unique_rel_lcI:
assumes "left_unique rel_c"
shows "left_unique rel_lc"
proof (rule left_uniqueI)
fix lc1 lc2 lc3
assume "rel_lc lc1 lc2" "rel_lc lc3 lc2"
thus "lc1=lc3"
apply (cases lc1, cases lc2, cases lc3, simp_all)
apply (auto simp: rel_lc_def left_uniqueD[OF assms])
done
qed

lemma right_unique_rel_lcI:
assumes "right_unique rel_c"
shows "right_unique rel_lc"
proof (rule right_uniqueI)
fix lc1 lc2 lc3
assume "rel_lc lc2 lc1" "rel_lc lc2 lc3"
thus "lc1=lc3"
apply (cases lc1, cases lc2, cases lc3, simp_all)
apply (auto simp: rel_lc_def right_uniqueD[OF assms])
done
qed

lemma bi_unique_rel_lcI:
assumes "bi_unique rel_c"
shows "bi_unique rel_lc"
using assms
by (auto simp: bi_unique_alt_def right_unique_rel_lcI left_unique_rel_lcI)

lemma left_unique_rel_gcI:
assumes "left_unique rel_c"
shows "left_unique rel_gc"
proof (rule left_uniqueI)
note A = left_unique_rel_lcI[OF assms, THEN multiset.left_unique_rel]

fix gc1 gc2 gc3
assume "rel_gc gc1 gc2" "rel_gc gc3 gc2"
thus "gc1=gc3"
apply (cases gc1, cases gc2, cases gc3, simp_all)
apply (auto simp: rel_gc_def left_uniqueD[OF A])
done
qed

lemma right_unique_rel_gcI:
assumes "right_unique rel_c"
shows "right_unique rel_gc"
proof (rule right_uniqueI)
note A = right_unique_rel_lcI[OF assms, THEN multiset.right_unique_rel]

fix gc1 gc2 gc3
assume "rel_gc gc1 gc2" "rel_gc gc1 gc3"
thus "gc2=gc3"
apply (cases gc1, cases gc2, cases gc3, simp_all)
apply (auto simp: rel_gc_def right_uniqueD[OF A])
done
qed

lemma bi_unique_rel_gcI:
assumes "bi_unique rel_c"
shows "bi_unique rel_gc"
using assms
by (auto simp: bi_unique_alt_def right_unique_rel_gcI left_unique_rel_gcI)

end

locale Gen_Cfg_LBisim =
Gen_Cfg_Bisim_Pre rel_c cstep1 cstep2 en ex
for rel_c :: "'c ⇒ 'd ⇒ bool"
and cstep1 :: "'c ⇒ 'a ⇒ 'c ⇒ bool"
and init1 :: "('c,'ls,'gs)global_config set"
and label1 :: "('c,'ls,'gs)global_config ⇒ 'l"
and cstep2 :: "'d ⇒ 'a ⇒ 'd ⇒ bool"
and init2 :: "('d,'ls,'gs)global_config set"
and label2 :: "('d,'ls,'gs)global_config ⇒ 'l"
and en
and ex :: "('ls×'gs) ⇒ 'a ⇒ ('ls×'gs)" +
assumes init_sim1: "⋀a0. a0 ∈ init1 ⟹ ∃b0. b0 ∈ init2 ∧ rel_gc a0 b0"
assumes init_sim2: "⋀b0. b0 ∈ init2 ⟹ ∃a0. a0 ∈ init1 ∧ rel_gc a0 b0"
assumes labeling_consistent: "⋀a b. rel_gc a b ⟹ label1 a = label2 b"
begin

sublocale s1: Gen_Scheduler'_linit cstep1 en ex init1 label1 by this
sublocale s2: Gen_Scheduler'_linit cstep2 en ex init2 label2 by this

sublocale lbisimulation "rel_of_pred rel_gc" s1.system_automaton s2.system_automaton
proof -
interpret bisim:
lbisimulation "rel_of_pred rel_gc" s1.system_automaton' s2.system_automaton'
apply unfold_locales
apply simp_all
using init_sim1 apply force
using gstep_sim1 apply force
using labeling_consistent apply force
using init_sim2 apply force
using gstep_sim2 apply force
using labeling_consistent apply force
done
interpret bisim:
lbisimulation "rel_of_pred rel_gc" s1.system_automaton s2.system_automaton
unfolding s1.system_automaton_alt_def s2.system_automaton_alt_def
using bisim.lstutter_extend by this
show "lbisimulation (rel_of_pred rel_gc) s1.system_automaton s2.system_automaton"
by unfold_locales
qed

end

end

```