Theory EnumeratorProps

(*  Author:  Gertrud Bauer, Tobias Nipkow  *)

section‹Properties of Patch Enumeration›

theory EnumeratorProps
imports Enumerator GraphProps
begin

lemma length_hideDupsRec[simp]: "x. length(hideDupsRec x xs) = length xs"
by(induct xs) auto

lemma length_hideDups[simp]: "length(hideDups xs) = length xs"
by(cases xs) simp_all

lemma length_indexToVertexList[simp]:
 "length(indexToVertexList x y xs) = length xs"
by(simp add:indexToVertexList_def)


(***************************** List not decreasing ***************************)
definition increasing :: "('a::linorder) list  bool" where
 "increasing ls   x y as bs. ls = as @ x # y # bs  x  y"

lemma increasing1: " as x. increasing ls  ls = as @ x # cs @ y # bs  x  y"
proof (induct cs)
  case Nil then show ?case
    by (auto simp: increasing_def)
next
  case (Cons c cs) then show ?case
    apply (subgoal_tac "c  y")
    apply (force simp: increasing_def)
    apply (rule_tac Cons) by simp_all
qed

lemma increasing2: "increasing (as@bs)  x  set as  y  set bs  x  y"
proof-
  assume n:"increasing (as@bs)" and x:"x  set as" and y: "y  set bs"
  from x obtain as' as'' where as: "as = as' @ x # as''" by (auto simp: in_set_conv_decomp)
  from y obtain bs' bs'' where bs: "bs = bs' @ y # bs''" by (auto simp: in_set_conv_decomp)
  from n as bs show ?thesis
  apply (auto intro!: increasing1)
  apply (subgoal_tac "as' @ x # as'' @ bs' @ y # bs'' = as' @ x # (as'' @ bs') @ y # bs''")
  by (assumption) auto
qed

