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