|
1 theory Finite_Reachable |
|
2 imports Small_Step |
|
3 begin |
|
4 |
|
5 subsection "Finite number of reachable commands" |
|
6 |
|
7 text{* This theory shows that in the small-step semantics one can only reach |
|
8 a finite number of commands from any given command. Hence one can see the |
|
9 command component of a small-step configuration as a combination of the |
|
10 program to be executed and a pc. *} |
|
11 |
|
12 definition reachable :: "com \<Rightarrow> com set" where |
|
13 "reachable c = {c'. \<exists>s t. (c,s) \<rightarrow>* (c',t)}" |
|
14 |
|
15 text{* Proofs need induction on the length of a small-step reduction sequence. *} |
|
16 |
|
17 fun small_stepsn :: "com * state \<Rightarrow> nat \<Rightarrow> com * state \<Rightarrow> bool" |
|
18 ("_ \<rightarrow>'(_') _" [55,0,55] 55) where |
|
19 "(cs \<rightarrow>(0) cs') = (cs' = cs)" | |
|
20 "cs \<rightarrow>(Suc n) cs'' = (\<exists>cs'. cs \<rightarrow> cs' \<and> cs' \<rightarrow>(n) cs'')" |
|
21 |
|
22 lemma stepsn_if_star: "cs \<rightarrow>* cs' \<Longrightarrow> \<exists>n. cs \<rightarrow>(n) cs'" |
|
23 proof(induction rule: star.induct) |
|
24 case refl show ?case by (metis small_stepsn.simps(1)) |
|
25 next |
|
26 case step thus ?case by (metis small_stepsn.simps(2)) |
|
27 qed |
|
28 |
|
29 lemma star_if_stepsn: "cs \<rightarrow>(n) cs' \<Longrightarrow> cs \<rightarrow>* cs'" |
|
30 by(induction n arbitrary: cs) (auto elim: star.step) |
|
31 |
|
32 lemma SKIP_starD: "(SKIP, s) \<rightarrow>* (c,t) \<Longrightarrow> c = SKIP" |
|
33 by(induction SKIP s c t rule: star_induct) auto |
|
34 |
|
35 lemma reachable_SKIP: "reachable SKIP = {SKIP}" |
|
36 by(auto simp: reachable_def dest: SKIP_starD) |
|
37 |
|
38 |
|
39 lemma Assign_starD: "(x::=a, s) \<rightarrow>* (c,t) \<Longrightarrow> c \<in> {x::=a, SKIP}" |
|
40 by (induction "x::=a" s c t rule: star_induct) (auto dest: SKIP_starD) |
|
41 |
|
42 lemma reachable_Assign: "reachable (x::=a) = {x::=a, SKIP}" |
|
43 by(auto simp: reachable_def dest:Assign_starD) |
|
44 |
|
45 |
|
46 lemma Seq_stepsnD: "(c1; c2, s) \<rightarrow>(n) (c', t) \<Longrightarrow> |
|
47 (\<exists>c1' m. c' = c1'; c2 \<and> (c1, s) \<rightarrow>(m) (c1', t) \<and> m \<le> n) \<or> |
|
48 (\<exists>s2 m1 m2. (c1,s) \<rightarrow>(m1) (SKIP,s2) \<and> (c2, s2) \<rightarrow>(m2) (c', t) \<and> m1+m2 < n)" |
|
49 proof(induction n arbitrary: c1 c2 s) |
|
50 case 0 thus ?case by auto |
|
51 next |
|
52 case (Suc n) |
|
53 from Suc.prems obtain s' c12' where "(c1;c2, s) \<rightarrow> (c12', s')" |
|
54 and n: "(c12',s') \<rightarrow>(n) (c',t)" by auto |
|
55 from this(1) show ?case |
|
56 proof |
|
57 assume "c1 = SKIP" "(c12', s') = (c2, s)" |
|
58 hence "(c1,s) \<rightarrow>(0) (SKIP, s') \<and> (c2, s') \<rightarrow>(n) (c', t) \<and> 0 + n < Suc n" |
|
59 using n by auto |
|
60 thus ?case by blast |
|
61 next |
|
62 fix c1' s'' assume 1: "(c12', s') = (c1'; c2, s'')" "(c1, s) \<rightarrow> (c1', s'')" |
|
63 hence n': "(c1';c2,s') \<rightarrow>(n) (c',t)" using n by auto |
|
64 from Suc.IH[OF n'] show ?case |
|
65 proof |
|
66 assume "\<exists>c1'' m. c' = c1''; c2 \<and> (c1', s') \<rightarrow>(m) (c1'', t) \<and> m \<le> n" |
|
67 (is "\<exists> a b. ?P a b") |
|
68 then obtain c1'' m where 2: "?P c1'' m" by blast |
|
69 hence "c' = c1'';c2 \<and> (c1, s) \<rightarrow>(Suc m) (c1'',t) \<and> Suc m \<le> Suc n" |
|
70 using 1 by auto |
|
71 thus ?case by blast |
|
72 next |
|
73 assume "\<exists>s2 m1 m2. (c1',s') \<rightarrow>(m1) (SKIP,s2) \<and> |
|
74 (c2,s2) \<rightarrow>(m2) (c',t) \<and> m1+m2 < n" (is "\<exists>a b c. ?P a b c") |
|
75 then obtain s2 m1 m2 where "?P s2 m1 m2" by blast |
|
76 hence "(c1,s) \<rightarrow>(Suc m1) (SKIP,s2) \<and> (c2,s2) \<rightarrow>(m2) (c',t) \<and> |
|
77 Suc m1 + m2 < Suc n" using 1 by auto |
|
78 thus ?case by blast |
|
79 qed |
|
80 qed |
|
81 qed |
|
82 |
|
83 corollary Seq_starD: "(c1; c2, s) \<rightarrow>* (c', t) \<Longrightarrow> |
|
84 (\<exists>c1'. c' = c1'; c2 \<and> (c1, s) \<rightarrow>* (c1', t)) \<or> |
|
85 (\<exists>s2. (c1,s) \<rightarrow>* (SKIP,s2) \<and> (c2, s2) \<rightarrow>* (c', t))" |
|
86 by(metis Seq_stepsnD star_if_stepsn stepsn_if_star) |
|
87 |
|
88 lemma reachable_Seq: "reachable (c1;c2) \<subseteq> |
|
89 (\<lambda>c1'. c1';c2) ` reachable c1 \<union> reachable c2" |
|
90 by(auto simp: reachable_def image_def dest!: Seq_starD) |
|
91 |
|
92 |
|
93 lemma If_starD: "(IF b THEN c1 ELSE c2, s) \<rightarrow>* (c,t) \<Longrightarrow> |
|
94 c = IF b THEN c1 ELSE c2 \<or> (c1,s) \<rightarrow>* (c,t) \<or> (c2,s) \<rightarrow>* (c,t)" |
|
95 by(induction "IF b THEN c1 ELSE c2" s c t rule: star_induct) auto |
|
96 |
|
97 lemma reachable_If: "reachable (IF b THEN c1 ELSE c2) \<subseteq> |
|
98 {IF b THEN c1 ELSE c2} \<union> reachable c1 \<union> reachable c2" |
|
99 by(auto simp: reachable_def dest!: If_starD) |
|
100 |
|
101 |
|
102 lemma While_stepsnD: "(WHILE b DO c, s) \<rightarrow>(n) (c2,t) \<Longrightarrow> |
|
103 c2 \<in> {WHILE b DO c, IF b THEN c ; WHILE b DO c ELSE SKIP, SKIP} |
|
104 \<or> (\<exists>c1. c2 = c1 ; WHILE b DO c \<and> (\<exists> s1 s2. (c,s1) \<rightarrow>* (c1,s2)))" |
|
105 proof(induction n arbitrary: s rule: less_induct) |
|
106 case (less n1) |
|
107 show ?case |
|
108 proof(cases n1) |
|
109 case 0 thus ?thesis using less.prems by (simp) |
|
110 next |
|
111 case (Suc n2) |
|
112 let ?w = "WHILE b DO c" |
|
113 let ?iw = "IF b THEN c ; ?w ELSE SKIP" |
|
114 from Suc less.prems have n2: "(?iw,s) \<rightarrow>(n2) (c2,t)" by(auto elim!: WhileE) |
|
115 show ?thesis |
|
116 proof(cases n2) |
|
117 case 0 thus ?thesis using n2 by auto |
|
118 next |
|
119 case (Suc n3) |
|
120 then obtain iw' s' where "(?iw,s) \<rightarrow> (iw',s')" |
|
121 and n3: "(iw',s') \<rightarrow>(n3) (c2,t)" using n2 by auto |
|
122 from this(1) |
|
123 show ?thesis |
|
124 proof |
|
125 assume "(iw', s') = (c; WHILE b DO c, s)" |
|
126 with n3 have "(c;?w, s) \<rightarrow>(n3) (c2,t)" by auto |
|
127 from Seq_stepsnD[OF this] show ?thesis |
|
128 proof |
|
129 assume "\<exists>c1' m. c2 = c1'; ?w \<and> (c,s) \<rightarrow>(m) (c1', t) \<and> m \<le> n3" |
|
130 thus ?thesis by (metis star_if_stepsn) |
|
131 next |
|
132 assume "\<exists>s2 m1 m2. (c, s) \<rightarrow>(m1) (SKIP, s2) \<and> |
|
133 (WHILE b DO c, s2) \<rightarrow>(m2) (c2, t) \<and> m1 + m2 < n3" (is "\<exists>x y z. ?P x y z") |
|
134 then obtain s2 m1 m2 where "?P s2 m1 m2" by blast |
|
135 with `n2 = Suc n3` `n1 = Suc n2`have "m2 < n1" by arith |
|
136 from less.IH[OF this] `?P s2 m1 m2` show ?thesis by blast |
|
137 qed |
|
138 next |
|
139 assume "(iw', s') = (SKIP, s)" |
|
140 thus ?thesis using star_if_stepsn[OF n3] by(auto dest!: SKIP_starD) |
|
141 qed |
|
142 qed |
|
143 qed |
|
144 qed |
|
145 |
|
146 lemma reachable_While: "reachable (WHILE b DO c) \<subseteq> |
|
147 {WHILE b DO c, IF b THEN c ; WHILE b DO c ELSE SKIP, SKIP} \<union> |
|
148 (\<lambda>c'. c' ; WHILE b DO c) ` reachable c" |
|
149 apply(auto simp: reachable_def image_def) |
|
150 by (metis While_stepsnD insertE singletonE stepsn_if_star) |
|
151 |
|
152 |
|
153 theorem finite_reachable: "finite(reachable c)" |
|
154 apply(induction c) |
|
155 apply(auto simp: reachable_SKIP reachable_Assign |
|
156 finite_subset[OF reachable_Seq] finite_subset[OF reachable_If] |
|
157 finite_subset[OF reachable_While]) |
|
158 done |
|
159 |
|
160 |
|
161 end |