Theory CSP_T_law_basic

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

theory CSP_T_law_basic
imports CSP_T_law_decompo
begin

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

         1. Commutativity
         2. Associativity
         3. Idempotence
         4. Left Commutativity
         5. IF

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

(*********************************************************
                       IF bool
 *********************************************************)

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

lemma cspT_IF_split: 
  "IF b THEN P ELSE Q =T[M,M] (if b then P else Q)"
apply (simp add: cspT_semantics)
apply (simp add: traces_def)
done

lemma cspT_IF_True:
  "IF True THEN P ELSE Q =T[M,M] P"
apply (rule cspT_rw_left)
apply (rule cspT_IF_split)
by (simp)

lemma cspT_IF_False:
  "IF False THEN P ELSE Q =T[M,M] Q"
apply (rule cspT_rw_left)
apply (rule cspT_IF_split)
by (simp)

lemmas cspT_IF = cspT_IF_True cspT_IF_False

(*-----------------------------------*
 |           Idempotence             |
 *-----------------------------------*)

lemma cspT_Ext_choice_idem: 
  "P [+] P =T[M,M] P"
apply (simp add: cspT_semantics)
apply (rule order_antisym)
 apply (rule, simp add: in_traces)+
done

lemma cspT_Int_choice_idem: 
  "P |~| P =T[M,M] P"
apply (simp add: cspT_semantics)
apply (rule order_antisym)
 apply (rule, simp add: in_traces)+
done

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

lemmas cspT_idem = cspT_Ext_choice_idem cspT_Int_choice_idem

(*-----------------------------------*
 |          Commutativity            |
 *-----------------------------------*)

(*********************************************************
                      Ext choice
 *********************************************************)

lemma cspT_Ext_choice_commut:
  "P [+] Q =T[M,M] Q [+] P"
apply (simp add: cspT_semantics)
apply (rule order_antisym)
apply (rule, simp add: in_traces, fast)+
done

(*********************************************************
                      Int choice
 *********************************************************)

lemma cspT_Int_choice_commut:
  "P |~| Q =T[M,M] Q |~| P"
apply (simp add: cspT_semantics)
apply (rule order_antisym)
apply (rule, simp add: in_traces, fast)+
done

(*********************************************************
                      Parallel
 *********************************************************)

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

apply (rule, simp add: in_traces)
apply (elim conjE exE)
apply (rule_tac x="ta" in exI)
apply (rule_tac x="s" in exI)
apply (simp add: par_tr_sym)

apply (rule, simp add: in_traces)
apply (elim conjE exE)
apply (rule_tac x="ta" in exI)
apply (rule_tac x="s" in exI)
apply (simp add: par_tr_sym)
done

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

lemmas cspT_commut = cspT_Ext_choice_commut 
                      cspT_Int_choice_commut
                      cspT_Parallel_commut

(*-----------------------------------*
 |          Associativity            |
 *-----------------------------------*)

lemma cspT_Ext_choice_assoc:
  "P [+] (Q [+] R) =T[M,M] (P [+] Q) [+] R"
apply (simp add: cspT_semantics)
apply (rule order_antisym)
apply (rule, simp add: in_traces)+
done

lemma cspT_Ext_choice_assoc_sym:
  "(P [+] Q) [+] R =T[M,M] P [+] (Q [+] R)"
apply (rule cspT_sym)
apply (simp add: cspT_Ext_choice_assoc)
done

lemma cspT_Int_choice_assoc:
  "P |~| (Q |~| R) =T[M,M] (P |~| Q) |~| R"
apply (simp add: cspT_semantics)
apply (rule order_antisym)
apply (rule, simp add: in_traces)+
done

lemma cspT_Int_choice_assoc_sym:
  "(P |~| Q) |~| R =T[M,M] P |~| (Q |~| R)"
apply (rule cspT_sym)
apply (simp add: cspT_Int_choice_assoc)
done

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

lemmas cspT_assoc = cspT_Ext_choice_assoc cspT_Int_choice_assoc
lemmas cspT_assoc_sym = cspT_Ext_choice_assoc_sym cspT_Int_choice_assoc_sym

