In order to simplify multiplicative expressions I wrote

```
fun times :: "aexp ⇒ aexp ⇒ aexp" where
"times (N i) (N j) = N(i*j)"
| "times (N 0) a = (N 0)"
| "times (N 1) a = a"
| "times (N i) a = Times (N i) a"
| "times a (N 0) = (N 0)"
| "times a (N 1) = a"
| "times a (N i) = Times (N i) a"
| "times a1 a2 = Times a1 a2"
```

for that I got

```
Malformed definition:
Non-constructor pattern not allowed in sequential mode.
⋀a. times (N 0) a = N 0
```

According to

this need not be a concern as 0 is a constant. Is N being int => aexp instead of nat => aexp the problem?

Once I did this exercise and I vaguely remember that it is by no accident that this works only:

```
fun plus :: "aexp ⇒ aexp ⇒ aexp" where
"plus (N i⇩1) (N i⇩2) = N(i⇩1+i⇩2)" |
"plus (N i) a = (if i=0 then a else Plus (N i) a)" |
"plus a (N i) = (if i=0 then a else Plus a (N i))" |
"plus a⇩1 a⇩2 = Plus a⇩1 a⇩2"
```

with an if. From my ML intuition that might not be carried to HOL, constructor + constant is a neat idea in a pattern. Why is it not here?

The full file is Ex_3_4.thy

Pattern matching on ints does not work, because they are not defined with constructors.

Even pattern matching on nats is, well, you can do it, but it can cause some pain. If it's just 0 that you're matching on, that's fine, but if you're matching on e.g. 3 you have to write ‘f (Suc (Suc (Suc 0))) = …’ and you get equations for `0`

, `Suc 0`

, `Suc (Suc 0)`

, and `Suc (Suc (Suc (Suc n)))`

, which is a bit excessive.

The problem is that the function package only allows to match on constructor patterns and not on things like equality. It could, in principle, but it is not implemented (and would probably be quite a bit of work to implement now).

It also implies that I cannot do a case analysis on the value? Basically, case analysis and pattern matching is the same thing, right?

You can define functions with more complex matching (even conditional matching like in Haskell), but then you have to prove exhaustiveness and non-overlapping of patterns yourself. See the Function package documentation for more information on that.

Also you lose executability.

(Although it can be restored by giving a code equation.)

Gergely Buday said:

It also implies that I cannot do a case analysis on the value? Basically, case analysis and pattern matching is the same thing, right?

Not sure what you mean by that.

Do you mean the `case`

combinator? If yes, I think that also only works on constructor patterns.

@Manuel Eberl yes, pattern matching as above, case analysis with the `case`

keyword

I actually don't know how `case`

works exactly, it's a bit of black magic because you can write nested pattern matches with `case`

and they somehow get transformed magically into calls to specific `case`

combinators like `case_nat`

, `case_option`

etc.

Probably checking phase or something like that.

(And similar caveats apply for `case`

; if your `case`

expressions become too elaborate you can get an exponential blow up in the term size. I vaguely recall some other system having smarter case expressions; Isabelle's are rather simplistic.)

Manuel Eberl said:

The problem is that the function package only allows to match on constructor patterns and not on things like equality. It could, in principle, but it is not implemented (and would probably be quite a bit of work to implement now).

Not sure. The problem is that the function package does disambiguation on the patterns. If you add equality, I am ~~so~~ not sure that it is still possible.

Yeah but you would have to write the disambiguator and extend the exhaustiveness/non-overlappingness prover to handle that.

I mean, I'm sure it is feasible, but I don't think it's trivial.

Feel free to do it if you feel like it. :grinning:

My intuition says that it is not possible in general, but I might be wrong :surprise:

Ah, you meant ‘I am not sure’? Because you wrote ‘I am so sure’.

Sorry, typo…

The simplifier handled well the if-then-else constructs. Probably they are less readable for humans but the simplifier is another beast.

True, equality will probably cause some problems. To imitate what e.g. SML/Haskell do, you would have to add a precondition `≠ foo`

to every equation after an equation of the form `f foo = …`

except when the function package can statically prove that the thing is `≠ foo`

.

And proving exhaustiveness is probably impossible in general unless you have a ‘catch-all’ equation somewhere.

Probably wouldn't be terribly usable all in all…

Gergely Buday said:

The simplifier handled well the if-then-else constructs. Probably they are less readable for humans but the simplifier is another beast.

Yes, if-then-else works well. The conditional matching I mentioned is basically a similar way to get the same thing.

You can still derive versions without the `if`

as derived simp rules.

For instance, if you have `f x = (if x = 1 then foo else bar x)`

, you can prove e.g. `f 1 = foo`

and `x ≠ 1 ⟹ f x = bar x`

. That can sometimes come in useful.

(In particular, you can then declare these as `simp`

rules and delete the original `simp`

rule. I for one don't like it when `if`

s crop up somewhere without me explicitly telling them to.

Last updated: Sep 25 2022 at 23:25 UTC