Theory FWLock

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

header {* \isaheader{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: split_if_asm Product_Type.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"]

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: split_if_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: split_if_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"
apply(cases l, auto split: split_if_asm elim!: may_lock.cases intro: may_lock.intros split:Nat.split_asm )
apply(case_tac n, auto intro: may_lock.intros)
done

lemma may_lock_release_all_conv [simp]:
  "may_lock (release_all l t) t = may_lock l t"
by(cases l, auto split: split_if_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"
apply(cases l, auto)
apply(case_tac b, auto)
done

lemma has_lock_lock_lock_unlock_lock_id [simp]:
  "has_lock l t ==> lock_lock (unlock_lock l) t = l"
apply(cases l, auto split: split_if_asm)
apply(case_tac b, auto)
done

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: split_if_asm)
qed


lemma has_lock_upd_lock_implies_has_lock:
  "[| has_lock (upd_lock l t L) t'; t ≠ t' |] ==> has_lock l t'"
apply(cases l)
 apply(cases L, auto)
apply(cases L, auto split: split_if_asm)
apply(case_tac b, auto split: split_if_asm)
done

lemma has_lock_upd_locks_implies_has_lock:
  assumes ul: "has_lock (upd_locks l t Ls) t'"
  and tt': "t ≠ t'"
  shows "has_lock l t'"
using ul
proof(induct Ls arbitrary: l)
  case Nil thus ?case by simp
next
  case (Cons L Ls l)
  from `has_lock (upd_locks l t (L # Ls)) t'`
  have "has_lock (upd_locks (upd_lock l t L) t Ls) t'" by simp
  with `!!l. has_lock (upd_locks l t Ls) t' ==> has_lock l t'`
  have "has_lock (upd_lock l t L) t'" .
  with tt' show ?case
    by -(rule has_lock_upd_lock_implies_has_lock)
qed

(* 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 not_lock_actions_ok_conv:
  "!!l. (¬ lock_actions_ok l t las) = (∃xs L ys. las = xs @ L # ys ∧ lock_actions_ok l t xs ∧ ¬ lock_action_ok (upd_locks l t xs) t L)"
  (is "!!l. ?lhs l = ?rhs l")
proof(induct las arbitrary: l)
  case Nil thus ?case by(simp)
next
  case (Cons la las l)
  note IH = `(¬ lock_actions_ok (upd_lock l t la) t las) =
              (∃xs L ys. las = xs @ L # ys ∧ lock_actions_ok (upd_lock l t la) t xs 
                      ∧ ¬ lock_action_ok (upd_locks (upd_lock l t la) t xs) t L)`
  show ?case
  proof(cases "lock_action_ok l t la")
    case True
    hence "(¬ lock_actions_ok l t (la # las)) = (¬ lock_actions_ok (upd_lock l t la) t las)"
      by auto
    also note IH
    also have "(∃xs L ys. las = xs @ L # ys ∧ lock_actions_ok (upd_lock l t la) t xs ∧ ¬ lock_action_ok (upd_locks (upd_lock l t la) t xs) t L) = 
               (∃xs L ys. la # las = xs @ L # ys ∧ lock_actions_ok l t xs ∧ ¬ lock_action_ok (upd_locks l t xs) t L)"
    proof(rule iffI)
      assume "∃xs L ys. las = xs @ L # ys ∧ lock_actions_ok (upd_lock l t la) t xs ∧ ¬ lock_action_ok (upd_locks (upd_lock l t la) t xs) t L"
      then obtain xs L ys
        where "las = xs @ L # ys"
        and "lock_actions_ok (upd_lock l t la) t xs"
        and "¬ lock_action_ok (upd_locks (upd_lock l t la) t xs) t L"
        by blast
      with True 
      have "(la # las) = (la # xs) @ L # ys"
        and "lock_actions_ok l t (la # xs)"
        and "¬ lock_action_ok (upd_locks l t (la # xs)) t L"
        by(auto)
      thus "∃xs L ys. la # las = xs @ L # ys ∧ lock_actions_ok l t xs ∧ ¬ lock_action_ok (upd_locks l t xs) t L"
        by blast
    next
      assume "∃xs L ys. la # las = xs @ L # ys ∧ lock_actions_ok l t xs ∧ ¬ lock_action_ok (upd_locks l t xs) t L"
      then obtain xs L ys
        where "la # las = xs @ L # ys"
        and "lock_actions_ok l t xs"
        and "¬ lock_action_ok (upd_locks l t xs) t L"
        by blast
      moreover
      with True have "xs ≠ []" by(auto)
      then obtain la' xs' where "xs = la' # xs'" by(cases xs, auto)
      ultimately
      have "las = xs' @ L # ys"
        and "lock_actions_ok (upd_lock l t la) t xs'"
        and "¬ lock_action_ok (upd_locks (upd_lock l t la) t xs') t L"
        by(auto)
      thus "∃xs L ys. las = xs @ L # ys ∧ lock_actions_ok (upd_lock l t la) t xs ∧ ¬ lock_action_ok (upd_locks (upd_lock l t la) t xs) t L" by blast
    qed
    finally show ?thesis .
  next
    case False
    hence "¬ lock_actions_ok l t (la # las)" by simp
    moreover
    with False have "la # las = [] @ la # las"
      and "lock_actions_ok l t []"
      and "¬ lock_action_ok (upd_locks l t []) t la"
      by (auto)
    ultimately show ?thesis
      by blast
  qed
qed


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 Ls arbitrary: l, auto)

lemma lock_actions_ok_Lock_may_lock:
  "[| lock_actions_ok l t Ls; Lock ∈ set Ls |] ==> may_lock l t"
by(induct Ls arbitrary: l, fastsimp+)

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"
apply(cases l, auto split: split_if_asm)
apply(case_tac b, auto)
done

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 n arbitrary: l, auto)

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 Ls arbitrary: l, auto)

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: split_if_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)

