# Theory Drinks_Subsumption

```subsection‹Example›
text‹This theory shows how contexts can be used to prove transition subsumption.›
theory Drinks_Subsumption
imports "Extended_Finite_State_Machine_Inference.Subsumption" "Extended_Finite_State_Machines.Drinks_Machine_2"
begin

lemma stop_at_3: "¬obtains 1 c drinks2 3 r t"
proof(induct t arbitrary: r)
case Nil
then show ?case
next
case (Cons a t)
then show ?case
apply (case_tac a)
apply clarify
qed

lemma no_1_2: "¬obtains 1 c drinks2 2 r t"
proof(induct t arbitrary: r)
case Nil
then show ?case
next
case (Cons a t)
then show ?case
apply (case_tac a)
apply clarify
apply clarsimp
apply (erule disjE)
apply simp
apply (erule disjE)
apply simp
qed

lemma no_change_1_1: "obtains 1 c drinks2 1 r t ⟹ c = r"
proof(induct t)
case Nil
then show ?case
next
case (Cons a t)
then show ?case
apply (case_tac a)
apply clarify
apply clarsimp
apply (erule disjE)
qed

lemma obtains_1: "obtains 1 c drinks2 0 <> t ⟹ c \$ 2 = Some (Num 0)"
proof(induct t)
case Nil
then show ?case
next
case (Cons a t)
then show ?case
apply (case_tac a)
apply clarify
using no_change_1_1 by fastforce
qed

lemma obtains_1_1_2:
"obtains 1 c1 drinks2 1 r t ⟹
obtains 1 c2 drinks 1 r t ⟹
c1 = r ∧ c2 = r"
proof(induct t arbitrary: r)
case Nil
then show ?case
next
case (Cons a t)
then show ?case
apply (case_tac a)
apply clarify
apply clarsimp
apply safe
using Cons.prems(1) no_change_1_1 apply blast
using Cons.prems(1) no_change_1_1 apply blast
using Cons.prems(1) no_change_1_1 apply blast
apply (metis drinks_rejects_future numeral_eq_one_iff obtains.cases obtains_recognises semiring_norm(85))
using no_1_2 apply blast
using no_1_2 apply blast
using Cons.prems(1) no_change_1_1 apply blast
using no_1_2 apply blast
using no_1_2 apply blast
using no_1_2 by blast
qed

lemma obtains_1_c2:
"obtains 1 c1 drinks2 0 <> t ⟹ obtains 1 c2 drinks 0 <> t ⟹ c2 \$ 2 = Some (Num 0)"
proof(induct t)
case Nil
then show ?case
next
case (Cons a t)
then show ?case
apply (case_tac a)
apply clarify
apply clarsimp
using obtains_1_1_2 by fastforce
qed

lemma directly_subsumes: "directly_subsumes drinks2 drinks 1 1 vend_fail vend_nothing"
apply (rule direct_subsumption[of _ _ _ _ "λc2. c2 \$ 2 = Some (Num 0)"])
apply (rule subsumption)
apply (simp add: vend_fail_def vend_nothing_def can_take value_gt_true)