Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] A (very) short Isabelle/HOL tutorial for the f...


view this post on Zulip Email Gateway (Aug 22 2022 at 11:46):

From: Thomas Genet <thomas.genet@irisa.fr>
Dear Isabelle users,

I wrote a 4 pages Isabelle/HOL tutorial for the functional programmer.
It is available here:

https://hal.inria.fr/hal-01208577v2

Any feedback and comments are welcome.

Best regards,

Thomas

view this post on Zulip Email Gateway (Aug 22 2022 at 11:46):

From: Makarius <makarius@sketis.net>
For me it is always interesting to see what needs to be explained on first
encounter.

The text reads a bit like a "script" for an interactive session, conducted
by the user or the presenter of a quick tutorial. It would be nice to see
online videos like that.

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 11:46):

From: Thomas Genet <thomas.genet@irisa.fr>
True, this could be better as a video tutorial. However, I do not feel
like doing this for the moment! :-)

Best,

Thomas

view this post on Zulip Email Gateway (Aug 22 2022 at 11:46):

From: Thomas Genet <thomas.genet@irisa.fr>
Dear Rustom,

you can define remove using "primrec" since it is a primitive recursive
function.

However, you should be able to define it using "fun" since "fun"
accepts a superset of functions, including primitive recursive ones.

Thomas

view this post on Zulip Email Gateway (Aug 22 2022 at 11:46):

From: Thomas Genet <thomas.genet@irisa.fr>
Yes, this is an error raised by Isabelle/HOL 2015...

I think that this has been pointed out by some other users of Isabelle.
Well, I guess so?

Thomas

view this post on Zulip Email Gateway (Aug 22 2022 at 11:46):

From: Thomas Genet <thomas.genet@irisa.fr>
OK, this is not an error. When defining functions with fun, the
termination has to be proved (it is not guaranteed by construction like
it is for primrec). The output states that the termination has been
proven automatically by using a termination order comparing the lenght
of the lists of the second argument of the function.

But, true, this should be clarified in the tutorial.

Thanks,

Thomas

view this post on Zulip Email Gateway (Aug 22 2022 at 11:47):

From: Rustom Mody <rustompmody@gmail.com>
Thanks for that Thomas!
Just one point -- I had to change the fun to primrec... Not sure I
understand why but saw that somewhere and tried

view this post on Zulip Email Gateway (Aug 22 2022 at 11:47):

From: Rustom Mody <rustompmody@gmail.com>
Well continuing I also get this when I put the first sledgehammer . Is it
expected?

Sledgehammering...
"spass": Try this: apply (simp add: member_rec(2)) (0.0 ms).
"cvc4": Try this: apply (simp add: member_rec(2)) (0.0 ms).
"z3": Try this: apply (simp add: member_rec(2)) (0.0 ms).
"remote_vampire": Internal error:
exception Match raised (line 407 of "~~/src/HOL/Tools/ATP/atp_proof.ML")

view this post on Zulip Email Gateway (Aug 22 2022 at 11:47):

From: Rustom Mody <rustompmody@gmail.com>
fun give this error

constants
remove :: "'a ⇒ 'a list ⇒ 'a list"
Found termination order: "(λp. length (snd p)) <mlex> {}"

view this post on Zulip Email Gateway (Aug 22 2022 at 11:47):

From: Rustom Mody <rustompmody@gmail.com>
On Mon, Oct 19, 2015 at 7:01 PM, Makarius <makarius@sketis.net> wrote:

On Mon, 19 Oct 2015, Thomas Genet wrote:

I wrote a 4 pages Isabelle/HOL tutorial for the functional programmer. It

is available here:

https://hal.inria.fr/hal-01208577v2

Any feedback and comments are welcome.

The text reads a bit like a "script" for an interactive session, conducted

by the user or the presenter of a quick tutorial. It would be nice to see
online videos like that.

When I reach there I'll make one :-) But for now...

For me it is always interesting to see what needs to be explained on first

encounter.

Programmers need a "Hello World" example to get off the ground.
Until I saw Thomas' example I could not understand that (or rather how)
Isabelle hops between define-mode (eg fun/primrec etc) and prove-mode
(lemma...apply... etc)

view this post on Zulip Email Gateway (Aug 22 2022 at 11:47):

From: Rustom Mody <rustompmody@gmail.com>
[I posted this earlier but it seems to have not appeared; since my posts on
this thread seem to be appearing I am reposting here]

Very new to Isabelle and theorem proving, so my questions may be stupid.
Please excuse!

I am interested in tools to help students with Dijkstra Scholten equational
logic
I find that there is one formalization in Maude:
https://www.ideals.illinois.edu/bitstream/handle/2142/11411/A%20Rewriting%20Decision%20Procedure%20for%20Dijkstra-Scholten's%20Syllogistic%20Logic%20with%20Complements.pdf?sequence=2
<https://www.ideals.illinois.edu/bitstream/handle/2142/11411/A%20Rewriting%20Decision%20Procedure%20for%20Dijkstra-Scholten%27s%20Syllogistic%20Logic%20with%20Complements.pdf?sequence=2>

Is redoing that in Isabelle a reasonable idea?

Regards
Rusi


Last updated: Nov 21 2024 at 12:39 UTC