Theory VeriComp.Lifting_Simulation_To_Bisimulation

theory Lifting_Simulation_To_Bisimulation
  imports
    Main
    "VeriComp.Well_founded"
begin

definition stuck_state :: "('a ⇒ 'b ⇒ bool) ⇒ 'a ⇒ bool" where
  "stuck_state ℛ s ⟷ (∄s'. ℛ s s')"

definition simulation ::
  "('a ⇒ 'a ⇒ bool) ⇒ ('b ⇒ 'b ⇒ bool) ⇒ ('c ⇒ 'a ⇒ 'b ⇒ bool) ⇒ ('c ⇒ 'c ⇒ bool) ⇒ bool"
where
  "simulation ℛ⇩₁ ℛ⇩₂ match order ⟷
    (∀i s1 s2 s1'. match i s1 s2 ⟶ ℛ⇩₁ s1 s1' ⟶
      (∃s2' i'. ℛ⇩₂⇧⁺⇧⁺ s2 s2' ∧ match i' s1' s2') ∨ (∃i'. match i' s1' s2 ∧ order i' i))"

lemma finite_progress:
  fixes
    step1 :: "'s1 ⇒ 's1 ⇒ bool" and
    step2 :: "'s2 ⇒ 's2 ⇒ bool" and
    match :: "'i ⇒ 's1 ⇒ 's2 ⇒ bool" and
    order :: "'i ⇒ 'i ⇒ bool"
  assumes
    matching_states_agree_on_stuck:
      "∀i s1 s2. match i s1 s2 ⟶ stuck_state step1 s1 ⟷ stuck_state step2 s2" and
    well_founded_order: "wfP order" and
    sim: "simulation step1 step2 match order"
  shows "match i s1 s2 ⟹ step1 s1 s1' ⟹
    ∃m s1'' n s2'' i'. (step1 ^^ m) s1' s1'' ∧ (step2 ^^ Suc n) s2 s2'' ∧ match i' s1'' s2''"
  using well_founded_order
