Theory NEList

Up to index of Isabelle/HOL/Tables

header {* Non-Empty Lists *}

theory NEList = Utils:

subsection {* Datatype Definition *}

typedef 'a neList = "{ xs :: 'a list . xs ~= [] }"
by auto

lemma Rep_neList_non_Nil[simp]: "Rep_neList x ~= []"
by (insert Rep_neList [of x], simp add: neList_def)

lemma neList_append[simp,intro?]:
 "\<lbrakk> xs : neList; ys : neList \<rbrakk> \<Longrightarrow> (xs @ ys) : neList"
by (simp add: neList_def)

lemma neList_map[simp,intro?]:
 "\<lbrakk> xs : neList \<rbrakk> \<Longrightarrow> (map f xs) : neList"
by (simp add: neList_def)

lemma neList_zipWith[simp,intro?]:
 "\<lbrakk> xs : neList; ys : neList \<rbrakk> \<Longrightarrow> (zipWith f xs ys) : neList"
apply (auto simp add: neList_def)
apply (cases xs, simp)
apply (cases ys, simp_all)
done

subsection {* Construction *}

constdefs
 singleton :: "'a \<Rightarrow> 'a neList"
 "singleton x == Abs_neList [x]"
 append :: "'a neList \<Rightarrow> 'a neList \<Rightarrow> 'a neList"
 "append xs ys == Abs_neList (Rep_neList xs @ Rep_neList ys)"
 cons1 :: "'a \<Rightarrow> 'a neList \<Rightarrow> 'a neList"
 "cons1 x xs == Abs_neList (x # Rep_neList xs)"

lemma singleton_inj: "singleton x = singleton y \<Longrightarrow> x = y"
apply (simp add: singleton_def Abs_neList_inverse)
apply (subgoal_tac "[x] = [y]")
  prefer 2
  apply (subst Abs_neList_inject [THEN sym])
  apply (simp add: neList_def)
  apply (simp add: neList_def)
  apply assumption
apply auto
done

lemma cons1:
 "cons1 x xs = append (singleton x) xs"
apply (unfold cons1_def)
apply (unfold append_def)
apply (unfold singleton_def)
apply (simp_all add: Abs_neList_inverse Rep_neList_inverse neList_def)
done

lemma cons1_inj: "cons1 x xs = cons1 y ys \<Longrightarrow> x = y & xs = ys"
apply (simp add: cons1_def Abs_neList_inverse)
apply (subgoal_tac "x # Rep_neList xs = y # Rep_neList ys")
  prefer 2
  apply (subst Abs_neList_inject [THEN sym])
  apply (simp add: neList_def)
  apply (simp add: neList_def)
  apply assumption
apply auto
apply (subst Rep_neList_inject [THEN sym])
apply assumption
done

lemma cons1_neq_tl[simp]: "cons1 x xs ~= xs"
apply (simp add: cons1_def singleton_def Abs_neList_inverse)
apply (cases "Rep_neList xs")
apply (auto simp add: neList_def Abs_neList_inverse)
done

lemma cons1_neq_singleton[simp]: "cons1 x xs ~= singleton y"
apply (simp add: cons1_def singleton_def Abs_neList_inverse)
apply (subst Abs_neList_inject)
apply (auto simp add: neList_def)
done

lemma singleton_neq_cons1[simp]: "singleton y ~= cons1 x xs"
apply (simp add: cons1_def singleton_def Abs_neList_inverse)
apply (subst Abs_neList_inject)
apply (auto simp add: neList_def)
apply (cases "Rep_neList xs")
apply (auto simp add: neList_def)
done

lemma append_neq_singleton[simp]: "append xs ys ~= singleton x"
apply (simp add: append_def singleton_def Abs_neList_inverse)
apply (subst Abs_neList_inject)
apply (auto simp add: neList_def)
apply (cases xs)
apply (cases ys)
apply (simp add: neList_def Abs_neList_inverse)
apply (case_tac ya, simp)
apply (case_tac y, simp_all)
done

lemma singleton_neq_append[simp]: "singleton x ~= append xs ys"
apply (simp add: append_def singleton_def Abs_neList_inverse)
apply (subst Abs_neList_inject)
apply (auto simp add: neList_def)
apply (cases xs)
apply (cases ys)
apply (simp add: neList_def Abs_neList_inverse)
apply (case_tac ya, simp)
apply (case_tac y, simp_all)
done

