Theory Domain_F_cms

Up to index of Isabelle/HOL/HOL-Complex/CSP-Prover

theory Domain_F_cms = Domain_F + RS: 
           (*-------------------------------------------*
            |                CSP-Prover                 |
            |               December 2004               |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory Domain_F_cms = Domain_F + RS:

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

         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 domF :: (type) ms0
by (intro_classes)

consts
  restFset :: "'a domF => nat => 'a failure set" ("_ restFset _" [55,56] 55)
  LimitFset:: "'a domF infinite_seq => 'a failure set"
  LimitF   :: "'a domF infinite_seq => 'a domF"  ("LimitF")

defs
 restFset_def  : 
   "F restFset n == {(s, X) |s X. (s, X) :f F &
               (lengtht s < n |
                lengtht s = n & (EX s'. s = s' @t [Tick]t))}"

 LimitFset_def : 
   "LimitFset Fs == {(s, X) |s X. 
           ((s, X) :f Fs (Suc (lengtht s)) |
            (s, X) :f Fs (lengtht s) & (EX s'. s = s' @t [Tick]t))}"

 LimitF_def :
  "LimitF Fs == Abs_domF (LimitFset Fs)"

defs (overloaded)
  restF_def : "F rest n == Abs_domF (F restFset n)"

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

(*** restFset_def in domF ***)

lemma restFset_in[simp] : "F restFset n : domF"
apply (simp add: restFset_def)
apply (simp add: domF_def HC_F2_def)
apply (intro allI impI)
apply (elim conjE)
apply (rule memF_F2)
by (simp_all)

(*********************************************************
                     rest on domF
 *********************************************************)

lemma in_restF: "(s, X) :f F rest n = 
                 ((s, X) :f F &
                (lengtht s < n |
                 lengtht s = n & (EX s'. s = s' @t [Tick]t)))"
apply (simp add: memF_def restF_def)
apply (simp add: Abs_domF_inverse)
apply (simp add: memF_def restFset_def)
done

lemma restF_eq_iff:
   "(F rest n = E rest m) =
    (ALL s X. 
         ((s, X) :f F &
          (lengtht s < n |
           lengtht s = n & (EX s'. s = s' @t [Tick]t)))
       = ((s, X) :f E &
          (lengtht s < m |
           lengtht s = m & (EX s'. s = s' @t [Tick]t))))"
apply (simp add: restF_def Abs_domF_inject)
apply (simp add: restFset_def)
by (auto)

(*** F rest = E rest --> F = E ***)

lemma rest_domF_eq: 
  "[| (s, X) :f F ; F restFset Suc (lengtht s) = 
                    E restFset Suc (lengtht s) |]
   ==> (s, X) :f E"
by (auto simp add: restFset_def)

(*********************************************************
                     DomF --> RS
 *********************************************************)

(*******************************
        zero_eq_rs_domF
 *******************************)

(*** (contra) restFset 0 ***)

lemma contra_zero_domF: "(F::'a domF) restFset n ~= {} ==> 0 < n"
apply (simp add: restFset_def)
apply (elim conjE exE)
apply (erule disjE)
apply (simp)

apply (elim conjE exE)
by (simp add: not_None_F)

(*** restFset 0 ***)

lemma zero_domF: "(F::'a domF) restFset 0 = {}"
apply (insert contra_zero_domF[of F 0])
apply (case_tac "F restFset 0 = {}")
by (simp_all)

(*** zero_eq_rs_domF ***)

lemma zero_eq_rs_domF: "(F::'a domF) rest 0 = E rest 0"
apply (simp add: restF_def Abs_domF_inject)
by (simp add: zero_domF)

(*******************************
         min_rs_domF
 *******************************)

lemma min_rs_domF:
  "((F::'a domF) rest m) rest n = F rest (min m n)"
apply (simp add: restF_eq_iff)
apply (simp add: in_restF)
apply (intro allI)
apply (rule iffI)

apply (elim conjE exE disjE)
apply (simp_all add: min_is)
apply (rule_tac x="s'" in exI, simp)+

apply (elim conjE exE disjE)
apply (simp_all)

apply (case_tac "m < n")
apply (simp add: min_is)
apply (rule_tac x="s'" in exI, simp)

