Theory Ext_pre_choice_cms

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

theory Ext_pre_choice_cms = Ext_pre_choice + Act_prefix_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 : contraction map
         2. [[? :X -> Pf]]F : contraction map
         3. 
         4. 

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

(*********************************************************
                   map Ext_pre_choice T
 *********************************************************)

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

lemma Ext_pre_choice_Act_prefix_restT_sub:
   "[| ALL a : X.
         [[a -> Pf a]]T ev1 rest n <= [[a -> 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: Ext_pre_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)
apply (simp add: Act_prefix_memT)
apply (drule mp)
 apply (rule_tac x="s" in exI)
 apply (simp)
apply (elim conjE exE)
apply (rule_tac x="a" in exI)
apply (rule_tac x="s" in exI)
apply (simp add: not_None_T)
done

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

lemma Ext_pre_choice_Act_prefix_restT:
   "[| ALL a : X.
         [[a -> Pf a]]T ev1 rest n = [[a -> 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: Ext_pre_choice_Act_prefix_restT_sub)

(*** distT lemma ***)

lemma Ext_pre_choice_Act_prefix_distT_nonempty:
"[| X ~= {} ;
    TTs = {([[a -> Pf a]]T ev1, [[a -> 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 (force)

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

(*** contractionT lemma ***)

lemma Ext_pre_choice_evalT_contraction_half_nonempty_lm:
  "[| X ~= {}; ALL a. distance ([[Pf a]]T ev1, [[Pf a]]T ev2) 
                   <= distance (ev1, ev2) |]
    ==> distance ([[? :X -> Pf]]T ev1, [[? :X -> Pf]]T ev2) * 2 
     <= distance (ev1, ev2)"
apply (insert Ext_pre_choice_Act_prefix_distT_nonempty
       [of X "{([[a -> Pf a]]T ev1, [[a -> Pf a]]T ev2) |a. a : X}" Pf ev1 ev2])
apply (simp)
apply (elim conjE exE, simp)
apply (drule_tac x="aa" in spec)
apply (subgoal_tac 
    "distance ([[aa -> Pf aa]]T ev1, [[aa -> Pf aa]]T ev2) * 2
   = distance ([[Pf aa]]T ev1, [[Pf aa]]T ev2)")
apply (simp)
by (simp add: Act_prefix_evalT_contraction_half_lm)

(*** Ext_pre_choice_evalT_contraction_half ***)

lemma Ext_pre_choice_evalT_contraction_half: 
 "ALL a. non_expanding [[Pf a]]T
  ==> contraction_alpha [[? :X -> Pf]]T (1 / 2)"
apply (simp add: contraction_alpha_def non_expanding_def map_alpha_def)
apply (case_tac "X = {}")
apply (simp add: evalT_def)
by (simp add: Ext_pre_choice_evalT_contraction_half_nonempty_lm)

(*** Ext_pre_choice_evalT_contraction ***)

lemma Ext_pre_choice_evalT_contraction: 
 "ALL a. non_expanding [[Pf a]]T
  ==> contraction [[? :X -> Pf]]T"
apply (simp add: contraction_def)
apply (rule_tac x="1/2" in exI)
by (simp add: Ext_pre_choice_evalT_contraction_half)

(*** Ext_pre_choice_evalT_non_expanding ***)

lemma Ext_pre_choice_evalT_non_expanding:
 "ALL a. non_expanding [[Pf a]]T ==> non_expanding [[? :X -> Pf]]T"
apply (rule contraction_non_expanding)
by (simp add: Ext_pre_choice_evalT_contraction)

(*********************************************************
                   map Ext_pre_choice F
 *********************************************************)

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

lemma Ext_pre_choice_Act_prefix_restF_sub:
   "[| ALL a : X.
         [[a -> Pf a]]F ev1 rest n <= [[a -> 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: Ext_pre_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 (simp add: Act_prefix_memF)
apply (drule mp)
 apply (rule_tac x="sa" in exI)
 apply (simp)
apply (elim conjE exE)
apply (rule_tac x="a" in exI)
apply (rule_tac x="sa" in exI)
apply (simp add: not_None_F)

apply (drule_tac x="a" in bspec, simp)
apply (drule_tac x="s" in spec)
apply (drule_tac x="Xa" in spec)
apply (simp add: Act_prefix_memF)
apply (drule mp)
 apply (rule conjI)
 apply (rule_tac x="sa" in exI, simp)
 apply (rule_tac x="s'" in exI, simp)
apply (elim conjE exE)
apply (rule_tac x="a" in exI)
apply (rule_tac x="sa" in exI)
apply (simp add: not_None_F)
done

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

lemma Ext_pre_choice_Act_prefix_restF:
   "[| ALL a : X.
         [[a -> Pf a]]F ev1 rest n = [[a -> 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: Ext_pre_choice_Act_prefix_restF_sub)

(*** distF lemma ***)

lemma Ext_pre_choice_Act_prefix_distF_nonempty:
"[| X ~= {} ;
    FFs = {([[a -> Pf a]]F ev1, [[a -> 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 (force)

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

(*** contractionF lemma ***)

lemma Ext_pre_choice_evalF_contraction_half_nonempty_lm:
  "[| X ~= {}; ALL a. distance ([[Pf a]]F ev1, [[Pf a]]F ev2) 
                   <= distance (ev1, ev2) |]
    ==> distance ([[? :X -> Pf]]F ev1, [[? :X -> Pf]]F ev2) * 2 
     <= distance (ev1, ev2)"
apply (insert Ext_pre_choice_Act_prefix_distF_nonempty
       [of X "{([[a -> Pf a]]F ev1, [[a -> Pf a]]F ev2) |a. a : X}" Pf ev1 ev2])
apply (simp)
apply (elim conjE exE, simp)
apply (drule_tac x="aa" in spec)
apply (subgoal_tac 
    "distance ([[aa -> Pf aa]]F ev1, [[aa -> Pf aa]]F ev2) * 2
   = distance ([[Pf aa]]F ev1, [[Pf aa]]F ev2)")
apply (simp)
by (simp add: Act_prefix_evalF_contraction_half_lm)

(*** Ext_pre_choice_evalF_contraction_half ***)

lemma Ext_pre_choice_evalF_contraction_half: 
 "ALL a. non_expanding [[Pf a]]F
  ==> contraction_alpha [[? :X -> Pf]]F (1 / 2)"
apply (simp add: contraction_alpha_def non_expanding_def map_alpha_def)
apply (case_tac "X = {}")
apply (simp add: evalF_def)
by (simp add: Ext_pre_choice_evalF_contraction_half_nonempty_lm)

(*** Ext_pre_choice_evalF_contraction ***)

lemma Ext_pre_choice_evalF_contraction: 
 "ALL a. non_expanding [[Pf a]]F
  ==> contraction [[? :X -> Pf]]F"
apply (simp add: contraction_def)
apply (rule_tac x="1/2" in exI)
by (simp add: Ext_pre_choice_evalF_contraction_half)

(*** Ext_pre_choice_evalF_non_expanding ***)

lemma Ext_pre_choice_evalF_non_expanding:
 "ALL a. non_expanding [[Pf a]]F ==> non_expanding [[? :X -> Pf]]F"
apply (rule contraction_non_expanding)
by (simp add: Ext_pre_choice_evalF_contraction)

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

declare disj_not1   [simp]
declare not_None_eq [simp]

end