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