Theory CSP_F_law_DIV

           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2005         |
            |               December 2005               |
            |                  April 2006  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_F_law_DIV = CSP_F_law_basic + CSP_T_law_DIV:

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

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

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

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

lemma cspF_DIV_Parallel: 
   "DIV |[X]| DIV =F DIV"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_DIV_Parallel)
apply (rule order_antisym)
apply (rule, simp add: in_failures)+
done

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

lemma cspF_DIV_Parallel_step_l:
   "DIV |[X]| (? :Y -> Qf) =F (? x:(Y-X) -> (DIV |[X]| Qf x)) [+] DIV"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_DIV_Parallel_step_l)
apply (rule order_antisym)

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

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

lemma cspF_DIV_Parallel_step_r:
   "(? :Y -> Qf) |[X]| DIV =F (? x:(Y-X) -> (Qf x |[X]| DIV)) [+] DIV"
apply (rule cspF_rw_left)
apply (rule cspF_commut)
apply (rule cspF_rw_right)
apply (rule cspF_decompo)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_commut)
apply (rule cspF_reflex)
apply (rule cspF_DIV_Parallel_step_l)
done

lemmas cspF_DIV_Parallel_step = 
       cspF_DIV_Parallel_step_l cspF_DIV_Parallel_step_r

(*********************************************************
                      DIV and Parallel
 *********************************************************)

lemma cspF_DIV_Parallel_Ext_choice_DIV_l:
  "(P [+] DIV) |[X]| DIV =F (P |[X]| DIV)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_DIV_Parallel_Ext_choice_DIV_l)
apply (rule order_antisym)

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

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

lemma cspF_DIV_Parallel_Ext_choice_DIV_r:
  "DIV |[X]| (P [+] DIV) =F (DIV |[X]| P)"
apply (rule cspF_rw_left)
apply (rule cspF_commut)
apply (rule cspF_rw_left)
apply (rule cspF_DIV_Parallel_Ext_choice_DIV_l)
apply (rule cspF_commut)
done

lemmas cspF_DIV_Parallel_Ext_choice_DIV =
       cspF_DIV_Parallel_Ext_choice_DIV_l
       cspF_DIV_Parallel_Ext_choice_DIV_r

(*********************************************************
                      DIV -- X
 *********************************************************)

lemma cspF_DIV_Hiding_Id: 
   "DIV -- X =F DIV"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_DIV_Hiding_Id)
apply (rule order_antisym)

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

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

(*** div-hide-step ***)

lemma cspF_DIV_Hiding_step:
  "((? :Y -> Pf) [+] DIV) -- X =F
   (((? x:(Y-X) -> (Pf x -- X)) [+] DIV) |~| (! x:(Y Int X) .. (Pf x -- X)))"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_DIV_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="<Ev a> ^^ sb" 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

(*********************************************************
                      DIV [[r]]
 *********************************************************)

lemma cspF_DIV_Renaming_Id: 
   "DIV [[r]] =F DIV"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_DIV_Renaming_Id)
apply (rule order_antisym)

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

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

(*********************************************************
                       DIV ;; P
 *********************************************************)

lemma cspF_DIV_Seq_compo: "DIV ;; P =F DIV"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_DIV_Seq_compo)
apply (rule order_antisym)

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

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

(*********************************************************
               DIV and Sequential composition
 *********************************************************)

lemma cspF_DIV_Seq_compo_step:
  "((? :X -> Pf) [> DIV) ;; Q =F (? x:X -> (Pf x ;; Q)) [> DIV"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_DIV_Seq_compo_step)
apply (rule order_antisym)

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

 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_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="<Ev a> ^^ sb" in exI)
  apply (rule_tac x="t" in exI)
  apply (simp add: appt_assoc)
done

(*********************************************************
                      DIV |. n
 *********************************************************)

lemma cspF_DIV_Depth_rest: 
   "DIV |. n =F DIV"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_DIV_Depth_rest)
apply (rule order_antisym)

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

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

(*********************************************************
                      cspF_DIV
 *********************************************************)

lemmas cspF_DIV =
       cspF_DIV_Parallel
       cspF_DIV_Parallel_step
       cspF_DIV_Parallel_Ext_choice_DIV
       cspF_DIV_Hiding_Id
       cspF_DIV_Hiding_step
       cspF_DIV_Renaming_Id
       cspF_DIV_Seq_compo
       cspF_DIV_Seq_compo_step
       cspF_DIV_Depth_rest

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

lemma cspF_Ext_choice_DIV_resolve: "P [+] DIV =F P [> DIV"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Ext_choice_DIV_resolve)
apply (rule order_antisym)

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

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

end