src/HOL/IMPP/Misc.ML
author wenzelm
Sat, 17 Sep 2005 20:14:30 +0200
changeset 17477 ceb42ea2f223
parent 15354 9234f5765d9c
permissions -rw-r--r--
converted to Isar theory format;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     1
(*  Title:      HOL/IMPP/Misc.ML
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     2
    ID:         $Id$
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     3
    Author:     David von Oheimb
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     4
    Copyright   1999 TUM
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     5
*)
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     6
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     7
section "state access";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     8
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     9
Goalw [getlocs_def] "getlocs (st g l) = l";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    10
by (Simp_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    11
qed "getlocs_def2";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    12
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    13
Goalw [update_def] "s[Loc Y::=s<Y>] = s";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    14
by (induct_tac "s" 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    15
by (simp_tac (simpset() addsimps [getlocs_def2]) 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    16
qed "update_Loc_idem2";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    17
Addsimps[update_Loc_idem2];
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    18
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    19
Goalw [update_def] "s[X::=x][X::=y] = s[X::=y]";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    20
by (induct_tac "X" 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    21
by  Auto_tac;
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    22
by  (ALLGOALS (induct_tac "s"));
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    23
by  Auto_tac;
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    24
by  (ALLGOALS (rtac ext));
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    25
by  Auto_tac;
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    26
qed "update_overwrt";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    27
Addsimps[update_overwrt];
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    28
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    29
Goalw [update_def]"(s[Loc Y::=k])<Y'> = (if Y=Y' then k else s<Y'>)";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    30
by (induct_tac "s" 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    31
by (simp_tac (simpset() addsimps [getlocs_def2]) 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    32
qed "getlocs_Loc_update";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    33
Addsimps[getlocs_Loc_update];
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    34
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    35
Goalw [update_def] "getlocs (s[Glb Y::=k]) = getlocs s";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    36
by (induct_tac "s" 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    37
by (simp_tac (simpset() addsimps [getlocs_def2]) 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    38
qed "getlocs_Glb_update";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    39
Addsimps[getlocs_Glb_update];
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    40
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    41
Goalw [setlocs_def] "getlocs (setlocs s l) = l";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    42
by (induct_tac "s" 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    43
by Auto_tac;
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    44
by (simp_tac (simpset() addsimps [getlocs_def2]) 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    45
qed "getlocs_setlocs";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    46
Addsimps[getlocs_setlocs];
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    47
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    48
Goal "getlocs (setlocs s (getlocs s')[Y::=k]) = getlocs (s'[Y::=k])";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    49
by (induct_tac "Y" 1);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8600
diff changeset
    50
by (rtac ext 2);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    51
by Auto_tac;
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    52
qed "getlocs_setlocs_lemma";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    53
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    54
(*unused*)
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    55
Goalw [hoare_valids_def] 
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    56
"!v. G|={%Z s. P Z (s[Loc Y::=v]) & s<Y> = a (s[Loc Y::=v])}. \
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    57
\ c .{%Z s. Q Z (s[Loc Y::=v])} ==> G|={P}. LOCAL Y:=a IN c .{Q}";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    58
by (full_simp_tac (simpset() addsimps [triple_valid_def2]) 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    59
by (Clarsimp_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    60
by (dres_inst_tac [("x","s<Y>")] spec 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    61
by (smp_tac 1 1);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8600
diff changeset
    62
by (dtac spec 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    63
by (dres_inst_tac [("x","s[Loc Y::=a s]")] spec 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    64
by (Full_simp_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    65
by (mp_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    66
by (smp_tac 1 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    67
by (Simp_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    68
qed "classic_Local_valid";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    69
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    70
Goal "!v. G|-{%Z s. P Z (s[Loc Y::=v]) & s<Y> = a (s[Loc Y::=v])}. \
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    71
\ c .{%Z s. Q Z (s[Loc Y::=v])} ==> G|-{P}. LOCAL Y:=a IN c .{Q}";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8600
diff changeset
    72
by (rtac export_s 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    73
(*variant 1*)
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8600
diff changeset
    74
by (rtac (hoare_derivs.Local RS conseq1) 1);
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8600
diff changeset
    75
by (etac spec 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    76
by (Force_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    77
(*variant 2
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    78
by (res_inst_tac [("P'","%Z s. s' = s & P Z (s[Loc Y::=a s][Loc Y::=s'<Y>]) & (s[Loc Y::=a s])<Y> = a (s[Loc Y::=a s][Loc Y::=s'<Y>])")] conseq1 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    79
by  (Clarsimp_tac 2);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8600
diff changeset
    80
by (rtac hoare_derivs.Local 1);
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8600
diff changeset
    81
by (etac spec 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    82
*)
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    83
qed "classic_Local";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    84
15354
9234f5765d9c Added > and >= sugar
nipkow
parents: 10962
diff changeset
    85
Goal "[| Y~=Y'; G|-{P}. c .{%Z s. s<Y'> = d} |] ==> \
9234f5765d9c Added > and >= sugar
nipkow
parents: 10962
diff changeset
    86
\ G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'> = d}";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8600
diff changeset
    87
by (rtac classic_Local 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    88
by (ALLGOALS Clarsimp_tac);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8600
diff changeset
    89
by (etac conseq12 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    90
by (Clarsimp_tac 1);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8600
diff changeset
    91
by (dtac sym 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    92
by (Asm_full_simp_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    93
qed "classic_Local_indep";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    94
15354
9234f5765d9c Added > and >= sugar
nipkow
parents: 10962
diff changeset
    95
Goal "[| Y~=Y'; G|-{P}. c .{%Z s. s<Y'> = d} |] ==> \
9234f5765d9c Added > and >= sugar
nipkow
parents: 10962
diff changeset
    96
\ G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'> = d}";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8600
diff changeset
    97
by (rtac export_s 1);
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8600
diff changeset
    98
by (rtac hoare_derivs.Local 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    99
by (Clarsimp_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   100
qed "Local_indep";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   101
15354
9234f5765d9c Added > and >= sugar
nipkow
parents: 10962
diff changeset
   102
Goal "[| Y'~=Y; G|-{P}. c .{%Z s. s<Y'> = d} |] ==> \
9234f5765d9c Added > and >= sugar
nipkow
parents: 10962
diff changeset
   103
\ G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'> = d}";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8600
diff changeset
   104
by (rtac weak_Local 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   105
by (ALLGOALS Clarsimp_tac);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   106
qed "weak_Local_indep";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   107
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   108
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   109
Goal "G|-{%Z s. Z = s<Y>}. LOCAL Y:=a IN c .{%Z s. Z = s<Y>}";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8600
diff changeset
   110
by (rtac export_s 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   111
by (res_inst_tac [("P'","%Z s. s'=s & True"), ("Q'","%Z s. s'<Y> = s<Y>")] (conseq12) 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   112
by  (Clarsimp_tac 2);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8600
diff changeset
   113
by (rtac hoare_derivs.Local 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   114
by (Clarsimp_tac 1);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8600
diff changeset
   115
by (rtac trueI 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   116
qed "export_Local_invariant";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   117
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   118
Goal "G|-{%Z s. Z = s<Y>}. LOCAL Y:=a IN c .{%Z s. Z = s<Y>}";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8600
diff changeset
   119
by (rtac classic_Local 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   120
by (Clarsimp_tac 1);
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 8600
diff changeset
   121
by (rtac (trueI RS conseq12) 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   122
by (Clarsimp_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   123
qed "classic_Local_invariant";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   124
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   125
Goal "G|-{P}. BODY pn .{%Z s. Q Z (setlocs s (getlocs s')[X::=s<Res>])} ==> \
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   126
\ G|-{%Z s. s'=s & I Z (getlocs (s[X::=k Z])) & P Z (setlocs s newlocs[Loc Arg::=a s])}. \
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   127
\ X:=CALL pn (a) .{%Z s. I Z (getlocs (s[X::=k Z])) & Q Z s}";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   128
by (res_inst_tac [("s'1","s'"),("Q'","%Z s. I Z (getlocs (s[X::=k Z])) = I Z (getlocs (s'[X::=k Z])) & Q Z s")] (hoare_derivs.Call RS conseq12) 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   129
by  (asm_simp_tac  (simpset() addsimps [getlocs_setlocs_lemma]) 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   130
by (Force_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   131
qed "Call_invariant";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   132
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   133