Theory Seq_compo (Isabelle2004: April 2004)

           (*-------------------------------------------*
            |                CSP-Prover                 |
            |               December 2004               |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory Seq_compo = CSP_semantics:

(*  The following simplification rules are deleted in this theory file *)
(*  because they unexpectly rewrite (notick | t = []t)                 *)
(*                                                                     *)
(*                  disj_not1: (~ P | Q) = (P --> Q)                   *)

declare disj_not1 [simp del]

(*  The following simplification is sometimes unexpected.              *)
(*                                                                     *)
(*             not_None_eq: (x ~= None) = (EX y. x = Some y)           *)

declare not_None_eq [simp del]

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

(*** Seq_compo_domT ***)

lemma Seq_compo_domT : 
  "{u. (EX s. u = rmtick s & s :t [[P]]T ev) |
       (EX s t. u = s @t t & s @t [Tick]t :t [[P]]T ev & t :t [[Q]]T ev)} : domT"
apply (simp add: domT_def HC_T1_def)
apply (rule conjI)
apply (rule_tac x="[]t" in exI, simp)
apply (rule disjI1)
apply (rule_tac x="[]t" in exI, simp)

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

 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 (erule disjE, simp)         (* None --> contra *)
  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 (erule exE)
  apply (case_tac "~ notick sa", simp)
  apply (case_tac "sa @t ta = None", simp add: not_None)
  apply (simp add: appt_decompo)

   apply (erule disjE)
   (* long case *)
   apply (elim conjE exE)
   apply (rule disjI2)
   apply (rule_tac x="sa" in exI)
   apply (rule_tac x="ua" in exI)
   apply (simp)
   apply (subgoal_tac "prefix ua (ua @t 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 @t ua @t [Tick]t)")
    apply (rule memT_prefix_closed, simp_all)
   apply (simp)

(* not None *)
apply (intro allI)
apply (case_tac "notick s & t ~= None")
apply (erule conjE)
apply (simp add: decompo_appt_not_None not_None)
by (auto)

(*** Seq_compo_memT ***)

lemma Seq_compo_memT:
  "(u :t [[P ;; Q]]T ev) = 
   ((EX s. u = rmtick s & s :t [[P]]T ev) |
    (EX s t. u = s @t t & s @t [Tick]t :t [[P]]T ev & t :t [[Q]]T ev))"
apply (simp add: evalT_def)
by (simp add: memT_def Abs_domT_inverse Seq_compo_domT[simplified memT_def])

(*********************************************************
                         DomF
 *********************************************************)

(*** Seq_compo_domF ***)

lemma Seq_compo_domF : 
  "{f. (EX t X.   f = (t,X) & (t, X Un {Tick}) :f [[P]]F ev & notick t) |
       (EX s t X. f = (s @t t,X) & s @t [Tick]t :t [[P]]T ev & (t, X) :f [[Q]]F ev) }
   : domF"
apply (simp add: domF_def HC_F2_def)
apply (intro conjI)
 apply (intro allI impI)
 apply (elim conjE exE)

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

  (* case 2 *)
  apply (elim conjE exE)
  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)

(* not None *)
apply (intro allI)
apply (case_tac "notick s & t ~= None")
apply (erule conjE)
apply (simp add: decompo_appt_not_None not_None)
by (auto)

lemma Seq_compo_memF:
  "(f :f [[P ;; Q]]F ev) = 
   ((EX t X.   f = (t,X) & (t, X Un {Tick}) :f [[P]]F ev & notick t) |
    (EX s t X. f = (s @t t,X) & s @t [Tick]t :t [[P]]T ev & (t, X) :f [[Q]]F ev))"
apply (simp only: evalF_def)
apply (simp only: memF_def Abs_domF_inverse Seq_compo_domF[simplified memF_def])
by (simp)

lemmas Seq_compo_mem = Seq_compo_memT Seq_compo_memF

(*********************************************************
                         domSF
 *********************************************************)

(*** T2 ***)

lemma Seq_compo_T2 :
  "[| ([[P]]T ev, [[P]]F ev) : domSF ; ([[Q]]T ev, [[Q]]F ev) : domSF |]
     ==> HC_T2 ([[P ;; Q]]T ev, [[P ;; Q]]F ev)"
apply (simp add: HC_T2_def Seq_compo_mem)
apply (intro allI)
apply (rule conjI)

 (* case 1 *)
 apply (intro impI)
 apply (rule disjI1)
 apply (rule_tac x="s" in exI, simp)
 apply (simp add: domSF_def HC_T2_def)
 apply (elim conjE)
 apply (drule_tac x="s" in spec)
 apply (force)

 (* case 2 *)
 apply (intro impI)
 apply (elim conjE exE disjE)
 apply (rule disjI2)
 apply (rule_tac x="sa" in exI)
 apply (rule_tac x="t" in exI)
 apply (simp add: domSF_def HC_T2_def)
 apply (elim conjE)
 apply (rotate_tac 4)
 apply (drule_tac x="t" in spec)
 apply (force)
