Email Gateway (Aug 22 2022 at 08:59): Email Gateway (Aug 22 2022 at 08:59):From: "W. Douglas Maurer" <maurer@gwu.edu>
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
Email Gateway (Aug 22 2022 at 09:19):From: Peter Lammich <lammich@in.tum.de>
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
Email Gateway (Aug 22 2022 at 09:30):From: David Cock <david.cock@inf.ethz.ch>
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
Email Gateway (Aug 22 2022 at 09:35):From: Manuel Eberl <eberlm@in.tum.de>
Why of course you can: "?x + ?x".
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 09:36):From: David Cock <david.cock@inf.ethz.ch>
Well there you go, you learn something new every day. ;)
Email Gateway (Aug 22 2022 at 09:37):From: Lars Noschinski <noschinl@in.tum.de>
However, you cannot search for a lemma which contains both "odd x" and
"even x" for the same x,
as in the query "odd ?x" "even ?x" both ?x are allowed to be different.
-- Lars
Email Gateway (Aug 22 2022 at 09:38):From: David Cock <david.cock@inf.ethz.ch>
Right, that's what I was trying to get at.
Dave
Last updated: Nov 21 2024 at 12:39 UTC