Theory CSP_F_law_SKIP_DIV (Isabelle2008: June 2008)

           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2004         |
            |               December 2004               |
            |                   July 2005  (modified)   |
            |              September 2005  (modified)   |
            |                                           |
            |        CSP-Prover on Isabelle2005         |
            |               November 2005  (modified)   |
            |                  April 2006  (modified)   |
            |                  March 2007  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_F_law_SKIP_DIV
imports CSP_F_law_SKIP CSP_F_law_DIV CSP_T_law_SKIP_DIV
begin

(*********************************************************
                   (SKIP [+] DIV)
 *********************************************************)

lemma cspF_SKIP_DIV_Ext_choice1: "(SKIP [+] DIV) =F[M1,M2] SKIP"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_SKIP_DIV_Ext_choice)
apply (rule order_antisym)

(* => *)
 apply (rule, simp add: in_traces in_failures)
 apply (force)

(* <= *)
 apply (rule, simp add: in_traces in_failures)
 apply (force)
done

(*********************************************************
                   (DIV [+] SKIP)
 *********************************************************)

lemma cspF_SKIP_DIV_Ext_choice2: "(DIV [+] SKIP) =F[M1,M2] SKIP"
apply (rule cspF_rw_left)
apply (rule cspF_commut)
apply (rule cspF_SKIP_DIV_Ext_choice1)
done

lemmas cspF_SKIP_DIV_Ext_choice =
       cspF_SKIP_DIV_Ext_choice1
       cspF_SKIP_DIV_Ext_choice2

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

lemma cspF_SKIP_DIV_Parallel1:
   "SKIP |[X]| DIV =F[M1,M2] DIV"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_SKIP_DIV_Parallel1)
apply (rule order_antisym)

(* => *)
 apply (rule)
 apply (simp add: in_failures)

(* <= *)
 apply (rule)
 apply (simp add: in_failures)
done

lemma cspF_SKIP_DIV_Parallel2:
   "DIV |[X]| SKIP =F[M1,M2] DIV"
apply (rule cspF_rw_left)
apply (rule cspF_commut)
apply (rule cspF_rw_left)
apply (rule cspF_SKIP_DIV_Parallel1)
apply (rule cspF_reflex)
done

lemmas cspF_SKIP_DIV_Parallel =
       cspF_SKIP_DIV_Parallel1
       cspF_SKIP_DIV_Parallel2
       cspF_Parallel_term
       cspF_DIV_Parallel

(*********************************************************
                 DIV and Parallel-SKIP
 *********************************************************)

(*********************************************************
                      SKIP and Parallel
 *********************************************************)

(*** SKIP and DIV ***)

lemma cspF_DIV_Parallel_Ext_choice_SKIP_l:
  "(P [+] SKIP) |[X]| DIV =F[M,M] (P |[X]| DIV)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_DIV_Parallel_Ext_choice_SKIP_l)
apply (rule order_antisym)
apply (rule, simp add: in_failures)+
done

lemma cspF_DIV_Parallel_Ext_choice_SKIP_r:
  "DIV |[X]| (P [+] SKIP) =F[M,M] (DIV |[X]| P)"
apply (rule cspF_rw_left)
apply (rule cspF_commut)
apply (rule cspF_rw_left)
apply (rule cspF_DIV_Parallel_Ext_choice_SKIP_l)
apply (rule cspF_commut)
done

lemmas cspF_DIV_Parallel_Ext_choice_SKIP =
       cspF_DIV_Parallel_Ext_choice_SKIP_l
       cspF_DIV_Parallel_Ext_choice_SKIP_r

lemmas cspF_DIV_Parallel_Ext_choice =
       cspF_DIV_Parallel_Ext_choice_SKIP
       cspF_DIV_Parallel_Ext_choice_DIV

(*********************************************************
                 SKIP and Parallel-DIV
 *********************************************************)

(*** DIV and SKIP ***)

lemma cspF_SKIP_Parallel_Ext_choice_DIV_l:
  "((? :Y -> Pf) [+] DIV) |[X]| SKIP =F[M,M]
   (? x:(Y - X) -> (Pf x |[X]| SKIP)) [+] DIV"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_SKIP_Parallel_Ext_choice_DIV_l)