done

(*** F3 ***)

lemma Seq_compo_F3 :
  "[| ([[P]]T ev, [[P]]F ev) : domSF ; ([[Q]]T ev, [[Q]]F ev) : domSF |]
     ==> HC_F3 ([[P ;; Q]]T ev, [[P ;; Q]]F ev)"
apply (simp add: HC_F3_def Seq_compo_mem)
apply (intro allI impI)
apply (elim conjE exE disjE)

 (* case 1 *)
 apply (simp add: domSF_def HC_F3_def)
 apply (elim conjE)
 apply (drule_tac x="s" in spec)
 apply (drule_tac x="insert Tick X" in spec)
 apply (drule_tac x="Y-{Tick}" in spec)
 apply (simp)
 apply (drule mp)
  apply (intro allI impI)
  apply (drule_tac x="a" in spec, simp)
  apply (simp add: not_tick_to_Ev)
  apply (elim conjE exE, simp)
  apply (rotate_tac -3)
  apply (drule_tac x="s @t [Ev aa]t" in spec, simp)
 apply (subgoal_tac 
   "insert Tick (X Un (Y - {Tick})) = insert Tick (X Un Y)", simp)
 apply (force)

 (* case 2 *)
 apply (simp add: domSF_def HC_F3_def)
 apply (elim conjE)
 apply (rotate_tac -2)
 apply (drule_tac x="t" in spec)
 apply (drule_tac x="X" in spec)
 apply (drule_tac x="Y" in spec)
 apply (simp)
 apply (drule mp)
  apply (intro allI impI)
  apply (drule_tac x="a" in spec, simp)
  apply (elim conjE)
  apply (rotate_tac -1)
  apply (drule_tac x="sa" in spec)
  apply (rotate_tac -1)
  apply (drule_tac x="t @t [a]t" in spec)
  apply (simp)
 apply (rule disjI2)
 apply (rule_tac x="sa" in exI)
 apply (rule_tac x="t" in exI)
 apply (simp)
done

(* T3_F4 *)

lemma Seq_compo_T3_F4 :
  "[| ([[P]]T ev, [[P]]F ev) : domSF ; ([[Q]]T ev, [[Q]]F ev) : domSF |]
     ==> HC_T3_F4 ([[P ;; Q]]T ev, [[P ;; Q]]F ev)"
apply (simp add: HC_T3_F4_def Seq_compo_mem)
apply (intro allI impI)
apply (elim conjE disjE)

 (* case 1 *)
 apply (elim conjE exE)
 apply (subgoal_tac "notick (s @t [Tick]t) ~= notick (rmtick sa)", simp)
 apply (simp (no_asm_use))
 apply (simp add: not_None)

 (* case 2 *)
 apply (elim conjE exE)
 apply (case_tac "~ notick sa", simp)
 apply (insert trace_last_nil_or_unnil)
 apply (drule_tac x="t" in spec)
 apply (simp add: not_None)
  (* []t *)
  apply (erule disjE)
  apply (rotate_tac -5)
  apply (drule_tac sym, simp)   (* contradict *)

  (* ... [Tick]t *)
  apply (elim conjE exE, simp)
  apply (simp add: appt_ass_rev del: appt_ass)
  apply (erule conjE)

  apply (rule conjI)

   (* F4 *)
   apply (rule disjI2)
   apply (rule_tac x="sa" in exI)
   apply (rule_tac x="sb" in exI)
   apply (simp add: domSF_def HC_F4_def)

   (* T3 *)
   apply (rule allI)
   apply (rule_tac x="sa" in exI)
   apply (rule_tac x="t" in exI)
   apply (simp add: domSF_def HC_T3_def)
done

(*** Seq_compo_domSF ***)

lemma Seq_compo_domSF :
  "[| ([[P]]T ev, [[P]]F ev) : domSF ; ([[Q]]T ev, [[Q]]F ev) : domSF |]
     ==> ([[P ;; Q]]T ev, [[P ;; Q]]F ev) : domSF"
apply (simp (no_asm) add: domSF_iff)
apply (simp add: Seq_compo_T2)
apply (simp add: Seq_compo_F3)
apply (simp add: Seq_compo_T3_F4)
done

(*********************************************************
                      mono
 *********************************************************)

(*** T ***)

lemma Seq_compo_evalT_mono:
  "[| [[P1]]T ev1 <= [[P2]]T ev2 ; [[Q1]]T ev1 <= [[Q2]]T ev2 |]
   ==> [[P1 ;; Q1]]T ev1 <= [[P2 ;; Q2]]T ev2"
