equal
deleted
inserted
replaced
14 \<close> |
14 \<close> |
15 |
15 |
16 type_synonym assn = "state \<Rightarrow> bool" |
16 type_synonym assn = "state \<Rightarrow> bool" |
17 |
17 |
18 definition |
18 definition |
19 hoare_valid :: "[assn, com, assn] \<Rightarrow> bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where |
19 hoare_valid :: "[assn, com, assn] \<Rightarrow> bool" (\<open>|= {(1_)}/ (_)/ {(1_)}\<close> 50) where |
20 "|= {P} c {Q} = (\<forall>s t. P s \<and> D c\<cdot>(Discr s) = Def t \<longrightarrow> Q t)" |
20 "|= {P} c {Q} = (\<forall>s t. P s \<and> D c\<cdot>(Discr s) = Def t \<longrightarrow> Q t)" |
21 |
21 |
22 lemma WHILE_rule_sound: |
22 lemma WHILE_rule_sound: |
23 "|= {A} c {A} \<Longrightarrow> |= {A} WHILE b DO c {\<lambda>s. A s \<and> \<not> bval b s}" |
23 "|= {A} c {A} \<Longrightarrow> |= {A} WHILE b DO c {\<lambda>s. A s \<and> \<not> bval b s}" |
24 apply (unfold hoare_valid_def) |
24 apply (unfold hoare_valid_def) |