src/HOL/IMPP/EvenOdd.thy
author wenzelm
Mon Jan 11 21:21:02 2016 +0100 (2016-01-11)
changeset 62145 5b946c81dfbf
parent 59807 22bc39064290
child 63167 0909deb8059b
permissions -rw-r--r--
eliminated old defs;
     1 (*  Title:      HOL/IMPP/EvenOdd.thy
     2     Author:     David von Oheimb, TUM
     3 *)
     4 
     5 section {* Example of mutually recursive procedures verified with Hoare logic *}
     6 
     7 theory EvenOdd
     8 imports Main Misc
     9 begin
    10 
    11 axiomatization
    12   Even :: pname and
    13   Odd :: pname
    14 where
    15   Even_neq_Odd: "Even ~= Odd" and
    16   Arg_neq_Res:  "Arg  ~= Res"
    17 
    18 definition
    19   evn :: com where
    20  "evn = (IF (%s. s<Arg> = 0)
    21          THEN Loc Res:==(%s. 0)
    22          ELSE(Loc Res:=CALL Odd(%s. s<Arg> - 1);;
    23               Loc Arg:=CALL Odd(%s. s<Arg> - 1);;
    24               Loc Res:==(%s. s<Res> * s<Arg>)))"
    25 
    26 definition
    27   odd :: com where
    28  "odd = (IF (%s. s<Arg> = 0)
    29          THEN Loc Res:==(%s. 1)
    30          ELSE(Loc Res:=CALL Even (%s. s<Arg> - 1)))"
    31 
    32 overloading bodies \<equiv> bodies
    33 begin
    34   definition "bodies == [(Even,evn),(Odd,odd)]"
    35 end
    36 
    37 definition
    38   Z_eq_Arg_plus :: "nat => nat assn" ("Z=Arg+_" [50]50) where
    39   "Z=Arg+n = (%Z s.      Z =  s<Arg>+n)"
    40 
    41 definition
    42   Res_ok :: "nat assn" where
    43   "Res_ok = (%Z s. even Z = (s<Res> = 0))"
    44 
    45 
    46 subsection "Arg, Res"
    47 
    48 declare Arg_neq_Res [simp] Arg_neq_Res [THEN not_sym, simp]
    49 declare Even_neq_Odd [simp] Even_neq_Odd [THEN not_sym, simp]
    50 
    51 lemma Z_eq_Arg_plus_def2: "(Z=Arg+n) Z s = (Z = s<Arg>+n)"
    52 apply (unfold Z_eq_Arg_plus_def)
    53 apply (rule refl)
    54 done
    55 
    56 lemma Res_ok_def2: "Res_ok Z s = (even Z = (s<Res> = 0))"
    57 apply (unfold Res_ok_def)
    58 apply (rule refl)
    59 done
    60 
    61 lemmas Arg_Res_simps = Z_eq_Arg_plus_def2 Res_ok_def2
    62 
    63 lemma body_Odd [simp]: "body Odd = Some odd"
    64 apply (unfold body_def bodies_def)
    65 apply auto
    66 done
    67 
    68 lemma body_Even [simp]: "body Even = Some evn"
    69 apply (unfold body_def bodies_def)
    70 apply auto
    71 done
    72 
    73 
    74 subsection "verification"
    75 
    76 lemma Odd_lemma: "{{Z=Arg+0}. BODY Even .{Res_ok}}|-{Z=Arg+Suc 0}. odd .{Res_ok}"
    77 apply (unfold odd_def)
    78 apply (rule hoare_derivs.If)
    79 apply (rule hoare_derivs.Ass [THEN conseq1])
    80 apply  (clarsimp simp: Arg_Res_simps)
    81 apply (rule export_s)
    82 apply (rule hoare_derivs.Call [THEN conseq1])
    83 apply  (rule_tac P = "Z=Arg+Suc (Suc 0) " in conseq12)
    84 apply (rule single_asm)
    85 apply (auto simp: Arg_Res_simps)
    86 done
    87 
    88 lemma Even_lemma: "{{Z=Arg+1}. BODY Odd .{Res_ok}}|-{Z=Arg+0}. evn .{Res_ok}"
    89 apply (unfold evn_def)
    90 apply (rule hoare_derivs.If)
    91 apply (rule hoare_derivs.Ass [THEN conseq1])
    92 apply  (clarsimp simp: Arg_Res_simps)
    93 apply (rule hoare_derivs.Comp)
    94 apply (rule_tac [2] hoare_derivs.Ass)
    95 apply clarsimp
    96 apply (rule_tac Q = "%Z s. P Z s & Res_ok Z s" and P = P for P in hoare_derivs.Comp)
    97 apply (rule export_s)
    98 apply  (rule_tac I1 = "%Z l. Z = l Arg & 0 < Z" and Q1 = "Res_ok" in Call_invariant [THEN conseq12])
    99 apply (rule single_asm [THEN conseq2])
   100 apply   (clarsimp simp: Arg_Res_simps)
   101 apply  (force simp: Arg_Res_simps)
   102 apply (rule export_s)
   103 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])
   104 apply (rule single_asm [THEN conseq2])
   105 apply  (clarsimp simp: Arg_Res_simps)
   106 apply (force simp: Arg_Res_simps)
   107 done
   108 
   109 
   110 lemma Even_ok_N: "{}|-{Z=Arg+0}. BODY Even .{Res_ok}"
   111 apply (rule BodyN)
   112 apply (simp (no_asm))
   113 apply (rule Even_lemma [THEN hoare_derivs.cut])
   114 apply (rule BodyN)
   115 apply (simp (no_asm))
   116 apply (rule Odd_lemma [THEN thin])
   117 apply (simp (no_asm))
   118 done
   119 
   120 lemma Even_ok_S: "{}|-{Z=Arg+0}. BODY Even .{Res_ok}"
   121 apply (rule conseq1)
   122 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)
   123 apply    auto
   124 apply (rule hoare_derivs.insert)
   125 apply (rule Odd_lemma [THEN thin])
   126 apply  (simp (no_asm))
   127 apply (rule Even_lemma [THEN thin])
   128 apply (simp (no_asm))
   129 done
   130 
   131 end