Particularization in algebraic statements in Isabelle

I'm new to Isabelle and I'm still becoming familiar with the basics.

I have an algebra for which (x || y) ; (z || w) <= (y ; z) ; (x || w) is an axiom, 1 is a neutral element for both ; and || (on both sides) and the <= relation is antisymmetric.

The current goal is to prove || is commutative.

On a paper and pencil proof, one could note the statement holds for all x, y, w and z, and in particular for w = 1 and z = 1, and simplify to show (x || y) <= (y || x). Then one could note the same statement holds under a renaming of variables, obtaining (y || x) <= (x || y), and conclude (x || y) = (y || x), since <= is antisymmetric.

However, I'm not sure how that translates to the Isabelle setting!

Assuming z = 1 and w = 1 requires an additional hypothesis, which does not hold in general, and I did not find a way to express particularization.

As requested in the comments, here I include the current state of the lemma:

lemma par_is_commutative [simp] :
" x || y = y || x "
proof -
have exchange : " (x || y) ; (z || w) \<sqsubseteq> (y ; z) || (x ; w) " by (metis exchange_law)
assume z_is_one : "z = 1"
assume w_is_one : "w = 1"
have replace_by_one :
" (x || y) ; (1 || 1) \<sqsubseteq> (y ; 1) || (x ; 1) "
by (metis exchange z_is_one w_is_one)
have simplify_ones :
" (x || y ) \<sqsubseteq> (y || x) "
by (metis
replace_by_one
one_is_seq_neuter_right
one_is_par_neuter_right)
have swapped_exchange :
" (y || x) ; (z || w) \<sqsubseteq> (x ; z) || (y ; w) "
by (metis exchange_law)
have swapped_replace_by_one :
" (y || x) ; (1 || 1) \<sqsubseteq> (x ; 1) || (y ; 1) "
by (metis swapped_exchange z_is_one w_is_one)
have swapped_simplify_ones :
" (y || x ) \<sqsubseteq> (x || y) "
by (metis
swapped_replace_by_one
one_is_seq_neuter_right
one_is_par_neuter_right)
have symmetric_order :
"(y || x ) \<sqsubseteq> (x || y) \<and> (x || y ) \<sqsubseteq> (y || x) "
by (metis
swapped_simplify_ones
simplify_ones)
have commutativity :
" (y || x) = (x || y) "
sorry
(* by (metis
symmetric_order
local.leq_is_antisymmetric

*)


This does not work, since x and y are assumed to be 1, and I can't even figure out where leq_is_antisymmetric is.

• Hi! In order to obtain an appropriate answer, could you specify what you can write at this point about the statement in Isabelle? Nov 29, 2023 at 19:02
• Hola Pedro! Agregué el código con un edit para contestar a la pregunta literalmente, aunque no creo que agregue mucho. Contestando al énfasis en can, nada. Nov 29, 2023 at 23:45
• It turned out it was possible to replace z and w with 1s in exchange directly, so none of this was required! Perhaps in more involved cases particularization cannot be done directly, but here and in similar cases it works :) Nov 30, 2023 at 14:00

The problem in the above code block seems that you can not specialize statements by using assume.

assume "z = 1" will add that fact to your assumption list, but then you'll end up only with a proof of that particular case.

Instead, you should deduce the particular case from the general instance, as in the following example.

theory Scratch

imports Main

begin


Here, the particular case follows immediately from the general statement hyp by the "trivial" proof method (abbreviated by .). Actually, in a situation as simple as this one, you would write something like hyp[of "1"] to invoke the particular case.