Theory CSP_proc (Isabelle2004: April 2004)

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

theory CSP_proc = SKIP + STOP + DIV + Act_prefix 
                + Ext_pre_choice + Ext_choice + Int_choice
                + Rep_int_choice + Parallel + Hiding
                + Conditional + Renaming + Seq_compo
                + Proc_name :

(*  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]

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

declare not_None_eq [simp del]

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

         1. ([[P]]T , [[P]]F) : domSF
         2. decompose
         3. mono
         4. Timeout eval

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

(*********************************************************
          !!!  ([[P]]T , [[P]]F) : domSF    !!!
 *********************************************************)

lemma proc_domSF[simp]: "([[P]]T ev , [[P]]F ev) : domSF"
apply (induct_tac P)
apply (simp add: STOP_domSF)
apply (simp add: SKIP_domSF)
apply (simp add: DIV_domSF)
apply (simp add: Act_prefix_domSF)
apply (simp add: Ext_pre_choice_domSF)
apply (simp add: Ext_choice_domSF)
apply (simp add: Int_choice_domSF)
apply (simp add: Rep_int_choice_domSF)
apply (simp add: Conditional_domSF)
apply (simp add: Parallel_domSF)
apply (simp add: Hiding_domSF)
apply (simp add: Renaming_domSF)
apply (simp add: Seq_compo_domSF)

apply (simp add: evalT_def evalF_def)
apply (simp add: fstSF_def sndSF_def)
done

(*********************************************************
                      decompose
 *********************************************************)

lemma fstSF_evalSF[simp]: "fstSF ([[P]]SF ev) = [[P]]T ev"
apply (simp add: evalSF_def)
apply (simp add: pairSF_def)
apply (simp add: fstSF_def)
apply (simp add: Abs_domSF_inverse)
done

lemma sndSF_evalSF[simp]: "sndSF ([[P]]SF ev) = [[P]]F ev"
apply (simp add: evalSF_def)
apply (simp add: pairSF_def)
apply (simp add: sndSF_def)
apply (simp add: Abs_domSF_inverse)
done

lemma proc_eqSF_decompo:
  "([[P]]SF ev1 = [[Q]]SF ev2)
 = (([[P]]T ev1 = [[Q]]T ev2) & ([[P]]F ev1 = [[Q]]F ev2))"
apply (simp add: evalSF_def)
apply (simp add: pairSF_def)
apply (simp add: Abs_domSF_inject)
done

lemma proc_eqSF_decompo_fun:
  "([[P]]SF = [[Q]]SF)
 = (([[P]]T = [[Q]]T) & ([[P]]F = [[Q]]F))"
apply (simp add: expand_fun_eq)
by (auto simp add: proc_eqSF_decompo)

(* subset *)

lemma proc_subsetSF_decompo:
  "([[P]]SF ev1 <= [[Q]]SF ev2)
 = (([[P]]T ev1 <= [[Q]]T ev2) & ([[P]]F ev1 <= [[Q]]F ev2))"
apply (simp add: evalSF_def)
apply (simp add: pairSF_def)
apply (simp add: subsetSF_def)
apply (simp add: Abs_domSF_inverse)
apply (simp add: order_pair_def)
done

lemma proc_subsetSF_decompo_fun:
  "([[P]]SF <= [[Q]]SF)
 = (([[P]]T <= [[Q]]T) & ([[P]]F <= [[Q]]F))"
apply (simp add: order_prod_def)
apply (simp add: proc_subsetSF_decompo)
apply (rule iffI)
apply (rule conjI)
apply (rule allI)
apply (drule_tac x="x" in spec, simp)
apply (rule allI)
apply (drule_tac x="x" in spec, simp)

apply (rule allI)
apply (erule conjE)
apply (drule_tac x="x" in spec)
apply (drule_tac x="x" in spec)
by (simp)

(*********************************************************
               !!!   mono [[P]]SF  !!!
 *********************************************************)

lemma evalSF_mono: 
  "ev1 <= ev2 ==> [[P]]SF ev1 <= [[P]]SF ev2"
apply (simp add: proc_subsetSF_decompo)
apply (induct_tac P)

(* STOP *)
apply (simp add: subsetT_iff STOP_memT)
apply (simp add: subsetF_iff STOP_memF)

(* SKIP *)
apply (simp add: subsetT_iff SKIP_memT)
apply (simp add: subsetF_iff SKIP_memF)

(* DIV *)
apply (simp add: subsetT_iff DIV_memT)
apply (simp add: subsetF_iff DIV_memF)

(* Prefix *)
apply (simp add: Act_prefix_evalT_mono)
apply (simp add: Act_prefix_evalF_mono)

(* Ext_pre_choice *)
apply (simp add: Ext_pre_choice_evalT_mono)
apply (simp add: Ext_pre_choice_evalF_mono)

(* Ext_choice *)
apply (simp add: Ext_choice_evalT_mono)
apply (simp add: Ext_choice_evalF_mono)

(* Int_choice *)
apply (simp add: Int_choice_evalT_mono)
apply (simp add: Int_choice_evalF_mono)

(* Rep_int_choice *)
apply (simp add: Rep_int_choice_evalT_mono)
apply (simp add: Rep_int_choice_evalF_mono)

