Theory Domain_SF (Isabelle2004: April 2004)

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

theory Domain_SF = Domain_T + Domain_F:

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

         1. 
         2. 
         3. 
         4. 

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

(*  The following simplification rules are deleted in this theory file *)
(*  because they unexpectly rewrite UnionT and InterT.                 *)
(*                  Union (B ` A) = (UN x:A. B x)                      *)
(*                  Inter (B ` A) = (INT x:A. B x)                     *)

declare Union_image_eq [simp del]
declare Inter_image_eq [simp del]

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

declare not_None_eq [simp del]

(*********************************************************
                      not_None
 *********************************************************)

lemmas not_None = not_None not_None_T not_None_F

(***********************************************************
                 type def (Stable Failure)
 ***********************************************************)

types 'a domTF = "'a domT * 'a domF"       (* synonym *)

consts
  HC_T2    :: "'a domTF => bool"
  HC_T3    :: "'a domTF => bool"
  HC_F3    :: "'a domTF => bool"
  HC_F4    :: "'a domTF => bool"
  HC_T3_F4 :: "'a domTF => bool"

defs
  HC_T2_def : 
    "HC_T2 TF == ALL s X. (s, X) :f (snd TF)
                --> s :t (fst TF)"

  HC_T3_def : 
    "HC_T3 TF == ALL s. s @t [Tick]t :t (fst TF) & notick s
                --> (ALL X. (s @t [Tick]t, X) :f (snd TF))"

  HC_F3_def : 
    "HC_F3 TF == ALL s X Y. (s, X) :f (snd TF) & notick s &
                          (ALL a. a : Y --> s @t [a]t ~:t fst TF)
                --> (s, X Un Y) :f (snd TF)"

  HC_F4_def : 
    "HC_F4 TF == ALL s. s @t [Tick]t :t (fst TF) & notick s
                --> (s, Evset) :f (snd TF)"

  HC_T3_F4_def : 
    "HC_T3_F4 TF == ALL s. s @t [Tick]t :t (fst TF) & notick s
                    --> ((s, Evset) :f (snd TF) &
                         (ALL X. (s @t [Tick]t, X) :f (snd TF)))"

lemma HC_T3_F4_iff : "HC_T3_F4 TF = (HC_T3 TF & HC_F4 TF)"
apply (simp add: HC_T3_F4_def HC_T3_def HC_F4_def)
by (auto)

(*** BOT in SF ***)

lemma BOT_SF: "HC_T2({[]t}t , {}f) & HC_F3({[]t}t , {}f) & 
               HC_T3_F4({[]t}t , {}f)"
by (simp add: HC_T2_def HC_F3_def HC_T3_F4_def)

(*******************************
           Type SF
 *******************************)

typedef 'a domSF = "{SF::('a domTF). HC_T2(SF) & HC_T3(SF) & HC_F3(SF) & HC_F4(SF)}"
apply (rule_tac x ="({[]t}t , {}f)" in exI)
by (simp add: BOT_SF HC_T3_F4_iff[THEN sym])

declare Rep_domSF         [simp]

lemma domSF_iff: "domSF = {SF. HC_T2 SF & HC_F3 SF & HC_T3_F4 SF}"
by (auto simp add: domSF_def HC_T3_F4_iff)

(*********************************************************
          The relation (<=) is defined over domSF
 *********************************************************)

instance domSF :: (type) ord 
by (intro_classes)

defs (overloaded)
  subsetSF_def   :  "SF <= SE  ==  (Rep_domSF SF) <= (Rep_domSF SE)"
  psubsetSF_def  :  "SF <  SE  ==  (Rep_domSF SF) <  (Rep_domSF SE)"

(*********************************************************
          The relation (<=) is a partial order
 *********************************************************)

instance domSF :: (type) order
apply (intro_classes)
apply (unfold subsetSF_def psubsetSF_def)
apply (simp)
apply (erule order_trans, simp)
apply (drule order_antisym, simp)
apply (simp add: Rep_domSF_inject)
apply (simp only: order_less_le Rep_domSF_inject)
done

(***********************************************************
                          lemmas
 ***********************************************************)

(*******************************
              basic
 *******************************)

(*** T2 ***)

lemma domTF_T2:
    "[| TF : domSF ; (s, X) :f snd TF |] ==> s :t fst TF"
by (auto simp add: domSF_def HC_T2_def)

lemma domSF_T2:
    "[| (T,F) : domSF ; (s, X) :f F |] ==> s :t T"
by (auto simp add: domSF_def HC_T2_def)

(*** T3 ***)

lemma domTF_T3:
  "[| TF : domSF ; s @t [Tick]t :t fst TF ; notick s |]
   ==> (s @t [Tick]t, X) :f snd TF"
