*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Illegal schematic goal statement*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Wed, 01 Apr 2015 09:36:23 +0200*In-reply-to*: <551B9E5E.6060604@inf.ethz.ch>*References*: <a062007acd140db08bbba@[192.168.1.20]> <1427873020.2600.21.camel@lapbroy33> <551B9E5E.6060604@inf.ethz.ch>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.6.0

Why of course you can: "?x + ?x". Cheers, Manuel On 01/04/15 09:29, David Cock wrote: > Also, specifically for the find panel, you want to use underscores > i.e. "_ @ _" will match any concatenation of two lists. Unfortunately > you can only specify syntactic constraints like this - you can't > explicitly search for "x + x", for any x, for example (as far as I know). > > David > > On 01/04/15 09:23, Peter Lammich wrote: >> This is a technical idiosyncrasy/feature of Isabelle. There are two >> kinds of variables, free variables (without ?) and schematic variables >> (with ?). The unifier only instantiates schematic variables. >> >> If you state a lemma, you do not want the variables in your lemma to be >> instantiated (and thus your lemma specialized). If you use a lemma, >> however, you want to instantiate the variables in it. >> >> Hence, the lemma command converts the free variables to schematics >> before storing the lemma, and that's what you see in the output of >> find_thms. >> >> To print a lemma, say dec_induct, with frees instead of schematics, try: >> >> thm dec_induct[no_vars] >> or >> print_statement dec_induct >> >> -- >> Peter >> >> >> >> >> On Di, 2015-03-31 at 18:33 -0500, W. Douglas Maurer wrote: >>> As should be clear from my previous posts, I continue trying to find >>> Isabelle induction rules that correspond with the way my students >>> learn induction. By accident I stumbled upon a file called >>> How_To_Prove_it.thy, which suggests: "There are many more special >>> induction rules. You can find all of them via the Find button...with >>> the following search criteria: name: Nat name: induct." So I tried >>> this, and I got 18 rules, some of which appear to apply to some of my >>> situations (particularly Nat.dec_induct). However, I am now getting >>> an error message which I have never seen before, when I try to enter >>> one of these, exactly as it appears in the Query window, as a lemma. >>> For example, the second one appears as Nat.nat_induct: ?P 0 ==> >>> (\bigwedge n. ?P n ==> ?P (Suc n)) ==> ?P ?n . When I enter this as a >>> lemma (in double quotes, of course) I get the message "Illegal >>> schematic goal statement." Well, I can always take the question marks >>> out, but why does Find Theorems find a theorem in a form that doesn't >>> enter? (I've also tried it without the double quotes, and this time I >>> get an outer syntax error on the \bigwedge .) Thanks! -WDMaurer >> >> > >

**Follow-Ups**:**Re: [isabelle] Illegal schematic goal statement***From:*David Cock

**Re: [isabelle] Illegal schematic goal statement***From:*Lars Noschinski

**References**:**[isabelle] Illegal schematic goal statement***From:*W. Douglas Maurer

**Re: [isabelle] Illegal schematic goal statement***From:*Peter Lammich

**Re: [isabelle] Illegal schematic goal statement***From:*David Cock

- Previous by Date: Re: [isabelle] Illegal schematic goal statement
- Next by Date: Re: [isabelle] Illegal schematic goal statement
- Previous by Thread: Re: [isabelle] Illegal schematic goal statement
- Next by Thread: Re: [isabelle] Illegal schematic goal statement
- Cl-isabelle-users April 2015 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