Theory Spectroscopy_Game

text ‹\newpage›
section ‹Weak Spectroscopy Game›
theory Spectroscopy_Game
  imports Energy_Games Energy LTS
begin

text ‹In this theory, we define the weak spectroscopy game as a locale.
This game is an energy game constructed by adding stable and branching conjunctions to a delay bisimulation game that depends on a LTS.
We play the weak spectroscopy game to compare the behaviour of processes and analyze which behavioural equivalences apply.
The moves of a weak spectroscopy game depend on the transitions of the processes and the available energy.
So in other words: If the defender wins the weak spectroscopy game starting with a certain energy, the corresponding behavioural equivalence applies.
\\ Since we added adding stable and branching conjunctions to a delay bisimulation game, we differentiate the positions accordingly.›
datatype ('s, 'a) spectroscopy_position =
         Attacker_Immediate (attacker_state: ‹'s›) (defender_states: ‹'s set›) |
         Attacker_Branch (attacker_state: ‹'s›) (defender_states: ‹'s set›) |
         Attacker_Clause (attacker_state: ‹'s›) (defender_state: ‹'s›) |
         Attacker_Delayed (attacker_state: ‹'s›) (defender_states: ‹'s set›) |

         Defender_Branch (attacker_state: ‹'s›) (attack_action: ‹'a›)
                         (attacker_state_succ: ‹'s›) (defender_states: ‹'s set›)
                         (defender_branch_states: ‹'s set›) |
         Defender_Conj (attacker_state: ‹'s›) (defender_states: ‹'s set›) |
         Defender_Stable_Conj (attacker_state: ‹'s›) (defender_states: ‹'s set›)

context LTS_Tau begin

text‹\label{specmoves}›
text‹We also define the moves of the weak spectroscopy game. Their names indicate the respective HML formulas they correspond to. This correspondence will be shown in section \ref{deviation:lemma3}. ›
fun spectroscopy_moves :: ‹('s, 'a) spectroscopy_position ⇒ ('s, 'a) spectroscopy_position ⇒ energy update option› where
  delay:
    ‹spectroscopy_moves (Attacker_Immediate p Q) (Attacker_Delayed p' Q')
     = (if p' = p ∧ Q ↠S Q' then Some Some else None)› |

  procrastination:
    ‹spectroscopy_moves (Attacker_Delayed p Q) (Attacker_Delayed p' Q')
      = (if (Q' = Q ∧ p ≠ p' ∧ p ↦ τ p') then Some Some else None)› |

  observation:
    ‹spectroscopy_moves (Attacker_Delayed p Q) (Attacker_Immediate p' Q')
      = (if (∃a. p ↦a a p' ∧ Q ↦aS a Q') then (subtract 1 0 0 0 0 0 0 0)
         else None)› |

  f_or_early_conj:
    ‹spectroscopy_moves (Attacker_Immediate p Q) (Defender_Conj p' Q')
      =(if (Q≠{} ∧ Q = Q' ∧ p = p') then (subtract 0 0 0 0 1 0 0 0)
        else None)› |

  late_inst_conj:
    ‹spectroscopy_moves (Attacker_Delayed p Q) (Defender_Conj p' Q')
      = (if p = p' ∧ Q = Q' then Some Some else None)› |

  conj_answer:
    ‹spectroscopy_moves (Defender_Conj p Q) (Attacker_Clause p' q)
      = (if p = p' ∧ q ∈ Q then (subtract 0 0 1 0 0 0 0 0) else None)› |

  pos_neg_clause:
    ‹spectroscopy_moves (Attacker_Clause p q) (Attacker_Delayed p' Q')
      = (if (p = p') then
          (if {q} ↠S Q' then Some min1_6 else None)
         else (if ({p} ↠S Q'∧ q=p')
               then Some (λe. Option.bind ((subtract_fn 0 0 0 0 0 0 0 1) e) min1_7) else None))› |

  late_stbl_conj:
    ‹spectroscopy_moves (Attacker_Delayed p Q) (Defender_Stable_Conj p' Q')
      = (if (p = p' ∧ Q' = { q ∈ Q. (∄q'. q ↦τ q')} ∧ (∄p''. p ↦τ p''))
          then Some Some else None)› |

  conj_s_answer:
    ‹spectroscopy_moves (Defender_Stable_Conj p Q) (Attacker_Clause p' q)
      = (if p = p' ∧ q ∈ Q then (subtract 0 0 0 1 0 0 0 0)
         else None)› |

  empty_stbl_conj_answer:
    ‹spectroscopy_moves (Defender_Stable_Conj p Q) (Defender_Conj p' Q')
      = (if Q = {} ∧ Q = Q' ∧ p = p' then (subtract 0 0 0 1 0 0 0 0)
         else None)› |

  br_conj:
    ‹spectroscopy_moves (Attacker_Delayed p Q) (Defender_Branch p' α p'' Q' Qα)
      = (if (p = p' ∧ Q' = Q - Qα ∧ p ↦a α p'' ∧ Qα ⊆ Q) then Some Some
         else None)› |

  br_answer:
    ‹spectroscopy_moves (Defender_Branch p α p' Q Qα) (Attacker_Clause p'' q)
      = (if (p = p'' ∧ q ∈ Q) then (subtract 0 1 1 0 0 0 0 0) else None)› |

  br_obsv:
    ‹spectroscopy_moves (Defender_Branch p α p' Q Qα) (Attacker_Branch p'' Q')
      = (if (p' = p'' ∧ Qα ↦aS α Q')
         then Some (λe. Option.bind ((subtract_fn 0 1 1 0 0 0 0 0) e) min1_6) else None)› |

  br_acct:
    ‹spectroscopy_moves (Attacker_Branch p Q) (Attacker_Immediate p' Q')
      = (if p = p' ∧ Q = Q' then subtract 1 0 0 0 0 0 0 0 else None)› |

  others: ‹spectroscopy_moves _ _ = None›

fun spectroscopy_defender where
  ‹spectroscopy_defender (Attacker_Immediate _ _) = False› |
  ‹spectroscopy_defender (Attacker_Branch _ _) = False› |
  ‹spectroscopy_defender (Attacker_Clause _ _) = False› |
  ‹spectroscopy_defender (Attacker_Delayed _ _) = False› |
  ‹spectroscopy_defender (Defender_Branch _ _ _ _ _) = True› |
  ‹spectroscopy_defender (Defender_Conj _ _) = True› |
  ‹spectroscopy_defender (Defender_Stable_Conj _ _) = True›

interpretation Game: energy_game ‹spectroscopy_moves› ‹spectroscopy_defender› ‹(≤)›
proof
  fix e e' ::energy
  show ‹e ≤ e' ⟹ e' ≤ e ⟹ e = e'› unfolding less_eq_energy_def
    by (smt (z3) energy.case_eq_if energy.expand nle_le)
next
  fix g g' e e' eu eu'
  assume monotonicity_assms:
    ‹spectroscopy_moves g g' ≠ None›
    ‹the (spectroscopy_moves g g') e = Some eu›
    ‹the (spectroscopy_moves g g') e' = Some eu'›
    ‹e ≤ e'›
  show ‹eu ≤ eu'›
  proof (cases g)
    case (Attacker_Immediate p Q)
    with monotonicity_assms
    show ?thesis
      by (cases g', simp_all, (smt (z3) option.distinct(1) option.sel minus_component_leq)+)
  next
    case (Attacker_Branch p Q)
    with monotonicity_assms
    show ?thesis
      by (cases g', simp_all, (smt (z3) option.distinct(1) option.sel minus_component_leq)+)
  next
    case (Attacker_Clause p q)
    hence ‹∃p' Q'. g'= (Attacker_Delayed p' Q')›
      using monotonicity_assms(1,2)
      by (metis spectroscopy_defender.cases spectroscopy_moves.simps(22,23,26,46,62,67))
    hence ‹spectroscopy_moves g g' = Some min1_6 ∨ spectroscopy_moves g g' = Some (λe. Option.bind ((subtract_fn 0 0 0 0 0 0 0 1) e) min1_7)›
      using monotonicity_assms(1,2) Attacker_Clause
      by (smt (verit, ccfv_threshold) spectroscopy_moves.simps(7))
    thus ?thesis
    proof safe
      assume ‹spectroscopy_moves g g' = Some min1_6›
      thus ?thesis
        using monotonicity_assms min.mono
        unfolding leq_components
        by (metis min_1_6_simps option.sel)
    next
      assume ‹spectroscopy_moves g g' = Some (λe. Option.bind (if ¬ E 0 0 0 0 0 0 0 1 ≤ e then None else Some (e - E 0 0 0 0 0 0 0 1)) min1_7)›
      thus ?thesis
        unfolding min_1_7_subtr_simp
        using monotonicity_assms
        by (smt (z3) enat_diff_mono energy.sel leq_components min.mono option.distinct(1) option.sel)
    qed
  next
    case (Attacker_Delayed p Q)
    hence ‹(∃p' Q'. g'=(Attacker_Delayed p' Q')) ∨
      (∃p' Q'. g'=(Attacker_Immediate p' Q')) ∨
      (∃p' Q'. g'=(Defender_Conj p' Q')) ∨
      (∃p' Q'. g'=(Defender_Stable_Conj p' Q')) ∨
      (∃p' p'' Q' α Qα . g'= (Defender_Branch p' α p'' Q' Qα))›
      by (metis monotonicity_assms(1) spectroscopy_defender.cases spectroscopy_moves.simps(27,59))
    thus ?thesis
    proof (safe)
      fix p' Q'
      assume ‹g' = Attacker_Delayed p' Q'›
      thus ‹eu ≤ eu'›
        using Attacker_Delayed monotonicity_assms local.procrastination
        by (metis option.sel)
    next
      fix p' Q'
      assume ‹g' = Attacker_Immediate p' Q'›
      hence ‹spectroscopy_moves g g' = (subtract 1 0 0 0 0 0 0 0)›
        using Attacker_Delayed monotonicity_assms local.observation
        by (clarify, presburger)
      thus ‹eu ≤ eu'›
        by (smt (verit, best) mono_subtract monotonicity_assms option.distinct(1) option.sel)
    next
      fix p' Q'
      assume ‹g' = Defender_Conj p' Q'›
      thus ‹eu ≤ eu'›
        using Attacker_Delayed monotonicity_assms local.late_inst_conj
        by (metis option.sel)
    next
      fix p' Q'
      assume ‹g' = Defender_Stable_Conj p' Q'›
      thus ‹eu ≤ eu'›
        using Attacker_Delayed monotonicity_assms local.late_stbl_conj
        by (metis (no_types, lifting) option.sel)
    next
      fix p' p'' Q' α Qα
      assume ‹g' = Defender_Branch p' α p'' Q' Qα›
      thus ‹eu ≤ eu'›
        using Attacker_Delayed monotonicity_assms local.br_conj
        by (metis (no_types, lifting) option.sel)
    qed
  next
    case (Defender_Branch p a p' Q' Qa)
    with monotonicity_assms show ?thesis
      by (cases g', auto simp del: leq_components, unfold min_1_6_subtr_simp)
        (smt (z3) enat_diff_mono mono_subtract option.discI energy.sel leq_components min.mono option.distinct(1) option.inject)+
  next
    case (Defender_Conj p Q)
    with monotonicity_assms show ?thesis
      by (cases g', simp_all del: leq_components)
        (smt (verit, ccfv_SIG) mono_subtract option.discI option.sel)
  next
    case (Defender_Stable_Conj x71 x72)
    with monotonicity_assms show ?thesis
      by (cases g', simp_all del: leq_components)
       (smt (verit, ccfv_SIG) mono_subtract option.discI option.sel)+
  qed
next
  fix g g' e e'
  assume defender_win_min_assms:
    ‹e ≤ e'›
    ‹spectroscopy_moves g g' ≠ None›
    ‹the (spectroscopy_moves g g') e' = None›
  thus
    ‹the (spectroscopy_moves g g') e = None›
  proof (cases g)
    case (Attacker_Immediate p Q)
    with defender_win_min_assms show ?thesis
      by (cases g', auto simp del: leq_components)
        (smt (verit, best) option.distinct(1) option.inject order.trans)+
  next
    case (Attacker_Branch p Q)
    with defender_win_min_assms show ?thesis
      by (cases g', auto)
        (smt (verit, best) option.distinct(1) option.inject order.trans)+
  next
    case (Attacker_Clause p q)
    hence ‹∃p' Q'. g'= (Attacker_Delayed p' Q')›
      using defender_win_min_assms(2)
      by (metis spectroscopy_defender.cases spectroscopy_moves.simps(21,52,58,62,67,72))
    hence ‹spectroscopy_moves g g' = Some min1_6 ∨ spectroscopy_moves g g' = Some (λe. Option.bind ((subtract_fn 0 0 0 0 0 0 0 1) e) min1_7)›
      using defender_win_min_assms(2) Attacker_Clause
      by (smt (verit, ccfv_threshold) spectroscopy_moves.simps(7))
    thus ?thesis
    proof safe
      assume ‹spectroscopy_moves g g' = Some min1_6›
      thus ‹the (spectroscopy_moves g g') e = None›
        using defender_win_min_assms min_1_6_some by fastforce
    next
      assume ‹spectroscopy_moves g g' = Some (λe. Option.bind (if ¬ E 0 0 0 0 0 0 0 1 ≤ e then None else Some (e - E 0 0 0 0 0 0 0 1)) min1_7)›
      thus ‹the (spectroscopy_moves g g') e = None›
        using defender_win_min_assms(1,3) bind.bind_lunit dual_order.trans min_1_7_some
        by (smt (verit, best) option.sel)
    qed
  next
    case (Attacker_Delayed p Q)
    hence ‹(∃p' Q'. g'=(Attacker_Delayed p' Q')) ∨
      (∃p' Q'. g'=(Attacker_Immediate p' Q')) ∨
      (∃p' Q'. g'=(Defender_Conj p' Q')) ∨
      (∃p' Q'. g'=(Defender_Stable_Conj p' Q')) ∨
      (∃p' p'' Q' α Qα . g'= (Defender_Branch p' α p'' Q' Qα))›
      by (metis defender_win_min_assms(2) spectroscopy_defender.cases spectroscopy_moves.simps(27,59))
    thus ?thesis
    proof (safe)
      fix p' Q'
      assume ‹g' = Attacker_Delayed p' Q'›
      hence False
        using Attacker_Delayed defender_win_min_assms(2,3) local.procrastination
        by (metis option.distinct(1) option.sel)
      thus ‹the (spectroscopy_moves g (Attacker_Delayed p' Q')) e = None› ..
    next
      fix p' Q'
      assume ‹g' = Attacker_Immediate p' Q'›
      moreover hence ‹spectroscopy_moves g g' = (subtract 1 0 0 0 0 0 0 0)›
        using Attacker_Delayed defender_win_min_assms(2,3) local.observation
        by (clarify, presburger)
      moreover hence ‹¬E 1 0 0 0 0 0 0 0 ≤ e'›
        using  defender_win_min_assms by force
      ultimately show  ‹the (spectroscopy_moves g (Attacker_Immediate p' Q')) e = None›
        using defender_win_min_assms(1) by force
    next
      fix p' Q'
      assume ‹g' = Defender_Conj p' Q'›
      hence False
        using Attacker_Delayed defender_win_min_assms(2,3) local.late_inst_conj
        by (metis option.distinct(1) option.sel)
      thus ‹the (spectroscopy_moves g (Defender_Conj p' Q')) e = None› ..
    next
      fix p' Q'
      assume ‹g' = Defender_Stable_Conj p' Q'›
      hence False
        using Attacker_Delayed defender_win_min_assms(2,3) local.late_stbl_conj
        by (metis (no_types, lifting) option.distinct(1) option.sel)
      thus ‹the (spectroscopy_moves g (Defender_Stable_Conj p' Q')) e = None› ..
    next
      fix p' p'' Q' α Qα
      assume ‹g' = Defender_Branch p' α p'' Q' Qα›
      hence False
        using Attacker_Delayed defender_win_min_assms(2,3) local.br_conj
        by (metis (no_types, lifting) option.distinct(1) option.sel)
      thus ‹the (spectroscopy_moves g (Defender_Branch p' α p'' Q' Qα)) e = None› ..
    qed
  next
    case (Defender_Branch p a p' Q' Qa)
    hence ‹(∃q'∈Q'. g' = Attacker_Clause p q')
      ∨ (∃Qa'. Qa ↦aS a Qa' ∧ g' = Attacker_Branch p' Qa')›
      using defender_win_min_assms by (cases g', auto) (metis not_None_eq)+
    hence ‹(spectroscopy_moves g g') = (subtract 0 1 1 0 0 0 0 0) ∨
      (spectroscopy_moves g g') = Some (λe. Option.bind ((subtract_fn 0 1 1 0 0 0 0 0) e) min1_6)›
      using Defender_Branch option.collapse[OF defender_win_min_assms(2)]
      by (cases g', auto)
    thus ?thesis
      using defender_win_min_assms min_1_6_some
      by (smt (verit, best) bind.bind_lunit option.distinct(1) dual_order.trans option.sel)
  next
    case (Defender_Conj p Q)
    with defender_win_min_assms show ?thesis
      by (cases g', auto)
        (smt (verit, best) option.distinct(1) option.inject order.trans)+
  next
    case (Defender_Stable_Conj x71 x72)
    with defender_win_min_assms show ?thesis
      by (cases g', simp_all del: leq_components)
         (smt (verit) dual_order.trans option.discI option.sel)+
  qed
qed

end

text ‹Now, we are able to define the weak spectroscopy game on an arbitrary (but inhabited) LTS.›
locale weak_spectroscopy_game =
  LTS_Tau step τ
  + energy_game ‹spectroscopy_moves› ‹spectroscopy_defender› ‹less_eq›
  for step :: ‹'s ⇒ 'a ⇒ 's ⇒ bool› (‹_ ↦_ _› [70, 70, 70] 80) and
      τ :: 'a

end