Databases
StackOverflow2013
Postsdbo
POHow can I bind the schematic variable ?case in a rule for proof by cases?
Body
 

Note that there are some explanatory texts on larger screens.

plurals
  1. POHow can I bind the schematic variable ?case in a rule for proof by cases?
    text
    copied!<p>I would like to define a rule for proof by cases, to be used with <code>proof (cases rule: &lt;rule-name&gt;)</code>. I managed to use the <code>case_names</code> and <code>consumes</code> parameters, but I did not manage to bind the schematic variable <code>?case</code>, so that, inside a case of a proof using my rule, one can write <code>show ?case ...</code>. How do I bind it?</p> <p>Concretely: I have the Mizar-inspired notion of a <em>trivial set</em>, i.e. empty or singleton set. I would like to prove properties of trivial sets by <em>empty</em> vs. <em>singleton</em> case analysis. So far I have:</p> <pre><code>definition trivial where "trivial x = (x ⊆ {the_elem x})" lemma trivial_cases [case_names empty singleton, consumes 1]: assumes "trivial X" assumes empty: "P {}" and singleton: "⋀ x . X = {x} ⟹ P {x}" shows "P X" using assms unfolding trivial_def by (metis subset_singletonD) </code></pre> <p>and I can make use of this as follows:</p> <pre><code>notepad begin fix Q fix X::"'a set" have "trivial X" sorry then have "Q X" proof (cases rule: trivial_cases) case empty show "Q {}" sorry next case (singleton x) show "Q {x}" sorry qed end </code></pre> <p>But I cannot use <code>show ?case</code>. If I try, it gives me the error message "Unbound schematic variable: ?case". <code>print_cases</code> inside the proof outputs the following:</p> <pre><code>cases: empty: let "?case" = "?P {}" singleton: fix x_ let "?case" = "?P {x_}" assume "X = {x_}" </code></pre> <p>Which suggests that it doesn't work because <code>?P</code> is not bound to <code>trivial</code>.</p> <p><em>BTW:</em> The full context in which I am using this can be seen at <a href="https://github.com/formare/auctions/blob/master/isabelle/Auction/SetUtils.thy" rel="nofollow">https://github.com/formare/auctions/blob/master/isabelle/Auction/SetUtils.thy</a>.</p>
 

Querying!

 
Guidance
An individual column

Larger individual text columns get their own page to allow for proper reading.

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