(*@|{}\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 =========================|@*)
(*@|%=======================================================================|@*)