(* 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) \<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 \ 's2) \ ('a, 's1) ioa \ ('a, 's2) ioa \ bool"
where "is_ref_map f C A \
((\<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 \ 's2) \ ('a, 's1) ioa \ ('a, 's2) ioa \ bool"
where "is_weak_ref_map f C A \
((\<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 \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 \
\<exists>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 \<open>\<open>weak_ref_map\<close> and \<open>ref_map\<close>\<close>
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 if_split [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)
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
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
