Email Gateway (Mar 26 2023 at 16:28): Email Gateway (Mar 26 2023 at 16:28):From: "\"Brozius, W.F. (Wouter)\"" <cl-isabelle-users@lists.cam.ac.uk>
Hello,
I am trying to implement a proof in Isabelle with a fairly large case distinction (35^3 cases).
The lemma “model_rule” seemingly does not finish.
I have tried to change the proof by using simp in between cases: apply (simp; cases x; simp; cases y; simp; cases z; simp), but this still does not seem to work.
I am new to Isabelle so I do not know the best types and definitions to use, do you see a way to improve?
Greetings,
Wouter Brozius
Email Gateway (Mar 27 2023 at 05:28):From: Emin Karayel <me@eminkarayel.de>
Dear Wouter,
I have looked into your problem, a solution is to convert the problem into
something that can be solved by eval or normalization.
These are methods that use the code equations to solve the goal in the ML
runtime, which is a lot faster.
There may be multiple methods, to verify the problem, the attached solution
is just an example it converts the cases (possible values x,y,z) into a
list of triples of length 35^3 and checks each case using filter.
The attached file contains a proof of lemma model_rule (but is otherwise
the same as your file.)
On my machine, it was less than a second to verify.
Let me know whether this helps?
Best,
Emin
Email Gateway (Nov 04 2023 at 15:26):From: "\"Brozius, W.F. (Wouter)\"" <cl-isabelle-users@lists.cam.ac.uk>
Hello,
I am trying to implement a proof in Isabelle with a fairly large case distinction (35^3 cases).
The lemma "model_rule" seemingly does not finish.
I have tried to change the proof by using simp in between cases: apply (simp; cases x; simp; cases y; simp; cases z; simp), but this still does not seem to work.
I am new to Isabelle so I do not know the best types and definitions to use, do you see a way to improve?
Greetings,
Wouter Brozius
Last updated: Apr 20 2024 at 08:16 UTC