Theory Table

Up to index of Isabelle/HOL/Tables

header {* The Table Datatype Definition *}

theory Table = NEList:

subsection {* Datatype and Primitive Operations *}

datatype ('h,'t) T = T "('h * 't) neList"

consts
 unT :: "('h,'t) T \<Rightarrow> ('h * 't) neList"

primrec
 unT_def[simp]: "unT (T ps) = ps"

constdefs
 addH :: "'h \<Rightarrow> 't \<Rightarrow> ('h,'t) T"
 "addH h t == T (singleton (h,t))"

constdefs
 hConc :: "('h,'t) T \<Rightarrow> ('h,'t) T \<Rightarrow> ('h,'t) T"
 "hConc t1 t2 == T (append (unT t1) (unT t2))"

lemma hConc_assoc[simp]: "hConc (hConc t1 t2) t3 = hConc t1 (hConc t2 t3)"
by (unfold hConc_def, simp)

lemma assoc_hConc[simp]: "assoc hConc"
by (rule assoc_intro, simp)

constdefs
 cell :: "'c \<Rightarrow> ('c, unit) T"
 "cell c == addH c ()"

subsection {* Folding and Induction via hConc *}

constdefs
 tFold :: "('h \<Rightarrow> 't \<Rightarrow> 'r) \<Rightarrow> ('r \<Rightarrow> 'r \<Rightarrow> 'r) \<Rightarrow> ('h,'t) T \<Rightarrow> 'r"
 "tFold h c t == neFold (uncurry h) c (unT t)"

lemma tFold_addH[simp]:
 "tFold ah c (addH h t) = ah h t"
by (simp add: tFold_def addH_def)

lemma tFold_hConc[simp]:
 "assoc c \<Longrightarrow> tFold h c (hConc t1 t2) = c (tFold h c t1) (tFold h c t2)"
by (simp add: tFold_def hConc_def)

lemma T_induct_0:
 "\<lbrakk>\<And>h t0 . P (addH h t0); \<And>t1 t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> P (hConc t1 t2)\<rbrakk>
  \<Longrightarrow> P t"
apply (cases t, simp)
apply (rule_tac zs=neList in neList_append_induct)
apply (subst surjective_pairing)
apply (simp only: addH_def)
apply (simp add: hConc_def)
apply (subgoal_tac "append xs ys = append (unT (T xs)) (unT (T ys))")
apply (simp (no_asm_simp) del: unT_def)
apply simp
done

lemma T_induct:
 "\<And> t . \<lbrakk>\<And>h t0 . P (addH h t0); \<And>t1 t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> P (hConc t1 t2)\<rbrakk>
  \<Longrightarrow> P t"
by (rule T_induct_0, auto)

subsection {* hCons *}

constdefs
  hCons :: "('h * 't) \<Rightarrow> ('h,'t) T \<Rightarrow> ('h,'t) T"
  "hCons p t1 == T (cons1 p (unT t1))"

lemma hCons:
  "hCons p t1 = hConc (uncurry addH p) t1"
proof -
 have "hCons p t1 = T (cons1 p (unT t1))" by (simp add: hCons_def)
 also have "\<dots> = T (append (singleton p) (unT t1))" by (simp add: cons1)
 also have "\<dots> = T (append (unT (T (singleton (fst p, snd p)))) (unT t1))" by simp
 also have "\<dots> = T (append (unT (addH (fst p) (snd p))) (unT t1))" by (simp add: addH_def)
 also have "\<dots> = hConc (addH (fst p) (snd p)) t1" by (simp add: hConc_def)
 also have "\<dots> = hConc (uncurry addH (fst p, snd p)) t1" by (simp del: surjective_pairing [THEN sym])
 also have "\<dots> = hConc (uncurry addH p) t1" by simp
 finally show ?thesis .
qed

lemma hCons_p:
  "hCons (h,t) t1 = hConc (addH h t) t1"
by (simp add: hCons)

lemma tFold_hCons[simp]:
 "tFold ah c (hCons p t) = c (uncurry ah p) (tFold ah c t)"
by (simp add: tFold_def hCons_def)

lemma T_cons_induct_0:
 "\<lbrakk>\<And>h t0 . P (addH h t0); \<And> p t2. P t2 \<Longrightarrow> P (hCons p t2)\<rbrakk>
  \<Longrightarrow> P t"
apply (cases t, simp)
apply (rule_tac zs=neList in neList_cons_induct)
apply (subst surjective_pairing)
apply (simp only: addH_def)
apply (subst surjective_pairing)
apply (simp add: hConc_def hCons_def addH_def)
apply (subgoal_tac "cons1 x xs = cons1 x (unT (T xs))")
apply (simp (no_asm_simp) del: unT_def)
apply simp
done

lemma T_cons_induct:
 "\<And> t .( \<lbrakk>\<And>h t0 . P (addH h t0); \<And> p t2. P t2 \<Longrightarrow> P (hCons p t2)\<rbrakk> \<Longrightarrow> P t )"
by (rule T_cons_induct_0, auto)


lemma T_cons_inductA:
 "\<lbrakk>\<And>h t0 . P (addH h t0); \<And> p t2. P t2 \<Longrightarrow> P (hCons p t2)\<rbrakk> \<Longrightarrow> ALL t . P t"
by (intro strip, rule T_cons_induct, simp_all)

lemma hConc_hCons[simp]: "hConc (hCons p t1) t2 = hCons p (hConc t1 t2)"
by (induct_tac t1 rule: T_cons_induct, simp_all add: hCons)


end

Datatype and Primitive Operations

lemma hConc_assoc:

  hConc (hConc t1 t2) t3 = hConc t1 (hConc t2 t3)

lemma assoc_hConc:

  assoc hConc

Folding and Induction via hConc

lemma tFold_addH:

  tFold ah c (addH h t) = ah h t

lemma tFold_hConc:

  assoc c ==> tFold h c (hConc t1 t2) = c (tFold h c t1) (tFold h c t2)

lemma T_induct_0:

  [| !!h t0. P (addH h t0); !!t1 t2. [| P t1; P t2 |] ==> P (hConc t1 t2) |]
  ==> P t

lemma T_induct:

  [| !!h t0. P (addH h t0); !!t1 t2. [| P t1; P t2 |] ==> P (hConc t1 t2) |]
  ==> P t

hCons

lemma hCons:

  hCons p t1 = hConc (uncurry addH p) t1

lemma hCons_p:

  hCons (h, t) t1 = hConc (addH h t) t1

lemma tFold_hCons:

  tFold ah c (hCons p t) = c (uncurry ah p) (tFold ah c t)

lemma T_cons_induct_0:

  [| !!h t0. P (addH h t0); !!p t2. P t2 ==> P (hCons p t2) |] ==> P t

lemma T_cons_induct:

  [| !!h t0. P (addH h t0); !!p t2. P t2 ==> P (hCons p t2) |] ==> P t

lemma T_cons_inductA:

  [| !!h t0. P (addH h t0); !!p t2. P t2 ==> P (hCons p t2) |] ==> ALL t. P t

lemma hConc_hCons:

  hConc (hCons p t1) t2 = hCons p (hConc t1 t2)