Email Gateway (Aug 18 2022 at 20:04): Email Gateway (Aug 18 2022 at 20:04):From: Bill Richter <richter@math.northwestern.edu>
Thanks, Brian and Makarius. I'm very glad to hear you have good
technical reasons for the dox being misleading. I want to believe in
you. One possible solution to the dox problem is to point out that
quotes & doublequotes are missing for readability, and to say to read
one file or another to get the accurate syntax.
When I code in jedit, I use fancy symbols like ∀, but in the file,
jedit seems to replace ∀ by \<forall>. Is there a way to change that?
I don't understand locales or Isabelle proofs. The dox aren't written
for dummies like me. Can you work an example proof for me? Jedit says
I've coded up my Tarski geometry axioms correctly, in the file below.
Now I want to use locale power to prove my theorems. Here's an easy
theorem, with lightly edited Mizar code (rewriting C a b c d as a b ≡ c d):
theorem EquivReflexive:
∀ a, b holds a,b ≡ a,b
proof
b a ≡ a b by A1;
hence a b ≡ a b by A2;
end;
theorem EquivSymmetric:
∀ a b c d holds
a b ≡c d ⇒ c d ≡ a b
proof
assume
H1: a b ≡ c d;
a b ≡ a b by EquivReflexive; hence
c d ≡ a b by H1, A2;
end;
------- Tarski.thy -------
theory Tarski
imports Complex_Main
begin
locale tarskiaxioms =
fixes C :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
fixes B :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
assumes A1: "\<forall> a b. C a b b a"
and A2: "\<forall> a b p q r s. C a b p q \<and> C a b r s ==> C p q r s"
and A3: "\<forall> a b c. C a b c c ==> a = b"
and A4: "\<forall> q a b c. \<exists> x. B q a x \<and> C a x b c"
and A5: "\<forall> a b c x a' b' c' x' . \<not>(a = b) \<and> B a b x \<and> B a' b' x' \<and> C b x b' x' \<and>
C a b a' b' \<and> C a c a' c' \<and> C b c b' c' ==> C c x c' x'"
and A6: "\<forall> a b. B a b a ==> a = b"
and A7: "\<forall> a b c p q. B a p c \<and> B b q c ==> (\<exists> x. B p x b \<and> B q x a)"
Email Gateway (Aug 18 2022 at 20:06):From: Makarius <makarius@sketis.net>
The prover refrains from using Unicode on its own, but the front-end may
do so based on certain translation tables. These are given as defaults in
ISABELLE_HOME/etc/symbols and ISABELLE_HOME_USER/etc/symbols, so in
principle this can be changed.
As a new user you should not try that, though, unless you want to spend
most of the time tinkering with the system instead of using it.
Makarius
Last updated: Apr 25 2024 at 16:19 UTC