Theory Ample_Abstract
section ‹Abstract Theory of Ample Set Partial Order Reduction›
theory Ample_Abstract
imports
Transition_System_Interpreted_Traces
"Extensions/Relation_Extensions"
begin
locale ample_base =
transition_system_interpreted_traces ex en int ind +
wellfounded_relation src
for ex :: "'action ⇒ 'state ⇒ 'state"
and en :: "'action ⇒ 'state ⇒ bool"
and int :: "'state ⇒ 'interpretation"
and ind :: "'action ⇒ 'action ⇒ bool"
and src :: "'state ⇒ 'state ⇒ bool"
begin
definition ample_set :: "'state ⇒ 'action set ⇒ bool"
where "ample_set q A ≡
A ⊆ {a. en a q} ∧
(A ⊂ {a. en a q} ⟶ A ≠ {}) ∧
(∀ a. A ⊂ {a. en a q} ⟶ a ∈ A ⟶ src (ex a q) q) ∧
(A ⊂ {a. en a q} ⟶ A ⊆ invisible) ∧
(∀ w. A ⊂ {a. en a q} ⟶ path w q ⟶ A ∩ set w = {} ⟶ Ind A (set w))"
lemma ample_subset:
assumes "ample_set q A"
shows "A ⊆ {a. en a q}"
using assms unfolding ample_set_def by auto
lemma ample_nonempty:
assumes "ample_set q A" "A ⊂ {a. en a q}"
shows "A ≠ {}"
using assms unfolding ample_set_def by auto
lemma ample_wellfounded:
assumes "ample_set q A" "A ⊂ {a. en a q}" "a ∈ A"
shows "src (ex a q) q"
using assms unfolding ample_set_def by auto
lemma ample_invisible:
assumes "ample_set q A" "A ⊂ {a. en a q}"
shows "A ⊆ invisible"
using assms unfolding ample_set_def by auto
lemma ample_independent:
assumes "ample_set q A" "A ⊂ {a. en a q}" "path w q" "A ∩ set w = {}"
shows "Ind A (set w)"
using assms unfolding ample_set_def by auto
lemma ample_en[intro]: "ample_set q {a. en a q}" unfolding ample_set_def by blast
end
locale ample_abstract =
S?: transition_system_complete ex en init int +
R: transition_system_complete ex ren init int +
ample_base ex en int ind src
for ex :: "'action ⇒ 'state ⇒ 'state"
and en :: "'action ⇒ 'state ⇒ bool"
and init :: "'state ⇒ bool"
and int :: "'state ⇒ 'interpretation"
and ind :: "'action ⇒ 'action ⇒ bool"
and src :: "'state ⇒ 'state ⇒ bool"
and ren :: "'action ⇒ 'state ⇒ bool"
+
assumes reduction_ample: "q ∈ nodes ⟹ ample_set q {a. ren a q}"
begin
lemma reduction_words_fin:
assumes "q ∈ nodes" "R.path w q"
shows "S.path w q"
using assms(2, 1) ample_subset reduction_ample by induct auto
lemma reduction_words_inf:
assumes "q ∈ nodes" "R.run w q"
shows "S.run w q"
using reduction_words_fin assms by (auto intro: words_infI_construct)
lemma reduction_step:
assumes "q ∈ nodes" "run w q"
obtains
(deferred) a where "ren a q" "[a] ≼⇩F⇩I w" |
(omitted) "{a. ren a q} ⊆ invisible" "Ind {a. ren a q} (sset w)"
proof (cases "{a. en a q} = {a. ren a q}")
case True
have 1: "run (shd w ## sdrop 1 w) q" using assms(2) by simp
show ?thesis
proof (rule deferred)
show "ren (shd w) q" using True 1 by blast
show "[shd w] ≼⇩F⇩I w" by simp
qed
next
case False
have 1: "{a. ren a q} ⊂ {a. en a q}" using ample_subset reduction_ample assms(1) False by auto
show ?thesis
proof (cases "{a. ren a q} ∩ sset w = {}")
case True
show ?thesis
proof (rule omitted)
show "{a. ren a q} ⊆ invisible" using ample_invisible reduction_ample assms(1) 1 by auto
show "Ind {a. ren a q} (sset w)"
proof safe
fix a b
assume 2: "b ∈ sset w" "ren a q"
obtain u v where 3: "w = u @- b ## v" using split_stream_first' 2(1) by this
have 4: "Ind {a. ren a q} (set (u @ [b]))"
proof (rule ample_independent)
show "ample_set q {a. ren a q}" using reduction_ample assms(1) by this
show "{a. ren a q} ⊂ {a. en a q}" using 1 by this
show "path (u @ [b]) q" using assms(2) 3 by blast
show "{a. ren a q} ∩ set (u @ [b]) = {}" using True 3 by auto
qed
show "ind a b" using 2 3 4 by auto
qed
qed
next
case False
obtain u a v where 2: "w = u @- a ## v" "{a. ren a q} ∩ set u = {}" "ren a q"
using split_stream_first[OF False] by auto
have 3: "path u q" using assms(2) unfolding 2(1) by auto
have 4: "Ind {a. ren a q} (set u)"
using ample_independent reduction_ample assms(1) 1 3 2(2) by this
have 5: "Ind (set [a]) (set u)" using 4 2(3) by simp
have 6: "[a] @ u =⇩F u @ [a]" using 5 by blast
show ?thesis
proof (rule deferred)
show "ren a q" using 2(3) by this
have "[a] ≼⇩F⇩I [a] @- u @- v" by blast
also have "[a] @- u @- v = ([a] @ u) @- v" by simp
also have "([a] @ u) @- v =⇩I (u @ [a]) @- v" using 6 by blast
also have "(u @ [a]) @- v = u @- [a] @- v" by simp
also have "… = w" unfolding 2(1) by simp
finally show "[a] ≼⇩F⇩I w" by this
qed
qed
qed
lemma reduction_chunk:
assumes "q ∈ nodes" "run ([a] @- v) q"
obtains b b⇩1 b⇩2 u
where
"R.path (b @ [a]) q"
"Ind {a} (set b)" "set b ⊆ invisible"
"b =⇩F b⇩1 @ b⇩2" "b⇩1 @- u =⇩I v" "Ind (set b⇩2) (sset u)"
using wellfounded assms
proof (induct q arbitrary: thesis v rule: wfP_induct_rule)
case (less q)
show ?case
proof (cases "ren a q")
case (True)
show ?thesis
proof (rule less(2))
show "R.path ([] @ [a]) q" using True by auto
show "Ind {a} (set [])" by auto
show "set [] ⊆ invisible" by auto
show "[] =⇩F [] @ []" by auto
show "[] @- v =⇩I v" by auto
show "Ind (set []) (sset v)" by auto
qed
next
case (False)
have 0: "{a. en a q} ≠ {a. ren a q}" using False less(4) by auto
show ?thesis
using less(3, 4)
proof (cases rule: reduction_step)
case (deferred c)
have 1: "ren c q" using deferred(1) by simp
have 2: "ind a c"
proof (rule le_fininf_ind'')
show "[a] ≼⇩F⇩I [a] @- v" by blast
show "[c] ≼⇩F⇩I [a] @- v" using deferred(2) by this
show "a ≠ c" using False 1 by auto
qed
obtain v' where 3: "[a] @- v =⇩I [c] @- [a] @- v'"
proof -
have 10: "[c] ≼⇩F⇩I v"
proof (rule le_fininf_not_member')
show "[c] ≼⇩F⇩I [a] @- v" using deferred(2) by this
show "c ∉ set [a]" using False 1 by auto
qed
obtain v' where 11: "v =⇩I [c] @- v'" using 10 by blast
have 12: "Ind (set [a]) (set [c])" using 2 by auto
have 13: "[a] @ [c] =⇩F [c] @ [a]" using 12 by blast
have "[a] @- v =⇩I [a] @- [c] @- v'" using 11 by blast
also have "… = ([a] @ [c]) @- v'" by simp
also have "… =⇩I ([c] @ [a]) @- v'" using 13 by blast
also have "… = [c] @- [a] @- v'" by simp
finally show ?thesis using that by auto
qed
have 4: "run ([c] @- [a] @- v') q" using eq_inf_word 3 less(4) by this
show ?thesis
proof (rule less(1))
show "src (ex c q) q"
using ample_wellfounded ample_subset reduction_ample less(3) 0 1 by blast
have 100: "en c q" using less(4) deferred(2) le_fininf_word by auto
show "ex c q ∈ nodes" using less(3) 100 by auto
show "run ([a] @- v') (ex c q)" using 4 by auto
next
fix b b⇩1 b⇩2 u
assume 5: "R.path (b @ [a]) (ex c q)"
assume 6: "Ind {a} (set b)"
assume 7: "set b ⊆ invisible"
assume 8: "b =⇩F b⇩1 @ b⇩2"
assume 9: "b⇩1 @- u =⇩I v'"
assume 10: "Ind (set b⇩2) (sset u)"
show "thesis"
proof (rule less(2))
show "R.path (([c] @ b) @ [a]) q" using 1 5 by auto
show "Ind {a} (set ([c] @ b))" using 6 2 by auto
have 11: "c ∈ invisible"
using ample_invisible ample_subset reduction_ample less(3) 0 1 by blast
show "set ([c] @ b) ⊆ invisible" using 7 11 by auto
have "[c] @ b =⇩F [c] @ b⇩1 @ b⇩2" using 8 by blast
also have "[c] @ b⇩1 @ b⇩2 = ([c] @ b⇩1) @ b⇩2" by simp
finally show "[c] @ b =⇩F ([c] @ b⇩1) @ b⇩2" by this
show "([c] @ b⇩1) @- u =⇩I v"
proof -
have 10: "Ind (set [a]) (set [c])" using 2 by auto
have 11: "[a] @ [c] =⇩F [c] @ [a]" using 10 by blast
have "[a] @- v =⇩I [c] @- [a] @- v'" using 3 by this
also have "… = ([c] @ [a]) @- v'" by simp
also have "… =⇩I ([a] @ [c]) @- v'" using 11 by blast
also have "… = [a] @- [c] @- v'" by simp
finally have 12: "[a] @- v =⇩I [a] @- [c] @- v'" by this
have 12: "v =⇩I [c] @- v'" using 12 by blast
have "([c] @ b⇩1) @- u = [c] @- b⇩1 @- u" by simp
also have "… =⇩I [c] @- v'" using 9 by blast
also have "… =⇩I v" using 12 by blast
finally show ?thesis by this
qed
show "Ind (set b⇩2) (sset u)" using 10 by this
qed
qed
next
case (omitted)
have 1: "{a. ren a q} ⊆ invisible" using omitted(1) by simp
have 2: "Ind {a. ren a q} (sset ([a] @- v))" using omitted(2) by simp
obtain c where 3: "ren c q"
proof -
have 1: "en a q" using less(4) by auto
show ?thesis using reduction_ample ample_nonempty less(3) 1 that by blast
qed
have 4: "Ind (set [c]) (sset ([a] @- v))" using 2 3 by auto
have 6: "path [c] q" using reduction_ample ample_subset less(3) 3 by auto
have 7: "run ([a] @- v) (target [c] q)" using diamond_fin_word_inf_word 4 6 less(4) by this
show ?thesis
proof (rule less(1))
show "src (ex c q) q"
using reduction_ample ample_wellfounded ample_subset less(3) 0 3 by blast
show "ex c q ∈ nodes" using less(3) 6 by auto
show "run ([a] @- v) (ex c q)" using 7 by auto
next
fix b s b⇩1 b⇩2 u
assume 5: "R.path (b @ [a]) (ex c q)"
assume 6: "Ind {a} (set b)"
assume 7: "set b ⊆ invisible"
assume 8: "b =⇩F b⇩1 @ b⇩2"
assume 9: "b⇩1 @- u =⇩I v"
assume 10: "Ind (set b⇩2) (sset u)"
show "thesis"
proof (rule less(2))
show "R.path (([c] @ b) @ [a]) q" using 3 5 by auto
show "Ind {a} (set ([c] @ b))"
proof -
have 1: "ind c a" using 4 by simp
have 2: "ind a c" using independence_symmetric 1 by this
show ?thesis using 6 2 by auto
qed
have 11: "c ∈ invisible" using 1 3 by auto
show "set ([c] @ b) ⊆ invisible" using 7 11 by auto
have 12: "Ind (set [c]) (set b⇩1)"
proof -
have 1: "set b⇩1 ⊆ sset v" using 9 by force
have 2: "Ind (set [c]) (sset v)" using 4 by simp
show ?thesis using 1 2 by auto
qed
have "[c] @ b =⇩F [c] @ b⇩1 @ b⇩2" using 8 by blast
also have "… = ([c] @ b⇩1) @ b⇩2" by simp
also have "… =⇩F (b⇩1 @ [c]) @ b⇩2" using 12 by blast
also have "… = b⇩1 @ [c] @ b⇩2" by simp
finally show "[c] @ b =⇩F b⇩1 @ [c] @ b⇩2" by this
show "b⇩1 @- u =⇩I v" using 9 by this
have 13: "Ind (set [c]) (sset u)"
proof -
have 1: "sset u ⊆ sset v" using 9 by force
have 2: "Ind (set [c]) (sset v)" using 4 by simp
show ?thesis using 1 2 by blast
qed
show "Ind (set ([c] @ b⇩2)) (sset u)" using 10 13 by auto
qed
qed
qed
qed
qed
inductive reduced_run :: "'state ⇒ 'action list ⇒ 'action stream ⇒ 'action list ⇒
'action list ⇒ 'action list ⇒ 'action list ⇒ 'action stream ⇒ bool"
where
init: "reduced_run q [] v [] [] [] [] v" |
absorb: "reduced_run q v⇩1 ([a] @- v⇩2) l w w⇩1 w⇩2 u ⟹ a ∈ set l ⟹
reduced_run q (v⇩1 @ [a]) v⇩2 (remove1 a l) w w⇩1 w⇩2 u" |
extend: "reduced_run q v⇩1 ([a] @- v⇩2) l w w⇩1 w⇩2 u ⟹ a ∉ set l ⟹
R.path (b @ [a]) (target w q) ⟹
Ind {a} (set b) ⟹ set b ⊆ invisible ⟹
b =⇩F b⇩1 @ b⇩2 ⟹ [a] @- b⇩1 @- u' =⇩I u ⟹ Ind (set b⇩2) (sset u') ⟹
reduced_run q (v⇩1 @ [a]) v⇩2 (l @ b⇩1) (w @ b @ [a]) (w⇩1 @ b⇩1 @ [a]) (w⇩2 @ b⇩2) u'"
lemma reduced_run_words_fin:
assumes "reduced_run q v⇩1 v⇩2 l w w⇩1 w⇩2 u"
shows "R.path w q"
using assms by induct auto
lemma reduced_run_invar_2:
assumes "reduced_run q v⇩1 v⇩2 l w w⇩1 w⇩2 u"
shows "v⇩2 =⇩I l @- u"
using assms
proof induct
case (init q v)
show ?case by simp
next
case (absorb q v⇩1 a v⇩2 l w w⇩1 w⇩2 u)
obtain l⇩1 l⇩2 where 10: "l = l⇩1 @ [a] @ l⇩2" "a ∉ set l⇩1"
using split_list_first[OF absorb(3)] by auto
have 11: "Ind {a} (set l⇩1)"
proof (rule le_fininf_ind')
show "[a] ≼⇩F⇩I l @- u" using absorb(2) by auto
show "l⇩1 ≼⇩F⇩I l @- u" unfolding 10(1) by auto
show "a ∉ set l⇩1" using 10(2) by this
qed
have 12: "Ind (set [a]) (set l⇩1)" using 11 by auto
have "[a] @ remove1 a l = [a] @ l⇩1 @ l⇩2" unfolding 10(1) remove1_append using 10(2) by auto
also have "… =⇩F ([a] @ l⇩1) @ l⇩2" by simp
also have "… =⇩F (l⇩1 @ [a]) @ l⇩2" using 12 by blast
also have "… = l" unfolding 10(1) by simp
finally have 13: "[a] @ remove1 a l =⇩F l" by this
have "[a] @- remove1 a l @- u = ([a] @ remove1 a l) @- u" unfolding conc_conc by simp
also have "… =⇩I l @- u" using 13 by blast
also have "… =⇩I [a] @- v⇩2" using absorb(2) by auto
finally show ?case by blast
next
case (extend q v⇩1 a v⇩2 l w w⇩1 w⇩2 u b b⇩1 b⇩2 u')
have 11: "Ind {a} (set l)"
proof (rule le_fininf_ind')
show "[a] ≼⇩F⇩I l @- u" using extend(2) by auto
show "l ≼⇩F⇩I l @- u" by auto
show "a ∉ set l" using extend(3) by this
qed
have 11: "Ind (set [a]) (set l)" using 11 by auto
have 12: "eq_fin ([a] @ l) (l @ [a])" using 11 by blast
have 131: "set b⇩1 ⊆ set b" using extend(7) by auto
have 132: "Ind (set [a]) (set b)" using extend(5) by auto
have 13: "Ind (set [a]) (set b⇩1)" using 131 132 by auto
have 14: "eq_fin ([a] @ b⇩1) (b⇩1 @ [a])" using 13 by blast
have "[a] @- ((l @ b⇩1) @- u') = ([a] @ l) @- b⇩1 @- u'" by simp
also have "eq_inf … ((l @ [a]) @- b⇩1 @- u')" using 12 by blast
also have "… = l @- [a] @- b⇩1 @- u'" by simp
also have "eq_inf … (l @- u)" using extend(8) by blast
also have "eq_inf … ([a] @- v⇩2)" using extend(2) by auto
finally show ?case by blast
qed
lemma reduced_run_invar_1:
assumes "reduced_run q v⇩1 v⇩2 l w w⇩1 w⇩2 u"
shows "v⇩1 @ l =⇩F w⇩1"
using assms
proof induct
case (init q v)
show ?case by simp
next
case (absorb q v⇩1 a v⇩2 l w w⇩1 w⇩2 u)
have 1: "[a] @- v⇩2 =⇩I l @- u" using reduced_run_invar_2 absorb(1) by this
obtain l⇩1 l⇩2 where 10: "l = l⇩1 @ [a] @ l⇩2" "a ∉ set l⇩1"
using split_list_first[OF absorb(3)] by auto
have 11: "Ind {a} (set l⇩1)"
proof (rule le_fininf_ind')
show "[a] ≼⇩F⇩I l @- u" using 1 by auto
show "l⇩1 ≼⇩F⇩I l @- u" unfolding 10(1) by auto
show "a ∉ set l⇩1" using 10(2) by this
qed
have 12: "Ind (set [a]) (set l⇩1)" using 11 by auto
have "[a] @ remove1 a l = [a] @ l⇩1 @ l⇩2" unfolding 10(1) remove1_append using 10(2) by auto
also have "… =⇩F ([a] @ l⇩1) @ l⇩2" by simp
also have "… =⇩F (l⇩1 @ [a]) @ l⇩2" using 12 by blast
also have "… = l" unfolding 10(1) by simp
finally have 13: "[a] @ remove1 a l =⇩F l" by this
have "w⇩1 =⇩F v⇩1 @ l" using absorb(2) by auto
also have "… =⇩F v⇩1 @ ([a] @ remove1 a l)" using 13 by blast
also have "… = (v⇩1 @ [a]) @ remove1 a l" by simp
finally show ?case by auto
next
case (extend q v⇩1 a v⇩2 l w w⇩1 w⇩2 u b b⇩1 b⇩2 u')
have 1: "[a] @- v⇩2 =⇩I l @- u" using reduced_run_invar_2 extend(1) by this
have 11: "Ind {a} (set l)"
proof (rule le_fininf_ind')
show "[a] ≼⇩F⇩I l @- u" using 1 by auto
show "l ≼⇩F⇩I l @- u" by auto
show "a ∉ set l" using extend(3) by auto
qed
have 11: "Ind (set [a]) (set l)" using 11 by auto
have 12: "eq_fin ([a] @ l) (l @ [a])" using 11 by blast
have 131: "set b⇩1 ⊆ set b" using extend(7) by auto
have 132: "Ind (set [a]) (set b)" using extend(5) by auto
have 13: "Ind (set [a]) (set b⇩1)" using 131 132 by auto
have 14: "eq_fin ([a] @ b⇩1) (b⇩1 @ [a])" using 13 by blast
have "eq_fin (w⇩1 @ b⇩1 @ [a]) (w⇩1 @ [a] @ b⇩1)" using 14 by blast
also have "eq_fin … ((v⇩1 @ l) @ [a] @ b⇩1)" using extend(2) by blast
also have "eq_fin … (v⇩1 @ (l @ [a]) @ b⇩1)" by simp
also have "eq_fin … (v⇩1 @ ([a] @ l) @ b⇩1)" using 12 by blast
also have "… = (v⇩1 @ [a]) @ l @ b⇩1" by simp
finally show ?case by auto
qed
lemma reduced_run_invisible:
assumes "reduced_run q v⇩1 v⇩2 l w w⇩1 w⇩2 u"
shows "set w⇩2 ⊆ invisible"
using assms
proof induct
case (init q v)
show ?case by simp
next
case (absorb q v⇩1 a v⇩2 l w w⇩1 w⇩2 u)
show ?case using absorb(2) by this
next
case (extend q v⇩1 a v⇩2 l w w⇩1 w⇩2 u b b⇩1 b⇩2 u')
have 1: "set b⇩2 ⊆ set b" using extend(7) by auto
show ?case unfolding set_append using extend(2) extend(6) 1 by blast
qed
lemma reduced_run_ind:
assumes "reduced_run q v⇩1 v⇩2 l w w⇩1 w⇩2 u"
shows "Ind (set w⇩2) (sset u)"
using assms
proof induct
case (init q v)
show ?case by simp
next
case (absorb q v⇩1 a v⇩2 l w w⇩1 w⇩2 u)
show ?case using absorb(2) by this
next
case (extend q v⇩1 a v⇩2 l w w⇩1 w⇩2 u b b⇩1 b⇩2 u')
have 1: "sset u' ⊆ sset u" using extend(8) by force
show ?case using extend(2) extend(9) 1 unfolding set_append by blast
qed
lemma reduced_run_decompose:
assumes "reduced_run q v⇩1 v⇩2 l w w⇩1 w⇩2 u"
shows "w =⇩F w⇩1 @ w⇩2"
using assms
proof induct
case (init q v)
show ?case by simp
next
case (absorb q v⇩1 a v⇩2 l w w⇩1 w⇩2 u)
show ?case using absorb(2) by this
next
case (extend q v⇩1 a v⇩2 l w w⇩1 w⇩2 u b b⇩1 b⇩2 u')
have 1: "Ind (set [a]) (set b⇩2)" using extend(5) extend(7) by auto
have 2: "Ind (set w⇩2) (set (b⇩1 @ [a]))"
proof -
have 1: "Ind (set w⇩2) (sset u)" using reduced_run_ind extend(1) by this
have 2: "u =⇩I [a] @- b⇩1 @- u'" using extend(8) by auto
have 3: "sset u = sset ([a] @- b⇩1 @- u')" using 2 by blast
show ?thesis unfolding set_append using 1 3 by simp
qed
have "w @ b @ [a] =⇩F (w⇩1 @ w⇩2) @ b @ [a]" using extend(2) by blast
also have "… =⇩F (w⇩1 @ w⇩2) @ (b⇩1 @ b⇩2) @ [a]" using extend(7) by blast
also have "… = w⇩1 @ w⇩2 @ b⇩1 @ (b⇩2 @ [a])" by simp
also have "… =⇩F w⇩1 @ w⇩2 @ b⇩1 @ ([a] @ b⇩2)" using 1 by blast
also have "… =⇩F w⇩1 @ (w⇩2 @ (b⇩1 @ [a])) @ b⇩2" by simp
also have "… =⇩F w⇩1 @ ((b⇩1 @ [a]) @ w⇩2) @ b⇩2" using 2 by blast
also have "… =⇩F (w⇩1 @ b⇩1 @ [a]) @ w⇩2 @ b⇩2" by simp
finally show ?case by this
qed
lemma reduced_run_project:
assumes "reduced_run q v⇩1 v⇩2 l w w⇩1 w⇩2 u"
shows "project visible w⇩1 = project visible w"
proof -
have 1: "w⇩1 @ w⇩2 =⇩F w" using reduced_run_decompose assms by auto
have 2: "set w⇩2 ⊆ invisible" using reduced_run_invisible assms by this
have 3: "project visible w⇩2 = []" unfolding filter_empty_conv using 2 by auto
have "project visible w⇩1 = project visible w⇩1 @ project visible w⇩2" using 3 by simp
also have "… = project visible (w⇩1 @ w⇩2)" by simp
also have "… = list_of (lproject visible (llist_of (w⇩1 @ w⇩2)))" by simp
also have "… = list_of (lproject visible (llist_of w))"
using eq_fin_lproject_visible 1 by metis
also have "… = project visible w" by simp
finally show ?thesis by this
qed
lemma reduced_run_length_1:
assumes "reduced_run q v⇩1 v⇩2 l w w⇩1 w⇩2 u"
shows "length v⇩1 ≤ length w⇩1"
using reduced_run_invar_1 assms by force
lemma reduced_run_length:
assumes "reduced_run q v⇩1 v⇩2 l w w⇩1 w⇩2 u"
shows "length v⇩1 ≤ length w"
proof -
have "length v⇩1 ≤ length w⇩1" using reduced_run_length_1 assms by this
also have "… ≤ length w" using reduced_run_decompose assms by force
finally show ?thesis by this
qed
lemma reduced_run_step:
assumes "q ∈ nodes" "run (v⇩1 @- [a] @- v⇩2) q"
assumes "reduced_run q v⇩1 ([a] @- v⇩2) l w w⇩1 w⇩2 u"
obtains l' w' w⇩1' w⇩2' u'
where "reduced_run q (v⇩1 @ [a]) v⇩2 l' (w @ w') (w⇩1 @ w⇩1') (w⇩2 @ w⇩2') u'"
proof (cases "a ∈ set l")
case True
show ?thesis
proof (rule that, rule absorb)
show "reduced_run q v⇩1 ([a] @- v⇩2) l (w @ []) (w⇩1 @ []) (w⇩2 @ []) u" using assms(3) by simp
show "a ∈ set l" using True by this
qed
next
case False
have 1: "v⇩1 @ l =⇩F w⇩1" using reduced_run_invar_1 assms(3) by this
have 2: "[a] @- v⇩2 =⇩I l @- u" using reduced_run_invar_2 assms(3) by this
have 3: "w =⇩F w⇩1 @ w⇩2" using reduced_run_decompose assms(3) by this
have "v⇩1 @ l @ w⇩2 = (v⇩1 @ l) @ w⇩2" by simp
also have "… =⇩F w⇩1 @ w⇩2" using 1 by blast
also have "… =⇩F w" using 3 by blast
finally have 4: "v⇩1 @ l @ w⇩2 =⇩F w" by this
have 5: "run ((v⇩1 @ l) @- w⇩2 @- u) q"
proof (rule diamond_fin_word_inf_word')
show "Ind (set w⇩2) (sset u)" using reduced_run_ind assms(3) by this
have 6: "R.path w q" using reduced_run_words_fin assms(3) by this
have 7: "path w q" using reduction_words_fin assms(1) 6 by auto
show "path ((v⇩1 @ l) @ w⇩2) q" using eq_fin_word 4 7 by auto
have 8: "v⇩1 @- [a] @- v⇩2 =⇩I v⇩1 @- l @- u" using 2 by blast
show "run ((v⇩1 @ l) @- u) q" using eq_inf_word assms(2) 8 by auto
qed
have 6: "run (w @- u) q" using eq_inf_word 4 5 by (metis eq_inf_concat_end shift_append)
have 7: "[a] ≼⇩F⇩I l @- u" using 2 by blast
have 8: "[a] ≼⇩F⇩I u" using le_fininf_not_member' 7 False by this
obtain u' where 9: "u =⇩I [a] @- u'" using 8 by rule
have 101: "target w q ∈ nodes" using assms(1) 6 by auto
have 10: "run ([a] @- u') (target w q)" using eq_inf_word 9 6 by blast
obtain b b⇩1 b⇩2 u'' where 11:
"R.path (b @ [a]) (target w q)"
"Ind {a} (set b)" "set b ⊆ invisible"
"b =⇩F b⇩1 @ b⇩2" "b⇩1 @- u'' =⇩I u'" "Ind (set b⇩2) (sset u'')"
using reduction_chunk 101 10 by this
show ?thesis
proof (rule that, rule extend)
show "reduced_run q v⇩1 ([a] @- v⇩2) l w w⇩1 w⇩2 u" using assms(3) by this
show "a ∉ set l" using False by this
show "R.path (b @ [a]) (target w q)" using 11(1) by this
show "Ind {a} (set b)" using 11(2) by this
show "set b ⊆ invisible" using 11(3) by this
show "b =⇩F b⇩1 @ b⇩2" using 11(4) by this
show "[a] @- b⇩1 @- u'' =⇩I u" using 9 11(5) by blast
show "Ind (set b⇩2) (sset u'')" using 11(6) by this
qed
qed
lemma reduction_word:
assumes "q ∈ nodes" "run v q"
obtains u w
where
"R.run w q"
"v =⇩I u" "u ≼⇩I w"
"lproject visible (llist_of_stream u) = lproject visible (llist_of_stream w)"
proof -
define P where "P ≡ λ k w w⇩1. ∃ l w⇩2 u. reduced_run q (stake k v) (sdrop k v) l w w⇩1 w⇩2 u"
obtain w w⇩1 where 1: "⋀ k. P k (w k) (w⇩1 k)" "chain w" "chain w⇩1"
proof (rule chain_construct_2'[of P])
show "P 0 [] []" unfolding P_def using init by force
next
fix k w w⇩1
assume 1: "P k w w⇩1"
obtain l w⇩2 u where 2: "reduced_run q (stake k v) (sdrop k v) l w w⇩1 w⇩2 u"
using 1 unfolding P_def by auto
obtain l' w' w⇩1' w⇩2' u' where 3:
"reduced_run q (stake k v @ [v !! k]) (sdrop (Suc k) v) l' (w @ w') (w⇩1 @ w⇩1') (w⇩2 @ w⇩2') u'"
proof (rule reduced_run_step)
show "q ∈ nodes" using assms(1) by this
show "run (stake k v @- [v !! k] @- sdrop (Suc k) v) q"
using assms(2) by (metis shift_append stake_Suc stake_sdrop)
show "reduced_run q (stake k v) ([v !! k] @- sdrop (Suc k) v) l w w⇩1 w⇩2 u"
using 2 by (metis sdrop_simps shift.simps stream.collapse)
qed
show "∃ w' w⇩1'. P (Suc k) w' w⇩1' ∧ w ≤ w' ∧ w⇩1 ≤ w⇩1'"
unfolding P_def using 3 by (metis prefix_fin_append stake_Suc)
show "k ≤ length w" using reduced_run_length 2 by force
show "k ≤ length w⇩1" using reduced_run_length_1 2 by force
qed rule
obtain l w⇩2 u where 2:
"⋀ k. reduced_run q (stake k v) (sdrop k v) (l k) (w k) (w⇩1 k) (w⇩2 k) (u k)"
using 1(1) unfolding P_def by metis
show ?thesis
proof
show "R.run (Word_Prefixes.limit w) q" using reduced_run_words_fin 1(2) 2 by blast
show "v =⇩I Word_Prefixes.limit w⇩1"
proof
show "v ≼⇩I Word_Prefixes.limit w⇩1"
proof (rule le_infI_chain_right')
show "chain w⇩1" using 1(3) by this
show "⋀ k. stake k v ≼⇩F w⇩1 k" using reduced_run_invar_1[OF 2] by auto
qed
show "Word_Prefixes.limit w⇩1 ≼⇩I v"
proof (rule le_infI_chain_left)
show "chain w⇩1" using 1(3) by this
next
fix k
have "w⇩1 k =⇩F stake k v @ l k" using reduced_run_invar_1 2 by blast
also have "… ≤⇩F⇩I stake k v @- l k @- u k" by auto
also have "… =⇩I stake k v @- sdrop k v" using reduced_run_invar_2[OF 2] by blast
also have "… = v" by simp
finally show "w⇩1 k ≼⇩F⇩I v" by this
qed
qed
show "Word_Prefixes.limit w⇩1 ≼⇩I Word_Prefixes.limit w"
proof (rule le_infI_chain_left)
show "chain w⇩1" using 1(3) by this
next
fix k
have "w⇩1 k ≼⇩F w k" using reduced_run_decompose[OF 2] by blast
also have "… ≤⇩F⇩I Word_Prefixes.limit w" using chain_prefix_limit 1(2) by this
finally show "w⇩1 k ≼⇩F⇩I Word_Prefixes.limit w" by this
qed
show "lproject visible (llist_of_stream (Word_Prefixes.limit w⇩1)) =
lproject visible (llist_of_stream (Word_Prefixes.limit w))"
using lproject_eq_limit_chain reduced_run_project 1 unfolding P_def by metis
qed
qed
lemma reduction_equivalent:
assumes "q ∈ nodes" "run u q"
obtains v
where "R.run v q" "snth (smap int (q ## trace u q)) ≈ snth (smap int (q ## trace v q))"
proof -
obtain v w where 1: "R.run w q" "u =⇩I v" "v ≼⇩I w"
"lproject visible (llist_of_stream v) = lproject visible (llist_of_stream w)"
using reduction_word assms by this
show ?thesis
proof
show "R.run w q" using 1(1) by this
show "snth (smap int (q ## trace u q)) ≈ snth (smap int (q ## trace w q))"
proof (rule execute_inf_visible)
show "run u q" using assms(2) by this
show "run w q" using reduction_words_inf assms(1) 1(1) by auto
have "u =⇩I v" using 1(2) by this
also have "… ≼⇩I w" using 1(3) by this
finally show "u ≼⇩I w" by this
show "w ≼⇩I w" by simp
have "lproject visible (llist_of_stream u) = lproject visible (llist_of_stream v)"
using eq_inf_lproject_visible 1(2) by this
also have "… = lproject visible (llist_of_stream w)" using 1(4) by this
finally show "lproject visible (llist_of_stream u) = lproject visible (llist_of_stream w)" by this
qed
qed
qed
lemma reduction_language_subset: "R.language ⊆ S.language"
unfolding S.language_def R.language_def using reduction_words_inf by blast
lemma reduction_language_stuttering:
assumes "u ∈ S.language"
obtains v
where "v ∈ R.language" "snth u ≈ snth v"
proof -
obtain q v where 1: "u = smap int (q ## trace v q)" "init q" "S.run v q" using assms by rule
obtain v' where 2: "R.run v' q" "snth (smap int (q ## trace v q)) ≈ snth (smap int (q ## trace v' q))"
using reduction_equivalent 1(2, 3) by blast
show ?thesis
proof (intro that R.languageI)
show "smap int (q ## trace v' q) = smap int (q ## trace v' q)" by rule
show "init q" using 1(2) by this
show "R.run v' q" using 2(1) by this
show "snth u ≈ snth (smap int (q ## trace v' q))" unfolding 1(1) using 2(2) by this
qed
qed
end
end