Theory NormalizeTotalProof
section ‹Proof of Procedure Normalize›
theory NormalizeTotalProof imports LevellistProof ShareReduceRepListProof
RepointProof begin
hide_const (open) DistinctTreeProver.set_of tree.Node tree.Tip
lemma (in Normalize_impl) Normalize_modifies:
shows
"∀σ. Γ⊢{σ} ´p :== PROC Normalize (´p)
{t. t may_only_modify_globals σ in [rep,mark,low,high,next]}"
apply (hoare_rule HoarePartial.ProcRec1)
apply (vcg spec=modifies)
done
lemma (in Normalize_impl) Normalize_spec:
shows "∀σ pret prebdt. Γ⊢⇩t
⦃σ. Dag ´p ´low ´high pret ∧ ordered pret ´var ∧
´p ≠ Null ∧ (∀n. n ∈ set_of pret ⟶ ´mark n = ´mark ´p) ∧
bdt pret ´var = Some prebdt⦄
´p :== PROC Normalize(´p)
⦃(∀pt. pt ∉ set_of pret
⟶ ⇗σ⇖rep pt = ´rep pt ∧ ⇗σ⇖low pt = ´low pt ∧ ⇗σ⇖high pt = ´high pt ∧
⇗σ⇖mark pt = ´mark pt ∧ ⇗σ⇖next pt = ´next pt) ∧
(∃postt. Dag ´p ´low ´high postt ∧ reduced postt ∧
shared postt ⇗σ⇖var ∧ ordered postt ⇗σ⇖var ∧
set_of postt ⊆ set_of pret ∧
(∃postbdt. bdt postt ⇗σ⇖var = Some postbdt ∧ prebdt ∼ postbdt)) ∧
(∀ no. no ∈ set_of pret ⟶ ´mark no = (¬ ⇗σ⇖mark ⇗σ⇖p)) ⦄"
apply (hoare_rule HoareTotal.ProcNoRec1)
apply (hoare_rule anno="
´levellist :==replicate (´p→´var + 1) Null;;
´levellist :== CALL Levellist (´p, (¬ ´p→´mark) , ´levellist);;
(ANNO (τ,ll). ⦃τ. Levellist ´levellist ´next ll ∧
Dag ⇗σ⇖p ⇗σ⇖low ⇗σ⇖high pret ∧ ordered pret ⇗σ⇖var ∧ ⇗σ⇖p ≠ Null ∧
(bdt pret ⇗σ⇖var = Some prebdt) ∧
wf_ll pret ll ⇗σ⇖var ∧
length ´levellist = ((⇗σ⇖p → ⇗σ⇖var) + 1) ∧
wf_marking pret ⇗σ⇖mark ´mark (¬ ⇗σ⇖mark ⇗σ⇖p) ∧
(∀pt. pt ∉ set_of pret ⟶ ⇗σ⇖next pt = ´next pt) ∧
´low = ⇗σ⇖low ∧ ´high = ⇗σ⇖high ∧ ´p = ⇗σ⇖p ∧ ´rep = ⇗σ⇖rep ∧
´var = ⇗σ⇖var⦄
´n :==0;;
WHILE (´n < length ´levellist)
INV ⦃Levellist ´levellist ´next ll ∧
Dag ⇗σ⇖p ⇗σ⇖low ⇗σ⇖high pret ∧ ordered pret ⇗σ⇖var ∧ ⇗σ⇖p ≠ Null ∧
(bdt pret ⇗σ⇖var = Some prebdt) ∧ wf_ll pret ll ⇗σ⇖var ∧
length ⇗τ⇖levellist = ((⇗σ⇖p → ⇗σ⇖var) + 1) ∧
wf_marking pret ⇗σ⇖mark ⇗τ⇖mark (¬ ⇗σ⇖mark ⇗σ⇖p) ∧
⇗τ⇖low = ⇗σ⇖low ∧ ⇗τ⇖high = ⇗σ⇖high ∧ ⇗τ⇖p = ⇗σ⇖p ∧ ⇗τ⇖rep = ⇗σ⇖rep ∧ ⇗τ⇖var = ⇗σ⇖var ∧
´n ≤ length ⇗τ⇖levellist ∧
(∀pt i. (pt ∉ set_of pret ∨ (´n <= i ∧ pt ∈ set (ll ! i) ∧
i <length ⇗τ⇖levellist )
⟶ ⇗σ⇖rep pt = ´rep pt)) ∧
´rep ` Nodes ´n ll ⊆ Nodes ´n ll ∧
(∀no ∈ Nodes ´n ll.
no→´rep→⇗σ⇖var <= no→⇗σ⇖var ∧
(∃not nort. Dag (´rep no) (´rep ∝ ⇗σ⇖low ) (´rep ∝ ⇗σ⇖high ) nort ∧
Dag no ⇗σ⇖low ⇗σ⇖high not ∧ reduced nort ∧
ordered nort ⇗σ⇖var ∧ set_of nort ⊆ ´rep ` Nodes ´n ll ∧
(∀ no ∈ set_of nort. ´rep no = no) ∧
(∃nobdt norbdt. bdt not ⇗σ⇖var = Some nobdt ∧
bdt nort ⇗σ⇖var = Some norbdt ∧ nobdt ∼ norbdt))) ∧
(∀t1 t2.
t1∈Dags (´rep `(Nodes ´n ll))(´rep ∝ ⇗σ⇖low )(´rep ∝ ⇗σ⇖high)∧
t2∈Dags (´rep `(Nodes ´n ll))(´rep ∝ ⇗σ⇖low )(´rep ∝ ⇗σ⇖high)
⟶
isomorphic_dags_eq t1 t2 ⇗σ⇖var) ∧
´levellist = ⇗τ⇖levellist ∧ ´next = ⇗τ⇖next ∧ ´mark = ⇗τ⇖mark ∧ ´low = ⇗σ⇖low ∧
´high = ⇗σ⇖high ∧ ´p = ⇗σ⇖p ∧ ´var = ⇗σ⇖var ⦄
VAR MEASURE (length ´levellist - ´n)
DO
CALL ShareReduceRepList(´levellist ! ´n);;
´n :==´n + 1
OD
⦃(∃postnormt. Dag (´rep ⇗σ⇖p) (´rep ∝ ⇗σ⇖low ) (´rep ∝ ⇗σ⇖high ) postnormt ∧
reduced postnormt ∧ shared postnormt ⇗σ⇖var ∧
ordered postnormt ⇗σ⇖var ∧ set_of postnormt ⊆ set_of pret ∧
(∃postnormbdt. bdt postnormt ⇗σ⇖var = Some postnormbdt ∧ prebdt ∼ postnormbdt) ∧
(∀ no ∈ set_of postnormt. (´rep no = no))) ∧
ordered pret ⇗σ⇖var ∧ ⇗σ⇖p ≠ Null ∧
(∀ pt. pt ∉ set_of pret ⟶ ⇗σ⇖rep pt = ´rep pt) ∧
´levellist = ⇗τ⇖levellist ∧ ´next = ⇗τ⇖next ∧ ´mark = ⇗τ⇖mark ∧ ´low = ⇗σ⇖low ∧ ´high = ⇗σ⇖high ∧
´p = ⇗σ⇖p ∧ (∀ no. no ∈ set_of pret ⟶ ´mark no = (¬ ⇗σ⇖mark ⇗σ⇖p)) ⦄)
;;
´p :== CALL Repoint (´p)"
in HoareTotal.annotateI)
apply (vcg spec=spec_total)
prefer 2
apply (simp add: Nodes_def null_comp_def)
apply (rule_tac x=pret in exI)
apply clarify
apply (rule conjI)
apply clarsimp
apply (case_tac i)
apply simp
apply simp
apply (rule conjI)
apply simp
apply (rule conjI)
apply simp
apply (rule conjI)
apply simp
apply clarify
apply (simp (no_asm_use) only: simp_thms)
apply (rule_tac x="ll" in exI)
apply (rule conjI)
apply assumption
apply clarify
apply (simp only: simp_thms triv_forall_equality True_implies_equals)
apply (rule_tac x=postnormt in exI)
apply (rule conjI)
apply simp
apply (rule conjI)
apply simp
apply clarify
apply (simp (no_asm_simp))
prefer 2
apply clarify
apply (simp only: simp_thms triv_forall_equality True_implies_equals)
apply (rule_tac x="ll!n" in exI)
apply (rule conjI)
apply (simp add: Levellist_def)
prefer 3
apply (clarify)
apply (simp (no_asm_use) only: simp_thms triv_forall_equality True_implies_equals)
proof -
fix var p rep mark vara lowa higha pa levellista repa marka nexta varb ll
nb pret prebdt and low :: "ref ⇒ ref" and
high :: "ref ⇒ ref" and repb :: "ref ⇒ ref"
assume ll: "Levellist levellista nexta ll"
assume wf_lla: "wf_ll pret ll var"
assume length_lla: "length levellista = var p + 1"
assume ord_pret: "ordered pret var"
assume pnN: " p ≠ Null"
assume rep_repb_nc:
"∀pt i. pt ∉ set_of pret ∨ nb ≤ i ∧ pt ∈ set (ll ! i) ∧
i < length levellista
⟶ rep pt = repb pt"
assume wf_marking_prop: " wf_marking pret mark marka (¬ mark p)"
assume pret_dag: "Dag p low high pret"
assume prebdt: "bdt pret var = Some prebdt"
assume not_nbslla: "¬ nb < length levellista"
assume nb_le_lla: " nb ≤ length levellista"
assume normalize_prop: "∀no∈Nodes nb ll.
var (repb no) ≤ var no ∧
(∃not nort. Dag (repb no) (repb ∝ low) (repb ∝ high) nort ∧
Dag no low high not ∧ reduced nort ∧ ordered nort var ∧
set_of nort ⊆ repb ` Nodes nb ll ∧
(∀no∈set_of nort. repb no = no) ∧
(∃nobdt norbdt. bdt not var = Some nobdt ∧
bdt nort var = Some norbdt ∧ nobdt ∼ norbdt))"
assume repbNodes_in_Nodes: " repb ` Nodes nb ll ⊆ Nodes nb ll"
assume shared_mult_dags:
"∀t1 t2. t1 ∈ Dags (repb ` Nodes nb ll) (repb ∝ low) (repb ∝ high) ∧
t2 ∈ Dags (repb ` Nodes nb ll) (repb ∝ low) (repb ∝ high)
⟶ isomorphic_dags_eq t1 t2 var"
show "(∃postnormt. Dag (repb p) (repb ∝ low) (repb ∝ high) postnormt ∧
reduced postnormt ∧ shared postnormt var ∧
ordered postnormt var ∧ set_of postnormt ⊆ set_of pret ∧
(∃postnormbdt.
bdt postnormt var = Some postnormbdt ∧ prebdt ∼ postnormbdt) ∧
(∀ no ∈ set_of postnormt. repb no = no)) ∧
ordered pret var ∧ p ≠ Null ∧
(∀pt. pt ∉ set_of pret ⟶ rep pt = repb pt) ∧
(∀no. no ∈ set_of pret ⟶ marka no = (¬ mark p))"
proof -
from ll have length_ll_eq: "length levellista = length ll"
by (simp add: Levellist_length)
from rep_repb_nc have rep_nc_post: "∀pt. pt ∉ set_of pret ⟶ rep pt = repb pt"
by auto
from pnN pret_dag obtain lt rt where pret_def: "pret = Node lt p rt"
by auto
from wf_marking_prop pret_def
have marking_inverted: "(∀no. no ∈ set_of pret ⟶ marka no = (¬ mark p))"
by (simp add: wf_marking_def)
from not_nbslla nb_le_lla have nb_length_lla: "nb = length levellista"
by simp
with length_lla have varp_s_nb: "var p < nb"
by simp
from pret_def have p_in_pret: "p ∈ set_of pret"
by simp
with wf_lla have "p ∈ set (ll ! (var p))"
by (simp add: wf_ll_def)
with varp_s_nb have p_in_Nodes: "p ∈ Nodes nb ll"
by (auto simp add: Nodes_def)
with normalize_prop obtain not nort where
varrepno_varno: " var (repb p) ≤ var p" and
nort_dag: "Dag (repb p) (repb ∝ low) (repb ∝ high) nort" and
not_dag: " Dag p low high not" and
red_nort: "reduced nort" and
ord_nort: "ordered nort var" and
nort_in_repNodes: " set_of nort ⊆ repb ` Nodes nb ll" and
nort_repb: "(∀no∈set_of nort. repb no = no)" and
bdt_prop: "∃nobdt norbdt. bdt not var = Some nobdt ∧ bdt nort var = Some norbdt ∧
nobdt ∼ norbdt"
by auto
from wf_lla nb_length_lla have Nodes_in_pret: "Nodes nb ll ⊆ set_of pret"
apply -
apply (rule Nodes_in_pret)
apply (auto simp add: length_ll_eq)
done
from pret_dag wf_lla nb_length_lla have "Null ∉ Nodes nb ll"
apply -
apply (rule Null_notin_Nodes)
apply (auto simp add: length_ll_eq)
done
with p_in_Nodes repbNodes_in_Nodes have rp_nNull: "repb p ≠ Null"
by auto
with nort_dag have nort_nTip: "nort≠ Tip"
by auto
have "∃postnormt. Dag (repb p) (repb ∝ low) (repb ∝ high) postnormt ∧
reduced postnormt ∧ shared postnormt var ∧
ordered postnormt var ∧ set_of postnormt ⊆ set_of pret ∧
(∃postnormbdt.
bdt postnormt var = Some postnormbdt ∧ prebdt ∼ postnormbdt) ∧
(∀no ∈ set_of postnormt. repb no = no)"
proof (rule_tac x=nort in exI)
from nort_in_repNodes repbNodes_in_Nodes Nodes_in_pret
have nort_in_pret: "set_of nort ⊆ set_of pret"
by blast
from not_dag pret_dag have not_pret: "not = pret"
by (simp add: Dag_unique)
with bdt_prop prebdt have pret_bdt_prop:
"∃postnormbdt.
bdt nort var = Some postnormbdt ∧ prebdt ∼ postnormbdt"
by auto
from shared_mult_dags have "shared nort var"
proof (auto simp add: shared_def isomorphic_dags_eq_def)
fix st1 st2 bdt1
assume shared_imp:
"∀t1 t2. t1∈Dags (repb ` Nodes nb ll) (repb ∝ low) (repb ∝ high) ∧
t2 ∈ Dags (repb ` Nodes nb ll) (repb ∝ low) (repb ∝ high)
⟶
(∃bdt1. bdt t1 var = Some bdt1 ∧ bdt t2 var = Some bdt1) ⟶ t1 = t2"
assume st1_nort: " st1 ≤ nort"
assume st2_nort: "st2 ≤ nort"
assume bdt_st1: "bdt st1 var = Some bdt1"
assume bdt_st2: " bdt st2 var = Some bdt1"
from nort_in_repNodes nort_dag nort_nTip
have nort_in_DagsrNodes:
"nort ∈ Dags (repb `(Nodes nb ll)) (repb ∝ low) (repb ∝ high)"
apply -
apply (rule DagsI)
apply auto
done
show "st1 = st2"
proof (cases st1)
case Tip
note st1_Tip=this
with bdt_st1 bdt_st2 show ?thesis
by auto
next
case (Node lst1 st1p rst1)
note st1_Node=this
then have st1_nTip: "st1 ≠ Tip"
by simp
show ?thesis
proof (cases st2)
case Tip
with bdt_st1 bdt_st2 show ?thesis
by auto
next
case (Node lst2 st2p rst2)
note st2_Node=this
then have st2_nTip: "st2 ≠ Tip"
by simp
from nort_in_DagsrNodes st1_nort ord_nort wf_lla st1_nTip
have st1_in_Dags:
"st1 ∈ Dags (repb ` Nodes nb ll) (repb ∝ low) (repb ∝ high)"
apply -
apply (rule Dags_subdags)
apply auto
done
from nort_in_DagsrNodes st2_nort ord_nort wf_lla st2_nTip
have st2_in_Dags:
"st2 ∈ Dags (repb ` Nodes nb ll) (repb ∝ low) (repb ∝ high)"
apply -
apply (rule Dags_subdags)
apply auto
done
from st1_in_Dags st2_in_Dags bdt_st1 bdt_st2 shared_imp show "st1=st2"
by simp
qed
qed
qed
with nort_dag red_nort ord_nort nort_in_pret pret_bdt_prop nort_repb
show "Dag (repb p) (repb ∝ low) (repb ∝ high) nort ∧
reduced nort ∧ shared nort var ∧ ordered nort var ∧
set_of nort ⊆ set_of pret ∧
(∃postnormbdt.
bdt nort var = Some postnormbdt ∧ prebdt ∼ postnormbdt) ∧
(∀no ∈ set_of nort. repb no = no)"
apply -
apply (intro conjI)
apply assumption+
done
qed
with wf_lla length_lla ord_pret pnN rep_nc_post marking_inverted
show ?thesis
by simp
qed
next
fix var low high p rep levellist marka "next"
nexta lowb highb pb levellista ll repa pret prebdt
and mark::"ref⇒bool" and postnormt postnormbdt
assume ll: "Levellist levellista nexta ll"
assume repoint_spec:
"Dag pb lowb highb postnormt"
"∀pt. pt ∉ set_of postnormt ⟶ low pt = lowb pt ∧ high pt = highb pt"
assume pret_dag: "Dag p low high pret"
assume ord_pret: "ordered pret var"
assume pnN: " p ≠ Null"
assume onemark_pret:
"∀n. n ∈ set_of pret ⟶ mark n = mark p" (is "∀n. ?in_pret n ⟶ ?eq_mark_p n")
assume pret_bdt: " bdt pret var = Some prebdt"
assume wf_ll: "wf_ll pret ll var" and
length_ll:"length levellist =var p + 1" and
wf_marking_ll: "wf_marking pret mark marka (¬ mark p)"
assume
postnormt_dag: "Dag (repa p) (repa ∝ low) (repa ∝ high) postnormt" and
reduced_postnormt: "reduced postnormt" and
shared_postnormt: "shared postnormt var" and
ordered_postnormt: "ordered postnormt var" and
subset_pret: "set_of postnormt ⊆ set_of pret"and
sim_bdt: "bdt postnormt var = Some postnormbdt" "prebdt ∼ postnormbdt" and
postdag_repa: "∀no ∈ set_of postnormt. repa no = no" and
rep_eq: "∀pt. pt ∉ set_of pret ⟶ rep pt = repa pt" and
pret_marked: "∀no. no ∈ set_of pret ⟶ marka no = (¬ mark p)"
assume unmodif_next: "∀p. p ∉ set_of pret ⟶ next p = nexta p"
show "(∀pt. pt ∉ set_of pret
⟶ low pt = lowb pt ∧ high pt = highb pt ∧
mark pt = marka pt ) "
proof -
from ll have length_ll_eq: "length levellista = length ll"
by (simp add: Levellist_length)
from repoint_spec pnN subset_pret
have repoint_nc: "(∀pt. pt ∉ set_of pret
⟶ low pt = lowb pt ∧ high pt = highb pt) ∧ Dag pb lowb highb postnormt"
by auto
then have lowhigh_b_eq: "∀pt. pt ∉ set_of pret
⟶ low pt = lowb pt ∧ high pt = highb pt"
by fastforce
from wf_marking_ll pret_dag pnN
have mark_b_eq: "∀pt. pt ∉ set_of pret ⟶ mark pt = marka pt"
apply -
apply (simp add: wf_marking_def)
apply (split dag.splits)
apply simp
apply (rule allI)
apply (rule impI)
apply (elim conjE)
apply (erule_tac x=pt in allE)
apply fastforce
done
with lowhigh_b_eq rep_eq unmodif_next
have pret_nc: "∀pt. pt ∉ set_of pret
⟶ rep pt = repa pt ∧ low pt = lowb pt ∧ high pt = highb pt ∧
mark pt = marka pt ∧ next pt = nexta pt"
by blast
from pret_nc
show ?thesis
by fastforce
qed
next
fix var low high p rep mark pret prebdt levellist ll "next" marka n repc
and repb :: "ref ⇒ ref"
assume ll: "Levellist levellist next ll"
assume pret_dag: "Dag p low high pret"
assume ord_pret: " ordered pret var"
assume pnN: "p ≠ Null"
assume prebdt_pret: "bdt pret var = Some prebdt"
assume wf_ll: "wf_ll pret ll var"
assume lll: "length levellist = var p + 1"
assume n_Suc_var_p: "n < var p + 1"
assume wf_marking_m_ma: "wf_marking pret mark marka (¬ mark p)"
assume rep_nc: "∀pt i.
pt ∉ set_of pret ∨ n ≤ i ∧ pt ∈ set (ll ! i) ∧ i < var p + 1 ⟶
rep pt = repb pt"
assume repbNodes_in_Nodes: "repb ` Nodes n ll ⊆ Nodes n ll"
assume
normalize_prop: "∀no∈Nodes n ll.
var (repb no) ≤ var no ∧
(∃not nort. Dag (repb no) (repb ∝ low) (repb ∝ high) nort ∧
Dag no low high not ∧ reduced nort ∧ ordered nort var ∧
set_of nort ⊆ repb ` Nodes n ll ∧
(∀no∈set_of nort. repb no = no) ∧
(∃nobdt. bdt not var = Some nobdt ∧
(∃norbdt. bdt nort var = Some norbdt ∧
nobdt ∼ norbdt)))"
assume
isomorphic_dags_eq:
"∀t1 t2. t1 ∈ Dags (repb ` Nodes n ll) (repb ∝ low) (repb ∝ high)∧
t2 ∈ Dags (repb ` Nodes n ll) (repb ∝ low) (repb ∝ high)
⟶ isomorphic_dags_eq t1 t2 var"
show "(∀no∈set (ll ! n).
no ≠ Null ∧
(low no = Null) = (high no = Null) ∧
low no ∉ set (ll ! n) ∧
high no ∉ set (ll ! n) ∧
isLeaf_pt no low high = (var no ≤ 1) ∧
(low no ≠ Null ⟶ repb (low no) ≠ Null) ∧ (repb ∝ low) no ∉ set (ll ! n)) ∧
(∀no1∈set (ll ! n). ∀no2∈set (ll ! n). var no1 = var no2) ∧
(∀repa. (∀no. no ∉ set (ll ! n) ⟶ repb no = repa no) ∧
(∀no∈set (ll ! n).
repa no ≠ Null ∧
(if (repa ∝ low) no = (repa ∝ high) no ∧ low no ≠ Null
then repa no = (repa ∝ low) no
else repa no ∈ set (ll ! n) ∧
repa (repa no) = repa no ∧
(∀no1∈set (ll ! n).
((repa ∝ high) no1 = (repa ∝ high) no ∧
(repa ∝ low) no1 = (repa ∝ low) no) =
(repa no = repa no1)))) ⟶
var p + 1 - (n + 1) < var p + 1 - n ∧
n + 1 ≤ var p + 1 ∧
(∀pt i. pt ∉ set_of pret ∨ (n + 1 ≤ i ∧ pt ∈ set (ll ! i) ∧ i < var p + 1) ⟶
rep pt = repa pt) ∧
repa ` Nodes (n + 1) ll ⊆ Nodes (n + 1) ll ∧
(∀no∈Nodes (n + 1) ll.
var (repa no) ≤ var no ∧
(∃not nort.
Dag (repa no) (repa ∝ low) (repa ∝ high) nort ∧
Dag no low high not ∧
reduced nort ∧
ordered nort var ∧
set_of nort ⊆ repa ` Nodes (n + 1) ll ∧
(∀no∈set_of nort. repa no = no) ∧
(∃nobdt.
bdt not var = Some nobdt ∧
(∃norbdt. bdt nort var = Some norbdt ∧ nobdt ∼ norbdt)))) ∧
(∀t1 t2.
t1 ∈ Dags (repa ` Nodes (n + 1) ll) (repa ∝ low) (repa ∝ high) ∧
t2 ∈ Dags (repa ` Nodes (n + 1) ll) (repa ∝ low) (repa ∝ high) ⟶
isomorphic_dags_eq t1 t2 var))"
proof -
from ll have length_ll_eq: "length levellist = length ll"
by (simp add: Levellist_length)
from n_Suc_var_p lll have nsll: "n < length levellist" by simp
hence nseqll: "n ≤ length levellist" by simp
have srrl_precond: "(∀no ∈ set (ll ! n).
no ≠ Null ∧
(low no = Null) = (high no = Null) ∧
low no ∉ set (ll ! n) ∧
high no ∉ set (ll ! n) ∧
isLeaf_pt no low high = (var no ≤ 1) ∧
(low no ≠ Null ⟶ repb (low no) ≠ Null) ∧
(repb ∝ low) no ∉ set (ll ! n))"
proof (intro ballI)
fix no
assume no_in_lln: "no ∈ set (ll ! n)"
with wf_ll nsll have no_in_pret_var: "no ∈ set_of pret ∧ var no = n"
by (simp add: wf_ll_def length_ll_eq)
with pret_dag have no_nNull: "no ≠ Null"
apply -
apply (rule set_of_nn)
apply auto
done
from pret_dag prebdt_pret no_in_pret_var
have balanced_no: "(low no = Null) = (high no = Null)"
apply -
apply (erule conjE)
apply (rule_tac p=p and low=low in balanced_bdt)
apply auto
done
have low_no_notin_lln: "low no ∉ set (ll ! n)"
proof (cases "low no = Null")
case True
note lno_Null=this
with balanced_no have hno_Null: "high no = Null"
by simp
show ?thesis
proof (cases "low no ∈ set (ll ! n)")
case True
with wf_ll nsll have "low no ∈ set_of pret ∧ var (low no) = n"
by (auto simp add: wf_ll_def length_ll_eq)
with pret_dag have "low no ≠ Null"
apply -
apply (rule set_of_nn)
apply auto
done
with lno_Null show ?thesis
by simp
next
assume lno_notin_lln: "low no ∉ set (ll ! n)"
then show ?thesis
by simp
qed
next
assume lno_nNull: "low no ≠ Null"
with balanced_no have hno_nNull: "high no ≠ Null"
by simp
with lno_nNull pret_dag ord_pret no_in_pret_var
have var_children_smaller: "var (low no) < var no ∧ var (high no) < var no"
apply -
apply (rule var_ordered_children)
apply auto
done
show ?thesis
proof (cases "low no ∈ set (ll ! n)")
case True
with wf_ll nsll have "low no ∈ set_of pret ∧ var (low no) = n"
by (simp add: wf_ll_def length_ll_eq)
with var_children_smaller no_in_pret_var show ?thesis
by simp
next
assume "low no ∉ set (ll ! n)"
thus ?thesis
by simp
qed
qed
have high_no_notin_lln: "high no ∉ set (ll ! n)"
proof (cases "high no = Null")
case True
note hno_Null=this
with balanced_no have lno_Null: "low no = Null"
by simp
show ?thesis
proof (cases "high no ∈ set (ll ! n)")
case True
with wf_ll nsll have "high no ∈ set_of pret ∧ var (high no) = n"
by (auto simp add: wf_ll_def length_ll_eq)
with pret_dag have "high no ≠ Null"
apply -
apply (rule set_of_nn)
apply auto
done
with hno_Null show ?thesis
by simp
next
assume hno_notin_lln: "high no ∉ set (ll ! n)"
then show ?thesis
by simp
qed
next
assume hno_nNull: "high no ≠ Null"
with balanced_no have lno_nNull: "low no ≠ Null"
by simp
with hno_nNull pret_dag ord_pret no_in_pret_var
have var_children_smaller: "var (low no) < var no ∧ var (high no) < var no"
apply -
apply (rule var_ordered_children)
apply auto
done
show ?thesis
proof (cases "high no ∈ set (ll ! n)")
case True
with wf_ll nsll have "high no ∈ set_of pret ∧ var (high no) = n"
by (simp add: wf_ll_def length_ll_eq)
with var_children_smaller no_in_pret_var show ?thesis
by simp
next
assume "high no ∉ set (ll ! n)"
thus ?thesis
by simp
qed
qed
from no_in_pret_var pret_dag no_nNull obtain not where
no_dag_ex: "Dag no low high not"
apply -
apply (rotate_tac 2)
apply (drule subnode_dag_cons)
apply (auto simp del: Dag_Ref)
done
with pret_dag prebdt_pret no_in_pret_var obtain nobdt
where nobdt_ex:
"bdt not var = Some nobdt"
apply -
apply (drule subbdt_ex_dag_def)
apply auto
done
have isLeaf_var: "isLeaf_pt no low high = (var no ≤ 1)"
proof
assume no_isLeaf: "isLeaf_pt no low high"
from nobdt_ex no_dag_ex no_isLeaf show "var no ≤ 1"
apply -
apply (rule bdt_Some_Leaf_var_le_1)
apply auto
done
next
assume varno_le_1: "var no ≤ 1"
show "isLeaf_pt no low high"
proof (cases "var no = 0")
case True
with nobdt_ex no_nNull no_dag_ex have "not = Node Tip no Tip"
apply -
apply (drule bdt_Some_var0_Zero)
apply auto
done
with no_dag_ex show "isLeaf_pt no low high"
by (simp add: isLeaf_pt_def)
next
assume "var no ≠ 0"
with varno_le_1 have "var no = 1"
by simp
with nobdt_ex no_nNull no_dag_ex have "not = Node Tip no Tip"
apply -
apply (drule bdt_Some_var1_One)
apply auto
done
with no_dag_ex show "isLeaf_pt no low high"
by (simp add: isLeaf_pt_def)
qed
qed
have repb_low_nNull: "(low no ≠ Null ⟶ repb (low no) ≠ Null)"
proof
assume lno_nNull: "low no ≠ Null"
with no_nNull no_in_pret_var pret_dag have lno_in_pret: "low no ∈ set_of pret"
apply -
apply (rule_tac low=low in subelem_set_of_low)
apply auto
done
from lno_nNull balanced_no have hno_nNull: "high no ≠ Null"
by simp
with lno_nNull pret_dag ord_pret no_in_pret_var
have var_children_smaller: "var (low no) < var no ∧ var (high no) < var no"
apply -
apply (rule var_ordered_children)
apply auto
done
with no_in_pret_var have var_lno_l_n: "var (low no) <n"
by simp
with wf_ll lno_in_pret nsll have "low no ∈ set (ll ! (var (low no)))"
by (simp add: wf_ll_def length_ll_eq)
with lno_in_pret var_lno_l_n have "low no ∈ Nodes n ll"
apply (simp add: Nodes_def)
apply (rule_tac x="var (low no)" in exI)
apply simp
done
hence "repb (low no) ∈ repb ` Nodes n ll"
by simp
with repbNodes_in_Nodes have repb_lno_in_Nodes:
"repb (low no) ∈ Nodes n ll"
by blast
from pret_dag wf_ll nsll have "Null ∉ Nodes n ll"
apply -
apply (rule Null_notin_Nodes)
apply (auto simp add: length_ll_eq)
done
with repb_lno_in_Nodes show "repb (low no) ≠ Null"
by auto
qed
have Null_notin_lln: "Null ∉ set (ll ! n)"
proof (cases "Null ∈ set (ll ! n)")
case True
with wf_ll nsll have "Null ∈ set_of pret ∧ var (Null) = n"
by (simp add: wf_ll_def length_ll_eq)
with pret_dag have "Null ≠ Null"
apply -
apply (rule set_of_nn)
apply auto
done
thus ?thesis
by auto
next
assume "Null ∉ set (ll ! n)"
thus ?thesis
by simp
qed
have "(repb ∝ low) no ∉ set (ll ! n)"
proof (cases "low no = Null")
case True
with Null_notin_lln show ?thesis
by (simp add: null_comp_def)
next
assume lno_nNull: "low no ≠ Null"
with no_nNull no_in_pret_var pret_dag have lno_in_pret: "low no ∈ set_of pret"
apply -
apply (rule_tac low=low in subelem_set_of_low)
apply auto
done
from lno_nNull have propto_eq_comp: "(repb ∝ low) no = repb (low no)"
by (simp add: null_comp_def)
from lno_nNull balanced_no have hno_nNull: "high no ≠ Null"
by simp
with lno_nNull pret_dag ord_pret no_in_pret_var
have var_children_smaller: "var (low no) < var no ∧ var (high no) < var no"
apply -
apply (rule var_ordered_children)
apply auto
done
with no_in_pret_var have var_lno_l_n: "var (low no) <n"
by simp
with wf_ll lno_in_pret nsll have "low no ∈ set (ll ! (var (low no)))"
by (simp add: wf_ll_def length_ll_eq)
with lno_in_pret var_lno_l_n have lno_in_Nodes_n: "low no ∈ Nodes n ll"
apply (simp add: Nodes_def)
apply (rule_tac x="var (low no)" in exI)
apply simp
done
hence "repb (low no) ∈ repb ` Nodes n ll"
by simp
with repbNodes_in_Nodes have repb_lno_in_Nodes:
"repb (low no) ∈ Nodes n ll"
by blast
with lno_in_Nodes_n normalize_prop have "var (repb (low no)) ≤ var (low no)"
by auto
with var_lno_l_n have var_rep_lno_l_n: " var (repb (low no)) < n"
by simp
with repb_lno_in_Nodes have "∃ k < n. repb (low no) ∈ set (ll ! k)"
by (auto simp add: Nodes_def)
with wf_ll propto_eq_comp nsll show " (repb ∝ low) no ∉ set (ll ! n)"
apply -
apply (erule exE)
apply (rule_tac i=k and j=n in no_in_one_ll)
apply (auto simp add: length_ll_eq)
done
qed
with no_nNull balanced_no low_no_notin_lln high_no_notin_lln isLeaf_var repb_low_nNull
show " no ≠ Null ∧
(low no = Null) = (high no = Null) ∧
low no ∉ set (ll ! n) ∧ high no ∉ set (ll ! n) ∧
isLeaf_pt no low high = (var no ≤ 1) ∧
(low no ≠ Null ⟶ repb (low no) ≠ Null) ∧
(repb ∝ low) no ∉ set (ll ! n)"
by auto
qed
have all_nodes_same_var: "∀no1 ∈ set (ll ! n). ∀no2 ∈ set (ll ! n). var no1 = var no2"
proof (intro ballI impI)
fix no1 no2
assume "no1 ∈ set (ll ! n)"
with wf_ll nsll have var_lln_i: "var no1 = n"
by (simp add: wf_ll_def length_ll_eq)
assume "no2 ∈ set (ll ! n)"
with wf_ll nsll have "var no2 = n"
by (simp add: wf_ll_def length_ll_eq)
with var_lln_i show " var no1 = var no2"
by simp
qed
have "(∀repa. (∀no. no ∉ set (ll ! n) ⟶ repb no = repa no) ∧
(∀no∈set (ll ! n).
repa no ≠ Null ∧
(if (repa ∝ low) no = (repa ∝ high) no ∧ low no ≠ Null
then repa no = (repa ∝ low) no
else repa no ∈ set (ll ! n) ∧
repa (repa no) = repa no ∧
(∀no1∈set (ll ! n).
((repa ∝ high) no1 = (repa ∝ high) no ∧
(repa ∝ low) no1 = (repa ∝ low) no) =
(repa no = repa no1)))) ⟶
var p + 1 - (n + 1) < var p + 1 - n ∧
n + 1 ≤ var p + 1 ∧
(∀pt i. pt ∉ set_of pret ∨ (n + 1 ≤ i ∧ pt ∈ set (ll ! i) ∧ i < var p + 1) ⟶
rep pt = repa pt) ∧
repa ` Nodes (n + 1) ll ⊆ Nodes (n + 1) ll ∧
(∀no∈Nodes (n + 1) ll.
var (repa no) ≤ var no ∧
(∃not nort.
Dag (repa no) (repa ∝ low) (repa ∝ high) nort ∧
Dag no low high not ∧
reduced nort ∧
ordered nort var ∧
set_of nort ⊆ repa ` Nodes (n + 1) ll ∧
(∀no∈set_of nort. repa no = no) ∧
(∃nobdt.
bdt not var = Some nobdt ∧
(∃norbdt. bdt nort var = Some norbdt ∧ nobdt ∼ norbdt)))) ∧
(∀t1 t2.
t1 ∈ Dags (repa ` Nodes (n + 1) ll) (repa ∝ low) (repa ∝ high) ∧
t2 ∈ Dags (repa ` Nodes (n + 1) ll) (repa ∝ low) (repa ∝ high) ⟶
isomorphic_dags_eq t1 t2 var))"
(is "(∀repc. ?srrl_post repc ⟶ ?norm_inv repc) ")
proof (intro allI impI, elim conjE)
fix repc
assume repbc_nc: "∀no. no ∉ set (ll ! n) ⟶ repb no = repc no"
assume rep_prop: " ∀no∈set (ll ! n).
repc no ≠ Null ∧
(if (repc ∝ low) no = (repc ∝ high) no ∧ low no ≠ Null
then repc no = (repc ∝ low) no
else repc no ∈ set (ll ! n) ∧
repc (repc no) = repc no ∧
(∀no1∈set (ll ! n).
((repc ∝ high) no1 = (repc ∝ high) no ∧
(repc ∝ low) no1 = (repc ∝ low) no) =
(repc no = repc no1)))"
show "?norm_inv repc"
proof -
from n_Suc_var_p have termi: "var p + 1 - (n + 1) < var p + 1 - n"
by arith
from wf_ll repbc_nc nsll
have Nodes_n_rep_nc: "∀p. p ∈ Nodes n ll ⟶ repb p = repc p"
apply -
apply (rule allI)
apply (rule impI)
apply (simp add: Nodes_def)
apply (erule exE)
apply (erule_tac x=p in allE)
apply (drule_tac i=x and j=n in no_in_one_ll)
apply (auto simp add: length_ll_eq)
done
from repbNodes_in_Nodes
have Nodes_n_rep_in_Nodesn:
"∀ p. p ∈ Nodes n ll ⟶ repb p ∈ Nodes n ll"
by auto
from wf_ll nsll have "Nodes n ll ⊆ set_of pret"
apply -
apply (rule Nodes_in_pret)
apply (auto simp add: length_ll_eq)
done
with Nodes_n_rep_in_Nodesn
have Nodes_n_rep_in_pret: "∀p. p ∈ Nodes n ll ⟶ repb p ∈ set_of pret"
apply -
apply (intro allI impI)
apply blast
done
have Nodes_repbc_Dags_eq: "∀p t. p ∈ Nodes n ll
⟶ Dag (repb p) (repb ∝ low) (repb ∝ high) t =
Dag (repc p) (repc ∝ low) (repc ∝ high) t"
proof (intro allI impI)
fix p t
assume p_in_Nodes: " p ∈ Nodes n ll"
then have repp_nc: "repb p = repc p"
by (rule Nodes_n_rep_nc [rule_format])
from p_in_Nodes normalize_prop obtain nort where
nort_repb_dag: "Dag (repb p) (repb ∝ low) (repb ∝ high) nort" and
nort_in_repbNodes: "set_of nort ⊆ repb ` Nodes n ll"
apply -
apply (erule_tac x=p in ballE)
prefer 2
apply auto
done
from nort_in_repbNodes repbNodes_in_Nodes
have nort_in_Nodesn: "set_of nort ⊆ Nodes n ll"
by blast
from pret_dag wf_ll nsll have "Null ∉ Nodes n ll"
apply -
apply (rule Null_notin_Nodes)
apply (auto simp add: length_ll_eq)
done
with p_in_Nodes repbNodes_in_Nodes have repp_nNull: "repb p ≠ Null"
by auto
from nort_repb_dag repp_nc
have nort_repbc_dag: "Dag (repc p) (repb ∝ low) (repb ∝ high) nort"
by simp
from nort_in_Nodesn have "∀x ∈ set_of nort. x ∈ Nodes n ll"
apply -
apply (rule ballI)
apply blast
done
with wf_ll nsll have "∀x ∈ set_of nort. x ∈ set_of pret ∧ var x < n"
apply -
apply (rule ballI)
apply (rule wf_ll_Nodes_pret)
apply (auto simp add: length_ll_eq)
done
with pret_dag prebdt_pret nort_repbc_dag ord_pret wf_ll nsll repbc_nc
have
"∀ x ∈ set_of nort. (repc ∝ low) x = (repb ∝ low) x ∧
(repc ∝ high) x = (repb ∝ high) x"
apply -
apply (rule nort_null_comp)
apply (auto simp add: length_ll_eq)
done
with nort_repbc_dag repp_nc
have "Dag (repc p) (repb ∝ low) (repb ∝ high) nort =
Dag (repc p) (repc ∝ low) (repc ∝ high) nort"
apply -
apply (rule heaps_eq_Dag_eq)
apply (rule ballI)
apply (erule_tac x=x in ballE)
apply (elim conjE)
apply (rule conjI)
apply auto
done
with nort_repbc_dag repp_nc show
"Dag (repb p) (repb ∝ low) (repb ∝ high) t =
Dag (repc p) (repc ∝ low) (repc ∝ high) t"
apply auto
apply (rotate_tac 2)
apply (frule_tac Dag_unique)
apply (rotate_tac 1)
apply simp
apply simp
apply (frule Dag_unique)
apply (rotate_tac 3)
apply simp
apply simp
done
qed
from rep_prop have repbc_changes: "∀no∈set (ll ! n).
repc no ≠ Null ∧
(if (repc ∝ low) no = (repc ∝ high) no ∧ low no ≠ Null
then repc no = (repc ∝ low) no
else repc no ∈ set (ll ! n) ∧ repc (repc no) = repc no ∧
(∀no1∈set (ll ! n). ((repc ∝ high) no1 = (repc ∝ high) no ∧
(repc ∝ low) no1 = (repc ∝ low) no) = (repc no = repc no1)))"
by blast
from nsll lll have n_var_prop: "n + 1 <= var p + 1"
by simp
from rep_nc have Sucn_repb_nc: "(∀pt. pt ∉ set_of pret ∨
(∃i. n + 1 ≤ i ∧ pt ∈ set (ll ! i) ∧ i < var p + 1)
⟶ rep pt = repb pt)"
apply -
apply (intro allI impI)
apply (erule_tac x=pt in allE)
apply auto
apply (rule_tac x="i" in exI)
apply auto
done
have repc_nc:
"(∀pt. pt ∉ set_of pret ∨
(∃i. n + 1 ≤ i ∧ pt ∈ set (ll ! i) ∧ i < var p + 1)
⟶ rep pt = repc pt)"
proof (intro allI impI)
fix pt
assume pt_notin_lower_ll: "pt ∉ set_of pret ∨
(∃i. n + 1 ≤ i ∧ pt ∈ set (ll ! i) ∧ i < var p + 1)"
show "rep pt = repc pt"
proof (cases "pt ∉ set_of pret")
case True
with wf_ll nsll have "pt ∉ set (ll ! n)"
apply (simp add: wf_ll_def length_ll_eq)
apply (case_tac "pt ∈ set (ll ! n)")
apply (subgoal_tac "pt ∈ set_of pret")
apply (auto)
done
with repbc_nc have "repb pt = repc pt"
by auto
with Sucn_repb_nc True show ?thesis
by auto
next
assume pt_in_pret: "¬ pt ∉ set_of pret"
with pt_notin_lower_ll have pt_in_higher_ll:
"∃i. n + 1 ≤ i ∧ pt ∈ set (ll ! i) ∧ i < var p + 1"
by simp
with nsll wf_ll lll have pt_notin_lln: "pt ∉ set (ll ! n)"
apply -
apply (erule exE)
apply (rule_tac i=i and j=n in no_in_one_ll)
apply (auto simp add: length_ll_eq)
done
with repbc_nc have "repb pt = repc pt"
by auto
with Sucn_repb_nc pt_in_higher_ll show ?thesis
by auto
qed
qed
from wf_ll nsll
have Nodesn_notin_lln: "∀no ∈ Nodes n ll. no ∉ set (ll ! n)"
apply (simp add: Nodes_def)
apply clarify
apply (drule no_in_one_ll)
apply (auto simp add: length_ll_eq)
done
with repbc_nc
have Nodesn_repnc: "∀no ∈ Nodes n ll. repb no = repc no"
apply -
apply (rule ballI)
apply (erule_tac x=no in allE)
apply simp
done
then have repbNodes_repcNodes:
"repb `(Nodes n ll) = repc `(Nodes n ll)"
apply -
apply rule
apply blast
apply rule
apply (erule imageE)
apply (erule_tac x=xa in ballE)
prefer 2
apply simp
apply rule
apply auto
done
have repcNodes_in_Nodes:
"repc ` Nodes (n + 1) ll ⊆ Nodes (n + 1) ll"
proof
fix x
assume x_in_repcNodesSucn: " x ∈ repc ` Nodes (n + 1) ll"
show "x ∈ Nodes (n + 1) ll"
proof (cases "x ∈ repc `Nodes n ll")
case True
with repbNodes_repcNodes repbNodes_in_Nodes have "x ∈ Nodes n ll"
by auto
with Nodes_subset show ?thesis
by auto
next
assume " x ∉ repc `Nodes n ll"
with x_in_repcNodesSucn have x_in_repclln: "x ∈ repc `set (ll ! n)"
apply (auto simp add: Nodes_def)
apply (case_tac "k<n")
apply auto
apply (case_tac "k = n")
apply simp
apply arith
done
from x_in_repclln show ?thesis
proof (elim imageE)
fix y
assume x_repcy: "x = repc y"
assume y_in_repclln: "y ∈ set (ll ! n)"
from rep_prop y_in_repclln obtain
repcy_nNull: "repc y ≠ Null" and
red_prop: "(repc ∝ low) y = (repc ∝ high) y ∧
low y ≠ Null ⟶ repc y = (repc ∝ high) y" and
share_prop: "((repc ∝ low) y = (repc ∝ high) y ⟶ low y = Null)
⟶ repc y ∈ set (ll ! n) ∧ repc (repc y) = repc y ∧
(∀no1∈set (ll ! n).
((repc ∝ high) no1 = (repc ∝ high) y ∧
(repc ∝ low) no1 = (repc ∝ low) y) = (repc y = repc no1))"
using [[simp_depth_limit = 4]]
by auto
from wf_ll nsll y_in_repclln obtain
y_in_pret: "y ∈ set_of pret" and
vary_n: "var y = n"
by (auto simp add: wf_ll_def length_ll_eq)
from y_in_pret pret_dag have y_nNull: "y ≠ Null"
apply -
apply (rule set_of_nn)
apply auto
done
show "x ∈ Nodes (n + 1) ll"
proof (cases "low y = Null")
case True
from pret_dag prebdt_pret True y_in_pret
have highy_Null: "high y = Null"
apply -
apply (drule balanced_bdt)
apply auto
done
with share_prop True obtain
repcy_in_llb: "repc y ∈ set (ll ! n)" and
rry_ry: " repc (repc y) = repc y" and
y_other_node_prop: "∀no1∈set (ll ! n).
((repc ∝ high) no1 = (repc ∝ high) y ∧
(repc ∝ low) no1 = (repc ∝ low) y) = (repc y = repc no1)"
by simp
from repcy_in_llb x_repcy show ?thesis
by (auto simp add: Nodes_def)
next
assume lowy_nNull: "low y ≠ Null"
with pret_dag prebdt_pret y_in_pret
have highy_nNull: "high y ≠ Null"
apply -
apply (drule balanced_bdt)
apply auto
done
show ?thesis
proof (cases "(repc ∝ low) y = (repc ∝ high) y")
case True
with red_prop lowy_nNull have "repc y = (repc ∝ high) y"
by auto
with highy_nNull have red_repc_y: "repc y = repc (high y)"
by (simp add: null_comp_def)
from pret_dag ord_pret y_in_pret lowy_nNull highy_nNull
have "var (low y) < var y ∧ var (high y) < var y"
apply -
apply (rule var_ordered_children)
apply auto
done
with vary_n have varhighy: "var (high y) < n"
by auto
from y_in_pret y_nNull highy_nNull pret_dag
have "high y ∈ set_of pret"
apply -
apply (drule subelem_set_of_high)
apply auto
done
with wf_ll varhighy have "high y ∈ Nodes n ll"
by (auto simp add: wf_ll_def Nodes_def)
with red_repc_y have "repc y ∈ repc `Nodes n ll"
by simp
with x_repcy have "x ∈ repc `Nodes n ll"
by simp
with repbNodes_repcNodes repbNodes_in_Nodes
have "x ∈ Nodes n ll"
by auto
with Nodes_subset show ?thesis
by auto
next
assume "(repc ∝ low) y ≠ (repc ∝ high) y"
with share_prop obtain
repcy_in_llbn: "repc y ∈ set (ll ! n)" and
rry_ry: "repc (repc y) = repc y" and
y_other_node_share: "∀no1∈set (ll ! n).
((repc ∝ high) no1 = (repc ∝ high) y ∧
(repc ∝ low) no1 = (repc ∝ low) y) = (repc y = repc no1)"
by auto
with repcy_in_llbn x_repcy have "x ∈ set (ll ! n)"
by auto
then show ?thesis
by (auto simp add: Nodes_def)
qed
qed
qed
qed
qed
have "(∀no∈Nodes (n + 1) ll.
var (repc no) ≤ var no ∧
(∃not nort. Dag (repc no) (repc ∝ low) (repc ∝ high) nort ∧
Dag no low high not ∧
reduced nort ∧ ordered nort var ∧
set_of nort ⊆ repc ` Nodes (n + 1) ll ∧
(∀no∈set_of nort. repc no = no) ∧
(∃nobdt. bdt not var = Some nobdt ∧
(∃norbdt. bdt nort var = Some norbdt ∧ nobdt ∼ norbdt))))"
(is "∀no∈Nodes (n + 1) ll. ?Q i no")
proof (intro ballI)
fix no
assume no_in_Nodes: "no ∈ Nodes (n + 1) ll"
from wf_ll no_in_Nodes nsll have no_in_pret: "no ∈ set_of pret"
apply (simp add: wf_ll_def Nodes_def length_ll_eq)
apply (erule conjE)
apply (thin_tac "∀q. q ∈ set_of pret ⟶ q ∈ set (ll ! var q)")
apply (erule exE)
apply (erule_tac x=x in allE)
apply (erule impE)
apply arith
apply (erule_tac x=no in ballE)
apply auto
done
from pret_dag no_in_pret have nonNull: "no≠ Null"
apply -
apply (rule set_of_nn [rule_format])
apply auto
done
show "?Q i no"
proof (cases "no ∈ Nodes n ll")
case True
note no_in_Nodesn=this
with wf_ll nsll no_in_Nodes
have no_notin_llbn: "no ∉ set (ll ! n)"
apply -
apply (simp add: Nodes_def length_ll_eq)
apply (elim exE)
apply (drule_tac ?i=xa and ?j=n in no_in_one_ll)
apply arith
apply simp
apply auto
done
with repbc_nc have repb_no_eq_repc_no: "repb no = repc no"
by simp
from repbc_nc no_in_Nodes no_notin_llbn normalize_prop True
have varrep_eq_var: "var (repc no) ≤ var no"
apply -
apply (erule_tac x=no in ballE)
prefer 2
apply simp
apply (erule_tac x=no in allE)
apply simp
done
moreover
from True normalize_prop no_in_Nodes obtain not nort where
nort_dag: "Dag (repb no) (repb ∝ low) (repb ∝ high) nort" and
ord_nort: "ordered nort var" and
subset_nort_not: "set_of nort ⊆ repb `(Nodes n ll)" and
not_dag: " Dag no low high not" and
red_nort: "reduced nort" and
nort_repb: "(∀no∈set_of nort. repb no = no)" and
bdt_prop: "∃nobdt norbdt. bdt not var = Some nobdt ∧
bdt nort var = Some norbdt ∧ nobdt ∼ norbdt"
by blast
moreover
from Nodesn_notin_lln repbc_nc nort_repb subset_nort_not repbNodes_in_Nodes
have nort_repc:
"(∀no∈set_of nort. repc no = no)"
apply auto
apply (subgoal_tac "no ∈ Nodes n ll")
apply fastforce
apply blast
done
moreover
from nort_dag have nortnodesnN: "(∀no. no ∈ set_of nort ⟶ no ≠ Null)"
apply -
apply (rule allI)
apply (rule impI)
apply (rule set_of_nn)
apply auto
done
moreover
have "Dag (repc no) (repc ∝ low) (repc ∝ high) nort"
proof -
from no_notin_llbn repbc_nc have repbc_no: "repc no = repb no"
by fastforce
with nort_dag
have nortrepbc_dag: "Dag (repc no) (repb ∝ low) (repb ∝ high) nort"
by simp
from wf_ll nseqll have "Nodes n ll ⊆ set_of pret"
apply -
apply (rule Nodes_levellist_subset_t)
apply assumption+
apply (simp add: length_ll_eq)
done
with repbNodes_in_Nodes subset_nort_not
have subset_nort_pret: "set_of nort ⊆ set_of pret"
by simp
have vxsn_in_pret: "∀ x ∈ set_of nort. var x < n ∧ x ∈ set_of pret"
proof (rule ballI)
fix x
assume x_in_nort: "x ∈ set_of nort"
from x_in_nort subset_nort_not repbNodes_in_Nodes
have "x ∈ Nodes n ll"
by blast
with wf_ll nsll have xsn: "var x < n"
apply (simp add: wf_ll_def Nodes_def length_ll_eq)
apply (erule conjE)
apply (thin_tac " ∀q. q ∈ set_of pret ⟶ q ∈ set (ll ! var q)")
apply (erule exE)
apply (erule_tac x=xa in allE)
apply (erule impE)
apply arith
apply (erule_tac x=x in ballE)
apply auto
done
from x_in_nort subset_nort_pret have x_in_pret: "x ∈ set_of pret"
by blast
with xsn show "var x < n ∧ x ∈ set_of pret" by simp
qed
with pret_dag prebdt_pret nortrepbc_dag ord_pret wf_ll nsll
repbc_nc
have "∀ x ∈ set_of nort. ((repc ∝ low) x = (repb ∝ low) x ∧
(repc ∝ high) x = (repb ∝ high) x)"
apply -
apply (rule nort_null_comp)
apply (auto simp add: length_ll_eq)
done
with nort_dag
have "Dag (repc no) (repc ∝ low) (repc ∝ high) nort =
Dag (repc no) (repb ∝ low) (repb ∝ high) nort"
apply -
apply (rule heaps_eq_Dag_eq)
apply simp
done
with nortrepbc_dag show ?thesis
by simp
qed
moreover
have "set_of nort ⊆ repc `(Nodes (n + 1) ll)"
proof -
have Nodesn_in_NodesSucn: "Nodes n ll ⊆ Nodes (n + 1) ll"
by (simp add: Nodes_def set_split)
then have repbNodesn_in_repbNodesSucn:
"repb `(Nodes n ll) ⊆ repb `(Nodes (n + 1) ll)"
by blast
from wf_ll nsll
have Nodes_n_notin_lln: "∀no ∈ Nodes n ll. no ∉ set (ll ! n)"
apply (simp add: Nodes_def length_ll_eq)
apply clarify
apply (drule no_in_one_ll)
apply auto
done
with repbc_nc have "∀no ∈ Nodes n ll. repb no = repc no"
apply -
apply (rule ballI)
apply (erule_tac x=no in allE)
apply simp
done
then have repbNodes_repcNodes:
"repb `(Nodes n ll) = repc `(Nodes n ll)"
apply -
apply rule
apply blast
apply rule
apply (erule imageE)
apply (erule_tac x=xa in ballE)
prefer 2
apply simp
apply rule
apply auto
done
from Nodesn_in_NodesSucn
have "repc `(Nodes n ll) ⊆ repc `(Nodes (n + 1) ll)"
by blast
with repbNodes_repcNodes subset_nort_not repbNodesn_in_repbNodesSucn
show ?thesis by simp
qed
ultimately show ?thesis
by blast
next
assume " no ∉ Nodes n ll"
with no_in_Nodes have no_in_llbn: "no ∈ set (ll ! n)"
apply (simp add: Nodes_def)
apply (erule exE)
apply (erule_tac x=x in allE)
apply (case_tac "x<n")
apply simp
apply simp
apply (elim conjE)
apply (case_tac "x=n")
apply simp
apply arith
done
with wf_ll nsll have varno: "var no = n"
by (simp add: wf_ll_def length_ll_eq)
from repbc_changes no_in_llbn
have repbcno_changes: "repc no ≠ Null ∧
((repc ∝ low) no = (repc ∝ high) no ∧ low no ≠ Null
⟶ repc no = (repc ∝ high) no) ∧
(((repc ∝ low) no = (repc ∝ high) no ⟶ low no = Null)
⟶ repc no ∈ set (ll ! n) ∧ repc (repc no) = repc no ∧
(∀no1∈set (ll ! n). ((repc ∝ high) no1 = (repc ∝ high) no ∧
(repc ∝ low) no1 = (repc ∝ low) no) = (repc no = repc no1)))"
(is "?rnonN ∧ ?repreduce ∧ ?repshare")
using [[simp_depth_limit=4]]
by (simp split: if_split)
then obtain
rnonN: "?rnonN" and
repreduce: "?repreduce" and
repshare: "?repshare"
by blast
have repcn_normalize: "var (repc no) ≤ var no ∧
(∃not nort. Dag (repc no) (repc ∝ low) (repc ∝ high) nort ∧
Dag no low high not ∧ reduced nort ∧ ordered nort var ∧
set_of nort ⊆ repc ` Nodes (n + 1) ll ∧
(∀no∈set_of nort. repc no = no) ∧
(∃nobdt. bdt not var = Some nobdt ∧
(∃norbdt. bdt nort var = Some norbdt ∧ nobdt ∼ norbdt)))"
(is "?varrep ∧ ?repcn_prop"
is "?varrep ∧
(∃not nort. ?nort_dag nort ∧ ?not_dag not ∧ ?red nort ∧
?ord nort ∧ ?nort_in_Nodes nort ∧ ?repcno_no_n nort ∧ ?bdt_equ not nort)")
proof (cases "high no = Null")
case True
note highnoNull=this
with pret_dag prebdt_pret no_in_pret
have lownoNull: "low no = Null"
apply -
apply (drule balanced_bdt)
apply assumption+
apply simp
done
with repshare have repcnoinlln:"repc no ∈ set (ll ! n)"
by simp
with wf_ll nsll have varrno_n: "var (repc no) = n"
by (simp add: wf_ll_def length_ll_eq)
with varno have varrep: "?varrep"
by simp
from wf_ll nsll no_in_llbn varrno_n
have varrno_varno: "var (repc no) = var no"
by (simp add: wf_ll_def length_ll_eq)
from wf_ll nsll repcnoinlln
have rno_in_pret: "repc no ∈ set_of pret"
by (simp add: wf_ll_def length_ll_eq)
from repcnoinlln repshare lownoNull
have reprep_eq_rep: "repc (repc no) = repc no"
by simp
with repcnoinlln repshare lownoNull
have repchildreneq:
"((repc ∝ high) (repc no) = (repc ∝ high) no ∧
(repc ∝ low) (repc no) = (repc ∝ low) no)"
by simp
have repcn_prop: "?repcn_prop"
apply -
apply (rule_tac x="(Node Tip no Tip)" in exI)
apply (rule_tac x="(Node Tip (repc no) Tip)" in exI)
apply (intro conjI)
apply simp
prefer 3
apply simp
prefer 3
apply simp
proof -
from pret_dag pnN rno_in_pret have rnonN: "repc no ≠ Null"
apply (case_tac "repc no = Null")
apply auto
done
from highnoNull repchildreneq
have rhighNull: "(repc ∝ high) (repc no) = Null"
by (simp add: null_comp_def)
from lownoNull repchildreneq
have rlowNull: "(repc ∝ low) (repc no) = Null"
by (simp add: null_comp_def)
with rhighNull rnonN
show "repc no ≠ Null ∧ (repc ∝ low) (repc no) = Null ∧
(repc ∝ high) (repc no) = Null"
by simp
next
from nonNull lownoNull highnoNull
show "?not_dag (Node Tip no Tip)"
by simp
next
from no_in_Nodes
show "set_of (Node Tip (repc no) Tip) ⊆ repc ` Nodes (n + 1) ll"
by simp
next
show "∀no∈set_of (Node Tip (repc no) Tip). repc no = no"
proof
fix pt
assume pt_in_repcLeaf: "pt ∈ set_of (Node Tip (repc no) Tip)"
with reprep_eq_rep show "repc pt = pt"
by simp
qed
next
show "?bdt_equ (Node Tip no Tip) (Node Tip (repc no) Tip)"
proof (cases "var no = 0")
case True
note vno_Null=this
then have nobdt: "bdt (Node Tip no Tip) var = Some Zero" by simp
from varrep vno_Null have varrno: "var (repc no) = 0" by simp
then have norbdt: "bdt (Node Tip (repc no) Tip) var = Some Zero" by simp
from nobdt norbdt vno_Null varrno show ?thesis
by (simp add: cong_eval_def)
next
assume vno_not_Null: "var no ≠ 0"
show ?thesis
proof (cases "var no = 1")
case True
note vno_One=this
then have nobdt: "bdt (Node Tip no Tip) var = Some One" by simp
from varrno_varno vno_One
have "bdt (Node Tip (repc no) Tip) var = Some One" by simp
with nobdt show ?thesis by (auto simp add: cong_eval_def)
next
assume vno_nOne: "var no ≠ 1"
with vno_not_Null have onesvno: "1 < var no" by simp
from nonNull lownoNull highnoNull
have no_dag: "Dag no low high (Node Tip no Tip)"
by simp
with pret_dag no_in_pret have not_in_pret: "(Node Tip no Tip) ≤ pret"
by (metis set_of_subdag)
with prebdt_pret have "∃bdt2. bdt (Node Tip no Tip) var = Some bdt2"
by (metis subbdt_ex)
with onesvno show ?thesis
by simp
qed
qed
qed
with varrep reprep_eq_rep show ?thesis by simp
next
assume hno_nNull: "high no ≠ Null"
with pret_dag prebdt_pret no_in_pret have lno_nNull: "low no ≠ Null"
by (metis balanced_bdt)
from no_in_pret nonNull hno_nNull pret_dag
have hno_in_pret: "high no ∈ set_of pret"
by (metis subelem_set_of_high)
with wf_ll
have hno_in_ll: "high no ∈ set (ll ! (var (high no)))"
by (simp add: wf_ll_def)
from pret_dag ord_pret no_in_pret lno_nNull hno_nNull
have varhnos_varno: "var (high no) < var no"
by (metis var_ordered_children)
with varno have varhnos_n: "var (high no) < n" by simp
with hno_in_ll have hno_in_Nodesn: "high no ∈ Nodes n ll"
apply (simp add: Nodes_def)
apply (rule_tac x="var (high no)" in exI)
apply simp
done
from wf_ll nsll hno_in_ll varhnos_n
have "high no ∉ set (ll ! n)"
apply -
apply (rule no_in_one_ll)
apply (auto simp add: length_ll_eq)
done
with repbc_nc have repb_repc_high: "repb (high no) = repc (high no)" by simp
with normalize_prop hno_in_Nodesn varhnos_varno varno
have high_normalize: "var (repc (high no)) ≤ var (high no) ∧
(∃not nort. Dag (repc (high no)) (repb ∝ low) (repb ∝ high) nort ∧
Dag (high no) low high not ∧ reduced nort ∧
ordered nort var ∧ set_of nort ⊆ repb `(Nodes n ll) ∧
(∀no∈set_of nort. repb no = no) ∧
(∃nobdt norbdt. bdt not var = Some nobdt ∧ bdt nort var =
Some norbdt ∧ nobdt ∼ norbdt))"
(is "?varrep_high ∧
(∃not nort. ?repbchigh_dag nort ∧ ?high_dag not ∧
?redhigh nort ∧ ?ordhigh nort ∧ ?rephigh_in_Nodes nort ∧
?repbno_no nort ∧ ?highdd_prop not nort)"
is "?varrep_high ∧ ?not_nort_prop")
apply simp
apply (erule_tac x="high no" in ballE)
apply (simp del: Dag_Ref)
apply simp
done
then have varrep_high: "?varrep_high" by simp
from varhnos_n varrep_high have varrephno_s_n:
"var (repc (high no)) < n"
by simp
from Nodes_subset
have "Nodes n ll ⊆ Nodes (Suc n) ll"
by auto
with hno_in_Nodesn repcNodes_in_Nodes
have "repc (high no) ∈ Nodes (Suc n) ll"
apply simp
apply blast
done
with wf_ll nsll have "repc (high no) ∈ set_of pret"
apply (simp add: wf_ll_def Nodes_def length_ll_eq)
apply (elim conjE exE)
apply (thin_tac " ∀q. q ∈ set_of pret ⟶ q ∈ set (ll ! var q)")
apply (erule_tac x=x in allE)
apply (erule impE)
apply simp
apply (erule_tac x="repc (high no)" in ballE)
apply auto
done
with wf_ll varrephno_s_n
have "∃ k<n. repc (high no) ∈ set (ll ! k)"
by (auto simp add: wf_ll_def)
with wf_ll nsll have "repc (high no) ∉ set (ll ! n)"
apply -
apply (erule exE)
apply (rule_tac i=k and j=n in no_in_one_ll)
apply (auto simp add: length_ll_eq)
done
with repbc_nc
have repbchigh_idem: "repb (repc (high no)) = repc (repc (high no))"
by auto
from high_normalize
have not_nort_prop_high: "?not_nort_prop" by (simp del: Dag_Ref)
from not_nort_prop_high obtain hnot where high_dag: "?high_dag hnot"
by auto
from wf_ll nsll
have "∀no ∈ Nodes n ll. no ∉ set (ll ! n)"
apply (simp add: Nodes_def length_ll_eq)
apply clarify
apply (drule no_in_one_ll)
apply auto
done
with repbc_nc have "∀no ∈ Nodes n ll. repb no = repc no"
apply -
apply (rule ballI)
apply (erule_tac x=no in allE)
apply simp
done
then
have repbNodes_repcNodes:
"repb `(Nodes n ll) = repc `(Nodes n ll)"
apply -
apply rule
apply blast
apply rule
apply (erule imageE)
apply (erule_tac x=xa in ballE)
prefer 2
apply simp
apply rule
apply auto
done
then have repcNodes_repbNodes:
"repc `(Nodes n ll) = repb `(Nodes n ll)"
by simp
from pret_dag nsll wf_ll
have null_notin_Nodesn: "Null ∉ Nodes n ll"
apply -
apply (rule Null_notin_Nodes)
apply (auto simp add: length_ll_eq)
done
from hno_in_Nodesn have "repc (high no) ∈ repc `(Nodes n ll)"
by blast
with repbNodes_in_Nodes repcNodes_repbNodes
have "repc (high no) ∈ Nodes n ll"
apply simp
apply blast
done
with null_notin_Nodesn have rhn_nNull: "repc (high no) ≠ Null"
by auto
from no_in_pret nonNull lno_nNull pret_dag
have lno_in_pret: "low no ∈ set_of pret"
by (rule subelem_set_of_low)
with wf_ll
have lno_in_ll: "low no ∈ set (ll ! (var (low no)))"
by (simp add: wf_ll_def)
from pret_dag ord_pret no_in_pret lno_nNull hno_nNull
have varlnos_varno: "var (low no) < var no"
apply -
apply (drule var_ordered_children)
apply assumption+
apply auto
done
with varno have varlnos_n: "var (low no) < n" by simp
with lno_in_ll have lno_in_Nodesn: "low no ∈ Nodes n ll"
apply (simp add: Nodes_def)
apply (rule_tac x="var (low no)" in exI)
apply simp
done
from varlnos_n wf_ll nsll lno_in_ll
have "low no ∉ set (ll ! n)"
apply -
apply (rule no_in_one_ll)
apply (auto simp add: length_ll_eq)
done
with repbc_nc have repb_repc_low: "repb (low no) = repc (low no)" by simp
with normalize_prop lno_in_Nodesn varlnos_varno varno
have low_normalize: "var (repc (low no)) ≤ var (low no) ∧
(∃not nort. Dag (repc (low no)) (repb ∝ low) (repb ∝ high) nort ∧
Dag (low no) low high not ∧ reduced nort ∧ ordered nort var ∧
set_of nort ⊆ repb `(Nodes n ll) ∧
(∀no∈set_of nort. repb no = no) ∧
(∃nobdt norbdt. bdt not var = Some nobdt ∧ bdt nort var = Some norbdt ∧
nobdt ∼ norbdt))"
(is "?varrep_low ∧
(∃not nort. ?repbclow_dag nort ∧ ?low_dag not ∧ ?redhigh nort ∧
?ordhigh nort ∧ ?replow_in_Nodes nort ∧ ?low_repno_no nort
∧ ?lowdd_prop not nort)"
is "?varrep_low ∧ ?not_nort_prop_low")
apply simp
apply (erule_tac x="low no" in ballE)
apply (simp del: Dag_Ref)
apply simp
done
then have varrep_low: "?varrep_low" by simp
from low_normalize have not_nort_prop_low: "?not_nort_prop_low"
by (simp del: Dag_Ref)
from lno_in_Nodesn have "repc (low no) ∈ repc `(Nodes n ll)"
by blast
with repbNodes_in_Nodes repcNodes_repbNodes
have "repc (low no) ∈ Nodes n ll"
apply simp
apply blast
done
with null_notin_Nodesn have rln_nNull: "repc (low no) ≠ Null"
by auto
show ?thesis
proof (cases "repc (low no) = repc (high no)")
case True
note red_case=this
with repreduce lno_nNull hno_nNull
have rno_eq_hrno: "repc no = repc (high no)"
by (simp add: null_comp_def)
from varhnos_varno rno_eq_hrno varrep_high have varrep: "?varrep" by simp
from not_nort_prop_high not_nort_prop_low have repcn_prop: "?repcn_prop"
apply -
apply (elim exE)
apply (rename_tac rnot lnot rnort lnort )
apply (rule_tac x="(Node lnot no rnot)" in exI)
apply (rule_tac x=rnort in exI)
apply (elim conjE)
apply (intro conjI)
prefer 7
apply (elim exE)
apply (rename_tac rnot lnot rnort lnort rnobdt lnobdt rnorbdt lnorbdt)
apply (elim conjE)
apply (case_tac "Suc 0 < var no")
apply (rule_tac x="(Bdt_Node lnobdt (var no) rnobdt)" in exI)
apply (rule conjI)
prefer 2
apply (rule_tac x=rnorbdt in exI)
apply (rule conjI)
proof -
fix rnot lnot rnort lnort
assume highnort_dag:
"Dag (repc (high no)) (repb ∝ low) (repb ∝ high) rnort"
assume ord_nort: " ordered rnort var"
assume rnort_in_repNodes: " set_of rnort ⊆ repb ` Nodes n ll"
from rnort_in_repNodes repbNodes_in_Nodes
have nort_in_Nodes: "set_of rnort ⊆ Nodes n ll"
by blast
from varhnos_n varrep_high
have vrhnos_n: "var (repc (high no)) < n" by simp
from rhn_nNull highnort_dag
have "∃lno rno. rnort = Node lno (repc (high no)) rno" by fastforce
with highnort_dag rhn_nNull have "root rnort = repc (high no)" by auto
with ord_nort have "∀x ∈ set_of rnort. var x <= var (repc (high no))"
apply -
apply (rule ballI)
apply (drule ordered_set_of)
apply auto
done
with vrhnos_n have vxsn: "∀x ∈ set_of rnort. var x < n"
by fastforce
from nort_in_Nodes have "∀x ∈ set_of rnort. x ∈ Nodes n ll"
by auto
with wf_ll nsll
have x_in_pret: "∀x ∈ set_of rnort. x ∈ set_of pret"
apply -
apply (rule ballI)
apply (drule wf_ll_Nodes_pret)
apply (auto simp add: length_ll_eq)
done
from vxsn x_in_pret
have vxsn_in_nort: "∀x ∈ set_of rnort. var x <n ∧ x ∈ set_of pret"
by auto
with pret_dag prebdt_pret highnort_dag ord_pret wf_ll nsll
repbc_nc
have "∀x ∈ set_of rnort. (repc ∝ low) x = (repb ∝ low) x ∧
(repc ∝ high) x = (repb ∝ high) x"
apply -
apply (rule nort_null_comp)
apply (auto simp add: length_ll_eq)
done
with rno_eq_hrno
have "Dag (repc no) (repc ∝ low) (repc ∝ high) rnort =
Dag (repc no) (repb ∝ low) (repb ∝ high) rnort"
apply -
apply (rule heaps_eq_Dag_eq)
apply simp
done
with highnort_dag rno_eq_hrno
show "Dag (repc no) (repc ∝ low) (repc ∝ high) rnort" by simp
next
fix rnot lnot rnort lnort
assume lnot_dag: "Dag (low no) low high lnot"
assume rnot_dag: "Dag (high no) low high rnot"
with lnot_dag nonNull
show "Dag no low high (Node lnot no rnot)" by simp
next
fix rnot lnot rnort lnort
assume " reduced rnort"
then show "reduced rnort" by simp
next
fix rnort
assume "ordered rnort var"
then show "ordered rnort var" by simp
next
fix rnort
assume rnort_in_Nodes: " set_of rnort ⊆ repb ` Nodes n ll"
have "Nodes n ll ⊆ Nodes (n + 1) ll"
by (simp add: Nodes_def set_split)
then have "repc ` Nodes n ll ⊆ repc ` Nodes (n + 1) ll"
by blast
with rnort_in_Nodes repbNodes_repcNodes
show " set_of rnort ⊆ repc ` Nodes (n + 1) ll"
by (simp add: Nodes_def)
next
fix rnort rnorbdt
assume " bdt rnort var = Some rnorbdt"
then show " bdt rnort var = Some rnorbdt" by simp
next
fix rnot lnot rnort lnort rnobdt lnobdt rnorbdt lnorbdt
assume rcongeval: "rnobdt ∼ rnorbdt"
assume lnort_dag:
"Dag (repc (low no)) (repb ∝ low) (repb ∝ high) lnort"
assume rnort_dag:
"Dag (repc (high no)) (repb ∝ low) (repb ∝ high) rnort"
assume lnorbdt_def: " bdt lnort var = Some lnorbdt"
assume rnorbdt_def: " bdt rnort var = Some rnorbdt"
assume lcongeval:"lnobdt ∼ lnorbdt"
from red_case lnort_dag rnort_dag
have lnort_rnort: "lnort = rnort"
by (simp add: Dag_unique del: Dag_Ref)
with lnorbdt_def lcongeval rnorbdt_def
have lnobdt_rnorbdt: "lnobdt ∼ rnorbdt" by simp
with rcongeval have "lnobdt ∼ rnobdt"
apply -
apply (rule cong_eval_trans)
apply (auto simp add: cong_eval_sym)
done
then have " Bdt_Node lnobdt (var no) rnobdt ∼ rnobdt"
apply -
apply (simp add: cong_eval_sym [rule_format])
apply (rule cong_eval_child_high)
apply assumption
done
with rcongeval show "Bdt_Node lnobdt (var no) rnobdt ∼ rnorbdt"
apply -
apply (rotate_tac 1)
apply (rule cong_eval_trans)
apply auto
done
next
fix lnot rnot lnobdt rnobdt
assume lnot_dag: "Dag (low no) low high lnot"
assume rnot_dag: " Dag (high no) low high rnot"
assume lnobdt_def: " bdt lnot var = Some lnobdt"
assume rnobdt_def: " bdt rnot var = Some rnobdt"
assume onesvarno: " Suc 0 < var no"
with rnobdt_def lnot_dag rnot_dag lnobdt_def
show "bdt (Node lnot no rnot) var =
Some (Bdt_Node lnobdt (var no) rnobdt)"
by simp
next
fix rnot lnot rnort lnort rnobdt lnobdt rnorbdt lnorbdt
assume lnobdt_def: " bdt lnot var = Some lnobdt"
assume rnobdt_def: " bdt rnot var = Some rnobdt"
assume rnorbdt_def: " bdt rnort var = Some rnorbdt"
assume cong_rno_rnor: " rnobdt ∼ rnorbdt"
assume lnot_dag: "Dag (low no) low high lnot"
assume rnot_dag: "Dag (high no) low high rnot"
assume "¬ Suc 0 < var no"
then have varnoseq1: "var no = 0 ∨ var no = 1" by auto
show "∃nobdt. bdt (Node lnot no rnot) var = Some nobdt ∧
(∃norbdt. bdt rnort var = Some norbdt ∧ nobdt ∼ norbdt)"
proof (cases "var no = 0")
case True
note vnoNull=this
with pret_dag ord_pret no_in_pret lno_nNull hno_nNull
show ?thesis
apply -
apply (drule var_ordered_children)
apply auto
done
next
assume "var no ≠ 0"
with varnoseq1 have vnoOne: "var no = 1" by simp
from pret_dag ord_pret no_in_pret lno_nNull hno_nNull
vnoOne
have vlvrNull: "var (low no) = 0 ∧ var (high no) = 0"
apply -
apply (drule var_ordered_children)
apply auto
done
then have vlNull: "var (low no) = 0" by simp
from vlvrNull have vrNull: "var (high no) = 0" by simp
from lnobdt_def lnot_dag vlNull lno_nNull
have lnobdt_Zero: "lnobdt = Zero"
apply -
apply (drule bdt_Some_var0_Zero)
apply auto
done
from rnobdt_def rnot_dag vrNull hno_nNull
have rnobdt_Zero: "rnobdt = Zero"
apply -
apply (drule bdt_Some_var0_Zero)
apply auto
done
from lnobdt_Zero lnobdt_def have "bdt lnot var = Some Zero" by simp
with lnot_dag vlNull
have lnot_Node: "lnot = (Node Tip (low no) Tip)"
by auto
from rnobdt_Zero rnobdt_def rnot_dag vrNull
have rnot_Node: "rnot = (Node Tip (high no) Tip)"
by auto
from pret_dag no_in_pret obtain not where
not_ex: "Dag no low high not"
apply -
apply (drule dag_setof_exD)
apply auto
done
with pret_dag no_in_pret have not_ex_in_pret: "not <= pret"
apply -
apply (rule set_of_subdag)
apply auto
done
from not_ex lnot_dag rnot_dag nonNull
have not_def: "not = (Node lnot no rnot)"
by (simp add: Dag_unique del: Dag_Ref)
with not_ex_in_pret prebdt_pret
have nobdt_ex: "∃nobdt. bdt (Node lnot no rnot) var = Some nobdt"
apply -
apply (rule subbdt_ex)
apply auto
done
then obtain nobdt where
nobdt_def: "bdt (Node lnot no rnot) var = Some nobdt" by auto
from not_def have "root not = no" by simp
with nobdt_def vnoOne not_def have "not = (Node Tip no Tip)"
apply -
apply (drule bdt_Some_var1_One)
apply auto
done
with not_def have "rnot = Tip" by simp
with rnot_Node show ?thesis by simp
qed
next
fix rnot lnot rnort lnort
assume rnort_in_repb_Nodesn: "set_of rnort ⊆ repb ` Nodes n ll"
assume rnort_repb_no: "∀no∈set_of rnort. repb no = no"
from repbNodes_in_Nodes rnort_in_repb_Nodesn
have rnort_in_Nodesn: "set_of rnort ⊆ Nodes n ll"
by blast
show "∀no∈set_of rnort. repc no = no"
proof
fix pt
assume pt_in_rnort: " pt ∈ set_of rnort"
with rnort_in_Nodesn have "pt ∈ Nodes n ll"
by blast
with Nodesn_notin_lln have "pt ∉ set (ll ! n)"
by auto
with repbc_nc have "repb pt = repc pt"
by auto
with rnort_repb_no pt_in_rnort show "repc pt = pt"
by auto
qed
qed
with varrep show ?thesis by simp
next
assume share_case_cond: "repc (low no) ≠ repc (high no)"
with lno_nNull hno_nNull
have share_case_cond_propto: "(repc ∝ low) no ≠ (repc ∝ high) no"
by (simp add: null_comp_def)
with repshare obtain
rno_in_llbn: "repc no ∈ set (ll ! n)" and
rrno_eq_rno: "repc (repc no) = repc no" and
twonodes_in_llbn_prop: "(∀no1∈set (ll ! n).
((repc ∝ high) no1 = (repc ∝ high) no ∧
(repc ∝ low) no1 = (repc ∝ low) no) = (repc no = repc no1))"
by auto
from wf_ll rno_in_llbn nsll
have varrepno_n: "var (repc no) = n"
by (simp add: wf_ll_def length_ll_eq)
with varno have varrep: "?varrep"
by simp
from not_nort_prop_high not_nort_prop_low have repcn_prop: "?repcn_prop"
apply-
apply (elim exE)
apply (rename_tac rnot lnot rnort lnort)
apply (rule_tac x="Node lnot no rnot" in exI)
apply (rule_tac x="Node lnort (repc no) rnort" in exI)
apply (elim conjE)
apply (intro conjI)
prefer 7
apply (elim exE)
apply (rename_tac rnot lnot rnort lnort rnobdt lnobdt rnorbdt lnorbdt)
apply (elim conjE)
apply (case_tac "Suc 0 < var no")
apply (rule_tac x="(Bdt_Node lnobdt (var no) rnobdt)" in exI)
apply (rule conjI)
prefer 2
apply (rule_tac x="(Bdt_Node lnorbdt (var (repc no)) rnorbdt)" in exI)
apply (rule conjI)
proof -
fix rnot lnot rnort lnort
assume rnort_dag:
"Dag (repc (high no)) (repb ∝ low) (repb ∝ high) rnort"
assume lnort_dag:
"Dag (repc (low no)) (repb ∝ low) (repb ∝ high) lnort"
assume rnort_in_repNodes: "set_of rnort ⊆ repb ` Nodes n ll"
assume lnort_in_repNodes: "set_of lnort ⊆ repb ` Nodes n ll"
from rnort_in_repNodes repbNodes_in_Nodes
have rnort_in_Nodes: "set_of rnort ⊆ Nodes n ll"
by simp
from lnort_in_repNodes repbNodes_in_Nodes
have lnort_in_Nodes: "set_of lnort ⊆ Nodes n ll"
by simp
from rnort_in_Nodes
have rnortx_in_Nodes: "∀ x ∈ set_of rnort. x ∈ Nodes n ll"
by blast
with wf_ll nsll
have "∀ x ∈ set_of rnort. x ∈ set_of pret ∧ var x < n"
apply -
apply (rule ballI)
apply (rule wf_ll_Nodes_pret)
apply (auto simp add: length_ll_eq)
done
with pret_dag prebdt_pret rnort_dag ord_pret wf_ll nsll
repbc_nc
have "∀x ∈ set_of rnort. (repc ∝ low) x = (repb ∝ low) x ∧
(repc ∝ high) x = (repb ∝ high) x"
apply -
apply (rule nort_null_comp)
apply (auto simp add: length_ll_eq)
done
then have "Dag (repc (high no)) (repc ∝ low) (repc ∝ high) rnort =
Dag (repc (high no)) (repb ∝ low) (repb ∝ high) rnort"
apply -
apply (rule heaps_eq_Dag_eq)
apply assumption
done
with rnort_dag
have rnort_dag_repc:
"Dag (repc (high no)) (repc ∝ low) (repc ∝ high) rnort"
by simp
from lnort_in_Nodes
have lnortx_in_Nodes: "∀x ∈ set_of lnort. x ∈ Nodes n ll"
by blast
with wf_ll nsll
have "∀ x ∈ set_of lnort. x ∈ set_of pret ∧ var x < n"
apply -
apply (rule ballI)
apply (rule wf_ll_Nodes_pret)
apply (auto simp add: length_ll_eq)
done
with pret_dag prebdt_pret lnort_dag ord_pret wf_ll nsll
repbc_nc
have "∀ x ∈ set_of lnort. (repc ∝ low) x = (repb ∝ low) x ∧
(repc ∝ high) x = (repb ∝ high) x"
apply -
apply (rule nort_null_comp)
apply (auto simp add: length_ll_eq)
done
then have
"Dag (repc (low no)) (repc ∝ low) (repc ∝ high) lnort =
Dag (repc (low no)) (repb ∝ low) (repb ∝ high) lnort"
apply -
apply (rule heaps_eq_Dag_eq)
apply assumption
done
with lnort_dag
have lnort_dag_repc:
"Dag (repc (low no)) (repc ∝ low) (repc ∝ high) lnort"
by simp
from lno_nNull hno_nNull
have propto_comp: "(repc ∝ low) no = repc (low no) ∧
(repc ∝ high) no = repc (high no)"
by (simp add: null_comp_def)
from rno_in_llbn twonodes_in_llbn_prop rrno_eq_rno
have "(repc ∝ high) (repc no) = (repc ∝ high) no ∧
(repc ∝ low) (repc no) = (repc ∝ low) no"
by simp
with propto_comp lnort_dag_repc rnort_dag_repc lno_nNull hno_nNull
rnonN
show "Dag(repc no)(repc ∝ low)(repc ∝ high)(Node lnort (repc no) rnort)"
by auto
next
fix rnot lnot rnort lnort
assume rnot_dag: "Dag (high no) low high rnot"
assume lnot_dag: "Dag (low no) low high lnot"
with rnot_dag nonNull
show "Dag no low high (Node lnot no rnot)"
by simp
next
fix rnort lnort
assume rnort_dag:
"Dag (repc (high no)) (repb ∝ low) (repb ∝ high) rnort"
assume lnort_dag:
"Dag (repc (low no)) (repb ∝ low) (repb ∝ high) lnort"
assume red_rnort: "reduced rnort"
assume red_lnort: " reduced lnort"
from rhn_nNull rnort_dag obtain lrnort rrnort where
rnort_Node: "rnort = (Node lrnort (repc (high no)) rrnort)"
by auto
from rln_nNull lnort_dag obtain llnort rlnort where
lnort_Node: "lnort = (Node llnort (repc (low no)) rlnort)"
by auto
from twonodes_in_llbn_prop rrno_eq_rno rno_in_llbn hno_nNull lno_nNull
have "((repc ∝ high) (repc no)) = repc (high no) ∧
((repc ∝ low) (repc no)) = repc (low no)"
apply -
apply (erule_tac x="repc no" in ballE)
apply (auto simp add: null_comp_def)
done
with share_case_cond
have "((repc ∝ high) (repc no)) ≠ ((repc ∝ low) (repc no))"
by auto
with red_lnort red_rnort rnort_Node lnort_Node share_case_cond
show "reduced (Node lnort (repc no) rnort)"
apply -
apply (rule_tac lp="repc (low no)" and rp="repc (high no)" and
llt=llnort and rlt = rlnort and lrt=lrnort and rrt=rrnort
in reduced_children_parent)
apply auto
done
next
fix lnort rnort
assume lnort_dag:
"Dag (repc (low no)) (repb ∝ low) (repb ∝ high) lnort"
assume ord_lnort: "ordered lnort var"
assume rnort_dag:
"Dag (repc (high no)) (repb ∝ low) (repb ∝ high) rnort"
assume ord_rnort: " ordered rnort var"
assume lnort_in_repNodes: "set_of lnort ⊆ repb `Nodes n ll"
assume rnort_in_repNodes: "set_of rnort ⊆ repb `Nodes n ll"
from lnort_in_repNodes repbNodes_in_Nodes
have lnort_in_Nodes: "set_of lnort ⊆ Nodes n ll"
by simp
from rnort_in_repNodes repbNodes_in_Nodes
have rnort_in_Nodes: "set_of rnort ⊆ Nodes n ll"
by simp
from rhn_nNull rnort_dag obtain lrnort rrnort where
rnort_Node: "rnort = (Node lrnort (repc (high no)) rrnort)"
by auto
from rln_nNull lnort_dag obtain llnort rlnort where
lnort_Node: "lnort = (Node llnort (repc (low no)) rlnort)"
by auto
from lnort_dag rln_nNull lnort_in_Nodes
have "repc (low no) ∈ set_of lnort"
by auto
with lnort_in_Nodes
have "repc (low no) ∈ Nodes n ll"
by blast
with wf_ll nsll
have vrlno_sn: "var (repc (low no)) < n"
apply -
apply (drule wf_ll_Nodes_pret)
apply (auto simp add: length_ll_eq)
done
from rnort_dag rhn_nNull rnort_in_Nodes
have "repc (high no) ∈ set_of rnort"
by auto
with rnort_in_Nodes
have "repc (high no) ∈ Nodes n ll"
by blast
with wf_ll nsll have vrhno_sn: "var (repc (high no)) < n"
apply -
apply (drule wf_ll_Nodes_pret)
apply (auto simp add: length_ll_eq)
done
with varrepno_n vrlno_sn lnort_dag ord_lnort rnort_dag rnort_Node
lnort_Node ord_rnort
show "ordered (Node lnort (repc no) rnort) var"
by auto
next
fix lnort rnort
assume lnort_in_Nodes: "set_of lnort ⊆ repb `Nodes n ll"
assume rnort_in_Nodes: "set_of rnort ⊆ repb `Nodes n ll"
from lnort_in_Nodes repbNodes_repcNodes
have lnort_in_repcNodes: "set_of lnort ⊆ repc `Nodes n ll"
by simp
from rnort_in_Nodes repbNodes_repcNodes
have rnort_in_repcNodes: "set_of rnort ⊆ repc `Nodes n ll"
by simp
have nNodessubset: "Nodes n ll ⊆ Nodes (n+1) ll"
by (simp add: Nodes_subset)
then have repc_Nodes_subset:
"repc `Nodes n ll ⊆ repc `Nodes (n+1) ll"
by blast
from no_in_Nodes have "repc no ∈ repc `Nodes (n+1) ll"
by blast
with repc_Nodes_subset lnort_in_repcNodes rnort_in_repcNodes
show "set_of (Node lnort (repc no) rnort) ⊆
repc `Nodes (n + 1) ll"
apply simp
apply blast
done
next
fix rnot lnot rnort lnort rnobdt lnobdt rnorbdt lnorbdt
assume lnobdt_def: " bdt lnot var = Some lnobdt"
assume rnobdt_def: " bdt rnot var = Some rnobdt"
assume rnorbdt_def: " bdt rnort var = Some rnorbdt"
assume cong_rno_rnor: " rnobdt ∼ rnorbdt"
assume lnot_dag: "Dag (low no) low high lnot"
assume rnot_dag: "Dag (high no) low high rnot"
assume "¬ Suc 0 < var no"
then have varnoseq1: "var no = 0 ∨ var no = 1" by auto
show "∃nobdt. bdt (Node lnot no rnot) var = Some nobdt ∧
(∃norbdt. bdt (Node lnort (repc no) rnort) var = Some norbdt ∧
nobdt ∼ norbdt)"
proof (cases "var no = 0")
case True
note vnoNull=this
with pret_dag ord_pret no_in_pret lno_nNull hno_nNull
show ?thesis
apply -
apply (drule var_ordered_children)
apply auto
done
next
assume "var no ≠ 0"
with varnoseq1 have vnoOne: "var no = 1" by simp
from pret_dag ord_pret no_in_pret lno_nNull hno_nNull
vnoOne
have vlvrNull: "var (low no) = 0 ∧ var (high no) = 0"
apply -
apply (drule var_ordered_children)
apply auto
done
then have vlNull: "var (low no) = 0" by simp
from vlvrNull have vrNull: "var (high no) = 0" by simp
from lnobdt_def lnot_dag vlNull lno_nNull
have lnobdt_Zero: "lnobdt = Zero"
apply -
apply (drule bdt_Some_var0_Zero)
apply auto
done
from rnobdt_def rnot_dag vrNull hno_nNull
have rnobdt_Zero: "rnobdt = Zero"
apply -
apply (drule bdt_Some_var0_Zero)
apply auto
done
from lnobdt_Zero lnobdt_def
have "bdt lnot var = Some Zero" by simp
with lnot_dag vlNull
have lnot_Node: "lnot = (Node Tip (low no) Tip)"
by auto
from rnobdt_Zero rnobdt_def rnot_dag vrNull
have rnot_Node: "rnot = (Node Tip (high no) Tip)"
by auto
from pret_dag no_in_pret obtain not
where not_ex: "Dag no low high not"
apply -
apply (drule dag_setof_exD)
apply auto
done
with pret_dag no_in_pret have not_ex_in_pret: "not <= pret"
apply -
apply (rule set_of_subdag)
apply auto
done
from not_ex lnot_dag rnot_dag nonNull
have not_def: "not = (Node lnot no rnot)"
by (simp add: Dag_unique del: Dag_Ref)
with not_ex_in_pret prebdt_pret
have nobdt_ex: "∃ nobdt. bdt (Node lnot no rnot) var = Some nobdt"
apply -
apply (rule subbdt_ex)
apply auto
done
then obtain nobdt where
nobdt_def: "bdt (Node lnot no rnot) var = Some nobdt" by auto
from not_def have "root not = no" by simp
with nobdt_def vnoOne not_def
have "not = (Node Tip no Tip)"
apply -
apply (drule bdt_Some_var1_One)
apply auto
done
with not_def have "rnot = Tip" by simp
with rnot_Node show ?thesis by simp
qed
next
fix lnot rnot lnobdt rnobdt
assume lnot_dag: "Dag (low no) low high lnot"
assume rnot_dag: " Dag (high no) low high rnot"
assume lnobdt_def: " bdt lnot var = Some lnobdt"
assume rnobdt_def: " bdt rnot var = Some rnobdt"
assume onesvarno: " Suc 0 < var no"
with rnobdt_def lnot_dag rnot_dag lnobdt_def
show "bdt (Node lnot no rnot) var =
Some (Bdt_Node lnobdt (var no) rnobdt)" by simp
next
fix rnot lnot rnort lnort rnobdt lnobdt rnorbdt lnorbdt
assume rnort_dag:
"Dag (repc (high no)) (repb ∝ low) (repb ∝ high) rnort"
assume lnort_dag:
"Dag (repc (low no)) (repb ∝ low) (repb ∝ high) lnort"
assume rnorbdt_def: " bdt rnort var = Some rnorbdt"
assume lnorbdt_def: "bdt lnort var = Some lnorbdt"
assume varno_bOne: "Suc 0 < var no"
with varno have "Suc 0 < n" by simp
with varrepno_n have "Suc 0 < var (repc no)" by simp
with rnorbdt_def lnorbdt_def
show "bdt (Node lnort (repc no) rnort) var =
Some (Bdt_Node lnorbdt (var (repc no)) rnorbdt)"
by simp
next
fix rnobdt lnobdt rnorbdt lnorbdt
assume lcong_eval: "lnobdt ∼ lnorbdt"
assume rcong_eval: " rnobdt ∼ rnorbdt"
from varno varrepno_n have "var (repc no) = var no" by simp
with lcong_eval rcong_eval
show "Bdt_Node lnobdt (var no) rnobdt ∼
Bdt_Node lnorbdt (var (repc no)) rnorbdt"
apply (unfold cong_eval_def)
apply (rule ext)
by simp
next
fix rnot lnot rnort lnort
assume lnort_repb: "∀no∈set_of lnort. repb no = no"
assume rnort_repb: "∀no∈set_of rnort. repb no = no"
assume rnort_in_repb_Nodesn: "set_of rnort ⊆ repb ` Nodes n ll"
assume lnort_in_repb_Nodesn: "set_of lnort ⊆ repb ` Nodes n ll"
from repbNodes_in_Nodes rnort_in_repb_Nodesn
have rnort_in_Nodesn: "set_of rnort ⊆ Nodes n ll"
by blast
from repbNodes_in_Nodes lnort_in_repb_Nodesn
have lnort_in_Nodesn: "set_of lnort ⊆ Nodes n ll"
by blast
have rnort_repc: "∀no∈set_of rnort. repc no = no"
proof
fix pt
assume pt_in_rnort: " pt ∈ set_of rnort"
with rnort_in_Nodesn have "pt ∈ Nodes n ll"
by blast
with Nodesn_notin_lln have "pt ∉ set (ll ! n)"
by auto
with repbc_nc have "repb pt = repc pt"
by auto
with rnort_repb pt_in_rnort show "repc pt = pt"
by auto
qed
have lnort_repc: "∀no∈set_of lnort. repc no = no"
proof
fix pt
assume pt_in_lnort: " pt ∈ set_of lnort"
with lnort_in_Nodesn have "pt ∈ Nodes n ll"
by blast
with Nodesn_notin_lln have "pt ∉ set (ll ! n)"
by auto
with repbc_nc have "repb pt = repc pt"
by auto
with lnort_repb pt_in_lnort show "repc pt = pt"
by auto
qed
show "∀no∈set_of (Node lnort (repc no) rnort). repc no = no"
proof
fix pt
assume pt_in_rept: "pt ∈ set_of (Node lnort (repc no) rnort)"
show "repc pt = pt"
proof (cases "pt ∈ set_of lnort")
case True
with lnort_repc show ?thesis
by auto
next
assume pt_notin_lnort: "pt ∉ set_of lnort"
show ?thesis
proof (cases "pt ∈ set_of rnort")
case True
with rnort_repc show ?thesis
by auto
next
assume pt_notin_rnort: "pt ∉ set_of rnort"
with pt_notin_lnort pt_in_rept have "pt = repc no"
by simp
with rrno_eq_rno show "repc pt = pt"
by simp
qed
qed
qed
qed
with varrep rrno_eq_rno show ?thesis by simp
qed
qed
with rnonN show ?thesis by simp
qed
qed
note while_while_prop=this
from wf_ll nsll
have "∀no ∈ Nodes n ll. no ∉ set (ll ! n)"
apply (simp add: Nodes_def length_ll_eq)
apply clarify
apply (drule no_in_one_ll)
apply auto
done
with repbc_nc have "∀no ∈ Nodes n ll. repb no = repc no"
apply -
apply (rule ballI)
apply (erule_tac x=no in allE)
apply simp
done
then have repbNodes_repcNodes:
"repb `(Nodes n ll) = repc `(Nodes n ll)"
apply -
apply rule
apply blast
apply rule
apply (erule imageE)
apply (erule_tac x=xa in ballE)
prefer 2
apply simp
apply rule
apply auto
done
then have repcNodes_repbNodes:
"repc `(Nodes n ll) = repb `(Nodes n ll)"
by simp
have repbc_dags_eq:
"Dags (repc ` Nodes n ll) (repc ∝ low) (repc ∝ high) =
Dags (repb ` Nodes n ll) (repb ∝ low) (repb ∝ high)"
apply -
apply rule
apply rule
apply (erule Dags.cases)
apply (rule DagsI)
prefer 4
apply rule
apply (erule Dags.cases)
apply (rule DagsI)
proof -
fix x p t
assume t_in_repcNodes: "set_of t ⊆ repc ` Nodes n ll"
assume x_t: "x=t"
with t_in_repcNodes repcNodes_repbNodes
show "set_of x ⊆ repb ` Nodes n ll"
by simp
next
fix x p t
assume t_in_repcNodes: "set_of t ⊆ repc ` Nodes n ll"
assume t_dag: "Dag p (repc ∝ low) (repc ∝ high) t"
assume t_nTip: " t ≠ Tip"
assume x_t: "x=t"
from t_nTip t_dag have "p ≠ Null"
apply -
apply (case_tac "p=Null")
apply auto
done
with t_nTip t_dag obtain lt rt where t_Node: "t=Node lt p rt"
by auto
from t_in_repcNodes t_dag t_nTip t_Node obtain q where
rq_p: "repc q = p" and q_in_Nodes: "q ∈ Nodes n ll"
apply simp
apply (elim conjE)
apply (erule imageE)
apply auto
done
from q_in_Nodes have "repb q = repc q"
by (rule Nodes_n_rep_nc [rule_format])
with rq_p have repbq_p: "repb q = p" by simp
from q_in_Nodes
have "Dag (repb q) (repb ∝ low) (repb ∝ high) t =
Dag (repc q) (repc ∝ low) (repc ∝ high) t"
by (rule Nodes_repbc_Dags_eq [rule_format])
with t_dag rq_p have "Dag (repb q) (repb ∝ low) (repb ∝ high) t" by simp
with repbq_p x_t show "Dag p (repb ∝ low) (repb ∝ high) x"
by simp
next
fix x p t
assume t_in_repcNodes: "set_of t ⊆ repb ` Nodes n ll"
assume x_t: "x=t"
with t_in_repcNodes repbNodes_repcNodes
show "set_of x ⊆ repc ` Nodes n ll"
by simp
next
fix x p t
assume t_in_repcNodes: "set_of t ⊆ repb ` Nodes n ll"
assume t_dag: "Dag p (repb ∝ low) (repb ∝ high) t"
assume t_nTip: " t ≠ Tip"
assume x_t: "x=t"
from t_nTip t_dag have "p ≠ Null"
apply -
apply (case_tac "p=Null")
apply auto
done
with t_nTip t_dag obtain lt rt where t_Node: "t=Node lt p rt"
by auto
from t_in_repcNodes t_dag t_nTip t_Node obtain q where
rq_p: "repb q = p" and q_in_Nodes: "q ∈ Nodes n ll"
apply simp
apply (elim conjE)
apply (erule imageE)
apply auto
done
from q_in_Nodes have "repb q = repc q"
by (rule Nodes_n_rep_nc [rule_format])
with rq_p have repbq_p: "repc q = p" by simp
from q_in_Nodes
have "Dag (repb q) (repb ∝ low) (repb ∝ high) t =
Dag (repc q) (repc ∝ low) (repc ∝ high) t"
by (rule Nodes_repbc_Dags_eq [rule_format])
with t_dag rq_p have "Dag (repc q) (repc ∝ low) (repc ∝ high) t" by simp
with repbq_p x_t show "Dag p (repc ∝ low) (repc ∝ high) x"
by simp
next
fix x p and t :: "dag"
assume x_t: "x = t"
assume t_nTip: " t ≠ Tip"
with x_t show "x≠ Tip" by simp
next
fix x p and t :: "dag"
assume x_t: "x = t"
assume t_nTip: " t ≠ Tip"
with x_t show "x≠ Tip" by simp
qed
from pret_dag wf_ll nsll
have null_notin_Nodes_Suc_n: "Null ∉ Nodes (Suc n) ll"
by - (rule Null_notin_Nodes,auto simp add: length_ll_eq)
{ fix t1 t2
assume t1_in_DagsNodesn:
"t1 ∈ Dags (repc ` Nodes n ll) (repc ∝ low) (repc ∝ high)"
assume t2_notin_DagsNodesn:
"t2 ∉ Dags (repc ` Nodes n ll) (repc ∝ low) (repc ∝ high)"
assume t2_in_DagsNodesSucn:
"t2 ∈ Dags (repc ` Nodes (Suc n) ll) (repc ∝ low) (repc ∝ high)"
assume isomorphic_dags_eq_asm:
"∀t1 t2. t1 ∈ Dags (repb ` Nodes n ll) (repb ∝ low) (repb ∝ high)
∧ t2 ∈ Dags (repb ` Nodes n ll) (repb ∝ low) (repb ∝ high)
⟶ isomorphic_dags_eq t1 t2 var"
assume repbc_Dags:
"Dags (repc ` Nodes n ll) (repc ∝ low) (repc ∝ high) =
Dags (repb ` Nodes n ll) (repb ∝ low) (repb ∝ high)"
from t1_in_DagsNodesn repbc_Dags
have t1_repb_subnode:
"t1 ∈ Dags (repb ` Nodes n ll) (repb ∝ low) (repb ∝ high)"
by simp
from t2_in_DagsNodesSucn
have t2_in_DagsNodesSucn:
"t2 ∈ Dags (repc ` Nodes (Suc n) ll) (repc ∝ low) (repc ∝ high)"
by simp
from repbNodes_in_Nodes repbNodes_repcNodes
have repcNodesn_in_Nodesn: "repc `Nodes n ll ⊆ Nodes n ll"
by simp
from t1_in_DagsNodesn obtain q where
Dag_q_Nodes_n:
"Dag (repc q) (repc ∝ low) (repc ∝ high) t1 ∧ q ∈ Nodes n ll"
proof (elim Dags.cases)
fix p t
assume t1_t: "t1 = t"
assume t_in_repcNodesn: "set_of t ⊆ repc ` Nodes n ll"
assume t_dag: "Dag p (repc ∝ low) (repc ∝ high) t"
assume t_nTip: " t ≠ Tip"
assume obtain_prop: "⋀q. Dag (repc q) (repc ∝ low) (repc ∝ high) t1 ∧
q ∈ Nodes n ll ⟹ ?thesis"
from t_nTip t_dag have "p ≠ Null"
apply -
apply (case_tac "p=Null")
apply auto
done
with t_nTip t_dag obtain lt rt where t_Node: "t=Node lt p rt"
by auto
from t_in_repcNodesn t_dag t_nTip t_Node obtain k where
rk_p: "repc k = p" and k_in_Nodes: "k ∈ Nodes n ll"
apply simp
apply (elim conjE)
apply (erule imageE)
apply auto
done
with t1_t t_dag obtain_prop rk_p k_in_Nodes show ?thesis
by auto
qed
with wf_ll nsll have varq_sn: "(var q < n)"
apply (simp add: Nodes_def)
apply (elim conjE)
apply (erule exE)
apply (simp add: wf_ll_def length_ll_eq)
apply (elim conjE)
apply (thin_tac " ∀q. q ∈ set_of pret ⟶ q ∈ set (ll ! var q)")
apply (erule_tac x=x in allE)
apply auto
done
from Dag_q_Nodes_n have q_in_Nodesn: "q ∈ Nodes n ll"
by simp
then have "∃ k<n. q ∈ set (ll ! k)"
by (simp add: Nodes_def)
with wf_ll nsll have "q ∉ set (ll ! n)"
apply -
apply (erule exE)
apply (rule_tac i=k and j=n in no_in_one_ll)
apply (auto simp add: length_ll_eq)
done
with repbc_nc have repbc_q: "repc q = repb q"
apply -
apply (erule_tac x=q in allE)
apply auto
done
from normalize_prop q_in_Nodesn have "var (repb q) <= var q"
apply -
apply (erule_tac x=q in ballE)
apply auto
done
with repbc_q have var_repc_q: "var (repc q) <= var q"
by simp
with varq_sn have var_repc_q_n: "var (repc q) < n"
by simp
from Nodes_subset Dag_q_Nodes_n while_while_prop
have ord_t1_var_rep: "ordered t1 var ∧ var (repc q) <= var q"
apply (elim conjE)
apply (erule_tac x=q in ballE)
apply auto
done
then have ord_t1: "ordered t1 var" by simp
from ord_t1_var_rep have varrep_q: "var (repc q) <= var q" by simp
from t2_in_DagsNodesSucn have ord_t2: "ordered t2 var"
proof (elim Dags.cases)
fix p t
assume t_in_repcNodes: "set_of t ⊆ repc ` Nodes (Suc n) ll"
assume t_nTip: " t ≠ Tip"
assume t2t: "t2 = t"
assume t_dag: "Dag p (repc ∝ low) (repc ∝ high) t"
from t_in_repcNodes have x_in_repcNodesSucn:
"∀x. x ∈ set_of t ⟶ x ∈ repc ` Nodes (Suc n) ll"
apply -
apply auto
done
from t_nTip t_dag have "p ≠ Null"
apply -
apply (case_tac "p=Null")
apply auto
done
with t_nTip t_dag obtain lt rt where t_Node: "t=Node lt p rt"
by auto
then have "p ∈ set_of t"
by auto
with x_in_repcNodesSucn have "p ∈ repc ` Nodes (Suc n) ll"
by simp
then obtain a where repca_p: "p=repc a" and
a_in_NodesSucn: "a ∈ Nodes (Suc n) ll"
by auto
with repca_p while_while_prop t_dag t2t show ?thesis
apply -
apply (erule_tac x=a in ballE)
apply (elim conjE exE)
apply (subgoal_tac "nort = t")
prefer 2
apply (simp add: Dag_unique)
apply auto
done
qed
from while_while_prop have while_prop_part:
"∀no ∈ Nodes (Suc n) ll.
var (repc no) <= var no"
by auto
from while_while_prop have rep_rep_nort:
"∀no∈Nodes (n + 1) ll. (∃nort. Dag (repc no) (repc ∝ low) (repc ∝ high) nort ∧
(∀no∈set_of nort. repc no = no))"
by auto
from repcNodes_in_Nodes null_notin_Nodes_Suc_n
have "∀no ∈ Nodes (n+1) ll. repc no ≠ Null"
by auto
with rep_rep_nort have "∀ no ∈ Nodes (n+1) ll. repc (repc no) = (repc no)"
apply -
apply (rule ballI)
apply (erule_tac x=no in ballE)
prefer 2
apply simp
apply (erule_tac x=no in ballE)
apply (erule exE)
apply (subgoal_tac "repc no ∈ set_of nort")
apply (elim conjE)
apply (erule_tac x="repc no" in ballE)
apply simp
apply simp
apply (simp)
apply (elim conjE)
apply (thin_tac "∀no∈set_of nort. repc no = no")
apply auto
done
with t2_in_DagsNodesSucn t2_notin_DagsNodesn ord_t2 while_prop_part
wf_ll nsll repcNodes_in_Nodes obtain a where
t2_repc_dag: "Dag (repc a) (repc ∝ low) (repc ∝ high) t2" and
a_in_lln: "a ∈ set (ll ! n)"
apply -
apply (drule restrict_root_Node)
apply (auto simp add: length_ll_eq)
done
with wf_ll nsll have a_in_pret: "a ∈ set_of pret"
by (simp add: wf_ll_def length_ll_eq)
from wf_ll nsll a_in_lln have vara_n: "var a = n"
by (simp add: wf_ll_def length_ll_eq)
from a_in_lln rep_prop obtain
repp_nNull: " repc a ≠ Null" and
repp_reduce: "(repc ∝ low) a = (repc ∝ high) a ∧ low a ≠ Null
⟶ repc a = (repc ∝ high) a" and
repp_share: "((repc ∝ low) a = (repc ∝ high) a ⟶ low a = Null)
⟶ repc a ∈ set (ll ! n) ∧
repc (repc a) = repc a ∧
(∀no1∈set (ll ! n). ((repc ∝ high) no1 = (repc ∝ high) a ∧
(repc ∝ low) no1 = (repc ∝ low) a) = (repc a = repc no1))"
using [[simp_depth_limit=4]]
by auto
from t2_repc_dag a_in_lln repp_nNull obtain lt2 rt2 where
t2_Node: "t2 = (Node lt2 (repc a) rt2)"
by auto
have "isomorphic_dags_eq t1 t2 var"
proof (cases "(repc ∝ low) a = (repc ∝ high) a ∧ low a ≠ Null")
case True
note red=this
then have red_case: "(repc ∝ low) a = (repc ∝ high) a"
by simp
from red have low_nNull: "low a ≠ Null"
by simp
with pret_dag prebdt_pret a_in_pret have highp_nNull: "high a ≠ Null"
apply -
apply (drule balanced_bdt)
apply auto
done
from pret_dag ord_pret a_in_pret low_nNull highp_nNull
have var_children_smaller: "var (low a) < var a ∧ var (high a) < var a"
apply -
apply (rule var_ordered_children)
apply auto
done
from pret_dag a_in_pret have a_nNull: "a ≠ Null"
apply -
apply (rule set_of_nn [rule_format])
apply auto
done
with a_in_pret highp_nNull pret_dag have "high a ∈ set_of pret"
apply -
apply (drule subelem_set_of_high)
apply auto
done
with wf_ll have "high a ∈ set (ll ! (var (high a)))"
by (simp add: wf_ll_def)
with a_in_lln t2_repc_dag var_children_smaller vara_n
have "∃ k<n. (high a) ∈ set (ll ! k)"
by auto
then have higha_in_Nodesn: "(high a) ∈ Nodes n ll"
by (simp add: Nodes_def)
then have rhigha_in_rNodesn: "repc (high a) ∈ repc ` Nodes n ll"
by simp
from higha_in_Nodesn normalize_prop obtain rt where
rt_dag: "Dag (repb (high a)) (repb ∝ low) (repb ∝ high) rt" and
rt_in_repbNort: "set_of rt ⊆ repb `Nodes n ll"
apply -
apply (erule_tac x="high a" in ballE)
apply auto
done
from rt_in_repbNort repbNodes_repcNodes
have rt_in_repcNodesn: "set_of rt ⊆ repc `Nodes n ll"
by blast
from rt_dag higha_in_Nodesn
have repcrt_dag: "Dag (repc (high a)) (repc ∝ low) (repc ∝ high) rt"
apply -
apply (drule Nodes_repbc_Dags_eq [rule_format])
apply auto
done
have rt_nTip: "rt ≠ Tip"
proof -
have "repc (high a) ≠ Null"
proof -
note rhigha_in_rNodesn
also have "repc `Nodes n ll ⊆ repc `Nodes (Suc n) ll"
using Nodes_subset
by blast
also have "… ⊆ Nodes (Suc n) ll"
using repcNodes_in_Nodes
by simp
finally show ?thesis
using null_notin_Nodes_Suc_n
by auto
qed
with repcrt_dag show ?thesis by auto
qed
from a_nNull a_in_pret low_nNull pret_dag have "low a ∈ set_of pret"
apply -
apply (drule subelem_set_of_low)
apply auto
done
with wf_ll have "low a ∈ set (ll ! (var (low a)))"
by (simp add: wf_ll_def)
with a_in_lln t2_repc_dag var_children_smaller vara_n
have "∃k<n. (low a) ∈ set (ll ! k)"
by auto
then have "(low a) ∈ Nodes n ll"
by (simp add: Nodes_def)
then have rlow_in_rNodesn: "repc (low a) ∈ repc ` Nodes n ll"
by simp
show ?thesis
proof -
from repp_reduce low_nNull highp_nNull red_case
have repc_p_def: "repc a = repc (high a)"
by (simp add: null_comp_def)
with rt_in_repcNodesn repcrt_dag rhigha_in_rNodesn a_in_lln t2_repc_dag
repc_p_def rt_nTip
have t2_in_Dags_Nodesn:
"t2 ∈ Dags (repc ` Nodes n ll) (repc ∝ low) (repc ∝ high)"
apply -
apply (rule DagsI)
apply simp
apply (subgoal_tac "t2=rt")
apply (auto simp add: Dag_unique)
done
from t1_in_DagsNodesn t2_in_Dags_Nodesn repbc_dags_eq isomorphic_dags_eq_asm
show shared_t1_t2: "isomorphic_dags_eq t1 t2 var"
apply -
apply (erule_tac x=t1 in allE)
apply (erule_tac x=t2 in allE)
apply simp
done
qed
next
assume share: " ¬ ((repc ∝ low) a = (repc ∝ high) a ∧ low a ≠ Null)"
then
have share: "(repc ∝ low) a ≠ (repc ∝ high) a ∨ low a = Null"
using [[simp_depth_limit=1]]
by simp
with repp_share obtain
ra_in_llbn: "repc a ∈ set (ll ! n)" and
rra_ra: "repc (repc a) = repc a" and
two_nodes_share: "(∀no1∈set (ll ! n).
((repc ∝ high) no1 = (repc ∝ high) a ∧
(repc ∝ low) no1 = (repc ∝ low) a) = (repc a = repc no1))"
using [[simp_depth_limit=3]]
by simp
from wf_ll ra_in_llbn nsll have var_repc_a_n: "var (repc a) = n"
by (auto simp add: wf_ll_def length_ll_eq)
show ?thesis
proof (auto simp add: isomorphic_dags_eq_def)
fix bdt1
assume bdt_t1: "bdt t1 var = Some bdt1"
assume bdt_t2: "bdt t2 var = Some bdt1"
show "t1 = t2"
proof (cases t1)
case Tip
with bdt_t1 show ?thesis
by simp
next
case (Node lt1 p1 rt1)
note t1_Node=this
with Dag_q_Nodes_n have "p1=(repc q)"
by simp
with t2_Node bdt_t1 bdt_t2 t1_Node have "var (repc q) = var (repc a)"
apply -
apply (rule same_bdt_var)
apply auto
done
with var_repc_q_n var_repc_a_n show ?thesis
by simp
qed
qed
qed }
note mixed_Dags_case = this
from repbc_dags_eq isomorphic_dags_eq
have dags_shared:
"∀t1 t2. t1 ∈ Dags (repc ` Nodes (Suc n) ll)(repc ∝ low)(repc ∝ high)∧
t2 ∈ Dags (repc ` Nodes (Suc n) ll) (repc ∝ low) (repc ∝ high)
⟶ isomorphic_dags_eq t1 t2 var"
apply -
apply (rule Dags_Nodes_cases)
apply (rule isomorphic_dags_eq_sym)
proof -
fix t1 t2
assume t1_in_Dagsn:
"t1 ∈ Dags (repc ` Nodes n ll) (repc ∝ low) (repc ∝ high)"
assume t2_in_Dagsn:
"t2 ∈ Dags (repc ` Nodes n ll) (repc ∝ low) (repc ∝ high)"
assume isomorphic_dags_eq_asm:
"∀t1 t2. t1 ∈ Dags (repb ` Nodes n ll) (repb ∝ low) (repb ∝ high) ∧
t2 ∈ Dags (repb ` Nodes n ll) (repb ∝ low) (repb ∝ high)
⟶ isomorphic_dags_eq t1 t2 var"
assume repb_repc_Dags:
"Dags (repc ` Nodes n ll) (repc ∝ low) (repc ∝ high) =
Dags (repb ` Nodes n ll) (repb ∝ low) (repb ∝ high)"
with t1_in_Dagsn t2_in_Dagsn isomorphic_dags_eq_asm
show "isomorphic_dags_eq t1 t2 var" by simp
next
fix t1 t2
assume t1_in_DagsNodesn:
"t1 ∈ Dags (repc ` Nodes n ll) (repc ∝ low) (repc ∝ high)"
assume t2_notin_DagsNodesn:
"t2 ∉ Dags (repc ` Nodes n ll) (repc ∝ low) (repc ∝ high)"
assume t2_in_DagsNodesSucn:
"t2 ∈ Dags (repc ` Nodes (Suc n) ll) (repc ∝ low) (repc ∝ high)"
assume isomorphic_dags_eq_asm:
"∀t1 t2. t1 ∈ Dags (repb ` Nodes n ll) (repb ∝ low) (repb ∝ high) ∧
t2 ∈ Dags (repb ` Nodes n ll) (repb ∝ low) (repb ∝ high)
⟶ isomorphic_dags_eq t1 t2 var"
assume repbc_Dags:
"Dags (repc ` Nodes n ll) (repc ∝ low) (repc ∝ high) =
Dags (repb ` Nodes n ll) (repb ∝ low) (repb ∝ high)"
from t1_in_DagsNodesn t2_notin_DagsNodesn t2_in_DagsNodesSucn
isomorphic_dags_eq_asm repbc_Dags
show "isomorphic_dags_eq t1 t2 var"
apply -
apply (rule mixed_Dags_case)
apply auto
done
next
fix t1 t2
assume t1_in_DagsNodesSucn:
"t1 ∈ Dags (repc ` Nodes (Suc n) ll) (repc ∝ low) (repc ∝ high)"
assume t1_notin_DagsNodesn:
"t1 ∉ Dags (repc ` Nodes n ll) (repc ∝ low) (repc ∝ high)"
assume t2_in_DagsNodesSucn:
"t2 ∈ Dags (repc ` Nodes (Suc n) ll) (repc ∝ low) (repc ∝ high)"
assume t2_notin_DagsNodesn:
"t2 ∉ Dags (repc ` Nodes n ll) (repc ∝ low) (repc ∝ high)"
from t1_in_DagsNodesSucn have ord_t1: "ordered t1 var"
proof (elim Dags.cases)
fix p t
assume t_in_repcNodes: "set_of t ⊆ repc ` Nodes (Suc n) ll"
assume t_nTip: " t ≠ Tip"
assume t2t: "t1 = t"
assume t_dag: "Dag p (repc ∝ low) (repc ∝ high) t"
from t_in_repcNodes
have x_in_repcNodesSucn:
"∀ x. x ∈ set_of t ⟶ x ∈ repc ` Nodes (Suc n) ll"
apply -
apply auto
done
from t_nTip t_dag have "p ≠ Null"
apply -
apply (case_tac "p=Null")
apply auto
done
with t_nTip t_dag obtain lt rt where t_Node: "t=Node lt p rt"
by auto
then have "p ∈ set_of t"
by auto
with x_in_repcNodesSucn have "p ∈ repc ` Nodes (Suc n) ll"
by simp
then obtain a where
repca_p: "p=repc a" and a_in_NodesSucn: "a ∈ Nodes (Suc n) ll"
by auto
with repca_p while_while_prop t_dag t2t show ?thesis
apply -
apply (erule_tac x=a in ballE)
apply (elim conjE exE)
apply (subgoal_tac "nort = t")
prefer 2
apply (simp add: Dag_unique)
apply auto
done
qed
from while_while_prop
have while_prop_part: "∀no ∈ Nodes (Suc n) ll.
var (repc no) <= var no"
by auto
from while_while_prop have rep_rep_nort:
"∀no∈Nodes (n + 1) ll.
(∃nort. Dag (repc no) (repc ∝ low) (repc ∝ high) nort ∧
(∀no∈set_of nort. repc no = no))"
by auto
from repcNodes_in_Nodes null_notin_Nodes_Suc_n
have "∀ no ∈ Nodes (n+1) ll. repc no ≠ Null"
by auto
with rep_rep_nort
have rep_rep_no: "∀no ∈ Nodes (n+1) ll. repc (repc no) = (repc no)"
apply -
apply (rule ballI)
apply (erule_tac x=no in ballE)
prefer 2
apply simp
apply (erule_tac x=no in ballE)
apply (erule exE)
apply (subgoal_tac "repc no ∈ set_of nort")
apply (elim conjE)
apply (erule_tac x="repc no" in ballE)
apply simp
apply simp
apply (simp)
apply (elim conjE)
apply (thin_tac "∀no∈set_of nort. repc no = no")
apply auto
done
with t1_in_DagsNodesSucn t1_notin_DagsNodesn ord_t1 while_prop_part wf_ll
nsll repcNodes_in_Nodes obtain a1 where
t1_repc_dag: "Dag (repc a1) (repc ∝ low) (repc ∝ high) t1" and
a1_in_lln: "a1 ∈ set (ll ! n)"
apply -
apply (drule restrict_root_Node)
apply (auto simp add: length_ll_eq)
done
with wf_ll nsll have a1_in_pret: "a1 ∈ set_of pret"
by (simp add: wf_ll_def length_ll_eq)
from wf_ll nsll a1_in_lln have vara1_n: "var a1 = n"
by (simp add: wf_ll_def length_ll_eq)
from a1_in_lln rep_prop obtain
repa1_nNull: " repc a1 ≠ Null" and
repa1_reduce: "(repc ∝ low) a1 = (repc ∝ high) a1 ∧ low a1 ≠ Null
⟶ repc a1 = (repc ∝ high) a1" and
repa1_share: "((repc ∝ low) a1 = (repc ∝ high) a1 ⟶ low a1 = Null)
⟶ repc a1 ∈ set (ll ! n) ∧ repc (repc a1) = repc a1 ∧
(∀no1∈set (ll ! n). ((repc ∝ high) no1 = (repc ∝ high) a1 ∧
(repc ∝ low) no1 = (repc ∝ low) a1) = (repc a1 = repc no1))"
using [[simp_depth_limit=4]]
by auto
from t1_repc_dag a1_in_lln repa1_nNull obtain lt1 rt1 where
t1_Node: "t1 = (Node lt1 (repc a1) rt1)"
by auto
from t2_in_DagsNodesSucn have ord_t2: "ordered t2 var"
proof (elim Dags.cases)
fix p t
assume t_in_repcNodes: "set_of t ⊆ repc ` Nodes (Suc n) ll"
assume t_nTip: " t ≠ Tip"
assume t2t: "t2 = t"
assume t_dag: "Dag p (repc ∝ low) (repc ∝ high) t"
from t_in_repcNodes
have x_in_repcNodesSucn:
"∀ x. x ∈ set_of t ⟶ x ∈ repc ` Nodes (Suc n) ll"
apply -
apply auto
done
from t_nTip t_dag have "p ≠ Null"
apply -
apply (case_tac "p=Null")
apply auto
done
with t_nTip t_dag obtain lt rt where t_Node: "t=Node lt p rt"
by auto
then have "p ∈ set_of t"
by auto
with x_in_repcNodesSucn have "p ∈ repc ` Nodes (Suc n) ll"
by simp
then obtain a where
repca_p: "p=repc a" and a_in_NodesSucn: "a ∈ Nodes (Suc n) ll"
by auto
with repca_p while_while_prop t_dag t2t show ?thesis
apply -
apply (erule_tac x=a in ballE)
apply (elim conjE exE)
apply (subgoal_tac "nort = t")
prefer 2
apply (simp add: Dag_unique)
apply auto
done
qed
from rep_rep_no t2_in_DagsNodesSucn t2_notin_DagsNodesn ord_t2 while_prop_part wf_ll
nsll repcNodes_in_Nodes obtain a2 where
t2_repc_dag: "Dag (repc a2) (repc ∝ low) (repc ∝ high) t2" and
a2_in_lln: "a2 ∈ set (ll ! n)"
apply -
apply (drule restrict_root_Node)
apply (auto simp add: length_ll_eq)
done
with wf_ll nsll have a2_in_pret: "a2 ∈ set_of pret"
by (simp add: wf_ll_def length_ll_eq)
from wf_ll nsll a2_in_lln have vara2_n: "var a2 = n"
by (simp add: wf_ll_def length_ll_eq)
from a2_in_lln rep_prop obtain
repa2_nNull: " repc a2 ≠ Null" and
repa2_reduce: "(repc ∝ low) a2 = (repc ∝ high) a2 ∧ low a2 ≠ Null
⟶ repc a2 = (repc ∝ high) a2" and
repa2_share: "((repc ∝ low) a2 = (repc ∝ high) a2 ⟶ low a2 = Null)
⟶ repc a2 ∈ set (ll ! n) ∧ repc (repc a2) = repc a2 ∧
(∀no1∈set (ll ! n). ((repc ∝ high) no1 = (repc ∝ high) a2 ∧
(repc ∝ low) no1 = (repc ∝ low) a2) = (repc a2 = repc no1))"
using [[simp_depth_limit = 4]]
by auto
from t2_repc_dag a2_in_lln repa2_nNull obtain lt2 rt2 where
t2_Node: "t2 = (Node lt2 (repc a2) rt2)"
by auto
show "isomorphic_dags_eq t1 t2 var"
proof (cases "(repc ∝ low) a1 = (repc ∝ high) a1 ∧ low a1 ≠ Null")
case True
note t1_red_cond=this
with t1_red_cond have t1_red_case: "(repc ∝ low) a1 = (repc ∝ high) a1"
by simp
from t1_red_cond have lowa1_nNull: "low a1 ≠ Null"
by simp
with pret_dag prebdt_pret a1_in_pret have higha1_nNull: "high a1 ≠ Null"
apply -
apply (drule balanced_bdt)
apply auto
done
from pret_dag ord_pret a1_in_pret lowa1_nNull higha1_nNull
have var_children_smaller_a1: "var (low a1) < var a1 ∧ var (high a1) < var a1"
apply -
apply (rule var_ordered_children)
apply auto
done
from pret_dag a1_in_pret have a1_nNull: "a1 ≠ Null"
apply -
apply (rule set_of_nn [rule_format])
apply auto
done
with a1_in_pret higha1_nNull pret_dag have "high a1 ∈ set_of pret"
apply -
apply (drule subelem_set_of_high)
apply auto
done
with wf_ll have "high a1 ∈ set (ll ! (var (high a1)))"
by (simp add: wf_ll_def)
with a1_in_lln t1_repc_dag var_children_smaller_a1 vara1_n
have "∃k<n. (high a1) ∈ set (ll ! k)"
by auto
then have higha1_in_Nodesn: "(high a1) ∈ Nodes n ll"
by (simp add: Nodes_def)
then have rhigha1_in_rNodesn: "repc (high a1) ∈ repc ` Nodes n ll"
by simp
from higha1_in_Nodesn normalize_prop obtain rt1 where
rt1_dag: "Dag (repb (high a1)) (repb ∝ low) (repb ∝ high) rt1" and
rt1_in_repbNort: "set_of rt1 ⊆ repb `Nodes n ll"
apply -
apply (erule_tac x="high a1" in ballE)
apply auto
done
from rt1_in_repbNort repbNodes_repcNodes
have rt1_in_repcNodesn: "set_of rt1 ⊆ repc `Nodes n ll"
by blast
from rt1_dag higha1_in_Nodesn
have repcrt1_dag: "Dag (repc (high a1)) (repc ∝ low) (repc ∝ high) rt1"
apply -
apply (drule Nodes_repbc_Dags_eq [rule_format])
apply auto
done
have rt1_nTip: "rt1 ≠ Tip"
proof -
have "repc (high a1) ≠ Null"
proof -
note rhigha1_in_rNodesn
also have "repc `Nodes n ll ⊆ repc `Nodes (Suc n) ll"
using Nodes_subset
by blast
also have "… ⊆ Nodes (Suc n) ll"
using repcNodes_in_Nodes
by simp
finally show ?thesis
using null_notin_Nodes_Suc_n
by auto
qed
with repcrt1_dag show ?thesis by auto
qed
from repa1_reduce lowa1_nNull higha1_nNull t1_red_case
have repc_a1_def: "repc a1 = repc (high a1)"
by (simp add: null_comp_def)
with rt1_in_repcNodesn repcrt1_dag rhigha1_in_rNodesn a1_in_lln
t1_repc_dag repc_a1_def rt1_nTip
have t1_in_Dags_Nodesn:
"t1 ∈ Dags (repc ` Nodes n ll) (repc ∝ low) (repc ∝ high)"
apply -
apply (rule DagsI)
apply simp
apply (subgoal_tac "t1=rt1")
apply (auto simp add: Dag_unique)
done
show ?thesis
proof (cases "(repc ∝ low) a2 = (repc ∝ high) a2 ∧ low a2 ≠ Null")
case True
note t2_red_cond=this
with t2_red_cond have t2_red_case: "(repc ∝ low) a2 = (repc ∝ high) a2"
by simp
from t2_red_cond have lowa2_nNull: "low a2 ≠ Null"
by simp
with pret_dag prebdt_pret a2_in_pret have higha2_nNull: "high a2 ≠ Null"
apply -
apply (drule balanced_bdt)
apply auto
done
from pret_dag ord_pret a2_in_pret lowa2_nNull higha2_nNull
have var_children_smaller_a2:
"var (low a2) < var a2 ∧ var (high a2) < var a2"
apply -
apply (rule var_ordered_children)
apply auto
done
from pret_dag a2_in_pret have a2_nNull: "a2 ≠ Null"
apply -
apply (rule set_of_nn [rule_format])
apply auto
done
with a2_in_pret higha2_nNull pret_dag have "high a2 ∈ set_of pret"
apply -
apply (drule subelem_set_of_high)
apply auto
done
with wf_ll have "high a2 ∈ set (ll ! (var (high a2)))"
by (simp add: wf_ll_def)
with a2_in_lln t2_repc_dag var_children_smaller_a2 vara2_n
have "∃ k<n. (high a2) ∈ set (ll ! k)"
by auto
then have higha2_in_Nodesn: "(high a2) ∈ Nodes n ll"
by (simp add: Nodes_def)
then have rhigha2_in_rNodesn: "repc (high a2) ∈ repc ` Nodes n ll"
by simp
from higha2_in_Nodesn normalize_prop obtain rt2 where
rt2_dag: "Dag (repb (high a2)) (repb ∝ low) (repb ∝ high) rt2" and
rt2_in_repbNort: "set_of rt2 ⊆ repb `Nodes n ll"
apply -
apply (erule_tac x="high a2" in ballE)
apply auto
done
from rt2_in_repbNort repbNodes_repcNodes
have rt2_in_repcNodesn: "set_of rt2 ⊆ repc `Nodes n ll"
by blast
from rt2_dag higha2_in_Nodesn
have repcrt2_dag: "Dag (repc (high a2)) (repc ∝ low) (repc ∝ high) rt2"
apply -
apply (drule Nodes_repbc_Dags_eq [rule_format])
apply auto
done
have rt2_nTip: "rt2 ≠ Tip"
proof -
have "repc (high a2) ≠ Null"
proof -
note rhigha2_in_rNodesn
also have "repc `Nodes n ll ⊆ repc `Nodes (Suc n) ll"
using Nodes_subset
by blast
also have "… ⊆ Nodes (Suc n) ll"
using repcNodes_in_Nodes
by simp
finally show ?thesis
using null_notin_Nodes_Suc_n
by auto
qed
with repcrt2_dag show ?thesis by auto
qed
from repa2_reduce lowa2_nNull higha2_nNull t2_red_case
have repc_a2_def: "repc a2 = repc (high a2)"
by (simp add: null_comp_def)
with rt2_in_repcNodesn repcrt2_dag rhigha2_in_rNodesn a2_in_lln
t2_repc_dag repc_a2_def rt2_nTip
have t2_in_Dags_Nodesn:
"t2 ∈ Dags (repc ` Nodes n ll) (repc ∝ low) (repc ∝ high)"
apply -
apply (rule DagsI)
apply simp
apply (subgoal_tac "t2=rt2")
apply (auto simp add: Dag_unique)
done
from isomorphic_dags_eq t1_in_Dags_Nodesn t2_in_Dags_Nodesn repbc_dags_eq
show ?thesis
by auto
next
assume t2_share_cond:
"¬ ((repc ∝ low) a2 = (repc ∝ high) a2 ∧ low a2 ≠ Null)"
from t1_in_Dags_Nodesn t2_notin_DagsNodesn t2_in_DagsNodesSucn
isomorphic_dags_eq repbc_dags_eq
show ?thesis
apply -
apply (rule mixed_Dags_case)
apply auto
done
qed
next
assume t1_share_cond:
"¬((repc ∝ low) a1 = (repc ∝ high) a1 ∧ low a1 ≠ Null)"
with repa1_share obtain
repca1_in_llbn: "repc a1 ∈ set (ll ! n)" and
reprepa1: "repc (repc a1) = repc a1" and
twonodes_llbn_a1:
"(∀no1∈set (ll ! n). ((repc ∝ high) no1 = (repc ∝ high) a1 ∧
(repc ∝ low) no1 = (repc ∝ low) a1) = (repc a1 = repc no1))"
using [[simp_depth_limit=2]]
by auto
show ?thesis
proof (cases "(repc ∝ low) a2 = (repc ∝ high) a2 ∧ low a2 ≠ Null")
case True
note t2_red_cond=this
with t2_red_cond have t2_red_case: "(repc ∝ low) a2 = (repc ∝ high) a2"
by simp
from t2_red_cond have lowa2_nNull: "low a2 ≠ Null"
by simp
with pret_dag prebdt_pret a2_in_pret have higha2_nNull: "high a2 ≠ Null"
apply -
apply (drule balanced_bdt)
apply auto
done
from pret_dag ord_pret a2_in_pret lowa2_nNull higha2_nNull
have var_children_smaller_a2:
"var (low a2) < var a2 ∧ var (high a2) < var a2"
apply -
apply (rule var_ordered_children)
apply auto
done
from pret_dag a2_in_pret have a2_nNull: "a2 ≠ Null"
apply -
apply (rule set_of_nn [rule_format])
apply auto
done
with a2_in_pret higha2_nNull pret_dag have "high a2 ∈ set_of pret"
apply -
apply (drule subelem_set_of_high)
apply auto
done
with wf_ll
have "high a2 ∈ set (ll ! (var (high a2)))"
by (simp add: wf_ll_def)
with a2_in_lln t2_repc_dag var_children_smaller_a2 vara2_n
have "∃ k<n. (high a2) ∈ set (ll ! k)"
by auto
then have higha2_in_Nodesn: "(high a2) ∈ Nodes n ll"
by (simp add: Nodes_def)
then have rhigha2_in_rNodesn: "repc (high a2) ∈ repc ` Nodes n ll"
by simp
from higha2_in_Nodesn normalize_prop obtain rt2 where
rt2_dag: "Dag (repb (high a2)) (repb ∝ low) (repb ∝ high) rt2" and
rt2_in_repbNort: "set_of rt2 ⊆ repb `Nodes n ll"
apply -
apply (erule_tac x="high a2" in ballE)
apply auto
done
from rt2_in_repbNort repbNodes_repcNodes
have rt2_in_repcNodesn: "set_of rt2 ⊆ repc `Nodes n ll"
by blast
from rt2_dag higha2_in_Nodesn
have repcrt2_dag: "Dag (repc (high a2)) (repc ∝ low) (repc ∝ high) rt2"
apply -
apply (drule Nodes_repbc_Dags_eq [rule_format])
apply auto
done
have rt2_nTip: "rt2 ≠ Tip"
proof -
have "repc (high a2) ≠ Null"
proof -
note rhigha2_in_rNodesn
also have "repc `Nodes n ll ⊆ repc `Nodes (Suc n) ll"
using Nodes_subset
by blast
also have "… ⊆ Nodes (Suc n) ll"
using repcNodes_in_Nodes
by simp
finally show ?thesis
using null_notin_Nodes_Suc_n
by auto
qed
with repcrt2_dag show ?thesis by auto
qed
from repa2_reduce lowa2_nNull higha2_nNull t2_red_case
have repc_a2_def: "repc a2 = repc (high a2)"
by (simp add: null_comp_def)
with rt2_in_repcNodesn repcrt2_dag rhigha2_in_rNodesn a2_in_lln
t2_repc_dag repc_a2_def rt2_nTip
have t2_in_Dags_Nodesn:
"t2 ∈ Dags (repc ` Nodes n ll) (repc ∝ low) (repc ∝ high)"
apply -
apply (rule DagsI)
apply simp
apply (subgoal_tac "t2=rt2")
apply (auto simp add: Dag_unique)
done
from t2_in_Dags_Nodesn t1_notin_DagsNodesn t1_in_DagsNodesSucn
isomorphic_dags_eq repbc_dags_eq
have "isomorphic_dags_eq t2 t1 var"
apply -
apply (rule mixed_Dags_case)
apply auto
done
then show ?thesis
by (simp add: isomorphic_dags_eq_sym)
next
assume t2_shared_cond:
"¬ ((repc ∝ low) a2 = (repc ∝ high) a2 ∧ low a2 ≠ Null)"
with repa2_share obtain
repca2_in_llbn: "repc a2 ∈ set (ll ! n)" and
reprepa2: "repc (repc a2) = repc a2" and
twonodes_llbn_a2: "(∀no1∈set (ll ! n).
((repc ∝ high) no1 = (repc ∝ high) a2 ∧
(repc ∝ low) no1 = (repc ∝ low) a2) = (repc a2 = repc no1))"
using [[simp_depth_limit=2]]
by auto
from twonodes_llbn_a2 a1_in_lln
have share_a1_a2:
"((repc ∝ high) a1 = (repc ∝ high) a2 ∧
(repc ∝ low) a1 = (repc ∝ low) a2) = (repc a2 = repc a1)"
by auto
from twonodes_llbn_a1 repca1_in_llbn reprepa1
have children_repc_eq_a1: "(repc ∝ high) (repc a1) = (repc ∝ high) a1 ∧
(repc ∝ low) (repc a1) = (repc ∝ low) a1"
by auto
from twonodes_llbn_a2 repca2_in_llbn reprepa2
have children_repc_eq_a2: "(repc ∝ high) (repc a2) = (repc ∝ high) a2 ∧
(repc ∝ low) (repc a2) = (repc ∝ low) a2"
by auto
from t1_Node t2_Node show ?thesis
proof (clarsimp simp add: isomorphic_dags_eq_def)
fix bdt1
assume t1_bdt: "bdt (Node lt1 (repc a1) rt1) var = Some bdt1"
assume t2_bdt: "bdt (Node lt2 (repc a2) rt2) var = Some bdt1"
show "lt1 = lt2 ∧ repc a1 = repc a2 ∧ rt1 = rt2"
proof (cases bdt1)
case Zero
with t1_bdt t1_Node obtain
lt1_Tip: "lt1 = Tip" and
rt1_Tip: "rt1 = Tip"
by simp
from Zero t2_bdt t2_Node obtain
lt2_Tip: "lt2 = Tip" and
rt2_Tip: "rt2 = Tip"
by simp
from t1_repc_dag t1_Node lt1_Tip have "(repc ∝ low) (repc a1) = Null"
by simp
with children_repc_eq_a1
have repc_low_a1_Null: "(repc ∝ low) a1 = Null"
by simp
from t1_repc_dag t1_Node rt1_Tip
have "(repc ∝ high) (repc a1) = Null"
by simp
with children_repc_eq_a1
have repc_high_a1_Null: "(repc ∝ high) a1 = Null"
by simp
from t2_repc_dag t2_Node lt2_Tip have "(repc ∝ low) (repc a2) = Null"
by simp
with children_repc_eq_a2
have repc_low_a2_Null: "(repc ∝ low) a2 = Null"
by simp
from t2_repc_dag t2_Node rt2_Tip
have "(repc ∝ high) (repc a2) = Null"
by simp
with children_repc_eq_a2
have repc_high_a2_Null: "(repc ∝ high) a2 = Null"
by simp
with share_a1_a2 repc_low_a1_Null repc_high_a1_Null
repc_low_a2_Null repc_high_a2_Null
have "repc a2 = repc a1"
by auto
with lt1_Tip rt1_Tip lt2_Tip rt2_Tip show ?thesis
by auto
next
case One
with t1_bdt t1_Node obtain
lt1_Tip: "lt1 = Tip" and
rt1_Tip: "rt1 = Tip"
by simp
from One t2_bdt t2_Node obtain
lt2_Tip: "lt2 = Tip" and
rt2_Tip: "rt2 = Tip"
by simp
from t1_repc_dag t1_Node lt1_Tip have "(repc ∝ low) (repc a1) = Null"
by simp
with children_repc_eq_a1
have repc_low_a1_Null: "(repc ∝ low) a1 = Null"
by simp
from t1_repc_dag t1_Node rt1_Tip have "(repc ∝ high) (repc a1) = Null"
by simp
with children_repc_eq_a1
have repc_high_a1_Null: "(repc ∝ high) a1 = Null"
by simp
from t2_repc_dag t2_Node lt2_Tip have "(repc ∝ low) (repc a2) = Null"
by simp
with children_repc_eq_a2
have repc_low_a2_Null: "(repc ∝ low) a2 = Null"
by simp
from t2_repc_dag t2_Node rt2_Tip have "(repc ∝ high) (repc a2) = Null"
by simp
with children_repc_eq_a2
have repc_high_a2_Null: "(repc ∝ high) a2 = Null"
by simp
with share_a1_a2 repc_low_a1_Null repc_high_a1_Null
repc_low_a2_Null repc_high_a2_Null
have "repc a2 = repc a1"
by auto
with lt1_Tip rt1_Tip lt2_Tip rt2_Tip show ?thesis
by auto
next
case (Bdt_Node lbdt v rbdt)
note bdt_Node_case=this
with t1_bdt t1_Node obtain
lbdt_def_lt1: "bdt lt1 var = Some lbdt" and
rbdt_def_rt1: "bdt rt1 var = Some rbdt"
by auto
from t2_bdt bdt_Node_case t2_Node obtain
lbdt_def_lt2: "bdt lt2 var = Some lbdt" and
rbdt_def_rt2: "bdt rt2 var = Some rbdt"
by auto
from lbdt_def_lt1 t1_Node t1_repc_dag children_repc_eq_a1
have "(repc ∝ low) a1 ≠ Null"
by auto
then have low_a1_nNull: "(low a1) ≠ Null"
by (auto simp: null_comp_def)
from rbdt_def_rt1 t1_Node t1_repc_dag children_repc_eq_a1
have "(repc ∝ high) a1 ≠ Null"
by auto
then have high_a1_nNull: "(high a1) ≠ Null"
by (auto simp: null_comp_def)
from lbdt_def_lt2 t2_Node t2_repc_dag children_repc_eq_a2
have "(repc ∝ low) a2 ≠ Null"
by auto
then have low_a2_nNull: "(low a2) ≠ Null"
by (auto simp: null_comp_def)
from rbdt_def_rt2 t2_Node t2_repc_dag children_repc_eq_a2
have "(repc ∝ high) a2 ≠ Null"
by auto
then have high_a2_nNull: "(high a2) ≠ Null"
by (auto simp: null_comp_def)
from pret_dag ord_pret a1_in_pret low_a1_nNull high_a1_nNull
have var_children_smaller_a1:
"var (low a1) < var a1 ∧ var (high a1) < var a1"
apply -
apply (rule var_ordered_children)
apply auto
done
from pret_dag a1_in_pret have a1_nNull: "a1 ≠ Null"
apply -
apply (rule set_of_nn [rule_format])
apply auto
done
with a1_in_pret high_a1_nNull pret_dag have "high a1 ∈ set_of pret"
apply -
apply (drule subelem_set_of_high)
apply auto
done
with wf_ll
have "high a1 ∈ set (ll ! (var (high a1)))"
by (simp add: wf_ll_def)
with a1_in_lln t1_repc_dag var_children_smaller_a1 vara1_n
have "∃ k<n. (high a1) ∈ set (ll ! k)"
by auto
then have higha1_in_Nodesn: "(high a1) ∈ Nodes n ll"
by (simp add: Nodes_def)
then have rhigha1_in_rNodesn:
"repc (high a1) ∈ repc ` Nodes n ll"
by simp
from higha1_in_Nodesn normalize_prop obtain rt1h where
rt1_dag: "Dag (repb (high a1)) (repb ∝ low) (repb ∝ high) rt1h" and
rt1_in_repbNort: "set_of rt1h ⊆ repb `Nodes n ll"
apply -
apply (erule_tac x="high a1" in ballE)
apply auto
done
from rt1_in_repbNort repbNodes_repcNodes
have rt1_in_repcNodesn: "set_of rt1h ⊆ repc `Nodes n ll"
by blast
from rt1_dag higha1_in_Nodesn
have repcrt1_dag:
"Dag (repc (high a1)) (repc ∝ low) (repc ∝ high) rt1h"
apply -
apply (drule Nodes_repbc_Dags_eq [rule_format])
apply auto
done
from t1_Node t1_repc_dag high_a1_nNull children_repc_eq_a1
have "Dag (repc (high a1)) (repc ∝ low) (repc ∝ high) rt1"
by (auto simp add: null_comp_def)
with repcrt1_dag have rt1h_rt1: "rt1h = rt1" by (simp add: Dag_unique)
have rt1_nTip: "rt1 ≠ Tip"
proof -
have "repc (high a1) ≠ Null"
proof -
note rhigha1_in_rNodesn
also have
"repc `Nodes n ll ⊆ repc `Nodes (Suc n) ll"
using Nodes_subset
by blast
also have "… ⊆ Nodes (Suc n) ll"
using repcNodes_in_Nodes
by simp
finally show ?thesis
using null_notin_Nodes_Suc_n
by auto
qed
with repcrt1_dag rt1h_rt1 show ?thesis by auto
qed
with rt1_in_repcNodesn repcrt1_dag rhigha1_in_rNodesn a1_in_lln
t1_repc_dag rt1h_rt1
have rt1_in_Dags_Nodesn:
"rt1 ∈ Dags (repc ` Nodes n ll) (repc ∝ low) (repc ∝ high)"
apply -
apply (rule DagsI)
apply auto
done
from a1_nNull a1_in_pret low_a1_nNull pret_dag
have "low a1 ∈ set_of pret"
apply -
apply (drule subelem_set_of_low)
apply auto
done
with wf_ll have
"low a1 ∈ set (ll ! (var (low a1)))" by (simp add: wf_ll_def)
with a1_in_lln t1_repc_dag var_children_smaller_a1 vara1_n
have "∃ k<n. (low a1) ∈ set (ll ! k)"
by auto
then have lowa1_in_Nodesn: "(low a1) ∈ Nodes n ll"
by (simp add: Nodes_def)
then have rlowa1_in_rNodesn: "repc (low a1) ∈ repc ` Nodes n ll"
by simp
from lowa1_in_Nodesn normalize_prop obtain lt1h where
lt1_dag: "Dag (repb (low a1)) (repb ∝ low) (repb ∝ high) lt1h" and
lt1_in_repbNort: "set_of lt1h ⊆ repb `Nodes n ll"
apply -
apply (erule_tac x="low a1" in ballE)
apply auto
done
from lt1_in_repbNort repbNodes_repcNodes
have lt1_in_repcNodesn: "set_of lt1h ⊆ repc `Nodes n ll"
by blast
from lt1_dag lowa1_in_Nodesn
have repclt1_dag: "Dag (repc (low a1)) (repc ∝ low) (repc ∝ high) lt1h"
apply -
apply (drule Nodes_repbc_Dags_eq [rule_format])
apply auto
done
from t1_Node t1_repc_dag low_a1_nNull children_repc_eq_a1
have "Dag (repc (low a1)) (repc ∝ low) (repc ∝ high) lt1"
by (auto simp add: null_comp_def)
with repclt1_dag have lt1h_lt1: "lt1h = lt1" by (simp add: Dag_unique)
have lt1_nTip: "lt1 ≠ Tip"
proof -
have "repc (low a1) ≠ Null"
proof -
note rlowa1_in_rNodesn
also have
"repc `Nodes n ll ⊆ repc `Nodes (Suc n) ll"
using Nodes_subset
by blast
also have "… ⊆ Nodes (Suc n) ll"
using repcNodes_in_Nodes
by simp
finally show ?thesis
using null_notin_Nodes_Suc_n
by auto
qed
with repclt1_dag lt1h_lt1 show ?thesis by auto
qed
with lt1_in_repcNodesn repclt1_dag rlowa1_in_rNodesn a1_in_lln
t1_repc_dag lt1h_lt1
have lt1_in_Dags_Nodesn:
"lt1 ∈ Dags (repc ` Nodes n ll) (repc ∝ low) (repc ∝ high)"
apply -
apply (rule DagsI)
apply auto
done
from pret_dag ord_pret a2_in_pret low_a2_nNull high_a2_nNull
have var_children_smaller_a2:
"var (low a2) < var a2 ∧ var (high a2) < var a2"
apply -
apply (rule var_ordered_children)
apply auto
done
from pret_dag a2_in_pret have a2_nNull: "a2 ≠ Null"
apply -
apply (rule set_of_nn [rule_format])
apply auto
done
with a2_in_pret high_a2_nNull pret_dag have "high a2 ∈ set_of pret"
apply -
apply (drule subelem_set_of_high)
apply auto
done
with wf_ll have "high a2 ∈ set (ll ! (var (high a2)))"
by (simp add: wf_ll_def)
with a2_in_lln t2_repc_dag var_children_smaller_a2 vara2_n
have "∃ k<n. (high a2) ∈ set (ll ! k)"
by auto
then have higha2_in_Nodesn: "(high a2) ∈ Nodes n ll"
by (simp add: Nodes_def)
then have rhigha2_in_rNodesn:
"repc (high a2) ∈ repc ` Nodes n ll"
by simp
from higha2_in_Nodesn normalize_prop obtain rt2h where
rt2_dag: "Dag (repb (high a2)) (repb ∝ low) (repb ∝ high) rt2h" and
rt2_in_repbNort: "set_of rt2h ⊆ repb `Nodes n ll"
apply -
apply (erule_tac x="high a2" in ballE)
apply auto
done
from rt2_in_repbNort repbNodes_repcNodes
have rt2_in_repcNodesn: "set_of rt2h ⊆ repc `Nodes n ll"
by blast
from rt2_dag higha2_in_Nodesn
have repcrt2_dag:
"Dag (repc (high a2)) (repc ∝ low) (repc ∝ high) rt2h"
apply -
apply (drule Nodes_repbc_Dags_eq [rule_format])
apply auto
done
from t2_Node t2_repc_dag high_a2_nNull children_repc_eq_a2
have "Dag (repc (high a2)) (repc ∝ low) (repc ∝ high) rt2"
by (auto simp add: null_comp_def)
with repcrt2_dag have rt2h_rt2: "rt2h = rt2" by (simp add: Dag_unique)
have rt2_nTip: "rt2 ≠ Tip"
proof -
have "repc (high a2) ≠ Null"
proof -
note rhigha2_in_rNodesn
also have
"repc `Nodes n ll ⊆ repc `Nodes (Suc n) ll"
using Nodes_subset
by blast
also have "… ⊆ Nodes (Suc n) ll"
using repcNodes_in_Nodes
by simp
finally show ?thesis
using null_notin_Nodes_Suc_n
by auto
qed
with repcrt2_dag rt2h_rt2 show ?thesis by auto
qed
with rt2_in_repcNodesn repcrt2_dag rhigha2_in_rNodesn a2_in_lln
t2_repc_dag rt2h_rt2
have rt2_in_Dags_Nodesn:
"rt2 ∈ Dags (repc ` Nodes n ll) (repc ∝ low) (repc ∝ high)"
apply -
apply (rule DagsI)
apply auto
done
from a2_nNull a2_in_pret low_a2_nNull pret_dag
have "low a2 ∈ set_of pret"
apply -
apply (drule subelem_set_of_low)
apply auto
done
with wf_ll have "low a2 ∈ set (ll ! (var (low a2)))"
by (simp add: wf_ll_def)
with a2_in_lln t2_repc_dag var_children_smaller_a2 vara2_n
have "∃ k<n. (low a2) ∈ set (ll ! k)"
by auto
then have lowa2_in_Nodesn: "(low a2) ∈ Nodes n ll"
by (simp add: Nodes_def)
then have rlowa2_in_rNodesn: "repc (low a2) ∈ repc ` Nodes n ll"
by simp
from lowa2_in_Nodesn normalize_prop obtain lt2h where
lt2_dag: "Dag (repb (low a2)) (repb ∝ low) (repb ∝ high) lt2h" and
lt2_in_repbNort: "set_of lt2h ⊆ repb `Nodes n ll"
apply -
apply (erule_tac x="low a2" in ballE)
apply auto
done
from lt2_in_repbNort repbNodes_repcNodes
have lt2_in_repcNodesn: "set_of lt2h ⊆ repc `Nodes n ll"
by blast
from lt2_dag lowa2_in_Nodesn
have repclt2_dag: "Dag (repc (low a2)) (repc ∝ low) (repc ∝ high) lt2h"
apply -
apply (drule Nodes_repbc_Dags_eq [rule_format])
apply auto
done
from t2_Node t2_repc_dag low_a2_nNull children_repc_eq_a2
have "Dag (repc (low a2)) (repc ∝ low) (repc ∝ high) lt2"
by (auto simp add: null_comp_def)
with repclt2_dag have lt2h_lt2: "lt2h = lt2" by (simp add: Dag_unique)
have lt2_nTip: "lt2 ≠ Tip"
proof -
have "repc (low a2) ≠ Null"
proof -
note rlowa2_in_rNodesn
also have
"repc `Nodes n ll ⊆ repc `Nodes (Suc n) ll"
using Nodes_subset
by blast
also have "… ⊆ Nodes (Suc n) ll"
using repcNodes_in_Nodes
by simp
finally show ?thesis
using null_notin_Nodes_Suc_n
by auto
qed
with repclt2_dag lt2h_lt2 show ?thesis by auto
qed
with lt2_in_repcNodesn repclt2_dag rlowa2_in_rNodesn a2_in_lln
t2_repc_dag lt2h_lt2
have lt2_in_Dags_Nodesn:
"lt2 ∈ Dags (repc ` Nodes n ll) (repc ∝ low) (repc ∝ high)"
apply -
apply (rule DagsI)
apply auto
done
from isomorphic_dags_eq lt1_in_Dags_Nodesn lt2_in_Dags_Nodesn repbc_dags_eq
have shared_lt1_lt2: "isomorphic_dags_eq lt1 lt2 var"
by auto
from isomorphic_dags_eq rt1_in_Dags_Nodesn rt2_in_Dags_Nodesn repbc_dags_eq
have shared_rt1_rt2: "isomorphic_dags_eq rt1 rt2 var"
by auto
from shared_lt1_lt2 lbdt_def_lt1 lbdt_def_lt2 have lt1_lt2: "lt1 = lt2"
by (auto simp add: isomorphic_dags_eq_def)
then have root_lt1_lt2: "root lt1 = root lt2"
by auto
from lt1_nTip t1_repc_dag t1_Node have "(repc ∝ low) (repc a1) ≠ Null"
by auto
with lt1_nTip t1_repc_dag t1_Node obtain llt1 lt1p rlt1 where
lt1_Node: "lt1 = Node llt1 lt1p rlt1"
by auto
with t1_repc_dag t1_Node children_repc_eq_a1 lt1_nTip
have root_lt1: "root lt1 = (repc ∝ low) a1"
by auto
from lt2_nTip t2_repc_dag t2_Node have "(repc ∝ low) (repc a2) ≠ Null"
by auto
with lt2_nTip t2_repc_dag t2_Node obtain llt2 lt2p rlt2 where
lt2_Node: "lt2 = Node llt2 lt2p rlt2"
by auto
with t2_repc_dag t2_Node children_repc_eq_a2 lt2_nTip
have root_lt2: "root lt2 = (repc ∝ low) a2"
by auto
from root_lt1_lt2 root_lt2 root_lt1
have low_a1_a2: "(repc ∝ low) a1 = (repc ∝ low) a2"
by auto
from shared_rt1_rt2 rbdt_def_rt1 rbdt_def_rt2 have rt1_rt2: "rt1 = rt2"
by (auto simp add: isomorphic_dags_eq_def)
then have root_rt1_rt2: "root rt1 = root rt2"
by auto
from rt1_nTip t1_repc_dag t1_Node have "(repc ∝ high) (repc a1) ≠ Null"
by auto
with rt1_nTip t1_repc_dag t1_Node obtain lrt1 rt1p rrt1 where
rt1_Node: "rt1 = Node lrt1 rt1p rrt1"
by auto
with t1_repc_dag t1_Node children_repc_eq_a1 rt1_nTip
have root_rt1: "root rt1 = (repc ∝ high) a1"
by auto
from rt2_nTip t2_repc_dag t2_Node
have "(repc ∝ high) (repc a2) ≠ Null"
by auto
with rt2_nTip t2_repc_dag t2_Node obtain lrt2 rt2p rrt2 where
rt2_Node: "rt2 = Node lrt2 rt2p rrt2"
by auto
with t2_repc_dag t2_Node children_repc_eq_a2 rt2_nTip
have root_rt2: "root rt2 = (repc ∝ high) a2"
by auto
from root_rt1_rt2 root_rt2 root_rt1
have high_a1_a2: "(repc ∝ high) a1 = (repc ∝ high) a2"
by auto
from low_a1_a2 high_a1_a2 share_a1_a2
have "repc a1 = repc a2"
by auto
with lt1_lt2 rt1_rt2 show ?thesis
by auto
qed
qed
qed
qed
qed
from termi dags_shared while_while_prop repcNodes_in_Nodes repc_nc n_var_prop
wf_marking_m_ma
show ?thesis
by auto
qed
qed
with srrl_precond all_nodes_same_var
show ?thesis
apply -
apply (intro conjI)
apply assumption+
done
qed
qed
end