Theory CSP_F_law

           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2004         |
            |               December 2004               |
            |                   June 2005  (modified)   |
            |              September 2005  (modified)   |
            |                                           |
            |        CSP-Prover on Isabelle2005         |
            |               November 2005  (modified)   |
            |               December 2005  (modified)   |
            |                  April 2006  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_F_law = CSP_F_law_SKIP     + CSP_F_law_ref       +
                   CSP_F_law_dist     + CSP_F_law_alpha_par +
                   CSP_F_law_step     + CSP_F_law_rep_par   +
                   CSP_F_law_fp       + 
                   CSP_F_law_DIV      + CSP_F_law_SKIP_DIV  +
                   CSP_F_law_step_ext + CSP_F_law_norm      +
                   CSP_T_law:

(*********************************************************
            SKIP , DIV  and Internal choice
 *********************************************************)

(*** |~| ***)

lemma cspF_SKIP_DIV_Int_choice: 
  "[| P = SKIP | P = DIV ; Q = SKIP | Q = DIV |] ==>
   (P |~| Q) =F (if (P = SKIP | Q = SKIP) then SKIP else DIV)"
apply (elim disjE)
apply (simp_all)
apply (rule cspF_rw_left)
apply (rule cspF_idem)
apply (rule cspF_reflex)
apply (rule cspF_rw_left)
apply (rule cspF_unit)
apply (rule cspF_reflex)
apply (rule cspF_rw_left)
apply (rule cspF_unit)
apply (rule cspF_reflex)
apply (rule cspF_rw_left)
apply (rule cspF_idem)
apply (rule cspF_reflex)
done

(*** !! ***)

lemma cspF_SKIP_DIV_Rep_int_choice: 
  "[| ALL c:C. (Qf c = SKIP | Qf c = DIV) |] ==>
   (!! c:C .. Qf c) =F
   (if (EX c:C. Qf c = SKIP) then SKIP else DIV)"
apply (case_tac "C={}")
apply (simp add: cspF_Rep_int_choice_empty)
apply (case_tac "ALL c:C. Qf c = DIV")
 apply (simp)
 apply (rule cspF_rw_left)
 apply (rule cspF_Rep_int_choice_const)
 apply (simp)
 apply (force)
 apply (simp)

 apply (simp)
 apply (elim bexE)
 apply (frule_tac x="c" in bspec)
 apply (simp_all)
 apply (intro conjI impI)

  apply (rule cspF_rw_left)
  apply (subgoal_tac 
   "!! :C .. Qf =F !! :({c:C. Qf c = SKIP} Un {c:C. Qf c = DIV}) .. Qf")
  apply (simp)
  apply (rule cspF_decompo)
  apply (force)
  apply (simp)

  apply (rule cspF_rw_left)
  apply (rule cspF_Rep_int_choice_union_Int)
  apply (rule cspF_rw_left)
  apply (rule cspF_decompo)
  apply (rule cspF_Rep_int_choice_const)
  apply (force)
  apply (rule ballI)
  apply (simp)
  apply (case_tac "{c : C. Qf c = DIV}={}")
   apply (simp (no_asm_simp))
   apply (rule cspF_Rep_int_choice0_DIV)

   apply (rule cspF_rw_left)
   apply (rule cspF_Rep_int_choice_const)
   apply (simp_all)
   apply (simp)

  apply (rule cspF_unit)
done

end