Stream: Beginner Questions

Topic: Lifting of theorems

Robert Soeldner (Aug 24 2022 at 20:39):

Dear all,

I would like to "lift" theorem from one typ to another, specifically, I have (very simplified) setup:

record ('a,'b) obj =
  param1 :: 'a
  param2 :: 'b

type_synonym nobj = "(nat,nat) obj"

definition to_nobj :: "('a::countable,'b::countable) obj ⇒ nobj" where
"to_nobj x ≡ ⦇param1 = to_nat (param1 x), param2 = to_nat (param2 x)⦈"

definition from_nobj :: "nobj ⇒ ('a::countable,'b::countable) obj" where
"from_nobj x ≡ ⦇param1 = from_nat (param1 x), param2 = from_nat (param2 x)⦈"

lemma ‹from_nobj (to_nobj x) = x›
  by (simp add: to_nobj_def from_nobj_def)

Is there a way to automatically "lift" theorems containing nobj (back) into the parametric one (i.e. ('a,'b) obj)?

Wolfgang Jeltsch (Aug 25 2022 at 22:43):

Without a deeper understanding of your code, my spontaneous idea is that “lifting” sounds a lot like a use for the Lifting package. Have you had a look at it? A word of warning: It’s all but trivial. You should have some idea about parametricity if you want to use it in more advanced ways.

Last updated: Oct 12 2024 at 20:18 UTC