Re: [isabelle] rigorous axiomatic geometry proof in Isabelle



Tim and Makarius, I can't follow the Isabelle dox, and I need
something like ``Isabelle for Dummies.''  I just want to know how to
write my FOL proofs in Isabelle, how to compile them, with examples.

Now I feel strongly that Isabelle (like Mizar) ought to be able to
check FOL proofs without specifying any proof strategies like Tim's
`simp add' or `blast'.  Mizar makes lots of proof shortcuts that I
wouldn't have expected, and I'd be happier if Isabelle did few proof
shortcuts.  I want the students to have to write up most of the proof.
I think in strict FOL, you have to insert so many needless steps that
the proofs become unreadable.  I guess we need a good compromise.

I untarred Isabelle2011-1_bundle_x86-linux.tar.gz and went to the
directory Isabelle2011-1.

I ran the executable ./Isabelle and up popped jedit.  I pasted in
Isabelle code from Tim's master's thesis into Scratch.thy.  There's
extensive jedit help on the Help menu, but I couldn't figure out how
to compile my buffer.    So then I tried 

bin/isabelle emacs po.thy &

and up popped a Proof General Emacs frame displaying my short file
po.thy based on the first example in the
Isabelle2011-1/doc/locales.pdf.

------ po.thy ----
theory PO
imports Main 
begin

locale partial_order =
  fixes le :: " 'a ⇒ 'a ⇒ bool " (infixl "\<sqsubseteq>" 50)
  assumes refl [intro, simp]: "x \<sqsubseteq> x"
    and anti_sym [intro]: "[[ x  \<sqsubseteq>  y; y \<sqsubseteq> x ]] =⇒ x = y"
    and trans [trans]: "[[ x \<sqsubseteq> y; y \<sqsubseteq> z ]] =⇒  x \<sqsubseteq> z"
------ end po.thy ----

Now I can see how to compile my file!  I click on menu item
Isabelle -> Start Isabelle 
I think that's the much the same thing as clicking the down-arrow
button which says ``process whole buffer''.  I get an error message:

* Inner lexical error at: ⇒ 'a ⇒ bool  (line 6 of "/home/richter/Isabelle/Isabelle2011-1/po.thy")
*** Failed to parse type
*** At command "locale" (line 5 of "/home/richter/Isabelle/Isabelle2011-1/po.thy")

I have no idea what this means.  Posibly I'm using the wrong quote.
I'm writing 'a, but locales.pdf actually shows ’a.  So I changed to
this quote, and I got a new error message:

*** Inner lexical error at: ’a ⇒ ’a ⇒ bool (line 6 of "/home/richter/Isabelle/Isabelle2011-1/po.thy")
*** Failed to parse type
*** At command "locale" (line 5 of "/home/richter/Isabelle/Isabelle2011-1/po.thy")

Maybe that's progress, because Proof General is now noticing my first
quote a, and not just the second one.  

I'm actually trying to understand Tim's Tarski geometry axiom code.
So I tried compiling a simple version of it below.   Proof General
gives me an error message similar to the above one:

*** Outer syntax error (line 5 of "/home/richter/Isabelle/Isabelle2011-1/Scratch.thy"): command expected,
*** but symbolic identifier - (line 5 of "/home/richter/Isabelle/Isabelle2011-1/Scratch.thy") was found

But it's the code I'm more interested in now.  Tim's axioms make
perfect sense, except for the (- - ≡ - - [99,99,99,99] 50) on the line
defining C.  I'm concerned about lemma A1, which just restates the
axiom A1.  I do something like that in my Mizar code, and I was really
hoping it wouldn't be necessary in Isabelle.  Maybe I don't know what
lemma A1 is for.  But there's plenty of stuff I don't understand in
Tim's proof, like
by (simp add: A1)
with A2 show ?thesis by blast

On p 123 of isar-ref.pdf, this is somewhat explained:

   Typically, the soundness proof is relatively straight-forward,
   often just by canonical automated tools such as “by simp ” or “by
   blast ”.

I'm guessing that simp and blast are like what HOL Light calls
tactics, search strategies for Isabelle to concoct a proof.  One of
the nice things about Mizar is that you don't ever have to specify any
proof strategies, although clearly Mizar is using a strategy.

Tim's ?thesis I bet can understand, from p 6:

?thesis — the main conclusion of the innermost pending claim

Tim's show ?thesis seems to be explained on p 126:

Typical idioms for concluding calculational proofs are “finally show ?thesis .”

---- simple version of Tim's Tarski code ----
theory Tarski
imports Main 
begin

locale tarski-first7 =
 fixes C :: "'p \<Rightarrow> 'p \<Rightarrow> 'p \<Rightarrow> 'p \<Rightarrow> bool "  (- - ≡ - - [99,99,99,99] 50)
fixes B :: 'p \<Rightarrow> 'p \<Rightarrow> 'p \<Rightarrow> bool
 assumes A1: \<forall> a b. a b \<equiv> b a
 and A2: \<forall> a b p q r s. a b \<equiv> p q \<and> a b \<equiv> r s −\<rightarrow> p q \<equiv> r s
 and A3: \<forall> a b c. a b \<equiv> c c −\<rightarrow> a = b
 and A4: \<forall> q a b c. \<exists> x. B q a x \<and> a x \<equiv> b c
 and A5: \<forall> a b c d a b c d . a = b \<and> B a b c \<and> B a b c
                              \<and>ab \<equiv> a b \<and>bc \<equiv> b c \<and>ad \<equiv> a d \<and> bd \<equiv> b d
                        −\<rightarrow> c d \<equiv> c d
 and A6: \<forall> a b. B a b a −\<rightarrow> a = b
 and A7: \<forall> a b c p q. B a p c \<and> B b q c −\<rightarrow> (\<exists> x. B p x b \<and> B q x a)

context tarski-first7
begin
 lemma A1 : a b \<equiv> b a
  by (simp add: A1)

lemma A2 : [[a b \<equiv> p q; a b \<equiv> r s]] =\<Rightarrow> p q \<equiv> r s
proof −
  assume a b \<equiv> p q and a b \<equiv> r s
  with A2 show ?thesis by blast
qed

lemma A3 : a b \<equiv> c c =\<Rightarrow> a = b
  by (simp add: A3)

theorem th2-1: a b \<equiv> a b
proof −
  from A2 [of b a a b a b] and A1 [of b a] show ?thesis by simp
qed

theorem th2-2: a b \<equiv> c d =\<Rightarrow> c d \<equiv> a b
proof −
  assume a b \<equiv> c d
  with A2 [of a b c d a b] and th2-1 [of a b] show ?thesis by simp
qed

theorem th2-3: [[a b \<equiv> c d; c d \<equiv> e f ]] =\<Rightarrow> a b \<equiv> e f
proof −
  assume a b \<equiv> c d
  with th2-2 [of a b c d] have c d \<equiv> a b by simp
  assume c d \<equiv> e f
  with A2 [of c d a b e f ] and c d \<equiv> a b show ?thesis by simp
qed

theorem th2-4: a b \<equiv> c d =\<Rightarrow> b a \<equiv> c d
proof −
  assume a b \<equiv> c d
  with th2-3 [of b a a b c d] and A1 [of b a] show ?thesis by simp
qed

theorem th2-5: a b \<equiv> c d =\<Rightarrow> a b \<equiv> d c
proof −
  assume a b \<equiv> c d
  with th2-3 [of a b c d d c] and A1 [of c d] show ?thesis by simp
qed

-- 
Best,
Bill 





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