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