There is no documentation I’m afraid, except that the interface and behaviour
is basically exactly the same as for IndDefLib, which is described in the
DESCRIPTION manual.
Michael
From: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Wednesday, 16 May 2018 at 06:11
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
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<mailto: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<mailto:12phdwah...@seecs.edu.pk>>
Date: Saturday, 12 May 2018 at 05:45
To: "Norrish, Michael (Data61, Acton)"
<michael.norr...@data61.csiro.au<mailto:michael.norr...@data61.csiro.au>>
Cc: hol-info
<hol-info@lists.sourceforge.net<mailto: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<mailto: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<mailto:12phdwah...@seecs.edu.pk>>
Date: Monday, 7 May 2018 at 11:38
To: "Norrish, Michael (Data61, Acton)"
<michael.norr...@data61.csiro.au<mailto:michael.norr...@data61.csiro.au>>
Cc: hol-info
<hol-info@lists.sourceforge.net<mailto: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<mailto: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<mailto:hol-info@lists.sourceforge.net>>
Reply-To: Waqar Ahmad
<12phdwah...@seecs.edu.pk<mailto:12phdwah...@seecs.edu.pk>>
Date: Sunday, 6 May 2018 at 11:58
To: hol-info
<hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>>
Cc: Waqar Ahmad <waqar.ah...@seecs.edu.pk<mailto: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/
[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<mailto: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<mailto: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<mailto: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
