Stream: General

Topic: [meta] an advice channel for tips/tricks we may stumble upon

Ant S. (Mar 20 2026 at 19:31):

Is it possible to have a channel where users can share anything they stumble upon as a nice trick to work more efficiently with Isabelle. e.g. to prove that a locale is inconsistent, it seems like lemma foo: False and sledgehammer are a nice starting point

Ant S. (Mar 20 2026 at 19:32):

(oops, I meant to send this in general. If someone could move it, that'd be great)

Notification Bot (Mar 20 2026 at 19:50):

This topic was moved here from #Beginner Questions > [meta] an advice channel for tips/tricks we may stumble upon by Kevin Kappelmann.

Kevin Kappelmann (Mar 24 2026 at 08:34):

Ant S. said:

Is it possible to have a channel where users can share anything they stumble upon as a nice trick to work more efficiently with Isabelle. e.g. to prove that a locale is inconsistent, it seems like lemma foo: False and sledgehammer are a nice starting point

I think you could add them here (in this topic) for a start and if demand proves to be high, we can think about creating a channel.

Ant S. (Apr 01 2026 at 21:45):

A general strategy for proofs by contraposition:

lemma foo: "P ⟹ Q"
proof -
  have "¬Q ⟹ ¬P" sorry (* replace with your proof*)
   then show "P ⟹ Q" by auto
qed

Ant S. (Apr 01 2026 at 21:47):

And here's one cool way I found to do case analysis on a disjunction:

lemma foo: "C"
proof
(* suppose you know `P \/ Q ==> C` *)
have "P \/ Q" sorry
then show "C" proof (cases "P \/ Q", erule disjE) sorry
qed

Mathias Fleury (Apr 03 2026 at 20:22):

This generalizes better:

lemma foo: "C"
proof -
(* suppose you know `P \/ Q ==> C` *)
  consider
    (1) "P" |
    (2) "Q"
    sorry
  then show "C"
  proof (cases) (*use the proof outline here*)

Mathias Fleury (Apr 03 2026 at 20:22):

(you can have any number of cases and each case can contain several properties)

Last updated: Apr 09 2026 at 09:11 UTC