Databases
StackOverflow2013
Postsdbo
PO
 

Note that there are some explanatory texts on larger screens.

plurals
  1. PO
    primarykey
    data
    text
    <p>Personally, I just tend to just use:</p> <pre><code>apply (metis thm) </code></pre> <p>which works most of the time without forcing me to think very hard (but will still occasionally fail if tricky resolution is required).</p> <p>Other methods that will also typically work include:</p> <pre><code>apply (rule thm) (* If "thm" has no premises. *) apply (erule thm) (* If "thm" has a single premise. *) apply (erule thm, assumption+) (* If "thm" has multiple premises. *) </code></pre> <p>Why is there no one single answer? The answer is a little complex:</p> <p>Internally, <code>solve_direct</code> calls <code>find_theorems solves</code>, which then performs the following:</p> <pre><code>fun etacn thm i = Seq.take (! tac_limit) o etac thm i; (* ... *) if Thm.no_prems thm then rtac thm 1 goal else (etacn thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal; </code></pre> <p>This is the ML code for something similar to <code>rule thm</code> if there are no premises on the rule, or:</p> <pre><code>apply (erule thm, assumption+) </code></pre> <p>if there are multiple premises on the rule. As commented by Brian on your question, the above might still fail if there are complex meta-logical connectives in the assumptions (which the <code>norm_hhf_tac</code> deals with, but is not directly exposed as an Isabelle method as far as I am aware).</p> <p>If you wanted, you could write a new method that exposes the tactic used by <code>find_theorems</code> directly, as follows:</p> <pre><code>ML {* fun solve_direct_tac thm ctxt goal = if Thm.no_prems thm then rtac thm 1 goal else (etac thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal; *} method_setup solve = {* Attrib.thm &gt;&gt; (fn thm =&gt; fn ctxt =&gt; SIMPLE_METHOD' (K (solve_direct_tac thm ctxt ))) *} "directly solve a rule" </code></pre> <p>This could then be used as follows:</p> <pre><code>lemma "⟦ a; b ⟧ ⟹ a ∧ b" by (solve conjI) </code></pre> <p>which should hopefully solve anything <code>solve_direct</code> throws at you.</p>
    singulars
    1. This table or related slice is empty.
    1. POHow can I use rules suggested by solve_direct? (by (rule …) doesn't always work)
      singulars
      1. PTQuestion
    1. PTAnswer
    1. USdavidg
    1. USdavidg
    plurals
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. POHow can I use rules suggested by solve_direct? (by (rule …) doesn't always work)
      singulars
      1. PTQuestion
    1. This table or related slice is empty.
    1. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    2. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    3. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    1. COThanks for pointing out how to really do it right. As I was asking from an end user's perspective this approach would be overkill for me. Indeed one of `by (metis thm)`, or sometimes `by metis` (when it turned out that metis didn't need the theorem), or sometimes `by (simp add: thm)` worked for me in the cases I have encountered so far.
      singulars
      1. PO
      1. USChristoph Lange
    2. CO@ChristophLange: I don't tend to know answers to questions such as this, so I look at the source code of Isabelle to work them out; I just wrote out my thought patterns so it didn't seem like my answer came by way of divination. `:)` It is probably worth moving my punchline to the top of the answer, though.
      singulars
      1. PO
      1. USdavidg
    3. COInstead of `apply (erule thm, assumption+)` you can also use `apply (erule (1) thm)`, where `1` is the number of additional premises to use.
      singulars
      1. PO
      1. USJoachim Breitner
 

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.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload