Theory CSP_T_traces

Up to index of Isabelle/HOL/CSP/CSP_T

theory CSP_T_traces
imports CSP_T_semantics

           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2004         |
            |               December 2004               |
            |                   June 2005 (modified)    |
            |                 August 2005 (modified)    |
            |                                           |
            |        CSP-Prover on Isabelle2005         |
            |                October 2005  (modified)   |
            |               December 2005  (modified)   |
            |                  March 2007  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_T_traces
imports  CSP_T_semantics
begin

(*  The following simplification rules are deleted in this theory file *)
(*  because they unexpectly rewrite UnionT and InterT.                 *)
(*                  disj_not1: (~ P | Q) = (P --> Q)                   *)

declare disj_not1 [simp del]

(*********************************************************
                        DomT
 *********************************************************)

(*--------------------------------*
 |             STOP               |
 *--------------------------------*)

lemma in_traces_STOP: "(t :t traces(STOP) M) = (t = <>)"
by (simp add: traces_def)

(*--------------------------------*
 |             SKIP               |
 *--------------------------------*)

lemma in_traces_SKIP: "(t :t traces(SKIP) M) = (t = <> | t = <Tick>)"
by (simp add: traces_def)

(*--------------------------------*
 |              DIV               |
 *--------------------------------*)

(*** DIV ***)

lemma in_traces_DIV: "(t :t traces(DIV) M) = (t = <>)"
by (simp add: traces_def)

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

(*** Act_prefix_domT ***)

lemma Act_prefix_domT: 
  "{t. t = <> | (EX s. t = <Ev a> ^^ s & s :t T)} : domT"
apply (simp add: domT_def HC_T1_def)
apply (rule conjI)
apply (rule_tac x="<>" in exI, simp)

apply (simp add: prefix_closed_def)
apply (intro allI impI)
apply (elim conjE exE)

apply (erule disjE, simp)    (* <> *)

apply (elim conjE exE, simp)
apply (erule disjE, simp)    (* <> *)

apply (elim conjE exE, simp)
apply (rule memT_prefix_closed)
by (simp_all)

(*** Act_prefix ***)

lemma in_traces_Act_prefix: 
  "t :t traces(a -> P) M = (t = <> | (EX s. t = <Ev a> ^^ s & s :t traces(P) M))"
apply (simp add: traces_def)
by (simp add: CollectT_open_memT Act_prefix_domT)

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

(*** Ext_pre_choice_domT ***)

lemma Ext_pre_choice_domT: 
  "{t. t = <> | 
       (EX a s. t = <Ev a> ^^ s & s :t Tf a & a : X) } : domT"
apply (simp add: domT_def HC_T1_def)
apply (rule conjI)
apply (rule_tac x="<>" in exI, simp)

apply (simp add: prefix_closed_def)
apply (intro allI impI)
apply (elim conjE exE)

apply (erule disjE, simp)    (* <> *)

apply (elim conjE exE, simp)
apply (erule disjE, simp)    (* <> *)

apply (elim conjE exE, simp)
apply (rule memT_prefix_closed)
by (simp_all)

(*** Ext_pre_choice ***)

lemma in_traces_Ext_pre_choice: 
  "(t :t traces(? :X -> Pf) M) =
   (t = <> | (EX a s. t = <Ev a> ^^ s & s :t traces(Pf a) M & a : X))"
apply (simp add: traces_def)
by (simp add: CollectT_open_memT Ext_pre_choice_domT)

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

(*** Ext_choice_memT ***)

lemma in_traces_Ext_choice: 
  "(t :t traces(P [+] Q) M) = (t :t traces(P) M | t :t traces(Q) M)"
by (simp add: traces_def)

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

(*** Int_choice_memT ***)

lemma in_traces_Int_choice: 
  "(t :t traces(P |~| Q) M) = (t :t traces(P) M| t :t traces(Q) M)"
by (simp add: traces_def)

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

(*** Rep_int_choice_domT ***)

lemma Rep_int_choice_domT: 
  "{t. t = <> | (EX a:X. t :t Tf a) } : domT"
apply (simp add: domT_def HC_T1_def)
apply (rule conjI)
apply (rule_tac x="<>" in exI, simp)

apply (simp add: prefix_closed_def)
apply (intro allI impI)
apply (elim conjE exE)

apply (erule disjE, simp)    (* <> *)

apply (elim conjE bexE)
apply (rule disjI2)
apply (rule_tac x="a" in bexI)
apply (rule memT_prefix_closed)
by (simp_all)

(*** Union_proc ***)

lemma in_traces_Union_proc: 
   "(t :t {t. t = <> | (EX a:X. t :t Tf a)}t) 
  = (t = <> | (EX a:X. t :t Tf a))"
