Theory Domain_T_cms

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

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

theory Domain_T_cms = Domain_T + 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]

(**********************************************************
           Definitions (Restriction in domT)
 **********************************************************)

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

consts
  restTset :: "'a domT => nat => 'a trace set" ("_ restTset _" [55,56] 55)
  LimitTset:: "'a domT infinite_seq => 'a trace set"
  LimitT :: "'a domT infinite_seq => 'a domT"

defs
 restTset_def  : "T restTset n == {s. s :t T & (lengtht s) <= n}"
 LimitTset_def : "LimitTset Ts == {s. s :t Ts (lengtht s)}"
 LimitT_def    : "LimitT Ts    == Abs_domT (LimitTset Ts)"

defs (overloaded)
  restT_def : "T rest n == Abs_domT (T restTset n)"

(**********************************************************
              Lemmas (Restriction in Dom_T)
 **********************************************************)

(*** restTset_def in domT ***)

lemma restTset_in[simp] : "T restTset n : domT"
apply (simp add: restTset_def)
apply (simp add: domT_def HC_T1_def)
apply (rule conjI)
apply (rule_tac x="[]t" in exI, simp)

apply (simp add: prefix_closed_def)
apply (intro allI impI)
apply (elim conjE exE)

apply (rule conjI)
apply (rule memT_prefix_closed, simp_all)

apply (subgoal_tac "lengtht s <= lengtht t", simp)
apply (rule length_of_prefix)
apply (simp_all add: memT_not_None)
done

(*** restTset in domT ***)

lemmas restTset_def_in = restTset_in[simplified memT_def restTset_def]

(*********************************************************
                     rest on dom_T
 *********************************************************)

lemma restT_iff: "T rest n = {s. s :t T & lengtht s <= n}t"
apply (simp add: restT_def)
apply (simp add: restTset_in[simplified restTset_def] Abs_domT_inject)
apply (simp add: restTset_def)
done

lemma in_restT: "s :t T rest n = (s :t T & lengtht s <= n)"
apply (simp add: memT_def restT_def)
apply (simp add: Abs_domT_inverse)
apply (simp add: memT_def restTset_def)
done

lemma restT_eq_iff:
   "(T rest n = S rest m) =
    (ALL s. (s :t T & lengtht s <= n) = (s :t S & lengtht s <= m))"
apply (simp add: restT_def Abs_domT_inject)
apply (simp add: restTset_def)
by (auto)

(*********************************************************
                     Dom_T --> RS
 *********************************************************)

(*******************************
        zero_eq_rs_domT
 *******************************)

(*** restTset 0 ***)

lemma zero_domT: "T restTset 0 = {[]t}"
apply (simp add: restTset_def)
apply (rule order_antisym)

apply (rule subsetI)
apply (simp)
apply (erule conjE)
apply (simp add: lengtht_zero memT_not_None)
by (simp)

(*** zero_eq_rs_domT ***)

lemma zero_eq_rs_domT: "(T::'a domT) rest 0 = S rest 0"
apply (simp add: restT_def)
apply (simp add: Abs_domT_inject)
apply (simp add: zero_domT)
done

(*******************************
         min_rs_domT
 *******************************)

lemma min_rs_domT: "((T::'a domT) rest m) rest n = T rest (min m n)"
apply (simp add: restT_def)
apply (simp add: Abs_domT_inject)

apply (simp add: restTset_def memT_def)
apply (simp add: restTset_in[simplified memT_def restTset_def]
                 Abs_domT_inverse)
done

(*******************************
         diff_rs_domT
 *******************************)

(*** contra = ***)

lemma contra_diff_rs_domT: 
  "(ALL n. (T::'a domT) rest n = S rest n) ==> T = S"
apply (simp add: restT_eq_iff)
apply (simp add: eq_iff)
by (auto)

(*** diff_rs_domT ***)

lemma diff_rs_domT: 
  "(T::'a domT) ~= S ==> (EX n. T rest n ~= S rest n)"
