equal
deleted
inserted
replaced
27 |
27 |
28 (* Hoare Rules *) |
28 (* Hoare Rules *) |
29 |
29 |
30 (* halting case *) |
30 (* halting case *) |
31 definition |
31 definition |
32 Hoare_halt :: "assert \<Rightarrow> tprog0 \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" [50, 49] 50) |
32 Hoare_halt :: "assert \<Rightarrow> tprog0 \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" 50) |
33 where |
33 where |
34 "{P} p {Q} \<equiv> \<forall>tp. P tp \<longrightarrow> (\<exists>n. is_final (steps0 (1, tp) p n) \<and> Q holds_for (steps0 (1, tp) p n))" |
34 "{P} p {Q} \<equiv> \<forall>tp. P tp \<longrightarrow> (\<exists>n. is_final (steps0 (1, tp) p n) \<and> Q holds_for (steps0 (1, tp) p n))" |
|
35 |
35 |
36 |
36 (* not halting case *) |
37 (* not halting case *) |
37 definition |
38 definition |
38 Hoare_unhalt :: "assert \<Rightarrow> tprog0 \<Rightarrow> bool" ("({(1_)}/ (_)) \<up>" [50, 49] 50) |
39 Hoare_unhalt :: "assert \<Rightarrow> tprog0 \<Rightarrow> bool" ("({(1_)}/ (_)) \<up>" [50, 49] 50) |
39 where |
40 where |