Theory CSP_F_mono

Up to index of Isabelle/HOL/HOL-Complex/CSP/CSP_T/CSP_F

theory CSP_F_mono
imports CSP_F_failuresfun CSP_T_mono
begin
           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2004         |
            |               December 2004               |
            |                   July 2005 (modified)    |
            |                 August 2005 (modified)    |
            |                                           |
            |        CSP-Prover on Isabelle2005         |
            |                October 2005  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_F_mono = CSP_F_failuresfun + CSP_T_mono:

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

         1. mono check of failuresfun
         2. 
         3. 
         4. 

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

(*--------------------------------*
 |        STOP,SKIP,DIV           |
 *--------------------------------*)

lemma mono_failuresfun_STOP: "mono (failuresfun (%x. STOP))"
by (simp add: mono_def failuresfun_def)

lemma mono_failuresfun_SKIP: "mono (failuresfun (%x. SKIP))"
by (simp add: mono_def failuresfun_def)

lemma mono_failuresfun_DIV: "mono (failuresfun (%x. DIV))"
by (simp add: mono_def failuresfun_def)

(*--------------------------------*
 |          Act_prefix            |
 *--------------------------------*)

lemma mono_failuresfun_Act_prefix:
 "mono (failuresfun Pf) ==> mono (failuresfun (%f. a -> (Pf f)))"
apply (simp add: mono_def)
apply (intro allI impI)
apply (drule_tac x="A" in spec)
apply (drule_tac x="B" in spec)
apply (simp)
apply (rule)
apply (simp add: in_failuresfun)
apply (auto)
done

(*--------------------------------*
 |        Ext_pre_choice          |
 *--------------------------------*)

lemma mono_failuresfun_Ext_pre_choice:
 "ALL a. mono (failuresfun (Pff a))
  ==> mono (failuresfun (%f. ? a:X -> (Pff a f)))"
apply (simp add: mono_def)
apply (intro allI impI)
apply (rule)
apply (simp add: in_failuresfun)
apply (erule disjE, simp)
apply (rule disjI2)
apply (elim conjE exE)
apply (drule_tac x="a" in spec)
apply (drule_tac x="A" in spec)
apply (drule_tac x="B" in spec)
apply (auto)
done

(*--------------------------------*
 |          Ext_choice            |
 *--------------------------------*)

lemma mono_failuresfun_Ext_choice:
 "[| Pf : Procfun ; Qf : Procfun ;
     mono (tracesfun Pf) ; mono (tracesfun Qf) ;
     mono (failuresfun Pf) ; mono (failuresfun Qf) |]
  ==> mono (failuresfun (%f. (Pf f [+] Qf f)))"
apply (simp add: mono_def)
apply (intro allI impI)
apply (rule)
apply (simp add: in_failuresfun)
apply (drule_tac x="A" in spec)
apply (drule_tac x="A" in spec)
apply (drule_tac x="B" in spec)
apply (drule_tac x="B" in spec)
apply (drule_tac x="(fstF o A)" in spec)
apply (drule_tac x="(fstF o A)" in spec)
apply (drule_tac x="(fstF o B)" in spec)
apply (drule_tac x="(fstF o B)" in spec)
apply (simp add: order_prod_def mono_fstF[simplified mono_def])
apply (elim conjE disjE)
apply (force)+
done

(*--------------------------------*
 |          Int_choice            |
 *--------------------------------*)

lemma mono_failuresfun_Int_choice:
 "[| mono (failuresfun Pf) ; mono (failuresfun Qf) |]
  ==> mono (failuresfun (%f. (Pf f |~| Qf f)))"
apply (simp add: mono_def)
apply (intro allI impI)
apply (rule)
apply (simp add: in_failuresfun)
apply (elim disjE)
apply (force)
apply (force)
done

(*--------------------------------*
 |        Rep_int_choice          |
 *--------------------------------*)

lemma mono_failuresfun_Rep_int_choice:
 "ALL c. mono (failuresfun (Pff c))
  ==> mono (failuresfun (%f. !! c:C .. (Pff c f)))"
apply (simp add: mono_def)
apply (intro allI impI)
apply (rule)
apply (simp add: in_failuresfun)
apply (elim conjE bexE)
apply (drule_tac x="c" in spec)
apply (drule_tac x="A" in spec)
apply (drule_tac x="B" in spec)
apply (auto)
done

(*--------------------------------*
 |              IF                |
 *--------------------------------*)

lemma mono_failuresfun_IF:
 "[| mono (failuresfun Pf) ; mono (failuresfun Qf) |]
  ==> mono (failuresfun (%f. IF b THEN (Pf f) ELSE (Qf f)))"
apply (simp add: mono_def)
apply (auto simp add: in_failuresfun subsetF_iff)
done

