# Theory BinDag

(*  Title:       BDD
Author:      Veronika Ortner and Norbert Schirmer, 2004
Maintainer:  Norbert Schirmer,  norbert.schirmer at web de
*)

(*
BinDag.thy

Copyright (C) 2004-2008 Veronika Ortner and Norbert Schirmer
Some rights reserved, TU Muenchen

This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as

This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.

You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)

section ‹BDD Abstractions›

theory BinDag
imports Simpl.Simpl_Heap
begin

datatype dag = Tip | Node dag ref dag

lemma [simp]: "Node lt a rt ≠ lt"
by (induct lt) auto

lemma [simp]: "lt ≠ Node lt a rt"
by (induct lt) auto

lemma [simp]: "Node lt a rt ≠ rt"
by (induct rt) auto

lemma [simp]: "rt ≠ Node lt a rt"
by (induct rt) auto

primrec set_of:: "dag ⇒ ref set" where
set_of_Tip: "set_of Tip = {}"
| set_of_Node: "set_of (Node lt a rt) = {a} ∪ set_of lt ∪ set_of rt"

primrec DAG:: "dag ⇒ bool" where
"DAG Tip = True"
| "DAG (Node l a r) = (a ∉ set_of l ∧ a ∉ set_of r ∧ DAG l ∧ DAG r)"

primrec subdag:: "dag ⇒ dag ⇒ bool" where
"subdag Tip t = False"
| "subdag (Node l a r) t = (t=l ∨ t=r ∨ subdag l t ∨ subdag r t)"

lemma subdag_size: "subdag t s ⟹ size s < size t"
by  (induct t) auto

lemma subdag_neq: "subdag t s ⟹ t≠s"
by (induct t) (auto dest: subdag_size)

lemma subdag_trans [trans]: "subdag t s ⟹ subdag s r ⟹ subdag t r"
by (induct t) auto

lemma subdag_NodeD:
"subdag t (Node lt a rt) ⟹ subdag t lt ∧ subdag t rt"
by (induct t) auto

lemma subdag_not_sym: "⋀t. ⟦subdag s t; subdag t s⟧ ⟹ P"
by (induct s) (auto dest: subdag_NodeD)

instantiation dag :: order
begin

definition
less_dag_def: "s < (t::dag) ⟷ subdag t s"

definition
le_dag_def: "s ≤ (t::dag) ⟷ s=t ∨ s < t"

lemma le_dag_refl: "(x::dag) ≤ x"

lemma le_dag_trans:
fixes x::dag and  y and z
assumes x_y: "x ≤ y" and y_z: "y ≤ z"
shows "x ≤ z"
proof (cases "x=y")
case True with y_z show ?thesis by simp
next
case False
note x_neq_y = this
with x_y have x_less_y: "x < y" by (simp add: le_dag_def)
show ?thesis
proof (cases "y=z")
case True
with x_y show ?thesis by simp
next
case False
with y_z have "y < z" by (simp add: le_dag_def)
with x_less_y have "x < z"
by (auto simp add: less_dag_def intro: subdag_trans)
thus ?thesis
qed
qed

lemma le_dag_antisym:
fixes x::dag and  y
assumes x_y: "x ≤ y" and y_x: "y ≤ x"
shows "x = y"
proof (cases "x=y")
case True thus ?thesis .
next
case False
with x_y y_x show ?thesis
by (auto simp add: less_dag_def le_dag_def intro: subdag_not_sym)
qed

lemma dag_less_le:
fixes x::dag and y
shows "(x < y) = (x ≤ y ∧ x ≠ y)"
by (auto simp add: less_dag_def le_dag_def dest: subdag_neq)

instance
by standard (auto simp add: dag_less_le le_dag_refl intro: le_dag_trans dest: le_dag_antisym)

end

lemma less_dag_Tip [simp]: "¬ (x < Tip)"

lemma less_dag_Node: "x < (Node l a r) =
(x ≤ l ∨ x ≤ r)"
by (auto simp add: order_le_less less_dag_def)

lemma less_dag_Node': "x < (Node l a r) =
(x=l ∨ x=r ∨ x < l ∨ x < r)"

lemma less_Node_dag: "(Node l a r) < x ⟹ l < x ∧ r < x"
by (auto simp add: less_dag_def dest: subdag_NodeD)

lemma less_dag_set_of: "x < y ⟹ set_of x ⊆ set_of y"
by (unfold less_dag_def, induct y, auto)

lemma le_dag_set_of: "x ≤ y ⟹ set_of x ⊆ set_of y"
apply (unfold le_dag_def)
apply (erule disjE)
apply simp
apply (erule less_dag_set_of)
done

lemma DAG_less: "DAG y ⟹ x < y ⟹ DAG x"
by (induct y) (auto simp add: less_dag_Node')

lemma less_DAG_set_of:
assumes x_less_y: "x < y"
assumes DAG_y: "DAG y"
shows "set_of x ⊂ set_of y"
proof (cases y)
case Tip with x_less_y show ?thesis by simp
next
case (Node l a r)
with DAG_y obtain a: "a ∉ set_of l" "a ∉ set_of r"
by simp
from Node obtain l_less_y: "l < y" and r_less_y: "r < y"
from Node a obtain
l_subset_y: "set_of l ⊂ set_of y" and
r_subset_y: "set_of r ⊂ set_of y"
by auto
from Node x_less_y have "x=l ∨ x=r ∨ x < l ∨ x < r"
thus ?thesis
proof (elim disjE)
assume "x=l"
with l_subset_y show ?thesis by simp
next
assume "x=r"
with r_subset_y show ?thesis by simp
next
assume "x < l"
hence "set_of x ⊆ set_of l"
by (rule less_dag_set_of)
also note l_subset_y
finally show ?thesis .
next
assume "x < r"
hence "set_of x ⊆ set_of r"
by (rule less_dag_set_of)
also note r_subset_y
finally show ?thesis .
qed
qed

lemma in_set_of_decomp:
"p ∈ set_of t = (∃l r. t=(Node l p r) ∨ subdag t (Node l p r))"
(is "?A = ?B")
proof
assume "?A" thus "?B"
by (induct t) auto
next
assume "?B" thus "?A"
by (induct t) auto
qed

primrec Dag:: "ref ⇒ (ref ⇒ ref) ⇒ (ref ⇒ ref) ⇒ dag ⇒ bool"
where
"Dag p l r Tip = (p = Null)" |
"Dag p l r (Node lt a rt) = (p = a ∧ p ≠ Null ∧
Dag (l p) l r lt ∧ Dag (r p) l r  rt)"

lemma Dag_Null [simp]: "Dag Null l r  t = (t = Tip)"
by (cases t) simp_all

lemma Dag_Ref [simp]:
"p≠Null ⟹ Dag p l r  t = (∃lt rt. t=Node lt p rt ∧
Dag (l p) l r lt ∧ Dag (r p) l r rt)"
by (cases t) auto

lemma Null_notin_Dag [simp, intro]: "⋀p l r. Dag p l r t ⟹ Null ∉ set_of t"
by (induct t) auto

theorem notin_Dag_update_l [simp]:
"⋀ p. q ∉ set_of t ⟹ Dag p (l(q := y)) r  t = Dag p l r t"
by (induct t) auto

theorem notin_Dag_update_r [simp]:
"⋀ p. q ∉ set_of t ⟹ Dag p l (r(q := y)) t = Dag p l r t"
by (induct t) auto

lemma Dag_upd_same_l_lemma: "⋀p. p≠Null ⟹ ¬ Dag p (l(p:=p)) r t"
apply (induct t)
apply simp
apply (simp (no_asm_simp) del: fun_upd_apply)
apply (simp (no_asm_simp) only: fun_upd_apply refl if_True)
apply blast
done

lemma Dag_upd_same_l [simp]: "Dag p (l(p:=p)) r t = (p=Null ∧ t=Tip)"
apply (cases "p=Null")
apply simp
apply (fast dest: Dag_upd_same_l_lemma)
done

text ‹@{thm[source] Dag_upd_same_l} prevents
@{term "p≠Null ⟹ Dag p (l(p:=p)) r t = X"} from looping, because of
@{thm[source] Dag_Ref} and @{thm[source] fun_upd_apply}.
›

lemma Dag_upd_same_r_lemma: "⋀p. p≠Null ⟹ ¬ Dag p l (r(p:=p)) t"
apply (induct t)
apply simp
apply (simp (no_asm_simp) del: fun_upd_apply)
apply (simp (no_asm_simp) only: fun_upd_apply refl if_True)
apply blast
done

lemma Dag_upd_same_r [simp]: "Dag p l (r(p:=p)) t = (p=Null ∧ t=Tip)"
apply (cases "p=Null")
apply simp
apply (fast dest: Dag_upd_same_r_lemma)
done

lemma  Dag_update_l_new [simp]: "⟦set_of t ⊆ set alloc⟧
⟹ Dag p (l(new (set alloc) := x)) r t = Dag p l r t"
by (rule notin_Dag_update_l) fastforce

lemma  Dag_update_r_new [simp]: "⟦set_of t ⊆ set alloc⟧
⟹ Dag p l (r(new (set alloc) := x)) t = Dag p l r t"
by (rule notin_Dag_update_r) fastforce

lemma Dag_update_lI [intro]:
"⟦Dag p l r t; q ∉ set_of t⟧ ⟹ Dag p (l(q := y)) r t"
by simp

lemma Dag_update_rI [intro]:
"⟦Dag p l r t; q ∉ set_of t⟧ ⟹ Dag p l (r(q := y)) t"
by simp

lemma Dag_unique: "⋀ p t2. Dag p l r t1 ⟹ Dag p l r t2 ⟹ t1=t2"
by (induct t1) auto

lemma Dag_unique1: "Dag p l r t ⟹ ∃!t. Dag p l r t"
by (blast intro: Dag_unique)

lemma Dag_subdag: "⋀ p. Dag p l r t ⟹ subdag t s ⟹ ∃ q. Dag q l r s"
by (induct t) auto

lemma Dag_root_not_in_subdag_l [simp,intro]:
assumes "Dag (l p) l r t"
shows "p ∉ set_of t"
proof -
{
fix lt rt
assume t: "t = Node lt p rt"
from assms have "Dag (l p) l r lt"
by (clarsimp simp only: t Dag.simps)
with assms have "t=lt"
by (rule Dag_unique)
with t have False
by simp
}
moreover
{
fix lt rt
assume subdag: "subdag t (Node lt p rt)"
with assms obtain q where "Dag q l r (Node lt p rt)"
by (rule Dag_subdag [elim_format]) iprover
hence "Dag (l p) l r lt"
by auto
with assms have "t=lt"
by (rule Dag_unique)
moreover
have "subdag t lt"
proof -
note subdag
also have "subdag (Node lt p rt) lt" by simp
finally show ?thesis .
qed
ultimately have False
}
ultimately show ?thesis
qed

lemma Dag_root_not_in_subdag_r [simp, intro]:
assumes "Dag (r p) l r t"
shows "p ∉ set_of t"
proof -
{
fix lt rt
assume t: "t = Node lt p rt"
from assms have "Dag (r p) l r rt"
by (clarsimp simp only: t Dag.simps)
with assms have "t=rt"
by (rule Dag_unique)
with t have False
by simp
}
moreover
{
fix lt rt
assume subdag: "subdag t (Node lt p rt)"
with assms obtain q where "Dag q l r (Node lt p rt)"
by (rule Dag_subdag [elim_format]) iprover
hence "Dag (r p) l r rt"
by auto
with assms have "t=rt"
by (rule Dag_unique)
moreover
have "subdag t rt"
proof -
note subdag
also have "subdag (Node lt p rt) rt" by simp
finally show ?thesis .
qed
ultimately have False
}
ultimately show ?thesis
qed

lemma Dag_is_DAG: "⋀p l r. Dag p l r t ⟹ DAG t"
by (induct t) auto

lemma heaps_eq_Dag_eq:
"⋀p. ∀x ∈ set_of t. l x = l' x ∧ r x = r' x
⟹ Dag p l r t = Dag p l' r' t"
by (induct t) auto

lemma heaps_eq_DagI1:
"⟦Dag p l r t; ∀x∈set_of t. l x = l' x ∧ r x = r' x⟧
⟹ Dag p l' r' t"
by (rule heaps_eq_Dag_eq [THEN iffD1])

lemma heaps_eq_DagI2:
"⟦Dag p l' r' t; ∀x∈set_of t. l x = l' x ∧ r x = r' x⟧
⟹ Dag p l r t"
by (rule heaps_eq_Dag_eq [THEN iffD2]) auto

lemma  Dag_unique_all_impl_simp [simp]:
"Dag p l r t ⟹ (∀t. Dag p l r t ⟶ P t) = P t"
by (auto dest: Dag_unique)

lemma Dag_unique_ex_conj_simp [simp]:
"Dag p l r t ⟹ (∃t. Dag p l r t ∧ P t) = P t"
by (auto dest: Dag_unique)

lemma Dags_eq_hp_eq:
"⋀p p'. ⟦Dag p l r t; Dag p' l' r' t⟧ ⟹
p'=p ∧ (∀no ∈ set_of t. l' no = l no ∧ r' no = r no)"
by (induct t) auto

definition isDag :: "ref ⇒ (ref ⇒ ref) ⇒ (ref ⇒ ref) ⇒ bool"
where "isDag p l r = (∃t. Dag p l r t)"

definition dag :: "ref ⇒ (ref ⇒ ref) ⇒ (ref ⇒ ref) ⇒ dag"
where "dag p l r = (THE t. Dag p l r t)"

lemma Dag_conv_isDag_dag: "Dag p l r t = (isDag p l r ∧ t=dag p l r)"
apply (rule iffI)
apply (rule conjI)
apply blast
apply (subst the1_equality)
apply (erule Dag_unique1)
apply assumption
apply (rule refl)
apply clarify
apply (rule theI)
apply assumption
apply (erule (1) Dag_unique)
done

lemma Dag_dag: "Dag p l r t ⟹ dag p l r = t"

end


# Theory General

(*  Title:       BDD
Author:      Veronika Ortner and Norbert Schirmer, 2004
Maintainer:  Norbert Schirmer,  norbert.schirmer at web de
*)

(*
General.thy

Copyright (C) 2004-2008 Veronika Ortner and Norbert Schirmer
Some rights reserved, TU Muenchen

This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as

This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.

You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)

section ‹General Lemmas on BDD Abstractions›

theory General imports BinDag begin

definition subdag_eq:: "dag ⇒ dag ⇒ bool" where
"subdag_eq t⇩1 t⇩2 = (t⇩1 = t⇩2 ∨ subdag t⇩1 t⇩2)"
(*"subtree_eq Tip t = (if t = Tip then True else False)"
"subtree_eq (Node l a r) t = (t=(Node l a r) ∨ subtree_eq l t ∨ subtree_eq r t)"*)

primrec root :: "dag ⇒ ref"
where
"root Tip = Null" |
"root (Node l a r) = a"

fun isLeaf :: "dag ⇒ bool" where
"isLeaf Tip = False"
| "isLeaf (Node Tip v Tip) = True"
| "isLeaf (Node (Node l v⇩1 r) v⇩2 Tip) = False"
| "isLeaf (Node Tip v⇩1 (Node l v⇩2 r)) = False"

datatype bdt = Zero | One | Bdt_Node bdt nat bdt

fun bdt_fn :: "dag ⇒ (ref ⇒ nat) ⇒ bdt option" where
"bdt_fn Tip = (λbdtvar . None)"
| "bdt_fn (Node Tip vref Tip) =
(λbdtvar .
(if (bdtvar vref = 0)
then Some Zero
else (if (bdtvar vref = 1)
then Some One
else None)))"
| "bdt_fn (Node Tip vref (Node l vref1 r)) = (λbdtvar . None)"
| "bdt_fn (Node (Node l vref1 r) vref Tip) = (λbdtvar . None)"
| "bdt_fn (Node (Node l1 vref1 r1) vref (Node l2 vref2 r2)) =
(λbdtvar .
(if (bdtvar vref = 0 ∨ bdtvar vref = 1)
then None
else
(case (bdt_fn (Node l1 vref1 r1) bdtvar) of
None ⇒ None
|(Some b1) ⇒
(case (bdt_fn (Node l2 vref2 r2) bdtvar) of
None ⇒ None
|(Some b2) ⇒ Some (Bdt_Node b1 (bdtvar vref) b2)))))"

(*
Kongruenzregeln sind das Feintuning für den Simplifier (siehe Kapitel 9 im Isabelle
Tutorial). Im Fall von case wird standardmäßig nur die case bedingung nicht
aber die einzelnen Fälle simplifiziert, analog dazu beim if. Dies simuliert die
Auswertungsstrategie einer Programmiersprache, da wird auch zunächst nur die
Bedingung vereinfacht. Will man mehr so kann man die entsprechenden Kongruenz
regeln dazunehmen.
*)
abbreviation "bdt == bdt_fn"

primrec eval :: "bdt ⇒ bool list ⇒ bool"
where
"eval Zero env = False" |
"eval One env  = True" |
"eval (Bdt_Node l v r) env  = (if (env ! v) then eval r env else eval l env)"

(*A given bdt is ordered if it is a One or Zero or its value is smaller than
its parents value*)
fun ordered_bdt:: "bdt ⇒ bool" where
"ordered_bdt Zero = True"
| "ordered_bdt One = True"
| "ordered_bdt (Bdt_Node (Bdt_Node l1 v1 r1) v (Bdt_Node l2 v2 r2)) =
((v1 < v) ∧ (v2 < v) ∧
(ordered_bdt (Bdt_Node l1 v1 r1)) ∧ (ordered_bdt (Bdt_Node l2 v2 r2)))"
| "ordered_bdt (Bdt_Node (Bdt_Node l1 v1 r1) v r) =
((v1 < v) ∧ (ordered_bdt (Bdt_Node l1 v1 r1)))"
| "ordered_bdt (Bdt_Node l v (Bdt_Node l2 v2 r2)) =
((v2 < v) ∧ (ordered_bdt (Bdt_Node l2 v2 r2)))"
| "ordered_bdt (Bdt_Node l v r) = True"

(*In case t = (Node Tip v Tip) v should have the values 0 or 1. This is not checked by this function*)
fun ordered:: "dag ⇒ (ref⇒nat) ⇒ bool" where
"ordered Tip = (λ var. True)"
| "ordered (Node (Node l⇩1 v⇩1 r⇩1) v (Node l⇩2 v⇩2 r⇩2)) =
(λ var. (var v⇩1 < var v ∧ var v⇩2 < var v) ∧
(ordered (Node l⇩1 v⇩1 r⇩1) var) ∧ (ordered (Node l⇩2 v⇩2 r⇩2) var))"
| "ordered (Node Tip v Tip) = (λ var. (True))"
| "ordered (Node Tip v r) =
(λ var. (var (root r) < var v) ∧ (ordered r var))"
| "ordered (Node l v Tip) =
(λ var. (var (root l) < var v) ∧ (ordered l var))"

(*Calculates maximal value in a non ordered bdt. Does not test parents of the
given bdt*)
primrec max_var :: "bdt ⇒ nat"
where
"max_var Zero = 0" |
"max_var One = 1" |
"max_var (Bdt_Node l v r) = max v (max (max_var l) (max_var r))"

lemma eval_zero: "⟦bdt (Node l v r) var = Some x;
var (root (Node l v r)) = (0::nat)⟧ ⟹ x = Zero"
apply (cases l)
apply (cases r)
apply simp
apply simp
apply (cases r)
apply simp
apply simp
done

lemma bdt_Some_One_iff [simp]:
"(bdt t var = Some One) = (∃ p. t = Node Tip p Tip ∧ var p = 1)"
apply (induct t rule: bdt_fn.induct)
apply (auto split: option.splits) (*in order to split the cases Zero and One*)
done

lemma bdt_Some_Zero_iff [simp]:
"(bdt t var = Some Zero) = (∃ p. t = Node Tip p Tip ∧ var p = 0)"
apply (induct t rule: bdt_fn.induct)
apply (auto split: option.splits)
done

lemma bdt_Some_Node_iff [simp]:
"(bdt t var = Some (Bdt_Node bdt1 v bdt2)) =
(∃ p l r. t = Node l p r ∧ bdt l var = Some bdt1 ∧ bdt r var = Some bdt2 ∧
1 < v ∧ var p = v )"
apply (induct t rule: bdt_fn.induct)
prefer 5
apply (fastforce split: if_splits option.splits)
apply auto
done

