Mario Carneiro (Aug 20 2024 at 22:36): Mario Carneiro (Aug 20 2024 at 22:36):The following is a syntax error at the ⟹ but I don't see why... Isn't this legal Pure syntax?
theory Scratch
imports Pure
begin
ML‹
val x = \<^term>‹⋀x. P x ⟹ Q x›;
›
Also, does \<^term> have an antiquotation syntax for ML values of type term?
Mathias Fleury (Aug 21 2024 at 05:01):Mario Carneiro said:
Also, does
\<^term>have an antiquotation syntax for ML values of typeterm?
What do you mean? \<^term> returns a term, so applying \<^term> would only return the identity?
Mathias Fleury (Aug 21 2024 at 05:04):And for the first part, I was first confused why it was working in HOL but not in Pure, but it is the usual implicit PROP inclusion. So
ML‹
val x = \<^term>‹⋀x. PROP P x ⟹ PROP Q x›;
›
works
Mario Carneiro (Aug 21 2024 at 06:23):Mathias Fleury said:
Mario Carneiro said:
Also, does
\<^term>have an antiquotation syntax for ML values of typeterm?What do you mean? \<^term> returns a term, so applying \<^term> would only return the identity?
I mean an antiquotation corresponding to the quotation syntax \<^term>‹...›. For example if I had val x = \<^term>‹1› then \<^term>‹$x + $x› yields the same term as if I had written \<^term>‹1 + 1›. This is using $x as an antiquotation syntax, but that's not the real syntax... what is, if any?
Mario Carneiro (Aug 21 2024 at 06:26):Mathias Fleury said:
it is the usual implicit PROP inclusion
I'm confused by what this PROP thing is. The pretty printer seems to insert it sometimes, and apparently the parser also wants to see it, but AFAICT it has no existence in the generated term, PROP is not an actual operator like Pure.imp or HOL.Trueprop. What is it?
Mario Carneiro (Aug 21 2024 at 06:28):From my understanding of Pure logic, there should not be anything there, we just have a variable P :: 'a ==> prop and Pure.imp :: prop ==> prop ==> prop is expecting an argument of type prop so P x ==> Q x should just work without anything extra.
Mathias Fleury (Aug 21 2024 at 06:37):I do not really know. I have decided years ago that trying to understand everything in Isabelle means never getting any work done, so I stopped trying. I just look how it is done in other places of the code (actually you can see in in Pure.thy that the PROP are there too)….
Mario Carneiro (Aug 21 2024 at 06:38):oh yes, I have definitely felt the "staring into the abyss" feeling when reading isabelle sources. I just hope that if I keep doing it enough eventually the feeling will subside...
Mario Carneiro (Aug 21 2024 at 06:40):I wonder whether it would be a good idea to try writing comments on as much as I can
Mathias Fleury (Aug 21 2024 at 06:41):My own feeling is that there are parts in Isabelle which are understood by 0.1 people like contexts (.1 because Makarius would write that he understands that… after spending one week work on it and complaining that everyone is doing it wrong)
Mathias Fleury (Aug 21 2024 at 06:41):Mario Carneiro said:
I wonder whether it would be a good idea to try writing comments on as much as I can
To quote Makarius:
"I would say that misleading error messages are quiet normal." ("[isabelle-dev] scala-2.12.2", 19 June 2017, 14h16)
Mathias Fleury (Aug 21 2024 at 06:42):so comments are great, but they will never end in the official sources and will probably just die out like the ML cookbook
Mario Carneiro (Aug 21 2024 at 06:43):why can't the official sources get comments?
Mathias Fleury (Aug 21 2024 at 06:44):IIRC Makarius arguments is that:
- comments never get updated. So they become wrong and it is better to have no comments that wrong comments
- the isabelle code is so beautiful that it does not need comments
Mario Carneiro (Aug 21 2024 at 06:45):I see. I couldn't disagree more on both counts, but I see I need to be having this conversation with someone else
Mathias Fleury (Aug 21 2024 at 06:47):I totally agree with you
Kevin Kappelmann (Aug 21 2024 at 07:14):Mario Carneiro said:
I'm confused by what this
PROPthing is. The pretty printer seems to insert it sometimes, and apparently the parser also wants to see it, but AFAICT it has no existence in the generated term,PROPis not an actual operator likePure.imporHOL.Trueprop. What is it?
PROP just exists in the pure grammar. It is not a logical constant. See the reference manual. As far as I know, it exists to suppress the implicit insertion of judgments (like Trueprop in Isabelle/HOL). Those judgments (which embed object logic propositions into prop) are added implicitly because, in most cases, people work in an object logic, not in Pure directly. It would be annoying to add judgments around statements, assumptions, etc. manually all the time, so Isabelle adds them implicitly for you. See also reference manual
Here's an example that. The first term uses variables A, B of type bool, the second one A, B of type prop.
theory Scratch
imports Main
begin
declare[[show_types]]
term "A ⟹ B"
term "PROP A ⟹ PROP B"
end
Speculation: Isabelle's parser could be smarter and simply add PROPs automatically for you in case there are no registered judgements in context.
Mario Carneiro (Aug 21 2024 at 07:15):the type bool is coming from HOL here?
Kevin Kappelmann (Aug 21 2024 at 07:15):Yes, see src/HOL/HOL.thy
Kevin Kappelmann (Aug 21 2024 at 07:19):Since you are working on Isabelle exports, I recommend to check out some sort of object logic setup (like HOL.thy) in any case. That might be instructive.
Mario Carneiro (Aug 21 2024 at 07:20):(I've been using the FOL session as my testbed, since it's quite a bit smaller than HOL main)
Kevin Kappelmann (Aug 21 2024 at 07:21):Yeah, the same things happen there. Just note that FOL imports IFOL and that's where the judgment is declared.
Mario Carneiro (Aug 21 2024 at 07:23):Is there syntax for constructing terms involving Var? I tried things like term<?P> but this seems to always fail saying "Unbound schematic variable"
Kevin Kappelmann (Aug 21 2024 at 07:30):val t = Proof_Context.read_term_schematic @{context} "?f (?x :: ?'a) ?x2"
Or read_term_pattern, depending on your preference.
Manuel Eberl (Aug 30 2024 at 09:12):Not sure if I understood your above questions correctly, but there are also some antiquotations that allow you to make a term with some "holes" in it that get filled in with ML values. A bit like string interpolation in Python.
Jonathan Julian Huerta y Munive (Aug 30 2024 at 09:33):Mario Carneiro said:
The following is a syntax error at the
⟹but I don't see why... Isn't this legal Pure syntax?
I do not know the precise answer to your question but I suspect that the syntax for your term is defined somewhere between Pure and "HOL.HOL".
Also, does
\<^term>have an antiquotation syntax for ML values of typeterm?
Do you mean @{term "write_your_term_here"}?
I'm confused by what this
PROPthing is. The pretty printer seems to insert it sometimes, and apparently the parser also wants to see it, but AFAICT it has no existence in the generated term,PROPis not an actual operator likePure.imporHOL.Trueprop. What is it?
You can check its definition in pure_thy.ML line 199 (at least it appears there in my Isabelle-repo version): [(const "Pure.prop", typ "prop ⇒ prop", mixfix ("_", [0], 0))]
Jonathan Julian Huerta y Munive (Aug 30 2024 at 09:39):Mario Carneiro said:
oh yes, I have definitely felt the "staring into the abyss" feeling when reading isabelle sources. I just hope that if I keep doing it enough eventually the feeling will subside...
I've spent a good chunk of 8 months reading Isabelle/ML and Isabelle/Scala files. I want to write a summary of my current understanding but I have other priorities in the next two months. What was useful for me is the discovery that reading Makarius' manuals and the Isabelle/ML cookbook alongside with the code, helps a lot in understanding its structure.
Last updated: Dec 21 2024 at 16:20 UTC