(*--------------------------------*
 |           Parallel             |
 *--------------------------------*)

lemma mono_failuresfun_Parallel:
 "[| mono (failuresfun Pf) ; mono (failuresfun Qf) |]
  ==> mono (failuresfun (%f. (Pf f) |[X]| (Qf f)))"
apply (simp add: mono_def)
apply (intro allI impI)
apply (rule)
apply (simp add: in_failuresfun)
apply (elim conjE exE)
apply (rule_tac x="Y" in exI)
apply (rule_tac x="Z" in exI)
apply (simp)
apply (rule_tac x="sa" in exI)
apply (rule_tac x="t" in exI)
apply (auto simp add: subsetF_iff)
done

(*--------------------------------*
 |            Hiding              |
 *--------------------------------*)

lemma mono_failuresfun_Hiding:
 "mono (failuresfun Pf)
  ==> mono (failuresfun (%f. (Pf f) -- X))"
apply (simp add: mono_def)
apply (intro allI impI)
apply (rule)
apply (simp add: in_failuresfun)
apply (elim conjE exE)
apply (rule_tac x="sa" in exI)
apply (auto simp add: subsetF_iff)
done

(*--------------------------------*
 |           Renaming             |
 *--------------------------------*)

lemma mono_failuresfun_Renaming:
 "mono (failuresfun Pf)
  ==> mono (failuresfun (%f. (Pf f) [[r]]))"
apply (simp add: mono_def)
apply (intro allI impI)
apply (rule)
apply (simp add: in_failuresfun)
apply (elim conjE exE)
apply (rule_tac x="sa" in exI)
apply (auto simp add: subsetF_iff)
done

(*--------------------------------*
 |           Seq_compo            |
 *--------------------------------*)

lemma mono_failuresfun_Seq_compo:
 "[| Pf : Procfun ; mono (tracesfun Pf) ;
     mono (failuresfun Pf) ; mono (failuresfun Qf) |]
  ==> mono (failuresfun (%f. (Pf f) ;; (Qf f)))"
apply (simp add: mono_def)
apply (intro allI impI)
apply (rule)
apply (simp add: in_failuresfun)

apply (erule disjE)
apply (simp add: subsetF_iff)

apply (elim conjE exE)
apply (rule disjI2)
apply (rule_tac x="sa" in exI)
apply (rule_tac x="t" in exI)
apply (drule_tac x="A" in spec)
apply (drule_tac x="A" in spec)
apply (drule_tac x="B" in spec)
apply (drule_tac x="B" in spec)
apply (drule_tac x="(fstF o A)" in spec)
apply (drule_tac x="(fstF o B)" in spec)
apply (simp add: order_prod_def mono_fstF[simplified mono_def])
apply (auto simp add: subsetF_iff)
done

(*--------------------------------*
 |          Depth_rest            |
 *--------------------------------*)

lemma mono_failuresfun_Depth_rest:
 "mono (failuresfun Pf)
  ==> mono (failuresfun (%f. (Pf f) |. n))"
apply (simp add: mono_def)
apply (intro allI impI)
apply (rule)
apply (simp add: in_failuresfun)
apply (elim conjE exE disjE)
apply (force)
apply (force)
done

(*--------------------------------*
 |            variable            |
 *--------------------------------*)

lemma mono_failuresfun_variable: 
   "mono (failuresfun (%f. f p))"
apply (simp add: mono_def)
apply (intro allI impI)
apply (rule)
apply (simp add: in_failuresfun)
apply (simp add: order_prod_def)
apply (drule_tac x="p" in spec)
apply (insert mono_sndF)
apply (simp add: mono_def)
apply (drule_tac x="A p" in spec)
apply (drule_tac x="B p" in spec)
apply (simp add: subsetF_iff order_prod_def)
done

(*--------------------------------*
 |            Procfun             |
 *--------------------------------*)

lemma mono_failuresfun: 
  "Pf : Procfun ==> mono (failuresfun Pf)"
apply (rule Procfun.induct[of Pf])
apply (simp)
apply (simp add: mono_failuresfun_variable)
apply (simp add: mono_failuresfun_STOP)
apply (simp add: mono_failuresfun_SKIP)
apply (simp add: mono_failuresfun_DIV)
apply (simp add: mono_failuresfun_Act_prefix)
apply (simp add: mono_failuresfun_Ext_pre_choice)
apply (simp add: mono_failuresfun_Ext_choice mono_tracesfun )
apply (simp add: mono_failuresfun_Int_choice)
apply (simp add: mono_failuresfun_Rep_int_choice)
apply (simp add: mono_failuresfun_IF)
apply (simp add: mono_failuresfun_Parallel)
apply (simp add: mono_failuresfun_Hiding)
apply (simp add: mono_failuresfun_Renaming)
apply (simp add: mono_failuresfun_Seq_compo mono_tracesfun)
apply (simp add: mono_failuresfun_Depth_rest)
done

