--- a/thys/uncomputable.thy Fri Jan 25 15:57:58 2013 +0100
+++ b/thys/uncomputable.thy Fri Jan 25 21:15:09 2013 +0000
@@ -64,24 +64,23 @@
inv_init3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
inv_init4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
- "inv_init0 x (l, r) = ((x > 1 \<and> l = Oc \<up> (x - 2) \<and> r = [Oc, Oc, Bk, Oc]) \<or>
- (x = 1 \<and> l = [] \<and> r = [Bk, Oc, Bk, Oc]))"
-| "inv_init1 x (l, r) = (l = [] \<and> r = Oc \<up> x)"
-| "inv_init2 x (l, r) = (\<exists> i j. i > 0 \<and> i + j = x \<and> l = Oc \<up> i \<and> r = Oc \<up> j)"
-| "inv_init3 x (l, r) = (x > 0 \<and> l = Bk # Oc \<up> x \<and> tl r = [])"
-| "inv_init4 x (l, r) = (x > 0 \<and> ((l = Oc \<up> x \<and> r = [Bk, Oc]) \<or> (l = Oc \<up> (x - 1) \<and> r = [Oc, Bk, Oc])))"
+ "inv_init0 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])))"
+| "inv_init1 n (l, r) = ((l, r) = ([], Oc \<up> n))"
+| "inv_init2 n (l, r) = (\<exists> i j. i > 0 \<and> i + j = n \<and> (l, r) = (Oc \<up> i, Oc \<up> j))"
+| "inv_init3 n (l, r) = (n > 0 \<and> (l, tl r) = (Bk # Oc \<up> n, []))"
+| "inv_init4 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_init :: "nat \<Rightarrow> config \<Rightarrow> bool"
where
- "inv_init x (s, l, r) =
- (if s = 0 then inv_init0 x (l, r)
- else if s = 1 then inv_init1 x (l, r)
- else if s = 2 then inv_init2 x (l, r)
- else if s = 3 then inv_init3 x (l, r)
- else if s = 4 then inv_init4 x (l, r)
+ "inv_init n (s, l, r) =
+ (if s = 0 then inv_init0 n (l, r) else
+ if s = 1 then inv_init1 n (l, r) else
+ if s = 2 then inv_init2 n (l, r) else
+ if s = 3 then inv_init3 n (l, r) else
+ if s = 4 then inv_init4 n (l, r)
else False)"
-declare inv_init.simps[simp del]
lemma [elim]: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow>
@@ -109,20 +108,19 @@
fun init_state :: "config \<Rightarrow> nat"
where
- "init_state (s, l, r) = (if s = 0 then 0
- else 5 - s)"
+ "init_state (s, l, r) = (if s = 0 then 0 else 5 - s)"
fun init_step :: "config \<Rightarrow> nat"
where
- "init_step (s, l, r) = (if s = 2 then length r
- else if s = 3 then if r = [] \<or> r = [Bk] then Suc 0 else 0
- else if s = 4 then length l
- else 0)"
+ "init_step (s, l, r) =
+ (if s = 2 then length r else
+ if s = 3 then (if r = [] \<or> r = [Bk] then 1 else 0) else
+ if s = 4 then length l
+ else 0)"
fun init_measure :: "config \<Rightarrow> nat \<times> nat"
where
- "init_measure c =
- (init_state c, init_step c)"
+ "init_measure c = (init_state c, init_step c)"
definition lex_pair :: "((nat \<times> nat) \<times> nat \<times> nat) set"
@@ -131,11 +129,11 @@
definition init_LE :: "(config \<times> config) set"
where
- "init_LE \<equiv> (inv_image lex_pair init_measure)"
+ "init_LE \<equiv> (inv_image lex_pair init_measure)"
lemma [simp]: "\<lbrakk>tl r = []; r \<noteq> []; r \<noteq> [Bk]\<rbrakk> \<Longrightarrow> r = [Oc]"
-apply(case_tac r, auto, case_tac a, auto)
-done
+by (case_tac r, auto, case_tac a, auto)
+
lemma wf_init_le: "wf init_LE"
by(auto intro:wf_inv_image simp:init_LE_def lex_pair_def)
@@ -164,11 +162,10 @@
ultimately show "(steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) (Suc n),
steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n) \<in> init_LE"
using a
- proof(simp)
+ proof(simp del: inv_init.simps)
assume "inv_init x (s, l, r)" "0 < s"
thus "(step (s, l, r) (tcopy_init, 0), s, l, r) \<in> init_LE"
- apply(auto simp: inv_init.simps init_LE_def lex_pair_def step.simps tcopy_init_def numeral
- split: if_splits)
+ apply(auto simp: init_LE_def lex_pair_def step.simps tcopy_init_def numeral split: if_splits)
apply(case_tac r, auto, case_tac a, auto)
done
qed
@@ -199,48 +196,31 @@
(* tcopy_loop *)
-fun inv_loop1_loop :: "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)"
-
-fun inv_loop1_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "inv_loop1_exit x (l, r) =
- (l = [] \<and> r = Bk # Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0 )"
-
-fun inv_loop1 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "inv_loop1 x (l, r) = (inv_loop1_loop x (l, r) \<or> inv_loop1_exit x (l, r))"
-
-fun inv_loop2 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "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)"
-
-fun inv_loop3 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "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)"
-
-fun inv_loop4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "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)"
-
-fun inv_loop5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+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_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"
where
- "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)"
-
-fun inv_loop5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "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)"
-
-fun inv_loop5 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "inv_loop5 x (l, r) = (inv_loop5_loop x (l, r) \<or>
- inv_loop5_exit x (l, r))"
+ "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
@@ -256,11 +236,6 @@
where
"inv_loop6 x (l, r) = (inv_loop6_loop x (l, r) \<or> inv_loop6_exit x (l, r))"
-fun inv_loop0 :: "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 )"
-
fun inv_loop :: "nat \<Rightarrow> config \<Rightarrow> bool"
where
"inv_loop x (s, l, r) =
@@ -277,21 +252,20 @@
inv_loop2.simps[simp del] inv_loop3.simps[simp del]
inv_loop4.simps[simp del] inv_loop5.simps[simp del]
inv_loop6.simps[simp del]
+
lemma [elim]: "Bk # list = Oc \<up> t \<Longrightarrow> RR"
-apply(case_tac t, auto)
-done
-
+by (case_tac t, auto)
lemma [simp]: "inv_loop1 x (b, []) = False"
by(simp add: inv_loop1.simps)
lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"
-apply(auto simp: inv_loop2.simps inv_loop3.simps)
-done
+by (auto simp: inv_loop2.simps inv_loop3.simps)
+
lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"
-apply(auto simp: inv_loop3.simps)
-done
+by (auto simp: inv_loop3.simps)
+
lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop5 x (b, [Oc])"
apply(auto simp: inv_loop4.simps inv_loop5.simps)
@@ -1070,10 +1044,10 @@
(* invariants of dither *)
abbreviation
- "dither_halt_inv \<equiv> \<lambda>(l, r). (\<exists>n. l = Bk \<up> n) \<and> r = [Oc, Oc]"
+ "dither_halt_inv \<equiv> \<lambda>(l, r). (\<exists>n. (l, r) = (Bk \<up> n, [Oc, Oc]))"
abbreviation
- "dither_unhalt_inv \<equiv> \<lambda>(l, r). (\<exists>n. l = Bk \<up> n) \<and> r = [Oc]"
+ "dither_unhalt_inv \<equiv> \<lambda>(l, r). (\<exists>n. (l, r) = (Bk \<up> n, [Oc]))"
lemma dither_loops_aux:
"(steps0 (1, Bk \<up> m, [Oc]) dither stp = (1, Bk \<up> m, [Oc])) \<or>
@@ -1330,9 +1304,9 @@
shows "False"
proof -
(* invariants *)
- def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [] \<and> r = <[code_tcontra]>)"
- def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[code_tcontra, code_tcontra]>)"
- def P3 \<equiv> "\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc]"
+ def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l, r) = ([], <[code_tcontra]>)"
+ def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l, r) = ([Bk], <[code_tcontra, code_tcontra]>)"
+ def P3 \<equiv> "\<lambda>(l, r). (\<exists>n. (l, r) = (Bk \<up> n, [Oc, Oc]))"
(*
{P1} tcopy {P2} {P2} H {P3}
@@ -1349,12 +1323,12 @@
proof (cases rule: Hoare_plus_halt_simple)
case A_halt (* of tcopy *)
show "{P1} tcopy {P2}" unfolding P1_def P2_def
- by (rule tcopy_correct2)
+ by (simp) (rule tcopy_correct2)
next
case B_halt (* of H *)
show "{P2} H {P3}"
unfolding P2_def P3_def
- using assms by (rule H_halt_inv)
+ using assms by (simp) (rule H_halt_inv)
qed (simp)
(* {P3} dither {P3} *)
@@ -1384,9 +1358,9 @@
shows "False"
proof -
(* invariants *)
- def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [] \<and> r = <[code_tcontra]>)"
- def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[code_tcontra, code_tcontra]>)"
- def P3 \<equiv> "\<lambda>(l::cell list, r::cell list). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc]"
+ def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l, r) = ([], <[code_tcontra]>)"
+ def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l, r) = ([Bk], <[code_tcontra, code_tcontra]>)"
+ def P3 \<equiv> "\<lambda>(l::cell list, r::cell list). (\<exists>n. (l, r) = (Bk \<up> n, [Oc]))"
(*
{P1} tcopy {P2} {P2} H {P3}
@@ -1403,12 +1377,12 @@
proof (cases rule: Hoare_plus_halt_simple)
case A_halt (* of tcopy *)
show "{P1} tcopy {P2}" unfolding P1_def P2_def
- by (rule tcopy_correct2)
+ by (simp) (rule tcopy_correct2)
next
case B_halt (* of H *)
then show "{P2} H {P3}"
unfolding P2_def P3_def
- using assms by (rule H_unhalt_inv)
+ using assms by (simp) (rule H_unhalt_inv)
qed (simp)
(* {P3} dither loops *)