by (simp add: domSF_def HC_T3_def)

lemma domSF_T3:
  "[| (T,F) : domSF ; s @t [Tick]t :t T ; notick s |]
   ==> (s @t [Tick]t, X) :f F"
by (simp add: domSF_def HC_T3_def)

(*** F3 ***)

lemma domTF_F3:
  "[| TF : domSF ; (s, X) :f snd TF ; notick s ;
      (ALL a. a : Y --> s @t [a]t ~:t fst TF) |]
   ==> (s, X Un Y) :f snd TF"
by (simp add: domSF_def HC_F3_def)

lemma domSF_F3:
  "[| (T,F) : domSF ; (s, X) :f F ; notick s ;
      (ALL a. a : Y --> s @t [a]t ~:t T) |]
   ==> (s, X Un Y) :f F"
by (simp add: domSF_def HC_F3_def)

(*** F4 ***)

lemma domTF_F4:
  "[| TF : domSF ; s @t [Tick]t :t fst TF ; notick s |]
   ==> (s, Evset) :f snd TF"
by (simp add: domSF_def HC_F4_def)

lemma domSF_F4:
  "[| (T,F) : domSF ; s @t [Tick]t :t T ; notick s |]
   ==> (s, Evset) :f F"
by (simp add: domSF_def HC_F4_def)

(*** T3_F4 ***)

lemma domTF_T3_F4:
  "[| TF : domSF ; s @t [Tick]t :t fst TF ; notick s |]
   ==> (s, Evset) :f snd TF & (ALL X. (s @t [Tick]t, X) :f snd TF)"
by (simp add: domSF_iff HC_T3_F4_def)

lemma domSF_T3_F4:
  "[| (T,F) : domSF ; s @t [Tick]t :t T ; notick s |]
   ==> (s, Evset) :f F & (ALL X. (s @t [Tick]t, X) :f F)"
by (simp add: domSF_iff HC_T3_F4_def)

(*** F2_F4 ***)

lemma domTF_F2_F4:
  "[| TF : domSF ; s @t [Tick]t :t fst TF ; notick s ; X <= Evset |]
   ==> (s, X) :f snd TF"
apply (simp add: domSF_def HC_F4_def)
by (auto intro: memF_F2)

lemma domSF_F2_F4:
  "[| (T,F) : domSF ; s @t [Tick]t :t T ; notick s ; X <= Evset |]
   ==> (s, X) :f F"
apply (insert domTF_F2_F4[of "(T,F)" s X])
by (simp)

(*******************************
         check in domSF
 *******************************)

(*** ({[]t}t, {}f) ***)

lemma BOT_in_domSF[simp]: "({[]t}t, {}f) : domSF"
by (simp add: domSF_iff BOT_SF)

(*******************************
       BOT is the bottom
 *******************************)

lemma BOT_is_bottom_domSF[simp]: "({[]t}t , {}f) <= SF"
by (simp add: order_pair_def)

(***********************************************************
                   operators on domSF
 ***********************************************************)

consts
  pairSF :: "'a domT => 'a domF => 'a domSF"  ("(0_ ,,/ _)" [51,52] 0)

  fstSF  :: "'a domSF => 'a domT"
  sndSF  :: "'a domSF => 'a domF"

defs
  pairSF_def : "(S,,F)  == Abs_domSF (S, F)"
  fstSF_def  : "fstSF   == fst o Rep_domSF"
  sndSF_def  : "sndSF   == snd o Rep_domSF"

(***********************************************************
                     pairSF lemmas
 ***********************************************************)

lemma pairSF_fstSF: "(S,F) : domSF ==> fstSF (S,,F) = S"
apply (simp add: pairSF_def fstSF_def)
by (simp add: Abs_domSF_inverse)

lemma pairSF_sndSF: "(S,F) : domSF ==> sndSF (S,,F) = F"
apply (simp add: pairSF_def sndSF_def)
by (simp add: Abs_domSF_inverse)

lemma eqSF_decompo: 
  "(SF = SE) = (fstSF SF = fstSF SE & sndSF SF = sndSF SE)"
apply (simp add: Rep_domSF_inject[THEN sym])
apply (simp add: pair_eq_decompo)
apply (simp add: fstSF_def sndSF_def)
done

lemmas pairSF = pairSF_fstSF pairSF_sndSF eqSF_decompo

(*********************************************************
                      subsetSF
 *********************************************************)

lemma subsetSF_decompo: 
  "(SF <= SE) = (fstSF SF <= fstSF SE & sndSF SF <= sndSF SE)"
apply (simp add: subsetSF_def)
apply (simp add: order_pair_def)
apply (simp add: fstSF_def sndSF_def)
done

