Quelle  RefMappings.thy   Sprache: Isabelle

(*  Title:      HOL/HOLCF/IOA/RefMappings.thy
    Author:     Olaf Müller
*)

section ‹Refinement Mappings in HOLCF/IOA›

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 ↝ 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 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 ‹1: start states›
  apply (simp add: rename_def rename_set_def starts_of_def)
  text ‹1: start states›
  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 ‹‹x› is input›
   apply (drule sym)
   apply (drule sym)
  apply simp
  apply hypsubst+
  apply (frule reachable_rename)
  apply simp
  text ‹‹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
  text ‹‹x› is internal›
  apply (frule reachable_rename)
  apply auto
  done

declare if_split [split]
declare if_weak_cong [cong]

end