Hi - I have this expression within a goal:

```
{if even n then (n, n div 2) else (n, 3 * n + 1) |n. True}
```

I would like to convince the proof to rewrite this as the union of two set comprehensions:

```
{(n, n div 2)|n. even n} \<union> {(n, 3*n+1|n. \<not> even n}
```

I have a lemma that proves this is safe in the general case:

```
lemma union_comprehension: "{if T then p else q| x. U} = ({p | x. U \<and> T} \<union> {q| x. U \<and> \<not> T})"
apply auto
done
```

However, I have tried `apply (subst union_comprehension)`

and similar things, but it isn't able to progress anything. I did try to rewrite this rule as a `fun`

but couldn't figure it out.

Thanks.

And of course within moments of posting, after an hour of scratching my head, I got it working. I had to make `union_comprehension`

much more specific to get it to unify.

```
lemma union_comprehension:
"{if T x then p x else q x| x. U x} =
({p x | x. U x \<and> T x} \<union> {q x| x. U x \<and> \<not> T x})"
apply auto
done
```

I do have a genuine follow-up question though. I'm writing a few of these lemmas that only exist to guide another proof. Is there any way to introduce them within the proof that they are used in? As sort of in-line once-off rules?

You should really switch to using Isar. Not only allows it to introduce these “local lemmas”; it also allows for much more readable proofs.

Wolfgang Jeltsch said:

You should really switch to using Isar. Not only allows it to introduce these “local lemmas”; it also allows for much more readable proofs.

OK. Thanks. I guess that's my "next thing" :D and will probably be a good excuse to tidy what I've got so far.

Wolfgang Jeltsch said:

You should really switch to using Isar. Not only allows it to introduce these “local lemmas”; it also allows for much more readable proofs.

What should I look at to learn isar? I have been working through https://isabelle.in.tum.de/doc/tutorial.pdf but it isn't really helping me to write proofs in isar.

Matthew Pocock said:

Wolfgang Jeltsch said:

What should I look at to learn isar? I have been working through https://isabelle.in.tum.de/doc/tutorial.pdf but it isn't really helping me to write proofs in isar.

Part I, Section 5 of Concrete Semantics?

http://concrete-semantics.org

For the original question: the issue is that you have the mark the dependencies in x, so:

```
lemma union_comprehension: "{if T x then p x else q x| x. U x} = ({p x | x. U x \<and> T x} \<union> {q x| x. U x \<and> \<not> T x})"
apply auto
done
lemma ‹A = {if even n then (n, n div 2) else (n, 3 * n + 1) |n. True}›
apply (subst union_comprehension)
```

Matthew Pocock said:

What should I look at to learn isar? I have been working through https://isabelle.in.tum.de/doc/tutorial.pdf but it isn't really helping me to write proofs in isar.

I think that’s the old tutorial. The best way of getting into Isabelle, in my opinion, is the `prog-prove`

tutorial, which is the very first piece of documentation listed on the documentation page of the Isabelle website and in the documentation panel of Isabelle/jEdit. From what I understand, it is a large excerpt from the first chapter of *Concrete Semantics*; so when @Yutaka Nagashima suggested to look at Part I, Section 5 of *Concrete Semantics*, he essentially suggested to look at Section 4 of the `prog-prove`

tutorial. :smile:

It happened several times recently that newcomers were looking at the old tutorial instead of `prog-prove`

. I wonder why that is, given that `prog-prove`

is listed first on the website and in Isabelle/jEdit and the old tutorial is listed under “Old Isabelle Manuals”. Do people just do a web search for “Isabelle tutorial” and find the old tutorial this way? @Matthew Pocock, how did you arrive at the old Isabelle tutorial?

If I was a beginner, I would probably also start with the tutorial, because it seems to be the best place to start ("Programming and Proving" does not really sound like an introduction)

Hmm, it’s *Programming and Proving in Isabelle/HOL*, which sounds to me like it would give a good overview about Isabelle/HOL. :man_shrugging:

true, but if I think of programming in Isabelle, I mostly think of ML, but… I don't really know

Wolfgang Jeltsch said:

It happened several times recently that newcomers were looking at the old tutorial instead of

`prog-prove`

. I wonder why that is

I hit the old tutorial both from google, and also perhaps google takes you to an older isabelle documentation page? Each time I googled for a tutorial and followed the links or the pages, it took me to the old tutorial. This is the first time I am seeing the `prog-prove`

tutorial, and only because I added `prog-prove`

into the google search term. It may be the first time google took me to the 2021 isabelle documentation page.

The `prog-prove`

tutorial has been in existence for a long time; so, even if you’re taken to, say, the Isabelle2021 documentation page, you should find it. What I can imagine is that, if you google for “Isabelle tutorial”, you are taken to the document that runs under the short name “Isabelle tutorial” but is unfortunately the outdated document.

Last updated: Dec 07 2023 at 08:19 UTC