Theory WordInterval

(*  Title:      WordInterval.thy
    Authors:    Julius Michaelis, Cornelius Diekmann
*)
theory WordInterval
  imports
  Main
  "Word_Lib.Word_Lemmas"
  "Word_Lib.Next_and_Prev"
begin

section‹WordInterval: Executable datatype for Machine Word Sets›
text‹Stores ranges of machine words as interval. This has been proven quite efficient for
     IP Addresses.›
(*NOTE: All algorithms here use a straight-forward implementation. There is a lot of room for
        improving the computation complexity, for example by making the WordInterval a balanced,
        sorted tree.*)

subsection‹Syntax›
context
  notes [[typedef_overloaded]]
begin
  datatype ('a::len) wordinterval = WordInterval
                                        "('a::len) word" ― ‹start (inclusive)›
                                        "('a::len) word" ― ‹end (inclusive)›
                                  | RangeUnion "'a wordinterval" "'a wordinterval"
end

subsection‹Semantics›
  fun wordinterval_to_set :: "'a::len wordinterval  ('a::len word) set"
  where
    "wordinterval_to_set (WordInterval start end) =
        {start .. end}" |
    "wordinterval_to_set (RangeUnion r1 r2) =
        wordinterval_to_set r1  wordinterval_to_set r2"

(*Note: The runtime of all the operations could be improved, for example by keeping the tree sorted
  and balanced.*)

subsection‹Basic operations›
  text∈›
  fun wordinterval_element :: "'a::len word  'a::len wordinterval  bool" where
    "wordinterval_element el (WordInterval s e)  s  el  el  e" |
    "wordinterval_element el (RangeUnion r1 r2) 
                                            wordinterval_element el r1  wordinterval_element el r2"
  lemma wordinterval_element_set_eq[simp]:
    "wordinterval_element el rg = (el  wordinterval_to_set rg)"
    by(induction rg rule: wordinterval_element.induct) simp_all

  definition wordinterval_union
    :: "'a::len wordinterval  'a::len wordinterval  'a::len wordinterval" where
    "wordinterval_union r1 r2 = RangeUnion r1 r2"
  lemma wordinterval_union_set_eq[simp]:
    "wordinterval_to_set (wordinterval_union r1 r2) = wordinterval_to_set r1  wordinterval_to_set r2"
    unfolding wordinterval_union_def by simp

  fun wordinterval_empty :: "'a::len wordinterval  bool" where
    "wordinterval_empty (WordInterval s e)  e < s" |
    "wordinterval_empty (RangeUnion r1 r2)  wordinterval_empty r1  wordinterval_empty r2"
  lemma wordinterval_empty_set_eq[simp]: "wordinterval_empty r  wordinterval_to_set r = {}"
    by(induction r) auto

  definition Empty_WordInterval :: "'a::len wordinterval" where
    "Empty_WordInterval  WordInterval 1 0"
  lemma wordinterval_empty_Empty_WordInterval: "wordinterval_empty Empty_WordInterval"
    by(simp add: Empty_WordInterval_def)
  lemma Empty_WordInterval_set_eq[simp]: "wordinterval_to_set Empty_WordInterval = {}"
    by(simp add: Empty_WordInterval_def)



subsection‹WordInterval and Lists›
  text‹A list of (start, end)› tuples.›

  text‹wordinterval to list›
  fun wi2l :: "'a::len wordinterval  ('a::len word × 'a::len word) list" where
    "wi2l (RangeUnion r1 r2) = wi2l r1 @ wi2l r2" |
    "wi2l (WordInterval s e) = (if e < s then [] else [(s,e)])"

  text‹list to wordinterval›
  fun l2wi :: "('a::len word × 'a word) list  'a wordinterval" where
    "l2wi [] = Empty_WordInterval" |
    "l2wi [(s,e)] = (WordInterval s e)" |
    "l2wi ((s,e)#rs) = (RangeUnion (WordInterval s e) (l2wi rs))"


  lemma l2wi_append: "wordinterval_to_set (l2wi (l1@l2)) =
                      wordinterval_to_set (l2wi l1)  wordinterval_to_set (l2wi l2)"
    proof(induction l1 arbitrary: l2 rule:l2wi.induct)
    case 1 thus ?case by simp
    next
    case (2 s e l2) thus ?case by (cases l2) simp_all
    next
    case 3 thus ?case by force
    qed

  lemma l2wi_wi2l[simp]: "wordinterval_to_set (l2wi (wi2l r)) = wordinterval_to_set r"
    by(induction r) (simp_all add: l2wi_append)

  lemma l2wi: "wordinterval_to_set (l2wi l) = ( (i,j)  set l. {i .. j})"
    by(induction l rule: l2wi.induct, simp_all)

  lemma wi2l: "((i,j)set (wi2l r). {i .. j}) = wordinterval_to_set r"
    by(induction r rule: wi2l.induct, simp_all)

  lemma l2wi_remdups[simp]: "wordinterval_to_set (l2wi (remdups ls)) = wordinterval_to_set (l2wi ls)"
    by(simp add: l2wi)

  lemma wi2l_empty[simp]: "wi2l Empty_WordInterval = []"
    unfolding Empty_WordInterval_def
    by simp


subsection‹Optimizing and minimizing @{typ "('a::len) wordinterval"}s›
text‹Removing empty intervals›
context
begin
  fun wordinterval_optimize_empty :: "'a::len wordinterval  'a wordinterval" where
    "wordinterval_optimize_empty (RangeUnion r1 r2) = (let r1o = wordinterval_optimize_empty r1;
                                                           r2o = wordinterval_optimize_empty r2
      in if
        wordinterval_empty r1o
      then
        r2o
      else if
        wordinterval_empty r2o
      then
        r1o
      else
        RangeUnion r1o r2o)" |
    "wordinterval_optimize_empty r = r"
  lemma wordinterval_optimize_empty_set_eq[simp]:
    "wordinterval_to_set (wordinterval_optimize_empty r) = wordinterval_to_set r"
    by(induction r) (simp_all add: Let_def)

  lemma wordinterval_optimize_empty_double:
    "wordinterval_optimize_empty (wordinterval_optimize_empty r) = wordinterval_optimize_empty r"
    by(induction r) (simp_all add: Let_def)

  private fun wordinterval_empty_shallow :: "'a::len wordinterval  bool"  where
    "wordinterval_empty_shallow (WordInterval s e)  e < s" |
    "wordinterval_empty_shallow (RangeUnion _ _)  False"
  private lemma helper_optimize_shallow:
    "wordinterval_empty_shallow (wordinterval_optimize_empty r) =
      wordinterval_empty (wordinterval_optimize_empty r)"
    by(induction r) fastforce+
  private fun wordinterval_optimize_empty2 where
    "wordinterval_optimize_empty2 (RangeUnion r1 r2) = (let r1o = wordinterval_optimize_empty r1;
                                                            r2o = wordinterval_optimize_empty r2
      in if
        wordinterval_empty_shallow r1o
      then
        r2o
      else if
        wordinterval_empty_shallow r2o
      then
        r1o
      else
        RangeUnion r1o r2o)" |
    "wordinterval_optimize_empty2 r = r"
  lemma wordinterval_optimize_empty_code[code_unfold]:
    "wordinterval_optimize_empty = wordinterval_optimize_empty2"
    by (subst fun_eq_iff, clarify, rename_tac r, induct_tac r)
       (unfold wordinterval_optimize_empty.simps wordinterval_optimize_empty2.simps
               Let_def helper_optimize_shallow, simp_all)
