Theory Domain_T

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

theory Domain_T = Prefix:

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

         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 (Trace Part)
 ***********************************************************)

consts
  HC_T1    :: "'a trace set => bool" 

defs
  HC_T1_def : "HC_T1 T == (T ~= {} & prefix_closed T & None ~: T)"

typedef 'a domT = "{T::('a trace set). HC_T1(T)}"
apply (rule_tac x ="{[]t}" in exI)
by (simp add: HC_T1_def prefix_closed_def)

declare Rep_domT         [simp]

(***********************************************************
                   operators on domT
 ***********************************************************)

consts
  memT     :: "'a trace => 'a domT => bool"  ("(_/ :t _)" [50, 51] 50)
  CollectT :: "('a trace => bool) => 'a domT"("CollectT")
  UnionT   :: "'a domT set => 'a domT"       ("UnionT _" [90] 90)
  InterT   :: "'a domT set => 'a domT"       ("InterT _" [90] 90)

  empT     :: "'a domT"                      ("{}t")
  UNIVT    :: "'a domT"                      ("UNIVt")

defs
  memT_def     : "x :t T     == x : (Rep_domT T)"
  CollectT_def : "CollectT P == Abs_domT (Collect P)"
  UnionT_def   : "UnionT Ts  == Abs_domT (Union (Rep_domT ` Ts))"
  InterT_def   : "InterT Ts  == Abs_domT (Inter (Rep_domT ` Ts))"

  empT_def     : "{}t        == Abs_domT {}"
  UNIVT_def    : "UNIVt      == Abs_domT UNIV"

syntax
  "_nonmemT"  :: "'a trace => 'a domT => bool"   ("(_/ ~:t _)" [50, 51] 50)
  "_UnT"      :: "'a domT => 'a domT => 'a domT" ("_ UnT _" [65,66] 65)
  "_IntT"     :: "'a domT => 'a domT => 'a domT" ("_ IntT _" [70,71] 70)

  "@CollT"    :: "pttrn => bool => 'a domT"      ("(1{_./ _}t)")
  "@FinsetT"  :: "args => 'a domT"               ("{(_)}t")

translations
  "x ~:t T"    == "~ x :t T"
  "T UnT S"    == "UnionT {T,S}"
  "T IntT S"   == "InterT {T,S}"

  "{x. P}t"    == "Abs_domT {x. P}"
  "{X}t"       == "Abs_domT {X}"

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

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

defs (overloaded)
  subsetT_def   :  "T <= S  ==  (Rep_domT T) <= (Rep_domT S)"
  psubsetT_def  :  "T <  S  ==  (Rep_domT T) <  (Rep_domT S)"

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

instance domT :: (type) order
apply (intro_classes)
apply (unfold subsetT_def psubsetT_def)
apply (simp)
apply (erule order_trans, simp)
apply (drule order_antisym, simp)
apply (simp add: Rep_domT_inject)
apply (simp only: order_less_le Rep_domT_inject)
done

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

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

lemma domT_is_non_empty: "T:domT ==> T ~= {}"
by (simp add: domT_def HC_T1_def)

lemma domT_is_prefix_closed: 
  "T:domT ==> prefix_closed T"
by (simp add: domT_def HC_T1_def)

lemma domT_is_prefix_closed_unfold: 
  "[| T:domT ; t : T ; prefix s t |] ==> s : T"
apply (simp add: domT_def HC_T1_def)
apply (rule prefix_closed_iff)
by (simp_all)

(*** {[]t} in domT ***)

lemma nilt_set_in[simp]: "{[]t} : domT"
by (simp add: domT_def HC_T1_def prefix_closed_def)

(*** {[]t, [a]t} in domT ***)

lemma one_t_set_in[simp]: "{[]t,  [a]t} : domT"
apply (simp add: domT_def HC_T1_def)
apply (simp add: prefix_closed_def)
apply (intro allI impI)
apply (erule exE)
apply (erule conjE)
apply (erule disjE)
by (simp_all)

(* []t is contained in all domT *)

lemma nilt_in_all_dom: "T : domT ==> []t : T"
apply (simp add: domT_def HC_T1_def)
apply (erule conjE)
apply (subgoal_tac "EX t. t : T")
apply (erule exE)
apply (rule prefix_closed_iff)
by (auto)

