Theory CSP_Laws

(*<*)
―‹ ********************************************************************
 * Project         : HOL-CSP - A Shallow Embedding of CSP in  Isabelle/HOL
 * Version         : 2.0
 *
 * Author          : Burkhart Wolff, Safouan Taha, Lina Ye, Benoît Ballenghien.
 *                   (Based on HOL-CSP 1.0 by Haykal Tej and Burkhart Wolff)
 *
 * This file       : A Combined CSP Theory
 *
 * Copyright (c) 2009 Université Paris-Sud, 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.
 ******************************************************************************›
(*>*)


chapter‹ The "Laws" of CSP ›

theory CSP_Laws                                               
  imports Bot Skip Stop Det Ndet Mprefix Mndetprefix Seq Hiding Sync Renaming
          "HOL-Eisbach.Eisbach"
begin 

method exI for y::'a = (rule_tac exI[where x = y])


section‹ General Laws›

lemma SKIP_Neq_STOP: "SKIP  STOP"
  by (auto simp: Process_eq_spec F_SKIP F_STOP D_SKIP D_STOP Un_def)

lemma BOT_less1[simp]: "  (X::'a process)"
  by (simp add: le_approx_implies_le_ref)

lemma BOT_less2[simp]: "BOT  (X::'a process)"
  by simp

section‹ Deterministic Choice Operator Laws ›

lemma mono_Det_FD_onside[simp]: " P  P'  (P  S)  (P'  S)"
  unfolding le_ref_def F_Det D_Det using F_subset_imp_T_subset by blast

lemma mono_Det_FD[simp]: " P  P'; S  S'  (P  S)  (P'  S')"
  by (metis Det_commute dual_order.trans mono_Det_FD_onside)

lemma mono_Det_ref: " P  P'; S  S'  (P  S)  (P'  S')"
  using below_trans mono_Det mono_Det_sym by blast

lemma Det_BOT : "(P  ) = "
  by (auto simp add:Process_eq_spec D_Det F_Det is_processT2 D_imp_front_tickFree F_UU D_UU) 

lemma Det_STOP: "(P  STOP) = P"
  by (auto simp add: Process_eq_spec D_Det F_Det D_STOP F_STOP T_STOP 
                      Un_def Sigma_def is_processT8 is_processT6_S2)  

lemma Det_id: "(P  P) = P"
  by (auto simp: Process_eq_spec D_Det F_Det Un_def Sigma_def is_processT8 is_processT6_S2)

lemma Det_assoc: "((M  P)  Q) = (M  (P  Q))"
  by (auto simp add: Process_eq_spec D_Det F_Det Un_def Sigma_def T_Det)  


section‹ NonDeterministic Choice Operator Laws ›

lemma mono_Ndet_FD[simp]: " P  P'; S  S'  (P  S)  (P'  S')"
  by (auto simp: le_ref_def F_Ndet D_Ndet)

lemma mono_Ndet_FD_left[simp]: "P  Q  (P  S)  Q" 
  by (metis D_Ndet F_Ndet dual_order.trans le_ref_def le_sup_iff order_refl)

lemma mono_Ndet_FD_right[simp]: "P  Q  (S  P)  Q" 
  by (metis D_Ndet F_Ndet dual_order.trans le_ref_def le_sup_iff order_refl)

lemma mono_Ndet_ref: " P  P'; S  S'  (P  S)  (P'  S')"
  using below_trans mono_Ndet mono_Ndet_sym by blast

lemma Ndet_BOT: "(P  ) = "
  by (auto simp: Process_eq_spec D_Ndet F_Ndet is_processT2 D_imp_front_tickFree F_UU D_UU)

lemma Ndet_id: "(P  P) = P"
  by (simp_all add: F_Ndet D_Ndet Process_eq_spec)  

lemma Ndet_assoc: "((M  P)  Q) = (M  (P  Q))"
  by (simp_all add: F_Ndet D_Ndet  Process_eq_spec Un_assoc)  

subsection‹ Multi-Operators laws  ›

lemma Det_distrib: "(M  (P  Q)) = ((M  P)  (M  Q))"
  by (auto simp add:  Process_eq_spec F_Det D_Det F_Ndet D_Ndet Un_def T_Ndet)

lemma Ndet_distrib: "(M  (P  Q)) = ((M  P)  (M  Q))"
  by (auto simp add:  Process_eq_spec F_Det D_Det F_Ndet 
                      D_Ndet Un_def T_Ndet is_processT8 is_processT6_S2)

lemma Ndet_FD_Det: "(P  Q)  (P  Q)"
  apply(auto simp add:le_ref_def D_Ndet D_Det F_Ndet F_Det T_Ndet T_Det Ra_def min_elems_def) 
  using is_processT6_S2 NF_ND by blast+


section‹ Sequence Operator Laws ›

subsection‹Preliminaries›

definition F_minus_D_Seq where 
    "F_minus_D_Seq P Q  {(t, X). (t, X  {tick})   P  tickFree t} 
                                {(t, X). t1 t2. t = t1 @ t2  t1 @ [tick]  𝒯 P  (t2, X)   Q}"

lemma F_minus_D_Seq_opt: "(a,b)  (P ; Q) = (a  𝒟(P ; Q)  (a,b)  F_minus_D_Seq P Q)"
  using NF_ND by (auto simp add: F_Seq D_Seq F_minus_D_Seq_def) blast+
  

lemma Process_eq_spec_optimized_Seq : 
"((P ; Q) = (U ; S)) = (𝒟 (P ; Q) = 𝒟 (U ; S)  
                            F_minus_D_Seq P Q   (U ; S)  
                            F_minus_D_Seq U S   (P ; Q))"
  unfolding Process_eq_spec_optimized[of "(P ; Q)" "(U ; S)"] 
  by (auto simp:F_minus_D_Seq_opt)

subsection‹Laws›

lemma mono_Seq_FD[simp]: " P  P'; S  S'  (P ; S)  (P' ; S')"
  apply (auto simp: le_ref_def F_Seq D_Seq)
  by (metis F_subset_imp_T_subset subsetCE)+

lemma mono_Seq_ref: " P  P'; S  S'  (P ; S)  (P' ; S')"
  using below_trans mono_Seq mono_Seq_sym by blast

lemma BOT_Seq: "( ; P) = "
  by (simp add: BOT_iff_D D_Seq D_UU)
   

lemma Seq_SKIP: "(P ; SKIP) = P"
  apply (auto simp add: Process_eq_spec F_Seq F_SKIP D_Seq D_SKIP T_F_spec is_processT6_S1)
      apply (use is_processT4 in blast)
     apply (meson append_single_T_imp_tickFree is_processT5_S7 non_tickFree_tick tickFree_append)
    apply (meson is_processT8)
   apply (use T_F_spec insert_absorb is_processT5_S2 in fastforce)
  by (metis F_T is_processT nonTickFree_n_frontTickFree)

lemma SKIP_Seq: "(SKIP ; P) = P"
  by (auto simp add: Process_eq_spec D_Seq T_SKIP F_Seq F_SKIP D_SKIP is_processT8_Pair)

lemma STOP_Seq: "(STOP ; P) = STOP"
  by (simp add: STOP_iff_T T_Seq T_STOP F_STOP D_STOP Collect_conv_if)


subsection‹ Multi-Operators laws  ›

lemma Seq_Ndet_distrR: "((P  Q) ; S) = ((P ; S)  (Q ; S))"
  by (auto simp add: Process_eq_spec D_Seq D_Ndet T_Ndet Un_def F_Seq T_Seq F_Ndet)

lemma Seq_Ndet_distrL: "(P ; (Q  S)) = ((P ; Q)  (P ; S))"
  by (auto simp add: Process_eq_spec D_Seq D_Ndet T_Ndet Un_def F_Seq F_Ndet)

lemma Seq_assoc_D: "𝒟 (P ; (Q ; S)) = 𝒟 ((P ; Q) ; S)"
proof(safe, goal_cases)
  show s  𝒟 (P ; (Q ; S))  s  𝒟 (P ; Q ; S) for s
    by (simp add: D_Seq T_Seq) (metis append.assoc)
next
  fix s
  assume s  𝒟 (P ; Q ; S)
  thus s  𝒟 (P ; (Q ; S))
  proof(auto simp add:D_Seq T_Seq, goal_cases)
    case (1 t1 t2 t1a t2a)
    from "1"(1)[rule_format, OF "1"(5)] show ?case
      apply (cases tickFree t2a)
       apply (metis "1"(4) "1"(5) append_single_T_imp_tickFree non_tickFree_tick tickFree_append)
      by (metis "1"(3) "1"(4) "1"(6) T_nonTickFree_imp_decomp append.assoc butlast_snoc)
  next
    case (2 t1 t2)
    then show ?case 
      by (meson D_imp_front_tickFree front_tickFree_implies_tickFree is_processT7 is_processT9_S_swap)
  qed