end



text‹Merging overlapping intervals›
context
begin

  private definition disjoint :: "'a set  'a set  bool" where
    "disjoint A B  A  B = {}"

  private primrec interval_of :: "('a::len) word × 'a word  'a word set" where
    "interval_of (s,e) = {s .. e}"
  declare interval_of.simps[simp del]

  private definition disjoint_intervals
    :: "(('a::len) word × ('a::len) word)  ('a word × 'a word)  bool"
  where
    "disjoint_intervals A B  disjoint (interval_of A) (interval_of B)"

  private definition not_disjoint_intervals
    :: "(('a::len) word × ('a::len) word)  ('a word × 'a word)  bool"
  where
    "not_disjoint_intervals A B  ¬ disjoint (interval_of A) (interval_of B)"

  private lemma [code]:
    "not_disjoint_intervals A B =
      (case A of (s,e)  case B of (s',e')  s  e'  s'  e  s  e  s'  e')"
    apply(cases A, cases B)
    apply(simp add: not_disjoint_intervals_def interval_of.simps disjoint_def)
    done

  private lemma [code]:
    "disjoint_intervals A B =
      (case A of (s,e)  case B of (s',e')  s > e'  s' > e  s > e  s' > e')"
    apply(cases A, cases B)
    apply(simp add: disjoint_intervals_def interval_of.simps disjoint_def)
    by fastforce


  text‹BEGIN merging overlapping intervals›
  (*result has no empty intervals and all are disjoint.
    merging things such as [1,7] [8,10] would still be possible*)
  private fun merge_overlap
    :: "(('a::len) word × ('a::len) word)  ('a word × 'a word) list  ('a word × 'a word) list"
  where
    "merge_overlap s [] = [s]" |
    "merge_overlap (s,e) ((s',e')#ss) = (
       if not_disjoint_intervals (s,e) (s',e')
       then (min s s', max e e')#ss
       else (s',e')#merge_overlap (s,e) ss)"

  private lemma not_disjoint_union:
      fixes s :: "('a::len) word"
      shows "¬ disjoint {s..e} {s'..e'}  {s..e}  {s'..e'} = {min s s' .. max e e'}"
    by(auto simp add: disjoint_def min_def max_def)

  private lemma disjoint_subset: "disjoint A B  A  B  C  A  C"
    unfolding disjoint_def
    by blast

  private lemma merge_overlap_helper1: "interval_of A  (s  set ss. interval_of s) 
      (s  set (merge_overlap A ss). interval_of s) = (s  set ss. interval_of s)"
    apply(induction ss)
     apply(simp; fail)
    apply(rename_tac x xs)
    apply(cases A, rename_tac a b)
    apply(case_tac x)
    apply(simp add: not_disjoint_intervals_def interval_of.simps)
    apply(intro impI conjI)
     apply(drule not_disjoint_union)
     apply blast
    apply(drule_tac C="(xset xs. interval_of x)" in disjoint_subset)
     apply(simp_all)
    done

  private lemma merge_overlap_helper2: "s'set ss. ¬ disjoint (interval_of A) (interval_of s') 
          interval_of A  (s  set ss. interval_of s) = (s  set (merge_overlap A ss). interval_of s)"
    apply(induction ss)
     apply(simp; fail)
    apply(rename_tac x xs)
    apply(cases A, rename_tac a b)
    apply(case_tac x)
    apply(simp add: not_disjoint_intervals_def interval_of.simps)
    apply(intro impI conjI)
     apply(drule not_disjoint_union)
     apply blast
    apply(simp)
    by blast

  private lemma merge_overlap_length:
    "s'  set ss. ¬ disjoint (interval_of A) (interval_of s') 
      length (merge_overlap A ss) = length ss"
    apply(induction ss)
     apply(simp)
    apply(rename_tac x xs)
    apply(cases A, rename_tac a b)
    apply(case_tac x)
    apply(simp add: not_disjoint_intervals_def interval_of.simps)
    done

  lemma "merge_overlap (1:: 16 word,2) [(1, 7)] = [(1, 7)]" by eval
  lemma "merge_overlap (1:: 16 word,2) [(2, 7)] = [(1, 7)]" by eval
  lemma "merge_overlap (1:: 16 word,2) [(3, 7)] = [(3, 7), (1,2)]" by eval

  private function listwordinterval_compress
    :: "(('a::len) word × ('a::len) word) list  ('a word × 'a word) list" where
    "listwordinterval_compress [] = []" |
    "listwordinterval_compress (s#ss) = (
            if s'  set ss. disjoint_intervals s s'
            then s#listwordinterval_compress ss
            else listwordinterval_compress (merge_overlap s ss))"
  by(pat_completeness, auto)

  private termination listwordinterval_compress
  apply (relation "measure length")
    apply(rule wf_measure)
   apply(simp)
  using disjoint_intervals_def merge_overlap_length by fastforce

  private lemma listwordinterval_compress:
    "(s  set (listwordinterval_compress ss). interval_of s) = (s  set ss. interval_of s)"
    apply(induction ss rule: listwordinterval_compress.induct)
     apply(simp)
    apply(simp)
    apply(intro impI)
    apply(simp add: disjoint_intervals_def)
    apply(drule merge_overlap_helper2)
    apply(simp)
    done

  lemma "listwordinterval_compress [(1::32 word,3), (8,10), (2,5), (3,7)] = [(8, 10), (1, 7)]"
    by eval

  private lemma A_in_listwordinterval_compress: "A  set (listwordinterval_compress ss) 
    interval_of A  (s  set ss. interval_of s)"
    using listwordinterval_compress by blast

  private lemma listwordinterval_compress_disjoint:
    "A  set (listwordinterval_compress ss)  B  set (listwordinterval_compress ss) 
      A  B  disjoint (interval_of A) (interval_of B)"
    apply(induction ss arbitrary: rule: listwordinterval_compress.induct)
     apply(simp)
    apply(simp split: if_split_asm)
    apply(elim disjE)
       apply(simp_all)
     apply(simp_all add: disjoint_intervals_def disjoint_def)
     apply(blast dest: A_in_listwordinterval_compress)+
    done
  text‹END merging overlapping intervals›


  text‹BEGIN merging adjacent intervals›
  private fun merge_adjacent
    :: "(('a::len) word × ('a::len) word)  ('a word × 'a word) list  ('a word × 'a word) list"
  where
    "merge_adjacent s [] = [s]" |
    "merge_adjacent (s,e) ((s',e')#ss) = (
       if s e  s'  e'  word_next e = s'
       then (s, e')#ss
       else if s e  s'  e'  word_next e' = s
       then (s', e)#ss
       else (s',e')#merge_adjacent (s,e) ss)"

  private lemma merge_adjacent_helper:
  "interval_of A  (s  set ss. interval_of s) = (s  set (merge_adjacent A ss). interval_of s)"
    apply(induction ss)
     apply(simp; fail)
    apply(rename_tac x xs)
    apply(cases A, rename_tac a b)
    apply(case_tac x)
    apply(simp add:  interval_of.simps)
    apply(intro impI conjI)
       apply (metis Un_assoc word_adjacent_union)
      apply(elim conjE)
      apply(drule(2) word_adjacent_union)
      subgoal by (blast)
     subgoal by (metis word_adjacent_union Un_assoc)
    by blast

  private lemma merge_adjacent_length:
    "(s', e')set ss. s  e  s'  e'  (word_next e = s'  word_next e' = s)
      length (merge_adjacent (s,e) ss) = length ss"
    apply(induction ss)
     apply(simp)
    apply(rename_tac x xs)
    apply(case_tac x)
    apply simp
    by blast

  private function listwordinterval_adjacent
    :: "(('a::len) word × ('a::len) word) list  ('a word × 'a word) list" where
    "listwordinterval_adjacent [] = []" |
    "listwordinterval_adjacent ((s,e)#ss) = (
            if (s',e')  set ss. ¬ (s e  s'  e'  (word_next e = s'  word_next e' = s))
            then (s,e)#listwordinterval_adjacent ss
            else listwordinterval_adjacent (merge_adjacent (s,e) ss))"
  by(pat_completeness, auto)

  private termination listwordinterval_adjacent
  apply (relation "measure length")
    apply(rule wf_measure)
   apply(simp)
  apply(simp)
  using merge_adjacent_length by fastforce

  private lemma listwordinterval_adjacent:
    "(s  set (listwordinterval_adjacent ss). interval_of s) = (s  set ss. interval_of s)"
    apply(induction ss rule: listwordinterval_adjacent.induct)
     apply(simp)
    apply(simp add: merge_adjacent_helper)
    done

  lemma "listwordinterval_adjacent [(1::16 word, 3), (5, 10), (10,10), (4,4)] = [(10, 10), (1, 10)]"
    by eval
  text‹END merging adjacent intervals›


  definition wordinterval_compress :: "('a::len) wordinterval  'a wordinterval" where
    "wordinterval_compress r 
      l2wi (remdups (listwordinterval_adjacent (listwordinterval_compress
        (wi2l (wordinterval_optimize_empty r)))))"

  text‹Correctness: Compression preserves semantics›
  lemma wordinterval_compress:
    "wordinterval_to_set (wordinterval_compress r) = wordinterval_to_set r"
    unfolding wordinterval_compress_def
    proof -
      have interval_of': "interval_of s = (case s of (s,e)  {s .. e})" for s
        by (cases s) (simp add: interval_of.simps)

      have "wordinterval_to_set (l2wi (remdups (listwordinterval_adjacent
              (listwordinterval_compress (wi2l (wordinterval_optimize_empty r)))))) =
            (xset (listwordinterval_adjacent (listwordinterval_compress
                (wi2l (wordinterval_optimize_empty r)))). interval_of x)"
        by (force simp: interval_of' l2wi)
      also have " =  (sset (wi2l (wordinterval_optimize_empty r)). interval_of s)"
        by(simp add: listwordinterval_compress listwordinterval_adjacent)
      also have " = ((i, j)set (wi2l (wordinterval_optimize_empty r)). {i..j})"
        by(simp add: interval_of')
      also have " = wordinterval_to_set r" by(simp add: wi2l)
      finally show "wordinterval_to_set
        (l2wi (remdups (listwordinterval_adjacent (listwordinterval_compress
            (wi2l (wordinterval_optimize_empty r))))))
          = wordinterval_to_set r" .
  qed

end

text‹Example›
lemma "(wi2l  (wordinterval_compress :: 32 wordinterval  32 wordinterval)  l2wi)
          [(70, 80001), (0,0), (150, 8000), (1,3), (42,41), (3,7), (56, 200), (8,10)] =
          [(56, 80001), (0, 10)]" by eval

lemma "wordinterval_compress (RangeUnion (RangeUnion (WordInterval (1::32 word) 5)
                                                        (WordInterval 8 10)) (WordInterval 3 7)) =
       WordInterval 1 10" by eval



