Gergely Buday (Jan 27 2021 at 10:27): Gergely Buday (Jan 27 2021 at 10:27):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
Mathias Fleury (Jan 27 2021 at 11:02):Pattern matching on ints does not work, because they are not defined with constructors.
Manuel Eberl (Jan 27 2021 at 11:05):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).
Gergely Buday (Jan 27 2021 at 11:06):It also implies that I cannot do a case analysis on the value? Basically, case analysis and pattern matching is the same thing, right?
Manuel Eberl (Jan 27 2021 at 11:06):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.
Manuel Eberl (Jan 27 2021 at 11:06):Also you lose executability.
Manuel Eberl (Jan 27 2021 at 11:07):(Although it can be restored by giving a code equation.)
Manuel Eberl (Jan 27 2021 at 11:07):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.
Manuel Eberl (Jan 27 2021 at 11:07):Do you mean the case combinator? If yes, I think that also only works on constructor patterns.
Gergely Buday (Jan 27 2021 at 11:08):@Manuel Eberl yes, pattern matching as above, case analysis with the case keyword
Manuel Eberl (Jan 27 2021 at 11:08):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.
Manuel Eberl (Jan 27 2021 at 11:08):Probably checking phase or something like that.
Manuel Eberl (Jan 27 2021 at 11:09):(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.)
Mathias Fleury (Jan 27 2021 at 11:10):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.
Manuel Eberl (Jan 27 2021 at 11:10):Yeah but you would have to write the disambiguator and extend the exhaustiveness/non-overlappingness prover to handle that.
Manuel Eberl (Jan 27 2021 at 11:11):I mean, I'm sure it is feasible, but I don't think it's trivial.
Manuel Eberl (Jan 27 2021 at 11:11):Feel free to do it if you feel like it. :grinning:
Mathias Fleury (Jan 27 2021 at 11:13):My intuition says that it is not possible in general, but I might be wrong :surprise:
Manuel Eberl (Jan 27 2021 at 11:14):Ah, you meant ‘I am not sure’? Because you wrote ‘I am so sure’.
Mathias Fleury (Jan 27 2021 at 11:15):Sorry, typo…
Gergely Buday (Jan 27 2021 at 11:16):The simplifier handled well the if-then-else constructs. Probably they are less readable for humans but the simplifier is another beast.
Manuel Eberl (Jan 27 2021 at 11:17):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.
Manuel Eberl (Jan 27 2021 at 11:17):And proving exhaustiveness is probably impossible in general unless you have a ‘catch-all’ equation somewhere.
Manuel Eberl (Jan 27 2021 at 11:18):Probably wouldn't be terribly usable all in all…
Manuel Eberl (Jan 27 2021 at 11:18):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.
Manuel Eberl (Jan 27 2021 at 11:18):You can still derive versions without the if as derived simp rules.
Manuel Eberl (Jan 27 2021 at 11:19):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.
Manuel Eberl (Jan 27 2021 at 11:20):(In particular, you can then declare these as simprules and delete the original simp rule. I for one don't like it when ifs crop up somewhere without me explicitly telling them to.
Last updated: Dec 21 2024 at 16:20 UTC