qed
  
lemma Seq_assoc: "(P ; (Q ; S)) = ((P ; Q) ; S)"
proof (auto simp: Process_eq_spec_optimized_Seq Seq_assoc_D, goal_cases)
  case (1 a b)
  then show ?case
  proof(auto simp add:F_minus_D_Seq_def Seq_assoc_D F_minus_D_Seq_opt append_single_T_imp_tickFree 
             del:conjI, 
        goal_cases 11 12)
    case (11 t1 t2)
    then show ?case by (metis (mono_tags, lifting) D_Seq Seq_assoc_D UnCI mem_Collect_eq)
  next
    case (12 t1 t1a t2a)
    hence "(t1 @ t1a) @ [tick]  𝒯 (P ; Q)" by (auto simp:T_Seq)
    then show ?case
      using 12(2)[rule_format, of "t1@t1a" t2a] 12(4,5,6) by simp
  qed
next
  case (2 a b)
  then show ?case
  proof(auto simp add:F_minus_D_Seq_def Seq_assoc_D F_minus_D_Seq_opt 
                       append_single_T_imp_tickFree T_Seq del:conjI, 
      goal_cases 21 22 23)
    case 21
    then show ?case
      using D_Seq by force
  next
    case (22 t1 t2 t1a t2a)
    then obtain t2b where  "t2a = t2b@[tick]"
      by (metis T_nonTickFree_imp_decomp append_single_T_imp_tickFree non_tickFree_tick tickFree_append)
    with 22 show ?case using append.assoc butlast_snoc by auto
  next
    case (23 t1 t2)
    hence "t1  𝒟 (P ; (Q ; S))" 
      by (simp add: D_Seq) (meson is_processT9_S_swap)
    with 23 Seq_assoc_D show ?case by (metis front_tickFree_implies_tickFree process_charn)
  qed
qed


section‹ The Multi-Prefix Operator Laws ›

lemma mono_Mprefix_FD[simp]: "x  A. P x  P' x  Mprefix A P  Mprefix A P'"
  by (auto simp: le_ref_def F_Mprefix D_Mprefix) blast+

lemmas mono_Mprefix_ref =  mono_Mprefix0

lemma Mprefix_STOP: "(Mprefix {} P) = STOP"
  by (auto simp:Process_eq_spec F_Mprefix D_Mprefix D_STOP F_STOP)

subsection‹ Multi-Operators laws  ›

lemma Mprefix_Un_distrib: "(Mprefix (A  B) P) = ((Mprefix A P)  (Mprefix B P))"
  apply (unfold Process_eq_spec, rule conjI)
  apply (auto, (elim disjE conjE | simp_all add: F_Det F_Mprefix Un_def image_def)+, auto)
  by (auto simp add: D_Det D_Mprefix Un_def)

lemma Mprefix_Seq: "((Mprefix A P) ; Q) = (Mprefix A (λx. (P x) ; Q))"
proof (unfold Process_eq_spec, rule conjI, rule subset_antisym, goal_cases)
  case 1
  then show ?case   
    apply(unfold split_def F_Seq D_Seq F_Mprefix T_Mprefix D_Mprefix)
    apply(rule subsetI, simp_all, elim disjE conjE exE)
        apply(rule disjI1, simp, meson tickFree_tl)
       apply (rule disjI2, rule conjI, simp) apply auto[1]
      apply (auto simp add:hd_append)[1]
   using tickFree_tl by fastforce
next
  case 2
  then show ?case 
    apply(unfold split_def F_Seq D_Seq F_Mprefix T_Mprefix D_Mprefix)
    apply(rule subsetI, simp_all, elim disjE conjE exE)
        apply(rule disjI1, simp, blast)
       apply(rule disjI1, metis event.simps(3) list.exhaust_sel tickFree_Cons)
  proof(goal_cases)
    case (1 x a t1 t2)
    then show ?case 
      apply(rule_tac disjI2, rule_tac disjI1, rule_tac x="(ev a)#t1" in exI) 
      using hd_Cons_tl image_iff by fastforce
  next
    case (2 x a)
    then show ?case     
      by (metis prod.collapse)
  qed
next
  case 3
  then show ?case     
    apply (auto simp add: D_Mprefix D_Seq T_Mprefix)
      apply (metis event.distinct(1) hd_append image_iff list.sel(1))
     apply (metis event.distinct(1) hd_append list.sel(1) tl_append2)
    by (metis Cons_eq_appendI hd_Cons_tl list.sel(1) list.sel(3))
qed

subsection‹ Derivative Operators laws  ›

lemma Mprefix_singl: "(Mprefix {a} P) = (a  (P a))"
  by (simp add:write0_def Mprefix_def, rule arg_cong[of _ _ "λx. Abs_process x"]) fastforce

lemma mono_read_FD: "(x. P x  Q x)   (c?x  (P x))  (c?x  (Q x))"
  by (simp add: read_def)

lemma mono_write_FD: "(P  Q)   (c!x  P)  (c!x  Q)"
  by (simp add: write_def)

lemma mono_write0_FD: "P  Q  (a  P)  (a  Q)"
  by (simp add: write0_def)

lemma mono_read_ref: "(x. P x  Q x)   (c?x  (P x))  (c?x  (Q x))"
  by (simp add: mono_Mprefix0 read_def)
                                         
lemma mono_write_ref: "(P  Q)   (c!x  P)  (c!x  Q)"
  by (simp add: mono_Mprefix0 write_def)

lemma mono_write0_ref: "P  Q  (a  P)  (a  Q)"
  by (simp add: mono_Mprefix0 write0_def)

lemma write0_Ndet: "(a  (P  Q)) = ((a  P)  (a  Q))"
  by (auto simp: Process_eq_spec write0_def D_Ndet F_Ndet F_Mprefix D_Mprefix Un_def)

lemma write0_Det_Ndet: "((a  P)  (a  Q)) = ((a  P)  (a  Q))"
  by (auto simp: Process_eq_spec write0_def D_Ndet F_Ndet F_Det D_Det) (simp add: F_Mprefix)+

lemma Mprefix_Det: (eA  P e)  (eA  Q e) = eA  (P e  Q e)
  by (auto simp: Process_eq_spec F_Det D_Det) (auto simp: D_Ndet F_Ndet F_Mprefix D_Mprefix)

section‹ The Hiding Operator Laws ›

subsection‹ Preliminaries ›

lemma elemDIselemHD: t  𝒟 P  trace_hide t (ev ` A)  𝒟 (P \ A)
proof (cases "tickFree t")
  case True
  assume "t  𝒟 P"
  with True show ?thesis by (simp add:D_Hiding, rule_tac x=t in exI, rule_tac x="[]" in exI, simp)
next
  case False
  assume a:"t  𝒟 P"
  with False obtain t' where "t = t'@[tick]" using D_imp_front_tickFree nonTickFree_n_frontTickFree by blast
  with a show ?thesis apply (auto simp add:D_Hiding, rule_tac x=t' in exI, rule_tac x="[tick]" in exI)  
    by (meson front_tickFree_implies_tickFree front_tickFree_single is_processT)
qed

lemma length_strict_mono: "strict_mono (f::nat  'a list)  length (f i)  i + length (f 0)"
  apply(induct i, simp)
  by (metis dual_order.trans lessI less_length_mono not_less not_less_eq_eq plus_nat.simps(2) strict_mono_def)

lemma mono_trace_hide: "a  b  trace_hide a (ev ` A)  trace_hide b (ev ` A)"
  by (metis filter_append le_list_def)

lemma mono_constant: 
  assumes "mono (f::nat  'a event list)" and "i. f i  a"
  shows "i. ji. f j = f i"
proof -
  from assms(2) have "i. length (f i)  length a"
    by (simp add: le_length_mono)
  hence aa:"finite {length (f i)|i. True}" 
    using finite_nat_set_iff_bounded_le by auto
  define lm where l2:"lm = Max {length (f i)|i. True}"
  with aa obtain im where "length (f im) = lm" using Max_in by fastforce
  with l2 assms(1) show ?thesis 
    apply(rule_tac x=im in exI, intro impI allI)
    by (metis (mono_tags, lifting) Max_ge aa antisym le_length_mono le_neq_trans less_length_mono 
              mem_Collect_eq mono_def order_less_irrefl)
qed
  
lemma elemTIselemHT: t  𝒯 P  trace_hide t (ev ` A)  𝒯 (P \ A)
proof (cases "tickFree t")
  case True
  assume a:"t  𝒯 P"
  with True show ?thesis
  proof (cases "(ta. trace_hide t (ev ` A) = trace_hide ta (ev ` A)  (ta, ev ` A)   P)")
    case True
    thus ?thesis by (simp add:T_Hiding)
  next
    case False
    with a False inf_hidden[of A t P] obtain f where "isInfHiddenRun f P A  t  range f" by auto
    with True show ?thesis 
      by (simp add:T_Hiding, rule_tac disjI2, rule_tac x=t in exI, rule_tac x="[]" in exI, auto)
  qed
