Theory Domain_SF_cms

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

theory Domain_SF_cms = Domain_SF + Domain_T_cms + Domain_F_cms + RS_pair:

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

         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]

(*********************************************************
                 Restriction in Dom_F
 *********************************************************)

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

consts
 restSFpair  :: "'a domSF => nat => 'a domTF" ("_ restSFpair _" [55,56] 55)
 LimitSFpair :: "'a domSF infinite_seq => 'a domTF"
 LimitSF     :: "'a domSF infinite_seq => 'a domSF"   ("LimitSF")

defs
  restSFpair_def  : 
   "SF restSFpair n == (Rep_domSF SF) rest n"
  LimitSFpair_def : 
   "LimitSFpair SFs == pair_Limit (Rep_domSF o SFs)"
  LimitSF_def     :
   "LimitSF SFs == Abs_domSF (LimitSFpair SFs)"

defs (overloaded)
  restSF_def : "SF rest n == Abs_domSF (SF restSFpair n)"

(*********************************************************
              Lemmas (Restriction in Dom_SF)
 *********************************************************)

(*** restSFpair (T2) ***)

lemma restSFpair_T2: "HC_T2 (SF restSFpair n)"
apply (simp add: HC_T2_def restSFpair_def)
apply (intro allI impI)
apply (simp add: pair_restriction_def)

apply (simp add: in_restT)
apply (simp add: in_restF)
by (auto simp add: domTF_T2)

(*** restSFpair (F2) ***)

lemma restSFpair_F3: "HC_F3 (SF restSFpair n)"
apply (simp add: HC_F3_def restSFpair_def)
apply (intro allI impI)
apply (simp add: pair_restriction_def)

apply (simp add: in_restT)
apply (simp add: in_restF)
by (auto simp add: domTF_F3)

(*** restSFpair (T3_F4) ***)

lemma restSFpair_T3_F4: "HC_T3_F4 (SF restSFpair n)"
apply (simp add: HC_T3_F4_def restSFpair_def)
apply (intro allI impI)
apply (simp add: pair_restriction_def)

apply (simp add: in_restT)
apply (simp add: in_restF)
apply (elim conjE)
by (auto simp add: domTF_T3 domTF_F4)

(*** restSFpair in domSF ***)

lemma restSFpair_in[simp]: "SF restSFpair n : domSF"
apply (simp add: domSF_iff)
apply (simp add: restSFpair_T2)
apply (simp add: restSFpair_F3)
apply (simp add: restSFpair_T3_F4)
done

(*********************************************************
                     Dom_SF --> RS
 *********************************************************)

(*** restSF --> restTF ***)

lemma Rep_restSF: 
  "((SF::'a domSF) rest n = SE rest m) =
   ((Rep_domSF SF) rest n = (Rep_domSF SE) rest m)"
apply (simp add: restSF_def)
apply (simp add: Abs_domSF_inject)
apply (simp add: restSFpair_def)
done

(*** zero_eq_rs_domSF ***)

lemma zero_eq_rs_domSF: "(SF::'a domSF) rest 0 = SE rest 0"
by (simp add: Rep_restSF)

(*** min_rs_domSF ***)

lemma min_rs_domSF:
  "((SF::'a domSF) rest m) rest n = SF rest (min m n)"
apply (simp add: Rep_restSF)
apply (simp add: restSF_def)
apply (simp add: Abs_domSF_inverse)
apply (simp add: restSFpair_def)
apply (simp add: min_rs)
done

(*** diff_rs_domSF ***)

lemma diff_rs_domSF: 
  "(SF::'a domSF) ~= SE ==> (EX (n::nat). SF rest n ~= SE rest n)"
apply (simp add: Rep_restSF)
apply (simp add: Rep_domSF_inject[THEN sym])
apply (simp add: diff_rs)
done

(***************************************************************
                        domSF ==> RS
 ***************************************************************)

instance domSF :: (type) rs
apply (intro_classes)
apply (simp add: zero_eq_rs_domSF)
apply (simp add: min_rs_domSF)
apply (simp add: diff_rs_domSF)
done

(************************************************************
                        domSF ==> MS
 ************************************************************)

