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               |
            |                  March 2007  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_F_law_etc
imports CSP_F_law_aux CSP_T_law_etc
begin

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

lemma cspF_Int_choice_to_Rep:
  "(P |~| Q) =F[M,M] (!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[M,M]
  (!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_sum_set_input:
  "!! c:C .. (!set X:(Xsf c) .. (? :X -> (Pff c)))
   =F[M,M] !set X:(Union {Xsf c |c. c : sumset C}) .. 
          (? a:X -> (!! c:{c:C. EX X. X:(Xsf c) & a:X}s .. (Pff c a)))"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Rep_int_choice_sum_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="Xa" 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="Xa" in bexI)
  apply (simp_all)

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

lemma cspF_Rep_int_choice_set_input:
  "!nat n:N .. (!set X:(Xsf n) .. (? :X -> (Pff n)))
   =F[M,M] !set X:(Union {Xsf n |n. n : N}) .. 
          (? a:X -> (!nat n:{n:N. EX X. X:(Xsf n) & a:X} .. (Pff n a)))"
apply (simp add: Rep_int_choice_nat_def)
apply (rule cspF_rw_left)
apply (rule cspF_Rep_int_choice_sum_set_input)
apply (rule cspF_decompo)
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[M,M] !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="Xa Un Xb" in exI)
  apply (force)

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

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

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

(* p.289 *)

lemma cspF_Int_choice_Ext_choice_SKIP:
  "(P [+] SKIP) |~| (Q [+] SKIP) =F[M,M] (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[M,M] (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[M,M] (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[M,M] (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[M,M] (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[M,M] 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[M,M] !nat n:{0, Suc 0} .. IF (n = 0) THEN P ELSE Q

lemma cspF_Rep_int_choice_sum_set_input:

  !! c:C .. !set X:Xsf c .. ? :X -> Pff c =F[M,M] 
  !set X:Union {Xsf c |c. c ∈ sumset C} .. 
   ? a:X -> (!! c:{c:C. ∃X. XXsf caX}s .. Pff c a)

lemma cspF_Rep_int_choice_set_input:

  !nat n:N .. !set X:Xsf n .. ? :X -> Pff n =F[M,M] 
  !set X:Union {Xsf n |n. nN} .. 
   ? a:X -> (!nat n:{n : N. ∃X. XXsf naX} .. Pff n a)

lemma cspF_Rep_int_choice_set_set_DIV:

  [| Xs ≠ {}; Ys ≠ {} |]
  ==> !set X:Xs .. !set Y:Ys .. ? a:(XY) -> DIV =F[M,M] 
      !set Z:{XY |X Y. XXsYYs} .. ? a:Z -> DIV

lemma cspF_Int_choice_Ext_choice_SKIP:

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

lemma cspF_Int_choice_Ext_choice_DIV:

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

lemma cspF_Int_choice_Ext_choice_SKIP_DIV:

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

lemma cspF_Int_choice_Ext_choice_DIV_SKIP:

  P [+] DIV |~| Q [+] SKIP =F[M,M] 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[M,M] P1.0 [+] Q1.0 [+] (P2.0 |~| Q2.0)

lemma cspF_Ext_choice_DIV_Int_choice_Id:

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