Theory CSP_law_SKIP

           (*-------------------------------------------*
            |                CSP-Prover                 |
            |               December 2004               |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_law_SKIP = CSP_law_commut + CSP_law_decompo:

(*  The following simplification is sometimes unexpected.              *)
(*                                                                     *)
(*             not_None_eq: (x ~= None) = (EX y. x = Some y)           *)

declare not_None_eq [simp del]

(*****************************************************************

         1. SKIP ;; P
         2. P ;; SKIP
         3. SKIP |[X]| P
         4. P |[X]| SKIP
         5. SKIP |[X]| SKIP
         6. SKIP -- X
         7. SKIP [[r]]

 *****************************************************************)

(*********************************************************
                       SKIP ;; P
 *********************************************************)

(*** domT ***)

lemma domT_Seq_compo_unit_l: "[[SKIP ;; P]]T ev = [[P]]T ev"
apply (rule eq_iffI)

(* => *)
 apply (rule)
 apply (simp add: Seq_compo_mem)
 apply (simp add: SKIP_mem)
 apply (force)

(* <= *)
 apply (rule)
 apply (simp add: Seq_compo_mem)
 apply (simp add: SKIP_mem)
done

(*** domF ***)

lemma domF_Seq_compo_unit_l: "[[SKIP ;; P]]F ev = [[P]]F ev"
apply (rule eq_iffI)

(* => *)
 apply (rule)
 apply (simp add: Seq_compo_mem)
 apply (simp add: SKIP_mem)
 apply (elim conjE disjE)
 apply (simp_all add: Evset_def)

(* <= *)
 apply (rule)
 apply (simp add: Seq_compo_mem)
 apply (simp add: SKIP_mem)
done

(*** domSF ***)

lemma domSF_Seq_compo_unit_l: "[[SKIP ;; P]]SF ev = [[P]]SF ev"
apply (simp add: proc_eqSF_decompo)
apply (simp add: domT_Seq_compo_unit_l)
apply (simp add: domF_Seq_compo_unit_l)
done

(*------------------*
 |      csp law     |
 *------------------*)

lemma csp_Seq_compo_unit_l: "LET:fp df IN SKIP ;; P =F LET:fp df IN P"
apply (induct_tac fp)
by (simp_all add: eqF_def domSF_Seq_compo_unit_l)

(*********************************************************
                       P ;; SKIP
 *********************************************************)

(*** domT ***)

lemma domT_Seq_compo_unit_r: "[[P ;; SKIP]]T ev = [[P]]T ev"
apply (rule eq_iffI)

(* => *)
 apply (rule)
 apply (simp add: Seq_compo_mem)
 apply (simp add: SKIP_mem)
 apply (elim conjE exE disjE)
 apply (simp)
 apply (rule memT_prefix_closed, simp)
 apply (simp add: rmtick_prefix_rev)
 apply (simp)
 apply (rule memT_prefix_closed, simp, simp)
 apply (simp)

(* <= *)
 apply (rule)
 apply (simp add: Seq_compo_mem)
 apply (simp add: SKIP_mem)
 apply (insert trace_last_notick_or_tick)
 apply (drule_tac x="t" in spec)
 apply (simp add: not_None_T)
 apply (erule disjE)
  apply (rule disjI1)
  apply (rule_tac x="t" in exI, simp)
  (* *)
  apply (rule disjI2)
  apply (elim conjE exE)
  apply (rule_tac x="s" in exI)
  apply (rule_tac x="[Tick]t" in exI)
  apply (simp)
done

(*** domF ***)

lemma domF_Seq_compo_unit_r: "[[P ;; SKIP]]F ev = [[P]]F ev"
apply (rule eq_iffI)

(* => *)
 apply (rule)
 apply (simp add: Seq_compo_mem)
 apply (simp add: SKIP_mem)
 apply (elim conjE exE disjE)
 apply (rule memF_F2, simp, fast)
 apply (rule domSF_F2_F4, simp_all)
 apply (case_tac "notick sa", simp_all)
 apply (rule domSF_T3, simp_all)
 apply (case_tac "notick sa", simp_all)

(* <= *)
 apply (rule)
 apply (simp add: Seq_compo_mem)
 apply (simp add: SKIP_mem)
 apply (insert trace_last_notick_or_tick)
 apply (drule_tac x="s" in spec)
 apply (simp add: not_None_F)
 apply (erule disjE)
  apply (case_tac "Tick : X")
   apply (rule disjI1, simp)
   apply (subgoal_tac "insert Tick X = X", simp, fast)
   (* Tick ~: X *)
   apply (case_tac "s @t [Tick]t ~:t [[P]]T ev")
    apply (rule disjI1, simp)
    apply (rule domSF_F3[of "[[P]]T ev" "[[P]]F ev" _ _ "{Tick}", simplified])
    apply (simp_all)
    (* *)
    apply (rule disjI2)
    apply (rule_tac x="s" in exI)
    apply (rule_tac x="[]t" in exI, simp)
    apply (simp add: Evset_def, fast)
  (* *)
  apply (elim conjE exE, simp)
  apply (rule_tac x="sa" in exI)
  apply (rule_tac x="[Tick]t" in exI)
  apply (simp)
  apply (rule domSF_T2[of _ "[[P]]F ev"], simp_all)
done

(*** domSF ***)

lemma domSF_Seq_compo_unit_r: "[[P ;; SKIP]]SF ev = [[P]]SF ev"
apply (simp add: proc_eqSF_decompo)
apply (simp add: domT_Seq_compo_unit_r)
apply (simp add: domF_Seq_compo_unit_r)
done

(*------------------*
 |      csp law     |
 *------------------*)

lemma csp_Seq_compo_unit_r: "LET:fp df IN P ;; SKIP =F LET:fp df IN P"
apply (induct_tac fp)
by (simp_all add: eqF_def domSF_Seq_compo_unit_r)

(*********************************************************
                      SKIP |[X]| P
 *********************************************************)

(*** domT ***)

lemma domT_Parallel_preterm_l: 
  "[[SKIP |[X]| (? :Y -> Qf)]]T ev = [[? x:(Y-X) -> (SKIP |[X]| Qf x)]]T ev"
apply (rule eq_iffI)

(* => *)
 apply (rule)
 apply (simp add: Parallel_mem)
 apply (simp add: SKIP_mem)
 apply (simp add: Ext_pre_choice_mem)
 apply (insert trace_nil_or_Tick_or_Ev)
 apply (elim disjE conjE exE)
  apply (simp_all)

  apply (drule_tac x="t" in spec)
  apply (simp add: par_tr_not_None)
  apply (erule disjE, simp)
  apply (erule disjE, simp)
  apply (elim conjE exE, simp)
  apply (simp add: par_tr_head)
  apply (simp add: not_None_T)
  apply (rule_tac x="a" in exI)
  apply (rule_tac x="sb" in exI, simp)
  apply (simp add: Parallel_mem SKIP_mem)
  apply (fast)

  apply (drule_tac x="t" in spec)
  apply (simp add: par_tr_not_None)
  apply (erule disjE, simp)
  apply (erule disjE, simp)
  apply (elim conjE exE, simp)
  apply (simp add: par_tr_head)

  apply (drule_tac x="t" in spec)
  apply (simp add: par_tr_not_None)
  apply (erule disjE, simp)
  apply (erule disjE, simp)
  apply (elim conjE exE, simp)
  apply (simp add: par_tr_head)
  apply (simp add: not_None_T)
  apply (rule_tac x="a" in exI)
  apply (rule_tac x="sb" in exI, simp)
  apply (simp add: Parallel_mem SKIP_mem)
  apply (fast)

(* <= *)

 apply (rule)
 apply (simp add: Ext_pre_choice_mem)
 apply (erule disjE, simp)
 apply (simp add: Parallel_mem)
 apply (simp add: SKIP_mem)
 apply (elim disjE conjE exE)
  apply (simp_all)

  apply (rule_tac x="[]t" in exI)
  apply (rule_tac x="[Ev a]t @t ta" in exI, simp)
  apply (simp add: par_tr_head)
  apply (simp add: Ext_pre_choice_mem)
  apply (fast)

  apply (rule_tac x="[Tick]t" in exI)
  apply (rule_tac x="[Ev a]t @t ta" in exI, simp)
  apply (simp add: par_tr_head)
  apply (simp add: Ext_pre_choice_mem)
  apply (fast)
done

(*** domF ***)

lemma domF_Parallel_preterm_l_set1: 
  "[| Ya - insert Tick (Ev ` X) = Z - insert Tick (Ev ` X) ; Ev ` Y Int Z = {} |]
   ==> Ev ` (Y - X) Int (Ya Un Z) = {}"
by (auto)

lemma domF_Parallel_preterm_l: 
  "[[SKIP |[X]| (? :Y -> Qf)]]F ev = [[? x:(Y-X) -> (SKIP |[X]| Qf x)]]F ev"
apply (rule eq_iffI)

(* => *)
 apply (rule)
 apply (simp add: Parallel_mem)
 apply (simp add: SKIP_mem)
 apply (simp add: Ext_pre_choice_mem)
 apply (insert trace_nil_or_Tick_or_Ev)
 apply (elim disjE conjE exE)
  apply (simp_all)

  apply (simp add: domF_Parallel_preterm_l_set1)

  apply (drule_tac x="s" in spec)
  apply (simp add: par_tr_not_None)
  apply (erule disjE, simp)
  apply (erule disjE, simp)
  apply (elim conjE exE, simp)
  apply (simp add: par_tr_head)
  apply (simp add: not_None_F)
  apply (simp add: Parallel_mem SKIP_mem)
  apply (fast)

  apply (drule_tac x="s" in spec)
  apply (simp add: par_tr_not_None)
  apply (erule disjE, simp)
  apply (erule disjE, simp)
  apply (elim conjE exE, simp)
  apply (simp add: par_tr_head)

  apply (drule_tac x="s" in spec)
  apply (simp add: par_tr_not_None)
  apply (erule disjE, simp)
  apply (erule disjE, simp)
  apply (elim conjE exE, simp)
  apply (simp add: par_tr_head)
  apply (simp add: not_None_F)
  apply (simp add: Parallel_mem SKIP_mem)
  apply (fast)

(* <= *)
 apply (rule)
 apply (simp add: Ext_pre_choice_mem)
 apply (erule disjE, simp)
  apply (simp add: Parallel_mem)
  apply (rule_tac x="Xa - {Tick}" in exI)
  apply (rule_tac x="Xa - (Ev ` X)" in exI)
  apply (rule conjI, fast)
  apply (rule conjI, fast)

  apply (simp add: SKIP_mem)
  apply (rule conjI)
  apply (simp add: Evset_def, fast)
  apply (simp add: Ext_pre_choice_mem)
  apply (fast)

 (* *)
  apply (simp add: Parallel_mem)
  apply (simp add: SKIP_mem)
  apply (elim disjE conjE exE)
  apply (simp_all)
   apply (rule_tac x="Ya" in exI)
   apply (rule_tac x="Z" in exI, simp)
   apply (rule_tac x="[]t" in exI)
   apply (rule_tac x="[Ev a]t @t t" in exI, simp)
   apply (simp add: par_tr_head)
   apply (simp add: Ext_pre_choice_mem)
   apply (fast)

   apply (rule_tac x="Ya" in exI)
   apply (rule_tac x="Z" in exI, simp)
   apply (rule_tac x="[Tick]t" in exI)
   apply (rule_tac x="[Ev a]t @t t" in exI, simp)
   apply (simp add: par_tr_head)
   apply (simp add: Ext_pre_choice_mem)
   apply (fast)
