Theory Spectroscopy_Game

(* License: LGPL *)

section ‹Weak Spectroscopy Game›

theory Spectroscopy_Game
  imports Energy_Games Energy Labeled_Transition_Systems
begin

text ‹
  The weak spectroscopy game is an energy game played over an LTS.
  The attacker's moves in the weak spectroscopy game depend on the transitions of the processes and the available energy.
  Intuitively, each move type corresponds to a production in the construction of distinguishing formulas; and each attacker position to a non-terminal in the underlying grammar.
›

subsection ‹Game Rules›

datatype ('s, 'a) spectroscopy_position =
  Attacker_Immediate (attacker_state: ‹'s›) (defender_states: ‹'s set›) |
  Attacker_Delayed (attacker_state: ‹'s›) (defender_states: ‹'s set›) |
  Attacker_Conjunct (attacker_state: ‹'s›) (defender_state: ‹'s›) |
  Attacker_Branch (attacker_state: ‹'s›) (defender_states: ‹'s set›) |

  Defender_Conj (attacker_state: ‹'s›) (defender_states: ‹'s set›) |
  Defender_Stable_Conj (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›)

context lts_tau
begin

text ‹The names of moves of the weak spectroscopy game indicate the respective HML constructs they correspond to.›
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 id_up else None)› |

  procrastination:
    ‹spectroscopy_moves (Attacker_Delayed p Q) (Attacker_Delayed p' Q')
      = (if (Q' = Q ∧ p ≠ p' ∧ p ↦ τ p') then id_up 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 id_up else None)› |

  conj_answer:
    ‹spectroscopy_moves (Defender_Conj p Q) (Attacker_Conjunct 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_Conjunct 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 id_up else None)› |

  conj_s_answer:
    ‹spectroscopy_moves (Defender_Stable_Conj p Q) (Attacker_Conjunct 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 id_up
         else None)› |

  br_answer:
    ‹spectroscopy_moves (Defender_Branch p α p' Q Qα) (Attacker_Conjunct 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_Conjunct _ _) = False› |
  ‹spectroscopy_defender (Attacker_Delayed _ _) = False› |
  ‹spectroscopy_defender (Defender_Branch _ _ _ _ _) = True› |
  ‹spectroscopy_defender (Defender_Conj _ _) = True› |
  ‹spectroscopy_defender (Defender_Stable_Conj _ _) = True›

subsection ‹Energy Game Properties›

text ‹Now, we are able to define the weak spectroscopy game on an arbitrary LTS.›
sublocale weak_spectroscopy_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_Conjunct p q)
    hence ‹∃p' Q'. g'= (Attacker_Delayed p' Q')›
      using monotonicity_assms(1,2)
      by (induct, auto)
    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_Conjunct
      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α)›
      using monotonicity_assms(1)
      by (induct, auto)
    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_Conjunct p q)
    hence ‹∃p' Q'. g'= (Attacker_Delayed p' Q')›
      using defender_win_min_assms(2) by (induct, auto)
    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_Conjunct
      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α))›
      using defender_win_min_assms(2) by (induct, auto)
    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_Conjunct 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

abbreviation ‹spectro_att_wins ≡ weak_spectroscopy_game.attacker_wins›

end ― ‹of \<^locale>‹lts_tau››

end