author nipkow Thu Sep 06 16:50:00 2018 +0200 (9 months ago) changeset 68919 027219002f32 parent 68916 2a1583baaaa0 child 68920 e50312982ba0
added int and real
     1.1 --- a/src/Doc/Prog_Prove/Bool_nat_list.thy	Wed Sep 05 21:56:44 2018 +0200
1.2 +++ b/src/Doc/Prog_Prove/Bool_nat_list.thy	Thu Sep 06 16:50:00 2018 +0200
1.3 @@ -1,6 +1,6 @@
1.4  (*<*)
1.5  theory Bool_nat_list
1.6 -imports Main
1.7 +imports Complex_Main
1.8  begin
1.9  (*>*)
1.10
1.11 @@ -423,6 +423,48 @@
1.12
1.13  From now on lists are always the predefined lists.
1.14
1.15 +\ifsem\else
1.16 +\subsection{Types @{typ int} and @{typ real}}
1.17 +
1.18 +In addition to @{typ nat} there are also the types @{typ int} and @{typ real}, the mathematical integers
1.19 +and real numbers. As mentioned above, numerals and most of the standard arithmetic operations are overloaded.
1.20 +In particular they are defined on @{typ int} and @{typ real}.
1.21 +
1.22 +\begin{warn}
1.23 +There are two infix exponentiation operators:
1.24 +@{term "(^)"} for @{typ nat} and @{typ int} (with exponent of type @{typ nat} in both cases)
1.25 +and @{term "(powr)"} for @{typ real}.
1.26 +\end{warn}
1.27 +\begin{warn}
1.28 +Type  @{typ int} is already part of theory @{theory Main}, but in order to use @{typ real} as well, you have to import
1.29 +theory @{theory Complex_Main} instead of @{theory Main}.
1.30 +\end{warn}
1.31 +
1.32 +There are three conversion functions, meaning inclusions:
1.33 +\begin{quote}
1.34 +\begin{tabular}{rcl}
1.35 +@{const int} &\<open>::\<close>& @{typ "nat \<Rightarrow> int"}\\
1.36 +@{const real} &\<open>::\<close>& @{typ "nat \<Rightarrow> real"}\\
1.37 +@{const real_of_int} &\<open>::\<close>& @{typ "int \<Rightarrow> real"}\\
1.38 +\end{tabular}
1.39 +\end{quote}
1.40 +
1.41 +Isabelle inserts these conversion functions automatically once you import \<open>Complex_Main\<close>.
1.42 +If there are multiple type-correct completions, Isabelle chooses an arbitrary one.
1.43 +For example, the input \noquotes{@{term[source] "(i::int) + (n::nat)"}} has the unique
1.44 +type-correct completion @{term"(i::int) + int(n::nat)"}. In contrast,
1.45 +\noquotes{@{term[source] "((n::nat) + n) :: real"}} has two type-correct completions,
1.46 +\noquotes{@{term[source]"real(n+n)"}} and \noquotes{@{term[source]"real n + real n"}}.
1.47 +
1.48 +There are also the coercion functions in the other direction:
1.49 +\begin{quote}
1.50 +\begin{tabular}{rcl}
1.51 +@{const nat} &\<open>::\<close>& @{typ "int \<Rightarrow> nat"}\\
1.52 +@{const floor} &\<open>::\<close>& @{typ "real \<Rightarrow> int"}\\
1.53 +@{const ceiling} &\<open>::\<close>& @{typ "real \<Rightarrow> int"}\\
1.54 +\end{tabular}
1.55 +\end{quote}
1.56 +\fi
1.57
1.58  \subsection*{Exercises}
1.59

     2.1 --- a/src/Doc/Prog_Prove/Types_and_funs.thy	Wed Sep 05 21:56:44 2018 +0200
2.2 +++ b/src/Doc/Prog_Prove/Types_and_funs.thy	Thu Sep 06 16:50:00 2018 +0200
2.3 @@ -538,6 +538,14 @@
2.4  Splitting if or case-expressions in the assumptions requires
2.5  @{text "split: if_splits"} or @{text "split: t.splits"}.
2.6
2.7 +\ifsem\else
2.8 +\subsection{Converting Numerals to @{const Suc} Terms}
2.9 +
2.10 +Recursive functions on type @{typ nat} are often defined by pattern matching over @{text 0} and @{const Suc},
2.11 +e.g. @{text "f 0 = ..."} and  @{text "f (Suc n) = ..."}. In order to simplify \<open>f 2\<close>, the \<open>2\<close>
2.12 +needs to be converted to @{term "Suc(Suc 0)"} first. The simplification rule @{thm[source] numeral_eq_Suc}
2.13 +converts all numerals to @{const Suc} terms.
2.14 +\fi
2.15
2.16  \subsection*{Exercises}
2.17