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.
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: Dec 07 2023 at 20:16 UTC