|
9243
|
1 |
(* Title: HOL/IMP/Examples.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: David von Oheimb, TUM
|
|
|
4 |
Copyright 2000 TUM
|
|
|
5 |
*)
|
|
|
6 |
|
|
12431
|
7 |
header "Examples"
|
|
|
8 |
|
|
16417
|
9 |
theory Examples imports Natural begin
|
|
12431
|
10 |
|
|
|
11 |
constdefs
|
|
|
12 |
factorial :: "loc => loc => com"
|
|
|
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"
|
|
9243
|
20 |
|
|
12431
|
21 |
lemma lemma1 [rule_format (no_asm)]:
|
|
|
22 |
"[| !x. P x \<longrightarrow> Q x; \<langle>w,s\<rangle> \<longrightarrow>\<^sub>c t |] ==>
|
|
|
23 |
!c. 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"
|
|
|
24 |
apply (erule evalc.induct)
|
|
|
25 |
apply auto
|
|
|
26 |
done
|
|
|
27 |
|
|
9243
|
28 |
|
|
12431
|
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 |
|
|
|
40 |
lemma Hoare_example: "!x. P x \<longrightarrow> Q x ==>
|
|
|
41 |
(\<langle>While P c; While Q c, s\<rangle> \<longrightarrow>\<^sub>c t) = (\<langle>While Q c, s\<rangle> \<longrightarrow>\<^sub>c t)"
|
|
|
42 |
by (blast intro: lemma1 lemma2 dest: semi [THEN iffD1])
|
|
|
43 |
|
|
9243
|
44 |
|
|
12431
|
45 |
subsection "Factorial"
|
|
|
46 |
|
|
|
47 |
lemma factorial_3: "a~=b ==>
|
|
|
48 |
\<langle>factorial a b, Mem(a:=3)\<rangle> \<longrightarrow>\<^sub>c Mem(b:=6, a:=0)"
|
|
|
49 |
apply (unfold factorial_def)
|
|
|
50 |
apply simp
|
|
|
51 |
done
|
|
|
52 |
|
|
|
53 |
text {* the same in single step mode: *}
|
|
|
54 |
lemmas [simp del] = evalc_cases
|
|
|
55 |
lemma "a~=b \<Longrightarrow> \<langle>factorial a b, Mem(a:=3)\<rangle> \<longrightarrow>\<^sub>c Mem(b:=6, a:=0)"
|
|
|
56 |
apply (unfold factorial_def)
|
|
|
57 |
apply (frule not_sym)
|
|
|
58 |
apply (rule evalc.intros)
|
|
|
59 |
apply (rule evalc.intros)
|
|
|
60 |
apply simp
|
|
|
61 |
apply (rule evalc.intros)
|
|
|
62 |
apply simp
|
|
|
63 |
apply (rule evalc.intros)
|
|
|
64 |
apply (rule evalc.intros)
|
|
|
65 |
apply simp
|
|
|
66 |
apply (rule evalc.intros)
|
|
|
67 |
apply simp
|
|
|
68 |
apply (rule evalc.intros)
|
|
|
69 |
apply simp
|
|
|
70 |
apply (rule evalc.intros)
|
|
|
71 |
apply (rule evalc.intros)
|
|
|
72 |
apply simp
|
|
|
73 |
apply (rule evalc.intros)
|
|
|
74 |
apply simp
|
|
|
75 |
apply (rule evalc.intros)
|
|
|
76 |
apply simp
|
|
|
77 |
apply (rule evalc.intros)
|
|
|
78 |
apply (rule evalc.intros)
|
|
|
79 |
apply simp
|
|
|
80 |
apply (rule evalc.intros)
|
|
|
81 |
apply simp
|
|
|
82 |
apply (rule evalc.intros)
|
|
|
83 |
apply simp
|
|
|
84 |
done
|
|
9243
|
85 |
|
|
|
86 |
end
|