Theory CSP_F_law_basic

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

theory CSP_F_law_basic = CSP_F_law_decompo + CSP_T_law_basic:

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

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

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

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

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

lemma cspF_IF_split: 
  "IF b THEN P ELSE Q =F (if b then P else Q)"
apply (simp add: cspF_semantics)
apply (simp add: traces_def)
apply (simp add: failures_def)
done

lemma cspF_IF_True:
  "IF True THEN P ELSE Q =F P"
apply (rule cspF_rw_left)
apply (rule cspF_IF_split)
by (simp)

lemma cspF_IF_False:
  "IF False THEN P ELSE Q =F Q"
apply (rule cspF_rw_left)
apply (rule cspF_IF_split)
by (simp)

lemmas cspF_IF = cspF_IF_True cspF_IF_False

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

lemma cspF_Ext_choice_idem: 
  "P [+] P =F P"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Ext_choice_idem)
apply (rule order_antisym)
 apply (rule, simp add: in_traces in_failures)
 apply (elim conjE disjE)
 apply (simp_all)
 apply (rule proc_F2_F4)
 apply (simp_all)
 apply (rule, simp add: in_traces in_failures)
done

lemma cspF_Int_choice_idem: 
  "P |~| P =F P"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Int_choice_idem)
apply (rule order_antisym)
 apply (rule, simp add: in_failures)+
done

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

lemmas cspF_idem = cspF_Ext_choice_idem cspF_Int_choice_idem

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

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

lemma cspF_Ext_choice_commut:
  "P [+] Q =F Q [+] P"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Ext_choice_commut)

apply (rule order_antisym)
apply (rule, simp add: in_failures, fast)+
done

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

lemma cspF_Int_choice_commut:
  "P |~| Q =F Q |~| P"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Int_choice_commut)
apply (rule order_antisym)
apply (rule, simp add: in_failures, fast)+
done

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

lemma cspF_Parallel_commut:
  "P |[X]| Q =F Q |[X]| P"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Parallel_commut)
apply (rule order_antisym)

apply (rule, simp add: in_failures)
apply (elim conjE exE)
apply (rule_tac x="Z" in exI)
apply (rule_tac x="Y" in exI, simp)
apply (rule conjI, fast)
apply (rule_tac x="t" in exI)
apply (rule_tac x="sa" in exI)
apply (simp add: par_tr_sym)

apply (rule, simp add: in_failures)
apply (elim conjE exE)
apply (rule_tac x="Z" in exI)
apply (rule_tac x="Y" in exI, simp)
apply (rule conjI, fast)
apply (rule_tac x="t" in exI)
apply (rule_tac x="sa" in exI)
apply (simp add: par_tr_sym)
done

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

lemmas cspF_commut = cspF_Ext_choice_commut cspF_Int_choice_commut cspF_Parallel_commut

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

lemma cspF_Ext_choice_assoc:
  "P [+] (Q [+] R) =F (P [+] Q) [+] R"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Ext_choice_assoc)
apply (rule order_antisym)
apply (rule, simp add: in_failures in_traces)
apply (force)
apply (rule, simp add: in_failures in_traces)
apply (force)
done

lemma cspF_Ext_choice_assoc_sym:
  "(P [+] Q) [+] R =F P [+] (Q [+] R)"
apply (rule cspF_sym)
apply (simp add: cspF_Ext_choice_assoc)
done

lemma cspF_Int_choice_assoc:
  "P |~| (Q |~| R) =F (P |~| Q) |~| R"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Int_choice_assoc)
apply (rule order_antisym)
apply (rule, simp add: in_failures)+
done

lemma cspF_Int_choice_assoc_sym:
  "(P |~| Q) |~| R =F P |~| (Q |~| R)"
apply (rule cspF_sym)
apply (simp add: cspF_Int_choice_assoc)
done

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

lemmas cspF_assoc = cspF_Ext_choice_assoc cspF_Int_choice_assoc
lemmas cspF_assoc_sym = cspF_Ext_choice_assoc_sym cspF_Int_choice_assoc_sym

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

lemma cspF_Ext_choice_left_commut:
  "P [+] (Q [+] R) =F Q [+] (P [+] R)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Ext_choice_left_commut)
