Theory CSP_F_law_etc

Up to index of Isabelle/HOL/HOL-Complex/CSP/CSP_T/CSP_F

theory CSP_F_law_etc
imports CSP_F_law_aux CSP_T_law_etc
begin
           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2004         |
            |                  April 2006               |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_F_law_etc = CSP_F_law_aux + CSP_T_law_etc:

(*------------------------*
         |~| --> !!
 *------------------------*)

lemma cspF_Int_choice_to_Rep:
  "(P |~| Q) =F (!nat n:{0, (Suc 0)} .. (IF (n = 0) THEN P ELSE Q))"
apply (rule cspF_rw_right)
apply (subgoal_tac 
 "(!nat n:{0, Suc 0} .. IF (n = 0) THEN P ELSE Q) =F
  (!nat n:({0} Un {Suc 0}) .. IF (n = 0) THEN P ELSE Q)")
apply (assumption)
apply (rule cspF_decompo)
apply (fast)
apply (simp)
apply (rule cspF_rw_right)
apply (rule cspF_Rep_int_choice_union_Int)
apply (rule cspF_decompo)

apply (rule cspF_rw_right)
apply (rule cspF_Rep_int_choice_singleton)
apply (simp)
apply (rule cspF_rw_right)
apply (rule cspF_IF)
apply (simp)

apply (rule cspF_rw_right)
apply (rule cspF_Rep_int_choice_singleton)
apply (simp)
apply (rule cspF_rw_right)
apply (rule cspF_IF)
apply (simp)
done

(*** cspF_Rep_int_choice_set_input ***)

lemma cspF_Rep_int_choice_set_input:
  "!! c:C .. (!set X:(Xsf c) .. (? :X -> (Pff c)))
   =F !set X:(Union {Xsf c |c. c : C}) .. 
          (? a:X -> (!! c:{c:C. EX X. X:(Xsf c) & a:X} .. (Pff c a)))"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Rep_int_choice_set_input)
apply (rule order_antisym)

(* <= *)
 apply (rule)
 apply (simp add: in_failures)
 apply (elim disjE conjE bexE exE)
 apply (simp_all)

  apply (rule_tac x="Xsf c" in exI)
  apply (rule conjI)
  apply (force)

  apply (rule_tac x="a" in bexI)
  apply (simp)
  apply (simp)

  apply (rule_tac x="Xsf c" in exI)
  apply (rule conjI)
  apply (force)
  apply (rule conjI)
  apply (force)
  apply (force)

(* => *)
 apply (rule)
 apply (simp add: in_failures)
 apply (elim disjE conjE exE bexE)
 apply (simp)
  apply (rule_tac x="c" in bexI)
  apply (rule_tac x="a" in bexI)
  apply (simp_all)

  apply (rule_tac x="ca" in bexI)
  apply (simp)
  apply (force)
  apply (simp)
done

(*** cspF_Rep_int_choice_set_set_DIV ***)

lemma cspF_Rep_int_choice_set_set_DIV:
  "[| Xs ~= {} ; Ys ~= {} |] ==> 
   !set X:Xs .. (!set Y:Ys .. (? a:(X Un Y) -> DIV))
   =F !set Z:{X Un Y |X Y. X:Xs & Y:Ys} .. (? a:Z -> DIV)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Rep_int_choice_set_set_DIV)
apply (rule order_antisym)

(* <= *)
 apply (rule)
 apply (simp add: in_failures)
 apply (elim conjE bexE exE)
  apply (rule_tac x="a Un aa" in exI)
  apply (force)

(* => *)
 apply (rule)
 apply (simp add: in_failures)
 apply (elim conjE bexE exE)
 apply (simp)

  apply (rule_tac x="Xa" in bexI)
  apply (rule_tac x="Y" in bexI)
  apply (simp_all)
done

(*********************************************************
               (P [+] SKIP) |~| (Q [+] SKIP)
 *********************************************************)

(* p.289 *)
(*********************************************************
               (P [+] SKIP) |~| (Q [+] SKIP)
 *********************************************************)

(* p.289 *)

lemma cspF_Int_choice_Ext_choice_SKIP:
  "(P [+] SKIP) |~| (Q [+] SKIP) =F (P [+] Q [+] SKIP)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Int_choice_Ext_choice_SKIP)
apply (rule order_antisym)

(* => *)
 apply (rule, simp add: in_traces in_failures)
 apply (force)

(* <= *)
 apply (rule, simp add: in_traces in_failures)
 apply (force)
done

(*********************************************************
               (P [+] DIV) |~| (Q [+] DIV)
 *********************************************************)

lemma cspF_Int_choice_Ext_choice_DIV:
  "(P [+] DIV) |~| (Q [+] DIV) =F (P [+] Q [+] DIV)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Int_choice_Ext_choice_DIV)
apply (rule order_antisym)

(* => *)
 apply (rule, simp add: in_traces in_failures)
 apply (force)

(* <= *)
 apply (rule, simp add: in_traces in_failures)
 apply (force)
done

(*********************************************************
             (P [+] SKIP) |~| (Q [+] DIV)
 *********************************************************)

