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`

)?

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