# Theory FWInterrupt

```(*  Title:      JinjaThreads/Framework/FWInterrupt.thy
Author:     Andreas Lochbihler
*)

section ‹Semantics of the thread actions for interruption›

theory FWInterrupt
imports
FWState
begin

primrec redT_updI :: "'t interrupts ⇒ 't interrupt_action ⇒ 't interrupts"
where
"redT_updI is (Interrupt t) = insert t is"
| "redT_updI is (ClearInterrupt t) = is - {t}"
| "redT_updI is (IsInterrupted t b) = is"

fun redT_updIs :: "'t interrupts ⇒ 't interrupt_action list ⇒ 't interrupts"
where
"redT_updIs is [] = is"
| "redT_updIs is (ia # ias) = redT_updIs (redT_updI is ia) ias"

primrec interrupt_action_ok :: "'t interrupts ⇒ 't interrupt_action ⇒ bool"
where
"interrupt_action_ok is (Interrupt t) = True"
| "interrupt_action_ok is (ClearInterrupt t) = True"
| "interrupt_action_ok is (IsInterrupted t b) = (b = (t ∈ is))"

fun interrupt_actions_ok :: "'t interrupts ⇒ 't interrupt_action list ⇒ bool"
where
"interrupt_actions_ok is [] = True"
| "interrupt_actions_ok is (ia # ias) ⟷ interrupt_action_ok is ia ∧ interrupt_actions_ok (redT_updI is ia) ias"

primrec interrupt_action_ok' :: "'t interrupts ⇒ 't interrupt_action ⇒ bool"
where
"interrupt_action_ok' is (Interrupt t) = True"
| "interrupt_action_ok' is (ClearInterrupt t) = True"
| "interrupt_action_ok' is (IsInterrupted t b) = (b ∨ t ∉ is)"

fun interrupt_actions_ok' :: "'t interrupts ⇒ 't interrupt_action list ⇒ bool"
where
"interrupt_actions_ok' is [] = True"
| "interrupt_actions_ok' is (ia # ias) ⟷ interrupt_action_ok' is ia ∧ interrupt_actions_ok' (redT_updI is ia) ias"

fun collect_interrupt :: "'t interrupt_action ⇒ 't set ⇒ 't set"
where
"collect_interrupt (IsInterrupted t True) Ts = insert t Ts"
| "collect_interrupt (Interrupt t) Ts = Ts - {t}"
| "collect_interrupt _ Ts = Ts"

definition collect_interrupts :: "'t interrupt_action list ⇒ 't set"
where "collect_interrupts ias = foldr collect_interrupt ias {}"

lemma collect_interrupts_interrupted:
"⟦ interrupt_actions_ok is ias; t' ∈ collect_interrupts ias ⟧ ⟹ t' ∈ is"
unfolding collect_interrupts_def
proof(induct ias arbitrary: "is")
case Nil thus ?case by simp
next
case (Cons ia ias) thus ?case
by(cases "(ia, foldr collect_interrupt ias {})" rule: collect_interrupt.cases) auto
qed

lemma interrupt_actions_ok_append [simp]:
"interrupt_actions_ok is (ias @ ias') ⟷ interrupt_actions_ok is ias ∧ interrupt_actions_ok (redT_updIs is ias) ias'"
by(induct ias arbitrary: "is") auto

lemma collect_interrupt_subset: "Ts ⊆ Ts' ⟹ collect_interrupt ia Ts ⊆ collect_interrupt ia Ts'"
by(cases "(ia, Ts)" rule: collect_interrupt.cases) auto

lemma foldr_collect_interrupt_subset:
"Ts ⊆ Ts' ⟹ foldr collect_interrupt ias Ts ⊆ foldr collect_interrupt ias Ts'"

lemma interrupt_actions_ok_all_nthI:
assumes "⋀n. n < length ias ⟹ interrupt_action_ok (redT_updIs is (take n ias)) (ias ! n)"
shows "interrupt_actions_ok is ias"
using assms
proof(induct ias arbitrary: "is")
case Nil thus ?case by simp
next
case (Cons ia ias)
from Cons.prems[of 0] have "interrupt_action_ok is ia" by simp
moreover
{ fix n
assume "n < length ias"
hence "interrupt_action_ok (redT_updIs (redT_updI is ia) (take n ias)) (ias ! n)"
using Cons.prems[of "Suc n"] by simp }
hence "interrupt_actions_ok (redT_updI is ia) ias" by(rule Cons.hyps)
ultimately show ?case by simp
qed

lemma interrupt_actions_ok_nthD:
assumes "interrupt_actions_ok is ias"
and "n < length ias"
shows "interrupt_action_ok (redT_updIs is (take n ias)) (ias ! n)"
using assms
by(induct n arbitrary: "is" ias)(case_tac [!] ias, auto)

lemma interrupt_actions_ok'_all_nthI:
assumes "⋀n. n < length ias ⟹ interrupt_action_ok' (redT_updIs is (take n ias)) (ias ! n)"
shows "interrupt_actions_ok' is ias"
using assms
proof(induct ias arbitrary: "is")
case Nil thus ?case by simp
next
case (Cons ia ias)
from Cons.prems[of 0] have "interrupt_action_ok' is ia" by simp
moreover
{ fix n
assume "n < length ias"
hence "interrupt_action_ok' (redT_updIs (redT_updI is ia) (take n ias)) (ias ! n)"
using Cons.prems[of "Suc n"] by simp }
hence "interrupt_actions_ok' (redT_updI is ia) ias" by(rule Cons.hyps)
ultimately show ?case by simp
qed

lemma interrupt_actions_ok'_nthD:
assumes "interrupt_actions_ok' is ias"
and "n < length ias"
shows "interrupt_action_ok' (redT_updIs is (take n ias)) (ias ! n)"
using assms
by(induct n arbitrary: "is" ias)(case_tac [!] ias, auto)

lemma interrupt_action_ok_imp_interrupt_action_ok' [simp]:
"interrupt_action_ok is ia ⟹ interrupt_action_ok' is ia"
by(cases ia) simp_all

lemma interrupt_actions_ok_imp_interrupt_actions_ok' [simp]:
"interrupt_actions_ok is ias ⟹ interrupt_actions_ok' is ias"
by(induct ias arbitrary: "is")(simp_all)

lemma collect_interruptsE:
assumes "t' ∈ collect_interrupts ias'"
obtains n' where "n' < length ias'" "ias' ! n' = IsInterrupted t' True"
and "Interrupt t' ∉ set (take n' ias')"
proof(atomize_elim)
from assms show "∃n'<length ias'. ias' ! n' = IsInterrupted t' True ∧ Interrupt t' ∉ set (take n' ias')"
unfolding collect_interrupts_def
proof(induct ias' arbitrary: t')
case Nil thus ?case by simp
next
case (Cons ia ias) thus ?case
by(cases "(ia, foldr collect_interrupt ias {})" rule: collect_interrupt.cases) fastforce+
qed
qed

lemma collect_interrupts_prefix:
"collect_interrupts ias ⊆ collect_interrupts (ias @ ias')"
by (metis Un_empty collect_interrupts_def foldr_append foldr_collect_interrupt_subset inf_sup_ord(1) inf_sup_ord(2) subset_Un_eq)

lemma redT_updI_insert_Interrupt:
"⟦ t ∈ redT_updI is ia; t ∉ is ⟧ ⟹ ia = Interrupt t"
by(cases ia) simp_all

lemma redT_updIs_insert_Interrupt:
"⟦ t ∈ redT_updIs is ias; t ∉ is ⟧ ⟹ Interrupt t ∈ set ias"
proof(induct ias arbitrary: "is")
case Nil thus ?case by simp
next
case (Cons ia ias) thus ?case
by(cases "t ∈ redT_updI is ia")(auto dest: redT_updI_insert_Interrupt)
qed

lemma interrupt_actions_ok_takeI:
"interrupt_actions_ok is ias ⟹ interrupt_actions_ok is (take n ias)"
by(subst (asm) append_take_drop_id[symmetric, where n=n])(simp del: append_take_drop_id)

lemma interrupt_actions_ok'_collect_interrupts_imp_interrupt_actions_ok:
assumes int: "interrupt_actions_ok' is ias"
and ci: "collect_interrupts ias ⊆ is"
and int': "interrupt_actions_ok is' ias"
shows "interrupt_actions_ok is ias"
proof(rule interrupt_actions_ok_all_nthI)
fix n
assume n: "n < length ias"
show "interrupt_action_ok (redT_updIs is (take n ias)) (ias ! n)"
proof(cases "∃t. ias ! n = IsInterrupted t True")
case False
with interrupt_actions_ok'_nthD[OF int n] show ?thesis by(cases "ias ! n") simp_all
next
case True
then obtain t where ia: "ias ! n = IsInterrupted t True" ..
from int' n have "interrupt_action_ok (redT_updIs is' (take n ias)) (ias ! n)" by(rule interrupt_actions_ok_nthD)
with ia have "t ∈ redT_updIs is' (take n ias)" by simp
moreover have "ias = take (Suc n) ias @ drop (Suc n) ias" by simp
with ci have "collect_interrupts (take (Suc n) ias) ⊆ is"
by (metis collect_interrupts_prefix subset_trans)
ultimately have "t ∈ redT_updIs is (take n ias)" using n ia int int'
proof(induct n arbitrary: "is" is' ias)
case 0 thus ?case by(clarsimp simp add: neq_Nil_conv collect_interrupts_def)
next
case (Suc n)
from ‹Suc n < length ias› obtain ia ias'
where ias [simp]: "ias = ia # ias'" by(cases ias) auto
from ‹interrupt_actions_ok is' ias›
have ia_ok: "interrupt_action_ok is' ia" by simp

from ‹t ∈ redT_updIs is' (take (Suc n) ias)›
have "t ∈ redT_updIs (redT_updI is' ia) (take n ias')" by simp
moreover from ‹collect_interrupts (take (Suc (Suc n)) ias) ⊆ is› ia_ok
have "collect_interrupts (take (Suc n) ias') ⊆ redT_updI is ia"
proof(cases "(ia, is)" rule: collect_interrupt.cases)
case ("3_2" t' Ts)
hence [simp]: "ia = ClearInterrupt t'" "Ts = is" by simp_all
have "t' ∉ collect_interrupts (take (Suc n) ias')"
proof
assume "t' ∈ collect_interrupts (take (Suc n) ias')"
then obtain n' where "n' < length (take (Suc n) ias')" "take (Suc n) ias' ! n' = IsInterrupted t' True"
"Interrupt t' ∉ set (take n' (take (Suc n) ias'))" by(rule collect_interruptsE)
hence "n' ≤ n" "ias' ! n' = IsInterrupted t' True" "Interrupt t' ∉ set (take n' ias')"
using ‹Suc n < length ias› by(simp_all add: min_def split: if_split_asm)
hence "Suc n' < length ias" using ‹Suc n < length ias› by(simp add: min_def)
with ‹interrupt_actions_ok is' ias›
have "interrupt_action_ok (redT_updIs is' (take (Suc n') ias)) (ias ! Suc n')"
by(rule interrupt_actions_ok_nthD)
with ‹Suc n < length ias› ‹ias' ! n' = IsInterrupted t' True›
have "t' ∈ redT_updIs (is' - {t'}) (take n' ias')" by simp
hence "Interrupt t' ∈ set (take n' ias')"
by(rule redT_updIs_insert_Interrupt) simp
with ‹Interrupt t' ∉ set (take n' ias')› show False by contradiction
qed
thus ?thesis using ‹collect_interrupts (take (Suc (Suc n)) ias) ⊆ is›
moreover from ‹Suc n < length ias› have "n < length ias'" by simp
moreover from ‹ias ! Suc n = IsInterrupted t True› have "ias' ! n = IsInterrupted t True" by simp
moreover from ‹interrupt_actions_ok' is ias› have "interrupt_actions_ok' (redT_updI is ia) ias'"
unfolding ias by simp
moreover from ‹interrupt_actions_ok is' ias› have "interrupt_actions_ok (redT_updI is' ia) ias'" by simp
ultimately have "t ∈ redT_updIs (redT_updI is ia) (take n ias')" by(rule Suc)
thus ?case by simp
qed
thus ?thesis unfolding ia by simp
qed
qed

end
```