--- a/thys/turing_basic.thy Sat Jan 19 12:46:28 2013 +0000
+++ b/thys/turing_basic.thy Sat Jan 19 14:29:56 2013 +0000
@@ -21,6 +21,8 @@
type_synonym tprog = "instr list \<times> nat"
+type_synonym tprog0 = "instr list"
+
type_synonym config = "state \<times> tape"
fun nth_of where
@@ -78,6 +80,13 @@
"steps c p 0 = c" |
"steps c p (Suc n) = steps (step c p) p n"
+
+abbreviation
+ "step0 c p \<equiv> step c (p, 0)"
+
+abbreviation
+ "steps0 c p n \<equiv> steps c (p, 0) n"
+
lemma step_red [simp]:
shows "steps c p (Suc n) = step (steps c p n) p"
by (induct n arbitrary: c) (auto)
@@ -90,8 +99,7 @@
tm_wf :: "tprog \<Rightarrow> bool"
where
"tm_wf (p, off) = (length p \<ge> 2 \<and> length p mod 2 = 0 \<and>
- (\<forall>(a, s) \<in> set p. s \<le> length p div 2
- + off \<and> s \<ge> off))"
+ (\<forall>(a, s) \<in> set p. s \<le> length p div 2 + off \<and> s \<ge> off))"
lemma halt_lemma:
"\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"
@@ -121,16 +129,15 @@
where
"shift p n = (map (\<lambda> (a, s). (a, (if s = 0 then 0 else s + n))) p)"
-
-lemma length_shift [simp]:
- "length (shift p n) = length p"
-by (simp)
-
fun
adjust :: "instr list \<Rightarrow> instr list"
where
"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"
+by simp
+
lemma length_adjust[simp]:
shows "length (adjust p) = length p"
by (induct p) (auto)
@@ -138,7 +145,7 @@
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)))"
+ "tm_comp p1 p2 = ((adjust p1) @ (shift p2 (length p1 div 2)))"
fun
is_final :: "config \<Rightarrow> bool"
@@ -155,21 +162,12 @@
where
"P holds_for (s, l, r) = P (l, r)"
-(*
-lemma step_0 [simp]:
- shows "step (0, (l, r)) p = (0, (l, r))"
-by simp
-
-lemma steps_0 [simp]:
- shows "steps (0, (l, r)) p n = (0, (l, r))"
-by (induct n) (simp_all)
-*)
-
lemma is_final_holds[simp]:
assumes "is_final c"
shows "Q holds_for (steps c (p, off) n) = Q holds_for c"
using assms
apply(induct n)
+apply(auto)
apply(case_tac [!] c)
apply(auto)
done
@@ -179,22 +177,23 @@
definition
assert_imp :: "assert \<Rightarrow> assert \<Rightarrow> bool" ("_ \<mapsto> _" [0, 0] 100)
where
- "P \<mapsto> Q = (\<forall>l r. P (l, r) \<longrightarrow> Q (l, r))"
+ "P \<mapsto> Q \<equiv> \<forall>l r. P (l, r) \<longrightarrow> Q (l, r)"
lemma holds_for_imp:
assumes "P holds_for c"
and "P \<mapsto> Q"
shows "Q holds_for c"
-using assms unfolding assert_imp_def by (case_tac c, auto)
+using assms unfolding assert_imp_def
+by (case_tac c) (auto)
definition
- Hoare :: "assert \<Rightarrow> tprog \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" 50)
+ Hoare :: "assert \<Rightarrow> tprog0 \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" 50)
where
"{P} p {Q} \<equiv>
- (\<forall>l r. P (l, r) \<longrightarrow> (\<exists>n. is_final (steps (1, (l, r)) p n) \<and> Q holds_for (steps (1, (l, r)) p n)))"
+ (\<forall>l r. P (l, r) \<longrightarrow> (\<exists>n. is_final (steps0 (1, (l, r)) p n) \<and> Q holds_for (steps0 (1, (l, r)) p n)))"
lemma HoareI:
- assumes "\<And>l r. P (l, r) \<Longrightarrow> \<exists>n. is_final (steps (1, (l, r)) p n) \<and> Q holds_for (steps (1, (l, r)) p n)"
+ assumes "\<And>l r. P (l, r) \<Longrightarrow> \<exists>n. is_final (steps0 (1, (l, r)) p n) \<and> Q holds_for (steps0 (1, (l, r)) p n)"
shows "{P} p {Q}"
unfolding Hoare_def using assms by auto
@@ -207,85 +206,46 @@
shows "steps (0, (l, r)) p n = (0, (l, r))"
by (induct n) (simp_all)
-declare steps.simps[simp del]
-
-lemma before_final_old:
- assumes "steps (1, tp) A n = (0, tp')"
- obtains n' where "\<not> is_final (steps (1, tp) A n')"
- and "steps (1, tp) A (Suc n') = (0, tp')"
-proof -
- from assms have "\<exists> n'. \<not> is_final (steps (1, tp) A n') \<and>
- steps (1, tp) A (Suc n') = (0, tp')"
- proof(induct n arbitrary: tp', simp add: steps.simps)
- fix n tp'
- assume ind:
- "\<And>tp'. steps (1, tp) A n = (0, tp') \<Longrightarrow>
- \<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')"
- and h: " steps (1, tp) A (Suc n) = (0, tp')"
- from h show "\<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')"
- proof(simp add: step_red del: steps.simps,
- case_tac "(steps (Suc 0, tp) A n)", case_tac "a = 0", simp)
- fix a b c
- assume " steps (Suc 0, tp) A n = (0, tp')"
- hence "\<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')"
- apply(rule_tac ind, simp)
- done
- thus "\<exists>n'. \<not> is_final (steps (Suc 0, tp) A n') \<and> step (steps (Suc 0, tp) A n') A = (0, tp')"
- apply(simp)
- done
- next
- fix a b c
- assume "steps (Suc 0, tp) A n = (a, b, c)"
- "step (steps (Suc 0, tp) A n) A = (0, tp')"
- "a \<noteq> 0"
- thus "\<exists>n'. \<not> is_final (steps (Suc 0, tp) A n') \<and>
- step (steps (Suc 0, tp) A n') A = (0, tp')"
- apply(rule_tac x = n in exI)
- apply(simp)
- done
- qed
- qed
- thus "(\<And>n'. \<lbrakk>\<not> is_final (steps (1, tp) A n');
- steps (1, tp) A (Suc n') = (0, tp')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis"
- by auto
-qed
-
+(* if the machine is in the halting state, there must have
+ been a state just before the halting state *)
lemma before_final:
- assumes "steps (1, tp) A n = (0, tp')"
- shows "\<exists> n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')"
+ 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: "steps (1, tp) A 0 = (0, tp')" by fact
- then show "\<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')"
- by (simp add: steps.simps)
+ 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'. steps (1, tp) A n = (0, tp') \<Longrightarrow>
- \<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')" by fact
- have asm: "steps (1, tp) A (Suc n) = (0, tp')" by fact
- obtain s l r where cases: "steps (1, tp) A n = (s, l, r)"
+ 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 (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')"
+ 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 "steps (1, tp) A n = (0, tp')"
- using asm cases by simp
+ 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 (steps (1, tp) A n) \<and> steps (1, tp) A (Suc n) = (0, tp')"
+ 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
-declare tm_comp.simps [simp del] adjust.simps[simp del] shift.simps[simp del]
lemma length_comp:
-"length (A |+| B) = length A + length B"
-apply(auto simp: tm_comp.simps)
-done
+ 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:
assumes "case (fetch A a x) of (ac, ns) \<Rightarrow> ns \<noteq> 0"
@@ -532,32 +492,32 @@
assumes aimpb: "Q1 \<mapsto> P2"
and A_wf : "tm_wf (A, 0)"
and B_wf : "tm_wf (B, 0)"
- and A_halt : "{P1} (A, 0) {Q1}"
- and B_halt : "{P2} (B, 0) {Q2}"
- shows "{P1} (A |+| B, 0) {Q2}"
+ and A_halt : "{P1} A {Q1}"
+ and B_halt : "{P2} B {Q2}"
+ shows "{P1} A |+| B {Q2}"
proof(rule HoareI)
fix l r
assume h: "P1 (l, r)"
then obtain n1
- where "is_final (steps (1, l, r) (A, 0) n1)" and "Q1 holds_for (steps (1, l, r) (A, 0) n1)"
+ where "is_final (steps0 (1, l, r) A n1)" and "Q1 holds_for (steps0 (1, l, r) A n1)"
using A_halt unfolding Hoare_def by auto
- then obtain l' r' where "steps (1, l, r) (A, 0) n1 = (0, l', r')" and c: "Q1 holds_for (0, l', r')"
- by(case_tac "steps (1, l, r) (A, 0) n1") (auto)
- then obtain stpa where d: "steps (1, l, r) (A |+| B, 0) stpa = (Suc (length A div 2), l', r')"
+ then obtain l' r' where "steps0 (1, l, r) A n1 = (0, l', r')" and c: "Q1 holds_for (0, l', r')"
+ by(case_tac "steps0 (1, l, r) A n1") (auto)
+ then obtain stpa where d: "steps0 (1, l, r) (A |+| B) stpa = (Suc (length A div 2), l', r')"
using A_wf by(rule_tac t_merge_pre_halt_same) (auto)
moreover
from c aimpb have "P2 holds_for (0, l', r')"
by (rule holds_for_imp)
then have "P2 (l', r')" by auto
then obtain n2
- where "is_final (steps (1, l', r') (B, 0) n2)" and "Q2 holds_for (steps (1, l', r') (B, 0) n2)"
+ 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 "steps (1, l', r') (B, 0) n2 = (0, l'', r'')" and g: "Q2 holds_for (0, l'', r'')"
- by (case_tac "steps (1, l', r') (B, 0) n2", auto)
- then have "steps (Suc (length A div 2), l', r') (A |+| B, 0) n2 = (0, l'', r'')"
+ 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)
+ 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 (steps (1, l, r) (A |+| B, 0) n) \<and> Q2 holds_for (steps (1, l, r) (A |+| B, 0) n)"
+ "\<exists>n. is_final (steps0 (1, l, r) (A |+| B) n) \<and> Q2 holds_for (steps0 (1, l, r) (A |+| B) n)"
using g
apply(rule_tac x = "stpa + n2" in exI)
apply(simp add: steps_add)
@@ -565,69 +525,70 @@
qed
definition
- Hoare_unhalt :: "assert \<Rightarrow> tprog \<Rightarrow> bool" ("({(1_)}/ (_))" 50)
+ 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 (steps (1, (l, r)) p n))))"
+ (\<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 (steps (1, (l, r)) p n)"
+ assumes "\<And>l r. P (l, r) \<Longrightarrow> \<forall> n. \<not> is_final (steps0 (1, (l, r)) p n)"
shows "{P} p"
unfolding Hoare_unhalt_def using assms by auto
-lemma Hoare_plus_unhalt:
+lemma Hoare_plus_unhalt:
+ fixes A B :: tprog0
assumes aimpb: "Q1 \<mapsto> P2"
and A_wf : "tm_wf (A, 0)"
and B_wf : "tm_wf (B, 0)"
- and A_halt : "{P1} (A, 0) {Q1}"
- and B_uhalt : "{P2} (B, 0)"
- shows "{P1} (A |+| B, 0)"
+ and A_halt : "{P1} A {Q1}"
+ and B_uhalt : "{P2} B"
+ shows "{P1} (A |+| B)"
proof(rule_tac Hoare_unhalt_I)
fix l r
assume h: "P1 (l, r)"
- then obtain n1 where a: "is_final (steps (1, l, r) (A, 0) n1)" and b: "Q1 holds_for (steps (1, l, r) (A, 0) n1)"
+ then obtain n1 where a: "is_final (steps0 (1, l, r) A n1)" and b: "Q1 holds_for (steps0 (1, l, r) A n1)"
using A_halt unfolding Hoare_def by auto
- then obtain l' r' where "steps (1, l, r) (A, 0) n1 = (0, l', r')" and c: "Q1 holds_for (0, l', r')"
- by(case_tac "steps (1, l, r) (A, 0) n1", auto)
- then obtain stpa where d: "steps (1, l, r) (A |+| B, 0) stpa = (Suc (length A div 2), l', r')"
+ then obtain l' r' where "steps0 (1, l, r) A n1 = (0, l', r')" and c: "Q1 holds_for (0, l', r')"
+ by(case_tac "steps0 (1, l, r) A n1", auto)
+ then obtain stpa where d: "steps0 (1, l, r) (A |+| B) stpa = (Suc (length A div 2), l', r')"
using A_wf
by(rule_tac t_merge_pre_halt_same, auto)
from c aimpb have "P2 holds_for (0, l', r')"
by(rule holds_for_imp)
from this have "P2 (l', r')" by auto
- from this have e: "\<forall> n. \<not> is_final (steps (Suc 0, l', r') (B, 0) n) "
+ from this have e: "\<forall> n. \<not> is_final (steps0 (Suc 0, l', r') B n) "
using B_uhalt unfolding Hoare_unhalt_def
by auto
- from e show "\<forall>n. \<not> is_final (steps (1, l, r) (A |+| B, 0) n)"
+ from e show "\<forall>n. \<not> is_final (steps0 (1, l, r) (A |+| B) n)"
proof(rule_tac allI, case_tac "n > stpa")
fix n
assume h2: "stpa < n"
- hence "\<not> is_final (steps (Suc 0, l', r') (B, 0) (n - stpa))"
+ hence "\<not> is_final (steps0 (Suc 0, l', r') B (n - stpa))"
using e
apply(erule_tac x = "n - stpa" in allE) by simp
- then obtain s'' l'' r'' where f: "steps (Suc 0, l', r') (B, 0) (n - stpa) = (s'', l'', r'')" and g: "s'' \<noteq> 0"
- apply(case_tac "steps (Suc 0, l', r') (B, 0) (n - stpa)", auto)
+ then obtain s'' l'' r'' where f: "steps0 (Suc 0, l', r') B (n - stpa) = (s'', l'', r'')" and g: "s'' \<noteq> 0"
+ apply(case_tac "steps0 (Suc 0, l', r') B (n - stpa)", auto)
done
- have k: "steps (Suc (length A div 2), l', r') (A |+| B, 0) (n - stpa) = (s''+ length A div 2, l'', r'') "
+ have k: "steps0 (Suc (length A div 2), l', r') (A |+| B) (n - stpa) = (s''+ length A div 2, l'', r'') "
using A_wf B_wf f g
apply(drule_tac t_merge_second_same, auto)
done
- show "\<not> is_final (steps (1, l, r) (A |+| B, 0) n)"
+ show "\<not> is_final (steps0 (1, l, r) (A |+| B) n)"
proof -
- have "\<not> is_final (steps (1, l, r) (A |+| B, 0) (stpa + (n - stpa)))"
+ have "\<not> is_final (steps0 (1, l, r) (A |+| B) (stpa + (n - stpa)))"
using d k A_wf
apply(simp only: steps_add d, simp add: tm_wf.simps)
done
- thus "\<not> is_final (steps (1, l, r) (A |+| B, 0) n)"
+ thus "\<not> is_final (steps0 (1, l, r) (A |+| B) n)"
using h2 by simp
qed
next
fix n
assume h2: "\<not> stpa < n"
- with d show "\<not> is_final (steps (1, l, r) (A |+| B, 0) n)"
+ with d show "\<not> is_final (steps0 (1, l, r) (A |+| B) n)"
apply(auto)
apply(subgoal_tac "\<exists> d. stpa = n + d", auto)
- apply(case_tac "(steps (Suc 0, l, r) (A |+| B, 0) n)", simp)
+ apply(case_tac "(steps0 (Suc 0, l, r) (A |+| B) n)", simp)
apply(rule_tac x = "stpa - n" in exI, simp)
done
qed