Again, at some point someone should provide some explanations for newcomers about locales in Isabelle. :flashlight:

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"?

@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.

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.

@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.

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

@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

ok thanks

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?

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

Add some parentheses to help Isabelle to find the intended parse tree out of all possible ones

Edit: Mathias was faster :)

Last updated: Dec 07 2023 at 12:30 UTC