apply (erule contrapos_pp)
apply (simp)
apply (rule contra_diff_rs_domT, simp)
done

(***************************************************************
                        domT ==> RS
 ***************************************************************)

instance domT :: (type) rs
apply (intro_classes)
apply (simp add: zero_eq_rs_domT)
apply (simp add: min_rs_domT)
apply (simp add: diff_rs_domT)
done

(************************************************************
                        domT ==> MS
 ************************************************************)

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

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

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

(*** normal_seq lemma ***)

lemma normal_seq_domT:
  "[| normal Ts ; lengtht s <= n |]
   ==> (s :t Ts (lengtht s)) = (s :t Ts n)"
apply (simp add: normal_def)
apply (drule_tac x="lengtht s" in spec)
apply (drule_tac x="n" in spec)
apply (simp add: min_is)

apply (simp add: distance_rs_less_1[THEN sym])
apply (simp add: restT_eq_iff)
apply (drule_tac x="s" in spec)
by (simp)

lemma normal_seq_domT_only_if:
  "[| normal Ts ; lengtht s <= n ; s :t Ts (lengtht s) |]
   ==> s :t Ts n"
by (simp add: normal_seq_domT)

lemma normal_seq_domT_if:
  "[| normal Ts ; lengtht s <= n ; s :t Ts n |]
   ==>  s :t Ts (lengtht s)"
by (simp add: normal_seq_domT)

(*** LimitTset_def in domT ***)

lemma LimitTset_in[simp]:
  "normal (Ts::'a domT infinite_seq) ==> LimitTset Ts : domT"
apply (simp add: domT_def HC_T1_def)
apply (rule conjI)

apply (simp add: LimitTset_def)
apply (rule_tac x="[]t" in exI)
apply (simp)

apply (simp add: prefix_closed_def LimitTset_def)
apply (intro allI impI)
apply (elim conjE exE)

apply (subgoal_tac "lengtht s <= lengtht t")
apply (rule normal_seq_domT_if)
apply (simp_all)
apply (rule memT_prefix_closed, simp_all)
apply (rule length_of_prefix)
apply (simp_all add: not_None_T)
done

(*** :t LimitT ***)

lemma LimitT_memT: 
  "normal (Ts::'a domT infinite_seq)
   ==> (s :t LimitT Ts) = (s :t Ts (lengtht s))"
apply (simp add: memT_def)
apply (simp add: LimitT_def)
apply (simp add: Abs_domT_inverse)
apply (simp add: LimitTset_def memT_def)
done

(*** LimitT lemma ***)

lemma LimitT_Limit_lm:
  "normal (Ts::'a domT infinite_seq)
   ==> (ALL n. (LimitT Ts) rest n = (Ts n) rest n)"
apply (intro allI)
apply (simp add: restT_eq_iff)
apply (simp add: LimitT_memT)
by (auto simp add: normal_seq_domT)

(*** (normal) Ts converges to (LimitT Ts) ***)

lemma LimitT_Limit:
  "normal (Ts::'a domT infinite_seq) ==> Ts convergeTo (LimitT Ts)"
by (simp add: LimitT_Limit_lm rest_Limit)

(*** (cauchy) Ts converges to (LimitT NF Ts) ***)

lemma cauchy_LimitT_Limit:
  "cauchy (Ts::'a domT infinite_seq) ==> Ts convergeTo (LimitT (NF Ts))"
apply (simp add: normal_form_seq_same_Limit)
apply (simp add: LimitT_Limit normal_form_seq_normal)
done

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

lemma domT_cms:
  "cauchy (Ts::'a domT infinite_seq) ==> (EX T. Ts convergeTo T)"
apply (rule_tac x="LimitT (NF Ts)" in exI)
by (simp add: cauchy_LimitT_Limit)

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

instance domT :: (type) cms
apply (intro_classes)
by (simp add: domT_cms)

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

(*** (normal) Limit Ts = LimitT Ts ***)