instance domSF :: (type) ms
apply (intro_classes)
apply (simp)
apply (simp add: diagonal_rs)
apply (simp add: symmetry_rs)
apply (simp add: triangle_inequality_rs)
done

(************************************************************
                 i.e.  domSF ==> MS & RS 
 ************************************************************)

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

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

(*** distance ***)

lemma distance_Rep_domSF:
  "distance((SF::'a domSF), SE) = distance(Rep_domSF SF, Rep_domSF SE)"
by (simp add: Rep_restSF rest_distance_eq)

lemma distance_Abs_domSF:
  "[| (T1, F1) : domSF ; (T2, F2) : domSF |]
   ==> distance (Abs_domSF (T1, F1), Abs_domSF (T2, F2))
     = distance ((T1, F1), T2, F2)"
by (simp add: distance_Rep_domSF Abs_domSF_inverse)

(*** normal ***)

lemma normal_domSF:
  "normal (SFs::'a domSF infinite_seq) = normal (Rep_domSF o SFs)"
by (simp add: normal_def distance_Rep_domSF)

lemma normal_domSF_only_if:
  "normal (SFs::'a domSF infinite_seq) ==> normal (Rep_domSF o SFs)"
by (simp add: normal_domSF)

(* T and F *)

lemma normal_of_domSF:
  "normal (SFs::'a domSF infinite_seq)
   ==> (normal (fstSF o SFs) & normal (sndSF o SFs))"
apply (simp add: normal_domSF)
apply (simp add: fstSF_def sndSF_def)
apply (simp add: o_assoc[THEN sym])
apply (simp add: pair_normal_seq)
done

(*** cauchy ***)

lemma cauchy_domSF:
  "cauchy (SFs::'a domSF infinite_seq) = cauchy (Rep_domSF o SFs)"
by (simp add: cauchy_def distance_Rep_domSF)

lemma cauchy_domSF_only_if:
  "cauchy (SFs::'a domSF infinite_seq) ==> cauchy (Rep_domSF o SFs)"
by (simp add: cauchy_domSF)

(* T and F *)

lemma cauchy_of_domSF:
  "cauchy (SFs::'a domSF infinite_seq)
   ==> (cauchy (fstSF o SFs) & cauchy (sndSF o SFs))"
apply (simp add: cauchy_domSF)
apply (simp add: fstSF_def sndSF_def)
apply (simp add: o_assoc[THEN sym])
apply (simp add: pair_cauchy_seq)
done

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

(*** convergeTo domSF ***)

lemma convergeTo_domSF:
  "[| (Rep_domSF o SFs) convergeTo TF ; TF : domSF |]
   ==> SFs convergeTo Abs_domSF TF"
apply (simp add: convergeTo_def)
apply (intro allI impI)
apply (drule_tac x="eps" in spec)
apply (simp)
apply (erule exE)
apply (rule_tac x="n" in exI)
apply (intro allI impI)
apply (drule_tac x="m" in spec)

apply (simp add: distance_Rep_domSF)
apply (simp add: Abs_domSF_inverse)
done

(*** LimitSFpair ***)

lemma LimitSFpair_iff:
  "normal (Rep_domSF o SFs) 
      ==> pair_Limit (Rep_domSF o SFs)
           = (LimitT (fstSF o SFs) , LimitF (sndSF o SFs))"
apply (simp add: pair_Limit_def)
apply (simp add: fstSF_def sndSF_def)
apply (simp add: o_assoc[THEN sym])
apply (simp add: pair_normal_seq LimitT_Limit_eq LimitF_Limit_eq)
done

(*******************************
      LimitSFpair in domF
 *******************************)

(*** F4 ***)

lemma LimitSFpair_F4:
  "normal SFs ==> HC_F4 (LimitT (fstSF o SFs) , LimitF (sndSF o SFs))"
apply (simp add: HC_F4_def)
apply (intro allI impI)

apply (simp add: normal_of_domSF LimitT_memT)
apply (simp add: normal_of_domSF LimitF_memF)

apply (subgoal_tac "(Rep_domSF (SFs (lengtht (s @t [Tick]t)))) : domSF")
apply (simp add: domSF_def HC_F4_def)
apply (elim conjE)
apply (drule_tac x="s" in spec)
apply (simp add: fstSF_def sndSF_def)
by (simp)

