Session BDD

Theory BinDag

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

(*  
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
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.

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  ts"
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"
  by (simp add: le_dag_def)

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
      by (simp add: le_dag_def)
  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)"
  by (simp add: less_dag_def)

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)" 
  by (simp add: less_dag_def)

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" 
    by (simp add: less_dag_Node)
  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"
    by (simp add: less_dag_Node')
  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]: 
  "pNull  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. pNull  ¬ 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 "pNull  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. pNull  ¬ 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
      by (simp add: subdag_neq)
  }
  ultimately show ?thesis
    by (auto simp add: in_set_of_decomp)
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
      by (simp add: subdag_neq)
  }
  ultimately show ?thesis
    by (auto simp add: in_set_of_decomp)
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; xset_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; xset_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 (simp add: isDag_def dag_def)
  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"
  by (simp add: Dag_conv_isDag_dag)

end

Theory General

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

(*  
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
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.

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 t1 t2 = (t1 = t2  subdag t1 t2)"
(*"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 v1 r) v2 Tip) = False"
| "isLeaf (Node Tip v1 (Node l v2 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  (refnat)  bool" where
"ordered Tip = (λ var. True)"
| "ordered (Node (Node l1 v1 r1) v (Node l2 v2 r2)) = 
    (λ var. (var v1 < var v  var v2 < var v)  
        (ordered (Node l1 v1 r1) var)  (ordered (Node l2 v2 r2) 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"
apply (simp add: dag_setofD)
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"
apply (simp add: dag_setofD)
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
apply (simp add: le_dag_def less_dag_def)
apply (simp add: le_dag_def less_dag_def)
apply (simp add: le_dag_def less_dag_def)
apply (simp add: le_dag_def less_dag_def)
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
apply (simp add: le_dag_def less_dag_def)
apply (simp add: le_dag_def less_dag_def)
apply (simp add: le_dag_def less_dag_def)
apply (simp add: le_dag_def less_dag_def)
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 (simp add: less_dag_def le_dag_def)
      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 bdt1 bdt2 = (eval bdt1 = eval bdt2)"

lemma cong_eval_sym: "l  r = r  l"
  by (auto simp add: cong_eval_def)

lemma cong_eval_trans: " l  r; r  t  l  t"
  by (simp add: cong_eval_def)

lemma cong_eval_child_high: " l  r  r  (Bdt_Node l v r)"
  apply (simp add: cong_eval_def )
  apply (rule ext)
  apply auto
  done

lemma cong_eval_child_low: " l  r  l  (Bdt_Node l v r)"
  apply (simp add: cong_eval_def )
  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)"
  by (simp add: null_comp_def)

lemma id_trans: "(a  id) (b (c p)) = (a  b) (c p)"
  by (simp add: null_comp_def)

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 st1 st2 var =
    (bdt1 bdt2. (bdt st1 var = Some bdt1  bdt st2 var = Some bdt2  (bdt1 = bdt2))
                  st1 = st2)"

lemma isomorphic_dags_eq_sym: "isomorphic_dags_eq st1 st2 var = isomorphic_dags_eq st2 st1  var"
  by (auto simp add: isomorphic_dags_eq_def)


(*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 = (st1 st2. (st1 <= t  st2 <= t)  isomorphic_dags_eq st1 st2 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); ij 
   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"
apply (simp add: wf_ll_def)
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 (simp add: wf_ll_def)
    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 
    apply (simp add: Nodes_def)
    apply (simp add: set_split)
    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" 
      by (simp add: less_dag_Node)
    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)))" 
      by (simp add: wf_ll_def)
    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)))" 
      by (simp add: wf_ll_def)
    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 
      by (simp add: null_comp_def)
  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"
      by (simp add: null_comp_def)
    from lowxNull have repblowNull: "(repb  low) x = Null"
      by (simp add: null_comp_def)
    with repclowNull have lowxrepbc: "(repc  low) x = (repb  low) x"
      by simp
    from highxNull have repchighNull: "(repc  high) x = Null"
      by (simp add: null_comp_def)
    from highxNull have "(repb  high) x = Null"
      by (simp add: null_comp_def)
    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 (simp add: wf_ll_def Nodes_def)
  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"
  apply (simp add: Nodes_def)
  apply (simp add: set_split)
  done