apply (simp add: subsetT_iff)
apply (intro allI impI)
apply (simp add: Seq_compo_memT)

 apply (elim conjE exE disjE)
 apply (rule disjI1)
 apply (rule_tac x="s" in exI)
 apply (simp)

 apply (rule disjI2)
 apply (rule_tac x="s" in exI)
 apply (rule_tac x="ta" in exI)
 apply (simp)
done

(*** F ***)

lemma Seq_compo_evalF_mono:
  "[| [[P1]]T ev1 <= [[P2]]T ev2 ; 
      [[P1]]F ev1 <= [[P2]]F ev2 ; [[Q1]]F ev1 <= [[Q2]]F ev2 |]
   ==> [[P1 ;; Q1]]F ev1 <= [[P2 ;; Q2]]F ev2"
apply (simp add: subsetF_iff subsetT_iff)
apply (intro allI impI)
apply (simp add: Seq_compo_memF)

apply (erule disjE, simp)
apply (elim conjE exE)
apply (rule disjI2)
apply (rule_tac x="sa" in exI)
apply (rule_tac x="t" in exI)
by (simp)

(****************** to add it again ******************)

declare disj_not1   [simp] 
declare not_None_eq [simp]

end

lemma Seq_compo_domT:

  {u. (∃s. u = rmtick s ∧ s :t [[P]]T ev) ∨
      (∃s t. u = s @t t ∧ s @t [Tick]t :t [[P]]T ev ∧ t :t [[Q]]T ev)}
  ∈ domT

lemma Seq_compo_memT:

  (u :t [[P ;; Q]]T ev) =
  ((∃s. u = rmtick s ∧ s :t [[P]]T ev) ∨
   (∃s t. u = s @t t ∧ s @t [Tick]t :t [[P]]T ev ∧ t :t [[Q]]T ev))

lemma Seq_compo_domF:

  {f. (∃t X. f = (t, X) ∧ (t, X ∪ {Tick}) :f [[P]]F ev ∧ notick t) ∨
      (∃s t X. f = (s @t t, X) ∧ s @t [Tick]t :t [[P]]T ev ∧ (t, X) :f [[Q]]F ev)}
  ∈ domF

lemma Seq_compo_memF:

  (f :f [[P ;; Q]]F ev) =
  ((∃t X. f = (t, X) ∧ (t, X ∪ {Tick}) :f [[P]]F ev ∧ notick t) ∨
   (∃s t X. f = (s @t t, X) ∧ s @t [Tick]t :t [[P]]T ev ∧ (t, X) :f [[Q]]F ev))

lemmas Seq_compo_mem:

  (u :t [[P ;; Q]]T ev) =
  ((∃s. u = rmtick s ∧ s :t [[P]]T ev) ∨
   (∃s t. u = s @t t ∧ s @t [Tick]t :t [[P]]T ev ∧ t :t [[Q]]T ev))

  (f :f [[P ;; Q]]F ev) =
  ((∃t X. f = (t, X) ∧ (t, X ∪ {Tick}) :f [[P]]F ev ∧ notick t) ∨
   (∃s t X. f = (s @t t, X) ∧ s @t [Tick]t :t [[P]]T ev ∧ (t, X) :f [[Q]]F ev))

lemma Seq_compo_T2:

  [| ([[P]]T ev, [[P]]F ev) ∈ domSF; ([[Q]]T ev, [[Q]]F ev) ∈ domSF |]
  ==> HC_T2 ([[P ;; Q]]T ev, [[P ;; Q]]F ev)

lemma Seq_compo_F3:

  [| ([[P]]T ev, [[P]]F ev) ∈ domSF; ([[Q]]T ev, [[Q]]F ev) ∈ domSF |]
  ==> HC_F3 ([[P ;; Q]]T ev, [[P ;; Q]]F ev)

lemma Seq_compo_T3_F4:

  [| ([[P]]T ev, [[P]]F ev) ∈ domSF; ([[Q]]T ev, [[Q]]F ev) ∈ domSF |]
  ==> HC_T3_F4 ([[P ;; Q]]T ev, [[P ;; Q]]F ev)

lemma Seq_compo_domSF:

  [| ([[P]]T ev, [[P]]F ev) ∈ domSF; ([[Q]]T ev, [[Q]]F ev) ∈ domSF |]
  ==> ([[P ;; Q]]T ev, [[P ;; Q]]F ev) ∈ domSF

lemma Seq_compo_evalT_mono:

  [| [[P1]]T ev1 ≤ [[P2]]T ev2; [[Q1]]T ev1 ≤ [[Q2]]T ev2 |]
  ==> [[P1 ;; Q1]]T ev1 ≤ [[P2 ;; Q2]]T ev2

lemma Seq_compo_evalF_mono:

  [| [[P1]]T ev1 ≤ [[P2]]T ev2; [[P1]]F ev1 ≤ [[P2]]F ev2;
     [[Q1]]F ev1 ≤ [[Q2]]F ev2 |]
  ==> [[P1 ;; Q1]]F ev1 ≤ [[P2 ;; Q2]]F ev2