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