Search code examples
isabelleisar

Factoring out a lemma premise as a definition causes failure in proof method (auto) application in isabelle

I have the following code in Isabelle:

typedecl Person
consts age :: "Person ⇒ int" 

lemma "⟦(∀p::Person. age p > 20);p ∈ Person⟧⟹ age p > 20"
apply (auto)
done

The auto proof method works fine and proves the lemma! when I want to factor out the first part of the premise in the lemma as a definition C1 as bellow: 

definition C1::bool where "C1 ≡ (∀p::Person. age p > 20)"

The auto methods fails to prove in the following code:

lemma "⟦C1;p ∈ Person⟧⟹ age p > 20"
apply (auto)
done

why this happens? If I am doing wrong in the way of factoring out the first assumption ---I am doing this to organize the assumption to look neat and structured-- what is the best way to do this that does not affect the prove methods (auto) functionality.

Thanks

Solution

  • First, to actually add some value, I show how to use declare to add C1_def as a simp rule. I then give you some unrequested pointers about your lemma, and then I give you some unasked for pointers about Stackoverflow etiquette (from my viewpoint).

    Declaring a definition as a simp rule

    As Alexander pointed out, a definition is not automatically added as a simp rule.

    You can declare it as a simp rule like this:

    declare C1_def [simp add]

    The use of simp rules by the automatic proof methods auto, simp, fastforce, etc. can cause bad looping, or expand formulas in ways that you don't want the formulas expanded, so after adding it, you can remove it as a simp rule like this:

    declare C1_def [simp del]

    Comments on your lemma

    It could be that the formula in your lemma is exactly what you want, but your notation, in my opinion, is a potential source of confusion. In particular, that you're using Person as both the name of a type and a set variable. I make these comments without asking for clarification.

    For myself, my question was, "How is it that p ∈ Person is not giving an error, because Person there is a set, where Person in typedecl Person is not a set.

    One way to get more information is with declare [[show_types, show_consts]].

    To answer my question, I did the following (converting symbols for browser portability), and I show some of what I saw in the output panel:

    declare [[show_types, show_consts]]
lemma "[|(!p::Person. age p > 20); p ∈ Person|] ==> (age p > 20)"
oops
(*OUTPUT:
  variables:
    Person :: Person set
    p :: Person *)

    It shows me that Person is a free variable. As to p, it's a bound variable in (!p::Person. age p > 20), but it's free in the rest of the lemma, so your hypothesis includes the formula that every p of type Person is in every set of type Person set.

    It could be that's what you want, but in this case, it makes no difference because your lemma is basically of the form A and B implies A.

    You need to accept an answer to an answered SO question

    Before I disappear in about 2 hours, for the isabelle tag, I again do my beloved duty as the SO etiquette police.

    You've asked three questions. In particular, there is this one:

    It's a straightforward question, and it's given a straightforward answer. You need to accept it as an answer. Otherwise,

    • when people click on the "unanswered" tab for the "isabelle" tag, it might show up as unanswered, when it has been unanswered,
    • you're not showing proper appreciation, to the extent you should, for the answer that was given.

    In the case of the question I linked to, you got an answer from one of the Isbelle/HOL experts (unlike me). It takes a significant amount of time for a person to type in an answer like that. It's not extraordinarily long, but then it's not a one-liner either.