lemma Nodes_levellist: 
" wf_ll pret levellista var; nb < length levellista; p  Nodes nb levellista 
  p  set (levellista ! nb)"
  apply (simp add: Nodes_def) 
  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 (simp add: Nodes_def wf_ll_def)
  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 "pNull" 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
    by (simp add: less_dag_def le_dag_def)
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"
      by (auto simp add:le_dag_def less_dag_def)
    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"
    by (simp add: le_dag_set_of)
  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 (simp add: wf_ll_def Nodes_def)
    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 (simp add: Nodes_def)
        apply (simp add: Nodes_def)
        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"
            by (simp add: wf_ll_def)
          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"
            by (auto simp add: Nodes_def)
          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))" 
            by (auto simp add: wf_ll_def) 
          with varx_snb have "x  Nodes nb levellista" 
            by (auto simp add: Nodes_def) 
          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 (simp add: isLeaf_pt_def)
    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))))"
  by (simp add: repNodes_eq_def null_comp_def)


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); xxs!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
    License:     LGPL
*)

(*  
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
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.

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
    License:     LPGL
*)

(*  
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
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.

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
    License:     LGPL
*)

(*
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
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.

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; pNull 
    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"
  by (simp add: dag_def)

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

lemma first_simps [simp]:
 "first [] = Null"
 "first (r#rs) = r"
by (simp_all add: first_def)

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

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

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


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

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

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


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


lemma (in Levellist_impl) Levellist_spec_total':
shows "ll σ t. Γ,Θt
        σ. Dag ´p ´low ´high t  (´p  Null  (´p´var) < length ´levellist) 
             ordered t ´var  Levellist ´levellist ´next ll 
             (n  set_of t.
              (if ´mark n = ´m
               then n  set (ll ! ´var n) 
                    (nt p. Dag n ´low ´high nt  p  set_of nt
                      ´mark p = ´m)
               else n  set (concat ll)))
          ´levellist :== PROC Levellist (´p, ´m, ´levellist)
       ll'. Levellist ´levellist ´next ll'  wf_levellist t ll ll' σvar 
        wf_marking t  σmark ´mark σm 
        (p. p  set_of t  σnext p = ´next p)
        "
apply (hoare_rule HoareTotal.ProcRec1
           [where r="measure (λ(s,p). size (dag sp slow shigh))"])
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"
    by (simp add: Levellist_length)
  assume orderedt: "ordered (Node lt p rt) var"
  show "(low p  Null  var (low p) < length levellist) 
          ordered lt var 
          (n  set_of lt.
              if mark n = m
              then n  set (ll ! var n) 
                   (nt p. Dag n low high nt  p  set_of nt  mark p = m)
              else n  set (concat ll)) 
          size (dag (low p) low high) < size (dag p low high) 
          (marka nexta levellist lla.
              Levellist levellist nexta lla 
              wf_levellist lt ll lla var  wf_marking lt mark marka m 
              (p. p  set_of lt  next p = nexta p)
              (high p  Null  var (high p) < length levellist) 
              ordered rt var 
              (lla. Levellist levellist nexta lla 
                     (n  set_of rt.
                        if marka n = m
                        then n  set (lla ! var n) 
                             (nt p. Dag n low high nt  p  set_of nt 
                                    marka p = m)
                        else n  set (concat lla)) 
                     size (dag (high p) low high) < size (dag p low high) 
                     (markb nextb levellist llb.
                         Levellist levellist nextb llb 
                         wf_levellist rt lla llb var 
                         wf_marking rt marka markb m 
                         (p. p  set_of rt  nexta p = nextb p) 
                         (ll'. Levellist (levellist[var p := p])
                                 (nextb(p := levellist ! var p)) ll' 
                                wf_levellist (Node lt p rt) ll ll' var 
                                wf_marking (Node lt p rt) mark (markb(p := m)) m 
                                (pa. pa  set_of (Node lt p rt) 
                                      next pa =
                                      (if pa = p then levellist ! var p
                                       else nextb pa))))))"
  proof (cases "lt")
    case Tip
    note lt_Tip = this
    show ?thesis
    proof (cases "rt")
      case Tip
      show ?thesis
        using size_rt_dec Tip lt_Tip Tip lt rt
        apply clarsimp
        subgoal premises prems for marka nexta levellista lla markb nextb levellistb llb
        proof -
          have lla: "Levellist levellista nexta lla" by fact
          have llb: "Levellist levellistb nextb llb" by fact
          have wfll_lt: "wf_levellist Tip ll lla var"
                        "wf_marking Tip mark marka m" by fact+

          then have ll_lla: "ll = lla"
            by (simp add: wf_levellist_def)

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

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

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

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

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

end

Theory ShareRepProof

(*  Title:       BDD

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

(*  
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
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.

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:  "noset 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 [snns . repNodes_eq sn p low high rep] 
        var nodeslist = var p"
  proof -
    from p_in_ns no_prop have p_not_Null: "pNull"
      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
      "nodeslistNull"
      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::"refnat" 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: "noset (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: "(ptset prx. repNodes_eq pt p low high rep) 
                       repa p = hd [snprx . repNodes_eq sn p low high rep] 
                      (pt. pt  p  rep pt = repa pt)"
  show "repa p = hd [snprx @ 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: "(ptset prx. repNodes_eq pt p low high rep)"
      apply -
      apply (rule_tac x=p in bexI)
      apply  (simp add: repNodes_eq_def)
      apply simp
      done
    hence not_empty: "[snprx . 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 [snprx . 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: "noset 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: "(ptset prx. repNodes_eq pt p low high repa) 
            repa p = hd [snprx . repNodes_eq sn p low high repa]"
  assume nomatch_prx: "ptset 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 "(noset prx  set (nodeslist # sfx).
              no  Null  (low no = Null) = (high no = Null)  var no = var p) 
        ((ptset (prx @ [nodeslist]). repNodes_eq pt p low high repa) 
           repa p = hd [snprx @ [nodeslist] . repNodes_eq sn p low high repa]) 
        (next nodeslist  Null 
            (ptset (prx @ [nodeslist]). ¬ repNodes_eq pt p low high repa))"
  proof -
    from nomatch_prx nomatch_nodeslist
    have "((ptset (prx @ [nodeslist]). repNodes_eq pt p low high repa) 
           repa p = hd [snprx @ [nodeslist] . repNodes_eq sn p low high repa])" 
      by auto
    moreover
    from nomatch_prx nomatch_nodeslist
    have "(next nodeslist  Null 
            (ptset (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: "noset 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: "(ptset prx. repNodes_eq pt p low high repa) 
        repa p = hd [snprx . repNodes_eq sn p low high repa]"
  assume nomatch_prx: "ptset prx. ¬ repNodes_eq pt p low high repa"
  assume match: "repNodes_eq nodeslist p low high repa"
  show "(noset 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) 
        ((ptset prx  set sfx. repNodes_eq pt p low high repa) 
           nodeslist =
           hd ([snprx . repNodes_eq sn p low high repa] @
               [snsfx . repNodes_eq sn p low high repa])) 
        ((ptset 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 ([snprx . repNodes_eq sn p low high repa] @
               [snsfx . repNodes_eq sn p low high repa]) = nodeslist"
      by simp
    from match sfx'
    have triv: "((ptset 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  (simp add: hd)
      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
    License:     LGPL
*)

(*  
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
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.

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. no1var = no2var))"
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    (simp add: isLeaf_pt_def )
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: "noset ns.
           repa no  Null 
           (if (repa  low) no = (repa  high) no  high no  Null
            then repa no = (repa  low) no
            else repa no = hd [snns . repNodes_eq sn no low high repa] 
                 repa (repa no) = repa no 
                 (no1set ns.
                     ((repa  high) no1 = (repa  high) no 
                      (repa  low) no1 = (repa  low) no) =
                     (repa no = repa no1)))"
  assume pre: "noset 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: "no1set ns. no2set 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 [snns . repNodes_eq sn no low high repa]  set ns 
        repa (hd [snns . repNodes_eq sn no low high repa]) =
        hd [snns . 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"
      by (simp add: repNodes_eq_def)
    from no_in_ns have ns_nempty: "ns  []"
      by auto
    from no_in_ns repNodes_eq_same_node 
    have repNodes_not_empty: "[snns . repNodes_eq sn no low high repa]  []"
      by (rule filter_not_empty)
    then have hd_term_in_ns: "hd [snns . repNodes_eq sn no low high repa]  set ns"
      by (rule hd_filter_in_list)
    with while_inv obtain 
      repa_hd_nNull: "repa  (hd [snns . repNodes_eq sn no low high repa])  Null"
      by auto
    let ?hd = "hd [snns . repNodes_eq sn no low high repa]"
    from hd_term_in_ns  pre obtain
      hd_nNull: " ?hd  Null" and
      hd_balanced: 
        "(low (hd [snns . repNodes_eq sn no low high repa]) = Null) = 
         (high (hd [snns . repNodes_eq sn no low high repa]) = Null)" and
      hd_isLeaf_var: 
      "isLeaf_pt (hd [snns . repNodes_eq sn no low high repa]) low high = 
      (var (hd [snns . repNodes_eq sn no low high repa])  Suc 0)"
      by blast
    have "repa (hd [snns . repNodes_eq sn no low high repa]) = 
      hd [snns . 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"
        by (simp add: isLeaf_pt_def)
      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 [snns . repNodes_eq sn no low high repa])  1"
        by simp
      with hd_isLeaf_var have 
        "isLeaf_pt (hd [snns . repNodes_eq sn no low high repa]) low high"
        by simp
      with while_inv hd_term_in_ns repNodes_not_empty show ?thesis
        apply (simp add: isLeaf_pt_def)
        apply (erule_tac x=
          "hd [snns . repNodes_eq sn no low high repa]" in ballE)
        prefer 2
        apply simp
        apply (simp (no_asm_use) add: repNodes_eq_def)
        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 [snns . repNodes_eq sn no low high repa]) no low high repa"
        by (rule hd_filter_prop)
      then 
      have "(repa  low) (hd [snns . repNodes_eq sn no low high repa]) = 
              (repa  low) no  
            (repa  high) (hd [snns . repNodes_eq sn no low high repa]) = 
              (repa  high) no"
        by (simp add: repNodes_eq_def)
      with repchildren_neq have 
        "(repa  low) (hd [snns . repNodes_eq sn no low high repa])
         (repa  high) (hd [snns . repNodes_eq sn no low high repa])"
        by simp
      with while_inv hd_term_in_ns repNodes_not_empty show ?thesis
        apply (simp add: isLeaf_pt_def)
        apply (erule_tac x=
          "hd [snns . repNodes_eq sn no low high repa]" in ballE)
        prefer 2
        apply simp
        apply (simp (no_asm_use) add: repNodes_eq_def)
        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: "noset (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: "no1set (prx @ node # sfx).
           no2set (prx @ node # sfx). var no1 = var no2"
  assume rep_repa_nc: "no. no  set prx  rep no = repa no"
  assume while_inv: "noset prx.
           repa no  Null 
           (if (repa  low) no = (repa  high) no  low no  Null
            then repa no = (repa  low) no
            else repa no = hd [snprx . repNodes_eq sn no low high repa] 
                 repa (repa no) = repa no 
                 (no1set 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) 
        (noset (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 [snprx @ [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 
                    (no1set (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 "noset (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 [snprx . repNodes_eq sn no low high repa] 
           repa (repa no) = repa no  
          (no1set 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"
          by (auto simp add: null_comp_def)
        from hno_notin_nodeslist 
        have ext_rep_null_comp_high: 
          "(repa (node := repa (low node))  high) no = (repa  high) no"
          by (auto simp add: null_comp_def)
        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