apply (case_tac "m = n")
apply (simp add: min_is)
apply (rule_tac x="s'" in exI, simp)

apply (case_tac "n < m")
apply (simp add: min_is)
apply (rule_tac x="s'" in exI, simp)

by (force)

(*******************************
        diff_rs_domF
 *******************************)

(*** contra <= ***)

lemma contra_diff_rs_domF_left: 
  "(ALL n. (F::'a domF) rest n = E rest n) ==> F <= E"
apply (simp add: restF_eq_iff)
apply (rule subsetFI)
apply (drule_tac x="Suc (lengtht s)" in spec)
apply (drule_tac x="s" in spec)
apply (drule_tac x="X" in spec)
by (simp)

(*** contra = ***)

lemma contra_diff_rs_domF: 
  "(ALL n. (F::'a domF) rest n = E rest n) ==> F = E"
apply (rule order_antisym)
by (simp_all add: contra_diff_rs_domF_left)

(*** diff_rs_domF ***)

lemma diff_rs_domF: 
  "(F::'a domF) ~= E ==> (EX (n::nat). F rest n ~= E rest n)"
apply (erule contrapos_np)
apply (rule contra_diff_rs_domF)
by (simp)

(***************************************************************
                        domF ==> RS
 ***************************************************************)

instance domF :: (type) rs
apply (intro_classes)
apply (simp add: zero_eq_rs_domF)
apply (simp add: min_rs_domF)
apply (simp add: diff_rs_domF)
done

(************************************************************
                        domF ==> MS
 ************************************************************)

instance domF :: (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.  domF ==> MS & RS 
 ************************************************************)

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

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

(*** normal_seq lemma ***)

lemma normal_seq_domF_less:
  "[| normal (Fs::'a domF infinite_seq) ; lengtht s < n |]
   ==> ((s,X) :f Fs (Suc (lengtht s))) = ((s,X) :f Fs n)"
apply (simp add: normal_def)
apply (drule_tac x="Suc (lengtht s)" in spec)
apply (drule_tac x="n" in spec)
apply (simp add: distance_rs_less_1[THEN sym])
apply (simp add: min_is)

apply (simp add: restF_eq_iff)
apply (drule_tac x="s" in spec)
apply (drule_tac x="X" in spec)
by (simp)

lemma normal_seq_domF_less_only_if:
  "[| normal (Fs::'a domF infinite_seq) ; lengtht s < n ;
      (s,X) :f Fs (Suc (lengtht s)) |]
   ==> ((s,X) :f Fs n)"
by (simp add: normal_seq_domF_less)

(*** normal_seq lemma (Tick)***)

lemma normal_seq_domF_Tick:
  "[| normal (Fs::'a domF infinite_seq) ; lengtht (s' @t [Tick]t) <= n |]
   ==> ((s' @t [Tick]t,X) :f Fs (lengtht (s' @t [Tick]t))) = 
       ((s' @t [Tick]t,X) :f Fs n)"
apply (simp add: normal_def)
apply (drule_tac x="lengtht (s' @t [Tick]t)" in spec)
apply (drule_tac x="n" in spec)
apply (simp add: distance_rs_less_1[THEN sym])
apply (simp add: min_is)

apply (simp add: restF_eq_iff)
apply (drule_tac x="s' @t [Tick]t" in spec)
apply (drule_tac x="X" in spec)
by (simp)

lemma normal_seq_domF_Tick_only_if:
  "[| normal (Fs::'a domF infinite_seq) ; lengtht (s' @t [Tick]t) <= n ;
      (s' @t [Tick]t,X) :f Fs (lengtht (s' @t [Tick]t)) |]
   ==> ((s' @t [Tick]t,X) :f Fs n)"
by (simp add: normal_seq_domF_Tick)

lemma normal_seq_domF_Tick_only_ifE:
  "[| (s' @t [Tick]t,X) :f Fs n ; 
      normal (Fs::'a domF infinite_seq) ; lengtht (s' @t [Tick]t) <= n ; 
      (s' @t [Tick]t,X) :f Fs (lengtht (s' @t [Tick]t)) ==> R |]
   ==> R"
by (simp add: normal_seq_domF_Tick)