lemma append_inj2_0: "(append xs ys = append xs zs) = (ys = zs)"
apply (simp add: append_def Abs_neList_inverse)
apply (subst Abs_neList_inject)
apply (auto simp add: neList_def Rep_neList_inject [THEN iffD1])
done

lemma append_inj2: "append xs ys = append xs zs \<Longrightarrow> ys = zs"
by (rule append_inj2_0 [THEN iffD1])

lemma append_inj2_neq: "append xs ys ~= append xs zs \<Longrightarrow> ys ~= zs"
by (insert append_inj2_0, auto)

lemma append_inj2_conv: "ys = zs \<Longrightarrow> append xs ys = append xs zs"
by (insert append_inj2_0, auto)

lemma append_inj2_neq_conv: "ys ~= zs \<Longrightarrow> append xs ys ~= append xs zs"
by (insert append_inj2_0, auto)

lemma append_inj1_0: "(append xs zs = append ys zs) = (xs = ys)"
apply (simp add: append_def Abs_neList_inverse)
apply (subst Abs_neList_inject)
apply (auto simp add: neList_def Rep_neList_inject [THEN iffD1])
done

lemma append_inj1: "append xs zs = append ys zs \<Longrightarrow> xs = ys"
by (rule append_inj1_0 [THEN iffD1])

lemma append_inj1_neq: "append xs zs ~= append ys zs \<Longrightarrow> xs ~= ys"
by (insert append_inj1_0, auto)

lemma append_assoc[simp]:
 "append (append xs ys) zs = append xs (append ys zs)"
apply (unfold append_def)
apply (cases "xs")
apply (cases "ys")
apply (cases "zs")
apply (subgoal_tac "y @ ya : neList")
apply (subgoal_tac "ya @ yb : neList")
apply (simp add: Abs_neList_inverse)
apply (unfold neList_def, simp_all)
done

lemma assoc_append[simp]: "assoc append"
by (rule assoc_intro, simp)

subsection {* foldr1 *}

constdefs
 foldr1 :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a neList \<Rightarrow> 'a"
 "foldr1 f xs == foldr_1 (f, Rep_neList xs)"

lemma foldr1_singleton[simp]:
 "foldr1 f (singleton x) = x"
apply (unfold singleton_def)
apply (unfold foldr1_def)
apply (simp_all add: Abs_neList_inverse Rep_neList_inverse neList_def)
done

lemma foldr1_cons1[simp]:
 "foldr1 f (cons1 x xs) = f x (foldr1 f xs)"
apply (unfold cons1_def)
apply (unfold foldr1_def)
apply (simp_all add: Abs_neList_inverse Rep_neList_inverse neList_def)
done

lemma foldr1_append_distr[simp]:
 "assoc f \<Longrightarrow> foldr1 f (append xs ys) = f (foldr1 f xs) (foldr1 f ys)"
apply (cases "xs")
apply (cases "ys")
apply (unfold append_def)
apply (unfold foldr1_def)
apply (cases "Rep_neList xs")
prefer 2
apply (cases "Rep_neList ys")
apply (simp_all add: Abs_neList_inverse Rep_neList_inverse neList_def
                del: foldr_1_cons)
apply (insert foldr_1_append_distr [of "Rep_neList xs" "Rep_neList ys" f, THEN sym])
apply (simp_all add: Abs_neList_inverse Rep_neList_inverse neList_def
                del: foldr_1_cons)
done

subsection {* map *}

constdefs
  map1 :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a neList \<Rightarrow> 'b neList"
  "map1 f xs == Abs_neList (map f (Rep_neList xs))"

lemma map1_singleton[simp]:
  "map1 f (singleton x) = singleton (f x)"
apply (unfold singleton_def)
apply (unfold map1_def)
apply (simp_all add: Abs_neList_inverse Rep_neList_inverse neList_def)
done

lemma map1_cons1[simp]:
  "map1 f (cons1 x xs) = cons1 (f x) (map1 f xs)"
apply (unfold cons1_def)
apply (unfold map1_def)
apply (simp_all add: Abs_neList_inverse Rep_neList_inverse neList_def)
done

lemma map1_append_distr[simp]:
 "map1 f (append xs ys) = append (map1 f xs) (map1 f ys)"
apply (cases "xs")
apply (cases "ys")
apply (unfold append_def)
apply (unfold map1_def)
apply (cases "Rep_neList xs")
prefer 2
apply (cases "Rep_neList ys")
apply (simp_all add: Abs_neList_inverse Rep_neList_inverse neList_def
                del: foldr_1_cons)
