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.
z
andw
with 1s inexchange
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 :) $\endgroup$