1(*  Title:      HOL/HOLCF/IOA/RefMappings.thy
2    Author:     Olaf M��ller
3*)
4
5section \<open>Refinement Mappings in HOLCF/IOA\<close>
6
7theory RefMappings
8imports Traces
9begin
10
11default_sort type
12
13definition move :: "('a, 's) ioa \<Rightarrow> ('a, 's) pairs \<Rightarrow> 's \<Rightarrow> 'a \<Rightarrow> 's \<Rightarrow> bool"
14  where "move ioa ex s a t \<longleftrightarrow>
15    is_exec_frag ioa (s, ex) \<and> Finite ex \<and>
16    laststate (s, ex) = t \<and>
17    mk_trace ioa \<cdot> ex = (if a \<in> ext ioa then a \<leadsto> nil else nil)"
18
19definition is_ref_map :: "('s1 \<Rightarrow> 's2) \<Rightarrow> ('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool"
20  where "is_ref_map f C A \<longleftrightarrow>
21   ((\<forall>s \<in> starts_of C. f s \<in> starts_of A) \<and>
22     (\<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))))"
23
24definition is_weak_ref_map :: "('s1 \<Rightarrow> 's2) \<Rightarrow> ('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool"
25  where "is_weak_ref_map f C A \<longleftrightarrow>
26    ((\<forall>s \<in> starts_of C. f s \<in> starts_of A) \<and>
27      (\<forall>s t a. reachable C s \<and> s \<midarrow>a\<midarrow>C\<rightarrow> t \<longrightarrow>
28        (if a \<in> ext C then (f s) \<midarrow>a\<midarrow>A\<rightarrow> (f t) else f s = f t)))"
29
30
31subsection \<open>Transitions and moves\<close>
32
33lemma transition_is_ex: "s \<midarrow>a\<midarrow>A\<rightarrow> t \<Longrightarrow> \<exists>ex. move A ex s a t"
34  apply (rule_tac x = " (a, t) \<leadsto> nil" in exI)
35  apply (simp add: move_def)
36  done
37
38lemma nothing_is_ex: "a \<notin> ext A \<and> s = t \<Longrightarrow> \<exists>ex. move A ex s a t"
39  apply (rule_tac x = "nil" in exI)
40  apply (simp add: move_def)
41  done
42
43lemma ei_transitions_are_ex:
44  "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''"
45  apply (rule_tac x = " (a,s') \<leadsto> (a',s'') \<leadsto>nil" in exI)
46  apply (simp add: move_def)
47  done
48
49lemma eii_transitions_are_ex:
50  "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>
51    \<exists>ex. move A ex s1 a1 s4"
52  apply (rule_tac x = "(a1, s2) \<leadsto> (a2, s3) \<leadsto> (a3, s4) \<leadsto> nil" in exI)
53  apply (simp add: move_def)
54  done
55
56
57subsection \<open>\<open>weak_ref_map\<close> and \<open>ref_map\<close>\<close>
58
59lemma weak_ref_map2ref_map: "ext C = ext A \<Longrightarrow> is_weak_ref_map f C A \<Longrightarrow> is_ref_map f C A"
60  apply (unfold is_weak_ref_map_def is_ref_map_def)
61  apply auto
62  apply (case_tac "a \<in> ext A")
63  apply (auto intro: transition_is_ex nothing_is_ex)
64  done
65
66lemma imp_conj_lemma: "(P \<Longrightarrow> Q \<longrightarrow> R) \<Longrightarrow> P \<and> Q \<longrightarrow> R"
67  by blast
68
69declare if_split [split del]
70declare if_weak_cong [cong del]
71
72lemma rename_through_pmap:
73  "is_weak_ref_map f C A \<Longrightarrow> is_weak_ref_map f (rename C g) (rename A g)"
74  apply (simp add: is_weak_ref_map_def)
75  apply (rule conjI)
76  text \<open>1: start states\<close>
77  apply (simp add: rename_def rename_set_def starts_of_def)
78  text \<open>1: start states\<close>
79  apply (rule allI)+
80  apply (rule imp_conj_lemma)
81  apply (simp (no_asm) add: rename_def rename_set_def)
82  apply (simp add: externals_def asig_inputs_def asig_outputs_def asig_of_def trans_of_def)
83  apply safe
84  apply (simplesubst if_split)
85   apply (rule conjI)
86   apply (rule impI)
87   apply (erule disjE)
88   apply (erule exE)
89  apply (erule conjE)
90  text \<open>\<open>x\<close> is input\<close>
91   apply (drule sym)
92   apply (drule sym)
93  apply simp
94  apply hypsubst+
95  apply (frule reachable_rename)
96  apply simp
97  text \<open>\<open>x\<close> is output\<close>
98   apply (erule exE)
99  apply (erule conjE)
100   apply (drule sym)
101   apply (drule sym)
102  apply simp
103  apply hypsubst+
104  apply (frule reachable_rename)
105  apply simp
106  text \<open>\<open>x\<close> is internal\<close>
107  apply (frule reachable_rename)
108  apply auto
109  done
110
111declare if_split [split]
112declare if_weak_cong [cong]
113
114end
115