11 |
11 |
12 datatype 'a acom = |
12 datatype 'a acom = |
13 SKIP 'a ("SKIP {_}" 61) | |
13 SKIP 'a ("SKIP {_}" 61) | |
14 Assign vname aexp 'a ("(_ ::= _/ {_})" [1000, 61, 0] 61) | |
14 Assign vname aexp 'a ("(_ ::= _/ {_})" [1000, 61, 0] 61) | |
15 Seq "('a acom)" "('a acom)" ("_;//_" [60, 61] 60) | |
15 Seq "('a acom)" "('a acom)" ("_;//_" [60, 61] 60) | |
16 If bexp "('a acom)" "('a acom)" 'a |
16 If bexp 'a "('a acom)" 'a "('a acom)" 'a |
17 ("(IF _/ THEN _/ ELSE _//{_})" [0, 0, 61, 0] 61) | |
17 ("(IF _/ THEN ({_}/ _)/ ELSE ({_}/ _)//{_})" [0, 0, 0, 61, 0, 0] 61) | |
18 While 'a bexp "('a acom)" 'a |
18 While 'a bexp 'a "('a acom)" 'a |
19 ("({_}//WHILE _/ DO (_)//{_})" [0, 0, 61, 0] 61) |
19 ("({_}//WHILE _/ DO ({_}/ _)//{_})" [0, 0, 0, 61, 0] 61) |
20 |
20 |
21 fun post :: "'a acom \<Rightarrow>'a" where |
21 fun post :: "'a acom \<Rightarrow>'a" where |
22 "post (SKIP {P}) = P" | |
22 "post (SKIP {P}) = P" | |
23 "post (x ::= e {P}) = P" | |
23 "post (x ::= e {P}) = P" | |
24 "post (c1; c2) = post c2" | |
24 "post (c1; c2) = post c2" | |
25 "post (IF b THEN c1 ELSE c2 {P}) = P" | |
25 "post (IF b THEN {P1} c1 ELSE {P2} c2 {P}) = P" | |
26 "post ({Inv} WHILE b DO c {P}) = P" |
26 "post ({Inv} WHILE b DO {Pc} c {P}) = P" |
27 |
27 |
28 fun strip :: "'a acom \<Rightarrow> com" where |
28 fun strip :: "'a acom \<Rightarrow> com" where |
29 "strip (SKIP {P}) = com.SKIP" | |
29 "strip (SKIP {P}) = com.SKIP" | |
30 "strip (x ::= e {P}) = (x ::= e)" | |
30 "strip (x ::= e {P}) = (x ::= e)" | |
31 "strip (c1;c2) = (strip c1; strip c2)" | |
31 "strip (c1;c2) = (strip c1; strip c2)" | |
32 "strip (IF b THEN c1 ELSE c2 {P}) = (IF b THEN strip c1 ELSE strip c2)" | |
32 "strip (IF b THEN {P1} c1 ELSE {P2} c2 {P}) = (IF b THEN strip c1 ELSE strip c2)" | |
33 "strip ({Inv} WHILE b DO c {P}) = (WHILE b DO strip c)" |
33 "strip ({Inv} WHILE b DO {Pc} c {P}) = (WHILE b DO strip c)" |
34 |
34 |
35 fun anno :: "'a \<Rightarrow> com \<Rightarrow> 'a acom" where |
35 fun anno :: "'a \<Rightarrow> com \<Rightarrow> 'a acom" where |
36 "anno a com.SKIP = SKIP {a}" | |
36 "anno a com.SKIP = SKIP {a}" | |
37 "anno a (x ::= e) = (x ::= e {a})" | |
37 "anno a (x ::= e) = (x ::= e {a})" | |
38 "anno a (c1;c2) = (anno a c1; anno a c2)" | |
38 "anno a (c1;c2) = (anno a c1; anno a c2)" | |
39 "anno a (IF b THEN c1 ELSE c2) = |
39 "anno a (IF b THEN c1 ELSE c2) = |
40 (IF b THEN anno a c1 ELSE anno a c2 {a})" | |
40 (IF b THEN {a} anno a c1 ELSE {a} anno a c2 {a})" | |
41 "anno a (WHILE b DO c) = |
41 "anno a (WHILE b DO c) = |
42 ({a} WHILE b DO anno a c {a})" |
42 ({a} WHILE b DO {a} anno a c {a})" |
43 |
43 |
44 fun annos :: "'a acom \<Rightarrow> 'a list" where |
44 fun annos :: "'a acom \<Rightarrow> 'a list" where |
45 "annos (SKIP {a}) = [a]" | |
45 "annos (SKIP {a}) = [a]" | |
46 "annos (x::=e {a}) = [a]" | |
46 "annos (x::=e {a}) = [a]" | |
47 "annos (C1;C2) = annos C1 @ annos C2" | |
47 "annos (C1;C2) = annos C1 @ annos C2" | |
48 "annos (IF b THEN C1 ELSE C2 {a}) = a # annos C1 @ annos C2" | |
48 "annos (IF b THEN {a1} C1 ELSE {a2} C2 {a}) = a1 # a2 #a # annos C1 @ annos C2" | |
49 "annos ({i} WHILE b DO C {a}) = i # a # annos C" |
49 "annos ({i} WHILE b DO {ac} C {a}) = i # ac # a # annos C" |
50 |
50 |
51 fun map_acom :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a acom \<Rightarrow> 'b acom" where |
51 fun map_acom :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a acom \<Rightarrow> 'b acom" where |
52 "map_acom f (SKIP {P}) = SKIP {f P}" | |
52 "map_acom f (SKIP {P}) = SKIP {f P}" | |
53 "map_acom f (x ::= e {P}) = (x ::= e {f P})" | |
53 "map_acom f (x ::= e {P}) = (x ::= e {f P})" | |
54 "map_acom f (c1;c2) = (map_acom f c1; map_acom f c2)" | |
54 "map_acom f (c1;c2) = (map_acom f c1; map_acom f c2)" | |
55 "map_acom f (IF b THEN c1 ELSE c2 {P}) = |
55 "map_acom f (IF b THEN {p1} c1 ELSE {p2} c2 {P}) = |
56 (IF b THEN map_acom f c1 ELSE map_acom f c2 {f P})" | |
56 (IF b THEN {f p1} map_acom f c1 ELSE {f p2} map_acom f c2 {f P})" | |
57 "map_acom f ({Inv} WHILE b DO c {P}) = |
57 "map_acom f ({Inv} WHILE b DO {p} c {P}) = |
58 ({f Inv} WHILE b DO map_acom f c {f P})" |
58 ({f Inv} WHILE b DO {f p} map_acom f c {f P})" |
59 |
59 |
60 |
60 |
61 lemma post_map_acom[simp]: "post(map_acom f c) = f(post c)" |
61 lemma post_map_acom[simp]: "post(map_acom f c) = f(post c)" |
62 by (induction c) simp_all |
62 by (induction c) simp_all |
63 |
63 |
76 "map_acom f c = c1';c2' \<longleftrightarrow> |
76 "map_acom f c = c1';c2' \<longleftrightarrow> |
77 (\<exists>c1 c2. c = c1;c2 \<and> map_acom f c1 = c1' \<and> map_acom f c2 = c2')" |
77 (\<exists>c1 c2. c = c1;c2 \<and> map_acom f c1 = c1' \<and> map_acom f c2 = c2')" |
78 by (cases c) auto |
78 by (cases c) auto |
79 |
79 |
80 lemma map_acom_If: |
80 lemma map_acom_If: |
81 "map_acom f c = IF b THEN c1' ELSE c2' {S'} \<longleftrightarrow> |
81 "map_acom f c = IF b THEN {p1'} c1' ELSE {p2'} c2' {S'} \<longleftrightarrow> |
82 (\<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)" |
82 (\<exists>S p1 p2 c1 c2. c = IF b THEN {p1} c1 ELSE {p2} c2 {S} \<and> |
|
83 map_acom f c1 = c1' \<and> map_acom f c2 = c2' \<and> p1' = f p1 \<and> p2' = f p2 \<and> S' = f S)" |
83 by (cases c) auto |
84 by (cases c) auto |
84 |
85 |
85 lemma map_acom_While: |
86 lemma map_acom_While: |
86 "map_acom f w = {I'} WHILE b DO c' {P'} \<longleftrightarrow> |
87 "map_acom f w = {I'} WHILE b DO {p'} c' {P'} \<longleftrightarrow> |
87 (\<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)" |
88 (\<exists>I p P c. w = {I} WHILE b DO {p} c {P} \<and> map_acom f c = c' \<and> I' = f I \<and> p' = f p \<and> P' = f P)" |
88 by (cases w) auto |
89 by (cases w) auto |
89 |
90 |
90 |
91 |
91 lemma strip_anno[simp]: "strip (anno a c) = c" |
92 lemma strip_anno[simp]: "strip (anno a c) = c" |
92 by(induct c) simp_all |
93 by(induct c) simp_all |
93 |
94 |
94 lemma strip_eq_SKIP: |
95 lemma strip_eq_SKIP: |
95 "strip c = com.SKIP \<longleftrightarrow> (EX P. c = SKIP {P})" |
96 "strip C = com.SKIP \<longleftrightarrow> (EX P. C = SKIP {P})" |
96 by (cases c) simp_all |
97 by (cases C) simp_all |
97 |
98 |
98 lemma strip_eq_Assign: |
99 lemma strip_eq_Assign: |
99 "strip c = x::=e \<longleftrightarrow> (EX P. c = x::=e {P})" |
100 "strip C = x::=e \<longleftrightarrow> (EX P. C = x::=e {P})" |
100 by (cases c) simp_all |
101 by (cases C) simp_all |
101 |
102 |
102 lemma strip_eq_Seq: |
103 lemma strip_eq_Seq: |
103 "strip c = c1;c2 \<longleftrightarrow> (EX d1 d2. c = d1;d2 & strip d1 = c1 & strip d2 = c2)" |
104 "strip C = c1;c2 \<longleftrightarrow> (EX C1 C2. C = C1;C2 & strip C1 = c1 & strip C2 = c2)" |
104 by (cases c) simp_all |
105 by (cases C) simp_all |
105 |
106 |
106 lemma strip_eq_If: |
107 lemma strip_eq_If: |
107 "strip c = IF b THEN c1 ELSE c2 \<longleftrightarrow> |
108 "strip C = IF b THEN c1 ELSE c2 \<longleftrightarrow> |
108 (EX d1 d2 P. c = IF b THEN d1 ELSE d2 {P} & strip d1 = c1 & strip d2 = c2)" |
109 (EX p1 p2 C1 C2 P. C = IF b THEN {p1} C1 ELSE {p2} C2 {P} & strip C1 = c1 & strip C2 = c2)" |
109 by (cases c) simp_all |
110 by (cases C) simp_all |
110 |
111 |
111 lemma strip_eq_While: |
112 lemma strip_eq_While: |
112 "strip c = WHILE b DO c1 \<longleftrightarrow> |
113 "strip C = WHILE b DO c1 \<longleftrightarrow> |
113 (EX I d1 P. c = {I} WHILE b DO d1 {P} & strip d1 = c1)" |
114 (EX I p C1 P. C = {I} WHILE b DO {p} C1 {P} & strip C1 = c1)" |
114 by (cases c) simp_all |
115 by (cases C) simp_all |
115 |
|
116 |
116 |
117 lemma set_annos_anno[simp]: "set (annos (anno a C)) = {a}" |
117 lemma set_annos_anno[simp]: "set (annos (anno a C)) = {a}" |
118 by(induction C)(auto) |
118 by(induction C)(auto) |
119 |
119 |
120 lemma size_annos_same: "strip C1 = strip C2 \<Longrightarrow> size(annos C1) = size(annos C2)" |
120 lemma size_annos_same: "strip C1 = strip C2 \<Longrightarrow> size(annos C1) = size(annos C2)" |