Re: [isabelle] setup_lifting: »No relator for the type … found«



Hi Florian,

When setup_lifting warns you about missing relators, it looks for a corresponding quotient theorem that is registered as [quot_map], something like

lemma Quotient_poly_mapping [quot_map]:
  assumes Q1: "Quotient R1 Abs1 Rep1 T1"
  and Q2: "Quotient R2 Abs2 Rep2 T2"
shows "Quotient (poly_mapping_rel R1 R2) (map_poly_mapping Rep1 Abs2) (map_poly_mapping Abs1 Rep2) (poly_mapping_rel T1 T2)"

If you can prove such a quotient theorem, setup_lifting will generate a parametrised relator for lifting to nat_mapping where the type of the type parameter can change. The lemmas that you have shown will help setup_lifting to prove properties of the relator pcr_nat_mapping.


Andreas

PS: I do not think that you can prove a quotient theorem like the above, because poly_mapping is not really parametric in its type parameters: 0::'b::zero has to be mapped to zero in the other type, and the finiteness constraint prevents quotients with non-finite equivalence classes.

On 19/04/14 09:34, Florian Haftmann wrote:
Hi all,

in the example beneath, on the last setup_lifting command, I get »No
relator for the type poly_mapping found«

I tried my best to glimpse from exisiting lifting examples and the
reference manual what is missing and added poly_mapping_rel with some
characteristic properties (proofs only sketched), but the warning remains.

Any hints?

Thanks a lot,
	Florian

typedef ('a, 'b) poly_mapping =
   "{f :: 'a ⇒ 'b::zero. finite {x. f x ≠ 0}}"
   morphisms lookup Abs_poly_mapping
proof -
   have "(λ_::'a. (0 :: 'b)) ∈ ?poly_mapping" by simp
   then show ?thesis by (blast intro!: exI)
qed

setup_lifting (no_code) type_definition_poly_mapping

lift_definition poly_mapping_rel :: "('a ⇒ 'b ⇒ bool) ⇒ ('c ⇒ 'd ⇒ bool)
   ⇒ ('a, 'c::zero) poly_mapping ⇒ ('b, 'd::zero) poly_mapping ⇒ bool"
   is "fun_rel"
   ..

lemma [relator_eq]:
   "poly_mapping_rel HOL.eq HOL.eq = HOL.eq"
   apply (rule ext)+
   apply transfer
   apply (simp add: fun_eq_iff fun_rel_def)
   done

lemma [relator_mono]:
   "C ≤ A ⟹ B ≤ D ⟹ poly_mapping_rel A B ≤ poly_mapping_rel C D"
   apply (rule le_funI)+
   apply transfer
   apply (drule fun_mono)
   apply auto
   done

lemma [relator_distr]:
   "poly_mapping_rel R S OO poly_mapping_rel R' S' ≤ poly_mapping_rel (R OO R') (S OO S')"
   "left_unique R ⟹ right_total R ⟹ right_unique R' ⟹ left_total R'
     ⟹ poly_mapping_rel (R OO R') (S OO S') ≤ poly_mapping_rel R S OO poly_mapping_rel R' S'"
   "right_unique R' ⟹ left_total R' ⟹ left_unique S' ⟹ right_total S'
     ⟹ poly_mapping_rel (R OO R') (S OO S') ≤ poly_mapping_rel R S OO poly_mapping_rel R' S'"
   apply (rule le_funI)+
   apply transfer apply (auto elim: fun_relE)[1]
   apply (rule le_funI)+
   apply transfer apply auto[1] defer
   apply (rule le_funI)+
   apply transfer apply auto[1] sorry

typedef 'a nat_mapping = "UNIV :: (nat, 'a) poly_mapping set" ..

setup_lifting type_definition_nat_mapping






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.