Theory VeriComp.Simulation

section ‹Simulations Between Dynamic Executions›

theory Simulation
  imports
    Semantics
    Inf
    Well_founded
    Lifting_Simulation_To_Bisimulation
begin

subsection ‹Backward simulation›

locale backward_simulation =
  L1: semantics step1 final1 +
  L2: semantics step2 final2 +
  well_founded "(⊏)"
  for
    step1 :: "'state1 ⇒ 'state1 ⇒ bool" and
    step2 :: "'state2 ⇒ 'state2 ⇒ bool" and
    final1 :: "'state1 ⇒ bool" and
    final2 :: "'state2 ⇒ bool" and
    order :: "'index ⇒ 'index ⇒ bool" (infix "⊏" 70) +
  fixes
    match :: "'index ⇒ 'state1 ⇒ 'state2 ⇒ bool"
  assumes
    match_final:
      "match i s1 s2 ⟹ final2 s2 ⟹ final1 s1" and
    simulation:
      "match i s1 s2 ⟹ step2 s2 s2' ⟹
        (∃i' s1'. step1⇧+⇧+ s1 s1' ∧ match i' s1' s2') ∨ (∃i'. match i' s1 s2' ∧ i' ⊏ i)"
begin

text ‹
A simulation is defined between two @{locale semantics} L1 and L2.
A @{term match} predicate expresses that two states from L1 and L2 are equivalent.
The @{term match} predicate is also parameterized with an ordering used to avoid stuttering.
The only two assumptions of a backward simulation are that a final state in L2 will also be a final in L1,and that a step in L2 will either represent a non-empty sequence of steps in L1 or will result in an equivalent state.
Stuttering is ruled out by the requirement that the index on the @{term match} predicate decreases with respect to the well-founded @{term order} ordering.
›

