Theory Simulation

section ‹Simulation›
theory Simulation
imports Automata
begin

  lemma finite_ImageI:
    assumes "finite A"  
    assumes "⋀a. a∈A ⟹ finite (R``{a})"
    shows "finite (R``A)"
  proof -
    note [[simproc add: finite_Collect]]
    have "R``A = ⋃{R``{a} | a. a:A}"
      by auto
    also have "finite (⋃{R``{a} | a. a:A})"
      apply (rule finite_Union)
      apply (simp add: assms)
      apply (clarsimp simp: assms)
      done
    finally show ?thesis .
  qed


  section ‹Simulation›


  subsection ‹Functional Relations›

  definition "the_br_α R ≡ λ x. SOME y. (x, y) ∈ R"
  abbreviation (input) "the_br_invar R ≡ λ x. x ∈ Domain R"

  lemma the_br[simp]: 
    assumes "single_valued R"  
    shows "br (the_br_α R) (the_br_invar R) = R"
    unfolding build_rel_def the_br_α_def
    apply auto
    apply (metis someI_ex)
    apply (metis assms someI_ex single_valuedD)
    done

  lemma the_br_br[simp]: 
    "I x ⟹ the_br_α (br α I) x = α x"
    "the_br_invar (br α I) = I"
    unfolding the_br_α_def build_rel_def[abs_def]
    by auto

  subsection ‹Relation between Runs›

  definition run_rel :: "('a × 'b) set ⇒ ('a word × 'b word) set" where
    "run_rel R ≡ {(ra, rb). ∀ i. (ra i, rb i) ∈ R}"

  lemma run_rel_converse[simp]: "(ra, rb) ∈ run_rel (R¯) ⟷ (rb, ra) ∈ run_rel R"  
    unfolding run_rel_def by auto

  lemma run_rel_single_valued: "single_valued R 
    ⟹ (ra, rb) ∈ run_rel R ⟷ ((∀i. the_br_invar R (ra i)) ∧ rb = the_br_α R o ra)"
    unfolding run_rel_def the_br_α_def
    apply (auto intro!: ext)
    apply (metis single_valuedD someI_ex)
    apply (metis DomainE someI_ex)
    done

  subsection ‹Simulation›
  locale simulation =
    a: graph A +
    b: graph B
    for R :: "('a × 'b) set"
    and A :: "('a, _) graph_rec_scheme"
    and B :: "('b, _) graph_rec_scheme"
    +
    assumes nodes_sim: "a ∈ a.V ⟹ (a, b) ∈ R ⟹ b ∈ b.V"
    assumes init_sim: "a0 ∈ a.V0 ⟹ ∃ b0. b0 ∈ b.V0 ∧ (a0, b0) ∈ R"
    assumes step_sim: "(a, a') ∈ a.E ⟹ (a, b) ∈ R ⟹ ∃ b'. (b, b') ∈ b.E ∧ (a', b') ∈ R"
  begin

    lemma simulation_this: "simulation R A B" by unfold_locales

    lemma run_sim: 
      assumes arun: "a.is_run ra"
      obtains rb where "b.is_run rb" "(ra, rb) ∈ run_rel R"
    proof -
      from arun have ainit: "ra 0 ∈ a.V0" 
        and astep: "∀i. (ra i, ra (Suc i)) ∈ a.E"
        using a.run_V0 a.run_ipath ipathD by blast+
      from init_sim obtain rb0 where rel0: "(ra 0, rb0) ∈ R" and binit: "rb0 ∈ b.V0"
        by (auto intro: ainit)
  
      define rb
        where "rb = rec_nat rb0 (λi rbi. SOME rbsi. (rbi, rbsi) ∈ b.E ∧ (ra (Suc i), rbsi) ∈ R)"
      
      have [simp]: 
        "rb 0 = rb0" 
        "⋀i. rb (Suc i) = (SOME rbsi. (rb i, rbsi) ∈ b.E ∧ (ra (Suc i), rbsi) ∈ R)"
        unfolding rb_def by auto
  
      {
        fix i
        have "(rb i, rb (Suc i)) ∈ b.E ∧ (ra (Suc i), rb (Suc i)) ∈ R"
        proof (induction i)
          case 0
          from step_sim astep rel0 obtain rb1 where "(rb 0, rb1) ∈ b.E" and "(ra 1, rb1) ∈ R"
            by fastforce
          thus ?case by (auto intro!: someI)
        next
          case (Suc i)
          with step_sim astep obtain rbss where "(rb (Suc i), rbss) ∈ b.E" and
            "(ra (Suc (Suc i)), rbss) ∈ R"
            by fastforce
          thus ?case by (auto intro!: someI)
        qed
      } note aux=this
      
      from aux binit have "b.is_run rb"
        unfolding b.is_run_def ipath_def by simp
      moreover from aux rel0 have "(ra, rb) ∈ run_rel R"
        unfolding run_rel_def
        apply safe
        apply (case_tac i)
        by auto
      ultimately show ?thesis by rule
    qed

    lemma stuck_sim: 
      assumes "(a, b) ∈ R"
      assumes "b ∉ Domain b.E"
      shows "a ∉ Domain a.E"
      using assms
      by (auto dest: step_sim)

    lemma run_Domain: "a.is_run r ⟹ r i ∈ Domain R"
      by (erule run_sim) (auto simp: run_rel_def)

    lemma br_run_sim:
      assumes "R = br α I"
      assumes "a.is_run r"
      shows "b.is_run (α o r)"
      using assms
      apply -
      apply (erule run_sim)
      apply (auto simp: run_rel_def build_rel_def a.is_run_def b.is_run_def ipath_def)
      done

    lemma is_reachable_sim: "a ∈ a.E⇧* `` a.V0 ⟹ ∃ b. (a, b) ∈ R ∧ b ∈ b.E⇧* `` b.V0"
      apply safe
      apply (erule rtrancl_induct)
      apply (metis ImageI init_sim rtrancl.rtrancl_refl)
      apply (metis rtrancl_image_advance step_sim)
      done

    lemma reachable_sim: "a.E⇧* `` a.V0 ⊆ R¯ `` b.E⇧* `` b.V0"
      using is_reachable_sim by blast

    lemma reachable_finite_sim:
      assumes "finite (b.E⇧* `` b.V0)"
      assumes "⋀b. b ∈ b.E⇧* `` b.V0 ⟹ finite (R¯ `` {b})"
      shows "finite (a.E⇧* `` a.V0)"
      apply (rule finite_subset[OF reachable_sim])
      apply (rule finite_ImageI)
      apply fact+
      done

  end  

  lemma simulation_trans[trans]:
    assumes "simulation R1 A B"
    assumes "simulation R2 B C"
    shows "simulation (R1 O R2) A C"
  proof -
    interpret s1: simulation R1 A B by fact
    interpret s2: simulation R2 B C by fact
    show ?thesis
      apply unfold_locales
      using s1.nodes_sim s2.nodes_sim apply blast
      using s1.init_sim s2.init_sim apply blast
      using s1.step_sim s2.step_sim apply blast
      done
  qed

  lemma (in graph) simulation_refl[simp]: "simulation Id G G" by unfold_locales auto

  locale lsimulation = 
    a: sa A +
    b: sa B +
    simulation R A B
    for R :: "('a × 'b) set"
    and A :: "('a, 'l, _) sa_rec_scheme"
    and B :: "('b, 'l, _) sa_rec_scheme"
    +
    assumes labeling_consistent: "(a, b) ∈ R ⟹ a.L a = b.L b"
  begin

    lemma lsimulation_this: "lsimulation R A B" by unfold_locales

    lemma run_rel_consistent: "(ra, rb) ∈ run_rel R ⟹ a.L o ra = b.L o rb"
      using labeling_consistent unfolding run_rel_def
      by auto

    lemma accept_sim: "a.accept w ⟹ b.accept w"
      unfolding a.accept_def b.accept_def
      apply clarsimp
      apply (erule run_sim)
      apply (auto simp: run_rel_consistent)
      done

  end

  lemma lsimulation_trans[trans]: 
    assumes "lsimulation R1 A B"
    assumes "lsimulation R2 B C"
    shows "lsimulation (R1 O R2) A C"
  proof -
    interpret s1: lsimulation R1 A B by fact
    interpret s2: lsimulation R2 B C by fact
    interpret simulation "R1 O R2" A C
      using simulation_trans s1.simulation_this s2.simulation_this by this
    show ?thesis
      apply unfold_locales
      using s1.labeling_consistent s2.labeling_consistent 
      by auto
  qed

  lemma (in sa) lsimulation_refl[simp]: "lsimulation Id G G" by unfold_locales auto


  subsection ‹Bisimulation›

  locale bisimulation = 
    a: graph A +
    b: graph B +
    s1: simulation "R" A B +
    s2: simulation "R¯" B A
    for R :: "('a × 'b) set"
    and A :: "('a, _) graph_rec_scheme"
    and B :: "('b, _) graph_rec_scheme"
  begin

    lemma bisimulation_this: "bisimulation R A B" by unfold_locales

    lemma converse: "bisimulation (R¯) B A"
    proof -
      interpret simulation "(R¯)¯" A B by simp unfold_locales
      show ?thesis by unfold_locales
    qed

    lemma br_run_conv:
      assumes "R = br α I"
      shows "b.is_run rb ⟷ (∃ra. rb=α o ra ∧ a.is_run ra)"
      using assms
      apply safe
      apply (erule s2.run_sim, auto 
        intro!: ext
        simp: run_rel_def build_rel_def) []
      apply (erule s1.br_run_sim, assumption)
      done

    lemma bri_run_conv:
      assumes "R = (br γ I)¯"
      shows "a.is_run ra ⟷ (∃rb. ra=γ o rb ∧ b.is_run rb)"
      using assms
      apply safe
      apply (erule s1.run_sim, auto simp: run_rel_def build_rel_def intro!: ext) []

      apply (erule s2.run_sim, auto simp: run_rel_def build_rel_def)
      by (metis (no_types, opaque_lifting) fun_comp_eq_conv)
  
    lemma inj_map_run_eq:
      assumes "inj α"
      assumes E: "α o r1 = α o r2"
      shows "r1 = r2"
    proof (rule ext)
      fix i
      from E have "α (r1 i) = α (r2 i)"
        by (simp add: comp_def) metis
      with ‹inj α› show "r1 i = r2 i" 
        by (auto dest: injD)
    qed

    lemma br_inj_run_conv:
      assumes INJ: "inj α"
      assumes [simp]: "R = br α I"
      shows "b.is_run (α o ra) ⟷ a.is_run ra"
      apply (subst br_run_conv[OF assms(2)])
      apply (auto dest: inj_map_run_eq[OF INJ])
      done

    lemma single_valued_run_conv:
      assumes "single_valued R"
      shows "b.is_run rb 
        ⟷ (∃ra. rb=the_br_α R o ra ∧ a.is_run ra)"
      using assms
      apply safe
      apply (erule s2.run_sim)
      apply (auto simp add: run_rel_single_valued)
      apply (erule s1.run_sim)
      apply (auto simp add: run_rel_single_valued)
      done

    lemma stuck_bisim: 
      assumes A: "(a, b) ∈ R"
      shows "a ∈ Domain a.E ⟷ b ∈ Domain b.E"
      using s1.stuck_sim[OF A]
      using s2.stuck_sim[OF A[THEN converseI[of _ _ R]]]
      by blast

  end

  lemma bisimulation_trans[trans]:
    assumes "bisimulation R1 A B" 
    assumes "bisimulation R2 B C"
    shows "bisimulation (R1 O R2) A C"
  proof -
    interpret s1: bisimulation R1 A B by fact
    interpret s2: bisimulation R2 B C by fact
    interpret t1: simulation "(R1 O R2)" A C
      using simulation_trans s1.s1.simulation_this s2.s1.simulation_this by this
    interpret t2: simulation "(R1 O R2)¯" C A
      using simulation_trans s2.s2.simulation_this s1.s2.simulation_this
      unfolding converse_relcomp
      by this
    show ?thesis by unfold_locales
  qed

  lemma (in graph) bisimulation_refl[simp]: "bisimulation Id G G" by unfold_locales auto

  locale lbisimulation = 
    a: sa A +
    b: sa B +
    s1: lsimulation "R" A B +
    s2: lsimulation "R¯" B A +
    bisimulation R A B
    for R :: "('a × 'b) set"
    and A :: "('a, 'l, _) sa_rec_scheme"
    and B :: "('b, 'l, _) sa_rec_scheme"
  begin

    lemma lbisimulation_this: "lbisimulation R A B" by unfold_locales

    lemma accept_bisim: "a.accept = b.accept"
      apply (rule ext)
      using s1.accept_sim s2.accept_sim by blast

  end

  lemma lbisimulation_trans[trans]:
    assumes "lbisimulation R1 A B" 
    assumes "lbisimulation R2 B C"
    shows "lbisimulation (R1 O R2) A C"
  proof -
    interpret s1: lbisimulation R1 A B by fact
    interpret s2: lbisimulation R2 B C by fact

    from lsimulation_trans[OF s1.s1.lsimulation_this s2.s1.lsimulation_this]
    interpret t1: lsimulation "(R1 O R2)" A C .

    from lsimulation_trans[OF s2.s2.lsimulation_this s1.s2.lsimulation_this, folded converse_relcomp]
    interpret t2: lsimulation "(R1 O R2)¯" C A .

    show ?thesis by unfold_locales
  qed

  lemma (in sa) lbisimulation_refl[simp]: "lbisimulation Id G G" by unfold_locales auto

end