src/HOL/IMP/ACom.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46225 d0a2c4a80a00
child 47613 e72e44cee6f2
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
     1
(* Author: Tobias Nipkow *)
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
     2
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
     3
theory ACom
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
     4
imports Com
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
     5
begin
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
     6
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
     7
(* is there a better place? *)
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
     8
definition "show_state xs s = [(x,s x). x \<leftarrow> xs]"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
     9
46225
nipkow
parents: 46157
diff changeset
    10
subsection "Annotated Commands"
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    11
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    12
datatype 'a acom =
45751
f8723843c29e enforce parantheses around SKIP {_}
nipkow
parents: 45746
diff changeset
    13
  SKIP   'a                           ("SKIP {_}" 61) |
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    14
  Assign vname aexp 'a                ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    15
  Semi   "('a acom)" "('a acom)"          ("_;//_"  [60, 61] 60) |
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    16
  If     bexp "('a acom)" "('a acom)" 'a
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    17
    ("(IF _/ THEN _/ ELSE _//{_})"  [0, 0, 61, 0] 61) |
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    18
  While  'a bexp "('a acom)" 'a
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    19
    ("({_}//WHILE _/ DO (_)//{_})"  [0, 0, 61, 0] 61)
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    20
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    21
fun post :: "'a acom \<Rightarrow>'a" where
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    22
"post (SKIP {P}) = P" |
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    23
"post (x ::= e {P}) = P" |
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    24
"post (c1; c2) = post c2" |
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    25
"post (IF b THEN c1 ELSE c2 {P}) = P" |
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    26
"post ({Inv} WHILE b DO c {P}) = P"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    27
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    28
fun strip :: "'a acom \<Rightarrow> com" where
45746
579fb74aa409 improved var names
nipkow
parents: 45623
diff changeset
    29
"strip (SKIP {P}) = com.SKIP" |
579fb74aa409 improved var names
nipkow
parents: 45623
diff changeset
    30
"strip (x ::= e {P}) = (x ::= e)" |
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    31
"strip (c1;c2) = (strip c1; strip c2)" |
45746
579fb74aa409 improved var names
nipkow
parents: 45623
diff changeset
    32
"strip (IF b THEN c1 ELSE c2 {P}) = (IF b THEN strip c1 ELSE strip c2)" |
579fb74aa409 improved var names
nipkow
parents: 45623
diff changeset
    33
"strip ({Inv} WHILE b DO c {P}) = (WHILE b DO strip c)"
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    34
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    35
fun anno :: "'a \<Rightarrow> com \<Rightarrow> 'a acom" where
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    36
"anno a com.SKIP = SKIP {a}" |
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    37
"anno a (x ::= e) = (x ::= e {a})" |
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    38
"anno a (c1;c2) = (anno a c1; anno a c2)" |
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    39
"anno a (IF b THEN c1 ELSE c2) =
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    40
  (IF b THEN anno a c1 ELSE anno a c2 {a})" |
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    41
"anno a (WHILE b DO c) =
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    42
  ({a} WHILE b DO anno a c {a})"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    43
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    44
fun map_acom :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a acom \<Rightarrow> 'b acom" where
45746
579fb74aa409 improved var names
nipkow
parents: 45623
diff changeset
    45
"map_acom f (SKIP {P}) = SKIP {f P}" |
579fb74aa409 improved var names
nipkow
parents: 45623
diff changeset
    46
"map_acom f (x ::= e {P}) = (x ::= e {f P})" |
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    47
"map_acom f (c1;c2) = (map_acom f c1; map_acom f c2)" |
45746
579fb74aa409 improved var names
nipkow
parents: 45623
diff changeset
    48
"map_acom f (IF b THEN c1 ELSE c2 {P}) =
579fb74aa409 improved var names
nipkow
parents: 45623
diff changeset
    49
  (IF b THEN map_acom f c1 ELSE map_acom f c2 {f P})" |
579fb74aa409 improved var names
nipkow
parents: 45623
diff changeset
    50
"map_acom f ({Inv} WHILE b DO c {P}) =
579fb74aa409 improved var names
nipkow
parents: 45623
diff changeset
    51
  ({f Inv} WHILE b DO map_acom f c {f P})"
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    52
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    53
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    54
lemma post_map_acom[simp]: "post(map_acom f c) = f(post c)"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    55
by (induction c) simp_all
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    56
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    57
lemma strip_acom[simp]: "strip (map_acom f c) = strip c"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    58
by (induction c) auto
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    59
46068
b9d4ec0f79ac tuned proofs
nipkow
parents: 45751
diff changeset
    60
lemma map_acom_SKIP:
b9d4ec0f79ac tuned proofs
nipkow
parents: 45751
diff changeset
    61
 "map_acom f c = SKIP {S'} \<longleftrightarrow> (\<exists>S. c = SKIP {S} \<and> S' = f S)"
b9d4ec0f79ac tuned proofs
nipkow
parents: 45751
diff changeset
    62
by (cases c) auto
b9d4ec0f79ac tuned proofs
nipkow
parents: 45751
diff changeset
    63
