equal
deleted
inserted
replaced
1 (* Author: Tobias Nipkow *) |
1 (* Author: Tobias Nipkow *) |
2 |
2 |
3 subsection "Hoare Logic for Total Correctness" |
3 subsection "Hoare Logic for Total Correctness" |
|
4 |
|
5 subsubsection "Separate Termination Relation" |
4 |
6 |
5 theory Hoare_Total |
7 theory Hoare_Total |
6 imports Hoare_Examples |
8 imports Hoare_Examples |
7 begin |
9 begin |
8 |
|
9 subsubsection "Hoare Logic for Total Correctness --- Separate Termination Relation" |
|
10 |
10 |
11 text\<open>Note that this definition of total validity @{text"\<Turnstile>\<^sub>t"} only |
11 text\<open>Note that this definition of total validity @{text"\<Turnstile>\<^sub>t"} only |
12 works if execution is deterministic (which it is in our case).\<close> |
12 works if execution is deterministic (which it is in our case).\<close> |
13 |
13 |
14 definition hoare_tvalid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" |
14 definition hoare_tvalid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" |