apply (rule order_antisym)

(* => *)
 apply (rule, simp add: in_failures)
 apply (elim conjE exE disjE)
 apply (simp_all)

  apply (simp add: par_tr_nil_right)
  apply (elim conjE)
  apply (simp add: image_iff)
  apply (rule_tac x="Ya" in exI)
  apply (rule_tac x="Z" in exI)
  apply (simp)
  apply (rule_tac x="sb" in exI)
  apply (rule_tac x="<>" in exI)
  apply (simp add: par_tr_nil_right)

  apply (simp add: par_tr_Tick_right)
  apply (elim conjE)
  apply (simp add: image_iff)
  apply (rule_tac x="Ya" in exI)
  apply (rule_tac x="Z" in exI)
  apply (simp)
  apply (rule_tac x="sb" in exI)
  apply (rule_tac x="<Tick>" in exI)
  apply (simp add: par_tr_Tick_right)

  apply (simp add: in_traces)

(* <= *)
 apply (rule, simp add: in_failures)
 apply (elim conjE exE disjE)
 apply (simp_all)

  apply (simp add: in_traces)
  apply (rule_tac x="Ya" in exI)
  apply (rule_tac x="Z" in exI)
  apply (simp add: par_tr_nil_right)
  apply (rule_tac x="<Ev a> ^^ sb" in exI)
  apply (rule_tac x="<>" in exI)
  apply (simp add: par_tr_nil_right)
  apply (simp add: image_iff)
  apply (fast)

  apply (rule_tac x="Ya" in exI)
  apply (rule_tac x="Z" in exI)
  apply (simp add: par_tr_Tick_right)
  apply (rule_tac x="<Ev a> ^^ sb" in exI)
  apply (rule_tac x="<Tick>" in exI)
  apply (simp add: par_tr_Tick_right)
  apply (simp add: image_iff)
  apply (fast)

  apply (simp add: in_traces)
  apply (simp add: in_traces)
done

lemma cspF_SKIP_Parallel_Ext_choice_DIV_r:
  "SKIP |[X]| ((? :Y -> Pf) [+] DIV) =F[M,M]
   (? x:(Y - X) -> (SKIP |[X]| Pf x)) [+] DIV"
apply (rule cspF_rw_left)
apply (rule cspF_commut)
apply (rule cspF_rw_left)
apply (rule cspF_SKIP_Parallel_Ext_choice_DIV_l)
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_commut)
apply (rule cspF_reflex)
apply (rule cspF_reflex)
done

lemmas cspF_SKIP_Parallel_Ext_choice_DIV =
       cspF_SKIP_Parallel_Ext_choice_DIV_l
       cspF_SKIP_Parallel_Ext_choice_DIV_r

lemmas cspF_SKIP_Parallel_Ext_choice =
       cspF_SKIP_Parallel_Ext_choice_SKIP
       cspF_SKIP_Parallel_Ext_choice_DIV

(*---------------------------------------------*
 |                 SKIP , DIV                  |
 *---------------------------------------------*)

lemmas cspF_SKIP_DIV_Parallel_step =
       cspF_Parallel_preterm
       cspF_DIV_Parallel_step

lemmas cspF_SKIP_DIV_Parallel_Ext_choice =
       cspF_SKIP_Parallel_Ext_choice
       cspF_DIV_Parallel_Ext_choice

lemmas cspF_SKIP_DIV_Hiding_Id =
       cspF_SKIP_Hiding_Id
       cspF_DIV_Hiding_Id

lemmas cspF_SKIP_DIV_Hiding_step =
       cspF_DIV_Hiding_step
       cspF_SKIP_Hiding_step

lemmas cspF_SKIP_DIV_Renaming_Id =
       cspF_SKIP_Renaming_Id
       cspF_DIV_Renaming_Id

lemmas cspF_SKIP_DIV_Seq_compo =
       cspF_Seq_compo_unit
       cspF_DIV_Seq_compo

lemmas cspF_SKIP_DIV_Seq_compo_step =
       cspF_SKIP_Seq_compo_step
       cspF_DIV_Seq_compo_step

