Theory CSP_proc_cms

           (*-------------------------------------------*
            |                CSP-Prover                 |
            |               December 2004               |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_proc_cms = CSP_proc           + STOP_cms
                    + SKIP_cms           + DIV_cms
                    + Act_prefix_cms     + Ext_choice_cms
                    + Ext_pre_choice_cms + Int_choice_cms
                    + Rep_int_choice_cms + Conditional_cms
                    + Parallel_cms       + Renaming_cms
                    + Seq_compo_cms      + Proc_name_cms :

(*  The following simplification rules are deleted in this theory file *)
(*  because they unexpectly rewrite UnionT and InterT.                 *)
(*                  Union (B ` A) = (UN x:A. B x)                      *)
(*                  Inter (B ` A) = (INT x:A. B x)                     *)

declare Union_image_eq [simp del]
declare Inter_image_eq [simp del]

   (* note: split_paired_All: (ALL x. ?P x) = (ALL a b. ?P (a, b)) *)
   (*       split_paired_Ex : (EX x. ?P x) = (EX a b. ?P (a, b))   *)

declare split_paired_All [simp del]
declare split_paired_Ex  [simp del]

(*  The following simplification is sometimes unexpected.              *)
(*                                                                     *)
(*             not_None_eq: (x ~= None) = (EX y. x = Some y)           *)

declare not_None_eq [simp del]

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

         1. proc : nohide --> non-expanding
         2. proc : guarded & nohide --> contraction
         3. 
         4. 

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

(*********************************************************
             decompose subset of proc_rest
 *********************************************************)

lemma proc_rest_subsetSF_decompo:
   "([[P]]SF ev1 rest n <= [[Q]]SF ev2 rest n)
    = ([[P]]T ev1 rest n <= [[Q]]T ev2 rest n &
       [[P]]F ev1 rest n <= [[Q]]F ev2 rest n)"
apply (simp add: restSF_def)
apply (simp add: subsetSF_def)
apply (simp add: Abs_domSF_inverse)

apply (simp add: evalSF_def)
apply (simp add: pairSF_def)
apply (simp add: restSFpair_def)
apply (simp add: Abs_domSF_inverse)
apply (simp add: pair_restriction_def)
apply (simp add: order_pair_def)
done

lemma proc_rest_subsetT_decompo:
   "([[P]]SF ev1 rest n <= [[Q]]SF ev2 rest n)
    ==> [[P]]T ev1 rest n <= [[Q]]T ev2 rest n"
by (simp add: proc_rest_subsetSF_decompo)

lemma proc_rest_subsetF_decompo:
   "([[P]]SF ev1 rest n <= [[Q]]SF ev2 rest n)
    ==> [[P]]F ev1 rest n <= [[Q]]F ev2 rest n"
by (simp add: proc_rest_subsetSF_decompo)

(* eq *)

lemma proc_rest_eqSF_decompo:
   "([[P]]SF ev1 rest n = [[Q]]SF ev2 rest n)
    = ([[P]]T ev1 rest n = [[Q]]T ev2 rest n &
       [[P]]F ev1 rest n = [[Q]]F ev2 rest n)"
apply (simp add: eq_iff)
apply (simp add: proc_rest_subsetSF_decompo)
apply (rule iffI)
by (simp_all)

lemma proc_rest_eqT_decompo:
   "([[P]]SF ev1 rest n = [[Q]]SF ev2 rest n)
    ==> [[P]]T ev1 rest n = [[Q]]T ev2 rest n"
by (simp add: proc_rest_eqSF_decompo)

lemma proc_rest_eqF_decompo:
   "([[P]]SF ev1 rest n = [[Q]]SF ev2 rest n)
    ==> [[P]]F ev1 rest n = [[Q]]F ev2 rest n"
by (simp add: proc_rest_eqSF_decompo)

(*********************************************************
              map_alpha decomposition
 *********************************************************)

(* Abs_domSF *)

lemma map_alpha_Abs_domSF:
  "map_alpha [[P]]SF alpha = map_alpha ([[P]]T ** [[P]]F) alpha"
apply (simp add: evalSF_def)
apply (simp add: pairSF_def)
apply (simp add: pair_fun_def)
apply (simp add: contraction_alpha_def map_alpha_def)
apply (simp add: distance_Abs_domSF)
done

(* decompo *)

lemma map_alpha_evalSF_decompo:
  "map_alpha [[P]]SF alpha = 
   (map_alpha [[P]]T alpha & map_alpha [[P]]F alpha)"
apply (simp add: map_alpha_Abs_domSF)
by (simp add: pair_map_alpha_compo)

(* non_expanding *)

lemma non_expanding_evalSF_decompo:
  "non_expanding [[P]]SF =
   (non_expanding [[P]]T & non_expanding [[P]]F)"
apply (simp add: non_expanding_def)
by (simp add: map_alpha_evalSF_decompo)

(* contraction_alpha *)

lemma contraction_alpha_evalSF_decompo:
  "contraction_alpha [[P]]SF alpha = 
   (contraction_alpha [[P]]T alpha & contraction_alpha [[P]]F alpha)"
apply (simp add: contraction_alpha_def)
by (auto simp add: map_alpha_evalSF_decompo)

(*********************************************************
             !!!   proc non-expanding   !!!
 *********************************************************)

lemma evalSF_non_expanding_lm:
  "ALL P. nohide P --> non_expanding [[P]]SF"
apply (rule allI)
apply (simp add: non_expanding_evalSF_decompo)
apply (induct_tac P)
apply (simp add: STOP_evalT_non_expanding 
                 STOP_evalF_non_expanding)
apply (simp add: SKIP_evalT_non_expanding 
                 SKIP_evalF_non_expanding)
apply (simp add: DIV_evalT_non_expanding 
                 DIV_evalF_non_expanding)
apply (simp add: Act_prefix_evalT_non_expanding 
                 Act_prefix_evalF_non_expanding)
apply (simp add: Ext_pre_choice_evalT_non_expanding
                 Ext_pre_choice_evalF_non_expanding)
apply (simp add: Ext_choice_evalT_non_expanding
                 Ext_choice_evalF_non_expanding)
apply (simp add: Int_choice_evalT_non_expanding
                 Int_choice_evalF_non_expanding)
apply (simp add: Rep_int_choice_evalT_non_expanding
                 Rep_int_choice_evalF_non_expanding)
apply (simp add: Conditional_evalT_non_expanding
                 Conditional_evalF_non_expanding)
apply (simp add: Parallel_evalT_non_expanding
                 Parallel_evalF_non_expanding)
apply (simp)     (* nohide *)
apply (simp add: Renaming_evalT_non_expanding
                 Renaming_evalF_non_expanding)
apply (simp add: Seq_compo_evalT_non_expanding
                 Seq_compo_evalF_non_expanding)
apply (simp add: Proc_name_evalSF_non_expanding
                 non_expanding_evalSF_decompo[THEN sym])
done

lemma evalSF_non_expanding:
  "nohide P ==> non_expanding [[P]]SF"
by (simp add: evalSF_non_expanding_lm)

lemma evalT_and_evalF_non_expanding:
  "nohide P ==> (non_expanding [[P]]T & non_expanding [[P]]F)"
apply (simp add: non_expanding_evalSF_decompo[THEN sym])
by (simp add: evalSF_non_expanding)

lemma evalT_non_expanding:
  "nohide P ==> non_expanding [[P]]T"
by (simp add: evalT_and_evalF_non_expanding)

lemma evalF_non_expanding:
  "nohide P ==> non_expanding [[P]]F"
by (simp add: evalT_and_evalF_non_expanding)

(*********************************************************
            !!!   proc contraction map   !!!
 *********************************************************)

lemma evalSF_contraction_half_lm:
  "ALL P. nohide P & guard P --> contraction_alpha [[P]]SF (1/2)"
apply (rule allI)
apply (simp add: contraction_alpha_evalSF_decompo)
apply (induct_tac P)
apply (simp add: STOP_evalT_contraction_alpha 
                 STOP_evalF_contraction_alpha)
apply (simp add: SKIP_evalT_contraction_alpha 
                 SKIP_evalF_contraction_alpha)
apply (simp add: DIV_evalT_contraction_alpha 
                 DIV_evalF_contraction_alpha)

apply (intro impI conjI)
apply (rule Act_prefix_evalT_contraction_half)
apply (simp add: evalT_non_expanding)
apply (rule Act_prefix_evalF_contraction_half)
apply (simp add: evalF_non_expanding)

apply (intro impI conjI)
apply (rule Ext_pre_choice_evalT_contraction_half)
apply (rule allI)
apply (simp add: evalT_non_expanding)
apply (rule Ext_pre_choice_evalF_contraction_half)
apply (rule allI)
apply (simp add: evalF_non_expanding)

apply (simp add: Ext_choice_evalT_contraction_alpha
                 Ext_choice_evalF_contraction_alpha)
apply (simp add: Int_choice_evalT_contraction_alpha
                 Int_choice_evalF_contraction_alpha)
apply (simp add: Rep_int_choice_evalT_contraction_alpha
                 Rep_int_choice_evalF_contraction_alpha)
apply (simp add: Conditional_evalT_contraction_alpha
                 Conditional_evalF_contraction_alpha)
apply (simp add: Parallel_evalT_contraction_alpha
                 Parallel_evalF_contraction_alpha)
apply (simp)     (* nohide *)
apply (simp add: Renaming_evalT_contraction_alpha
                 Renaming_evalF_contraction_alpha)
apply (simp add: Seq_compo_evalT_contraction_alpha
                 Seq_compo_evalF_contraction_alpha)
apply (simp)     (* guard *)
done

lemma evalSF_contraction_half:
  "[| nohide P ; guard P |] ==> contraction_alpha [[P]]SF (1/2)"
by (simp add: evalSF_contraction_half_lm)

lemma evalT_and_evalF_contraction_half:
  "[| nohide P ; guard P |]
   ==> (contraction_alpha [[P]]T (1/2) & contraction_alpha [[P]]F (1/2))"
apply (simp add: contraction_alpha_evalSF_decompo[THEN sym])
by (simp add: evalSF_contraction_half)

lemma evalT_contraction_half:
  "[| nohide P ; guard P |]
   ==> contraction_alpha [[P]]T (1/2)"
by (simp add: evalT_and_evalF_contraction_half)

lemma evalF_contraction_half:
  "[| nohide P ; guard P |]
   ==> contraction_alpha [[P]]F (1/2)"
by (simp add: evalT_and_evalF_contraction_half)

(*------------------------------------------------------*
 |             Banach theorem for procDF                |
 *------------------------------------------------------*)

(***********************
      mono evalDF
 ***********************)

lemma evalDF_mono: 
  "ev1 <= ev2 ==> [[df]]DF ev1  <= [[df]]DF ev2"
apply (simp add: evalDF_def)
apply (simp (no_asm) add: order_prod_def)
apply (simp add: evalSF_mono)
done

lemma evalDF_mono_fun: "mono [[df]]DF"
by (simp add: evalDF_mono mono_def)

(************************
   non-expanding evalDF
 ************************)

lemma evalDF_non_expanding:
  "(ALL C. nohide (df C)) ==> non_expanding [[df]]DF"
apply (simp add: prod_non_expand)
apply (simp add: proj_fun_evalDF)
apply (rule allI)
apply (drule_tac x="i" in spec)
apply (simp add: evalSF_non_expanding)
done

(***************************
   contraction_half evalDF
 ***************************)

lemma evalDF_contraction_half:
  "(ALL C. nohide (df C) & guard (df C)) ==> contraction_alpha [[df]]DF (1/2)"
apply (simp add: prod_contra_alpha)
apply (simp add: proj_fun_evalDF)
apply (rule allI)
apply (drule_tac x="i" in spec)
apply (simp add: evalSF_contraction_half)
done

(***************************
     contraction evalDF
 ***************************)

lemma evalDF_contraction:
  "(ALL C. nohide (df C) & guard (df C)) ==> contraction [[df]]DF"
apply (simp add: contraction_def)
apply (rule_tac x="1/2" in exI)
apply (simp add: evalDF_contraction_half)
done

(************************
      Banach evalDF
 ************************)

lemma evalDF_Banach_thm:
   "(ALL C. nohide (df C) & guard (df C))
     ==> [[df]]DF hasUFP & (%n. ([[df]]DF^n) x0) convergeTo UFP [[df]]DF"
apply (rule Banach_thm)
apply (simp add: evalDF_contraction)
done

(*------------------------------------------------------*
 |          Fixed Point Induction procDF                |
 *------------------------------------------------------*)

lemma evalDF_constructive_rs:
  "(ALL C. nohide (df C) & guard (df C)) ==> constructive_rs [[df]]DF"
by (simp add: contra_alpha_to_contst evalDF_contraction_half)

(****************** to add them again ******************)

declare Union_image_eq   [simp]
declare Inter_image_eq   [simp]

declare split_paired_All [simp]
declare split_paired_Ex  [simp]

declare not_None_eq      [simp]

end