Theory Rep_int_choice_cms (Isabelle2004: April 2004)

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

theory Rep_int_choice_cms = Rep_int_choice + Domain_SF_prod_cms:

(*  The following simplification rules are deleted in this theory file *)
(*  because they unexpectly rewrite UnionT and InterT.                 *)
(*                  disj_not1: (~ P | Q) = (P --> Q)                   *)

declare disj_not1 [simp del]

(*  The following simplification is sometimes unexpected.              *)
(*                                                                     *)
(*             not_None_eq: (x ~= None) = (EX y. x = Some y)           *)

declare not_None_eq [simp del]

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

         1. [[! :X .. Pf]]T : non_expanding
         2. [[! :X .. Pf]]F : non_expanding
         3. 
         4. 

 *****************************************************************)

(*********************************************************
                   map Rep_int_choice T
 *********************************************************)

(*** restT (subset) ***)

lemma Rep_int_choice_restT_sub:
   "[| ALL a : X. [[Pf a]]T ev1 rest n <= [[Pf a]]T ev2 rest n |]
        ==> [[! :X .. Pf]]T ev1 rest n <= [[! :X .. Pf]]T ev2 rest n"
apply (simp add: subsetT_iff)
apply (intro allI impI)
apply (simp add: in_restT)
apply (simp add: Rep_int_choice_memT)
apply (elim conjE exE disjE)
apply (simp_all)

apply (drule_tac x="a" in bspec, simp)
apply (drule_tac x="t" in spec, simp)
by (fast)

(*** restT (equal) ***)

lemma Rep_int_choice_restT:
   "[| ALL a : X. [[Pf a]]T ev1 rest n = [[Pf a]]T ev2 rest n |]
        ==> [[! :X .. Pf]]T ev1 rest n = [[! :X .. Pf]]T ev2 rest n"
apply (rule order_antisym)
by (simp_all add: Rep_int_choice_restT_sub)

(*** distT lemma ***)

lemma Rep_int_choice_distT_nonempty:
"[| X ~= {} ; TTs = {([[Pf a]]T ev1, [[Pf a]]T ev2)|a. a : X} |]
 ==> (EX TT. TT:TTs & 
             distance([[! :X .. Pf]]T ev1, [[! :X .. Pf]]T ev2) 
          <= distance((fst TT), (snd TT)))"
apply (rule rest_to_dist_pair)
apply (fast)

apply (intro allI impI)
apply (rule Rep_int_choice_restT)
apply (rule ballI)
apply (simp)
apply (drule_tac x="[[Pf a]]T ev1" in spec)
apply (drule_tac x="[[Pf a]]T ev2" in spec)
by (auto)

(*** map_alpha T lemma ***)

lemma Rep_int_choice_evalT_map_alpha_nonempty_lm:
  "[| X ~= {};
      ALL a. distance ([[Pf a]]T ev1, [[Pf a]]T ev2) 
           <= alpha * distance (ev1, ev2) |]
    ==> distance ([[! :X .. Pf]]T ev1, [[! :X .. Pf]]T ev2)
     <= alpha *  distance (ev1, ev2)"
apply (insert Rep_int_choice_distT_nonempty
       [of X "{([[Pf a]]T ev1, [[Pf a]]T ev2) |a. a : X}" Pf ev1 ev2])
apply (simp)
apply (elim conjE exE, simp)
apply (drule_tac x="aa" in spec)
by (force)

(*** Rep_int_choice_evalT_map_alpha ***)

lemma Rep_int_choice_evalT_map_alpha:
 "ALL a. map_alpha [[Pf a]]T alpha ==> map_alpha [[! :X .. Pf]]T alpha"
apply (simp add: map_alpha_def)
apply (case_tac "X = {}")
 apply (simp add: evalT_def)
 apply (simp add: real_mult_order_eq)
apply (simp add: Rep_int_choice_evalT_map_alpha_nonempty_lm)
done

(*** Rep_int_choice_evalT_non_expanding ***)

lemma Rep_int_choice_evalT_non_expanding:
 "ALL a. non_expanding [[Pf a]]T ==> non_expanding [[! :X .. Pf]]T"
