*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Fwd: Code generation for typedefs with an invariant*From*: Manuel Eberl <manuel at pruvisto.org>*Date*: Thu, 14 Oct 2021 21:31:42 +0200*Authentication-results*: cam.ac.uk; iprev=pass (mta1.cl.cam.ac.uk) smtp.remote-ip=128.232.0.57; spf=none smtp.mailfrom=pruvisto.org; arc=none*Authentication-results*: cam.ac.uk; iprev=pass (smtprelay04.ispgateway.de) smtp.remote-ip=80.67.18.16; spf=none smtp.mailfrom=pruvisto.org; arc=none*In-reply-to*: <796951f0-49fc-a0f0-1324-3a0b0ee2ed8d@uibk.ac.at>*References*: <796951f0-49fc-a0f0-1324-3a0b0ee2ed8d@uibk.ac.at>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:91.0) Gecko/20100101 Thunderbird/91.1.2

Hello, I have a typedef of the form typedef good_nat = "{n::nat. good n}"

See attachment for all the details. Thanks, Manuel

theory Test imports Main begin (* Imagine that this is either difficult to compute or good not computable *) consts good :: "nat \<Rightarrow> bool" axiomatization where good_42 [simp]: "good 42" and good_23 [simp]: "good 23" (* I define a type of good numbers *) typedef (overloaded) good_nat = "{n::nat. good n}" by (rule exI[of _ 23]) auto lemma [code abstype]: "Abs_good_nat (Rep_good_nat x) = x" by (simp add: Rep_good_nat_inverse) setup_lifting type_definition_good_nat (* Suppose I have some very complicated computation here, but I know it only produces good numbers. *) definition my_complicated_computation :: "nat \<Rightarrow> nat list" where "my_complicated_computation n = [23, 42] \<comment> \<open>placeholder\<close>" lemma my_complicated_computation_good: "\<forall>x\<in>set (my_complicated_computation n). good x" by (auto simp: my_complicated_computation_def) (* I can now lift that computation such that the goodness information is present in the type: *) lift_definition my_complicated_computation' :: "nat \<Rightarrow> good_nat list" is my_complicated_computation using my_complicated_computation_good by (auto simp: list.pred_set) (* But it*s not executable :( *) value "my_complicated_computation' 13" (* My workaround: *) typedef (overloaded) good_nat_list = "{ns::nat list. \<forall>n\<in>set ns. good n}" by (rule exI[of _ "[]"]) auto lemma [code abstype]: "Abs_good_nat_list (Rep_good_nat_list x) = x" by (simp add: Rep_good_nat_list_inverse) setup_lifting type_definition_good_nat_list lift_definition my_complicated_computation'' :: "nat \<Rightarrow> good_nat_list" is my_complicated_computation using my_complicated_computation_good by (auto simp: list.pred_set) lemma [code]: "Rep_good_nat_list (my_complicated_computation'' x) = my_complicated_computation x" by transfer auto (* Now this is executable, but I still have to turn the "good_nat_list" into a "good_nat list" somehow *) value "my_complicated_computation'' 13" lift_definition list_of_good_nat_list :: "good_nat_list \<Rightarrow> good_nat list" is "\<lambda>xs. xs" by (auto simp: list.pred_set) lemma [code]: "my_complicated_computation' x = list_of_good_nat_list (my_complicated_computation'' x)" by transfer auto (* Still not executable *) value "list_of_good_nat_list (my_complicated_computation' 13)" (* So let's take a brute force approach *) lift_definition hd_good_nat_list :: "good_nat_list \<Rightarrow> good_nat" is "\<lambda>xs. if xs = [] then 23 else hd xs" by auto lift_definition tl_good_nat_list :: "good_nat_list \<Rightarrow> good_nat_list" is tl by (auto simp: tl_def) lift_definition null_good_nat_list :: "good_nat_list \<Rightarrow> bool" is "\<lambda>xs. xs = []" . lemma [code]: "list_of_good_nat_list xs = (if null_good_nat_list xs then [] else hd_good_nat_list xs # list_of_good_nat_list (tl_good_nat_list xs))" by transfer auto (* And now it works *) value "my_complicated_computation' 13" end

**Follow-Ups**:**Re: [isabelle] Fwd: Code generation for typedefs with an invariant***From:*Manuel Eberl

- Previous by Date: [isabelle] [Isabelle2021-1-RC0] Simp-rules for bit
- Next by Date: Re: [isabelle] Fwd: Code generation for typedefs with an invariant
- Previous by Thread: [isabelle] [Isabelle2021-1-RC0] Simp-rules for bit
- Next by Thread: Re: [isabelle] Fwd: Code generation for typedefs with an invariant
- Cl-isabelle-users October 2021 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