Introduction

is_atomic p ≡ S p = State p ∧ card (post p) = 1 ∧ card (Pre p) = 1 ∧ State p = (Pre p) ∪ (Field (post p)) ∧ (card (post p) = 1 ∧ card (Pre p) = 1 → fst (THE x. x ∈ post p) = (THE x. x ∈ Pre p))

get_atomic [] :: ‘a Program ⇒ (‘a Program) set

get_atomic p = {〈State={a,b}, Pre={a}, post={(a, b)} 〉

a b . (a,b) ∈ post p ∧ a ∈ Pre p}

evaluate [] :: ‘a CNF ⇒ ‘a set ⇒ ‘a Program

evaluate p s ≡ ⋃ (map (λxs. Concat xs s) p)

interleave [⫴] :: ‘a list ⇒ ‘a list ⇒ ‘a list list

[ ] ⫴ ys = [ys]

(xs) ⫴ [ ] = [xs]

(x#xs) ⫴ (y#ys) = map ((#) x) (xs ⫴ (y#ys)) @ map ((#) y) ((x#xs) ⫴ ys)

cnf_concurrency [∥] :: ‘a CNF ⇒ ‘a CNF ⇒ ‘a CNF

cnf_concurrency xs ys = concat [path_m ⫴ path_n. path_m ← xs, path_n ← ys]

is_rounded [] :: ‘a Program ⇒ bool

is_rounded p ≡ Domain (post p) ⊆ Pre p

is_exact [] :: ‘a Program ⇒ bool

is_exact p ≡ is_rounded p ∧ is_feasible p

feasible_version [] :: ‘a Program ⇒ ‘a Program

feasible_version p ≡ 〈State = S p, Pre = Pre p ∩ Domain (post p), post = post p〉

rounded_version [] :: ‘a Program ⇒ ‘a Program

rounded_version p ≡ 〈State = S p, Pre = Pre p , post = post p / Pre p〉

exact_version [] :: ‘a Program ⇒ ‘a Program

exact_version p ≡ 〈State = S p, Pre = Pre p ∩ Domain (post p) , post = post p / Pre p〉

civilized_n [] :: ‘a Program ⇒ ‘a Program set ⇒ nat ⇒ bool

civilized_n x B 0 = (((x ∈ B) ∨ x = Fail {} ∨ x = Skip (complete_state (set_to_list B))) ∧ finite B)

civilized_n x B (n + 1) = (((∃a b. civilized_n a B n ∧ civilized_n b B n ∧ (a ; b = x ∨ a ∪ b = x)) ∧ finite B) ∨ civilized_n x B n)

civilized [] :: ‘a Program ⇒ ‘a Program set ⇒ bool

civilized x B ≡ (∃n. civilized_n x B n)

equal_cnf [] :: ‘a CNF ⇒ ‘a CNF ⇒ bool

equal_cnf a b ≡ (set a = set b) ∧ (size a = 1) = (size b = 1)

restrict_path [] :: ‘a Program list ⇒ ‘a set ⇒ ‘a Program list

restrict_path [ ] C = [ ]

restrict_path (x#xs) C = (x / C)#xs

restriction_cnf [/] :: ‘a CNF ⇒ ‘a set ⇒ ‘a CNF

restriction_cnf p C ≡ [restrict_path path_p C. path_p ← p]

corestrict_path [] :: ‘a Program list ⇒ ‘a set ⇒ ‘a Program list

corestrict_path [ ] C = [ ]

corestrict_path (xs@[x]) C = xs@[x ∖ C]

corestriction_cnf [∖] :: ‘a CNF ⇒ ‘a set ⇒ ‘a CNF

corestriction_cnf p C ≡ [corestrict_path path_p C. path_p ← p]

complete_cnf_state [] :: ‘a CNF ⇒ ‘a set

complete_cnf_state p ≡ ⋃ {complete_state tr

tr. tr ∈ set p }

normal_of [] :: ‘a CNF ⇒ ‘a Program set ⇒ bool

normal_of p xs ≡ (basic p ⊆ (xs ∪ {Fail {}, Skip (complete_state (set_to_list xs))})) ∧ finite xs

feas_of [] :: ‘a Program ⇒ ‘a Program

feas_of p ≡ 〈State=S p, Pre=Pre p ∩ Domain (post p), post=post p〉

set_to_list_r [] :: ‘a set ⇒ ‘a list

set_to_list_r s = (SOME l. set l = s)

factorial [] :: nat ⇒ nat

factorial 0 = 1

factorial (n + 1) = (n + 1) * factorial n

sum [] :: nat list ⇒ nat

sum [ ] = 0

sum (x#xs) = x + sum xs

nmb_interleavings_pre [] :: nat ⇒ nat ⇒ nat

nmb_interleavings_pre x y ≡ factorial (x + y) div (factorial x * factorial y)

nmb_interleavings [] :: ‘a list ⇒ ‘a list ⇒ nat

nmb_interleavings xs ys ≡ nmb_interleavings_pre (size xs) (size ys)

list_equiv [] :: ‘a Program list ⇒ ‘a Program list ⇒ bool

list_equiv [ ] [ ] = True

list_equiv (x#xs) (y#ys) = ((x ≡ y) ∧ list_equiv xs ys)

list_equiv _ _ = False

cnf_size [] :: ‘a CNF ⇒ nat

cnf_size [ ] = 0

cnf_size (x#xs) = length x + cnf_size xs + 1

equiv_list [] :: ‘a Program list ⇒ ‘a Program list ⇒ bool

equiv_list [ ] [ ] = True

equiv_list (x#xs) [ ] = False

equiv_list [ ] (y#ys) = False

equiv_list (x#xs) (y#ys) = (x ≡ y ∧ equiv_list xs ys)

cnf_concurrency2 [] :: ‘a CNF ⇒ ‘a CNF ⇒ ‘a set ⇒ ‘a Program

cnf_concurrency2 [ ] ys C = Fail {}

cnf_concurrency2 xs [ ] C = Fail {}

cnf_concurrency2 (x#xs) (y#ys) C = (case (xs , ys) of ([ ], [ ]) ⇒ (case (x, y) of ([ ], [ ]) ⇒ Skip C | ([a], [b]) ⇒ a;b ∪ b;a | ([ ], bs) ⇒ evaluate [bs] C | (as, [ ]) ⇒ evaluate [as] C | (a#as, b#bs) ⇒ a; (cnf_concurrency2 [as] [b#bs] C) ∪ b; (cnf_concurrency2 [a#as] [bs] C)) | (f#fs, [ ]) ⇒ cnf_concurrency2 [x] [y] C ∪ cnf_concurrency2 (f#fs) [y] C | ([ ], g#gs) ⇒ cnf_concurrency2 [x] [y] C ∪ cnf_concurrency2 [x] (g#gs) C | (f#fs, g#gs) ⇒ cnf_concurrency2 [x] (y#g#gs) C ∪ cnf_concurrency2 (f#fs) (y#g#gs) C )

Relation_operations.thy

restrict_r [/] :: ‘a rel ⇒ ‘a set ⇒ ‘a rel

restrict_r R S = {r ∈ R. fst r ∈ S}

inv_restrict_r [/_-] :: ‘a rel ⇒ ‘a set ⇒ ‘a rel

inv_restrict_r R S = {r ∈ R. fst r ∉ S}

corestrict_r [∖] :: ‘a rel ⇒ ‘a set ⇒ ‘a rel

corestrict_r R S = {r ∈ R. snd r ∈ S}

inv_corestrict_r [∖_-] :: ‘a rel ⇒ ‘a set ⇒ ‘a rel

inv_corestrict_r R S = {r ∈ R. snd r ∉ S}

is_function [] :: ‘a rel ⇒ bool

is_function R = (∀r₁ ∈ R.∀r₂∈R. fst r₁ = fst r₂ → snd r₁ = snd r₂)

Theorems and Lemmas

PRISM.thy

cond_for_commutative_1

Range_p p₁ ∩ Pre p₂ = {} ⟹ Range_p p₂ ∩ Pre p₁ = {} ⟹ commute_programs3 p₁ p₂

distinct_state_range_dist_from_pre

used_states p₁ ∩ used_states p₂ = {} ⟹ Range_p p₁ ∩ Pre p₂ = {} ∧ Range_p p₂ ∩ Pre p₁ = {}

used_states p₁ ∩ used_states p₂ = {} ⟹ commute_programs1 p₁ p₂

x ; until_loop a C b n ≡ until_loop (x ; a) C b n

p ; q ≡ p ; (q / (Range_p p))

T_03_Basic_programs.thy

special_empty1

Skip {} = Fail {}

special_empty2

Havoc {} = Fail {}

special_empty3

Havoc {} = Infeas {}

Havoc C = 〈State=C, Pre=TRUE C, post=TRUE C 〉

Skip C = 〈State=C, Pre=TRUE C, post=ID C〉

Fail C = 〈State=C, Pre=FALSE, post=FALSE〉

Infeas C = 〈State=C, Pre=TRUE C, post=FALSE〉

special_refine1

Infeas C ⊑ Skip C

special_refine2

Skip C ⊑ Havoc C

special_refine3

Havoc C ⊑ Fail C

special_refine4

Infeas C ⊑ Fail C

special_specialize1

Fail C ⊆ Infeas C

special_specialize2

Infeas C ⊆ Skip C

special_specialize3

Skip C ⊆ Havoc C

C ⊆ D ⟹ Fail D ⊑ Fail C

C ⊆ D ⟹ Fail C ⊆ Fail D

C ⊆ D ⟹ Infeas D ⊑ Infeas C

C ⊆ D ⟹ Infeas C ⊆ Infeas D

C ⊆ D ⟹ Skip D ⊑ Skip C

C ⊆ D ⟹ Skip C ⊆ Skip D

C ⊆ D ⟹ Havoc C ⊑ Havoc D

C ⊆ D ⟹ Havoc D ⊑ Havoc C

C ⊆ D ⟹ Havoc C ⊆ Havoc D

Characteristic_relation.thy

char_rel_is_unique_in_equality_1

p₁ = p₂ ⟹ char_rel p₁ = char_rel p₂

equal_charrel1

p₁ = p₂ ⟹ char_rel p₁ = char_rel p₂

equiv_charrel1

p₁ ≡ p₂ ⟹ char_rel p₁ = char_rel p₂

char_rel_is_unique_in_equality_2

all_feasible [p₁, p₂] ⟹ (char_rel p₁ = char_rel p₂) ⟹ (p₁ = p₂)

char_rel_is_unique_in_equal_2

all_feasible [p₁, p₂] ⟹ (char_rel p₁ = char_rel p₂) ⟹ (p₁ = p₂)

equiv_charrel2

all_feasible [p₁, p₂] ⟹ (char_rel p₁ = char_rel p₂) = (p₁ ≡ p₂)

char_rel_choice

char_rel (p₁ ∪ p₂) = char_rel p₁ ∪ char_rel p₂

char_rel_composition

char_rel (p₁ ; p₂) = char_rel p₁ O char_rel p₂

char_rel_restriction

char_rel (p / C) = char_rel p / C

char_rel_corestriction

char_rel (p ∖ C) = char_rel p ∖ C

char_rel_strengthens

strengthens p₁ p₂ ⟹ char_rel p₁ / Domain (char_rel p₂) ⊆ char_rel p₂

char_rel_weakens

is_feasible p₁ ⟹ weakens p₁ p₂ ⟹ Domain (char_rel p₂) ⊆ Domain (char_rel p₁)

char_rel_prop1

p ⊑ q ⟹ char_rel p / (Domain (char_rel q)) ⊆ char_rel q

charrel_strengthen

all_feasible [p, q] ⟹ char_rel p / (Domain (char_rel q)) ⊆ char_rel q = strengthens p q

charrel_weaken

all_feasible [p, q] ⟹ Domain (char_rel q) ⊆ Domain (char_rel p) = weakens p q

charrel_specialize

q ⊆ p ⟹ char_rel q < char_rel p

charrel_refine

q ⊑ p ⟹ char_rel q / (Pre p) < char_rel p

char_rel_prop6

Field (char_rel a) ⊆ S a

Definitions.thy

〈State={}, Pre={1::nat}, post={(1,2)}〉 ⊆ 〈State={}, Pre={1::nat}, post={(1,2)}〉

Pre p ⊆ I ∧ Range_p p ⊆ I ⟹ Range_p (p / I) ⊆ I

a ∪ (a ∩ b) ≡ a

a ∩ (a ∪ b) ≡ a

civ_n_finite

civilized_n p B n ⟹ finite B

Equalities.thy

equals_equiv_relation_1

p₁ = p₂ ⟹ p₁ = p₂

equals_equiv_relation_2

p₁ = p₂ ⟹ p₁ ≡ p₂

equals_equiv_relation_3

p₁ = p₂ ⟹ p₁ ≡ p₂

equal_is_reflexive

p₁ = p₁

equiv_is_reflexive

p₁ ≡ p₁

equal_is_symetric

p₁ = p₂ ⟹ p₂ = p₁

equiv_is_symetric

p₁ ≡ p₂ ⟹ p₂ ≡ p₁

equal_is_transitive

p₁ = p₂ ⟹ p₂ = p₃ ⟹ p₁ = p₃

equiv_is_transitive

p₁ ≡ p₂ ⟹ p₂ ≡ p₃ ⟹ p₁ ≡ p₃

inverse_equality_1

¬ p₁ ≡ p₂ ⟹ ¬ p₁ = p₂

inverse_equality_2

¬ p₁ ≡ p₂ ⟹ ¬ p₁ = p₂

inverse_equality_3

¬ p₁ = p₂ ⟹ ¬ p₁ = p₂

empty_state_space_equal

S a = {} ⟹ S b = {} ⟹ a = b

Feasibility.thy

equal_maintains_feasiblity

is_feasible p₁ ⟹ p₁ = p₂ ⟹ is_feasible p₂

equiv_maintains_feasiblity

is_feasible p₁ ⟹ p₁ ≡ p₂ ⟹ is_feasible p₂

Helper.thy

rel_id_prop

Field a ⊆ C ⟹ a O Id_on C = a

list_comp_prop_1

∀p. [p i. i ← [0..((int (n + 1)))]] = [p i. i ← [0..(int n)]] @ [p ((int (n + 1)))]

orig_is_permutation_1

List.member (insert_all x xs) (x#xs)

permutation_reflexive

List.member (permutations xs) xs

set (insert_all x (ps)) ≠ {}

x#xs ∈ set (insert_all x xs)

xs@[x] ∈ set (insert_all x xs)

a@x#b ∈ set (insert_all x (a@b))

p ∈ set (insert_all x (a # xs)) ⟹ (hd p = x) ∨ (hd p = a)

l5_2

p ∈ set (insert_all x (a # xs)) ⟹ (h_hd p = [x]) ∨ (h_hd p = [a])

h_hd p = [x] ⟹ hd p = x

h_tl p = x ≡ tl p = x

(h_hd p)@(h_tl p) = p

a#p ∈ set (insert_all x (a # xs)) ⟹ p ∈ set (insert_all x xs)

l10

p ∈ set (insert_all x xs) ⟹ ∃a b. a@x#b=p

l11

p ∈ set (insert_all x ps) ⟹ x ∈ set p

l12

y ∈ set p ⟹ p ∈ set (insert_all x (a # ps)) ⟹ y ≠ a ⟹ p’ ∈ set (insert_all x ps) ⟹ y ∈ set p’

l13

y ∈ set p ⟹ p ∈ set (insert_all x ps) ⟹ y ∉ set ps ⟹ y = x

permutation_symmetric_1

List.member (permutations xs) p ⟹ List.member p y ⟹ List.member xs y

l14

p ∈ set (insert_all x ps) ⟹ ∃a b. p = a @ x # b ∧ ps = a @ b

count_invariant

List.member (permutations xs) p ⟹ count_list p y = count_list xs y

permutation_split

List.member (permutations (x#xs)) xs’ ⟹ ∃a b. a@x#b = xs’

permutation_size

List.member (permutations x1) x2 ⟹ size x2 = size x1

insert_perm_rel

x ∈ set (insert_all a xs) ⟹ x ∈ set (permutations (a#xs))

insert_all_set_equality

p1 ∈ set (insert_all x ps) ⟹ set p1 = insert x (set ps)

permutation_set_equality

p1 ∈ set (permutations xs) ⟹ set xs = set p1

permutation_set_equality_2

p1 ∈ set (permutations xs) ⟹ p2 ∈ set (permutations xs) ⟹ set p1 = set p2

permutation_split_set

x2 ∈ set (permutations (a # x1)) ⟹ ∃y z. x2 = y @ a # z ∧ y @ z ∈ set (permutations x1)

insert_4

(xs @ ([x] @ ys)) ∈ set (insert_all x (xs @ ys))

count_eq_member

List.count_list p y > 0 = List.member p y

member_invariant

p ∈ set (permutations xs) ⟹ List.member p y ⟹ List.member xs y

length_prop_1

List.member xs x ⟹ ∃a b. a@[x]@b = xs

length_prop_2

count_list (a @ [x] @ b) x = Suc (count_list (a @ b) x)

length_prop_3

x₁≠x₂ ⟹ xs = a@[x₂]@b ⟹ count_list (xs) x₁ = count_list (a@b) x₁

length_prop_4

x₁=x₂ ⟹ xs = a@[x₂]@b ⟹ count_list (xs) x₁ = Suc (count_list (a@b) x₁)

length_prop_5

∀x₁. count_list (a # xs) x₁ = count_list (a # xs’) x₁ ⟹ ∀x₁. count_list (xs) x₁ = count_list (xs’) x₁

length_prop_6

∀x₁. count_list xs x₁ = count_list xs’ x₁ ⟹ length xs = length xs’

length_inv

x ∈ set (permutations xs) ⟹ length x = length xs

perm_inv_2

xb@xe ∈ set (permutations x1) ⟹ xb@a#xe ∈ set (permutations (a # x1))

singleton_permutation

[x] ∈ set (permutations xs) ⟹ xs = [x]

count_invariant_2

∀y. count_list p y = count_list xs y ⟹ List.member (permutations xs) p

count_invariant_3

x1 ∉ set (permutations x2) ⟹ ∃t. count_list x1 t ≠ count_list x2 t

permutations_set_equality

x1 ∈ set (permutations x2) ⟹ set (permutations x1) = set (permutations x2)

perm_lemma_1

x1 ∉ set (permutations x2) ⟹ a # x1 ∉ set (permutations (a # x2))

perm_split

a # x1 ∈ set (permutations (y @ a # z)) ⟹ x1 ∈ set (permutations (y @ z))

perm_inv_3

x1 ∈ set (permutations x2) ⟹ x2 ∈ set (permutations x1)

orig_is_permutation_3

List.member (permutations x1) x2 ⟹ List.member (permutations x2) x1

complete_state_prop_1

fold (λ p s. S p ∪ s) xs C = foldl (λ s p. S p ∪ s) C xs

complete_state_prop_2

complete_state xs = fold (∪) (map (λp. S p) xs) {}

complete_state_prop_3

fold (λ p s. S p ∪ s) xs C = fold (∪) (map (λp. S p) xs) C

complete_state_prop_4

fold (∪) xs C = fold (∪) xs {} ∪ C

complete_state_prop_5

fold (∪) (map (λp. S p) xs) C = fold (∪) (map (λp. S p) xs) {} ∪ C

complete_state_prop

complete_state (x # xs) = complete_state xs ∪ S x

permutation_complete_state_equality

x1 ∈ set (permutations x2) ⟹ complete_state x2 = complete_state x1

permutation_S_equiv

x1 ∈ set (permutations x2) ⟹ fold (∪) (map (λp. S p) x1) {} ≡ fold (∪) (map (λp. S p) x2) {}

complete_state_union_1

complete_state (a # xs) = complete_state (xs) ∪ complete_state ([a])

complete_state_union_2

complete_state (xs) = complete_state (xs) ∪ complete_state ([ ])

complete_state_union_3

complete_state (a @ b) = complete_state a ∪ complete_state b

perm_1

x ∈ set (permutations xs) ⟹ a#x ∈ set (permutations (a#xs))

perm_2

set (permutations (a#xs)) = set (permutations (xs@[a]))

perm_3

set (permutations ([a]@st@ed)) = set (permutations (st@[a]@ed))

x ∈ set (permutations xs) ⟹ y ∈ set (permutations ys) ⟹ x@y ∈ set (permutations (xs@ys))

elements_atomic

x ∈ get_atomic p ⟹ is_atomic x

empty_prop1

finite s ⟹ set_to_list s = [ ] ≡ s = {}

empty_prop2

is_feasible p ⟹ get_atomic p = {} ⟹ Pre p = {}

finite_prop1

finite xs ⟹ finite ys ⟹ finite {f a b

a b . a ∈ xs ∧ b ∈ ys}

finite_prop2

finite xs ⟹ finite ys ⟹ finite {f a b

a b . (a, b) ∈ xs ∧ a ∉ ys}

finite_relation

finite r ≡ finite (Field r)

decomp_program

finite (S p) ⟹ x ∉ F ⟹ S p = insert x F ⟹ q = 〈State={s

s. s ∈ State p ∧ s ∈ F}, Pre={s

s. s ∈ Pre p ∧ s ∈ F}, post={(a,b)

a b. a ∈ F ∧ b ∈ F ∧ (a,b) ∈ post p}〉 ⟹ r = 〈State={s

s. s ∈ State p}, Pre={s

s. s ∈ Pre p}, post={(a,b)

a b. (a = x ∨ b = x) ∧ (a,b) ∈ post p}〉 ⟹ p ≡ q ∪ r

decomp_program2

finite (S p) ⟹ x ∉ F ⟹ S p = insert x F ⟹ finite (S 〈State={s

s. s ∈ State p ∧ s ∈ F}, Pre={s

s. s ∈ Pre p ∧ s ∈ F}, post={(a,b)

a b. a ∈ F ∧ b ∈ F ∧ (a,b) ∈ post p}〉)

decomp_program3

finite (S p) ⟹ x ∉ F ⟹ S p = insert x F ⟹ finite (S 〈State={s

s. s ∈ State p}, Pre={s

s. s ∈ Pre p}, post={(a,b)

a b. (a = x ∨ b = x) ∧ (a,b) ∈ post p}〉)

card_prop

finite a ⟹ b ∩ c = {} ⟹ a = b ∪ c ⟹ card a = card b + card c

card_prop2

finite b ⟹ finite c ⟹ b ∩ c = {} ⟹ a = b ∪ c ⟹ card a = card b + card c

finite_prop3

finite x ⟹ finite {f a

a . a ∈ x}

finite_prop4

finite x ⟹ finite {f a b

a b. (a, b) ∈ x}

finite_prop5

finite (S p) ⟹ finite (get_atomic p)

atomic_idem

is_atomic p ⟹ (get_atomic p) ∪ {p} = get_atomic (p ∪ p)

atomic_state

is_atomic x ⟹ S x = State x

atomic_prop1

is_atomic x ⟹ ∃a b. 〈State={a,b}, Pre={a}, post={(a,b)}〉 = x

atomic_prop2

∃a b. 〈State={a,b}, Pre={a}, post={(a,b)}〉 = x ⟹ is_atomic x

atomic_prop3

∃a b. 〈State={a,b}, Pre={a}, post={(a,b)}〉 = x ≡ is_atomic x

atomic_post

is_atomic x ⟹ restr_post x = post x

atomic_monotone

get_atomic p ⊆ get_atomic (p ∪ q)

atomic_split

finite (get_atomic p) ⟹ finite (get_atomic q) ⟹ (get_atomic p) ∪ (get_atomic q) = get_atomic (p ∪ q)

is_atomic x ⟹ (get_atomic p) ∪ {x} = get_atomic (p ∪ x)

fail_atomic

get_atomic (Fail {}) = {}

set_list_set

finite xs ⟹ set (set_to_list xs) = xs

set_list_prop

finite F ⟹ xs = set_to_list (insert x F) ⟹ ∃a b. a@x#b = xs

set_to_list_distinct

xs = set_to_list F ⟹ distinct xs

set_to_list_size

size (set_to_list F) = card F

set_to_list_one

set_to_list {x} = [x]

atomic_prop_1

is_atomic x ⟹ get_atomic x = {x}

Consistent_feasible

is_feasible (feasible_version p)

Consistent_round

is_rounded (rounded_version p)

Consistent_exact

is_exact (exact_version p)

Feasible_round

is_feasible p ⟹ is_feasible (rounded_version p)

Round_feasible

is_rounded p ⟹ is_rounded (feasible_version p)

Equiv_prog

a ≡ b ≡ (Pre (rounded_version a) = Pre (rounded_version b) ∧ post (rounded_version a) = post (rounded_version b))

Charrel_restriction

rounded_version (p / C) = rounded_version p / C

Charrel_choice

rounded_version (p ∪ q) = rounded_version p ∪ rounded_version q

Charrel_composition

rounded_version (p ; q) = rounded_version p ; rounded_version q

Charrel_corestriction

rounded_version (p ∖ C) = rounded_version p ∖ C

Restrict_rounded

is_rounded p ⟹ is_rounded (p / C)

Choice_rounded

is_rounded (p ∪ q)

is_rounded q ⟹ is_rounded p ⟹ is_rounded (p ; q)

Corestrict_feasible

is_feasible p ⟹ is_feasible ((p / (Pre p ∩ Domain (post p ∖ C))) ∖ C)

Implementation.thy

implementation_1

x ∈ X ⟹ x ∈ Domain (R) ⟹ x ∈ Domain (R / X)

implementation_theorem

implements p₂ p₁ ⟹ is_feasible p₁

implementation_is_reflexive

is_feasible p₁ ⟹ implements p₁ p₁

implementation_is_transitive

implements p₁ p₂ ⟹ implements p₂ p₃ ⟹ implements p₁ p₃

implementation_is_antisymetric

implements p₁ p₂ ⟹ implements p₂ p₁ ⟹ p₁ ≡ p₂

Independence.thy

independent_symetric

independent p₁ p₂ = independent p₂ p₁

independent_weakens

independent p₁ p₂ ⟹ Pre p₂ ≠ {} ⟹ ¬ weakens p₁ p₂

independent_strengthens

independent p₁ p₂ ⟹ strengthens p₁ p₂

Range_p.thy

same_range_p_3

p₁ ≡ p₂ ⟹ Range_p p₁ = Range_p p₂

same_range_p_2

a = b ⟹ Range_p a = Range_p b

range_p_explicit_1

y ∈ Range_p a ⟹ ∃x. (x,y) ∈ post a ∧ x ∈ Pre a

range_p_explicit_2

(x,y) ∈ post a ∧ x ∈ Pre a ⟹ y ∈ Range_p a

no_range_fail

is_feasible p ⟹ Range_p p = {} ⟹ p ≡ Fail {}

Refinement.thy

refines_is_reflexive

p₁ ⊑ p₁

refines_is_transitive_e

p₁ ⊑ p₂ ⟹ p₂ ⊑ p₃ ⟹ extends p₁ p₃

refines_is_transitive_w

p₁ ⊑ p₂ ⟹ p₂ ⊑ p₃ ⟹ weakens p₁ p₃

refines_is_transitive_s

p₁ ⊑ p₂ ⟹ p₂ ⊑ p₃ ⟹ strengthens p₁ p₃

refines_is_transitive

p₁ ⊑ p₂ ⟹ p₂ ⊑ p₃ ⟹ p₁ ⊑ p₃

refines_is_antisymetric

p₁ ⊑ p₂ ⟹ p₂ ⊑ p₁ ⟹ p₁ ≡ p₂

refines_is_preorder

p₁ ⊑ p₁ ∧ (p₂ ⊑ p₃ ∧ p₃ ⊑ p₄ → p₂ ⊑ p₄)

refines_is_order

(p₁ ⊑ p₁) ∧ (p₂ ⊑ p₃ ∧ p₃ ⊑ p₄ → p₂ ⊑ p₄) ∧ (p₅ ⊑ p₆ ∧ p₆ ⊑ p₅ → p₅ ≡ p₆)

extends_is_reflexive

extends p p

extends_is_transitive

extends p q ⟹ extends q r ⟹ extends p r

weakens_is_reflexive

weakens p p

weakens_is_transitive

weakens p q ⟹ weakens q r ⟹ weakens p r

strengthens_is_reflexive

strengthens p p

strengthens_is_transitive_1

weakens p q ⟹ weakens q r ⟹ strengthens p q ⟹ strengthens q r ⟹ strengthens p r

strengthens_is_transitive_2

weakens q p ⟹ weakens r q ⟹ strengthens p q ⟹ strengthens q r ⟹ strengthens p r

Relation_operations.thy

corestriction_restriction_on_relcomp

r₁ ∖ s₁ O r₂ = r₁ O r₂ / s₁

Subprogram.thy

specialize_is_reflexive

p₁ ⊆ p₁

specialize_is_transitive

p₁ ⊆ p₂ ⟹ p₂ ⊆ p₃ ⟹ p₁ ⊆ p₃

specialize_is_antisymetric

p₁ ⊆ p₂ ⟹ p₂ ⊆ p₁ ⟹ p₁ ≡ p₂

specialize_is_preorder

p₁ ⊆ p₁ ∧ (p₂ ⊆ p₃ ∧ p₃ ⊆ p₄ → p₂ ⊆ p₄)

specialize_is_order

(p₁ ⊆ p₁) ∧ (p₂ ⊆ p₃ ∧ p₃ ⊆ p₄ → p₂ ⊆ p₄) ∧ (p₅ ⊆ p₆ ∧ p₆ ⊆ p₅ → p₅ ≡ p₆)

choice_decomp_1

a ⊆ c ∧ b ⊆ c ⟹ a ∪ b ⊆ c

choice_decomp_2

a ∪ b ⊆ c ⟹ a ⊆ c ∧ b ⊆ c

choice_decomp

a ⊆ c ∧ b ⊆ c ≡ a ∪ b ⊆ c

specialize_equiv

a ⊆ b ⟹ a ≡ c ⟹ b ≡ d ⟹ c ⊆ d

equiv_specialize_transitivity

S a ⊆ S b ⟹ S c ⊆ S d ⟹ a ≡ b ⟹ b ⊆ c ⟹ c ≡ d ⟹ a ⊆ d

Validity.thy

valid_generalization

is_valid p ⟹ prop (S p) = prop (State p)

pre_in_s

is_valid p ⟹ Pre p ⊆ State p

post_in_s

is_valid p ⟹ (Field (post p) ⊆ State p)

validity_inverse

is_valid p ⟹ is_valid (p ^-¹)

validity_composition

all_valid [p₁, p₂] ⟹ is_valid (p₁ ; p₂)

validity_choice

all_valid [p₁, p₂] ⟹ is_valid (p₁ ∪ p₂)

validity_restriction

is_valid p ⟹ is_valid (p / C)

validity_corestriction

is_valid p ⟹ is_valid (p ∖ C)

validity_equality

is_valid p ⟹ is_valid q ⟹ p = q ⟹ p = q

Choice.thy

choice_idem_4

Fail {} ∪ (p ∪ p) = Fail {} ∪ p

choice_idem_5

q ∪ (p ∪ p) = q ∪ p

choice_idem_6

(p ∪ p) ∪ q = p ∪ q

choice_equiv

f₁ ≡ p₁ ⟹ f₂ ≡ p₂ ⟹ f₁ ∪ f₂ ≡ p₁ ∪ p₂

equality_is_maintained_by_choice

f₁ = p₁ ⟹ f₂ = p₂ ⟹ f₁ ∪ f₂ = p₁ ∪ p₂

choice_feasible

all_feasible [p₁, p₂] ⟹ is_feasible (p₁ ∪ p₂)

condition_for_choice_simplification

Range_p a ∩ Pre y = {} ⟹ Range_p x ∩ Pre b = {} ⟹ a ; b ∪ x ; y ≡ (a ∪ x) ; (b ∪ y)

choice_range

Range_p (p₁ ∪ p₂) = Range_p p₁ ∪ Range_p p₂

refinement_safety_choice_e

q₁ ⊑ p₁ ⟹ q₂ ⊑ p₂ ⟹ extends (q₁ ∪ q₂) (p₁ ∪ p₂)

refinement_safety_choice_w

q₁ ⊑ p₁ ⟹ q₂ ⊑ p₂ ⟹ weakens (q₁ ∪ q₂) (p₁ ∪ p₂)

refinement_safety_choice_s_1

q₁ ⊑ p₁ ⟹ q₂ ⊑ p₂ ⟹ strengthens (q₁ ∪ q₂) (p₁ ∪ p₂)

refinement_safety_choice_s_2

strengthens q₁ p₂ ⟹ strengthens q₂ p₁ ⟹ q₁ ⊑ p₁ ⟹ q₂ ⊑ p₂ ⟹ strengthens (q₁ ∪ q₂) (p₁ ∪ p₂)

refinement_safety_choice

q₁ ⊑ p₁ ⟹ q₂ ⊑ p₂ ⟹ (q₁ ∪ q₂) ⊑ (p₁ ∪ p₂)

refinement_safety_choice

strengthens a c ⟹ a ⊑ b ⟹ (a ∪ c) ⊑ (b ∪ c)

refinement_safety_choice_1

strengthens q₁ p₂ ⟹ strengthens q₂ p₁ ⟹ q₁ ⊑ p₁ ⟹ q₂ ⊑ p₂ ⟹ (q₁ ∪ q₂) ⊑ (p₁ ∪ p₂)

refinement_safety_choice_2

independent q₁ p₂ ⟹ independent q₂ p₁ ⟹ q₁ ⊑ p₁ ⟹ q₂ ⊑ p₂ ⟹ (q₁ ∪ q₂) ⊑ (p₁ ∪ p₂)

choice_safety1

a ⊆ b ⟹ a ∪ c ⊆ b ∪ c

implements_safety_choice

is_feasible c ⟹ implements a b ⟹ implements (a ∪ c) (b ∪ c)

implements_safety_choice

strengthens a c ⟹ is_feasible c ⟹ implements a b ⟹ implements (a ∪ c) (b ∪ c)

program_is_specialize_of_choice

p₁ ⊆ (p₁ ∪ p₂)

choice_choice_range

Range_p p ⊆ Range_p (p ∪ q)

choice_range_p_prop_2

x ∈ Range_p (p ∪ q) ⟹ x ∉ Range_p p ⟹ x ∈ Range_p q

choice_range_p_prop_3

x ∉ Range_p (p ∪ q) ⟹ x ∉ Range_p p

empty_is_neutral

S a = {} ⟹ a ∪ (b ∪ c) = b ∪ c

choice_idem_2

a ∪ (a ∪ b) = a ∪ b

choice_suprogram_prop

a ⊆ c ⟹ b ⊆ c ⟹ a ∪ b ⊆ c

Composition.thy

composition_simplification_1

p₁ ; p₂ = p₁ ∖ Pre p₂ ; p₂

composition_simplification_2

p₁ ; p₂ = p₁ ; p₂ / Pre p₂

composition_equiv

f₁ ≡ p₁ ⟹ f₂ ≡ p₂ ⟹ f₁ ; f₂ ≡ p₁ ; p₂

equality_is_maintained_by_composition

f₁ = p₁ ⟹ f₂ = p₂ ⟹ f₁ ; f₂ = p₁ ; p₂

compose_feasible_lemma

all_feasible [p₁, p₂] ⟹ Domain ((post p₁) ∖ (Pre p₂)) = Domain ((post p₁) ∖ (Pre p₂) O post p₂)

compose_feasible2

all_feasible [p₁, p₂] ⟹ is_feasible (p₁ ; p₂)

composition_removes_dead_code_1

p / (Pre p) ; q ≡ p ; q

composition_removes_dead_code_2

p ; q / (Pre q) ≡ p ; q

compose_feasible

is_feasible p₂ ⟹ is_feasible (p₁ ; p₂)

p₁ ; p₂ ≡ 〈State ={}, Pre=Pre p₁ ∩ Domain (post p₁ ∖ Pre p₂), post=post p₁〉 ; p₂

range_decreases_composition

Range_p (y ; x) ⊆ Range_p x

p ⊑ q ⟹ p ; a ⊑ q ; a

composition_subsafety

a ⊆ b ⟹ a ; c ⊆ b ; c

composition_subsafety2

a ⊆ b ⟹ c ; a ⊆ c ; b

comp_range_p_prop

Range_p (q) ⊆ C ⟹ Range_p (p ; q) ⊆ C

comp_range_p_prop_2

x ∉ Range_p q ⟹ x ∉ Range_p (p ; q)

connecting_element

(x,y) ∈ post (a ; b) ⟹ ∃z. (x,z) ∈ post a ∧ (z,y) ∈ post b ∧ z ∈ Pre b

knowing_pre_composition

x ∈ Pre (a) ⟹ (x, y) ∈ post (a ; b) ⟹ x ∈ Pre (a ; b)

Corestriction.thy

corestrict_idem

(p ∖ C) ∖ C = p ∖ C

corestrict_prop_1

Range_p (p ∖ D) ⊆ D

corestrict_prop_2

Range_p (p ∖ D) ⊆ Range_p p

corestrict_prop_

Range_p (p ∖ D) ⊆ Range_p p ∩ D

NOT_corestricted_p_refines_p

p ∖ C ⊑ p

NOT_p_refines_corestricted_p

p ⊑ p ∖ C

corestricted_refines_unrestricted_1

p ∖ C ⊑ p

unrestricted_refines_corestricted_1

p ⊑ p ∖ C

corestricted_refines_unrestricted_2

is_feasible p ⟹ p ∖ C ⊑ p

unrestricted_refines_corestricted_2

is_feasible p ⟹ p ⊑ p ∖ C

corestrict_subprog

p ∖ C ⊆ p

unrestricted_weakens_corestricted

weakens p (p ∖ C)

corestricted_strengthens_unrestricted

strengthens (p ∖ C) p

corestriction_prop

D ⊆ C ⟹ p ∖ D ⊑ p ∖ C

corestriction_prop

D ⊆ C ⟹ p ∖ C ⊑ p ∖ D

corestriction_weakens_prop

D ⊆ C ⟹ weakens (p ∖ C) (p ∖ D)

corestriction_strengthens_prop

D ⊆ C ⟹ strengthens (p ∖ D) (p ∖ C)

corestrict_subprogorder1

D ⊆ C ⟹ (p ∖ D) ⊆ (p ∖ C)

equivalence_is_maintained_by_corestriction

f₁ ≡ p₁ ⟹ (f₁ ∖ C) ≡ p₁ ∖ C

equality_is_maintained_by_corestriction

f₁ = p₁ ⟹ (f₁ ∖ C) = p₁ ∖ C

corestrict_feasible

is_feasible p ⟹ is_feasible (p ∖ C)

corestriction_subsafety

q ⊆ p ⟹ q ∖ C ⊆ p ∖ C

refinement_safety_corestriction

q ⊑ p ⟹ q ∖ C ⊑ p ∖ C

implements_safety_corestriction

implements a b ⟹ implements (a ∖ C) (b ∖ C)

weakens_corestriction_1

all_feasible [p, q] ⟹ q ⊑ p ⟹ weakens (q ∖ C) (p ∖ C)

weakens_corestriction_2

q ⊑ p ⟹ weakens (p ∖ C) (q ∖ C)

strengthens_corestriction_1

q ⊑ p ⟹ strengthens (p ∖ C) (q ∖ C)

strengthens_corestriction_2

q ⊑ p ⟹ strengthens (q ∖ C) (p ∖ C)

corestrict_range_prop

x ∈ C ⟹ x ∉ Range_p (p ∖ C) ⟹ x ∉ Range_p (p)

corestrict_range_prop_2

is_feasible a ⟹ Range_p a ⊆ C ⟹ a ∖ C ≡ a

corestrict_range_prop_3

Range_p(a) ∩ C = {} ⟹ a∖C ≡ Fail {}

corestrict_range_porp_4

is_feasible p ⟹ p ∖ Range_p p ≡ p

corestrict_inter

(p ∖ C) ∖ D = p∖ (C ∩ D)

corestrict_commute

(p ∖ C) ∖ D = (p ∖ D) ∖ C

Inverse.thy

inverse_feasible

is_feasible p ⟹ is_feasible (p ^-¹)

inverse_of_inverse_is_self

is_feasible p ⟹ p ^-¹^-¹ ≡ p

pre_of_inverse

is_deterministic (p ^-¹) ⟹ Pre p = Pre (p ; (p ^-¹))

pre_is_unchanged

is_feasible p ⟹ Pre (p ; (p ^-¹)) = Pre p

post_is_identity

is_deterministic (p ^-¹) ⟹ (x,y)∈ restr_post (p ; (p ^-¹)) ⟹ x = y

post_is_identity_2

is_deterministic (p ^-¹) ⟹ (x,y)∈ restr_post (p ; (p ^-¹)) ⟹ x = y

post_of_inverse

is_feasible p ⟹ is_deterministic (p ^-¹) ⟹ restr_post (Skip (Pre p)) = restr_post (p ; (p ^-¹))

inverse_reverses_composition_1

is_feasible p ⟹ is_deterministic (p ^-¹) ⟹ Skip (Pre p) ≡ (p ; (p ^-¹))

inverse_reverses_composition_2

Skip (S p) ⊑ (p ; (p ^-¹))

equivalence_is_maintained_by_inverse

f ≡ p ⟹ f ^-¹ ≡ p ^-¹

equality_is_maintained_by_inverse

f = p ⟹ f ^-¹ = p ^-¹

refinement_safety_inverse

S f = S g ⟹ all_feasible [f, g] ⟹ f ⊑ g ⟹ (g ^-¹) ⊑ (f ^-¹)

inverse_makes_feasible

is_feasible (p ^-¹)

Operation_interactions.thy

unsafe_compose_absorb

(p₁ ;p₂)/C = p₁/C ;p₂

unsafe_compose_absorb_2

(p₁ ;p₂)/C = p₁/C ;p₂

unsafe_compose_absorb_3

(p₁ ;p₂)/C ≡ p₁/C ;p₂

range_p_unsafe_composition

Range_p(a) ∩ C = {} ⟹ a ;b/(-C) ≡ a ;b

compose_absorb_1

(p₁ ; p₂)/C = p₁/C ; p₂

compose_absorb_2

(p₁ ; p₂)/C = p₁/C ; p₂

compose_absorb_3

(p₁ ; p₂)/C ≡ p₁/C ; p₂

range_p_composition

Range_p(a) ∩ C = {} ⟹ a ; b/(-C) ≡ a ; b

restrict_distrib_1

(p₁ ∪ p₂)/C = (p₁/C ∪ p₂/C)

restrict_distrib_2

(p₁ ∪ p₂)/C = (p₁/C ∪ p₂/C)

restrict_distrib_3

(p₁ ∪ p₂)/C ≡ (p₁/C ∪ p₂/C)

restrict_distrib_4

a ∪ (p₁ ∪ p₂)/C = a ∪ (p₁/C ∪ p₂/C)

restriction_absorbed_by_inverse_1

(p ^-¹)/C = ((p∖C) ^-¹)

restriction_absorbed_by_inverse_2

(p ^-¹)/C = (p∖C) ^-¹

restriction_absorbed_by_inverse_3

(p ^-¹)/C ≡ (p∖C) ^-¹

compose_distrib1_1

q ; (p₁∪p₂) = (q ; p₁) ∪ (q ; p₂)

compose_distrib1_2

q ; (p₁∪p₂) = (q ; p₁) ∪ (q ; p₂)

compose_distrib1_3

q ; (p₁∪p₂) ≡ (q ; p₁) ∪ (q ; p₂)

compose_distrib2_1

(p₁∪p₂) ; q = (p₁ ; q) ∪ (p₂ ; q)

compose_distrib2_2

(p₁∪p₂) ; q = (p₁ ; q) ∪ (p₂ ; q)

compose_distrib2_3

(p₁∪p₂) ; q ≡ (p₁ ; q) ∪ (p₂ ; q)

choice_distributes_over_composition

q∪(p₁ ; p₂) ≡ (q∪p₁) ; (q∪p₂)

corestriction_on_composition

p₁ ∖ s₁ ; p₂ = p₁ ; p₂ / s₁

corestrict_compose

(p₁ ; p₂) ∖ C = p₁ ; (p₂ ∖ C)

unsafe_gets_safe_1

(p₁ ;p₂) ; p₃ = (p₁ ; p₂) ; p₃

unsafe_gets_safe_2

(p₁ ;p₂) ; p₃ = (p₁ ; p₂) ; p₃

unsafe_gets_safe_3

(p₁ ;p₂) ; p₃ ≡ (p₁ ; p₂) ; p₃

unsafe_gets_safe_extended

((p₁ ;p₂) ;p₃) ; p₄ ≡ ((p₁ ; p₂) ; p₃) ; p₄

equivalency_of_compositions_1

(p₁∖Pre p₂) ;p₂ = p₁ ; p₂

equivalency_of_compositions_2

(p₁∖Pre p₂) ;p₂ = p₁ ; p₂

equivalency_of_compositions_3

(p₁∖Pre p₂) ;p₂ ≡ p₁ ; p₂

composition_inverse_1

(p ; q) ^-¹ = (q ^-¹) ; (p ^-¹)

composition_inverse_2

(p ; q) ^-¹ = (q ^-¹) ; (p ^-¹)

composition_inverse_3

(p ; q) ^-¹ ≡ (q ^-¹) ; (p ^-¹)

choice_inverse_1

(p ∪ q) ^-¹ = (p ^-¹) ∪ (q ^-¹)

choice_inverse_2

(p ∪ q) ^-¹ = (p ^-¹) ∪ (q ^-¹)

choice_inverse_3

(p ∪ q) ^-¹ ≡ (p ^-¹) ∪ (q ^-¹)

corestriction_restriction_on_unsafe_composition_1

p₁ ∖ s₁ ; p₂ ≡ p₁ ; p₂ / s₁

corestrict_gets_absorbed_by_unsafe_composition_1

(p₁ ; p₂) ∖ C ≡ (p₁ ∖ C) ; p₂

corestrict_gets_absorbed_by_unsafe_composition_2

(p₁ ; p₂) ∖ C ≡ p₁ ; (p₂ ∖ C)

corestriction_on_unsafe_composition

p₁ ∖ s ; p₂ = p₁ ; p₂ / s

corestrict_unsafe_compose

is_feasible p₁ ⟹ (p₁ ; p₂) ∖ C ≡ p₁ ; (p₂ ∖ C)

corestriction_absorbed_by_inverse_1

(p ^-¹)∖C = ((p/C) ^-¹)

corestriction_absorbed_by_inverse_2

(p ^-¹)∖C = ((p/C) ^-¹)

corestriction_absorbed_by_inverse_3

(p ^-¹)∖C ≡ (p/C) ^-¹

unsafe_composition_inverse_1

(p ;q) ^-¹ ≡ (q ^-¹) ;(p ^-¹)

corestrict_choice_1

(p₁ ∪ p₂) ∖ C = (p₁ ∖ C) ∪ (p₂ ∖ C)

corestrict_choice_2

(p₁ ∪ p₂) ∖ C = (p₁ ∖ C) ∪ (p₂ ∖ C)

corestrict_choice_3

(p₁ ∪ p₂) ∖ C ≡ (p₁ ∖ C) ∪ (p₂ ∖ C)

unsafe_compose_distrib1_3_1

q ;(p₁∪p₂) = (q ;p₁) ∪ (q ;p₂)

unsafe_compose_distrib1_3_2

q ;(p₁∪p₂) = (q ;p₁) ∪ (q ;p₂)

unsafe_compose_distrib1_3_3

q ;(p₁∪p₂) ≡ (q ;p₁) ∪ (q ;p₂)

unsafe_compose_distrib2_1

(p₁∪p₂) ;q = (p₁ ;q) ∪ (p₂ ;q)

unsafe_compose_distrib2_2

(p₁∪p₂) ;q = (p₁ ;q) ∪ (p₂ ;q)

unsafe_compose_distrib2_3

(p₁∪p₂) ;q ≡ (p₁ ;q) ∪ (p₂ ;q)

choice_distributes_over_composition_4

q∪(p₁ ;p₂) ≡ (q∪p₁) ; (q∪p₂)

until_simplification_1

a ; n∖C ∪ a ; m∖C ≡ a ; (n ∪ m)∖C

until_simplification_2

a ;n∖C ∪ a ;m∖C ≡ a ;(n ∪ m)∖C

Prime.thy

finite_Field_implies_finite_relation

finite (Field r) ⟹ finite r

finite (S p) ⟹ finite (Pre p)

finite_S_implies_finite_post

finite (S p) ⟹ finite (post p)

post_cardinality_equals_P_cardinality

P = {〈State={a,b}, Pre={a}, post={(a,b)}〉

a b. (a,b) ∈ (post p)} ⟹ card (post p) = card P

same_card_and_finite_impl_finite

card a = card b ⟹ finite a ⟹ card a > 0 ⟹ finite b

fst_in_state

is_feasible p ⟹ is_minimal p ⟹ P = {〈State={a,b}, Pre={a}, post={(a,b)}〉

a b. (a,b) ∈ post p} ⟹ r ∈ post p ⟹ fst r ∈ State p

snd_is_state

is_feasible p ⟹ is_minimal p ⟹ P = {〈State={a,b}, Pre={a}, post={(a,b)}〉

a b. (a,b) ∈ post p} ⟹ r ∈ post p ⟹ snd r ∈ State p

is_feasible p ⟹ is_minimal p ⟹ P = {〈State={a,b}, Pre={a}, post={(a,b)}〉 | a b. (a,b) ∈ post p} ⟹ s ∈ State p ⟹ ∃r ∈ post p. fst r = s ∨ snd r = s

choice_set_decomp_1

finite F ⟹ ⋃_P (insert x F) = ⋃_P F ∪ x

choice_set_decomp_1

⋃_P (insert x F) = ⋃_P F ∪ x

choice_set_equality

finite (S p) ⟹ is_feasible p ⟹ is_minimal p ⟹ P = {〈State={a,b}, Pre={a}, post={(a,b)}〉

a b. (a,b) ∈ post p} ⟹ p_i ∈ P ⟹ ⋃_P P = p

finite (S p) ⟹ is_feasible p ⟹ is_minimal p ⟹ P = {〈State={a,b},Pre={a},post={(a,b)}〉 |a b . (a,b) ∈ (post p)} ⟹ p_i ∈ P ⟹ is_prime p_i ∧ p_i ⊆ p ∧ ⋃_P P = p

finite (S p) ⟹ is_feasible p ⟹ is_minimal p ⟹ ∃ P. p_i ∈ P → is_prime p_i ∧ p_i ⊆ p ∧ ⋃_P P = p

Restriction.thy

restrict_prop_1

Pre (p / D) ⊆ D

restrict_prop_2

Pre (p / D) ⊆ Pre p

restrict_prop

Pre (p / D) ⊆ Pre p ∩ D

restrict_idem

(p / C) / C = p / C

restrict_inter

(p/C₁)/C₂ = p/(C₁ ∩ C₂)

restriction_equiv

f₁ ≡ p₁ ⟹ (f₁ / C) ≡ p₁ / C

equality_is_maintained_by_restriction

f₁ = p₁ ⟹ (f₁ / C) = p₁ / C

restrict_feasible

is_feasible p ⟹ is_feasible (p / C)

restrict_might_make_feasible

C ⊆ Domain (post p) ⟹ is_feasible (p / C)

restrict_refine_1

strengthens p (p / C)

restrict_refine_2

strengthens (p / C) p

restrict_refine_3

strengthens p q ⟹ strengthens (p / C) (q / C)

restrict_refine_4

weakens p (p / C)

restrict_refine_5

weakens p q ⟹ weakens (p / C) (q / C)

restrict_refine

p ⊑ p / C

restrict_refineorder1

D ⊆ C ⟹ p / C ⊑ p / D

restriction_refsafety

q ⊑ p ⟹ q / C ⊑ p / C

restriction_subsafety

q ⊆ p ⟹ q / C ⊆ p / C

restriction_refsafety2

q ⊑ p ⟹ D ⊆ C ⟹ q / C ⊑ p / D

implements_safety_restriction

implements a b ⟹ implements (a / C) (b / C)

restrict_subprogorder1

D ⊆ C ⟹ p / D ⊆ p / C

restrict_subprog

p / C ⊆ p

Unsafe_composition.thy

equivalence_is_maintained_by_unsafe_composition

f₁ ≡ p₁ ⟹ f₂ ≡ p₂ ⟹ f₁ ; f₂ ≡ p₁ ; p₂

equality_is_maintained_by_unsafe_composition

f₁ = p₁ ⟹ f₂ = p₂ ⟹ f₁ ; f₂ = p₁ ; p₂

unsafe_compose_feasible_1

is_feasible (p₁ ; p₂) ⟹ is_feasible p₁

unsafe_compose_feasible_2

all_feasible [p₁, p₂] ⟹ Range_p p₁ ⊆ Pre p₂ ⟹ is_feasible (p₁ ; p₂)

Unsafe_composition2.thy

Pre (p₁ ;^p (p₂ ;^p p₃)) ⊆ Pre ((p₁ ;^p p₂) ;^p p₃)

Pre ((p ;^p q) ;^p r) = Pre (p ;^p (q ;^p r))

equivalence_is_maintained_by_unsafe_composition

f₁ ≡ p₁ ⟹ f₂ ≡ p₂ ⟹ f₁ ;^p f₂ ≡ p₁ ;^p p₂

unsafe_compose_feasible_1

is_feasible (p₁ ;^p p₂) ⟹ is_feasible p₁

unsafe_compose_feasible_2

all_feasible [p₁, p₂] ⟹ Range_p p₁ ⊆ Pre p₂ ⟹ is_feasible (p₁ ;^p p₂)

Unsafe_composition3.thy

equivalence_is_maintained_by_unsafe_composition

f₁ ≡ p₁ ⟹ f₂ ≡ p₂ ⟹ f₁ ;_P f₂ ≡ p₁ ;_P p₂

equality_is_maintained_by_unsafe_composition

f₁ = p₁ ⟹ f₂ = p₂ ⟹ f₁ ;_P f₂ = p₁ ;_P p₂

unsafe_compose_feasible_1

is_feasible (p₁ ;_P p₂) ⟹ is_feasible p₁

unsafe_compose_feasible_2

all_feasible [p₁, p₂] ⟹ Range_p p₁ ⊆ Pre p₂ ⟹ is_feasible (p₁ ;_P p₂)

Boolean.thy

restrict_true

p / (TRUE (S p)) = p

restrict_false

p / (FALSE) ≡ Fail (S p)

cond_false_1

p / FALSE ≡ Fail (S p)

corestrict_true

is_feasible p ⟹ p ∖ (TRUE (S p)) ≡ p

corestrict_false

p ∖ FALSE = Fail (S p)

corestrict_false

p ∖ FALSE ≡ Infeas (Pre p)

if_true

ITE (TRUE (S p₁ ∪ S p₂)) p₁ p₂ ≡ p₁

if_false1

ITE (FALSE) p₁ p₂ ≡ p₂

true_selects_first_program_2

GC [(TRUE (S p₁ ∪ S p₂), p₁), (FALSE, p₂)] ≡ p₁

false_selects_second_program_2

GC [(FALSE, p₁), ((TRUE (S p₁ ∪ S p₂)), p₂)] ≡ p₂

restrict_false2

S p ⊆ S q ⟹ p / FALSE ∪ q = Fail {} ∪ q

implies_prop

(C →_s D) = UNIV ≡ (C ⊆ D)

and_prop

A ⊆ X ⟹ B ⊆ X ⟹ A ∧_s B = TRUE X ≡ A = X ∧ B = X

or_prop

TRUE X ⊆ (A ∨_s B) ≡ ∀x∈X. x ∈ A ∨ x ∈ B

Fail.thy

fail_is_valid

is_valid (Fail s)

fail_is_feasible

is_feasible (Fail s)

fail_is_total

is_total (Fail s)

fail_is_idempondent_composition

Fail C ; Fail C = Fail C

fail_is_idempondent_unsafe_composition

Fail C ; Fail C = Fail C

fail_equiv

Fail C ≡ Fail D

no_pre_is_fail

Pre p = {} ⟹ Fail s ≡ p

NOT_fail_choice_r

p ∪ Fail (S p) = p

fail_choice_r

p ∪ Fail C ≡ p

NOT_fail_choice_l

Fail (S p) ∪ p = p

fail_choice_l

Fail C ∪ p ≡ p

fail_compose_l_2

Fail (S p) ; p = Fail (S p)

fail_compose_l

Fail C ; p = Fail (C ∪ S p)

fail_compose_r_2

p ; Fail C = Fail (C ∪ S p)

fail_compose_r

p ; Fail C ≡ Fail C

only_fail_refines_fail

(p ⊑ Fail (S p)) = (p ≡ Fail (S p))

refine_fail

p ⊑ Fail (S p)

fail_refine_self

(Fail (S p) ⊑ p) = (p ≡ Fail (S p))

fail_specialize_self

(p ⊆ Fail (S p)) = (p ≡ Fail (S p))

range_of_fail

Range_p (Fail C) = {}

choice_fail_implication

(a ∪ b ≡ Fail {}) = (a ≡ Fail {} ∧ b ≡ Fail {})

fail_refine

C ⊆ S p ⟹ p ⊑ Fail C

C ⊆ S p ⟹ Fail C ⊆ p

fail_specialize2

p ⊆ Fail (S p) ≡ p ≡ Fail {}

fail_refine2

Fail (S p) ⊑ p ≡ p ≡ Fail {}

compose_empty_1

S a = {} ⟹ b ; a = Fail (S b)

compose_empty_2

S a = {} ⟹ a ; b = Fail (S b)

fail_union_1

C ⊆ S p ⟹ Fail C ∪ (p ∪ q) = (p ∪ q)

fail_compose

Fail (S p) ; p = Fail (S p)

fail_union_2

C ⊆ S a ⟹ a ∪ Fail C = a ∪ Fail {}

fail_choice_decomp

p ∪ q ≡ Fail {} ≡ p ≡ Fail {} ∧ q ≡ Fail {}

fail_specialize

C ⊆ S p ⟹ Fail C ⊆ p

fail_specialize3

Fail {} ⊆ p

Havoc.thy

havoc_is_valid

is_valid (Havoc s)

havoc_is_feasible

is_feasible (Havoc s)

havoc_is_total

is_total (Havoc s)

havoc_is_idempondent_composition

Havoc C ; Havoc C = Havoc C

havoc_is_idempondent_unsafe_composition

Havoc C ; Havoc C = Havoc C

havoc_choice_l

S p ⊆ C ⟹ Havoc C ∪ p = Havoc C

havoc_choice_r

S p ⊆ C ⟹ p ∪ Havoc C = Havoc C

havoc_pre_State

State (p ; Havoc (S p)) = State (Havoc (S p) / Pre p)

havoc_pre_S

S p ⊆ C ⟹ S (p ; Havoc C) = S (Havoc C / Pre p)

NOT_havoc_pre_Pre

Pre (p ; Havoc (S p)) = Pre (Havoc (S p) / Pre p)

havoc_pre_Pre

S p ⊆ C ⟹is_feasible p ⟹ Pre (p ; Havoc C) = Pre (Havoc C / Pre p)

NOT_havoc_pre_post_1

post (p ; Havoc (S p)) = post (Havoc (S p) / Pre p)

NOT_havoc_pre_post_1

is_feasible p ⟹ post (p ; Havoc (S p)) = post (Havoc (S p) / Pre p)

havoc_pre_post

S p ⊆ C ⟹is_feasible p ⟹ restr_post (p ; Havoc C)/ Pre p = restr_post (Havoc C / Pre p)

NOT_havoc_pre

p ; Havoc (S p) ≡ Havoc (S p) / Pre p

havoc_pre

S p ⊆ C ⟹is_feasible p ⟹ (p ; Havoc C) ≡ Havoc C / Pre p

havoc_pre_unsafe

S p ⊆ C ⟹ (p ; Havoc C) ≡ Havoc C / Pre p

havoc_co_restricted

(Havoc C / D) ∖ D ≡ Havoc (C ∩ D)

havoc_from_left_S

S p ⊆ C ⟹ is_feasible p ⟹ S (Havoc C ; p) = S(Havoc C ∖ Range_p (p))

havoc_from_left_Pre

S p ⊆ C ⟹ is_feasible p ⟹ ¬ p ≡ Fail C ⟹ Pre (Havoc C ; p) = C

havoc_from_left_post

S p ⊆ C ⟹ is_feasible p ⟹ post (Havoc C ; p) = post (Havoc C ∖ Range_p (p))

havoc_from_left

S p ⊆ C ⟹ is_feasible p ⟹ ¬ p ≡ Fail C ⟹ Havoc C ; p ≡ Havoc C ∖ Range_p p

refine_havoc

p ⊑ Havoc (S p) / Pre p

specialize_havoc

p ⊆ Havoc (S p) / Pre p

refine_havoc2

is_total p ⟹ p ⊑ Havoc (S p)

specialize_havoc2

S p ⊆ C ⟹ p ⊆ Havoc (C)

Infeas.thy

infeas_is_valid

is_valid (Infeas s)

infeas_is_feasible

is_feasible (Infeas s)

infeas_is_total

is_total (Infeas s)

infeas_is_idempondent_composition

Infeas C ; Infeas C = Infeas C

infeas_is_idempondent_unsafe_composition

Infeas C ; Infeas C = Infeas C

fail_equiv

Infeas C ≡ Infeas D

not_total_infeas_makes_infeasible

¬ is_total p ⟹ ¬ is_feasible (p ∪ Infeas (S p))

infeas_makes_total

is_total (p ∪ Infeas (S p))

infeas_to_smaller_self

p ; Infeas (S p) ≡ Infeas (Pre p ∩ Domain (post p))

infeas_composition

Infeas (S p) ; p = Fail (S p)

infeas_unsafe_composition_1

Infeas (S p) ; p = Infeas (S p)

infeas_unsafe_composition_2

p ; Infeas (S p) ≡ Infeas (Pre p)

infeas_restriction

Infeas (C) / D ≡ Infeas (C ∩ D)

infeas_corestriction

Infeas (C) ∖ D = Fail (C)

infeas_corestriction2

Infeas (C) ∖ D = Infeas (C)

Skip.thy

skip_is_valid

is_valid (Skip s)

skip_is_feasible

is_feasible (Skip s)

skip_is_total

is_total (Skip s)

skip_is_idempondent_composition

Skip C ; Skip C = Skip C

skip_is_idempondent_unsafe_composition

Skip C ; Skip C = Skip C

skip_unsafe_compose_r_1

p ; Skip (S p) = p

skip_compose_r_post

post (p ; Skip (S p)) = post p

skip_compose_r_Pre_1

Pre (p ; Skip (S p)) = (Pre p ∩ Domain (post p))

skip_compose_r_S

S (p ; Skip (S p)) = S p

Skip_compleft

is_feasible p ⟹ p ; Skip (S p) = p

is_feasible p ⟹ Skip (S p) ; p = p

skip_compose2

is_feasible p ⟹ p ; Skip (S p) ≡ p

skip_compose_r_range2

is_feasible p ⟹ p ; Skip (Range (post p)) = p

skip_compose_r_range

is_feasible p ⟹ p ; Skip (Range_p p) ≡ p

skip_compose4

is_feasible p ⟹ Skip (Pre p) ; p ≡ p

skip_compose_r_3

p ; Skip (S p) ≡ p / Domain (post p)

skip_makes_feasible

is_feasible (p ; Skip (S p))

skip_compose_l_S

S (Skip (S p) ; p) = S p

skip_compose_l_Pre

Pre (Skip (S p) ; p) = Pre p

skip_compose_l_post

post (Skip (S p) ; p) = post p / Pre p

skip_compose_l_1

Skip (S p) ; p = 〈 State = S p, Pre = Pre p, post = post p / Pre p〉

skip_compose3

Skip (S p) ; p ≡ p

skip_unsafe_compose_r_2

Skip (S p) ; p = 〈State=S p, Pre=S p, post = restr_post p 〉

corestriction_prop

p ∖ C ≡ p ; (Skip (S p) / C)

skip_prop

Skip C ∪ Skip D ≡ Skip (C ∪ D)

skip_prop_2

Skip (S p) / C ; p ≡ p / C

Skip (C) ; p = p / C

Skip_comprestrict

Skip (C) ; p ≡ p / C

skip_prop_4

Skip D / C ≡ Skip (D ∩ C)

skip_prop_5

C ⊆ D ⟹ Skip D / C ≡ Skip C

skip_prop_6

S p ⊆ C ⟹ Skip C ; p ≡ p

corestrict_skip

p ; Skip (C) ≡ p ∖ C

skip_prop_8

Skip D ∖ C ≡ Skip (D ∩ C)

skip_prop_9

S (Skip (C)) = C

skip_prop_10

Skip x ∪ Skip y = Skip (x ∪ y)

skip_prop_11

Skip {} ∪ p ≡ p

skip_prop_12

Skip {} ∪ (p ∪ q) = p ∪ q

skip_prop_13

(a ; Skip (S a ∪ S b) ) ; b = a ; b

skip_prop_14

(a ; Skip (S a) ) ; b = a ; b

skip_prop_15

(a ; Skip (S b) ) ; b = a ; b

skip_prop_16

S a ⊆ C ⟹ post ((a ; Skip C) ; b) = post (a ; b)

skip_prop_17

S b ⊆ C ⟹ post ((a ; Skip C) ; b) = post (a ; b)

skip_prop_18

S a ⊆ C ⟹ Skip C ; (a ; Skip C) = (Skip (S a) ; a) ; Skip C

Arbitrary_repetition.thy

loop_l1

s=0 ⟹ f=0 ⟹ loop p s f = Skip (S p) / (Pre p)

loop_l2

s=0 ⟹ f=1 ⟹ loop p s f = Skip (S p) / (Pre p) ∪ (Skip (S p) / (Pre p) ; p)

loop_l2_01

loop p (f + 1) f = Fail (S p)

loop_l2_02

loop p 0 f ; p = loop p (0 + 1) (f + 1)

loop_l2_03

loop p s s ; p = loop p (s + 1) (s + 1)

loop_l2_04

s<f ⟹ loop p s f ; p = loop p (s + 1) (f + 1)

loop_l2_05

0<s ⟹ loop p s s = p^s ∪ Fail {}

loop_l2_1

s=f ⟹ loop p s f ≡ p^s

loop_l2_2

loop p s (s + 1) = p^s ∪ p^{s + 1}

loop_l3

s<f ⟹ loop p s (f + 1) ≡ (p^{f + 1}) ∪ (loop p s f)

loop_l4

s<f ⟹ loop p s f ≡ (p^s) ∪ (loop p (s + 1) f)

loop_l6

s=0 ⟹ s<f ⟹ loop p s f ≡ (Skip (S p) / (Pre p)) ∪ (loop p 1 f)

0<s ⟹ s<f ⟹ loop p s f ≡ p^s ∪ loop p (s + 1) f

loop_l5

s<f ⟹ s < k ⟹ k < f ⟹ loop p s f ≡ (loop p s k) ∪ (loop p (k + 1) f)

loop_simplification

all_feasible [x,y] ⟹ Range_p x ∩ Pre y = {} ⟹ Range_p y ∩ Pre x = {} ⟹ (loop x s f) ∪ (loop y s f) ≡ loop (x ∪ y) s f

equiv_is_maintained_by_arbitrary_repetition_1

all_feasible [p₁, p₂] ⟹ p₁ ≡ p₂ ⟹ S p₁ = S p₂ ⟹ loop p₁ s f ≡ loop p₂ s f

equiv_is_maintained_by_arbitrary_repetition_2

all_feasible [p₁, p₂] ⟹ p₁ ≡ p₂ ⟹ 0<s ⟹ loop p₁ s f ≡ loop p₂ s f

arbitrary_rep_feasibility_l1

s > f ⟹ is_feasible p ⟹ is_feasible (loop p s f)

arbitrary_rep_feasibility_l2

s < f ⟹ is_feasible p ⟹ is_feasible (loop p s f)

arbitrary_rep_feasibility

is_feasible p ⟹ is_feasible (loop p s f)

skip_compose_l_of_loop_1

s < f ⟹ s=0 ⟹ loop p s f ≡ Skip (S p) / (Pre p) ∪ loop p s f

skip_compose_r_of_loop_2

is_feasible p ⟹ loop p s f ≡ loop p s f ; Skip (S p)

skip_compose_l_of_loop_3

is_feasible p ⟹ loop p s f ≡ Skip (S p) ; loop p s f

range_fixed_rep

s<m ⟹ m<f ⟹ x ∉ Range_p (loop p s f) ⟹ x ∉ Range_p (p^m)

pre_is_known_arbitrary_rep_1

∀x y. x ∈ Pre a ∧ (x, y) ∈ post (a ; (b / (- C))ⁿ) → x ∈ Pre (a ; (b / (- C))ⁿ)

pre_is_known_arbitrary_rep_2

x ∈ Pre a ⟹ (x, y) ∈ post (a ; (b / (- C))ⁿ) ⟹ x ∈ Pre (a ; (b / (- C))ⁿ)

bad_index_is_fail_arbitrary

f<s ⟹ loop a s f ≡ Fail {}

fail_stays_fail_arbitrary

s<f ⟹ loop p s f ≡ Fail {} ⟹ loop p s (f + 1) ≡ Fail {}

fail_stays_fail_arbitrary_2

s<f ⟹ loop p s (f + 1) ≡ Fail {} ⟹ loop p s f ≡ Fail {}

fail_stays_fail_arbitrary_3

s<f ⟹ loop p s (f + 1) ≡ Fail {} ≡ loop p s f ≡ Fail {}

fail_stays_fail_arbitrary_4

s<f ⟹ loop p s s ≡ Fail {} ≡ loop p s f ≡ Fail {}

fail_arbitrary_implies_fixed

k < n ⟹ loop (b / (- C)) 0 n ≡ Fail {} ⟹ (b / (- C)) ^{«/sup>/a> k}≡ Fail {}

extract_fixed_from_arbitrary

k<n ⟹ a ; loop (b / (- C)) 0 n ∖ C ≡ a ; loop (b / (- C)) 0 n ∖ C ∪ a ; ((b / (- C)) ^{«/sup>/a> k)}∖ C

fail_arbitrary_implies_fixed_2

k < n ⟹ a ; loop (b / (- C)) 0 n ∖ C ≡ Fail {} ⟹ a ; ((b / (- C)) ^{«/sup>/a> k)}∖ C ≡ Fail {}

Fail (S x) ∪ x ^{«/sup>/a> 0 = x}^{«/sup>/a> 0}

fixed_prop

0<f ⟹ Fail (S x) ∪ x ^{«/sup>/a> f = x}^{«/sup>/a> f}

loop_choice3

0<s ⟹ 0<f ⟹ all_feasible [x,y] ⟹ Range_p x ∩ Pre y = {} ⟹ Range_p y ∩ Pre x = {} ⟹ (loop x s f) ∪ (loop y s f) = loop (x ∪ y) s f

Loop_fail

loop p 0 n ≡ Fail {} ⟹ loop p 0 m ≡ Fail{}

Atomic_concurrency.thy

foldl (f::’a Program ⇒ ‘a Program ⇒ ‘a Program) (f a x) xs = f a (foldl f x xs)

complete_state_subset_fold_composition

x ∈ complete_state xs ⟹ x ∈ S (foldl (;) (Skip (complete_state xs)) xs)

fold_choice_inv_1

foldl (∪) (Fail {}) (a # xs) = a ∪ foldl (∪) (Fail {}) (xs)

fold_choice_inv_2

S (foldl (∪) (Fail {}) xs ) = ⋃ (set (map (S) xs))

conc_elems_state

x ∈ set (conc_elems xs) ⟹ S x = complete_state xs

atomic_conc_complete_state

S (atomic_conc xs) = complete_state xs

atomic_conc_equivalence

xs ≠ [ ] ⟹ S (Concat xs C) = S (atomic_conc xs)

pre_zero

Pre (atomic_conc [ ]) = {}

pre_one

is_feasible x ⟹ Pre (atomic_conc [x]) = Pre x

lemma_pre_1

Pre (atomic_conc (a#[b])) ⊆ Pre a ∪ Pre b

list_equiv_reflexive

list_equiv xs xs

list_equiv_comp_equiv

list_equiv xs ys ⟹ b ≡ b’ ⟹ fold (;) xs b ≡ fold (;) ys b’

skip_prop_1

is_feasible a ⟹ S a ⊆ C ⟹ a ; Skip C ≡ a

skip_prop_2

is_feasible a ⟹a ; Skip (complete_state (a # xs)) ≡ a

skip_restrict

is_feasible a ⟹ fold (;) xs (a ; Skip (complete_state (a # xs))) ≡ fold (;) xs a

feas_of_prop

is_feasible (feas_of p)

feas_of_prop2

is_feasible p ⟹ feas_of p = p

skip_prop_4

a ; Skip (S a) ≡ feas_of a

skip_prop_5

fold (;) xs (Skip (complete_state (a # xs)) ; a) ≡ fold (;) xs a

get_trace

xs ≠ [ ] ⟹ x ∈ set (conc_elems xs) ⟹ ∃tr. tr ∈ set (permutations xs) ∧ x = Concat tr C

skip_prop_6

Skip (S p ∪ x) ; p ≡ Skip (S p) ; p

no_right_neutral

∃t. p ; t ≡ p

corestrict_skip

(a ; Skip (S a ∪ S b)) ; b ≡ a ; b

skip_prop_8

(a ; Skip (S a)) ; b ≡ a ; b

skip_prop_9

(a ; Skip (S b)) ; b ≡ a ; b

fold_decomp

xs ≠ [ ] ⟹ (foldl (;) (a) (xs)) ≡ a ; (foldl (;) (Skip (complete_state xs)) (xs))

fold_decomp2

xs ≠ [ ] ⟹ (foldl (;) (a) (xs)) ≡ a ; (foldl (;) (Skip (S a)) (xs))

fold_equiv_maintained

a ≡ b ⟹ foldl (;) a xs ≡ foldl (;) b xs

fold_compress_1

ys ≠ [ ] ⟹ ∃e’. (a) ; e’ ≡ (foldl (;) (Skip (complete_state ([a]@ys))) ([a]@ys))

fold_compress_2

∃e’. e’ ; a ≡ (foldl (;) (Skip (complete_state (ys@[a]))) (ys@[a]))

fold_compress_3

∃s’ e’. (s’ ; a) ; e’ ≡ (foldl (;) (Skip (complete_state (xs@[a]@ys))) (xs@[a]@ys)) ∨ s’ ; a=(foldl (;) (Skip (complete_state (xs@[a]@ys))) (xs@[a]@ys))

conc_elems_dec

x ∈ set (conc_elems (a # xs)) ⟹ ∃s’ e’. (s’ ; a) ; e’ = x ∨ s’ ; a=x ∨ a = x∨ a ; e’ = x

concat_prop_1

xs ≠ [ ] ⟹ tr ∈ set (permutations xs) ⟹ Concat tr (complete_state xs) ∈ set (conc_elems xs)

fold_choice_inv

t ∈ set (xs) ⟹ foldl (∪) (x) (xs) = t ∪ (foldl (∪) (x) (xs))

atomic_conc_inv

tr ∈ set (conc_elems xs) ⟹ tr ∪ atomic_conc xs ≡ atomic_conc xs

atomic_conc_inv2

x ∈ set (conc_elems xs) ⟹ x ⊆ atomic_conc xs

atomic_conc_inv3

xs ≠ [ ] ⟹ Concat xs (complete_state xs) ⊆ atomic_conc xs

perm_prop

set (permutations (a@b)) = set (permutations (b@a))

perm_prop2

x ∈ set (permutations y) ⟹ set (conc_elems (y)) = set (conc_elems (x))

perm_prop3

set (conc_elems (a@b)) = set (conc_elems (b@a))

perm_prop4

size (insert_all x xs) = size xs + 1

perm_prop5

size (concat [ ]) = 0

perm_prop6

size (concat (x#xs)) = size x + size (concat (xs))

perm_prop7

size (concat xs) = foldl (λa b. a + (size b)) 0 xs

perm_prop8

a ∈ set (map (insert_all x) (permutations xs)) ⟹ b ∈ set a ⟹ size b = size xs + 1

perm_prop9

a ∈ set (map (insert_all x) (permutations xs)) ⟹ size a = size xs + 1

size_concat

size (concat xss) = sum_list (map size xss)

insert_all_prop

size (concat (map (insert_all x) xss)) = sum_list (map (λy. Suc (size y)) xss)

x ∈ set (permutations xs) ⟹ y ∈ set (permutations xs) ⟹ size x = size y

sum_list_simp

(∀x ∈ set xss. ∀ y ∈ set xss. size x = size y) ⟹ sum_list (map size xss) = size xss * size (hd xss)

size_lemma

∀x ∈ set xs. size x = n ⟹ size (concat xs) = size xs * n

length_concat_insert_all

length (concat (map (insert_all x) (permutations xs))) = (length xs + 1) * length (permutations xs)

size_permutations_fact

length (permutations xs) = fact (length xs)

perm_size_eq

size xs = size ys ⟹ size (permutations xs) = size (permutations ys)

perm_prop10

size (permutations (x#xs)) = size (permutations (xs)) * size (x#xs)

fold_choice_prop1

permutations a = permutations b ⟹ set (conc_elems a) = set (conc_elems b)

size xs > 0⟹ size (conc_elems xs) > 0

fold_choice_prop2

a ∈ set xs ⟹ foldl (∪) a xs = foldl (∪) (Skip {}) xs

fold_choice_prop3

a ∈ set (conc_elems (xs)) ⟹ foldl (∪) (a) (conc_elems (xs)) = foldl (∪) (Skip {}) (conc_elems (xs))

fold_choice_prop5

foldl (∪) x (x’#xs) = foldl (∪) (Fail {}) (x#x’#xs)

atomic_prop2

xs ≠ [ ] ⟹ ys ∈ set (permutations xs) ⟹ Concat ys (complete_state xs) ⊆ atomic_conc xs

atomic_prop3

atomic_conc [a,b] ≡ a ; b ∪ b ; a

equiv_to_equal

S a = S b ⟹ post a = post b ⟹ a ≡ b ⟹ a = b

atomic_prop4

atomic_conc [a, b ∪ c] ≡ atomic_conc [a,b] ∪ atomic_conc [a,c]

atomic_prop5

atomic_conc [a ∪ b] = atomic_conc [a] ∪ atomic_conc [b]

set_to_list_set

finite xs ⟹ set (set_to_list xs) = xs

specialize_prop

a = b ⟹ b ⊆ a ∧ a ⊆ b

atomic_prop6

atomic_conc [a ∪ b, c] ≡ atomic_conc [a,c] ∪ atomic_conc [b,c]

commute_compose

commute_programs3 a b ⟹ atomic_conc [a,b] ≡ a ; b

Big_choice.thy

fold_compose

foldl (;) (a ; b) xs = a ; (foldl (;) b xs)

fold_choice

foldl (∪) (a ∪ b) xs = a ∪ (foldl (∪) b xs)

Choice_prop_1_2

xs ≠ [ ] ⟹ ⋃ (x#xs) = x ∪ ⋃ xs

Choice_prop_1_3

a@b ≠ [ ] ⟹ ⋃ (a@x#b) = x ∪ ⋃ (a@b)

Choice_prop_1_1

ys ∈ set (permutations xs) ⟹ ⋃ xs = ⋃ ys

Choice_prop_1

xs ≠ [ ] ⟹ ⋃ (xs@[x]) = x ∪ ⋃ xs

Choice_prop_1_4

xs ≠ [ ] ⟹ foldl (∪) x xs = x ∪ Choice xs

Choice_prop_2

⋃ [a ; t. t ← xs] ≡ a ;⋃ [t. t ← xs]

Choice_prop_3

xs ≠ [ ] ⟹ ⋃ (xs@[x]) = ⋃ (xs) ∪ x

Choice_prop_4

⋃ [t ; a. t ← xs] ≡ ⋃ [t. t ← xs] ; a

Choice_state

S (⋃ (xs)) = ⋃ {S x

x . x ∈ set xs}

Union_prop_1

xs ≠ {} ⟹ ⋃ {t

x . x ∈ xs} = t

Choice_prop_5

size xs = 1 ⟹ set (xs) = {x} ⟹ (⋃ xs = x)

Choice_prop_6

size xs > 1 ⟹ set (xs) = {x} ⟹ (⋃ xs = x ∪ x)

Choice_prop_7

a ≠ [ ] ⟹ b ≠ [ ] ⟹ ⋃ a ∪ ⋃ b = ⋃ (a@b)

Choice_prop_8

∃x ∈ set xs. p x ⟹ ∃x ∈ set xs. ¬ p x ⟹ ⋃ (filter (λx. p x) xs) ∪ ⋃ (filter (λx. ¬ p x) xs) = ⋃ xs

Choice_prop_9

size xs>1 ⟹ size ys>1 ⟹ set xs = set ys ⟹ ⋃ (xs) = ⋃ (ys)

Choice_prop_10

size xs=1 ⟹ size ys=1 ⟹ set xs = set ys ⟹ ⋃ (xs) = ⋃ (ys)

Choice_prop11

size xs > 1 ⟹ ⋃ (filter (λt. P t) xs) ∪ ⋃ (filter (λt. ¬ P t) xs) = ⋃ xs

Choice_prop12

x ∈ set xs ⟹ ⋃ (filter ((=) x) (x#xs)) = x ∪ x

Choice_state_1

complete_state xs = S (Choice xs)

Concat_prop_1

xs ≠ [ ] ⟹ foldl (;) x xs = x ; Concat xs s

Concat_state

xs ≠ [ ] ⟹ complete_state xs = S (Concat xs s)

Choice_prop_13

size xs > 0 ⟹ ⋃ [a ; (Concat t s). t ← xs] ≡ a ;⋃ [(Concat t s). t ← xs]

Choice_prop_14

⋃ [t / C . t ← xs] ≡ ⋃ [t . t ← xs]/ C

⋃ [t / C . t ← xs] = ⋃ [t . t ← xs]/ C

Choice_prop_15

⋃ [t ∖ C . t ← xs] = ⋃ [t . t ← xs]∖ C

Concat_prop_2

xs ≠ [ ] ⟹ Concat (xs@[x]) s = Concat xs s ; x

Concat_prop_3

xs ≠ [ ] ⟹ Concat xs s / C ≡ Concat (hd xs / C # tl xs) s

Concat_prop_4

xs ≠ [ ] ⟹ Concat xs s ∖ C ≡ Concat (butlast xs @ [(last xs)∖ C]) s

Choice_prop_16

x ∈ set xs ⟹ ⋃ xs ≡ ⋃ xs ∪ x

Choice_prop_17

size xs > 1 ⟹ x ∈ set xs ⟹ ⋃ xs = ⋃ xs ∪ x

Concat_prop_5

xs ≠ [ ] ⟹ ys ≠ [ ] ⟹ Concat (xs@ys) s = Concat xs s ; Concat ys s

Concat_prop_6

Concat (a ∪ b # xs) s = Concat (a # xs) s ∪ Concat (b # xs) s

Concat_prop_7

Concat (xs@[a ∪ b]) s ≡ Concat (xs@[a]) s ∪ Concat (xs@[b]) s

Concat_prop_8

e ≠ [ ] ⟹ Concat (s@(a ∪ b)#e) s’ ≡ Concat (s@a#e) s’ ∪ Concat (s@b#e) s’

Choice_prop_18

size b > 1 ⟹ ⋃ b = ⋃ b ∪ Fail {}

Choice_prop_19

size (a@b) > 1 ⟹ ⋃ a ∪ ⋃ b = ⋃ (a@b)

Choice_prop_20

size (a@b) > 0 ⟹ ⋃ a ∪ (x ∪ ⋃ b) = ⋃ (a@x#b)

Choice_prop_21

S x ⊆ complete_state (a@b) ⟹ ⋃ a ∪ (x / FALSE ∪ ⋃ b) = ⋃ a ∪ (Fail {} ∪ ⋃ b)

list_prop

1 < i ⟹ i < n ⟹ [p . t ← [1 .. int n]] = [p . t ← [1 .. int i]] @ [p . t ← [int (i + 1) .. int n]]

list_prop2

[p . t ← [1 .. int (n + 1)]] = [p . t ← [1 .. int n]]@[p]

list_prop3

size x = size y ⟹ [p. t ← x] = [p. t ← y]

list_prop4

[p . t ← [1 .. int (n + 1)]] = p#[p . t ← [1 .. int n]]

Concat_prop_9

0<n ⟹ Concat [p . t ← [1 .. int n]] s ; p = Concat [p . t ← [1 .. int (n + 1)]] s

Concat_prop_10

xs ≠ [ ] ⟹ Concat (x#xs) s = x ; Concat xs s

Concat_prop_11

0<n ⟹ p ; Concat [p . t ← [1 .. int n]] s = Concat [p . t ← [1 .. int (n + 1)]] s

Choice_prop_22

a ∪ ⋃ (x#xs) = a ∪ (x ∪ ⋃ xs)

Choice_prop_23

∀x ∈ set xs. x = y ⟹ ⋃ xs = Fail {} ∨ ⋃ xs = y ∨ ⋃ xs = y ∪ y

Choice_prop_24

distinct xs ⟹ distinct ys ⟹ set xs = set ys ⟹ size xs = size ys ⟹ ⋃ xs = ⋃ ys

atomic_prop_1

finite F ⟹ ∀x ∈ F. is_atomic x ⟹ get_atomic (⋃ (set_to_list F)) = F

decomp_programs

Pre a = Pre p - {y} ⟹ post b = {t. t ∈ post p ∧ (fst t=y ∨ snd t=y)} ⟹ Pre b = Pre p ∩ ({y} ∪ Domain (post p ∖ {y})) ⟹ post a = {t. t ∈ post p ∧ (fst t ≠ y ∧ snd t ≠ y)} ⟹ a ∪ b ≡ p

is_feasible p ⟹ finite (S p) ⟹ ∃xs. ⋃ xs ≡ p ∧ (∀x ∈ set xs. is_atomic x)

civilized_finite

civilized_n x B n ⟹ finite B

civilized_ind

civilized_n x B n ⟹ civilized_n x B (n + 1)

civilized_ind2

⋀m. n<m ⟹ civilized_n x B n ⟹ civilized_n x B m

civilized_generic

civilized_n x B n = ((∃a b m m’. m<n ∧ m’<n ∧ civilized_n a B m ∧ civilized_n b B m’ ∧ (a ; b = x ∨ a ∪ b = x)) ∧ finite B) ∨ civilized_n x B 0

civ_prop_1

civilized_n p B n ⟹ civilized p B

civ_prop_2

civilized p B ⟹ civilized q B ⟹ civilized (p ; q) B

civ_prop_3

civilized p B ⟹ civilized q B ⟹ civilized (p ∪ q) B

fold_prop

foldl (∪) {} xs = {} ⟹ t ∈ set xs ⟹ t = {}

fold_prop2

x ∈ tr ⟹ tr ∈ set xs ⟹ foldl (∪) {} xs ⊆ B ⟹ x ∈ B

normal_prop1

set x ⊆ {p} ⟹ ∃n. x = replicate n p

basic_normal

basic a = basic b ⟹ normal_of a B = normal_of b B

basic_normal2

basic a = insert (Fail {}) (basic b) ⟹ normal_of a B = normal_of b B

normal_prop2

finite B ⟹ normal_of [[ ]] B

normal_prop3

finite B ⟹ normal_of [[〈State = {}, Pre = {}, post = {}〉]] B

normal_prop4

infinite B ⟹ ¬ normal_of xs B

normal_prop5

finite B ⟹ normal_of xs B ⟹ normal_of ([ ]#xs) B

normal_prop6

finite B ⟹ normal_of ([ ]#xs) B ⟹ normal_of xs B

normal_prop7

normal_of [x#xs] B = (normal_of [[x]] B ∧ normal_of [xs] B)

basic_prop0

basic [[x]] ∪ basic [xs] = basic [x#xs]

basic_prop1

basic [x] ∪ basic xs = basic (x#xs)

basic_prop2

basic xs ∪ basic ys = basic (xs@ys)

normal_prop8

trace ∈ set xs ⟹ normal_of xs B ⟹ normal_of [trace] B

normal_prop9

normal_of ((a # x) # xs) B ⟹ normal_of [[a]] B

basic_prop3

trace ∈ set xs ⟹ basic [trace] ⊆ basic xs

basic_prop4

x ∈ set trace ⟹ basic [[x]] ⊆ basic [trace]

normal_prop10

x ∈ set trace ⟹ trace ∈ set xs ⟹ normal_of xs B ⟹ normal_of [[x]] B

normal_prop11

normal_of ((a#x)#xs) B = (normal_of [[a]] B ∧ normal_of (x#xs) B)

normal_prop12

normal_of (x#xs) B = (normal_of [x] B ∧ normal_of xs B)

normal_prop13

normal_of (a#p) B = normal_of ((〈State = {}, Pre = {}, post = {}〉#Skip (complete_state (set_to_list B))#a)#p) B

fold_prop1

trace ∈ set p ⟹ x ∈ set trace ⟹ x ∈ foldl (∪) {} (map set p)

normal_prop14

normal_of p B ⟹ trace ∈ set p ⟹ x ∈ set trace ⟹ x ∈ {Fail {}, Skip (complete_state (set_to_list B))} ∪ B

basic_monotone1

basic a ⊆ basic (x#a)

basic_monotone2

x ∈ set p ⟹ basic [x] ⊆ basic p

basic_decomp1

basic [x] ∪ basic xs = basic (x#xs)

basic_decomp2

basic [x] ∪ basic xs = basic (xs@[x])

fold_prop3

foldl (∪) (foldl (∪) {} xs) ys = foldl (∪) {} xs ∪ foldl (∪) {} ys

basic_decomp

basic a ∪ basic b = basic (a@b)

basic_monotone

set a ⊆ set b ⟹ basic a ⊆ basic b

basic_prop

basic (a@b) ⊆ B ⟹ basic b ⊆ B

basic_prop5

basic (a@b) ⊆ B ⟹ basic a ⊆ B

basic_monotone3

basic [a] ⊆ basic [a@b]

basic_monotone4

basic [b] ⊆ basic [a@b]

basic_monotone5

basic [b] ∪ basic [a] = basic [a@b]

civilized_empty2

finite B ⟹ civilized_n (⋃ [ ]) B 0

civilized_empty3

finite B ⟹ civilized_n (Fail {}) B 0

civilized_empty4

finite B ⟹ civilized_n (Skip {}) B 0

normal_civilized

normal_of p B ⟹ civilized (evaluate p (complete_state (set_to_list B))) B

concat_prop1

evaluate ([ ] ; b) c = Fail {}

concat_prop2

evaluate [ ] c = Fail {}

concat_prop3

xs ≠ [ ] ⟹ evaluate (x#xs) c = evaluate [x] c ∪ evaluate xs c

concat_prop4

complete_cnf_state (x#xs) ⊆ c ⟹ xs ≠ [ ] ⟹ evaluate (x#xs) c = evaluate [x] c ∪ evaluate xs c

concat_prop4_1

evaluate (x#xs) c ≡ evaluate [x] c ∪ evaluate xs c

fail_compose

Fail {} ; p ≡ Fail {}

concat_prop5

evaluate (a@b) c ≡ evaluate a c ∪ evaluate b c

Skip_concat

Skip (complete_state a) ; Concat a (complete_state a) ≡ Concat a (complete_state a)

concat_prop

a ≠ [ ] ⟹ Concat a (insert x (complete_state a)) ≡ Concat a (complete_state a)

state_prop1

S (evaluate xs C) ∪ S (evaluate [x] C) = S (evaluate (x#xs) C)

state_prop2

S (evaluate xs C) ∪ S (evaluate ys C) = S (evaluate (ys@xs) C)

eval_prop

[ ] ∉ set xs ⟹ evaluate xs C = evaluate xs D

state_prop3

[ ] ∈ set xs ⟹ complete_cnf_state (xs) ⊆ S (evaluate (xs) (complete_cnf_state (xx#xs)))

state_prop4

[ ] ∉ set xs ⟹ complete_cnf_state (xs) ⊆ S (evaluate (xs) (complete_cnf_state (xx#xs)))

state_prop5

complete_cnf_state (xs) ⊆ S (evaluate (xs) (complete_cnf_state (xx#xs)))

state_prop6

S (evaluate xs (complete_cnf_state xs)) = complete_cnf_state xs

skip_prop2

Skip (complete_cnf_state xs) ; evaluate (xs) (complete_cnf_state xs) ≡ evaluate (xs) (complete_cnf_state xs)

concat_prop6

evaluate ([ ]#xs) (complete_cnf_state xs) ≡ Skip (complete_cnf_state xs) ∪ evaluate xs (complete_cnf_state xs)

non_empty0

non_empty (non_empty xs) = non_empty xs

non_empty1

non_empty [ ] = [ ]

non_empty2

non_empty [[ ]] = [ ]

cnf_choice1

[ ] ∪ p = non_empty p

cnf_choice1

[ ] ∪ p = p

non_empty3

non_empty ([ ]#xs) = non_empty xs

non_empty4

non_empty (a@b) = non_empty a @ non_empty b

cnf_choice2

non_empty (x#xs) = [x] ∪ xs

cnf_choice2

(x#xs) = [x] ∪ xs

cnf_choice3

ys ∪ (x#xs) = (ys@[x]) ∪ xs

non_empty5

non_empty ((xx # x) # b) = (xx#x) # (non_empty b)

non_empty6

non_empty ((xx # x) # b) = [xx#x] ∪ (non_empty b)

non_empty6

((xx # x) # b) = [xx#x] ∪ b

non_empty7

((x#xs)@(y#ys)) = (x#xs) ∪ (y#ys)

non_empty7

non_empty ((x#xs)@(y#ys)) = (x#xs) ∪ (y#ys)

non_empty8

a ∪ b ≠ [[ ]] ⟹ a ∪ b = (non_empty a) ∪ (non_empty b)

evaluate (non_empty a) = evaluate a

cnf_choice_4

evaluate (a ∪ b) = evaluate (non_empty a ∪ non_empty b)

state_prop7

S (evaluate [y] (complete_state y)) = complete_state y

skip_prop

S x ⊆ C ⟹ is_feasible x ⟹x ; Skip C ≡ x

concat_prop8

complete_state y ⊆ C ⟹ evaluate [[ ]] C ; evaluate [y] C ≡ evaluate ([[ ]] ; [y]) C

concat_prop9

x ≠ [ ] ⟹ y ≠ [ ] ⟹ [x] ; [y] = [x@y]

concat_prop10

complete_state (x#xs) ⊆ C ⟹ all_feasible (x#xs) ⟹ evaluate [[x]] C ; evaluate [xs] C ≡ evaluate ([[x]] ; [xs]) C

feas_prop1

all_feasible (x @ y) ⟹ all_feasible x

feas_prop2

all_feasible (x @ y) ⟹ all_feasible y

concat_prop11

all_feasible (x@y) ⟹ complete_state (x@y) ⊆ C ⟹ evaluate [x] C ; evaluate [y] C ≡ evaluate ([x] ; [y]) C

concat_prop11_1

all_feasible (x@y) ⟹ evaluate [x] (complete_state (x@y)) ; evaluate [y] (complete_state (x@y)) ≡ evaluate ([x] ; [y]) (complete_state (x@y))

concat_prop12

all_feasible (a#x@y) ⟹ (complete_state (a#x@y)) ⊆ C ⟹ evaluate [a # x] C ; evaluate [y] C ≡ evaluate ([a # x] ; [y]) C

concat_prop12_1

all_feasible (a#x@y) ⟹ evaluate [a # x] (complete_state (a#x@y)) ; evaluate [y] (complete_state (a#x@y)) ≡ evaluate ([a # x] ; [y]) (complete_state (a#x@y))

choice_non_empty

non_empty a ∪ b = a ∪ b

choice_non_empty2

non_empty a ∪ non_empty b = a ∪ b

non_empty9

x ∈ set (non_empty xs) ⟹ x ∈ set xs

non_empty10

non_empty xs = [y] ⟹ ∃a b. a@y#b = xs

non_empty11

xs = [ ] ⟹ evaluate xs C = Fail {}

non_empty12

non_empty xs = [x] ⟹ non_empty xs = xs ⟹ evaluate xs = evaluate [x]

nonempty_monotonic

size (non_empty (x#xs)) > size (non_empty xs)

non_empty_reduces_size

size (non_empty xs) < size xs

non_empty_13

size (x#xs) = size (non_empty (x#xs)) ⟹ x ≠ [ ]

non_empty_14

size b = size (non_empty b) ⟹ b = (non_empty b)

eval_prop3

size b = 1 ⟹ size (non_empty b) = 1 ⟹ evaluate b = evaluate (non_empty b)

comp_cnf3

x ≠ [ ] ⟹ y ≠ [ ] ⟹ Concat x (complete_state (x@y)) ; Concat y (complete_state (x@y)) = Concat (x @ y) (complete_state (x@y))

comp_prop1

x ; (y ∪ Skip {}) ≡ x ; y

choice_cnf_thm

evaluate xs (complete_cnf_state (xs@ys)) ∪ evaluate ys (complete_cnf_state (xs@ys)) ≡ evaluate (xs ∪ ys) (complete_cnf_state (xs@ys))

non_empty14

∀t ∈ set xs. t ≠ [ ] ⟹ non_empty xs = xs

choic_cnf1

(x#xs) ; ys = ([x] ; ys) ∪ (xs ; ys)

comp_distrib_r

(b ∪ c) ; a = (b ; a) ∪ (c ; a)

choice_cnf_commute

a ∪ (b ∪ c) = (a ∪ b) ∪ c

equal_sym

equal_cnf a b = equal_cnf b a

equal_empty

equal_cnf a [ ] ⟹ a = [ ]

eval_prop1

ys≠[ ] ⟹ evaluate ys C ∪ evaluate [y] C = evaluate (ys @ [y]) C

evaluate_switch

evaluate (y#ys) C = evaluate (ys@[y]) C

evaluate_split

xs≠[ ] ⟹ ys ≠ [ ] ⟹ evaluate (xs@ys) C = evaluate xs C ∪ evaluate ys C

evaluate_switch2

evaluate (yss@yse) C = evaluate (yse@yss) C

eval_perm

a#ys’ ∈ set (permutations ys) ⟹ evaluate (a#ys’) C = evaluate ys C

perm_eval

xs ∈ set (permutations ys) ⟹ evaluate xs C = evaluate ys C

perm_prop

[t. t ← xs, ¬ p t] @ [t. t ← xs, p t] ∈ set (permutations xs)

size_prop

size ([t. t ← xs, ¬ p t] @ [t. t ← xs, p t]) = size xs

evaluate_split1

size (xs@ys) ≠ 1 ⟹ evaluate xs C ∪ evaluate ys C = evaluate (xs@ys) C

evaluate_split2

size xs ≠1 ⟹ evaluate xs C = evaluate [t. t ← xs, t =x] C ∪ evaluate [t. t ← xs, t≠x] C

size_prop1

size [t. t←a, t=x] + size [t. t←a, t≠x] = size a

evaluate_prop

size xs = 1 ⟹ ∀t ∈ set xs. t=x ⟹ evaluate xs = evaluate [x]

evaluate_prop2

size xs > 1 ⟹ ∀t ∈ set xs. t=x ⟹ evaluate xs C = evaluate [x] C ∪ evaluate [x] C

equal_eval

equal_cnf a b ⟹ evaluate a C = evaluate b C

eval_simp

∀C. evaluate a C = evaluate b C ⟹ evaluate a = evaluate b

equal_eval2

equal_cnf a b ⟹ evaluate a = evaluate b

eq_reflexive

equal xs xs

comp_prop

tr ∈ set (xs ; ys) ⟹ ∃x y. x ∈ set xs ∧ y ∈ set ys ∧ x@y = tr

comp_prop2

x ∈ set xs ⟹ y ∈ set ys ⟹ x@y ∈ set (xs ; ys)

choice_prop

tr ∈ set (xs ∪ ys) ⟹ (tr ∈ set xs ∨ tr ∈ set ys)

same_traces_size_equal

∀tr ∈ set xs. tr ∈ set ys ⟹ ∀tr ∈ set ys. tr ∈ set xs ⟹ size xs = size ys ⟹ equal_cnf xs ys

same_traces_size_equal2

size xs = size ys ⟹ equal_cnf xs ys ⟹ ∀tr ∈ set xs. tr ∈ set ys

same_traces_size_equal3

size xs = size ys ⟹ equal_cnf xs ys ⟹ ∀tr ∈ set ys. tr ∈ set xs

comp_prop3

∃q w. q ∈ set a ∧ w ∈ set b ∧ tr = q @ w ∧ q ≠ [ ] ∧ w ≠ [ ] ⟹ tr ∈ set (a ; b)

choice_prop2

∃q. (q ∈ set a ∨ q ∈ set b) ∧ tr = q ∧ q ≠ [ ] ⟹ tr ∈ set (a ∪ b)

size (a ∪ b) = size (a) + size (b)

comp_size

x ≠ [ ] ⟹ length (((xx # x) # xs) ; b) = length ((x # xs) ; b)

comp_size2

size ([[a]] ; b) = size b

comp_size3

size (a ; b) = size a * size b

feas_prop

all_feasible xs ⟹ is_feasible (Concat xs C)

feas_prop3

is_feasible (evaluate [ ] C)

feas_prop4

is_feasible (evaluate [[ ]] C)

feas_prop5

is_feasible x ⟹ is_feasible (evaluate [[x]] C)

eval_prop4

xs ≠ [ ] ⟹ evaluate [x # xs] C = evaluate [[x]] C ; evaluate [xs] C

feas_prop6

all_feasible xs ⟹ is_feasible (evaluate [xs] C)

feas_prop7

∀bb ∈ set b. all_feasible bb ⟹ is_feasible (evaluate b C)

cnf_state_prop

complete_cnf_state (x#b) ⊆ C ⟹ complete_cnf_state b ⊆ C

cnf_state_prop2

complete_state xs ⊆ C ⟹ S (evaluate [xs] C) ⊆ C

cnf_state_prop1

complete_cnf_state xs ⊆ C ⟹ S (evaluate xs C) ⊆ C

skip_left_neutral

complete_cnf_state b ⊆ C ⟹ Skip C ; evaluate b C ≡ evaluate b C

skip_right_neutral

∀bb ∈ set b. all_feasible bb ⟹ complete_cnf_state b ⊆ C ⟹ evaluate b C ; Skip C ≡ evaluate b C

feas_prop8

all_feasible x ⟹ all_feasible b1 ⟹ all_feasible (x @ b1)

state_prop

y ∈set ys ⟹ complete_state (ys) = complete_state (y#ys)

state_prop8

set xs ⊆ set ys ⟹ complete_state xs ⊆ complete_state ys

state_prop9

complete_cnf_state (xs # [ys]) = complete_state (xs @ ys)

compose_equiv

complete_cnf_state (x#b) ⊆ C ⟹ all_feasible x ⟹ ∀bb ∈ set b. all_feasible bb ⟹ evaluate [x] C ; evaluate b C ≡ evaluate ([x] ; b) C

state_prop10

complete_cnf_state (a) ⊆ complete_cnf_state (a @ b)

state_prop11

complete_cnf_state (b) ⊆ complete_cnf_state (a @ b)

state_prop12

set xs ⊆ set ys ⟹ complete_cnf_state xs ⊆ complete_cnf_state ys

eval_choice

evaluate xs C ∪ evaluate ys C ≡ evaluate (xs ∪ ys) C

comp_choice

([x] ; b) ∪ (a’ ; b) = (x#a’) ; b

normal_prop15

set a = set b ⟹ normal_of a B = normal_of b B

normal_prop16

set a ⊆ set b ⟹ normal_of b B → normal_of a B

non_empty_is_smaller

set (non_empty xs) ⊆ set xs

normal_prop17

normal_of a B ⟹ normal_of (non_empty a) B

normal_prop17_5

normal_of xs B ⟹ normal_of [x] B ⟹ normal_of (x#xs) B

normal_prop18

normal_of a B ⟹ normal_of b B ⟹ normal_of (a ∪ b) B

basic_prop6

basic (map ((@) x) bs) ⊆ basic [x] ∪ basic bs

normal_prop19

normal_of [x] B ⟹ normal_of b B ⟹ normal_of [x@ys. ys ← b] B

normal_prop20

normal_of a B ⟹ normal_of b B ⟹ normal_of (a ; b) B

state_prop13

normal_of [x] B ⟹ complete_cnf_state [x] ⊆ complete_state (set_to_list B)

state_prop14

normal_of xs B ⟹ complete_cnf_state xs ⊆ complete_state (set_to_list B)

feas_prop9

all_feasible (set_to_list B) ⟹ normal_of xs B ⟹ ∀tr ∈ set xs. all_feasible tr

comp_prop4

all_feasible x ⟹ all_feasible y ⟹ complete_state x ⊆ C ⟹ complete_state y ⊆ C ⟹ evaluate ([x] ; [y]) C ≡ evaluate [x] C ; evaluate [y] C

complete_cnf_state (x#ys) ⊆ C ⟹ ∀tr∈set (x#ys). all_feasible tr ⟹ evaluate ([x] ; ys) C ≡ evaluate ([x]) C ; evaluate (ys) C

civilized_thm1

all_feasible (set_to_list B) ⟹ S p ⊆ C ⟹ civilized_n p B n ⟹ ∃(y::’a CNF). evaluate y C ≡ p ∧ normal_of y B

set_to_list_prop

finite F ⟹ y ∉ F ⟹ count_list (set_to_list F) y = 0

set_to_list_prop2

finite F ⟹ count_list (set_to_list (F - {y})) y = 0

set_to_list_prop3

count_list (set_to_list {y}) y = 1

set_to_list_prop4

count_list (set_to_list {}) y = 0

set_to_list_prop5

finite F ⟹ y ∉ F ⟹ set_to_list (insert y F) ∈ set (permutations (y # set_to_list F))

finite F ⟹ count_list (set_to_list (insert x F)) x = 1

set_to_list_prop6

finite F ⟹ x ∉ F ⟹ count_list (set_to_list (insert x F)) y = count_list (x#set_to_list F) y

set_to_list_prop7

finite F ⟹ x ∉ F ⟹ x ≠ y ⟹ count_list (set_to_list (insert x F)) y = count_list (set_to_list F) y

set_to_list_prop8

x=y ⟹ count_list (yst@x#ynd) y = count_list (yst@ynd) y + 1

set_to_list_prop9

x≠y ⟹ count_list (yst@x#ynd) y = count_list (yst@ynd) y

set_to_list_prop10

xs ∈ set (permutations ys) ⟹ count_list xs = count_list ys

set_to_list_prop11

finite F ⟹ count_list (set_to_list F) x < 1

set_to_list_prop12

finite F ⟹ x ∈ F ⟹ count_list (set_to_list F) x = 1

set_to_list_prop13

count_list xs x = 1 ⟹ count_list (set_to_list (set xs)) x = 1

set_to_list_prop14

finite F ⟹ complete_state (set_to_list (insert y F)) = complete_state (set_to_list (F)) ∪ S y

set_to_list_prop15

civilized p B ⟹ S p ⊆ complete_state (set_to_list B)

civilized_thm2

all_feasible (set_to_list B) ⟹ civilized p B ⟹ ∃(y::’a CNF). evaluate y (complete_state (set_to_list B)) ≡ p ∧ normal_of y B

fail_is_civilized

finite B ⟹ civilized (Fail{}) B

skip_is_civilized

finite B ⟹ civilized (Skip (complete_state (set_to_list B))) B

civilized_thm3

∃(y::’a CNF). evaluate y (complete_state (set_to_list B)) = p ∧ normal_of y B ⟹ civilized p B

composition_cnf_prop1

[[x]] ; xs = [x#ys. ys ← xs]

composition_cnf_prop2

[y#ys] ; xs = [( y#ys)@t. t ← xs]

non2_prop1

non_empty x = [ ] ⟹ non_empty2 (x # xs) = non_empty2 xs

non2_prop2

non_empty x ≠ [ ] ⟹ non_empty2 (x # xs) = non_empty x # non_empty2 xs

non2_prop3

non_empty2 (xs @ ys) = non_empty2 xs @ non_empty2 ys

non2_prop4

size (non_empty2 xs) < size xs

non2_prop5

non_empty2 (x#xs) = x#xs ⟹ non_empty2 xs = xs

non2_prop5_5

non_empty2 [x] = [x] ⟹ ∀path∈set x. path ≠ [ ]

non2_prop6

non_empty2 xs = xs ⟹ ∀prog ∈ set xs. prog ≠ [ ] ∧ (∀path ∈ set prog. path ≠ [ ])

non_prop1

non_empty xs = xs ⟹ ∀path ∈ set xs. path ≠ [ ]

non2_prop7

non_empty2 xs = xs ⟹ x ∈ set xs ⟹ non_empty x = x

non2_idem

non_empty2 xs = non_empty2 (non_empty2 xs)

inter_head

p ∈ set ((x#xs) ⫴ (y#ys)) ⟹ hd p = x ∨ hd p = y

count_prop

count_list (map ((#) x) xs) (x#p) = count_list xs p

count_prop2

x≠y ⟹ count_list (map ((#) x) xs) (y#p) = 0

interleave_non_empty

p ∈ set ((x#xs) ⫴ (y#ys)) ⟹ p ≠ [ ]

inter2

count_list (ys ⫴ xs) p = count_list (xs ⫴ ys) p

inter_perm

ys ⫴ xs ∈ set (permutations (xs ⫴ ys))

size xs = size ys ⟹ ∀t∈set (zip xs ys). fst t ∈ set (permutations (snd t)) ⟹ concat xs ∈ set (permutations (concat ys))

t15

size xs = size ys ⟹ ∃xs’. xs’ ∈ set (permutations xs) ∧ (∀t∈set (zip xs’ ys). fst t ∈ set (permutations (snd t))) ⟹ concat xs ∈ set (permutations (concat ys))

size [f x y. x ← xs, y ← ys] = size xs * size ys

size [path_m ⫴ path_n. path_m ← xs, path_n ← ys] = size [path_m ⫴ path_n. path_m ← ys, path_n ← xs]

index_prop

length xs = a ⟹ (xs@ys)!(a+b) = ys!b

index_prop2

a < length xs ⟹ xs!a = (xs@ys)!a

index_prop3

size (concat (map (λx. f x y # map (f x) ys) xs)) = size xs * size (y#ys)

list_comp_index

x_ind < size xs ⟹ y_ind < size ys ⟹ [f x y. x ← xs, y ← ys] ! (x_ind * size ys + y_ind) = f (xs ! x_ind) (ys ! y_ind)

interleave_ind_comp

x_ind<size xs ⟹ y_ind<size ys ⟹ [path_m ⫴ path_n. path_m ← xs, path_n ← ys] ! ((x_ind* (size ys))+y_ind) = (xs ! x_ind) ⫴ (ys ! y_ind)

x_ind < size xs ⟹ y_ind < size ys ⟹ [path_m ⫴ path_n. path_m ← xs, path_n ← ys] ! ((x_ind* (size ys))+y_ind) = [path_m ⫴ path_n. path_m ← ys, path_n ← xs] ! ((y_ind* (size xs))+x_ind)

all_elements_have_permutation

x_ind < size xs ⟹ y_ind < size ys ⟹ [path_m ⫴ path_n. path_m ← xs, path_n ← ys] ! ((x_ind* (size ys))+y_ind) ∈ set (permutations ([path_m ⫴ path_n. path_m ← ys, path_n ← xs] ! ((y_ind* (size xs))+x_ind)))

perm_prop1

xs ∈ set (permutations xs’) ⟹ ys ∈ set (permutations ys’) ⟹ xs@ys ∈ set (permutations (xs’@ys’))

is_perm

size xy = sx * sy ⟹ [xy ! ((x_ind*sy)+y_ind). x_ind ← [0..<sx], y_ind ← [0..<sy]] ∈ set (permutations xy)

is_perm2

size xy = size xs * size ys ⟹ [xy ! ((x_ind*(size ys))+y_ind). x_ind ← [0..<size xs], y_ind ← [0..<size ys]] ∈ set (permutations xy)

index_prop4

i < size xs * size ys ⟹ concat (map (λx. map (f x) ys) xs) ! i = f (xs ! (i div length ys)) (ys ! (i mod length ys))

index_prop5

concat (map (λx. map (f x) ys) xs) = [f (xs ! (i div length ys)) (ys ! (i mod length ys)). i ← [0..<size xs * size ys]]

perm_prop2

[ ] ∈ set (permutations xy) ⟹ xy = [ ]

perm_prop5

concat (map (λy. map (λx. f x y) [x]) (ys)) @ concat (map (λy. map (λx. f x y) xs) (ys)) ∈ set (permutations (concat (map (λy. map (λx. f x y) (x # xs)) (ys))))

perm_prop3

[f x y. x ← xs, y ← ys] ∈ set (permutations xy) ⟹ [f x y. y ← ys, x ← xs] ∈ set (permutations xy)

is_perm4

size xy = sx * sy ⟹ [xy ! ((x_ind*sy)+y_ind). y_ind ← [0..<sy], x_ind ← [0..<sx]] ∈ set (permutations xy)

perm_exists

xy = [path_m ⫴ path_n. path_m ← xs, path_n ← ys] ⟹ yx = [path_m ⫴ path_n. path_m ← ys, path_n ← xs] ⟹ ∃xy’. xy’ ∈ set (permutations xy) ∧ (∀t∈set (zip xy’ yx). fst t ∈ set (permutations (snd t)))

is_permutation

(xs ∥ ys) ∈ set (permutations (ys ∥ xs))

size (xs ∥ ys) = size (ys ∥ xs)

inter_prop1

xs ≠ [ ] ⟹ interleave xs ys ≠ [ ]

perm_is_equal

xs ∈ set (permutations ys) ⟹ evaluate xs = evaluate ys

evaluate (xs ∥ ys) = evaluate (ys ∥ xs)

CNF_concurrency.thy

(a@b)∥c =(a∥c)@(b∥c)

fact_eq

factorial n = fact n

factorial_mod_product

factorial (a + b) mod (factorial a * factorial b) = (0::nat)

factorial_bound

factorial n > 0

simp_div

a mod b = 0 ⟹ c mod b = 0 ⟹ (a::nat) div b + c div b = (a + c) div b

exits_mulit

∃t::nat. n*t=m ⟹ m mod n = 0

nmb_interleavings_pre (nmb_interleavings_pre x y) z = nmb_interleavings_pre x (nmb_interleavings_pre y z)

number_interleav

length (xs ⫴ ys) = nmb_interleavings xs ys

monoton_fact

a < b ⟹ factorial a < factorial b

interleave_size

size xs * size ys < size (xs ⫴ ys)

list_comp_size

size [f path_m path_n. path_m ← xs, path_n ← ys] > size xs * size ys

interleav_lower_bound

size (xs ⫴ ys) > 1

concat_prop

∀x ∈ set xs. size x > 1 ⟹ size (concat xs) > size xs

conc_size

size xs * size ys < size (xs ∥ ys)

size_one1

size (xs ∥ ys) = 1 ⟹ size xs = 1

size_one2

size (xs ∥ ys) = 1 ⟹ size ys = 1

sum_1

size (concat xs) = sum [size x. x←xs]

path_decomp

path ∈ set (p ∥ q) ⟹ ∃path_p path_q. path_p ∈ set p ∧ path_q ∈ set q ∧ path ∈ set (path_p ⫴ path_q)

path_decomp2

path_p ∈ set p ⟹ path_q ∈ set q ⟹ path ∈ set (path_p ⫴ path_q) ⟹ path ∈ set (p ∥ q)

inter_leav1

(p#path) ∈ set ((x#xs) ⫴ (y#ys)) ⟹ ((p=x) ∧ path ∈ set (xs ⫴ (y#ys))) ∨ ((p=y) ∧ path ∈ set ((x#xs) ⫴ (ys)))

inter_leav2

((p=y) ∧ path ∈ set ((x#xs) ⫴ (ys))) ⟹ (p#path) ∈ set ((x#xs) ⫴ (y#ys))

inter_leav3

((p=x) ∧ path ∈ set (xs ⫴ (y#ys))) ⟹ (p#path) ∈ set ((x#xs) ⫴ (y#ys))

conc_lem1

set (xs ∥ ys) = ⋃ {set (path_x ⫴ path_y)

path_x path_y. path_x ∈ set xs ∧ path_y ∈ set ys}

set ((x#xs) ∥ ys) = set ([x]∥ys) ∪ set (xs∥ys)

assoc_1

set (([x] ∥ [y]) ∥ [z]) ⊆ set ([x] ∥ ([y] ∥ [z]))

assoc_2

set ([x] ∥ ([y] ∥ [z])) ⊆ set (([x] ∥ [y]) ∥ [z])

assoc_3

set (([x] ∥ [y]) ∥ [z]) ⊆ set (((x#xs) ∥ (y#ys)) ∥ (z#zs))

assoc_4

set ([x] ∥ ([y] ∥ [z])) ⊆ set ((x#xs) ∥ ((y#ys) ∥ (z#zs)))

assoc_5

set xs = set xs’ ⟹ set ys = set ys’ ⟹ set (xs ∥ ys) = set (xs’ ∥ ys’)

assoc_6

y ∈ set ys ⟹ x ∈ set xs ⟹ set ((x#xs) ∥ (y#ys)) = set ((xs) ∥ (ys))

assoc_7

set ((xs ∥ ys) ∥ zs) ⊆ set (xs ∥ (ys ∥ zs))

assoc_8

set (xs ∥ (ys ∥ zs)) ⊆ set ((xs ∥ ys) ∥ zs)

assoc_9

set (xs ∥ (ys ∥ zs)) = set ((xs ∥ ys) ∥ zs)

inter_size

size (x ⫴ y) > 0” apply (cases “x=[ ]

inter_size2

size (x ⫴ y) = 1 ⟹ size x = 0 ∨ size y = 0

inter_size3

size x = 0 ∨ size y = 0 ⟹ size (x ⫴ y) = 1

interleaving_lemma

size ([x] ∥ [y]) = nmb_interleavings_pre (size x) (size y)

inter_size4

size (xs ∥ ys) = 1 ⟹ size xs = 1 ∨ size ys = 1

conc_prop

xs ∥ [[ ]] = xs

conc_prop2

[[ ]] ∥ xs = xs

assoc_10

size (xs ∥ (ys ∥ zs)) = 1 ⟹ size ((xs ∥ ys) ∥ zs) = 1

assoc_11

size ((xs ∥ ys) ∥ zs) = 1 ⟹ size (xs ∥ (ys ∥ zs)) = 1

assoc_12

size (xs ∥ (ys ∥ zs)) = 1 ≡ size ((xs ∥ ys) ∥ zs) = 1

assoc_cnf1

equal_cnf ((xs ∥ ys) ∥ zs) (xs ∥ (ys ∥ zs))

assoc_cnf

evaluate ((xs ∥ ys) ∥ zs) = evaluate (xs ∥ (ys ∥ zs))

cnf_prop

xs ≠ [ ] ⟹ evaluate [x#xs] C = x ; (evaluate [xs] C)

cnf_prop2

xs ≠ [ ] ⟹ evaluate [xs@[x]] C = (evaluate [xs] C) ; x

restrict_cnf1

D ⊆ C ⟹ evaluate ([x] / C) D = (evaluate [x] D) / C

restr_distrib

a / C ∪ b / C = (a ∪ b) / C

restrict_cnf

D ⊆ C ⟹ evaluate (xs / C) D = (evaluate xs D) / C

corestrict_cnf1

D ⊆ C ⟹ evaluate ([x] ∖ C) D = (evaluate [x] D) ∖ C

corestrict_cnf

D ⊆ C ⟹ evaluate (xs ∖ C) D= (evaluate xs D) ∖ C

conc_prop1

set (xs ∥ ys) ⊆ set (xs ∥ (y#ys))

conc_prop3

set (xs ∥ ys) ⊆ set (xs ∥ (ys ∪ zs))

conc_prop4

set (xs ∥ (ys ∪ zs)) = set (xs ∥ (zs ∪ ys))

conc_choice1_1

set (xs ∥ (ys ∪ zs)) = set ((xs ∥ ys) ∪ (xs ∥ zs))

choice_size1

size (xs ∥ (ys ∪ zs)) = 1 ⟹ size ((xs ∥ ys) ∪ (xs ∥ zs)) = 1

choice_size2

size ((xs ∥ ys) ∪ (xs ∥ zs)) = 1 ⟹ size (xs ∥ (ys ∪ zs)) = 1

Conc_choice1_1

equal_cnf ((xs ∥ ys) ∪ (xs ∥ zs)) (xs ∥ (ys ∪ zs))

Conc_choice1_

evaluate ((xs ∥ ys) ∪ (xs ∥ zs)) = evaluate (xs ∥ (ys ∪ zs))

conc_prop5

set (xs ∥ ys) ⊆ set ((x#xs) ∥ ys)

conc_prop6

set (xs ∥ ys) ⊆ set ((xs ∪ zs) ∥ ys)

conc_prop7

set ((zs ∪ xs) ∥ ys) = set ((xs ∪ zs) ∥ ys)

conc_choice2_1

set ((xs ∪ ys) ∥ zs) = set ((xs ∥ zs) ∪ (ys ∥ zs))

choice_size3

size ((xs ∪ ys) ∥ zs) = 1 ⟹ size ((xs ∥ zs) ∪ (ys ∥ zs)) = 1

choice_size4

size ((xs ∥ zs) ∪ (ys ∥ zs)) = 1 ⟹ size ((xs ∪ ys) ∥ zs) = 1

Conc_choice2_1

equal_cnf ((xs ∥ zs) ∪ (ys ∥ zs)) ((xs ∪ ys) ∥ zs)

Conc_choice2_

evaluate ((xs ∥ zs) ∪ (ys ∥ zs)) = evaluate ((xs ∪ ys) ∥ zs)

eval_specialize

evaluate ys C ⊆ evaluate (y # ys) C

eval_specialize2

evaluate [y] C ⊆ evaluate (y # ys) C

eval_specialize3

set xs ⊆ set [y] ⟹ evaluate xs C ⊆ evaluate [y] C

eval_specialize4

set [x] ⊆ set ys ⟹ evaluate [x] C ⊆ evaluate ys C

eval_specialize5

size xs > 1 ⟹ equal_cnf xs zs ⟹ evaluate xs C = evaluate [ ] C ∪ evaluate zs C

eval_specialize6

size (ys @ zs) > 1 ⟹ evaluate ys C ∪ evaluate zs C = evaluate (ys ∪ zs) C

eval_specialize7

size xs ≠ 1 ⟹ equal_cnf xs (ys ∪ zs) ⟹ evaluate xs C = evaluate ys C ∪ evaluate zs C

eval_specialize8

evaluate [x. x ← xs, f x] C ⊆ evaluate xs C

eval_specialize9

evaluate [x. x ← (x#xx#xs), f x] C ∪ evaluate [x. x ← x#xx#xs, ¬ f x] C = (evaluate [x] C ∪ evaluate [xx] C) ∪ (evaluate [x. x ← (xs), f x] C ∪ evaluate [x. x ← xs, ¬ f x] C)

eval_specialize10

(evaluate [x] C ∪ evaluate [xx] C) ∪ (evaluate [x. x ← (xs), f x] C ∪ evaluate [x. x ← xs, ¬ f x] C) = (evaluate [x] C ∪ evaluate [xx] C) ∪ (evaluate xs C)

eval_specialize11

size xs > 1 ⟹ evaluate [x. x ← xs, f x] C ∪ evaluate [x. x ← xs, ¬ f x] C = evaluate xs C

eval_specialize12

set xs ⊆ set ys ⟹ evaluate xs C⊆ evaluate ys C

subset1

set (p ; xs) ⊆ set (p ; (x#xs))

subset2

set (xs ; p) ⊆ set ((x#xs) ; p)

subset3

set (p ∪ xs) ⊆ set (p ∪ (x#xs))

subset4

set (xs ∪ p) ⊆ set ((x#xs) ∪ p)

subset5

set q ⊆ set q’ ⟹ set (p ; q) ⊆ set (p ; q’)

subset6

set q ⊆ set q’ ⟹ set (q ; p) ⊆ set (q’ ; p)

subset7

set q ⊆ set q’ ⟹ set (p ∪ q) ⊆ set (p ∪ q’)

subset8

set q ⊆ set q’ ⟹ set (q ∪ p) ⊆ set (q’ ∪ p)

subset9

set q ⊆ set q’ ⟹ set (p ∥ q) ⊆ set (p ∥ q’)

subset10

set q ⊆ set q’ ⟹ set (q ∥ p) ⊆ set (q’ ∥ p)

interleav_prop

ps @ rs ∈ set (ps ⫴ rs)

prop5

set (map (λxs. xs @ [p]) (ps ⫴ (qs @ [q]))) = {tr @ [p]

tr. tr ∈ set (ps ⫴ (qs @ [q]))}

prop6

set (map (λxs. xs @ [q]) ((ps @ [p]) ⫴ qs )) = {tr @ [q]

tr. tr ∈ set ((ps @ [p]) ⫴ qs)}

prop3_1

[x] ⫴ ys = insert_all x ys

prop3_2

ys ⫴ [x] = rev (insert_all x ys)

prop3_3

set ([x] ⫴ (y#ys)) = {x#y#ys} ∪ {y#x#ys} ∪ ((#) y) ` set ([x] ⫴ ys)

prop3_4

set ([x] ⫴ (ys@[y])) = {ys@[x,y]} ∪ {ys@[y,x]} ∪ (λtr. tr@[y]) ` set ([x] ⫴ ys)

prop3_5

set ([x] ⫴ rev (y#ys)) = {(rev ys)@[x,y]} ∪ {(rev ys)@[y,x]} ∪ (λtr. tr@[y]) ` set ([x] ⫴ (rev ys))

prop3_6

{rev tr

tr. tr ∈ set ([x] ⫴ (ys))} = set ([x] ⫴ rev ys)

prop3_7

rev ` set ([x] ⫴ ys) = set ([x] ⫴ rev ys)

prop3_8

(λtr. tr @ [y]) ` set ([x] ⫴ ys) ⊆ set ([x] ⫴ (ys @ [y]))

prop3_9

tr ∈ set ([x] ⫴ rev ys) ⟹ tr @ [y] ∈ set ([x] ⫴ (rev ys @ [y]))

prop3_10

(map (λzs. zs@[y]) (insert_all x ys)) @ [ys@[y,x]] = insert_all x (ys@[y])

prop3_10_1

map (λtr. tr @ [y]) ([x] ⫴ ys) @ [ys@[y,x]] = insert_all x (ys@[y])

prop3_11

xa ∈ set ([x] ⫴ (rev ys @ [y])) ⟹ xa ∉ (λtr. tr @ [y]) ` set ([x] ⫴ rev ys) ⟹ xa = rev ys @ [y, x]

prop3_12

x≠y ⟹ set (map ((#) y) ((x#xs) ⫴ ys)) ∩ set (map ((#) x) (xs ⫴ (y#ys))) = {}

prop3_13

x≠y ⟹ set (map ((#) x) (xs ⫴ (y#ys))) = set ((x#xs) ⫴ (y#ys)) - set (map ((#) y) ((x#xs) ⫴ ys))

prop3_14

(x#xs) ⫴ (x#ys) = map ((#) x) ((xs ⫴ (x#ys)) @ ((x#xs) ⫴ ys))

prop3_15

set [(xs @ [x, y])] ∪ (λtr. tr @ [x]) ` set ((xs ⫴ [y])) = set (((xs @ [x]) ⫴ [y]))

prop3_16

set (map (λtr. tr@[y]) (rev (x#xs) ⫴ rev ys)) ∪ set (map (λtr. tr@[x]) (rev xs ⫴ rev (y#ys))) = set (rev (x # xs) ⫴ rev (y # ys))

prop3

set (map rev (xs ⫴ ys)) = set (rev xs ⫴ rev ys)

prop4

set ((ps @ [p]) ⫴ (qs @ [q])) = {tr @ [p]

tr. tr ∈ set (ps ⫴ (qs @ [q]))} ∪ {tr @ [q]

tr. tr ∈ set ((ps @ [p]) ⫴ qs)}

prop7

set ((ps@[p]) ⫴ (qs@[q])) = set (map (λxs. xs@[p]) (ps ⫴ (qs@[q])) @ map (λxs. xs@[q]) ((ps@[p]) ⫴ qs))

prop8

xs ∈ set ys ⟹ xs@[x] ∈ set (map (λt. t@[x]) ys)

prop9

xs ∈ set (p ⫴ q) ⟹ xs @ r ∈ set (p ⫴ (q @ r))

prop9_1

xs ∈ set ((p ⫴ r)) ⟹ q @ xs ∈ set (p ⫴ (q @ r))

prop10

set ([p] ∥ [q] ; [r]) ⊆ set ([p] ∥ ([q] ; [r]))

prop10_1

set ([p] ∥ [r] ; [q]) ⊆ set (([p] ; [q]) ∥ [r])

prop10_2

set ([q] ; [p] ∥ [r]) ⊆ set ([p] ∥ ([q] ; [r]))

prop10_3

set ([p] ; [q] ∥ [r]) ⊆ set (([p] ; [q]) ∥ [r])

inter1

set ((ps ⫴ qs) ; (rs ⫴ vs)) ⊆ set ((ps @ rs) ⫴ (qs @ vs))

prop10_3_1

set ([p] ∥ [q] ; [r] ∥ [v]) ⊆ set (([p] ; [r]) ∥ ([q] ; [v]))

prop10_4

set ([p] ∥ [q] ; [r] ∥ vs) ⊆ set (([p] ; [r]) ∥ ([q] ; vs))

prop11

set ([p] ∥ qs ; [r]) ⊆ set ([p] ∥ (qs ; [r]))

prop12

set (([p] ∥ rs) ; [q]) ⊆ set (([p] ; [q]) ∥ rs)

prop13

set ([q] ; [p] ∥ rs) ⊆ set ([p] ∥ ([q] ; rs))

prop14

set ([p] ; qs ∥ [r]) ⊆ set (([p] ; qs) ∥ [r])

prop15

set ([p] ∥ ([q]) ; rs ∥ s) ⊆ set (([p] ; rs) ∥ ([q] ; s))

subset12

set (ps ∥ q ; [r]) ⊆ set (ps ∥ (q ; [r]))

subset13

set ((ps ∥ r) ; [q]) ⊆ set ((ps ; [q]) ∥ r)

subset14

set ([q] ; ps ∥ r) ⊆ set (ps ∥ ([q] ; r))

subset15

set ([p] ; q ∥ rs) ⊆ set (([p] ; q) ∥ rs)

subset16

set ([p] ∥ qs ; r ∥ s) ⊆ set (([p] ; r) ∥ (qs ; s))

Conc_composeright_1

set ((p ∥ q) ; rs) ⊆ set (p ∥ (q ; rs))

Conc_composeright1_1

set ((p ∥ r) ; qs) ⊆ set ((p ; qs) ∥ r)

Conc_composeleft1_1

set (qs ; (p ∥ r)) ⊆ set (p ∥ (qs ; r))

Conc_composeright_2

set (ps ; (q ∥ r)) ⊆ set ((ps ; q) ∥ r)

Conc_composeleft

evaluate ((p ∥ q) ; r) C ⊆ evaluate (p ∥ (q ; r)) C

Conc_composeleftright

evaluate (q ; (p ∥ r)) C ⊆ evaluate (p ∥ (q ; r)) C

Conc_composeright

evaluate (p ; (q ∥ r)) C ⊆ evaluate ((p ; q) ∥ r) C

Conc_composerightleft

evaluate ((p ∥ r) ; q) C ⊆ evaluate ((p ; q) ∥ r) C

Conc_composegeneral

set (([p] ; [q]) ∥ ([u] ; [v])) ⊆ set (([p] ; [u]) ∥ ([q] ; [v]))

Conc_composegeneral

set (([p] ; [u]) ∥ ([q] ; [v])) ⊆ set (([p] ; [q]) ∥ ([u] ; [v]))

Conc_composegeneral

set ((p ; q) ∥ (u ; v)) ⊆ set ((p ; u) ∥ (q ; v))

Conc_composegeneral_1

set ((ps ∥ q) ; (r ∥ s)) ⊆ set ((ps ; r) ∥ (q ; s))

Conc_composegeneral

evaluate ((p ∥ q) ; (r ∥ s)) C ⊆ evaluate ((p ; r) ∥ (q ; s)) C

foldl (+) (b::nat) xs = b + foldl (+) 0 xs

cnf_prop1

cnf_concurrency2 [[x]] [[y]] C = evaluate ([x] ⫴ [y]) C

is_rounded a ⟹ (a ; b) ∪ (a ; c) = a ; (b ∪ c)

cnf2_prop

cnf_feasible ([y]#ys) ⟹ complete_cnf_state ([y]#ys) ⊆ C ⟹ ⋃ (map ((λxs. Concat xs C) ∘ (#) y) (ys)) ≡ y ; ⋃ (map (λxs. Concat xs C) (ys))

cnf2_prop2

cnf_feasible xs ⟹ is_feasible x ⟹ cnf_feasible (map ((#) x) (xs))

cnf2_prop3

cnf_feasible xs ⟹ cnf_feasible ys ⟹ cnf_feasible (xs@ys)

cnf2_prop4

all_feasible (xs@ys) ⟹ cnf_feasible (xs ⫴ ys)

cnf2_prop5

xs ≠ [ ] ⟹ complete_cnf_state (map ((#) x) xs) = S x ∪ complete_cnf_state xs

cnf2_prop6

complete_cnf_state xs ∪ complete_cnf_state ys = complete_cnf_state (xs@ys)

cnf2_prop7

complete_state xs ∪ complete_state ys = complete_cnf_state (xs ⫴ ys)

cnf2_prop8

S y ⊆ C ⟹ is_feasible y ⟹ ⋃ (map ((λxs. Concat xs C) ∘ (#) y) ys) ≡ ⋃ (map (λxs. y ; Concat xs C) ys)

cnf2_prop9

⋃ (map (λxs. y ; Concat xs C) xs) ≡ y ; ⋃ (map (λxs. Concat xs C) xs)

cnf2_prop10

is_feasible y ⟹ S y ⊆ C ⟹ y ; ⋃ (map (λxs. Concat xs C) ([x] ⫴ ys)) ≡ ⋃ (map ((λxs. Concat xs C) ∘ (#) y) ([x] ⫴ ys))

cnf2_prop11

size xs = size ys ⟹ ∀z ∈ set (zip xs ys). fst z ≡ snd z ⟹ ⋃ xs ≡ ⋃ ys

cnf2_prop12

is_feasible x ⟹ S x ⊆ C ⟹ evaluate (map ((#) x) xs) C ≡ x ; evaluate xs C

cnf_prop5

all_feasible (xs@ys) ⟹ complete_state (xs@ys) ⊆ C ⟹ cnf_concurrency2 [xs] [ys] C ≡ evaluate (xs ⫴ ys) C

cnf_prop3

all_feasible (x#ys) ⟹ complete_state (x#ys) ⊆ C ⟹ cnf_concurrency2 [[x]] [ys] C ≡ evaluate ([x] ⫴ ys) C

cnf2_prop13

all_feasible (x#xs@[y]) ⟹ complete_state (x#xs@[y]) ⊆ C ⟹ x ; cnf_concurrency2 [xs] [[y]] C ≡ evaluate (map ((#) x) (xs ⫴ [y])) C

cnf2_prop14

all_feasible (xs@ys) ⟹ complete_state (xs@ys) ⊆ C ⟹ cnf_concurrency2 [xs] [ys] C ≡ evaluate ([xs] ∥ [ys]) C

cnf2_prop15

cnf_feasible (x#ys) ⟹ complete_cnf_state (x#ys) ⊆ C ⟹ cnf_concurrency2 [x] ys C ≡ evaluate(concat (map ((⫴) x) ys)) C

cnf2_prop16

cnf_feasible (xs @ ys) ⟹ cnf_feasible ys

cnf2_prop17

cnf_feasible (xs @ ys) ⟹ cnf_feasible xs

cnf_feasible (xs @ ys) ⟹ complete_cnf_state (xs @ ys) ⊆ C ⟹ cnf_concurrency2 xs ys C ≡ evaluate (xs ∥ ys) C

Complex_operation_interactions.thy

cond_distrib2_1

GC [(C₁, p), (C₂, q)] / D = GC [((D ∩ C₁), p), ((D ∩ C₂), q)]

Cond_distrib2_2

GC [(C₁, p), (C₂, q)] / D ≡ GC [((D ∩ C₁), p), ((D ∩ C₂), q)]

restriction_ite

(ITE C a b) / D = (ITE C (a/D) (b/D))

restriction_ite

(ITE C a b) / D = (ITE C (a/D) (b/D))

restriction_ite

(ITE C a b) / D ≡ (ITE C (a/D) (b/D))

restriction_fixed_repetition_1

0<n ⟹ (p^{n + 1}) / C ≡ (p / C) ; (pⁿ)

restriction_fixed_repetition_2

is_feasible p ⟹ (pⁿ) / C ≡ (Skip (S p) / C) ; (pⁿ)

restriction_fixed_repetition_3

(pⁿ) / C ≡ (Skip C) ; (pⁿ)

loop p s f / C ≡ Skip C ; loop p s f

cond_distrib1_gc_1

GC [(C₁, p₁), (C₂, (p₂ ∪ p₃))] = (GC [(C₁, p₁), (C₂, p₂)]) ∪ (GC [(C₁, p₁), (C₂, p₃)])

cond_distrib1_gc_2

GC [(C₁, p₁), (C₂, (p₂ ∪ p₃))] ≡ (GC [(C₁, p₁), (C₂, p₂)]) ∪ (GC [(C₁, p₁), (C₂, p₃)])

cond_distrib1_gc_3

GC [(C₁, (p₁ ∪ p₃)), (C₂, p₂)] = GC [(C₁, p₁), ( C₂, p₂)] ∪ GC [(C₁, p₃), ( C₂, p₂)]

cond_distrib1_gc_4

GC [(C₁, (p₁ ∪ p₃)), ( C₂, p₂)] ≡ GC [(C₁, p₁), ( C₂, p₂)] ∪ GC [(C₁, p₃), ( C₂, p₂)]

cond_distrib1_ite_1

(ITE C p₁ (p₂ ∪ p₃)) = (ITE C p₁ p₂) ∪ (ITE C p₁ p₃)

cond_distrib1_ite_2

(ITE C p₁ (p₂ ∪ p₃)) ≡ (ITE C p₁ p₂) ∪ (ITE C p₁ p₃)

cond_distrib1_ite_3

(ITE C (p₁ ∪ p₂) p₃) = (ITE C p₁ p₃) ∪ (ITE C p₂ p₃)

cond_distrib1_ite_4

(ITE C (p₁ ∪ p₂) p₃) ≡ (ITE C p₁ p₃) ∪ (ITE C p₂ p₃)

guard_ifthenelse

ITE C p₁ p₂ = GC [(C, p₁), ((-C), p₂)]

until_def_lemma

until_loop a C b n ≡ a ; (loop (b/(-C)) 0 n)∖C

Fixed_repetition.thy

state_space_is_same

S p = S (p ^{«/sup>/a> n)}

state_space_is_same2

State (pⁿ) = S p

fixed_pre_decreases

Pre (p^{n + 1}) ⊆ Pre (pⁿ)

fixed_rep_one_1

p¹ ≡ p / (Pre p)

fixed_rep_one_2

is_feasible p ⟹ p¹ ≡ p

fixed_rep_one_3

x ; p¹ ≡ x ; p

fixed_rep_two_1

p² ≡ p ; p

fixed_rep_decomp_front

0<i ⟹ p^{i + 1} ≡ p ; pⁱ

fixed_rep_decomp_back

is_feasible p ⟹ p^{i + 1} ≡ pⁱ ; p

fixed_rep_feasibility

is_feasible p ⟹ is_feasible (pⁿ)

fixed_rep_prop_2

p^{i + 1} ≡ pⁱ ; p

range_decreases_fixed_repetition

0 < n ⟹ Range_p (x ^{«/sup>/a> n) ⊆}Range_p x

range_decreases_fixed_repetition_2

0 < n ⟹ Range_p (x ^{«/sup>/a> n + 1) ⊆}Range_p (x ^{«/sup>/a> n)}

fixed_prop

x¹ = Skip (Pre x) ; x

skip_choice

Skip (Pre x) ; x ∪ Skip (Pre y) ; y = Skip (Pre x ∪ Pre y) ; (x ∪ y)

comp_prop

Range_p a ∩ Pre d = {} ⟹ Range_p c ∩ Pre b = {} ⟹ a ; b ∪ c ; d = (a ∪ c) ; (b ∪ d)

arbitrary_repetition_simplification

0<n ⟹ all_feasible [x,y] ⟹ Range_p x ∩ Pre y = {} ⟹ Range_p y ∩ Pre x = {} ⟹ xⁿ ∪ yⁿ = (x ∪ y)ⁿ

arbitrary_repetition_simplification2

0<n ⟹ all_feasible [x,y] ⟹ Range_p x ∩ Pre y = {} ⟹ Range_p y ∩ Pre x = {} ⟹ xⁿ ∪ yⁿ ≡ (x ∪ y)ⁿ

equality_is_maintained_by_fixed_repetition

p₁ = p₂ ⟹ p₁ⁿ = p₂ⁿ

equiv_is_maintained_by_fixed_repetition

0<n ⟹ all_feasible [p₁, p₂] ⟹ p₁ ≡ p₂ ⟹ p₁ⁿ ≡ p₂ⁿ

skip_compose_r_of_fixed_rep_1

is_feasible p ⟹ pⁿ ≡ pⁿ ; Skip (S p)

skip_compose_l_of_fixed_rep_1

pⁿ ≡ Skip (S p) ; pⁿ

fail_stays_fail_fixed

pⁿ ≡ Fail {} ⟹ pⁿ + 1 ≡ Fail {}

repetition_fail

i<j ⟹ pⁱ ≡ Fail {} ⟹ p^j ≡ Fail {}

fix_rep_prop1

0<i ⟹ pⁱ = Skip (S p) / (Pre p) ; Concat [p . t ← [1 .. int i]] (S p)

fix_rep_prop2

pⁱ = Concat ((Skip (S p) / (Pre p))#[p . t ← [1 .. int i]]) (S p)

Guarded_conditional.thy

gc_S

S (GC ((C,p)#xs)) = S p ∪ S (GC xs)

gc_S_1

S (GC (xs)) = complete_state ([snd t. t ← (xs)])

cond_helper_1

GC (x#xs) = GC (xs @ [x])

cond_helper_2

xs≠[ ] ⟹ GC (x#xs) = GC [x] ∪ GC xs

cond_helper_3

a ≠[ ] ⟹ b≠ [ ] ⟹ GC (a@b) = GC a ∪ GC b

cond_commute

xs ∈ set (permutations ys) ⟹ GC xs = GC ys

cond_sub1

D₁ ⊆ C₁ ⟹ D₂ ⊆ C₂ ⟹ (GC [(D₁, p), (D₂, q)]) ⊆ (GC [(C₁, p), (C₂, q)])

property_on_gc_3

all_feasible [p₁, p₂] ⟹ GC [(C₁, p₁), (C₂, p₂)] ⊑ p₁ / C₁

property_on_gc_3_1

weakens (GC [(C₁, p₁), (C₂, p₂)]) (p₁ / C₁)

property_on_gc_3_2

strengthens (p₁ / C₁) (GC [(C₁, p₁), (C₂, p₂)])

cond_sub4

(p₁ / C₁) ⊆ (GC [(C₁, p₁), (C₂, p₂)])

refinement_safety_gc_1

all_feasible [p, q] ⟹ D₁ ⊆ C₁ ⟹ D₂ ⊆ C₂ ⟹ GC [(D₁, p), (D₂, q)] ⊑ GC [(C₁, p), (C₂, q)]

refinement_safety_gc_2

all_feasible [p, q] ⟹ D₁ ⊆ C₁ ⟹ D₂ ⊆ C₂ ⟹ GC [(C₁, p), (C₂, q)] ⊑ GC [(D₁, p), (D₂, q)]

refinement_safety_gc_weakens

D₁ ⊆ C₁ ⟹ D₂ ⊆ C₂ ⟹ weakens (GC [(C₁, p), (C₂, q)]) (GC [(D₁, p), (D₂, q)])

refinement_safety_gc_strengthens

D₁ ⊆ C₁ ⟹ D₂ ⊆ C₂ ⟹ strengthens (GC [(D₁, p), (D₂, q)]) (GC [(C₁, p), (C₂, q)])

cond_refine1

D₁ ⊆ C₁ ⟹ D₂ ⊆ C₂ ⟹ (GC [(D₁, p), (D₂, q)]) ⊑ (GC [(C₁, p), (C₂, q)])

cond_refine2

q₁ ⊑ p₁ ⟹ q₂ ⊑ p₂ ⟹ GC [(C, q₁), (C, q₂)] ⊑ GC [(C, p₁), (C, p₂)]

refinement_safety_gc_3

all_feasible [p₁, p₂, q₁, q₂] ⟹ strengthens q₁ p₂ ⟹ strengthens q₂ p₁ ⟹ q₁ ⊑ p₁ ⟹ q₂ ⊑ p₂ ⟹ GC [(C, q₁), (C, q₂)] ⊑ GC [(C, p₁), (C, p₂)]

refinement_safety_gc_4

all_feasible [p₁, p₂, q₁, q₂] ⟹ independent q₁ p₂ ⟹ independent q₂ p₁ ⟹ q₁ ⊑ p₁ ⟹ q₂ ⊑ p₂ ⟹ GC [(C, q₁), (C, q₂)] ⊑ GC [(C, p₁), (C, p₂)]

cond_refine4

GC [(C₁, p₁), (C₂, p₂)] ⊑ p₁ / C₁

cond_sub2

q₁ ⊆ p₁ ⟹ q₂ ⊆ p₂ ⟹ GC [(C, q₁), (C, q₂)] ⊆ GC [(C, p₁), (C, p₂)]

cond_distrib

GC xs / C ≡ GC [(fst t ∩ C, snd t) . t ← xs]

GC_prop_22

a ∪ GC (x#xs) = a ∪ (GC [x] ∪ GC xs)

gc_prop1

S (snd x) ⊆ complete_state (map snd xs) ⟹ fst x = FALSE ⟹ 1 < length xs ⟹ GC (x # xs) = GC xs

gc_prop2

S (snd x) ⊆ complete_state (map snd (a@b)) ⟹ fst x = FALSE ⟹ size (a@b) > 1 ⟹ GC (a@x#b) = GC(a@b)

if_false2

fst x = FALSE ⟹ GC (a@x#b) ≡ GC(a@b)

gc_prop4

S (snd x) ⊆ complete_state (map snd (a@b)) ⟹ fst x = FALSE ⟹ size (a@b) = 0 ⟹ GC (a@x#b) = GC(a@b)

fail_choice

S q ⊆ S p ⟹ q ≡ Fail {} ⟹ q ∪ p = Fail {} ∪ p

gc_prop5

S (snd x) ⊆ complete_state (map snd (a@b)) ⟹ fst x = FALSE ⟹ size (a@b) = 1 ⟹ GC (a@x#b) = Fail {} ∪ GC(a@b)

cond_one

GC [(C,p)] = p/C

gc_prop6

x / C ⊆ GC ((C,x) # xs)

gc_prop7

GC a ⊆ GC (a@b)

cond_sub3

(C, x) ∈ set (xs) ⟹ x/C ⊆ GC xs

If_then_else.thy

ite_S

S (ITE C q₁ q₂) = S q₁ ∪ S q₂

cond_swap

ITE C p₁ p₂ = ITE (-C) p₂ p₁

property_on_ite_2

Pre (p / C) = Pre (ITE C p (Skip (S p)))

cond_refine3

q₁ ⊑ p₁ ⟹ q₂ ⊑ p₂ ⟹ ITE C q₁ q₂ ⊑ ITE C p₁ p₂

cond_refine4

q₁ ⊆ p₁ ⟹ q₂ ⊆ p₂ ⟹ ITE C q₁ q₂ ⊆ ITE C p₁ p₂

Non_atomic_concurrency.thy

non_atomic_prop1

[ ] ∥ x = x

non_atomic_prop2

((a # xs) ∥ x) ≡ a ; (xs ∥ x) ∪ Concat (x#a#xs)

compose_distrib

(b ∪ (a ; c ∪ a ; d)) = (b ∪ a ; (c ∪ d))

concur_two

[a]∥b = a ; b ∪ b ; a

concur_commute

[a]∥b = ([b]∥a)

compose_distrib2

∀x ∈ set xs. x ≠ [ ] ⟹ xs ≠ [ ] ⟹ b ∪ ⋃ [a ; (Concat t). t ← xs] = b ∪ a ;⋃ [(Concat t). t ← xs]

concur_recursive

((a # xs) ∥ x) = a ; (xs ∥ x) ∪ Concat (x#a#xs)

non_atomic_conc_S

S (xs∥x) = complete_state (x#xs)

concor_three_1

[p₁, p₂] ∥ q = ((q ; p₁) ; p₂ ∪ ((p₁ ; q) ; p₂)) ∪ ((p₁ ; p₂) ; q)

concor_three_2

[p₁, p₂] ∥ q = ((q ; p₁) ; p₂ ∪ ((p₁ ; q) ; p₂)) ∪ ((p₁ ; p₂) ; q)

concor_three_3

[p₁, p₂] ∥ q ≡ ((q ; p₁) ; p₂ ∪ ((p₁ ; q) ; p₂)) ∪ ((p₁ ; p₂) ; q)

Concat_feasible

all_feasible xs ⟹ is_feasible (Concat xs)

Choice_feasible

all_feasible xs ⟹ is_feasible (⋃ xs)

all_feasible_prop

all_feasible xs ⟹ x ∈ set xs ⟹ is_feasible x

all_feasible_prop_1

∀x ∈ set xs. is_feasible x ≡ all_feasible xs

all_feasible_prop_2

xs ∈ set (permutations ys) ⟹ all_feasible ys ⟹ all_feasible xs

non_atomic_conc_feasible_preserving

all_feasible (x#xs) ⟹ is_feasible (xs ∥ x)

atomic_conc_refinement_safe

q₁ ⊑ p₁ ⟹ q₂ ⊑ p₂ ⟹ q₃ ⊑ p₃ ⟹ ([q₁, q₂] ∥ q₃) ⊑ ([p₁, p₂] ∥ p₃)

((ys@[x])@xs) ∥_G q ≡ (ys@([x]@xs)) ∥_G q

atomic_restrict_1

(xs ∥ x) / C ≡ ⋃ [Concat t / C. t ← insert_all x xs]

concur_restrict

(xs ∥ x) / C = ⋃ [Concat t / C. t ← insert_all x xs]

atomic_corestrict_1

(xs ∥ x) ∖ C ≡ ⋃ [Concat t ∖ C. t ← insert_all x xs]

equiv_list_prop_2

equiv_list xs ys ⟹ ⋃ xs ≡ ⋃ ys

equiv_list_prop_1

∀a ∈ set xs. a ≠ [ ] ⟹ equiv_list [Concat t / C. t ← xs] [Concat (hd t / C # tl t). t ← xs]

equiv_list_prop_3

∀a ∈ set xs. a ≠ [ ] ⟹ equiv_list [Concat t ∖ C. t ← xs] [Concat (butlast t @ [(last t)∖ C]). t ← xs]

concur_restrict

(xs ∥ x) / C ≡ ⋃ [Concat (hd t/C#tl t). t ← insert_all x xs]

concur_corestrict

(xs ∥ x) ∖ C ≡ ⋃ [Concat (butlast t @ [(last t)∖ C]). t ← insert_all x xs]

concur_specialize1

p ; q ⊆ ([p] ∥ q)

non_atomic_specialize

ys ∈ set (insert_all x xs) ⟹ (Concat ys) ⊆ (xs ∥ x)

commute_compose

commute_programs3 a b ⟹ [a] ∥ b ≡ a ; b

concur_distrib1

xs∥(b ∪ c) ≡ (xs∥b) ∪ (xs∥c)

concur_choice1

[a∪b]∥(c) = ([a]∥c) ∪ ([b]∥c)

concur_choice2

xs∥(b ∪ c) = (xs∥b) ∪ (xs∥c)

concur_specialize2

([Concat xs] ∥ x) ⊆ (xs ∥ x)

Permutations.thy

simp_2

∀x₁ x₂ x₃. f (f x₁ x₂) x₃ = f x₁ (f x₂ x₃) ⟹ foldl f (f a x) xs = f a (foldl f x xs)

fold_composition_assoc

foldl (;) x (as @ [a]) = (foldl (;) x as) ; a

S_foldl_composition

S (foldl (;) x as) = ⋃ (S ` (set (x # as)))

main_theorem

S (foldl (;) x (a # as)) = S ((foldl (;) x as) ; a)

skip_fold_complete_state

S (Skip (complete_state (x # xs))) ∪ S x ∪ S (foldl (;) x xs) = complete_state (x # xs) ∪ S x ∪ complete_state xs

simp_5

S (foldl (;) (Skip (complete_state xs)) xs) = complete_state xs

simp_4_right

S (foldl (;) (Skip (complete_state xs)) xs) ⊆ complete_state xs

fold_composition_state_inv

S (fold (;) t b) = S (foldl (;) b t)

S (fold (;) t (Skip (complete_state t))) = S (foldl (;) (Skip (complete_state t)) t)

permutation_fold_subset_complete_state

t ∈ set (permutations xs) ⟹ S (fold (;) t (Skip (complete_state t))) ⊆ complete_state xs

state_composition

x ∈ S a ⟹ x ∈ S (a ; b)

state_composition_1

x ∈ S p ⟹ x ∈ S (foldl (;) p (xs))

state_composition_2

x ∈ S a ⟹ x ∈ S (foldl (;) p (a#xs))

state_composition_3

x ∈ S a ⟹ x ∈ S (foldl (;) p (ys@a#xs))

complete_state_subset

complete_state xs ⊆ S (Skip (complete_state xs))

foldl_composition_preserves_state

S p ⊆ S (foldl (;) p xs)

Union_prop_1

⋃ (set (xs@[x])) = x ∪ ⋃ (set xs)

Union_prop_2

⋃ (xs ∪ {x}) = x ∪ ⋃ xs

fold_comp_prop1

xs ≠ [ ] ⟹ foldl (;) x xs = foldl (;) (x ; Skip (S x)) xs

fold_comp_prop2

xs ≠ [ ] ⟹ foldl (;) x xs = foldl (;) (x ; Skip (complete_state (x#xs))) xs

fold_comp_prop3

S (foldl (;) x xs) = complete_state (x # xs)

fold_comp_prop4

xs ≠ [ ] ⟹ foldl (;) x xs = foldl (;) (x ; Skip (complete_state (xs))) xs

perm_prop_1

(filter (p) xs) @ (filter (λx. ¬ p x) xs) ∈ set (permutations xs)

perm_prop_2

xs ∈ set (permutations ys) ⟹ map p xs ∈ set (permutations (map p ys))

Until_loop.thy

until_conncetion

until_loop a C b n = until_support a C b 0 n

until_decomposition

until_loop a C b (n + 1) ≡ a ; ((b/(-C))^{n + 1} ∪ (loop (b/(-C)) 0 n)) ∖ C

until_decomposition_2

until_loop a C b (n + 1) ≡ a ; ((b/(-C))^{n + 1}) ∖ C ∪ until_loop a C b n

until_def_lemma_3

until_loop a C b n ≡ a ; ((Skip (S (b/(-C))) / (Pre (b/(-C)))) ∪ (loop (b/(-C)) 1 n)) ∖ C

loop_choice1

until_loop a C b n ≡ ⋃ [a ; ((b / (- C))^{nat i})∖C. i ← [0..int n]]

loop_choice2

Range_p (until_loop a C b n) = ⋃ (set [Range_p (a ; ((b / (- C))^{nat i})∖C). i ← [0..int n]])

until_loop_feasible

all_feasible [a, b] ⟹ is_feasible (until_loop a C b n)

equiv_is_maintained_by_until_loop_2

a₁ ≡ a₂ ⟹ b₁ ≡ b₂ ⟹ S b₁ = S b₂ ⟹ all_feasible [b₁, b₂] ⟹ until_loop a₁ C b₁ n ≡ until_loop a₂ C b₂ n

until_decom

k<n ⟹ until_loop a C b n ≡ until_loop a C b n ∪ until_loop a C b k

range_until_loop_1

m<n ⟹ x ∉ Range_p (until_loop a C b n) ⟹ x ∉ Range_p (until_loop a C b m)

range_until_loop_2

m<n ⟹ x ∉ Range_p (until_loop a C b n) ⟹ x ∉ Range_p (until_support a C b s m)

loop_range

Range_p (until_loop a C b n) ⊆ C

split_front

until_loop (x ; a) C b n ≡ x ; until_loop a C b n

fail_until

until_loop a C b (n + 1) ≡ Fail {} ⟹ until_loop a C b n ≡ Fail {}

fail_until_2

k<n ⟹ until_loop a C b n ≡ Fail {} ⟹ until_loop a C b k ≡ Fail {}

loop_prop1

S (loop (b/(-C)) 0 n) = S b

loop_prop2

State (loop (b/(-C)) 0 n) = S b

loop_prop3

S (until_loop a C b n) = S a ∪ S b

loop_prop4

State (until_loop a C b n) = S (until_loop a C b n)

loop_prop5

State (until_loop a C b n) = S a ∪ S b

loop_prop6

until_loop (Skip D) FALSE (Skip D) n = Fail D

Until_support.thy

until_decomp_1

until_support a C b 0 n ≡ until_support a C b 0 0 ∪ until_support a C b (0 + 1) n

until_decomp_2

until_support a C b 0 (n + 1) ≡ until_support a C b 0 n ∪ until_support a C b (n + 1) (n + 1)

until_decomp_3

s < f ⟹ until_support a C b s f ≡ until_support a C b s s ∪ until_support a C b (s + 1) f

until_decomp_4

s < f ⟹ until_support a C b s (f + 1) ≡ until_support a C b (f + 1) (f + 1) ∪ until_support a C b s f

until_decomp_5

0 < k ⟹ k < n ⟹ until_support a C b 0 n ≡ until_support a C b 0 k ∪ until_support a C b (k + 1) n

until_decomp_6

s < k ⟹ k < f ⟹ until_support a C b s f ≡ until_support a C b s k ∪ until_support a C b (k + 1) f

until_decomp_7

s = f ⟹ until_support a C b s f ≡ a ; ((b / (- C))^f) ∖ C

until_support_feasible

all_feasible [a, b] ⟹ is_feasible (until_support a C b s f)

equiv_is_maintained_by_until_support_1

a₁ ≡ a₂ ⟹ b₁ ≡ b₂ ⟹ S b₁ = S b₂ ⟹ all_feasible [b₁, b₂] ⟹ until_support a₁ C b₁ s f ≡ until_support a₂ C b₂ s f

equiv_is_maintained_by_until_support_2

a₁ ≡ a₂ ⟹ b₁ ≡ b₂ ⟹ 0<s ⟹ all_feasible [b₁, b₂] ⟹ until_support a₁ C b₁ s f ≡ until_support a₂ C b₂ s f

bad_index_is_fail_support

f < s ⟹ until_support a C b s f ≡ Fail {}

bad_index_range_support

f < s ⟹ Range_p (until_support a C b s f) = {}

until_support_decomp

s<s’ ⟹ f’<f ⟹ until_support a C b s f ≡ until_support a C b s f ∪ until_support a C b s’ f’

Contract.thy

consequence_rule

post₁ ⊆ post₂ ⟹ Pre₂ ⊆ Pre₁ ⟹ is_correct 〈a_specification=〈State=Pre₁ ∪ Field post₂, Pre=Pre₁, post=post₁〉, a_implementation=b〉 ⟹ is_correct 〈a_specification=〈State=Pre₁ ∪ Field post₂, Pre=Pre₂, post=post₂〉, a_implementation=b〉