# 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)

"∃i. can_take_transition t1 i r ∧ evaluate_outputs t1 i r ≠ evaluate_outputs t2 i r ⟹
¬ subsumes t2 r t1"

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 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›

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
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
next
case (insert x e2)
then show ?case
apply standard
apply auto[1]
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

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›

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›
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›
by auto

text_raw‹\snip{directSubsumptionReflexive}{1}{2}{%›
lemma directly_subsumes_reflexive: "directly_subsumes e1 e2 s1 s2 t t"
text_raw‹}%endsnip›