Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Hotkeys for writing the theorem state in Isar.

Email Gateway (Aug 23 2022 at 08:54):

From: Georgy Dunaev <georgedunaev@gmail.com>
I have some long statement that I want to prove:

theorem thm:"A0==>A1==>A2==>A3==>B"
proof -

Now I want to write

assume H00:"A0"
assume H01:"A1"
assume H02:"A2"
assume H03:"A3"
show "B"
proof

It takes time to write or manually copy expressions from "State" tab.
Is there an automatisation for this? If no, it would be very useful!

Yours sincerely,
Georgy Dunaev

Email Gateway (Aug 23 2022 at 08:54):

From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi Georgy,

I know two solutions:

1. The tactic sketch and explore (included in Isabelle) is able to do
something
  like what you want:

theory Scratch
    imports
       Main "HOL-ex.Sketch_and_Explore"
    begin

theorem "A0==>A1==>A2==>A3==>B"
      sketch -
    (*
    proof -
      show B
        if A0
          and A1
          and A2
          and A3
        using that sorry
    qed
    *)

explore -
    (*
    proof -
      have B
        if "A0 x"
          and "A1 x y"
          and A2
          and A3
        using that sorry
      then show ?thesis
        by -
    qed
    *)

As far as I know, It supports only quotes ("A0").

2. My own variant of Explore (available at
https://bitbucket.org/isafol/isafol/src/master/lib/Explorer.thy)
  produces something closer to what you want:

theory Scratch
    imports
       Main "$ISAFOL/lib/Explorer"
    begin

theorem "A0==>A1==>A2==>A3==>B"
      explore
    (*
    proof -
      assume
        ‹A0› and
        ‹A1› and
        ‹A2› and
        ‹A3›
      show ‹B› sorry
    qed
    *)

(also useful, to rewrite the form of the lemma)
     explore_lemma
    (*
    lemma
      assumes
        ‹A0› and
        ‹A1› and
        ‹A2› and
        ‹A3›
      shows ‹B›
    proof -
      show ?thesis sorry
    qed
    *)

You can switch between cartouches (‹A0›) and quotes ("A0").

Best,
Mathias

Email Gateway (Aug 23 2022 at 08:54):

From: Makarius <makarius@sketis.net>
Here is a more standard way to write this in Isabelle/Isar:

theorem "thm":
assumes 0: "A0"
and 1: "A1"
and 2: "A2"
and 3: "A3"
shows "B"
proof -
qed

• Long statements have first-class syntax.

• The same works for statements within a proof, using postfix notation:

  have B if A0 and A1 ...

• Meaningless names for facts could be just numerals, 1, 2, 3, or , , .
  You should not "encode" the manner how facts get introduce in the name (like H
  for "hypothesis" or A for "assumption") because that role often changes as a
  prove evolves over time. (E.g. "assume" may become "have" or "obtain" later.)

• A notable exception: skip 0, 1, 2, 3 above and use assms(0), assms(1) etc.
  in the proof, as long as the whole proof setup is rather small and adhoc.

  Makarius

Last updated: Apr 24 2024 at 08:20 UTC