Theory CSP_law_step2

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

theory CSP_law_step2 = CSP_proc:

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

declare not_None_eq [simp del]

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

         1. step laws
         2.
         3. 
         4. 

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

consts
  Renaming_step ::
      "('a * 'a) set => 'a set => ('a => ('n,'a) proc) => ('n,'a) proc"

defs
  Renaming_step_def :
   "Renaming_step r X Pf ==
      ? y:(r `` X) -> (! x:{x. x:X & (x,y):r} .. (Pf x)[[r]])"

consts
  Seq_compo_step ::
      "'a set => ('a => ('n,'a) proc) => ('n,'a) proc => ('n,'a) proc"

defs
  Seq_compo_step_def :
   "Seq_compo_step X Pf Q == ? x:X -> (Pf x ;; Q)"

(*********************************************************
                    Renaming expansion
 *********************************************************)

(*** domT ***)

lemma domT_Renaming_step:
  "[[(? :X -> Pf) [[r]] ]]T ev =
   [[Renaming_step r X Pf]]T ev"
apply (simp add: Renaming_step_def)
apply (rule eq_iffI)

(* => *)
 apply (rule)
 apply (simp add: Renaming_mem)
 apply (simp add: Ext_pre_choice_mem)
 apply (elim disjE conjE exE)
  (* 1 *)
  apply (simp)

  (* 2 *)
  apply (rule disjI2)
  apply (simp add: ren_tr_Ev_decompo)
  apply (elim conjE exE)
  apply (rule_tac x="b" in exI)
  apply (rule_tac x="ta" in exI)
  apply (simp)
  apply (rule conjI)
   apply (simp add: Rep_int_choice_mem)
   apply (simp add: Renaming_mem)
   apply (fast)
   apply (simp add: Image_iff)
   apply (fast)

(* <= *)
 apply (rule)
 apply (simp add: Ext_pre_choice_mem)
 apply (erule disjE, simp)
 apply (simp add: Rep_int_choice_mem)
 apply (elim disjE conjE exE)
  apply (simp add: Image_iff)
  apply (erule bexE)
  apply (simp add: Renaming_mem)
  apply (rule_tac x="[Ev x]t" in exI)
  apply (simp add: Ext_pre_choice_mem)
 (* *)
  apply (simp add: Renaming_mem)
  apply (elim conjE exE)
  apply (rule_tac x="[Ev aa]t @t sa" in exI)
  apply (simp add: Ext_pre_choice_mem)
  apply (fast)
done

(*** domF ***)

lemma domF_Renaming_step:
  "[[(? :X -> Pf) [[r]] ]]F ev =
   [[Renaming_step r X Pf]]F ev"
apply (simp add: Renaming_step_def)
apply (rule eq_iffI)

(* => *)
 apply (rule)
 apply (simp add: Renaming_mem)
 apply (simp add: Ext_pre_choice_mem)
 apply (elim disjE conjE exE)
  (* 1 *)
  apply (simp add: ren_inv_def)
  apply (force)
  (* 2 *)
  apply (simp add: ren_tr_Ev_decompo)
  apply (elim conjE exE)
  apply (rule disjI2)
  apply (rule_tac x="b" in exI)
  apply (rule_tac x="t" in exI)
  apply (simp)
  apply (simp add: Rep_int_choice_mem)
  apply (rule conjI)
  apply (simp add: Renaming_mem)
  apply (fast)
  apply (fast)

(* <= *)
 apply (rule)
 apply (simp add: Ext_pre_choice_mem)
 apply (elim disjE conjE exE)
  (* 1 *)
  apply (simp add: Ext_pre_choice_mem)
  apply (simp add: Renaming_mem)
  apply (simp add: Ext_pre_choice_mem)
  apply (simp add: ren_inv_def)
  apply (force)
  (* 2 *)
  apply (simp add: Rep_int_choice_mem)
  apply (simp add: Renaming_mem)
  apply (elim conjE exE)
  apply (rule_tac x="[Ev aa]t @t sb" in exI)
  apply (simp add: Ext_pre_choice_mem)
  apply (fast)
done

(*** domSF ***)

lemma domSF_Renaming_step:
  "[[(? :X -> Pf) [[r]] ]]SF ev =
   [[Renaming_step r X Pf]]SF ev"
apply (simp add: proc_eqSF_decompo)
apply (simp add: domT_Renaming_step)
apply (simp add: domF_Renaming_step)
done

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

lemma csp_Renaming_step:
  "LET:fp df IN (? :X -> Pf) [[r]] =F
   LET:fp df IN Renaming_step r X Pf"
