Theory Tables

Up to index of Isabelle/HOL/Tables

header {* Table Utilities and Properties *}

theory Tables = Table:

subsection {* Additional Properties of @{text "tFold"} *}

lemma tFold_const2_idempotent[simp]:
 "\<lbrakk> assoc c; idempotent c \<rbrakk> \<Longrightarrow> tFold (% h t . a) c t = a"
by (induct_tac t rule: T_induct, simp_all)

lemma tFold_tFold_join:
 "\<lbrakk> assoc c2 \<rbrakk> \<Longrightarrow>
  tFold a2 c2 (tFold (\<lambda>h0 t0. addH (HH h h0 t0) (TT h h0 t0)) hConc t) =
   tFold (\<lambda> h0 t0 . a2 (HH h h0 t0) (TT h h0 t0)) c2 t"
by (induct_tac t rule: T_induct, simp_all)

lemma tFold_tFold_hConc:
 "\<lbrakk> assoc c2 \<rbrakk> \<Longrightarrow>
  tFold a2 c2 (tFold a1 hConc t) =
  tFold (\<lambda> h0 t0 . tFold a2 c2 (a1 h0 t0)) c2 t"
by (induct_tac t rule: T_induct, simp_all)

lemma tFold_tFold_const:
 "\<lbrakk> assoc c2 \<rbrakk> \<Longrightarrow>
  tFold a2 c2 (tFold a1 const t) =
  tFold (\<lambda> h0 t0 . tFold a2 c2 (a1 h0 t0)) const t"
apply (induct_tac t rule: T_induct, simp_all del: const)
apply (subst const)+
apply (simp del: const)
done

lemma f_tFold_const:
  "f (tFold a const t) = tFold (% h0 t0 . f (a h0 t0)) const t"
apply (induct_tac t rule: T_induct, simp_all del: const)
apply (subst const)+
apply (simp del: const)
done

lemma tFold_const_const[simp]: "tFold (% h t . r) const t = r"
by (induct_tac t rule: T_induct, simp_all del: const, simp)

lemma tFold_foldr1_hConc:
 "assoc c \<Longrightarrow> tFold a c (foldr1 hConc ts) = foldr1 c (map1 (tFold a c) ts)"
by (induct_tac ts rule: neList_append_induct, simp_all)

lemma tFold_LRunit[simp]:
  "\<lbrakk> \<And> h t . LRunit c (a h t); assoc c \<rbrakk> \<Longrightarrow>
   tFold a c t = a arbitrary arbitrary"
apply (induct_tac t rule: T_induct, simp_all)
apply (rule LRunit_equal [of c], simp_all add: LRunit_left LRunit_right)
done

consts tFold0 :: "('c \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('c,'u) T \<Rightarrow> 'c"
defs tFold0_def: "tFold0 == tFold (% h t . h)"

lemma tFold0_addH[simp]: "tFold0 c (addH h t) = h"
by (unfold tFold0_def, simp)

lemma tFold0_hConc[simp]:
  "assoc c \<Longrightarrow> tFold0 c (hConc t1 t2) = c (tFold0 c t1) (tFold0 c t2)"
by (unfold tFold0_def, simp)

subsection {* tFoldC *}

consts tFoldC :: "('h \<Rightarrow> 'c) \<Rightarrow> ('c \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('h,'u) T \<Rightarrow> 'c"
defs tFoldC_def: "tFoldC a == tFold (% h t . a h)"

subsection {* hHead *}

constdefs
  hHead :: "('h,'t) T \<Rightarrow> ('h * 't)"
  "hHead == tFold Pair const"

lemma hHead_addH[simp]: "hHead (addH h t) = (h,t)"
by (simp add: hHead_def)

lemma hHead_uncurry_addH[simp]: "hHead (uncurry addH p) = p"
by (simp add: hHead_def)

lemma hHead_hCons[simp]: "hHead (hCons p t) = p"
by (simp add: hHead_def)

lemma hHead_hConc[simp]: "hHead (hConc t1 t2) = hHead t1"
by (simp add: hHead_def)

constdefs
 hLength :: "('h,'t) T \<Rightarrow> nat"
 "hLength == tFold (% h t . 1) (% x y . x + y)"

lemma hLength_addH[simp]: "hLength (addH h t) = 1"
by (simp add: hLength_def)

lemma hLength_hCons[simp]: "hLength (hCons p t) = Suc (hLength t)"
by (simp add: hLength_def)

lemma hLength_hConc[simp]: "hLength (hConc t1 t2) = hLength t1 + hLength t2"
apply (subgoal_tac "assoc ((op +) :: nat \<Rightarrow> nat \<Rightarrow> nat)")
  prefer 2
  apply (rule assoc_intro, simp)
apply (simp add: hLength_def)
done

lemma hLength_pos[simp]: "0 < hLength t"
by (induct_tac t rule: T_induct, simp_all)

subsection {* The ``Cons View'' *}

constdefs
  hUnCons0 :: "(('h * 't) + (('h * 't) * ('h,'t) T)) * ('h,'t) T \<Rightarrow>
               (('h * 't) + (('h * 't) * ('h,'t) T)) * ('h,'t) T \<Rightarrow>
               (('h * 't) + (('h * 't) * ('h,'t) T)) * ('h,'t) T"
  "hUnCons0 p1 p2 == (case fst p1 of
                        Inl p \<Rightarrow> Inr (p,snd p2)
                      | Inr (p,t) \<Rightarrow> Inr (p,hConc t (snd p2))
                     ,hConc (snd p1) (snd p2)
                     )"

lemma snd_hUnCons0_p: "snd (hUnCons0 p1 p2) = hConc (snd p1) (snd p2)"
by (simp add: hUnCons0_def)

lemma fst_hUnCons0_p: "fst (hUnCons0 p1 p2) = (case fst p1 of
                          Inl p \<Rightarrow> Inr (p,snd p2)
                        | Inr (p,t) \<Rightarrow> Inr (p,hConc t (snd p2)))"
by (simp add: hUnCons0_def)

lemma snd_hUnCons0[simp]: "snd (hUnCons0 (r1,t1) (r2,t2)) = hConc t1 t2"
by (simp add: snd_hUnCons0_p)

lemma assoc_hUnCons0[simp]: "assoc hUnCons0"
apply (rule assoc_intro)
apply (simp add: hUnCons0_def)
apply (split sum.split, rule conjI)
apply (intro strip, simp)
apply (intro strip, simp)
apply (split sum.split, rule conjI)
apply (intro strip)
apply (case_tac b, simp)
apply (intro strip, case_tac b, simp)
apply (rotate_tac -2, drule sym, simp)
done

constdefs
  hUnCons1 :: "('h,'t) T \<Rightarrow> (('h * 't) + (('h * 't) * ('h,'t) T)) * ('h,'t) T"
  "hUnCons1 == tFold (% h t . (Inl (h,t), addH h t)) hUnCons0"

lemma hUnCons1_addH[simp]: "hUnCons1 (addH h t) = (Inl (h,t), addH h t)"
by (simp add: hUnCons1_def)

lemma hUnCons1_hCons[simp]: "hUnCons1 (hCons p t) = (Inr (p,t), hCons p t)"
apply (simp add: hUnCons1_def hUnCons0_def)
apply (induct_tac t rule: T_induct)
apply (simp add: hCons)
apply (simp add: snd_hUnCons0_p hCons)
done

