(* Title: HOL/HOLCF/IOA/meta_theory/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