apply (induct_tac fp)
by (simp_all add: eqF_def domSF_Renaming_step)

(*********************************************************
            Sequential composition expansion
 *********************************************************)

(*** domT ***)

lemma domT_Seq_compo_step: 
  "[[(? :X -> Pf) ;; Q]]T ev =
   [[Seq_compo_step X Pf Q]]T ev"
apply (simp add: Seq_compo_step_def)
apply (rule eq_iffI)

(* => *)
 apply (rule)
 apply (simp add: Seq_compo_mem)
 apply (simp add: Ext_pre_choice_mem)
 apply (elim conjE exE disjE)

  (* 1 *)
  apply (simp)

  (* 2 *)
 apply (simp add: Seq_compo_mem)
 apply (fast)

  (* 3 *)
 apply (simp)
 apply (insert trace_last_nil_or_unnil)
 apply (drule_tac x="sa" in spec)
 apply (simp add: not_None_T)
 apply (erule disjE, simp)
 apply (elim conjE exE, simp)
 apply (simp add: appt_ass_rev del: appt_ass)
 apply (rule_tac x="a" in exI)
 apply (rule_tac x="sb @t ta" in exI)
 apply (simp)
 apply (simp add: Seq_compo_mem)
 apply (fast)

(* <= *)
 apply (rule)
 apply (simp add: Ext_pre_choice_mem)
 apply (erule disjE, simp)
 apply (simp add: Seq_compo_mem)
 apply (elim conjE exE disjE)

 (* 1 *)
  apply (rule disjI1)
  apply (rule_tac x="[Ev a]t @t sa" in exI, simp)
  apply (simp add: Ext_pre_choice_mem)
  apply (fast)

 (* 2 *)
  apply (rule disjI2)
  apply (rule_tac x="[Ev a]t @t sa" in exI)
  apply (rule_tac x="ta" in exI, simp)
  apply (simp add: Ext_pre_choice_mem)
  apply (fast)
done

(*** domF ***)

lemma domF_Seq_compo_step: 
  "[[(? :X -> Pf) ;; Q]]F ev =
   [[Seq_compo_step X Pf Q]]F ev"
apply (simp add: Seq_compo_step_def)
apply (rule eq_iffI)

(* => *)
 apply (rule)
 apply (simp add: Seq_compo_mem)
 apply (simp add: Ext_pre_choice_mem)
 apply (elim conjE exE disjE)

  (* 1 *)
  apply (simp)

  (* 2 *)
 apply (simp add: Seq_compo_mem)
 apply (fast)

  (* 3 *)
 apply (simp)
 apply (insert trace_last_nil_or_unnil)
 apply (drule_tac x="sb" in spec)
 apply (simp add: not_None_T)
 apply (erule disjE, simp)
 apply (elim conjE exE, simp)
 apply (simp add: appt_ass_rev del: appt_ass)
 apply (rule_tac x="a" in exI)
 apply (rule_tac x="sc @t t" in exI)
 apply (simp)
 apply (simp add: Seq_compo_mem)
 apply (fast)

(* <= *)
 apply (rule)
 apply (simp add: Ext_pre_choice_mem)
 apply (erule disjE)
 (* 1 *)
  apply (simp add: Seq_compo_mem)
  apply (rule disjI1)
  apply (simp add: Ext_pre_choice_mem)
  apply (fast)

 (* 2 *)
  apply (elim conjE exE, simp)
  apply (simp add: Seq_compo_mem)
  apply (elim conjE exE disjE)

  (* 2-1 *)
   apply (simp add: Ext_pre_choice_mem)
   apply (fast)

  (* 2-2 *)
   apply (rule disjI2)
   apply (simp add: Ext_pre_choice_mem)
   apply (rule_tac x="[Ev a]t @t sb" in exI)
   apply (rule_tac x="t" in exI, simp)
   apply (rule_tac x="a" in exI)
   apply (rule_tac x="sb @t [Tick]t" in exI, simp)
done

(*** domSF ***)

lemma domSF_Seq_compo_step:
  "[[(? :X -> Pf) ;; Q]]SF ev =
   [[Seq_compo_step X Pf Q]]SF ev"
apply (simp add: proc_eqSF_decompo)
apply (simp add: domT_Seq_compo_step)
apply (simp add: domF_Seq_compo_step)
done

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

lemma csp_Seq_compo_step: 
  "LET:fp df IN (? :X -> Pf) ;; Q =F
   LET:fp df IN Seq_compo_step X Pf Q"
apply (induct_tac fp)
by (simp_all add: eqF_def domSF_Seq_compo_step)

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

declare not_None_eq    [simp]

end