done

(*** domSF ***)

lemma domSF_Parallel_preterm_l:
  "[[SKIP |[X]| (? :Y -> Qf)]]SF ev = [[? x:(Y-X) -> (SKIP |[X]| Qf x)]]SF ev"
apply (simp add: proc_eqSF_decompo)
apply (simp add: domT_Parallel_preterm_l)
apply (simp add: domF_Parallel_preterm_l)
done

(*------------------*
 |      csp law     |
 *------------------*)

lemma csp_Parallel_preterm_l: 
   "LET:fp df IN SKIP |[X]| (? :Y -> Qf)
 =F LET:fp df IN ? x:(Y-X) -> (SKIP |[X]| Qf x)"
apply (induct_tac fp)
by (simp_all add: eqF_def domSF_Parallel_preterm_l)

(*********************************************************
                      P |[X]| SKIP
 *********************************************************)

lemma csp_Parallel_preterm_r: 
   "LET:fp df IN (? :Y -> Pf) |[X]| SKIP
 =F LET:fp df IN ? x:(Y-X) -> (Pf x |[X]| SKIP)"
apply (rule csp_trans)
apply (rule csp_Parallel_commut)
apply (rule csp_trans)
apply (rule csp_Parallel_preterm_l)
apply (rule csp_rm_head, simp)
apply (rule csp_Parallel_commut)
done

