Theory CSP_T_law_norm

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

theory CSP_T_law_norm = CSP_T_law_basic:

(*********************************************************
                       ?-div
 *********************************************************)

lemma cspT_input_DIV:
  "? :A -> Pf =T (? :A -> Pf [+] DIV) |~| ? a:A -> DIV"
apply (simp add: cspT_semantics)
apply (rule order_antisym)

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

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

(*********************************************************
                    !!-!set-div
 *********************************************************)

lemma cspT_Rep_int_choice_set_DIV:
  "!! c:C .. (!set X:(Xsf c) .. (? a:X -> DIV))
   =T !set X:(Union {Xsf c |c. c : C}) .. (? a:X -> 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="Xsf c" in exI)
 apply (force)

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

(*********************************************************
                      ?-!set-<=
 *********************************************************)

lemma cspT_input_Rep_int_choice_set_subset:
  "[| Xs <= Ys ; ALL Y:Ys. EX X:Xs. X <= Y & Y <= A |] ==>
   ((? :A -> Pf) [+] Q) 
   |~| (!set X : Xs .. ? a:X -> DIV)
   =T
   ((? :A -> Pf) [+] Q)
   |~| (!set Y : Ys .. ? a:Y -> DIV)"
apply (simp add: cspT_semantics)
apply (rule order_antisym)

(* => *)
 apply (rule, simp add: in_traces)
 apply (elim disjE conjE exE bexE)
 apply (simp_all)
 apply (drule_tac x="a" in bspec)
 apply (force)
 apply (force)

(* <= *)
 apply (rule, simp add: in_traces)
 apply (elim disjE conjE exE bexE)
 apply (simp_all)
 apply (drule_tac x="a" in bspec, simp)
 apply (force)
done

lemmas cspT_norm = cspT_input_DIV 
                   cspT_Rep_int_choice_set_DIV
                   cspT_input_Rep_int_choice_set_subset

end