lemma lift_simulation_plus:
  "step2⇧+⇧+ s2 s2' ⟹ match i1 s1 s2 ⟹
    (∃i2 s1'. step1⇧+⇧+ s1 s1' ∧ match i2 s1' s2') ∨
    (∃i2. match i2 s1 s2' ∧ order⇧+⇧+ i2 i1)"
  thm tranclp_induct
proof(induction s2' arbitrary: i1 s1 rule: tranclp_induct)
  case (base s2')
  from simulation[OF base.prems(1) base.hyps(1)] show ?case
    by auto
next
  case (step s2' s2'')
  show ?case
    using step.IH[OF ‹match i1 s1 s2›]
  proof
    assume "∃i2 s1'. step1⇧+⇧+ s1 s1' ∧ match i2 s1' s2'"
    then obtain i2 s1' where "step1⇧+⇧+ s1 s1'" and "match i2 s1' s2'" by auto
    from simulation[OF ‹match i2 s1' s2'› ‹step2 s2' s2''›] show ?thesis
    proof
      assume "∃i3 s1''. step1⇧+⇧+ s1' s1'' ∧ match i3 s1'' s2''"
      then obtain i3 s1'' where "step1⇧+⇧+ s1' s1''" and "match i3 s1'' s2''" by auto
      then show ?thesis
        using tranclp_trans[OF ‹step1⇧+⇧+ s1 s1'›] by auto
    next
      assume "∃i3. match i3 s1' s2'' ∧ i3 ⊏ i2"
      then obtain i3 where "match i3 s1' s2''" and "i3 ⊏ i2" by auto
      then show ?thesis
        using ‹step1⇧+⇧+ s1 s1'› by auto
    qed
  next
    assume "∃i2. match i2 s1 s2' ∧ (⊏)⇧+⇧+ i2 i1"
    then obtain i3 where "match i3 s1 s2'" and "(⊏)⇧+⇧+ i3 i1" by auto
    then show ?thesis
      using simulation[OF ‹match i3 s1 s2'› ‹step2 s2' s2''›] by auto
  qed
qed

lemma lift_simulation_eval:
  "L2.eval s2 s2' ⟹ match i1 s1 s2 ⟹ ∃i2 s1'. L1.eval s1 s1' ∧ match i2 s1' s2'"
proof(induction s2 arbitrary: i1 s1 rule: converse_rtranclp_induct)
  case (base s2)
  thus ?case by auto
next
  case (step s2 s2'')
  from simulation[OF ‹match i1 s1 s2› ‹step2 s2 s2''›] show ?case
  proof
    assume "∃i2 s1'. step1⇧+⇧+ s1 s1' ∧ match i2 s1' s2''"
    thus ?thesis
      by (meson rtranclp_trans step.IH tranclp_into_rtranclp)
  next
    assume "∃i2. match i2 s1 s2'' ∧ i2 ⊏ i1"
    thus ?thesis
      by (auto intro: step.IH)
  qed
qed

lemma match_inf:
  assumes
    "match i s1 s2" and
    "inf step2 s2"
  shows "inf step1 s1"
proof -
  from assms have "inf_wf step1 order i s1"
  proof (coinduction arbitrary: i s1 s2)
    case inf_wf
    obtain s2' where "step2 s2 s2'" and "inf step2 s2'"
      using inf_wf(2) by (auto elim: inf.cases)
    from simulation[OF ‹match i s1 s2› ‹step2 s2 s2'›] show ?case
      using ‹inf step2 s2'› by auto
  qed
  thus ?thesis using inf_wf_to_inf
    by (auto intro: inf_wf_to_inf well_founded_axioms)
qed

subsubsection ‹Preservation of behaviour›

text ‹
The main correctness theorem states that, for any two matching programs, any not wrong behaviour of the later is also a behaviour of the former.
In other words, if the compiled program does not crash, then its behaviour, whether it terminates or not, is a also a valid behaviour of the source program.
›

lemma simulation_behaviour :
  "L2.state_behaves s⇩2 b⇩2 ⟹ ¬is_wrong b⇩2 ⟹ match i s⇩1 s⇩2 ⟹
    ∃b⇩1 i'. L1.state_behaves s⇩1 b⇩1 ∧ rel_behaviour (match i') b⇩1 b⇩2"
proof(induction rule: L2.state_behaves.cases)
  case (state_terminates s2 s2')
  then obtain i' s1' where "L1.eval s⇩1 s1'" and "match i' s1' s2'"
    using lift_simulation_eval by blast
  hence "final1 s1'"
    by (auto intro: state_terminates.hyps match_final)
  hence "L1.state_behaves s⇩1 (Terminates s1')"
    using L1.final_finished
    by (simp add: L1.state_terminates ‹L1.eval s⇩1 s1'›)
  moreover have "rel_behaviour (match i') (Terminates s1') b⇩2"
    by (simp add: ‹match i' s1' s2'› state_terminates.hyps)
  ultimately show ?case by blast
next
  case (state_diverges s2)
  then show ?case
    using match_inf L1.state_diverges by fastforce
next
  case (state_goes_wrong s2 s2')
  then show ?case using ‹¬is_wrong b⇩2› by simp
qed

end

subsection ‹Forward simulation›

locale forward_simulation =
  L1: semantics step1 final1 +
  L2: semantics step2 final2 +
  well_founded "(⊏)"
  for
    step1 :: "'state1 ⇒ 'state1 ⇒ bool" and
    step2 :: "'state2 ⇒ 'state2 ⇒ bool" and
    final1 :: "'state1 ⇒ bool" and
    final2 :: "'state2 ⇒ bool" and
    order :: "'index ⇒ 'index ⇒ bool" (infix "⊏" 70) +
  fixes
    match :: "'index ⇒ 'state1 ⇒ 'state2 ⇒ bool"
  assumes
    match_final:
      "match i s1 s2 ⟹ final1 s1 ⟹ final2 s2" and
    simulation:
      "match i s1 s2 ⟹ step1 s1 s1' ⟹
        (∃i' s2'. step2⇧+⇧+ s2 s2' ∧ match i' s1' s2') ∨ (∃i'. match i' s1' s2 ∧ i' ⊏ i)"
begin

lemma lift_simulation_plus:
  "step1⇧+⇧+ s1 s1' ⟹ match i s1 s2 ⟹
    (∃i' s2'. step2⇧+⇧+ s2 s2' ∧ match i' s1' s2') ∨
    (∃i'. match i' s1' s2 ∧ order⇧+⇧+ i' i)"
proof (induction s1' arbitrary: i s2 rule: tranclp_induct)
  case (base s1')
  with simulation[OF base.prems(1) base.hyps(1)] show ?case
    by auto
next
  case (step s1' s1'')
  show ?case
    using step.IH[OF ‹match i s1 s2›]
  proof (elim disjE exE conjE)
    fix i' s2'
    assume "step2⇧+⇧+ s2 s2'" and "match i' s1' s2'"

    have "(∃i' s2'a. step2⇧+⇧+ s2' s2'a ∧ match i' s1'' s2'a) ∨ (∃i'a. match i'a s1'' s2' ∧ i'a ⊏ i')"
      using simulation[OF ‹match i' s1' s2'› ‹step1 s1' s1''›] .
    thus ?thesis
    proof (elim disjE exE conjE)
      fix i'' s2''
      assume "step2⇧+⇧+ s2' s2''" and "match i'' s1'' s2''"
      thus ?thesis
        using tranclp_trans[OF ‹step2⇧+⇧+ s2 s2'›] by auto
    next
      fix i''
      assume "match i'' s1'' s2'" and "i'' ⊏ i'"
      thus ?thesis
        using ‹step2⇧+⇧+ s2 s2'› by auto
    qed
  next
    fix i'
    assume "match i' s1' s2" and "(⊏)⇧+⇧+ i' i"
    then show ?thesis
      using simulation[OF ‹match i' s1' s2› ‹step1 s1' s1''›] by auto
  qed
qed

lemma lift_simulation_eval:
  "L1.eval s1 s1' ⟹ match i s1 s2 ⟹ ∃i' s2'. L2.eval s2 s2' ∧ match i' s1' s2'"
proof(induction s1 arbitrary: i s2 rule: converse_rtranclp_induct)
  case (base s2)
  thus ?case by auto
next
  case (step s1 s1'')
  show ?case
    using simulation[OF ‹match i s1 s2› ‹step1 s1 s1''›]
  proof (elim disjE exE conjE)
    fix i' s2'
    assume "step2⇧+⇧+ s2 s2'" and "match i' s1'' s2'"
    thus ?thesis
      by (auto intro: rtranclp_trans dest!: tranclp_into_rtranclp step.IH)
  next
    fix i'
    assume "match i' s1'' s2" and "i' ⊏ i"
    thus ?thesis
      by (auto intro: step.IH)
  qed
qed

lemma match_inf:
  assumes "match i s1 s2" and "inf step1 s1"
  shows "inf step2 s2"
proof -
  from assms have "inf_wf step2 order i s2"
  proof (coinduction arbitrary: i s1 s2)
    case inf_wf
    obtain s1' where step_s1: "step1 s1 s1'" and inf_s1': "inf step1 s1'"
      using inf_wf(2) by (auto elim: inf.cases)
    from simulation[OF ‹match i s1 s2› step_s1] show ?case
      using inf_s1' by auto
  qed
  thus ?thesis using inf_wf_to_inf
    by (auto intro: inf_wf_to_inf well_founded_axioms)
qed


subsubsection ‹Preservation of behaviour›

lemma simulation_behaviour :
  "L1.state_behaves s1 b1 ⟹ ¬ is_wrong b1 ⟹ match i s1 s2 ⟹
    ∃b2 i'. L2.state_behaves s2 b2 ∧ rel_behaviour (match i') b1 b2"
proof(induction rule: L1.state_behaves.cases)
  case (state_terminates s1 s1')
  then obtain i' s2' where steps_s2: "L2.eval s2 s2'" and match_s1'_s2': "match i' s1' s2'"
    using lift_simulation_eval by blast
  hence "final2 s2'"
    by (auto intro: state_terminates.hyps match_final)
  hence "L2.state_behaves s2 (Terminates s2')"
    using L2.final_finished L2.state_terminates[OF steps_s2]
    by simp
  moreover have "rel_behaviour (match i') b1 (Terminates s2')"
    by (simp add: ‹match i' s1' s2'› state_terminates.hyps)
  ultimately show ?case by blast
next
  case (state_diverges s2)
  then show ?case
    using match_inf[THEN L2.state_diverges] by fastforce
next
  case (state_goes_wrong s2 s2')
  then show ?case using ‹¬is_wrong b1› by simp
qed


subsubsection ‹Forward to backward›

lemma state_behaves_forward_to_backward:
  assumes
    match_s1_s2: "match i s1 s2" and
    safe_s1: "L1.safe s1" and
    behaves_s2: "L2.state_behaves s2 b2" and
    right_unique2: "right_unique step2"
  shows "∃b1 i. L1.state_behaves s1 b1 ∧ rel_behaviour (match i) b1 b2"
proof -
  obtain b1 where behaves_s1: "L1.state_behaves s1 b1"
    using L1.left_total_state_behaves
    by (auto elim: left_totalE)

  have not_wrong_b1: "¬ is_wrong b1"
    by (rule L1.safe_state_behaves_not_wrong[OF safe_s1 behaves_s1])

  obtain i' where "L2.state_behaves s2 b2" and rel_b1_B2: "rel_behaviour (match i') b1 b2"
    using simulation_behaviour[OF behaves_s1 not_wrong_b1 match_s1_s2]
    using L2.right_unique_state_behaves[OF right_unique2, THEN right_uniqueD]
    using behaves_s2
    by auto

  show ?thesis
    using behaves_s1 rel_b1_B2 by auto
qed

end

subsection ‹Bisimulation›

locale bisimulation =
  forward_simulation step1 step2 final1 final2 order match +
  backward_simulation step1 step2 final1 final2 order match
  for
    step1 :: "'state1 ⇒ 'state1 ⇒ bool" and
    step2 :: "'state2 ⇒ 'state2 ⇒ bool" and
    final1 :: "'state1 ⇒ bool" and
    final2 :: "'state2 ⇒ bool" and
    order :: "'index ⇒ 'index ⇒ bool" and
    match :: "'index ⇒ 'state1 ⇒ 'state2 ⇒ bool"

lemma obtains_bisimulation_from_forward_simulation:
  fixes
    step1 :: "'state1 ⇒ 'state1 ⇒ bool" and final1 :: "'state1 ⇒ bool" and
    step2 :: "'state2 ⇒ 'state2 ⇒ bool" and final2 :: "'state2 ⇒ bool" and
    match :: "'index ⇒ 'state1 ⇒ 'state2 ⇒ bool" and
    lt :: "'index ⇒ 'index ⇒ bool"
  assumes "right_unique step1" and "right_unique step2" and
    final1_stuck: "∀s1. final1 s1 ⟶ (∄s1'. step1 s1 s1')" and
    final2_stuck: "∀s2. final2 s2 ⟶ (∄s2'. step2 s2 s2')" and
    matching_states_agree_on_final: "∀i s1 s2. match i s1 s2 ⟶ final1 s1 ⟷ final2 s2" and
    matching_states_are_safe:
      "∀i s1 s2. match i s1 s2 ⟶ safe_state step1 final1 s1 ∧ safe_state step2 final2 s2" and
    "wfP lt" and
    fsim: "∀i s1 s2 s1'. match i s1 s2 ⟶ step1 s1 s1' ⟶
      (∃i' s2'. step2⇧+⇧+ s2 s2' ∧ match i' s1' s2') ∨ (∃i'. match i' s1' s2 ∧ lt i' i)"
  obtains
    MATCH :: "nat × nat ⇒ 'state1 ⇒ 'state2 ⇒ bool" and
    ORDER :: "nat × nat ⇒ nat × nat ⇒ bool"
  where
    "bisimulation step1 step2 final1 final2 ORDER MATCH"
proof -
  have "simulation step1 step2 match lt"
    using fsim unfolding simulation_def by metis

  obtain
    MATCH :: "nat × nat ⇒ 'state1 ⇒ 'state2 ⇒ bool" and
    ORDER :: "nat × nat ⇒ nat × nat ⇒ bool"
  where
    "(⋀i s1 s2. match i s1 s2 ⟹ ∃j. MATCH j s1 s2)" and
    "(⋀j s1 s2. MATCH j s1 s2 ⟹ final1 s1 = final2 s2)" and
    "(⋀j s1 s2. MATCH j s1 s2 ⟹ stuck_state step1 s1 = stuck_state step2 s2)" and
    "(⋀j s1 s2. MATCH j s1 s2 ⟹ safe_state step1 final1 s1 ∧ safe_state step2 final2 s2)" and
    "wfP ORDER" and
    fsim': "simulation step1 step2 MATCH ORDER" and
    bsim': "simulation step2 step1 (λi s2 s1. MATCH i s1 s2) ORDER"
    using lift_strong_simulation_to_bisimulation'[OF assms(1,2) final1_stuck final2_stuck
        matching_states_agree_on_final matching_states_are_safe ‹wfP lt›
        ‹simulation step1 step2 match lt›]
    by blast

  have "bisimulation step1 step2 final1 final2 ORDER MATCH"
  proof unfold_locales
    show "⋀i s1 s2. MATCH i s1 s2 ⟹ final1 s1 ⟹ final2 s2"
      using ‹⋀s2 s1 j. MATCH j s1 s2 ⟹ final1 s1 = final2 s2› by metis
  next
    show "⋀i s1 s2. MATCH i s1 s2 ⟹ final2 s2 ⟹ final1 s1"
      using ‹⋀s2 s1 j. MATCH j s1 s2 ⟹ final1 s1 = final2 s2› by metis
  next
    show "wfP ORDER"
      using ‹wfP ORDER› .
  next
    show "⋀i s1 s2 s1'. MATCH i s1 s2 ⟹ step1 s1 s1' ⟹
      (∃i' s2'. step2⇧+⇧+ s2 s2' ∧ MATCH i' s1' s2') ∨ (∃i'. MATCH i' s1' s2 ∧ ORDER i' i)"
      using fsim' unfolding simulation_def by metis
  next
    show "⋀i s1 s2 s2'. MATCH i s1 s2 ⟹ step2 s2 s2' ⟹
      (∃i' s1'. step1⇧+⇧+ s1 s1' ∧ MATCH i' s1' s2') ∨ (∃i'. MATCH i' s1 s2' ∧ ORDER i' i)"
      using bsim' unfolding simulation_def by metis
  next
    show "⋀s. final1 s ⟹ finished step1 s"
      by (simp add: final1_stuck finished_def)
  next
    show "⋀s. final2 s ⟹ finished step2 s"
      by (simp add: final2_stuck finished_def)
  qed

  thus thesis
    using that by metis
qed

corollary ex_bisimulation_from_forward_simulation:
  fixes
    step1 :: "'state1 ⇒ 'state1 ⇒ bool" and final1 :: "'state1 ⇒ bool" and
    step2 :: "'state2 ⇒ 'state2 ⇒ bool" and final2 :: "'state2 ⇒ bool" and
    match :: "'index ⇒ 'state1 ⇒ 'state2 ⇒ bool" and
    lt :: "'index ⇒ 'index ⇒ bool"
  assumes "right_unique step1" and "right_unique step2" and
    final1_stuck: "∀s1. final1 s1 ⟶ (∄s1'. step1 s1 s1')" and
    final2_stuck: "∀s2. final2 s2 ⟶ (∄s2'. step2 s2 s2')" and
    matching_states_agree_on_final: "∀i s1 s2. match i s1 s2 ⟶ final1 s1 ⟷ final2 s2" and
    matching_states_are_safe:
      "∀i s1 s2. match i s1 s2 ⟶ safe_state step1 final1 s1 ∧ safe_state step2 final2 s2" and
    "wfP lt" and
    fsim: "∀i s1 s2 s1'. match i s1 s2 ⟶ step1 s1 s1' ⟶
      (∃i' s2'. step2⇧+⇧+ s2 s2' ∧ match i' s1' s2') ∨ (∃i'. match i' s1' s2 ∧ lt i' i)"
  shows "∃(MATCH :: nat × nat ⇒ 'state1 ⇒ 'state2 ⇒ bool)
    (ORDER :: nat × nat ⇒ nat × nat ⇒ bool).
    bisimulation step1 step2 final1 final2 ORDER MATCH"
  using obtains_bisimulation_from_forward_simulation[OF assms] by metis

lemma obtains_bisimulation_from_backward_simulation:
  fixes
    step1 :: "'state1 ⇒ 'state1 ⇒ bool" and final1 :: "'state1 ⇒ bool" and
    step2 :: "'state2 ⇒ 'state2 ⇒ bool" and final2 :: "'state2 ⇒ bool" and
    match :: "'index ⇒ 'state1 ⇒ 'state2 ⇒ bool" and
    lt :: "'index ⇒ 'index ⇒ bool"
  assumes "right_unique step1" and "right_unique step2" and
    final1_stuck: "∀s1. final1 s1 ⟶ (∄s1'. step1 s1 s1')" and
    final2_stuck: "∀s2. final2 s2 ⟶ (∄s2'. step2 s2 s2')" and
    matching_states_agree_on_final: "∀i s1 s2. match i s1 s2 ⟶ final1 s1 ⟷ final2 s2" and
    matching_states_are_safe:
      "∀i s1 s2. match i s1 s2 ⟶ safe_state step1 final1 s1 ∧ safe_state step2 final2 s2" and
    "wfP lt" and
    bsim: "∀i s1 s2 s2'. match i s1 s2 ⟶ step2 s2 s2' ⟶
      (∃i' s1'. step1⇧+⇧+ s1 s1' ∧ match i' s1' s2') ∨ (∃i'. match i' s1 s2' ∧ lt i' i)"
  obtains
    MATCH :: "nat × nat ⇒ 'state1 ⇒ 'state2 ⇒ bool" and
    ORDER :: "nat × nat ⇒ nat × nat ⇒ bool"
  where
    "bisimulation step1 step2 final1 final2 ORDER MATCH"
proof -
  have matching_states_agree_on_final': "∀i s2 s1. (λi s2 s1. match i s1 s2) i s2 s1 ⟶ final2 s2 ⟷ final1 s1"
    using matching_states_agree_on_final by simp

  have matching_states_are_safe':
      "∀i s2 s1. (λi s2 s1. match i s1 s2) i s2 s1 ⟶ safe_state step2 final2 s2 ∧ safe_state step1 final1 s1"
    using matching_states_are_safe by simp

  have "simulation step2 step1 (λi s2 s1. match i s1 s2) lt"
    using bsim unfolding simulation_def by metis

  obtain
    MATCH :: "nat × nat ⇒ 'state2 ⇒ 'state1 ⇒ bool" and
    ORDER :: "nat × nat ⇒ nat × nat ⇒ bool"
  where
    "(⋀i s1 s2. match i s1 s2 ⟹ ∃j. MATCH j s2 s1)" and
    "(⋀j s1 s2. MATCH j s2 s1 ⟹ final1 s1 = final2 s2)" and
    "(⋀j s1 s2. MATCH j s2 s1 ⟹ stuck_state step1 s1 = stuck_state step2 s2)" and
    "(⋀j s1 s2. MATCH j s2 s1 ⟹ safe_state step1 final1 s1 ∧ safe_state step2 final2 s2)" and
    "wfP ORDER" and
    fsim': "simulation step1 step2 (λi s1 s2. MATCH i s2 s1) ORDER" and
    bsim': "simulation step2 step1 (λi s2 s1. MATCH i s2 s1) ORDER"
    using lift_strong_simulation_to_bisimulation'[OF assms(2,1) final2_stuck final1_stuck
        matching_states_agree_on_final' matching_states_are_safe' ‹wfP lt›
        ‹simulation step2 step1 (λi s2 s1. match i s1 s2) lt›]
    by (smt (verit))

  have "bisimulation step1 step2 final1 final2 ORDER (λi s1 s2. MATCH i s2 s1)"
  proof unfold_locales
    show "⋀i s1 s2. MATCH i s2 s1 ⟹ final1 s1 ⟹ final2 s2"
      using ‹⋀s2 s1 j. MATCH j s2 s1 ⟹ final1 s1 = final2 s2› by metis
  next
    show "⋀i s1 s2. MATCH i s2 s1 ⟹ final2 s2 ⟹ final1 s1"
      using ‹⋀s2 s1 j. MATCH j s2 s1 ⟹ final1 s1 = final2 s2› by metis
  next
    show "wfP ORDER"
      using ‹wfP ORDER› .
  next
    show "⋀i s1 s2 s1'. MATCH i s2 s1 ⟹ step1 s1 s1' ⟹
      (∃i' s2'. step2⇧+⇧+ s2 s2' ∧ MATCH i' s2' s1') ∨ (∃i'. MATCH i' s2 s1' ∧ ORDER i' i)"
      using fsim' unfolding simulation_def by metis
  next
    show "⋀i s1 s2 s2'. MATCH i s2 s1 ⟹ step2 s2 s2' ⟹
      (∃i' s1'. step1⇧+⇧+ s1 s1' ∧ MATCH i' s2' s1') ∨ (∃i'. MATCH i' s2' s1 ∧ ORDER i' i)"
      using bsim' unfolding simulation_def by metis
  next
    show "⋀s. final1 s ⟹ finished step1 s"
      by (simp add: final1_stuck finished_def)
  next
    show "⋀s. final2 s ⟹ finished step2 s"
      by (simp add: final2_stuck finished_def)
  qed

  thus thesis
    using that by metis
qed

corollary ex_bisimulation_from_backward_simulation:
  fixes
    step1 :: "'state1 ⇒ 'state1 ⇒ bool" and final1 :: "'state1 ⇒ bool" and
    step2 :: "'state2 ⇒ 'state2 ⇒ bool" and final2 :: "'state2 ⇒ bool" and
    match :: "'index ⇒ 'state1 ⇒ 'state2 ⇒ bool" and
    lt :: "'index ⇒ 'index ⇒ bool"
  assumes "right_unique step1" and "right_unique step2" and
    final1_stuck: "∀s1. final1 s1 ⟶ (∄s1'. step1 s1 s1')" and
    final2_stuck: "∀s2. final2 s2 ⟶ (∄s2'. step2 s2 s2')" and
    matching_states_agree_on_final: "∀i s1 s2. match i s1 s2 ⟶ final1 s1 ⟷ final2 s2" and
    matching_states_are_safe:
      "∀i s1 s2. match i s1 s2 ⟶ safe_state step1 final1 s1 ∧ safe_state step2 final2 s2" and
    "wfP lt" and
    bsim: "∀i s1 s2 s2'. match i s1 s2 ⟶ step2 s2 s2' ⟶
      (∃i' s1'. step1⇧+⇧+ s1 s1' ∧ match i' s1' s2') ∨ (∃i'. match i' s1 s2' ∧ lt i' i)"
  shows "∃(MATCH :: nat × nat ⇒ 'state1 ⇒ 'state2 ⇒ bool)
    (ORDER :: nat × nat ⇒ nat × nat ⇒ bool).
    bisimulation step1 step2 final1 final2 ORDER MATCH"
  using obtains_bisimulation_from_backward_simulation[OF assms] by metis

subsection ‹Composition of backward simulations›

definition rel_comp ::
  "('a ⇒ 'b ⇒ 'c ⇒ bool) ⇒ ('d ⇒ 'c ⇒ 'e ⇒ bool) ⇒ ('a × 'd) ⇒ 'b ⇒ 'e ⇒ bool" where
  "rel_comp r1 r2 i ≡ (r1 (fst i) OO r2 (snd i))"

lemma backward_simulation_composition:
  assumes
    "backward_simulation step1 step2 final1 final2 order1 match1"
    "backward_simulation step2 step3 final2 final3 order2 match2"
  shows
    "backward_simulation step1 step3 final1 final3
      (lex_prodp order1⇧+⇧+ order2) (rel_comp match1 match2)"
proof intro_locales
  show "semantics step1 final1"
    by (auto intro: backward_simulation.axioms assms)
next
  show "semantics step3 final3"
    by (auto intro: backward_simulation.axioms assms)
next
  show "well_founded (lex_prodp order1⇧+⇧+ order2)"
    using assms[THEN backward_simulation.axioms(3)]
    by (simp add: lex_prodp_well_founded well_founded.intro well_founded.wf wfP_trancl)
next
  show "backward_simulation_axioms step1 step3 final1 final3
    (lex_prodp order1⇧+⇧+ order2) (rel_comp match1 match2)"
  proof
    fix i s1 s3
    assume
      match: "rel_comp match1 match2 i s1 s3" and
      final: "final3 s3"
    obtain i1 i2 s2 where "match1 i1 s1 s2" and "match2 i2 s2 s3" and "i = (i1, i2)"
      using match unfolding rel_comp_def by auto
    thus "final1 s1"
      using final assms[THEN backward_simulation.match_final]
      by simp
  next
    fix i s1 s3 s3'
    assume
      match: "rel_comp match1 match2 i s1 s3" and
      step: "step3 s3 s3'"
    obtain i1 i2 s2 where "match1 i1 s1 s2" and "match2 i2 s2 s3" and i_def: "i = (i1, i2)"
      using match unfolding rel_comp_def by auto
    from backward_simulation.simulation[OF assms(2) ‹match2 i2 s2 s3› step]
    show "(∃i' s1'. step1⇧+⇧+ s1 s1' ∧ rel_comp match1 match2 i' s1' s3') ∨
       (∃i'. rel_comp match1 match2 i' s1 s3' ∧ lex_prodp order1⇧+⇧+ order2 i' i)"
      (is "(∃i' s1'. ?STEPS i' s1') ∨ ?STALL")
    proof
      assume "∃i2' s2'. step2⇧+⇧+ s2 s2' ∧ match2 i2' s2' s3'"
      then obtain i2' s2' where "step2⇧+⇧+ s2 s2'" and "match2 i2' s2' s3'" by auto
      from backward_simulation.lift_simulation_plus[OF assms(1) ‹step2⇧+⇧+ s2 s2'› ‹match1 i1 s1 s2›]
      show ?thesis
      proof
        assume "∃i2 s1'. step1⇧+⇧+ s1 s1' ∧ match1 i2 s1' s2'"
        then obtain i2 s1' where "step1⇧+⇧+ s1 s1'" and "match1 i2 s1' s2'" by auto
        hence "?STEPS (i2, i2') s1'"
          by (auto intro: ‹match2 i2' s2' s3'› simp: rel_comp_def)
        thus ?thesis by auto
      next
        assume "∃i2. match1 i2 s1 s2' ∧ order1⇧+⇧+ i2 i1"
        then obtain i2'' where "match1 i2'' s1 s2'" and "order1⇧+⇧+ i2'' i1" by auto
        hence ?STALL
          unfolding rel_comp_def i_def lex_prodp_def
          using ‹match2 i2' s2' s3'› by auto
        thus ?thesis by simp
      qed
    next
      assume "∃i2'. match2 i2' s2 s3' ∧ order2 i2' i2"
      then obtain i2' where "match2 i2' s2 s3'" and "order2 i2' i2" by auto
      hence ?STALL
        unfolding rel_comp_def i_def lex_prodp_def
        using ‹match1 i1 s1 s2› by auto
      thus ?thesis by simp
    qed
  qed
qed

context
  fixes r :: "'i ⇒ 'a ⇒ 'a ⇒ bool"
begin

fun rel_comp_pow where
  "rel_comp_pow [] x y = False" |
  "rel_comp_pow [i] x y = r i x y" |
  "rel_comp_pow (i # is) x z = (∃y. r i x y ∧ rel_comp_pow is y z)"

end

lemma backward_simulation_pow:
  assumes
    "backward_simulation step step final final order match"
  shows
    "backward_simulation step step final final (lexp order⇧+⇧+) (rel_comp_pow match)"
proof intro_locales
  show "semantics step final"
    by (auto intro: backward_simulation.axioms assms)
next
  show "well_founded (lexp order⇧+⇧+)"
    using backward_simulation.axioms(3)[OF assms] lex_list_well_founded
    using well_founded.intro well_founded.wf wfP_trancl by blast
next
  show "backward_simulation_axioms step step final final (lexp order⇧+⇧+) (rel_comp_pow match)"
  proof unfold_locales
    fix "is" s1 s2
    assume "rel_comp_pow match is s1 s2" and "final s2"
    thus "final s1" thm rel_comp_pow.induct
    proof (induction "is" s1 s2 rule: rel_comp_pow.induct)
      case (1 x y)
      then show ?case by simp
    next
      case (2 i x y)
      then show ?case
        using backward_simulation.match_final[OF assms(1)] by simp
    next
      case (3 i1 i2 "is" x z)
      from "3.prems"[simplified] obtain y where
        match: "match i1 x y" and "rel_comp_pow match (i2 # is) y z"
        by auto
      hence "final y" using "3.IH" "3.prems" by simp
      thus ?case
        using "3.prems" match backward_simulation.match_final[OF assms(1)] by auto
    qed
  next
    fix "is" s1 s3 s3'
    assume "rel_comp_pow match is s1 s3" and "step s3 s3'"
    hence "(∃is' s1'. step⇧+⇧+ s1 s1' ∧ length is' = length is ∧ rel_comp_pow match is' s1' s3') ∨
      (∃is'. rel_comp_pow match is' s1 s3' ∧ lexp order⇧+⇧+ is' is)"
    proof (induction "is" s1 s3 arbitrary: s3' rule: rel_comp_pow.induct)
      case 1
      then show ?case by simp
    next
      case (2 i s1 s3)
      from backward_simulation.simulation[OF assms(1) "2.prems"[simplified]] show ?case
      proof
        assume "∃i' s1'. step⇧+⇧+ s1 s1' ∧ match i' s1' s3'"
        then obtain i' s1' where "step⇧+⇧+ s1 s1'" and "match i' s1' s3'" by auto
        hence "step⇧+⇧+ s1 s1' ∧ rel_comp_pow match [i'] s1' s3'" by simp
        thus ?thesis
          by (metis length_Cons)
      next
        assume "∃i'. match i' s1 s3' ∧ order i' i"
        then obtain i' where "match i' s1 s3'" and "order i' i" by auto
        hence "rel_comp_pow match [i'] s1 s3' ∧ lexp order⇧+⇧+ [i'] [i]"
          by (simp add: lexp_head tranclp.r_into_trancl)
        thus ?thesis by blast
      qed
    next
      case (3 i1 i2 "is" s1 s3)
      from "3.prems"[simplified] obtain s2 where
        "match i1 s1 s2" and 0: "rel_comp_pow match (i2 # is) s2 s3"
        by auto
      from "3.IH"[OF 0 "3.prems"(2)] show ?case
      proof
        assume "∃is' s2'. step⇧+⇧+ s2 s2' ∧ length is' = length (i2 # is) ∧
          rel_comp_pow match is' s2' s3'"
        then obtain i2' is' s2' where
          "step⇧+⇧+ s2 s2'" and "length is' = length is" and "rel_comp_pow match (i2' # is') s2' s3'"
          by (metis Suc_length_conv)
        from backward_simulation.lift_simulation_plus[OF assms(1) ‹step⇧+⇧+ s2 s2'› ‹match i1 s1 s2›]
        show ?thesis
        proof
          assume "∃i2 s1'. step⇧+⇧+ s1 s1' ∧ match i2 s1' s2'"
          thus ?thesis
            using ‹rel_comp_pow match (i2' # is') s2' s3'›
            by (metis ‹length is' = length is› length_Cons rel_comp_pow.simps(3))
        next
          assume "∃i2. match i2 s1 s2' ∧ order⇧+⇧+ i2 i1"
          then obtain i1' where "match i1' s1 s2'" and "order⇧+⇧+ i1' i1" by auto
          hence "rel_comp_pow match (i1' # i2' # is') s1 s3'"
            using ‹rel_comp_pow match (i2' # is') s2' s3'› by auto
          moreover have "lexp order⇧+⇧+ (i1' # i2' # is') (i1 # i2 # is)"
            using ‹order⇧+⇧+ i1' i1› ‹length is' = length is›
            by (auto intro: lexp_head)
          ultimately show ?thesis by fast
        qed
      next
        assume "∃i'. rel_comp_pow match i' s2 s3' ∧ lexp order⇧+⇧+ i' (i2 # is)"
        then obtain i2' is' where
          "rel_comp_pow match (i2' # is') s2 s3'" and "lexp order⇧+⇧+ (i2' # is') (i2 # is)"
          by (metis lexp.simps)
        thus ?thesis
          by (metis ‹match i1 s1 s2› lexp.simps(1) rel_comp_pow.simps(3))
      qed
    qed
    thus "(∃is' s1'. step⇧+⇧+ s1 s1' ∧ rel_comp_pow match is' s1' s3') ∨
      (∃is'. rel_comp_pow match is' s1 s3' ∧ lexp order⇧+⇧+ is' is)"
      by auto
  qed
qed

definition lockstep_backward_simulation where
  "lockstep_backward_simulation step1 step2 match ≡
    ∀s1 s2 s2'. match s1 s2 ⟶ step2 s2 s2' ⟶ (∃s1'. step1 s1 s1' ∧ match s1' s2')"

definition plus_backward_simulation where
  "plus_backward_simulation step1 step2 match ≡
    ∀s1 s2 s2'. match s1 s2 ⟶ step2 s2 s2' ⟶ (∃s1'. step1⇧+⇧+ s1 s1' ∧ match s1' s2')"

lemma
  assumes "lockstep_backward_simulation step1 step2 match"
  shows "plus_backward_simulation step1 step2 match"
unfolding plus_backward_simulation_def
proof safe
  fix s1 s2 s2'
  assume "match s1 s2" and "step2 s2 s2'"
  then obtain s1' where "step1 s1 s1'" and "match s1' s2'"
    using assms(1) unfolding lockstep_backward_simulation_def by blast
  then show "∃s1'. step1⇧+⇧+ s1 s1' ∧ match s1' s2'"
    by auto
qed

lemma lockstep_to_plus_backward_simulation:
  fixes
    match :: "'state1 ⇒ 'state2 ⇒ bool" and
    step1 :: "'state1 ⇒ 'state1 ⇒ bool" and
    step2 :: "'state2 ⇒ 'state2 ⇒ bool"
  assumes
    lockstep_simulation: "⋀s1 s2 s2'. match s1 s2 ⟹ step2 s2 s2' ⟹ (∃s1'. step1 s1 s1' ∧ match s1' s2')" and
    match: "match s1 s2" and
    step: "step2 s2 s2'"
  shows "∃s1'. step1⇧+⇧+ s1 s1' ∧ match s1' s2'"
proof -
  obtain s1' where "step1 s1 s1'" and "match s1' s2'"
    using lockstep_simulation[OF match step] by auto
  thus ?thesis by auto
qed

lemma lockstep_to_option_backward_simulation:
  fixes
    match :: "'state1 ⇒ 'state2 ⇒ bool" and
    step1 :: "'state1 ⇒ 'state1 ⇒ bool" and
    step2 :: "'state2 ⇒ 'state2 ⇒ bool" and
    measure :: "'state2 ⇒ nat"
  assumes
    lockstep_simulation: "⋀s1 s2 s2'. match s1 s2 ⟹ step2 s2 s2' ⟹ (∃s1'. step1 s1 s1' ∧ match s1' s2')" and
    match: "match s1 s2" and
    step: "step2 s2 s2'"
  shows "(∃s1'. step1 s1 s1' ∧ match s1' s2') ∨ match s1 s2' ∧ measure s2' < measure s2"
  using lockstep_simulation[OF match step] ..

lemma plus_to_star_backward_simulation:
  fixes
    match :: "'state1 ⇒ 'state2 ⇒ bool" and
    step1 :: "'state1 ⇒ 'state1 ⇒ bool" and
    step2 :: "'state2 ⇒ 'state2 ⇒ bool" and
    measure :: "'state2 ⇒ nat"
  assumes
    star_simulation: "⋀s1 s2 s2'. match s1 s2 ⟹ step2 s2 s2' ⟹ (∃s1'. step1⇧+⇧+ s1 s1' ∧ match s1' s2')" and
    match: "match s1 s2" and
    step: "step2 s2 s2'"
  shows "(∃s1'. step1⇧+⇧+ s1 s1' ∧ match s1' s2') ∨ match s1 s2' ∧ measure s2' < measure s2"
  using star_simulation[OF match step] ..

lemma lockstep_to_plus_forward_simulation:
  fixes
    match :: "'state1 ⇒ 'state2 ⇒ bool" and
    step1 :: "'state1 ⇒ 'state1 ⇒ bool" and
    step2 :: "'state2 ⇒ 'state2 ⇒ bool"
  assumes
    lockstep_simulation: "⋀s1 s2 s2'. match s1 s2 ⟹ step1 s1 s1' ⟹ (∃s2'. step2 s2 s2' ∧ match s1' s2')" and
    match: "match s1 s2" and
    step: "step1 s1 s1'"
  shows "∃s2'. step2⇧+⇧+ s2 s2' ∧ match s1' s2'"
proof -
  obtain s2' where "step2 s2 s2'" and "match s1' s2'"
    using lockstep_simulation[OF match step] by auto
  thus ?thesis by auto
qed

end