(*********************************************************
                    SKIP |[X]| SKIP
 *********************************************************)

(*** domT ***)

lemma domT_Parallel_term:
  "[[SKIP |[X]| SKIP]]T ev = [[SKIP]]T ev"
apply (rule eq_iffI)

(* => *)
 apply (rule)
 apply (simp add: Parallel_mem)
 apply (simp add: SKIP_mem)
 apply (elim disjE conjE exE)
  apply (simp_all)

  apply (insert trace_nil_or_Tick_or_Ev)
  apply (drule_tac x="t" in spec)
  apply (simp add: par_tr_not_None)
  apply (erule disjE, simp)+
  apply (elim conjE exE, simp)
  apply (simp add: par_tr_head)

  apply (drule_tac x="t" in spec)
  apply (simp add: par_tr_not_None)
  apply (erule disjE, simp)+
  apply (elim conjE exE, simp)
  apply (simp add: par_tr_head)

(* <= *)
 apply (rule)
 apply (simp add: SKIP_mem)
 apply (erule disjE, simp)
 apply (simp add: Parallel_mem)
 apply (simp add: SKIP_mem)
done

(*** domF ***)

lemma domF_Parallel_term:
  "[[SKIP |[X]| SKIP]]F ev = [[SKIP]]F ev"
apply (rule eq_iffI)

