Re: [isabelle] locales and proofs programming bugs

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

     b a ≡ a b by A1;
     hence a b ≡ a b by A2;

theorem EquivSymmetric:
   ∀ a  b  c  d holds
   a b ≡c d ⇒ c d ≡ a b

H1:  a b ≡ c d;
     a b ≡ a b by EquivReflexive;  hence
     c d ≡ a b by H1, A2;

------- Tarski.thy ------- 
theory Tarski
imports Complex_Main 
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)"


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