58 @{typ 'a}. *} |
58 @{typ 'a}. *} |
59 |
59 |
60 locale Abs_Int = Gamma where \<gamma>=\<gamma> for \<gamma> :: "'av::semilattice \<Rightarrow> val set" |
60 locale Abs_Int = Gamma where \<gamma>=\<gamma> for \<gamma> :: "'av::semilattice \<Rightarrow> val set" |
61 begin |
61 begin |
62 |
62 |
63 fun step' :: "'av st option \<Rightarrow> 'av st option acom \<Rightarrow> 'av st option acom" where |
63 (* Interpretation would be nicer but is impossible *) |
64 "step' S (SKIP {P}) = (SKIP {S})" | |
64 definition "step' = Step.Step |
65 "step' S (x ::= e {P}) = |
65 (\<lambda>x e S. case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(update S x (aval' e S))) |
66 x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(update S x (aval' e S))}" | |
66 (\<lambda>b S. S)" |
67 "step' S (C1; C2) = step' S C1; step' (post C1) C2" | |
67 |
68 "step' S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) = |
68 lemma [code,simp]: "step' S (SKIP {P}) = (SKIP {S})" |
69 (IF b THEN {S} step' P1 C1 ELSE {S} step' P2 C2 {post C1 \<squnion> post C2})" | |
69 by(simp add: step'_def Step.Step.simps) |
70 "step' S ({I} WHILE b DO {P} C {Q}) = |
70 lemma [code,simp]: "step' S (x ::= e {P}) = |
71 {S \<squnion> post C} WHILE b DO {I} step' P C {I}" |
71 x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(update S x (aval' e S))}" |
|
72 by(simp add: step'_def Step.Step.simps) |
|
73 lemma [code,simp]: "step' S (C1; C2) = step' S C1; step' (post C1) C2" |
|
74 by(simp add: step'_def Step.Step.simps) |
|
75 lemma [code,simp]: "step' S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) = |
|
76 IF b THEN {S} step' P1 C1 ELSE {S} step' P2 C2 |
|
77 {post C1 \<squnion> post C2}" |
|
78 by(simp add: step'_def Step.Step.simps) |
|
79 lemma [code,simp]: "step' S ({I} WHILE b DO {P} C {Q}) = |
|
80 {S \<squnion> post C} WHILE b DO {I} step' P C {I}" |
|
81 by(simp add: step'_def Step.Step.simps) |
72 |
82 |
73 definition AI :: "com \<Rightarrow> 'av st option acom option" where |
83 definition AI :: "com \<Rightarrow> 'av st option acom option" where |
74 "AI c = pfp (step' (Top(vars c))) (bot c)" |
84 "AI c = pfp (step' (Top(vars c))) (bot c)" |
75 |
85 |
76 |
86 |
93 next |
103 next |
94 case Seq thus ?case by auto |
104 case Seq thus ?case by auto |
95 next |
105 next |
96 case (If b p1 C1 p2 C2 P) |
106 case (If b p1 C1 p2 C2 P) |
97 hence "post C1 \<le> post C1 \<squnion> post C2 \<and> post C2 \<le> post C1 \<squnion> post C2" |
107 hence "post C1 \<le> post C1 \<squnion> post C2 \<and> post C2 \<le> post C1 \<squnion> post C2" |
98 by(simp, metis post_in_L join_ge1 join_ge2) |
108 by(simp, metis post_in_L sup_ge1 sup_ge2) |
99 thus ?case using If by (auto simp: mono_gamma_o) |
109 thus ?case using If by (auto simp: mono_gamma_o) |
100 next |
110 next |
101 case While thus ?case by (auto simp: mono_gamma_o) |
111 case While thus ?case by (auto simp: mono_gamma_o) |
102 qed |
112 qed |
103 |
113 |
131 end |
141 end |
132 |
142 |
133 |
143 |
134 subsubsection "Monotonicity" |
144 subsubsection "Monotonicity" |
135 |
145 |
136 lemma le_join_disj: "y \<in> L X \<Longrightarrow> (z::_::semilatticeL) \<in> L X \<Longrightarrow> |
146 lemma le_sup_disj: "y \<in> L X \<Longrightarrow> (z::_::semilatticeL) \<in> L X \<Longrightarrow> |
137 x \<le> y \<or> x \<le> z \<Longrightarrow> x \<le> y \<squnion> z" |
147 x \<le> y \<or> x \<le> z \<Longrightarrow> x \<le> y \<squnion> z" |
138 by (metis join_ge1 join_ge2 order_trans) |
148 by (metis sup_ge1 sup_ge2 order_trans) |
139 |
149 |
140 locale Abs_Int_mono = Abs_Int + |
150 locale Abs_Int_mono = Abs_Int + |
141 assumes mono_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> plus' a1 a2 \<le> plus' b1 b2" |
151 assumes mono_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> plus' a1 a2 \<le> plus' b1 b2" |
142 begin |
152 begin |
143 |
153 |
147 |
157 |
148 theorem mono_step': "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow> |
158 theorem mono_step': "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow> |
149 S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> step' S1 C1 \<le> step' S2 C2" |
159 S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> step' S1 C1 \<le> step' S2 C2" |
150 apply(induction C1 C2 arbitrary: S1 S2 rule: less_eq_acom.induct) |
160 apply(induction C1 C2 arbitrary: S1 S2 rule: less_eq_acom.induct) |
151 apply (auto simp: Let_def mono_aval' mono_post |
161 apply (auto simp: Let_def mono_aval' mono_post |
152 le_join_disj le_join_disj[OF post_in_L post_in_L] |
162 le_sup_disj le_sup_disj[OF post_in_L post_in_L] |
153 split: option.split) |
163 split: option.split) |
154 done |
164 done |
155 |
165 |
156 lemma mono_step'_top: "C \<in> L X \<Longrightarrow> C' \<in> L X \<Longrightarrow> |
166 lemma mono_step'_top: "C \<in> L X \<Longrightarrow> C' \<in> L X \<Longrightarrow> |
157 C \<le> C' \<Longrightarrow> step' (Top X) C \<le> step' (Top X) C'" |
167 C \<le> C' \<Longrightarrow> step' (Top X) C \<le> step' (Top X) C'" |