Re: [isabelle] frustrated by blast and instantiation



I don't think this has anything to do with which quantifier you use - blast just seems unable to prove the goal. This may be due to the presence of "=". Larry may be able to comment.

Concerning the quantifiers: certainly simp, but I believe also blast don't care what quantifiers a premise carries.

Meta-level quantifiers in premises can be dealt with like object-level ones with the rules meta_spec and meta_allE.

Tobias

Michael Norrish schrieb:
I am currently trying to prove what feels like a trivial lemma and
becoming frustrated by meta-level quantifiers and blast, and no doubt
any number of sophisticated considerations that I'm not aware of.

Here is a miniature theory that illustrates a stripped down version of
my problem.

----------------------------------------------------------------------
theory foo
  imports Main

begin

consts c :: "nat"
consts f :: "nat => 'a"

lemma foo1: "ALL i. EX! n. n < c & f n = i"
sorry

lemma foo2: "(ALL k. P k) = (ALL i. i < c --> P (f i))"
apply rule
  apply simp
apply rule+
apply (insert foo1[where 'a = 'a])
apply (drule_tac x = k in spec)
apply blast
done

end
----------------------------------------------------------------------

(The theorem foo1 actually has a proof in the real setting.)

This proof succeeds, but there are two things I dislike about it.

1.  It seems as if I am doing the wrong thing in not converting foo1
    to be in "rule_format" (or proving it that way in the first
    place).  All the documentation I have suggests that rule_format is
    the right way to store lemmas.  But, I seem to have to keep the
    object level universal if I'm to be able to import/insert the
    result into the proof foo2.  If I have it in rule_format and
    insert it un-modified, then I get a meta-level implication in my
    premises, and I don't know how to do anything with that.  If I try
    to use "of" or "where" to instantiate a rule_format version of
    foo1, then the meta-level quantifier on the goal shifts its
    quantification over the goal's k to dodge my implication.

2.  I have to instantiate foo1 by hand, both to get its type variable
    correct, and then to instantiate i.  Why doesn't

     apply (blast intro: foo1)

    just solve this goal at the outset?  If I set the corresponding
    situation up in HOL4, my proof of foo2 looks like

      val foo2 = store_thm(
       "foo2",
       ``(!k. P k) = (!i. i < c ==> P (f i))``,
       PROVE_TAC [foo1])

    [ Perhaps I'm giving blast the wrong modifier.  But then, why
      doesn't blast let me just use add: and then figure out for
      itself how to use the given theorem?  I can believe that
      theorems being permanently added to the underlying reasoners
      should be carefully categorised as intro, dest or elim
      (particularly as there so many of them), but for a one-off
      tactic, having to apply thought is just a hindrance to getting
      through the proof. ]

So, what is the 'right' way to state foo1, and the right way to prove
foo2?

Michael.





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.