# Theory Language_Semantics

```section ‹Simple While Language with probabilistic choice and parallel execution›

theory Language_Semantics
imports Interface
begin

subsection ‹Preliminaries›

text‹Trivia›

declare zero_le_mult_iff[simp]
declare split_mult_pos_le[simp]
declare zero_le_divide_iff[simp]

lemma in_minus_Un[simp]:
assumes "i ∈ I"
shows "I - {i} Un {i} = I" and "{i} Un (I - {i}) = I"
apply(metis Un_commute assms insert_Diff_single insert_absorb insert_is_Un)
by (metis assms insert_Diff_single insert_absorb insert_is_Un)

lemma less_plus_cases[case_names Left Right]:
assumes
*: "(i::nat) < n1 ⟹ phi" and
**: "⋀ i2. i = n1 + i2 ⟹ phi"
shows phi
proof(cases "i < n1")
case True
thus ?thesis using * by simp
next
case False hence "n1 ≤ i" by simp
then obtain i2 where "i = n1 + i2" by (metis le_iff_add)
thus ?thesis using ** by blast
qed

lemma less_plus_elim[elim!, consumes 1, case_names Left Right]:
assumes i: "(i:: nat) < n1 + n2" and
*: "i < n1 ⟹ phi" and
**: "⋀ i2. ⟦i2 < n2; i = n1 + i2⟧ ⟹ phi"
shows phi
apply(rule less_plus_cases[of i n1])
using assms by auto

lemma nth_append_singl[simp]:
"i < length al ⟹ (al @ [a]) ! i = al ! i"

lemma take_append_singl[simp]:
assumes "n < length al" shows "take n (al @ [a]) = take n al"
using assms by (induct al rule: rev_induct) auto

lemma length_unique_prefix:
"al1 ≤ al ⟹ al2 ≤ al ⟹ length al1 = length al2 ⟹ al1 = al2"
by (metis not_equal_is_parallel parallelE prefix_same_cases less_eq_list_def)

text‹take:›

lemma take_length[simp]:
"take (length al) al = al"
using take_all by auto

lemma take_le:
assumes "n < length al"
shows "take n al @ [al ! n] ≤ al"
by (metis assms take_Suc_conv_app_nth take_is_prefix less_eq_list_def)

lemma list_less_iff_prefix: "a < b ⟷ strict_prefix a b"
by (metis le_less less_eq_list_def less_irrefl prefix_order.le_less prefix_order.less_irrefl)

lemma take_lt:
"n < length al ⟹ take n al < al"
unfolding list_less_iff_prefix
using prefix_order.le_less[of "take n al" al]

lemma le_take:
assumes "n1 ≤ n2"
shows "take n1 al ≤ take n2 al"
using assms proof(induct al arbitrary: n1 n2)
case (Cons a al)
thus ?case
by (cases n1 n2 rule: nat.exhaust[case_product nat.exhaust]) auto
qed auto

lemma inj_take:
assumes "n1 ≤ length al" and "n2 ≤ length al"
shows "take n1 al = take n2 al ⟷ n1 = n2"
proof-
{assume "take n1 al = take n2 al"
hence "n1 = n2"
using assms proof(induct al arbitrary: n1 n2)
case (Cons a al)
thus ?case
by (cases n1 n2 rule: nat.exhaust[case_product nat.exhaust]) auto
qed auto
}
thus ?thesis by auto
qed

lemma lt_take: "n1 < n2 ⟹ n2 ≤ length al ⟹ take n1 al < take n2 al"
by (metis inj_take le_less_trans le_take not_less_iff_gr_or_eq order.not_eq_order_implies_strict order.strict_implies_order)

text‹lsum:›

definition lsum :: "('a ⇒ nat) ⇒ 'a list ⇒ nat" where
"lsum f al ≡ sum_list (map f al)"

lemma lsum_simps[simp]:
"lsum f [] = 0"
"lsum f (al @ [a]) = lsum f al + f a"
unfolding lsum_def by auto

lemma lsum_append:
"lsum f (al @ bl) = lsum f al + lsum f bl"
unfolding lsum_def by auto

lemma lsum_cong[fundef_cong]:
assumes "⋀ a. a ∈ set al ⟹ f a = g a"
shows "lsum f al = lsum g al"
using assms unfolding lsum_def by (metis map_eq_conv)

lemma lsum_gt_0[simp]:
assumes "al ≠ []" and "⋀ a. a ∈ set al ⟹ 0 < f a"
shows "0 < lsum f al"
using assms by (induct rule: rev_induct) auto

lemma lsum_mono[simp]:
assumes "al ≤ bl"
shows "lsum f al ≤ lsum f bl"
proof-
obtain cl where bl: "bl = al @ cl" using assms unfolding prefix_def less_eq_list_def by blast
thus ?thesis unfolding bl lsum_append by simp
qed

lemma lsum_mono2[simp]:
assumes f: "⋀ b. b ∈ set bl ⟹ f b > 0" and le: "al < bl"
shows "lsum f al < lsum f bl"
proof-
obtain cl where bl: "bl = al @ cl" and cl: "cl ≠ []"
using assms unfolding list_less_iff_prefix prefix_def strict_prefix_def by blast
have "lsum f al < lsum f al + lsum f cl"
using f cl unfolding bl by simp
also have "... = lsum f bl" unfolding bl lsum_append by simp
finally show ?thesis .
qed

lemma lsum_take[simp]:
"lsum f (take n al) ≤ lsum f al"
by (metis lsum_mono take_is_prefix less_eq_list_def)

lemma less_lsum_nchotomy:
assumes f: "⋀ a. a ∈ set al ⟹ 0 < f a"
and i: "(i::nat) < lsum f al"
shows "∃ n j. n < length al ∧ j < f (al ! n) ∧ i = lsum f (take n al) + j"
using assms proof(induct rule: rev_induct)
case (snoc a al)
hence i: "i < lsum f al + f a" and
pos: "0 < f a"  "⋀a'. a' ∈ set al ⟹ 0 < f a'" by auto
from i show ?case
proof(cases rule: less_plus_elim)
case Left
then obtain n j where "n < length al ∧ j < f (al ! n) ∧ i = lsum f (take n al) + j"
using pos snoc by auto
thus ?thesis
apply - apply(rule exI[of _ n]) apply(rule exI[of _ j]) by auto
next
case (Right j)
thus ?thesis
apply - apply(rule exI[of _ "length al"]) apply(rule exI[of _ j]) by simp
qed
qed auto

lemma less_lsum_unique:
assumes "⋀ a. a ∈ set al ⟹ (0::nat) < f a"
and "n1 < length al ∧ j1 < f (al ! n1)"
and "n2 < length al ∧ j2 < f (al ! n2)"
and "lsum f (take n1 al) + j1 = lsum f (take n2 al) + j2"
shows "n1 = n2 ∧ j1 = j2"
using assms proof(induct al arbitrary: n1 n2 j1 j2 rule: rev_induct)
case (snoc a al)
hence pos: "0 < f a"   "⋀ a'. a' ∈ set al ⟹ 0 < f a'"
and n1: "n1 < length al + 1" and n2: "n2 < length al + 1" by auto
from n1 show ?case
proof(cases rule: less_plus_elim)
case Left note n1 = Left
hence j1: "j1 < f (al ! n1)" using snoc by auto
obtain al' where al: "al = (take n1 al) @ ((al ! n1) # al')"
using n1 by (metis append_take_drop_id Cons_nth_drop_Suc)
have "j1 < lsum f ((al ! n1) # al')" using pos j1 unfolding lsum_def by simp
hence "lsum f (take n1 al) + j1 < lsum f (take n1 al) + lsum f ((al ! n1) # al')" by simp
also have "... = lsum f al" unfolding lsum_append[THEN sym] using al by simp
finally have lsum1: "lsum f (take n1 al) + j1 < lsum f al" .
from n2 show ?thesis
proof(cases rule: less_plus_elim)
case Left note n2 = Left
hence j2: "j2 < f (al ! n2)" using snoc by auto
show ?thesis apply(rule snoc(1)) using snoc using pos n1 j1 n2 j2 by auto
next
case Right
hence n2: "n2 = length al" by simp
hence j2: "j2 < f a" using snoc by simp
have "lsum f (take n1 al) + j1 = lsum f al + j2" using n1 n2 snoc by simp
hence False using lsum1 by auto
thus ?thesis by simp
qed
next
case Right
hence n1: "n1 = length al" by simp
hence j1: "j1 < f a" using snoc by simp
from n2 show ?thesis
proof(cases rule: less_plus_elim)
case Left note n2 = Left
hence j2: "j2 < f (al ! n2)" using snoc by auto
obtain al' where al: "al = (take n2 al) @ ((al ! n2) # al')"
using n2 by (metis append_take_drop_id Cons_nth_drop_Suc)
have "j2 < lsum f ((al ! n2) # al')" using pos j2 unfolding lsum_def by simp
hence "lsum f (take n2 al) + j2 < lsum f (take n2 al) + lsum f ((al ! n2) # al')" by simp
also have "... = lsum f al" unfolding lsum_append[THEN sym] using al by simp
finally have lsum2: "lsum f (take n2 al) + j2 < lsum f al" .
have "lsum f al + j1 = lsum f (take n2 al) + j2" using n1 n2 snoc by simp
hence False using lsum2 by auto
thus ?thesis by simp
next
case Right
hence n2: "n2 = length al" by simp
have "j1 = j2" using n1 n2 snoc by simp
thus ?thesis using n1 n2 by simp
qed
qed
qed auto

definition locate_pred where
"locate_pred f al (i::nat) n_j ≡
fst n_j < length al ∧
snd n_j < f (al ! (fst n_j)) ∧
i = lsum f (take (fst n_j) al) + (snd n_j)"

definition locate where
"locate f al i ≡ SOME n_j. locate_pred f al i n_j"

definition locate1 where "locate1 f al i ≡ fst (locate f al i)"
definition locate2 where "locate2 f al i ≡ snd (locate f al i)"

lemma locate_pred_ex:
assumes "⋀ a. a ∈ set al ⟹ 0 < f a"
and "i < lsum f al"
shows "∃ n_j. locate_pred f al i n_j"
using assms less_lsum_nchotomy unfolding locate_pred_def by force

lemma locate_pred_unique:
assumes "⋀ a. a ∈ set al ⟹ 0 < f a"
and "locate_pred f al i n1_j1" "locate_pred f al i n2_j2"
shows "n1_j1 = n2_j2"
using assms less_lsum_unique unfolding locate_pred_def
apply(cases n1_j1, cases n2_j2) apply simp by blast

lemma locate_locate_pred:
assumes "⋀ a. a ∈ set al ⟹ (0::nat) < f a"
and "i < lsum f al"
shows "locate_pred f al i (locate f al i)"
proof-
obtain n_j where "locate_pred f al i n_j"
using assms locate_pred_ex[of al f i] by auto
thus ?thesis unfolding locate_def apply(intro someI[of "locate_pred f al i"]) by blast
qed

lemma locate_locate_pred_unique:
assumes "⋀ a. a ∈ set al ⟹ (0::nat) < f a"
and "locate_pred f al i n_j"
shows "n_j = locate f al i"
unfolding locate_def apply(rule sym, rule some_equality)
using assms locate_locate_pred apply force
using assms locate_pred_unique by blast

lemma locate:
assumes "⋀ a. a ∈ set al ⟹ 0 < f a"
and "i < lsum f al"
shows "locate1 f al i < length al ∧
locate2 f al i < f (al ! (locate1 f al i)) ∧
i = lsum f (take (locate1 f al i) al) + (locate2 f al i)"
using assms locate_locate_pred
unfolding locate1_def locate2_def locate_pred_def by auto

lemma locate_unique:
assumes "⋀ a. a ∈ set al ⟹ 0 < f a"
and "n < length al" and "j < f (al ! n)" and "i = lsum f (take n al) + j"
shows "n = locate1 f al i ∧ j = locate2 f al i"
proof-
define n_j where "n_j = (n,j)"
have "locate_pred f al i n_j" using assms unfolding n_j_def locate_pred_def by auto
hence "n_j = locate f al i" using assms locate_locate_pred_unique by blast
thus ?thesis unfolding n_j_def locate1_def locate2_def by (metis fst_conv n_j_def snd_conv)
qed

text‹sum:›

lemma sum_2[simp]:
"sum f {..< 2} = f 0 + f (Suc 0)"
proof-
have "{..< 2} = {0, Suc 0}" by auto
thus ?thesis by force
qed

lemma inj_Plus[simp]:
"inj ((+) (a::nat))"
unfolding inj_on_def by auto

lemma inj_on_Plus[simp]:
"inj_on ((+) (a::nat)) A"
unfolding inj_on_def by auto

lemma Plus_int[simp]:
fixes a :: nat
shows "(+) b ` {..< a} = {b ..< b + a}"
proof safe
fix x::nat assume "x ∈ {b..< b + a}"
hence "b ≤ x" and x: "x < a + b" by auto
then obtain y where xb: "x = b + y" by (metis le_iff_add)
hence "y < a" using x by simp
thus "x ∈ (+) b ` {..<a}" using xb by auto
qed auto