lemma hUnCons1_hConc[simp]:
 "hUnCons1 (hConc t1 t2) = hUnCons0 (hUnCons1 t1) (hUnCons1 t2)"
by (simp add: hUnCons1_def)

lemma snd_hUnCons1[simp]: "snd (hUnCons1 t) = t"
by (induct_tac t rule: T_induct, simp_all add: snd_hUnCons0_p)

constdefs
  hUnCons :: "('h,'t) T \<Rightarrow> (('h * 't) + (('h * 't) * ('h,'t) T))"
  "hUnCons t == fst (hUnCons1 t)"

lemma hUnCons_addH[simp]: "hUnCons (addH h t) = Inl (h,t)"
by (simp add: hUnCons_def)

lemma hUnCons_hCons[simp]: "hUnCons (hCons p t) = Inr (p,t)"
by (simp add: hUnCons_def)

lemma hUnCons_hConc[simp]: "hUnCons (hConc t1 t2) = (case hUnCons t1 of
     Inl p \<Rightarrow> Inr (p, t2)
     | Inr (p, t) \<Rightarrow> Inr (p, hConc t t2))"
apply (simp add: hUnCons_def fst_hUnCons0_p)
apply (subst snd_hUnCons1, simp)
done

consts
  tFoldr0 :: "('h \<Rightarrow> 't \<Rightarrow> 'r) * ('h \<Rightarrow> 't \<Rightarrow> 'r \<Rightarrow> 'r) * ('h,'t) T \<Rightarrow> 'r"

lemma tFoldr0_measure[simp]:
  "\<forall>h t t'. (\<exists>ta. hUnCons t = Inr ((h, ta), t')) \<longrightarrow> hLength t' < hLength t"
apply (rule allI)
apply (rule allI)
apply (rule_tac x=h in spec)
apply (induct_tac t rule: T_induct, auto)
apply (case_tac "hUnCons t1", simp)
apply (case_tac b, simp)
apply (erule conjE, rotate_tac -1, drule sym, simp)
done

recdef tFoldr0 "measure (% (a,f,t) . hLength t)"
  tFoldr0_def: "tFoldr0 (a,f,t) = (case hUnCons t of
        Inl (h,t) \<Rightarrow> a h t
      | Inr ((h,t),t') \<Rightarrow> f h t (tFoldr0 (a,f,t')))"

constdefs
  tFoldr :: "('h \<Rightarrow> 't \<Rightarrow> 'r) \<Rightarrow> ('h \<Rightarrow> 't \<Rightarrow> 'r \<Rightarrow> 'r) \<Rightarrow> ('h,'t) T \<Rightarrow> 'r"
  "tFoldr a f == % t . tFoldr0 (a,f,t)"

lemma tFoldr_addH[simp]: "tFoldr a f (addH h t) = a h t"
by (simp add: tFoldr_def tFoldr0_def)

lemma tFoldr_hCons[simp]: "tFoldr a f (hCons p t) = uncurry f p (tFoldr a f t)"
by (case_tac p, simp add: tFoldr_def tFoldr0_def)

lemma tFoldr_hConc:
  "tFoldr a f (hConc t1 t2) = tFoldr (% h t . f h t (tFoldr a f t2)) f t1"
apply (induct_tac t1 rule: T_cons_induct, simp)
apply (subst hCons_p [THEN sym], simp_all)
done

lemma hConc_via_tFoldr:
  "hConc t1 t2 = tFoldr (% h t . hCons (h,t) t2) (curry hCons) t1"
by (induct_tac t1 rule: T_cons_induct, simp_all, simp add: hCons)

lemma tFold_via_tFoldr:
  "tFold a c t = tFoldr a (% h t r . c (a h t) r) t"
by (induct_tac t rule: T_cons_induct, simp_all)

subsection {* Mapping *}

constdefs
 hMap :: "('h1 \<Rightarrow> 'h2) \<Rightarrow> ('h1,'t) T \<Rightarrow> ('h2,'t) T"
 "hMap f == tFold (addH o f) (hConc)"
 tMap :: "('t1 \<Rightarrow> 't2) \<Rightarrow> ('h,'t1) T \<Rightarrow> ('h,'t2) T"
 "tMap f == tFold (% h t . addH h (f t)) (hConc)"

lemma tMap_addH[simp]: "tMap f (addH h t) = addH h (f t)"
by (simp add: tMap_def)

lemma tMap_hConc[simp]: "tMap f (hConc t1 t2) = hConc (tMap f t1) (tMap f t2)"
by (simp add: tMap_def)

lemma tMap_hCons[simp]: "tMap f (hCons p t) = hCons (fst p, f (snd p)) (tMap f t)"
by (simp add: tMap_def hCons)

lemma hMap_addH[simp]: "hMap f (addH h t) = addH (f h) t"
by (simp add: hMap_def)

lemma hMap_hConc[simp]: "hMap f (hConc t1 t2) = hConc (hMap f t1) (hMap f t2)"
by (simp add: hMap_def)

lemma hMap_hCons[simp]: "hMap f (hCons p t) = hCons (f (fst p), snd p) (hMap f t)"
by (simp add: hMap_def hCons)

lemma tFold_tMap[simp]:
  "assoc c \<Longrightarrow> tFold a c (tMap f t) = tFold (% h t0 . a h (f t0)) c t"
by (induct_tac t rule: T_induct, simp_all)

lemma tMap_tFold_hConc:
 "tMap f (tFold a hConc t) = tFold (\<lambda> h0 t0 . tMap f (a h0 t0)) hConc t"
by (induct_tac t rule: T_induct, simp_all)

lemma tMap_tMap: "tMap f (tMap g t) = tMap (f o g) t"
by (induct_tac t rule: T_induct, simp_all)

lemma tMap_const_tMap[simp]:
 "tMap (const t1) (tMap f t) = tMap (const t1) t"
by (subst tMap_tMap, simp add: comp_def)

lemma tMap_CONST_tMap[simp]:
 "tMap (\<lambda> x . t1) (tMap f t) = tMap (const t1) t"
by (subst tMap_tMap, simp add: comp_def)

subsection {* Headers and Subtables *}

constdefs
 headers :: "('h,'t) T \<Rightarrow> 'h neList"
 "headers == tFold (% h t . singleton h) append"
 subtables ::  "('h,'t) T \<Rightarrow> 't neList"
 "subtables == tFold (% h t . singleton t) append"

lemma headers_addH[simp]: "headers (addH h t) = singleton h"
by (simp add: headers_def)

lemma headers_hCons[simp]: "headers (hCons p t) = cons1 (fst p) (headers t)"
by (simp add: headers_def cons1)

lemma headers_hConc[simp]: "headers (hConc t1 t2) = append (headers t1) (headers t2)"
by (simp add: headers_def)

lemma subtables_addH[simp]: "subtables (addH h t) = singleton t"
by (simp add: subtables_def)

lemma subtables_hCons[simp]: "subtables (hCons p t) = cons1 (snd p) (subtables t)"
by (simp add: subtables_def cons1)

lemma subtables_hConc[simp]: "subtables (hConc t1 t2) = append (subtables t1) (subtables t2)"
by (simp add: subtables_def)

lemma headers_eq_singleton_0:
 "headers t = singleton h \<longrightarrow> (EX t0 . t = addH h t0)"
