section ‹Set Interface›
theory IICF_Set
imports "../../Sepref"
begin
subsection ‹Operations›
context
notes [simp] = IS_LEFT_UNIQUE_def
begin
context
fixes t :: "nat"
begin
definition "mop_set_empty = SPECT [ {} ↦ enat t ]"
lemma mop_set_empty: "tt ≤ lst (SPECT [ {} ↦ t ]) Q ⟹ tt
≤ lst (mop_set_empty) Q" unfolding mop_set_empty_def by simp
sepref_register "mop_set_empty"
print_theorems
end
context
fixes t :: "'c set ⇒ nat"
begin
definition "mop_set_isempty S = SPECT [ S={} ↦ t S ]"
lemma mop_set_isempty: "tt ≤ lst (SPECT [ S={} ↦ t S ]) Q
⟹ tt ≤ lst (mop_set_isempty S) Q" unfolding mop_set_isempty_def by simp
sepref_register "mop_set_isempty"
print_theorems
end
context
fixes t :: "'c set ⇒ nat"
begin
definition "mop_set_pick S = do { ASSERT (S≠{}); SPECT (emb (λx. x∈S) (t S)) }"
lemma mop_set_pick: "tt ≤ lst (SPECT (emb (λx. x∈S) (t S))) Q
⟹ S ≠ {} ⟹ tt ≤ lst (mop_set_pick S) Q" unfolding mop_set_pick_def by simp
thm progress_rules
lemma progress_mop_set_pick[progress_rules]: "t S > 0 ⟹ progress (mop_set_pick S)"
unfolding mop_set_pick_def by (auto intro!: progress_rules simp add: zero_enat_def)
sepref_register "mop_set_pick"
print_theorems
end
context
fixes t :: "'c set ⇒ nat"
begin
definition "mop_set_pick_extract S = do { ASSERT (S≠{}); SPECT (emb (λ(x,C). x∈S ∧ C=S-{x}) (t S)) }"
lemma mop_set_pick_extract: "tt ≤ lst (SPECT (emb (λ(x,C). x∈S ∧ C=S-{x}) (t S))) Q
⟹ S ≠ {} ⟹ tt ≤ lst (mop_set_pick_extract S) Q" unfolding mop_set_pick_extract_def by simp
thm progress_rules
lemma progress_mop_set_pick_extract[progress_rules]: "t S > 0 ⟹ progress (mop_set_pick_extract S)"
unfolding mop_set_pick_extract_def by (auto intro!: progress_rules simp add: zero_enat_def)
sepref_register "mop_set_pick_extract"
print_theorems
end
context
fixes t:: "'a set ⇒ nat"
begin
definition "mop_set_member x S = SPECT [ x ∈ S ↦ enat (t S) ]"
sepref_register "mop_set_member"
print_theorems
end
context
fixes t :: "'c set ⇒ nat"
begin
definition "mop_set_del S x = SPECT [ S - {x} ↦ (t S)]"
lemma mop_set_del: "tt ≤ lst (SPECT [ S - {x} ↦ (t S)]) Q
⟹ tt ≤ lst (mop_set_del S x) Q" unfolding mop_set_del_def by simp
lemma progress_mop_set_del[progress_rules]: "t S > 0 ⟹ progress (mop_set_del S x)"
unfolding mop_set_del_def by (auto intro: progress_rules simp add: zero_enat_def)
sepref_register "mop_set_del"
print_theorems
end
context
fixes t :: "'c set ⇒ nat"
begin
definition "mop_set_insert x S = SPECT [insert x S ↦ t S]"
lemma mop_set_insert: "tt ≤ lst (SPECT [ (insert x S) ↦ t S]) Q ⟹
tt ≤ lst (mop_set_insert x S) Q" unfolding mop_set_insert_def by simp
sepref_register "mop_set_insert"
print_theorems
end
end
subsection ‹Patterns›
end