246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1
theory UF_Rec
258
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 2
imports Recs Turing2
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 3
begin
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 4
267
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 5
section {* Coding of Turing Machines and Tapes*}
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 6
258
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 7
267
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 8
fun actnum :: "action \<Rightarrow> nat"
258
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 9
where
267
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 10
"actnum W0 = 0"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 11
| "actnum W1 = 1"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 12
| "actnum L = 2"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 13
| "actnum R = 3"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 14
| "actnum Nop = 4"
258
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 15
267
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 16
fun cellnum :: "cell \<Rightarrow> nat" where
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 17
"cellnum Bk = 0"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 18
| "cellnum Oc = 1"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 19
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 20
text {* Coding tapes *}
258
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 21
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 22
fun code_tp :: "cell list \<Rightarrow> nat list"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 23
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 24
"code_tp [] = []"
267
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 25
| "code_tp (c # tp) = (cellnum c) # code_tp tp"
258
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 26
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 27
fun Code_tp where
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 28
"Code_tp tp = lenc (code_tp tp)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 29
261
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 30
lemma code_tp_append [simp]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 31
"code_tp (tp1 @ tp2) = code_tp tp1 @ code_tp tp2"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 32
by(induct tp1) (simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 33
260
1e45b5b6482a
added definitions and proofs for right-std and left-std tapes
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 34
lemma code_tp_length [simp]:
1e45b5b6482a
added definitions and proofs for right-std and left-std tapes
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 35
"length (code_tp tp) = length tp"
1e45b5b6482a
added definitions and proofs for right-std and left-std tapes
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 36
by (induct tp) (simp_all)
1e45b5b6482a
added definitions and proofs for right-std and left-std tapes
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 37
1e45b5b6482a
added definitions and proofs for right-std and left-std tapes
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 38
lemma code_tp_nth [simp]:
267
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 39
"n < length tp \<Longrightarrow> (code_tp tp) ! n = cellnum (tp ! n)"
260
1e45b5b6482a
added definitions and proofs for right-std and left-std tapes
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 40
apply(induct n arbitrary: tp)
1e45b5b6482a
added definitions and proofs for right-std and left-std tapes
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 41
apply(simp_all)
1e45b5b6482a
added definitions and proofs for right-std and left-std tapes
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 42
apply(case_tac [!] tp)
1e45b5b6482a
added definitions and proofs for right-std and left-std tapes
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 43
apply(simp_all)
1e45b5b6482a
added definitions and proofs for right-std and left-std tapes
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 44
done
1e45b5b6482a
added definitions and proofs for right-std and left-std tapes
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 45
261
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 46
lemma code_tp_replicate [simp]:
267
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 47
"code_tp (c \<up> n) = (cellnum c) \<up> n"
261
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 48
by(induct n) (simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 49
267
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 50
text {* Coding Configurations and TMs *}
261
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 51
258
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 52
fun Code_conf where
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 53
"Code_conf (s, l, r) = (s, Code_tp l, Code_tp r)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 54
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 55
fun code_instr :: "instr \<Rightarrow> nat" where
267
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 56
"code_instr i = penc (actnum (fst i)) (snd i)"
258
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 Code_instr :: "instr \<times> instr \<Rightarrow> nat" where
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 59
"Code_instr i = penc (code_instr (fst i)) (code_instr (snd i))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 60
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 61
fun code_tprog :: "tprog \<Rightarrow> nat list"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 62
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 63
"code_tprog [] = []"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 64
| "code_tprog (i # tm) = Code_instr i # code_tprog tm"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 65
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 66
lemma code_tprog_length [simp]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 67
"length (code_tprog tp) = length tp"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 68
by (induct tp) (simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 69
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 70
lemma code_tprog_nth [simp]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 71
"n < length tp \<Longrightarrow> (code_tprog tp) ! n = Code_instr (tp ! n)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 72
by (induct tp arbitrary: n) (simp_all add: nth_Cons')
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 73
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 74
fun Code_tprog :: "tprog \<Rightarrow> nat"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 75
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 76
"Code_tprog tm = lenc (code_tprog tm)"
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 77
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 78
267
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 79
section {* An Universal Function in HOL *}
258
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 80
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 81
text {* Reading and writing the encoded tape *}
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 82
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 83
fun Read where
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 84
"Read tp = ldec tp 0"
250
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 85
258
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 86
fun Write where
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 87
"Write n tp = penc (Suc n) (pdec2 tp)"
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 88
258
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 89
text {*
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 90
The @{text Newleft} and @{text Newright} functions on page 91 of B book.
267
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 91
They calculate the new left and right tape (@{text p} and @{text r})
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 92
according to an action @{text a}. Adapted to our encoding functions.
258
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 93
*}
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 94
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 95
fun Newleft :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 96
where
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 97
"Newleft l r a = (if a = 0 then l else
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 98
if a = 1 then l else
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 99
if a = 2 then pdec2 l else
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 100
if a = 3 then penc (Suc (Read r)) l
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 101
else l)"
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 102
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 103
fun Newright :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 104
where
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 105
"Newright l r a = (if a = 0 then Write 0 r
258
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 106
else if a = 1 then Write 1 r
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 107
else if a = 2 then penc (Suc (Read l)) r
258
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 108
else if a = 3 then pdec2 r
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 109
else r)"
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
text {*
263
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 112
The @{text "Action"} function given on page 92 of B book, which is used to
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 113
fetch Turing Machine intructions. In @{text "Action m q r"}, @{text "m"} is
258
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 114
the code of the Turing Machine, @{text "q"} is the current state of
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 115
Turing Machine, and @{text "r"} is the scanned cell of is the right tape.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 116
*}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 117
263
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 118
fun Actn :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 119
"Actn n 0 = pdec1 (pdec1 n)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 120
| "Actn n _ = pdec1 (pdec2 n)"
250
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 121
263
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 122
fun Action :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 123
where
263
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 124
"Action m q c = (if q \<noteq> 0 \<and> within m (q - 1) then Actn (ldec m (q - 1)) c else 4)"
258
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 125
263
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 126
fun Newstat :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 127
"Newstat n 0 = pdec2 (pdec1 n)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 128
| "Newstat n _ = pdec2 (pdec2 n)"
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 129
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 130
fun Newstate :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 131
where
263
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 132
"Newstate m q r = (if q \<noteq> 0 then Newstat (ldec m (q - 1)) r else 0)"
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 133
258
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 134
fun Conf :: "nat \<times> (nat \<times> nat) \<Rightarrow> nat"
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 135
where
261
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 136
"Conf (q, l, r) = lenc [q, l, r]"
258
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 137
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 138
fun State where
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 139
"State cf = ldec cf 0"
246
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 Left where
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 142
"Left cf = ldec cf 1"
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 143
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 144
fun Right where
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 145
"Right cf = ldec cf 2"
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 146
267
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 147
text {*
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 148
@{text "Steps cf m k"} computes the TM configuration after @{text "k"} steps of
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 149
execution of TM coded as @{text "m"}. @{text Step} is a single step of the TM.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 150
*}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 151
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 152
fun Step :: "nat \<Rightarrow> nat \<Rightarrow> nat"
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 153
where
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 154
"Step cf m = Conf (Newstate m (State cf) (Read (Right cf)),
263
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 155
Newleft (Left cf) (Right cf) (Action m (State cf) (Read (Right cf))),
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 156
Newright (Left cf) (Right cf) (Action m (State cf) (Read (Right cf))))"
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 157
258
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 158
fun Steps :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 159
where
258
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 160
"Steps cf p 0 = cf"
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 161
| "Steps cf p (Suc n) = Steps (Step cf p) p n"
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 162
265
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 163
lemma Step_Steps_comm:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 164
"Step (Steps cf p n) p = Steps (Step cf p) p n"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 165
by (induct n arbitrary: cf) (simp_all only: Steps.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 166
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 167
267
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 168
text {* Decoding tapes back into numbers. *}
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 169
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 170
definition Stknum :: "nat \<Rightarrow> nat"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 171
where
261
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 172
"Stknum z \<equiv> (\<Sum>i < enclen z. ldec z i)"
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 173
261
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 174
lemma Stknum_append:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 175
"Stknum (Code_tp (tp1 @ tp2)) = Stknum (Code_tp tp1) + Stknum (Code_tp tp2)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 176
apply(simp only: Code_tp.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 177
apply(simp only: code_tp_append)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 178
apply(simp only: Stknum_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 179
apply(simp only: enclen_length length_append code_tp_length)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 180
apply(simp only: list_encode_inverse)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 181
apply(simp only: enclen_length length_append code_tp_length)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 182
apply(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 183
apply(subgoal_tac "{..<length tp1 + length tp2} = {..<length tp1} \<union> {length tp1 ..<length tp1 + length tp2}")
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 184
prefer 2
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 185
apply(auto)[1]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 186
apply(simp only:)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 187
apply(subst setsum_Un_disjoint)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 188
apply(auto)[2]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 189
apply (metis ivl_disj_int_one(2))
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 190
apply(simp add: nth_append)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 191
apply(subgoal_tac "{length tp1..<length tp1 + length tp2} = (\<lambda>x. x + length tp1) ` {0..<length tp2}")
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 192
prefer 2
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 193
apply(simp only: image_add_atLeastLessThan)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 194
apply (metis comm_monoid_add_class.add.left_neutral nat_add_commute)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 195
apply(simp only:)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 196
apply(subst setsum_reindex)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 197
prefer 2
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 198
apply(simp add: comp_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 199
apply (metis atLeast0LessThan)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 200
apply(simp add: inj_on_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 201
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 202
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 203
lemma Stknum_up:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 204
"Stknum (lenc (a \<up> n)) = n * a"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 205
apply(induct n)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 206
apply(simp_all add: Stknum_def list_encode_inverse del: replicate.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 207
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 208
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 209
lemma result:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 210
"Stknum (Code_tp (<n> @ Bk \<up> l)) - 1 = n"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 211
apply(simp only: Stknum_append)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 212
apply(simp only: tape_of_nat.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 213
apply(simp only: Code_tp.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 214
apply(simp only: code_tp_replicate)
267
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 215
apply(simp only: cellnum.simps)
261
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 216
apply(simp only: Stknum_up)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 217
apply(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 218
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 219
267
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 220
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 221
section {* Standard Tapes *}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 222
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 223
definition
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 224
"right_std z \<equiv> (\<exists>i \<le> enclen z. 1 \<le> i \<and> (\<forall>j < i. ldec z j = 1) \<and> (\<forall>j < enclen z - i. ldec z (i + j) = 0))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 225
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 226
definition
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 227
"left_std z \<equiv> (\<forall>j < enclen z. ldec z j = 0)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 228
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 229
lemma ww:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 230
"(\<exists>k l. 1 \<le> k \<and> tp = Oc \<up> k @ Bk \<up> l) \<longleftrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 231
(\<exists>i\<le>length tp. 1 \<le> i \<and> (\<forall>j < i. tp ! j = Oc) \<and> (\<forall>j < length tp - i. tp ! (i + j) = Bk))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 232
apply(rule iffI)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 233
apply(erule exE)+
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 234
apply(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 235
apply(rule_tac x="k" in exI)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 236
apply(auto)[1]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 237
apply(simp add: nth_append)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 238
apply(simp add: nth_append)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 239
apply(erule exE)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 240
apply(rule_tac x="i" in exI)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 241
apply(rule_tac x="length tp - i" in exI)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 242
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 243
apply(rule sym)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 244
apply(subst append_eq_conv_conj)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 245
apply(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 246
apply(rule conjI)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 247
apply (smt length_replicate length_take nth_equalityI nth_replicate nth_take)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 248
by (smt length_drop length_replicate nth_drop nth_equalityI nth_replicate)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 249
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 250
lemma right_std:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 251
"(\<exists>k l. 1 \<le> k \<and> tp = Oc \<up> k @ Bk \<up> l) \<longleftrightarrow> right_std (Code_tp tp)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 252
apply(simp only: ww)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 253
apply(simp add: right_std_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 254
apply(simp only: list_encode_inverse)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 255
apply(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 256
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 257
apply(rule_tac x="i" in exI)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 258
apply(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 259
apply(rule conjI)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 260
apply (metis Suc_eq_plus1 Suc_neq_Zero cellnum.cases cellnum.simps(1) leD less_trans linorder_neqE_nat)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 261
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 262
by (metis One_nat_def cellnum.cases cellnum.simps(2) less_diff_conv n_not_Suc_n nat_add_commute)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 263
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 264
lemma left_std:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 265
"(\<exists>k. tp = Bk \<up> k) \<longleftrightarrow> left_std (Code_tp tp)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 266
apply(simp add: left_std_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 267
apply(simp only: list_encode_inverse)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 268
apply(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 269
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 270
apply(rule_tac x="length tp" in exI)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 271
apply(induct tp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 272
apply(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 273
apply(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 274
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 275
apply(case_tac a)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 276
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 277
apply(case_tac a)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 278
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 279
by (metis Suc_less_eq nth_Cons_Suc)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 280
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 281
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 282
section {* Standard- and Final Configurations, the Universal Function *}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 283
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 284
text {*
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 285
@{text "Std cf"} returns true, if the configuration @{text "cf"}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 286
is a stardard tape.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 287
*}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 288
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 289
fun Std :: "nat \<Rightarrow> bool"
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 290
where
260
1e45b5b6482a
added definitions and proofs for right-std and left-std tapes
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 291
"Std cf = (left_std (Left cf) \<and> right_std (Right cf))"
246
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
text{*
266
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 294
@{text "Stop m cf k"} means that afer @{text k} steps of
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 295
execution the TM coded by @{text m} and started in configuration
266
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 296
@{text cf} is in a stardard final configuration. *}
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 297
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 298
fun Final :: "nat \<Rightarrow> bool"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 299
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 300
"Final cf = (State cf = 0)"
250
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 301
261
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 302
fun Stop :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 303
where
261
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 304
"Stop m cf k = (Final (Steps cf m k) \<and> Std (Steps cf m k))"
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 305
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 306
text{*
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 307
@{text "Halt"} is the function calculating the steps a TM needs to
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 308
execute before reaching a stardard final configuration. This recursive
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 309
function is the only one that uses unbounded minimization. So it is the
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 310
only non-primitive recursive function needs to be used in the construction
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 311
of the universal function @{text "UF"}.
258
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 312
*}
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 313
250
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 314
fun Halt :: "nat \<Rightarrow> nat \<Rightarrow> nat"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 315
where
261
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 316
"Halt m cf = (LEAST k. Stop m cf k)"
250
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 317
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 318
fun UF :: "nat \<Rightarrow> nat \<Rightarrow> nat"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 319
where
261
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 320
"UF m cf = Stknum (Right (Steps cf m (Halt m cf))) - 1"
258
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 321
267
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 322
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 323
section {* The UF simulates Turing machines *}
258
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 324
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 325
lemma Update_left_simulate:
267
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 326
shows "Newleft (Code_tp l) (Code_tp r) (actnum a) = Code_tp (fst (update a (l, r)))"
258
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 327
apply(induct a)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 328
apply(simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 329
apply(case_tac l)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 330
apply(simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 331
apply(case_tac r)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 332
apply(simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 333
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 334
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 335
lemma Update_right_simulate:
267
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 336
shows "Newright (Code_tp l) (Code_tp r) (actnum a) = Code_tp (snd (update a (l, r)))"
258
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 337
apply(induct a)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 338
apply(simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 339
apply(case_tac r)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 340
apply(simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 341
apply(case_tac r)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 342
apply(simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 343
apply(case_tac l)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 344
apply(simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 345
apply(case_tac r)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 346
apply(simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 347
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 348
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 349
lemma Fetch_state_simulate:
267
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 350
"tm_wf tp \<Longrightarrow> Newstate (Code_tprog tp) st (cellnum c) = snd (fetch tp st c)"
258
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 351
apply(induct tp st c rule: fetch.induct)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 352
apply(simp_all add: list_encode_inverse split: cell.split)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 353
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 354
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 355
lemma Fetch_action_simulate:
267
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 356
"tm_wf tp \<Longrightarrow> Action (Code_tprog tp) st (cellnum c) = actnum (fst (fetch tp st c))"
258
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 357
apply(induct tp st c rule: fetch.induct)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 358
apply(simp_all add: list_encode_inverse split: cell.split)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 359
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 360
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 361
lemma Read_simulate:
267
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 362
"Read (Code_tp tp) = cellnum (read tp)"
258
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 363
apply(case_tac tp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 364
apply(simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 365
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 366
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 367
lemma misc:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 368
"2 < (3::nat)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 369
"1 < (3::nat)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 370
"0 < (3::nat)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 371
"length [x] = 1"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 372
"length [x, y] = 2"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 373
"length [x, y , z] = 3"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 374
"[x, y, z] ! 0 = x"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 375
"[x, y, z] ! 1 = y"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 376
"[x, y, z] ! 2 = z"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 377
apply(simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 378
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 379
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 380
lemma Step_simulate:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 381
assumes "tm_wf tp"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 382
shows "Step (Conf (Code_conf (st, l, r))) (Code_tprog tp) = Conf (Code_conf (step (st, l, r) tp))"
258
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 383
apply(subst step.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 384
apply(simp only: Let_def)
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 385
apply(subst Step.simps)
258
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 386
apply(simp only: Conf.simps Code_conf.simps Right.simps Left.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 387
apply(simp only: list_encode_inverse)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 388
apply(simp only: misc if_True Code_tp.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 389
apply(simp only: prod_case_beta)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 390
apply(subst Fetch_state_simulate[OF assms, symmetric])
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 391
apply(simp only: State.simps)
258
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 392
apply(simp only: list_encode_inverse)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 393
apply(simp only: misc if_True)
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 394
apply(simp only: Read_simulate[simplified Code_tp.simps])
258
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 395
apply(simp only: Fetch_action_simulate[OF assms])
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 396
apply(simp only: Update_left_simulate[simplified Code_tp.simps])
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 397
apply(simp only: Update_right_simulate[simplified Code_tp.simps])
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 398
apply(case_tac "update (fst (fetch tp st (read r))) (l, r)")
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 399
apply(simp only: Code_conf.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 400
apply(simp only: Conf.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 401
apply(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 402
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 403
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 404
lemma Steps_simulate:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 405
assumes "tm_wf tp"
258
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 406
shows "Steps (Conf (Code_conf cf)) (Code_tprog tp) n = Conf (Code_conf (steps cf tp n))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 407
apply(induct n arbitrary: cf)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 408
apply(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 409
apply(simp only: Steps.simps steps.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 410
apply(case_tac cf)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 411
apply(simp only: )
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 412
apply(subst Step_simulate)
258
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 413
apply(rule assms)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 414
apply(drule_tac x="step (a, b, c) tp" in meta_spec)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 415
apply(simp)
250
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 416
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 417
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 418
lemma Final_simulate:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 419
"Final (Conf (Code_conf cf)) = is_final cf"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 420
by (case_tac cf) (simp)
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 421
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 422
lemma Std_simulate:
261
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 423
"Std (Conf (Code_conf cf)) = std_tape cf"
259
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 424
apply(case_tac cf)
260
1e45b5b6482a
added definitions and proofs for right-std and left-std tapes
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 425
apply(simp only: std_tape_def)
1e45b5b6482a
added definitions and proofs for right-std and left-std tapes
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 426
apply(simp only: Code_conf.simps)
1e45b5b6482a
added definitions and proofs for right-std and left-std tapes
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 427
apply(simp only: Conf.simps)
261
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 428
apply(simp only: Std.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 429
apply(simp only: Left.simps Right.simps)
260
1e45b5b6482a
added definitions and proofs for right-std and left-std tapes
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 430
apply(simp only: list_encode_inverse)
1e45b5b6482a
added definitions and proofs for right-std and left-std tapes
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 431
apply(simp only: misc if_True)
261
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 432
apply(simp only: left_std[symmetric] right_std[symmetric])
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 433
apply(simp)
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 434
by (metis Suc_le_D Suc_neq_Zero append_Cons nat.exhaust not_less_eq_eq replicate_Suc)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 435
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 436
261
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 437
lemma UF_simulate:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 438
assumes "tm_wf tm"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 439
shows "UF (Code_tprog tm) (Conf (Code_conf cf)) =
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 440
Stknum (Right (Conf
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 441
(Code_conf (steps cf tm (LEAST n. is_final (steps cf tm n) \<and> std_tape (steps cf tm n)))))) - 1"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 442
apply(simp only: UF.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 443
apply(subst Steps_simulate[symmetric, OF assms])
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 444
apply(subst Final_simulate[symmetric])
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 445
apply(subst Std_simulate[symmetric])
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 446
apply(simp only: Halt.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 447
apply(simp only: Steps_simulate[symmetric, OF assms])
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 448
apply(simp only: Stop.simps[symmetric])
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 449
done
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 450
250
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 451
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 452
section {* Universal Function as Recursive Functions *}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 453
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 454
definition
262
5704925ad138
started with the definitions of the recursive functions for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 455
"rec_read = CN rec_ldec [Id 1 0, constn 0]"
250
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 456
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 457
definition
269
fa40fd8abb54
implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 458
"rec_write = CN rec_penc [CN S [Id 2 0], CN rec_pdec2 [Id 2 1]]"
262
5704925ad138
started with the definitions of the recursive functions for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 459
250
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 460
definition
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 461
"rec_newleft =
263
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 462
(let cond0 = CN rec_eq [Id 3 2, constn 0] in
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 463
let cond1 = CN rec_eq [Id 3 2, constn 1] in
250
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 464
let cond2 = CN rec_eq [Id 3 2, constn 2] in
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 465
let cond3 = CN rec_eq [Id 3 2, constn 3] in
263
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 466
let case3 = CN rec_penc [CN S [CN rec_read [Id 3 1]], Id 3 0] in
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 467
CN rec_if [cond0, Id 3 0,
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 468
CN rec_if [cond1, Id 3 0,
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 469
CN rec_if [cond2, CN rec_pdec2 [Id 3 0],
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 470
CN rec_if [cond3, case3, Id 3 0]]]])"
250
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 471
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 472
definition
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 473
"rec_newright =
263
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 474
(let cond0 = CN rec_eq [Id 3 2, constn 0] in
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 475
let cond1 = CN rec_eq [Id 3 2, constn 1] in
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 476
let cond2 = CN rec_eq [Id 3 2, constn 2] in
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 477
let cond3 = CN rec_eq [Id 3 2, constn 3] in
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 478
let case2 = CN rec_penc [CN S [CN rec_read [Id 3 0]], Id 3 1] in
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 479
CN rec_if [cond0, CN rec_write [constn 0, Id 3 1],
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 480
CN rec_if [cond1, CN rec_write [constn 1, Id 3 1],
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 481
CN rec_if [cond2, case2,
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 482
CN rec_if [cond3, CN rec_pdec2 [Id 3 1], Id 3 1]]]])"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 483
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 484
definition
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 485
"rec_actn = rec_swap (PR (CN rec_pdec1 [CN rec_pdec1 [Id 1 0]])
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 486
(CN rec_pdec1 [CN rec_pdec2 [Id 3 2]]))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 487
250
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 488
definition
263
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 489
"rec_action = (let cond1 = CN rec_noteq [Id 3 1, Z] in
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 490
let cond2 = CN rec_within [Id 3 0, CN rec_pred [Id 3 1]] in
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 491
let if_branch = CN rec_actn [CN rec_ldec [Id 3 0, CN rec_pred [Id 3 1]], Id 3 2]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 492
in CN rec_if [CN rec_conj [cond1, cond2], if_branch, constn 4])"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 493
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 494
definition
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 495
"rec_newstat = rec_swap (PR (CN rec_pdec2 [CN rec_pdec1 [Id 1 0]])
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 496
(CN rec_pdec2 [CN rec_pdec2 [Id 3 2]]))"
250
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 497
263
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 498
definition
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 499
"rec_newstate = (let cond = CN rec_noteq [Id 3 1, Z] in
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 500
let if_branch = CN rec_newstat [CN rec_ldec [Id 3 0, CN rec_pred [Id 3 1]], Id 3 2]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 501
in CN rec_if [cond, if_branch, Z])"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 502
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 503
definition
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 504
"rec_conf = rec_lenc [Id 3 0, Id 3 1, Id 3 2]"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 505
250
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 506
definition
263
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 507
"rec_state = CN rec_ldec [Id 1 0, Z]"
250
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 508
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 509
definition
263
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 510
"rec_left = CN rec_ldec [Id 1 0, constn 1]"
250
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 511
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 512
definition
263
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 513
"rec_right = CN rec_ldec [Id 1 0, constn 2]"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 514
265
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 515
definition
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 516
"rec_step = (let left = CN rec_left [Id 2 0] in
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 517
let right = CN rec_right [Id 2 0] in
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 518
let state = CN rec_state [Id 2 0] in
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 519
let read = CN rec_read [right] in
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 520
let action = CN rec_action [Id 2 1, state, read] in
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 521
let newstate = CN rec_newstate [Id 2 1, state, read] in
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 522
let newleft = CN rec_newleft [left, right, action] in
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 523
let newright = CN rec_newright [left, right, action]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 524
in CN rec_conf [newstate, newleft, newright])"
250
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 525
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 526
definition
269
fa40fd8abb54
implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 527
"rec_steps = PR (Id 2 0) (CN rec_step [Id 4 1, Id 4 3])"
250
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 528
265
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 529
definition
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 530
"rec_stknum = CN rec_minus
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 531
[CN (rec_sigma1 (CN rec_ldec [Id 2 1, Id 2 0])) [CN rec_enclen [Id 1 0], Id 1 0],
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 532
CN rec_ldec [Id 1 0, CN rec_enclen [Id 1 0]]]"
250
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 533
265
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 534
definition
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 535
"rec_right_std = (let bound = CN rec_enclen [Id 1 0] in
269
fa40fd8abb54
implemented new UF in scala; made some small adjustments to the definitions in the theory
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 536
let cond1 = CN rec_le [CN (constn 1) [Id 2 0], Id 2 0] in
265
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 537
let cond2 = rec_all1_less (CN rec_eq [CN rec_ldec [Id 2 1, Id 2 0], constn 1]) in
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 538
let bound2 = CN rec_minus [CN rec_enclen [Id 2 1], Id 2 0] in
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 539
let cond3 = CN (rec_all2_less
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 540
(CN rec_eq [CN rec_ldec [Id 3 2, CN rec_add [Id 3 1, Id 3 0]], Z]))
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 541
[bound2, Id 2 0, Id 2 1] in
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 542
CN (rec_ex1 (CN rec_conj [CN rec_conj [cond1, cond2], cond3])) [bound, Id 1 0])"
250
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 543
265
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 544
definition
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 545
"rec_left_std = (let cond = CN rec_eq [CN rec_ldec [Id 2 1, Id 2 0], Z]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 546
in CN (rec_all1_less cond) [CN rec_enclen [Id 1 0], Id 1 0])"
250
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 547
265
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 548
definition
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 549
"rec_std = CN rec_conj [CN rec_left_std [CN rec_left [Id 1 0]],
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 550
CN rec_right_std [CN rec_right [Id 1 0]]]"
250
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 551
265
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 552
definition
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 553
"rec_final = CN rec_eq [CN rec_state [Id 1 0], Z]"
250
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 554
265
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 555
definition
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 556
"rec_stop = (let steps = CN rec_steps [Id 3 2, Id 3 1, Id 3 0] in
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 557
CN rec_conj [CN rec_final [steps], CN rec_std [steps]])"
250
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 558
267
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 559
definition
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 560
"rec_halt = MN (CN rec_not [CN rec_stop [Id 3 1, Id 3 2, Id 3 0]])"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 561
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 562
definition
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 563
"rec_uf = CN rec_pred
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 564
[CN rec_stknum
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 565
[CN rec_right
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 566
[CN rec_steps [CN rec_halt [Id 2 0, Id 2 1], Id 2 1, Id 2 0]]]]"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 567
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 568
lemma read_lemma [simp]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 569
"rec_eval rec_read [x] = Read x"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 570
by (simp add: rec_read_def)
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 write_lemma [simp]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 573
"rec_eval rec_write [x, y] = Write x y"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 574
by (simp add: rec_write_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 575
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 576
lemma newleft_lemma [simp]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 577
"rec_eval rec_newleft [p, r, a] = Newleft p r a"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 578
by (simp add: rec_newleft_def Let_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 579
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 580
lemma newright_lemma [simp]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 581
"rec_eval rec_newright [p, r, a] = Newright p r a"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 582
by (simp add: rec_newright_def Let_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 583
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 584
lemma act_lemma [simp]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 585
"rec_eval rec_actn [n, c] = Actn n c"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 586
apply(simp add: rec_actn_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 587
apply(case_tac c)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 588
apply(simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 589
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 590
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 591
lemma action_lemma [simp]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 592
"rec_eval rec_action [m, q, c] = Action m q c"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 593
by (simp add: rec_action_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 594
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 595
lemma newstat_lemma [simp]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 596
"rec_eval rec_newstat [n, c] = Newstat n c"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 597
apply(simp add: rec_newstat_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 598
apply(case_tac c)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 599
apply(simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 600
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 601
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 602
lemma newstate_lemma [simp]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 603
"rec_eval rec_newstate [m, q, r] = Newstate m q r"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 604
by (simp add: rec_newstate_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 605
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 606
lemma conf_lemma [simp]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 607
"rec_eval rec_conf [q, l, r] = Conf (q, l, r)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 608
by(simp add: rec_conf_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 609
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 610
lemma state_lemma [simp]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 611
"rec_eval rec_state [cf] = State cf"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 612
by (simp add: rec_state_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 613
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 614
lemma left_lemma [simp]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 615
"rec_eval rec_left [cf] = Left cf"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 616
by (simp add: rec_left_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 617
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 618
lemma right_lemma [simp]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 619
"rec_eval rec_right [cf] = Right cf"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 620
by (simp add: rec_right_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 621
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 622
lemma step_lemma [simp]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 623
"rec_eval rec_step [cf, m] = Step cf m"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 624
by (simp add: Let_def rec_step_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 625
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 626
lemma steps_lemma [simp]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 627
"rec_eval rec_steps [n, cf, p] = Steps cf p n"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 628
by (induct n) (simp_all add: rec_steps_def Step_Steps_comm del: Step.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 629
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 630
lemma stknum_lemma [simp]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 631
"rec_eval rec_stknum [z] = Stknum z"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 632
by (simp add: rec_stknum_def Stknum_def lessThan_Suc_atMost[symmetric])
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 633
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 634
lemma left_std_lemma [simp]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 635
"rec_eval rec_left_std [z] = (if left_std z then 1 else 0)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 636
by (simp add: Let_def rec_left_std_def left_std_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 637
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 638
lemma right_std_lemma [simp]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 639
"rec_eval rec_right_std [z] = (if right_std z then 1 else 0)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 640
by (simp add: Let_def rec_right_std_def right_std_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 641
265
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 642
lemma std_lemma [simp]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 643
"rec_eval rec_std [cf] = (if Std cf then 1 else 0)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 644
by (simp add: rec_std_def)
250
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 645
265
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 646
lemma final_lemma [simp]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 647
"rec_eval rec_final [cf] = (if Final cf then 1 else 0)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 648
by (simp add: rec_final_def)
250
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 649
265
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 650
lemma stop_lemma [simp]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 651
"rec_eval rec_stop [m, cf, k] = (if Stop m cf k then 1 else 0)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 652
by (simp add: Let_def rec_stop_def)
250
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 653
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 654
lemma halt_lemma [simp]:
265
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 655
"rec_eval rec_halt [m, cf] = Halt m cf"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 656
by (simp add: rec_halt_def del: Stop.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 657
250
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 658
lemma uf_lemma [simp]:
265
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 659
"rec_eval rec_uf [m, cf] = UF m cf"
250
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 660
by (simp add: rec_uf_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 661
284
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 662
(* value "size rec_uf" *)
248
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 663
end
246
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 664