lemma increasing3: " as bs. (ls = as @ bs  ( x  set as.  y  set bs. x  y))  increasing (ls)"
apply (simp add: increasing_def) apply safe
proof -
  fix as bs x y
  assume p: "asa bsa. as @ x # y # bs = asa @ bsa  (xset asa. yset bsa. x  y)"
  then have p': " asa bsa. as @ x # y # bs = asa @ bsa  (xset asa. yset bsa. x  y)" by auto
  then have "(xset (as @ [x]). yset (y # bs). x  y)" by (rule_tac p') auto
  then show "x  y" by (auto simp: increasing_def)
qed

lemma increasing4: "increasing (as@bs)  increasing as"
apply (simp add: increasing_def) apply safe by auto

lemma increasing5: "increasing (as@bs)  increasing bs"
proof -
  assume nd: "increasing (as@bs)"
  then have r: " x y asa bsa. (asa bsa. as @ bs = asa @ x # y # bsa)  x  y" by (auto simp: increasing_def)
  show ?thesis apply (clarsimp simp add: increasing_def)
    apply (rule_tac r)
    apply (rule_tac x="as @ _" in exI)
    apply auto
    done
qed


(*********************************** EnumeratorProps *************************************)

(********** enumBase ***********)

lemma enumBase_length: "ls  set (enumBase nmax)  length ls = 1"
by (auto simp: enumBase_def)

lemma enumBase_bound: "y  set (enumBase nmax). z  set y. z  nmax"
by (auto simp: enumBase_def)

lemmas enumBase_simps = enumBase_length enumBase_bound


(********** enumAppend ************)

lemma enumAppend_bound: "ls  set ((enumAppend nmax) lss) 
  y  set lss.  z  set y. z  nmax  x  set ls  x   nmax"
by (auto simp add: enumAppend_def split: if_split_asm)


lemma enumAppend_bound_rec: "ls  set (((enumAppend nmax) ^^ n) lss) 
   y  set lss.  z  set y. z  nmax  x  set ls  x   nmax"
proof -
  assume ls: "ls  set ((enumAppend nmax ^^ n) lss)" and lss: "yset lss. zset y. z  nmax" and x: "x  set ls"
  have ind:" lss. yset lss. zset y. z  nmax   y  set (((enumAppend nmax) ^^ n) lss).  z  set y. z  nmax"
  proof (induct n)
    case 0 then show ?case by auto
  next
    case (Suc n) show ?case apply (intro ballI) apply (rule enumAppend_bound) by (auto intro!: Suc)
  qed
  with lss have " y  set (((enumAppend nmax) ^^ n) lss).  z  set y. z  nmax" apply (rule_tac ind) .
  with ls x show ?thesis by auto
qed

lemma enumAppend_increase_rec:
  " m as bs. ls  set (((enumAppend nmax) ^^ m) (enumBase nmax)) 
  as @ bs = ls    x  set as.  y  set bs. x  y"
apply (induct ls rule: rev_induct) apply force apply auto apply (case_tac "m") apply simp  apply (drule_tac enumBase_length)
apply (case_tac as) apply simp_all
proof -
  fix x xs m as bs xa xb n
  assume ih: "m as bs.
           xs  set ((enumAppend nmax ^^ m) (enumBase nmax)); as @ bs = xs
            xset as. xaset bs. x  xa"
    and xs:"xs @ [x]  set (enumAppend nmax ((enumAppend nmax ^^ n) (enumBase nmax)))"
    and asbs: "as @ bs = xs @ [x]" and xa:"xa  set as" and xb: "xb  set bs" and m: "m = Suc n"
  from ih have ih2: " as bs x y. xs  set ((enumAppend nmax ^^ n) (enumBase nmax)); as @ bs = xs; x  set as; y  set bs
            x  y" by auto

  from xb have "bs  []"  by auto
  then obtain bs' b where bs': "bs = bs' @ [b]" apply (cases rule: rev_exhaust) by auto
  with asbs have beq:"b = x" by auto
  from bs' asbs have xs': "as @ bs' = xs" by auto
  with xs have "xa  x"
  proof (cases "xs" rule: rev_exhaust)
    case Nil with xa xs' show ?thesis by auto
  next
    case (snoc ys y)
    have "xa  y"
    proof (cases "xa = y")
      case True then show ?thesis by auto
    next
      case False
      from xa xs' have "xa  set xs" by auto
      with False snoc have "xa  set ys" by auto
      with xs snoc  show ?thesis
        apply (rule_tac ih2)
        by (auto simp: enumAppend_def)
    qed
    with xs snoc show "xa  x" by (auto simp: enumAppend_def split:if_split_asm)
  qed
  then show "xa  xb" apply (cases "xb = b") apply (simp add: beq)
  proof (rule_tac ih2)
    from xs
    show "xs  set ((enumAppend nmax ^^ n) (enumBase nmax))"
    by (auto simp: enumAppend_def)
  next
    from xs' show "as @ bs' = xs" by auto
  next
    from xa show "xa  set as" by auto
  next
    assume "xb  b"
    with xb bs' show "xb  set bs'" by auto
  qed
qed

lemma enumAppend_length1: "ls. ls  set ((enumAppend nmax ^^ n) lss) 
 (l  set lss. |l| = k)  |ls| = k + n"
apply (induct n)
apply simp
by (auto simp add:enumAppend_def split: if_split_asm)

lemma enumAppend_length2: "ls. ls  set ((enumAppend nmax ^^ n) lss) 
 (l. l  set lss  |l| = k)  K = k + n  |ls| = K"
 by (auto simp add: enumAppend_length1)


(*********** enum *********)

lemma enum_enumerator:
 "enum i j = enumerator i j"
by(simp add: enum_def enumTab_def tabulate2_def tabulate_def)


(*********** enumerator *********)

lemma enumerator_hd: "ls  set (enumerator m n)  hd ls = 0"
by (auto simp: enumerator_def split: if_split_asm)

lemma enumerator_last: "ls  set (enumerator m n)  last ls = (n - 1)"
by (auto simp: enumerator_def split: if_split_asm)

lemma enumerator_length: "ls  set (enumerator m n)  2  length ls"
by (auto simp: enumerator_def split: if_split_asm)

lemmas set_enumerator_simps = enumerator_hd enumerator_last enumerator_length

lemma enumerator_not_empty[dest]: "ls  set (enumerator m n)  ls   []"
apply (subgoal_tac "2  length ls") apply force  by (rule enumerator_length)

lemma enumerator_length2: "ls  set (enumerator m n)  2 < m  length ls = m"
proof -
  assume ls:"ls  set (enumerator m n)" and m: "2 < m"
  define k where "k = m - 3"
  with m have k: "m = k + 3" by arith
  with ls have "ls  set (enumerator (k+3) n)" by auto
  then have "length ls = k + 3"
    apply (auto simp: enumerator_def enumBase_def)
    apply (erule enumAppend_length2) by auto
  with k show ?thesis by simp
qed

lemma enumerator_bound: "ls  set (enumerator m nmax) 
 0 < nmax  x  set ls  x < nmax"
apply (auto simp: enumerator_def split: if_split_asm)
apply (subgoal_tac "x  nmax - 2") apply arith
apply (rule_tac enumAppend_bound_rec) by(auto simp:enumBase_simps)

lemma enumerator_bound2: "ls  set (enumerator m nmax)  1 < nmax  x  set (butlast ls)  x < nmax - Suc 0"
apply (auto simp: enumerator_def split: if_split_asm)
apply (subgoal_tac "x   (nmax - 2)") apply arith
apply (rule_tac enumAppend_bound_rec) by(auto simp:enumBase_simps)

lemma enumerator_bound3: "ls  set (enumerator m nmax)  1 < nmax  last (butlast ls) < nmax - Suc 0"
apply (case_tac "ls" rule: rev_exhaust) apply force
apply (rule_tac enumerator_bound2) apply assumption
apply auto
apply (case_tac "ys" rule: rev_exhaust) apply simp
apply (subgoal_tac "2  length (ys @ [y])") apply simp
apply (rule_tac enumerator_length) by auto


lemma enumerator_increase: " as bs. ls  set (enumerator m nmax)   as @ bs = ls   x  set as.  y  set bs. x  y"
apply (auto simp: enumerator_def del: Nat.diff_is_0_eq' split: if_split_asm intro: enumAppend_increase_rec)
apply (case_tac as) apply simp apply simp
apply (case_tac bs rule: rev_exhaust)  apply simp apply simp apply auto
apply (drule_tac enumAppend_bound_rec) apply (auto simp:enumBase_simps)
by (auto dest!: enumAppend_increase_rec)

lemma enumerator_increasing: "ls  set (enumerator m nmax)  increasing ls"
apply (rule increasing3)
by (auto dest: enumerator_increase)

definition incrIndexList :: "nat list  nat  nat  bool" where
 "incrIndexList ls m nmax 
  1 < m  1 < nmax 
  hd ls = 0  last ls = (nmax - 1)  length ls = m
  last (butlast ls) < last ls  increasing ls"

lemma incrIndexList_1lem[simp]: "incrIndexList ls m nmax  Suc 0 < m"
by (unfold incrIndexList_def) simp

lemma incrIndexList_1len[simp]: "incrIndexList ls m nmax  Suc 0 < nmax"
by (unfold incrIndexList_def) simp

lemma incrIndexList_help2[simp]: "incrIndexList ls m nmax  hd ls = 0"
by (unfold incrIndexList_def) simp

lemma incrIndexList_help21[simp]: "incrIndexList (l # ls) m nmax  l = 0"
by (auto dest: incrIndexList_help2)

lemma incrIndexList_help3[simp]: "incrIndexList ls m nmax  last ls = (nmax - (Suc 0))"
by (unfold incrIndexList_def)  simp

lemma incrIndexList_help4[simp]: "incrIndexList ls m nmax  length ls = m "
by (unfold incrIndexList_def)  simp

lemma incrIndexList_help5[intro]: "incrIndexList ls m nmax   last (butlast ls) < nmax - Suc 0"
by (unfold incrIndexList_def) auto

lemma incrIndexList_help6[simp]: "incrIndexList ls m nmax  increasing ls"
by (unfold incrIndexList_def) simp

lemma incrIndexList_help7[simp]: "incrIndexList ls m nmax  ls  []"
apply (subgoal_tac "length ls   0") apply force
apply simp
apply (subgoal_tac "1 < m")  apply arith apply force done

lemma incrIndexList_help71[simp]: "¬ incrIndexList [] m nmax"
by (auto dest: incrIndexList_help7)

lemma incrIndexList_help8[simp]: "incrIndexList ls m nmax  butlast ls  []"
proof (rule ccontr)
  assume props: "incrIndexList ls m nmax" and butl: "¬ butlast ls  []"
  then have "ls  []" by auto
  then have ls': "ls = (butlast ls) @ [last ls]" by auto
  define l where "l = last ls"
  with butl ls' have "ls = [l]" by auto
  then have "length ls = 1" by auto
  with props have "m = 1" by auto
  with props show "False" by (auto dest: incrIndexList_1lem)
qed

lemma incrIndexList_help81[simp]: "¬ incrIndexList [l] m nmax"
by (auto dest: incrIndexList_help8)

lemma incrIndexList_help9[intro]: "(incrIndexList ls m nmax)  
  x  set (butlast ls)  x  nmax - 2"
proof -
  assume props: "(incrIndexList ls m nmax)"  and x: "x  set (butlast ls)"
  then have "last (butlast ls) < last ls" by auto
  with props have "last (butlast ls) < nmax - 1" by auto
  then have leq: "last (butlast ls)   nmax - 2" by arith
  from props  have "ls  []" by auto
  then have ls1: "ls = butlast ls @ [last ls]" by auto
  define ls' where "ls' = butlast (butlast ls)"
  define last2 where "last2 = last (butlast ls)"
  define last1 where "last1 = last ls"
  from props  have "butlast ls  []" by auto
  with ls'_def last2_def have bls: "butlast ls = ls' @ [last2]" by auto
  with last1_def ls1 props have ls3: "ls = ls' @ [last2] @ [last1]" by auto
  from props  have "increasing ls" by auto
  with ls3 have increasing: "increasing (ls' @ ([last2] @ [last1]))" by auto
  then have "x  set ls'  x  last2" by (auto intro: increasing2)
  then have "x  set (ls' @ [last2])  x  last2" by auto
  with bls x have "x  last2" by auto
  with leq last2_def show ?thesis by auto
qed


lemma incrIndexList_help10[intro]: "(incrIndexList ls m nmax)  
  x  set ls  x < nmax" apply (cases ls rule: rev_exhaust) apply auto
  apply (frule incrIndexList_help3) apply (auto dest: incrIndexList_1len)
  apply (frule incrIndexList_help9) apply auto apply (drule incrIndexList_1len)
  by arith

lemma enumerator_correctness: "2 < m  1 < nmax 
  ls  set (enumerator m nmax) 
  incrIndexList ls m nmax"
proof -
  assume m: "2 < m" and nmax: "1 < nmax" and enum: "ls  set (enumerator m nmax)"
  then have "(hd ls = 0  last ls = (nmax - 1)  length ls = m  last (butlast ls) < last ls   increasing ls)"
    by (auto intro: enumerator_increasing enumerator_hd enumerator_last enumerator_length2 enumerator_bound3 simp: set_enumerator_simps)
  with m nmax show ?thesis by (unfold incrIndexList_def) auto
qed

lemma enumerator_completeness_help: " ls. increasing ls  ls  []  length ls = Suc ks  list_all (λx. x < Suc nmax) ls  ls  set ((enumAppend nmax ^^ ks) (enumBase nmax))"
proof (induct ks)
  case 0
  assume "increasing ls" "ls  []" "length ls = Suc 0" "list_all (λx. x < Suc nmax) ls"
  then have " x. ls = [x]"
    apply (case_tac "ls::nat list") by auto
  then obtain x where ls1: "ls = [x]" by auto
  with 0 have "x < Suc nmax" by auto
  with ls1 show ?case apply (simp add: enumBase_def) by auto
next
  case (Suc n)
  define ls' where "ls' = butlast ls"
  define l where "l = last ls"
  define ll where "ll = last ls'"
  define bl where "bl = butlast ls'"
  define ls'list where "ls'list = (enumAppend nmax ^^ n) (enumBase nmax)"
  then have short: "(enumAppend nmax ^^ n) (enumBase nmax) = ls'list" by simp
  from Suc have "ls  []" by auto
  then have "ls = butlast ls @ [last ls]" by auto
  with ls'_def l_def have ls1: "ls = ls' @ [l]" by auto
  with Suc have "length ls' = Suc n" by auto
  then have ls'ne: "ls'  []" by auto
  with ll_def bl_def have ls'1: "ls' = bl @ [ll]" by auto
  then have ll_in_ls': "ll  set ls'" by simp
  from Suc ls1 have "list_all (λx. x < Suc nmax) ls'" by auto
  with ll_in_ls' have "ll < Suc nmax" by (induct ls') auto
  with ll_def have llsmall: "last ls'  nmax"  by auto

  from ls1 have l_in_ls: "l  set ls" by auto
  from Suc have "list_all (λx. x < Suc nmax) ls" by auto
  with l_in_ls have "l < Suc nmax" by (induct ls) auto
  then have lo: "l  nmax" by auto

  from Suc ls1 ls'1 have "increasing ((bl @ [ll]) @ [l])" by auto
  then have "ll   l" by (rule increasing2) auto
  with ll_def have lu: "last ls'  l" by simp

  from Suc ls1 have vors: "ls'  set ((enumAppend nmax ^^ n) (enumBase nmax))"
    by (rule_tac Suc) (auto intro: increasing4)
  with short have "ls'  set ls'list"  by  auto
  with short llsmall ls1 lo lu show ?case  apply simp  apply (simp add: enumAppend_def)
    apply (intro bexI) by auto
qed

lemma enumerator_completeness: "2 < m  incrIndexList ls m nmax 
  ls  set (enumerator m nmax)"
proof -
  assume m: "2 < m" and props: "incrIndexList ls m nmax"
  then have props': "(hd ls = 0  last ls = (nmax - 1)
    length ls = m  last (butlast ls) < last ls   increasing ls)"
   by (unfold incrIndexList_def) auto
  show ?thesis
  proof -
    have props'': "hd ls = 0  last ls = (nmax - 1)  length ls = m 
       increasing ls"
      by (auto simp: props')
    show "ls  set (enumerator m nmax)"
    proof -
      from m props'' have l_ls: "2 < length ls"  by auto
      then have " x y ks. ls = x # ks @ [y]"
        apply (case_tac "ls::(nat list)") apply auto
        apply (case_tac "list" rule: rev_exhaust) by auto
      then obtain x y ks where "ls = x # ks @ [y]" by auto
      with props'' have ls': "ls = 0 # ks @ [nmax - 1]" by auto
      with l_ls have l_ms: "0 < length ks" by auto
      then have ms_ne: "ks  []" by auto
      from ls' have lks: "length ks = length ls - 2" by auto
      from props'' have nd: "increasing ls" by auto
      from props'' have " z. z  set ks  0  z" by auto
      from props'' ls' have "increasing ((0 # ks) @ [nmax - 1])" by auto
      then have z: " z. z  set ks  z  (nmax - 1)"
        by (drule_tac increasing2) auto
      from props  ls' have z': " z. z  set ks  z  (nmax - 2)" by auto

      have "ks  set ((enumAppend (nmax - 2)
         ^^ (length ks - Suc 0)) (enumBase (nmax - 2)))"
      proof (cases "ks = []")   
        case True with ms_ne show ?thesis by simp
      next
        case False
        from props'' have "increasing ls" by auto
        with ls' have "increasing (0 # ks)" by (auto intro: increasing4)
        then have "increasing ([0] @ ks)" by auto
        then have ndks: "increasing ks" by (rule_tac increasing5)
        have listall: "list_all (λx. x < Suc (nmax - 2)) ks"
          apply (simp add: list_all_iff)
          by (auto dest: z')
        with False ndks show ?thesis
          apply (rule_tac enumerator_completeness_help) by auto
      qed
      with lks props' have
        "ks  set ((enumAppend (nmax - 2) ^^ (m - 3)) (enumBase (nmax - 2)))" by auto
      with m ls' show ?thesis by (simp add: enumerator_def)
    qed
  qed
qed

lemma enumerator_equiv[simp]:
 "2 < n  1 < m  is  set(enumerator n m) = incrIndexList is n m"
by (auto intro: enumerator_correctness enumerator_completeness)


end