Theory Subsumption

section ‹Contexts and Subsumption›
text‹This theory uses contexts to extend the idea of transition subsumption from \<^cite>‹"lorenzoli2008"› to
EFSM transitions with register update functions. The \emph{subsumption in context} relation is the
main contribution of \<^cite>‹"foster2018"›.›

theory Subsumption
  imports
    "Extended_Finite_State_Machines.EFSM"
begin

definition posterior_separate :: "nat ⇒ vname gexp list ⇒ update_function list ⇒ inputs ⇒ registers ⇒ registers option" where
  "posterior_separate a g u i r = (if can_take a g i r then Some (apply_updates u (join_ir i r) r) else None)"

definition posterior :: "transition ⇒ inputs ⇒ registers ⇒ registers option" where
  "posterior t i r = posterior_separate (Arity t) (Guards t) (Updates t) i r"

definition subsumes :: "transition ⇒ registers ⇒ transition ⇒ bool" where
  "subsumes t2 r t1 = (Label t1 = Label t2 ∧ Arity t1 = Arity t2 ∧
                       (∀i. can_take_transition t1 i r ⟶ can_take_transition t2 i r) ∧
                       (∀i. can_take_transition t1 i r ⟶
                            evaluate_outputs t1 i r = evaluate_outputs t2 i r) ∧
                       (∀p1 p2 i. posterior_separate (Arity t1) (Guards t1) (Updates t2) i r = Some p2 ⟶
                                  posterior_separate (Arity t1) (Guards t1) (Updates t1) i r = Some p1 ⟶
                                  (∀P r'. (p1 $ r' = None) ∨ (P (p2 $ r') ⟶ P (p1 $ r'))))
                      )"

lemma no_functionality_subsumed:
  "Label t1 = Label t2 ⟹
   Arity t1 = Arity t2 ⟹
   ∄i. can_take_transition t1 i c ⟹
   subsumes t2 c t1"
  by (simp add: subsumes_def posterior_separate_def can_take_transition_def)

lemma subsumes_updates:
  "subsumes t2 r t1 ⟹
   can_take_transition t1 i r ⟹
   evaluate_updates t1 i r $ a = Some x ⟹
   evaluate_updates t2 i r $ a = Some x"
  apply (simp add: subsumes_def posterior_separate_def can_take_transition_def[symmetric])
  apply clarsimp
  apply (erule_tac x=i in allE)+
  apply (erule_tac x="evaluate_updates t1 i r" in allE)
  apply (erule_tac x="evaluate_updates t2 i r" in allE)
  apply (erule_tac x=i in allE)
  apply simp
  apply (simp add: all_comm[of "λP r'.
            P (evaluate_updates t2 i r $ r') ⟶ evaluate_updates t1 i r $ r' = None ∨ P (evaluate_updates t1 i r $ r')"])
  apply (erule_tac x=a in allE)
  by auto

lemma subsumption:
  "(Label t1 = Label t2 ∧ Arity t1 = Arity t2) ⟹
   (∀i. can_take_transition t1 i r ⟶ can_take_transition t2 i r) ⟹
   (∀i. can_take_transition t1 i r ⟶
        evaluate_outputs t1 i r = evaluate_outputs t2 i r) ⟹

   (∀p1 p2 i. posterior_separate (Arity t1) (Guards t1) (Updates t2) i r = Some p2 ⟶
              posterior_separate (Arity t1) (Guards t1) (Updates t1) i r = Some p1 ⟶
              (∀P r'. (p1 $ r' = None) ∨ (P (p2 $ r') ⟶ P (p1 $ r')))) ⟹
   subsumes t2 r t1"
  by (simp add: subsumes_def)

lemma bad_guards:
  "∃i. can_take_transition t1 i r ∧ ¬ can_take_transition t2 i r ⟹
   ¬ subsumes t2 r t1"
  by (simp add: subsumes_def)

lemma inconsistent_updates:
  "∃p2 p1. (∃i. posterior_separate (Arity t1) (Guards t1) (Updates t2) i r = Some p2 ∧
                posterior_separate (Arity t1) (Guards t1) (Updates t1) i r = Some p1) ∧
           (∃r' P. P (p2 $ r') ∧ (∃y. p1 $ r' = Some y) ∧ ¬ P (p1 $ r')) ⟹

    ¬ subsumes t2 r t1"
  by (metis (no_types, opaque_lifting) option.simps(3) subsumes_def)

lemma bad_outputs:
  "∃i. can_take_transition t1 i r ∧ evaluate_outputs t1 i r ≠ evaluate_outputs t2 i r ⟹
   ¬ subsumes t2 r t1"
  by (simp add: subsumes_def)

lemma no_choice_no_subsumption: "Label t = Label t' ⟹
   Arity t = Arity t' ⟹
   ¬ choice t t' ⟹
   ∃i. can_take_transition t' i c ⟹
  ¬ subsumes t c t'"
  by (meson bad_guards can_take_def can_take_transition_def choice_def)

lemma subsumption_def_alt: "subsumes t1 c t2 = (Label t2 = Label t1 ∧
    Arity t2 = Arity t1 ∧
    (∀i. can_take_transition t2 i c ⟶ can_take_transition t1 i c) ∧
    (∀i. can_take_transition t2 i c ⟶ evaluate_outputs t2 i c = evaluate_outputs t1 i c) ∧
    (∀i. can_take_transition t2 i c ⟶
         (∀r' P.
             P (evaluate_updates t1 i c $ r') ⟶
             evaluate_updates t2 i c $ r' = None ∨ P (evaluate_updates t2 i c $ r'))))"
  apply (simp add: subsumes_def posterior_separate_def can_take_transition_def[symmetric])
  by blast

