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