168
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1
(* Title: thys/Uncomputable.thy
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 2
Author: Jian Xu, Xingyuan Zhang, and Christian Urban
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 3
*)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 4
168
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 5
header {* Undeciablity of the Halting Problem *}
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 6
163
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 7
theory Uncomputable
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 8
imports Turing_Hoare
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 9
begin
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 10
63
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 11
lemma numeral:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 12
shows "1 = Suc 0"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 13
and "2 = Suc 1"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 14
and "3 = Suc 2"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 15
and "4 = Suc 3"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 16
and "5 = Suc 4"
112
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 17
and "6 = Suc 5"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 18
and "7 = Suc 6"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 19
and "8 = Suc 7"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 20
and "9 = Suc 8"
168
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 21
and "10 = Suc 9"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 22
by simp_all
63
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 23
168
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 24
text {* The Copying TM, which duplicates its input. *}
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 25
68
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 26
definition
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 27
tcopy_begin :: "instr list"
68
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 28
where
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 29
"tcopy_begin \<equiv> [(W0, 0), (R, 2), (R, 3), (R, 2),
68
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 30
(W1, 3), (L, 4), (L, 4), (L, 0)]"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 31
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 32
definition
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 33
tcopy_loop :: "instr list"
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 34
where
68
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 35
"tcopy_loop \<equiv> [(R, 0), (R, 2), (R, 3), (W0, 2),
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 36
(R, 3), (R, 4), (W1, 5), (R, 4),
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 37
(L, 6), (L, 5), (L, 6), (L, 1)]"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 38
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 39
definition
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 40
tcopy_end :: "instr list"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 41
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 42
"tcopy_end \<equiv> [(L, 0), (R, 2), (W1, 3), (L, 4),
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 43
(R, 2), (R, 2), (L, 5), (W0, 4),
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 44
(R, 0), (L, 5)]"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 45
92
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 46
definition
68
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 47
tcopy :: "instr list"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 48
where
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 49
"tcopy \<equiv> (tcopy_begin |+| tcopy_loop) |+| tcopy_end"
68
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 51
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 52
(* tcopy_begin *)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 53
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 54
fun
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 55
inv_begin0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 56
inv_begin1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 57
inv_begin2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 58
inv_begin3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 59
inv_begin4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 60
where
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 61
"inv_begin0 n (l, r) = ((n > 1 \<and> (l, r) = (Oc \<up> (n - 2), [Oc, Oc, Bk, Oc])) \<or>
95
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 62
(n = 1 \<and> (l, r) = ([], [Bk, Oc, Bk, Oc])))"
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 63
| "inv_begin1 n (l, r) = ((l, r) = ([], Oc \<up> n))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 64
| "inv_begin2 n (l, r) = (\<exists> i j. i > 0 \<and> i + j = n \<and> (l, r) = (Oc \<up> i, Oc \<up> j))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 65
| "inv_begin3 n (l, r) = (n > 0 \<and> (l, tl r) = (Bk # Oc \<up> n, []))"
95
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 66
| "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]))"
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 67
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 68
fun inv_begin :: "nat \<Rightarrow> config \<Rightarrow> bool"
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 69
where
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 70
"inv_begin n (s, tp) =
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 71
(if s = 0 then inv_begin0 n tp else
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 72
if s = 1 then inv_begin1 n tp else
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 73
if s = 2 then inv_begin2 n tp else
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 74
if s = 3 then inv_begin3 n tp else
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 75
if s = 4 then inv_begin4 n tp
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 76
else False)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 77
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 78
lemma [elim]: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 79
\<exists>ia>0. ia + j - Suc 0 = i + j \<and> Oc # Oc \<up> i = Oc \<up> ia"
95
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 80
by (rule_tac x = "Suc i" in exI, simp)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 81
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 82
lemma inv_begin_step:
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 83
assumes "inv_begin n cf"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 84
and "n > 0"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 85
shows "inv_begin n (step0 cf tcopy_begin)"
95
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 86
using assms
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 87
unfolding tcopy_begin_def
168
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 88
apply(cases cf)
96
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 89
apply(auto simp: numeral split: if_splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 90
apply(case_tac "hd c")
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 91
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 92
apply(case_tac c)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 93
apply(simp_all)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 94
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 95
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 96
lemma inv_begin_steps:
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 97
assumes "inv_begin n cf"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 98
and "n > 0"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 99
shows "inv_begin n (steps0 cf tcopy_begin stp)"
95
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 100
apply(induct stp)
96
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 101
apply(simp add: assms)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 102
apply(auto simp del: steps.simps)
95
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 103
apply(rule_tac inv_begin_step)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 104
apply(simp_all add: assms)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 105
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 106
102
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 107
lemma begin_partial_correctness:
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 108
assumes "is_final (steps0 (1, [], Oc \<up> n) tcopy_begin stp)"
103
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 109
shows "0 < n \<Longrightarrow> {inv_begin1 n} tcopy_begin {inv_begin0 n}"
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 110
proof(rule_tac Hoare_haltI)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 111
fix l r
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 112
assume h: "0 < n" "inv_begin1 n (l, r)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 113
have "inv_begin n (steps0 (1, [], Oc \<up> n) tcopy_begin stp)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 114
using h by (rule_tac inv_begin_steps) (simp_all add: inv_begin.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 115
then show
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 116
"\<exists>stp. is_final (steps0 (1, l, r) tcopy_begin stp) \<and>
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 117
inv_begin0 n holds_for steps (1, l, r) (tcopy_begin, 0) stp"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 118
using h assms
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 119
apply(rule_tac x = stp in exI)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 120
apply(case_tac "(steps0 (1, [], Oc \<up> n) tcopy_begin stp)", simp add: inv_begin.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 121
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 122
qed
102
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 123
96
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 124
fun measure_begin_state :: "config \<Rightarrow> nat"
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 125
where
96
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 126
"measure_begin_state (s, l, r) = (if s = 0 then 0 else 5 - s)"
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 127
96
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 128
fun measure_begin_step :: "config \<Rightarrow> nat"
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 129
where
96
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 130
"measure_begin_step (s, l, r) =
81
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 131
(if s = 2 then length r else
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 132
if s = 3 then (if r = [] \<or> r = [Bk] then 1 else 0) else
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 133
if s = 4 then length l
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 134
else 0)"
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 135
96
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 136
definition
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 137
"measure_begin = measures [measure_begin_state, measure_begin_step]"
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 138
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 139
lemma wf_measure_begin:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 140
shows "wf measure_begin"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 141
unfolding measure_begin_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 142
by auto
81
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 143
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 144
lemma measure_begin_induct [case_names Step]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 145
"\<lbrakk>\<And>n. \<not> P (f n) \<Longrightarrow> (f (Suc n), (f n)) \<in> measure_begin\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 146
using wf_measure_begin
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 147
by (metis wf_iff_no_infinite_down_chain)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 148
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 149
lemma begin_halts:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 150
assumes h: "x > 0"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 151
shows "\<exists> stp. is_final (steps0 (1, [], Oc \<up> x) tcopy_begin stp)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 152
proof (induct rule: measure_begin_induct)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 153
case (Step n)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 154
have "\<not> is_final (steps0 (1, [], Oc \<up> x) tcopy_begin n)" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 155
moreover
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 156
have "inv_begin x (steps0 (1, [], Oc \<up> x) tcopy_begin n)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 157
by (rule_tac inv_begin_steps) (simp_all add: inv_begin.simps h)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 158
moreover
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 159
obtain s l r where eq: "(steps0 (1, [], Oc \<up> x) tcopy_begin n) = (s, l, r)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 160
by (metis measure_begin_state.cases)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 161
ultimately
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 162
have "(step0 (s, l, r) tcopy_begin, s, l, r) \<in> measure_begin"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 163
apply(auto simp: measure_begin_def tcopy_begin_def numeral split: if_splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 164
apply(subgoal_tac "r = [Oc]")
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 165
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 166
by (metis cell.exhaust list.exhaust tl.simps(2))
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 167
then
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 168
show "(steps0 (1, [], Oc \<up> x) tcopy_begin (Suc n), steps0 (1, [], Oc \<up> x) tcopy_begin n) \<in> measure_begin"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 169
using eq by (simp only: step_red)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 170
qed
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 171
94
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 172
lemma begin_correct:
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 173
shows "0 < n \<Longrightarrow> {inv_begin1 n} tcopy_begin {inv_begin0 n}"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 174
using begin_partial_correctness begin_halts by blast
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 175
96
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 176
declare tm_comp.simps [simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 177
declare adjust.simps[simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 178
declare shift.simps[simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 179
declare tm_wf.simps[simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 180
declare step.simps[simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 181
declare steps.simps[simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 182
68
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 183
(* tcopy_loop *)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 184
81
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 185
fun
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 186
inv_loop1_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 187
inv_loop1_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 188
inv_loop5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 189
inv_loop5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 190
inv_loop6_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 191
inv_loop6_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 192
where
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 193
"inv_loop1_loop n (l, r) = (\<exists> i j. i + j + 1 = n \<and> (l, r) = (Oc\<up>i, Oc#Oc#Bk\<up>j @ Oc\<up>j) \<and> j > 0)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 194
| "inv_loop1_exit n (l, r) = (0 < n \<and> (l, r) = ([], Bk#Oc#Bk\<up>n @ Oc\<up>n))"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 195
| "inv_loop5_loop x (l, r) =
84
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 196
(\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> k + t = j \<and> t > 0 \<and> (l, r) = (Oc\<up>k@Bk\<up>j@Oc\<up>i, Oc\<up>t))"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 197
| "inv_loop5_exit x (l, r) =
84
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 198
(\<exists> i j. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> (l, r) = (Bk\<up>(j - 1)@Oc\<up>i, Bk # Oc\<up>j))"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 199
| "inv_loop6_loop x (l, r) =
84
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 200
(\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> k + t + 1 = j \<and> (l, r) = (Bk\<up>k @ Oc\<up>i, Bk\<up>(Suc t) @ Oc\<up>j))"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 201
| "inv_loop6_exit x (l, r) =
84
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 202
(\<exists> i j. i + j = x \<and> j > 0 \<and> (l, r) = (Oc\<up>i, Oc#Bk\<up>j @ Oc\<up>j))"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 203
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 204
fun
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 205
inv_loop0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
81
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 206
inv_loop1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 207
inv_loop2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 208
inv_loop3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 209
inv_loop4 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 210
inv_loop5 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 211
inv_loop6 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 212
where
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 213
"inv_loop0 n (l, r) = (0 < n \<and> (l, r) = ([Bk], Oc # Bk\<up>n @ Oc\<up>n))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 214
| "inv_loop1 n (l, r) = (inv_loop1_loop n (l, r) \<or> inv_loop1_exit n (l, r))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 215
| "inv_loop2 n (l, r) = (\<exists> i j any. i + j = n \<and> n > 0 \<and> i > 0 \<and> j > 0 \<and> (l, r) = (Oc\<up>i, any#Bk\<up>j@Oc\<up>j))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 216
| "inv_loop3 n (l, r) =
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 217
(\<exists> i j k t. i + j = n \<and> i > 0 \<and> j > 0 \<and> k + t = Suc j \<and> (l, r) = (Bk\<up>k@Oc\<up>i, Bk\<up>t@Oc\<up>j))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 218
| "inv_loop4 n (l, r) =
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 219
(\<exists> i j k t. i + j = n \<and> i > 0 \<and> j > 0 \<and> k + t = j \<and> (l, r) = (Oc\<up>k @ Bk\<up>(Suc j)@Oc\<up>i, Oc\<up>t))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 220
| "inv_loop5 n (l, r) = (inv_loop5_loop n (l, r) \<or> inv_loop5_exit n (l, r))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 221
| "inv_loop6 n (l, r) = (inv_loop6_loop n (l, r) \<or> inv_loop6_exit n (l, r))"
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 222
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 223
fun inv_loop :: "nat \<Rightarrow> config \<Rightarrow> bool"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 224
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 225
"inv_loop x (s, l, r) =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 226
(if s = 0 then inv_loop0 x (l, r)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 227
else if s = 1 then inv_loop1 x (l, r)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 228
else if s = 2 then inv_loop2 x (l, r)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 229
else if s = 3 then inv_loop3 x (l, r)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 230
else if s = 4 then inv_loop4 x (l, r)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 231
else if s = 5 then inv_loop5 x (l, r)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 232
else if s = 6 then inv_loop6 x (l, r)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 233
else False)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 234
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 235
declare inv_loop.simps[simp del] inv_loop1.simps[simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 236
inv_loop2.simps[simp del] inv_loop3.simps[simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 237
inv_loop4.simps[simp del] inv_loop5.simps[simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 238
inv_loop6.simps[simp del]
81
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 239
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 240
lemma [elim]: "Bk # list = Oc \<up> t \<Longrightarrow> RR"
81
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 241
by (case_tac t, auto)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 242
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 243
lemma [simp]: "inv_loop1 x (b, []) = False"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 244
by (simp add: inv_loop1.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 245
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 246
lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"
81
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 247
by (auto simp: inv_loop2.simps inv_loop3.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 248
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 249
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 250
lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"
81
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 251
by (auto simp: inv_loop3.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 252
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 253
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 254
lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop5 x (b, [Oc])"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 255
apply(auto simp: inv_loop4.simps inv_loop5.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 256
apply(rule_tac [!] x = i in exI,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 257
rule_tac [!] x = "Suc j" in exI, simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 258
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 259
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 260
lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x ([], [])\<rbrakk> \<Longrightarrow> RR"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 261
by (auto simp: inv_loop4.simps inv_loop5.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 262
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 263
lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x (b, []); b \<noteq> []\<rbrakk> \<Longrightarrow> RR"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 264
by (auto simp: inv_loop4.simps inv_loop5.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 265
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 266
lemma [elim]: "inv_loop6 x ([], []) \<Longrightarrow> RR"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 267
by (auto simp: inv_loop6.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 268
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 269
lemma [elim]: "inv_loop6 x (b, []) \<Longrightarrow> RR"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 270
by (auto simp: inv_loop6.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 272
lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> b = []"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 273
by (auto simp: inv_loop1.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 274
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 275
lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> list = Oc # Bk \<up> x @ Oc \<up> x"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 276
by (auto simp: inv_loop1.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 277
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 278
lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, list)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 279
apply(auto simp: inv_loop2.simps inv_loop3.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 280
apply(rule_tac [!] x = i in exI, rule_tac [!] x = j in exI, simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 281
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 282
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 283
lemma [elim]: "Bk # list = Oc \<up> j \<Longrightarrow> RR"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 284
by (case_tac j, simp_all)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 285
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 286
lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, list)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 287
apply(auto simp: inv_loop3.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 288
apply(rule_tac [!] x = i in exI,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 289
rule_tac [!] x = j in exI, simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 290
apply(case_tac [!] t, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 291
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 292
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 293
lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop5 x (b, Oc # list)"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 294
by (auto simp: inv_loop4.simps inv_loop5.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 295
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 296
lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 297
by (auto simp: inv_loop6.simps inv_loop5.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 298
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 299
lemma [simp]: "inv_loop5_loop x (b, Bk # list) = False"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 300
by (auto simp: inv_loop5.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 301
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 302
lemma [simp]: "inv_loop6_exit x (b, Bk # list) = False"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 303
by (auto simp: inv_loop6.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 304
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 305
declare inv_loop5_loop.simps[simp del] inv_loop5_exit.simps[simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 306
inv_loop6_loop.simps[simp del] inv_loop6_exit.simps[simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 307
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 308
lemma [elim]:"\<lbrakk>0 < x; inv_loop5_exit x (b, Bk # list); b \<noteq> []; hd b = Bk\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 309
\<Longrightarrow> inv_loop6_loop x (tl b, Bk # Bk # list)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 310
apply(simp only: inv_loop5_exit.simps inv_loop6_loop.simps )
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 311
apply(erule_tac exE)+
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 312
apply(rule_tac x = i in exI,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 313
rule_tac x = j in exI,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 314
rule_tac x = "j - Suc (Suc 0)" in exI,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 315
rule_tac x = "Suc 0" in exI, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 316
apply(case_tac [!] j, simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 317
apply(case_tac [!] nat, simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 318
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 319
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 320
lemma [simp]: "inv_loop6_loop x (b, Oc # Bk # list) = False"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 321
by (auto simp: inv_loop6_loop.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 322
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 323
lemma [elim]: "\<lbrakk>x > 0; inv_loop5_exit x (b, Bk # list); b \<noteq> []; hd b = Oc\<rbrakk> \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 324
inv_loop6_exit x (tl b, Oc # Bk # list)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 325
apply(simp only: inv_loop5_exit.simps inv_loop6_exit.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 326
apply(erule_tac exE)+
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 327
apply(rule_tac x = "x - 1" in exI, rule_tac x = 1 in exI, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 328
apply(case_tac j, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 329
apply(case_tac [!] nat, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 330
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 331
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 332
lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop6 x (tl b, hd b # Bk # list)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 333
apply(simp add: inv_loop5.simps inv_loop6.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 334
apply(case_tac "hd b", simp_all, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 335
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 336
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 337
lemma [simp]: "inv_loop6 x ([], Bk # xs) = False"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 338
apply(simp add: inv_loop6.simps inv_loop6_loop.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 339
inv_loop6_exit.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 340
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 341
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 342
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 343
lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 344
by (simp)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 345
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 346
lemma [simp]: "inv_loop6_exit x (b, Bk # list) = False"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 347
by (simp add: inv_loop6_exit.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 348
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 349
lemma [elim]: "\<lbrakk>0 < x; inv_loop6_loop x (b, Bk # list); b \<noteq> []; hd b = Bk\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 350
\<Longrightarrow> inv_loop6_loop x (tl b, Bk # Bk # list)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 351
apply(simp only: inv_loop6_loop.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 352
apply(erule_tac exE)+
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 353
apply(rule_tac x = i in exI, rule_tac x = j in exI,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 354
rule_tac x = "k - 1" in exI, rule_tac x = "Suc t" in exI, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 355
apply(case_tac [!] k, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 356
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 357
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 358
lemma [elim]: "\<lbrakk>0 < x; inv_loop6_loop x (b, Bk # list); b \<noteq> []; hd b = Oc\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 359
\<Longrightarrow> inv_loop6_exit x (tl b, Oc # Bk # list)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 360
apply(simp only: inv_loop6_loop.simps inv_loop6_exit.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 361
apply(erule_tac exE)+
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 362
apply(rule_tac x = "i - 1" in exI, rule_tac x = j in exI, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 363
apply(case_tac [!] k, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 364
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 365
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 366
lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop6 x (tl b, hd b # Bk # list)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 367
apply(simp add: inv_loop6.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 368
apply(case_tac "hd b", simp_all, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 369
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 370
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 371
lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop2 x (Oc # b, list)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 372
apply(auto simp: inv_loop1.simps inv_loop2.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 373
apply(rule_tac x = "Suc i" in exI, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 374
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 375
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 376
lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop2 x (b, Bk # list)"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 377
by (auto simp: inv_loop2.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 378
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 379
lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop4 x (Oc # b, list)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 380
apply(auto simp: inv_loop3.simps inv_loop4.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 381
apply(rule_tac [!] x = i in exI, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 382
apply(rule_tac [!] x = "Suc 0" in exI, rule_tac [!] x = "j - 1" in exI, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 383
apply(case_tac [!] t, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 384
apply(case_tac [!] j, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 385
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 386
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 387
lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop4 x (Oc # b, list)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 388
apply(auto simp: inv_loop4.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 389
apply(rule_tac [!] x = "i" in exI, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 390
apply(rule_tac [!] x = "Suc k" in exI, rule_tac [!] x = "t - 1" in exI, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 391
apply(case_tac [!] t, simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 392
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 393
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 394
lemma [simp]: "inv_loop5 x ([], list) = False"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 395
by (auto simp: inv_loop5.simps inv_loop5_exit.simps inv_loop5_loop.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 396
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 397
lemma [simp]: "inv_loop5_exit x (b, Oc # list) = False"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 398
by (auto simp: inv_loop5_exit.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 399
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 400
lemma [elim]: " \<lbrakk>inv_loop5_loop x (b, Oc # list); b \<noteq> []; hd b = Bk\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 401
\<Longrightarrow> inv_loop5_exit x (tl b, Bk # Oc # list)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 402
apply(simp only: inv_loop5_loop.simps inv_loop5_exit.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 403
apply(erule_tac exE)+
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 404
apply(rule_tac x = i in exI, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 405
apply(case_tac [!] k, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 406
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 407
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 408
lemma [elim]: "\<lbrakk>inv_loop5_loop x (b, Oc # list); b \<noteq> []; hd b = Oc\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 409
\<Longrightarrow> inv_loop5_loop x (tl b, Oc # Oc # list)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 410
apply(simp only: inv_loop5_loop.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 411
apply(erule_tac exE)+
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 412
apply(rule_tac x = i in exI, rule_tac x = j in exI)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 413
apply(rule_tac x = "k - 1" in exI, rule_tac x = "Suc t" in exI, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 414
apply(case_tac [!] k, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 415
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 416
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 417
lemma [elim]: "\<lbrakk>inv_loop5 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop5 x (tl b, hd b # Oc # list)"
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 418
apply(simp add: inv_loop5.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 419
apply(case_tac "hd b", simp_all, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 420
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 421
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 422
lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x ([], Oc # list)\<rbrakk> \<Longrightarrow> inv_loop1 x ([], Bk # Oc # list)"
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 423
apply(auto simp: inv_loop6.simps inv_loop1.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 424
inv_loop6_loop.simps inv_loop6_exit.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 425
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 426
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 427
lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x (b, Oc # list); b \<noteq> []\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 428
\<Longrightarrow> inv_loop1 x (tl b, hd b # Oc # list)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 429
apply(auto simp: inv_loop6.simps inv_loop1.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 430
inv_loop6_loop.simps inv_loop6_exit.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 431
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 432
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 433
lemma inv_loop_step:
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 434
"\<lbrakk>inv_loop x cf; x > 0\<rbrakk> \<Longrightarrow> inv_loop x (step cf (tcopy_loop, 0))"
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 435
apply(case_tac cf, case_tac c, case_tac [2] aa)
63
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 436
apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral split: if_splits)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 437
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 438
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 439
lemma inv_loop_steps:
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 440
"\<lbrakk>inv_loop x cf; x > 0\<rbrakk> \<Longrightarrow> inv_loop x (steps cf (tcopy_loop, 0) stp)"
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 441
apply(induct stp, simp add: steps.simps, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 442
apply(erule_tac inv_loop_step, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 443
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 444
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 445
fun loop_stage :: "config \<Rightarrow> nat"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 446
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 447
"loop_stage (s, l, r) = (if s = 0 then 0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 448
else (Suc (length (takeWhile (\<lambda>a. a = Oc) (rev l @ r)))))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 449
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 450
fun loop_state :: "config \<Rightarrow> nat"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 451
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 452
"loop_state (s, l, r) = (if s = 2 \<and> hd r = Oc then 0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 453
else if s = 1 then 1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 454
else 10 - s)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 455
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 456
fun loop_step :: "config \<Rightarrow> nat"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 457
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 458
"loop_step (s, l, r) = (if s = 3 then length r
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 459
else if s = 4 then length r
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 460
else if s = 5 then length l
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 461
else if s = 6 then length l
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 462
else 0)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 463
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 464
definition measure_loop :: "(config \<times> config) set"
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 465
where
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 466
"measure_loop = measures [loop_stage, loop_state, loop_step]"
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 467
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 468
lemma wf_measure_loop: "wf measure_loop"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 469
unfolding measure_loop_def
96
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 470
by (auto)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 471
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 472
lemma measure_loop_induct [case_names Step]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 473
"\<lbrakk>\<And>n. \<not> P (f n) \<Longrightarrow> (f (Suc n), (f n)) \<in> measure_loop\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 474
using wf_measure_loop
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 475
by (metis wf_iff_no_infinite_down_chain)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 476
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 477
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 478
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 479
lemma [simp]: "inv_loop2 x ([], b) = False"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 480
by (auto simp: inv_loop2.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 481
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 482
lemma [simp]: "inv_loop2 x (l', []) = False"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 483
by (auto simp: inv_loop2.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 484
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 485
lemma [simp]: "inv_loop3 x (b, []) = False"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 486
by (auto simp: inv_loop3.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 487
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 488
lemma [simp]: "inv_loop4 x ([], b) = False"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 489
by (auto simp: inv_loop4.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 490
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 491
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 492
lemma [elim]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 493
"\<lbrakk>inv_loop4 x (l', []); l' \<noteq> []; x > 0;
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 494
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ [Oc])) \<noteq>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 495
length (takeWhile (\<lambda>a. a = Oc) (rev l'))\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 496
\<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev l' @ [Oc])) < length (takeWhile (\<lambda>a. a = Oc) (rev l'))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 497
apply(auto simp: inv_loop4.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 498
apply(case_tac [!] j, simp_all add: List.takeWhile_tail)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 499
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 500
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 501
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 502
lemma [elim]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 503
"\<lbrakk>inv_loop4 x (l', Bk # list); l' \<noteq> []; 0 < x;
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 504
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list)) \<noteq>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 505
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 506
\<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list)) <
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 507
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 508
by (auto simp: inv_loop4.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 509
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 510
lemma takeWhile_replicate_append:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 511
"P a \<Longrightarrow> takeWhile P (a\<up>x @ ys) = a\<up>x @ takeWhile P ys"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 512
by (induct x, auto)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 513
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 514
lemma takeWhile_replicate:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 515
"P a \<Longrightarrow> takeWhile P (a\<up>x) = a\<up>x"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 516
by (induct x, auto)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 517
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 518
lemma [elim]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 519
"\<lbrakk>inv_loop5 x (l', Bk # list); l' \<noteq> []; 0 < x;
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 520
length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) \<noteq>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 521
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 522
\<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) <
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 523
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 524
apply(auto simp: inv_loop5.simps inv_loop5_exit.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 525
apply(case_tac [!] j, simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 526
apply(case_tac [!] "nat", simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 527
apply(case_tac nata, simp_all add: List.takeWhile_tail)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 528
apply(simp add: takeWhile_replicate_append takeWhile_replicate)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 529
apply(case_tac nata, simp_all add: List.takeWhile_tail)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 530
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 531
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 532
lemma [elim]: "\<lbrakk>inv_loop1 x (l', Oc # list)\<rbrakk> \<Longrightarrow> hd list = Oc"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 533
by (auto simp: inv_loop1.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 534
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 535
lemma [elim]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 536
"\<lbrakk>inv_loop6 x (l', Bk # list); l' \<noteq> []; 0 < x;
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 537
length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) \<noteq>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 538
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 539
\<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) <
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 540
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 541
apply(auto simp: inv_loop6.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 542
apply(case_tac l', simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 543
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 544
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 545
lemma [elim]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 546
"\<lbrakk>inv_loop2 x (l', Oc # list); l' \<noteq> []; 0 < x\<rbrakk> \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 547
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list)) <
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 548
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 549
apply(auto simp: inv_loop2.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 550
apply(simp_all add: takeWhile_tail takeWhile_replicate_append
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 551
takeWhile_replicate)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 552
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 553
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 554
lemma [elim]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 555
"\<lbrakk>inv_loop5 x (l', Oc # list); l' \<noteq> []; 0 < x;
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 556
length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list)) \<noteq>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 557
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 558
\<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list)) <
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 559
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 560
apply(auto simp: inv_loop5.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 561
apply(case_tac l', auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 562
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 563
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 564
lemma[elim]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 565
"\<lbrakk>inv_loop6 x (l', Oc # list); l' \<noteq> []; 0 < x;
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 566
length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list))
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 567
\<noteq> length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 568
\<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list)) <
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 569
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 570
apply(case_tac l')
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 571
apply(auto simp: inv_loop6.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 572
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 573
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 574
lemma loop_halts:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 575
assumes h: "n > 0" "inv_loop n (1, l, r)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 576
shows "\<exists> stp. is_final (steps0 (1, l, r) tcopy_loop stp)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 577
proof (induct rule: measure_loop_induct)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 578
case (Step stp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 579
have "\<not> is_final (steps0 (1, l, r) tcopy_loop stp)" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 580
moreover
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 581
have "inv_loop n (steps0 (1, l, r) tcopy_loop stp)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 582
by (rule_tac inv_loop_steps) (simp_all only: h)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 583
moreover
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 584
obtain s l' r' where eq: "(steps0 (1, l, r) tcopy_loop stp) = (s, l', r')"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 585
by (metis measure_begin_state.cases)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 586
ultimately
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 587
have "(step0 (s, l', r') tcopy_loop, s, l', r') \<in> measure_loop"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 588
using h(1)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 589
apply(case_tac r')
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 590
apply(case_tac [2] a)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 591
apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral measure_loop_def split: if_splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 592
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 593
then
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 594
show "(steps0 (1, l, r) tcopy_loop (Suc stp), steps0 (1, l, r) tcopy_loop stp) \<in> measure_loop"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 595
using eq by (simp only: step_red)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 596
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 597
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 598
lemma loop_correct:
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 599
shows "0 < n \<Longrightarrow> {inv_loop1 n} tcopy_loop {inv_loop0 n}"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 600
using assms
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 601
proof(rule_tac Hoare_haltI)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 602
fix l r
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 603
assume h: "0 < n" "inv_loop1 n (l, r)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 604
then obtain stp where k: "is_final (steps0 (1, l, r) tcopy_loop stp)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 605
using loop_halts
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 606
apply(simp add: inv_loop.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 607
apply(blast)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 608
done
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 609
moreover
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 610
have "inv_loop n (steps0 (1, l, r) tcopy_loop stp)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 611
using h
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 612
by (rule_tac inv_loop_steps) (simp_all add: inv_loop.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 613
ultimately show
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 614
"\<exists>stp. is_final (steps0 (1, l, r) tcopy_loop stp) \<and>
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 615
inv_loop0 n holds_for steps0 (1, l, r) tcopy_loop stp"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 616
using h(1)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 617
apply(rule_tac x = stp in exI)
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 618
apply(case_tac "(steps0 (1, l, r) tcopy_loop stp)")
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 619
apply(simp add: inv_loop.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 620
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 621
qed
68
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 622
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 623
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 624
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 625
68
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 626
(* tcopy_end *)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 627
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 628
fun
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 629
inv_end5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 630
inv_end5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 631
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 632
"inv_end5_loop x (l, r) =
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 633
(\<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)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 634
| "inv_end5_exit x (l, r) = (x > 0 \<and> l = [] \<and> r = Bk # Oc\<up>x @ Bk # Oc\<up>x)"
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 635
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 636
fun
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 637
inv_end0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 638
inv_end1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 639
inv_end2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 640
inv_end3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 641
inv_end4 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 642
inv_end5 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 643
where
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 644
"inv_end0 n (l, r) = (n > 0 \<and> (l, r) = ([Bk], Oc\<up>n @ Bk # Oc\<up>n))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 645
| "inv_end1 n (l, r) = (n > 0 \<and> (l, r) = ([Bk], Oc # Bk\<up>n @ Oc\<up>n))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 646
| "inv_end2 n (l, r) = (\<exists> i j. i + j = Suc n \<and> n > 0 \<and> l = Oc\<up>i @ [Bk] \<and> r = Bk\<up>j @ Oc\<up>n)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 647
| "inv_end3 n (l, r) =
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 648
(\<exists> i j. n > 0 \<and> i + j = n \<and> l = Oc\<up>i @ [Bk] \<and> r = Oc # Bk\<up>j@ Oc\<up>n)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 649
| "inv_end4 n (l, r) = (\<exists> any. n > 0 \<and> l = Oc\<up>n @ [Bk] \<and> r = any#Oc\<up>n)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 650
| "inv_end5 n (l, r) = (inv_end5_loop n (l, r) \<or> inv_end5_exit n (l, r))"
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 651
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 652
fun
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 653
inv_end :: "nat \<Rightarrow> config \<Rightarrow> bool"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 654
where
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 655
"inv_end n (s, l, r) = (if s = 0 then inv_end0 n (l, r)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 656
else if s = 1 then inv_end1 n (l, r)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 657
else if s = 2 then inv_end2 n (l, r)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 658
else if s = 3 then inv_end3 n (l, r)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 659
else if s = 4 then inv_end4 n (l, r)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 660
else if s = 5 then inv_end5 n (l, r)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 661
else False)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 662
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 663
declare inv_end.simps[simp del] inv_end1.simps[simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 664
inv_end0.simps[simp del] inv_end2.simps[simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 665
inv_end3.simps[simp del] inv_end4.simps[simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 666
inv_end5.simps[simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 667
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 668
lemma [simp]: "inv_end1 x (b, []) = False"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 669
by (auto simp: inv_end1.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 670
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 671
lemma [simp]: "inv_end2 x (b, []) = False"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 672
by (auto simp: inv_end2.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 673
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 674
lemma [simp]: "inv_end3 x (b, []) = False"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 675
by (auto simp: inv_end3.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 676
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 677
lemma [simp]: "inv_end4 x (b, []) = False"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 678
by (auto simp: inv_end4.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 679
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 680
lemma [simp]: "inv_end5 x (b, []) = False"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 681
by (auto simp: inv_end5.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 682
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 683
lemma [simp]: "inv_end1 x ([], list) = False"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 684
by (auto simp: inv_end1.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 685
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 686
lemma [elim]: "\<lbrakk>0 < x; inv_end1 x (b, Bk # list); b \<noteq> []\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 687
\<Longrightarrow> inv_end0 x (tl b, hd b # Bk # list)"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 688
by (auto simp: inv_end1.simps inv_end0.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 689
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 690
lemma [elim]: "\<lbrakk>0 < x; inv_end2 x (b, Bk # list)\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 691
\<Longrightarrow> inv_end3 x (b, Oc # list)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 692
apply(auto simp: inv_end2.simps inv_end3.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 693
apply(rule_tac x = "j - 1" in exI)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 694
apply(case_tac j, simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 695
apply(case_tac x, simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 696
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 697
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 698
lemma [elim]: "\<lbrakk>0 < x; inv_end3 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Bk # b, list)"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 699
by (auto simp: inv_end2.simps inv_end3.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 700
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 701
lemma [elim]: "\<lbrakk>0 < x; inv_end4 x ([], Bk # list)\<rbrakk> \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 702
inv_end5 x ([], Bk # Bk # list)"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 703
by (auto simp: inv_end4.simps inv_end5.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 704
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 705
lemma [elim]: "\<lbrakk>0 < x; inv_end4 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 706
inv_end5 x (tl b, hd b # Bk # list)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 707
apply(auto simp: inv_end4.simps inv_end5.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 708
apply(rule_tac x = 1 in exI, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 709
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 710
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 711
lemma [elim]: "\<lbrakk>0 < x; inv_end5 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_end0 x (Bk # b, list)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 712
apply(auto simp: inv_end5.simps inv_end0.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 713
apply(case_tac [!] j, simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 714
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 715
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 716
lemma [elim]: "\<lbrakk>0 < x; inv_end1 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Oc # b, list)"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 717
by (auto simp: inv_end1.simps inv_end2.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 718
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 719
lemma [elim]: "\<lbrakk>0 < x; inv_end2 x ([], Oc # list)\<rbrakk> \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 720
inv_end4 x ([], Bk # Oc # list)"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 721
by (auto simp: inv_end2.simps inv_end4.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 722
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 723
lemma [elim]: "\<lbrakk>0 < x; inv_end2 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 724
inv_end4 x (tl b, hd b # Oc # list)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 725
apply(auto simp: inv_end2.simps inv_end4.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 726
apply(case_tac [!] j, simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 727
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 728
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 729
lemma [elim]: "\<lbrakk>0 < x; inv_end3 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Oc # b, list)"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 730
by (auto simp: inv_end2.simps inv_end3.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 731
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 732
lemma [elim]: "\<lbrakk>0 < x; inv_end4 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end4 x (b, Bk # list)"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 733
by (auto simp: inv_end2.simps inv_end4.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 734
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 735
lemma [elim]: "\<lbrakk>0 < x; inv_end5 x ([], Oc # list)\<rbrakk> \<Longrightarrow> inv_end5 x ([], Bk # Oc # list)"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 736
by (auto simp: inv_end2.simps inv_end5.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 737
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 738
declare inv_end5_loop.simps[simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 739
inv_end5_exit.simps[simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 740
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 741
lemma [simp]: "inv_end5_exit x (b, Oc # list) = False"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 742
by (auto simp: inv_end5_exit.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 743
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 744
lemma [simp]: "inv_end5_loop x (tl b, Bk # Oc # list) = False"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 745
apply(auto simp: inv_end5_loop.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 746
apply(case_tac [!] j, simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 747
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 748
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 749
lemma [elim]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 750
"\<lbrakk>0 < x; inv_end5_loop x (b, Oc # list); b \<noteq> []; hd b = Bk\<rbrakk> \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 751
inv_end5_exit x (tl b, Bk # Oc # list)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 752
apply(auto simp: inv_end5_loop.simps inv_end5_exit.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 753
apply(case_tac [!] i, simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 754
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 755
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 756
lemma [elim]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 757
"\<lbrakk>0 < x; inv_end5_loop x (b, Oc # list); b \<noteq> []; hd b = Oc\<rbrakk> \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 758
inv_end5_loop x (tl b, Oc # Oc # list)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 759
apply(simp only: inv_end5_loop.simps inv_end5_exit.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 760
apply(erule_tac exE)+
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 761
apply(rule_tac x = "i - 1" in exI,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 762
rule_tac x = "Suc j" in exI, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 763
apply(case_tac [!] i, simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 764
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 765
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 766
lemma [elim]: "\<lbrakk>0 < x; inv_end5 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 767
inv_end5 x (tl b, hd b # Oc # list)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 768
apply(simp add: inv_end2.simps inv_end5.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 769
apply(case_tac "hd b", simp_all, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 770
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 771
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 772
lemma inv_end_step:
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 773
"\<lbrakk>x > 0; inv_end x cf\<rbrakk> \<Longrightarrow> inv_end x (step cf (tcopy_end, 0))"
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 774
apply(case_tac cf, case_tac c, case_tac [2] aa)
63
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 775
apply(auto simp: inv_end.simps step.simps tcopy_end_def numeral split: if_splits)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 776
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 777
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 778
lemma inv_end_steps:
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 779
"\<lbrakk>x > 0; inv_end x cf\<rbrakk> \<Longrightarrow> inv_end x (steps cf (tcopy_end, 0) stp)"
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 780
apply(induct stp, simp add:steps.simps, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 781
apply(erule_tac inv_end_step, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 782
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 783
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 784
fun end_state :: "config \<Rightarrow> nat"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 785
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 786
"end_state (s, l, r) =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 787
(if s = 0 then 0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 788
else if s = 1 then 5
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 789
else if s = 2 \<or> s = 3 then 4
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 790
else if s = 4 then 3
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 791
else if s = 5 then 2
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 792
else 0)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 793
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 794
fun end_stage :: "config \<Rightarrow> nat"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 795
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 796
"end_stage (s, l, r) =
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 797
(if s = 2 \<or> s = 3 then (length r) else 0)"
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 798
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 799
fun end_step :: "config \<Rightarrow> nat"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 800
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 801
"end_step (s, l, r) =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 802
(if s = 4 then (if hd r = Oc then 1 else 0)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 803
else if s = 5 then length l
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 804
else if s = 2 then 1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 805
else if s = 3 then 0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 806
else 0)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 807
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 808
definition end_LE :: "(config \<times> config) set"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 809
where
96
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 810
"end_LE = measures [end_state, end_stage, end_step]"
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 811
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 812
lemma wf_end_le: "wf end_LE"
96
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 813
unfolding end_LE_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 814
by (auto)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 815
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 816
lemma [simp]: "inv_end5 x ([], Oc # list) = False"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 817
by (auto simp: inv_end5.simps inv_end5_loop.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 818
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 819
lemma halt_lemma:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 820
"\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 821
by (metis wf_iff_no_infinite_down_chain)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 822
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 823
lemma end_halt:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 824
"\<lbrakk>x > 0; inv_end x (Suc 0, l, r)\<rbrakk> \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 825
\<exists> stp. is_final (steps (Suc 0, l, r) (tcopy_end, 0) stp)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 826
proof(rule_tac LE = end_LE in halt_lemma)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 827
show "wf end_LE" by(intro wf_end_le)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 828
next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 829
assume great: "0 < x"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 830
and inv_start: "inv_end x (Suc 0, l, r)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 831
show "\<forall>n. \<not> is_final (steps (Suc 0, l, r) (tcopy_end, 0) n) \<longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 832
(steps (Suc 0, l, r) (tcopy_end, 0) (Suc n), steps (Suc 0, l, r) (tcopy_end, 0) n) \<in> end_LE"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 833
proof(rule_tac allI, rule_tac impI)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 834
fix n
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 835
assume notfinal: "\<not> is_final (steps (Suc 0, l, r) (tcopy_end, 0) n)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 836
obtain s' l' r' where d: "steps (Suc 0, l, r) (tcopy_end, 0) n = (s', l', r')"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 837
apply(case_tac "steps (Suc 0, l, r) (tcopy_end, 0) n", auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 838
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 839
hence "inv_end x (s', l', r') \<and> s' \<noteq> 0"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 840
using great inv_start notfinal
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 841
apply(drule_tac stp = n in inv_end_steps, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 842
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 843
hence "(step (s', l', r') (tcopy_end, 0), s', l', r') \<in> end_LE"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 844
apply(case_tac r', case_tac [2] a)
96
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 845
apply(auto simp: inv_end.simps step.simps tcopy_end_def numeral end_LE_def split: if_splits)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 846
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 847
thus "(steps (Suc 0, l, r) (tcopy_end, 0) (Suc n),
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 848
steps (Suc 0, l, r) (tcopy_end, 0) n) \<in> end_LE"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 849
using d
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 850
by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 851
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 852
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 853
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 854
lemma end_correct:
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 855
"n > 0 \<Longrightarrow> {inv_end1 n} tcopy_end {inv_end0 n}"
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 856
proof(rule_tac Hoare_haltI)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 857
fix l r
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 858
assume h: "0 < n"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 859
"inv_end1 n (l, r)"
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 860
then have "\<exists> stp. is_final (steps0 (1, l, r) tcopy_end stp)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 861
by (simp add: end_halt inv_end.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 862
then obtain stp where "is_final (steps0 (1, l, r) tcopy_end stp)" ..
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 863
moreover have "inv_end n (steps0 (1, l, r) tcopy_end stp)"
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 864
apply(rule_tac inv_end_steps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 865
using h by(simp_all add: inv_end.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 866
ultimately show
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 867
"\<exists>stp. is_final (steps (1, l, r) (tcopy_end, 0) stp) \<and>
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 868
inv_end0 n holds_for steps (1, l, r) (tcopy_end, 0) stp"
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 869
using h
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 870
apply(rule_tac x = stp in exI)
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 871
apply(case_tac "(steps0 (1, l, r) tcopy_end stp)")
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 872
apply(simp add: inv_end.simps)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 873
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 874
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 875
68
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 876
(* tcopy *)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 877
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 878
lemma [intro]: "tm_wf (tcopy_begin, 0)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 879
by (auto simp: tm_wf.simps tcopy_begin_def)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 880
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 881
lemma [intro]: "tm_wf (tcopy_loop, 0)"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 882
by (auto simp: tm_wf.simps tcopy_loop_def)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 883
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 884
lemma [intro]: "tm_wf (tcopy_end, 0)"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 885
by (auto simp: tm_wf.simps tcopy_end_def)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 886
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 887
lemma tcopy_correct1:
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 888
assumes "0 < x"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 889
shows "{inv_begin1 x} tcopy {inv_end0 x}"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 890
proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 891
have "{inv_begin1 x} tcopy_begin {inv_begin0 x}"
94
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 892
by (metis assms begin_correct)
99
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 893
moreover
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 894
have "inv_begin0 x \<mapsto> inv_loop1 x"
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 895
unfolding assert_imp_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 896
unfolding inv_begin0.simps inv_loop1.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 897
unfolding inv_loop1_loop.simps inv_loop1_exit.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 898
apply(auto simp add: numeral Cons_eq_append_conv)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 899
by (rule_tac x = "Suc 0" in exI, auto)
99
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 900
ultimately have "{inv_begin1 x} tcopy_begin {inv_loop1 x}"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 901
by (rule_tac Hoare_consequence) (auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 902
moreover
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 903
have "{inv_loop1 x} tcopy_loop {inv_loop0 x}"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 904
by (metis assms loop_correct)
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 905
ultimately
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 906
have "{inv_begin1 x} (tcopy_begin |+| tcopy_loop) {inv_loop0 x}"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 907
by (rule_tac Hoare_plus_halt) (auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 908
moreover
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 909
have "{inv_end1 x} tcopy_end {inv_end0 x}"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 910
by (metis assms end_correct)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 911
moreover
99
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 912
have "inv_loop0 x = inv_end1 x"
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 913
by(auto simp: inv_end1.simps inv_loop1.simps assert_imp_def)
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 914
ultimately
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 915
show "{inv_begin1 x} tcopy {inv_end0 x}"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 916
unfolding tcopy_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 917
by (rule_tac Hoare_plus_halt) (auto)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 918
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 919
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 920
abbreviation (input)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 921
"pre_tcopy n \<equiv> \<lambda>tp. tp = ([]::cell list, <(n::nat)>)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 922
abbreviation (input)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 923
"post_tcopy n \<equiv> \<lambda>tp. tp= ([Bk], <(n, n::nat)>)"
69
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 924
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 925
lemma tcopy_correct:
69
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 926
shows "{pre_tcopy n} tcopy {post_tcopy n}"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 927
proof -
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 928
have "{inv_begin1 (Suc n)} tcopy {inv_end0 (Suc n)}"
69
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 929
by (rule tcopy_correct1) (simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 930
moreover
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 931
have "pre_tcopy n = inv_begin1 (Suc n)"
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 932
by (auto simp add: tape_of_nl_abv tape_of_nat_abv)
69
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 933
moreover
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 934
have "inv_end0 (Suc n) = post_tcopy n"
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 935
by (auto simp add: inv_end0.simps tape_of_nat_abv tape_of_nat_pair)
69
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 936
ultimately
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 937
show "{pre_tcopy n} tcopy {post_tcopy n}"
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 938
by simp
69
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 939
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 940
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 941
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 942
section {* The {\em Dithering} Turing Machine *}
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 943
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 944
text {*
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 945
The {\em Dithering} TM, when the input is @{text "1"}, it will loop forever, otherwise, it will
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 946
terminate.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 947
*}
66
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 948
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 949
definition dither :: "instr list"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 950
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 951
"dither \<equiv> [(W0, 1), (R, 2), (L, 1), (L, 0)] "
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 952
70
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 953
(* invariants of dither *)
94
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 954
abbreviation (input)
99
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 955
"dither_halt_inv \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"
70
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 956
94
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 957
abbreviation (input)
99
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 958
"dither_unhalt_inv \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"
70
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 959
80
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 960
lemma dither_loops_aux:
66
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 961
"(steps0 (1, Bk \<up> m, [Oc]) dither stp = (1, Bk \<up> m, [Oc])) \<or>
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 962
(steps0 (1, Bk \<up> m, [Oc]) dither stp = (2, Oc # Bk \<up> m, []))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 963
apply(induct stp)
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 964
apply(auto simp: steps.simps step.simps dither_def numeral tape_of_nat_abv)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 965
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 966
66
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 967
lemma dither_loops:
70
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 968
shows "{dither_unhalt_inv} dither \<up>"
66
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 969
apply(rule Hoare_unhaltI)
80
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 970
using dither_loops_aux
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 971
apply(auto simp add: numeral tape_of_nat_abv)
80
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 972
by (metis Suc_neq_Zero is_final_eq)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 973
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 974
lemma dither_halts_aux:
91
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 975
shows "steps0 (1, Bk \<up> m, [Oc, Oc]) dither 2 = (0, Bk \<up> m, [Oc, Oc])"
66
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 976
unfolding dither_def
80
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 977
by (simp add: steps.simps step.simps numeral)
66
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 978
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 979
lemma dither_halts:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 980
shows "{dither_halt_inv} dither {dither_halt_inv}"
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 981
apply(rule Hoare_haltI)
80
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 982
using dither_halts_aux
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 983
apply(auto simp add: tape_of_nat_abv)
66
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 984
by (metis (lifting, mono_tags) holds_for.simps is_final_eq prod.cases)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 985
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 986
80
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 987
section {* The diagnal argument below shows the undecidability of Halting problem *}
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 988
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 989
text {*
169
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 990
@{text "halts tp x"} means TM @{text "tp"} terminates on input @{text "x"}
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 991
and the final configuration is standard.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 992
*}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 993
169
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 994
definition halts :: "tprog0 \<Rightarrow> nat list \<Rightarrow> bool"
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 995
where
169
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 996
"halts p ns \<equiv> {(\<lambda>tp. tp = ([], <ns>))} p {(\<lambda>tp. (\<exists>k n l. tp = (Bk \<up> k, <n::nat> @ Bk \<up> l)))}"
65
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 997
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 998
lemma [intro, simp]: "tm_wf0 tcopy"
82
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 999
by (auto simp: tcopy_def)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1000
65
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1001
lemma [intro, simp]: "tm_wf0 dither"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1002
by (auto simp: tm_wf.simps dither_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1003
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1004
text {*
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1005
The following locale specifies that TM @{text "H"} can be used to solve
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1006
the {\em Halting Problem} and @{text "False"} is going to be derived
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1007
under this locale. Therefore, the undecidability of {\em Halting Problem}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1008
is established.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1009
*}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1010
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1011
locale uncomputable =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1012
-- {* The coding function of TM, interestingly, the detailed definition of this
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1013
funciton @{text "code"} does not affect the final result. *}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1014
fixes code :: "instr list \<Rightarrow> nat"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1015
-- {*
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1016
The TM @{text "H"} is the one which is assummed being able to solve the Halting problem.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1017
*}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1018
and H :: "instr list"
70
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1019
assumes h_wf[intro]: "tm_wf0 H"
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1020
-- {*
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1021
The following two assumptions specifies that @{text "H"} does solve the Halting problem.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1022
*}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1023
and h_case:
169
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1024
"\<And> M ns. halts M ns \<Longrightarrow> {(\<lambda>tp. tp = ([Bk], <(code M, ns)>))} H {(\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>))}"
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1025
and nh_case:
169
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1026
"\<And> M ns. \<not> halts M ns \<Longrightarrow> {(\<lambda>tp. tp = ([Bk], <(code M, ns)>))} H {(\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>))}"
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1027
begin
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1028
70
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1029
(* invariants for H *)
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1030
abbreviation (input)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1031
"pre_H_inv M ns \<equiv> \<lambda>tp. tp = ([Bk], <(code M, ns::nat list)>)"
70
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1032
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1033
abbreviation (input)
99
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1034
"post_H_halt_inv \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"
70
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1035
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1036
abbreviation (input)
99
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1037
"post_H_unhalt_inv \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"
70
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1038
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1039
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1040
lemma H_halt_inv:
169
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1041
assumes "\<not> halts M ns"
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1042
shows "{pre_H_inv M ns} H {post_H_halt_inv}"
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1043
using assms nh_case by auto
70
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1044
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1045
lemma H_unhalt_inv:
169
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1046
assumes "halts M ns"
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1047
shows "{pre_H_inv M ns} H {post_H_unhalt_inv}"
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1048
using assms h_case by auto
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1049
67
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1050
(* TM that produces the contradiction and its code *)
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1051
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1052
definition
67
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1053
"tcontra \<equiv> (tcopy |+| H) |+| dither"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1054
abbreviation
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1055
"code_tcontra \<equiv> code tcontra"
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1056
67
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1057
(* assume tcontra does not halt on its code *)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1058
lemma tcontra_unhalt:
169
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1059
assumes "\<not> halts tcontra [code tcontra]"
66
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1060
shows "False"
65
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1061
proof -
64
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1062
(* invariants *)
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1063
def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <code_tcontra>)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1064
def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"
99
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1065
def P3 \<equiv> "\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"
64
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1066
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1067
(*
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1068
{P1} tcopy {P2} {P2} H {P3}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1069
----------------------------
65
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1070
{P1} (tcopy |+| H) {P3} {P3} dither {P3}
64
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1071
------------------------------------------------
68
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1072
{P1} tcontra {P3}
64
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1073
*)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1074
65
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1075
have H_wf: "tm_wf0 (tcopy |+| H)" by auto
64
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1076
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1077
(* {P1} (tcopy |+| H) {P3} *)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1078
have first: "{P1} (tcopy |+| H) {P3}"
99
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1079
proof (cases rule: Hoare_plus_halt)
64
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1080
case A_halt (* of tcopy *)
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1081
show "{P1} tcopy {P2}" unfolding P1_def P2_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1082
by (rule tcopy_correct)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1083
next
70
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1084
case B_halt (* of H *)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1085
show "{P2} H {P3}"
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1086
unfolding P2_def P3_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1087
using H_halt_inv[OF assms]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1088
by (simp add: tape_of_nat_pair tape_of_nl_abv)
65
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1089
qed (simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1090
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1091
(* {P3} dither {P3} *)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1092
have second: "{P3} dither {P3}" unfolding P3_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1093
by (rule dither_halts)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1094
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1095
(* {P1} tcontra {P3} *)
67
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1096
have "{P1} tcontra {P3}"
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1097
unfolding tcontra_def
99
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1098
by (rule Hoare_plus_halt[OF first second H_wf])
65
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1099
67
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1100
with assms show "False"
70
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1101
unfolding P1_def P3_def
169
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1102
unfolding halts_def
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1103
unfolding Hoare_halt_def
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1104
apply(auto)
84
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1105
apply(drule_tac x = n in spec)
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1106
apply(case_tac "steps0 (Suc 0, [], <code tcontra>) tcontra n")
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1107
apply(auto simp add: tape_of_nl_abv)
141
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1108
by (metis append_Nil2 replicate_0)
65
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1109
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1110
67
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1111
(* asumme tcontra halts on its code *)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1112
lemma tcontra_halt:
169
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1113
assumes "halts tcontra [code tcontra]"
66
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1114
shows "False"
65
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1115
proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1116
(* invariants *)
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1117
def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <code_tcontra>)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1118
def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"
99
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1119
def Q3 \<equiv> "\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"
65
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1120
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1121
(*
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1122
{P1} tcopy {P2} {P2} H {Q3}
65
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1123
----------------------------
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1124
{P1} (tcopy |+| H) {Q3} {Q3} dither loops
65
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1125
------------------------------------------------
68
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1126
{P1} tcontra loops
65
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1127
*)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1128
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1129
have H_wf: "tm_wf0 (tcopy |+| H)" by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1130
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1131
(* {P1} (tcopy |+| H) {Q3} *)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1132
have first: "{P1} (tcopy |+| H) {Q3}"
99
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1133
proof (cases rule: Hoare_plus_halt)
65
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1134
case A_halt (* of tcopy *)
69
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1135
show "{P1} tcopy {P2}" unfolding P1_def P2_def
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1136
by (rule tcopy_correct)
65
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1137
next
70
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1138
case B_halt (* of H *)
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1139
then show "{P2} H {Q3}"
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1140
unfolding P2_def Q3_def using H_unhalt_inv[OF assms]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1141
by(simp add: tape_of_nat_pair tape_of_nl_abv)
65
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1142
qed (simp)
64
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1143
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1144
(* {P3} dither loops *)
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1145
have second: "{Q3} dither \<up>" unfolding Q3_def
64
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1146
by (rule dither_loops)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1147
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1148
(* {P1} tcontra loops *)
67
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1149
have "{P1} tcontra \<up>"
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1150
unfolding tcontra_def
99
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1151
by (rule Hoare_plus_unhalt[OF first second H_wf])
65
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1152
66
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1153
with assms show "False"
70
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1154
unfolding P1_def
169
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1155
unfolding halts_def
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1156
unfolding Hoare_halt_def Hoare_unhalt_def
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1157
by (auto simp add: tape_of_nl_abv)
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1158
qed
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1159
63
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1160
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1161
text {*
64
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1162
@{text "False"} can finally derived.
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1163
*}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1164
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1165
lemma false: "False"
67
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1166
using tcontra_halt tcontra_unhalt
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1167
by auto
63
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1168
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1169
end
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1170
66
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1171
declare replicate_Suc[simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1172
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1173
44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1174
end
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1175