|
|
|
|
Quelle CSP_Laws.thy
Sprache: Isabelle
|
|
(*<*)
―‹ ********************************************************************
* Project : HOL-CSP - A Shallow Embedding of CSP in Isabelle/HOL
* Version : 2.0
*
* Author : Benoît Ballenghien, Safouan Taha, Burkhart Wolff, Lina Ye.
* (Based on HOL-CSP 1.0 by Haykal Tej and Burkhart Wolff)
*
* This file : Algebraic laws
*
* Copyright (c) 2009 Université Paris-Sud, France
* Copyright (c) 2025 Université Paris-Saclay, France
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are
* met:
*
* * Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
*
* * Redistributions in binary form must reproduce the above
* copyright notice, this list of conditions and the following
* disclaimer in the documentation and/or other materials provided
* with the distribution.
*
* * Neither the name of the copyright holders nor the names of its
* contributors may be used to endorse or promote products derived
* from this software without specific prior written permission.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
******************************************************************************›
(*>*)
section ‹ Powerful Laws of CSP ›
(*<*)
theory CSP_Laws
imports Basic_CSP_Laws Step_CSP_Laws_Extended
begin
(*>*)
subsection‹ Laws for Mndetprefix and Sync›
lemma Mndetprefix_Sync_Det_distr_FD :
‹(⊓ a ∈ A → (P a [ C ] (⊓ b ∈ B → Q b))) ◻
(⊓ b ∈ B → ((⊓ a ∈ A → P a) [ C ] Q b))
⊑FD (⊓ a ∈ A → P a) [ C ] (⊓ b ∈ B → Q b)›
(is ‹?lhs1 ◻ ?lhs2 ⊑FD ?rhs›)
if ‹A ≠ {}› ‹B ≠ {}› ‹A ∩ C = {}› ‹B ∩ C = {}›
proof -
have ‹?lhs1 = ⊓ b∈B. ⊓ a∈A. (a → (P a [C] (b → Q b)))› (is ‹_ = ?lhs1'›)
by (simp add: ‹A ≠ {}› ‹B ≠ {}› Mndetprefix_GlobalNdet
Sync_distrib_GlobalNdet_left Sync_distrib_GlobalNdet_right
write0_def GlobalNdet_Mprefix_distr[OF ‹B ≠ {}›, symmetric])
(subst GlobalNdet_sets_commute, simp)
moreover have ‹?lhs2 = ⊓ b∈B. ⊓ a∈A. (b → (a → P a [C] Q b))› (is ‹_ = ?lhs2'›)
by (simp add: ‹A ≠ {}› ‹B ≠ {}› Mndetprefix_GlobalNdet
Sync_distrib_GlobalNdet_left Sync_distrib_GlobalNdet_right
write0_def GlobalNdet_Mprefix_distr[OF ‹A ≠ {}›, symmetric])
ultimately have ‹?lhs1 ◻ ?lhs2 = ?lhs1' ◻ ?lhs2'› by simp
moreover have ‹?lhs1' ◻ ?lhs2' ⊑FD ⊓ b∈B. ⊓ a∈A. (a → (P a [C] (b → Q b)))
◻ (b → ((a → P a) [C] Q b))›
by (auto simp add: ‹A ≠ {}› ‹B ≠ {}› refine_defs GlobalNdet_projs Det_projs write0_def)
moreover have ‹… = ⊓ b∈B. ⊓ a∈A. ((a → P a) [C] (b → Q b))›
by (rule mono_GlobalNdet_eq, rule mono_GlobalNdet_eq,
simp add: write0_def, subst Mprefix_Sync_Mprefix_indep)
(use ‹A ∩ C = {}› ‹B ∩ C = {}› in auto)
moreover have ‹… = ?rhs›
by (simp add: ‹A ≠ {}› ‹B ≠ {}› Mndetprefix_GlobalNdet
Sync_distrib_GlobalNdet_left Sync_distrib_GlobalNdet_right)
ultimately show ‹?lhs1 ◻ ?lhs2 ⊑FD ?rhs› by argo
qed
lemmas Mndetprefix_Sync_Det_distr_F = Mndetprefix_Sync_Det_distr_FD[THEN leFD_imp_leF]
and Mndetprefix_Sync_Det_distr_D = Mndetprefix_Sync_Det_distr_FD[THEN leFD_imp_leD]
lemmas Mndetprefix_Sync_Det_distr_T = Mndetprefix_Sync_Det_distr_F[THEN leF_imp_leT]
lemma Mndetprefix_Sync_Det_distr_DT :
‹[A ≠ {}; B ≠ {}; A ∩ C = {}; B ∩ C = {}] ==>
(⊓ a ∈ A → (P a [ C ] (⊓ b ∈ B → Q b))) ◻
(⊓ b ∈ B → ((⊓ a ∈ A → P a) [ C ] Q b))
⊑DT (⊓ a ∈ A → P a) [ C ] (⊓ b ∈ B → Q b)›
by (simp add: Mndetprefix_Sync_Det_distr_D Mndetprefix_Sync_Det_distr_T leD_leT_imp_leDT)
subsection ‹Hiding Operator Laws›
theorem Hiding_Hiding_less_eq_process_Hiding_Un : ‹P \ A \ B ⊑FD P \ (A ∪ B)›
proof (rule failure_divergence_refine_optimizedI)
fix s assume ‹s ∈ D (P \ (A ∪ B))›
then obtain t u
where * : ‹ftF u› ‹tF t› ‹s = trace_hide t (ev ` (A ∪ B)) @ u›
‹t ∈ D P ∨ (∃f. isInfHiddenRun f P (A ∪ B) ∧ t ∈ range f)›
unfolding D_Hiding by blast
have ** : ‹trace_hide t (ev ` (A ∪ B)) = trace_hide (trace_hide t (ev ` A)) (ev ` B)›
using trace_hide_ev_union by blast
from "*"(4) show ‹s ∈ D (P \ A \ B)›
proof (elim disjE exE)
assume ‹t ∈ D P›
with mem_D_imp_mem_D_Hiding have ‹trace_hide t (ev ` A) ∈ D (P \ A)› by blast
thus ‹s ∈ D (P \ A \ B)›
by (subst D_Hiding) (use"*"(1, 2, 3) "**" Hiding_tickFree in blast)
next
fix f assume ** : ‹isInfHiddenRun f P (A ∪ B) ∧ t ∈ range f›
hence ‹strict_mono f› by simp
define ff where ‹ff i ≡ take (i + length (f 0)) (f i)› for i
have *** : ‹isInfHiddenRun ff P (A ∪ B) ∧ t ∈ range ff›
proof (intro conjI allI)
show ‹strict_mono ff›
proof (unfold strict_mono_Suc_iff, rule allI, unfold ff_def)
fix i nat
from length_strict_mono[of f ‹Suc i›, OF ‹strict_mono f›]
have $ : ‹take (i + length (f 0)) (f (Suc i)) < take ((Suc i) + length (f 0)) (f (Suc i))›
by (simp add: take_Suc_conv_app_nth)
from ‹strict_mono f›[THEN strict_monoD, of i ‹Suc i›, simplified]
obtain t where ‹f (Suc i) = f i @ t› by (meson strict_prefixE')
with length_strict_mono[of f i, OF ‹strict_mono f›]
have ‹take (i + length (f 0)) (f i) = take (i + length (f 0)) (f (Suc i))› by simp
with "$" show ‹take (i + length (f 0)) (f i) < take (Suc i + length (f 0)) (f (Suc i))› by simp
qed
next
show ‹ff i ∈ T P› for i
by (unfold ff_def) (metis "**" prefixI append_take_drop_id is_processT3_TR)
next
show ‹trace_hide (ff i) (ev ` (A ∪ B)) = trace_hide (ff 0) (ev ` (A ∪ B))› for i
proof (rule order_antisym)
have ‹f 0 ≤ f i› by (simp add: "**" strict_mono_less_eq)
hence ‹f 0 ≤ take (i + length (f 0)) (f i)›
by (metis prefixE Prefix_Order.prefixI le_add2 take_all_iff take_append)
from mono_trace_hide[OF this]
show ‹trace_hide (ff 0) (ev ` (A ∪ B)) ≤ trace_hide (ff i) (ev ` (A ∪ B))›
by (unfold ff_def) (metis le_add2 take_all_iff)
next
have ‹take (i + length (f 0)) (f i) ≤ f i›
by (metis prefixI append_take_drop_id)
from mono_trace_hide[OF this]
show ‹trace_hide (ff i) (ev ` (A ∪ B)) ≤ trace_hide (ff 0) (ev ` (A ∪ B))›
by (unfold ff_def) (metis "**" le_add2 take_all_iff)
qed
next
from "**" obtain i where ‹t = f i› by blast
moreover have ‹f 0 ≤ f i› by (simp add: "**" strict_mono_less_eq)
ultimately have ‹t = ff (max i (length t - length (f 0)))›
by (simp add: ff_def max_def le_length_mono)
(metis "**" prefixE append_eq_conv_conj strict_mono_less_eq)
thus ‹t ∈ range ff› by blast
qed
show ‹s ∈ D (P \ A \ B)›
proof (cases ‹∃m. ∀i>m. last (ff i) ∈ ev ` A›)
assume ‹∃m. ∀i>m. last (ff i) ∈ ev ` A›
then obtain m where $ : ‹m < i ==> last (ff i) ∈ ev ` A› for i by blast
hence ‹tF (ff m)›
by (metis "***" strict_prefixE' append_T_imp_tickFree list.distinct(1) strict_mono_Suc_iff)
have $$ : ‹∃t. ff (i + m) = ff m @ t ∧ set t ⊆ ev ` A› for i
proof (induct i)
show ‹∃t. ff (0 + m) = ff m @ t ∧ set t ⊆ ev ` A› by simp
next
fix i assume ‹∃t. ff (i + m) = ff m @ t ∧ set t ⊆ ev ` A›
then obtain t where ‹ff (i + m) = ff m @ t› ‹set t ⊆ ev ` A› by blast
obtain r where ‹ff (Suc i + m) = ff (i + m) @ r›
by (metis "***" strict_prefixE' add_Suc strict_mono_Suc_iff)
moreover have ‹length (ff (Suc i + m)) = Suc (length (ff (i + m)))›
by (simp add: ff_def) (metis "**" add_Suc length_strict_mono min_absorb2)
ultimately have ‹length r = 1› by (metis Suc_eq_plus1 add_left_cancel length_append)
with ‹ff (Suc i + m) = ff (i + m) @ r›
have ‹ff (Suc i + m) = ff (i + m) @ [last (ff (Suc i + m))]› by (cases r) simp_all
with ‹ff (i + m) = ff m @ t›
have ‹ff (Suc i + m) = ff m @ t @ [last (ff (Suc i + m))]› by simp
moreover have ‹last (ff (Suc i + m)) ∈ ev ` A› by (simp add: "$")
ultimately show ‹∃t. ff (Suc i + m) = ff m @ t ∧ set t ⊆ ev ` A›
by (intro exI[of _ ‹t @ [last (ff (Suc i + m))]›]) (simp add: ‹set t ⊆ ev ` A›)
qed
then obtain fff where $$$$ : ‹ff (i + m) = ff m @ fff i› ‹set (fff i) ⊆ ev ` A› for i by metis
show ‹s ∈ D (P \ A \ B)›
apply (simp add: D_Hiding)
apply (rule exI[of _ ‹trace_hide (ff m) (ev ` A)›], rule exI[of _ u], intro conjI)
subgoal by (fact ‹ftF u›)
subgoal using Hiding_tickFree ‹tF (ff m)› by blast
subgoal by (metis (no_types) "*"(3) "***" rangeE trace_hide_ev_union)
apply (rule disjI1)
apply (rule exI[of _ ‹ff m›], rule exI[of _ ‹[]›], simp add: ‹tF (ff m)›)
apply (rule disjI2)
apply (rule exI[of _ ‹λi. ff (i + m)›], intro conjI)
subgoal by (metis (mono_tags, lifting) "***" add_Suc strict_mono_Suc_iff)
subgoal using "***" by blast
subgoal using "$$$$" by (simp add: subset_iff)
by (metis (mono_tags) add_0 rangeI)
next
assume ‹∄m. ∀i>m. last (ff i) ∈ ev ` A›
{ fix i :: nat assume ‹0 < i›
from "***" obtain t where ‹ff i = ff 0 @ t› ‹set t ⊆ ev ` (A ∪ B)›
unfolding isInfHiddenRun_1 by blast
with ‹0 < i› have ‹last (ff i) ∈ ev ` (A ∪ B)›
by (cases t) (auto simp add: "***" strict_mono_eq)
}
with ‹∄m. ∀i>m. last (ff i) ∈ ev ` A› have $ : ‹∀i. ∃j>i. last(ff j) ∈ ev ` B - ev ` A›
by (metis Un_Diff_cancel2 Un_iff gr0I image_Un not_less0)
define fff where ‹fff = rec_nat t (λi t. ff (SOME j. t < ff j ∧ last (ff j) ∈ ev ` B - ev ` A))›
hence ‹fff i ∈ range ff› for i
unfolding fff_def
by (metis (mono_tags, lifting) "***" gr0_conv_Suc nat.rec(2)
old.nat.simps(6) rangeI zero_less_iff_neq_zero)
have $$$ : ‹strict_mono (λi. trace_hide (fff i) (ev ` A))›
proof (unfold strict_mono_Suc_iff, rule allI)
fix i
have "£" : ‹fff (Suc i) = ff (SOME j. fff i < ff j ∧ last (ff j) ∈ ev ` B - ev ` A)›
by (simp add: fff_def)
from ‹∧i. fff i ∈ range ff› obtain j where ‹fff i = ff j› by blast
hence ‹∃j. fff i < ff j ∧ last (ff j) ∈ ev ` B - ev ` A› by (metis "$" "***" monotoneD)
hence "££" : ‹fff i < fff (Suc i) ∧ last (fff (Suc i)) ∉ ev ` A›
by (metis (no_types, lifting) Diff_iff "£" someI_ex)
then obtain r where ‹fff (Suc i) = fff i @ r› ‹last r ∉ ev ` A›
by (metis append_self_conv last_append less_eq_list_def prefix_def less_list_def)
thus ‹trace_hide (fff i) (ev ` A) < trace_hide (fff (Suc i)) (ev ` A)›
by (metis (mono_tags, lifting) prefixI "££" empty_filter_conv
filter_append last_in_set nless_le self_append_conv)
qed
show ‹s ∈ D (P \ A \ B)›
apply (simp add: D_Hiding)
apply (rule exI[of _ ‹trace_hide t (ev ` A)›], rule exI[of _ u], intro conjI)
subgoal by (fact ‹ftF u›)
subgoal using Hiding_tickFree ‹tF t› by blast
subgoal by (simp add: "*"(3))
apply (rule disjI2)
apply (rule exI[of _ ‹λi. trace_hide (fff i) (ev ` A)›], intro conjI)
subgoal by (fact "$$$")
subgoal by (metis "***" ‹∧i. fff i ∈ range ff› mem_T_imp_mem_T_Hiding rangeE)
subgoal by (metis (no_types) "***" ‹∧i. fff i ∈ range ff› rangeE trace_hide_ev_union)
by (metis (mono_tags, lifting) fff_def old.nat.simps(6) rangeI)
qed
qed
next
assume subset_div : ‹D (P \ (A ∪ B)) ⊆ D (P \ A \ B)›
fix s X assume ‹(s, X) ∈ F (P \ (A ∪ B))›
then consider ‹s ∈ D (P \ (A ∪ B))›
| t where ‹s = trace_hide t (ev ` (A ∪ B))› ‹(t, X ∪ ev ` (A ∪ B)) ∈ F P›
unfolding F_Hiding D_Hiding by blast
thus ‹(s, X) ∈ F (P \ A \ B)›
proof cases
from subset_div D_F show ‹s ∈ D (P \ (A ∪ B)) ==> (s, X) ∈ F (P \ A \ B)› by blast
next
fix t assume ‹s = trace_hide t (ev ` (A ∪ B))› ‹(t, X ∪ ev ` (A ∪ B)) ∈ F P›
hence * : ‹s = trace_hide (trace_hide t (ev ` A)) (ev ` B)›
‹(t, X ∪ ev ` B ∪ ev ` A) ∈ F P›
by (simp_all add: image_Un sup_commute sup_left_commute)
show ‹(s, X) ∈ F (P \ A \ B)›
by (simp add: F_Hiding) (use "*" in blast)
qed
qed
theorem Hiding_Un : ‹P \ (A ∪ B) = P \ A \ B›
if ‹finite A› for P :: ‹('a, 'r) processptick›
proof (rule order_antisym)
show ‹P \ (A ∪ B) ≤ P \ A \ B›
proof (rule failure_divergence_refine_optimizedI)
fix s assume ‹s ∈ D (P \ A \ B)›
then obtain t u
where * : ‹ftF u› ‹tF t› ‹s = trace_hide t (ev ` B) @ u›
‹t ∈ D (P \ A) ∨ (∃x. isInfHidden_seqRun_strong x (P \ A) B t)›
by (elim D_Hiding_seqRunE)
from "*"(4) show ‹s ∈ D (P \ (A ∪ B))›
proof (elim disjE exE)
assume ‹t ∈ D (P \ A)›
then obtain t' u'
where ** : ‹ftF u'› ‹tF t'› ‹t = trace_hide t' (ev ` A) @ u'›
‹t' ∈ D P ∨ (∃x. isInfHidden_seqRun_strong x P A t')›
by (elim D_Hiding_seqRunE)
from "*"(1, 2) "**"(3) have *** : ‹ftF (trace_hide u' (ev ` B) @ u)›
using Hiding_tickFree front_tickFree_append tickFree_append_iff by blast
show ‹s ∈ D (P \ (A ∪ B))›
apply (unfold D_Hiding_seqRun, clarify)
apply (rule exI[of _ t'], rule exI[of _ ‹trace_hide u' (ev ` B) @ u›])
apply (intro conjI)
subgoal by (fact "***")
subgoal by (fact "**"(2))
subgoal by (simp add: "*"(3) "**"(3))
by (metis "**"(4) Un_iff image_Un)
next
fix x assume ** : ‹isInfHidden_seqRun_strong x (P \ A) B t›
have trH_x : ‹trace_hide (seqRun t x i) (ev ` B) = trace_hide t (ev ` B)› for i
using "**" trace_hide_seqRun_eq_iff by blast
from "**" have ‹∀i. seqRun t x i ∈ {trace_hide t (ev ` A) |t. (t, ev ` A) ∈ F P}›
unfolding T_Hiding D_Hiding by blast
with F_T have ‹∀i. ∃w. seqRun t x i = trace_hide w (ev ` A) ∧ w ∈ T P› by blast
then obtain f where *** : ‹seqRun t x i = trace_hide (f i) (ev ` A)› ‹f i ∈ T P› for i by metis
have ‹inj f› by (rule injI) (metis "***"(1) seqRun_eq_iff)
with finite_imageD have ‹infinite (range f)› by blast
have $ : ‹set (take i t') ⊆ set (seqRun t x i) ∪ ev ` A› if ‹t' ∈ range f› for i t'
proof -
from ‹t' ∈ range f› obtain j where ‹t' = f j› ..
hence "£" : ‹seqRun t x j = trace_hide t' (ev ` A)› ‹t' ∈ T P› by (simp_all add: "***")
consider ‹i ≤ j› | ‹j ≤ i› by linarith
thus ‹set (take i t') ⊆ set (seqRun t x i) ∪ ev ` A›
proof cases
assume ‹j ≤ i›
hence ‹seqRun t x j ≤ seqRun t x i› by simp
hence ‹set (seqRun t x j) ⊆ set (seqRun t x i)›
by (metis prefixE Un_iff set_append subsetI)
moreover have ‹set (take i t') ⊆ set (seqRun t x j) ∪ ev ` A›
by (rule subsetI, drule in_set_takeD) (simp add: "£"(1))
ultimately show ‹set (take i t') ⊆ set (seqRun t x i) ∪ ev ` A› by blast
next
assume ‹i ≤ j›
hence ‹seqRun t x i ≤ seqRun t x j› by simp
hence ‹take i (seqRun t x j) ≤ seqRun t x i› by simp
have ‹seqRun t x j = trace_hide (take i t') (ev ` A) @ trace_hide (drop i t') (ev ` A)›
by (metis "£"(1) append_take_drop_id filter_append)
moreover have ‹length (trace_hide (take i t') (ev ` A)) ≤ i›
by (metis length_filter_le length_take min.bounded_iff)
ultimately have ‹trace_hide (take i t') (ev ` A) ≤ take i (seqRun t x j)› by simp
with ‹take i (seqRun t x j) ≤ seqRun t x i› obtain t''
where ‹seqRun t x i = trace_hide (take i t') (ev ` A) @ t''›
by (meson prefixE dual_order.trans)
thus ‹set (take i t') ⊆ set (seqRun t x i) ∪ ev ` A› by (simp add: subsetI)
qed
qed
have ‹finite {take i w |w. w ∈ range f}› for i
proof (induct i)
show ‹finite {take 0 w |w. w ∈ range f}› by simp
next
fix i assume hyp : ‹finite {take i w |w. w ∈ range f}›
show ‹finite {take (Suc i) w |w. w ∈ range f}›
proof (rule finite_subset)
show ‹ {take (Suc i) w |w. w ∈ range f}
⊆ {take i w |w. w ∈ range f}
∪ (∪e∈set (seqRun t x (Suc i)) ∪ ev ` A. {take i w @ [e] |w. w ∈ range f})›
(is ‹?lhs ⊆ {take i w |w. w ∈ range f} ∪ (∪e∈?S1. ?S2 e)›)
proof (intro subsetI)
fix t' assume ‹t' ∈ ?lhs›
then obtain w where "£" : ‹t' = take (Suc i) w› ‹w ∈ range f› by blast
show ‹t' ∈ {take i w |w. w ∈ range f} ∪ (∪e∈?S1. ?S2 e)›
proof (cases ‹i < length t'›)
assume ‹i < length t'›
with "£"(1) take_Suc_conv_app_nth
have ‹take (Suc i) t' = take i w @ [t' ! i]› by auto
moreover from "£" "$" ‹i < length t'› nth_mem have ‹t' ! i ∈ ?S1› by blast
ultimately have ‹t' ∈ (∪e∈?S1. ?S2 e)›
by (intro UN_I[of ‹t' ! i›], simp_all)
(metis "£" less_not_refl min.absorb2 not_le_imp_less take_take)
thus ‹t' ∈ {take i w |w. w ∈ range f} ∪ (∪e∈?S1. ?S2 e)› by simp
next
assume ‹¬ i < length t'›
hence ‹take (Suc i) t' = take i t'› by simp
with "£" show ‹t' ∈ {take i w |w. w ∈ range f} ∪ (∪e∈?S1. ?S2 e)› by auto
qed
qed
next
show ‹finite ({take i w |w. w ∈ range f} ∪
(∪e∈set (seqRun t x (Suc i)) ∪ ev ` A.
{take i w @ [e] |w. w ∈ range f}))›
proof (rule finite_UnI)
show ‹finite {take i w |w. w ∈ range f}› by (fact hyp)
next
show ‹finite (∪e∈set (seqRun t x (Suc i)) ∪ ev ` A. {take i w @ [e] |w. w ∈ range f})›
proof (rule finite_UN_I)
show ‹finite (set (seqRun t x (Suc i)) ∪ ev ` A)›
by (simp add: ‹finite A›) ―‹Here we use that term‹A› is const‹finite›.›
next
fix e assume ‹e ∈ set (seqRun t x (Suc i)) ∪ ev ` A›
have ‹ {take i w @ [e] |w. w ∈ range f}
= (λt'. t' @ [e]) ` {take i w |w. w ∈ range f}› by auto
also have ‹finite …› by (rule finite_imageI) (fact hyp)
finally show ‹finite {take i w @ [e] |w. w ∈ range f}› .
qed
qed
qed
qed
also have ‹{take i w |w. w ∈ range f} = {w. ∃t'∈range f. w = take i t'}› for i by auto
finally have ‹∀i. finite {w. ∃t'∈range f. w = take i t'}› ..
from KoenigLemma[OF ‹infinite (range f)› this]
obtain ff :: ‹nat → ('a, 'r) traceptick›
where $$ : ‹strict_mono ff› ‹range ff ⊆ {t. ∃t'∈range f. t ≤ t'}› by blast
from "$$"(2) have $$$ : ‹∃t'. ff (Suc j) ≤ t' ∧ t' ∈ range f› for j by blast
hence ‹ftF (ff (Suc j))› for j
by (metis "***"(2) imageE is_processT2_TR is_processT3_TR)
hence ‹tF (ff j)› for j
using strict_monoD[OF "$$"(1), of j ‹Suc j›, simplified]
by (metis strict_prefixE' front_tickFree_append_iff list.distinct(1))
from "$$"(2) "***"(2) have ‹ff (j + i) ∈ T P› for i j
by (simp add: subset_iff) (meson is_processT3_TR rangeI)
have $$$$ : ‹∃w. trace_hide (ff i) (ev ` A) ≤ t @ w› for i
proof -
from "$$"(2) obtain j where ‹ff i ≤ f j› by auto
moreover from "**" isInfHiddenRun_1 have ‹∃w. seqRun t x j = t @ w›
by (simp add: seqRun_def)
ultimately show ‹∃w. trace_hide (ff i) (ev ` A) ≤ t @ w›
by (metis "***"(1) mono_trace_hide)
qed
have ‹∃i. t ≤ trace_hide (ff i) (ev ` A)›
proof (rule ccontr)
define fff where ‹fff i ≡ trace_hide (ff i) (ev ` A)› for i
assume assm : ‹∄i. t ≤ fff i›
moreover from "$$$$" have ‹∀i. ∃w. fff i ≤ t @ w› unfolding fff_def ..
ultimately have assm_bis : ‹∀i. fff i ≤ t›
by (metis prefixI le_same_imp_eq_or_less order.order_iff_strict)
have ‹mono fff›
by (rule monoI, simp add: fff_def)
(metis "$$"(1) prefixE prefixI filter_append strict_mono_less_eq)
from mono_constant[OF this assm_bis]
obtain j where ‹j ≤ i ==> fff i = fff j› for i by blast
have ‹fff j ∈ D (P \ A)›
apply (unfold D_Hiding, clarify)
apply (rule exI[of _ ‹ff j›], rule exI[of _ ‹[]›])
apply (simp add: fff_def ‹tF (ff j)›)
apply (rule disjI2)
apply (rule exI[of _ ‹λi. ff (j + i)›])
apply (intro conjI)
subgoal by (simp add: "$$"(1) strict_monoI strict_mono_less)
subgoal by (simp add: ‹∧i. ff (j + i) ∈ T P›)
subgoal by (metis ‹∧i. j ≤ i ==> fff i = fff j› fff_def le_add1)
subgoal by (metis Nat.add_0_right rangeI) .
thus False
by (metis (no_types) "**" prefixE T_imp_front_tickFree append.right_neutral assm_bis
front_tickFree_append_iff is_processT3_TR is_processT7 t_le_seqRun)
qed
then obtain j where ‹t ≤ trace_hide (ff j) (ev ` A)› ..
have "£" : ‹s = trace_hide (ff j) (ev ` (A ∪ B)) @ u›
proof (unfold "*"(3), rule arg_cong[where f = ‹λx. x @ _›])
from "$$"(1) "$$$" obtain l where ‹ff j ≤ f l›
by (metis dual_order.trans order_less_imp_le rangeE strict_mono_Suc_iff)
from mono_trace_hide[OF this] have ‹trace_hide (ff j) (ev ` A) ≤ seqRun t x l›
unfolding "***"(1) by presburger
with mono_trace_hide[OF this] mono_trace_hide[OF ‹t ≤ trace_hide (ff j) (ev ` A)›]
show ‹trace_hide t (ev ` B) = trace_hide (ff j) (ev ` (A ∪ B))›
by (metis trH_x dual_order.eq_iff trace_hide_ev_union)
qed
have "££" : ‹trace_hide (ff (j + i)) (ev ` (A ∪ B)) = trace_hide (ff (j + 0)) (ev ` (A ∪ B))› for i
proof -
from "$$"(1) "$$$" obtain l where ‹ff (j + i) ≤ f l›
by (metis dual_order.trans order_less_imp_le rangeE strict_mono_Suc_iff)
from mono_trace_hide[OF this] have ‹trace_hide (ff (j + i)) (ev ` A) ≤ seqRun t x l›
unfolding "***"(1) by presburger
from mono_trace_hide[OF this, of B]
mono_trace_hide[THEN mono_trace_hide, of _ _ B A,
OF ‹strict_mono ff›[THEN strict_mono_mono, THEN monoD, of j ‹j + i›, simplified]]
mono_trace_hide[OF ‹t ≤ trace_hide (ff j) (ev ` A)›, of B]
show ‹trace_hide (ff (j + i)) (ev ` (A ∪ B)) =
trace_hide (ff (j + 0)) (ev ` (A ∪ B))› by (simp add: trH_x)
qed
show ‹s ∈ D (P \ (A ∪ B))›
apply (unfold D_Hiding, clarify)
apply (rule exI[of _ ‹ff j›], rule exI[of _ u])
apply (intro conjI)
subgoal by (fact ‹ftF u›)
subgoal by (fact ‹tF (ff j)›)
subgoal by (fact "£")
apply (rule disjI2)
apply (rule exI[of _ ‹λi. ff (j + i)›])
apply (intro conjI)
subgoal by (simp add: "$$"(1) strict_monoI strict_mono_less)
subgoal by (simp add: ‹∧i. ff (j + i) ∈ T P›)
subgoal by (use "££" in blast)
by (metis Nat.add_0_right rangeI)
qed
next
assume subset_div : ‹D (P \ A \ B) ⊆ D (P \ (A ∪ B))›
fix s X assume ‹(s, X) ∈ F (P \ A \ B)›
from this[simplified F_Hiding[of ‹P \ A› B]] D_Hiding[of ‹P \ A› B]
consider ‹s ∈ D (P \ A \ B)›
| t where ‹s = trace_hide t (ev ` B)› ‹(t, X ∪ ev ` B) ∈ F (P \ A)› by blast
thus ‹(s, X) ∈ F (P \ (A ∪ B))›
proof cases
from subset_div D_F show ‹s ∈ D (P \ A \ B) ==> (s, X) ∈ F (P \ (A ∪ B))› by blast
next
fix t assume * : ‹s = trace_hide t (ev ` B)› ‹(t, X ∪ ev ` B) ∈ F (P \ A)›
from "*"(2) consider ‹t ∈ D (P \ A)›
| u where ‹t = trace_hide u (ev ` A)› ‹(u, X ∪ ev ` B ∪ ev ` A) ∈ F P›
unfolding F_Hiding D_Hiding by blast
thus ‹(s, X) ∈ F (P \ (A ∪ B))›
proof cases
assume ‹t ∈ D (P \ A)›
with "*"(1) mem_D_imp_mem_D_Hiding have ‹s ∈ D (P \ A \ B)› by fast
with subset_div D_F show ‹(s, X) ∈ F (P \ (A ∪ B))› by blast
next
fix u assume ** : ‹t = trace_hide u (ev ` A)› ‹(u, X ∪ ev ` B ∪ ev ` A) ∈ F P›
from "*"(1) "**"(1) have ‹s = trace_hide u (ev ` (A ∪ B))› by simp
moreover from "**"(2) have ‹(u, X ∪ ev ` (A ∪ B)) ∈ F P›
by (simp add: image_Un sup_commute sup_left_commute)
ultimately show ‹(s, X) ∈ F (P \ (A ∪ B))› unfolding F_Hiding by blast
qed
qed
qed
next
show ‹P \ A \ B ≤ P \ (A ∪ B)› by (fact Hiding_Hiding_less_eq_process_Hiding_Un)
qed
subsection‹ Sync Operator Laws ›
subsubsection‹ Preliminaries ›
lemma tickFree_isInfHiddenRun : ‹tF s›
if ‹isInfHiddenRun f P A› and ‹s ∈ range f›
proof -
from ‹s ∈ range f› obtain i where ‹s = f i› ..
moreover have ‹f i < f (Suc i)› by (meson ‹isInfHiddenRun f P A› strict_mono_Suc_iff)
ultimately obtain t where ‹t ≠ []› ‹f (Suc i) = s @ t› by (meson strict_prefixE' list.discI)
moreover from ‹isInfHiddenRun f P A› is_processT2_TR
have ‹ftF (f (Suc i))› by blast
ultimately show ‹tF s› by (simp add: front_tickFree_append_iff)
qed
lemma Hiding_interleave:
‹r setinterleaves ((t, u), C) ==>
(trace_hide r A) setinterleaves ((trace_hide t A, trace_hide u A), C)›
(* The hypothesis \<open>A \<inter> C = {}\<close> was useless, see if we can obtain more powerful results *)
proof (induct ‹(t, C, u)› arbitrary: r t u rule: setinterleaving.induct)
case 1 thus ?case by simp
next
case (2 x t) thus ?case by auto
next
case (3 y u) thus ?case by auto
next
case (4 x t y u)
thus ?case
by (simp split: if_splits)
(safe, simp_all, (use SyncSingleHeadAdd setinterleaving_sym in blast)+)
qed
lemma non_Sync_interleaving:
‹(set t ∪ set u) ∩ C = {} ==> setinterleaving (t, C, u) ≠ {}› (* FINALLY NON-USED*)
by (induct ‹(t, C, u)› arbitrary: t u rule: setinterleaving.induct) simp_all
lemma interleave_Hiding:
‹s setinterleaves ((trace_hide t A, trace_hide u A), C)
==> ∃r. s = trace_hide r A ∧ r setinterleaves ((t, u), C)› if ‹A ∩ C = {}›
proof (induct ‹(t, C, u)› arbitrary: t u s rule: setinterleaving.induct)
case 1
thus ?case by simp
next
case (2 y u)
from "2.prems" ‹A ∩ C = {}› show ?case
by (simp add: disjoint_iff split: if_split_asm)
(metis "2.hyps" "2.prems" emptyLeftProperty filter.simps(1))+
next
case (3 x t)
from "3.prems" ‹A ∩ C = {}› show ?case
by (simp add: disjoint_iff split: if_split_asm)
(metis "3.hyps" "3.prems" emptyRightProperty filter.simps(1))+
next
case (4 x t y u)
from "4.prems" ‹A ∩ C = {}› show ?case
apply (cases ‹x = y›, simp_all add: disjoint_iff split: if_split_asm)
subgoal using "4.hyps"(1) by force
subgoal by (metis (no_types, lifting) "4.hyps"(3) "4.hyps"(4) filter.simps(2))
subgoal by (metis (no_types, lifting) "4.hyps"(3) filter.simps(2))
subgoal using "4.hyps"(2) by force
subgoal by (metis (no_types, lifting) "4.hyps"(3) "4.hyps"(4) filter.simps(2))
subgoal using "4.hyps"(5) by force
subgoal by (metis (no_types, lifting) "4.hyps"(2) "4.hyps"(4) filter.simps(2))
subgoal by (metis (no_types, lifting) "4.hyps"(3) "4.hyps"(5) filter.simps(2))
subgoal by (metis (no_types, lifting) "4.hyps"(4) filter.simps(2))
done
qed
lemma le_trace_hide : ‹u ≤ trace_hide t S ==> ∃u'. u = trace_hide u' S ∧ u' ≤ t›
proof (induct t arbitrary: u)
show ‹u ≤ trace_hide [] S ==> ∃u'. u = trace_hide u' S ∧ u' ≤ []› for u by simp
next
fix a t u assume prem: ‹u ≤ trace_hide (a # t) S›
assume hyp : ‹u ≤ trace_hide t S ==> ∃u'. u = trace_hide u' S ∧ u' ≤ t› for u
from prem consider ‹u = []› | ‹a ∈ S› ‹u ≤ trace_hide t S›
| v where ‹a ∉ S› ‹u = a # v› ‹v ≤ trace_hide t S›
by (cases u) (simp_all split: if_split_asm)
thus ‹∃u'. u = trace_hide u' S ∧ u' ≤ a # t›
proof cases
show ‹u = [] ==> ∃u'. u = trace_hide u' S ∧ u' ≤ a # t›
by (metis filter.simps(1) nil_le)
next
assume ‹a ∈ S› ‹u ≤ trace_hide t S›
from hyp[OF ‹u ≤ trace_hide t S›] obtain u' where ‹u = trace_hide u' S ∧ u' ≤ t› ..
with ‹a ∈ S› have ‹u = trace_hide (a # u') S ∧ a # u' ≤ a # t› by simp
thus ‹∃u'. u = trace_hide u' S ∧ u' ≤ a # t› ..
next
fix v assume ‹a ∉ S› ‹u = a # v› ‹v ≤ trace_hide t S›
from hyp[OF ‹v ≤ trace_hide t S›] obtain v' where ‹v = trace_hide v' S ∧ v' ≤ t› ..
with ‹a ∉ S› ‹u = a # v› have ‹u = trace_hide (a # v') S ∧ a # v' ≤ a # t› by simp
thus ‹∃u'. u = trace_hide u' S ∧ u' ≤ a # t› ..
qed
qed
lemma append_interleave :
‹s1 setinterleaves ((t1, u1), S) ==> s2 setinterleaves ((t2, u2), S) ==>
(s1 @ s2) setinterleaves ((t1 @ t2, u1 @ u2), S)›
proof (induct ‹(t1, S, u1)› arbitrary: s1 t1 u1 rule: setinterleaving.induct)
case 1 thus ?case by simp
next
case (2 y u1)
thus ?case by (auto split: if_split_asm)
(use SyncSingleHeadAdd setinterleaving_sym in blast)
next
case (3 x t1)
thus ?case by (auto split: if_split_asm) (blast intro: SyncSingleHeadAdd)
next
case (4 x t2 y u2)
thus ?case by auto
qed
subsubsection ‹The Theorem: Sync and Hiding›
theorem Hiding_Sync : ‹(P [S] Q) \ A = (P \ A) [S] (Q \ A)›
if ‹finite A› and ‹A ∩ S = {}› for P Q :: ‹('a, 'r) processptick›
― ‹Monster theorem!›
proof (subst Process_eq_spec_optimized, safe)
let ?trH_A = ‹λt. trace_hide t (ev ` A)› and ?tick_S = ‹range tick ∪ ev ` S›
fix s assume ‹s ∈ D (P [S] Q \ A)›
then obtain t u
where * : ‹ftF u› ‹tF t› ‹s = ?trH_A t @ u›
‹t ∈ D (P [S] Q) ∨ (∃x. isInfHidden_seqRun_strong x (P [S] Q) A t)›
by (elim D_Hiding_seqRunE)
from "*"(4) show ‹s ∈ D ((P \ A) [S] (Q \ A))›
proof (elim disjE exE)
assume ‹t ∈ D (P [S] Q)›
then obtain t' u' r' v'
where ** : ‹ftF v'› ‹tF r' ∨ v' = []›
‹t = r' @ v'› ‹r' setinterleaves ((t', u'), ?tick_S)›
‹t' ∈ D P ∧ u' ∈ T Q ∨ t' ∈ D Q ∧ u' ∈ T P›
unfolding D_Sync by blast
{ fix t' u' and P Q
assume *** : ‹r' setinterleaves ((t', u'), ?tick_S)›
‹t' ∈ D P› ‹u' ∈ T Q›
have ‹?trH_A r' setinterleaves ((?trH_A t', ?trH_A u'), ?tick_S)›
using "***"(1) Hiding_interleave by blast
moreover from "***"(2) mem_D_imp_mem_D_Hiding have ‹?trH_A t' ∈ D (P \ A)› by blast
moreover from "***"(3) mem_T_imp_mem_T_Hiding have ‹?trH_A u' ∈ T (Q \ A)› by blast
ultimately have ‹s ∈ D ((P \ A) [S] (Q \ A))›
apply (simp add: "*"(3) D_Sync)
apply (rule exI[of _ ‹?trH_A t'›], rule exI[of _ ‹?trH_A u'›],
rule exI[of _ ‹?trH_A r'›], rule exI[of _ ‹?trH_A v' @ u›])
apply (simp add: "*"(3) "**"(3) Hiding_tickFree)
using "*"(1, 2) "**"(3) Hiding_tickFree front_tickFree_append tickFree_append_iff by blast
} note $ = this
from "**"(5) show ‹s ∈ D ((P \ A) [S] (Q \ A))›
proof (elim disjE conjE)
show ‹t' ∈ D P ==> u' ∈ T Q ==> s ∈ D ((P \ A) [S] (Q \ A))›
by (metis "$" "**"(4))
show ‹t' ∈ D Q ==> u' ∈ T P ==> s ∈ D ((P \ A) [S] (Q \ A))›
by (metis "$" "**"(4) Sync_commute)
qed
next
fix x assume ** : ‹isInfHidden_seqRun_strong x (P [S] Q) A t›
from "**" have *** : ‹∃t' u'. t' ∈ T P ∧ u' ∈ T Q ∧
seqRun t x i setinterleaves ((t', u'), ?tick_S)› for i
unfolding T_Sync D_Sync by blast
define ftu where ‹ftu i ≡ SOME (t', u'). t' ∈ T P ∧ u' ∈ T Q ∧
seqRun t x i setinterleaves ((t', u'), ?tick_S)› for i
define ft fu where ‹ft ≡ λi. fst (ftu i)› and ‹fu ≡ λi. snd (ftu i)›
have **** : ‹ft i ∈ T P› ‹fu i ∈ T Q›
‹seqRun t x i setinterleaves ((ft i, fu i), ?tick_S)› for i
by (use "***"[of i] in ‹simp add: ft_def fu_def,
cases ‹ftu i›, simp add: ftu_def,
metis (mono_tags, lifting) case_prod_conv someI_ex›)+
from "**" have ‹set (seqRun t x i) ⊆ set t ∪ ev ` A› for i
by (auto simp add: seqRun_def)
have ‹set (ft i) ∪ set (fu i) ⊆ set t ∪ ev ` A› for i
by (rule subset_trans[OF interleave_set[OF "****"(3)]])
(fact ‹set (seqRun t x i) ⊆ set t ∪ ev ` A›)
have ‹inj ftu›
proof (rule injI)
fix i j assume ‹ftu i = ftu j›
obtain t' u' where ‹(t', u') = ftu i› by (metis surj_pair)
with ‹ftu i = ftu j› have ‹seqRun t x i setinterleaves ((t', u'), ?tick_S)›
‹seqRun t x j setinterleaves ((t', u'), ?tick_S)›
by (metis "****"(3) fst_conv ft_def fu_def snd_conv)+
from interleave_eq_size[OF this] have ‹length (seqRun t x i) = length (seqRun t x j)› .
thus ‹i = j› by simp
qed
hence ‹infinite (range ftu)› using finite_imageD by blast
moreover have ‹range ftu ⊆ range ft × range fu›
by (clarify, metis fst_conv ft_def fu_def rangeI snd_conv)
ultimately have ‹infinite (range ft) ∨ infinite (range fu)›
by (meson finite_SigmaI infinite_super)
{ fix ft fu P Q
assume assms : ‹infinite (range ft)›
‹∧i. set (ft i) ∪ set (fu i) ⊆ set t ∪ ev ` A›
‹∧i. ft i ∈ T P› ‹∧i. fu i ∈ T Q›
‹∧i. seqRun t x i setinterleaves ((ft i, fu i), ?tick_S)›
have ‹finite {t. ∃t'∈range ft. t = take i t'}› for i
proof (rule finite_subset)
show ‹ {w. ∃t'∈range ft. w = take i t'}
⊆ {w. set w ⊆ set t ∪ ev ` A ∧ length w ≤ i}›
by auto (meson Un_iff assms(2) in_set_takeD subsetD)
next
show ‹finite {w. set w ⊆ set t ∪ ev ` A ∧ length w ≤ i}›
by (rule finite_lists_length_le) (simp add: ‹finite A›)
― ‹Here we use the assumption @{thm ‹finite A›}.›
qed
with assms(1) obtain ft' :: ‹nat → _›
where $ : ‹strict_mono ft'› ‹range ft' ⊆ {w. ∃t'∈range ft. w ≤ t'}›
using KoenigLemma by blast
from "$"(2) assms(3) is_processT3_TR have ‹range ft' ⊆ T P› by blast
define ft'' where ‹ft'' i ≡ ft' (i + length t)› for i
from ‹range ft' ⊆ T P› have ‹range ft'' ⊆ T P› and ‹strict_mono ft''›
by (auto simp add: ft''_def "$"(1) strict_monoD strict_monoI)
have $$ : ‹?trH_A (ft'' i) = ?trH_A (ft'' 0)› for i
proof -
have ‹length t ≤ length (ft'' 0)›
by (metis "$"(1) add_0 add_leD1 ft''_def length_strict_mono)
obtain t' where ‹ft'' i = ft'' 0 @ t'›
by (meson prefixE ‹strict_mono ft''› strict_mono_less_eq zero_order(1))
moreover from "$"(2) obtain j where ‹ft'' i ≤ ft j› by (auto simp add: ft''_def)
ultimately obtain t'' where ‹ft j = ft'' 0 @ t' @ t''› by (metis prefixE append.assoc)
have ‹set (t' @ t'') ⊆ set (drop (length t) (seqRun t x j))›
proof (rule subset_trans)
show ‹set (t' @ t'') ⊆ set (drop (length (ft'' 0)) (seqRun t x j))›
by (rule interleave_order, fold ‹ft j = ft'' 0 @ t' @ t''›, fact assms(5))
next
show ‹set (drop (length (ft'' 0)) (seqRun t x j)) ⊆ set (drop (length t) (seqRun t x j))›
by (simp add: ‹length t ≤ length (ft'' 0)› set_drop_subset_set_drop)
qed
also from "**" have ‹set (drop (length t) (seqRun t x j)) ⊆ ev ` A›
by (auto simp add: seqRun_def)
finally show ‹?trH_A (ft'' i) = ?trH_A (ft'' 0)›
by (simp add: ‹ft'' i = ft'' 0 @ t'› subset_iff)
qed
from "$"(2) obtain i where ‹ft'' 0 ≤ ft i› by (auto simp add: ft''_def)
with prefixE obtain v where ‹ft i = ft'' 0 @ v› by blast
have ‹ftF u› by (fact "*"(1))
moreover have ‹tF (?trH_A (seqRun t x i)) ∨ u = []›
by (metis "*"(2) "**" Hiding_tickFree trace_hide_seqRun_eq_iff)
moreover have ‹s = ?trH_A (seqRun t x i) @ u›
by (metis "*"(3) "**" trace_hide_seqRun_eq_iff)
moreover have ‹?trH_A (seqRun t x i) setinterleaves ((?trH_A (ft i), ?trH_A (fu i)), ?tick_S)›
using assms(5) Hiding_interleave by blast
moreover have ‹?trH_A (ft i) ∈ D (P \ A)›
apply (unfold D_Hiding, clarify)
apply (rule exI[of _ ‹ft'' 0›])
apply (rule exI[of _ ‹?trH_A v›])
apply (intro conjI)
subgoal by (metis assms(3) Hiding_front_tickFree ‹ft i = ft'' 0 @ v›
front_tickFree_Nil front_tickFree_nonempty_append_imp is_processT2_TR)
subgoal by (metis strict_prefixE' T_imp_front_tickFree ‹range ft'' ⊆ T P› ‹strict_mono ft''›
front_tickFree_append_iff list.distinct(1) range_subsetD strict_mono_Suc_iff)
subgoal by (simp add: ‹ft i = ft'' 0 @ v›)
subgoal using "$$" ‹range ft'' ⊆ T P› ‹strict_mono ft''› by blast .
moreover have ‹?trH_A (fu i) ∈ T (Q \ A)›
proof (cases ‹∃t'. ?trH_A t' = ?trH_A (fu i) ∧ (t', ev ` A) ∈ F Q›)
assume ‹∃t'. ?trH_A t' = ?trH_A (fu i) ∧ (t', ev ` A) ∈ F Q›
then obtain t' where ‹?trH_A (fu i) = ?trH_A t'› ‹(t', ev ` A) ∈ F Q› by metis
thus ‹?trH_A (fu i) ∈ T (Q \ A)› unfolding T_Hiding by blast
next
assume ‹∄t'. ?trH_A t' = ?trH_A (fu i) ∧ (t', ev ` A) ∈ F Q›
with assms(4) inf_hidden obtain fu' j
where $$$ : ‹isInfHiddenRun fu' Q A› ‹fu i = fu' j› by blast
show ‹?trH_A (fu i) ∈ T (Q \ A)›
apply (unfold T_Hiding, simp)
apply (rule disjI2)
apply (rule exI[of _ ‹fu' j›], rule exI[of _ ‹[]›])
apply (intro conjI)
subgoal by simp
subgoal by (metis "$$$"(1) strict_prefixE' T_imp_front_tickFree neq_Nil_conv
front_tickFree_nonempty_append_imp strict_mono_Suc_iff)
subgoal by (simp add: "$$$"(2))
subgoal using "$$$"(1) by blast .
qed
ultimately have ‹s ∈ D ((P \ A) [S] (Q \ A))› unfolding D_Sync by blast
} note $ = this
from ‹infinite (range ft) ∨ infinite (range fu)›
show ‹s ∈ D ((P \ A) [S] (Q \ A))›
proof (elim disjE)
from "$" "****" ‹∧i. set (ft i) ∪ set (fu i) ⊆ set t ∪ ev ` A›
show ‹infinite (range ft) ==> s ∈ D ((P \ A) [S] (Q \ A))› by blast
next
from "$" "****" ‹∧i. set (ft i) ∪ set (fu i) ⊆ set t ∪ ev ` A›
show ‹infinite (range fu) ==> s ∈ D ((P \ A) [S] (Q \ A))›
by (metis Sync_commute setinterleaving_sym sup_commute)
qed
qed
next
let ?trH_A = ‹λt. trace_hide t (ev ` A)› and ?tick_S = ‹range tick ∪ ev ` S›
assume same_div : ‹D (P [S] Q \ A) = D ((P \ A) [S] (Q \ A))›
fix s X assume ‹(s, X) ∈ F (P [S] Q \ A)›
then consider ‹s ∈ D (P [S] Q \ A)›
| t where ‹s = trace_hide t (ev ` A)› ‹(t, X ∪ ev ` A) ∈ F (P [S] Q)›
unfolding F_Hiding D_Hiding by blast
thus ‹(s, X) ∈ F ((P \ A) [S] (Q \ A))›
proof cases
from same_div D_F show ‹s ∈ D (P [S] Q \ A) ==> (s, X) ∈ F ((P \ A) [S] (Q \ A))› by blast
next
fix t assume * : ‹s = ?trH_A t› ‹(t, X ∪ ev ` A) ∈ F (P [S] Q)›
then consider ‹t ∈ D (P [S] Q)›
| (F) t_P X_P t_Q X_Q
where ‹(t_P, X_P) ∈ F P› ‹(t_Q, X_Q) ∈ F Q›
‹t setinterleaves ((t_P, t_Q), ?tick_S)›
‹X ∪ ev ` A = (X_P ∪ X_Q) ∩ ?tick_S ∪ X_P ∩ X_Q›
by (auto simp add: F_Sync D_Sync)
thus ‹(s, X) ∈ F ((P \ A) [S] (Q \ A))›
proof cases
assume ‹t ∈ D (P [S] Q)›
with "*"(1) mem_D_imp_mem_D_Hiding have ‹s ∈ D (P [S] Q \ A)› by blast
with same_div D_F show ‹(s, X) ∈ F ((P \ A) [S] (Q \ A))› by blast
next
case F
from inf_hidden[OF _ F(1)[THEN F_T], of A] inf_hidden[OF _ F(2)[THEN F_T], of A]
consider (D_P) f_P where ‹isInfHiddenRun f_P P A› ‹t_P ∈ range f_P›
| (D_Q) f_Q where ‹isInfHiddenRun f_Q Q A› ‹t_Q ∈ range f_Q›
| (F_both) t_P' t_Q'
where ‹?trH_A t_P' = ?trH_A t_P› ‹(t_P', ev ` A) ∈ F P›
‹?trH_A t_Q' = ?trH_A t_Q› ‹(t_Q', ev ` A) ∈ F Q›
by blast
thus ‹(s, X) ∈ F ((P \ A) [S] (Q \ A))›
proof cases
case D_P
have $ : ‹?trH_A t_P ∈ D (P \ A)›
apply (unfold D_Hiding, clarify)
apply (rule exI[of _ ‹t_P›], rule exI[of _ ‹[]›])
using tickFree_isInfHiddenRun D_P front_tickFree_Nil by blast
from F(2) F_T mem_T_imp_mem_T_Hiding
have $$ : ‹?trH_A t_Q ∈ T (Q \ A)› by blast
show ‹(s, X) ∈ F ((P \ A) [S] (Q \ A))›
apply (simp add: F_Sync)
apply (rule disjI2)
apply (rule exI[of _ ‹?trH_A t_P›])
apply (rule exI[of _ ‹?trH_A t_Q›])
apply (rule exI[of _ ‹?trH_A t›], rule exI[of _ ‹[]›])
by (simp add: "*"(1) F(3) Hiding_interleave "$" "$$")
next
case D_Q
from F(1) F_T mem_T_imp_mem_T_Hiding
have $ : ‹?trH_A t_P∈ T (P \ A)› by blast
have $$ : ‹?trH_A t_Q ∈ D (Q \ A)›
apply (unfold D_Hiding, clarify)
apply (rule exI[of _ ‹t_Q›], rule exI[of _ ‹[]›])
using tickFree_isInfHiddenRun D_Q front_tickFree_Nil by blast
show ‹(s, X) ∈ F ((P \ A) [S] (Q \ A))›
apply (simp add: F_Sync)
apply (rule disjI2)
apply (rule exI[of _ ‹?trH_A t_Q›])
apply (rule exI[of _ ‹?trH_A t_P›])
apply (rule exI[of _ ‹?trH_A t›], rule exI[of _ ‹[]›])
by (simp add: "*"(1) F(3) Hiding_interleave setinterleaving_sym "$" "$$")
next
case F_both
from F(4) ‹A ∩ S = {}› have ‹ev ` A ⊆ X_P› and ‹ev ` A ⊆ X_Q› by auto
have ‹(?trH_A t_P, X_P) ∈ F (P \ A)›
by (simp add: F_Hiding) (metis F(1) F_both(1) ‹ev ` A ⊆ X_P› sup.orderE)
moreover have ‹(?trH_A t_Q, X_Q) ∈ F (Q \ A)›
by (simp add: F_Hiding) (metis F(2) F_both(3) ‹ev ` A ⊆ X_Q› sup.orderE)
moreover from F(3) Hiding_interleave
have ‹s setinterleaves ((?trH_A t_P, ?trH_A t_Q), ?tick_S)›
unfolding "*"(1) by blast
ultimately have ‹(s, (X_P ∪ X_Q) ∩ ?tick_S ∪ X_P ∩ X_Q) ∈ F ((P \ A) [S] (Q \ A))›
unfolding F_Sync by blast
moreover from F(4) have ‹X ⊆ (X_P ∪ X_Q) ∩ ?tick_S ∪ X_P ∩ X_Q› by blast
ultimately show ‹(s, X) ∈ F ((P \ A) [S] (Q \ A))› by (fact is_processT4)
qed
qed
qed
next
let ?trH_A = ‹λt. trace_hide t (ev ` A)› and ?tick_S = ‹range tick ∪ ev ` S›
fix s assume ‹s ∈ D ((P \ A) [S] (Q \ A))›
then obtain t_P t_Q r v
where * : ‹ftF v› ‹tF r ∨ v = []› ‹s = r @ v› ‹r setinterleaves ((t_P, t_Q), ?tick_S)›
‹t_P ∈ D (P \ A) ∧ t_Q ∈ T (Q \ A) ∨ t_P ∈ D (Q \ A) ∧ t_Q ∈ T (P \ A)›
unfolding D_Sync by blast
from ‹s ∈ D ((P \ A) [S] (Q \ A))› have ‹ftF s›
by (simp add: D_imp_front_tickFree)
{ fix t_P t_Q and P Q
assume ** : ‹r setinterleaves ((t_P, t_Q), ?tick_S)›
‹t_P ∈ D (P \ A)› ‹t_Q ∈ T (Q \ A)›
from **(2) obtain t u
where *** : ‹ftF u› ‹tF t› ‹t_P = ?trH_A t @ u›
‹t ∈ D P ∨ (∃x. isInfHidden_seqRun_strong x P A t)›
by (elim D_Hiding_seqRunE)
from interleave_append_left[OF "**"(1)[unfolded "***"(3)]]
obtain t_Q1 t_Q2 r1 r2
where **** : ‹t_Q = t_Q1 @ t_Q2› ‹r = r1 @ r2›
‹r1 setinterleaves ((?trH_A t, t_Q1), ?tick_S)›
‹r2 setinterleaves ((u, t_Q2), ?tick_S)› by blast
from "**"(3) consider t_Q' where ‹t_Q = ?trH_A t_Q'› ‹(t_Q', ev ` A) ∈ F Q›
| (D_Q) t' u' where ‹ftF u'› ‹tF t'› ‹t_Q = ?trH_A t' @ u'›
‹t' ∈ D Q ∨ (∃y. isInfHidden_seqRun_strong y Q A t')›
by (elim T_Hiding_seqRunE)
hence ‹s ∈ D (P [S] Q \ A)›
proof cases
fix t_Q' assume ‹t_Q = ?trH_A t_Q'› ‹(t_Q', ev ` A) ∈ F Q›
from trace_hide_append[OF this(1)[unfolded "****"(1)]]
obtain t_Q1' t_Q2' where $ : ‹t_Q' = t_Q1' @ t_Q2'› ‹t_Q1 = ?trH_A t_Q1'›
‹t_Q2 = ?trH_A t_Q2'› by blast
from ‹A ∩ S = {}› have ‹ev ` A ∩ ?tick_S = {}› by blast
from interleave_Hiding[OF this "****"(3)[unfolded "$"(2)]]
obtain r1' where $$ : ‹r1 = ?trH_A r1'›
‹r1' setinterleaves ((t, t_Q1'), ?tick_S)› by blast
show ‹s ∈ D (P [S] Q \ A)›
proof (rule D_Hiding_seqRunI)
show ‹ftF (r2 @ v)›
by (metis "*"(1, 3) "****"(2) ‹ftF s›
front_tickFree_append_iff tickFree_append_iff)
next
show ‹tF r1'›
by (metis "$"(1) "$$"(2) "***"(2) F_imp_front_tickFree SyncWithTick_imp_NTF
‹(t_Q', ev ` A) ∈ F Q› front_tickFree_dw_closed nonTickFree_n_frontTickFree
non_tickFree_tick tickFree_append_iff ftf_Sync tickFree_imp_front_tickFree)
next
from "$$"(1) "*"(3) "****"(2) append.assoc
show ‹s = ?trH_A r1' @ r2 @ v› by blast
next
from "***"(4) show ‹r1' ∈ D (P [S] Q) ∨
(∃x. ∀i. seqRun r1' x i ∈ T (P [S] Q) ∧ x i ∈ ev ` A)›
proof (elim disjE exE)
assume ‹t ∈ D P›
moreover have ‹t_Q1' ∈ T Q›
by (metis "$"(1) F_T prefixI ‹(t_Q', ev ` A) ∈ F Q› is_processT3_TR)
ultimately have ‹r1' ∈ D (P [S] Q)›
unfolding D_Sync using "$$"(2) front_tickFree_Nil by blast
thus ‹r1' ∈ D (P [S] Q) ∨ (∃x. isInfHidden_seqRun x (P [S] Q) A r1')› ..
next
fix x assume "£" : ‹isInfHidden_seqRun_strong x P A t›
from "£" ‹A ∩ S = {}› have ‹set (map x [0..<i]) ∩ ?tick_S = {}› for i
by (simp add: disjoint_iff image_iff)
(metis eventptick.distinct(1) eventptick.inject(1))
from "$$"(2)[THEN interleave_append_tail_left, OF this, folded seqRun_def]
have "££" : ‹seqRun r1' x i setinterleaves ((seqRun t x i, t_Q1'), ?tick_S)› for i .
have ‹isInfHidden_seqRun x (P [S] Q) A r1'›
proof (intro allI conjI)
have ‹t_Q1' ∈ T Q›
by (metis "$"(1) F_T prefixI ‹(t_Q', ev ` A) ∈ F Q› is_processT3_TR)
with "£" "££" show ‹seqRun r1' x i ∈ T (P [S] Q)› for i
unfolding T_Sync by blast
next
show ‹x i ∈ ev ` A› for i by (simp add: "£")
qed
thus ‹r1' ∈ D (P [S] Q) ∨ (∃x. isInfHidden_seqRun x (P [S] Q) A r1')› by blast
qed
qed
next
case D_Q
have ‹t ∈ T P› using "***"(4) D_T by (metis seqRun_0)
consider ‹?trH_A t' ≤ t_Q1› | ‹t_Q1 ≤ ?trH_A t'›
by (metis "****"(1) D_Q(3) prefixI dual_order.eq_iff le_same_imp_eq_or_less nless_le)
thus ‹s ∈ D (P [S] Q \ A)›
proof cases
assume ‹?trH_A t' ≤ t_Q1›
from interleave_le_right[OF "****"(3) this]
obtain r1_bis t_hidden_bis
where ‹r1_bis ≤ r1› ‹t_hidden_bis ≤ ?trH_A t›
‹r1_bis setinterleaves ((t_hidden_bis, ?trH_A t'), ?tick_S)› by blast
moreover from le_trace_hide[OF ‹t_hidden_bis ≤ ?trH_A t›]
obtain t_bis where ‹t_hidden_bis = ?trH_A t_bis ∧ t_bis ≤ t› ..
ultimately have $ : ‹r1_bis ≤ r1› ‹t_bis ≤ t›
‹r1_bis setinterleaves ((?trH_A t_bis, ?trH_A t'), ?tick_S)› by blast+
from interleave_Hiding[OF _ "$"(3)] ‹A ∩ S = {}›
obtain r1_bis_unhidden
where $$ : ‹r1_bis = ?trH_A r1_bis_unhidden›
‹r1_bis_unhidden setinterleaves ((t_bis, t'), ?tick_S)› by blast
from "$"(2) ‹t ∈ T P› is_processT3_TR have ‹t_bis ∈ T P› by blast
from D_Q(4) have ‹r1_bis ∈ D (P [S] Q \ A)›
proof (elim disjE exE)
assume ‹t' ∈ D Q›
with "$$"(2) ‹t_bis ∈ T P› have ‹r1_bis_unhidden ∈ D (P [S] Q)›
by (simp add: D_Sync)
(use front_tickFree_Nil setinterleaving_sym in blast)
with "$$"(1) mem_D_imp_mem_D_Hiding show ‹r1_bis ∈ D (P [S] Q \ A)› by blast
next
fix y assume £ : ‹isInfHidden_seqRun_strong y Q A t'›
(* with exists_suff obtain g_suff
where g_suff_props : \<open>g i = g 0 @ g_suff i\<close> \<open>set (g_suff i) \<subseteq> ev ` A\<close>
\<open>set (g_suff i) \<inter> ?tick_S = {}\<close> \<open>strict_mono g_suff\<close> for i by metis *)
from "£" ‹A ∩ S = {}› have ‹set (map y [0..<i]) ∩ ?tick_S = {}› for i
by (simp add: disjoint_iff image_iff)
(metis eventptick.distinct(1) eventptick.inject(1))
from "$$"(2)[THEN interleave_append_tail_right, OF this, folded seqRun_def]
have $$$ : ‹seqRun r1_bis_unhidden y i setinterleaves ((t_bis, seqRun t' y i), ?tick_S)› for i .
have $$$$ : ‹isInfHidden_seqRun y (P [S] Q) A r1_bis_unhidden›
proof (intro allI conjI)
from "$$$" "£" ‹t_bis ∈ T P›
show ‹seqRun r1_bis_unhidden y i ∈ T (P [S] Q)› for i
unfolding T_Sync by blast
next
show ‹y i ∈ ev ` A› for i by (simp add: "£")
qed
show ‹r1_bis ∈ D (P [S] Q \ A)›
proof (rule D_Hiding_seqRunI)
show ‹ftF []› by simp
next
show ‹tF r1_bis_unhidden›
by (metis "$$"(2) D_Q(2) SyncWithTick_imp_NTF T_imp_front_tickFree ‹t_bis ∈ T P›
ftf_Sync nonTickFree_n_frontTickFree non_tickFree_tick
tickFree_append_iff tickFree_imp_front_tickFree)
next
show ‹r1_bis = ?trH_A r1_bis_unhidden @ []› by (simp add: $$(1))
next
from "$$$$" show ‹r1_bis_unhidden ∈ D (P [S] Q) ∨
(∃x. isInfHidden_seqRun x (P [S] Q) A r1_bis_unhidden)› by blast
qed
qed
with "$"(1) show ‹s ∈ D (P [S] Q \ A)›
unfolding less_eq_list_def prefix_def
by (metis (no_types, opaque_lifting) "*"(3) "****"(2) ‹ftF s›
append_Nil2 front_tickFree_append_iff front_tickFree_dw_closed is_processT7)
next
assume ‹t_Q1 ≤ ?trH_A t'›
from le_trace_hide[OF this] obtain t_Q1_unhidden
where $ : ‹t_Q1 = ?trH_A t_Q1_unhidden› ‹t_Q1_unhidden ≤ t'› by blast
from ‹A ∩ S = {}› have ‹ev ` A ∩ ?tick_S = {}› by blast
from "****"(3)[unfolded "$"(1)]
have ‹r1 setinterleaves ((?trH_A t, ?trH_A t_Q1_unhidden), ?tick_S)› .
from interleave_Hiding[OF ‹ev ` A ∩ ?tick_S = {}› this]
obtain r1_unhidden
where $$ : ‹r1 = ?trH_A r1_unhidden›
‹r1_unhidden setinterleaves ((t, t_Q1_unhidden), ?tick_S)› by blast
from ‹t_Q1_unhidden ≤ t'› have ‹t_Q1_unhidden ∈ T Q›
by (metis D_Q(4) D_T is_processT3_TR t_le_seqRun)
from "***"(4) have ‹r1 ∈ D (P [S] Q \ A)›
proof (elim disjE exE)
assume ‹t ∈ D P›
have ‹r1_unhidden ∈ D (P [S] Q)›
proof (unfold D_Sync, clarify, intro exI conjI)
show ‹ftF []› ‹tF r1_unhidden ∨ [] = []›
‹r1_unhidden = r1_unhidden @ []› by simp_all
next
show ‹r1_unhidden setinterleaves ((t, t_Q1_unhidden), ?tick_S)› by (fact "$$"(2))
next
show ‹t ∈ D P ∧ t_Q1_unhidden ∈ T Q ∨ t ∈ D Q ∧ t_Q1_unhidden ∈ T P›
by (simp add: ‹t ∈ D P› ‹t_Q1_unhidden ∈ T Q›)
qed
thus ‹r1 ∈ D (P [S] Q \ A)› unfolding "$$"(1) by (fact mem_D_imp_mem_D_Hiding)
next
fix x assume £ : ‹isInfHidden_seqRun_strong x P A t›
from "£" ‹A ∩ S = {}› have ‹set (map x [0..<i]) ∩ ?tick_S = {}› for i
by (simp add: disjoint_iff image_iff)
(metis eventptick.distinct(1) eventptick.inject(1))
from "$$"(2)[THEN interleave_append_tail_left, OF this, folded seqRun_def]
have "££" : ‹seqRun r1_unhidden x i setinterleaves ((seqRun t x i, t_Q1_unhidden), ?tick_S)› for i .
have "£££" : ‹isInfHidden_seqRun x (P [S] Q) A r1_unhidden›
proof (intro allI conjI)
from "£" "££" ‹t_Q1_unhidden ∈ T Q›
show ‹seqRun r1_unhidden x i ∈ T (P [S] Q)› for i unfolding T_Sync by blast
next
from "£" show ‹x i ∈ ev ` A› for i by blast
qed
show ‹r1 ∈ D (P [S] Q \ A)›
proof (unfold D_Hiding_seqRun, clarify, intro exI conjI)
show ‹ftF []› by simp
next
from isInfHidden_seqRun_imp_tickFree[OF "£££"] show ‹tF r1_unhidden› .
next
show ‹r1 = ?trH_A r1_unhidden @ []› by (simp add: "$$"(1))
next
from "£££" show ‹r1_unhidden ∈ D (P [S] Q) ∨
(∃x. isInfHidden_seqRun x (P [S] Q) A r1_unhidden)› by blast
qed
qed
thus ‹s ∈ D (P [S] Q \ A)›
by (metis "*"(3) "****"(2) ‹ftF s› append.right_neutral
front_tickFree_append_iff front_tickFree_dw_closed is_processT7)
qed
qed
} note $ = this
from "*"(5) show ‹s ∈ D (P [S] Q \ A)›
by (elim disjE conjE) (metis "$" "*"(4), metis "$" "*"(4) Sync_commute)
next
let ?trH_A = ‹λt. trace_hide t (ev ` A)› and ?tick_S = ‹range tick ∪ ev ` S›
assume same_div : ‹D (P [S] Q \ A) = D ((P \ A) [S] (Q \ A))›
fix s X assume ‹(s, X) ∈ F ((P \ A) [S] (Q \ A))›
then consider ‹s ∈ D ((P \ A) [S] (Q \ A))›
| (F) s_P X_P s_Q X_Q
where ‹(s_P, X_P) ∈ F (P \ A)› ‹(s_Q, X_Q) ∈ F (Q \ A)›
‹s setinterleaves ((s_P, s_Q), ?tick_S)›
‹X = (X_P ∪ X_Q) ∩ ?tick_S ∪ X_P ∩ X_Q›
unfolding F_Sync D_Sync by blast
thus ‹(s, X) ∈ F (P [S] Q \ A)›
proof cases
from same_div D_F show ‹s ∈ D ((P \ A) [S] (Q \ A)) ==> (s, X) ∈ F (P [S] Q \ A)› by blast
next
case F
from F(1, 2) consider ‹s_P ∈ D (P \ A)› | ‹s_Q ∈ D (Q \ A)›
| (F_both) s_P' s_Q'
where ‹s_P = ?trH_A s_P'› ‹(s_P', X_P ∪ ev ` A) ∈ F P›
‹s_Q = ?trH_A s_Q'› ‹(s_Q', X_Q ∪ ev ` A) ∈ F Q›
unfolding F_Hiding D_Hiding by blast
thus ‹(s, X) ∈ F (P [S] Q \ A)›
proof cases
assume ‹s_P ∈ D (P \ A)›
moreover from F(2) F_T have ‹s_Q ∈ T (Q \ A)› by blast
ultimately have ‹s ∈ D ((P \ A) [S] (Q \ A))›
using F(3) front_tickFree_Nil unfolding D_Sync by blast
with same_div D_F show ‹(s, X) ∈ F (P [S] Q \ A)› by blast
next
from F(1) F_T have ‹s_P ∈ T (P \ A)› by blast
moreover assume ‹s_Q ∈ D (Q \ A)›
moreover have ‹s setinterleaves ((s_Q, s_P), range tick ∪ ev ` S)›
by (simp add: F(3) setinterleaving_sym)
ultimately have ‹s ∈ D ((P \ A) [S] (Q \ A))›
using front_tickFree_Nil unfolding D_Sync by blast
with same_div D_F show ‹(s, X) ∈ F (P [S] Q \ A)› by blast
next
case F_both
from ‹A ∩ S = {}› have ‹ev ` A ∩ (range tick ∪ ev ` S) = {}› by blast
from interleave_Hiding[OF this F(3)[unfolded F_both(1, 3)]]
obtain s' where * : ‹s = ?trH_A s'›
‹s' setinterleaves ((s_P', s_Q'), range tick ∪ ev ` S)› by blast
have ‹X ∪ ev ` A = (X_P ∪ ev ` A ∪ (X_Q ∪ ev ` A)) ∩ (range tick ∪ ev ` S)
∪ (X_P ∪ ev ` A) ∩ (X_Q ∪ ev ` A)›
by (simp add: F(4) Un_Int_distrib2 Un_assoc sup_left_commute)
thus ‹(s, X) ∈ F (P [S] Q \ A)›
by (simp add: "*"(1) F_Hiding F_Sync) (use "*"(2) F_both(2, 4) in blast)
qed
qed
qed
(* TODO: do we need this ? *)
(* Trivial results have been removed *)
(*
lemmas Par_SKIP_SKIP = SKIP_Sync_SKIP[where S = \<open>UNIV\<close>]
and Par_SKIP_STOP = SKIP_Sync_STOP[where S = \<open>UNIV\<close>]
and Par_commute = Sync_commute[where S = \<open>UNIV\<close>]
and Par_assoc = Sync_assoc[where S = \<open>UNIV\<close>]
and Mprefix_Par_SKIP = Mprefix_Sync_SKIP[where S = \<open>UNIV\<close>, simplified]
and prefix_Par_SKIP = prefix_Sync_SKIP[where S = \<open>UNIV\<close>, simplified]
and prefix_Par1 = prefix_Sync1[where S = \<open>UNIV\<close>, simplified]
and prefix_Par2 = prefix_Sync2[where S = \<open>UNIV\<close>, simplified]
and Mprefix_Par_distr = Mprefix_Sync_Mprefix_subset[where S = \<open>UNIV\<close>, simplified]
and Inter_SKIP_SKIP = SKIP_Sync_SKIP[where S = \<open>{}\<close>]
and Inter_SKIP_STOP = SKIP_Sync_STOP[where S = \<open>{}\<close>]
and Inter_commute = Sync_commute[where S = \<open>{}\<close>]
and Inter_assoc = Sync_assoc[where S = \<open>{}\<close>]
and Mprefix_Inter_SKIP = Mprefix_Sync_SKIP[where S = \<open>{}\<close>, simplified]
and prefix_Inter_SKIP = prefix_Sync_SKIP[where S = \<open>{}\<close>, simplified]
(* and Hiding_Inter = Hiding_Sync[where S = \<open>{}\<close>, simplified] *)
and Mprefix_Inter_distr = Mprefix_Sync_Mprefix_indep[where S = ‹{}›, simplified]
and prefix_Inter = Mprefix_Sync_Mprefix_indep[of ‹{a}› ‹{}› ‹{b}› ‹λx. P› ‹λx. Q›,
simplified, folded write0_def] for a P b Q
*)
subsection ‹Renaming Operator Laws›
lemma Renaming_Ndet: ‹Renaming (P ⊓ Q) f g = Renaming P f g ⊓ Renaming Q f g›
by (subst Process_eq_spec) (auto simp add: F_Renaming D_Renaming F_Ndet D_Ndet)
lemma Renaming_Det: ‹Renaming (P ◻ Q) f g = Renaming P f g ◻ Renaming Q f g›
proof (subst Process_eq_spec, safe)
show ‹(s, X) ∈ F (Renaming (P ◻ Q) f g) ==>
(s, X) ∈ F (Renaming P f g ◻ Renaming Q f g)› for s X
by (cases s) (auto simp add: F_Renaming F_Det D_Renaming D_Det T_Renaming)+
next
fix s X assume ‹(s, X) ∈ F (Renaming P f g ◻ Renaming Q f g)›
then consider ‹s = []› ‹(s, X) ∈ F (Renaming P f g)› ‹(s, X) ∈ F (Renaming Q f g)›
| e s' where ‹s = e # s'› ‹(s, X) ∈ F (Renaming P f g) ∨ (s, X) ∈ F (Renaming Q f g)›
| ‹s = []› ‹s ∈ D (Renaming P f g) ∨ s ∈ D (Renaming Q f g)›
| r where ‹s = []› ‹🚫(r) ∉ X› ‹([🚫(r)] ∈ T (Renaming P f g) ∨ [🚫(r)] ∈ T (Renaming Q f g))›
by (cases s) (auto simp add: F_Det)
thus ‹(s, X) ∈ F (Renaming (P ◻ Q) f g)›
proof cases
show ‹[s = []; (s, X) ∈ F (Renaming P f g); (s, X) ∈ F (Renaming Q f g)]
==> (s, X) ∈ F (Renaming (P ◻ Q) f g)›
by (auto simp add: F_Renaming F_Det)
next
show ‹s = e # s' ==> (s, X) ∈ F (Renaming P f g) ∨ (s, X) ∈ F (Renaming Q f g)
==> (s, X) ∈ F (Renaming (P ◻ Q) f g)› for s' e
by (simp add: F_Renaming F_Det D_Det, safe)
(metis list.distinct(1) list.simps(9), presburger)+
next
show ‹s = [] ==> s ∈ D (Renaming P f g) ∨ s ∈ D (Renaming Q f g)
==> (s, X) ∈ F (Renaming (P ◻ Q) f g)›
by (simp add: D_Renaming F_Renaming D_Det)
next
show ‹[s = []; 🚫(r) ∉ X; [🚫(r)] ∈ T (Renaming P f g) ∨ [🚫(r)] ∈ T (Renaming Q f g)]
==> (s, X) ∈ F (Renaming (P ◻ Q) f g)› for r
by (auto simp add: T_Renaming F_Renaming D_Det F_Det
dest: map_eventptick_eq_tick_iff[THEN iffD1, OF sym, of r])
(metis append_eq_Cons_conv list.map_disc_iff map_eventptick_tickFree
non_tickFree_tick tickFree_Nil tickFree_append_iff)+
qed
next
show ‹s ∈ D (Renaming (P ◻ Q) f g) ==> s ∈ D (Renaming P f g ◻ Renaming Q f g)›
and ‹s ∈ D (Renaming P f g ◻ Renaming Q f g) ==> s ∈ D (Renaming (P ◻ Q) f g)› for s
by (auto simp add: D_Renaming D_Det)
qed
lemma Sliding_STOP_Det [simp] : ‹(P ⊳ STOP) ◻ Q = P ⊳ Q›
by (simp add: Det_commute Det_distrib_Ndet_left Sliding_def)
lemma Sliding_Det: ‹(P ⊳ P') ◻ Q = P ⊳ P' ◻ Q›
by (metis Det_assoc Sliding_STOP_Det)
lemma Renaming_Sliding:
‹Renaming (P ⊳ Q) f g = Renaming P f g ⊳ Renaming Q f g›
by (simp add: Renaming_Det Renaming_Ndet Sliding_def)
(* TODO: do we need the following versions ? *)
lemma Renaming_Mprefix_image:
‹Renaming (◻ a ∈ A → P (f a)) f g =
◻ b ∈ f ` A → Renaming (P b) f g› (is ‹?lhs = ?rhs›)
by (subst Renaming_Mprefix, rule mono_Mprefix_eq)
(simp add: Process_eq_spec F_GlobalNdet D_GlobalNdet F_Renaming D_Renaming, safe, auto)
lemma Renaming_Mprefix_image_inj_on:
‹Renaming (Mprefix A P) f g = ◻ b ∈ f ` A → Renaming (P (THE a. a ∈ A ∧ f a = b)) f g›
if inj_on_f: ‹inj_on f A›
apply (subst Renaming_Mprefix_image[symmetric])
apply (intro arg_cong[where f = ‹λQ. Renaming Q f g›] mono_Mprefix_eq)
by (metis that the_inv_into_def the_inv_into_f_f)
corollary Renaming_Mprefix_image_inj:
‹Renaming (Mprefix A P) f g = ◻ b ∈ f ` A → Renaming (P (THE a. f a = b)) f g› if inj_f: ‹inj f›
apply (subst Renaming_Mprefix_image_inj_on, metis inj_eq inj_onI that)
apply (rule mono_Mprefix_eq[rule_format])
by (metis imageE inj_eq[OF inj_f])
lemma Renaming_Mndetprefix_image: ‹Renaming (⊓ a ∈ A → P (f a)) f g = ⊓ b ∈ f ` A → Renaming (P b) f g›
by (auto simp add: Mndetprefix_GlobalNdet Renaming_distrib_GlobalNdet write0_def Renaming_Mprefix
intro!: mono_Mprefix_eq mono_GlobalNdet_eq2 intro: sym)
corollary Renaming_Mndetprefix_inj_on:
‹Renaming (Mndetprefix A P) f g = ⊓ b ∈ f ` A → Renaming (P (THE a. a ∈ A ∧ f a = b)) f g›
if inj_on_f: ‹inj_on f A›
apply (subst Renaming_Mndetprefix_image[symmetric])
apply (intro arg_cong[where f = ‹λQ. Renaming Q f g›] mono_Mndetprefix_eq)
by (metis that the_inv_into_def the_inv_into_f_f)
corollary Renaming_Mndetprefix_inj:
‹Renaming (Mndetprefix A P) f g = ⊓ b ∈ f ` A → Renaming (P (THE a. f a = b)) f g›
if inj_f: ‹inj f›
apply (subst Renaming_Mndetprefix_inj_on, metis inj_eq inj_onI that)
apply (rule mono_Mndetprefix_eq[rule_format])
by (metis imageE inj_eq[OF inj_f])
lemma Hiding_distrib_FD_GlobalNdet :
‹(⊓a ∈ A. P a) \ S ⊑FD ⊓a ∈ A. (P a \ S)› (is ‹?lhs ⊑FD ?rhs›)
proof (cases ‹A = {}›)
show ‹A = {} ==> ?lhs ⊑FD ?rhs› by simp
next
show ‹?lhs ⊑FD ?rhs› if ‹A ≠ {}›
proof (rule failure_divergence_refine_optimizedI)
show ‹s ∈ D ?rhs ==> s ∈ D ?lhs› for s
by (simp add: GlobalNdet_projs D_Hiding_seqRun) blast
next
assume subset_div : ‹D ?rhs ⊆ D ?lhs›
fix s X assume ‹(s, X) ∈ F ?rhs›
then obtain a where ‹a ∈ A› ‹(s, X) ∈ F (P a \ S)›
by (auto simp add: F_GlobalNdet ‹A ≠ {}›)
from ‹(s, X) ∈ F (P a \ S)› consider ‹s ∈ D (P a \ S)›
| t where ‹s = trace_hide t (ev ` S)› ‹(t, X ∪ ev ` S) ∈ F (P a)›
unfolding D_Hiding F_Hiding by blast
thus ‹(s, X) ∈ F ?lhs›
proof cases
assume ‹s ∈ D (P a \ S)›
with ‹a ∈ A› have ‹s ∈ D ?rhs› by (auto simp add: D_GlobalNdet)
with subset_div D_F show ‹(s, X) ∈ F ?lhs› by blast
next
from ‹a ∈ A› show ‹s = trace_hide t (ev ` S) ==> (t, X ∪ ev ` S) ∈ F (P a)
==> (s, X) ∈ F ?lhs› for t
by (simp add: F_Hiding_seqRun F_GlobalNdet) blast
qed
qed
qed
lemma Renaming_Seq :
‹Renaming (P ; Q) f g = Renaming P f g ; Renaming Q f g› (is ‹?lhs = ?rhs›)
proof (rule Process_eq_optimizedI)
fix t assume ‹t ∈ D ?lhs›
then obtain u v where ‹t = map (map_eventptick f g) u @ v› ‹tF u› ‹ftF v› ‹u ∈ D (P ; Q)›
unfolding D_Renaming by blast
from ‹u ∈ D (P ; Q)› consider ‹u ∈ D P›
| u1 u2 r where ‹u = u1 @ u2› ‹u1 @ [🚫(r)] ∈ T P› ‹u2 ∈ D Q›
unfolding D_Seq by blast
thus ‹t ∈ D ?rhs›
proof cases
from ‹ftF v› ‹t = map (map_eventptick f g) u @ v› ‹tF u›
show ‹u ∈ D P ==> t ∈ D ?rhs› by (auto simp add: D_Seq D_Renaming)
next
fix u1 u2 r assume ‹u = u1 @ u2› ‹u1 @ [🚫
u1 @ [🚫np i)"
by (and "s1 <>itns' \zeta>
moreover from ‹u2 ∈ D Q› ‹tF u› ‹u = u1 @ u2›
have ‹map (map_event "(ns,, con(i, i'), ns')\i>trans (pnet np ⟨i⟩)"
by (simp add: D_Renaming) (use front_tickFree_Nil in blast)
_eventtc Dr›u = u1 @ u2› D_Seq
<t ∈ D ?rhs› by (simp add: ‹t = map (map_eventptick f g) u @ v› ‹ftF v›
\<open>tF u\<close> is_processT7 map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k_tickFree)
qed
next
fix t assume \<open>t \<in> \<D> ?rhs\<close>
thm this[simplified D_Seq, simplified]
then consider \<open>t \<in> \<D> (Renaming P f g)\<close>
| t1 t2 s where \<open>t = t1 @ t2\<close> \<open>t1 @ [\<checkmark>(s)] \<in> \<T> (Renaming P f g)\<close>
\<open>t1 @ [\<checkmark>(s)] \<notin> \<D> (Renaming P f g)\<close> \<open>t2 \<in> \<D> (Renaming Q f g)\<close>
by (simp add: D_Seq) (metis D_imp_front_tickFree append_T_imp_tickFree
is_processT7 is_processT9 list.distinct(1))
thus \<open>t \<in> \<D> ?lhs\<close>
proof cases
show \<open>t \<in> \<D> (Renaming P f g) \<Longrightarrow> t \<in> \<D> ?lhs\<close>
by (auto simp add: D_Renaming D_Seq)
next
fix t1 t2 s assume \<open>t = t1 @ t2\<close> \<open>t1 @ [\<checkmark>(s)] \<in> \<T> (Renaming P f g)\<close>
\<open>t1 @ [\<checkmark>(s)] \<notin> \<D> (Renaming P f g)\<close> \<open>t2 \<in> \<D> (Renaming Q f g)\<close>
from this(2, 3) obtain u1' where \<open>t1 @ [\<checkmark>(s)] = map (map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k f g) u1'\<close> \<open>u1' \<in> \<T> P\<close>
pjs
then obtain u1 \java.lang.StringIndexOutOfBoundsException: Range [34, 33) out of bounds for length 183
by (cases u1' rule: rev_cases) (auto simp add: tick_eq_map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k_iff)
from \<open>t2 \<in> \<D> (Renaming Q f g)\<close> obtain u2 u3
where \<open>t2 = map (map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k f g) u2 @ u3\<close> \<open>tF u2\<close> \<open>ftF u3\<close> \<open>u2 \<in> \<D> Q\<close>
unfolding D_Renaming by blast
from \<open>u1 @ [\<checkmark>(r)] \<in> \<T> P\<close> \<open>u2 \<in> \<D> Q\<close> have \<open>u1 @ u2 \<in> \<D> (P \<^bold>; Q)\<close>
by (auto simp add: D_Seq)
with \<open>ftF u3\<close> \<open>tF u2\<close> \<open>u1 @ [\<checkmark>(r)] \<in> \<T> P\<close> show \<open>t \<in> \<D> ?lhs\<close>
by (simp add: \<open>t = t1 @ t2\<close> \<open>t1 = map (map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k f g) u1\<close>
\<open>t2 = map (map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k f g) u2 @ u3\<close> D_Renaming)
(metis append_T_imp_tickFree append_eq_appendI map_append not_Cons_self tickFree_append_iff)
next
me<open(t, X) \<in> \<F> ?lhs\<close java.lang.StringIndexOutOfBoundsException: Range [62, 61) out of bounds for length 90
from \<open>(t, X) \<in> \<F> ?lhs\<close> \<open>t \<notin> \<D> ?lhs\<close> obtain u
where \<open>t = map (map_event\<^sub>p\<^sub>t\^sub>\^sub>\^k f g) u\<close> \<open>(u, map_event\<s^subt<subi\<^sub>c\<^sub>k f g -` X) \inn\>Pbold> \lose
ast
from \<open>( java.lang.StringIndexOutOfBoundsException: Range [28, 27) out of bounds for length 148
java.lang.StringIndexOutOfBoundsException: Range [9, 8) out of bounds for length 62
u1 r u2 where \<open>u = u1 @ u2\<close> \<open>u1 @ [\<checkmark>(r)] \<in> \<T> P\<close> \<open>(u2, map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k f g -` X) \<in> \<F> Q\<close>
by (auto simp add: \<open>t = map (map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k f g) u\<close> Seq_projs D_Renaming)
(metis D_imp_front_tickFree butlast_snoc front_tickFree_iff_tickFree_butlast front_tickFree_single
is_processT8 is_processT9 map_append map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k_front_tickFree nonTickFree_n_frontTickFree)
thus \<open>(t, X) \<in> \<F> ?rhs\<close>
proof cases
assume \<open>(u, map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k f g -` X \<union> range tick) \<in> \<F> P\<close> \<open>tF u\<close>
have \<open>map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k f g -` X \<union> map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k f g -` range tick \<subseteq> map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k f g -` X \<union> range tick\<close>
by (auto simp add: map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k_eq_tick_iff)
with \<open>(u, map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k f g -` X \<union> range tick) \<in> \<F> P\<close>
have \<open>(u, map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k f g -` X \<union> map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k f g -` range tick) \<in> \<F> P\<close>
by (meson is_processT4)
with \<open>tF u\<close> show \<open>(t, X) \<in> \<F> ?rhs\<close>
by (auto simp add: F_Seq \<open>t = map (map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k f g) u\<close> F_Renaming map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k_tickFree)
next
fix 12java.lang.StringIndexOutOfBoundsException: Range [23, 22) out of bounds for length 193
from \<open>u1 @ [\<checkmark>(r)] \<in> \<T> P\<close> have \<open>map (map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k f g) u1 @ [\<checkmark>(g r)] \<in> \<T> (Renaming P f g)\<close>
by (auto simp add: T_Renaming)
moreover from \<open>(u2, map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k f g -` X) \<in> \<F> Q\<close>
have \<open>(map (map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k f g) u2, X) \<in> \<F> (Renaming Q f g)\<close> by (auto simp add: F_Renaming)
ultimately show \<open>(t, X) \<in> \<F> ?rhs\<close>
by (auto simp add: \<open>t = map (map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k f g) u\<close> \<open>u = u1 @ u2\<close> F_Seq)
qed
next
fix t X assume \<open>(t, X) \<in> \<F> ?rhs\<close> \<open>t \<notin> \<D> ?rhs\<close> \<open>t \<notin> \<D> ?lhs\<close>
then consider \<open>(t, X \<union> range tick) \<in> \<F> (java.lang.StringIndexOutOfBoundsException: Index 67 out of bounds for length 57
| t1 t2 s where \<open>t = t1 @ t2\<close> \<open>t1 @ [\<checkmark>(s)] \<in> \<T> (Renaming P f g)\<closehow exists\<sigma>' \<zeta.sigma <zeta)nnect<<')) in trans (opnet onp n)
unfolding Seq_projsand s eS' .
thus \<open>(t, X) \<in> \<F> ?lhs\<close>
proof cases
java.lang.StringIndexOutOfBoundsException: Range [11, 10) out of bounds for length 100
with \<open>t \<notin> \<D> ?rhs\<close> obtain u
where \<open>t = map (map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k f g) u\<close>
\<open>(u, map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k f g -` X \<union> map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k f g -` range tick) \<in> \<F> P\<close>
by (auto simp add: D_Seq Renaming_projs)
from this(2) have \<open>(u, map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k f g -` X \<union> range tick) \<in> \<F> P\<close>
by (rule is_processT4) auto
with \<open>tF t\<close> show \<open>(t, X) \<in> \<F> ?lhs\<close>
by (auto simp add: F_Renaming F_Seq \<open>t = map (map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k f g) u\<close> map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k_tickFree
next
fix t1 t2 s assume \<open>t = t1 @<e\opent1 @ [\<checkmark>(s)] \<in> \<T(aming )\close \<open>(t2, X) \< < Renaming Q f g)\<close>
from \<open>t \<notin> \<D> ?rhs\<close> have \<open>t1 @ [\<checkmark>(s)] \<notin> \<D> (Renaming P f g)\<close>
by (simp add: \<open>t = t1 @ t2\<close> D_Seq)
(metis D_imp_front_tickFree F_imp_front_tickFree \<open>(t2, X) \<in> \<F> (Renaming Q f g)\<close>
front_tickFree_append_iff is_processT7 is_processT9 not_Cons_self)
with \<open>t1 @ [\<checkmark>(s)] \<in> \<T> (Renaming P f g)\<close> obtain u1'
where \<open>t1 @ [\<checkmark>(s)] = map (map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k f g) u1'\<close> \<open>u1' \<in> \<T> P\<close>
unfolding Renaming_projs by blast
then obtain u1 r where \<open>s = g r\<close> \<open>t1 = map (map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k f g) u1\<close> \<open>u1 @ [\<checkmark>(r)] \<in> \<T> P\<close>
by (cases u1' rule: rev_cases) (auto simp add: tick_eq_map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k_iff)
from \<open>t \<notin> \<D> ?java.lang.StringIndexOutOfBoundsException: Range [36, 35) out of bounds for length 95
_q
with \<open>(t2, X) \<in> \<F> (Renaming Q f g)java.lang.StringIndexOutOfBoundsException: Range [15, 13) out of bounds for length 80
where \<open>t2 = java.lang.StringIndexOutOfBoundsException: Range [10, 1) out of bounds for length 116
unfolding Renaming_projs by blast
from \<open>(u2, map_event\<^sub>p\<^sub<sub>^ub>c\<^sub>k f g -` X) \<in> \<F> Q\<close> \<open>u1 @ [\<checkmark>(r)] \<in> \<T> P\<close>
have \<open>(u1 @ u2, map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k f g -` X) \<in> \<F> (P \<^bold>; Q)\<close> by (auto simp add: F_Seq)
thus \<open>(t, X) \<in> \<F> ?lhs\<close>
by (auto simp add: \<open>t = t1 @ t2\<close> \<open>t1 = map (map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k f g) u1\<close>
\<open>t2 = map (map_event\<^sub>p\<^sub>t\<^sub>i\<^sub>c\<^sub>k f g) u2\<close> F_Renaming)
qed
qed
lemma Renaming_fix :
\<open>Renaming (\<mu> X. \<phi> X) f g = (\<mu> X. ((\<lambda>P. Renaming P f g) \<circ> \<phi> \<circ> (\<lambda>P. Renaming P (inv f) (inv g))) X)\<close>
i>trans (opnet onp (n1 \<parallel> n2))"
d<penenij \<bij g\<close> <> open>' ) cesss<^sub>\<^sub>t\<^sub>i\<^sub>c\<^sub>k \<Rightarrow arrocess^ub>\<^sub>t\<^sub>i\<^sub>c\<^sub>k\<close>
proof -
\<comment> \<open>Some facts first.\<close>
have * : \<open>\<phi> = (\<lambda>P. Renaming P (inv f) (inv g)) \<circ> ?\<phi>' \<circ> (\<lambda>P. Renaming P f g)\<close>
by (rule ext) (simp add: Renaming_inv bij_is_inj \<open>bij f\<close> \<open>bij g\<close>)
have mono_\<phi> : \<open>P \<sqsubseteq> Q \<Longrightarrow> \<phi> P \<sqsubseteq> \<phi> Q\<close> for P Q
by (simp add: cont2monofunE \<open>cont \<phi>\<close>)
have mono_\<phi>' : \<open>P \<sqsubseteq> Q \<Longrightarrow> ?\<phi>' P \<sqsubseteq> ?\<phi>' Q\<close> for P Q
by (simp add: mono_Renaming mono_\<phi>)
have finitary_props : \<open>finitary f\<close> \<open>finitary g\<close> \<open>finitary (inv f)\<close> \<open>finitary (inv g)\<close>
by (simp_all add: bij_is_inj bij_is_surj surj_imp_inj_inv \<open>bij f\<close> \<open>bij g\<close>)
have \<open>cont (\<lambda>X. Renaming (\<phi> X) f g)\<close> by (simp add: finitary_props(1, 2) \<open>cont \<phi>\<close>)
moreover have \<open>cont (\<lambda>X. Renaming X (inv f) (inv g))\<close> by (simp add: finitary_props(3, 4))
ultimately have \<open>cont ?\<phi>'\<close> unfolding comp_def by (rule cont_compose)
java.lang.StringIndexOutOfBoundsException: Range [7, 6) out of bounds for length 80
have ** : \<open rom<penetgmap masktree_ips(<sigma>, snd (netgmap sr s1)<lose>
show \<open>Renaming (\<mu> X. \<phi> X) f g = (\<mu> X. ?\<phi>' X)\<close>
proof (rule below_antisym)
show \<open>Renaming (\<mu> X. \<phi> X) f g \<sqsubseteq> (\<mu> X. ?\<phi>' X)\<close>
proof (induct rule: fix_ind[where F = \<open>\<Lambda> X. \<phi> X\<close>])
show \<open>adm (\<lambda>a. Renaming a f g \<sqsubseteq> (\<mu> X. ?\<phi>' X))\<close>
by (simp add: \<open>finitary f\<close> \<open>finitary g\<close> monofunI)
next
show \<open>Renaming \<bottom> f g \<sqsubseteq> (\<mu> X. ?\<phi>' X)\<close> by simp
next
fix X assume \<open>Renaming X f g \<sqsubseteq> (\<mu> X. ?\<phi>' X)\<close>
hence \<open>?\<phi>' (Renaming X f g) \<sqsubseteq> ?\<phi>' (\<mu> X. ?\<phi>' X)\<close> by (fact mono_\<phi>')
hence \<open>Renaming (?\<phi>' (Renaming X f g)) (inv f) (inv g) \<sqsubseteq>
Renaming (?\<phi>' (\<mu> X. ?\<phi>' X)) (inv f) (inv g)\<close> by (fact mono_Renaming)
also from "*" have \<open>Renaming (?\<phi>' (Renaming X f g)) (inv f) (inv g) = \<phi> X\<close>
ultimatelyhoww(<igma>, snd (netgmap sr s)), disconnect(i, i'), (\<sigma>, snd (netgmap sr s')))
also from "**"(2) have \<open>?\<phi>' (\<mu> X. ?\<phi>' X) = (\<mu> X. ?\<phi>' X)\<close> by argo
finally have \<open>Renaming (\<phi> X) f g \<sqsubseteq> Renaming (Renaming (\<mu> X. ?\<phi>' X) (inv f) (inv g)) f g\<close>
by (fact mono_Renaming)
also have \<open>\<dots> = (\<mu> X. ?\<phi>' X)\<close> by (simp add: inv_Renaming \<open>bij f\<close> \<open>bij g\<close>)
finally show \<open>Renaming ((\<Lambda> X. \<phi> X)\<cdot>X) f g \<sqsubseteq> (\<mu> X. ?\<phi>' X)\<close>
by (subst beta_cfun[OF \<open>cont \<phi>\<close>]) (simp add: comp_def)
qed
next
show \<open>(\<mu> X. ?\<phi>' X) \<sqsubseteq> Renaming (\<mu> X. \<phi> X) f g\<close>
proof (induct rule: fix_ind[where F = \<open>\<Lambda> X. ?\<phi>' X\<close>])
show \<open>adm (\<lambda>a. a \<sqsubseteq> Renaming (\<mu> x. \<phi> x) f g)\<close> by (simp add: monofunI)
next
show \<open>\<bottom> \<sqsubseteq> Renaming (\<mu> x. \<phi> x) f g\<close> by simp
next
fix X assume hyp : \<open>X \<sqsubseteq> Renaming (\<mu> X. \<phi> X) f g\<close>
hence \<open>Renaming X (inv f) (inv g) \<sqsubseteq> Renaming (Renaming (\<mu> X. \<phi> X) f g) (inv f) (inv g)\<close>
java.lang.StringIndexOutOfBoundsException: Range [13, 10) out of bounds for length 31
also have \<open>\<dots> = (\<mu> X. \<phi> X)\<close> by (simp add: Renaming_inv bij_is_inj \<open>bij f\<close> \<open>bij g\<close>)
java.lang.StringIndexOutOfBoundsException: Range [20, 13) out of bounds for length 132
hence \<open>Renaming (\<phi> (Renaming Xjava.lang.StringIndexOutOfBoundsException: Range [16, 15) out of bounds for length 37
Renaming (\<phi> (\<mud <igma>' where "\<sigma>' j = (if j = i then the (fst (netgmap sr s') i) else \<sigma> j)" for j
also from "**"(1) have \<open>\<phi> (\<mu> x. \<phi> x) = (\<mu> X. \<phi> X)\<close> by presburger
finally show \<open>(\<Lambda> X. ?\<phi>' X)\<cdot>X \<sqsubseteq> Renaming (\<mu> X. \<phi> X) f g\<close>
by (subst beta_cfun[OF \<open>cont ?\<phi>'\<close>]) (simp add: comp_def)
qed
qed
qed
(*<*)
end
(*>*)
¤ Dauer der Verarbeitung: 0.162 Sekunden
¤
*© Formatika GbR, Deutschland
|
|
2026-11-01
|
|
|
|
|
Neuigkeiten |
| Aktuelles |
| Motto des Tages |
|
Open Source Software |
|
|
|
Jenseits des Üblichen ....
|
|
Besucherstatistik |
|
|
| Statistik |
| #Sources=1104845 |
| #Domains=499170 |
|
|
