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"
by (auto simp add: nth_append)

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]
  by (simp add: take_is_prefix)

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 A2have "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›

(* "The Finished Threads": The sublist of finished threads from a list of threads  *)
definition "theFT cl  {n. n < length cl  finished (cl!n)}"

(* "The NopnFinished Threads": *)
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"
  by (simp add: algebra_simps)

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
  by (metis add.comm_neutral brn_index)
  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