src/HOL/HOLCF/IMP/HoareEx.thy
 author blanchet Tue Nov 07 15:16:42 2017 +0100 (21 months ago) changeset 67022 49309fe530fd parent 63549 b0d31c7def86 child 67443 3abf6a722518 permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
```     1 (*  Title:      HOL/HOLCF/IMP/HoareEx.thy
```
```     2     Author:     Tobias Nipkow, TUM
```
```     3     Copyright   1997 TUM
```
```     4 *)
```
```     5
```
```     6 section "Correctness of Hoare by Fixpoint Reasoning"
```
```     7
```
```     8 theory HoareEx imports Denotational begin
```
```     9
```
```    10 text \<open>
```
```    11   An example from the HOLCF paper by Mueller, Nipkow, Oheimb, Slotosch
```
```    12   @{cite MuellerNvOS99}.  It demonstrates fixpoint reasoning by showing
```
```    13   the correctness of the Hoare rule for while-loops.
```
```    14 \<close>
```
```    15
```
```    16 type_synonym assn = "state \<Rightarrow> bool"
```
```    17
```
```    18 definition
```
```    19   hoare_valid :: "[assn, com, assn] \<Rightarrow> bool"  ("|= {(1_)}/ (_)/ {(1_)}" 50) where
```
```    20   "|= {P} c {Q} = (\<forall>s t. P s \<and> D c\<cdot>(Discr s) = Def t \<longrightarrow> Q t)"
```
```    21
```
```    22 lemma WHILE_rule_sound:
```
```    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)
```
```    25   apply (simp (no_asm))
```
```    26   apply (rule fix_ind)
```
```    27     apply (simp (no_asm)) \<comment> "simplifier with enhanced \<open>adm\<close>-tactic"
```
```    28    apply (simp (no_asm))
```
```    29   apply (simp (no_asm))
```
```    30   apply blast
```
```    31   done
```
```    32
```
```    33 end
```