(* Conditional *)
apply (simp add: Conditional_evalT_mono)
apply (simp add: Conditional_evalF_mono)

(* Parallel *)
apply (simp add: Parallel_evalT_mono)
apply (simp add: Parallel_evalF_mono)

(* Hiding *)
apply (simp add: Hiding_evalT_mono)
apply (simp add: Hiding_evalF_mono)

(* Renaming *)
apply (simp add: Renaming_evalT_mono)
apply (simp add: Renaming_evalF_mono)

(* Seq_compo *)
apply (simp add: Seq_compo_evalT_mono)
apply (simp add: Seq_compo_evalF_mono)

(* Proc_name *)
apply (simp add: Proc_name_evalT_mono)
apply (simp add: Proc_name_evalF_mono)
done

(* mono *)

lemma evalSF_mono_fun[simp]: "mono [[P]]SF"
by (simp add: mono_def evalSF_mono)

(*********************************************************
                     Timeout trace eval
 *********************************************************)

lemma Timeout_memT:
  "(t :t [[P [> Q]]T ev) = (t :t [[P]]T ev | t :t [[Q]]T ev)"
by (simp add: evalT_def memT_UnT)

(*********************************************************
                     Timeout failure eval
 *********************************************************)

lemma Timeout_memF:
  "f :f [[P [> Q]]F ev 
   = (f :f [[Q]]F ev | 
     (EX s X. f = (s,X) & s ~= []t & (s,X) :f [[P]]F ev) |
     (EX   X. f = ([]t,X) & X <= Evset & [Tick]t :t [[P]]T ev))"
apply (simp add: Ext_choice_memF)
apply (simp add: memF_UnF memF_IntF)
apply (simp add: Int_choice_memF)
apply (simp add: memT_UnT)
apply (simp add: Int_choice_memT)
apply (simp add: STOP_memF STOP_memT)
apply (rule iffI)

 (* => *)
 apply (elim conjE exE disjE, simp_all)
 apply (rule disjI1)
 apply (rule domSF_F2_F4, simp_all)

 (* <= *)
 apply (elim conjE exE disjE, simp_all)
 apply (auto elim: memF_pairE)
done

lemmas Timeout_mem = Timeout_memT Timeout_memF

(*------------------------------------------------------*
 |             RewriteBy and composition                |
 *------------------------------------------------------*)

lemma RewriteBy_compo: "[[Rewrite P By f]]SF = [[P]]SF o [[f]]DF"
apply (induct_tac P)
apply (simp_all add: expand_fun_eq proc_eqSF_decompo
                     evalT_def evalF_def)
by (simp add: evalDF_def)

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

declare Union_image_eq [simp]
declare Inter_image_eq [simp]
declare not_None_eq    [simp]

end

lemma proc_domSF:

  ([[P]]T ev, [[P]]F ev) ∈ domSF

lemma fstSF_evalSF:

  fstSF ([[P]]SF ev) = [[P]]T ev

lemma sndSF_evalSF:

  sndSF ([[P]]SF ev) = [[P]]F ev

lemma proc_eqSF_decompo:

  ([[P]]SF ev1 = [[Q]]SF ev2) =
  ([[P]]T ev1 = [[Q]]T ev2 ∧ [[P]]F ev1 = [[Q]]F ev2)

lemma proc_eqSF_decompo_fun:

  ([[P]]SF = [[Q]]SF) = ([[P]]T = [[Q]]T ∧ [[P]]F = [[Q]]F)

lemma proc_subsetSF_decompo:

  ([[P]]SF ev1 ≤ [[Q]]SF ev2) =
  ([[P]]T ev1 ≤ [[Q]]T ev2 ∧ [[P]]F ev1 ≤ [[Q]]F ev2)

lemma proc_subsetSF_decompo_fun:

  ([[P]]SF ≤ [[Q]]SF) = ([[P]]T ≤ [[Q]]T ∧ [[P]]F ≤ [[Q]]F)

lemma evalSF_mono:

  ev1 ≤ ev2 ==> [[P]]SF ev1 ≤ [[P]]SF ev2

lemma evalSF_mono_fun:

  mono [[P]]SF

lemma Timeout_memT:

  (t :t [[P [> Q]]T ev) = (t :t [[P]]T ev ∨ t :t [[Q]]T ev)

lemma Timeout_memF:

  (f :f [[P [> Q]]F ev) =
  (f :f [[Q]]F ev ∨
   (∃s X. f = (s, X) ∧ s ≠ []t ∧ (s, X) :f [[P]]F ev) ∨
   (∃X. f = ([]t, X) ∧ X ⊆ Evset ∧ [Tick]t :t [[P]]T ev))

lemmas Timeout_mem:

  (t :t [[P [> Q]]T ev) = (t :t [[P]]T ev ∨ t :t [[Q]]T ev)

  (f :f [[P [> Q]]F ev) =
  (f :f [[Q]]F ev ∨
   (∃s X. f = (s, X) ∧ s ≠ []t ∧ (s, X) :f [[P]]F ev) ∨
   (∃X. f = ([]t, X) ∧ X ⊆ Evset ∧ [Tick]t :t [[P]]T ev))

lemma RewriteBy_compo:

  [[Rewrite P By f]]SF = [[P]]SF ˆ [[f]]DF