Re: [isabelle] Illegal schematic goal statement

Why of course you can: "?x + ?x".



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

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