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



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


-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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