*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Illegal schematic goal statement*From*: Peter Lammich <lammich at in.tum.de>*Date*: Wed, 01 Apr 2015 09:23:40 +0200*In-reply-to*: <a062007acd140db08bbba@[192.168.1.20]>*References*: <a062007acd140db08bbba@[192.168.1.20]>

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

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

- Previous by Date: Re: [isabelle] Abruptly Terminating a State Monad
- Next by Date: Re: [isabelle] Illegal schematic goal statement
- Previous by Thread: [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