Re: [isabelle] Quotient package and the type real



Hello Filip,

I cannot say anything about the descending method, but your example works fine with Lifting and Transfer in Isabelle 2013 (see below). And since there are plans to eventually remove the Quotient package (https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-March/msg00026.html), I would recommend to use these more recent tools.

Dmitriy

(* Homogeneous coordinates in the complex plane *)
fun homo_coords_eq :: "complex × complex ⇒ complex
× complex ⇒ bool" where
"homo_coords_eq (z1, z2) (w1, w2) ⟷ (∃
k::complex. k ≠ 0 ∧ w1 = k * z1 ∧ w2 = k * z2)"

quotient_type
complex_homo_coords = "complex × 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 × complex" where "zero_rep = (0, 1)"
lift_definition zero :: "complex_homo_coords" is zero_rep
unfolding zero_rep_def by simp

definition of_complex_rep :: "complex ⇒ complex × complex" where "of_complex_rep x = (x, 1)" lift_definition of_complex :: "complex ⇒ complex_homo_coords" is of_complex_rep
unfolding of_complex_rep_def by simp

lemma "of_complex 0 = zero"
by transfer (auto simp add: zero_rep_def of_complex_rep_def)

definition of_real_rep :: "real ⇒ complex ×
complex" where "of_real_rep x = (complex_of_real x, 1)"
lift_definition of_real :: "real ⇒ complex_homo_coords" is of_real_rep
unfolding of_real_rep_def by simp

lemma "of_real 0 = zero"
by transfer (auto simp add: zero_rep_def of_real_rep_def)


Am 18.11.2013 16:03, schrieb Filip Marić:
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.