# IRC log for #isabelle, 2016-09-06

All times shown according to UTC.

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