Theory CSP_F_law_SKIP

Up to index of Isabelle/HOL/HOL-Complex/CSP/CSP_T/CSP_F

theory CSP_F_law_SKIP
imports CSP_F_law_basic CSP_T_law_SKIP
begin
           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2004         |
            |               December 2004               |
            |                   July 2005  (modified)   |
            |              September 2005  (modified)   |
            |                                           |
            |        CSP-Prover on Isabelle2005         |
            |               November 2005  (modified)   |
            |                  April 2006  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_F_law_SKIP = CSP_F_law_basic + CSP_T_law_SKIP:

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

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

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

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

lemma cspF_Parallel_term:
   "SKIP |[X]| SKIP =F SKIP"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Parallel_term)
apply (rule order_antisym)

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

(* <= *)
 apply (rule)
 apply (simp add: in_failures)
 apply (erule disjE)
  apply (simp)
  apply (fast)

  apply (simp)
  apply (fast)
done

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

lemma cspF_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 cspF_Parallel_preterm_l: 
   "SKIP |[X]| (? :Y -> Qf) =F ? x:(Y-X) -> (SKIP |[X]| Qf x)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Parallel_preterm_l)
apply (rule order_antisym)

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

  apply (simp add: cspF_Parallel_preterm_l_set1)

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

      (* automatized by "par_tr_nil_Tick" *)

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

(* <= *)
 apply (rule)
 apply (simp add: in_failures)
 apply (erule disjE, simp)
  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 (rule conjI)
  apply (simp add: Evset_def, fast)
  apply (fast)

 (* *)
  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="<>" in exI)
   apply (rule_tac x="<Ev a> ^^ t" in exI, simp)
   apply (simp add: par_tr_head)

   apply (rule_tac x="Ya" in exI)
   apply (rule_tac x="Z" in exI, simp)
   apply (rule_tac x="<Tick>" in exI)
   apply (rule_tac x="<Ev a> ^^ t" in exI, simp)
   apply (simp add: par_tr_head)
done

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

lemma cspF_Parallel_preterm_r: 
   "(? :Y -> Pf) |[X]| SKIP
     =F ? x:(Y-X) -> (Pf x |[X]| SKIP)"
apply (rule cspF_trans)
apply (rule cspF_Parallel_commut)
apply (rule cspF_trans)
apply (rule cspF_Parallel_preterm_l)
apply (rule cspF_rm_head, simp)
apply (rule cspF_Parallel_commut)
done

lemmas cspF_Parallel_preterm = cspF_Parallel_preterm_l cspF_Parallel_preterm_r

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

(* p.288 *)

lemma cspF_SKIP_Parallel_Ext_choice_SKIP_l:
  "((? :Y -> Pf) [+] SKIP) |[X]| SKIP =F 
   (? x:(Y - X) -> (Pf x |[X]| SKIP)) [+] SKIP"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_SKIP_Parallel_Ext_choice_SKIP_l)
apply (rule order_antisym)

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

  apply (rule disjI1)
  apply (blast)

  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 (rule, simp add: in_traces)

  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 (rule, simp add: in_failures)
 apply (elim conjE exE disjE)
 apply (simp_all)

  apply (simp add: in_traces)
  apply (rule_tac x="Xa" in exI)
  apply (rule_tac x="Xa" in exI)
  apply (simp)

  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 (rule_tac x="Xa" in exI)
  apply (rule_tac x="Xa" in exI)
  apply (simp)

  apply (simp add: in_traces)

  apply (rule_tac x="Xa" in exI)
  apply (rule_tac x="Xa" in exI)
  apply (simp)
done

lemma cspF_SKIP_Parallel_Ext_choice_SKIP_r:
  "SKIP |[X]| ((? :Y -> Pf) [+] SKIP)  =F
    (? x:(Y - X) -> (SKIP |[X]| Pf x)) [+] SKIP"
apply (rule cspF_rw_left)
apply (rule cspF_commut)
apply (rule cspF_rw_left)
apply (rule cspF_SKIP_Parallel_Ext_choice_SKIP_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_SKIP =
       cspF_SKIP_Parallel_Ext_choice_SKIP_l
       cspF_SKIP_Parallel_Ext_choice_SKIP_r

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

lemma cspF_SKIP_Hiding_Id: 
   "SKIP -- X =F SKIP"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_SKIP_Hiding_Id)
apply (rule order_antisym)

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

(* <= *)
 apply (rule)
 apply (simp add: in_failures)
 apply (elim disjE conjE exE)
 apply (simp_all)
  apply (rule_tac x="<>" in exI)
  apply (simp add: Evset_def)
  apply (fast)
  apply (rule_tac x="<Tick>" in exI)
  apply (simp)
done

(*********************************************************
                      SKIP and Hiding
 *********************************************************)

