229
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1
theory Abacus_Hoare
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 2
imports Abacus
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 3
begin
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 4
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 5
type_synonym abc_assert = "nat list \<Rightarrow> bool"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 7
definition
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 8
assert_imp :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" ("_ \<mapsto> _" [0, 0] 100)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 9
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 10
"assert_imp P Q \<equiv> \<forall>xs. P xs \<longrightarrow> Q xs"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 11
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 12
fun abc_holds_for :: "(nat list \<Rightarrow> bool) \<Rightarrow> (nat \<times> nat list) \<Rightarrow> bool" ("_ abc'_holds'_for _" [100, 99] 100)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 13
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 14
"P abc_holds_for (s, lm) = P lm"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 15
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 16
(* Hoare Rules *)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 17
(* halting case *)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 18
(*consts abc_Hoare_halt :: "abc_assert \<Rightarrow> abc_prog \<Rightarrow> abc_assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" 50)*)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 19
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 20
fun abc_final :: "(nat \<times> nat list) \<Rightarrow> abc_prog \<Rightarrow> bool"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 21
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 22
"abc_final (s, lm) p = (s = length p)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 23
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 24
fun abc_notfinal :: "abc_conf \<Rightarrow> abc_prog \<Rightarrow> bool"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 25
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 26
"abc_notfinal (s, lm) p = (s < length p)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 27
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 28
definition
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 29
abc_Hoare_halt :: "abc_assert \<Rightarrow> abc_prog \<Rightarrow> abc_assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" 50)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 30
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 31
"abc_Hoare_halt P p Q \<equiv> \<forall>lm. P lm \<longrightarrow> (\<exists>n. abc_final (abc_steps_l (0, lm) p n) p \<and> Q abc_holds_for (abc_steps_l (0, lm) p n))"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 32
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 33
lemma abc_Hoare_haltI:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 34
assumes "\<And>lm. P lm \<Longrightarrow> \<exists>n. abc_final (abc_steps_l (0, lm) p n) p \<and> Q abc_holds_for (abc_steps_l (0, lm) p n)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 35
shows "{P} (p::abc_prog) {Q}"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 36
unfolding abc_Hoare_halt_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 37
using assms by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 38
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 39
text {*
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 40
{P} A {Q} {Q} B {S}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 41
-----------------------------------------
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 42
{P} A [+] B {S}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 43
*}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 44
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 45
definition
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 46
abc_Hoare_unhalt :: "abc_assert \<Rightarrow> abc_prog \<Rightarrow> bool" ("({(1_)}/ (_)) \<up>" 50)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 47
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 48
"abc_Hoare_unhalt P p \<equiv> \<forall>args. P args \<longrightarrow> (\<forall> n .abc_notfinal (abc_steps_l (0, args) p n) p)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 49
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 50
lemma abc_Hoare_unhaltI:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 51
assumes "\<And>args n. P args \<Longrightarrow> abc_notfinal (abc_steps_l (0, args) p n) p"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 52
shows "{P} (p::abc_prog) \<up>"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 53
unfolding abc_Hoare_unhalt_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 54
using assms by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 55
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 56
fun abc_inst_shift :: "abc_inst \<Rightarrow> nat \<Rightarrow> abc_inst"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 57
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 58
"abc_inst_shift (Inc m) n = Inc m" |
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 59
"abc_inst_shift (Dec m e) n = Dec m (e + n)" |
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 60
"abc_inst_shift (Goto m) n = Goto (m + n)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 61
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 62
fun abc_shift :: "abc_inst list \<Rightarrow> nat \<Rightarrow> abc_inst list"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 63
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 64
"abc_shift xs n = map (\<lambda> x. abc_inst_shift x n) xs"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 65
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 66
fun abc_comp :: "abc_inst list \<Rightarrow> abc_inst list \<Rightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 67
abc_inst list" (infixl "[+]" 99)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 68
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 69
"abc_comp al bl = (let al_len = length al in
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 70
al @ abc_shift bl al_len)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 71
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 72
lemma abc_comp_first_step_eq_pre:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 73
"s < length A
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 74
\<Longrightarrow> abc_step_l (s, lm) (abc_fetch s (A [+] B)) =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 75
abc_step_l (s, lm) (abc_fetch s A)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 76
by(simp add: abc_step_l.simps abc_fetch.simps nth_append)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 77
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 78
lemma abc_before_final:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 79
"\<lbrakk>abc_final (abc_steps_l (0, lm) p n) p; p \<noteq> []\<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 80
\<Longrightarrow> \<exists> n'. abc_notfinal (abc_steps_l (0, lm) p n') p \<and>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 81
abc_final (abc_steps_l (0, lm) p (Suc n')) p"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 82
proof(induct n)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 83
case 0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 84
thus "?thesis"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 85
by(simp add: abc_steps_l.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 86
next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 87
case (Suc n)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 88
have ind: " \<lbrakk>abc_final (abc_steps_l (0, lm) p n) p; p \<noteq> []\<rbrakk> \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 89
\<exists>n'. abc_notfinal (abc_steps_l (0, lm) p n') p \<and> abc_final (abc_steps_l (0, lm) p (Suc n')) p"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 90
by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 91
have final: "abc_final (abc_steps_l (0, lm) p (Suc n)) p" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 92
have notnull: "p \<noteq> []" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 93
show "?thesis"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 94
proof(cases "abc_final (abc_steps_l (0, lm) p n) p")
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 95
case True
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 96
have "abc_final (abc_steps_l (0, lm) p n) p" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 97
then have "\<exists>n'. abc_notfinal (abc_steps_l (0, lm) p n') p \<and> abc_final (abc_steps_l (0, lm) p (Suc n')) p"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 98
using ind notnull
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 99
by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 100
thus "?thesis"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 101
by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 102
next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 103
case False
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 104
have "\<not> abc_final (abc_steps_l (0, lm) p n) p" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 105
from final this have "abc_notfinal (abc_steps_l (0, lm) p n) p"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 106
by(case_tac "abc_steps_l (0, lm) p n", simp add: abc_step_red2
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 107
abc_step_l.simps abc_fetch.simps split: if_splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 108
thus "?thesis"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 109
using final
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 110
by(rule_tac x = n in exI, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 111
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 112
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 113
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 114
lemma notfinal_Suc:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 115
"abc_notfinal (abc_steps_l (0, lm) A (Suc n)) A \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 116
abc_notfinal (abc_steps_l (0, lm) A n) A"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 117
apply(case_tac "abc_steps_l (0, lm) A n")
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 118
apply(simp add: abc_step_red2 abc_fetch.simps abc_step_l.simps split: if_splits)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 119
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 120
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 121
lemma abc_comp_frist_steps_eq_pre:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 122
assumes notfinal: "abc_notfinal (abc_steps_l (0, lm) A n) A"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 123
and notnull: "A \<noteq> []"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 124
shows "abc_steps_l (0, lm) (A [+] B) n = abc_steps_l (0, lm) A n"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 125
using notfinal
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 126
proof(induct n)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 127
case 0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 128
thus "?case"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 129
by(simp add: abc_steps_l.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 130
next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 131
case (Suc n)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 132
have ind: "abc_notfinal (abc_steps_l (0, lm) A n) A \<Longrightarrow> abc_steps_l (0, lm) (A [+] B) n = abc_steps_l (0, lm) A n"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 133
by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 134
have h: "abc_notfinal (abc_steps_l (0, lm) A (Suc n)) A" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 135
then have a: "abc_notfinal (abc_steps_l (0, lm) A n) A"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 136
by(simp add: notfinal_Suc)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 137
then have b: "abc_steps_l (0, lm) (A [+] B) n = abc_steps_l (0, lm) A n"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 138
using ind by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 139
obtain s lm' where c: "abc_steps_l (0, lm) A n = (s, lm')"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 140
by (metis prod.exhaust)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 141
then have d: "s < length A \<and> abc_steps_l (0, lm) (A [+] B) n = (s, lm')"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 142
using a b by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 143
thus "?case"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 144
using c
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 145
by(simp add: abc_step_red2 abc_fetch.simps abc_step_l.simps nth_append)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 146
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 147
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 148
declare abc_shift.simps[simp del] abc_comp.simps[simp del]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 149
lemma halt_steps2: "st \<ge> length A \<Longrightarrow> abc_steps_l (st, lm) A stp = (st, lm)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 150
apply(induct stp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 151
by(simp_all add: abc_step_red2 abc_steps_l.simps abc_step_l.simps abc_fetch.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 152
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 153
lemma halt_steps: "abc_steps_l (length A, lm) A n = (length A, lm)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 154
apply(induct n, simp add: abc_steps_l.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 155
apply(simp add: abc_step_red2 abc_step_l.simps nth_append abc_fetch.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 156
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 157
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 158
lemma abc_steps_add:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 159
"abc_steps_l (as, lm) ap (m + n) =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 160
abc_steps_l (abc_steps_l (as, lm) ap m) ap n"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 161
apply(induct m arbitrary: n as lm, simp add: abc_steps_l.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 162
proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 163
fix m n as lm
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 164
assume ind:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 165
"\<And>n as lm. abc_steps_l (as, lm) ap (m + n) =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 166
abc_steps_l (abc_steps_l (as, lm) ap m) ap n"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 167
show "abc_steps_l (as, lm) ap (Suc m + n) =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 168
abc_steps_l (abc_steps_l (as, lm) ap (Suc m)) ap n"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 169
apply(insert ind[of as lm "Suc n"], simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 170
apply(insert ind[of as lm "Suc 0"], simp add: abc_steps_l.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 171
apply(case_tac "(abc_steps_l (as, lm) ap m)", simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 172
apply(simp add: abc_steps_l.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 173
apply(case_tac "abc_step_l (a, b) (abc_fetch a ap)",
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 174
simp add: abc_steps_l.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 175
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 176
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 177
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 178
lemma equal_when_halt:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 179
assumes exc1: "abc_steps_l (s, lm) A na = (length A, lma)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 180
and exc2: "abc_steps_l (s, lm) A nb = (length A, lmb)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 181
shows "lma = lmb"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 182
proof(cases "na > nb")
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 183
case True
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 184
then obtain d where "na = nb + d"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 185
by (metis add_Suc_right less_iff_Suc_add)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 186
thus "?thesis" using assms halt_steps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 187
by(simp add: abc_steps_add)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 188
next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 189
case False
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 190
then obtain d where "nb = na + d"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 191
by (metis add.comm_neutral less_imp_add_positive nat_neq_iff)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 192
thus "?thesis" using assms halt_steps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 193
by(simp add: abc_steps_add)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 194
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 195
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 196
lemma abc_comp_frist_steps_halt_eq':
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 197
assumes final: "abc_steps_l (0, lm) A n = (length A, lm')"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 198
and notnull: "A \<noteq> []"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 199
shows "\<exists> n'. abc_steps_l (0, lm) (A [+] B) n' = (length A, lm')"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 200
proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 201
have "\<exists> n'. abc_notfinal (abc_steps_l (0, lm) A n') A \<and>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 202
abc_final (abc_steps_l (0, lm) A (Suc n')) A"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 203
using assms
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 204
by(rule_tac n = n in abc_before_final, simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 205
then obtain na where a:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 206
"abc_notfinal (abc_steps_l (0, lm) A na) A \<and>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 207
abc_final (abc_steps_l (0, lm) A (Suc na)) A" ..
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 208
obtain sa lma where b: "abc_steps_l (0, lm) A na = (sa, lma)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 209
by (metis prod.exhaust)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 210
then have c: "abc_steps_l (0, lm) (A [+] B) na = (sa, lma)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 211
using a abc_comp_frist_steps_eq_pre[of lm A na B] assms
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 212
by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 213
have d: "sa < length A" using b a by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 214
then have e: "abc_step_l (sa, lma) (abc_fetch sa (A [+] B)) =
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 215
abc_step_l (sa, lma) (abc_fetch sa A)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 216
by(rule_tac abc_comp_first_step_eq_pre)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 217
from a have "abc_steps_l (0, lm) A (Suc na) = (length A, lm')"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 218
using final equal_when_halt
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 219
by(case_tac "abc_steps_l (0, lm) A (Suc na)" , simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 220
then have "abc_steps_l (0, lm) (A [+] B) (Suc na) = (length A, lm')"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 221
using a b c e
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 222
by(simp add: abc_step_red2)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 223
thus "?thesis"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 224
by blast
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 225
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 226
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 227
lemma abc_exec_null: "abc_steps_l sam [] n = sam"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 228
apply(cases sam)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 229
apply(induct n)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 230
apply(auto simp: abc_step_red2)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 231
apply(auto simp: abc_step_l.simps abc_steps_l.simps abc_fetch.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 232
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 233
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 234
lemma abc_comp_frist_steps_halt_eq:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 235
assumes final: "abc_steps_l (0, lm) A n = (length A, lm')"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 236
shows "\<exists> n'. abc_steps_l (0, lm) (A [+] B) n' = (length A, lm')"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 237
using final
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 238
apply(case_tac "A = []")
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 239
apply(rule_tac x = 0 in exI, simp add: abc_steps_l.simps abc_exec_null)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 240
apply(rule_tac abc_comp_frist_steps_halt_eq', simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 241
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 242
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 243
lemma abc_comp_second_step_eq:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 244
assumes exec: "abc_step_l (s, lm) (abc_fetch s B) = (sa, lma)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 245
shows "abc_step_l (s + length A, lm) (abc_fetch (s + length A) (A [+] B))
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 246
= (sa + length A, lma)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 247
using assms
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 248
apply(auto simp: abc_step_l.simps abc_fetch.simps nth_append abc_comp.simps abc_shift.simps split : if_splits )
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 249
apply(case_tac [!] "B ! s", auto simp: Let_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 250
done
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 abc_comp_second_steps_eq:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 253
assumes exec: "abc_steps_l (0, lm) B n = (sa, lm')"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 254
shows "abc_steps_l (length A, lm) (A [+] B) n = (sa + length A, lm')"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 255
using assms
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 256
proof(induct n arbitrary: sa lm')
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 257
case 0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 258
thus "?case"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 259
by(simp add: abc_steps_l.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 260
next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 261
case (Suc n)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 262
have ind: "\<And>sa lm'. abc_steps_l (0, lm) B n = (sa, lm') \<Longrightarrow>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 263
abc_steps_l (length A, lm) (A [+] B) n = (sa + length A, lm')" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 264
have exec: "abc_steps_l (0, lm) B (Suc n) = (sa, lm')" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 265
obtain sb lmb where a: " abc_steps_l (0, lm) B n = (sb, lmb)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 266
by (metis prod.exhaust)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 267
then have "abc_steps_l (length A, lm) (A [+] B) n = (sb + length A, lmb)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 268
using ind by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 269
moreover have "abc_step_l (sb + length A, lmb) (abc_fetch (sb + length A) (A [+] B)) = (sa + length A, lm') "
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 270
using a exec abc_comp_second_step_eq
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 271
by(simp add: abc_step_red2)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 272
ultimately show "?case"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 273
by(simp add: abc_step_red2)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 274
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 275
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 276
lemma length_abc_comp[simp, intro]:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 277
"length (A [+] B) = length A + length B"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 278
by(auto simp: abc_comp.simps abc_shift.simps)
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 abc_Hoare_plus_halt :
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 281
assumes A_halt : "{P} (A::abc_prog) {Q}"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 282
and B_halt : "{Q} (B::abc_prog) {S}"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 283
shows "{P} (A [+] B) {S}"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 284
proof(rule_tac abc_Hoare_haltI)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 285
fix lm
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 286
assume a: "P lm"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 287
then obtain na lma where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 288
"abc_final (abc_steps_l (0, lm) A na) A"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 289
and b: "abc_steps_l (0, lm) A na = (length A, lma)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 290
and c: "Q abc_holds_for (length A, lma)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 291
using A_halt unfolding abc_Hoare_halt_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 292
by (metis (full_types) abc_final.simps abc_holds_for.simps prod.exhaust)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 293
have "\<exists> n. abc_steps_l (0, lm) (A [+] B) n = (length A, lma)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 294
using abc_comp_frist_steps_halt_eq b
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 295
by(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 296
then obtain nx where h1: "abc_steps_l (0, lm) (A [+] B) nx = (length A, lma)" ..
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 297
from c have "Q lma"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 298
using c unfolding abc_holds_for.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 299
by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 300
then obtain nb lmb where
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 301
"abc_final (abc_steps_l (0, lma) B nb) B"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 302
and d: "abc_steps_l (0, lma) B nb = (length B, lmb)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 303
and e: "S abc_holds_for (length B, lmb)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 304
using B_halt unfolding abc_Hoare_halt_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 305
by (metis (full_types) abc_final.simps abc_holds_for.simps prod.exhaust)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 306
have h2: "abc_steps_l (length A, lma) (A [+] B) nb = (length B + length A, lmb)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 307
using d abc_comp_second_steps_eq
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 308
by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 309
thus "\<exists>n. abc_final (abc_steps_l (0, lm) (A [+] B) n) (A [+] B) \<and>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 310
S abc_holds_for abc_steps_l (0, lm) (A [+] B) n"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 311
using h1 e
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 312
by(rule_tac x = "nx + nb" in exI, simp add: abc_steps_add)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 313
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 314
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 315
lemma abc_unhalt_append_eq:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 316
assumes unhalt: "{P} (A::abc_prog) \<up>"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 317
and P: "P args"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 318
shows "abc_steps_l (0, args) (A [+] B) stp = abc_steps_l (0, args) A stp"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 319
proof(induct stp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 320
case 0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 321
thus "?case"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 322
by(simp add: abc_steps_l.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 323
next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 324
case (Suc stp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 325
have ind: "abc_steps_l (0, args) (A [+] B) stp = abc_steps_l (0, args) A stp"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 326
by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 327
obtain s nl where a: "abc_steps_l (0, args) A stp = (s, nl)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 328
by (metis prod.exhaust)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 329
then have b: "s < length A"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 330
using unhalt P
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 331
apply(auto simp: abc_Hoare_unhalt_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 332
by (metis abc_notfinal.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 333
thus "?case"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 334
using a ind
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 335
by(simp add: abc_step_red2 abc_step_l.simps abc_fetch.simps nth_append abc_comp.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 336
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 337
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 338
lemma abc_Hoare_plus_unhalt1:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 339
"{P} (A::abc_prog) \<up> \<Longrightarrow> {P} (A [+] B) \<up>"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 340
apply(rule_tac abc_Hoare_unhaltI)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 341
apply(frule_tac args = args and B = B and stp = n in abc_unhalt_append_eq)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 342
apply(simp_all add: abc_Hoare_unhalt_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 343
apply(erule_tac x = args in allE, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 344
apply(erule_tac x = n in allE)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 345
apply(case_tac "(abc_steps_l (0, args) A n)", simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 346
done
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
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 349
lemma notfinal_all_before:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 350
"\<lbrakk>abc_notfinal (abc_steps_l (0, args) A x) A; y\<le>x \<rbrakk>
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 351
\<Longrightarrow> abc_notfinal (abc_steps_l (0, args) A y) A "
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 352
apply(subgoal_tac "\<exists> d. x = y + d", auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 353
apply(case_tac "abc_steps_l (0, args) A y",simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 354
apply(rule_tac classical, simp add: abc_steps_add leI halt_steps2)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 355
by arith
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 356
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 357
lemma abc_Hoare_plus_unhalt2':
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 358
assumes unhalt: "{Q} (B::abc_prog) \<up>"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 359
and halt: "{P} (A::abc_prog) {Q}"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 360
and notnull: "A \<noteq> []"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 361
and P: "P args"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 362
shows "abc_notfinal (abc_steps_l (0, args) (A [+] B) n) (A [+] B)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 363
proof -
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 364
obtain st nl stp where a: "abc_final (abc_steps_l (0, args) A stp) A"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 365
and b: "Q abc_holds_for (length A, nl)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 366
and c: "abc_steps_l (0, args) A stp = (st, nl)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 367
using halt P unfolding abc_Hoare_halt_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 368
by (metis abc_holds_for.simps prod.exhaust)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 369
thm abc_before_final
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 370
obtain stpa where d:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 371
"abc_notfinal (abc_steps_l (0, args) A stpa) A \<and> abc_final (abc_steps_l (0, args) A (Suc stpa)) A"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 372
using a notnull abc_before_final[of args A stp]
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 373
by(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 374
thus "?thesis"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 375
proof(cases "n < Suc stpa")
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 376
case True
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 377
have h: "n < Suc stpa" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 378
then have "abc_notfinal (abc_steps_l (0, args) A n) A"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 379
using d
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 380
by(rule_tac notfinal_all_before, auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 381
moreover then have "abc_steps_l (0, args) (A [+] B) n = abc_steps_l (0, args) A n"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 382
using notnull
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 383
by(rule_tac abc_comp_frist_steps_eq_pre, simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 384
ultimately show "?thesis"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 385
by(case_tac "abc_steps_l (0, args) A n", simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 386
next
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 387
case False
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 388
have "\<not> n < Suc stpa" by fact
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 389
then obtain d where i1: "n = Suc stpa + d"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 390
by (metis add_Suc less_iff_Suc_add not_less_eq)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 391
have "abc_steps_l (0, args) A (Suc stpa) = (length A, nl)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 392
using d a c
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 393
apply(case_tac "abc_steps_l (0, args) A stp", simp add: equal_when_halt)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 394
by(case_tac "abc_steps_l (0, args) A (Suc stpa)", simp add: equal_when_halt)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 395
moreover have "abc_steps_l (0, args) (A [+] B) stpa = abc_steps_l (0, args) A stpa"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 396
using notnull d
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 397
by(rule_tac abc_comp_frist_steps_eq_pre, simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 398
ultimately have i2: "abc_steps_l (0, args) (A [+] B) (Suc stpa) = (length A, nl)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 399
using d
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 400
apply(case_tac "abc_steps_l (0, args) A stpa", simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 401
by(simp add: abc_step_red2 abc_steps_l.simps abc_fetch.simps abc_comp.simps nth_append)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 402
obtain s' nl' where i3:"abc_steps_l (0, nl) B d = (s', nl')"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 403
by (metis prod.exhaust)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 404
then have i4: "abc_steps_l (0, args) (A [+] B) (Suc stpa + d) = (length A + s', nl')"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 405
using i2 apply(simp only: abc_steps_add)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 406
using abc_comp_second_steps_eq[of nl B d s' nl']
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 407
by simp
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 408
moreover have "s' < length B"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 409
using unhalt b i3
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 410
apply(simp add: abc_Hoare_unhalt_def)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 411
apply(erule_tac x = nl in allE, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 412
by(erule_tac x = d in allE, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 413
ultimately show "?thesis"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 414
using i1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 415
by(simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 416
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 417
qed
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 418
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 419
lemma abc_comp_null_left[simp]: "[] [+] A = A"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 420
apply(induct A)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 421
apply(case_tac [2] a)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 422
apply(auto simp: abc_comp.simps abc_shift.simps abc_inst_shift.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 423
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 424
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 425
lemma abc_comp_null_right[simp]: "A [+] [] = A"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 426
apply(induct A)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 427
apply(case_tac [2] a)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 428
apply(auto simp: abc_comp.simps abc_shift.simps abc_inst_shift.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 429
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 430
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 431
lemma abc_Hoare_plus_unhalt2:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 432
"\<lbrakk>{Q} (B::abc_prog)\<up>; {P} (A::abc_prog) {Q}\<rbrakk>\<Longrightarrow> {P} (A [+] B) \<up>"
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 433
apply(case_tac "A = []")
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 434
apply(simp add: abc_Hoare_halt_def abc_Hoare_unhalt_def abc_exec_null)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 435
apply(rule_tac abc_Hoare_unhaltI)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 436
apply(erule_tac abc_Hoare_plus_unhalt2', simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 437
apply(simp, simp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 438
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 439
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 440
end
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 441
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 442