lemmas cspF_SKIP_DIV_Depth_rest =
       cspF_SKIP_Depth_rest
       cspF_DIV_Depth_rest

lemmas cspF_SKIP_DIV =
       cspF_SKIP_DIV_Parallel_step
       cspF_SKIP_DIV_Ext_choice
       cspF_SKIP_DIV_Parallel
       cspF_SKIP_DIV_Parallel_Ext_choice
       cspF_SKIP_DIV_Hiding_Id
       cspF_SKIP_DIV_Hiding_step
       cspF_SKIP_DIV_Renaming_Id
       cspF_SKIP_DIV_Seq_compo
       cspF_SKIP_DIV_Seq_compo_step
       cspF_SKIP_DIV_Depth_rest

(*** resolve ***)

lemmas cspF_Ext_choice_SKIP_DIV_resolve =
       cspF_Ext_choice_SKIP_resolve
       cspF_Ext_choice_DIV_resolve

(*----------------------------------------------*
 |                                              |
 |        for convenienve  (SKIP or DIV)        |
 |                                              |
 *----------------------------------------------*)

(*********************************************************
            (SKIP or DIV [+] SKIP or DIV)
 *********************************************************)

lemma cspF_SKIP_or_DIV_Ext_choice:
  "[| P = SKIP | P = DIV ; Q = SKIP | Q = DIV |] ==>
   (P [+] Q) =F[M1,M2] (if (P = SKIP | Q = SKIP) then SKIP else DIV)"
apply (elim disjE)
apply (simp_all)
apply (rule cspF_rw_left)
apply (rule cspF_Ext_choice_idem)
apply (simp)
apply (simp add: cspF_SKIP_DIV)
apply (simp add: cspF_SKIP_DIV)
apply (rule cspF_rw_left)
apply (rule cspF_Ext_choice_idem)
apply (simp)
done

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

lemma cspF_SKIP_or_DIV_Parallel:
  "[| P = SKIP | P = DIV ; Q = SKIP | Q = DIV |] ==>
   (P |[X]| Q) =F[M1,M2] (if (P = SKIP & Q = SKIP) then SKIP else DIV)"
apply (elim disjE)
apply (simp_all add: cspF_SKIP_DIV)
done

(*********************************************************
                  (SKIP or DIV) and Hiding
 *********************************************************)

lemma cspF_SKIP_or_DIV_Hiding_step:
  "Q = SKIP | Q = DIV ==>
   ((? :Y -> Pf) [+] Q) -- X =F[M,M] 
   (((? x:(Y-X) -> (Pf x -- X)) [+] Q) |~| (! x:(Y Int X) .. (Pf x -- X)))"
apply (erule disjE)
apply (simp_all add: cspF_SKIP_DIV)
done

(*********************************************************
                  SKIP or DIV |. Suc n
 *********************************************************)

lemma cspF_SKIP_or_DIV_Depth_rest: 
   "Q = SKIP | Q = DIV ==> Q |. (Suc n) =F[M1,M2] Q"
apply (erule disjE)
apply (simp_all add: cspF_SKIP_DIV)
done

(*********************************************************
                    P [+] (SKIP or DIV)
 *********************************************************)

lemma cspF_Ext_choice_SKIP_or_DIV_resolve:
  "Q = SKIP | Q = DIV ==> P [+] Q =F[M,M] P [> Q"
apply (erule disjE)
apply (simp_all add: cspF_Ext_choice_SKIP_DIV_resolve)
done

lemmas cspF_SKIP_or_DIV =
       cspF_SKIP_or_DIV_Ext_choice
       cspF_SKIP_or_DIV_Parallel
       cspF_SKIP_or_DIV_Hiding_step
       cspF_SKIP_or_DIV_Depth_rest

       (* no resolv *)

end

lemma cspF_SKIP_DIV_Ext_choice1:

  SKIP [+] DIV =F[M1.0,M2.0] SKIP

lemma cspF_SKIP_DIV_Ext_choice2:

  DIV [+] SKIP =F[M1.0,M2.0] SKIP

lemma cspF_SKIP_DIV_Ext_choice:

  SKIP [+] DIV =F[M1.0,M2.0] SKIP

  DIV [+] SKIP =F[M1.0,M2.0] SKIP

