Theory CSP_F_failures

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

theory CSP_F_failures
imports CSP_F_semantics

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

theory CSP_F_failures
imports CSP_F_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]

(*********************************************************
                        setF
 *********************************************************)

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

(*** STOP_setF ***)

lemma STOP_setF: "{f. EX X. f = (<>, X)} : setF"
by (simp add: setF_def HC_F2_def)

(*** STOP ***)

lemma in_failures_STOP : "(f :f failures(STOP) M) = (EX X. f = (<>, X))"
apply (simp add: failures_def)
by (simp add: CollectF_open_memF STOP_setF)

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

(*** SKIP_setF ***)

lemma SKIP_setF: "{f. (EX X. f = (<>, X) & X <= Evset) |
                      (EX X. f = (<Tick>, X)) } : setF"
by (auto simp add: setF_def HC_F2_def)

(*** SKIP ***)

lemma in_failures_SKIP :
  "(f :f failures(SKIP) M) = ((EX X. f = (<>, X) & X <= Evset) |
                              (EX X. f = (<Tick>, X)))"
apply (simp add: failures_def)
by (simp add: CollectF_open_memF SKIP_setF)

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

(*** DIV ***)

lemma in_failures_DIV : "(f ~:f failures(DIV) M)"
by (simp add: failures_def)

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

(*** Act_prefix_setF ***)

lemma Act_prefix_setF: 
  "{f. (EX X.   f = (<>,X) & Ev a ~: X) |
       (EX s X. f = (<Ev a> ^^ s, X) & (s,X) :f F) } : setF"
apply (simp add: setF_def HC_F2_def)
apply (intro allI impI)
apply (elim conjE disjE, force)

apply (elim conjE exE, simp)
apply (rule memF_F2, simp_all)
done

(*** Act_prefix ***)

lemma in_failures_Act_prefix: 
  "(f :f failures(a -> P) M) 
    = ((EX X.   f = (<>,X) & Ev a ~: X) |
       (EX s X. f = (<Ev a> ^^ s, X) & (s,X) :f failures(P) M))"
apply (simp add: failures_def)
by (simp add: CollectF_open_memF Act_prefix_setF)

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

(*** Ext_pre_choice_setF ***)

lemma Ext_pre_choice_setF: 
  "{f. (EX Y. f = (<>,Y) & Ev`X Int Y = {}) |
       (EX a s Y. f = (<Ev a> ^^ s, Y) & (s,Y) :f Ff a & a : X) } : setF"
apply (simp add: setF_def HC_F2_def)
apply (intro allI impI)
apply (elim conjE disjE, force)

apply (elim conjE exE, simp)
apply (rule memF_F2, simp_all)
done

(*** Ext_pre_choice ***)

