Quelle RefMappings.thy Sprache: Isabelle

(*  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

quality100%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.