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 1 2 match order 
    (i s1 s2 s1'. match i s1 s2  1 s1 s1' 
      (s2' i'. 2++ 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 1 :: "'a  'a  bool" and 2 :: "'b  'b  bool" and
    match :: "'c  'a  'b  bool" and order :: "'c  'c  bool"
where
  bisim_stuck: "stuck_state 1 s1  stuck_state 2 s2  match i s1 s2 
    match_bisim 1 2 match order (0, 0) s1 s2" |

  bisim_steps: "match i s10 s20  1** s10 s1  (1 ^^ Suc m) s1 s1' 
    2** s20 s2  (2 ^^ Suc n) s2 s2'  match i' s1' s2' 
    match_bisim 1 2 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 s20 n1 n2 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 s10 s20 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 s10 s20"
              using match i s10 s20 .
          next
            show "step1** s10 s1'"
              using step1** s10 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** s20 s2"
              using step2** s20 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 s10 s20 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 s10 s20"
              using match i s10 s20 .
          next
            show "step1** s10 s1"
              using step1** s10 s1 .
          next
            show "(step1 ^^ Suc m) s1 s1'"
              using (step1 ^^ Suc m) s1 s1' .
          next
            show "step2** s20 s2'"
              using step2** s20 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