lemma subsumes_update_equality:
  "subsumes t1 c t2 ⟹ (∀i. can_take_transition t2 i c ⟶
         (∀r'.
             ((evaluate_updates t1 i c $ r') = (evaluate_updates t2 i c $ r')) ∨
             evaluate_updates t2 i c $ r' = None))"
  apply (simp add: subsumption_def_alt)
  apply clarify
  subgoal for i r' y
    apply (erule_tac x=i in allE)+
    apply simp
    apply (erule_tac x=r' in allE)
    by auto
  done

text_raw‹\snip{subsumptionReflexive}{1}{2}{%›
lemma subsumes_reflexive: "subsumes t c t"
text_raw‹$\langle\isa{proof}\rangle$}%endsnip›
  by (simp add: subsumes_def)

text_raw‹\snip{subsumptionTransitive}{1}{2}{%›
lemma subsumes_transitive:
  assumes p1: "subsumes t1 c t2"
      and p2: "subsumes t2 c t3"
  shows "subsumes t1 c t3"
text_raw‹}%endsnip›
  using p1 p2
  apply (simp add: subsumes_def)
  by (metis subsumes_update_equality p1 p2 can_take_transition_def option.distinct(1) option.sel posterior_separate_def)

lemma subsumes_possible_steps_replace:
  "(s2', t2') |∈| possible_steps e2 s2 r2 l i ⟹
   subsumes t2 r2 t1 ⟹
   ((s2, s2'), t2') = ((ss2, ss2'), t1) ⟹
   (s2', t2) |∈| possible_steps (replace e2 ((ss2, ss2'), t1) ((ss2, ss2'), t2)) s2 r2 l i"
proof(induct e2)
  case empty
  then show ?case
    by (simp add: no_outgoing_transitions)
next
  case (insert x e2)
  then show ?case
    apply (simp add: fmember_possible_steps subsumes_def)
    apply standard
    apply (simp add: replace_def)
     apply auto[1]
    by (simp add: can_take)
qed

subsection‹Direct Subsumption›
text‹When merging EFSM transitions, one must \emph{account for} the behaviour of the other. The
\emph{subsumption in context} relation formalises the intuition that, in certain contexts, a
transition $t_2$ reproduces the behaviour of, and updates the data state in a manner consistent
with, another transition $t_1$, meaning that $t_2$ can be used in place of $t_1$ with no observable
difference in behaviour.

The subsumption in context relation requires us to supply a context in which to test subsumption,
but there is a problem when we try to apply this to inference: Which context should we use? The
\emph{direct subsumption} relation works at EFSM level to determine when and whether one transition
is able to account for the behaviour of another such that we can use one in place of another without
adversely effecting observable behaviour.›

text_raw‹\snip{directlySubsumes}{1}{2}{%›
definition directly_subsumes :: "transition_matrix ⇒ transition_matrix ⇒ cfstate ⇒ cfstate ⇒ transition ⇒ transition ⇒ bool" where
  "directly_subsumes e1 e2 s1 s2 t1 t2 ≡ (∀c1 c2 t. (obtains s1 c1 e1 0 <> t ∧ obtains s2 c2 e2 0 <> t) ⟶ subsumes t1 c2 t2)"
text_raw‹}%endsnip›

text_raw‹\snip{subsumesAllContexts}{1}{2}{%›
lemma subsumes_in_all_contexts_directly_subsumes:
  "(⋀c. subsumes t2 c t1) ⟹ directly_subsumes e1 e2 s s' t2 t1"
text_raw‹}%endsnip›
  by (simp add: directly_subsumes_def)

text_raw‹\snip{directSubsumption}{1}{2}{%›
lemma direct_subsumption:
  "(⋀t c1 c2. obtains s1 c1 e1 0 <> t ⟹ obtains s2 c2 e2 0 <> t ⟹ f c2) ⟹
   (⋀c. f c ⟹ subsumes t1 c t2) ⟹
   directly_subsumes e1 e2 s1 s2 t1 t2"
   text_raw‹}%endsnip›
  apply (simp add: directly_subsumes_def)
  by auto

text_raw‹\snip{obtainableNoSubsumption}{1}{2}{%›
lemma visits_and_not_subsumes:
  "(∃c1 c2 t. obtains s1 c1 e1 0 <> t ∧ obtains s2 c2 e2 0 <> t ∧ ¬ subsumes t1 c2 t2) ⟹
   ¬ directly_subsumes e1 e2 s1 s2 t1 t2"
text_raw‹}%endsnip›
  apply (simp add: directly_subsumes_def)
  by auto

text_raw‹\snip{directSubsumptionReflexive}{1}{2}{%›
lemma directly_subsumes_reflexive: "directly_subsumes e1 e2 s1 s2 t t"
text_raw‹}%endsnip›
  apply (simp add: directly_subsumes_def)
  by (simp add: subsumes_reflexive)

text_raw‹\snip{directSubsumptionTransitive}{1}{2}{%›
lemma directly_subsumes_transitive:
  assumes p1: "directly_subsumes e1 e2 s1 s2 t1 t2"
      and p2: "directly_subsumes e1 e2 s1 s2 t2 t3"
  shows "directly_subsumes e1 e2 s1 s2 t1 t3"
  text_raw‹}%endsnip›
  using p1 p2
  apply (simp add: directly_subsumes_def)
  using subsumes_transitive by blast

end