src/HOL/IMP/ACom.thy
author nipkow
Mon, 05 Dec 2011 07:31:00 +0100
changeset 45751 f8723843c29e
parent 45746 579fb74aa409
child 46068 b9d4ec0f79ac
permissions -rw-r--r--
enforce parantheses around SKIP {_}
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
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    10
section "Annotated Commands"
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
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    60
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    61
lemma strip_anno[simp]: "strip (anno a c) = c"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    62
by(induct c) simp_all
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    63
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    64
lemma strip_eq_SKIP: "strip c = com.SKIP \<longleftrightarrow> (EX P. c = SKIP {P})"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    65
by (cases c) simp_all
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    66
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    67
lemma strip_eq_Assign: "strip c = x::=e \<longleftrightarrow> (EX P. c = x::=e {P})"
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    68
by (cases c) simp_all
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    69
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    70
lemma strip_eq_Semi:
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    71
  "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
    72
by (cases c) simp_all
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    73
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    74
lemma strip_eq_If:
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    75
  "strip c = IF b THEN c1 ELSE c2 \<longleftrightarrow>
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    76
  (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
    77
by (cases c) simp_all
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    78
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    79
lemma strip_eq_While:
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    80
  "strip c = WHILE b DO c1 \<longleftrightarrow>
f682f3f7b726 Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff changeset
    81
  (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
    82
by (cases c) simp_all
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
end