merged
authornipkow
Thu Sep 06 16:50:16 2018 +0200 (9 months ago)
changeset 68920e50312982ba0
parent 68918 3a0db30e5d87
parent 68919 027219002f32
child 68921 35ea237696cf
child 68922 1751765b636d
merged
     1.1 --- a/src/Doc/Prog_Prove/Bool_nat_list.thy	Thu Sep 06 14:08:35 2018 +0200
     1.2 +++ b/src/Doc/Prog_Prove/Bool_nat_list.thy	Thu Sep 06 16:50:16 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	Thu Sep 06 14:08:35 2018 +0200
     2.2 +++ b/src/Doc/Prog_Prove/Types_and_funs.thy	Thu Sep 06 16:50:16 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