lemma cspF_SKIP_DIV_Parallel1:

  SKIP |[X]| DIV =F[M1.0,M2.0] DIV

lemma cspF_SKIP_DIV_Parallel2:

  DIV |[X]| SKIP =F[M1.0,M2.0] DIV

lemma cspF_SKIP_DIV_Parallel:

  SKIP |[X]| DIV =F[M1.0,M2.0] DIV

  DIV |[X]| SKIP =F[M1.0,M2.0] DIV

  SKIP |[X]| SKIP =F[M1.0,M2.0] SKIP

  DIV |[X]| DIV =F[M1.0,M2.0] DIV

lemma cspF_DIV_Parallel_Ext_choice_SKIP_l:

  (P [+] SKIP) |[X]| DIV =F[M,M] P |[X]| DIV

lemma cspF_DIV_Parallel_Ext_choice_SKIP_r:

  DIV |[X]| (P [+] SKIP) =F[M,M] DIV |[X]| P

lemma cspF_DIV_Parallel_Ext_choice_SKIP:

  (P [+] SKIP) |[X]| DIV =F[M,M] P |[X]| DIV

  DIV |[X]| (P [+] SKIP) =F[M,M] DIV |[X]| P

lemma cspF_DIV_Parallel_Ext_choice:

  (P [+] SKIP) |[X]| DIV =F[M,M] P |[X]| DIV

  DIV |[X]| (P [+] SKIP) =F[M,M] DIV |[X]| P

  (P [+] DIV) |[X]| DIV =F[M,M] P |[X]| DIV

  DIV |[X]| (P [+] DIV) =F[M,M] DIV |[X]| P

lemma cspF_SKIP_Parallel_Ext_choice_DIV_l:

  (? :Y -> Pf [+] DIV) |[X]| SKIP =F[M,M] ? x:(Y - X) -> (Pf x |[X]| SKIP) [+] DIV

lemma cspF_SKIP_Parallel_Ext_choice_DIV_r:

  SKIP |[X]| (? :Y -> Pf [+] DIV) =F[M,M] ? x:(Y - X) -> (SKIP |[X]| Pf x) [+] DIV

lemma cspF_SKIP_Parallel_Ext_choice_DIV:

  (? :Y -> Pf [+] DIV) |[X]| SKIP =F[M,M] ? x:(Y - X) -> (Pf x |[X]| SKIP) [+] DIV

  SKIP |[X]| (? :Y -> Pf [+] DIV) =F[M,M] ? x:(Y - X) -> (SKIP |[X]| Pf x) [+] DIV

lemma cspF_SKIP_Parallel_Ext_choice:

  (? :Y -> Pf [+] SKIP) |[X]| SKIP =F[M,M] 
  ? x:(Y - X) -> (Pf x |[X]| SKIP) [+] SKIP

  SKIP |[X]| (? :Y -> Pf [+] SKIP) =F[M,M] 
  ? x:(Y - X) -> (SKIP |[X]| Pf x) [+] SKIP

  (? :Y -> Pf [+] DIV) |[X]| SKIP =F[M,M] ? x:(Y - X) -> (Pf x |[X]| SKIP) [+] DIV

  SKIP |[X]| (? :Y -> Pf [+] DIV) =F[M,M] ? x:(Y - X) -> (SKIP |[X]| Pf x) [+] DIV

lemma cspF_SKIP_DIV_Parallel_step:

  SKIP |[X]| ? :Y -> Qf =F[M,M] ? x:(Y - X) -> (SKIP |[X]| Qf x)

  ? :Y -> Pf |[X]| SKIP =F[M,M] ? x:(Y - X) -> (Pf x |[X]| SKIP)

  DIV |[X]| ? :Y -> Qf =F[M,M] ? x:(Y - X) -> (DIV |[X]| Qf x) [+] DIV

  ? :Y -> Qf |[X]| DIV =F[M,M] ? x:(Y - X) -> (Qf x |[X]| DIV) [+] DIV

