(* 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 \<Rightarrow> ('a, 's) pairs \<Rightarrow> 's \<Rightarrow> 'a \<Rightarrow> 's \<Rightarrow> bool"
where "move ioa ex s a t \<longleftrightarrow>
is_exec_frag ioa (s, ex) \<and> Finite ex \<and>
laststate (s, ex) = t \<and>
mk_trace ioa \<cdot> ex = (if a \<in> ext ioa then a \<leadsto> nil else nil)"
definition is_ref_map :: "('s1 \<Rightarrow> 's2) \<Rightarrow> ('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool"
where "is_ref_map f C A \<longleftrightarrow>
((\<forall>s \<in> starts_of C. f s \<in> starts_of A) \<and>
(\<forall>s t a. reachable C s \<and> s \<midarrow>a\<midarrow>C\<rightarrow> t \<longrightarrow> (\<exists>ex. move A ex (f s) a (f t))))"
definition is_weak_ref_map :: "('s1 \<Rightarrow> 's2) \<Rightarrow> ('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool"
where "is_weak_ref_map f C A \<longleftrightarrow>
((\<forall>s \<in> starts_of C. f s \<in> starts_of A) \<and>
(\<forall>s t a. reachable C s \<and> s \<midarrow>a\<midarrow>C\<rightarrow> t \<longrightarrow>
(if a \<in> ext C then (f s) \<midarrow>a\<midarrow>A\<rightarrow> (f t) else f s = f t)))"
subsection \<open>Transitions and moves\<close>
lemma transition_is_ex: "s \<midarrow>a\<midarrow>A\<rightarrow> t \<Longrightarrow> \<exists>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 \<notin> ext A \<and> s = t \<Longrightarrow> \<exists>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' \<and> s' \<midarrow>a'\<midarrow>A\<rightarrow> s'' \<and> a' \<notin> ext A \<Longrightarrow> \<exists>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 \<and> s2 \<midarrow>a2\<midarrow>A\<rightarrow> s3 \<and> s3 \<midarrow>a3\<midarrow>A\<rightarrow> s4 \<and> a2 \<notin> ext A \<and> a3 \<notin> ext A \<Longrightarrow>
\<exists>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 \<open>\<open>weak_ref_map\<close> and \<open>ref_map\<close>\<close>
lemma weak_ref_map2ref_map: "ext C = ext A \<Longrightarrow> is_weak_ref_map f C A \<Longrightarrow> is_ref_map f C A"
apply (unfold is_weak_ref_map_def is_ref_map_def)
apply auto
apply (case_tac "a \<in> ext A")
apply (auto intro: transition_is_ex nothing_is_ex)
done
lemma imp_conj_lemma: "(P \<Longrightarrow> Q \<longrightarrow> R) \<Longrightarrow> P \<and> Q \<longrightarrow> R"
by blast
declare if_split [split del]
declare if_weak_cong [cong del]
lemma rename_through_pmap:
"is_weak_ref_map f C A \<Longrightarrow> is_weak_ref_map f (rename C g) (rename A g)"
apply (simp add: is_weak_ref_map_def)
apply (rule conjI)
text \<open>1: start states\<close>
apply (simp add: rename_def rename_set_def starts_of_def)
text \<open>1: start states\<close>
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 if_split)
apply (rule conjI)
apply (rule impI)
apply (erule disjE)
apply (erule exE)
apply (erule conjE)
text \<open>\<open>x\<close> is input\<close>
apply (drule sym)
apply (drule sym)
apply simp
apply hypsubst+
apply (frule reachable_rename)
apply simp
text \<open>\<open>x\<close> is output\<close>
apply (erule exE)
apply (erule conjE)
apply (drule sym)
apply (drule sym)
apply simp
apply hypsubst+
apply (frule reachable_rename)
apply simp
text \<open>\<open>x\<close> is internal\<close>
apply (frule reachable_rename)
apply auto
done
declare if_split [split]
declare if_weak_cong [cong]
end