Theory Program_Analysis
theory Program_Analysis
imports
UPPAAL_State_Networks_Impl
Munta_Base.More_Methods
begin
fun steps_approx :: "nat ⇒ 't instrc option list ⇒ addr ⇒ addr set" where
"steps_approx 0 prog pc = (if pc < length prog then {pc} else {})" |
"steps_approx (Suc n) prog pc =
(
if pc ≥ length prog
then {}
else
case prog ! pc of
None ⇒ {pc}
| Some cmd ⇒
let succs =
(
case cmd of
CEXP ac ⇒ {pc + 1}
| INSTR instr ⇒ (
case instr of
CALL ⇒ {..<length prog}
| RETURN ⇒ {..<length prog}
| JMPZ pc' ⇒ {pc + 1, pc'}
| HALT ⇒ {}
| _ ⇒ {pc + 1})
)
in {pc} ∪ ⋃ (steps_approx n prog ` succs)
)
"
lemma bounded_less_simp[simp]:
"∀q∈{..<p::nat}. P q ≡ ∀ q < p. P q"
by (rule eq_reflection) auto
context
fixes prog :: "int instrc option list"
and strip :: "real instrc ⇒ instr"
assumes instr_id[simp]:
"strip (INSTR cmd) = cmd"
"strip (CEXP ac) ∉ {CALL, RETURN, HALT} ∪ (JMPZ ` UNIV)"
begin
private definition [simp]:
"P' ≡ map_option strip o (conv_prog (λ i. if i < length prog then prog ! i else None))"
lemma steps_out_of_range':
assumes "steps P' n (pc, st, s, f, rs) (pc', st', s', f', rs')" "pc ≥ length prog"
shows "pc' = pc"
using assms by cases (auto simp: striptp_def)
lemmas steps_out_of_range = steps_out_of_range'[unfolded striptp_def P'_def]
lemma steps_steps_approx':
assumes "steps P' n (pc, st, s, f, rs) (pc', st', s', f', rs')" "pc' < length prog"
shows "pc' ∈ steps_approx n prog pc"
proof -
{
fix pc :: nat
and st :: "int list"
and m :: "int list"
and f :: bool
and rs :: "nat list"
and a :: nat
and aa :: "int list"
and ab :: "int list"
and ac :: bool
and b :: "nat list"
and n :: nat
and za :: "int instrc"
and x2 :: "int instrc"
assume A:
"UPPAAL_Asm.step (strip (map_instrc real_of_int za)) (pc, st, m, f, rs)
= Some (a, aa, ab, ac, b)"
"UPPAAL_Asm.steps (map_option strip ∘
(λpc. conv_prog (If (pc < length prog) (prog ! pc)) None)) n
(a, aa, ab, ac, b) (pc', st', s', f', rs')"
"pc' ∈ steps_approx n prog a"
"pc' < length prog"
"(if pc < length prog then prog ! pc else None) = Some za"
"prog ! pc = Some x2"
"¬ (∃x∈case x2::int instrc of INSTR (JMPZ pc') ⇒ {pc + 1, pc'}
| INSTR CALL ⇒ {..<length prog} | INSTR instr.RETURN ⇒ {..<length prog}
| INSTR HALT ⇒ {} | INSTR _ ⇒ {pc + 1}
| CEXP ac ⇒ {pc + 1}. pc' ∈ steps_approx n prog x)"
have "pc' = pc"
proof (cases x2)
case (INSTR x1)
with A show "pc' = pc"
apply (cases x1)
apply (solves ‹auto elim!: UPPAAL_Asm.step.elims split: if_split_asm›)+
apply (auto elim!: UPPAAL_Asm.step.elims split: if_split_asm)[]
subgoal for q _
apply (cases "q < length prog")
apply force
apply (drule steps_out_of_range; simp; fail)
done
subgoal for q _
apply (cases "q < length prog")
apply force
apply (drule steps_out_of_range; simp; fail)
done
apply (auto elim!: UPPAAL_Asm.step.elims split: if_split_asm)[]
subgoal for q
apply (cases "q + 1 < length prog")
apply force
apply (drule steps_out_of_range; simp)
done
subgoal for q
apply (cases "q + 1 < length prog")
apply force
apply (drule steps_out_of_range; simp)
done
apply (solves ‹auto elim!: UPPAAL_Asm.step.elims split: if_split_asm›)+
done
next
case (CEXP x2)
with A show ?thesis
using instr_id by (fastforce split: if_split_asm elim!: UPPAAL_Asm.step.elims)
qed
} note * = this
show ?thesis
using assms
apply (
induction P' n "(pc, st, s, f, rs)" "(pc', st', s', f', rs')"
arbitrary: pc st s f rs rule: steps.induct
)
apply (solves ‹simp split: option.split›)
apply (clarsimp, rule conjI)
apply (simp add: striptp_def split: if_split_asm; fail)
apply (clarsimp split: option.split, rule conjI)
apply (solves ‹auto simp add: striptp_def split: if_split_asm›)
apply safe
by (rule *)
qed
lemmas steps_steps_approx = steps_steps_approx'[unfolded P'_def]
end
context
fixes prog :: "int instrc option list"
begin
private abbreviation "P i ≡ if i < length prog then prog ! i else None"
lemma stepsc_out_of_range:
assumes "stepsc (conv_prog P) n u (pc, st, s, f, rs) (pc', st', s', f', rs')" "pc ≥ length prog"
shows "pc' = pc"
using assms by cases auto
lemma stepsc_steps_approx:
assumes "stepsc (conv_prog P) n u (pc, st, s, f, rs) (pc', st', s', f', rs')" "pc' < length prog"
shows "pc' ∈ steps_approx n prog pc"
proof -
{
fix u :: "nat ⇒ real"
and pc :: nat
and st :: "int list"
and m :: "int list"
and f :: bool
and rs :: "nat list"
and a :: nat
and aa :: "int list"
and ab :: "int list"
and ac :: bool
and b :: "nat list"
and n :: nat
and z :: "int instrc"
assume A: "stepc (map_instrc real_of_int z) u (pc, st, m, f, rs) = Some (a, aa, ab, ac, b)"
"stepsc (conv_prog P) n u (a, aa, ab, ac, b) (pc', st', s', f', rs')"
"pc' ∈ steps_approx n prog a"
"pc' < length prog"
"P pc = Some z"
have "∀x2. prog ! pc = Some x2 ⟶ pc' = pc ∨
(∃x∈case x2 of INSTR (JMPZ pc') ⇒ {pc + 1, pc'} | INSTR CALL ⇒ {..<length prog}
| INSTR instr.RETURN ⇒ {..<length prog} | INSTR HALT ⇒ {} | INSTR _ ⇒ {pc + 1}
| CEXP ac ⇒ {pc + 1}. pc' ∈ steps_approx n prog x)"
proof(cases z)
case (INSTR x1)
with A show ?thesis
apply (simp split: option.split_asm if_split_asm)
apply (cases x1)
apply (simp split: if_split_asm; fail)
apply (solves ‹auto elim!: UPPAAL_Asm.step.elims split: if_split_asm›)+
apply (auto elim!: UPPAAL_Asm.step.elims split: if_split_asm)[]
subgoal for q
apply (cases "q < length prog")
apply force
apply (drule stepsc_out_of_range; simp)
done
subgoal for q
apply (cases "q < length prog")
apply force
apply (drule stepsc_out_of_range; simp)
done
apply (auto elim!: UPPAAL_Asm.step.elims split: if_split_asm)[]
subgoal for q
apply (cases "q + 1 < length prog")
apply force
apply (drule stepsc_out_of_range; simp)
done
subgoal for q
apply (cases "q + 1 < length prog")
apply force
apply (drule stepsc_out_of_range; simp)
done
apply (drule stepsc_out_of_range; simp)
apply (solves ‹auto elim!: UPPAAL_Asm.step.elims split: if_split_asm›)+
done
next
case (CEXP x2)
with A show ?thesis
by (force split: if_split_asm)
qed
} note * = this
show ?thesis
using assms
apply (
induction "conv_prog P" n u "(pc, st, s, f, rs)" "(pc', st', s', f', rs')"
arbitrary: pc st s f rs rule: stepsc.induct
)
apply (simp split: option.split)
apply clarsimp
apply (rule conjI)
apply (simp split: if_split_asm; fail)
apply (clarsimp split: option.split)
apply (rule conjI)
apply (simp split: if_split_asm; fail)
by (rule *)
qed
definition
"time_indep_check pc n ≡
∀ pc' ∈ steps_approx n prog pc. pc' < length prog
⟶ (case prog ! pc' of Some cmd ⇒ is_instr cmd | _ ⇒ True)"
lemma time_indep_overapprox:
assumes
"time_indep_check pc n"
shows "time_indep (conv_prog P) n (pc, st, s, f, rs)"
proof -
{ fix pc' st' s' f' rs' cmd u
assume A:
"stepsc (conv_prog local.P) n u (pc, st, s, f, rs) (pc', st', s', f', rs')"
"conv_prog local.P pc' = Some cmd"
have "is_instr cmd"
proof (cases "pc' < length prog")
case True
with A(2) obtain cmd' where "prog ! pc' = Some cmd'" by auto
with True stepsc_steps_approx[OF A(1)] A(2) assms show ?thesis
by (cases cmd') (auto simp: time_indep_check_def)
next
case False
with A(2) show ?thesis by (auto split: option.split_asm)
qed
}
then show ?thesis unfolding time_indep_def by blast
qed
end
context UPPAAL_Reachability_Problem_precompiled_defs
begin
definition
"collect_cexp' pc = {ac. Some (CEXP ac) ∈ ((!) prog) ` steps_approx max_steps prog pc}"
definition "clkp_set'' i l ≡
collect_clock_pairs (inv ! i ! l) ∪
⋃ ((λ (g, _). constraint_pair ` collect_cexp' g) ` set (trans ! i ! l))"
definition
"collect_cexp = {ac. Some (CEXP ac) ∈ set prog}"
definition
"collect_store' pc =
{(c, x). Some (INSTR (STOREC c x)) ∈ ((!) prog) ` steps_approx max_steps prog pc}"
end
lemma visited_resets_mono:
"set r ⊆ set r'" if "visited P n (pc, st, s, f, r) (pc', st', s', f', r') pcs"
using that
apply (
induction P ≡ P n "(pc, st, s, f, r :: nat list)" "(pc', st', s', f', r')" pcs
arbitrary: pc st s f r rule: visited.induct
)
apply blast
by (erule step.elims; force split: option.splits if_splits elim!: step.elims)+
lemma visitedc_resets_mono:
"set r ⊆ set r'" if "visitedc P n u (pc, st, s, f, r) (pc', st', s', f', r') pcs"
using that
apply (
induction P ≡ P n u "(pc, st, s, f, r :: nat list)" "(pc', st', s', f', r')" pcs
arbitrary: pc st s f r rule: visitedc.induct
)
apply blast
by (erule stepc.elims; force split: option.splits if_splits elim!: step.elims)+
lemma visited_reset:
"∃ x. ∃ pc ∈ set pcs. Some (STOREC c x) = P pc"
if "visited P n (pc, st, s, f, r) (pc', st', s', f', r') pcs" "c ∈ set r' - set r"
using that
apply (
induction P ≡ P n "(pc, st, s, f, r :: nat list)" "(pc', st', s', f', r')" pcs
arbitrary: pc st s f r rule: visited.induct
)
apply blast
by (erule step.elims; force split: option.split_asm if_split_asm elim!: step.elims)
lemma visitedc_reset:
"∃ x. ∃ pc ∈ set pcs. Some (INSTR (STOREC c x)) = P pc"
if "visitedc P n u (pc, st, s, f, r) (pc', st', s', f', r') pcs" "c ∈ set r' - set r"
using that
apply (
induction P ≡ P n u "(pc, st, s, f, r :: nat list)" "(pc', st', s', f', r')" pcs
arbitrary: pc st s f r rule: visitedc.induct
)
apply blast
by (erule stepc.elims; force split: option.split_asm if_split_asm elim!: step.elims)
lemma visited_fuel_mono:
"visited P n' s s' pcs" if "visited P n s s' pcs" "n' ≥ n"
using that
apply (induction arbitrary: n')
subgoal for _ _ _ n'
by (cases n') (auto intro: visited.intros)
subgoal for _ _ _ _ _ _ _ _ _ _ _ n'
by (cases n') (auto intro: visited.intros)
done
lemma visitedc_fuel_mono:
"visitedc P n' u s s' pcs" if "visitedc P n u s s' pcs" "n' ≥ n"
using that
apply (induction arbitrary: n')
subgoal for _ _ _ _ n'
by (cases n') (auto intro: visitedc.intros)
subgoal for _ _ _ _ _ _ _ _ _ _ _ _ n'
by (cases n') (auto intro: visitedc.intros)
done
lemma visted_split:
assumes "visited P n (pc, st, s, f, r) s'' (pcs' @ pc' # pcs)"
obtains st' s' f' r' where
"visited P n (pc, st, s, f, r) (pc', st', s', f', r') pcs"
"visited P n (pc', st', s', f', r') s'' (pcs' @ [pc'])"
apply atomize_elim
using assms
proof (induction _ _ _ _ "pcs' @ pc' # pcs" arbitrary: pcs rule: visited.induct)
case (1 prog n u start)
then show ?case by simp
next
case prems: (2 cmd pc st m f rs s prog n s' pcs pcs'')
show ?case
proof (cases "pcs'' = []")
case True
with prems show ?thesis by (blast intro: visited.intros)
next
case False
with ‹pcs @ [pc] = _› obtain pcs3 where "pcs'' = pcs3 @ [pc]"
by (metis append_butlast_last_id last_ConsR last_append last_snoc list.distinct(1))
with prems obtain st' s'a f' r' where
"visited prog n s (pc', st', s'a, f', r') pcs3"
"visited prog n (pc', st', s'a, f', r') s' (pcs' @ [pc'])"
by (auto 9 2)
with prems ‹pcs'' = _› show ?thesis by (auto 4 6 intro: visited.intros visited_fuel_mono)
qed
qed
lemma visited_steps':
assumes "visited P n (pc, st, s, f, r) s'' pcs" "pc' ∈ set pcs"
obtains st' s' f' r' where "steps P n (pc, st, s, f, r) (pc', st', s', f', r')"
using assms by (force dest!: split_list dest: visited_steps elim: visted_split)
lemma vistedc_split:
assumes "visitedc P n u (pc, st, s, f, r) s'' (pcs' @ pc' # pcs)"
obtains st' s' f' r' where
"visitedc P n u (pc, st, s, f, r) (pc', st', s', f', r') pcs"
"visitedc P n u (pc', st', s', f', r') s'' (pcs' @ [pc'])"
apply atomize_elim
using assms
proof (induction _ _ _ _ _ "pcs' @ pc' # pcs" arbitrary: pcs rule: visitedc.induct)
case (1 prog n u start)
then show ?case by simp
next
case prems: (2 cmd u pc st m f rs s prog n s' pcs pcs'')
show ?case
proof (cases "pcs'' = []")
case True
with prems show ?thesis by (blast intro: visitedc.intros)
next
case False
with ‹pcs @ [pc] = _› obtain pcs3 where "pcs'' = pcs3 @ [pc]"
by (metis append_butlast_last_id last_ConsR last_append last_snoc list.distinct(1))
with prems obtain st' s'a f' r' where
"visitedc prog n u s (pc', st', s'a, f', r') pcs3"
"visitedc prog n u (pc', st', s'a, f', r') s' (pcs' @ [pc'])"
by (auto 9 2)
with prems ‹pcs'' = _› show ?thesis by (auto 4 6 intro: visitedc.intros visitedc_fuel_mono)
qed
qed
lemma visitedc_stepsc':
assumes "visitedc P n u (pc, st, s, f, r) s'' pcs" "pc' ∈ set pcs"
obtains st' s' f' r' where "stepsc P n u (pc, st, s, f, r) (pc', st', s', f', r')"
using assms by (force dest!: split_list dest: visitedc_stepsc elim: vistedc_split)
lemma steps_fuel_mono:
"steps P n' s s'" if "steps P n s s'" "n' ≥ n"
using that
apply (induction arbitrary: n')
subgoal for _ _ _ n'
by (cases n') auto
subgoal for _ _ _ _ _ _ _ _ _ _ n'
by (cases n') auto
done
lemma exec_steps':
assumes "exec prog n s pcs = Some (s', pcs')" "pc' ∈ set pcs' - set pcs"
obtains st m f rs where "steps prog n s (pc', st, m, f, rs)"
apply atomize_elim
using assms
proof (induction P ≡ prog n s pcs arbitrary: s' rule: exec.induct)
case 1
then show ?case by simp
next
case (2 n pc st m f rs pcs)
then obtain instr where "prog pc = Some instr" by (cases "prog pc") auto
show ?case
proof (cases "instr = HALT")
case True
with "2.prems" ‹prog pc = _› show ?thesis by (auto 2 6)
next
case F: False
show ?thesis
proof (cases "pc' = pc")
case True
with ‹prog pc = _› show ?thesis by (auto 2 5)
next
case False
with ‹prog pc = _› 2(2,3) F show ?thesis
by - (
erule exec.elims;
auto 5 6
dest!: 2(1)[OF ‹prog pc = _› F, rotated, OF sym]
simp: option.split_asm if_split_asm
)
qed
qed
qed
lemma exec_visited:
assumes "exec prog n s pcs = Some ((pc, st, m, f, rs), pcs')"
obtains pcs'' where
"visited prog n s (pc, st, m, f, rs) pcs'' ∧ pcs' = pc # pcs'' @ pcs ∧ prog pc = Some HALT"
apply atomize_elim
using assms proof (induction P ≡ prog n s pcs arbitrary: pc st m f rs rule: exec.induct)
case 1
then show ?case by simp
next
case (2 n pc' st' m' f' rs' pcs')
then obtain instr where "prog pc' = Some instr" by (cases "prog pc'") auto
show ?case
proof (cases "instr = HALT")
case True
with "2.prems" ‹prog pc' = _› show ?thesis by (auto elim: exec.elims intro: visited.intros)
next
case False
with 2(2) ‹prog pc' = _› show ?thesis
by - (
erule exec.elims;
auto split: option.split_asm if_split_asm intro: visited.intros
dest!: 2(1)[OF ‹prog pc' = _› False, rotated, OF sym]
)
qed
qed
lemma exec_reset':
"∃ x. ∃ pc ∈ set pcs'. Some (STOREC c x) = P pc"
if "exec P n (pc, st, s, f, r) pcs = Some ((pc', st', s', f', r'), pcs')" "c ∈ set r' - set r"
proof -
from exec_visited[OF that(1)] obtain pcs'' where *:
"visited P n (pc, st, s, f, r) (pc', st', s', f', r') pcs''"
"pcs' = pc' # pcs'' @ pcs ∧ P pc' = Some HALT"
by auto
from visited_reset[OF this(1) that(2)] obtain x pc where
"pc∈set pcs''" "Some (STOREC c x) = P pc"
by auto
with *(2) show ?thesis by auto
qed
lemma steps_approx_out_of_range:
"steps_approx n prog pc = {}" if "pc ≥ length prog"
using that by (induction n) auto
lemma steps_resets_mono:
"set r ⊆ set r'" if "steps P n (pc, st, s, f, r) (pc', st', s', f', r')"
using that
by (induction "(pc, st, s, f, r)" "(pc', st', s', f', r')" arbitrary: pc st s f r;
fastforce intro: visited.intros elim!: step.elims split: if_split_asm)
lemma resets_start:
assumes
"∀ pc ∈ {pc..pc'}. ∃ c x. prog ! pc = Some (INSTR (STOREC c x))"
"steps
(map_option stripf o (λpc. if pc < size prog then prog ! pc else None))
n (pc, st, s, f, r) (pc_t, st', s', f', r')"
"prog ! pc_t = Some (INSTR HALT)"
shows "{c. ∃ x. ∃ pc ∈ {pc .. pc'}. prog ! pc = Some (INSTR (STOREC c x))} ⊆ set r'"
using assms(2,3,1)
proof (induction
"(map_option stripf o (λpc. if pc < size prog then prog ! pc else None))" n "(pc, st, s, f, r)"
"(pc_t, st', s', f', r')" arbitrary: pc st s f r
)
case prems: 1
show ?case
proof (cases "pc' ≥ pc_t")
case True
with prems obtain c x where "prog ! pc_t = Some (INSTR (STOREC c x))"
by fastforce
with prems show ?thesis by simp
next
case False
with prems show ?thesis by auto
qed
next
case prems: (2 cmd pc st m f rs s n)
show ?case
proof (cases "pc' ≥ pc")
case True
with prems(6) obtain c d where "prog ! pc = Some (INSTR (STOREC c d))"
by fastforce
moreover obtain pc1 st' s' f' r1 where "s = (pc1, st', s', f', r1)"
using prod.exhaust by metis
ultimately have "pc1 = pc + 1"
using prems(1,2) by (auto elim!: step.elims split: if_split_asm)
with prems(4)[OF ‹s = _› prems(5)] prems(6) have
"{c. ∃x. ∃pc∈{pc1..pc'}. prog ! pc = Some (INSTR (STOREC c x))} ⊆ set r'"
by auto
moreover have "c ∈ set r1"
using prems(1,2) ‹s = _› ‹prog ! pc = _› by (auto elim!: step.elims split: if_split_asm)
moreover then have "c ∈ set r'"
using prems(3) ‹s = _› by (auto dest: steps_resets_mono)
ultimately show ?thesis
using ‹pc1 = _› ‹prog ! pc = _› apply clarsimp
subgoal for _ _ pc''
by (cases "pc'' = pc"; force)
done
next
case False
then show ?thesis by auto
qed
qed
unbundle lattice_syntax
function find_resets_start where
"find_resets_start prog pc =
(
if pc < length prog
then
case prog ! pc of
Some (INSTR (STOREC c x)) ⇒ (Some pc ⊔ find_resets_start prog (pc + 1)) |
_ ⇒ None
else None
)
"
by auto
termination
by (relation "measure (λ (prog, pc). length prog - pc)") auto
lemma find_resets_start:
"∀ pc ∈ {pc..pc'}. ∃ c x. prog ! pc = Some (INSTR (STOREC c x))" if
"find_resets_start prog pc = Some pc'"
using that
proof (induction arbitrary: pc' rule: find_resets_start.induct)
case prems: (1 prog pc)
from prems(2) show ?case
apply (simp split: if_split_asm)
apply (
auto 4 3 simp flip: not_less_eq_eq
simp del: find_resets_start.simps simp: le_max_iff_disj sup_nat_def sup_option_def
split: option.split_asm instr.split_asm instrc.split_asm dest!: prems(1)
)
done
qed
lemmas resets_start' = resets_start[OF find_resets_start]
context UPPAAL_Reachability_Problem_precompiled_defs
begin
definition
"collect_store'' pc ≡
case find_resets_start prog pc of
None ⇒ {} |
Some pc' ⇒
{(c, x). Some (INSTR (STOREC c x)) ∈ ((!) prog) ` {pc .. pc'}}"
end
lemma bexp_atLeastAtMost_iff:
"(∀ pc ∈ {pc_s..pc_t}. P pc) ⟷ (∀ pc. pc_s ≤ pc ∧ pc ≤ pc_t ⟶ P pc)"
by auto
lemma bexp_atLeastLessThan_iff:
"(∀ pc ∈ {pc_s..<pc_t}. P pc) ⟷ (∀ pc. pc_s ≤ pc ∧ pc < pc_t ⟶ P pc)"
by auto
lemma guaranteed_execution:
assumes
"∀ pc ∈ {pc..<pc_t}.
prog ! pc ≠ None
∧ prog ! pc ∉ Some ` INSTR `
{STORE, HALT, POP, CALL, RETURN, instr.AND, instr.NOT, instr.ADD, instr.LT, instr.LE, instr.EQ}
∧ (∀ c d. prog ! pc = Some (INSTR (STOREC c d)) ⟶ d = 0)
"
"∀ pc ∈ {pc..<pc_t}. ∀ pc'. prog ! pc = Some (INSTR (JMPZ pc')) ⟶ pc' > pc ∧ pc' ≤ pc_t"
"prog ! pc_t = Some (INSTR HALT)" "pc_t ≥ pc" "n > pc_t - pc" "pc_t < length prog"
shows "∃ st' s' f' r'. steps
(map_option stripf o (λpc. if pc < size prog then prog ! pc else None))
n (pc, st, s, f, r) (pc_t, st', s', f', r')"
using assms
proof (induction "pc_t - pc" arbitrary: pc st s f r n rule: less_induct)
case less
let ?prog = "(map_option stripf ∘ (λpc. if pc < length prog then prog ! pc else None))"
from ‹pc_t - pc < n› obtain n' where [simp]: "n = Suc n'" by (cases n) auto
from less.prems(3-) have [simp]: "pc < length prog" "pc_t < length prog" by auto
show ?case
proof (cases "pc_t = pc")
case True
then show ?thesis by force
next
case False
with less.prems(1,4) have valid_instr:
"prog ! pc ∉ Some ` INSTR `
{STORE, HALT, POP, CALL, RETURN, instr.AND, instr.NOT, instr.ADD, instr.LT, instr.LE, instr.EQ}"
"prog ! pc ≠ None"
by auto
from ‹pc ≤ _› ‹pc_t ≠ _› less.prems(2) have jumps:
"pc' > pc ∧ pc' ≤ pc_t" if "prog ! pc = Some (INSTR (JMPZ pc'))" for pc'
using that by fastforce
from ‹pc ≤ _› ‹pc_t ≠ _› less.prems(1) have stores:
"d = 0" if "prog ! pc = Some (INSTR (STOREC c d))" for c d
using that by fastforce
show ?thesis
proof (cases "prog ! pc")
case None
from ‹pc_t ≠ _› less.prems(1,4) have "prog ! pc ≠ None"
by simp
with None show ?thesis by auto
next
case (Some a)
then show ?thesis
proof (cases a)
case (INSTR instr)
have *:
"∃st' s' f' r'. steps ?prog n' (pc', st, s, f, r) (pc_t, st', s', f', r')"
if "pc < pc'" "pc' ≤ pc_t" for pc' st s f r
apply (rule less.hyps[of pc'])
subgoal
using that by simp
subgoal
using that less.prems(1) by force
subgoal
apply clarsimp
subgoal premises prems for pc_s pc'
proof -
from prems that have "pc_s ∈ {pc..<pc_t}" by simp
with prems(1) less.prems(2) show ?thesis by blast
qed
done
using ‹prog ! pc_t = _› ‹pc_t - pc < n› that by auto
from ‹pc_t ≠ pc› ‹pc ≤ _› have "Suc pc ≤ pc_t" by simp
then obtain pc' st' s' f' r' where
"step instr (pc, st, s, f, r) = Some (pc', st', s', f', r')" "pc < pc'" "pc' ≤ pc_t"
apply atomize_elim
apply (cases instr)
using valid_instr ‹a = _› ‹_ = Some a› by (auto simp: stores jumps)
with ‹a = _› ‹_ = Some a› show ?thesis by (force dest!: *)
next
case (CEXP x2)
have *:
"∃st' s' f' r'. steps ?prog n' (Suc pc, st, s, f, r) (pc_t, st', s', f', r')"
if "Suc pc ≤ pc_t" for st s f r
apply (rule less.hyps[of "Suc pc"])
subgoal
using ‹pc ≤ _› ‹pc_t ≠ pc› by simp
subgoal
using less.prems(1) by force
subgoal
apply clarsimp
subgoal premises prems for pc_s pc'
proof -
from prems have "pc_s ∈ {pc..<pc_t}" by simp
with prems(1) less.prems(2) show ?thesis by blast
qed
done
using ‹prog ! pc_t = _› ‹pc_t - pc < n› that by auto
from ‹pc_t ≠ pc› ‹pc ≤ _› have "Suc pc ≤ pc_t" by simp
with ‹a = _› ‹_ = Some a› show ?thesis by (force dest!: *)
qed
qed
qed
qed
function find_next_halt where
"find_next_halt prog pc =
(
if pc < length prog
then
case prog ! pc of
Some (INSTR HALT) ⇒ Some pc |
_ ⇒ find_next_halt prog (pc + 1)
else None
)
"
by auto
termination
by (relation "measure (λ (prog, pc). length prog - pc)") auto
lemma find_next_halt_finds_halt:
"prog ! pc' = Some (INSTR HALT) ∧ pc ≤ pc' ∧ pc' < length prog"
if "find_next_halt prog pc = Some pc'"
using that proof (induction prog pc rule: find_next_halt.induct)
case prems: (1 prog pc)
from prems(20) show ?case
by (
simp,
simp
split: if_split_asm option.split_asm instrc.split_asm instr.split_asm
del: find_next_halt.simps;
fastforce dest: prems(1-19) simp del: find_next_halt.simps)
qed
definition
"guaranteed_execution_cond prog pc_s n ≡
case find_next_halt prog pc_s of
None ⇒ False |
Some pc_t ⇒
(
∀ pc ∈ {pc_s..<pc_t}.
prog ! pc ≠ None
∧ prog ! pc ∉ Some ` INSTR `
{STORE, HALT, POP, CALL, RETURN, instr.AND, instr.NOT, instr.ADD, instr.LT, instr.LE, instr.EQ}
∧ (∀ c d. prog ! pc = Some (INSTR (STOREC c d)) ⟶ d = 0)
) ∧
(∀ pc ∈ {pc_s..<pc_t}. ∀ pc'. prog ! pc = Some (INSTR (JMPZ pc')) ⟶ pc' > pc ∧ pc' ≤ pc_t)
∧ n > pc_t - pc_s
"
lemma guaranteed_execution_cond_alt_def[code]:
"guaranteed_execution_cond prog pc_s n ≡
case find_next_halt prog pc_s of
None ⇒ False |
Some pc_t ⇒
(
∀ pc ∈ {pc_s..<pc_t}.
prog ! pc ≠ None
∧ prog ! pc ∉ Some ` INSTR `
{STORE, HALT, POP, CALL, RETURN, instr.AND, instr.NOT, instr.ADD, instr.LT, instr.LE, instr.EQ}
∧ (case prog ! pc of Some (INSTR (STOREC c d)) ⇒ d = 0 | _ ⇒ True)
) ∧
(∀ pc ∈ {pc_s..<pc_t}.
case prog ! pc of Some (INSTR (JMPZ pc')) ⇒ pc' > pc ∧ pc' ≤ pc_t | _ ⇒ True)
∧ n > pc_t - pc_s
"
proof (rule eq_reflection, goal_cases)
case 1
have *:
"(∀ c d. prog ! pc = Some (INSTR (STOREC c d)) ⟶ d = 0) ⟷
(case prog ! pc of Some (INSTR (STOREC c d)) ⇒ d = 0 | _ ⇒ True)" for pc
by (auto split: option.split instrc.split instr.split)
have **:
"(∀ pc'. prog ! pc = Some (INSTR (JMPZ pc')) ⟶ pc' > pc ∧ pc' ≤ pc_t) ⟷
(case prog ! pc of Some (INSTR (JMPZ pc')) ⇒ pc' > pc ∧ pc' ≤ pc_t | _ ⇒ True)" for pc pc_t
by (auto split: option.split instrc.split instr.split)
show ?case unfolding guaranteed_execution_cond_def * ** ..
qed
lemma guaranteed_execution':
"∃ pc_t st' s' f' r' pcs'. exec
(map_option stripf o (λpc. if pc < size prog then prog ! pc else None))
n (pc, st, s, f, r) pcs = Some ((pc_t, st', s', f', r'), pcs')"
if "guaranteed_execution_cond prog pc n"
proof -
from that obtain pc_t where "find_next_halt prog pc = Some pc_t"
unfolding guaranteed_execution_cond_def bexp_atLeastAtMost_iff
by (auto split: option.split_asm)
then have "prog ! pc_t = Some (INSTR HALT) ∧ pc ≤ pc_t ∧ pc_t < length prog"
by (rule find_next_halt_finds_halt)
moreover then have "∃ st' s' f' r'. steps
(map_option stripf o (λpc. if pc < size prog then prog ! pc else None))
n (pc, st, s, f, r) (pc_t, st', s', f', r')"
using ‹_ = Some pc_t› that
unfolding guaranteed_execution_cond_def bexp_atLeastAtMost_iff
by - (rule guaranteed_execution, auto)
ultimately show ?thesis by (force dest: steps_exec)
qed
context UPPAAL_Reachability_Problem_precompiled_defs
begin
lemma collect_cexp_alt_def:
"collect_cexp =
set (List.map_filter
(λ x. case x of Some (CEXP ac) ⇒ Some ac | _ ⇒ None)
prog)"
unfolding collect_cexp_def set_map_filter by (auto split: option.split_asm instrc.split_asm)
lemma clkp_set'_alt_def:
"clkp_set' =
⋃ (collect_clock_pairs ` set (concat inv)) ∪ (constraint_pair ` collect_cexp)"
unfolding clkp_set'_def collect_cexp_def by auto
definition
"collect_store = {(c, x). Some (INSTR (STOREC c x)) ∈ set prog}"
lemma collect_store_alt_def:
"collect_store =
set (List.map_filter
(λ x. case x of Some (INSTR (STOREC c x)) ⇒ Some (c, x) | _ ⇒ None)
prog)"
unfolding collect_store_def set_map_filter
by (auto split: option.split_asm instrc.split_asm instr.split_asm)
lemma clk_set'_alt_def: "clk_set' = (fst ` clkp_set' ∪ fst ` collect_store)"
unfolding clk_set'_def collect_store_def by auto
end
fun conj_instr :: "'t instrc ⇒ addr ⇒ bool" where
"conj_instr (CEXP _) _ = True" |
"conj_instr (INSTR COPY) _ = True" |
"conj_instr (INSTR (JMPZ pc)) pc_t = (pc = pc_t)" |
"conj_instr (INSTR instr.AND) _ = True" |
"conj_instr _ _ = False"
inductive is_conj_block' :: "'t instrc option list ⇒ addr ⇒ addr ⇒ bool" where
"is_conj_block' prog pc pc" if
"pc < length prog"
"prog ! pc = Some (INSTR HALT)" |
"is_conj_block' prog pc pc'" if
"pc' < length prog"
"prog ! pc = Some (INSTR COPY)" "prog ! (pc + 1) = Some (CEXP ac)"
"prog ! (pc + 2) = Some (INSTR instr.AND)"
"is_conj_block' prog (pc + 3) pc'" |
"is_conj_block' prog pc pc'" if
"pc' < length prog"
"prog ! pc = Some (INSTR COPY)"
"prog ! (pc + 1) = Some (INSTR (JMPZ pc'))"
"prog ! (pc + 2) = Some (CEXP ac)"
"prog ! (pc + 3) = Some (INSTR instr.AND)"
"is_conj_block' prog (pc + 4) pc'"
inductive_cases stepscE: "stepsc prog n u (pc, st, m, f, rs) (pc', st', m', f', rs')"
function check_conj_block' :: "'t instrc option list ⇒ addr ⇒ addr option" where
"check_conj_block' prog pc = (
if pc ≥ length prog then None
else if prog ! pc = Some (INSTR HALT) then Some pc
else if
prog ! pc = Some (INSTR COPY) ∧ (case prog ! (pc + 1) of Some (CEXP ac) ⇒ True | _ ⇒ False)
∧ prog ! (pc + 2) = Some (INSTR instr.AND)
then check_conj_block' prog (pc + 3)
else if
prog ! pc = Some (INSTR COPY) ∧ (case prog ! (pc + 2) of Some (CEXP ac) ⇒ True | _ ⇒ False)
∧ prog ! (pc + 3) = Some (INSTR instr.AND)
∧ (case prog ! (pc + 1) of Some (INSTR (JMPZ pc')) ⇒ True | _ ⇒ False)
then
(case (prog ! (pc + 1), check_conj_block' prog (pc + 4)) of (Some (INSTR (JMPZ pc')), Some pc'')
⇒ if pc' = pc'' then Some pc' else None | _ ⇒ None)
else None
)
"
by pat_completeness auto
termination
by (relation "measure (λ (prog, pc). length prog - pc)") auto
lemma is_conj_block'_len_prog:
"pc' < length prog" if "is_conj_block' prog pc pc'"
using that by induction auto
lemma check_conj_block':
"check_conj_block' prog pc = Some pc' ⟹ is_conj_block' prog pc pc'"
apply (induction prog pc rule: check_conj_block'.induct)
apply (erule check_conj_block'.elims)
by (auto
split: if_split_asm option.split_asm instrc.split_asm instr.split_asm
simp del: check_conj_block'.simps
intro: is_conj_block'.intros is_conj_block'_len_prog)
lemma stepsc_reverseE':
assumes "stepsc prog (Suc n) u s s''" "s'' ≠ s"
obtains pc' st' m' f' rs' cmd where
"stepc cmd u (pc', st', m', f', rs') = Some s''"
"prog pc' = Some cmd"
"stepsc prog n u s (pc', st', m', f', rs')"
apply atomize_elim
using assms
proof (induction prog "Suc n" u s s'' arbitrary: n rule: stepsc.induct)
case (1 prog n u start)
then show ?case by simp
next
case prems: (2 cmd u pc st m f rs s prog n s')
then show ?case
proof (cases "s' = s")
case True
with prems show ?thesis
apply simp
apply solve_ex_triv+
by (auto elim: stepsc.cases)
next
case False
with prems(3) have "n > 0" by (auto elim!: stepsc.cases)
then obtain n' where "n = Suc n'" by (cases n) auto
from prems(4)[OF this False] obtain cmd pc' st' m' f' rs' where
"stepc cmd u (pc', st', m', f', rs') = Some s'" "prog pc' = Some cmd"
"stepsc prog n' u s (pc', st', m', f', rs')"
by atomize_elim
with prems show ?thesis unfolding ‹n = _› by blast
qed
qed
lemma stepsc_reverseE:
assumes "stepsc prog n u s s''" "s'' ≠ s"
obtains n' pc' st' m' f' rs' cmd where
"n = Suc n'"
"stepc cmd u (pc', st', m', f', rs') = Some s''"
"prog pc' = Some cmd"
"stepsc prog n' u s (pc', st', m', f', rs')"
proof -
from assms have "n > 0" by (auto elim!: stepsc.cases)
then obtain n' where "n = Suc n'" by (cases n) auto
with assms show ?thesis by (auto elim!: stepsc_reverseE' intro!: that)
qed
lemma
"pc = pc' - 1" if
"stepc (CEXP cc) u (pc, st, m, f, rs) = Some (pc', st', m', f', rs')"
using that by auto
lemma
"pc = pc' - 1" if
"stepc (INSTR instr) u (pc, st, m, f, rs) = Some (pc', st', m', f', rs')"
"¬ (∃ x. instr = JMPZ pc')" "instr ≠ RETURN" "instr ≠ CALL"
using that by (auto split: option.split_asm if_split_asm elim!: step.elims)
lemma stepc_pc_no_jump:
"pc = pc' - 1" if
"stepc cmd u (pc, st, m, f, rs) = Some (pc', st', m', f', rs')"
"cmd ≠ INSTR (JMPZ pc')" "cmd ≠ INSTR RETURN" "cmd ≠ INSTR CALL"
using that by (cases cmd) (auto split: option.split_asm if_split_asm elim!: step.elims)
inductive stepsn :: "'t programc ⇒ nat ⇒ (nat, 't :: time) cval ⇒ state ⇒ state ⇒ bool"
for prog where
"stepsn prog 0 u start start" |
"stepsn prog (Suc n) u (pc, st, m, f, rs) s'" if
"stepc cmd u (pc, st, m, f, rs) = Some s"
"prog pc = Some cmd"
"stepsn prog n u s s'"
declare stepsn.intros[intro]
lemma stepsc_stepsn:
assumes "stepsc P n u s s'"
obtains n' where "stepsn P n' u s s'" "n' < n"
using assms by induction auto
lemma stepsn_stepsc:
assumes "stepsn P n' u s s'" "n' < n"
shows "stepsc P n u s s'"
using assms
proof (induction arbitrary: n)
case (1 u start)
then obtain n' where "n = Suc n'" by (cases n) auto
then show ?case by auto
next
case (2 cmd u pc st m f rs s n s' n')
from ‹_ < n'› have "n < n' - 1" by simp
from 2(4)[OF this] 2(1,2,3,5) show ?case
proof -
have "(∃fa n fb p. P = fa ∧ n' = Suc n ∧ u = fb ∧ (pc, st, m, f, rs) = p ∧ s' = p) ∨ (∃i fa n is isa b ns p fb na pa. P = fb ∧ n' = Suc na ∧ u = fa ∧ (pc, st, m, f, rs) = (n, is, isa, b, ns) ∧ s' = pa ∧ stepc i fa (n, is, isa, b, ns) = Some p ∧ fb n = Some i ∧ stepsc fb na fa p pa)"
using "2.prems" Suc_pred' ‹P pc = Some cmd› ‹stepc cmd u (pc, st, m, f, rs) = Some s› ‹stepsc P (n' - 1) u s s'› gr_implies_not_zero by blast
then show ?thesis
by blast
qed
qed
lemma stepsn_extend:
assumes "stepsn P n1 u s s1" "stepsn P n2 u s s2" "n1 ≤ n2"
shows "stepsn P (n2 - n1) u s1 s2"
using assms
proof (induction arbitrary: n2 s2)
case (1 u start)
then show ?case by simp
next
case (2 cmd u pc st m f rs s n s')
from 2(1,2,5-) have "stepsn P (n2 - 1) u s s2" by (auto elim: stepsn.cases)
from 2(4)[OF this] ‹Suc n <= _› show ?case by simp
qed
lemma stepsc_halt:
"s' = (pc, s)" if "stepsc P n u (pc, s) s'" "P pc = Some (INSTR HALT)"
using that by (induction P n u "(pc, s)" s') auto
lemma stepsn_halt:
"s' = (pc, s)" if "stepsn P n u (pc, s) s'" "P pc = Some (INSTR HALT)"
apply (rule stepsc_halt[OF stepsn_stepsc[where n = "Suc n"]])
using that by simp+
lemma is_conj_block'_pc_mono:
"pc ≤ pc'" if "is_conj_block' prog pc pc'"
using that by induction auto
lemma is_conj_block'_halt:
"prog ! pc' = Some (INSTR HALT)" if "is_conj_block' prog pc pc'"
using that by induction auto
lemma numeral_4_eq_4:
"4 = Suc (Suc (Suc (Suc 0)))"
by simp
lemma is_conj_block'_is_conj:
assumes "is_conj_block' P pc pc'"
and "stepsn (λ i. if i < length P then P ! i else None) n u (pc, st, s, f, rs) (pc_t, st_t, s_t, True, rs_t)"
and "P ! pc_t = Some (INSTR HALT)"
shows "f ∧ pc_t = pc'"
using assms
proof (induction arbitrary: n st s f rs)
case (1 pc prog)
with stepsn_halt[OF this(3)] show ?case by simp
next
case prems: (2 pc' prog pc ac)
let ?P = "(λi. if i < length prog then prog ! i else None)"
consider (0) "n = 0" | (1) "n = 1" | (2) "n = 2" | (3) "n ≥ 3" by force
then show ?case
proof cases
case 0
with prems show ?thesis by (auto elim!: stepsn.cases)
next
case 1
with prems show ?thesis by (auto elim!: stepsn.cases simp: int_of_def split: if_split_asm)
next
case 2
with prems show ?thesis by (auto elim!: stepsn.cases simp: int_of_def numeral_2_eq_2 split: if_split_asm)
next
case 3
from prems have "pc + 2 < length prog" by (auto dest: is_conj_block'_pc_mono)
with prems(2-4) obtain st1 s1 rs1 where
"stepsn ?P 3 u (pc, st, s, f, rs) (pc + 3, st1, s1, f ∧ (u ⊢⇩a ac), rs1)"
by (force simp: int_of_def numeral_3_eq_3)
from stepsn_extend[OF this prems(7) 3] have
"stepsn ?P (n - 3) u (pc + 3, st1, s1, f ∧ (u ⊢⇩a ac), rs1) (pc_t, st_t, s_t, True, rs_t)" .
from prems(6)[OF this ‹prog ! pc_t = _›] have "pc_t = pc'" "u ⊢⇩a ac" f by auto
then show ?thesis by simp
qed
next
case prems: (3 pc' prog pc ac)
let ?P = "(λi. if i < length prog then prog ! i else None)"
consider (0) "n = 0" | (1) "n = 1" | (2) "n = 2" | (3) "n = 3" | (4) "n ≥ 4" by force
then show ?case
proof cases
case 0
with prems show ?thesis by (auto elim!: stepsn.cases)
next
case 1
with prems show ?thesis by (auto elim!: stepsn.cases simp: int_of_def split: if_split_asm)
next
case 2
with prems show ?thesis by (auto elim!: stepsn.cases simp: int_of_def numeral_2_eq_2 split: if_split_asm)
next
case 3
with prems show ?thesis
by (auto elim!: stepsn.cases simp: int_of_def numeral_3_eq_3 split: if_split_asm dest!: is_conj_block'_halt)
next
case 4
from prems have "pc + 3 < length prog" by (auto dest: is_conj_block'_pc_mono)
show ?thesis
proof (cases f)
case True
with ‹pc + 3 < _› prems(2-6) obtain st1 s1 rs1 where
"stepsn ?P 4 u (pc, st, s, f, rs) (pc + 4, st1, s1, f ∧ (u ⊢⇩a ac), rs1)"
by (force simp: int_of_def numeral_3_eq_3 numeral_4_eq_4)
from stepsn_extend[OF this prems(8) 4] have
"stepsn ?P (n - 4) u (pc + 4, st1, s1, f ∧ (u ⊢⇩a ac), rs1) (pc_t, st_t, s_t, True, rs_t)" .
from prems(7)[OF this ‹prog ! pc_t = _›] have "pc_t = pc'" "u ⊢⇩a ac" f by auto
then show ?thesis by simp
next
case False
with ‹pc + 3 < _› prems(1-6) obtain st1 s1 rs1 where
"stepsn ?P 2 u (pc, st, s, f, rs) (pc', st1, s1, False, rs1)"
by (force simp: int_of_def numeral_2_eq_2)
from stepsn_extend[OF this prems(8)] 4 have
"stepsn ?P (n - 2) u (pc', st1, s1, False, rs1) (pc_t, st_t, s_t, True, rs_t)" by simp
from stepsn_halt[OF this] prems(1,6) show ?thesis by (auto dest: is_conj_block'_halt)
qed
qed
qed
lemma is_conj_block'_is_conj':
assumes "is_conj_block' P pc pc'"
and "stepst (λ i. if i < length P then P ! i else None) n u (pc, st, s, f, rs) (pc_t, st_t, s_t, True, rs_t)"
shows "f ∧ pc_t = pc'"
using assms
unfolding stepst_def by (auto split: if_split_asm elim!: is_conj_block'_is_conj stepsc_stepsn)
lemma is_conj_block'_is_conj2:
assumes "is_conj_block' P (pc + 1) pc'" "P ! pc = Some (CEXP ac)"
and "stepst (λ i. if i < length P then P ! i else None) n u (pc, st, s, f, rs) (pc_t, st_t, s_t, True, rs_t)"
shows "(u ⊢⇩a ac) ∧ pc_t = pc'"
proof -
let ?P = "(λ i. if i < length P then P ! i else None)"
from assms(1) have "pc < pc'" "pc' < length P"
by (auto dest: is_conj_block'_pc_mono is_conj_block'_len_prog)
with assms(2,3) obtain st' s' rs' where
"stepst ?P (n - 1) u (pc + 1, st', s', u ⊢⇩a ac, rs') (pc_t, st_t, s_t, True, rs_t)"
unfolding stepst_def
apply (clarsimp split: if_split_asm)
apply (erule stepsc.cases)
by auto
from is_conj_block'_is_conj'[OF assms(1) this] show ?thesis .
qed
lemma is_conj_block'_is_conj3:
assumes "is_conj_block' P (pc + 2) pc'" "P ! pc = Some (CEXP ac)" "P ! (pc + 1) = Some (INSTR instr.AND)"
and "stepst (λ i. if i < length P then P ! i else None) n u (pc, st, s, f, rs) (pc_t, st_t, s_t, True, rs_t)"
shows "(u ⊢⇩a ac) ∧ pc_t = pc'"
proof -
let ?P = "(λ i. if i < length P then P ! i else None)"
from assms(1) have "pc < pc'" "pc' < length P"
by (auto dest: is_conj_block'_pc_mono is_conj_block'_len_prog)
with assms(2,3,4) obtain st' s' rs' f where
"stepst ?P (n - 2) u (pc + 2, st', s', f ∧ (u ⊢⇩a ac), rs') (pc_t, st_t, s_t, True, rs_t)"
unfolding stepst_def
apply (clarsimp split: if_split_asm)
apply (erule stepsc.cases)
apply force
apply (erule stepsc.cases)
by (auto split: if_split_asm option.split_asm elim!: UPPAAL_Asm.step.elims)
from is_conj_block'_is_conj'[OF assms(1) this] show ?thesis by simp
qed
definition
"is_conj_block P pc pc' ≡
(∃ ac. P ! pc = Some (CEXP ac)) ∧ is_conj_block' P (pc + 1) pc'
∨ (∃ ac.
P ! pc = Some (CEXP ac)) ∧ P ! (pc + 1) = Some (INSTR instr.AND)
∧ is_conj_block' P (pc + 2) pc'"
lemma is_conj_block_alt_def[code]:
"is_conj_block P pc pc' ≡
(case P ! pc of Some (CEXP ac) ⇒ True | _ ⇒ False) ∧ is_conj_block' P (pc + 1) pc'
∨ (case P ! pc of Some (CEXP ac) ⇒ True | _ ⇒ False) ∧ P ! (pc + 1) = Some (INSTR instr.AND)
∧ is_conj_block' P (pc + 2) pc'"
unfolding is_conj_block_def
by (rule eq_reflection) (auto split: option.split_asm instrc.split_asm)
lemma is_conj_block_is_conj:
assumes "is_conj_block P pc pc'" "P ! pc = Some (CEXP ac)"
and
"stepst
(λ i. if i < length P then P ! i else None) n u
(pc, st, s, f, rs)
(pc_t, st_t, s_t, True, rs_t)"
shows "(u ⊢⇩a ac) ∧ pc_t = pc'"
using assms
unfolding is_conj_block_def
apply safe
by ((drule is_conj_block'_is_conj2 is_conj_block'_is_conj3; simp), simp)+
lemma is_conj_block'_decomp:
"is_conj_block P pc' pc''" if
"is_conj_block' P pc pc''" "P ! pc' = Some (CEXP ac)" "pc ≤ pc'" "pc' ≤ pc''"
using that
proof (induction arbitrary: pc')
case (1 pc prog)
then show ?case by (simp add: is_conj_block_def)
next
case prems: (2 pc'' prog pc ac)
with ‹pc ≤ _› consider "pc' = pc" | "pc' = Suc pc" | "pc' = Suc (Suc pc)" | "pc + 3 ≤ pc'"
by force
then show ?case using prems by cases (auto simp add: numeral_3_eq_3 is_conj_block_def)
next
case prems: (3 pc'' prog pc ac)
with ‹pc ≤ _› consider
"pc' = pc" | "pc' = Suc pc" | "pc' = Suc (Suc pc)" | "pc' = Suc (Suc (Suc pc))" | "pc + 4 ≤ pc'"
by force
then show ?case using prems by cases (auto simp add: numeral_3_eq_3 numeral_4_eq_4 is_conj_block_def)+
qed
lemma is_conj_block_decomp:
"is_conj_block P pc' pc''" if
"is_conj_block P pc pc''" "P ! pc' = Some (CEXP ac)" "pc ≤ pc'" "pc' ≤ pc''"
using that
apply (subst (asm) is_conj_block_def)
apply safe
using One_nat_def add_Suc_right is_conj_block'_decomp le_simps(3) that(1)
apply (metis add.right_neutral le_neq_implies_less)
by (metis
One_nat_def Suc_1 add.right_neutral add_Suc_right instrc.simps(4) is_conj_block'_decomp
le_antisym not_less_eq_eq option.inject that(1))
lemma steps_approx_finite[intro,simp]:
"finite (steps_approx n P pc_s)"
by (induction rule: steps_approx.induct; clarsimp split: option.split instrc.split instr.split)
abbreviation "conv_P ≡ map (map_option (map_instrc real_of_int))"
lemma stepst_stepc_extend:
"stepst P n u (pc', s') (pc'', s'')"
if "stepst P n u (pc, s) (pc'', s'')" "stepsc P n u (pc, s) (pc', s')"
proof -
from that have "P pc'' = Some (INSTR HALT)" unfolding stepst_def by auto
from that obtain n1 n2 where *:
"stepsn P n1 u (pc, s) (pc'', s'')" "stepsn P n2 u (pc, s) (pc', s')" "n1 < n" "n2 < n"
unfolding stepst_def by (auto elim!: stepsc_stepsn)
show ?thesis
proof (cases "n1 ≥ n2")
case True
from stepsn_extend[OF *(2,1) this] ‹n1 < _› ‹n2 < _› ‹P pc'' = _› show ?thesis
unfolding stepst_def by (auto intro: stepsn_stepsc)
next
case False
with stepsn_extend[OF *(1,2)] ‹n1 < _› ‹n2 < _› ‹P pc'' = _› show ?thesis
unfolding stepst_def by (auto intro: stepsn_stepsc dest!: stepsn_halt)
qed
qed
lemma conv_P_conj_block'[intro]:
"is_conj_block' (conv_P P) pc pc'" if "is_conj_block' P pc pc'"
using that
apply induction
apply (rule is_conj_block'.intros(1))
apply (simp; fail)
apply (simp; fail)
apply (rule is_conj_block'.intros(2))
apply (simp; fail)
apply (frule is_conj_block'_pc_mono; force dest: is_conj_block'_len_prog)
apply (frule is_conj_block'_pc_mono; force dest: is_conj_block'_len_prog)
apply (frule is_conj_block'_pc_mono; force dest: is_conj_block'_len_prog)
apply (simp; fail)
apply (rule is_conj_block'.intros(3))
apply (simp; fail)
apply (frule is_conj_block'_pc_mono; force dest: is_conj_block'_len_prog)
apply (frule is_conj_block'_pc_mono; force dest: is_conj_block'_len_prog)
apply (frule is_conj_block'_pc_mono; force dest: is_conj_block'_len_prog)
apply (frule is_conj_block'_pc_mono; force dest: is_conj_block'_len_prog)
apply (simp; fail)
done
lemma conv_P_conj_block[intro]:
"is_conj_block (conv_P P) pc pc'" if "is_conj_block P pc pc'"
using that[unfolded is_conj_block_def]
apply safe
by (frule is_conj_block'_pc_mono; force dest: is_conj_block'_len_prog simp: is_conj_block_def)+
context
fixes P :: "int instrc option list"
and pc_s :: addr
and n :: nat
begin
private abbreviation "prog i ≡ if i < length P then P ! i else None"
lemma stepst_conv_P:
"stepst (λ i. if i < length (conv_P P) then conv_P P ! i else None) n u s s'" if
"stepst (conv_prog prog) n u s s'" using that unfolding stepst_def
apply safe
subgoal for pc a aa ab b z
apply rotate_tac
by (induction "conv_prog prog" n u s "(pc, a, aa, ab, b)" rule: stepsc.induct)
(auto split: if_split_asm)
by (auto split: if_split_asm)
lemma is_conj:
fixes u :: "nat ⇒ real"
defines "S ≡ steps_approx n P pc_s"
defines "pc_c ≡ Min {pc. ∃ ac. pc ∈ S ∧ P ! pc = Some (CEXP ac)}"
assumes "is_conj_block P pc_c (Max S)"
and "stepst (conv_prog prog) n u (pc_s, st, s, f, rs) (pc_t, st_t, s_t, True, rs_t)"
and "stepsc (conv_prog prog) n u (pc_s, st, s, f, rs) (pc', st', s', f', rs')"
and "P ! pc' = Some (CEXP ac)" "pc' < length P"
shows "(u ⊢⇩a conv_ac ac) ∧ pc_t = Max S"
proof -
from stepst_stepc_extend[OF assms(4,5)] have *:
"stepst (conv_prog prog) n u (pc', st', s', f', rs') (pc_t, st_t, s_t, True, rs_t)" .
from ‹stepsc _ _ _ _ _› ‹P ! pc' = _› ‹pc' < _› have "pc_c ≤ pc'" "pc' ≤ Max S"
unfolding pc_c_def S_def by (auto intro: stepsc_steps_approx Min_le Max_ge)
from is_conj_block_decomp[OF assms(3) ‹P ! pc' = _› this] have
"is_conj_block P pc' (Max S)" .
then have "is_conj_block (conv_P P) pc' (Max S)" by auto
from is_conj_block_is_conj[OF this _ stepst_conv_P[OF *]] ‹P ! pc' = _› ‹pc' < _›
show ?thesis
by auto
qed
lemma is_conj':
fixes u :: "nat ⇒ real"
defines "S ≡ steps_approx n P pc_s"
assumes "{pc. ∃ ac. pc ∈ S ∧ P ! pc = Some (CEXP ac)} = {}"
and "stepsc (conv_prog prog) n u (pc_s, st, s, f, rs) (pc', st', s', f', rs')"
and "P ! pc' = Some (CEXP ac)" "pc' < length P"
shows False
using stepsc_steps_approx[OF assms(3,5)] assms(4) assms(2) unfolding S_def by auto
definition
"check_conj_block pc pc' ≡
(case P ! pc of Some (CEXP ac) ⇒ True | _ ⇒ False) ∧ check_conj_block' P (pc + 1) = Some pc'
∨ (case P ! pc of Some (CEXP ac) ⇒ True | _ ⇒ False) ∧ P ! (pc + 1) = Some (INSTR instr.AND)
∧ check_conj_block' P (pc + 2) = Some pc'"
lemma check_conj_block:
"check_conj_block pc pc' ⟹ is_conj_block P pc pc'"
unfolding is_conj_block_alt_def check_conj_block_def
by (auto dest!: check_conj_block' simp del: check_conj_block'.simps)
definition
"conjunction_check ≡
let S = steps_approx n P pc_s; S' = {pc. ∃ ac. pc ∈ S ∧ P ! pc = Some (CEXP ac)} in
S' = {} ∨ check_conj_block (Min S') (Max S)
"
lemma conjunction_check_alt_def[code]:
"conjunction_check =
(
let
S = steps_approx n P pc_s;
S' = {pc. pc ∈ S ∧ (case P ! pc of Some (CEXP ac) ⇒ True | _ ⇒ False)}
in
S' = {} ∨ check_conj_block (Min S') (Max S)
)
"
proof -
let ?S = "steps_approx n P pc_s"
have "
{pc. pc ∈ ?S ∧ (case P ! pc of Some (CEXP ac) ⇒ True | _ ⇒ False)}
= {pc. ∃ ac. pc ∈ ?S ∧ P ! pc = Some (CEXP ac)}
" by safe (auto split: option.splits instrc.splits)
show ?thesis unfolding conjunction_check_def Let_def ‹_ = _› ..
qed
lemma conjunction_check:
fixes u :: "nat ⇒ real"
assumes "conjunction_check"
and "stepst (conv_prog prog) n u (pc_s, st, s, f, rs) (pc_t, st_t, s_t, True, rs_t)"
and "stepsc (conv_prog prog) n u (pc_s, st, s, f, rs) (pc', st', s', f', rs')"
and "P ! pc' = Some (CEXP ac)" "pc' < length P"
shows "u ⊢⇩a conv_ac ac"
using assms
unfolding conjunction_check_def Let_def
apply -
apply (erule disjE)
apply (drule is_conj'; simp)
apply (drule check_conj_block)
apply (subst is_conj; simp)
done
end
end