lemma cspF_SKIP_DIV_Parallel_Ext_choice:

  (? :Y -> Pf [+] SKIP) |[X]| SKIP =F[M,M] 
  ? x:(Y - X) -> (Pf x |[X]| SKIP) [+] SKIP

  SKIP |[X]| (? :Y -> Pf [+] SKIP) =F[M,M] 
  ? x:(Y - X) -> (SKIP |[X]| Pf x) [+] SKIP

  (? :Y -> Pf [+] DIV) |[X]| SKIP =F[M,M] ? x:(Y - X) -> (Pf x |[X]| SKIP) [+] DIV

  SKIP |[X]| (? :Y -> Pf [+] DIV) =F[M,M] ? x:(Y - X) -> (SKIP |[X]| Pf x) [+] DIV

  (P [+] SKIP) |[X]| DIV =F[M,M] P |[X]| DIV

  DIV |[X]| (P [+] SKIP) =F[M,M] DIV |[X]| P

  (P [+] DIV) |[X]| DIV =F[M,M] P |[X]| DIV

  DIV |[X]| (P [+] DIV) =F[M,M] DIV |[X]| P

lemma cspF_SKIP_DIV_Hiding_Id:

  SKIP -- X =F[M,M] SKIP

  DIV -- X =F[M1.0,M2.0] DIV

lemma cspF_SKIP_DIV_Hiding_step:

  (? :Y -> Pf [+] DIV) -- X =F[M,M] 
  ? x:(Y - X) -> Pf x -- X [+] DIV |~| ! x:(Y ∩ X) .. Pf x -- X

  (? :Y -> Pf [+] SKIP) -- X =F[M,M] 
  ? x:(Y - X) -> Pf x -- X [+] SKIP |~| ! x:(Y ∩ X) .. Pf x -- X

lemma cspF_SKIP_DIV_Renaming_Id:

  SKIP [[r]] =F[M1.0,M2.0] SKIP

  DIV [[r]] =F[M1.0,M2.0] DIV

lemma cspF_SKIP_DIV_Seq_compo:

  SKIP ;; P =F[M,M] P

  P ;; SKIP =F[M,M] P

  DIV ;; P =F[M1.0,M2.0] DIV