(*** LimitFset_def in domF ***)

lemma LimitFset_in[simp]:
  "LimitFset (Fs::'a domF infinite_seq) : domF"
apply (simp add: LimitFset_def)
apply (simp add: domF_def HC_F2_def)
apply (intro allI impI)
apply (erule conjE)
apply (erule disjE)

apply (rule disjI1)
apply (rule memF_F2)
apply (simp_all)

apply (elim conjE exE)
apply (rule disjI2)
apply (rule memF_F2)
apply (simp_all)
done

(*** LimitF_memF ***)

lemma LimitF_memF: 
  "((s, X) :f LimitF Fs) = 
   ((s, X) :f Fs (Suc (lengtht s)) |
    (s, X) :f Fs (lengtht s) & (EX s'. s = s' @t [Tick]t))"
apply (simp add: LimitF_def memF_def)
apply (simp add: Abs_domF_inverse)
apply (simp add: LimitFset_def memF_def)
done

(*** LimitF lemma ***)

lemma LimitF_Limit_lm:
  "normal (Fs::'a domF infinite_seq)
   ==> (ALL n. (LimitF Fs) rest n = (Fs n) rest n)"
apply (simp add: restF_eq_iff)
apply (intro allI)
apply (simp add: LimitF_memF)
apply (rule iffI)

(* => *)
apply (elim conjE disjE)
apply (simp_all add: normal_seq_domF_less)

apply (elim conjE exE)
apply (simp)
apply (erule normal_seq_domF_Tick_only_ifE)
apply (simp_all)

apply (elim conjE exE)
apply (simp)
apply (rule normal_seq_domF_Tick_only_if)
apply (simp_all)

(* <= *)
apply (elim conjE disjE)
apply (simp add: normal_seq_domF_less)
apply (simp)
done

(*** (normal) Fs converges to (LimitF Fs) ***)

lemma LimitF_Limit:
  "normal (Fs::'a domF infinite_seq) ==> Fs convergeTo (LimitF Fs)"
by (simp add: LimitF_Limit_lm rest_Limit)

(*** (cauchy) Fs converges to (LimitF NF Fs) ***)

lemma cauchy_LimitF_Limit:
  "cauchy (Fs::'a domF infinite_seq) ==> Fs convergeTo (LimitF (NF Fs))"
apply (simp add: normal_form_seq_same_Limit)
apply (simp add: LimitF_Limit normal_form_seq_normal)
done

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

lemma domF_cms:
  "cauchy (Fs::'a domF infinite_seq) ==> (EX F. Fs convergeTo F)"
apply (rule_tac x="LimitF (NF Fs)" in exI)
by (simp add: cauchy_LimitF_Limit)

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

instance domF :: (type) cms
apply (intro_classes)
by (simp add: domF_cms)

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

(*** (normal) Limit Fs = LimitF Fs ***)

lemma LimitF_Limit_eq:
  "normal (Fs::'a domF infinite_seq) ==> Limit Fs = LimitF Fs"
apply (insert unique_convergence[of Fs "Limit Fs" "LimitF Fs"])
by (simp add:  LimitF_Limit Limit_is normal_cauchy)

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

consts
  RefF :: "'a domF => 'a domF => bool"
  RevF :: "'a domF => 'a domF => bool"

defs
  RefF_def : "RefF E == (%F. (E <= F))"
  RevF_def : "RevF E == (%F. (F <= E))"

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

lemma continuous_rs_RefF: "continuous_rs (RefF E)"
apply (simp add: continuous_rs_def)
apply (intro allI impI)
apply (simp add: RefF_def)
apply (simp add: subsetF_iff)
apply (elim conjE exE)

apply (rule_tac x="Suc (lengtht s)" in exI)
apply (intro allI impI)
apply (rule_tac x="s" in exI)
apply (rule_tac x="X" in exI)
apply (simp add: restF_eq_iff)
apply (drule_tac x="s" in spec)
apply (drule_tac x="X" in spec)
by (simp)

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

lemma continuous_rs_RevF: "continuous_rs (RevF E)"
apply (simp add: continuous_rs_def)
apply (intro allI impI)
apply (simp add: RevF_def)
apply (simp add: subsetF_iff)
apply (elim conjE exE)

