src/HOL/IMPP/EvenOdd.ML
author wenzelm
Sat, 17 Sep 2005 20:14:30 +0200
changeset 17477 ceb42ea2f223
parent 15354 9234f5765d9c
permissions -rw-r--r--
converted to Isar theory format;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     1
(*  Title:      HOL/IMPP/EvenOdd.ML
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     2
    ID:         $Id$
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     3
    Author:     David von Oheimb
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     4
    Copyright   1999 TUM
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     5
*)
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     6
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 15354
diff changeset
     7
section "even";
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     8
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     9
Goalw [even_def] "even 0";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    10
by (Simp_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    11
qed "even_0";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    12
Addsimps [even_0];
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    13
11701
3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents: 11464
diff changeset
    14
Goalw [even_def] "even (Suc 0) = False";
11364
01020b10c0a7 simplified a proof using new dvd rules
paulson
parents: 10962
diff changeset
    15
by (Simp_tac 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    16
qed "not_even_1";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    17
Addsimps [not_even_1];
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    18
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    19
Goalw [even_def] "even (Suc (Suc n)) = even n";
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
    20
by (subgoal_tac "Suc (Suc n) = n+2" 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    21
by  (Simp_tac 2);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8791
diff changeset
    22
by (etac ssubst 1);
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8791
diff changeset
    23
by (rtac dvd_reduce 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    24
qed "even_step";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    25
Addsimps[even_step];
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    26
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    27
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    28
section "Arg, Res";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    29
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    30
Addsimps[Arg_neq_Res,Arg_neq_Res RS not_sym];
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    31
Addsimps[Even_neq_Odd, Even_neq_Odd RS not_sym];
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    32
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    33
Goalw [Z_eq_Arg_plus_def] "(Z=Arg+n) Z s = (Z = s<Arg>+n)";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8791
diff changeset
    34
by (rtac refl 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    35
qed "Z_eq_Arg_plus_def2";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    36
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    37
Goalw [Res_ok_def] "Res_ok Z s = (even Z = (s<Res> = 0))";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8791
diff changeset
    38
by (rtac refl 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    39
qed "Res_ok_def2";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    40
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    41
val Arg_Res_css = (claset(),simpset()addsimps[Z_eq_Arg_plus_def2,Res_ok_def2]);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    42
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    43
Goalw [body_def, bodies_def] "body Odd = Some odd";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    44
by Auto_tac;
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    45
qed "body_Odd";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    46
Goalw [body_def, bodies_def] "body Even = Some evn";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    47
by Auto_tac;
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    48
qed "body_Even";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    49
Addsimps[body_Odd, body_Even];
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    50
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    51
section "verification";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    52
11701
3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents: 11464
diff changeset
    53
Goalw [odd_def] "{{Z=Arg+0}. BODY Even .{Res_ok}}|-{Z=Arg+Suc 0}. odd .{Res_ok}";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8791
diff changeset
    54
by (rtac hoare_derivs.If 1);
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8791
diff changeset
    55
by (rtac (hoare_derivs.Ass RS conseq1) 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    56
by  (clarsimp_tac Arg_Res_css 1);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8791
diff changeset
    57
by (rtac export_s 1);
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8791
diff changeset
    58
by (rtac (hoare_derivs.Call RS conseq1) 1);
11701
3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents: 11464
diff changeset
    59
by  (res_inst_tac [("P","Z=Arg+Suc (Suc 0)")] conseq12 1);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8791
diff changeset
    60
by (rtac single_asm 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    61
by (auto_tac Arg_Res_css);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    62
qed "Odd_lemma";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    63
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    64
Goalw [evn_def] "{{Z=Arg+1}. BODY Odd .{Res_ok}}|-{Z=Arg+0}. evn .{Res_ok}";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8791
diff changeset
    65
by (rtac hoare_derivs.If 1);
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8791
diff changeset
    66
by (rtac (hoare_derivs.Ass RS conseq1) 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    67
by  (clarsimp_tac Arg_Res_css 1);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8791
diff changeset
    68
by (rtac hoare_derivs.Comp 1);
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8791
diff changeset
    69
by (rtac hoare_derivs.Ass 2);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    70
by (Clarsimp_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    71
by (res_inst_tac [("Q","%Z s. ?P Z s & Res_ok Z s")] hoare_derivs.Comp 1);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8791
diff changeset
    72
by (rtac export_s 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    73
by  (res_inst_tac [("I1","%Z l. Z = l Arg & 0 < Z"),
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 15354
diff changeset
    74
                   ("Q1","Res_ok")] (Call_invariant RS conseq12) 1);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8791
diff changeset
    75
by (rtac (single_asm RS conseq2) 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    76
by   (clarsimp_tac Arg_Res_css 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    77
by  (force_tac Arg_Res_css 1);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8791
diff changeset
    78
by (rtac export_s 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    79
by (res_inst_tac [("I1","%Z l. even Z = (l Res = 0)"),
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 15354
diff changeset
    80
                  ("Q1","%Z s. even Z = (s<Arg> = 0)")]
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 15354
diff changeset
    81
                 (Call_invariant RS conseq12) 1);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8791
diff changeset
    82
by (rtac (single_asm RS conseq2) 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    83
by  (clarsimp_tac Arg_Res_css 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    84
by (force_tac Arg_Res_css 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    85
qed "Even_lemma";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    86
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    87
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    88
Goal "{}|-{Z=Arg+0}. BODY Even .{Res_ok}";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8791
diff changeset
    89
by (rtac BodyN 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    90
by (Simp_tac 1);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8791
diff changeset
    91
by (rtac (Even_lemma RS hoare_derivs.cut) 1);
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8791
diff changeset
    92
by (rtac BodyN 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    93
by (Simp_tac 1);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8791
diff changeset
    94
by (rtac (Odd_lemma RS thin) 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    95
by (Simp_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    96
qed "Even_ok_N";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    97
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    98
Goal "{}|-{Z=Arg+0}. BODY Even .{Res_ok}";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8791
diff changeset
    99
by (rtac conseq1 1);
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 15354
diff changeset
   100
by  (res_inst_tac [("Procs","{Odd, Even}"), ("pn","Even"),
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   101
      ("P","%pn. Z=Arg+(if pn = Odd then 1 else 0)"),
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   102
      ("Q","%pn. Res_ok")] Body1 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   103
by    Auto_tac;
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8791
diff changeset
   104
by (rtac hoare_derivs.insert 1);
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8791
diff changeset
   105
by (rtac (Odd_lemma RS thin) 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   106
by  (Simp_tac 1);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8791
diff changeset
   107
by (rtac (Even_lemma RS thin) 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   108
by (Simp_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   109
qed "Even_ok_S";