Logics_ZF/document/ZF.tex

113 The language of set theory, as studied by logicians, has no constants.  The
127 Local abbreviations can be introduced by a \isa{let} construct whose
129 the constant~\cdx{Let}.  It can be expanded by rewriting with its
266 The constant \cdx{Collect} constructs sets by the principle of {\bf
274 The constant \cdx{Replace} constructs sets by the principle of {\bf
418 presented by Suppes~\cite{suppes72}.  Most of the theory consists of
421 been replaced by meta-level ones wherever possible, to simplify use of the
528   rules} \tdx{ball_cong} and \tdx{bex_cong} are required by Isabelle's
533 relations (proof by extensionality), and rules about the empty set and the
700 (\tdx{mem_asym}) is proved by applying the Axiom of Foundation to
796   by the parser and printer.  Thus the internal and external form of a term
801 variable binding construct which is internally described by a
929 Functions, represented by graphs, are notoriously difficult to reason
941 family of sets $\{B(x)\}@{x\in A}$.  Conversely, by \tdx{range_of_fun},
1182 automatically.  The induction rule shown is stronger than the one proved by
1249 list functions by primitive recursion.  See theory \texttt{List}.
1312 Theory \thydx{Univ} defines a `universe' $\isa{univ}(A)$, which is used by
1320 Theory \thydx{QUniv} defines a `universe' $\isa{quniv}(A)$, which is used by
1340 The default simpset used by \isa{simp} contains congruence rules for all of ZF's
1370 essentially type-checking.  Such proofs are built by applying rules such as
1381 we have a specific term~$t$ and need to infer its `type' by instantiating the
1437 %by (asm_simp_tac
1501 by primitive recursion.  Division and remainder are defined by repeated
1518 can either be tolerated or else eliminated by proving that the argument is a
1567 operators defined in Fig.\ts\ref{zf-int} coerce their operands to integers by
1575 by simplification.  The simplifier also collects similar terms, multiplying
1576 them by a numerical coefficient.  It also cancels occurrences of the same
1639 defined by
1648 Trees and forests can be modelled by the mutually recursive datatype
1662 The datatype \isa{term}, which is defined by
1696 without mutual or nested recursion, the rule has the form exemplified by
1812 \subsubsection{The theorems proved by a datatype declaration}
1856 We begin by declaring the constructor's typechecking rules
1871 This can be proved by the structural induction tactic:
1907 \ \ \isacommand{by}\ (blast\ elim!:\ bt.free\_elims)
1961 \ \ \isacommand{by}\ simp
1975   recursion}.  Such definitions rely on the recursion operator defined by the
1979 In principle, one could introduce primitive recursive functions by asserting
2020 If you would like to refer to some rule by name, then you must prefix
2028 \ \ \isacommand{by}\ (induct\_tac\ t,\ auto)
2033 syntax for defining functions by cases.
2057 \ \ \isacommand{by}\ (induct\_tac\ t,\ simp\_all)
2071 \ \isacommand{by}\ (simp\ add:\ n\_nodes\_tail\_def\ n\_nodes\_aux\_eq)
2090 seen as arising by applying a rule to elements of~$R$.)  An important example
2273 Finally, here are some coinductive definitions.  We begin by defining
2509 two inclusions by extensionality:\index{*equalityI theorem}
2526 Subgoal~1 follows by applying the monotonicity of \isa{Pow} to $A\int
2550 The next step replaces the \isa{Pow} by the subset
2575 We could have performed this proof instantly by calling
2579 \isacommand{by}
2582 the symbols are replaced by their definitions.
2662 We must show that the pair belongs to~$f$ or~$g$; by~\tdx{UnI1} we