lemma sum_minus[simp]:
fixes a :: nat
shows "sum f {a ..< a + b} = sum (%x. f (a + x)) {..< b}"
using sum.reindex[of "(+) a" "{..< b}" f] by auto

lemma sum_Un_introL:
assumes "A1 = B1 Un C1" and "x = x1 + x2"
"finite A1" and
"B1 Int C1 = {}" and
"sum f1 B1 = x1" and "sum f1 C1 = x2"
shows "sum f1 A1 = x"
by (metis assms finite_Un sum.union_disjoint)

lemma sum_Un_intro:
assumes "A1 = B1 Un C1" and "A2 = B2 Un C2" and
"finite A1" and "finite A2" and
"B1 Int C1 = {}" and "B2 Int C2 = {}" and
"sum f1 B1 = sum f2 B2" and "sum f1 C1 = sum f2 C2"
shows "sum f1 A1 = sum f2 A2"
by (metis assms finite_Un sum.union_disjoint)

lemma sum_UN_introL:
assumes A1: "A1 = (UN n : N. B1 n)" and a2: "a2 = sum b2 N" and
fin: "finite N" "⋀ n. n ∈ N ⟹ finite (B1 n)" and
int: "⋀ m n. {m, n} ⊆ N ∧ m ≠ n ⟹ B1 m ∩ B1 n = {}" and
ss: "⋀ n. n ∈ N ⟹ sum f1 (B1 n) = b2 n"
shows "sum f1 A1 = a2" (is "?L = a2")
proof-
have "?L = sum (%n. sum f1 (B1 n)) N"
unfolding A1 using sum.UNION_disjoint[of N B1 f1] fin int by simp
also have "... = sum b2 N" using ss fin by auto
also have "... = a2" using a2 by simp
finally show ?thesis .
qed