apply (rule order_antisym)
apply (rule, simp add: in_failures in_traces)
apply (force)
apply (rule, simp add: in_failures in_traces)
apply (force)
done

lemma cspF_Int_choice_left_commut:
  "P |~| (Q |~| R) =F Q |~| (P |~| R)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Int_choice_left_commut)
apply (rule order_antisym)
 apply (rule, simp add: in_failures)+
done

lemmas cspF_left_commut = 
       cspF_Ext_choice_left_commut cspF_Int_choice_left_commut

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

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

lemma cspF_Ext_choice_unit_l: 
  "STOP [+] P =F P"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Ext_choice_unit_l)
apply (rule order_antisym)
 apply (rule, simp add: in_traces in_failures)
 apply (elim conjE disjE)
 apply (simp_all)
 apply (rule proc_F2_F4)
 apply (simp_all)

 apply (rule, simp add: in_failures)
done

lemma cspF_Ext_choice_unit_r: 
  "P [+] STOP =F P"
apply (rule cspF_rw_left)
apply (rule cspF_Ext_choice_commut)
apply (simp add: cspF_Ext_choice_unit_l)
done

lemmas cspF_Ext_choice_unit = 
       cspF_Ext_choice_unit_l cspF_Ext_choice_unit_r

lemma cspF_Int_choice_unit_l: 
  "DIV |~| P =F P"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Int_choice_unit_l)
apply (rule order_antisym)
 apply (rule, simp add: in_failures)
 apply (rule, simp add: in_failures)
done

lemma cspF_Int_choice_unit_r: 
  "P |~| DIV =F P"
apply (rule cspF_rw_left)
apply (rule cspF_Int_choice_commut)
apply (simp add: cspF_Int_choice_unit_l)
done

lemmas cspF_Int_choice_unit = 
       cspF_Int_choice_unit_l cspF_Int_choice_unit_r

lemmas cspF_unit = cspF_Ext_choice_unit cspF_Int_choice_unit

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

lemma cspF_Rep_int_choice0_DIV:
   "!! :{} .. Pf =F DIV"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Rep_int_choice_DIV)
apply (simp add: failures_def)
apply (simp add: empF_def)
done

lemma cspF_Rep_int_choice_fun_DIV:
   "inj f ==> !!<f> :{} .. Pf =F DIV"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Rep_int_choice_fun_DIV)
apply (simp add: failures_def)
apply (simp add: empF_def)
done

lemma cspF_Rep_int_choice2_DIV:
   "!set :{} .. Pf =F DIV"
by (simp add: cspF_Rep_int_choice_fun_DIV)

lemma cspF_Rep_int_choice3_DIV:
   "!nat :{} .. Pf =F DIV"
by (simp add: cspF_Rep_int_choice_fun_DIV)

lemma cspF_Rep_int_choice1_DIV:
   "! :{} .. Pf =F DIV"
apply (simp add: Rep_int_choice_com_def)
apply (simp add: cspF_Rep_int_choice2_DIV)
done

lemmas cspF_Rep_int_choice_DIV = cspF_Rep_int_choice0_DIV
                                 cspF_Rep_int_choice1_DIV
                                 cspF_Rep_int_choice2_DIV
                                 cspF_Rep_int_choice3_DIV

lemmas cspF_Rep_int_choice_DIV_sym = cspF_Rep_int_choice0_DIV[THEN cspF_sym]

lemmas cspF_Rep_int_choice_empty = cspF_Rep_int_choice_DIV

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

lemma cspF_Rep_int_choice_unit0:
  "C ~= {} ==> !! c:C .. P =F P"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Rep_int_choice_unit0)
apply (rule order_antisym)
 apply (rule, simp add: in_failures)
 apply (rule, simp add: in_failures)
 apply (force)
done

lemma cspF_Rep_int_choice_unit_fun:
  "X ~= {} ==> !!<f> x:X .. P =F P"
apply (simp add: Rep_int_choice_fun_def)
apply (simp add: cspF_Rep_int_choice_unit0)
done

lemma cspF_Rep_int_choice_unit_com:
  "X ~= {} ==> ! x:X .. P =F P"
apply (simp add: Rep_int_choice_com_def)
apply (simp add: cspF_Rep_int_choice_unit_fun)
done