apply (insert Rep_int_choice_domT[of X Tf])
apply (simp add: CollectT_open_memT)
done

lemma in_traces_UNIV_Union_proc: 
   "(t :t {t. EX a. t :t Tf a}t) 
  = (EX a. t :t Tf a)"
apply (insert in_traces_Union_proc[of t UNIV Tf])
apply (simp)
apply (subgoal_tac "{t. t = <> | (EX a. t :t Tf a)}
                  = {t. EX a. t :t Tf a}")
by (auto)

(*** Rep_int_choice ***)

lemma in_traces_Rep_int_choice_sum: 
   "(t :t traces(!! :C .. Pf) M) =
    (t = <> | (EX c: sumset C. t :t traces(Pf c) M))"
apply (simp add: traces_def)
apply (simp add: in_traces_Union_proc)
done

lemma in_traces_Rep_int_choice_nat: 
   "(t :t traces(!nat :N .. Pf) M) = (t = <> | (EX n:N. t :t traces(Pf n) M))"
by (simp add: Rep_int_choice_ss_def in_traces_Rep_int_choice_sum)

lemma in_traces_Rep_int_choice_set: 
   "(t :t traces(!set :Xs .. Pf) M) = (t = <> | (EX X:Xs. t :t traces(Pf X) M))"
by (simp add: Rep_int_choice_ss_def in_traces_Rep_int_choice_sum)

lemma in_traces_Rep_int_choice_com: 
   "(t :t traces(! :X .. Pf) M) = (t = <> | (EX a:X. t :t traces(Pf a) M))"
apply (simp add: traces_def)
apply (simp add: in_traces_Union_proc)
done

lemma in_traces_Rep_int_choice_f: 
   "inj f ==> (t :t traces(!<f> :X .. Pf) M) = (t = <> | (EX a:X. t :t traces(Pf a) M))"
apply (simp add: traces_def)
apply (simp add: in_traces_Union_proc)
done

lemmas in_traces_Rep_int_choice = in_traces_Rep_int_choice_sum
                                  in_traces_Rep_int_choice_set
                                  in_traces_Rep_int_choice_nat
                                  in_traces_Rep_int_choice_com
                                  in_traces_Rep_int_choice_f

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

(*** IF ***)

lemma in_traces_IF: 
  "(t :t traces(IF b THEN P ELSE Q) M)
 = (if b then t :t traces(P) M else t :t traces(Q) M)"
by (simp add: traces_def)

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

(*** Parallel_domT ***)

lemma Parallel_domT : 
  "{u. EX s t. u : s |[X]|tr t & s :t T & t :t S} : domT"
apply (simp add: domT_def HC_T1_def)
apply (rule conjI)
apply (rule_tac x="<>" in exI, simp)

(* prefix closed *)
apply (simp add: prefix_closed_def)
apply (intro allI impI)
apply (elim conjE exE)
apply (erule par_tr_prefixE, simp)
apply (rule_tac x="s'" in exI)
apply (rule_tac x="t'" in exI)
apply (simp)

apply (rule conjI)
by (rule memT_prefix_closed, simp_all)+

(*** Parallel ***)

lemma in_traces_Parallel:
  "(u :t traces(P |[X]| Q) M) = 
   (EX s t. u : s |[X]|tr t & s :t traces(P) M & t :t traces(Q) M)"
apply (simp add: traces_def)
by (simp add: CollectT_open_memT Parallel_domT)

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

(*** Hiding_domT ***)

lemma Hiding_domT : 
  "{t. EX s. t = s --tr X & s :t T } : domT"
apply (simp add: domT_def HC_T1_def)
apply (rule conjI)
apply (rule_tac x="<>" in exI, simp)

(* prefix closed *)
apply (simp add: prefix_closed_def)
apply (intro allI impI)
apply (elim conjE exE)
apply (simp add: hide_tr_prefix)
apply (elim conjE exE)
apply (rule_tac x="ta" in exI)
apply (simp)
apply (rule memT_prefix_closed)
by (simp_all)

(*** Hiding ***)

lemma in_traces_Hiding:
  "(t :t traces(P -- X) M) = 
   (EX s. t = s --tr X & s :t traces(P) M)"
apply (simp add: traces_def)
by (simp add: CollectT_open_memT Hiding_domT)

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

(*** Renaming_domT ***)

lemma Renaming_domT : "{t. EX s. s [[r]]* t & s :t T } : domT"
apply (simp add: domT_def HC_T1_def)
apply (rule conjI)
apply (rule_tac x="<>" in exI, simp)

(* prefix closed *)
apply (simp add: prefix_closed_def)
apply (intro allI impI)
apply (elim conjE exE)
apply (erule ren_tr_prefixE, simp)
apply (rule_tac x="ta" in exI)
apply (simp)
apply (rule memT_prefix_closed)
by (simp_all)

(*** Renaming ***)

lemma in_traces_Renaming:
  "(t :t traces(P [[r]]) M) = (EX s. s [[r]]* t & s :t traces(P) M)"
apply (simp add: traces_def)
by (simp add: CollectT_open_memT Renaming_domT)

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

(*** Seq_compo_domT ***)

lemma Seq_compo_domT : 
  "{u. (EX s. u = rmTick s & s :t S ) |
       (EX s t. u = s ^^ t & s ^^ <Tick> :t S & t :t T & noTick s ) } : domT"
