Email Gateway (Aug 28 2026 at 15:38): Email Gateway (Aug 28 2026 at 15:38):From: Nicolas FRANCOIS <cl-isabelle-users@lists.cam.ac.uk>
Hi.
For reference, you'll find definition files for Propositional Logic and
"Variational Logic" in files LP.thy and DiffLP.thy. To sum up briefly
what I'm working on, Variational Formulas are constructed with
conjunctions, disjunctions and negation on atoms of the form a^v, where
a is a (propositional) variable and v and "variation symbol". An
interpretation is a member of Omega^2, and for example, (I,J)
(abbreviated simply in IJ) satisfies a^+ if I satisfies (not a) and J
satisfies a. With this we are trying to encode variations of states.
I'm working on some properties of this notion of Variational Formulas,
and in the process learning how to use Isabelle, and more precisely
Isar. Automatic proofs works quite fine, but I would like to enhance my
knowledge of more complicated proof methods.
For example, I'm trying to prove that operator |> distributes on
conjunction (in file DiffLP_lemmas.thy):
a |> (b /\ c) <=> (a |> b) /\ (a |> c)
I'm starting like this:
lemma distr_devient_conj1: "((α⇩1 ∧⋅ α⇩2) ▷ β) ≡⇩Δ ((α⇩1 ▷ β) ∧⇩Δ (α⇩2
▷ β))"
proof
show ‹(((α⇩1 ∧⋅ α⇩2) ▷ β) ≡⇩Δ ((α⇩1 ▷ β) ∧⇩Δ (α⇩2 ▷ β))) ⟷ (∀IJ.
DiffLPResult IJ ((α⇩1 ∧⋅ α⇩2) ▷ β) = DiffLPResult IJ (α⇩1 ▷ β ∧⇩Δ α⇩2 ▷
β))›
unfolding DiffLPEquivalence_def by auto
...
qed
but Isabelle doesn't seem satisfied by this: when positioning the
cursor just after "proof", it says
proof (prove)
goal (1 subgoal):
(α⇩1 ∧⋅ α⇩2) ▷ β ≡⇩Δ (α⇩1 ▷ β ∧⇩Δ α⇩2 ▷ β)
Failed to apply initial proof method:
goal (1 subgoal):
(α⇩1 ∧⋅ α⇩2) ▷ β ≡⇩Δ (α⇩1 ▷ β ∧⇩Δ α⇩2 ▷ β)
But if I position it after "auto", the problem seems to disappear:
theorem distr_devient_conj1: (?α⇩1 ∧⋅ ?α⇩2) ▷ ?β ≡⇩Δ (?α⇩1 ▷ ?β ∧⇩Δ ?α⇩2 ▷ ?β)
I'm quite new to all this, so if someone could explain what I don't
understand, it would be great.
Thank to anyone who had the courage to read until this :-)
\bye
--
Nicolas FRANCOIS | /\
http://nicolas.francois.free.fr | |__|
X--/\\
We are the Micro$oft. _\_V
Resistance is futile.
You will be assimilated. darthvader penguin
DiffLP.thy
DiffLP_lemmas.thy
LP.thy
Email Gateway (Sep 02 2026 at 10:17):From: "Thiemann, René" <cl-isabelle-users@lists.cam.ac.uk>
Dear Nicolas,
I'm starting like this:
lemma distr_devient_conj1: "((α⇩1 ∧⋅ α⇩2) ▷ β) ≡⇩Δ ((α⇩1 ▷ β) ∧⇩Δ (α⇩2
▷ β))"
proof
show ‹(((α⇩1 ∧⋅ α⇩2) ▷ β) ≡⇩Δ ((α⇩1 ▷ β) ∧⇩Δ (α⇩2 ▷ β))) ⟷ (∀IJ.
DiffLPResult IJ ((α⇩1 ∧⋅ α⇩2) ▷ β) = DiffLPResult IJ (α⇩1 ▷ β ∧⇩Δ α⇩2 ▷
β))›
unfolding DiffLPEquivalence_def by auto
...
qed
starting your Isar proof with
“proof” without arguments wants to already the “initial proof method”, but since
for your "≡⇩Δ” operator there is no such standard proof method registered, it fails.
Hence, you should start in this case with
lemma …
proof -
where the - tells the system not to use any initial method.
Also the next step the use of “show” is wrong, since what you state
is an intermediate statement, where you have to you use “have” instead.
In total
lemma distr_devient_conj1: "((α⇩1 ∧⋅ α⇩2) ▷ β) ≡⇩Δ ((α⇩1 ▷ β) ∧⇩Δ (α⇩2
▷ β))"
proof -
have ‹(((α⇩1 ∧⋅ α⇩2) ▷ β) ≡⇩Δ ((α⇩1 ▷ β) ∧⇩Δ (α⇩2 ▷ β))) ⟷ (∀IJ.
DiffLPResult IJ ((α⇩1 ∧⋅ α⇩2) ▷ β) = DiffLPResult IJ (α⇩1 ▷ β ∧⇩Δ α⇩2 ▷
β))›
unfolding DiffLPEquivalence_def by auto
… continue with further reasoning …
show ?thesis …
qed
I recommend to you, to first read Chapter 4 on Isar in the
“Prog-Prove” Tutorial (isabelle doc prog-prove) where this and many
more elements of Isar are described in more detail.
Best,
René
but Isabelle doesn't seem satisfied by this: when positioning the
cursor just after "proof", it saysproof (prove)
goal (1 subgoal):
1. (α⇩1 ∧⋅ α⇩2) ▷ β ≡⇩Δ (α⇩1 ▷ β ∧⇩Δ α⇩2 ▷ β)
Failed to apply initial proof method:
goal (1 subgoal):
1. (α⇩1 ∧⋅ α⇩2) ▷ β ≡⇩Δ (α⇩1 ▷ β ∧⇩Δ α⇩2 ▷ β)But if I position it after "auto", the problem seems to disappear:
theorem distr_devient_conj1: (?α⇩1 ∧⋅ ?α⇩2) ▷ ?β ≡⇩Δ (?α⇩1 ▷ ?β ∧⇩Δ ?α⇩2 ▷ ?β)
I'm quite new to all this, so if someone could explain what I don't
understand, it would be great.Thank to anyone who had the courage to read until this :-)
\bye
--
Nicolas FRANCOIS | /\
http://nicolas.francois.free.fr | |__|
X--/\\
We are the Micro$oft. _\_V
Resistance is futile.
You will be assimilated. darthvader penguin
<DiffLP.thy><DiffLP_lemmas.thy><LP.thy>
Last updated: Sep 02 2026 at 16:10 UTC