Theory Domain_F

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

theory Domain_F = Trace:

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

         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]

(***********************************************************
                 type def (Failure Part)
 ***********************************************************)

types 'a failure = "'a trace * 'a event set"       (* synonym *)

consts
  HC_F2    :: "'a failure set => bool" 

defs
  HC_F2_def : "HC_F2 F == (ALL s X Y. ((s,X) : F & Y <= X) --> (s,Y) : F) 
                    & (ALL X. (None, X) ~: F)"

typedef 'a domF = "{F::('a failure set). HC_F2(F)}"
apply (rule_tac x ="{}" in exI)
by (simp add: HC_F2_def)

declare Rep_domF         [simp]

(***********************************************************
                   operators on domF
 ***********************************************************)

consts
  memF     :: "'a failure => 'a domF => bool"  ("(_/ :f _)" [50, 51] 50)
  CollectF :: "('a failure => bool) => 'a domF"("CollectF")
  UnionF   :: "'a domF set => 'a domF"         ("UnionF _" [90] 90)
  InterF   :: "'a domF set => 'a domF"         ("InterF _" [90] 90)

  empF     :: "'a domF"                        ("{}f")
  UNIVF    :: "'a domF"                        ("UNIVf")

defs
  memF_def     : "x :f F     == x : (Rep_domF F)"
  CollectF_def : "CollectF P == Abs_domF (Collect P)"
  UnionF_def   : "UnionF Fs  == Abs_domF (Union (Rep_domF ` Fs))"
  InterF_def   : "InterF Fs  == Abs_domF (Inter (Rep_domF ` Fs))"

  empF_def     : "{}f        == Abs_domF {}"
  UNIVF_def    : "UNIVf      == Abs_domF UNIV"

syntax
  "_nonmemF"  :: "'a failure => 'a domF => bool"   ("(_/ ~:f _)" [50, 51] 50)
  "_UnF"      :: "'a domF => 'a domF => 'a domF"   ("_ UnF _" [65,66] 65)
  "_IntF"     :: "'a domF => 'a domF => 'a domF"   ("_ IntF _" [70,71] 70)

  "@CollF"    :: "pttrn => bool => 'a domF"        ("(1{_./ _}f)")
  "@FinsetF"  :: "args => 'a domF"                 ("{(_)}f")

translations
  "x ~:f F"    == "~ x :f F"
  "F UnF E"    == "UnionF {F,E}"
  "F IntF E"   == "InterF {F,E}"

  "{x. P}f"    == "Abs_domF {x. P}"
  "{X}f"       == "Abs_domF {X}"

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

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

defs (overloaded)
  subsetF_def   :  "F <= E  ==  (Rep_domF F) <= (Rep_domF E)"
  psubsetF_def  :  "F <  E  ==  (Rep_domF F) <  (Rep_domF E)"

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

instance domF :: (type) order
apply (intro_classes)
apply (unfold subsetF_def psubsetF_def)
apply (simp)
apply (erule order_trans, simp)
apply (drule order_antisym, simp)
apply (simp add: Rep_domF_inject)
apply (simp only: order_less_le Rep_domF_inject)
done

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

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

lemma domF_F2:
  "[| F:domF ; (s,X) : F ; Y <= X |] ==> (s,Y) : F"
apply (simp add: domF_def)
apply (unfold HC_F2_def)
apply (erule conjE)
apply (drule_tac x="s" in spec)
apply (drule_tac x="X" in spec)
apply (drule_tac x="X" in spec)
apply (drule_tac x="Y" in spec)
by (simp)

(*** {} in domF ***)

lemma emptyset_in_domF[simp]: "{} : domF"
by (simp add: domF_def HC_F2_def)

(* all the traces in domF is defined *)

lemma domF_not_None: "[| (s,X) : F ; F : domF |] ==> s ~= None"
apply (erule contrapos_pn)
apply (simp add: domF_def)
apply (unfold HC_F2_def)
apply (erule conjE)
apply (drule_tac x="X" in spec)
by (assumption)

lemma None_notin_Rep_domF[simp]: "(None, X) ~: Rep_domF F"
apply (subgoal_tac "Rep_domF F : domF")
apply (case_tac "(None, X) ~: Rep_domF F", simp)
apply (insert domF_not_None[of None X "Rep_domF F"])
by (simp_all)

