--- a/thys/uncomputable.thy Fri Jan 25 21:15:09 2013 +0000
+++ b/thys/uncomputable.thy Fri Jan 25 22:03:03 2013 +0000
@@ -197,44 +197,42 @@
(* tcopy_loop *)
fun
- inv_loop0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
inv_loop1_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
inv_loop1_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+ inv_loop5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+ inv_loop5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+ inv_loop6_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+ inv_loop6_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+where
+ "inv_loop1_loop x (l, r) = (\<exists> i j. i + j + 1 = x \<and> l = Oc\<up>i \<and> r = Oc # Oc # Bk\<up>j @ Oc\<up>j \<and> j > 0)"
+| "inv_loop1_exit x (l, r) = (l = [] \<and> r = Bk # Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0)"
+| "inv_loop5_loop x (l, r) =
+ (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> k + t = j \<and> t > 0 \<and> l = Oc\<up>k@Bk\<up>j@Oc\<up>i \<and> r = Oc\<up>t)"
+| "inv_loop5_exit x (l, r) =
+ (\<exists> i j. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> l = Bk\<up>(j - 1)@Oc\<up>i \<and> r = Bk # Oc\<up>j)"
+| "inv_loop6_loop x (l, r) =
+ (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> k + t + 1 = j \<and> l = Bk\<up>k @ Oc\<up>i \<and> r = Bk\<up>(Suc t) @ Oc\<up>j)"
+| "inv_loop6_exit x (l, r) =
+ (\<exists> i j. i + j = x \<and> j > 0 \<and> l = Oc\<up>i \<and> r = Oc # Bk\<up>j @ Oc\<up>j)"
+
+fun
+ inv_loop0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
inv_loop1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
inv_loop2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
inv_loop3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
inv_loop4 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
- inv_loop5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
- inv_loop5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
- inv_loop5 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+ inv_loop5 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+ inv_loop6 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
"inv_loop0 x (l, r) = (l = [Bk] \<and> r = Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0 )"
-| "inv_loop1_loop x (l, r) = (\<exists> i j. i + j + 1 = x \<and> l = Oc\<up>i \<and> r = Oc # Oc # Bk\<up>j @ Oc\<up>j \<and> j > 0)"
-| "inv_loop1_exit x (l, r) = (l = [] \<and> r = Bk # Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0)"
| "inv_loop1 x (l, r) = (inv_loop1_loop x (l, r) \<or> inv_loop1_exit x (l, r))"
| "inv_loop2 x (l, r) = (\<exists> i j any. i + j = x \<and> x > 0 \<and> i > 0 \<and> j > 0 \<and> l = Oc\<up>i \<and> r = any#Bk\<up>j@Oc\<up>j)"
| "inv_loop3 x (l, r) =
(\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and> k + t = Suc j \<and> l = Bk\<up>k@Oc\<up>i \<and> r = Bk\<up>t@Oc\<up>j)"
| "inv_loop4 x (l, r) =
(\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and> k + t = j \<and> l = Oc\<up>k @ Bk\<up>(Suc j)@Oc\<up>i \<and> r = Oc\<up>t)"
-| "inv_loop5_loop x (l, r) =
- (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> k + t = j \<and> t > 0 \<and> l = Oc\<up>k@Bk\<up>j@Oc\<up>i \<and> r = Oc\<up>t)"
-| "inv_loop5_exit x (l, r) = (\<exists> i j. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> l = Bk\<up>(j - 1)@Oc\<up>i \<and> r = Bk # Oc\<up>j)"
| "inv_loop5 x (l, r) = (inv_loop5_loop x (l, r) \<or> inv_loop5_exit x (l, r))"
-
-fun inv_loop6_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "inv_loop6_loop x (l, r) =
- (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> k + t + 1 = j \<and> l = Bk\<up>k @ Oc\<up>i \<and> r = Bk\<up>(Suc t) @ Oc\<up>j)"
-
-fun inv_loop6_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "inv_loop6_exit x (l, r) =
- (\<exists> i j. i + j = x \<and> j > 0 \<and> l = Oc\<up>i \<and> r = Oc # Bk\<up>j @ Oc\<up>j)"
-
-fun inv_loop6 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "inv_loop6 x (l, r) = (inv_loop6_loop x (l, r) \<or> inv_loop6_exit x (l, r))"
+| "inv_loop6 x (l, r) = (inv_loop6_loop x (l, r) \<or> inv_loop6_exit x (l, r))"
fun inv_loop :: "nat \<Rightarrow> config \<Rightarrow> bool"
where
@@ -257,7 +255,7 @@
by (case_tac t, auto)
lemma [simp]: "inv_loop1 x (b, []) = False"
-by(simp add: inv_loop1.simps)
+by (simp add: inv_loop1.simps)
lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"
by (auto simp: inv_loop2.simps inv_loop3.simps)
@@ -274,29 +272,22 @@
done
lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x ([], [])\<rbrakk> \<Longrightarrow> RR"
-apply(auto simp: inv_loop4.simps inv_loop5.simps)
-done
+by (auto simp: inv_loop4.simps inv_loop5.simps)
lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x (b, []); b \<noteq> []\<rbrakk> \<Longrightarrow> RR"
-apply(auto simp: inv_loop4.simps inv_loop5.simps)
-done
+by (auto simp: inv_loop4.simps inv_loop5.simps)
lemma [elim]: "inv_loop6 x ([], []) \<Longrightarrow> RR"
-apply(auto simp: inv_loop6.simps)
-done
+by (auto simp: inv_loop6.simps)
-thm inv_loop6_exit.simps
lemma [elim]: "inv_loop6 x (b, []) \<Longrightarrow> RR"
-apply(auto simp: inv_loop6.simps)
-done
+by (auto simp: inv_loop6.simps)
lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> b = []"
-apply(auto simp: inv_loop1.simps)
-done
+by (auto simp: inv_loop1.simps)
lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> list = Oc # Bk \<up> x @ Oc \<up> x"
-apply(auto simp: inv_loop1.simps)
-done
+by (auto simp: inv_loop1.simps)
lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, list)"
apply(auto simp: inv_loop2.simps inv_loop3.simps)
@@ -304,8 +295,7 @@
done
lemma [elim]: "Bk # list = Oc \<up> j \<Longrightarrow> RR"
-apply(case_tac j, simp_all)
-done
+by (case_tac j, simp_all)
lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, list)"
apply(auto simp: inv_loop3.simps)
@@ -315,20 +305,16 @@
done
lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop5 x (b, Oc # list)"
-apply(auto simp: inv_loop4.simps inv_loop5.simps)
-done
+by (auto simp: inv_loop4.simps inv_loop5.simps)
lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"
-apply(auto simp: inv_loop6.simps inv_loop5.simps)
-done
+by (auto simp: inv_loop6.simps inv_loop5.simps)
lemma [simp]: "inv_loop5_loop x (b, Bk # list) = False"
-apply(auto simp: inv_loop5_loop.simps)
-done
+by (auto simp: inv_loop5.simps)
lemma [simp]: "inv_loop6_exit x (b, Bk # list) = False"
-apply(auto simp: inv_loop6.simps)
-done
+by (auto simp: inv_loop6.simps)
declare inv_loop5_loop.simps[simp del] inv_loop5_exit.simps[simp del]
inv_loop6_loop.simps[simp del] inv_loop6_exit.simps[simp del]
@@ -346,8 +332,7 @@
done
lemma [simp]: "inv_loop6_loop x (b, Oc # Bk # list) = False"
-apply(auto simp: inv_loop6_loop.simps)
-done
+by (auto simp: inv_loop6_loop.simps)
lemma [elim]: "\<lbrakk>x > 0; inv_loop5_exit x (b, Bk # list); b \<noteq> []; hd b = Oc\<rbrakk> \<Longrightarrow>
inv_loop6_exit x (tl b, Oc # Bk # list)"
@@ -370,12 +355,10 @@
done
lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"
-apply(simp)
-done
+by (simp)
lemma [simp]: "inv_loop6_exit x (b, Bk # list) = False"
-apply(simp add: inv_loop6_exit.simps)
-done
+by (simp add: inv_loop6_exit.simps)
lemma [elim]: "\<lbrakk>0 < x; inv_loop6_loop x (b, Bk # list); b \<noteq> []; hd b = Bk\<rbrakk>
\<Longrightarrow> inv_loop6_loop x (tl b, Bk # Bk # list)"
@@ -405,8 +388,7 @@
done
lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop2 x (b, Bk # list)"
-apply(auto simp: inv_loop2.simps)
-done
+by (auto simp: inv_loop2.simps)
lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop4 x (Oc # b, list)"
apply(auto simp: inv_loop3.simps inv_loop4.simps)
@@ -424,12 +406,10 @@
done
lemma [simp]: "inv_loop5 x ([], list) = False"
-apply(auto simp: inv_loop5.simps inv_loop5_exit.simps inv_loop5_loop.simps)
-done
+by (auto simp: inv_loop5.simps inv_loop5_exit.simps inv_loop5_loop.simps)
lemma [simp]: "inv_loop5_exit x (b, Oc # list) = False"
-apply(auto simp: inv_loop5_exit.simps)
-done
+by (auto simp: inv_loop5_exit.simps)
lemma [elim]: " \<lbrakk>inv_loop5_loop x (b, Oc # list); b \<noteq> []; hd b = Bk\<rbrakk>
\<Longrightarrow> inv_loop5_exit x (tl b, Bk # Oc # list)"
@@ -448,14 +428,12 @@
apply(case_tac [!] k, auto)
done
-lemma [elim]: "\<lbrakk>inv_loop5 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow>
- inv_loop5 x (tl b, hd b # Oc # list)"
+lemma [elim]: "\<lbrakk>inv_loop5 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop5 x (tl b, hd b # Oc # list)"
apply(simp add: inv_loop5.simps)
apply(case_tac "hd b", simp_all, auto)
done
-lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x ([], Oc # list)\<rbrakk> \<Longrightarrow>
- inv_loop1 x ([], Bk # Oc # list)"
+lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x ([], Oc # list)\<rbrakk> \<Longrightarrow> inv_loop1 x ([], Bk # Oc # list)"
apply(auto simp: inv_loop6.simps inv_loop1.simps
inv_loop6_loop.simps inv_loop6_exit.simps)
done
@@ -467,8 +445,7 @@
done
lemma inv_loop_step:
- "\<lbrakk>inv_loop x cf; x > 0\<rbrakk>
- \<Longrightarrow> inv_loop x (step cf (tcopy_loop, 0))"
+ "\<lbrakk>inv_loop x cf; x > 0\<rbrakk> \<Longrightarrow> inv_loop x (step cf (tcopy_loop, 0))"
apply(case_tac cf, case_tac c, case_tac [2] aa)
apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral split: if_splits)
done
@@ -517,23 +494,19 @@
"loop_LE \<equiv> (inv_image lex_triple loop_measure)"
lemma wf_loop_le: "wf loop_LE"
-by(auto intro:wf_inv_image simp: loop_LE_def wf_lex_triple)
+by (auto intro:wf_inv_image simp: loop_LE_def wf_lex_triple)
lemma [simp]: "inv_loop2 x ([], b) = False"
-apply(auto simp: inv_loop2.simps)
-done
+by (auto simp: inv_loop2.simps)
lemma [simp]: "inv_loop2 x (l', []) = False"
-apply(auto simp: inv_loop2.simps)
-done
+by (auto simp: inv_loop2.simps)
lemma [simp]: "inv_loop3 x (b, []) = False"
-apply(auto simp: inv_loop3.simps)
-done
+by (auto simp: inv_loop3.simps)
lemma [simp]: "inv_loop4 x ([], b) = False"
-apply(auto simp: inv_loop4.simps)
-done
+by (auto simp: inv_loop4.simps)
lemma [elim]:
"\<lbrakk>inv_loop4 x (l', []); l' \<noteq> []; x > 0;
@@ -551,17 +524,15 @@
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>
\<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list)) <
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))"
-apply(auto simp: inv_loop4.simps)
-done
+by (auto simp: inv_loop4.simps)
lemma takeWhile_replicate_append:
"P a \<Longrightarrow> takeWhile P (a\<up>x @ ys) = a\<up>x @ takeWhile P ys"
-apply(induct x, auto)
-done
+by (induct x, auto)
lemma takeWhile_replicate:
"P a \<Longrightarrow> takeWhile P (a\<up>x) = a\<up>x"
-by(induct x, auto)
+by (induct x, auto)
lemma [elim]:
"\<lbrakk>inv_loop5 x (l', Bk # list); l' \<noteq> []; 0 < x;
@@ -578,8 +549,7 @@
done
lemma [elim]: "\<lbrakk>inv_loop1 x (l', Oc # list)\<rbrakk> \<Longrightarrow> hd list = Oc"
-apply(auto simp: inv_loop1.simps)
-done
+by (auto simp: inv_loop1.simps)
lemma [elim]:
"\<lbrakk>inv_loop6 x (l', Bk # list); l' \<noteq> []; 0 < x;
@@ -680,43 +650,35 @@
(* tcopy_end *)
-
-fun inv_end1 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "inv_end1 x (l, r) = (x > 0 \<and> l = [Bk] \<and> r = Oc # Bk\<up>x @ Oc\<up>x)"
-fun inv_end2 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "inv_end2 x (l, r) = (\<exists> i j. i + j = Suc x \<and> x > 0 \<and> l = Oc\<up>i @ [Bk] \<and> r = Bk\<up>j @ Oc\<up>x)"
-
-fun inv_end3 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "inv_end3 x (l, r) =
- (\<exists> i j. x > 0 \<and> i + j = x \<and> l = Oc\<up>i @ [Bk] \<and> r = Oc # Bk\<up>j@ Oc\<up>x )"
-
-fun inv_end4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "inv_end4 x (l, r) = (\<exists> any. x > 0 \<and> l = Oc\<up>x @ [Bk] \<and> r = any#Oc\<up>x)"
+fun
+ inv_end5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+ inv_end5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+where
+ "inv_end5_loop x (l, r) =
+ (\<exists> i j. i + j = x \<and> x > 0 \<and> j > 0 \<and> l = Oc\<up>i @ [Bk] \<and> r = Oc\<up>j @ Bk # Oc\<up>x)"
+| "inv_end5_exit x (l, r) = (x > 0 \<and> l = [] \<and> r = Bk # Oc\<up>x @ Bk # Oc\<up>x)"
-fun inv_end5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "inv_end5_loop x (l, r) =
- (\<exists> i j. i + j = x \<and> x > 0 \<and> j > 0 \<and> l = Oc\<up>i @ [Bk] \<and> r = Oc\<up>j @ Bk # Oc\<up>x)"
-
-fun inv_end5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "inv_end5_exit x (l, r) = (x > 0 \<and> l = [] \<and> r = Bk # Oc\<up>x @ Bk # Oc\<up>x)"
+fun
+ inv_end0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+ inv_end1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+ inv_end2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+ inv_end3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+ inv_end4 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+
+ inv_end5 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+where
+ "inv_end0 x (l, r) = (x > 0 \<and> l = [Bk] \<and> r = Oc\<up>x @ Bk # Oc\<up>x)"
+| "inv_end1 x (l, r) = (x > 0 \<and> l = [Bk] \<and> r = Oc # Bk\<up>x @ Oc\<up>x)"
+| "inv_end2 x (l, r) = (\<exists> i j. i + j = Suc x \<and> x > 0 \<and> l = Oc\<up>i @ [Bk] \<and> r = Bk\<up>j @ Oc\<up>x)"
+| "inv_end3 x (l, r) =
+ (\<exists> i j. x > 0 \<and> i + j = x \<and> l = Oc\<up>i @ [Bk] \<and> r = Oc # Bk\<up>j@ Oc\<up>x)"
+| "inv_end4 x (l, r) = (\<exists> any. x > 0 \<and> l = Oc\<up>x @ [Bk] \<and> r = any#Oc\<up>x)"
+| "inv_end5 x (l, r) = (inv_end5_loop x (l, r) \<or> inv_end5_exit x (l, r))"
-fun inv_end5 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "inv_end5 x (l, r) = (inv_end5_loop x (l, r) \<or> inv_end5_exit x (l, r))"
-
-fun inv_end0 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "inv_end0 x (l, r) = (x > 0 \<and> l = [Bk] \<and> r = Oc\<up>x @ Bk # Oc\<up>x)"
-
-fun inv_end :: "nat \<Rightarrow> config \<Rightarrow> bool"
- where
+fun
+ inv_end :: "nat \<Rightarrow> config \<Rightarrow> bool"
+where
"inv_end x (s, l, r) = (if s = 0 then inv_end0 x (l, r)
else if s = 1 then inv_end1 x (l, r)
else if s = 2 then inv_end2 x (l, r)
@@ -731,34 +693,26 @@
inv_end5.simps[simp del]
lemma [simp]: "inv_end1 x (b, []) = False"
-apply(auto simp: inv_end1.simps)
-done
+by (auto simp: inv_end1.simps)
lemma [simp]: "inv_end2 x (b, []) = False"
-apply(auto simp: inv_end2.simps)
-done
+by (auto simp: inv_end2.simps)
lemma [simp]: "inv_end3 x (b, []) = False"
-apply(auto simp: inv_end3.simps)
-done
+by (auto simp: inv_end3.simps)
-thm inv_end4.simps
lemma [simp]: "inv_end4 x (b, []) = False"
-apply(auto simp: inv_end4.simps)
-done
+by (auto simp: inv_end4.simps)
lemma [simp]: "inv_end5 x (b, []) = False"
-apply(auto simp: inv_end5.simps)
-done
+by (auto simp: inv_end5.simps)
lemma [simp]: "inv_end1 x ([], list) = False"
-apply(auto simp: inv_end1.simps)
-done
+by (auto simp: inv_end1.simps)
lemma [elim]: "\<lbrakk>0 < x; inv_end1 x (b, Bk # list); b \<noteq> []\<rbrakk>
\<Longrightarrow> inv_end0 x (tl b, hd b # Bk # list)"
-apply(auto simp: inv_end1.simps inv_end0.simps)
-done
+by (auto simp: inv_end1.simps inv_end0.simps)
lemma [elim]: "\<lbrakk>0 < x; inv_end2 x (b, Bk # list)\<rbrakk>
\<Longrightarrow> inv_end3 x (b, Oc # list)"
@@ -769,13 +723,11 @@
done
lemma [elim]: "\<lbrakk>0 < x; inv_end3 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Bk # b, list)"
-apply(auto simp: inv_end2.simps inv_end3.simps)
-done
+by (auto simp: inv_end2.simps inv_end3.simps)
lemma [elim]: "\<lbrakk>0 < x; inv_end4 x ([], Bk # list)\<rbrakk> \<Longrightarrow>
inv_end5 x ([], Bk # Bk # list)"
-apply(auto simp: inv_end4.simps inv_end5.simps)
-done
+by (auto simp: inv_end4.simps inv_end5.simps)
lemma [elim]: "\<lbrakk>0 < x; inv_end4 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow>
inv_end5 x (tl b, hd b # Bk # list)"
@@ -789,13 +741,11 @@
done
lemma [elim]: "\<lbrakk>0 < x; inv_end1 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Oc # b, list)"
-apply(auto simp: inv_end1.simps inv_end2.simps)
-done
+by (auto simp: inv_end1.simps inv_end2.simps)
lemma [elim]: "\<lbrakk>0 < x; inv_end2 x ([], Oc # list)\<rbrakk> \<Longrightarrow>
inv_end4 x ([], Bk # Oc # list)"
-apply(auto simp: inv_end2.simps inv_end4.simps)
-done
+by (auto simp: inv_end2.simps inv_end4.simps)
lemma [elim]: "\<lbrakk>0 < x; inv_end2 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow>
inv_end4 x (tl b, hd b # Oc # list)"
@@ -804,23 +754,19 @@
done
lemma [elim]: "\<lbrakk>0 < x; inv_end3 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Oc # b, list)"
-apply(auto simp: inv_end2.simps inv_end3.simps)
-done
+by (auto simp: inv_end2.simps inv_end3.simps)
lemma [elim]: "\<lbrakk>0 < x; inv_end4 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end4 x (b, Bk # list)"
-apply(auto simp: inv_end2.simps inv_end4.simps)
-done
+by (auto simp: inv_end2.simps inv_end4.simps)
lemma [elim]: "\<lbrakk>0 < x; inv_end5 x ([], Oc # list)\<rbrakk> \<Longrightarrow> inv_end5 x ([], Bk # Oc # list)"
-apply(auto simp: inv_end2.simps inv_end5.simps)
-done
+by (auto simp: inv_end2.simps inv_end5.simps)
declare inv_end5_loop.simps[simp del]
inv_end5_exit.simps[simp del]
lemma [simp]: "inv_end5_exit x (b, Oc # list) = False"
-apply(auto simp: inv_end5_exit.simps)
-done
+by (auto simp: inv_end5_exit.simps)
lemma [simp]: "inv_end5_loop x (tl b, Bk # Oc # list) = False"
apply(auto simp: inv_end5_loop.simps)
@@ -851,16 +797,13 @@
done
lemma inv_end_step:
- "\<lbrakk>x > 0;
- inv_end x cf\<rbrakk>
- \<Longrightarrow> inv_end x (step cf (tcopy_end, 0))"
+ "\<lbrakk>x > 0; inv_end x cf\<rbrakk> \<Longrightarrow> inv_end x (step cf (tcopy_end, 0))"
apply(case_tac cf, case_tac c, case_tac [2] aa)
apply(auto simp: inv_end.simps step.simps tcopy_end_def numeral split: if_splits)
done
lemma inv_end_steps:
- "\<lbrakk>x > 0; inv_end x cf\<rbrakk>
-\<Longrightarrow> inv_end x (steps cf (tcopy_end, 0) stp)"
+ "\<lbrakk>x > 0; inv_end x cf\<rbrakk> \<Longrightarrow> inv_end x (steps cf (tcopy_end, 0) stp)"
apply(induct stp, simp add:steps.simps, simp)
apply(erule_tac inv_end_step, simp)
done
@@ -878,8 +821,7 @@
fun end_stage :: "config \<Rightarrow> nat"
where
"end_stage (s, l, r) =
- (if s = 2 \<or> s = 3 then (length r)
- else 0)"
+ (if s = 2 \<or> s = 3 then (length r) else 0)"
fun end_step :: "config \<Rightarrow> nat"
where
@@ -900,11 +842,10 @@
"end_LE \<equiv> (inv_image lex_triple end_measure)"
lemma wf_end_le: "wf end_LE"
-by(auto intro:wf_inv_image simp: end_LE_def wf_lex_triple)
+by (auto intro: wf_inv_image simp: end_LE_def wf_lex_triple)
lemma [simp]: "inv_end5 x ([], Oc # list) = False"
-apply(auto simp: inv_end5.simps inv_end5_loop.simps)
-done
+by (auto simp: inv_end5.simps inv_end5_loop.simps)
lemma end_halt:
"\<lbrakk>x > 0; inv_end x (Suc 0, l, r)\<rbrakk> \<Longrightarrow>
@@ -964,18 +905,16 @@
(* tcopy *)
lemma [intro]: "tm_wf (tcopy_init, 0)"
-by(auto simp: tm_wf.simps tcopy_init_def)
+by (auto simp: tm_wf.simps tcopy_init_def)
lemma [intro]: "tm_wf (tcopy_loop, 0)"
-by(auto simp: tm_wf.simps tcopy_loop_def)
+by (auto simp: tm_wf.simps tcopy_loop_def)
lemma [intro]: "tm_wf (tcopy_end, 0)"
-by(auto simp: tm_wf.simps tcopy_end_def)
+by (auto simp: tm_wf.simps tcopy_end_def)
lemma [intro]: "\<lbrakk>tm_wf (A, 0); tm_wf (B, 0)\<rbrakk> \<Longrightarrow> tm_wf (A |+| B, 0)"
-apply(auto simp: tm_wf.simps shift.simps adjust.simps tm_comp_length
- tm_comp.simps)
-done
+by (auto simp: tm_wf.simps shift.simps adjust.simps tm_comp_length tm_comp.simps)
lemma tcopy_correct1:
"\<lbrakk>x > 0\<rbrakk> \<Longrightarrow> {inv_init1 x} tcopy {inv_end0 x}"
@@ -1010,9 +949,9 @@
qed
abbreviation
- "pre_tcopy n \<equiv> \<lambda>(l::cell list, r::cell list). (l = [] \<and> r = <[n::nat]>)"
+ "pre_tcopy n \<equiv> \<lambda>(l::cell list, r::cell list). ((l, r) = ([], <[n::nat]>))"
abbreviation
- "post_tcopy n \<equiv> \<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[n, n::nat]>)"
+ "post_tcopy n \<equiv> \<lambda>(l::cell list, r::cell list). ((l, r) = ([Bk], <[n, n::nat]>))"
lemma tcopy_correct2:
shows "{pre_tcopy n} tcopy {post_tcopy n}"
@@ -1087,13 +1026,13 @@
definition haltP :: "tprog \<Rightarrow> nat list \<Rightarrow> bool"
where
- "haltP p lm \<equiv> \<exists>n a b c. steps (Suc 0, [], <lm>) p n = (0, Bk \<up> a, Oc \<up> b @ Bk \<up> c)"
+ "haltP p lm \<equiv> \<exists>n a b c. steps (1, [], <lm>) p n = (0, Bk \<up> a, Oc \<up> b @ Bk \<up> c)"
abbreviation
"haltP0 p lm \<equiv> haltP (p, 0) lm"
lemma [intro, simp]: "tm_wf0 tcopy"
-by(auto simp: tcopy_def)
+by (auto simp: tcopy_def)
lemma [intro, simp]: "tm_wf0 dither"
by (auto simp: tm_wf.simps dither_def)
@@ -1180,85 +1119,20 @@
The following two assumptions specifies that @{text "H"} does solve the Halting problem.
*}
and h_case:
- "\<And> M lm. (haltP0 M lm) \<Longrightarrow> \<exists> na nb. (steps0 (1, [], <code M # lm>) H na = (0, Bk \<up> nb, [Oc]))"
+ "\<And> M lm. (haltP0 M lm) \<Longrightarrow> \<exists> na nb. (steps0 (1, [Bk], <code M # lm>) H na = (0, Bk \<up> nb, [Oc]))"
and nh_case:
- "\<And> M lm. (\<not> haltP0 M lm) \<Longrightarrow>
- \<exists> na nb. (steps0 (1, [], <code M # lm>) H na = (0, Bk \<up> nb, [Oc, Oc]))"
+ "\<And> M lm. (\<not> haltP0 M lm) \<Longrightarrow> \<exists> na nb. (steps0 (1, [Bk], <code M # lm>) H na = (0, Bk \<up> nb, [Oc, Oc]))"
begin
-lemma h_newcase:
- "\<And> M lm. haltP0 M lm \<Longrightarrow> \<exists> na nb. (steps0 (1, Bk \<up> x , <code M # lm>) H na = (0, Bk \<up> nb, [Oc]))"
-proof -
- fix M lm
- assume "haltP (M, 0) lm"
- hence "\<exists> na nb. (steps (1, [], <code M # lm>) (H, 0) na
- = (0, Bk\<up>nb, [Oc]))"
- by (rule h_case)
- from this obtain na nb where
- cond1:"(steps (1, [], <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc]))" by blast
- thus "\<exists> na nb. (steps (1, Bk\<up>x, <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc]))"
- proof(rule_tac x = na in exI, case_tac "steps (1, Bk\<up>x, <code M # lm>) (H, 0) na", simp)
- fix a b c
- assume cond2: "steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na = (a, b, c)"
- have "tinres (Bk\<up>nb) b \<and> [Oc] = c \<and> 0 = a"
- proof(rule_tac tinres_steps)
- show "tinres [] (Bk\<up>x)"
- apply(simp add: tinres_def)
- apply(auto)
- done
- next
- show "(steps (1, [], <code M # lm>) (H, 0) na
- = (0, Bk\<up>nb, [Oc]))"
- by(simp add: cond1[simplified])
- next
- show "steps (1, Bk\<up>x, <code M # lm>) (H, 0) na = (a, b, c)"
- by(simp add: cond2[simplified])
- qed
- thus "a = 0 \<and> (\<exists>nb. b = (Bk\<up>nb)) \<and> c = [Oc]"
- by(auto elim: tinres_ex1)
- qed
-qed
-
-lemma nh_newcase:
- "\<And> M lm. \<not> (haltP (M, 0) lm) \<Longrightarrow> \<exists> na nb. (steps0 (1, Bk\<up>x, <code M # lm>) H na = (0, Bk\<up>nb, [Oc, Oc]))"
-proof -
- fix M lm
- assume "\<not> haltP (M, 0) lm"
- hence "\<exists> na nb. (steps (1, [], <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc, Oc]))"
- by (rule nh_case)
- from this obtain na nb where
- cond1: "(steps (1, [], <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc, Oc]))" by blast
- thus "\<exists> na nb. (steps (1, Bk\<up>x, <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc, Oc]))"
- proof(rule_tac x = na in exI, case_tac "steps (1, Bk\<up>x, <code M # lm>) (H, 0) na", simp)
- fix a b c
- assume cond2: "steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na = (a, b, c)"
- have "tinres (Bk\<up>nb) b \<and> [Oc, Oc] = c \<and> 0 = a"
- proof(rule_tac tinres_steps)
- show "tinres [] (Bk\<up>x)"
- apply(auto simp: tinres_def)
- done
- next
- show "(steps (Suc 0, [], <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc, Oc]))"
- by(simp add: cond1[simplified])
- next
- show "steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na = (a, b, c)"
- by(simp add: cond2[simplified])
- qed
- thus "a = 0 \<and> (\<exists>nb. b = Bk\<up>nb) \<and> c = [Oc, Oc]"
- by(auto elim: tinres_ex1)
- qed
-qed
-
-
(* invariants for H *)
abbreviation
- "pre_H_inv M n \<equiv> \<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[code M, n]>)"
+ "pre_H_inv M n \<equiv> \<lambda>(l::cell list, r::cell list). ((l, r) = ([Bk], <[code M, n]>))"
abbreviation
- "post_H_halt_inv \<equiv> \<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc]"
+ "post_H_halt_inv \<equiv> \<lambda>(l, r). (\<exists>n. (l, r) = (Bk \<up> n, [Oc, Oc]))"
abbreviation
- "post_H_unhalt_inv \<equiv> \<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc]"
+ "post_H_unhalt_inv \<equiv> \<lambda>(l, r). (\<exists>n. (l, r) = (Bk \<up> n, [Oc]))"
lemma H_halt_inv:
@@ -1266,8 +1140,8 @@
shows "{pre_H_inv M n} H {post_H_halt_inv}"
proof -
obtain stp i
- where "steps0 (1, Bk \<up> 1, <[code M, n]>) H stp = (0, Bk \<up> i, [Oc, Oc])"
- using nh_newcase[of "M" "[n]" "1", OF assms] by auto
+ where "steps0 (1, [Bk], <[code M, n]>) H stp = (0, Bk \<up> i, [Oc, Oc])"
+ using nh_case[of "M" "[n]", OF assms] by auto
then show "{pre_H_inv M n} H {post_H_halt_inv}"
unfolding Hoare_halt_def
apply(auto)
@@ -1281,8 +1155,8 @@
shows "{pre_H_inv M n} H {post_H_unhalt_inv}"
proof -
obtain stp i
- where "steps0 (1, Bk \<up> 1, <[code M, n]>) H stp = (0, Bk \<up> i, [Oc])"
- using h_newcase[of "M" "[n]" "1", OF assms] by auto
+ where "steps0 (1, [Bk], <[code M, n]>) H stp = (0, Bk \<up> i, [Oc])"
+ using h_case[of "M" "[n]", OF assms] by auto
then show "{pre_H_inv M n} H {post_H_unhalt_inv}"
unfolding Hoare_halt_def
apply(auto)
@@ -1323,12 +1197,12 @@
proof (cases rule: Hoare_plus_halt_simple)
case A_halt (* of tcopy *)
show "{P1} tcopy {P2}" unfolding P1_def P2_def
- by (simp) (rule tcopy_correct2)
+ by (rule tcopy_correct2)
next
case B_halt (* of H *)
show "{P2} H {P3}"
unfolding P2_def P3_def
- using assms by (simp) (rule H_halt_inv)
+ using assms by (rule H_halt_inv)
qed (simp)
(* {P3} dither {P3} *)
@@ -1377,12 +1251,12 @@
proof (cases rule: Hoare_plus_halt_simple)
case A_halt (* of tcopy *)
show "{P1} tcopy {P2}" unfolding P1_def P2_def
- by (simp) (rule tcopy_correct2)
+ by (rule tcopy_correct2)
next
case B_halt (* of H *)
then show "{P2} H {P3}"
unfolding P2_def P3_def
- using assms by (simp) (rule H_unhalt_inv)
+ using assms by (rule H_unhalt_inv)
qed (simp)
(* {P3} dither loops *)