Theory RepointProof
section ‹Proof of Procedure Repoint›
theory RepointProof imports ProcedureSpecs begin
hide_const (open) DistinctTreeProver.set_of tree.Node tree.Tip
lemma (in Repoint_impl) Repoint_modifies:
shows "∀σ. Γ⊢{σ} ´p :== PROC Repoint (´p)
{t. t may_only_modify_globals σ in [low,high]}"
apply (hoare_rule HoarePartial.ProcRec1)
apply (vcg spec=modifies)
done
lemma low_high_exchange_dag:
assumes pt_same: "∀pt. pt ∉ set_of lt ⟶ low pt = lowa pt ∧ high pt = higha pt"
assumes pt_changed: "∀pt ∈ set_of lt. lowa pt = (rep ∝ low) pt ∧
higha pt = (rep ∝ high) pt"
assumes rep_pt: "∀pt ∈ set_of rt. rep pt = pt"
shows "⋀q. Dag q (rep ∝ low) (rep ∝ high) rt ⟹
Dag q (rep ∝ lowa) (rep ∝ higha) rt"
using rep_pt
proof (induct rt)
case Tip thus ?case by simp
next
case (Node lrt q' rrt)
have "Dag q (rep ∝ low) (rep ∝ high) (Node lrt q' rrt)" by fact
then obtain
q': "q = q'" and
q_notNull: "q ≠ Null" and
lrt: "Dag ((rep ∝ low) q) (rep ∝ low) (rep ∝ high) lrt" and
rrt: "Dag ((rep ∝ high) q) (rep ∝ low) (rep ∝ high) rrt"
by auto
have rlowa_rlow: "((rep ∝ lowa) q) = ((rep ∝ low) q)"
proof (cases "q ∈ set_of lt")
case True
note q_in_lt=this
with pt_changed have lowa_q: "lowa q = (rep ∝ low) q"
by simp
thus "(rep ∝ lowa) q = (rep ∝ low) q"
proof (cases "low q = Null")
case True
with lowa_q have "lowa q = Null"
by (simp add: null_comp_def)
with True show ?thesis
by (simp add: null_comp_def)
next
assume lq_nNull: "low q ≠ Null"
show ?thesis
proof (cases "(rep ∝ low) q = Null")
case True
with lowa_q have "lowa q = Null"
by simp
with True show ?thesis
by (simp add: null_comp_def)
next
assume rlq_nNull: "(rep ∝ low) q ≠ Null"
with lrt lowa_q have "lowa q ∈ set_of lrt"
by auto
with Node.prems Node have "lowa q ∈ set_of (Node lrt q' rrt)"
by simp
with Node.prems have "rep (lowa q) = lowa q"
by auto
with lowa_q rlq_nNull show ?thesis
by (simp add: null_comp_def)
qed
qed
next
assume q_notin_lt: " q ∉ set_of lt"
with pt_same have "low q = lowa q"
by auto
thus ?thesis
by (simp add: null_comp_def)
qed
have rhigha_rhigh: "((rep ∝ higha) q) = ((rep ∝ high) q)"
proof (cases "q ∈ set_of lt")
case True
note q_in_lt=this
with pt_changed have higha_q: "higha q = (rep ∝ high) q"
by simp
thus ?thesis
proof (cases "high q = Null")
case True
with higha_q have "higha q = Null"
by (simp add: null_comp_def)
with True show ?thesis
by (simp add: null_comp_def)
next
assume hq_nNull: "high q ≠ Null"
show ?thesis
proof (cases "(rep ∝ high) q = Null")
case True
with higha_q have "higha q = Null"
by simp
with True show ?thesis
by (simp add: null_comp_def)
next
assume rhq_nNull: "(rep ∝ high) q ≠ Null"
with rrt higha_q have "higha q ∈ set_of rrt"
by auto
with Node.prems Node have "higha q ∈ set_of (Node lrt q' rrt)"
by simp
with Node.prems have "rep (higha q) = higha q"
by auto
with higha_q rhq_nNull show ?thesis
by (simp add: null_comp_def)
qed
qed
next
assume q_notin_lt: " q ∉ set_of lt"
with pt_same have "high q = higha q"
by auto
thus ?thesis
by (simp add: null_comp_def)
qed
with rrt have rhigha_mixed_dag:
"Dag ((rep ∝ higha) q) (rep ∝ low) (rep ∝ high) rrt"
by simp
from lrt rlowa_rlow have rlowa_mixed_dag:
" Dag ((rep ∝ lowa) q) (rep ∝ low) (rep ∝ high) lrt"
by simp
from Node.prems have lrt_rep_eq: " ∀pt∈set_of lrt. rep pt = pt"
by simp
from Node.prems have rrt_rep_eq: "∀pt∈set_of rrt. rep pt = pt"
by simp
from rlowa_mixed_dag lrt_rep_eq have lowa_lrt:
" Dag ((rep ∝ lowa) q) (rep ∝ lowa) (rep ∝ higha) lrt"
apply -
apply (rule Node.hyps)
apply auto
done
from rhigha_mixed_dag rrt_rep_eq have higha_rrt:
" Dag ((rep ∝ higha) q) (rep ∝ lowa) (rep ∝ higha) rrt"
apply -
apply (rule Node.hyps)
apply auto
done
with lowa_lrt q' q_notNull
show " Dag q (rep ∝ lowa) (rep ∝ higha) (Node lrt q' rrt)"
by simp
qed
lemma (in Repoint_impl) Repoint_spec':
shows
"∀σ. Γ⊢ {σ}
´p :== PROC Repoint (´p)
⦃∀ rept. ((Dag ((⇗σ⇖rep ∝ id) ⇗σ⇖p) (⇗σ⇖rep ∝ ⇗σ⇖low) (⇗σ⇖rep ∝ ⇗σ⇖high) rept)
∧ (∀ no ∈ set_of rept. ⇗σ⇖rep no = no))
⟶ Dag ´p ´low ´high rept ∧
(∀pt. pt ∉ set_of rept ⟶ ⇗σ⇖low pt = ´low pt ∧ ⇗σ⇖high pt = ´high pt)⦄"
apply (hoare_rule HoarePartial.ProcRec1)
apply vcg
apply (rule conjI)
apply clarify
prefer 2
apply (intro impI allI )
apply (simp add: null_comp_def)
apply (rule conjI)
prefer 2
apply (clarsimp)
apply clarify
proof -
fix low high p rep lowa higha pa lowb highb pb rept
assume p_nNull: "p ≠ Null"
assume rp_nNull: " rep p ≠ Null"
assume rec_spec_lrept:
"∀rept. Dag ((rep ∝ id) (low (rep p))) (rep ∝ low) (rep ∝ high) rept
∧ (∀no∈set_of rept. rep no = no)
⟶ Dag pa lowa higha rept ∧
(∀pt. pt ∉ set_of rept ⟶ low pt = lowa pt ∧ high pt = higha pt)"
assume rec_spec_rrept:
"∀rept. Dag ((rep ∝ id) (higha (rep p))) (rep ∝ lowa(rep p := pa)) (rep ∝ higha) rept
∧ (∀no∈set_of rept. rep no = no)
⟶ Dag pb lowb highb rept ∧
(∀pt. pt ∉ set_of rept ⟶ (lowa(rep p := pa)) pt = lowb pt ∧ higha pt = highb pt)"
assume rept_dag: "Dag ((rep ∝ id) p) (rep ∝ low) (rep ∝ high) rept"
assume rno_rept: "∀no∈set_of rept. rep no = no"
show " Dag (rep p) lowb (highb(rep p := pb)) rept ∧
(∀pt. pt ∉ set_of rept ⟶ low pt = lowb pt ∧ high pt = (highb(rep p := pb)) pt)"
proof -
from rp_nNull rept_dag p_nNull obtain lrept rrept where
rept_def: "rept = Node lrept (rep p) rrept"
by auto
with rept_dag p_nNull have lrept_dag:
"Dag ((rep ∝ low) (rep p)) (rep ∝ low) (rep ∝ high) lrept"
by simp
from rept_def rept_dag p_nNull have rrept_dag:
"Dag ((rep ∝ high) (rep p)) (rep ∝ low) (rep ∝ high) rrept"
by simp
from rno_rept rept_def have rno_lrept: "∀ no ∈ set_of lrept. rep no = no"
by auto
from rno_rept rept_def have rno_rrept: "∀ no ∈ set_of rrept. rep no = no"
by auto
have repoint_post_low:
" Dag pa lowa higha lrept ∧
(∀pt. pt ∉ set_of lrept ⟶ low pt = lowa pt ∧ high pt = higha pt)"
proof -
from lrept_dag have " Dag ((rep ∝ id) (low (rep p))) (rep ∝ low) (rep ∝ high) lrept"
by (simp add: id_trans)
with rec_spec_lrept rno_lrept show ?thesis
apply -
apply (erule_tac x=lrept in allE)
apply (erule impE)
apply simp
apply assumption
done
qed
hence low_lowa_nc: "(∀pt. pt ∉ set_of lrept ⟶ low pt = lowa pt ∧ high pt = higha pt)"
by simp
from lrept_dag repoint_post_low obtain
pa_def: "pa = (rep ∝ low) (rep p)" and
lowa_higha_def: "(∀ no ∈ set_of lrept. lowa no = (rep ∝ low) no ∧ higha no = (rep ∝ high) no)"
apply -
apply (drule Dags_eq_hp_eq)
apply auto
done
from rept_dag have rept_DAG: "DAG rept"
by (rule Dag_is_DAG)
with rept_def have rp_notin_lrept: "rep p ∉ set_of lrept"
by simp
from rept_DAG rept_def have rp_notin_rrept: "rep p ∉ set_of rrept"
by simp
have "Dag ((rep ∝ id) (higha (rep p))) (rep ∝ lowa(rep p := pa)) (rep ∝ higha) rrept"
proof -
from low_lowa_nc rp_notin_lrept have "(rep ∝ high) (rep p) = (rep ∝ higha) (rep p)"
by (auto simp add: null_comp_def)
with rrept_dag have higha_mixed_rrept:
"Dag ((rep ∝ id) (higha (rep p))) (rep ∝ low) (rep ∝ high) rrept"
by (simp add: id_trans)
thm low_high_exchange_dag
with low_lowa_nc lowa_higha_def rno_rrept have lowa_higha_rrept:
"Dag ((rep ∝ id) (higha (rep p))) (rep ∝ lowa) (rep ∝ higha) rrept"
apply -
apply (rule low_high_exchange_dag)
apply auto
done
have "Dag ((rep ∝ id) (higha (rep p))) (rep ∝ lowa) (rep ∝ higha) rrept =
Dag ((rep ∝ id) (higha (rep p))) (rep ∝ lowa(rep p := pa)) (rep ∝ higha) rrept"
proof -
have "∀ no ∈ set_of rrept. (rep ∝ lowa) no = (rep ∝ lowa(rep p := pa)) no ∧
(rep ∝ higha) no = (rep ∝ higha) no"
proof
fix no
assume no_in_rrept: "no ∈ set_of rrept"
with rp_notin_rrept have "no ≠ rep p"
by blast
thus "(rep ∝ lowa) no = (rep ∝ lowa(rep p := pa)) no ∧
(rep ∝ higha) no = (rep ∝ higha) no"
by (simp add: null_comp_def)
qed
thus ?thesis
by (rule heaps_eq_Dag_eq)
qed
with lowa_higha_rrept show ?thesis
by simp
qed
with rec_spec_rrept rno_rrept have repoint_rrept: "Dag pb lowb highb rrept ∧
(∀pt. pt ∉ set_of rrept ⟶
(lowa(rep p := pa)) pt = lowb pt ∧ higha pt = highb pt)"
apply -
apply (erule_tac x=rrept in allE)
apply (erule impE)
apply simp
apply assumption
done
then have ab_nc: "(∀pt. pt ∉ set_of rrept ⟶
(lowa(rep p := pa)) pt = lowb pt ∧ higha pt = highb pt)"
by simp
from repoint_rrept rrept_dag obtain
pb_def: "pb = ((rep ∝ high) (rep p))" and
lowb_highb_def: "(∀ no ∈ set_of rrept. lowb no = (rep ∝ low) no ∧ highb no = (rep ∝ high) no)"
apply -
apply (drule Dags_eq_hp_eq)
apply auto
done
have rept_end_dag: " Dag (rep p) lowb (highb(rep p := pb)) rept"
proof -
have "∀ no ∈ set_of rept. lowb no = (rep ∝ low) no ∧ (highb(rep p := pb)) no = (rep ∝ high) no"
proof
fix no
assume no_in_rept: " no ∈ set_of rept"
show "lowb no = (rep ∝ low) no ∧ (highb(rep p := pb)) no = (rep ∝ high) no"
proof (cases "no ∈ set_of rrept")
case True
with lowb_highb_def pb_def show ?thesis
by simp
next
assume no_notin_rrept: " no ∉ set_of rrept"
show ?thesis
proof (cases "no ∈ set_of lrept")
case True
with no_notin_rrept rp_notin_lrept ab_nc
have ab_nc_no: "lowa no = lowb no ∧ higha no = highb no"
apply -
apply (erule_tac x=no in allE)
apply (erule impE)
apply simp
apply (subgoal_tac "no ≠ rep p")
apply simp
apply blast
done
from lowa_higha_def True have
"lowa no = (rep ∝ low) no ∧ higha no = (rep ∝ high) no"
by auto
with ab_nc_no have "lowb no = (rep ∝ low) no ∧ highb no =(rep ∝ high) no"
by simp
with rp_notin_lrept True show ?thesis
apply (subgoal_tac "no ≠ rep p")
apply simp
apply blast
done
next
assume no_notin_lrept: " no ∉ set_of lrept"
with no_in_rept rept_def no_notin_rrept have no_rp: "no = rep p"
by simp
with rp_notin_lrept low_lowa_nc have a_nc:
"low no = lowa no ∧ high no = higha no"
by auto
from rp_notin_rrept no_rp ab_nc have
"(lowa(rep p := pa)) no = lowb no ∧ higha no = highb no"
by auto
with a_nc pa_def no_rp have "(rep ∝ low) no = lowb no ∧ high no = highb no"
by auto
with pb_def no_rp show ?thesis
by simp
qed
qed
qed
with rept_dag have " Dag (rep p) lowb (highb(rep p := pb)) rept =
Dag (rep p) (rep ∝ low) (rep ∝ high) rept"
apply -
thm heaps_eq_Dag_eq
apply (rule heaps_eq_Dag_eq)
apply auto
done
with rept_dag p_nNull show ?thesis
by simp
qed
have "(∀pt. pt ∉ set_of rept ⟶ low pt = lowb pt ∧ high pt = (highb(rep p := pb)) pt)"
proof (intro allI impI)
fix pt
assume pt_notin_rept: "pt ∉ set_of rept"
with rept_def obtain
pt_notin_lrept: "pt ∉ set_of lrept" and
pt_notin_rrept: "pt ∉ set_of rrept" and
pt_neq_rp: "pt ≠ rep p"
by simp
with low_lowa_nc ab_nc show "low pt = lowb pt ∧ high pt = (highb(rep p := pb)) pt"
by auto
qed
with rept_end_dag show ?thesis
by simp
qed
qed
lemma (in Repoint_impl) Repoint_spec:
shows
"∀σ rept. Γ⊢ ⦃σ. Dag ((´rep ∝ id) ´p) (´rep ∝ ´low) (´rep ∝ ´high) rept
∧ (∀ no ∈ set_of rept. ´rep no = no) ⦄
´p :== PROC Repoint (´p)
⦃Dag ´p ´low ´high rept ∧
(∀pt. pt ∉ set_of rept ⟶ ⇗σ⇖low pt = ´low pt ∧ ⇗σ⇖high pt = ´high pt)⦄"
apply (hoare_rule HoarePartial.ProcRec1)
apply vcg
apply (rule conjI)
prefer 2
apply (clarsimp simp add: null_comp_def)
apply clarify
apply (rule conjI)
prefer 2
apply clarsimp
apply clarify
proof -
fix rept low high rep p
assume rept_dag: "Dag ((rep ∝ id) p) (rep ∝ low) (rep ∝ high) rept"
assume rno_rept: "∀no∈set_of rept. rep no = no"
assume p_nNull: "p ≠ Null"
assume rp_nNull: " rep p ≠ Null"
show "∃lrept.
Dag ((rep ∝ id) (low (rep p))) (rep ∝ low) (rep ∝ high) lrept ∧
(∀no∈set_of lrept. rep no = no) ∧
(∀lowa higha pa.
Dag pa lowa higha lrept ∧
(∀pt. pt ∉ set_of lrept ⟶
low pt = lowa pt ∧ high pt = higha pt) ⟶
(∃rrept.
Dag ((rep ∝ id) (higha (rep p))) (rep ∝ lowa(rep p := pa))
(rep ∝ higha) rrept ∧
(∀no∈set_of rrept. rep no = no) ∧
(∀lowb highb pb.
Dag pb lowb highb rrept ∧
(∀pt. pt ∉ set_of rrept ⟶
(lowa(rep p := pa)) pt = lowb pt ∧
higha pt = highb pt) ⟶
Dag (rep p) lowb (highb(rep p := pb)) rept ∧
(∀pt. pt ∉ set_of rept ⟶
low pt = lowb pt ∧
high pt = (highb(rep p := pb)) pt))))"
proof -
from rp_nNull rept_dag p_nNull obtain lrept rrept where
rept_def: "rept = Node lrept (rep p) rrept"
by auto
with rept_dag p_nNull have lrept_dag:
"Dag ((rep ∝ low) (rep p)) (rep ∝ low) (rep ∝ high) lrept"
by simp
from rept_def rept_dag p_nNull have rrept_dag:
"Dag ((rep ∝ high) (rep p)) (rep ∝ low) (rep ∝ high) rrept"
by simp
from rno_rept rept_def have rno_lrept: "∀ no ∈ set_of lrept. rep no = no"
by auto
from rno_rept rept_def have rno_rrept: "∀ no ∈ set_of rrept. rep no = no"
by auto
show ?thesis
apply (rule_tac x=lrept in exI)
apply (rule conjI)
apply (simp add: id_trans lrept_dag)
apply (rule conjI)
apply (rule rno_lrept)
apply clarify
subgoal premises prems for lowa higha pa
proof -
have lrepta: "Dag pa lowa higha lrept" by fact
have low_lowa_nc:
"∀pt. pt ∉ set_of lrept ⟶ low pt = lowa pt ∧ high pt = higha pt" by fact
from lrept_dag lrepta obtain
pa_def: "pa = (rep ∝ low) (rep p)" and
lowa_higha_def: "∀no ∈ set_of lrept.
lowa no = (rep ∝ low) no ∧ higha no = (rep ∝ high) no"
apply -
apply (drule Dags_eq_hp_eq)
apply auto
done
from rept_dag have rept_DAG: "DAG rept"
by (rule Dag_is_DAG)
with rept_def have rp_notin_lrept: "rep p ∉ set_of lrept"
by simp
from rept_DAG rept_def have rp_notin_rrept: "rep p ∉ set_of rrept"
by simp
have rrepta: "Dag ((rep ∝ id) (higha (rep p)))
(rep ∝ lowa(rep p := pa)) (rep ∝ higha) rrept"
proof -
from low_lowa_nc rp_notin_lrept
have "(rep ∝ high) (rep p) = (rep ∝ higha) (rep p)"
by (auto simp add: null_comp_def)
with rrept_dag have higha_mixed_rrept:
"Dag ((rep ∝ id) (higha (rep p))) (rep ∝ low) (rep ∝ high) rrept"
by (simp add: id_trans)
thm low_high_exchange_dag
with low_lowa_nc lowa_higha_def rno_rrept
have lowa_higha_rrept:
"Dag ((rep ∝ id) (higha (rep p))) (rep ∝ lowa) (rep ∝ higha) rrept"
apply -
apply (rule low_high_exchange_dag)
apply auto
done
have "Dag ((rep ∝ id) (higha (rep p))) (rep ∝ lowa) (rep ∝ higha) rrept =
Dag ((rep ∝ id) (higha (rep p)))
(rep ∝ lowa(rep p := pa)) (rep ∝ higha) rrept"
proof -
have "∀no ∈ set_of rrept.
(rep ∝ lowa) no = (rep ∝ lowa(rep p := pa)) no ∧
(rep ∝ higha) no = (rep ∝ higha) no"
proof
fix no
assume no_in_rrept: "no ∈ set_of rrept"
with rp_notin_rrept have "no ≠ rep p"
by blast
thus "(rep ∝ lowa) no = (rep ∝ lowa(rep p := pa)) no ∧
(rep ∝ higha) no = (rep ∝ higha) no"
by (simp add: null_comp_def)
qed
thus ?thesis
by (rule heaps_eq_Dag_eq)
qed
with lowa_higha_rrept show ?thesis
by simp
qed
show ?thesis
apply (rule_tac x=rrept in exI)
apply (rule conjI)
apply (rule rrepta)
apply (rule conjI)
apply (rule rno_rrept)
apply clarify
subgoal premises prems for lowb highb pb
proof -
have rreptb: "Dag pb lowb highb rrept" by fact
have ab_nc: "∀pt. pt ∉ set_of rrept ⟶
(lowa(rep p := pa)) pt = lowb pt ∧ higha pt = highb pt" by fact
from rreptb rrept_dag obtain
pb_def: "pb = ((rep ∝ high) (rep p))" and
lowb_highb_def: "∀no ∈ set_of rrept.
lowb no = (rep ∝ low) no ∧ highb no = (rep ∝ high) no"
apply -
apply (drule Dags_eq_hp_eq)
apply auto
done
have rept_end_dag: " Dag (rep p) lowb (highb(rep p := pb)) rept"
proof -
have "∀no ∈ set_of rept.
lowb no = (rep ∝ low) no ∧ (highb(rep p := pb)) no = (rep ∝ high) no"
proof
fix no
assume no_in_rept: " no ∈ set_of rept"
show "lowb no = (rep ∝ low) no ∧
(highb(rep p := pb)) no = (rep ∝ high) no"
proof (cases "no ∈ set_of rrept")
case True
with lowb_highb_def pb_def show ?thesis
by simp
next
assume no_notin_rrept: " no ∉ set_of rrept"
show ?thesis
proof (cases "no ∈ set_of lrept")
case True
with no_notin_rrept rp_notin_lrept ab_nc
have ab_nc_no: "lowa no = lowb no ∧ higha no = highb no"
apply -
apply (erule_tac x=no in allE)
apply (erule impE)
apply simp
apply (subgoal_tac "no ≠ rep p")
apply simp
apply blast
done
from lowa_higha_def True have
"lowa no = (rep ∝ low) no ∧ higha no = (rep ∝ high) no"
by auto
with ab_nc_no
have "lowb no = (rep ∝ low) no ∧ highb no =(rep ∝ high) no"
by simp
with rp_notin_lrept True show ?thesis
apply (subgoal_tac "no ≠ rep p")
apply simp
apply blast
done
next
assume no_notin_lrept: " no ∉ set_of lrept"
with no_in_rept rept_def no_notin_rrept have no_rp: "no = rep p"
by simp
with rp_notin_lrept low_lowa_nc
have a_nc: "low no = lowa no ∧ high no = higha no"
by auto
from rp_notin_rrept no_rp ab_nc
have "(lowa(rep p := pa)) no = lowb no ∧ higha no = highb no"
by auto
with a_nc pa_def no_rp
have "(rep ∝ low) no = lowb no ∧ high no = highb no"
by auto
with pb_def no_rp show ?thesis
by simp
qed
qed
qed
with rept_dag
have "Dag (rep p) lowb (highb(rep p := pb)) rept =
Dag (rep p) (rep ∝ low) (rep ∝ high) rept"
apply -
apply (rule heaps_eq_Dag_eq)
apply auto
done
with rept_dag p_nNull show ?thesis
by simp
qed
have "(∀pt. pt ∉ set_of rept ⟶ low pt = lowb pt ∧
high pt = (highb(rep p := pb)) pt)"
proof (intro allI impI)
fix pt
assume pt_notin_rept: "pt ∉ set_of rept"
with rept_def obtain
pt_notin_lrept: "pt ∉ set_of lrept" and
pt_notin_rrept: "pt ∉ set_of rrept" and
pt_neq_rp: "pt ≠ rep p"
by simp
with low_lowa_nc ab_nc
show "low pt = lowb pt ∧ high pt = (highb(rep p := pb)) pt"
by auto
qed
with rept_end_dag show ?thesis
by simp
qed
done
qed
done
qed
qed
lemma (in Repoint_impl) Repoint_spec_total:
shows
"∀σ rept. Γ⊢⇩t ⦃σ. Dag ((´rep ∝ id) ´p) (´rep ∝ ´low) (´rep ∝ ´high) rept
∧ (∀ no ∈ set_of rept. ´rep no = no) ⦄
´p :== PROC Repoint (´p)
⦃Dag ´p ´low ´high rept ∧
(∀pt. pt ∉ set_of rept ⟶ ⇗σ⇖low pt = ´low pt ∧ ⇗σ⇖high pt = ´high pt)⦄"
apply (hoare_rule HoareTotal.ProcRec1
[where r="measure (λ(s,p). size
(dag ((⇗s⇖rep ∝ id) ⇗s⇖p) (⇗s⇖rep ∝ ⇗s⇖low) (⇗s⇖rep ∝ ⇗s⇖high)))"])
apply vcg
apply (rule conjI)
prefer 2
apply (clarsimp simp add: null_comp_def)
apply clarify
apply (rule conjI)
prefer 2
apply clarsimp
apply clarify
proof -
fix rept low high rep p
assume rept_dag: "Dag ((rep ∝ id) p) (rep ∝ low) (rep ∝ high) rept"
assume rno_rept: "∀no∈set_of rept. rep no = no"
assume p_nNull: "p ≠ Null"
assume rp_nNull: " rep p ≠ Null"
show "∃lrept.
Dag ((rep ∝ id) (low (rep p))) (rep ∝ low) (rep ∝ high) lrept ∧
(∀no∈set_of lrept. rep no = no) ∧
size (dag ((rep ∝ id) (low (rep p))) (rep ∝ low) (rep ∝ high))
< size (dag ((rep ∝ id) p) (rep ∝ low) (rep ∝ high)) ∧
(∀lowa higha pa.
Dag pa lowa higha lrept ∧
(∀pt. pt ∉ set_of lrept ⟶
low pt = lowa pt ∧ high pt = higha pt) ⟶
(∃rrept.
Dag ((rep ∝ id) (higha (rep p))) (rep ∝ lowa(rep p := pa))
(rep ∝ higha) rrept ∧
(∀no∈set_of rrept. rep no = no) ∧
size (dag ((rep ∝ id) (higha (rep p)))
(rep ∝ lowa(rep p := pa)) (rep ∝ higha))
< size (dag ((rep ∝ id) p) (rep ∝ low) (rep ∝ high)) ∧
(∀lowb highb pb.
Dag pb lowb highb rrept ∧
(∀pt. pt ∉ set_of rrept ⟶
(lowa(rep p := pa)) pt = lowb pt ∧
higha pt = highb pt) ⟶
Dag (rep p) lowb (highb(rep p := pb)) rept ∧
(∀pt. pt ∉ set_of rept ⟶
low pt = lowb pt ∧
high pt = (highb(rep p := pb)) pt))))"
proof -
from rp_nNull rept_dag p_nNull obtain lrept rrept where
rept_def: "rept = Node lrept (rep p) rrept"
by auto
with rept_dag p_nNull have lrept_dag:
"Dag ((rep ∝ low) (rep p)) (rep ∝ low) (rep ∝ high) lrept"
by simp
from rept_def rept_dag p_nNull have rrept_dag:
"Dag ((rep ∝ high) (rep p)) (rep ∝ low) (rep ∝ high) rrept"
by simp
from rno_rept rept_def have rno_lrept: "∀ no ∈ set_of lrept. rep no = no"
by auto
from rno_rept rept_def have rno_rrept: "∀ no ∈ set_of rrept. rep no = no"
by auto
show ?thesis
apply (rule_tac x=lrept in exI)
apply (rule conjI)
apply (simp add: id_trans lrept_dag)
apply (rule conjI)
apply (rule rno_lrept)
apply (rule conjI)
using rept_dag rept_def
apply (simp only: Dag_dag)
apply (clarsimp simp add: id_trans Dag_dag)
apply clarify
subgoal premises prems for lowa higha pa
proof -
have lrepta: "Dag pa lowa higha lrept" by fact
have low_lowa_nc:
"∀pt. pt ∉ set_of lrept ⟶ low pt = lowa pt ∧ high pt = higha pt" by fact
from lrept_dag lrepta obtain
pa_def: "pa = (rep ∝ low) (rep p)" and
lowa_higha_def: "∀no ∈ set_of lrept.
lowa no = (rep ∝ low) no ∧ higha no = (rep ∝ high) no"
apply -
apply (drule Dags_eq_hp_eq)
apply auto
done
from rept_dag have rept_DAG: "DAG rept"
by (rule Dag_is_DAG)
with rept_def have rp_notin_lrept: "rep p ∉ set_of lrept"
by simp
from rept_DAG rept_def have rp_notin_rrept: "rep p ∉ set_of rrept"
by simp
have rrepta: "Dag ((rep ∝ id) (higha (rep p)))
(rep ∝ lowa(rep p := pa)) (rep ∝ higha) rrept"
proof -
from low_lowa_nc rp_notin_lrept
have "(rep ∝ high) (rep p) = (rep ∝ higha) (rep p)"
by (auto simp add: null_comp_def)
with rrept_dag have higha_mixed_rrept:
"Dag ((rep ∝ id) (higha (rep p))) (rep ∝ low) (rep ∝ high) rrept"
by (simp add: id_trans)
thm low_high_exchange_dag
with low_lowa_nc lowa_higha_def rno_rrept
have lowa_higha_rrept:
"Dag ((rep ∝ id) (higha (rep p))) (rep ∝ lowa) (rep ∝ higha) rrept"
apply -
apply (rule low_high_exchange_dag)
apply auto
done
have "Dag ((rep ∝ id) (higha (rep p))) (rep ∝ lowa) (rep ∝ higha) rrept =
Dag ((rep ∝ id) (higha (rep p)))
(rep ∝ lowa(rep p := pa)) (rep ∝ higha) rrept"
proof -
have "∀no ∈ set_of rrept.
(rep ∝ lowa) no = (rep ∝ lowa(rep p := pa)) no ∧
(rep ∝ higha) no = (rep ∝ higha) no"
proof
fix no
assume no_in_rrept: "no ∈ set_of rrept"
with rp_notin_rrept have "no ≠ rep p"
by blast
thus "(rep ∝ lowa) no = (rep ∝ lowa(rep p := pa)) no ∧
(rep ∝ higha) no = (rep ∝ higha) no"
by (simp add: null_comp_def)
qed
thus ?thesis
by (rule heaps_eq_Dag_eq)
qed
with lowa_higha_rrept show ?thesis
by simp
qed
show ?thesis
apply (rule_tac x=rrept in exI)
apply (rule conjI)
apply (rule rrepta)
apply (rule conjI)
apply (rule rno_rrept)
apply (rule conjI)
using rept_dag rept_def rrepta
apply (simp only: Dag_dag)
apply (clarsimp simp add: id_trans Dag_dag)
apply clarify
subgoal premises prems for lowb highb pb
proof -
have rreptb: "Dag pb lowb highb rrept" by fact
have ab_nc: "∀pt. pt ∉ set_of rrept ⟶
(lowa(rep p := pa)) pt = lowb pt ∧ higha pt = highb pt" by fact
from rreptb rrept_dag obtain
pb_def: "pb = ((rep ∝ high) (rep p))" and
lowb_highb_def: "∀no ∈ set_of rrept.
lowb no = (rep ∝ low) no ∧ highb no = (rep ∝ high) no"
apply -
apply (drule Dags_eq_hp_eq)
apply auto
done
have rept_end_dag: " Dag (rep p) lowb (highb(rep p := pb)) rept"
proof -
have "∀no ∈ set_of rept.
lowb no = (rep ∝ low) no ∧ (highb(rep p := pb)) no = (rep ∝ high) no"
proof
fix no
assume no_in_rept: " no ∈ set_of rept"
show "lowb no = (rep ∝ low) no ∧
(highb(rep p := pb)) no = (rep ∝ high) no"
proof (cases "no ∈ set_of rrept")
case True
with lowb_highb_def pb_def show ?thesis
by simp
next
assume no_notin_rrept: " no ∉ set_of rrept"
show ?thesis
proof (cases "no ∈ set_of lrept")
case True
with no_notin_rrept rp_notin_lrept ab_nc
have ab_nc_no: "lowa no = lowb no ∧ higha no = highb no"
apply -
apply (erule_tac x=no in allE)
apply (erule impE)
apply simp
apply (subgoal_tac "no ≠ rep p")
apply simp
apply blast
done
from lowa_higha_def True have
"lowa no = (rep ∝ low) no ∧ higha no = (rep ∝ high) no"
by auto
with ab_nc_no
have "lowb no = (rep ∝ low) no ∧ highb no =(rep ∝ high) no"
by simp
with rp_notin_lrept True show ?thesis
apply (subgoal_tac "no ≠ rep p")
apply simp
apply blast
done
next
assume no_notin_lrept: " no ∉ set_of lrept"
with no_in_rept rept_def no_notin_rrept have no_rp: "no = rep p"
by simp
with rp_notin_lrept low_lowa_nc
have a_nc: "low no = lowa no ∧ high no = higha no"
by auto
from rp_notin_rrept no_rp ab_nc
have "(lowa(rep p := pa)) no = lowb no ∧ higha no = highb no"
by auto
with a_nc pa_def no_rp
have "(rep ∝ low) no = lowb no ∧ high no = highb no"
by auto
with pb_def no_rp show ?thesis
by simp
qed
qed
qed
with rept_dag
have "Dag (rep p) lowb (highb(rep p := pb)) rept =
Dag (rep p) (rep ∝ low) (rep ∝ high) rept"
apply -
apply (rule heaps_eq_Dag_eq)
apply auto
done
with rept_dag p_nNull show ?thesis
by simp
qed
have "(∀pt. pt ∉ set_of rept ⟶ low pt = lowb pt ∧
high pt = (highb(rep p := pb)) pt)"
proof (intro allI impI)
fix pt
assume pt_notin_rept: "pt ∉ set_of rept"
with rept_def obtain
pt_notin_lrept: "pt ∉ set_of lrept" and
pt_notin_rrept: "pt ∉ set_of rrept" and
pt_neq_rp: "pt ≠ rep p"
by simp
with low_lowa_nc ab_nc
show "low pt = lowb pt ∧ high pt = (highb(rep p := pb)) pt"
by auto
qed
with rept_end_dag show ?thesis
by simp
qed
done
qed
done
qed
qed
end