by (simp add: non_expanding_def Rep_int_choice_evalT_map_alpha)

(*** Rep_int_choice_evalT_contraction_alpha ***)

lemma Rep_int_choice_evalT_contraction_alpha:
 "ALL a. contraction_alpha [[Pf a]]T alpha 
     ==> contraction_alpha [[! :X .. Pf]]T alpha"
by (simp add: contraction_alpha_def Rep_int_choice_evalT_map_alpha)

(*********************************************************
                   map Rep_int_choice F
 *********************************************************)

(*** restF (subset) ***)

lemma Rep_int_choice_restF_sub:
   "[| ALL a : X. [[Pf a]]F ev1 rest n <= [[Pf a]]F ev2 rest n |]
        ==> [[! :X .. Pf]]F ev1 rest n <= [[! :X .. Pf]]F ev2 rest n"
apply (simp add: subsetF_iff)
apply (intro allI impI)
apply (simp add: in_restF)
apply (simp add: Rep_int_choice_memF)
apply (elim conjE exE disjE)
apply (simp_all)

apply (drule_tac x="a" in bspec, simp)
apply (drule_tac x="s" in spec)
apply (drule_tac x="Xa" in spec)
apply (rule_tac x="a" in exI, simp)
by (fast)

(*** restF (equal) ***)

lemma Rep_int_choice_restF:
   "[| ALL a : X. [[Pf a]]F ev1 rest n = [[Pf a]]F ev2 rest n |]
        ==> [[! :X .. Pf]]F ev1 rest n = [[! :X .. Pf]]F ev2 rest n"
apply (rule order_antisym)
by (simp_all add: Rep_int_choice_restF_sub)

(*** distF lemma ***)

lemma Rep_int_choice_distF_nonempty:
"[| X ~= {} ; FFs = {([[Pf a]]F ev1, [[Pf a]]F ev2)|a. a : X} |]
 ==> (EX FF. FF:FFs & 
             distance([[! :X .. Pf]]F ev1, [[! :X .. Pf]]F ev2) 
          <= distance((fst FF), (snd FF)))"
apply (rule rest_to_dist_pair)
apply (fast)

apply (intro allI impI)
apply (rule Rep_int_choice_restF)
apply (rule ballI)
apply (simp)
apply (drule_tac x="[[Pf a]]F ev1" in spec)
apply (drule_tac x="[[Pf a]]F ev2" in spec)
by (auto)

(*** map_alpha F lemma ***)

lemma Rep_int_choice_evalF_map_alpha_nonempty_lm:
  "[| X ~= {};
      ALL a. distance ([[Pf a]]F ev1, [[Pf a]]F ev2) 
           <= alpha * distance (ev1, ev2) |]
    ==> distance ([[! :X .. Pf]]F ev1, [[! :X .. Pf]]F ev2)
     <= alpha *  distance (ev1, ev2)"
apply (insert Rep_int_choice_distF_nonempty
       [of X "{([[Pf a]]F ev1, [[Pf a]]F ev2) |a. a : X}" Pf ev1 ev2])
apply (simp)
apply (elim conjE exE, simp)
apply (drule_tac x="aa" in spec)
by (force)

(*** Rep_int_choice_evalF_map_alpha ***)

lemma Rep_int_choice_evalF_map_alpha:
 "ALL a. map_alpha [[Pf a]]F alpha ==> map_alpha [[! :X .. Pf]]F alpha"
apply (simp add: map_alpha_def)
apply (case_tac "X = {}")
 apply (simp add: evalF_def)
 apply (simp add: real_mult_order_eq)
apply (simp add: Rep_int_choice_evalF_map_alpha_nonempty_lm)
done

(*** Rep_int_choice_evalF_non_expanding ***)

lemma Rep_int_choice_evalF_non_expanding:
 "ALL a. non_expanding [[Pf a]]F ==> non_expanding [[! :X .. Pf]]F"
by (simp add: non_expanding_def Rep_int_choice_evalF_map_alpha)

(*** Rep_int_choice_evalF_contraction_alpha ***)