lemma balanced_bdt:
"⋀ p bdt1. ⟦ Dag p low high t; bdt t var = Some bdt1; no ∈ set_of t⟧
⟹ (low no = Null) = (high no = Null)"
proof (induct t)
case Tip
then show ?case by simp
next
case (Node lt a rt)
note NN= this
have bdt1: "bdt (Node lt a rt) var = Some bdt1" by fact
have no_in_t: " no ∈ set_of (Node lt a rt)" by fact
have p_tree: "Dag p low high (Node lt a rt)" by fact
from Node.prems obtain
lt: "Dag (low p) low high lt" and
rt: "Dag (high p) low high rt"
by auto
show ?case
proof (cases lt)
case (Node llt l rlt)
note Nlt=this
show ?thesis
proof (cases rt)
case (Node lrt r rrt)
note Nrt=this
from Nlt Nrt bdt1 obtain lbdt rbdt where
lbdt_def: "bdt lt var = Some lbdt" and
rbdt_def: "bdt rt var = Some rbdt" and
bdt1_def: "bdt1 = Bdt_Node lbdt (var a) rbdt"
by (auto split: if_split_asm option.splits)
from no_in_t show ?thesis
proof (simp, elim disjE)
assume " no = a"
with p_tree Nlt Nrt show ?thesis
by auto
next
assume "no ∈ set_of lt"
with Node.hyps lbdt_def lt show ?thesis
by simp
next
assume "no ∈ set_of rt"
with Node.hyps rbdt_def rt show ?thesis
by simp
qed
next
case Tip
with Nlt bdt1 show ?thesis
by simp
qed
next
case Tip
note ltTip=this
show ?thesis
proof (cases rt)
case Tip
with ltTip bdt1 no_in_t p_tree show ?thesis
by auto
next
case (Node rlt r rrt)
with bdt1 ltTip show ?thesis
by simp
qed
qed
qed

primrec dag_map :: "(ref ⇒ ref) ⇒ dag ⇒ dag"
where
"dag_map f Tip = Tip" |
"dag_map f (Node l a r) = (Node (dag_map f l) (f a) (dag_map f r))"

definition wf_marking :: "dag ⇒ (ref ⇒ bool) ⇒ (ref ⇒ bool) ⇒ bool ⇒ bool"
where
"wf_marking t mark_old mark_new marked =
(case t of Tip ⇒ mark_new = mark_old
| (Node lt p rt) ⇒
(∀ n. n ∉ set_of t ⟶ mark_new n = mark_old n) ∧
(∀ n. n ∈ set_of t ⟶ mark_new n = marked))"

definition dag_in_levellist:: "dag ⇒ (ref list list) ⇒ (ref ⇒ nat) ⇒ bool"
where "dag_in_levellist t levellist var = (t ≠ Tip ⟶
(∀ st. subdag_eq t st ⟶ root st ∈ set (levellist ! (var (root st)))))"

lemma set_of_nn: "⟦ Dag p low high t; n ∈ set_of t⟧ ⟹ n ≠ Null"
apply (induct t)
apply simp
apply auto
done

lemma subnodes_ordered [rule_format]:
"∀p. n ∈ set_of t ⟶ Dag p low high t ⟶ ordered t var ⟶ var n <= var p"
apply (induct t)
apply simp
apply (intro allI)
apply (erule_tac x="low p" in allE)
apply (erule_tac x="high p" in allE)
apply clarsimp
apply (case_tac t1)
apply (case_tac t2)
apply simp
apply fastforce
apply (case_tac t2)
apply fastforce
apply fastforce
done

lemma ordered_set_of:
"⋀ x. ⟦ordered t var; x ∈ set_of t⟧ ⟹ var x <= var (root t)"
apply (induct t)
apply simp
apply simp
apply (elim disjE)
apply simp
apply (case_tac t1)
apply simp
apply (case_tac t2)
apply fastforce
apply fastforce
apply (case_tac t2)
apply simp
apply (case_tac t1)
apply fastforce
apply fastforce
done

lemma dag_setofD: "⋀ p low high n. ⟦ Dag p low high t; n ∈ set_of t ⟧ ⟹
(∃ nt. Dag n low high nt) ∧ (∀ nt. Dag n low high nt ⟶ set_of nt ⊆ set_of t)"
apply (induct t)
apply simp
apply auto
apply fastforce
apply (fastforce dest: Dag_unique)
apply (fastforce dest: Dag_unique)
apply blast
apply blast
done

lemma dag_setof_exD: "⟦Dag p low high t; n ∈ set_of t⟧ ⟹ ∃ nt. Dag n low high nt"
done

lemma dag_setof_subsetD: "⟦Dag p low high t; n ∈ set_of t; Dag n low high nt⟧ ⟹ set_of nt ⊆ set_of t"
done

lemma subdag_parentdag_low: "not <= lt ⟹ not <= (Node lt p rt)"
apply (cases "not = lt")
apply (cases lt)
apply simp
apply (cases rt)
apply simp
done

lemma subdag_parentdag_high: "not <= rt ⟹ not <= (Node lt p rt)"
apply (cases "not = rt")
apply (cases lt)
apply simp
apply (cases rt)
apply simp
done

lemma set_of_subdag: "⋀ p not no.
⟦Dag p low high t; Dag no low high not; no ∈ set_of t⟧ ⟹ not <= t"
proof (induct t)
case Tip
then show ?case by simp
next
case (Node lt po rt)
note rtNode=this
from Node.prems have ppo: "p=po"
by simp
show ?case
proof (cases "no = p")
case True
with ppo Node.prems have "not = (Node lt po rt)"
by (simp add: Dag_unique del: Dag_Ref)
with Node.prems ppo show ?thesis by (simp add: subdag_eq_def)
next
assume " no ≠ p"
with Node.prems have no_in_ltorrt: "no ∈ set_of lt ∨ no ∈ set_of rt"
by simp
show ?thesis
proof (cases "no ∈ set_of lt")
case True
from Node.prems ppo have "Dag (low po) low high lt"
by simp
with Node.prems ppo True have "not <= lt"
apply -
apply (rule Node.hyps)
apply assumption+
done
with Node.prems no_in_ltorrt show ?thesis
apply -
apply (rule subdag_parentdag_low)
apply simp
done
next
assume "no ∉ set_of lt"
with no_in_ltorrt have no_in_rt: "no ∈ set_of rt"
by simp
from Node.prems ppo have "Dag (high po) low high rt"
by simp
with Node.prems ppo no_in_rt have "not <= rt"
apply -
apply (rule Node.hyps)
apply assumption+
done
with Node.prems no_in_rt show ?thesis
apply -
apply (rule subdag_parentdag_high)
apply simp
done
qed
qed
qed

lemma children_ordered: "⟦ordered (Node lt p rt) var⟧ ⟹
ordered lt var ∧ ordered rt var"
proof (cases lt)
case Tip
note ltTip=this
assume  orderedNode: "ordered (Node lt p rt) var"
show ?thesis
proof (cases rt)
case Tip
note rtTip = this
with ltTip show ?thesis
by simp
next
case (Node lrt r rrt)
with orderedNode ltTip show ?thesis
by simp
qed
next
case (Node llt l rlt)
note ltNode=this
assume orderedNode: "ordered (Node lt p rt) var"
show ?thesis
proof (cases rt)
case Tip
note rtTip = this
with orderedNode ltNode show ?thesis by simp
next
case (Node lrt r rrt)
note rtNode = this
with orderedNode ltNode show ?thesis by simp
qed
qed

lemma ordered_subdag: "⟦ordered t var; not <= t⟧ ⟹ ordered not var"
proof (induct t)
case Tip
then show ?thesis by (simp add: less_dag_def le_dag_def)
next
case (Node lt p rt)
show ?case
proof (cases "not = Node lt p rt")
case True
with Node.prems show ?thesis by simp
next
assume notnt: "not ≠ Node lt p rt"
with Node.prems have notstltorrt: "not <= lt ∨ not <= rt"
apply -
apply fastforce
done
from Node.prems have ord_lt: "ordered lt var"
apply -
apply (drule children_ordered)
apply simp
done
from Node.prems have ord_rt: "ordered rt var"
apply -
apply (drule children_ordered)
apply simp
done
show ?thesis
proof (cases "not <= lt")
case True
with ord_lt show ?thesis
apply -
apply (rule Node.hyps)
apply assumption+
done
next
assume "¬ not ≤ lt"
with notstltorrt have notinrt: "not <= rt"
by simp
from Node.hyps have hyprt: "⟦ordered rt var; not ≤ rt⟧ ⟹ ordered not var" by simp
from notinrt ord_rt show ?thesis
apply -
apply (rule hyprt)
apply assumption+
done
qed
qed
qed

lemma subdag_ordered:
"⋀ not no p. ⟦ordered t var; Dag p low high t; Dag no low high not;
no ∈ set_of t⟧ ⟹ ordered not var"
proof (induct t)
case Tip
from Tip.prems show ?case by simp
next
case (Node lt po rt)
note nN=this
show ?case
proof (cases lt)
case Tip
note ltTip=this
show ?thesis
proof (cases rt)
case Tip
from Node.prems have ppo: "p=po"
by simp
from Tip ltTip Node.prems have "no=p"
by simp
with ppo Node.prems have "not=(Node lt po rt)"
by (simp del: Dag_Ref add: Dag_unique)
with Node.prems show ?thesis by simp
next
case (Node lrnot rn rrnot)
from Node.prems ltTip Node have ord_rt: "ordered rt var"
by simp
from Node.prems have ppo: "p=po"
by simp
from Node.prems have ponN: "po ≠ Null"
by auto
with ppo ponN ltTip Node.prems have *: "Dag (high po) low high rt"
by auto
show ?thesis
proof (cases "no=po")
case True
with ppo Node.prems have "not = Node lt po rt"
by (simp del: Dag_Ref add: Dag_unique)
with Node.prems show ?thesis
by simp
next
case False
with Node.prems ltTip have "no ∈ set_of rt"
by simp
with ord_rt * ‹Dag no low high not› show ?thesis
by (rule Node.hyps)
qed
qed
next
case (Node llt l rlt)
note ltNode=this
show ?thesis
proof (cases rt)
case Tip
from Node.prems Tip ltNode have ord_lt: "ordered lt var"
by simp
from Node.prems have ppo: "p=po"
by simp
from Node.prems have ponN: "po ≠ Null"
by auto
with ppo ponN Tip Node.prems ltNode have *: "Dag (low po) low high lt"
by auto
show ?thesis
proof (cases "no=po")
case True
with ppo Node.prems have "not = (Node lt po rt)"
by (simp del: Dag_Ref add: Dag_unique)
with Node.prems show ?thesis by simp
next
case False
with Node.prems Tip have "no ∈ set_of lt"
by simp
with ord_lt * ‹Dag no low high not› show ?thesis
by (rule Node.hyps)
qed
next
case (Node lrt r rrt)
from Node.prems have ppo: "p=po"
by simp
from Node.prems Node ltNode have ord_lt: "ordered lt var"
by simp
from Node.prems Node ltNode have ord_rt: "ordered rt var"
by simp
from Node.prems have ponN: "po ≠ Null"
by auto
with ppo ponN Node Node.prems ltNode have lt_Dag: "Dag (low po) low high lt"
by auto
with ppo ponN Node Node.prems ltNode have rt_Dag: "Dag (high po) low high rt"
by auto
show ?thesis
proof (cases "no = po")
case True
with ppo Node.prems have "not = (Node lt po rt)"
by (simp del: Dag_Ref add: Dag_unique)
with Node.prems show ?thesis by simp
next
assume "no ≠ po"
with Node.prems have no_in_lt_or_rt: "no ∈ set_of lt ∨ no ∈ set_of rt"
by simp
show ?thesis
proof (cases "no ∈ set_of lt")
case True
with ord_lt lt_Dag Node.prems show ?thesis
apply -
apply (rule Node.hyps)
apply assumption+
done
next
assume " no ∉ set_of lt"
with no_in_lt_or_rt have no_in_rt: "no ∈ set_of rt"
by simp
from Node.hyps have hyp2:
"⋀p no not. ⟦ordered rt var; Dag p low high rt; Dag no low high not; no ∈ set_of rt⟧
⟹ ordered not var"
apply -
apply assumption
done
from no_in_rt ord_rt rt_Dag Node.prems show ?thesis
apply -
apply (rule hyp2)
apply assumption+
done
qed
qed
qed
qed
qed

lemma elem_set_of: "⋀ x st. ⟦x ∈ set_of st; set_of st ⊆ set_of t⟧ ⟹ x ∈ set_of t"
by blast

(*procedure Levellist converts a dag with root p in a ref list list (levellist) with nodes of var = i in
levellist ! i.
In order to convert the two datastructures a dag traversal is required using a mark on nodes. m indicates
the value which is assumed for a node to be marked.
(∃ nt. Dag n ⇗σ⇖low ⇗σ⇖high nt ∧
{⇗σ⇖m} = set_of (dag_map ⇗σ⇖mark nt))*)

definition wf_ll :: "dag ⇒ ref list list ⇒ (ref ⇒ nat) ⇒ bool"
where
"wf_ll t levellist var =
((∀p. p ∈ set_of t ⟶ p ∈ set (levellist ! var p)) ∧
(∀k < length levellist. ∀p ∈ set (levellist ! k). p ∈ set_of t ∧ var p = k))"

definition cong_eval :: "bdt ⇒ bdt ⇒ bool" (infix "∼" 60)
where "cong_eval bdt⇩1 bdt⇩2 = (eval bdt⇩1 = eval bdt⇩2)"

lemma cong_eval_sym: "l ∼ r = r ∼ l"

lemma cong_eval_trans: "⟦ l ∼ r; r ∼ t⟧ ⟹ l ∼ t"

lemma cong_eval_child_high: " l ∼ r ⟹ r ∼ (Bdt_Node l v r)"
apply (rule ext)
apply auto
done

lemma cong_eval_child_low: " l ∼ r ⟹ l ∼ (Bdt_Node l v r)"
apply (rule ext)
apply auto
done

definition null_comp :: "(ref ⇒ ref) ⇒ (ref ⇒ ref) ⇒ (ref ⇒ ref)" (infix "∝" 60)
where "null_comp a b = (λ p. (if (b p) = Null then Null else ((a ∘ b) p)))"

lemma null_comp_not_Null [simp]: "h q ≠ Null ⟹ (g ∝ h) q = g (h q)"

lemma id_trans: "(a ∝ id) (b (c p)) = (a ∝ b) (c p)"

definition Nodes :: "nat ⇒ ref list list ⇒ ref set"
where "Nodes i levellist = (⋃k∈{k. k < i} . set (levellist ! k))"

inductive_set Dags :: "ref set ⇒ (ref ⇒ ref) ⇒ (ref ⇒ ref) ⇒ dag set"
for "nodes" "low" "high"
where
DagsI: "⟦ set_of t ⊆  nodes; Dag p low high t; t ≠ Tip⟧
⟹ t ∈ Dags nodes low high"

lemma empty_Dags [simp]: "Dags {} low high = {}"
apply rule
apply rule
apply (erule Dags.cases)
apply (case_tac t)
apply simp
apply simp
apply rule
done

definition isLeaf_pt :: "ref ⇒ (ref ⇒ ref) ⇒ (ref ⇒ ref) ⇒ bool"
where "isLeaf_pt p low high = (low p = Null ∧ high p = Null)"

definition repNodes_eq :: "ref ⇒ ref ⇒ (ref ⇒ ref) ⇒ (ref ⇒ ref) ⇒ (ref ⇒ ref) ⇒ bool"
where
"repNodes_eq p q low high rep ==
(rep ∝ high) p = (rep ∝ high) q ∧ (rep ∝ low) p = (rep ∝ low) q"

definition isomorphic_dags_eq :: "dag ⇒ dag ⇒ (ref ⇒ nat) ⇒ bool"
where
"isomorphic_dags_eq st⇩1 st⇩2 var =
(∀bdt⇩1 bdt⇩2. (bdt st⇩1 var = Some bdt⇩1 ∧ bdt st⇩2 var = Some bdt⇩2 ∧ (bdt⇩1 = bdt⇩2))
⟶ st⇩1 = st⇩2)"

lemma isomorphic_dags_eq_sym: "isomorphic_dags_eq st⇩1 st⇩2 var = isomorphic_dags_eq st⇩2 st⇩1  var"

(*consts subdags_shared :: "dag ⇒ dag ⇒ (ref ⇒ nat) ⇒ bool"
defs subdags_shared_def : "subdags_shared t1 t2 var == ∀ st1 st2. (st1 <= t1 ∧ st2 <= t2) ⟶ shared_prop st1 st2 var"

consts shared :: " dag ⇒ dag ⇒ (ref ⇒ nat) ⇒ bool"
defs shared_def: "shared t1 t2 var == subdags_shared t1 t1 var ∧ subdags_shared t2 t2 var ∧ subdags_shared t1 t2 var"*)

definition shared :: "dag ⇒ (ref ⇒ nat) ⇒ bool"
where "shared t var = (∀st⇩1 st⇩2. (st⇩1 <= t ∧ st⇩2 <= t) ⟶ isomorphic_dags_eq st⇩1 st⇩2 var)"

(* shared returns True if the Dag has no different subdags which represent the same
bdts.
Note: The two subdags can have different references and code the same bdt nevertheless!
consts shared :: "dag ⇒ (ref ⇒ nat) ⇒ bool"
defs shared_def: "shared t bdtvar ≡ ∀ st1 st2. (subdag t st1 ∧ subdag t st2 ∧
(bdt st1 bdtvar = bdt st2 bdtvar ⟶ st1 = st2))"

consts shared_lower_levels :: "dag ⇒ nat ⇒ (ref ⇒ nat) ⇒ bool"
defs shared_lower_levels_def : "shared_lower_levels t i bdtvar == ∀ st1 st2. (st1 < t ∧ st2 < t ∧ bdtvar (root st1) < i ∧ bdtvar (root st2) < i ∧
(bdt st1 bdtvar = bdt st2 bdtvar ⟶ st1 = st2))"
*)

fun reduced :: "dag ⇒ bool" where
"reduced Tip = True"
| "reduced (Node Tip v Tip) = True"
| "reduced (Node l v r) = (l ≠ r ∧ reduced l ∧ reduced r)"

primrec reduced_bdt :: "bdt ⇒ bool"
where
"reduced_bdt Zero = True"
| "reduced_bdt One = True"
| "reduced_bdt (Bdt_Node lbdt v rbdt) =
(if lbdt = rbdt then False
else (reduced_bdt lbdt ∧ reduced_bdt rbdt))"

lemma replicate_elem: "i < n ==>  (replicate n x !i) = x"
apply (induct n)
apply simp
apply (cases i)
apply auto
done

lemma no_in_one_ll:
"⟦wf_ll pret levellista var; i<length levellista; j < length levellista;
no ∈ set (levellista ! i); i≠j⟧
⟹ no ∉ set (levellista ! j) "
apply (unfold wf_ll_def)
apply (erule conjE)
apply (rotate_tac 5)
apply (frule_tac x = i and ?R= "no ∈ set_of pret ∧ var no = i" in allE)
apply (erule impE)
apply simp
apply (rotate_tac 6)
apply (erule_tac x=no in ballE)
apply assumption
apply simp
apply (cases "no ∉ set (levellista ! j)")
apply assumption
apply (erule_tac x=j in allE)
apply (erule impE)
apply assumption
apply (rotate_tac 7)
apply (erule_tac x=no in ballE)
prefer 2
apply assumption
apply (elim conjE)
apply (thin_tac "∀q. q ∈ set_of pret ⟶ q ∈ set (levellista ! var q)")
apply fastforce
done

lemma nodes_in_wf_ll:
"⟦wf_ll pret levellista var; i < length levellista;  no ∈ set (levellista ! i)⟧
⟹ var no = i ∧ no ∈ set_of pret"
done

