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'"
by(induct ias)(simp_all add: collect_interrupt_subset)

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›
          by(auto simp add: collect_interrupts_def)
      qed(auto simp add: collect_interrupts_def)
      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