--- a/thys/uncomputable.thy Tue Jan 29 12:37:06 2013 +0000
+++ b/thys/uncomputable.thy Tue Jan 29 13:00:51 2013 +0000
@@ -65,11 +65,11 @@
inv_begin4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
"inv_begin0 n (l, r) = ((n > 1 \<and> (l, r) = (Oc \<up> (n - 2), [Oc, Oc, Bk, Oc])) \<or>
- (n = 1 \<and> (l, r) = ([], [Bk, Oc, Bk, Oc])))"
+ (n = 1 \<and> (l, r) = ([], [Bk, Oc, Bk, Oc])))"
| "inv_begin1 n (l, r) = ((l, r) = ([], Oc \<up> n))"
| "inv_begin2 n (l, r) = (\<exists> i j. i > 0 \<and> i + j = n \<and> (l, r) = (Oc \<up> i, Oc \<up> j))"
| "inv_begin3 n (l, r) = (n > 0 \<and> (l, tl r) = (Bk # Oc \<up> n, []))"
-| "inv_begin4 n (l, r) = (n > 0 \<and> ((l, r) = (Oc \<up> n, [Bk, Oc]) \<or> (l, r) = (Oc \<up> (n - 1), [Oc, Bk, Oc])))"
+| "inv_begin4 n (l, r) = (n > 0 \<and> (l, r) = (Oc \<up> n, [Bk, Oc]) \<or> (l, r) = (Oc \<up> (n - 1), [Oc, Bk, Oc]))"
fun inv_begin :: "nat \<Rightarrow> config \<Rightarrow> bool"
where
@@ -83,11 +83,13 @@
lemma [elim]: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow>
\<exists>ia>0. ia + j - Suc 0 = i + j \<and> Oc # Oc \<up> i = Oc \<up> ia"
-apply(rule_tac x = "Suc i" in exI, simp)
-done
+by (rule_tac x = "Suc i" in exI, simp)
lemma inv_begin_step:
- "\<lbrakk>inv_begin x cf; x > 0\<rbrakk> \<Longrightarrow> inv_begin x (step cf (tcopy_begin, 0))"
+ assumes "inv_begin x cf"
+ and "x > 0"
+ shows "inv_begin x (step0 cf tcopy_begin)"
+using assms
unfolding tcopy_begin_def
apply(case_tac cf)
apply(auto simp: inv_begin.simps step.simps tcopy_begin_def numeral split: if_splits)
@@ -96,11 +98,14 @@
done
lemma inv_begin_steps:
- "\<lbrakk>inv_begin x (s, l, r); x > 0\<rbrakk>
- \<Longrightarrow> inv_begin x (steps (s, l, r) (tcopy_begin, 0) stp)"
-apply(induct stp, simp add: steps.simps)
+ assumes "inv_begin x cf"
+ and "x > 0"
+ shows "inv_begin x (steps0 cf tcopy_begin stp)"
+apply(induct stp)
+apply(simp add: steps.simps assms)
apply(auto simp: step_red)
-apply(rule_tac inv_begin_step, simp_all)
+apply(rule_tac inv_begin_step)
+apply(simp_all add: assms)
done
fun begin_state :: "config \<Rightarrow> nat"
@@ -136,28 +141,28 @@
by(auto intro:wf_inv_image simp:begin_LE_def lex_pair_def)
lemma begin_halt:
- "x > 0 \<Longrightarrow> \<exists> stp. is_final (steps0 (Suc 0, [], Oc\<up>x) tcopy_begin stp)"
+ "x > 0 \<Longrightarrow> \<exists> stp. is_final (steps0 (1, [], Oc\<up>x) tcopy_begin stp)"
proof(rule_tac LE = begin_LE in halt_lemma)
show "wf begin_LE" by(simp add: wf_begin_le)
next
assume h: "0 < x"
- show "\<forall>n. \<not> is_final (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<longrightarrow>
- (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) (Suc n),
- steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> begin_LE"
+ show "\<forall>n. \<not> is_final (steps (1, [], Oc \<up> x) (tcopy_begin, 0) n) \<longrightarrow>
+ (steps (1, [], Oc \<up> x) (tcopy_begin, 0) (Suc n),
+ steps (1, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> begin_LE"
proof(rule_tac allI, rule_tac impI)
fix n
- assume a: "\<not> is_final (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n)"
- have b: "inv_begin x (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n)"
+ assume a: "\<not> is_final (steps (1, [], Oc \<up> x) (tcopy_begin, 0) n)"
+ have b: "inv_begin x (steps (1, [], Oc \<up> x) (tcopy_begin, 0) n)"
apply(rule_tac inv_begin_steps)
apply(simp_all add: inv_begin.simps h)
done
- obtain s l r where c: "(steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) = (s, l, r)"
- apply(case_tac "steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n", auto)
+ obtain s l r where c: "(steps (1, [], Oc \<up> x) (tcopy_begin, 0) n) = (s, l, r)"
+ apply(case_tac "steps (1, [], Oc \<up> x) (tcopy_begin, 0) n", auto)
done
moreover hence "inv_begin x (s, l, r)"
using c b by simp
- ultimately show "(steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) (Suc n),
- steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> begin_LE"
+ ultimately show "(steps (1, [], Oc \<up> x) (tcopy_begin, 0) (Suc n),
+ steps (1, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> begin_LE"
using a
proof(simp del: inv_begin.simps)
assume "inv_begin x (s, l, r)" "0 < s"
@@ -174,10 +179,10 @@
proof(rule_tac Hoare_haltI)
fix l r
assume h: "0 < x" "inv_begin1 x (l, r)"
- hence "\<exists> stp. is_final (steps0 (Suc 0, [], Oc \<up> x) tcopy_begin stp)"
+ hence "\<exists> stp. is_final (steps0 (1, [], Oc \<up> x) tcopy_begin stp)"
by (rule_tac begin_halt)
- then obtain stp where "is_final (steps (Suc 0, [], Oc\<up>x) (tcopy_begin, 0) stp)" ..
- moreover have "inv_begin x (steps (Suc 0, [], Oc\<up>x) (tcopy_begin, 0) stp)"
+ then obtain stp where "is_final (steps (1, [], Oc\<up>x) (tcopy_begin, 0) stp)" ..
+ moreover have "inv_begin x (steps (1, [], Oc\<up>x) (tcopy_begin, 0) stp)"
apply(rule_tac inv_begin_steps)
using h by(simp_all add: inv_begin.simps)
ultimately show
@@ -185,7 +190,7 @@
inv_begin0 x holds_for steps (1, l, r) (tcopy_begin, 0) n"
using h
apply(rule_tac x = stp in exI)
- apply(case_tac "(steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) stp)", simp add: inv_begin.simps)
+ apply(case_tac "(steps (1, [], Oc \<up> x) (tcopy_begin, 0) stp)", simp add: inv_begin.simps)
done
qed