lemma cspF_SKIP_DIV_Seq_compo_step:

  (? :X -> Pf [> SKIP) ;; Q =F[M,M] ? x:X -> (Pf x ;; Q) [> Q

  (? :X -> Pf [> DIV) ;; Q =F[M,M] ? x:X -> (Pf x ;; Q) [> DIV

lemma cspF_SKIP_DIV_Depth_rest:

  SKIP |. Suc n =F[M1.0,M2.0] SKIP

  DIV |. n =F[M1.0,M2.0] DIV

lemma cspF_SKIP_DIV:

  SKIP |[X]| ? :Y -> Qf =F[M,M] ? x:(Y - X) -> (SKIP |[X]| Qf x)

  ? :Y -> Pf |[X]| SKIP =F[M,M] ? x:(Y - X) -> (Pf x |[X]| SKIP)

  DIV |[X]| ? :Y -> Qf =F[M,M] ? x:(Y - X) -> (DIV |[X]| Qf x) [+] DIV

  ? :Y -> Qf |[X]| DIV =F[M,M] ? x:(Y - X) -> (Qf x |[X]| DIV) [+] DIV

  SKIP [+] DIV =F[M1.0,M2.0] SKIP

  DIV [+] SKIP =F[M1.0,M2.0] SKIP

  SKIP |[X]| DIV =F[M1.0,M2.0] DIV

  DIV |[X]| SKIP =F[M1.0,M2.0] DIV

  SKIP |[X]| SKIP =F[M1.0,M2.0] SKIP

  DIV |[X]| DIV =F[M1.0,M2.0] DIV

  (? :Y -> Pf [+] SKIP) |[X]| SKIP =F[M,M] 
  ? x:(Y - X) -> (Pf x |[X]| SKIP) [+] SKIP

  SKIP |[X]| (? :Y -> Pf [+] SKIP) =F[M,M] 
  ? x:(Y - X) -> (SKIP |[X]| Pf x) [+] SKIP

  (? :Y -> Pf [+] DIV) |[X]| SKIP =F[M,M] ? x:(Y - X) -> (Pf x |[X]| SKIP) [+] DIV

  SKIP |[X]| (? :Y -> Pf [+] DIV) =F[M,M] ? x:(Y - X) -> (SKIP |[X]| Pf x) [+] DIV

  (P [+] SKIP) |[X]| DIV =F[M,M] P |[X]| DIV

  DIV |[X]| (P [+] SKIP) =F[M,M] DIV |[X]| P

  (P [+] DIV) |[X]| DIV =F[M,M] P |[X]| DIV

  DIV |[X]| (P [+] DIV) =F[M,M] DIV |[X]| P

  SKIP -- X =F[M,M] SKIP

  DIV -- X =F[M1.0,M2.0] DIV

  (? :Y -> Pf [+] DIV) -- X =F[M,M] 
  ? x:(Y - X) -> Pf x -- X [+] DIV |~| ! x:(Y ∩ X) .. Pf x -- X

  (? :Y -> Pf [+] SKIP) -- X =F[M,M] 
  ? x:(Y - X) -> Pf x -- X [+] SKIP |~| ! x:(Y ∩ X) .. Pf x -- X

  SKIP [[r]] =F[M1.0,M2.0] SKIP

  DIV [[r]] =F[M1.0,M2.0] DIV

  SKIP ;; P =F[M,M] P

  P ;; SKIP =F[M,M] P

  DIV ;; P =F[M1.0,M2.0] DIV

  (? :X -> Pf [> SKIP) ;; Q =F[M,M] ? x:X -> (Pf x ;; Q) [> Q

  (? :X -> Pf [> DIV) ;; Q =F[M,M] ? x:X -> (Pf x ;; Q) [> DIV

  SKIP |. Suc n =F[M1.0,M2.0] SKIP

  DIV |. n =F[M1.0,M2.0] DIV

lemma cspF_Ext_choice_SKIP_DIV_resolve:

  P [+] SKIP =F[M,M] P [> SKIP

  P [+] DIV =F[M,M] P [> DIV

lemma cspF_SKIP_or_DIV_Ext_choice:

  [| P = SKIP ∨ P = DIV; Q = SKIP ∨ Q = DIV |]
  ==> P [+] Q =F[M1.0,M2.0] (if P = SKIP ∨ Q = SKIP then SKIP else DIV)

lemma cspF_SKIP_or_DIV_Parallel:

  [| P = SKIP ∨ P = DIV; Q = SKIP ∨ Q = DIV |]
  ==> P |[X]| Q =F[M1.0,M2.0] (if P = SKIP ∧ Q = SKIP then SKIP else DIV)

lemma cspF_SKIP_or_DIV_Hiding_step:

  Q = SKIP ∨ Q = DIV
  ==> (? :Y -> Pf [+] Q) -- X =F[M,M] 
      ? x:(Y - X) -> Pf x -- X [+] Q |~| ! x:(Y ∩ X) .. Pf x -- X

lemma cspF_SKIP_or_DIV_Depth_rest:

  Q = SKIP ∨ Q = DIV ==> Q |. Suc n =F[M1.0,M2.0] Q

lemma cspF_Ext_choice_SKIP_or_DIV_resolve:

  Q = SKIP ∨ Q = DIV ==> P [+] Q =F[M,M] P [> Q

lemma cspF_SKIP_or_DIV:

  [| P = SKIP ∨ P = DIV; Q = SKIP ∨ Q = DIV |]
  ==> P [+] Q =F[M1.0,M2.0] (if P = SKIP ∨ Q = SKIP then SKIP else DIV)

  [| P = SKIP ∨ P = DIV; Q = SKIP ∨ Q = DIV |]
  ==> P |[X]| Q =F[M1.0,M2.0] (if P = SKIP ∧ Q = SKIP then SKIP else DIV)

  Q = SKIP ∨ Q = DIV
  ==> (? :Y -> Pf [+] Q) -- X =F[M,M] 
      ? x:(Y - X) -> Pf x -- X [+] Q |~| ! x:(Y ∩ X) .. Pf x -- X

  Q = SKIP ∨ Q = DIV ==> Q |. Suc n =F[M1.0,M2.0] Q