(*=============================================================*
 |                         [[P]]Ffun                           |
 *=============================================================*)

lemma mono_semFfun: 
  "Pf : Procfun ==> mono [[Pf]]Ffun"
apply (subgoal_tac "mono (tracesfun Pf)")
apply (subgoal_tac "mono (failuresfun Pf)")
apply (simp add: mono_def)
apply (simp add: subdomF_decompo)
apply (simp add: semFfun_def)
apply (simp add: tracesfun_f failuresfun_f)
apply (simp add: traces_Proc_F failures_Proc_F)

apply (intro allI impI)
apply (drule_tac x="(%p. fstF (A p))" in spec)
apply (drule_tac x="(%p. fstF (B p))" in spec)
apply (drule mp)
apply (simp add: order_prod_def)
apply (simp add: mono_fstF[simplified mono_def])
apply (simp)
apply (simp add: mono_failuresfun)
apply (simp add: mono_tracesfun)
done

(*=============================================================*
 |                         failuresFun                           |
 *=============================================================*)

lemma mono_failuresFun: 
  "PF : ProcFun ==> mono (failuresFun PF)"
apply (simp add: prod_mono)
apply (simp add: proj_failuresFun_failuresfun)
apply (simp add: ProcFun_def)
apply (simp add: mono_failuresfun)
done

(*=============================================================*
 |                         [[P]]FFun                           |
 *=============================================================*)

lemma mono_semFFun:
   "PF : ProcFun ==> mono [[PF]]FFun"
apply (simp add: prod_mono)
apply (simp add: proj_semFFun_semFfun)
apply (simp add: ProcFun_def)
apply (simp add: mono_semFfun)
done

end

lemma mono_failuresfun_STOP: 

  mono (failuresfun (%x. STOP))

lemma mono_failuresfun_SKIP: 

  mono (failuresfun (%x. SKIP))

lemma mono_failuresfun_DIV: 

  mono (failuresfun (%x. DIV))

lemma mono_failuresfun_Act_prefix: 

  mono (failuresfun Pf) ==> mono (failuresfun (%f. a -> Pf f))

lemma mono_failuresfun_Ext_pre_choice: 

  ∀a. mono (failuresfun (Pff a)) ==> mono (failuresfun (%f. ? a:X -> Pff a f))

lemma mono_failuresfun_Ext_choice: 

  [| Pf ∈ Procfun; Qf ∈ Procfun; mono (tracesfun Pf); mono (tracesfun Qf);
     mono (failuresfun Pf); mono (failuresfun Qf) |]
  ==> mono (failuresfun (%f. Pf f [+] Qf f))

lemma mono_failuresfun_Int_choice: 

  [| mono (failuresfun Pf); mono (failuresfun Qf) |]
  ==> mono (failuresfun (%f. Pf f |~| Qf f))

lemma mono_failuresfun_Rep_int_choice: 

  ∀c. mono (failuresfun (Pff c)) ==> mono (failuresfun (%f. !! c:C .. Pff c f))

lemma mono_failuresfun_IF: 

  [| mono (failuresfun Pf); mono (failuresfun Qf) |]
  ==> mono (failuresfun (%f. IF b THEN Pf f ELSE Qf f))

lemma mono_failuresfun_Parallel: 

  [| mono (failuresfun Pf); mono (failuresfun Qf) |]
  ==> mono (failuresfun (%f. Pf f |[X]| Qf f))

lemma mono_failuresfun_Hiding: 

  mono (failuresfun Pf) ==> mono (failuresfun (%f. Pf f -- X))

lemma mono_failuresfun_Renaming: 

  mono (failuresfun Pf) ==> mono (failuresfun (%f. Pf f [[r]]))

lemma mono_failuresfun_Seq_compo: 

  [| Pf ∈ Procfun; mono (tracesfun Pf); mono (failuresfun Pf);
     mono (failuresfun Qf) |]
  ==> mono (failuresfun (%f. Pf f ;; Qf f))

lemma mono_failuresfun_Depth_rest: 

  mono (failuresfun Pf) ==> mono (failuresfun (%f. Pf f |. n))

lemma mono_failuresfun_variable: 

  mono (failuresfun (%f. f p))

lemma mono_failuresfun: 

  Pf ∈ Procfun ==> mono (failuresfun Pf)

lemma mono_semFfun: 

  Pf ∈ Procfun ==> mono [[Pf]]Ffun

lemma mono_failuresFun: 

  PF ∈ ProcFun ==> mono (failuresFun PF)

lemma mono_semFFun: 

  PF ∈ ProcFun ==> mono [[PF]]FFun