Theory RefMappings

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