[isabelle] Schematic vars or universal bound vars in theorem?



Hi,

I summarize my question first.

I have two theorems, SigmaE_is_unique and SigmaE_is_unique2. In the first, I end up with "u" as a universally quantified bound variable, because that's how I specified it in the formula. In the second, I end up with "u" as a schematic variable, because I left it as a free variable in the formula.

Which of these do I want? This question also applies to my axiom Sigma_exA.

I read this thread, "Free variables vs schematic variables":

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-June/msg00048.html

I've also read this email, which is an aside:

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-June/msg00172.html

The context of that thread was meta-logic, so when Makarius says, "Outermost quantifiers are circumvented... there is an explicit core inference that removes the quantifiers and expresses the generality in terms of schematic variables", I conclude that he's talking about the \<And> quantifier. This is because I don't see any removal of \<forall>.

I do notice in proof steps and theorem results, that Isabelle may rearrange a \<forall> in a formula, such as taking a \<forall> to the outside of some parentheses. That's fine with me.

Here, I use my limited knowledge to determine the difference in my two theorems mentioned above. If all the variables in the theorem are bound, then the formula in the theorem will simply be used as a fact.

If there are schematic variables in the theorem, then schematic variables will first be instantiated, and the instantiated formula of the theorem will be used as a fact.

I don't know why I need variables to be instantiated to make it more general, or whether I don't want variables to be instantiated so that it's tighter.

This also applies to my axiom Sigma_exA. I can strip out all the universal quantifiers, and everything still works, but I end up with schematic variables being used, as shown by "thm show_info2", although it may be the proof step of show_info2 that's really a true reflection of Sigma_EeA, in which the variables are still free.

I attached the theory, where some names above are rough translations.

Thanks,
GB

(*@|{}\input{article-ipre}|@*)
(*@|\begin{document}|@*)
(*@|\isaTitlePage{sTs}
                 {\ }
                 {\ }
                 {\myIsaName}|@*)
(*@|{}\input{article-ifront}|@*)
(*@|\newpage|@*)
(*@|%=======================================================================|@*)
(*@|%========================== MAINMATTER =================================|@*)
(*@|%=======================================================================|@*)

