src/HOL/IMPP/EvenOdd.ML

clarified syntax of ``long'' statements: fixes/assumes/shows;

(*  Title:      HOL/IMPP/EvenOdd.ML
    ID:         $Id$
    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";