Theory CSP_law_etc

Up to index of Isabelle/HOL/HOL-Complex/CSP-Prover

theory CSP_law_etc = CSP_law_SKIP + CSP_law_dist + CSP_law_ref + CSP_law_step1 + CSP_law_step2 + CSP_law_fp_cms + CSP_law_fp_cpo: 
           (*-------------------------------------------*
            |                CSP-Prover                 |
            |               December 2004               |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_law_etc = CSP_law_SKIP   + 
                     CSP_law_dist   + CSP_law_ref +
                     CSP_law_step1  + CSP_law_step2 +
                     CSP_law_fp_cms + CSP_law_fp_cpo:

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

         1. Conditional
         2. Internal ... simp
         3. External ... simp
         4. Mix      ... simp
         5. Extended reflex

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

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

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

lemma csp_Conditional_split: 
  "LET:fp df IN IF b THEN P ELSE Q =F LET:fp df IN (if b then P else Q)"
apply (induct_tac fp)
apply (simp add: eqF_def)
apply (simp add: proc_eqSF_decompo)
apply (simp add: evalT_def)
apply (simp add: evalF_def)
apply (simp add: eqF_def)
apply (simp add: proc_eqSF_decompo)
apply (simp add: evalT_def)
apply (simp add: evalF_def)
done

lemma csp_Conditional_True:
  "LET:fp df IN IF True THEN P ELSE Q =F LET:fp df IN P"
apply (rule csp_rw_left)
apply (rule csp_Conditional_split)
by (simp)

lemma csp_Conditional_False:
  "LET:fp df IN IF False THEN P ELSE Q =F LET:fp df IN Q"
apply (rule csp_rw_left)
apply (rule csp_Conditional_split)
by (simp)

(*****************************************************************
                       Internal ... simp                         
 *****************************************************************)

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

lemma csp_DIV_unwind:
   "LET:fp df IN DIV =F LET:fp df IN ! x:{} .. DIV"
apply (induct_tac fp)
apply (simp add: eqF_def proc_eqSF_decompo,
       simp add: evalT_def evalF_def empF_def)+
done

(*** ! :{a} ***)

lemma domSF_Rep_int_choice_unique:
  "[[! :{a} .. Pf]]SF ev = [[Pf a]]SF ev"
apply (simp add: proc_eqSF_decompo)
apply (rule)
 apply (rule eq_iffI)
  apply (rule)
  apply (simp add: Rep_int_choice_mem)
  apply (force)
  apply (rule)
  apply (simp add: Rep_int_choice_mem)

 apply (rule eq_iffI)
  apply (rule)
  apply (simp add: Rep_int_choice_mem)
  apply (rule)
  apply (simp add: Rep_int_choice_mem)
done

lemma csp_Rep_int_choice_unique:
  "LET:fp df IN ! :{a} .. Pf =F LET:fp df IN Pf a"
apply (induct_tac fp)
by (simp_all add: eqF_def domSF_Rep_int_choice_unique)

(* Int choice idempotence *)

lemma csp_Int_choice_idem: 
  "LET:fp df IN P |~| P =F LET:fp df IN P"
apply (induct_tac fp)
apply (simp add: eqF_def)
apply (simp add: proc_eqSF_decompo)
apply (rule)
apply (rule eq_iffI,
      (rule, simp add: Int_choice_mem)+)+

apply (simp add: eqF_def)
apply (simp add: proc_eqSF_decompo)
apply (rule)
apply (rule eq_iffI,
      (rule, simp add: Int_choice_mem)+)+
done

lemma csp_Int_choice_idem_weak: 
  "LET:fp df IN P =F LET:fp df IN Q ==> LET:fp df IN P |~| Q =F LET:fp df IN P"
apply (rule csp_rw_left)
apply (rule csp_decompo)
apply (rule csp_reflex)
apply (erule csp_symE)
apply (simp)
apply (simp add: csp_Int_choice_idem)
done

(*****************************************************************
                      External ... simp
 *****************************************************************)

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

lemma domSF_Ext_choice_unit_l: 
  "[[STOP [+] P]]SF ev = [[P]]SF ev"
apply (simp add: proc_eqSF_decompo)
apply (rule conjI)

(* T *)
 apply (rule eq_iffI)

 (* <= *)
  apply (rule)
  apply (simp add: Ext_choice_mem)
  apply (erule disjE)
  apply (simp add: STOP_mem)
  apply (simp)
 (* => *)
  apply (rule)
  apply (simp add: Ext_choice_mem)

(* F *)
 apply (rule eq_iffI)

 (* <= *)
  apply (rule)
  apply (simp add: Ext_choice_mem)
  apply (elim disjE)
   apply (simp add: memF_IntF)
   apply (simp add: STOP_mem, fast)
   apply (simp add: memF_UnF)
   apply (elim conjE disjE)
   apply (simp_all add: STOP_mem)
   apply (simp add: memT_UnT)
   apply (elim conjE disjE)
   apply (simp add: STOP_mem)
   apply (rule domSF_F2_F4)
   apply (simp_all)
 (* => *)
  apply (rule)
  apply (simp add: Ext_choice_mem)
  apply (case_tac "s = []t")
   apply (simp add: memF_IntF)
   apply (simp add: STOP_mem)
  (* s ~= []t *)
   apply (simp add: memF_UnF)
done

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

lemma csp_Ext_choice_unit_l: 
  "LET:fp df IN STOP [+] P =F LET:fp df IN P"
apply (induct_tac fp)
by (simp_all add: eqF_def domSF_Ext_choice_unit_l)

lemma csp_Ext_choice_STOP_r: 
  "LET:fp df IN P [+] STOP =F LET:fp df IN P"
apply (rule csp_rw_left)
apply (rule csp_Ext_choice_commut)
apply (simp add: csp_Ext_choice_unit_l)
done

(*** weak ***)

lemma csp_Ext_choice_unit_l_weak: 
  "LET:fp df IN Q =F LET:fp df IN STOP 
   ==> LET:fp df IN Q [+] P =F LET:fp df IN P"
apply (rule csp_rw_left)
apply (rule csp_decompo)
apply (assumption)
apply (rule csp_reflex)
apply (simp add: csp_Ext_choice_unit_l)
done

lemma csp_Ext_choice_unit_r_weak: 
  "LET:fp df IN Q =F LET:fp df IN STOP 
   ==> LET:fp df IN P [+] Q =F LET:fp df IN P"
apply (rule csp_rw_left)
apply (rule csp_commut)
apply (simp add: csp_Ext_choice_unit_l_weak)
done

(*****************************************************************
                      Mix ... simp
 *****************************************************************)

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

(*** <= Timeout ***)

lemma csp_Timeout_right:
  "[| LET:fp1 df IN P <=F LET:fp2 df IN Q1 ;
      LET:fp1 df IN P <=F LET:fp2 df IN Q2 |]
      ==> LET:fp1 df IN P <=F LET:fp2 df IN Q1 [> Q2"
apply (rule csp_rw_right)
apply (rule csp_dist)
apply (rule csp_Int_choice_right)
apply (rule csp_Ext_choice_right, simp_all)
apply (rule csp_rw_right)
apply (rule csp_Ext_choice_unit_l, simp_all)
done

(*** STOP [> P  =  P ***)

lemma csp_STOP_Timeout:
  "LET:fp df IN STOP [> P =F LET:fp df IN P"
apply (rule csp_rw_left)
apply (rule csp_dist)
apply (rule csp_rw_left)
apply (rule csp_Int_choice_idem)
apply (rule csp_Ext_choice_unit_l_weak)
by (simp)

lemma csp_STOP_Timeout_weak:
  "[| LET:fp df IN P1 =F LET:fp df IN STOP ;
      LET:fp df IN P2 =F LET:fp df IN STOP |]
   ==> LET:fp df IN (P1 |~| P2) [+] Q =F LET:fp df IN Q"
apply (rule csp_rw_left)
apply (rule csp_decompo)
apply (rule csp_decompo)
apply (simp_all)
apply (rule csp_reflex)
apply (simp add: csp_STOP_Timeout)
done

(*****************************************************************
                Extended reflex by empty sets
 *****************************************************************)

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

lemma csp_Ext_pre_choice_empty: 
  "LET:fp df IN ? :{} -> Pf =F LET:fp df IN ? x:{} -> DIV"
apply (induct_tac fp)
by (simp add: eqF_def proc_eqSF_decompo evalT_def evalF_def)+

lemma csp_Ext_pre_choice_STOP:
   "LET:fp df IN ? :{} -> Pf =F LET:fp df IN STOP"
apply (rule csp_rw_right)
apply (rule csp_STOP_step)
apply (rule csp_Ext_pre_choice_empty)
done

lemmas csp_Ext_pre_choice_STOP_sym = csp_Ext_pre_choice_STOP[THEN csp_sym]

lemma csp_Rep_int_choice_DIV:
   "LET:fp df IN ! :{} .. Pf =F LET:fp df IN DIV"
apply (induct_tac fp)
by (simp add: eqF_def proc_eqSF_decompo evalT_def evalF_def empF_def)+

lemmas csp_Rep_int_choice_DIV_sym = csp_Rep_int_choice_DIV[THEN csp_sym]

lemma csp_Ext_pre_choice_empty_reflex:
   "LET:fp df IN ? :{} -> Pf =F LET:fp df IN ? :{} -> Qf"
apply (rule csp_trans[of _ "LET:fp df IN STOP"])
apply (simp add: csp_Ext_pre_choice_STOP)
apply (simp add: csp_Ext_pre_choice_STOP_sym)
done

lemma csp_Rep_int_choice_empty_reflex:
   "LET:fp df IN ! :{} .. Pf =F LET:fp df IN ! :{} .. Qf"
apply (rule csp_trans[of _ "LET:fp df IN DIV"])
apply (simp add: csp_Rep_int_choice_DIV)
apply (simp add: csp_Rep_int_choice_DIV_sym)
done

lemmas csp_reflex_ex = csp_Ext_pre_choice_STOP
                       csp_Ext_pre_choice_STOP_sym
                       csp_Rep_int_choice_DIV
                       csp_Rep_int_choice_DIV_sym
                       csp_Ext_pre_choice_empty_reflex
                       csp_Rep_int_choice_empty_reflex

declare csp_reflex_ex [simp]

end

lemma csp_Conditional_split: 

  
  LET:fp df IN IF b THEN P ELSE Q =F 
  LET:fp df IN (if b then P else Q)

lemma csp_Conditional_True: 

  
  LET:fp df IN IF True THEN P ELSE Q =F 
  LET:fp df IN P

lemma csp_Conditional_False: 

  
  LET:fp df IN IF False THEN P ELSE Q =F 
  LET:fp df IN Q

lemma csp_DIV_unwind: 

  
  LET:fp df IN DIV =F 
  LET:fp df IN ! x:{} .. DIV

lemma domSF_Rep_int_choice_unique: 

  [[! :{a} .. Pf]]SF ev = [[Pf a]]SF ev

lemma csp_Rep_int_choice_unique: 

  
  LET:fp df IN ! :{a} .. Pf =F 
  LET:fp df IN Pf a

lemma csp_Int_choice_idem: 

  
  LET:fp df IN P |~| P =F 
  LET:fp df IN P

lemma csp_Int_choice_idem_weak: 

  
  LET:fp df IN P =F 
  LET:fp df IN Q
  ==> 
      LET:fp df IN P |~| Q =F 
      LET:fp df IN P

lemma domSF_Ext_choice_unit_l: 

  [[STOP [+] P]]SF ev = [[P]]SF ev

lemma csp_Ext_choice_unit_l: 

  
  LET:fp df IN STOP [+] P =F 
  LET:fp df IN P

lemma csp_Ext_choice_STOP_r: 

  
  LET:fp df IN P [+] STOP =F 
  LET:fp df IN P

lemma csp_Ext_choice_unit_l_weak: 

  
  LET:fp df IN Q =F 
  LET:fp df IN STOP
  ==> 
      LET:fp df IN Q [+] P =F 
      LET:fp df IN P

lemma csp_Ext_choice_unit_r_weak: 

  
  LET:fp df IN Q =F 
  LET:fp df IN STOP
  ==> 
      LET:fp df IN P [+] Q =F 
      LET:fp df IN P

lemma csp_Timeout_right: 

  [| 
     LET:fp1 df IN P <=F 
     LET:fp2 df IN Q1;
     
     LET:fp1 df IN P <=F 
     LET:fp2 df IN Q2 |]
  ==> 
      LET:fp1 df IN P <=F 
      LET:fp2 df IN Q1 [> Q2

lemma csp_STOP_Timeout: 

  
  LET:fp df IN STOP [> P =F 
  LET:fp df IN P

lemma csp_STOP_Timeout_weak: 

  [| 
     LET:fp df IN P1 =F 
     LET:fp df IN STOP;
     
     LET:fp df IN P2 =F 
     LET:fp df IN STOP |]
  ==> 
      LET:fp df IN (P1 |~| P2) [+] Q =F 
      LET:fp df IN Q

lemma csp_Ext_pre_choice_empty: 

  
  LET:fp df IN ? :{} -> Pf =F 
  LET:fp df IN ? x:{} -> DIV

lemma csp_Ext_pre_choice_STOP: 

  
  LET:fp df IN ? :{} -> Pf =F 
  LET:fp df IN STOP

lemmas csp_Ext_pre_choice_STOP_sym: 

  
  LET:fp_1 df_1 IN STOP =F 
  LET:fp_1 df_1 IN ? :{} -> Pf_1

lemma csp_Rep_int_choice_DIV: 

  
  LET:fp df IN ! :{} .. Pf =F 
  LET:fp df IN DIV

lemmas csp_Rep_int_choice_DIV_sym: 

  
  LET:fp_1 df_1 IN DIV =F 
  LET:fp_1 df_1 IN ! :{} .. Pf_1

lemma csp_Ext_pre_choice_empty_reflex: 

  
  LET:fp df IN ? :{} -> Pf =F 
  LET:fp df IN ? :{} -> Qf

lemma csp_Rep_int_choice_empty_reflex: 

  
  LET:fp df IN ! :{} .. Pf =F 
  LET:fp df IN ! :{} .. Qf

lemmas csp_reflex_ex: 

  
  LET:fp df IN ? :{} -> Pf =F 
  LET:fp df IN STOP
  
  LET:fp_1 df_1 IN STOP =F 
  LET:fp_1 df_1 IN ? :{} -> Pf_1
  
  LET:fp df IN ! :{} .. Pf =F 
  LET:fp df IN DIV
  
  LET:fp_1 df_1 IN DIV =F 
  LET:fp_1 df_1 IN ! :{} .. Pf_1
  
  LET:fp df IN ? :{} -> Pf =F 
  LET:fp df IN ? :{} -> Qf
  
  LET:fp df IN ! :{} .. Pf =F 
  LET:fp df IN ! :{} .. Qf