apply (induct_tac t rule: T_cons_induct, auto)
apply (rule_tac x=t0 in exI, drule singleton_inj, simp)
done

lemma headers_eq_singleton[dest?]:
 "headers t = singleton h \<Longrightarrow> (EX t0 . t = addH h t0)"
by (rule headers_eq_singleton_0 [THEN mp])

lemma headers_eq_cons1_0:
  "headers t1 = cons1 h hs \<longrightarrow>
   (EX t0 t2 . t1 = hCons (h,t0) t2 & headers t2 = hs)"
apply (induct_tac t1 rule: T_cons_induct, simp_all)
apply (intro strip)
apply (drule cons1_inj, erule conjE, simp)
apply (rule_tac x="snd p" in exI)
apply (rule_tac x=t2 in exI)
apply (rotate_tac -2, drule sym, simp)
done

lemma headers_eq_cons1[dest?]:
  "headers t1 = cons1 h hs \<Longrightarrow>
   (EX t0 t2 . t1 = hCons (h,t0) t2 & headers t2 = hs)"
by (rule headers_eq_cons1_0 [THEN mp])

lemma headers_tMap[simp]: "headers (tMap f t) = headers t"
by (induct_tac t rule: T_induct, simp_all)

lemma headers_tFold_hConc[simp]:
  "headers (tFold a hConc t) = tFold (% h t . headers (a h t)) append t"
by (induct_tac t rule: T_induct, simp_all)

lemma tMap_CONST__headers:
 "tMap (\<lambda> x . c) t = foldr1 hConc (map1 (\<lambda> h . addH h c) (headers t))"
by (induct_tac t rule: T_induct, simp_all)

lemma tFold_CONST_hConc__headers:
  "tFold (\<lambda>h (t :: unit). c t) hConc t = foldr1 hConc (map1 (\<lambda> h . c ()) (headers t))"
by (induct_tac t rule: T_induct, simp_all)

subsection {* Regular Skeletons *}

constdefs
 regSkelStep :: "('t \<Rightarrow> 's option) \<Rightarrow> ('h, 't) T \<Rightarrow> ('h neList * 's) option"
 "regSkelStep rs t == option_map (% s . (headers t, s))
                                 (tFold (% h t . rs t) optEq t)"

lemma regSkelStep_addH[simp]:
 "regSkelStep rs (addH h t) = option_map (% s . (singleton h, s)) (rs t)"
by (simp add: regSkelStep_def)

lemma regSkelStep_hConc[simp]:
 "regSkelStep rs (hConc t1 t2) =
    optThen (regSkelStep rs t1) (\<lambda> p1 .
    optThen (regSkelStep rs t2) (\<lambda> p2 .
    if snd p1 = snd p2
    then Some (append (fst p1) (fst p2), snd p1)
    else None))"
apply (simp add: regSkelStep_def)
apply (cases "(tFold (\<lambda>h. rs) optEq t1)", simp add: optEq_N)
apply (cases "(tFold (\<lambda>h. rs) optEq t2)", simp)
apply simp
done

lemma regSkelStep_hCons[simp]:
 "regSkelStep rs (hCons p t) =
    optThen (rs (snd p))
     (\<lambda>hs2. optThen (regSkelStep rs t)
            (\<lambda>p2. if hs2 = snd p2
                  then Some (cons1 (fst p) (fst p2), hs2) else None))"
apply (simp add: hCons cons1)
apply (cases "rs (snd p)", simp_all add: cons1)
apply (cases "regSkelStep rs t", simp_all add: cons1)
done

constdefs
 regSkelOuter1 :: "('h,'t) T \<Rightarrow> 'h neList option"
 "regSkelOuter1 t == Some (headers t)"

lemma regSkelOuter1_addH[simp]:
 "regSkelOuter1 (addH h t) = Some (singleton h)"
by (simp add: regSkelOuter1_def)

lemma regSkelOuter1_hConc[simp]:
 "regSkelOuter1 (hConc t1 t2) = Some (append (headers t1) (headers t2))"
by (simp add: regSkelOuter1_def)

lemma regSkelOuter1_hCons[simp]:
 "regSkelOuter1 (hCons p t) = Some (cons1 (fst p) (headers t))"
by (simp add: hCons cons1)

constdefs
 regSkelOuter2 :: "('h1,('h2,'t) T) T \<Rightarrow> ('h1 neList * ('h2 neList)) option"
 "regSkelOuter2 t == regSkelStep regSkelOuter1 t"

lemma regSkelOuter2_addH[simp]:
   "regSkelOuter2 (addH h t) = Some (singleton h, headers t)"
by (simp add: regSkelOuter2_def regSkelOuter1_def)

lemma regSkelOuter2_hCons[simp]:
   "regSkelOuter2 (hCons p t2) = optThen (regSkelOuter2 t2)
            (\<lambda>p2. if headers (snd p) = snd p2
                  then Some (cons1 (fst p) (fst p2), snd p2) else None)"
by (case_tac "regSkelOuter2 t2", simp_all add: regSkelOuter2_def regSkelOuter1_def)

lemma regSkelOuter2_hConc[simp]:
   "regSkelOuter2 (hConc t1 t2) = optThen (regSkelOuter2 t1)
     (\<lambda>p1. optThen (regSkelOuter2 t2)
            (\<lambda>p2. if snd p1 = snd p2
                  then Some (append (fst p1) (fst p2), snd p1) else None))"
by (simp add: regSkelOuter2_def)

lemma regSkelOuter2_addH_eq_Some:
   "regSkelOuter2 (addH h t) = Some (hs1, hs2) \<Longrightarrow>
    hs1 = singleton h &  hs2 = headers t"
by (simp add: regSkelOuter1_def regSkelOuter2_def)

lemma regSkelOuter2_hConc_eq_Some:
   "regSkelOuter2 (hConc t1 t2) = Some (hs1, hs2) \<Longrightarrow>
    EX hs1a hs1b . append hs1a hs1b = hs1 &
                   regSkelOuter2 t1 = Some (hs1a, hs2) &
                   regSkelOuter2 t2 = Some (hs1b, hs2)"
apply simp
apply (drule optThen_result_Some, erule exE, erule conjE)
apply (drule optThen_result_Some, erule exE, erule conjE)
apply (split split_if_asm)
apply (rule_tac x="fst y" in exI)
apply (rule_tac x="fst ya" in exI)
apply simp
apply (erule conjE, rule conjI)
apply (rotate_tac 2, drule sym, simp)
apply (rotate_tac -1, drule sym, simp)
apply fastsimp
done

lemma regSkelOuter2_hCons_eq_Some:
   "regSkelOuter2 (hCons p t2) = Some (hs1, hs2) \<Longrightarrow>
    EX h1 t1 hs1b . p = (h1,t1) &
                    hs1 = cons1 h1 hs1b &
                    headers t1 = hs2 &
                    regSkelOuter2 t2 = Some (hs1b, hs2)"
apply (simp only: cons1 hCons)
apply (drule regSkelOuter2_hConc_eq_Some)
apply (erule exE, erule exE, erule conjE, erule conjE)
apply (rule_tac x="fst p" in exI)
apply (rule_tac x="snd p" in exI)
apply (rule_tac x="hs1b" in exI)
apply simp
done

