Theory UPPAAL_State_Networks
theory UPPAAL_State_Networks
imports Munta_Model_Checker.State_Networks Timed_Automata.Normalized_Zone_Semantics UPPAAL_Asm_Clocks
AutoCorres2.Subgoals
begin
section ‹Networks of Timed Automata -- UPPAAL Style›
text ‹Networks of Timed Automata with Shared State and UPPAAL-style Assembler guards and updates.›
no_notation Ref.update ("_ := _" 62)
no_notation fun_rel_syn (infixr "→" 60)
lemma finite_lists_boundedI:
assumes "∀ i < r. finite (S i)"
shows "finite {s. length s = r ∧ (∀i<r. s ! i ∈ S i)}" (is "finite ?R")
proof -
let ?S = "⋃ {S i | i. i < r}"
have "?R ⊆ {s. set s ⊆ ?S ∧ length s = r}"
by (auto dest!: mem_nth)
moreover have "finite …" by (rule finite_lists_length_eq) (use assms in auto)
ultimately show ?thesis by (rule finite_subset)
qed
subsection ‹Syntax and Operational Semantics›
text ‹
We formalize Networks of Timed Automata with integer variable state using UPPAAL-style
guards and updates. The specification language for guards and updates is our formalization of
the UPPAAL like Assembler language.
We extend Networks of Timed Automata with arbitrary shared (global) state.
Syntactically, this extension is very simple.
We can just use the free action label slot to annotate edges with a guard
and an update function on discrete states.
The slightly more clumsy part is adding invariants for discrete states
by directly specifying an invariant annotating function.
›
type_synonym
('c, 'time, 's) invassn = "'s ⇒ ('c, 'time) cconstraint"
type_synonym
('a, 's) transition = "'s * addr * 'a * addr * 's"
type_synonym
('a, 'c, 'time, 's) uta = "('a, 's) transition set * ('c, 'time, 's) invassn"
type_synonym
('a, 'time, 's) unta =
"'time programc × ('a act, nat, 'time, 's) uta list × ('s ⇒ addr) list × (int * int) list"
definition
"bounded bounds s ≡
length s = length bounds ∧ (∀ i < length s. fst (bounds ! i) < s ! i ∧ s ! i < snd (bounds ! i))"
inductive step_u ::
"('a, 't :: time, 's) unta ⇒ nat ⇒ 's list ⇒ int list ⇒ (nat, 't) cval ⇒ 'a label
⇒ 's list ⇒ int list ⇒ (nat, 't) cval ⇒ bool"
("_ ⊢⇩_ ⟨_, _, _⟩ →⇘_⇙ ⟨_, _, _⟩" [61,61,61,61,61,61] 61)
where
step_u_t:
"⟦
∀ p < length N. ∃ pc st s' rs.
stepst P n (u ⊕ d) ((I ! p) (L ! p), [], s, True, []) (pc, st, s', True, rs);
∀ p < length N. u ⊕ d ⊢ snd (N ! p) (L ! p);
d ≥ 0;
bounded B s
⟧
⟹ (P, N, I, B) ⊢⇩n ⟨L, s, u⟩ →⇘Del⇙ ⟨L, s, u ⊕ d⟩" |
step_u_i:
"⟦
stepst P n u (pc_g, [], s, True, []) (_, _, _, True, _);
stepst P n u (pc_u, [], s, True, []) (_, _, s', _, r);
∀ p < length N. ∃ pc st s rs.
stepst P n u' ((I ! p) (L' ! p), [], s', True, []) (pc, st, s, True, rs);
(l, pc_g, Sil a, pc_u, l') ∈ fst (N ! p);
∀ p < length N. u' ⊢ snd (N ! p) (L' ! p);
L!p = l; p < length L; L' = L[p := l']; u' = [r→0]u;
bounded B s'
⟧
⟹ (P, N, I, B) ⊢⇩n ⟨L, s, u⟩ →⇘Act a⇙ ⟨L', s', u'⟩" |
step_u_s:
"⟦
stepst P n u (pc_g1, [], s, True, []) (_, _, _, True, _);
stepst P n u (pc_g2, [], s, True, []) (_, _, _, True, _);
stepst P n u (pc_u2, [], s, True, []) (_, _, s1, _, r2);
((∃ pc st s' f. stepst P n u (pc_u1, [], s, True, []) (pc, st, s', f, r1))
∨ (¬ (∃ pc st s' f r'. stepst P n u (pc_u1, [], s, True, []) (pc, st, s', f, r')) ∧ r1 = []));
stepst P n u (pc_u1, [], s1, True, []) ( _, _, s', _, _);
∀ p < length N. ∃ pc st s rs.
stepst P n u' ((I ! p) (L' ! p), [], s', True, []) (pc, st, s, True, rs);
(l1, pc_g1, In a, pc_u1, l1') ∈ fst (N ! p);
(l2, pc_g2, Out a, pc_u2, l2') ∈ fst (N ! q);
∀ p < length N. u' ⊢ snd (N ! p) (L' ! p);
L!p = l1; L!q = l2; p < length L; q < length L; p ≠ q;
L' = L[p := l1', q := l2']; u' = [(r1 @ r2)→0]u;
bounded B s'
⟧ ⟹ (P, N, I, B) ⊢⇩n ⟨L, s, u⟩ →⇘Syn a⇙ ⟨L', s', u'⟩"
inductive_cases[elim!]: "A ⊢⇩n ⟨L, s, u⟩ →⇘a⇙ ⟨L', s', u'⟩"
inductive steps_un ::
"('a, 't :: time, 's) unta ⇒ nat ⇒ 's list ⇒ int list ⇒ (nat, 't) cval
⇒ 's list ⇒ int list ⇒ (nat, 't) cval ⇒ bool"
("_ ⊢⇩_ ⟨_, _, _⟩ →* ⟨_, _, _⟩" [61,61,61,61,61,61] 61)
where
refl: "A ⊢⇩n ⟨L, s, u⟩ →* ⟨L, s, u⟩" |
step: "A ⊢⇩n ⟨L, s, u⟩ →* ⟨L', s', u'⟩ ⟹ A ⊢⇩n ⟨L', s', u'⟩ →⇘a⇙ ⟨L'', s'', u''⟩
⟹ A ⊢⇩n ⟨L, s, u⟩ →* ⟨L'', s'', u''⟩"
declare steps_un.intros[intro]
lemma stepI2:
"A ⊢⇩n ⟨L, s, u⟩ →* ⟨L'', s'', u''⟩" if
"A ⊢⇩n ⟨L', s', u'⟩ →* ⟨L'', s'', u''⟩" "A ⊢⇩n ⟨L, s, u⟩ →⇘a⇙ ⟨L', s', u'⟩"
using that
apply induction
apply (rule steps_un.step)
apply (rule refl)
apply assumption
apply simp
by (rule steps_un.step; assumption)
subsection ‹Equivalent State Network Automaton›
definition "stripp p ≡ map_option strip o p"
definition "stripfp p ≡ map_option stripf o p"
definition "striptp p ≡ map_option stript o p"
locale Equiv_TA_Defs =
fixes A :: "('a, 't, 's) unta"
and n :: nat
begin
abbreviation "N ≡ fst (snd A)"
abbreviation "P ≡ fst A"
abbreviation "I ≡ fst (snd (snd A))"
abbreviation "B ≡ snd (snd (snd A))"
abbreviation "P' ≡ stripfp P"
abbreviation "PF ≡ stripfp P"
abbreviation "PT ≡ striptp P"
definition "p ≡ length N"
definition "make_f pc_u ≡ λ s.
case (exec P' n (pc_u, [], s, True, []) []) of
None ⇒ []
| Some ((_, _, _, _, r), _) ⇒ r"
definition "make_mt pc_u ≡ λ s.
case (exec PT n (pc_u, [], s, True, []) []) of
None ⇒ None
| Some ((_, _, s', _, r), _) ⇒ Some s'"
definition "make_mf pc_u ≡ λ s.
case (exec PF n (pc_u, [], s, True, []) []) of
None ⇒ None
| Some ((_, _, s', _, r), _) ⇒ Some s'"
definition "make_c pc_g ≡ λ s.
case (exec PT n (pc_g, [], s, True, []) []) of
None ⇒ False
| Some ((_, _, _, f, _), _) ⇒ f"
definition "make_g pc_g ≡ λ s.
case (exec PT n (pc_g, [], s, True, []) []) of
None ⇒ []
| Some ((_, _, _, _, _), pcs) ⇒
List.map_filter (λ pc.
case P pc of
Some (CEXP ac) ⇒ Some ac
| _ ⇒ None
)
pcs"
definition "
state_trans_t i ≡
{(l, make_g pc_g, (a, make_c pc_g, make_mf pc_u), make_f pc_u, l') | l a l' pc_g pc_u.
(l, pc_g, a, pc_u, l') ∈ fst (N ! i)
}
"
abbreviation "state_trans ≡ state_trans_t"
definition "
state_pred i ≡ λ l s.
case (exec P' n ((I ! i) l, [], s, True, []) []) of
None ⇒ False
| Some ((_, _, _, f, _), _) ⇒ f ∧ bounded B s
"
definition "
state_inv i ≡ snd (N ! i)
"
definition "
state_ta ≡ (map (λ p. (state_trans p, state_inv p)) [0..<p], map state_pred [0..<p])
"
sublocale defs: Prod_TA_Defs state_ta .
lemma bounded_finite:
"finite {s. bounded B s}" (is "finite ?S")
proof -
have
"?S ⊆ {s. length s = length B ∧ (∀i<length B. fst (B ! i) < s ! i ∧ s ! i < snd (B ! i))}"
unfolding bounded_def by auto
moreover have "finite …" unfolding bounded_def using finite_lists_boundedI by force
ultimately show "finite ?S" by (rule finite_subset)
qed
lemma finite_state:
"∀ q < p. ∀ l. finite {s. (defs.P ! q) l s}"
proof safe
fix q l assume ‹q < p›
let ?S = "{s. (defs.P ! q) l s}"
from ‹q < p› have "?S ⊆ {s. bounded B s}"
unfolding state_ta_def state_pred_def by (auto split: option.splits)
moreover have "finite …" by (rule bounded_finite)
ultimately show "finite ?S" by (rule finite_subset)
qed
end
fun is_instr :: "'t instrc ⇒ bool" where
"is_instr (INSTR _) = True" |
"is_instr _ = False"
lemma step_stripf:
assumes
"is_instr cmd"
shows
"stepc cmd u (pc, st, s, f, rs) = step (stripf cmd) (pc, st, s, f, rs)"
proof (cases cmd)
case (INSTR instr)
with assms(1) show ?thesis
by (cases instr) (auto split: option.split)
next
case (CEXP x2)
with assms show ?thesis by auto
qed
lemma step_stript:
assumes
"is_instr cmd"
shows
"stepc cmd u (pc, st, s, f, rs) = step (stript cmd) (pc, st, s, f, rs)"
proof (cases cmd)
case (INSTR instr)
with assms(1) show ?thesis
by (cases instr) (auto split: option.split)
next
case (CEXP x2)
with assms show ?thesis by auto
qed
lemmas [intro] = stepsc.intros
lemma stepsc_f_complete:
assumes
"stepsc P n' u start end"
"⋀ pc' st s' f' rs cmd.
stepsc P n' u start (pc', st, s', f', rs) ⟹ P pc' = Some cmd
⟹ is_instr cmd"
shows
"steps (stripfp P) n' start end"
using assms proof (induction P ≡ P n' u ≡ u x4 ≡ start "end" arbitrary: start rule: stepsc.induct)
case 1
then show ?case unfolding stripfp_def by auto
next
case (2 cmd pc st m f rs s n' s')
have "is_instr cmd" if
"stepsc P n' u s (pc', st, s', f', rs)" "P pc' = Some cmd" for pc' st s' f' rs cmd
using 2(1,2) that by (auto intro: 2(5))
with 2(4) have *: "steps (stripfp P) n' s s'" by auto
show ?case
proof (cases cmd)
case (INSTR instr)
with 2(1) step_stripf have
"step (stripf cmd) (pc, st, m, f, rs) = Some s"
by (auto split: option.split_asm)
with 2(1-3) 2(5-) * show ?thesis unfolding stripfp_def by auto
next
case (CEXP ac)
with 2 show ?thesis by fastforce
qed
qed
lemma stepsc_f_sound:
assumes
"steps (stripfp P) n' start end"
"⋀ pc' st s' f' rs cmd.
stepsc P n' u start (pc', st, s', f', rs) ⟹ P pc' = Some cmd
⟹ is_instr cmd"
shows
"stepsc P n' u start end"
using assms proof (induction "stripfp P" n' start "end")
case (1 n start)
then show ?case by auto
next
case (2 instr pc st m f rs s n s')
from 2(2) obtain cmd where "P pc = Some cmd" unfolding stripfp_def by auto
show ?case
proof (cases cmd)
case prems: (INSTR instr)
with ‹P pc = _› 2(2) step_stripf[of cmd, symmetric] 2(1) have step:
"stepc cmd u (pc, st, m, f, rs) = Some s"
unfolding stripfp_def by auto
with ‹P pc = _› have "is_instr cmd" if
"stepsc P n u s (pc', st, s', f', rs)" "P pc' = Some cmd" for pc' st s' f' rs cmd
using that unfolding stripfp_def by (force intro: 2(5))
with 2(4) have "stepsc P n u s s'" by auto
with step ‹P pc = _› show ?thesis unfolding stripfp_def by auto
next
case prems: (CEXP ac)
from ‹P pc = _› 2(5) have "is_instr cmd" by blast
with prems show ?thesis by auto
qed
qed
definition
"time_indep P n start ≡
∀ pc' st s' f' rs cmd u.
stepsc P n u start (pc', st, s', f', rs) ∧ P pc' = Some cmd
⟶ is_instr cmd"
lemma stepsc_t_complete:
assumes
"stepsc P n' u start end"
"⋀ pc' st s' f' rs ac.
stepsc P n' u start (pc', st, s', f', rs) ⟹ P pc' = Some (CEXP ac) ⟹ u ⊢⇩a ac"
shows
"steps (striptp P) n' start end"
using assms proof (induction P ≡ P n' u ≡ u x4 ≡ start "end" arbitrary: start rule: stepsc.induct)
case 1
then show ?case unfolding stripfp_def by auto
next
case (2 cmd pc st m f rs s n' s')
have "u ⊢⇩a ac" if
"stepsc P n' u s (pc', st, s', f', rs)" "P pc' = Some (CEXP ac)" for pc' st s' f' rs ac
using 2(1,2) that by (auto intro: 2(5))
with 2(4) have *: "steps (striptp P) n' s s'" by auto
show ?case
proof (cases cmd)
case (INSTR instr)
with 2(1) step_stript have
"step (stript cmd) (pc, st, m, f, rs) = Some s"
by (auto split: option.split_asm)
with 2(1-3) 2(5-) * show ?thesis unfolding striptp_def by auto
next
case (CEXP ac)
with 2(1-3) have "u ⊢⇩a ac" by (auto intro: 2(5))
with 2(1) have
"step (stript cmd) (pc, st, m, f, rs) = Some s"
using ‹cmd = _› by auto
with 2(1-3) 2(5-) * show ?thesis unfolding striptp_def by auto
qed
qed
lemma stepsc_t_complete2:
assumes
"stepsc P n' u start (pc', st', s', f', rs')"
"⋀ pc' st s' f' rs ac.
stepsc P n' u start (pc', st, s', f', rs) ⟹ P pc' = Some (CEXP ac) ⟹ u ⊢⇩a ac"
shows
"steps (striptp P) n' start (pc', st', s', f', rs') ∧ (∀ ac. P pc' = Some (CEXP ac) ⟶ u ⊢⇩a ac)"
using assms
proof (induction P ≡ P n' u ≡ u x4 ≡ start "(pc', st', s', f', rs')" arbitrary: start rule: stepsc.induct)
case 1
then show ?case unfolding stripfp_def by blast
next
case (2 cmd pc st m f rs s n')
have "u ⊢⇩a ac" if
"stepsc P n' u s (pc', st, s', f', rs)" "P pc' = Some (CEXP ac)" for pc' st s' f' rs ac
using 2(1,2) that by (auto intro: 2(5))
with 2(4) have *:
"steps (striptp P) n' s (pc', st', s', f', rs')" "∀ac. P pc' = Some (CEXP ac) ⟶ u ⊢⇩a ac"
by auto
show ?case
proof (cases cmd)
case (INSTR instr)
with 2(1) step_stript have
"step (stript cmd) (pc, st, m, f, rs) = Some s"
by (auto split: option.split_asm)
with 2(1-3) 2(5-) * show ?thesis unfolding striptp_def by auto
next
case (CEXP ac)
with 2(1-3) have "u ⊢⇩a ac" by (auto intro: 2(5))
with 2(1) have
"step (stript cmd) (pc, st, m, f, rs) = Some s"
using ‹cmd = _› by auto
with 2(1-3) 2(5-) * show ?thesis unfolding striptp_def by auto
qed
qed
lemma stepsc_t_visitedc:
assumes
"stepsc P n' u start end"
"⋀ pc' st s' f' rs.
stepsc P n' u start (pc', st, s', f', rs) ⟹ Q pc'"
shows "∃ pcs. visitedc P n' u start end pcs
∧ (∀ pc ∈ set pcs. Q pc)"
using assms by (induction) (fastforce intro!: visitedc.intros)+
lemma visitedc_t_visited:
assumes
"visitedc P n' u start end pcs"
"⋀ pc' ac. pc' ∈ set pcs ⟹ P pc' = Some (CEXP ac) ⟹ u ⊢⇩a ac"
shows
"visited (striptp P) n' start end pcs
∧ (∀ pc ac. pc' ∈ set pcs ∧ P pc' = Some (CEXP ac) ⟶ u ⊢⇩a ac)"
using assms
proof (induction P ≡ P n' u ≡ u x4 ≡ start "end" pcs arbitrary: start rule: visitedc.induct)
case 1
then show ?case by (auto intro: visited.intros)
next
case (2 cmd pc st m f rs s n' s' pcs)
have "u ⊢⇩a ac" if
"pc' ∈ set pcs" "P pc' = Some (CEXP ac)" for pc' ac
using 2(1,2) that by (auto intro: 2(5))
with 2(4) have *:
"visited (striptp P) n' s s' pcs" "∀pc ac. pc' ∈ set pcs ∧ P pc' = Some (CEXP ac) ⟶ u ⊢⇩a ac"
by auto
show ?case
proof (cases cmd)
case (INSTR instr)
with 2(1) step_stript have
"step (stript cmd) (pc, st, m, f, rs) = Some s"
by (auto split: option.split_asm)
with 2(1-3) 2(5-) * show ?thesis unfolding striptp_def by (auto intro: visited.intros)
next
case (CEXP ac)
with 2(1-3) have "u ⊢⇩a ac" by (auto intro: 2(5))
with 2(1) have
"step (stript cmd) (pc, st, m, f, rs) = Some s"
using ‹cmd = _› by auto
with 2(1-3) 2(5-) * show ?thesis unfolding striptp_def by (auto intro: visited.intros)
qed
qed
lemma stepsc_t_sound:
assumes
"steps (striptp P) n' start end"
"⋀ pc' st s' f' rs ac.
stepsc P n' u start (pc', st, s', f', rs) ⟹ P pc' = Some (CEXP ac) ⟹ u ⊢⇩a ac"
shows
"stepsc P n' u start end"
using assms proof (induction "striptp P" n' start "end")
case (1 n start)
then show ?case by auto
next
case (2 instr pc st m f rs s n s')
from 2(2) obtain cmd where "P pc = Some cmd" unfolding striptp_def by auto
show ?case
proof (cases cmd)
case prems: (INSTR instr)
with ‹P pc = _› 2(2) step_stript[of cmd, symmetric] 2(1) have step:
"stepc cmd u (pc, st, m, f, rs) = Some s"
unfolding striptp_def by auto
with ‹P pc = _› have "u ⊢⇩a ac" if
"stepsc P n u s (pc', st, s', f', rs)" "P pc' = Some (CEXP ac)" for pc' st s' f' rs ac
using that unfolding striptp_def by (force intro: 2(5))
with 2(4) have "stepsc P n u s s'" by auto
with step ‹P pc = _› show ?thesis unfolding striptp_def by auto
next
case prems: (CEXP ac)
with ‹P pc = _› 2(2) have [simp]: "P pc = Some (CEXP ac)" by auto
then have "u ⊢⇩a ac" by (auto intro: 2(5))
with 2(2,1) ‹cmd = _› have step:
"stepc cmd u (pc, st, m, f, rs) = Some s"
unfolding striptp_def by auto
with ‹P pc = Some cmd› have "u ⊢⇩a ac" if
"stepsc P n u s (pc', st, s', f', rs)" "P pc' = Some (CEXP ac)" for pc' st s' f' rs ac
using that unfolding striptp_def by (force intro: 2(5))
with 2(4) have "stepsc P n u s s'" by auto
with step ‹P pc = Some cmd› show ?thesis unfolding striptp_def by auto
qed
qed
lemma stepsc_visitedc:
"∃ cc. visitedc P n u start end cc" if "stepsc P n u start end"
using that by induction (auto intro: visitedc.intros)
lemma visitedc_stepsc:
"stepsc P n u start end" if "visitedc P n u start end cc"
using that by (induction; blast)
lemma steps_visited:
"∃ cc. visited P n start end cc" if "steps P n start end"
using that by induction (auto intro: visited.intros)
lemma visited_steps:
"steps P n start end" if "visited P n start end cc"
using that by (induction; blast)
context
fixes P n u start
assumes constraints_conj: "∀ pc' st s' f' rs ac.
stepsc P n u start (pc', st, s', f', rs) ∧ P pc' = Some (CEXP ac) ⟶ u ⊢⇩a ac"
begin
lemma stepsc_t_sound':
assumes
"steps (striptp P) n start end"
shows
"stepsc P n u start end"
using assms constraints_conj by (auto intro: stepsc_t_sound)
lemma stepsc_t_complete':
assumes
"stepsc P n u start end"
shows
"steps (striptp P) n start end"
using assms constraints_conj by (auto intro: stepsc_t_complete)
lemma stepsc_t_complete'':
assumes
"stepsc P n u start end"
shows
"∃ pcs. visitedc P n u start end pcs ∧ (∀ pc ∈ set pcs. ∀ ac. P pc = Some (CEXP ac) ⟶ u ⊢⇩a ac)"
using assms constraints_conj by (auto intro: stepsc_t_complete stepsc_t_visitedc)
lemma stepsc_t_visited:
assumes
"stepsc P n u start end"
shows
"∃ pcs. visited (striptp P) n start end pcs ∧ (∀ pc ∈ set pcs. ∀ ac. P pc = Some (CEXP ac) ⟶ u ⊢⇩a ac)"
using stepsc_t_complete''[OF assms] visitedc_t_visited by blast
lemma stepst_t_complete:
assumes
"stepst P n u start end"
shows
"∃ pcs. exec (striptp P) n start [] = Some (end, pcs) ∧ (∀ pc ∈ set pcs. ∀ ac. P pc = Some (CEXP ac) ⟶ u ⊢⇩a ac)"
using assms by (auto dest!: stepsc_t_visited visited_exec' simp: striptp_def stepst_def)
lemma stepst_t_equiv:
"(∃ pcs'. exec (striptp P) n start pcs = Some ((pc, st, m, f, rs), pcs'))
⟷ stepst P n u start (pc, st, m, f, rs)"
apply safe
apply (drule exec_steps)
unfolding stepst_def
apply safe
apply (rule stepsc_t_sound'; assumption)
apply (simp add: striptp_def)
apply safe
subgoal for z
by (cases z) auto
by (auto dest!: stepsc_t_complete' steps_exec simp: striptp_def)
end
context
fixes P n start
assumes time_indep: "time_indep P n start"
begin
lemma time_indep':
"⋀ pc' st s' f' rs cmd.
stepsc P n u start (pc', st, s', f', rs) ⟹ P pc' = Some cmd
⟹ is_instr cmd"
using time_indep unfolding time_indep_def by blast
lemma stepsc_f_complete':
assumes
"stepsc P n u start end"
shows
"steps (stripfp P) n start end"
using assms time_indep' by (auto intro: stepsc_f_complete[where P = P])
lemma stepsc_f_sound':
assumes
"steps (stripfp P) n start end"
shows
"stepsc P n u start end"
using assms time_indep' by (auto intro: stepsc_f_sound[where P = P])
lemma stepsc_f_equiv:
"steps (stripfp P) n start end ⟷ stepsc P n u start end"
using stepsc_f_sound' stepsc_f_complete' by fast
lemma stepst_f_equiv:
"(∃ pcs'. exec (stripfp P) n start pcs = Some ((pc, st, m, f, rs), pcs'))
⟷ stepst P n u start (pc, st, m, f, rs)"
apply safe
apply (drule exec_steps)
unfolding stepst_def
apply safe
apply (rule stepsc_f_sound'; assumption)
apply (simp add: stripfp_def)
apply safe
subgoal for z
by (cases z) auto
by (auto dest!: stepsc_f_complete' steps_exec simp: stripfp_def)
end
lemma exec_acc:
assumes "exec P n s pcs = Some (s', pcs')"
shows "∃ pcs''. pcs' = pcs'' @ pcs"
using assms by (induction P n s pcs rule: exec.induct; force split: option.split_asm if_split_asm)
lemma exec_acc':
assumes "Some (s', pcs') = exec P n s pcs"
shows "∃ pcs''. pcs' = pcs'' @ pcs"
using assms
using assms exec_acc by metis
lemma exec_min_steps:
assumes "exec P n s pcs = Some (s', pcs' @ pcs)"
shows "exec P (length pcs') s pcs = Some (s', pcs' @ pcs)"
using assms proof (induction n arbitrary: s pcs s' pcs')
case 0
then show ?case by auto
next
case (Suc n)
obtain pc st m f rs pc' st' m' f' rs' where [simp]:
"s = (pc, st, m, f, rs)" "s' = (pc', st', m', f', rs')"
using prod.exhaust by metis
from Suc obtain instr where "P pc = Some instr" by (auto split: option.splits if_splits)
show ?case
proof (cases "instr = HALT")
case True
with ‹P pc = _› Suc show ?thesis by auto
next
case False
with Suc.prems ‹P pc = _› obtain s'' where s'':
"step instr s = Some s''" "exec P n s'' (pc # pcs) = Some (s', pcs' @ pcs)"
by (auto split: option.splits)
with exec_acc[OF this(2)] obtain pcs'' where "pcs' = pcs'' @ [pc]" by auto
with Suc.IH[of s'' "pc # pcs" s' "pcs''"] ‹P pc = _› False s'' show ?thesis by auto
qed
qed
lemma exec_steps_visited:
assumes
"exec P (length pcs') s pcs = Some (s', pcs' @ pcs)"
"steps P (length pcs') s (pc, st, m, f, rs)"
shows "pc ∈ set pcs'"
using assms proof (induction P ≡ P "length pcs'" s pcs arbitrary: pc st m f rs pcs' rule: exec.induct)
case 1
then show ?case by simp
next
case (2 n pc' st' m' f' rs' pcs pcs')
from this(2)[symmetric] this(3) obtain instr where "P pc' = Some instr" by (cases "P pc'") auto
show ?case
proof (cases "instr = HALT")
case True
with "2.prems" ‹P pc' = _› ‹Suc n = _›[symmetric] show ?thesis by (force elim: steps.cases)
next
case False
with 2 obtain pcs'' where "pcs' = pcs'' @ [pc']"
apply atomize_elim
by (erule exec.elims) (auto dest: exec_acc' split: option.split_asm if_split_asm)
with False 2 ‹P pc' = _› ‹Suc n = _›[symmetric] show ?thesis
by (auto split: option.split_asm elim: steps.cases)
qed
qed
lemma stepsc_mono:
assumes "stepsc P n u start end" "n' ≥ n"
shows "stepsc P n' u start end"
using assms proof (induction arbitrary: n')
case (1 prog n u start)
then show ?case by (cases n') auto
next
case (2 cmd u pc st m f rs s prog n s')
then show ?case by (cases n') auto
qed
lemma stepst_mono:
assumes "stepst P n u start end" "n' ≥ n"
shows "stepst P n' u start end"
using assms stepsc_mono unfolding stepst_def by blast
definition
"state_indep P n ≡
∀ pc f pc' st f' rs u s1 s1' s2 s2' rs1 rs2.
stepsc P n u (pc, st, s1, f, rs) (pc', st, s1', f', rs1) ∧
stepsc P n u (pc, st, s2, f, rs) (pc', st, s2', f', rs2)
⟶ rs1 = rs2"
lemma exec_len:
"n ≥ (length pcs' - length pcs)" if "exec P n s pcs = Some (s', pcs')"
using that
by (induction P n s pcs arbitrary: rule: exec.induct)
(force split: option.split_asm if_split_asm)+
lemma steps_striptp_stepsc:
assumes "
⋀ pc st m f rs ac.
steps (striptp P) n s' (pc, st, m, f, rs) ⟹ P pc = Some (CEXP ac)
⟹ u' ⊢⇩a ac
"
and "steps (striptp P) n s' s''"
shows "stepsc P n u' s' s''"
using assms(2,1)
proof (induction "striptp P" n s' s'')
case (1 n start)
show ?case by (rule stepsc.intros)
next
case (2 cmd pc st m f rs s n s')
have "u' ⊢⇩a ac"
if "P pc = Some (CEXP ac)" "UPPAAL_Asm.steps (striptp P) n s (pc, st, m, f, rs)"
for pc st m f rs ac
using that 2(1-3) by - (rule 2(5); force)
with 2(4) have "stepsc P n u' s s'" by auto
with 2(1-3) show ?case
apply (cases "P pc")
apply (simp add: striptp_def)
subgoal for cmd'
apply (cases cmd')
subgoal
by (force split: option.split simp: striptp_def)
subgoal
by (rule stepsc.intros) (auto intro!: 2(5) simp: striptp_def)
done
done
qed
locale Equiv_TA =
Equiv_TA_Defs A n for A :: "('a, 't :: time, 's) unta" and n :: nat +
fixes L :: "'s list" and s :: "int list"
assumes states[intro]: "L ∈ defs.states' s"
and pred_time_indep:
"∀ s. ∀ L ∈ defs.states' s. ∀ q < p. time_indep P n ((I ! q) (L ! q), [], s, True, [])"
and upd_time_indep:
"∀ l pc_g a l' pc_u s. ∀ q < p. (l, pc_g, a, pc_u, l') ∈ fst (N ! q)
⟶ time_indep P n (pc_u, [], s, True, [])"
and clock_conj:
"∀ l pc_g a l' pc_u s u. ∀ q < p. (l, pc_g, a, pc_u, l') ∈ fst (N ! q) ∧
(∃ pc' st s' rs. stepst P n u (pc_g, [], s, True, []) (pc', st, s', True, rs)) ⟶
(∀ pc' st s' f' rs ac.
stepsc P n u (pc_g, [], s, True, []) (pc', st, s', f', rs) ∧ P pc' = Some (CEXP ac) ⟶
u ⊢⇩a ac)"
assumes Len: "length N = length I"
and inv: "∀ q < p. ∃ pc st s' rs pcs.
exec P' n ((I ! q) (L ! q), [], s, True, []) [] = Some ((pc, st, s', True, rs), pcs)"
and bounded: "bounded B s"
begin
lemma length_defs_N[simp]:
"length defs.N = p"
unfolding p_def state_ta_def by simp
lemma length_defs_P[simp]:
"length defs.P = p"
unfolding p_def state_ta_def by simp
lemma inv':
"∀p<length defs.P. (defs.P ! p) (L ! p) s"
using inv bounded unfolding state_ta_def state_pred_def by (force simp: p_def)
lemma inv'':
"∃ pc st s' rs. stepst P n u' ((I ! q) (L ! q), [], s, True, []) (pc, st, s', True, rs)"
if "q < p" for u'
proof -
from pred_time_indep that have "time_indep P n ((I ! q) (L ! q), [], s, True, [])" by blast
with inv that stepst_f_equiv[symmetric] show ?thesis by blast
qed
lemma A_simp[simp]:
"PP = P" "N' = N" "I' = I" "B' = B" if "A = (PP, N', I', B')"
using that by auto
lemma A_unfold:
"A = (P, N, I, B)"
by simp
sublocale prod: Prod_TA state_ta by standard (auto simp: inv')
lemma inv_simp:
"snd (defs.N ! q) (L' ! q) = snd (N ! q) (L' ! q)" if "q < p" for L'
using that unfolding state_ta_def state_inv_def by simp
lemma defs_p_eq[simp]:
"defs.p = p"
by (simp add: defs.p_def p_def)
lemma ball_lessThan[simp]:
"(∀ x ∈ {..<m}. Q x) ⟷ (∀ x < m. Q x)"
by auto
lemma trans_state_taD:
assumes "(l, g, (a, c, m), f, l') ∈ fst (defs.N ! q)" "q < p"
shows
"(l, g, (a, c, m), f, l') ∈ state_trans_t q"
using assms unfolding state_ta_def by simp
lemma N_transD:
assumes "(l, pc_g, a, pc_u, l') ∈ fst (N ! q)" "q < p"
shows "(l, make_g pc_g, (a, make_c pc_g, make_mf pc_u), make_f pc_u, l') ∈ fst (defs.N ! q)"
using assms unfolding state_ta_def state_trans_t_def by auto
lemma pred_time_indep':
"∀ L' s' u'. ∀ p' < p. A ⊢⇩n ⟨L, s, u⟩ →* ⟨L', s', u'⟩
⟶ time_indep P n ((I ! p') (L' ! p'), [], s', True, [])"
using pred_time_indep oops
lemma P_steps_upd:
assumes
"Some s'' = make_mf pc_u s'" "(l, pc_g, a, pc_u, l') ∈ fst (N ! q)" "q < p"
shows
"∃ pc st f. stepst P n u' (pc_u, [], s', True, []) (pc, st, s'', f, make_f pc_u s')"
proof -
from assms upd_time_indep have *: "time_indep P n (pc_u, [], s', True, [])" by auto
from assms(1) ‹q < p› obtain pc st f rs pcs where
"exec PF n (pc_u, [], s', True, []) [] = Some ((pc, st, s'', f, rs), pcs)"
unfolding make_mf_def state_ta_def by (fastforce split: option.splits)
with stepst_f_equiv[OF *] show ?thesis unfolding make_f_def by fastforce
qed
lemma P_steps_reset:
assumes
"q < p" "(l, pc_g, a, pc_u, l') ∈ fst (N ! q)"
shows
"(∃pc st s'' f. stepst P n u (pc_u, [], s', True, []) (pc, st, s'', f, make_f pc_u s')) ∨
(∄pc st s'' f r'. stepst P n u (pc_u, [], s', True, []) (pc, st, s'', f, r')) ∧
make_f pc_u s' = []"
proof (cases "∃pc st s'' f r'. stepst P n u (pc_u, [], s', True, []) (pc, st, s'', f, r')")
case True
then obtain pc st s'' f r' where *:
"stepst P n u (pc_u, [], s', True, []) (pc, st, s'', f, r')"
by blast
from assms upd_time_indep have "time_indep P n (pc_u, [], s', True, [])" by auto
from * stepst_f_equiv[OF this, symmetric, where pcs = "[]"] show ?thesis
unfolding make_f_def by (force split: option.split)
next
case False
from assms upd_time_indep have "time_indep P n (pc_u, [], s', True, [])" by auto
from False stepst_f_equiv[OF this, where pcs = "[]"] show ?thesis
unfolding make_f_def by (auto split: option.split)
qed
lemma steps_P_reset:
assumes
"(∃pc st s'' f. stepst P n u (pc_u, [], s', True, []) (pc, st, s'', f, r)) ∨
(∄pc st s'' f r'. stepst P n u (pc_u, [], s', True, []) (pc, st, s'', f, r')) ∧ r = []"
"q < p" "(l, pc_g, a, pc_u, l') ∈ fst (N ! q)"
shows "make_f pc_u s' = r"
using assms(1)
proof (safe, goal_cases)
case prems: (1 pc st s'' f)
from assms upd_time_indep have "time_indep P n (pc_u, [], s', True, [])" by auto
from stepst_f_equiv[OF this, symmetric] prems ‹q < p› obtain pc st f pcs where
"exec PF n (pc_u, [], s', True, []) [] = Some ((pc, st, s'', f, r), pcs)"
unfolding make_f_def state_ta_def by (fastforce split: option.splits)
then show ?case unfolding make_f_def by (auto split: option.split)
next
case prems: 2
have "exec PF n (pc_u, [], s', True, []) [] = None"
proof (cases "exec PF n (pc_u, [], s', True, []) []")
case None
then show ?thesis .
next
case (Some a)
obtain pc'' st'' s'' f'' rs'' pcs'' where "a = ((pc'', st'', s'', f'', rs''), pcs'')"
by (cases a) auto
from assms upd_time_indep have "time_indep P n (pc_u, [], s', True, [])" by auto
from stepst_f_equiv[OF this] ‹_ = Some a› prems ‹a = _› show ?thesis by auto metis
qed
then show ?case unfolding make_f_def by simp
qed
lemma steps_P_upd:
assumes
"stepst P n u' (pc_u, [], s', True, []) (pc, st, s'', f, r)"
"q < p" "(l, pc_g, a, pc_u, l') ∈ fst (N ! q)"
shows
"Some s'' = make_mf pc_u s'" (is "?A") "r = make_f pc_u s'" (is "?B")
proof -
from assms upd_time_indep have "time_indep P n (pc_u, [], s', True, [])" by auto
from stepst_f_equiv[OF this, symmetric] assms(1) ‹q < p› obtain pc st f pcs where
"exec PF n (pc_u, [], s', True, []) [] = Some ((pc, st, s'', f, r), pcs)"
unfolding make_mf_def state_ta_def by (fastforce split: option.splits)
then show ?A ?B unfolding make_f_def make_mf_def by (auto split: option.split)
qed
lemma steps_P_guard:
assumes
"stepst P n u' (pc_g, [], s', True, []) (pc, st, s'', True, rs)"
"q < p" "(l, pc_g, a, pc_u, l') ∈ fst (N ! q)"
shows
"make_c pc_g s'" (is "?A") "u' ⊢ make_g pc_g s'" (is "?B")
proof -
from stepst_t_complete[OF _ assms(1)] clock_conj assms obtain pcs where
"exec PT n (pc_g, [], s', True, []) [] = Some ((pc, st, s'', True, rs), pcs)"
"∀ pc∈set pcs. ∀ac. P pc = Some (CEXP ac) ⟶ u' ⊢⇩a ac"
by fastforce
then show ?A ?B unfolding make_c_def make_g_def
by (auto split: option.split instrc.split_asm simp: list_all_iff set_map_filter clock_val_def)
qed
lemma P_steps_guard:
assumes
"make_c pc_g s'" "u' ⊢ make_g pc_g s'"
"q < p" "(l, pc_g, a, pc_u, l') ∈ fst (N ! q)"
shows
"∃ pc s'' st rs. stepst P n u' (pc_g, [], s', True, []) (pc, st, s'', True, rs)"
proof -
from assms(1) ‹q < p› obtain pc st s'' rs pcs where *:
"exec PT n (pc_g, [], s', True, []) [] = Some ((pc, st, s'', True, rs), pcs)"
unfolding make_c_def state_ta_def by (fastforce split: option.splits)
with exec_min_steps[of PT n _ "[]" _ pcs] have **:
"exec PT (length pcs) (pc_g, [], s', True, []) [] = Some ((pc, st, s'', True, rs), pcs @ [])"
by auto
from * assms(2) have
"u' ⊢ List.map_filter (λpc. case P pc of
None ⇒ None
| Some (INSTR xa) ⇒ Map.empty xa
| Some (CEXP xa) ⇒ Some xa) pcs" unfolding make_g_def
by auto
moreover from ** exec_steps_visited[of PT pcs _ "[]"] have "pc ∈ set pcs"
if "steps PT (length pcs) (pc_g, [], s', True, []) (pc, st, m, f, rs)" for pc st m f rs
using that by fastforce
ultimately have "u' ⊢⇩a ac"
if "steps PT (length pcs) (pc_g, [], s', True, []) (pc, st, m, f, rs)" "P pc = Some (CEXP ac)"
for pc st m f rs ac
using that by (auto 4 3 split: option.splits simp: list_all_iff set_map_filter clock_val_def)
moreover from ** have
"steps PT (length pcs) (pc_g, [], s', True, []) (pc, st, s'', True, rs)" "PT pc = Some HALT"
by (auto dest: exec_steps)
ultimately have "stepst P (length pcs) u' (pc_g, [], s', True, []) (pc, st, s'', True, rs)"
by (auto intro: steps_striptp_stepsc simp: stepst_def striptp_def elim: stript.elims)
moreover from exec_len[OF *] have "n ≥ length pcs" by simp
ultimately show ?thesis by (blast intro: stepst_mono)
qed
lemma P_bounded:
assumes
"(defs.P ! q) (L' ! q) s'" "q < p"
shows "bounded B s'"
using assms unfolding state_pred_def state_ta_def by (auto split: option.splits)
lemma P_steps:
assumes
"(defs.P ! q) (L' ! q) s'"
"q < p" "L' ∈ defs.states' s'"
shows
"∃ pc st s'' rs. stepst P n u' ((I ! q) (L' ! q), [], s', True, []) (pc, st, s'', True, rs)"
proof -
from assms pred_time_indep have *: "time_indep P n ((I ! q) (L' ! q), [], s', True, [])" by auto
from assms(1) ‹q < p› obtain pc st s'' rs pcs where
"exec PF n ((I ! q) (L' ! q), [], s', True, []) [] = Some ((pc, st, s'', True, rs), pcs)"
unfolding state_pred_def state_ta_def by (auto split: option.splits)
with stepst_f_equiv[OF *] show ?thesis by blast
qed
lemma steps_P:
assumes
"stepst P n u' ((I ! q) (L' ! q), [], s', True, []) (pc, st, s'', True, rs)"
"q < p" "L' ∈ defs.states' s'"
"bounded B s'"
shows
"(defs.P ! q) (L' ! q) s'"
proof -
from assms pred_time_indep have "time_indep P n ((I ! q) (L' ! q), [], s', True, [])" by auto
from stepst_f_equiv[OF this] assms(1) obtain pcs' where
"exec PF n ((I ! q) (L' ! q), [], s', True, []) [] = Some ((pc, st, s'', True, rs), pcs')"
by blast
with ‹q < p› ‹bounded B s'› show ?thesis unfolding state_pred_def state_ta_def by simp
qed
lemma P_iff:
"(∃ pc st rs s''. stepst P n u' ((I ! q) (L' ! q), [], s', True, []) (pc, st, s'', True, rs)
∧ bounded B s')
⟷ (defs.P ! q) (L' ! q) s'" if "q < p" "L' ∈ defs.states' s'"
using that by (metis steps_P P_steps P_bounded)
lemma states'_updI':
assumes "(L' ! q, g, (a, c, m), f, l') ∈ fst (defs.N ! q)" "L' ∈ defs.states' s''"
shows "L'[q := l'] ∈ defs.states' s'"
using assms
unfolding prod.states'_simp[of s' s'']
unfolding Product_TA_Defs.states_def
apply clarsimp
subgoal for p
by (cases "p = q"; force simp: prod.trans_of_N_s_2[simplified] Prod_TA_Defs.N_s_length)
done
lemma states'_updI:
assumes "(L ! q, g, (a, c, m), f, l') ∈ fst (defs.N ! q)"
shows "L[q := l'] ∈ defs.states' s'"
using assms by (auto intro: states'_updI')
lemma states'_updI'':
assumes
"(L' ! q, g, (a, c, m), f, l') ∈ fst (defs.N ! q)"
"(L' ! q', g', (a', c', m'), f', l'') ∈ fst (defs.N ! q')"
"L' ∈ defs.states' s''" "q ≠ q'"
shows "L'[q := l', q' := l''] ∈ defs.states' s'"
using assms by (auto intro: states'_updI')
lemma equiv_sound:
assumes step: "state_ta ⊢ ⟨L, s, u⟩ →⇘a⇙ ⟨L', s', u'⟩"
shows "A ⊢⇩n ⟨L, s, u⟩ →⇘a⇙ ⟨L', s', u'⟩"
using step proof cases
case (step_sn_t N d I)
then show ?thesis
apply simp
apply (subst A_unfold)
apply (frule prod.A_simp(1))
apply (frule prod.A_simp(2))
apply (rule step_u_t)
using inv'' bounded by (auto simp: inv_simp p_def)
next
case (step_sn_i l g a c m f l' N p r I)
then show ?thesis
apply (simp)
apply (frule prod.A_simp(1))
apply (frule prod.A_simp(2))
apply (simp add: Prod_TA_Defs.N_s_length)
apply (subst A_unfold)
apply (drule trans_state_taD)
apply assumption
unfolding state_trans_t_def
apply safe
apply (drule (2) P_steps_upd)
apply (drule (3) P_steps_guard)
apply safe
apply (rule step_u_i)
subgoals ‹∀p<length local.N. ∃pc. _›
apply safe
apply (rule P_steps)
apply (fastforce simp: p_def)
apply (fastforce simp: p_def)
by (metis Prod_TA_Defs'.states'_simp Prod_TA_Defs'.states_step local.step states)
by (auto simp: inv_simp p_def Prod_TA_Defs.N_s_length intro!: P_bounded)
next
case (step_sn_s l1 g1 a ci mi f1 l1' N p l2 g2 co mo f2 l2' q r1 r2 I)
then show ?thesis
apply (simp)
apply (frule prod.A_simp(1))
apply (frule prod.A_simp(2))
apply (simp add: Prod_TA_Defs.N_s_length)
apply (subst A_unfold)
apply (drule trans_state_taD)
apply assumption
apply (drule trans_state_taD)
apply assumption
subgoal
unfolding state_trans_t_def
apply safe
apply (drule (2) P_steps_upd)
apply (drule (2) P_steps_upd)
apply (drule (3) P_steps_guard)
apply (drule (3) P_steps_guard)
apply safe
apply (rule step_u_s)
prefers ‹_ ∨ _›
apply (rule P_steps_reset; force)
subgoals ‹∀pa<length local.N. ∃pc. _›
apply safe
apply (rule P_steps)
apply (fastforce simp: p_def)
apply (fastforce simp: p_def)
by (metis Prod_TA_Defs'.states'_simp Prod_TA_Defs'.states_step local.step states)
by (auto simp: inv_simp p_def Prod_TA_Defs.N_s_length intro!: P_bounded)
done
qed
lemma state_ta_unfold:
"state_ta = (defs.N, defs.P)"
by simp
lemma equiv_complete:
assumes step: "A ⊢⇩n ⟨L, s, u⟩ →⇘a⇙ ⟨L', s', u'⟩"
shows "state_ta ⊢ ⟨L, s, u⟩ →⇘a⇙ ⟨L', s', u'⟩"
using step proof cases
case (step_u_t N P d I)
note [simp] = A_simp[OF this(1)]
from step_u_t(2-) show ?thesis
by (auto simp: state_ta_def p_def state_inv_def intro: step_sn_t)
next
case (step_u_i P pc_g uu uv uw ux pc_u uy uz va r N I l a l' p)
note [simp] = A_simp[OF this(1)]
from step_u_i(2-) show ?thesis
apply -
apply (simp add: Prod_TA_Defs.N_s_length)
apply (subst state_ta_unfold)
apply (frule steps_P_guard(1))
apply assumption
apply (simp; fail)
apply (drule steps_P_guard(2))
apply assumption
apply (simp; fail)
apply (frule steps_P_upd(1))
apply assumption
apply (simp; fail)
apply (drule steps_P_upd(2))
apply assumption
apply (simp; fail)
apply (drule N_transD)
apply assumption
apply (rule step_sn_i)
apply assumption
apply (simp add: state_ta_def p_def state_inv_def state_pred_def; fail)+
apply (simp add: Prod_TA_Defs.N_s_length; fail)
apply (simp add: state_ta_def p_def state_inv_def state_pred_def; fail)+
by (auto 4 3 simp: p_def intro: steps_P intro!: states'_updI)
next
case (step_u_s P pc_g1 vb vc vd ve pc_g2 vf vg vh vi pc_u2 vj vk s1 vl r2 pc_u1 r1 vm vn vo vp
N I l1 a l1' p' l2 l2' q
)
note [simp] = A_simp[OF this(1)]
from ‹q < length L› have "q < p" by (simp add: Prod_TA_Defs.N_s_length)
from step_u_s(2-) show ?thesis
apply -
apply (simp add: Prod_TA_Defs.N_s_length)
apply (subst state_ta_unfold)
apply (frule steps_P_guard(1))
apply assumption
apply (simp; fail)
apply (drule steps_P_guard(2))
apply assumption
apply (simp; fail)
apply (frule steps_P_guard(1))
apply (rule ‹q < p›)
apply (simp; fail)
apply (drule steps_P_guard(2))
apply (rule ‹q < p›)
apply (simp; fail)
apply (frule steps_P_upd(1))
apply (rule ‹q < p›)
apply (simp; fail)
apply (drule steps_P_upd(2))
apply (rule ‹q < p›)
apply (simp; fail)
apply (drule steps_P_reset[simplified])
apply assumption
apply (simp; fail)
apply (frule steps_P_upd(1))
apply assumption
apply (simp; fail)
apply (drule steps_P_upd(2))
apply assumption
apply (simp; fail)
apply (drule N_transD)
apply assumption
apply (drule N_transD)
apply assumption
apply (rule step_sn_s)
apply assumption
apply assumption
apply (all ‹(auto; fail)?›)
apply (simp add: state_ta_def p_def state_inv_def state_pred_def; fail)
apply (simp add: Prod_TA_Defs.N_s_length; fail)
apply (simp add: Prod_TA_Defs.N_s_length; fail)
apply (clarsimp simp: p_def)
subgoal premises prems for p
using prems(2, 6-)
apply -
apply (erule allE[where x = p], erule impE, rule prems)
by (fastforce simp: p_def intro: steps_P intro!: states'_updI'')
done
qed
lemma equiv_sound':
assumes step: "state_ta ⊢ ⟨L, s, u⟩ →⇘a⇙ ⟨L', s', u'⟩"
shows "A ⊢⇩n ⟨L, s, u⟩ →⇘a⇙ ⟨L', s', u'⟩ ∧ L' ∈ defs.states' s' ∧ (∀q<p. ∃pc st s'' rs pcs.
exec PF n ((I ! q) (L' ! q), [], s', True, []) [] =
Some ((pc, st, s'', True, rs), pcs))"
using step proof cases
case (step_sn_t N d I)
then show ?thesis
apply simp
apply (subst A_unfold)
apply (frule prod.A_simp(1))
apply (frule prod.A_simp(2))
apply (rule conjI)
apply (rule step_u_t)
using inv inv'' bounded by (auto simp: inv_simp p_def)
next
case (step_sn_i l g a c m f l' N p r I)
then show ?thesis
apply (simp)
apply (frule prod.A_simp(1))
apply (frule prod.A_simp(2))
apply (simp add: Prod_TA_Defs.N_s_length)
apply (subst A_unfold)
apply (drule trans_state_taD)
apply assumption
subgoal
unfolding state_trans_t_def
apply safe
apply (drule (2) P_steps_upd)
apply (drule (3) P_steps_guard)
apply safe
apply (rule step_u_i)
subgoals ‹∀p<length local.N. ∃pc. _›
apply safe
apply (rule P_steps)
apply (fastforce simp: p_def)
apply (fastforce simp: p_def)
by (metis Prod_TA_Defs'.states'_simp Prod_TA_Defs'.states_step local.step states)
apply (solves ‹auto simp: inv_simp p_def Prod_TA_Defs.N_s_length intro!: P_bounded›)+
subgoal
by (metis Prod_TA_Defs'.states'_simp Prod_TA_Defs'.states_step local.step states)
apply simp
subgoal premises prems for pc_g pc_u q
using prems(9) ‹q < _› unfolding state_ta_def state_pred_def
by (auto 4 3 simp: p_def split: option.splits)
done
done
next
case (step_sn_s l1 g1 a ci mi f1 l1' N p l2 g2 co mo f2 l2' q r1 r2 I)
then show ?thesis
apply simp
apply (frule prod.A_simp(1))
apply (frule prod.A_simp(2))
apply (simp add: Prod_TA_Defs.N_s_length)
apply (subst A_unfold)
apply (drule trans_state_taD)
apply assumption
apply (drule trans_state_taD)
apply assumption
subgoal
unfolding state_trans_t_def
apply safe
apply (drule (2) P_steps_upd)
apply (drule (2) P_steps_upd)
apply (drule (3) P_steps_guard)
apply (drule (3) P_steps_guard)
apply safe
apply (rule step_u_s)
prefers disj
apply (rule P_steps_reset; force)
subgoals ‹∀pa<length local.N. ∃pc. _›
apply safe
apply (rule P_steps)
apply (fastforce simp: p_def)
apply (fastforce simp: p_def)
by (metis Prod_TA_Defs'.states'_simp Prod_TA_Defs'.states_step local.step states)
subgoals ‹_ ∈ defs.states' s'›
by (metis Prod_TA_Defs'.states'_simp Prod_TA_Defs'.states_step local.step states)
subgoals ‹∃pc. _›
apply simp
subgoal premises prems for pc_g pc_ga pc_u pc_ua q'
using prems(14) ‹q' < _› unfolding state_ta_def state_pred_def
by (auto 4 3 simp: p_def split: option.splits)
done
apply (auto simp: inv_simp p_def Prod_TA_Defs.N_s_length intro!: P_bounded)
done
done
qed
lemma equiv_complete':
assumes step: "A ⊢⇩n ⟨L, s, u⟩ →⇘a⇙ ⟨L', s', u'⟩"
shows "state_ta ⊢ ⟨L, s, u⟩ →⇘a⇙ ⟨L', s', u'⟩ ∧ L' ∈ defs.states' s'
∧ (∀ q < p. (defs.P ! q) (L' ! q) s')"
using step proof cases
case (step_u_t N P d I)
note [simp] = A_simp[OF this(1)]
from step_u_t(2-) show ?thesis
apply safe
subgoal
by (auto simp: state_ta_def p_def state_inv_def intro: step_sn_t)
by (fastforce simp: p_def intro: steps_P intro!: states'_updI)+
next
case (step_u_i P pc_g uu uv uw ux pc_u uy uz va r N I l a l' p)
note [simp] = A_simp[OF this(1)]
from step_u_i(2-) show ?thesis
apply -
apply (simp add: Prod_TA_Defs.N_s_length)
apply (subst state_ta_unfold)
apply (frule steps_P_guard(1))
apply assumption
apply (simp; fail)
apply (drule steps_P_guard(2))
apply assumption
apply (simp; fail)
apply (frule steps_P_upd(1))
apply assumption
apply (simp; fail)
apply (drule steps_P_upd(2))
apply assumption
apply (simp; fail)
apply (drule N_transD)
apply assumption
apply safe
apply (rule step_sn_i)
apply assumption
apply (solves auto; fail)+
apply (simp add: state_ta_def p_def state_inv_def state_pred_def; fail)
apply (solves auto; fail)+
apply (simp add: Prod_TA_Defs.N_s_length; fail)
apply (solves auto; fail)+
by (fastforce simp: p_def intro: steps_P intro!: states'_updI)+
next
case (step_u_s P pc_g1 vb vc vd ve pc_g2 vf vg vh vi pc_u2 vj vk s1 vl r2 pc_u1 r1 vm vn vo vp N
I l1 a l1' p' l2 l2' q
)
note [simp] = A_simp[OF this(1)]
from ‹q < length L› have "q < p" by (simp add: Prod_TA_Defs.N_s_length)
from step_u_s(2-) show ?thesis
apply -
apply (simp add: Prod_TA_Defs.N_s_length)
apply (subst state_ta_unfold)
apply (frule steps_P_guard(1))
apply assumption
apply (simp; fail)
apply (drule steps_P_guard(2))
apply assumption
apply (simp; fail)
apply (frule steps_P_guard(1))
apply (rule ‹q < p›)
apply (simp; fail)
apply (drule steps_P_guard(2))
apply (rule ‹q < p›)
apply (simp; fail)
apply (frule steps_P_upd(1))
apply (rule ‹q < p›)
apply (simp; fail)
apply (drule steps_P_upd(2))
apply (rule ‹q < p›)
apply (simp; fail)
apply (drule steps_P_reset[simplified])
apply assumption
apply (simp; fail)
apply (frule steps_P_upd(1))
apply assumption
apply (simp; fail)
apply (drule steps_P_upd(2))
apply assumption
apply (simp; fail)
apply (drule N_transD)
apply assumption
apply (drule N_transD)
apply assumption
apply safe
apply (rule step_sn_s)
apply assumption
apply assumption
apply (all ‹(auto; fail)?›)
apply (simp add: state_ta_def p_def state_inv_def state_pred_def; fail)
apply (simp add: Prod_TA_Defs.N_s_length; fail)
apply (simp add: Prod_TA_Defs.N_s_length; fail)
subgoals ‹(defs.P ! _) (L[p' := l1', q := l2'] ! _) s'›
by (metis Equiv_TA_Defs.p_def states states'_updI'' steps_P)
subgoal
by simp (metis Equiv_TA_Defs.p_def states states'_updI'' steps_P)
apply (fastforce simp: p_def intro: steps_P intro!: states'_updI'')
done
qed
lemma equiv_complete'':
assumes step: "A ⊢⇩n ⟨L, s, u⟩ →⇘a⇙ ⟨L', s', u'⟩" "p > 0"
shows "(∀q<p. ∃pc st s'' rs pcs.
exec PF n ((I ! q) (L' ! q), [], s', True, []) [] =
Some ((pc, st, s'', True, rs), pcs))" (is ?A)
"bounded B s'" (is ?B)
proof -
from assms equiv_complete' have *: "∀q<p. (defs.P ! q) (L' ! q) s'" by simp
then show ?A unfolding state_ta_def state_pred_def by (fastforce split: option.splits)
from ‹p > 0› * have "(defs.P ! 0) (L' ! 0) s'" by auto
with ‹p > 0› show ?B unfolding state_ta_def state_pred_def by (auto split: option.splits)
qed
lemma equiv_steps_sound':
assumes step: "state_ta ⊢ ⟨L, s, u⟩ →* ⟨L', s', u'⟩"
shows "A ⊢⇩n ⟨L, s, u⟩ →* ⟨L', s', u'⟩ ∧ L' ∈ defs.states' s' ∧
(∀q<p. ∃pc st s'' rs pcs.
exec PF n ((I ! q) (L' ! q), [], s', True, []) [] =
Some ((pc, st, s'', True, rs), pcs)) ∧ bounded B s'"
using step states inv
proof (induction A ≡ state_ta L ≡ L s ≡ s u ≡ u L' s' u' arbitrary: rule: steps_sn.induct)
case (refl)
with bounded show ?case by blast
next
case prems: (step L' s' u' a L'' s'' u'')
from prems have *:
"A ⊢⇩n ⟨L, s, u⟩ →* ⟨L', s', u'⟩" "L' ∈ defs.states' s'"
"(∀q<p. ∃pc st s'' rs pcs.
exec PF n ((I ! q) (L' ! q), [], s', True, []) [] =
Some ((pc, st, s'', True, rs), pcs))"
"bounded B s'"
by auto
interpret interp: Equiv_TA A n L' s'
using pred_time_indep upd_time_indep clock_conj * by unfold_locales (auto simp: Len intro!: *)
from prems(3) have
"A ⊢⇩n ⟨L', s', u'⟩ →⇘a⇙ ⟨L'', s'', u''⟩" "L'' ∈ defs.states' s''"
"∀q<p. ∃pc st s''' rs pcs.
exec PF n ((I ! q) (L'' ! q), [], s'', True, []) [] =
Some ((pc, st, s''', True, rs), pcs)"
"bounded B s''"
by (force dest!: interp.equiv_sound')+
with * interp.states show ?case
by - (assumption | rule conjI steps_un.intros)+
qed
lemma equiv_steps_complete':
"state_ta ⊢ ⟨L, s, u⟩ →* ⟨L', s', u'⟩ ∧ L' ∈ defs.states' s' ∧
(∀q<p. ∃pc st s'' rs pcs.
exec PF n ((I ! q) (L' ! q), [], s', True, []) [] =
Some ((pc, st, s'', True, rs), pcs)) ∧ bounded B s'"
if "A ⊢⇩n ⟨L, s, u⟩ →* ⟨L', s', u'⟩" "p > 0"
using that states inv proof (induction A ≡ A n ≡ n L ≡ L s ≡ s u ≡ u _ _ _ rule: steps_un.induct)
case refl
with bounded show ?case by blast
next
case prems: (step L' s' u' a L'' s'' u'')
from prems have *:
"state_ta ⊢ ⟨L, s, u⟩ →* ⟨L', s', u'⟩" "L' ∈ defs.states' s'"
"(∀q<p. ∃pc st s'' rs pcs.
exec PF n ((I ! q) (L' ! q), [], s', True, []) [] =
Some ((pc, st, s'', True, rs), pcs))"
"bounded B s'"
by auto
interpret interp: Equiv_TA A n L' s'
using pred_time_indep upd_time_indep clock_conj by unfold_locales (auto simp: Len intro!: *)
from interp.equiv_complete'[OF prems(3)] interp.equiv_complete''[OF prems(3) ‹p > 0›] have
"state_ta ⊢ ⟨L', s', u'⟩ →⇘a⇙ ⟨L'', s'', u''⟩" "L'' ∈ defs.states' s''"
"∀q<p. ∃pc st s''' rs pcs.
exec PF n ((I ! q) (L'' ! q), [], s'', True, []) [] =
Some ((pc, st, s''', True, rs), pcs)"
"bounded B s''"
by auto
with * interp.states show ?case
by auto
qed
lemmas equiv_steps_sound = equiv_steps_sound'[THEN conjunct1]
lemmas equiv_steps_complete = equiv_steps_complete'[THEN conjunct1]
lemma equiv_correct:
"state_ta ⊢ ⟨L, s, u⟩ →* ⟨L', s', u'⟩ ⟷ A ⊢⇩n ⟨L, s, u⟩ →* ⟨L', s', u'⟩" if "p > 0"
using that equiv_steps_sound equiv_steps_complete by metis
lemma prod_correct:
"defs.prod_ta ⊢ ⟨(L, s), u⟩ →* ⟨(L', s'), u'⟩ ⟷ A ⊢⇩n ⟨L, s, u⟩ →* ⟨L', s', u'⟩" if "p > 0"
by (metis prod.prod_correct equiv_correct that)
end
end