Theory CSP_law_ref

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

theory CSP_law_ref = CSP_law_commut + CSP_law_decompo: 
           (*-------------------------------------------*
            |                CSP-Prover                 |
            |               December 2004               |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_law_ref = CSP_law_commut + CSP_law_decompo:

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

declare not_None_eq [simp del]

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

         1. rules for refinement

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

(*-------------------------------------------------------*
 |              decompose Internal choice                |
 *-------------------------------------------------------*)

(*** or <= ***)                                         (* unsafe *)

lemma domSF_Int_choice_left1:
  "[[Q]]SF ev1 <= [[P1]]SF ev2
   ==> [[Q]]SF ev1 <= [[P1 |~| P2]]SF ev2"
apply (simp add: proc_subsetSF_decompo)
apply (rule)
by (rule, simp add: Int_choice_mem, force)+

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

lemma csp_Int_choice_left1:
  "LET:fp1 df IN P1 <=F LET:fp2 df IN Q
   ==> LET:fp1 df IN P1 |~| P2 <=F LET:fp2 df IN Q"
apply (insert fp_type_is[of fp1])
apply (insert fp_type_is[of fp2])
apply (elim disjE)
by (simp_all add: refF_def domSF_Int_choice_left1)

lemma csp_Int_choice_left2:
  "LET:fp1 df IN P2 <=F LET:fp2 df IN Q
   ==> LET:fp1 df IN P1 |~| P2 <=F LET:fp2 df IN Q"
apply (rule csp_rw_left)
apply (rule csp_commut)
by (simp add: csp_Int_choice_left1)

(*** <= and ***)                                          (* safe *)

lemma domSF_Int_choice_right1:
  "[| [[Q1]]SF ev1 <= [[P]]SF ev2 ; [[Q2]]SF ev1 <= [[P]]SF ev2 |]
   ==> [[Q1 |~| Q2]]SF ev1 <= [[P]]SF ev2"
apply (simp add: proc_subsetSF_decompo)
apply (rule)
by (rule, simp add: Int_choice_mem, force)+

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

lemma csp_Int_choice_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 (insert fp_type_is[of fp1])
apply (insert fp_type_is[of fp2])
apply (elim disjE)
by (simp_all add: refF_def domSF_Int_choice_right1)

(*-------------------------------------------------------*
 |        decompose Replicated internal choice           |
 *-------------------------------------------------------*)

(*** EX <= ***)                                           (* unsafe *)

lemma domSF_Rep_int_choice_left:
  "(EX a. a:X & [[Q]]SF ev1 <= [[Pf a]]SF ev2)
   ==> [[Q]]SF ev1 <= [[! :X .. Pf]]SF ev2"
apply (simp add: proc_subsetSF_decompo)
apply (rule)
by (rule, simp add: Rep_int_choice_mem, force)+

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

lemma csp_Rep_int_choice_left:
  "(EX a. a:X & LET:fp1 df IN Pf a <=F LET:fp2 df IN Q)
      ==> LET:fp1 df IN ! :X .. Pf <=F LET:fp2 df IN Q"
apply (insert fp_type_is[of fp1])
apply (insert fp_type_is[of fp2])
apply (elim disjE)
by (simp_all add: refF_def domSF_Rep_int_choice_left)

lemma csp_Rep_int_choice_left_x:
  "[| x:X ; LET:fp1 df IN Pf x <=F LET:fp2 df IN Q |]
  ==> LET:fp1 df IN ! :X .. Pf <=F LET:fp2 df IN Q"
apply (rule csp_Rep_int_choice_left)
by (fast)

(*** <= ALL ***)                                         (* safe *)

lemma domSF_Rep_int_choice_right:
  "[| !!a. a:X ==> [[Qf a]]SF ev1 <= [[P]]SF ev2 |]
        ==> [[! :X .. Qf]]SF ev1 <= [[P]]SF ev2"
apply (simp add: proc_subsetSF_decompo)
apply (rule)
by (rule, simp add: Rep_int_choice_mem, force)+

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

lemma csp_Rep_int_choice_right:
  "[| !!a. a:X ==> LET:fp1 df IN P <=F LET:fp2 df IN Qf a |]
               ==> LET:fp1 df IN P <=F LET:fp2 df IN ! :X .. Qf"
apply (insert fp_type_is[of fp1])
apply (insert fp_type_is[of fp2])
apply (elim disjE)
by (simp_all add: refF_def domSF_Rep_int_choice_right)

(*-------------------------------------------------------*
 |             decomposition with subset                 |
 *-------------------------------------------------------*)

(*** Rep_int_choice ***)                                        (* unsafe *)

lemma domSF_Rep_int_choice_subset:
  "[|  Y <= X  ; !!a. a:Y ==> [[Qf a]]SF ev1 <= [[Pf a]]SF ev2 |]
                    ==> [[! :Y .. Qf]]SF ev1 <= [[! :X .. Pf]]SF ev2"
apply (simp add: proc_subsetSF_decompo)
apply (rule)
by (rule, simp add: Rep_int_choice_mem, force)+

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

lemma csp_Rep_int_choice_subset:
  "[|  Y <= X  ; !!a. a:Y ==> LET:fp1 df IN Pf a <=F LET:fp2 df IN Qf a |]
                    ==> LET:fp1 df IN ! :X .. Pf <=F LET:fp2 df IN ! :Y .. Qf"
apply (insert fp_type_is[of fp1])
apply (insert fp_type_is[of fp2])
apply (elim disjE)
by (simp_all add: refF_def domSF_Rep_int_choice_subset)

(*** ! x:X .. and ? -> ***)

lemma domSF_Int_Ext_pre_choice_subset:
  "[| Y ~={} ; Y <= X ; !!a. a:Y ==> [[Qf a]]SF ev1 <= [[Pf a]]SF ev2 |]
        ==> [[? :Y -> Qf]]SF ev1 <= [[! x:X .. (x -> Pf x)]]SF ev2"
apply (simp add: proc_subsetSF_decompo)
apply (rule)
 apply (rule)
 apply (simp add: Rep_int_choice_mem Ext_pre_choice_mem Act_prefix_mem)
 apply (elim disjE conjE exE, simp)
 apply (rule disjI2)
 apply (rule_tac x="a" in exI)
 apply (rule)
 apply (rule disjI2)
 apply (rule_tac x="s" in exI)
 apply (simp)
 apply (force)
 apply (fast)

 apply (rule)
 apply (simp add: Rep_int_choice_mem Ext_pre_choice_mem Act_prefix_mem)
 apply (elim disjE conjE exE, simp)
  apply (subgoal_tac "EX a. a:Y")
  apply (elim exE)
  apply (rule_tac x="a" in exI)
  apply (case_tac "Ev a ~: Xa", simp)
  apply (fast)
  apply (fast)
  apply (fast)

 apply (rule_tac x="a" in exI)
 apply (rule)
 apply (rule disjI2)
 apply (rule_tac x="sa" in exI)
 apply (simp)
 apply (force)
 apply (fast)
done

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

lemma csp_Int_Ext_pre_choice_subset:
  "[| Y ~={} ; Y <= X ; !!a. a:Y ==> LET:fp1 df IN Pf a <=F LET:fp2 df IN Qf a |]
        ==> LET:fp1 df IN ! x:X .. (x -> Pf x) <=F
            LET:fp2 df IN ? :Y -> Qf"
apply (insert fp_type_is[of fp1])
apply (insert fp_type_is[of fp2])
apply (elim disjE)
by (simp_all add: refF_def domSF_Int_Ext_pre_choice_subset)

lemmas csp_decompo_subset = csp_Rep_int_choice_subset
                            csp_Int_Ext_pre_choice_subset

(*-------------------------------------------------------*
 |               decompose external choice               |
 *-------------------------------------------------------*)

lemma domSF_Ext_choice_right:
  "[| [[Q1]]SF ev1 <= [[P]]SF ev2 ; [[Q2]]SF ev1 <= [[P]]SF ev2 |]
      ==> [[Q1 [+] Q2]]SF ev1 <= [[P]]SF ev2"
apply (simp add: proc_subsetSF_decompo)
apply (rule)
 apply (rule)
 apply (simp add: Ext_choice_mem)
 apply (force)

 apply (rule)
 apply (simp add: Ext_choice_mem)
 apply (simp add: memF_IntF memF_UnF memT_UnT)
 apply (elim disjE conjE exE, simp)
 apply (force, force, force)

 apply (simp)
 apply (subgoal_tac "([]t, X) :f [[Q1]]F ev1")
 apply (force)
 apply (rule domSF_F2_F4[of "[[Q1]]T ev1" "[[Q1]]F ev1"])
 apply (simp_all)

 apply (subgoal_tac "([]t, X) :f [[Q2]]F ev1")
 apply (force)
 apply (rule domSF_F2_F4[of "[[Q2]]T ev1" "[[Q2]]F ev1"])
 apply (simp_all)
done

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

lemma csp_Ext_choice_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 (insert fp_type_is[of fp1])
apply (insert fp_type_is[of fp2])
apply (elim disjE)
by (simp_all add: refF_def domSF_Ext_choice_right)

(*-------------------------------------------------------*
 |              Int_choice_Ext_choice                    |
 *-------------------------------------------------------*)

lemma domSF_Int_choice_Ext_choice:
  "[[P1 [+] P2]]SF ev <= [[P1 |~| P2]]SF ev"
apply (simp add: proc_subsetSF_decompo)
apply (rule)
 apply (rule)
 apply (simp add: Ext_choice_mem Int_choice_mem)
 apply (rule)
 apply (simp add: Ext_choice_mem Int_choice_mem)
 apply (simp add: memF_IntF memF_UnF memT_UnT)
 apply (elim disjE conjE exE)
  apply (simp_all)

  apply (rule disjI1)
  apply (rule domSF_F2_F4)
  apply (simp_all)

  apply (rule disjI2)
  apply (rule domSF_F2_F4)
  apply (simp_all)
done

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

lemma csp_Int_choice_Ext_choice:
  "LET:fp df IN P1 |~| P2 <=F LET:fp df IN P1 [+] P2"
apply (induct_tac fp)
by (simp_all add: refF_def domSF_Int_choice_Ext_choice)

lemma csp_Int_choice_left3:
  "LET:fp df IN P1 [+] P2 <=F LET:fp df IN Q
   ==> LET:fp df IN P1 |~| P2 <=F LET:fp df IN Q"
apply (rule csp_trans)
apply (rule csp_Int_choice_Ext_choice)
by (simp)

end

lemma domSF_Int_choice_left1: 

  [[Q]]SF ev1 ≤ [[P1]]SF ev2 ==> [[Q]]SF ev1 ≤ [[P1 |~| P2]]SF ev2

lemma csp_Int_choice_left1: 

  
  LET:fp1 df IN P1 <=F 
  LET:fp2 df IN Q
  ==> 
      LET:fp1 df IN P1 |~| P2 <=F 
      LET:fp2 df IN Q

lemma csp_Int_choice_left2: 

  
  LET:fp1 df IN P2 <=F 
  LET:fp2 df IN Q
  ==> 
      LET:fp1 df IN P1 |~| P2 <=F 
      LET:fp2 df IN Q

lemma domSF_Int_choice_right1: 

  [| [[Q1]]SF ev1 ≤ [[P]]SF ev2; [[Q2]]SF ev1 ≤ [[P]]SF ev2 |]
  ==> [[Q1 |~| Q2]]SF ev1 ≤ [[P]]SF ev2

lemma csp_Int_choice_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 domSF_Rep_int_choice_left: 

  ∃a. a ∈ X ∧ [[Q]]SF ev1 ≤ [[Pf a]]SF ev2 ==> [[Q]]SF ev1 ≤ [[! :X .. Pf]]SF ev2

lemma csp_Rep_int_choice_left: 

  ∃a. a ∈ X ∧ 
              LET:fp1 df IN Pf a <=F 
              LET:fp2 df IN Q
  ==> 
      LET:fp1 df IN ! :X .. Pf <=F 
      LET:fp2 df IN Q

lemma csp_Rep_int_choice_left_x: 

  [| x ∈ X; 
            LET:fp1 df IN Pf x <=F 
            LET:fp2 df IN Q |]
  ==> 
      LET:fp1 df IN ! :X .. Pf <=F 
      LET:fp2 df IN Q

lemma domSF_Rep_int_choice_right: 

  (!!a. a ∈ X ==> [[Qf a]]SF ev1 ≤ [[P]]SF ev2)
  ==> [[! :X .. Qf]]SF ev1 ≤ [[P]]SF ev2

lemma csp_Rep_int_choice_right: 

  (!!a. a ∈ X ==> 
                  LET:fp1 df IN P <=F 
                  LET:fp2 df IN Qf a)
  ==> 
      LET:fp1 df IN P <=F 
      LET:fp2 df IN ! :X .. Qf

lemma domSF_Rep_int_choice_subset: 

  [| Y ⊆ X; !!a. a ∈ Y ==> [[Qf a]]SF ev1 ≤ [[Pf a]]SF ev2 |]
  ==> [[! :Y .. Qf]]SF ev1 ≤ [[! :X .. Pf]]SF ev2

lemma csp_Rep_int_choice_subset: 

  [| Y ⊆ X; !!a. a ∈ Y ==> 
                           LET:fp1 df IN Pf a <=F 
                           LET:fp2 df IN Qf a |]
  ==> 
      LET:fp1 df IN ! :X .. Pf <=F 
      LET:fp2 df IN ! :Y .. Qf

lemma domSF_Int_Ext_pre_choice_subset: 

  [| Y ≠ {}; Y ⊆ X; !!a. a ∈ Y ==> [[Qf a]]SF ev1 ≤ [[Pf a]]SF ev2 |]
  ==> [[? :Y -> Qf]]SF ev1 ≤ [[! x:X .. x -> Pf x]]SF ev2

lemma csp_Int_Ext_pre_choice_subset: 

  [| Y ≠ {}; Y ⊆ X;
     !!a. a ∈ Y ==> 
                    LET:fp1 df IN Pf a <=F 
                    LET:fp2 df IN Qf a |]
  ==> 
      LET:fp1 df IN ! x:X .. x -> Pf x <=F 
      LET:fp2 df IN ? :Y -> Qf

lemmas csp_decompo_subset: 

  [| Y ⊆ X; !!a. a ∈ Y ==> 
                           LET:fp1 df IN Pf a <=F 
                           LET:fp2 df IN Qf a |]
  ==> 
      LET:fp1 df IN ! :X .. Pf <=F 
      LET:fp2 df IN ! :Y .. Qf
  [| Y ≠ {}; Y ⊆ X;
     !!a. a ∈ Y ==> 
                    LET:fp1 df IN Pf a <=F 
                    LET:fp2 df IN Qf a |]
  ==> 
      LET:fp1 df IN ! x:X .. x -> Pf x <=F 
      LET:fp2 df IN ? :Y -> Qf

lemma domSF_Ext_choice_right: 

  [| [[Q1]]SF ev1 ≤ [[P]]SF ev2; [[Q2]]SF ev1 ≤ [[P]]SF ev2 |]
  ==> [[Q1 [+] Q2]]SF ev1 ≤ [[P]]SF ev2

lemma csp_Ext_choice_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 domSF_Int_choice_Ext_choice: 

  [[P1 [+] P2]]SF ev ≤ [[P1 |~| P2]]SF ev

lemma csp_Int_choice_Ext_choice: 

  
  LET:fp df IN P1 |~| P2 <=F 
  LET:fp df IN P1 [+] P2

lemma csp_Int_choice_left3: 

  
  LET:fp df IN P1 [+] P2 <=F 
  LET:fp df IN Q
  ==> 
      LET:fp df IN P1 |~| P2 <=F 
      LET:fp df IN Q