StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
text
Body
copied!<p>As Joachim already mentioned, unlike <code>induct</code>, the <code>cases</code> method does not bind the schematic variable <code>?case</code>. I would say the "canonical" way of conducting <em>case analysis</em> (as a proof method) conforms to this setup, since typically only different assumptions -- which taken together are exhaustive -- are considered, whereas the conclusion stays the same (abbreviated by <code>?thesis</code> in Isabelle) throughout the different cases. I would set up your <code>trivial_cases</code> as follows:</p> <pre><code>lemma trivial_cases [consumes 1, case_names empty singleton]: assumes "trivial X" and "X = {} ⟹ P" and "⋀x . X = {x} ⟹ P" shows "P" using assms by (auto simp: trivial_def) </code></pre> <p>Then you can use it like</p> <pre><code>notepad begin fix P and X :: "'a set" have "trivial X" sorry then have "P X" proof (cases rule: trivial_cases) case empty then show ?thesis sorry next case (singleton x) then show ?thesis sorry qed end </code></pre> <p>where the simplifier or explicit unfolding takes care of specializing <code>X</code> to <code>{}</code> and <code>{x}</code>, respectively.</p> <p><strong>Side Note:</strong> You can further tune <code>trivial_cases</code> by adding the attribtue <code>cases pred: trivial</code>. Then, whenever <code>trivial ?X</code> is the major assumption fed to <code>cases</code>, the rule <code>trivial_cases</code> is used implicitly, i.e., you can do the following</p> <pre><code>have "trivial X" sorry then have "P X" proof (cases) </code></pre> <p>in the above proof.</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