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 t⇩1 t⇩2 = (t⇩1 = t⇩2 ∨ subdag t⇩1 t⇩2)"
(*"subtree_eq Tip t = (if t = Tip then True else False)"
"subtree_eq (Node l a r) t = (t=(Node l a r) ∨ subtree_eq l t ∨ subtree_eq r t)"*)

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

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

datatype bdt = Zero | One | Bdt_Node bdt nat bdt

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

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

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

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

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

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

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

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


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

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

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


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

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

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

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


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

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

lemma dag_setof_exD: "⟦Dag p low high t; n ∈ set_of t⟧ ⟹ ∃ nt. Dag n low high nt"
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)" for not
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)" for not
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" for not
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 bdt⇩1 bdt⇩2 = (eval bdt⇩1 = eval bdt⇩2)"

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 st⇩1 st⇩2 var =
    (∀bdt⇩1 bdt⇩2. (bdt st⇩1 var = Some bdt⇩1 ∧ bdt st⇩2 var = Some bdt⇩2 ∧ (bdt⇩1 = bdt⇩2))
                 ⟶ st⇩1 = st⇩2)"

lemma isomorphic_dags_eq_sym: "isomorphic_dags_eq st⇩1 st⇩2 var = isomorphic_dags_eq st⇩2 st⇩1  var"
  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 = (∀st⇩1 st⇩2. (st⇩1 <= t ∧ st⇩2 <= t) ⟶ isomorphic_dags_eq st⇩1 st⇩2 var)"

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

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


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

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


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

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

lemma nodes_in_wf_ll: 
"⟦wf_ll pret levellista var; i < length levellista;  no ∈ set (levellista ! i)⟧ 
 ⟹ var no = i ∧ no ∈ set_of pret"
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" for not
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 "p≠Null" by (cases t) auto
  with t_subset_Nodes t_dag have "p ∈ Nodes (Suc nb) levellista" 
    by (cases t) auto
  with t_dag show ?thesis
    by auto
qed

  


lemma subdag_dag: 
"⋀ p. ⟦Dag p low high t; st <= t⟧ ⟹ ∃ stp. Dag stp low high st"
proof (induct t)
  case Tip
  then show ?case
    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); x≠xs!n; n < length xs⟧ ⟹ x ∈ set (take n xs)"     
apply (induct xs)
apply  simp
apply (case_tac n)
apply  simp
using [[simp_depth_limit=2]]
apply fastforce
done

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

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

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


end