(*** T3 ***)

lemma LimitSFpair_T3:
  "normal SFs ==> HC_T3 (LimitT (fstSF o SFs) , LimitF (sndSF o SFs))"
apply (simp add: HC_T3_def)
apply (intro allI impI)
apply (simp add: normal_of_domSF LimitT_memT)
apply (simp add: normal_of_domSF LimitF_memF)

apply (subgoal_tac "(Rep_domSF (SFs (lengtht (s @t [Tick]t)))) : domSF")
apply (simp add: domSF_def HC_T3_def)
apply (elim conjE)
apply (drule_tac x="s" in spec)
apply (simp add: fstSF_def sndSF_def)
by (simp)

(*** F3 ***)

lemma LimitSFpair_F3:
  "normal SFs ==> HC_F3 (LimitT (fstSF o SFs) , LimitF (sndSF o SFs))"
apply (simp add: HC_F3_def)
apply (intro allI impI)

apply (simp add: normal_of_domSF LimitT_memT)
apply (simp add: normal_of_domSF LimitF_memF)
apply (elim conjE disjE)

apply (subgoal_tac "(Rep_domSF (SFs (Suc (lengtht s)))) : domSF")
apply (simp add: domSF_def HC_F3_def)
apply (elim conjE)
apply (drule_tac x="s" in spec)
apply (drule_tac x="X" in spec)
apply (drule_tac x="Y" in spec)
apply (simp add: fstSF_def sndSF_def)
apply (simp)

apply (erule exE)
apply (simp)
done

(*** T2 ***)

lemma LimitSFpair_T2:
  "normal SFs ==> HC_T2 (LimitT (fstSF o SFs) , LimitF (sndSF o SFs))"
apply (simp add: HC_T2_def)
apply (intro allI impI)

apply (simp add: normal_of_domSF LimitT_memT)
apply (simp add: normal_of_domSF LimitF_memF)
apply (elim exE disjE)

apply (subgoal_tac "(Rep_domSF (SFs (Suc (lengtht s)))) : domSF")
apply (simp add: domSF_def HC_T2_def)
apply (elim conjE)
apply (drule_tac x="s" in spec)
apply (simp add: fstSF_def sndSF_def)
apply (drule mp)
apply (rule_tac x="X" in exI, simp)
apply (rule normal_seq_domT_if)
 apply (subgoal_tac "(%u. fst (Rep_domSF (SFs u))) = (fstSF o SFs )")
 apply (simp add: normal_of_domSF)
 apply (simp add: expand_fun_eq fstSF_def)
 apply (simp_all)

(* *)

apply (elim conjE exE)
apply (subgoal_tac "(Rep_domSF (SFs (lengtht s))) : domSF")
apply (simp add: domSF_def HC_T2_def)
apply (elim conjE)
apply (drule_tac x="s" in spec)
apply (simp add: fstSF_def sndSF_def)
apply (drule mp)
apply (rule_tac x="X" in exI, simp)
apply (simp_all)
done

(*** LimitSFpari_in ***)

lemma LimitSFpair_in:
  "normal SFs ==> LimitSFpair SFs : domSF"
apply (simp add: LimitSFpair_def)
apply (simp add: LimitSFpair_iff normal_domSF_only_if)
apply (simp add: domSF_def)
apply (simp add: LimitSFpair_F4)
apply (simp add: LimitSFpair_T3)
apply (simp add: LimitSFpair_F3)
apply (simp add: LimitSFpair_T2)
done

(*** (normal) SFs converges to (LimitSF SFs) ***)

lemma LimitSF_Limit: "normal SFs ==> SFs convergeTo (LimitSF SFs)"
apply (simp add: LimitSF_def)
apply (rule convergeTo_domSF)
apply (simp add: LimitSFpair_def)
apply (simp add: pair_cms_cauchy_Limit normal_cauchy normal_domSF)

by (simp add: LimitSFpair_in)

(*** (cauchy) Fs converges to (LimitSF NF SFs) ***)

lemma cauchy_LimitSF_Limit:
  "cauchy SFs ==> SFs convergeTo (LimitSF (NF SFs))"