lemma regSkelOuter2_eq_Some_0:
   "ALL hs1 hs2 . regSkelOuter2 t = Some (hs1, hs2) \<longrightarrow> headers t = hs1"
apply (induct_tac t rule: T_induct, simp_all)
apply (intro strip)
apply (erule exE, drule optThen_result_Some, simp)
apply (erule exE, erule exE, erule conjE, drule optThen_result_Some, simp)
apply (erule exE, erule exE, erule conjE, simp)
apply (split split_if_asm, simp_all)
done

lemma regSkelOuter2_eq_Some[simp]:
   "regSkelOuter2 t = Some (hs1, hs2) \<Longrightarrow> headers t = hs1"
by (insert regSkelOuter2_eq_Some_0, auto)

lemma regSkelOuter2_tMap_const[simp]:
 "regSkelOuter2 (tMap (const t2) t1) = Some (headers t1, headers t2)"
by (induct_tac t1 rule: T_induct, simp_all)

lemma regSkelOuter2_tMap_CONST[simp]:
 "regSkelOuter2 (tMap (% x . t2) t1) = Some (headers t1, headers t2)"
by (induct_tac t1 rule: T_induct, simp_all)

lemma regSkelOuter2_tMap_h_0:
 "\<lbrakk> \<And>t. headers (h t) = headers t; \<And>t. h (h t) = h t;
    \<And>t1 t2. h (hConc t1 t2) = hConc (h t1) (h t2)
  \<rbrakk> \<Longrightarrow>
  ALL hs1 hs2 .
  regSkelOuter2 t = Some (hs1, hs2) \<longrightarrow>
  regSkelOuter2 (tMap h t) = Some (hs1, hs2)"
apply (induct_tac t rule: T_cons_induct, simp_all)
apply (intro strip)
apply (drule optThen_result_Some, erule exE, erule conjE)
apply (split split_if_asm) prefer 2 apply simp
apply (case_tac p, case_tac y, simp)
done

lemma regSkelOuter2_tMap_h[simp]:
 "\<lbrakk> \<And>t. headers (h t) = headers t; \<And>t. h (h t) = h t;
    \<And>t1 t2. h (hConc t1 t2) = hConc (h t1) (h t2);
    regSkelOuter2 t = Some (hs1, hs2)
  \<rbrakk> \<Longrightarrow>
  regSkelOuter2 (tMap h t) = Some (hs1, hs2)"
by (insert regSkelOuter2_tMap_h_0 [of h t], auto)

subsection {* Two-Dimensional Regular Tables *}

constdefs
 regularOuter2 :: "('h1,('h2,'t) T) T \<Rightarrow> bool"
 "regularOuter2 t == option False (% x . True) (regSkelOuter2 t)"

lemma regularOuter2I[simp,intro]:
  "regSkelOuter2 t = Some (hs1, hs2) \<Longrightarrow> regularOuter2 t"
by (simp add: regularOuter2_def)

lemma regularOuter2[simp,dest]:
  "regularOuter2 t \<Longrightarrow> EX hs1 hs2 . regSkelOuter2 t = Some (hs1, hs2)"
by (case_tac "regSkelOuter2 t", simp_all add: regularOuter2_def)

