author | nipkow |
Tue, 23 Feb 2016 16:25:08 +0100 | |
changeset 62390 | 842917225d56 |
parent 62116 | bc178c0fe1a1 |
child 63549 | b0d31c7def86 |
permissions | -rw-r--r-- |
62008 | 1 |
(* Title: HOL/HOLCF/IOA/RefMappings.thy |
40945 | 2 |
Author: Olaf Müller |
3071 | 3 |
*) |
4 |
||
62002 | 5 |
section \<open>Refinement Mappings in HOLCF/IOA\<close> |
3071 | 6 |
|
17233 | 7 |
theory RefMappings |
8 |
imports Traces |
|
9 |
begin |
|
10 |
||
36452 | 11 |
default_sort type |
3071 | 12 |
|
62116 | 13 |
definition 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 $ ex = (if a \<in> ext ioa then a \<leadsto> nil else nil)" |
|
17233 | 18 |
|
62116 | 19 |
definition 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))))" |
|
3071 | 23 |
|
62116 | 24 |
definition 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)))" |
|
19741 | 29 |
|
30 |
||
62116 | 31 |
subsection \<open>Transitions and moves\<close> |
19741 | 32 |
|
62116 | 33 |
lemma 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 |
||
38 |
lemma 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 |
|
19741 | 42 |
|
62116 | 43 |
lemma 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 |
||
49 |
lemma 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 |
|
19741 | 55 |
|
56 |
||
62116 | 57 |
subsection \<open>\<open>weak_ref_map\<close> and \<open>ref_map\<close>\<close> |
19741 | 58 |
|
62116 | 59 |
lemma 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 |
|
19741 | 65 |
|
62116 | 66 |
lemma imp_conj_lemma: "(P \<Longrightarrow> Q \<longrightarrow> R) \<Longrightarrow> P \<and> Q \<longrightarrow> R" |
19741 | 67 |
by blast |
68 |
||
62390 | 69 |
declare if_split [split del] |
19741 | 70 |
declare if_weak_cong [cong del] |
71 |
||
62116 | 72 |
lemma 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 |
|
62390 | 84 |
apply (simplesubst if_split) |
62116 | 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 |
|
19741 | 110 |
|
62390 | 111 |
declare if_split [split] |
19741 | 112 |
declare if_weak_cong [cong] |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
113 |
|
3071 | 114 |
end |