done

lemma map1_contract_comp:
 "map1 f (map1 g xs) = map1 (f o g) xs"
apply (unfold map1_def)
apply (cases "xs")
apply (cases "Rep_neList xs")
apply (simp_all add: Abs_neList_inverse Rep_neList_inverse neList_def map_compose
                del: foldr_1_cons)
done

lemma map1_comp:
 "(map1 f) o (map1 g) = map1 (f o g)"
by (simp add: comp_def map1_contract_comp)

subsection {* Induction *}

lemma neList_patterns:
  "(EX x . xs = singleton x) | (EX y ys . xs = append (singleton y) ys)"
apply (cases "xs")
apply (cases "Rep_neList xs")
apply (simp_all add: Abs_neList_inverse Rep_neList_inverse neList_def
                del: foldr_1_cons)
apply (cases "tl (Rep_neList xs)")
apply (unfold singleton_def)
apply (rule disjI1)
apply (rule exI)
apply (simp add: Abs_neList_inverse Rep_neList_inverse neList_def
                del: foldr_1_cons)
apply (rule disjI2)
apply (rule_tac x="a" in exI)
apply (rule_tac x="Abs_neList list" in exI)
apply (unfold append_def)
apply (simp add: Abs_neList_inverse Rep_neList_inverse neList_def
                del: foldr_1_cons)
done

