src/HOL/IMP/Examples.thy
 author nipkow Fri Aug 28 18:52:41 2009 +0200 (2009-08-28) changeset 32436 10cd49e0c067 parent 27362 a6dc1769fdda child 41589 bbd861837ebc permissions -rw-r--r--
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
```     1 (*  Title:      HOL/IMP/Examples.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     David von Oheimb, TUM
```
```     4     Copyright   2000 TUM
```
```     5 *)
```
```     6
```
```     7 header "Examples"
```
```     8
```
```     9 theory Examples imports Natural begin
```
```    10
```
```    11 definition
```
```    12   factorial :: "loc => loc => com" where
```
```    13   "factorial a b = (b :== (%s. 1);
```
```    14                     \<WHILE> (%s. s a ~= 0) \<DO>
```
```    15                     (b :== (%s. s b * s a); a :== (%s. s a - 1)))"
```
```    16
```
```    17 declare update_def [simp]
```
```    18
```
```    19 subsection "An example due to Tony Hoare"
```
```    20
```
```    21 lemma lemma1:
```
```    22   assumes 1: "!x. P x \<longrightarrow> Q x"
```
```    23     and 2: "\<langle>w,s\<rangle> \<longrightarrow>\<^sub>c t"
```
```    24   shows "w = While P c \<Longrightarrow> \<langle>While Q c,t\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> \<langle>While Q c,s\<rangle> \<longrightarrow>\<^sub>c u"
```
```    25   using 2 apply induct
```
```    26   using 1 apply auto
```
```    27   done
```
```    28
```
```    29 lemma lemma2 [rule_format (no_asm)]:
```
```    30   "[| !x. P x \<longrightarrow> Q x; \<langle>w,s\<rangle> \<longrightarrow>\<^sub>c u |] ==>
```
```    31   !c. w = While Q c \<longrightarrow> \<langle>While P c; While Q c,s\<rangle> \<longrightarrow>\<^sub>c u"
```
```    32 apply (erule evalc.induct)
```
```    33 apply (simp_all (no_asm_simp))
```
```    34 apply blast
```
```    35 apply (case_tac "P s")
```
```    36 apply auto
```
```    37 done
```
```    38
```
```    39 lemma Hoare_example: "!x. P x \<longrightarrow> Q x ==>
```
```    40   (\<langle>While P c; While Q c, s\<rangle> \<longrightarrow>\<^sub>c t) = (\<langle>While Q c, s\<rangle> \<longrightarrow>\<^sub>c t)"
```
```    41   by (blast intro: lemma1 lemma2 dest: semi [THEN iffD1])
```
```    42
```
```    43
```
```    44 subsection "Factorial"
```
```    45
```
```    46 lemma factorial_3: "a~=b ==>
```
```    47     \<langle>factorial a b, Mem(a:=3)\<rangle> \<longrightarrow>\<^sub>c Mem(b:=6, a:=0)"
```
```    48   by (simp add: factorial_def)
```
```    49
```
```    50 text {* the same in single step mode: *}
```
```    51 lemmas [simp del] = evalc_cases
```
```    52 lemma  "a~=b \<Longrightarrow> \<langle>factorial a b, Mem(a:=3)\<rangle> \<longrightarrow>\<^sub>c Mem(b:=6, a:=0)"
```
```    53 apply (unfold factorial_def)
```
```    54 apply (frule not_sym)
```
```    55 apply (rule evalc.intros)
```
```    56 apply  (rule evalc.intros)
```
```    57 apply simp
```
```    58 apply (rule evalc.intros)
```
```    59 apply   simp
```
```    60 apply  (rule evalc.intros)
```
```    61 apply   (rule evalc.intros)
```
```    62 apply  simp
```
```    63 apply  (rule evalc.intros)
```
```    64 apply simp
```
```    65 apply (rule evalc.intros)
```
```    66 apply   simp
```
```    67 apply  (rule evalc.intros)
```
```    68 apply   (rule evalc.intros)
```
```    69 apply  simp
```
```    70 apply  (rule evalc.intros)
```
```    71 apply simp
```
```    72 apply (rule evalc.intros)
```
```    73 apply   simp
```
```    74 apply  (rule evalc.intros)
```
```    75 apply   (rule evalc.intros)
```
```    76 apply  simp
```
```    77 apply  (rule evalc.intros)
```
```    78 apply simp
```
```    79 apply (rule evalc.intros)
```
```    80 apply simp
```
```    81 done
```
```    82
```
```    83 end
```