CODEWITHSUNDEEP
isabelle
Joachim Breitner
Joachim Breitner

Reputation: 25763

Simplify meta-universally quantified assumptions with equality

Sorry for not being able to come up with a shorter example.

I have a proof state of

 1. ⋀e1 T1 L e2 T2 G1.
       typing (G1 @ (x, U) # G2) e1 T1 ⟹
       typing (G1 @ G2) e1 T1 ⟹
       (⋀xa. xa |∉| L ⟹
              typing ((xa, T1) # G1 @ (x, U) # G2) (open e2 (exp_fvar xa))
               T2) ⟹
       (⋀xa G1a.
           xa |∉| L ⟹
           (xa, T1) # G1 = G1a ⟹
           x |∉| fv (open e2 (exp_fvar xa)) ⟹
           typing (G1a @ G2) (open e2 (exp_fvar xa)) T2) ⟹
       x |∉| fv e1 ⟹ x |∉| fv e2 ⟹ typing (G1 @ G2) (exp_let e1 e2) T2

Note the fourth premise (the large one): It universally meta-quantifies over G1a, but G1a is actually determined by the equation there. So it could just substitute this (and then simplify the conclusion of the premise) and auto would be able to solve the goal.

Can I make the simplifier solve this?

I guess a small example is

lemma foo:
  "(⋀ G.  x#xs = G ⟹ P x ⟹ f G) ⟹ f (x#xs)"
apply simp

There is a somewhat related question about equalities under existentials.

Upvotes: 1

Views: 54

Answers (1)

Andreas Lochbihler
Andreas Lochbihler

Reputation: 5058

This problem can only be solved reliably using a simproc. The induct proof method in ~~/src/Tools/induct.ML already has an implementation for this, so you might be able to adapt the code. The idea is that you move the equations to the front using Induct.rearrange_eqs_simproc and then use appropriate one point rules to eliminate the equality.

Upvotes: 1

Related Questions