(* => *)
 apply (rule)
 apply (simp add: Parallel_mem)
 apply (simp add: SKIP_mem)
 apply (elim disjE conjE exE)
  apply (simp_all)
  apply (fast)

  apply (insert trace_nil_or_Tick_or_Ev)
  apply (drule_tac x="s" in spec)
  apply (simp add: par_tr_not_None)
  apply (erule disjE, simp)+
  apply (elim conjE exE, simp)
  apply (simp add: par_tr_head)

  apply (drule_tac x="s" in spec)
  apply (simp add: par_tr_not_None)
  apply (erule disjE, simp)+
  apply (elim conjE exE, simp)
  apply (simp add: par_tr_head)

(* <= *)
 apply (rule)
 apply (simp add: SKIP_mem)
 apply (erule disjE)
  apply (simp add: Parallel_mem)
  apply (simp add: SKIP_mem)
  apply (fast)
  apply (simp add: Parallel_mem)
  apply (simp add: SKIP_mem)
  apply (fast)
done

(*** domSF ***)

lemma domSF_Parallel_term:
  "[[SKIP |[X]| SKIP]]SF ev = [[SKIP]]SF ev"
apply (simp add: proc_eqSF_decompo)
apply (simp add: domT_Parallel_term)
apply (simp add: domF_Parallel_term)
done

(*------------------*
 |      csp law     |
 *------------------*)

lemma csp_Parallel_term:
   "LET:fp df IN SKIP |[X]| SKIP =F LET:fp df IN SKIP"
apply (induct_tac fp)
by (simp_all add: eqF_def domSF_Parallel_term)

(*********************************************************
                      SKIP -- X
 *********************************************************)