(*@|%=======================================================================|@*)
(*@|%========================== HEADER START ===============================|@*)
(*@|\setcounter{\CTRONE}{0}|@*)
(*@|\uONE{Theory Header}{0.0}{a}|@*)
(*@|% VRBF sets the start number. DON'T DELETE AND REPLACE IT WITH A VRBL   |@*)
(*@|\VRBF|@*)
theory sTs_
imports Main
       (*"../../pi/I"*)(*Declare, print, sledge, nitP cmds. Not really needed.*)
begin
(*@|\end{Verbatim}|@*)
(*@|%========================== HEADER END =================================|@*)
(*@|%=======================================================================|@*)

text{*@|\aONE{Scratch}{1.0}{a}|@*}
(*@|\VRBL|@*)
--"Set Variable and Constant Naming Convention"
  --"Everything is a set, but some sets are viewed primarily as 'sets', and some
     primarily viewed as 'elements'."
  --"For the beginning parts of axiomatic-modeled set theory, lower case is
     used."
  --"This is to emphasize first-order formulas. At some point, there is a switch
     to uppercase to represent 'sets', with lowercase representing 'elements of
     sets'."
  --"Variables in the scope of '\<forall>' are called 'variables'."
  --"For naming, variables in the scope of '\<exists>' are loosely called 'constants'."
  --"Variables are generally taken from the end of the alphabet."
  --"Constants are generally taken from the beginning of the alphabet."
  --"Context should ultimately be used to interpret what names imply; naming
     conventions might be ignored at times."
  --"Set variables...............r, s, t, u, v."
  --"Element variables...........w, x, y, z."
  --"Set and element constants...a, b, c, d, etc."

--"============================================================================"
typedecl --"The primitive set type: everything is a set."
  \<sigma>\<^isub>e\<^isub>t
--"============================================================================"
type_synonym --"Set property: Axiom schema of comprehension property type."
  \<sigma>\<^isub>p\<^isub>t = "\<sigma>\<^isub>e\<^isub>t \<Rightarrow> bool"
--"============================================================================"
consts --"Set membership predicate: to be axiomatized by subsequent axioms."
  in\<^isub>\<sigma>::"\<sigma>\<^isub>e\<^isub>t \<Rightarrow> \<sigma>\<^isub>e\<^isub>t \<Rightarrow> bool" (infixl "\<in>\<^isub>\<sigma>" 55)
--"============================================================================"
consts --"The empty set: naively named as a constant."
  \<Sigma>\<^isub>\<E>::\<sigma>\<^isub>e\<^isub>t
--"============================================================================"
axiomatization --"Axiom of existence: the empty set is empty." where
  \<Sigma>\<^isub>\<E>\<^isub>e\<^isub>A:"\<forall>x\<Colon>\<sigma>\<^isub>e\<^isub>t. \<not>(x \<in>\<^isub>\<sigma> \<Sigma>\<^isub>\<E>)"
--"============================================================================"
axiomatization --"Axiom of extention: set equality." where
  \<Sigma>\<^isub>e\<^isub>x\<^isub>A: "\<forall>u\<Colon>\<sigma>\<^isub>e\<^isub>t. \<forall>v\<Colon>\<sigma>\<^isub>e\<^isub>t. \<forall>x\<Colon>\<sigma>\<^isub>e\<^isub>t.((x \<in>\<^isub>\<sigma> u \<longleftrightarrow> x \<in>\<^isub>\<sigma> v) \<longrightarrow> u = v )"
  (*\<Sigma>\<^isub>e\<^isub>x\<^isub>A: "(x \<in>\<^isub>\<sigma> u \<longleftrightarrow> x \<in>\<^isub>\<sigma> v) \<longrightarrow> u = v"*)
  --"SHOW INFO-----------------------------------------------------------------"
  theorem show_info:
   "(\<forall>u\<Colon>\<sigma>\<^isub>e\<^isub>t. \<forall>v\<Colon>\<sigma>\<^isub>e\<^isub>t. \<forall>x\<Colon>\<sigma>\<^isub>e\<^isub>t.((x \<in>\<^isub>\<sigma> u \<longleftrightarrow> x \<in>\<^isub>\<sigma> v) \<longrightarrow> u = v )) =
    (\<forall>u\<Colon>\<sigma>\<^isub>e\<^isub>t. \<forall>v\<Colon>\<sigma>\<^isub>e\<^isub>t. \<forall>x\<Colon>\<sigma>\<^isub>e\<^isub>t.((x \<in>\<^isub>\<sigma> u \<longleftrightarrow> x \<in>\<^isub>\<sigma> v) \<longrightarrow> u = v ))"
    by(auto)
    thm show_info
  theorem show_info2:
   "((x \<in>\<^isub>\<sigma> u \<longleftrightarrow> x \<in>\<^isub>\<sigma> v) \<longrightarrow> u = v) =
    ((x \<in>\<^isub>\<sigma> u \<longleftrightarrow> x \<in>\<^isub>\<sigma> v) \<longrightarrow> u = v)"
    by(auto)
    thm show_info2
--"============================================================================"
  --"MarW EXPL-----------------------------------------------------------------"
  theorem example1: "x = y ==> y = z ==> x = z" 
    by (rule trans)
    thm example1
  theorem example2: "\<And>x y z. x = y ==> y = z ==> x = z" 
    by (rule trans) 
    thm example2
--"============================================================================"
theorem \<Sigma>\<^isub>\<E>\<^isub>'is\<^isub>'unique --"The empty set is unique.":
  "\<forall>u.((\<forall>x. \<not>(x \<in>\<^isub>\<sigma> u) \<longrightarrow> u = \<Sigma>\<^isub>\<E>))"
  --"PROOF---------------------------------------------------------------------"
  by (metis \<Sigma>\<^isub>\<E>\<^isub>e\<^isub>A \<Sigma>\<^isub>e\<^isub>x\<^isub>A)
  thm \<Sigma>\<^isub>\<E>\<^isub>'is\<^isub>'unique
--"============================================================================"
theorem \<Sigma>\<^isub>\<E>\<^isub>'is\<^isub>'unique2 --"The empty set is unique.":
  "(\<forall>x. \<not>(x \<in>\<^isub>\<sigma> u)) \<longrightarrow> u = \<Sigma>\<^isub>\<E>"
  --"PROOF---------------------------------------------------------------------"
  by (metis \<Sigma>\<^isub>\<E>\<^isub>e\<^isub>A \<Sigma>\<^isub>e\<^isub>x\<^isub>A)
  thm \<Sigma>\<^isub>\<E>\<^isub>'is\<^isub>'unique2
--"============================================================================"
axiomatization --"Axiom of pairs: unordered pair set." where
  \<Sigma>\<^isub>u\<^isub>p\<^isub>A: "\<forall>u\<Colon>\<sigma>\<^isub>e\<^isub>t. \<forall>v\<Colon>\<sigma>\<^isub>e\<^isub>t. \<exists>a\<Colon>\<sigma>\<^isub>e\<^isub>t. \<forall>x\<Colon>\<sigma>\<^isub>e\<^isub>t.(x \<in>\<^isub>\<sigma> a \<longleftrightarrow> (x = u \<or> x = v))"
--"============================================================================"
axiomatization --"Axiom schema of comprehension: schema set." where
  \<Sigma>\<^isub>s\<^isub>c\<^isub>A: "\<forall>u\<Colon>\<sigma>\<^isub>e\<^isub>t. \<forall>P\<Colon>\<sigma>\<^isub>p\<^isub>t. \<exists>a\<Colon>\<sigma>\<^isub>e\<^isub>t. \<forall>x\<Colon>\<sigma>\<^isub>e\<^isub>t.(x \<in>\<^isub>\<sigma> a \<longleftrightarrow> (x \<in>\<^isub>\<sigma> u \<and> P x))"



text{*@|\uONE{Theory End}{99.0}{a}|@*}
(*@|\VRBL|@*)
end
(*@|\end{Verbatim}|@*)
(*@|%============================= END THEORY ==============================|@*)
(*@|%=======================================================================|@*)

(*@|%=======================================================================|@*)
(*@|%========================== AUTO-GENERATED FILES =======================|@*)
(*@|\newpage|@*)
(*@|\uONE{[---sTs.thy---]}{0.1}{b}|@*)
(*@|{}\input{sTs_Z_VerbMath.tex}|@*)
(*@|\newpage|@*)
(*@|\uONE{[---sTs.thy \textbackslash$<$cmds$>$---]}{0.1}{b}|@*)
(*@|{}\input{sTs_Z_VerbNoConvert.tex}|@*)
(*@|%========================== AUTO-GENERATED FILES =======================|@*)
(*@|%=======================================================================|@*)

(*@|%=======================================================================|@*)
(*@|%========================== BACKMATTER & END ===========================|@*)
(*@|\end{document}|@*)
(*@|%========================== BACKMATTER & END ===========================|@*)
(*@|%=======================================================================|@*)

(*@|%=======================================================================|@*)
(*@|%========================== WINEDT TREE INPUTS =========================|@*)
(*@|%input "%@('2p');\pi\pi\iEti.tex"|@*)
(*@|%========================== WINEDT TREE INPUTS =========================|@*)
(*@|%=======================================================================|@*)


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