Email Gateway (Mar 02 2021 at 10:33): Email Gateway (Mar 02 2021 at 10:33):From: Martin Raška <RaskaMartin@seznam.cz>
Hello,
while working on formalization of combinatorics on words, we face the phenomenon that most of the definitions and theorems about lists have symmetric versions obtained by isomorphism
rev:: 'a list ⇒ 'a list.
Although in the theory Sublist.thy the reverse-symmetry is treated by simple repeating the symmetric claims, we would like to approach the problem in a more systematic way, since we face this phenomenon to a greater extent.
My question is whether it is good practice to create a rule attribute [reversed] for transforming theorems about lists to their reverse-symmetric versions.
Simple example (mostly from Sublist.thy):
definition prefix :: "'a list ⇒ 'a list ⇒ bool"
where "prefix xs ys ⟷ (∃zs. ys = xs @ zs)"
symmetric definition:
definition suffix :: "'a list ⇒ 'a list ⇒ bool"
where "suffix xs ys = (∃zs. ys = zs @ xs)"
example theorem:
lemma prefixE: prefix xs ys ⟹ (⋀zs. ys = xs @ zs ⟹ thesis) ⟹ thesis
consider following "reversal" rules:
lemma "(⋀x. PROP P x) ≡ (⋀x. PROP P (rev x))"
lemma rev_append [symmetric]: "rev ys @ rev xs = rev (xs @ ys)"
lemma rev_is_rev_conv: "(rev xs = rev ys) = (xs = ys)"
lemma suffix_to_prefix [symmetric]: "prefix (rev xs) (rev ys) ⟷ suffix xs ys"
Then by instantiations xs="rev xs" ys="rev ys" in prefixE and rewritings according to reversal rules, we obtain symmetric
lemma suffixE: suffix xs ys ⟹ (⋀zs. ys = zs @ xs ⟹ thesis) ⟹ thesis
From this follows my approach:
I started writing a declaration attribute [reversal_rule] for storing the rules performing rewritings and a rule attribute [reversed] which transforms theorem by instantiating list-type schematic variables xs to "rev xs" and by performing rewritings according to the current list of reversal rules.
After that, we could write:
lemma suffixE: suffix xs ys ⟹ (⋀zs. ys = zs @ xs ⟹ thesis) ⟹ thesis
by (fact prefixE[reversed])
or
lemmas suffixE = prefixE[reversed]
or simply use prefixE[reversed] in proofs without having binding suffixE at all.
Is there a better/canonical way to treat this?
Best regards,
Martin Raska
Last updated: Apr 20 2024 at 04:19 UTC