theory NetCheck
imports
Fofu_Impl_Base
Network
"Graph_Impl"
"cava/DFS_Framework/Examples/Reachable_Nodes"
begin
declare [[coercion_delete int]]
declare [[coercion_delete "real::nat=>real"]]
type_synonym edge_list = "(node × node × capacity_impl) list"
definition ln_invar :: "edge_list => bool" where
"ln_invar el ≡
distinct (map (λ(u, v, _). (u,v)) el)
∧ (∀(u,v,c)∈set el. c>0)
"
definition ln_α :: "edge_list => capacity_impl graph" where
"ln_α el ≡ λ(u,v).
if ∃c. (u, v, c) ∈ set el ∧ c ≠ 0 then
SOME c. (u, v, c) ∈ set el ∧ c ≠ 0
else 0"
definition "ln_rel ≡ br ln_α ln_invar"
lemma ln_equivalence: "(el, c') ∈ ln_rel <-> ln_invar el ∧ c' = ln_α el"
unfolding ln_rel_def br_def by auto
definition ln_N :: "(node×node×_) list => nat" where
"ln_N el ≡ Max ((fst`set el) ∪ ((fst o snd)`set el)) + 1"
lemma ln_α_imp_in_set: "[|ln_α el (u,v)≠(0)|] ==> (u,v,ln_α el (u,v))∈set el"
apply (auto simp: ln_α_def split: split_if_asm)
apply (metis (mono_tags, lifting) someI_ex)
done
lemma ln_N_correct: "Graph.V (ln_α el) ⊆ {0..<ln_N el}"
apply (clarsimp simp: Graph.V_def Graph.E_def)
apply (safe dest!: ln_α_imp_in_set)
apply (fastforce simp: ln_N_def less_Suc_eq_le intro: Max_ge)
apply (force simp: ln_N_def less_Suc_eq_le intro: Max_ge)
done
record pre_network =
pn_c :: "capacity_impl graph"
pn_V :: "nat set"
pn_succ :: "nat => nat list"
pn_pred :: "nat => nat list"
pn_adjmap :: "nat => nat list"
pn_s_node :: bool
pn_t_node :: bool
fun read :: "edge_list => nat => nat =>
pre_network option" where
"read [] _ _ = Some (|
pn_c = (λ _. 0),
pn_V = {},
pn_succ = (λ _. []),
pn_pred = (λ _. []),
pn_adjmap = (λ _. []),
pn_s_node = False,
pn_t_node = False
|)),"
| "read ((u, v, c) # es) s t = ((case (read es s t) of
Some x =>
(if (pn_c x) (u, v) = 0 ∧ (pn_c x) (v, u) = 0 ∧ c > 0 then
(if u = v ∨ v = s ∨ u = t then
None
else
Some (x(|
pn_c := (pn_c x) ((u, v) := c),
pn_V := insert u (insert v (pn_V x)),
pn_succ := (pn_succ x) (u := v # ((pn_succ x) u)),
pn_pred := (pn_pred x) (v := u # ((pn_pred x) v)),
pn_adjmap := ((pn_adjmap x) (u := v # (pn_adjmap x) u)) (v := u # (pn_adjmap x) v),
pn_s_node := pn_s_node x ∨ u = s,
pn_t_node := pn_t_node x ∨ v = t
|)),))
else
None)
| None => None))"
lemma read_correct1: "read es s t = Some (|pn_c = c, pn_V = V, pn_succ = succ,
pn_pred = pred , pn_adjmap = adjmap, pn_s_node = s_n, pn_t_node = t_n|)), ==>
(es, c) ∈ ln_rel ∧ Graph.V c = V ∧ finite V ∧
(s_n --> s ∈ V) ∧ (t_n --> t ∈ V) ∧ (¬s_n --> s ∉ V) ∧ (¬t_n --> t ∉ V) ∧
(∀u v. c (u,v) ≥ 0) ∧
(∀u. c(u, u) = 0) ∧ (∀u. c (u, s) = 0) ∧ (∀u. c (t, u) = 0) ∧
(∀u v. c (u, v) ≠ 0 --> c (v, u) = 0) ∧
(∀u. set (succ u) = Graph.E c``{u} ∧ distinct (succ u)) ∧
(∀u. set (pred u) = (Graph.E c)¯``{u} ∧ distinct (pred u)) ∧
(∀u. set (adjmap u) = Graph.E c``{u} ∪ (Graph.E c)¯``{u} ∧ distinct (adjmap u))"
proof (induction es arbitrary: c V succ pred adjmap s_n t_n)
case Nil
thus ?case unfolding Graph.V_def Graph.E_def ln_rel_def br_def ln_α_def ln_invar_def by auto
next
case (Cons e es)
obtain u1 v1 c1 where obt1: "e = (u1, v1, c1)" by (meson prod_cases3)
obtain x where obt2: "read es s t = Some x"
using Cons.prems obt1 by (auto split: option.splits)
have fct0: "(pn_c x) (u1, v1) = 0 ∧ (pn_c x) (v1, u1) = 0 ∧ c1 > 0"
using Cons.prems obt1 obt2 by (auto split: option.splits if_splits)
have fct1: "c1 > 0 ∧ u1 ≠ v1 ∧ v1 ≠ s ∧ u1 ≠ t"
using Cons.prems obt1 obt2 by (auto split: option.splits if_splits)
obtain c' V' sc' ps' pd' s_n' t_n' where obt3: "x = (|pn_c = c', pn_V = V',
pn_succ = sc', pn_pred = pd', pn_adjmap = ps', pn_s_node = s_n', pn_t_node = t_n'|)),"
apply (cases x) by auto
then have "read es s t = Some (|pn_c = c', pn_V = V', pn_succ = sc', pn_pred = pd',
pn_adjmap = ps', pn_s_node = s_n', pn_t_node = t_n'|))," using obt2 by blast
note fct = Cons.IH[OF this]
have fct2: "s_n = (s_n' ∨ u1 = s)"
using fct0 fct1 Cons.prems obt1 obt2 obt3 by simp
have fct3: "t_n = (t_n' ∨ v1 = t)"
using fct0 fct1 Cons.prems obt1 obt2 obt3 by simp
have fct4: "c = c' ((u1, v1) := c1)"
using fct0 fct1 Cons.prems obt1 obt2 obt3 by simp
have fct5: "V = V' ∪ {u1, v1}"
using fct0 fct1 Cons.prems obt1 obt2 obt3 by simp
have fct6: "succ = sc' (u1 := v1 # sc' u1)"
using fct0 fct1 Cons.prems obt1 obt2 obt3 by simp
have fct7: "pred = pd' (v1 := u1 # pd' v1)"
using fct0 fct1 Cons.prems obt1 obt2 obt3 by simp
have fct8: "adjmap = (ps' (u1 := v1 # ps' u1)) (v1 := u1 # ps' v1)"
using fct0 fct1 Cons.prems obt1 obt2 obt3 by simp
{
have "(es, c') ∈ ln_rel" using fct by blast
then have "ln_invar es" and "c' = ln_α es" unfolding ln_rel_def br_def by auto
have "ln_invar (e # es)"
proof (rule ccontr)
assume "¬ ?thesis"
have f1: "∀(u, v, c) ∈ set (e # es). c>0" using `ln_invar es` fct0 obt1
unfolding ln_invar_def by auto
have f2: "distinct (map (λ(u, v, _). (u,v)) es)" using `ln_invar es`
unfolding ln_invar_def by auto
have "∃c1'. (u1, v1, c1') ∈ (set es) ∧ c1' ≠ 0"
proof (rule ccontr)
assume "¬ ?thesis"
then have "∀c1'. (u1, v1, c1') ∉ (set es) ∨ c1' = 0" by blast
then have "distinct (map (λ(u, v, _). (u,v)) (e # es))" using obt1 f2 f1 by auto
then have "ln_invar (e # es)" unfolding ln_invar_def using f1 by simp
thus "False" using `¬ ln_invar (e # es)` by blast
qed
then obtain c1' where "(u1, v1, c1') ∈ (set es) ∧ c1' ≠ 0" by blast
then have "c' (u1, v1) = (SOME c. (u1, v1, c) ∈ set es ∧ c ≠ 0)"
using `c' = ln_α es` unfolding ln_α_def by auto
then have "c' (u1, v1) ≠ 0" using `(u1, v1, c1') ∈ (set es) ∧ c1' ≠ 0` f1
by (metis (mono_tags, lifting) tfl_some)
thus "False" using fct0 obt3 by simp
qed
moreover {
{
fix a
have f1: "distinct (map (λ(u, v, _). (u,v)) (e # es))"
and f2: "∀u v. (u, v, 0) ∉ set (e # es)"
using `ln_invar (e # es)` unfolding ln_invar_def by auto
have "c a = ln_α (e # es) a"
proof (cases "a = (u1, v1)")
case True
have "c a = c1" using fct4 True by simp
moreover {
have "(ln_α (e # es)) a = (SOME c. (u1, v1, c) ∈ set (e # es) ∧ c ≠ 0)"
(is "?L = ?R") unfolding ln_α_def using obt1 fct0 True by auto
moreover have "?R = c1"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain c1' where "(u1, v1, c1') ∈ set (e # es)
∧ c1' ≠ 0 ∧ c1' ≠ c1" using fct0 obt1 by auto
then have "¬distinct (map (λ(u, v, _). (u,v)) (e # es))"
using obt1 by (metis (mono_tags, lifting) Pair_inject
distinct_map_eq list.set_intros(1) split_conv)
thus "False" using f1 by blast
qed
ultimately have "?L = c1" by blast
}
ultimately show ?thesis by simp
next
case False
have f1: "∀u1' v1' c1'. u1' ≠ u1 ∨ v1' ≠ v1 --> ((u1', v1', c1') ∈ set (e # es)
<-> (u1', v1', c1') ∈ set es)" using obt1 by auto
obtain u1' v1' where "a = (u1', v1')" apply (cases a) by auto
{
have "(ln_α (e # es)) (u1', v1') = (ln_α es) (u1', v1')"
proof (cases "∃ c1'. (u1', v1', c1') ∈ set (e # es) ∧ c1' ≠ 0")
case True
thus ?thesis unfolding ln_α_def
using f1 False True `a = (u1', v1')` by auto
next
case False
thus ?thesis unfolding ln_α_def by auto
qed
then have "(ln_α (e # es)) a = (ln_α es) a" using `a = (u1', v1')` by simp
}
moreover have "c a = c' a" using False fct4 by simp
moreover have "c' a = ln_α es a" using `c' = ln_α es` by simp
ultimately show ?thesis by simp
qed
}
then have "c = ln_α (e # es)" by auto
}
ultimately have "(e # es, c) ∈ ln_rel" unfolding ln_rel_def br_def by simp
}
moreover {
have "Graph.V c = Graph.V c' ∪ {u1, v1}" unfolding Graph.V_def Graph.E_def
using fct0 fct4 by auto
moreover have "Graph.V c' = V'" using fct by blast
ultimately have "Graph.V c = V" using fct5 by auto
}
moreover {
have "finite V'" using fct by blast
then have "finite V" using fct5 by auto
}
moreover {
assume "s_n"
then have "s_n' ∨ u1 = s" using fct2 by blast
then have "s ∈ V"
proof
assume "s_n'"
thus ?thesis using fct fct5 by auto
next
assume "u1 = s"
thus ?thesis using fct5 by simp
qed
}
moreover {
assume "t_n"
then have "t_n' ∨ v1 = t" using fct3 by blast
then have "t ∈ V"
proof
assume "t_n'"
thus ?thesis using fct fct5 by auto
next
assume "v1 = t"
thus ?thesis using fct5 by simp
qed
}
moreover {
assume "¬s_n"
then have "¬s_n' ∧ u1 ≠ s" using fct2 by blast
then have "s ∉ V" using fct fct5 fct1 by auto
}
moreover {
assume "¬t_n"
then have "¬t_n' ∧ v1 ≠ t" using fct3 by blast
then have "t ∉ V" using fct fct5 fct1 by auto
}
moreover have "∀u v. (c (u, v) ≥ 0)" using fct fct4 fct1 fct0 by auto
moreover have "∀u. c (u, u) = 0" using fct fct4 fct1 fct0 by auto
moreover have "∀u. c (u, s) = 0" using fct fct4 fct1 fct0 by auto
moreover have "∀u. c (t, u) = 0" using fct fct4 fct1 fct0 by auto
moreover {
fix a b
assume "c (a, b) ≠ 0"
then have "a ≠ b" using `∀u. c (u, u) = 0` by auto
have "c (b, a) = 0"
proof (cases "(a, b) = (u1, v1)")
case True
then have "c (b, a) = c' (v1, u1)" using fct4 `a ≠ b` by auto
moreover have "c' (v1, u1) = 0" using fct0 obt3 by auto
ultimately show ?thesis by simp
next
case False
thus ?thesis
proof (cases "(b, a) = (u1, v1)")
case True
then have "c (a, b) = c' (v1, u1)" using fct4 `a ≠ b` by auto
moreover have "c' (v1, u1) = 0" using fct0 obt3 by auto
ultimately show ?thesis using `c (a, b) ≠ 0` by simp
next
case False
then have "c (b, a) = c' (b, a)" using fct4 by auto
moreover have "c (a, b) = c' (a, b)"
using False `(a, b) ≠ (u1, v1)` fct4 by auto
ultimately show ?thesis using fct `c (a, b) ≠ 0` by auto
qed
qed
} note n_fct = this
moreover {
{
fix a
assume "a ≠ u1"
then have "succ a = sc' a" using fct6 by simp
moreover have "set (sc' a) = Graph.E c' `` {a} ∧ distinct (sc' a)"
using fct by blast
ultimately have "set (succ a) = Graph.E c``{a} ∧ distinct (succ a)"
unfolding Graph.E_def using fct4 `a ≠ u1` by auto
}
moreover {
fix a
assume "a = u1"
have "set (succ a) = Graph.E c``{a} ∧ distinct (succ a)"
proof (cases "c' (u1, v1) = 0")
case True
have fct: "set (sc' a) = Graph.E c' `` {a} ∧ distinct (sc' a)"
using fct by blast
have "succ a = v1 # sc' a" using `a = u1` fct6 True by simp
moreover have "Graph.E c = Graph.E c' ∪ {(u1, v1)}"
unfolding Graph.E_def using fct4 fct0 by auto
moreover have "v1 ∉ set (sc' a)"
proof (rule ccontr)
assume "¬ ?thesis"
then have "c' (a, v1) ≠ 0" using fct unfolding Graph.E_def by auto
thus "False" using True `a = u1` by simp
qed
ultimately show ?thesis using `a = u1` fct by auto
next
case False
thus ?thesis using fct0 obt3 by auto
qed
}
ultimately have "∀u. set (succ u) = Graph.E c `` {u} ∧ distinct (succ u)" by metis
}
moreover {
{
fix a
assume "a ≠ v1"
then have "pred a = pd' a" using fct7 by simp
moreover have "set (pd' a) = (Graph.E c')¯ `` {a} ∧ distinct (pd' a)"
using fct by blast
ultimately have "set (pred a) = (Graph.E c)¯``{a} ∧ distinct (pred a)"
unfolding Graph.E_def using fct4 `a ≠ v1` by auto
}
moreover {
fix a
assume "a = v1"
have "set (pred a) = (Graph.E c)¯``{a} ∧ distinct (pred a)"
proof (cases "c' (u1, v1) = 0")
case True
have fct: "set (pd' a) = (Graph.E c')¯ `` {a} ∧ distinct (pd' a)"
using fct by blast
have "pred a = u1 # pd' a" using `a = v1` fct7 True by simp
moreover have "Graph.E c = Graph.E c' ∪ {(u1, v1)}"
unfolding Graph.E_def using fct4 fct0 by auto
moreover have "u1 ∉ set (pd' a)"
proof (rule ccontr)
assume "¬ ?thesis"
then have "c' (u1, a) ≠ 0" using fct unfolding Graph.E_def by auto
thus "False" using True `a = v1` by simp
qed
ultimately show ?thesis using `a = v1` fct by auto
next
case False
thus ?thesis using fct0 obt3 by auto
qed
}
ultimately have "∀u. set (pred u) = (Graph.E c)¯`` {u} ∧ distinct (pred u)" by metis
}
moreover {
{
fix a
assume "a ≠ u1 ∧ a ≠ v1"
then have "adjmap a = ps' a" using fct8 by simp
moreover have "set (ps' a) =
Graph.E c'``{a} ∪ (Graph.E c')¯``{a} ∧ distinct (ps' a)" using fct by blast
ultimately have "set (adjmap a) = Graph.E c``{a} ∪ (Graph.E c)¯``{a} ∧
distinct (adjmap a)" unfolding Graph.E_def using fct4 `a ≠ u1 ∧ a ≠ v1` by auto
}
moreover {
fix a
assume "a = u1 ∨ a = v1"
then have "set (adjmap a) = Graph.E c``{a} ∪ (Graph.E c)¯``{a} ∧ distinct (adjmap a)"
proof
assume "a = u1"
show ?thesis
proof (cases "c' (u1, v1) = 0 ∧ c' (v1, u1) = 0")
case True
have fct: "set (ps' a) = Graph.E c' `` {a} ∪ (Graph.E c')¯ `` {a} ∧
distinct (ps' a)" using fct by blast
have "adjmap a = v1 # ps' a" using `a = u1` fct8 True by simp
moreover have "Graph.E c = Graph.E c' ∪ {(u1, v1)}"
unfolding Graph.E_def using fct4 fct0 by auto
moreover have "v1 ∉ set (ps' a)"
proof (rule ccontr)
assume "¬ ?thesis"
then have "c' (a, v1) ≠ 0 ∨ c' (v1, a) ≠ 0"
using fct unfolding Graph.E_def by auto
thus "False" using True `a = u1` by simp
qed
ultimately show ?thesis using `a = u1` fct by auto
next
case False
thus ?thesis using fct0 obt3 by auto
qed
next
assume "a = v1"
show ?thesis
proof (cases "c' (u1, v1) = 0 ∧ c' (v1, u1) = 0")
case True
have fct: "set (ps' a) = Graph.E c' `` {a} ∪ (Graph.E c')¯ `` {a} ∧
distinct (ps' a)" using fct by blast
have "adjmap a = u1 # ps' a" using `a = v1` fct8 True by simp
moreover have "Graph.E c = Graph.E c' ∪ {(u1, v1)}"
unfolding Graph.E_def using fct4 fct0 by auto
moreover have "u1 ∉ set (ps' a)"
proof (rule ccontr)
assume "¬ ?thesis"
then have "c' (u1, a) ≠ 0 ∨ c' (a, u1) ≠ 0"
using fct unfolding Graph.E_def by auto
thus "False" using True `a = v1` by simp
qed
ultimately show ?thesis using `a = v1` fct by auto
next
case False
thus ?thesis using fct0 obt3 by auto
qed
qed
}
ultimately have "∀u. set (adjmap u) = Graph.E c``{u} ∪ (Graph.E c)¯``{u} ∧
distinct (adjmap u)" by metis
}
ultimately show ?case by simp
qed
lemma read_correct2: "read el s t = None ==> ¬ln_invar el
∨ (∃u v c. (u,v,c) ∈ set el ∧ ¬(c > 0))
∨ (∃u c. (u, u, c) ∈ set el ∧ c ≠ 0) ∨
(∃u c. (u, s, c) ∈ set el ∧ c ≠ 0) ∨ (∃u c. (t, u, c) ∈ set el ∧ c ≠ 0) ∨
(∃u v c1 c2. (u, v, c1) ∈ set el ∧ (v, u, c2) ∈ set el ∧ c1 ≠ 0 ∧ c2 ≠ 0)"
proof (induction el)
case Nil
thus ?case by auto
next
case (Cons e el)
thus ?case
proof (cases "read el s t = None")
case True
note Cons.IH[OF this]
thus ?thesis
proof
assume "¬ln_invar el"
then have "¬distinct (map (λ(u, v, _). (u,v)) (e # el)) ∨
(∃(u, v, c) ∈ set (e # el). ¬(c>0))" unfolding ln_invar_def by fastforce
thus ?thesis unfolding ln_invar_def by fastforce
next
assume "(∃u v c. (u, v, c) ∈ set (el) ∧ ¬(c > 0))
∨ (∃u c. (u, u, c) ∈ set el ∧ c ≠ 0) ∨
(∃u c. (u, s, c) ∈ set el ∧ c ≠ 0) ∨ (∃u c. (t, u, c) ∈ set el ∧ c ≠ 0) ∨
(∃u v c1 c2. (u, v, c1) ∈ set el ∧ (v, u, c2) ∈ set el ∧ c1 ≠ 0 ∧ c2 ≠ 0)"
moreover {
assume "(∃u v c. (u, v, c) ∈ set el ∧ ¬(c > 0))"
then have "(∃u v c. (u, v, c) ∈ set (e # el) ∧ ¬(c > 0))" by auto
}
moreover {
assume "(∃u c. (u, u, c) ∈ set el ∧ c ≠ 0)"
then have "(∃u c. (u, u, c) ∈ set (e # el) ∧ c ≠ 0)" by auto
}
moreover {
assume "(∃u c. (u, s, c) ∈ set el ∧ c ≠ 0)"
then have "(∃u c. (u, s, c) ∈ set (e # el) ∧ c ≠ 0)" by auto
}
moreover {
assume "(∃u c. (t, u, c) ∈ set el ∧ c ≠ 0)"
then have "(∃u c. (t, u, c) ∈ set (e # el) ∧ c ≠ 0)" by auto
}
moreover {
assume "(∃u v c1 c2. (u, v, c1) ∈ set el ∧ (v, u, c2) ∈ set el ∧ c1 ≠ 0 ∧ c2 ≠ 0)"
then have "(∃u v c1 c2. (u, v, c1) ∈ set (e # el) ∧
(v, u, c2) ∈ set (e # el) ∧ c1 ≠ 0 ∧ c2 ≠ 0)" by auto
}
ultimately show ?thesis by blast
qed
next
case False
then obtain x where obt1: "read el s t = Some x" by auto
obtain u1 v1 c1 where obt2: "e = (u1, v1, c1)" apply (cases e) by auto
obtain c' V' sc' pd' ps' s_n' t_n' where obt3: "x = (|pn_c = c', pn_V = V', pn_succ = sc',
pn_pred = pd', pn_adjmap = ps', pn_s_node = s_n', pn_t_node = t_n'|)),"
apply (cases x) by auto
then have "(el, c') ∈ ln_rel" using obt1 read_correct1[of el s t] by simp
then have "c' = ln_α el" unfolding ln_rel_def br_def by simp
have "(c' (u1, v1) ≠ 0 ∨ c' (v1, u1) ≠ 0 ∨ c1 ≤ 0) ∨
(c1 > 0 ∧ (u1 = v1 ∨ v1 = s ∨ u1 = t))"
using obt1 obt2 obt3 False Cons.prems
by (auto split:option.splits if_splits)
moreover {
assume "c1 ≤ 0"
then have "¬ ln_invar (e # el)" unfolding ln_invar_def using obt2 by auto
}
moreover {
assume "c1 > 0 ∧ u1 = v1"
then have "(∃u c. (u, u, c) ∈ set (e # el) ∧ c > 0)" using obt2 by auto
}
moreover {
assume "c1 > 0 ∧ v1 = s"
then have "(∃u c. (u, s, c) ∈ set (e # el) ∧ c > 0)" using obt2 by auto
}
moreover {
assume "c1 > 0 ∧ u1 = t"
then have "(∃u c. (t, u, c) ∈ set (e # el) ∧ c > 0)" using obt2 by auto
}
moreover {
assume "c' (u1, v1) ≠ 0"
then have "∃c1'. (u1, v1, c1') ∈ set el" using `c' = ln_α el` unfolding ln_α_def
by (auto split:if_splits)
then have "¬ distinct (map (λ(u, v, _). (u, v)) (e # el))" using obt2 by force
then have "¬ln_invar (e # el)" unfolding ln_invar_def by auto
}
moreover {
assume "c' (v1, u1) ≠ 0"
then have "∃c1'. (v1, u1, c1') ∈ set el ∧ c1' ≠ 0"
using `c' = ln_α el` unfolding ln_α_def by (auto split:if_splits)
then have "¬ln_invar (e # el) ∨ (∃u v c1 c2.
(u, v, c1) ∈ set (e # el) ∧ (v, u, c2) ∈ set (e # el) ∧ c1 ≠ 0 ∧ c2 ≠ 0)"
proof (cases "c1 ≠ 0")
case True
thus ?thesis using `∃c1'. (v1, u1, c1') ∈ set el ∧ c1' ≠ 0` obt2 by auto
next
case False
then have "¬ln_invar (e # el)" unfolding ln_invar_def using obt2 by auto
thus ?thesis by blast
qed
}
ultimately show ?thesis by blast
qed
qed
record 'capacity::linordered_idom pre_network' =
pn_c' :: "(nat*nat,'capacity) ahm"
pn_V' :: "nat ahs"
pn_succ' :: "(nat,nat list) ahm"
pn_pred' :: "(nat,nat list) ahm"
pn_adjmap' :: "(nat,nat list) ahm"
pn_s_node' :: bool
pn_t_node' :: bool
definition "pnet_α pn' ≡ (|
pn_c = the_default 0 o (ahm.α (pn_c' pn')),
pn_V = ahs_α (pn_V' pn'),
pn_succ = the_default [] o (ahm.α (pn_succ' pn')),
pn_pred = the_default [] o (ahm.α (pn_pred' pn')),
pn_adjmap = the_default [] o (ahm.α (pn_adjmap' pn')),
pn_s_node = pn_s_node' pn',
pn_t_node = pn_t_node' pn'
|)),"
definition "pnet_rel ≡ br pnet_α (λ_. True)"
definition "ahm_ld a ahm k ≡ the_default a (ahm.lookup k ahm)"
abbreviation "cap_lookup ≡ ahm_ld 0"
abbreviation "succ_lookup ≡ ahm_ld []"
fun read' :: "(nat × nat × 'capacity::linordered_idom) list => nat => nat =>
'capacity pre_network' option" where
"read' [] _ _ = Some (|
pn_c' = ahm.empty (),
pn_V' = ahs.empty (),
pn_succ' = ahm.empty (),
pn_pred' = ahm.empty (),
pn_adjmap' = ahm.empty (),
pn_s_node' = False,
pn_t_node' = False
|)),"
| "read' ((u, v, c) # es) s t = ((case (read' es s t) of
Some x =>
(if cap_lookup (pn_c' x) (u, v) = 0 ∧ cap_lookup (pn_c' x) (v, u) = 0 ∧ c > 0 then
(if u = v ∨ v = s ∨ u = t then
None
else
Some (x(|
pn_c' := ahm.update (u, v) c (pn_c' x),
pn_V' := ahs.ins u (ahs.ins v (pn_V' x)),
pn_succ' := ahm.update u (v # (succ_lookup (pn_succ' x) u)) (pn_succ' x),
pn_pred' := ahm.update v (u # (succ_lookup (pn_pred' x) v)) (pn_pred' x),
pn_adjmap' := ahm.update u (v # (succ_lookup (pn_adjmap' x) u))
(ahm.update v (u # (succ_lookup (pn_adjmap' x) v)) (pn_adjmap' x)),
pn_s_node' := pn_s_node' x ∨ u = s,
pn_t_node' := pn_t_node' x ∨ v = t
|)),))
else
None)
| None => None))"
lemma read'_correct: "read el s t = map_option pnet_α (read' el s t)"
apply (induction el s t rule: read.induct)
by (auto
simp: pnet_α_def o_def ahm.correct ahs.correct ahm_ld_def
split: option.splits)
lemma read'_correct_alt: "(read' el s t, read el s t) ∈ ⟨pnet_rel⟩option_rel"
unfolding pnet_rel_def br_def
apply (simp add: option_rel_def read'_correct)
using domIff by force
export_code read in SML
definition "reachable_spec c s ≡ RETURN (((Graph.E c)⇧*)``{s}) "
definition "reaching_spec c t ≡ RETURN ((((Graph.E c)¯)⇧*)``{t})"
definition "checkNet cc s t ≡ do {
if s = t then
RETURN None
else do {
let rd = read cc s t;
case rd of
None => RETURN None
| Some x => do {
if pn_s_node x ∧ pn_t_node x then
do {
ASSERT(finite ((Graph.E (pn_c x))⇧* `` {s}));
ASSERT(finite (((Graph.E (pn_c x))¯)⇧* `` {t}));
ASSERT(∀u. set ((pn_succ x) u) = Graph.E (pn_c x) `` {u} ∧ distinct ((pn_succ x) u));
ASSERT(∀u. set ((pn_pred x) u) = (Graph.E (pn_c x))¯ `` {u} ∧ distinct ((pn_pred x) u));
succ_s \<leftarrow> reachable_spec (pn_c x) s;
pred_t \<leftarrow> reaching_spec (pn_c x) t;
if (pn_V x) = succ_s ∧ (pn_V x) = pred_t then
RETURN (Some (pn_c x, pn_adjmap x))
else
RETURN None
}
else
RETURN None
}
}
}"
lemma checkNet_pre_correct1 : "checkNet el s t ≤
SPEC (λ r. r = Some (c, adjmap) --> (el, c) ∈ ln_rel ∧ Network c s t ∧
(∀u. set (adjmap u) = Graph.E c``{u} ∪ (Graph.E c)¯``{u} ∧ distinct (adjmap u)))"
unfolding checkNet_def reachable_spec_def reaching_spec_def
apply (refine_vcg)
apply clarsimp_all
proof -
{
fix x
assume asm1: "s ≠ t"
assume asm2: "read el s t = Some x"
assume asm3: "pn_s_node x"
assume asm4: "pn_t_node x"
obtain c V sc pd adjmap where obt: "x = (|pn_c = c, pn_V = V,
pn_succ = sc, pn_pred = pd, pn_adjmap = adjmap, pn_s_node = True, pn_t_node = True|)),"
apply (cases x) using asm3 asm4 by auto
then have "read el s t = Some (|pn_c = c, pn_V = V, pn_succ = sc, pn_pred = pd,
pn_adjmap = adjmap, pn_s_node = True, pn_t_node = True|))," using asm2 by simp
note fct = read_correct1[OF this]
then have [simp, intro!]: "finite (Graph.V c)" by blast
have "Graph.E c ⊆ (Graph.V c) × (Graph.V c)" unfolding Graph.V_def by auto
from finite_subset[OF this] have "finite (Graph.E (pn_c x))" by (simp add: obt)
then show "finite ((Graph.E (pn_c x))⇧* `` {s})"
and "finite (((Graph.E (pn_c x))¯)⇧* `` {t})" by (auto simp add: finite_rtrancl_Image)
}
{
fix x
assume asm1: "s ≠ t"
assume asm2: "read el s t = Some x"
assume asm3: "finite ((Graph.E (pn_c x))⇧* `` {s})"
assume asm4: "finite (((Graph.E (pn_c x))¯)⇧* `` {t})"
assume asm5: "pn_s_node x"
assume asm6: "pn_t_node x"
obtain c V sc pd adjmap where obt: "x = (|pn_c = c, pn_V = V,
pn_succ = sc, pn_pred = pd, pn_adjmap = adjmap, pn_s_node = True, pn_t_node = True|)),"
apply (cases x) using asm5 asm6 by auto
then have "read el s t = Some (|pn_c = c, pn_V = V, pn_succ = sc, pn_pred = pd,
pn_adjmap = adjmap, pn_s_node = True, pn_t_node = True|))," using asm2 by simp
note fct = read_correct1[OF this]
have "!!u. set ((pn_succ x) u) = Graph.E (pn_c x) `` {u} ∧ distinct ((pn_succ x) u)"
using fct obt by simp
moreover have "!!u. set ((pn_pred x) u) = (Graph.E (pn_c x))¯ `` {u} ∧
distinct ((pn_pred x) u)" using fct obt by simp
ultimately show "!!u. set ((pn_succ x) u) = Graph.E (pn_c x) `` {u}" and
"!!u. distinct ((pn_succ x) u)" and "!!u. set ((pn_pred x) u) = (Graph.E (pn_c x))¯ `` {u}"
and "!!u. distinct ((pn_pred x) u)" by auto
}
{
fix x
assume asm1: "s ≠ t"
assume asm2: "read el s t = Some x"
assume asm3: "pn_s_node x"
assume asm4: "pn_t_node x"
assume asm5: "((Graph.E (pn_c x))¯)⇧* `` {t} = (Graph.E (pn_c x))⇧* `` {s}"
assume asm6: "pn_V x = (Graph.E (pn_c x))⇧* `` {s}"
assume asm7: "c = pn_c x"
assume asm8: "adjmap = pn_adjmap x"
obtain V sc pd where obt: "x = (|pn_c = c, pn_V = V,
pn_succ = sc, pn_pred = pd, pn_adjmap = adjmap, pn_s_node = True, pn_t_node = True|)),"
apply (cases x) using asm3 asm4 asm7 asm8 by auto
then have "read el s t = Some (|pn_c = c, pn_V = V, pn_succ = sc, pn_pred = pd,
pn_adjmap = adjmap, pn_s_node = True, pn_t_node = True|))," using asm2 by simp
note fct = read_correct1[OF this]
have "!!u. set ((pn_succ x) u) = Graph.E (pn_c x) `` {u} ∧ distinct ((pn_succ x) u)"
using fct obt by simp
moreover have "!!u. set ((pn_pred x) u) = (Graph.E (pn_c x))¯ `` {u} ∧
distinct ((pn_pred x) u)" using fct obt by simp
moreover have "(el, pn_c x) ∈ ln_rel" using fct asm7 by simp
moreover {
{
{
have "Graph.V c ⊆ ((Graph.E c))⇧* `` {s}" using asm6 obt fct by simp
then have "∀v∈(Graph.V c). Graph.isReachable c s v"
unfolding Graph.connected_def using Graph.rtc_isPath[of s _ c] by auto
}
moreover {
have "Graph.V c ⊆ ((Graph.E c)¯)⇧* `` {t}" using asm5 asm6 obt fct by simp
then have "∀v∈(Graph.V c). Graph.isReachable c v t"
unfolding Graph.connected_def using Graph.rtci_isPath by fastforce
}
ultimately have "∀v∈(Graph.V c). Graph.isReachable c s v ∧ Graph.isReachable c v t" by simp
}
moreover {
have "finite (Graph.V c)" and "s ∈ (Graph.V c)" using fct obt by auto
note Graph.reachable_ss_V[OF `s ∈ (Graph.V c)`]
note finite_subset[OF this `finite (Graph.V c)`]
}
ultimately have "Network (pn_c x) s t" unfolding Network_def using asm1 fct asm7
by (simp add: Graph.E_def)
}
moreover have "∀u.(set (pn_adjmap x u) =
Graph.E (pn_c x) `` {u} ∪ (Graph.E (pn_c x))¯ `` {u})" using fct obt by simp
moreover have "∀u. distinct (pn_adjmap x u)" using fct obt by simp
ultimately show "(el, pn_c x) ∈ ln_rel" and "Network (pn_c x) s t" and
"!!u. set (pn_adjmap x u) = Graph.E (pn_c x) `` {u} ∪ (Graph.E (pn_c x))¯ `` {u}" and
"!!u. distinct (pn_adjmap x u)" by auto
}
qed
lemma checkNet_pre_correct2_aux:
assumes asm1: "s ≠ t"
assumes asm2: "read el s t = Some x"
assumes asm3: "∀u. set (pn_succ x u) = Graph.E (pn_c x) `` {u} ∧ distinct (pn_succ x u)"
assumes asm4: "∀u. set (pn_pred x u) = (Graph.E (pn_c x))¯ `` {u} ∧ distinct (pn_pred x u)"
assumes asm5: "pn_V x = (Graph.E (pn_c x))⇧* `` {s} --> (Graph.E (pn_c x))⇧* `` {s} ≠
((Graph.E (pn_c x))¯)⇧* `` {t}"
assumes asm6: "pn_s_node x"
assumes asm7: "pn_t_node x"
assumes asm8: "ln_invar el"
assumes asm9: "Network (ln_α el) s t"
shows "False"
proof -
obtain c V sc pd ps where obt: "x = (|pn_c = c, pn_V = V, pn_succ = sc, pn_pred = pd,
pn_adjmap = ps, pn_s_node = True, pn_t_node = True|)),"
apply (cases x) using asm3 asm4 asm6 asm7 by auto
then have "read el s t = Some (|pn_c = c, pn_V = V, pn_succ = sc, pn_pred = pd,
pn_adjmap = ps, pn_s_node = True, pn_t_node = True|))," using asm2 by simp
note fct = read_correct1[OF this]
have "pn_V x ≠ (Graph.E (pn_c x))⇧* `` {s} ∨ (pn_V x = (Graph.E (pn_c x))⇧* `` {s} ∧
((Graph.E (pn_c x))¯)⇧* `` {t} ≠ (Graph.E (pn_c x))⇧* `` {s})" using asm5 by blast
thus "False"
proof
assume "pn_V x = (Graph.E (pn_c x))⇧* `` {s} ∧
((Graph.E (pn_c x))¯)⇧* `` {t} ≠ (Graph.E (pn_c x))⇧* `` {s}"
then have "¬(Graph.V c ⊆ ((Graph.E c)¯)⇧* `` {t}) ∨ ¬(((Graph.E c)¯)⇧* `` {t} ⊆ Graph.V c)"
using asm5 obt fct by simp
then have "∃v∈(Graph.V c). ¬Graph.isReachable c v t"
proof
assume "¬(((Graph.E c)¯)⇧* `` {t} ⊆ Graph.V c)"
then obtain x where o1:"x ∈ ((Graph.E c)¯)⇧* `` {t} ∧ x ∉ Graph.V c" by blast
then have "∃p. Graph.isPath c x p t" using Graph.rtci_isPath by auto
then obtain p where "Graph.isPath c x p t" by blast
then have "x ∈ Graph.V c"
proof (cases "p = []")
case True
then have "x = t" using `Graph.isPath c x p t` Graph.isPath.simps(1) by auto
thus ?thesis using fct by auto
next
case False
then obtain p1 ps where "p = p1 # ps" by (meson neq_Nil_conv)
then have "Graph.isPath c x (p1 # ps) t" using `Graph.isPath c x p t` by auto
then have "fst p1 = x ∧ c p1 ≠ 0" using Graph.isPath_head[of c x p1 ps t] by (auto simp: Graph.E_def)
then have "∃v. c (x, v) ≠ 0" by (metis prod.collapse)
then have "x ∈ Graph.V c" unfolding Graph.V_def Graph.E_def by auto
thus ?thesis by simp
qed
thus ?thesis using o1 by auto
next
assume "¬(Graph.V c ⊆ ((Graph.E c)¯)⇧* `` {t})"
then obtain x where o1:"x ∉ ((Graph.E c)¯)⇧* `` {t} ∧ x ∈ Graph.V c" by blast
then have "(x , t) ∉ (Graph.E c)⇧*" by (meson Image_singleton_iff rtrancl_converseI)
have "∀p. ¬Graph.isPath c x p t"
proof (rule ccontr)
assume "¬?thesis"
then obtain p where "Graph.isPath c x p t" by blast
thus "False" using Graph.isPath_rtc `(x , t) ∉ (Graph.E c)⇧*` by auto
qed
then have "¬Graph.isReachable c x t" unfolding Graph.connected_def by auto
thus ?thesis using o1 by auto
qed
moreover {
have "(el, c) ∈ ln_rel" using fct obt by simp
then have "c = ln_α el" unfolding ln_rel_def br_def by auto
}
ultimately have "¬Network (ln_α el) s t" unfolding Network_def by auto
thus ?thesis using asm9 by blast
next
assume "pn_V x ≠ (Graph.E (pn_c x))⇧* `` {s}"
then have "¬(Graph.V c ⊆ (Graph.E c)⇧* `` {s}) ∨ ¬((Graph.E c)⇧* `` {s} ⊆ Graph.V c)"
using asm5 obt fct by simp
then have "∃v∈(Graph.V c). ¬Graph.isReachable c s v"
proof
assume "¬((Graph.E c)⇧* `` {s} ⊆ Graph.V c)"
then obtain x where o1:"x ∈ (Graph.E c)⇧* `` {s} ∧ x ∉ Graph.V c" by blast
then have "∃p. Graph.isPath c s p x" using Graph.rtc_isPath by auto
then obtain p where "Graph.isPath c s p x" by blast
then have "x ∈ Graph.V c"
proof (cases "p = []")
case True
then have "x = s" using `Graph.isPath c s p x` by (auto simp: Graph.isPath.simps(1))
thus ?thesis using fct by auto
next
case False
then obtain p1 ps where "p = ps @ [p1]" by (metis append_butlast_last_id)
then have "Graph.isPath c s (ps @ [p1]) x" using `Graph.isPath c s p x` by auto
then have "snd p1 = x ∧ c p1 ≠ 0" using Graph.isPath_tail[of c s ps p1 x] by (auto simp: Graph.E_def)
then have "∃v. c (v, x) ≠ 0" by (metis prod.collapse)
then have "x ∈ Graph.V c" unfolding Graph.V_def Graph.E_def by auto
thus ?thesis by simp
qed
thus ?thesis using o1 by auto
next
assume "¬(Graph.V c ⊆ (Graph.E c)⇧* `` {s})"
then obtain x where o1:"x ∉ (Graph.E c)⇧* `` {s} ∧ x ∈ Graph.V c" by blast
then have "(s , x) ∉ (Graph.E c)⇧*" by (meson Image_singleton_iff rtrancl_converseI)
have "∀p. ¬Graph.isPath c s p x"
proof (rule ccontr)
assume "¬?thesis"
then obtain p where "Graph.isPath c s p x" by blast
thus "False" using Graph.isPath_rtc `(s, x) ∉ (Graph.E c)⇧*` by auto
qed
then have "¬Graph.isReachable c s x" unfolding Graph.connected_def by auto
thus ?thesis using o1 by auto
qed
moreover {
have "(el, c) ∈ ln_rel" using fct obt by simp
then have "c = ln_α el" unfolding ln_rel_def br_def by auto
}
ultimately have "¬Network (ln_α el) s t" unfolding Network_def by auto
thus ?thesis using asm9 by blast
qed
qed
lemma checkNet_pre_correct2:
"checkNet el s t ≤ SPEC (λr. r = None --> ¬ln_invar el ∨ ¬Network (ln_α el) s t)"
unfolding checkNet_def reachable_spec_def reaching_spec_def
apply (refine_vcg)
apply (clarsimp_all)
proof -
{
assume "s = t" and "ln_invar el" and "Network (ln_α el) t t"
thus "False" using Network_def by auto
}
next {
assume "s ≠ t" and "read el s t = None" and "ln_invar el" and "Network (ln_α el) s t"
note read_correct2[OF `read el s t = None`]
thus "False"
proof
assume "¬ln_invar el"
thus ?thesis using `ln_invar el` by blast
next
assume asm: "(∃u v c. (u, v, c) ∈ set el ∧ ¬(c > 0))
∨ (∃u c. (u, u, c) ∈ set el ∧ c≠0) ∨ (∃u c. (u, s, c) ∈ set el ∧ c≠0) ∨
(∃u c. (t, u, c) ∈ set el ∧ c≠0) ∨ (∃u v c1 c2. (u, v, c1) ∈ set el ∧
(v, u, c2) ∈ set el ∧ c1≠0 ∧ c2≠0)"
moreover {
assume A: "(∃u v c. (u, v, c) ∈ set el ∧ ¬(c>0))"
then have "¬ln_invar el" using not_less by (fastforce simp: ln_invar_def)
with ‹ln_invar el› have False by simp
}
moreover {
assume "(∃u c. (u, u, c) ∈ set el ∧ c≠0)"
then have "∃ u. ln_α el (u, u) ≠ 0" unfolding ln_α_def apply (auto split:if_splits)
by (metis (mono_tags, lifting) tfl_some)
then have "False" using `Network (ln_α el) s t` unfolding Network_def by (auto simp: Graph.E_def)
}
moreover {
assume "(∃u c. (u, s, c) ∈ set el ∧ c≠0)"
then have "∃ u. ln_α el (u, s) ≠ 0" unfolding ln_α_def apply (auto split:if_splits)
by (metis (mono_tags, lifting) tfl_some)
then have "False" using `Network (ln_α el) s t` unfolding Network_def by (auto simp: Graph.E_def)
}
moreover {
assume "(∃u c. (t, u, c) ∈ set el ∧ c≠0)"
then have "∃ u. ln_α el (t, u) ≠ 0" unfolding ln_α_def apply (auto split:if_splits)
by (metis (mono_tags, lifting) tfl_some)
then have "False" using `Network (ln_α el) s t` unfolding Network_def by (auto simp: Graph.E_def)
}
moreover {
assume "(∃u v c1 c2. (u, v, c1) ∈ set el ∧ (v, u, c2) ∈ set el ∧ c1≠0 ∧ c2≠0)"
then obtain u v c1 c2 where o1: "(u, v, c1) ∈ set el ∧ (v, u, c2) ∈ set el
∧ c1≠0 ∧ c2≠0" by blast
then have "ln_α el (u, v) ≠ 0" unfolding ln_α_def
apply (auto split:if_splits) by (metis (mono_tags, lifting) tfl_some)
moreover have "ln_α el (v, u) ≠ 0" unfolding ln_α_def using o1
apply (auto split:if_splits) by (metis (mono_tags, lifting) tfl_some)
ultimately have "¬ (∀u v. (ln_α el) (u, v) ≠ 0 --> (ln_α el) (v, u) = 0)" by auto
then have "False" using `Network (ln_α el) s t` unfolding Network_def by (auto simp: Graph.E_def)
}
ultimately show ?thesis by force
qed
}
next {
fix x
assume asm1: "s ≠ t"
assume asm2: "read el s t = Some x"
assume asm3: "pn_s_node x"
assume asm4: "pn_t_node x"
obtain c V sc pd adjmap where obt: "x = (|pn_c = c, pn_V = V,
pn_succ = sc, pn_pred = pd, pn_adjmap = adjmap, pn_s_node = True, pn_t_node = True|)),"
apply (cases x) using asm3 asm4 by auto
then have "read el s t = Some (|pn_c = c, pn_V = V, pn_succ = sc, pn_pred = pd,
pn_adjmap = adjmap, pn_s_node = True, pn_t_node = True|))," using asm2 by simp
note fct = read_correct1[OF this]
then have [simp]: "finite (Graph.V c)" by blast
have "Graph.E c ⊆ (Graph.V c) × (Graph.V c)" unfolding Graph.V_def by auto
from finite_subset[OF this] have "finite (Graph.E (pn_c x))" by (auto simp: obt)
then show "finite ((Graph.E (pn_c x))⇧* `` {s})"
and "finite (((Graph.E (pn_c x))¯)⇧* `` {t})" by (auto simp add: finite_rtrancl_Image)
}
{
fix x
assume asm1: "s ≠ t"
assume asm2: "read el s t = Some x"
assume asm3: "finite ((Graph.E (pn_c x))⇧* `` {s})"
assume asm4: "finite (((Graph.E (pn_c x))¯)⇧* `` {t})"
assume asm5: "pn_s_node x"
assume asm6: "pn_t_node x"
obtain c V sc pd adjmap where obt: "x = (|pn_c = c, pn_V = V,
pn_succ = sc, pn_pred = pd, pn_adjmap = adjmap, pn_s_node = True, pn_t_node = True|)),"
apply (cases x) using asm5 asm6 by auto
then have "read el s t = Some (|pn_c = c, pn_V = V, pn_succ = sc, pn_pred = pd,
pn_adjmap = adjmap, pn_s_node = True, pn_t_node = True|))," using asm2 by simp
note fct = read_correct1[OF this]
have "!!u. set ((pn_succ x) u) = Graph.E (pn_c x) `` {u} ∧ distinct ((pn_succ x) u)"
using fct obt by simp
moreover have "!!u. set ((pn_pred x) u) = (Graph.E (pn_c x))¯ `` {u} ∧
distinct ((pn_pred x) u)" using fct obt by simp
ultimately show "!!u. set ((pn_succ x) u) = Graph.E (pn_c x) `` {u}" and
"!!u. distinct ((pn_succ x) u)" and "!!u. set ((pn_pred x) u) = (Graph.E (pn_c x))¯ `` {u}"
and "!!u. distinct ((pn_pred x) u)" by auto
}
next {
fix x
assume asm1: "s ≠ t"
assume asm2: "read el s t = Some x"
assume asm3: "pn_s_node x --> ¬pn_t_node x"
assume asm4: "ln_invar el"
assume asm5: "Network (ln_α el) s t"
obtain c V sc pd ps s_node t_node where obt: "x = (|pn_c = c, pn_V = V, pn_succ = sc, pn_pred = pd,
pn_adjmap = ps, pn_s_node = s_node, pn_t_node = t_node|))," apply (cases x) by auto
then have "read el s t = Some (|pn_c = c, pn_V = V, pn_succ = sc, pn_pred = pd,
pn_adjmap = ps, pn_s_node = s_node, pn_t_node = t_node|))," using asm2 by simp
note fct = read_correct1[OF this]
have "(el, c) ∈ ln_rel" using fct obt by simp
then have "c = ln_α el" unfolding ln_rel_def br_def by auto
have "¬pn_s_node x ∨ ¬pn_t_node x" using asm3 by auto
then show "False"
proof
assume "¬pn_s_node x"
then have "¬s_node" using obt fct by auto
then have "s ∉ Graph.V c" using fct by auto
thus ?thesis using `c = ln_α el` asm5 Network_def by auto
next
assume "¬pn_t_node x"
then have "¬t_node" using obt fct by auto
then have "t ∉ Graph.V c" using fct by auto
thus ?thesis using `c = ln_α el` asm5 Network_def by auto
qed
}
next show "!!x. s ≠ t ==>
read el s t = Some x ==>
∀u. set (pn_succ x u) = Graph.E (pn_c x) `` {u} ∧ distinct (pn_succ x u) ==>
∀u. set (pn_pred x u) = (Graph.E (pn_c x))¯ `` {u} ∧ distinct (pn_pred x u) ==>
pn_V x = (Graph.E (pn_c x))⇧* `` {s} --> (Graph.E (pn_c x))⇧* `` {s} ≠ ((Graph.E (pn_c x))¯)⇧* `` {t} ==>
pn_s_node x ==> pn_t_node x ==> ln_invar el ==> Network (ln_α el) s t ==> False"
using checkNet_pre_correct2_aux by blast
qed
lemma checkNet_correct' : "checkNet el s t ≤ SPEC (λ r. case r of
Some (c, adjmap) =>
(el, c) ∈ ln_rel ∧ Network c s t
∧ (∀u. set (adjmap u) = Graph.E c``{u} ∪ (Graph.E c)¯``{u} ∧ distinct (adjmap u))
| None => ¬ln_invar el ∨ ¬Network (ln_α el) s t)"
using checkNet_pre_correct1[of el s t] checkNet_pre_correct2[of el s t]
by (auto split: option.splits simp: pw_le_iff refine_pw_simps)
lemma checkNet_correct : "checkNet el s t ≤ SPEC (λr. case r of
Some (c, adjmap) => (el, c) ∈ ln_rel ∧ Network c s t ∧ Graph.is_adj_map c adjmap
| None => ¬ln_invar el ∨ ¬Network (ln_α el) s t)"
using checkNet_pre_correct1[of el s t] checkNet_pre_correct2[of el s t]
by (auto split: option.splits simp: Graph.is_adj_map_def pw_le_iff refine_pw_simps)
definition "graph_of pn s ≡ (|
g_V = UNIV,
g_E = Graph.E (pn_c pn),
g_V0 = {s}
|)),"
definition "rev_graph_of pn s ≡ (|
g_V = UNIV,
g_E = (Graph.E (pn_c pn))¯,
g_V0 = {s}
|)),"
definition "checkNet2 cc s t ≡ do {
if s = t then
RETURN None
else do {
let rd = read cc s t;
case rd of
None => RETURN None
| Some x => do {
if pn_s_node x ∧ pn_t_node x then
do {
ASSERT(finite ((Graph.E (pn_c x))⇧* `` {s}));
ASSERT(finite (((Graph.E (pn_c x))¯)⇧* `` {t}));
ASSERT(∀u. set ((pn_succ x) u) = Graph.E (pn_c x) `` {u} ∧ distinct ((pn_succ x) u));
ASSERT(∀u. set ((pn_pred x) u) = (Graph.E (pn_c x))¯ `` {u} ∧ distinct ((pn_pred x) u));
let succ_s = (op_reachable (graph_of x s));
let pred_t = (op_reachable (rev_graph_of x t));
if (pn_V x) = succ_s ∧ (pn_V x) = pred_t then
RETURN (Some (pn_c x, pn_adjmap x))
else
RETURN None
}
else
RETURN None
}
}
}"
lemma checkNet2_correct: "checkNet2 c s t ≤ checkNet c s t"
apply (rule refine_IdD)
unfolding checkNet_def checkNet2_def graph_of_def rev_graph_of_def reachable_spec_def reaching_spec_def
apply (refine_rcg)
apply refine_dref_type
apply auto
done
definition "graph_of_impl pn' s ≡ (|
gi_V = λ_. True,
gi_E = succ_lookup (pn_succ' pn'),
gi_V0 = [s]
|)),"
definition "rev_graph_of_impl pn' t ≡ (|
gi_V = λ_. True,
gi_E = succ_lookup (pn_pred' pn'),
gi_V0 = [t]
|)),"
definition "well_formed_pn x ≡
(∀u. set ((pn_succ x) u) = Graph.E (pn_c x) `` {u} ∧ distinct ((pn_succ x) u))"
definition "rev_well_formed_pn x ≡
(∀u. set ((pn_pred x) u) = (Graph.E (pn_c x))¯ `` {u} ∧ distinct ((pn_pred x) u))"
lemma id_slg_rel_alt_a: "⟨Id⟩slg_rel
= { (s,E). ∀u. distinct (s u) ∧ set (s u) = E``{u} }"
by (auto simp add: slg_rel_def br_def list_set_rel_def dest: fun_relD)
lemma graph_of_impl_correct: "well_formed_pn pn ==> (pn', pn) ∈ pnet_rel ==>
(graph_of_impl pn' s, graph_of pn s) ∈ ⟨unit_rel,Id⟩g_impl_rel_ext"
unfolding pnet_rel_def graph_of_impl_def graph_of_def
g_impl_rel_ext_def gen_g_impl_rel_ext_def
apply (auto simp: fun_set_rel_def br_def list_set_rel_def id_slg_rel_alt_a ahm_ld_def)
apply (auto simp: well_formed_pn_def Graph.E_def pnet_α_def o_def ahm_correct)
done
lemma rev_graph_of_impl_correct:"[|rev_well_formed_pn pn; (pn',pn)∈pnet_rel|] ==>
(rev_graph_of_impl pn' s, rev_graph_of pn s) ∈ ⟨unit_rel,Id⟩g_impl_rel_ext"
unfolding pnet_rel_def rev_graph_of_impl_def rev_graph_of_def
g_impl_rel_ext_def gen_g_impl_rel_ext_def
apply (auto simp: fun_set_rel_def br_def list_set_rel_def id_slg_rel_alt_a ahm_ld_def)
apply (auto simp: rev_well_formed_pn_def Graph.E_def pnet_α_def o_def ahm_correct)
done
schematic_lemma reachable_impl:
assumes [simp]: "finite ((g_E G)⇧* `` g_V0 G)" "graph G"
assumes [autoref_rules]: "(Gi,G)∈⟨unit_rel,nat_rel⟩g_impl_rel_ext"
shows "RETURN (?c::?'c) ≤ \<Down>?R (RETURN (op_reachable G))"
by autoref_monadic
concrete_definition reachable_impl uses reachable_impl
thm reachable_impl.refine
term reachable_impl term pn_V'
term "⟨nat_rel⟩dflt_ahs_rel"
term ahs.rel
context begin
interpretation autoref_syn .
schematic_lemma sets_eq_impl:
fixes a b :: "nat set"
assumes [autoref_rules]: "(ai,a) ∈ ⟨nat_rel⟩ahs.rel"
assumes [autoref_rules]: "(bi,b) ∈ ⟨nat_rel⟩dflt_ahs_rel"
shows "(?c, (a ::: ⟨nat_rel⟩ahs.rel) = (b ::: ⟨nat_rel⟩dflt_ahs_rel )) ∈ bool_rel"
apply (autoref (keep_goal) )
done
concrete_definition sets_eq_impl uses sets_eq_impl
end
definition "net_α ≡ (λ(ci, adjmapi) .
((the_default 0 o (ahm.α ci)), (the_default [] o (ahm.α adjmapi))))"
lemma [code]: "net_α (ci, adjmapi) = (
cap_lookup ci, succ_lookup adjmapi
)"
unfolding net_α_def by (auto split: option.splits simp: ahm.correct ahm_ld_def)
definition "checkNet3 cc s t ≡ do {
if s = t then
RETURN None
else do {
let rd = read' cc s t;
case rd of
None => RETURN None
| Some x => do {
if pn_s_node' x ∧ pn_t_node' x then
do {
ASSERT(finite ((Graph.E (pn_c (pnet_α x)))⇧* `` {s}));
ASSERT(finite (((Graph.E (pn_c (pnet_α x)))¯)⇧* `` {t}));
ASSERT(∀u. set ((pn_succ (pnet_α x)) u) =
Graph.E (pn_c (pnet_α x)) `` {u} ∧ distinct ((pn_succ (pnet_α x)) u));
ASSERT(∀u. set ((pn_pred (pnet_α x)) u) =
(Graph.E (pn_c (pnet_α x)))¯ `` {u} ∧ distinct ((pn_pred (pnet_α x)) u));
let succ_s = (reachable_impl (graph_of_impl x s));
let pred_t = (reachable_impl (rev_graph_of_impl x t));
if (sets_eq_impl (pn_V' x) succ_s) ∧ (sets_eq_impl (pn_V' x) pred_t) then
RETURN (Some (net_α (pn_c' x, pn_adjmap' x)))
else
RETURN None
}
else
RETURN None
}
}
}"
thm reachable_impl.refine
term map2set_rel
thm sets_eq_impl.refine[simplified]
lemma aux1: "(x', x) ∈ pnet_rel ==> (pn_V' x', pn_V x) ∈ br ahs.α ahs.invar"
unfolding pnet_rel_def br_def pnet_α_def by auto
lemma [simp]: "graph (graph_of pn s)"
apply unfold_locales
unfolding graph_of_def
by auto
lemma [simp]: "graph (rev_graph_of pn s)"
apply unfold_locales
unfolding rev_graph_of_def
by auto
context begin
private lemma sets_eq_impl_correct_aux1:
assumes A: "(pn', pn) ∈ pnet_rel"
assumes WF: "well_formed_pn pn"
assumes F: "finite ((Graph.E (pn_c (pnet_α pn')))⇧* `` {s})"
shows "sets_eq_impl (pn_V' pn') (reachable_impl (graph_of_impl pn' s))
<-> pn_V pn = (g_E (graph_of pn s))⇧* `` g_V0 (graph_of pn s)"
proof -
from A have S1i: "(pn_V' pn', pn_V pn) ∈ br ahs.α ahs.invar"
unfolding pnet_rel_def br_def pnet_α_def by auto
note GI = graph_of_impl_correct[OF WF A]
have G: "graph (graph_of pn s)" by simp
have F': "finite ((g_E (graph_of pn s))⇧* `` g_V0 (graph_of pn s))"
using F A by (simp add: graph_of_def pnet_α_def pnet_rel_def br_def)
note S2i = reachable_impl.refine[simplified, OF F' G GI]
from sets_eq_impl.refine[simplified, OF S1i S2i] show ?thesis .
qed
private lemma sets_eq_impl_correct_aux2:
assumes A: "(pn', pn) ∈ pnet_rel"
assumes WF: "rev_well_formed_pn pn"
assumes F: "finite (((Graph.E (pn_c (pnet_α pn')))¯)⇧* `` {s})"
shows "sets_eq_impl (pn_V' pn') (reachable_impl (rev_graph_of_impl pn' s))
<-> pn_V pn = (g_E (rev_graph_of pn s))⇧* `` g_V0 (rev_graph_of pn s)"
proof -
from A have S1i: "(pn_V' pn', pn_V pn) ∈ br ahs.α ahs.invar"
unfolding pnet_rel_def br_def pnet_α_def by auto
note GI = rev_graph_of_impl_correct[OF WF A]
have G: "graph (rev_graph_of pn s)" by simp
have F': "finite ((g_E (rev_graph_of pn s))⇧* `` g_V0 (rev_graph_of pn s))"
using F A by (simp add: rev_graph_of_def pnet_α_def pnet_rel_def br_def)
note S2i = reachable_impl.refine[simplified, OF F' G GI]
from sets_eq_impl.refine[simplified, OF S1i S2i] show ?thesis .
qed
lemma checkNet3_correct: "checkNet3 el s t ≤ checkNet2 el s t"
unfolding checkNet3_def checkNet2_def
apply (rule refine_IdD)
apply (refine_rcg)
apply clarsimp_all
apply (rule introR[where R="⟨pnet_rel⟩option_rel"])
apply (simp add: read'_correct_alt; fail)
apply ((simp add: pnet_rel_def br_def pnet_α_def)+) [7]
apply (subst sets_eq_impl_correct_aux1; assumption?)
apply (simp add: well_formed_pn_def)
apply (subst sets_eq_impl_correct_aux2; assumption?)
apply (simp add: rev_well_formed_pn_def)
apply simp
apply (simp add: net_α_def o_def pnet_α_def pnet_rel_def br_def)
done
end
schematic_lemma checkNet4: "RETURN ?c ≤ checkNet3 el s t"
unfolding checkNet3_def
by (refine_transfer)
concrete_definition checkNet4 for el s t uses checkNet4
lemma checkNet4_correct: "case checkNet4 el s t of
Some (c, adjmap) => (el, c) ∈ ln_rel ∧ Network c s t ∧ Graph.is_adj_map c adjmap
| None => ¬ln_invar el ∨ ¬Network (ln_α el) s t"
proof -
note checkNet4.refine
also note checkNet3_correct
also note checkNet2_correct
also note checkNet_correct
finally show ?thesis by simp
qed
definition prepareNet :: "edge_list => node => node => (capacity_impl graph × (node=>node list) × nat) option"
where
"prepareNet el s t ≡ do {
(c,adjmap) \<leftarrow> checkNet4 el s t;
let N = ln_N el;
Some (c,adjmap,N)
}"
export_code prepareNet checking SML
lemma prepareNet_correct: "case (prepareNet el s t) of
Some (c, adjmap,N) => (el, c) ∈ ln_rel ∧ Network c s t ∧ Graph.is_adj_map c adjmap ∧ Graph.V c ⊆ {0..<N}
| None => ¬ln_invar el ∨ ¬Network (ln_α el) s t"
using checkNet4_correct[of el s t] ln_N_correct[of el]
unfolding prepareNet_def
by (auto split: Option.bind_split simp: ln_rel_def br_def)
end