# Theory Set_without_equal

(*  Title:      JinjaThreads/Basic/Set_without_equal.thy
Author:     Andreas Lochbihler
*)

theory Set_without_equal
imports Main
begin

text ‹
Adapt @{type "set"} code setup such that @{const "insert"},
@{const "union"}, and @{term "set_of_pred"} do not generate
sort constraint @{class equal}.
›

definition insert' :: "'a ⇒ 'a set ⇒ 'a set"
where "insert' = Set.insert"

definition union' :: "'a set ⇒ 'a set ⇒ 'a set"
where "union' A B = sup A B"

declare
insert'_def [symmetric, code_unfold]
union'_def [symmetric, code_unfold]

lemma insert'_code:
"insert' x (set xs) = set (x # xs)"
by (rule set_eqI) (simp add: insert'_def)

lemma union'_code:
"union' (set xs) (set ys) = set (xs @ ys)"
by (rule set_eqI) (simp add: union'_def fun_eq_iff)

declare
insert'_code [code]
union'_code [code]

text ‹Merge name spaces to avoid cyclic module dependencies›

code_identifier
code_module Set_without_equal ⇀
(SML) Set and (Haskell) Set and (OCaml) Set

end



theory Set_Monad
imports
Main
begin

lemma member_SUP: (* FIXME delete candidate: should be subsumed by default simpset as soon as SUP_apply is included *)
"x ∈ ⋃(f  A) = (SUP B∈A. (λx. x ∈ f B)) x"
by auto

abbreviation (input) "of_pred == Predicate.set_of_pred" (* FIXME delte alias *)
abbreviation (input) "of_seq == Predicate.set_of_seq" (* FIXME delte alias *)

lemmas bind_def = Set.bind_def (* FIXME delte alias *)
lemmas bind_bind = Set.bind_bind (* FIXME delte alias *)
lemmas empty_bind = Set.empty_bind (* FIXME delte alias *)
lemmas bind_const = Set.bind_const (* FIXME delte alias *)
lemmas member_of_pred = Predicate.member_set_of_pred (* FIXME delte alias *)
lemmas member_of_seq = Predicate.member_set_of_seq (* FIXME delte alias *)

definition single :: "'a ⇒ 'a set"
where "single a = {a}"

definition undefined :: "'a set"
where [simp]: "undefined = Collect HOL.undefined"

declare [[code abort: undefined]]

definition Undefined :: "unit ⇒ 'a set"
where "Undefined _ = Collect HOL.undefined"

declare [[code abort: Undefined]]

lemma undefined_code [code_unfold]:
"undefined = Undefined ()"

lemma bind_single [simp, code_unfold]:
"A ⤜ single = A"

lemma single_bind [simp, code_unfold]:
"single a ⤜ B = B a"

declare Set.empty_bind [code_unfold]

lemma member_single [simp]:
"x ∈ single a ⟷ x = a"

lemma single_sup_simps [simp, code_unfold]:
shows single_sup: "sup (single a) A = insert a A"
and sup_single: "sup A (single a) = insert a A"
by (unfold set_eq_iff) auto

lemma single_code [code]:
"single a = set [a]"

end


# Theory JT_ICF

section ‹Adapting the Isabelle Collection Framework for Jinja Threads›
theory JT_ICF
imports Collections.CollectionsV1
begin

text ‹Hide stuff that may lead to confusions later›

hide_const (open) Array
hide_type (open) array

end


# Theory Auxiliary

(*  Title:      JinjaThreads/Basic/Aux.thy
Author:     Andreas Lochbihler, David von Oheimb, Tobias Nipkow

Based on the Jinja theory Common/Aux.thy by David von Oheimb and Tobias Nipkow
*)

section ‹Auxiliary Definitions and Lemmata›

theory Auxiliary
imports
Complex_Main
"HOL-Library.Transitive_Closure_Table"
"HOL-Library.Predicate_Compile_Alternative_Defs"
"HOL-Library.Infinite_Set"
FinFun.FinFun
begin

unbundle finfun_syntax

(* FIXME move and possibly turn into a general simproc *)
"((n::nat) + max i j ≤ m) = (n + i ≤ m ∧ n + j ≤ m)"
(*<*)by arith(*>*)

"(Suc(n + max i j) ≤ m) = (Suc(n + i) ≤ m ∧ Suc(n + j) ≤ m)"
(*<*)by arith(*>*)

lemma less_min_eq1:
"(a :: 'a :: order) < b ⟹ min a b = a"

lemma less_min_eq2:
"(a :: 'a :: order) > b ⟹ min a b = b"

no_notation floor ("⌊_⌋")
notation Some ("(⌊_⌋)")

(*<*)
declare
option.splits[split]
Let_def[simp]
subset_insertI2 [simp]
(*>*)

declare not_Cons_self [no_atp]

lemma Option_bind_eq_None_conv:
"x ⤜ y = None ⟷ x = None ∨ (∃x'. x = Some x' ∧ y x' = None)"
by(cases x) simp_all

lemma Option_bind_eq_Some_conv:
"x ⤜ y = Some z ⟷ (∃x'. x = Some x' ∧ y x' = Some z)"
by(cases x) simp_all

lemma map_upds_xchg_snd:
"⟦ length xs ≤ length ys; length xs ≤ length zs; ∀i. i < length xs ⟶ ys ! i = zs ! i ⟧
⟹ f(xs [↦] ys) = f(xs [↦] zs)"
proof(induct xs arbitrary: ys zs f)
case Nil thus ?case by simp
next
case (Cons x xs)
note IH = ‹⋀f ys zs. ⟦ length xs ≤ length ys; length xs ≤ length zs; ∀i<length xs. ys ! i = zs ! i⟧
⟹ f(xs [↦] ys) = f(xs [↦] zs)›
note leny = ‹length (x # xs) ≤ length ys›
note lenz = ‹length (x # xs) ≤ length zs›
note nth = ‹∀i<length (x # xs). ys ! i = zs ! i›
from lenz obtain z zs' where zs [simp]: "zs = z # zs'" by(cases zs, auto)
from leny obtain y ys' where ys [simp]: "ys = y # ys'" by(cases ys, auto)
from lenz leny nth have "(f(x ↦ y))(xs [↦] ys') = (f(x ↦ y))(xs [↦] zs')"
by-(rule IH, auto)
moreover from nth have "y = z" by auto
ultimately show ?case by(simp add: map_upds_def)
qed

subsection ‹‹distinct_fst››

definition
distinct_fst  :: "('a × 'b) list ⇒ bool"
where
"distinct_fst  ≡  distinct ∘ map fst"

lemma distinct_fst_Nil [simp]:
"distinct_fst []"
(*<*)
apply (unfold distinct_fst_def)
apply (simp (no_asm))
done
(*>*)

lemma distinct_fst_Cons [simp]:
"distinct_fst ((k,x)#kxs) = (distinct_fst kxs ∧ (∀y. (k,y) ∉ set kxs))"
(*<*)
apply (unfold distinct_fst_def)
apply (auto simp:image_def)
done
(*>*)

lemma distinct_fstD: "⟦ distinct_fst xs; (x, y) ∈ set xs; (x, z) ∈ set xs ⟧ ⟹ y = z"
by(induct xs) auto

lemma map_of_SomeI:
"⟦ distinct_fst kxs; (k,x) ∈ set kxs ⟧ ⟹ map_of kxs k = Some x"
(*<*)by (induct kxs) (auto simp:fun_upd_apply)(*>*)

lemma rel_option_Some1:
"rel_option R (Some x) y ⟷ (∃y'. y = Some y' ∧ R x y')"
by(cases y) simp_all

lemma rel_option_Some2:
"rel_option R x (Some y) ⟷ (∃x'. x = Some x' ∧ R x' y)"
by(cases x) simp_all

subsection ‹Using @{term list_all2} for relations›

definition
fun_of :: "('a × 'b) set ⇒ 'a ⇒ 'b ⇒ bool"
where
"fun_of S ≡ λx y. (x,y) ∈ S"

text ‹Convenience lemmas›
(*<*)
declare fun_of_def [simp]
(*>*)
lemma rel_list_all2_Cons [iff]:
"list_all2 (fun_of S) (x#xs) (y#ys) =
((x,y) ∈ S ∧ list_all2 (fun_of S) xs ys)"
(*<*)by simp(*>*)

lemma rel_list_all2_Cons1:
"list_all2 (fun_of S) (x#xs) ys =
(∃z zs. ys = z#zs ∧ (x,z) ∈ S ∧ list_all2 (fun_of S) xs zs)"
(*<*)by (cases ys) auto(*>*)

lemma rel_list_all2_Cons2:
"list_all2 (fun_of S) xs (y#ys) =
(∃z zs. xs = z#zs ∧ (z,y) ∈ S ∧ list_all2 (fun_of S) zs ys)"
(*<*)by (cases xs) auto(*>*)

lemma rel_list_all2_refl:
"(⋀x. (x,x) ∈ S) ⟹ list_all2 (fun_of S) xs xs"

lemma rel_list_all2_antisym:
"⟦ (⋀x y. ⟦(x,y) ∈ S; (y,x) ∈ T⟧ ⟹ x = y);
list_all2 (fun_of S) xs ys; list_all2 (fun_of T) ys xs ⟧ ⟹ xs = ys"
(*<*)by (rule list_all2_antisym) auto(*>*)

lemma rel_list_all2_trans:
"⟦ ⋀a b c. ⟦(a,b) ∈ R; (b,c) ∈ S⟧ ⟹ (a,c) ∈ T;
list_all2 (fun_of R) as bs; list_all2 (fun_of S) bs cs⟧
⟹ list_all2 (fun_of T) as cs"
(*<*)by (rule list_all2_trans) auto(*>*)

lemma rel_list_all2_update_cong:
"⟦ i<size xs; list_all2 (fun_of S) xs ys; (x,y) ∈ S ⟧
⟹ list_all2 (fun_of S) (xs[i:=x]) (ys[i:=y])"

lemma rel_list_all2_nthD:
"⟦ list_all2 (fun_of S) xs ys; p < size xs ⟧ ⟹ (xs!p,ys!p) ∈ S"
(*<*)by (drule list_all2_nthD) auto(*>*)

lemma rel_list_all2I:
"⟦ length a = length b; ⋀n. n < length a ⟹ (a!n,b!n) ∈ S ⟧ ⟹ list_all2 (fun_of S) a b"
(*<*)by (erule list_all2_all_nthI) simp(*>*)

(*<*)declare fun_of_def [simp del](*>*)

lemma list_all2_induct[consumes 1, case_names Nil Cons]:
assumes major: "list_all2 P xs ys"
and Nil: "Q [] []"
and Cons: "⋀x xs y ys. ⟦ P x y; list_all2 P xs ys; Q xs ys ⟧ ⟹ Q (x # xs) (y # ys)"
shows "Q xs ys"
using major
by(induct xs arbitrary: ys)(auto simp add: list_all2_Cons1 Nil intro!: Cons)

lemma list_all2_split:
assumes major: "list_all2 P xs ys"
and split: "⋀x y. P x y ⟹ ∃z. Q x z ∧ R z y"
shows "∃zs. list_all2 Q xs zs ∧ list_all2 R zs ys"
using major
by(induct rule: list_all2_induct)(auto dest: split)

lemma list_all2_refl_conv:
"list_all2 P xs xs ⟷ (∀x∈set xs. P x x)"
unfolding list_all2_conv_all_nth Ball_def in_set_conv_nth
by auto

lemma list_all2_op_eq [simp]:
"list_all2 (=) xs ys ⟷ xs = ys"
by(induct xs arbitrary: ys)(auto simp add: list_all2_Cons1)

lemmas filter_replicate_conv = filter_replicate

lemma length_greater_Suc_0_conv: "Suc 0 < length xs ⟷ (∃x x' xs'. xs = x # x' # xs')"
by(cases xs, auto simp add: neq_Nil_conv)

lemmas zip_same_conv = zip_same_conv_map

lemma nth_Cons_subtract: "0 < n ⟹ (x # xs) ! n = xs ! (n - 1)"
by(auto simp add: nth_Cons split: nat.split)

lemma f_nth_set:
"⟦ f (xs ! n) = v; n < length xs ⟧ ⟹ v ∈ f  set xs"
unfolding set_conv_nth by auto

lemma nth_concat_eqI:
"⟦ n = sum_list (map length (take i xss)) + k; i < length xss; k < length (xss ! i); x = xss ! i ! k ⟧
⟹ concat xss ! n = x"
apply(induct xss arbitrary: n i k)
apply simp
apply simp
apply(case_tac i)
done

lemma replicate_eq_append_conv:
"(replicate n x = xs @ ys) = (∃m≤n. xs = replicate m x ∧ ys = replicate (n-m) x)"
proof(induct n arbitrary: xs ys)
case 0 thus ?case by simp
next
case (Suc n xs ys)
have IH: "⋀xs ys. (replicate n x = xs @ ys) = (∃m≤n. xs = replicate m x ∧ ys = replicate (n - m) x)" by fact
show ?case
proof(unfold replicate_Suc, rule iffI)
assume a: "x # replicate n x = xs @ ys"
show "∃m≤Suc n. xs = replicate m x ∧ ys = replicate (Suc n - m) x"
proof(cases xs)
case Nil
thus ?thesis using a
by(auto)
next
case (Cons X XS)
with a have x: "x = X" and "replicate n x = XS @ ys" by auto
hence "∃m≤n. XS = replicate m x ∧ ys = replicate (n - m) x"
by -(rule IH[THEN iffD1])
then obtain m where "m ≤ n" and XS: "XS = replicate m x" and ys: "ys = replicate (n - m) x" by blast
with x Cons show ?thesis
by(fastforce)
qed
next
assume "∃m≤Suc n. xs = replicate m x ∧ ys = replicate (Suc n - m) x"
then obtain m where m: "m ≤ Suc n" and xs: "xs = replicate m x" and ys: "ys = replicate (Suc n - m) x" by blast
thus "x # replicate n x = xs @ ys"
qed
qed

lemma replicate_Suc_snoc:
"replicate (Suc n) x = replicate n x @ [x]"
by (metis replicate_Suc replicate_append_same)

lemma map_eq_append_conv:
"map f xs = ys @ zs ⟷ (∃ys' zs'. map f ys' = ys ∧ map f zs' = zs ∧ xs = ys' @ zs')"
apply(rule iffI)
apply(metis append_eq_conv_conj append_take_drop_id drop_map take_map)
by(clarsimp)

lemma append_eq_map_conv:
"ys @ zs = map f xs ⟷ (∃ys' zs'. map f ys' = ys ∧ map f zs' = zs ∧ xs = ys' @ zs')"
unfolding map_eq_append_conv[symmetric]
by auto

lemma map_eq_map_conv:
"map f xs = map g ys ⟷ list_all2 (λx y. f x = g y) xs ys"
apply(induct xs arbitrary: ys)
done

lemma map_eq_all_nth_conv:
"map f xs = ys ⟷ length xs = length ys ∧ (∀n < length xs. f (xs ! n) = ys ! n)"
apply(induct xs arbitrary: ys)
apply(fastforce simp add: nth_Cons Suc_length_conv split: nat.splits)+
done

lemma take_eq_take_le_eq:
"⟦ take n xs = take n ys; m ≤ n ⟧ ⟹ take m xs = take m ys"
by(metis min.absorb_iff1 take_take)

lemma take_list_update_beyond:
"n ≤ m ⟹ take n (xs[m := x]) = take n xs"
by(cases "n ≤ length xs")(rule nth_take_lemma, simp_all)

lemma hd_drop_conv_nth:
"n < length xs ⟹ hd (drop n xs) = xs ! n"
by(rule hd_drop_conv_nth) (metis list.size(3) not_less0)

lemma set_tl_subset: "set (tl xs) ⊆ set xs"
by(cases xs) auto

lemma tl_conv_drop: "tl xs = drop 1 xs"
by(cases xs) simp_all

lemma takeWhile_eq_Nil_dropWhile_eq_Nil_imp_Nil:
"⟦ takeWhile P xs = []; dropWhile P xs = [] ⟧ ⟹ xs = []"
by (metis dropWhile_eq_drop drop_0 list.size(3))

lemma takeWhile_eq_Nil_conv:
"takeWhile P xs = [] ⟷ (xs = [] ∨ ¬ P (hd xs))"
by(cases xs) simp_all

lemma dropWhile_append1': "dropWhile P xs ≠ [] ⟹ dropWhile P (xs @ ys) = dropWhile P xs @ ys"
by(cases xs) auto

lemma dropWhile_append2': "dropWhile P xs = [] ⟹ dropWhile P (xs @ ys) = dropWhile P ys"
by(simp)

lemma takeWhile_append1': "dropWhile P xs ≠ [] ⟹ takeWhile P (xs @ ys) = takeWhile P xs"
by auto

lemma takeWhile_takeWhile: "takeWhile P (takeWhile Q xs) = takeWhile (λx. P x ∧ Q x) xs"
by(induct xs) simp_all

lemma dropWhile_eq_ConsD:
"dropWhile P xs = y # ys ⟹ y ∈ set xs ∧ ¬ P y"
by(induct xs)(auto split: if_split_asm)

lemma dropWhile_eq_hd_conv: "dropWhile P xs = hd xs # rest ⟷ xs ≠ [] ∧ rest = tl xs ∧ ¬ P (hd xs)"
by (metis append_Nil append_is_Nil_conv dropWhile_eq_Cons_conv list.sel(1) neq_Nil_conv takeWhile_dropWhile_id takeWhile_eq_Nil_conv list.sel(3))

lemma dropWhile_eq_same_conv: "dropWhile P xs = xs ⟷ (xs = [] ∨ ¬ P (hd xs))"
by (metis dropWhile.simps(1) eq_Nil_appendI hd_dropWhile takeWhile_dropWhile_id takeWhile_eq_Nil_conv)

lemma subset_code [code_unfold]:
"set xs ⊆ set ys ⟷ (∀x ∈ set xs. x ∈ set ys)"
by(rule Set.subset_eq)

lemma eval_bot [simp]:
"Predicate.eval bot = (λ_. False)"

lemma not_is_emptyE:
assumes "¬ Predicate.is_empty P"
obtains x where "Predicate.eval P x"
using assms
by(fastforce simp add: Predicate.is_empty_def bot_pred_def intro!: pred_iffI)

lemma is_emptyD:
assumes "Predicate.is_empty P"
shows "Predicate.eval P x ⟹ False"
using assms
by(simp add: Predicate.is_empty_def bot_pred_def bot_apply Set.empty_def)

lemma eval_bind_conv:
"Predicate.eval (P ⤜ R) y = (∃x. Predicate.eval P x ∧ Predicate.eval (R x) y)"
by(blast elim: bindE intro: bindI)

lemma eval_single_conv: "Predicate.eval (Predicate.single a) b ⟷ a = b"
by(blast intro: singleI elim: singleE)

lemma conj_asm_conv_imp:
"(A ∧ B ⟹ PROP C) ≡ (A ⟹ B ⟹ PROP C)"
apply(rule equal_intr_rule)
apply(erule meta_mp)
apply(erule (1) conjI)
apply(erule meta_impE)
apply(erule conjunct1)
apply(erule meta_mp)
apply(erule conjunct2)
done

lemma meta_all_eq_conv: "(⋀a. a = b ⟹ PROP P a) ≡ PROP P b"
apply(rule equal_intr_rule)
apply(erule meta_allE)
apply(erule meta_mp)
apply(rule refl)
apply(hypsubst)
apply assumption
done

lemma meta_all_eq_conv2: "(⋀a. b = a ⟹ PROP P a) ≡ PROP P b"
apply(rule equal_intr_rule)
apply(erule meta_allE)
apply(erule meta_mp)
apply(rule refl)
apply(hypsubst)
apply assumption
done

lemma disj_split:
"P (a ∨ b) ⟷ (a ⟶ P True) ∧ (b ⟶ P True) ∧ (¬ a ∧ ¬ b ⟶ P False)"
apply(cases a)
apply(case_tac [!] b)
apply auto
done

lemma disj_split_asm:
"P (a ∨ b) ⟷ ¬ (a ∧ ¬ P True ∨ b ∧ ¬ P True ∨ ¬ a ∧ ¬ b ∧ ¬ P False)"
done

lemma disjCE:
assumes "P ∨ Q"
obtains P | "Q" "¬ P"
using assms by blast

lemma case_option_conv_if:
"(case v of None ⇒ f | Some x ⇒ g x) = (if ∃a. v = Some a then g (the v) else f)"
by(simp)

lemma LetI: "(⋀x. x = t ⟹ P x) ⟹ let x = t in P x"
by(simp)

(* rearrange parameters and premises to allow application of one-point-rules *)
(* adapted from Tools/induct.ML and Isabelle Developer Workshop 2010 *)

simproc_setup rearrange_eqs ("Pure.all t") = ‹
let
fun swap_params_conv ctxt i j cv =
let
fun conv1 0 ctxt = Conv.forall_conv (cv o snd) ctxt
| conv1 k ctxt =
Conv.rewr_conv @{thm swap_params} then_conv
Conv.forall_conv (conv1 (k - 1) o snd) ctxt
fun conv2 0 ctxt = conv1 j ctxt
| conv2 k ctxt = Conv.forall_conv (conv2 (k - 1) o snd) ctxt
in conv2 i ctxt end;

fun swap_prems_conv 0 = Conv.all_conv
| swap_prems_conv i =
Conv.implies_concl_conv (swap_prems_conv (i - 1)) then_conv
Conv.rewr_conv Drule.swap_prems_eq;

fun find_eq ctxt t =
let
val l = length (Logic.strip_params t);
val Hs = Logic.strip_assums_hyp t;
fun find (i, (_ $(Const ("HOL.eq", _)$ Bound j $_))) = SOME (i, j) | find (i, (_$ (Const ("HOL.eq", _) $_$ Bound j))) = SOME (i, j)
| find _ = NONE
in
(case get_first find (map_index I Hs) of
NONE => NONE
| SOME (0, 0) => NONE
| SOME (i, j) => SOME (i, l - j - 1, j))
end;

fun mk_swap_rrule ctxt ct =
(case find_eq ctxt (Thm.term_of ct) of
NONE => NONE
| SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct))
in
fn _ => mk_swap_rrule
end
›
declare [[simproc del: rearrange_eqs]]
lemmas meta_onepoint = meta_all_eq_conv meta_all_eq_conv2

lemma meta_all2_eq_conv: "(⋀a b. a = c ⟹ PROP P a b) ≡ (⋀b. PROP P c b)"
apply(rule equal_intr_rule)
apply(erule meta_allE)+
apply(erule meta_mp)
apply(rule refl)
apply(erule meta_allE)
apply simp
done

lemma meta_all3_eq_conv: "(⋀a b c. a = d ⟹ PROP P a b c) ≡ (⋀b c. PROP P d b c)"
apply(rule equal_intr_rule)
apply(erule meta_allE)+
apply(erule meta_mp)
apply(rule refl)
apply(erule meta_allE)+
apply simp
done

lemma meta_all4_eq_conv: "(⋀a b c d. a = e ⟹ PROP P a b c d) ≡ (⋀b c d. PROP P e b c d)"
apply(rule equal_intr_rule)
apply(erule meta_allE)+
apply(erule meta_mp)
apply(rule refl)
apply(erule meta_allE)+
apply simp
done

lemma meta_all5_eq_conv: "(⋀a b c d e. a = f ⟹ PROP P a b c d e) ≡ (⋀b c d e. PROP P f b c d e)"
apply(rule equal_intr_rule)
apply(erule meta_allE)+
apply(erule meta_mp)
apply(rule refl)
apply(erule meta_allE)+
apply simp
done

lemma inj_on_image_mem_iff:
"⟦ inj_on f A; B ⊆ A; a ∈ A ⟧ ⟹ f a ∈ f  B ⟷ a ∈ B"
by(metis inv_into_f_eq inv_into_image_cancel rev_image_eqI)

lemma sum_hom:
assumes hom_add [simp]: "⋀a b. f (a + b) = f a + f b"
and hom_0 [simp]: "f 0 = 0"
shows "sum (f ∘ h) A = f (sum h A)"
proof(cases "finite A")
case False thus ?thesis by simp
next
case True thus ?thesis
by(induct) simp_all
qed

"a ≤ b ⟹ sum f {..<(a :: nat)} + sum f {a..<b} = sum f {..<b}"
by (metis atLeast0LessThan le0 sum.atLeastLessThan_concat)

lemma nat_fun_sum_eq_conv:
fixes f :: "'a ⇒ nat"
shows "(λa. f a + g a) = (λa. 0) ⟷ f = (λa .0) ∧ g = (λa. 0)"

lemma in_ran_conv: "v ∈ ran m ⟷ (∃k. m k = Some v)"

lemma map_le_dom_eq_conv_eq:
"⟦ m ⊆⇩m m'; dom m = dom m' ⟧ ⟹ m = m'"
by (metis map_le_antisym map_le_def)

lemma map_leI:
"(⋀k v. f k = Some v ⟹ g k = Some v) ⟹ f ⊆⇩m g"
unfolding map_le_def by auto

lemma map_le_SomeD: "⟦ m ⊆⇩m m'; m x = ⌊y⌋ ⟧ ⟹ m' x = ⌊y⌋"
by(auto simp add: map_le_def dest: bspec)

lemma map_le_same_upd:
"f x = None ⟹ f ⊆⇩m f(x ↦ y)"

lemma map_upd_map_add: "X(V ↦ v) = (X ++ [V ↦ v])"
by(simp)

lemma foldr_filter_conv:
"foldr f (filter P xs) = foldr (λx s. if P x then f x s else s) xs"
by(induct xs)(auto intro: ext)

lemma foldr_insert_conv_set:
"foldr insert xs A = A ∪ set xs"
by(induct xs arbitrary: A) auto

lemma snd_o_Pair_conv_id: "snd o Pair a = id"

lemma if_intro:
"⟦ P ⟹ A; ¬ P ⟹ B ⟧ ⟹ if P then A else B"
by(auto)

lemma ex_set_conv: "(∃x. x ∈ set xs) ⟷ xs ≠ []"
apply(auto)
done

lemma subset_Un1: "A ⊆ B ⟹ A ⊆ B ∪ C" by blast
lemma subset_Un2: "A ⊆ C ⟹ A ⊆ B ∪ C" by blast
lemma subset_insert: "A ⊆ B ⟹ A ⊆ insert a B" by blast
lemma UNION_subsetD: "⟦ (⋃x∈A. f x) ⊆ B; a ∈ A ⟧ ⟹ f a ⊆ B" by blast

lemma Collect_eq_singleton_conv:
"{a. P a} = {a} ⟷ P a ∧ (∀a'. P a' ⟶ a = a')"
by(auto)

lemma Collect_conv_UN_singleton: "{f x|x. x ∈ P} = (⋃x∈P. {f x})"
by blast

lemma if_else_if_else_eq_if_else [simp]:
"(if b then x else if b then y else z) = (if b then x else z)"
by(simp)

lemma rec_prod_split [simp]: "old.rec_prod = case_prod"

lemma inj_Pair_snd [simp]: "inj (Pair x)"
by(rule injI) auto

lemma rtranclp_False [simp]: "(λa b. False)⇧*⇧* = (=)"
by(auto simp add: fun_eq_iff elim: rtranclp_induct)

lemmas rtranclp_induct3 =
rtranclp_induct[where a="(ax, ay, az)" and b="(bx, by, bz)", split_rule, consumes 1, case_names refl step]

lemmas tranclp_induct3 =
tranclp_induct[where a="(ax, ay, az)" and b="(bx, by, bz)", split_rule, consumes 1, case_names refl step]

lemmas rtranclp_induct4 =
rtranclp_induct[where a="(ax, ay, az, aw)" and b="(bx, by, bz, bw)", split_rule, consumes 1, case_names refl step]

lemmas tranclp_induct4 =
tranclp_induct[where a="(ax, ay, az, aw)" and b="(bx, by, bz, bw)", split_rule, consumes 1, case_names refl step]

lemmas converse_tranclp_induct2 =
converse_tranclp_induct [of _ "(ax,ay)" "(bx,by)", split_rule,
consumes 1, case_names base step]

lemma wfP_induct' [consumes 1, case_names wfP]:
"⟦wfP r; ⋀x. (⋀y. r y x ⟹ P y) ⟹ P x⟧ ⟹ P a"
by(blast intro: wfP_induct)

lemma wfP_induct2 [consumes 1, case_names wfP]:
"⟦wfP r; ⋀x x'. (⋀y y'. r (y, y') (x, x') ⟹ P y y') ⟹ P x x' ⟧ ⟹ P x x'"
by(drule wfP_induct'[where P="λ(x, y). P x y"]) blast+

lemma wfP_minimalE:
assumes "wfP r"
and "P x"
obtains z where "P z" "r^** z x" "⋀y. r y z ⟹ ¬ P y"
proof -
let ?Q = "λx'. P x' ∧ r^** x' x"
from ‹P x› have "?Q x" by blast
from ‹wfP r› have "⋀Q. x ∈ Q ⟶ (∃z∈Q. ∀y. r y z ⟶ y ∉ Q)"
unfolding wfP_eq_minimal by blast
from this[rule_format, of "Collect ?Q"] ‹?Q x›
obtain z where "?Q z" and min: "⋀y. r y z ⟹ ¬ ?Q y" by auto
from ‹?Q z› have "P z" "r^** z x" by auto
moreover
{ fix y
assume "r y z"
hence "¬ ?Q y" by(rule min)
moreover from ‹r y z› ‹r^** z x› have "r^** y x"
by(rule converse_rtranclp_into_rtranclp)
ultimately have "¬ P y" by blast }
ultimately show thesis ..
qed

lemma coinduct_set_wf [consumes 3, case_names coinduct, case_conclusion coinduct wait step]:
assumes "mono f" "wf r" "(a, b) ∈ X"
and step: "⋀x b. (x, b) ∈ X ⟹ (∃b'. (b', b) ∈ r ∧ (x, b') ∈ X) ∨ (x ∈ f (fst  X ∪ gfp f))"
shows "a ∈ gfp f"
proof -
from ‹(a, b) ∈ X› have "a ∈ fst  X" by(auto intro: rev_image_eqI)
moreover
{ fix a b
assume "(a, b) ∈ X"
with ‹wf r› have "a ∈ f (fst  X ∪ gfp f)"
by(induct)(blast dest: step) }
hence "fst  X ⊆ f (fst  X ∪ gfp f)" by(auto)
ultimately show ?thesis by(rule coinduct_set[OF ‹mono f›])
qed

subsection ‹reflexive transitive closure for label relations›

inductive converse3p :: "('a ⇒ 'b ⇒ 'c ⇒ bool) ⇒ 'c ⇒ 'b ⇒ 'a ⇒ bool"
for r :: "'a ⇒ 'b ⇒ 'c ⇒ bool"
where
converse3pI: "r a b c ⟹ converse3p r c b a"

lemma converse3p_converse3p: "converse3p (converse3p r) = r"
by(auto intro: converse3pI intro!: ext elim: converse3p.cases)

lemma converse3pD: "converse3p r c b a ⟹ r a b c"
by(auto elim: converse3p.cases)

inductive rtrancl3p :: "('a ⇒ 'b ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'b list ⇒ 'a ⇒ bool"
for r :: "'a ⇒ 'b ⇒ 'a ⇒ bool"
where
rtrancl3p_refl [intro!, simp]: "rtrancl3p r a [] a"
| rtrancl3p_step: "⟦ rtrancl3p r a bs a'; r a' b a'' ⟧ ⟹ rtrancl3p r a (bs @ [b]) a''"

lemmas rtrancl3p_induct3 =
rtrancl3p.induct[of _ "(ax,ay,az)" _ "(cx,cy,cz)", split_format (complete),
consumes 1, case_names refl step]

lemmas rtrancl3p_induct4 =
rtrancl3p.induct[of _ "(ax,ay,az,aw)" _ "(cx,cy,cz,cw)", split_format (complete),
consumes 1, case_names refl step]

lemma rtrancl3p_induct4' [consumes 1, case_names refl step]:
assumes major: "rtrancl3p r (ax, (ay, az), aw) bs (cx, (cy, cz), cw)"
and refl: "⋀a aa b ba. P a aa b ba [] a aa b ba"
and step: "⋀a aa b ba bs ab ac bb bc bd ad ae be bf.
⟦ rtrancl3p r (a, (aa, b), ba) bs (ab, (ac, bb), bc);
P a aa b ba bs ab ac bb bc; r (ab, (ac, bb), bc) bd (ad, (ae, be), bf) ⟧
⟹ P a aa b ba (bs @ [bd]) ad ae be bf"
shows "P ax ay az aw bs cx cy cz cw"
using major
apply -
apply(drule_tac P="λ(a, (aa, b), ba) bs (cx, (cy, cz), cw). P a aa b ba bs cx cy cz cw" in rtrancl3p.induct)
by(auto intro: refl step)

lemma rtrancl3p_induct1:
"⟦ rtrancl3p r a bs c; P a; ⋀bs c b d. ⟦ rtrancl3p r a bs c; r c b d; P c ⟧ ⟹ P d ⟧ ⟹ P c"
apply(induct rule: rtrancl3p.induct)
apply(auto)
done

inductive_cases rtrancl3p_cases:
"rtrancl3p r x [] y"
"rtrancl3p r x (b # bs) y"

lemma rtrancl3p_trans [trans]:
assumes one: "rtrancl3p r a bs a'"
and two: "rtrancl3p r a' bs' a''"
shows "rtrancl3p r a (bs @ bs') a''"
using two one
proof(induct rule: rtrancl3p.induct)
case rtrancl3p_refl thus ?case by simp
next
case rtrancl3p_step thus ?case
by(auto simp only: append_assoc[symmetric] intro: rtrancl3p.rtrancl3p_step)
qed

lemma rtrancl3p_step_converse:
assumes step: "r a b a'"
and stepify: "rtrancl3p r a' bs a''"
shows "rtrancl3p r a (b # bs) a''"
using stepify step
proof(induct rule: rtrancl3p.induct)
case rtrancl3p_refl
with rtrancl3p.rtrancl3p_refl[where r=r and a=a] show ?case
by(auto dest: rtrancl3p.rtrancl3p_step simp del: rtrancl3p.rtrancl3p_refl)
next
case rtrancl3p_step thus ?case
unfolding append_Cons[symmetric]
by -(rule rtrancl3p.rtrancl3p_step)
qed

lemma converse_rtrancl3p_step:
"rtrancl3p r a (b # bs) a'' ⟹ ∃a'. r a b a' ∧ rtrancl3p r a' bs a''"
apply(induct bs arbitrary: a'' rule: rev_induct)
apply(erule rtrancl3p.cases)
apply(clarsimp)+
apply(erule rtrancl3p.cases)
apply(clarsimp)
apply(rule_tac x="a''a" in exI)
apply(clarsimp)
apply(clarsimp)
apply(erule rtrancl3p.cases)
apply(clarsimp)
apply(clarsimp)
by(fastforce intro: rtrancl3p_step)

lemma converse_rtrancl3pD:
"rtrancl3p (converse3p r) a' bs a ⟹ rtrancl3p r a (rev bs) a'"
apply(induct rule: rtrancl3p.induct)
apply(fastforce intro: rtrancl3p.intros)
apply(auto dest: converse3pD intro: rtrancl3p_step_converse)
done

lemma rtrancl3p_converseD:
"rtrancl3p r a bs a' ⟹ rtrancl3p (converse3p r) a' (rev bs) a"
proof(induct rule: rtrancl3p.induct)
case rtrancl3p_refl thus ?case
by(auto intro: rtrancl3p.intros)
next
case rtrancl3p_step thus ?case
by(auto intro: rtrancl3p_step_converse converse3p.intros)
qed

lemma rtrancl3p_converse_induct [consumes 1, case_names refl step]:
assumes ih: "rtrancl3p r a bs a''"
and refl: "⋀a. P a [] a"
and step: "⋀a b a' bs a''. ⟦ rtrancl3p r a' bs a''; r a b a'; P a' bs a'' ⟧ ⟹ P a (b # bs) a''"
shows "P a bs a''"
using ih
proof(induct bs arbitrary: a a'')
case Nil thus ?case
by(auto elim: rtrancl3p.cases intro: refl)
next
case Cons thus ?case
by(auto dest!: converse_rtrancl3p_step intro: step)
qed

lemma rtrancl3p_converse_induct' [consumes 1, case_names refl step]:
assumes ih: "rtrancl3p r a bs a''"
and refl: "P a'' []"
and step: "⋀a b a' bs. ⟦ rtrancl3p r a' bs a''; r a b a'; P a' bs ⟧ ⟹ P a (b # bs)"
shows "P a bs"
using rtrancl3p_converse_induct[OF ih, where P="λa bs a'. a' = a'' ⟶ P a bs"]
by(auto intro: refl step)

lemma rtrancl3p_converseE[consumes 1, case_names refl step]:
"⟦ rtrancl3p r a bs a'';
⟦ a = a''; bs = [] ⟧ ⟹ thesis;
⋀bs' b a'. ⟦ bs = b # bs'; r a b a'; rtrancl3p r a' bs' a'' ⟧ ⟹ thesis ⟧
⟹ thesis"
by(induct rule: rtrancl3p_converse_induct)(auto)

lemma rtrancl3p_induct' [consumes 1, case_names refl step]:
assumes major: "rtrancl3p r a bs c"
and refl: "P a [] a"
and step: "⋀bs a' b a''. ⟦ rtrancl3p r a bs a'; P a bs a'; r a' b a'' ⟧
⟹ P a (bs @ [b]) a''"
shows "P a bs c"
proof -
from major have "(P a [] a ∧ (∀bs a' b a''. rtrancl3p r a bs a' ∧ P a bs a' ∧ r a' b a'' ⟶ P a (bs @ [b]) a'')) ⟶ P a bs c"
by-(erule rtrancl3p.induct, blast+)
with refl step show ?thesis by blast
qed

lemma r_into_rtrancl3p:
"r a b a' ⟹ rtrancl3p r a [b] a'"
by(rule rtrancl3p_step_converse) auto

lemma rtrancl3p_appendE:
assumes "rtrancl3p r a (bs @ bs') a''"
obtains a' where "rtrancl3p r a bs a'" "rtrancl3p r a' bs' a''"
using assms
apply(induct a "bs @ bs'" arbitrary: bs rule: rtrancl3p_converse_induct')
apply(fastforce intro: rtrancl3p_step_converse simp add: Cons_eq_append_conv)+
done

lemma rtrancl3p_Cons:
"rtrancl3p r a (b # bs) a' ⟷ (∃a''. r a b a'' ∧ rtrancl3p r a'' bs a')"
by(auto intro: rtrancl3p_step_converse converse_rtrancl3p_step)

lemma rtrancl3p_Nil:
"rtrancl3p r a [] a' ⟷ a = a'"
by(auto elim: rtrancl3p_cases)

definition invariant3p :: "('a ⇒ 'b ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ bool"
where "invariant3p r I ⟷ (∀s tl s'. s ∈ I ⟶ r s tl s' ⟶ s' ∈ I)"

lemma invariant3pI: "(⋀s tl s'. ⟦ s ∈ I; r s tl s' ⟧ ⟹ s' ∈ I) ⟹ invariant3p r I"
unfolding invariant3p_def by blast

lemma invariant3pD: "⋀tl. ⟦ invariant3p r I; r s tl s'; s ∈ I ⟧ ⟹ s' ∈ I"
unfolding invariant3p_def by(blast)

lemma invariant3p_rtrancl3p:
assumes inv: "invariant3p r I"
and rtrancl: "rtrancl3p r a bs a'"
and start: "a ∈ I"
shows "a' ∈ I"
using rtrancl start by(induct)(auto dest: invariant3pD[OF inv])

lemma invariant3p_UNIV [simp, intro!]:
"invariant3p r UNIV"
by(blast intro: invariant3pI)

lemma invarinat3p_empty [simp, intro!]:
"invariant3p r {}"
by(blast intro: invariant3pI)

lemma invariant3p_IntI [simp, intro]:
"⟦ invariant3p r I; invariant3p r J ⟧ ⟹ invariant3p r (I ∩ J)"
by(blast dest: invariant3pD intro: invariant3pI)

subsection ‹Concatenation for @{typ String.literal}›

definition concat :: "String.literal list ⇒ String.literal"
where [code_abbrev, code del]: "concat = sum_list"

"String.explode (s + t) = String.explode s @ String.explode t"
by (fact plus_literal.rep_eq)

code_printing
constant concat ⇀
(SML) "String.concat"
and (OCaml) "String.concat \"\""

hide_const (open) concat

end


# Theory Basic_Main

theory Basic_Main
imports Main
"HOL-Library.Sublist"
"HOL-Library.Transitive_Closure_Table"
"HOL-Library.Predicate_Compile_Alternative_Defs"
"HOL-Library.Dlist"
Set_without_equal
Coinductive.Lazy_TLList

(*
"../../Collections/impl/ListSetImpl_Invar"
"../../Collections/impl/RBTSetImpl"
"../../Collections/impl/TrieMapImpl"
"../../Collections/impl/ListMapImpl"
"../../Collections/impl/Fifo"
*)
"../Basic/JT_ICF"

Auxiliary
begin

end


# Theory FWState

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

section ‹State of the multithreaded semantics›

theory FWState
imports
"../Basic/Auxiliary"
begin

datatype lock_action =
Lock
| Unlock
| UnlockFail
| ReleaseAcquire

datatype 't conditional_action =
Join 't
| Yield

datatype ('t, 'w) wait_set_action =
Suspend 'w
| Notify 'w
| NotifyAll 'w
| WakeUp 't
| Notified
| WokenUp

datatype 't interrupt_action
= IsInterrupted 't bool
| Interrupt 't
| ClearInterrupt 't

type_synonym 'l lock_actions = "'l ⇒f lock_action list"

translations
(type) "'l lock_actions" <= (type) "'l ⇒f lock_action list"

type_synonym
"'l lock_actions × ('t,'x,'m) new_thread_action list ×
't conditional_action list × ('t, 'w) wait_set_action list ×
't interrupt_action list × 'o list"
(* pretty printing for thread_action type *)
print_translation ‹
let
fun tr'
[Const (@{type_syntax finfun}, _) $l$
(Const (@{type_syntax list}, _) $Const (@{type_syntax lock_action}, _)), Const (@{type_syntax "prod"}, _)$
(Const (@{type_syntax list}, _) $(Const (@{type_syntax new_thread_action}, _)$ t1 $x$ m)) $(Const (@{type_syntax "prod"}, _)$
(Const (@{type_syntax list}, _) $(Const (@{type_syntax conditional_action}, _)$ t2)) $(Const (@{type_syntax "prod"}, _)$
(Const (@{type_syntax list}, _) $(Const (@{type_syntax wait_set_action}, _)$ t3 $w))$
(Const (@{type_syntax "prod"}, _) $(Const (@{type_syntax "list"}, _)$ (Const (@{type_syntax "interrupt_action"}, _) $t4))$
(Const (@{type_syntax "list"}, _) $o1))))] = if t1 = t2 andalso t2 = t3 andalso t3 = t4 then Syntax.const @{type_syntax thread_action}$ l $t1$ x $m$ w $o1 else raise Match; in [(@{type_syntax "prod"}, K tr')] end › typ "('l,'t,'x,'m,'w,'o) thread_action" definition locks_a :: "('l,'t,'x,'m,'w,'o) thread_action ⇒ 'l lock_actions" ("⦃_⦄⇘l⇙" [0] 1000) where "locks_a ≡ fst" definition thr_a :: "('l,'t,'x,'m,'w,'o) thread_action ⇒ ('t,'x,'m) new_thread_action list" ("⦃_⦄⇘t⇙" [0] 1000) where "thr_a ≡ fst o snd" definition cond_a :: "('l,'t,'x,'m,'w,'o) thread_action ⇒ 't conditional_action list" ("⦃_⦄⇘c⇙" [0] 1000) where "cond_a = fst o snd o snd" definition wset_a :: "('l,'t,'x,'m,'w,'o) thread_action ⇒ ('t, 'w) wait_set_action list" ("⦃_⦄⇘w⇙" [0] 1000) where "wset_a = fst o snd o snd o snd" definition interrupt_a :: "('l,'t,'x,'m,'w,'o) thread_action ⇒ 't interrupt_action list" ("⦃_⦄⇘i⇙" [0] 1000) where "interrupt_a = fst o snd o snd o snd o snd" definition obs_a :: "('l,'t,'x,'m,'w,'o) thread_action ⇒ 'o list" ("⦃_⦄⇘o⇙" [0] 1000) where "obs_a ≡ snd o snd o snd o snd o snd" lemma locks_a_conv [simp]: "locks_a (ls, ntsjswss) = ls" by(simp add:locks_a_def) lemma thr_a_conv [simp]: "thr_a (ls, nts, jswss) = nts" by(simp add: thr_a_def) lemma cond_a_conv [simp]: "cond_a (ls, nts, js, wws) = js" by(simp add: cond_a_def) lemma wset_a_conv [simp]: "wset_a (ls, nts, js, wss, isobs) = wss" by(simp add: wset_a_def) lemma interrupt_a_conv [simp]: "interrupt_a (ls, nts, js, ws, is, obs) = is" by(simp add: interrupt_a_def) lemma obs_a_conv [simp]: "obs_a (ls, nts, js, wss, is, obs) = obs" by(simp add: obs_a_def) fun ta_update_locks :: "('l,'t,'x,'m,'w,'o) thread_action ⇒ lock_action ⇒ 'l ⇒ ('l,'t,'x,'m,'w,'o) thread_action" where "ta_update_locks (ls, nts, js, wss, obs) lta l = (ls(l$:= ls $l @ [lta]), nts, js, wss, obs)" fun ta_update_NewThread :: "('l,'t,'x,'m,'w,'o) thread_action ⇒ ('t,'x,'m) new_thread_action ⇒ ('l,'t,'x,'m,'w,'o) thread_action" where "ta_update_NewThread (ls, nts, js, wss, is, obs) nt = (ls, nts @ [nt], js, wss, is, obs)" fun ta_update_Conditional :: "('l,'t,'x,'m,'w,'o) thread_action ⇒ 't conditional_action ⇒ ('l,'t,'x,'m,'w,'o) thread_action" where "ta_update_Conditional (ls, nts, js, wss, is, obs) j = (ls, nts, js @ [j], wss, is, obs)" fun ta_update_wait_set :: "('l,'t,'x,'m,'w,'o) thread_action ⇒ ('t, 'w) wait_set_action ⇒ ('l,'t,'x,'m,'w,'o) thread_action" where "ta_update_wait_set (ls, nts, js, wss, is, obs) ws = (ls, nts, js, wss @ [ws], is, obs)" fun ta_update_interrupt :: "('l,'t,'x,'m,'w,'o) thread_action ⇒ 't interrupt_action ⇒ ('l,'t,'x,'m,'w,'o) thread_action" where "ta_update_interrupt (ls, nts, js, wss, is, obs) i = (ls, nts, js, wss, is @ [i], obs)" fun ta_update_obs :: "('l,'t,'x,'m,'w,'o) thread_action ⇒ 'o ⇒ ('l,'t,'x,'m,'w,'o) thread_action" where "ta_update_obs (ls, nts, js, wss, is, obs) ob = (ls, nts, js, wss, is, obs @ [ob])" abbreviation empty_ta :: "('l,'t,'x,'m,'w,'o) thread_action" where "empty_ta ≡ (K$ [], [], [], [], [], [])"

notation (input) empty_ta ("ε")

text ‹
Pretty syntax for specifying thread actions:
Write ‹⦃ Lock→l, Unlock→l, Suspend w, Interrupt t⦄› instead of
@{term "((K$[])(l$:= [Lock, Unlock]), [], [Suspend w], [Interrupt t], [])"}.

Automatically coerce basic thread actions into that type and then dispatch to the right
update function by pattern matching.
by the specific ones, i.e. constructors.
To avoid ambiguities with observable actions, the observable actions must be of sort ‹obs_action›,
which the basic thread action types are not.
›

class obs_action

= LockAction "lock_action × 'l"
| ConditionalAction "'t conditional_action"
| WaitSetAction "('t, 'w) wait_set_action"
| InterruptAction "'t interrupt_action"
| ObsAction 'o

setup ‹
›

where

nonterminal ta_let and ta_lets
syntax
"_ta_snoc" :: "ta_lets ⇒ ta_let ⇒ ta_lets" ("_,/ _")
"_ta_block" :: "ta_lets ⇒ 'a" ("⦃_⦄" [0] 1000)
"_ta_empty" :: "ta_lets" ("")
"_ta_single" :: "ta_let ⇒ ta_lets" ("_")
"_ta_inject" :: "logic ⇒ ta_let" ("(_)")
"_ta_lock" :: "logic ⇒ logic ⇒ ta_let" ("_→_")

translations
"_ta_block _ta_empty" == "CONST empty_ta"
"_ta_block (_ta_single bta)" == "_ta_block (_ta_snoc _ta_empty bta)"
"_ta_inject bta" == "CONST inject_thread_action bta"
"_ta_lock la l" == "CONST inject_thread_action (CONST Pair la l)"

lemma ta_upd_proj_simps [simp]:
shows ta_obs_proj_simps:
"⦃ta_update_obs ta obs⦄⇘l⇙ = ⦃ta⦄⇘l⇙" "⦃ta_update_obs ta obs⦄⇘t⇙ = ⦃ta⦄⇘t⇙" "⦃ta_update_obs ta obs⦄⇘w⇙ = ⦃ta⦄⇘w⇙"
"⦃ta_update_obs ta obs⦄⇘c⇙ = ⦃ta⦄⇘c⇙" "⦃ta_update_obs ta obs⦄⇘i⇙ = ⦃ta⦄⇘i⇙" "⦃ta_update_obs ta obs⦄⇘o⇙ = ⦃ta⦄⇘o⇙ @ [obs]"
and ta_lock_proj_simps:
"⦃ta_update_locks ta x l⦄⇘l⇙ = (let ls = ⦃ta⦄⇘l⇙ in ls(l $:= ls$ l @ [x]))"
"⦃ta_update_locks ta x l⦄⇘t⇙ = ⦃ta⦄⇘t⇙" "⦃ta_update_locks ta x l⦄⇘w⇙ = ⦃ta⦄⇘w⇙" "⦃ta_update_locks ta x l⦄⇘c⇙ = ⦃ta⦄⇘c⇙"
"⦃ta_update_locks ta x l⦄⇘i⇙ = ⦃ta⦄⇘i⇙" "⦃ta_update_locks ta x l⦄⇘o⇙ = ⦃ta⦄⇘o⇙"
"⦃ta_update_NewThread ta t⦄⇘l⇙ = ⦃ta⦄⇘l⇙" "⦃ta_update_NewThread ta t⦄⇘t⇙ = ⦃ta⦄⇘t⇙ @ [t]" "⦃ta_update_NewThread ta t⦄⇘w⇙ = ⦃ta⦄⇘w⇙"
and ta_wset_proj_simps:
"⦃ta_update_wait_set ta w⦄⇘l⇙ = ⦃ta⦄⇘l⇙" "⦃ta_update_wait_set ta w⦄⇘t⇙ = ⦃ta⦄⇘t⇙" "⦃ta_update_wait_set ta w⦄⇘w⇙ = ⦃ta⦄⇘w⇙ @ [w]"
"⦃ta_update_wait_set ta w⦄⇘c⇙ = ⦃ta⦄⇘c⇙" "⦃ta_update_wait_set ta w⦄⇘i⇙ = ⦃ta⦄⇘i⇙" "⦃ta_update_wait_set ta w⦄⇘o⇙ = ⦃ta⦄⇘o⇙"
and ta_cond_proj_simps:
"⦃ta_update_Conditional ta c⦄⇘l⇙ = ⦃ta⦄⇘l⇙" "⦃ta_update_Conditional ta c⦄⇘t⇙ = ⦃ta⦄⇘t⇙" "⦃ta_update_Conditional ta c⦄⇘w⇙ = ⦃ta⦄⇘w⇙"
"⦃ta_update_Conditional ta c⦄⇘c⇙ = ⦃ta⦄⇘c⇙ @ [c]" "⦃ta_update_Conditional ta c⦄⇘i⇙ = ⦃ta⦄⇘i⇙" "⦃ta_update_Conditional ta c⦄⇘o⇙ = ⦃ta⦄⇘o⇙"
and ta_interrupt_proj_simps:
"⦃ta_update_interrupt ta i⦄⇘l⇙ = ⦃ta⦄⇘l⇙" "⦃ta_update_interrupt ta i⦄⇘t⇙ = ⦃ta⦄⇘t⇙" "⦃ta_update_interrupt ta i⦄⇘c⇙ = ⦃ta⦄⇘c⇙"
"⦃ta_update_interrupt ta i⦄⇘w⇙ = ⦃ta⦄⇘w⇙" "⦃ta_update_interrupt ta i⦄⇘i⇙ = ⦃ta⦄⇘i⇙ @ [i]" "⦃ta_update_interrupt ta i⦄⇘o⇙ = ⦃ta⦄⇘o⇙"
by(cases ta, simp)+

by(simp_all)

lemmas ta_upd_simps =
ta_update_wait_set.simps ta_update_interrupt.simps ta_update_obs.simps

declare ta_upd_simps [simp del]

hide_const (open)
LockAction NewThreadAction ConditionalAction WaitSetAction InterruptAction ObsAction

datatype wake_up_status =
WSNotified
| WSWokenUp

datatype 'w wait_set_status =
InWS 'w
| PostWS wake_up_status

type_synonym 't lock = "('t × nat) option"
type_synonym ('l,'t) locks = "'l ⇒f 't lock"
type_synonym 'l released_locks = "'l ⇒f nat"
type_synonym ('l,'t,'x) thread_info = "'t ⇀ ('x × 'l released_locks)"
type_synonym ('w,'t) wait_sets = "'t ⇀ 'w wait_set_status"
type_synonym 't interrupts = "'t set"
type_synonym ('l,'t,'x,'m,'w) state = "('l,'t) locks × (('l,'t,'x) thread_info × 'm) × ('w,'t) wait_sets × 't interrupts"

translations
(type) "('l, 't) locks" <= (type) "'l ⇒f ('t × nat) option"
(type) "('l, 't, 'x) thread_info" <= (type) "'t ⇀ ('x × ('l ⇒f nat))"

(* pretty printing for state type *)
print_translation ‹
let
fun tr'
[Const (@{type_syntax finfun}, _) $l1$
(Const (@{type_syntax option}, _) $(Const (@{type_syntax "prod"}, _)$ t1 $Const (@{type_syntax nat}, _))), Const (@{type_syntax "prod"}, _)$
(Const (@{type_syntax "prod"}, _) $(Const (@{type_syntax fun}, _)$ t2 $(Const (@{type_syntax option}, _)$
(Const (@{type_syntax "prod"}, _) $x$
(Const (@{type_syntax finfun}, _) $l2$ Const (@{type_syntax nat}, _))))) $m)$
(Const (@{type_syntax prod}, _) $(Const (@{type_syntax fun}, _)$ t3 $(Const (@{type_syntax option}, _)$ (Const (@{type_syntax wait_set_status}, _) $w)))$
(Const (@{type_syntax fun}, _) $t4$ (Const (@{type_syntax bool}, _))))] =
if t1 = t2 andalso t1 = t3 andalso t1 = t4 andalso l1 = l2
then Syntax.const @{type_syntax state} $l1$ t1 $x$ m $w else raise Match; in [(@{type_syntax "prod"}, K tr')] end › typ "('l,'t,'x,'m,'w) state" abbreviation no_wait_locks :: "'l ⇒f nat" where "no_wait_locks ≡ (K$ 0)"

lemma neq_no_wait_locks_conv:
"⋀ln. ln ≠ no_wait_locks ⟷ (∃l. ln $l > 0)" by(auto simp add: expand_finfun_eq fun_eq_iff) lemma neq_no_wait_locksE: fixes ln assumes "ln ≠ no_wait_locks" obtains l where "ln$ l > 0"
using assms

text ‹
Use type variables for components instead of @{typ "('l,'t,'x,'m,'w) state"} in types for state projections
to allow to reuse them for refined state implementations for code generation.
›

definition locks :: "('locks × ('thread_info × 'm) × 'wsets × 'interrupts) ⇒ 'locks" where
"locks lstsmws ≡ fst lstsmws"

definition thr :: "('locks × ('thread_info × 'm) × 'wsets × 'interrupts) ⇒ 'thread_info" where
"thr lstsmws ≡ fst (fst (snd lstsmws))"

definition shr :: "('locks × ('thread_info × 'm) × 'wsets × 'interrupts) ⇒ 'm" where
"shr lstsmws ≡ snd (fst (snd lstsmws))"

definition wset :: "('locks × ('thread_info × 'm) × 'wsets × 'interrupts) ⇒ 'wsets" where
"wset lstsmws ≡ fst (snd (snd lstsmws))"

definition interrupts :: "('locks × ('thread_info × 'm) × 'wsets × 'interrupts) ⇒ 'interrupts" where
"interrupts lstsmws ≡ snd (snd (snd lstsmws))"

lemma locks_conv [simp]: "locks (ls, tsmws) = ls"

lemma thr_conv [simp]: "thr (ls, (ts, m), ws) = ts"

lemma shr_conv [simp]: "shr (ls, (ts, m), ws, is) = m"

lemma wset_conv [simp]: "wset (ls, (ts, m), ws, is) = ws"

lemma interrupts_conv [simp]: "interrupts (ls, (ts, m), ws, is) = is"

where

"NewThread t x h = convert_new_thread_action f nta ⟷ (∃x'. nta = NewThread t x' h ∧ x = f x')"
"convert_new_thread_action f nta = NewThread t x h ⟷ (∃x'. nta = NewThread t x' h ∧ x = f x')"
by(cases nta, auto)+

"⟦ ⋀t x m. nta = NewThread t x m ⟹ nta' = NewThread t (f x) m;
⋀t b. nta = ThreadExists t b ⟹ nta' = ThreadExists t b ⟧
⟹ convert_new_thread_action f nta = nta'"
apply(cases nta)
apply fastforce+
done

apply(cases ta)
done

"inj (convert_new_thread_action f) = inj f"
apply(rule iffI)
apply(rule injI)
apply(drule_tac x="NewThread undefined x undefined" in injD)
apply auto[2]
apply(rule injI)
apply(case_tac x)
apply(auto dest: injD)
done

"convert_new_thread_action (λx. x) = (id :: ('t, 'x, 'm) new_thread_action ⇒ ('t, 'x, 'm) new_thread_action)" (is ?thesis2)
proof -
show ?thesis1 by(rule ext)(case_tac x, simp_all)
qed

definition convert_extTA :: "('x ⇒ 'x') ⇒ ('l,'t,'x,'m,'w,'o) thread_action ⇒ ('l,'t,'x','m,'w,'o) thread_action"
where "convert_extTA f ta = (⦃ta⦄⇘l⇙, map (convert_new_thread_action f) ⦃ta⦄⇘t⇙, snd (snd ta))"

lemma convert_extTA_simps [simp]:
"convert_extTA f ε = ε"
"⦃convert_extTA f ta⦄⇘l⇙ = ⦃ta⦄⇘l⇙"
"⦃convert_extTA f ta⦄⇘t⇙ = map (convert_new_thread_action f) ⦃ta⦄⇘t⇙"
"⦃convert_extTA f ta⦄⇘c⇙ = ⦃ta⦄⇘c⇙"
"⦃convert_extTA f ta⦄⇘w⇙ = ⦃ta⦄⇘w⇙"
"⦃convert_extTA f ta⦄⇘i⇙ = ⦃ta⦄⇘i⇙"
"convert_extTA f (las, tas, was, cas, is, obs) = (las, map (convert_new_thread_action f) tas, was, cas, is, obs)"
apply(cases ta, simp)+
done

lemma convert_extTA_eq_conv:
"convert_extTA f ta = ta' ⟷
⦃ta⦄⇘l⇙ = ⦃ta'⦄⇘l⇙ ∧ ⦃ta⦄⇘c⇙ = ⦃ta'⦄⇘c⇙ ∧ ⦃ta⦄⇘w⇙ = ⦃ta'⦄⇘w⇙ ∧ ⦃ta⦄⇘o⇙ = ⦃ta'⦄⇘o⇙ ∧ ⦃ta⦄⇘i⇙ = ⦃ta'⦄⇘i⇙ ∧ length ⦃ta⦄⇘t⇙ = length ⦃ta'⦄⇘t⇙ ∧
(∀n < length ⦃ta⦄⇘t⇙. convert_new_thread_action f (⦃ta⦄⇘t⇙ ! n) = ⦃ta'⦄⇘t⇙ ! n)"
apply(cases ta, cases ta')
done

lemma convert_extTA_compose [simp]:
"convert_extTA f (convert_extTA g ta) = convert_extTA (f o g) ta"

lemma obs_a_convert_extTA [simp]: "obs_a (convert_extTA f ta) = obs_a ta"
by(cases ta) simp

datatype 'o action =
NormalAction 'o

instance action :: (type) obs_action
proof qed

where
"convert_obs_initial ta = (⦃ta⦄⇘l⇙, ⦃ta⦄⇘t⇙, ⦃ta⦄⇘c⇙, ⦃ta⦄⇘w⇙, ⦃ta⦄⇘i⇙, map NormalAction ⦃ta⦄⇘o⇙)"

lemma inj_NormalAction [simp]: "inj NormalAction"
by(rule injI) auto

lemma convert_obs_initial_inject [simp]:
"convert_obs_initial ta = convert_obs_initial ta' ⟷ ta = ta'"
by(cases ta)(cases ta', auto simp add: convert_obs_initial_def)

lemma convert_obs_initial_empty_TA [simp]:
"convert_obs_initial ε = ε"

lemma convert_obs_initial_eq_empty_TA [simp]:
"convert_obs_initial ta = ε ⟷ ta = ε"
"ε = convert_obs_initial ta ⟷ ta = ε"
by(case_tac [!] ta)(auto simp add: convert_obs_initial_def)

lemma convert_obs_initial_simps [simp]:
"⦃convert_obs_initial ta⦄⇘o⇙ = map NormalAction ⦃ta⦄⇘o⇙"
"⦃convert_obs_initial ta⦄⇘l⇙ = ⦃ta⦄⇘l⇙"
"⦃convert_obs_initial ta⦄⇘t⇙ = ⦃ta⦄⇘t⇙"
"⦃convert_obs_initial ta⦄⇘c⇙ = ⦃ta⦄⇘c⇙"
"⦃convert_obs_initial ta⦄⇘w⇙ = ⦃ta⦄⇘w⇙"
"⦃convert_obs_initial ta⦄⇘i⇙ = ⦃ta⦄⇘i⇙"

type_synonym
('l,'t,'x,'m,'w,'o) semantics =
"'t ⇒ 'x × 'm ⇒ ('l,'t,'x,'m,'w,'o) thread_action ⇒ 'x × 'm ⇒ bool"

(* pretty printing for semantics *)
print_translation ‹
let
fun tr'
[t4,
Const (@{type_syntax fun}, _) $(Const (@{type_syntax "prod"}, _)$ x1 $m1)$
(Const (@{type_syntax fun}, _) $(Const (@{type_syntax "prod"}, _)$
(Const (@{type_syntax finfun}, _) $l$
(Const (@{type_syntax list}, _) $Const (@{type_syntax lock_action}, _)))$
(Const (@{type_syntax "prod"}, _) $(Const (@{type_syntax list}, _)$ (Const (@{type_syntax new_thread_action}, _) $t1$ x2 $m2))$
(Const (@{type_syntax "prod"}, _) $(Const (@{type_syntax list}, _)$ (Const (@{type_syntax conditional_action}, _) $t2))$
(Const (@{type_syntax "prod"}, _) $(Const (@{type_syntax list}, _)$ (Const (@{type_syntax wait_set_action}, _) $t3$ w)) $(Const (@{type_syntax prod}, _)$
(Const (@{type_syntax list}, _) $(Const (@{type_syntax interrupt_action}, _)$ t5)) $(Const (@{type_syntax list}, _)$ o1)))))) $(Const (@{type_syntax fun}, _)$ (Const (@{type_syntax "prod"}, _) $x3$ m3) $Const (@{type_syntax bool}, _)))] = if x1 = x2 andalso x1 = x3 andalso m1 = m2 andalso m1 = m3 andalso t1 = t2 andalso t2 = t3 andalso t3 = t4 andalso t4 = t5 then Syntax.const @{type_syntax semantics}$ l $t1$ x1 $m1$ w $o1 else raise Match; in [(@{type_syntax fun}, K tr')] end › typ "('l,'t,'x,'m,'w,'o) semantics" end  # Theory FWLock (* Title: JinjaThreads/Framework/FWLock.thy Author: Andreas Lochbihler *) section ‹All about a managing a single lock› theory FWLock imports FWState begin fun has_locks :: "'t lock ⇒ 't ⇒ nat" where "has_locks None t = 0" | "has_locks ⌊(t', n)⌋ t = (if t = t' then Suc n else 0)" lemma has_locks_iff: "has_locks l t = n ⟷ (l = None ∧ n = 0) ∨ (∃n'. l = ⌊(t, n')⌋ ∧ Suc n' = n) ∨ (∃t' n'. l = ⌊(t', n')⌋ ∧ t' ≠ t ∧ n = 0)" by(cases l, auto) lemma has_locksE: "⟦ has_locks l t = n; ⟦ l = None; n = 0 ⟧ ⟹ P; ⋀n'. ⟦ l = ⌊(t, n')⌋; Suc n' = n ⟧ ⟹ P; ⋀t' n'. ⟦ l = ⌊(t', n')⌋; t' ≠ t; n = 0 ⟧ ⟹ P ⟧ ⟹ P" by(auto simp add: has_locks_iff split: if_split_asm prod.split_asm) inductive may_lock :: "'t lock ⇒ 't ⇒ bool" where "may_lock None t" | "may_lock ⌊(t, n)⌋ t" lemma may_lock_iff [code]: "may_lock l t = (case l of None ⇒ True | ⌊(t', n)⌋ ⇒ t = t')" by(auto intro: may_lock.intros elim: may_lock.cases) lemma may_lockI: "l = None ∨ (∃n. l = ⌊(t, n)⌋) ⟹ may_lock l t" by(cases l, auto intro: may_lock.intros) lemma may_lockE [consumes 1, case_names None Locked]: "⟦ may_lock l t; l = None ⟹ P; ⋀n. l = ⌊(t, n)⌋ ⟹ P ⟧ ⟹ P" by(auto elim: may_lock.cases) lemma may_lock_may_lock_t_eq: "⟦ may_lock l t; may_lock l t' ⟧ ⟹ (l = None) ∨ (t = t')" by(auto elim!: may_lockE) abbreviation has_lock :: "'t lock ⇒ 't ⇒ bool" where "has_lock l t ≡ 0 < has_locks l t" lemma has_locks_Suc_has_lock: "has_locks l t = Suc n ⟹ has_lock l t" by(auto) lemmas has_lock_has_locks_Suc = gr0_implies_Suc[where n = "has_locks l t"] for l t lemma has_lock_has_locks_conv: "has_lock l t ⟷ (∃n. has_locks l t = (Suc n))" by(auto intro: has_locks_Suc_has_lock has_lock_has_locks_Suc) lemma has_lock_may_lock: "has_lock l t ⟹ may_lock l t" by(cases l, auto intro: may_lockI) lemma has_lock_may_lock_t_eq: "⟦ has_lock l t; may_lock l t' ⟧ ⟹ t = t'" by(auto elim!: may_lockE split: if_split_asm) lemma has_locks_has_locks_t_eq: "⟦has_locks l t = Suc n; has_locks l t' = Suc n'⟧ ⟹ t = t'" by(auto elim: has_locksE) lemma has_lock_has_lock_t_eq: "⟦ has_lock l t; has_lock l t' ⟧ ⟹ t = t'" unfolding has_lock_has_locks_conv by(auto intro: has_locks_has_locks_t_eq) lemma not_may_lock_conv: "¬ may_lock l t ⟷ (∃t'. t' ≠ t ∧ has_lock l t')" by(cases l, auto intro: may_lock.intros elim: may_lockE) (* State update functions for locking *) fun lock_lock :: "'t lock ⇒ 't ⇒ 't lock" where "lock_lock None t = ⌊(t, 0)⌋" | "lock_lock ⌊(t', n)⌋ t = ⌊(t', Suc n)⌋" fun unlock_lock :: "'t lock ⇒ 't lock" where "unlock_lock None = None" | "unlock_lock ⌊(t, n)⌋ = (case n of 0 ⇒ None | Suc n' ⇒ ⌊(t, n')⌋)" fun release_all :: "'t lock ⇒ 't ⇒ 't lock" where "release_all None t = None" | "release_all ⌊(t', n)⌋ t = (if t = t' then None else ⌊(t', n)⌋)" fun acquire_locks :: "'t lock ⇒ 't ⇒ nat ⇒ 't lock" where "acquire_locks L t 0 = L" | "acquire_locks L t (Suc m) = acquire_locks (lock_lock L t) t m" lemma acquire_locks_conv: "acquire_locks L t n = (case L of None ⇒ (case n of 0 ⇒ None | Suc m ⇒ ⌊(t, m)⌋) | ⌊(t', m)⌋ ⇒ ⌊(t', n + m)⌋)" by(induct n arbitrary: L)(auto) lemma lock_lock_ls_Some: "∃t' n. lock_lock l t = ⌊(t', n)⌋" by(cases l, auto) lemma unlock_lock_SomeD: "unlock_lock l = ⌊(t', n)⌋ ⟹ l = ⌊(t', Suc n)⌋" by(cases l, auto split: nat.split_asm) lemma has_locks_Suc_lock_lock_has_locks_Suc_Suc: "has_locks l t = Suc n ⟹ has_locks (lock_lock l t) t = Suc (Suc n)" by(auto elim!: has_locksE) lemma has_locks_lock_lock_conv [simp]: "may_lock l t ⟹ has_locks (lock_lock l t) t = Suc (has_locks l t)" by(auto elim: may_lockE) lemma has_locks_release_all_conv [simp]: "has_locks (release_all l t) t = 0" by(cases l, auto split: if_split_asm) lemma may_lock_lock_lock_conv [simp]: "may_lock (lock_lock l t) t = may_lock l t" by(cases l, auto elim!: may_lock.cases intro: may_lock.intros) lemma has_locks_acquire_locks_conv [simp]: "may_lock l t ⟹ has_locks (acquire_locks l t n) t = has_locks l t + n" by(induct n arbitrary: l, auto) lemma may_lock_unlock_lock_conv [simp]: "has_lock l t ⟹ may_lock (unlock_lock l) t = may_lock l t" by(cases l)(auto split: if_split_asm nat.splits elim!: may_lock.cases intro: may_lock.intros) lemma may_lock_release_all_conv [simp]: "may_lock (release_all l t) t = may_lock l t" by(cases l, auto split: if_split_asm intro!: may_lockI elim: may_lockE) lemma may_lock_t_may_lock_unlock_lock_t: "may_lock l t ⟹ may_lock (unlock_lock l) t" by(auto intro: may_lock.intros elim!: may_lockE split: nat.split) lemma may_lock_has_locks_lock_lock_0: "⟦may_lock l t'; t ≠ t'⟧ ⟹ has_locks (lock_lock l t') t = 0" by(auto elim!: may_lock.cases) lemma has_locks_unlock_lock_conv [simp]: "has_lock l t ⟹ has_locks (unlock_lock l) t = has_locks l t - 1" by(cases l)(auto split: nat.split) lemma has_lock_lock_lock_unlock_lock_id [simp]: "has_lock l t ⟹ lock_lock (unlock_lock l) t = l" by(cases l)(auto split: if_split_asm nat.split) lemma may_lock_unlock_lock_lock_lock_id [simp]: "may_lock l t ⟹ unlock_lock (lock_lock l t) = l" by(cases l) auto lemma may_lock_has_locks_0: "⟦ may_lock l t; t ≠ t' ⟧ ⟹ has_locks l t' = 0" by(auto elim!: may_lockE) fun upd_lock :: "'t lock ⇒ 't ⇒ lock_action ⇒ 't lock" where "upd_lock l t Lock = lock_lock l t" | "upd_lock l t Unlock = unlock_lock l" | "upd_lock l t UnlockFail = l" | "upd_lock l t ReleaseAquire = release_all l t" fun upd_locks :: "'t lock ⇒ 't ⇒ lock_action list ⇒ 't lock" where "upd_locks l t [] = l" | "upd_locks l t (L # Ls) = upd_locks (upd_lock l t L) t Ls" lemma upd_locks_append [simp]: "upd_locks l t (Ls @ Ls') = upd_locks (upd_locks l t Ls) t Ls'" by(induct Ls arbitrary: l, auto) lemma upd_lock_Some_thread_idD: assumes ul: "upd_lock l t L = ⌊(t', n)⌋" and tt': "t ≠ t'" shows "∃n. l = ⌊(t', n)⌋" proof(cases L) case Lock with ul tt' show ?thesis by(cases l, auto) next case Unlock with ul tt' show ?thesis by(auto dest: unlock_lock_SomeD) next case UnlockFail with ul show ?thesis by(simp) next case ReleaseAcquire with ul show ?thesis by(cases l, auto split: if_split_asm) qed lemma has_lock_upd_lock_implies_has_lock: "⟦ has_lock (upd_lock l t L) t'; t ≠ t' ⟧ ⟹ has_lock l t'" by(cases l L rule: option.exhaust[case_product lock_action.exhaust])(auto split: if_split_asm nat.split_asm) lemma has_lock_upd_locks_implies_has_lock: "⟦ has_lock (upd_locks l t Ls) t'; t ≠ t' ⟧ ⟹ has_lock l t'" by(induct l t Ls rule: upd_locks.induct)(auto intro: has_lock_upd_lock_implies_has_lock) (* Preconditions for lock actions *) fun lock_action_ok :: "'t lock ⇒ 't ⇒ lock_action ⇒ bool" where "lock_action_ok l t Lock = may_lock l t" | "lock_action_ok l t Unlock = has_lock l t" | "lock_action_ok l t UnlockFail = (¬ has_lock l t)" | "lock_action_ok l t ReleaseAcquire = True" fun lock_actions_ok :: "'t lock ⇒ 't ⇒ lock_action list ⇒ bool" where "lock_actions_ok l t [] = True" | "lock_actions_ok l t (L # Ls) = (lock_action_ok l t L ∧ lock_actions_ok (upd_lock l t L) t Ls)" lemma lock_actions_ok_append [simp]: "lock_actions_ok l t (Ls @ Ls') ⟷ lock_actions_ok l t Ls ∧ lock_actions_ok (upd_locks l t Ls) t Ls'" by(induct Ls arbitrary: l) auto lemma not_lock_action_okE [consumes 1, case_names Lock Unlock UnlockFail]: "⟦ ¬ lock_action_ok l t L; ⟦ L = Lock; ¬ may_lock l t ⟧ ⟹ Q; ⟦ L = Unlock; ¬ has_lock l t ⟧ ⟹ Q; ⟦ L = UnlockFail; has_lock l t ⟧ ⟹ Q⟧ ⟹ Q" by(cases L) auto lemma may_lock_upd_lock_conv [simp]: "lock_action_ok l t L ⟹ may_lock (upd_lock l t L) t = may_lock l t" by(cases L) auto lemma may_lock_upd_locks_conv [simp]: "lock_actions_ok l t Ls ⟹ may_lock (upd_locks l t Ls) t = may_lock l t" by(induct l t Ls rule: upd_locks.induct) simp_all lemma lock_actions_ok_Lock_may_lock: "⟦ lock_actions_ok l t Ls; Lock ∈ set Ls ⟧ ⟹ may_lock l t" by(induct l t Ls rule: lock_actions_ok.induct) auto lemma has_locks_lock_lock_conv' [simp]: "⟦ may_lock l t'; t ≠ t' ⟧ ⟹ has_locks (lock_lock l t') t = has_locks l t" by(cases l)(auto elim: may_lock.cases) lemma has_locks_unlock_lock_conv' [simp]: "⟦ has_lock l t'; t ≠ t' ⟧ ⟹ has_locks (unlock_lock l) t = has_locks l t" by(cases l)(auto split: if_split_asm nat.split) lemma has_locks_release_all_conv' [simp]: "t ≠ t' ⟹ has_locks (release_all l t') t = has_locks l t" by(cases l) auto lemma has_locks_acquire_locks_conv' [simp]: "⟦ may_lock l t; t ≠ t' ⟧ ⟹ has_locks (acquire_locks l t n) t' = has_locks l t'" by(induct l t n rule: acquire_locks.induct) simp_all lemma lock_action_ok_has_locks_upd_lock_eq_has_locks [simp]: "⟦ lock_action_ok l t' L; t ≠ t' ⟧ ⟹ has_locks (upd_lock l t' L) t = has_locks l t" by(cases L) auto lemma lock_actions_ok_has_locks_upd_locks_eq_has_locks [simp]: "⟦ lock_actions_ok l t' Ls; t ≠ t' ⟧ ⟹ has_locks (upd_locks l t' Ls) t = has_locks l t" by(induct l t' Ls rule: upd_locks.induct) simp_all lemma has_lock_acquire_locks_implies_has_lock: "⟦ has_lock (acquire_locks l t n) t'; t ≠ t' ⟧ ⟹ has_lock l t'" unfolding acquire_locks_conv by(cases n)(auto split: if_split_asm) lemma has_lock_has_lock_acquire_locks: "has_lock l T ⟹ has_lock (acquire_locks l t n) T" unfolding acquire_locks_conv by(auto) fun lock_actions_ok' :: "'t lock ⇒ 't ⇒ lock_action list ⇒ bool" where "lock_actions_ok' l t [] = True" | "lock_actions_ok' l t (L#Ls) = ((L = Lock ∧ ¬ may_lock l t) ∨ lock_action_ok l t L ∧ lock_actions_ok' (upd_lock l t L) t Ls)" lemma lock_actions_ok'_iff: "lock_actions_ok' l t las ⟷ lock_actions_ok l t las ∨ (∃xs ys. las = xs @ Lock # ys ∧ lock_actions_ok l t xs ∧ ¬ may_lock (upd_locks l t xs) t)" proof(induct l t las rule: lock_actions_ok.induct) case (2 L t LA LAS) show ?case proof(cases "LA = Lock ∧ ¬ may_lock L t") case True hence "(∃ys. Lock # LAS = [] @ Lock # ys) ∧ lock_actions_ok L t [] ∧ ¬ may_lock (upd_locks L t []) t" by(simp) with True show ?thesis by(simp (no_asm))(blast) next case False with 2 show ?thesis by(fastforce simp add: Cons_eq_append_conv elim: allE[where x="LA # xs" for xs]) qed qed simp lemma lock_actions_ok'E[consumes 1, case_names ok Lock]: "⟦ lock_actions_ok' l t las; lock_actions_ok l t las ⟹ P; ⋀xs ys. ⟦ las = xs @ Lock # ys; lock_actions_ok l t xs; ¬ may_lock (upd_locks l t xs) t ⟧ ⟹ P ⟧ ⟹ P" by(auto simp add: lock_actions_ok'_iff) end  # Theory FWLocking (* Title: JinjaThreads/Framework/FWLocking.thy Author: Andreas Lochbihler *) section ‹Semantics of the thread actions for locking› theory FWLocking imports FWLock begin definition redT_updLs :: "('l,'t) locks ⇒ 't ⇒ 'l lock_actions ⇒ ('l,'t) locks" where "redT_updLs ls t las ≡ (λ(l, la). upd_locks l t la) ∘$ (($ls, las$))"

lemma redT_updLs_iff [simp]: "redT_updLs ls t las $l = upd_locks (ls$ l) t (las $l)" by(simp add: redT_updLs_def) lemma upd_locks_empty_conv [simp]: "(λ(l, las). upd_locks l t las) ∘$ ($ls, K$ []$) = ls" by(auto intro: finfun_ext) lemma redT_updLs_Some_thread_idD: "⟦ has_lock (redT_updLs ls t las$ l) t'; t ≠ t' ⟧ ⟹ has_lock (ls $l) t'" by(auto simp add: redT_updLs_def intro: has_lock_upd_locks_implies_has_lock) definition acquire_all :: "('l, 't) locks ⇒ 't ⇒ ('l ⇒f nat) ⇒ ('l, 't) locks" where "⋀ln. acquire_all ls t ln ≡ (λ(l, la). acquire_locks l t la) ∘$ (($ls, ln$))"

lemma acquire_all_iff [simp]:
"⋀ln. acquire_all ls t ln $l = acquire_locks (ls$ l) t (ln $l)" by(simp add: acquire_all_def) definition lock_ok_las :: "('l,'t) locks ⇒ 't ⇒ 'l lock_actions ⇒ bool" where "lock_ok_las ls t las ≡ ∀l. lock_actions_ok (ls$ l) t (las $l)" lemma lock_ok_lasI [intro]: "(⋀l. lock_actions_ok (ls$ l) t (las $l)) ⟹ lock_ok_las ls t las" by(simp add: lock_ok_las_def) lemma lock_ok_lasE: "⟦ lock_ok_las ls t las; (⋀l. lock_actions_ok (ls$ l) t (las $l)) ⟹ Q ⟧ ⟹ Q" by(simp add: lock_ok_las_def) lemma lock_ok_lasD: "lock_ok_las ls t las ⟹ lock_actions_ok (ls$ l) t (las $l)" by(simp add: lock_ok_las_def) lemma lock_ok_las_code [code]: "lock_ok_las ls t las = finfun_All ((λ(l, la). lock_actions_ok l t la) ∘$ ($ls, las$))"

lemma lock_ok_las_may_lock:
"⟦ lock_ok_las ls t las; Lock ∈ set (las $l) ⟧ ⟹ may_lock (ls$ l) t"
by(erule lock_ok_lasE)(rule lock_actions_ok_Lock_may_lock)

lemma redT_updLs_may_lock [simp]:
"lock_ok_las ls t las ⟹ may_lock (redT_updLs ls t las $l) t = may_lock (ls$ l) t"
by(auto dest!: lock_ok_lasD[where l=l])

lemma redT_updLs_has_locks [simp]:
"⟦ lock_ok_las ls t' las; t ≠ t' ⟧ ⟹ has_locks (redT_updLs ls t' las $l) t = has_locks (ls$ l) t"
by(auto dest!: lock_ok_lasD[where l=l])

definition may_acquire_all :: "('l, 't) locks ⇒ 't ⇒ ('l ⇒f nat) ⇒ bool"
where "⋀ln. may_acquire_all ls t ln ≡ ∀l. ln $l > 0 ⟶ may_lock (ls$ l) t"

lemma may_acquire_allI [intro]:
"⋀ln. (⋀l. ln $l > 0 ⟹ may_lock (ls$ l) t) ⟹ may_acquire_all ls t ln"

lemma may_acquire_allE:
"⋀ln. ⟦ may_acquire_all ls t ln; ∀l. ln $l > 0 ⟶ may_lock (ls$ l) t ⟹ P ⟧ ⟹ P"

lemma may_acquire_allD [dest]:
"⋀ln. ⟦ may_acquire_all ls t ln; ln $l > 0 ⟧ ⟹ may_lock (ls$ l) t"

lemma may_acquire_all_has_locks_acquire_locks [simp]:
fixes ln
shows "⟦ may_acquire_all ls t ln; t ≠ t' ⟧ ⟹ has_locks (acquire_locks (ls $l) t (ln$ l)) t' = has_locks (ls $l) t'" by(cases "ln$ l > 0")(auto dest: may_acquire_allD)

lemma may_acquire_all_code [code]:
"⋀ln. may_acquire_all ls t ln ⟷ finfun_All ((λ(lock, n). n > 0 ⟶ may_lock lock t) ∘$($ls, ln$))" by(auto simp add: may_acquire_all_def finfun_All_All o_def) definition collect_locks :: "'l lock_actions ⇒ 'l set" where "collect_locks las = {l. Lock ∈ set (las$ l)}"

lemma collect_locksI:
"Lock ∈ set (las $l) ⟹ l ∈ collect_locks las" by(simp add: collect_locks_def) lemma collect_locksE: "⟦ l ∈ collect_locks las; Lock ∈ set (las$ l) ⟹ P ⟧ ⟹ P"

lemma collect_locksD:
"l ∈ collect_locks las ⟹ Lock ∈ set (las $l)" by(simp add: collect_locks_def) fun must_acquire_lock :: "lock_action list ⇒ bool" where "must_acquire_lock [] = False" | "must_acquire_lock (Lock # las) = True" | "must_acquire_lock (Unlock # las) = False" | "must_acquire_lock (_ # las) = must_acquire_lock las" lemma must_acquire_lock_append: "must_acquire_lock (xs @ ys) ⟷ (if Lock ∈ set xs ∨ Unlock ∈ set xs then must_acquire_lock xs else must_acquire_lock ys)" proof(induct xs) case Nil thus ?case by simp next case (Cons L Ls) thus ?case by (cases L, simp_all) qed lemma must_acquire_lock_contains_lock: "must_acquire_lock las ⟹ Lock ∈ set las" proof(induct las) case (Cons l las) thus ?case by(cases l) auto qed simp lemma must_acquire_lock_conv: "must_acquire_lock las = (case (filter (λL. L = Lock ∨ L = Unlock) las) of [] ⇒ False | L # Ls ⇒ L = Lock)" proof(induct las) case Nil thus ?case by simp next case (Cons LA LAS) thus ?case by(cases LA, auto split: list.split_asm) qed definition collect_locks' :: "'l lock_actions ⇒ 'l set" where "collect_locks' las ≡ {l. must_acquire_lock (las$ l)}"

lemma collect_locks'I:
"must_acquire_lock (las $l) ⟹ l ∈ collect_locks' las" by(simp add: collect_locks'_def) lemma collect_locks'E: "⟦ l ∈ collect_locks' las; must_acquire_lock (las$ l) ⟹ P ⟧ ⟹ P"

lemma collect_locks'_subset_collect_locks:
"collect_locks' las ⊆ collect_locks las"
by(auto simp add: collect_locks'_def collect_locks_def intro: must_acquire_lock_contains_lock)

definition lock_ok_las' :: "('l,'t) locks ⇒ 't ⇒ 'l lock_actions ⇒ bool" where
"lock_ok_las' ls t las ≡ ∀l. lock_actions_ok' (ls $l) t (las$ l)"

lemma lock_ok_las'I: "(⋀l. lock_actions_ok' (ls $l) t (las$ l)) ⟹ lock_ok_las' ls t las"

lemma lock_ok_las'D: "lock_ok_las' ls t las ⟹ lock_actions_ok' (ls $l) t (las$ l)"

lemma not_lock_ok_las'_conv:
"¬ lock_ok_las' ls t las ⟷ (∃l. ¬ lock_actions_ok' (ls $l) t (las$ l))"

lemma lock_ok_las'_code:
"lock_ok_las' ls t las = finfun_All ((λ(l, la). lock_actions_ok' l t la) ∘$($ls, las$))" by(simp add: lock_ok_las'_def finfun_All_All o_def) lemma lock_ok_las'_collect_locks'_may_lock: assumes lot': "lock_ok_las' ls t las" and mayl: "∀l ∈ collect_locks' las. may_lock (ls$ l) t"
and l: "l ∈ collect_locks las"
shows "may_lock (ls $l) t" proof(cases "l ∈ collect_locks' las") case True thus ?thesis using mayl by auto next case False hence nmal: "¬ must_acquire_lock (las$ l)"
by(auto intro: collect_locks'I)
from l have locklasl: "Lock ∈ set (las $l)" by(rule collect_locksD) then obtain ys zs where las: "las$ l = ys @ Lock # zs"
and notin: "Lock ∉ set ys"
by(auto dest: split_list_first)
from lot' have "lock_actions_ok' (ls $l) t (las$ l)"
thus ?thesis
proof(induct rule: lock_actions_ok'E)
case ok
with locklasl show ?thesis
by -(rule lock_actions_ok_Lock_may_lock)
next
case (Lock YS ZS)
note LAS = ‹las $l = YS @ Lock # ZS› note lao = ‹lock_actions_ok (ls$ l) t YS›
note nml = ‹¬ may_lock (upd_locks (ls $l) t YS) t› from LAS las nmal notin have "Unlock ∈ set YS" by -(erule contrapos_np, auto simp add: must_acquire_lock_append append_eq_append_conv2 append_eq_Cons_conv) then obtain ys' zs' where YS: "YS = ys' @ Unlock # zs'" and unlock: "Unlock ∉ set ys'" by(auto dest: split_list_first) from YS las LAS lao have lao': "lock_actions_ok (ls$ l) t (ys' @ [Unlock])" by(auto)
hence "has_lock (upd_locks (ls $l) t ys') t" by simp hence "may_lock (upd_locks (ls$ l) t ys') t"
by(rule has_lock_may_lock)
moreover from lao' have "lock_actions_ok (ls $l) t ys'" by simp ultimately show ?thesis by simp qed qed lemma lock_actions_ok'_must_acquire_lock_lock_actions_ok: "⟦ lock_actions_ok' l t Ls; must_acquire_lock Ls ⟶ may_lock l t⟧ ⟹ lock_actions_ok l t Ls" proof(induct l t Ls rule: lock_actions_ok.induct) case 1 thus ?case by simp next case (2 l t L LS) thus ?case proof(cases "L = Lock ∨ L = Unlock") case True with 2 show ?thesis by(auto simp add: lock_actions_ok'_iff Cons_eq_append_conv intro: has_lock_may_lock) qed(cases L, auto) qed lemma lock_ok_las'_collect_locks_lock_ok_las: assumes lol': "lock_ok_las' ls t las" and clml: "⋀l. l ∈ collect_locks las ⟹ may_lock (ls$ l) t"
shows "lock_ok_las ls t las"
proof(rule lock_ok_lasI)
fix l
from lol' have "lock_actions_ok' (ls $l) t (las$ l)" by(rule lock_ok_las'D)
thus "lock_actions_ok (ls $l) t (las$ l)"
proof(rule lock_actions_ok'_must_acquire_lock_lock_actions_ok[OF _ impI])
assume mal: "must_acquire_lock (las $l)" thus "may_lock (ls$ l) t"
by(auto intro!: clml collect_locksI elim: must_acquire_lock_contains_lock )
qed
qed

lemma lock_ok_las'_into_lock_on_las:
"⟦lock_ok_las' ls t las; ⋀l. l ∈ collect_locks' las ⟹ may_lock (ls $l) t⟧ ⟹ lock_ok_las ls t las" by (metis lock_ok_las'_collect_locks'_may_lock lock_ok_las'_collect_locks_lock_ok_las) end  # Theory FWThread (* Title: JinjaThreads/Framework/FWThread.thy Author: Andreas Lochbihler *) section ‹Semantics of the thread actions for thread creation› theory FWThread imports FWState begin text‹Abstractions for thread ids› context notes [[inductive_internals]] begin inductive free_thread_id :: "('l,'t,'x) thread_info ⇒ 't ⇒ bool" for ts :: "('l,'t,'x) thread_info" and t :: 't where "ts t = None ⟹ free_thread_id ts t" declare free_thread_id.cases [elim] end lemma free_thread_id_iff: "free_thread_id ts t = (ts t = None)" by(auto elim: free_thread_id.cases intro: free_thread_id.intros) text‹Update functions for the multithreaded state› fun redT_updT :: "('l,'t,'x) thread_info ⇒ ('t,'x,'m) new_thread_action ⇒ ('l,'t,'x) thread_info" where "redT_updT ts (NewThread t' x m) = ts(t' ↦ (x, no_wait_locks))" | "redT_updT ts _ = ts" fun redT_updTs :: "('l,'t,'x) thread_info ⇒ ('t,'x,'m) new_thread_action list ⇒ ('l,'t,'x) thread_info" where "redT_updTs ts [] = ts" | "redT_updTs ts (ta#tas) = redT_updTs (redT_updT ts ta) tas" lemma redT_updTs_append [simp]: "redT_updTs ts (tas @ tas') = redT_updTs (redT_updTs ts tas) tas'" by(induct ts tas rule: redT_updTs.induct) auto lemma redT_updT_None: "redT_updT ts ta t = None ⟹ ts t = None" by(cases ta)(auto split: if_splits) lemma redT_updTs_None: "redT_updTs ts tas t = None ⟹ ts t = None" by(induct ts tas rule: redT_updTs.induct)(auto intro: redT_updT_None) lemma redT_updT_Some1: "ts t = ⌊xw⌋ ⟹ ∃xw. redT_updT ts ta t = ⌊xw⌋" by(cases ta) auto lemma redT_updTs_Some1: "ts t = ⌊xw⌋ ⟹ ∃xw. redT_updTs ts tas t = ⌊xw⌋" unfolding not_None_eq[symmetric] by(induct ts tas arbitrary: xw rule: redT_updTs.induct)(simp_all del: split_paired_Ex, blast dest: redT_updT_Some1) lemma redT_updT_finite_dom_inv: "finite (dom (redT_updT ts ta)) = finite (dom ts)" by(cases ta) auto lemma redT_updTs_finite_dom_inv: "finite (dom (redT_updTs ts tas)) = finite (dom ts)" by(induct ts tas rule: redT_updTs.induct)(simp_all add: redT_updT_finite_dom_inv) text‹Preconditions for thread creation actions› text‹These primed versions are for checking preconditions only. They allow the thread actions to have a type for thread-local information that is different than the thread info state itself.› fun redT_updT' :: "('l,'t,'x) thread_info ⇒ ('t,'x','m) new_thread_action ⇒ ('l,'t,'x) thread_info" where "redT_updT' ts (NewThread t' x m) = ts(t' ↦ (undefined, no_wait_locks))" | "redT_updT' ts _ = ts" fun redT_updTs' :: "('l,'t,'x) thread_info ⇒ ('t,'x','m) new_thread_action list ⇒ ('l,'t,'x) thread_info" where "redT_updTs' ts [] = ts" | "redT_updTs' ts (ta#tas) = redT_updTs' (redT_updT' ts ta) tas" lemma redT_updT'_None: "redT_updT' ts ta t = None ⟹ ts t = None" by(cases ta)(auto split: if_splits) primrec thread_ok :: "('l,'t,'x) thread_info ⇒ ('t,'x','m) new_thread_action ⇒ bool" where "thread_ok ts (NewThread t x m) = free_thread_id ts t" | "thread_ok ts (ThreadExists t b) = (b ≠ free_thread_id ts t)" fun thread_oks :: "('l,'t,'x) thread_info ⇒ ('t,'x','m) new_thread_action list ⇒ bool" where "thread_oks ts [] = True" | "thread_oks ts (ta#tas) = (thread_ok ts ta ∧ thread_oks (redT_updT' ts ta) tas)" lemma thread_ok_ts_change: "(⋀t. ts t = None ⟷ ts' t = None) ⟹ thread_ok ts ta ⟷ thread_ok ts' ta" by(cases ta)(auto simp add: free_thread_id_iff) lemma thread_oks_ts_change: "(⋀t. ts t = None ⟷ ts' t = None) ⟹ thread_oks ts tas ⟷ thread_oks ts' tas" proof(induct tas arbitrary: ts ts') case Nil thus ?case by simp next case (Cons ta tas ts ts') note IH = ‹⋀ts ts'. (⋀t. (ts t = None) = (ts' t = None)) ⟹ thread_oks ts tas = thread_oks ts' tas› note eq = ‹⋀t. (ts t = None) = (ts' t = None)› from eq have "thread_ok ts ta ⟷ thread_ok ts' ta" by(rule thread_ok_ts_change) moreover from eq have "⋀t. (redT_updT' ts ta t = None) = (redT_updT' ts' ta t = None)" by(cases ta)(auto) hence "thread_oks (redT_updT' ts ta) tas = thread_oks (redT_updT' ts' ta) tas" by(rule IH) ultimately show ?case by simp qed lemma redT_updT'_eq_None_conv: "(⋀t. ts t = None ⟷ ts' t = None) ⟹ redT_updT' ts ta t = None ⟷ redT_updT ts' ta t = None" by(cases ta) simp_all lemma redT_updTs'_eq_None_conv: "(⋀t. ts t = None ⟷ ts' t = None) ⟹ redT_updTs' ts tas t = None ⟷ redT_updTs ts' tas t = None" apply(induct tas arbitrary: ts ts') apply simp_all apply(blast intro: redT_updT'_eq_None_conv del: iffI) done lemma thread_oks_redT_updT_conv [simp]: "thread_oks (redT_updT' ts ta) tas = thread_oks (redT_updT ts ta) tas" by(rule thread_oks_ts_change)(rule redT_updT'_eq_None_conv refl)+ lemma thread_oks_append [simp]: "thread_oks ts (tas @ tas') = (thread_oks ts tas ∧ thread_oks (redT_updTs' ts tas) tas')" by(induct tas arbitrary: ts, auto) lemma thread_oks_redT_updTs_conv [simp]: "thread_oks (redT_updTs' ts ta) tas = thread_oks (redT_updTs ts ta) tas" by(rule thread_oks_ts_change)(rule redT_updTs'_eq_None_conv refl)+ lemma redT_updT_Some: "⟦ ts t = ⌊xw⌋; thread_ok ts ta ⟧ ⟹ redT_updT ts ta t = ⌊xw⌋" by(cases ta) auto lemma redT_updTs_Some: "⟦ ts t = ⌊xw⌋; thread_oks ts tas ⟧ ⟹ redT_updTs ts tas t = ⌊xw⌋" by(induct ts tas rule: redT_updTs.induct)(auto intro: redT_updT_Some) lemma redT_updT'_Some: "⟦ ts t = ⌊xw⌋; thread_ok ts ta ⟧ ⟹ redT_updT' ts ta t = ⌊xw⌋" by(cases ta) auto lemma redT_updTs'_Some: "⟦ ts t = ⌊xw⌋; thread_oks ts tas ⟧ ⟹ redT_updTs' ts tas t = ⌊xw⌋" by(induct ts tas rule: redT_updTs'.induct)(auto intro: redT_updT'_Some) lemma thread_ok_new_thread: "thread_ok ts (NewThread t m' x) ⟹ ts t = None" by(auto) lemma thread_oks_new_thread: "⟦ thread_oks ts tas; NewThread t x m ∈ set tas ⟧ ⟹ ts t = None" by(induct ts tas rule: thread_oks.induct)(auto intro: redT_updT'_None) lemma redT_updT_new_thread_ts: "thread_ok ts (NewThread t x m) ⟹ redT_updT ts (NewThread t x m) t = ⌊(x, no_wait_locks)⌋" by(simp) lemma redT_updTs_new_thread_ts: "⟦ thread_oks ts tas; NewThread t x m ∈ set tas ⟧ ⟹ redT_updTs ts tas t = ⌊(x, no_wait_locks)⌋" by(induct ts tas rule: redT_updTs.induct)(auto intro: redT_updTs_Some) lemma redT_updT_new_thread: "⟦ redT_updT ts ta t = ⌊(x, w)⌋; thread_ok ts ta; ts t = None ⟧ ⟹ ∃m. ta = NewThread t x m ∧ w = no_wait_locks" by(cases ta)(auto split: if_split_asm) lemma redT_updTs_new_thread: "⟦ redT_updTs ts tas t = ⌊(x, w)⌋; thread_oks ts tas; ts t = None ⟧ ⟹ ∃m .NewThread t x m ∈ set tas ∧ w = no_wait_locks" proof(induct tas arbitrary: ts) case Nil thus ?case by simp next case (Cons TA TAS TS) note IH = ‹⋀ts. ⟦redT_updTs ts TAS t = ⌊(x, w)⌋; thread_oks ts TAS; ts t = None⟧ ⟹ ∃m. NewThread t x m ∈ set TAS ∧ w = no_wait_locks› note es't = ‹redT_updTs TS (TA # TAS) t = ⌊(x, w)⌋› note cct = ‹thread_oks TS (TA # TAS)› hence cctta: "thread_ok TS TA" and ccts: "thread_oks (redT_updT TS TA) TAS" by auto note est = ‹TS t = None› { fix X W assume rest: "redT_updT TS TA t = ⌊(X, W)⌋" then obtain m where "TA = NewThread t X m ∧ W = no_wait_locks" using cctta est by (auto dest!: redT_updT_new_thread) then obtain "TA = NewThread t X m" "W = no_wait_locks" .. moreover from rest ccts have "redT_updTs TS (TA # TAS) t = ⌊(X, W)⌋" by(auto intro:redT_updTs_Some) with es't have "X = x" "W = w" by auto ultimately have ?case by auto } moreover { assume rest: "redT_updT TS TA t = None" hence "⋀m. TA ≠ NewThread t x m" using est cct by(clarsimp) with rest ccts es't have ?case by(auto dest: IH) } ultimately show ?case by(cases "redT_updT TS TA t", auto) qed lemma redT_updT_upd: "⟦ ts t = ⌊xw⌋; thread_ok ts ta ⟧ ⟹ redT_updT ts ta(t ↦ xw') = redT_updT (ts(t ↦ xw')) ta" by(cases ta)(fastforce intro: fun_upd_twist)+ lemma redT_updTs_upd: "⟦ ts t = ⌊xw⌋; thread_oks ts tas ⟧ ⟹ redT_updTs ts tas(t ↦ xw') = redT_updTs (ts(t ↦ xw')) tas" by(induct ts tas rule: redT_updTs.induct)(auto simp del: fun_upd_apply simp add: redT_updT_upd dest: redT_updT_Some) lemma thread_ok_upd: "ts t = ⌊xln⌋ ⟹ thread_ok (ts(t ↦ xln')) ta = thread_ok ts ta" by(rule thread_ok_ts_change) simp lemma thread_oks_upd: "ts t = ⌊xln⌋ ⟹ thread_oks (ts(t ↦ xln')) tas = thread_oks ts tas" by(rule thread_oks_ts_change) simp lemma thread_ok_convert_new_thread_action [simp]: "thread_ok ts (convert_new_thread_action f ta) = thread_ok ts ta" by(cases ta) auto lemma redT_updT'_convert_new_thread_action_eq_None: "redT_updT' ts (convert_new_thread_action f ta) t = None ⟷ redT_updT' ts ta t = None" by(cases ta) auto lemma thread_oks_convert_new_thread_action [simp]: "thread_oks ts (map (convert_new_thread_action f) tas) = thread_oks ts tas" by(induct ts tas rule: thread_oks.induct)(simp_all add: thread_oks_ts_change[OF redT_updT'_convert_new_thread_action_eq_None]) lemma map_redT_updT: "map_option (map_prod f id) (redT_updT ts ta t) = redT_updT (λt. map_option (map_prod f id) (ts t)) (convert_new_thread_action f ta) t" by(cases ta) auto lemma map_redT_updTs: "map_option (map_prod f id) (redT_updTs ts tas t) = redT_updTs (λt. map_option (map_prod f id) (ts t)) (map (convert_new_thread_action f) tas) t" by(induct tas arbitrary: ts)(auto simp add: map_redT_updT) end  # Theory FWWait (* Title: JinjaThreads/Framework/FWWait.thy Author: Andreas Lochbihler *) section ‹Semantics of the thread actions for wait, notify and interrupt› theory FWWait imports FWState begin text ‹Update functions for the wait sets in the multithreaded state› inductive redT_updW :: "'t ⇒ ('w, 't) wait_sets ⇒ ('t,'w) wait_set_action ⇒ ('w,'t) wait_sets ⇒ bool" for t :: 't and ws :: "('w, 't) wait_sets" where "ws t' = ⌊InWS w⌋ ⟹ redT_updW t ws (Notify w) (ws(t' ↦ PostWS WSNotified))" | "(⋀t'. ws t' ≠ ⌊InWS w⌋) ⟹ redT_updW t ws (Notify w) ws" | "redT_updW t ws (NotifyAll w) (λt. if ws t = ⌊InWS w⌋ then ⌊PostWS WSNotified⌋ else ws t)" | "redT_updW t ws (Suspend w) (ws(t ↦ InWS w))" | "ws t' = ⌊InWS w⌋ ⟹ redT_updW t ws (WakeUp t') (ws(t' ↦ PostWS WSInterrupted))" | "(⋀w. ws t' ≠ ⌊InWS w⌋) ⟹ redT_updW t ws (WakeUp t') ws" | "redT_updW t ws Notified (ws(t := None))" | "redT_updW t ws WokenUp (ws(t := None))" definition redT_updWs :: "'t ⇒ ('w,'t) wait_sets ⇒ ('t,'w) wait_set_action list ⇒ ('w,'t) wait_sets ⇒ bool" where "redT_updWs t = rtrancl3p (redT_updW t)" inductive_simps redT_updW_simps [simp]: "redT_updW t ws (Notify w) ws'" "redT_updW t ws (NotifyAll w) ws'" "redT_updW t ws (Suspend w) ws'" "redT_updW t ws (WakeUp t') ws'" "redT_updW t ws WokenUp ws'" "redT_updW t ws Notified ws'" lemma redT_updW_total: "∃ws'. redT_updW t ws wa ws'" by(cases wa)(auto simp add: redT_updW.simps) lemma redT_updWs_total: "∃ws'. redT_updWs t ws was ws'" proof(induct was rule: rev_induct) case Nil thus ?case by(auto simp add: redT_updWs_def) next case (snoc wa was) then obtain ws' where "redT_updWs t ws was ws'" .. also from redT_updW_total[of t ws' wa] obtain ws'' where "redT_updW t ws' wa ws''" .. ultimately show ?case unfolding redT_updWs_def by(auto intro: rtrancl3p_step) qed lemma redT_updWs_trans: "⟦ redT_updWs t ws was ws'; redT_updWs t ws' was' ws'' ⟧ ⟹ redT_updWs t ws (was @ was') ws''" unfolding redT_updWs_def by(rule rtrancl3p_trans) lemma redT_updW_None_implies_None: "⟦ redT_updW t' ws wa ws'; ws t = None; t ≠ t' ⟧ ⟹ ws' t = None" by(auto simp add: redT_updW.simps) lemma redT_updWs_None_implies_None: assumes "redT_updWs t' ws was ws'" and "t ≠ t'" and "ws t = None" shows "ws' t = None" using ‹redT_updWs t' ws was ws'› ‹ws t = None› unfolding redT_updWs_def by induct(auto intro: redT_updW_None_implies_None[OF _ _ ‹t ≠ t'›]) lemma redT_updW_PostWS_imp_PostWS: "⟦ redT_updW t ws wa ws'; ws t'' = ⌊PostWS w⌋; t'' ≠ t ⟧ ⟹ ws' t'' = ⌊PostWS w⌋" by(auto simp add: redT_updW.simps) lemma redT_updWs_PostWS_imp_PostWS: "⟦ redT_updWs t ws was ws'; t'' ≠ t; ws t'' = ⌊PostWS w⌋ ⟧ ⟹ ws' t'' = ⌊PostWS w⌋" unfolding redT_updWs_def by(induct rule: rtrancl3p.induct)(auto dest: redT_updW_PostWS_imp_PostWS) lemma redT_updW_Some_otherD: "⟦ redT_updW t' ws wa ws'; ws' t = ⌊w⌋; t ≠ t' ⟧ ⟹ (case w of InWS w' ⇒ ws t = ⌊InWS w'⌋ | _ ⇒ ws t = ⌊w⌋ ∨ (∃w'. ws t = ⌊InWS w'⌋))" by(auto simp add: redT_updW.simps split: if_split_asm wait_set_status.split) lemma redT_updWs_Some_otherD: "⟦ redT_updWs t' ws was ws'; ws' t = ⌊w⌋; t ≠ t' ⟧ ⟹ (case w of InWS w' ⇒ ws t = ⌊InWS w'⌋ | _ ⇒ ws t = ⌊w⌋ ∨ (∃w'. ws t = ⌊InWS w'⌋))" unfolding redT_updWs_def apply(induct arbitrary: w rule: rtrancl3p.induct) apply(fastforce split: wait_set_status.splits dest: redT_updW_Some_otherD)+ done lemma redT_updW_None_SomeD: "⟦ redT_updW t ws wa ws'; ws' t' = ⌊w⌋; ws t' = None ⟧ ⟹ t = t' ∧ (∃w'. w = InWS w' ∧ wa = Suspend w')" by(auto simp add: redT_updW.simps split: if_split_asm) lemma redT_updWs_None_SomeD: "⟦ redT_updWs t ws was ws'; ws' t' = ⌊w⌋; ws t' = None ⟧ ⟹ t = t' ∧ (∃w'. Suspend w' ∈ set was)" unfolding redT_updWs_def proof(induct arbitrary: w rule: rtrancl3p.induct) case (rtrancl3p_refl ws) thus ?case by simp next case (rtrancl3p_step ws was ws' wa ws'') show ?case proof(cases "ws' t'") case None from redT_updW_None_SomeD[OF ‹redT_updW t ws' wa ws''›, OF ‹ws'' t' = ⌊w⌋› this] show ?thesis by auto next case (Some w') with ‹ws t' = None› rtrancl3p_step.hyps(2) show ?thesis by auto qed qed lemma redT_updW_neq_Some_SomeD: "⟦ redT_updW t' ws wa ws'; ws' t = ⌊InWS w⌋; ws t ≠ ⌊InWS w⌋ ⟧ ⟹ t = t' ∧ wa = Suspend w" by(auto simp add: redT_updW.simps split: if_split_asm) lemma redT_updWs_neq_Some_SomeD: "⟦ redT_updWs t ws was ws'; ws' t' = ⌊InWS w⌋; ws t' ≠ ⌊InWS w⌋ ⟧ ⟹ t = t' ∧ Suspend w ∈ set was" unfolding redT_updWs_def proof(induct rule: rtrancl3p.induct) case rtrancl3p_refl thus ?case by simp next case (rtrancl3p_step ws was ws' wa ws'') show ?case proof(cases "ws' t' = ⌊InWS w⌋") case True with ‹ws t' ≠ ⌊InWS w⌋› ‹⟦ws' t' = ⌊InWS w⌋; ws t' ≠ ⌊InWS w⌋⟧ ⟹ t = t' ∧ Suspend w ∈ set was› show ?thesis by simp next case False with ‹redT_updW t ws' wa ws''› ‹ws'' t' = ⌊InWS w⌋› have "t' = t ∧ wa = Suspend w" by(rule redT_updW_neq_Some_SomeD) thus ?thesis by auto qed qed lemma redT_updW_not_Suspend_Some: "⟦ redT_updW t ws wa ws'; ws' t = ⌊w'⌋; ws t = ⌊w⌋; ⋀w. wa ≠ Suspend w ⟧ ⟹ w' = w ∨ (∃w'' w'''. w = InWS w'' ∧ w' = PostWS w''')" by(auto simp add: redT_updW.simps split: if_split_asm) lemma redT_updWs_not_Suspend_Some: "⟦ redT_updWs t ws was ws'; ws' t = ⌊w'⌋; ws t = ⌊w⌋; ⋀w. Suspend w ∉ set was ⟧ ⟹ w' = w ∨ (∃w'' w'''. w = InWS w'' ∧ w' = PostWS w''')" unfolding redT_updWs_def proof(induct arbitrary: w rule: rtrancl3p_converse_induct) case refl thus ?case by simp next case (step ws wa ws' was ws'') note ‹ws'' t = ⌊w'⌋› moreover have "ws' t ≠ None" proof assume "ws' t = None" with ‹rtrancl3p (redT_updW t) ws' was ws''› ‹ws'' t = ⌊w'⌋› obtain w' where "Suspend w' ∈ set was" unfolding redT_updWs_def[symmetric] by(auto dest: redT_updWs_None_SomeD) with ‹Suspend w' ∉ set (wa # was)› show False by simp qed then obtain w'' where "ws' t = ⌊w''⌋" by auto moreover { fix w from ‹Suspend w ∉ set (wa # was)› have "Suspend w ∉ set was" by simp } ultimately have "w' = w'' ∨ (∃w''' w''''. w'' = InWS w''' ∧ w' = PostWS w'''')" by(rule step.hyps) moreover { fix w from ‹Suspend w ∉ set (wa # was)› have "wa ≠ Suspend w" by auto } note redT_updW_not_Suspend_Some[OF ‹redT_updW t ws wa ws'›, OF ‹ws' t = ⌊w''⌋› ‹ws t = ⌊w⌋› this] ultimately show ?case by auto qed lemma redT_updWs_WokenUp_SuspendD: "⟦ redT_updWs t ws was ws'; Notified ∈ set was ∨ WokenUp ∈ set was; ws' t = ⌊w⌋ ⟧ ⟹ ∃w. Suspend w ∈ set was" unfolding redT_updWs_def by(induct rule: rtrancl3p_converse_induct)(auto dest: redT_updWs_None_SomeD[unfolded redT_updWs_def]) lemma redT_updW_Woken_Up_same_no_Notified_Interrupted: "⟦ redT_updW t ws wa ws'; ws' t = ⌊PostWS w⌋; ws t = ⌊PostWS w⌋; ⋀w. wa ≠ Suspend w ⟧ ⟹ wa ≠ Notified ∧ wa ≠ WokenUp" by(fastforce) lemma redT_updWs_Woken_Up_same_no_Notified_Interrupted: "⟦ redT_updWs t ws was ws'; ws' t = ⌊PostWS w⌋; ws t = ⌊PostWS w⌋; ⋀w. Suspend w ∉ set was ⟧ ⟹ Notified ∉ set was ∧ WokenUp ∉ set was" unfolding redT_updWs_def proof(induct rule: rtrancl3p_converse_induct) case refl thus ?case by simp next case (step ws wa ws' was ws'') note Suspend = ‹⋀w. Suspend w ∉ set (wa # was)› note ‹ws'' t = ⌊PostWS w⌋› moreover have "ws' t = ⌊PostWS w⌋" proof(cases "ws' t") case None with ‹rtrancl3p (redT_updW t) ws' was ws''› ‹ws'' t = ⌊PostWS w⌋› obtain w where "Suspend w ∈ set was" unfolding redT_updWs_def[symmetric] by(auto dest: redT_updWs_None_SomeD) with Suspend[of w] have False by simp thus ?thesis .. next case (Some w') thus ?thesis using ‹ws t = ⌊PostWS w⌋› Suspend ‹redT_updW t ws wa ws'› by(auto simp add: redT_updW.simps split: if_split_asm) qed moreover { fix w from Suspend[of w] have "Suspend w ∉ set was" by simp } ultimately have "Notified ∉ set was ∧ WokenUp ∉ set was" by(rule step.hyps) moreover { fix w from Suspend[of w] have "wa ≠ Suspend w" by auto } with ‹redT_updW t ws wa ws'› ‹ws' t = ⌊PostWS w⌋› ‹ws t = ⌊PostWS w⌋› have "wa ≠ Notified ∧ wa ≠ WokenUp" by(rule redT_updW_Woken_Up_same_no_Notified_Interrupted) ultimately show ?case by auto qed text ‹Preconditions for wait set actions› definition wset_actions_ok :: "('w,'t) wait_sets ⇒ 't ⇒ ('t,'w) wait_set_action list ⇒ bool" where "wset_actions_ok ws t was ⟷ (if Notified ∈ set was then ws t = ⌊PostWS WSNotified⌋ else if WokenUp ∈ set was then ws t = ⌊PostWS WSWokenUp⌋ else ws t = None)" lemma wset_actions_ok_Nil [simp]: "wset_actions_ok ws t [] ⟷ ws t = None" by(simp add: wset_actions_ok_def) definition waiting :: "'w wait_set_status option ⇒ bool" where "waiting w ⟷ (∃w'. w = ⌊InWS w'⌋)" lemma not_waiting_iff: "¬ waiting w ⟷ w = None ∨ (∃w'. w = ⌊PostWS w'⌋)" apply(cases "w") apply(case_tac [2] a) apply(auto simp add: waiting_def) done lemma waiting_code [code]: "waiting None = False" "⋀w. waiting ⌊PostWS w⌋ = False" "⋀w. waiting ⌊InWS w⌋ = True" by(simp_all add: waiting_def) end  # Theory FWCondAction (* Title: JinjaThreads/Framework/FWCondAction.thy Author: Andreas Lochbihler *) section ‹Semantics of the thread actions for purely conditional purpose such as Join› theory FWCondAction imports FWState begin locale final_thread = fixes final :: "'x ⇒ bool" begin primrec cond_action_ok :: "('l,'t,'x,'m,'w) state ⇒ 't ⇒ 't conditional_action ⇒ bool" where "⋀ln. cond_action_ok s t (Join T) = (case thr s T of None ⇒ True | ⌊(x, ln)⌋ ⇒ t ≠ T ∧ final x ∧ ln = no_wait_locks ∧ wset s T = None)" | "cond_action_ok s t Yield = True" primrec cond_action_oks :: "('l,'t,'x,'m,'w) state ⇒ 't ⇒ 't conditional_action list ⇒ bool" where "cond_action_oks s t [] = True" | "cond_action_oks s t (ct#cts) = (cond_action_ok s t ct ∧ cond_action_oks s t cts)" lemma cond_action_oks_append [simp]: "cond_action_oks s t (cts @ cts') ⟷ cond_action_oks s t cts ∧ cond_action_oks s t cts'" by(induct cts, auto) lemma cond_action_oks_conv_set: "cond_action_oks s t cts ⟷ (∀ct ∈ set cts. cond_action_ok s t ct)" by(induct cts) simp_all lemma cond_action_ok_Join: "⋀ln. ⟦ cond_action_ok s t (Join T); thr s T = ⌊(x, ln)⌋ ⟧ ⟹ final x ∧ ln = no_wait_locks ∧ wset s T = None" by(auto) lemma cond_action_oks_Join: "⋀ln. ⟦ cond_action_oks s t cas; Join T ∈ set cas; thr s T = ⌊(x, ln)⌋ ⟧ ⟹ final x ∧ ln = no_wait_locks ∧ wset s T = None ∧ t ≠ T" by(induct cas)(auto) lemma cond_action_oks_upd: assumes tst: "thr s t = ⌊xln⌋" shows "cond_action_oks (locks s, (thr s(t ↦ xln'), shr s), wset s, interrupts s) t cas = cond_action_oks s t cas" proof(induct cas) case Nil thus ?case by simp next case (Cons ca cas) from tst have eq: "cond_action_ok (locks s, (thr s(t ↦ xln'), shr s), wset s, interrupts s) t ca = cond_action_ok s t ca" by(cases ca) auto with Cons show ?case by(auto simp del: fun_upd_apply) qed lemma cond_action_ok_shr_change: "cond_action_ok (ls, (ts, m), ws, is) t ct ⟹ cond_action_ok (ls, (ts, m'), ws, is) t ct" by(cases ct) auto lemma cond_action_oks_shr_change: "cond_action_oks (ls, (ts, m), ws, is) t cts ⟹ cond_action_oks (ls, (ts, m'), ws, is) t cts" by(auto simp add: cond_action_oks_conv_set intro: cond_action_ok_shr_change) primrec cond_action_ok' :: "('l,'t,'x,'m,'w) state ⇒ 't ⇒ 't conditional_action ⇒ bool" where "cond_action_ok' _ _ (Join t) = True" | "cond_action_ok' _ _ Yield = True" primrec cond_action_oks' :: "('l,'t,'x,'m,'w) state ⇒ 't ⇒ 't conditional_action list ⇒ bool" where "cond_action_oks' s t [] = True" | "cond_action_oks' s t (ct#cts) = (cond_action_ok' s t ct ∧ cond_action_oks' s t cts)" lemma cond_action_oks'_append [simp]: "cond_action_oks' s t (cts @ cts') ⟷ cond_action_oks' s t cts ∧ cond_action_oks' s t cts'" by(induct cts, auto) lemma cond_action_oks'_subset_Join: "set cts ⊆ insert Yield (range Join) ⟹ cond_action_oks' s t cts" apply(induct cts) apply(auto) done end definition collect_cond_actions :: "'t conditional_action list ⇒ 't set" where "collect_cond_actions cts = {t. Join t ∈ set cts}" declare collect_cond_actions_def [simp] lemma cond_action_ok_final_change: "⟦ final_thread.cond_action_ok final1 s1 t ca; ⋀t. thr s1 t = None ⟷ thr s2 t = None; ⋀t x1. ⟦ thr s1 t = ⌊(x1, no_wait_locks)⌋; final1 x1; wset s1 t = None ⟧ ⟹ ∃x2. thr s2 t = ⌊(x2, no_wait_locks)⌋ ∧ final2 x2 ∧ ln2 = no_wait_locks ∧ wset s2 t = None ⟧ ⟹ final_thread.cond_action_ok final2 s2 t ca" apply(cases ca) apply(fastforce simp add: final_thread.cond_action_ok.simps)+ done lemma cond_action_oks_final_change: assumes major: "final_thread.cond_action_oks final1 s1 t cas" and minor: "⋀t. thr s1 t = None ⟷ thr s2 t = None" "⋀t x1. ⟦ thr s1 t = ⌊(x1, no_wait_locks)⌋; final1 x1; wset s1 t = None ⟧ ⟹ ∃x2. thr s2 t = ⌊(x2, no_wait_locks)⌋ ∧ final2 x2 ∧ ln2 = no_wait_locks ∧ wset s2 t = None" shows "final_thread.cond_action_oks final2 s2 t cas" using major by(induct cas)(auto simp add: final_thread.cond_action_oks.simps intro: cond_action_ok_final_change[OF _ minor]) end  # Theory FWWellform (* Title: JinjaThreads/Framework/FWWellform.thy Author: Andreas Lochbihler *) section ‹Wellformedness conditions for the multithreaded state› theory FWWellform imports FWLocking FWThread FWWait FWCondAction begin text‹Well-formedness property: Locks are held by real threads› definition lock_thread_ok :: "('l, 't) locks ⇒ ('l, 't,'x) thread_info ⇒ bool" where [code del]: "lock_thread_ok ls ts ≡ ∀l t. has_lock (ls$ l) t ⟶ (∃xw. ts t = ⌊xw⌋)"

"lock_thread_ok ls ts = finfun_All ((λl. case l of None ⇒ True | ⌊(t, n)⌋ ⇒ (ts t ≠ None)) ∘$ls)" by(simp add: lock_thread_ok_def finfun_All_All has_lock_has_locks_conv has_locks_iff o_def) lemma lock_thread_okI: "(⋀l t. has_lock (ls$ l) t ⟹ ∃xw. ts t = ⌊xw⌋) ⟹ lock_thread_ok ls ts"

"⟦ lock_thread_ok ls ts; has_lock (ls $l) t ⟧ ⟹ ∃xw. ts t = ⌊xw⌋" by(fastforce simp add: lock_thread_ok_def) lemma lock_thread_okD': "⟦ lock_thread_ok ls ts; has_locks (ls$ l) t = Suc n ⟧ ⟹ ∃xw. ts t = ⌊xw⌋"
by(auto elim: lock_thread_okD[where l=l] simp del: split_paired_Ex)

"⟦ lock_thread_ok ls ts; ∀l t. has_lock (ls $l) t ⟶ (∃xw. ts t = ⌊xw⌋) ⟹ P ⟧ ⟹ P" by(auto simp add: lock_thread_ok_def simp del: split_paired_Ex) lemma lock_thread_ok_upd: "lock_thread_ok ls ts ⟹ lock_thread_ok ls (ts(t ↦ xw))" by(auto intro!: lock_thread_okI dest: lock_thread_okD) lemma lock_thread_ok_has_lockE: assumes "lock_thread_ok ls ts" and "has_lock (ls$ l) t"
obtains x ln' where "ts t = ⌊(x, ln')⌋"
using assms

and tst: "ts t = ⌊xw⌋"
shows "lock_thread_ok (redT_updLs ls t las) ts"
fix L T
assume ru: "has_lock (redT_updLs ls t las $L) T" show "∃xw. ts T = ⌊xw⌋" proof(cases "t = T") case True thus ?thesis using tst lto by(auto elim: lock_thread_okE) next case False with ru have "has_lock (ls$ L) T"
thus ?thesis using lto
by(auto elim!: lock_thread_okE simp del: split_paired_Ex)
qed
qed

shows "lock_thread_ok ls (redT_updTs ts nts)"
fix l t
assume "has_lock (ls $l) t" with lto have "∃xw. ts t = ⌊xw⌋" by(auto elim!: lock_thread_okE simp del: split_paired_Ex) thus "∃xw. redT_updTs ts nts t = ⌊xw⌋" by(auto intro: redT_updTs_Some1 simp del: split_paired_Ex) qed lemma lock_thread_ok_has_lock: assumes "lock_thread_ok ls ts" and "has_lock (ls$ l) t"
obtains xw where "ts t = ⌊xw⌋"
using assms

"⟦ lock_thread_ok ls ts; ts t = None ⟧ ⟹ has_locks (ls \$ l) t = 0"

⟹ lock_thread_ok (redT_updLs ls t las) (redT_updTs ts tas(t ↦ xw'))"
apply(clarsimp simp del: split_paired_Ex)
apply(drule has_lock_upd_locks_implies_has_lock, simp)
apply(erule exE)
by(rule redT_updTs_Some1)

fixes ln
shows "⟦ lock_thread_ok ls ts; ts t = ⌊(x, ln)⌋ ⟧ ⟹ lock_thread_ok (acquire_all ls t ln) (ts(t ↦ xw))"

text ‹Well-formedness condition: Wait sets contain only real threads›

definition wset_thread_ok :: "('w, 't) wait_sets ⇒ ('l, 't, 'x) thread_info ⇒ bool"
where "wset_thread_ok ws ts ≡ ∀t. ts t = None ⟶ ws t = None"

"(⋀t. ts t = None ⟹ ws t = None) ⟹ wset_thread_ok ws ts"

"⟦ wset_thread_ok ws ts; ts t = None ⟧ ⟹ ws t = None"

"wset_thread_ok ws ts ⟷ dom ws ⊆ dom ts"

"⟦ wset_thread_ok ws ts; ts t = ⌊xln⌋ ⟧ ⟹ wset_thread_ok (ws(t := w)) ts"

"wset_thread_ok ws ts ⟹ wset_thread_ok (λt. if ws t = ⌊w t⌋ then ⌊w' t⌋ else ws t) ts"

shows "wset_thread_ok ws (redT_updTs ts nts)"
fix t
assume "redT_updTs ts nts t = None"
hence "ts t = None" by(rule redT_updTs_None)
with wto show "ws t = None" by(rule wset_thread_okD)
qed

"⟦ wset_thread_ok ws ts; redT_updW t ws wa ws'; ts t = ⌊xln⌋ ⟧ ⟹ wset_thread_ok ws' ts"

"⟦ wset_thread_ok ws ts; redT_updWs t ws was ws'; ts t = ⌊xln⌋ ⟧ ⟹ wset_thread_ok ws' ts"
unfolding redT_updWs_def apply(rotate_tac 1)

text ‹Well-formedness condition: Wait sets contain only non-final threads›

definition wset_final_ok :: "('w, 't) wait_sets ⇒ ('l, 't, 'x) thread_info ⇒ bool"
where "wset_final_ok ws ts ⟷ (∀t ∈ dom ws. ∃x ln. ts t = ⌊(x, ln)⌋ ∧ ¬ final x)"

lemma wset_final_okI:
"(⋀t w. ws t = ⌊w⌋ ⟹ ∃x ln. ts t = ⌊(x, ln)⌋ ∧ ¬ final x) ⟹ wset_final_ok ws ts"
unfolding wset_final_ok_def by(blast)

lemma wset_final_okD:
"⟦ wset_final_ok ws ts; ws t = ⌊w⌋ ⟧ ⟹ ∃x ln. ts t = ⌊(x, ln)⌋ ∧ ¬ final x"
unfolding wset_final_ok_def by(blast)

lemma wset_final_okE:
assumes "wset_final_ok ws ts" "ws t = ⌊w⌋"
and "⋀x ln. ts t = ⌊(x, ln)⌋ ⟹ ¬ final x ⟹ thesis"
shows thesis
using assms by(blast dest: wset_final_okD)

"wset_final_ok ws ts ⟹ wset_thread_ok ws ts"

(*  Title:      JinjaThreads/Framework/FWLockingThread.thy
Author:     Andreas Lochbihl