lemma neList_list_induct:
 "(\<forall> x . P (singleton x)) \<longrightarrow>
  (\<forall> x y ys . P (Abs_neList (y # ys)) \<longrightarrow> P (Abs_neList (x # y # ys))) \<longrightarrow>
  (\<forall> z . P (Abs_neList (z # zs)))"
apply (induct_tac zs)
apply (simp add: Abs_neList_inverse Rep_neList_inverse neList_def singleton_def
                del: foldr_1_cons)
apply (intro strip)
apply simp
done

lemma neList_cons_induct_0:
 "\<lbrakk>\<And>x . P (singleton x); \<And>x xs. P xs \<Longrightarrow> P (cons1 x xs)\<rbrakk>
  \<Longrightarrow> P zs"
apply (insert neList_patterns [of zs])
apply (simp only: cons1)
apply (erule disjE)
apply (erule exE)
apply simp
apply (erule exE)
apply (erule exE)
apply (insert neList_list_induct [of P "tl (Rep_neList zs)"])
apply simp
apply (subgoal_tac "\<forall>x y ys. P (Abs_neList (y # ys)) \<longrightarrow> P (Abs_neList (x # y # ys))")
  prefer 2
  apply (intro strip)
  apply (subgoal_tac "P (singleton x)")
    prefer 2
    apply simp
  apply (subgoal_tac "P (append (singleton x) (Abs_neList (ya # ysa)))")
    prefer 2
    apply simp
  apply (subgoal_tac "Abs_neList (x # ya # ysa) = append (singleton x) (Abs_neList (ya # ysa))")
    prefer 2
    apply (simp (no_asm_simp) add: Abs_neList_inverse Rep_neList_inverse neList_def singleton_def append_def
                del: foldr_1_cons)
  apply simp
apply simp
apply (drule_tac x=y in spec)
apply (simp add: Abs_neList_inverse Rep_neList_inverse neList_def singleton_def append_def
                del: foldr_1_cons)
done

lemma neList_cons_induct:
 "\<And> zs . \<lbrakk>\<And>x . P (singleton x); \<And>x xs. P xs \<Longrightarrow> P (cons1 x xs)\<rbrakk>
  \<Longrightarrow> P zs"
by (rule neList_cons_induct_0, auto)

lemma neList_cons_inductA:
 "\<lbrakk>\<And>x . P (singleton x); \<And>x xs. P xs \<Longrightarrow> P (cons1 x xs)\<rbrakk>
  \<Longrightarrow> ALL zs . P zs"
by (intro strip, rule neList_cons_induct, simp_all)

lemma neList_append_induct_0:
 "\<lbrakk>\<And>x . P (singleton x); \<And>xs ys. P xs \<Longrightarrow> P ys \<Longrightarrow> P (append xs ys)\<rbrakk>
  \<Longrightarrow> P zs"
apply (insert neList_patterns [of zs])
apply (erule disjE)
apply (erule exE)
apply simp
apply (erule exE)
apply (erule exE)
apply (insert neList_list_induct [of P "tl (Rep_neList zs)"])
apply simp
apply (subgoal_tac "\<forall>x y ys. P (Abs_neList (y # ys)) \<longrightarrow> P (Abs_neList (x # y # ys))")
  prefer 2
  apply (intro strip)
  apply (subgoal_tac "P (singleton x)")
    prefer 2
    apply simp
  apply (subgoal_tac "P (append (singleton x) (Abs_neList (ya # ysa)))")
    prefer 2
    apply simp
  apply (subgoal_tac "Abs_neList (x # ya # ysa) = append (singleton x) (Abs_neList (ya # ysa))")
    prefer 2
    apply (simp (no_asm_simp) add: Abs_neList_inverse Rep_neList_inverse neList_def singleton_def append_def
                del: foldr_1_cons)
  apply simp
apply simp
apply (drule_tac x=y in spec)
apply (simp add: Abs_neList_inverse Rep_neList_inverse neList_def singleton_def append_def
                del: foldr_1_cons)
done

lemma neList_append_induct:
 "\<And> zs . \<lbrakk>\<And>x . P (singleton x); \<And>xs ys. P xs \<Longrightarrow> P ys \<Longrightarrow> P (append xs ys)\<rbrakk>
  \<Longrightarrow> P zs"
by (rule neList_append_induct_0, auto)

subsection {* Elements *}

constdefs
 elem :: "'a \<Rightarrow> 'a neList \<Rightarrow> bool"
 "elem x xs == x mem (Rep_neList xs)"

lemma elem_singleton[simp]:
 "elem x (singleton y) = (x = y)"
apply (simp add: Abs_neList_inverse Rep_neList_inverse neList_def singleton_def elem_def
                del: foldr_1_cons)
apply fast
done

lemma elem_append[simp]:
 "elem x (append xs ys) = (elem x xs | elem x ys)"
by (simp add: Abs_neList_inverse Rep_neList_inverse neList_def elem_def append_def
                del: foldr_1_cons)

constdefs
 set1 :: "'a neList \<Rightarrow> 'a set"
 "set1 xs == set (Rep_neList xs)"

lemma set1_singleton[simp]:
 "set1 (singleton x) = { x }"
by (simp add: Abs_neList_inverse Rep_neList_inverse neList_def singleton_def set1_def
                del: foldr_1_cons)

lemma set1_append[simp]:
 "set1 (append xs ys) = set1 xs Un set1 ys"
apply (subgoal_tac "(Rep_neList xs @ Rep_neList ys) : neList")
apply (simp add: Abs_neList_inverse Rep_neList_inverse neList_def append_def set1_def
                del: foldr_1_cons)
apply (cases xs)
apply (simp add: Abs_neList_inverse Rep_neList_inverse neList_def elem_def append_def
                del: foldr_1_cons)
done

subsection {* neFold *}

constdefs
 neFold :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a neList \<Rightarrow> 'b"
 "neFold s c xs == foldr1 c (map1 s xs)"

lemma neFold_singleton[simp]:
 "neFold s c (singleton x) = s x"
by (simp add: neFold_def)

lemma neFold_cons1[simp]:
 "neFold s c (cons1 x xs) = c (s x) (neFold s c xs)"
by (simp add: neFold_def)

lemma neFold_append[simp]:
 "assoc c \<Longrightarrow> neFold s c (append xs ys) = c (neFold s c xs) (neFold s c ys)"
by (simp add: neFold_def)

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

subsection {* ZipWith *}

constdefs
 zipWith1 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a neList \<Rightarrow> 'b neList \<Rightarrow> 'c neList"
 "zipWith1 f xs ys == Abs_neList (zipWith f (Rep_neList xs) (Rep_neList ys))"

lemma zipWith1_S_S[simp]:
 "zipWith1 f (singleton x) (singleton y) = singleton (f x y)"
by (simp add: Abs_neList_inverse Rep_neList_inverse neList_def singleton_def zipWith1_def)

lemma zipWith1_S_C[simp]:
 "zipWith1 f (singleton x) (cons1 y ys) = singleton (f x y)"
by (simp add: Abs_neList_inverse Rep_neList_inverse neList_def singleton_def cons1_def append_def zipWith1_def)

lemma zipWith1_C_S[simp]:
 "zipWith1 f(cons1 x xs) (singleton y) = singleton (f x y)"
by (simp add: Abs_neList_inverse Rep_neList_inverse neList_def singleton_def cons1_def append_def zipWith1_def)

lemma zipWith1_C_C[simp]:
 "zipWith1 f(cons1 x xs) (cons1 y ys) = cons1 (f x y) (zipWith1 f xs ys)"
apply (subgoal_tac "zipWith f (Rep_neList xs) (Rep_neList ys) : neList")
apply (simp add: Abs_neList_inverse Rep_neList_inverse neList_def singleton_def cons1_def append_def zipWith1_def)
apply (cases xs, simp)
apply (cases ys, simp)
apply (simp_all add: Abs_neList_inverse)
done

lemma zipWith1_assoc[simp]:
 "assoc f \<Longrightarrow> zipWith1 f (zipWith1 f xs ys) zs = zipWith1 f xs (zipWith1 f ys zs)"
apply (simp add: zipWith1_def)
apply (cases xs, simp)
apply (cases ys, simp)
apply (cases zs, simp)
apply (simp_all add: Abs_neList_inverse)
done

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

text {* Attempting a direct proof of this associativity, not using associativity of zipWith: *}

lemma zipWith1_assoc_2[simp]:
 "assoc f \<Longrightarrow>
  ALL xs ys zs . zipWith1 f (zipWith1 f xs ys) zs = zipWith1 f xs (zipWith1 f ys zs)"
apply (rule neList_cons_inductA)
apply (rule neList_cons_inductA)
apply simp_all
apply (rule neList_cons_inductA)
apply simp_all
apply (rule neList_cons_inductA)
apply simp_all
done

lemma zipWith1_assoc_1[simp]:
 "assoc f \<Longrightarrow>
  ALL ys zs . zipWith1 f (zipWith1 f xs ys) zs = zipWith1 f xs (zipWith1 f ys zs)"
apply (induct_tac xs rule: neList_cons_induct)
apply simp
apply (rule allI)
apply (induct_tac ys rule: neList_cons_induct)
apply (simp add: cons1)
apply (rule allI)
apply (induct_tac zs rule: neList_cons_induct)
apply (simp_all add: cons1)
done

lemma zipWith1_assoc_3[simp]:
 "assoc f \<Longrightarrow>
  zipWith1 f (zipWith1 f xs ys) zs = zipWith1 f xs (zipWith1 f ys zs)"
apply (induct_tac xs rule: neList_cons_induct)
apply simp
apply (induct_tac ys rule: neList_cons_induct)
apply (simp add: cons1)
apply (induct_tac zs rule: neList_cons_induct)
apply (simp_all add: cons1)
done

subsection {* Other Properties *}

lemma foldr1_map1_LRunit[simp]:
  "\<lbrakk> \<And> x . LRunit f (u x); assoc f \<rbrakk> \<Longrightarrow>
   foldr1 f (map1 u xs) = u arbitrary"
apply (induct_tac xs rule: neList_append_induct, simp_all)
apply (rule LRunit_equal [of f], simp_all add: LRunit_left LRunit_right)
done

end

Datatype Definition

lemma Rep_neList_non_Nil:

  Rep_neList x ~= []

lemma neList_append:

  [| xs : neList; ys : neList |] ==> xs @ ys : neList

lemma neList_map:

  xs : neList ==> map f xs : neList

lemma neList_zipWith:

  [| xs : neList; ys : neList |] ==> zipWith f xs ys : neList

Construction

lemma singleton_inj:

  singleton x = singleton y ==> x = y

lemma cons1:

  cons1 x xs = append (singleton x) xs

lemma cons1_inj:

  cons1 x xs = cons1 y ys ==> x = y & xs = ys

lemma cons1_neq_tl:

  cons1 x xs ~= xs

lemma cons1_neq_singleton:

  cons1 x xs ~= singleton y

lemma singleton_neq_cons1:

  singleton y ~= cons1 x xs

lemma append_neq_singleton:

  append xs ys ~= singleton x

lemma singleton_neq_append:

  singleton x ~= append xs ys

lemma append_inj2_0:

  (append xs ys = append xs zs) = (ys = zs)

lemma append_inj2:

  append xs ys = append xs zs ==> ys = zs

lemma append_inj2_neq:

  append xs ys ~= append xs zs ==> ys ~= zs

lemma append_inj2_conv:

  ys = zs ==> append xs ys = append xs zs

lemma append_inj2_neq_conv:

  ys ~= zs ==> append xs ys ~= append xs zs

lemma append_inj1_0:

  (append xs zs = append ys zs) = (xs = ys)

lemma append_inj1:

  append xs zs = append ys zs ==> xs = ys

lemma append_inj1_neq:

  append xs zs ~= append ys zs ==> xs ~= ys

lemma append_assoc:

  append (append xs ys) zs = append xs (append ys zs)

lemma assoc_append:

  assoc append

foldr1

lemma foldr1_singleton:

  foldr1 f (singleton x) = x

lemma foldr1_cons1:

  foldr1 f (cons1 x xs) = f x (foldr1 f xs)

lemma foldr1_append_distr:

  assoc f ==> foldr1 f (append xs ys) = f (foldr1 f xs) (foldr1 f ys)

map

lemma map1_singleton:

  map1 f (singleton x) = singleton (f x)

lemma map1_cons1:

  map1 f (cons1 x xs) = cons1 (f x) (map1 f xs)

lemma map1_append_distr:

  map1 f (append xs ys) = append (map1 f xs) (map1 f ys)

lemma map1_contract_comp:

  map1 f (map1 g xs) = map1 (f o g) xs

lemma map1_comp:

  map1 f o map1 g = map1 (f o g)

Induction

lemma neList_patterns:

  (EX x. xs = singleton x) | (EX y ys. xs = append (singleton y) ys)

lemma neList_list_induct:

  (ALL x. P (singleton x)) -->
  (ALL x y ys. P (Abs_neList (y # ys)) --> P (Abs_neList (x # y # ys))) -->
  (ALL z. P (Abs_neList (z # zs)))

lemma neList_cons_induct_0:

  [| !!x. P (singleton x); !!x xs. P xs ==> P (cons1 x xs) |] ==> P zs

lemma neList_cons_induct:

  [| !!x. P (singleton x); !!x xs. P xs ==> P (cons1 x xs) |] ==> P zs

lemma neList_cons_inductA:

  [| !!x. P (singleton x); !!x xs. P xs ==> P (cons1 x xs) |] ==> ALL zs. P zs

lemma neList_append_induct_0:

  [| !!x. P (singleton x); !!xs ys. [| P xs; P ys |] ==> P (append xs ys) |]
  ==> P zs

lemma neList_append_induct:

  [| !!x. P (singleton x); !!xs ys. [| P xs; P ys |] ==> P (append xs ys) |]
  ==> P zs

Elements

lemma elem_singleton:

  elem x (singleton y) = (x = y)

lemma elem_append:

  elem x (append xs ys) = (elem x xs | elem x ys)

lemma set1_singleton:

  set1 (singleton x) = {x}

lemma set1_append:

  set1 (append xs ys) = set1 xs Un set1 ys

neFold

lemma neFold_singleton:

  neFold s c (singleton x) = s x

lemma neFold_cons1:

  neFold s c (cons1 x xs) = c (s x) (neFold s c xs)

lemma neFold_append:

  assoc c ==> neFold s c (append xs ys) = c (neFold s c xs) (neFold s c ys)

lemma neFold_const_idempotent:

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

ZipWith

lemma zipWith1_S_S:

  zipWith1 f (singleton x) (singleton y) = singleton (f x y)

lemma zipWith1_S_C:

  zipWith1 f (singleton x) (cons1 y ys) = singleton (f x y)

lemma zipWith1_C_S:

  zipWith1 f (cons1 x xs) (singleton y) = singleton (f x y)

lemma zipWith1_C_C:

  zipWith1 f (cons1 x xs) (cons1 y ys) = cons1 (f x y) (zipWith1 f xs ys)

lemma zipWith1_assoc:

  assoc f ==> zipWith1 f (zipWith1 f xs ys) zs = zipWith1 f xs (zipWith1 f ys zs)

lemma assoc_zipWith1:

  assoc f ==> assoc (zipWith1 f)

lemma zipWith1_assoc_2:

  assoc f
  ==> ALL xs ys zs.
         zipWith1 f (zipWith1 f xs ys) zs = zipWith1 f xs (zipWith1 f ys zs)

lemma zipWith1_assoc_1:

  assoc f
  ==> ALL ys zs.
         zipWith1 f (zipWith1 f xs ys) zs = zipWith1 f xs (zipWith1 f ys zs)

lemma zipWith1_assoc_3:

  assoc f ==> zipWith1 f (zipWith1 f xs ys) zs = zipWith1 f xs (zipWith1 f ys zs)

Other Properties

lemma foldr1_map1_LRunit:

  [| !!x. LRunit f (u x); assoc f |] ==> foldr1 f (map1 u xs) = u arbitrary