Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Mon, 15 May 1995 12:40:22 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA116916384; Mon, 15 May 1995 05:13:04 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA116886362; Mon, 15 May 1995 05:12:43 -0600 Received: from dunlin.cl.cam.ac.uk (user lcp (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Mon, 15 May 1995 12:11:33 +0100 X-Mailer: exmh version 1.6 4/21/95 To: info-hol@leopard.cs.byu.edu, chou@cs.ucla.edu Subject: (in)finite sequences X-Uri: X-Face: "OrDM]eXxWpb;,!g'n)u!-ss/8qvWB4*r>rA5~IAaMPwt$YO^oBckRP3N&D0.K"wKN7B> E&BJ5P-gy=o">rX=;.8M:sNp55m9?O%dK#v4{5e#8=-q9FUHURBbRfE:g\DybYQW4~MkQ 13swsz`i*9}*8fy}.au9jo. Date: Mon, 15 May 1995 12:11:30 +0100 From: Lawrence C Paulson Message-Id: <"swan.cl.cam.:107210:950515111137"@cl.cam.ac.uk> First, some theory. Finite lists are usually formalized using a least fixedpoint. Using a greatest fixedpoint instead gives you a set containing both finite and infinite lists. The set of finite lists is a subset of this set of sequences, and structural induction is valid for finite lists. A proof principle suitable for the infinite lists is co-induction, which allows you to prove that two infinite lists are equal by exhibiting a bisimulation between them. Operations on the infinite lists can be expressed using co-recursion. Formalizing these ideas in higher-order logic is not trivial, but has been done to some extent in Isabelle/HOL. For discussion and details, please see the paper Co-induction and Co-recursion in Higher-Order Logic at URL http://www.cl.cam.ac.uk/Research/Reports/TR304-lcp-coinduction.ps.gz Larry Paulson