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

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

-- 
Best,
Bill 





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