lemma Rep_int_choice_evalF_contraction_alpha:
 "ALL a. contraction_alpha [[Pf a]]F alpha 
     ==> contraction_alpha [[! :X .. Pf]]F alpha"
by (simp add: contraction_alpha_def Rep_int_choice_evalF_map_alpha)

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

declare disj_not1   [simp]
declare not_None_eq [simp]

end

lemma Rep_int_choice_restT_sub:

  ∀a∈X. [[Pf a]]T ev1 rest n ≤ [[Pf a]]T ev2 rest n
  ==> [[! :X .. Pf]]T ev1 rest n ≤ [[! :X .. Pf]]T ev2 rest n

lemma Rep_int_choice_restT:

  ∀a∈X. [[Pf a]]T ev1 rest n = [[Pf a]]T ev2 rest n
  ==> [[! :X .. Pf]]T ev1 rest n = [[! :X .. Pf]]T ev2 rest n

lemma Rep_int_choice_distT_nonempty:

  [| X ≠ {}; TTs = {([[Pf a]]T ev1, [[Pf a]]T ev2) |a. a ∈ X} |]
  ==> ∃TT. TT ∈ TTs ∧
           distance ([[! :X .. Pf]]T ev1, [[! :X .. Pf]]T ev2)
           ≤ distance (fst TT, snd TT)

lemma Rep_int_choice_evalT_map_alpha_nonempty_lm:

  [| X ≠ {};
     ∀a. distance ([[Pf a]]T ev1, [[Pf a]]T ev2) ≤ alpha * distance (ev1, ev2) |]
  ==> distance ([[! :X .. Pf]]T ev1, [[! :X .. Pf]]T ev2)
      ≤ alpha * distance (ev1, ev2)

lemma Rep_int_choice_evalT_map_alpha:

  ∀a. map_alpha [[Pf a]]T alpha ==> map_alpha [[! :X .. Pf]]T alpha

lemma Rep_int_choice_evalT_non_expanding:

  ∀a. non_expanding [[Pf a]]T ==> non_expanding [[! :X .. Pf]]T

lemma Rep_int_choice_evalT_contraction_alpha:

  ∀a. contraction_alpha [[Pf a]]T alpha
  ==> contraction_alpha [[! :X .. Pf]]T alpha

lemma Rep_int_choice_restF_sub:

  ∀a∈X. [[Pf a]]F ev1 rest n ≤ [[Pf a]]F ev2 rest n
  ==> [[! :X .. Pf]]F ev1 rest n ≤ [[! :X .. Pf]]F ev2 rest n

lemma Rep_int_choice_restF:

  ∀a∈X. [[Pf a]]F ev1 rest n = [[Pf a]]F ev2 rest n
  ==> [[! :X .. Pf]]F ev1 rest n = [[! :X .. Pf]]F ev2 rest n

lemma Rep_int_choice_distF_nonempty:

  [| X ≠ {}; FFs = {([[Pf a]]F ev1, [[Pf a]]F ev2) |a. a ∈ X} |]
  ==> ∃FF. FF ∈ FFs ∧
           distance ([[! :X .. Pf]]F ev1, [[! :X .. Pf]]F ev2)
           ≤ distance (fst FF, snd FF)

lemma Rep_int_choice_evalF_map_alpha_nonempty_lm:

  [| X ≠ {};
     ∀a. distance ([[Pf a]]F ev1, [[Pf a]]F ev2) ≤ alpha * distance (ev1, ev2) |]
  ==> distance ([[! :X .. Pf]]F ev1, [[! :X .. Pf]]F ev2)
      ≤ alpha * distance (ev1, ev2)

lemma Rep_int_choice_evalF_map_alpha:

  ∀a. map_alpha [[Pf a]]F alpha ==> map_alpha [[! :X .. Pf]]F alpha

lemma Rep_int_choice_evalF_non_expanding:

  ∀a. non_expanding [[Pf a]]F ==> non_expanding [[! :X .. Pf]]F

lemma Rep_int_choice_evalF_contraction_alpha:

  ∀a. contraction_alpha [[Pf a]]F alpha
  ==> contraction_alpha [[! :X .. Pf]]F alpha