1(*  Title:      HOL/IMPP/EvenOdd.thy
2    Author:     David von Oheimb, TUM
3*)
4
5section \<open>Example of mutually recursive procedures verified with Hoare logic\<close>
6
7theory EvenOdd
8imports Main Misc
9begin
10
11axiomatization
12  Even :: pname and
13  Odd :: pname
14where
15  Even_neq_Odd: "Even ~= Odd" and
16  Arg_neq_Res:  "Arg  ~= Res"
17
18definition
19  evn :: com where
20 "evn = (IF (%s. s<Arg> = 0)
21         THEN Loc Res:==(%s. 0)
22         ELSE(Loc Res:=CALL Odd(%s. s<Arg> - 1);;
23              Loc Arg:=CALL Odd(%s. s<Arg> - 1);;
24              Loc Res:==(%s. s<Res> * s<Arg>)))"
25
26definition
27  odd :: com where
28 "odd = (IF (%s. s<Arg> = 0)
29         THEN Loc Res:==(%s. 1)
30         ELSE(Loc Res:=CALL Even (%s. s<Arg> - 1)))"
31
32overloading bodies \<equiv> bodies
33begin
34  definition "bodies == [(Even,evn),(Odd,odd)]"
35end
36
37definition
38  Z_eq_Arg_plus :: "nat => nat assn" ("Z=Arg+_" [50]50) where
39  "Z=Arg+n = (%Z s.      Z =  s<Arg>+n)"
40
41definition
42  Res_ok :: "nat assn" where
43  "Res_ok = (%Z s. even Z = (s<Res> = 0))"
44
45
46subsection "Arg, Res"
47
48declare Arg_neq_Res [simp] Arg_neq_Res [THEN not_sym, simp]
49declare Even_neq_Odd [simp] Even_neq_Odd [THEN not_sym, simp]
50
51lemma Z_eq_Arg_plus_def2: "(Z=Arg+n) Z s = (Z = s<Arg>+n)"
52apply (unfold Z_eq_Arg_plus_def)
53apply (rule refl)
54done
55
56lemma Res_ok_def2: "Res_ok Z s = (even Z = (s<Res> = 0))"
57apply (unfold Res_ok_def)
58apply (rule refl)
59done
60
61lemmas Arg_Res_simps = Z_eq_Arg_plus_def2 Res_ok_def2
62
63lemma body_Odd [simp]: "body Odd = Some odd"
64apply (unfold body_def bodies_def)
65apply auto
66done
67
68lemma body_Even [simp]: "body Even = Some evn"
69apply (unfold body_def bodies_def)
70apply auto
71done
72
73
74subsection "verification"
75
76lemma Odd_lemma: "{{Z=Arg+0}. BODY Even .{Res_ok}}|-{Z=Arg+Suc 0}. odd .{Res_ok}"
77apply (unfold odd_def)
78apply (rule hoare_derivs.If)
79apply (rule hoare_derivs.Ass [THEN conseq1])
80apply  (clarsimp simp: Arg_Res_simps)
81apply (rule export_s)
82apply (rule hoare_derivs.Call [THEN conseq1])
83apply  (rule_tac P = "Z=Arg+Suc (Suc 0) " in conseq12)
84apply (rule single_asm)
85apply (auto simp: Arg_Res_simps)
86done
87
88lemma Even_lemma: "{{Z=Arg+1}. BODY Odd .{Res_ok}}|-{Z=Arg+0}. evn .{Res_ok}"
89apply (unfold evn_def)
90apply (rule hoare_derivs.If)
91apply (rule hoare_derivs.Ass [THEN conseq1])
92apply  (clarsimp simp: Arg_Res_simps)
93apply (rule hoare_derivs.Comp)
94apply (rule_tac [2] hoare_derivs.Ass)
95apply clarsimp
96apply (rule_tac Q = "%Z s. P Z s & Res_ok Z s" and P = P for P in hoare_derivs.Comp)
97apply (rule export_s)
98apply  (rule_tac I1 = "%Z l. Z = l Arg & 0 < Z" and Q1 = "Res_ok" in Call_invariant [THEN conseq12])
99apply (rule single_asm [THEN conseq2])
100apply   (clarsimp simp: Arg_Res_simps)
101apply  (force simp: Arg_Res_simps)
102apply (rule export_s)
103apply (rule_tac I1 = "%Z l. even Z = (l Res = 0) " and Q1 = "%Z s. even Z = (s<Arg> = 0) " in Call_invariant [THEN conseq12])
104apply (rule single_asm [THEN conseq2])
105apply  (clarsimp simp: Arg_Res_simps)
106apply (force simp: Arg_Res_simps)
107done
108
109
110lemma Even_ok_N: "{}|-{Z=Arg+0}. BODY Even .{Res_ok}"
111apply (rule BodyN)
112apply (simp (no_asm))
113apply (rule Even_lemma [THEN hoare_derivs.cut])
114apply (rule BodyN)
115apply (simp (no_asm))
116apply (rule Odd_lemma [THEN thin])
117apply (simp (no_asm))
118done
119
120lemma Even_ok_S: "{}|-{Z=Arg+0}. BODY Even .{Res_ok}"
121apply (rule conseq1)
122apply  (rule_tac Procs = "{Odd, Even}" and pn = "Even" and P = "%pn. Z=Arg+ (if pn = Odd then 1 else 0) " and Q = "%pn. Res_ok" in Body1)
123apply    auto
124apply (rule hoare_derivs.insert)
125apply (rule Odd_lemma [THEN thin])
126apply  (simp (no_asm))
127apply (rule Even_lemma [THEN thin])
128apply (simp (no_asm))
129done
130
131end
132