Theory Complementation_Implement
section ‹Complementation Implementation›
theory Complementation_Implement
imports
"Transition_Systems_and_Automata.NBA_Implement"
"Complementation"
begin
unbundle lattice_syntax
type_synonym item = "nat × bool"
type_synonym 'state items = "'state ⇀ item"
type_synonym state = "(nat × item) list"
abbreviation "item_rel ≡ nat_rel ×⇩r bool_rel"
abbreviation "state_rel ≡ ⟨nat_rel, item_rel⟩ list_map_rel"
abbreviation "pred A a q ≡ {p. q ∈ transition A a p}"
subsection ‹Phase 1›
definition cs_lr :: "'state items ⇒ 'state lr" where
"cs_lr f ≡ map_option fst ∘ f"
definition cs_st :: "'state items ⇒ 'state st" where
"cs_st f ≡ f -` Some ` snd -` {True}"
abbreviation cs_abs :: "'state items ⇒ 'state cs" where
"cs_abs f ≡ (cs_lr f, cs_st f)"
definition cs_rep :: "'state cs ⇒ 'state items" where
"cs_rep ≡ λ (g, P) p. map_option (λ k. (k, p ∈ P)) (g p)"
lemma cs_abs_rep[simp]: "cs_rep (cs_abs f) = f"
proof
show "cs_rep (cs_abs f) x = f x" for x
unfolding cs_lr_def cs_st_def cs_rep_def by (cases "f x") (force+)
qed
lemma cs_rep_lr[simp]: "cs_lr (cs_rep (g, P)) = g"
proof
show "cs_lr (cs_rep (g, P)) x = g x" for x
unfolding cs_rep_def cs_lr_def by (cases "g x") (auto)
qed
lemma cs_rep_st[simp]: "cs_st (cs_rep (g, P)) = P ∩ dom g"
unfolding cs_rep_def cs_st_def by force
lemma cs_lr_dom[simp]: "dom (cs_lr f) = dom f" unfolding cs_lr_def by simp
lemma cs_lr_apply[simp]:
assumes "p ∈ dom f"
shows "the (cs_lr f p) = fst (the (f p))"
using assms unfolding cs_lr_def by auto
lemma cs_rep_dom[simp]: "dom (cs_rep (g, P)) = dom g" unfolding cs_rep_def by auto
lemma cs_rep_apply[simp]:
assumes "p ∈ dom f"
shows "fst (the (cs_rep (f, P) p)) = the (f p)"
using assms unfolding cs_rep_def by auto
abbreviation cs_rel :: "('state items × 'state cs) set" where
"cs_rel ≡ br cs_abs top"
lemma cs_rel_inv_single_valued: "single_valued (cs_rel¯)"
by (auto intro!: inj_onI) (metis cs_abs_rep)
definition refresh_1 :: "'state items ⇒ 'state items" where
"refresh_1 f ≡ if True ∈ snd ` ran f then f else map_option (apsnd top) ∘ f"
definition ranks_1 ::
"('label, 'state) nba ⇒ 'label ⇒ 'state items ⇒ 'state items set" where
"ranks_1 A a f ≡ {g.
dom g = ⋃((transition A a) ` (dom f)) ∧
(∀ p ∈ dom f. ∀ q ∈ transition A a p. fst (the (g q)) ≤ fst (the (f p))) ∧
(∀ q ∈ dom g. accepting A q ⟶ even (fst (the (g q)))) ∧
cs_st g = {q ∈ ⋃((transition A a) ` (cs_st f)). even (fst (the (g q)))}}"
definition complement_succ_1 ::
"('label, 'state) nba ⇒ 'label ⇒ 'state items ⇒ 'state items set" where
"complement_succ_1 A a = ranks_1 A a ∘ refresh_1"
definition complement_1 :: "('label, 'state) nba ⇒ ('label, 'state items) nba" where
"complement_1 A ≡ nba
(alphabet A)
({const (Some (2 * card (nodes A), False)) |` initial A})
(complement_succ_1 A)
(λ f. cs_st f = {})"
lemma refresh_1_dom[simp]: "dom (refresh_1 f) = dom f" unfolding refresh_1_def by simp
lemma refresh_1_apply[simp]: "fst (the (refresh_1 f p)) = fst (the (f p))"
unfolding refresh_1_def by (cases "f p") (auto)
lemma refresh_1_cs_st[simp]: "cs_st (refresh_1 f) = (if cs_st f = {} then dom f else cs_st f)"
unfolding refresh_1_def cs_st_def ran_def image_def vimage_def by auto
lemma complement_succ_1_abs:
assumes "g ∈ complement_succ_1 A a f"
shows "cs_abs g ∈ complement_succ A a (cs_abs f)"
unfolding complement_succ_def
proof (simp, rule)
have 1:
"dom g = ⋃((transition A a) ` (dom f))"
"∀ p ∈ dom f. ∀ q ∈ transition A a p. fst (the (g q)) ≤ fst (the (f p))"
"∀ p ∈ dom g. accepting A p ⟶ even (fst (the (g p)))"
using assms unfolding complement_succ_1_def ranks_1_def by simp_all
show "cs_lr g ∈ lr_succ A a (cs_lr f)"
unfolding lr_succ_def
proof (intro CollectI conjI ballI impI)
show "dom (cs_lr g) = ⋃ (transition A a ` dom (cs_lr f))" using 1 by simp
next
fix p q
assume 2: "p ∈ dom (cs_lr f)" "q ∈ transition A a p"
have 3: "q ∈ dom (cs_lr g)" using 1 2 by auto
show "the (cs_lr g q) ≤ the (cs_lr f p)" using 1 2 3 by simp
next
fix p
assume 2: "p ∈ dom (cs_lr g)" "accepting A p"
show "even (the (cs_lr g p))" using 1 2 by auto
qed
have 2: "cs_st g = {q ∈ ⋃ (transition A a ` cs_st (refresh_1 f)). even (fst (the (g q)))}"
using assms unfolding complement_succ_1_def ranks_1_def by simp
show "cs_st g = st_succ A a (cs_lr g) (cs_st f)"
proof (cases "cs_st f = {}")
case True
have 3: "the (cs_lr g q) = fst (the (g q))" if "q ∈ ⋃((transition A a) ` (dom f))" for q
using that 1(1) by simp
show ?thesis using 2 3 unfolding st_succ_def refresh_1_cs_st True cs_lr_dom 1(1) by force
next
case False
have 3: "the (cs_lr g q) = fst (the (g q))" if "q ∈ ⋃((transition A a) ` (cs_st f))" for q
using that 1(1) by
(auto intro!: cs_lr_apply)
(metis IntE UN_iff cs_abs_rep cs_lr_dom cs_rep_st domD prod.collapse)
have "cs_st g = {q ∈ ⋃ (transition A a ` cs_st (refresh_1 f)). even (fst (the (g q)))}"
using 2 by this
also have "cs_st (refresh_1 f) = cs_st f" using False by simp
also have "{q ∈ ⋃((transition A a) ` (cs_st f)). even (fst (the (g q)))} =
{q ∈ ⋃((transition A a) ` (cs_st f)). even (the (cs_lr g q))}" using 3 by metis
also have "… = st_succ A a (cs_lr g) (cs_st f)" unfolding st_succ_def using False by simp
finally show ?thesis by this
qed
qed
lemma complement_succ_1_rep:
assumes "P ⊆ dom f" "(g, Q) ∈ complement_succ A a (f, P)"
shows "cs_rep (g, Q) ∈ complement_succ_1 A a (cs_rep (f, P))"
unfolding complement_succ_1_def ranks_1_def comp_apply
proof (intro CollectI conjI ballI impI)
have 1:
"dom g = ⋃((transition A a) ` (dom f))"
"∀ p ∈ dom f. ∀ q ∈ transition A a p. the (g q) ≤ the (f p)"
"∀ p ∈ dom g. accepting A p ⟶ even (the (g p))"
using assms(2) unfolding complement_succ_def lr_succ_def by simp_all
have 2: "Q = {q ∈ if P = {} then dom g else ⋃((transition A a) ` P). even (the (g q))}"
using assms(2) unfolding complement_succ_def st_succ_def by simp
have 3: "Q ⊆ dom g" unfolding 2 1(1) using assms(1) by auto
show "dom (cs_rep (g, Q)) = ⋃ (transition A a ` dom (refresh_1 (cs_rep (f, P))))" using 1 by simp
show "⋀ p q. p ∈ dom (refresh_1 (cs_rep (f, P))) ⟹ q ∈ transition A a p ⟹
fst (the (cs_rep (g, Q) q)) ≤ fst (the (refresh_1 (cs_rep (f, P)) p))"
using 1(1, 2) by (auto) (metis UN_I cs_rep_apply domI option.sel)
show "⋀ p. p ∈ dom (cs_rep (g, Q)) ⟹ accepting A p ⟹ even (fst (the (cs_rep (g, Q) p)))"
using 1(1, 3) by auto
show "cs_st (cs_rep (g, Q)) = {q ∈ ⋃ (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))).
even (fst (the (cs_rep (g, Q) q)))}"
proof (cases "P = {}")
case True
have "cs_st (cs_rep (g, Q)) = Q" using 3 by auto
also have "… = {q ∈ dom g. even (the (g q))}" unfolding 2 using True by auto
also have "… = {q ∈ dom g. even (fst (the (cs_rep (g, Q) q)))}" using cs_rep_apply by metis
also have "dom g = ⋃((transition A a) ` (dom f))" using 1(1) by this
also have "dom f = cs_st (refresh_1 (cs_rep (f, P)))" using True by simp
finally show ?thesis by this
next
case False
have 4: "fst (the (cs_rep (g, Q) q)) = the (g q)" if "q ∈ ⋃((transition A a) ` P)" for q
using 1(1) that assms(1) by (fast intro: cs_rep_apply)
have "cs_st (cs_rep (g, Q)) = Q" using 3 by auto
also have "… = {q ∈ ⋃((transition A a) ` P). even (the (g q))}" unfolding 2 using False by auto
also have "… = {q ∈ ⋃((transition A a) ` P). even (fst (the (cs_rep (g, Q) q)))}" using 4 by force
also have "P = (cs_st (refresh_1 (cs_rep (f, P))))" using assms(1) False by auto
finally show ?thesis by simp
qed
qed
lemma complement_succ_1_refine: "(complement_succ_1, complement_succ) ∈
Id → Id → cs_rel → ⟨cs_rel⟩ set_rel"
proof (clarsimp simp: br_set_rel_alt in_br_conv)
fix A :: "('a, 'b) nba"
fix a f
show "complement_succ A a (cs_abs f) = cs_abs ` complement_succ_1 A a f"
proof safe
fix g Q
assume 1: "(g, Q) ∈ complement_succ A a (cs_abs f)"
have 2: "Q ⊆ dom g"
using 1 unfolding complement_succ_def lr_succ_def st_succ_def
by (auto) (metis IntE cs_abs_rep cs_lr_dom cs_rep_st)
have 3: "cs_st f ⊆ dom (cs_lr f)" unfolding cs_st_def by auto
show "(g, Q) ∈ cs_abs ` complement_succ_1 A a f"
proof
show "(g, Q) = cs_abs (cs_rep (g, Q))" using 2 by auto
have "cs_rep (g, Q) ∈ complement_succ_1 A a (cs_rep (cs_abs f))"
using complement_succ_1_rep 3 1 by this
also have "cs_rep (cs_abs f) = f" by simp
finally show "cs_rep (g, Q) ∈ complement_succ_1 A a f" by this
qed
next
fix g
assume 1: "g ∈ complement_succ_1 A a f"
show "cs_abs g ∈ complement_succ A a (cs_abs f)" using complement_succ_1_abs 1 by this
qed
qed
lemma complement_1_refine: "(complement_1, complement) ∈ ⟨Id, Id⟩ nba_rel → ⟨Id, cs_rel⟩ nba_rel"
unfolding complement_1_def complement_def
proof parametricity
fix A B :: "('a, 'b) nba"
assume 1: "(A, B) ∈ ⟨Id, Id⟩ nba_rel"
have 2: "(const (Some (2 * card (nodes B), False)) |` initial B,
const (Some (2 * card (nodes B))) |` initial B, {}) ∈ cs_rel"
unfolding cs_lr_def cs_st_def in_br_conv by (force simp: restrict_map_def)
show "(complement_succ_1 A, complement_succ B) ∈ Id → cs_rel → ⟨cs_rel⟩ set_rel"
using complement_succ_1_refine 1 by parametricity auto
show "({const (Some (2 * card (nodes A), False)) |` initial A},
{const (Some (2 * card (nodes B))) |` initial B} × {{}}) ∈ ⟨cs_rel⟩ set_rel"
using 1 2 by simp parametricity
show "(λ f. cs_st f = {}, λ (f, P). P = {}) ∈ cs_rel → bool_rel" by (auto simp: in_br_conv)
qed
subsection ‹Phase 2›
definition ranks_2 :: "('label, 'state) nba ⇒ 'label ⇒ 'state items ⇒ 'state items set" where
"ranks_2 A a f ≡ {g.
dom g = ⋃((transition A a) ` (dom f)) ∧
(∀ q l d. g q = Some (l, d) ⟶
l ≤ ⨅ (fst ` Some -` f ` pred A a q) ∧
(d ⟷ ⨆ (snd ` Some -` f ` pred A a q) ∧ even l) ∧
(accepting A q ⟶ even l))}"
definition complement_succ_2 ::
"('label, 'state) nba ⇒ 'label ⇒ 'state items ⇒ 'state items set" where
"complement_succ_2 A a ≡ ranks_2 A a ∘ refresh_1"
definition complement_2 :: "('label, 'state) nba ⇒ ('label, 'state items) nba" where
"complement_2 A ≡ nba
(alphabet A)
({const (Some (2 * card (nodes A), False)) |` initial A})
(complement_succ_2 A)
(λ f. True ∉ snd ` ran f)"
lemma ranks_2_refine: "ranks_2 = ranks_1"
proof (intro ext)
fix A :: "('a, 'b) nba" and a f
show "ranks_2 A a f = ranks_1 A a f"
proof safe
fix g
assume 1: "g ∈ ranks_2 A a f"
have 2: "dom g = ⋃((transition A a) ` (dom f))" using 1 unfolding ranks_2_def by auto
have 3: "g q = Some (l, d) ⟹ l ≤ ⨅ (fst ` Some -` f ` pred A a q)" for q l d
using 1 unfolding ranks_2_def by auto
have 4: "g q = Some (l, d) ⟹ d ⟷ ⨆ (snd ` Some -` f ` pred A a q) ∧ even l" for q l d
using 1 unfolding ranks_2_def by auto
have 5: "g q = Some (l, d) ⟹ accepting A q ⟹ even l" for q l d
using 1 unfolding ranks_2_def by auto
show "g ∈ ranks_1 A a f"
unfolding ranks_1_def
proof (intro CollectI conjI ballI impI)
show "dom g = ⋃((transition A a) ` (dom f))" using 2 by this
next
fix p q
assume 10: "p ∈ dom f" "q ∈ transition A a p"
obtain k c where 11: "f p = Some (k, c)" using 10(1) by auto
have 12: "q ∈ dom g" using 10 2 by auto
obtain l d where 13: "g q = Some (l, d)" using 12 by auto
have "fst (the (g q)) = l" unfolding 13 by simp
also have "… ≤ ⨅ (fst ` Some -` f ` pred A a q)" using 3 13 by this
also have "… ≤ k"
proof (rule cInf_lower)
show "k ∈ fst ` Some -` f ` pred A a q" using 11 10(2) by force
show "bdd_below (fst ` Some -` f ` pred A a q)" by simp
qed
also have "… = fst (the (f p))" unfolding 11 by simp
finally show "fst (the (g q)) ≤ fst (the (f p))" by this
next
fix q
assume 10: "q ∈ dom g" "accepting A q"
show "even (fst (the (g q)))" using 10 5 by auto
next
show "cs_st g = {q ∈ ⋃((transition A a) ` (cs_st f)). even (fst (the (g q)))}"
proof
show "cs_st g ⊆ {q ∈ ⋃((transition A a) ` (cs_st f)). even (fst (the (g q)))}"
using 4 unfolding cs_st_def image_def vimage_def by auto metis+
show "{q ∈ ⋃((transition A a) ` (cs_st f)). even (fst (the (g q)))} ⊆ cs_st g"
proof safe
fix p q
assume 10: "even (fst (the (g q)))" "p ∈ cs_st f" "q ∈ transition A a p"
have 12: "q ∈ dom g" using 10 2 unfolding cs_st_def by auto
show "q ∈ cs_st g" using 10 4 12 unfolding cs_st_def image_def by force
qed
qed
qed
next
fix g
assume 1: "g ∈ ranks_1 A a f"
have 2: "dom g = ⋃((transition A a) ` (dom f))" using 1 unfolding ranks_1_def by auto
have 3: "⋀ p q. p ∈ dom f ⟹ q ∈ transition A a p ⟹ fst (the (g q)) ≤ fst (the (f p))"
using 1 unfolding ranks_1_def by auto
have 4: "⋀ q. q ∈ dom g ⟹ accepting A q ⟹ even (fst (the (g q)))"
using 1 unfolding ranks_1_def by auto
have 5: "cs_st g = {q ∈ ⋃((transition A a) ` (cs_st f)). even (fst (the (g q)))}"
using 1 unfolding ranks_1_def by auto
show "g ∈ ranks_2 A a f"
unfolding ranks_2_def
proof (intro CollectI conjI allI impI)
show "dom g = ⋃((transition A a) ` (dom f))" using 2 by this
next
fix q l d
assume 10: "g q = Some (l, d)"
have 11: "q ∈ dom g" using 10 by auto
show "l ≤ ⨅ (fst ` Some -` f ` pred A a q)"
proof (rule cInf_greatest)
show "fst ` Some -` f ` pred A a q ≠ {}" using 11 unfolding 2 image_def vimage_def by force
show "⋀ x. x ∈ fst ` Some -` f ` pred A a q ⟹ l ≤ x"
using 3 10 by (auto) (metis domI fst_conv option.sel)
qed
have "d ⟷ q ∈ cs_st g" unfolding cs_st_def by (force simp: 10)
also have "cs_st g = {q ∈ ⋃((transition A a) ` (cs_st f)). even (fst (the (g q)))}" using 5 by this
also have "q ∈ … ⟷ (∃ x ∈ cs_st f. q ∈ transition A a x) ∧ even l"
unfolding mem_Collect_eq 10 by simp
also have "… ⟷ ⨆ (snd ` Some -` f ` pred A a q) ∧ even l"
unfolding cs_st_def image_def vimage_def by auto metis+
finally show "d ⟷ ⨆ (snd ` Some -` f ` pred A a q) ∧ even l" by this
show "accepting A q ⟹ even l" using 4 10 11 by force
qed
qed
qed
lemma complement_2_refine: "(complement_2, complement_1) ∈ ⟨Id, Id⟩ nba_rel → ⟨Id, Id⟩ nba_rel"
unfolding complement_2_def complement_1_def complement_succ_2_def complement_succ_1_def
unfolding ranks_2_refine cs_st_def image_def vimage_def ran_def by auto
subsection ‹Phase 3›
definition bounds_3 :: "('label, 'state) nba ⇒ 'label ⇒ 'state items ⇒ 'state items" where
"bounds_3 A a f ≡ λ q. let S = Some -` f ` pred A a q in
if S = {} then None else Some (⨅(fst ` S), ⨆(snd ` S))"
definition items_3 :: "('label, 'state) nba ⇒ 'state ⇒ item ⇒ item set" where
"items_3 A p ≡ λ (k, c). {(l, c ∧ even l) |l. l ≤ k ∧ (accepting A p ⟶ even l)}"
definition get_3 :: "('label, 'state) nba ⇒ 'state items ⇒ ('state ⇀ item set)" where
"get_3 A f ≡ λ p. map_option (items_3 A p) (f p)"
definition complement_succ_3 ::
"('label, 'state) nba ⇒ 'label ⇒ 'state items ⇒ 'state items set" where
"complement_succ_3 A a ≡ expand_map ∘ get_3 A ∘ bounds_3 A a ∘ refresh_1"
definition complement_3 :: "('label, 'state) nba ⇒ ('label, 'state items) nba" where
"complement_3 A ≡ nba
(alphabet A)
({(Some ∘ (const (2 * card (nodes A), False))) |` initial A})
(complement_succ_3 A)
(λ f. ∀ (p, k, c) ∈ map_to_set f. ¬ c)"
lemma bounds_3_dom[simp]: "dom (bounds_3 A a f) = ⋃((transition A a) ` (dom f))"
unfolding bounds_3_def Let_def dom_def by (force split: if_splits)
lemma items_3_nonempty[intro!, simp]: "items_3 A p s ≠ {}" unfolding items_3_def by auto
lemma items_3_finite[intro!, simp]: "finite (items_3 A p s)"
unfolding items_3_def by (auto split: prod.splits)
lemma get_3_dom[simp]: "dom (get_3 A f) = dom f" unfolding get_3_def by (auto split: bind_splits)
lemma get_3_finite[intro, simp]: "S ∈ ran (get_3 A f) ⟹ finite S"
unfolding get_3_def ran_def by auto
lemma get_3_update[simp]: "get_3 A (f (p ↦ s)) = (get_3 A f) (p ↦ items_3 A p s)"
unfolding get_3_def by auto
lemma expand_map_get_bounds_3: "expand_map ∘ get_3 A ∘ bounds_3 A a = ranks_2 A a"
proof (intro ext set_eqI, unfold comp_apply)
fix f g
have 1: "(∀ x S y. get_3 A (bounds_3 A a f) x = Some S ⟶ g x = Some y ⟶ y ∈ S) ⟷
(∀ q S l d. get_3 A (bounds_3 A a f) q = Some S ⟶ g q = Some (l, d) ⟶ (l, d) ∈ S)"
by auto
have 2: "(∀ S. get_3 A (bounds_3 A a f) q = Some S ⟶ g q = Some (l, d) ⟶ (l, d) ∈ S) ⟷
(g q = Some (l, d) ⟶ l ≤ ⨅(fst ` (Some -` f ` pred A a q)) ∧
(d ⟷ ⨆(snd ` (Some -` f ` pred A a q)) ∧ even l) ∧ (accepting A q ⟶ even l))"
if 3: "dom g = ⋃((transition A a) ` (dom f))" for q l d
proof -
have 4: "q ∉ dom g" if "Some -` f ` pred A a q = {}" unfolding 3 using that by force
show ?thesis unfolding get_3_def items_3_def bounds_3_def Let_def using 4 by auto
qed
show "g ∈ expand_map (get_3 A (bounds_3 A a f)) ⟷ g ∈ ranks_2 A a f"
unfolding expand_map_alt_def ranks_2_def mem_Collect_eq
unfolding get_3_dom bounds_3_dom 1 using 2 by blast
qed
lemma complement_succ_3_refine: "complement_succ_3 = complement_succ_2"
unfolding complement_succ_3_def complement_succ_2_def expand_map_get_bounds_3 by rule
lemma complement_initial_3_refine: "{const (Some (2 * card (nodes A), False)) |` initial A} =
{(Some ∘ (const (2 * card (nodes A), False))) |` initial A}"
unfolding comp_apply by rule
lemma complement_accepting_3_refine: "True ∉ snd ` ran f ⟷ (∀ (p, k, c) ∈ map_to_set f. ¬ c)"
unfolding map_to_set_def ran_def by auto
lemma complement_3_refine: "(complement_3, complement_2) ∈ ⟨Id, Id⟩ nba_rel → ⟨Id, Id⟩ nba_rel"
unfolding complement_3_def complement_2_def
unfolding complement_succ_3_refine complement_initial_3_refine complement_accepting_3_refine
by auto
subsection ‹Phase 4›
definition items_4 :: "('label, 'state) nba ⇒ 'state ⇒ item ⇒ item set" where
"items_4 A p ≡ λ (k, c). {(l, c ∧ even l) |l. k ≤ Suc l ∧ l ≤ k ∧ (accepting A p ⟶ even l)}"
definition get_4 :: "('label, 'state) nba ⇒ 'state items ⇒ ('state ⇀ item set)" where
"get_4 A f ≡ λ p. map_option (items_4 A p) (f p)"
definition complement_succ_4 ::
"('label, 'state) nba ⇒ 'label ⇒ 'state items ⇒ 'state items set" where
"complement_succ_4 A a ≡ expand_map ∘ get_4 A ∘ bounds_3 A a ∘ refresh_1"
definition complement_4 :: "('label, 'state) nba ⇒ ('label, 'state items) nba" where
"complement_4 A ≡ nba
(alphabet A)
({(Some ∘ (const (2 * card (nodes A), False))) |` initial A})
(complement_succ_4 A)
(λ f. ∀ (p, k, c) ∈ map_to_set f. ¬ c)"
lemma get_4_dom[simp]: "dom (get_4 A f) = dom f" unfolding get_4_def by (auto split: bind_splits)
definition R :: "'state items rel" where
"R ≡ {(f, g).
dom f = dom g ∧
(∀ p ∈ dom f. fst (the (f p)) ≤ fst (the (g p))) ∧
(∀ p ∈ dom f. snd (the (f p)) ⟷ snd (the (g p)))}"
lemma bounds_R:
assumes "(f, g) ∈ R"
assumes "bounds_3 A a (refresh_1 f) p = Some (n, e)"
assumes "bounds_3 A a (refresh_1 g) p = Some (k, c)"
shows "n ≤ k" "e ⟷ c"
proof -
have 1:
"dom f = dom g"
"∀ p ∈ dom f. fst (the (f p)) ≤ fst (the (g p))"
"∀ p ∈ dom f. snd (the (f p)) ⟷ snd (the (g p))"
using assms(1) unfolding R_def by auto
have "n = ⨅(fst ` (Some -` refresh_1 f ` pred A a p))"
using assms(2) unfolding bounds_3_def by (auto simp: Let_def split: if_splits)
also have "fst ` Some -` refresh_1 f ` pred A a p = fst ` Some -` f ` pred A a p"
proof
show " fst ` Some -` refresh_1 f ` pred A a p ⊆ fst ` Some -` f ` pred A a p"
unfolding refresh_1_def image_def
by (auto simp: map_option_case split: option.split) (force)
show "fst ` Some -` f ` pred A a p ⊆ fst ` Some -` refresh_1 f ` pred A a p"
unfolding refresh_1_def image_def
by (auto simp: map_option_case split: option.split) (metis fst_conv option.sel)
qed
also have "… = fst ` Some -` f ` (pred A a p ∩ dom f)"
unfolding dom_def image_def Int_def by auto metis
also have "… = fst ` the ` f ` (pred A a p ∩ dom f)"
unfolding dom_def by force
also have "… = (fst ∘ the ∘ f) ` (pred A a p ∩ dom f)" by force
also have "⨅((fst ∘ the ∘ f) ` (pred A a p ∩ dom f)) ≤
⨅((fst ∘ the ∘ g) ` (pred A a p ∩ dom g))"
proof (rule cINF_mono)
show "pred A a p ∩ dom g ≠ {}"
using assms(2) 1(1) unfolding bounds_3_def refresh_1_def
by (auto simp: Let_def split: if_splits) (force+)
show "bdd_below ((fst ∘ the ∘ f) ` (pred A a p ∩ dom f))" by rule
show "∃ n ∈ pred A a p ∩ dom f. (fst ∘ the ∘ f) n ≤ (fst ∘ the ∘ g) m"
if "m ∈ pred A a p ∩ dom g" for m using 1 that by auto
qed
also have "(fst ∘ the ∘ g) ` (pred A a p ∩ dom g) = fst ` the ` g ` (pred A a p ∩ dom g)" by force
also have "… = fst ` Some -` g ` (pred A a p ∩ dom g)"
unfolding dom_def by force
also have "… = fst ` Some -` g ` pred A a p"
unfolding dom_def image_def Int_def by auto metis
also have "… = fst ` Some -` refresh_1 g ` pred A a p"
proof
show "fst ` Some -` g ` pred A a p ⊆ fst ` Some -` refresh_1 g ` pred A a p"
unfolding refresh_1_def image_def
by (auto simp: map_option_case split: option.split) (metis fst_conv option.sel)
show "fst ` Some -` refresh_1 g ` pred A a p ⊆ fst ` Some -` g ` pred A a p"
unfolding refresh_1_def image_def
by (auto simp: map_option_case split: option.split) (force)
qed
also have "⨅(fst ` (Some -` refresh_1 g ` pred A a p)) = k"
using assms(3) unfolding bounds_3_def by (auto simp: Let_def split: if_splits)
finally show "n ≤ k" by this
have "e ⟷ ⨆(snd ` (Some -` refresh_1 f ` pred A a p))"
using assms(2) unfolding bounds_3_def by (auto simp: Let_def split: if_splits)
also have "snd ` Some -` refresh_1 f ` pred A a p = snd ` Some -` refresh_1 f ` (pred A a p ∩ dom (refresh_1 f))"
unfolding dom_def image_def Int_def by auto metis
also have "… = snd ` the ` refresh_1 f ` (pred A a p ∩ dom (refresh_1 f))"
unfolding dom_def by force
also have "… = (snd ∘ the ∘ refresh_1 f) ` (pred A a p ∩ dom (refresh_1 f))" by force
also have "… = (snd ∘ the ∘ refresh_1 g) ` (pred A a p ∩ dom (refresh_1 g))"
proof (rule image_cong)
show "pred A a p ∩ dom (refresh_1 f) = pred A a p ∩ dom (refresh_1 g)"
unfolding refresh_1_dom 1(1) by rule
show "(snd ∘ the ∘ refresh_1 f) q ⟷ (snd ∘ the ∘ refresh_1 g) q"
if 2: "q ∈ pred A a p ∩ dom (refresh_1 g)" for q
proof
have 3: "∀ x ∈ ran f. ¬ snd x ⟹ (n, True) ∈ ran g ⟹ g q = Some (k, c) ⟹ c" for n k c
using 1(1, 3) unfolding dom_def ran_def
by (auto dest!: Collect_inj) (metis option.sel snd_conv)
have 4: "g q = Some (n, True) ⟹ f q = Some (k, c) ⟹ c" for n k c
using 1(3) unfolding dom_def by force
have 5: "∀ x ∈ ran g. ¬ snd x ⟹ (k, True) ∈ ran f ⟹ False" for k
using 1(1, 3) unfolding dom_def ran_def
by (auto dest!: Collect_inj) (metis option.sel snd_conv)
show "(snd ∘ the ∘ refresh_1 f) q ⟹ (snd ∘ the ∘ refresh_1 g) q"
using 1(1, 3) 2 3 unfolding refresh_1_def by (force split: if_splits)
show "(snd ∘ the ∘ refresh_1 g) q ⟹ (snd ∘ the ∘ refresh_1 f) q"
using 1(1, 3) 2 4 5 unfolding refresh_1_def
by (auto simp: map_option_case split: option.splits if_splits) (force+)
qed
qed
also have "… = snd ` the ` refresh_1 g ` (pred A a p ∩ dom (refresh_1 g))" by force
also have "… = snd ` Some -` refresh_1 g ` (pred A a p ∩ dom (refresh_1 g))"
unfolding dom_def by force
also have "… = snd ` Some -` refresh_1 g ` pred A a p"
unfolding dom_def image_def Int_def by auto metis
also have "⨆(snd ` (Some -` refresh_1 g ` pred A a p)) ⟷ c"
using assms(3) unfolding bounds_3_def by (auto simp: Let_def split: if_splits)
finally show "e ⟷ c" by this
qed
lemma complement_4_language_1: "language (complement_3 A) ⊆ language (complement_4 A)"
proof (rule simulation_language)
show "alphabet (complement_3 A) ⊆ alphabet (complement_4 A)"
unfolding complement_3_def complement_4_def by simp
show "∃ q ∈ initial (complement_4 A). (p, q) ∈ R" if "p ∈ initial (complement_3 A)" for p
using that unfolding complement_3_def complement_4_def R_def by simp
show "∃ g' ∈ transition (complement_4 A) a g. (f', g') ∈ R"
if "f' ∈ transition (complement_3 A) a f" "(f, g) ∈ R"
for a f f' g
proof -
have 1: "f' ∈ expand_map (get_3 A (bounds_3 A a (refresh_1 f)))"
using that(1) unfolding complement_3_def complement_succ_3_def by auto
have 2:
"dom f = dom g"
"∀ p ∈ dom f. fst (the (f p)) ≤ fst (the (g p))"
"∀ p ∈ dom f. snd (the (f p)) ⟷ snd (the (g p))"
using that(2) unfolding R_def by auto
have "dom f' = dom (get_3 A (bounds_3 A a (refresh_1 f)))" using expand_map_dom 1 by this
also have "… = dom (bounds_3 A a (refresh_1 f))" by simp
finally have 3: "dom f' = dom (bounds_3 A a (refresh_1 f))" by this
define g' where "g' p ≡ do
{
(k, c) ← bounds_3 A a (refresh_1 g) p;
(l, d) ← f' p;
Some (if even k = even l then k else k - 1, d)
}" for p
have 4: "g' p = do
{
kc ← bounds_3 A a (refresh_1 g) p;
ld ← f' p;
Some (if even (fst kc) = even (fst ld) then fst kc else fst kc - 1, snd ld)
}" for p unfolding g'_def case_prod_beta by rule
have "dom g' = dom (bounds_3 A a (refresh_1 g)) ∩ dom f'" using 4 bind_eq_Some_conv by fastforce
also have "… = dom f'" using 2 3 by simp
finally have 5: "dom g' = dom f'" by this
have 6: "(l, d) ∈ items_3 A p (k, c)"
if "bounds_3 A a (refresh_1 f) p = Some (k, c)" "f' p = Some (l, d)" for p k c l d
using 1 that unfolding expand_map_alt_def get_3_def by blast
show ?thesis
unfolding complement_4_def nba.sel complement_succ_4_def comp_apply
proof
show "(f', g') ∈ R"
unfolding R_def mem_Collect_eq prod.case
proof (intro conjI ballI)
show "dom f' = dom g'" using 5 by rule
next
fix p
assume 10: "p ∈ dom f'"
have 11: "p ∈ dom (bounds_3 A a (refresh_1 g))" using 2(1) 3 10 by simp
obtain k c where 12: "bounds_3 A a (refresh_1 g) p = Some (k, c)" using 11 by fast
obtain l d where 13: "f' p = Some (l, d)" using 10 by auto
obtain n e where 14: "bounds_3 A a (refresh_1 f) p = Some (n, e)" using 10 3 by fast
have 15: "(l, d) ∈ items_3 A p (n, e)" using 6 14 13 by this
have 16: "n ≤ k" using bounds_R(1) that(2) 14 12 by this
have 17: "l ≤ k" using 15 16 unfolding items_3_def by simp
have 18: "even k ⟷ odd l ⟹ l ≤ k ⟹ l ≤ k - 1" by presburger
have 19: "e ⟷ c" using bounds_R(2) that(2) 14 12 by this
show "fst (the (f' p)) ≤ fst (the (g' p))" using 17 18 unfolding 4 12 13 by simp
show "snd (the (f' p)) ⟷ snd (the (g' p))" using 19 unfolding 4 12 13 by simp
qed
show "g' ∈ expand_map (get_4 A (bounds_3 A a (refresh_1 g)))"
unfolding expand_map_alt_def mem_Collect_eq
proof (intro conjI allI impI)
show "dom g' = dom (get_4 A (bounds_3 A a (refresh_1 g)))" using 2(1) 3 5 by simp
fix p S xy
assume 10: "get_4 A (bounds_3 A a (refresh_1 g)) p = Some S"
assume 11: "g' p = Some xy"
obtain k c where 12: "bounds_3 A a (refresh_1 g) p = Some (k, c)" "S = items_4 A p (k, c)"
using 10 unfolding get_4_def by auto
obtain l d where 13: "f' p = Some (l, d)" "xy = (if even k ⟷ even l then k else k - 1, d)"
using 11 12 unfolding g'_def by (auto split: bind_splits)
obtain n e where 14: "bounds_3 A a (refresh_1 f) p = Some (n, e)" using 13(1) 3 by fast
have 15: "(l, d) ∈ items_3 A p (n, e)" using 6 14 13(1) by this
have 16: "n ≤ k" using bounds_R(1) that(2) 14 12(1) by this
have 17: "e ⟷ c" using bounds_R(2) that(2) 14 12(1) by this
show "xy ∈ S" using 15 16 17 unfolding 12(2) 13(2) items_3_def items_4_def by auto
qed
qed
qed
show "⋀ p q. (p, q) ∈ R ⟹ accepting (complement_3 A) p ⟹ accepting (complement_4 A) q"
unfolding complement_3_def complement_4_def R_def map_to_set_def
by (auto) (metis domIff eq_snd_iff option.exhaust_sel option.sel)
qed
lemma complement_4_less: "complement_4 A ≤ complement_3 A"
unfolding less_eq_nba_def
unfolding complement_4_def complement_3_def nba.sel
unfolding complement_succ_4_def complement_succ_3_def
proof (safe intro!: le_funI, unfold comp_apply)
fix a f g
assume "g ∈ expand_map (get_4 A (bounds_3 A a (refresh_1 f)))"
then show "g ∈ expand_map (get_3 A (bounds_3 A a (refresh_1 f)))"
unfolding get_4_def get_3_def items_4_def items_3_def expand_map_alt_def by blast
qed
lemma complement_4_language_2: "language (complement_4 A) ⊆ language (complement_3 A)"
using language_mono complement_4_less by (auto dest: monoD)
lemma complement_4_language: "language (complement_3 A) = language (complement_4 A)"
using complement_4_language_1 complement_4_language_2 by blast
lemma complement_4_finite[simp]:
assumes "finite (nodes A)"
shows "finite (nodes (complement_4 A))"
proof -
have "(nodes (complement_3 A), nodes (complement_2 A)) ∈ ⟨Id⟩ set_rel"
using complement_3_refine by parametricity auto
also have "(nodes (complement_2 A), nodes (complement_1 A)) ∈ ⟨Id⟩ set_rel"
using complement_2_refine by parametricity auto
also have "(nodes (complement_1 A), nodes (complement A)) ∈ ⟨cs_rel⟩ set_rel"
using complement_1_refine by parametricity auto
finally have 1: "(nodes (complement_3 A), nodes (complement A)) ∈ ⟨cs_rel⟩ set_rel" by simp
have 2: "finite (nodes (complement A))" using complement_finite assms(1) by this
have 3: "finite (nodes (complement_3 A))"
using finite_set_rel_transfer_back 1 cs_rel_inv_single_valued 2 by this
have 4: "nodes (complement_4 A) ⊆ nodes (complement_3 A)"
using nodes_mono complement_4_less by (auto dest: monoD)
show "finite (nodes (complement_4 A))" using finite_subset 4 3 by this
qed
lemma complement_4_correct:
assumes "finite (nodes A)"
shows "language (complement_4 A) = streams (alphabet A) - language A"
proof -
have "language (complement_4 A) = language (complement_3 A)"
using complement_4_language by rule
also have "(language (complement_3 A), language (complement_2 A)) ∈ ⟨⟨Id⟩ stream_rel⟩ set_rel"
using complement_3_refine by parametricity auto
also have "(language (complement_2 A), language (complement_1 A)) ∈ ⟨⟨Id⟩ stream_rel⟩ set_rel"
using complement_2_refine by parametricity auto
also have "(language (complement_1 A), language (complement A)) ∈ ⟨⟨Id⟩ stream_rel⟩ set_rel"
using complement_1_refine by parametricity auto
also have "language (complement A) = streams (alphabet A) - language A"
using complement_language assms(1) by this
finally show "language (complement_4 A) = streams (alphabet A) - language A" by simp
qed
subsection ‹Phase 5›
definition refresh_5 :: "'state items ⇒ 'state items nres" where
"refresh_5 f ≡ if ∃ (p, k, c) ∈ map_to_set f. c
then RETURN f
else do
{
ASSUME (finite (dom f));
FOREACH (map_to_set f) (λ (p, k, c) m. do
{
ASSERT (p ∉ dom m);
RETURN (m (p ↦ (k, True)))
}
) Map.empty
}"
definition merge_5 :: "item ⇒ item option ⇒ item" where
"merge_5 ≡ λ (k, c). λ None ⇒ (k, c) | Some (l, d) ⇒ (k ⊓ l, c ⊔ d)"
definition bounds_5 :: "('label, 'state) nba ⇒ 'label ⇒ 'state items ⇒ 'state items nres" where
"bounds_5 A a f ≡ do
{
ASSUME (finite (dom f));
ASSUME (∀ p. finite (transition A a p));
FOREACH (map_to_set f) (λ (p, s) m.
FOREACH (transition A a p) (λ q f.
RETURN (f (q ↦ merge_5 s (f q))))
m)
Map.empty
}"
definition items_5 :: "('label, 'state) nba ⇒ 'state ⇒ item ⇒ item set" where
"items_5 A p ≡ λ (k, c). do
{
let values = if accepting A p then Set.filter even {k - 1 .. k} else {k - 1 .. k};
let item = λ l. (l, c ∧ even l);
item ` values
}"
definition get_5 :: "('label, 'state) nba ⇒ 'state items ⇒ ('state ⇀ item set)" where
"get_5 A f ≡ λ p. map_option (items_5 A p) (f p)"
definition expand_5 :: "('a ⇀ 'b set) ⇒ ('a ⇀ 'b) set nres" where
"expand_5 f ≡ FOREACH (map_to_set f) (λ (x, S) X. do {
ASSERT (∀ g ∈ X. x ∉ dom g);
ASSERT (∀ a ∈ S. ∀ b ∈ S. a ≠ b ⟶ (λ y. (λ g. g (x ↦ y)) ` X) a ∩ (λ y. (λ g. g (x ↦ y)) ` X) b = {});
RETURN (⋃ y ∈ S. (λ g. g (x ↦ y)) ` X)
}) {Map.empty}"
definition complement_succ_5 ::
"('label, 'state) nba ⇒ 'label ⇒ 'state items ⇒ 'state items set nres" where
"complement_succ_5 A a f ≡ do
{
f ← refresh_5 f;
f ← bounds_5 A a f;
ASSUME (finite (dom f));
expand_5 (get_5 A f)
}"
lemma bounds_3_empty: "bounds_3 A a Map.empty = Map.empty"
unfolding bounds_3_def Let_def by auto
lemma bounds_3_update: "bounds_3 A a (f (p ↦ s)) =
override_on (bounds_3 A a f) (Some ∘ merge_5 s ∘ bounds_3 A a (f (p := None))) (transition A a p)"
proof
note fun_upd_image[simp]
fix q
show "bounds_3 A a (f (p ↦ s)) q =
override_on (bounds_3 A a f) (Some ∘ merge_5 s ∘ bounds_3 A a (f (p := None))) (transition A a p) q"
proof (cases "q ∈ transition A a p")
case True
define S where "S ≡ Some -` f ` (pred A a q - {p})"
have 1: "Some -` f (p := Some s) ` pred A a q = insert s S" using True unfolding S_def by auto
have 2: "Some -` f (p := None) ` pred A a q = S" unfolding S_def by auto
have "bounds_3 A a (f (p ↦ s)) q = Some (⨅(fst ` (insert s S)), ⨆(snd ` (insert s S)))"
unfolding bounds_3_def 1 by simp
also have "… = Some (merge_5 s (bounds_3 A a (f (p := None)) q))"
unfolding 2 bounds_3_def merge_5_def by (cases s) (simp_all add: cInf_insert)
also have "… = override_on (bounds_3 A a f) (Some ∘ merge_5 s ∘ bounds_3 A a (f (p := None)))
(transition A a p) q" using True by simp
finally show ?thesis by this
next
case False
then have "pred A a q ∩ {x. x ≠ p} = pred A a q"
by auto
with False show ?thesis by (simp add: bounds_3_def)
qed
qed
lemma refresh_5_refine: "(refresh_5, λ f. RETURN (refresh_1 f)) ∈ Id → ⟨Id⟩ nres_rel"
proof safe
fix f :: "'a ⇒ item option"
have 1: "(∃ (p, k, c) ∈ map_to_set f. c) ⟷ True ∈ snd ` ran f"
unfolding image_def map_to_set_def ran_def by force
show "(refresh_5 f, RETURN (refresh_1 f)) ∈ ⟨Id⟩ nres_rel"
unfolding refresh_5_def refresh_1_def 1
by (refine_vcg FOREACH_rule_map_eq[where X = "λ m. map_option (apsnd ⊤) ∘ m"]) (auto)
qed
lemma bounds_5_refine: "(bounds_5 A a, λ f. RETURN (bounds_3 A a f)) ∈ Id → ⟨Id⟩ nres_rel"
unfolding bounds_5_def by
(refine_vcg FOREACH_rule_map_eq[where X = "bounds_3 A a"] FOREACH_rule_insert_eq)
(auto simp: override_on_insert bounds_3_empty bounds_3_update)
lemma items_5_refine: "items_5 = items_4"
unfolding items_5_def items_4_def by (intro ext) (auto split: if_splits)
lemma get_5_refine: "get_5 = get_4"
unfolding get_5_def get_4_def items_5_refine by rule
lemma expand_5_refine: "(expand_5 f, ASSERT (finite (dom f)) ⪢ RETURN (expand_map f)) ∈ ⟨Id⟩ nres_rel"
unfolding expand_5_def
by (refine_vcg FOREACH_rule_map_eq[where X = expand_map]) (auto dest!: expand_map_dom map_upd_eqD1)
lemma complement_succ_5_refine: "(complement_succ_5, RETURN ∘∘∘ complement_succ_4) ∈
Id → Id → Id → ⟨Id⟩ nres_rel"
unfolding complement_succ_5_def complement_succ_4_def get_5_refine comp_apply
by (refine_vcg vcg1[OF refresh_5_refine] vcg1[OF bounds_5_refine] vcg0[OF expand_5_refine]) (auto)
subsection ‹Phase 6›
definition expand_map_get_6 :: "('label, 'state) nba ⇒ 'state items ⇒ 'state items set nres" where
"expand_map_get_6 A f ≡ FOREACH (map_to_set f) (λ (k, v) X. do {
ASSERT (∀ g ∈ X. k ∉ dom g);
ASSERT (∀ a ∈ (items_5 A k v). ∀ b ∈ (items_5 A k v). a ≠ b ⟶ (λ y. (λ g. g (k ↦ y)) ` X) a ∩ (λ y. (λ g. g (k ↦ y)) ` X) b = {});
RETURN (⋃ y ∈ items_5 A k v. (λ g. g (k ↦ y)) ` X)
}) {Map.empty}"
lemma expand_map_get_6_refine: "(expand_map_get_6, expand_5 ∘∘ get_5) ∈ Id → Id → ⟨Id⟩ nres_rel"
unfolding expand_map_get_6_def expand_5_def get_5_def by (auto intro: FOREACH_rule_map_map[param_fo])
definition complement_succ_6 ::
"('label, 'state) nba ⇒ 'label ⇒ 'state items ⇒ 'state items set nres" where
"complement_succ_6 A a f ≡ do
{
f ← refresh_5 f;
f ← bounds_5 A a f;
ASSUME (finite (dom f));
expand_map_get_6 A f
}"
lemma complement_succ_6_refine:
"(complement_succ_6, complement_succ_5) ∈ Id → Id → Id → ⟨Id⟩ nres_rel"
unfolding complement_succ_6_def complement_succ_5_def
by (refine_vcg vcg2[OF expand_map_get_6_refine]) (auto intro: refine_IdI)
subsection ‹Phase 7›
interpretation autoref_syn by this
context
fixes fi f
assumes fi[autoref_rules]: "(fi, f) ∈ state_rel"
begin
private lemma [simp]: "finite (dom f)"
using list_map_rel_finite fi unfolding finite_map_rel_def by force
schematic_goal refresh_7: "(?f :: ?'a, refresh_5 f) ∈ ?R"
unfolding refresh_5_def by (autoref_monadic (plain))
end
concrete_definition refresh_7 uses refresh_7
lemma refresh_7_refine: "(λ f. RETURN (refresh_7 f), refresh_5) ∈ state_rel → ⟨state_rel⟩ nres_rel"
using refresh_7.refine by fast
context
fixes A :: "('label, nat) nba"
fixes succi a fi f
assumes succi[autoref_rules]: "(succi, transition A a) ∈ nat_rel → ⟨nat_rel⟩ list_set_rel"
assumes fi[autoref_rules]: "(fi, f) ∈ state_rel"
begin
private lemma [simp]: "finite (transition A a p)"
using list_set_rel_finite succi[param_fo] unfolding finite_set_rel_def by blast
private lemma [simp]: "finite (dom f)" using fi by force
private lemma [autoref_op_pat]: "transition A a ≡ OP (transition A a)" by simp
private lemma [autoref_rules]: "(min, min) ∈ nat_rel → nat_rel → nat_rel" by simp
schematic_goal bounds_7:
notes ty_REL[where R = "⟨nat_rel, item_rel⟩ dflt_ahm_rel", autoref_tyrel]
shows "(?f :: ?'a, bounds_5 A a f) ∈ ?R"
unfolding bounds_5_def merge_5_def sup_bool_def inf_nat_def by (autoref_monadic (plain))
end
concrete_definition bounds_7 uses bounds_7
lemma bounds_7_refine: "(si, transition A a) ∈ nat_rel → ⟨nat_rel⟩ list_set_rel ⟹
(λ p. RETURN (bounds_7 si p), bounds_5 A a) ∈
state_rel → ⟨⟨nat_rel, item_rel⟩ dflt_ahm_rel⟩ nres_rel"
using bounds_7.refine by auto
context
fixes A :: "('label, nat) nba"
fixes acci
assumes [autoref_rules]: "(acci, accepting A) ∈ nat_rel → bool_rel"
begin
private lemma [autoref_op_pat]: "accepting A ≡ OP (accepting A)" by simp
private lemma [autoref_rules]: "((dvd), (dvd)) ∈ nat_rel → nat_rel → bool_rel" by simp
private lemma [autoref_rules]: "(λ k l. upt k (Suc l), atLeastAtMost) ∈
nat_rel → nat_rel → ⟨nat_rel⟩ list_set_rel"
by (auto simp: list_set_rel_def in_br_conv)
schematic_goal items_7: "(?f :: ?'a, items_5 A) ∈ ?R"
unfolding items_5_def Let_def Set.filter_def by autoref
end
concrete_definition items_7 uses items_7
context
fixes A :: "('label, nat) nba"
fixes ai
fixes fi f
assumes ai: "(ai, accepting A) ∈ nat_rel → bool_rel"
assumes fi[autoref_rules]: "(fi, f) ∈ ⟨nat_rel, item_rel⟩ dflt_ahm_rel"
begin
private lemma [simp]: "finite (dom f)"
using dflt_ahm_rel_finite_nat fi unfolding finite_map_rel_def by force
private lemma [simp]:
assumes "⋀ m. m ∈ S ⟹ x ∉ dom m"
shows "inj_on (λ m. m (x ↦ y)) S"
using assms unfolding dom_def inj_on_def by (auto) (metis fun_upd_triv fun_upd_upd)
private lemmas [simp] = op_map_update_def[abs_def]
private lemma [autoref_op_pat]: "items_5 A ≡ OP (items_5 A)" by simp
private lemmas [autoref_rules] = items_7.refine[OF ai]
schematic_goal expand_map_get_7: "(?f, expand_map_get_6 A f) ∈
⟨⟨state_rel⟩ list_set_rel⟩ nres_rel"
unfolding expand_map_get_6_def by (autoref_monadic (plain))
end
concrete_definition expand_map_get_7 uses expand_map_get_7
lemma expand_map_get_7_refine:
assumes "(ai, accepting A) ∈ nat_rel → bool_rel"
shows "(λ fi. RETURN (expand_map_get_7 ai fi),
λ f. ASSUME (finite (dom f)) ⪢ expand_map_get_6 A f) ∈
⟨nat_rel, item_rel⟩ dflt_ahm_rel → ⟨⟨state_rel⟩ list_set_rel⟩ nres_rel"
using expand_map_get_7.refine[OF assms] by auto
context
fixes A :: "('label, nat) nba"
fixes a :: "'label"
fixes p :: "nat items"
fixes Ai
fixes ai
fixes pi
assumes Ai: "(Ai, A) ∈ ⟨Id, Id⟩ nbai_nba_rel"
assumes ai: "(ai, a) ∈ Id"
assumes pi[autoref_rules]: "(pi, p) ∈ state_rel"
begin
private lemmas succi = nbai_nba_param(4)[THEN fun_relD, OF Ai, THEN fun_relD, OF ai]
private lemmas acceptingi = nbai_nba_param(5)[THEN fun_relD, OF Ai]
private lemma [autoref_op_pat]: "(λ g. ASSUME (finite (dom g)) ⪢ expand_map_get_6 A g) ≡
OP (λ g. ASSUME (finite (dom g)) ⪢ expand_map_get_6 A g)" by simp
private lemma [autoref_op_pat]: "bounds_5 A a ≡ OP (bounds_5 A a)" by simp
private lemmas [autoref_rules] =
refresh_7_refine
bounds_7_refine[OF succi]
expand_map_get_7_refine[OF acceptingi]
schematic_goal complement_succ_7: "(?f :: ?'a, complement_succ_6 A a p) ∈ ?R"
unfolding complement_succ_6_def by (autoref_monadic (plain))
end
concrete_definition complement_succ_7 uses complement_succ_7
lemma complement_succ_7_refine:
"(RETURN ∘∘∘ complement_succ_7, complement_succ_6) ∈
⟨Id, Id⟩ nbai_nba_rel → Id → state_rel →
⟨⟨state_rel⟩ list_set_rel⟩ nres_rel"
using complement_succ_7.refine unfolding comp_apply by parametricity
context
fixes A :: "('label, nat) nba"
fixes Ai
fixes n ni :: nat
assumes Ai: "(Ai, A) ∈ ⟨Id, Id⟩ nbai_nba_rel"
assumes ni[autoref_rules]: "(ni, n) ∈ Id"
begin
private lemma [autoref_op_pat]: "initial A ≡ OP (initial A)" by simp
private lemmas [autoref_rules] = nbai_nba_param(3)[THEN fun_relD, OF Ai]
schematic_goal complement_initial_7:
"(?f, {(Some ∘ (const (2 * n, False))) |` initial A}) ∈ ⟨state_rel⟩ list_set_rel"
by autoref
end
concrete_definition complement_initial_7 uses complement_initial_7
schematic_goal complement_accepting_7: "(?f, λ f. ∀ (p, k, c) ∈ map_to_set f. ¬ c) ∈
state_rel → bool_rel"
by autoref
concrete_definition complement_accepting_7 uses complement_accepting_7
definition complement_7 :: "('label, nat) nbai ⇒ nat ⇒ ('label, state) nbai" where
"complement_7 Ai ni ≡ nbai
(alphabeti Ai)
(complement_initial_7 Ai ni)
(complement_succ_7 Ai)
(complement_accepting_7)"
lemma complement_7_refine[autoref_rules]:
assumes "(Ai, A) ∈ ⟨Id, Id⟩ nbai_nba_rel"
assumes "(ni,
(OP card ::: ⟨Id⟩ ahs_rel bhc → nat_rel) $
((OP nodes ::: ⟨Id, Id⟩ nbai_nba_rel → ⟨Id⟩ ahs_rel bhc) $ A)) ∈ nat_rel"
shows "(complement_7 Ai ni, (OP complement_4 :::
⟨Id, Id⟩ nbai_nba_rel → ⟨Id, state_rel⟩ nbai_nba_rel) $ A) ∈ ⟨Id, state_rel⟩ nbai_nba_rel"
proof -
note complement_succ_7_refine
also note complement_succ_6_refine
also note complement_succ_5_refine
finally have 1: "(complement_succ_7, complement_succ_4) ∈
⟨Id, Id⟩ nbai_nba_rel → Id → state_rel → ⟨state_rel⟩ list_set_rel"
unfolding nres_rel_comp unfolding nres_rel_def unfolding fun_rel_def by auto
show ?thesis
unfolding complement_7_def complement_4_def
using 1 complement_initial_7.refine complement_accepting_7.refine assms
unfolding autoref_tag_defs
by parametricity
qed
end