src/HOL/IMPP/EvenOdd.thy
 author haftmann Fri Jan 02 08:12:46 2009 +0100 (2009-01-02) changeset 29332 edc1e2a56398 parent 27362 a6dc1769fdda child 41589 bbd861837ebc permissions -rw-r--r--
named code theorem for Fract_norm
```     1 (*  Title:      HOL/IMPP/EvenOdd.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     David von Oheimb
```
```     4     Copyright   1999 TUM
```
```     5 *)
```
```     6
```
```     7 header {* Example of mutually recursive procedures verified with Hoare logic *}
```
```     8
```
```     9 theory EvenOdd
```
```    10 imports Misc
```
```    11 begin
```
```    12
```
```    13 definition
```
```    14   even :: "nat => bool" where
```
```    15   "even n = (2 dvd n)"
```
```    16
```
```    17 axiomatization
```
```    18   Even :: pname and
```
```    19   Odd :: pname
```
```    20 where
```
```    21   Even_neq_Odd: "Even ~= Odd" and
```
```    22   Arg_neq_Res:  "Arg  ~= Res"
```
```    23
```
```    24 definition
```
```    25   evn :: com where
```
```    26  "evn = (IF (%s. s<Arg> = 0)
```
```    27          THEN Loc Res:==(%s. 0)
```
```    28          ELSE(Loc Res:=CALL Odd(%s. s<Arg> - 1);;
```
```    29               Loc Arg:=CALL Odd(%s. s<Arg> - 1);;
```
```    30               Loc Res:==(%s. s<Res> * s<Arg>)))"
```
```    31
```
```    32 definition
```
```    33   odd :: com where
```
```    34  "odd = (IF (%s. s<Arg> = 0)
```
```    35          THEN Loc Res:==(%s. 1)
```
```    36          ELSE(Loc Res:=CALL Even (%s. s<Arg> - 1)))"
```
```    37
```
```    38 defs
```
```    39   bodies_def: "bodies == [(Even,evn),(Odd,odd)]"
```
```    40
```
```    41 definition
```
```    42   Z_eq_Arg_plus :: "nat => nat assn" ("Z=Arg+_" [50]50) where
```
```    43   "Z=Arg+n = (%Z s.      Z =  s<Arg>+n)"
```
```    44
```
```    45 definition
```
```    46   Res_ok :: "nat assn" where
```
```    47   "Res_ok = (%Z s. even Z = (s<Res> = 0))"
```
```    48
```
```    49
```
```    50 subsection "even"
```
```    51
```
```    52 lemma even_0 [simp]: "even 0"
```
```    53 apply (unfold even_def)
```
```    54 apply simp
```
```    55 done
```
```    56
```
```    57 lemma not_even_1 [simp]: "even (Suc 0) = False"
```
```    58 apply (unfold even_def)
```
```    59 apply simp
```
```    60 done
```
```    61
```
```    62 lemma even_step [simp]: "even (Suc (Suc n)) = even n"
```
```    63 apply (unfold even_def)
```
```    64 apply (subgoal_tac "Suc (Suc n) = n+2")
```
```    65 prefer 2
```
```    66 apply  simp
```
```    67 apply (erule ssubst)
```
```    68 apply (rule dvd_reduce)
```
```    69 done
```
```    70
```
```    71
```
```    72 subsection "Arg, Res"
```
```    73
```
```    74 declare Arg_neq_Res [simp] Arg_neq_Res [THEN not_sym, simp]
```
```    75 declare Even_neq_Odd [simp] Even_neq_Odd [THEN not_sym, simp]
```
```    76
```
```    77 lemma Z_eq_Arg_plus_def2: "(Z=Arg+n) Z s = (Z = s<Arg>+n)"
```
```    78 apply (unfold Z_eq_Arg_plus_def)
```
```    79 apply (rule refl)
```
```    80 done
```
```    81
```
```    82 lemma Res_ok_def2: "Res_ok Z s = (even Z = (s<Res> = 0))"
```
```    83 apply (unfold Res_ok_def)
```
```    84 apply (rule refl)
```
```    85 done
```
```    86
```
```    87 lemmas Arg_Res_simps = Z_eq_Arg_plus_def2 Res_ok_def2
```
```    88
```
```    89 lemma body_Odd [simp]: "body Odd = Some odd"
```
```    90 apply (unfold body_def bodies_def)
```
```    91 apply auto
```
```    92 done
```
```    93
```
```    94 lemma body_Even [simp]: "body Even = Some evn"
```
```    95 apply (unfold body_def bodies_def)
```
```    96 apply auto
```
```    97 done
```
```    98
```
```    99
```
```   100 subsection "verification"
```
```   101
```
```   102 lemma Odd_lemma: "{{Z=Arg+0}. BODY Even .{Res_ok}}|-{Z=Arg+Suc 0}. odd .{Res_ok}"
```
```   103 apply (unfold odd_def)
```
```   104 apply (rule hoare_derivs.If)
```
```   105 apply (rule hoare_derivs.Ass [THEN conseq1])
```
```   106 apply  (clarsimp simp: Arg_Res_simps)
```
```   107 apply (rule export_s)
```
```   108 apply (rule hoare_derivs.Call [THEN conseq1])
```
```   109 apply  (rule_tac P = "Z=Arg+Suc (Suc 0) " in conseq12)
```
```   110 apply (rule single_asm)
```
```   111 apply (auto simp: Arg_Res_simps)
```
```   112 done
```
```   113
```
```   114 lemma Even_lemma: "{{Z=Arg+1}. BODY Odd .{Res_ok}}|-{Z=Arg+0}. evn .{Res_ok}"
```
```   115 apply (unfold evn_def)
```
```   116 apply (rule hoare_derivs.If)
```
```   117 apply (rule hoare_derivs.Ass [THEN conseq1])
```
```   118 apply  (clarsimp simp: Arg_Res_simps)
```
```   119 apply (rule hoare_derivs.Comp)
```
```   120 apply (rule_tac [2] hoare_derivs.Ass)
```
```   121 apply clarsimp
```
```   122 apply (rule_tac Q = "%Z s. ?P Z s & Res_ok Z s" in hoare_derivs.Comp)
```
```   123 apply (rule export_s)
```
```   124 apply  (rule_tac I1 = "%Z l. Z = l Arg & 0 < Z" and Q1 = "Res_ok" in Call_invariant [THEN conseq12])
```
```   125 apply (rule single_asm [THEN conseq2])
```
```   126 apply   (clarsimp simp: Arg_Res_simps)
```
```   127 apply  (force simp: Arg_Res_simps)
```
```   128 apply (rule export_s)
```
```   129 apply (rule_tac I1 = "%Z l. even Z = (l Res = 0) " and Q1 = "%Z s. even Z = (s<Arg> = 0) " in Call_invariant [THEN conseq12])
```
```   130 apply (rule single_asm [THEN conseq2])
```
```   131 apply  (clarsimp simp: Arg_Res_simps)
```
```   132 apply (force simp: Arg_Res_simps)
```
```   133 done
```
```   134
```
```   135
```
```   136 lemma Even_ok_N: "{}|-{Z=Arg+0}. BODY Even .{Res_ok}"
```
```   137 apply (rule BodyN)
```
```   138 apply (simp (no_asm))
```
```   139 apply (rule Even_lemma [THEN hoare_derivs.cut])
```
```   140 apply (rule BodyN)
```
```   141 apply (simp (no_asm))
```
```   142 apply (rule Odd_lemma [THEN thin])
```
```   143 apply (simp (no_asm))
```
```   144 done
```
```   145
```
```   146 lemma Even_ok_S: "{}|-{Z=Arg+0}. BODY Even .{Res_ok}"
```
```   147 apply (rule conseq1)
```
```   148 apply  (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)
```
```   149 apply    auto
```
```   150 apply (rule hoare_derivs.insert)
```
```   151 apply (rule Odd_lemma [THEN thin])
```
```   152 apply  (simp (no_asm))
```
```   153 apply (rule Even_lemma [THEN thin])
```
```   154 apply (simp (no_asm))
```
```   155 done
```
```   156
```
```   157 end
```