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