Theory Partial_Order_Reduction.Transition_System_Interpreted_Traces
section ‹Interpreted Transition Systems and Traces›
theory Transition_System_Interpreted_Traces
imports
Transition_System_Traces
"Basics/Stuttering"
begin
locale transition_system_interpreted_traces =
transition_system_interpreted ex en int +
transition_system_traces ex en ind
for ex :: "'action ⇒ 'state ⇒ 'state"
and en :: "'action ⇒ 'state ⇒ bool"
and int :: "'state ⇒ 'interpretation"
and ind :: "'action ⇒ 'action ⇒ bool"
+
assumes independence_invisible: "a ∈ visible ⟹ b ∈ visible ⟹ ¬ ind a b"
begin
lemma eq_swap_lproject_visible:
assumes "u =⇩S v"
shows "lproject visible (llist_of u) = lproject visible (llist_of v)"
using assms independence_invisible by (induct, auto)
lemma eq_fin_lproject_visible:
assumes "u =⇩F v"
shows "lproject visible (llist_of u) = lproject visible (llist_of v)"
using assms eq_swap_lproject_visible by (induct, auto)
lemma le_fin_lproject_visible:
assumes "u ≼⇩F v"
shows "lproject visible (llist_of u) ≤ lproject visible (llist_of v)"
proof -
obtain w where 1: "u @ w =⇩F v" using assms by rule
have "lproject visible (llist_of u) ≤
lproject visible (llist_of u) $ lproject visible (llist_of w)" by auto
also have "… = lproject visible (llist_of (u @ w))" using lappend_llist_of_llist_of by auto
also have "… = lproject visible (llist_of v)" using eq_fin_lproject_visible 1 by this
finally show ?thesis by this
qed
lemma le_fininf_lproject_visible:
assumes "u ≼⇩F⇩I v"
shows "lproject visible (llist_of u) ≤ lproject visible (llist_of_stream v)"
proof -
obtain w where 1: "w ≤⇩F⇩I v" "u ≼⇩F w" using assms by rule
have "lproject visible (llist_of u) ≤ lproject visible (llist_of w)"
using le_fin_lproject_visible 1(2) by this
also have "… ≤ lproject visible (llist_of_stream v)" using 1(1) by blast
finally show ?thesis by this
qed
lemma le_inf_lproject_visible:
assumes "u ≼⇩I v"
shows "lproject visible (llist_of_stream u) ≤ lproject visible (llist_of_stream v)"
proof (rule lproject_prefix_limit)
fix w
assume 1: "w ≤ llist_of_stream u" "lfinite w"
have 2: "list_of w ≤⇩F⇩I stream_of_llist (llist_of_stream u)" using 1 by blast
have 3: "list_of w ≼⇩F⇩I v" using assms 2 by auto
have "lproject visible w = lproject visible (llist_of (list_of w))" using 1(2) by simp
also have "… ≤ lproject visible (llist_of_stream v)" using le_fininf_lproject_visible 3 by this
finally show "lproject visible w ≤ lproject visible (llist_of_stream v)" by this
qed
lemma eq_inf_lproject_visible:
assumes "u =⇩I v"
shows "lproject visible (llist_of_stream u) = lproject visible (llist_of_stream v)"
using le_inf_lproject_visible assms by (metis antisym eq_infE)
lemma stutter_selection_lproject_visible:
assumes "run u p"
shows "stutter_selection (lift (liset visible (llist_of_stream u)))
(llist_of_stream (smap int (p ## trace u p)))"
proof
show "0 ∈ lift (liset visible (llist_of_stream u))" by auto
next
fix k i
assume 3: "enat (Suc k) < esize (lift (liset visible (llist_of_stream u)))"
assume 4: "nth_least (lift (liset visible (llist_of_stream u))) k < i"
assume 5: "i < nth_least (lift (liset visible (llist_of_stream u))) (Suc k)"
have 6: "int ((p ## trace u p) !! nth_least (lift (liset visible (llist_of_stream u))) k) =
int ((p ## trace u p) !! i)"
proof (rule execute_inf_word_invisible)
show "run u p" using assms by this
show "nth_least (lift (liset visible (llist_of_stream u))) k ≤ i" using 4 by auto
next
fix j
assume 6: "nth_least (lift (liset visible (llist_of_stream u))) k ≤ j"
assume 7: "j < i"
have 8: "Suc j ∉ lift (liset visible (llist_of_stream u))"
proof (rule nth_least_not_contains)
show "enat (Suc k) < esize (lift (liset visible (llist_of_stream u)))" using 3 by this
show "nth_least (lift (liset visible (llist_of_stream u))) k < Suc j" using 6 by auto
show "Suc j < nth_least (lift (liset visible (llist_of_stream u))) (Suc k)" using 5 7 by simp
qed
have 9: "j ∉ liset visible (llist_of_stream u)" using 8 by auto
show "u !! j ∉ visible" using 9 by auto
qed
show "llist_of_stream (smap int (p ## trace u p)) ?! i = llist_of_stream (smap int (p ## trace u p)) ?!
nth_least (lift (liset visible (llist_of_stream u))) k"
using 6 by (metis lnth_list_of_stream snth_smap)
next
fix i
assume 1: "finite (lift (liset visible (llist_of_stream u)))"
assume 3: "Max (lift (liset visible (llist_of_stream u))) < i"
have 4: "int ((p ## trace u p) !! Max (lift (liset visible (llist_of_stream u)))) =
int ((p ## trace u p) !! i)"
proof (rule execute_inf_word_invisible)
show "run u p" using assms by this
show "Max (lift (liset visible (llist_of_stream u))) ≤ i" using 3 by auto
next
fix j
assume 6: "Max (lift (liset visible (llist_of_stream u))) ≤ j"
assume 7: "j < i"
have 8: "Suc j ∉ lift (liset visible (llist_of_stream u))"
proof (rule ccontr)
assume 9: "¬ Suc j ∉ lift (liset visible (llist_of_stream u))"
have 10: "Suc j ∈ lift (liset visible (llist_of_stream u))" using 9 by simp
have 11: "Suc j ≤ Max (lift (liset visible (llist_of_stream u)))" using Max_ge 1 10 by this
show "False" using 6 11 by auto
qed
have 9: "j ∉ liset visible (llist_of_stream u)" using 8 by auto
show "u !! j ∉ visible" using 9 by auto
qed
show "llist_of_stream (smap int (p ## trace u p)) ?! i = llist_of_stream (smap int (p ## trace u p)) ?!
Max (lift (liset visible (llist_of_stream u)))" using 4 by (metis lnth_list_of_stream snth_smap)
qed
lemma execute_fin_visible:
assumes "path u q" "path v q" "u ≼⇩F⇩I w" "v ≼⇩F⇩I w"
assumes "project visible u = project visible v"
shows "int (target u q) = int (target v q)"
proof -
obtain w' where 1: "u ≼⇩F w'" "v ≼⇩F w'" using subsume_fin assms(3, 4) by this
obtain u' v' where 2: "u @ u' =⇩F w'" "v @ v' =⇩F w'" using 1 by blast
have "u @ u' =⇩F w'" using 2(1) by this
also have "… =⇩F v @ v'" using 2(2) by blast
finally have 3: "u @ u' =⇩F v @ v'" by this
obtain s⇩1 s⇩2 s⇩3 where 4: "u =⇩F s⇩1 @ s⇩2" "v =⇩F s⇩1 @ s⇩3" "Ind (set s⇩2) (set s⇩3)"
using levi_lemma 3 by this
have 5: "project visible (s⇩1 @ s⇩2) = project visible (s⇩1 @ s⇩3)"
using eq_fin_lproject_visible assms(5) 4(1, 2) by auto
have 6: "project visible s⇩2 = project visible s⇩3" using 5 by simp
have 7: "set (project visible s⇩2) = set (project visible s⇩3)" using 6 by simp
have 8: "set s⇩2 ∩ visible = set s⇩3 ∩ visible" using 7 by auto
have 9: "set s⇩2 ⊆ invisible ∨ set s⇩3 ⊆ invisible" using independence_invisible 4(3) by auto
have 10: "set s⇩2 ⊆ invisible" "set s⇩3 ⊆ invisible" using 8 9 by auto
have 11: "path s⇩2 (target s⇩1 q)" using eq_fin_word 4(1) assms(1) by auto
have 12: "path s⇩3 (target s⇩1 q)" using eq_fin_word 4(2) assms(2) by auto
have "int (fold ex u q) = int (fold ex (s⇩1 @ s⇩2) q)" using eq_fin_execute assms(1) 4(1) by simp
also have "… = int (fold ex s⇩1 q)" using execute_fin_word_invisible 11 10(1) by simp
also have "… = int (fold ex (s⇩1 @ s⇩3) q)" using execute_fin_word_invisible 12 10(2) by simp
also have "… = int (fold ex v q)" using eq_fin_execute assms(2) 4(2) by simp
finally show ?thesis by this
qed
lemma execute_inf_visible:
assumes "run u q" "run v q" "u ≼⇩I w" "v ≼⇩I w"
assumes "lproject visible (llist_of_stream u) = lproject visible (llist_of_stream v)"
shows "snth (smap int (q ## trace u q)) ≈ snth (smap int (q ## trace v q))"
proof -
have 1: "lnth (llist_of_stream (smap int (q ## trace u q))) ≈
lnth (llist_of_stream (smap int (q ## trace v q)))"
proof
show "linfinite (llist_of_stream (smap int (q ## trace u q)))" by simp
show "linfinite (llist_of_stream (smap int (q ## trace v q)))" by simp
show "stutter_selection (lift (liset visible (llist_of_stream u))) (llist_of_stream (smap int (q ## trace u q)))"
using stutter_selection_lproject_visible assms(1) by this
show "stutter_selection (lift (liset visible (llist_of_stream v))) (llist_of_stream (smap int (q ## trace v q)))"
using stutter_selection_lproject_visible assms(2) by this
show "lselect (lift (liset visible (llist_of_stream u))) (llist_of_stream (smap int (q ## trace u q))) =
lselect (lift (liset visible (llist_of_stream v))) (llist_of_stream (smap int (q ## trace v q)))"
proof
have "llength (lselect (lift (liset visible (llist_of_stream u)))
(llist_of_stream (smap int (q ## trace u q)))) = eSuc (llength (lproject visible (llist_of_stream u)))"
by (simp add: lselect_llength)
also have "… = eSuc (llength (lproject visible (llist_of_stream v)))"
unfolding assms(5) by rule
also have "… = llength (lselect (lift (liset visible (llist_of_stream v)))
(llist_of_stream (smap int (q ## trace v q))))" by (simp add: lselect_llength)
finally show "llength (lselect (lift (liset visible (llist_of_stream u)))
(llist_of_stream (smap int (q ## trace u q)))) = llength (lselect (lift (liset visible (llist_of_stream v)))
(llist_of_stream (smap int (q ## trace v q))))" by this
next
fix i
assume 1:
"enat i < llength (lselect (lift (liset visible (llist_of_stream u)))
(llist_of_stream (smap int (q ## trace u q))))"
"enat i < llength (lselect (lift (liset visible (llist_of_stream v)))
(llist_of_stream (smap int (q ## trace v q))))"
have 2:
"enat i ≤ llength (lproject visible (llist_of_stream u))"
"enat i ≤ llength (lproject visible (llist_of_stream v))"
using 1 by (simp add: lselect_llength)+
define k where "k ≡ nth_least (lift (liset visible (llist_of_stream u))) i"
define l where "l ≡ nth_least (lift (liset visible (llist_of_stream v))) i"
have "lselect (lift (liset visible (llist_of_stream u))) (llist_of_stream (smap int (q ## trace u q))) ?! i =
int ((q ## trace u q) !! nth_least (lift (liset visible (llist_of_stream u))) i)"
by (metis 1(1) lnth_list_of_stream lselect_lnth snth_smap)
also have "… = int ((q ## trace u q) !! k)" unfolding k_def by rule
also have "… = int ((q ## trace v q) !! l)"
unfolding sscan_scons_snth
proof (rule execute_fin_visible)
show "path (stake k u) q" using assms(1) by (metis run_shift_elim stake_sdrop)
show "path (stake l v) q" using assms(2) by (metis run_shift_elim stake_sdrop)
show "stake k u ≼⇩F⇩I w" "stake l v ≼⇩F⇩I w" using assms(3, 4) by auto
have "project visible (stake k u) =
list_of (lproject visible (llist_of (stake k u)))" by simp
also have "… = list_of (lproject visible (ltake (enat k) (llist_of_stream u)))"
by (metis length_stake llength_llist_of llist_of_inf_llist_prefix lprefix_ltake prefix_fininf_prefix)
also have "… = list_of (ltake (enat i) (lproject visible (llist_of_stream u)))"
unfolding k_def lproject_ltake[OF 2(1)] by rule
also have "… = list_of (ltake (enat i) (lproject visible (llist_of_stream v)))"
unfolding assms(5) by rule
also have "… = list_of (lproject visible (ltake (enat l) (llist_of_stream v)))"
unfolding l_def lproject_ltake[OF 2(2)] by rule
also have "… = project visible (stake l v)"
by (metis length_stake lfilter_llist_of list_of_llist_of llength_llist_of
llist_of_inf_llist_prefix lprefix_ltake prefix_fininf_prefix)
finally show "project visible (stake k u) = project visible (stake l v)" by this
qed
also have "… = int ((q ## trace v q) !! nth_least (lift (liset visible (llist_of_stream v))) i)"
unfolding l_def by simp
also have "… = lselect (lift (liset visible (llist_of_stream v)))
(llist_of_stream (smap int (q ## trace v q))) ?! i"
using 1 by (metis lnth_list_of_stream lselect_lnth snth_smap)
finally show "lselect (lift (liset visible (llist_of_stream u)))
(llist_of_stream (smap int (q ## trace u q))) ?! i = lselect (lift (liset visible (llist_of_stream v)))
(llist_of_stream (smap int (q ## trace v q))) ?! i" by this
qed
qed
show ?thesis using 1 by simp
qed
end
end