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