Theory CSP_T_traces

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

theory CSP_T_traces
imports CSP_T_semantics
begin

           (*-------------------------------------------*
            |        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

lemma in_traces_STOP:

  (t :t traces STOP M) = (t = <>)

lemma in_traces_SKIP:

  (t :t traces SKIP M) = (t = <> ∨ t = <Tick>)

lemma in_traces_DIV:

  (t :t traces DIV M) = (t = <>)

lemma Act_prefix_domT:

  {t. t = <> ∨ (∃s. t = <Ev a> ^^ ss :t T)} ∈ domT

lemma in_traces_Act_prefix:

  (t :t traces (a -> P) M) = (t = <> ∨ (∃s. t = <Ev a> ^^ ss :t traces P M))

lemma Ext_pre_choice_domT:

  {t. t = <> ∨ (∃a s. t = <Ev a> ^^ ss :t Tf aaX)} ∈ domT

lemma in_traces_Ext_pre_choice:

  (t :t traces (? :X -> Pf) M) =
  (t = <> ∨ (∃a s. t = <Ev a> ^^ ss :t traces (Pf a) MaX))

lemma in_traces_Ext_choice:

  (t :t traces (P [+] Q) M) = (t :t traces P Mt :t traces Q M)

lemma in_traces_Int_choice:

  (t :t traces (P |~| Q) M) = (t :t traces P Mt :t traces Q M)

lemma Rep_int_choice_domT:

  {t. t = <> ∨ (∃aX. t :t Tf a)} ∈ domT

lemma in_traces_Union_proc:

  (t :t {t. t = <> ∨ (∃aX. t :t Tf a)}t) = (t = <> ∨ (∃aX. t :t Tf a))

lemma in_traces_UNIV_Union_proc:

  (t :t {t. ∃a. t :t Tf a}t) = (∃a. t :t Tf a)

lemma in_traces_Rep_int_choice_sum:

  (t :t traces (!! :C .. Pf) M) = (t = <> ∨ (∃c∈sumset C. t :t traces (Pf c) M))

lemma in_traces_Rep_int_choice_nat:

  (t :t traces (!nat :N .. Pf) M) = (t = <> ∨ (∃nN. t :t traces (Pf n) M))

lemma in_traces_Rep_int_choice_set:

  (t :t traces (!set :Xs .. Pf) M) = (t = <> ∨ (∃XXs. t :t traces (Pf X) M))

lemma in_traces_Rep_int_choice_com:

  (t :t traces (! :X .. Pf) M) = (t = <> ∨ (∃aX. t :t traces (Pf a) M))

lemma in_traces_Rep_int_choice_f:

  inj f
  ==> (t :t traces (!<f> :X .. Pf) M) = (t = <> ∨ (∃aX. t :t traces (Pf a) M))

lemma in_traces_Rep_int_choice:

  (t :t traces (!! :C .. Pf) M) = (t = <> ∨ (∃c∈sumset C. t :t traces (Pf c) M))
  (t :t traces (!set :Xs .. Pf) M) = (t = <> ∨ (∃XXs. t :t traces (Pf X) M))
  (t :t traces (!nat :N .. Pf) M) = (t = <> ∨ (∃nN. t :t traces (Pf n) M))
  (t :t traces (! :X .. Pf) M) = (t = <> ∨ (∃aX. t :t traces (Pf a) M))
  inj f
  ==> (t :t traces (!<f> :X .. Pf) M) = (t = <> ∨ (∃aX. t :t traces (Pf a) M))

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)

lemma Parallel_domT:

  {u. ∃s t. us |[X]|tr ts :t Tt :t S} ∈ domT

lemma in_traces_Parallel:

  (u :t traces (P |[X]| Q) M) =
  (∃s t. us |[X]|tr ts :t traces P Mt :t traces Q M)

lemma Hiding_domT:

  {s --tr X |s. s :t T} ∈ domT

lemma in_traces_Hiding:

  (t :t traces (P -- X) M) = (∃s. t = s --tr Xs :t traces P M)

lemma Renaming_domT:

  {t. ∃s. s [[r]]* ts :t T} ∈ domT

lemma in_traces_Renaming:

  (t :t traces (P [[r]]) M) = (∃s. s [[r]]* ts :t traces P M)

