Theory LevellistProof
section ‹Proof of Procedure Levellist›
theory LevellistProof imports ProcedureSpecs Simpl.HeapList begin
hide_const (open) DistinctTreeProver.set_of tree.Node tree.Tip
lemma (in Levellist_impl) Levellist_modifies:
shows "∀σ. Γ⊢{σ} ´levellist :== PROC Levellist (´p, ´m, ´levellist)
{t. t may_only_modify_globals σ in [mark,next]}"
apply (hoare_rule HoarePartial.ProcRec1)
apply (vcg spec=modifies)
done
lemma all_stop_cong: "(∀x. P x) = (∀x. P x)"
by simp
lemma Dag_RefD:
"⟦Dag p l r t; p≠Null⟧ ⟹
∃lt rt. t=Node lt p rt ∧ Dag (l p) l r lt ∧ Dag (r p) l r rt"
by simp
lemma Dag_unique_ex_conjI:
"⟦Dag p l r t; P t⟧ ⟹ (∃t. Dag p l r t ∧ P t)"
by simp
lemma dag_Null [simp]: "dag Null l r = Tip"
by (simp add: dag_def)
definition first:: "ref list ⇒ ref" where
"first ps = (case ps of [] ⇒ Null | (p#rs) ⇒ p)"
lemma first_simps [simp]:
"first [] = Null"
"first (r#rs) = r"
by (simp_all add: first_def)
definition Levellist:: "ref list ⇒ (ref ⇒ ref) ⇒ (ref list list) ⇒ bool" where
"Levellist hds next ll ⟷ (map first ll = hds) ∧
(∀i < length hds. List (hds ! i) next (ll!i))"
lemma Levellist_unique:
assumes ll: "Levellist hds next ll"
assumes ll': "Levellist hds next ll'"
shows "ll=ll'"
proof -
from ll have "length ll = length hds"
by (clarsimp simp add: Levellist_def)
moreover
from ll' have "length ll' = length hds"
by (clarsimp simp add: Levellist_def)
ultimately have leq: "length ll = length ll'" by simp
show ?thesis
proof (rule nth_equalityI [OF leq, rule_format])
fix i
assume "i < length ll"
with ll ll'
show "ll!i = ll'!i"
apply (clarsimp simp add: Levellist_def)
apply (erule_tac x=i in allE)
apply (erule_tac x=i in allE)
apply simp
by (erule List_unique)
qed
qed
lemma Levellist_unique_ex_conj_simp [simp]:
"Levellist hds next ll ⟹ (∃ll. Levellist hds next ll ∧ P ll) = P ll"
by (auto dest: Levellist_unique)
lemma in_set_concat_idx:
"x ∈ set (concat xss) ⟹ ∃i < length xss. x ∈ set (xss!i)"
apply (induct xss)
apply simp
apply clarsimp
apply (erule disjE)
apply (rule_tac x=0 in exI)
apply simp
apply auto
done
definition wf_levellist :: "dag ⇒ ref list list ⇒ ref list list ⇒
(ref ⇒ nat) ⇒ bool" where
"wf_levellist t levellist_old levellist_new var =
(case t of Tip ⇒ levellist_old = levellist_new
| (Node lt p rt) ⇒
(∀ q. q ∈ set_of t ⟶ q ∈ set (levellist_new ! (var q))) ∧
(∀ i ≤ var p. (∃ prx. (levellist_new ! i) = prx@(levellist_old ! i)
∧ (∀ pt ∈ set prx. pt ∈ set_of t ∧ var pt = i))) ∧
(∀ i. (var p) < i ⟶ (levellist_new ! i) = (levellist_old ! i)) ∧
(length levellist_new = length levellist_old))"
lemma wf_levellist_subset:
assumes wf_ll: "wf_levellist t ll ll' var"
shows "set (concat ll') ⊆ set (concat ll) ∪ set_of t"
proof (cases t)
case Tip with wf_ll show ?thesis by (simp add: wf_levellist_def)
next
case (Node lt p rt)
show ?thesis
proof -
{
fix n
assume "n ∈ set (concat ll')"
from in_set_concat_idx [OF this]
obtain i where i_bound: "i < length ll'" and n_in: "n ∈ set (ll' ! i)"
by blast
have "n ∈ set (concat ll) ∪ set_of t"
proof (cases "i ≤ var p")
case True
with wf_ll obtain prx where
ll'_ll: "ll' ! i = prx @ ll ! i" and
prx: "∀pt ∈ set prx. pt ∈ set_of t" and
leq: "length ll' = length ll"
apply (clarsimp simp add: wf_levellist_def Node)
apply (erule_tac x="i" in allE)
apply clarsimp
done
show ?thesis
proof (cases "n ∈ set prx")
case True
with prx have "n ∈ set_of t"
by simp
thus ?thesis by simp
next
case False
with n_in ll'_ll
have "n ∈ set (ll ! i)"
by simp
with i_bound leq
have "n ∈ set (concat ll)"
by auto
thus ?thesis by simp
qed
next
case False
with wf_ll obtain "ll'!i = ll!i" "length ll' = length ll"
by (auto simp add: wf_levellist_def Node)
with n_in i_bound
have "n ∈ set (concat ll)"
by auto
thus ?thesis by simp
qed
}
thus ?thesis by auto
qed
qed
lemma Levellist_ext_to_all: "((∃ll. Levellist hds next ll ∧ P ll) ⟶ Q)
=
(∀ll. Levellist hds next ll ∧ P ll ⟶ Q)"
apply blast
done
lemma Levellist_length: "Levellist hds p ll ⟹ length ll = length hds"
by (auto simp add: Levellist_def)
lemma map_update:
"⋀i. i < length xss ⟹ map f (xss[i := xs]) = (map f xss) [i := f xs]"
apply (induct xss)
apply simp
apply (case_tac i)
apply simp
apply simp
done
lemma (in Levellist_impl) Levellist_spec_total':
shows "∀ll σ t. Γ,Θ⊢⇩t
⦃σ. Dag ´p ´low ´high t ∧ (´p ≠ Null ⟶ (´p→´var) < length ´levellist) ∧
ordered t ´var ∧ Levellist ´levellist ´next ll ∧
(∀n ∈ set_of t.
(if ´mark n = ´m
then n ∈ set (ll ! ´var n) ∧
(∀nt p. Dag n ´low ´high nt ∧ p ∈ set_of nt
⟶ ´mark p = ´m)
else n ∉ set (concat ll)))⦄
´levellist :== PROC Levellist (´p, ´m, ´levellist)
⦃∃ll'. Levellist ´levellist ´next ll' ∧ wf_levellist t ll ll' ⇗σ⇖var ∧
wf_marking t ⇗σ⇖mark ´mark ⇗σ⇖m ∧
(∀p. p ∉ set_of t ⟶ ⇗σ⇖next p = ´next p)
⦄"
apply (hoare_rule HoareTotal.ProcRec1
[where r="measure (λ(s,p). size (dag ⇗s⇖p ⇗s⇖low ⇗s⇖high))"])
apply vcg
apply (rule conjI)
apply clarify
apply (rule conjI)
apply clarify
apply (clarsimp simp del: BinDag.set_of.simps split del: if_split)
defer
apply (rule impI)
apply (clarsimp simp del: BinDag.set_of.simps split del: if_split)
defer
apply (clarsimp simp add: wf_levellist_def wf_marking_def)
apply (simp only: Levellist_ext_to_all )
proof -
fix ll var low high mark "next" nexta p levellist m lt rt
assume pnN: "p ≠ Null"
assume mark_p: "mark p = (¬ m)"
assume lt: "Dag (low p) low high lt"
assume rt: "Dag (high p) low high rt"
from pnN lt rt have Dag_p: "Dag p low high (Node lt p rt)" by simp
from Dag_p rt
have size_rt_dec: "size (dag (high p) low high) < size (dag p low high)"
by (simp only: Dag_dag) simp
from Dag_p lt
have size_lt_dec: "size (dag (low p) low high) < size (dag p low high)"
by (simp only: Dag_dag) simp
assume ll: "Levellist levellist next ll"
assume marked_child_ll:
"∀n ∈ set_of (Node lt p rt).
if mark n = m
then n ∈ set (ll ! var n) ∧
(∀nt p. Dag n low high nt ∧ p ∈ set_of nt ⟶ mark p = m)
else n ∉ set (concat ll)"
with mark_p have p_notin_ll: "p ∉ set (concat ll)"
by auto
assume varsll': "var p < length levellist"
with ll have varsll: "var p < length ll"
by (simp add: Levellist_length)
assume orderedt: "ordered (Node lt p rt) var"
show "(low p ≠ Null ⟶ var (low p) < length levellist) ∧
ordered lt var ∧
(∀n ∈ set_of lt.
if mark n = m
then n ∈ set (ll ! var n) ∧
(∀nt p. Dag n low high nt ∧ p ∈ set_of nt ⟶ mark p = m)
else n ∉ set (concat ll)) ∧
size (dag (low p) low high) < size (dag p low high) ∧
(∀marka nexta levellist lla.
Levellist levellist nexta lla ∧
wf_levellist lt ll lla var ∧ wf_marking lt mark marka m ∧
(∀p. p ∉ set_of lt ⟶ next p = nexta p)⟶
(high p ≠ Null ⟶ var (high p) < length levellist) ∧
ordered rt var ∧
(∃lla. Levellist levellist nexta lla ∧
(∀n ∈ set_of rt.
if marka n = m
then n ∈ set (lla ! var n) ∧
(∀nt p. Dag n low high nt ∧ p ∈ set_of nt ⟶
marka p = m)
else n ∉ set (concat lla)) ∧
size (dag (high p) low high) < size (dag p low high) ∧
(∀markb nextb levellist llb.
Levellist levellist nextb llb ∧
wf_levellist rt lla llb var ∧
wf_marking rt marka markb m ∧
(∀p. p ∉ set_of rt ⟶ nexta p = nextb p) ⟶
(∃ll'. Levellist (levellist[var p := p])
(nextb(p := levellist ! var p)) ll' ∧
wf_levellist (Node lt p rt) ll ll' var ∧
wf_marking (Node lt p rt) mark (markb(p := m)) m ∧
(∀pa. pa ∉ set_of (Node lt p rt) ⟶
next pa =
(if pa = p then levellist ! var p
else nextb pa))))))"
proof (cases "lt")
case Tip
note lt_Tip = this
show ?thesis
proof (cases "rt")
case Tip
show ?thesis
using size_rt_dec Tip lt_Tip Tip lt rt
apply clarsimp
subgoal premises prems for marka nexta levellista lla markb nextb levellistb llb
proof -
have lla: "Levellist levellista nexta lla" by fact
have llb: "Levellist levellistb nextb llb" by fact
have wfll_lt: "wf_levellist Tip ll lla var"
"wf_marking Tip mark marka m" by fact+
then have ll_lla: "ll = lla"
by (simp add: wf_levellist_def)
moreover
with wfll_lt lt_Tip lt have "marka = mark"
by (simp add: wf_marking_def)
moreover
have wfll_rt:"wf_levellist Tip lla llb var"
"wf_marking Tip marka markb m" by fact+
then have lla_llb: "lla = llb"
by (simp add: wf_levellist_def)
moreover
with wfll_rt Tip rt have "markb = marka"
by (simp add: wf_marking_def)
moreover
from varsll llb ll_lla lla_llb
obtain "var p < length levellistb" "var p < length llb"
by (simp add: Levellist_length)
with llb pnN
have llc: "Levellist (levellistb[var p := p]) (nextb(p := levellistb ! var p))
(llb[var p := p # llb ! var p])"
apply (clarsimp simp add: Levellist_def map_update)
apply (erule_tac x=i in allE)
apply clarsimp
apply (subgoal_tac "p ∉ set (llb ! i) ")
prefer 2
using p_notin_ll ll_lla lla_llb
apply simp
apply (case_tac "i=var p")
apply simp
apply simp
done
ultimately
show ?thesis
using lt_Tip Tip varsll
apply (clarsimp simp add: wf_levellist_def wf_marking_def)
proof -
fix i
assume varsllb: "var p < length llb"
assume "i ≤ var p"
show "∃prx. llb[var p := p#llb!var p]!i = prx @ llb!i ∧
(∀pt∈set prx. pt = p ∧ var pt = i)"
proof (cases "i = var p")
case True
with pnN lt rt varsllb lt_Tip Tip show ?thesis
apply -
apply (rule_tac x="[p]" in exI)
apply (simp add: subdag_eq_def)
done
next
assume "i ≠ var p"
with varsllb show ?thesis
apply -
apply (rule_tac x="[]" in exI)
apply (simp add: subdag_eq_def)
done
qed
qed
qed
done
next
case (Node dag1 a dag2)
have rt_node: "rt = Node dag1 a dag2" by fact
with rt have high_p: "high p = a"
by simp
have s: "⋀nexta. (∀p. next p = nexta p) = (next = nexta)"
by auto
show ?thesis
using size_rt_dec size_lt_dec rt_node lt_Tip Tip lt rt
apply (clarsimp simp del: set_of_Node split del: if_split simp add: s)
subgoal premises prems for marka levellista lla
proof -
have lla: "Levellist levellista next lla" by fact
have wfll_lt:"wf_levellist Tip ll lla var"
"wf_marking Tip mark marka m" by fact+
from this have ll_lla: "ll = lla"
by (simp add: wf_levellist_def)
moreover
from wfll_lt lt_Tip lt have marklrec: "marka = mark"
by (simp add: wf_marking_def)
from orderedt varsll lla ll_lla rt_node lt_Tip high_p
have var_highp_bound: "var (high p) < length levellista"
by (auto simp add: Levellist_length)
from orderedt high_p rt_node lt_Tip
have ordered_rt: "ordered (Node dag1 (high p) dag2) var"
by simp
from high_p marklrec marked_child_ll lt rt lt_Tip rt_node ll_lla
have mark_rt: "(∀n∈set_of (Node dag1 (high p) dag2).
if marka n = m
then n ∈ set (lla ! var n) ∧
(∀nt p. Dag n low high nt ∧ p ∈ set_of nt ⟶ marka p = m)
else n ∉ set (concat lla))"
apply (simp only: BinDag.set_of.simps)
apply clarify
apply (drule_tac x=n in bspec)
apply blast
apply assumption
done
show ?thesis
apply (rule conjI)
apply (rule var_highp_bound)
apply (rule conjI)
apply (rule ordered_rt)
apply (rule conjI)
apply (rule mark_rt)
apply clarify
apply clarsimp
subgoal premises prems for markb nextb levellistb llb
proof -
have llb: "Levellist levellistb nextb llb" by fact
have wfll_rt: "wf_levellist (Node dag1 (high p) dag2) lla llb var" by fact
have wfmarking_rt: "wf_marking (Node dag1 (high p) dag2) marka markb m" by fact
from wfll_rt varsll llb ll_lla
obtain var_p_bounds: "var p < length levellistb" "var p < length llb"
by (simp add: Levellist_length wf_levellist_def)
with p_notin_ll ll_lla wfll_rt
have p_notin_llb: "∀i < length llb. p ∉ set (llb ! i)"
apply -
apply (intro allI impI)
apply (clarsimp simp add: wf_levellist_def)
apply (case_tac "i ≤ var (high p)")
apply (drule_tac x=i in spec)
using orderedt rt_node lt_Tip high_p
apply clarsimp
apply (drule_tac x=i in spec)
apply (drule_tac x=i in spec)
apply clarsimp
done
with llb pnN var_p_bounds
have llc: "Levellist (levellistb[var p := p])
(nextb(p := levellistb ! var p))
(llb[var p := p # llb ! var p])"
apply (clarsimp simp add: Levellist_def map_update)
apply (erule_tac x=i in allE)
apply (erule_tac x=i in allE)
apply clarsimp
apply (case_tac "i=var p")
apply simp
apply simp
done
then show ?thesis
apply simp
using wfll_rt wfmarking_rt
lt_Tip rt_node varsll orderedt lt rt pnN ll_lla marklrec
apply (clarsimp simp add: wf_levellist_def wf_marking_def)
apply (intro conjI)
apply (rule allI)
apply (rule conjI)
apply (erule_tac x="q" in allE)
apply (case_tac "var p = var q")
apply fastforce
apply fastforce
apply (case_tac "var p = var q")
apply hypsubst_thin
apply fastforce
apply fastforce
apply (rule allI)
apply (rotate_tac 4)
apply (erule_tac x="i" in allE)
apply (case_tac "i=var p")
apply simp
apply (case_tac "var (high p) < i")
apply simp
apply simp
apply (erule exE)
apply (rule_tac x="prx" in exI)
apply (intro conjI)
apply simp
apply clarify
apply (rotate_tac 15)
apply (erule_tac x="pt" in ballE)
apply fastforce
apply fastforce
done
qed
done
qed
done
qed
next
case (Node llt l rlt)
have lt_Node: "lt = Node llt l rlt" by fact
from orderedt lt varsll' lt_Node
obtain ordered_lt:
"ordered lt var" "(low p ≠ Null ⟶ var (low p) < length levellist)"
by (cases rt) auto
from lt lt_Node marked_child_ll
have mark_lt: "∀n∈set_of lt.
if mark n = m
then n ∈ set (ll ! var n) ∧
(∀nt p. Dag n low high nt ∧ p ∈ set_of nt ⟶ mark p = m)
else n ∉ set (concat ll)"
apply (simp only: BinDag.set_of.simps)
apply clarify
apply (drule_tac x=n in bspec)
apply blast
apply assumption
done
show ?thesis
apply (intro conjI ordered_lt mark_lt size_lt_dec)
apply (clarify)
apply (simp add: size_rt_dec split del: if_split)
apply (simp only: Levellist_ext_to_all)
subgoal premises prems for marka nexta levellista lla
proof -
have lla: "Levellist levellista nexta lla" by fact
have wfll_lt: "wf_levellist lt ll lla var" by fact
have wfmarking_lt:"wf_marking lt mark marka m" by fact
from wfll_lt lt_Node
have lla_eq_ll: "length lla = length ll"
by (simp add: wf_levellist_def)
with ll lla have lla_eq_ll': "length levellista = length levellist"
by (simp add: Levellist_length)
with orderedt rt lt_Node lt varsll'
obtain ordered_rt:
"ordered rt var" "(high p ≠ Null ⟶ var (high p) < length levellista)"
by (cases rt) auto
from wfll_lt lt_Node
have nodes_in_lla: "∀ q. q ∈ set_of lt ⟶ q ∈ set (lla ! (q→var))"
by (simp add: wf_levellist_def)
from wfll_lt lt_Node lt
have lla_st: "(∀i ≤ (low p)→var.
(∃prx. (lla ! i) = prx@(ll ! i) ∧
(∀pt ∈ set prx. pt ∈ set_of lt ∧ pt→var = i)))"
by (simp add: wf_levellist_def)
from wfll_lt lt_Node lt
have lla_nc: "∀i. ((low p)→var) < i ⟶ (lla ! i) = (ll ! i)"
by (simp add: wf_levellist_def)
from wfmarking_lt lt_Node lt
have mot_nc: "∀ n. n ∉ set_of lt ⟶ mark n = marka n"
by (simp add: wf_marking_def)
from wfmarking_lt lt_Node lt
have mit_marked: "∀n. n ∈ set_of lt ⟶ marka n = m"
by (simp add: wf_marking_def)
from marked_child_ll nodes_in_lla mot_nc mit_marked lla_st
have mark_rt: "∀n∈set_of rt.
if marka n = m
then n ∈ set (lla ! var n) ∧
(∀nt p. Dag n low high nt ∧ p ∈ set_of nt ⟶ marka p = m)
else n ∉ set (concat lla)"
apply -
apply (rule ballI)
apply (drule_tac x="n" in bspec)
apply (simp)
proof -
fix n
assume nodes_in_lla: "∀q. q ∈ set_of lt ⟶ q ∈ set (lla ! var q)"
assume mot_nc: "∀n. n ∉ set_of lt ⟶ mark n = marka n"
assume mit_marked: "∀n. n ∈ set_of lt ⟶ marka n = m"
assume marked_child_ll: "if mark n = m
then n ∈ set (ll ! var n) ∧
(∀nt p. Dag n low high nt ∧ p ∈ set_of nt ⟶ mark p = m)
else n ∉ set (concat ll)"
assume lla_st: "∀i≤var (low p).
∃prx. lla ! i = prx @ ll ! i ∧
(∀pt∈set prx. pt ∈ set_of lt ∧ var pt = i)"
assume n_in_rt: " n ∈ set_of rt"
show n_in_lla_marked: "if marka n = m
then n ∈ set (lla ! var n) ∧
(∀nt p. Dag n low high nt ∧ p ∈ set_of nt ⟶ marka p = m)
else n ∉ set (concat lla)"
proof (cases "n ∈ set_of lt")
case True
from True nodes_in_lla have n_in_ll: "n ∈ set (lla ! var n)"
by simp
moreover
from True wfmarking_lt
have "marka n = m"
apply (cases lt)
apply (auto simp add: wf_marking_def)
done
moreover
{
fix nt p
assume "Dag n low high nt"
with lt True have subset_nt_lt: "set_of nt ⊆ set_of lt"
by (rule dag_setof_subsetD)
moreover assume " p ∈ set_of nt"
ultimately have "p ∈ set_of lt"
by blast
with mit_marked have " marka p = m"
by simp
}
ultimately show ?thesis
using n_in_rt
apply clarsimp
done
next
assume n_notin_lt: "n ∉ set_of lt"
show ?thesis
proof (cases "marka n = m")
case True
from n_notin_lt mot_nc have marka_eq_mark: "mark n = marka n"
by simp
from marka_eq_mark True have n_marked: "mark n = m"
by simp
from rt n_in_rt have nnN: "n ≠ Null"
apply -
apply (rule set_of_nn [rule_format])
apply fastforce
apply assumption
done
from marked_child_ll n_in_rt marka_eq_mark nnN n_marked
have n_in_ll: "n ∈ set (ll ! var n)"
by fastforce
from marked_child_ll n_in_rt marka_eq_mark nnN n_marked lt rt
have nt_mark: "∀nt p. Dag n low high nt ∧ p ∈ set_of nt ⟶ mark p = m"
by simp
from nodes_in_lla n_in_ll lla_st
have n_in_lla: "n ∈ set (lla ! var n)"
proof (cases "var (low p) < (var n)")
case True
with lla_nc have "(lla ! var n) = (ll ! var n)"
by fastforce
with n_in_ll show ?thesis
by fastforce
next
assume varnslp: " ¬ var (low p) < var n"
with lla_st
have ll_in_lla: "∃prx. lla ! (var n) = prx @ ll ! (var n)"
apply -
apply (erule_tac x="var n" in allE)
apply fastforce
done
with n_in_ll show ?thesis
by fastforce
qed
{
fix nt pt
assume nt_Dag: "Dag n low high nt"
assume pt_in_nt: "pt ∈ set_of nt"
have " marka pt = m"
proof (cases "pt ∈ set_of lt")
case True
with mit_marked show ?thesis
by fastforce
next
assume pt_notin_lt: " pt ∉ set_of lt"
with mot_nc have "mark pt = marka pt"
by fastforce
with nt_mark nt_Dag pt_in_nt show ?thesis
by fastforce
qed
}
then have nt_marka:
"∀nt pt. Dag n low high nt ∧ pt ∈ set_of nt ⟶ marka pt = m"
by fastforce
with n_in_lla nt_marka True show ?thesis
by fastforce
next
case False
note n_not_marka = this
with wfmarking_lt n_notin_lt
have "mark n ≠ m"
by (simp add: wf_marking_def lt_Node)
with marked_child_ll
have n_notin_ll: "n ∉ set (concat ll)"
by simp
show ?thesis
proof (cases "n ∈ set (concat lla)")
case False with n_not_marka show ?thesis by simp
next
case True
with wf_levellist_subset [OF wfll_lt] n_notin_ll
have "n ∈ set_of lt"
by blast
with n_notin_lt have False by simp
thus ?thesis ..
qed
qed
qed
qed
show ?thesis
apply (intro conjI ordered_rt mark_rt)
apply clarify
subgoal premises prems for markb nextb levellistb llb
proof -
have llb: "Levellist levellistb nextb llb" by fact
have wfll_rt: "wf_levellist rt lla llb var" by fact
have wfmarking_rt: "wf_marking rt marka markb m" by fact
show ?thesis
proof (cases rt)
case Tip
from wfll_rt Tip have lla_llb: "lla = llb"
by (simp add: wf_levellist_def)
moreover
from wfmarking_rt Tip rt have "markb = marka"
by (simp add: wf_marking_def)
moreover
from wfll_lt varsll llb lla_llb
obtain var_p_bounds: "var p < length levellistb" "var p < length llb"
by (simp add: Levellist_length wf_levellist_def lt_Node Tip)
with p_notin_ll lla_llb wfll_lt
have p_notin_llb: "∀i < length llb. p ∉ set (llb ! i)"
apply -
apply (intro allI impI)
apply (clarsimp simp add: wf_levellist_def lt_Node)
apply (case_tac "i ≤ var l")
apply (drule_tac x=i in spec)
using orderedt Tip lt_Node
apply clarsimp
apply (drule_tac x=i in spec)
apply (drule_tac x=i in spec)
apply clarsimp
done
with llb pnN var_p_bounds
have llc: "Levellist (levellistb[var p := p])
(nextb(p := levellistb ! var p))
(llb[var p := p # llb ! var p])"
apply (clarsimp simp add: Levellist_def map_update)
apply (erule_tac x=i in allE)
apply (erule_tac x=i in allE)
apply clarsimp
apply (case_tac "i=var p")
apply simp
apply simp
done
ultimately show ?thesis
using Tip lt_Node varsll orderedt lt rt pnN wfll_lt wfmarking_lt
apply (clarsimp simp add: wf_levellist_def wf_marking_def)
apply (intro conjI)
apply (rule allI)
apply (rule conjI)
apply (erule_tac x="q" in allE)
apply (case_tac "var p = var q")
apply fastforce
apply fastforce
apply (case_tac "var p = var q")
apply hypsubst_thin
apply fastforce
apply fastforce
apply (rule allI)
apply (rotate_tac 4)
apply (erule_tac x="i" in allE)
apply (case_tac "i=var p")
apply simp
apply (case_tac "var (low p) < i")
apply simp
apply simp
apply (erule exE)
apply (rule_tac x="prx" in exI)
apply (intro conjI)
apply simp
apply clarify
apply (rotate_tac 15)
apply (erule_tac x="pt" in ballE)
apply fastforce
apply fastforce
done
next
case (Node lrt r rrt)
have rt_Node: "rt = Node lrt r rrt" by fact
from wfll_rt rt_Node
have llb_eq_lla: "length llb = length lla"
by (simp add: wf_levellist_def)
with llb lla
have llb_eq_lla': "length levellistb = length levellista"
by (simp add: Levellist_length)
from wfll_rt rt_Node
have nodes_in_llb: "∀q. q ∈ set_of rt ⟶ q ∈ set (llb ! (q→var))"
by (simp add: wf_levellist_def)
from wfll_rt rt_Node rt
have llb_st: "(∀ i ≤ (high p)→var.
(∃ prx. (llb ! i) = prx@(lla ! i) ∧
(∀pt ∈ set prx. pt ∈ set_of rt ∧ pt→var = i)))"
by (simp add: wf_levellist_def)
from wfll_rt rt_Node rt
have llb_nc:
"∀i. ((high p)→var) < i ⟶ (llb ! i) = (lla ! i)"
by (simp add: wf_levellist_def)
from wfmarking_rt rt_Node rt
have mort_nc: "∀n. n ∉ set_of rt ⟶ marka n = markb n"
by (simp add: wf_marking_def)
from wfmarking_rt rt_Node rt
have mirt_marked: "∀n. n ∈ set_of rt ⟶ markb n = m"
by (simp add: wf_marking_def)
with p_notin_ll wfll_rt wfll_lt
have p_notin_llb: "∀i < length llb. p ∉ set (llb ! i)"
apply -
apply (intro allI impI)
apply (clarsimp simp add: wf_levellist_def lt_Node rt_Node)
apply (case_tac "i ≤ var r")
apply (drule_tac x=i in spec)
using orderedt rt_Node lt_Node
apply clarsimp
apply (erule disjE)
apply clarsimp
apply (case_tac "i ≤ var l")
apply (drule_tac x=i in spec)
apply clarsimp
apply clarsimp
apply (subgoal_tac "llb ! i = lla ! i")
prefer 2
apply clarsimp
apply (case_tac "i ≤ var l")
apply (drule_tac x=i in spec, erule impE, assumption)
apply clarsimp
using orderedt rt_Node lt_Node
apply clarsimp
apply clarsimp
done
from wfll_lt wfll_rt varsll lla llb
obtain var_p_bounds: "var p < length levellistb" "var p < length llb"
by (simp add: Levellist_length wf_levellist_def lt_Node rt_Node)
with p_notin_llb llb pnN var_p_bounds
have llc: "Levellist (levellistb[var p := p])
(nextb(p := levellistb ! var p))
(llb[var p := p # llb ! var p])"
apply (clarsimp simp add: Levellist_def map_update)
apply (erule_tac x=i in allE)
apply (erule_tac x=i in allE)
apply clarsimp
apply (case_tac "i=var p")
apply simp
apply simp
done
then show ?thesis
proof (clarsimp)
show "wf_levellist (Node lt p rt) ll (llb[var p := p#llb ! var p]) var ∧
wf_marking (Node lt p rt) mark (markb(p := m)) m"
proof -
have nodes_in_upllb: "∀ q. q ∈ set_of (Node lt p rt)
⟶ q ∈ set (llb[var p :=p # llb ! var p] ! (var q))"
apply -
apply (rule allI)
apply (rule impI)
proof -
fix q
assume q_in_t: "q ∈ set_of (Node lt p rt)"
show q_in_upllb:
"q ∈ set (llb[var p :=p # llb ! var p] ! (var q))"
proof (cases "q ∈ set_of rt")
case True
with nodes_in_llb have q_in_llb: "q ∈ set (llb ! (var q))"
by fastforce
from orderedt rt_Node lt_Node lt rt
have ordered_rt: "ordered rt var"
by fastforce
from True rt ordered_rt rt_Node lt lt_Node have "var q ≤ var r"
apply -
apply (drule subnodes_ordered)
apply fastforce
apply fastforce
apply fastforce
done
with orderedt rt lt rt_Node lt_Node have "var q < var p"
by fastforce
then have
"llb[var p :=p#llb ! var p] ! var q =
llb ! var q"
by fastforce
with q_in_llb show ?thesis
by fastforce
next
assume q_notin_rt: "q ∉ set_of rt"
show "q ∈ set (llb[var p :=p # llb ! var p] ! var q)"
proof (cases "q ∈ set_of lt")
case True
assume q_in_lt: "q ∈ set_of lt"
with nodes_in_lla have q_in_lla: "q ∈ set (lla ! (var q))"
by fastforce
from orderedt rt_Node lt_Node lt rt
have ordered_lt: "ordered lt var"
by fastforce
from q_in_lt lt ordered_lt rt_Node rt lt_Node
have "var q ≤ var l"
apply -
apply (drule subnodes_ordered)
apply fastforce
apply fastforce
apply fastforce
done
with orderedt rt lt rt_Node lt_Node have qsp: "var q < var p"
by fastforce
then show ?thesis
proof (cases "var q ≤ var (high p)")
case True
with llb_st
have "∃prx. (llb ! (var q)) = prx@(lla ! (var q))"
by fastforce
with nodes_in_lla q_in_lla
have q_in_llb: "q ∈ set (llb ! (var q))"
by fastforce
from qsp
have "llb[var p :=p#llb ! var p]!var q =
llb ! (var q)"
by fastforce
with q_in_llb show ?thesis
by fastforce
next
assume "¬ var q ≤ var (high p)"
with llb_nc have "llb ! (var q) = lla ! (var q)"
by fastforce
with q_in_lla have q_in_llb: "q ∈ set (llb ! (var q))"
by fastforce
from qsp have
"llb[var p :=p # llb ! var p] ! var q = llb ! (var q)"
by fastforce
with q_in_llb show ?thesis
by fastforce
qed
next
assume q_notin_lt: "q ∉ set_of lt"
with q_notin_rt rt lt rt_Node lt_Node q_in_t have qp: "q = p"
by fastforce
with varsll lla_eq_ll llb_eq_lla have "var p < length llb"
by fastforce
with qp show ?thesis
by simp
qed
qed
qed
have prx_ll_st: "∀i ≤ var p.
(∃prx. llb[var p :=p#llb!var p]!i = prx@(ll!i) ∧
(∀pt ∈ set prx. pt ∈ set_of (Node lt p rt) ∧ var pt = i))"
apply -
apply (rule allI)
apply (rule impI)
proof -
fix i
assume isep: "i ≤ var p"
show "∃prx. llb[var p :=p#llb!var p]!i = prx@ll!i ∧
(∀pt∈set prx. pt ∈ set_of (Node lt p rt) ∧ var pt = i)"
proof (cases "i = var p")
case True
with orderedt lt lt_Node rt rt_Node
have lpsp: "var (low p) < var p"
by fastforce
with orderedt lt lt_Node rt rt_Node
have hpsp: "var (high p) < var p"
by fastforce
with lpsp lla_nc
have llall: "lla ! var p = ll ! var p"
by fastforce
with hpsp llb_nc have "llb ! var p = ll ! var p"
by fastforce
with llb_eq_lla lla_eq_ll isep True varsll lt rt show ?thesis
apply -
apply (rule_tac x="[p]" in exI)
apply (rule conjI)
apply simp
apply (rule ballI)
apply fastforce
done
next
assume inp: " i ≠ var p"
show ?thesis
proof (cases "var (low p) < i")
case True
with lla_nc have llall: "lla ! i = ll ! i"
by fastforce
assume vpsi: "var (low p) < i"
show ?thesis
proof (cases "var (high p) < i")
case True
with llall llb_nc have "llb ! i = ll ! i"
by fastforce
with inp True vpsi varsll lt rt show ?thesis
apply -
apply (rule_tac x="[]" in exI)
apply (rule conjI)
apply simp
apply (rule ballI)
apply fastforce
done
next
assume isehp: " ¬ var (high p) < i"
with vpsi lla_nc have lla_ll: "lla ! i = ll ! i"
by fastforce
with isehp llb_st
have prx_lla: "∃prx. llb ! i = prx @ lla ! i ∧
(∀pt∈set prx. pt ∈ set_of rt ∧ var pt = i)"
apply -
apply (erule_tac x="i" in allE)
apply simp
done
with lla_ll inp rt show ?thesis
apply -
apply (erule exE)
apply (rule_tac x="prx" in exI)
apply simp
done
qed
next
assume iselp: "¬ var (low p) < i"
show ?thesis
proof (cases "var (high p) < i")
case True
with llb_nc have llb_ll: "llb ! i = lla ! i"
by fastforce
with iselp lla_st
have prx_ll: "∃prx. lla ! i = prx @ ll ! i ∧
(∀pt∈set prx. pt ∈ set_of lt ∧ var pt = i)"
apply -
apply (erule_tac x="i" in allE)
apply simp
done
with llb_ll inp lt show ?thesis
apply -
apply (erule exE)
apply (rule_tac x="prx" in exI)
apply simp
done
next
assume isehp: " ¬ var (high p) < i"
from iselp lla_st
have prxl: "∃prx. lla ! i = prx @ ll ! i ∧
(∀pt∈set prx. pt ∈ set_of lt ∧ var pt = i)"
by fastforce
from isehp llb_st
have prxh: "∃prx. llb ! i = prx @ lla ! i ∧
(∀pt∈set prx. pt ∈ set_of rt ∧ var pt = i)"
by fastforce
with prxl inp lt pnN rt show ?thesis
apply -
apply (elim exE)
apply (rule_tac x="prxa @ prx" in exI)
apply simp
apply (elim conjE)
apply fastforce
done
qed
qed
qed
qed
have big_Nodes_nc: "∀i. (p->var) < i
⟶ (llb[var p :=p # llb ! var p]) ! i = ll ! i"
apply -
apply (rule allI)
apply (rule impI)
proof -
fix i
assume psi: "var p < i"
with orderedt lt rt lt_Node rt_Node have lpsi: "var (low p) < i"
by fastforce
with lla_nc have lla_ll: "lla ! i = ll ! i"
by fastforce
from psi orderedt lt rt lt_Node rt_Node have hpsi: "var (high p) < i"
by fastforce
with llb_nc have llb_lla: "llb ! i = lla ! i"
by fastforce
from psi
have upllb_llb: "llb[var p :=p#llb!var p]!i = llb!i"
by fastforce
from upllb_llb llb_lla lla_ll
show "llb[var p :=p # llb ! var p] ! i = ll ! i"
by fastforce
qed
from lla_eq_ll llb_eq_lla
have length_eq: "length (llb[var p :=p # llb ! var p]) = length ll"
by fastforce
from length_eq big_Nodes_nc prx_ll_st nodes_in_upllb
have wf_ll_upllb:
"wf_levellist (Node lt p rt) ll (llb[var p :=p # llb ! var p]) var"
by (simp add: wf_levellist_def)
have mark_nc:
"∀ n. n ∉ set_of (Node lt p rt) ⟶ (markb(p:=m)) n = mark n"
apply -
apply (rule allI)
apply (rule impI)
proof -
fix n
assume nnit: "n ∉ set_of (Node lt p rt)"
with lt rt have nnilt: " n ∉ set_of lt"
by fastforce
from nnit lt rt have nnirt: " n ∉ set_of rt"
by fastforce
with nnilt mot_nc mort_nc have mb_eq_m: "markb n = mark n"
by fastforce
from nnit have "n≠p"
by fastforce
then have upmarkb_markb: "(markb(p :=m)) n = markb n"
by fastforce
with mb_eq_m show "(markb(p :=m)) n = mark n"
by fastforce
qed
have mark_c: "∀ n. n ∈ set_of (Node lt p rt) ⟶ (markb(p :=m)) n = m"
apply -
apply (intro allI)
apply (rule impI)
proof -
fix n
assume nint: " n ∈ set_of (Node lt p rt)"
show "(markb(p :=m)) n = m"
proof (cases "n=p")
case True
then show ?thesis
by fastforce
next
assume nnp: " n ≠ p"
show ?thesis
proof (cases "n ∈ set_of rt")
case True
with mirt_marked have "markb n = m"
by fastforce
with nnp show ?thesis
by fastforce
next
assume nninrt: " n ∉ set_of rt"
with nint nnp have ninlt: "n ∈ set_of lt"
by fastforce
with mit_marked have marka_m: "marka n = m"
by fastforce
from mort_nc nninrt have "marka n = markb n"
by fastforce
with marka_m have "markb n = m"
by fastforce
with nnp show ?thesis
by fastforce
qed
qed
qed
from mark_c mark_nc
have wf_mark: "wf_marking (Node lt p rt) mark (markb(p :=m)) m"
by (simp add: wf_marking_def)
with wf_ll_upllb show ?thesis
by fastforce
qed
qed
qed
qed
done
qed
done
qed
next
fix var low high p lt rt and levellist and
ll::"ref list list" and mark::"ref ⇒ bool" and "next"
assume pnN: "p ≠ Null"
assume ll: "Levellist levellist next ll"
assume vpsll: "var p < length levellist"
assume orderedt: "ordered (Node lt p rt) var"
assume marked_child_ll: "∀n∈set_of (Node lt p rt).
if mark n = mark p
then n ∈ set (ll ! var n) ∧
(∀nt pa. Dag n low high nt ∧ pa ∈ set_of nt ⟶ mark pa = mark p)
else n ∉ set (concat ll)"
assume lt: "Dag (low p) low high lt"
assume rt: "Dag (high p) low high rt"
show "wf_levellist (Node lt p rt) ll ll var ∧
wf_marking (Node lt p rt) mark mark (mark p)"
proof -
from marked_child_ll pnN lt rt have marked_st:
"(∀pa. pa ∈ set_of (Node lt p rt) ⟶ mark pa = mark p)"
apply -
apply (drule_tac x="p" in bspec)
apply simp
apply (clarsimp)
apply (erule_tac x="(Node lt p rt)" in allE)
apply simp
done
have nodest_in_ll:
"∀q. q ∈ set_of (Node lt p rt) ⟶ q ∈ set (ll ! var q)"
proof -
from marked_child_ll pnN have pinll: "p ∈ set (ll ! var p)"
apply -
apply (drule_tac x="p" in bspec)
apply simp
apply fastforce
done
from marked_st marked_child_ll lt rt show ?thesis
apply -
apply (rule allI)
apply (erule_tac x="q" in allE)
apply (rule impI)
apply (erule impE)
apply assumption
apply (drule_tac x="q" in bspec)
apply simp
apply fastforce
done
qed
have levellist_nc: "∀ i ≤ var p. (∃ prx. ll ! i = prx@(ll ! i) ∧
(∀ pt ∈ set prx. pt ∈ set_of (Node lt p rt) ∧ var pt = i))"
apply -
apply (rule allI)
apply (rule impI)
apply (rule_tac x="[]" in exI)
apply fastforce
done
have ll_nc: "∀ i. (var p) < i ⟶ ll ! i = ll ! i"
by fastforce
have length_ll: "length ll = length ll"
by fastforce
with ll_nc levellist_nc nodest_in_ll
have wf: "wf_levellist (Node lt p rt) ll ll var"
by (simp add: wf_levellist_def)
have m_nc: "∀ n. n ∉ set_of (Node lt p rt) ⟶ mark n = mark n"
by fastforce
from marked_st have "∀ n. n ∈ set_of (Node lt p rt) ⟶ mark n = mark p"
by fastforce
with m_nc have " wf_marking (Node lt p rt) mark mark (mark p)"
by (simp add: wf_marking_def)
with wf show ?thesis
by fastforce
qed
qed
lemma allD: "∀ll. P ll ⟹ P ll"
by blast
lemma replicate_spec: "⟦∀i < n. xs ! i = x; n=length xs⟧
⟹ replicate (length xs) x = xs"
apply hypsubst_thin
apply (induct xs)
apply simp
apply force
done
lemma (in Levellist_impl) Levellist_spec_total:
shows "∀σ t. Γ,Θ⊢⇩t
⦃σ. Dag ´p ´low ´high t ∧ (∀i < length ´levellist. ´levellist ! i = Null) ∧
length ´levellist = ´p → ´var + 1 ∧
ordered t ´var ∧ (∀n ∈ set_of t. ´mark n = (¬ ´m) )⦄
´levellist :== PROC Levellist (´p, ´m, ´levellist)
⦃∃ll. Levellist ´levellist ´next ll ∧ wf_ll t ll ⇗σ⇖var ∧
length ´levellist = ⇗σ⇖p → ⇗σ⇖var + 1 ∧
wf_marking t ⇗σ⇖mark ´mark ⇗σ⇖m ∧
(∀p. p ∉ set_of t ⟶ ⇗σ⇖next p = ´next p)⦄"
apply (hoare_rule HoareTotal.conseq)
apply (rule_tac ll="replicate (⇗σ⇖p→⇗σ⇖var + 1) []" in allD [OF Levellist_spec_total'])
apply (intro allI impI)
apply (rule_tac x=σ in exI)
apply (rule_tac x=t in exI)
apply (rule conjI)
apply (clarsimp split:if_split_asm simp del: concat_replicate_trivial)
apply (frule replicate_spec [symmetric])
apply (simp)
apply (clarsimp simp add: Levellist_def )
apply (case_tac i)
apply simp
apply simp
apply (simp add: Collect_conv_if split:if_split_asm)
apply vcg_step
apply (elim exE conjE)
apply (rule_tac x=ll' in exI)
apply simp
apply (thin_tac "∀p. p ∉ set_of t ⟶ next p = nexta p")
apply (simp add: wf_levellist_def wf_ll_def)
apply (case_tac "t = Tip")
apply simp
apply (rule conjI)
apply clarsimp
apply (case_tac k)
apply simp
apply simp
apply (subgoal_tac "length ll'=Suc (var Null)")
apply (simp add: Levellist_length)
apply fastforce
apply (split dag.splits)
apply simp
apply (elim conjE)
apply (intro conjI)
apply (rule allI)
apply (erule_tac x="pa" in allE)
apply clarify
prefer 2
apply (simp add: Levellist_length)
apply (rule allI)
apply (rule impI)
apply (rule ballI)
apply (rotate_tac 11)
apply (erule_tac x="k" in allE)
apply (rename_tac dag1 ref dag2 k pa)
apply (subgoal_tac "k <= var ref")
prefer 2
apply (subgoal_tac "ref = p")
apply simp
apply clarify
apply (erule_tac ?P = "Dag p low high (Node dag1 ref dag2)" in rev_mp)
apply (simp (no_asm))
apply (rotate_tac 14)
apply (erule_tac x=k in allE)
apply clarify
apply (erule_tac x=k in allE)
apply clarify
apply (case_tac k)
apply simp
apply simp
done
end