lemmas cspF_Rep_int_choice_unit = 
       cspF_Rep_int_choice_unit0
       cspF_Rep_int_choice_unit_fun
       cspF_Rep_int_choice_unit_com

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

(* const *)

lemma cspF_Rep_int_choice_const0:
  "[| C ~= {} ; ALL c:C. Pf c = P |] ==> !! :C .. Pf =F P"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Rep_int_choice_const0)
apply (rule order_antisym)
 apply (rule, simp add: in_failures)
 apply (rule, simp add: in_failures)
 apply (force)
done

lemma cspF_Rep_int_choice_const_fun:
  "[| inj f ; X ~= {} ; ALL x:X. Pf x = P |] ==> !!<f> :X .. Pf =F P"
apply (simp add: Rep_int_choice_fun_def)
apply (rule cspF_Rep_int_choice_const0)
apply (simp)
apply (intro ballI)
apply (simp add: image_iff)
apply (erule bexE)
apply (simp)
done

lemma cspF_Rep_int_choice_const_com:
  "[| X ~= {} ; ALL x:X. Pf x = P |] ==> ! :X .. Pf =F P"
apply (simp add: Rep_int_choice_com_def)
apply (rule cspF_Rep_int_choice_const_fun)
apply (auto)
done

lemmas cspF_Rep_int_choice_const =
       cspF_Rep_int_choice_const0
       cspF_Rep_int_choice_const_fun
       cspF_Rep_int_choice_const_com

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

lemma cspF_Int_Rep_int_choice_union:
  "(!! :C1 .. P1f) |~| (!! :C2 .. P2f)
   =F (!! c:(C1 Un C2) ..
          IF (c : C1 & c : C2) THEN (P1f c |~| P2f c)
          ELSE IF (c : C1) THEN P1f c ELSE P2f c)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Int_Rep_int_choice_union)
apply (rule order_antisym)

 apply (rule)
 apply (simp add: in_failures)
 apply (elim conjE bexE disjE)
  apply (rule_tac x="c" in bexI)
  apply (simp)
  apply (simp)
  apply (rule_tac x="c" in bexI)
  apply (simp)
  apply (simp)

(* => *)
 apply (rule)
 apply (simp add: in_failures)
 apply (elim conjE exE bexE)
 apply (simp_all)
 apply (elim disjE)
 apply (simp_all)
 apply (case_tac "c : C2")
 apply (simp add: in_failures)
 apply (force)
 apply (simp add: in_failures)
 apply (force)
 apply (case_tac "c : C1")
 apply (simp add: in_failures)
 apply (force)
 apply (simp add: in_failures)
 apply (force)
done

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

lemma cspF_Rep_int_choice_union_Int0:
  "(!! :(C1 Un C2) .. Pf)
   =F (!! c:C1 .. Pf c) |~| (!! c:C2 .. Pf c)"
apply (rule cspF_rw_right)
apply (rule cspF_Int_Rep_int_choice_union)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_rw_right)
apply (rule cspF_IF_split)
apply (simp)
apply (simp add: cspF_idem[THEN cspF_sym])
apply (intro impI)
apply (rule cspF_rw_right)
apply (rule cspF_IF_split)
apply (simp)
done

lemma cspF_Rep_int_choice_union_Int_fun:
  "(!!<f> :(X1 Un X2) .. Pf)
   =F (!!<f> x:X1 .. Pf x) |~| (!!<f> x:X2 .. Pf x)"
apply (simp add: Rep_int_choice_fun_def)
apply (rule cspF_rw_right)
apply (rule cspF_Rep_int_choice_union_Int0[THEN cspF_sym])
apply (rule cspF_decompo)
apply (auto)
done

lemma cspF_Rep_int_choice_union_Int_com:
  "(! :(X1 Un X2) .. Pf)
   =F (! x:X1 .. Pf x) |~| (! x:X2 .. Pf x)"
apply (simp add: Rep_int_choice_com_def)
apply (rule cspF_rw_right)
apply (rule cspF_Rep_int_choice_union_Int_fun[THEN cspF_sym])
apply (rule cspF_decompo)
apply (auto)
done