next
  case False
  assume a:"t  𝒯 P"
  with False obtain t' where tt:"t = t'@[tick]" using T_nonTickFree_imp_decomp by auto
  with a show ?thesis 
  proof (cases "(ta. trace_hide t (ev ` A) = trace_hide ta (ev ` A)  (ta, ev ` A)   P)")
    case True
    thus ?thesis by (simp add:T_Hiding)
  next
    case False
    assume "t  𝒯 P"
    with False inf_hidden[of A t P] obtain f where "isInfHiddenRun f P A  t  range f" by auto
    then show ?thesis 
      apply (simp add:T_Hiding, rule_tac disjI2, rule_tac x=t' in exI, rule_tac x="[tick]" in exI, auto)
        apply (metis append_T_imp_tickFree list.distinct(1) tt)
       using tt apply force
      by (metis False append_T_imp_tickFree is_processT5_S7 non_tickFree_tick not_Cons_self2 tickFree_append tt)
  qed
qed

lemma Hiding_Un_D1: 𝒟 (P \ (A  B))  𝒟 ((P \ A) \ B)
proof (simp add:conj_commute D_Hiding, intro conjI subset_antisym subsetI, simp_all, goal_cases)
  case (1 x)
  then obtain t u where B1:"x = trace_hide t (ev ` (A  B)) @ u" 
                    and B2:"tickFree t" and B3:"front_tickFree u" 
                    and B4:"(t  𝒟 P  ((f:: nat  'a event list). isInfHiddenRun f P (A  B) 
                                                                       t  range f))" by auto
  thus ?case
    apply(erule_tac  disjE)
    apply(rule_tac x="trace_hide t (ev ` A)" in exI, rule_tac x=u in exI)
    apply(simp add:Hiding_tickFree tickFree_def)
    apply(rule disjI1, rule_tac x=t in exI, rule_tac x="[]" in exI, simp) 
  proof(goal_cases)
    case 1
    then obtain f n where fc:"isInfHiddenRun f P (A  B)  t = f n" by auto
    define ff where "ff = (λi. take (i + length (f 0)) (f i))"
    with fc have ffc:"isInfHiddenRun ff P (A  B)  t  range ff" 
    proof (auto, goal_cases)
      case 1
      { fix x
        from length_strict_mono[of f "Suc x ", OF 1(2)]
        have a:"take (x + length (f 0)) (f (Suc x)) < take ((Suc x) + length (f 0)) (f (Suc x))"
          by (simp add: take_Suc_conv_app_nth)
        from 1(2)[THEN strict_monoD, of x "Suc x", simplified] 
          obtain t where "f (Suc x) = (f x @ t)" by (metis le_list_def less_imp_le)
        with length_strict_mono[of f x, OF 1(2)]
          have "take (x + length (f 0)) (f x) = take (x + length (f 0)) (f (Suc x))" by simp
        with a have "take (x + length (f 0)) (f x) < take (Suc x + length (f 0)) (f (Suc x))" by simp
      }
      thus ?case by (meson lift_Suc_mono_less strict_mono_def)
    next
      case (2 i)
      have "take (i + length (f 0)) (f i)  f i"
        using append_take_drop_id le_list_def by blast
      also have "x y. x  y  y  𝒯 P  x  𝒯 P" using is_processT3_ST_pref by blast
      ultimately show ?case using "2"(3) by blast 
    next
      case (3 i)
      hence "(f i)  (f 0)" using strict_mono_less_eq by blast
      hence "take (i + length (f 0)) (f i)  (f 0)"
        by (metis add.commute append_eq_conv_conj le_list_def take_add)
      hence a:"   [xtake (i + length (f 0)) (f i) . x  ev ` A  x  ev ` B] 
                 [xf 0 . x  ev ` A  x  ev ` B]"
        by (metis (no_types, lifting) filter_append le_list_def)
      have "take (i + length (f 0)) (f i)  f i"
        using append_take_drop_id le_list_def by blast
      hence "  [xtake (i + length (f 0)) (f i) . x  ev ` A  x  ev ` B] 
              [xf i . x  ev ` A  x  ev ` B]"
        by (metis (no_types, lifting) filter_append le_list_def)
      with a 3(4) show ?case by (metis (no_types, lifting) dual_order.antisym)
    next
      case 4
      have "f (length (f n) - length (f 0))  f n"
        by (simp add: "4"(2) add_le_imp_le_diff length_strict_mono strict_mono_less_eq)
      hence "f n = (λi. take (i + length (f 0)) (f i)) (length (f n) - length (f 0))" 
        by (metis "4"(2) add.commute append_eq_conv_conj diff_is_0_eq' 
                  le_add_diff_inverse le_list_def le_zero_eq nat_le_linear strict_mono_less_eq)
      then show ?case by blast
    qed
    thus ?case proof(cases "m. (i>m. last (ff i)  (ev ` A))")
      case True
      then obtain m where mc:"i>m. last (ff i)  (ev ` A)" by blast
      hence mc2:"tickFree (ff m)" 
        by (metis (no_types, lifting) B2 event.distinct(1) ffc 
                                      image_iff mem_Collect_eq set_filter tickFree_def)
      with mc mc2 1 ffc show ?thesis 
        apply(rule_tac x="trace_hide (ff m) (ev ` A)" in exI, rule_tac x=u in exI, simp, intro conjI)    
        apply (metis (no_types, lifting) mem_Collect_eq set_filter tickFree_def)
        apply (metis (no_types, lifting) rangeE)
        apply(rule disjI1, rule_tac x="ff m" in exI, rule_tac x="[]" in exI, intro conjI, simp_all)
        apply(rule disjI2, rule_tac x="λi. ff(i + m)" in exI, intro conjI)
           apply (metis (no_types, lifting) add.commute add.right_neutral rangeI) 
          apply (simp add: strict_mono_def)
         apply blast
        proof(rule allI, goal_cases)
          case (1 i)
          from ffc ff_def True have "t. (ff (i + m)) = (ff m) @ t  set t  (ev ` A)" 
          proof(induct i)
            case 0
            then show ?case by fastforce
          next
            case (Suc i)
            then obtain tt where tc:"(ff (i + m)) = (ff m) @ tt  set tt  (ev ` A)" by blast
            from ffc ff_def length_strict_mono[of ff] have lc:"length (ff (Suc i + m)) 
                                                              = Suc (length (ff (i + m)))" 
              by (metis (no_types, lifting) add_Suc fc length_strict_mono length_take min.absorb2)
            from True obtain l where lc2:"l = last (ff (Suc i + m))  l  (ev ` A)"
              by (meson less_add_same_cancel2 mc zero_less_Suc)
            from ffc obtain r where rc:"ff (Suc i + m) = ff (i + m)@r"
              by (metis add.commute add_Suc_right le_list_def lessI less_imp_le strict_mono_less_eq)
            with lc have "length r = 1" by (metis Suc_eq_plus1 add_left_cancel length_append)
            with rc lc2 have "r = [l]"
              by (metis (no_types, lifting) Nil_is_append_conv Suc_eq_plus1 append_butlast_last_id 
                        append_eq_append_conv append_eq_append_conv2 length_Cons length_append)
            with Suc lc2 tc rc show ?case by (rule_tac x="tt@[l]" in exI, auto) 
          qed
          then show ?case using filter_empty_conv by fastforce
        qed
    next
      case False
      { fix i
        assume as:"(i::nat) > 0"
        with ffc obtain tt where ttc:"ff i = ff 0 @ tt  set tt  ev ` (A  B)" 
          unfolding isInfHiddenRun_1 by blast
        with ffc as have "tt  []" using strict_mono_eq by fastforce
        with ttc have "last (ff i)  ev ` (A  B)" by auto
      }
      hence as2:"i. j>i. last(ff j)  ((ev ` B) - (ev ` A))"
        by (metis DiffI False UnE gr_implies_not_zero gr_zeroI image_Un)
      define ffb where "ffb = rec_nat t (λi t. (let j = SOME j. ff j > t  
                              last(ff j)  ((ev ` B) - (ev ` A)) in ff j))"
      with as2 have ffbff:"n. ffb n  range ff"
        by (metis (no_types, lifting) ffc old.nat.exhaust old.nat.simps(6) old.nat.simps(7) rangeI)
      from 1 ffb_def show ?thesis
        apply(rule_tac x="trace_hide t (ev ` A)" in exI, rule_tac x=u in exI, simp, intro conjI)
         apply (meson filter_is_subset set_rev_mp tickFree_def)        
      proof(rule disjI2, rule_tac x="λi. trace_hide (ffb i) (ev ` A)" in exI, intro conjI, goal_cases)
        case 1
        then show ?case by (metis (no_types, lifting) old.nat.simps(6) rangeI) 
      next
        case 2
        { fix n
          have a0:"(ffb (Suc n)) = ff (SOME j. ff j > ffb n  last(ff j)  ((ev ` B) - (ev ` A)))" 
            by (simp add: ffb_def)
          from ffbff obtain i where a1:"ffb n = ff i" by blast
          with as2 have "j. ff j > ffb n  last(ff j)  ((ev ` B) - (ev ` A))"
            by (metis ffc strict_mono_def)
          with a0 a1 have a:"(ffb (Suc n)) > (ffb n)  last (ffb (Suc n))  (ev ` A)"
            by (metis (no_types, lifting) Diff_iff tfl_some) 
          then obtain r where  "ffb (Suc n) =  (ffb n)@r  last r  (ev ` A)"
            by (metis append_self_conv last_append le_list_def less_list_def) 
          hence "trace_hide (ffb (Suc n)) (ev ` A) > trace_hide (ffb n) (ev ` A)"
            by (metis (no_types, lifting) a append_self_conv filter_append filter_empty_conv 
                                          last_in_set le_list_def less_list_def)
        }
        then show ?case by (metis (mono_tags, lifting) lift_Suc_mono_less_iff strict_monoI)
      next
        case 3
        then show ?case by (metis (mono_tags) elemTIselemHT ffbff ffc rangeE)  
      next
        case 4
        from ffbff ffc show ?case by (metis rangeE trace_hide_union)
      qed
    qed
  qed