(*** domT ***)

lemma domT_SKIP_Hiding_Id:
  "[[SKIP -- X]]T ev = [[SKIP]]T ev"
apply (rule eq_iffI)

(* => *)
 apply (rule)
 apply (simp add: Hiding_mem)
 apply (simp add: SKIP_mem)
 apply (elim disjE conjE exE)
 apply (simp_all)

(* <= *)
 apply (rule)
 apply (simp add: SKIP_mem)
 apply (erule disjE, simp)
 apply (simp add: Hiding_mem)
 apply (rule_tac x="[Tick]t" in exI)
 apply (simp add: SKIP_mem)
done

(*** domF ***)

lemma domF_SKIP_Hiding_Id:
  "[[SKIP -- X]]F ev = [[SKIP]]F ev"
apply (rule eq_iffI)

(* => *)
 apply (rule)
 apply (simp add: Hiding_mem)
 apply (simp add: SKIP_mem)
 apply (elim disjE conjE exE)
 apply (simp_all)
 apply (fast)

(* <= *)
 apply (rule)
 apply (simp add: SKIP_mem)
 apply (simp add: Hiding_mem)
 apply (simp add: SKIP_mem)
 apply (erule disjE)
  apply (rule_tac x="[]t" in exI)
  apply (simp add: Evset_def, fast)
  apply (rule_tac x="[Tick]t" in exI)
  apply (simp)
done

(*** domSF ***)

lemma domSF_SKIP_Hiding_Id:
  "[[SKIP -- X]]SF ev = [[SKIP]]SF ev"
apply (simp add: proc_eqSF_decompo)
apply (simp add: domT_SKIP_Hiding_Id)
apply (simp add: domF_SKIP_Hiding_Id)
done

(*------------------*
 |      csp law     |
 *------------------*)

lemma csp_SKIP_Hiding_Id: 
   "LET:fp df IN SKIP -- X =F LET:fp df IN SKIP"
apply (induct_tac fp)
by (simp_all add: eqF_def domSF_SKIP_Hiding_Id)

(*********************************************************
                      SKIP [[r]]
 *********************************************************)

(*** domT ***)

lemma domT_SKIP_Renaming_Id:
  "[[SKIP [[r]]]]T ev = [[SKIP]]T ev"
apply (rule eq_iffI)

(* => *)
 apply (rule)
 apply (simp add: Renaming_mem)
 apply (simp add: SKIP_mem)
 apply (elim disjE conjE exE)
 apply (simp_all)

(* <= *)
 apply (rule)
 apply (simp add: SKIP_mem)
 apply (erule disjE, simp)
 apply (simp add: Renaming_mem)
 apply (simp add: SKIP_mem)
done

(*** domF ***)

lemma domF_SKIP_Renaming_Id:
  "[[SKIP [[r]]]]F ev = [[SKIP]]F ev"
apply (rule eq_iffI)

(* => *)
 apply (rule)
 apply (simp add: Renaming_mem)
 apply (simp add: SKIP_mem)
 apply (elim disjE conjE exE)
 apply (simp_all)

(* <= *)
 apply (rule)
 apply (simp add: SKIP_mem)
 apply (simp add: Renaming_mem)
 apply (simp add: SKIP_mem)
 apply (erule disjE)
 apply (simp_all)
done

(*** domSF ***)

lemma domSF_SKIP_Renaming_Id:
  "[[SKIP [[r]]]]SF ev = [[SKIP]]SF ev"
apply (simp add: proc_eqSF_decompo)
apply (simp add: domT_SKIP_Renaming_Id)
apply (simp add: domF_SKIP_Renaming_Id)
done

(*------------------*
 |      csp law     |
 *------------------*)

lemma csp_SKIP_Renaming_Id: 
   "LET:fp df IN SKIP [[r]] =F LET:fp df IN SKIP"
apply (induct_tac fp)
by (simp_all add: eqF_def domSF_SKIP_Renaming_Id)

(****************** to add them again ******************)

declare not_None_eq    [simp]

end