lemmas cspF_Rep_int_choice_union_Int
     = cspF_Rep_int_choice_union_Int0
       cspF_Rep_int_choice_union_Int_fun
       cspF_Rep_int_choice_union_Int_com

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

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

lemma cspF_Depth_rest_Zero:
  "P |. 0 =F DIV"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Depth_rest_Zero)
apply (rule order_antisym)

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

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

lemma cspF_Depth_rest_min:
  "P |. n |. m =F P |. min n m"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Depth_rest_min)
apply (simp add: failures.simps)
apply (simp add: min_rs)
done

lemma cspF_Depth_rest_congE:
  "[| P =F Q ; ALL m. P |. m =F Q |. m ==> S |] ==> S"
apply (simp add: cspF_semantics)
apply (simp add: traces.simps)
apply (simp add: failures.simps)
done

lemma cspF_Depth_rest_n:
  "P |. n |. n =F P |. n"
apply (rule cspF_rw_left)
apply (rule cspF_Depth_rest_min)
apply (simp)
done

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

lemma cspF_nat_Depth_rest_UNIV: 
  "P =F !nat n .. (P |. n)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_nat_Depth_rest_UNIV)
apply (rule order_antisym)

 (* <= *)
 apply (rule)
 apply (simp add: in_failures)
 apply (case_tac "noTick s")

  apply (rule_tac x="Suc (lengtht s)" in exI)
  apply (simp)

  apply (rule_tac x="lengtht s" in exI)
  apply (simp)
  apply (rule_tac x="(butlastt s)" in exI)
  apply (simp add: Tick_decompo)
  apply (simp add: noTick_butlast)

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

lemma cspF_nat_Depth_rest_lengthset: "P =F !nat n:(lengthset P) .. (P |. n)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_nat_Depth_rest_lengthset)
apply (rule order_antisym)

 (* <= *)
 apply (rule)
 apply (simp add: in_failures)
 apply (case_tac "noTick s")

  apply (rule_tac x="Suc (lengtht s)" in bexI)
  apply (simp)
  apply (simp add: lengthset_def)
  apply (rule_tac x="s" in exI)
  apply (simp add: proc_T2)

  apply (rule_tac x="lengtht s" in bexI)
  apply (simp)
  apply (rule_tac x="(butlastt s)" in exI)
  apply (simp add: Tick_decompo)
  apply (simp add: noTick_butlast)
  apply (simp add: lengthset_def)
  apply (rule_tac x="s" in exI)
  apply (simp add: proc_T2)

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

lemmas cspF_nat_Depth_rest = cspF_nat_Depth_rest_UNIV
                             cspF_nat_Depth_rest_lengthset

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

lemma cspF_Ext_pre_choice_partial:
  "? :X -> Pf =F ? x:X -> (IF (x:X) THEN Pf x ELSE DIV)"
apply (rule cspF_decompo)
apply (simp_all)
apply (rule cspF_rw_right)
apply (rule cspF_IF)
apply (simp)
done

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

lemma cspF_Rep_int_choice_partial0:
  "!! :C .. Pf =F !! c:C .. (IF (c:C) THEN Pf c ELSE DIV)"
apply (rule cspF_decompo)
apply (simp_all)
apply (rule cspF_rw_right)
apply (rule cspF_IF)
apply (simp)
done

lemma cspF_Rep_int_choice_partial_fun:
  "inj f ==> !!<f> :X .. Pf =F !!<f> x:X .. (IF (x:X) THEN Pf x ELSE DIV)"
apply (simp add: Rep_int_choice_fun_def)
apply (rule cspF_rw_left)
apply (rule cspF_Rep_int_choice_partial0)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_decompo)
apply (auto)
done

lemma cspF_Rep_int_choice_partial_com:
  "! :X .. Pf =F ! x:X .. (IF (x:X) THEN Pf x ELSE DIV)"
apply (simp add: Rep_int_choice_com_def)
apply (rule cspF_rw_left)
apply (rule cspF_Rep_int_choice_partial_fun)
apply (simp)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_decompo)
apply (auto)
done

lemmas cspF_Rep_int_choice_partial =
       cspF_Rep_int_choice_partial0 
       cspF_Rep_int_choice_partial_fun
       cspF_Rep_int_choice_partial_com

end