(*
 * Well farg, contrary to initial expectations, the logic in
 * AddWithRetentionAndNoJunkAlt1 does not deal with the duplicates issue in
 * that it does not retain the number of duplicates per each duplicated item.
 * I.e., the counterexample used at the end of retention-with-no-junk.rsl still
 * applies to this logic.  I.e., if o = 1 and l = [1, 1, 1, 1], the logic of
 * AddWithRetentionAndNoJunkAlt1 is true if l' = [1, 1, 1, 1, 2] or if l' = [1,
 * 2, 2, 2, 2].
 *
 * The upshot is that AddWithRetentionAndNoJunkAlt1 is just a waste of time,
 * since the clever bit in the AddWithRetentionAndNoJunk avoids the extra
 * forall.  What follows beyond Alt1 (Alt2, etc.) are some other good things,
 * worthy of the maybe discussion cited the "18dec04 Thoughts" section of
 * books/se/formal-spec.me
 *)

  obj Object;-- A la Java, this should be THE top object from which all inherit

  function AddWithRetentionAndNoJunkAlt1(
        o:Object, l:Object*, l':Object*) -> boolean =

    (*
     * The object to be added is in the output list.
     *)
    (o in l')

        and

    (*
     * Everything in the input list is in the output list.
     *)
    (forall (o in l) o in l')

        and

    (*
     * Everything in the output list is in the input list, except for the
     * newly-added object.
     *)
    (forall (o' in l') if o' != o then o' in l)

        and

    (*
     * The length of the output list is one greater than the length of the
     * input list.  This ensures no extra copies of the same object in the
     * output list, since the 'in' operator in the preceding logic is true if
     * one or more copies of the same object is in the output list.
     *)
    (#l' = #l + 1);


  (*
   * This version uses a NumberOfOccurrences aux function to nail down the
   * same-number-of-duplicates issue (hopefully).  The parenthetical hopefully
   * should stay until we prove the theorems that follow.
   *)
  function AddWithRetentionAndNoJunkAlt2(o:Object, l:Object*, l':Object*) = (
    (*
     * The object to be added is in the output list.
     *)
    (o in l')

        and

    (*
     * The number of occurrences of each item in the input list is the same as
     * in the output list.
     *)
    (forall (o in l) NumberOfOccurrences(o, l) =  NumberOfOccurrences(o, l'))

        and

    (*
     * The length of the output list is one greater than the length of the
     * input list.  We still need this here as a no-junk clause, since it
     * prevents things not in the input from being in the output.
     *)
    (#l' = #l + 1)
  );


  function NumberOfOccurrences(o:Object, l:Object*) =
    if #l = 0
    then 0
    else if o = l[1]
         then 1 + NumberOfOccurrences(o, l[2:#l])
	 else NumberOfOccurrences(o, l[2:#l]);


  object ObjectList =  Object*;

  (* The deal here is that just because the number of occurrences of all objects
   * in a particular list, l, is the same as the number of occurrences of those
   * same objects in another list, l', it does not mean that the length of the
   * lists are the same.  This is because l' could contain objects not in l
   * that never get considered. *)
  thm T1 = forall (l,l': ObjectList)
    not ( (forall (o in l) NumberOfOccurrences(o, l) =
                           NumberOfOccurrences(o, l'))
               =>

	   (#l = #l') );

  (* It does appear to be true that if we look at all objects, counting the
   * number of occurrences within any two lists ensures the lists are the same
   * length, because here we count the zero-occurrence cases in both lists. *)
  thm T2 = forall (o:Object) forall (l,l':ObjectList)
    (NumberOfOccurrences(o, l) = NumberOfOccurrences(o, l')) <=>
               (#l = #l');

  (* It would appear that even the stronger case is true, namely that having
   * the same number of occurrences of items in any two lists means the lists
   * are equal. *)
  thm T3 = forall (o:Object) forall (l,l':ObjectList)
    (NumberOfOccurrences(o, l) = NumberOfOccurrences(o, l')) <=>
               (l = l');


(*
 * And here's yet another approach to AddWithRetentionAndNoJunk that covers the
 * duplicate issues.  The approach here is to quantify over integer positions.
 * The funky thing about this is that it has the same semantics as constructive
 * append, since it requires that everything in l' be in the same position as
 * it is in l.  And though we don't force the newly-added item to be at the
 * end, there's no other choice given what's left to do.
 *)
  function AddWithRetentionAndNoJunkAlt3(o:Object, l:Object*, l':Object*) = (

    (o in l')

        and

    (forall (i in [1..#l]) l[i] = l'[i])

        and

    (#l' = #l + 1)    

  );


(*
 * And while we're at it, let's see how to use the NumberOfOccurrences function
 * in the unbounded quantification version.
 *)
  function AddWithRetentionAndNoJunkAlt436(o:Object, l:Object*, l':Object*) = (

    forall (o':Object)
        if o' != o
        then NumberOfOccurrences(o', l') = NumberOfOccurrences(o', l)
        else NumberOfOccurrences(o', l') = NumberOfOccurrences(o', l) + 1

  );

(*
 * Hmm, this looks pretty freaking sweet, assuming the strong equality thm
 * above is true.
 *)