qed

lemma Hiding_Un_D2: finite A  𝒟 ((P \ A) \ B)  𝒟 (P \ (A  B))
proof (simp add:conj_commute D_Hiding, intro conjI subset_antisym subsetI, simp_all, goal_cases)
  case (1 x)
  then obtain t u where B1:"x = trace_hide t (ev ` B) @ u" 
                   and  B2:"tickFree t" 
                   and  B3:"front_tickFree u" 
                   and  B4:(t  𝒟 (P \ A)  
                            ((f:: nat  'a event list). isInfHiddenRun f (P \ A) B  t  range f))
    by (simp add:D_Hiding) blast
  thus ?case
  proof(erule_tac disjE, auto simp add:D_Hiding, goal_cases)
    case (1 ta ua)
    then show ?case 
      by (rule_tac x=ta in exI, rule_tac x = "trace_hide ua (ev ` B) @ u" in exI, 
          auto simp add: front_tickFree_append tickFree_def)
  next
    case (2 ua f xa)
    then show ?case 
      apply(rule_tac x="f xa" in exI, rule_tac x="trace_hide ua (ev ` B) @ u" in exI, 
            intro conjI disjI2)
         apply(auto simp add: front_tickFree_append tickFree_def)
      by (rule_tac x="f" in exI) (metis (no_types) filter_filter rangeI)
  next
    case (3 f xx)
    note "3a" = 3
    then show ?case
    proof(cases i. f i  𝒟 (P \ A))
      case True
      with 3 show ?thesis 
      proof(auto simp add:D_Hiding, goal_cases)
        case (1 i ta ua)
        then show ?case 
        apply (rule_tac x=ta in exI, rule_tac x="trace_hide ua (ev ` B) @ u" in exI, intro conjI)
           apply (metis (full_types) front_tickFree_append Hiding_tickFree tickFree_append)
          apply(subgoal_tac "trace_hide (f xx) (ev ` B) = trace_hide (f i) (ev ` B)", auto)
         apply (metis (full_types) filter_append filter_filter)
        by (metis (full_types) filter_append filter_filter)
      next
        case (2 i ua fa xa)
        hence "trace_hide (f xx) (ev ` B) = trace_hide (f i) (ev ` B)" by metis
        with 2 show ?case
          apply (rule_tac x="fa xa" in exI, rule_tac x="trace_hide ua (ev ` B) @ u" in exI, intro conjI)
             apply (metis (full_types) front_tickFree_append Hiding_tickFree tickFree_append)
            apply (simp_all) 
          apply(rule_tac disjI2, rule_tac x=fa in exI, auto)
          by (metis (no_types) filter_filter)      
      qed
    next
      case False
      with 3 have Falsebis:i. (f i  𝒯 (P \ A)  f i  𝒟 (P \ A)) by blast
      with T_Hiding[of P A] D_Hiding[of P A] 
      have "i. (f i  {trace_hide t (ev ` A) |t. (t, ev ` A)   P})" 
        by (metis (no_types, lifting) UnE)
      hence ff0:"i. (t. f i = trace_hide t (ev ` A)  t  𝒯 P)" using F_T by fastforce
      define ff where ff1:"ff = (λi. SOME t. f i = trace_hide t (ev ` A)  t  𝒯 P)"
      hence "inj ff" unfolding inj_def by (metis (mono_tags, lifting) "3"(4) ff0 strict_mono_eq tfl_some)
      hence ff2:"infinite (range ff)" using finite_imageD by blast
      { fix tt i
        assume "tt  range ff"
        then obtain k where "ff k = tt" using finite_nat_set_iff_bounded_le by blast
        hence kk0:"f k = trace_hide tt (ev ` A)  tt  𝒯 P" using ff1 
          by (metis (mono_tags, lifting) ff0 someI_ex)
        hence "set (take i tt)  set (f i)  (ev ` A)"
        proof(cases "k  i")
          case True
          hence "set (f k)  set (f i)" 
            by (metis "3"(4) le_list_def set_append strict_mono_less_eq sup.cobounded1)
          moreover from kk0 have "set (take i tt)  set (f k)  (ev ` A)" using in_set_takeD by fastforce
          ultimately show ?thesis by blast
        next
          case False
          have a:"length (f i)  i" by (meson "3"(4) dual_order.trans le_add1 length_strict_mono)
          have b:"f i  f k" using "3"(4) False nat_le_linear strict_mono_less_eq by blast
          with a have c:"take i (f k)  (f i)"
            by (metis append_eq_conv_conj le_add_diff_inverse le_list_def take_add)
          from kk0[THEN conjunct1] have c1:"f k = (trace_hide (take i tt) (ev ` A)) @
                                                  (trace_hide (drop i tt) (ev ` A))"
            by (metis append_take_drop_id filter_append)
          have "length (trace_hide (take i tt) (ev ` A))  i"
            by (metis length_filter_le length_take min.absorb2 nat_le_linear order.trans take_all)
          with c1 have "take i (f k)  (trace_hide (take i tt) (ev ` A))" by (simp add: le_list_def)
          with c obtain t where d:"f i = (trace_hide (take i tt) (ev ` A))@t"
            by (metis append.assoc le_list_def)
          then show ?thesis using in_set_takeD by fastforce
        qed
      } note ee=this
      { fix i
        have "finite {(take i t)|t. t  range ff}" 
        proof(induct i, simp)
          case (Suc i)
          have ff:"{take (Suc i) t|t. t  range ff}  {(take i t)|t. t  range ff} 
                      (e(set (f (Suc i))  (ev ` A)). {(take i t)@[e]|t. t  range ff})" (is "?AA  ?BB")
            proof
              fix t
              assume "t  ?AA"
              then obtain t' where hh:"t'  range ff  t = take (Suc i) t'" 
                using finite_nat_set_iff_bounded_le by blast
              with ee[of t'] show "t  ?BB"
                proof(cases "length t' > i")
                  case True
                  hence ii:"take (Suc i) t' = take i t' @ [t'!i]" by (simp add: take_Suc_conv_app_nth)
                  with ee[of t' "Suc i"] have "t'!i  set (f (Suc i))  (ev ` A)" by (simp add: hh)
                  with ii hh show ?thesis by blast
                next
                  case False
                  hence "take (Suc i) t' = take i t'" by fastforce
                  with hh show ?thesis by auto
                qed
            qed
          { fix e 
            have "{x @ [e] |x. t. x = take i t  t  range ff} = {take i t' @ [e] |t'. t'  range ff}"
              by auto
            hence "finite({(take i t') @ [e] |t'. t'range ff})"
              using finite_image_set[of _ "λt. t@[e]", OF Suc] by auto 
          } note gg=this
          have "finite(set (f (Suc i))  (ev ` A))" using 1(1) by simp
          with ff gg Suc show ?case by (metis (no_types, lifting) finite_UN finite_Un finite_subset)
        qed
      } note ff=this
      hence "i. {take i t |t. t  range ff} = {t. t'. t = take i (ff t')}" by auto
      with KoenigLemma[of "range ff"] ff ff2
      obtain f' where gg:"strict_mono (f':: nat  'a event list)  
                                            range f'  {t. t'range ff. t  t'}" by auto
      { fix i
        from gg obtain n where aa:"f' i  ff n" by blast
        have "t. f n = f 0 @ t" by (metis "3a"(4) le0 le_list_def strict_mono_less_eq)
        with mono_trace_hide[OF aa, of A] ff0 ff1 have "t. trace_hide (f' i) (ev ` A)  f 0 @ t" 
          by (metis (mono_tags, lifting) someI_ex)
      } note zz=this
      {
        define ff' where "ff' = (λi. trace_hide (f' i) (ev ` A))"
        with gg have "mono ff'"
          by (rule_tac monoI, simp add: mono_trace_hide strict_mono_less_eq)
        assume aa:"i. trace_hide (f' i) (ev ` A)  f 0"
        with aa mono_constant have "i. ji. ff' j = ff' i" using mono ff' ff'_def by blast
        then obtain m where bb:"jm. ff' j = ff' m" by blast
        have ff' m  𝒟 (P \ A) 
        proof(simp add:D_Hiding, rule_tac x="f' m" in exI, rule_tac x="[]" in exI, 
              intro conjI, simp, goal_cases)
          case 1
          from gg have "f' m < f' (Suc m)" by (meson lessI strict_monoD)
          moreover from gg obtain k where "f' (Suc m)  ff k" by blast
          moreover have "ff k  𝒯 P" by (metis (mono_tags, lifting) ff0 ff1 someI_ex)
          ultimately show ?case
          by (metis NF_NT append_Nil2 front_tickFree_mono is_processT le_list_def less_list_def)
        next
          case 2
          then show ?case unfolding ff'_def by simp
        next
          case 3
          then show ?case
          proof(rule disjI2, rule_tac x="λi. f' (m + i)" in exI, simp_all, intro conjI allI, goal_cases)
            case 1
            show ?case using gg[THEN conjunct1] 
              by (rule_tac strict_monoI, simp add: strict_monoD) 
          next
            case (2 i)
            from gg obtain k where "f' (m + i)  ff k" by blast
            moreover from ff0 ff1 have "ff k  𝒯 P" by (metis (mono_tags, lifting) someI_ex)
            ultimately have "f' (m + i)  𝒯 P" using is_processT3_ST_pref by blast
            then show ?case by (simp add: add.commute)
          next
            case (3 i)
            then show ?case using bb[THEN spec, of "m+i", simplified] unfolding ff'_def by assumption
          next
            case 4
            then show ?case by (metis Nat.add_0_right rangeI) 
          qed
        qed 
        with gg False have "False"
          by (metis (no_types, lifting) Falsebis aa append_Nil2 ff'_def front_tickFree_mono 
                                        is_processT is_processT2_TR le_list_def) 
      }
      with zz obtain m where hh:"trace_hide (f' m) (ev ` A)  f 0"
        unfolding le_list_def by (metis append_eq_append_conv2)
      from ff0 ff1 gg show ?thesis
      proof(auto simp add:T_Hiding, rule_tac x="f' m" in exI, rule_tac x=u in exI, 
                          intro conjI, simp_all add:3(3), goal_cases)
        case 1
        hence "f' m < f' (Suc m)" by (meson lessI strict_monoD)
        moreover from gg obtain k where "f' (Suc m)  ff k" by blast
        moreover have "ff k  𝒯 P" by (metis (mono_tags, lifting) ff0 ff1 someI_ex)
        ultimately show ?case
          by (metis NF_NT append_Nil2 front_tickFree_mono is_processT le_list_def less_list_def)
      next
        case 2
        from gg obtain k where "f' m  ff k" by blast
        with ff0 ff1 mono_trace_hide[of "f' m"] have "trace_hide (f' m) (ev ` A)  f k" 
          by (metis (mono_tags, lifting) someI_ex)
        with mono_trace_hide[OF this, of B] mono_trace_hide[OF hh, of B] 3(6)[THEN spec, of k] 3(6)
        show ?case by (metis (full_types) dual_order.antisym filter_filter)
      next
        case 3 show ?case 
        proof(rule disjI2, rule_tac x="λi. f' (m + i)" in exI, simp_all, intro conjI allI, goal_cases)
          case 1
          then show ?case by (metis Nat.add_0_right rangeI) 
        next
          case 2 with 3(4) show ?case 
            by (rule_tac strict_monoI, simp add: strict_monoD)
        next
          case (3 i)
          from gg obtain k where "f' (m + i)  ff k" by blast
          moreover from ff0 ff1 have "ff k  𝒯 P" by (metis (mono_tags, lifting) someI_ex)
          ultimately have "f' (m + i)  𝒯 P" using is_processT3_ST_pref by blast
          then show ?case by (simp add: add.commute)
        next
          case (4 i)
          from gg obtain k where "f' (m + i)  ff k" by blast
          with ff0 ff1 mono_trace_hide[of "f' (m + i)"] have ll:"trace_hide (f' (m + i)) (ev ` A)  f k" 
            by (metis (mono_tags, lifting) someI_ex)
          { fix a b c assume "(a::'a event list)  b" and "b  c" and "c  a" hence "b = c" by auto}
          note jj=this
          from jj[OF mono_trace_hide[OF hh, of B],
                  OF mono_trace_hide[THEN mono_trace_hide, of "f' m" "f' (m + i)" B A, 
                               OF gg[THEN conjunct1, THEN strict_mono_mono, 
                               THEN monoD, of "m" "m+i", simplified]]]
               mono_trace_hide[OF ll, of B]
          show ?case unfolding "3a"(6) [THEN spec, of k] by simp
        qed
      qed
    qed
  qed
qed

lemma Hiding_Un_D: finite A  𝒟 ((P \ A) \ B) = 𝒟 (P \ (A  B))
  using Hiding_Un_D1 Hiding_Un_D2 by blast
 
subsection‹ Laws ›

lemma mono_Hiding_FD[simp]: P  Q  P \ A  Q \ A
  apply (auto simp: le_ref_def F_Hiding D_Hiding) 
  using F_subset_imp_T_subset by blast+

lemmas mono_Hiding_ref = mono_Hiding

lemma Hiding_Un: finite A  P \ (A  B) = (P \ A) \ B
proof (simp add:Process_eq_spec, intro conjI, unfold F_Hiding, goal_cases)
  case 1
  thus ?case (is "{(s, X). ?A s X}  {(s, X). ?B s} = 
                  {(s, X). (t. (?C1 s t  (t, X  ev ` B)  ?C2  ?C3))}  {(s, X). ?D s}")
  proof(unfold F_Hiding set_eq_subset Un_subset_iff, intro conjI, goal_cases)
    case 1
    then show ?case
      by (auto, metis (no_types) filter_filter image_Un sup_commute sup_left_commute)
  next
    case 2
    then show ?case 
      by (rule_tac Un_mono[of "{}", simplified], insert Hiding_Un_D[of A P B], simp add: D_Hiding)
  next
    case 3
    have "{(s, X). (t. (?C1 s t  (t, X  ev ` B)  ?C2))}  {(s, X). ?A s X}" 
      by (auto, metis (no_types) filter_filter image_Un sup_commute sup_left_commute)
    moreover have "{(s, X). (t. (?C1 s t  (t, X  ev ` B)  ?C3))}  {(s, X). ?B s}"
    proof(auto,goal_cases)
      case (1 ta u)
      then show ?case using Hiding_fronttickFree by blast
    next
      case (2 u f x)
      then show ?case 
         apply(rule_tac x="f x" in exI, rule_tac x="trace_hide u (ev ` B)" in exI, auto)
         using Hiding_fronttickFree apply blast
        apply(erule_tac x=f in allE) by (metis (no_types) filter_filter rangeI)
    qed
    moreover have "{(s, X). (t. (?C1 s t  (t, X  ev ` B)  ?C2  ?C3))} = 
                                  {(s, X). (t. (?C1 s t  (t, X  ev ` B)  ?C2 ))}  
                                  {(s, X). (t. (?C1 s t  (t, X  ev ` B)  ?C3))}" by blast 
    ultimately show ?case by (metis (no_types, lifting) Un_mono) 
  next
    case 4
    then show ?case  
      by (rule_tac Un_mono[of "{}", simplified], insert Hiding_Un_D[of A P B], simp add:D_Hiding)
  qed
next
  case 2
  then show ?case by (simp add: Hiding_Un_D)
qed

lemma Hiding_set_BOT: ( \ A) = 
  apply(auto simp add:Process_eq_spec D_Hiding F_Hiding F_UU D_UU)
        using Hiding_fronttickFree apply blast
       using front_tickFree_append Hiding_tickFree apply blast
      using front_tickFree_append Hiding_tickFree apply blast
     apply (metis (full_types) append_Nil filter.simps(1) tickFree_Nil tickFree_implies_front_tickFree)
    using front_tickFree_append Hiding_tickFree apply blast 
   using front_tickFree_append Hiding_tickFree apply blast
  using tickFree_Nil by fastforce 

lemma Hiding_set_STOP: (STOP \ A) = STOP
  apply(auto simp add:Process_eq_spec D_Hiding F_Hiding F_STOP D_STOP T_STOP)
  by (metis (full_types) lessI less_irrefl strict_mono_eq) +

lemma Hiding_set_SKIP: (SKIP \ A) = SKIP 
  apply(auto simp add:Process_eq_spec D_Hiding F_Hiding F_SKIP D_SKIP T_SKIP split:if_splits)
       apply (metis filter.simps(1) non_tickFree_tick)
      apply (metis (full_types) Hiding_tickFree n_not_Suc_n non_tickFree_tick strict_mono_eq)
     apply (metis (full_types) Hiding_tickFree n_not_Suc_n non_tickFree_tick strict_mono_eq)
    apply (metis event.distinct(1) filter.simps(1) imageE)
   apply (metis event.distinct(1) filter.simps(1) filter.simps(2) imageE)
  by (metis (full_types) Hiding_tickFree n_not_Suc_n non_tickFree_tick strict_mono_eq)

lemma Hiding_set_empty: (P \ {}) = P
  apply(auto simp add:Process_eq_spec D_Hiding F_Hiding is_processT7 is_processT8_S strict_mono_eq)
  by (metis append_Nil2 front_tickFree_implies_tickFree front_tickFree_single is_processT 
            nonTickFree_n_frontTickFree)

subsection‹ Multi-Operators laws  ›

lemma Hiding_Ndet: (P  Q) \ A = ((P \ A)  (Q \ A))  
proof(auto simp add:Process_eq_spec D_Hiding F_Hiding, 
      simp_all add: F_Ndet T_Ndet D_Ndet D_Hiding F_Hiding, goal_cases)
  case (1 b t)
  then show ?case by blast
next
  case (2 b t u)
  then show ?case by blast
next
  case (3 b u f x)
  from 3(4) have A:"infinite ({i. f i  𝒯 P})  infinite ({i. f i  𝒯 Q})"
    using finite_nat_set_iff_bounded by auto
  hence "(i. f i  𝒯 P)  (i. f i  𝒯 Q)" 
    by (metis (no_types, lifting) 3(3) finite_nat_set_iff_bounded 
            is_processT3_ST_pref mem_Collect_eq not_less strict_mono_less_eq)
  with A show ?case by (metis (no_types, lifting) 3(1,2,3,5) rangeI)
next
  case (4 a b)
  then show ?case by blast
next
  case (5 t u)
  then show ?case by blast
next
  case (6 u f x)
  from 6(4) have A:"infinite ({i. f i  𝒯 P})  infinite ({i. f i  𝒯 Q})"
    using finite_nat_set_iff_bounded by auto
  hence "(i. f i  𝒯 P)  (i. f i  𝒯 Q)" 
    by (metis (no_types, lifting) 6(3) finite_nat_set_iff_bounded 
            is_processT3_ST_pref mem_Collect_eq not_less strict_mono_less_eq)
  with A show ?case by (metis (no_types, lifting) 6(1,2,3,5) rangeI)
next
  case (7 x)
  then show ?case by blast
qed

lemma Hiding_Mprefix_distr: 
  (B  A) = {}  ((Mprefix A P) \ B) = (Mprefix A (λx. ((P x) \ B)))
proof (auto simp add: Process_eq_spec, 
     simp_all add: F_Mprefix T_Mprefix D_Mprefix D_Hiding F_Hiding,
     goal_cases)
  case (1 x b) then show ?case
  proof(elim exE disjE conjE, goal_cases)
    case (1 t)
    then show ?case by (simp add: inf_sup_distrib2)
  next
    case (2 t a)
    then show ?case 
      by (metis (no_types, lifting) disjoint_iff_not_equal event.inject filter.simps(2) 
                                    imageE list.sel(1) list.sel(3) list.collapse neq_Nil_conv)
  next
    case (3 t u a)    
    hence "hd t  ev ` B" by force
    with 3 have"x = hd t # trace_hide (tl t) (ev ` B) @ u"
      by (metis append_Cons filter.simps(2) list.exhaust_sel)
    with 3 show ?case by (metis list.distinct(1) list.sel(1) list.sel(3) tickFree_tl) 
  next
    case (4 t u f)
    then obtain k where kk:"t = f k" by blast
    from 4 obtain a where "f 1  []  ev a = hd (f 1)" and aa:"a  A"
      by (metis less_numeral_extra(1) nil_le not_less strict_mono_less_eq) 
    with 4(1) 4(6)[THEN spec, of 0] 4(7)[THEN spec, of 1] have "f 0  []  hd (f 0) = ev a" 
      apply auto 
        apply (metis (no_types, lifting) disjoint_iff_not_equal event.inject 
                                         filter.simps(2) hd_Cons_tl imageE list.distinct(1))
       apply (metis (no_types, lifting) disjoint_iff_not_equal event.inject filter.simps(2) 
                                        hd_Cons_tl imageE list.distinct(1)) 
      by (metis (no_types, lifting) disjoint_iff_not_equal event.inject filter.simps(2)
                                    hd_Cons_tl imageE list.sel(1))
    with 4(1, 7) aa have nf: "i. f i  []  hd (f i) = ev a"    
      by (metis (mono_tags, opaque_lifting) "4"(5) append_Cons le_list_def le_simps(2) list.distinct(1) 
                list.exhaust_sel list.sel(1) neq0_conv old.nat.distinct(1) strict_mono_less_eq) 
    with 4(5) have sm:"strict_mono (tl  f)" by (simp add: less_tail strict_mono_def)
    with 4 aa kk nf show ?case
      apply(rule_tac disjI2, intro conjI) 
        apply (metis (no_types, lifting) Nil_is_append_conv disjoint_iff_not_equal event.inject 
                                          filter.simps(2) hd_Cons_tl imageE list.distinct(1))
       apply (metis (no_types, lifting) disjoint_iff_not_equal event.inject filter.simps(2) 
                                        hd_Cons_tl hd_append2 image_iff list.distinct(1) list.sel(1))
      apply(rule_tac x=a in exI, intro conjI disjI2) 
       apply (metis disjoint_iff_not_equal event.inject filter.simps(2) 
                    hd_Cons_tl hd_append2 image_iff list.distinct(1) list.sel(1))
     apply(rule_tac x="tl t" in exI, rule_tac x="u" in exI, intro conjI, simp_all) 
        apply (metis tickFree_tl)
       apply (metis (no_types, lifting) disjoint_iff_not_equal event.inject filter.simps(2) 
                                        hd_Cons_tl imageE list.distinct(1) list.sel(3) tl_append2)
      apply(subst disj_commute, rule_tac disjCI)
      apply(rule_tac x="tl  f" in exI, intro conjI)
         apply auto         
      apply (metis (no_types, lifting) filter.simps(2) hd_Cons_tl list.sel(3))
      done
  qed
next
  case (2 x b)
  then show ?case proof(elim exE disjE conjE, goal_cases)
    case 1 then show ?case 
      apply(rule_tac disjI1, rule_tac x="[]" in exI) 
      by (simp add: disjoint_iff_not_equal inf_sup_distrib2)
  next
    case (2 a t) then show ?case 
      apply(rule_tac disjI1, rule_tac  x="(ev a)#t" in exI) 
      using list.collapse by fastforce
  next
    case (3 a t u)
    then show ?case 
      apply(rule_tac disjI2, rule_tac  x="(ev a)#t" in exI, rule_tac x=u in exI) 
      using list.collapse by fastforce
  next
    case (4 a t u f)
    then show ?case 
      apply(rule_tac disjI2)        
      apply(rule_tac x="(ev a) # t" in exI, rule_tac x="u" in exI, intro conjI, simp)
        apply auto[1]
       using hd_Cons_tl apply fastforce
      apply(rule_tac disjI2, rule_tac x="λi. (ev a) # (f i)" in exI)
      by (auto simp add: less_cons strict_mono_def)
  qed
next
  case (3 x) then show ?case
  proof(elim exE disjE conjE, goal_cases)
    case (1 t u a)
    hence aa: "hd (trace_hide t (ev ` B)) = ev a  trace_hide t (ev ` B)  []"
      by (metis (no_types, lifting) disjoint_iff_not_equal event.inject filter.simps(2) hd_Cons_tl 
                                    imageE list.distinct(1) list.sel(1))
    with 1 have  "hd x = ev a  x  []" by simp 
    with 1 show ?case 
      apply(intro conjI, simp_all, rule_tac x=a in exI, simp)
      apply(rule_tac x="tl t" in exI, rule_tac x="u" in exI, intro conjI, simp_all)
       using tickFree_tl apply blast
       using aa by (metis (no_types, lifting) disjoint_iff_not_equal event.inject filter.simps(2) 
                          hd_Cons_tl imageE list.sel(3) tl_append2)
  next
    case (2 t u f)
    then obtain k where kk:"t = f k" by blast
    from 2 obtain a where "f 1  []  ev a = hd (f 1)" and aa:"a  A"
      by (metis less_numeral_extra(1) nil_le not_less strict_mono_less_eq) 
    with 2(1) 2(6)[THEN spec, of 0] 2(7)[THEN spec, of 1] have "f 0  []  hd (f 0) = ev a" 
      apply auto 
        apply (metis (no_types, lifting) disjoint_iff_not_equal event.inject 
                                         filter.simps(2) hd_Cons_tl imageE list.distinct(1))
       apply (metis (no_types, lifting) disjoint_iff_not_equal event.inject filter.simps(2) 
                                        hd_Cons_tl imageE list.distinct(1)) 
      by (metis (no_types, lifting) disjoint_iff_not_equal event.inject filter.simps(2)
                                    hd_Cons_tl imageE list.sel(1))
    with 2(1, 7) aa have nf: "i. f i  []  hd (f i) = ev a"    
      by (metis (mono_tags, opaque_lifting) 2(5) append_Cons le_list_def le_simps(2) list.distinct(1) 
                list.exhaust_sel list.sel(1) neq0_conv old.nat.distinct(1) strict_mono_less_eq) 
    with 2(5) have sm:"strict_mono (tl  f)" by (simp add: less_tail strict_mono_def)
    from 2(1,4) nf aa kk have x1:"x  []"
      by (metis Nil_is_append_conv disjoint_iff_not_equal event.inject filter.simps(2) 
                hd_Cons_tl imageE list.distinct(1))
    with 2(1,4) nf aa kk have x2: "hd (trace_hide t (ev ` B)) = ev a  trace_hide t (ev ` B)  []"
      by (metis (no_types, lifting) disjoint_iff_not_equal event.inject filter.simps(2) hd_Cons_tl 
                                    imageE list.distinct(1) list.sel(1))
    with 2(1,4) nf aa kk x1 have x3:"hd x = ev a" by simp    
    with 2 aa kk nf sm x1  show ?case
      apply(intro conjI, simp_all)
     apply(rule_tac x="tl t" in exI, rule_tac x="u" in exI, intro conjI, simp_all) 
        apply (metis tickFree_tl)
       apply (metis (no_types, lifting) disjoint_iff_not_equal event.inject filter.simps(2) 
                                        hd_Cons_tl imageE list.distinct(1) list.sel(3) tl_append2)
      apply(subst disj_commute, rule_tac disjCI)
      apply(rule_tac x="tl  f" in exI, intro conjI)
         apply auto         
       apply (metis (no_types, lifting) filter.simps(2) hd_Cons_tl list.sel(3))
      by (metis (no_types, lifting) filter.simps(2) hd_Cons_tl list.sel(3))
  qed
next
  case (4 x) then show ?case
  proof(elim exE disjE conjE, goal_cases)
    case (1 a t u)
    then show ?case
      apply(rule_tac  x="(ev a)#t" in exI, rule_tac x=u in exI) 
      using list.collapse by fastforce
  next
    case (2 a t u f) 
    then show ?case 
      apply(rule_tac x="(ev a) # t" in exI, rule_tac x="u" in exI, intro conjI, simp_all)
        apply auto[1]
       using hd_Cons_tl apply fastforce
      apply(rule_tac disjI2, rule_tac x="λi. (ev a) # (f i)" in exI)
      by (auto simp add: less_cons strict_mono_def)
  qed
qed

lemma no_Hiding_read: (y. c y  B)  ((c?x  (P x)) \ B) = (c?x  ((P x) \ B))
  by (simp add: read_def o_def, subst Hiding_Mprefix_distr, auto)

lemma no_Hiding_write0: a  B  ((a  P) \ B) = (a  (P \ B))
  by (simp add: Hiding_Mprefix_distr write0_def)

lemma Hiding_write0: a  B   ((a  P) \ B) = (P \ B)
proof (auto simp add: write0_def Process_eq_spec, 
       simp_all add: F_Mprefix T_Mprefix D_Mprefix D_Hiding F_Hiding,
       goal_cases)
  case (1 x b)
  then show ?case
    apply(elim exE disjE conjE)
      apply (metis filter.simps(2) hd_Cons_tl image_eqI)
     apply (metis (no_types, lifting) filter.simps(2) image_eqI list.sel(1) 
                                      list.sel(3) neq_Nil_conv tickFree_tl)
  proof(goal_cases)
    case (1 t u f)
    have fS: "strict_mono (f  Suc)" by (metis "1"(5) Suc_mono comp_def strict_mono_def)
    from  1 have aa:"i. f (Suc i)  []"
      by (metis (full_types) less_Suc_eq_le less_irrefl nil_le strict_mono_less_eq)      
    with fS have sm:"strict_mono (tl  f  Suc)" by (simp add: less_tail strict_mono_def)
    with 1 aa show ?case
      apply(subst disj_commute, rule_tac disjCI, simp)        
      apply(rule_tac x="tl (f 1)" in exI, rule_tac x="u" in exI, intro conjI, simp_all) 
        apply (metis Hiding_tickFree imageE tickFree_tl)
      apply (metis (no_types, lifting) filter.simps(2) hd_Cons_tl image_eqI rangeE)
      apply(subst disj_commute, rule_tac disjCI)        
      apply(rule_tac x="tl  f  Suc" in exI, intro conjI)
         apply auto
         apply (metis (no_types, lifting) filter.simps(2) hd_Cons_tl list.sel(3))
      done
  qed
next
  case (2 aa b)
  then show ?case     
    apply(elim exE disjE conjE)
      apply (metis (no_types, lifting) filter.simps(2) image_eqI list.distinct(1) 
                                        list.sel(1) list.sel(3))
  proof(goal_cases)
    case (1 t u)
    then show ?case by (rule_tac disjI2, rule_tac x="(ev a)#t" in exI, auto)
  next
    case (2 t u f)
    then show ?case
      apply(rule_tac disjI2)         
      apply(rule_tac x="(ev a) # t" in exI, rule_tac x="u" in exI, intro conjI, simp_all)
      apply(rule_tac disjI2)       
      apply(rule_tac x="λi. (ev a) # (f i)" in exI, intro conjI)
      by (auto simp add: less_cons strict_mono_def)
  qed
next
  case (3 x)
  then show ?case 
    apply(elim exE disjE conjE)
     apply(rule_tac x="tl t" in exI, rule_tac x="u" in exI, intro conjI, simp_all)
    using tickFree_tl apply blast
     apply (metis filter.simps(2) hd_Cons_tl image_eqI)
  proof(goal_cases)
    case (1 t u f)
    have fS: "strict_mono (f  Suc)" by (metis "1"(5) Suc_mono comp_def strict_mono_def)
    from  1 have aa:"i. f (Suc i)  []"
      by (metis (full_types) less_Suc_eq_le less_irrefl nil_le strict_mono_less_eq)      
    with fS have sm:"strict_mono (tl  f  Suc)" by (simp add: less_tail strict_mono_def)
    with 1 aa show ?case
      apply(rule_tac x="tl (f 1)" in exI, rule_tac x="u" in exI, intro conjI, simp_all) 
        apply (metis Hiding_tickFree imageE tickFree_tl)
      apply (metis (no_types, lifting) filter.simps(2) hd_Cons_tl image_eqI rangeE)
      apply(subst disj_commute, rule_tac disjCI)        
      apply(rule_tac x="tl  f  Suc" in exI, intro conjI)
         apply auto
         apply (metis (no_types, lifting) filter.simps(2) hd_Cons_tl list.sel(3))
      done
  qed
next
  case (4 x)
  then show ?case
    apply(elim exE disjE conjE)
  proof(goal_cases)
    case (1 t u)
    then show ?case by (rule_tac x="(ev a)#t" in exI, auto)
  next
    case (2 t u f)
    then show ?case
      apply(rule_tac x="(ev a) # t" in exI, rule_tac x="u" in exI, intro conjI, simp_all)
      apply(rule_tac disjI2)       
      apply(rule_tac x="λi. (ev a) # (f i)" in exI, intro conjI)
      by (auto simp add: less_cons strict_mono_def)
  qed
qed

lemma no_Hiding_write: (y. c y  B)  ((c!a  P) \ B) = (c!a  (P \ B))
  by(simp add: write_def, subst Hiding_Mprefix_distr, auto)

lemma Hiding_write: (c a)  B  ((c!a  P) \ B) = (P \ B)
  by (simp add: write_def Hiding_write0 Mprefix_singl)


section‹ The Sync Operator Laws ›  

subsection‹ Preliminaries ›

lemma SyncTlEmpty:"a setinterleaves (([], u), A)  tl a setinterleaves (([], tl u), A)"
  by (case_tac u, simp, case_tac a, simp_all split:if_splits)

lemma SyncHd_Tl: 
   "a setinterleaves ((t, u), A)  hd t  A  hd u  A
     hd a = hd u  tl a setinterleaves ((t, tl u), A)"
  by (case_tac u) (case_tac t, auto split:if_splits)+
 
lemma SyncHdAddEmpty: 
   "(tl a) setinterleaves (([], u), A)  hd a  A  a  [] 
     a setinterleaves (([], hd a # u), A)"  
  using hd_Cons_tl by fastforce 

lemma SyncHdAdd: 
  "(tl a) setinterleaves ((t, u), A)  hd a  A  hd t  A  a  [] 
    a setinterleaves ((t, hd a # u), A)" 
  by (case_tac a, simp, case_tac t, auto) 

lemmas SyncHdAdd1 = SyncHdAdd[of "a#r", simplified] for a r

lemma SyncSameHdTl:
  "a setinterleaves ((t, u), A)  hd t  A  hd u  A
    hd t = hd u  hd a = hd t  (tl a) setinterleaves ((tl t, tl u), A)"
  by (case_tac u) (case_tac t, auto split:if_splits)+

lemma SyncSingleHeadAdd: 
   "a setinterleaves ((t, u), A)  h  A
     (h#a) setinterleaves ((h#t, u), A)"
  by (case_tac u, auto split:if_splits)

lemma TickLeftSync:
   "tick  A  front_tickFree t  s setinterleaves (([tick], t), A)  s = t  last t = tick"
proof(induct t arbitrary: s)
  case Nil
  then show ?case by (simp add: Nil.prems)
next
  case (Cons a t)
  then show ?case
    apply (auto split:if_splits)
      using emptyLeftProperty apply blast
     apply (metis last_ConsR last_snoc nonTickFree_n_frontTickFree tickFree_Cons)
    by (metis append_Cons append_Nil front_tickFree_mono)+
qed  
  
lemma EmptyLeftSync:"s setinterleaves (([], t), A)  s = t  set t  A = {}"
  by (meson Int_emptyI emptyLeftNonSync emptyLeftProperty)

lemma tick_T_F:"t@[tick]  𝒯 P  (t@[tick], X)   P"
  using append_T_imp_tickFree is_processT5_S7 by force

lemma event_set: "(e::'a event)  insert tick (range ev)"
  by (metis event.exhaust insert_iff rangeI)

lemma Mprefix_Sync_distr1_D: 
  " A  S 
     B  S 
      𝒟 (Mprefix A P S Mprefix B Q) =  𝒟 ( x   A  B  (P x S Q x))"  
  apply(auto,simp_all add:D_Sync F_Sync F_Mprefix T_Mprefix D_Mprefix)  
   apply(elim exE disjE conjE)  
          apply (metis (no_types, lifting) Sync.sym empty_iff image_iff insertI2 
                       list.exhaust_sel setinterleaving.simps(2) subsetCE)
proof(goal_cases)
  case (1 x t u r v a aa)
  from 1(1,2,6,8,11,13) have aa1: "hd tinsert tick (ev ` S)hd uinsert tick (ev ` S)"   
    by blast
  from 1(5,6,7,8,11,13) aa1 have aa2: " hd x  ev ` (A  B)"  
    by (metis (no_types, lifting) IntI empty_setinterleaving event.inject 
                                  hd_append2 image_iff SyncSameHdTl)
  then show ?case  
    using 1(3,4,5,6,7,9,10,13,14) by (metis (no_types, lifting)  Nil_is_append_conv aa1 
                                            empty_setinterleaving event.inject hd_append2 
                                            SyncSameHdTl tickFree_tl tl_append2)
next
  case (2 x t u r v a)
  then show ?case      
    by (metis (no_types, lifting) Sync.si_empty3 equals0D imageE image_eqI insertI2 list.exhaust_sel subsetCE) 
next
  case (3 x t u r v a aa)
  from 3(1,2,6,8,11,13) have aa1: "hd tinsert tick (ev ` S)hd uinsert tick (ev ` S)"   
    by blast
  from 3(5,6,7,8,11,13) aa1 have aa2: " hd x  ev ` (A  B)"  
    by (metis (no_types, lifting) IntI empty_setinterleaving event.inject hd_append2 image_iff SyncSameHdTl)
  then show ?case 
    using 3(3,4,5,6,7,9,10,13,14) 
    by (metis (no_types, lifting)  Nil_is_append_conv aa1 empty_setinterleaving event.inject 
                                   hd_append2 SyncSameHdTl  tickFree_tl tl_append2) 
next
  case (4 x t u r v a)
  then show ?case        
    by (metis (no_types, lifting) Sync.si_empty3 equals0D imageE image_eqI insertI2 list.exhaust_sel subsetCE)  
next
  case (5 x t u r v a aa)
  from 5(1,2,6,8,11,13) have aa1: "hd tinsert tick (ev ` S)hd uinsert tick (ev ` S)"   
    by blast
  from 5(5,6,7,8,11,13) aa1 have aa2: " hd x  ev ` (A  B)"  
    by (metis (no_types, lifting) IntI empty_setinterleaving event.inject hd_append2 image_iff SyncSameHdTl)
  then show ?case 
    using 5(3,4,5,6,7,9,10,13,14) by (metis  aa1 append_Nil2 empty_setinterleaving event.inject SyncSameHdTl)   
next
  case (6 x t u r v a)
  then show ?case       
    by (metis (no_types, lifting) Sync.si_empty3 equals0D imageE image_eqI insertI2 list.exhaust_sel subsetCE) 
next
  case (7 x t u r v a aa)
  from 7(1,2,6,8,11,13) have aa1: "hd tinsert tick (ev ` S)hd uinsert tick (ev ` S)"   
    by blast
  from 7(5,6,7,8,11,13) aa1 have aa2: " hd x  ev ` (A  B)"  
    by (metis (no_types, lifting) IntI empty_setinterleaving event.inject hd_append2 image_iff SyncSameHdTl)
  then show ?case  
      using 7(3,4,5,6,7,9,10,13,14) by (metis  aa1 append_Nil2 empty_setinterleaving event.inject SyncSameHdTl) 
next
  case (8 x)
  then show ?case 
    apply(elim exE disjE conjE)  
  proof(goal_cases)
    case (1 a t u r v)
    obtain r1 t1 u1 where aa0: "r1=hd x#rt1=hd x#tu1=hd x#u" 
      by auto
    from 1(3,4,5,7,8,9) have aa1: "tickFree r1x = r1 @ v" 
      by (metis  Cons_eq_appendI aa0 event.distinct(1) list.exhaust_sel tickFree_Cons)
    from 1(2,4,9) have aa2: "r1 setinterleaves ((t1, u1), insert tick (ev ` S))t1  []"   
      using aa0 subsetCE by auto
    from 1(4,5,10,11) aa0 
    have aa3: "(tl t1)  𝒟 (P a)  (tl u1)  𝒯 (Q a)  ev a = hd t1  ev a = hd u1