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?

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`

.

Ahh, that works. Thanks a lot.

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.

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.

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.

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!

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
```

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…

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

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

this tells you where the execution is stalled

this is how I realized that the `i`

in `{(a,i). a ∈ x} `

was different from `i`

in the definition

Oh, okay, I see, thanks a lot!

Last updated: Nov 11 2024 at 04:22 UTC