Particularization in algebraic statements in Isabelle

Question

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.

Answer 1

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

notepad begin
  fix f g :: "nat ⇒ nat"
  assume hyp: "⋀x. f(x) = g(x)"
  from hyp
  have "f(1) = g(1)" .
end

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.