(* Title: HOL/IMPP/EvenOdd.ML ID: $Id: EvenOdd.ML,v 1.9 2005/09/17 18:14:30 wenzelm Exp $ Author: David von Oheimb Copyright 1999 TUM *) section "even"; Goalw [even_def] "even 0"; by (Simp_tac 1); qed "even_0"; Addsimps [even_0]; Goalw [even_def] "even (Suc 0) = False"; by (Simp_tac 1); qed "not_even_1"; Addsimps [not_even_1]; Goalw [even_def] "even (Suc (Suc n)) = even n"; by (subgoal_tac "Suc (Suc n) = n+2" 1); by (Simp_tac 2); by (etac ssubst 1); by (rtac dvd_reduce 1); qed "even_step"; Addsimps[even_step]; section "Arg, Res"; Addsimps[Arg_neq_Res,Arg_neq_Res RS not_sym]; Addsimps[Even_neq_Odd, Even_neq_Odd RS not_sym]; Goalw [Z_eq_Arg_plus_def] "(Z=Arg+n) Z s = (Z = s<Arg>+n)"; by (rtac refl 1); qed "Z_eq_Arg_plus_def2"; Goalw [Res_ok_def] "Res_ok Z s = (even Z = (s<Res> = 0))"; by (rtac refl 1); qed "Res_ok_def2"; val Arg_Res_css = (claset(),simpset()addsimps[Z_eq_Arg_plus_def2,Res_ok_def2]); Goalw [body_def, bodies_def] "body Odd = Some odd"; by Auto_tac; qed "body_Odd"; Goalw [body_def, bodies_def] "body Even = Some evn"; by Auto_tac; qed "body_Even"; Addsimps[body_Odd, body_Even]; section "verification"; Goalw [odd_def] "{{Z=Arg+0}. BODY Even .{Res_ok}}|-{Z=Arg+Suc 0}. odd .{Res_ok}"; by (rtac hoare_derivs.If 1); by (rtac (hoare_derivs.Ass RS conseq1) 1); by (clarsimp_tac Arg_Res_css 1); by (rtac export_s 1); by (rtac (hoare_derivs.Call RS conseq1) 1); by (res_inst_tac [("P","Z=Arg+Suc (Suc 0)")] conseq12 1); by (rtac single_asm 1); by (auto_tac Arg_Res_css); qed "Odd_lemma"; Goalw [evn_def] "{{Z=Arg+1}. BODY Odd .{Res_ok}}|-{Z=Arg+0}. evn .{Res_ok}"; by (rtac hoare_derivs.If 1); by (rtac (hoare_derivs.Ass RS conseq1) 1); by (clarsimp_tac Arg_Res_css 1); by (rtac hoare_derivs.Comp 1); by (rtac hoare_derivs.Ass 2); by (Clarsimp_tac 1); by (res_inst_tac [("Q","%Z s. ?P Z s & Res_ok Z s")] hoare_derivs.Comp 1); by (rtac export_s 1); by (res_inst_tac [("I1","%Z l. Z = l Arg & 0 < Z"), ("Q1","Res_ok")] (Call_invariant RS conseq12) 1); by (rtac (single_asm RS conseq2) 1); by (clarsimp_tac Arg_Res_css 1); by (force_tac Arg_Res_css 1); by (rtac export_s 1); by (res_inst_tac [("I1","%Z l. even Z = (l Res = 0)"), ("Q1","%Z s. even Z = (s<Arg> = 0)")] (Call_invariant RS conseq12) 1); by (rtac (single_asm RS conseq2) 1); by (clarsimp_tac Arg_Res_css 1); by (force_tac Arg_Res_css 1); qed "Even_lemma"; Goal "{}|-{Z=Arg+0}. BODY Even .{Res_ok}"; by (rtac BodyN 1); by (Simp_tac 1); by (rtac (Even_lemma RS hoare_derivs.cut) 1); by (rtac BodyN 1); by (Simp_tac 1); by (rtac (Odd_lemma RS thin) 1); by (Simp_tac 1); qed "Even_ok_N"; Goal "{}|-{Z=Arg+0}. BODY Even .{Res_ok}"; by (rtac conseq1 1); by (res_inst_tac [("Procs","{Odd, Even}"), ("pn","Even"), ("P","%pn. Z=Arg+(if pn = Odd then 1 else 0)"), ("Q","%pn. Res_ok")] Body1 1); by Auto_tac; by (rtac hoare_derivs.insert 1); by (rtac (Odd_lemma RS thin) 1); by (Simp_tac 1); by (rtac (Even_lemma RS thin) 1); by (Simp_tac 1); qed "Even_ok_S";