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