Stream: Beginner Questions

Topic: About AFP in Isabelle 2020

Hongjian Jiang (May 24 2023 at 20:18):

From the link https://www.isa-afp.org/help/, Isabelle 2021 - till now can use the components to install the afp(isabelle components -u /home/myself/afp/thys), so how to use it in Isabelle 2020?

Anybody can help that?

Wenda Li (May 25 2023 at 15:49):

In a Linux/Mac environment, you can directly add the AFP path to the file .isabelle/Isabelle2019/ROOTS (here it is for Isabelle2019). For example, the last line of my .isabelle/Isabelle2019/ROOTS is /Users/wenda/Workspace/afp2019/thys.

Hongjian Jiang (May 25 2023 at 17:45):

Ahh, that works. Thanks a lot.

Hongjian Jiang (May 25 2023 at 17:58):

BTW, it tell an error "Cannot start:
*** Unknown option "document_logo"
*** The error(s) above occurred in session entry "Sturm_Sequences" (line 3 of "/Users/sword/Downloads/afp-2023-03-16/thys/Sturm_Sequences/ROOT")
"
I see there is no logo in this thy.

Wenda Li (May 25 2023 at 18:09):

I guess the problem is due to the incompatibility between Isabelle2022 and Isabelle2020. Your downloaded AFP (afp-2023-03-16) is only guaranteed to be compatible with Isabelle 2022.

Hongjian Jiang (May 25 2023 at 19:23):

Yes, you are right. It's so strang that no 2020 version on the afp website. I downlowd a 2020-version from the github. It works. Thank you.

Gokul (Jul 09 2023 at 17:02):

Hi,
I am trying something rather simple, but can't see what is missing. Here is the code:

type_synonym atom = "char list"
type_synonym exatom = "(char list)* nat"
type_synonym trace = "atom set list"

fun M2b::"trace ⇒ nat ⇒((char list)*nat) set" where
"M2b [] i = {}" |
"M2b (x#xs) i = {(a,i). a ∈ x} ∪ (M2b xs (Suc i))"

value "(M2b ([{''s1''}]) (0::nat))"

I was expecting value to give me output: {(''s1'',0)}. But instead, I get an error: exception Match raised (line 233 of "generated code"). Please help!

Mathias Fleury (Jul 09 2023 at 17:09):

Always try value[simp] in those cases. You would find out that the definition does not do what you want:

lemma "(M2b ([{''s1''}]) (0::nat)) = {''s1''} × UNIV"
  by auto

Mathias Fleury (Jul 09 2023 at 17:10):

This version:

fun M2b::"trace ⇒ nat ⇒((char list)*nat) set" where
"M2b [] i = {}" |
"M2b (x#xs) i = ({a. a ∈ x} × {i}) ∪ (M2b xs (Suc i))"

seems to be executable…

Gokul (Jul 09 2023 at 17:12):

Thanks a lot, so any clue why the previous one did not work?

Mathias Fleury (Jul 09 2023 at 17:13):

value[simp] "(M2b ([{''s1''}]) (0::nat))"

Mathias Fleury (Jul 09 2023 at 17:13):

this tells you where the execution is stalled

Mathias Fleury (Jul 09 2023 at 17:14):

this is how I realized that the i in {(a,i). a ∈ x} was different from i in the definition

Gokul (Jul 09 2023 at 17:15):

Oh, okay, I see, thanks a lot!

Last updated: Apr 27 2024 at 20:14 UTC