src/HOL/HOLCF/IOA/RefMappings.thy

clarified directory structure;

(*  Title:      HOL/HOLCF/IOA/RefMappings.thy
    Author:     Olaf Müller
*)

section \<open>Refinement Mappings in HOLCF/IOA\<close>

theory RefMappings
imports Traces
begin

default_sort type

definition
  move :: "[('a,'s)ioa,('a,'s)pairs,'s,'a,'s] => bool" where
  "move ioa ex s a t =
    (is_exec_frag ioa (s,ex) &  Finite ex &
     laststate (s,ex)=t  &
     mk_trace ioa$ex = (if a:ext(ioa) then a\<leadsto>nil else nil))"

definition
  is_ref_map :: "[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" where
  "is_ref_map f C A =
   ((!s:starts_of(C). f(s):starts_of(A)) &
   (!s t a. reachable C s &
            s \<midarrow>a\<midarrow>C\<rightarrow> t
            --> (? ex. move A ex (f s) a (f t))))"

definition
  is_weak_ref_map :: "[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" where
  "is_weak_ref_map f C A =
   ((!s:starts_of(C). f(s):starts_of(A)) &
   (!s t a. reachable C s &
            s \<midarrow>a\<midarrow>C\<rightarrow> t
            --> (if a:ext(C)
                 then (f s) \<midarrow>a\<midarrow>A\<rightarrow> (f t)
                 else (f s)=(f t))))"


subsection "transitions and moves"


lemma transition_is_ex: "s \<midarrow>a\<midarrow>A\<rightarrow> t ==> ? ex. move A ex s a t"
apply (rule_tac x = " (a,t) \<leadsto>nil" in exI)
apply (simp add: move_def)
done


lemma nothing_is_ex: "(~a:ext A) & s=t ==> ? ex. move A ex s a t"
apply (rule_tac x = "nil" in exI)
apply (simp add: move_def)
done


lemma ei_transitions_are_ex: "(s \<midarrow>a\<midarrow>A\<rightarrow> s') & (s' \<midarrow>a'\<midarrow>A\<rightarrow> s'') & (~a':ext A)  
         ==> ? ex. move A ex s a s''"
apply (rule_tac x = " (a,s') \<leadsto> (a',s'') \<leadsto>nil" in exI)
apply (simp add: move_def)
done


lemma eii_transitions_are_ex: "(s1 \<midarrow>a1\<midarrow>A\<rightarrow> s2) & (s2 \<midarrow>a2\<midarrow>A\<rightarrow> s3) & (s3 \<midarrow>a3\<midarrow>A\<rightarrow> s4) & 
      (~a2:ext A) & (~a3:ext A) ==>  
      ? ex. move A ex s1 a1 s4"
apply (rule_tac x = " (a1,s2) \<leadsto> (a2,s3) \<leadsto> (a3,s4) \<leadsto>nil" in exI)
apply (simp add: move_def)
done


subsection "weak_ref_map and ref_map"

lemma weak_ref_map2ref_map:
  "[| ext C = ext A;  
     is_weak_ref_map f C A |] ==> is_ref_map f C A"
apply (unfold is_weak_ref_map_def is_ref_map_def)
apply auto
apply (case_tac "a:ext A")
apply (auto intro: transition_is_ex nothing_is_ex)
done


lemma imp_conj_lemma: "(P ==> Q-->R) ==> P&Q --> R"
  by blast

declare split_if [split del]
declare if_weak_cong [cong del]

lemma rename_through_pmap: "[| is_weak_ref_map f C A |]  
      ==> (is_weak_ref_map f (rename C g) (rename A g))"
apply (simp add: is_weak_ref_map_def)
apply (rule conjI)
(* 1: start states *)
apply (simp add: rename_def rename_set_def starts_of_def)
(* 2: reachable transitions *)
apply (rule allI)+
apply (rule imp_conj_lemma)
apply (simp (no_asm) add: rename_def rename_set_def)
apply (simp add: externals_def asig_inputs_def asig_outputs_def asig_of_def trans_of_def)
apply safe
apply (simplesubst split_if)
 apply (rule conjI)
 apply (rule impI)
 apply (erule disjE)
 apply (erule exE)
apply (erule conjE)
(* x is input *)
 apply (drule sym)
 apply (drule sym)
apply simp
apply hypsubst+
apply (frule reachable_rename)
apply simp
(* x is output *)
 apply (erule exE)
apply (erule conjE)
 apply (drule sym)
 apply (drule sym)
apply simp
apply hypsubst+
apply (frule reachable_rename)
apply simp
(* x is internal *)
apply (frule reachable_rename)
apply auto
done

declare split_if [split]
declare if_weak_cong [cong]

end