(*-----------------------------------*
 |        Left Commutativity         |
 *-----------------------------------*)

lemma cspT_Ext_choice_left_commut:
  "P [+] (Q [+] R) =T[M,M] Q [+] (P [+] R)"
apply (simp add: cspT_semantics)
apply (rule order_antisym)
apply (rule, simp add: in_traces)+
done

lemma cspT_Int_choice_left_commut:
  "P |~| (Q |~| R) =T[M,M] Q |~| (P |~| R)"
apply (simp add: cspT_semantics)
apply (rule order_antisym)
apply (rule, simp add: in_traces)+
done

lemmas cspT_left_commut = 
       cspT_Ext_choice_left_commut cspT_Int_choice_left_commut

(*-----------------------------------*
 |              Unit                 |
 *-----------------------------------*)

(*** STOP [+] P ***)

lemma cspT_Ext_choice_unit_l: 
  "STOP [+] P =T[M,M] P"
apply (simp add: cspT_semantics)
apply (rule order_antisym)
 apply (rule, simp add: in_traces)
 apply (force)
 apply (rule, simp add: in_traces)
done

lemma cspT_Ext_choice_unit_r: 
  "P [+] STOP =T[M,M] P"
apply (rule cspT_rw_left)
apply (rule cspT_Ext_choice_commut)
apply (simp add: cspT_Ext_choice_unit_l)
done

lemmas cspT_Ext_choice_unit = 
       cspT_Ext_choice_unit_l cspT_Ext_choice_unit_r

lemma cspT_Int_choice_unit_l: 
  "DIV |~| P =T[M,M] P"
apply (simp add: cspT_semantics)
apply (rule order_antisym)
 apply (rule, simp add: in_traces)
 apply (force)
 apply (rule, simp add: in_traces)
done

lemma cspT_Int_choice_unit_r: 
  "P |~| DIV =T[M,M] P"
apply (rule cspT_rw_left)
apply (rule cspT_Int_choice_commut)
apply (simp add: cspT_Int_choice_unit_l)
done

lemmas cspT_Int_choice_unit = 
       cspT_Int_choice_unit_l cspT_Int_choice_unit_r

lemmas cspT_unit = cspT_Ext_choice_unit cspT_Int_choice_unit

(*-----------------------------------*
 |             !-empty               |
 *-----------------------------------*)

lemma cspT_Rep_int_choice_nat_DIV:
   "!nat :{} .. Pf =T[M1,M2] DIV"
apply (simp add: cspT_semantics)
apply (simp add: traces_def)
done

lemma cspT_Rep_int_choice_set_DIV:
   "!set :{} .. Pf =T[M1,M2] DIV"
apply (simp add: cspT_semantics)
apply (simp add: traces_def)
done

lemma cspT_Rep_int_choice_com_DIV:
   "! :{} .. Pf =T[M1,M2] DIV"
apply (simp add: Rep_int_choice_com_def)
apply (simp add: cspT_Rep_int_choice_set_DIV)
done

lemma cspT_Rep_int_choice_f_DIV:
   "inj f ==> !<f> :{} .. Pf =T[M1,M2] DIV"
apply (simp add: cspT_semantics)
apply (simp add: traces_def)
done

lemmas cspT_Rep_int_choice_DIV = cspT_Rep_int_choice_nat_DIV
                                 cspT_Rep_int_choice_set_DIV
                                 cspT_Rep_int_choice_com_DIV
                                 cspT_Rep_int_choice_f_DIV

lemmas cspT_Rep_int_choice_DIV_sym = cspT_Rep_int_choice_DIV[THEN cspT_sym]
lemmas cspT_Rep_int_choice_empty = cspT_Rep_int_choice_DIV

(*-----------------------------------*
 |             !-unit                |
 *-----------------------------------*)

lemma cspT_Rep_int_choice_traces_unit:
  "Z ~= {} ==> (!traces :Z .. (%z. P)) M = traces P M"
