PLT-5369 - Simplification of some linorder instances #169
Conversation
hrajchert
force-pushed
the
hrajchert/scp-3505-small-fixes
branch
2 times, most recently
from
81e76e4
to
2f1fcc7
Compare
hrajchert
force-pushed
the
hrajchert/linorder-simplification
branch
from
ee8c6a7
to
4f4d5f5
Compare
hrajchert
force-pushed
the
hrajchert/scp-3505-small-fixes
branch
from
5694151
to
97fac7d
Compare
hrajchert
force-pushed
the
hrajchert/linorder-simplification
branch
from
4f4d5f5
to
22e262d
Compare
|
|
||
|
|
||
| definition "a \<le> b = less_eq_BS a b" | ||
| definition "a \<le> b = less_eq_BS' (innerListByteString a) (innerListByteString b)" |
There was a problem hiding this comment.
Like we discussed, it is better to have them as pattern matching and as fun rather than point-free and definition, because when using Isabelle interactively it expands worse, and also because definitions do not simplify by default whereas fun does, and fun generates many more lemmas for free
There was a problem hiding this comment.
If I try to do it with fun directly it fails to prove termination automatically.
I agree that this one in particular is the ugliest of the current definitions, but is still a step forward from previous code
| fun less_Party :: "Party \<Rightarrow> Party \<Rightarrow> bool" where | ||
| "less_Party a b = (\<not> (less_eq_Party b a))" | ||
| definition less_Party :: "Party \<Rightarrow> Party \<Rightarrow> bool" where | ||
| "less_Party a b \<longleftrightarrow> \<not> ( b \<le> a)" |
There was a problem hiding this comment.
If you can choose between having an abstract predicate that is not executable and something that is just a normal computable function, choosing the abstract predicate to save a parenthesis really isn't worth it. If it was a lemma, then I would understand, but it is just a function
There was a problem hiding this comment.
Not sure what you mean with something abstract that is not executable. This is exported as code as following:
The "simp problem" mentioned in a previous comment is easily solved here by the line directly below:
declare less_Party_def [simp add]
which adds the definition to the simp set. I'm using the principle of least power. If you can solve a problem two different ways, and one of them is simpler, the simpler tool should be used. I assume that is the reason why definition, primrec, fun and function exist in the first place, and a simple search by text in the Isabelle source code yields
7526 definition
819 primrec
2241 fun
1460 function
|
|
||
| definition "a < b = less_BS a b" | ||
| definition less_ByteString :: "ByteString \<Rightarrow> ByteString \<Rightarrow> bool" where | ||
| "less_ByteString a b \<longleftrightarrow> \<not> (b \<le> a)" |
| )" | ||
|
|
||
| definition less_ChoiceId :: "ChoiceId \<Rightarrow> ChoiceId \<Rightarrow> bool" where | ||
| "less_ChoiceId a b \<longleftrightarrow> \<not> (b \<le> a)" |
palas
changed the title
This PR is marked as Draft until PR 168 is merged.After applying the small fixes in PR 168 regarding the linorder instances, I saw that I could simplify them even further.