(*******************************
         check in domF
 *******************************)

(*** [] (for STOP) ***)

lemma nilt_in_domF[simp]: "{([]t, X) |X. X <= EvsetTick} : domF"
by (auto simp add: domF_def HC_F2_def)

(*** [Tick] (for SKIP) ***)
lemma nilt_Tick_in_domF[simp]: "{([]t, X) |X. X <= Evset} Un 
                                {([Tick]t, X) |X. X <= EvsetTick} : domF"
apply (simp add: domF_def HC_F2_def)
apply (intro allI impI)
apply (elim conjE disjE)
by (simp_all)

(*** Union ***)

lemma domF_Union_in_domF: "(Union (Rep_domF ` Fs)) : domF"
apply (simp add: domF_def HC_F2_def)
apply (intro allI impI)

apply (erule conjE)
apply (erule bexE)
apply (rename_tac s X Y F)
apply (rule_tac x="F" in bexI)
apply (rule domF_F2)
by (simp_all)

(*** Un ***)

lemma domF_Un_in_domF:
  "(Rep_domF F Un Rep_domF E) : domF"
apply (insert domF_Union_in_domF[of "{F,E}"])
by (simp)

(*** Inter ***)

lemma domF_Inter_in_domF: "Fs ~= {} ==> (Inter (Rep_domF ` Fs)) : domF"
apply (simp add: domF_def HC_F2_def)
apply (intro allI impI)

apply (rule ballI)
apply (rename_tac s X Y F)
apply (erule conjE)
apply (drule_tac x="F" in bspec, simp)
apply (rule domF_F2)
by (simp_all)

(*** Int ***)

lemma domF_Int_in_domF:
  "(Rep_domF F Int Rep_domF E) : domF"
apply (insert domF_Inter_in_domF[of "{F,E}"])
by (simp)

lemmas in_domF = domF_Union_in_domF domF_Un_in_domF
                 domF_Inter_in_domF domF_Int_in_domF

(*******************************
     domF type --> set type
 *******************************)

(*** UnionF ***)

lemma domF_UnionF_Rep:
  "Rep_domF (UnionF Fs) = Union (Rep_domF ` Fs)"
by (simp add: UnionF_def Abs_domF_inverse in_domF)

(*** UnF ***)

lemma domF_UnF_Rep:
  "Rep_domF (F UnF E) = (Rep_domF F) Un (Rep_domF E)"
by (simp add: domF_UnionF_Rep)

(*** InterF ***)

lemma domF_InterF_Rep:
  "Fs ~= {} ==> Rep_domF (InterF Fs) = Inter (Rep_domF ` Fs)"
by (simp add: InterF_def Abs_domF_inverse in_domF)

(*** IntF ***)

lemma domF_IntF_Rep:
  "Rep_domF (F IntF E) = (Rep_domF F) Int (Rep_domF E)"
by (simp add: domF_InterF_Rep)

(*********************************************************
                       memF
 *********************************************************)

(* memF_F2 *)

lemma memF_F2:
  "[| (s,X) :f F ; Y <= X |] ==> (s,Y) :f F"
apply (simp add: memF_def)
apply (rule domF_F2)
by (simp_all)

(* not None *)

lemma memF_not_None: "(s,X) :f F ==> s ~= None"
apply (simp add: memF_def)
apply (rule domF_not_None[of s X "Rep_domF F"])
by (simp_all)

lemmas not_None_F = domF_not_None memF_not_None

lemma None_not_memF[simp]: "(None,X) ~:f F"
by (simp add: memF_def)

(* UnionF *)

lemma memF_UnionF_only_if:
  "sX :f UnionF Fs ==> EX F:Fs. sX :f F"
by (simp add: memF_def domF_UnionF_Rep)

lemma memF_UnionF_if:
  "[| F:Fs ; sX :f F |] ==> sX :f UnionF Fs"
apply (subgoal_tac "Fs ~= {}")
apply (simp add: memF_def domF_UnionF_Rep)
apply (rule_tac x="F" in bexI)
by (auto)

lemma memF_UnionF:
  "sX :f UnionF Fs = (EX F:Fs. sX :f F)"