(* all the traces in domT is defined *)

lemma domT_not_None: "[| t : T ; T : domT |] ==> t ~= None"
apply (erule contrapos_pn)
by (simp add: domT_def HC_T1_def)

lemma None_notin_Rep_domT[simp]: "None ~: Rep_domT T"
apply (subgoal_tac "Rep_domT T : domT")
apply (simp add: domT_def HC_T1_def)
by (simp)

(*******************************
        check in domT 
 *******************************)

(*** Union ***)

lemma domT_Union_in_domT:
  "Ts ~= {} ==> (Union (Rep_domT ` Ts)) : domT"
apply (simp add: domT_def HC_T1_def)
apply (simp add: prefix_closed_def)
apply (rule conjI)

apply (subgoal_tac "EX T. T : Ts")
apply (erule exE)
apply (rule_tac x="T" in bexI)
apply (simp add: domT_is_non_empty)
apply (simp)
apply (force)

apply (intro allI impI)
apply (elim conjE exE bexE)
apply (rule_tac x="x" in bexI)

apply (rule prefix_closed_iff, simp_all)
apply (rule domT_is_prefix_closed)
apply (simp)
done

(*** Un ***)

lemma domT_Un_in_domT:
  "(Rep_domT T Un Rep_domT S) : domT"
apply (insert domT_Union_in_domT[of "{T,S}"])
by (simp)

(*** Inter ***)

lemma domT_Inter_in_domT: 
  "Ts ~= {} ==> (Inter (Rep_domT ` Ts)) : domT"
apply (simp add: domT_def HC_T1_def)
apply (rule conjI)

apply (subgoal_tac "[]t : Inter (Rep_domT ` Ts)", force)
apply (simp add: Inter_def)
apply (simp add: nilt_in_all_dom)

apply (simp add: prefix_closed_def)
apply (intro allI impI ballI)
apply (elim conjE exE)
apply (drule_tac x="x" in bspec, simp)

apply (rule prefix_closed_iff, simp_all)
apply (simp add: domT_is_prefix_closed)
done

(*** Int ***)

lemma domT_Int_in_domT:
  "(Rep_domT T Int Rep_domT S) : domT"
apply (insert domT_Inter_in_domT[of "{T,S}"])
by (simp)

lemmas in_domT = domT_Union_in_domT domT_Un_in_domT
                  domT_Inter_in_domT domT_Int_in_domT

(*******************************
    domT type --> set type
 *******************************)

(*** UnionT ***)

lemma domT_UnionT_Rep:
  "Ts ~= {} ==> Rep_domT (UnionT Ts) = Union (Rep_domT ` Ts)"
by (simp add: UnionT_def Abs_domT_inverse in_domT)

(*** UnT ***)

lemma domT_UnT_Rep:
  "Rep_domT (T UnT S) = (Rep_domT T) Un (Rep_domT S)"
by (simp add: domT_UnionT_Rep)

(*** InterT ***)

lemma domT_InterT_Rep:
  "Ts ~= {} ==> Rep_domT (InterT Ts) = Inter (Rep_domT ` Ts)"
by (simp add: InterT_def Abs_domT_inverse in_domT)

(*** IntT ***)

lemma domT_IntT_Rep:
  "Rep_domT (T IntT S) = (Rep_domT T) Int (Rep_domT S)"
by (simp add: domT_InterT_Rep)

(*********************************************************
                       memT
 *********************************************************)

(* prefix closed *)

lemma memT_prefix_closed:
  "[| t :t T ; prefix s t |] ==> s :t T"
apply (simp add: memT_def)
apply (rule domT_is_prefix_closed_unfold)
by (simp_all)

(* []t *)

lemma nilt_in_T[simp]: "[]t :t T"
by (simp add: memT_def nilt_in_all_dom)

(* not None *)

lemma memT_not_None: "t :t T ==> t ~= None"
apply (simp add: memT_def)
apply (rule domT_not_None[of t "Rep_domT T"])
by (simp_all)

lemmas not_None_T = domT_not_None memT_not_None

lemma None_not_memT[simp]: "None ~:t T"
by (simp add: memT_def)

(* UnionT *)