apply (unfold Rep_int_choice_traces_def)
apply (rule order_antisym)
 apply (rule)
 apply (simp only: in_traces)
 apply (force)
 apply (rule)
 apply (simp only: in_traces)
 apply (force)
done

lemma cspT_Rep_int_choice_nat_unit:
  "N ~= {} ==> !nat n:N .. P =T[M,M] P"
apply (simp add: cspT_semantics)
apply (simp add: Rep_int_choice_traces)
apply (simp add: cspT_Rep_int_choice_traces_unit)
done

lemma cspT_Rep_int_choice_set_unit:
  "Xs ~= {} ==> !set X:Xs .. P =T[M,M] P"
apply (simp add: cspT_semantics)
apply (simp add: Rep_int_choice_traces)
apply (simp add: cspT_Rep_int_choice_traces_unit)
done

lemma cspT_Rep_int_choice_com_unit:
  "X ~= {} ==> ! a:X .. P =T[M,M] P"
apply (simp add: cspT_semantics)
apply (simp add: Rep_int_choice_traces)
apply (simp add: cspT_Rep_int_choice_traces_unit)
done

lemma cspT_Rep_int_choice_f_unit:
  "X ~= {} ==> !<f> a:X .. P =T[M,M] P"
apply (simp add: Rep_int_choice_f_def)
apply (simp add: cspT_Rep_int_choice_com_unit)
done

lemmas cspT_Rep_int_choice_unit = 
       cspT_Rep_int_choice_nat_unit
       cspT_Rep_int_choice_set_unit
       cspT_Rep_int_choice_com_unit
       cspT_Rep_int_choice_f_unit

(*-----------------------------------*
 |              !-const              |
 *-----------------------------------*)

(* const *)

lemma cspT_Rep_int_choice_traces_const:
  "[| Z ~= {} ; ALL z:Z. Pf z = P |] ==> (!traces :Z .. Pf) M = traces P M"
apply (unfold Rep_int_choice_traces_def)
apply (rule order_antisym)
 apply (rule)
 apply (simp only: in_traces)
 apply (force)
 apply (rule)
 apply (simp only: in_traces)
 apply (force)
done

lemma cspT_Rep_int_choice_nat_const:
  "[| N ~= {} ; ALL n:N. Pf n = P |] ==> !nat :N .. Pf =T[M,M] P"
apply (simp add: cspT_semantics)
apply (simp add: Rep_int_choice_traces)
apply (simp add: cspT_Rep_int_choice_traces_const)
done

lemma cspT_Rep_int_choice_set_const:
  "[| Xs ~= {} ; ALL X:Xs. Pf X = P |] ==> !set :Xs .. Pf =T[M,M] P"
apply (simp add: cspT_semantics)
apply (simp add: Rep_int_choice_traces)
apply (simp add: cspT_Rep_int_choice_traces_const)
done

lemma cspT_Rep_int_choice_com_const:
  "[| X ~= {} ; ALL a:X. Pf a = P |] ==> ! :X .. Pf =T[M,M] P"
apply (simp add: cspT_semantics)
apply (simp add: Rep_int_choice_traces)
apply (simp add: cspT_Rep_int_choice_traces_const)
done

lemma cspT_Rep_int_choice_f_const:
  "[| inj f ; X ~= {} ; ALL a:X. Pf a = P |] ==> !<f> :X .. Pf =T[M,M] P"
apply (simp add: cspT_semantics)
apply (simp add: Rep_int_choice_traces)
apply (simp add: cspT_Rep_int_choice_traces_const)
done

lemmas cspT_Rep_int_choice_const =
       cspT_Rep_int_choice_nat_const
       cspT_Rep_int_choice_set_const
       cspT_Rep_int_choice_com_const
       cspT_Rep_int_choice_f_const

(*-----------------------------------*
 |            |~|-!-union            |
 *-----------------------------------*)

