Theory CSP_T_mono

           (*-------------------------------------------*
            |        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_T_mono = CSP_T_tracesfun:

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

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

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

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

lemma mono_tracesfun_STOP: "mono (tracesfun (%f. STOP))"
by (simp add: mono_def tracesfun_def)

lemma mono_tracesfun_SKIP: "mono (tracesfun (%f. SKIP))"
by (simp add: mono_def tracesfun_def)

lemma mono_tracesfun_DIV: "mono (tracesfun (%f. DIV))"
by (simp add: mono_def tracesfun_def)

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

lemma mono_tracesfun_Act_prefix:
 "mono (tracesfun Pf) ==> mono (tracesfun (%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_tracesfun)
apply (auto)
done

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

lemma mono_tracesfun_Ext_pre_choice:
 "ALL a. mono (tracesfun (Pff a))
  ==> mono (tracesfun (%f. ? a:X -> (Pff a f)))"
apply (simp add: mono_def)
apply (intro allI impI)
apply (rule)
apply (simp add: in_tracesfun)
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_tracesfun_Ext_choice:
 "[| mono (tracesfun Pf) ; mono (tracesfun Qf) |]
  ==> mono (tracesfun (%f. (Pf f [+] Qf f)))"
apply (simp add: mono_def)
apply (auto simp add: in_tracesfun subdomT_iff)
done

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

lemma mono_tracesfun_Int_choice:
 "[| mono (tracesfun Pf) ; mono (tracesfun Qf) |]
  ==> mono (tracesfun (%f. (Pf f |~| Qf f)))"
apply (simp add: mono_def)
apply (auto simp add: in_tracesfun subdomT_iff)
done

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

lemma mono_tracesfun_Rep_int_choice:
 "ALL c. mono (tracesfun (Pff c))
  ==> mono (tracesfun (%f. !! c:C .. (Pff c f)))"
apply (simp add: mono_def)
apply (intro allI impI)
apply (rule)
apply (simp add: in_tracesfun)
apply (erule disjE, simp)
apply (rule disjI2)
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_tracesfun_IF:
 "[| mono (tracesfun Pf) ; mono (tracesfun Qf) |]
  ==> mono (tracesfun (%f. IF b THEN (Pf f) ELSE (Qf f)))"
apply (simp add: mono_def)
apply (auto simp add: in_tracesfun subdomT_iff)
done

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

lemma mono_tracesfun_Parallel:
 "[| mono (tracesfun Pf) ; mono (tracesfun Qf) |]
  ==> mono (tracesfun (%f. (Pf f) |[X]| (Qf f)))"
apply (simp add: mono_def)
apply (intro allI impI)
apply (rule)
apply (simp add: in_tracesfun)
apply (elim conjE exE)
apply (rule_tac x="s" in exI)
apply (rule_tac x="ta" in exI)
apply (auto simp add: subdomT_iff)
done

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

lemma mono_tracesfun_Hiding:
 "mono (tracesfun Pf)
  ==> mono (tracesfun (%f. (Pf f) -- X))"
apply (simp add: mono_def)
apply (intro allI impI)
apply (rule)
apply (simp add: in_tracesfun)
apply (elim conjE exE)
apply (rule_tac x="s" in exI)
apply (auto simp add: subdomT_iff)
done

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

lemma mono_tracesfun_Renaming:
 "mono (tracesfun Pf)
  ==> mono (tracesfun (%f. (Pf f) [[r]]))"
apply (simp add: mono_def)
apply (intro allI impI)
apply (rule)
apply (simp add: in_tracesfun)
apply (elim conjE exE)
apply (rule_tac x="s" in exI)
apply (auto simp add: subdomT_iff)
done

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

lemma mono_tracesfun_Seq_compo:
 "[| mono (tracesfun Pf) ; mono (tracesfun Qf) |]
  ==> mono (tracesfun (%f. (Pf f) ;; (Qf f)))"
apply (simp add: mono_def)
apply (intro allI impI)
apply (rule)
apply (simp add: in_tracesfun)
apply (erule disjE)
apply (simp add: subdomT_iff)
apply (fast)

apply (elim conjE exE)
apply (rule disjI2)
apply (rule_tac x="s" in exI)
apply (rule_tac x="ta" in exI)
apply (auto simp add: subdomT_iff)
done

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

lemma mono_tracesfun_Depth_rest:
 "mono (tracesfun Pf)
  ==> mono (tracesfun (%f. (Pf f) |. n))"
apply (simp add: mono_def)
apply (intro allI impI)
apply (rule)
apply (simp add: in_tracesfun)
apply (elim conjE exE)
apply (auto simp add: subdomT_iff)
done

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

lemma mono_tracesfun_variable: 
   "mono (tracesfun (%f. f p))"
apply (simp add: mono_def)
apply (intro allI impI)
apply (rule)
apply (simp add: in_tracesfun)
apply (simp add: order_prod_def)
apply (auto simp add: subdomT_iff)
done

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

lemma mono_tracesfun: 
  "Pf : Procfun ==> mono (tracesfun Pf)"
apply (rule Procfun.induct[of Pf])
apply (simp)
apply (simp add: mono_tracesfun_variable)
apply (simp add: mono_tracesfun_STOP)
apply (simp add: mono_tracesfun_SKIP)
apply (simp add: mono_tracesfun_DIV)
apply (simp add: mono_tracesfun_Act_prefix)
apply (simp add: mono_tracesfun_Ext_pre_choice)
apply (simp add: mono_tracesfun_Ext_choice)
apply (simp add: mono_tracesfun_Int_choice)
apply (simp add: mono_tracesfun_Rep_int_choice)
apply (simp add: mono_tracesfun_IF)
apply (simp add: mono_tracesfun_Parallel)
apply (simp add: mono_tracesfun_Hiding)
apply (simp add: mono_tracesfun_Renaming)
apply (simp add: mono_tracesfun_Seq_compo)
apply (simp add: mono_tracesfun_Depth_rest)
done

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

lemma mono_semTfun: 
  "Pf : Procfun ==> mono [[Pf]]Tfun"
by (simp add: semT_to_traces mono_tracesfun)

(*=============================================================*
 |                         tracesFun                           |
 *=============================================================*)

lemma mono_tracesFun: 
  "PF : ProcFun ==> mono (tracesFun PF)"
apply (simp add: prod_mono)
apply (simp add: proj_tracesFun_tracesfun)
apply (simp add: ProcFun_def)
apply (simp add: mono_tracesfun)
done

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

lemma mono_semTFun: 
  "PF : ProcFun ==> mono [[PF]]TFun"
by (simp add: semT_to_traces mono_tracesFun)

end