lemma cspF_Int_choice_Ext_choice_SKIP_DIV: 
  "(P [+] SKIP) |~| (Q [+] DIV) =F (P [+] Q [+] SKIP)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Int_choice_Ext_choice_SKIP_DIV)
apply (rule order_antisym)
apply (rule, simp add: in_traces in_failures, force)+
done

(*********************************************************
             (P [+] DIV) |~| (Q [+] SKIP)
 *********************************************************)

lemma cspF_Int_choice_Ext_choice_DIV_SKIP: 
  "(P [+] DIV) |~| (Q [+] SKIP) =F (P [+] Q [+] SKIP)"
apply (rule cspF_rw_left)
apply (rule cspF_commut)
apply (rule cspF_rw_left)
apply (rule cspF_Int_choice_Ext_choice_SKIP_DIV)
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (rule cspF_commut)
apply (rule cspF_reflex)
apply (rule cspF_reflex)
done

(*********************************************************
         (P [+] SKIP or DIV) |~| (Q [+] DIV or SKIP)
 *********************************************************)

lemma cspF_Int_choice_Ext_choice_SKIP_or_DIV:
  "[| P2 = SKIP | P2 = DIV ; Q2 = SKIP | Q2 = DIV |] ==>
   (P1 [+] P2) |~| (Q1 [+] Q2) =F (P1 [+] Q1 [+] (P2 |~| Q2))"
apply (elim disjE)
apply (simp)
apply (rule cspF_rw_right)
apply (rule cspF_decompo)
apply (rule cspF_reflex)
apply (rule cspF_idem)
apply (simp add: cspF_Int_choice_Ext_choice_SKIP)

apply (simp)
apply (rule cspF_rw_right)
apply (rule cspF_decompo)
apply (rule cspF_reflex)
apply (rule cspF_unit)
apply (simp add: cspF_Int_choice_Ext_choice_SKIP_DIV)

apply (simp)
apply (rule cspF_rw_right)
apply (rule cspF_decompo)
apply (rule cspF_reflex)
apply (rule cspF_unit)
apply (simp add: cspF_Int_choice_Ext_choice_DIV_SKIP)

apply (simp)
apply (rule cspF_rw_right)
apply (rule cspF_decompo)
apply (rule cspF_reflex)
apply (rule cspF_unit)
apply (simp add: cspF_Int_choice_Ext_choice_DIV)
done

(*********************************************************
                    (P [+] DIV) |~| P
 *********************************************************)

lemma cspF_Ext_choice_DIV_Int_choice_Id:
  "(P [+] DIV) |~| P =F P"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Ext_choice_DIV_Int_choice_Id)
apply (rule order_antisym)

(* => *)
 apply (rule, simp add: in_failures)
 apply (elim disjE conjE exE)
 apply (simp_all add: in_traces)
 apply (rule memF_F2)
 apply (rule proc_F4)
 apply (simp)
 apply (simp)
 apply (simp)

(* <= *)
 apply (rule, simp add: in_failures)
done

end

lemma cspF_Int_choice_to_Rep: 

  P |~| Q =F !nat n:{0, Suc 0} .. IF (n = 0) THEN P ELSE Q

lemma cspF_Rep_int_choice_set_input: 

  !! c:C .. !set X:Xsf c .. ? :X -> Pff c =F 
  !set X:Union {Xsf c |c. c ∈ C} .. 
   ? a:X -> (!! c:{c : C. ∃X. X ∈ Xsf c ∧ a ∈ X} .. Pff c a)

lemma cspF_Rep_int_choice_set_set_DIV: 

  [| Xs ≠ {}; Ys ≠ {} |]
  ==> !set X:Xs .. !set Y:Ys .. ? a:(X ∪ Y) -> DIV =F 
      !set Z:{X ∪ Y |X Y. X ∈ Xs ∧ Y ∈ Ys} .. ? a:Z -> DIV

lemma cspF_Int_choice_Ext_choice_SKIP: 

  P [+] SKIP |~| Q [+] SKIP =F P [+] Q [+] SKIP

lemma cspF_Int_choice_Ext_choice_DIV: 

  P [+] DIV |~| Q [+] DIV =F P [+] Q [+] DIV

lemma cspF_Int_choice_Ext_choice_SKIP_DIV: 

  P [+] SKIP |~| Q [+] DIV =F P [+] Q [+] SKIP

lemma cspF_Int_choice_Ext_choice_DIV_SKIP: 

  P [+] DIV |~| Q [+] SKIP =F P [+] Q [+] SKIP

lemma cspF_Int_choice_Ext_choice_SKIP_or_DIV: 

  [| P2.0 = SKIP ∨ P2.0 = DIV; Q2.0 = SKIP ∨ Q2.0 = DIV |]
  ==> P1.0 [+] P2.0 |~| Q1.0 [+] Q2.0 =F P1.0 [+] Q1.0 [+] (P2.0 |~| Q2.0)

lemma cspF_Ext_choice_DIV_Int_choice_Id: 

  P [+] DIV |~| P =F P