# File EvenOdd.ML

    (*  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";