(* p.288 version
  "((? :Y -> Pf) [+] SKIP) -- X =F
       IF (Y Int X = {}) THEN ((? x:Y -> (Pf x -- X)) [+] SKIP)
                         ELSE (((? x:(Y-X) -> (Pf x -- X)) [+] SKIP)
                               |~| (! x:(Y Int X) .. (Pf x -- X)))"
*)

lemma cspF_SKIP_Hiding_step:
  "((? :Y -> Pf) [+] SKIP) -- X =F
   (((? x:(Y-X) -> (Pf x -- X)) [+] SKIP) |~| (! x:(Y Int X) .. (Pf x -- X)))"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_SKIP_Hiding_step)
apply (rule order_antisym)

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

  apply (case_tac "a : X")
  apply (simp)
  apply (blast)
  apply (force)

(* <= *)
 apply (rule)

  apply (simp add: in_failures)
  apply (elim conjE exE bexE disjE)
  apply (simp_all)

   apply (rule_tac x="<>" in exI)
   apply (simp add: in_traces)
   apply (simp add: Evset_def)
   apply (fast)

   apply (rule_tac x="<Ev a> ^^ sb" in exI)
   apply (simp)

   apply (rule_tac x="<Tick>" in exI)
   apply (simp)

   apply (simp add: in_traces)

   apply (rule_tac x="<>" in exI)
   apply (simp add: Evset_def)
   apply (fast)

   apply (rule_tac x="<Ev a> ^^ sa" in exI)
   apply (simp)
done

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

lemma cspF_SKIP_Renaming_Id: 
   "SKIP [[r]] =F SKIP"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_SKIP_Renaming_Id)
apply (rule order_antisym)

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

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

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

lemma cspF_Seq_compo_unit_l: "SKIP ;; P =F P"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Seq_compo_unit_l)
apply (rule order_antisym)

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

(* <= *)
 apply (rule, simp add: in_failures)
 apply (rule disjI2)
 apply (rule_tac x="<>" in exI)
 apply (rule_tac x="s" in exI)
 apply (simp add: in_traces)
done

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

lemma cspF_Seq_compo_unit_r: "P ;; SKIP =F P"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Seq_compo_unit_r)
apply (rule order_antisym)

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

(* <= *)
 apply (rule)
 apply (simp add: in_failures)
 apply (insert trace_last_noTick_or_Tick)
 apply (drule_tac x="s" in spec)
 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 ^^ <Tick> ~:t [[P]]T")
    apply (rule disjI1, simp)
    apply (rule domF_F3[of "[[P]]T" "failures P" _ _ "{Tick}", simplified])
    apply (simp_all add: semT_def)
    (* *)
    apply (rule disjI2)
    apply (rule_tac x="s" in exI)
    apply (rule_tac x="<>" 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>" in exI)
  apply (simp)
  apply (rule domF_T2[of _ "failures P"], simp_all)
done

lemmas cspF_Seq_compo_unit = cspF_Seq_compo_unit_l cspF_Seq_compo_unit_r

(*********************************************************
               SKIP and Sequential composition
 *********************************************************)

(* p.141 *)

lemma cspF_SKIP_Seq_compo_step:
  "((? :X -> Pf) [> SKIP) ;; Q =F (? x:X -> (Pf x ;; Q)) [> Q"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_SKIP_Seq_compo_step)
apply (rule order_antisym)

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

 apply (rule disjI2)
 apply (rule disjI1)
 apply (insert trace_nil_or_Tick_or_Ev)
 apply (drule_tac x="sa" in spec)

 apply (elim disjE conjE exE)
  apply (simp_all)
  apply (simp add: appt_assoc)
  apply (rule disjI2)
  apply (rule disjI1)
  apply (rule_tac x="sc" in exI)
  apply (rule_tac x="t" in exI)
  apply (simp)

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

  apply (rule disjI2)
  apply (rule_tac x="<>" in exI)
  apply (rule_tac x="<>" in exI)
  apply (simp)

  apply (rule disjI2)
  apply (rule_tac x="<>" in exI)
  apply (rule_tac x="<>" in exI)
  apply (simp)

  apply (rule disjI2)
  apply (rule_tac x="<Ev a> ^^ sb" in exI)
  apply (rule_tac x="t" in exI)
  apply (simp add: appt_assoc)

  apply (rule disjI2)
  apply (rule_tac x="<>" in exI)
  apply (rule_tac x="s" in exI)
  apply (simp)

  apply (rule disjI2)
  apply (rule_tac x="<>" in exI)
  apply (rule_tac x="<>" in exI)
  apply (simp)
  apply (rule proc_F2_F4)
  apply (simp_all)
done

(*********************************************************
                      SKIP |. n
 *********************************************************)

lemma cspF_SKIP_Depth_rest: 
   "SKIP |. Suc n =F SKIP"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_SKIP_Depth_rest)
apply (rule order_antisym)

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

(* <= *)
 apply (rule)
 apply (simp add: in_failures)
 apply (elim conjE disjE)
 apply (simp)
 apply (simp)
 apply (case_tac "0 < n", simp)
 apply (simp)
 apply (rule_tac x="<>" in exI)
 apply (simp)