by (simp add: LimitSF_Limit normal_form_seq_same_Limit normal_form_seq_normal)

(**************************************
    Dom_SF --> Complete Metric Space
 **************************************)

lemma domSF_cms:
  "cauchy (SFs::'a domSF infinite_seq) ==> (EX SF. SFs convergeTo SF)"
apply (rule_tac x="LimitSF (NF SFs)" in exI)
by (simp add: cauchy_LimitSF_Limit)

(************************************************************
                   domSF ==> CMS and RS
 ************************************************************)

instance domSF :: (type) cms
apply (intro_classes)
by (simp add: domSF_cms)

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

(*** (normal) Limit SFs = LimitSF SFs ***)

lemma LimitSF_Limit_eq:
  "normal (SFs::'a domSF infinite_seq) ==> Limit SFs = LimitSF SFs"
apply (rule unique_convergence[of SFs])
by (simp_all add: LimitSF_Limit Limit_is normal_cauchy)

(*----------------------------------------------------------*
 |                                                          |
 |         Fixed point induction for refinement             |
 |                                                          |
 *----------------------------------------------------------*)

consts
  RefSF :: "'a domSF => 'a domSF => bool"
  RevSF :: "'a domSF => 'a domSF => bool"

defs
  RefSF_def : "RefSF SE == (%SF. (SE <= SF))"
  RevSF_def : "RevSF SE == (%SF. (SF <= SE))"

(************************************************************
                continuity lemma 
 ************************************************************)

(*** (f o Rep_domSF) ***)

lemma continuous_rs_compo:
  "continuous_rs f ==> continuous_rs (f o Rep_domSF)"
apply (simp add: continuous_rs_def)
apply (intro allI impI)
apply (drule_tac x="fst (Rep_domSF x)" in spec)
apply (drule_tac x="snd (Rep_domSF x)" in spec)
apply (simp)
apply (erule exE)
apply (rule_tac x="n" in exI)
apply (intro allI impI)
apply (drule_tac x="fst (Rep_domSF y)" in spec)
apply (drule_tac x="snd (Rep_domSF y)" in spec)
apply (drule mp)
apply (simp add: Rep_restSF)
by (simp)

(*** RefSF iff ***)

lemma RefSF_iff:
   "RefSF SE = (%SF. RefT (fstSF SE) (fstSF SF) & RefF (sndSF SE) (sndSF SF))"
apply (simp add: RefSF_def)
apply (simp add: expand_fun_eq)
apply (rule allI)
apply (simp add: RefT_def RefF_def)
apply (simp add: subsetSF_decompo)
done

(*** RevSF iff ***)

lemma RevSF_iff:
   "RevSF SE = (%SF. RevT (fstSF SE) (fstSF SF) & RevF (sndSF SE) (sndSF SF))"
apply (simp add: RevSF_def)
apply (simp add: expand_fun_eq)
apply (rule allI)
apply (simp add: RevT_def RevF_def)
apply (simp add: subsetSF_decompo)
done

lemma continuous_rs_domSF: 
  "[| continuous_rs R1 ; continuous_rs R2 |]
   ==> continuous_rs (%SF. R1 (fstSF SF) & R2 (sndSF SF))"
apply (simp add: fstSF_def sndSF_def)
apply (subgoal_tac 
  "(%SF. R1 (fst (Rep_domSF SF)) & R2 (snd (Rep_domSF SF)))
   = (%TF. R1 (fst TF) & R2 (snd TF)) o Rep_domSF")
apply (simp)
apply (rule continuous_rs_compo)
apply (rule pair_continuous_rs, simp_all)
apply (simp add: expand_fun_eq)
done

(************************************************************
             continuity lemma for refinement
 ************************************************************)

lemma continuous_rs_RefSF: "continuous_rs (RefSF SE)"
apply (simp add: RefSF_iff)
by (simp add: continuous_rs_domSF continuous_rs_RefT continuous_rs_RefF)

(************************************************************
         continuity lemma for (Reverse) refinement
 ************************************************************)

lemma continuous_rs_RevSF: "continuous_rs (RevSF SE)"
apply (simp add: RevSF_iff)
by (simp add: continuous_rs_domSF continuous_rs_RevT continuous_rs_RevF)

end