lemma Seq_compo_domT:

  {u. (∃s. u = rmTick ss :t S) ∨
      (∃s t. u = s ^^ ts ^^ <Tick> :t St :t T ∧ noTick s)}
  ∈ domT

lemma in_traces_Seq_compo:

  (u :t traces (P ;; Q) M) =
  ((∃s. u = rmTick ss :t traces P M) ∨
   (∃s t. u = s ^^ ts ^^ <Tick> :t traces P Mt :t traces Q M ∧ noTick s))

lemma in_traces_Depth_rest:

  (t :t traces (P |. n) M) = (t :t traces P M ∧ lengtht t  n)

lemma in_traces_Proc_name:

  (t :t traces ($p) M) = (t :t M p)

lemma traces_domT:

  {t. t = <> ∨ (∃s. t = <Ev a> ^^ ss :t T)} ∈ domT
  {t. t = <> ∨ (∃a s. t = <Ev a> ^^ ss :t Tf aaX)} ∈ domT
  {t. t = <> ∨ (∃aX. t :t Tf a)} ∈ domT
  {u. ∃s t. us |[X]|tr ts :t Tt :t S} ∈ domT
  {s --tr X |s. s :t T} ∈ domT
  {t. ∃s. s [[r]]* ts :t T} ∈ domT
  {u. (∃s. u = rmTick ss :t S) ∨
      (∃s t. u = s ^^ ts ^^ <Tick> :t St :t T ∧ noTick s)}
  ∈ domT

lemma in_traces:

  (t :t traces STOP M) = (t = <>)
  (t :t traces SKIP M) = (t = <> ∨ t = <Tick>)
  (t :t traces DIV M) = (t = <>)
  (t :t traces (a -> P) M) = (t = <> ∨ (∃s. t = <Ev a> ^^ ss :t traces P M))
  (t :t traces (? :X -> Pf) M) =
  (t = <> ∨ (∃a s. t = <Ev a> ^^ ss :t traces (Pf a) MaX))
  (t :t traces (P [+] Q) M) = (t :t traces P Mt :t traces Q M)
  (t :t traces (P |~| Q) M) = (t :t traces P Mt :t traces Q M)
  (t :t traces (!! :C .. Pf) M) = (t = <> ∨ (∃c∈sumset C. t :t traces (Pf c) M))
  (t :t traces (!set :Xs .. Pf) M) = (t = <> ∨ (∃XXs. t :t traces (Pf X) M))
  (t :t traces (!nat :N .. Pf) M) = (t = <> ∨ (∃nN. t :t traces (Pf n) M))
  (t :t traces (! :X .. Pf) M) = (t = <> ∨ (∃aX. t :t traces (Pf a) M))
  inj f
  ==> (t :t traces (!<f> :X .. Pf) M) = (t = <> ∨ (∃aX. t :t traces (Pf a) M))
  (t :t traces (IF b THEN P ELSE Q) M) =
  (if b then t :t traces P M else t :t traces Q M)
  (u :t traces (P |[X]| Q) M) =
  (∃s t. us |[X]|tr ts :t traces P Mt :t traces Q M)
  (t :t traces (P -- X) M) = (∃s. t = s --tr Xs :t traces P M)
  (t :t traces (P [[r]]) M) = (∃s. s [[r]]* ts :t traces P M)
  (u :t traces (P ;; Q) M) =
  ((∃s. u = rmTick ss :t traces P M) ∨
   (∃s t. u = s ^^ ts ^^ <Tick> :t traces P Mt :t traces Q M ∧ noTick s))
  (t :t {t. t = <> ∨ (∃aX. t :t Tf a)}t) = (t = <> ∨ (∃aX. t :t Tf a))
  (t :t {t. ∃a. t :t Tf a}t) = (∃a. t :t Tf a)
  (t :t traces (P |. n) M) = (t :t traces P M ∧ lengtht t  n)
  (t :t traces ($p) M) = (t :t M p)

lemma in_traces_Timeout1:

  (t :t traces (P [> Q) M) = (t :t traces P Mt :t traces Q M)

lemma in_traces_Timeout2:

  (t :t traces (P [>def Q) M) = (t :t traces P Mt :t traces Q M)

lemma in_traces_Timeout:

  (t :t traces (P [> Q) M) = (t :t traces P Mt :t traces Q M)
  (t :t traces (P [>def Q) M) = (t :t traces P Mt :t traces Q M)