done

(*********************************************************
                      cspF_SKIP
 *********************************************************)

lemmas cspF_SKIP =
       cspF_Parallel_term
       cspF_Parallel_preterm
       cspF_SKIP_Parallel_Ext_choice_SKIP
       cspF_SKIP_Hiding_Id
       cspF_SKIP_Hiding_step
       cspF_SKIP_Renaming_Id
       cspF_Seq_compo_unit
       cspF_SKIP_Seq_compo_step
       cspF_SKIP_Depth_rest

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

(* p.141 *)

lemma cspF_Ext_choice_SKIP_resolve: "P [+] SKIP =F P [> SKIP"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Ext_choice_SKIP_resolve)
apply (rule order_antisym)

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

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

end

lemma cspF_Parallel_term: 

  SKIP |[X]| SKIP =F SKIP

lemma cspF_Parallel_preterm_l_set1: 

  [| Ya - insert Tick (Ev ` X) = Z - insert Tick (Ev ` X); Ev ` Y ∩ Z = {} |]
  ==> Ev ` (Y - X) ∩ (Ya ∪ Z) = {}

lemma cspF_Parallel_preterm_l: 

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

lemma cspF_Parallel_preterm_r: 

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

lemmas cspF_Parallel_preterm: 

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

lemmas cspF_Parallel_preterm: 

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

lemma cspF_SKIP_Parallel_Ext_choice_SKIP_l: 

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

lemma cspF_SKIP_Parallel_Ext_choice_SKIP_r: 

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

lemmas cspF_SKIP_Parallel_Ext_choice_SKIP: 

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

lemmas cspF_SKIP_Parallel_Ext_choice_SKIP: 

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

lemma cspF_SKIP_Hiding_Id: 

  SKIP -- X =F SKIP

lemma cspF_SKIP_Hiding_step: 

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

lemma cspF_SKIP_Renaming_Id: 

  SKIP [[r]] =F SKIP

lemma cspF_Seq_compo_unit_l: 

  SKIP ;; P =F P

lemma cspF_Seq_compo_unit_r: 

  P ;; SKIP =F P

lemmas cspF_Seq_compo_unit: 

  SKIP ;; P =F P
  P ;; SKIP =F P

lemmas cspF_Seq_compo_unit: 

  SKIP ;; P =F P
  P ;; SKIP =F P

lemma cspF_SKIP_Seq_compo_step: 

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

lemma cspF_SKIP_Depth_rest: 

  SKIP |. Suc n =F SKIP

lemmas cspF_SKIP: 

  SKIP |[X]| SKIP =F SKIP
  SKIP |[X]| ? :Y -> Qf =F ? x:(Y - X) -> (SKIP |[X]| Qf x)
  ? :Y -> Pf |[X]| SKIP =F ? x:(Y - X) -> (Pf x |[X]| SKIP)
  (? :Y -> Pf [+] SKIP) |[X]| SKIP =F ? x:(Y - X) -> (Pf x |[X]| SKIP) [+] SKIP
  SKIP |[X]| (? :Y -> Pf [+] SKIP) =F ? x:(Y - X) -> (SKIP |[X]| Pf x) [+] SKIP
  SKIP -- X =F SKIP
  (? :Y -> Pf [+] SKIP) -- X =F 
  ? x:(Y - X) -> Pf x -- X [+] SKIP |~| ! x:(Y ∩ X) .. Pf x -- X
  SKIP [[r]] =F SKIP
  SKIP ;; P =F P
  P ;; SKIP =F P
  (? :X -> Pf [> SKIP) ;; Q =F ? x:X -> (Pf x ;; Q) [> Q
  SKIP |. Suc n =F SKIP

lemmas cspF_SKIP: 

  SKIP |[X]| SKIP =F SKIP
  SKIP |[X]| ? :Y -> Qf =F ? x:(Y - X) -> (SKIP |[X]| Qf x)
  ? :Y -> Pf |[X]| SKIP =F ? x:(Y - X) -> (Pf x |[X]| SKIP)
  (? :Y -> Pf [+] SKIP) |[X]| SKIP =F ? x:(Y - X) -> (Pf x |[X]| SKIP) [+] SKIP
  SKIP |[X]| (? :Y -> Pf [+] SKIP) =F ? x:(Y - X) -> (SKIP |[X]| Pf x) [+] SKIP
  SKIP -- X =F SKIP
  (? :Y -> Pf [+] SKIP) -- X =F 
  ? x:(Y - X) -> Pf x -- X [+] SKIP |~| ! x:(Y ∩ X) .. Pf x -- X
  SKIP [[r]] =F SKIP
  SKIP ;; P =F P
  P ;; SKIP =F P
  (? :X -> Pf [> SKIP) ;; Q =F ? x:X -> (Pf x ;; Q) [> Q
  SKIP |. Suc n =F SKIP

lemma cspF_Ext_choice_SKIP_resolve: 

  P [+] SKIP =F P [> SKIP