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