(*********************************************************
                       memTF
 *********************************************************)

lemmas memTF_def = memT_def memF_def

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

declare Union_image_eq [simp]
declare Inter_image_eq [simp]
declare not_None_eq    [simp]

end

lemmas not_None:

  notick t ==> t ≠ None

  notick s ==> s @t [e]t ≠ None

  notick s ==> None ≠ s @t [e]t

  [| notick s; t ≠ None |] ==> s @t t ≠ None

  s ≠ None ==> [Ev a]t @t s ≠ None

  [| s ≠ None; s ≠ []t |] ==> tlt s ≠ None

  [| s ≠ None; s ≠ []t |] ==> butlastt s ≠ None

  [| t ∈ T; T ∈ domT |] ==> t ≠ None

  t :t T ==> t ≠ None

  [| (s, X) ∈ F; F ∈ domF |] ==> s ≠ None

  (s, X) :f F ==> s ≠ None

lemma HC_T3_F4_iff:

  HC_T3_F4 TF = (HC_T3 TF ∧ HC_F4 TF)

lemma BOT_SF:

  HC_T2 ({[]t}t, {}f) ∧ HC_F3 ({[]t}t, {}f) ∧ HC_T3_F4 ({[]t}t, {}f)

lemma domSF_iff:

  domSF = {SF. HC_T2 SF ∧ HC_F3 SF ∧ HC_T3_F4 SF}

lemma domTF_T2:

  [| TF ∈ domSF; (s, X) :f snd TF |] ==> s :t fst TF

lemma domSF_T2:

  [| (T, F) ∈ domSF; (s, X) :f F |] ==> s :t T

lemma domTF_T3:

  [| TF ∈ domSF; s @t [Tick]t :t fst TF; notick s |]
  ==> (s @t [Tick]t, X) :f snd TF

lemma domSF_T3:

  [| (T, F) ∈ domSF; s @t [Tick]t :t T; notick s |] ==> (s @t [Tick]t, X) :f F

lemma domTF_F3:

  [| TF ∈ domSF; (s, X) :f snd TF; notick s; ∀a. a ∈ Y --> s @t [a]t ~:t fst TF |]
  ==> (s, X ∪ Y) :f snd TF

lemma domSF_F3:

  [| (T, F) ∈ domSF; (s, X) :f F; notick s; ∀a. a ∈ Y --> s @t [a]t ~:t T |]
  ==> (s, X ∪ Y) :f F

lemma domTF_F4:

  [| TF ∈ domSF; s @t [Tick]t :t fst TF; notick s |] ==> (s, Evset) :f snd TF

lemma domSF_F4:

  [| (T, F) ∈ domSF; s @t [Tick]t :t T; notick s |] ==> (s, Evset) :f F

lemma domTF_T3_F4:

  [| TF ∈ domSF; s @t [Tick]t :t fst TF; notick s |]
  ==> (s, Evset) :f snd TF ∧ (∀X. (s @t [Tick]t, X) :f snd TF)

lemma domSF_T3_F4:

  [| (T, F) ∈ domSF; s @t [Tick]t :t T; notick s |]
  ==> (s, Evset) :f F ∧ (∀X. (s @t [Tick]t, X) :f F)

lemma domTF_F2_F4:

  [| TF ∈ domSF; s @t [Tick]t :t fst TF; notick s; X ⊆ Evset |]
  ==> (s, X) :f snd TF

lemma domSF_F2_F4:

  [| (T, F) ∈ domSF; s @t [Tick]t :t T; notick s; X ⊆ Evset |] ==> (s, X) :f F

lemma BOT_in_domSF:

  ({[]t}t, {}f) ∈ domSF

lemma BOT_is_bottom_domSF:

  ({[]t}t, {}f) ≤ SF

lemma pairSF_fstSF:

  (S, F) ∈ domSF ==> fstSF (S ,, F) = S

lemma pairSF_sndSF:

  (S, F) ∈ domSF ==> sndSF (S ,, F) = F

lemma eqSF_decompo:

  (SF = SE) = (fstSF SF = fstSF SE ∧ sndSF SF = sndSF SE)

lemmas pairSF:

  (S, F) ∈ domSF ==> fstSF (S ,, F) = S

  (S, F) ∈ domSF ==> sndSF (S ,, F) = F

  (SF = SE) = (fstSF SF = fstSF SE ∧ sndSF SF = sndSF SE)

lemma subsetSF_decompo:

  (SF ≤ SE) = (fstSF SF ≤ fstSF SE ∧ sndSF SF ≤ sndSF SE)

lemmas memTF_def:

  x :t T == x ∈ Rep_domT T

  x :f F == x ∈ Rep_domF F