proof (induction i arbitrary: s1 s1' rule: wfP_induct_rule)
  case (less i)
  show ?case
    using sim[unfolded simulation_def, rule_format, OF ‹match i s1 s2› ‹step1 s1 s1'›]
  proof (elim disjE exE conjE)
    show "⋀s2' i'. step2⇧⁺⇧⁺ s2 s2' ⟹ match i' s1' s2' ⟹ ?thesis"
      by (metis Suc_pred relpowp_0_I tranclp_power)
  next
    fix i'
    assume "match i' s1' s2" and "order i' i"

    have "¬ stuck_state step1 s1"
      using ‹step1 s1 s1'› stuck_state_def by metis
    hence "¬ stuck_state step2 s2"
      using ‹match i s1 s2› matching_states_agree_on_stuck by metis
    hence "¬ stuck_state step1 s1'"
      using ‹match i' s1' s2› matching_states_agree_on_stuck by metis

    then obtain s1'' where "step1 s1' s1''"
      by (metis stuck_state_def)

    obtain m s1''' n s2' i'' where
      "(step1 ^^ m) s1'' s1'''" and
      "(step2 ^^ Suc n) s2 s2'" and
      "match i'' s1''' s2'"
      using less.IH[OF ‹order i' i› ‹match i' s1' s2› ‹step1 s1' s1''›] by metis

    show ?thesis
    proof (intro exI conjI)
      show "(step1 ^^ Suc m) s1' s1'''"
        using ‹(step1 ^^ m) s1'' s1'''› ‹step1 s1' s1''› by (metis relpowp_Suc_I2)
    next
      show "(step2 ^^ Suc n) s2 s2'"
        using ‹(step2 ^^ Suc n) s2 s2'› .
    next
      show "match i'' s1''' s2'"
        using ‹match i'' s1''' s2'› .
    qed
  qed
qed

context begin

private inductive match_bisim
  for ℛ⇩₁ :: "'a ⇒ 'a ⇒ bool" and ℛ⇩₂ :: "'b ⇒ 'b ⇒ bool" and
    match :: "'c ⇒ 'a ⇒ 'b ⇒ bool" and order :: "'c ⇒ 'c ⇒ bool"
where
  bisim_stuck: "stuck_state ℛ⇩₁ s1 ⟹ stuck_state ℛ⇩₂ s2 ⟹ match i s1 s2 ⟹
    match_bisim ℛ⇩₁ ℛ⇩₂ match order (0, 0) s1 s2" |

  bisim_steps: "match i s1⇩₀ s2⇩₀ ⟹ ℛ⇩₁⇧^*⇧^* s1⇩₀ s1 ⟹ (ℛ⇩₁ ^^ Suc m) s1 s1' ⟹
    ℛ⇩₂⇧^*⇧^* s2⇩₀ s2 ⟹ (ℛ⇩₂ ^^ Suc n) s2 s2' ⟹ match i' s1' s2' ⟹
    match_bisim ℛ⇩₁ ℛ⇩₂ match order (m, n) s1 s2"

theorem lift_strong_simulation_to_bisimulation:
  fixes
    step1 :: "'s1 ⇒ 's1 ⇒ bool" and
    step2 :: "'s2 ⇒ 's2 ⇒ bool" and
    match :: "'i ⇒ 's1 ⇒ 's2 ⇒ bool" and
    order :: "'i ⇒ 'i ⇒ bool"
  assumes
    matching_states_agree_on_stuck:
      "∀i s1 s2. match i s1 s2 ⟶ stuck_state step1 s1 ⟷ stuck_state step2 s2" and
    well_founded_order: "wfP order" and
    sim: "simulation step1 step2 match order"
  obtains
    MATCH :: "nat × nat ⇒ 's1 ⇒ 's2 ⇒ bool" and
    ORDER :: "nat × nat ⇒ nat × nat ⇒ bool"
  where
    "⋀i s1 s2. match i s1 s2 ⟹ (∃j. MATCH j s1 s2)"
    "⋀j s1 s2. MATCH j s1 s2 ⟹
      (∃i. stuck_state step1 s1 ∧ stuck_state step2 s2 ∧ match i s1 s2) ∨
      (∃i s1' s2'. step1⇧⁺⇧⁺ s1 s1' ∧ step2⇧⁺⇧⁺ s2 s2' ∧ match i s1' s2')" and
    "wfP ORDER" and
    "right_unique step1 ⟹ simulation step1 step2 (λi s1 s2. MATCH i s1 s2) ORDER" and
    "right_unique step2 ⟹ simulation step2 step1 (λi s2 s1. MATCH i s1 s2) ORDER"
proof -
  define MATCH :: "nat × nat ⇒ 's1 ⇒ 's2 ⇒ bool" where
    "MATCH = match_bisim step1 step2 match order"

  define ORDER :: "nat × nat ⇒ nat × nat ⇒ bool" where
    "ORDER = lex_prodp ((<) :: nat ⇒ nat ⇒ bool) ((<) :: nat ⇒ nat ⇒ bool)"

  have MATCH_if_match: "⋀i s1 s2. match i s1 s2 ⟹ ∃j. MATCH j s1 s2"
  proof -
    fix i s1 s2
    assume "match i s1 s2"

    have "stuck_state step1 s1 ⟷ stuck_state step2 s2"
      using ‹match i s1 s2› matching_states_agree_on_stuck by metis
    hence "(stuck_state step1 s1 ∧ stuck_state step2 s2) ∨ (∃s1' s2'. step1 s1 s1' ∧ step2 s2 s2')"
      by (metis stuck_state_def)
    thus "∃j. MATCH j s1 s2"
    proof (elim disjE conjE exE)
      show "stuck_state step1 s1 ⟹ stuck_state step2 s2 ⟹ ∃j. MATCH j s1 s2"
        by (metis MATCH_def ‹match i s1 s2› bisim_stuck)
    next
      fix s1' s2'
      assume "step1 s1 s1'" and "step2 s2 s2'"

      obtain m n s1'' s2'' i' where
        "(step1 ^^ m) s1' s1''" and
        "(step2 ^^ Suc n) s2 s2''" and
        "match i' s1'' s2''"
        using finite_progress[OF assms ‹match i s1 s2› ‹step1 s1 s1'›] by metis

      show "∃j. MATCH j s1 s2"
      proof (intro exI)
        show "MATCH (m, n) s1 s2"
          unfolding MATCH_def
        proof (rule bisim_steps)
          show "match i s1 s2"
            using ‹match i s1 s2› .
        next
          show "step1⇧^*⇧^* s1 s1"
            by simp
        next
          show "(step1 ^^ Suc m) s1 s1''"
            using ‹step1 s1 s1'› ‹(step1 ^^ m) s1' s1''› by (metis relpowp_Suc_I2)
        next
          show "step2⇧^*⇧^* s2 s2"
            by simp
        next
          show "(step2 ^^ Suc n) s2 s2''"
            using ‹(step2 ^^ Suc n) s2 s2''› .
        next
          show "match i' s1'' s2''"
            using ‹match i' s1'' s2''› .
        qed
      qed
    qed
  qed

  show thesis
  proof (rule that)
    show "⋀i s1 s2. match i s1 s2 ⟹ ∃j. MATCH j s1 s2"
      using MATCH_if_match .
  next
    fix j :: "nat × nat" and s1 :: 's1 and s2 :: 's2
    assume "MATCH j s1 s2"
    thus "(∃i. stuck_state step1 s1 ∧ stuck_state step2 s2 ∧ match i s1 s2) ∨
      (∃i s1' s2'. step1⇧⁺⇧⁺ s1 s1' ∧ step2⇧⁺⇧⁺ s2 s2' ∧ match i s1' s2')"
      unfolding MATCH_def
    proof (cases step1 step2 match order j s1 s2 rule: match_bisim.cases)
      case (bisim_stuck i)
      thus ?thesis
        by blast
    next
      case (bisim_steps m s1' i s2⇩₀ n⇩₁ n⇩₂ s2' i')
      hence "∃i s1' s2'. step1⇧⁺⇧⁺ s1 s1' ∧ step2⇧⁺⇧⁺ s2 s2' ∧ match i s1' s2'"
        by (metis tranclp_power zero_less_Suc)
      thus ?thesis ..
    qed
  next
    show "wfP ORDER"
      unfolding ORDER_def
      using lex_prodp_wfP wfP_less well_founded_order by metis
  next
    assume "right_unique step1"
    show "simulation step1 step2 MATCH ORDER"
      unfolding simulation_def
    proof (intro allI impI)
      fix j :: "nat × nat" and s1 s1' :: 's1 and s2 :: 's2
      assume "MATCH j s1 s2" and "step1 s1 s1'"
      hence "match_bisim step1 step2 match order j s1 s2"
        unfolding MATCH_def by metis
      thus "(∃s2' j'. step2⇧⁺⇧⁺ s2 s2' ∧ MATCH j' s1' s2') ∨ (∃j'. MATCH j' s1' s2 ∧ ORDER j' j)"
      proof (cases step1 step2 match order j s1 s2 rule: match_bisim.cases)
        case (bisim_stuck i)
        hence False
          using ‹step1 s1 s1'› stuck_state_def by metis
        thus ?thesis ..
      next
        case (bisim_steps i s1⇩₀ s2⇩₀ m s1'' n s2' i')

        have "(step1 ^^ m) s1' s1''"
          using ‹step1 s1 s1'› ‹(step1 ^^ Suc m) s1 s1''› ‹right_unique step1›
          by (metis relpowp_Suc_D2 right_uniqueD)

        show ?thesis
        proof (cases m)
          case 0
          hence "s1'' = s1'"
            using ‹(step1 ^^ m) s1' s1''› by simp

          have "step2⇧⁺⇧⁺ s2 s2'"
            using ‹(step2 ^^ Suc n) s2 s2'› by (metis tranclp_power zero_less_Suc)

          moreover have "∃j'. MATCH j' s1' s2'"
            using ‹match i' s1'' s2'› ‹s1'' = s1'› MATCH_if_match by metis

          ultimately show ?thesis
            by metis
        next
          case (Suc m')
          define j' where
            "j' = (m', n)"

          have "MATCH j' s1' s2"
            unfolding MATCH_def j'_def
          proof (rule match_bisim.bisim_steps)
            show "match i s1⇩₀ s2⇩₀"
              using ‹match i s1⇩₀ s2⇩₀› .
          next
            show "step1⇧^*⇧^* s1⇩₀ s1'"
              using ‹step1⇧^*⇧^* s1⇩₀ s1› ‹step1 s1 s1'› by auto
          next
            show "(step1 ^^ Suc m') s1' s1''"
              using ‹(step1 ^^ m) s1' s1''› ‹m = Suc m'› by argo
          next
            show "step2⇧^*⇧^* s2⇩₀ s2"
              using ‹step2⇧^*⇧^* s2⇩₀ s2› .
          next
            show "(step2 ^^ Suc n) s2 s2'"
              using ‹(step2 ^^ Suc n) s2 s2'› .
          next
            show "match i' s1'' s2'"
              using ‹match i' s1'' s2'› .
          qed

          moreover have "ORDER j' j"
            unfolding ORDER_def ‹j' = (m', n)› ‹j = (m, n)› ‹m = Suc m'›
            by (simp add: lex_prodp_def)

          ultimately show ?thesis
            by metis
        qed
      qed
    qed
  next
    assume "right_unique step2"
    show "simulation step2 step1 (λi s2 s1. MATCH i s1 s2) ORDER"
      unfolding simulation_def
    proof (intro allI impI)
      fix j :: "nat × nat" and s1 :: 's1 and s2 s2' :: 's2
      assume "MATCH j s1 s2" and "step2 s2 s2'"
      hence "match_bisim step1 step2 match order j s1 s2"
        unfolding MATCH_def by metis
      thus "(∃s1' j'. step1⇧⁺⇧⁺ s1 s1' ∧ MATCH j' s1' s2') ∨ (∃j'. MATCH j' s1 s2' ∧ ORDER j' j)"
      proof (cases step1 step2 match order j s1 s2 rule: match_bisim.cases)
        case (bisim_stuck i)
        hence "stuck_state step2 s2"
          by argo
        hence False
          using ‹step2 s2 s2'› stuck_state_def by metis
        thus ?thesis ..
      next
        case (bisim_steps i s1⇩₀ s2⇩₀ m s1' n s2'' i')
        show ?thesis
        proof (cases n)
          case 0
          hence "s2'' = s2'"
            using ‹step2 s2 s2'› ‹(step2 ^^ Suc n) s2 s2''› ‹right_unique step2›
            by (metis One_nat_def relpowp_1 right_uniqueD)

          have "step1⇧⁺⇧⁺ s1 s1'"
            using ‹(step1 ^^ Suc m) s1 s1'›
            by (metis less_Suc_eq_0_disj tranclp_power)

          moreover have "∃j'. MATCH j' s1' s2'"
            using ‹match i' s1' s2''› ‹s2'' = s2'› MATCH_if_match by metis

          ultimately show ?thesis
            by metis
        next
          case (Suc n')

          define j' where
            "j' = (m, n')"

          have "MATCH j' s1 s2'"
            unfolding MATCH_def j'_def
          proof (rule match_bisim.bisim_steps)
            show "match i s1⇩₀ s2⇩₀"
              using ‹match i s1⇩₀ s2⇩₀› .
          next
            show "step1⇧^*⇧^* s1⇩₀ s1"
              using ‹step1⇧^*⇧^* s1⇩₀ s1› .
          next
            show "(step1 ^^ Suc m) s1 s1'"
              using ‹(step1 ^^ Suc m) s1 s1'› .
          next
            show "step2⇧^*⇧^* s2⇩₀ s2'"
              using ‹step2⇧^*⇧^* s2⇩₀ s2› ‹step2 s2 s2'› by auto
          next
            show "(step2 ^^ Suc n') s2' s2''"
              using ‹step2 s2 s2'› ‹(step2 ^^ Suc n) s2 s2''› ‹right_unique step2›
              by (metis Suc relpowp_Suc_D2 right_uniqueD)
          next
            show "match i' s1' s2''"
              using ‹match i' s1' s2''› .
          qed

          moreover have "ORDER j' j"
            unfolding ORDER_def ‹j' = (m, n')› ‹j = (m, n)› ‹n = Suc n'›
            by (simp add: lex_prodp_def)

          ultimately show ?thesis
            by metis
        qed
      qed
    qed
  qed
qed

end

definition safe_state where
  "safe_state ℛ ℱ s ⟷ (∀s'. ℛ⇧^*⇧^* s s' ⟶ ℱ s' ∨ (∃s''. ℛ s' s''))"

lemma step_preserves_safe_state:
  "ℛ s s' ⟹ safe_state ℛ ℱ s ⟹ safe_state ℛ ℱ s'"
  by (simp add: converse_rtranclp_into_rtranclp safe_state_def)

lemma rtranclp_step_preserves_safe_state:
  "ℛ⇧^*⇧^* s s' ⟹ safe_state ℛ ℱ s ⟹ safe_state ℛ ℱ s'"
  by (simp add: rtranclp_induct step_preserves_safe_state)

lemma tranclp_step_preserves_safe_state:
  "ℛ⇧⁺⇧⁺ s s' ⟹ safe_state ℛ ℱ s ⟹ safe_state ℛ ℱ s'"
  by (simp add: step_preserves_safe_state tranclp_induct)

lemma safe_state_before_step_if_safe_state_after:
  assumes "right_unique ℛ"
  shows "ℛ s s' ⟹ safe_state ℛ ℱ s' ⟹ safe_state ℛ ℱ s"
  by (metis (full_types) assms converse_rtranclpE right_uniqueD safe_state_def)

lemma safe_state_before_rtranclp_step_if_safe_state_after:
  assumes "right_unique ℛ"
  shows "ℛ⇧^*⇧^* s s' ⟹ safe_state ℛ ℱ s' ⟹ safe_state ℛ ℱ s"
  by (smt (verit, best) assms converse_rtranclp_induct safe_state_before_step_if_safe_state_after)

lemma safe_state_before_tranclp_step_if_safe_state_after:
  assumes "right_unique ℛ"
  shows "ℛ⇧⁺⇧⁺ s s' ⟹ safe_state ℛ ℱ s' ⟹ safe_state ℛ ℱ s"
  by (meson assms safe_state_before_rtranclp_step_if_safe_state_after tranclp_into_rtranclp)

lemma safe_state_if_all_states_safe:
  assumes "⋀s. ℱ s ∨ (∃s'. ℛ s s')"
  shows "safe_state ℛ ℱ s"
  using assms by (simp add: safe_state_def)

lemma matching_states_agree_on_stuck_if_they_agree_on_final:
  assumes
    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"
  shows "∀i s1 s2. match i s1 s2 ⟶ stuck_state step1 s1 ⟷ stuck_state step2 s2"
    using assms by (metis rtranclp.rtrancl_refl safe_state_def stuck_state_def)


corollary lift_strong_simulation_to_bisimulation':
  fixes
    step1 :: "'s1 ⇒ 's1 ⇒ bool" and
    step2 :: "'s2 ⇒ 's2 ⇒ bool" and
    match :: "'i ⇒ 's1 ⇒ 's2 ⇒ bool" and
    order :: "'i ⇒ 'i ⇒ 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
    order_well_founded: "wfP order" and
    sim: "simulation step1 step2 match order"
  obtains
    MATCH :: "nat × nat ⇒ 's1 ⇒ 's2 ⇒ bool" and
    ORDER :: "nat × nat ⇒ nat × nat ⇒ bool"
  where
    "⋀i s1 s2. match i s1 s2 ⟹ (∃j. MATCH j s1 s2)"
    "⋀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
    "simulation step1 step2 (λi s1 s2. MATCH i s1 s2) ORDER" and
    "simulation step2 step1 (λi s2 s1. MATCH i s1 s2) ORDER"
proof -
  have matching_states_agree_on_stuck:
    "∀i s1 s2. match i s1 s2 ⟶ stuck_state step1 s1 ⟷ stuck_state step2 s2"
    using matching_states_agree_on_stuck_if_they_agree_on_final[OF final1_stuck final2_stuck
        matching_states_agree_on_final matching_states_are_safe] .

  obtain
    MATCH :: "nat × nat ⇒ 's1 ⇒ 's2 ⇒ bool" and
    ORDER :: "nat × nat ⇒ nat × nat ⇒ bool"
  where
    MATCH_if_match: "⋀i s1 s2. match i s1 s2 ⟹ ∃j. MATCH j s1 s2" and
    MATCH_spec: "⋀j s1 s2. MATCH j s1 s2 ⟹
      (∃i. stuck_state step1 s1 ∧ stuck_state step2 s2 ∧ match i s1 s2) ∨
      (∃i s1' s2'. step1⇧⁺⇧⁺ s1 s1' ∧ step2⇧⁺⇧⁺ s2 s2' ∧ match i s1' s2')" and
    "wfP ORDER" and
    "simulation step1 step2 MATCH ORDER" and
    "simulation step2 step1 (λi s2 s1. MATCH i s1 s2) ORDER"
    using ‹right_unique step1› ‹right_unique step2›
    using lift_strong_simulation_to_bisimulation[
        OF matching_states_agree_on_stuck
        order_well_founded sim]
    by (smt (verit))

  show thesis
  proof (rule that)
    show "⋀i s1 s2. match i s1 s2 ⟹ ∃j. MATCH j s1 s2"
      using MATCH_if_match .
  next
    show "⋀j s1 s2. MATCH j s1 s2 ⟹ final1 s1 = final2 s2"
      using MATCH_spec
      by (metis converse_tranclpE final1_stuck final2_stuck matching_states_agree_on_final)
  next
    show "⋀j s1 s2. MATCH j s1 s2 ⟹ stuck_state step1 s1 = stuck_state step2 s2"
      using MATCH_spec
      by (metis stuck_state_def tranclpD)
  next
    fix j s1 s2
    assume "MATCH j s1 s2"
    then show "safe_state step1 final1 s1 ∧ safe_state step2 final2 s2"
      apply -
      apply (drule MATCH_spec)
      apply (elim disjE exE conjE)
      using matching_states_are_safe apply metis
      using safe_state_before_tranclp_step_if_safe_state_after
      by (metis assms(1) assms(2) matching_states_are_safe)
  next
    show "wfP ORDER"
      using ‹wfP ORDER› .
  next
    show "simulation step1 step2 (λi s1 s2. MATCH i s1 s2) ORDER"
      using ‹simulation step1 step2 (λi s1 s2. MATCH i s1 s2) ORDER› .
  next
    show "simulation step2 step1 (λi s2 s1. MATCH i s1 s2) ORDER"
      using ‹simulation step2 step1 (λi s2 s1. MATCH i s1 s2) ORDER› .
  qed
qed

end