apply (rule iffI)
apply (simp add: memF_UnionF_only_if)
by (auto simp add: memF_UnionF_if)

(* UnF *)

lemma memF_UnF:
  "sX :f E UnF F = (sX :f E | sX :f F)"
by (simp add: memF_UnionF)

(* InterF *)

lemma memF_InterF_only_if:
  "[| Fs ~= {} ; sX :f InterF Fs |] ==> ALL F:Fs. sX :f F"
by (simp add: memF_def domF_InterF_Rep)

lemma memF_InterF_if:
  "[| Fs ~= {} ; ALL F:Fs. sX :f F |] ==> sX :f InterF Fs"
by (simp add: memF_def domF_InterF_Rep)

lemma memF_InterF:
  "Fs ~= {} ==> sX :f InterF Fs = (ALL F:Fs. sX :f F)"
apply (rule iffI)
apply (rule memF_InterF_only_if, simp_all)
by (simp add: memF_InterF_if)

(* IntF *)

lemma memF_IntF:
  "sX :f E IntF F = (sX :f E & sX :f F)"
by (simp add: memF_InterF)

(* empty *)

lemma memF_empF[simp]: "sX ~:f {}f"
apply (simp add: memF_def empF_def)
by (simp add: Abs_domF_inverse)

(* pair *)

lemma memF_pair_iff: "(f :f F) = (EX s X. f = (s,X) & (s,X) :f F)"
apply (rule)
apply (rule_tac x="fst f" in exI)
apply (rule_tac x="snd f" in exI)
by (auto)

lemma memF_pairI: "(EX s X. f = (s,X) & (s,X) :f F) ==> (f :f F)"
by (auto)

lemma memF_pairE_lm: "[| f :f F ; (EX s X. f = (s,X) & (s,X) :f F) --> R |] ==> R"
apply (drule mp)
apply (rule_tac x="fst f" in exI)
apply (rule_tac x="snd f" in exI)
by (auto)

lemma memF_pairE: "[| f :f F ; !! s X. [| f = (s,X) ; (s,X) :f F |] ==> R |] ==> R"
apply (erule memF_pairE_lm)
by (auto)

(*********************************************************
                       subsetF
 *********************************************************)

lemma subsetFI [intro!]: "(!! s X. (s, X) :f E ==> (s, X) :f F) ==> E <= F"
by (auto simp add: subsetF_def memF_def)

lemma subsetFE [elim!]: 
  "[| E <= F ; (!!s X. (s, X) :f E ==> (s, X) :f F) ==> R |] ==> R"
by (auto simp add: subsetF_def memF_def)

lemma subsetF_iff: "((E::'a domF) <= F) 
                  = (ALL s X. (s, X) :f E --> (s, X) :f F)"
by (auto)

(*** {}f is bottom ***)

lemma BOT_is_bottom_domF[simp]: "{}f <= F"
by (simp add: subsetF_iff)

lemma memF_subsetF: "[| (s,X) :f E ; E <= F |] ==> (s,X) :f F"
by (simp add: subsetF_iff)

(*********************************************************
                         UnF
 *********************************************************)

lemma UnF_commut: "E UnF F = F UnF E"
by (simp add: eq_iff subsetF_iff memF_UnF)

lemma UnF_ass: "(E UnF F) UnF R = E UnF (F UnF R)"
by (simp add: eq_iff subsetF_iff memF_UnF)

lemma UnF_left_commut: "E UnF (F UnF R) = F UnF (E UnF R)"
by (simp add: eq_iff subsetF_iff memF_UnF)

lemmas UnF_rules = UnF_commut UnF_ass UnF_left_commut

(*********************************************************
                         IntF
 *********************************************************)

lemma IntF_commut: "E IntF F = F IntF E"
by (simp add: eq_iff subsetF_iff memF_IntF)

lemma IntF_ass: "(E IntF F) IntF R = E IntF (F IntF R)"
by (simp add: eq_iff subsetF_iff memF_IntF)

lemma IntF_left_commut: "E IntF (F IntF R) = F IntF (E IntF R)"
by (simp add: eq_iff subsetF_iff memF_IntF)

lemmas IntF_rules = IntF_commut IntF_ass IntF_left_commut

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

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

end