b9d4ec0f79ac tuned proofs
nipkow
parents: 45751
diff changeset
    64
lemma map_acom_Assign:
b9d4ec0f79ac tuned proofs
nipkow
parents: 45751
diff changeset
    65
 "map_acom f c = x ::= e {S'} \<longleftrightarrow> (\<exists>S. c = x::=e {S} \<and> S' = f S)"
b9d4ec0f79ac tuned proofs
nipkow
parents: 45751
diff changeset
    66
by (cases c) auto
b9d4ec0f79ac tuned proofs
nipkow
parents: 45751
diff changeset
    67
b9d4ec0f79ac tuned proofs
nipkow
parents: 45751
diff changeset
    68
lemma map_acom_Semi:
b9d4ec0f79ac tuned proofs
nipkow
parents: 45751
diff changeset
    69
 "map_acom f c = c1';c2' \<longleftrightarrow>
b9d4ec0f79ac tuned proofs
nipkow
parents: 45751
diff changeset
    70
 (\<exists>c1 c2. c = c1;c2 \<and> map_acom f c1 = c1' \<and> map_acom f c2 = c2')"
b9d4ec0f79ac tuned proofs
nipkow
parents: 45751
diff changeset
    71
by (cases c) auto
b9d4ec0f79ac tuned proofs
nipkow
parents: 45751
diff changeset
    72
b9d4ec0f79ac tuned proofs
nipkow
parents: 45751
diff changeset
    73
lemma map_acom_If:
b9d4ec0f79ac tuned proofs
nipkow
parents: 45751
diff changeset
    74
 "map_acom f c = IF b THEN c1' ELSE c2' {S'} \<longleftrightarrow>
b9d4ec0f79ac tuned proofs
nipkow
parents: 45751
diff changeset
    75
 (\<exists>S c1 c2. c = IF b THEN c1 ELSE c2 {S} \<and> map_acom f c1 = c1' \<and> map_acom f c2 = c2' \<and> S' = f S)"
b9d4ec0f79ac tuned proofs
nipkow
parents: 45751
diff changeset
    76
by (cases c) auto
b9d4ec0f79ac tuned proofs
nipkow
parents: 45751
diff changeset
    77
b9d4ec0f79ac tuned proofs
nipkow
parents: 45751
diff changeset
    78
lemma map_acom_While:
b9d4ec0f79ac tuned proofs
nipkow
parents: 45751
diff changeset
    79
 "map_acom f w = {I'} WHILE b DO c' {P'} \<longleftrightarrow>
b9d4ec0f79ac tuned proofs
nipkow
parents: 45751
diff changeset
    80
 (\<exists>I P c. w = {I} WHILE b DO c {P} \<and> map_acom f c = c' \<and> I' = f I \<and> P' = f P)"
b9d4ec0f79ac tuned proofs
nipkow
parents: 45751
diff changeset
    81
by (cases w) auto
b9d4ec0f79ac tuned proofs
nipkow
parents: 45751
diff changeset
    82
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    83
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    84
lemma strip_anno[simp]: "strip (anno a c) = c"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    85
by(induct c) simp_all
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    86
46157
3d518b508bbb added lemmas
nipkow
parents: 46068
diff changeset
    87
lemma strip_eq_SKIP:
3d518b508bbb added lemmas
nipkow
parents: 46068
diff changeset
    88
  "strip c = com.SKIP \<longleftrightarrow> (EX P. c = SKIP {P})"
3d518b508bbb added lemmas
nipkow
parents: 46068
diff changeset
    89
by (cases c) simp_all
3d518b508bbb added lemmas
nipkow
parents: 46068
diff changeset
    90
3d518b508bbb added lemmas
nipkow
parents: 46068
diff changeset
    91
lemma strip_eq_Assign:
3d518b508bbb added lemmas
nipkow
parents: 46068
diff changeset
    92
  "strip c = x::=e \<longleftrightarrow> (EX P. c = x::=e {P})"
3d518b508bbb added lemmas
nipkow
parents: 46068
diff changeset
    93
by (cases c) simp_all
3d518b508bbb added lemmas
nipkow
parents: 46068
diff changeset
    94
45623
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    95
lemma strip_eq_Semi:
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    96
  "strip c = c1;c2 \<longleftrightarrow> (EX d1 d2. c = d1;d2 & strip d1 = c1 & strip d2 = c2)"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    97
by (cases c) simp_all
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    98
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    99
lemma strip_eq_If:
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   100
  "strip c = IF b THEN c1 ELSE c2 \<longleftrightarrow>
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   101
  (EX d1 d2 P. c = IF b THEN d1 ELSE d2 {P} & strip d1 = c1 & strip d2 = c2)"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   102
by (cases c) simp_all
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   103
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   104
lemma strip_eq_While:
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   105
  "strip c = WHILE b DO c1 \<longleftrightarrow>
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   106
  (EX I d1 P. c = {I} WHILE b DO d1 {P} & strip d1 = c1)"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   107
by (cases c) simp_all
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   108
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
   109
end