--- a/thys/turing_basic.thy Sat Jan 19 14:44:07 2013 +0000
+++ b/thys/turing_basic.thy Sat Jan 19 15:27:21 2013 +0000
@@ -95,6 +95,65 @@
shows "steps c p (m + n) = steps (steps c p m) p n"
by (induct m arbitrary: c) (auto)
+lemma step_0 [simp]:
+ shows "step (0, (l, r)) p = (0, (l, r))"
+by (case_tac p, simp)
+
+lemma steps_0 [simp]:
+ shows "steps (0, (l, r)) p n = (0, (l, r))"
+by (induct n) (simp_all)
+
+
+
+fun
+ is_final :: "config \<Rightarrow> bool"
+where
+ "is_final (s, l, r) = (s = 0)"
+
+lemma is_final_eq:
+ shows "is_final (s, tp) = (s = 0)"
+by (case_tac tp) (auto)
+
+lemma is_final_steps:
+ assumes "is_final (s, l, r)"
+ shows "is_final (steps (s, l, r) (p, off) n)"
+using assms
+by (induct n) (auto)
+
+
+(* if the machine is in the halting state, there must have
+ been a state just before the halting state *)
+lemma before_final:
+ assumes "steps0 (1, tp) A n = (0, tp')"
+ shows "\<exists> n'. \<not> is_final (steps0 (1, tp) A n') \<and> steps0 (1, tp) A (Suc n') = (0, tp')"
+using assms
+proof(induct n arbitrary: tp')
+ case (0 tp')
+ have asm: "steps0 (1, tp) A 0 = (0, tp')" by fact
+ then show "\<exists>n'. \<not> is_final (steps0 (1, tp) A n') \<and> steps0 (1, tp) A (Suc n') = (0, tp')"
+ by simp
+next
+ case (Suc n tp')
+ have ih: "\<And>tp'. steps0 (1, tp) A n = (0, tp') \<Longrightarrow>
+ \<exists>n'. \<not> is_final (steps0 (1, tp) A n') \<and> steps0 (1, tp) A (Suc n') = (0, tp')" by fact
+ have asm: "steps0 (1, tp) A (Suc n) = (0, tp')" by fact
+ obtain s l r where cases: "steps0 (1, tp) A n = (s, l, r)"
+ by (auto intro: is_final.cases)
+ then show "\<exists>n'. \<not> is_final (steps0 (1, tp) A n') \<and> steps0 (1, tp) A (Suc n') = (0, tp')"
+ proof (cases "s = 0")
+ case True (* in halting state *)
+ then have "steps0 (1, tp) A n = (0, tp')"
+ using asm cases by (simp del: steps.simps)
+ then show ?thesis using ih by simp
+ next
+ case False (* not in halting state *)
+ then have "\<not> is_final (steps0 (1, tp) A n) \<and> steps0 (1, tp) A (Suc n) = (0, tp')"
+ using asm cases by simp
+ then show ?thesis by auto
+ qed
+qed
+
+(* well-formedness of Turing machine programs *)
fun
tm_wf :: "tprog \<Rightarrow> bool"
where
@@ -135,117 +194,54 @@
"adjust p = map (\<lambda> (a, s). (a, if s = 0 then (Suc (length p div 2)) else s)) p"
lemma length_shift [simp]:
- "length (shift p n) = length p"
+ shows "length (shift p n) = length p"
by simp
-lemma length_adjust[simp]:
+lemma length_adjust [simp]:
shows "length (adjust p) = length p"
by (induct p) (auto)
+
+(* composition of two Turing machines *)
fun
tm_comp :: "instr list \<Rightarrow> instr list \<Rightarrow> instr list" ("_ |+| _" [0, 0] 100)
where
"tm_comp p1 p2 = ((adjust p1) @ (shift p2 (length p1 div 2)))"
-lemma step_0 [simp]:
- shows "step (0, (l, r)) p = (0, (l, r))"
-by (case_tac p, simp)
-
-lemma steps_0 [simp]:
- shows "steps (0, (l, r)) p n = (0, (l, r))"
-by (induct n) (simp_all)
-
-fun
- is_final :: "config \<Rightarrow> bool"
-where
- "is_final (s, l, r) = (s = 0)"
-
-lemma is_final_steps:
- assumes "is_final (s, l, r)"
- shows "is_final (steps (s, l, r) (p, off) n)"
-using assms by (induct n) (auto)
-
-
-
-(* if the machine is in the halting state, there must have
- been a state just before the halting state *)
-lemma before_final:
- assumes "steps0 (1, tp) A n = (0, tp')"
- shows "\<exists> n'. \<not> is_final (steps0 (1, tp) A n') \<and> steps0 (1, tp) A (Suc n') = (0, tp')"
-using assms
-proof(induct n arbitrary: tp')
- case (0 tp')
- have asm: "steps0 (1, tp) A 0 = (0, tp')" by fact
- then show "\<exists>n'. \<not> is_final (steps0 (1, tp) A n') \<and> steps0 (1, tp) A (Suc n') = (0, tp')"
- by simp
-next
- case (Suc n tp')
- have ih: "\<And>tp'. steps0 (1, tp) A n = (0, tp') \<Longrightarrow>
- \<exists>n'. \<not> is_final (steps0 (1, tp) A n') \<and> steps0 (1, tp) A (Suc n') = (0, tp')" by fact
- have asm: "steps0 (1, tp) A (Suc n) = (0, tp')" by fact
- obtain s l r where cases: "steps0 (1, tp) A n = (s, l, r)"
- by (auto intro: is_final.cases)
- then show "\<exists>n'. \<not> is_final (steps0 (1, tp) A n') \<and> steps0 (1, tp) A (Suc n') = (0, tp')"
- proof (cases "s = 0")
- case True (* in halting state *)
- then have "steps0 (1, tp) A n = (0, tp')"
- using asm cases by (simp del: steps.simps)
- then show ?thesis using ih by simp
- next
- case False (* not in halting state *)
- then have "\<not> is_final (steps0 (1, tp) A n) \<and> steps0 (1, tp) A (Suc n) = (0, tp')"
- using asm cases by simp
- then show ?thesis by auto
- qed
-qed
-
-
-lemma length_comp:
+lemma tm_comp_length:
shows "length (A |+| B) = length A + length B"
by auto
-declare steps.simps[simp del]
-declare tm_comp.simps [simp del] adjust.simps[simp del] shift.simps[simp del]
-
-
-lemma tmcomp_fetch_in_first:
+lemma tm_comp_fetch_in_first:
assumes "case (fetch A a x) of (ac, ns) \<Rightarrow> ns \<noteq> 0"
shows "fetch (A |+| B) a x = fetch A a x"
using assms
-apply(case_tac a, case_tac [!] x,
-auto simp: length_comp tm_comp.simps length_adjust nth_append)
-apply(simp_all add: adjust.simps)
-done
-
-
-lemma is_final_eq: "is_final (ba, tp) = (ba = 0)"
-apply(case_tac tp, simp add: is_final.simps)
+apply(case_tac a)
+apply(case_tac [!] x)
+apply(auto simp: tm_comp_length nth_append)
done
lemma t_merge_pre_eq_step:
- assumes step: "step (a, b, c) (A, 0) = cf"
+ assumes step: "step0 (s, l, r) A = cf"
and tm_wf: "tm_wf (A, 0)"
and unfinal: "\<not> is_final cf"
- shows "step (a, b, c) (A |+| B, 0) = cf"
+ shows "step0 (s, l, r) (A |+| B) = cf"
proof -
- have "fetch (A |+| B) a (read c) = fetch A a (read c)"
- proof(rule_tac tmcomp_fetch_in_first)
- from step and unfinal show "case fetch A a (read c) of (ac, ns) \<Rightarrow> ns \<noteq> 0"
- apply(auto simp: is_final.simps)
- apply(case_tac "fetch A a (read c)", simp_all add: is_final_eq)
- done
- qed
- thus "?thesis"
- using step
- apply(auto simp: step.simps is_final.simps)
- done
+ from step unfinal
+ have "\<not> is_final (step0 (s, l, r) A)" by simp
+ then have "fetch (A |+| B) s (read r) = fetch A s (read r)"
+ by (rule_tac tm_comp_fetch_in_first) (auto simp add: is_final_eq)
+ then show ?thesis
+ using step by auto
qed
+declare steps.simps[simp del]
+declare tm_comp.simps [simp del] adjust.simps[simp del] shift.simps[simp del]
declare tm_wf.simps[simp del] step.simps[simp del]
lemma t_merge_pre_eq:
- "\<lbrakk>steps (Suc 0, tp) (A, 0) stp = cf; \<not> is_final cf; tm_wf (A, 0)\<rbrakk>
- \<Longrightarrow> steps (Suc 0, tp) (A |+| B, 0) stp = cf"
+ "\<lbrakk>steps0 (Suc 0, tp) A stp = cf; \<not> is_final cf; tm_wf (A, 0)\<rbrakk>
+ \<Longrightarrow> steps0 (Suc 0, tp) (A |+| B) stp = cf"
proof(induct stp arbitrary: cf, simp add: steps.simps)
fix stp cf
assume ind: "\<And>cf. \<lbrakk>steps (Suc 0, tp) (A, 0) stp = cf; \<not> is_final cf; tm_wf (A, 0)\<rbrakk>
@@ -280,7 +276,7 @@
shows "fetch (A |+| B) a x = (ac, Suc (length A div 2))"
using assms
apply(case_tac a, case_tac [!] x,
-auto simp: length_comp tm_comp.simps length_adjust nth_append)
+auto simp: tm_comp_length tm_comp.simps length_adjust nth_append)
apply(simp_all add: adjust.simps)
done
@@ -376,7 +372,7 @@
\<Longrightarrow> fetch (A |+| B) (sa' + (length A div 2)) x = (a, 0)"
apply(case_tac x)
apply(case_tac [!] sa',
- auto simp: fetch.simps length_comp length_adjust nth_append tm_comp.simps
+ auto simp: fetch.simps tm_comp_length length_adjust nth_append tm_comp.simps
tm_wf.simps shift.simps split: if_splits)
done
@@ -385,7 +381,7 @@
\<Longrightarrow> fetch (A |+| B) (sa + length A div 2) x = (a, s + length A div 2)"
apply(case_tac x)
apply(case_tac [!] sa,
- auto simp: fetch.simps length_comp length_adjust nth_append tm_comp.simps
+ auto simp: fetch.simps tm_comp_length length_adjust nth_append tm_comp.simps
tm_wf.simps shift.simps split: if_splits)
done
--- a/thys/turing_hoare.thy Sat Jan 19 14:44:07 2013 +0000
+++ b/thys/turing_hoare.thy Sat Jan 19 15:27:21 2013 +0000
@@ -2,8 +2,6 @@
imports turing_basic
begin
-
-
type_synonym assert = "tape \<Rightarrow> bool"
definition
@@ -11,8 +9,6 @@
where
"P \<mapsto> Q \<equiv> \<forall>l r. P (l, r) \<longrightarrow> Q (l, r)"
-
-
fun
holds_for :: "(tape \<Rightarrow> bool) \<Rightarrow> config \<Rightarrow> bool" ("_ holds'_for _" [100, 99] 100)
where
@@ -48,8 +44,8 @@
text {*
- {P1} A {Q1} {P2} B {Q2} Q1 \<mapsto> P2
- -----------------------------------
+ {P1} A {Q1} {P2} B {Q2} Q1 \<mapsto> P2 A, B well-formed
+ ------------------------------------------------------
{P1} A |+| B {Q2}
*}
@@ -79,12 +75,12 @@
where "is_final (steps0 (1, l', r') B n2)" and "Q2 holds_for (steps0 (1, l', r') B n2)"
using B_halt unfolding Hoare_def by auto
then obtain l'' r'' where "steps0 (1, l', r') B n2 = (0, l'', r'')" and g: "Q2 holds_for (0, l'', r'')"
- by (case_tac "steps0 (1, l', r') B n2", auto)
+ by (case_tac "steps0 (1, l', r') B n2") (auto)
then have "steps0 (Suc (length A div 2), l', r') (A |+| B) n2 = (0, l'', r'')"
by (rule_tac t_merge_second_halt_same) (auto simp: A_wf B_wf)
ultimately show
"\<exists>n. is_final (steps0 (1, l, r) (A |+| B) n) \<and> Q2 holds_for (steps0 (1, l, r) (A |+| B) n)"
- using g
+ using g
apply(rule_tac x = "stpa + n2" in exI)
apply(simp add: steps_add)
done
@@ -93,8 +89,7 @@
definition
Hoare_unhalt :: "assert \<Rightarrow> tprog0 \<Rightarrow> bool" ("({(1_)}/ (_))" 50)
where
- "{P} p \<equiv>
- (\<forall>l r. P (l, r) \<longrightarrow> (\<forall> n . \<not> (is_final (steps0 (1, (l, r)) p n))))"
+ "{P} p \<equiv> (\<forall>l r. P (l, r) \<longrightarrow> (\<forall> n . \<not> (is_final (steps0 (1, (l, r)) p n))))"
lemma Hoare_unhalt_I:
assumes "\<And>l r. P (l, r) \<Longrightarrow> \<forall> n. \<not> is_final (steps0 (1, (l, r)) p n)"