Email Gateway (Aug 22 2022 at 11:46): 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
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
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
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
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
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
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
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")
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> {}"
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)
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: Apr 25 2024 at 20:15 UTC