lemma subelem_set_of_low:
"⋀ p. ⟦ x ∈ set_of t; x ≠ Null; low x ≠ Null; Dag p low high t ⟧
⟹ (low x) ∈ set_of t"
proof (induct t)
case Tip
then show ?case by simp
next
case (Node lt po rt)
note tNode=this
then have ppo: "p=po" by simp
show ?case
proof (cases "x=p")
case True
with Node.prems have lxrootlt: "low x = root lt"
proof (cases lt)
case Tip
with True Node.prems show ?thesis
by auto
next
case (Node llt l rlt)
with Node.prems True show ?thesis
by auto
qed
with True Node.prems have "low x ∈ set_of (Node lt p rt)"
proof (cases lt)
case Tip
with lxrootlt Node.prems show ?thesis
by simp
next
case (Node llt l rlt)
with lxrootlt Node.prems show ?thesis
by simp
qed
with ppo show ?thesis
by simp
next
assume xnp: " x ≠ p"
with Node.prems have "x ∈ set_of lt ∨ x ∈ set_of rt"
by simp
show ?thesis
proof (cases "x ∈ set_of lt")
case True
note xinlt=this
from Node.prems have "Dag (low p) low high lt"
by fastforce
with Node.prems True have "low x ∈ set_of lt"
apply -
apply (rule Node.hyps)
apply assumption+
done
with Node.prems show ?thesis
by auto
next
assume xnotinlt: " x ∉ set_of lt"
with xnp Node.prems have xinrt: "x ∈ set_of rt"
by simp
from Node.prems have "Dag (high p) low high rt"
by fastforce
with Node.prems xinrt have "low x ∈ set_of rt"
apply -
apply (rule Node.hyps)
apply assumption+
done
with Node.prems show ?thesis
by auto
qed
qed
qed

lemma subelem_set_of_high:
"⋀ p. ⟦ x ∈ set_of t; x ≠ Null; high x ≠ Null; Dag p low high t ⟧
⟹ (high x) ∈ set_of t"
proof (induct t)
case Tip
then show ?case by simp
next
case (Node lt po rt)
note tNode=this
then have ppo: "p=po" by simp
show ?case
proof (cases "x=p")
case True
with Node.prems have lxrootlt: "high x = root rt"
proof (cases rt)
case Tip
with True Node.prems show ?thesis
by auto
next
case (Node lrt l rrt)
with Node.prems True show ?thesis
by auto
qed
with True Node.prems have "high x ∈ set_of (Node lt p rt)"
proof (cases rt)
case Tip
with lxrootlt Node.prems show ?thesis
by simp
next
case (Node lrt l rrt)
with lxrootlt Node.prems show ?thesis
by simp
qed
with ppo show ?thesis
by simp
next
assume xnp: " x ≠ p"
with Node.prems have "x ∈ set_of lt ∨ x ∈ set_of rt"
by simp
show ?thesis
proof (cases "x ∈ set_of lt")
case True
note xinlt=this
from Node.prems have "Dag (low p) low high lt"
by fastforce
with Node.prems True have "high x ∈ set_of lt"
apply -
apply (rule Node.hyps)
apply assumption+
done
with Node.prems show ?thesis
by auto
next
assume xnotinlt: " x ∉ set_of lt"
with xnp Node.prems have xinrt: "x ∈ set_of rt"
by simp
from Node.prems have "Dag (high p) low high rt"
by fastforce
with Node.prems xinrt have "high x ∈ set_of rt"
apply -
apply (rule Node.hyps)
apply assumption+
done
with Node.prems show ?thesis
by auto
qed
qed
qed

lemma set_split: "{k. k<(Suc n)} = {k. k<n} ∪ {n}"
apply auto
done

lemma Nodes_levellist_subset_t:
"⟦wf_ll t levellist var; i<= length levellist⟧ ⟹ Nodes i levellist ⊆ set_of t"
proof (induct i)
case 0
show ?case by (simp add: Nodes_def)
next
case (Suc n)
from Suc.prems Suc.hyps have Nodesn_in_t: "Nodes n levellist ⊆ set_of t"
by simp
from Suc.prems have "∀ x ∈ set (levellist ! n). x ∈ set_of t"
apply -
apply (rule ballI)
apply (erule conjE)
apply (thin_tac " ∀q. q ∈ set_of t ⟶ q ∈ set (levellist ! var q)")
apply (erule_tac x=n in allE)
apply (erule impE)
apply simp
apply fastforce
done
with Suc.prems have "set (levellist ! n) ⊆ set_of t"
apply blast
done
with Suc.prems Nodesn_in_t show ?case
done
qed

lemma bdt_child:
"⟦ bdt (Node (Node llt l rlt) p (Node lrt r rrt)) var = Some bdt1⟧
⟹ ∃ lbdt rbdt.  bdt (Node llt l rlt) var = Some lbdt ∧
bdt (Node lrt r rrt) var = Some rbdt"
by (simp split: option.splits)

lemma subbdt_ex_dag_def:
"⋀ bdt1 p. ⟦Dag p low high t; bdt t var = Some bdt1; Dag no low high not;
no ∈ set_of t⟧ ⟹ ∃ bdt2.  bdt not var = Some bdt2"
proof (induct t)
case Tip
then show ?case by simp
next
case (Node lt po rt)
note pNode=this
with Node.prems have p_po: "p=po" by simp
show ?case
proof (cases "no = po")
case True
note no_eq_po=this
from p_po Node.prems no_eq_po have "not = (Node lt po rt)" by (simp add: Dag_unique del: Dag_Ref)
with Node.prems have "bdt not var = Some bdt1" by (simp add: le_dag_def)
then show ?thesis by simp
next
assume "no ≠ po"
with Node.prems have no_in_lt_or_rt: "no ∈ set_of lt ∨ no ∈ set_of rt" by simp
show ?thesis
proof (cases "no ∈ set_of lt")
case True
note no_in_lt=this
from Node.prems p_po have lt_dag: "Dag (low po) low high lt" by simp
from Node.prems have lbdt_def: "∃ lbdt. bdt lt var = Some lbdt"
proof (cases lt)
case Tip
with Node.prems no_in_lt show ?thesis by (simp add: le_dag_def)
next
case (Node llt l rlt)
note lNode=this
show ?thesis
proof (cases rt)
case Tip
note rNode=this
with lNode Node.prems show ?thesis by simp
next
case (Node lrt r rrt)
note rNode=this
with lNode Node.prems show ?thesis by (simp split: option.splits)
qed
qed
then obtain lbdt where "bdt lt var = Some lbdt"..
with Node.prems lt_dag no_in_lt show ?thesis
apply -
apply (rule Node.hyps)
apply assumption+
done
next
assume "no ∉ set_of lt"
with no_in_lt_or_rt have no_in_rt: "no ∈ set_of rt" by simp
from Node.prems p_po have rt_dag: "Dag (high po) low high rt" by simp
from Node.hyps have hyp2: "⋀ rbdt. ⟦Dag (high po) low high rt; bdt rt var = Some rbdt; Dag no low high not; no ∈ set_of rt⟧ ⟹ ∃bdt2. bdt not var = Some bdt2"
by simp
from Node.prems have lbdt_def: "∃ rbdt. bdt rt var = Some rbdt"
proof (cases rt)
case Tip
with Node.prems no_in_rt show ?thesis by (simp add: le_dag_def)
next
case (Node lrt l rrt)
note rNode=this
show ?thesis
proof (cases lt)
case Tip
note lTip=this
with rNode Node.prems show ?thesis by simp
next
case (Node llt r rlt)
note lNode=this
with rNode Node.prems show ?thesis by (simp split: option.splits)
qed
qed
then obtain rbdt where "bdt rt var = Some rbdt"..
with Node.prems rt_dag no_in_rt show ?thesis
apply -
apply (rule hyp2)
apply assumption+
done
qed
qed
qed

lemma subbdt_ex:
"⋀ bdt1. ⟦ (Node lst stp rst) <= t; bdt t var = Some bdt1⟧
⟹ ∃ bdt2.  bdt (Node lst stp rst) var = Some bdt2"
proof (induct t)
case Tip
then show ?case by (simp add: le_dag_def)
next
case (Node lt p rt)
note pNode=this
show ?case
proof (cases "Node lst stp rst = Node lt p rt")
case True
with Node.prems show ?thesis by simp
next
assume " Node lst stp rst ≠ Node lt p rt"
with Node.prems have "Node lst stp rst < Node lt p rt" apply (simp add: le_dag_def) apply auto done
then have in_ltrt: "Node lst stp rst <= lt ∨ Node lst stp rst <= rt"
show ?thesis
proof (cases "Node lst stp rst <= lt")
case True
note in_lt=this
from Node.prems have lbdt_def: "∃ lbdt. bdt lt var = Some lbdt"
proof (cases lt)
case Tip
with Node.prems in_lt show ?thesis by (simp add: le_dag_def)
next
case (Node llt l rlt)
note lNode=this
show ?thesis
proof (cases rt)
case Tip
note rNode=this
with lNode Node.prems show ?thesis by simp
next
case (Node lrt r rrt)
note rNode=this
with lNode Node.prems show ?thesis by (simp split: option.splits)
qed
qed
then obtain lbdt where "bdt lt var = Some lbdt"..
with Node.prems in_lt show ?thesis
apply -
apply (rule Node.hyps)
apply assumption+
done
next
assume " ¬ Node lst stp rst ≤ lt"
with in_ltrt have in_rt: "Node lst stp rst <= rt" by simp
from Node.hyps have hyp2: "⋀ rbdt. ⟦Node lst stp rst <= rt; bdt rt var = Some rbdt⟧ ⟹ ∃bdt2. bdt (Node lst stp rst) var = Some bdt2"
by simp
from Node.prems have rbdt_def: "∃ rbdt. bdt rt var = Some rbdt"
proof (cases rt)
case Tip
with Node.prems in_rt show ?thesis by (simp add: le_dag_def)
next
case (Node lrt l rrt)
note rNode=this
show ?thesis
proof (cases lt)
case Tip
note lNode=this
with rNode Node.prems show ?thesis by simp
next
case (Node lrt r rrt)
note lNode=this
with rNode Node.prems show ?thesis by (simp split: option.splits)
qed
qed
then obtain rbdt where "bdt rt var = Some rbdt"..
with Node.prems in_rt show ?thesis
apply -
apply (rule hyp2)
apply assumption+
done
qed
qed
qed

lemma var_ordered_children:
"⋀ p. ⟦ Dag p low high t; ordered t var; no ∈ set_of t;
low no ≠ Null; high no ≠ Null⟧
⟹ var (low no) < var no ∧ var (high no) < var no"
proof (induct t)
case Tip
then show ?case by simp
next
case (Node lt po rt)
then have ppo: "p=po" by simp
show ?case
proof (cases "no = po")
case True
note no_po=this
from Node.prems have "var (low po) < var po ∧ var (high po) < var po"
proof (cases lt)
case Tip
note ltTip=this
with Node.prems no_po ppo show ?thesis by simp
next
case (Node llt l rlt)
note lNode=this
show ?thesis
proof (cases rt)
case Tip
note rTip=this
with Node.prems no_po ppo show ?thesis by simp
next
case (Node lrt r rrt)
note rNode=this
with Node.prems ppo no_po lNode  show ?thesis by (simp del: Dag_Ref)
qed
qed
with no_po show ?thesis by simp
next
assume " no ≠ po"
with Node.prems have no_in_ltrt: "no ∈ set_of lt ∨ no ∈ set_of rt"
by simp
show ?thesis
proof (cases "no ∈ set_of lt")
case True
note no_in_lt=this
from Node.prems ppo have lt_dag: "Dag (low po) low high lt"
by simp
from Node.prems have ord_lt: "ordered lt var"
apply -
apply (drule children_ordered)
apply simp
done
from no_in_lt lt_dag ord_lt Node.prems show ?thesis
apply -
apply (rule Node.hyps)
apply assumption+
done
next
assume " no ∉ set_of lt"
with no_in_ltrt have no_in_rt: "no ∈ set_of rt" by simp
from Node.prems ppo have rt_dag: "Dag (high po) low high rt" by simp
from Node.hyps have hyp2: " ⟦Dag (high po) low high rt; ordered rt var; no ∈ set_of rt; low no ≠ Null; high no ≠ Null⟧
⟹ var (low no) < var no ∧ var (high no) < var no"
by simp
from Node.prems have ord_rt: "ordered rt var"
apply -
apply (drule children_ordered)
apply simp
done
from rt_dag ord_rt no_in_rt Node.prems show ?thesis
apply -
apply (rule hyp2)
apply assumption+
done
qed
qed
qed

lemma nort_null_comp:
assumes pret_dag: "Dag p low high pret" and
prebdt_pret: "bdt pret var = Some prebdt" and
nort_dag: "Dag (repc no) (repb ∝ low) (repb ∝ high) nort" and
ord_pret: "ordered pret var" and
wf_llb: "wf_ll pret levellistb var" and
nbsll: "nb < length levellistb" and
repbc_nc: "∀ nt. nt ∉ set (levellistb ! nb) ⟶ repb nt = repc nt" and
xsnb_in_pret: "∀ x ∈ set_of nort. var x < nb ∧ x ∈ set_of pret"
shows "∀ x ∈ set_of nort. ((repc ∝ low) x = (repb ∝ low) x ∧
(repc ∝ high) x = (repb ∝ high) x)"
proof (rule ballI)
fix x
assume x_in_nort: "x ∈ set_of nort"
with nort_dag have xnN: "x ≠ Null"
apply -
apply (rule set_of_nn [rule_format])
apply auto
done
from x_in_nort xsnb_in_pret have xsnb: "var x <nb"
by simp
from x_in_nort xsnb_in_pret have x_in_pret: "x ∈ set_of pret"
by blast
show " (repc ∝ low) x = (repb ∝ low) x ∧ (repc ∝ high) x = (repb ∝ high) x"
proof (cases "(low x) ≠ Null")
case True
with pret_dag prebdt_pret x_in_pret have highnN: "(high x) ≠ Null"
apply -
apply (drule balanced_bdt)
apply assumption+
apply simp
done
from x_in_pret ord_pret highnN True have children_var_smaller: "var (low x) < var x ∧ var (high x) < var x"
apply -
apply (rule var_ordered_children)
apply (rule pret_dag)
apply (rule ord_pret)
apply (rule x_in_pret)
apply (rule True)
apply (rule highnN)
done
with xsnb have lowxsnb: "var (low x) < nb"
by arith
from children_var_smaller xsnb have highxsnb: "var (high x) < nb"
by arith
from x_in_pret xnN True pret_dag have lowxinpret: "(low x) ∈ set_of pret"
apply -
apply (drule subelem_set_of_low)
apply assumption
apply (thin_tac "x ≠ Null")
apply assumption+
done
with wf_llb have "low x ∈ set (levellistb ! (var (low x)))"
with wf_llb nbsll lowxsnb have "low x ∉ set (levellistb ! nb)"
apply -
apply (rule_tac ?i="(var (low x))" and ?j=nb in no_in_one_ll)
apply auto
done
with repbc_nc have repclow: "repc (low x) = repb (low x)"
by auto
from x_in_pret xnN highnN pret_dag have highxinpret: "(high x) ∈ set_of pret"
apply -
apply (drule subelem_set_of_high)
apply assumption
apply (thin_tac "x ≠ Null")
apply assumption+
done
with wf_llb have "high x ∈ set (levellistb ! (var (high x)))"
with wf_llb nbsll highxsnb have "high x ∉ set (levellistb ! nb)"
apply -
apply (rule_tac ?i="(var (high x))" and ?j=nb in no_in_one_ll)
apply auto
done
with repbc_nc have repchigh: "repc (high x) = repb (high x)"
by auto
with repclow show ?thesis
next
assume " ¬ low x ≠ Null"
then have lowxNull: "low x = Null" by simp
with pret_dag x_in_pret prebdt_pret have highxNull: "high x =Null"
apply -
apply (drule balanced_bdt)
apply simp
apply simp
apply simp
done
from lowxNull have repclowNull: "(repc ∝ low) x = Null"
from lowxNull have repblowNull: "(repb ∝ low) x = Null"
with repclowNull have lowxrepbc: "(repc ∝ low) x = (repb ∝ low) x"
by simp
from highxNull have repchighNull: "(repc ∝ high) x = Null"
from highxNull have "(repb ∝ high) x = Null"
with repchighNull have highxrepbc: "(repc ∝ high) x = (repb ∝ high) x"
by simp
with lowxrepbc show ?thesis
by simp
qed
qed

lemma wf_ll_Nodes_pret:
"⟦wf_ll pret levellista var; nb < length levellista; x ∈ Nodes nb levellista⟧
⟹ x ∈ set_of pret ∧ var x < nb"
apply (erule conjE)
apply (thin_tac " ∀q. q ∈ set_of pret ⟶ q ∈ set (levellista ! var q)")
apply (erule exE)
apply (elim conjE)
apply (erule_tac x=xa in allE)
apply (erule impE)
apply arith
apply (erule_tac x=x in ballE)
apply auto
done

lemma bdt_Some_var1_One:
"⋀ x. ⟦ bdt t var = Some x; var (root t) = 1⟧
⟹ x = One ∧ t = (Node Tip (root t) Tip)"
proof (induct t)
case Tip
then show  ?case by simp
next
case (Node lt p rt)
note tNode = this
show ?case
proof (cases lt)
case Tip
note ltTip=this
show ?thesis
proof (cases rt)
case Tip
note rtTip = this
with ltTip Node.prems show ?thesis by auto
next
case (Node lrt r rrt)
note rtNode=this
with Node.prems ltTip show ?thesis by auto
qed
next
case (Node llt l rlt)
note ltNode=this
show ?thesis
proof (cases rt)
case Tip
with ltNode Node.prems show ?thesis by auto
next
case (Node lrt r rrt)
note rtNode=this
with ltNode Node.prems show ?thesis by auto
qed
qed
qed

lemma bdt_Some_var0_Zero:
"⋀ x. ⟦ bdt t var = Some x; var (root t) = 0⟧
⟹ x = Zero ∧ t = (Node Tip (root t) Tip)"
proof (induct t)
case Tip
then show  ?case by simp
next
case (Node lt p rt)
note tNode = this
show ?case
proof (cases lt)
case Tip
note ltTip=this
show ?thesis
proof (cases rt)
case Tip
note rtTip = this
with ltTip Node.prems show ?thesis by auto
next
case (Node lrt r rrt)
note rtNode=this
with Node.prems ltTip show ?thesis by auto
qed
next
case (Node llt l rlt)
note ltNode=this
show ?thesis
proof (cases rt)
case Tip
with ltNode Node.prems show ?thesis by auto
next
case (Node lrt r rrt)
note rtNode=this
with ltNode Node.prems show ?thesis by auto
qed
qed
qed

lemma reduced_children_parent:
"⟦ reduced l; l= (Node llt lp rlt); reduced r; r=(Node lrt rp rrt);
lp ≠ rp ⟧
⟹ reduced (Node l p r)"
by simp

(*Die allgemeine Form mit i <=j ⟹ Nodes i levellista ⊆ Nodes j levellista wäre schöner, aber wie beweist man das? *)
lemma Nodes_subset: "Nodes i levellista ⊆ Nodes (Suc i) levellista"
done

lemma Nodes_levellist:
"⟦ wf_ll pret levellista var; nb < length levellista; p ∈ Nodes nb levellista⟧
⟹ p ∉ set (levellista ! nb)"
apply (erule exE)
apply (rule_tac i=x and j=nb in no_in_one_ll)
apply auto
done

lemma Nodes_var_pret:
"⟦wf_ll pret levellista var; nb < length levellista; p ∈ Nodes nb levellista⟧
⟹ var p < nb ∧ p ∈ set_of pret"
apply (erule conjE)
apply (thin_tac "∀q. q ∈ set_of pret ⟶ q ∈ set (levellista ! var q)")
apply (erule exE)
apply (erule_tac x=x in allE)
apply (erule impE)
apply arith
apply (erule_tac x=p in ballE)
apply arith
apply simp
done

lemma Dags_root_in_Nodes:
assumes t_in_DagsSucnb: "t ∈ Dags (Nodes (Suc nb) levellista) low high"
shows "∃ p . Dag p low high t  ∧ p ∈ Nodes (Suc nb) levellista"
proof -
from t_in_DagsSucnb obtain p where t_dag: "Dag p low high t" and t_subset_Nodes: "set_of t ⊆ Nodes (Suc nb) levellista" and t_nTip: "t≠ Tip"
by (fastforce elim: Dags.cases)
from t_dag t_nTip have "p≠Null" by (cases t) auto
with t_subset_Nodes t_dag have "p ∈ Nodes (Suc nb) levellista"
by (cases t) auto
with t_dag show ?thesis
by auto
qed

