[isabelle] Quotient package and the type real



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




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