apply (rule_tac x="Suc (lengtht s)" in exI)
apply (intro allI impI)
apply (rule_tac x="s" in exI)
apply (rule_tac x="X" in exI)
apply (simp add: restF_eq_iff)
apply (drule_tac x="s" in spec)
apply (drule_tac x="X" in spec)
by (simp)

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

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

end

lemma restFset_in: 

  F restFset n ∈ domF

lemma in_restF: 

  ((s, X) :f F rest n) =
  ((s, X) :f F ∧ (lengtht s < n ∨ lengtht s = n ∧ (∃s'. s = s' @t [Tick]t)))

lemma restF_eq_iff: 

  (F rest n = E rest m) =
  (∀s X. ((s, X) :f F ∧
          (lengtht s < n ∨ lengtht s = n ∧ (∃s'. s = s' @t [Tick]t))) =
         ((s, X) :f E ∧
          (lengtht s < m ∨ lengtht s = m ∧ (∃s'. s = s' @t [Tick]t))))

lemma rest_domF_eq: 

  [| (s, X) :f F; F restFset Suc (lengtht s) = E restFset Suc (lengtht s) |]
  ==> (s, X) :f E

lemma contra_zero_domF: 

  F restFset n ≠ {} ==> 0 < n

lemma zero_domF: 

  F restFset 0 = {}

lemma zero_eq_rs_domF: 

  F rest 0 = E rest 0

lemma min_rs_domF: 

  F rest m rest n = F rest min m n

lemma contra_diff_rs_domF_left: 

  ∀n. F rest n = E rest n ==> F ≤ E

lemma contra_diff_rs_domF: 

  ∀n. F rest n = E rest n ==> F = E

lemma diff_rs_domF: 

  F ≠ E ==> ∃n. F rest n ≠ E rest n

lemma normal_seq_domF_less: 

  [| normal Fs; lengtht s < n |]
  ==> ((s, X) :f Fs (Suc (lengtht s))) = ((s, X) :f Fs n)

lemma normal_seq_domF_less_only_if: 

  [| normal Fs; lengtht s < n; (s, X) :f Fs (Suc (lengtht s)) |]
  ==> (s, X) :f Fs n

lemma normal_seq_domF_Tick: 

  [| normal Fs; lengtht (s' @t [Tick]t) ≤ n |]
  ==> ((s' @t [Tick]t, X) :f Fs (lengtht (s' @t [Tick]t))) =
      ((s' @t [Tick]t, X) :f Fs n)

lemma normal_seq_domF_Tick_only_if: 

  [| normal Fs; lengtht (s' @t [Tick]t) ≤ n;
     (s' @t [Tick]t, X) :f Fs (lengtht (s' @t [Tick]t)) |]
  ==> (s' @t [Tick]t, X) :f Fs n

lemma normal_seq_domF_Tick_only_ifE: 

  [| (s' @t [Tick]t, X) :f Fs n; normal Fs; lengtht (s' @t [Tick]t) ≤ n;
     (s' @t [Tick]t, X) :f Fs (lengtht (s' @t [Tick]t)) ==> R |]
  ==> R

lemma LimitFset_in: 

  LimitFset Fs ∈ domF

lemma LimitF_memF: 

  ((s, X) :f LimitF Fs) =
  ((s, X) :f Fs (Suc (lengtht s)) ∨
   (s, X) :f Fs (lengtht s) ∧ (∃s'. s = s' @t [Tick]t))

lemma LimitF_Limit_lm: 

  normal Fs ==> ∀n. LimitF Fs rest n = Fs n rest n

lemma LimitF_Limit: 

  normal Fs ==> Fs convergeTo LimitF Fs

lemma cauchy_LimitF_Limit: 

  cauchy Fs ==> Fs convergeTo LimitF (NF Fs)

lemma domF_cms: 

  cauchy Fs ==> ∃F. Fs convergeTo F

lemma LimitF_Limit_eq: 

  normal Fs ==> Limit Fs = LimitF Fs

lemma continuous_rs_RefF: 

  continuous_rs (RefF E)

lemma continuous_rs_RevF: 

  continuous_rs (RevF E)