src/Doc/ProgProve/Types_and_funs.thy
changeset 51393 df0f306f030f
parent 48985 5386df44a037
child 51465 c5c466706549
equal deleted inserted replaced
51392:635562bc14ef 51393:df0f306f030f
    89 "lookup [] x = None" |
    89 "lookup [] x = None" |
    90 "lookup ((a,b) # ps) x = (if a = x then Some b else lookup ps x)"
    90 "lookup ((a,b) # ps) x = (if a = x then Some b else lookup ps x)"
    91 
    91 
    92 text{*
    92 text{*
    93 Note that @{text"\<tau>\<^isub>1 * \<tau>\<^isub>2"} is the type of pairs, also written @{text"\<tau>\<^isub>1 \<times> \<tau>\<^isub>2"}.
    93 Note that @{text"\<tau>\<^isub>1 * \<tau>\<^isub>2"} is the type of pairs, also written @{text"\<tau>\<^isub>1 \<times> \<tau>\<^isub>2"}.
       
    94 Pairs can be taken apart either by pattern matching (as above) or with the
       
    95 projection functions @{const fst} and @{const snd}: @{thm fst_conv} and @{thm snd_conv}. Tuples are simulated by pairs nested to the right: @{term"(a,b,c)"}
       
    96 abbreviates @{text"(a, (b, c))"} and @{text "\<tau>\<^isub>1 \<times> \<tau>\<^isub>2 \<times> \<tau>\<^isub>3"} abbreviates
       
    97 @{text "\<tau>\<^isub>1 \<times> (\<tau>\<^isub>2 \<times> \<tau>\<^isub>3)"}.
    94 
    98 
    95 \subsection{Definitions}
    99 \subsection{Definitions}
    96 
   100 
    97 Non recursive functions can be defined as in the following example:
   101 Non recursive functions can be defined as in the following example:
    98 *}
   102 *}