Theory Simple_Network_Language_Impl_Refine
theory Simple_Network_Language_Impl_Refine
imports Simple_Network_Language_Impl
begin
unbundle no_library_syntax
notation fun_rel_syn (infixr "→" 60)
hide_const (open) upd
paragraph ‹Expression evaluation›
fun bval :: "('a ⇒ 'b) ⇒ ('a, 'b :: linorder) bexp ⇒ bool" and eval where
"bval _ bexp.true ⟷ True" |
"bval s (not e) ⟷ ¬ bval s e" |
"bval s (and e1 e2) ⟷ bval s e1 ∧ bval s e2" |
"bval s (bexp.or e1 e2) ⟷ bval s e1 ∨ bval s e2" |
"bval s (imply e1 e2) ⟷ bval s e1 ⟶ bval s e2" |
"bval s (eq i x) ⟷ eval s i = eval s x" |
"bval s (le i x) ⟷ eval s i ≤ eval s x" |
"bval s (lt i x) ⟷ eval s i < eval s x" |
"bval s (ge i x) ⟷ eval s i ≥ eval s x" |
"bval s (gt i x) ⟷ eval s i > eval s x"
| "eval s (const c) = c"
| "eval s (var x) = s x"
| "eval s (if_then_else b e1 e2) = (if bval s b then eval s e1 else eval s e2)"
| "eval s (binop f e1 e2) = f (eval s e1) (eval s e2)"
| "eval s (unop f e) = f (eval s e)"
lemma check_bexp_determ:
"check_bexp s b b1 ⟹ check_bexp s b b2 ⟹ b1 = b2"
and is_val_determ: "is_val s e v1 ⟹ is_val s e v2 ⟹ v1 = v2"
by (induction b and e arbitrary: b1 b2 and v1 v2)
(auto dest: elim!: is_val_elims check_bexp_elims)+
lemma is_upd_determ:
"s1 = s2" if "is_upd s f s1" "is_upd s f s2"
using that unfolding is_upd_def
by (clarsimp, fo_rule arg_cong)
(smt
case_prodE case_prodE' case_prod_conv is_val_determ list.rel_eq list_all2_swap list_all2_trans
)
lemma is_upds_determ:
"s1 = s2" if "is_upds s fs s1" "is_upds s fs s2"
using that
by (induction fs arbitrary: s) (auto 4 4 elim: is_upds.cases dest: is_upd_determ)
lemma check_bexp_bval:
"∀x ∈ vars_of_bexp b. x ∈ dom s ⟹ check_bexp s b (bval (the o s) b)"
and is_val_eval:
"∀x ∈ vars_of_exp e. x ∈ dom s ⟹ is_val s e (eval (the o s) e)"
apply (induction b and e)
apply (simp; (subst eq_commute)?; rule check_bexp_is_val.intros; simp add: dom_def)+
apply ((subst eq_commute eval.simps)?; rule check_bexp_is_val.intros; simp add: dom_def)+
done
lemma is_upd_dom:
"dom s' = dom s" if "is_upd s (x, e) s'" "x ∈ dom s"
using that unfolding is_upd_def by (auto split: if_split_asm)
lemma is_upds_dom:
"dom s' = dom s" if "is_upds s upds s'" "∀(x, e) ∈ set upds. x ∈ dom s"
using that
by (induction upds arbitrary: s)
(erule is_upds.cases; auto simp: is_upd_dom split: prod.split_asm)+
definition
"mk_upd ≡ λ(x, e) s. s(x ↦ eval (the o s) e)"
definition mk_upds ::
"('a ⇒ ('b :: linorder) option) ⇒ ('a × ('a, 'b) exp) list ⇒ ('a ⇒ 'b option)" where
"mk_upds s upds = fold mk_upd upds s"
lemma is_upd_make_updI:
"is_upd s upd (mk_upd upd s)" if "upd = (x, e)" "∀x ∈ vars_of_exp e. x ∈ dom s"
using that(1) is_val_eval[OF that(2)] unfolding is_upd_def mk_upd_def by auto
lemma dom_mk_upd:
"dom s ⊆ dom (mk_upd upd s)"
unfolding mk_upd_def by (auto split: prod.split)
lemma is_upds_make_updsI:
"is_upds s upds (mk_upds s upds)" if "∀ (_, e) ∈ set upds. ∀x ∈ vars_of_exp e. x ∈ dom s"
using that
proof (induction upds arbitrary: s)
case Nil
then show ?case
by (auto intro!: is_upds.intros simp: mk_upds_def)
next
case (Cons upd upds)
let ?s = "mk_upd upd s"
from Cons(2) have "is_upd s upd ?s"
by (auto simp: dom_def intro: is_upd_make_updI)
moreover have "is_upds ?s upds (mk_upds ?s upds)"
using Cons.prems dom_mk_upd by (intro Cons.IH) force
ultimately show ?case
using dom_mk_upd by (auto intro!: is_upds.intros simp: mk_upds_def)
qed
paragraph ‹Implementation auxiliaries›
definition
"union_map_of xs =
fold (λ (x, y) m. case m x of None ⇒ m(x ↦ [y]) | Some ys ⇒ m(x ↦ y # ys)) xs Map.empty"
lemma union_map_of_alt_def:
"union_map_of xs x = (let
ys = rev (map snd (filter (λ (x', y). x' = x) xs))
in if ys = [] then None else Some ys)"
proof -
have "fold (λ (x, y) m. case m x of None ⇒ m(x ↦ [y]) | Some ys ⇒ m(x ↦ y # ys)) xs m x
= (let
ys = rev (map snd (filter (λ (x', y). x' = x) xs))
in
case m x of None ⇒ if ys = [] then None else Some ys | Some zs ⇒ Some (ys @ zs))" for x m
by (induction xs arbitrary: m; clarsimp split: option.split)
then show ?thesis
unfolding union_map_of_def by simp
qed
lemma in_union_map_ofI:
"∃ ys. union_map_of xs x = Some ys ∧ y ∈ set ys" if "(x, y) ∈ set xs"
unfolding union_map_of_alt_def Let_def using that set_filter[of "λ(x', y). x' = x" xs] by auto+
lemma in_union_map_ofD:
"(x, y) ∈ set xs" if "union_map_of xs x = Some ys" "y ∈ set ys"
using that unfolding union_map_of_alt_def by (auto split: if_split_asm)
paragraph ‹Implementation of state set›
context Simple_Network_Impl_nat_defs
begin
definition
"states_i i = (⋃(l, e, g, a, r, u, l')∈set (fst (snd (snd (automata ! i)))). {l, l'})"
lemma states_mem_compute[code]:
"L ∈ states ⟷ length L = n_ps ∧ (∀i<n_ps. L ! i ∈ states_i i)"
unfolding states_def states_i_def by simp (metis mem_trans_N_iff)
lemma states_mem_compute':
"L ∈ states ⟷ length L = n_ps ∧ (∀i<n_ps. L ! i ∈ map states_i [0..<n_ps] ! i)"
unfolding states_mem_compute by simp
end
context Simple_Network_Impl_nat
begin
paragraph ‹Fundamentals›
lemma mem_trans_N_iff:
‹t ∈ Simple_Network_Language.trans (N i) ⟷ t ∈ set (fst (snd (snd (automata ! i))))›
if "i < n_ps"
unfolding N_def fst_conv snd_conv
unfolding automaton_of_def
unfolding trans_def
using that by (cases "automata ! i") (auto simp: length_automata_eq_n_ps)
lemma L_i_len:
‹L ! i < num_states i› if "i < n_ps" "L ∈ states"
using trans_num_states that
unfolding states_def by (auto 4 4 simp: mem_trans_N_iff)
lemma L_i_simp:
‹[0..<num_states i] ! (L ! i) = L ! i›
if "i < n_ps" "L ∈ states"
using L_i_len[OF that] by simp
lemma action_setD:
‹pred_act (λa'. a' < num_actions) a›
if ‹(l, b, g, a, f, r, l') ∈ Simple_Network_Language.trans (N p)› ‹p < n_ps›
using that action_set
by (cases "automata ! p")
(subst (asm) mem_trans_N_iff; force dest!: nth_mem simp flip: length_automata_eq_n_ps)
paragraph ‹More precise state sets›
definition
"states' ≡ {(L, s). L ∈ states ∧ dom s = {0..<n_vs} ∧ bounded bounds s}"
lemma states'_states[intro, dest]:
"L ∈ states" if "(L, s) ∈ states'"
using that unfolding states'_def by auto
lemma states'_dom[intro, dest]:
"dom s = {0..<n_vs}" if "(L, s) ∈ states'"
using that unfolding states'_def by auto
lemma states'_bounded[intro, dest]:
"bounded bounds s" if "(L, s) ∈ states'"
using that unfolding states'_def by auto
paragraph ‹Implementation of invariants›
definition (in Simple_Network_Impl_nat_defs)
"invs i ≡ let m = default_map_of [] (snd (snd (snd (automata ! i))));
m' = map (λ j. m j) [0..<num_states i]
in m'"
definition (in Simple_Network_Impl_nat_defs)
"invs1 ≡ map (λ i. let m = default_map_of [] (snd (snd (snd (automata ! i))));
m' = map (λ j. m j) [0..<num_states i]
in m') [0..<n_ps]"
definition (in Simple_Network_Impl_nat_defs)
"invs2 ≡ IArray (map (λ i. let m = default_map_of [] (snd (snd (snd (automata ! i))));
m' = IArray (map (λ j. m j) [0..<num_states i])
in m') [0..<n_ps])"
lemma refine_invs2:
"invs2 !! i !! j = invs1 ! i ! j" if "i < n_ps"
using that unfolding invs2_def invs1_def by simp
definition (in Simple_Network_Impl_nat_defs)
"inv_fun ≡ λ(L, _).
concat (map (λi. invs1 ! i ! (L ! i)) [0..<n_ps])"
lemma refine_invs1:
‹invs1 ! i = invs i› if ‹i < n_ps›
using that unfolding invs_def invs1_def by simp
lemma invs_simp:
"invs1 ! i ! (L ! i) = Simple_Network_Language.inv (N i) (L ! i)"
if "i < n_ps" "L ∈ states"
using that unfolding refine_invs1[OF ‹i < _›] invs_def N_def fst_conv snd_conv
unfolding inv_def
by (subst nth_map;
clarsimp split: prod.split simp: automaton_of_def length_automata_eq_n_ps L_i_len)
lemma inv_fun_inv_of':
"(inv_fun, inv_of prod_ta) ∈ inv_rel R states'" if "R ⊆ Id ×⇩r S"
using that
unfolding inv_rel_def
unfolding inv_fun_def
unfolding inv_of_prod prod_inv_def
apply (clarsimp simp: states'_def)
apply (rule arg_cong[where f = concat])
apply (auto simp add: invs_simp cong: map_cong)
done
lemma inv_fun_alt_def:
"inv_fun = (λ(L, _). concat (map (λi. invs2 !! i !! (L ! i)) [0..<n_ps]))"
unfolding inv_fun_def
apply (intro ext)
apply (clarsimp simp del: IArray.sub_def)
apply (fo_rule arg_cong)
apply (simp add: refine_invs2 del: IArray.sub_def)
done
end
paragraph ‹Implementation of transitions›
context Simple_Network_Impl_nat_defs
begin
definition
"bounds_map ≡ the o map_of bounds'"
definition
"check_bounded s =
(∀x ∈ dom s. fst (bounds_map x) ≤ the (s x) ∧ the (s x) ≤ snd (bounds_map x))"
text ‹Compute pairs of processes with committed initial locations from location vector.›
definition
"get_committed L =
List.map_filter (λp.
let l = L ! p in
if l ∈ set (fst (automata ! p)) then Some (p, l) else None) [0..<n_ps]"
text ‹Given a process and a location, return the corresponding transitions.›
definition
"trans_map i ≡
let m = union_map_of (fst (snd (snd (automata ! i)))) in (λj.
case m j of None ⇒ [] | Some xs ⇒ xs)"
text ‹Filter for internal transitions.›
definition
"trans_i_map i j ≡
List.map_filter
(λ (b, g, a, m, l'). case a of Sil a ⇒ Some (b, g, a, m, l') | _ ⇒ None)
(trans_map i j)"
text ‹Compute valid internal successors given:
▪ a process ‹p›,
▪ initial location ‹l›,
▪ location vector ‹L›,
▪ and initial state ‹s›.
›
definition
"int_trans_from_loc p l L s ≡
let trans = trans_i_map p l
in
List.map_filter (λ (b, g, a, f, r, l').
let s' = mk_upds s f in
if bval (the o s) b ∧ check_bounded s' then Some (g, Internal a, r, (L[p := l'], s'))
else None
) trans"
definition
"int_trans_from_vec pairs L s ≡
concat (map (λ(p, l). int_trans_from_loc p l L s) pairs)"
definition
"int_trans_from_all L s ≡
concat (map (λp. int_trans_from_loc p (L ! p) L s) [0..<n_ps])"
definition
"int_trans_from ≡ λ (L, s).
let pairs = get_committed L in
if pairs = []
then int_trans_from_all L s
else int_trans_from_vec pairs L s
"
definition
"actions_by_state i ≡
fold (λ t acc. acc[fst (snd (snd t)) := (i, t) # (acc ! fst (snd (snd t)))])"
definition
"all_actions_by_state t L ≡
fold (λ i. actions_by_state i (t i (L ! i))) [0..<n_ps] (repeat [] num_actions)"
definition
"all_actions_from_vec t vec ≡
fold (λ(p, l). actions_by_state p (t p l)) vec (repeat [] num_actions)"
definition
"pairs_by_action L s OUT IN ≡
concat (
map (λ (p, b1, g1, a1, f1, r1, l1).
List.map_filter (λ (q, b2, g2, a2, f2, r2, l2).
if p = q then None else
let s' = mk_upds (mk_upds s f1) f2 in
if bval (the o s) b1 ∧ bval (the o s) b2 ∧ check_bounded s'
then Some (g1 @ g2, Bin a1, r1 @ r2, (L[p := l1, q := l2], s'))
else None
) OUT) IN)
"
definition
"trans_in_map i j ≡
List.map_filter
(λ (b, g, a, m, l'). case a of In a ⇒ Some (b, g, a, m, l') | _ ⇒ None)
(trans_map i j)"
definition
"trans_out_map i j ≡
List.map_filter
(λ (b, g, a, m, l'). case a of Out a ⇒ Some (b, g, a, m, l') | _ ⇒ None)
(trans_map i j)"
definition
"bin_actions = filter (λa. a ∉ set broadcast) [0..<num_actions]"
lemma mem_bin_actions_iff:
"a ∈ set bin_actions ⟷ a ∉ local.broadcast ∧ a < num_actions "
unfolding bin_actions_def broadcast_def by auto
definition
"bin_trans_from ≡ λ(L, s).
let
pairs = get_committed L;
In = all_actions_by_state trans_in_map L;
Out = all_actions_by_state trans_out_map L
in
if pairs = [] then
concat (map (λa. pairs_by_action L s (Out ! a) (In ! a)) bin_actions)
else
let
In2 = all_actions_from_vec trans_in_map pairs;
Out2 = all_actions_from_vec trans_out_map pairs
in
concat (map (λa. pairs_by_action L s (Out ! a) (In2 ! a)) bin_actions)
@ concat (map (λa. pairs_by_action L s (Out2 ! a) (In ! a)) bin_actions)
"
definition
"trans_in_broad_map i j ≡
List.map_filter
(λ (b, g, a, m, l').
case a of In a ⇒ if a ∈ set broadcast then Some (b, g, a, m, l') else None | _ ⇒ None)
(trans_map i j)"
definition
"trans_out_broad_map i j ≡
List.map_filter
(λ (b, g, a, m, l').
case a of Out a ⇒ if a ∈ set broadcast then Some (b, g, a, m, l') else None | _ ⇒ None)
(trans_map i j)"
definition
"actions_by_state' xs ≡
fold (λ t acc. acc[fst (snd (snd t)) := t # (acc ! fst (snd (snd t)))])
xs (repeat [] num_actions)"
definition
"trans_out_broad_grouped i j ≡ actions_by_state' (trans_out_broad_map i j)"
definition
"trans_in_broad_grouped i j ≡ actions_by_state' (trans_in_broad_map i j)"
definition
"pair_by_action OUT IN ≡
concat (
map (λ(g1, a, r1, (L, s)).
List.map (λ(q, g2, a2, f2, r2, l2).
(g1 @ g2, a, r1 @ r2, (L[q := l2], mk_upds s f2))
) OUT) IN)
"
definition make_combs where
"make_combs p a xs ≡
let
ys = List.map_filter
(λi.
if i = p then None
else if xs ! i ! a = [] then None
else Some (map (λt. (i, t)) (xs ! i ! a))
)
[0..<n_ps]
in if ys = [] then [] else product_lists ys
"
definition make_combs_from_pairs where
"make_combs_from_pairs p a pairs xs ≡
let
ys = List.map_filter
(λi.
if i = p then None
else if xs ! i ! a = [] then None
else Some (map (λt. (i, t)) (xs ! i ! a))
)
[0..<n_ps]
in if ys = [] then [] else product_lists ys
"
definition
"broad_trans_from ≡ λ(L, s).
let
pairs = get_committed L;
In = map (λp. trans_in_broad_grouped p (L ! p)) [0..<n_ps];
Out = map (λp. trans_out_broad_grouped p (L ! p)) [0..<n_ps];
In = map (map (filter (λ (b, _). bval (the o s) b))) In;
Out = map (map (filter (λ (b, _). bval (the o s) b))) Out
in
if pairs = [] then
concat (
map (λa.
concat (map (λp.
let
outs = Out ! p ! a
in if outs = [] then []
else
let
combs = make_combs p a In;
outs = map (λt. (p, t)) outs;
combs = (
if combs = [] then [[x]. x ← outs]
else concat (map (λx. map (λxs. x # xs) combs) outs));
init = ([], Broad a, [], (L, s))
in
List.map_filter (λcomb.
let (g, a, r, L', s) =
fold
(λ(q, _, g2, a2, f2, r2, l2) (g1, a, r1, (L, s)).
(g1 @ g2, a, r1 @ r2, (L[q := l2], mk_upds s f2))
)
comb
init
in if check_bounded s then Some (g, a, r, L', s) else None
) combs
)
[0..<n_ps])
)
[0..<num_actions])
else
concat (
map (λa.
let
ins_committed =
List.map_filter (λ(p, _). if In ! p ! a ≠ [] then Some p else None) pairs;
always_committed = (length ins_committed > 1)
in
concat (map (λp.
let
outs = Out ! p ! a
in if outs = [] then []
else if
¬ always_committed ∧ (ins_committed = [p] ∨ ins_committed = [])
∧ ¬ list_ex (λ (q, _). q = p) pairs
then []
else
let
combs = make_combs p a In;
outs = map (λt. (p, t)) outs;
combs = (
if combs = [] then [[x]. x ← outs]
else concat (map (λx. map (λxs. x # xs) combs) outs));
init = ([], Broad a, [], (L, s))
in
List.map_filter (λcomb.
let (g, a, r, L', s) =
fold
(λ(q, _, g2, a2, f2, r2, l2) (g1, a, r1, (L, s)).
(g1 @ g2, a, r1 @ r2, (L[q := l2], mk_upds s f2))
)
comb
init
in if check_bounded s then Some (g, a, r, L', s) else None
) combs
)
[0..<n_ps])
)
[0..<num_actions])
"
end
lemma product_lists_empty: "product_lists xss = [] ⟷ (∃xs ∈ set xss. xs = [])" for xss
by (induction xss) auto
context Simple_Network_Impl_nat
begin
lemma broad_trans_from_alt_def:
"broad_trans_from ≡ λ(L, s).
let
pairs = get_committed L;
In = map (λp. trans_in_broad_grouped p (L ! p)) [0..<n_ps];
Out = map (λp. trans_out_broad_grouped p (L ! p)) [0..<n_ps];
In = map (map (filter (λ (b, _). bval (the o s) b))) In;
Out = map (map (filter (λ (b, _). bval (the o s) b))) Out
in
if pairs = [] then
concat (
map (λa.
concat (map (λp.
let
outs = Out ! p ! a
in if outs = [] then []
else
let
combs = make_combs p a In;
outs = map (λt. (p, t)) outs;
combs = (
if combs = [] then [[x]. x ← outs]
else concat (map (λx. map (λxs. x # xs) combs) outs));
init = ([], Broad a, [], (L, s))
in
filter (λ (g, a, r, L, s). check_bounded s) (
map (λcomb.
fold
(λ(q, _, g2, a2, f2, r2, l2) (g1, a, r1, (L, s)).
(g1 @ g2, a, r1 @ r2, (L[q := l2], mk_upds s f2))
)
comb
init
) combs)
)
[0..<n_ps])
)
[0..<num_actions])
else
concat (
map (λa.
let
ins_committed =
List.map_filter (λ(p, _). if In ! p ! a ≠ [] then Some p else None) pairs
in
concat (map (λp.
let
outs = Out ! p ! a
in if outs = [] then []
else if
(ins_committed = [p] ∨ ins_committed = []) ∧ ¬ list_ex (λ(q, _). q = p) pairs
then []
else
let
combs = make_combs p a In;
outs = map (λt. (p, t)) outs;
combs = (
if combs = [] then [[x]. x ← outs]
else concat (map (λx. map (λxs. x # xs) combs) outs));
init = ([], Broad a, [], (L, s))
in
filter (λ (g, a, r, L, s). check_bounded s) (
map (λcomb.
fold
(λ(q, _, g2, a2, f2, r2, l2) (g1, a, r1, (L, s)).
(g1 @ g2, a, r1 @ r2, (L[q := l2], mk_upds s f2))
)
comb
init
) combs)
)
[0..<n_ps])
)
[0..<num_actions])
"
apply (rule eq_reflection)
unfolding broad_trans_from_def
unfolding filter_map_map_filter
unfolding Let_def
by (fo_rule
arg_cong2[where f = map] arg_cong2[where f = List.map_filter] arg_cong HOL.refl |
rule if_cong ext | auto split: if_split_asm)+
paragraph ‹Correctness for implementations of primitives›
lemma dom_bounds_eq:
"dom bounds = {0..<n_vs}"
using bounds unfolding bounds_def
apply simp
unfolding n_vs_def dom_map_of_conv_image_fst
apply safe
apply (force dest: mem_nth; fail)
apply (force dest: nth_mem; fail)
done
lemma check_bounded_iff:
"Simple_Network_Language.bounded bounds s ⟷ check_bounded s" if "dom s = {0..<n_vs}"
using that
unfolding dom_bounds_eq[symmetric]
unfolding check_bounded_def Simple_Network_Language.bounded_def bounds_map_def bounds_def
by auto
lemma get_committed_mem_iff:
"(p, l) ∈ set (get_committed L) ⟷ (l = L ! p ∧ l ∈ committed (N p) ∧ p < n_ps)"
unfolding get_committed_def
unfolding set_map_filter Let_def
apply clarsimp
unfolding N_def fst_conv snd_conv
unfolding committed_def
by safe
((subst nth_map | subst (asm) nth_map);
auto split: prod.splits simp: automaton_of_def length_automata_eq_n_ps
)+
lemma get_committed_empty_iff:
"(∀p < n_ps. L ! p ∉ committed (N p)) ⟷ get_committed L = []"
apply safe
subgoal
proof (rule ccontr)
assume prems:
"∀p<n_ps. L ! p ∉ committed (N p)" and
"get_committed L ≠ []"
then obtain p l where "(p, l) ∈ set (get_committed L)"
by (metis length_greater_0_conv nth_mem old.prod.exhaust)
from this[unfolded get_committed_mem_iff] prems(1)
show "False"
by auto
qed
subgoal for p
using get_committed_mem_iff[of p "L ! p" L] by auto
done
lemma get_committed_distinct: "distinct (get_committed L)"
unfolding get_committed_def by (rule distinct_map_filterI) (auto simp: Let_def)
lemma is_upds_make_updsI2:
"is_upds s upds (mk_upds s upds)"
if "(l, b, g, a, upds, r, l') ∈ Simple_Network_Language.trans (N p)" "p < n_ps"
"dom s = {0..<n_vs}"
using that var_set
by (intro is_upds_make_updsI, subst (asm) mem_trans_N_iff)
(auto 4 5 simp flip: length_automata_eq_n_ps dest!: nth_mem)
lemma var_setD:
"∀(x, upd)∈set f. x < n_vs ∧ (∀i∈vars_of_exp upd. i < n_vs)"
if "(l, b, g, a, f, r, l') ∈ Simple_Network_Language.trans (N p)" "p < n_ps"
using var_set that
by (force dest: nth_mem simp flip: length_automata_eq_n_ps simp: mem_trans_N_iff)+
lemma var_setD2:
"∀i∈vars_of_bexp b. i < n_vs"
if "(l, b, g, a, f, r, l') ∈ Simple_Network_Language.trans (N p)" "p < n_ps"
using var_set that
by (force dest: nth_mem simp flip: length_automata_eq_n_ps simp: mem_trans_N_iff)+
lemma is_upds_dom2:
"dom s' = {0..<n_vs}" if "is_upds s f s'"
"(l, b, g, a, f, r, l') ∈ Simple_Network_Language.trans (N p)" "p < n_ps"
"dom s = {0..<n_vs}"
unfolding that(4)[symmetric] using that by - (drule (1) var_setD, erule is_upds_dom, auto)
lemma is_updsD:
"s' = mk_upds s f" if "is_upds s f s'"
"(l, b, g, a, f, r, l') ∈ Simple_Network_Language.trans (N p)" "p < n_ps"
"dom s = {0..<n_vs}"
proof -
from is_upds_make_updsI2[OF that(2-)] have "is_upds s f (mk_upds s f)" .
from is_upds_determ[OF that(1) this] show ?thesis .
qed
lemma is_upds_make_upds_concatI2:
"is_upds s (concat upds) (mk_upds s (concat upds))"
if "dom s = {0..<n_vs}"
"∀upd ∈ set upds. ∃p < n_ps. ∃l b g a r l'.
(l, b, g, a, upd, r, l') ∈ Simple_Network_Language.trans (N p)"
using that var_set
by (intro is_upds_make_updsI, clarsimp)
(smt (z3) atLeastLessThan_iff case_prod_conv domD var_setD zero_le)
lemma is_upds_concat_dom2:
assumes "is_upds s (concat upds) s'"
and "∀f ∈ set upds. ∃ p < n_ps. ∃ l b g a r l'.
(l, b, g, a, f, r, l') ∈ Simple_Network_Language.trans (N p)"
and "dom s = {0..<n_vs}"
shows "dom s' = dom s"
using assms by (elim is_upds_dom) (auto dest!: var_setD)
lemma is_upds_dom3:
assumes "is_upds s (concat_map fs ps) s'"
and "∀p∈set ps. (L ! p, bs p, gs p, a, fs p, rs p, ls' p) ∈ trans (N p)"
and "set ps ⊆ {0..<n_ps}"
and "dom s = {0..<n_vs}"
shows "dom s' = dom s"
using assms by (elim is_upds_concat_dom2; force)
lemma is_upds_make_updsI3:
"is_upds s (concat_map fs ps) (mk_upds s (concat_map fs ps))"
if "dom s = {0..<n_vs}"
and "∀p∈set ps. (L ! p, bs p, gs p, a, fs p, rs p, ls' p) ∈ trans (N p)"
and "set ps ⊆ {0..<n_ps}"
for s :: "nat ⇒ int option"
using that by (elim is_upds_make_upds_concatI2) force
lemma is_upds_concatD:
assumes
"dom s = {0..<n_vs}" and
"∀p∈set ps.
(ls p, bs p, gs p, a, fs p, rs p, ls' p)
∈ Simple_Network_Language.trans (N p)" and
"set ps ⊆ {0..<n_ps}" and
"is_upds s (concat_map fs ps) s'"
shows "s' = mk_upds s (concat_map fs ps)"
proof -
let ?upds = "concat_map fs ps"
have "is_upds s ?upds (mk_upds s ?upds)"
using assms(1-3) by (intro is_upds_make_upds_concatI2; force)
from is_upds_determ[OF assms(4) this] show ?thesis
by (simp add: fold_map comp_def)
qed
context
notes [simp] = length_automata_eq_n_ps
begin
lemma trans_mapI:
assumes
"(L ! p, g, a, f, r, l') ∈ Simple_Network_Language.trans (N p)"
"p < n_ps"
shows
"(g, a, f, r, l') ∈ set (trans_map p (L ! p))"
using assms unfolding trans_map_def N_def fst_conv snd_conv trans_def
by (subst (asm) nth_map) (auto dest: in_union_map_ofI split: prod.split_asm simp: automaton_of_def)
lemma trans_i_mapI:
assumes
"(L ! p, b, g, Sil a', f, r, l') ∈ Simple_Network_Language.trans (N p)"
"p < n_ps"
shows
"(b, g, a', f, r, l') ∈ set (trans_i_map p (L ! p))"
using assms unfolding trans_i_map_def set_map_filter by (fastforce dest: trans_mapI)
lemma trans_mapI':
assumes
"(l, b, g, a, f, r, l') ∈ Simple_Network_Language.trans (N p)"
"p < n_ps"
shows
"(b, g, a, f, r, l') ∈ set (trans_map p l)"
using assms unfolding trans_map_def N_def fst_conv snd_conv trans_def
by (subst (asm) nth_map) (auto dest: in_union_map_ofI split: prod.split_asm simp: automaton_of_def)
lemma trans_mapD:
assumes
"(b, g, a, f, r, l') ∈ set (trans_map p l)"
"p < n_ps"
shows
"(l, b, g, a, f, r, l') ∈ Simple_Network_Language.trans (N p)"
using assms unfolding trans_map_def N_def fst_conv snd_conv trans_def
by (subst nth_map) (auto split: prod.split elim: in_union_map_ofD[rotated] simp: automaton_of_def)
lemma trans_map_iff:
assumes
"p < n_ps"
shows
"(b, g, a, f, r, l') ∈ set (trans_map p l)
⟷ (l, b, g, a, f, r, l') ∈ Simple_Network_Language.trans (N p)"
using trans_mapD trans_mapI' ‹p < n_ps› by auto
lemma trans_i_mapD:
assumes
"(b, g, a', f, r, l') ∈ set (trans_i_map p (L ! p))"
"p < n_ps"
shows
"(L ! p, b, g, Sil a', f, r, l') ∈ Simple_Network_Language.trans (N p)"
using assms unfolding trans_i_map_def set_map_filter
by (force split: act.split_asm intro: trans_mapD)
paragraph ‹An additional brute force method for forward-chaining of facts›
method frules_all =
repeat_rotate ‹frules›, dedup_prems
paragraph ‹Internal transitions›
lemma get_committed_memI:
"(p, L ! p) ∈ set (get_committed L)" if "L ! p ∈ committed (N p)" "p < n_ps"
using that unfolding get_committed_mem_iff by simp
lemma check_bexp_bvalI:
"bval (the o s) b" if "check_bexp s b True"
"(l, b, g, a, f, r, l') ∈ Simple_Network_Language.trans (N p)" "p < n_ps"
"dom s = {0..<n_vs}"
proof -
from var_setD2[OF that(2,3)] ‹dom s = {0..<n_vs}› have "check_bexp s b (bval (the o s) b)"
by (intro check_bexp_bval, simp)
with check_bexp_determ that(1) show ?thesis
by auto
qed
lemma check_bexp_bvalD:
"check_bexp s b True" if "bval (the o s) b"
"(l, b, g, a, f, r, l') ∈ Simple_Network_Language.trans (N p)" "p < n_ps"
"dom s = {0..<n_vs}"
proof -
from var_setD2[OF that(2,3)] ‹dom s = {0..<n_vs}› have "check_bexp s b (bval (the o s) b)"
by (intro check_bexp_bval, simp)
with check_bexp_determ that(1) show ?thesis
by auto
qed
lemmas [forward2] =
trans_i_mapD
trans_i_mapI
get_committed_memI
lemmas [forward3] =
is_upds_make_updsI2
lemmas [forward4] =
is_updsD
is_upds_dom2
check_bexp_bvalI
check_bexp_bvalD
lemma int_trans_from_correct:
"(int_trans_from, trans_int) ∈ transition_rel states'"
unfolding transition_rel_def
proof (safe del: iffI)
note [more_elims] = allE
fix L s g a r L' s' assume "(L, s) ∈ states'"
then have "L ∈ states" "dom s = {0..<n_vs}" "bounded bounds s"
by auto
then have [simp]: "length L = n_ps" "check_bounded s"
by (auto simp: check_bounded_iff)
show "(((L, s), g, a, r, L', s') ∈ trans_int)
⟷ ((g, a, r, L', s') ∈ set (int_trans_from (L, s)))"
proof (cases "get_committed L = []")
case True
then have *: "((L, s), g, a, r, L', s') ∈ trans_int ⟷
((L, s), g, a, r, L', s') ∈ {((L, s), g, Internal a, r, (L', s')) | L s l b g f p a r l' L' s'.
(l, b, g, Sil a, f, r, l') ∈ trans (N p) ∧
(∀p < n_ps. L ! p ∉ committed (N p)) ∧
check_bexp s b True ∧
L!p = l ∧ p < length L ∧ L' = L[p := l'] ∧ is_upds s f s' ∧
L ∈ states ∧ bounded bounds s ∧ bounded bounds s'
}"
unfolding get_committed_empty_iff[symmetric] trans_int_def by blast
from True have **: "int_trans_from (L, s) = int_trans_from_all L s"
unfolding int_trans_from_def by simp
from ‹dom s = _› show ?thesis
unfolding * ** int_trans_from_all_def
apply clarsimp
unfolding int_trans_from_loc_def Let_def set_map_filter
apply clarsimp
apply safe
subgoal for b f p a' l'
apply frules
unfolding check_bounded_iff by (intros; solve_triv)
subgoal for p _ a' upds l'
apply simp
apply frules
using ‹L ∈ states› ‹check_bounded s› True[folded get_committed_empty_iff]
unfolding check_bounded_iff by (intros; solve_triv)
done
next
case False
then have *: "((L, s), g, a, r, L', s') ∈ trans_int ⟷
((L, s), g, a, r, L', s') ∈ {((L, s), g, Internal a, r, (L', s')) | L s l b g f p a r l' L' s'.
(l, b, g, Sil a, f, r, l') ∈ trans (N p) ∧
l ∈ committed (N p) ∧
L!p = l ∧ p < length L ∧ check_bexp s b True ∧ L' = L[p := l'] ∧ is_upds s f s' ∧
L ∈ states ∧ bounded bounds s ∧ bounded bounds s'
}"
unfolding get_committed_empty_iff[symmetric] trans_int_def by blast
from False have **: "int_trans_from (L, s) = int_trans_from_vec (get_committed L) L s"
unfolding int_trans_from_def by simp
from ‹dom s = _› ‹L ∈ states› show ?thesis
unfolding * ** int_trans_from_vec_def
apply clarsimp
unfolding int_trans_from_loc_def Let_def set_map_filter
apply clarsimp
apply safe
subgoal for f p a' l'
apply frules
unfolding check_bounded_iff by (intros; solve_triv)
subgoal for p _ a' upds l'
unfolding get_committed_mem_iff
apply (elims; simp)
apply frules
unfolding check_bounded_iff by (intros; solve_triv)
done
qed
qed
paragraph ‹Mostly copied›
lemma in_actions_by_stateI:
assumes
"(b1, g1, a, r1) ∈ set xs" "a < length acc"
shows
"(q, b1, g1, a, r1) ∈ set (actions_by_state q xs acc ! a)
∧ a < length (actions_by_state q xs acc)"
using assms unfolding actions_by_state_def
apply (induction xs arbitrary: acc)
apply (simp; fail)
apply simp
apply (erule disjE)
apply (rule fold_acc_preserv
[where P = "λ acc. (q, b1, g1, a, r1) ∈ set (acc ! a) ∧ a < length acc"]
)
apply (subst list_update_nth_split; auto)
by auto
lemma in_actions_by_state'I:
assumes
"(b1, g1, a, r1) ∈ set xs" "a < num_actions"
shows
"(b1, g1, a, r1) ∈ set (actions_by_state' xs ! a)
∧ a < length (actions_by_state' xs)"
proof -
let ?f = "(λt acc. acc[fst (snd (snd t)) := t # acc ! fst (snd (snd t))])"
have "(b1, g1, a, r1) ∈ set (fold ?f xs acc ! a)
∧ a < length (fold ?f xs acc)" if "a < length acc" for acc
using assms(1) that
apply (induction xs arbitrary: acc)
apply (simp; fail)
apply simp
apply (erule disjE)
apply (rule fold_acc_preserv
[where P = "λ acc. (b1, g1, a, r1) ∈ set (acc ! a) ∧ a < length acc"]
)
apply (subst list_update_nth_split; auto)
by auto
with ‹a < _› show ?thesis
unfolding actions_by_state'_def by simp
qed
lemma in_actions_by_state_preserv:
assumes
"(q, b1, g1, a, r1) ∈ set (acc ! a)" "a < length acc"
shows
"(q, b1, g1, a, r1) ∈ set (actions_by_state y xs acc ! a)
∧ a < length (actions_by_state y xs acc)"
using assms unfolding actions_by_state_def
apply -
apply (rule fold_acc_preserv
[where P = "λ acc. (q, b1, g1, a, r1) ∈ set (acc ! a) ∧ a < length acc"]
)
apply (subst list_update_nth_split; auto)
by auto
lemma length_actions_by_state_preserv[simp]:
shows "length (actions_by_state y xs acc) = length acc"
unfolding actions_by_state_def by (auto intro: fold_acc_preserv simp: list_update_nth_split)
lemma in_all_actions_by_stateI:
assumes
"a < num_actions" "q < n_ps" "(b1, g1, a, r1) ∈ set (M q (L ! q))"
shows
"(q, b1, g1, a, r1) ∈ set (all_actions_by_state M L ! a)"
unfolding all_actions_by_state_def
apply (rule fold_acc_ev_preserv
[where P = "λ acc. (q, b1, g1, a, r1) ∈ set (acc ! a)" and Q = "λ acc. a < length acc",
THEN conjunct1]
)
apply (rule in_actions_by_state_preserv[THEN conjunct1])
using assms by (auto intro: in_actions_by_stateI[THEN conjunct1])
lemma in_all_actions_from_vecI:
assumes
"a < num_actions" "(b1, g1, a, r1) ∈ set (M q l)" "(q, l) ∈ set pairs"
shows
"(q, b1, g1, a, r1) ∈ set (all_actions_from_vec M pairs ! a)"
unfolding all_actions_from_vec_def using assms
by (intro fold_acc_ev_preserv
[where P = "λ acc. (q, b1, g1, a, r1) ∈ set (acc ! a)" and Q = "λ acc. a < length acc",
THEN conjunct1])
(auto intro: in_actions_by_stateI[THEN conjunct1] in_actions_by_state_preserv[THEN conjunct1])
lemma actions_by_state_inj:
assumes "j < length acc"
shows "∀ (q, a) ∈ set (actions_by_state i xs acc ! j). (q, a) ∉ set (acc ! j) ⟶ i = q"
unfolding actions_by_state_def
apply (rule fold_acc_preserv
[where P =
"λ acc'. (∀ (q, a) ∈ set (acc' ! j). (q, a) ∉ set (acc ! j) ⟶ i = q) ∧ j < length acc'",
THEN conjunct1])
subgoal for x acc
by (cases "fst (snd (snd x)) = j"; simp)
using assms by auto
lemma actions_by_state_inj':
assumes "j < length acc" "(q, a) ∉ set (acc ! j)" "(q, a) ∈ set (actions_by_state i xs acc ! j)"
shows "i = q"
using actions_by_state_inj[OF assms(1)] assms(2-) by fast
lemma in_actions_by_stateD:
assumes
"(q, b, g, a, t) ∈ set (actions_by_state i xs acc ! j)" "(q, b, g, a, t) ∉ set (acc ! j)"
"j < length acc"
shows
"(b, g, a, t) ∈ set xs ∧ j = a"
using assms unfolding actions_by_state_def
apply -
apply (drule fold_evD
[where y = "(b, g, a, t)" and Q = "λ acc'. length acc' = length acc"
and R = "λ (_, _, a', t). a' = j"]
)
apply assumption
apply (subst (asm) list_update_nth_split[of j]; force)
apply simp+
apply (subst (asm) list_update_nth_split[of j]; force)
by auto
lemma in_actions_by_state'D:
assumes
"(b, g, a, r) ∈ set (actions_by_state' xs ! a')" "a' < num_actions"
shows
"(b, g, a, r) ∈ set xs ∧ a' = a"
proof -
let ?f = "(λt acc. acc[fst (snd (snd t)) := t # acc ! fst (snd (snd t))])"
have "(b, g, a, r) ∈ set xs ∧ a' = a"
if "(b, g, a, r) ∈ set (fold ?f xs acc ! a')" "(b, g, a, r) ∉ set (acc ! a')" "a' < length acc"
for acc
using that
apply -
apply (drule fold_evD
[where y = "(b, g, a, r)" and Q = "λ acc'. length acc' = length acc"
and R = "λ (_, _, a, t). a = a'"]
)
apply ((subst (asm) list_update_nth_split[where j = a'])?; solves auto)+
done
with assms show ?thesis
unfolding actions_by_state'_def by auto
qed
lemma in_all_actions_by_stateD:
assumes
"(q, b1, g1, a, r1) ∈ set (all_actions_by_state M L ! a')" "a' < num_actions"
shows
"(b1, g1, a, r1) ∈ set (M q (L ! q)) ∧ q < n_ps ∧ a' = a"
using assms
unfolding all_actions_by_state_def
apply -
apply (drule fold_evD''[where y = q and Q = "λ acc. length acc = num_actions"])
apply (simp; fail)
apply (drule actions_by_state_inj'[rotated])
apply (simp; fail)+
apply safe
apply (drule in_actions_by_stateD)
apply assumption
apply (rule fold_acc_preserv)
apply (simp; fail)+
subgoal premises prems
proof -
from prems(2) have "q ∈ set [0..<n_ps]" by auto
then show ?thesis by simp
qed
by (auto intro: fold_acc_preserv dest!: in_actions_by_stateD)
lemma length_all_actions_by_state_preserv:
"length (all_actions_by_state M L) = num_actions"
unfolding all_actions_by_state_def by (auto intro: fold_acc_preserv)
lemma length_actions_by_state'_preserv:
"length (actions_by_state' xs) = num_actions"
unfolding actions_by_state'_def by (rule fold_acc_preserv; simp)
lemma all_actions_from_vecD:
assumes
"(q, b1, g1, a, r1) ∈ set (all_actions_from_vec M pairs ! a')" "a' < num_actions"
"distinct (map fst pairs)"
shows
"∃ l. (q, l) ∈ set pairs ∧ (b1, g1, a, r1) ∈ set (M q l) ∧ a' = a"
using assms(1,2)
unfolding all_actions_from_vec_def
apply -
apply (drule fold_evD2'[where
y = "(q, SOME l. (q, l) ∈ set pairs)"
and Q = "λ acc. length acc = num_actions"])
apply (clarsimp; fail)
apply clarsimp
apply (drule actions_by_state_inj'[rotated])
apply assumption
apply assumption
apply simp
subgoal
using assms(3) by (meson distinct_map_fstD someI_ex)
apply (solves auto)+
apply clarsimp
apply (drule in_actions_by_stateD)
apply (simp; fail)
apply (rule fold_acc_preserv)
apply (solves auto)+
subgoal premises prems for ys zs
using prems(4) by (subst ‹pairs = _›) auto
done
lemma all_actions_from_vecD2:
assumes
"(q, b1, g1, a, r1) ∈ set (all_actions_from_vec M pairs ! a')" "a' < num_actions"
"(q, l) ∈ set pairs" "distinct (map fst pairs)"
shows
"(b1, g1, a, r1) ∈ set (M q l) ∧ a' = a"
using assms(1,2,3)
unfolding all_actions_from_vec_def
apply -
apply (drule fold_evD2'[where y = "(q, l)" and Q = "λ acc. length acc = num_actions"])
apply (clarsimp; fail)
apply clarsimp
apply (drule actions_by_state_inj'[rotated])
apply assumption
apply assumption
apply simp
subgoal
using assms(4) by (meson distinct_map_fstD)
by (auto intro: fold_acc_preserv dest!: in_actions_by_stateD)
paragraph ‹Binary transitions›
lemma bin_trans_from_correct:
"(bin_trans_from, trans_bin) ∈ transition_rel states'"
unfolding transition_rel_def
proof (safe del: iffI)
fix L s g a r L' s' assume "(L, s) ∈ states'"
then have "L ∈ states" "dom s = {0..<n_vs}" "bounded bounds s"
by auto
then have [simp]: "length L = n_ps"
by auto
define IN where "IN = all_actions_by_state trans_in_map L"
define OUT where "OUT = all_actions_by_state trans_out_map L"
have IN_I:
"(p, b, g, a', f, r, l') ∈ set (IN ! a')"
if "(L ! p, b, g, In a', f, r, l') ∈ Simple_Network_Language.trans (N p)"
"p < n_ps" "a' < num_actions"
for p b g a' f r l'
proof -
from trans_mapI[OF that(1,2)] have "(b, g, In a', f, r, l') ∈ set (trans_map p (L ! p))"
by auto
then have "(b, g, a', f, r, l') ∈ set (trans_in_map p (L ! p))"
unfolding trans_in_map_def set_map_filter by (auto 4 7)
with ‹p < _› ‹a' < _› show ?thesis
unfolding IN_def by (intro in_all_actions_by_stateI)
qed
have OUT_I:
"(p, b, g, a', f, r, l') ∈ set (OUT ! a')"
if "(L ! p, b, g, Out a', f, r, l') ∈ Simple_Network_Language.trans (N p)"
"p < n_ps" "a' < num_actions"
for p b g a' f r l'
proof -
from trans_mapI[OF that(1,2)] have "(b, g, Out a', f, r, l') ∈ set (trans_map p (L ! p))"
by auto
then have "(b, g, a', f, r, l') ∈ set (trans_out_map p (L ! p))"
unfolding trans_out_map_def set_map_filter by (auto 4 7)
with ‹p < _› ‹a' < _› show ?thesis
unfolding OUT_def by (intro in_all_actions_by_stateI)
qed
have IN_D:
"(L ! p, b, g, In a', f, r, l') ∈ Simple_Network_Language.trans (N p) ∧ p < n_ps ∧ a' = a1"
if "(p, b, g, a', f, r, l') ∈ set (IN ! a1)" "a1 < num_actions"
for p b g a' f r l' a1
using that
unfolding IN_def
apply -
apply (drule in_all_actions_by_stateD)
apply assumption
unfolding trans_in_map_def set_map_filter
apply (clarsimp split: option.split_asm)
apply (auto split: act.split_asm dest: trans_mapD)
done
have OUT_D:
"(L ! p, b, g, Out a1, f, r, l') ∈ Simple_Network_Language.trans (N p) ∧ p < n_ps"
if "(p, b, g, a', f, r, l') ∈ set (OUT ! a1)" "a1 < num_actions"
for p b g a' f r l' a1
using that
unfolding OUT_def
apply -
apply (drule in_all_actions_by_stateD)
apply assumption
unfolding trans_out_map_def set_map_filter
apply (clarsimp split: option.split_asm)
apply (auto split: act.split_asm dest: trans_mapD)
done
have IN_p_num:
"p < n_ps"
if "(p, b, g, a', f, r, l') ∈ set (IN ! a1)" "a1 < num_actions"
for p b g a' f r l' a1
using that unfolding IN_def by (auto dest: in_all_actions_by_stateD split: option.split_asm)
have OUT_p_num:
"p < n_ps"
if "(p, b, g, a', f, r, l') ∈ set (OUT ! a1)" "a1 < num_actions"
for p b g a' f r l' a1
using that unfolding OUT_def by (auto dest: in_all_actions_by_stateD split: option.split_asm)
have actions_unique:
"a' = a1"
if "(p, b, g, a', f, r, l') ∈ set (IN ! a1)" "a1 < num_actions"
for p b g a' f r l' a1
using that unfolding IN_def trans_in_map_def set_map_filter
by (auto dest: in_all_actions_by_stateD split: option.split_asm)
note [forward3] = OUT_I IN_I
note [forward2] = action_setD IN_D OUT_D
show "(((L, s), g, a, r, L', s') ∈ trans_bin) =
((g, a, r, L', s') ∈ set (bin_trans_from (L, s)))"
proof (cases "get_committed L = []")
case True
with get_committed_empty_iff[of L] have "∀p<n_ps. L ! p ∉ committed (N p)"
by simp
then have *: "((L, s), g, a, r, L', s') ∈ trans_bin ⟷ ((L, s), g, a, r, L', s') ∈
{((L, s), g1 @ g2, Bin a, r1 @ r2, (L', s'')) |
L s L' s' s'' a p q l1 b1 g1 f1 r1 l1' l2 b2 g2 f2 r2 l2'.
a ∉ local.broadcast ∧
(l1, b1, g1, In a, f1, r1, l1') ∈ trans (N p) ∧
(l2, b2, g2, Out a, f2, r2, l2') ∈ trans (N q) ∧
L!p = l1 ∧ L!q = l2 ∧ p < length L ∧ q < length L ∧ p ≠ q ∧
check_bexp s b1 True ∧ check_bexp s b2 True ∧
L' = L[p := l1', q := l2'] ∧ is_upds s f1 s' ∧ is_upds s' f2 s''
∧ L ∈ states ∧ bounded bounds s ∧ bounded bounds s''
}
"
unfolding trans_bin_def by blast
from True have **:
"bin_trans_from (L, s)
= concat (map (λa. pairs_by_action L s (OUT ! a) (IN ! a)) bin_actions)"
unfolding bin_trans_from_def IN_def OUT_def by simp
from ‹dom s = _› ‹L ∈ _› show ?thesis
unfolding * **
apply clarsimp
unfolding pairs_by_action_def
apply (clarsimp simp: set_map_filter Let_def)
apply safe
subgoal for _ s'' _ a' p q l1 b1 g1 f1 r1 l1' l2 b2 g2 f2 r2 l2'
apply clarsimp
apply (inst_existentials a')
subgoal
apply frules
apply simp
apply frules_all
unfolding check_bounded_iff by (intros; solve_triv)
subgoal
by (simp add: mem_bin_actions_iff; frules; simp)
done
subgoal
unfolding mem_bin_actions_iff
apply simp
apply (erule conjE)
apply frules
apply elims
apply frules_all
apply frules_all
apply elims
apply intros
using ‹bounded bounds s› unfolding check_bounded_iff[symmetric] by solve_triv+
done
next
case False
with get_committed_empty_iff[of L] have "∃p<n_ps. L ! p ∈ committed (N p)"
by simp
then have *: "((L, s), g, a, r, L', s') ∈ trans_bin ⟷ ((L, s), g, a, r, L', s') ∈
{((L, s), g1 @ g2, Bin a, r1 @ r2, (L', s'')) |
L s L' s' s'' a p q l1 b1 g1 f1 r1 l1' l2 b2 g2 f2 r2 l2'.
a ∉ local.broadcast ∧
(l1, b1, g1, In a, f1, r1, l1') ∈ trans (N p) ∧
(l2, b2, g2, Out a, f2, r2, l2') ∈ trans (N q) ∧
(l1 ∈ committed (N p) ∨ l2 ∈ committed (N q)) ∧
L!p = l1 ∧ L!q = l2 ∧ p < length L ∧ q < length L ∧ p ≠ q ∧
check_bexp s b1 True ∧ check_bexp s b2 True ∧
L' = L[p := l1', q := l2'] ∧ is_upds s f1 s' ∧ is_upds s' f2 s'' ∧
L ∈ states ∧ bounded bounds s ∧ bounded bounds s''
}"
unfolding trans_bin_def
by - (rule iffI; elims add: CollectE; intros add: CollectI; blast)
let ?S1 =
"{((L, s), g1 @ g2, Bin a, r1 @ r2, (L', s'')) |
L s L' s' s'' a p q l1 b1 g1 f1 r1 l1' l2 b2 g2 f2 r2 l2'.
a ∉ local.broadcast ∧
(l1, b1, g1, In a, f1, r1, l1') ∈ trans (N p) ∧
(l2, b2, g2, Out a, f2, r2, l2') ∈ trans (N q) ∧
l1 ∈ committed (N p) ∧
L!p = l1 ∧ L!q = l2 ∧ p < length L ∧ q < length L ∧ p ≠ q ∧
check_bexp s b1 True ∧ check_bexp s b2 True ∧
L' = L[p := l1', q := l2'] ∧ is_upds s f1 s' ∧ is_upds s' f2 s'' ∧
L ∈ states ∧ bounded bounds s ∧ bounded bounds s''
}"
let ?S2 =
"{((L, s), g1 @ g2, Bin a, r1 @ r2, (L', s'')) |
L s L' s' s'' a p q l1 b1 g1 f1 r1 l1' l2 b2 g2 f2 r2 l2'.
a ∉ local.broadcast ∧
(l1, b1, g1, In a, f1, r1, l1') ∈ trans (N p) ∧
(l2, b2, g2, Out a, f2, r2, l2') ∈ trans (N q) ∧
l2 ∈ committed (N q) ∧
L!p = l1 ∧ L!q = l2 ∧
p < length L ∧ q < length L ∧ p ≠ q ∧
check_bexp s b1 True ∧ check_bexp s b2 True ∧
L' = L[p := l1', q := l2'] ∧
is_upds s f1 s' ∧ is_upds s' f2 s'' ∧
L ∈ states ∧ bounded bounds s ∧ bounded bounds s''
}"
have *: "((L, s), g, a, r, L', s') ∈ trans_bin ⟷
((L, s), g, a, r, L', s') ∈ ?S1 ∨ ((L, s), g, a, r, L', s') ∈ ?S2"
unfolding * by clarsimp (rule iffI; elims add: disjE; intros add: disjI1 disjI2 HOL.refl)
define pairs where "pairs = get_committed L"
define In2 where "In2 = all_actions_from_vec trans_in_map pairs"
define Out2 where "Out2 = all_actions_from_vec trans_out_map pairs"
have In2_I:
"(p, b, g, a', f, r, l') ∈ set (In2 ! a')"
if "(L ! p, b, g, In a', f, r, l') ∈ Simple_Network_Language.trans (N p)"
"p < n_ps" "a' < num_actions" "L ! p ∈ committed (N p)"
for p b g a' f r l'
proof -
from ‹L ! p ∈ committed (N p)› ‹p < n_ps› have "(p, L ! p) ∈ set pairs"
unfolding pairs_def get_committed_mem_iff by blast
from trans_mapI[OF that(1,2)] have "(b, g, In a', f, r, l') ∈ set (trans_map p (L ! p))"
by auto
then have "(b, g, a', f, r, l') ∈ set (trans_in_map p (L ! p))"
unfolding trans_in_map_def set_map_filter by (auto 4 7)
with ‹p < _› ‹a' < _› ‹_ ∈ set pairs› show ?thesis
unfolding In2_def by (intro in_all_actions_from_vecI)
qed
have Out2_I:
"(p, b, g, a', f, r, l') ∈ set (Out2 ! a')"
if "(L ! p, b, g, Out a', f, r, l') ∈ Simple_Network_Language.trans (N p)"
"p < n_ps" "a' < num_actions" "L ! p ∈ committed (N p)"
for p b g a' f r l'
proof -
from ‹L ! p ∈ committed (N p)› ‹p < n_ps› have "(p, L ! p) ∈ set pairs"
unfolding pairs_def get_committed_mem_iff by blast
from trans_mapI[OF that(1,2)] have "(b, g, Out a', f, r, l') ∈ set (trans_map p (L ! p))"
by auto
then have "(b, g, a', f, r, l') ∈ set (trans_out_map p (L ! p))"
unfolding trans_out_map_def set_map_filter by (auto 4 7)
with ‹p < _› ‹a' < _› ‹_ ∈ set pairs› show ?thesis
unfolding Out2_def by (intro in_all_actions_from_vecI)
qed
have "distinct (map fst pairs)"
unfolding pairs_def get_committed_def distinct_map inj_on_def Let_def
by (auto simp: set_map_filter intro!: distinct_map_filterI split: if_split_asm)
have in_pairsD: "p < n_ps" "l = L ! p" "L ! p ∈ committed (N p)"
if "(p, l) ∈ set pairs" for p l
using that using get_committed_mem_iff pairs_def by auto
have In2_D:
"(L ! p, b, g, In a', f, r, l') ∈ Simple_Network_Language.trans (N p) ∧
p < n_ps ∧ a' = a1 ∧ L ! p ∈ committed (N p)"
if "(p, b, g, a', f, r, l') ∈ set (In2 ! a1)" "a1 < num_actions"
for p b g a' f r l' a1
using that
unfolding In2_def
apply -
apply (drule all_actions_from_vecD)
apply assumption
apply (rule ‹distinct _›)
unfolding trans_in_map_def set_map_filter
apply (clarsimp split: option.split_asm)
apply (auto dest: in_pairsD trans_mapD split: act.split_asm)
done
have Out2_D:
"(L ! p, b, g, Out a', f, r, l') ∈ Simple_Network_Language.trans (N p)
∧ p < n_ps ∧ a' = a1 ∧ L ! p ∈ committed (N p)"
if "(p, b, g, a', f, r, l') ∈ set (Out2 ! a1)" "a1 < num_actions"
for p b g a' f r l' a1
using that
unfolding Out2_def
apply -
apply (drule all_actions_from_vecD)
apply assumption
apply (rule ‹distinct _›)
unfolding trans_out_map_def set_map_filter
apply (clarsimp split: option.split_asm)
apply (auto dest: in_pairsD trans_mapD split: act.split_asm)
done
from False have **: "bin_trans_from (L, s) =
concat (map (λa. pairs_by_action L s (OUT ! a) (In2 ! a)) bin_actions)
@ concat (map (λa. pairs_by_action L s (Out2 ! a) (IN ! a)) bin_actions)"
unfolding bin_trans_from_def IN_def OUT_def In2_def Out2_def pairs_def
by (simp add: Let_def)
from ‹dom s = _› ‹L ∈ _› have "
((L, s), g, a, r, L', s') ∈ ?S1 ⟷ (g, a, r, L', s') ∈
set (concat (map (λa. pairs_by_action L s (OUT ! a) (In2 ! a)) bin_actions))"
apply clarsimp
unfolding pairs_by_action_def
apply (clarsimp simp: set_map_filter Let_def)
apply safe
subgoal for _ s'' _ a' p q l1 b1 g1 f1 r1 l1' l2 b2 g2 f2 r2 l2'
apply clarsimp
apply (inst_existentials a')
subgoal
supply [forward4] = In2_I
apply frules_all
apply simp
apply frules_all
unfolding check_bounded_iff by (intros; solve_triv)
subgoal
by (simp add: mem_bin_actions_iff; frules; simp)
done
subgoal
supply [forward2] = In2_D OUT_D
apply simp
unfolding mem_bin_actions_iff
apply (erule conjE)
apply frules_all
apply elims
apply frules_all
apply elims
apply simp
apply frules_all
using ‹bounded bounds s› unfolding check_bounded_iff[symmetric] by (intros; solve_triv)
done
moreover from ‹dom s = _› ‹L ∈ _› have "
((L, s), g, a, r, L', s') ∈ ?S2 ⟷ (g, a, r, L', s')
∈ set (concat (map (λa. pairs_by_action L s (Out2 ! a) (IN ! a)) bin_actions))"
supply [forward2] = Out2_D In2_D
supply [forward4] = Out2_I
apply clarsimp
unfolding pairs_by_action_def
apply (clarsimp simp: set_map_filter Let_def)
apply safe
subgoal for _ s'' _ a' p q l1 b1 g1 f1 r1 l1' l2 b2 g2 f2 r2 l2'
apply clarsimp
apply (inst_existentials a')
subgoal
apply frules_all
apply simp
apply frules_all
unfolding check_bounded_iff by (intros; solve_triv)
subgoal
unfolding mem_bin_actions_iff by frules_all simp
done
subgoal
apply simp
unfolding mem_bin_actions_iff
apply (erule conjE)
apply frules_all
apply elims
apply frules_all
apply elims
apply simp
apply frules_all
using ‹bounded bounds s› unfolding check_bounded_iff[symmetric] by (intros; solve_triv)
done
ultimately show ?thesis
unfolding * ** by simp
qed
qed
paragraph ‹Broadcast transitions›
lemma make_combs_alt_def:
"make_combs p a xs ≡
let
ys =
map (λ i. map (λt. (i, t)) (xs ! i ! a))
(filter
(λi. xs ! i ! a ≠ [] ∧ i ≠ p)
[0..<n_ps])
in if ys = [] then [] else product_lists ys"
apply (rule eq_reflection)
unfolding make_combs_def
apply (simp add: map_filter_def comp_def if_distrib[where f = the])
apply intros
apply (fo_rule arg_cong)
apply auto
done
lemma list_all2_fst_aux:
"map fst xs = ys" if "list_all2 (λx y. fst x = y) xs ys"
using that by (induction) auto
lemma broad_trans_from_correct:
"(broad_trans_from, trans_broad) ∈ transition_rel states'"
unfolding transition_rel_def
proof (safe del: iffI)
fix L s g a r L' s' assume "(L, s) ∈ states'"
then have "L ∈ states" "dom s = {0..<n_vs}" "bounded bounds s"
by auto
then have [simp]: "length L = n_ps"
by auto
define IN where "IN = map (λp. trans_in_broad_grouped p (L ! p)) [0..<n_ps]"
define OUT where "OUT = map (λp. trans_out_broad_grouped p (L ! p)) [0..<n_ps]"
define IN' where "IN' = map (map (filter (λ (b, _). bval (the o s) b))) IN"
define OUT' where "OUT' = map (map (filter (λ (b, _). bval (the o s) b))) OUT"
have IN_I:
"(b, g, a', f, r, l') ∈ set (IN ! p ! a')"
if "(L ! p, b, g, In a', f, r, l') ∈ Simple_Network_Language.trans (N p)"
"p < n_ps" "a' < num_actions" "a' ∈ set broadcast"
for p b g a' f r l'
proof -
from trans_mapI[OF that(1,2)] ‹a' ∈ _› have
"(b, g, a', f, r, l') ∈ set (trans_in_broad_map p (L ! p))"
unfolding trans_in_broad_map_def set_map_filter by (auto 4 7)
with ‹a' < _› have "(b, g, a', f, r, l') ∈ set (trans_in_broad_grouped p (L ! p) ! a')"
unfolding trans_in_broad_grouped_def by (auto dest: in_actions_by_state'I)
with ‹p < _› show ?thesis
unfolding IN_def by auto
qed
have OUT_I:
"(b, g, a', f, r, l') ∈ set (OUT ! p ! a')"
if "(L ! p, b, g, Out a', f, r, l') ∈ Simple_Network_Language.trans (N p)"
"p < n_ps" "a' < num_actions" "a' ∈ set broadcast"
for p b g a' f r l'
proof -
from trans_mapI[OF that(1,2)] ‹a' ∈ _› have
"(b, g, a', f, r, l') ∈ set (trans_out_broad_map p (L ! p))"
unfolding trans_out_broad_map_def set_map_filter by (auto 4 7)
with ‹a' < _› have "(b, g, a', f, r, l') ∈ set (trans_out_broad_grouped p (L ! p) ! a')"
unfolding trans_out_broad_grouped_def by (auto dest: in_actions_by_state'I)
with ‹p < _› show ?thesis
unfolding OUT_def by auto
qed
have IN_D:
"(L ! p, b, g, In a', f, r, l') ∈ Simple_Network_Language.trans (N p)
∧ a' = a1 ∧ a1 ∈ set broadcast"
if "(b, g, a', f, r, l') ∈ set (IN ! p ! a1)" "a1 < num_actions" "p < n_ps"
for p b g a' f r l' a1
using that unfolding IN_def trans_in_broad_grouped_def
apply simp
apply (drule in_actions_by_state'D)
unfolding trans_in_broad_map_def set_map_filter
by (auto split: option.split_asm) (auto split: act.split_asm if_split_asm dest: trans_mapD)
have [simp]: "length IN = n_ps" "length OUT = n_ps"
unfolding IN_def OUT_def by simp+
have [simp]: "length (IN ! p) = num_actions" "length (OUT ! p) = num_actions" if "p < n_ps" for p
using that by (simp add:
length_actions_by_state'_preserv trans_in_broad_grouped_def trans_out_broad_grouped_def
IN_def OUT_def)+
have OUT_D:
"(L ! p, b, g, Out a', f, r, l') ∈ Simple_Network_Language.trans (N p)
∧ a' = a1 ∧ a1 ∈ set broadcast"
if "(b, g, a', f, r, l') ∈ set (OUT ! p ! a1)" "a1 < num_actions" "p < n_ps"
for p b g a' f r l' a1
using that unfolding OUT_def trans_out_broad_grouped_def
apply simp
apply (drule in_actions_by_state'D)
unfolding trans_out_broad_map_def set_map_filter
by (auto split: option.split_asm) (auto split: act.split_asm if_split_asm dest: trans_mapD)
have IN'_I:
"(b, g, a', f, r, l') ∈ set (IN' ! p ! a')"
if "(b, g, a', f, r, l') ∈ set (IN ! p ! a')" "p < n_ps" "a' < num_actions"
"check_bexp s b True" for p b g a' f r l'
using that ‹dom s = {0..<n_vs}› unfolding IN'_def
by (auto dest!: IN_D[THEN conjunct1] elim: check_bexp_bvalI)
have IN'_D:
"(L ! p, b, g, In a', f, r, l') ∈ Simple_Network_Language.trans (N p)
∧ a' = a1 ∧ a1 ∈ set broadcast ∧ check_bexp s b True"
if "(b, g, a', f, r, l') ∈ set (IN' ! p ! a1)" "a1 < num_actions" "p < n_ps"
for p b g a' f r l' a1
using that ‹dom s = {0..<n_vs}› unfolding IN'_def by (auto dest!: IN_D elim: check_bexp_bvalD)
have OUT'_I:
"(b, g, a', f, r, l') ∈ set (OUT' ! p ! a')"
if "(b, g, a', f, r, l') ∈ set (OUT ! p ! a')" "p < n_ps" "a' < num_actions"
"check_bexp s b True" for p b g a' f r l'
using that ‹dom s = {0..<n_vs}› unfolding OUT'_def
by (auto dest!: OUT_D[THEN conjunct1] elim: check_bexp_bvalI)
have OUT'_D:
"(L ! p, b, g, Out a', f, r, l') ∈ Simple_Network_Language.trans (N p)
∧ a' = a1 ∧ a1 ∈ set broadcast ∧ check_bexp s b True"
if "(b, g, a', f, r, l') ∈ set (OUT' ! p ! a1)" "a1 < num_actions" "p < n_ps"
for p b g a' f r l' a1
using that ‹dom s = {0..<n_vs}› unfolding OUT'_def by (auto dest!: OUT_D elim: check_bexp_bvalD)
define make_trans where "make_trans a p ≡
let
outs = OUT' ! p ! a
in if outs = [] then []
else
let
combs = make_combs p a IN';
outs = map (λt. (p, t)) outs;
combs = (
if combs = [] then [[x]. x ← outs]
else concat (map (λx. map (λxs. x # xs) combs) outs));
init = ([], Broad a, [], (L, s))
in
filter (λ (g, a, r, L, s). check_bounded s) (
map (λcomb.
fold
(λ(q, b2, g2, a2, f2, r2, l2) (g1, a, r1, (L, s)).
(g1 @ g2, a, r1 @ r2, (L[q := l2], mk_upds s f2))
)
comb
init
) combs)" for a p
{
fix p ps bs gs a' fs rs ls'
assume assms:
"∀p∈set ps.
(L ! p, bs p, gs p, In a', fs p, rs p, ls' p) ∈ trans (N p)"
"∀q<n_ps. q ∉ set ps ∧ p ≠ q ⟶
(∀b g f r l'. (L ! q, b, g, In a', f, r, l') ∉ trans (N q) ∨ ¬ check_bexp s b True)"
"p < n_ps" "set ps ⊆ {0..<n_ps}" "p ∉ set ps" "distinct ps" "sorted ps"
"a' < num_actions" "a' ∈ set broadcast" "∀p ∈ set ps. check_bexp s (bs p) True"
define ys where "ys = List.map_filter
(λ i.
if i = p then None
else if IN' ! i ! a' = [] then None
else Some (map (λt. (i, t)) (IN' ! i ! a'))
)
[0..<n_ps]"
have "filter (λi. IN' ! i ! a' ≠ [] ∧ i ≠ p) [0..<n_ps] = ps"
apply (rule filter_distinct_eqI)
subgoal
using assms(4-) by (simp add: sorted_distinct_subseq_iff)
subgoal
using assms(1,3-) by (auto 4 3 dest!: IN_I IN'_I)
subgoal
using assms(1,2,4,8-)
apply -
apply (rule ccontr)
apply simp
apply elims
apply (drule hd_in_set)
subgoal for x
by (cases "hd (IN' ! x ! a')") (fastforce dest!: IN'_D)
done
by auto
then have "length ys = length ps"
unfolding ys_def map_filter_def by simp
have non_empty: "ys ≠ []" if "ps ≠ []"
using ‹_ = ps› ‹ps ≠ []› unfolding ys_def map_filter_def by simp
have make_combsD:
"map (λp. (p, bs p, gs p, a', fs p, rs p, ls' p)) ps ∈ set (make_combs p a' IN')"
if "ps ≠ []"
proof -
from assms(1,3-) have
"∀i<length ps. let p = ps ! i in (p, bs p, gs p, a', fs p, rs p, ls' p) ∈ set (ys ! i)"
unfolding ys_def Let_def map_filter_def
apply (simp add: comp_def if_distrib[where f = the])
apply (subst (2) map_cong)
apply (rule HOL.refl)
apply (simp; fail)
apply (simp add: ‹_ = ps›)
by (intros add: image_eqI[OF HOL.refl] IN_I IN'_I; simp add: subset_code(1))
with non_empty[OF that] show ?thesis
unfolding make_combs_def ys_def[symmetric] Let_def
by (auto simp: ‹length ys = _› product_lists_set intro:list_all2_all_nthI)
qed
have make_combs_empty:
"make_combs p a' IN' = [] ⟷ ps = []"
proof (cases "ps = []")
case True
then show ?thesis
using ‹length ys = length ps› unfolding make_combs_def ys_def[symmetric] Let_def by auto
next
case False
then show ?thesis
using make_combsD by auto
qed
note make_combsD make_combs_empty
} note make_combsD = this(1) and make_combs_empty = this(2)
have make_combs_emptyD: "filter (λi. IN' ! i ! a' ≠ [] ∧ i ≠ p) [0..<n_ps] = []"
if "make_combs p a' IN' = []" for p a'
apply (rule filter_distinct_eqI)
subgoal
by auto
subgoal
by auto
subgoal
using that unfolding make_combs_alt_def
by (auto simp: filter_empty_conv product_lists_empty split: if_split_asm)
subgoal
by simp
done
have make_combsI:
"∃ ps bs gs fs rs ls'.
(∀p∈set ps.
(L ! p, bs p, gs p, In a', fs p, rs p, ls' p) ∈ trans (N p)) ∧
(∀q<n_ps. q ∉ set ps ∧ p ≠ q ⟶
(∀b g f r l'. (L ! q, b, g, In a', f, r, l') ∉ trans (N q) ∨ ¬ check_bexp s b True)) ∧
set ps ⊆ {0..<n_ps} ∧ p ∉ set ps ∧ distinct ps ∧ sorted ps ∧ ps ≠ [] ∧ a' ∈ set broadcast
∧ (∀p ∈ set ps. check_bexp s (bs p) True)
∧ xs = map (λ p. (p, bs p, gs p, a', fs p, rs p, ls' p)) ps
∧ filter (λi. IN' ! i ! a' ≠ [] ∧ i ≠ p) [0..<n_ps] = ps"
if "xs ∈ set (make_combs p a' IN')" "p < n_ps" "a' < num_actions"
for xs p a'
proof -
define ps bs gs fs rs ls' where defs:
"ps = map fst xs"
"bs = (λi. case the (map_of xs i) of (b, g, a, f, r, l') ⇒ b)"
"gs = (λi. case the (map_of xs i) of (b, g, a, f, r, l') ⇒ g)"
"fs = (λi. case the (map_of xs i) of (b, g, a, f, r, l') ⇒ f)"
"rs = (λi. case the (map_of xs i) of (b, g, a, f, r, l') ⇒ r)"
"ls' = (λi. case the (map_of xs i) of (b, g, a, f, r, l') ⇒ l')"
have "filter (λi. IN' ! i ! a' ≠ [] ∧ i ≠ p) [0..<n_ps] = ps"
apply (rule filter_distinct_eqI)
subgoal
using that
unfolding defs make_combs_alt_def Let_def
by (auto simp: set_map_filter product_lists_set list_all2_map2 list.rel_eq
dest: list_all2_map_fst_aux split: if_split_asm)
subgoal
using that unfolding defs make_combs_alt_def Let_def
by (auto simp: set_map_filter product_lists_set dest!: list_all2_set1 split: if_split_asm)
subgoal
using that
unfolding defs make_combs_alt_def Let_def
by (auto
simp: set_map_filter product_lists_set list_all2_map2 list.rel_eq
dest!: map_eq_imageD list_all2_map_fst_aux split: if_split_asm)
subgoal
by simp
done
then have "set ps ⊆ {0..<n_ps}" "p ∉ set ps" "distinct ps" "sorted ps"
by (auto intro: sorted_filter')
have to_map: "a' = a" "the (map_of xs q) = (b, g, a, r, f, l')"
if "(q, b, g, a, r, f, l') ∈ set xs" for b q g a r f l'
using that
apply -
subgoal
using ‹set ps ⊆ _› ‹a' < _› ‹xs ∈ _›
by
(simp
add: make_combs_alt_def product_lists_set ‹_ = ps› list_all2_map2
split: if_split_asm
) (auto 4 3 dest!: IN'_D list_all2_set1)
subgoal
using ‹distinct ps›
by (subst (asm) map_of_eq_Some_iff[of xs q, symmetric]) (auto simp: defs)
done
from that have *: "∀p∈set ps.
(L ! p, bs p, gs p, In a', fs p, rs p, ls' p) ∈ Simple_Network_Language.trans (N p)"
unfolding make_combs_alt_def ‹_ = ps›
apply (clarsimp simp: set_map_filter product_lists_set split: if_split_asm)
using ‹set ps ⊆ _› unfolding defs
by (auto simp: comp_def list_all2_map2 list_all2_same to_map
elim!: IN'_D[THEN conjunct1, rotated]
)
from that have "ps ≠ []" "a' ∈ set broadcast"
apply (simp_all add: make_combs_alt_def set_map_filter product_lists_set split: if_split_asm)
using ‹_ = ps› ‹set ps ⊆ {0..<n_ps}›
by (cases xs; auto dest: IN'_D simp: list_all2_Cons1)+
with that have "∀q<n_ps. q ∉ set ps ∧ p ≠ q ⟶
(∀b g f r l'. (L ! q, b, g, In a', f, r, l') ∉ trans (N q) ∨ ¬ check_bexp s b True)"
unfolding make_combs_alt_def
by (auto 4 3 dest!: list_all2_set2 IN_I IN'_I
simp: defs set_map_filter product_lists_set split: if_split_asm)
have "xs = map (λ p. (p, bs p, gs p, a', fs p, rs p, ls' p)) ps"
apply (intro nth_equalityI)
apply (simp add: defs; fail)
subgoal for i
by (cases "xs ! i") (auto 4 4 simp: defs dest: to_map nth_mem)
done
have "∀p∈set ps. check_bexp s (bs p) True"
proof
fix q assume "q ∈ set ps"
from ‹xs ∈ _› have "distinct (map fst xs)"
unfolding make_combs_alt_def
by (auto simp: product_lists_set list_all2_map2 to_map
dest!: list_all2_fst_aux[OF list_all2_mono]
split: if_split_asm)
from ‹q ∈ set ps› ‹_ = ps› have "IN' ! q ! a' ≠ []" "q ≠ p" "q < n_ps"
by auto
with that have "the (map_of xs q) ∈ set (IN' ! q ! a')"
using set_map_of_compr[OF ‹distinct (map _ _)›] unfolding make_combs_alt_def
apply (clarsimp simp: set_map_filter product_lists_set split: if_split_asm)
apply (drule list_all2_set2)
apply auto
done
then obtain a where "(bs q, gs q, a, fs q, rs q, ls' q) ∈ set (IN' ! q ! a')"
unfolding defs by atomize_elim (auto split!: prod.splits)
then show "check_bexp s (bs q) True"
using IN'_D ‹a' < _› ‹set ps ⊆ _› ‹q ∈ set ps› by auto
qed
show ?thesis
by (inst_existentials ps bs gs fs rs ls'; fact)
qed
let ?f = "λ(q, b2, g2, a2, f2, r2, l2) (g1, a, r1, L, s).
(g1 @ g2, a, r1 @ r2, L[q := l2], mk_upds s f2)"
have ***: "
fold ?f (map (λp. (p, bs p, gs p, a', fs p, rs p, ls' p)) ps) (g, a, r, L, s)
= (g @ concat (map gs ps), a, r @ concat (map rs ps),
fold (λp L. L[p := ls' p]) ps L, mk_upds s (concat_map fs ps))
" for ps bs gs a' fs rs ls' g a r L s
by (induction ps arbitrary: g a r L s; simp add: mk_upds_def)
have upd_swap:
"(fold (λp L . L[p := ls' p]) ps L)[p := l'] = fold (λp L . L[p := ls' p]) ps (L[p := l'])"
if "p ∉ set ps" for ps ls' p l'
using that by (induction ps arbitrary: L) (auto simp: list_update_swap)
have make_transI:
"a' < num_actions ∧ p < n_ps ∧
(g1 @ concat (map gs ps), Broad a', r1 @ concat (map rs ps),
(fold (λp L. L[p := ls' p]) ps L)[p := l'], s') ∈ set (make_trans a' p)"
if
"L ∈ states" and
"g = g1 @ concat (map gs ps)" and
"a = Broad a'" and
"r = r1 @ concat (map rs ps)" and
"L' = (fold (λp L. L[p := ls' p]) ps L)[p := l']" and
"a' ∈ set broadcast" and
"(L ! p, b1, g1, Out a', f1, r1, l') ∈ trans (N p)" and
"∀p∈set ps. (L ! p, bs p, gs p, In a', fs p, rs p, ls' p) ∈ trans (N p)"
and
"∀q<n_ps. q ∉ set ps ∧ p ≠ q
⟶ (∀b g f r l'. (L ! q, b, g, In a', f, r, l') ∉ trans (N q) ∨ ¬ check_bexp s b True)" and
"p < n_ps" and
"set ps ⊆ {0..<n_ps}" and
"p ∉ set ps" and
"distinct ps" and
"sorted ps" and
"check_bexp s b1 True" and
"∀p∈set ps. check_bexp s (bs p) True" and
"is_upds s f1 s''" and
"is_upds s'' (concat_map fs ps) s'" and
"Simple_Network_Language.bounded bounds s'"
for a' p b1 g1 bs gs ps r1 rs ls' l' f1 s'' fs
using that ‹dom s = {0..<n_vs}›
unfolding make_trans_def
apply (clarsimp simp: set_map_filter Let_def split: prod.split)
supply [forward2] = action_setD
supply [forward4] = is_upds_dom2 is_upds_dom3 is_upds_concatD[rotated 3] OUT_I OUT'_I
apply frule2
apply simp
apply (rule conjI, rule impI)
subgoal
apply (subst (asm) make_combs_empty, (assumption | simp)+)
apply frules_all
apply (intro conjI)
apply (solves auto)
apply (intros add: more_intros)
apply (solve_triv | intros add: more_intros UN_I)+
subgoal
unfolding comp_def by (auto elim!: is_upds.cases)
by (auto simp: check_bounded_iff[symmetric] elim: is_upds_NilE)
apply (rule impI)
apply (frule make_combsD, simp, assumption+)
subgoal
by (subst (asm) make_combs_empty) (assumption | simp)+
apply frules_all
apply simp
apply (intro conjI)
apply (solves auto)
apply (intros add: more_intros)
apply (solve_triv | intros add: more_intros UN_I)+
apply (simp add: *** upd_swap; fail)
unfolding check_bounded_iff[symmetric] .
have make_transD:
"∃s'' b ga f ra l' bs gs fs rs ls' ps.
g = ga @ concat (map gs ps) ∧
a = Broad a' ∧
r = ra @ concat (map rs ps) ∧
L' = (fold (λp L. L[p := ls' p]) ps L)[p := l'] ∧
a' ∈ set broadcast ∧
(L ! p, b, ga, Out a', f, ra, l') ∈ trans (N p) ∧
(∀p∈set ps. (L ! p, bs p, gs p, In a', fs p, rs p, ls' p) ∈ trans (N p)) ∧
(∀q<n_ps.
q ∉ set ps ∧ p ≠ q ⟶
(∀b g f r l'. (L ! q, b, g, In a', f, r, l') ∉ trans (N q) ∨ ¬ check_bexp s b True)) ∧
p < n_ps ∧
set ps ⊆ {0..<n_ps} ∧
p ∉ set ps ∧
distinct ps ∧
sorted ps ∧
check_bexp s b True ∧ (∀p∈set ps. check_bexp s (bs p) True) ∧
is_upds s f s'' ∧ is_upds s'' (concat_map fs ps) s' ∧
bounded bounds s' ∧
filter (λi. IN' ! i ! a' ≠ [] ∧ i ≠ p) [0..<n_ps] = ps"
if
"L ∈ states" and
"a' < num_actions" and
"p < n_ps" and
"(g, a, r, L', s') ∈ set (make_trans a' p)"
for a' p
supply [forward2] = action_setD
supply [forward3] = is_upds_make_updsI3[rotated] OUT'_D
supply [forward4] = is_upds_dom2 is_upds_dom3 is_upds_concatD[rotated 3] OUT_I OUT'_I
using that ‹dom s = {0..<n_vs}›
unfolding make_trans_def
apply mini_ex
apply (clarsimp simp: set_map_filter Let_def split: prod.split if_split_asm)
subgoal for b a1 f l'
apply (inst_existentials
"b :: (nat, int) bexp"
"g :: (nat, int) acconstraint list"
"f :: (nat × (nat, int) exp) list"
"r :: nat list"
l'
"undefined :: nat ⇒ (nat, int) bexp"
"undefined :: nat ⇒ (nat, int) acconstraint list"
"undefined :: nat ⇒ (nat × (nat, int) exp) list"
"undefined :: nat ⇒ nat list"
"undefined :: nat ⇒ nat"
"[] :: nat list")
apply (solves ‹auto dest: OUT'_D›)+
subgoal
by (auto 4 3 simp: filter_empty_conv dest: bspec dest!: make_combs_emptyD OUT'_D IN_I IN'_I)
apply (solves ‹auto dest: OUT'_D›)+
subgoal
apply (inst_existentials s')
subgoal is_upd
by (auto intro: is_upds_make_updsI2 dest: OUT'_D)
subgoal
by simp (rule is_upds.intros)
subgoal
by (subst check_bounded_iff) (metis OUT'_D is_upds_dom2 is_upd)+
subgoal
by (rule make_combs_emptyD)
done
done
subgoal for b1 g1 a1 r1 f1 l1' xs
apply (drule make_combsI, assumption+)
apply frules
apply elims
apply dedup_prems
apply frules_all
apply (simp add: *** )
apply intros
apply solve_triv+
apply (erule upd_swap[symmetric]; fail)
apply solve_triv+
apply (erule bspec; assumption)
apply (elims add: allE; intros?; assumption)
apply solve_triv+
subgoal for ps gs fs rs ls'
apply (subst check_bounded_iff)
subgoal
apply (subst is_upds_dom3)
apply (simp add: fold_map comp_def; fail)
apply assumption+
done
subgoal
by simp
done
apply solve_triv
done
done
have make_trans_iff: "
(∃s'' aa p b ga f ra l' bs gs fs rs ls' ps.
g = ga @ concat (map gs ps) ∧
a = Broad aa ∧
r = ra @ concat (map rs ps) ∧
L' = (fold (λp L. L[p := ls' p]) ps L)[p := l'] ∧
aa ∈ set broadcast ∧
(L ! p, b, ga, Out aa, f, ra, l') ∈ Simple_Network_Language.trans (N p) ∧
(∀p∈set ps.
(L ! p, bs p, gs p, In aa, fs p, rs p, ls' p)
∈ Simple_Network_Language.trans (N p)) ∧
(∀q<n_ps.
q ∉ set ps ∧ p ≠ q ⟶
(∀b g f r l'.
(L ! q, b, g, In aa, f, r, l') ∉ trans (N q) ∨ ¬ check_bexp s b True)) ∧
p < n_ps ∧
set ps ⊆ {0..<n_ps} ∧
p ∉ set ps ∧
distinct ps ∧
sorted ps ∧
check_bexp s b True ∧ (∀p∈set ps. check_bexp s (bs p) True) ∧
is_upds s f s'' ∧
is_upds s'' (concat_map fs ps) s' ∧
bounded bounds s') =
(∃a'∈{0..<num_actions}.
∃p∈{0..<n_ps}. (g, a, r, L', s') ∈ set (make_trans a' p))" (is "?l ⟷ ?r")
if "dom s = {0..<n_vs}" "L ∈ states"
proof (intro iffI)
assume ?l
with that show ?r
by elims (drule make_transI; (elims; intros)?; solve_triv)
next
assume ?r
with that show ?l
apply elims
subgoal for a' p
apply simp
apply (drule make_transD)
apply assumption+
apply elims
apply intros
apply assumption+
apply blast+
done
done
qed
show "(((L, s), g, a, r, L', s') ∈ trans_broad) =
((g, a, r, L', s') ∈ set (broad_trans_from (L, s)))"
proof (cases "get_committed L = []")
case True
with get_committed_empty_iff[of L] have "∀p<n_ps. L ! p ∉ committed (N p)"
by simp
then have *: "((L, s), g, a, r, L', s') ∈ trans_broad ⟷ ((L, s), g, a, r, L', s') ∈
{((L, s), g @ concat (map gs ps), Broad a, r @ concat (map rs ps), (L', s'')) |
L s L' s' s'' a p l b g f r l' bs gs fs rs ls' ps.
a ∈ set broadcast ∧
(l, b, g, Out a, f, r, l') ∈ trans (N p) ∧
(∀p ∈ set ps. (L ! p, bs p, gs p, In a, fs p, rs p, ls' p) ∈ trans (N p)) ∧
(∀q < n_ps. q ∉ set ps ∧ p ≠ q ⟶
¬ (∃b g f r l'. (L ! q, b, g, In a, f, r, l') ∈ trans (N q) ∧ check_bexp s b True)) ∧
L!p = l ∧
p < length L ∧ set ps ⊆ {0..<n_ps} ∧ p ∉ set ps ∧ distinct ps ∧ sorted ps ∧
check_bexp s b True ∧ (∀p ∈ set ps. check_bexp s (bs p) True) ∧
L' = (fold (λp L . L[p := ls' p]) ps L)[p := l'] ∧
is_upds s f s' ∧ is_upds s' (concat_map fs ps) s'' ∧
L ∈ states ∧ bounded bounds s ∧ bounded bounds s''
}
"
unfolding trans_broad_def broadcast_def[simplified]
by (intro iffI; elims add: CollectE; intros add: CollectI) blast+
from True have **:
"broad_trans_from (L, s)
= concat (
map (λa.
concat (map (λp. make_trans a p) [0..<n_ps])
)
[0..<num_actions]
)"
unfolding broad_trans_from_alt_def IN_def OUT_def IN'_def OUT'_def Let_def make_trans_def
by simp
from ‹dom s = _› ‹L ∈ _› ‹bounded bounds s› show ?thesis
unfolding * **
apply simp
apply (subst make_trans_iff[symmetric])
apply simp+
apply (intro iffI; elims; intros)
apply (solve_triv | blast)+
done
next
case False
with get_committed_empty_iff[of L] have "¬ (∀p<n_ps. L ! p ∉ committed (N p))"
by simp
then have *: "((L, s), g, a, r, L', s') ∈ trans_broad ⟷ ((L, s), g, a, r, L', s') ∈
{((L, s), g @ concat (map gs ps), Broad a, r @ concat (map rs ps), (L', s'')) |
L s L' s' s'' a p l b g f r l' bs gs fs rs ls' ps.
a ∈ set broadcast ∧
(l, b, g, Out a, f, r, l') ∈ trans (N p) ∧
(∀p ∈ set ps. (L ! p, bs p, gs p, In a, fs p, rs p, ls' p) ∈ trans (N p)) ∧
(l ∈ committed (N p) ∨ (∃p ∈ set ps. L ! p ∈ committed (N p))) ∧
(∀q < n_ps. q ∉ set ps ∧ p ≠ q ⟶
¬ (∃b g f r l'. (L ! q, b, g, In a, f, r, l') ∈ trans (N q) ∧ check_bexp s b True)) ∧
L!p = l ∧
p < length L ∧ set ps ⊆ {0..<n_ps} ∧ p ∉ set ps ∧ distinct ps ∧ sorted ps ∧
check_bexp s b True ∧ (∀p ∈ set ps. check_bexp s (bs p) True) ∧
L' = (fold (λp L . L[p := ls' p]) ps L)[p := l'] ∧
is_upds s f s' ∧ is_upds s' (concat_map fs ps) s'' ∧
L ∈ states ∧ bounded bounds s ∧ bounded bounds s''
}"
unfolding trans_broad_def broadcast_def[simplified]
by (intro iffI; elims add: CollectE; intros add: CollectI) blast+
have committed_iff: "
List.map_filter (λ(p, _). if IN' ! p ! a' = [] then None else Some p) (get_committed L) ≠ [p] ∧
List.map_filter (λ(p, _). if IN' ! p ! a' = [] then None else Some p) (get_committed L) ≠ []
⟷ (∃q<n_ps. IN' ! q ! a' ≠ [] ∧ q ≠ p ∧ L ! q ∈ committed (N q))"
for p a'
proof -
have *: "xs ≠ [p] ∧ xs ≠ [] ⟷ (∃x ∈ set xs. x ≠ p)" if "distinct xs" for xs
using that by auto (metis distinct.simps(2) distinct_length_2_or_more revg.elims)
show ?thesis
by (subst *)
(auto
intro: distinct_map_filterI get_committed_distinct
simp: set_map_filter get_committed_mem_iff split: if_split_asm
)
qed
from False have **:
"broad_trans_from (L, s)
= concat (
map (λa.
let
ins_committed =
List.map_filter (λ(p, _). if IN' ! p ! a ≠ [] then Some p else None) (get_committed L)
in
concat (map (λp.
if
(ins_committed = [p] ∨ ins_committed = [])
∧ ¬ list_ex (λ (q, _). q = p) (get_committed L)
then []
else
make_trans a p
)
[0..<n_ps])
)
[0..<num_actions])
"
unfolding broad_trans_from_alt_def IN_def OUT_def IN'_def OUT'_def make_trans_def
unfolding Let_def if_contract
apply simp
apply (fo_rule if_cong arg_cong2[where f = map] arg_cong[where f = concat] | rule ext)+
apply blast+
done
from ‹dom s = _› ‹L ∈ _› ‹bounded bounds s› show ?thesis
unfolding * **
apply (simp add: make_trans_iff)
apply (intro iffI; elims)
subgoal for s'a aa p ga f ra l' gs fs rs ls' ps
apply (frule make_transI)
apply (assumption | blast)+
apply elims
apply intros
apply (simp; fail)
apply (simp add: Let_def)
apply (erule disjE)
subgoal
using get_committed_mem_iff[of p "L ! p" L, simplified, symmetric]
by (inst_existentials p) (auto simp add: list_ex_iff)
apply (erule bexE)
subgoal for q
apply (inst_existentials p)
apply assumption
apply (rule IntI)
apply (simp; fail)
apply simp
unfolding committed_iff
apply (rule disjI1; inst_existentials q; force dest!: IN_I IN'_I)
done
done
subgoal for a'
apply (clarsimp split: if_split_asm simp: Let_def)
apply (drule make_transD[rotated 4])
apply assumption+
apply elims
apply intros
apply assumption+
apply (erule bspec; assumption)
subgoal for p s'' g' f r' l' gs fs rs ls' ps
unfolding committed_iff by (auto simp: get_committed_mem_iff list_ex_iff)
apply blast+
done
done
qed
qed
paragraph ‹Refinement of the State Implementation›
definition state_rel :: "(nat ⇀ int) ⇒ int list ⇒ bool"
where
"state_rel s xs ≡ length xs = n_vs ∧ dom s = {0..<n_vs} ∧ (∀i < n_vs. xs ! i = the (s i))"
definition loc_rel where
"loc_rel ≡ {((L', s'), (L, s)) | L s L' s'. L' = L ∧ length L = n_ps ∧ state_rel s s'}"
lemma state_impl_abstract:
"∃L s. ((Li, si), (L, s)) ∈ loc_rel" if "length Li = n_ps" "length si = n_vs"
using that unfolding loc_rel_def state_rel_def
by (inst_existentials Li "λi. if i < n_vs then Some (si ! i) else None")(auto split: if_split_asm)
lemma state_rel_left_unique:
"l ∈ states' ⟹ (li, l) ∈ loc_rel ⟹ (li', l) ∈ loc_rel ⟹ li' = li"
unfolding loc_rel_def state_rel_def by (auto intro: nth_equalityI)
lemma state_rel_right_unique:
"l ∈ states' ⟹ l' ∈ states' ⟹ (li, l) ∈ loc_rel ⟹ (li, l') ∈ loc_rel ⟹ l' = l"
unfolding loc_rel_def state_rel_def
apply clarsimp
apply (rule ext)
subgoal premises prems for L s s'1 s'2 x
proof -
show "s'1 x = s x"
proof (cases "x < n_vs")
case True
then have "x ∈ dom s'1" "x ∈ dom s"
using prems by auto
with ‹x < n_vs› show ?thesis
using prems(9) by auto
next
case False
then have "x ∉ dom s'1" "x ∉ dom s"
using prems by auto
then show ?thesis
by (auto simp: dom_def)
qed
qed
done
end
end
fun bvali :: "_ ⇒ (nat, 'b :: linorder) bexp ⇒ bool" and evali where
"bvali s bexp.true = True" |
"bvali s (not e) ⟷ ¬ bvali s e" |
"bvali s (and e1 e2) ⟷ bvali s e1 ∧ bvali s e2" |
"bvali s (bexp.or e1 e2) ⟷ bvali s e1 ∨ bvali s e2" |
"bvali s (imply e1 e2) ⟷ bvali s e1 ⟶ bvali s e2" |
"bvali s (eq i x) ⟷ evali s i = evali s x" |
"bvali s (le i x) ⟷ evali s i ≤ evali s x" |
"bvali s (lt i x) ⟷ evali s i < evali s x" |
"bvali s (ge i x) ⟷ evali s i ≥ evali s x" |
"bvali s (gt i x) ⟷ evali s i > evali s x"
| "evali s (const c) = c"
| "evali s (var x) = s ! x"
| "evali s (if_then_else b e1 e2) = (if bvali s b then evali s e1 else evali s e2)"
| "evali s (binop f e1 e2) = f (evali s e1) (evali s e2)"
| "evali s (unop f e) = f (evali s e)"
definition mk_updsi ::
"int list ⇒ (nat × (nat, int) exp) list ⇒ int list" where
"mk_updsi s upds = fold (λ(x, upd) s. s[x := evali s upd]) upds s"
context Simple_Network_Impl_nat_defs
begin
definition
"check_boundedi s =
(∀x < length s. fst (bounds_map x) ≤ s ! x ∧ s ! x ≤ snd (bounds_map x))"
definition
"states'_memi ≡ λ(L, s). L ∈ states ∧ length s = n_vs ∧ check_boundedi s"
definition
"int_trans_from_loc_impl p l L s ≡
let trans = trans_i_map p l
in
List.map_filter (λ (b, g, a, f, r, l').
let s' = mk_updsi s f in
if bvali s b ∧ check_boundedi s' then Some (g, Internal a, r, (L[p := l'], s'))
else None
) trans"
definition
"int_trans_from_vec_impl pairs L s ≡
concat (map (λ(p, l). int_trans_from_loc_impl p l L s) pairs)"
definition
"int_trans_from_all_impl L s ≡
concat (map (λp. int_trans_from_loc_impl p (L ! p) L s) [0..<n_ps])"
definition
"int_trans_impl ≡ λ (L, s).
let pairs = get_committed L in
if pairs = []
then int_trans_from_all_impl L s
else int_trans_from_vec_impl pairs L s
"
definition
"pairs_by_action_impl L s OUT IN ≡
concat (
map (λ (p, b1, g1, a1, f1, r1, l1).
List.map_filter (λ (q, b2, g2, a2, f2, r2, l2).
if p = q then None else
let s' = mk_updsi (mk_updsi s f1) f2 in
if bvali s b1 ∧ bvali s b2 ∧ check_boundedi s'
then Some (g1 @ g2, Bin a1, r1 @ r2, (L[p := l1, q := l2], s'))
else None
) OUT) IN)
"
definition
"bin_trans_from_impl ≡ λ(L, s).
let
pairs = get_committed L;
In = all_actions_by_state trans_in_map L;
Out = all_actions_by_state trans_out_map L
in
if pairs = [] then
concat (map (λa. pairs_by_action_impl L s (Out ! a) (In ! a)) bin_actions)
else
let
In2 = all_actions_from_vec trans_in_map pairs;
Out2 = all_actions_from_vec trans_out_map pairs
in
concat (map (λa. pairs_by_action_impl L s (Out ! a) (In2 ! a)) bin_actions)
@ concat (map (λa. pairs_by_action_impl L s (Out2 ! a) (In ! a)) bin_actions)
"
definition
"compute_upds init ≡ List.map_filter (λcomb.
let (g, a, r, L', s) =
fold
(λ(q, b2, g2, a2, f2, r2, l2) (g1, a, r1, (L, s)).
(g1 @ g2, a, r1 @ r2, (L[q := l2], mk_upds s f2))
)
comb
init
in if check_bounded s then Some (g, a, r, L', s) else None
)"
definition
"compute_upds_impl init ≡ List.map_filter (λcomb.
let (g, a, r, L', s) =
fold
(λ(q, b2, g2, a2, f2, r2, l2) (g1, a, r1, (L, s)).
(g1 @ g2, a, r1 @ r2, (L[q := l2], mk_updsi s f2))
)
comb
init
in if check_boundedi s then Some (g, a, r, L', s) else None
)"
definition trans_from where
"trans_from st = int_trans_from st @ bin_trans_from st @ broad_trans_from st"
definition
"broad_trans_from_impl ≡ λ(L, s).
let
pairs = get_committed L;
In = map (λp. trans_in_broad_grouped p (L ! p)) [0..<n_ps];
Out = map (λp. trans_out_broad_grouped p (L ! p)) [0..<n_ps];
In = map (map (filter (λ(b, _). bvali s b))) In;
Out = map (map (filter (λ(b, _). bvali s b))) Out
in
if pairs = [] then
concat (
map (λa.
concat (map (λp.
let
outs = Out ! p ! a
in if outs = [] then []
else
let
combs = make_combs p a In;
outs = map (λt. (p, t)) outs;
combs = (
if combs = [] then [[x]. x ← outs]
else concat (map (λx. map (λxs. x # xs) combs) outs));
init = ([], Broad a, [], (L, s))
in
compute_upds_impl init combs
)
[0..<n_ps])
)
[0..<num_actions])
else
concat (
map (λa.
let
ins_committed =
List.map_filter (λ(p, _). if In ! p ! a ≠ [] then Some p else None) pairs;
always_committed = (length ins_committed > 1)
in
concat (map (λp.
let
outs = Out ! p ! a
in if outs = [] then []
else if
¬ always_committed ∧ (ins_committed = [p] ∨ ins_committed = [])
∧ ¬ list_ex (λ (q, _). q = p) pairs
then []
else
let
combs = make_combs p a In;
outs = map (λt. (p, t)) outs;
combs = (
if combs = [] then [[x]. x ← outs]
else concat (map (λx. map (λxs. x # xs) combs) outs));
init = ([], Broad a, [], (L, s))
in
compute_upds_impl init combs
)
[0..<n_ps])
)
[0..<num_actions])
"
definition trans_impl where
"trans_impl st = int_trans_impl st @ bin_trans_from_impl st @ broad_trans_from_impl st"
end
context Simple_Network_Impl_nat
begin
lemma bval_bvali:
"state_rel s si ⟹ ∀x ∈ vars_of_bexp b. x ∈ dom s ⟹ bval (the o s) b = bvali si b"
and eval_evali:
"state_rel s si ⟹ ∀x ∈ vars_of_exp e. x ∈ dom s ⟹ eval (the o s) e = evali si e"
by (induction b and e) (auto simp: state_rel_def)
lemma mk_upds_mk_updsi:
"state_rel (mk_upds s upds) (mk_updsi si upds)"
if assms: "state_rel s si" "∀ (_, e) ∈ set upds. ∀x ∈ vars_of_exp e. x < n_vs"
"∀ (x, e) ∈ set upds. x < n_vs"
proof -
have upd_stepI: "state_rel (mk_upd (x, e) s') (si'[x := evali si' e])"
if "state_rel s' si'" "∀x ∈ vars_of_exp e. x < n_vs" "x < n_vs"
for s' si' x e
using that assms unfolding mk_upd_def state_rel_def by (auto simp: state_rel_def eval_evali)
from assms show ?thesis
proof (induction upds arbitrary: s si)
case Nil
then show ?case
by (simp add: mk_upds_def mk_updsi_def)
next
case (Cons upd upds)
then show ?case
by (simp add: mk_upds_def mk_updsi_def split: prod.splits) (rprem, auto intro!: upd_stepI)
qed
qed
lemma check_bounded_check_boundedi:
"check_bounded s = check_boundedi si" if "state_rel s si"
using that unfolding check_bounded_def check_boundedi_def state_rel_def by auto
definition
"valid_upd ≡ λ(x, e). x < n_vs ∧ (∀x ∈ vars_of_exp e. x < n_vs)"
definition
"valid_check b ≡ (∀x ∈ vars_of_bexp b. x < n_vs)"
context includes lifting_syntax begin
notation rel_prod (infixr "×⇩R" 56)
definition is_at_least_equality where
"is_at_least_equality R ≡ ∀x y. R x y ⟶ x = y" for R
named_theorems is_at_least_equality
lemma [is_at_least_equality]:
"is_at_least_equality (=)"
by (simp add: is_at_least_equality_def)
lemma [is_at_least_equality]:
"is_at_least_equality R" if "is_equality R" for R
using that by (simp add: is_at_least_equality_def is_equality_def)
lemma [is_at_least_equality]:
"is_at_least_equality (eq_onp P)"
by (simp add: is_at_least_equality_def eq_onp_def)
lemma is_at_least_equality_list_all2[is_at_least_equality]:
"is_at_least_equality (list_all2 R)" if "is_at_least_equality R" for R
using that unfolding is_at_least_equality_def
by (auto simp: list.rel_eq dest: list_all2_mono[where Q = "(=)"])
lemma is_at_least_equality_rel_prod[is_at_least_equality]:
"is_at_least_equality (R1 ×⇩R R2)"
if "is_at_least_equality R1" "is_at_least_equality R2" for R1 R2
using that unfolding is_at_least_equality_def by auto
lemma is_at_least_equality_cong1:
"(S1 ===> (=)) f f" if "is_at_least_equality S1" "is_at_least_equality S2" for S1 f
using that unfolding is_at_least_equality_def by (intro rel_funI) auto
lemma is_at_least_equality_cong2:
"(S1 ===> S2 ===> (=)) f f" if "is_at_least_equality S1" "is_at_least_equality S2" for S1 S2 f
using that unfolding is_at_least_equality_def by (intro rel_funI) auto
lemma is_at_least_equality_cong3:
"(S1 ===> S2 ===> S3 ===> (=)) f f"
if "is_at_least_equality S1" "is_at_least_equality S2" "is_at_least_equality S3" for S1 S2 S3 f
using that unfolding is_at_least_equality_def by (intro rel_funI) force
lemma is_at_least_equality_Let:
"(S ===> ((=) ===> R) ===> R) Let Let" if "is_at_least_equality S" for R
using that unfolding is_at_least_equality_def
by (intro rel_funI) (erule Let_transfer[THEN rel_funD, THEN rel_funD, rotated], auto)
lemma map_transfer_length:
fixes R S n
shows
"((R ===> S)
===> (λx y. list_all2 R x y ∧ length x = n)
===> (λx y. list_all2 S x y ∧ length x = n))
map map"
apply (intro rel_funI conjI)
apply (erule list.map_transfer[THEN rel_funD, THEN rel_funD], erule conjunct1)
apply simp
done
lemma upt_0_transfer:
"(eq_onp (λx. x = 0) ===> eq_onp (λx. x = n) ===> list_all2 (eq_onp (λx. x < n))) upt upt" for n
apply (intro rel_funI upt_transfer_upper_bound[THEN rel_funD, THEN rel_funD])
apply (assumption | erule eq_onp_to_eq)+
done
lemma upt_length_transfer:
"(eq_onp (λx. x = 0) ===> eq_onp (λx. x = n)
===> (λ x y. list_all2 (eq_onp (λx. x < n)) x y ∧ length x = n)) upt upt" for n
apply (intro rel_funI conjI upt_0_transfer[THEN rel_funD, THEN rel_funD], assumption+)
apply (simp add: eq_onp_def)
done
lemma case_prod_transfer_strong:
fixes A B C
assumes "⋀ x y. A1 x y ⟹ A x y" "⋀ x y. B1 x y ⟹ B x y"
shows "((A ===> B ===> C) ===> A1 ×⇩R B1 ===> C) case_prod case_prod"
apply (intro rel_funI)
apply clarsimp
apply (drule assms)+
apply (drule (1) rel_funD)+
apply assumption
done
lemma concat_transfer_strong:
fixes A B C
assumes "⋀x y. A x y ⟹ B x y" "⋀ x y. C x y ⟹ list_all2 (list_all2 A) x y"
shows "(C ===> list_all2 B) concat concat"
apply (intro rel_funI concat_transfer[THEN rel_funD])
apply (drule assms)
apply (erule list_all2_mono)
apply (erule list_all2_mono)
apply (erule assms)
done
lemma map_transfer_strong:
fixes A B C
assumes "⋀xs ys. C xs ys ⟹ list_all2 A xs ys"
shows "((A ===> B) ===> C ===> list_all2 B) map map"
apply (intro rel_funI)
apply (erule list.map_transfer[THEN rel_funD, THEN rel_funD])
apply (erule assms)
done
lemma list_update_transfer':
fixes A :: "'a ⇒ 'b ⇒ bool"
shows "(list_all2 A ===> eq_onp (λi. i<n_ps) ===> A ===> list_all2 A) list_update list_update"
apply (intro rel_funI)
apply (rule list_update_transfer[THEN rel_funD, THEN rel_funD, THEN rel_funD])
apply (auto simp: eq_onp_def)
done
lemma list_update_transfer'':
fixes A :: "'a ⇒ 'b ⇒ bool" and n
shows "((λ x y. list_all2 A x y ∧ length x = n) ===> eq_onp (λi. i<n) ===> A
===> (λ x y. list_all2 A x y ∧ length x = n)) list_update list_update"
apply (intro rel_funI conjI)
subgoal
apply (erule conjE)
apply (rule List.list_update_transfer[THEN rel_funD, THEN rel_funD, THEN rel_funD])
apply (assumption | elim eq_onp_to_eq)+
done
apply simp
done
lemma list_update_transfer''':
fixes A :: "'a ⇒ 'b ⇒ bool" and n
shows "((λ x y. list_all2 A x y ∧ length x = n) ===> (=) ===> A
===> (λ x y. list_all2 A x y ∧ length x = n)) list_update list_update"
apply (intro rel_funI conjI)
subgoal
apply (erule conjE)
apply (rule List.list_update_transfer[THEN rel_funD, THEN rel_funD, THEN rel_funD])
apply (assumption | elim eq_onp_to_eq)+
done
apply simp
done
lemma fold_transfer_strong:
fixes A B
assumes "⋀x y. A1 x y ⟹ A x y" "⋀x y. B1 x y ⟹ B x y" "⋀x y. B x y ⟹ B2 x y"
"⋀x y. B x y ⟹ B3 x y"
shows "((A ===> B2 ===> B1) ===> list_all2 A1 ===> B ===> B3) fold fold"
apply (intro rel_funI, rule assms)
apply (rule fold_transfer[THEN rel_funD, THEN rel_funD, THEN rel_funD])
apply (intro rel_funI)
apply (drule rel_funD, erule assms)
apply (drule rel_funD, erule assms, erule assms)
apply assumption+
done
lemma bval_bvali_transfer[transfer_rule]:
"(state_rel ===> eq_onp valid_check ===> (=)) (λ s. bval (the o s)) bvali"
by (intro rel_funI) (auto simp: eq_onp_def valid_check_def state_rel_def intro!: bval_bvali)
lemma mk_upds_mk_updsi_transfer[transfer_rule]:
"(state_rel ===> list_all2 (eq_onp valid_upd) ===> state_rel) mk_upds mk_updsi"
apply (intro rel_funI)
subgoal for x y upds upds'
apply (subgoal_tac "upds' = upds")
apply simp
apply (rule mk_upds_mk_updsi)
apply assumption
subgoal
by (smt (z3) case_prodI2 case_prod_conv eq_onp_def list_all2_same valid_upd_def)
subgoal
by (smt (z3) case_prodE case_prod_conv eq_onp_def list_all2_same valid_upd_def)
subgoal
by (metis eq_onp_to_eq list.rel_eq_onp)
done
done
lemma check_bounded_transfer[transfer_rule]:
"(state_rel ===> (=)) check_bounded check_boundedi"
by (simp add: check_bounded_check_boundedi rel_funI)
lemma trans_map_transfer:
"(eq_onp (λi. i<n_ps) ===> (=) ===>
list_all2 (
eq_onp valid_check ×⇩R (=) ×⇩R eq_onp (pred_act (λx. x < num_actions))
×⇩R list_all2 (eq_onp valid_upd) ×⇩R (=)
)) trans_map trans_map"
apply (intro rel_funI, simp add: eq_onp_def, intro list.rel_refl_strong)
apply clarsimp
apply (auto 4 4 dest!: trans_mapD dest: action_setD var_setD var_setD2 intro: list.rel_refl_strong
simp: valid_upd_def valid_check_def
)
done
lemma trans_map_transfer':
"(eq_onp (λi. i<n_ps) ===> (=) ===>
list_all2 (eq_onp valid_check ×⇩R (=) ×⇩R (=) ×⇩R list_all2 (eq_onp valid_upd) ×⇩R (=))
) trans_map trans_map"
apply (intro rel_funI, simp add: eq_onp_def, intro list.rel_refl_strong)
apply clarsimp
apply (intro conjI list.rel_refl_strong)
apply (auto 4 4 dest: var_setD trans_mapD var_setD2 simp: valid_upd_def valid_check_def)
done
lemma map_filter_transfer[transfer_rule]:
"((S ===> rel_option R) ===> list_all2 S ===> list_all2 R) List.map_filter List.map_filter"
unfolding map_filter_def
apply (clarsimp intro!: rel_funI)
subgoal for f g xs ys
apply (rule list.map_transfer[THEN rel_funD, THEN rel_funD, of "λ x y. f x ≠ None ∧ S x y"])
apply (rule rel_funI)
subgoal for a b
apply (cases "f a")
apply (auto simp: option_rel_Some1 option_rel_Some2 dest!: rel_funD)
done
subgoal
apply rotate_tac
apply (induction rule: list_all2_induct)
apply (auto dest: rel_funD)
done
done
done
lemma trans_i_map_transfer[transfer_rule]:
"(eq_onp (λi. i<n_ps) ===> (=) ===>
list_all2 (eq_onp valid_check ×⇩R (=) ×⇩R (=) ×⇩R list_all2 (eq_onp valid_upd) ×⇩R (=))
) trans_i_map trans_i_map"
supply [transfer_rule] = trans_map_transfer'
unfolding trans_i_map_def by transfer_prover
lemma int_trans_from_loc_transfer[transfer_rule]:
"(eq_onp (λi. i<n_ps) ===> (=) ===> (λx y. list_all2 (=) x y ∧ length x = n_ps) ===> state_rel
===> list_all2((=) ×⇩R (=) ×⇩R (=) ×⇩R (λx y. list_all2 (=) x y ∧ length x = n_ps) ×⇩R state_rel))
int_trans_from_loc int_trans_from_loc_impl"
supply [transfer_rule] = list_update_transfer''
unfolding int_trans_from_loc_def int_trans_from_loc_impl_def Let_def by transfer_prover
lemma n_ps_transfer:
"eq_onp (λx. x = n_ps) n_ps n_ps"
by (simp add: eq_onp_def)
lemma zero_nat_transfer:
"(=) 0 (0::nat)"
..
lemma int_trans_from_all_transfer[transfer_rule]:
"((λx y. list_all2 (=) x y ∧ length x = n_ps) ===> state_rel
===> list_all2((=) ×⇩R (=) ×⇩R (=) ×⇩R (λx y. list_all2 (=) x y ∧ length x = n_ps) ×⇩R state_rel))
int_trans_from_all int_trans_from_all_impl"
supply [transfer_rule] = zero_nat_transfer n_ps_transfer
unfolding int_trans_from_all_def int_trans_from_all_impl_def Let_def
by transfer_prover
lemma int_trans_from_vec_transfer[transfer_rule]:
"(list_all2 (eq_onp (λx. x < n_ps) ×⇩R (=)) ===> (λx y. list_all2 (=) x y ∧ length x = n_ps)
===> state_rel
===> list_all2((=) ×⇩R (=) ×⇩R (=) ×⇩R (λx y. list_all2 (=) x y ∧ length x = n_ps) ×⇩R state_rel))
int_trans_from_vec int_trans_from_vec_impl"
unfolding int_trans_from_vec_def int_trans_from_vec_impl_def Let_def
by transfer_prover
private definition R where "R ≡ (λx y. list_all2 (=) x y ∧ length x = n_ps)"
lemma get_committed_transfer[transfer_rule]:
"((λx y. list_all2 (=) x y ∧ length x = n_ps) ===> list_all2 (eq_onp (λx. x < n_ps) ×⇩R (=)))
get_committed get_committed"
proof -
have [transfer_rule]:
"R automata automata"
unfolding R_def by (simp add: n_ps_def list.rel_eq)
show ?thesis
supply [transfer_rule] = zero_nat_transfer n_ps_transfer
unfolding get_committed_def
unfolding Let_def
apply transfer_prover_start
using [[goals_limit=15]]
prefer 8
apply transfer_step
prefer 8
unfolding R_def
apply transfer_step+
apply transfer_prover
done
qed
lemma eq_transfer:
"(list_all2 (eq_onp (λx. x < n_ps) ×⇩R (=)) ===> list_all2 (=) ===> (=)) (=) (=)"
unfolding eq_onp_def
apply (intro rel_funI)
apply (drule list_all2_mono[where Q = "(=)"])
apply (auto simp add: list.rel_eq rel_prod.simps)
done
lemma int_trans_from_transfer:
"((λx y. list_all2 (=) x y ∧ length x = n_ps) ×⇩R state_rel
===> list_all2 ((=) ×⇩R (=) ×⇩R (=) ×⇩R ((λx y. list_all2 (=) x y ∧ length x = n_ps) ×⇩R state_rel)))
int_trans_from int_trans_impl"
supply [transfer_rule] = eq_transfer
unfolding int_trans_impl_def int_trans_from_def Let_def
by transfer_prover
lemma pairs_by_action_transfer[transfer_rule]:
"((λx y. list_all2 (=) x y ∧ length x = n) ===> state_rel ===>
list_all2 ((=) ×⇩R eq_onp valid_check ×⇩R (=) ×⇩R (=) ×⇩R list_all2 (eq_onp valid_upd) ×⇩R (=) ×⇩R (=))
===>
list_all2 ((=) ×⇩R eq_onp valid_check ×⇩R (=) ×⇩R (=) ×⇩R list_all2 (eq_onp valid_upd) ×⇩R (=) ×⇩R (=))
===>
list_all2 ((=) ×⇩R (=) ×⇩R (=) ×⇩R (λx y. list_all2 (=) x y ∧ length x = n) ×⇩R state_rel))
pairs_by_action pairs_by_action_impl"
supply [transfer_rule] = list_update_transfer'''
unfolding pairs_by_action_def pairs_by_action_impl_def by transfer_prover
lemmas rel_elims =
rel_prod.cases
rel_funD
lemmas rel_intros =
rel_funI
lemma pairs_by_action_transfer':
"((λx y. list_all2 (=) x y ∧ length x = n) ===> state_rel ===>
list_all2 (B ×⇩R eq_onp valid_check ×⇩R C ×⇩R D ×⇩R list_all2 (eq_onp valid_upd) ×⇩R E ×⇩R F) ===>
list_all2 (B ×⇩R eq_onp valid_check ×⇩R C ×⇩R D ×⇩R list_all2 (eq_onp valid_upd) ×⇩R E ×⇩R F) ===>
list_all2 ((=) ×⇩R (=) ×⇩R (=) ×⇩R (λx y. list_all2 (=) x y ∧ length x = n) ×⇩R state_rel))
pairs_by_action pairs_by_action_impl"
if "⋀x y. B x y ⟹ x = y"
"⋀x y. C x y ⟹ x = y" "⋀x y. D x y ⟹ x = y"
"⋀x y. E x y ⟹ x = y" "⋀x y. F x y ⟹ x = y"
for B C D E F
apply (intro rel_funI)
apply (rule pairs_by_action_transfer[THEN rel_funD, THEN rel_funD, THEN rel_funD, THEN rel_funD])
apply (assumption | erule that list_all2_mono prod.rel_mono_strong)+
done
lemma trans_in_map_transfer[transfer_rule]:
"(eq_onp (λi. i<n_ps) ===> (=)
===> list_all2 (
eq_onp valid_check ×⇩R (=) ×⇩R eq_onp (λa. a < num_actions) ×⇩R list_all2 (eq_onp valid_upd) ×⇩R (=))
) trans_in_map trans_in_map"
supply [transfer_rule] = trans_map_transfer[folded act.rel_eq_onp]
unfolding trans_in_map_def by transfer_prover
lemma trans_in_map_transfer[transfer_rule]:
"(eq_onp (λi. i<n_ps) ===> (=)
===> list_all2 (eq_onp valid_check ×⇩R (=) ×⇩R (=) ×⇩R list_all2 (eq_onp valid_upd) ×⇩R (=))
) trans_in_map trans_in_map"
unfolding trans_in_map_def oops
lemma trans_out_map_transfer[transfer_rule]:
"(eq_onp (λi. i<n_ps) ===> (=)
===> list_all2 (
eq_onp valid_check ×⇩R (=) ×⇩R eq_onp (λa. a < num_actions) ×⇩R list_all2 (eq_onp valid_upd) ×⇩R (=)
)) trans_out_map trans_out_map"
supply [transfer_rule] = trans_map_transfer[folded act.rel_eq_onp]
unfolding trans_out_map_def by transfer_prover
lemma trans_out_map_transfer[transfer_rule]:
"(eq_onp (λi. i<n_ps) ===> (=) ===> list_all2 (
eq_onp valid_check ×⇩R (=) ×⇩R (=) ×⇩R list_all2 (eq_onp valid_upd) ×⇩R (=)))
trans_out_map trans_out_map"
unfolding trans_out_map_def oops
lemma actions_by_state_transfer[transfer_rule]:
"(eq_onp (λi. i < n_ps) ===>
list_all2 ((=) ×⇩R (=) ×⇩R eq_onp (λi. i < n) ×⇩R (=)) ===>
(λ x y. list_all2 (list_all2 (eq_onp (λi. i<n_ps) ×⇩R (=) ×⇩R (=) ×⇩R eq_onp (λx. x < n) ×⇩R (=))) x y ∧ length x = n) ===>
(λ x y. list_all2 (list_all2 (eq_onp (λi. i<n_ps) ×⇩R (=) ×⇩R (=) ×⇩R eq_onp (λx. x < n) ×⇩R (=))) x y ∧ length x = n)
)
actions_by_state actions_by_state" for n
supply [transfer_rule] = list_update_transfer''
unfolding actions_by_state_def by transfer_prover
lemma actions_by_state_transfer'[transfer_rule]:
"(
eq_onp (λi. i < n_ps) ===>
list_all2 (eq_onp valid_check ×⇩R (=) ×⇩R eq_onp (λi. i < n) ×⇩R list_all2 (eq_onp valid_upd) ×⇩R (=)) ===>
(λ x y. list_all2 (list_all2 (
eq_onp (λi. i<n_ps) ×⇩R eq_onp valid_check ×⇩R (=) ×⇩R eq_onp (λx. x < n)
×⇩R list_all2 (eq_onp valid_upd) ×⇩R (=))) x y ∧ length x = n) ===>
(λ x y. list_all2 (list_all2 (
eq_onp (λi. i<n_ps) ×⇩R eq_onp valid_check ×⇩R (=) ×⇩R eq_onp (λx. x < n)
×⇩R list_all2 (eq_onp valid_upd) ×⇩R (=))) x y ∧ length x = n)
)
actions_by_state actions_by_state"
for n
supply [transfer_rule] = list_update_transfer''
unfolding actions_by_state_def by transfer_prover
lemma transfer_consts:
"(eq_onp (λx. x = num_actions)) num_actions num_actions" "(eq_onp (λx. x = 0)) (0::nat) 0"
"(eq_onp (λx. x = n_ps)) n_ps n_ps"
by (auto simp: eq_onp_def)
lemma all_actions_by_state_transfer[transfer_rule]:
"
(
(eq_onp (λi. i<n_ps) ===> (=) ===> list_all2 (eq_onp valid_check ×⇩R (=) ×⇩R eq_onp (λi. i < num_actions) ×⇩R list_all2 (eq_onp valid_upd) ×⇩R (=)))
===>
(λx y. list_all2 (=) x y ∧ length x = n_ps)
===>
(λ x y. list_all2 (list_all2 (eq_onp (λi. i<n_ps) ×⇩R eq_onp valid_check ×⇩R (=) ×⇩R eq_onp (λi. i<num_actions) ×⇩R list_all2 (eq_onp valid_upd) ×⇩R (=))) x y ∧ length x = num_actions)
)
all_actions_by_state all_actions_by_state"
supply [transfer_rule] = map_transfer_length upt_0_transfer upt_length_transfer transfer_consts
n_ps_transfer
unfolding all_actions_by_state_def by transfer_prover
lemma all_actions_from_vec_transfer[transfer_rule]:
"
(
(eq_onp (λi. i<n_ps) ===> (=) ===> list_all2 (eq_onp valid_check ×⇩R (=) ×⇩R eq_onp (λi. i < num_actions) ×⇩R list_all2 (eq_onp valid_upd) ×⇩R (=)))
===>
list_all2 (eq_onp (λi. i < n_ps) ×⇩R (=))
===>
(λ x y. list_all2 (list_all2 (eq_onp (λi. i<n_ps) ×⇩R eq_onp valid_check ×⇩R (=) ×⇩R eq_onp (λi. i<num_actions) ×⇩R list_all2 (eq_onp valid_upd) ×⇩R (=))) x y ∧ length x = num_actions)
)
all_actions_from_vec all_actions_from_vec"
supply [transfer_rule] = map_transfer_length upt_length_transfer transfer_consts
unfolding all_actions_from_vec_def all_actions_from_vec_def by transfer_prover
lemma bin_actions_transfer[transfer_rule]:
"(list_all2 (eq_onp (λx. x < num_actions))) bin_actions bin_actions"
proof -
have *: "list_all2 (eq_onp (λx. x < num_actions)) [0..<num_actions] [0..<num_actions]"
by (rule list.rel_refl_strong) (auto simp: eq_onp_def)
show ?thesis
unfolding bin_actions_def
by (rule filter_transfer[THEN rel_funD, THEN rel_funD, OF _ *]) (auto simp: eq_onp_def)
qed
lemma Let_transfer_bin_aux:
"((λx y. list_all2 (list_all2
(eq_onp (λi. i < n_ps) ×⇩R eq_onp valid_check ×⇩R list_all2 (rel_acconstraint (=) (=)) ×⇩R
eq_onp (λi. i < num_actions) ×⇩R list_all2 (eq_onp valid_upd) ×⇩R list_all2 (=) ×⇩R (=))) x y
∧ length x = num_actions) ===>
((λx y. list_all2 (list_all2
((=) ×⇩R eq_onp valid_check ×⇩R list_all2 (rel_acconstraint (=) (=)) ×⇩R
(=) ×⇩R list_all2 (eq_onp valid_upd) ×⇩R list_all2 (=) ×⇩R (=))) x y
∧ length x = num_actions) ===>
list_all2
(list_all2 (rel_acconstraint (=) (=)) ×⇩R rel_label (=) ×⇩R
list_all2 (=) ×⇩R (λx y. list_all2 (=) x y ∧ length x = n_ps) ×⇩R state_rel)) ===>
list_all2
(list_all2 (rel_acconstraint (=) (=)) ×⇩R rel_label (=) ×⇩R
list_all2 (=) ×⇩R (λx y. list_all2 (=) x y ∧ length x = n_ps) ×⇩R state_rel))
Let Let"
unfolding Let_def
by (intro rel_funI, drule rel_funD)
(auto simp: eq_onp_def elim!: list_all2_mono prod.rel_mono_strong)
lemma bin_trans_from_transfer:
"((λx y. list_all2 (=) x y ∧ length x = n_ps) ×⇩R state_rel
===> list_all2 ((=) ×⇩R (=) ×⇩R (=) ×⇩R ((λx y. list_all2 (=) x y ∧ length x = n_ps) ×⇩R state_rel)))
bin_trans_from bin_trans_from_impl"
unfolding bin_trans_from_impl_def bin_trans_from_def
supply [transfer_rule] =
map_transfer_length upt_length_transfer transfer_consts eq_transfer Let_transfer_bin_aux
by transfer_prover
lemma trans_map_transfer'':
"((=) ===> (=) ===>
list_all2 (eq_onp valid_check ×⇩R (=) ×⇩R eq_onp (pred_act (λx. x < num_actions)) ×⇩R list_all2 (eq_onp valid_upd) ×⇩R (=)))
trans_map trans_map"
apply (intro rel_funI, simp add: eq_onp_def, intro list.rel_refl_strong)
apply clarsimp
apply (auto 4 4 dest!: trans_mapD dest: action_setD var_setD intro: list.rel_refl_strong simp: valid_upd_def)
oops
lemma compute_upds_transfer:
"(
(list_all2 (=) ×⇩R (=) ×⇩R list_all2 (=) ×⇩R (λx y. list_all2 (=) x y ∧ length x = n) ×⇩R state_rel)
===> list_all2 (list_all2
((=) ×⇩R eq_onp valid_check ×⇩R list_all2 (=) ×⇩R (=) ×⇩R list_all2 (eq_onp valid_upd)
×⇩R list_all2 (=) ×⇩R (=))) ===>
list_all2 (
list_all2 (=) ×⇩R (=) ×⇩R list_all2 (=) ×⇩R (λx y. list_all2 (=) x y ∧ length x = n) ×⇩R state_rel
)) compute_upds compute_upds_impl"
supply [transfer_rule] = list_update_transfer'''
unfolding compute_upds_def compute_upds_impl_def by transfer_prover
lemma in_transfer:
"(eq_onp (λx. x < num_actions) ===> (=) ===> (=)) (∈) (∈)"
by (intro rel_funI, rule member_transfer[of "(=)", THEN rel_funD, THEN rel_funD])
(auto simp: eq_onp_def rel_set_eq intro: bi_unique_eq)
lemma trans_in_broad_map_transfer[transfer_rule]:
"(eq_onp (λi. i<n_ps) ===> (=) ===> list_all2 (eq_onp valid_check ×⇩R (=) ×⇩R eq_onp (λx. x < num_actions) ×⇩R list_all2 (eq_onp valid_upd) ×⇩R (=)))
trans_in_broad_map trans_in_broad_map"
supply [transfer_rule] = trans_map_transfer[folded act.rel_eq_onp] in_transfer
unfolding trans_in_broad_map_def by transfer_prover
lemma trans_out_broad_map_transfer[transfer_rule]:
"(eq_onp (λi. i<n_ps) ===> (=) ===> list_all2 (eq_onp valid_check ×⇩R (=) ×⇩R eq_onp (λx. x < num_actions) ×⇩R list_all2 (eq_onp valid_upd) ×⇩R (=)))
trans_out_broad_map trans_out_broad_map"
supply [transfer_rule] = trans_map_transfer[folded act.rel_eq_onp] in_transfer
unfolding trans_out_broad_map_def by transfer_prover
text ‹We are using the ``equality version'' of parametricty for @{term "(!)"} here.›
lemma actions_by_state'_transfer[transfer_rule]:
"(list_all2 (eq_onp valid_check ×⇩R (=) ×⇩R eq_onp (λx. x < num_actions) ×⇩R list_all2 (eq_onp valid_upd) ×⇩R (=))
===> (λ x y. list_all2 (
list_all2 (eq_onp valid_check ×⇩R (=) ×⇩R eq_onp (λx. x < num_actions) ×⇩R list_all2 (eq_onp valid_upd) ×⇩R (=))) x y
∧ length x = num_actions
))
actions_by_state' actions_by_state'"
supply [transfer_rule] = transfer_consts
upt_length_transfer
map_transfer_length
list_update_transfer''
unfolding actions_by_state'_def by transfer_prover
lemma trans_in_broad_grouped_transfer[transfer_rule]:
"(eq_onp (λi. i<n_ps) ===> (=)
===> (λ x y. list_all2 (
list_all2 (eq_onp valid_check ×⇩R (=) ×⇩R eq_onp (λx. x < num_actions) ×⇩R list_all2 (eq_onp valid_upd) ×⇩R (=))) x y
∧ length x = num_actions
)) trans_in_broad_grouped trans_in_broad_grouped"
unfolding trans_in_broad_grouped_def by transfer_prover
lemma trans_out_broad_grouped_transfer[transfer_rule]:
"(eq_onp (λi. i<n_ps) ===> (=)
===> (λ x y. list_all2 (
list_all2 (eq_onp valid_check ×⇩R (=) ×⇩R eq_onp (λx. x < num_actions) ×⇩R list_all2 (eq_onp valid_upd) ×⇩R (=))) x y
∧ length x = num_actions
)) trans_out_broad_grouped trans_out_broad_grouped"
unfolding trans_out_broad_grouped_def by transfer_prover
lemma make_combs_transfer:
fixes R
assumes "⋀x y. R x y ⟹ x = y"
shows
"(eq_onp (λx. x < n_ps)
===> eq_onp (λx. x < num_actions)
===> (λx y. list_all2 (λx y. list_all2 (list_all2 R) x y ∧ length x = num_actions) x y
∧ length x = n_ps)
===> list_all2 (list_all2 (eq_onp (λx. x < n_ps) ×⇩R R)))
make_combs make_combs"
proof -
have [transfer_rule]:
"(eq_onp (λx. x < n_ps) ===> eq_onp (λx. x < n_ps) ===> (=)) (=) (=)"
"(list_all2 R ===> list_all2 R ===> (=)) (=) (=)"
"(list_all2 (list_all2 (eq_onp (λx. x < n_ps) ×⇩R R))
===> list_all2 (list_all2 (eq_onp (λx. x < n_ps) ×⇩R R)) ===> (=)) (=) (=)"
apply (simp_all add: eq_onp_def)
subgoal
by (smt (z3) assms list.rel_eq list_all2_mono rel_funI)
subgoal
by (smt (z3) assms fun.rel_eq list_all2_eq list_all2_mono rel_fun_mono rel_prod.cases)
subgoal
by (smt (z3) assms fun.rel_eq list_all2_eq list_all2_mono rel_fun_mono rel_prod.cases)
done
show ?thesis
supply [transfer_rule] = upt_0_transfer transfer_consts
unfolding make_combs_def by transfer_prover
qed
lemma broad_trans_from_alt_def2:
"broad_trans_from = (λ(L, s).
let
pairs = get_committed L;
In = map (λp. trans_in_broad_grouped p (L ! p)) [0..<n_ps];
Out = map (λp. trans_out_broad_grouped p (L ! p)) [0..<n_ps];
In = map (map (filter (λ(b, _). bval (the ∘ s) b))) In;
Out = map (map (filter (λ(b, _). bval (the ∘ s) b))) Out
in
if pairs = [] then
concat (
map (λa.
concat (map (λp.
let
outs = Out ! p ! a
in if outs = [] then []
else
let
combs = make_combs p a In;
outs = map (λt. (p, t)) outs;
combs = (
if combs = [] then [[x]. x ← outs]
else concat (map (λx. map (λxs. x # xs) combs) outs));
init = ([], Broad a, [], (L, s))
in
compute_upds init combs
)
[0..<n_ps])
)
[0..<num_actions])
else
concat (
map (λa.
let
ins_committed =
List.map_filter (λ(p, _). if In ! p ! a ≠ [] then Some p else None) pairs;
always_committed = (length ins_committed > 1)
in
concat (map (λp.
let
outs = Out ! p ! a
in if outs = [] then []
else if
¬ always_committed ∧ (ins_committed = [p] ∨ ins_committed = [])
∧ ¬ list_ex (λ (q, _). q = p) pairs
then []
else
let
combs = make_combs p a In;
outs = map (λt. (p, t)) outs;
combs = (
if combs = [] then [[x]. x ← outs]
else concat (map (λx. map (λxs. x # xs) combs) outs));
init = ([], Broad a, [], (L, s))
in
compute_upds init combs
)
[0..<n_ps])
)
[0..<num_actions])
)
"
unfolding broad_trans_from_def compute_upds_def
apply (rule HOL.refl)
done
lemma concat_length_transfer:
"((λ x y. list_all2 (list_all2 A) x y ∧ length x = n) ===> list_all2 A) concat concat" for A n
by (intro rel_funI concat_transfer[THEN rel_funD], elim conjunct1)
lemma broad_trans_from_transfer:
"((λx y. list_all2 (=) x y ∧ length x = n_ps) ×⇩R state_rel
===> list_all2 ((=) ×⇩R (=) ×⇩R (=) ×⇩R ((λx y. list_all2 (=) x y ∧ length x = n_ps) ×⇩R state_rel)))
broad_trans_from broad_trans_from_impl"
proof -
have compute_upds_impl_transfer[transfer_rule]: "
(list_all2 (=) ×⇩R
rel_label (eq_onp (λx. x < num_actions)) ×⇩R
list_all2 (=) ×⇩R
(λx y. list_all2 (=) x y ∧ length x = n_ps) ×⇩R state_rel ===>
list_all2
(list_all2
(eq_onp (λx. x < n_ps) ×⇩R
eq_onp valid_check ×⇩R
list_all2 (rel_acconstraint (=) (=)) ×⇩R
eq_onp (λx. x < num_actions) ×⇩R
list_all2 (eq_onp valid_upd) ×⇩R list_all2 (=) ×⇩R (=))) ===>
list_all2
(list_all2 (=) ×⇩R
(=) ×⇩R
list_all2 (=) ×⇩R (λx y. list_all2 (=) x y ∧ length x = n_ps) ×⇩R state_rel))
compute_upds compute_upds_impl"
apply (intro rel_funI)
apply (rule compute_upds_transfer[THEN rel_funD, THEN rel_funD])
apply (elim rel_prod.cases)
apply (simp only:)
apply (intro rel_prod.intros)
apply assumption
subgoal
by (drule label.rel_mono_strong[of _ _ _ "(=)"]; simp add: eq_onp_def label.rel_eq)
apply (simp; fail)+
apply (elim list_all2_mono rel_prod.cases)
apply (simp only:)
apply (intro rel_prod.intros)
apply (assumption | simp add: eq_onp_def acconstraint.rel_eq)+
done
have [is_at_least_equality]: "is_equality (rel_acconstraint (=) (=))"
by (tactic ‹Transfer.eq_tac @{context} 1›)
have eq_transfer1:
"(list_all2
(eq_onp valid_check ×⇩R list_all2 (rel_acconstraint (=) (=)) ×⇩R eq_onp (λx. x < num_actions) ×⇩R
list_all2 (eq_onp valid_upd) ×⇩R list_all2 (=) ×⇩R (=)) ===>
list_all2
(eq_onp valid_check ×⇩R list_all2 (rel_acconstraint (=) (=)) ×⇩R eq_onp (λx. x < num_actions) ×⇩R
list_all2 (eq_onp valid_upd) ×⇩R list_all2 (=) ×⇩R (=))
===> (=)) (=) (=)
"
by (intro is_at_least_equality_cong2 is_at_least_equality)
let ?R = "(eq_onp (λx. x < n_ps) ×⇩R eq_onp valid_check ×⇩R
list_all2 (rel_acconstraint (=) (=)) ×⇩R
eq_onp (λx. x < num_actions) ×⇩R list_all2 (eq_onp valid_upd) ×⇩R list_all2 (=) ×⇩R (=))"
have eq_transfer5:
"(list_all2 (list_all2 ?R) ===> list_all2 (list_all2 ?R) ===> (=)) (=) (=)"
by (intro is_at_least_equality_cong2 is_at_least_equality)
have eq_transfer2:
"(list_all2 (eq_onp (λx. x < n_ps)) ===> list_all2 (eq_onp (λx. x < n_ps)) ===> (=)) (=) (=)"
by (intro is_at_least_equality_cong2 is_at_least_equality)
have eq_transfer3:
"(eq_onp (λx. x < n_ps) ===> eq_onp (λx. x < n_ps) ===> (=)) (=) (=)"
by (intro is_at_least_equality_cong2 is_at_least_equality)
have eq_transfer4:
"(list_all2 (eq_onp (λx. x < n_ps) ×⇩R (=)) ===>
list_all2 (eq_onp (λx. x < n_ps) ×⇩R (=)) ===> (=)) (=) (=)"
by (intro is_at_least_equality_cong2 is_at_least_equality)
have make_combs_transfer: "
(eq_onp (λx. x < n_ps) ===>
eq_onp (λx. x < num_actions) ===>
(λx y. list_all2 (λx y. list_all2 (list_all2
(eq_onp valid_check ×⇩R list_all2 (rel_acconstraint (=) (=)) ×⇩R eq_onp (λx. x < num_actions) ×⇩R
list_all2 (eq_onp valid_upd) ×⇩R list_all2 (=) ×⇩R (=)))
x y ∧ length x = num_actions) x y ∧ length x = n_ps) ===>
list_all2 (list_all2 (eq_onp (λx. x < n_ps) ×⇩R
eq_onp valid_check ×⇩R list_all2 (rel_acconstraint (=) (=)) ×⇩R eq_onp (λx. x < num_actions) ×⇩R
list_all2 (eq_onp valid_upd) ×⇩R list_all2 (=) ×⇩R (=))
)
) make_combs make_combs"
apply (intro rel_funI)
apply (rule make_combs_transfer[THEN rel_funD, THEN rel_funD, THEN rel_funD])
subgoal
apply (simp add: acconstraint.rel_eq list.rel_eq prod.rel_eq)
apply (drule prod.rel_mono_strong[of _ _ _ _ "(=)" "(=)"], erule eq_onp_to_eq)
apply (drule prod.rel_mono_strong[of _ _ _ _ "(=)" "(=)"])
apply assumption
apply (drule prod.rel_mono_strong[of _ _ _ _ "(=)" "(=)"], erule eq_onp_to_eq)
apply (drule prod.rel_mono_strong[of _ _ _ _ "(=)" "(=)"])
apply (drule list_all2_mono[of _ _ _ "(=)"], erule eq_onp_to_eq, simp only: list.rel_eq)
apply assumption
apply (drule (2) prod.rel_mono_strong[of _ _ _ _ "(=)" "(=)"];
simp add: acconstraint.rel_eq list.rel_eq prod.rel_eq)+
done
apply (simp add: prod.rel_eq)+
done
have "
((λx y. list_all2 (=) x y ∧ length x = n_ps) ×⇩R state_rel
===> list_all2 (
(=) ×⇩R (=) ×⇩R (=) ×⇩R ((λx y. list_all2 (=) x y ∧ length x = n_ps) ×⇩R state_rel)))
(
λ(L, s).
let
pairs = [];
In = map (λp. trans_in_broad_grouped p (L ! p)) [0..<n_ps];
Out = map (λp. trans_out_broad_grouped p (L ! p)) [0..<n_ps]
in
concat (
map (λa.
concat (map (λp.
let
outs = Out ! p ! a
in if outs = [] then []
else
let
combs = make_combs p a In;
outs = map (λt. (p, t)) outs;
combs = (
if combs = [] then [[x]. x ← outs]
else concat (map (λx. map (λxs. x # xs) combs) outs));
init = ([], Broad a, [], (L, s))
in
compute_upds init combs
)
[0..<n_ps])
)
[0..<num_actions])
) (
λ(L, s).
let
pairs = [];
In = map (λp. trans_in_broad_grouped p (L ! p)) [0..<n_ps];
Out = map (λp. trans_out_broad_grouped p (L ! p)) [0..<n_ps]
in
concat (
map (λa.
concat (map (λp.
let
outs = Out ! p ! a
in if outs = [] then []
else
let
combs = make_combs p a In;
outs = map (λt. (p, t)) outs;
combs = (
if combs = [] then [[x]. x ← outs]
else concat (map (λx. map (λxs. x # xs) combs) outs));
init = ([], Broad a, [], (L, s))
in
compute_upds_impl init combs
)
[0..<n_ps])
)
[0..<num_actions]))
"
supply [transfer_rule] =
transfer_consts
upt_0_transfer
map_transfer_length
upt_length_transfer
make_combs_transfer
compute_upds_transfer
concat_length_transfer
eq_transfer1
eq_transfer2
eq_transfer3
eq_transfer5
unfolding Let_def by transfer_prover
have "
((λx y. list_all2 (=) x y ∧ length x = n_ps) ×⇩R state_rel
===> list_all2 (
(=) ×⇩R (=) ×⇩R (=) ×⇩R ((λx y. list_all2 (=) x y ∧ length x = n_ps) ×⇩R state_rel)))
(
λ(L, s).
let
pairs = get_committed L;
In = map (λp. trans_in_broad_grouped p (L ! p)) [0..<n_ps];
Out = map (λp. trans_out_broad_grouped p (L ! p)) [0..<n_ps]
in
concat (
map (λa.
let
ins_committed =
List.map_filter (λ(p, _). if In ! p ! a ≠ [] then Some p else None) pairs;
always_committed = (length ins_committed > 1)
in
concat (map (λp.
let
outs = Out ! p ! a
in if outs = [] then []
else if
¬ always_committed ∧ (ins_committed = [p] ∨ ins_committed = [])
∧ ¬ list_ex (λ (q, _). q = p) pairs
then []
else
let
combs = make_combs p a In;
outs = map (λt. (p, t)) outs;
combs = (
if combs = [] then [[x]. x ← outs]
else concat (map (λx. map (λxs. x # xs) combs) outs));
init = ([], Broad a, [], (L, s))
in
compute_upds init combs
)
[0..<n_ps])
)
[0..<num_actions])
)
(
λ(L, s).
let
pairs = get_committed L;
In = map (λp. trans_in_broad_grouped p (L ! p)) [0..<n_ps];
Out = map (λp. trans_out_broad_grouped p (L ! p)) [0..<n_ps]
in
concat (
map (λa.
let
ins_committed =
List.map_filter (λ(p, _). if In ! p ! a ≠ [] then Some p else None) pairs;
always_committed = (length ins_committed > 1)
in
concat (map (λp.
let
outs = Out ! p ! a
in if outs = [] then []
else if
¬ always_committed ∧ (ins_committed = [p] ∨ ins_committed = [])
∧ ¬ list_ex (λ (q, _). q = p) pairs
then []
else
let
combs = make_combs p a In;
outs = map (λt. (p, t)) outs;
combs = (
if combs = [] then [[x]. x ← outs]
else concat (map (λx. map (λxs. x # xs) combs) outs));
init = ([], Broad a, [], (L, s))
in
compute_upds_impl init combs
)
[0..<n_ps])
)
[0..<num_actions])
)"
supply [transfer_rule] =
transfer_consts
upt_0_transfer
map_transfer_length
upt_length_transfer
make_combs_transfer
compute_upds_transfer
concat_length_transfer
eq_transfer1
eq_transfer2
eq_transfer3
eq_transfer5
unfolding Let_def by transfer_prover
show ?thesis
supply [transfer_rule] =
transfer_consts
upt_0_transfer
map_transfer_length
upt_length_transfer
make_combs_transfer
compute_upds_transfer
concat_length_transfer
eq_transfer1
eq_transfer2
eq_transfer3
eq_transfer4
eq_transfer5
unfolding broad_trans_from_alt_def2 broad_trans_from_impl_def Let_def by transfer_prover
qed
lemma trans_from_transfer:
"((λx y. list_all2 (=) x y ∧ length x = n_ps) ×⇩R state_rel
===> list_all2 ((=) ×⇩R (=) ×⇩R (=) ×⇩R ((λx y. list_all2 (=) x y ∧ length x = n_ps) ×⇩R state_rel)))
trans_from trans_impl"
supply [transfer_rule] = int_trans_from_transfer bin_trans_from_transfer broad_trans_from_transfer
unfolding trans_from_def trans_impl_def by transfer_prover
lemma list_all2_swap:
"list_all2 S ys xs" if "list_all2 R xs ys" "S = (λx y. R y x)" for R S
using list_all2_swap that by blast
lemma swap_rel_prod: "(λ x y. (R ×⇩R S) y x) = (λx y. R y x) ×⇩R (λx y. S y x)" for R S
by (intro ext) auto
lemma swap_eq:
"(λx y. y = x) = (=)"
by auto
lemma trans_from_refine:
"(trans_impl, trans_from) ∈ fun_rel_syn loc_rel (list_rel (Id ×⇩r Id ×⇩r Id ×⇩r loc_rel))"
proof -
have [rel2p]:
"rel2p loc_rel = (λ x y. ((λx y. list_all2 (=) x y ∧ length x = n_ps) ×⇩R state_rel) y x)"
unfolding loc_rel_def rel2p_def by (intro ext) (auto simp: list.rel_eq)
have "rel2p (fun_rel_syn
{((L', s'), L, s) |L s L' s'. L' = L ∧ length L = n_ps ∧ state_rel s s'}
(⟨Id ×⇩r Id ×⇩r Id ×⇩r loc_rel⟩list_rel))
trans_impl trans_from"
unfolding rel2p rel2p_def state_rel_def
by (intro rel_funI trans_from_transfer[THEN rel_funD, THEN list_all2_swap])
(auto simp: list.rel_eq state_rel_def swap_rel_prod swap_eq)
then show ?thesis
unfolding rel2p_def relAPP_def loc_rel_def .
qed
lemma trans_from_correct:
"(trans_from, trans_prod) ∈ transition_rel states'"
using int_trans_from_correct bin_trans_from_correct broad_trans_from_correct
unfolding trans_from_def trans_prod_def transition_rel_def by auto
lemma states'_alt_def:
"states' = {(L, s). L ∈ states ∧ bounded bounds s}"
unfolding states'_def bounded_def dom_bounds_eq by auto
lemma states'_alt_def2:
"states' = {(L, s). L ∈ states ∧ dom s = {0..<n_vs} ∧ check_bounded s}"
proof -
have "states' = {(L, s). L ∈ states ∧ dom s = {0..<n_vs} ∧ bounded bounds s}"
unfolding states'_def bounded_def dom_bounds_eq by auto
then show ?thesis
by (auto simp: check_bounded_iff)
qed
lemma trans_prod_states'_inv:
"l' ∈ states'" if "(l, g, a, r, l') ∈ trans_prod" "l ∈ states'"
using that unfolding states'_alt_def
by (cases l') (auto dest: trans_prod_bounded_inv trans_prod_states_inv)
lemma prod_ta_states'_inv:
"l' ∈ states'" if "prod_ta ⊢ l ⟶⇗g,a,r⇖ l'" "l ∈ states'"
using that by simp (rule trans_prod_states'_inv)
lemma dom_eq_transfer [transfer_rule]:
"(state_rel ===> (=)) (λs. dom s = {0..<n_vs}) (λs. length s = n_vs)"
by (rule rel_funI) (auto simp: state_rel_def)
lemma states'_memi_correct:
"(states'_memi, (λl. l ∈ states')) ∈ loc_rel → bool_rel"
proof -
define t where "t s ≡ dom s = {0..<n_vs}" for s :: "nat ⇀ int"
define ti where "ti s ≡ length s = n_vs" for s :: "int list"
let ?R = "λx y. (eq_onp (λL. length L = n_ps) ×⇩R state_rel) y x"
note [transfer_rule] = dom_eq_transfer[folded t_def ti_def]
have [p2rel]: "p2rel ((λx y. (eq_onp (λL. length L = n_ps) ×⇩R state_rel) y x)) = loc_rel"
by (auto simp: eq_onp_def p2rel_def loc_rel_def)
have *: "(λ(L, s). L ∈ states ∧ dom s = {0..<n_vs} ∧ check_bounded s) = (λl. l ∈ states')"
by (intro ext) (auto simp: states'_alt_def2)
have "(((=) ×⇩R state_rel) ===> (=))
(λ(L, s). L ∈ states ∧ t s ∧ check_bounded s) (λ(L, s). L ∈ states ∧ ti s ∧ check_boundedi s)"
by transfer_prover
then have
"(((=) ×⇩R state_rel) ===> (=))
(λ(L, s). L ∈ states ∧ dom s = {0..<n_vs} ∧ check_bounded s)
states'_memi"
unfolding t_def ti_def states'_memi_def .
then have [p2rel]: "(?R ===> (=)) states'_memi (λl. l ∈ states')"
unfolding * by (intro rel_funI) (auto simp: eq_onp_def elim!: rel_funE)
then have "(states'_memi, (λl. l ∈ states')) ∈ p2rel (?R ===> (=))"
unfolding p2rel_def by simp
then show ?thesis
unfolding p2rel .
qed
end
end
end