109 |
109 |
110 lemma is_final_eq: |
110 lemma is_final_eq: |
111 shows "is_final (s, tp) = (s = 0)" |
111 shows "is_final (s, tp) = (s = 0)" |
112 by (case_tac tp) (auto) |
112 by (case_tac tp) (auto) |
113 |
113 |
|
114 lemma is_finalI [intro]: |
|
115 shows "is_final (0, tp)" |
|
116 by (simp add: is_final_eq) |
|
117 |
114 lemma after_is_final: |
118 lemma after_is_final: |
115 assumes "is_final c" |
119 assumes "is_final c" |
116 shows "is_final (steps c p n)" |
120 shows "is_final (steps c p n)" |
117 using assms |
121 using assms |
118 apply(induct n) |
122 apply(induct n) |
119 apply(case_tac [!] c) |
123 apply(case_tac [!] c) |
120 apply(auto) |
124 apply(auto) |
121 done |
125 done |
|
126 |
|
127 lemma is_final: |
|
128 assumes a: "is_final (steps c p n1)" |
|
129 and b: "n1 \<le> n2" |
|
130 shows "is_final (steps c p n2)" |
|
131 proof - |
|
132 obtain n3 where eq: "n2 = n1 + n3" using b by (metis le_iff_add) |
|
133 from a show "is_final (steps c p n2)" unfolding eq |
|
134 by (simp add: after_is_final) |
|
135 qed |
122 |
136 |
123 lemma not_is_final: |
137 lemma not_is_final: |
124 assumes a: "\<not> is_final (steps c p n1)" |
138 assumes a: "\<not> is_final (steps c p n1)" |
125 and b: "n2 \<le> n1" |
139 and b: "n2 \<le> n1" |
126 shows "\<not> is_final (steps c p n2)" |
140 shows "\<not> is_final (steps c p n2)" |
162 using asm cases by simp |
176 using asm cases by simp |
163 then show ?thesis by auto |
177 then show ?thesis by auto |
164 qed |
178 qed |
165 qed |
179 qed |
166 |
180 |
|
181 lemma least_steps: |
|
182 assumes "steps0 (1, tp) A n = (0, tp')" |
|
183 shows "\<exists> n'. (\<forall>n'' < n'. \<not> is_final (steps0 (1, tp) A n'')) \<and> |
|
184 (\<forall>n'' \<ge> n'. is_final (steps0 (1, tp) A n''))" |
|
185 proof - |
|
186 from before_final[OF assms] |
|
187 obtain n' where |
|
188 before: "\<not> is_final (steps0 (1, tp) A n')" and |
|
189 final: "steps0 (1, tp) A (Suc n') = (0, tp')" by auto |
|
190 from before |
|
191 have "\<forall>n'' < Suc n'. \<not> is_final (steps0 (1, tp) A n'')" |
|
192 using not_is_final by auto |
|
193 moreover |
|
194 from final |
|
195 have "\<forall>n'' \<ge> Suc n'. is_final (steps0 (1, tp) A n'')" |
|
196 using is_final[of _ _ "Suc n'"] by (auto simp add: is_final_eq) |
|
197 ultimately |
|
198 show "\<exists> n'. (\<forall>n'' < n'. \<not> is_final (steps0 (1, tp) A n'')) \<and> (\<forall>n'' \<ge> n'. is_final (steps0 (1, tp) A n''))" |
|
199 by blast |
|
200 qed |
|
201 |
|
202 |
|
203 |
167 (* well-formedness of Turing machine programs *) |
204 (* well-formedness of Turing machine programs *) |
168 abbreviation "is_even n \<equiv> (n::nat) mod 2 = 0" |
205 abbreviation "is_even n \<equiv> (n::nat) mod 2 = 0" |
169 |
206 |
170 fun |
207 fun |
171 tm_wf :: "tprog \<Rightarrow> bool" |
208 tm_wf :: "tprog \<Rightarrow> bool" |