Great!. This is exactly what I want. Thanks for helping me out...:) I
located the file "CoIndDefLib" in the HOL folder "src/IndDef".. Is there
any documentation available regarding this file?
On Sun, May 13, 2018 at 6:04 AM, <michael.norr...@data61.csiro.au> wrote:
> If you want the coinductively defined streams predicate over lllist, you
> can write
>
>
>
> > CoIndDefLib.Hol_coreln `!a s. a IN A /\ streams A s ==> streams A
> (LCONS a s)`;
>
> <<HOL message: inventing new type variable names: 'a>>
>
> <<HOL message: Treating "A" as schematic variable>>
>
> val it =
>
> (⊢ ∀A a s. a ∈ A ∧ streams A s ⇒ streams A (a:::s),
>
> ⊢ ∀A streams'.
>
> (∀a0. streams' a0 ⇒ ∃a s. (a0 = a:::s) ∧ a ∈ A ∧ streams' s) ⇒
>
> ∀a0. streams' a0 ⇒ streams A a0,
>
> ⊢ ∀A a0. streams A a0 ⇔ ∃a s. (a0 = a:::s) ∧ a ∈ A ∧ streams A s):
>
>
>
> I think the last theorem of the triple is the cases theorem you want.
>
>
>
> Note that if you are going to define Stream with
>
>
>
> Stream L = LFILTER (\n. T) L
>
>
>
> You might as well write the equivalent
>
>
>
> Stream L = L
>
>
>
> Best wishes,
>
> Michael
>
>
>
>
>
>
>
> *From: *Waqar Ahmad <12phdwah...@seecs.edu.pk>
> *Date: *Saturday, 12 May 2018 at 05:45
>
> *To: *"Norrish, Michael (Data61, Acton)" <michael.norr...@data61.csiro.au>
> *Cc: *hol-info <hol-info@lists.sourceforge.net>
> *Subject: *Re: [Hol-info] Extension of Co-algebraic Datatype
>
>
>
> Thanks!. I understand that the working of LNIL and LCONS constructors
> since I'm exploring "llistTheory" for quite some time. To be very clear,
> I'm in the process of porting "stream theory" form Isabelle
> https://www.isa-afp.org/browser_info/current/HOL/HOL-Library/Stream.html which
> is formalized as coinductive "stream":
>
>
>
> codatatype (sset: 'a) stream =
>
> SCons (shd: 'a) (stl: "'a stream") (infixr "##" 65)
>
> for
>
> map: smap
>
> rel: stream_all2
>
>
>
> I can see that its datatype is very similar to lazy list (llistTheory)
> datatype so rather defining a new type I defined a function that returns
> the same 'a llist-typed (lazy) list as given to its input:
>
>
>
> *∀***L. Stream L = LFILTER (*λ*n. T) L:
>
>
>
> type_of ``stream``;
>
>
>
> ``:*α* llist -> *α* llist``:
>
>
>
>
>
> Later in Isabelle "stream theory", a coinductive set "streams" is defined
> based on "stream" datatype as:
>
>
>
> coinductive_set
>
> streams :: "'a set *⇒** * 'a stream set"
>
> for A :: "'a set"
>
> where
>
> Stream[intro!, simp, no_atp]: "[[a *∈*** A; s *∈*** streams A]] ⟹ a
> ## s *∈*** streams A"
>
> end
>
>
>
> Using llistTheory functions, I'm able to define a similar function as:
>
>
>
> *∀***A. streams A = IMAGE (*λ*a. Stream a) {llist_abs (*λ*n. SOME
> x) | x *∈*** A}:
>
>
>
> type_of ``streams``;
>
>
>
> ``:('a -> bool) -> 'a llist -> bool``:
>
>
>
> However, by using shallow embedding approach, I'm not able to use some
> essential properties that are accompanied when a new coinductive datatype
> is defined. For instance, if a streams datatype is define, I may have this
> property of form:
>
>
>
> streams.cases (Isabelle):
>
>
>
> a *∈*** streams A *⇒*** (? a s. a = a ##s *⇒** a **∈** A **⇒*
> * s **∈** *streams A *⇒*** P) *⇒*** P
>
>
>
> I'm having the issues of defining these types in HOL4. Is there any way
> that I can replicate the same in HOL4?
>
>
>
>
>
> On Mon, May 7, 2018 at 8:49 PM, <michael.norr...@data61.csiro.au> wrote:
>
> You can probably define a function of that type, but you can’t define a *
> *constructor** of that type for llist. (Contrast what I’d consider to
> be llist’s standard constructors, LNIL and LCONS. They have types α llist,
> and α -> α llist -> α llist respectively.)
>
>
>
> You said you wanted a stream type, does this mean you want a constructor
> for stream of type
>
>
>
> (α -> bool) -> α stream
>
>
>
> ?
>
>
>
> Such a constructor is not recursive, so I can just write
>
>
>
> Datatype`stream = SetConstructor (α -> bool)`
>
>
>
> The SetConstructor term then has the desired type.
>
>
>
> So I’m afraid I still don’t understand your question.
>
>
>
> Michael
>
>
>
> *From: *Waqar Ahmad <12phdwah...@seecs.edu.pk>
> *Date: *Monday, 7 May 2018 at 11:38
> *To: *"Norrish, Michael (Data61, Acton)" <michael.norr...@data61.csiro.au>
> *Cc: *hol-info <hol-info@lists.sourceforge.net>
> *Subject: *Re: [Hol-info] Extension of Co-algebraic Datatype
>
>
>
> Thanks for the explanation. Let me state it clearly. Can I write down a
> constructor of type
>
>
>
> (*α*** -> bool) -> *α* llist
>
>
>
>
>
>
>
> On Sun, May 6, 2018 at 8:39 PM, <michael.norr...@data61.csiro.au> wrote:
>
> I think you may be able to make your needs more precise by explicitly
> considering what your co-algebra would be.
>
>
>
> In particular, write down the type of the “general” destructor
>
>
>
> myType -> F(myType)
>
>
>
> For lazy lists, this is
>
>
>
> α llist -> (α # α llist) option
>
>
>
> For the co-algebraic numbers it’s
>
>
>
> num -> num option
>
>
>
> For arbitrarily (but finite)-branching trees, it’s
>
>
>
> Tree -> Tree list
>
>
>
> (If you change list to llist you get possibly infinitely branching trees.)
>
>
>
> In the lazy lists, this destructor might be called “HDTL”; in the numbers,
> it’s “predecessor”; in the trees it’s “children”. Because the types are
> co-algebraic each might be iterable an infinite number of times. (The
> corresponding destructors in the algebraic types are always well-founded.)
>
>
>
> What are the co-algebras for your desired types? I don’t think I’ve
> understood what you want, but it superficially appears as if you want
> dependent types, where you combine the type with some term-level predicate.
> That sort of thing is impossible to capture within a HOL type.
>
>
>
> Finally, I’m afraid that there is no general tool for defining
> co-algebraic types in HOL4 at the moment.
>
>
>
> Michael
>
>
>
> *From: *Waqar Ahmad via hol-info <hol-info@lists.sourceforge.net>
> *Reply-To: *Waqar Ahmad <12phdwah...@seecs.edu.pk>
> *Date: *Sunday, 6 May 2018 at 11:58
> *To: *hol-info <hol-info@lists.sourceforge.net>
> *Cc: *Waqar Ahmad <waqar.ah...@seecs.edu.pk>
> *Subject: *[Hol-info] Extension of Co-algebraic Datatype
>
>
>
> Hi,
>
>
>
> Lately, I've been exploring the HOL4 lazy list theory "llistTheory", which
> is developed based on the co-algebraic datatype. I understand that the
> datatype *'a llist *is derived as a subset of the option type * :num ->
> 'a option. * Now, I want to define a new datatype based on datatype 'a
> llist. For instance,
>
>
>
> P of 'a llist
>
>
>
> such that *P: 'a llist -> 'a stream*, where *'a stream* is essentially
> the similar datatype as *'a llist* but having different properties. In
> shallow embedding, I can define it by using filter function of llistTheory
> as:
>
>
>
>
>
> val Stream = Define `Stream L = LFILTER (\n:'a. T) L`;
>
>
>
> One way of defining the co-inductive datatype *stream* is to follow the
> same procedure as described in "llistTheory", which is quite cumbersome. Is
> there any alternate way similar to that of package "Hol_datatype"?
>
>
>
> Secondly, Is it possible to define a co-inductive datatype that takes a
> set type (:'a -> bool) and maps it to a set of type (:'a llist -> bool)? A
> similar function, in shallow embedding, I can think of is:
>
>
>
> val streams_def = Define
>
> `streams A = IMAGE (\a. Stream a) {llist_abs x | x IN A} `;
>
>
>
> where the function streams is of type (:num -> 'a option) ->bool -> 'a
> llist-> bool
>
>
>
> In some cases, the function *streams* doesn't suffice for modeling the
> correct behavior of streams related properties..
>
>
>
> Any suggestion or thoughts would be highly helpful...
>
>
>
>
>
>
>
>
>
>
>
>
>
> --
>
> Waqar Ahmad, Ph.D.
> Post Doc at Hardware Verification Group (HVG)
> Department of Electrical and Computer Engineering
> Concordia University, QC, Canada
> Web: http://save.seecs.nust.edu.pk/waqar-ahmad/
> [image:
> http://research.bournemouth.ac.uk/wp-content/uploads/2014/02/NUST_Logo2.png]
>
>
> ------------------------------------------------------------
> ------------------
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
>
>
>
> --
>
> Waqar Ahmad, Ph.D.
> Post Doc at Hardware Verification Group (HVG)
> Department of Electrical and Computer Engineering
> Concordia University, QC, Canada
> Web: http://save.seecs.nust.edu.pk/waqar-ahmad/
>
>
> ------------------------------------------------------------
> ------------------
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
>
>
>
> --
>
> Waqar Ahmad, Ph.D.
> Post Doc at Hardware Verification Group (HVG)
> Department of Electrical and Computer Engineering
> Concordia University, QC, Canada
> Web: http://save.seecs.nust.edu.pk/waqar-ahmad/
>
> ------------------------------------------------------------
> ------------------
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
Waqar Ahmad, Ph.D.
Post Doc at Hardware Verification Group (HVG)
Department of Electrical and Computer Engineering
Concordia University, QC, Canada
Web: http://save.seecs.nust.edu.pk/waqar-ahmad/
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
