Time 
Nick 
Message 
01:47 

ilbot3 joined #isabelle 
01:47 

Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html  Now with logging: http://irclog.perlgeek.de/isabelle/ 
06:11 

larsrh joined #isabelle 
09:59 

simi joined #isabelle 
10:00 
simi 
(completely new to isabelle) in a proof i'm trying "then have ?thesis" then the output shows a goal of the form "\exists x,y,z. foo"; i want to prove this statement by instantiating x,y,z myself 
10:01 
simi 
but if i write: then have ?thesis by (rule exI) i get "failed to apply initial method using this [...]" 
10:03 
larsrh 
simi: "then" adds so called "chained facts" to the local context 
10:03 
larsrh 
some proof methods, like "rule", expect these chained facts to be in a specific shape 
10:04 
larsrh 
in your case, the shape would need to be "\exists y,z. foo"; that is, exactly one quantifier stripped away 
10:04 
larsrh 
but you can just remove the "then" and you won't get these chained facts 
10:05 
simi 
perfect thanks 
10:05 
larsrh 
however, there's a better way which I'd recommend 
10:05 
larsrh 
before your final statement, prove a fact with the full instantiation, that is: have "foo 1 2 3" ... 
10:05 
larsrh 
then you can write "then have ?thesis by blast" 
10:06 
larsrh 
This is much cleaner because you immediately see all the instantiations in the statement 
10:06 
simi 
nice 
10:15 
simi 
larsrh: why does "have ?thesis" work but not "show ?thesis" with the same proof? 
10:22 
larsrh 
simi: can you show a larger example? 
10:23 
larsrh 
use http://downthetypehole.de/paste/ as a pastebin with Isabelle support 
10:25 
ThreeOfEight 
simi: my guess would be that you have an inital proof method that modified your goal 
10:25 
ThreeOfEight 
then "?thesis" is the original goal, not the current goal 
10:26 
ThreeOfEight 
If you write "proof", that stands for "proof standard" (I think) 
10:26 
ThreeOfEight 
e.g. if your goal is "∃x. P x", then "proof" will turn it into "P ?x" 
10:26 
ThreeOfEight 
(where ?x is a schematic variable for which you can fill in whatever you want, you could e.g. show "P 3") 
10:26 
ThreeOfEight 
If you want to start a proof without modifying the goal at all, write "proof " 
10:27 
ThreeOfEight 
(it is a bit confusing) 
10:41 
simi 
i see, thanks 