lemma in_failures_Ext_pre_choice: 
  "(f :f failures(? :X -> Pf) M) = 
   ((EX Y.     f = (<>,Y) & Ev`X Int Y = {}) |
    (EX a s Y. f = (<Ev a> ^^ s, Y) & (s,Y) :f failures(Pf a) M & a : X))"
apply (simp add: failures_def)
by (simp add: CollectF_open_memF Ext_pre_choice_setF)

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

(*** Ext_choice_setF ***)

lemma Ext_choice_setF: 
  "{f. (EX X. f = (<>, X)) & f :f F & f :f E |
              (EX s. (EX X. f = (s, X)) & (f :f F | f :f E) & s ~= <>) |
              (EX X. f = (<>, X) &
                     (<Tick> :t T | <Tick> :t S) & X <= Evset)} : setF"
apply (simp add: setF_def HC_F2_def)
apply (intro allI impI)
apply (elim conjE disjE)
apply (simp_all)

(* part1 *)
apply (rule disjI1)
apply (rule conjI)
apply (rule memF_F2, simp_all)
apply (rule memF_F2, simp_all)

(* part2 *)
apply (rule disjI1)
apply (rule memF_F2, simp_all)
apply (rule disjI2)
apply (rule memF_F2, simp_all)

(* part3 *)
apply (auto)
done

(*** Ext_choice ***)

lemma in_failures_Ext_choice: 
  "(f :f failures(P [+] Q) M) =
    ((EX X. f = (<>, X)) & f :f failures P M & f :f failures Q M |
     (EX s. (EX X. f = (s, X)) &
            (f :f failures P M | f :f failures Q M) & s ~= <>) |
     (EX X. f = (<>, X) &
            (<Tick> :t traces P (fstF o M) | <Tick> :t traces Q (fstF o M)) & X <= Evset))"
apply (simp add: failures_def)
by (simp only: CollectF_open_memF Ext_choice_setF)

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

(*** Int_choice ***)

lemma in_failures_Int_choice: 
  "(f :f failures(P |~| Q) M) = (f :f failures(P) M | f :f failures(Q) M)"
by (simp add: failures_def)

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

(*** Rep_int_choice_setF ***)

lemma Rep_int_choice_setF: 
  "{f. EX a:X. f :f Ff a} : setF"
apply (simp add: setF_def HC_F2_def)
apply (intro allI impI)
apply (elim conjE bexE)
apply (rule_tac x="a" in bexI)
apply (rule memF_F2, simp_all)
done

(*** Union_proc ***)

lemma in_failures_Union_proc:
   "f :f {f. EX a:X. f :f Ff a}f = (EX a:X. f :f Ff a)"
by (simp add: CollectF_open_memF Rep_int_choice_setF)

lemma in_failures_UNIV_Union_proc:
   "f :f {f. EX a. f :f Ff a}f = (EX a. f :f Ff a)"
apply (insert in_failures_Union_proc[of f UNIV Ff])
by (simp)

(*** Rep_int_choice ***)

lemma in_failures_Rep_int_choice_sum: 
  "(f :f failures(!! :C .. Pf) M) = (EX c: sumset C. f :f failures(Pf c) M)"
apply (simp add: failures_def)
by (simp add: in_failures_Union_proc)

lemma in_failures_Rep_int_choice_nat: 
  "(f :f failures(!nat :N .. Pf) M) = (EX n:N. f :f failures(Pf n) M)"
by (simp add: Rep_int_choice_ss_def in_failures_Rep_int_choice_sum)

lemma in_failures_Rep_int_choice_set: 
  "(f :f failures(!set :Xs .. Pf) M) = (EX X:Xs. f :f failures(Pf X) M)"
by (simp add: Rep_int_choice_ss_def in_failures_Rep_int_choice_sum)

lemma in_failures_Rep_int_choice_com: 
  "(f :f failures(! :X .. Pf) M) = (EX a:X. f :f failures(Pf a) M)"
apply (simp add: failures_def)
by (simp add: in_failures_Union_proc)

lemma in_failures_Rep_int_choice_f: 
  "inj g ==>
   (f :f failures(!<g> :X .. Pf) M) = (EX a:X. f :f failures(Pf a) M)"
apply (simp add: failures_def)
by (simp add: in_failures_Union_proc)

lemmas in_failures_Rep_int_choice =
       in_failures_Rep_int_choice_sum
       in_failures_Rep_int_choice_nat
       in_failures_Rep_int_choice_set
       in_failures_Rep_int_choice_com
       in_failures_Rep_int_choice_f

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

(*** IF ***)

lemma in_failures_IF: 
  "(f :f failures(IF b THEN P ELSE Q) M)
 = (if b then f :f failures(P) M else f :f failures(Q) M)"
by (simp add: failures_def)

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

(*** Parallel_setF ***)

lemma Parallel_setF : 
  "{(u, Y Un Z) |u Y Z.
     Y - insert Tick (Ev ` X) = Z - insert Tick (Ev ` X) &
     (EX s t. u : s |[X]|tr t & (s, Y) :f F & (t, Z) :f E)}
    : setF"
apply (simp add: setF_def HC_F2_def)
apply (intro allI impI)
apply (elim conjE exE, simp)
apply (rename_tac u Y Z Y1 Y2 s t)
apply (rule_tac x="Z Int (Y1 - (Y2 - insert Tick (Ev ` X))) Un
                   Z Int (Y2 - insert Tick (Ev ` X))" in exI)
apply (rule_tac x="Z Int (Y2 - (Y2 - insert Tick (Ev ` X))) Un
                   Z Int (Y2 - insert Tick (Ev ` X))" in exI)

(* (s,Y), Z <= Y, Y = Y1 Un Y2, Z = Z1 Un Z2 *)

apply (rule conjI, force)
apply (rule conjI, force)

apply (rule_tac x="s" in exI)
apply (rule_tac x="t" in exI)
apply (simp)
apply (rule conjI)
apply (rule memF_F2, simp, force)+
done

lemma in_failures_Parallel:
  "(f :f failures(P |[X]| Q) M) = 
   (EX u Y Z. f = (u, Y Un Z) & Y - insert Tick (Ev ` X) = Z - insert Tick (Ev ` X) &
      (EX s t. u : s |[X]|tr t & (s,Y) :f failures(P) M & (t,Z) :f failures(Q) M))"
apply (simp add: failures_def)
by (simp only: CollectF_open_memF Parallel_setF)

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

(*** Hiding_setF ***)

lemma Hiding_setF : 
  "{f. EX s Y. f = (s --tr X, Y) & (s,(Ev`X) Un Y) :f F} : setF"