lemma sum_UN_intro:
assumes A1: "A1 = (UN n : N. B1 n)" and A2: "A2 = (UN n : N. B2 n)" and
fin: "finite N" "⋀ n. n ∈ N ⟹ finite (B1 n) ∧ finite (B2 n)" and
int: "⋀ m n. {m, n} ⊆ N ∧ m ≠ n ⟹ B1 m ∩ B1 n = {}" "⋀ m n. {m, n} ⊆ N ⟹ B2 m ∩ B2 n = {}" and
ss: "⋀ n. n ∈ N ⟹ sum f1 (B1 n) = sum f2 (B2 n)"
shows "sum f1 A1 = sum f2 A2" (is "?L = ?R")
proof-
have "?L = sum (%n. sum f1 (B1 n)) N"
unfolding A1 using sum.UNION_disjoint[of N B1 f1] fin int by simp
also have "... = sum (%n. sum f2 (B2 n)) N" using ss fin sum.mono_neutral_left by auto
also have "... = ?R"
unfolding A2 using sum.UNION_disjoint[of N B2 f2] fin int by simp
finally show ?thesis .
qed

lemma sum_Minus_intro:
fixes f1 :: "'a1 ⇒ real" and f2 :: "'a2 ⇒ real"
assumes "B1 = A1 - {a1}" and "B2 = A2 - {a2}" and
"a1 : A1" and "a2 : A2" and "finite A1" and "finite A2"
"sum f1 A1 = sum f2 A2" and "f1 a1 = f2 a2"
shows "sum f1 B1 = sum f2 B2"
proof-
have 1: "A1 = B1 Un {a1}" and 2: "A2 = B2 Un {a2}"
using assms by blast+
from assms have "a1 ∉ B1" by simp
with 1 ‹finite A1› have "sum f1 A1 = sum f1 B1 + f1 a1"
by simp
hence 3: "sum f1 B1 = sum f1 A1 - f1 a1" by simp
from assms have "a2 ∉ B2" by simp
with 2 ‹finite A2 ›have "sum f2 A2 = sum f2 B2 + f2 a2"
by simp
hence "sum f2 B2 = sum f2 A2 - f2 a2" by simp
thus ?thesis using 3 assms by simp
qed

lemma sum_singl_intro:
assumes "b = f a"
and "finite A" and "a ∈ A"
and "⋀ a'. ⟦a' ∈ A; a' ≠ a⟧ ⟹ f a' = 0"
shows "sum f A = b"
proof-
define B where "B = A - {a}"
have "A = B Un {a}" unfolding B_def using assms by blast
moreover have "B Int {a} = {}" unfolding B_def by blast
ultimately have "sum f A = sum f B + sum f {a}"
using assms sum.union_disjoint by blast
moreover have "∀ b ∈ B. f b = 0" using assms unfolding B_def by auto
ultimately show ?thesis using assms by auto
qed

lemma sum_all0_intro:
assumes "b = 0"
and "⋀ a. a ∈ A ⟹ f a = 0"
shows "sum f A = b"
using assms by simp

lemma sum_1:
assumes I: "finite I" and ss: "sum f I = 1" and i: "i ∈ I - I1" and I1: "I1 ⊆ I"
and f: "⋀i. i ∈ I ⟹ (0::real) ≤ f i"
shows "f i ≤ 1 - sum f I1"
proof-
have "sum f I = sum f ({i} Un (I - {i}))" using i
by (metis DiffE insert_Diff_single insert_absorb insert_is_Un)
also have "... = sum f {i} + sum f (I - {i})"
apply(rule sum.union_disjoint) using I by auto
finally have "1 = f i + sum f (I - {i})" unfolding ss[THEN sym] by simp
moreover have "sum f (I - {i}) ≥ sum f I1"
apply(rule sum_mono2) using assms by auto
ultimately have "1 ≥ f i + sum f I1" by auto
thus ?thesis by auto
qed

subsection ‹Syntax›

