src/Doc/Tutorial/Recdef/examples.thy
changeset 58860 fee7cfa69c50
parent 48985 5386df44a037
child 67406 23307fd33906
     1.1 --- a/src/Doc/Tutorial/Recdef/examples.thy	Sat Nov 01 11:40:55 2014 +0100
     1.2 +++ b/src/Doc/Tutorial/Recdef/examples.thy	Sat Nov 01 14:20:38 2014 +0100
     1.3 @@ -1,16 +1,16 @@
     1.4  (*<*)
     1.5 -theory examples imports Main begin;
     1.6 +theory examples imports Main begin
     1.7  (*>*)
     1.8  
     1.9  text{*
    1.10  Here is a simple example, the \rmindex{Fibonacci function}:
    1.11  *}
    1.12  
    1.13 -consts fib :: "nat \<Rightarrow> nat";
    1.14 +consts fib :: "nat \<Rightarrow> nat"
    1.15  recdef fib "measure(\<lambda>n. n)"
    1.16    "fib 0 = 0"
    1.17    "fib (Suc 0) = 1"
    1.18 -  "fib (Suc(Suc x)) = fib x + fib (Suc x)";
    1.19 +  "fib (Suc(Suc x)) = fib x + fib (Suc x)"
    1.20  
    1.21  text{*\noindent
    1.22  \index{measure functions}%
    1.23 @@ -27,11 +27,11 @@
    1.24  between any two elements of a list:
    1.25  *}
    1.26  
    1.27 -consts sep :: "'a \<times> 'a list \<Rightarrow> 'a list";
    1.28 +consts sep :: "'a \<times> 'a list \<Rightarrow> 'a list"
    1.29  recdef sep "measure (\<lambda>(a,xs). length xs)"
    1.30    "sep(a, [])     = []"
    1.31    "sep(a, [x])    = [x]"
    1.32 -  "sep(a, x#y#zs) = x # a # sep(a,y#zs)";
    1.33 +  "sep(a, x#y#zs) = x # a # sep(a,y#zs)"
    1.34  
    1.35  text{*\noindent
    1.36  This time the measure is the length of the list, which decreases with the
    1.37 @@ -43,20 +43,20 @@
    1.38  need not be exhaustive:
    1.39  *}
    1.40  
    1.41 -consts last :: "'a list \<Rightarrow> 'a";
    1.42 +consts last :: "'a list \<Rightarrow> 'a"
    1.43  recdef last "measure (\<lambda>xs. length xs)"
    1.44    "last [x]      = x"
    1.45 -  "last (x#y#zs) = last (y#zs)";
    1.46 +  "last (x#y#zs) = last (y#zs)"
    1.47  
    1.48  text{*
    1.49  Overlapping patterns are disambiguated by taking the order of equations into
    1.50  account, just as in functional programming:
    1.51  *}
    1.52  
    1.53 -consts sep1 :: "'a \<times> 'a list \<Rightarrow> 'a list";
    1.54 +consts sep1 :: "'a \<times> 'a list \<Rightarrow> 'a list"
    1.55  recdef sep1 "measure (\<lambda>(a,xs). length xs)"
    1.56    "sep1(a, x#y#zs) = x # a # sep1(a,y#zs)"
    1.57 -  "sep1(a, xs)     = xs";
    1.58 +  "sep1(a, xs)     = xs"
    1.59  
    1.60  text{*\noindent
    1.61  To guarantee that the second equation can only be applied if the first
    1.62 @@ -74,10 +74,10 @@
    1.63    arguments as in the following definition:
    1.64  \end{warn}
    1.65  *}
    1.66 -consts sep2 :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list";
    1.67 +consts sep2 :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"
    1.68  recdef sep2 "measure length"
    1.69    "sep2 (x#y#zs) = (\<lambda>a. x # a # sep2 (y#zs) a)"
    1.70 -  "sep2 xs       = (\<lambda>a. xs)";
    1.71 +  "sep2 xs       = (\<lambda>a. xs)"
    1.72  
    1.73  text{*
    1.74  Because of its pattern-matching syntax, \isacommand{recdef} is also useful
    1.75 @@ -85,10 +85,10 @@
    1.76  degenerates to the empty set @{term"{}"}:
    1.77  *}
    1.78  
    1.79 -consts swap12 :: "'a list \<Rightarrow> 'a list";
    1.80 +consts swap12 :: "'a list \<Rightarrow> 'a list"
    1.81  recdef swap12 "{}"
    1.82    "swap12 (x#y#zs) = y#x#zs"
    1.83 -  "swap12 zs       = zs";
    1.84 +  "swap12 zs       = zs"
    1.85  
    1.86  (*<*)
    1.87  end