equal
deleted
inserted
replaced
2 Author: Leonor Prensa Nieto & Tobias Nipkow |
2 Author: Leonor Prensa Nieto & Tobias Nipkow |
3 Copyright 1998 TUM |
3 Copyright 1998 TUM |
4 Author: Walter Guttmann (extension to total-correctness proofs) |
4 Author: Walter Guttmann (extension to total-correctness proofs) |
5 *) |
5 *) |
6 |
6 |
7 section \<open>Sugared semantic embedding of Hoare logic\<close> |
7 section \<open>Hoare logic\<close> |
|
8 |
|
9 theory Hoare_Logic |
|
10 imports Hoare_Syntax Hoare_Tac |
|
11 begin |
|
12 |
|
13 subsection \<open>Sugared semantic embedding of Hoare logic\<close> |
8 |
14 |
9 text \<open> |
15 text \<open> |
10 Strictly speaking a shallow embedding (as implemented by Norbert Galm |
16 Strictly speaking a shallow embedding (as implemented by Norbert Galm |
11 following Mike Gordon) would suffice. Maybe the datatype com comes in useful |
17 following Mike Gordon) would suffice. Maybe the datatype com comes in useful |
12 later. |
18 later. |
13 \<close> |
19 \<close> |
14 |
|
15 theory Hoare_Logic |
|
16 imports Hoare_Syntax Hoare_Tac |
|
17 begin |
|
18 |
20 |
19 type_synonym 'a bexp = "'a set" |
21 type_synonym 'a bexp = "'a set" |
20 type_synonym 'a assn = "'a set" |
22 type_synonym 'a assn = "'a set" |
21 type_synonym 'a var = "'a \<Rightarrow> nat" |
23 type_synonym 'a var = "'a \<Rightarrow> nat" |
22 |
24 |
165 thus ?thesis |
167 thus ?thesis |
166 using assms(1) ValidTC_def by force |
168 using assms(1) ValidTC_def by force |
167 qed |
169 qed |
168 |
170 |
169 |
171 |
170 subsection \<open>Concrete syntax\<close> |
172 subsubsection \<open>Concrete syntax\<close> |
171 |
173 |
172 setup \<open> |
174 setup \<open> |
173 Hoare_Syntax.setup |
175 Hoare_Syntax.setup |
174 {Basic = \<^const_syntax>\<open>Basic\<close>, |
176 {Basic = \<^const_syntax>\<open>Basic\<close>, |
175 Skip = \<^const_syntax>\<open>annskip\<close>, |
177 Skip = \<^const_syntax>\<open>annskip\<close>, |
179 Valid = \<^const_syntax>\<open>Valid\<close>, |
181 Valid = \<^const_syntax>\<open>Valid\<close>, |
180 ValidTC = \<^const_syntax>\<open>ValidTC\<close>} |
182 ValidTC = \<^const_syntax>\<open>ValidTC\<close>} |
181 \<close> |
183 \<close> |
182 |
184 |
183 |
185 |
184 subsection \<open>Proof methods: VCG\<close> |
186 subsubsection \<open>Proof methods: VCG\<close> |
185 |
187 |
186 declare BasicRule [Hoare_Tac.BasicRule] |
188 declare BasicRule [Hoare_Tac.BasicRule] |
187 and SkipRule [Hoare_Tac.SkipRule] |
189 and SkipRule [Hoare_Tac.SkipRule] |
188 and SeqRule [Hoare_Tac.SeqRule] |
190 and SeqRule [Hoare_Tac.SeqRule] |
189 and CondRule [Hoare_Tac.CondRule] |
191 and CondRule [Hoare_Tac.CondRule] |