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 s2 b2  ¬is_wrong b2  match i s1 s2 
    b1 i'. L1.state_behaves s1 b1  rel_behaviour (match i') b1 b2"
proof(induction rule: L2.state_behaves.cases)
  case (state_terminates s2 s2')
  then obtain i' s1' where "L1.eval s1 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 s1 (Terminates s1')"
    using L1.final_finished
    by (simp add: L1.state_terminates L1.eval s1 s1')
  moreover have "rel_behaviour (match i') (Terminates s1') b2"
    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 b2 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