Theory LTL_to_GBA.LTL_to_GBA
section ‹LTL to GBA translation›
theory LTL_to_GBA
imports
CAVA_Base.CAVA_Base
LTL.LTL
CAVA_Automata.Automata
begin
subsection ‹Statistics›
code_printing
code_module Gerth_Statistics ⇀ (SML) ‹
structure Gerth_Statistics = struct
val active = Unsynchronized.ref false
val data = Unsynchronized.ref (0,0,0)
fun is_active () = !active
fun set_data num_states num_init num_acc = (
active := true;
data := (num_states, num_init, num_acc)
)
fun to_string () = let
val (num_states, num_init, num_acc) = !data
in
"Num states: " ^ IntInf.toString (num_states) ^ "\n"
^ " Num initial: " ^ IntInf.toString num_init ^ "\n"
^ " Num acc-classes: " ^ IntInf.toString num_acc ^ "\n"
end
val _ = Statistics.register_stat ("Gerth LTL_to_GBA",is_active,to_string)
end
›
code_reserved SML Gerth_Statistics
consts
stat_set_data_int :: "integer ⇒ integer ⇒ integer ⇒ unit"
code_printing
constant stat_set_data_int ⇀ (SML) "Gerth'_Statistics.set'_data"
definition "stat_set_data ns ni na
≡ stat_set_data_int (integer_of_nat ns) (integer_of_nat ni) (integer_of_nat na)"
lemma [autoref_rules]:
"(stat_set_data,stat_set_data) ∈ nat_rel → nat_rel → nat_rel → unit_rel"
by auto
abbreviation "stat_set_data_nres ns ni na ≡ RETURN (stat_set_data ns ni na)"
lemma discard_stat_refine[refine]:
"m1≤m2 ⟹ stat_set_data_nres ns ni na ⪢ m1 ≤ m2" by simp_all
subsection ‹Preliminaries›
text ‹Some very special lemmas for reasoning about the nres-monad›
lemma SPEC_rule_nested2:
"⟦m ≤ SPEC P; ⋀r1 r2. P (r1, r2) ⟹ g (r1, r2) ≤ SPEC P⟧
⟹ m ≤ SPEC (λr'. g r' ≤ SPEC P)"
by (simp add: pw_le_iff) blast
lemma SPEC_rule_param2:
assumes "f x ≤ SPEC (P x)"
and "⋀r1 r2. (P x) (r1, r2) ⟹ (P x') (r1, r2)"
shows "f x ≤ SPEC (P x')"
using assms
by (simp add: pw_le_iff)
lemma SPEC_rule_weak:
assumes "f x ≤ SPEC (Q x)" and "f x ≤ SPEC (P x)"
and "⋀r1 r2. ⟦(Q x) (r1, r2); (P x) (r1, r2)⟧ ⟹ (P x') (r1, r2)"
shows "f x ≤ SPEC (P x')"
using assms
by (simp add: pw_le_iff)
lemma SPEC_rule_weak_nested2: "⟦f ≤ SPEC Q; f ≤ SPEC P;
⋀r1 r2. ⟦Q (r1, r2); P (r1, r2)⟧ ⟹ g (r1, r2) ≤ SPEC P⟧
⟹ f ≤ SPEC (λr'. g r' ≤ SPEC P)"
by (simp add: pw_le_iff) blast
subsection ‹Creation of States›
text ‹
In this section, the first part of the algorithm, which creates the states of the
automaton, is formalized.
›
type_synonym node_name = nat
type_synonym 'a frml = "'a ltlr"
type_synonym 'a interprt = "'a set word"
record 'a node =
name :: node_name
incoming :: "node_name set"
new :: "'a frml set"
old :: "'a frml set"
"next" :: "'a frml set"
context
begin
fun new1 where
"new1 (μ and⇩r ψ) = {μ,ψ}"
| "new1 (μ U⇩r ψ) = {μ}"
| "new1 (μ R⇩r ψ) = {ψ}"
| "new1 (μ or⇩r ψ) = {μ}"
| "new1 _ = {}"
fun next1 where
"next1 (X⇩r ψ) = {ψ}"
| "next1 (μ U⇩r ψ) = {μ U⇩r ψ}"
| "next1 (μ R⇩r ψ) = {μ R⇩r ψ}"
| "next1 _ = {}"
fun new2 where
"new2 (μ U⇩r ψ) = {ψ}"
| "new2 (μ R⇩r ψ) = {μ, ψ}"
| "new2 (μ or⇩r ψ) = {ψ}"
| "new2 _ = {}"
definition "expand_init ≡ 0"
definition "expand_new_name ≡ Suc"
lemma expand_new_name_expand_init: "expand_init < expand_new_name nm"
by (auto simp add:expand_init_def expand_new_name_def)
lemma expand_new_name_step[intro]:
fixes n :: "'a node"
shows "name n < expand_new_name (name n)"
by (auto simp add:expand_new_name_def)
lemma expand_new_name__less_zero[intro]: "0 < expand_new_name nm"
proof -
from expand_new_name_expand_init have "expand_init < expand_new_name nm"
by auto
then show ?thesis
by (metis gr0I less_zeroE)
qed
abbreviation
"upd_incoming_f n ≡ (λn'.
if (old n' = old n ∧ next n' = next n) then
n'⦇ incoming := incoming n ∪ incoming n' ⦈
else n'
)"
definition
"upd_incoming n ns ≡ ((upd_incoming_f n) ` ns)"
lemma upd_incoming__elem:
assumes "nd∈upd_incoming n ns"
shows "nd∈ns
∨ (∃nd'∈ns. nd = nd'⦇ incoming := incoming n ∪ incoming nd' ⦈ ∧
old nd' = old n ∧
next nd' = next n)"
proof -
obtain nd' where "nd'∈ns" and nd_eq: "nd = upd_incoming_f n nd'"
using assms unfolding upd_incoming_def by blast
then show ?thesis by auto
qed
lemma upd_incoming__ident_node:
assumes "nd∈upd_incoming n ns" and "nd∈ns"
shows "incoming n ⊆ incoming nd ∨ ¬ (old nd = old n ∧ next nd = next n)"
proof (rule ccontr)
assume "¬ ?thesis"
then have nsubset: "¬ (incoming n ⊆ incoming nd)" and
old_next_eq: "old nd = old n ∧ next nd = next n"
by auto
moreover
obtain nd' where "nd'∈ns" and nd_eq: "nd = upd_incoming_f n nd'"
using assms unfolding upd_incoming_def by blast
{ assume "old nd' = old n ∧ next nd' = next n"
with nd_eq have "nd = nd'⦇incoming := incoming n ∪ incoming nd'⦈" by auto
with nsubset have "False" by auto }
moreover
{ assume "¬ (old nd' = old n ∧ next nd' = next n)"
with nd_eq old_next_eq have "False" by auto }
ultimately show "False" by fast
qed
lemma upd_incoming__ident:
assumes "∀n∈ns. P n"
and "⋀n. ⟦n∈ns; P n⟧ ⟹ (⋀v. P (n⦇ incoming := v ⦈))"
shows "∀n∈upd_incoming n ns. P n"
proof
fix nd v
let ?f = "λn'.
if (old n' = old n ∧ next n' = next n) then
n'⦇ incoming := incoming n ∪ incoming n' ⦈
else n'"
assume "nd∈upd_incoming n ns"
then obtain nd' where "nd'∈ns" and nd_eq: "nd = ?f nd'"
unfolding upd_incoming_def by blast
{ assume "old nd' = old n ∧ next nd' = next n"
then obtain v where "nd = nd'⦇ incoming := v ⦈" using nd_eq by auto
with assms ‹nd'∈ns› have "P nd" by auto }
then show "P nd" using nd_eq ‹nd'∈ns› assms by auto
qed
lemma name_upd_incoming_f[simp]: "name (upd_incoming_f n x) = name x"
by auto
lemma name_upd_incoming[simp]:
"name ` (upd_incoming n ns) = name ` ns" (is "?lhs = ?rhs")
unfolding upd_incoming_def
proof safe
fix x
assume "x∈ns"
then have "upd_incoming_f n x ∈ (λn'. local.upd_incoming_f n n') ` ns" by auto
then have "name (upd_incoming_f n x) ∈ name ` (λn'. local.upd_incoming_f n n') ` ns"
by blast
then show "name x ∈ name ` (λn'. local.upd_incoming_f n n') ` ns" by simp
qed auto
abbreviation expand_body
where
"expand_body ≡ (λexpand (n,ns).
if new n = {} then (
if (∃n'∈ns. old n' = old n ∧ next n' = next n) then
RETURN (name n, upd_incoming n ns)
else
expand (
⦇
name=expand_new_name (name n),
incoming={name n},
new=next n,
old={},
next={}
⦈,
{n} ∪ ns)
) else do {
φ ← SPEC (λx. x∈(new n));
let n = n⦇ new := new n - {φ} ⦈;
if (∃q. φ = prop⇩r(q) ∨ φ = nprop⇩r(q)) then
(if (not⇩r φ) ∈ old n then RETURN (name n, ns)
else expand (n⦇ old := {φ} ∪ old n ⦈, ns))
else if φ = true⇩r then expand (n⦇ old := {φ} ∪ old n ⦈, ns)
else if φ = false⇩r then RETURN (name n, ns)
else if (∃ν μ. (φ = ν and⇩r μ) ∨ (φ = X⇩r ν)) then
expand (
n⦇
new := new1 φ ∪ new n,
old := {φ} ∪ old n,
next := next1 φ ∪ next n
⦈,
ns)
else do {
(nm, nds) ← expand (
n⦇
new := new1 φ ∪ new n,
old := {φ} ∪ old n,
next := next1 φ ∪ next n
⦈,
ns);
expand (n⦇ name := nm, new := new2 φ ∪ new n, old := {φ} ∪ old n ⦈, nds)
}
}
)"
lemma expand_body_mono: "trimono expand_body" by refine_mono
definition expand :: "('a node × ('a node set)) ⇒ (node_name × 'a node set) nres"
where "expand ≡ REC expand_body"
lemma REC_rule_old:
fixes x::"'x"
assumes M: "trimono body"
assumes I0: "Φ x"
assumes IS: "⋀f x. ⟦ ⋀x. Φ x ⟹ f x ≤ M x; Φ x; f ≤ REC body ⟧
⟹ body f x ≤ M x"
shows "REC body x ≤ M x"
by (rule REC_rule_arb[where pre="λ_. Φ" and M="λ_. M", OF assms])
lemma expand_rec_rule:
assumes I0: "Φ x"
assumes IS: "⋀f x. ⟦ ⋀x. f x ≤ expand x; ⋀x. Φ x ⟹ f x ≤ M x; Φ x ⟧
⟹ expand_body f x ≤ M x"
shows "expand x ≤ M x"
unfolding expand_def
apply (rule REC_rule_old[where Φ="Φ"])
apply (rule expand_body_mono)
apply (rule I0)
apply (rule IS[unfolded expand_def])
apply (blast dest: le_funD)
apply blast
apply blast
done
abbreviation
"expand_assm_incoming n_ns
≡ (∀nm∈incoming (fst n_ns). name (fst n_ns) > nm)
∧ 0 < name (fst n_ns)
∧ (∀q∈snd n_ns.
name (fst n_ns) > name q
∧ (∀nm∈incoming q. name (fst n_ns) > nm))"
abbreviation
"expand_rslt_incoming nm_nds
≡ (∀q∈snd nm_nds. (fst nm_nds > name q ∧ (∀nm'∈incoming q. fst nm_nds > nm')))"
abbreviation
"expand_rslt_name n_ns nm_nds
≡ (name (fst n_ns) ≤ fst nm_nds ∧ name ` (snd n_ns) ⊆ name ` (snd nm_nds))
∧ name ` (snd nm_nds)
= name ` (snd n_ns) ∪ name ` {nd∈snd nm_nds. name nd ≥ name (fst n_ns)}"
abbreviation
"expand_name_ident nds
≡ (∀q∈nds. ∃!q'∈nds. name q = name q')"
abbreviation
"expand_assm_exist ξ n_ns
≡ {η. ∃μ. μ U⇩r η ∈ old (fst n_ns) ∧ ξ ⊨⇩r η} ⊆ new (fst n_ns) ∪ old (fst n_ns)
∧ (∀ψ∈new (fst n_ns). ξ ⊨⇩r ψ)
∧ (∀ψ∈old (fst n_ns). ξ ⊨⇩r ψ)
∧ (∀ψ∈next (fst n_ns). ξ ⊨⇩r X⇩r ψ)"
abbreviation
"expand_rslt_exist__node_prop ξ n nd
≡ incoming n ⊆ incoming nd
∧ (∀ψ∈old nd. ξ ⊨⇩r ψ) ∧ (∀ψ∈next nd. ξ ⊨⇩r X⇩r ψ)
∧ {η. ∃μ. μ U⇩r η ∈ old nd ∧ ξ ⊨⇩r η} ⊆ old nd"
abbreviation
"expand_rslt_exist ξ n_ns nm_nds
≡ (∃nd∈snd nm_nds. expand_rslt_exist__node_prop ξ (fst n_ns) nd)"
abbreviation
"expand_rslt_exist_eq__node n nd
≡ name n = name nd
∧ old n = old nd
∧ next n = next nd
∧ incoming n ⊆ incoming nd"
abbreviation
"expand_rslt_exist_eq n_ns nm_nds ≡
(∀n∈snd n_ns. ∃nd∈snd nm_nds. expand_rslt_exist_eq__node n nd)"
lemma expand_name_propag:
assumes "expand_assm_incoming n_ns ∧ expand_name_ident (snd n_ns)" (is "?Q n_ns")
shows "expand n_ns ≤ SPEC (λr. expand_rslt_incoming r
∧ expand_rslt_name n_ns r
∧ expand_name_ident (snd r))"
(is "expand _ ≤ SPEC (?P n_ns)")
using assms
proof (rule_tac expand_rec_rule[where Φ="?Q"], simp, intro refine_vcg, goal_cases)
case prems: (1 _ _ n ns)
then have Q: "?Q (n, ns)" by fast
let ?nds = "upd_incoming n ns"
from prems have "∀q∈?nds. name q < name n"
by (rule_tac upd_incoming__ident) auto
moreover
have "∀q∈?nds. ∀nm'∈incoming q. nm' < name n" (is "∀q∈_. ?sg q")
proof
fix q
assume q_in:"q∈?nds"
show "?sg q"
proof (cases "q∈ns")
case True
with prems show ?thesis by auto
next
case False
with upd_incoming__elem[OF q_in]
obtain nd' where
nd'_def:"nd'∈ns ∧ q = nd'⦇incoming := incoming n ∪ incoming nd'⦈"
by blast
{ fix nm'
assume "nm'∈incoming q"
moreover
{ assume "nm'∈incoming n"
with Q have "nm' < name n" by auto }
moreover
{ assume "nm'∈incoming nd'"
with Q nd'_def have "nm' < name n" by auto }
ultimately have "nm' < name n" using nd'_def by auto }
then show ?thesis by fast
qed
qed
moreover
have "expand_name_ident ?nds"
proof (rule upd_incoming__ident, goal_cases)
case 1
show ?case
proof
fix q
assume "q∈ns"
with Q have "∃!q'∈ns. name q = name q'" by auto
then obtain q' where "q'∈ns" and "name q = name q'"
and q'_all: "∀q''∈ns. name q' = name q'' ⟶ q' = q''"
by auto
let ?q' = "upd_incoming_f n q'"
have P_a: "?q'∈?nds ∧ name q = name ?q'"
using ‹q'∈ns› ‹name q = name q'› q'_all
unfolding upd_incoming_def by auto
have P_all: "∀q''∈?nds. name ?q' = name q'' ⟶ ?q' = q''"
proof(clarify)
fix q''
assume "q''∈?nds" and q''_name_eq: "name ?q' = name q''"
{ assume "q''∉ns"
with upd_incoming__elem[OF ‹q''∈?nds›]
obtain nd'' where
"nd''∈ns"
and q''_is: "q'' = nd''⦇incoming := incoming n ∪ incoming nd''⦈
∧ old nd'' = old n ∧ next nd'' = next n"
by auto
then have "name nd'' = name q'"
using q''_name_eq
by (cases "old q' = old n ∧ next q' = next n") auto
with ‹nd''∈ns› q'_all have "nd'' = q'" by auto
then have "?q' = q''" using q''_is by simp }
moreover
{ assume "q''∈ns"
moreover
have "name q' = name q''"
using q''_name_eq
by (cases "old q' = old n ∧ next q' = next n") auto
moreover
then have "incoming n ⊆ incoming q''
⟹ incoming q'' = incoming n ∪ incoming q''"
by auto
ultimately have "?q' = q''"
using upd_incoming__ident_node[OF ‹q''∈?nds›] q'_all
by auto
}
ultimately show "?q' = q''" by fast
qed
show "∃!q'∈upd_incoming n ns. name q = name q'"
proof(rule ex1I[of _ ?q'], goal_cases)
case 1
then show ?case using P_a by simp
next
case 2
then show ?case
using P_all unfolding P_a[THEN conjunct2, THEN sym]
by blast
qed
qed
qed simp
ultimately show ?case using prems by auto
next
case prems: (2 f x n ns)
then have step: "⋀x. ?Q x ⟹ f x ≤ SPEC (?P x)" by simp
from prems have Q: "?Q (n, ns)" by auto
show ?case unfolding ‹x = (n, ns)›
proof (rule_tac SPEC_rule_param2[where P = "?P"], rule_tac step, goal_cases)
case 1
with expand_new_name_step[of n] show ?case
using Q
by (auto elim: order_less_trans[rotated])
next
case prems': (2 _ nds)
then have "name ` ns ⊆ name ` nds" by auto
with expand_new_name_step[of n] show ?case
using prems' by auto
qed
next
case 3
then show ?case by auto
next
case prems: (4 f)
then have step: "⋀x. ?Q x ⟹ f x ≤ SPEC (?P x)"
by simp_all
with prems show ?case
by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
case prems: (5 f)
then have step: "⋀x. ?Q x ⟹ f x ≤ SPEC (?P x)"
by simp_all
from prems show ?case
by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
case 6
then show ?case by auto
next
case prems: (7 f)
then have step: "⋀x. ?Q x ⟹ f x ≤ SPEC (?P x)"
by simp_all
from prems show ?case
by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
case prems: (8 f x n ns ψ)
then have goal_assms: "ψ ∈ new n ∧ (∃ν μ. ψ = ν or⇩r μ ∨ ψ = ν U⇩r μ ∨ ψ = ν R⇩r μ)"
by (cases ψ) auto
from prems have Q: "?Q (n, ns)" and step: "⋀x. ?Q x ⟹ f x ≤ SPEC (?P x)"
by simp_all
show ?case
using goal_assms Q
unfolding case_prod_unfold ‹x = (n, ns)›
proof (rule_tac SPEC_rule_nested2, goal_cases)
case 1
then show ?case
by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
case prems: (2 nm nds)
then have P_x: "(name n ≤ nm ∧ name ` ns ⊆ name ` nds)
∧ name ` nds = name ` ns ∪ name ` {nd∈nds. name nd ≥ name n}"
(is "_ ∧ ?nodes_eq nds ns (name n)") by auto
show ?case
proof (rule_tac SPEC_rule_param2[where P = "?P"], goal_cases)
case 1
with prems show ?case by (rule_tac step) auto
next
case prems': (2 nm' nds')
then have "∀q∈nds'. name q < nm' ∧ (∀nm''∈incoming q. nm'' < nm')" by auto
moreover
have "?nodes_eq nds ns (name n)" and "?nodes_eq nds' nds nm" and "name n ≤ nm"
using prems' P_x by auto
then have "?nodes_eq nds' ns (name n)" by auto
then have "expand_rslt_name (n, ns) (nm', nds')"
using prems' P_x subset_trans[of "name ` ns" "name ` nds"] by auto
ultimately show ?case using prems' by auto
qed
qed
qed
lemmas expand_name_propag__incoming = SPEC_rule_conjunct1[OF expand_name_propag]
lemmas expand_name_propag__name =
SPEC_rule_conjunct1[OF SPEC_rule_conjunct2[OF expand_name_propag]]
lemmas expand_name_propag__name_ident =
SPEC_rule_conjunct2[OF SPEC_rule_conjunct2[OF expand_name_propag]]
lemma expand_rslt_exist_eq:
shows "expand n_ns ≤ SPEC (expand_rslt_exist_eq n_ns)"
(is "_ ≤ SPEC (?P n_ns)")
proof (rule_tac expand_rec_rule[where Φ="λ_. True"], simp, intro refine_vcg, goal_cases)
case prems: (1 f x n ns)
let ?r = "(name n, upd_incoming n ns)"
have "expand_rslt_exist_eq (n, ns) ?r"
unfolding snd_conv
proof
fix n'
assume "n'∈ns"
{ assume "old n' = old n ∧ next n' = next n"
with ‹n'∈ns›
have "n'⦇ incoming := incoming n ∪ incoming n' ⦈ ∈ upd_incoming n ns"
unfolding upd_incoming_def by auto
}
moreover
{ assume "¬ (old n' = old n ∧ next n' = next n)"
with ‹n'∈ns› have "n' ∈ upd_incoming n ns"
unfolding upd_incoming_def by auto
}
ultimately show "∃nd∈upd_incoming n ns. expand_rslt_exist_eq__node n' nd"
by force
qed
with prems show ?case by auto
next
case prems: (2 f)
then have step: "⋀x. f x ≤ SPEC (?P x)" by simp
with prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
case 3 then show ?case by auto
next
case prems: (4 f)
then have step: "⋀x. f x ≤ SPEC (?P x)" by simp
with prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
case prems: (5 f)
then have step: "⋀x. f x ≤ SPEC (?P x)" by simp
with prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
case 6 then show ?case by auto
next
case prems: (7 f)
then have step: "⋀x. f x ≤ SPEC (?P x)" by simp
with prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
case prems: (8 f x n ns)
then have step: "⋀x. f x ≤ SPEC (?P x)" by simp
show ?case
proof (rule_tac SPEC_rule_nested2, goal_cases)
case 1
with prems show ?case
by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
case (2 nm nds)
with prems have P_x: "?P (n, ns) (nm, nds)" by fast
show ?case
unfolding case_prod_unfold ‹x = (n, ns)›
proof (rule_tac SPEC_rule_param2[where P = "?P"], goal_cases)
case 1
then show ?case by (rule_tac step)
next
case prems': (2 nm' nds')
{
fix n'
assume "n'∈ns"
with P_x obtain nd where "nd∈nds" and n'_split: "expand_rslt_exist_eq__node n' nd"
by auto
with prems' obtain nd' where "nd'∈nds'" and "expand_rslt_exist_eq__node nd nd'"
by auto
then have "∃nd'∈nds'. expand_rslt_exist_eq__node n' nd'"
using n'_split subset_trans[of "incoming n'"] by auto
}
then have "expand_rslt_exist_eq (n, ns) (nm', nds')" by auto
with prems show ?case by auto
qed
qed
qed
lemma expand_prop_exist:
"expand n_ns ≤ SPEC (λr. expand_assm_exist ξ n_ns ⟶ expand_rslt_exist ξ n_ns r)"
(is "_ ≤ SPEC (?P n_ns)")
proof (rule_tac expand_rec_rule[where Φ="λ_. True"], simp, intro refine_vcg, goal_cases)
case prems: (1 f x n ns)
let ?nds = "upd_incoming n ns"
let ?r = "(name n, ?nds)"
{ assume Q: "expand_assm_exist ξ (n, ns)"
note ‹∃n'∈ns. old n' = old n ∧ next n' = next n›
then obtain n' where "n'∈ns" and assm_eq: "old n' = old n ∧ next n' = next n"
by auto
let ?nd = "n'⦇ incoming := incoming n ∪ incoming n'⦈"
have "?nd ∈ ?nds" using ‹n'∈ns› assm_eq unfolding upd_incoming_def by auto
moreover
have "incoming n ⊆ incoming ?nd" by auto
moreover
have "expand_rslt_exist__node_prop ξ n ?nd" using Q assm_eq ‹new n = {}›
by simp
ultimately have "expand_rslt_exist ξ (n, ns) ?r"
unfolding fst_conv snd_conv by blast
}
with prems show ?case
by auto
next
case prems: (2 f x n ns)
then have step: "⋀x. f x ≤ SPEC (?P x)"
and f_sup: "⋀x. f x ≤ expand x" by auto
show ?case
unfolding ‹x = (n, ns)›
proof (rule_tac SPEC_rule_weak[where Q = "expand_rslt_exist_eq"], goal_cases)
case 1
then show ?case
by (rule_tac order_trans, rule_tac f_sup, rule_tac expand_rslt_exist_eq)
next
case 2
then show ?case by (rule_tac step)
next
case prems': (3 nm nds)
then have "name ` ns ⊆ name ` nds" by auto
moreover
{ assume assm_ex: "expand_assm_exist ξ (n, ns)"
with prems' obtain nd where "nd∈nds" and "expand_rslt_exist_eq__node n nd"
by force+
then have "expand_rslt_exist__node_prop ξ n nd"
using assm_ex ‹new n = {}› by auto
then have "expand_rslt_exist ξ (n, ns) (nm, nds)" using ‹nd∈nds› by auto }
ultimately show ?case
using expand_new_name_step[of n] prems' by auto
qed
next
case prems: (3 f x n ns ψ)
{ assume "expand_assm_exist ξ (n, ns)"
with prems have "ξ ⊨⇩r ψ" and "ξ ⊨⇩r not⇩r ψ"
by (metis (no_types, lifting) fstI node.select_convs(4) node.surjective node.update_convs(3))+
then have False by simp }
with prems show ?case by auto
next
case prems: (4 f x n ns ψ)
then have goal_assms: "ψ ∈ new n ∧ (∃q. ψ = prop⇩r(q) ∨ ψ = nprop⇩r(q))"
and step: "⋀x. f x ≤ SPEC (?P x)" by simp_all
show ?case
using goal_assms unfolding ‹x = (n, ns)›
proof (rule_tac SPEC_rule_param2, rule_tac step, goal_cases)
case prems': (1 nm nds)
{ assume "expand_assm_exist ξ (n, ns)"
with prems' have "expand_rslt_exist ξ (n, ns) (nm, nds)" by auto }
then show ?case by auto
qed
next
case prems: (5 f x n ns ψ)
then have goal_assms: "ψ ∈ new n ∧ ψ = true⇩r"
and step: "⋀x. f x ≤ SPEC (?P x)" by simp_all
show ?case
using goal_assms unfolding ‹x = (n, ns)›
proof (rule_tac SPEC_rule_param2, rule_tac step, goal_cases)
case prems': (1 nm nds)
{ assume "expand_assm_exist ξ (n, ns)"
with prems' have "expand_rslt_exist ξ (n, ns) (nm, nds)" by auto }
then show ?case by auto
qed
next
case prems: (6 f x n ns ψ)
{ assume "expand_assm_exist ξ (n, ns)"
with prems have "ξ ⊨⇩r false⇩r" by auto }
with prems show ?case by auto
next
case prems: (7 f x n ns ψ)
then have goal_assms: "ψ ∈ new n ∧ (∃ν μ. ψ = ν and⇩r μ ∨ ψ = X⇩r ν)"
and step: "⋀x. f x ≤ SPEC (?P x)" by simp_all
show ?case
using goal_assms unfolding ‹x = (n, ns)›
proof (rule_tac SPEC_rule_param2, rule_tac step, goal_cases)
case prems': (1 nm nds)
{ assume "expand_assm_exist ξ (n, ns)"
with prems' have "expand_rslt_exist ξ (n, ns) (nm, nds)" by auto }
then show ?case by auto
qed
next
case prems: (8 f x n ns ψ)
then have goal_assms: "ψ ∈ new n ∧ (∃ν μ. ψ = ν or⇩r μ ∨ ψ = ν U⇩r μ ∨ ψ = ν R⇩r μ)"
by (cases ψ) auto
from prems have step: "⋀x. f x ≤ SPEC (?P x)"
and f_sup: "⋀x. f x ≤ expand x" by auto
let ?x1 = "(n⦇new := new n - {ψ}, new := new1 ψ ∪ new (n⦇new := new n - {ψ}⦈),
old := {ψ} ∪ old n, next := next1 ψ ∪ next n⦈, ns)"
let ?new1_assm_sel = "λψ. (case ψ of μ U⇩r η => η | μ R⇩r η ⇒ μ | μ or⇩r η ⇒ η)"
{ assume new1_assm: "¬ (ξ ⊨⇩r (?new1_assm_sel ψ))"
then have ?case
using goal_assms unfolding ‹x = (n, ns)›
proof (rule_tac SPEC_rule_nested2, goal_cases)
case prems': 1
then show ?case
proof (rule_tac SPEC_rule_param2, rule_tac step, goal_cases)
case prems'': (1 nm nds)
{ assume "expand_assm_exist ξ (n, ns)"
with prems'' have "expand_assm_exist ξ ?x1"
unfolding fst_conv
proof (cases ψ, goal_cases)
case ψ: (8 μ η)
then have "ξ ⊨⇩r μ U⇩r η" by fast
then have "ξ ⊨⇩r μ" and "ξ ⊨⇩r X⇩r (μ U⇩r η)"
using ψ ltlr_expand_Until[of ξ μ η] by auto
with ψ show ?case by auto
next
case ψ: (9 μ η)
then have *: "ξ ⊨⇩r μ R⇩r η" by fast
with ψ have "ξ ⊨⇩r η" and "ξ ⊨⇩r X⇩r (μ R⇩r η)"
using ltlr_expand_Release[of ξ μ η] by auto
with ψ * show ?case by auto
qed auto
with prems'' have "expand_rslt_exist ξ (n, ns) (nm, nds)" by force }
with prems'' show ?case by auto
qed
next
case prems': (2 nm nds)
then have P_x: "?P (n, ns) (nm, nds)" by fast
show ?case
unfolding case_prod_unfold
proof (rule_tac SPEC_rule_weak[where P = "?P" and Q = "expand_rslt_exist_eq"], goal_cases)
case 1
then show ?case
by (rule_tac order_trans,
rule_tac f_sup,
rule_tac expand_rslt_exist_eq)
next
case 2
then show ?case by (rule_tac step)
next
case prems'': (3 nm' nds')
{ assume "expand_assm_exist ξ (n, ns)"
with P_x have "expand_rslt_exist ξ (n, ns) (nm, nds)" by simp
then obtain nd where nd: "nd∈nds" "expand_rslt_exist__node_prop ξ n nd"
using goal_assms by auto
with prems'' obtain nd' where
"nd'∈nds'" and "expand_rslt_exist_eq__node nd nd'"
by force
with nd have "expand_rslt_exist__node_prop ξ n nd'"
using subset_trans[of "incoming n" "incoming nd"] by auto
then have "expand_rslt_exist ξ (n,ns) (nm', nds')"
using ‹nd'∈nds'› goal_assms by auto }
then show ?case by fast
qed
qed
}
moreover
{ assume new1_assm: "ξ ⊨⇩r (?new1_assm_sel ψ)"
let ?x2f = "λ(nm::node_name, nds::'a node set). (
n⦇new := new n - {ψ},
name := nm,
new := new2 ψ ∪ new (n⦇new := new n - {ψ}⦈),
old := {ψ} ∪ old n⦈,
nds)"
have P_x: "f ?x1 ≤ SPEC (?P ?x1)" by (rule step)
moreover
{ fix r :: "node_name × 'a node set"
let ?x2 = "?x2f r"
assume assm: "(?P ?x1) r"
have "f ?x2 ≤ SPEC (?P (n, ns))"
unfolding case_prod_unfold fst_conv
proof (rule_tac SPEC_rule_param2, rule_tac step, goal_cases)
case prems': (1 nm' nds')
{ assume "expand_assm_exist ξ (n, ns)"
with new1_assm goal_assms have "expand_assm_exist ξ ?x2"
proof (cases r, cases ψ, goal_cases)
case prems'': (9 _ _ μ η)
then have *: "ξ ⊨⇩r μ R⇩r η" unfolding fst_conv by fast
with ltlr_expand_Release[of ξ μ η] have "ξ ⊨⇩r η" by auto
with prems'' * show ?case by auto
qed auto
with prems' have "expand_rslt_exist ξ ?x2 (nm', nds')"
unfolding case_prod_unfold fst_conv snd_conv by fast
then have "expand_rslt_exist ξ (n, ns) (nm', nds')" by (cases r, auto) }
then show ?case by simp
qed
}
then have "SPEC (?P ?x1)
≤ SPEC (λr. (case r of (nm, nds) =>
f (?x2f (nm, nds))) ≤ SPEC (?P (n, ns)))"
using goal_assms by (rule_tac SPEC_rule) force
finally have ?case unfolding case_prod_unfold ‹x = (n, ns)› by simp
}
ultimately show ?case by fast
qed
text ‹Termination proof›
definition expand⇩T :: "('a node × ('a node set)) ⇒ (node_name × 'a node set) nres"
where "expand⇩T n_ns ≡ REC⇩T expand_body n_ns"
abbreviation "old_next_pair n ≡ (old n, next n)"
abbreviation "old_next_limit φ ≡ Pow (subfrmlsr φ) × Pow (subfrmlsr φ)"
lemma old_next_limit_finite: "finite (old_next_limit φ)"
using subfrmlsr_finite by auto
definition
"expand_ord φ ≡
inv_image (finite_psupset (old_next_limit φ) <*lex*> less_than)
(λ(n, ns). (old_next_pair ` ns, size_set (new n)))"
lemma expand_ord_wf[simp]: "wf (expand_ord φ)"
using finite_psupset_wf[OF old_next_limit_finite]
unfolding expand_ord_def by auto
abbreviation
"expand_inv_node φ n
≡ finite (new n) ∧ finite (old n) ∧ finite (next n)
∧ (new n) ∪ (old n) ∪ (next n) ⊆ subfrmlsr φ"
abbreviation
"expand_inv_result φ ns ≡ finite ns ∧ (∀n'∈ns. (new n') ∪ (old n') ∪ (next n') ⊆ subfrmlsr φ)"
definition
"expand_inv φ n_ns ≡ (case n_ns of (n, ns) ⇒ expand_inv_node φ n ∧ expand_inv_result φ ns)"
lemma new1_less_sum:
"size_set (new1 φ) < size_set {φ}"
proof (cases φ)
case (And_ltlr ν μ)
thus ?thesis
by (cases "ν = μ"; simp)
qed (simp_all)
lemma new2_less_sum:
"size_set (new2 φ) < size_set {φ}"
proof (cases φ)
case (Release_ltlr ν μ)
thus ?thesis
by (cases "ν = μ"; simp)
qed (simp_all)
lemma new1_finite[intro]: "finite (new1 ψ)"
by (cases ψ) auto
lemma new1_subset_frmls: "φ ∈ new1 ψ ⟹ φ ∈ subfrmlsr ψ"
by (cases ψ) auto
lemma new2_finite[intro]: "finite (new2 ψ)"
by (cases ψ) auto
lemma new2_subset_frmls: "φ ∈ new2 ψ ⟹ φ ∈ subfrmlsr ψ"
by (cases ψ) auto
lemma next1_finite[intro]: "finite (next1 ψ)"
by (cases ψ) auto
lemma next1_subset_frmls: "φ ∈ next1 ψ ⟹ φ ∈ subfrmlsr ψ"
by (cases ψ) auto
lemma expand_inv_impl[intro!]:
assumes "expand_inv φ (n, ns)"
and newn: "ψ ∈ new n"
and "old_next_pair ` ns ⊆ old_next_pair ` ns'"
and "expand_inv_result φ ns'"
and "(n' = n⦇ new := new n - {ψ},
old := {ψ} ∪ old n ⦈) ∨
(n' = n⦇ new := new1 ψ ∪ (new n - {ψ}),
old := {ψ} ∪ old n,
next := next1 ψ ∪ next n ⦈) ∨
(n' = n⦇ name := nm,
new := new2 ψ ∪ (new n - {ψ}),
old := {ψ} ∪ old n ⦈)"
(is "?case1 ∨ ?case2 ∨ ?case3")
shows "((n', ns'), (n, ns))∈expand_ord φ ∧ expand_inv φ (n', ns')"
(is "?concl1 ∧ ?concl2")
proof
from assms consider ?case1 | ?case2 | ?case3 by blast
then show ?concl1
proof cases
case n'def: 1
with assms show ?thesis
unfolding expand_ord_def expand_inv_def finite_psupset_def
apply (cases "old_next_pair ` ns ⊂ old_next_pair ` ns'")
apply simp_all
apply auto [1]
apply (metis (no_types, lifting) add_Suc diff_Suc_less psubsetI sum.remove sum_diff1_nat zero_less_Suc)
done
next
case n'def: 2
have ψinnew: "ψ ∈ new n" and fin_new: "finite (new n)"
using assms unfolding expand_inv_def by auto
then have "size_set (new n - {ψ}) = size_set (new n) - size_set {ψ}"
using size_set_diff by fastforce
moreover
from fin_new sum_Un_nat[OF new1_finite _, of "new n - {ψ}" size ψ]
have "size_set (new n') ≤ size_set (new1 ψ) + size_set (new n - {ψ})"
unfolding n'def by (simp add: new1_finite sum_Un_nat)
moreover
have sum_leq: "size_set (new n) ≥ size_set {ψ}"
using ψinnew sum_mono2[OF fin_new, of "{ψ}"]
by blast
ultimately
have "size_set (new n') < size_set (new n)"
using new1_less_sum[of ψ] by auto
with assms show ?thesis
unfolding expand_ord_def finite_psupset_def by auto
next
case n'def: 3
have ψinnew: "ψ ∈ new n" and fin_new: "finite (new n)"
using assms unfolding expand_inv_def by auto
from ψinnew sum_diff1_nat[of size "new n" ψ]
have "size_set (new n - {ψ}) = size_set (new n) - size_set {ψ}"
using size_set_diff[of "new n" "{ψ}"] by fastforce
moreover
from fin_new sum_Un_nat[OF new2_finite _, of "new n - {ψ}" size ψ]
have "size_set (new n') ≤ size_set (new2 ψ) + size_set (new n - {ψ})"
unfolding n'def by (simp add: new2_finite sum_Un_nat)
moreover
have sum_leq:"size_set (new n) ≥ size_set {ψ}"
using ψinnew sum_mono2[OF fin_new, of "{ψ}"] by blast
ultimately
have "size_set (new n') < size_set (new n)"
using new2_less_sum[of ψ] sum_leq by auto
with assms show ?thesis
unfolding expand_ord_def finite_psupset_def by auto
qed
next
have "new1 ψ ⊆ subfrmlsr φ"
and "new2 ψ ⊆ subfrmlsr φ"
and "next1 ψ ⊆ subfrmlsr φ"
using assms subfrmlsr_subset[OF new1_subset_frmls[of _ ψ]]
subfrmlsr_subset[of ψ φ, OF rev_subsetD[of _ "new n"]]
subfrmlsr_subset[OF new2_subset_frmls[of _ ψ]]
subfrmlsr_subset[OF next1_subset_frmls[of _ ψ]]
unfolding expand_inv_def
apply -
apply (clarsimp split: prod.splits)
apply (metis in_mono new1_subset_frmls)
apply (clarsimp split: prod.splits)
apply (metis new2_subset_frmls rev_subsetD)
apply (clarsimp split: prod.splits)
apply (metis in_mono next1_subset_frmls)
done
with assms show ?concl2
unfolding expand_inv_def
by auto
qed
lemma expand_term_prop_help:
assumes "((n', ns'), (n, ns))∈expand_ord φ ∧ expand_inv φ (n', ns')"
and assm_rule: "⟦expand_inv φ (n', ns'); ((n', ns'), n, ns) ∈ expand_ord φ⟧
⟹ f (n', ns') ≤ SPEC P"
shows "f (n', ns') ≤ SPEC P"
using assms by (rule_tac assm_rule) auto
lemma expand_inv_upd_incoming:
assumes "expand_inv φ (n, ns)"
shows "expand_inv_result φ (upd_incoming n ns)"
using assms unfolding expand_inv_def upd_incoming_def by force
lemma upd_incoming_eq_old_next_pair: "old_next_pair ` ns = old_next_pair ` (upd_incoming n ns)"
(is "?A = ?B")
proof
show "?A ⊆ ?B"
proof
fix x
let ?f = "λn'. n'⦇incoming := incoming n ∪ incoming n'⦈"
assume "x ∈ ?A"
then obtain n' where "n' ∈ ns" and xeq: "x = (old n', next n')"
by auto
have "x ∈ (old_next_pair ` (λn'. n'⦇incoming := incoming n ∪ incoming n'⦈)
` (ns ∩ {n' ∈ ns. old n' = old n ∧ next n' = next n}))
∪ (old_next_pair ` (ns ∩ {n' ∈ ns. old n' ≠ old n ∨ next n' ≠ next n}))"
proof (cases "old n' = old n ∧ next n' = next n")
case True
with ‹n' ∈ ns›
have "?f n' ∈ ?f ` (ns ∩ {n'∈ns. old n' = old n ∧ next n' = next n})" (is "_ ∈ ?C")
by auto
then have "old_next_pair (?f n') ∈ old_next_pair ` ?C"
by (rule_tac imageI) auto
with xeq have "x∈old_next_pair ` ?C" by auto
then show ?thesis by blast
next
case False
with ‹n' ∈ ns› xeq
have "x ∈ old_next_pair ` (ns ∩ {n'∈ns. old n' ≠ old n ∨ next n' ≠ next n})"
by auto
then show ?thesis by blast
qed
then show "x ∈ ?B"
using ‹x ∈ ?A› unfolding upd_incoming_def by auto
qed
show "?B ⊆ ?A"
unfolding upd_incoming_def by (force intro:imageI)
qed
lemma expand_term_prop:
"expand_inv φ n_ns ⟹
expand⇩T n_ns ≤ SPEC (λ(_, nds). old_next_pair ` snd n_ns⊆old_next_pair `nds
∧ expand_inv_result φ nds)"
(is "_ ⟹ _ ≤ SPEC (?P n_ns)")
unfolding expand⇩T_def
apply (rule_tac RECT_rule[where pre="λ(n, ns). expand_inv φ (n, ns)" and V="expand_ord φ"])
apply (refine_mono)
apply simp
apply simp
proof (intro refine_vcg, goal_cases)
case prems: (1 _ _ n ns)
have "old_next_pair ` ns ⊆ old_next_pair ` (upd_incoming n ns)"
by (rule equalityD1[OF upd_incoming_eq_old_next_pair])
with prems show ?case
using expand_inv_upd_incoming[of φ n ns] by auto
next
case prems: (2 expand x n ns)
let ?n' = "⦇
name = expand_new_name (name n),
incoming = {name n},
new = next n,
old = {},
next = {}⦈"
let ?ns' = "{n} ∪ ns"
from prems have SPEC_sub:"SPEC (?P (?n', ?ns')) ≤ SPEC (?P x)"
by (rule_tac SPEC_rule) auto
from prems have "old_next_pair n ∉ old_next_pair ` ns"
by auto
then have "old_next_pair ` ns ⊂ old_next_pair ` (insert n ns)"
by auto
moreover from prems have "expand_inv φ (n, ns)"
by simp
ultimately have "((?n', ?ns'), (n, ns)) ∈ expand_ord φ"
by (auto simp add: expand_ord_def finite_psupset_def expand_inv_def)
moreover from prems have "expand_inv φ (?n', ?ns')"
unfolding expand_inv_def by auto
ultimately have "expand (?n', ?ns') ≤ SPEC (?P (?n', ?ns'))"
using prems by fast
with SPEC_sub show ?case
by (rule_tac order_trans) fast+
next
case 3
then show ?case by (auto simp add:expand_inv_def)
next
case 4
then show ?case
apply (rule_tac expand_term_prop_help[OF expand_inv_impl])
apply (simp add: expand_inv_def)+
apply force
done
next
case 5
then show ?case
apply (rule_tac expand_term_prop_help[OF expand_inv_impl])
apply (simp add: expand_inv_def)+
apply force
done
next
case 6
then show ?case by (simp add: expand_inv_def)
next
case 7
then show ?case
apply (rule_tac expand_term_prop_help[OF expand_inv_impl])
apply (simp add: expand_inv_def)+
apply force
done
next
case prems: (8 f x a b xa)
let ?n' = "a⦇
new := new1 xa ∪ (new a - {xa}),
old := insert xa (old a),
next := next1 xa ∪ next a⦈"
let ?n'' = "λnm. a⦇
name := nm,
new := new2 xa ∪ (new a - {xa}),
old := insert xa (old a)⦈"
have step:"((?n', b), (a, b)) ∈ expand_ord φ ∧ expand_inv φ (?n', b)"
using prems by (rule_tac expand_inv_impl) (auto simp add: expand_inv_def)
with prems have assm1: "f (?n', b) ≤ SPEC (?P (a, b))"
by auto
moreover
{
fix nm::node_name and nds::"'a node set"
assume assm1: "old_next_pair ` b ⊆ old_next_pair ` nds"
and assm2: "expand_inv_result φ nds"
with prems step have "((?n'' nm, nds), (a, b)) ∈ expand_ord φ ∧ expand_inv φ (?n'' nm, nds)"
by (rule_tac expand_inv_impl) auto
with prems have "f (?n'' nm, nds) ≤ SPEC (?P (?n'' nm, nds))"
by auto
moreover
have "SPEC (?P (?n'' nm, nds)) ≤ SPEC (?P (a, b))"
using assm2 subset_trans[OF assm1] by auto
ultimately have "f (?n'' nm, nds) ≤ SPEC (?P (a, b))"
by (rule order_trans)
}
then have assm2: "SPEC (?P (a, b))
≤ SPEC (λr. (case r of (nm, nds) ⇒ f (?n'' nm, nds)) ≤ SPEC (?P (a, b)))"
by (rule_tac SPEC_rule) auto
from prems order_trans[OF assm1 assm2] show ?case
by auto
qed
lemma expand_eq_expand⇩T:
assumes inv: "expand_inv φ n_ns"
shows "expand⇩T n_ns = expand n_ns"
unfolding expand⇩T_def expand_def
apply (rule RECT_eq_REC)
unfolding expand⇩T_def[symmetric]
using expand_term_prop[OF inv] apply auto
done
lemma expand_nofail:
assumes inv: "expand_inv φ n_ns"
shows "nofail (expand⇩T n_ns)"
using expand_term_prop[OF inv] by (simp add: pw_le_iff)
lemma [intro!]: "expand_inv φ (
⦇
name = expand_new_name expand_init,
incoming = {expand_init},
new = {φ},
old = {},
next = {} ⦈,
{})"
by (auto simp add: expand_inv_def)
definition create_graph :: "'a frml ⇒ 'a node set nres"
where
"create_graph φ ≡
do {
(_, nds) ← expand (
⦇
name = expand_new_name expand_init,
incoming = {expand_init},
new = {φ},
old = {},
next = {}
⦈::'a node,
{}::'a node set);
RETURN nds
}"
definition create_graph⇩T :: "'a frml ⇒ 'a node set nres"
where
"create_graph⇩T φ ≡ do {
(_, nds) ← expand⇩T (
⦇
name = expand_new_name expand_init,
incoming = {expand_init},
new = {φ},
old = {},
next = {}
⦈::'a node,
{}::'a node set);
RETURN nds
}"
lemma create_graph_eq_create_graph⇩T: "create_graph φ = create_graph⇩T φ"
unfolding create_graph⇩T_def create_graph_def
unfolding eq_iff
proof (standard, goal_cases)
case 1
then show ?case
by refine_mono (unfold expand_def expand⇩T_def, rule REC_le_RECT)
next
case 2
then show ?case
by (refine_mono, rule expand_eq_expand⇩T[unfolded eq_iff, THEN conjunct1]) auto
qed
lemma create_graph_finite: "create_graph φ ≤ SPEC finite"
unfolding create_graph_def expand_def
apply (intro refine_vcg)
apply (rule_tac order_trans)
apply (rule_tac REC_le_RECT)
apply (fold expand⇩T_def)
apply (rule_tac order_trans[OF expand_term_prop])
apply auto[1]
apply (rule_tac SPEC_rule)
apply auto
done
lemma create_graph_nofail: "nofail (create_graph φ)"
by (rule_tac pwD1[OF create_graph_finite]) auto
abbreviation
"create_graph_rslt_exist ξ nds
≡ ∃nd∈nds.
expand_init∈incoming nd
∧ (∀ψ∈old nd. ξ ⊨⇩r ψ) ∧ (∀ψ∈next nd. ξ ⊨⇩r X⇩r ψ)
∧ {η. ∃μ. μ U⇩r η ∈ old nd ∧ ξ ⊨⇩r η} ⊆ old nd"
lemma L4_7:
assumes "ξ ⊨⇩r φ"
shows "create_graph φ ≤ SPEC (create_graph_rslt_exist ξ)"
using assms unfolding create_graph_def
by (intro refine_vcg, rule_tac order_trans, rule_tac expand_prop_exist) (
auto simp add:expand_new_name_expand_init)
lemma expand_incoming_name_exist:
assumes "name (fst n_ns) > expand_init
∧ (∀nm∈incoming (fst n_ns). nm ≠ expand_init ⟶ nm∈name ` (snd n_ns))
∧ expand_assm_incoming n_ns ∧ expand_name_ident (snd n_ns)" (is "?Q n_ns")
and "∀nd∈snd n_ns.
name nd > expand_init
∧ (∀nm∈incoming nd. nm ≠ expand_init ⟶ nm∈name ` (snd n_ns))"
(is "?P (snd n_ns)")
shows "expand n_ns ≤ SPEC (λnm_nds. ?P (snd nm_nds))"
using assms
apply (rule_tac expand_rec_rule[where Φ="λn_ns. ?Q n_ns ∧ ?P (snd n_ns)"])
apply simp
apply (intro refine_vcg)
proof goal_cases
case (1 f x n ns)
then show ?case
proof (simp, clarify, goal_cases)
case prems: (1 _ _ nd)
{ assume "nd∈ns"
with prems have ?case by auto }
moreover
{ assume "nd∉ns"
with upd_incoming__elem[OF ‹nd∈upd_incoming n ns›]
obtain nd' where "nd'∈ns" and "nd = nd'⦇incoming :=
incoming n ∪ incoming nd'⦈ ∧
old nd' = old n ∧
next nd' = next n" by auto
with prems have ?case by auto }
ultimately show ?case by fast
qed
next
case (2 f x n ns)
then have step: "⋀x. ?Q x ∧ ?P (snd x) ⟹ f x ≤ SPEC (λx. ?P (snd x))"
and QP: "?Q (n, ns) ∧ ?P ns"
and f_sup: "⋀x. f x ≤ expand x" by auto
show ?case
unfolding ‹x = (n, ns)›
using QP expand_new_name_expand_init
proof (rule_tac step, goal_cases)
case prems: 1
then have name_less: "name n < expand_new_name (name n)"
by auto
moreover
from prems name_less have "∀nm∈incoming n. nm < expand_new_name (name n)"
by auto
moreover
from prems name_less have **: "∀q∈ns. name q < expand_new_name (name n) ∧
(∀nm∈incoming q. nm < expand_new_name (name n))"
by force
moreover
from QP have "∃!q'. (q' = n ∨ q' ∈ ns) ∧ name n = name q'"
by force
moreover
have "∀q∈ns. ∃!q'.
(q' = n ∨ q' ∈ ns) ∧
name q = name q' " using QP by auto
ultimately show ?case using prems by simp
qed
next
case 3
then show ?case by simp
next
case 4
then show ?case by simp
next
case 5
then show ?case by simp
next
case 6
then show ?case by simp
next
case 7
then show ?case by simp
next
case prems: (8 f x n ns ψ)
then have goal_assms: "ψ ∈ new n ∧ (∃ν μ. ψ = ν or⇩r μ ∨ ψ = ν U⇩r μ ∨ ψ = ν R⇩r μ)"
by (cases ψ) auto
with prems have QP: "?Q (n, ns) ∧ ?P ns"
and step: "⋀x. ?Q x ∧ ?P (snd x) ⟹ f x ≤ SPEC (λx'. ?P (snd x'))"
and f_sup: "⋀x. f x ≤ expand x" by auto
let ?x = "(n⦇new := new n - {ψ}, new := new1 ψ ∪ new (n⦇new := new n - {ψ}⦈),
old := {ψ} ∪ old (n⦇new := new n - {ψ}⦈),
next := next1 ψ ∪ next (n⦇new := new n - {ψ}⦈)⦈, ns)"
let ?props = "λx r. expand_rslt_incoming r
∧ expand_rslt_name x r
∧ expand_name_ident (snd r)"
show ?case
using goal_assms QP unfolding case_prod_unfold ‹x = (n, ns)›
proof (rule_tac SPEC_rule_weak_nested2[where Q = "?props ?x"], goal_cases)
case 1
then show ?case
by (rule_tac order_trans, rule_tac f_sup, rule_tac expand_name_propag) simp
next
case 2
then show ?case
by (rule_tac SPEC_rule_param2[where P = "λx r. ?P (snd r)"], rule_tac step)
auto
next
case (3 nm nds)
then show ?case
proof (rule_tac SPEC_rule_weak[where P = "λx r. ?P (snd r)"
and Q = "λx r. expand_rslt_exist_eq x r ∧ ?props x r"], goal_cases)
case 1
then show ?case
by (rule_tac SPEC_rule_conjI,
rule_tac order_trans,
rule_tac f_sup,
rule_tac expand_rslt_exist_eq,
rule_tac order_trans,
rule_tac f_sup,
rule_tac expand_name_propag) force
next
case 2
then show ?case
by (rule_tac SPEC_rule_param2[where P = "λx r. ?P (snd r)"],
rule_tac step) force
next
case (3 nm' nds')
then show ?case
by simp
qed
qed
qed
lemma create_graph__incoming_name_exist:
"create_graph φ ≤ SPEC (λnds. ∀nd∈nds. expand_init < name nd ∧ (∀nm∈incoming nd. nm ≠ expand_init ⟶ nm∈name ` nds))"
unfolding create_graph_def
by (intro refine_vcg,
rule_tac order_trans,
rule_tac expand_incoming_name_exist) (
auto simp add:expand_new_name_expand_init)
abbreviation
"expand_rslt_all__ex_equiv ξ nd nds ≡
(∃nd'∈nds.
name nd ∈ incoming nd'
∧ (∀ψ∈old nd'. suffix 1 ξ ⊨⇩r ψ) ∧ (∀ψ∈next nd'. suffix 1 ξ ⊨⇩r X⇩r ψ)
∧ {η. ∃μ. μ U⇩r η ∈ old nd' ∧ suffix 1 ξ ⊨⇩r η} ⊆ old nd')"
abbreviation
"expand_rslt_all ξ n_ns nm_nds ≡
(∀nd∈snd nm_nds. name nd ∉ name ` (snd n_ns) ∧
(∀ψ∈old nd. ξ ⊨⇩r ψ) ∧ (∀ψ∈next nd. ξ ⊨⇩r X⇩r ψ)
⟶ expand_rslt_all__ex_equiv ξ nd (snd nm_nds))"
lemma expand_prop_all:
assumes "expand_assm_incoming n_ns ∧ expand_name_ident (snd n_ns)" (is "?Q n_ns")
shows "expand n_ns ≤ SPEC (expand_rslt_all ξ n_ns)"
(is "_ ≤ SPEC (?P n_ns)")
using assms
apply (rule_tac expand_rec_rule[where Φ="?Q"])
apply simp
apply (intro refine_vcg)
proof goal_cases
case 1
then show ?case by (simp, rule_tac upd_incoming__ident) simp_all
next
case (2 f x n ns)
then have step: "⋀x. ?Q x ⟹ f x ≤ SPEC (?P x)"
and Q: "?Q (n, ns)"
and f_sup: "⋀x. f x ≤ expand x" by auto
let ?x = "(⦇name = expand_new_name (name n),
incoming = {name n}, new = next n, old = {}, next = {}⦈, {n} ∪ ns)"
from Q have name_le: "name n < expand_new_name (name n)" by auto
show ?case
unfolding ‹x = (n, ns)›
proof (rule_tac SPEC_rule_weak[where
Q = "λp r.
(expand_assm_exist (suffix 1 ξ) ?x ⟶ expand_rslt_exist (suffix 1 ξ) ?x r)
∧ expand_rslt_exist_eq p r ∧ (expand_name_ident (snd r))"], goal_cases)
case 1
then show ?case
proof (rule_tac SPEC_rule_conjI,
rule_tac order_trans,
rule_tac f_sup,
rule_tac expand_prop_exist,
rule_tac SPEC_rule_conjI,
rule_tac order_trans,
rule_tac f_sup,
rule_tac expand_rslt_exist_eq,
rule_tac order_trans,
rule_tac f_sup,
rule_tac expand_name_propag__name_ident,
goal_cases)
case 1
then show ?case using Q name_le by force
qed
next
case 2
then show ?case using Q name_le by (rule_tac step) force
next
case prems: (3 nm nds)
then obtain n' where "n'∈nds"
and eq_node: "expand_rslt_exist_eq__node n n'" by auto
with prems have ex1_name: "∃!q∈nds. name n = name q" by auto
then have nds_eq: "nds = {n'} ∪ {x ∈ nds. name n ≠ name x}"
using eq_node ‹n'∈nds› by blast
have name_notin: "name n ∉ name ` ns" using Q by auto
from prems have P_x: "expand_rslt_all ξ ?x (nm, nds)" by fast
show ?case
unfolding snd_conv
proof clarify
fix nd
assume "nd ∈ nds" and name_img: "name nd ∉ name ` ns"
and nd_old_equiv: "∀ψ∈old nd. ξ ⊨⇩r ψ"
and nd_next_equiv: "∀ψ∈next nd. ξ ⊨⇩r X⇩r ψ"
show "expand_rslt_all__ex_equiv ξ nd nds"
proof (cases "name nd = name n")
case True
with nds_eq eq_node ‹nd∈nds› have "nd = n'" by auto
with prems(1)[THEN conjunct1, simplified]
nd_old_equiv nd_next_equiv eq_node
show ?thesis by simp
next
case False
with name_img ‹nd ∈ nds› nd_old_equiv nd_next_equiv P_x
show ?thesis by simp
qed
qed
qed
next
case 3
then show ?case by auto
next
case prems: (4 f)
then have step: "⋀x. ?Q x ⟹ f x ≤ SPEC (?P x)" by simp
from prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
case prems: (5 f)
then have step: "⋀x. ?Q x ⟹ f x ≤ SPEC (?P x)" by simp
from prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
case 6
then show ?case by auto
next
case prems: (7 f)
then have step: "⋀x. ?Q x ⟹ f x ≤ SPEC (?P x)" by simp
from prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
case prems: (8 f x n ns ψ)
then have goal_assms: "ψ ∈ new n ∧ (∃ν μ. ψ = ν or⇩r μ ∨ ψ = ν U⇩r μ ∨ ψ = ν R⇩r μ)"
by (cases ψ) auto
from prems have Q: "?Q (n, ns)"
and step: "⋀x. ?Q x ⟹ f x ≤ SPEC (?P x)"
and f_sup: "⋀x. f x ≤ expand x" by auto
let ?x = "(n⦇new := new n - {ψ}, new := new1 ψ ∪ new (n⦇new := new n - {ψ}⦈),
old := {ψ} ∪ old (n⦇new := new n - {ψ}⦈),
next := next1 ψ ∪ next (n⦇new := new n - {ψ}⦈)
⦈, ns)"
let ?props = "λx r. expand_rslt_incoming r
∧ expand_rslt_name x r
∧ expand_name_ident (snd r)"
show ?case
using goal_assms Q
unfolding case_prod_unfold ‹x = (n, ns)›
proof (rule_tac SPEC_rule_weak_nested2[where Q = "?props ?x"], goal_cases)
case 1
then show ?case
by (rule_tac order_trans, rule_tac f_sup, rule_tac expand_name_propag) simp
next
case 2
then show ?case
by (rule_tac SPEC_rule_param2[where P = "?P"], rule_tac step) auto
next
case prems: (3 nm nds)
then show ?case
proof (rule_tac SPEC_rule_weak[where
P = "?P" and
Q = "λx r. expand_rslt_exist_eq x r ∧ ?props x r"], goal_cases)
case 1
then show ?case
by (rule_tac SPEC_rule_conjI,
rule_tac order_trans,
rule_tac f_sup,
rule_tac expand_rslt_exist_eq,
rule_tac order_trans,
rule_tac f_sup,
rule_tac expand_name_propag) auto
next
case 2
then show ?case
by (rule_tac SPEC_rule_param2[where P = "?P"], rule_tac step) auto
next
case prems': (3 nm' nds')
then have P_x: "?P (n, ns) (nm, nds)"
and P_x': "?P (n, nds) (nm', nds')" by simp_all
show ?case
unfolding snd_conv
proof clarify
fix nd
assume "nd∈nds'"
and name_nd_notin: "name nd ∉ name ` ns"
and old_equiv: "∀ψ∈old nd. ξ ⊨⇩r ψ"
and next_equiv: "∀ψ∈next nd. ξ ⊨⇩r X⇩r ψ"
show "expand_rslt_all__ex_equiv ξ nd nds'"
proof (cases "name nd ∈ name ` nds")
case True
then obtain n' where "n' ∈ nds" and "name nd = name n'" by auto
with prems' obtain nd' where "nd'∈nds'"
and nd'_eq: "expand_rslt_exist_eq__node n' nd'"
by auto
moreover from prems' have "∀q∈nds'. ∃!q'∈nds'. name q = name q'"
by simp
ultimately have "nd' = nd"
using ‹name nd = name n'› ‹nd ∈ nds'› by auto
with nd'_eq have n'_eq: "expand_rslt_exist_eq__node n' nd"
by simp
then have "name n'∉name ` ns" and "∀ψ∈old n'. ξ ⊨⇩r ψ" and "∀ψ∈next n'. ξ ⊨⇩r X⇩r ψ"
using name_nd_notin old_equiv next_equiv ‹n' ∈ nds›
by auto
then have "expand_rslt_all__ex_equiv ξ n' nds" (is "∃nd'∈nds. ?sthm n' nd'")
using P_x ‹n' ∈ nds› unfolding snd_conv by blast
then obtain sucnd where sucnd: "sucnd∈nds" and sthm: "?sthm n' sucnd"
by blast
moreover
from prems' sucnd sthm obtain sucnd' where "sucnd'∈nds'"
and sucnd'_eq: "expand_rslt_exist_eq__node sucnd sucnd'"
by auto
ultimately have "?sthm n' sucnd'" by auto
then show ?thesis
using ‹sucnd' ∈ nds'›
unfolding ‹name nd = name n'› by blast
next
case False
with ‹nd ∈ nds'› P_x' old_equiv next_equiv
show ?thesis unfolding snd_conv by blast
qed
qed
qed
qed
qed
abbreviation
"create_graph_rslt_all ξ nds
≡ ∀q∈nds. (∀ψ∈old q. ξ ⊨⇩r ψ) ∧ (∀ψ∈next q. ξ ⊨⇩r X⇩r ψ)
⟶ (∃q'∈nds. name q ∈ incoming q'
∧ (∀ψ∈old q'. suffix 1 ξ ⊨⇩r ψ)
∧ (∀ψ∈next q'. suffix 1 ξ ⊨⇩r X⇩r ψ)
∧ {η. ∃μ. μ U⇩r η ∈ old q' ∧ suffix 1 ξ ⊨⇩r η} ⊆ old q')"
lemma L4_5: "create_graph φ ≤ SPEC (create_graph_rslt_all ξ)"
unfolding create_graph_def
apply (refine_vcg expand_prop_all)
apply (auto simp add:expand_new_name_expand_init)
done
subsection ‹Creation of GBA›
text ‹This section formalizes the second part of the algorithm, that creates
the actual generalized B\"uchi automata from the set of nodes.›
definition create_gba_from_nodes :: "'a frml ⇒ 'a node set ⇒ ('a node, 'a set) gba_rec"
where "create_gba_from_nodes φ qs ≡ ⦇
g_V = qs,
g_E = {(q, q'). q∈qs ∧ q'∈qs ∧ name q∈incoming q'},
g_V0 = {q∈qs. expand_init∈incoming q},
gbg_F = {{q∈qs. μ U⇩r η∈old q ⟶ η∈old q}|μ η. μ U⇩r η ∈ subfrmlsr φ},
gba_L = λq l. q∈qs ∧ {p. prop⇩r(p)∈old q}⊆l ∧ {p. nprop⇩r(p)∈old q} ∩ l = {}
⦈"
end
locale create_gba_from_nodes_precond =
fixes φ :: "'a ltlr"
fixes qs :: "'a node set"
assumes res: "inres (create_graph φ) qs"
begin
lemma finite_qs[simp, intro!]: "finite qs"
using res create_graph_finite by (auto simp add: pw_le_iff)
lemma create_gba_from_nodes__invar: "gba (create_gba_from_nodes φ qs)"
using [[simproc finite_Collect]]
apply unfold_locales
apply (auto
intro!: finite_vimageI subfrmlsr_finite injI
simp: create_gba_from_nodes_def)
done
sublocale gba: gba "create_gba_from_nodes φ qs"
by (rule create_gba_from_nodes__invar)
lemma create_gba_from_nodes__fin: "finite (g_V (create_gba_from_nodes φ qs))"
unfolding create_gba_from_nodes_def by auto
lemma create_gba_from_nodes__ipath:
"ipath gba.E r ⟷ (∀i. r i ∈qs ∧ name (r i)∈incoming (r (Suc i)))"
unfolding create_gba_from_nodes_def ipath_def
by auto
lemma create_gba_from_nodes__is_run:
"gba.is_run r ⟷ expand_init ∈ incoming (r 0)
∧ (∀i. r i∈qs ∧ name (r i)∈incoming (r (Suc i)))"
unfolding gba.is_run_def
apply (simp add: create_gba_from_nodes__ipath)
apply (auto simp: create_gba_from_nodes_def)
done
context
begin
abbreviation
"auto_run_j j ξ q ≡
(∀ψ∈old q. suffix j ξ ⊨⇩r ψ) ∧ (∀ψ∈next q. suffix j ξ ⊨⇩r X⇩r ψ) ∧
{η. ∃μ. μ U⇩r η ∈ old q ∧ suffix j ξ ⊨⇩r η} ⊆ old q"
fun auto_run :: "['a interprt, 'a node set] ⇒ 'a node word"
where
"auto_run ξ nds 0
= (SOME q. q∈nds ∧ expand_init ∈ incoming q ∧ auto_run_j 0 ξ q)"
| "auto_run ξ nds (Suc k)
= (SOME q'. q'∈nds ∧ name (auto_run ξ nds k) ∈ incoming q'
∧ auto_run_j (Suc k) ξ q')"
lemma run_propag_on_create_graph:
assumes "ipath gba.E σ"
shows "σ k∈qs ∧ name (σ k)∈incoming (σ (k+1))"
using assms
by (auto simp: create_gba_from_nodes__ipath)
lemma expand_false_propag:
assumes "false⇩r ∉ old (fst n_ns) ∧ (∀nd∈snd n_ns. false⇩r ∉ old nd)"
(is "?Q n_ns")
shows "expand n_ns ≤ SPEC (λnm_nds. ∀nd∈snd nm_nds. false⇩r ∉ old nd)"
using assms
proof (rule_tac expand_rec_rule[where Φ="?Q"], simp, intro refine_vcg, goal_cases)
case 1
then show ?case by (simp, rule_tac upd_incoming__ident) auto
next
case 8
then show ?case by (rule_tac SPEC_rule_nested2) auto
qed auto
lemma false_propag_on_create_graph: "create_graph φ ≤ SPEC (λnds. ∀nd∈nds. false⇩r ∉ old nd)"
unfolding create_graph_def
by (intro refine_vcg, rule_tac order_trans, rule_tac expand_false_propag) auto
lemma expand_and_propag:
assumes "μ and⇩r η ∈ old (fst n_ns)
⟶ {μ, η} ⊆ old (fst n_ns) ∪ new (fst n_ns)" (is "?Q n_ns")
and "∀nd∈snd n_ns. μ and⇩r η ∈ old nd ⟶ {μ, η} ⊆ old nd" (is "?P (snd n_ns)")
shows "expand n_ns ≤ SPEC (λnm_nds. ?P (snd nm_nds))"
using assms
proof (rule_tac expand_rec_rule[where Φ="λx. ?Q x ∧ ?P (snd x)"],
simp, intro refine_vcg, goal_cases)
case 1
then show ?case by (simp, rule_tac upd_incoming__ident) auto
next
case prems: (4 f x n ns)
then have step: "⋀x. ?Q x ∧ ?P (snd x) ⟹ f x ≤ SPEC (λx'. ?P (snd x'))" by simp
with prems show ?case by (rule_tac step) auto
next
case prems: (5 f x n ns)
then have step: "⋀x. ?Q x ∧ ?P (snd x) ⟹ f x ≤ SPEC (λx'. ?P (snd x'))" by simp
with prems show ?case by (rule_tac step) auto
next
case (6 f x n ns)
then show ?case by auto
next
case prems: (7 f x n ns)
then have step: "⋀x. ?Q x ∧ ?P (snd x) ⟹ f x ≤ SPEC (λx'. ?P (snd x'))" by simp
with prems show ?case by (rule_tac step) auto
next
case prems: (8 f x n ns ψ)
then have goal_assms: "ψ ∈ new n
∧ ¬ (∃q. ψ = prop⇩r(q) ∨ ψ = nprop⇩r(q))
∧ ψ ≠ true⇩r ∧ ψ ≠ false⇩r
∧ ¬ (∃ν μ. ψ = ν and⇩r μ ∨ ψ = X⇩r ν)
∧ (∃ν μ. ψ = ν or⇩r μ ∨ ψ = ν U⇩r μ ∨ ψ = ν R⇩r μ)"
by (cases ψ) auto
from prems have QP: "?Q (n, ns) ∧ ?P ns"
and step: "⋀x. ?Q x ∧ ?P (snd x) ⟹ f x ≤ SPEC (λx'. ?P (snd x'))"
by simp_all
show ?case
using goal_assms QP unfolding case_prod_unfold ‹x = (n, ns)›
proof (rule_tac SPEC_rule_nested2, goal_cases)
case 1
then show ?case by (rule_tac step) auto
next
case 2
then show ?case by (rule_tac step) auto
qed
qed auto
lemma and_propag_on_create_graph:
"create_graph φ ≤ SPEC (λnds. ∀nd∈nds. μ and⇩r η ∈ old nd ⟶ {μ, η} ⊆ old nd)"
unfolding create_graph_def
by (intro refine_vcg, rule_tac order_trans, rule_tac expand_and_propag) auto
lemma expand_or_propag:
assumes "μ or⇩r η ∈ old (fst n_ns)
⟶ {μ, η} ∩ (old (fst n_ns) ∪ new (fst n_ns)) ≠ {}" (is "?Q n_ns")
and "∀nd∈snd n_ns. μ or⇩r η ∈ old nd ⟶ {μ, η} ∩ old nd ≠ {}"
(is "?P (snd n_ns)")
shows "expand n_ns ≤ SPEC (λnm_nds. ?P (snd nm_nds))"
using assms
proof (rule_tac expand_rec_rule[where Φ="λx. ?Q x ∧ ?P (snd x)"],
simp, intro refine_vcg, goal_cases)
case 1
then show ?case by (simp, rule_tac upd_incoming__ident) auto
next
case prems: (4 f x n ns)
then have step: "⋀x. ?Q x ∧ ?P (snd x) ⟹ f x ≤ SPEC (λx'. ?P (snd x'))" by simp
with prems show ?case by (rule_tac step) auto
next
case prems: (5 f x n ns)
then have step: "⋀x. ?Q x ∧ ?P (snd x) ⟹ f x ≤ SPEC (λx'. ?P (snd x'))" by simp
with prems show ?case by (rule_tac step) auto
next
case (6 f x n ns)
then show ?case by auto
next
case prems: (7 f x n ns)
then have step: "⋀x. ?Q x ∧ ?P (snd x) ⟹ f x ≤ SPEC (λx'. ?P (snd x'))" by simp
with prems show ?case by (rule_tac step) auto
next
case prems: (8 f x n ns ψ)
then have goal_assms: "ψ ∈ new n
∧ ¬ (∃q. ψ = prop⇩r(q) ∨ ψ = nprop⇩r(q))
∧ ψ ≠ true⇩r ∧ ψ ≠ false⇩r
∧ ¬ (∃ν μ. ψ = ν and⇩r μ ∨ ψ = X⇩r ν)
∧ (∃ν μ. ψ = ν or⇩r μ ∨ ψ = ν U⇩r μ ∨ ψ = ν R⇩r μ)"
by (cases ψ) auto
from prems have QP: "?Q (n, ns) ∧ ?P ns"
and step: "⋀x. ?Q x ∧ ?P (snd x) ⟹ f x ≤ SPEC (λx'. ?P (snd x'))"
by simp_all
show ?case
using goal_assms QP
unfolding case_prod_unfold ‹x = (n, ns)›
proof (rule_tac SPEC_rule_nested2, goal_cases)
case 1
then show ?case by (rule_tac step) auto
next
case 2
then show ?case by (rule_tac step) auto
qed
qed auto
lemma or_propag_on_create_graph:
"create_graph φ ≤ SPEC (λnds. ∀nd∈nds. μ or⇩r η ∈ old nd ⟶ {μ, η} ∩ old nd ≠ {})"
unfolding create_graph_def
by (intro refine_vcg, rule_tac order_trans, rule_tac expand_or_propag) auto
abbreviation
"next_propag__assm μ n_ns ≡
(X⇩r μ ∈ old (fst n_ns) ⟶ μ ∈ next (fst n_ns))
∧ (∀nd∈snd n_ns. X⇩r μ ∈ old nd ∧ name nd ∈ incoming (fst n_ns)
⟶ μ ∈ old (fst n_ns) ∪ new (fst n_ns))"
abbreviation
"next_propag__rslt μ ns ≡
∀nd∈ns. ∀nd'∈ns. X⇩r μ ∈ old nd ∧ name nd ∈ incoming nd' ⟶ μ ∈ old nd'"
lemma expand_next_propag:
fixes n_ns :: "_ × 'a node set"
assumes "next_propag__assm μ n_ns
∧ next_propag__rslt μ (snd n_ns)
∧ expand_assm_incoming n_ns
∧ expand_name_ident (snd n_ns)" (is "?Q n_ns")
shows "expand n_ns ≤ SPEC (λr. next_propag__rslt μ (snd r))"
(is "_ ≤ SPEC ?P")
using assms
proof (rule_tac expand_rec_rule[where Φ="?Q"], simp, intro refine_vcg, goal_cases)
case (1 f x n ns)
then show ?case
proof (simp, rule_tac upd_incoming__ident, goal_cases)
case prems: 1
{
fix nd :: "'a node" and nd' :: "'a node"
assume "nd∈ns" and nd'_elem: "nd'∈upd_incoming n ns"
have "μ ∈ old nd'" if *: "X⇩r μ ∈ old nd" and **: "name nd ∈ incoming nd'"
proof (cases "nd'∈ns")
case True
with prems * ** show ?thesis using ‹nd∈ns› by auto
next
case False
with upd_incoming__elem[of nd' n ns] nd'_elem * **
obtain nd'' where "nd''∈ns"
and nd'_eq: "nd' = nd''⦇incoming := incoming n ∪ incoming nd''⦈"
and old_eq: "old nd'' = old n" by auto
have "μ ∈ old nd'"
proof (cases "name nd ∈ incoming n")
case True
with prems * ‹nd∈ns› have "μ ∈ old n" by auto
then show ?thesis using nd'_eq old_eq by simp
next
case False
then have "name nd ∈ incoming nd''"
using ‹name nd ∈incoming nd'› nd'_eq by simp
then show ?thesis
unfolding nd'_eq using ‹nd∈ns› ‹nd''∈ns› * prems by auto
qed
then show ?thesis by auto
qed
}
then show ?case by auto
next
case 2
then show ?case by simp
qed
next
case prems: (2 f x n ns)
then have step: "⋀x. ?Q x ⟹ f x ≤ SPEC ?P"
and f_sup: "⋀x. f x ≤ expand x" by auto
from prems have Q: "?Q (n, ns)" by auto
from Q have name_le: "name n < expand_new_name (name n)" by auto
let ?x' = "(⦇name = expand_new_name (name n),
incoming = {name n}, new = next n,
old = {}, next = {}⦈, {n} ∪ ns)"
have Q'1: "expand_assm_incoming ?x'∧ expand_name_ident (snd ?x')"
using ‹new n = {}› Q[THEN conjunct2, THEN conjunct2] name_le by force
have Q'2: "next_propag__assm μ ?x' ∧ next_propag__rslt μ (snd ?x')"
using Q ‹new n = {}› by auto
show ?case
using ‹new n = {}›
unfolding ‹x = (n, ns)›
proof (rule_tac SPEC_rule_weak[where
Q = "λ_ r. expand_name_ident (snd r)" and P = "λ_. ?P"], goal_cases)
case 1
then show ?case
using Q'1
by (rule_tac order_trans,
rule_tac f_sup,
rule_tac expand_name_propag__name_ident) auto
next
case 2
then show ?case
using Q'1 Q'2 by (rule_tac step) simp
next
case (3 nm nds)
then show ?case by simp
qed
next
case 3
then show ?case by auto
next
case prems: (4 f)
then have step: "⋀x. ?Q x ⟹ f x ≤ SPEC ?P" by simp
from prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
case prems: (5 f)
then have step: "⋀x. ?Q x ⟹ f x ≤ SPEC ?P" by simp
from prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
case 6
then show ?case by auto
next
case prems: (7 f)
then have step: "⋀x. ?Q x ⟹ f x ≤ SPEC ?P" by simp
from prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
case prems: (8 f x n ns ψ)
then have goal_assms: "ψ ∈ new n ∧ (∃ν μ. ψ = ν or⇩r μ ∨ ψ = ν U⇩r μ ∨ ψ = ν R⇩r μ)"
by (cases ψ) auto
from prems have Q: "?Q (n, ns)"
and step: "⋀x. ?Q x ⟹ f x ≤ SPEC ?P"
and f_sup: "⋀x. f x ≤ expand x"
by auto
let ?x = "(n⦇new := new n - {ψ}, new := new1 ψ ∪ new (n⦇new := new n - {ψ}⦈),
old := {ψ} ∪ old (n⦇new := new n - {ψ}⦈),
next := next1 ψ ∪ next (n⦇new := new n - {ψ}⦈)
⦈, ns)"
let ?props = "λx r. expand_rslt_exist_eq x r
∧ expand_rslt_incoming r ∧ expand_rslt_name x r ∧ expand_name_ident (snd r)"
show ?case
using goal_assms Q unfolding case_prod_unfold ‹x = (n, ns)›
proof (rule_tac SPEC_rule_weak_nested2[where Q = "?props ?x"], goal_cases)
case 1 then
show ?case
by (rule_tac SPEC_rule_conjI,
rule_tac order_trans,
rule_tac f_sup,
rule_tac expand_rslt_exist_eq,
rule_tac order_trans,
rule_tac f_sup,
rule_tac expand_name_propag) simp+
next
case 2
then show ?case
by (rule_tac SPEC_rule_param2[where P = "λ_. ?P"], rule_tac step) auto
next
case prems': (3 nm nds)
let ?x' = "(n⦇new := new n - {ψ},
name := fst (nm, nds),
new := new2 ψ ∪ new (n⦇new := new n - {ψ}⦈),
old := {ψ} ∪ old (n⦇new := new n - {ψ}⦈)⦈, nds)"
from prems' show ?case
proof (rule_tac step, goal_cases)
case prems'': 1
then have "expand_assm_incoming ?x'" by auto
moreover
from prems'' have nds_ident: "expand_name_ident (snd ?x')" by simp
moreover
have "X⇩r μ ∈ old (fst ?x') ⟶ μ∈next (fst ?x')"
using Q[THEN conjunct1] goal_assms by auto
moreover
from prems'' have "next_propag__rslt μ (snd ?x')" by simp
moreover
from prems'' have name_nds_eq: "name ` nds = name ` ns ∪ name ` {nd∈nds. name nd ≥ name n}"
by auto
have "∀nd∈nds. (X⇩r μ ∈ old nd ∧ name nd ∈ incoming (fst ?x'))
⟶ μ∈old (fst ?x')∪new (fst ?x')"
(is "∀nd∈nds. ?assm (fst ?x') nd ⟶ ?concl (fst ?x') nd")
proof
fix nd
assume "nd∈nds"
{ assume loc_assm: "name nd∈name ` ns"
then obtain n' where n': "n'∈ns" "name n' = name nd" by auto
moreover
from prems'' n' obtain nd' where "nd'∈nds"
and n'_nd'_eq: "expand_rslt_exist_eq__node n' nd'"
by auto
ultimately have "nd = nd'"
using nds_ident ‹nd∈nds› loc_assm by auto
moreover from prems'' have "?assm n n' ⟶ ?concl n n'"
using ‹n'∈ns› by auto
ultimately have "?assm (fst ?x') nd ⟶ ?concl (fst ?x') nd"
using n'_nd'_eq by auto }
moreover
{ assume "name nd∉name ` ns"
with name_nds_eq ‹nd∈nds› have "name nd ≥ name n" by auto
with prems'' have "¬ (?assm (fst ?x') nd)" by auto }
ultimately show "?assm (fst ?x') nd ⟶ ?concl (fst ?x') nd" by auto
qed
ultimately show ?case by simp
qed
qed
qed
lemma next_propag_on_create_graph:
"create_graph φ ≤ SPEC (λnds. ∀n∈nds. ∀n'∈nds. X⇩r μ∈old n ∧ name n∈incoming n' ⟶ μ∈old n')"
unfolding create_graph_def
apply (refine_vcg expand_next_propag)
apply (auto simp add:expand_new_name_expand_init)
done
abbreviation
"release_propag__assm μ η n_ns ≡
(μ R⇩r η ∈ old (fst n_ns)
⟶ {μ, η}⊆old (fst n_ns)∪new (fst n_ns) ∨
(η∈old (fst n_ns)∪new (fst n_ns)) ∧ μ R⇩r η ∈ next (fst n_ns))
∧ (∀nd∈snd n_ns.
μ R⇩r η ∈ old nd ∧ name nd ∈ incoming (fst n_ns)
⟶ {μ, η}⊆old nd ∨
(η∈old nd ∧ μ R⇩r η ∈ old (fst n_ns)∪new (fst n_ns)))"
abbreviation
"release_propag__rslt μ η ns ≡
∀nd∈ns.
∀nd'∈ns.
μ R⇩r η ∈ old nd ∧ name nd ∈ incoming nd'
⟶ {μ, η}⊆old nd ∨
(η∈old nd ∧ μ R⇩r η ∈ old nd')"
lemma expand_release_propag:
fixes n_ns :: "_ × 'a node set"
assumes "release_propag__assm μ η n_ns
∧ release_propag__rslt μ η (snd n_ns)
∧ expand_assm_incoming n_ns
∧ expand_name_ident (snd n_ns)" (is "?Q n_ns")
shows "expand n_ns ≤ SPEC (λr. release_propag__rslt μ η (snd r))"
(is "_ ≤ SPEC ?P")
using assms
proof (rule_tac expand_rec_rule[where Φ="?Q"], simp, intro refine_vcg, goal_cases)
case (1 f x n ns)
then show ?case
proof (simp, rule_tac upd_incoming__ident, goal_cases)
case prems: 1
{ fix nd :: "'a node" and nd' :: "'a node"
let ?V_prop = "μ R⇩r η ∈ old nd ∧ name nd ∈ incoming nd'
⟶ {μ, η} ⊆ old nd ∨ η ∈ old nd ∧ μ R⇩r η ∈ old nd'"
assume "nd∈ns" and nd'_elem: "nd'∈upd_incoming n ns"
{ assume "nd'∈ns"
with prems have ?V_prop using ‹nd∈ns› by auto }
moreover
{ assume "nd'∉ns"
and V_in_nd: "μ R⇩r η ∈ old nd" and "name nd ∈incoming nd'"
with upd_incoming__elem[of nd' n ns] nd'_elem
obtain nd'' where "nd''∈ns"
and nd'_eq: "nd' = nd''⦇incoming := incoming n ∪ incoming nd''⦈"
and old_eq: "old nd'' = old n"
by auto
{ assume "name nd ∈ incoming n"
with prems V_in_nd ‹nd∈ns›
have "{μ, η} ⊆ old nd ∨ η ∈ old nd ∧ μ R⇩r η ∈ old n"
by auto
then have "{μ, η} ⊆ old nd ∨ η ∈ old nd ∧ μ R⇩r η ∈ old nd'"
using nd'_eq old_eq by simp }
moreover
{ assume "name nd ∉ incoming n"
then have "name nd ∈ incoming nd''"
using ‹name nd ∈incoming nd'› nd'_eq by simp
then have "{μ, η} ⊆ old nd ∨ η ∈ old nd ∧ μ R⇩r η ∈ old nd'"
unfolding nd'_eq
using prems ‹nd∈ns› ‹nd''∈ns› V_in_nd by auto }
ultimately have "{μ, η} ⊆ old nd ∨ η ∈ old nd ∧ μ R⇩r η ∈ old nd'"
by fast
}
ultimately have ?V_prop by auto
}
then show ?case by auto
next
case 2
then show ?case by simp
qed
next
case prems: (2 f x n ns)
then have step: "⋀x. ?Q x ⟹ f x ≤ SPEC ?P"
and f_sup: "⋀x. f x ≤ expand x" by auto
from prems have Q: "?Q (n, ns)" by auto
from Q have name_le: "name n < expand_new_name (name n)" by auto
let ?x' = "(⦇name = expand_new_name (name n),
incoming = {name n}, new = next n,
old = {}, next = {}⦈, {n} ∪ ns)"
have Q'1: "expand_assm_incoming ?x'∧ expand_name_ident (snd ?x')"
using ‹new n = {}› Q[THEN conjunct2, THEN conjunct2] name_le by force
have Q'2: "release_propag__assm μ η ?x' ∧ release_propag__rslt μ η (snd ?x')"
using Q ‹new n = {}› by auto
show ?case using ‹new n = {}› unfolding ‹x = (n, ns)›
proof (rule_tac SPEC_rule_weak[where
Q = "λ_ r. expand_name_ident (snd r)" and P = "λ_. ?P"], goal_cases)
case 1
then show ?case using Q'1
by (rule_tac order_trans,
rule_tac f_sup,
rule_tac expand_name_propag__name_ident) auto
next
case 2
then show ?case using Q'1 Q'2 by (rule_tac step) simp
next
case (3 nm nds)
then show ?case by simp
qed
next
case 3 then show ?case by auto
next
case prems: (4 f x n ns ψ)
then have goal_assms: "ψ ∈ new n ∧ (∃q. ψ = prop⇩r(q) ∨ ψ = nprop⇩r(q))" by simp
from prems have step: "⋀x. ?Q x ⟹ f x ≤ SPEC ?P" and Q: "?Q (n, ns)"
by simp_all
show ?case
using Q goal_assms by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
case prems: (5 f x n ns ψ)
then have goal_assms: "ψ ∈ new n ∧ ψ = true⇩r" by simp
from prems have step: "⋀x. ?Q x ⟹ f x ≤ SPEC ?P" and Q: "?Q (n, ns)"
by simp_all
show ?case using Q goal_assms by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
case 6
then show ?case by auto
next
case prems: (7 f x n ns ψ)
then have goal_assms: "ψ ∈ new n ∧ (∃ν μ. ψ = ν and⇩r μ ∨ ψ = X⇩r ν)" by simp
from prems have step: "⋀x. ?Q x ⟹ f x ≤ SPEC ?P" and Q: "?Q (n, ns)"
by simp_all
show ?case using Q goal_assms by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
case prems: (8 f x n ns ψ)
then have goal_assms: "ψ ∈ new n ∧ (∃ν μ. ψ = ν or⇩r μ ∨ ψ = ν U⇩r μ ∨ ψ = ν R⇩r μ)"
by (cases ψ) auto
from prems have Q: "?Q (n, ns)"
and step: "⋀x. ?Q x ⟹ f x ≤ SPEC ?P"
and f_sup: "⋀x. f x ≤ expand x" by auto
let ?x = "(n⦇new := new n - {ψ}, new := new1 ψ ∪ new (n⦇new := new n - {ψ}⦈),
old := {ψ} ∪ old (n⦇new := new n - {ψ}⦈),
next := next1 ψ ∪ next (n⦇new := new n - {ψ}⦈)
⦈, ns)"
let ?props = "λx r. expand_rslt_exist_eq x r
∧ expand_rslt_incoming r ∧ expand_rslt_name x r ∧ expand_name_ident (snd r)"
show ?case using goal_assms Q unfolding case_prod_unfold ‹x = (n, ns)›
proof (rule_tac SPEC_rule_weak_nested2[where Q = "?props ?x"], goal_cases)
case 1
then show ?case
by (rule_tac SPEC_rule_conjI,
rule_tac order_trans,
rule_tac f_sup,
rule_tac expand_rslt_exist_eq,
rule_tac order_trans,
rule_tac f_sup,
rule_tac expand_name_propag) simp+
next
case 2
then show ?case
by (rule_tac SPEC_rule_param2[where P = "λ_. ?P"], rule_tac step) auto
next
case prems': (3 nm nds)
let ?x' = "(n⦇new := new n - {ψ},
name := fst (nm, nds),
new := new2 ψ ∪ new (n⦇new := new n - {ψ}⦈),
old := {ψ} ∪ old (n⦇new := new n - {ψ}⦈)⦈, nds)"
from prems' show ?case
proof (rule_tac step, goal_cases)
case prems'': 1
then have "expand_assm_incoming ?x'" by auto
moreover
from prems'' have nds_ident: "expand_name_ident (snd ?x')" by simp
moreover
have "(μ R⇩r η ∈ old (fst ?x')
⟶ ({μ, η}⊆old (fst ?x') ∪ new (fst ?x')
∨ (η∈old (fst ?x')∪new (fst ?x')
∧ μ R⇩r η ∈ next (fst ?x'))))"
using Q[THEN conjunct1] goal_assms by auto
moreover
from prems'' have "release_propag__rslt μ η (snd ?x')" by simp
moreover
from prems'' have name_nds_eq: "name ` nds = name ` ns ∪ name ` {nd∈nds. name nd ≥ name n}"
by auto
have "∀nd∈nds. (μ R⇩r η ∈ old nd ∧ name nd ∈ incoming (fst ?x'))
⟶ ({μ, η}⊆old nd
∨ (η∈old nd ∧ μ R⇩r η ∈old (fst ?x')∪new (fst ?x')))"
(is "∀nd∈nds. ?assm (fst ?x') nd ⟶ ?concl (fst ?x') nd")
proof
fix nd
assume "nd∈nds"
{ assume loc_assm: "name nd∈name ` ns"
then obtain n' where n': "n'∈ns" "name n' = name nd" by auto
with prems'' obtain nd' where "nd'∈nds"
and n'_nd'_eq: "expand_rslt_exist_eq__node n' nd'"
by auto
with n' have "nd = nd'" using nds_ident ‹nd∈nds› loc_assm
by auto
moreover from prems'' have "?assm n n' ⟶ ?concl n n'"
using ‹n'∈ns› by auto
ultimately have "?assm (fst ?x') nd ⟶ ?concl (fst ?x') nd"
using n'_nd'_eq by auto }
moreover
{ assume "name nd∉name ` ns"
with name_nds_eq ‹nd∈nds› have "name nd ≥ name n" by auto
with prems'' have "¬ (?assm (fst ?x') nd)" by auto }
ultimately show "?assm (fst ?x') nd ⟶ ?concl (fst ?x') nd" by auto
qed
ultimately show ?case by simp
qed
qed
qed
lemma release_propag_on_create_graph:
"create_graph φ
≤ SPEC (λnds. ∀n∈nds. ∀n'∈nds. μ R⇩r η∈old n ∧ name n∈incoming n'
⟶ ({μ, η}⊆old n ∨ η∈old n ∧ μ R⇩r η∈old n'))"
unfolding create_graph_def
apply (refine_vcg expand_release_propag)
by (auto simp add:expand_new_name_expand_init)
abbreviation
"until_propag__assm f g n_ns ≡
(f U⇩r g ∈ old (fst n_ns)
⟶ (g∈old (fst n_ns)∪new (fst n_ns)
∨ (f∈old (fst n_ns)∪new (fst n_ns) ∧ f U⇩r g ∈ next (fst n_ns))))
∧ (∀nd∈snd n_ns. f U⇩r g ∈ old nd ∧ name nd ∈ incoming (fst n_ns)
⟶ (g∈old nd ∨ (f∈old nd ∧ f U⇩r g ∈old (fst n_ns)∪new (fst n_ns))))"
abbreviation
"until_propag__rslt f g ns ≡
∀n∈ns. ∀nd∈ns. f U⇩r g ∈ old n ∧ name n ∈ incoming nd
⟶ (g ∈ old n ∨ (f∈old n ∧ f U⇩r g ∈ old nd))"
lemma expand_until_propag:
fixes n_ns :: "_ × 'a node set"
assumes "until_propag__assm μ η n_ns
∧ until_propag__rslt μ η (snd n_ns)
∧ expand_assm_incoming n_ns
∧ expand_name_ident (snd n_ns)" (is "?Q n_ns")
shows "expand n_ns ≤ SPEC (λr. until_propag__rslt μ η (snd r))"
(is "_ ≤ SPEC ?P")
using assms
proof (rule_tac expand_rec_rule[where Φ="?Q"], simp, intro refine_vcg, goal_cases)
case prems: (1 f x n ns)
then show ?case
proof (simp, rule_tac upd_incoming__ident, goal_cases)
case prems': 1
{ fix nd :: "'a node" and nd' :: "'a node"
let ?U_prop = "μ U⇩r η ∈ old nd ∧ name nd ∈ incoming nd'
⟶ η ∈ old nd ∨ μ ∈ old nd ∧ μ U⇩r η ∈ old nd'"
assume "nd∈ns" and nd'_elem: "nd'∈upd_incoming n ns"
{ assume "nd'∈ns"
with prems' have ?U_prop using ‹nd∈ns› by auto }
moreover
{ assume "nd'∉ns" and
U_in_nd: "μ U⇩r η ∈ old nd" and "name nd ∈incoming nd'"
with upd_incoming__elem[of nd' n ns] nd'_elem
obtain nd'' where "nd''∈ns"
and nd'_eq: "nd' = nd''⦇incoming := incoming n ∪ incoming nd''⦈"
and old_eq: "old nd'' = old n" by auto
{ assume "name nd ∈ incoming n"
with prems' U_in_nd ‹nd∈ns›
have "η ∈ old nd ∨ μ ∈ old nd ∧ μ U⇩r η ∈ old n" by auto
then have "η ∈ old nd ∨ μ ∈ old nd ∧ μ U⇩r η ∈ old nd'"
using nd'_eq old_eq by simp }
moreover
{ assume "name nd ∉ incoming n"
then have "name nd ∈ incoming nd''"
using ‹name nd ∈incoming nd'› nd'_eq by simp
then have "η ∈ old nd ∨ μ ∈ old nd ∧ μ U⇩r η ∈ old nd'"
unfolding nd'_eq
using prems' ‹nd∈ns› ‹nd''∈ns› U_in_nd by auto }
ultimately have "η ∈ old nd ∨ μ ∈ old nd ∧ μ U⇩r η ∈ old nd'" by fast }
ultimately have ?U_prop by auto }
then show ?case by auto
next
case 2
then show ?case by simp
qed
next
case prems: (2 f x n ns)
then have step: "⋀x. ?Q x ⟹ f x ≤ SPEC ?P" and f_sup: "⋀x. f x ≤ expand x"
by auto
from prems have Q: "?Q (n, ns)" by auto
from Q have name_le: "name n < expand_new_name (name n)" by auto
let ?x' = "(⦇name = expand_new_name (name n),
incoming = {name n}, new = next n,
old = {}, next = {}⦈, {n} ∪ ns)"
have Q'1: "expand_assm_incoming ?x'∧ expand_name_ident (snd ?x')"
using ‹new n = {}› Q[THEN conjunct2, THEN conjunct2] name_le by force
have Q'2: "until_propag__assm μ η ?x' ∧ until_propag__rslt μ η (snd ?x')"
using Q ‹new n = {}› by auto
show ?case
using ‹new n = {}› unfolding ‹x = (n, ns)›
proof (rule_tac SPEC_rule_weak[where
Q = "λ_ r. expand_name_ident (snd r)" and P = "λ_. ?P"], goal_cases)
case 1
then show ?case using Q'1
by (rule_tac order_trans,
rule_tac f_sup,
rule_tac expand_name_propag__name_ident) auto
next
case 2
then show ?case using Q'1 Q'2 by (rule_tac step) simp
next
case (3 nm nds)
then show ?case by simp
qed
next
case 3
then show ?case by auto
next
case prems: (4 f)
then have step: "⋀x. ?Q x ⟹ f x ≤ SPEC ?P" by simp_all
from prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
case prems: (5 f)
then have step: "⋀x. ?Q x ⟹ f x ≤ SPEC ?P" by simp_all
from prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
case 6
then show ?case by auto
next
case prems: (7 f)
then have step: "⋀x. ?Q x ⟹ f x ≤ SPEC ?P" by simp_all
from prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
case prems: (8 f x n ns ψ)
then have goal_assms: "ψ ∈ new n ∧ (∃ν μ. ψ = ν or⇩r μ ∨ ψ = ν U⇩r μ ∨ ψ = ν R⇩r μ)"
by (cases ψ) auto
from prems have Q: "?Q (n, ns)"
and step: "⋀x. ?Q x ⟹ f x ≤ SPEC ?P"
and f_sup: "⋀x. f x ≤ expand x" by auto
let ?x = "(n⦇new := new n - {ψ}, new := new1 ψ ∪ new (n⦇new := new n - {ψ}⦈),
old := {ψ} ∪ old (n⦇new := new n - {ψ}⦈),
next := next1 ψ ∪ next (n⦇new := new n - {ψ}⦈)
⦈, ns)"
let ?props = "λx r. expand_rslt_exist_eq x r
∧ expand_rslt_incoming r ∧ expand_rslt_name x r ∧ expand_name_ident (snd r)"
show ?case
using goal_assms Q unfolding case_prod_unfold ‹x = (n, ns)›
proof (rule_tac SPEC_rule_weak_nested2[where Q = "?props ?x"], goal_cases)
case 1
then show ?case
by (rule_tac SPEC_rule_conjI,
rule_tac order_trans,
rule_tac f_sup,
rule_tac expand_rslt_exist_eq,
rule_tac order_trans,
rule_tac f_sup,
rule_tac expand_name_propag) simp+
next
case 2
then show ?case
by (rule_tac SPEC_rule_param2[where P = "λ_. ?P"], rule_tac step) auto
next
case prems: (3 nm nds)
let ?x' = "(n⦇new := new n - {ψ},
name := fst (nm, nds),
new := new2 ψ ∪ new (n⦇new := new n - {ψ}⦈),
old := {ψ} ∪ old (n⦇new := new n - {ψ}⦈)⦈, nds)"
from prems show ?case
proof (rule_tac step, goal_cases)
case prems': 1
then have "expand_assm_incoming ?x'" by auto
moreover
from prems' have nds_ident: "expand_name_ident (snd ?x')"
by simp
moreover
have "(μ U⇩r η ∈ old (fst ?x')
⟶ (η∈old (fst ?x')∪new (fst ?x')
∨ (μ∈old (fst ?x')∪new (fst ?x')
∧ μ U⇩r η ∈ next (fst ?x'))))"
using Q[THEN conjunct1] goal_assms by auto
moreover
from prems' have "until_propag__rslt μ η (snd ?x')"
by simp
moreover
from prems' have name_nds_eq:
"name ` nds = name ` ns ∪ name ` {nd∈nds. name nd ≥ name n}"
by auto
have "∀nd∈nds. (μ U⇩r η ∈ old nd ∧ name nd ∈ incoming (fst ?x'))
⟶ (η∈old nd ∨ (μ∈old nd ∧ μ U⇩r η ∈old (fst ?x')∪new (fst ?x')))"
(is "∀nd∈nds. ?assm (fst ?x') nd ⟶ ?concl (fst ?x') nd")
proof
fix nd
assume "nd∈nds"
{ assume loc_assm: "name nd∈name ` ns"
then obtain n' where n': "n'∈ns" "name n' = name nd" by auto
moreover
from prems' n' obtain nd' where "nd'∈nds"
and n'_nd'_eq: "expand_rslt_exist_eq__node n' nd'"
by auto
ultimately have "nd = nd'"
using nds_ident ‹nd∈nds› loc_assm by auto
moreover from prems' have "?assm n n' ⟶ ?concl n n'"
using ‹n'∈ns› by auto
ultimately have "?assm (fst ?x') nd ⟶ ?concl (fst ?x') nd"
using n'_nd'_eq by auto }
moreover
{ assume "name nd∉name ` ns"
with name_nds_eq ‹nd∈nds› have "name nd ≥ name n" by auto
with prems' have "¬ (?assm (fst ?x') nd)" by auto }
ultimately show "?assm (fst ?x') nd ⟶ ?concl (fst ?x') nd" by auto
qed
ultimately show ?case by simp
qed
qed
qed
lemma until_propag_on_create_graph:
"create_graph φ ≤ SPEC (λnds. ∀n∈nds. ∀n'∈nds. μ U⇩r η∈old n ∧ name n∈incoming n'
⟶ (η∈old n ∨ μ∈old n ∧ μ U⇩r η∈old n'))"
unfolding create_graph_def
apply (refine_vcg expand_until_propag)
by (auto simp add:expand_new_name_expand_init)
definition all_subfrmls :: "'a node ⇒ 'a frml set"
where "all_subfrmls n ≡ ⋃(subfrmlsr ` (new n ∪ old n ∪ next n))"
lemma all_subfrmls__UnionD:
assumes "(⋃x∈A. subfrmlsr x) ⊆ B"
and "x∈A"
and "y∈subfrmlsr x"
shows "y∈B"
proof -
note subfrmlsr_id[of x]
also have "subfrmlsr x ⊆ (⋃x∈A. subfrmlsr x)"
using assms by auto
finally show ?thesis using assms by auto
qed
lemma expand_all_subfrmls_propag:
assumes "all_subfrmls (fst n_ns) ⊆ B ∧ (∀nd∈snd n_ns. all_subfrmls nd ⊆ B)" (is "?Q n_ns")
shows "expand n_ns ≤ SPEC (λr. ∀nd∈snd r. all_subfrmls nd ⊆ B)"
(is "_ ≤ SPEC ?P")
using assms
proof (rule_tac expand_rec_rule[where Φ="?Q"], simp, intro refine_vcg, goal_cases)
case 1
then show ?case
proof (simp, rule_tac upd_incoming__ident, goal_cases)
case 1
then show ?case by auto
next
case 2
then show ?case by (simp add: all_subfrmls_def)
qed
next
case 2
then show ?case by (auto simp add: all_subfrmls_def)
next
case 3
then show ?case by (auto simp add: all_subfrmls_def)
next
case prems: (4 f)
then have step: "⋀x. ?Q x ⟹ f x ≤ SPEC ?P" by simp_all
from prems show ?case by (rule_tac step) (auto simp add: all_subfrmls_def)
next
case prems: (5 f _ n ns ψ)
then have goal_assms: "ψ ∈ new n ∧ ψ = true⇩r" by simp
from prems have step: "⋀x. ?Q x ⟹ f x ≤ SPEC ?P" and Q: "?Q (n, ns)"
by simp_all
show ?case using Q goal_assms
by (rule_tac step) (auto dest: all_subfrmls__UnionD simp add: all_subfrmls_def)
next
case 6
then show ?case by auto
next
case prems: (7 f x n ns ψ)
then have goal_assms: "ψ ∈ new n ∧ (∃ν μ. ψ = ν and⇩r μ ∨ ψ = X⇩r ν)" by simp
from prems have step: "⋀x. ?Q x ⟹ f x ≤ SPEC ?P" and Q: "?Q (n, ns)"
by simp_all
show ?case
using Q goal_assms
by (rule_tac step) (auto dest: all_subfrmls__UnionD simp add: all_subfrmls_def)
next
case prems: (8 f x n ns ψ)
then have goal_assms: "ψ ∈ new n
∧ ¬ (∃q. ψ = prop⇩r(q) ∨ ψ = nprop⇩r(q))
∧ ψ ≠ true⇩r ∧ ψ ≠ false⇩r
∧ ¬ (∃ν μ. ψ = ν and⇩r μ ∨ ψ = X⇩r ν)
∧ (∃ν μ. ψ = ν or⇩r μ ∨ ψ = ν U⇩r μ ∨ ψ = ν R⇩r μ)"
by (cases ψ) auto
from prems have Q: "?Q (n, ns)" and step: "⋀x. ?Q x ⟹ f x ≤ SPEC ?P"
by simp_all
show ?case
using goal_assms Q unfolding case_prod_unfold ‹x = (n, ns)›
proof (rule_tac SPEC_rule_nested2, goal_cases)
case 1
then show ?case
by (rule_tac step) (auto dest: all_subfrmls__UnionD simp: all_subfrmls_def)
next
case 2
then show ?case
by (rule_tac step) (auto dest: all_subfrmls__UnionD simp: all_subfrmls_def)
qed
qed
lemma old_propag_on_create_graph: "create_graph φ ≤ SPEC (λnds. ∀n∈nds. old n ⊆ subfrmlsr φ)"
unfolding create_graph_def
by (intro refine_vcg,
rule_tac order_trans,
rule_tac expand_all_subfrmls_propag[where B = "subfrmlsr φ"])
(force simp add:all_subfrmls_def expand_new_name_expand_init)+
lemma L4_2__aux:
assumes run: "ipath gba.E σ"
and "μ U⇩r η ∈ old (σ 0)"
and "∀j. (∀i<j. {μ, μ U⇩r η} ⊆ old (σ i)) ⟶ η ∉ old (σ j)"
shows "∀i. {μ, μ U⇩r η} ⊆ old (σ i) ∧ η ∉ old (σ i)"
proof -
have "∀i<j. {μ, μ U⇩r η} ⊆ old (σ i)" (is "?sbthm j") for j
proof (induct j)
show "?sbthm 0" by auto
next
fix k
assume step: "?sbthm k"
then have σ_k_prop: "η ∉ old (σ k)
∧ σ k∈qs ∧ σ (Suc k)∈qs
∧ name (σ k) ∈ incoming (σ (Suc k))"
using assms run_propag_on_create_graph[OF run] by auto
with inres_SPEC[OF res until_propag_on_create_graph[where μ = μ and η = η]]
have "{μ, μ U⇩r η} ⊆ old (σ k)" (is "?subsetthm")
proof (cases k)
assume "k = 0"
with assms σ_k_prop
inres_SPEC[OF res until_propag_on_create_graph[where μ = μ and η = η]]
show ?subsetthm by auto
next
fix l
assume "k = Suc l"
then have "{μ, μ U⇩r η}⊆old (σ l) ∧ η∉old (σ l)
∧ σ l∈qs ∧ σ k∈qs
∧ name (σ l)∈incoming (σ k)"
using step assms run_propag_on_create_graph[OF run] by auto
with inres_SPEC[OF res until_propag_on_create_graph[where μ = μ and η = η]]
have "μ U⇩r η∈old (σ k)" by auto
with σ_k_prop
inres_SPEC[OF res until_propag_on_create_graph[where μ = μ and η = η]]
show ?subsetthm by auto
qed
with step show "?sbthm (Suc k)" by (metis less_SucE)
qed
with assms show ?thesis by auto
qed
lemma L4_2a:
assumes "ipath gba.E σ"
and "μ U⇩r η ∈ old (σ 0)"
shows "(∀i. {μ, μ U⇩r η} ⊆ old (σ i) ∧ η ∉ old (σ i))
∨ (∃j. (∀i<j. {μ, μ U⇩r η} ⊆ old (σ i)) ∧ η ∈ old (σ j))"
(is "?A ∨ ?B")
proof (rule disjCI)
assume "¬ ?B"
then show ?A
using assms by (rule_tac L4_2__aux) blast+
qed
lemma L4_2b:
assumes run: "ipath gba.E σ"
and "μ U⇩r η ∈ old (σ 0)"
and ACC: "gba.is_acc σ"
shows "∃j. (∀i<j. {μ, μ U⇩r η} ⊆ old (σ i)) ∧ η ∈ old (σ j)"
proof (rule ccontr)
assume "¬ ?thesis"
then have contr: "∀i. {μ, μ U⇩r η}⊆old(σ i) ∧ η∉old(σ i)"
using assms L4_2a[of σ μ η] by blast
define S where "S = {q ∈ qs. μ U⇩r η ∈ old q ⟶ η ∈ old q}"
from assms inres_SPEC[OF res old_propag_on_create_graph] create_gba_from_nodes__ipath
have "μ U⇩r η ∈ subfrmlsr φ"
by (metis assms(2) subsetD)
then have "S∈gbg_F(create_gba_from_nodes φ qs)"
unfolding S_def create_gba_from_nodes_def by auto
with ACC have 1: "∃⇩∞i. σ i ∈ S"
unfolding gba.is_acc_def by blast
from INFM_EX[OF 1] obtain k where "σ k ∈ qs" and "μ U⇩r η ∈ old (σ k) ⟶ η ∈ old (σ k)"
unfolding S_def by auto
moreover have "{μ, μ U⇩r η}⊆old(σ k) ∧ η∉old(σ k)"
using contr by auto
ultimately show False by auto
qed
lemma L4_2c:
assumes run: "ipath gba.E σ"
and "μ R⇩r η ∈ old (σ 0)"
shows "∀i. η ∈ old (σ i) ∨ (∃j<i. μ ∈ old (σ j))"
proof -
have "{η, μ R⇩r η} ⊆ old (σ i) ∨ (∃j<i. μ ∈ old (σ j))" (is "?thm i") for i
proof (induct i)
case 0
have "σ 0∈qs ∧ σ 1∈qs ∧ name (σ 0) ∈ incoming (σ 1)"
using create_gba_from_nodes__ipath assms by auto
then show ?case
using assms inres_SPEC[OF res release_propag_on_create_graph, of μ η]
by auto
next
case (Suc k)
note ‹?thm k›
moreover
{ assume "{η, μ R⇩r η} ⊆ old (σ k)"
moreover
have "σ k∈qs ∧ σ (Suc k)∈qs ∧ name (σ k) ∈ incoming (σ (Suc k))"
using create_gba_from_nodes__ipath assms by auto
ultimately have "μ ∈ old (σ k) ∨ μ R⇩r η ∈ old (σ (Suc k))"
using assms inres_SPEC[OF res release_propag_on_create_graph, of μ η]
by auto
moreover
{ assume "μ ∈ old (σ k)"
then have ?case by blast }
moreover
{ assume "μ R⇩r η ∈ old (σ (Suc k))"
moreover
have "σ (Suc k)∈qs ∧ σ (Suc (Suc k))∈qs
∧ name (σ (Suc k)) ∈ incoming (σ (Suc (Suc k)))"
using create_gba_from_nodes__ipath assms by auto
ultimately have ?case
using assms
inres_SPEC[OF res release_propag_on_create_graph, of μ η]
by auto }
ultimately have ?case by fast }
moreover
{ assume "∃j<k. μ ∈ old (σ j)"
then have ?case by auto }
ultimately show ?case by auto
qed
then show ?thesis by auto
qed
lemma L4_8':
assumes "ipath gba.E σ" (is "?inf_run σ")
and "gba.is_acc σ" (is "?gbarel_accept σ")
and "∀i. gba.L (σ i) (ξ i)" (is "?lgbarel_accept ξ σ")
and "ψ ∈ old (σ 0)"
shows "ξ ⊨⇩r ψ"
using assms
proof (induct ψ arbitrary: σ ξ)
case True_ltlr
show ?case by auto
next
case False_ltlr
then show ?case
using inres_SPEC[OF res false_propag_on_create_graph]
create_gba_from_nodes__ipath
by (metis)
next
case (Prop_ltlr p)
then show ?case
unfolding create_gba_from_nodes_def by auto
next
case (Nprop_ltlr p)
then show ?case
unfolding create_gba_from_nodes_def by auto
next
case (And_ltlr μ η)
then show ?case
using inres_SPEC[OF res and_propag_on_create_graph, of μ η]
create_gba_from_nodes__ipath
by (metis insert_subset semantics_ltlr.simps(5))
next
case (Or_ltlr μ η)
then have "μ ∈ old (σ 0) ∨ η ∈ old (σ 0)"
using inres_SPEC[OF res or_propag_on_create_graph, of μ η]
create_gba_from_nodes__ipath
by (metis (full_types) Int_empty_left Int_insert_left_if0)
moreover have "ξ ⊨⇩r μ" if "μ ∈ old (σ 0)"
using Or_ltlr that by auto
moreover have "ξ ⊨⇩r η" if "η ∈ old (σ 0)"
using Or_ltlr that by auto
ultimately show ?case by auto
next
case (Next_ltlr μ)
with create_gba_from_nodes__ipath[of σ]
have "σ 0 ∈ qs ∧ σ 1 ∈ qs ∧ name (σ 0) ∈ incoming (σ 1)"
by auto
with inres_SPEC[OF res next_propag_on_create_graph, of μ] have "μ∈old (suffix 1 σ 0)"
using Next_ltlr by auto
moreover
have "?inf_run (suffix 1 σ)"
and "?gbarel_accept (suffix 1 σ)"
and "?lgbarel_accept (suffix 1 ξ) (suffix 1 σ )"
using Next_ltlr create_gba_from_nodes__ipath
apply -
apply (metis ipath_suffix)
apply (auto simp del: suffix_nth) []
apply auto
done
ultimately show ?case using Next_ltlr by simp
next
case (Until_ltlr μ η)
then have "∃j. (∀i<j. {μ, μ U⇩r η} ⊆ old (σ i)) ∧ η ∈ old (σ j)"
using L4_2b by auto
then obtain j where σ_pre: "∀i<j. {μ, μ U⇩r η} ⊆ old (σ i)" and "η ∈ old (suffix j σ 0)"
by auto
moreover
have "?inf_run (suffix j σ)"
and "?gbarel_accept (suffix j σ)"
and "?lgbarel_accept (suffix j ξ) (suffix j σ)"
unfolding limit_suffix
using Until_ltlr create_gba_from_nodes__ipath
apply -
apply (metis ipath_suffix)
apply (auto simp del: suffix_nth) []
apply auto
done
ultimately have "suffix j ξ ⊨⇩r η"
using Until_ltlr by simp
moreover {
fix i
assume "i < j"
have "?inf_run (suffix i σ)"
and "?gbarel_accept (suffix i σ)"
and "?lgbarel_accept (suffix i ξ) (suffix i σ )"
unfolding limit_suffix
using Until_ltlr create_gba_from_nodes__ipath
apply -
apply (metis ipath_suffix)
apply (auto simp del: suffix_nth) []
apply auto
done
moreover have "μ∈old (suffix i σ 0)"
using σ_pre ‹i<j› by auto
ultimately have "suffix i ξ ⊨⇩r μ" using Until_ltlr by simp
}
ultimately show ?case by auto
next
case (Release_ltlr μ η)
{ fix i
assume "η ∈ old (σ i) ∨ (∃j<i. μ ∈ old (σ j))"
moreover
{
assume *: "η ∈ old (σ i)"
have "?inf_run (suffix i σ)"
and "?gbarel_accept (suffix i σ)"
and "?lgbarel_accept (suffix i ξ) (suffix i σ )"
unfolding limit_suffix
using Release_ltlr create_gba_from_nodes__ipath
apply -
apply (metis ipath_suffix)
apply (auto simp del: suffix_nth) []
apply auto
done
with * have "suffix i ξ ⊨⇩r η"
using Release_ltlr by auto
}
moreover
{
assume "∃j<i. μ ∈ old (σ j)"
then obtain j where "j<i" and "μ ∈ old (σ j)" by auto
moreover
have "?inf_run (suffix j σ)"
and "?gbarel_accept (suffix j σ)"
and "?lgbarel_accept (suffix j ξ) (suffix j σ )" unfolding limit_suffix
using Release_ltlr create_gba_from_nodes__ipath
apply -
apply (metis ipath_suffix)
apply (auto simp del: suffix_nth) []
apply auto
done
ultimately have "suffix j ξ ⊨⇩r μ"
using Release_ltlr by auto
then have "∃j<i. suffix j ξ ⊨⇩r μ"
using ‹j<i› by auto
}
ultimately have "suffix i ξ ⊨⇩r η ∨ (∃j<i. suffix j ξ ⊨⇩r μ)" by auto
}
then show ?case using Release_ltlr L4_2c by auto
qed
lemma L4_8:
assumes "gba.is_acc_run σ"
and "∀i. gba.L (σ i) (ξ i)"
and "ψ ∈ old (σ 0)"
shows "ξ ⊨⇩r ψ"
using assms
unfolding gba.is_acc_run_def gba.is_run_def
using L4_8' by blast
lemma expand_expand_init_propag:
assumes "(∀nm∈incoming n'. nm < name n')
∧ name n' ≤ name (fst n_ns)
∧ (incoming n' ∩ incoming (fst n_ns) ≠ {}
⟶ new n' ⊆ old (fst n_ns) ∪ new (fst n_ns))
" (is "?Q n_ns")
and "∀nd∈snd n_ns. ∀nm∈incoming n'. nm∈incoming nd ⟶ new n' ⊆ old nd"
(is "?P (snd n_ns)")
shows "expand n_ns ≤ SPEC (λr. name n'≤fst r ∧ ?P (snd r))"
using assms
proof (rule_tac expand_rec_rule[where Φ="λx. ?Q x ∧ ?P (snd x)"],
simp,
intro refine_vcg, goal_cases)
case prems: (1 f x n ns)
then have goal_assms: "new n = {} ∧ ?Q (n, ns) ∧ ?P ns" by simp
{ fix nd nm
assume "nd∈upd_incoming n ns" and "nm∈incoming n'" and "nm∈incoming nd"
{ assume "nd∈ns"
with goal_assms ‹nm∈incoming n'› ‹nm∈incoming nd› have "new n' ⊆ old nd"
by auto }
moreover
{ assume "nd∉ns"
with upd_incoming__elem[OF ‹nd∈upd_incoming n ns›]
obtain nd' where "nd'∈ns"
and nd_eq: "nd = nd'⦇incoming := incoming n ∪ incoming nd'⦈"
and old_next_eq: "old nd' = old n ∧ next nd' = next n" by auto
{ assume "nm∈incoming nd'"
with goal_assms ‹nm∈incoming n'› ‹nd'∈ns› have "new n' ⊆ old nd"
unfolding nd_eq by auto }
moreover
{ assume "nm∈incoming n"
with nd_eq old_next_eq goal_assms ‹nm∈incoming n'›
have "new n' ⊆ old nd"
by auto }
ultimately have "new n' ⊆ old nd" using ‹nm∈incoming nd› nd_eq by auto }
ultimately have "new n' ⊆ old nd" by fast }
with prems show ?case by auto
next
case prems: (2 f x n ns)
then have goal_assms: "new n = {} ∧ ?Q (n, ns) ∧ ?P ns" and step: "⋀x. ?Q x ∧ ?P (snd x)
⟹ f x ≤ SPEC (λr. name n' ≤ fst r ∧ ?P (snd r))"
by simp_all
then show ?case
proof (rule_tac step, goal_cases)
case prems': 1
have expand_new_name_less: "name n < expand_new_name (name n)"
by auto
moreover have "name n ∉ incoming n'"
using goal_assms by auto
ultimately show ?case using prems' by auto
qed
next
case 3 then show ?case by auto
next
case prems: (4 f x n ns)
then have step: "⋀x. ?Q x ∧ ?P (snd x) ⟹ f x ≤ SPEC (λr. name n' ≤ fst r ∧ ?P (snd r))"
by simp
from prems show ?case by (rule_tac step) auto
next
case prems: (5 f x n ns)
then have step: "⋀x. ?Q x ∧ ?P (snd x) ⟹ f x ≤ SPEC (λr. name n' ≤ fst r ∧ ?P (snd r))"
by simp
from prems show ?case by (rule_tac step) auto
next
case 6 then show ?case by auto
next
case prems: (7 f x n ns)
then have step: "⋀x. ?Q x ∧ ?P (snd x) ⟹ f x ≤ SPEC (λr. name n' ≤ fst r ∧ ?P (snd r))"
by simp
from prems show ?case by (rule_tac step) auto
next
case prems: (8 f x n ns ψ)
then have goal_assms: "ψ ∈ new n
∧ ¬ (∃q. ψ = prop⇩r(q) ∨ ψ = nprop⇩r(q))
∧ ψ ≠ true⇩r ∧ ψ ≠ false⇩r
∧ ¬ (∃ν μ. ψ = ν and⇩r μ ∨ ψ = X⇩r ν)
∧ (∃ν μ. ψ = ν or⇩r μ ∨ ψ = ν U⇩r μ ∨ ψ = ν R⇩r μ)"
by (cases ψ) auto
from prems have QP: "?Q (n, ns) ∧ ?P ns" and
step: "⋀x. ?Q x ∧ ?P (snd x) ⟹ f x ≤ SPEC (λr. name n' ≤ fst r ∧ ?P (snd r))"
by simp_all
show ?case
using goal_assms QP unfolding case_prod_unfold ‹x = (n, ns)›
proof (rule_tac SPEC_rule_nested2, goal_cases)
case 1
then show ?case by (rule_tac step) auto
next
case 2
then show ?case by (rule_tac step) auto
qed
qed
lemma expand_init_propag_on_create_graph:
"create_graph φ ≤ SPEC(λnds. ∀nd∈nds. expand_init∈incoming nd ⟶ φ ∈ old nd)"
unfolding create_graph_def
by (intro refine_vcg, rule_tac order_trans,
rule_tac expand_expand_init_propag[where
n' = "⦇ name = expand_new_name expand_init,
incoming = {expand_init},
new = {φ},
old = {},
next = {} ⦈"]) (auto simp add:expand_new_name_expand_init)
lemma L4_6:
assumes "q∈gba.V0"
shows "φ∈old q"
using assms inres_SPEC[OF res expand_init_propag_on_create_graph]
unfolding create_gba_from_nodes_def by auto
lemma L4_9:
assumes acc: "gba.accept ξ"
shows "ξ ⊨⇩r φ"
proof -
from acc obtain σ where accept: "gba.is_acc_run σ ∧ (∀i. gba.L (σ i) (ξ i))"
unfolding gba.accept_def by auto
then have "σ 0∈gba.V0"
unfolding gba.is_acc_run_def gba.is_run_def by simp
with L4_6 have "φ∈old (σ 0)" by auto
with L4_8 accept show ?thesis by auto
qed
lemma L4_10:
assumes "ξ ⊨⇩r φ"
shows "gba.accept ξ"
proof -
define σ where "σ = auto_run ξ qs"
let ?G = "create_graph φ"
have σ_prop_0: "(σ 0)∈qs ∧ expand_init∈incoming(σ 0) ∧ auto_run_j 0 ξ (σ 0)"
(is "?sbthm")
using inres_SPEC[OF res L4_7[OF ‹ξ ⊨⇩r φ›]]
unfolding σ_def auto_run.simps by (rule_tac someI_ex, simp) blast
have σ_valid: "∀j. σ j ∈ qs ∧ auto_run_j j ξ (σ j)" (is "∀j. ?σ_valid j")
proof
fix j
show "?σ_valid j"
proof(induct j)
from σ_prop_0 show "?σ_valid 0" by fast
next
fix k
assume goal_assms: "σ k ∈ qs ∧ auto_run_j k ξ (σ k)"
with inres_SPEC[OF res L4_5, of "suffix k ξ"]
have sbthm: "∃q'. q'∈qs ∧ name (σ k)∈incoming q' ∧ auto_run_j (Suc k) ξ q'"
(is "∃q'. ?sbthm q'")
by auto
have "?sbthm (σ (Suc k))" using someI_ex[OF sbthm]
unfolding σ_def auto_run.simps by blast
then show "?σ_valid (Suc k)" by fast
qed
qed
have σ_prop_Suc: "⋀k. σ k∈ qs ∧ σ (Suc k)∈qs
∧ name (σ k)∈incoming (σ (Suc k))
∧ auto_run_j (Suc k) ξ (σ (Suc k))"
proof -
fix k
from σ_valid have "σ k ∈ qs" and "auto_run_j k ξ (σ k)" by blast+
with inres_SPEC[OF res L4_5, of "suffix k ξ"]
have sbthm: "∃q'. q'∈qs ∧ name (σ k)∈incoming q'
∧ auto_run_j (Suc k) ξ q'" (is "∃q'. ?sbthm q'")
by auto
show "σ k∈ qs ∧ ?sbthm (σ (Suc k))" using ‹σ k∈qs› someI_ex[OF sbthm]
unfolding σ_def auto_run.simps by blast
qed
have σ_vnaccpt:
"∀k μ η. μ U⇩r η ∈ old (σ k) ⟶ ¬ (∀i. {μ, μ U⇩r η} ⊆ old (σ (k+i)) ∧ η ∉ old (σ (k+i)))"
proof clarify
fix k μ η
assume U_in: "μ U⇩r η ∈ old (σ k)"
and cntr_prm: "∀i. {μ, μ U⇩r η} ⊆ old (σ (k+i)) ∧ η ∉ old (σ (k+i))"
have "suffix k ξ ⊨⇩r μ U⇩r η"
using U_in σ_valid by force
then obtain i where "suffix (k+i) ξ ⊨⇩r η" and "∀j<i. suffix (k+j) ξ ⊨⇩r μ"
by auto
moreover have "μ U⇩r η ∈ old (σ (k+i)) ∧ η ∉ old (σ (k+i))"
using cntr_prm by auto
ultimately show False
using σ_valid by force
qed
have σ_exec: "gba.is_run σ"
using σ_prop_0 σ_prop_Suc σ_valid
unfolding gba.is_run_def ipath_def
unfolding create_gba_from_nodes_def
by auto
moreover
have σ_vaccpt:
"∀k μ η. μ U⇩r η ∈ old (σ k) ⟶
(∃j. (∀i<j. {μ, μ U⇩r η} ⊆ old (σ (k+i))) ∧ η ∈ old (σ (k+j)))"
proof(clarify)
fix k μ η
assume U_in: "μ U⇩r η ∈ old (σ k)"
then have "¬ (∀i. {μ, μ U⇩r η} ⊆ old (suffix k σ i) ∧ η ∉ old (suffix k σ i))"
using σ_vnaccpt[THEN allE, of k] by auto
moreover have "suffix k σ 0 ∈ qs" using σ_valid by auto
ultimately show "∃j. (∀i<j. {μ, μ U⇩r η} ⊆ old (σ (k+i))) ∧ η ∈ old (σ (k+j))"
apply -
apply (rule make_pos_rule'[OF L4_2a])
apply (fold suffix_def)
apply (rule ipath_suffix)
using σ_exec[unfolded gba.is_run_def]
apply simp
using U_in apply simp
apply simp
done
qed
have "gba.is_acc σ"
unfolding gba.is_acc_def
proof
fix S
assume "S∈gba.F"
then obtain μ η where S_eq: "S = {q ∈ qs. μ U⇩r η ∈ old q ⟶ η ∈ old q}"
and "μ U⇩r η ∈ subfrmlsr φ"
by (auto simp add: create_gba_from_nodes_def)
have range_subset: "range σ ⊆ qs"
proof
fix q
assume "q∈range σ"
with full_SetCompr_eq[of σ] obtain k where "q = σ k" by auto
then show "q ∈ qs" using σ_valid by auto
qed
with limit_nonempty[of σ]
limit_in_range[of σ]
finite_subset[OF range_subset]
inres_SPEC[OF res create_graph_finite]
obtain q where q_in_limit: "q ∈ limit σ" and q_is_node: "q∈qs"
by auto
show "∃⇩∞i. σ i ∈ S"
proof (cases "μ U⇩r η ∈ old q")
case False
with S_eq q_in_limit q_is_node
show ?thesis
by (auto simp: limit_iff_frequent intro: INFM_mono)
next
case True
obtain k where q_eq: "q = σ k" using q_in_limit
unfolding limit_iff_frequent by (metis (lifting, full_types) INFM_nat_le)
have "∃⇩∞ k. η ∈ old (σ k)"
unfolding INFM_nat
proof (rule ccontr)
assume "¬ (∀m. ∃n>m. η ∈ old (σ n))"
then obtain m where "∀n>m. η ∉ old (σ n)" by auto
moreover
from q_eq q_in_limit limit_iff_frequent[of q σ] INFM_nat[of "λn. σ n = q"]
obtain n where "m<n" and σn_eq: "σ n = σ k" by auto
moreover
obtain j where "η ∈ old (σ (n+j))"
using σ_vaccpt ‹μ U⇩r η ∈ old q› unfolding q_eq by (fold σn_eq) force
ultimately show False by auto
qed
then have "∃⇩∞ k. σ k ∈ qs ∧ η ∈ old (σ k)"
using σ_valid by (auto intro: INF_mono)
then show "∃⇩∞ k. σ k ∈ S"
unfolding S_eq by (rule INFM_mono) simp
qed
qed
moreover have "gba.L (σ i) (ξ i)" for i
proof -
from σ_valid have [simp]: "σ i ∈ qs" by auto
have "∀ψ∈old (σ i). suffix i ξ ⊨⇩r ψ"
using σ_valid by auto
then show ?thesis
unfolding create_gba_from_nodes_def by auto
qed
ultimately show ?thesis
unfolding gba.accept_def gba.is_acc_run_def by blast
qed
end
end
lemma create_graph__name_ident: "create_graph φ ≤ SPEC (λnds. ∀q∈nds. ∃!q'∈nds. name q = name q')"
unfolding create_graph_def
apply (refine_vcg expand_name_propag__name_ident)
by (auto simp add:expand_new_name_expand_init)
corollary create_graph__name_inj: "create_graph φ ≤ SPEC (λnds. inj_on name nds)"
by (rule order_trans[OF create_graph__name_ident]) (auto intro: inj_onI)
definition
"create_gba φ
≡ do { nds ← create_graph⇩T φ;
RETURN (create_gba_from_nodes φ nds) }"
lemma create_graph_precond: "create_graph φ
≤ SPEC (create_gba_from_nodes_precond φ)"
apply (clarsimp simp: pw_le_iff create_graph_nofail)
apply unfold_locales
apply simp
done
lemma create_gba__invar: "create_gba φ ≤ SPEC gba"
unfolding create_gba_def create_graph_eq_create_graph⇩T[symmetric]
apply (refine_rcg refine_vcg order_trans[OF create_graph_precond])
by (rule create_gba_from_nodes_precond.create_gba_from_nodes__invar)
lemma create_gba_acc:
shows "create_gba φ ≤ SPEC(λ𝒜. ∀ξ. gba.accept 𝒜 ξ ⟷ ξ ⊨⇩r φ)"
unfolding create_gba_def create_graph_eq_create_graph⇩T[symmetric]
apply (refine_rcg refine_vcg order_trans[OF create_graph_precond])
using create_gba_from_nodes_precond.L4_9
using create_gba_from_nodes_precond.L4_10
by blast
lemma create_gba__name_inj:
shows "create_gba φ ≤ SPEC(λ𝒜. (inj_on name (g_V 𝒜)))"
unfolding create_gba_def create_graph_eq_create_graph⇩T[symmetric]
apply (refine_rcg refine_vcg order_trans[OF create_graph__name_inj])
apply (auto simp: create_gba_from_nodes_def)
done
lemma create_gba__fin:
shows "create_gba φ ≤ SPEC(λ𝒜. (finite (g_V 𝒜)))"
unfolding create_gba_def create_graph_eq_create_graph⇩T[symmetric]
apply (refine_rcg refine_vcg order_trans[OF create_graph_finite])
apply (auto simp: create_gba_from_nodes_def)
done
lemma create_graph_old_finite:
"create_graph φ ≤ SPEC (λnds. ∀nd∈nds. finite (old nd))"
proof -
show ?thesis
unfolding create_graph_def create_graph_eq_create_graph⇩T[symmetric]
unfolding expand_def
apply (intro refine_vcg)
apply (rule_tac order_trans)
apply (rule_tac REC_le_RECT)
apply (fold expand⇩T_def)
apply (rule_tac order_trans[OF expand_term_prop])
apply auto[1]
apply (rule_tac SPEC_rule)
apply auto
by (metis infinite_super subfrmlsr_finite)
qed
lemma create_gba__old_fin:
shows "create_gba φ ≤ SPEC(λ𝒜. ∀nd∈g_V 𝒜. finite (old nd))"
unfolding create_gba_def create_graph_eq_create_graph⇩T[symmetric]
apply (refine_rcg refine_vcg order_trans[OF create_graph_old_finite])
apply (simp add: create_gba_from_nodes_def)
done
lemma create_gba__incoming_exists:
shows "create_gba φ
≤ SPEC(λ𝒜. ∀nd∈g_V 𝒜. incoming nd ⊆ insert expand_init (name ` (g_V 𝒜)))"
unfolding create_gba_def create_graph_eq_create_graph⇩T[symmetric]
apply (refine_rcg refine_vcg order_trans[OF create_graph__incoming_name_exist])
apply (auto simp add: create_gba_from_nodes_def)
done
lemma create_gba__no_init:
shows "create_gba φ ≤ SPEC(λ𝒜. expand_init ∉ name ` (g_V 𝒜))"
unfolding create_gba_def create_graph_eq_create_graph⇩T[symmetric]
apply (refine_rcg refine_vcg order_trans[OF create_graph__incoming_name_exist])
apply (auto simp add: create_gba_from_nodes_def)
done
definition "nds_invars nds ≡
inj_on name nds
∧ finite nds
∧ expand_init ∉ name`nds
∧ (∀nd∈nds.
finite (old nd)
∧ incoming nd ⊆ insert expand_init (name ` nds))"
lemma create_gba_nds_invars: "create_gba φ ≤ SPEC (λ𝒜. nds_invars (g_V 𝒜))"
using create_gba__name_inj[of φ] create_gba__fin[of φ]
create_gba__old_fin[of φ] create_gba__incoming_exists[of φ]
create_gba__no_init[of φ]
unfolding nds_invars_def
by (simp add: pw_le_iff)
theorem T4_1:
"create_gba φ ≤ SPEC(
λ𝒜. gba 𝒜
∧ finite (g_V 𝒜)
∧ (∀ξ. gba.accept 𝒜 ξ ⟷ ξ ⊨⇩r φ)
∧ (nds_invars (g_V 𝒜)))"
using create_gba__invar create_gba__fin create_gba_acc create_gba_nds_invars
apply (simp add: pw_le_iff)
apply blast
done
definition "create_name_gba φ ≡ do {
G ← create_gba φ;
ASSERT (nds_invars (g_V G));
RETURN (gba_rename name G)
}"
theorem create_name_gba_correct:
"create_name_gba φ ≤ SPEC(λ𝒜. gba 𝒜 ∧ finite (g_V 𝒜) ∧ (∀ξ. gba.accept 𝒜 ξ ⟷ ξ ⊨⇩r φ))"
unfolding create_name_gba_def
apply (refine_rcg refine_vcg order_trans[OF T4_1])
apply (simp_all add: nds_invars_def gba_rename_correct)
done
definition create_name_igba :: "'a::linorder ltlr ⇒ _" where
"create_name_igba φ ≡ do {
A ← create_name_gba φ;
A' ← gba_to_idx A;
stat_set_data_nres (card (g_V A)) (card (g_V0 A')) (igbg_num_acc A');
RETURN A'
}"
lemma create_name_igba_correct: "create_name_igba φ ≤ SPEC (λG.
igba G ∧ finite (g_V G) ∧ (∀ξ. igba.accept G ξ ⟷ ξ ⊨⇩r φ))"
unfolding create_name_igba_def
apply (refine_rcg
order_trans[OF create_name_gba_correct]
order_trans[OF gba.gba_to_idx_ext_correct]
refine_vcg)
apply clarsimp_all
proof -
fix G :: "(nat, 'a set) gba_rec"
fix A :: "nat set"
assume 1: "gba G"
assume 2: "finite (g_V G)" "A ∈ gbg_F G"
interpret gba G using 1 .
show "finite A" using finite_V_Fe 2 .
qed
context
notes [refine_vcg] = order_trans[OF create_name_gba_correct]
begin
lemma "create_name_igba φ ≤ SPEC (λG. igba G ∧ (∀ξ. igba.accept G ξ ⟷ ξ ⊨⇩r φ))"
unfolding create_name_igba_def
proof (refine_rcg refine_vcg, clarsimp_all)
fix G :: "(nat, 'a set) gba_rec"
assume "gba G"
then interpret gba G .
note [refine_vcg] = order_trans[OF gba_to_idx_ext_correct]
assume "∀ξ. gba.accept G ξ = ξ ⊨⇩r φ" "finite (g_V G)"
then show "gba_to_idx G ≤ SPEC (λG'. igba G' ∧ (∀ξ. igba.accept G' ξ = ξ ⊨⇩r φ))"
by (refine_rcg refine_vcg) (auto intro: finite_V_Fe)
qed
end
end