Theory CSP_T_law_DIV

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

theory CSP_T_law_DIV
imports CSP_T_law_basic
begin

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

theory CSP_T_law_DIV
imports CSP_T_law_basic
begin

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

         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
 *********************************************************)

(* T *)

lemma cspT_DIV_Parallel:
   "DIV |[X]| DIV =T[M1,M2] DIV"
apply (simp add: cspT_semantics)
apply (rule order_antisym)
apply (rule, simp add: in_traces)+
done

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

lemma cspT_DIV_Parallel_step_l:
   "DIV |[X]| (? :Y -> Qf) =T[M,M] (? x:(Y-X) -> (DIV |[X]| Qf x)) [+] DIV"
apply (simp add: cspT_semantics)
apply (rule order_antisym)

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

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

(* <= *)

 apply (rule)
 apply (simp add: in_traces)
 apply (elim disjE conjE exE)
  apply (simp_all)

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

(*** r ***)

lemma cspT_DIV_Parallel_step_r:
  "(? :Y -> Pf) |[X]| DIV =T[M,M] 
   (? x:(Y - X) -> (Pf x |[X]| DIV)) [+] DIV"
apply (rule cspT_rw_left)
apply (rule cspT_commut)
apply (rule cspT_rw_left)
apply (rule cspT_DIV_Parallel_step_l)
apply (rule cspT_rw_left)
apply (rule cspT_decompo)
apply (rule cspT_decompo)
apply (simp)
apply (rule cspT_commut)
apply (rule cspT_reflex)
apply (rule cspT_reflex)
done

lemmas cspT_DIV_Parallel_step = 
       cspT_DIV_Parallel_step_l cspT_DIV_Parallel_step_r

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

lemma cspT_DIV_Parallel_Ext_choice_DIV_l:
  "(P [+] DIV) |[X]| DIV =T[M,M] (P |[X]| DIV)"
apply (simp add: cspT_semantics)
apply (rule order_antisym)

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

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

lemma cspT_DIV_Parallel_Ext_choice_DIV_r:
  "DIV |[X]| (P [+] DIV) =T[M,M] (DIV |[X]| P)"
apply (rule cspT_rw_left)
apply (rule cspT_commut)
apply (rule cspT_rw_left)
apply (rule cspT_DIV_Parallel_Ext_choice_DIV_l)
apply (rule cspT_commut)
done

lemmas cspT_DIV_Parallel_Ext_choice_DIV =
       cspT_DIV_Parallel_Ext_choice_DIV_l
       cspT_DIV_Parallel_Ext_choice_DIV_r

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

lemma cspT_DIV_Hiding_Id: 
   "DIV -- X =T[M1,M2] DIV"
apply (simp add: cspT_semantics)
apply (rule order_antisym)

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

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

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

lemma cspT_DIV_Hiding_step:
  "((? :Y -> Pf) [+] DIV) -- X =T[M,M] 
   (((? x:(Y-X) -> (Pf x -- X)) [+] DIV) |~| (! x:(Y Int X) .. (Pf x -- X)))"
apply (simp add: cspT_semantics)
apply (rule order_antisym)

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

  apply (case_tac "a : X", force)
  apply (force)

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

   apply (force)

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

   apply (force)

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

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

lemma cspT_DIV_Renaming_Id: 
   "DIV [[r]] =T[M1,M2] DIV"
apply (simp add: cspT_semantics)
apply (rule order_antisym)

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

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

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

lemma cspT_DIV_Seq_compo: "DIV ;; P =T[M1,M2] DIV"
apply (simp add: cspT_semantics)
apply (rule order_antisym)

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

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

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

lemma cspT_DIV_Seq_compo_step:
  "((? :X -> Pf) [> DIV) ;; Q =T[M,M] (? x:X -> (Pf x ;; Q)) [> DIV"
apply (simp add: cspT_semantics)
apply (rule order_antisym)

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

 apply (elim conjE exE disjE)
 apply (simp_all)

  apply (rule disjI1)
  apply (fast)

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

  apply (elim disjE conjE exE)
  apply (simp_all)

  apply (simp add: appt_assoc)
  apply (rule disjI2)

  apply (rule_tac x="sb" in exI)
  apply (rule_tac x="ta" in exI)
  apply (simp)

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

 apply (elim conjE exE disjE)
 apply (simp_all)

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

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

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

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


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

lemma cspT_DIV_Depth_rest: 
   "DIV |. n =T[M1,M2] DIV"
apply (simp add: cspT_semantics)
apply (rule order_antisym)

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

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

(*********************************************************
                      cspT_DIV
 *********************************************************)

lemmas cspT_DIV =
       cspT_DIV_Parallel
       cspT_DIV_Parallel_step
       cspT_DIV_Parallel_Ext_choice_DIV
       cspT_DIV_Hiding_Id
       cspT_DIV_Hiding_step
       cspT_DIV_Renaming_Id
       cspT_DIV_Seq_compo
       cspT_DIV_Seq_compo_step
       cspT_DIV_Depth_rest

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

lemma cspT_Ext_choice_DIV_resolve: "P [+] DIV =T[M,M] P [> DIV"
apply (simp add: cspT_semantics)
apply (rule order_antisym)

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

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

end

lemma cspT_DIV_Parallel:

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

lemma cspT_DIV_Parallel_step_l:

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

lemma cspT_DIV_Parallel_step_r:

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

lemma cspT_DIV_Parallel_step:

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

lemma cspT_DIV_Parallel_Ext_choice_DIV_l:

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

lemma cspT_DIV_Parallel_Ext_choice_DIV_r:

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

lemma cspT_DIV_Parallel_Ext_choice_DIV:

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

lemma cspT_DIV_Hiding_Id:

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

lemma cspT_DIV_Hiding_step:

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

lemma cspT_DIV_Renaming_Id:

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

lemma cspT_DIV_Seq_compo:

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

lemma cspT_DIV_Seq_compo_step:

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

lemma cspT_DIV_Depth_rest:

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

lemma cspT_DIV:

  DIV |[X]| DIV =T[M1.0,M2.0] DIV
  DIV |[X]| ? :Y -> Qf =T[M,M] ? x:(Y - X) -> (DIV |[X]| Qf x) [+] DIV
  ? :Y -> Pf |[X]| DIV =T[M,M] ? x:(Y - X) -> (Pf x |[X]| DIV) [+] DIV
  (P [+] DIV) |[X]| DIV =T[M,M] P |[X]| DIV
  DIV |[X]| (P [+] DIV) =T[M,M] DIV |[X]| P
  DIV -- X =T[M1.0,M2.0] DIV
  (? :Y -> Pf [+] DIV) -- X =T[M,M] 
  ? x:(Y - X) -> Pf x -- X [+] DIV |~| ! x:(YX) .. Pf x -- X
  DIV [[r]] =T[M1.0,M2.0] DIV
  DIV ;; P =T[M1.0,M2.0] DIV
  (? :X -> Pf [> DIV) ;; Q =T[M,M] ? x:X -> (Pf x ;; Q) [> DIV
  DIV |. n =T[M1.0,M2.0] DIV

lemma cspT_Ext_choice_DIV_resolve:

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