(* 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