Theory Simple_Network_Language_Impl
theory Simple_Network_Language_Impl
imports
Simple_Network_Language
Munta_Base.Normalized_Zone_Semantics_Impl_Refine
"HOL-Library.IArray" "HOL-Library.AList"
Munta_Base.More_Methods
Munta_Base.Bijective_Embedding
TA_Impl_Misc2
TA_More2
TA_Equivalences
"HOL-Eisbach.Eisbach_Tools"
Munta_Base.TA_Syntax_Bundles
begin
unbundle no_library_syntax
paragraph ‹Default maps›
definition default_map_of :: "'b ⇒ ('a × 'b) list ⇒ 'a ⇒ 'b" where
"default_map_of a xs ≡ FinFun.map_default a (map_of xs)"
lemma default_map_of_alt_def:
"default_map_of a xs x = (if x ∈ dom (map_of xs) then the (map_of xs x) else a)"
unfolding default_map_of_def map_default_def by (auto split: option.split_asm)
lemma range_default_map_of:
"range (default_map_of x xs) ⊆ snd ` set xs ∪ {x}"
unfolding default_map_of_def map_default_def
by (auto split: option.split_asm) (meson img_snd map_of_SomeD)
lemma finite_range_default_map_of:
"finite (range (default_map_of x m))"
proof -
have "range (default_map_of x m) ⊆ the ` range (map_of m) ∪ {x}"
unfolding default_map_of_def FinFun.map_default_def
by (auto split: option.splits) (metis image_eqI option.sel rangeI)
also have "finite …"
by (blast intro: finite_range_map_of)
finally show ?thesis .
qed
lemma map_index'_inj:
"L = L'"
if "length L = length L'" "map_index' n f L = map_index' n g L'" "set L ⊆ S" "set L' ⊆ T"
"∀ i < length L + n. ∀ x ∈ S. ∀y ∈ T. f i x = g i y ⟶ x = y"
using that
proof (induction "length L" arbitrary: L L' n)
case 0
then show ?case
by simp
next
case (Suc x)
from Suc.prems obtain a b L1 L1' where *:
"length L1 = x" "length L1' = x" "L = a # L1" "L' = b # L1'"
by (smt (z3) Suc.hyps(2) length_Suc_conv)
show ?case
unfolding ‹L = _› ‹L' = _›
apply (clarsimp, rule conjI)
subgoal
by (smt (z3) *(3,4) Suc.hyps(2) Suc.prems Suc_less_eq add_Suc_shift less_add_Suc2 list.set_intros(1) list_tail_coinc map_index'.simps(2) set_mp)
subgoal
apply (rule Suc.hyps)
using Suc.prems * by auto
done
qed
lemma map_index_inj:
"L = L'"
if "map_index f L = map_index g L'" "set L ⊆ S" "set L' ⊆ T"
"∀ i < length L. ∀ x ∈ S. ∀y ∈ T. f i x = g i y ⟶ x = y"
using that by - (rule map_index'_inj, auto dest: map_index_eq_imp_length_eq)
lemma map_index_inj1:
"L = L'"
if "map_index f L = map_index g L'"
"∀ i < length L. f i (L ! i) = g i (L' ! i) ⟶ L ! i = L' ! i"
proof (intros add: nth_equalityI)
from that(1) show ‹length L = length L'›
by (rule map_index_eq_imp_length_eq)
fix i :: ‹nat›
assume ‹i < length L›
with that have "map_index f L ! i = map_index g L' ! i"
by auto
with ‹i < length L› ‹length L = length L'› have "f i (L ! i) = g i (L' ! i)"
by simp
with ‹i < length L› that(2) show ‹L ! i = L' ! i›
by simp
qed
lemma map_index_update:
"map_index f (xs[i := a]) = (map_index f xs)[i := f i a]"
by (rule nth_equalityI) (auto simp: nth_list_update')
lemma map_trans_broad_aux1:
"map_index map_loc (fold (λp L. L[p := ls' p]) ps L) =
fold (λp L. L[p := map_loc p (ls' p)]) ps (map_index map_loc L)"
by (induction ps arbitrary: L) (auto simp: map_index_update)
lemma InD2:
fixes map_action
assumes "inj map_action" "In (map_action a) = map_act map_action a'"
shows "a' = In a"
using assms(2) by (cases a') (auto simp: injD[OF assms(1)])
lemma OutD2:
fixes map_action
assumes "inj map_action" "Out (map_action a) = map_act map_action a'"
shows "a' = Out a"
using assms(2) by (cases a') (auto simp: injD[OF assms(1)])
lemma (in Prod_TA_Defs) trans_broad_alt_def:
"trans_broad =
{((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 ∈ 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))
∨ (∀p < n_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'' ∧
(∀p. p∉set ps ⟶ bs p = bexp.true) ∧ (∀p. p∉set ps ⟶ gs p = []) ∧
(∀p. p∉set ps ⟶ fs p = []) ∧ (∀p. p∉set ps ⟶ rs p = [])
}"
unfolding trans_broad_def
proof ((intro Collect_eqI iffI; elims add: more_elims), goal_cases)
case prems: (1 x L s L' s' s'' a p l b g f r l' bs gs fs rs ls' ps)
let ?f = "λgs p. if p ∈ set ps then gs p else []"
let ?bs = "λp. if p ∈ set ps then bs p else bexp.true"
let ?gs = "?f gs" let ?fs = "?f fs" let ?rs = "?f rs"
have [simp]: "map gs ps = map ?gs ps" "map rs ps = map ?rs ps" "map fs ps = map ?fs ps"
by (simp cong: map_cong)+
with prems show ?case
by (inst_existentials L s L' s' s'' a p l b g f r l' ?bs ?gs ?fs ?rs ls' ps; (assumption | simp))
next
case (2 x L s L' s' s'' a p l b g f r l' bs gs fs rs ls' ps)
then show ?case
by blast
qed
definition
"conv_automaton ≡ λ(committed, urgent, trans, inv).
(committed,
urgent,
map (λ(l, b, g, a, f, r, l'). (l, b, conv_cc g, a, f, r, l')) trans,
map (λ(s, cc). (s, conv_cc cc)) inv)"
definition
"automaton_of ≡
λ(committed, urgent, trans, inv). (set committed, set urgent, set trans, default_map_of [] inv)"
locale Simple_Network_Impl_Defs =
fixes automata ::
"('s list × 's list × ('a act, 's, 'c, 't, 'x, int) transition list
× ('s × ('c, 't) cconstraint) list) list"
and broadcast :: "'a list"
and bounds' :: "('x × (int × int)) list"
begin
definition
"n_vs = length bounds'"
definition
"B x ≡ if x ∈ dom (map_of bounds') then the (map_of bounds' x) else (0, 0)"
sublocale Prod_TA_Defs
"(set broadcast, map automaton_of automata, map_of bounds')" .
lemma L_len[intro, dest]:
"length L = n_ps" if "L ∈ states"
using that unfolding states_def by simp
lemma N_eq:
‹N i = automaton_of (automata ! i)› if ‹i < n_ps›
using that unfolding N_def n_ps_def fst_conv snd_conv by (intro nth_map; simp)
end
locale Simple_Network_Impl =
fixes automata ::
"('s list × 's list × ('a act, 's, 'c, int, 'x, int) transition list
× ('s × ('c, int) cconstraint) list) list"
and broadcast :: "'a list"
and bounds' :: "('x × (int × int)) list"
begin
sublocale Simple_Network_Impl_Defs automata broadcast bounds' .
end
paragraph ‹Mapping through the product construction›
lemma f_the_inv_f:
"f (the_inv f x) = x" if "inj f" "x ∈ range f"
using that by (auto simp: the_inv_f_f)
method fprem =
(match premises in R: _ ⇒ ‹rule R[elim_format]›, assumption)
context Simple_Network_Impl
begin
paragraph ‹Conversion from integers to reals commutes with product construction.›
sublocale conv: Prod_TA_Defs
"(set broadcast, map (Simple_Network_Language.conv_A o automaton_of) automata, map_of bounds')" .
lemma (in -) conv_ac_inj:
"ac = ac'" if "conv_ac ac = conv_ac ac'"
using that by (cases ac; cases ac'; auto)
lemma (in -) conv_cc_inj:
"cc = cc'" if "conv_cc cc = conv_cc cc'"
using that by (subst (asm) inj_map_eq_map) (auto simp add: conv_ac_inj intro: injI)
context
begin
lemma conv_alt_def:
"conv (set broadcast, map automaton_of automata, map_of bounds') =
(set broadcast, map (Simple_Network_Language.conv_A o automaton_of) automata, map_of bounds')"
unfolding conv_def by simp
private lemma 2:
"Simple_Network_Language.conv_A o automaton_of = (λ(committed, urgent, trans, inv).
(set committed,
set urgent,
set (map Simple_Network_Language.conv_t trans),
default_map_of [] (map (λ (l, g). (l, conv_cc g)) inv)))"
apply (rule ext)
apply clarsimp
unfolding Simple_Network_Language.conv_A_def automaton_of_def
apply (clarsimp split: prod.split)
unfolding default_map_of_def
unfolding FinFun.map_default_def
apply (rule ext)
subgoal for xs a
by (induction xs) auto
done
lemma conv_n_ps_eq:
"conv.n_ps = n_ps"
by (simp add: Prod_TA_Defs.n_ps_def)
lemma conv_N_eq:
"conv.N i = Simple_Network_Language.conv_A (N i)" if "i < n_ps"
using that unfolding n_ps_def Prod_TA_Defs.N_def fst_conv snd_conv by (subst nth_map | simp)+
private lemma 5:
"inv (conv.N i) = conv_cc o (inv (N i))" if "i < n_ps"
unfolding conv_N_eq[OF that] unfolding Simple_Network_Language.conv_A_def
by (simp split: prod.split add: inv_def)
lemma trans_conv_N_eq:
"trans (conv.N i) = Simple_Network_Language.conv_t ` (trans (N i))" if "i < n_ps"
unfolding conv_N_eq[OF that] unfolding Simple_Network_Language.conv_A_def
by (simp split: prod.split add: trans_def)
private lemma 71:
"(l, b, conv_cc g, a, r, u, l')∈Simple_Network_Language.trans (conv.N i)"
if "(l, b, g, a, r, u, l')∈Simple_Network_Language.trans (N i)" "i < n_ps"
using that by (force simp add: trans_conv_N_eq Simple_Network_Language.conv_t_def)
private lemma 72:
"(l, b, conv_cc g, a, r, u, l')∈Simple_Network_Language.trans (conv.N i)
⟷ (l, b, g, a, r, u, l')∈Simple_Network_Language.trans (N i)" if "i < n_ps"
by (auto simp: trans_conv_N_eq[OF that] Simple_Network_Language.conv_t_def
dest: conv_cc_inj intro: image_eqI[rotated])
private lemma 73:
"∃g'. g = conv_cc g' ∧ (l, b, g', a, r, u, l')∈Simple_Network_Language.trans (N i)"
if "(l, b, g, a, r, u, l')∈Simple_Network_Language.trans (conv.N i)" "i < n_ps"
using that by (force simp: trans_conv_N_eq Simple_Network_Language.conv_t_def)
lemma conv_bounds[simp]:
"conv.bounds = bounds"
unfolding conv.bounds_def bounds_def by simp
lemma conv_states[simp]:
"conv.states = states"
unfolding conv.states_def states_def conv_n_ps_eq
by (auto simp add: trans_conv_N_eq Simple_Network_Language.conv_t_def) (fastforce, force)
private lemma 9:
"committed (conv.N p) = committed (N p)" if ‹p < n_ps›
unfolding conv_N_eq[OF that] unfolding Simple_Network_Language.conv_A_def
by (simp split: prod.split add: committed_def)
private lemma 10:
"conv.broadcast = set broadcast"
unfolding conv.broadcast_def by simp
lemma conv_trans_int:
"conv.trans_int = (λ(l, g, a, r, l'). (l, map conv_ac g, a, r, l')) ` trans_int"
unfolding conv.trans_int_def trans_int_def
supply [simp] = L_len
apply standard
subgoal
by (clarsimp simp: Simple_Network_Language.conv_t_def conv_n_ps_eq trans_conv_N_eq 9)
(intros add: more_intros, solve_triv+)
subgoal
by (rule subsetI,
clarsimp simp: Simple_Network_Language.conv_t_def conv_n_ps_eq trans_conv_N_eq 9[symmetric])
((drule (1) 71)+, intros add: more_intros, solve_triv+)
done
lemma conv_trans_bin:
"conv.trans_bin = (λ(l, g, a, r, l'). (l, map conv_ac g, a, r, l')) ` trans_bin"
unfolding conv.trans_bin_def trans_bin_def 10 broadcast_def
supply [simp] = L_len
apply standard
subgoal
by (clarsimp simp add: Simple_Network_Language.conv_t_def conv_n_ps_eq trans_conv_N_eq 9)
(intros add: more_intros, solve_triv+)
subgoal
by (rule subsetI,
clarsimp simp: Simple_Network_Language.conv_t_def conv_n_ps_eq trans_conv_N_eq 9[symmetric])
((drule (1) 71)+, intros add: more_intros, solve_triv+)
done
lemma n_ps_rangeD:
"p < n_ps" if "p ∈ set ps" "set ps ⊆ {0..<n_ps}"
using that by auto
lemma maximalD:
"(∀g f r l'.
(L ! q, b, g, In a', f, r, l')
∉ (λ(l, b, g, a, f, r, l').
(l, b, map conv_ac g, a, f, r, l')) ` trans (N q)) ∨ ¬ check_bexp s b True" if
"∀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)"
"q<n_ps" "q ∉ set ps" "p ≠ q"
for b ps p q L a' s using that by fastforce
lemma conv_trans_broad:
"conv.trans_broad = (λ(l, g, a, r, l'). (l, map conv_ac g, a, r, l')) ` trans_broad"
unfolding conv.trans_broad_alt_def trans_broad_alt_def
apply standard
supply [simp] = L_len
subgoal
proof -
have **: "∃ gs'. gs = conv_cc o gs' ∧
(∀p∈set ps.(L ! p, bs p, gs' p, In a, fs p, rs p, ls' p) ∈ trans (N p))"
if assms:
"∀p∈set ps. (L ! p, bs p, gs p, In a, fs p, rs p, ls' p) ∈ trans (conv.N p)"
"set ps ⊆ {0..<n_ps}" "∀p. p ∉ set ps ⟶ gs p = []"
for L ps bs gs a fs rs ls'
proof -
have *: "gs p = conv_cc (Hilbert_Choice.inv conv_cc (gs p))" if "p ∈ set ps" for p
using that assms by (auto 4 3 simp: f_inv_into_f dest!: 73)
show ?thesis
apply (inst_existentials "Hilbert_Choice.inv conv_cc o gs")
subgoal
apply (rule ext)
subgoal for p
apply (cases "p ∈ set ps")
subgoal
by (simp, erule *)
subgoal
using that(3) by (auto intro: injI inv_f_eq conv_ac_inj)
done
done
subgoal
using that * by (force dest!: conv_cc_inj 73)
done
qed
have *: "set ps ⊆ {0..<n_ps} ⟷ (∀p ∈ set ps. p < n_ps)" for ps
by auto
have maximalI:
"∀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)" if
"∀q<n_ps. q ∉ set ps ∧ p ≠ q ⟶ (∀b. (∀g f r l'.
(L ! q, b, g, In a', f, r, l') ∉ trans (conv.N q)) ∨ ¬ check_bexp s b True)"
for ps p L a' s
using that by (blast dest!: 71)
show ?thesis
apply (rule subsetI)
apply (clarsimp simp add: conv_n_ps_eq 9 10 broadcast_def split: prod.split_asm)
apply (drule (2) **)
apply (drule (1) 73)+
apply elims
apply (intro image_eqI[rotated] CollectI exI conjI)
apply solve_triv+
subgoal premises prems
using prems(2) ‹set _ ⊆ {0..<n_ps}› by (auto dest: n_ps_rangeD simp: 9)
apply (erule maximalI; fail)
by solve_triv+ (simp split: prod.split add: map_concat)
qed
subgoal
apply (rule subsetI)
apply (clarsimp simp:
Simple_Network_Language.conv_t_def
conv_n_ps_eq trans_conv_N_eq 9[symmetric] 10 broadcast_def map_concat)
apply (drule (1) 71)
apply (intros add: more_intros)
apply solve_triv+
apply (subst comp_def; rule 71; fast elim: n_ps_rangeD; fail)
subgoal premises prems for L s s' s'' aj p g f r l' gs fs rs ls' ps
using prems(3,6) 9 by fastforce
apply (erule maximalD)
apply (solve_triv | blast)+
done
done
lemma conv_prod_ta:
"conv.prod_ta = Normalized_Zone_Semantics_Impl.conv_A prod_ta"
unfolding conv.prod_ta_def prod_ta_def
unfolding conv.trans_prod_def trans_prod_def
unfolding conv.prod_inv_def prod_inv_def
unfolding conv.N_def N_def conv_n_ps_eq
unfolding conv_A_def
apply simp
apply (rule conjI)
subgoal
unfolding image_Un
by ((fo_rule arg_cong2)+; rule conv_trans_int conv_trans_bin conv_trans_broad)
subgoal
unfolding conv.N_def N_def
by (rule ext) (auto simp: 5 map_concat intro!: map_cong arg_cong[where f = concat])
done
end
paragraph ‹Fundamentals›
definition "clkp_set' ≡
(⋃ A ∈ set automata. ⋃ g ∈ set (snd (snd (snd A))). collect_clock_pairs (snd g))
∪ (⋃ A ∈ set automata. ⋃ (l, b, g, _) ∈ set (fst (snd (snd A))). collect_clock_pairs g)"
definition clk_set' where
‹clk_set' =
fst ` clkp_set' ∪
(⋃ A ∈ set automata. ⋃ (_, _, _, _, _, r, _) ∈ set (fst (snd (snd A))). set r)›
lemma (in -) default_map_of_in_listD:
"x ∈ ⋃ (set ` snd ` set invs)" if "x ∈ set (default_map_of [] invs l)"
proof -
have "[] ≠ default_map_of [] invs l"
using that by force
then have "default_map_of [] invs l ∈ snd ` set invs"
by (metis (no_types) UNIV_I Un_insert_right range_default_map_of[of "[]" "invs"]
image_eqI insertE subsetCE sup_bot.right_neutral)
with that show ?thesis
by blast
qed
lemma collect_clock_pairs_invsI:
"(a, b) ∈ ⋃ ((collect_clock_pairs o snd) ` set invs)"
if "(a, b) ∈ collect_clock_pairs (default_map_of [] invs l)"
using that unfolding collect_clock_pairs_def by (auto dest!: default_map_of_in_listD)
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_eq[OF that] by (auto split: prod.splits simp: automaton_of_def trans_def)
lemma length_automata_eq_n_ps:
"length automata = n_ps"
unfolding n_ps_def by simp
lemma clkp_set'_subs:
"Timed_Automata.clkp_set prod_ta ⊆ clkp_set'"
unfolding Timed_Automata.clkp_set_def clkp_set'_def
proof (rule union_subsetI, goal_cases)
case 1
have *: False
if "i < n_ps" "L ∈ states"
"(a, b) ∈ collect_clock_pairs (Simple_Network_Language.inv (N i) (L ! i))"
"∀x∈set automata. ∀x∈set (snd (snd (snd x))). (a, b) ∉ collect_clock_pairs (snd x)"
for a :: 'c and b :: int and L :: "'s list" and i :: nat
using that
apply (subst (asm) N_eq)
apply assumption
apply (inst_existentials "automata ! i")
unfolding automaton_of_def
by (force dest!: nth_mem collect_clock_pairs_invsI
split: prod.split_asm simp: inv_def Prod_TA_Defs.n_ps_def)
from 1 show ?case
unfolding Timed_Automata.collect_clki_def inv_of_prod prod_inv_def
by (auto simp: collect_clock_pairs_concat intro: *)
next
case 2
then show ?case
apply simp
unfolding trans_prod_def Timed_Automata.collect_clkt_def
apply safe
subgoal
unfolding trans_int_def by (fastforce simp: length_automata_eq_n_ps mem_trans_N_iff)
subgoal
unfolding trans_bin_def
by (fastforce
simp: length_automata_eq_n_ps mem_trans_N_iff
dest!: collect_clock_pairs_append_cases)
subgoal
unfolding trans_broad_def
apply (clarsimp simp: length_automata_eq_n_ps mem_trans_N_iff)
apply (drule collect_clock_pairs_append_cases)
unfolding collect_clock_pairs_concat
apply (clarsimp; safe)
by (fastforce simp: length_automata_eq_n_ps mem_trans_N_iff)+
done
qed
lemma collect_clkvt_subs:
"collect_clkvt (trans_of prod_ta) ⊆
(⋃ A ∈ set automata. ⋃ (_, _, _, _, _, r, _) ∈ set (fst (snd (snd A))). set r)"
apply simp
unfolding collect_clkvt_def
apply safe
unfolding trans_prod_def
subgoal
apply simp
unfolding trans_prod_def Timed_Automata.collect_clkt_def
apply safe
subgoal
unfolding trans_int_def
by (fastforce
simp: length_automata_eq_n_ps mem_trans_N_iff
dest!: collect_clock_pairs_append_cases)
subgoal
unfolding trans_bin_def
by (fastforce
simp: length_automata_eq_n_ps mem_trans_N_iff
dest!: collect_clock_pairs_append_cases)
subgoal
unfolding trans_broad_def
apply (clarsimp simp: length_automata_eq_n_ps mem_trans_N_iff)
unfolding collect_clock_pairs_concat
apply safe
by (fastforce simp: length_automata_eq_n_ps mem_trans_N_iff)+
done
done
lemma clk_set'_subs: "clk_set prod_ta ⊆ clk_set'"
using collect_clkvt_subs clkp_set'_subs unfolding clk_set'_def by auto
end
lemma (in Prod_TA_Defs) finite_range_invI:
"finite (range prod_inv)" if assms: "∀ i < n_ps. finite (range (inv (N i)))"
proof -
let ?N = "⋃ (range ` inv ` N ` {0..<n_ps})"
let ?X = "{I. set I ⊆ ?N ∧ length I ≤ n_ps}"
have "finite ?N"
using assms by auto
then have "finite ?X"
by (rule finite_lists_length_le)
moreover have "range prod_inv ⊆ concat ` ?X ∪ {[]}"
proof
fix x assume "x ∈ range prod_inv"
then consider L where "x = concat (map (λp. (inv (N p)) (L ! p)) [0..<n_ps])" | "x = []"
unfolding prod_inv_def by (auto split: if_split_asm)
then show "x ∈ concat ` ?X ∪ {[]}"
by (cases; force)
qed
ultimately show ?thesis by - (drule finite_subset; auto)
qed
definition (in Prod_TA_Defs)
"loc_set =
(⋃ {fst ` trans (N p) | p. p < n_ps} ∪
⋃ {(snd o snd o snd ∘ snd ∘ snd ∘ snd) ` trans (N p) | p. p < n_ps})"
lemma (in Prod_TA_Defs) states_loc_set:
"states ⊆ {L. set L ⊆ loc_set ∧ length L = n_ps}"
unfolding states_def loc_set_def
apply (intros add: more_intros)
apply (elims add: more_elims)
apply (drule mem_nth)
apply simp
apply (elims add: allE, assumption)
apply (simp split: prod.split_asm)
apply (erule disjE; (intros add: disjI1 disjI2 more_intros, solve_triv+); fail)
by (elims add: more_elims)
lemma (in Prod_TA_Defs) finite_states:
assumes finite_trans: "∀p < n_ps. finite (Simple_Network_Language.trans (N p))"
shows "finite states"
proof -
have "states ⊆ {L. set L ⊆ loc_set ∧ length L = n_ps}"
by (rule states_loc_set)
also from finite_trans have "finite …"
unfolding loc_set_def by (intro finite_intros) auto
finally show ?thesis .
qed
context Simple_Network_Impl
begin
lemma trans_N_finite:
assumes "p < n_ps"
shows "finite (Simple_Network_Language.trans (N p))"
using assms by (subst N_eq) (auto simp: automaton_of_def trans_def split: prod.split)
lemma states_finite:
"finite states"
by (intros add: finite_states trans_N_finite)
lemma bounded_finite:
"finite {s. bounded bounds s}"
proof -
let ?l = "Min {fst (the (bounds x)) | x. x ∈ dom bounds}"
let ?u = "Max {snd (the (bounds x)) | x. x ∈ dom bounds}"
have "finite (dom bounds)"
unfolding bounds_def by simp
then have "{s. bounded bounds s} ⊆ {s. dom s = dom bounds ∧ ran s ⊆ {?l..?u}}"
unfolding bounded_def
apply clarsimp
apply (rule conjI)
subgoal for s v
unfolding ran_is_image
apply clarsimp
subgoal for x l u
by (rule order.trans[where b = "fst (the (bounds x))"]; (rule Min_le)?; force)
done
subgoal for s v
unfolding ran_is_image
apply clarsimp
subgoal for x l u
by (rule order.trans[where b = "snd (the (bounds x))"]; (rule Max_ge)?; force)
done
done
also from ‹finite (dom bounds)› have "finite …"
by (rule finite_set_of_finite_maps) blast
finally show ?thesis .
qed
lemma trans_prod_finite:
"finite trans_prod"
proof -
have "finite trans_int"
proof -
have "trans_int ⊆
{((L, s), g, Internal a, r, (L', s')) | L s p l b g a f r l' s' L'.
L ∈ states ∧ bounded bounds s ∧ p < n_ps ∧
(l, b, g, Sil a, f, r, l') ∈ trans (N p) ∧
bounded bounds s'
∧ L' = L[p := l']
}"
unfolding trans_int_def by (force simp: L_len)
also have "finite …"
proof -
have "finite {(a, b, c, d, e, f, g). (a, b, c, Sil d, e, f, g) ∈ trans (N p)}"
if "p < n_ps" for p
using [[simproc add: finite_Collect]] that
by (auto intro: trans_N_finite finite_vimageI injI)
with states_finite bounded_finite show ?thesis
by defer_ex
qed
finally show ?thesis .
qed
moreover have "finite trans_bin"
proof -
have "trans_bin ⊆
{((L, s), g1 @ g2, Bin a, r1 @ r2, (L', s'')) |
L s p q l1 b1 g1 a f1 r1 l1' l2 b2 g2 f2 r2 l2' s'' L'.
L ∈ states ∧ bounded bounds s ∧
p < n_ps ∧ q < n_ps ∧
(l1, b1, g1, In a, f1, r1, l1') ∈ trans (N p) ∧
(l2, b2, g2, Out a, f2, r2, l2') ∈ trans (N q) ∧
bounded bounds s'' ∧
L' = L[p := l1', q := l2']
}"
unfolding trans_bin_def by (fastforce simp: L_len)
also have "finite …"
proof -
have "finite {(a, b, c, d, e, f, g). (a, b, c, In d, e, f, g) ∈ trans (N p)}"
if "p < n_ps" for p
using [[simproc add: finite_Collect]] that
by (auto intro: trans_N_finite finite_vimageI injI)
moreover have "finite {(a, b, c, e, f, g). (a, b, c, Out d, e, f, g) ∈ trans (N p)}"
if "p < n_ps" for p d
using [[simproc add: finite_Collect]] that
by (auto intro: trans_N_finite finite_vimageI injI)
ultimately show ?thesis
using states_finite bounded_finite by defer_ex
qed
finally show ?thesis .
qed
moreover have "finite trans_broad"
proof -
define P where "P ps ≡ set ps ⊆ {0..<n_ps} ∧ distinct ps" for ps
define Q where "Q a n bs gs fs rs ≡
(∀p < n. ∃ q < n_ps. ∃ l l'. (l, bs ! p, gs ! p, In a, fs ! p, rs ! p, l') ∈ trans (N q)) ∧
length bs = n ∧ length gs = n ∧ length fs = n ∧ length rs = n" for a n bs gs fs rs
define tag where "tag x = True" for x :: 's
have Q_I: "Q a (length ps) (map bs ps) (map gs ps) (map fs ps) (map rs ps)"
if "set ps ⊆ {0..<n_ps}"
"∀p∈set ps. (L ! p, bs p, gs p, In a, fs p, rs p, ls' p) ∈ trans (N p)"
for ps :: "nat list" and L a bs gs fs rs ls'
using that unfolding Q_def by (auto 4 4 dest!: nth_mem)
have "trans_broad ⊆
{((L, s), g @ concat gs, Broad a, r @ concat rs, (L', s'')) |
L s a p l b g f r l' ps bs gs fs rs L' s''.
L ∈ states ∧ bounded bounds s ∧ a ∈ set broadcast ∧
p < n_ps ∧
(l, b, g, Out a, f, r, l') ∈ trans (N p) ∧
P ps ∧
Q a (length ps) bs gs fs rs ∧
L' ∈ states ∧
bounded bounds s'' ∧
tag l'
}"
unfolding trans_broad_def broadcast_def
apply (rule subsetI)
apply (elims add: more_elims)
apply (intros add: more_intros)
apply solve_triv+
apply (simp add: L_len; fail)
apply assumption
apply (unfold P_def; intros; assumption)
apply (rule Q_I; assumption)
subgoal
by (blast intro: state_preservation_updI state_preservation_fold_updI)
apply assumption
unfolding tag_def ..
also have "finite …"
proof -
have "finite {(a, b, c, e, f, g). (a, b, c, Out d, e, f, g) ∈ trans (N p)}"
if "p < n_ps" for p d
using [[simproc add: finite_Collect]] that
by (auto intro: trans_N_finite finite_vimageI injI)
moreover have "finite {ps. P ps}"
unfolding P_def by (simp add: finite_intros)
moreover have "finite {(bs, gs, fs, rs). Q a n bs gs fs rs}" (is "finite ?S") for a n
proof -
let ?T = "⋃ (trans ` N ` {0..<n_ps})"
have "?S ⊆ {(bs, gs, fs, rs).
(set bs ⊆ (λ(_,b,_). b) ` ?T ∧ length bs = n) ∧
(set gs ⊆ (λ(_,_,g,_). g) ` ?T ∧ length gs = n) ∧
(set fs ⊆ (λ(_,_,_,_,f,_). f) ` ?T ∧ length fs = n) ∧
(set rs ⊆ (λ(_,_,_,_,_,r,_). r) ` ?T ∧ length rs = n)
}"
unfolding Q_def
apply safe
apply (all ‹drule mem_nth; elims; drule spec; elims›)
apply force+
done
also have "finite …"
using trans_N_finite by (intro finite_intros more_finite_intros) auto
finally show ?thesis .
qed
ultimately show ?thesis
using states_finite bounded_finite by defer_ex
qed
finally show ?thesis .
qed
ultimately show ?thesis
by (simp add: trans_prod_def)
qed
lemma prod_inv_finite:
"finite (range prod_inv)"
apply (intros add: finite_range_invI)
unfolding length_automata_eq_n_ps[symmetric]
unfolding N_def
unfolding automaton_of_def
by (auto intro: finite_range_default_map_of split: prod.split simp: inv_def)
end
paragraph ‹Collecting variables from expressions.›
fun vars_of_bexp and vars_of_exp where
"vars_of_bexp (not e) = vars_of_bexp e"
| "vars_of_bexp (and e1 e2) = (vars_of_bexp e1 ∪ vars_of_bexp e2)"
| "vars_of_bexp (bexp.or e1 e2) = (vars_of_bexp e1 ∪ vars_of_bexp e2)"
| "vars_of_bexp (imply e1 e2) = (vars_of_bexp e1 ∪ vars_of_bexp e2)"
| "vars_of_bexp (eq i x) = vars_of_exp i ∪ vars_of_exp x"
| "vars_of_bexp (le i x) = vars_of_exp i ∪ vars_of_exp x"
| "vars_of_bexp (lt i x) = vars_of_exp i ∪ vars_of_exp x"
| "vars_of_bexp (ge i x) = vars_of_exp i ∪ vars_of_exp x"
| "vars_of_bexp (gt i x) = vars_of_exp i ∪ vars_of_exp x"
| "vars_of_bexp bexp.true = {}"
| "vars_of_exp (const c) = {}"
| "vars_of_exp (var x) = {x}"
| "vars_of_exp (if_then_else b e1 e2) = vars_of_bexp b ∪ vars_of_exp e1 ∪ vars_of_exp e2"
| "vars_of_exp (binop _ e1 e2) = vars_of_exp e1 ∪ vars_of_exp e2"
| "vars_of_exp (unop _ e) = vars_of_exp e"
definition (in Prod_TA_Defs)
"var_set =
(⋃S ∈ {(fst ∘ snd) ` trans (N p) | p. p < n_ps}. ⋃b ∈ S. vars_of_bexp b) ∪
(⋃S ∈ {(fst ∘ snd ∘ snd ∘ snd ∘ snd) ` trans (N p) | p. p < n_ps}.
⋃f ∈ S. ⋃ (x, e) ∈ set f. {x} ∪ vars_of_exp e)"
locale Simple_Network_Impl_nat_defs =
Simple_Network_Impl automata
for automata ::
"(nat list × nat list × (nat act, nat, nat, int, nat, int) transition list
× (nat × (nat, int) cconstraint) list) list" +
fixes m :: nat and num_states :: "nat ⇒ nat" and num_actions :: nat
locale Simple_Network_Impl_nat =
Simple_Network_Impl_nat_defs +
assumes has_clock: "m > 0"
assumes non_empty: "0 < length automata"
assumes trans_num_states:
"∀i < n_ps. let (_, _, trans, _) = (automata ! i) in ∀ (l, _, _, _, _, _, l') ∈ set trans.
l < num_states i ∧ l' < num_states i"
and inv_num_states:
"∀i < n_ps. let (_, _, _, inv) = (automata ! i) in ∀ (x, _) ∈ set inv. x < num_states i"
assumes var_set:
"∀(_, _, trans, _) ∈ set automata. ∀(_, _, _, _, f, _, _) ∈ set trans.
∀(x, upd) ∈ set f. x < n_vs ∧ (∀i ∈ vars_of_exp upd. i < n_vs)"
"∀(_, _, trans, _) ∈ set automata. ∀(_, b, _, _, _, _, _) ∈ set trans.
∀i ∈ vars_of_bexp b. i < n_vs"
assumes bounds:
"∀ i < n_vs. fst (bounds' ! i) = i"
assumes action_set:
"∀a ∈ set broadcast. a < num_actions"
"∀(_, _, trans, _) ∈ set automata. ∀(_, _, _, a, _, _, _) ∈ set trans.
pred_act (λa. a < num_actions) a"
assumes clock_set:
"∀(_, _, trans, _) ∈ set automata. ∀(_, _, g, _, _, r, _) ∈ set trans.
(∀c ∈ set r. 0 < c ∧ c ≤ m) ∧
(∀ (c, x) ∈ collect_clock_pairs g. 0 < c ∧ c ≤ m ∧ x ∈ ℕ)
"
"∀(_, _, _, inv) ∈ set automata. ∀(l, g) ∈ set inv.
(∀ (c, x) ∈ collect_clock_pairs g. 0 < c ∧ c ≤ m ∧ x ∈ ℕ)
"
assumes broadcast_receivers:
"∀(_, _, trans, _) ∈ set automata. ∀(_, _, g, a, _, _, _) ∈ set trans.
case a of In a ⇒ a ∈ set broadcast ⟶ g = [] | _ ⇒ True"
begin
lemma broadcast_receivers_unguarded:
"∀p<n_ps. ∀l b g a f r l'.
(l, b, g, In a, f, r, l') ∈ Simple_Network_Language.trans (N p) ∧ a ∈ set broadcast ⟶ g = []"
using broadcast_receivers by (fastforce dest: nth_mem simp: n_ps_def mem_trans_N_iff)
sublocale conv: Prod_TA
"(set broadcast, map (Simple_Network_Language.conv_A o automaton_of) automata, map_of bounds')"
using broadcast_receivers_unguarded
by - (standard,
fastforce simp: conv.broadcast_def Simple_Network_Language.conv_t_def conv_n_ps_eq trans_conv_N_eq)
sublocale TA_Start_No_Ceiling prod_ta init m
proof standard
show "finite (trans_of prod_ta)"
using trans_prod_finite by simp
next
show "finite (range (inv_of prod_ta))"
using prod_inv_finite by simp
next
from clk_set'_subs have "clk_set prod_ta ⊆ clk_set'" .
also have "… ⊆ {1..m}"
using clock_set unfolding clk_set'_def clkp_set'_def by force
finally show "clk_set prod_ta ⊆ {1..m}" .
next
from clock_set have "∀(_, d)∈clkp_set'. d ∈ ℕ"
unfolding clkp_set'_def by force
then show "∀(_, d)∈Timed_Automata.clkp_set prod_ta. d ∈ ℕ"
by (auto dest!: subsetD[OF clkp_set'_subs])
next
show "0 < m"
by (rule has_clock)
qed
end
context Simple_Network_Impl
begin
definition "sem ≡ (set broadcast, map (automaton_of o conv_automaton) automata, map_of bounds')"
sublocale sem: Prod_TA_sem sem .
lemma sem_N_eq:
"sem.N p = automaton_of (conv_automaton (automata ! p))" if ‹p < n_ps›
using that unfolding sem.N_def n_ps_def unfolding sem_def fst_conv snd_conv
by (subst nth_map) auto
end
inductive_cases step_u_elims:
"A ⊢ ⟨L, s, u⟩ →⇘Del⇙ ⟨L', s', u'⟩"
"A ⊢ ⟨L, s, u⟩ →⇘Internal a⇙ ⟨L', s', u'⟩"
"A ⊢ ⟨L, s, u⟩ →⇘Bin a⇙ ⟨L', s'', u'⟩"
"A ⊢ ⟨L, s, u⟩ →⇘Broad a⇙ ⟨L', s'', u'⟩"
inductive_cases step_u_elims':
"(broadcast, N, B) ⊢ ⟨L, s, u⟩ →⇘Del⇙ ⟨L', s', u'⟩"
"(broadcast, N, B) ⊢ ⟨L, s, u⟩ →⇘Internal a⇙ ⟨L', s', u'⟩"
"(broadcast, N, B) ⊢ ⟨L, s, u⟩ →⇘Bin a⇙ ⟨L', s'', u'⟩"
"(broadcast, N, B) ⊢ ⟨L, s, u⟩ →⇘Broad a⇙ ⟨L', s'', u'⟩"
lemma (in Prod_TA_Defs) states_lengthD:
"length L = n_ps" if "L ∈ states"
using that unfolding states_def by simp
end