lemma subdag_dag:
"⋀ p. ⟦Dag p low high t; st <= t⟧ ⟹ ∃ stp. Dag stp low high st"
proof (induct t)
case Tip
then show ?case
next
case (Node lt po rt)
note t_Node=this
with Node.prems have p_po: "p=po"
by simp
show ?case
proof (cases "st = Node lt po rt")
case True
note st_t=this
with Node.prems show ?thesis
by auto
next
assume st_nt: "st ≠ Node lt po rt"
with Node.prems p_po have st_subdag_lt_rt: "st<=lt ∨ st <=rt"
from Node.prems p_po obtain lp rp where lt_dag: "Dag lp low high lt" and rt_dag: "Dag rp low high rt"
by auto
show ?thesis
proof (cases "st<=lt")
case True
note st_lt=this
with lt_dag show ?thesis
apply-
apply (rule Node.hyps)
apply auto
done
next
assume "¬ st ≤ lt"
with st_subdag_lt_rt have st_rt: "st <= rt"
by simp
from Node.hyps have rhyp: "⟦Dag rp low high rt; st ≤ rt⟧ ⟹ ∃stp. Dag stp low high st"
by simp
from st_rt rt_dag show ?thesis
apply -
apply (rule rhyp)
apply auto
done
qed
qed
qed

lemma Dags_subdags:
assumes t_in_Dags: "t ∈ Dags nodes low high" and
st_t: "st <= t" and
st_nTip: "st ≠ Tip"
shows "st ∈ Dags nodes low high"
proof -
from t_in_Dags obtain p where t_dag: "Dag p low high t" and t_subset_Nodes: "set_of t ⊆ nodes" and t_nTip: "t≠ Tip"
by (fastforce elim: Dags.cases)
from st_t have "set_of st ⊆ set_of t"
with t_subset_Nodes have st_subset_fnctNodes: "set_of st ⊆ nodes"
by blast
from st_t t_dag obtain stp where "Dag stp low high st"
apply -
apply (drule subdag_dag)
apply auto
done
with st_subset_fnctNodes st_nTip show ?thesis
apply -
apply (rule DagsI)
apply auto
done
qed

lemma Dags_Nodes_cases:
assumes P_sym: "⋀ t1 t2. P t1 t2 var = P t2 t1 var" and
dags_in_lower_levels:
"⋀ t1 t2. ⟦t1 ∈ Dags (fnct (Nodes n levellista)) low high;
t2  ∈ Dags (fnct (Nodes n levellista)) low high⟧
⟹ P t1 t2 var" and
dags_in_mixed_levels:
"⋀ t1 t2. ⟦t1 ∈ Dags (fnct (Nodes n levellista)) low high;
t2  ∈ Dags (fnct (Nodes (Suc n) levellista)) low high;
t2 ∉  Dags (fnct (Nodes n levellista)) low high⟧
⟹ P t1 t2 var" and
dags_in_high_level:
"⋀ t1 t2. ⟦t1 ∈ Dags (fnct (Nodes (Suc n) levellista)) low high;
t1 ∉  Dags (fnct (Nodes n levellista)) low high;
t2 ∈ Dags (fnct (Nodes (Suc n) levellista)) low high;
t2 ∉  Dags (fnct (Nodes n levellista)) low high⟧
⟹ P t1 t2 var"
shows "∀ t1 t2.  t1 ∈ Dags (fnct (Nodes (Suc n) levellista)) low high ∧
t2 ∈ Dags (fnct (Nodes (Suc n) levellista)) low high
⟶ P t1 t2 var"
proof (intro allI impI , elim conjE)
fix t1 t2
assume t1_in_higher_levels: "t1 ∈ Dags (fnct  Nodes (Suc n) levellista) low high"
assume t2_in_higher_levels: "t2 ∈ Dags (fnct  Nodes (Suc n) levellista) low high"
show  "P t1 t2 var"
proof (cases "t1 ∈ Dags (fnct  Nodes n levellista) low high")
case True
note t1_in_ll = this
show ?thesis
proof (cases "t2 ∈ Dags (fnct  Nodes n levellista) low high")
case True
note t2_in_ll=this
with t1_in_ll dags_in_lower_levels show ?thesis
by simp
next
assume t2_notin_ll: "t2 ∉ Dags (fnct  Nodes n levellista) low high"
with t1_in_ll t2_in_higher_levels dags_in_mixed_levels show ?thesis
by simp
qed
next
assume t1_notin_ll: "t1 ∉ Dags (fnct  Nodes n levellista) low high"
show ?thesis
proof (cases "t2 ∈ Dags (fnct  Nodes n levellista) low high")
case True
note t2_in_ll=this
with dags_in_mixed_levels t1_in_higher_levels t1_notin_ll P_sym show ?thesis
by auto
next
assume t2_notin_ll: "t2 ∉ Dags (fnct  Nodes n levellista) low high"
with t1_notin_ll t1_in_higher_levels t2_in_higher_levels dags_in_high_level show ?thesis
by simp
qed
qed
qed

lemma Null_notin_Nodes: "⟦Dag p low high t; nb <= length levellista; wf_ll t levellista var⟧ ⟹ Null ∉ Nodes nb levellista"
apply (simp add: Nodes_def wf_ll_def del: Dag_Ref)
apply (rule allI)
apply (rule impI)
apply (elim conjE)
apply (thin_tac "∀q. P q" for P)
apply (erule_tac x=x in allE)
apply (erule impE)
apply simp
apply (erule_tac x=Null in ballE)
apply (erule conjE)
apply (drule set_of_nn [rule_format])
apply auto
done

lemma Nodes_in_pret: "⟦wf_ll t levellista var; nb <= length levellista⟧ ⟹ Nodes nb levellista ⊆ set_of t"
apply -
apply rule
apply (erule exE)
apply (elim conjE)
apply (thin_tac "∀q. q ∈ set_of t ⟶ q ∈ set (levellista ! var q)")
apply (erule_tac x=xa in allE)
apply (erule impE)
apply simp
apply (erule_tac x=x in ballE)
apply auto
done

lemma restrict_root_Node:
"⟦t ∈ Dags (repc Nodes (Suc nb) levellista) (repc ∝ low) (repc ∝ high); t ∉  Dags (repc Nodes nb levellista) (repc ∝ low) (repc ∝ high);
ordered t var; ∀ no ∈ Nodes (Suc nb) levellista. var (repc no) <= var no ∧ repc (repc no) = repc no; wf_ll pret levellista var; nb < length levellista;repc Nodes (Suc nb) levellista ⊆ Nodes (Suc nb) levellista⟧
⟹ ∃ q. Dag (repc q) (repc ∝ low) (repc ∝ high) t ∧ q ∈ set (levellista ! nb)"
proof (elim Dags.cases)
fix p and ta :: "dag"
assume t_notin_DagsNodesnb: "t ∉ Dags (repc  Nodes nb levellista) (repc ∝ low) (repc ∝ high)"
assume t_ta: "t = ta"
assume ta_in_repc_NodesSucnb: "set_of ta ⊆ repc  Nodes (Suc nb) levellista"
assume ta_dag: "Dag p (repc ∝ low) (repc ∝ high) ta"
assume ta_nTip: "ta ≠ Tip"
assume ord_t: "ordered t var"
assume varrep_prop: "∀ no ∈ Nodes (Suc nb) levellista. var (repc no) <= var no ∧ repc (repc no) = repc no"
assume wf_lla: "wf_ll pret levellista var"
assume nbslla: "nb < length levellista"
assume repcNodes_in_Nodes: "repc Nodes (Suc nb) levellista ⊆ Nodes (Suc nb) levellista"
from ta_nTip ta_dag have p_nNull: "p≠ Null"
by auto
with ta_nTip ta_dag obtain lt rt where ta_Node: " ta = Node lt p rt"
by auto
with ta_nTip ta_dag have p_in_ta: "p ∈ set_of ta"
by auto
with ta_in_repc_NodesSucnb have p_in_repcNodes_Sucnb: "p ∈ repc Nodes (Suc nb) levellista"
by auto
show ?thesis
proof (cases "p ∈ repc (set (levellista ! nb))")
case True
then obtain q where
p_repca: "p=repc q" and
a_in_llanb: "q ∈ set (levellista ! nb)"
by auto
with ta_dag t_ta show ?thesis
apply -
apply (rule_tac x=q in exI)
apply simp
done
next
assume p_notin_repc_llanb: "p ∉ repc  set (levellista ! nb)"
with p_in_repcNodes_Sucnb have p_in_repc_Nodesnb: "p ∈ repc Nodes nb levellista"
apply -
apply (erule imageE)
apply rule
apply (erule exE conjE)
apply (case_tac "xa=nb")
apply simp
apply (rule_tac x=xa in exI)
apply auto
done
have "t ∈ Dags (repc Nodes nb levellista) (repc ∝ low) (repc ∝ high)"
proof -
have "set_of t ⊆ repc Nodes nb levellista"
proof (rule)
fix x :: ref
assume x_in_t: "x ∈ set_of t"
with ord_t have "var x <= var (root t)"
apply -
apply (rule ordered_set_of)
apply auto
done
with t_ta ta_Node have varx_varp: "var x <= var p"
by auto
from p_in_repc_Nodesnb obtain k where ksnb: "k < nb" and p_in_repc_llak:  "p ∈ repc (set (levellista ! k))"
by (auto simp add: Nodes_def ImageE)
then obtain q where p_repcq: "p=repc q" and q_in_llak: "q ∈ set (levellista ! k)"
by auto
from q_in_llak wf_lla nbslla ksnb have varqk: "var q = k"
have Nodesnb_in_NodesSucnb: "Nodes nb levellista ⊆ Nodes (Suc nb) levellista"
by (rule Nodes_subset)
from q_in_llak ksnb have "q ∈ Nodes nb levellista"
with varrep_prop Nodesnb_in_NodesSucnb have "var (repc q) <= var q"
by auto
with varqk ksnb p_repcq have "var p < nb"
by auto
with varx_varp have varx_snb: "var x < nb"
by auto
from x_in_t t_ta ta_in_repc_NodesSucnb obtain a where
x_repca: "x= repc a" and
a_in_NodesSucnb: "a ∈ Nodes (Suc nb) levellista"
by auto
with varrep_prop have rx_x: "repc x = x"
by auto
have "x ∈ set_of pret"
proof -
from wf_lla nbslla have "Nodes (Suc nb) levellista ⊆ set_of pret"
apply -
apply (rule Nodes_in_pret)
apply auto
done
with x_in_t t_ta ta_in_repc_NodesSucnb repcNodes_in_Nodes show ?thesis
by auto
qed
with wf_lla have "x ∈ set (levellista ! (var x))"
with varx_snb have "x ∈ Nodes nb levellista"
with rx_x show "x ∈ repc Nodes nb levellista"
apply -
apply rule
apply (subgoal_tac "x=repc x")
apply auto
done
qed
with ta_nTip ta_dag t_ta show ?thesis
apply -
apply (rule DagsI)
apply auto
done
qed
with t_notin_DagsNodesnb show ?thesis
by auto
qed
qed

lemma same_bdt_var: "⟦bdt (Node lt1 p1 rt1) var = Some bdt1; bdt (Node lt2 p2 rt2) var = Some bdt1⟧
⟹ var p1 = var p2"
proof (induct bdt1)
case Zero
then obtain var_p1: "var p1 = 0" and var_p2: "var p2 = 0"
by simp
then show ?case
by simp
next
case One
then obtain var_p1: "var p1 = 1" and var_p2: "var p2 = 1"
by simp
then show ?case
by simp
next
case (Bdt_Node lbdt v rbdt)
then obtain var_p1: "var p1 = v" and var_p2: "var p2 = v"
by simp
then show ?case by simp
qed

lemma bdt_Some_Leaf_var_le_1:
"⟦Dag p low high t; bdt t var = Some x; isLeaf_pt p low high⟧
⟹ var p <= 1"
proof (induct t)
case Tip
thus ?case by simp
next
case (Node lt p rt)
note tNode=this
from Node.prems tNode show ?case
apply (case_tac "var p = 0")
apply simp
apply (case_tac "var p = Suc 0")
apply simp
apply simp
done
qed

lemma subnode_dag_cons:
"⋀ p. ⟦Dag p low high t; no ∈ set_of t⟧ ⟹ ∃ not. Dag no low high not"
proof (induct t)
case Tip
thus ?case by simp
next
case (Node lt q rt)
with Node.prems have q_p: "p = q"
by simp
from Node.prems have lt_dag: "Dag (low p) low high lt"
by auto
from Node.prems have rt_dag: "Dag (high p) low high rt"
by auto
show ?case
proof (cases "no ∈ set_of lt")
case True
with Node.hyps lt_dag show ?thesis
by simp
next
assume no_notin_lt: "no ∉ set_of lt"
show ?thesis
proof (cases "no=p")
case True
with Node.prems q_p show ?thesis
by auto
next
assume no_neq_p: "no ≠ p"
with Node.prems no_notin_lt have no_in_rt: "no ∈ set_of rt"
by simp
with rt_dag Node.hyps show ?thesis
by auto
qed
qed
qed

(*theorems for the proof of share_reduce_rep_list*)

lemma nodes_in_taken_in_takeSucn: "no ∈ set (take n nodeslist) ⟹ no ∈ set (take (Suc n) nodeslist) "
proof -
assume no_in_taken: "no ∈ set (take n nodeslist)"
have "set (take n nodeslist) ⊆ set (take (Suc n) nodeslist)"
apply -
apply (rule set_take_subset_set_take)
apply simp
done
with no_in_taken show ?thesis
by blast
qed

lemma ind_in_higher_take: "⋀n k. ⟦n < k;  n < length xs⟧
⟹ xs ! n ∈ set (take k xs)"
apply (induct xs)
apply simp
apply simp
apply (case_tac n)
apply simp
apply (case_tac k)
apply simp
apply simp
apply simp
apply (case_tac k)
apply simp
apply simp
done

lemma take_length_set: "⋀n. n=length xs ⟹ set (take n xs) = set xs"
apply (induct xs)
apply (auto simp add: take_Cons split: nat.splits)
done

lemma repNodes_eq_ext_rep: "⟦low no ≠ nodeslist! n; high no ≠ nodeslist ! n;
low sn ≠ nodeslist ! n; high sn ≠ nodeslist ! n⟧
⟹ repNodes_eq sn no low high repa = repNodes_eq sn no low high (repa(nodeslist ! n := repa (low (nodeslist ! n))))"

lemma filter_not_empty: "⟦x ∈ set xs; P x⟧ ⟹ filter P xs ≠ []"
by (induct xs) auto

lemma "x ∈ set (filter P xs) ⟹ P x"
by auto

lemma hd_filter_in_list: "filter P xs ≠ [] ⟹ hd (filter P xs) ∈ set xs"
by (induct xs) auto

lemma hd_filter_in_filter: "filter P xs ≠ [] ⟹ hd (filter P xs) ∈ set (filter P xs)"
by (induct xs) auto

lemma hd_filter_prop:
assumes non_empty: "filter P xs ≠ []"
shows "P (hd (filter P xs))"
proof -
from non_empty have "hd (filter P xs) ∈ set (filter P xs)"
by (rule hd_filter_in_filter)
thus ?thesis
by auto
qed

lemma index_elem: "x ∈ set xs ⟹ ∃i<length xs. x = xs ! i"
apply (induct xs)
apply simp
apply (case_tac "x=a")
apply  auto
done

lemma filter_hd_P_rep_indep:
"⟦∀x. P x x; ∀a b. P x a ⟶ P a b ⟶ P x b; filter (P x) xs ≠ []⟧  ⟹
hd (filter (P (hd (filter (P x) xs))) xs) =  hd (filter (P x) xs)"
apply (induct xs)
apply simp
apply (case_tac "P x a")
using [[simp_depth_limit=2]]
apply  (simp)
apply clarsimp
apply (fastforce dest: hd_filter_prop)
done

lemma take_Suc_not_last:
"⋀n. ⟦x ∈ set (take (Suc n) xs); x≠xs!n; n < length xs⟧ ⟹ x ∈ set (take n xs)"
apply (induct xs)
apply  simp
apply (case_tac n)
apply  simp
using [[simp_depth_limit=2]]
apply fastforce
done

lemma P_eq_list_filter: "∀x ∈ set xs. P x = Q x ⟹ filter P xs = filter Q xs"
apply (induct xs)
apply auto
done

lemma hd_filter_take_more: "⋀n m.⟦filter P (take n xs) ≠ []; n ≤ m⟧ ⟹
hd (filter P (take n xs)) =  hd (filter P (take m xs))"
apply (induct xs)
apply  simp
apply (case_tac n)
apply  simp
apply (case_tac m)
apply  simp
apply clarsimp
done

(*
consts wf_levellist :: "dag ⇒ ref list list ⇒ ref list list ⇒
(ref ⇒ nat) ⇒ bool"
defs wf_levellist_def: "wf_levellist t levellist_old levellist_new var  ≡
case t of Tip ⇒ levellist_old = levellist_new
| (Node lt p rt) ⇒
(∀ q. q ∈ set_of t ⟶ q ∈ set (levellist_new ! (var q))) ∧
(∀ i ≤ var p. (∃ prx. (levellist_new ! i) = prx@(levellist_old ! i)
∧ (∀ pt ∈ set prx. pt ∈ set_of t ∧ var pt = i))) ∧
(∀ i. (var p) < i ⟶ (levellist_new ! i) = (levellist_old ! i)) ∧
(length levellist_new = length levellist_old)"
*)

end


# Theory ProcedureSpecs

(*  Title:       BDD
Author:      Veronika Ortner and Norbert Schirmer, 2004
Maintainer:  Norbert Schirmer,  norbert.schirmer at web de
*)

(*
ProcedureSpecs.thy

Copyright (C) 2004-2008 Veronika Ortner and Norbert Schirmer
Some rights reserved, TU Muenchen

This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as

This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.

You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)

section ‹Definitions of Procedures›
theory ProcedureSpecs
imports General Simpl.Vcg
begin

record "globals" =
var_' :: "ref ⇒ nat"
low_' :: "ref ⇒ ref"
high_' :: "ref ⇒ ref"
rep_' :: "ref ⇒ ref"
mark_' :: "ref ⇒ bool"
next_' ::"ref ⇒ ref"

record 'g bdd_state = "'g state" +
varval_' :: "bool list"
p_' :: "ref"
R_' :: "bool"
levellist_' :: "ref list"
nodeslist_' :: "ref"
node_':: "ref"
m_' :: "bool"
n_' :: "nat"

(*Evaluation even of unsymmetric dags.
If a child is unexpectedly Null Eval returns False*)

procedures
Eval (p, varval | R) =
"IF (´p→´var = 0) THEN ´R :==False
ELSE IF (´p→´var = 1) THEN ´R :==True
ELSE IF (´varval ! (´p→´var)) THEN CALL Eval (´p→´high, ´varval, ´R)
ELSE CALL Eval (´p→´low, ´varval, ´R)
FI
FI
FI"

procedures
Levellist (p, m, levellist | levellist) =
"IF (´p ≠ Null)
THEN
IF (´p → ´mark ≠ ´m)
THEN
´levellist :== CALL Levellist ( ´p → ´low, ´m, ´levellist );;
´levellist :== CALL Levellist ( ´p → ´high, ´m, ´levellist );;
´p → ´next :== ´levellist ! (´p→´var);;
´levellist ! (´p→´var) :== ´p;;
´p → ´mark :==´m
FI
FI"

procedures
ShareRep (nodeslist, p) =
"IF (isLeaf_pt ´p ´low ´high)
THEN ´p → ´rep :== ´nodeslist
ELSE
WHILE (´nodeslist ≠ Null) DO
IF (repNodes_eq ´nodeslist ´p ´low ´high ´rep)
THEN ´p→´rep :== ´nodeslist;; ´nodeslist :== Null
ELSE ´nodeslist :== ´nodeslist→´next
FI
OD
FI"

procedures
ShareReduceRepList (nodeslist | ) =
"´node :== ´nodeslist;;
WHILE (´node ≠ Null) DO
IF (¬ isLeaf_pt ´node ´low ´high ∧
´node → ´low → ´rep = ´node → ´high → ´rep )
THEN ´node → ´rep :== ´node → ´low → ´rep
ELSE CALL ShareRep (´nodeslist , ´node )
FI;;
´node :==´node → ´next
OD"

procedures
Repoint (p|p) =
"IF ( ´p ≠ Null )
THEN
´p :== ´p → ´rep;;
IF ( ´p ≠ Null )
THEN ´p  → ´low :== CALL Repoint (´p  → ´low);;
´p  → ´high :== CALL Repoint (´p → ´high)
FI
FI"

procedures
Normalize (p|p) =
"´levellist :==replicate (´p→´var +1) Null;;
´levellist :== CALL Levellist (´p, (¬ ´p→´mark) , ´levellist);;
(´n :==0;;
WHILE (´n < length ´levellist) DO
CALL ShareReduceRepList(´levellist ! ´n);;
´n :==´n + 1
OD);;
´p :== CALL Repoint (´p)"

