Theory SM.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


  lemma rel_option_add_simps[simp]: 
    "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 (auto simp: union_mset_add_mset_left)
    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 add: rel_mset_Zero)
      apply simp
      apply (rule rel_mset_Plus)
      apply (simp add: build_relp_def)
      .
  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