Anthony Bordg (Jul 07 2019 at 13:50): Anthony Bordg (Jul 07 2019 at 13:50):Again, at some point someone should provide some explanations for newcomers about locales in Isabelle. :flashlight:
Roland Coghetto (Jul 15 2019 at 09:16):I don't quite understand the difference between "local" and "class". Do the "local" resemble the notion of Bourbaki-Structure? For example, to encode the classic notion of Group, there is a difference to choose the definition of the notion of Group from "local" or "class"?
Anthony Bordg (Jul 15 2019 at 16:47):@Roland Coghetto It's an excellent question. I don't have a definitive answer. However, my feeling is that for the formalization of mathematics locales should be preferred. I would bet that locales are closer to Bourbaki's structures. It might even be that class are deprecated.
Lawrence Paulson (Jul 16 2019 at 11:32):There's a new paper online, From LCF to Isabelle/HOL, where you will find material on axiomatic type classes (Section 4.2) and locales (Section 8.4). Briefly, locales are more general but also more heavyweight in use.
Anthony Bordg (Jul 16 2019 at 12:44):@Roland Coghetto The second half of page 17 in Larry's reference is particularly relevant. They mention explicitly the difference between type class for groups and locale for groups.
Roland Coghetto (Jul 16 2019 at 18:18):Ok thanks but Let us take the following example:
The question: using locales and context, I have difficulty demonstrating these 2 proposals (independently of each other)
lemma two_distinct_points:
"∃ x ::'p. ∃ y :: 'p. x ≠ y"
or
lemma two_distinct_points_bis:
"∃ x y. x ≠ y"
I have, in the proof, the line " then have "x ≠ y" by blast" and after why I can't proof the thesis ?
The code (I cleaned the code to show only the 2 theorems that cause problems.)
section "Tarski's geometry"
theory TARSKI
imports Main
begin
locale TarskiBC =
fixes B :: "'p ⇒ 'p ⇒ 'p ⇒ bool" ("\<between> _ _ _" [99,99,99] 50)
and C :: "'p ⇒ 'p ⇒ 'p ⇒ 'p ⇒ bool" ("_ _ \<congruent> _ _" [99,99,99,99] 50)
locale Tarski1 = TarskiBC +
assumes A1: "∀a b. a b \<congruent> b a"
locale Tarski2 = TarskiBC +
assumes A2: "∀a b p q r s. a b \<congruent> p q ∧ a b \<congruent> r s ⟶ p q \<congruent> r s"
locale Tarski3 = TarskiBC +
assumes A3: "∀a b c. a b \<congruent> c c ⟶ a = b"
locale Tarski4 = TarskiBC +
assumes A4: "∀q a b c. ∃x. \<between> q a x ∧ a x \<congruent> b c"
locale Tarski8 = TarskiBC +
assumes A8: "∃ a b c. ¬ \<between> a b c ∧ ¬\<between> b c a ∧ ¬\<between> c a b"
locale Tarski12 = Tarski1 + Tarski2
locale Tarski123 = Tarski12 + Tarski3
locale Tarski34 = Tarski3 + Tarski4
locale Tarski1234 = Tarski123 + Tarski4
locale Tarski348 = Tarski34 + Tarski8
locale Tarski12348 = Tarski1234 + Tarski8
lemma (in Tarski3) A3':
assumes "a b \<congruent> c c"
shows "a = b"
using A3 assms(1) by blast
theorem (in Tarski12) Satz2p1: (GeoCoq cong_reflexivity)
"a b \<congruent> a b"
using A1 A2 by blast
theorem (in Tarski12) Satz2p2: (GeoCoq cong_symmetry)
assumes "a b \<congruent> c d"
shows "c d \<congruent> a b"
using A2 Satz2p1 assms(1) by blast
theorem (in Tarski34) Satz3p1: (GeoCoq between_trivial)
"\<between> a b b"
using A3' A4 by blast
theorem (in Tarski348) Satz3p13:
shows "∃ a b c. ¬ \<between> a b c ∧ ¬ \<between> b c a ∧ ¬ \<between> c a b ∧ a ≠ b ∧ b ≠ c ∧ c ≠ a"
using A8 Satz3p1 by blast
context Tarski12348
begin
theorem Satz3p14: (* GeoCoq point_construction_different *)
shows "∀ a b. ∃ c. \<between> a b c ∧ b ≠ c"
by (metis (full_types) A3 A4 Tarski34.intro Tarski348.Satz3p13 Tarski348_def Tarski3_axioms Tarski4_axioms Tarski8_axioms Satz2p2)
lemma two_distinct_points:
"∃ x ::'p. ∃ y :: 'p. x ≠ y"
proof -
obtain x y where "x ≠ y ∧ \<between> x x x ∧ \<between> y y y"
using Satz3p14 Tarski34.Satz3p1 Tarski34.intro Tarski3_axioms Tarski4_axioms by fastforce
then have "x ≠ y" by blast
then show ?thesis sorry
qed
lemma two_distinct_points_bis:
"∃ x y. x ≠ y"
proof -
obtain x y where "x ≠ y ∧ \<between> x x x ∧ \<between> y y y"
using Satz3p14 Tarski34.Satz3p1 Tarski34.intro Tarski3_axioms Tarski4_axioms by fastforce
then have "x ≠ y" by blast
then show ?thesis sorry
qed
end
Anthony Bordg (Jul 16 2019 at 18:42):@Roland Coghetto simply write
lemma two_distinct_points:
"∃ x ::'a. ∃ y ::'a. x ≠ y"
proof-
obtain x y where "x ≠ y ∧ \<between> x x x ∧ \<between> y y y"
using Satz3p14 Tarski34.Satz3p1 Tarski34.intro Tarski3_axioms Tarski4_axioms by fastforce
then show ?thesis by auto
qed
or more concisely
lemma two_distinct_points: "∃ x ::'a. ∃ y ::'a. x ≠ y" using Satz3p14 Tarski34.Satz3p1 Tarski34.intro Tarski3_axioms Tarski4_axioms by fastforce
and for the second version
lemma two_distinct_points_bis:
"∃ x y::'a. x ≠ y"
proof -
obtain x y where "x ≠ y ∧ \<between> x x x ∧ \<between> y y y"
using Satz3p14 Tarski34.Satz3p1 Tarski34.intro Tarski3_axioms Tarski4_axioms by fastforce
then show ?thesis by auto
qed
or more concisely
lemma two_distinct_points_bis: "∃ x y::'a. x ≠ y" using Satz3p14 Tarski34.Satz3p1 Tarski34.intro Tarski3_axioms Tarski4_axioms by fastforce
Roland Coghetto (Jul 17 2019 at 03:20):ok thanks
Roland Coghetto (Aug 02 2019 at 14:36):In the previous example, I reconstructed the locale differently. But I get the following message: "Ambiguous input⌂ produces 15 parse trees (10 displayed):" What does that mean?
Mathias Fleury (Aug 02 2019 at 14:49):Isabelle parses all possible outputs. If only one possible output is correctly typed, you get the warning you have. If more than one is type correct or none is, you get an error
Hanna Lachnitt (Aug 02 2019 at 14:51):Add some parentheses to help Isabelle to find the intended parse tree out of all possible ones
Edit: Mathias was faster :)
Last updated: Apr 18 2024 at 16:19 UTC