lemma LimitT_Limit_eq:
  "normal (Ts::'a domT infinite_seq) ==> Limit Ts = LimitT Ts"
apply (insert unique_convergence[of Ts "Limit Ts" "LimitT Ts"])
by (simp add: LimitT_Limit Limit_is normal_cauchy)

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

consts
  RefT :: "'a domT => 'a domT => bool"
  RevT :: "'a domT => 'a domT => bool"

defs
  RefT_def : "RefT S == (%T. (S <= T))"
  RevT_def : "RevT S == (%T. (T <= S))"

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

lemma continuous_rs_RefT: "continuous_rs (RefT S)"
apply (simp add: continuous_rs_def)
apply (intro allI impI)
apply (simp add: RefT_def)
apply (simp add: subsetT_iff)
apply (elim conjE exE)
apply (rename_tac T t)

apply (rule_tac x="lengtht t" in exI)
apply (intro allI impI)
apply (rule_tac x="t" in exI)

apply (simp add: restT_eq_iff)
apply (drule_tac x="t" in spec)
by (simp)

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

lemma continuous_rs_RevT: "continuous_rs (RevT S)"
apply (simp add: continuous_rs_def)
apply (intro allI impI)
apply (simp add: RevT_def)
apply (simp add: subsetT_iff)
apply (elim conjE exE)
apply (rename_tac T t)

apply (rule_tac x="lengtht t" in exI)
apply (intro allI impI)
apply (rule_tac x="t" in exI)

apply (simp add: restT_eq_iff)
apply (drule_tac x="t" 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 restTset_in: 

  T restTset n ∈ domT

lemmas restTset_def_in: 

  {s. s ∈ Rep_domT T ∧ lengtht s ≤ n} ∈ domT

lemma restT_iff: 

  T rest n = {s. s :t T ∧ lengtht s ≤ n}t

lemma in_restT: 

  (s :t T rest n) = (s :t T ∧ lengtht s ≤ n)

lemma restT_eq_iff: 

  (T rest n = S rest m) =
  (∀s. (s :t T ∧ lengtht s ≤ n) = (s :t S ∧ lengtht s ≤ m))

lemma zero_domT: 

  T restTset 0 = {[]t}

lemma zero_eq_rs_domT: 

  T rest 0 = S rest 0

lemma min_rs_domT: 

  T rest m rest n = T rest min m n

lemma contra_diff_rs_domT: 

  ∀n. T rest n = S rest n ==> T = S

lemma diff_rs_domT: 

  T ≠ S ==> ∃n. T rest n ≠ S rest n

lemma normal_seq_domT: 

  [| normal Ts; lengtht s ≤ n |] ==> (s :t Ts (lengtht s)) = (s :t Ts n)

lemma normal_seq_domT_only_if: 

  [| normal Ts; lengtht s ≤ n; s :t Ts (lengtht s) |] ==> s :t Ts n

lemma normal_seq_domT_if: 

  [| normal Ts; lengtht s ≤ n; s :t Ts n |] ==> s :t Ts (lengtht s)

lemma LimitTset_in: 

  normal Ts ==> LimitTset Ts ∈ domT

lemma LimitT_memT: 

  normal Ts ==> (s :t LimitT Ts) = (s :t Ts (lengtht s))

lemma LimitT_Limit_lm: 

  normal Ts ==> ∀n. LimitT Ts rest n = Ts n rest n

lemma LimitT_Limit: 

  normal Ts ==> Ts convergeTo LimitT Ts

lemma cauchy_LimitT_Limit: 

  cauchy Ts ==> Ts convergeTo LimitT (NF Ts)

lemma domT_cms: 

  cauchy Ts ==> ∃T. Ts convergeTo T

lemma LimitT_Limit_eq: 

  normal Ts ==> Limit Ts = LimitT Ts

lemma continuous_rs_RefT: 

  continuous_rs (RefT S)

lemma continuous_rs_RevT: 

  continuous_rs (RevT S)