Theory CSP_T_law_etc

           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2004         |
            |                  April 2006               |
            |                  March 2007  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_T_law_etc
imports CSP_T_law_aux
begin

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

lemma cspT_Int_choice_to_Rep:
  "(P |~| Q) =T[M,M] (!nat n:{0, (Suc 0)} .. (IF (n = 0) THEN P ELSE Q))"
apply (rule cspT_rw_right)
apply (subgoal_tac 
 "(!nat n:{0, Suc 0} .. IF (n = 0) THEN P ELSE Q) =T[M,M]
  (!nat n:({0} Un {Suc 0}) .. IF (n = 0) THEN P ELSE Q)")
apply (assumption)
apply (rule cspT_decompo)
apply (fast)
apply (simp)
apply (rule cspT_rw_right)
apply (rule cspT_Rep_int_choice_union_Int)
apply (rule cspT_decompo)

apply (rule cspT_rw_right)
apply (rule cspT_Rep_int_choice_singleton)
apply (simp)
apply (rule cspT_rw_right)
apply (rule cspT_IF)
apply (simp)

apply (rule cspT_rw_right)
apply (rule cspT_Rep_int_choice_singleton)
apply (simp)
apply (rule cspT_rw_right)
apply (rule cspT_IF)
apply (simp)
done

(*** cspT_Rep_int_choice_set_input ***)

lemma cspT_Rep_int_choice_set_input:
  "!nat n:N .. (!set X:(Xsf n) .. (? :X -> (Pff n)))
   =T[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: cspT_semantics)
apply (rule order_antisym)

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

(* => *)
 apply (rule)
 apply (simp add: in_traces)
 apply (elim conjE exE bexE disjE)
 apply (simp_all)
  apply (rule_tac x="n" in bexI)
  apply (force)
  apply (simp)

  apply (simp)
  apply (rule_tac x="na" in bexI)
  apply (simp)
  apply (simp)
  apply (fast)
  apply (simp)
done

(*** cspT_Rep_int_choice_set_set_DIV ***)

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

(* <= *)
 apply (rule)
 apply (simp add: in_traces)
 apply (elim conjE exE bexE disjE)
 apply (simp_all)
  apply (rule_tac x="X Un Xa" in exI)
  apply (simp)
  apply (rule_tac x="X" in exI)
  apply (rule_tac x="Xa" in exI)
  apply (simp)
  apply (rule_tac x="X Un Xa" in exI)
  apply (simp)
  apply (rule_tac x="X" in exI)
  apply (rule_tac x="Xa" in exI)
  apply (simp)

(* => *)
 apply (rule)
 apply (simp add: in_traces)
 apply (elim conjE exE bexE disjE)
 apply (simp_all)
 apply (force)
done

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

(* p.289 *)

lemma cspT_Int_choice_Ext_choice_SKIP:
  "(P [+] SKIP) |~| (Q [+] SKIP) =T[M,M] (P [+] Q [+] SKIP)"
apply (simp add: cspT_semantics)
apply (rule order_antisym)

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

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

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

lemma cspT_Int_choice_Ext_choice_DIV:
  "(P [+] DIV) |~| (Q [+] DIV) =T[M,M] (P [+] Q [+] DIV)"
apply (simp add: cspT_semantics)
apply (rule order_antisym)

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

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

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

lemma cspT_Int_choice_Ext_choice_SKIP_DIV: 
  "(P [+] SKIP) |~| (Q [+] DIV) =T[M,M] (P [+] Q [+] SKIP)"
apply (simp add: cspT_semantics)
apply (rule order_antisym)
apply (rule, simp add: in_traces, force)+
done

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

lemma cspT_Int_choice_Ext_choice_DIV_SKIP: 
  "(P [+] DIV) |~| (Q [+] SKIP) =T[M,M] (P [+] Q [+] SKIP)"
apply (simp add: cspT_semantics)
apply (rule order_antisym)
apply (rule, simp add: in_traces, force)+
done

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

lemma cspT_Int_choice_Ext_choice_SKIP_or_DIV:
  "[| P2 = SKIP | P2 = DIV ; Q2 = SKIP | Q2 = DIV |] ==>
   (P1 [+] P2) |~| (Q1 [+] Q2) =T[M,M] (P1 [+] Q1 [+] (P2 |~| Q2))"
apply (elim disjE)
apply (simp)
apply (rule cspT_rw_right)
apply (rule cspT_decompo)
apply (rule cspT_reflex)
apply (rule cspT_idem)
apply (simp add: cspT_Int_choice_Ext_choice_SKIP)

apply (simp)
apply (rule cspT_rw_right)
apply (rule cspT_decompo)
apply (rule cspT_reflex)
apply (rule cspT_unit)
apply (simp add: cspT_Int_choice_Ext_choice_SKIP_DIV)

apply (simp)
apply (rule cspT_rw_right)
apply (rule cspT_decompo)
apply (rule cspT_reflex)
apply (rule cspT_unit)
apply (simp add: cspT_Int_choice_Ext_choice_DIV_SKIP)

apply (simp)
apply (rule cspT_rw_right)
apply (rule cspT_decompo)
apply (rule cspT_reflex)
apply (rule cspT_unit)
apply (simp add: cspT_Int_choice_Ext_choice_DIV)
done

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

lemma cspT_Ext_choice_DIV_Int_choice_Id:
  "(P [+] DIV) |~| P =T[M,M] P"
apply (simp add: cspT_semantics)
apply (rule order_antisym)
 apply (rule, simp add: in_traces)
 apply (force)
 apply (rule, simp add: in_traces)
done

end