(* Title: thys/Abacus_Hoare.thy+ −
Author: Jian Xu, Xingyuan Zhang, and Christian Urban+ −
Modifications: Sebastiaan Joosten+ −
*)+ −
+ −
theory Abacus_Hoare+ −
imports Abacus+ −
begin+ −
+ −
type_synonym abc_assert = "nat list \<Rightarrow> bool"+ −
+ −
definition + −
assert_imp :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" ("_ \<mapsto> _" [0, 0] 100)+ −
where+ −
"assert_imp P Q \<equiv> \<forall>xs. P xs \<longrightarrow> Q xs"+ −
+ −
fun abc_holds_for :: "(nat list \<Rightarrow> bool) \<Rightarrow> (nat \<times> nat list) \<Rightarrow> bool" ("_ abc'_holds'_for _" [100, 99] 100)+ −
where+ −
"P abc_holds_for (s, lm) = P lm" + −
+ −
(* Hoare Rules *)+ −
(* halting case *)+ −
(*consts abc_Hoare_halt :: "abc_assert \<Rightarrow> abc_prog \<Rightarrow> abc_assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" 50)*)+ −
+ −
fun abc_final :: "(nat \<times> nat list) \<Rightarrow> abc_prog \<Rightarrow> bool"+ −
where + −
"abc_final (s, lm) p = (s = length p)"+ −
+ −
fun abc_notfinal :: "abc_conf \<Rightarrow> abc_prog \<Rightarrow> bool"+ −
where+ −
"abc_notfinal (s, lm) p = (s < length p)"+ −
+ −
definition + −
abc_Hoare_halt :: "abc_assert \<Rightarrow> abc_prog \<Rightarrow> abc_assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" 50)+ −
where+ −
"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))"+ −
+ −
lemma abc_Hoare_haltI:+ −
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)"+ −
shows "{P} (p::abc_prog) {Q}"+ −
unfolding abc_Hoare_halt_def + −
using assms by auto+ −
+ −
text {*+ −
{P} A {Q} {Q} B {S} + −
-----------------------------------------+ −
{P} A [+] B {S}+ −
*}+ −
+ −
definition+ −
abc_Hoare_unhalt :: "abc_assert \<Rightarrow> abc_prog \<Rightarrow> bool" ("({(1_)}/ (_)) \<up>" 50)+ −
where+ −
"abc_Hoare_unhalt P p \<equiv> \<forall>args. P args \<longrightarrow> (\<forall> n .abc_notfinal (abc_steps_l (0, args) p n) p)"+ −
+ −
lemma abc_Hoare_unhaltI:+ −
assumes "\<And>args n. P args \<Longrightarrow> abc_notfinal (abc_steps_l (0, args) p n) p"+ −
shows "{P} (p::abc_prog) \<up>"+ −
unfolding abc_Hoare_unhalt_def + −
using assms by auto+ −
+ −
fun abc_inst_shift :: "abc_inst \<Rightarrow> nat \<Rightarrow> abc_inst"+ −
where+ −
"abc_inst_shift (Inc m) n = Inc m" |+ −
"abc_inst_shift (Dec m e) n = Dec m (e + n)" |+ −
"abc_inst_shift (Goto m) n = Goto (m + n)"+ −
+ −
fun abc_shift :: "abc_inst list \<Rightarrow> nat \<Rightarrow> abc_inst list" + −
where+ −
"abc_shift xs n = map (\<lambda> x. abc_inst_shift x n) xs" + −
+ −
fun abc_comp :: "abc_inst list \<Rightarrow> abc_inst list \<Rightarrow> + −
abc_inst list" (infixl "[+]" 99)+ −
where+ −
"abc_comp al bl = (let al_len = length al in + −
al @ abc_shift bl al_len)"+ −
+ −
lemma abc_comp_first_step_eq_pre: + −
"s < length A+ −
\<Longrightarrow> abc_step_l (s, lm) (abc_fetch s (A [+] B)) = + −
abc_step_l (s, lm) (abc_fetch s A)"+ −
by(simp add: abc_step_l.simps abc_fetch.simps nth_append)+ −
+ −
lemma abc_before_final: + −
"\<lbrakk>abc_final (abc_steps_l (0, lm) p n) p; p \<noteq> []\<rbrakk>+ −
\<Longrightarrow> \<exists> n'. abc_notfinal (abc_steps_l (0, lm) p n') p \<and> + −
abc_final (abc_steps_l (0, lm) p (Suc n')) p"+ −
proof(induct n)+ −
case 0+ −
thus "?thesis"+ −
by(simp add: abc_steps_l.simps)+ −
next+ −
case (Suc n)+ −
have ind: " \<lbrakk>abc_final (abc_steps_l (0, lm) p n) p; p \<noteq> []\<rbrakk> \<Longrightarrow> + −
\<exists>n'. abc_notfinal (abc_steps_l (0, lm) p n') p \<and> abc_final (abc_steps_l (0, lm) p (Suc n')) p"+ −
by fact+ −
have final: "abc_final (abc_steps_l (0, lm) p (Suc n)) p" by fact+ −
have notnull: "p \<noteq> []" by fact+ −
show "?thesis"+ −
proof(cases "abc_final (abc_steps_l (0, lm) p n) p")+ −
case True+ −
have "abc_final (abc_steps_l (0, lm) p n) p" by fact+ −
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"+ −
using ind notnull+ −
by simp+ −
thus "?thesis"+ −
by simp+ −
next+ −
case False+ −
have "\<not> abc_final (abc_steps_l (0, lm) p n) p" by fact+ −
from final this have "abc_notfinal (abc_steps_l (0, lm) p n) p" + −
by(case_tac "abc_steps_l (0, lm) p n", simp add: abc_step_red2 + −
abc_step_l.simps abc_fetch.simps split: if_splits)+ −
thus "?thesis"+ −
using final+ −
by(rule_tac x = n in exI, simp)+ −
qed+ −
qed+ −
+ −
lemma notfinal_Suc:+ −
"abc_notfinal (abc_steps_l (0, lm) A (Suc n)) A \<Longrightarrow> + −
abc_notfinal (abc_steps_l (0, lm) A n) A"+ −
apply(case_tac "abc_steps_l (0, lm) A n")+ −
apply(simp add: abc_step_red2 abc_fetch.simps abc_step_l.simps split: if_splits)+ −
done+ −
+ −
lemma abc_comp_frist_steps_eq_pre: + −
assumes notfinal: "abc_notfinal (abc_steps_l (0, lm) A n) A"+ −
and notnull: "A \<noteq> []"+ −
shows "abc_steps_l (0, lm) (A [+] B) n = abc_steps_l (0, lm) A n"+ −
using notfinal+ −
proof(induct n)+ −
case 0+ −
thus "?case"+ −
by(simp add: abc_steps_l.simps)+ −
next+ −
case (Suc n)+ −
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"+ −
by fact+ −
have h: "abc_notfinal (abc_steps_l (0, lm) A (Suc n)) A" by fact+ −
then have a: "abc_notfinal (abc_steps_l (0, lm) A n) A"+ −
by(simp add: notfinal_Suc)+ −
then have b: "abc_steps_l (0, lm) (A [+] B) n = abc_steps_l (0, lm) A n"+ −
using ind by simp+ −
obtain s lm' where c: "abc_steps_l (0, lm) A n = (s, lm')"+ −
by (metis prod.exhaust)+ −
then have d: "s < length A \<and> abc_steps_l (0, lm) (A [+] B) n = (s, lm')" + −
using a b by simp+ −
thus "?case"+ −
using c+ −
by(simp add: abc_step_red2 abc_fetch.simps abc_step_l.simps nth_append)+ −
qed+ −
+ −
declare abc_shift.simps[simp del] abc_comp.simps[simp del]+ −
lemma halt_steps2: "st \<ge> length A \<Longrightarrow> abc_steps_l (st, lm) A stp = (st, lm)"+ −
apply(induct stp)+ −
by(simp_all add: abc_step_red2 abc_steps_l.simps abc_step_l.simps abc_fetch.simps)+ −
+ −
lemma halt_steps: "abc_steps_l (length A, lm) A n = (length A, lm)"+ −
apply(induct n, simp add: abc_steps_l.simps)+ −
apply(simp add: abc_step_red2 abc_step_l.simps nth_append abc_fetch.simps)+ −
done+ −
+ −
lemma abc_steps_add: + −
"abc_steps_l (as, lm) ap (m + n) = + −
abc_steps_l (abc_steps_l (as, lm) ap m) ap n"+ −
apply(induct m arbitrary: n as lm, simp add: abc_steps_l.simps)+ −
proof -+ −
fix m n as lm+ −
assume ind: + −
"\<And>n as lm. abc_steps_l (as, lm) ap (m + n) = + −
abc_steps_l (abc_steps_l (as, lm) ap m) ap n"+ −
show "abc_steps_l (as, lm) ap (Suc m + n) = + −
abc_steps_l (abc_steps_l (as, lm) ap (Suc m)) ap n"+ −
apply(insert ind[of as lm "Suc n"], simp)+ −
apply(insert ind[of as lm "Suc 0"], simp add: abc_steps_l.simps)+ −
apply(case_tac "(abc_steps_l (as, lm) ap m)", simp)+ −
apply(simp add: abc_steps_l.simps)+ −
apply(case_tac "abc_step_l (a, b) (abc_fetch a ap)", + −
simp add: abc_steps_l.simps)+ −
done+ −
qed+ −
+ −
lemma equal_when_halt: + −
assumes exc1: "abc_steps_l (s, lm) A na = (length A, lma)"+ −
and exc2: "abc_steps_l (s, lm) A nb = (length A, lmb)"+ −
shows "lma = lmb"+ −
proof(cases "na > nb")+ −
case True+ −
then obtain d where "na = nb + d"+ −
by (metis add_Suc_right less_iff_Suc_add)+ −
thus "?thesis" using assms halt_steps+ −
by(simp add: abc_steps_add)+ −
next+ −
case False+ −
then obtain d where "nb = na + d"+ −
by (metis add.comm_neutral less_imp_add_positive nat_neq_iff)+ −
thus "?thesis" using assms halt_steps+ −
by(simp add: abc_steps_add)+ −
qed + −
+ −
lemma abc_comp_frist_steps_halt_eq': + −
assumes final: "abc_steps_l (0, lm) A n = (length A, lm')"+ −
and notnull: "A \<noteq> []"+ −
shows "\<exists> n'. abc_steps_l (0, lm) (A [+] B) n' = (length A, lm')"+ −
proof -+ −
have "\<exists> n'. abc_notfinal (abc_steps_l (0, lm) A n') A \<and> + −
abc_final (abc_steps_l (0, lm) A (Suc n')) A"+ −
using assms+ −
by(rule_tac n = n in abc_before_final, simp_all)+ −
then obtain na where a:+ −
"abc_notfinal (abc_steps_l (0, lm) A na) A \<and> + −
abc_final (abc_steps_l (0, lm) A (Suc na)) A" ..+ −
obtain sa lma where b: "abc_steps_l (0, lm) A na = (sa, lma)"+ −
by (metis prod.exhaust)+ −
then have c: "abc_steps_l (0, lm) (A [+] B) na = (sa, lma)"+ −
using a abc_comp_frist_steps_eq_pre[of lm A na B] assms + −
by simp+ −
have d: "sa < length A" using b a by simp+ −
then have e: "abc_step_l (sa, lma) (abc_fetch sa (A [+] B)) = + −
abc_step_l (sa, lma) (abc_fetch sa A)"+ −
by(rule_tac abc_comp_first_step_eq_pre)+ −
from a have "abc_steps_l (0, lm) A (Suc na) = (length A, lm')"+ −
using final equal_when_halt+ −
by(case_tac "abc_steps_l (0, lm) A (Suc na)" , simp)+ −
then have "abc_steps_l (0, lm) (A [+] B) (Suc na) = (length A, lm')"+ −
using a b c e+ −
by(simp add: abc_step_red2)+ −
thus "?thesis"+ −
by blast+ −
qed+ −
+ −
lemma abc_exec_null: "abc_steps_l sam [] n = sam"+ −
apply(cases sam)+ −
apply(induct n)+ −
apply(auto simp: abc_step_red2)+ −
apply(auto simp: abc_step_l.simps abc_steps_l.simps abc_fetch.simps)+ −
done+ −
+ −
lemma abc_comp_frist_steps_halt_eq: + −
assumes final: "abc_steps_l (0, lm) A n = (length A, lm')"+ −
shows "\<exists> n'. abc_steps_l (0, lm) (A [+] B) n' = (length A, lm')"+ −
using final+ −
apply(case_tac "A = []")+ −
apply(rule_tac x = 0 in exI, simp add: abc_steps_l.simps abc_exec_null)+ −
apply(rule_tac abc_comp_frist_steps_halt_eq', simp_all)+ −
done+ −
+ −
+ −
lemma abc_comp_second_step_eq: + −
assumes exec: "abc_step_l (s, lm) (abc_fetch s B) = (sa, lma)"+ −
shows "abc_step_l (s + length A, lm) (abc_fetch (s + length A) (A [+] B))+ −
= (sa + length A, lma)"+ −
using assms+ −
apply(auto simp: abc_step_l.simps abc_fetch.simps nth_append abc_comp.simps abc_shift.simps split : if_splits )+ −
apply(case_tac [!] "B ! s", auto simp: Let_def)+ −
done+ −
+ −
lemma abc_comp_second_steps_eq:+ −
assumes exec: "abc_steps_l (0, lm) B n = (sa, lm')"+ −
shows "abc_steps_l (length A, lm) (A [+] B) n = (sa + length A, lm')"+ −
using assms+ −
proof(induct n arbitrary: sa lm')+ −
case 0+ −
thus "?case"+ −
by(simp add: abc_steps_l.simps)+ −
next+ −
case (Suc n)+ −
have ind: "\<And>sa lm'. abc_steps_l (0, lm) B n = (sa, lm') \<Longrightarrow> + −
abc_steps_l (length A, lm) (A [+] B) n = (sa + length A, lm')" by fact+ −
have exec: "abc_steps_l (0, lm) B (Suc n) = (sa, lm')" by fact+ −
obtain sb lmb where a: " abc_steps_l (0, lm) B n = (sb, lmb)"+ −
by (metis prod.exhaust)+ −
then have "abc_steps_l (length A, lm) (A [+] B) n = (sb + length A, lmb)"+ −
using ind by simp+ −
moreover have "abc_step_l (sb + length A, lmb) (abc_fetch (sb + length A) (A [+] B)) = (sa + length A, lm') "+ −
using a exec abc_comp_second_step_eq+ −
by(simp add: abc_step_red2) + −
ultimately show "?case"+ −
by(simp add: abc_step_red2)+ −
qed+ −
+ −
lemma length_abc_comp[simp, intro]: + −
"length (A [+] B) = length A + length B"+ −
by(auto simp: abc_comp.simps abc_shift.simps) + −
+ −
lemma abc_Hoare_plus_halt : + −
assumes A_halt : "{P} (A::abc_prog) {Q}"+ −
and B_halt : "{Q} (B::abc_prog) {S}"+ −
shows "{P} (A [+] B) {S}"+ −
proof(rule_tac abc_Hoare_haltI)+ −
fix lm+ −
assume a: "P lm"+ −
then obtain na lma where + −
"abc_final (abc_steps_l (0, lm) A na) A"+ −
and b: "abc_steps_l (0, lm) A na = (length A, lma)"+ −
and c: "Q abc_holds_for (length A, lma)"+ −
using A_halt unfolding abc_Hoare_halt_def+ −
by (metis (full_types) abc_final.simps abc_holds_for.simps prod.exhaust)+ −
have "\<exists> n. abc_steps_l (0, lm) (A [+] B) n = (length A, lma)"+ −
using abc_comp_frist_steps_halt_eq b+ −
by(simp)+ −
then obtain nx where h1: "abc_steps_l (0, lm) (A [+] B) nx = (length A, lma)" .. + −
from c have "Q lma"+ −
using c unfolding abc_holds_for.simps+ −
by simp+ −
then obtain nb lmb where+ −
"abc_final (abc_steps_l (0, lma) B nb) B"+ −
and d: "abc_steps_l (0, lma) B nb = (length B, lmb)"+ −
and e: "S abc_holds_for (length B, lmb)"+ −
using B_halt unfolding abc_Hoare_halt_def+ −
by (metis (full_types) abc_final.simps abc_holds_for.simps prod.exhaust)+ −
have h2: "abc_steps_l (length A, lma) (A [+] B) nb = (length B + length A, lmb)"+ −
using d abc_comp_second_steps_eq+ −
by simp+ −
thus "\<exists>n. abc_final (abc_steps_l (0, lm) (A [+] B) n) (A [+] B) \<and>+ −
S abc_holds_for abc_steps_l (0, lm) (A [+] B) n"+ −
using h1 e+ −
by(rule_tac x = "nx + nb" in exI, simp add: abc_steps_add)+ −
qed+ −
+ −
lemma abc_unhalt_append_eq:+ −
assumes unhalt: "{P} (A::abc_prog) \<up>"+ −
and P: "P args"+ −
shows "abc_steps_l (0, args) (A [+] B) stp = abc_steps_l (0, args) A stp"+ −
proof(induct stp)+ −
case 0+ −
thus "?case"+ −
by(simp add: abc_steps_l.simps)+ −
next+ −
case (Suc stp)+ −
have ind: "abc_steps_l (0, args) (A [+] B) stp = abc_steps_l (0, args) A stp"+ −
by fact+ −
obtain s nl where a: "abc_steps_l (0, args) A stp = (s, nl)"+ −
by (metis prod.exhaust)+ −
then have b: "s < length A"+ −
using unhalt P+ −
apply(auto simp: abc_Hoare_unhalt_def)+ −
by (metis abc_notfinal.simps)+ −
thus "?case"+ −
using a ind+ −
by(simp add: abc_step_red2 abc_step_l.simps abc_fetch.simps nth_append abc_comp.simps)+ −
qed+ −
+ −
lemma abc_Hoare_plus_unhalt1: + −
"{P} (A::abc_prog) \<up> \<Longrightarrow> {P} (A [+] B) \<up>"+ −
apply(rule_tac abc_Hoare_unhaltI)+ −
apply(frule_tac args = args and B = B and stp = n in abc_unhalt_append_eq)+ −
apply(simp_all add: abc_Hoare_unhalt_def)+ −
apply(erule_tac x = args in allE, simp)+ −
apply(erule_tac x = n in allE)+ −
apply(case_tac "(abc_steps_l (0, args) A n)", simp)+ −
done+ −
+ −
+ −
lemma notfinal_all_before:+ −
"\<lbrakk>abc_notfinal (abc_steps_l (0, args) A x) A; y\<le>x \<rbrakk>+ −
\<Longrightarrow> abc_notfinal (abc_steps_l (0, args) A y) A "+ −
apply(subgoal_tac "\<exists> d. x = y + d", auto)+ −
apply(case_tac "abc_steps_l (0, args) A y",simp)+ −
apply(rule_tac classical, simp add: abc_steps_add leI halt_steps2)+ −
by arith+ −
+ −
lemma abc_Hoare_plus_unhalt2':+ −
assumes unhalt: "{Q} (B::abc_prog) \<up>"+ −
and halt: "{P} (A::abc_prog) {Q}"+ −
and notnull: "A \<noteq> []"+ −
and P: "P args" + −
shows "abc_notfinal (abc_steps_l (0, args) (A [+] B) n) (A [+] B)"+ −
proof -+ −
obtain st nl stp where a: "abc_final (abc_steps_l (0, args) A stp) A"+ −
and b: "Q abc_holds_for (length A, nl)"+ −
and c: "abc_steps_l (0, args) A stp = (st, nl)"+ −
using halt P unfolding abc_Hoare_halt_def+ −
by (metis abc_holds_for.simps prod.exhaust)+ −
thm abc_before_final+ −
obtain stpa where d: + −
"abc_notfinal (abc_steps_l (0, args) A stpa) A \<and> abc_final (abc_steps_l (0, args) A (Suc stpa)) A"+ −
using a notnull abc_before_final[of args A stp]+ −
by(auto)+ −
thus "?thesis"+ −
proof(cases "n < Suc stpa")+ −
case True+ −
have h: "n < Suc stpa" by fact+ −
then have "abc_notfinal (abc_steps_l (0, args) A n) A"+ −
using d+ −
by(rule_tac notfinal_all_before, auto)+ −
moreover then have "abc_steps_l (0, args) (A [+] B) n = abc_steps_l (0, args) A n"+ −
using notnull+ −
by(rule_tac abc_comp_frist_steps_eq_pre, simp_all)+ −
ultimately show "?thesis"+ −
by(case_tac "abc_steps_l (0, args) A n", simp)+ −
next+ −
case False+ −
have "\<not> n < Suc stpa" by fact+ −
then obtain d where i1: "n = Suc stpa + d"+ −
by (metis add_Suc less_iff_Suc_add not_less_eq)+ −
have "abc_steps_l (0, args) A (Suc stpa) = (length A, nl)"+ −
using d a c+ −
apply(case_tac "abc_steps_l (0, args) A stp", simp add: equal_when_halt)+ −
by(case_tac "abc_steps_l (0, args) A (Suc stpa)", simp add: equal_when_halt)+ −
moreover have "abc_steps_l (0, args) (A [+] B) stpa = abc_steps_l (0, args) A stpa"+ −
using notnull d+ −
by(rule_tac abc_comp_frist_steps_eq_pre, simp_all)+ −
ultimately have i2: "abc_steps_l (0, args) (A [+] B) (Suc stpa) = (length A, nl)"+ −
using d+ −
apply(case_tac "abc_steps_l (0, args) A stpa", simp)+ −
by(simp add: abc_step_red2 abc_steps_l.simps abc_fetch.simps abc_comp.simps nth_append)+ −
obtain s' nl' where i3:"abc_steps_l (0, nl) B d = (s', nl')"+ −
by (metis prod.exhaust)+ −
then have i4: "abc_steps_l (0, args) (A [+] B) (Suc stpa + d) = (length A + s', nl')"+ −
using i2 apply(simp only: abc_steps_add)+ −
using abc_comp_second_steps_eq[of nl B d s' nl']+ −
by simp+ −
moreover have "s' < length B"+ −
using unhalt b i3+ −
apply(simp add: abc_Hoare_unhalt_def)+ −
apply(erule_tac x = nl in allE, simp)+ −
by(erule_tac x = d in allE, simp)+ −
ultimately show "?thesis"+ −
using i1+ −
by(simp)+ −
qed+ −
qed+ −
+ −
lemma abc_comp_null_left[simp]: "[] [+] A = A"+ −
apply(induct A)+ −
apply(case_tac [2] a)+ −
apply(auto simp: abc_comp.simps abc_shift.simps abc_inst_shift.simps)+ −
done+ −
+ −
lemma abc_comp_null_right[simp]: "A [+] [] = A"+ −
apply(induct A)+ −
apply(case_tac [2] a)+ −
apply(auto simp: abc_comp.simps abc_shift.simps abc_inst_shift.simps)+ −
done+ −
+ −
lemma abc_Hoare_plus_unhalt2:+ −
"\<lbrakk>{Q} (B::abc_prog)\<up>; {P} (A::abc_prog) {Q}\<rbrakk>\<Longrightarrow> {P} (A [+] B) \<up>"+ −
apply(case_tac "A = []")+ −
apply(simp add: abc_Hoare_halt_def abc_Hoare_unhalt_def abc_exec_null)+ −
apply(rule_tac abc_Hoare_unhaltI)+ −
apply(erule_tac abc_Hoare_plus_unhalt2', simp)+ −
apply(simp, simp)+ −
done+ −
+ −
end+ −
+ −
+ −