author | wenzelm |
Wed, 30 Dec 2015 22:05:00 +0100 | |
changeset 62003 | ba465fcd0267 |
parent 62002 | f1599e98c4d0 |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/IOA/meta_theory/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 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
13 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
14 |
move :: "[('a,'s)ioa,('a,'s)pairs,'s,'a,'s] => bool" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
15 |
"move ioa ex s a t = |
17233 | 16 |
(is_exec_frag ioa (s,ex) & Finite ex & |
17 |
laststate (s,ex)=t & |
|
62001 | 18 |
mk_trace ioa$ex = (if a:ext(ioa) then a\<leadsto>nil else nil))" |
3071 | 19 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
20 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
21 |
is_ref_map :: "[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
22 |
"is_ref_map f C A = |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
23 |
((!s:starts_of(C). f(s):starts_of(A)) & |
17233 | 24 |
(!s t a. reachable C s & |
62003 | 25 |
s \<midarrow>a\<midarrow>C\<rightarrow> t |
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
26 |
--> (? ex. move A ex (f s) a (f t))))" |
17233 | 27 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
28 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
29 |
is_weak_ref_map :: "[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
30 |
"is_weak_ref_map f C A = |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
31 |
((!s:starts_of(C). f(s):starts_of(A)) & |
17233 | 32 |
(!s t a. reachable C s & |
62003 | 33 |
s \<midarrow>a\<midarrow>C\<rightarrow> t |
17233 | 34 |
--> (if a:ext(C) |
62003 | 35 |
then (f s) \<midarrow>a\<midarrow>A\<rightarrow> (f t) |
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
36 |
else (f s)=(f t))))" |
3071 | 37 |
|
19741 | 38 |
|
39 |
subsection "transitions and moves" |
|
40 |
||
41 |
||
62003 | 42 |
lemma transition_is_ex: "s \<midarrow>a\<midarrow>A\<rightarrow> t ==> ? ex. move A ex s a t" |
62001 | 43 |
apply (rule_tac x = " (a,t) \<leadsto>nil" in exI) |
19741 | 44 |
apply (simp add: move_def) |
45 |
done |
|
46 |
||
47 |
||
48 |
lemma nothing_is_ex: "(~a:ext A) & s=t ==> ? ex. move A ex s a t" |
|
49 |
apply (rule_tac x = "nil" in exI) |
|
50 |
apply (simp add: move_def) |
|
51 |
done |
|
52 |
||
53 |
||
62003 | 54 |
lemma ei_transitions_are_ex: "(s \<midarrow>a\<midarrow>A\<rightarrow> s') & (s' \<midarrow>a'\<midarrow>A\<rightarrow> s'') & (~a':ext A) |
19741 | 55 |
==> ? ex. move A ex s a s''" |
62001 | 56 |
apply (rule_tac x = " (a,s') \<leadsto> (a',s'') \<leadsto>nil" in exI) |
19741 | 57 |
apply (simp add: move_def) |
58 |
done |
|
59 |
||
60 |
||
62003 | 61 |
lemma eii_transitions_are_ex: "(s1 \<midarrow>a1\<midarrow>A\<rightarrow> s2) & (s2 \<midarrow>a2\<midarrow>A\<rightarrow> s3) & (s3 \<midarrow>a3\<midarrow>A\<rightarrow> s4) & |
19741 | 62 |
(~a2:ext A) & (~a3:ext A) ==> |
63 |
? ex. move A ex s1 a1 s4" |
|
62001 | 64 |
apply (rule_tac x = " (a1,s2) \<leadsto> (a2,s3) \<leadsto> (a3,s4) \<leadsto>nil" in exI) |
19741 | 65 |
apply (simp add: move_def) |
66 |
done |
|
67 |
||
68 |
||
69 |
subsection "weak_ref_map and ref_map" |
|
70 |
||
26306 | 71 |
lemma weak_ref_map2ref_map: |
19741 | 72 |
"[| ext C = ext A; |
73 |
is_weak_ref_map f C A |] ==> is_ref_map f C A" |
|
74 |
apply (unfold is_weak_ref_map_def is_ref_map_def) |
|
26359 | 75 |
apply auto |
19741 | 76 |
apply (case_tac "a:ext A") |
26359 | 77 |
apply (auto intro: transition_is_ex nothing_is_ex) |
19741 | 78 |
done |
79 |
||
80 |
||
81 |
lemma imp_conj_lemma: "(P ==> Q-->R) ==> P&Q --> R" |
|
82 |
by blast |
|
83 |
||
84 |
declare split_if [split del] |
|
85 |
declare if_weak_cong [cong del] |
|
86 |
||
87 |
lemma rename_through_pmap: "[| is_weak_ref_map f C A |] |
|
88 |
==> (is_weak_ref_map f (rename C g) (rename A g))" |
|
89 |
apply (simp add: is_weak_ref_map_def) |
|
90 |
apply (rule conjI) |
|
91 |
(* 1: start states *) |
|
92 |
apply (simp add: rename_def rename_set_def starts_of_def) |
|
93 |
(* 2: reachable transitions *) |
|
94 |
apply (rule allI)+ |
|
95 |
apply (rule imp_conj_lemma) |
|
96 |
apply (simp (no_asm) add: rename_def rename_set_def) |
|
97 |
apply (simp add: externals_def asig_inputs_def asig_outputs_def asig_of_def trans_of_def) |
|
98 |
apply safe |
|
99 |
apply (simplesubst split_if) |
|
100 |
apply (rule conjI) |
|
101 |
apply (rule impI) |
|
102 |
apply (erule disjE) |
|
103 |
apply (erule exE) |
|
104 |
apply (erule conjE) |
|
105 |
(* x is input *) |
|
106 |
apply (drule sym) |
|
107 |
apply (drule sym) |
|
108 |
apply simp |
|
109 |
apply hypsubst+ |
|
110 |
apply (frule reachable_rename) |
|
111 |
apply simp |
|
112 |
(* x is output *) |
|
113 |
apply (erule exE) |
|
114 |
apply (erule conjE) |
|
115 |
apply (drule sym) |
|
116 |
apply (drule sym) |
|
117 |
apply simp |
|
118 |
apply hypsubst+ |
|
119 |
apply (frule reachable_rename) |
|
120 |
apply simp |
|
121 |
(* x is internal *) |
|
122 |
apply (frule reachable_rename) |
|
123 |
apply auto |
|
124 |
done |
|
125 |
||
126 |
declare split_if [split] |
|
127 |
declare if_weak_cong [cong] |
|
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
128 |
|
3071 | 129 |
end |