# Theory List

Up to index of Isabelle/FOL/ex

theory List
imports Nat2
uses [List.ML]
begin

    (*  Title:      FOL/ex/list
        ID:         $Id: List.thy,v 1.7 2005/09/03 15:15:51 wenzelm Exp $
        Author:     Tobias Nipkow
        Copyright   1991  University of Cambridge
    *)

    header {* Examples of simplification and induction on lists *}

    theory List
    imports Nat2
    begin

    typedecl 'a list
    arities list :: ("term") "term"

    consts
       hd           :: "'a list => 'a"
       tl           :: "'a list => 'a list"
       forall       :: "['a list, 'a => o] => o"
       len          :: "'a list => nat"
       at           :: "['a list, nat] => 'a"
       Nil          :: "'a list"                          ("[]")
       Cons         :: "['a, 'a list] => 'a list"         (infixr "." 80)
       app          :: "['a list, 'a list] => 'a list"    (infixr "++" 70)

    axioms
     list_ind: "[| P([]);  ALL x l. P(l)-->P(x . l) |] ==> All(P)"

     forall_cong:
      "[| l = l';  !!x. P(x)<->P'(x) |] ==> forall(l,P) <-> forall(l',P')"

     list_distinct1: "~[] = x . l"
     list_distinct2: "~x . l = []"

     list_free:      "x . l = x' . l' <-> x=x' & l=l'"

     app_nil:        "[]++l = l"
     app_cons:       "(x . l)++l' = x .(l++l')"
     tl_eq:  "tl(m . q) = q"
     hd_eq:  "hd(m . q) = m"

     forall_nil: "forall([],P)"
     forall_cons: "forall(x . l,P) <-> P(x) & forall(l,P)"

     len_nil: "len([]) = 0"
     len_cons: "len(m . q) = succ(len(q))"

     at_0: "at(m . q,0) = m"
     at_succ: "at(m . q,succ(n)) = at(q,n)"

    ML {* use_legacy_bindings (the_context ()) *}

    end

theorem list_exh:

      [| P([]); !!x l. P(x . l) |] ==> All(P)

theorem append_assoc:

      (l1.0 ++ l2.0) ++ l3.0 = l1.0 ++ l2.0 ++ l3.0

theorem app_nil_right:

      l ++ [] = l

theorem app_eq_nil_iff:

      l1.0 ++ l2.0 = [] <-> l1.0 = [] ∧ l2.0 = []

theorem forall_app:

      forall(l ++ l', P) <-> forall(l, P) ∧ forall(l', P)

theorem forall_conj:

      forall(l, %x. P(x) ∧ Q(x)) <-> forall(l, P) ∧ forall(l, Q)

theorem forall_ne:

      l ≠ [] --> forall(l, P) <-> P(hd(l)) ∧ forall(tl(l), P)

theorem len_app:

      len(l1.0 ++ l2.0) = len(l1.0) + len(l2.0)

theorem at_app1:

      i < len(l1.0) --> at(l1.0 ++ l2.0, i) = at(l1.0, i)

theorem at_app_hd2:

      at(l1.0 ++ x . l2.0, len(l1.0)) = x