apply (simp add: setF_def HC_F2_def)
apply (intro allI impI)
apply (elim conjE exE, simp)
apply (rename_tac t Y Z s)
apply (rule_tac x="s" in exI)
apply (simp)
by (rule memF_F2, simp, force)

lemma in_failures_Hiding:
  "(f :f failures(P -- X) M) = 
   (EX s Y. f = (s --tr X, Y) & (s,(Ev`X) Un Y) :f failures(P) M)"
apply (simp add: failures_def)
by (simp only: CollectF_open_memF Hiding_setF)

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

(*** Renaming_setF ***)

lemma Renaming_setF : 
  "{f. EX s t X. f = (t,X) & (s [[r]]* t) & 
                 (s, [[r]]inv X) :f F } : setF"
apply (simp add: setF_def HC_F2_def)
apply (intro allI impI)
apply (elim conjE exE)
apply (rule_tac x="sa" in exI)
apply (simp)
apply (rule memF_F2, simp)
apply (rule ren_inv_sub, simp)
done

lemma in_failures_Renaming:
  "(f :f failures(P[[r]]) M) =
   (EX s t X. f = (t,X) & s [[r]]* t & (s, [[r]]inv X) :f failures(P) M)"
apply (simp add: failures_def)
by (simp only: CollectF_open_memF Renaming_setF)

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

(*** Seq_compo_setF ***)

lemma Seq_compo_setF : 
  "{f. (EX t X. f = (t, X) & (t, insert Tick X) :f F & noTick t) |
        (EX s t X.
            f = (s ^^ t, X) & s ^^ <Tick> :t T & (t, X) :f E & noTick s)}
    : setF"
apply (simp add: setF_def HC_F2_def)
 apply (intro allI impI)
 apply (elim conjE exE disjE)

  (* case 1 *)
  apply (rule disjI1, simp)
  apply (rule memF_F2, simp, force)

  (* case 2 *)
  apply (rule disjI2)
  apply (rule_tac x="sa" in exI)
  apply (rule_tac x="t" in exI)
  apply (simp)
  apply (rule memF_F2, simp, simp)
done

lemma in_failures_Seq_compo:
  "(f :f failures(P ;; Q) M) =
   ((EX t X.   f = (t,X) & (t, X Un {Tick}) :f failures(P) M & noTick t) |
    (EX s t X. f = (s ^^ t,X) & s ^^ <Tick> :t traces(P) (fstF o M)
               & (t, X) :f failures(Q) M & noTick s))"
apply (simp add: failures_def)
by (simp only: CollectF_open_memF Seq_compo_setF)

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

(*** Depth_rest ***)

lemma in_failures_Depth_rest:
  "(f :f failures(P |. n) M) =
   (EX t X. f = (t,X) & (t, X) :f  failures(P) M &
                (lengtht t < n |
                 lengtht t = n & (EX s. t = s ^^ <Tick> & noTick s)))"
apply (simp add: failures_def)
apply (subgoal_tac "EX t X. f = (t, X)")
apply (elim exE)
apply (simp add: in_rest_setF)
apply (auto)
done

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

(*** Proc_name ***)

lemma in_failures_Proc_name:
  "(f :f failures($p) M) = (f :f  sndF(M p))"
apply (simp add: failures_def)
done

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

lemmas failures_setF = STOP_setF       SKIP_setF
                       Act_prefix_setF Ext_pre_choice_setF
                       Ext_choice_setF Rep_int_choice_setF
                       Parallel_setF   Hiding_setF
                       Renaming_setF   Seq_compo_setF

lemmas in_failures = in_failures_STOP  in_failures_SKIP  in_failures_DIV
                     in_failures_Act_prefix     in_failures_Ext_pre_choice
                     in_failures_Ext_choice     in_failures_Int_choice
                     in_failures_Rep_int_choice in_failures_IF
                     in_failures_Parallel       in_failures_Hiding
                     in_failures_Renaming       in_failures_Seq_compo
                     in_failures_Union_proc     in_failures_UNIV_Union_proc
                     in_failures_Depth_rest     in_failures_Proc_name

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

declare disj_not1   [simp]

end