end


# Theory EvalProof

(*  Title:       BDD

Author:      Veronika Ortner and Norbert Schirmer, 2004
Maintainer:  Norbert Schirmer,  norbert.schirmer at web de
*)

(*
EvalProof.thy

Copyright (C) 2004-2008 Veronika Ortner and Norbert Schirmer
Some rights reserved, TU Muenchen

This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as

This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.

You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)

section ‹Proof of Procedure Eval›
theory EvalProof imports ProcedureSpecs begin

lemma (in Eval_impl) Eval_modifies:
shows "∀σ. Γ⊢{σ}  PROC Eval (´p, ´varval, ´R)
{t. t may_not_modify_globals σ}"
apply (hoare_rule HoarePartial.ProcRec1)
apply (vcg spec=modifies)
done

lemma (in Eval_impl) Eval_spec:
shows "∀σ t bdt1. Γ⊢
⦃σ. Dag ´p ´low ´high t ∧ bdt t ´var = Some bdt1⦄
´R :== PROC Eval(´p, ´varval)
⦃´R = eval bdt1 ⇗σ⇖varval ⦄"
apply (hoare_rule HoarePartial.ProcRec1)
apply vcg
apply clarsimp
apply safe
apply    (case_tac bdt1)
apply      simp
apply     fastforce
apply    fastforce
apply   simp
apply   (case_tac bdt1)
apply     fastforce
apply    fastforce
apply   fastforce
apply  (case_tac bdt1)
apply    fastforce
apply   fastforce
apply  fastforce
apply (case_tac bdt1)
apply   fastforce
apply  fastforce
apply fastforce
done

end


# Theory LevellistProof

(*  Title:       BDD
Author:      Veronika Ortner and Norbert Schirmer, 2004
Maintainer:  Norbert Schirmer,  norbert.schirmer at web de
*)

(*
LevellistProof.thy

Copyright (C) 2004-2008 Veronika Ortner and Norbert Schirmer
Some rights reserved, TU Muenchen

This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as

This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.

You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)

section ‹Proof of Procedure Levellist›
theory LevellistProof imports ProcedureSpecs Simpl.HeapList begin

hide_const (open) DistinctTreeProver.set_of tree.Node tree.Tip

lemma (in Levellist_impl) Levellist_modifies:
shows "∀σ. Γ⊢{σ} ´levellist :== PROC Levellist (´p, ´m, ´levellist)
{t. t may_only_modify_globals σ in [mark,next]}"
apply (hoare_rule HoarePartial.ProcRec1)
apply (vcg spec=modifies)
done

(*a well formed levellist is a list that contains all nodes with variable
i on position i
because the elements of levellist can contain old elements before the call of Levellist,
subdag_eq t pt can not be postulated for all elements of the sublists. One has to make
shure that the initial call of Levellist is parameterized with a levellist with empty sublists.
Otherwise some problems could arise in the call of Reduce!
(∃ ptt. (Dag pt low high ptt ∧ subdag_eq (Node lt p rt) ptt ∧ pt→var = i))
consts wf_levellist :: "dag ⇒ ref list list ⇒ ref list list ⇒
(ref ⇒ nat) ⇒ (ref ⇒ ref) ⇒ (ref ⇒ ref) ⇒ bool"
defs wf_levellist_def: "wf_levellist t levellist_old levellist_new var low high ≡
case t of Tip ⇒ levellist_old = levellist_new
| (Node lt p rt) ⇒
(∀ q. q ∈ set_of t ⟶ q ∈ set (levellist_new ! (q→var))) ∧
(∀ i ≤ p→var. (∃ prx. (levellist_new ! i) = prx@(levellist_old ! i)
∧ (∀ pt ∈ set prx. pt ∈ set_of t ∧ pt→var = i))) ∧
(∀ i. (p→var) < i ⟶ (levellist_new ! i) = (levellist_old ! i)) ∧
(length levellist_new = length levellist_old)"
*)

lemma all_stop_cong: "(∀x. P x) = (∀x. P x)"
by simp

lemma Dag_RefD:
"⟦Dag p l r t; p≠Null⟧ ⟹
∃lt rt. t=Node lt p rt ∧ Dag (l p) l r lt ∧ Dag (r p) l r rt"
by simp

lemma Dag_unique_ex_conjI:
"⟦Dag p l r t;   P t⟧ ⟹ (∃t. Dag p l r t ∧ P t)"
by simp

(* FIXME: To BinDag *)
lemma dag_Null [simp]: "dag Null l r = Tip"

definition first:: "ref list ⇒ ref" where
"first ps = (case ps of [] ⇒ Null | (p#rs) ⇒ p)"

lemma first_simps [simp]:
"first [] = Null"
"first (r#rs) = r"

definition Levellist:: "ref list ⇒ (ref ⇒ ref) ⇒ (ref list list) ⇒ bool" where
"Levellist hds next ll ⟷ (map first ll = hds) ∧
(∀i < length hds. List (hds ! i) next (ll!i))"

lemma Levellist_unique:
assumes ll: "Levellist hds next ll"
assumes ll': "Levellist hds next ll'"
shows "ll=ll'"
proof -
from ll have "length ll = length hds"
moreover
from ll' have "length ll' = length hds"
ultimately have leq: "length ll = length ll'" by simp
show ?thesis
proof (rule nth_equalityI [OF leq, rule_format])
fix i
assume "i < length ll"
with ll ll'
show "ll!i = ll'!i"
apply (erule_tac x=i in allE)
apply (erule_tac x=i in allE)
apply simp
by (erule List_unique)
qed
qed

lemma Levellist_unique_ex_conj_simp [simp]:
"Levellist hds next ll ⟹ (∃ll. Levellist hds next ll ∧ P ll) = P ll"
by (auto dest: Levellist_unique)

lemma in_set_concat_idx:
"x ∈ set (concat xss) ⟹ ∃i < length xss. x ∈ set (xss!i)"
apply (induct xss)
apply  simp
apply clarsimp
apply (erule disjE)
apply  (rule_tac x=0 in exI)
apply  simp
apply auto
done

definition wf_levellist :: "dag ⇒ ref list list ⇒ ref list list ⇒
(ref ⇒ nat) ⇒ bool" where
"wf_levellist t levellist_old levellist_new var =
(case t of Tip ⇒ levellist_old = levellist_new
| (Node lt p rt) ⇒
(∀ q. q ∈ set_of t ⟶ q ∈ set (levellist_new ! (var q))) ∧
(∀ i ≤ var p. (∃ prx. (levellist_new ! i) = prx@(levellist_old ! i)
∧ (∀ pt ∈ set prx. pt ∈ set_of t ∧ var pt = i))) ∧
(∀ i. (var p) < i ⟶ (levellist_new ! i) = (levellist_old ! i)) ∧
(length levellist_new = length levellist_old))"