lemma memT_UnionT_only_if:
  "[| Ts ~= {} ; t :t UnionT Ts |] ==> EX T:Ts. t :t T"
by (simp add: memT_def domT_UnionT_Rep)

lemma memT_UnionT_if:
  "[| T:Ts ; t :t T |] ==> t :t UnionT Ts"
apply (subgoal_tac "Ts ~= {}")
apply (simp add: memT_def domT_UnionT_Rep)
apply (rule_tac x="T" in bexI)
by (auto)

lemma memT_UnionT:
  "Ts ~= {} ==> t :t UnionT Ts = (EX T:Ts. t :t T)"
apply (rule iffI)
apply (simp add: memT_UnionT_only_if)
by (auto simp add: memT_UnionT_if)

(* UnT *)

lemma memT_UnT:
  "t :t S UnT T = (t :t S | t :t T)"
by (simp add: memT_UnionT)

(* InterT *)

lemma memT_InterT_only_if:
  "[| Ts ~= {} ; t :t InterT Ts |] ==> ALL T:Ts. t :t T"
by (simp add: memT_def domT_InterT_Rep)

lemma memT_InterT_if:
  "[| Ts ~= {} ; ALL T:Ts. t :t T |] ==> t :t InterT Ts"
by (simp add: memT_def domT_InterT_Rep)

lemma memT_InterT:
  "Ts ~= {} ==> t :t InterT Ts = (ALL T:Ts. t :t T)"
apply (rule iffI)
apply (rule memT_InterT_only_if, simp_all)
by (simp add: memT_InterT_if)

(* IntT *)

lemma memT_IntT:
  "t :t S IntT T = (t :t S & t :t T)"
by (simp add: memT_InterT)

(* []t *)

lemma memT_nilt[simp]: "t :t {[]t}t = (t = []t)"
by (simp add: memT_def Abs_domT_inverse)

(* [e]t, []t *)

lemma memT_nilt_one[simp]: "t :t {[]t, [a]t}t = (t = []t | t = [a]t)"
by (simp add: memT_def Abs_domT_inverse)

(*********************************************************
                       subsetT
 *********************************************************)

lemma subsetTI [intro!]: "(!! t. t :t S ==> t :t T) ==> S <= T"
by (auto simp add: subsetT_def memT_def)

lemma subsetTE [elim!]: "[| S <= T ; (!!t. t :t S ==> t :t T) ==> R |] ==> R"
by (auto simp add: subsetT_def memT_def)

lemma subsetT_iff: "((S::'a domT) <= T) = (ALL t. t :t S --> t :t T)"
by (auto)

(*** {[]t}t is bottom ***)

lemma BOT_is_bottom_domT[simp]: "{[]t}t <= T"
by (simp add: subsetT_iff)

(*********************************************************
                         UnT
 *********************************************************)

lemma UnT_commut: "S UnT T = T UnT S"
by (simp add: eq_iff subsetT_iff memT_UnT)

lemma UnT_ass: "(S UnT T) UnT R = S UnT (T UnT R)"
by (simp add: eq_iff subsetT_iff memT_UnT)

lemma UnT_left_commut: "S UnT (T UnT R) = T UnT (S UnT R)"
by (simp add: eq_iff subsetT_iff memT_UnT)

lemmas UnT_rules = UnT_commut UnT_ass UnT_left_commut

lemma UnT_nilt_left[simp]: "{[]t}t UnT T = T"
apply (simp add: eq_iff)
by (auto simp add: memT_UnT)

lemma UnT_nilt_right[simp]: "T UnT {[]t}t = T"
apply (simp add: eq_iff)
by (auto simp add: memT_UnT)

(*********************************************************
                         IntT
 *********************************************************)

lemma IntT_commut: "S IntT T = T IntT S"
by (simp add: eq_iff subsetT_iff memT_IntT)

lemma IntT_ass: "(S IntT T) IntT R = S IntT (T IntT R)"
by (simp add: eq_iff subsetT_iff memT_IntT)

lemma IntT_left_commut: "S IntT (T IntT R) = T IntT (S IntT R)"
by (simp add: eq_iff subsetT_iff memT_IntT)

lemmas IntT_rules = IntT_commut IntT_ass IntT_left_commut

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

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

end