lemma cspT_Int_Rep_int_choice_traces_union:
  "(!traces :Z1 .. P1f) M UnT (!traces :Z2 .. P2f) M
   = (!traces :(Z1 Un Z2) .. (%z.
          IF (z : Z1 & z : Z2) THEN (P1f z |~| P2f z)
          ELSE IF (z : Z1) THEN P1f z ELSE P2f z)) M"
apply (simp add: Rep_int_choice_traces_def)
apply (rule order_antisym)

 apply (rule)
 apply (simp add: in_traces_Union_proc)
 apply (elim conjE bexE disjE)
 apply (simp_all)
  apply (rule disjI2)
  apply (rule_tac x="z" in bexI)
  apply (simp add: in_traces)
  apply (simp)
  apply (rule disjI2)
  apply (rule_tac x="z" in bexI)
  apply (simp add: in_traces)
  apply (simp)

(* => *)
 apply (rule)
 apply (simp add: in_traces_Union_proc)
 apply (elim conjE exE bexE disjE)
 apply (simp_all)
 apply (elim conjE exE bexE disjE)
 apply (simp_all)
 apply (case_tac "z : Z2")
 apply (simp add: in_traces)
 apply (force)
 apply (simp add: in_traces)
 apply (force)
 apply (case_tac "z : Z1")
 apply (simp add: in_traces)
 apply (force)
 apply (simp add: in_traces)
 apply (force)
done

lemma cspT_Int_Rep_int_choice_nat_union:
  "(!nat :N1 .. P1f) |~| (!nat :N2 .. P2f)
   =T[M,M] (!nat n:(N1 Un N2) ..
          IF (n : N1 & n : N2) THEN (P1f n |~| P2f n)
          ELSE IF (n : N1) THEN P1f n ELSE P2f n)"
