Chengsong Tan (Apr 22 2024 at 13:48): Chengsong Tan (Apr 22 2024 at 13:48):Hi all,
I am looking for help in "typing the knots" of a theory file where I need to find a proof for getting from a larger lemma to its more compact version.
I have proven the lemma in which some predicate with a large definition(hundreds of conjuncts) has been expanded and explicitly separated as assumptions, and then I used it to prove its more compact form (which is needed later). The issue is that I cannot seem to turn one lemma into the other.
The giant lemma with a large number of assumptions looks like this:
lemma giant1:
assumes i0: "fact 0 about T"
and i1....
....
and i300 ...
shows "P T' "
proof
...
qed
The definition of P is the conjunction of most of the assumption facts:
definition P = i2 /\ ... /\ i300
The more compact lemma looks like this"
lemma smaller1: shows "[| P T; fact 0; fact 1 |] ==> P T'"
I cannot seem to find a sledgehammer proof from giant1 to smaller1 (timeout, even if more time given the one-liner would be unusable). Is there an exact way to manipulate the proof states so that proof of smaller1 can be derived from giant1?
See line 217, 1758 of the ILExp.thy file for the giant1 and smaller1 lemmas in the concrete problem.
ILExp.thy
BasicInvariants.thy
BuggyRules.thy
CoherenceProperties.thy
Transposed.thy
Thansk a lot!
Best wishes,
Chengsong
Last updated: May 08 2024 at 12:29 UTC