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