apply (simp add: domT_def HC_T1_def)
apply (rule conjI)
apply (rule_tac x="<>" in exI)
apply (rule disjI1)
apply (rule_tac x="<>" in exI, simp)

(* prefix closed *)
apply (simp add: prefix_closed_def)

 apply (intro allI impI)
 apply (elim conjE exE)
 apply (erule disjE)

  (* case 1 *)
  apply (elim conjE exE)
  apply (rule disjI1)
  apply (simp add: rmTick_prefix)
  apply (elim conjE exE)
  apply (rule_tac x="u" in exI, simp)
  apply (rule memT_prefix_closed, simp_all)
  
  (* case 2 *)
  apply (elim conjE exE)
  apply (simp add: prefix_def)
  apply (elim exE conjE)
  apply (simp add: appt_decompo)

   apply (erule disjE)
   (* long case *)
   apply (elim conjE exE)
   apply (rule disjI2)
   apply (rule_tac x="sa" in exI, simp)
   apply (rule_tac x="ua" in exI, simp)
   apply (subgoal_tac "prefix ua (ua ^^ u)")
    apply (rule memT_prefix_closed, simp_all)
   apply (simp)

   (* short case *)
   apply (elim conjE exE)
   apply (rule disjI1)
   apply (rule_tac x="s" in exI)
   apply (case_tac "~ noTick s", simp)
   apply (simp)
   apply (subgoal_tac "prefix s (s ^^ ua ^^ <Tick>)")
    apply (rule memT_prefix_closed, simp_all)
   apply (simp)
done

(*** Seq_compo ***)

lemma in_traces_Seq_compo:
  "(u :t traces(P ;; Q) M) =
   ((EX s. u = rmTick s & s :t traces(P) M) |
    (EX s t. u = s ^^ t & s ^^ <Tick> :t traces(P) M & t :t traces(Q) M & noTick s))"
apply (simp add: traces_def)
by (simp add: CollectT_open_memT Seq_compo_domT)

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

(*** Depth_rest ***)

lemma in_traces_Depth_rest:
  "(t :t traces(P |. n) M) = (t :t traces(P) M & (lengtht t) <= n)"
apply (simp add: traces_def)
apply (simp add: in_rest_domT)
done

(*--------------------------------*
 |          Proc_name             |
 *--------------------------------*)

(*** Proc_name ***)

lemma in_traces_Proc_name:
  "(t :t traces($p) M) = (t :t M p)"
apply (simp add: traces_def)
done

(*--------------------------------*
 |             alias              |
 *--------------------------------*)

lemmas traces_domT = Act_prefix_domT     Ext_pre_choice_domT
                     Rep_int_choice_domT Parallel_domT
                     Hiding_domT         Renaming_domT
                     Seq_compo_domT

lemmas in_traces = in_traces_STOP  in_traces_SKIP  in_traces_DIV
                   in_traces_Act_prefix     in_traces_Ext_pre_choice
                   in_traces_Ext_choice     in_traces_Int_choice
                   in_traces_Rep_int_choice in_traces_IF
                   in_traces_Parallel       in_traces_Hiding
                   in_traces_Renaming       in_traces_Seq_compo
                   in_traces_Union_proc     in_traces_UNIV_Union_proc
                   in_traces_Depth_rest     in_traces_Proc_name

(*--------------------------------*
 |            Timeout             |
 *--------------------------------*)

(*** Timemout ***)

lemma in_traces_Timeout1:
  "(t :t traces(P [> Q) M) = (t :t traces(P) M | t :t traces(Q) M)"
apply (simp add: traces_def)
done

lemma in_traces_Timeout2:
  "(t :t traces(P [>def Q) M) = (t :t traces(P) M | t :t traces(Q) M)"
apply (simp add: Timeout_def traces_def)
done

lemmas in_traces_Timeout = in_traces_Timeout1 in_traces_Timeout2

(****************** to add them again ******************)

declare disj_not1   [simp]

end