lemma lock_actions_ok_not_may_lock_upd_lock:
  "[| lock_actions_ok L t las; ¬ may_lock (upd_locks L t las) t |] ==> set las ⊆ { UnlockFail, ReleaseAcquire }"
proof(induct las arbitrary: L)
  case Nil thus ?case by auto
next
  case (Cons LA LAS l)
  note IH = `!!L. [|lock_actions_ok L t LAS; ¬ may_lock (upd_locks L t LAS) t|] ==> set LAS ⊆ {UnlockFail, ReleaseAcquire}`
  note laos = `lock_actions_ok l t (LA # LAS)`
  hence lao: "lock_action_ok l t LA" by simp
  have "LA = UnlockFail ∨ LA = ReleaseAcquire"
  proof(cases LA)
    case Lock
    with lao have "may_lock l t" by simp
    with laos have "may_lock (upd_locks l t (LA # LAS)) t" by simp
    with `¬ may_lock (upd_locks l t (LA # LAS)) t`
    have False by contradiction
    thus ?thesis ..
  next
    case Unlock
    with lao have "has_lock l t" by simp
    with laos have "may_lock (upd_locks l t (LA # LAS)) t"
      by(auto intro: has_lock_may_lock)
    with `¬ may_lock (upd_locks l t (LA # LAS)) t`
    have False by contradiction
    thus ?thesis ..
  qed(auto)
  moreover from IH[of "upd_lock l t LA"] laos `¬ may_lock (upd_locks l t (LA # LAS)) t`
  have "set LAS ⊆ {UnlockFail, ReleaseAcquire}" by(simp)
  ultimately show ?case by auto
qed



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 las arbitrary: l)
  case Nil thus ?case by simp
next
  case (Cons LA LAS L)
  note IH = `!!l. 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))`
  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
    hence LA: "LA = Lock --> may_lock L t" by simp
    show ?thesis
    proof(rule iffI)
      assume "lock_actions_ok' L t (LA # LAS)"
      with LA have "lock_action_ok L t LA"
        and "lock_actions_ok' (upd_lock L t LA) t LAS" by(auto)
      hence "lock_actions_ok (upd_lock L t LA) t LAS ∨
             (∃xs ys. LAS = xs @ Lock # ys ∧ lock_actions_ok (upd_lock L t LA) t xs ∧
                      ¬ may_lock (upd_locks L t (LA # xs)) t)"
        by(simp add: IH)
      with `lock_action_ok L t LA`
      show "lock_actions_ok L t (LA # LAS) ∨ 
            (∃xs ys. LA # LAS = xs @ Lock # ys ∧ 
                     lock_actions_ok L t xs ∧ ¬ may_lock (upd_locks L t xs) t)"
        apply(auto)
        apply(erule_tac x="LA # xs" in allE)
        by(auto)
    next
      assume "lock_actions_ok L t (LA # LAS) ∨
              (∃xs ys. LA # LAS = xs @ Lock # ys ∧ lock_actions_ok L t xs ∧ ¬ may_lock (upd_locks L t xs) t)"
      with LA
      have "lock_action_ok L t LA ∧ (lock_actions_ok (upd_lock L t LA) t LAS ∨ 
                                     (∃xs ys. LAS = xs @ Lock # ys ∧ lock_actions_ok (upd_lock L t LA) t xs ∧
                                              ¬ may_lock (upd_locks (upd_lock L t LA) t xs) t))"
        by(auto simp add: Cons_eq_append_conv)
      hence "lock_action_ok L t LA ∧ lock_actions_ok' (upd_lock L t LA) t LAS"
        unfolding IH by auto
      with LA show "lock_actions_ok' L t (LA # LAS)" by(auto)
    qed
  qed
qed

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)

lemma not_lock_actions_ok'_conv: 
  "(¬ 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)"
by(auto simp add: lock_actions_ok'_iff)

end