typedef (regT2) ('h1,'h2,'t) regT2 =
        "{t :: ('h1,('h2,'t) T) T . regularOuter2 t}"
apply (rule_tac x="addH arbitrary (addH arbitrary arbitrary)" in exI)
apply (simp add: regularOuter2_def)
done

lemma regT2[simp,intro!]: "regSkelOuter2 t = Some (hs1, hs2) \<Longrightarrow> t \<in> regT2"
by (simp add: regT2_def, fast)

consts
  regSkel2 :: "('h1,'h2,'t) regT2 \<Rightarrow> 'h1 neList * 'h2 neList"
  reg2dim1 :: "('h1,'h2,'t) regT2 \<Rightarrow> 'h1 neList"
  reg2dim2 :: "('h1,'h2,'t) regT2 \<Rightarrow> 'h2 neList"

defs
  regSkel2_def: "regSkel2 t == option arbitrary id (regSkelOuter2 (Rep_regT2 t))"

lemma regSkel2[simp]:
  "regSkelOuter2 t = Some (hs1, hs2) \<Longrightarrow> regSkel2 (Abs_regT2 t) = (hs1, hs2)"
apply (simp add: regSkel2_def regT2)
apply (subst Abs_regT2_inverse, fast)
apply simp
done

defs
  reg2dim1_def: "reg2dim1 == fst o regSkel2"
  reg2dim2_def: "reg2dim2 == snd o regSkel2"

lemma reg2dim1[simp]:
  "regSkelOuter2 t = Some (hs1, hs2) \<Longrightarrow> reg2dim1 (Abs_regT2 t) = hs1"
by (auto simp add: reg2dim1_def dest: regSkel2)

lemma reg2dim2[simp]:
  "regSkelOuter2 t = Some (hs1, hs2) \<Longrightarrow> reg2dim2 (Abs_regT2 t) = hs2"
by (auto simp add: reg2dim2_def dest: regSkel2)


subsection {* List Interface *}

constdefs
 tList :: "('h, 't) T \<Rightarrow> ('h * 't) neList"
 "tList == tFold (% h t . singleton (h,t)) append"
 tOfList :: "('h * 't) neList \<Rightarrow> ('h, 't) T"
 "tOfList == foldr1 hConc o map1 (uncurry addH)"
 zipT :: "'h neList \<Rightarrow> 't neList \<Rightarrow> ('h, 't) T"
 "zipT hs ts == foldr1 hConc (zipWith1 addH hs ts)"

lemma tList_addH[simp]:  "tList (addH h t) = singleton (h,t)"
by (simp add: tList_def)

lemma tList_hConc[simp]: "tList (hConc t1 t2) = append (tList t1) (tList t2)"
by (simp add: tList_def)

lemma tList_hCons[simp]: "tList (hCons p t2) = cons1 p (tList t2)"
by (simp add: hCons cons1)

lemma tOfList_singleton[simp]: "tOfList (singleton (h,t)) = addH h t"
by (simp add: tOfList_def)

lemma tOfList_append[simp]: "tOfList (append t1 t2) = hConc (tOfList t1) (tOfList t2)"
by (simp add: tOfList_def)

lemma tOfList_cons1[simp]: "tOfList (cons1 p ps) = hCons p (tOfList ps)"
by (simp add: tOfList_def cons1 hCons)

subsection {* ZipWith *}

constdefs
 tZipWith :: "(('h1 * 't1) \<Rightarrow> ('h2 * 't2) \<Rightarrow> ('h * 't)) \<Rightarrow>
               ('h1, 't1) T \<Rightarrow> ('h2, 't2) T \<Rightarrow> ('h, 't) T"
 "tZipWith f t1 t2 ==
  foldr1 hConc (map1 (uncurry addH) (zipWith1 f (tList t1) (tList t2)))"

lemma tZipWith_A_A[simp]:
  "tZipWith f (addH h1 t1) (addH h2 t2) = uncurry addH (f (h1,t1) (h2,t2))"
by (simp add: tZipWith_def)

lemma tZipWith_A_C[simp]:
  "tZipWith f (addH h1 t1) (hCons p2 t2) = uncurry addH (f (h1,t1) p2)"
by (simp add: tZipWith_def)

lemma tZipWith_C_A[simp]:
  "tZipWith f (hCons p1 t1) (addH h2 t2) = uncurry addH (f p1 (h2,t2))"
by (simp add: tZipWith_def)

lemma tZipWith_C_C[simp]:
  "tZipWith f (hCons p1 t1) (hCons p2 t2) = hCons (f p1 p2) (tZipWith f t1 t2)"
proof -
  have "tZipWith f (hCons p1 t1) (hCons p2 t2) = foldr1 hConc
     (map1 (\<lambda>p. addH (fst p) (snd p))
       (zipWith1 f (append (singleton p1) (tList t1))
         (append (singleton p2) (tList t2))))"
   by (simp add: tZipWith_def hCons)
  also have "\<dots> = hCons (f p1 p2) (tZipWith f t1 t2)"
   by (simp add: tZipWith_def hCons cons1 [THEN sym])
  finally show ?thesis .
qed

lemma tZipWith_A[simp]:
  "tZipWith f (addH h1 t1) t2 = uncurry addH (f (h1,t1) (hHead t2))"
by (induct_tac t2 rule: T_cons_induct, simp_all)

lemma tZipWith_C[simp]:
  "hHead (tZipWith f (hCons p1 t1) t2) = f p1 (hHead t2)"
by (induct_tac t2 rule: T_cons_induct, simp_all)

lemma tZipWith__A[simp]:
  "tZipWith f t1 (addH h2 t2) = uncurry addH (f (hHead t1) (h2,t2))"
by (induct_tac t1 rule: T_cons_induct, simp_all)

lemma tZipWith__C[simp]:
  "hHead (tZipWith f t1 (hCons p2 t2)) = f (hHead t1) p2"
by (induct_tac t1 rule: T_cons_induct, simp_all)

lemma tZipWith_assoc_0[simp]:
 "assoc f \<Longrightarrow>
  ALL t1 t2 t3 . tZipWith f (tZipWith f t1 t2) t3 = tZipWith f t1 (tZipWith f t2 t3)"
apply (rule T_cons_inductA)
apply (rule T_cons_inductA, simp_all)
apply (rule T_cons_inductA, simp_all)
apply (rule T_cons_inductA, simp_all)
done

lemma assoc_tZipWith[simp]: "assoc f \<Longrightarrow> assoc (tZipWith f)"
by (rule assoc_intro, simp)

subsection {* Collapsing *}

constdefs
  collapse :: "('h1 \<Rightarrow> 't1 \<Rightarrow> ('h2, 't2) T) \<Rightarrow> ('h1, 't1) T \<Rightarrow> ('h2, 't2) T"
  "collapse f == tFold f hConc"

lemma collapse_addH[simp]: "collapse f (addH h t) = f h t"
by (simp add: collapse_def)

lemma collapse_hConc[simp]:
   "collapse f (hConc t1 t2) = hConc (collapse f t1) (collapse f t2)"
by (simp add: collapse_def)

constdefs
  collapse2 :: "('h1 \<Rightarrow> 'h2 \<Rightarrow> 'h3) \<Rightarrow> ('h1, ('h2, 't2) T) T \<Rightarrow> ('h3, 't2) T"
  "collapse2 f == collapse (% h1 . hMap (f h1))"

lemma collapse2_addH[simp]: "collapse2 f (addH h t) = hMap (f h) t"
by (simp add: collapse2_def)

lemma collapse2_hConc[simp]:
   "collapse2 f (hConc t1 t2) = hConc (collapse2 f t1) (collapse2 f t2)"
by (simp add: collapse2_def)

theorem collapse2_tFold2:
  "\<lbrakk> assoc c1; assoc c2;
     \<And> h1 h2 x . a1 h1 (a2 h2 x) = a3 (f h1 h2) x;
     \<And> h x y .   a1 h (c2 x y) = c1 (a1 h x) (a1 h y)
   \<rbrakk> \<Longrightarrow>
   tFold a1 c1 (tMap (tFold a2 c2) t) = tFold a3 c1 (collapse2 f t)"
apply (induct_tac t rule: T_induct, simp)
apply (induct_tac t0 rule: T_induct, simp_all)
done

theorem collapse2_tFold2_wrapped:
  "\<lbrakk> assoc c1; assoc c2; assoc c3;
     \<And> h1 h2 x . w1 (a1 h1 (a2 h2 x)) = w3 (a3 (f h1 h2) x);
     \<And> h x y   . w1 (a1 h (c2 x y)) = c4 (w1 (a1 h x)) (w1 (a1 h y));
     \<And> x y     . w1 (c1 x y) = c5 (w1 x) (w1 y);
(* These swapped equations look more intuitive, but destroy simplification:
     \<And> x y     . w3 (c3 x y) = c4 (w3 x) (w3 y);
     \<And> x y     . w3 (c3 x y) = c5 (w3 x) (w3 y)
*)
     \<And> x y     . c4 (w3 x) (w3 y) = w3 (c3 x y);
     \<And> x y     . c5 (w3 x) (w3 y) = w3 (c3 x y)
   \<rbrakk> \<Longrightarrow>
   w1 (tFold a1 c1 (tMap (tFold a2 c2) t)) = w3 (tFold a3 c3 (collapse2 f t))"
apply (induct_tac t rule: T_induct, simp)
apply (induct_tac t0 rule: T_induct, simp_all del: tFold_tMap)
done

subsection {* Compression *}

lemma hCompress_0:
  "\<lbrakk> assoc c;
     \<And> h1 h2 t1 t2 . c (a h1 t1) (a h2 t2) = a (c' h1 h2) (c'' t1 t2) 
   \<rbrakk> \<Longrightarrow>
   tFold a c (hCons (h1,t1) (hCons (h2,t2) t)) =
   tFold a c (hCons (c' h1 h2, c'' t1 t2) t)"
by (simp del: assoc add: assoc [THEN sym])

consts
  dim1addH :: "('h \<Rightarrow> 'c \<Rightarrow> 'v) \<Rightarrow> ('h \<Rightarrow> ('c,'u) T \<Rightarrow> 'v)"

defs
  dim1addH_def: "dim1addH a h == tFold (% c u . a h c) arbitrary"

lemma dim1addH[simp]: "dim1addH a h (cell c) = a h c"
by (simp add: dim1addH_def cell_def)

lemma hCompress_cells:
  "\<lbrakk> assoc c;
     \<And> h1 h2 g1 g2 . c (a h1 g1) (a h2 g2) = a (c' h1 h2) (c'' g1 g2) 
   \<rbrakk> \<Longrightarrow>
   tFold (dim1addH a) c (hCons (h1,cell g1) (hCons (h2,cell g2) t)) =
   tFold (dim1addH a) c (hCons (c' h1 h2, cell (c'' g1 g2)) t)"
by (simp del: assoc add: assoc [THEN sym])

subsection {* Elementary Transformations *}

text {*
The titles of the subsections here
are the structural elementary transformations as listed in \cite{Zucker-1996}.

The lemmas show the corresponding general properties for the first dimension;
for other dimensions; the corresponding properties can be obtained
using theorem @{text "tTranspose_tFold2"}.
*}

subsubsection {* Permuting two $(-1)$-slices with their corresponding header entries *}

lemma hCommute:
  "\<lbrakk> assoc c; commutative c \<rbrakk> \<Longrightarrow>
   tFold a c (hConc t1 t2) = tFold a c (hConc t2 t1)"
by (simp, erule commutative)


subsubsection {* Deleting a $(-1)$-slice with ``\textsf{false}'' in the corresponding header entry *}

text {* Since Zucker also does not allow empty tables,
this deletion is only possible for tables that are in the range of
@{text "hConc"}. *}

lemma hDelLeftUnitHeader:
  "\<lbrakk> assoc c; \<And> t1 b . c (a h1 t1) b = b \<rbrakk> \<Longrightarrow>
   tFold a c (hConc (addH h1 t1) t) = tFold a c t"
by simp

lemma hDelLeftUnitHeader_hCons:
  "\<lbrakk> assoc c; \<And> t1 b . c (a h1 t1) b = b \<rbrakk> \<Longrightarrow>
   tFold a c (hCons (h1,t1) t) = tFold a c t"
by simp

lemma hDelRightUnitHeader:
  "\<lbrakk> assoc c; \<And> t1 b . c b (a h1 t1) = b \<rbrakk> \<Longrightarrow>
   tFold a c (hConc t (addH h1 t1)) = tFold a c t"
by simp


subsubsection {* Deleting a principal slice with only ``\textsf{false}'' entries from an inverted table *}

lemma hDelLeftUnitSubtable:
  "\<lbrakk> assoc c; \<And> h1 b . c (a h1 t1) b = b \<rbrakk> \<Longrightarrow>
   tFold a c (hConc (addH h1 t1) t) = tFold a c t"
by simp

lemma hDelLeftUnitSubtable_hCons:
  "\<lbrakk> assoc c; \<And> h1 b . c (a h1 t1) b = b \<rbrakk> \<Longrightarrow>
   tFold a c (hCons (h1,t1) t) = tFold a c t"
by simp

lemma hDelRightUnitSubtable:
  "\<lbrakk> assoc c; \<And> h1 b . c b (a h1 t1) = b \<rbrakk> \<Longrightarrow>
   tFold a c (hConc t (addH h1 t1)) = tFold a c t"
by simp


subsubsection {* Splitting a principal slice by ``splitting a disjunction'' in the corresponding header in an inverted table *}

text {* This is strange: the corresponding header of a principal slice
in an inverted table is a value header!

Another thing to keep in mind here is that
splitting a condition header in a normal or inverted table may turn
a proper table into an improper table.
*}

lemma hSplitHeader:
  "\<lbrakk> assoc c; \<And> h1 h2 t . a (c' h1 h2) t = c (a h1 t) (a h2 t) \<rbrakk> \<Longrightarrow>
   tFold a c (addH (c' h1 h2) t) =
   tFold a c (hConc (addH h1 t) (addH h2 t))"
by simp

subsubsection {* Combining two or more principal slices with the same value header entry into a single slice in an inverted table *}

lemma hCombineEqualHeaders:
  "\<lbrakk> assoc c; \<And> h t1 t2 . c (a h t1) (a h t2) = a h (c' t1 t2) \<rbrakk> \<Longrightarrow>
   tFold a c (hConc (addH h t1) (addH h t2)) =
   tFold a c (addH h (c' t1 t2))"
by simp

end

Additional Properties of @{text "tFold"}

lemma tFold_const2_idempotent:

  [| assoc c; idempotent c |] ==> tFold (%h t. a) c t = a

lemma tFold_tFold_join:

  assoc c2
  ==> tFold a2 c2 (tFold (%h0 t0. addH (HH h h0 t0) (TT h h0 t0)) hConc t) =
      tFold (%h0 t0. a2 (HH h h0 t0) (TT h h0 t0)) c2 t

lemma tFold_tFold_hConc:

  assoc c2
  ==> tFold a2 c2 (tFold a1 hConc t) = tFold (%h0 t0. tFold a2 c2 (a1 h0 t0)) c2 t

lemma tFold_tFold_const:

  assoc c2
  ==> tFold a2 c2 (tFold a1 const t) =
      tFold (%h0 t0. tFold a2 c2 (a1 h0 t0)) const t

lemma f_tFold_const:

  f (tFold a const t) = tFold (%h0 t0. f (a h0 t0)) const t

lemma tFold_const_const:

  tFold (%h t. r) const t = r

lemma tFold_foldr1_hConc:

  assoc c ==> tFold a c (foldr1 hConc ts) = foldr1 c (map1 (tFold a c) ts)

lemma tFold_LRunit:

  [| !!h t. LRunit c (a h t); assoc c |] ==> tFold a c t = a arbitrary arbitrary

lemma tFold0_addH:

  tFold0 c (addH h t) = h

lemma tFold0_hConc:

  assoc c ==> tFold0 c (hConc t1 t2) = c (tFold0 c t1) (tFold0 c t2)

tFoldC

hHead

lemma hHead_addH:

  hHead (addH h t) = (h, t)

lemma hHead_uncurry_addH:

  hHead (uncurry addH p) = p

lemma hHead_hCons:

  hHead (hCons p t) = p

lemma hHead_hConc:

  hHead (hConc t1 t2) = hHead t1

lemma hLength_addH:

  hLength (addH h t) = 1

lemma hLength_hCons:

  hLength (hCons p t) = Suc (hLength t)

lemma hLength_hConc:

  hLength (hConc t1 t2) = hLength t1 + hLength t2

lemma hLength_pos:

  0 < hLength t

The ``Cons View''

lemma snd_hUnCons0_p:

  snd (hUnCons0 p1 p2) = hConc (snd p1) (snd p2)

lemma fst_hUnCons0_p:

  fst (hUnCons0 p1 p2) =
  (case fst p1 of Inl p => Inr (p, snd p2)
   | Inr (p, t) => Inr (p, hConc t (snd p2)))

lemma snd_hUnCons0:

  snd (hUnCons0 (r1, t1) (r2, t2)) = hConc t1 t2

lemma assoc_hUnCons0:

  assoc hUnCons0

lemma hUnCons1_addH:

  hUnCons1 (addH h t) = (Inl (h, t), addH h t)

lemma hUnCons1_hCons:

  hUnCons1 (hCons p t) = (Inr (p, t), hCons p t)

lemma hUnCons1_hConc:

  hUnCons1 (hConc t1 t2) = hUnCons0 (hUnCons1 t1) (hUnCons1 t2)

lemma snd_hUnCons1:

  snd (hUnCons1 t) = t

lemma hUnCons_addH:

  hUnCons (addH h t) = Inl (h, t)

lemma hUnCons_hCons:

  hUnCons (hCons p t) = Inr (p, t)

lemma hUnCons_hConc:

  hUnCons (hConc t1 t2) =
  (case hUnCons t1 of Inl p => Inr (p, t2) | Inr (p, t) => Inr (p, hConc t t2))

lemma tFoldr0_measure:

  ALL h t t'. (EX ta. hUnCons t = Inr ((h, ta), t')) --> hLength t' < hLength t

lemma tFoldr_addH:

  tFoldr a f (addH h t) = a h t

lemma tFoldr_hCons:

  tFoldr a f (hCons p t) = uncurry f p (tFoldr a f t)

lemma tFoldr_hConc:

  tFoldr a f (hConc t1 t2) = tFoldr (%h t. f h t (tFoldr a f t2)) f t1

lemma hConc_via_tFoldr:

  hConc t1 t2 = tFoldr (%h t. hCons (h, t) t2) (curry hCons) t1

lemma tFold_via_tFoldr:

  tFold a c t = tFoldr a (%h t. c (a h t)) t

Mapping

lemma tMap_addH:

  tMap f (addH h t) = addH h (f t)

lemma tMap_hConc:

  tMap f (hConc t1 t2) = hConc (tMap f t1) (tMap f t2)

lemma tMap_hCons:

  tMap f (hCons p t) = hCons (fst p, f (snd p)) (tMap f t)

lemma hMap_addH:

  hMap f (addH h t) = addH (f h) t

lemma hMap_hConc:

  hMap f (hConc t1 t2) = hConc (hMap f t1) (hMap f t2)

lemma hMap_hCons:

  hMap f (hCons p t) = hCons (f (fst p), snd p) (hMap f t)

lemma tFold_tMap:

  assoc c ==> tFold a c (tMap f t) = tFold (%h t0. a h (f t0)) c t

lemma tMap_tFold_hConc:

  tMap f (tFold a hConc t) = tFold (%h0 t0. tMap f (a h0 t0)) hConc t

lemma tMap_tMap:

  tMap f (tMap g t) = tMap (f o g) t

lemma tMap_const_tMap:

  tMap (const t1) (tMap f t) = tMap (const t1) t

lemma tMap_CONST_tMap:

  tMap (%x. t1) (tMap f t) = tMap (const t1) t

Headers and Subtables

lemma headers_addH:

  headers (addH h t) = singleton h

lemma headers_hCons:

  headers (hCons p t) = cons1 (fst p) (headers t)

lemma headers_hConc:

  headers (hConc t1 t2) = append (headers t1) (headers t2)

lemma subtables_addH:

  subtables (addH h t) = singleton t

lemma subtables_hCons:

  subtables (hCons p t) = cons1 (snd p) (subtables t)

lemma subtables_hConc:

  subtables (hConc t1 t2) = append (subtables t1) (subtables t2)

lemma headers_eq_singleton_0:

  headers t = singleton h --> (EX t0. t = addH h t0)

lemma headers_eq_singleton:

  headers t = singleton h ==> EX t0. t = addH h t0

lemma headers_eq_cons1_0:

  headers t1 = cons1 h hs --> (EX t0 t2. t1 = hCons (h, t0) t2 & headers t2 = hs)

lemma headers_eq_cons1:

  headers t1 = cons1 h hs ==> EX t0 t2. t1 = hCons (h, t0) t2 & headers t2 = hs

lemma headers_tMap:

  headers (tMap f t) = headers t

lemma headers_tFold_hConc:

  headers (tFold a hConc t) = tFold (%h t. headers (a h t)) append t

lemma tMap_CONST__headers:

  tMap (%x. c) t = foldr1 hConc (map1 (%h. addH h c) (headers t))

lemma tFold_CONST_hConc__headers:

  tFold (%h. c) hConc t = foldr1 hConc (map1 (%h. c ()) (headers t))

Regular Skeletons

lemma regSkelStep_addH:

  regSkelStep rs (addH h t) = option_map (Pair (singleton h)) (rs t)

lemma regSkelStep_hConc:

  regSkelStep rs (hConc t1 t2) =
  optThen (regSkelStep rs t1)
   (%p1. optThen (regSkelStep rs t2)
          (%p2. if snd p1 = snd p2 then Some (append (fst p1) (fst p2), snd p1)
                else None))

lemma regSkelStep_hCons:

  regSkelStep rs (hCons p t) =
  optThen (rs (snd p))
   (%hs2. optThen (regSkelStep rs t)
           (%p2. if hs2 = snd p2 then Some (cons1 (fst p) (fst p2), hs2)
                 else None))

lemma regSkelOuter1_addH:

  regSkelOuter1 (addH h t) = Some (singleton h)

lemma regSkelOuter1_hConc:

  regSkelOuter1 (hConc t1 t2) = Some (append (headers t1) (headers t2))

lemma regSkelOuter1_hCons:

  regSkelOuter1 (hCons p t) = Some (cons1 (fst p) (headers t))

lemma regSkelOuter2_addH:

  regSkelOuter2 (addH h t) = Some (singleton h, headers t)

lemma regSkelOuter2_hCons:

  regSkelOuter2 (hCons p t2) =
  optThen (regSkelOuter2 t2)
   (%p2. if headers (snd p) = snd p2 then Some (cons1 (fst p) (fst p2), snd p2)
         else None)

lemma regSkelOuter2_hConc:

  regSkelOuter2 (hConc t1 t2) =
  optThen (regSkelOuter2 t1)
   (%p1. optThen (regSkelOuter2 t2)
          (%p2. if snd p1 = snd p2 then Some (append (fst p1) (fst p2), snd p1)
                else None))

lemma regSkelOuter2_addH_eq_Some:

  regSkelOuter2 (addH h t) = Some (hs1, hs2)
  ==> hs1 = singleton h & hs2 = headers t

lemma regSkelOuter2_hConc_eq_Some:

  regSkelOuter2 (hConc t1 t2) = Some (hs1, hs2)
  ==> EX hs1a hs1b.
         append hs1a hs1b = hs1 &
         regSkelOuter2 t1 = Some (hs1a, hs2) & regSkelOuter2 t2 = Some (hs1b, hs2)

lemma regSkelOuter2_hCons_eq_Some:

  regSkelOuter2 (hCons p t2) = Some (hs1, hs2)
  ==> EX h1 t1 hs1b.
         p = (h1, t1) &
         hs1 = cons1 h1 hs1b &
         headers t1 = hs2 & regSkelOuter2 t2 = Some (hs1b, hs2)

lemma regSkelOuter2_eq_Some_0:

  ALL hs1 hs2. regSkelOuter2 t = Some (hs1, hs2) --> headers t = hs1

lemma regSkelOuter2_eq_Some:

  regSkelOuter2 t = Some (hs1, hs2) ==> headers t = hs1

lemma regSkelOuter2_tMap_const:

  regSkelOuter2 (tMap (const t2) t1) = Some (headers t1, headers t2)

lemma regSkelOuter2_tMap_CONST:

  regSkelOuter2 (tMap (%x. t2) t1) = Some (headers t1, headers t2)

lemma regSkelOuter2_tMap_h_0:

  [| !!t. headers (h t) = headers t; !!t. h (h t) = h t;
     !!t1 t2. h (hConc t1 t2) = hConc (h t1) (h t2) |]
  ==> ALL hs1 hs2.
         regSkelOuter2 t = Some (hs1, hs2) -->
         regSkelOuter2 (tMap h t) = Some (hs1, hs2)

lemma regSkelOuter2_tMap_h:

  [| !!t. headers (h t) = headers t; !!t. h (h t) = h t;
     !!t1 t2. h (hConc t1 t2) = hConc (h t1) (h t2);
     regSkelOuter2 t = Some (hs1, hs2) |]
  ==> regSkelOuter2 (tMap h t) = Some (hs1, hs2)

Two-Dimensional Regular Tables

lemma regularOuter2I:

  regSkelOuter2 t = Some (hs1, hs2) ==> regularOuter2 t

lemma regularOuter2:

  regularOuter2 t ==> EX hs1 hs2. regSkelOuter2 t = Some (hs1, hs2)

lemma regT2:

  regSkelOuter2 t = Some (hs1, hs2) ==> t : regT2

lemma regSkel2:

  regSkelOuter2 t = Some (hs1, hs2) ==> regSkel2 (Abs_regT2 t) = (hs1, hs2)

lemma reg2dim1:

  regSkelOuter2 t = Some (hs1, hs2) ==> reg2dim1 (Abs_regT2 t) = hs1

lemma reg2dim2:

  regSkelOuter2 t = Some (hs1, hs2) ==> reg2dim2 (Abs_regT2 t) = hs2

List Interface

lemma tList_addH:

  tList (addH h t) = singleton (h, t)

lemma tList_hConc:

  tList (hConc t1 t2) = append (tList t1) (tList t2)

lemma tList_hCons:

  tList (hCons p t2) = cons1 p (tList t2)

lemma tOfList_singleton:

  tOfList (singleton (h, t)) = addH h t

lemma tOfList_append:

  tOfList (append t1 t2) = hConc (tOfList t1) (tOfList t2)

lemma tOfList_cons1:

  tOfList (cons1 p ps) = hCons p (tOfList ps)

ZipWith

lemma tZipWith_A_A:

  tZipWith f (addH h1 t1) (addH h2 t2) = uncurry addH (f (h1, t1) (h2, t2))

lemma tZipWith_A_C:

  tZipWith f (addH h1 t1) (hCons p2 t2) = uncurry addH (f (h1, t1) p2)

lemma tZipWith_C_A:

  tZipWith f (hCons p1 t1) (addH h2 t2) = uncurry addH (f p1 (h2, t2))

lemma tZipWith_C_C:

  tZipWith f (hCons p1 t1) (hCons p2 t2) = hCons (f p1 p2) (tZipWith f t1 t2)

lemma tZipWith_A:

  tZipWith f (addH h1 t1) t2 = uncurry addH (f (h1, t1) (hHead t2))

lemma tZipWith_C:

  hHead (tZipWith f (hCons p1 t1) t2) = f p1 (hHead t2)

lemma tZipWith__A:

  tZipWith f t1 (addH h2 t2) = uncurry addH (f (hHead t1) (h2, t2))

lemma tZipWith__C:

  hHead (tZipWith f t1 (hCons p2 t2)) = f (hHead t1) p2

lemma tZipWith_assoc_0:

  assoc f
  ==> ALL t1 t2 t3.
         tZipWith f (tZipWith f t1 t2) t3 = tZipWith f t1 (tZipWith f t2 t3)

lemma assoc_tZipWith:

  assoc f ==> assoc (tZipWith f)

Collapsing

lemma collapse_addH:

  collapse f (addH h t) = f h t

lemma collapse_hConc:

  collapse f (hConc t1 t2) = hConc (collapse f t1) (collapse f t2)

lemma collapse2_addH:

  collapse2 f (addH h t) = hMap (f h) t

lemma collapse2_hConc:

  collapse2 f (hConc t1 t2) = hConc (collapse2 f t1) (collapse2 f t2)

theorem collapse2_tFold2:

  [| assoc c1; assoc c2; !!h1 h2 x. a1 h1 (a2 h2 x) = a3 (f h1 h2) x;
     !!h x y. a1 h (c2 x y) = c1 (a1 h x) (a1 h y) |]
  ==> tFold a1 c1 (tMap (tFold a2 c2) t) = tFold a3 c1 (collapse2 f t)

theorem collapse2_tFold2_wrapped:

  [| assoc c1; assoc c2; assoc c3;
     !!h1 h2 x. w1 (a1 h1 (a2 h2 x)) = w3 (a3 (f h1 h2) x);
     !!h x y. w1 (a1 h (c2 x y)) = c4 (w1 (a1 h x)) (w1 (a1 h y));
     !!x y. w1 (c1 x y) = c5 (w1 x) (w1 y); !!x y. c4 (w3 x) (w3 y) = w3 (c3 x y);
     !!x y. c5 (w3 x) (w3 y) = w3 (c3 x y) |]
  ==> w1 (tFold a1 c1 (tMap (tFold a2 c2) t)) = w3 (tFold a3 c3 (collapse2 f t))

Compression

lemma hCompress_0:

  [| assoc c; !!h1 h2 t1 t2. c (a h1 t1) (a h2 t2) = a (c' h1 h2) (c'' t1 t2) |]
  ==> tFold a c (hCons (h1, t1) (hCons (h2, t2) t)) =
      tFold a c (hCons (c' h1 h2, c'' t1 t2) t)

lemma dim1addH:

  dim1addH a h (cell c) = a h c

lemma hCompress_cells:

  [| assoc c; !!h1 h2 g1 g2. c (a h1 g1) (a h2 g2) = a (c' h1 h2) (c'' g1 g2) |]
  ==> tFold (dim1addH a) c (hCons (h1, cell g1) (hCons (h2, cell g2) t)) =
      tFold (dim1addH a) c (hCons (c' h1 h2, cell (c'' g1 g2)) t)

Elementary Transformations

Permuting two $(-1)$-slices with their corresponding header entries

lemma hCommute:

  [| assoc c; commutative c |]
  ==> tFold a c (hConc t1 t2) = tFold a c (hConc t2 t1)

Deleting a $(-1)$-slice with ``\textsf{false}'' in the corresponding header entry

lemma hDelLeftUnitHeader:

  [| assoc c; !!t1 b. c (a h1 t1) b = b |]
  ==> tFold a c (hConc (addH h1 t1) t) = tFold a c t

lemma hDelLeftUnitHeader_hCons:

  [| assoc c; !!t1 b. c (a h1 t1) b = b |]
  ==> tFold a c (hCons (h1, t1) t) = tFold a c t

lemma hDelRightUnitHeader:

  [| assoc c; !!t1 b. c b (a h1 t1) = b |]
  ==> tFold a c (hConc t (addH h1 t1)) = tFold a c t

Deleting a principal slice with only ``\textsf{false}'' entries from an inverted table

lemma hDelLeftUnitSubtable:

  [| assoc c; !!h1 b. c (a h1 t1) b = b |]
  ==> tFold a c (hConc (addH h1 t1) t) = tFold a c t

lemma hDelLeftUnitSubtable_hCons:

  [| assoc c; !!h1 b. c (a h1 t1) b = b |]
  ==> tFold a c (hCons (h1, t1) t) = tFold a c t

lemma hDelRightUnitSubtable:

  [| assoc c; !!h1 b. c b (a h1 t1) = b |]
  ==> tFold a c (hConc t (addH h1 t1)) = tFold a c t

Splitting a principal slice by ``splitting a disjunction'' in the corresponding header in an inverted table

lemma hSplitHeader:

  [| assoc c; !!h1 h2 t. a (c' h1 h2) t = c (a h1 t) (a h2 t) |]
  ==> tFold a c (addH (c' h1 h2) t) = tFold a c (hConc (addH h1 t) (addH h2 t))

Combining two or more principal slices with the same value header entry into a single slice in an inverted table

lemma hCombineEqualHeaders:

  [| assoc c; !!h t1 t2. c (a h t1) (a h t2) = a h (c' t1 t2) |]
  ==> tFold a c (hConc (addH h t1) (addH h t2)) = tFold a c (addH h (c' t1 t2))