lemma wf_levellist_subset:
assumes wf_ll: "wf_levellist t ll ll' var"
shows "set (concat ll') ⊆  set (concat ll) ∪ set_of t"
proof (cases t)
case Tip with wf_ll show ?thesis by (simp add: wf_levellist_def)
next
case (Node lt p rt)
show ?thesis
proof -
{
fix n
assume "n ∈ set (concat ll')"
from in_set_concat_idx [OF this]
obtain i where i_bound: "i < length ll'" and n_in: "n ∈ set (ll' ! i)"
by blast
have "n ∈ set (concat ll) ∪ set_of t"
proof (cases "i ≤ var p")
case True
with wf_ll obtain prx where
ll'_ll: "ll' ! i = prx @ ll ! i" and
prx: "∀pt ∈ set prx. pt ∈ set_of t"  and
leq: "length ll' = length ll"
apply (clarsimp simp add: wf_levellist_def Node)
apply (erule_tac x="i" in allE)
apply clarsimp
done
show ?thesis
proof (cases "n ∈ set prx")
case True
with prx have "n ∈ set_of t"
by simp
thus ?thesis by simp
next
case False
with n_in ll'_ll
have "n ∈ set (ll ! i)"
by simp
with i_bound leq
have "n ∈ set (concat ll)"
by auto
thus ?thesis by simp
qed
next
case False
with wf_ll obtain "ll'!i = ll!i" "length ll' = length ll"
by (auto simp add: wf_levellist_def Node)
with n_in i_bound
have "n ∈ set (concat ll)"
by auto
thus ?thesis by simp
qed
}
thus ?thesis by auto
qed
qed
(*
next
show "set (concat ll) ∪ set_of t ⊆ set (concat ll')"
proof -
{
fix n
assume "n ∈ set (concat ll)"
from in_set_concat_idx [OF this]
obtain i where i_bound: "i < length ll" and n_in: "n ∈ set (ll ! i)"
by blast
with wf_ll
obtain "n ∈ set (ll' ! i)" "length ll = length ll'"
apply (clarsimp simp add: wf_levellist_def Node)
apply (case_tac "i ≤ var p")
apply  fastforce
apply fastforce
done
with i_bound have "n ∈ set (concat ll')"
by auto
}
moreover
{
fix n
assume "n ∈ set_of t"
with wf_ll obtain "n ∈ set (ll' ! var n)" "length ll' = length ll"
by (auto simp add: wf_levellist_def Node)
with root

next

proof (cases prx)
case Nil
with ll'_ll i_bound leq n_in
have "n ∈ set (concat ll)"
by auto
thus ?thesis by simp
next
case (Cons p prx')
show ?thesis

apply auto
*)

(*
consts wf_levellist :: "dag ⇒ ref list ⇒ ref list ⇒
(ref ⇒ ref) ⇒ (ref ⇒ ref) ⇒
(ref ⇒ nat) ⇒ bool"
defs wf_levellist_def:
"wf_levellist t levellist_old levellist_new next_old next_new var  ≡
case t of Tip ⇒ levellist_old = levellist_new
| (Node lt p rt) ⇒
(∀ q. q ∈ set_of t ⟶ (∃ns. List (levellist_new ! (var q)) next_new ns ∧
q ∈ set ns)) ∧
(∀ i ≤ var p. (∃ns_new ns_old.
List (levellist_new ! i) next_new ns_new ∧
List (levellist_old ! i) next_old ns_old ∧
(∃ prx. ns_new = prx@ns_old
∧ (∀ pt ∈ set prx. pt ∈ set_of t ∧ var pt = i)))) ∧
(∀ i. (var p) < i ⟶ (∃ns_new ns_old.
List (levellist_new ! i) next_new ns_new ∧
List (levellist_old ! i) next_old ns_old ∧
ns_new = ns_old)) ∧
(length levellist_new = length levellist_old)"
*)

lemma Levellist_ext_to_all: "((∃ll. Levellist hds next ll ∧ P ll) ⟶ Q)
=
(∀ll. Levellist hds next ll ∧ P ll ⟶ Q)"
apply blast
done

lemma Levellist_length: "Levellist hds p ll ⟹ length ll = length hds"

lemma map_update:
"⋀i. i < length xss ⟹ map f (xss[i := xs]) = (map f xss) [i := f xs]"
apply (induct xss)
apply  simp
apply (case_tac i)
apply  simp
apply simp
done

lemma (in Levellist_impl) Levellist_spec_total':
shows "∀ll σ t. Γ,Θ⊢⇩t
⦃σ. Dag ´p ´low ´high t ∧ (´p ≠ Null ⟶ (´p→´var) < length ´levellist) ∧
ordered t ´var ∧ Levellist ´levellist ´next ll ∧
(∀n ∈ set_of t.
(if ´mark n = ´m
then n ∈ set (ll ! ´var n) ∧
(∀nt p. Dag n ´low ´high nt ∧ p ∈ set_of nt
⟶ ´mark p = ´m)
else n ∉ set (concat ll)))⦄
´levellist :== PROC Levellist (´p, ´m, ´levellist)
⦃∃ll'. Levellist ´levellist ´next ll' ∧ wf_levellist t ll ll' ⇗σ⇖var ∧
wf_marking t  ⇗σ⇖mark ´mark ⇗σ⇖m ∧
(∀p. p ∉ set_of t ⟶ ⇗σ⇖next p = ´next p)
⦄"
apply (hoare_rule HoareTotal.ProcRec1
[where r="measure (λ(s,p). size (dag ⇗s⇖p ⇗s⇖low ⇗s⇖high))"])
apply vcg
apply (rule conjI)
apply  clarify
apply  (rule conjI)
apply   clarify
apply   (clarsimp simp del: BinDag.set_of.simps split del: if_split)
defer
apply   (rule impI)
apply   (clarsimp simp del: BinDag.set_of.simps split del: if_split)
defer
apply   (clarsimp simp add: wf_levellist_def wf_marking_def) (* p=Null*)
apply (simp only: Levellist_ext_to_all )
proof -
fix ll var low high mark "next" nexta p levellist m lt rt
assume pnN: "p ≠ Null"
assume mark_p: "mark p = (¬ m)"
assume lt: "Dag (low p) low high lt"
assume rt: "Dag (high p) low high rt"
from pnN lt rt have Dag_p: "Dag p low high (Node lt p rt)" by simp
from Dag_p rt
have size_rt_dec: "size (dag (high p) low high) < size (dag p low high)"
by (simp only: Dag_dag) simp
from Dag_p lt
have size_lt_dec: "size (dag (low p) low high) < size (dag p low high)"
by (simp only: Dag_dag) simp
assume ll: "Levellist levellist next ll"

assume marked_child_ll:
"∀n ∈ set_of (Node lt p rt).
if mark n = m
then n ∈ set (ll ! var n) ∧
(∀nt p. Dag n low high nt ∧ p ∈ set_of nt ⟶ mark p = m)
else n ∉ set (concat ll)"
with mark_p have p_notin_ll: "p ∉ set (concat ll)"
by auto
assume varsll': "var p < length levellist"
with ll have varsll: "var p < length ll"
assume orderedt: "ordered (Node lt p rt) var"
show "(low p ≠ Null ⟶ var (low p) < length levellist) ∧
ordered lt var ∧
(∀n ∈ set_of lt.
if mark n = m
then n ∈ set (ll ! var n) ∧
(∀nt p. Dag n low high nt ∧ p ∈ set_of nt ⟶ mark p = m)
else n ∉ set (concat ll)) ∧
size (dag (low p) low high) < size (dag p low high) ∧
(∀marka nexta levellist lla.
Levellist levellist nexta lla ∧
wf_levellist lt ll lla var ∧ wf_marking lt mark marka m ∧
(∀p. p ∉ set_of lt ⟶ next p = nexta p)⟶
(high p ≠ Null ⟶ var (high p) < length levellist) ∧
ordered rt var ∧
(∃lla. Levellist levellist nexta lla ∧
(∀n ∈ set_of rt.
if marka n = m
then n ∈ set (lla ! var n) ∧
(∀nt p. Dag n low high nt ∧ p ∈ set_of nt ⟶
marka p = m)
else n ∉ set (concat lla)) ∧
size (dag (high p) low high) < size (dag p low high) ∧
(∀markb nextb levellist llb.
Levellist levellist nextb llb ∧
wf_levellist rt lla llb var ∧
wf_marking rt marka markb m ∧
(∀p. p ∉ set_of rt ⟶ nexta p = nextb p) ⟶
(∃ll'. Levellist (levellist[var p := p])
(nextb(p := levellist ! var p)) ll' ∧
wf_levellist (Node lt p rt) ll ll' var ∧
wf_marking (Node lt p rt) mark (markb(p := m)) m ∧
(∀pa. pa ∉ set_of (Node lt p rt) ⟶
next pa =
(if pa = p then levellist ! var p
else nextb pa))))))"
proof (cases "lt")
case Tip
note lt_Tip = this
show ?thesis
proof (cases "rt")
case Tip
show ?thesis
using size_rt_dec Tip lt_Tip Tip lt rt
apply clarsimp
subgoal premises prems for marka nexta levellista lla markb nextb levellistb llb
proof -
have lla: "Levellist levellista nexta lla" by fact
have llb: "Levellist levellistb nextb llb" by fact
have wfll_lt: "wf_levellist Tip ll lla var"
"wf_marking Tip mark marka m" by fact+

then have ll_lla: "ll = lla"

moreover
with wfll_lt lt_Tip lt have "marka = mark"
moreover
have wfll_rt:"wf_levellist Tip lla llb var"
"wf_marking Tip marka markb m" by fact+
then have lla_llb: "lla = llb"
moreover
with wfll_rt Tip rt have "markb = marka"
moreover
from varsll llb ll_lla lla_llb
obtain "var p < length levellistb" "var p < length llb"
with llb pnN
have llc: "Levellist (levellistb[var p := p]) (nextb(p := levellistb ! var p))
(llb[var p := p # llb ! var p])"
apply (clarsimp simp add: Levellist_def map_update)
apply (erule_tac x=i in allE)
apply clarsimp
apply (subgoal_tac "p ∉ set (llb ! i) ")
prefer 2
using  p_notin_ll ll_lla lla_llb
apply  simp
apply (case_tac "i=var p")
apply  simp
apply simp
done
ultimately
show ?thesis
using lt_Tip Tip varsll
apply (clarsimp simp add: wf_levellist_def wf_marking_def)
proof -
fix i
assume varsllb: "var p < length llb"
assume "i ≤ var p"
show "∃prx. llb[var p := p#llb!var p]!i = prx @ llb!i ∧
(∀pt∈set prx. pt = p ∧ var pt = i)"
proof (cases "i = var p")
case True
with pnN lt rt varsllb lt_Tip Tip show ?thesis
apply -
apply (rule_tac x="[p]" in exI)
done
next
assume "i ≠ var p"
with varsllb show ?thesis
apply -
apply (rule_tac x="[]" in exI)
done
qed
qed
qed
done
next
case (Node dag1 a dag2)
have rt_node: "rt = Node dag1 a dag2" by fact
with rt have high_p: "high p = a"
by simp
have s: "⋀nexta. (∀p. next p = nexta p) = (next = nexta)"
by auto
show ?thesis
using size_rt_dec size_lt_dec rt_node lt_Tip Tip lt rt
apply (clarsimp simp del: set_of_Node split del: if_split simp add: s)
subgoal premises prems for marka levellista lla
proof -
have lla: "Levellist levellista next lla" by fact
have wfll_lt:"wf_levellist Tip ll lla var"
"wf_marking Tip mark marka m" by fact+
from this have ll_lla: "ll = lla"
moreover
from wfll_lt lt_Tip lt have marklrec: "marka = mark"
from orderedt varsll lla ll_lla rt_node lt_Tip high_p
have var_highp_bound: "var (high p) < length levellista"
from orderedt high_p rt_node lt_Tip
have ordered_rt: "ordered (Node dag1 (high p) dag2) var"
by simp
from high_p marklrec marked_child_ll lt rt lt_Tip rt_node ll_lla
have mark_rt: "(∀n∈set_of (Node dag1 (high p) dag2).
if marka n = m
then n ∈ set (lla ! var n) ∧
(∀nt p. Dag n low high nt ∧ p ∈ set_of nt ⟶ marka p = m)
else n ∉ set (concat lla))"
apply (simp only: BinDag.set_of.simps)
apply clarify
apply (drule_tac x=n in bspec)
apply  blast
apply assumption
done
show ?thesis
apply (rule conjI)
apply  (rule var_highp_bound)
apply (rule conjI)
apply  (rule ordered_rt)
apply (rule conjI)
apply  (rule mark_rt)
apply clarify
apply clarsimp
subgoal premises prems for markb nextb levellistb llb
proof -
have llb: "Levellist levellistb nextb llb" by fact
have wfll_rt: "wf_levellist (Node dag1 (high p) dag2) lla llb var" by fact
have wfmarking_rt: "wf_marking (Node dag1 (high p) dag2) marka markb m" by fact
from wfll_rt varsll llb ll_lla
obtain var_p_bounds: "var p < length levellistb" "var p < length llb"
with p_notin_ll ll_lla wfll_rt
have p_notin_llb: "∀i < length llb. p ∉ set (llb ! i)"
apply -
apply (intro allI impI)
apply (case_tac "i ≤ var (high p)")
apply  (drule_tac x=i in spec)
using  orderedt rt_node lt_Tip high_p
apply  clarsimp
apply (drule_tac x=i in spec)
apply (drule_tac x=i in spec)
apply clarsimp
done
with llb pnN var_p_bounds
have llc: "Levellist (levellistb[var p := p])
(nextb(p := levellistb ! var p))
(llb[var p := p # llb ! var p])"
apply (clarsimp simp add: Levellist_def map_update)
apply (erule_tac x=i in allE)
apply (erule_tac x=i in allE)
apply clarsimp
apply (case_tac "i=var p")
apply  simp
apply simp
done
then show ?thesis
apply simp
using wfll_rt wfmarking_rt
lt_Tip rt_node varsll orderedt lt rt pnN ll_lla marklrec
apply (clarsimp simp add: wf_levellist_def wf_marking_def)
apply (intro conjI)
apply  (rule allI)
apply  (rule conjI)
apply   (erule_tac x="q" in allE)
apply   (case_tac "var p = var q")
apply    fastforce
apply   fastforce
apply  (case_tac "var p = var q")
apply   hypsubst_thin
apply   fastforce
apply  fastforce
apply (rule allI)
apply (rotate_tac 4)
apply (erule_tac x="i" in allE)
apply (case_tac "i=var p")
apply  simp
apply (case_tac "var (high p) < i")
apply  simp
apply simp
apply (erule exE)
apply (rule_tac x="prx" in exI)
apply (intro conjI)
apply  simp
apply clarify
apply (rotate_tac 15)
apply (erule_tac x="pt" in ballE)
apply  fastforce
apply fastforce
done
qed
done
qed
done
qed
next
case (Node llt l rlt)
have lt_Node: "lt = Node llt l rlt" by fact
from orderedt lt varsll' lt_Node
obtain ordered_lt:
"ordered lt var" "(low p ≠ Null ⟶ var (low p) < length levellist)"
by (cases rt) auto
from lt lt_Node marked_child_ll
have mark_lt: "∀n∈set_of lt.
if mark n = m
then n ∈ set (ll ! var n) ∧
(∀nt p. Dag n low high nt ∧ p ∈ set_of nt ⟶ mark p = m)
else n ∉ set (concat ll)"
apply (simp only: BinDag.set_of.simps)
apply clarify
apply (drule_tac x=n in bspec)
apply  blast
apply assumption
done
show ?thesis
apply (intro conjI ordered_lt mark_lt size_lt_dec)
apply (clarify)
apply (simp add: size_rt_dec split del: if_split)
apply (simp only: Levellist_ext_to_all)
subgoal premises prems for marka nexta levellista lla
proof -
have lla: "Levellist levellista nexta lla" by fact
have wfll_lt: "wf_levellist lt ll lla var"  by fact
have wfmarking_lt:"wf_marking lt mark marka m" by fact
from wfll_lt lt_Node
have lla_eq_ll: "length lla = length ll"
with ll lla have lla_eq_ll': "length levellista = length levellist"
with orderedt rt lt_Node lt varsll'
obtain ordered_rt:
"ordered rt var" "(high p ≠ Null ⟶ var (high p) < length levellista)"
by (cases rt) auto
from wfll_lt lt_Node
have nodes_in_lla: "∀ q. q ∈ set_of lt ⟶ q ∈ set (lla ! (q→var))"
from wfll_lt lt_Node lt
have lla_st: "(∀i ≤ (low p)→var.
(∃prx. (lla ! i) = prx@(ll ! i) ∧
(∀pt ∈ set prx. pt ∈ set_of lt ∧ pt→var = i)))"
from wfll_lt lt_Node lt
have lla_nc: "∀i. ((low p)→var) < i ⟶ (lla ! i) = (ll ! i)"
from wfmarking_lt lt_Node lt
have mot_nc: "∀ n. n ∉ set_of lt ⟶ mark n = marka n"
from wfmarking_lt lt_Node lt
have mit_marked: "∀n. n ∈ set_of lt ⟶ marka n = m"
from marked_child_ll nodes_in_lla mot_nc mit_marked lla_st
have mark_rt: "∀n∈set_of rt.
if marka n = m
then n ∈ set (lla ! var n) ∧
(∀nt p. Dag n low high nt ∧ p ∈ set_of nt ⟶ marka p = m)
else n ∉ set (concat lla)"
apply -
apply (rule ballI)
apply (drule_tac x="n" in bspec)
apply (simp)
proof -
fix n

assume nodes_in_lla: "∀q. q ∈ set_of lt ⟶ q ∈ set (lla ! var q)"
assume mot_nc: "∀n. n ∉ set_of lt ⟶ mark n = marka n"
assume mit_marked: "∀n. n ∈ set_of lt ⟶ marka n = m"
assume marked_child_ll: "if mark n = m
then n ∈ set (ll ! var n) ∧
(∀nt p. Dag n low high nt ∧ p ∈ set_of nt ⟶ mark p = m)
else n ∉ set (concat ll)"

assume lla_st: "∀i≤var (low p).
∃prx. lla ! i = prx @ ll ! i ∧
(∀pt∈set prx. pt ∈ set_of lt ∧ var pt = i)"

assume n_in_rt: " n ∈ set_of rt"
show n_in_lla_marked: "if marka n = m
then n ∈ set (lla ! var n) ∧
(∀nt p. Dag n low high nt ∧ p ∈ set_of nt ⟶ marka p = m)
else n ∉ set (concat lla)"
proof (cases "n ∈ set_of lt")
case True
from True nodes_in_lla have n_in_ll: "n ∈ set (lla ! var n)"
by simp
moreover
from True wfmarking_lt
have "marka n = m"
apply (cases lt)
done
moreover
{
fix nt p
assume "Dag n low high nt"
with lt True have subset_nt_lt: "set_of nt ⊆ set_of lt"
by (rule dag_setof_subsetD)
moreover assume " p ∈ set_of nt"
ultimately have "p ∈ set_of lt"
by blast
with mit_marked have " marka p = m"
by simp
}
ultimately show ?thesis
using n_in_rt
apply clarsimp
done
next
assume n_notin_lt: "n ∉ set_of lt"
show ?thesis
proof (cases "marka n = m")
case True
from n_notin_lt mot_nc have marka_eq_mark: "mark n = marka n"
by simp
from marka_eq_mark True have n_marked: "mark n = m"
by simp
from rt n_in_rt have nnN: "n ≠ Null"
apply -
apply (rule set_of_nn [rule_format])
apply fastforce
apply assumption
done
from marked_child_ll n_in_rt marka_eq_mark nnN n_marked
have n_in_ll: "n ∈ set (ll ! var n)"
by fastforce
from marked_child_ll n_in_rt marka_eq_mark nnN n_marked lt rt
have nt_mark: "∀nt p. Dag n low high nt ∧ p ∈ set_of nt ⟶ mark p = m"
by simp
from nodes_in_lla n_in_ll lla_st
have n_in_lla: "n ∈ set (lla ! var n)"
proof (cases "var (low p) < (var n)")
case True
with lla_nc have "(lla ! var n) = (ll ! var n)"
by fastforce
with n_in_ll show ?thesis
by fastforce
next
assume varnslp: " ¬ var (low p) < var n"
with lla_st
have ll_in_lla: "∃prx. lla ! (var n) = prx @ ll ! (var n)"
apply -
apply (erule_tac x="var n" in allE)
apply fastforce
done
with n_in_ll show ?thesis
by fastforce
qed
{
fix nt pt
assume nt_Dag: "Dag n low high nt"
assume pt_in_nt: "pt ∈ set_of nt"
have " marka pt = m"
proof (cases "pt ∈ set_of lt")
case True
with mit_marked show ?thesis
by fastforce
next
assume pt_notin_lt: " pt ∉ set_of lt"
with mot_nc have "mark pt = marka pt"
by fastforce
with nt_mark nt_Dag pt_in_nt show ?thesis
by fastforce
qed
}
then have nt_marka:
"∀nt pt. Dag n low high nt ∧ pt ∈ set_of nt ⟶ marka pt = m"
by fastforce
with n_in_lla nt_marka True show ?thesis
by fastforce
next
case False
note n_not_marka = this
with wfmarking_lt n_notin_lt
have "mark n ≠ m"
with marked_child_ll
have n_notin_ll: "n ∉ set (concat ll)"
by simp
show ?thesis
proof (cases "n ∈ set (concat lla)")
case False with n_not_marka show ?thesis by simp
next
case True
with wf_levellist_subset [OF wfll_lt] n_notin_ll
have "n ∈ set_of lt"
by blast
with n_notin_lt have False by simp
thus ?thesis ..
qed
qed
qed
qed
show ?thesis
apply (intro conjI ordered_rt mark_rt)
apply clarify
subgoal premises prems for markb nextb levellistb llb
proof -
have llb: "Levellist levellistb nextb llb" by fact
have wfll_rt: "wf_levellist rt lla llb var" by fact
have wfmarking_rt: "wf_marking rt marka markb m" by fact
show ?thesis
proof (cases rt)
case Tip
from wfll_rt Tip have lla_llb: "lla = llb"
moreover
from wfmarking_rt Tip rt have "markb = marka"
moreover
from wfll_lt varsll llb lla_llb
obtain var_p_bounds: "var p < length levellistb" "var p < length llb"
by (simp add: Levellist_length wf_levellist_def lt_Node Tip)
with p_notin_ll lla_llb wfll_lt
have p_notin_llb: "∀i < length llb. p ∉ set (llb ! i)"
apply -
apply (intro allI impI)
apply (clarsimp simp add: wf_levellist_def lt_Node)
apply (case_tac "i ≤ var l")
apply  (drule_tac x=i in spec)
using  orderedt Tip lt_Node
apply  clarsimp
apply (drule_tac x=i in spec)
apply (drule_tac x=i in spec)
apply clarsimp
done
with llb pnN var_p_bounds
have llc: "Levellist (levellistb[var p := p])
(nextb(p := levellistb ! var p))
(llb[var p := p # llb ! var p])"
apply (clarsimp simp add: Levellist_def map_update)
apply (erule_tac x=i in allE)
apply (erule_tac x=i in allE)
apply clarsimp
apply (case_tac "i=var p")
apply  simp
apply simp
done
ultimately show ?thesis
using Tip lt_Node varsll orderedt lt rt pnN wfll_lt wfmarking_lt
apply (clarsimp simp add: wf_levellist_def wf_marking_def)
apply (intro conjI)
apply  (rule allI)
apply  (rule conjI)
apply   (erule_tac x="q" in allE)
apply   (case_tac "var p = var q")
apply    fastforce
apply   fastforce
apply  (case_tac "var p = var q")
apply   hypsubst_thin
apply   fastforce
apply  fastforce
apply (rule allI)
apply (rotate_tac 4)
apply (erule_tac x="i" in allE)
apply (case_tac "i=var p")
apply  simp
apply (case_tac "var (low p) < i")
apply  simp
apply simp
apply (erule exE)
apply (rule_tac x="prx" in exI)
apply (intro conjI)
apply  simp
apply clarify
apply (rotate_tac 15)
apply (erule_tac x="pt" in ballE)
apply  fastforce
apply fastforce
done
next
case (Node lrt r rrt)
have rt_Node: "rt = Node lrt r rrt" by fact
from wfll_rt rt_Node
have llb_eq_lla: "length llb = length lla"
with llb lla
have llb_eq_lla': "length levellistb = length levellista"
from wfll_rt rt_Node
have nodes_in_llb: "∀q. q ∈ set_of rt ⟶ q ∈ set (llb ! (q→var))"
from wfll_rt rt_Node rt
have llb_st: "(∀ i ≤ (high p)→var.
(∃ prx. (llb ! i) = prx@(lla ! i) ∧
(∀pt ∈ set prx. pt ∈ set_of rt ∧ pt→var = i)))"
from wfll_rt rt_Node rt
have llb_nc:
"∀i. ((high p)→var) < i ⟶ (llb ! i) = (lla ! i)"
from wfmarking_rt rt_Node rt
have mort_nc: "∀n. n ∉ set_of rt ⟶ marka n = markb n"
from wfmarking_rt rt_Node rt
have mirt_marked: "∀n. n ∈ set_of rt ⟶ markb n = m"
with p_notin_ll wfll_rt wfll_lt
have p_notin_llb: "∀i < length llb. p ∉ set (llb ! i)"
apply -
apply (intro allI impI)
apply (clarsimp simp add: wf_levellist_def lt_Node rt_Node)
apply (case_tac "i ≤ var r")
apply  (drule_tac x=i in spec)
using  orderedt rt_Node lt_Node
apply  clarsimp
apply  (erule disjE)
apply   clarsimp
apply  (case_tac "i ≤ var l")
apply   (drule_tac x=i in spec)
apply   clarsimp
apply  clarsimp
apply (subgoal_tac "llb ! i = lla ! i")
prefer 2
apply  clarsimp
apply (case_tac "i ≤ var l")
apply  (drule_tac x=i in spec, erule impE, assumption)
apply  clarsimp
using  orderedt rt_Node lt_Node
apply  clarsimp
apply clarsimp
done
from wfll_lt wfll_rt varsll lla llb
obtain var_p_bounds: "var p < length levellistb" "var p < length llb"
by (simp add: Levellist_length wf_levellist_def lt_Node rt_Node)
with p_notin_llb llb pnN var_p_bounds
have llc: "Levellist (levellistb[var p := p])
(nextb(p := levellistb ! var p))
(llb[var p := p # llb ! var p])"
apply (clarsimp simp add: Levellist_def map_update)
apply (erule_tac x=i in allE)
apply (erule_tac x=i in allE)
apply clarsimp
apply (case_tac "i=var p")
apply  simp
apply simp
done
then show ?thesis
proof (clarsimp)
show "wf_levellist (Node lt p rt) ll (llb[var p := p#llb ! var p]) var ∧
wf_marking (Node lt p rt) mark (markb(p := m)) m"
proof -
have nodes_in_upllb: "∀ q. q ∈ set_of (Node lt p rt)
⟶ q ∈ set (llb[var p :=p # llb ! var p] ! (var q))"
apply -
apply (rule allI)
apply (rule impI)
proof -
fix q
assume q_in_t: "q ∈ set_of (Node lt p rt)"
show q_in_upllb:
"q ∈ set (llb[var p :=p # llb ! var p] ! (var q))"
proof (cases "q ∈ set_of rt")
case True
with nodes_in_llb have q_in_llb: "q ∈ set (llb ! (var q))"
by fastforce
from orderedt rt_Node lt_Node lt rt
have ordered_rt: "ordered rt var"
by fastforce
from True rt ordered_rt rt_Node lt lt_Node have "var q ≤ var r"
apply -
apply (drule subnodes_ordered)
apply fastforce
apply fastforce
apply fastforce
done
with orderedt rt lt rt_Node lt_Node have "var q < var p"
by fastforce
then have
"llb[var p :=p#llb ! var p] ! var q =
llb ! var q"
by fastforce
with q_in_llb show ?thesis
by fastforce
next
assume q_notin_rt: "q ∉ set_of rt"
show "q ∈ set (llb[var p :=p # llb ! var p] ! var q)"
proof (cases "q ∈ set_of lt")
case True
assume q_in_lt: "q ∈ set_of lt"
with nodes_in_lla have q_in_lla: "q ∈ set (lla ! (var q))"
by fastforce
from orderedt rt_Node lt_Node lt rt
have ordered_lt: "ordered lt var"
by fastforce
from q_in_lt lt ordered_lt rt_Node rt lt_Node
have "var q ≤ var l"
apply -
apply (drule subnodes_ordered)
apply fastforce
apply fastforce
apply fastforce
done
with orderedt rt lt rt_Node lt_Node have qsp: "var q < var p"
by fastforce
then show ?thesis
proof (cases "var q ≤ var (high p)")
case True
with llb_st
have "∃prx. (llb ! (var q)) = prx@(lla ! (var q))"
by fastforce
with nodes_in_lla q_in_lla
have q_in_llb: "q ∈ set (llb ! (var q))"
by fastforce
from qsp
have "llb[var p :=p#llb ! var p]!var q =
llb ! (var q)"
by fastforce
with q_in_llb show ?thesis
by fastforce
next
assume "¬ var q ≤ var (high p)"
with llb_nc have "llb ! (var q) = lla ! (var q)"
by fastforce
with q_in_lla have q_in_llb: "q ∈ set (llb ! (var q))"
by fastforce
from qsp have
"llb[var p :=p # llb ! var p] ! var q = llb ! (var q)"
by fastforce
with q_in_llb show ?thesis
by fastforce
qed
next
assume q_notin_lt: "q ∉ set_of lt"
with q_notin_rt rt lt rt_Node lt_Node q_in_t have qp: "q = p"
by fastforce
with varsll lla_eq_ll llb_eq_lla have "var p < length llb"
by fastforce
with qp show ?thesis
by simp
qed
qed
qed
have prx_ll_st: "∀i ≤ var p.
(∃prx. llb[var p :=p#llb!var p]!i = prx@(ll!i) ∧
(∀pt ∈ set prx. pt ∈ set_of (Node lt p rt) ∧ var pt = i))"
apply -
apply (rule allI)
apply (rule impI)
proof -
fix i
assume isep: "i ≤ var p"
show "∃prx. llb[var p :=p#llb!var p]!i = prx@ll!i ∧
(∀pt∈set prx. pt ∈ set_of (Node lt p rt) ∧ var pt = i)"
proof (cases "i = var p")
case True
with orderedt lt lt_Node rt rt_Node
have lpsp: "var (low p) < var p"
by fastforce
with orderedt lt lt_Node rt rt_Node
have hpsp: "var (high p) < var p"
by fastforce
with lpsp lla_nc
have llall: "lla ! var p = ll ! var p"
by fastforce
with hpsp llb_nc have "llb ! var p = ll ! var p"
by fastforce
with llb_eq_lla lla_eq_ll isep True varsll lt rt show ?thesis
apply -
apply (rule_tac x="[p]" in exI)
apply (rule conjI)
apply simp
apply (rule ballI)
apply fastforce
done
next
assume inp: " i ≠ var p"
show ?thesis
proof (cases "var (low p) < i")
case True
with lla_nc have llall: "lla ! i = ll ! i"
by fastforce
assume vpsi: "var (low p) < i"
show ?thesis
proof (cases "var (high p) < i")
case True
with llall llb_nc have "llb ! i = ll ! i"
by fastforce
with inp True vpsi varsll lt rt show ?thesis
apply -
apply (rule_tac x="[]" in exI)
apply (rule conjI)
apply simp
apply (rule ballI)
apply fastforce
done
next
assume isehp: " ¬ var (high p) < i"
with vpsi lla_nc have lla_ll: "lla ! i = ll ! i"
by fastforce
with isehp llb_st
have prx_lla: "∃prx. llb ! i = prx @ lla ! i ∧
(∀pt∈set prx. pt ∈ set_of rt ∧ var pt = i)"
apply -
apply (erule_tac x="i" in allE)
apply simp
done
with lla_ll inp rt show ?thesis
apply -
apply (erule exE)
apply (rule_tac x="prx" in exI)
apply simp
done
qed
next
assume iselp: "¬ var (low p) < i"
show ?thesis
proof (cases "var (high p) < i")
case True
with llb_nc have llb_ll: "llb ! i = lla ! i"
by fastforce
with iselp lla_st
have prx_ll: "∃prx. lla ! i = prx @ ll ! i ∧
(∀pt∈set prx. pt ∈ set_of lt ∧ var pt = i)"
apply -
apply (erule_tac x="i" in allE)
apply simp
done
with llb_ll inp lt show ?thesis
apply -
apply (erule exE)
apply (rule_tac x="prx" in exI)
apply simp
done
next
assume isehp: " ¬ var (high p) < i"
from iselp lla_st
have prxl: "∃prx. lla ! i = prx @ ll ! i ∧
(∀pt∈set prx. pt ∈ set_of lt ∧ var pt = i)"
by fastforce
from isehp llb_st
have prxh: "∃prx. llb ! i = prx @ lla ! i ∧
(∀pt∈set prx. pt ∈ set_of rt ∧ var pt = i)"
by fastforce
with prxl inp lt pnN rt show ?thesis
apply -
apply (elim exE)
apply (rule_tac x="prxa @ prx" in exI)
apply simp
apply (elim conjE)
apply fastforce
done
qed
qed
qed
qed
have big_Nodes_nc: "∀i. (p->var) < i
⟶ (llb[var p :=p # llb ! var p]) ! i = ll ! i"
apply -
apply (rule allI)
apply (rule impI)
proof -
fix i
assume psi: "var p < i"
with orderedt lt rt lt_Node rt_Node have lpsi: "var (low p) < i"
by fastforce
with lla_nc have lla_ll: "lla ! i = ll ! i"
by fastforce
from psi orderedt lt rt lt_Node rt_Node have hpsi: "var (high p) < i"
by fastforce
with llb_nc have llb_lla: "llb ! i = lla ! i"
by fastforce
from psi
have upllb_llb: "llb[var p :=p#llb!var p]!i = llb!i"
by fastforce
from upllb_llb llb_lla lla_ll
show "llb[var p :=p # llb ! var p] ! i = ll ! i"
by fastforce
qed
from lla_eq_ll llb_eq_lla
have length_eq: "length (llb[var p :=p # llb ! var p]) = length ll"
by fastforce
from length_eq big_Nodes_nc prx_ll_st nodes_in_upllb
have wf_ll_upllb:
"wf_levellist (Node lt p rt) ll (llb[var p :=p # llb ! var p]) var"
have mark_nc:
"∀ n. n ∉ set_of (Node lt p rt) ⟶ (markb(p:=m)) n = mark n"
apply -
apply (rule allI)
apply (rule impI)
proof -
fix n
assume nnit: "n ∉ set_of (Node lt p rt)"
with lt rt have nnilt: " n ∉ set_of lt"
by fastforce
from nnit lt rt have nnirt: " n ∉ set_of rt"
by fastforce
with nnilt mot_nc mort_nc have mb_eq_m: "markb n = mark n"
by fastforce
from nnit have "n≠p"
by fastforce
then have upmarkb_markb: "(markb(p :=m)) n = markb n"
by fastforce
with mb_eq_m show "(markb(p :=m)) n = mark n"
by fastforce
qed
have mark_c: "∀ n. n ∈ set_of (Node lt p rt) ⟶ (markb(p :=m)) n = m"
apply -
apply (intro allI)
apply (rule impI)
proof -
fix n
assume nint: " n ∈ set_of (Node lt p rt)"
show "(markb(p :=m)) n = m"
proof (cases "n=p")
case True
then show ?thesis
by fastforce
next
assume nnp: " n ≠ p"
show ?thesis
proof (cases "n ∈ set_of rt")
case True
with mirt_marked have "markb n = m"
by fastforce
with nnp show ?thesis
by fastforce
next
assume nninrt: " n ∉ set_of rt"
with nint nnp have ninlt: "n ∈ set_of lt"
by fastforce
with mit_marked have marka_m: "marka n = m"
by fastforce
from mort_nc nninrt have "marka n = markb n"
by fastforce
with marka_m have "markb n = m"
by fastforce
with nnp show ?thesis
by fastforce
qed
qed
qed
from mark_c mark_nc
have wf_mark: "wf_marking (Node lt p rt) mark (markb(p :=m)) m"
with wf_ll_upllb show ?thesis
by fastforce
qed
qed
qed
qed
done
qed
done
qed
next
fix var low high p lt rt and levellist and
ll::"ref list list" and mark::"ref ⇒ bool" and "next"
assume pnN: "p ≠ Null"
assume ll: "Levellist levellist next ll"
assume vpsll: "var p < length levellist"
assume orderedt: "ordered (Node lt p rt) var"
assume marked_child_ll: "∀n∈set_of (Node lt p rt).
if mark n = mark p
then n ∈ set (ll ! var n) ∧
(∀nt pa. Dag n low high nt ∧ pa ∈ set_of nt ⟶ mark pa = mark p)
else n ∉ set (concat ll)"
assume lt: "Dag (low p) low high lt"
assume rt: "Dag (high p) low high rt"
show "wf_levellist (Node lt p rt) ll ll var ∧
wf_marking (Node lt p rt) mark mark (mark p)"
proof -
from marked_child_ll pnN lt rt have marked_st:
"(∀pa. pa ∈ set_of (Node lt p rt) ⟶ mark pa = mark p)"
apply -
apply (drule_tac x="p" in bspec)
apply  simp
apply (clarsimp)
apply (erule_tac x="(Node lt p rt)" in allE)
apply simp
done
have nodest_in_ll:
"∀q. q ∈ set_of (Node lt p rt) ⟶ q ∈ set (ll ! var q)"
proof -
from marked_child_ll pnN have pinll: "p ∈ set (ll ! var p)"
apply -
apply (drule_tac x="p" in bspec)
apply  simp
apply fastforce
done
from marked_st marked_child_ll lt rt show ?thesis
apply -
apply (rule allI)
apply (erule_tac x="q" in allE)
apply (rule impI)
apply (erule impE)
apply  assumption
apply (drule_tac x="q" in bspec)
apply  simp
apply fastforce
done
qed
have levellist_nc: "∀ i ≤ var p. (∃ prx. ll ! i = prx@(ll ! i) ∧
(∀ pt ∈ set prx. pt ∈ set_of (Node lt p rt) ∧ var pt = i))"
apply -
apply (rule allI)
apply (rule impI)
apply (rule_tac x="[]" in exI)
apply fastforce
done
have ll_nc: "∀ i. (var p) < i ⟶ ll ! i = ll ! i"
by fastforce
have length_ll: "length ll = length ll"
by fastforce
with ll_nc levellist_nc nodest_in_ll
have wf: "wf_levellist (Node lt p rt) ll ll var"
have m_nc: "∀ n. n ∉ set_of (Node lt p rt) ⟶ mark n = mark n"
by fastforce
from marked_st have "∀ n. n ∈ set_of (Node lt p rt) ⟶ mark n = mark p"
by fastforce
with m_nc have " wf_marking (Node lt p rt) mark mark (mark p)"
with wf show ?thesis
by fastforce
qed
qed

lemma allD: "∀ll. P ll ⟹ P ll"
by blast

lemma replicate_spec: "⟦∀i < n. xs ! i = x; n=length xs⟧
⟹ replicate (length xs) x = xs"
apply hypsubst_thin
apply (induct xs)
apply  simp
apply force
done

lemma (in Levellist_impl) Levellist_spec_total:
shows "∀σ t. Γ,Θ⊢⇩t
⦃σ. Dag ´p ´low ´high t ∧ (∀i < length ´levellist. ´levellist ! i = Null) ∧
length ´levellist  = ´p → ´var + 1 ∧
ordered t ´var ∧ (∀n ∈ set_of t. ´mark n = (¬ ´m) )⦄
´levellist :== PROC Levellist (´p, ´m, ´levellist)
⦃∃ll. Levellist ´levellist ´next ll ∧ wf_ll t ll ⇗σ⇖var  ∧
length ´levellist = ⇗σ⇖p → ⇗σ⇖var + 1 ∧
wf_marking t ⇗σ⇖mark ´mark ⇗σ⇖m ∧
(∀p. p ∉ set_of t ⟶ ⇗σ⇖next p = ´next p)⦄"
apply (hoare_rule HoareTotal.conseq)
apply  (rule_tac ll="replicate (⇗σ⇖p→⇗σ⇖var + 1) []" in allD [OF Levellist_spec_total'])
apply (intro allI impI)
apply (rule_tac x=σ in exI)
apply (rule_tac x=t in exI)
apply (rule conjI)
apply  (clarsimp split:if_split_asm simp del: concat_replicate_trivial)
apply  (frule replicate_spec [symmetric])
apply   (simp)
apply  (clarsimp simp add: Levellist_def )
apply  (case_tac i)
apply   simp
apply  simp
apply vcg_step
apply (elim exE conjE)
apply (rule_tac x=ll' in exI)
apply simp
apply (thin_tac "∀p. p ∉ set_of t ⟶ next p = nexta p")
apply (case_tac "t = Tip")
apply  simp
apply  (rule conjI)
apply   clarsimp
apply   (case_tac k)
apply    simp
apply   simp
apply  (subgoal_tac "length ll'=Suc (var Null)")
apply  fastforce
apply (split dag.splits)
apply  simp
apply (elim conjE)
apply (intro conjI)
apply   (rule allI)
apply   (erule_tac x="pa" in allE)
apply   clarify
prefer 2
apply (rule allI)
apply (rule impI)
apply (rule ballI)
apply (rotate_tac 11)
apply (erule_tac x="k" in allE)
apply (rename_tac dag1 ref dag2 k pa)
apply (subgoal_tac "k <= var ref")
prefer 2
apply  (subgoal_tac "ref = p")
apply   simp
apply  clarify
apply  (erule_tac ?P = "Dag p low high (Node dag1 ref dag2)" in rev_mp)
apply  (simp (no_asm))
apply (rotate_tac 14)
apply (erule_tac x=k in allE)
apply clarify
apply (erule_tac x=k in allE)
apply clarify
apply (case_tac k)
apply  simp
apply simp
done

end


# Theory ShareRepProof

(*  Title:       BDD

Author:      Veronika Ortner and Norbert Schirmer, 2004
Maintainer:  Norbert Schirmer,  norbert.schirmer at web de
*)

(*
ShareRepProof.thy

Copyright (C) 2004-2008 Veronika Ortner and Norbert Schirmer
Some rights reserved, TU Muenchen

This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as

This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.

You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)

section ‹Proof of Procedure ShareRep›
theory ShareRepProof imports ProcedureSpecs Simpl.HeapList begin

lemma (in ShareRep_impl) ShareRep_modifies:
shows "∀σ. Γ⊢{σ}  PROC ShareRep (´nodeslist, ´p)
{t. t may_only_modify_globals σ in [rep]}"
apply (hoare_rule HoarePartial.ProcRec1)
apply (vcg spec=modifies)
done

lemma hd_filter_cons:
"⋀ i. ⟦ P (xs ! i) p; i < length xs; ∀ no ∈ set (take i xs). ¬ P no p; ∀ a b.  P a b = P b a⟧
⟹ xs ! i = hd (filter (P p) xs)"
apply (induct xs)
apply simp
apply (case_tac "P a p")
apply simp
apply (case_tac i)
apply simp
apply simp
apply (case_tac i)
apply simp
apply auto
done

lemma (in ShareRep_impl) ShareRep_spec_total:
shows
"∀σ ns. Γ,Θ⊢⇩t
⦃σ. List ´nodeslist ´next ns ∧
(∀no ∈ set ns. no ≠ Null  ∧
((no→´low = Null) = (no→´high = Null)) ∧
(isLeaf_pt ´p ´low ´high ⟶ isLeaf_pt no ´low ´high) ∧
no→´var = ´p→´var) ∧
´p ∈ set ns⦄
PROC ShareRep (´nodeslist, ´p)
⦃ (⇗σ⇖p → ´rep = hd (filter (λ sn. repNodes_eq sn ⇗σ⇖p ⇗σ⇖low ⇗σ⇖high ⇗σ⇖rep) ns)) ∧
(∀pt.  pt ≠ ⇗σ⇖p ⟶ pt→⇗σ⇖rep = pt→´rep) ∧
(⇗σ⇖p→´rep→⇗σ⇖var = ⇗σ⇖p → ⇗σ⇖var)⦄"
apply (hoare_rule HoareTotal.ProcNoRec1)
apply (hoare_rule anno=
"IF (isLeaf_pt ´p ´low ´high)
THEN ´p → ´rep :== ´nodeslist
ELSE
WHILE (´nodeslist ≠ Null)
INV ⦃∃prx sfx. List ´nodeslist ´next sfx ∧ ns=prx@sfx ∧
¬ isLeaf_pt ´p ´low ´high ∧
(∀no ∈ set ns. no ≠ Null ∧
((no→⇗σ⇖low = Null) = (no→⇗σ⇖high = Null)) ∧
(isLeaf_pt ⇗σ⇖p ⇗σ⇖low ⇗σ⇖high ⟶ isLeaf_pt no ⇗σ⇖low ⇗σ⇖high) ∧
no→⇗σ⇖var = ⇗σ⇖p→⇗σ⇖var) ∧
⇗σ⇖p ∈ set ns ∧
((∃pt ∈ set prx.  repNodes_eq pt ⇗σ⇖p ⇗σ⇖low ⇗σ⇖high ⇗σ⇖rep)
⟶ ´rep  ⇗σ⇖p =  hd (filter (λ sn. repNodes_eq sn ⇗σ⇖p ⇗σ⇖low ⇗σ⇖high ⇗σ⇖rep) prx) ∧
(∀pt. pt ≠ ⇗σ⇖p ⟶ pt→⇗σ⇖rep = pt→´rep)) ∧
((∀pt ∈ set prx.  ¬ repNodes_eq pt ⇗σ⇖p ⇗σ⇖low ⇗σ⇖high ⇗σ⇖rep) ⟶  ⇗σ⇖rep = ´rep) ∧
(´nodeslist ≠ Null ⟶
(∀pt ∈ set prx. ¬ repNodes_eq pt ⇗σ⇖p ⇗σ⇖low ⇗σ⇖high ⇗σ⇖rep)) ∧
(´p = ⇗σ⇖p ∧ ´high = ⇗σ⇖high ∧ ´low = ⇗σ⇖low)⦄
VAR MEASURE (length (list ´nodeslist ´next))
DO
IF (repNodes_eq ´nodeslist ´p ´low ´high ´rep)
THEN ´p→´rep :== ´nodeslist;; ´nodeslist :== Null
ELSE ´nodeslist :== ´nodeslist→´next
FI
OD
FI" in HoareTotal.annotateI)
apply vcg
using  [[simp_depth_limit = 2]]
apply   (rule conjI)
apply    clarify
apply    (simp (no_asm_use))
prefer 2
apply    clarify
apply    (rule_tac x="[]" in exI)
apply    (rule_tac x=ns in exI)
apply    (simp (no_asm_use))
prefer 2
apply   clarify
apply   (rule conjI)
apply    clarify
apply    (rule conjI)
apply     (clarsimp simp add: List_list) (* solving termination contraint *)
apply    (simp (no_asm_use))
apply    (rule conjI)
apply    assumption
prefer 2
apply    clarify
apply    (simp (no_asm_use))
apply    (rule conjI)
apply    (clarsimp simp add: List_list) (* solving termination constraint *)
apply    (simp only: List_not_Null simp_thms triv_forall_equality)
apply    clarify
apply    (simp only: triv_forall_equality)
apply    (rename_tac sfx)
apply    (rule_tac x="prx@[nodeslist]" in exI)
apply    (rule_tac x="sfx" in exI)
apply    (rule conjI)
apply     assumption
apply    (rule conjI)
apply     simp
prefer 4
apply   (elim exE conjE)
apply   (simp (no_asm_use))
apply   hypsubst
using  [[simp_depth_limit = 100]]
proof -
(* IF-THEN to postcondition *)
fix ns var low high rep "next" p nodeslist
assume ns: "List nodeslist next ns"
assume no_prop:  "∀no∈set ns.
no ≠ Null ∧
(low no = Null) = (high no = Null) ∧
(isLeaf_pt p low high ⟶ isLeaf_pt no low high) ∧ var no = var p"
assume p_in_ns: "p ∈ set ns"
assume p_Leaf: "isLeaf_pt p low high"
show "nodeslist = hd [sn←ns . repNodes_eq sn p low high rep] ∧
var nodeslist = var p"
proof -
from p_in_ns no_prop have p_not_Null: "p≠Null"
using [[simp_depth_limit=2]]
by auto
from p_in_ns have "ns ≠ []"
by (cases ns) auto
with ns obtain ns' where ns': "ns = nodeslist#ns'"
by (cases "nodeslist=Null") auto
with no_prop p_Leaf obtain
"isLeaf_pt nodeslist low high" and
var_eq: "var nodeslist = var p" and
"nodeslist≠Null"
using [[simp_depth_limit=2]]
by auto
with p_not_Null p_Leaf have "repNodes_eq nodeslist p low high rep"
by (simp add: repNodes_eq_def isLeaf_pt_def null_comp_def)
with ns' var_eq
show ?thesis
by simp
qed
next
(* From invariant to postcondition *)
fix var::"ref⇒nat" and low high rep repa p prx sfx "next"
assume sfx: "List Null next sfx"
assume p_in_ns: "p ∈ set (prx @ sfx)"
assume no_props: "∀no∈set (prx @ sfx).
no ≠ Null ∧
(low no = Null) = (high no = Null) ∧
(isLeaf_pt p low high ⟶ isLeaf_pt no low high) ∧ var no = var p"
assume match_prx: "(∃pt∈set prx. repNodes_eq pt p low high rep) ⟶
repa p = hd [sn←prx . repNodes_eq sn p low high rep] ∧
(∀pt. pt ≠ p ⟶ rep pt = repa pt)"
show "repa p = hd [sn←prx @ sfx . repNodes_eq sn p low high rep] ∧
(∀pt. pt ≠ p ⟶ rep pt = repa pt) ∧ var (repa p) = var p"
proof -
from sfx
have sfx_Nil: "sfx=[]"
by simp
with p_in_ns have ex_match: "(∃pt∈set prx. repNodes_eq pt p low high rep)"
apply -
apply (rule_tac x=p in bexI)
apply simp
done
hence not_empty: "[sn←prx . repNodes_eq sn p low high rep] ≠ []"
apply -
apply (erule bexE)
apply (rule filter_not_empty)
apply auto
done
from ex_match match_prx obtain
found: "repa p = hd [sn←prx . repNodes_eq sn p low high rep]" and
unmodif: "∀pt. pt ≠ p ⟶ rep pt = repa pt"
by blast
from hd_filter_in_list [OF not_empty] found
have "repa p ∈ set prx"
by simp
with no_props
have "var (repa p) = var p"
using [[simp_depth_limit=2]]
by simp
with found unmodif sfx_Nil
show ?thesis
by simp
qed
next
(* Invariant to invariant; ELSE part *)
fix var low high p repa "next" nodeslist prx sfx
assume nodeslist_not_Null: "nodeslist ≠ Null"
assume p_no_Leaf: "¬ isLeaf_pt p low high"
assume no_props: "∀no∈set prx ∪ set (nodeslist # sfx).
no ≠ Null ∧ (low no = Null) = (high no = Null) ∧ var no = var p"
assume p_in_ns: "p ∈ set prx ∨ p ∈ set (nodeslist # sfx)"
assume match_prx: "(∃pt∈set prx. repNodes_eq pt p low high repa) ⟶
repa p = hd [sn←prx . repNodes_eq sn p low high repa]"
assume nomatch_prx: "∀pt∈set prx. ¬ repNodes_eq pt p low high repa"
assume nomatch_nodeslist: "¬ repNodes_eq nodeslist p low high repa"
assume sfx: "List (next nodeslist) next sfx"
show "(∀no∈set prx ∪ set (nodeslist # sfx).
no ≠ Null ∧ (low no = Null) = (high no = Null) ∧ var no = var p) ∧
((∃pt∈set (prx @ [nodeslist]). repNodes_eq pt p low high repa) ⟶
repa p = hd [sn←prx @ [nodeslist] . repNodes_eq sn p low high repa]) ∧
(next nodeslist ≠ Null ⟶
(∀pt∈set (prx @ [nodeslist]). ¬ repNodes_eq pt p low high repa))"
proof -
from nomatch_prx nomatch_nodeslist
have "((∃pt∈set (prx @ [nodeslist]). repNodes_eq pt p low high repa) ⟶
repa p = hd [sn←prx @ [nodeslist] . repNodes_eq sn p low high repa])"
by auto
moreover
from nomatch_prx nomatch_nodeslist
have "(next nodeslist ≠ Null ⟶
(∀pt∈set (prx @ [nodeslist]). ¬ repNodes_eq pt p low high repa))"
by auto
ultimately show ?thesis
using no_props
by (intro conjI)
qed
next
(* Invariant to invariant: THEN part *)
fix var low high p repa "next" nodeslist prx sfx
assume nodeslist_not_Null: "nodeslist ≠ Null"
assume sfx: "List nodeslist next sfx"
assume p_not_Leaf: "¬ isLeaf_pt p low high"
assume no_props: "∀no∈set prx ∪ set sfx.
no ≠ Null ∧
(low no = Null) = (high no = Null) ∧
(isLeaf_pt p low high ⟶ isLeaf_pt no low high) ∧ var no = var p"
assume p_in_ns: "p ∈ set prx ∨ p ∈ set sfx"
assume match_prx: "(∃pt∈set prx. repNodes_eq pt p low high repa) ⟶
repa p = hd [sn←prx . repNodes_eq sn p low high repa]"
assume nomatch_prx: "∀pt∈set prx. ¬ repNodes_eq pt p low high repa"
assume match: "repNodes_eq nodeslist p low high repa"
show "(∀no∈set prx ∪ set sfx.
no ≠ Null ∧
(low no = Null) = (high no = Null) ∧
(isLeaf_pt p low high ⟶ isLeaf_pt no low high) ∧ var no = var p) ∧
(p ∈ set prx ∨ p ∈ set sfx) ∧
((∃pt∈set prx ∪ set sfx. repNodes_eq pt p low high repa) ⟶
nodeslist =
hd ([sn←prx . repNodes_eq sn p low high repa] @
[sn←sfx . repNodes_eq sn p low high repa])) ∧
((∀pt∈set prx ∪ set sfx. ¬ repNodes_eq pt p low high repa) ⟶
repa = repa(p := nodeslist))"
proof -
from nodeslist_not_Null sfx
obtain sfx' where sfx': "sfx=nodeslist#sfx'"
by (cases "nodeslist=Null") auto
from nomatch_prx match sfx'
have hd: "hd ([sn←prx . repNodes_eq sn p low high repa] @
[sn←sfx . repNodes_eq sn p low high repa]) = nodeslist"
by simp
from match sfx'
have triv: "((∀pt∈set prx ∪ set sfx. ¬ repNodes_eq pt p low high repa) ⟶
repa = repa(p := nodeslist))"
by simp
show ?thesis
apply (rule conjI)
apply (rule no_props)
apply (intro conjI)
apply   (rule p_in_ns)
apply (rule triv)
done
qed
qed

end


# Theory ShareReduceRepListProof

(*  Title:       BDD

Author:      Veronika Ortner and Norbert Schirmer, 2004
Maintainer:  Norbert Schirmer,  norbert.schirmer at web de
*)

(*
ShareReduceRepListProof.thy

Copyright (C) 2004 Veronika Ortner and Norbert Schirmer
Some rights reserved, TU Muenchen

This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as

This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.

You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)

section ‹Proof of Procedure ShareReduceRepList›
theory ShareReduceRepListProof imports ShareRepProof begin

lemma (in ShareReduceRepList_impl) ShareReduceRepList_modifies:
shows "∀σ. Γ⊢{σ}  PROC ShareReduceRepList (´nodeslist)
{t. t may_only_modify_globals σ in [rep]}"
apply (hoare_rule HoarePartial.ProcRec1)
apply (vcg spec=modifies)
done

lemma hd_filter_app: "⟦filter P xs ≠ []; zs=xs@ys⟧ ⟹
hd (filter P zs) =  hd (filter P xs)"
by (induct xs arbitrary: n m) auto

lemma (in ShareReduceRepList_impl) ShareReduceRepList_spec_total:
defines "var_eq ≡ (λns var. (∀no1 ∈ set ns. ∀no2 ∈ set ns. no1→var = no2→var))"
shows
"∀σ ns. Γ⊢⇩t
⦃σ. List ´nodeslist ´next ns ∧
(∀no ∈ set ns.
no ≠ Null ∧ ((no→´low = Null) = (no→´high = Null)) ∧
no→´low ∉ set ns ∧ no→´high ∉ set ns ∧
(isLeaf_pt no ´low ´high = (no→´var ≤ 1)) ∧
(no→´low ≠ Null ⟶ (no→´low)→´rep ≠ Null) ∧
((´rep ∝ ´low) no ∉ set ns)) ∧
var_eq ns ´var⦄
PROC  ShareReduceRepList (´nodeslist)
⦃(∀no. no ∉ set ns ⟶ no→⇗σ⇖rep = no→´rep)  ∧
(∀no ∈ set ns. no→´rep ≠ Null ∧
(if ((´rep ∝ ⇗σ⇖low) no = (´rep ∝ ⇗σ⇖high) no ∧ no→ ⇗σ⇖low ≠ Null)
then (no→´rep = (´rep ∝ ⇗σ⇖low) no )
else ((no→´rep) ∈ set ns ∧ no→´rep→´rep = no→´rep ∧
(∀ no1 ∈ set ns.
((´rep ∝ ⇗σ⇖high) no1 = (´rep ∝ ⇗σ⇖high) no ∧
(´rep ∝ ⇗σ⇖low) no1 = (´rep ∝ ⇗σ⇖low) no) = (no→´rep = no1→´rep)))))⦄"
apply (hoare_rule HoareTotal.ProcNoRec1)
apply (hoare_rule anno=
" ´node :== ´nodeslist;;
WHILE (´node ≠ Null )
INV ⦃∃prx sfx. List ´node ´next sfx ∧
List ´nodeslist ´next ns ∧ ns=prx@sfx ∧
(∀no ∈ set ns.
no ≠ Null ∧ ((no→⇗σ⇖low = Null) = (no→⇗σ⇖high = Null)) ∧
no→⇗σ⇖low ∉ set ns ∧ no→⇗σ⇖high ∉ set ns ∧
(isLeaf_pt no  ⇗σ⇖low ⇗σ⇖high = (no→⇗σ⇖var ≤ 1)) ∧
(no→⇗σ⇖low ≠ Null ⟶ (no→⇗σ⇖low)→⇗σ⇖rep ≠ Null) ∧
((⇗σ⇖rep ∝ ⇗σ⇖low) no  ∉ set ns)) ∧
var_eq ns ´var ∧
(∀no.  no ∉ set prx ⟶ no→⇗σ⇖rep = no →´rep)  ∧
(∀ no ∈ set prx. no→´rep ≠ Null ∧
(if ((´rep ∝ ⇗σ⇖low) no = (´rep ∝ ⇗σ⇖high) no ∧ no→⇗σ⇖low ≠ Null)
then (no→´rep = (´rep ∝ ⇗σ⇖low) no )
else ((no→´rep)=hd (filter (λsn. repNodes_eq sn no ⇗σ⇖low ⇗σ⇖high ´rep)
prx) ∧
((no→´rep)→´rep) = no→´rep ∧
(∀no1 ∈ set prx.
((´rep ∝ ⇗σ⇖high) no1 = (´rep ∝ ⇗σ⇖high) no ∧
(´rep ∝ ⇗σ⇖low) no1 = (´rep ∝ ⇗σ⇖low) no) =
(no→´rep = no1→´rep))))) ∧
´nodeslist= ⇗σ⇖nodeslist ∧ ´high=⇗σ⇖high ∧ ´low=⇗σ⇖low ∧ ´var=⇗σ⇖var⦄
VAR MEASURE (length (list ´node ´next))
DO
IF (¬ isLeaf_pt ´node ´low ´high ∧
´node → ´low → ´rep = ´node → ´high → ´rep )
THEN ´node → ´rep :== ´node → ´low → ´rep
ELSE CALL ShareRep (´nodeslist , ´node)
FI;;
´node :==´node → ´next
OD" in HoareTotal.annotateI)
apply (vcg spec=spec_total)
apply   (rule_tac x="[]" in exI)
apply   (rule_tac x="ns" in exI)
using [[simp_depth_limit = 2]]
apply   (simp (no_asm_use))
prefer 2
using [[simp_depth_limit = 4]]
apply (clarsimp)
prefer 2
apply  (rule conjI)
apply   clarify
apply   (rule conjI)
apply    (clarsimp simp add: List_list) (* termination *)
apply   (simp only: List_not_Null simp_thms triv_forall_equality)
apply   clarify
apply   (simp only: triv_forall_equality)
apply   (rename_tac sfx)
apply   (rule_tac x="prx@[node]" in exI)
apply   (rule_tac x="sfx" in exI)
apply   (rule conjI)
apply    assumption
apply   (rule conjI)
apply    (simp (no_asm))
apply   (rule conjI)
apply    (assumption)
prefer 2
apply   clarify
apply   (simp only: List_not_Null simp_thms triv_forall_equality)
apply   clarify
apply   (simp only: triv_forall_equality)
apply   (rename_tac sfx)
apply   (rule_tac x="prx@node#sfx" in exI) (* Precondition for ShareRep *)
apply   (rule conjI)
apply    assumption
apply   (rule conjI)
apply    (rule ballI)
apply    (frule_tac x=no in bspec, assumption)
apply    (drule_tac x=node in bspec)
apply     (simp (no_asm_use))
apply    (elim conjE)
apply    (rule conjI)
apply     assumption
apply    (rule conjI)
apply     assumption
apply    (unfold var_eq_def)
apply    (drule_tac x=node in bspec, simp)
apply    (drule_tac x=no in bspec,assumption)
apply   (rule conjI)
apply    (simp (no_asm))
apply   (clarify)
apply   (rule conjI)
apply    (subgoal_tac "List node next (node#sfx)") (* termination *)
apply     (simp only: List_list)
apply     (simp (no_asm))
apply    (simp (no_asm_simp))
apply   (rule_tac x="prx@[node]" in exI)
apply   (rule_tac x="sfx" in exI)
apply   (rule conjI)
apply    assumption
apply   (rule conjI)
apply    (simp (no_asm))
apply   (rule conjI)
apply    (assumption)
using [[simp_depth_limit = 100]]
proof - (* From invariant to postcondition *)
fix var low high rep nodeslist ns repa "next" no
assume ns: "List nodeslist next ns"
assume no_in_ns: "no ∈ set ns"
assume while_inv: "∀no∈set ns.
repa no ≠ Null ∧
(if (repa ∝ low) no = (repa ∝ high) no ∧ high no ≠ Null
then repa no = (repa ∝ low) no
else repa no = hd [sn←ns . repNodes_eq sn no low high repa] ∧
repa (repa no) = repa no ∧
(∀no1∈set ns.
((repa ∝ high) no1 = (repa ∝ high) no ∧
(repa ∝ low) no1 = (repa ∝ low) no) =
(repa no = repa no1)))"
assume pre: "∀no∈set ns.
no ≠ Null ∧
(low no = Null) = (high no = Null) ∧
low no ∉ set ns ∧
high no ∉ set ns ∧
isLeaf_pt no low high = (var no ≤ Suc 0) ∧
(low no ≠ Null ⟶ rep (low no) ≠ Null) ∧ (rep ∝ low) no ∉ set ns"
assume same_var: "∀no1∈set ns. ∀no2∈set ns. var no1 = var no2"
assume share_case: "(repa ∝ low) no = (repa ∝ high) no ⟶ high no = Null"
assume unmodif: "∀no. no ∉ set ns ⟶ rep no = repa no"
show "hd [sn←ns . repNodes_eq sn no low high repa] ∈ set ns ∧
repa (hd [sn←ns . repNodes_eq sn no low high repa]) =
hd [sn←ns . repNodes_eq sn no low high repa]"
proof -
from no_in_ns pre obtain
no_nNull: " no ≠ Null" and
no_balanced: "(low no = Null) = (high no = Null)" and
isLeaf_var: "isLeaf_pt no low high = (var no ≤ Suc 0)"
by blast
have repNodes_eq_same_node: "repNodes_eq no no low high repa"
from no_in_ns have ns_nempty: "ns ≠ []"
by auto
from no_in_ns repNodes_eq_same_node
have repNodes_not_empty: "[sn←ns . repNodes_eq sn no low high repa] ≠ []"
by (rule filter_not_empty)
then have hd_term_in_ns: "hd [sn←ns . repNodes_eq sn no low high repa] ∈ set ns"
by (rule hd_filter_in_list)
with while_inv obtain
repa_hd_nNull: "repa  (hd [sn←ns . repNodes_eq sn no low high repa]) ≠ Null"
by auto
let ?hd = "hd [sn←ns . repNodes_eq sn no low high repa]"
from hd_term_in_ns  pre obtain
hd_nNull: " ?hd ≠ Null" and
hd_balanced:
"(low (hd [sn←ns . repNodes_eq sn no low high repa]) = Null) =
(high (hd [sn←ns . repNodes_eq sn no low high repa]) = Null)" and
hd_isLeaf_var:
"isLeaf_pt (hd [sn←ns . repNodes_eq sn no low high repa]) low high =
(var (hd [sn←ns . repNodes_eq sn no low high repa]) ≤ Suc 0)"
by blast
have "repa (hd [sn←ns . repNodes_eq sn no low high repa]) =
hd [sn←ns . repNodes_eq sn no low high repa]"
proof (cases "high no = Null")
case True
with no_balanced have "low no = Null"
by simp
with True have no_Leaf: "isLeaf_pt no low high"
with isLeaf_var have varno: "var no <= 1"
by simp
from same_var [rule_format, OF no_in_ns hd_term_in_ns] varno
have "var (hd [sn←ns . repNodes_eq sn no low high repa]) ≤ 1"
by simp
with hd_isLeaf_var have
"isLeaf_pt (hd [sn←ns . repNodes_eq sn no low high repa]) low high"
by simp
with while_inv hd_term_in_ns repNodes_not_empty show ?thesis
apply (erule_tac x=
"hd [sn←ns . repNodes_eq sn no low high repa]" in ballE)
prefer 2
apply simp
apply (rule filter_hd_P_rep_indep)
apply   (simp (no_asm_simp))
apply  (simp (no_asm_simp))
apply assumption
done
next
assume hno_nNull:  "high no ≠ Null"
with share_case have repchildren_neq: "(repa ∝ low) no ≠ (repa ∝ high) no"
by simp
from repNodes_not_empty have
"repNodes_eq  (hd [sn←ns . repNodes_eq sn no low high repa]) no low high repa"
by (rule hd_filter_prop)
then
have "(repa ∝ low) (hd [sn←ns . repNodes_eq sn no low high repa]) =
(repa ∝ low) no ∧
(repa ∝ high) (hd [sn←ns . repNodes_eq sn no low high repa]) =
(repa ∝ high) no"
with repchildren_neq have
"(repa ∝ low) (hd [sn←ns . repNodes_eq sn no low high repa])
≠ (repa ∝ high) (hd [sn←ns . repNodes_eq sn no low high repa])"
by simp
with while_inv hd_term_in_ns repNodes_not_empty show ?thesis
apply (erule_tac x=
"hd [sn←ns . repNodes_eq sn no low high repa]" in ballE)
prefer 2
apply simp
apply (rule filter_hd_P_rep_indep)
apply simp
apply fastforce
apply fastforce
done
qed
with hd_term_in_ns
show ?thesis
by simp
qed
next
(* invariant to invariant, THEN part  --  REDUCING*)
fix var low high rep nodeslist repa "next" node prx sfx
assume ns: "List nodeslist next (prx @ node # sfx)"
assume sfx: "List (next node) next sfx"
assume node_not_Null: "node ≠ Null"
assume nodes_balanced_ordered: "∀no∈set (prx @ node # sfx).
no ≠ Null ∧
(low no = Null) = (high no = Null) ∧
low no ∉ set (prx @ node # sfx) ∧
high no ∉ set (prx @ node # sfx) ∧
isLeaf_pt no low high = (var no ≤ (1::nat)) ∧
(low no ≠ Null ⟶ rep (low no) ≠ Null) ∧
(rep ∝ low) no ∉ set (prx @ node # sfx)"
assume all_nodes_same_var: "∀no1∈set (prx @ node # sfx).
∀no2∈set (prx @ node # sfx). var no1 = var no2"
assume rep_repa_nc: "∀no. no ∉ set prx ⟶ rep no = repa no"
assume while_inv: "∀no∈set prx.
repa no ≠ Null ∧
(if (repa ∝ low) no = (repa ∝ high) no ∧ low no ≠ Null
then repa no = (repa ∝ low) no
else repa no = hd [sn←prx . repNodes_eq sn no low high repa] ∧
repa (repa no) = repa no ∧
(∀no1∈set prx.
((repa ∝ high) no1 = (repa ∝ high) no ∧
(repa ∝ low) no1 = (repa ∝ low) no) =
(repa no = repa no1)))"
assume not_Leaf: "¬ isLeaf_pt node low high"
assume repchildren_eq_nln: "repa (low node) = repa (high node)"
show "(∀no. no ∉ set (prx @ [node]) ⟶
rep no = (repa(node := repa (high node))) no) ∧
(∀no∈set (prx @ [node]).
(repa(node := repa (high node))) no ≠ Null ∧
(if (repa(node := repa (high node)) ∝ low) no =
(repa(node := repa (high node)) ∝ high) no ∧
low no ≠ Null
then (repa(node := repa (high node))) no =
(repa(node := repa (high node)) ∝ low) no
else (repa(node := repa (high node))) no =
hd [sn←prx @ [node] .
repNodes_eq sn no low high
(repa(node := repa (high node)))] ∧
(repa(node := repa (high node)))
((repa(node := repa (high node))) no) =
(repa(node := repa (high node))) no ∧
(∀no1∈set (prx @ [node]).
((repa(node := repa (high node)) ∝ high) no1 =
(repa(node := repa (high node)) ∝ high) no ∧
(repa(node := repa (high node)) ∝ low) no1 =
(repa(node := repa (high node)) ∝ low) no) =
((repa(node := repa (high node))) no =
(repa(node := repa (high node))) no1))))"
(is "?NodesUnmodif ∧ ?NodesModif")
proof -
― ‹This proof was originally conducted without the
substitution @{term "repa (low node) = repa (high node)"} preformed.
So don't be confused if we show everythin for @{text "repa (low node)"}.›
from rep_repa_nc
have nodes_unmodif: ?NodesUnmodif
by auto
hence rep_Sucna_nc:
"(∀no. no ∉ set (prx @ [node])
⟶ rep no = (repa(node := repa (low (node )))) no)"
by auto
have nodes_modif: ?NodesModif (is "∀no∈set (prx @ [node]). ?P no ∧ ?Q no")
proof (rule ballI)
fix no
assume no_in_take_Sucna: " no ∈ set (prx @ [node])"
show "?P no ∧ ?Q no"
proof (cases "no = node")
case False
note no_noteq_nln=this
with no_in_take_Sucna
have no_in_take_n: "no ∈ set prx"
by auto
with no_in_take_n while_inv obtain
repa_no_nNull: " repa no ≠ Null" and
repa_cases: "(if (repa ∝ low) no = (repa ∝ high) no ∧ low no ≠ Null
then repa no = (repa ∝ low) no
else  repa no = hd [sn←prx . repNodes_eq sn no low high repa]
∧ repa (repa no) = repa no ∧
(∀no1∈set prx. ((repa ∝ high) no1 = (repa ∝ high) no
∧ (repa ∝ low) no1 = (repa ∝ low) no)
= (repa no = repa no1)))"
using [[simp_depth_limit = 2]]
by auto
from no_in_take_n
have no_in_nodeslist: "no ∈ set (prx @ node # sfx)"
by auto
from repa_no_nNull no_noteq_nln have ext_repa_nNull: "?P no"
by auto
from no_in_nodeslist nodes_balanced_ordered obtain
nln_nNull: "node ≠ Null" and
nln_balanced_children: "(low node = Null) = (high node = Null)" and
lnln_notin_nodeslist: "low node ∉ set (prx @ node # sfx)" and
hnln_notin_nodeslist: "high node ∉ set (prx @ node # sfx)" and
isLeaf_var_nln: "isLeaf_pt node low high = (var node ≤ 1)" and
node_nNull_rap_nNull_nln: "(low node ≠ Null
⟶ rep (low node) ≠ Null)" and
nln_varrep_le_var: "(rep ∝ low) node ∉ set (prx @ node # sfx)"
apply (erule_tac x="node" in ballE)
apply auto
done
from  no_in_nodeslist nodes_balanced_ordered no_in_take_Sucna
obtain
no_nNull: "no ≠ Null" and
balanced_children: "(low no = Null) = (high no = Null)" and
lno_notin_nodeslist: "low no ∉ set (prx @ node # sfx)" and
hno_notin_nodeslist: "high no ∉ set (prx @ node # sfx)" and
isLeaf_var_no: "isLeaf_pt no low high = (var no ≤ 1)" and
node_nNull_rep_nNull: "(low no ≠ Null ⟶ rep (low no) ≠ Null)" and
varrep_le_var: "(rep ∝ low) no ∉ set (prx @ node # sfx)"
apply -
apply (erule_tac x=no in ballE)
apply auto
done
from lno_notin_nodeslist
have ext_rep_null_comp_low:
"(repa (node := repa (low node)) ∝ low) no = (repa ∝ low) no"
from hno_notin_nodeslist
have ext_rep_null_comp_high:
"(repa (node := repa (low node)) ∝ high) no = (repa ∝ high) no"
have share_reduce_if: "?Q no"
proof (cases "(repa (node := repa (low node)) ∝ low) no =
(repa(node := repa (low node)) ∝ high) no ∧ low no ≠ Null")
case True
then obtain
red_case: "(repa (node := repa (low node)) ∝ low) no =
(repa(node := repa (low node)) ∝ high) no" and
lno_nNull: "low no ≠ Null"
by simp
from lno_nNull balanced_children have hno_nNull: "high no ≠ Null"
by simp
from True ext_rep_null_comp_low ext_rep_null_comp_high
have repchildren_eq_no: "(repa ∝ low) no = (repa ∝ high) no"
by simp
with repa_cases lno_nNull have "repa no = (repa ∝ low`