*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] frustrated by blast and instantiation*From*: Michael Norrish <michael.norrish at nicta.com.au>*Date*: Tue, 16 Jan 2007 14:52:17 +1100*Organization*: National ICT Australia*User-agent*: Thunderbird 1.5.0.8 (X11/20061117)

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.

**Follow-Ups**:**Re: [isabelle] frustrated by blast and instantiation***From:*Tobias Nipkow

**Re: [isabelle] frustrated by blast and instantiation***From:*Lawrence Paulson

- Previous by Date: [isabelle] LFMTP'07: Call For Papers
- Next by Date: Re: [isabelle] frustrated by blast and instantiation
- Previous by Thread: [isabelle] LFMTP'07: Call For Papers
- Next by Thread: Re: [isabelle] frustrated by blast and instantiation
- Cl-isabelle-users January 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list