1 (* Author: Tobias Nipkow *) |
|
2 |
|
3 theory ACom_ITP |
|
4 imports "../Com" |
|
5 begin |
|
6 |
|
7 subsection "Annotated Commands" |
|
8 |
|
9 datatype 'a acom = |
|
10 SKIP 'a ("SKIP {_}" 61) | |
|
11 Assign vname aexp 'a ("(_ ::= _/ {_})" [1000, 61, 0] 61) | |
|
12 Seq "('a acom)" "('a acom)" ("_;;//_" [60, 61] 60) | |
|
13 If bexp "('a acom)" "('a acom)" 'a |
|
14 ("(IF _/ THEN _/ ELSE _//{_})" [0, 0, 61, 0] 61) | |
|
15 While 'a bexp "('a acom)" 'a |
|
16 ("({_}//WHILE _/ DO (_)//{_})" [0, 0, 61, 0] 61) |
|
17 |
|
18 fun post :: "'a acom \<Rightarrow>'a" where |
|
19 "post (SKIP {P}) = P" | |
|
20 "post (x ::= e {P}) = P" | |
|
21 "post (c1;; c2) = post c2" | |
|
22 "post (IF b THEN c1 ELSE c2 {P}) = P" | |
|
23 "post ({Inv} WHILE b DO c {P}) = P" |
|
24 |
|
25 fun strip :: "'a acom \<Rightarrow> com" where |
|
26 "strip (SKIP {P}) = com.SKIP" | |
|
27 "strip (x ::= e {P}) = (x ::= e)" | |
|
28 "strip (c1;;c2) = (strip c1;; strip c2)" | |
|
29 "strip (IF b THEN c1 ELSE c2 {P}) = (IF b THEN strip c1 ELSE strip c2)" | |
|
30 "strip ({Inv} WHILE b DO c {P}) = (WHILE b DO strip c)" |
|
31 |
|
32 fun anno :: "'a \<Rightarrow> com \<Rightarrow> 'a acom" where |
|
33 "anno a com.SKIP = SKIP {a}" | |
|
34 "anno a (x ::= e) = (x ::= e {a})" | |
|
35 "anno a (c1;;c2) = (anno a c1;; anno a c2)" | |
|
36 "anno a (IF b THEN c1 ELSE c2) = |
|
37 (IF b THEN anno a c1 ELSE anno a c2 {a})" | |
|
38 "anno a (WHILE b DO c) = |
|
39 ({a} WHILE b DO anno a c {a})" |
|
40 |
|
41 fun annos :: "'a acom \<Rightarrow> 'a list" where |
|
42 "annos (SKIP {a}) = [a]" | |
|
43 "annos (x::=e {a}) = [a]" | |
|
44 "annos (C1;;C2) = annos C1 @ annos C2" | |
|
45 "annos (IF b THEN C1 ELSE C2 {a}) = a # annos C1 @ annos C2" | |
|
46 "annos ({i} WHILE b DO C {a}) = i # a # annos C" |
|
47 |
|
48 fun map_acom :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a acom \<Rightarrow> 'b acom" where |
|
49 "map_acom f (SKIP {P}) = SKIP {f P}" | |
|
50 "map_acom f (x ::= e {P}) = (x ::= e {f P})" | |
|
51 "map_acom f (c1;;c2) = (map_acom f c1;; map_acom f c2)" | |
|
52 "map_acom f (IF b THEN c1 ELSE c2 {P}) = |
|
53 (IF b THEN map_acom f c1 ELSE map_acom f c2 {f P})" | |
|
54 "map_acom f ({Inv} WHILE b DO c {P}) = |
|
55 ({f Inv} WHILE b DO map_acom f c {f P})" |
|
56 |
|
57 |
|
58 lemma post_map_acom[simp]: "post(map_acom f c) = f(post c)" |
|
59 by (induction c) simp_all |
|
60 |
|
61 lemma strip_acom[simp]: "strip (map_acom f c) = strip c" |
|
62 by (induction c) auto |
|
63 |
|
64 lemma map_acom_SKIP: |
|
65 "map_acom f c = SKIP {S'} \<longleftrightarrow> (\<exists>S. c = SKIP {S} \<and> S' = f S)" |
|
66 by (cases c) auto |
|
67 |
|
68 lemma map_acom_Assign: |
|
69 "map_acom f c = x ::= e {S'} \<longleftrightarrow> (\<exists>S. c = x::=e {S} \<and> S' = f S)" |
|
70 by (cases c) auto |
|
71 |
|
72 lemma map_acom_Seq: |
|
73 "map_acom f c = c1';;c2' \<longleftrightarrow> |
|
74 (\<exists>c1 c2. c = c1;;c2 \<and> map_acom f c1 = c1' \<and> map_acom f c2 = c2')" |
|
75 by (cases c) auto |
|
76 |
|
77 lemma map_acom_If: |
|
78 "map_acom f c = IF b THEN c1' ELSE c2' {S'} \<longleftrightarrow> |
|
79 (\<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)" |
|
80 by (cases c) auto |
|
81 |
|
82 lemma map_acom_While: |
|
83 "map_acom f w = {I'} WHILE b DO c' {P'} \<longleftrightarrow> |
|
84 (\<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)" |
|
85 by (cases w) auto |
|
86 |
|
87 |
|
88 lemma strip_anno[simp]: "strip (anno a c) = c" |
|
89 by(induct c) simp_all |
|
90 |
|
91 lemma strip_eq_SKIP: |
|
92 "strip c = com.SKIP \<longleftrightarrow> (EX P. c = SKIP {P})" |
|
93 by (cases c) simp_all |
|
94 |
|
95 lemma strip_eq_Assign: |
|
96 "strip c = x::=e \<longleftrightarrow> (EX P. c = x::=e {P})" |
|
97 by (cases c) simp_all |
|
98 |
|
99 lemma strip_eq_Seq: |
|
100 "strip c = c1;;c2 \<longleftrightarrow> (EX d1 d2. c = d1;;d2 & strip d1 = c1 & strip d2 = c2)" |
|
101 by (cases c) simp_all |
|
102 |
|
103 lemma strip_eq_If: |
|
104 "strip c = IF b THEN c1 ELSE c2 \<longleftrightarrow> |
|
105 (EX d1 d2 P. c = IF b THEN d1 ELSE d2 {P} & strip d1 = c1 & strip d2 = c2)" |
|
106 by (cases c) simp_all |
|
107 |
|
108 lemma strip_eq_While: |
|
109 "strip c = WHILE b DO c1 \<longleftrightarrow> |
|
110 (EX I d1 P. c = {I} WHILE b DO d1 {P} & strip d1 = c1)" |
|
111 by (cases c) simp_all |
|
112 |
|
113 |
|
114 lemma set_annos_anno[simp]: "set (annos (anno a C)) = {a}" |
|
115 by(induction C)(auto) |
|
116 |
|
117 lemma size_annos_same: "strip C1 = strip C2 \<Longrightarrow> size(annos C1) = size(annos C2)" |
|
118 apply(induct C2 arbitrary: C1) |
|
119 apply (auto simp: strip_eq_SKIP strip_eq_Assign strip_eq_Seq strip_eq_If strip_eq_While) |
|
120 done |
|
121 |
|
122 lemmas size_annos_same2 = eqTrueI[OF size_annos_same] |
|
123 |
|
124 |
|
125 end |
|