src/HOL/IMPP/Misc.thy
author wenzelm
Wed Sep 17 21:27:14 2008 +0200 (2008-09-17)
changeset 28263 69eaa97e7e96
parent 27148 5b78e50adc49
child 28524 644b62cf678f
permissions -rw-r--r--
moved global ML bindings to global place;
     1 (*  Title:      HOL/IMPP/Misc.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4     Copyright   1999 TUM
     5 *)
     6 
     7 header {* Several examples for Hoare logic *}
     8 
     9 theory Misc
    10 imports Hoare
    11 begin
    12 
    13 defs
    14   newlocs_def: "newlocs       == %x. arbitrary"
    15   setlocs_def: "setlocs s l'  == case s of st g l => st g l'"
    16   getlocs_def: "getlocs s     == case s of st g l => l"
    17    update_def: "update s vn v == case vn of
    18                                Glb gn => (case s of st g l => st (g(gn:=v)) l)
    19                              | Loc ln => (case s of st g l => st g (l(ln:=v)))"
    20 
    21 
    22 subsection "state access"
    23 
    24 lemma getlocs_def2: "getlocs (st g l) = l"
    25 apply (unfold getlocs_def)
    26 apply simp
    27 done
    28 
    29 lemma update_Loc_idem2 [simp]: "s[Loc Y::=s<Y>] = s"
    30 apply (unfold update_def)
    31 apply (induct_tac s)
    32 apply (simp add: getlocs_def2)
    33 done
    34 
    35 lemma update_overwrt [simp]: "s[X::=x][X::=y] = s[X::=y]"
    36 apply (unfold update_def)
    37 apply (induct_tac X)
    38 apply  auto
    39 apply  (induct_tac [!] s)
    40 apply  auto
    41 done
    42 
    43 lemma getlocs_Loc_update [simp]: "(s[Loc Y::=k])<Y'> = (if Y=Y' then k else s<Y'>)"
    44 apply (unfold update_def)
    45 apply (induct_tac s)
    46 apply (simp add: getlocs_def2)
    47 done
    48 
    49 lemma getlocs_Glb_update [simp]: "getlocs (s[Glb Y::=k]) = getlocs s"
    50 apply (unfold update_def)
    51 apply (induct_tac s)
    52 apply (simp add: getlocs_def2)
    53 done
    54 
    55 lemma getlocs_setlocs [simp]: "getlocs (setlocs s l) = l"
    56 apply (unfold setlocs_def)
    57 apply (induct_tac s)
    58 apply auto
    59 apply (simp add: getlocs_def2)
    60 done
    61 
    62 lemma getlocs_setlocs_lemma: "getlocs (setlocs s (getlocs s')[Y::=k]) = getlocs (s'[Y::=k])"
    63 apply (induct_tac Y)
    64 apply (rule_tac [2] ext)
    65 apply auto
    66 done
    67 
    68 (*unused*)
    69 lemma classic_Local_valid: 
    70 "!v. G|={%Z s. P Z (s[Loc Y::=v]) & s<Y> = a (s[Loc Y::=v])}.  
    71   c .{%Z s. Q Z (s[Loc Y::=v])} ==> G|={P}. LOCAL Y:=a IN c .{Q}"
    72 apply (unfold hoare_valids_def)
    73 apply (simp (no_asm_use) add: triple_valid_def2)
    74 apply clarsimp
    75 apply (drule_tac x = "s<Y>" in spec)
    76 apply (tactic "smp_tac 1 1")
    77 apply (drule spec)
    78 apply (drule_tac x = "s[Loc Y::=a s]" in spec)
    79 apply (simp (no_asm_use))
    80 apply (erule (1) notE impE)
    81 apply (tactic "smp_tac 1 1")
    82 apply simp
    83 done
    84 
    85 lemma classic_Local: "!v. G|-{%Z s. P Z (s[Loc Y::=v]) & s<Y> = a (s[Loc Y::=v])}.  
    86   c .{%Z s. Q Z (s[Loc Y::=v])} ==> G|-{P}. LOCAL Y:=a IN c .{Q}"
    87 apply (rule export_s)
    88 apply (rule hoare_derivs.Local [THEN conseq1])
    89 apply (erule spec)
    90 apply force
    91 done
    92 
    93 lemma classic_Local_indep: "[| Y~=Y'; G|-{P}. c .{%Z s. s<Y'> = d} |] ==>  
    94   G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'> = d}"
    95 apply (rule classic_Local)
    96 apply clarsimp
    97 apply (erule conseq12)
    98 apply clarsimp
    99 apply (drule sym)
   100 apply simp
   101 done
   102 
   103 lemma Local_indep: "[| Y~=Y'; G|-{P}. c .{%Z s. s<Y'> = d} |] ==>  
   104   G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'> = d}"
   105 apply (rule export_s)
   106 apply (rule hoare_derivs.Local)
   107 apply clarsimp
   108 done
   109 
   110 lemma weak_Local_indep: "[| Y'~=Y; G|-{P}. c .{%Z s. s<Y'> = d} |] ==>  
   111   G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'> = d}"
   112 apply (rule weak_Local)
   113 apply auto
   114 done
   115 
   116 
   117 lemma export_Local_invariant: "G|-{%Z s. Z = s<Y>}. LOCAL Y:=a IN c .{%Z s. Z = s<Y>}"
   118 apply (rule export_s)
   119 apply (rule_tac P' = "%Z s. s'=s & True" and Q' = "%Z s. s'<Y> = s<Y>" in conseq12)
   120 prefer 2
   121 apply  clarsimp
   122 apply (rule hoare_derivs.Local)
   123 apply clarsimp
   124 apply (rule trueI)
   125 done
   126 
   127 lemma classic_Local_invariant: "G|-{%Z s. Z = s<Y>}. LOCAL Y:=a IN c .{%Z s. Z = s<Y>}"
   128 apply (rule classic_Local)
   129 apply clarsimp
   130 apply (rule trueI [THEN conseq12])
   131 apply clarsimp
   132 done
   133 
   134 lemma Call_invariant: "G|-{P}. BODY pn .{%Z s. Q Z (setlocs s (getlocs s')[X::=s<Res>])} ==>  
   135   G|-{%Z s. s'=s & I Z (getlocs (s[X::=k Z])) & P Z (setlocs s newlocs[Loc Arg::=a s])}.  
   136   X:=CALL pn (a) .{%Z s. I Z (getlocs (s[X::=k Z])) & Q Z s}"
   137 apply (rule_tac s'1 = "s'" and
   138   Q' = "%Z s. I Z (getlocs (s[X::=k Z])) = I Z (getlocs (s'[X::=k Z])) & Q Z s" in
   139   hoare_derivs.Call [THEN conseq12])
   140 apply  (simp (no_asm_simp) add: getlocs_setlocs_lemma)
   141 apply force
   142 done
   143 
   144 end