datatype ('test, 'atom, 'choice) cmd =
Done
| Atm "'atom"
| Seq "('test, 'atom, 'choice) cmd" "('test, 'atom, 'choice) cmd" ("_ ;; _"  [60, 61] 60)
| While "'test" "('test, 'atom, 'choice) cmd"
| Ch 'choice "('test, 'atom, 'choice) cmd" "('test, 'atom, 'choice) cmd"
| Par "('test, 'atom, 'choice) cmd list"
| ParT "('test, 'atom, 'choice) cmd list"

(* Commands containing no while loops: *)
fun noWhile where
"noWhile Done ⟷ True"
| "noWhile (Atm atm) ⟷ True"
| "noWhile (c1 ;; c2) ⟷ noWhile c1 ∧ noWhile c2"
| "noWhile (While tst c) ⟷ False"
| "noWhile (Ch ch c1 c2) ⟷ noWhile c1 ∧ noWhile c2"
| "noWhile (Par cl) ⟷ (∀ c ∈ set cl. noWhile c)"
| "noWhile (ParT cl) ⟷ (∀ c ∈ set cl. noWhile c)"

(* ``Finished" commands: *)
fun finished where
"finished Done ⟷ True"
| "finished (Atm atm) ⟷ False"
| "finished (c1 ;; c2) ⟷ False"
| "finished (While tst c) ⟷ False"
| "finished (Ch ch c1 c2) ⟷ False"
| "finished (Par cl) ⟷ (∀ c ∈ set cl. finished c)"
| "finished (ParT cl) ⟷ (∀ c ∈ set cl. finished c)"

definition noWhileL where
"noWhileL cl ≡ ∀ c ∈ set cl. noWhile c"

lemma fin_Par_noWhileL[simp]:
"noWhile (Par cl) ⟷ noWhileL cl"
unfolding noWhileL_def by simp

lemma fin_ParT_noWhileL[simp]:
"noWhile (ParT cl) ⟷ noWhileL cl"
unfolding noWhileL_def by simp

declare noWhile.simps(6) [simp del]
declare noWhile.simps(7) [simp del]

lemma noWhileL_intro[intro]:
assumes "⋀ c. c ∈ set cl ⟹ noWhile c"
shows "noWhileL cl"
using assms unfolding noWhileL_def by auto

lemma noWhileL_fin[simp]:
assumes "noWhileL cl" and "c ∈ set cl"
shows "noWhile c"
using assms unfolding noWhileL_def by simp

lemma noWhileL_update[simp]:
assumes cl: "noWhileL cl" and c': "noWhile c'"
shows "noWhileL (cl[n := c'])"
proof(cases "n < length cl")
case True
show ?thesis
unfolding noWhileL_def proof safe
fix c assume "c ∈ set (cl[n := c'])"
hence "c ∈ insert c' (set cl)" using set_update_subset_insert by fastforce
thus "noWhile c" using assms by (cases "c = c'") auto
qed
qed (insert cl, auto)

definition finishedL where
"finishedL cl ≡ ∀ c ∈ set cl. finished c"

lemma finished_Par_finishedL[simp]:
"finished (Par cl) ⟷ finishedL cl"
unfolding finishedL_def by simp

lemma finished_ParT_finishedL[simp]:
"finished (ParT cl) ⟷ finishedL cl"
unfolding finishedL_def by simp

declare finished.simps(6) [simp del]
declare finished.simps(7) [simp del]

lemma finishedL_intro[intro]:
assumes "⋀ c. c ∈ set cl ⟹ finished c"
shows "finishedL cl"
using assms unfolding finishedL_def by auto

lemma finishedL_finished[simp]:
assumes "finishedL cl" and "c ∈ set cl"
shows "finished c"
using assms unfolding finishedL_def by simp

lemma finishedL_update[simp]:
assumes cl: "finishedL cl" and c': "finished c'"
shows "finishedL (cl[n := c'])"
proof(cases "n < length cl")
case True
show ?thesis
unfolding finishedL_def proof safe
fix c assume "c ∈ set (cl[n := c'])"
hence "c ∈ insert c' (set cl)" using set_update_subset_insert by fastforce
thus "finished c" using assms by (cases "c = c'") auto
qed
qed (insert cl, auto)

lemma finished_fin[simp]:
"finished c ⟹ noWhile c"
by(induct c) auto

lemma finishedL_noWhileL[simp]:
"finishedL cl ⟹ noWhileL cl"
unfolding finishedL_def noWhileL_def by auto

locale PL =
fixes
aval :: "'atom ⇒ 'state ⇒ 'state" and
tval :: "'test ⇒ 'state ⇒ bool" and
cval :: "'choice ⇒ 'state ⇒ real"
assumes
properCh: "⋀ ch s. 0 ≤ cval ch s ∧ cval ch s ≤ 1"
begin

lemma [simp]: "(n::nat) < N ⟹ 0 ≤ 1 / N" by auto

lemma [simp]: "(n::nat) < N ⟹ 1 / N ≤ 1" by auto

lemma [simp]: "(n::nat) < N ⟹ 0 ≤ 1 - 1 / N" by (simp add: divide_simps)

lemma sum_equal: "0 < (N::nat) ⟹ sum (λ n. 1/N) {..< N} = 1"
unfolding sum_constant by auto

fun proper where
"proper Done ⟷ True"
| "proper (Atm x) ⟷ True"
| "proper (Seq c1 c2) ⟷ proper c1 ∧ proper c2"
| "proper (While tst c) ⟷ proper c"
| "proper (Ch ch c1 c2) ⟷ proper c1 ∧ proper c2"
| "proper (Par cl) ⟷ cl ≠ [] ∧ (∀ c ∈ set cl. proper c)"
| "proper (ParT cl) ⟷ cl ≠ [] ∧ (∀ c ∈ set cl. proper c)"

definition properL where
"properL cl ≡ cl ≠ [] ∧ (∀ c ∈ set cl. proper c)"

lemma proper_Par_properL[simp]:
"proper (Par cl) ⟷ properL cl"
unfolding properL_def by simp

lemma proper_ParT_properL[simp]:
"proper (ParT cl) ⟷ properL cl"
unfolding properL_def by simp

declare proper.simps(6) [simp del]
declare proper.simps(7) [simp del]

lemma properL_intro[intro]:
"⟦cl ≠ []; ⋀ c. c ∈ set cl ⟹ proper c⟧ ⟹ properL cl"
unfolding properL_def by auto

lemma properL_notEmp[simp]: "properL cl ⟹ cl ≠ []"
unfolding properL_def by simp

lemma properL_proper[simp]:
"⟦properL cl; c ∈ set cl⟧ ⟹ proper c"
unfolding properL_def by simp

lemma properL_update[simp]:
assumes cl: "properL cl" and c': "proper c'"
shows "properL (cl[n := c'])"
proof(cases "n < length cl")
case True
show ?thesis
unfolding properL_def proof safe
fix c assume "c ∈ set (cl[n := c'])"
hence "c ∈ insert c' (set cl)" using set_update_subset_insert by fastforce
thus "proper c" using assms by (cases "c = c'") auto
qed (insert cl, auto)
qed (insert cl, auto)

lemma proper_induct[consumes 1, case_names Done Atm Seq While Ch Par ParT]:
assumes *: "proper c"
and Done: "phi Done"
and Atm: "⋀ atm. phi (Atm atm)"
and Seq: "⋀ c1 c2. ⟦phi c1; phi c2⟧ ⟹ phi (c1 ;; c2)"
and While: "⋀ tst c. phi c ⟹ phi (While tst c)"
and Ch: "⋀ ch c1 c2. ⟦phi c1; phi c2⟧ ⟹ phi (Ch ch c1 c2)"
and Par: "⋀ cl. ⟦properL cl; ⋀ c. c ∈ set cl ⟹ phi c⟧ ⟹ phi (Par cl)"
and ParT: "⋀ cl. ⟦properL cl; ⋀ c. c ∈ set cl ⟹ phi c⟧ ⟹ phi (ParT cl)"
shows "phi c"
using * apply(induct c)
using assms unfolding properL_def by auto

subsubsection ‹Operational Small-Step Semantics›

definition "theFT cl ≡ {n. n < length cl ∧ finished (cl!n)}"

definition "theNFT cl ≡ {n. n < length cl ∧ ¬ finished (cl!n)}"

lemma finite_theFT[simp]: "finite (theFT cl)"
unfolding theFT_def by simp

lemma theFT_length[simp]: "n ∈ theFT cl ⟹ n < length cl"
unfolding theFT_def by simp

lemma theFT_finished[simp]: "n ∈ theFT cl ⟹ finished (cl!n)"
unfolding theFT_def by simp

lemma finite_theNFT[simp]: "finite (theNFT cl)"
unfolding theNFT_def by simp

lemma theNFT_length[simp]: "n ∈ theNFT cl ⟹ n < length cl"
unfolding theNFT_def by simp

lemma theNFT_notFinished[simp]: "n ∈ theNFT cl ⟹ ¬ finished (cl!n)"
unfolding theNFT_def by simp

lemma theFT_Int_theNFT[simp]:
"theFT cl Int theNFT cl = {}" and "theNFT cl Int theFT cl = {}"
unfolding theFT_def theNFT_def by auto

lemma theFT_Un_theNFT[simp]:
"theFT cl Un theNFT cl = {..< length cl}" and
"theNFT cl Un theFT cl = {..< length cl}"
unfolding theFT_def theNFT_def by auto

lemma in_theFT_theNFT[simp]:
assumes "n1 ∈ theFT cl" and "n2 ∈ theNFT cl"
shows "n1 ≠ n2" and "n2 ≠ n1"
using assms theFT_Int_theNFT by blast+

(* The cumulated weight of the finished threads: *)
definition "WtFT cl ≡ sum (λ (n::nat). 1/(length cl)) (theFT cl)"

(* The cumulated weight of the non-finished threads: *)
definition "WtNFT cl ≡ sum (λ (n::nat). 1/(length cl)) (theNFT cl)"

lemma WtFT_WtNFT[simp]:
assumes "0 < length cl"
shows "WtFT cl + WtNFT cl = 1" (is "?A = 1")
proof-
let ?w = "λ n. 1 / length cl" let ?L = "theFT cl" let ?Lnot = "theNFT cl"
have 1: "{..< length cl} = ?L Un ?Lnot" by auto
have "?A = sum ?w ?L + sum ?w ?Lnot" unfolding WtFT_def WtNFT_def by simp
also have "... = sum ?w {..< length cl}" unfolding 1
apply(rule sum.union_disjoint[THEN sym]) by auto
also have "... = 1" unfolding sum_equal[OF assms] by auto
finally show ?thesis .
qed

lemma WtNFT_1_WtFT: "0 < length cl ⟹ WtNFT cl = 1 - WtFT cl"

lemma WtNFT_WtFT_1[simp]:
assumes "0 < length cl" and "WtFT cl ≠ 1"
shows "WtNFT cl / (1 - WtFT cl) = 1" (is "?A / ?B = 1")
proof-
have A: "?A = ?B" using assms WtNFT_1_WtFT by auto
show ?thesis unfolding A using assms by auto
qed

lemma WtFT_ge_0[simp]: "WtFT cl ≥ 0"
unfolding WtFT_def by (rule sum_nonneg) simp

lemma WtFT_le_1[simp]: "WtFT cl ≤ 1" (is "?L ≤ 1")
proof-
let ?N = "length cl"
have "?L ≤ sum (λ n::nat. 1/?N) {..< ?N}"
unfolding WtFT_def apply(rule sum_mono2) by auto
also have "... ≤ 1"
by (metis div_by_0 le_cases neq0_conv not_one_le_zero of_nat_0 sum.neutral sum_equal)
finally show ?thesis .
qed

lemma le_1_WtFT[simp]: "0 ≤ 1 - WtFT cl" (is "0 ≤ ?R")
proof-
have a: "-1 ≤ - WtFT cl" by simp
have "(0 :: real) = 1 + (-1)" by simp
also have "1 + (-1) ≤ 1 + (- WtFT cl)" using a by arith
also have "... = ?R" by simp
finally show ?thesis .
qed

lemma WtFT_lt_1[simp]: "WtFT cl ≠ 1 ⟹ WtFT cl < 1"
using WtFT_le_1 by (auto simp add: le_less)

lemma lt_1_WtFT[simp]: "WtFT cl ≠ 1 ⟹ 0 < 1 - WtFT cl"
using le_1_WtFT by (metis le_1_WtFT eq_iff_diff_eq_0 less_eq_real_def)

lemma notFinished_WtFT[simp]:
assumes "n < length cl" and "¬ finished (cl ! n)"
shows "1 / length cl ≤ 1 - WtFT cl"
proof-
have "0 < length cl" using assms by auto
thus ?thesis unfolding WtFT_def apply(intro sum_1[of "{..< length cl}"])
using assms by auto
qed

(* The branching of a command: *)
fun brn :: "('test, 'atom, 'choice) cmd ⇒ nat" where
"brn Done = 1"
| "brn (Atm atm) = 1"
| "brn (c1 ;; c2) = brn c1"
| "brn (While tst c) = 1"
| "brn (Ch ch c1 c2) = 2"
| "brn (Par cl) = lsum brn cl"
| "brn (ParT cl) = lsum brn cl"

lemma brn_gt_0: "proper c ⟹ 0 < brn c"
by (induct rule: proper_induct) auto

lemma brn_gt_0_L: "⟦properL cl; c ∈ set cl⟧ ⟹ 0 < brn c"
by (metis brn_gt_0 properL_def)

(* The locate-thread and locate-index operators.
Given a thread list cl with n = length cl and i < (∑ l < length cl . brn cl),
(locateT cl i, locateI cl i) are (k, j) from the paper's Figure 1.
*)
definition "locateT ≡ locate1 brn"   definition "locateI ≡ locate2 brn"

definition "brnL cl n ≡ lsum brn (take n cl)"

lemma brnL_lsum: "brnL cl (length cl) = lsum brn cl"
unfolding brnL_def by simp

lemma brnL_unique:
assumes "properL cl" and "n1 < length cl ∧ j1 < brn (cl ! n1)"
and "n2 < length cl ∧ j2 < brn (cl ! n2)" and "brnL cl n1 + j1 = brnL cl n2 + j2"
shows "n1 = n2 ∧ j1 = j2"
apply (rule less_lsum_unique) using assms brn_gt_0 unfolding brnL_def properL_def by auto

lemma brn_Par_simp[simp]: "brn (Par cl) = brnL cl (length cl)"
unfolding brnL_lsum by simp

lemma brn_ParT_simp[simp]: "brn (ParT cl) = brnL cl (length cl)"
unfolding brnL_lsum by simp

declare brn.simps(6)[simp del]   declare brn.simps(7)[simp del]

lemma brnL_0[simp]: "brnL cl 0 = 0"
unfolding brnL_def by auto

lemma brnL_Suc[simp]: "n < length cl ⟹ brnL cl (Suc n) = brnL cl n + brn (cl ! n)"
unfolding brnL_def using take_Suc_conv_app_nth[of n cl] by simp

lemma brnL_mono[simp]: "n1 ≤ n2 ⟹ brnL cl n1 ≤ brnL cl n2"
using le_take[of n1 n2 cl] unfolding brnL_def by simp

lemma brnL_mono2[simp]:
assumes p: "properL cl" and n: "n1 < n2" and l: "n2 ≤ length cl"
shows "brnL cl n1 < brnL cl n2" (is "?L < ?R")
proof-
have 1: "⋀c. c ∈ set (take n2 cl) ⟹ 0 < brn c"
using p by (metis brn_gt_0 in_set_takeD properL_proper)
have "take n1 cl < take n2 cl" using n l lt_take by auto
hence "lsum brn (take n1 cl) < lsum brn (take n2 cl)"
using lsum_mono2[of "take n2 cl" "%c. brn c" "take n1 cl"] 1 by simp
thus ?thesis unfolding brnL_def .
qed

lemma brn_index[simp]:
assumes n: "n < length cl" and i: "i < brn (cl ! n)"
shows "brnL cl n + i < brnL cl (length cl)" (is "?L < ?R")
proof-
have "?L < brnL cl (Suc n)" using assms by simp
also have "... ≤ ?R"
using n brnL_mono[of "Suc n" "length cl" cl] by simp
finally show ?thesis .
qed

lemma brnL_gt_0[simp]: "⟦properL cl; 0 < n⟧ ⟹ 0 < brnL cl n"
by (metis properL_def brnL_mono brnL_mono2 le_0_eq length_greater_0_conv nat_le_linear neq0_conv)

lemma locateTI:
assumes "properL cl" and "ii < brn (Par cl)"
shows
"locateT cl ii < length cl ∧
locateI cl ii < brn (cl ! (locateT cl ii)) ∧
ii = brnL cl (locateT cl ii) + locateI cl ii"
using assms locate[of cl brn ii] brn_gt_0
unfolding locateT_def locateI_def brnL_def
unfolding brnL_lsum[THEN sym] by auto

lemma locateTI_unique:
assumes "properL cl" and "n < length cl"
and "i < brn (cl ! n)" and "ii = brnL cl n + i"
shows "n = locateT cl ii ∧ i = locateI cl ii"
using assms locate_unique[of cl brn] brn_gt_0
unfolding locateT_def locateI_def brnL_def
unfolding brnL_lsum[THEN sym] by auto

(*  pickFT picks a finished thread (if there is any).
It will be used to perform a dummy transition in case the cumulated weight of the
finished threads is 0; specifically, one will assign probability 1 to that picked fresh.
(Obviously, the particular choice does not matter.)   *)
definition pickFT_pred where "pickFT_pred cl n ≡ n < length cl ∧ finished (cl!n)"
definition pickFT where "pickFT cl ≡ SOME n. pickFT_pred cl n"

lemma pickFT_pred:
assumes "WtFT cl = 1"  shows "∃ n. pickFT_pred cl n"
proof(rule ccontr, unfold not_ex)
assume "∀n. ¬ pickFT_pred cl n"
hence "⋀ n. n < length cl ⟹ ¬ finished (cl!n)"
unfolding pickFT_pred_def by auto
hence "theFT cl = {}" unfolding theFT_def by auto
hence "WtFT cl = 0" unfolding WtFT_def by simp
thus False using assms by simp
qed

lemma pickFT_pred_pickFT: "WtFT cl = 1 ⟹ pickFT_pred cl (pickFT cl)"
unfolding pickFT_def by(auto intro: someI_ex pickFT_pred)

lemma pickFT_length[simp]: "WtFT cl = 1 ⟹ pickFT cl < length cl"
using pickFT_pred_pickFT unfolding pickFT_pred_def by auto

lemma pickFT_finished[simp]: "WtFT cl = 1 ⟹ finished (cl ! (pickFT cl))"
using pickFT_pred_pickFT unfolding pickFT_pred_def by auto

lemma pickFT_theFT[simp]: "WtFT cl = 1 ⟹ pickFT cl ∈ theFT cl"
unfolding theFT_def by auto

(* The weight, continuation and effect defined as a single operator: *)
fun wt_cont_eff where
"wt_cont_eff Done s i = (1, Done, s)"
|
"wt_cont_eff (Atm atm) s i = (1, Done, aval atm s)"
|
"wt_cont_eff (c1 ;; c2) s i =
(case wt_cont_eff c1 s i of
(x, c1', s') ⇒
if finished c1' then (x, c2, s') else (x, c1' ;; c2, s'))"
|
"wt_cont_eff (While tst c) s i =
(if tval tst s
then (1, c ;; (While tst c), s)
else (1, Done, s))"
|
"wt_cont_eff (Ch ch c1 c2) s i =
(if i = 0 then cval ch s else 1 - cval ch s,
if i = 0 then c1 else c2,
s)"
|
"wt_cont_eff (Par cl) s ii =
(if cl ! (locateT cl ii) ∈ set cl then
(case wt_cont_eff
(cl ! (locateT cl ii))
s
(locateI cl ii) of
(w, c', s') ⇒
((1 / (length cl)) * w,
Par (cl [(locateT cl ii) := c']),
s'))
else undefined)"
|
"wt_cont_eff (ParT cl) s ii =
(if cl ! (locateT cl ii) ∈ set cl
then
(case wt_cont_eff
(cl ! (locateT cl ii))
s
(locateI cl ii) of
(w, c', s') ⇒
(if WtFT cl = 1
then (if locateT cl ii = pickFT cl ∧ locateI cl ii = 0
then 1
else 0)
else if finished (cl ! (locateT cl ii))
then 0
else (1 / (length cl))
/ (1 - WtFT cl)
* w,
ParT (cl [(locateT cl ii) := c']),
s'))
else undefined)"

(* weight, cont (transition) and effect: *)
definition wt where "wt c s i = fst (wt_cont_eff c s i)"
definition cont where "cont c s i = fst (snd (wt_cont_eff c s i))"
definition eff where "eff c s i = snd (snd (wt_cont_eff c s i))"

(* Their individual equations (corresponding to the paper's Figure 1):  *)
lemma wt_Done[simp]: "wt Done s i = 1"
unfolding wt_def by simp

lemma wt_Atm[simp]: "wt (Atm atm) s i = 1"
unfolding wt_def by simp

lemma wt_Seq[simp]:
"wt (c1 ;; c2) s = wt c1 s"
proof-
{fix i have "wt (c1 ;; c2) s i = wt c1 s i"
proof(cases "wt_cont_eff c1 s i")
case (fields _ c1' _)
thus ?thesis unfolding wt_def by(cases c1', auto)
qed
}
thus ?thesis by auto
qed

lemma wt_While[simp]: "wt (While tst c) s i = 1"
unfolding wt_def by simp

lemma wt_Ch_L[simp]: "wt (Ch ch c1 c2) s 0 = cval ch s"
unfolding wt_def by simp

lemma wt_Ch_R[simp]: "wt (Ch ch c1 c2) s (Suc n) = 1 - cval ch s"
unfolding wt_def by simp

(*  *)
lemma cont_Done[simp]: "cont Done s i = Done"
unfolding cont_def by simp

lemma cont_Atm[simp]: "cont (Atm atm) s i = Done"
unfolding cont_def by simp

lemma cont_Seq_finished[simp]: "finished (cont c1 s i) ⟹ cont (c1 ;; c2) s i = c2"
unfolding cont_def by(cases "wt_cont_eff c1 s i") auto

lemma cont_Seq_notFinished[simp]:
assumes "¬ finished (cont c1 s i)"
shows "cont (c1 ;; c2) s i = (cont c1 s i) ;; c2"
proof(cases "wt_cont_eff c1 s i")
case (fields _ c1' _)
thus ?thesis using assms unfolding cont_def by(cases c1')  auto
qed

lemma cont_Seq_not_eq_finished[simp]: "¬ finished c2 ⟹ ¬ finished (cont (Seq c1 c2) s i)"
by (cases "finished (cont c1 s i)") auto

lemma cont_While_False[simp]: "tval tst s = False ⟹ cont (While tst c) s i = Done"
unfolding cont_def by simp

lemma cont_While_True[simp]: "tval tst s = True ⟹ cont (While tst c) s i = c ;; (While tst c)"
unfolding cont_def by simp

lemma cont_Ch_L[simp]: "cont (Ch ch c1 c2) s 0 = c1"
unfolding cont_def by simp

lemma cont_Ch_R[simp]: "cont (Ch ch c1 c2) s (Suc n) = c2"
unfolding cont_def by simp

(*  *)

lemma eff_Done[simp]: "eff Done s i = s"
unfolding eff_def by simp

lemma eff_Atm[simp]: "eff (Atm atm) s i = aval atm s"
unfolding eff_def by simp

lemma eff_Seq[simp]: "eff (c1 ;; c2) s = eff c1 s"
proof-
{fix i have "eff (c1 ;; c2) s i = eff c1 s i"
proof(cases "wt_cont_eff c1 s i")
case (fields _ c1' _)
thus ?thesis
unfolding eff_def by(cases c1') auto
qed
}
thus ?thesis by auto
qed

lemma eff_While[simp]: "eff (While tst c) s i = s"
unfolding eff_def by simp

lemma eff_Ch[simp]: "eff (Ch ch c1 c2) s i = s"
unfolding eff_def by simp

(* wt-cont-eff simps for parallel composition *)
lemma brnL_nchotomy:
assumes "properL cl" and "ii < brnL cl (length cl)"
shows "∃ n i. n < length cl ∧ i < brn (cl ! n) ∧ ii = brnL cl n + i"
unfolding brnL_def apply(rule less_lsum_nchotomy) using assms brn_gt_0
unfolding brnL_lsum[THEN sym] by auto

corollary brnL_cases[consumes 2, case_names Local, elim]:
assumes "properL cl" and "ii < brnL cl (length cl)" and
"⋀ n i. ⟦n < length cl; i < brn (cl ! n); ii = brnL cl n + i⟧ ⟹ phi"
shows phi
using assms brnL_nchotomy by blast

lemma wt_cont_eff_Par[simp]:
assumes p: "properL cl"
and n: "n < length cl" and i: "i < brn (cl ! n)"
shows
"wt (Par cl) s (brnL cl n + i) =
1 / (length cl) * wt (cl ! n) s i"
(is "?wL = ?wR")
(*  *)
"cont (Par cl) s (brnL cl n + i) =
Par (cl [n := cont (cl ! n) s i])"
(is "?mL = ?mR")
(*  *)
"eff (Par cl) s (brnL cl n + i) =
eff (cl ! n) s i"
(is "?eL = ?eR")
proof-
define ii where "ii = brnL cl n + i"
define n1 where "n1 = locateT cl ii"
define i1 where "i1 = locateI cl ii"
have n_i: "n = n1" "i = i1" using p unfolding n1_def i1_def
using ii_def locateTI_unique n i by auto
have lsum1: "ii < brnL cl (length cl)" unfolding ii_def using n i by simp
hence "n1 < length cl"
unfolding n1_def using i p locateTI[of cl ii] by simp
hence set: "cl ! n1 ∈ set cl" by simp
(*  *)
have "?wL = 1 / (length cl)* wt (cl ! n1) s i1"
unfolding ii_def[THEN sym]
apply (cases "wt_cont_eff (cl ! n1) s i1")
using set unfolding n1_def i1_def unfolding wt_def by simp
also have "... = ?wR" unfolding n_i by simp
finally show "?wL = ?wR" .
(*  *)
have "?mL = Par (cl [n1 := cont (cl ! n1) s i1])"
unfolding ii_def[THEN sym]
apply (cases "wt_cont_eff (cl ! n1) s i1")
using set unfolding n1_def i1_def unfolding cont_def by simp
also have "... = ?mR" unfolding n_i by simp
finally show "?mL = ?mR" .
(*  *)
have "?eL = eff (cl ! n1) s i1"
unfolding ii_def[THEN sym]
apply (cases "wt_cont_eff (cl ! n1) s i1")
using set unfolding n1_def i1_def unfolding eff_def by simp
also have "eff (cl ! n1) s i1 = ?eR" unfolding n_i by simp
finally show "?eL = ?eR" .
qed

lemma cont_eff_ParT[simp]:
assumes p: "properL cl"
and n: "n < length cl" and i: "i < brn (cl ! n)"
shows
"cont (ParT cl) s (brnL cl n + i) =
ParT (cl [n := cont (cl ! n) s i])"
(is "?mL = ?mR")
(*  *)
"eff (ParT cl) s (brnL cl n + i) =
eff (cl ! n) s i"
(is "?eL = ?eR")
proof-
define ii where "ii = brnL cl n + i"
define n1 where "n1 = locateT cl ii"
define i1 where "i1 = locateI cl ii"
have n_i: "n = n1" "i = i1" using p unfolding n1_def i1_def
using ii_def locateTI_unique n i by auto
have lsum1: "ii < brnL cl (length cl)" unfolding ii_def using n i by simp
hence "n1 < length cl"
unfolding n1_def using i p locateTI[of cl ii] by simp
hence set: "cl ! n1 ∈ set cl" by simp
(*  *)
have "?mL = ParT (cl [n1 := cont (cl ! n1) s i1])"
unfolding ii_def[THEN sym]
apply (cases "wt_cont_eff (cl ! n1) s i1")
using set unfolding n1_def i1_def unfolding cont_def by simp
also have "... = ?mR" unfolding n_i by simp
finally show "?mL = ?mR" .
(*  *)
have "?eL = eff (cl ! n1) s i1"
unfolding ii_def[THEN sym]
apply (cases "wt_cont_eff (cl ! n1) s i1")
using set unfolding n1_def i1_def unfolding eff_def by simp
also have "eff (cl ! n1) s i1 = ?eR" unfolding n_i by simp
finally show "?eL = ?eR" .
qed

lemma wt_ParT_WtFT_pickFT_0[simp]:
assumes p: "properL cl" and WtFT: "WtFT cl = 1"
shows "wt (ParT cl) s (brnL cl (pickFT cl)) = 1"
(is "?wL = 1")
proof-
define ii where "ii = brnL cl (pickFT cl)"
define n1 where "n1 = locateT cl ii"
define i1 where "i1 = locateI cl ii"
have ni: "pickFT cl < length cl" "0 < brn (cl! (pickFT cl))"
using WtFT p brn_gt_0 by auto
hence n_i: "pickFT cl = n1" "0 = i1" using p unfolding n1_def i1_def
using ii_def locateTI_unique[of cl "pickFT cl" 0 ii] by auto
have lsum1: "ii < brnL cl (length cl)" unfolding ii_def using ni
hence "n1 < length cl"
unfolding n1_def using ni p locateTI[of cl ii] by simp
hence set: "cl ! n1 ∈ set cl" by simp
(*  *)
have n1i1: "n1 = pickFT cl ∧ i1 = 0" using WtFT ni unfolding n_i by auto
show "?wL = 1"
unfolding ii_def[THEN sym]
apply (cases "wt_cont_eff (cl ! n1) s i1")
using WtFT n1i1 set unfolding n1_def i1_def unfolding wt_def by simp
qed

lemma wt_ParT_WtFT_notPickFT_0[simp]:
assumes p: "properL cl" and n: "n < length cl" and i: "i < brn (cl ! n)"
and WtFT: "WtFT cl = 1" and ni: "n = pickFT cl ⟶ i ≠ 0"
shows "wt (ParT cl) s (brnL cl n + i) = 0" (is "?wL = 0")
proof-
define ii where "ii = brnL cl n + i"
define n1 where "n1 = locateT cl ii"
define i1 where "i1 = locateI cl ii"
have n_i: "n = n1" "i = i1" using p unfolding n1_def i1_def
using ii_def locateTI_unique n i by auto
have lsum1: "ii < brnL cl (length cl)" unfolding ii_def using n i by simp
hence "n1 < length cl"
unfolding n1_def using i p locateTI[of cl ii] by simp
hence set: "cl ! n1 ∈ set cl" by simp
(*  *)
have n1i1: "n1 ≠ pickFT cl ∨ i1 ≠ 0" using WtFT ni unfolding n_i by auto
show "?wL = 0"
unfolding ii_def[THEN sym]
apply (cases "wt_cont_eff (cl ! n1) s i1")
using WtFT n1i1 set unfolding n1_def i1_def unfolding wt_def by force
qed

lemma wt_ParT_notWtFT_finished[simp]:
assumes p: "properL cl" and n: "n < length cl" and i: "i < brn (cl ! n)"
and WtFT: "WtFT cl ≠ 1" and f: "finished (cl ! n)"
shows "wt (ParT cl) s (brnL cl n + i) = 0" (is "?wL = 0")
proof-
define ii where "ii = brnL cl n + i"
define n1 where "n1 = locateT cl ii"
define i1 where "i1 = locateI cl ii"
have n_i: "n = n1" "i = i1" using p unfolding n1_def i1_def
using ii_def locateTI_unique n i by auto
have lsum1: "ii < brnL cl (length cl)" unfolding ii_def using n i by simp
hence "n1 < length cl"
unfolding n1_def using i p locateTI[of cl ii] by simp
hence set: "cl ! n1 ∈ set cl" by simp
(*  *)
have f: "finished (cl ! n1)" using f unfolding n_i by auto
show "?wL = 0"
unfolding ii_def[THEN sym]
apply (cases "wt_cont_eff (cl ! n1) s i1")
using WtFT f set unfolding n1_def i1_def unfolding wt_def by simp
qed

lemma wt_cont_eff_ParT_notWtFT_notFinished[simp]:
assumes p: "properL cl" and n: "n < length cl" and i: "i < brn (cl ! n)"
and WtFT: "WtFT cl ≠ 1" and nf: "¬ finished (cl ! n)"
shows "wt (ParT cl) s (brnL cl n + i) =
(1 / (length cl)) / (1 - WtFT cl) * wt (cl ! n) s i" (is "?wL = ?wR")
proof-
define ii where "ii = brnL cl n + i"
define n1 where "n1 = locateT cl ii"
define i1 where "i1 = locateI cl ii"
have n_i: "n = n1" "i = i1" using p unfolding n1_def i1_def
using ii_def locateTI_unique n i by auto
have lsum1: "ii < brnL cl (length cl)" unfolding ii_def using n i by simp
hence "n1 < length cl" unfolding n1_def using i p locateTI[of cl ii] by simp
hence set: "cl ! n1 ∈ set cl" by simp
(*  *)
have nf: "¬ finished (cl ! n1)" using nf unfolding n_i by auto
have "?wL = (1 / (length cl)) / (1 - WtFT cl) * wt (cl ! n1) s i1"
unfolding ii_def[THEN sym]
apply (cases "wt_cont_eff (cl ! n1) s i1")
using WtFT nf set unfolding n1_def i1_def unfolding wt_def by simp
also have "... = ?wR" unfolding n_i by simp
finally show "?wL = ?wR" .
qed

(*  *)
lemma wt_ge_0[simp]:
assumes "proper c" and "i < brn c"
shows "0 ≤ wt c s i"
using assms proof (induct c arbitrary: i s rule: proper_induct)
case (Ch ch c1 c2)
thus ?case
using properCh  by (cases i) (auto simp: algebra_simps)
next
case (Par cl ii)
have "properL cl" and "ii < brnL cl (length cl)" using Par by auto
thus ?case
apply (cases rule: brnL_cases)
using Par by simp
next
case (ParT cl ii)
have "properL cl" and "ii < brnL cl (length cl)" using ParT by auto
thus ?case
proof(cases rule: brnL_cases)
case (Local n i)
show ?thesis
proof (cases "WtFT cl = 1")
case True
thus ?thesis using Local ParT by (cases "n = pickFT cl ∧ i = 0") auto
next
case False
thus ?thesis using Local ParT by (cases "finished (cl ! n)") auto
qed
qed
qed auto

lemma wt_le_1[simp]:
assumes "proper c" and "i < brn c"
shows "wt c s i ≤ 1"
using assms proof (induct c arbitrary: i s rule: proper_induct)
case (Ch ch c1 c2)
thus ?case
using properCh by (cases i) auto
next
case (Par cl ii)
hence "properL cl" and "ii < brnL cl (length cl)" by auto
thus ?case
apply (cases rule: brnL_cases) apply simp
using Par apply auto
by (metis add_increasing2 diff_is_0_eq gr0_conv_Suc less_imp_diff_less less_or_eq_imp_le nth_mem of_nat_0_le_iff of_nat_Suc)
next
case (ParT cl ii)
have "properL cl" and "ii < brnL cl (length cl)" using ParT by auto
thus ?case
proof(cases rule: brnL_cases)
case (Local n i)
show ?thesis
proof (cases "WtFT cl = 1")
case True
thus ?thesis using Local ParT by (cases "n = pickFT cl ∧ i = 0", auto)
next
case False note sch = False
thus ?thesis using Local ParT proof (cases "finished (cl ! n)")
case False note cln = False
let ?L1 = "1 / (length cl)" let ?L2 = "wt (cl ! n) s i"
let ?R = "WtFT cl"
have "0 ≤ ?L1" and "0 ≤ ?L2" using ParT Local by auto
moreover have "?L2 ≤ 1" using ParT Local by auto
ultimately have "?L1 * ?L2 ≤ ?L1" by (metis mult_right_le_one_le)
also have "?L1 ≤ 1 - ?R" using ParT Local cln by auto
finally have "?L1 * ?L2 ≤ 1 - ?R" .
thus ?thesis using Local ParT cln sch
by (auto simp: pos_divide_le_eq mult.commute)
qed (insert sch ParT Local, auto)
qed
qed
qed auto

abbreviation fromPlus ("(1{_..<+_})") where
"{a ..<+ b} ≡ {a ..< a + b}"

lemma brnL_UN:
assumes "properL cl"
shows "{..< brnL cl (length cl)} = (⋃ n < length cl. {brnL cl n ..<+ brn (cl!n)})"
(is "?L = (⋃ n < length cl. ?R n)")
proof safe
fix ii assume ii: "ii < brnL cl (length cl)"
from assms ii show "ii ∈ (⋃ n < length cl. ?R n)"
proof(cases rule: brnL_cases)
case (Local n i)
hence "ii ∈ ?R n" by simp
thus ?thesis using Local by force
qed
qed auto

lemma brnL_Int_lt:
assumes n12: "n1 < n2" and n2: "n2 < length cl"
shows
"{brnL cl n1 ..<+ brn (cl!n1)} ∩ {brnL cl n2 ..<+ brn (cl!n2)} = {}"
proof-
have "Suc n1 ≤ n2" using assms by simp
hence "brnL cl (Suc n1) ≤ brnL cl n2" by simp
thus ?thesis using assms by simp
qed

lemma brnL_Int:
assumes "n1 ≠ n2" and "n1 < length cl" and "n2 < length cl"
shows "{brnL cl n1 ..<+ brn (cl!n1)} ∩ {brnL cl n2 ..<+ brn (cl!n2)} = {}"
proof(cases "n1 < n2")
case True thus ?thesis using assms brnL_Int_lt by auto
next
case False
hence "n2 < n1" using assms by simp
thus ?thesis using brnL_Int_lt assms by fastforce
qed

lemma sum_wt_Par_sub[simp]:
assumes cl: "properL cl" and n: "n < length cl" and I: "I ⊆ {..< brn (cl ! n)}"
shows "sum (wt (Par cl) s) ((+) (brnL cl n) ` I) =
1 /(length cl) * sum (wt (cl ! n) s) I" (is "?L = ?wSch * ?R")
proof-
have "?L = sum (%i. ?wSch * wt (cl ! n) s i) I"
apply(rule sum.reindex_cong[of "(+) (brnL cl n)"]) using assms by auto
also have "... = ?wSch * ?R"
unfolding sum_distrib_left by simp
finally show ?thesis .
qed

lemma sum_wt_Par[simp]:
assumes cl: "properL cl" and n: "n < length cl"
shows "sum (wt (Par cl) s) {brnL cl n ..<+ brn (cl!n)} =
1 /(length cl) * sum (wt (cl ! n) s) {..< brn (cl ! n)}" (is "?L = ?W * ?R")
using assms by (simp add: sum_distrib_left)

lemma sum_wt_ParT_sub_WtFT_pickFT_0[simp]:
assumes cl: "properL cl" and nf: "WtFT cl = 1"
and I: "I ⊆ {..< brn (cl ! (pickFT cl))}" "0 ∈ I"
shows "sum (wt (ParT cl) s) ((+) (brnL cl (pickFT cl)) ` I) = 1" (is "?L = 1")
proof-
let ?n = "pickFT cl"
let ?w = "%i. if i = 0 then (1::real) else 0"
have n: "?n < length cl" using nf by simp
have 0: "I = {0} Un (I - {0})" using I by auto
have finI: "finite I" using I by (metis finite_nat_iff_bounded)
have "?L = sum ?w I"
proof (rule sum.reindex_cong [of "plus (brnL cl ?n)"])
fix i assume i: "i ∈ I"
have "i < brn (cl ! ?n)" using i I by auto
note i = this i
show "wt (ParT cl) s (```