apply (simp add: cspT_semantics)
apply (simp add: Rep_int_choice_traces)
apply (subgoal_tac 
  "traces (!nat :N1 .. P1f |~| !nat :N2 .. P2f) M =
   traces (!nat :N1 .. P1f) M UnT traces(!nat :N2 .. P2f) M")
apply (simp add: Rep_int_choice_traces)
apply (simp add: cspT_Int_Rep_int_choice_traces_union)
apply (simp add: traces_def)
done

lemma cspT_Int_Rep_int_choice_set_union:
  "(!set :Xs1 .. P1f) |~| (!set :Xs2 .. P2f)
   =T[M,M] (!set X:(Xs1 Un Xs2) ..
          IF (X : Xs1 & X : Xs2) THEN (P1f X |~| P2f X)
          ELSE IF (X : Xs1) THEN P1f X ELSE P2f X)"
apply (simp add: cspT_semantics)
apply (simp add: Rep_int_choice_traces)
apply (subgoal_tac 
  "traces (!set :Xs1 .. P1f |~| !set :Xs2 .. P2f) M =
   traces (!set :Xs1 .. P1f) M UnT traces(!set :Xs2 .. P2f) M")
apply (simp add: Rep_int_choice_traces)
apply (simp add: cspT_Int_Rep_int_choice_traces_union)
apply (simp add: traces_def)
done

lemma cspT_Int_Rep_int_choice_com_union:
  "(! :X1 .. P1f) |~| (! :X2 .. P2f)
   =T[M,M] (! a:(X1 Un X2) ..
          IF (a : X1 & a : X2) THEN (P1f a |~| P2f a)
          ELSE IF (a : X1) THEN P1f a ELSE P2f a)"
apply (simp add: cspT_semantics)
apply (simp add: Rep_int_choice_traces)
apply (subgoal_tac 
  "traces (! :X1 .. P1f |~| ! :X2 .. P2f) M =
   traces (! :X1 .. P1f) M UnT traces(! :X2 .. P2f) M")
apply (simp add: Rep_int_choice_traces)
apply (simp add: cspT_Int_Rep_int_choice_traces_union)
apply (simp add: traces_def)
done

lemma cspT_Int_Rep_int_choice_f_union:
  "inj f ==>
  (!<f> :X1 .. P1f) |~| (!<f> :X2 .. P2f)
   =T[M,M] (!<f> a:(X1 Un X2) ..
          IF (a : X1 & a : X2) THEN (P1f a |~| P2f a)
          ELSE IF (a : X1) THEN P1f a ELSE P2f a)"
apply (simp add: cspT_semantics)
apply (simp add: Rep_int_choice_traces)
apply (subgoal_tac 
  "traces (!<f> :X1 .. P1f |~| !<f> :X2 .. P2f) M =
   traces (!<f> :X1 .. P1f) M UnT traces(!<f> :X2 .. P2f) M")
apply (simp add: Rep_int_choice_traces)
apply (simp add: cspT_Int_Rep_int_choice_traces_union)
apply (simp add: traces_def)
done

lemmas cspT_Int_Rep_int_choice_union =
       cspT_Int_Rep_int_choice_nat_union
       cspT_Int_Rep_int_choice_set_union
       cspT_Int_Rep_int_choice_com_union
       cspT_Int_Rep_int_choice_f_union

(*-----------------------------------*
 |           !!-union-|~|            |
 *-----------------------------------*)

lemma cspT_Rep_int_choice_nat_union_Int:
  "(!nat :(N1 Un N2) .. Pf)
   =T[M,M] (!nat n:N1 .. Pf n) |~| (!nat n:N2 .. Pf n)"
apply (rule cspT_rw_right)
apply (rule cspT_Int_Rep_int_choice_union)
apply (rule cspT_decompo)
apply (simp)
apply (rule cspT_rw_right)
apply (rule cspT_IF_split)
apply (simp)
apply (simp add: cspT_idem[THEN cspT_sym])
apply (intro impI)
apply (rule cspT_rw_right)
apply (rule cspT_IF_split)
apply (simp)
done

lemma cspT_Rep_int_choice_set_union_Int:
  "(!set :(Xs1 Un Xs2) .. Pf)
   =T[M,M] (!set X:Xs1 .. Pf X) |~| (!set X:Xs2 .. Pf X)"
apply (rule cspT_rw_right)
apply (rule cspT_Int_Rep_int_choice_union)
apply (rule cspT_decompo)
apply (simp)
apply (rule cspT_rw_right)
apply (rule cspT_IF_split)
apply (simp)
apply (simp add: cspT_idem[THEN cspT_sym])
apply (intro impI)
apply (rule cspT_rw_right)
apply (rule cspT_IF_split)
apply (simp)
done

lemma cspT_Rep_int_choice_com_union_Int:
  "(! :(X1 Un X2) .. Pf)
   =T[M,M] (! a:X1 .. Pf a) |~| (! a:X2 .. Pf a)"
apply (rule cspT_rw_right)
apply (rule cspT_Int_Rep_int_choice_union)
apply (rule cspT_decompo)
apply (simp)
apply (rule cspT_rw_right)
apply (rule cspT_IF_split)
apply (simp)
apply (simp add: cspT_idem[THEN cspT_sym])
apply (intro impI)
apply (rule cspT_rw_right)
apply (rule cspT_IF_split)
apply (simp)
done

lemma cspT_Rep_int_choice_f_union_Int:
  "inj f ==>
   (!<f> :(X1 Un X2) .. Pf)
   =T[M,M] (!<f> a:X1 .. Pf a) |~| (!<f> a:X2 .. Pf a)"
apply (rule cspT_rw_right)
apply (rule cspT_Int_Rep_int_choice_union)
apply (simp)
apply (rule cspT_decompo)
apply (simp)
apply (simp)
apply (rule cspT_rw_right)
apply (rule cspT_IF_split)
apply (simp)
apply (simp add: cspT_idem[THEN cspT_sym])
apply (intro impI)
apply (rule cspT_rw_right)
apply (rule cspT_IF_split)
apply (simp)
done

lemmas cspT_Rep_int_choice_union_Int =
       cspT_Rep_int_choice_nat_union_Int
       cspT_Rep_int_choice_set_union_Int
       cspT_Rep_int_choice_com_union_Int
       cspT_Rep_int_choice_f_union_Int

(*********************************************************
                     Depth_rest
 *********************************************************)

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

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

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

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

lemma cspT_Depth_rest_min:
  "P |. n |. m =T[M,M] P |. min n m"
apply (simp add: cspT_semantics)
apply (simp add: traces.simps)
apply (simp add: min_rs)
done

lemma cspT_Depth_rest_congE:
  "[| P =T[M1,M2] Q ; ALL m. P |. m =T[M1,M2] Q |. m ==> S |] ==> S"
apply (simp add: cspT_semantics)
apply (simp add: traces.simps)
done

(*------------------*
 |     !nat-rest    |
 *------------------*)

lemma cspT_nat_Depth_rest_UNIV: 
  "P =T[M,M] !nat n .. (P |. n)"
apply (simp add: cspT_eqT_semantics)
apply (rule order_antisym)

 (* <= *)
 apply (rule)
 apply (simp add: in_traces)
 apply (rule disjI2)
 apply (rule_tac x="lengtht t" in exI)
 apply (simp)

 (* => *)
 apply (rule)
 apply (simp add: in_traces)
 apply (erule disjE)
 apply (simp_all)
done

lemma cspT_nat_Depth_rest_lengthset: 
  "P =T[M,M] !nat n:(lengthset P M) .. (P |. n)"
apply (simp add: cspT_eqT_semantics)
apply (rule order_antisym)

 (* <= *)
 apply (rule)
 apply (simp add: in_traces)
 apply (rule disjI2)
 apply (rule_tac x="lengtht t" in bexI)
 apply (simp)
 apply (simp add: lengthset_def)
 apply (rule_tac x="t" in exI)
 apply (simp)

 (* => *)
 apply (rule)
 apply (simp add: in_traces)
 apply (erule disjE)
 apply (simp_all)
done

lemmas cspT_nat_Depth_rest = cspT_nat_Depth_rest_UNIV
                             cspT_nat_Depth_rest_lengthset

(*------------------*
 |    ?-partial     |
 *------------------*)

lemma cspT_Ext_pre_choice_partial:
  "? :X -> Pf =T[M,M] ? x:X -> (IF (x:X) THEN Pf x ELSE DIV)"
apply (rule cspT_decompo)
apply (simp_all)
apply (rule cspT_rw_right)
apply (rule cspT_IF)
apply (simp)
done

(*------------------*
 |   !!-partial     |
 *------------------*)

lemma cspT_Rep_int_choice_nat_partial:
  "!nat :N .. Pf =T[M,M] !nat n:N .. (IF (n:N) THEN Pf n ELSE DIV)"
apply (rule cspT_decompo)
apply (simp_all)
apply (rule cspT_rw_right)
apply (rule cspT_IF)
apply (simp)
done

lemma cspT_Rep_int_choice_set_partial:
  "!set :Xs .. Pf =T[M,M] !set X:Xs .. (IF (X:Xs) THEN Pf X ELSE DIV)"
apply (rule cspT_decompo)
apply (simp_all)
apply (rule cspT_rw_right)
apply (rule cspT_IF)
apply (simp)
done

lemma cspT_Rep_int_choice_com_partial:
  "! :X .. Pf =T[M,M] ! a:X .. (IF (a:X) THEN Pf a ELSE DIV)"
apply (rule cspT_decompo)
apply (simp_all)
apply (rule cspT_rw_right)
apply (rule cspT_IF)
apply (simp)
done

lemma cspT_Rep_int_choice_f_partial:
  "inj f ==> !<f> :X .. Pf =T[M,M] !<f> a:X .. (IF (a:X) THEN Pf a ELSE DIV)"
apply (rule cspT_decompo)
apply (simp_all)
apply (rule cspT_rw_right)
apply (rule cspT_IF)
apply (simp)
done

lemmas cspT_Rep_int_choice_partial =
       cspT_Rep_int_choice_nat_partial
       cspT_Rep_int_choice_set_partial
       cspT_Rep_int_choice_com_partial
       cspT_Rep_int_choice_f_partial

end