(* Title: HOLCF/IOA/meta_theory/RefMappings.thy
ID: $Id$
Author: Olaf Müller
*)
header {* Refinement Mappings in HOLCF/IOA *}
theory RefMappings
imports Traces
begin
defaultsort 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>>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 -a--C-> 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 -a--C-> t
--> (if a:ext(C)
then (f s) -a--A-> (f t)
else (f s)=(f t))))"
subsection "transitions and moves"
lemma transition_is_ex: "s -a--A-> t ==> ? ex. move A ex s a t"
apply (rule_tac x = " (a,t) >>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 -a--A-> s') & (s' -a'--A-> s'') & (~a':ext A)
==> ? ex. move A ex s a s''"
apply (rule_tac x = " (a,s') >> (a',s'') >>nil" in exI)
apply (simp add: move_def)
done
lemma eii_transitions_are_ex: "(s1 -a1--A-> s2) & (s2 -a2--A-> s3) & (s3 -a3--A-> s4) &
(~a2:ext A) & (~a3:ext A) ==>
? ex. move A ex s1 a1 s4"
apply (rule_tac x = " (a1,s2) >> (a2,s3) >> (a3,s4) >>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 (tactic "safe_tac set_cs")
apply (case_tac "a:ext A")
apply (rule transition_is_ex)
apply (simp (no_asm_simp))
apply (rule nothing_is_ex)
apply simp
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