1(* Title: HOL/IMPP/Hoare.thy 2 Author: David von Oheimb 3 Copyright 1999 TUM 4*) 5 6section \<open>Inductive definition of Hoare logic for partial correctness\<close> 7 8theory Hoare 9imports Natural 10begin 11 12text \<open> 13 Completeness is taken relative to completeness of the underlying logic. 14 15 Two versions of completeness proof: nested single recursion 16 vs. simultaneous recursion in call rule 17\<close> 18 19type_synonym 'a assn = "'a => state => bool" 20translations 21 (type) "'a assn" <= (type) "'a => state => bool" 22 23definition 24 state_not_singleton :: bool where 25 "state_not_singleton = (\<exists>s t::state. s ~= t)" (* at least two elements *) 26 27definition 28 peek_and :: "'a assn => (state => bool) => 'a assn" (infixr "&>" 35) where 29 "peek_and P p = (%Z s. P Z s & p s)" 30 31datatype 'a triple = 32 triple "'a assn" com "'a assn" ("{(1_)}./ (_)/ .{(1_)}" [3,60,3] 58) 33 34definition 35 triple_valid :: "nat => 'a triple => bool" ( "|=_:_" [0 , 58] 57) where 36 "|=n:t = (case t of {P}.c.{Q} => 37 \<forall>Z s. P Z s \<longrightarrow> (\<forall>s'. <c,s> -n-> s' \<longrightarrow> Q Z s'))" 38abbreviation 39 triples_valid :: "nat => 'a triple set => bool" ("||=_:_" [0 , 58] 57) where 40 "||=n:G == Ball G (triple_valid n)" 41 42definition 43 hoare_valids :: "'a triple set => 'a triple set => bool" ("_||=_" [58, 58] 57) where 44 "G||=ts = (\<forall>n. ||=n:G --> ||=n:ts)" 45abbreviation 46 hoare_valid :: "'a triple set => 'a triple => bool" ("_|=_" [58, 58] 57) where 47 "G |=t == G||={t}" 48 49(* Most General Triples *) 50definition 51 MGT :: "com => state triple" ("{=}._.{->}" [60] 58) where 52 "{=}.c.{->} = {%Z s0. Z = s0}. c .{%Z s1. <c,Z> -c-> s1}" 53 54inductive 55 hoare_derivs :: "'a triple set => 'a triple set => bool" ("_||-_" [58, 58] 57) and 56 hoare_deriv :: "'a triple set => 'a triple => bool" ("_|-_" [58, 58] 57) 57where 58 "G |-t == G||-{t}" 59 60| empty: "G||-{}" 61| insert: "[| G |-t; G||-ts |] 62 ==> G||-insert t ts" 63 64| asm: "ts <= G ==> 65 G||-ts" (* {P}.BODY pn.{Q} instead of (general) t for SkipD_lemma *) 66 67| cut: "[| G'||-ts; G||-G' |] ==> G||-ts" (* for convenience and efficiency *) 68 69| weaken: "[| G||-ts' ; ts <= ts' |] ==> G||-ts" 70 71| conseq: "\<forall>Z s. P Z s \<longrightarrow> (\<exists>P' Q'. G|-{P'}.c.{Q'} \<and> 72 (\<forall>s'. (\<forall>Z'. P' Z' s \<longrightarrow> Q' Z' s') \<longrightarrow> Q Z s')) 73 ==> G|-{P}.c.{Q}" 74 75 76| Skip: "G|-{P}. SKIP .{P}" 77 78| Ass: "G|-{%Z s. P Z (s[X::=a s])}. X:==a .{P}" 79 80| Local: "G|-{P}. c .{%Z s. Q Z (s[Loc X::=s'<X>])} 81 ==> G|-{%Z s. s'=s & P Z (s[Loc X::=a s])}. LOCAL X:=a IN c .{Q}" 82 83| Comp: "[| G|-{P}.c.{Q}; 84 G|-{Q}.d.{R} |] 85 ==> G|-{P}. (c;;d) .{R}" 86 87| If: "[| G|-{P &> b }.c.{Q}; 88 G|-{P &> (Not o b)}.d.{Q} |] 89 ==> G|-{P}. IF b THEN c ELSE d .{Q}" 90 91| Loop: "G|-{P &> b}.c.{P} ==> 92 G|-{P}. WHILE b DO c .{P &> (Not o b)}" 93 94(* 95 BodyN: "(insert ({P}. BODY pn .{Q}) G) 96 |-{P}. the (body pn) .{Q} ==> 97 G|-{P}. BODY pn .{Q}" 98*) 99| Body: "[| G Un (%p. {P p}. BODY p .{Q p})`Procs 100 ||-(%p. {P p}. the (body p) .{Q p})`Procs |] 101 ==> G||-(%p. {P p}. BODY p .{Q p})`Procs" 102 103| Call: "G|-{P}. BODY pn .{%Z s. Q Z (setlocs s (getlocs s')[X::=s<Res>])} 104 ==> G|-{%Z s. s'=s & P Z (setlocs s newlocs[Loc Arg::=a s])}. 105 X:=CALL pn(a) .{Q}" 106 107 108section \<open>Soundness and relative completeness of Hoare rules wrt operational semantics\<close> 109 110lemma single_stateE: 111 "state_not_singleton \<Longrightarrow> \<forall>t. (\<forall>s::state. s = t) \<longrightarrow> False" 112apply (unfold state_not_singleton_def) 113apply clarify 114apply (case_tac "ta = t") 115apply blast 116apply (blast dest: not_sym) 117done 118 119declare peek_and_def [simp] 120 121 122subsection "validity" 123 124lemma triple_valid_def2: 125 "|=n:{P}.c.{Q} = (\<forall>Z s. P Z s \<longrightarrow> (\<forall>s'. <c,s> -n-> s' \<longrightarrow> Q Z s'))" 126apply (unfold triple_valid_def) 127apply auto 128done 129 130lemma Body_triple_valid_0: "|=0:{P}. BODY pn .{Q}" 131apply (simp (no_asm) add: triple_valid_def2) 132apply clarsimp 133done 134 135(* only ==> direction required *) 136lemma Body_triple_valid_Suc: "|=n:{P}. the (body pn) .{Q} = |=Suc n:{P}. BODY pn .{Q}" 137apply (simp (no_asm) add: triple_valid_def2) 138apply force 139done 140 141lemma triple_valid_Suc [rule_format (no_asm)]: "|=Suc n:t --> |=n:t" 142apply (unfold triple_valid_def) 143apply (induct_tac t) 144apply simp 145apply (fast intro: evaln_Suc) 146done 147 148lemma triples_valid_Suc: "||=Suc n:ts ==> ||=n:ts" 149apply (fast intro: triple_valid_Suc) 150done 151 152 153subsection "derived rules" 154 155lemma conseq12: "[| G|-{P'}.c.{Q'}; \<forall>Z s. P Z s \<longrightarrow> 156 (\<forall>s'. (\<forall>Z'. P' Z' s \<longrightarrow> Q' Z' s') --> Q Z s') |] 157 ==> G|-{P}.c.{Q}" 158apply (rule hoare_derivs.conseq) 159apply blast 160done 161 162lemma conseq1: "[| G|-{P'}.c.{Q}; \<forall>Z s. P Z s \<longrightarrow> P' Z s |] ==> G|-{P}.c.{Q}" 163apply (erule conseq12) 164apply fast 165done 166 167lemma conseq2: "[| G|-{P}.c.{Q'}; \<forall>Z s. Q' Z s \<longrightarrow> Q Z s |] ==> G|-{P}.c.{Q}" 168apply (erule conseq12) 169apply fast 170done 171 172lemma Body1: "[| G Un (\<lambda>p. {P p}. BODY p .{Q p})`Procs 173 ||- (\<lambda>p. {P p}. the (body p) .{Q p})`Procs; 174 pn \<in> Procs |] ==> G|-{P pn}. BODY pn .{Q pn}" 175apply (drule hoare_derivs.Body) 176apply (erule hoare_derivs.weaken) 177apply fast 178done 179 180lemma BodyN: "(insert ({P}. BODY pn .{Q}) G) |-{P}. the (body pn) .{Q} ==> 181 G|-{P}. BODY pn .{Q}" 182apply (rule Body1) 183apply (rule_tac [2] singletonI) 184apply clarsimp 185done 186 187lemma escape: "[| \<forall>Z s. P Z s \<longrightarrow> G|-{\<lambda>Z s'. s'=s}.c.{\<lambda>Z'. Q Z} |] ==> G|-{P}.c.{Q}" 188apply (rule hoare_derivs.conseq) 189apply fast 190done 191 192lemma "constant": "[| C ==> G|-{P}.c.{Q} |] ==> G|-{\<lambda>Z s. P Z s & C}.c.{Q}" 193apply (rule hoare_derivs.conseq) 194apply fast 195done 196 197lemma LoopF: "G|-{\<lambda>Z s. P Z s \<and> \<not>b s}.WHILE b DO c.{P}" 198apply (rule hoare_derivs.Loop [THEN conseq2]) 199apply (simp_all (no_asm)) 200apply (rule hoare_derivs.conseq) 201apply fast 202done 203 204(* 205Goal "[| G'||-ts; G' <= G |] ==> G||-ts" 206by (etac hoare_derivs.cut 1); 207by (etac hoare_derivs.asm 1); 208qed "thin"; 209*) 210lemma thin [rule_format]: "G'||-ts \<Longrightarrow> \<forall>G. G' <= G \<longrightarrow> G||-ts" 211apply (erule hoare_derivs.induct) 212apply (tactic \<open>ALLGOALS (EVERY'[clarify_tac \<^context>, REPEAT o smp_tac \<^context> 1])\<close>) 213apply (rule hoare_derivs.empty) 214apply (erule (1) hoare_derivs.insert) 215apply (fast intro: hoare_derivs.asm) 216apply (fast intro: hoare_derivs.cut) 217apply (fast intro: hoare_derivs.weaken) 218apply (rule hoare_derivs.conseq, intro strip, tactic "smp_tac \<^context> 2 1", clarify, tactic "smp_tac \<^context> 1 1",rule exI, rule exI, erule (1) conjI) 219prefer 7 220apply (rule_tac hoare_derivs.Body, drule_tac spec, erule_tac mp, fast) 221apply (tactic \<open>ALLGOALS (resolve_tac \<^context> ((funpow 5 tl) @{thms hoare_derivs.intros}) THEN_ALL_NEW (fast_tac \<^context>))\<close>) 222done 223 224lemma weak_Body: "G|-{P}. the (body pn) .{Q} ==> G|-{P}. BODY pn .{Q}" 225apply (rule BodyN) 226apply (erule thin) 227apply auto 228done 229 230lemma derivs_insertD: "G||-insert t ts ==> G|-t & G||-ts" 231apply (fast intro: hoare_derivs.weaken) 232done 233 234lemma finite_pointwise [rule_format (no_asm)]: "[| finite U; 235 \<forall>p. G |- {P' p}.c0 p.{Q' p} --> G |- {P p}.c0 p.{Q p} |] ==> 236 G||-(%p. {P' p}.c0 p.{Q' p}) ` U --> G||-(%p. {P p}.c0 p.{Q p}) ` U" 237apply (erule finite_induct) 238apply simp 239apply clarsimp 240apply (drule derivs_insertD) 241apply (rule hoare_derivs.insert) 242apply auto 243done 244 245 246subsection "soundness" 247 248lemma Loop_sound_lemma: 249 "G|={P &> b}. c .{P} ==> 250 G|={P}. WHILE b DO c .{P &> (Not o b)}" 251apply (unfold hoare_valids_def) 252apply (simp (no_asm_use) add: triple_valid_def2) 253apply (rule allI) 254apply (subgoal_tac "\<forall>d s s'. <d,s> -n-> s' --> d = WHILE b DO c --> ||=n:G --> (\<forall>Z. P Z s --> P Z s' & ~b s') ") 255apply (erule thin_rl, fast) 256apply ((rule allI)+, rule impI) 257apply (erule evaln.induct) 258apply (simp_all (no_asm)) 259apply fast 260apply fast 261done 262 263lemma Body_sound_lemma: 264 "[| G Un (%pn. {P pn}. BODY pn .{Q pn})`Procs 265 ||=(%pn. {P pn}. the (body pn) .{Q pn})`Procs |] ==> 266 G||=(%pn. {P pn}. BODY pn .{Q pn})`Procs" 267apply (unfold hoare_valids_def) 268apply (rule allI) 269apply (induct_tac n) 270apply (fast intro: Body_triple_valid_0) 271apply clarsimp 272apply (drule triples_valid_Suc) 273apply (erule (1) notE impE) 274apply (simp add: ball_Un) 275apply (drule spec, erule impE, erule conjI, assumption) 276apply (fast intro!: Body_triple_valid_Suc [THEN iffD1]) 277done 278 279lemma hoare_sound: "G||-ts ==> G||=ts" 280apply (erule hoare_derivs.induct) 281apply (tactic \<open>TRYALL (eresolve_tac \<^context> [@{thm Loop_sound_lemma}, @{thm Body_sound_lemma}] THEN_ALL_NEW assume_tac \<^context>)\<close>) 282apply (unfold hoare_valids_def) 283apply blast 284apply blast 285apply (blast) (* asm *) 286apply (blast) (* cut *) 287apply (blast) (* weaken *) 288apply (tactic \<open>ALLGOALS (EVERY' 289 [REPEAT o Rule_Insts.thin_tac \<^context> "hoare_derivs _ _" [], 290 simp_tac \<^context>, clarify_tac \<^context>, REPEAT o smp_tac \<^context> 1])\<close>) 291apply (simp_all (no_asm_use) add: triple_valid_def2) 292apply (intro strip, tactic "smp_tac \<^context> 2 1", blast) (* conseq *) 293apply (tactic \<open>ALLGOALS (clarsimp_tac \<^context>)\<close>) (* Skip, Ass, Local *) 294prefer 3 apply (force) (* Call *) 295apply (erule_tac [2] evaln_elim_cases) (* If *) 296apply blast+ 297done 298 299 300section "completeness" 301 302(* Both versions *) 303 304(*unused*) 305lemma MGT_alternI: "G|-MGT c \<Longrightarrow> 306 G|-{\<lambda>Z s0. \<forall>s1. <c,s0> -c-> s1 \<longrightarrow> Z=s1}. c .{\<lambda>Z s1. Z=s1}" 307apply (unfold MGT_def) 308apply (erule conseq12) 309apply auto 310done 311 312(* requires com_det *) 313lemma MGT_alternD: "state_not_singleton \<Longrightarrow> 314 G|-{\<lambda>Z s0. \<forall>s1. <c,s0> -c-> s1 \<longrightarrow> Z=s1}. c .{\<lambda>Z s1. Z=s1} \<Longrightarrow> G|-MGT c" 315apply (unfold MGT_def) 316apply (erule conseq12) 317apply auto 318apply (case_tac "\<exists>t. <c,s> -c-> t" for s) 319apply (fast elim: com_det) 320apply clarsimp 321apply (drule single_stateE) 322apply blast 323done 324 325lemma MGF_complete: 326 "{}|-(MGT c::state triple) ==> {}|={P}.c.{Q} ==> {}|-{P}.c.{Q::state assn}" 327apply (unfold MGT_def) 328apply (erule conseq12) 329apply (clarsimp simp add: hoare_valids_def eval_eq triple_valid_def2) 330done 331 332declare WTs_elim_cases [elim!] 333declare not_None_eq [iff] 334(* requires com_det, escape (i.e. hoare_derivs.conseq) *) 335lemma MGF_lemma1 [rule_format (no_asm)]: "state_not_singleton \<Longrightarrow> 336 \<forall>pn \<in> dom body. G|-{=}.BODY pn.{->} \<Longrightarrow> WT c --> G|-{=}.c.{->}" 337apply (induct_tac c) 338apply (tactic \<open>ALLGOALS (clarsimp_tac \<^context>)\<close>) 339prefer 7 apply (fast intro: domI) 340apply (erule_tac [6] MGT_alternD) 341apply (unfold MGT_def) 342apply (drule_tac [7] bspec, erule_tac [7] domI) 343apply (rule_tac [7] escape, tactic \<open>clarsimp_tac \<^context> 7\<close>, 344 rename_tac [7] "fun" y Z, 345 rule_tac [7] P1 = "%Z' s. s= (setlocs Z newlocs) [Loc Arg ::= fun Z]" in hoare_derivs.Call [THEN conseq1], erule_tac [7] conseq12) 346apply (erule_tac [!] thin_rl) 347apply (rule hoare_derivs.Skip [THEN conseq2]) 348apply (rule_tac [2] hoare_derivs.Ass [THEN conseq1]) 349apply (rule_tac [3] escape, tactic \<open>clarsimp_tac \<^context> 3\<close>, 350 rename_tac [3] loc "fun" y Z, 351 rule_tac [3] P1 = "%Z' s. s= (Z[Loc loc::=fun Z])" in hoare_derivs.Local [THEN conseq1], 352 erule_tac [3] conseq12) 353apply (erule_tac [5] hoare_derivs.Comp, erule_tac [5] conseq12) 354apply (tactic \<open>(resolve_tac \<^context> @{thms hoare_derivs.If} THEN_ALL_NEW 355 eresolve_tac \<^context> @{thms conseq12}) 6\<close>) 356apply (rule_tac [8] hoare_derivs.Loop [THEN conseq2], erule_tac [8] conseq12) 357apply auto 358done 359 360(* Version: nested single recursion *) 361 362lemma nesting_lemma [rule_format]: 363 assumes "!!G ts. ts <= G ==> P G ts" 364 and "!!G pn. P (insert (mgt_call pn) G) {mgt(the(body pn))} ==> P G {mgt_call pn}" 365 and "!!G c. [| wt c; \<forall>pn\<in>U. P G {mgt_call pn} |] ==> P G {mgt c}" 366 and "!!pn. pn \<in> U ==> wt (the (body pn))" 367 shows "finite U ==> uG = mgt_call`U ==> 368 \<forall>G. G <= uG --> n <= card uG --> card G = card uG - n --> (\<forall>c. wt c --> P G {mgt c})" 369apply (induct_tac n) 370apply (tactic \<open>ALLGOALS (clarsimp_tac \<^context>)\<close>) 371apply (subgoal_tac "G = mgt_call ` U") 372prefer 2 373apply (simp add: card_seteq) 374apply simp 375apply (erule assms(3-)) (*MGF_lemma1*) 376apply (rule ballI) 377apply (rule assms) (*hoare_derivs.asm*) 378apply fast 379apply (erule assms(3-)) (*MGF_lemma1*) 380apply (rule ballI) 381apply (case_tac "mgt_call pn \<in> G") 382apply (rule assms) (*hoare_derivs.asm*) 383apply fast 384apply (rule assms(2-)) (*MGT_BodyN*) 385apply (drule spec, erule impE, erule_tac [2] impE, drule_tac [3] spec, erule_tac [3] mp) 386apply (erule_tac [3] assms(4-)) 387apply fast 388apply (drule finite_subset) 389apply (erule finite_imageI) 390apply (simp (no_asm_simp)) 391done 392 393lemma MGT_BodyN: "insert ({=}.BODY pn.{->}) G|-{=}. the (body pn) .{->} ==> 394 G|-{=}.BODY pn.{->}" 395apply (unfold MGT_def) 396apply (rule BodyN) 397apply (erule conseq2) 398apply force 399done 400 401(* requires BodyN, com_det *) 402lemma MGF: "[| state_not_singleton; WT_bodies; WT c |] ==> {}|-MGT c" 403apply (rule_tac P = "%G ts. G||-ts" and U = "dom body" in nesting_lemma) 404apply (erule hoare_derivs.asm) 405apply (erule MGT_BodyN) 406apply (rule_tac [3] finite_dom_body) 407apply (erule MGF_lemma1) 408prefer 2 apply (assumption) 409apply blast 410apply clarsimp 411apply (erule (1) WT_bodiesD) 412apply (rule_tac [3] le_refl) 413apply auto 414done 415 416 417(* Version: simultaneous recursion in call rule *) 418 419(* finiteness not really necessary here *) 420lemma MGT_Body: "[| G Un (%pn. {=}. BODY pn .{->})`Procs 421 ||-(%pn. {=}. the (body pn) .{->})`Procs; 422 finite Procs |] ==> G ||-(%pn. {=}. BODY pn .{->})`Procs" 423apply (unfold MGT_def) 424apply (rule hoare_derivs.Body) 425apply (erule finite_pointwise) 426prefer 2 apply (assumption) 427apply clarify 428apply (erule conseq2) 429apply auto 430done 431 432(* requires empty, insert, com_det *) 433lemma MGF_lemma2_simult [rule_format (no_asm)]: "[| state_not_singleton; WT_bodies; 434 F<=(%pn. {=}.the (body pn).{->})`dom body |] ==> 435 (%pn. {=}. BODY pn .{->})`dom body||-F" 436apply (frule finite_subset) 437apply (rule finite_dom_body [THEN finite_imageI]) 438apply (rotate_tac 2) 439apply (tactic "make_imp_tac \<^context> 1") 440apply (erule finite_induct) 441apply (clarsimp intro!: hoare_derivs.empty) 442apply (clarsimp intro!: hoare_derivs.insert simp del: range_composition) 443apply (erule MGF_lemma1) 444prefer 2 apply (fast dest: WT_bodiesD) 445apply clarsimp 446apply (rule hoare_derivs.asm) 447apply (fast intro: domI) 448done 449 450(* requires Body, empty, insert, com_det *) 451lemma MGF': "[| state_not_singleton; WT_bodies; WT c |] ==> {}|-MGT c" 452apply (rule MGF_lemma1) 453apply assumption 454prefer 2 apply (assumption) 455apply clarsimp 456apply (subgoal_tac "{}||- (%pn. {=}. BODY pn .{->}) `dom body") 457apply (erule hoare_derivs.weaken) 458apply (fast intro: domI) 459apply (rule finite_dom_body [THEN [2] MGT_Body]) 460apply (simp (no_asm)) 461apply (erule (1) MGF_lemma2_simult) 462apply (rule subset_refl) 463done 464 465(* requires Body+empty+insert / BodyN, com_det *) 466lemmas hoare_complete = MGF' [THEN MGF_complete] 467 468 469subsection "unused derived rules" 470 471lemma falseE: "G|-{%Z s. False}.c.{Q}" 472apply (rule hoare_derivs.conseq) 473apply fast 474done 475 476lemma trueI: "G|-{P}.c.{%Z s. True}" 477apply (rule hoare_derivs.conseq) 478apply (fast intro!: falseE) 479done 480 481lemma disj: "[| G|-{P}.c.{Q}; G|-{P'}.c.{Q'} |] 482 ==> G|-{%Z s. P Z s | P' Z s}.c.{%Z s. Q Z s | Q' Z s}" 483apply (rule hoare_derivs.conseq) 484apply (fast elim: conseq12) 485done (* analogue conj non-derivable *) 486 487lemma hoare_SkipI: "(\<forall>Z s. P Z s \<longrightarrow> Q Z s) \<Longrightarrow> G|-{P}. SKIP .{Q}" 488apply (rule conseq12) 489apply (rule hoare_derivs.Skip) 490apply fast 491done 492 493 494subsection "useful derived rules" 495 496lemma single_asm: "{t}|-t" 497apply (rule hoare_derivs.asm) 498apply (rule subset_refl) 499done 500 501lemma export_s: "[| !!s'. G|-{%Z s. s'=s & P Z s}.c.{Q} |] ==> G|-{P}.c.{Q}" 502apply (rule hoare_derivs.conseq) 503apply auto 504done 505 506 507lemma weak_Local: "[| G|-{P}. c .{Q}; \<forall>k Z s. Q Z s --> Q Z (s[Loc Y::=k]) |] ==> 508 G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{Q}" 509apply (rule export_s) 510apply (rule hoare_derivs.Local) 511apply (erule conseq2) 512apply (erule spec) 513done 514 515(* 516Goal "!Q. G |-{%Z s. ~(? s'. <c,s> -c-> s')}. c .{Q}" 517by (induct_tac "c" 1); 518by Auto_tac; 519by (rtac conseq1 1); 520by (rtac hoare_derivs.Skip 1); 521force 1; 522by (rtac conseq1 1); 523by (rtac hoare_derivs.Ass 1); 524force 1; 525by (defer_tac 1); 526### 527by (rtac hoare_derivs.Comp 1); 528by (dtac spec 2); 529by (dtac spec 2); 530by (assume_tac 2); 531by (etac conseq1 2); 532by (Clarsimp_tac 2); 533force 1; 534*) 535 536end 537