subsection‹Further operations›

  text⋃›
  definition wordinterval_Union :: "('a::len) wordinterval list  'a wordinterval" where
    "wordinterval_Union ws = wordinterval_compress (foldr wordinterval_union ws Empty_WordInterval)"

  lemma wordinterval_Union:
    "wordinterval_to_set (wordinterval_Union ws) = ( w  (set ws). wordinterval_to_set w)"
    by(induction ws) (simp_all add: wordinterval_compress wordinterval_Union_def)


context
begin
  private fun wordinterval_setminus'
    :: "'a::len wordinterval  'a wordinterval  'a wordinterval" where
    "wordinterval_setminus' (WordInterval s e) (WordInterval ms me) = (
      if s > e  ms > me then WordInterval s e else
      if me  e
        then
          WordInterval (if ms = 0 then 1 else s) (min e (word_prev ms))
        else if ms  s
        then
          WordInterval (max s (word_next me)) (if me = - 1 then 0 else e)
        else
          RangeUnion (WordInterval (if ms = 0 then 1 else s) (word_prev ms))
                     (WordInterval (word_next me) (if me = - 1 then 0 else e))
        )" |
     "wordinterval_setminus' (RangeUnion r1 r2) t =
        RangeUnion (wordinterval_setminus' r1 t) (wordinterval_setminus' r2 t)"|
     "wordinterval_setminus' t (RangeUnion r1 r2) =
        wordinterval_setminus' (wordinterval_setminus' t r1) r2"

  private lemma wordinterval_setminus'_rr_set_eq:
    "wordinterval_to_set(wordinterval_setminus' (WordInterval s e) (WordInterval ms me)) =
    wordinterval_to_set (WordInterval s e) - wordinterval_to_set (WordInterval ms me)"
     apply(simp only: wordinterval_setminus'.simps)
     apply(case_tac "e < s")
      apply simp
     apply(case_tac "me < ms")
      apply simp
     apply(case_tac [!] "e  me")
      apply(case_tac [!] "ms = 0")
        apply(case_tac [!] "ms  s")
            apply(case_tac [!] "me = - 1")
                    apply(simp_all add: word_next_unfold word_prev_unfold min_def max_def)
            apply(safe)
                                  apply(auto)
                          apply(uint_arith)
                         apply(uint_arith)
                        apply(uint_arith)
                       apply(uint_arith)
                      apply(uint_arith)
                     apply(uint_arith)
                    apply(uint_arith)
                   apply(uint_arith)
                  apply(uint_arith)
                 apply(uint_arith)
                apply(uint_arith)
               apply(uint_arith)
              apply(uint_arith)
             apply(uint_arith)
            apply(uint_arith)
           apply(uint_arith)
          apply(uint_arith)
         apply(uint_arith)
        apply(uint_arith)
       apply(uint_arith)
      apply(uint_arith)
     apply(uint_arith)
   done

  private lemma wordinterval_setminus'_set_eq:
    "wordinterval_to_set (wordinterval_setminus' r1 r2) =
      wordinterval_to_set r1 - wordinterval_to_set r2"
    apply(induction rule: wordinterval_setminus'.induct)
      using wordinterval_setminus'_rr_set_eq apply blast
     apply auto
    done
  lemma wordinterval_setminus'_empty_struct:
    "wordinterval_empty r2  wordinterval_setminus' r1 r2 = r1"
    by(induction r1 r2 rule: wordinterval_setminus'.induct) auto


  definition wordinterval_setminus
    :: "'a::len wordinterval  'a::len wordinterval  'a::len wordinterval" where
    "wordinterval_setminus r1 r2 = wordinterval_compress (wordinterval_setminus' r1 r2)"

  lemma wordinterval_setminus_set_eq[simp]: "wordinterval_to_set (wordinterval_setminus r1 r2) =
    wordinterval_to_set r1 - wordinterval_to_set r2"
    by(simp add: wordinterval_setminus_def wordinterval_compress wordinterval_setminus'_set_eq)
end

definition wordinterval_UNIV :: "'a::len wordinterval" where
  "wordinterval_UNIV  WordInterval 0 (- 1)"
lemma wordinterval_UNIV_set_eq[simp]: "wordinterval_to_set wordinterval_UNIV = UNIV"
  unfolding wordinterval_UNIV_def
  using max_word_max by fastforce

fun wordinterval_invert :: "'a::len wordinterval  'a::len wordinterval" where
  "wordinterval_invert r = wordinterval_setminus wordinterval_UNIV r"
lemma wordinterval_invert_set_eq[simp]:
  "wordinterval_to_set (wordinterval_invert r) = UNIV - wordinterval_to_set r" by(auto)

lemma wordinterval_invert_UNIV_empty:
  "wordinterval_empty (wordinterval_invert wordinterval_UNIV)" by simp

lemma wi2l_univ[simp]: "wi2l wordinterval_UNIV = [(0, - 1)]"
  unfolding wordinterval_UNIV_def
  by simp

text∩›
context
begin
  private lemma "{(s::nat) .. e}  {s' .. e'} = {}  s > e'  s' > e  s > e  s' > e'"
    by simp linarith
  private fun wordinterval_intersection'
    :: "'a::len wordinterval  'a::len wordinterval  'a::len wordinterval" where
    "wordinterval_intersection' (WordInterval s e) (WordInterval s' e') = (
        if s > e  s' > e'  s > e'  s' > e  s > e  s' > e'
        then
          Empty_WordInterval
        else
          WordInterval (max s s') (min e e')
        )" |
    "wordinterval_intersection' (RangeUnion r1 r2) t =
        RangeUnion (wordinterval_intersection' r1 t) (wordinterval_intersection' r2 t)"|
    "wordinterval_intersection' t (RangeUnion r1 r2) =
        RangeUnion (wordinterval_intersection' t r1) (wordinterval_intersection' t r2)"

  private lemma wordinterval_intersection'_set_eq:
    "wordinterval_to_set (wordinterval_intersection' r1 r2) =
      wordinterval_to_set r1  wordinterval_to_set r2"
    by(induction r1 r2 rule: wordinterval_intersection'.induct) (auto)

  lemma "wordinterval_intersection'
          (RangeUnion (RangeUnion (WordInterval (1::32 word) 3) (WordInterval 8 10))
                      (WordInterval 1 3)) (WordInterval 1 3) =
          RangeUnion (RangeUnion (WordInterval 1 3) (WordInterval 1 0)) (WordInterval 1 3)" by eval

  definition wordinterval_intersection
    :: "'a::len wordinterval  'a::len wordinterval  'a::len wordinterval" where
    "wordinterval_intersection r1 r2  wordinterval_compress (wordinterval_intersection' r1 r2)"

  lemma wordinterval_intersection_set_eq[simp]:
    "wordinterval_to_set (wordinterval_intersection r1 r2) =
      wordinterval_to_set r1  wordinterval_to_set r2"
    by(simp add: wordinterval_intersection_def
                 wordinterval_compress wordinterval_intersection'_set_eq)

  lemma "wordinterval_intersection
          (RangeUnion (RangeUnion (WordInterval (1::32 word) 3) (WordInterval 8 10))
                      (WordInterval 1 3)) (WordInterval 1 3) =
          WordInterval 1 3" by eval
end


definition wordinterval_subset :: "'a::len wordinterval  'a::len wordinterval  bool" where
  "wordinterval_subset r1 r2  wordinterval_empty (wordinterval_setminus r1 r2)"
lemma wordinterval_subset_set_eq[simp]:
  "wordinterval_subset r1 r2 = (wordinterval_to_set r1  wordinterval_to_set r2)"
  unfolding wordinterval_subset_def by simp

definition wordinterval_eq :: "'a::len wordinterval  'a::len wordinterval  bool" where
  "wordinterval_eq r1 r2 = (wordinterval_subset r1 r2  wordinterval_subset r2 r1)"
lemma wordinterval_eq_set_eq:
  "wordinterval_eq r1 r2  wordinterval_to_set r1 = wordinterval_to_set r2"
  unfolding wordinterval_eq_def by auto

thm iffD1[OF wordinterval_eq_set_eq]
(*declare iffD1[OF wordinterval_eq_set_eq, simp]*)

lemma wordinterval_eq_comm: "wordinterval_eq r1 r2  wordinterval_eq r2 r1"
  unfolding wordinterval_eq_def by fast
lemma wordinterval_to_set_alt: "wordinterval_to_set r = {x. wordinterval_element x r}"
  unfolding wordinterval_element_set_eq by blast

lemma wordinterval_un_empty:
  "wordinterval_empty r1  wordinterval_eq (wordinterval_union r1 r2) r2"
  by(subst wordinterval_eq_set_eq, simp)
lemma wordinterval_un_emty_b:
  "wordinterval_empty r2  wordinterval_eq (wordinterval_union r1 r2) r1"
  by(subst wordinterval_eq_set_eq, simp)

lemma wordinterval_Diff_triv:
  "wordinterval_empty (wordinterval_intersection a b)  wordinterval_eq (wordinterval_setminus a b) a"
  unfolding wordinterval_eq_set_eq
  by simp blast



text‹A size of the datatype, does not correspond to the cardinality of the corresponding set›
fun wordinterval_size :: "('a::len) wordinterval  nat" where
  "wordinterval_size (RangeUnion a b) = wordinterval_size a + wordinterval_size b" |
  "wordinterval_size (WordInterval s e) = (if s  e then 1 else 0)"

lemma wordinterval_size_length: "wordinterval_size r = length (wi2l r)"
  by(induction r) (auto)

lemma Ex_wordinterval_nonempty: "x::('a::len wordinterval). y  wordinterval_to_set x"
  proof show "y  wordinterval_to_set wordinterval_UNIV" by simp qed

lemma wordinterval_eq_reflp:
  "reflp wordinterval_eq"
  apply(rule reflpI)
  by(simp only: wordinterval_eq_set_eq)
lemma wordintervalt_eq_symp:
  "symp wordinterval_eq"
  apply(rule sympI)
  by(simp add: wordinterval_eq_comm)
lemma wordinterval_eq_transp:
  "transp wordinterval_eq"
  apply(rule transpI)
  by(simp only: wordinterval_eq_set_eq)

lemma wordinterval_eq_equivp:
  "equivp wordinterval_eq"
  by (auto intro: equivpI wordinterval_eq_reflp wordintervalt_eq_symp wordinterval_eq_transp)


text‹The smallest element in the interval›
  definition is_lowest_element :: "'a::ord  'a set  bool" where
    "is_lowest_element x S = (x  S  (yS. y  x  y = x))"

  lemma
  	fixes x :: "'a :: complete_lattice"
  	assumes "x  S"
  	shows " x = Inf S  is_lowest_element x S"
  using assms apply(simp add: is_lowest_element_def)
   by (simp add: Inf_lower eq_iff)

  lemma
  	fixes x :: "'a :: linorder"
  	assumes "finite S" and "x  S"
  	shows "is_lowest_element x S  x = Min S"
  apply(rule)
  subgoal
   apply(simp add: is_lowest_element_def)
   apply(subst Min_eqI[symmetric])
   using assms by(auto)
  by (metis Min.coboundedI assms(1) assms(2) dual_order.antisym is_lowest_element_def)

text‹Smallest element in the interval›
  fun wordinterval_lowest_element :: "'a::len wordinterval  'a word option" where
    "wordinterval_lowest_element (WordInterval s e) = (if s  e then Some s else None)" |
    "wordinterval_lowest_element (RangeUnion A B) =
      (case (wordinterval_lowest_element A, wordinterval_lowest_element B) of
          (Some a, Some b)  Some (if a < b then a else b) |
          (None, Some b)  Some b |
          (Some a, None)  Some a |
          (None, None)  None)"

  lemma wordinterval_lowest_none_empty: "wordinterval_lowest_element r = None  wordinterval_empty r"
    proof(induction r)
    case WordInterval thus ?case by simp
    next
    case RangeUnion thus ?case by fastforce
    qed


  lemma wordinterval_lowest_element_correct_A:
    "wordinterval_lowest_element r = Some x  is_lowest_element x (wordinterval_to_set r)"
    unfolding is_lowest_element_def
    apply(induction r arbitrary: x rule: wordinterval_lowest_element.induct)
     apply(rename_tac rs re x, case_tac "rs  re", auto)[1]
    apply(subst(asm) wordinterval_lowest_element.simps(2))
    apply(rename_tac A B x)
    apply(case_tac     "wordinterval_lowest_element B")
     apply(case_tac[!] "wordinterval_lowest_element A")
       apply(simp_all add: wordinterval_lowest_none_empty)[3]
    apply fastforce
  done


  lemma wordinterval_lowest_element_set_eq: assumes "¬ wordinterval_empty r"
    shows "(wordinterval_lowest_element r = Some x) = (is_lowest_element x (wordinterval_to_set r))"
    (*unfolding is_lowest_element_def*)
    proof(rule iffI)
      assume "wordinterval_lowest_element r = Some x"
      thus "is_lowest_element x (wordinterval_to_set r)"
     using wordinterval_lowest_element_correct_A wordinterval_lowest_none_empty by simp
    next
      assume "is_lowest_element x (wordinterval_to_set r)"
      with assms show "(wordinterval_lowest_element r = Some x)"
        proof(induction r arbitrary: x rule: wordinterval_lowest_element.induct)
        case 1 thus ?case by(simp add: is_lowest_element_def)
        next
        case (2 A B x)

        have is_lowest_RangeUnion: "is_lowest_element x (wordinterval_to_set A  wordinterval_to_set B) 
          is_lowest_element x (wordinterval_to_set A)  is_lowest_element x (wordinterval_to_set B)"
          by(simp add: is_lowest_element_def)

         (*why ⋀ A B?*)
         have wordinterval_lowest_element_RangeUnion:
          "a b A B. wordinterval_lowest_element A = Some a 
                  wordinterval_lowest_element B = Some b 
                  wordinterval_lowest_element (RangeUnion A B) = Some (min a b)"
           by(auto dest!: wordinterval_lowest_element_correct_A simp add: is_lowest_element_def min_def)

        from 2 show ?case
        apply(case_tac     "wordinterval_lowest_element B")
         apply(case_tac[!] "wordinterval_lowest_element A")
           apply(auto simp add: is_lowest_element_def)[3]
        apply(subgoal_tac "¬ wordinterval_empty A  ¬ wordinterval_empty B")
         prefer 2
         using arg_cong[where f = Not, OF wordinterval_lowest_none_empty] apply blast
        apply(drule(1) wordinterval_lowest_element_RangeUnion)
        apply(simp split: option.split_asm add: min_def)
         apply(drule is_lowest_RangeUnion)
         apply(elim disjE)
          apply(simp add: is_lowest_element_def)
         apply(clarsimp simp add: wordinterval_lowest_none_empty)

        apply(simp add: is_lowest_element_def)
        apply(clarsimp simp add: wordinterval_lowest_none_empty)
        using wordinterval_lowest_element_correct_A[simplified is_lowest_element_def]
        by (metis Un_iff not_le)
      qed
    qed


text‹Cardinality approximation for @{typ "('a::len) wordinterval"}s›
context
begin
  lemma card_atLeastAtMost_word: fixes s::"('a::len) word" shows "card {s..e} = Suc (unat e) - (unat s)"
    apply(cases "s > e")
     apply(simp)
     apply(subst(asm) Word.word_less_nat_alt)
     apply simp
    apply(subst upto_enum_set_conv2[symmetric])
    apply(subst List.card_set)
    apply(simp add: remdups_enum_upto)
    done

  fun wordinterval_card :: "('a::len) wordinterval  nat" where
    "wordinterval_card (WordInterval s e) = Suc (unat e) - (unat s)" |
    "wordinterval_card (RangeUnion a b) = wordinterval_card a + wordinterval_card b"

  lemma wordinterval_card: "wordinterval_card r  card (wordinterval_to_set r)"
    proof(induction r)
    case WordInterval thus ?case by (simp add: card_atLeastAtMost_word)
    next
    case (RangeUnion r1 r2)
      have "card (wordinterval_to_set r1  wordinterval_to_set r2) 
              card (wordinterval_to_set r1) + card (wordinterval_to_set r2)"
        using Finite_Set.card_Un_le by blast
      with RangeUnion show ?case by(simp)
    qed

  text‹With @{thm wordinterval_compress} it should be possible to get the exact cardinality›
end

end