StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
primarykey
Id
17204199
data
AcceptedAnswerId
0
AnswerCount
0
ClosedDate
CommentCount
0
CommunityOwnedDate
CreationDate
2013-06-20T02:06:23.613
FavoriteCount
0
LastActivityDate
2013-06-21T14:14:41.147
LastEditDate
2013-06-21T14:14:41.147
LastEditorUserId
476803
OwnerUserId
476803
ParentId
17091759
PostTypeId
2
Score
7
ViewCount
0
LastEditorDisplayName
text
Body
Concerning your statement sledgehammer is one of the most important parts of Isabelle: You never need sledgehammer to succeed with a proof. But of course sledgehammer is very convenient and can save a lot of tedious reasoning. Thus it is definitely a very important part for making Isabelle more usable for people who did not spend many years using it (and even for those sledgehammer makes everyday proving more productive). Coming to your question <blockquote> Try the <code>blast</code> or <code>auto</code> proof methods, passing the necessary facts via <code>unfolding</code>, <code>using</code>, <code>intro:</code>, <code>elim:</code>, <code>dest:</code>, or <code>simp:</code>, as appropriate. [...] So what about [this] option. Are there any easy to follow heuristics that I can apply? </blockquote> Indeed there are: <code>unfolding</code>: This (recursively) unfolds equations, i.e., it is very similar to <code>apply (simp only: ...)</code>. The heuristic is, when you do not get the expected result with <code>simp: ...</code> try <code>unfolding ...</code> instead (it might be the case that other equations are interfering). <code>using</code>: This is used to add additional assumptions to the current subgoal. The heuristic is, whenever a fact does not fit one of the patterns below, try <code>using</code> instead. <code>intro:</code>: This is used for introduction rules, i.e., of the form that whenever certain assumptions are satisfied some connective (or more generally constant) may be introduced. Example: <code>A ==> B ==> A & B</code> (where the introduced constant is <code>op &</code>). <code>elim:</code>: This is used for elimination rules, i.e., of the form that from the presence of a certain connective (or more generally constant) some facts may be concluded as additional assumptions. Example: <code>A & B ==> (A ==> B ==> P) ==> P</code> (where the constant <code>op &</code> is eliminated in favour of explicitly having <code>A</code> and <code>B</code> as assumptions). Note the general form of the conclusion (which is not related to the major premise <code>A & B</code>), this is important to not loose provability (see also <code>dest:</code>). <code>dest:</code>: This is used for destruction rules, i.e., of the form that from the presence of a certain constant some facts may be concluded directly. Example: <code>A & B ==> B</code> (Note that the information that <code>A</code> holds is lost in the conclusion, unlike in the <code>elim:</code> example.) <code>simp:</code>: This is used for simplification rules, i.e., (conditional) equations, which are always applied from left to right (thus it is sometimes useful to add <code>[symmetric]</code> to a fact, in order to apply it from right to left, but beware of nontermination, for it is easy to introduce looping derivations in this way). Having said this, often it is just experience that lets you decide in which way best to employ a given fact inside a proof. What I usually do when I got a proof by <code>sledgehammer</code> which is too slow in Isar is to inspect the facts that where used by the found proof. Then categorize them as above, invoke <code>auto</code> appropriately and if that did not completely solve the goal, apply <code>sledgehammer</code> once more (hopefully delivering an "easier" proof this time).
Tags
Title
singulars
PostAcceptedAnswerId
1. This table or related slice is empty.
PostParentId
1. POIsabelle: Sledgehammer finds a proof but it fails
 singulars
 PostTypePostTypeId
 PTQuestion
PostTypePostTypeId
1. PTAnswer
UserLastEditorUserId
1. USchris
UserOwnerUserId
1. USchris
plurals
PostLinksPostIdRelatedPostId
1. This table or related slice is empty.
PostLinksRelatedPostIdPostId
1. This table or related slice is empty.
PostsAcceptedAnswerId
1. POIsabelle: Sledgehammer finds a proof but it fails
 singulars
 PostTypePostTypeId
 PTQuestion
PostsParentIdCreationDate
1. This table or related slice is empty.
VotesPostIdCreationDate
1. VO
 singulars
 PostPostId
 PO
 UserUserId
 This table or related slice is empty.
 VoteTypeVoteTypeId
 VTUpMod
2. VO
 singulars
 PostPostId
 PO
 UserUserId
 This table or related slice is empty.
 VoteTypeVoteTypeId
 VTUpMod
3. VO
 singulars
 PostPostId
 PO
 UserUserId
 This table or related slice is empty.
 VoteTypeVoteTypeId
 VTAcceptedByOriginator
CommentsPostId
1. This table or related slice is empty.

Querying!

Guidance

A row detail

Detail views are divided into sections. All the information in the data section comes from columns in the selected row. The other sections display data from other, related rows.

Related data can be related in a to-one or a to-many fashion. Captions of data related in a to-many fashion link to a list view showing a filtered view of the table.

Try moving around until you find a non-empty to-many entry and click on the label to get to one. You can move back to the root by clicking on the database name in the header.