*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Parametricity as a poor man's dependent typing*From*: Joachim Breitner <breitner at kit.edu>*Date*: Fri, 10 Aug 2012 13:23:32 +0200*In-reply-to*: <1330098760.5176.31.camel@kirk>*References*: <1330097248.5176.21.camel@kirk> <9D4D4BD4-C9A1-4E3E-AA44-50884345719C@loria.fr> <1330098760.5176.31.camel@kirk>

Hi, I thought more about using parametricity to ease working with definitions that only make sense on a set of values, and where lots of lemmata will have such a set membership as an assumption. Right now I am wondering if the transfer package can be of some help here. So I start with some abstract set: axiomatization a_set :: "nat set" where ne: "a_set ≠ {}" and I want to prove something like lemma goal: assumes "list_all (λx. x ∈ a_set) xs" and "∀x ∈ a_set. f x ∈ a_set" shows "list_all (λx. x ∈ a_set) (map f xs)" where "map" is just an example for a possibly much more complicated polymophic expression. To make working with closed functions on the set easier, I create a type and set it up for the transfer package: typedef (open) a_type = a_set using ne by auto setup_lifting type_definition_a_type The idea is that if I can do some calculation on this type that’s related to a calculation on a_set, then the result will also be in the set: lemma untransfer: "list_all2 cr_a_type x y ⟹ list_all (λx. x∈a_set) x" by (induct rule: list_all2_induct, auto simp add:cr_a_type_def Rep_a_type) And indeed I can prove the goal: lemma goal: assumes "list_all (λx. x ∈ a_set) xs" and "∀x ∈ a_set. f x ∈ a_set" shows "list_all (λx. x ∈ a_set) (map f xs)" proof- have "list_all2 cr_a_type xs (map Abs_a_type xs)" (is "list_all2 _ _ ?xs'") using assms(1) by (auto simp add:list_all2_def cr_a_type_def set_zip list_all_length Abs_a_type_inverse) moreover have "fun_rel cr_a_type cr_a_type f (λ x. Abs_a_type (f (Rep_a_type x)))" (is "fun_rel _ _ _ ?f'") using assms(2) by (auto simp add:cr_a_type_def Abs_a_type_inverse Rep_a_type) ultimately have "list_all2 cr_a_type (map f xs) (map ?f' ?xs')" by -(rule fun_relD[OF fun_relD[OF map_transfer]]) thus ?thesis by (rule untransfer) qed Note that everything related to the actual operation I am doing on f and x is just mechanical application of transfer rules. Also the first two steps are what the lifting package does all the time. So it seems that this pattern can be automated. The main problem seems to be that this only works well for a globally-defined set "a_set". Trying to make goal abstract in "a_set" using a context fails context fixes S :: "nat set" assumes ne:"S ≠ {}" begin typedef (open) S_type = S using ne by auto setup_lifting type_definition_a_type (* ... *) with Illegal variables in representing set: "S" The error(s) above occurred in typedef "S_type". So one question is: Is it fundamentally not possible (i.e. unsound) to define a type within a context that depends on a parameter? Or is theoretically acceptable as long as the type does not escape the context, i.e. only lemmas are available to the outside that do not mention this type? Greetings, Joachim -- Dipl.-Math. Dipl.-Inform. Joachim Breitner Wissenschaftlicher Mitarbeiter http://pp.info.uni-karlsruhe.de/~breitner

**Attachment:
signature.asc**

- Previous by Date: Re: [isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?
- Next by Date: Re: [isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?
- Previous by Thread: Re: [isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?
- Next by Thread: [isabelle] New nat induct rule in Cong.thy
- Cl-isabelle-users August 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list