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.
Description: PNG image