Email Gateway (Aug 18 2022 at 20:03): Email Gateway (Aug 18 2022 at 20:03):From: Brian Huffman <huffman@in.tum.de>
On Fri, May 4, 2012 at 6:01 AM, Bill Richter
<richter@math.northwestern.edu> wrote:
My axiomatic geometry quest is now entirely about locales, and I have
a documentation bug. The syntax looks incorrect in both locales.pdf
and p 40 of the Isabelle/Isar Reference Manual, which has a nice group
theory example, from which I learned something about proofs.So I created the file Group1.thy below and had a lot of fun playing
with it in jedit. First notice all the "s and 's I inserted. There
are none of p 40, or in locales.pdf, and wouldn't that be great if we
didn't need them. I figured that out the"'s &''s easily by trial
and error, but It took me a long time to realize I had to put the
final period after the `"'.
I agree that the omission of quotation marks in our pdf documentation
is misleading and confusing, especially for new users who naturally
want to copy examples manually from the pdf into their theory files.
As a workaround, it may be useful to locate the source theories for
the pdfs, and copy the definitions directly. (Look inside the doc-src
directory in the distribution.)
I can happily report that the new "Programming and Proving in
Isabelle/HOL" tutorial in the upcoming Isabelle2012 release does show
quotation marks in the examples.
I didn't know how to make the -1 exponent
in jedit, so I changed x^{-1} to sqrt x. Can someone tell me how?
See appendix B of the Isabelle/Isar Reference Manual for a list of
predefined symbols.
And here's another newbie question: If you have a 4-ary relation C,
how do you tell Isabelle you want to write it as a b <\equiv> c d?
That's what Tim does, but where is that explained?
To introduce syntax like this, you will need to use the "notation"
command with a mixfix declaration. (Search for "mixfix" in the
Isabelle tutorial and old reference manual.)
Email Gateway (Aug 18 2022 at 20:03):From: Makarius <makarius@sketis.net>
On Fri, 4 May 2012, Brian Huffman wrote:
I agree that the omission of quotation marks in our pdf documentation is
misleading and confusing, especially for new users who naturally want to
copy examples manually from the pdf into their theory files.
This is an old problem, but showing the quotes alone does not help. Most
new users try to copy-paste mechanically, not manually, and then get
disappointed by the approximative result. Quotes, underscores, special
symbols etc. may all appear differently depending on the underlying LaTeX
styles of the documents in question.
I can happily report that the new "Programming and Proving in
Isabelle/HOL" tutorial in the upcoming Isabelle2012 release does show
quotation marks in the examples.
Copy paste fails here, as anticipated. E.g. page 8, middle:
fun app :: "′a list ⇒ ′a list ⇒ ′a list" where "app Nil ys = ys" |
"app (Cons x xs) ys = Cons x (app xs ys)"
The single quotes are not the ASCII ones, so Isabelle will choke on that
input. Such things can be tweaking in the LaTeX setup, but it is a
never-ending story.
I've once tried a systematic approach where the original Isabelle source
is associated with the visual typesetting (whatever that is), and it
almost worked. Unfortunately some PDF browsers had problems with this
addition to the PDF format from a few years ago, especially Mac OS Preview
and Windows Acrobat Reader. Evince/Poppler on Linux was the only platform
that worked reliably when I did the experiment 1-2 years ago.
Makarius
Email Gateway (Aug 18 2022 at 20:04):From: Bill Richter <richter@math.northwestern.edu>
Brian, I read ref.pdf p 30--32 on misfixes, but I could not figure out
how to write (in my code below)
C a b c d as a b \<equiv> c d.
I seem to have a priority problem. I'm using the priority stuff
ps = [99,99,99,99] and p = 70, and I've tried lots of others.
My "\<forall> a b . a b \<equiv> b a" gets me the error, a
do-not-enter on locale, and when I click on locale, I see in the
output window
Ambiguous input. 2 types are correct:
(\<forall> (a b) . (a b \<equiv> b a))
((\<forall> (a b) . (a b)) \<equiv> (b a))
If I change that to "a b \<equiv> b a", and then I get no error, but
the output window reads
Ambiguous input produces 2 parse trees: [which seem to be]
(C a b b a)
(C a b) (C b a)
Fortunately, only one is correct,
but you may still want to disambiguate your grammar or input.
There's more of the same for every \<equiv> expression in my axioms.
II tried to write a simple proof following p 40--42 of isar-ref.pdf,
but it didn't work. I get do-not-enter signs on every line of the
proof. The following commented proof is no better.
----- Tarski2.thy Tarski2
theory Tarski2
imports Complex_Main
begin
locale tarskifirst7 =
fixes C :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("_ _ \<equiv> _ _" [99,99,99,99] 70)
fixes B :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
(*
assumes A1: "\<forall> a b . a b \<equiv> b a"
*)
assumes A1: "a b \<equiv> b a"
and A2: "a b \<equiv> p q \<and> a b \<equiv> r s --> p q \<equiv> r s"
and A3: "a b \<equiv> c c ==> a = b"
and A4: "\<exists> x. B q a x \<and> a x \<equiv> b c"
and A5: "a \<noteq> b \<and> B a b x \<and> B a' b' x' \<and> b x \<equiv> b' x' \<and>
a b \<equiv> a' b' \<and> a c \<equiv> a' c' \<and> b c \<equiv> b' c' --> c x \<equiv> c' x'"
and A6: "B a b a ==> a = b"
and A7: "B a p c \<and> B b q c ==> (\<exists> x. B p x b \<and> B q x a)"
context tarskifirst7
begin
theorem EquivReflexive: "a b \<equiv> a b"
proof -
have "b a \<equiv> a b" by (rule A1)
have "b a \<equiv> a b" by (rule A1)
thus "a b \<equiv> a b" by (rule A2)
qed
end
(*
proof -
have "b a \<equiv> a b" by (rule A1 [symmetric])
have "b a \<equiv> a b" by (rule A1 [symmetric])
also have "a b \<equiv> a b" by (rule A2 [symmetric])
finally show "a b \<equiv> a b"
qed
end
*)
(* end *)
(*
lemma A1: "C a b b a"
by (simp add: A1)
lemma A2: "C a b p q \<and> C a b r s ==> C p q r s"
by (simp add: A2)
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
definition is-segment :: 'p set \<Rightarrow> bool where
is-segment X \<exists> x y. X = {x, y}
definition segments :: p set set where
segments = {X. is-segment X}
definition SC :: p set \<Rightarrow> p set \<Rightarrow> bool where
SC X Y \<exists> w x y z. X = {w, x} \<and> Y = {y, z} \<and> w x \<equiv> y z
*)
Email Gateway (Aug 18 2022 at 20:04):From: Brian Huffman <huffman@in.tum.de>
On Sun, May 6, 2012 at 1:01 AM, Bill Richter
<richter@math.northwestern.edu> wrote:
Brian, I read ref.pdf p 30--32 on misfixes, but I could not figure out
how to write (in my code below)
C a b c d as a b \<equiv> c d.
I seem to have a priority problem. I'm using the priority stuff
ps = [99,99,99,99] and p = 70, and I've tried lots of others.My "\<forall> a b . a b \<equiv> b a" gets me the error, a
do-not-enter on locale, and when I click on locale, I see in the
output window
Ambiguous input. 2 types are correct:
(\<forall> (a b) . (a b \<equiv> b a))
((\<forall> (a b) . (a b)) \<equiv> (b a))
Your syntax is ambiguous because \<equiv> is also used to write
meta-equality (i.e. definitional equality) in Isabelle. "a b \<equiv>
c d" looks like an equality between two function applications.
You will have a much easier time avoiding ambiguous parse
warnings/errors if you simply use a different symbol, such as \<cong>.
fixes C :: "'a => 'a => 'a => 'a => bool" ("_ _ \<cong> _ _" [99,99,99,99] 70)
The other potential source of ambiguous parsing here is when one of
the arguments to C is a function application:
term "(f x) b \<cong> c d"
This parses fine, but it prints out as "f x b \<cong> c d". If you try
to parse it again without the parentheses, you get an ambiguity.
To fix this, I would bump up the argument precedences to the maximum
(1000), which is higher than function application. This makes it so
every argument to C must be either a variable or a parenthesized
expression (which will also be the case for the pretty-printer's
output).
fixes C :: "'a => 'a => 'a => 'a => bool" ("_ _ \<cong> _ _"
[1000,1000,1000,1000] 70)
II tried to write a simple proof following p 40--42 of isar-ref.pdf,
but it didn't work. I get do-not-enter signs on every line of the
proof. The following commented proof is no better.
[...]
assumes A1: "a b \<equiv> b a"
and A2: "a b \<equiv> p q \<and> a b \<equiv> r s --> p q \<equiv> r s"
Rules stated in terms of object logic connectives, like "P \<and> Q
--> R", aren't very useful with the "rule" method. You had better
state rules using "==>", like
"P ==> Q ==> R" instead.
Hope this helps,
Email Gateway (Aug 18 2022 at 20:04):From: Bill Richter <richter@math.northwestern.edu>
Thanks, Brian, that's very helpful! I was really confused by the
\equiv biz. Can you explain two more things:
what do the 1000 priorities here even mean: [1000,1000,1000,1000] 70?
If we right a b \cong c d, I want a & b to be bound really tightly
together, so 1000 sounds like a good number, and I want the whole
expression to be bound tighter than say and or implies, so 70 is a
good number. But then I'd write it as [1000, 70, 1000].
Rules stated in terms of object logic connectives, like "P \<and> Q
--> R", aren't very useful with the "rule" method. You had better
state rules using "==>", like
"P ==> Q ==> R" instead.
I've been puzzled for some time by the preference (especially in
Julien's Tarski geometry Coq code) by folks writing
P ==> Q ==> R ==> S ==> T ==> U
instead of the more sensible
P & Q & R & S & T ==> U .
And you're saying there's a good reason for this! Great! Can you
explain why the first approach works better with rules?
Last updated: Apr 18 2024 at 12:27 UTC