Theory Domain_SF_prod

           (*-------------------------------------------*
            |                CSP-Prover                 |
            |               December 2004               |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory Domain_SF_prod = Domain_SF:

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

         1. 
         2. 
         3. 
         4. 

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

(***********************************************************
              type def (Product Stable Failure)
 ***********************************************************)

types ('i,'a) domSF_prod = "'i => 'a domSF"     (* synonym *)

(*----------------------------------------------------------*
 |                                                          |
 |         Fixed point induction for refinement             |
 |                                                          |
 *----------------------------------------------------------*)

consts
  RefSF_prod :: "('i,'a) domSF_prod => ('i,'a) domSF_prod => bool"
  RevSF_prod :: "('i,'a) domSF_prod => ('i,'a) domSF_prod => bool"

defs
  RefSF_prod_def : "RefSF_prod SEp == (%SFp. (SEp <= SFp))"
  RevSF_prod_def : "RevSF_prod SEp == (%SFp. (SFp <= SEp))"

(*********************************************************
                order decomposition
 *********************************************************)

lemma subsetSF_prod_decompo:
  "SFp <= SEp = ((fstSF o SFp <= fstSF o SEp) & (sndSF o SFp <= sndSF o SEp))"
apply (simp add: order_prod_def)
apply (simp add: subsetSF_decompo)
apply (rule iffI)
 apply (rule conjI)
  apply (rule allI)
  apply (drule_tac x="x" in spec, simp)
  apply (rule allI)
  apply (drule_tac x="x" in spec, simp)

 apply (rule allI)
 apply (erule conjE)
 apply (drule_tac x="x" in spec)
 apply (drule_tac x="x" in spec)
 apply (simp)
done

end