doc-src/TutorialI/Misc/types.thy

some preliminary stuff on conversion;

(*<*)
theory "types" = Main:;
(*>*)types number       = nat
      gate         = "bool \<Rightarrow> bool \<Rightarrow> bool"
      ('a,'b)alist = "('a \<times> 'b)list";

text{*\noindent\indexbold{*types}%
Internally all synonyms are fully expanded.  As a consequence Isabelle's
output never contains synonyms.  Their main purpose is to improve the
readability of theories.  Synonyms can be used just like any other
type:
*}

consts nand :: gate
       exor :: gate;

text{*
\subsection{Constant definitions}
\label{sec:ConstDefinitions}
\indexbold{definition}

The above constants @{term"nand"} and @{term"exor"} are non-recursive and can
therefore be defined directly by
*}

defs nand_def: "nand A B \<equiv> \<not>(A \<and> B)"
     exor_def: "exor A B \<equiv> A \<and> \<not>B \<or> \<not>A \<and> B";

text{*\noindent%
where \isacommand{defs}\indexbold{*defs} is a keyword and
@{thm[source]nand_def} and @{thm[source]exor_def} are user-supplied names.
The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
that must be used in constant definitions.
Declarations and definitions can also be merged
*}

constdefs nor :: gate
         "nor A B \<equiv> \<not>(A \<or> B)"
          exor2 :: gate
         "exor2 A B \<equiv> (A \<or> B) \<and> (\<not>A \<or> \<not>B)";

text{*\noindent\indexbold{*constdefs}%
in which case the default name of each definition is $f$@{text"_def"}, where
$f$ is the name of the defined constant.*}(*<*)
end
(*>*)