[isabelle] I want to print axiomatization info



Hi,

I have a function:

axiomatization--"Set membership predicate."
in\<^isub>\<sigma>::"\<sigma>\<^isub>t \<Rightarrow> \<sigma>\<^isub>t \<Rightarrow> \<sigma>\<^isub>t\<^isub>b" ("_ \<in>\<^isub>\<sigma> _" 55)

I then state multiple axioms about it, one of them being:

axiomatization--"Axiom schema of comprehension: schema set." where
\<Sigma>\<^isub>s\<^isub>c\<^isub>A: "\<forall>u. \<forall>P. \<exists>a. \<forall>x.(x \<in>\<^isub>\<sigma> a \<longleftrightarrow> (x \<in>\<^isub>\<sigma> u \<and> P x))"

I want to look at how Isabelle decided to type variables in my axiomatization, but I can't find any print or find commands that will do that for me. I also want to see if explicit parentheses will be added as I expect, and see if there are any operator priority surprises.

Is there such a command that will do this for me?

The above is the basic question. Here's what led me to want to know this:

1) I used "\<in>" as notation for my set membership.
2) I got lots of warnings like: "Ambiguous input produces 4 parse trees... Fortunately, only one parse tree is type correct..." 3) I change my notation to " \<in>\<^isub>\<sigma>", and it gets rid of some of the warnings. 4) For the axiom above, I still get "ambiguous" warnings, with some of the variables explicitly typed. 5) So, I explicitly type every variable in the formula, and I still get "ambiguous" warnings. 6) So, I remove all the typing, and it seems to work. Explicit or non-explicit typing doesn't affect the warnings. 7) I then conclude that Isabelle gets all of the typing information in the formula from my one uniquely named function, "in\<^isub>\<sigma>". Consequently, I ask myself, "Is that too good to be true?"

Okay, if I knew how to prove anything, maybe I would know how to get the information I want. However, even if I was an expert, I would want to be able to get immediate feedback to check my typing, see if I'm correctly using parentheses, and see if I understand correctly the priority of the operators.

I attach a screen shot of my code. I don't think attaching images and PDFs is the best way to give people code information. On the other hand, the above low-level Isar shows that nice looking things in jEdit cease to be good for reading in a text file. Also, "\<^isub>" doesn't result in subscripted, unicode characters when copying and pasting.

jEdit Stuff: I edited the etc/symbols file and jEdit gave me an exception error when loading. Afterwards, jEdit wouldn't translate commands like "\<in>" in the one file. About an hour later, or two, I deleted "jEdit/recent.xml" and it started working again.

Regards,
GB

Attachment: wantToPrintAxiomInfo.png
Description: PNG image



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