0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1
(* Title: Turing machine's definition and its charater
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 2
Author: XuJian <xujian817@hotmail.com>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 3
Maintainer: Xujian
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 4
*)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 5
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 6
header {* Undeciablity of the {\em Halting problem} *}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 7
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 8
theory uncomputable
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 9
imports Main turing_basic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 10
begin
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 11
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 12
text {*
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 13
The {\em Copying} TM, which duplicates its input.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 14
*}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 15
definition tcopy :: "tprog"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 16
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 17
"tcopy \<equiv> [(W0, 0), (R, 2), (R, 3), (R, 2),
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 18
(W1, 3), (L, 4), (L, 4), (L, 5), (R, 11), (R, 6),
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 19
(R, 7), (W0, 6), (R, 7), (R, 8), (W1, 9), (R, 8),
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 20
(L, 10), (L, 9), (L, 10), (L, 5), (R, 12), (R, 12),
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 21
(W1, 13), (L, 14), (R, 12), (R, 12), (L, 15), (W0, 14),
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 22
(R, 0), (L, 15)]"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 23
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 24
text {*
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 25
@{text "wipeLastBs tp"} removes all blanks at the end of tape @{text "tp"}.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 26
*}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 27
fun wipeLastBs :: "block list \<Rightarrow> block list"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 28
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 29
"wipeLastBs bl = rev (dropWhile (\<lambda>a. a = Bk) (rev bl))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 30
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 31
fun isBk :: "block \<Rightarrow> bool"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 32
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 33
"isBk b = (b = Bk)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 34
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 35
text {*
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 36
The following functions are used to expression invariants of {\em Copying} TM.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 37
*}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 38
fun tcopy_F0 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 39
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 40
"tcopy_F0 x tp = (let (ln, rn) = tp in
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 41
list_all isBk ln & rn = replicate x Oc
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 42
@ [Bk] @ replicate x Oc)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 43
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 44
fun tcopy_F1 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 45
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 46
"tcopy_F1 x (ln, rn) = (ln = [] & rn = replicate x Oc)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 47
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 48
fun tcopy_F2 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 49
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 50
"tcopy_F2 0 tp = False" |
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 51
"tcopy_F2 (Suc x) (ln, rn) = (length ln > 0 &
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 52
ln @ rn = replicate (Suc x) Oc)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 53
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 54
fun tcopy_F3 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 55
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 56
"tcopy_F3 0 tp = False" |
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 57
"tcopy_F3 (Suc x) (ln, rn) =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 58
(ln = Bk # replicate (Suc x) Oc & length rn <= 1)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 59
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 60
fun tcopy_F4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 61
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 62
"tcopy_F4 0 tp = False" |
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 63
"tcopy_F4 (Suc x) (ln, rn) =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 64
((ln = replicate x Oc & rn = [Oc, Bk, Oc])
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 65
| (ln = replicate (Suc x) Oc & rn = [Bk, Oc])) "
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 66
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 67
fun tcopy_F5 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 68
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 69
"tcopy_F5 0 tp = False" |
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 70
"tcopy_F5 (Suc x) (ln, rn) =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 71
(if rn = [] then False
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 72
else if hd rn = Bk then (ln = [] &
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 73
rn = Bk # (Oc # replicate (Suc x) Bk
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 74
@ replicate (Suc x) Oc))
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 75
else if hd rn = Oc then
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 76
(\<exists>n. ln = replicate (x - n) Oc
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 77
& rn = Oc # (Oc # replicate n Bk @ replicate n Oc)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 78
& n > 0 & n <= x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 79
else False)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 80
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 81
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 82
fun tcopy_F6 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 83
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 84
"tcopy_F6 0 tp = False" |
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 85
"tcopy_F6 (Suc x) (ln, rn) =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 86
(\<exists>n. ln = replicate (Suc x -n) Oc
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 87
& tl rn = replicate n Bk @ replicate n Oc
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 88
& n > 0 & n <= x)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 89
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 90
fun tcopy_F7 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 91
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 92
"tcopy_F7 0 tp = False" |
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 93
"tcopy_F7 (Suc x) (ln, rn) =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 94
(let lrn = (rev ln) @ rn in
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 95
(\<exists>n. lrn = replicate ((Suc x) - n) Oc @
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 96
replicate (Suc n) Bk @ replicate n Oc
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 97
& n > 0 & n <= x &
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 98
length rn >= n & length rn <= 2 * n ))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 99
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 100
fun tcopy_F8 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 101
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 102
"tcopy_F8 0 tp = False" |
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 103
"tcopy_F8 (Suc x) (ln, rn) =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 104
(let lrn = (rev ln) @ rn in
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 105
(\<exists>n. lrn = replicate ((Suc x) - n) Oc @
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 106
replicate (Suc n) Bk @ replicate n Oc
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 107
& n > 0 & n <= x & length rn < n)) "
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 108
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 109
fun tcopy_F9 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 110
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 111
"tcopy_F9 0 tp = False" |
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 112
"tcopy_F9 (Suc x) (ln, rn) =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 113
(let lrn = (rev ln) @ rn in
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 114
(\<exists>n. lrn = replicate (Suc (Suc x) - n) Oc
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 115
@ replicate n Bk @ replicate n Oc
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 116
& n > Suc 0 & n <= Suc x & length rn > 0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 117
& length rn <= Suc n))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 118
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 119
fun tcopy_F10 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 120
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 121
"tcopy_F10 0 tp = False" |
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 122
"tcopy_F10 (Suc x) (ln, rn) =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 123
(let lrn = (rev ln) @ rn in
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 124
(\<exists>n. lrn = replicate (Suc (Suc x) - n) Oc
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 125
@ replicate n Bk @ replicate n Oc & n > Suc 0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 126
& n <= Suc x & length rn > Suc n &
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 127
length rn <= 2*n + 1 ))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 128
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 129
fun tcopy_F11 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 130
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 131
"tcopy_F11 0 tp = False" |
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 132
"tcopy_F11 (Suc x) (ln, rn) =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 133
(ln = [Bk] & rn = Oc # replicate (Suc x) Bk
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 134
@ replicate (Suc x) Oc)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 135
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 136
fun tcopy_F12 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 137
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 138
"tcopy_F12 0 tp = False" |
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 139
"tcopy_F12 (Suc x) (ln, rn) =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 140
(let lrn = ((rev ln) @ rn) in
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 141
(\<exists>n. n > 0 & n <= Suc (Suc x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 142
& lrn = Bk # replicate n Oc @ replicate (Suc (Suc x) - n) Bk
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 143
@ replicate (Suc x) Oc
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 144
& length ln = Suc n))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 145
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 146
fun tcopy_F13 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 147
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 148
"tcopy_F13 0 tp = False" |
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 149
"tcopy_F13 (Suc x) (ln, rn) =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 150
(let lrn = ((rev ln) @ rn) in
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 151
(\<exists>n. n > Suc 0 & n <= Suc (Suc x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 152
& lrn = Bk # replicate n Oc @ replicate (Suc (Suc x) - n) Bk
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 153
@ replicate (Suc x) Oc
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 154
& length ln = n))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 155
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 156
fun tcopy_F14 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 157
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 158
"tcopy_F14 0 tp = False" |
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 159
"tcopy_F14 (Suc x) (ln, rn) =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 160
(ln = replicate (Suc x) Oc @ [Bk] &
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 161
tl rn = replicate (Suc x) Oc)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 162
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 163
fun tcopy_F15 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 164
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 165
"tcopy_F15 0 tp = False" |
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 166
"tcopy_F15 (Suc x) (ln, rn) =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 167
(let lrn = ((rev ln) @ rn) in
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 168
lrn = Bk # replicate (Suc x) Oc @ [Bk] @
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 169
replicate (Suc x) Oc & length ln <= (Suc x))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 170
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 171
text {*
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 172
The following @{text "inv_tcopy"} is the invariant of the {\em Copying} TM.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 173
*}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 174
fun inv_tcopy :: "nat \<Rightarrow> t_conf \<Rightarrow> bool"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 175
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 176
"inv_tcopy x c = (let (state, tp) = c in
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 177
if state = 0 then tcopy_F0 x tp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 178
else if state = 1 then tcopy_F1 x tp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 179
else if state = 2 then tcopy_F2 x tp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 180
else if state = 3 then tcopy_F3 x tp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 181
else if state = 4 then tcopy_F4 x tp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 182
else if state = 5 then tcopy_F5 x tp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 183
else if state = 6 then tcopy_F6 x tp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 184
else if state = 7 then tcopy_F7 x tp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 185
else if state = 8 then tcopy_F8 x tp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 186
else if state = 9 then tcopy_F9 x tp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 187
else if state = 10 then tcopy_F10 x tp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 188
else if state = 11 then tcopy_F11 x tp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 189
else if state = 12 then tcopy_F12 x tp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 190
else if state = 13 then tcopy_F13 x tp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 191
else if state = 14 then tcopy_F14 x tp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 192
else if state = 15 then tcopy_F15 x tp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 193
else False)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 194
declare tcopy_F0.simps [simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 195
tcopy_F1.simps [simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 196
tcopy_F2.simps [simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 197
tcopy_F3.simps [simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 198
tcopy_F4.simps [simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 199
tcopy_F5.simps [simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 200
tcopy_F6.simps [simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 201
tcopy_F7.simps [simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 202
tcopy_F8.simps [simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 203
tcopy_F9.simps [simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 204
tcopy_F10.simps [simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 205
tcopy_F11.simps [simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 206
tcopy_F12.simps [simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 207
tcopy_F13.simps [simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 208
tcopy_F14.simps [simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 209
tcopy_F15.simps [simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 210
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 211
lemma list_replicate_Bk[dest]: "list_all isBk list \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 212
list = replicate (length list) Bk"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 213
apply(induct list)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 214
apply(simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 215
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 216
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 217
lemma [simp]: "dropWhile (\<lambda> a. a = b) (replicate x b @ ys) =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 218
dropWhile (\<lambda> a. a = b) ys"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 219
apply(induct x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 220
apply(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 221
apply(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 222
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 223
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 224
lemma [elim]: "\<lbrakk>tstep (0, a, b) tcopy = (s, l, r); s \<noteq> 0\<rbrakk> \<Longrightarrow> RR"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 225
apply(simp add: tstep.simps tcopy_def fetch.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 226
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 227
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 228
lemma [elim]: "\<lbrakk>tstep (Suc 0, a, b) tcopy = (s, l, r); s \<noteq> 0; s \<noteq> 2\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 229
\<Longrightarrow> RR"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 230
apply(simp add: tstep.simps tcopy_def fetch.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 231
apply(simp split: block.splits list.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 232
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 233
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 234
lemma [elim]: "\<lbrakk>tstep (2, a, b) tcopy = (s, l, r); s \<noteq> 2; s \<noteq> 3\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 235
\<Longrightarrow> RR"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 236
apply(simp add: tstep.simps tcopy_def fetch.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 237
apply(simp split: block.splits list.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 238
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 239
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 240
lemma [elim]: "\<lbrakk>tstep (3, a, b) tcopy = (s, l, r); s \<noteq> 3; s \<noteq> 4\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 241
\<Longrightarrow> RR"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 242
by(simp add: tstep.simps tcopy_def fetch.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 243
split: block.splits list.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 244
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 245
lemma [elim]: "\<lbrakk>tstep (4, a, b) tcopy = (s, l, r); s \<noteq> 4; s \<noteq> 5\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 246
\<Longrightarrow> RR"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 247
by(simp add: tstep.simps tcopy_def fetch.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 248
split: block.splits list.splits)
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>tstep (5, a, b) tcopy = (s, l, r); s \<noteq> 6; s \<noteq> 11\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 251
\<Longrightarrow> RR"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 252
by(simp add: tstep.simps tcopy_def fetch.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 253
split: block.splits list.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 254
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 255
lemma [elim]: "\<lbrakk>tstep (6, a, b) tcopy = (s, l, r); s \<noteq> 6; s \<noteq> 7\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 256
\<Longrightarrow> RR"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 257
by(simp add: tstep.simps tcopy_def fetch.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 258
split: block.splits list.splits)
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>tstep (7, a, b) tcopy = (s, l, r); s \<noteq> 7; s \<noteq> 8\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 261
\<Longrightarrow> RR"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 262
by(simp add: tstep.simps tcopy_def fetch.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 263
split: block.splits list.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 264
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 265
lemma [elim]: "\<lbrakk>tstep (8, a, b) tcopy = (s, l, r); s \<noteq> 8; s \<noteq> 9\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 266
\<Longrightarrow> RR"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 267
by(simp add: tstep.simps tcopy_def fetch.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 268
split: block.splits list.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 269
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 270
lemma [elim]: "\<lbrakk>tstep (9, a, b) tcopy = (s, l, r); s \<noteq> 9; s \<noteq> 10\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 271
\<Longrightarrow> RR"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 272
by(simp add: tstep.simps tcopy_def fetch.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 273
split: block.splits list.splits)
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>tstep (10, a, b) tcopy = (s, l, r); s \<noteq> 10; s \<noteq> 5\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 276
\<Longrightarrow> RR"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 277
by(simp add: tstep.simps tcopy_def fetch.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 278
split: block.splits list.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 279
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 280
lemma [elim]: "\<lbrakk>tstep (11, a, b) tcopy = (s, l, r); s \<noteq> 12\<rbrakk> \<Longrightarrow> RR"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 281
by(simp add: tstep.simps tcopy_def fetch.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 282
split: block.splits list.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 283
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 284
lemma [elim]: "\<lbrakk>tstep (12, a, b) tcopy = (s, l, r); s \<noteq> 13; s \<noteq> 14\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 285
\<Longrightarrow> RR"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 286
by(simp add: tstep.simps tcopy_def fetch.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 287
split: block.splits list.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 288
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 289
lemma [elim]: "\<lbrakk>tstep (13, a, b) tcopy = (s, l, r); s \<noteq> 12\<rbrakk> \<Longrightarrow> RR"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 290
by(simp add: tstep.simps tcopy_def fetch.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 291
split: block.splits list.splits)
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>tstep (14, a, b) tcopy = (s, l, r); s \<noteq> 14; s \<noteq> 15\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 294
\<Longrightarrow> RR"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 295
by(simp add: tstep.simps tcopy_def fetch.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 296
split: block.splits list.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 297
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 298
lemma [elim]: "\<lbrakk>tstep (15, a, b) tcopy = (s, l, r); s \<noteq> 0; s \<noteq> 15\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 299
\<Longrightarrow> RR"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 300
by(simp add: tstep.simps tcopy_def fetch.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 301
split: block.splits list.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 302
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 303
lemma min_Suc4: "min (Suc (Suc x)) x = x"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 304
by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 305
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 306
lemma takeWhile2replicate:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 307
"\<exists>n. takeWhile (\<lambda>a. a = b) list = replicate n b"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 308
apply(induct list)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 309
apply(rule_tac x = 0 in exI, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 310
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 311
apply(rule_tac x = "Suc n" in exI, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 312
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 313
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 314
lemma rev_replicate_same: "rev (replicate x b) = replicate x b"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 315
by(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 316
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 317
lemma rev_equal: "a = b \<Longrightarrow> rev a = rev b"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 318
by simp
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 rev_equal_rev: "rev a = rev b \<Longrightarrow> a = b"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 321
by simp
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 rep_suc_rev[simp]:"replicate n b @ [b] = replicate (Suc n) b"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 324
apply(rule rev_equal_rev)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 325
apply(simp only: rev_append rev_replicate_same)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 326
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 327
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 328
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 329
lemma replicate_Cons_simp: "b # replicate n b @ xs =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 330
replicate n b @ b # xs"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 331
apply(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 332
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 333
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 334
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 335
lemma [elim]: "\<lbrakk>tstep (14, b, c) tcopy = (15, ab, ba);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 336
tcopy_F14 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F15 x (ab, ba)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 337
apply(case_tac x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 338
apply(auto simp: tstep.simps tcopy_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 339
tcopy_F14.simps tcopy_F15.simps fetch.simps new_tape.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 340
split: if_splits list.splits block.splits)
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 dropWhile_drophd: "\<not> p a \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 344
(dropWhile p xs @ (a # as)) = (dropWhile p (xs @ [a]) @ as)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 345
apply(induct xs)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 346
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 347
done
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 dropWhile_append3: "\<lbrakk>\<not> p a;
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 350
listall ((dropWhile p xs) @ [a]) isBk\<rbrakk> \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 351
listall (dropWhile p (xs @ [a])) isBk"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 352
apply(drule_tac p = p and xs = xs and a = a in dropWhile_drophd, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 353
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 354
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 355
lemma takeWhile_append3: "\<lbrakk>\<not>p a; (takeWhile p xs) = b\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 356
\<Longrightarrow> takeWhile p (xs @ (a # as)) = b"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 357
apply(drule_tac P = p and xs = xs and x = a and l = as in
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 358
takeWhile_tail)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 359
apply(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 360
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 361
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 362
lemma listall_append: "list_all p (xs @ ys) =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 363
(list_all p xs \<and> list_all p ys)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 364
apply(induct xs)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 365
apply(simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 366
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 367
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 368
lemma [elim]: "\<lbrakk>tstep (15, b, c) tcopy = (15, ab, ba);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 369
tcopy_F15 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F15 x (ab, ba)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 370
apply(case_tac x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 371
apply(auto simp: tstep.simps tcopy_F15.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 372
tcopy_def fetch.simps new_tape.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 373
split: if_splits list.splits block.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 374
apply(case_tac b, simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 375
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 376
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 377
lemma [elim]: "\<lbrakk>tstep (14, b, c) tcopy = (14, ab, ba);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 378
tcopy_F14 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F14 x (ab, ba)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 379
apply(case_tac x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 380
apply(auto simp: tcopy_F14.simps tcopy_def tstep.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 381
tcopy_F14.simps fetch.simps new_tape.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 382
split: if_splits list.splits block.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 383
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 384
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 385
lemma [intro]: "list_all isBk (replicate x Bk)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 386
apply(induct x, simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 387
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 388
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 389
lemma [elim]: "list_all isBk (dropWhile (\<lambda>a. a = Oc) b) \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 390
list_all isBk (dropWhile (\<lambda>a. a = Oc) (tl b))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 391
apply(case_tac b, auto split: if_splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 392
apply(drule list_replicate_Bk)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 393
apply(case_tac "length list", auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 394
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 395
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 396
lemma [elim]: "list_all (\<lambda> a. a = Oc) list \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 397
list = replicate (length list) Oc"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 398
apply(induct list)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 399
apply(simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 400
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 401
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 402
lemma append_length: "\<lbrakk>as @ bs = cs @ ds; length bs = length ds\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 403
\<Longrightarrow> as = cs & bs = ds"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 404
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 405
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 406
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 407
lemma Suc_elim: "Suc (Suc m) - n = Suc na \<Longrightarrow> Suc m - n = na"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 408
apply(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 409
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 410
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 411
lemma [elim]: "\<lbrakk>0 < n; n \<le> Suc (Suc na);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 412
rev b @ Oc # list =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 413
Bk # replicate n Oc @ replicate (Suc (Suc na) - n) Bk @
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 414
Oc # replicate na Oc;
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 415
length b = Suc n; b \<noteq> []\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 416
\<Longrightarrow> list_all isBk (dropWhile (\<lambda>a. a = Oc) (tl b))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 417
apply(case_tac "rev b", auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 418
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 419
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 420
lemma b_cons_same: "b#bs = replicate x a @ as \<Longrightarrow> a \<noteq> b \<longrightarrow> x = 0"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 421
apply(case_tac x, simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 422
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 423
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 424
lemma tcopy_tmp[elim]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 425
"\<lbrakk>0 < n; n \<le> Suc (Suc na);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 426
rev b @ Oc # list =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 427
Bk # replicate n Oc @ replicate (Suc (Suc na) - n) Bk
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 428
@ Oc # replicate na Oc; length b = Suc n; b \<noteq> []\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 429
\<Longrightarrow> list = replicate na Oc"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 430
apply(case_tac "rev b", simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 431
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 432
apply(frule b_cons_same, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 433
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 434
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 435
lemma [elim]: "\<lbrakk>tstep (12, b, c) tcopy = (14, ab, ba);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 436
tcopy_F12 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F14 x (ab, ba)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 437
apply(case_tac x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 438
apply(auto simp:tcopy_F12.simps tcopy_F14.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 439
tcopy_def tstep.simps fetch.simps new_tape.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 440
split: if_splits list.splits block.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 441
apply(frule tcopy_tmp, simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 442
apply(case_tac n, simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 443
apply(case_tac nata, simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 444
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 445
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 446
lemma replicate_app_Cons: "replicate a b @ b # replicate c b
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 447
= replicate (Suc (a + c)) b"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 448
apply(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 449
apply(simp add: replicate_app_Cons_same)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 450
apply(simp only: replicate_add[THEN sym])
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 451
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 452
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 453
lemma replicate_same_exE_pref: "\<exists>x. bs @ (b # cs) = replicate x y
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 454
\<Longrightarrow> (\<exists>n. bs = replicate n y)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 455
apply(induct bs)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 456
apply(rule_tac x = 0 in exI, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 457
apply(drule impI)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 458
apply(erule impE)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 459
apply(erule exE, simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 460
apply(case_tac x, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 461
apply(case_tac x, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 462
apply(rule_tac x = "Suc n" in exI, simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 463
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 464
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 465
lemma replicate_same_exE_inf: "\<exists>x. bs @ (b # cs) = replicate x y \<Longrightarrow> b = y"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 466
apply(induct bs, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 467
apply(case_tac x, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 468
apply(drule impI)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 469
apply(erule impE)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 470
apply(case_tac x, simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 471
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 472
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 473
lemma replicate_same_exE_suf:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 474
"\<exists>x. bs @ (b # cs) = replicate x y \<Longrightarrow> \<exists>n. cs = replicate n y"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 475
apply(induct bs, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 476
apply(case_tac x, simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 477
apply(drule impI, erule impE)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 478
apply(case_tac x, simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 479
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 480
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 481
lemma replicate_same_exE: "\<exists>x. bs @ (b # cs) = replicate x y
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 482
\<Longrightarrow> (\<exists>n. bs = replicate n y) & (b = y) & (\<exists>m. cs = replicate m y)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 483
apply(rule conjI)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 484
apply(drule replicate_same_exE_pref, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 485
apply(rule conjI)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 486
apply(drule replicate_same_exE_inf, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 487
apply(drule replicate_same_exE_suf, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 488
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 489
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 490
lemma replicate_same: "bs @ (b # cs) = replicate x y
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 491
\<Longrightarrow> (\<exists>n. bs = replicate n y) & (b = y) & (\<exists>m. cs = replicate m y)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 492
apply(rule_tac replicate_same_exE)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 493
apply(rule_tac x = x in exI)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 494
apply(assumption)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 495
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 496
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 497
lemma [elim]: "\<lbrakk> 0 < n; n \<le> Suc (Suc na);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 498
(rev ab @ Bk # list) = Bk # replicate n Oc
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 499
@ replicate (Suc (Suc na) - n) Bk @ Oc # replicate na Oc; ab \<noteq> []\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 500
\<Longrightarrow> n \<le> Suc na"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 501
apply(rule contrapos_pp, simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 502
apply(case_tac "rev ab", simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 503
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 504
apply(simp only: replicate_app_Cons)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 505
apply(drule replicate_same)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 506
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 507
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 508
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 [elim]: "\<lbrakk>0 < n; n \<le> Suc (Suc na);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 511
rev ab @ Bk # list = Bk # replicate n Oc @
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 512
replicate (Suc (Suc na) - n) Bk @ Oc # replicate na Oc;
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 513
length ab = Suc n; ab \<noteq> []\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 514
\<Longrightarrow> rev ab @ Oc # list = Bk # Oc # replicate n Oc @
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 515
replicate (Suc na - n) Bk @ Oc # replicate na Oc"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 516
apply(case_tac "rev ab", simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 517
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 518
apply(simp only: replicate_Cons_simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 519
apply(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 520
apply(case_tac "Suc (Suc na) - n", simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 521
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 522
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 523
lemma [elim]: "\<lbrakk>tstep (12, b, c) tcopy = (13, ab, ba);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 524
tcopy_F12 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F13 x (ab, ba)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 525
apply(case_tac x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 526
apply(simp_all add:tcopy_F12.simps tcopy_F13.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 527
tcopy_def tstep.simps fetch.simps new_tape.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 528
apply(simp split: if_splits list.splits block.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 529
apply(auto)
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
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 533
lemma [elim]: "\<lbrakk>tstep (11, b, c) tcopy = (12, ab, ba);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 534
tcopy_F11 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F12 x (ab, ba)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 535
apply(case_tac x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 536
apply(simp_all add:tcopy_F12.simps tcopy_F11.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 537
tcopy_def tstep.simps fetch.simps new_tape.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 538
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 539
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 540
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 541
lemma equal_length: "a = b \<Longrightarrow> length a = length b"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 542
by(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 543
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 544
lemma [elim]: "\<lbrakk>tstep (13, b, c) tcopy = (12, ab, ba);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 545
tcopy_F13 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F12 x (ab, ba)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 546
apply(case_tac x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 547
apply(simp_all add:tcopy_F12.simps tcopy_F13.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 548
tcopy_def tstep.simps fetch.simps new_tape.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 549
apply(simp split: if_splits list.splits block.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 550
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 551
apply(drule equal_length, simp)
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]: "\<lbrakk>tstep (5, b, c) tcopy = (11, ab, ba);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 555
tcopy_F5 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F11 x (ab, ba)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 556
apply(case_tac x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 557
apply(simp_all add:tcopy_F11.simps tcopy_F5.simps tcopy_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 558
tstep.simps fetch.simps new_tape.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 559
apply(simp split: if_splits list.splits block.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 560
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 561
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 562
lemma less_equal: "\<lbrakk>length xs <= b; \<not> Suc (length xs) <= b\<rbrakk> \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 563
length xs = b"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 564
apply(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 565
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 566
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 567
lemma length_cons_same: "\<lbrakk>xs @ b # ys = as @ bs;
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 568
length ys = length bs\<rbrakk> \<Longrightarrow> xs @ [b] = as & ys = bs"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 569
apply(drule rev_equal)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 570
apply(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 571
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 572
apply(drule rev_equal, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 573
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 574
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 575
lemma replicate_set_equal: "\<lbrakk> xs @ [a] = replicate n b; a \<noteq> b\<rbrakk> \<Longrightarrow> RR"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 576
apply(drule rev_equal, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 577
apply(case_tac n, simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 578
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 579
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 580
lemma [elim]: "\<lbrakk>tstep (10, b, c) tcopy = (10, ab, ba);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 581
tcopy_F10 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F10 x (ab, ba)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 582
apply(case_tac x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 583
apply(auto simp:tcopy_F10.simps tcopy_def tstep.simps fetch.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 584
new_tape.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 585
split: if_splits list.splits block.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 586
apply(rule_tac x = n in exI, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 587
apply(case_tac b, simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 588
apply(rule contrapos_pp, simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 589
apply(frule less_equal, simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 590
apply(drule length_cons_same, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 591
apply(drule replicate_set_equal, simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 592
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 593
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 594
lemma less_equal2: "\<not> (n::nat) \<le> m \<Longrightarrow> \<exists>x. n = x + m & x > 0"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 595
apply(rule_tac x = "n - m" in exI)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 596
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 597
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 598
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 599
lemma replicate_tail_length[dest]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 600
"\<lbrakk>rev b @ Bk # list = xs @ replicate n Bk @ replicate n Oc\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 601
\<Longrightarrow> length list >= n"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 602
apply(rule contrapos_pp, simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 603
apply(drule less_equal2, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 604
apply(drule rev_equal)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 605
apply(simp add: replicate_add)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 606
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 607
apply(case_tac x, simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 608
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 609
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 610
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 611
lemma [elim]: "\<lbrakk>tstep (9, b, c) tcopy = (10, ab, ba);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 612
tcopy_F9 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F10 x (ab, ba)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 613
apply(case_tac x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 614
apply(auto simp:tcopy_F10.simps tcopy_F9.simps tcopy_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 615
tstep.simps fetch.simps new_tape.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 616
split: if_splits list.splits block.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 617
apply(rule_tac x = n in exI, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 618
apply(case_tac b, simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 619
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 620
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 621
lemma [elim]: "\<lbrakk>tstep (9, b, c) tcopy = (9, ab, ba);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 622
tcopy_F9 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F9 x (ab, ba)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 623
apply(case_tac x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 624
apply(simp_all add: tcopy_F9.simps tcopy_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 625
tstep.simps fetch.simps new_tape.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 626
split: if_splits list.splits block.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 627
apply(rule_tac x = n in exI, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 628
apply(case_tac b, simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 629
apply(rule contrapos_pp, simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 630
apply(drule less_equal, simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 631
apply(drule rev_equal, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 632
apply(case_tac "length list", simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 633
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 634
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 635
lemma app_cons_app_simp: "xs @ a # bs @ ys = (xs @ [a]) @ bs @ ys"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 636
apply(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 637
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 638
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 639
lemma [elim]: "\<lbrakk>tstep (8, b, c) tcopy = (9, ab, ba);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 640
tcopy_F8 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F9 x (ab, ba)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 641
apply(case_tac x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 642
apply(auto simp:tcopy_F8.simps tcopy_F9.simps tcopy_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 643
tstep.simps fetch.simps new_tape.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 644
split: if_splits list.splits block.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 645
apply(rule_tac x = "Suc n" in exI, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 646
apply(rule_tac x = "n" in exI, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 647
apply(simp only: app_cons_app_simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 648
apply(frule replicate_tail_length, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 649
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 650
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 651
lemma [elim]: "\<lbrakk>tstep (8, b, c) tcopy = (8, ab, ba);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 652
tcopy_F8 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F8 x (ab, ba)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 653
apply(case_tac x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 654
apply(simp_all add:tcopy_F8.simps tcopy_def tstep.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 655
fetch.simps new_tape.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 656
apply(simp split: if_splits list.splits block.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 657
apply(rule_tac x = "n" in exI, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 658
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 659
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 660
lemma ex_less_more: "\<lbrakk>(x::nat) >= m ; x <= n\<rbrakk> \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 661
\<exists>y. x = m + y & y <= n - m"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 662
by(rule_tac x = "x -m" in exI, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 663
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 664
lemma replicate_split: "x <= n \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 665
(\<exists>y. replicate n b = replicate (y + x) b)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 666
apply(rule_tac x = "n - x" in exI)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 667
apply(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 668
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 669
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 670
lemma app_app_app_app_simp: "as @ bs @ cs @ ds =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 671
(as @ bs) @ (cs @ ds)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 672
by simp
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 lengthtailsame_append_elim:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 675
"\<lbrakk>as @ bs = cs @ ds; length bs = length ds\<rbrakk> \<Longrightarrow> bs = ds"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 676
apply(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 677
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 678
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 679
lemma rep_suc: "replicate (Suc n) x = replicate n x @ [x]"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 680
by(induct n, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 681
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 682
lemma length_append_diff_cons:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 683
"\<lbrakk>b @ x # ba = xs @ replicate m y @ replicate n x; x \<noteq> y;
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 684
Suc (length ba) \<le> m + n\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 685
\<Longrightarrow> length ba < n"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 686
apply(induct n arbitrary: ba, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 687
apply(drule_tac b = y in replicate_split,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 688
simp add: replicate_add, erule exE, simp del: replicate.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 689
proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 690
fix ba ya
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 691
assume h1:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 692
"b @ x # ba = xs @ y # replicate ya y @ replicate (length ba) y"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 693
and h2: "x \<noteq> y"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 694
thus "False"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 695
using append_eq_append_conv[of "b @ [x]"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 696
"xs @ y # replicate ya y" "ba" "replicate (length ba) y"]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 697
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 698
apply(case_tac ya, simp,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 699
simp add: rep_suc del: rep_suc_rev replicate.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 700
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 701
next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 702
fix n ba
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 703
assume ind: "\<And>ba. \<lbrakk>b @ x # ba = xs @ replicate m y @ replicate n x;
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 704
x \<noteq> y; Suc (length ba) \<le> m + n\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 705
\<Longrightarrow> length ba < n"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 706
and h1: "b @ x # ba = xs @ replicate m y @ replicate (Suc n) x"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 707
and h2: "x \<noteq> y" and h3: "Suc (length ba) \<le> m + Suc n"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 708
show "length ba < Suc n"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 709
proof(cases "length ba")
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 710
case 0 thus "?thesis" by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 711
next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 712
fix nat
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 713
assume "length ba = Suc nat"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 714
hence "\<exists> ys a. ba = ys @ [a]"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 715
apply(rule_tac x = "butlast ba" in exI)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 716
apply(rule_tac x = "last ba" in exI)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 717
using append_butlast_last_id[of ba]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 718
apply(case_tac ba, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 719
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 720
from this obtain ys where "\<exists> a. ba = ys @ [a]" ..
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 721
from this obtain a where "ba = ys @ [a]" ..
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 722
thus "?thesis"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 723
using ind[of ys] h1 h2 h3
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 724
apply(simp del: rep_suc_rev replicate.simps add: rep_suc)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 725
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 726
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 727
qed
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]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 730
"\<lbrakk>b @ Oc # ba = xs @ Bk # replicate n Bk @ replicate n Oc;
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 731
Suc (length ba) \<le> 2 * n\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 732
\<Longrightarrow> length ba < n"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 733
apply(rule_tac length_append_diff_cons[of b Oc ba xs "Suc n" Bk n])
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 734
apply(simp, simp, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 735
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 736
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 737
lemma [elim]: "\<lbrakk>tstep (7, b, c) tcopy = (8, ab, ba);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 738
tcopy_F7 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F8 x (ab, ba)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 739
apply(case_tac x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 740
apply(simp_all add:tcopy_F8.simps tcopy_F7.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 741
tcopy_def tstep.simps fetch.simps new_tape.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 742
apply(simp split: if_splits list.splits block.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 743
apply(rule_tac x = "n" in exI, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 744
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 745
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 746
lemma [elim]: "\<lbrakk>tstep (7, b, c) tcopy = (7, ab, ba);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 747
tcopy_F7 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F7 x (ab, ba)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 748
apply(case_tac x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 749
apply(auto simp:tcopy_F7.simps tcopy_def tstep.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 750
fetch.simps new_tape.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 751
split: if_splits list.splits block.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 752
apply(rule_tac x = "n" in exI, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 753
apply(simp only: app_cons_app_simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 754
apply(frule replicate_tail_length, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 755
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 756
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 757
lemma Suc_more: "n <= m \<Longrightarrow> Suc m - n = Suc (m - n)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 758
by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 759
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 760
lemma [elim]: "\<lbrakk>tstep (6, b, c) tcopy = (7, ab, ba);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 761
tcopy_F6 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F7 x (ab, ba)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 762
apply(case_tac x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 763
apply(auto simp:tcopy_F7.simps tcopy_F6.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 764
tcopy_def tstep.simps fetch.simps new_tape.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 765
split: if_splits list.splits block.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 766
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 767
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 768
lemma [elim]: "\<lbrakk>tstep (6, b, c) tcopy = (6, ab, ba);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 769
tcopy_F6 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F6 x (ab, ba)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 770
apply(case_tac x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 771
apply(auto simp:tcopy_F6.simps tcopy_def tstep.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 772
new_tape.simps fetch.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 773
split: if_splits list.splits block.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 774
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 775
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 776
lemma [elim]: "\<lbrakk>tstep (5, b, c) tcopy = (6, ab, ba);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 777
tcopy_F5 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F6 x (ab, ba)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 778
apply(case_tac x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 779
apply(auto simp:tcopy_F5.simps tcopy_F6.simps tcopy_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 780
tstep.simps fetch.simps new_tape.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 781
split: if_splits list.splits block.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 782
apply(rule_tac x = n in exI, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 783
apply(rule_tac x = n in exI, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 784
apply(drule Suc_more, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 785
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 786
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 787
lemma ex_less_more2: "\<lbrakk>(n::nat) < x ; x <= 2 * n\<rbrakk> \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 788
\<exists>y. (x = n + y & y <= n)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 789
apply(rule_tac x = "x - n" in exI)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 790
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 791
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 792
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 793
lemma app_app_app_simp: "xs @ ys @ za = (xs @ ys) @ za"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 794
apply(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 795
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 796
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 797
lemma [elim]: "rev xs = replicate n b \<Longrightarrow> xs = replicate n b"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 798
using rev_replicate[of n b]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 799
thm rev_equal
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 800
by(drule_tac rev_equal, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 801
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 802
lemma app_cons_tail_same[dest]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 803
"\<lbrakk>rev b @ Oc # list =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 804
replicate (Suc (Suc na) - n) Oc @ replicate n Bk @ replicate n Oc;
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 805
Suc 0 < n; n \<le> Suc na; n < length list; length list \<le> 2 * n; b \<noteq> []\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 806
\<Longrightarrow> list = replicate n Bk @ replicate n Oc
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 807
& b = replicate (Suc na - n) Oc"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 808
using length_append_diff_cons[of "rev b" Oc list
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 809
"replicate (Suc (Suc na) - n) Oc" n Bk n]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 810
apply(case_tac "length list = 2*n", simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 811
using append_eq_append_conv[of "rev b @ [Oc]" "replicate
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 812
(Suc (Suc na) - n) Oc" "list" "replicate n Bk @ replicate n Oc"]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 813
apply(case_tac n, simp, simp add: Suc_more rep_suc
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 814
del: rep_suc_rev replicate.simps, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 815
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 816
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 817
lemma hd_replicate_false1: "\<lbrakk>replicate x Oc \<noteq> [];
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 818
hd (replicate x Oc) = Bk\<rbrakk> \<Longrightarrow> RR"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 819
apply(case_tac x, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 820
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 821
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 822
lemma hd_replicate_false2: "\<lbrakk>replicate x Oc \<noteq> [];
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 823
hd (replicate x Oc) \<noteq> Oc\<rbrakk> \<Longrightarrow> RR"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 824
apply(case_tac x, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 825
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 826
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 827
lemma Suc_more_less: "\<lbrakk>n \<le> Suc m; n >= m\<rbrakk> \<Longrightarrow> n = m | n = Suc m"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 828
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 829
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 830
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 831
lemma replicate_not_Nil: "replicate x a \<noteq> [] \<Longrightarrow> x > 0"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 832
apply(case_tac x, simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 833
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 834
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 835
lemma [elim]: "\<lbrakk>tstep (10, b, c) tcopy = (5, ab, ba);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 836
tcopy_F10 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F5 x (ab, ba)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 837
apply(case_tac x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 838
apply(auto simp:tcopy_F5.simps tcopy_F10.simps tcopy_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 839
tstep.simps fetch.simps new_tape.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 840
split: if_splits list.splits block.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 841
apply(frule app_cons_tail_same, simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 842
apply(rule_tac x = n in exI, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 843
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 844
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 845
lemma [elim]: "\<lbrakk>tstep (4, b, c) tcopy = (5, ab, ba);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 846
tcopy_F4 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F5 x (ab, ba)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 847
apply(case_tac x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 848
apply(auto simp:tcopy_F5.simps tcopy_F4.simps tcopy_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 849
tstep.simps fetch.simps new_tape.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 850
split: if_splits list.splits block.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 851
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 852
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 853
lemma [elim]: "\<lbrakk>tstep (3, b, c) tcopy = (4, ab, ba);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 854
tcopy_F3 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F4 x (ab, ba)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 855
apply(case_tac x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 856
apply(auto simp:tcopy_F3.simps tcopy_F4.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 857
tcopy_def tstep.simps fetch.simps new_tape.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 858
split: if_splits list.splits block.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 859
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 860
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 861
lemma [elim]: "\<lbrakk>tstep (4, b, c) tcopy = (4, ab, ba);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 862
tcopy_F4 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F4 x (ab, ba)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 863
apply(case_tac x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 864
apply(auto simp:tcopy_F3.simps tcopy_F4.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 865
tcopy_def tstep.simps fetch.simps new_tape.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 866
split: if_splits list.splits block.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 867
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 868
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 869
lemma [elim]: "\<lbrakk>tstep (3, b, c) tcopy = (3, ab, ba);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 870
tcopy_F3 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F3 x (ab, ba)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 871
apply(case_tac x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 872
apply(auto simp:tcopy_F3.simps tcopy_F4.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 873
tcopy_def tstep.simps fetch.simps new_tape.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 874
split: if_splits list.splits block.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 875
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 876
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 877
lemma replicate_cons_back: "y # replicate x y = replicate (Suc x) y"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 878
apply(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 879
done
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 replicate_cons_same: "bs @ (b # cs) = y # replicate x y \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 882
(\<exists>n. bs = replicate n y) & (b = y) & (\<exists>m. cs = replicate m y)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 883
apply(simp only: replicate_cons_back)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 884
apply(drule_tac replicate_same)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 885
apply(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 886
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 887
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 888
lemma [elim]: "\<lbrakk>tstep (2, b, c) tcopy = (3, ab, ba);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 889
tcopy_F2 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F3 x (ab, ba)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 890
apply(case_tac x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 891
apply(auto simp:tcopy_F3.simps tcopy_F2.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 892
tcopy_def tstep.simps fetch.simps new_tape.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 893
split: if_splits list.splits block.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 894
apply(drule replicate_cons_same, auto)+
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 895
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 896
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 897
lemma [elim]: "\<lbrakk>tstep (2, b, c) tcopy = (2, ab, ba);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 898
tcopy_F2 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F2 x (ab, ba)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 899
apply(case_tac x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 900
apply(auto simp:tcopy_F3.simps tcopy_F2.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 901
tcopy_def tstep.simps fetch.simps new_tape.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 902
split: if_splits list.splits block.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 903
apply(frule replicate_cons_same, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 904
apply(simp add: replicate_app_Cons_same)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 905
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 906
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 907
lemma [elim]: "\<lbrakk>tstep (Suc 0, b, c) tcopy = (2, ab, ba);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 908
tcopy_F1 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F2 x (ab, ba)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 909
apply(case_tac x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 910
apply(simp_all add:tcopy_F2.simps tcopy_F1.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 911
tcopy_def tstep.simps fetch.simps new_tape.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 912
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 913
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 914
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 915
lemma [elim]: "\<lbrakk>tstep (Suc 0, b, c) tcopy = (0, ab, ba);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 916
tcopy_F1 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F0 x (ab, ba)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 917
apply(case_tac x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 918
apply(simp_all add:tcopy_F0.simps tcopy_F1.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 919
tcopy_def tstep.simps fetch.simps new_tape.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 920
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 921
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 922
lemma ex_less: "Suc x <= y \<Longrightarrow> \<exists>z. y = x + z & z > 0"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 923
apply(rule_tac x = "y - x" in exI, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 924
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 925
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 926
lemma [elim]: "\<lbrakk>xs @ Bk # ba =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 927
Bk # Oc # replicate n Oc @ Bk # Oc # replicate n Oc;
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 928
length xs \<le> Suc n; xs \<noteq> []\<rbrakk> \<Longrightarrow> RR"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 929
apply(case_tac xs, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 930
apply(case_tac list, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 931
apply(drule ex_less, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 932
apply(simp add: replicate_add)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 933
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 934
apply(case_tac z, simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 935
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 936
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 937
lemma [elim]: "\<lbrakk>tstep (15, b, c) tcopy = (0, ab, ba);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 938
tcopy_F15 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F0 x (ab, ba)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 939
apply(case_tac x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 940
apply(auto simp: tcopy_F15.simps tcopy_F0.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 941
tcopy_def tstep.simps new_tape.simps fetch.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 942
split: if_splits list.splits block.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 943
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 944
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 945
lemma [elim]: "\<lbrakk>tstep (0, b, c) tcopy = (0, ab, ba);
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 946
tcopy_F0 x (b, c)\<rbrakk> \<Longrightarrow> tcopy_F0 x (ab, ba)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 947
apply(case_tac x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 948
apply(simp_all add: tcopy_F0.simps tcopy_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 949
tstep.simps new_tape.simps fetch.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 950
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 951
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 952
declare tstep.simps[simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 953
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 954
text {*
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 955
Finally establishes the invariant of Copying TM, which is used to dervie
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 956
the parital correctness of Copying TM.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 957
*}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 958
lemma inv_tcopy_step:"inv_tcopy x c \<Longrightarrow> inv_tcopy x (tstep c tcopy)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 959
apply(induct c)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 960
apply(auto split: if_splits block.splits list.splits taction.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 961
apply(auto simp: tstep.simps tcopy_def fetch.simps new_tape.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 962
split: if_splits list.splits block.splits taction.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 963
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 964
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 965
declare inv_tcopy.simps[simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 966
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 967
text {*
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 968
Invariant under mult-step execution.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 969
*}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 970
lemma inv_tcopy_steps:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 971
"inv_tcopy x (steps (Suc 0, [], replicate x Oc) tcopy stp) "
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 972
apply(induct stp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 973
apply(simp add: tstep.simps tcopy_def steps.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 974
tcopy_F1.simps inv_tcopy.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 975
apply(drule_tac inv_tcopy_step, simp add: tstep_red)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 976
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 977
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 978
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 979
text {*
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 980
The followng lemmas gives the parital correctness of Copying TM.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 981
*}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 982
theorem inv_tcopy_rs:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 983
"steps (Suc 0, [], replicate x Oc) tcopy stp = (0, l, r)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 984
\<Longrightarrow> \<exists> n. l = replicate n Bk \<and>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 985
r = replicate x Oc @ Bk # replicate x Oc"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 986
apply(insert inv_tcopy_steps[of x stp])
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 987
apply(auto simp: inv_tcopy.simps tcopy_F0.simps isBk.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 988
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 989
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 990
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 991
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
(*----------halt problem of tcopy----------------------------------------*)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 994
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 995
section {*
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 996
The following definitions are used to construct the measure function used to show
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 997
the termnation of Copying TM.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 998
*}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 999
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1000
definition lex_pair :: "((nat \<times> nat) \<times> nat \<times> nat) set"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1001
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1002
"lex_pair \<equiv> less_than <*lex*> less_than"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1003
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1004
definition lex_triple ::
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1005
"((nat \<times> (nat \<times> nat)) \<times> (nat \<times> (nat \<times> nat))) set"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1006
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1007
"lex_triple \<equiv> less_than <*lex*> lex_pair"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1008
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1009
definition lex_square ::
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1010
"((nat \<times> nat \<times> nat \<times> nat) \<times> (nat \<times> nat \<times> nat \<times> nat)) set"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1011
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1012
"lex_square \<equiv> less_than <*lex*> lex_triple"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1013
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1014
lemma wf_lex_triple: "wf lex_triple"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1015
by (auto intro:wf_lex_prod simp:lex_triple_def lex_pair_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1016
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1017
lemma wf_lex_square: "wf lex_square"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1018
by (auto intro:wf_lex_prod
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1019
simp:lex_triple_def lex_square_def lex_pair_def)
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
text {*
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1022
A measurement functions used to show the termination of copying machine:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1023
*}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1024
fun tcopy_phase :: "t_conf \<Rightarrow> nat"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1025
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1026
"tcopy_phase c = (let (state, tp) = c in
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1027
if state > 0 & state <= 4 then 5
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1028
else if state >=5 & state <= 10 then 4
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1029
else if state = 11 then 3
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1030
else if state = 12 | state = 13 then 2
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1031
else if state = 14 | state = 15 then 1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1032
else 0)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1033
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1034
fun tcopy_phase4_stage :: "tape \<Rightarrow> nat"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1035
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1036
"tcopy_phase4_stage (ln, rn) =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1037
(let lrn = (rev ln) @ rn
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1038
in length (takeWhile (\<lambda>a. a = Oc) lrn))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1039
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1040
fun tcopy_stage :: "t_conf \<Rightarrow> nat"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1041
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1042
"tcopy_stage c = (let (state, ln, rn) = c in
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1043
if tcopy_phase c = 5 then 0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1044
else if tcopy_phase c = 4 then
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1045
tcopy_phase4_stage (ln, rn)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1046
else if tcopy_phase c = 3 then 0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1047
else if tcopy_phase c = 2 then length rn
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1048
else if tcopy_phase c = 1 then 0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1049
else 0)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1050
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1051
fun tcopy_phase4_state :: "t_conf \<Rightarrow> nat"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1052
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1053
"tcopy_phase4_state c = (let (state, ln, rn) = c in
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1054
if state = 6 & hd rn = Oc then 0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1055
else if state = 5 then 1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1056
else 12 - state)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1057
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1058
fun tcopy_state :: "t_conf \<Rightarrow> nat"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1059
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1060
"tcopy_state c = (let (state, ln, rn) = c in
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1061
if tcopy_phase c = 5 then 4 - state
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1062
else if tcopy_phase c = 4 then
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1063
tcopy_phase4_state c
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1064
else if tcopy_phase c = 3 then 0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1065
else if tcopy_phase c = 2 then 13 - state
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1066
else if tcopy_phase c = 1 then 15 - state
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1067
else 0)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1068
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1069
fun tcopy_step2 :: "t_conf \<Rightarrow> nat"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1070
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1071
"tcopy_step2 (s, l, r) = length r"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1072
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1073
fun tcopy_step3 :: "t_conf \<Rightarrow> nat"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1074
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1075
"tcopy_step3 (s, l, r) = (if r = [] | r = [Bk] then Suc 0 else 0)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1076
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1077
fun tcopy_step4 :: "t_conf \<Rightarrow> nat"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1078
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1079
"tcopy_step4 (s, l, r) = length l"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1080
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1081
fun tcopy_step7 :: "t_conf \<Rightarrow> nat"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1082
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1083
"tcopy_step7 (s, l, r) = length r"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1084
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1085
fun tcopy_step8 :: "t_conf \<Rightarrow> nat"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1086
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1087
"tcopy_step8 (s, l, r) = length r"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1088
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1089
fun tcopy_step9 :: "t_conf \<Rightarrow> nat"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1090
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1091
"tcopy_step9 (s, l, r) = length l"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1092
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1093
fun tcopy_step10 :: "t_conf \<Rightarrow> nat"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1094
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1095
"tcopy_step10 (s, l, r) = length l"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1096
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1097
fun tcopy_step14 :: "t_conf \<Rightarrow> nat"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1098
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1099
"tcopy_step14 (s, l, r) = (case hd r of
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1100
Oc \<Rightarrow> 1 |
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1101
Bk \<Rightarrow> 0)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1102
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1103
fun tcopy_step15 :: "t_conf \<Rightarrow> nat"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1104
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1105
"tcopy_step15 (s, l, r) = length l"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1106
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1107
fun tcopy_step :: "t_conf \<Rightarrow> nat"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1108
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1109
"tcopy_step c = (let (state, ln, rn) = c in
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1110
if state = 0 | state = 1 | state = 11 |
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1111
state = 5 | state = 6 | state = 12 | state = 13 then 0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1112
else if state = 2 then tcopy_step2 c
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1113
else if state = 3 then tcopy_step3 c
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1114
else if state = 4 then tcopy_step4 c
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1115
else if state = 7 then tcopy_step7 c
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1116
else if state = 8 then tcopy_step8 c
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1117
else if state = 9 then tcopy_step9 c
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1118
else if state = 10 then tcopy_step10 c
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1119
else if state = 14 then tcopy_step14 c
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1120
else if state = 15 then tcopy_step15 c
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1121
else 0)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1122
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1123
text {*
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1124
The measure function used to show the termination of Copying TM.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1125
*}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1126
fun tcopy_measure :: "t_conf \<Rightarrow> (nat * nat * nat * nat)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1127
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1128
"tcopy_measure c =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1129
(tcopy_phase c, tcopy_stage c, tcopy_state c, tcopy_step c)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1130
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1131
definition tcopy_LE :: "((nat \<times> block list \<times> block list) \<times>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1132
(nat \<times> block list \<times> block list)) set"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1133
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1134
"tcopy_LE \<equiv> (inv_image lex_square tcopy_measure)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1135
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1136
lemma wf_tcopy_le: "wf tcopy_LE"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1137
by(auto intro:wf_inv_image wf_lex_square simp:tcopy_LE_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1138
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1139
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1140
declare steps.simps[simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1141
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1142
declare tcopy_phase.simps[simp del] tcopy_stage.simps[simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1143
tcopy_state.simps[simp del] tcopy_step.simps[simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1144
inv_tcopy.simps[simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1145
declare tcopy_F0.simps [simp]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1146
tcopy_F1.simps [simp]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1147
tcopy_F2.simps [simp]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1148
tcopy_F3.simps [simp]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1149
tcopy_F4.simps [simp]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1150
tcopy_F5.simps [simp]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1151
tcopy_F6.simps [simp]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1152
tcopy_F7.simps [simp]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1153
tcopy_F8.simps [simp]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1154
tcopy_F9.simps [simp]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1155
tcopy_F10.simps [simp]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1156
tcopy_F11.simps [simp]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1157
tcopy_F12.simps [simp]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1158
tcopy_F13.simps [simp]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1159
tcopy_F14.simps [simp]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1160
tcopy_F15.simps [simp]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1161
fetch.simps[simp]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1162
new_tape.simps[simp]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1163
lemma [elim]: "tcopy_F1 x (b, c) \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1164
(tstep (Suc 0, b, c) tcopy, Suc 0, b, c) \<in> tcopy_LE"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1165
apply(simp add: tcopy_F1.simps tstep.simps tcopy_def tcopy_LE_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1166
lex_square_def lex_triple_def lex_pair_def tcopy_phase.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1167
tcopy_stage.simps tcopy_state.simps tcopy_step.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1168
apply(simp split: if_splits list.splits block.splits taction.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1169
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1170
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1171
lemma [elim]: "tcopy_F2 x (b, c) \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1172
(tstep (2, b, c) tcopy, 2, b, c) \<in> tcopy_LE"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1173
apply(simp add:tstep.simps tcopy_def tcopy_LE_def lex_square_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1174
lex_triple_def lex_pair_def tcopy_phase.simps tcopy_stage.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1175
tcopy_state.simps tcopy_step.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1176
apply(simp split: if_splits list.splits block.splits taction.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1177
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1178
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1179
lemma [elim]: "tcopy_F3 x (b, c) \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1180
(tstep (3, b, c) tcopy, 3, b, c) \<in> tcopy_LE"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1181
apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1182
lex_triple_def lex_pair_def tcopy_phase.simps tcopy_stage.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1183
tcopy_state.simps tcopy_step.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1184
apply(simp split: if_splits list.splits block.splits taction.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1185
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1186
apply(case_tac x, simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1187
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1188
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1189
lemma [elim]: "tcopy_F4 x (b, c) \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1190
(tstep (4, b, c) tcopy, 4, b, c) \<in> tcopy_LE"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1191
apply(case_tac x, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1192
apply(simp add: tcopy_F4.simps tstep.simps tcopy_def tcopy_LE_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1193
lex_square_def lex_triple_def lex_pair_def tcopy_phase.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1194
tcopy_stage.simps tcopy_state.simps tcopy_step.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1195
apply(simp split: if_splits list.splits block.splits taction.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1196
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1197
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1198
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1199
lemma[simp]: "takeWhile (\<lambda>a. a = b) (replicate x b @ ys) =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1200
replicate x b @ (takeWhile (\<lambda>a. a = b) ys)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1201
apply(induct x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1202
apply(simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1203
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1204
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1205
lemma [elim]: "tcopy_F5 x (b, c) \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1206
(tstep (5, b, c) tcopy, 5, b, c) \<in> tcopy_LE"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1207
apply(case_tac x, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1208
apply(simp add: tstep.simps tcopy_def tcopy_LE_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1209
lex_square_def lex_triple_def lex_pair_def tcopy_phase.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1210
apply(simp split: if_splits list.splits block.splits taction.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1211
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1212
apply(simp_all add: tcopy_phase.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1213
tcopy_stage.simps tcopy_state.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1214
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1215
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1216
lemma [elim]: "\<lbrakk>replicate n x = []; n > 0\<rbrakk> \<Longrightarrow> RR"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1217
apply(case_tac n, simp+)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1218
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1219
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1220
lemma [elim]: "tcopy_F6 x (b, c) \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1221
(tstep (6, b, c) tcopy, 6, b, c) \<in> tcopy_LE"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1222
apply(case_tac x, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1223
apply(simp add: tstep.simps tcopy_def tcopy_LE_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1224
lex_square_def lex_triple_def lex_pair_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1225
tcopy_phase.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1226
apply(simp split: if_splits list.splits block.splits taction.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1227
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1228
apply(simp_all add: tcopy_phase.simps tcopy_stage.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1229
tcopy_state.simps tcopy_step.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1230
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1231
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1232
lemma [elim]: "tcopy_F7 x (b, c) \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1233
(tstep (7, b, c) tcopy, 7, b, c) \<in> tcopy_LE"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1234
apply(case_tac x, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1235
apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1236
lex_triple_def lex_pair_def tcopy_phase.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1237
apply(simp split: if_splits list.splits block.splits taction.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1238
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1239
apply(simp_all add: tcopy_phase.simps tcopy_stage.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1240
tcopy_state.simps tcopy_step.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1241
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1242
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1243
lemma [elim]: "tcopy_F8 x (b, c) \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1244
(tstep (8, b, c) tcopy, 8, b, c) \<in> tcopy_LE"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1245
apply(case_tac x, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1246
apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1247
lex_triple_def lex_pair_def tcopy_phase.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1248
apply(simp split: if_splits list.splits block.splits taction.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1249
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1250
apply(simp_all add: tcopy_phase.simps tcopy_stage.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1251
tcopy_state.simps tcopy_step.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1252
apply(simp only: app_cons_app_simp, frule replicate_tail_length, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1253
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1254
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1255
lemma app_app_app_equal: "xs @ ys @ zs = (xs @ ys) @ zs"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1256
by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1257
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1258
lemma append_cons_assoc: "as @ b # bs = (as @ [b]) @ bs"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1259
apply(rule rev_equal_rev)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1260
apply(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1261
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1262
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1263
lemma rev_tl_hd_merge: "bs \<noteq> [] \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1264
rev (tl bs) @ hd bs # as = rev bs @ as"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1265
apply(rule rev_equal_rev)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1266
apply(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1267
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1268
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1269
lemma [elim]: "tcopy_F9 x (b, c) \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1270
(tstep (9, b, c) tcopy, 9, b, c) \<in> tcopy_LE"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1271
apply(case_tac x, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1272
apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1273
lex_triple_def lex_pair_def tcopy_phase.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1274
apply(simp split: if_splits list.splits block.splits taction.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1275
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1276
apply(simp_all add: tcopy_phase.simps tcopy_stage.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1277
tcopy_state.simps tcopy_step.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1278
apply(drule_tac bs = b and as = "Bk # list" in rev_tl_hd_merge)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1279
apply(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1280
apply(drule_tac bs = b and as = "Oc # list" in rev_tl_hd_merge)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1281
apply(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1282
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1283
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1284
lemma [elim]: "tcopy_F10 x (b, c) \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1285
(tstep (10, b, c) tcopy, 10, b, c) \<in> tcopy_LE"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1286
apply(case_tac x, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1287
apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1288
lex_triple_def lex_pair_def tcopy_phase.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1289
apply(simp split: if_splits list.splits block.splits taction.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1290
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1291
apply(simp_all add: tcopy_phase.simps tcopy_stage.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1292
tcopy_state.simps tcopy_step.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1293
apply(drule_tac bs = b and as = "Bk # list" in rev_tl_hd_merge)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1294
apply(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1295
apply(drule_tac bs = b and as = "Oc # list" in rev_tl_hd_merge)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1296
apply(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1297
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1298
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1299
lemma [elim]: "tcopy_F11 x (b, c) \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1300
(tstep (11, b, c) tcopy, 11, b, c) \<in> tcopy_LE"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1301
apply(case_tac x, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1302
apply(simp add: tstep.simps tcopy_def tcopy_LE_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1303
lex_square_def lex_triple_def lex_pair_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1304
tcopy_phase.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1305
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1306
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1307
lemma [elim]: "tcopy_F12 x (b, c) \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1308
(tstep (12, b, c) tcopy, 12, b, c) \<in> tcopy_LE"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1309
apply(case_tac x, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1310
apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1311
lex_triple_def lex_pair_def tcopy_phase.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1312
apply(simp split: if_splits list.splits block.splits taction.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1313
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1314
apply(simp_all add: tcopy_phase.simps tcopy_stage.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1315
tcopy_state.simps tcopy_step.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1316
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1317
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1318
lemma [elim]: "tcopy_F13 x (b, c) \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1319
(tstep (13, b, c) tcopy, 13, b, c) \<in> tcopy_LE"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1320
apply(case_tac x, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1321
apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1322
lex_triple_def lex_pair_def tcopy_phase.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1323
apply(simp split: if_splits list.splits block.splits taction.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1324
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1325
apply(simp_all add: tcopy_phase.simps tcopy_stage.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1326
tcopy_state.simps tcopy_step.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1327
apply(drule equal_length, simp)+
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1328
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1329
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1330
lemma [elim]: "tcopy_F14 x (b, c) \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1331
(tstep (14, b, c) tcopy, 14, b, c) \<in> tcopy_LE"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1332
apply(case_tac x, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1333
apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1334
lex_triple_def lex_pair_def tcopy_phase.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1335
apply(simp split: if_splits list.splits block.splits taction.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1336
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1337
apply(simp_all add: tcopy_phase.simps tcopy_stage.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1338
tcopy_state.simps tcopy_step.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1339
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1340
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1341
lemma [elim]: "tcopy_F15 x (b, c) \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1342
(tstep (15, b, c) tcopy, 15, b, c) \<in> tcopy_LE"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1343
apply(case_tac x, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1344
apply(simp add: tstep.simps tcopy_def tcopy_LE_def lex_square_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1345
lex_triple_def lex_pair_def tcopy_phase.simps )
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1346
apply(simp split: if_splits list.splits block.splits taction.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1347
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1348
apply(simp_all add: tcopy_phase.simps tcopy_stage.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1349
tcopy_state.simps tcopy_step.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1350
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1351
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1352
lemma tcopy_wf_step:"\<lbrakk>a > 0; inv_tcopy x (a, b, c)\<rbrakk> \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1353
(tstep (a, b, c) tcopy, (a, b, c)) \<in> tcopy_LE"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1354
apply(simp add:inv_tcopy.simps split: if_splits, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1355
apply(auto simp: tstep.simps tcopy_def tcopy_LE_def lex_square_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1356
lex_triple_def lex_pair_def tcopy_phase.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1357
tcopy_stage.simps tcopy_state.simps tcopy_step.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1358
split: if_splits list.splits block.splits taction.splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1359
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1360
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1361
lemma tcopy_wf:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1362
"\<forall>n. let nc = steps (Suc 0, [], replicate x Oc) tcopy n in
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1363
let Sucnc = steps (Suc 0, [], replicate x Oc) tcopy (Suc n) in
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1364
\<not> isS0 nc \<longrightarrow> ((Sucnc, nc) \<in> tcopy_LE)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1365
proof(rule allI, case_tac
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1366
"steps (Suc 0, [], replicate x Oc) tcopy n", auto simp: tstep_red)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1367
fix n a b c
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1368
assume h: "\<not> isS0 (a, b, c)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1369
"steps (Suc 0, [], replicate x Oc) tcopy n = (a, b, c)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1370
hence "inv_tcopy x (a, b, c)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1371
using inv_tcopy_steps[of x n] by(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1372
thus "(tstep (a, b, c) tcopy, a, b, c) \<in> tcopy_LE"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1373
using h
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1374
by(rule_tac tcopy_wf_step, auto simp: isS0_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1375
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1376
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1377
text {*
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1378
The termination of Copying TM:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1379
*}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1380
lemma tcopy_halt:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1381
"\<exists>n. isS0 (steps (Suc 0, [], replicate x Oc) tcopy n)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1382
apply(insert halt_lemma
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1383
[of tcopy_LE isS0 "steps (Suc 0, [], replicate x Oc) tcopy"])
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1384
apply(insert tcopy_wf [of x])
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1385
apply(simp only: Let_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1386
apply(insert wf_tcopy_le)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1387
apply(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1388
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1389
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1390
text {*
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1391
The total correntess of Copying TM:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1392
*}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1393
theorem tcopy_halt_rs: "\<exists>stp m.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1394
steps (Suc 0, [], replicate x Oc) tcopy stp =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1395
(0, replicate m Bk, replicate x Oc @ Bk # replicate x Oc)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1396
using tcopy_halt[of x]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1397
proof(erule_tac exE)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1398
fix n
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1399
assume h: "isS0 (steps (Suc 0, [], replicate x Oc) tcopy n)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1400
have "inv_tcopy x (steps (Suc 0, [], replicate x Oc) tcopy n)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1401
using inv_tcopy_steps[of x n] by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1402
thus "?thesis"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1403
using h
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1404
apply(cases "(steps (Suc 0, [], replicate x Oc) tcopy n)",
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1405
auto simp: isS0_def inv_tcopy.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1406
apply(rule_tac x = n in exI, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1407
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1408
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1409
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1410
section {*
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1411
The {\em Dithering} Turing Machine
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1412
*}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1413
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1414
text {*
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1415
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
+ − 1416
terminate.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1417
*}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1418
definition dither :: "tprog"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1419
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1420
"dither \<equiv> [(W0, 1), (R, 2), (L, 1), (L, 0)] "
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1421
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1422
lemma dither_halt_rs:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1423
"\<exists> stp. steps (Suc 0, Bk\<^bsup>m\<^esup>, [Oc, Oc]) dither stp =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1424
(0, Bk\<^bsup>m\<^esup>, [Oc, Oc])"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1425
apply(rule_tac x = "Suc (Suc (Suc 0))" in exI)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1426
apply(simp add: dither_def steps.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1427
tstep.simps fetch.simps new_tape.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1428
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1429
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1430
lemma dither_unhalt_state:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1431
"(steps (Suc 0, Bk\<^bsup>m\<^esup>, [Oc]) dither stp =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1432
(Suc 0, Bk\<^bsup>m\<^esup>, [Oc])) \<or>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1433
(steps (Suc 0, Bk\<^bsup>m\<^esup>, [Oc]) dither stp = (2, Oc # Bk\<^bsup>m\<^esup>, []))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1434
apply(induct stp, simp add: steps.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1435
apply(simp add: tstep_red, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1436
apply(auto simp: tstep.simps fetch.simps dither_def new_tape.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1437
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1438
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1439
lemma dither_unhalt_rs:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1440
"\<not> (\<exists> stp. isS0 (steps (Suc 0, Bk\<^bsup>m\<^esup>, [Oc]) dither stp))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1441
proof(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1442
fix stp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1443
assume h1: "isS0 (steps (Suc 0, Bk\<^bsup>m\<^esup>, [Oc]) dither stp)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1444
have "\<not> isS0 ((steps (Suc 0, Bk\<^bsup>m\<^esup>, [Oc]) dither stp))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1445
using dither_unhalt_state[of m stp]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1446
by(auto simp: isS0_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1447
from h1 and this show False by (auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1448
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1449
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1450
section {*
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1451
The final diagnal arguments to show the undecidability of Halting problem.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1452
*}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1453
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1454
text {*
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1455
@{text "haltP tp x"} means TM @{text "tp"} terminates on input @{text "x"}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1456
and the final configuration is standard.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1457
*}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1458
definition haltP :: "tprog \<Rightarrow> nat \<Rightarrow> bool"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1459
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1460
"haltP t x = (\<exists>n a b c. steps (Suc 0, [], Oc\<^bsup>x\<^esup>) t n = (0, Bk\<^bsup>a\<^esup>, Oc\<^bsup>b\<^esup> @ Bk\<^bsup>c\<^esup>))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1461
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1462
lemma [simp]: "length (A |+| B) = length A + length B"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1463
by(auto simp: t_add.simps tshift.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1464
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1465
lemma [intro]: "\<lbrakk>iseven (x::nat); iseven y\<rbrakk> \<Longrightarrow> iseven (x + y)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1466
apply(auto simp: iseven_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1467
apply(rule_tac x = "x + xa" in exI, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1468
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1469
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1470
lemma t_correct_add[intro]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1471
"\<lbrakk>t_correct A; t_correct B\<rbrakk> \<Longrightarrow> t_correct (A |+| B)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1472
apply(auto simp: t_correct.simps tshift.simps t_add.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1473
change_termi_state.simps list_all_iff)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1474
apply(erule_tac x = "(a, b)" in ballE, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1475
apply(case_tac "ba = 0", auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1476
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1477
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1478
lemma [intro]: "t_correct tcopy"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1479
apply(simp add: t_correct.simps tcopy_def iseven_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1480
apply(rule_tac x = 15 in exI, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1481
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1482
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1483
lemma [intro]: "t_correct dither"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1484
apply(simp add: t_correct.simps dither_def iseven_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1485
apply(rule_tac x = 2 in exI, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1486
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1487
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1488
text {*
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1489
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
+ − 1490
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
+ − 1491
under this locale. Therefore, the undecidability of {\em Halting Problem}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1492
is established.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1493
*}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1494
locale uncomputable =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1495
-- {* 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
+ − 1496
funciton @{text "code"} does not affect the final result. *}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1497
fixes code :: "tprog \<Rightarrow> nat"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1498
-- {*
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1499
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
+ − 1500
*}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1501
and H :: "tprog"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1502
assumes h_wf[intro]: "t_correct H"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1503
-- {*
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1504
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
+ − 1505
*}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1506
and h_case:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1507
"\<And> M n. \<lbrakk>(haltP M n)\<rbrakk> \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1508
\<exists> na nb. (steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na = (0, Bk\<^bsup>nb\<^esup>, [Oc]))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1509
and nh_case:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1510
"\<And> M n. \<lbrakk>(\<not> haltP M n)\<rbrakk> \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1511
\<exists> na nb. (steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code M\<^esup> @ Bk # Oc\<^bsup>n\<^esup>) H na = (0, Bk\<^bsup>nb\<^esup>, [Oc, Oc]))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1512
begin
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1513
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1514
term t_correct
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1515
declare haltP_def[simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1516
definition tcontra :: "tprog \<Rightarrow> tprog"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1517
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1518
"tcontra h \<equiv> ((tcopy |+| h) |+| dither)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1519
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1520
lemma [simp]: "a\<^bsup>0\<^esup> = []"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1521
by(simp add: exponent_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1522
lemma haltP_weaking:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1523
"haltP (tcontra H) (code (tcontra H)) \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1524
\<exists>stp. isS0 (steps (Suc 0, [], Oc\<^bsup>code (tcontra H)\<^esup>)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1525
((tcopy |+| H) |+| dither) stp)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1526
apply(simp add: haltP_def, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1527
apply(rule_tac x = n in exI, simp add: isS0_def tcontra_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1528
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1529
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1530
lemma h_uh: "haltP (tcontra H) (code (tcontra H))
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1531
\<Longrightarrow> \<not> haltP (tcontra H) (code (tcontra H))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1532
proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1533
let ?cn = "code (tcontra H)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1534
let ?P1 = "\<lambda> tp. let (l, r) = tp in (l = [] \<and>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1535
(r::block list) = Oc\<^bsup>(?cn)\<^esup>)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1536
let ?Q1 = "\<lambda> (l, r).(\<exists> nb. l = Bk\<^bsup>nb\<^esup> \<and>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1537
r = Oc\<^bsup>(?cn)\<^esup> @ Bk # Oc\<^bsup>(?cn)\<^esup>)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1538
let ?P2 = ?Q1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1539
let ?Q2 = "\<lambda> (l, r). (\<exists> nd. l = Bk\<^bsup>nd \<^esup>\<and> r = [Oc])"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1540
let ?P3 = "\<lambda> tp. False"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1541
assume h: "haltP (tcontra H) (code (tcontra H))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1542
hence h1: "\<And> x. \<exists> na nb. steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>code (tcontra H)\<^esup> @ Bk #
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1543
Oc\<^bsup>code (tcontra H)\<^esup>) H na = (0, Bk\<^bsup>nb\<^esup>, [Oc])"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1544
by(drule_tac x = x in h_case, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1545
have "?P1 \<turnstile>-> \<lambda> tp. (\<exists> stp tp'. steps (Suc 0, tp) (tcopy |+| H) stp = (0, tp') \<and> ?Q2 tp')"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1546
proof(rule_tac turing_merge.t_merge_halt[of tcopy H "?P1" "?P2" "?P3"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1547
"?P3" "?Q1" "?Q2"], auto simp: turing_merge_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1548
show "\<exists>stp. case steps (Suc 0, [], Oc\<^bsup>?cn\<^esup>) tcopy stp of (s, tp') \<Rightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1549
s = 0 \<and> (case tp' of (l, r) \<Rightarrow> (\<exists>nb. l = Bk\<^bsup>nb\<^esup>) \<and> r = Oc\<^bsup>?cn\<^esup> @ Bk # Oc\<^bsup>?cn\<^esup>)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1550
using tcopy_halt_rs[of "?cn"]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1551
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1552
apply(rule_tac x = stp in exI, auto simp: exponent_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1553
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1554
next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1555
fix nb
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1556
show "\<exists>stp. case steps (Suc 0, Bk\<^bsup>nb\<^esup>, Oc\<^bsup>code (tcontra H)\<^esup> @ Bk # Oc\<^bsup>code (tcontra H)\<^esup>) H stp of
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1557
(s, tp') \<Rightarrow> s = 0 \<and> (case tp' of (l, r) \<Rightarrow> (\<exists>nd. l = Bk\<^bsup>nd\<^esup>) \<and> r = [Oc])"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1558
using h1[of nb]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1559
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1560
apply(rule_tac x = na in exI, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1561
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1562
next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1563
show "\<lambda>(l, r). ((\<exists>nb. l = Bk\<^bsup>nb\<^esup>) \<and> r = Oc\<^bsup>code (tcontra H)\<^esup> @ Bk # Oc\<^bsup>code (tcontra H)\<^esup>) \<turnstile>->
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1564
\<lambda>(l, r). ((\<exists>nb. l = Bk\<^bsup>nb\<^esup>) \<and> r = Oc\<^bsup>code (tcontra H)\<^esup> @ Bk # Oc\<^bsup>code (tcontra H)\<^esup>)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1565
apply(simp add: t_imply_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1566
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1567
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1568
hence "\<exists>stp tp'. steps (Suc 0, [], Oc\<^bsup>?cn\<^esup>) (tcopy |+| H) stp = (0, tp') \<and>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1569
(case tp' of (l, r) \<Rightarrow> \<exists>nd. l = Bk\<^bsup>nd\<^esup> \<and> r = [Oc])"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1570
apply(simp add: t_imply_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1571
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1572
hence "?P1 \<turnstile>-> \<lambda> tp. \<not> (\<exists> stp. isS0 (steps (Suc 0, tp) ((tcopy |+| H) |+| dither) stp))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1573
proof(rule_tac turing_merge.t_merge_uhalt[of "tcopy |+| H" dither "?P1" "?P3" "?P3"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1574
"?Q2" "?Q2" "?Q2"], simp add: turing_merge_def, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1575
fix stp nd
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1576
assume "steps (Suc 0, [], Oc\<^bsup>code (tcontra H)\<^esup>) (tcopy |+| H) stp = (0, Bk\<^bsup>nd\<^esup>, [Oc])"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1577
thus "\<exists>stp. case steps (Suc 0, [], Oc\<^bsup>code (tcontra H)\<^esup>) (tcopy |+| H) stp of (s, tp')
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1578
\<Rightarrow> s = 0 \<and> (case tp' of (l, r) \<Rightarrow> (\<exists>nd. l = Bk\<^bsup>nd\<^esup>) \<and> r = [Oc])"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1579
apply(rule_tac x = stp in exI, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1580
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1581
next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1582
fix stp nd nda stpa
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1583
assume "isS0 (steps (Suc 0, Bk\<^bsup>nda\<^esup>, [Oc]) dither stpa)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1584
thus "False"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1585
using dither_unhalt_rs[of nda]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1586
apply auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1587
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1588
next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1589
fix stp nd
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1590
show "\<lambda>(l, r). ((\<exists>nd. l = Bk\<^bsup>nd\<^esup>) \<and> r = [Oc]) \<turnstile>->
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1591
\<lambda>(l, r). ((\<exists>nd. l = Bk\<^bsup>nd\<^esup>) \<and> r = [Oc])"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1592
by (simp add: t_imply_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1593
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1594
thus "\<not> haltP (tcontra H) (code (tcontra H))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1595
apply(simp add: t_imply_def haltP_def tcontra_def, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1596
apply(erule_tac x = n in allE, simp add: isS0_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1597
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1598
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1599
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1600
lemma uh_h:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1601
assumes uh: "\<not> haltP (tcontra H) (code (tcontra H))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1602
shows "haltP (tcontra H) (code (tcontra H))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1603
proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1604
let ?cn = "code (tcontra H)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1605
have h1: "\<And> x. \<exists> na nb. steps (Suc 0, Bk\<^bsup>x\<^esup>, Oc\<^bsup>?cn\<^esup> @ Bk # Oc\<^bsup>?cn\<^esup>)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1606
H na = (0, Bk\<^bsup>nb\<^esup>, [Oc, Oc])"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1607
using uh
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1608
by(drule_tac x = x in nh_case, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1609
let ?P1 = "\<lambda> tp. let (l, r) = tp in (l = [] \<and>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1610
(r::block list) = Oc\<^bsup>(?cn)\<^esup>)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1611
let ?Q1 = "\<lambda> (l, r).(\<exists> na. l = Bk\<^bsup>na\<^esup> \<and> r = [Oc, Oc])"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1612
let ?P2 = ?Q1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1613
let ?Q2 = ?Q1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1614
let ?P3 = "\<lambda> tp. False"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1615
have "?P1 \<turnstile>-> \<lambda> tp. (\<exists> stp tp'. steps (Suc 0, tp) ((tcopy |+| H ) |+| dither)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1616
stp = (0, tp') \<and> ?Q2 tp')"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1617
proof(rule_tac turing_merge.t_merge_halt[of "tcopy |+| H" dither ?P1 ?P2 ?P3 ?P3
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1618
?Q1 ?Q2], auto simp: turing_merge_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1619
show "\<exists>stp. case steps (Suc 0, [], Oc\<^bsup>code (tcontra H)\<^esup>) (tcopy |+| H) stp of (s, tp') \<Rightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1620
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1621
s = 0 \<and> (case tp' of (l, r) \<Rightarrow> (\<exists>na. l = Bk\<^bsup>na\<^esup>) \<and> r = [Oc, Oc])"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1622
proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1623
let ?Q1 = "\<lambda> (l, r).(\<exists> nb. l = Bk\<^bsup>nb\<^esup> \<and> r = Oc\<^bsup>(?cn)\<^esup> @ Bk # Oc\<^bsup>(?cn)\<^esup>)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1624
let ?P2 = "?Q1"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1625
let ?Q2 = "\<lambda> (l, r).(\<exists> na. l = Bk\<^bsup>na\<^esup> \<and> r = [Oc, Oc])"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1626
have "?P1 \<turnstile>-> \<lambda> tp. (\<exists> stp tp'. steps (Suc 0, tp) (tcopy |+| H )
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1627
stp = (0, tp') \<and> ?Q2 tp')"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1628
proof(rule_tac turing_merge.t_merge_halt[of tcopy H ?P1 ?P2 ?P3 ?P3
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1629
?Q1 ?Q2], auto simp: turing_merge_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1630
show "\<exists>stp. case steps (Suc 0, [], Oc\<^bsup>code (tcontra H)\<^esup>) tcopy stp of (s, tp') \<Rightarrow> s = 0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1631
\<and> (case tp' of (l, r) \<Rightarrow> (\<exists>nb. l = Bk\<^bsup>nb\<^esup>) \<and> r = Oc\<^bsup>code (tcontra H)\<^esup> @ Bk # Oc\<^bsup>code (tcontra H)\<^esup>)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1632
using tcopy_halt_rs[of "?cn"]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1633
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1634
apply(rule_tac x = stp in exI, simp add: exponent_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1635
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1636
next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1637
fix nb
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1638
show "\<exists>stp. case steps (Suc 0, Bk\<^bsup>nb\<^esup>, Oc\<^bsup>code (tcontra H)\<^esup> @ Bk # Oc\<^bsup>code (tcontra H)\<^esup>) H stp of
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1639
(s, tp') \<Rightarrow> s = 0 \<and> (case tp' of (l, r) \<Rightarrow> (\<exists>na. l = Bk\<^bsup>na\<^esup>) \<and> r = [Oc, Oc])"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1640
using h1[of nb]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1641
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1642
apply(rule_tac x = na in exI, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1643
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1644
next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1645
show "\<lambda>(l, r). ((\<exists>nb. l = Bk\<^bsup>nb\<^esup>) \<and> r = Oc\<^bsup>code (tcontra H)\<^esup> @ Bk # Oc\<^bsup>code (tcontra H)\<^esup>) \<turnstile>->
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1646
\<lambda>(l, r). ((\<exists>nb. l = Bk\<^bsup>nb\<^esup>) \<and> r = Oc\<^bsup>code (tcontra H)\<^esup> @ Bk # Oc\<^bsup>code (tcontra H)\<^esup>)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1647
by(simp add: t_imply_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1648
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1649
hence "(\<exists> stp tp'. steps (Suc 0, [], Oc\<^bsup>?cn\<^esup>) (tcopy |+| H ) stp = (0, tp') \<and> ?Q2 tp')"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1650
apply(simp add: t_imply_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1651
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1652
thus "?thesis"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1653
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1654
apply(rule_tac x = stp in exI, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1655
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1656
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1657
next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1658
fix na
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1659
show "\<exists>stp. case steps (Suc 0, Bk\<^bsup>na\<^esup>, [Oc, Oc]) dither stp of (s, tp')
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1660
\<Rightarrow> s = 0 \<and> (case tp' of (l, r) \<Rightarrow> (\<exists>na. l = Bk\<^bsup>na\<^esup>) \<and> r = [Oc, Oc])"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1661
using dither_halt_rs[of na]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1662
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1663
apply(rule_tac x = stp in exI, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1664
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1665
next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1666
show "\<lambda>(l, r). ((\<exists>na. l = Bk\<^bsup>na\<^esup>) \<and> r = [Oc, Oc]) \<turnstile>->
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1667
(\<lambda>(l, r). (\<exists>na. l = Bk\<^bsup>na\<^esup>) \<and> r = [Oc, Oc])"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1668
by (simp add: t_imply_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1669
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1670
hence "\<exists> stp tp'. steps (Suc 0, [], Oc\<^bsup>?cn\<^esup>) ((tcopy |+| H ) |+| dither)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1671
stp = (0, tp') \<and> ?Q2 tp'"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1672
apply(simp add: t_imply_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1673
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1674
thus "haltP (tcontra H) (code (tcontra H))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1675
apply(auto simp: haltP_def tcontra_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1676
apply(rule_tac x = stp in exI,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1677
rule_tac x = na in exI,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1678
rule_tac x = "Suc (Suc 0)" in exI,
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1679
rule_tac x = "0" in exI, simp add: exp_ind_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1680
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1681
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1682
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1683
text {*
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1684
@{text "False"} is finally derived.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1685
*}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1686
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1687
lemma "False"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1688
using uh_h h_uh
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1689
by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1690
end
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1691
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1692
end
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1693