1(* Author: Tobias Nipkow *)
2
3theory ACom
4imports Com
5begin
6
7subsection "Annotated Commands"
8
9datatype '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 "('a acom)" 'a "('a acom)" 'a
14    ("(IF _/ THEN ({_}/ _)/ ELSE ({_}/ _)//{_})"  [0, 0, 0, 61, 0, 0] 61) |
15  While 'a bexp 'a "('a acom)" 'a
16    ("({_}//WHILE _//DO ({_}//_)//{_})"  [0, 0, 0, 61, 0] 61)
17
18notation com.SKIP ("SKIP")
19
20text_raw\<open>\snip{stripdef}{1}{1}{%\<close>
21fun strip :: "'a acom \<Rightarrow> com" where
22"strip (SKIP {P}) = SKIP" |
23"strip (x ::= e {P}) = x ::= e" |
24"strip (C\<^sub>1;;C\<^sub>2) = strip C\<^sub>1;; strip C\<^sub>2" |
25"strip (IF b THEN {P\<^sub>1} C\<^sub>1 ELSE {P\<^sub>2} C\<^sub>2 {P}) =
26  IF b THEN strip C\<^sub>1 ELSE strip C\<^sub>2" |
27"strip ({I} WHILE b DO {P} C {Q}) = WHILE b DO strip C"
28text_raw\<open>}%endsnip\<close>
29
30text_raw\<open>\snip{asizedef}{1}{1}{%\<close>
31fun asize :: "com \<Rightarrow> nat" where
32"asize SKIP = 1" |
33"asize (x ::= e) = 1" |
34"asize (C\<^sub>1;;C\<^sub>2) = asize C\<^sub>1 + asize C\<^sub>2" |
35"asize (IF b THEN C\<^sub>1 ELSE C\<^sub>2) = asize C\<^sub>1 + asize C\<^sub>2 + 3" |
36"asize (WHILE b DO C) = asize C + 3"
37text_raw\<open>}%endsnip\<close>
38
39text_raw\<open>\snip{annotatedef}{1}{1}{%\<close>
40definition shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a" where
41"shift f n = (\<lambda>p. f(p+n))"
42
43fun annotate :: "(nat \<Rightarrow> 'a) \<Rightarrow> com \<Rightarrow> 'a acom" where
44"annotate f SKIP = SKIP {f 0}" |
45"annotate f (x ::= e) = x ::= e {f 0}" |
46"annotate f (c\<^sub>1;;c\<^sub>2) = annotate f c\<^sub>1;; annotate (shift f (asize c\<^sub>1)) c\<^sub>2" |
47"annotate f (IF b THEN c\<^sub>1 ELSE c\<^sub>2) =
48  IF b THEN {f 0} annotate (shift f 1) c\<^sub>1
49  ELSE {f(asize c\<^sub>1 + 1)} annotate (shift f (asize c\<^sub>1 + 2)) c\<^sub>2
50  {f(asize c\<^sub>1 + asize c\<^sub>2 + 2)}" |
51"annotate f (WHILE b DO c) =
52  {f 0} WHILE b DO {f 1} annotate (shift f 2) c {f(asize c + 2)}"
53text_raw\<open>}%endsnip\<close>
54
55text_raw\<open>\snip{annosdef}{1}{1}{%\<close>
56fun annos :: "'a acom \<Rightarrow> 'a list" where
57"annos (SKIP {P}) = [P]" |
58"annos (x ::= e {P}) = [P]" |
59"annos (C\<^sub>1;;C\<^sub>2) = annos C\<^sub>1 @ annos C\<^sub>2" |
60"annos (IF b THEN {P\<^sub>1} C\<^sub>1 ELSE {P\<^sub>2} C\<^sub>2 {Q}) =
61  P\<^sub>1 # annos C\<^sub>1 @  P\<^sub>2 # annos C\<^sub>2 @ [Q]" |
62"annos ({I} WHILE b DO {P} C {Q}) = I # P # annos C @ [Q]"
63text_raw\<open>}%endsnip\<close>
64
65definition anno :: "'a acom \<Rightarrow> nat \<Rightarrow> 'a" where
66"anno C p = annos C ! p"
67
68definition post :: "'a acom \<Rightarrow>'a" where
69"post C = last(annos C)"
70
71text_raw\<open>\snip{mapacomdef}{1}{2}{%\<close>
72fun map_acom :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a acom \<Rightarrow> 'b acom" where
73"map_acom f (SKIP {P}) = SKIP {f P}" |
74"map_acom f (x ::= e {P}) = x ::= e {f P}" |
75"map_acom f (C\<^sub>1;;C\<^sub>2) = map_acom f C\<^sub>1;; map_acom f C\<^sub>2" |
76"map_acom f (IF b THEN {P\<^sub>1} C\<^sub>1 ELSE {P\<^sub>2} C\<^sub>2 {Q}) =
77  IF b THEN {f P\<^sub>1} map_acom f C\<^sub>1 ELSE {f P\<^sub>2} map_acom f C\<^sub>2
78  {f Q}" |
79"map_acom f ({I} WHILE b DO {P} C {Q}) =
80  {f I} WHILE b DO {f P} map_acom f C {f Q}"
81text_raw\<open>}%endsnip\<close>
82
83
84lemma annos_ne: "annos C \<noteq> []"
85by(induction C) auto
86
87lemma strip_annotate[simp]: "strip(annotate f c) = c"
88by(induction c arbitrary: f) auto
89
90lemma length_annos_annotate[simp]: "length (annos (annotate f c)) = asize c"
91by(induction c arbitrary: f) auto
92
93lemma size_annos: "size(annos C) = asize(strip C)"
94by(induction C)(auto)
95
96lemma size_annos_same: "strip C1 = strip C2 \<Longrightarrow> size(annos C1) = size(annos C2)"
97apply(induct C2 arbitrary: C1)
98apply(case_tac C1, simp_all)+
99done
100
101lemmas size_annos_same2 = eqTrueI[OF size_annos_same]
102
103lemma anno_annotate[simp]: "p < asize c \<Longrightarrow> anno (annotate f c) p = f p"
104apply(induction c arbitrary: f p)
105apply (auto simp: anno_def nth_append nth_Cons numeral_eq_Suc shift_def
106            split: nat.split)
107  apply (metis add_Suc_right add_diff_inverse add.commute)
108 apply(rule_tac f=f in arg_cong)
109 apply arith
110apply (metis less_Suc_eq)
111done
112
113lemma eq_acom_iff_strip_annos:
114  "C1 = C2 \<longleftrightarrow> strip C1 = strip C2 \<and> annos C1 = annos C2"
115apply(induction C1 arbitrary: C2)
116apply(case_tac C2, auto simp: size_annos_same2)+
117done
118
119lemma eq_acom_iff_strip_anno:
120  "C1=C2 \<longleftrightarrow> strip C1 = strip C2 \<and> (\<forall>p<size(annos C1). anno C1 p = anno C2 p)"
121by(auto simp add: eq_acom_iff_strip_annos anno_def
122     list_eq_iff_nth_eq size_annos_same2)
123
124lemma post_map_acom[simp]: "post(map_acom f C) = f(post C)"
125by (induction C) (auto simp: post_def last_append annos_ne)
126
127lemma strip_map_acom[simp]: "strip (map_acom f C) = strip C"
128by (induction C) auto
129
130lemma anno_map_acom: "p < size(annos C) \<Longrightarrow> anno (map_acom f C) p = f(anno C p)"
131apply(induction C arbitrary: p)
132apply(auto simp: anno_def nth_append nth_Cons' size_annos)
133done
134
135lemma strip_eq_SKIP:
136  "strip C = SKIP \<longleftrightarrow> (\<exists>P. C = SKIP {P})"
137by (cases C) simp_all
138
139lemma strip_eq_Assign:
140  "strip C = x::=e \<longleftrightarrow> (\<exists>P. C = x::=e {P})"
141by (cases C) simp_all
142
143lemma strip_eq_Seq:
144  "strip C = c1;;c2 \<longleftrightarrow> (\<exists>C1 C2. C = C1;;C2 & strip C1 = c1 & strip C2 = c2)"
145by (cases C) simp_all
146
147lemma strip_eq_If:
148  "strip C = IF b THEN c1 ELSE c2 \<longleftrightarrow>
149  (\<exists>P1 P2 C1 C2 Q. C = IF b THEN {P1} C1 ELSE {P2} C2 {Q} & strip C1 = c1 & strip C2 = c2)"
150by (cases C) simp_all
151
152lemma strip_eq_While:
153  "strip C = WHILE b DO c1 \<longleftrightarrow>
154  (\<exists>I P C1 Q. C = {I} WHILE b DO {P} C1 {Q} & strip C1 = c1)"
155by (cases C) simp_all
156
157lemma [simp]: "shift (\<lambda>p. a) n = (\<lambda>p. a)"
158by(simp add:shift_def)
159
160lemma set_annos_anno[simp]: "set (annos (annotate (\<lambda>p. a) c)) = {a}"
161by(induction c) simp_all
162
163lemma post_in_annos: "post C \<in> set(annos C)"
164by(auto simp: post_def annos_ne)
165
166lemma post_anno_asize: "post C = anno C (size(annos C) - 1)"
167by(simp add: post_def last_conv_nth[OF annos_ne] anno_def)
168
169end
170