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)

Ant S. (Apr 23 2026 at 19:29):

#Beginner Questions > ✔ How can I shorten this simple Isar proof? @ 💬
This entire thread from this point on.

Ant S. (May 25 2026 at 10:27):

Proving two functions equal. In the Isabelle/HOL manual,
page 39: > Extensionality is built into the meta-logic, and this rule expresses a related
property.

(* assume f and g are already defined *)
lemma foo: "f  = g"
proof (rule ext)
fix xa
(* rest of you proof here*)
oops

Mathias Fleury (May 25 2026 at 12:13):

It is even used by default:

definition f :: ‹nat ⇒ nat› where
‹f x = undefined›

definition g :: ‹nat ⇒ nat› where
‹g x = undefined›

lemma ‹f = g›
proof
  oops

Ant S. (May 25 2026 at 12:15):

It doesn't seem to be used when e.g. we have f (h) = g where f :: ('a => 'a) => 'a => 'a

Ant S. (May 25 2026 at 12:15):

so we wts !!x. f (h) x = g x

Mathias Fleury (May 25 2026 at 12:16):

definition f :: ‹('a => 'a) => 'a => 'a› where
‹f x = undefined›

definition g :: ‹'a => 'a› where
‹g x = undefined›

lemma ‹f h = g›
proof
(*
proof (state)
goal (1 subgoal):
 1. ⋀x. f h x = g x
*)
  oops

Ant S. (May 25 2026 at 12:16):

hold up... let me see what the difference is between what I'm working on and the MRE I wrote

Ant S. (May 25 2026 at 12:19):

hmm, I must've just missed that. (Was fun stumbling upon this in HOL's axiomatization though) (oops)

Last updated: Jun 12 2026 at 11:44 UTC