*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Quotient package and the type real*From*: Filip Marić <filipmatfbgacrs at gmail.com>*Date*: Mon, 18 Nov 2013 16:03:44 +0100*Reply-to*: filip at matf.bg.ac.rs

Hello, I am using the quotient package in Isabelle 2013 and I get an error when I try to use the descending method and the type real is involved in the quotient_definition. Here is a (simlified) example. (* Homogeneous coordinates in the complex plane *) fun homo_coords_eq :: "complex \<times> complex \<Rightarrow> complex \<times> complex \<Rightarrow> bool" where "homo_coords_eq (z1, z2) (w1, w2) \<longleftrightarrow> (\<exists> k::complex. k \<noteq> 0 \<and> w1 = k * z1 \<and> w2 = k * z2)" quotient_type complex_homo_coords = "complex \<times> complex" / homo_coords_eq proof (rule equivpI) show "reflp homo_coords_eq" unfolding reflp_def by (auto, rule_tac x=1 in exI, simp) next show "symp homo_coords_eq" unfolding symp_def by (auto, rule_tac x="1/k" in exI, simp) next show "transp homo_coords_eq" unfolding transp_def by (auto, rule_tac x="k*ka" in exI, simp) qed (* Zero *) definition zero_rep :: "complex \<times> complex" where "zero_rep = (0, 1)" quotient_definition zero where "zero :: complex_homo_coords" is zero_rep done (* Coercion of complex number - everything is OK *) definition of_complex_rep :: "complex \<Rightarrow> complex \<times> complex" where "of_complex_rep x = (x, 1)" quotient_definition of_complex where "of_complex :: complex \<Rightarrow> complex_homo_coords" is of_complex_rep done lemma "of_complex 0 = zero" by (descending) (auto simp add: zero_rep_def of_complex_rep_def) (* Coercion of real number - descending raises an error *) definition of_real_rep :: "real \<Rightarrow> complex \<times> complex" where "of_real_rep x = (complex_of_real x, 1)" quotient_definition of_real where "of_real :: real \<Rightarrow> complex_homo_coords" is of_real_rep done lemma "of_real 0 = zero" apply (descending) *** [regularize (constant mismatch) *** tmp.of_real::(nat \<Rightarrow> (nat \<times> nat) \<times> nat \<times> nat) \<Rightarrow> complex \<times> complex *** tmp.of_real::real \<Rightarrow> complex_homo_coords] *** The quotient theorem *** tmp.of_real 0 = zero *** *** does not match with original theorem *** homo_coords_eq (tmp.of_real 0) zero_rep *** At command "apply" (line 40 of "/home/filip/Dropbox/moebius/tmp.thy") The same behavior occurs with every quotient definition where the type real is involved - it seems that instead of real the system expects (nat \<Rightarrow> (nat \<times> nat) \<times> nat \<times> nat) - I suppose that is because real type itself is defined as a quotient? Is there a way to make the given example work and to use the type real in quotient definitions as any other type? Thank you! Filip

**Follow-Ups**:**Re: [isabelle] Quotient package and the type real***From:*Dmitriy Traytel

- Previous by Date: Re: [isabelle] 0::'a
- Next by Date: Re: [isabelle] Quotient package and the type real
- Previous by Thread: [isabelle] new AFP entry: Decreasing Diagrams
- Next by Thread: Re: [isabelle] Quotient package and the type real
- Cl-isabelle-users November 2013 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