src/Doc/Tutorial/ToyList/ToyList1.txt
author wenzelm
Wed, 25 Mar 2015 11:39:52 +0100
changeset 59809 87641097d0f3
parent 58926 baf5a3c28f0c
permissions -rw-r--r--
tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15136
1275417e3930 Adapted text to new theory header syntax.
nipkow
parents: 9541
diff changeset
     1
theory ToyList
58926
baf5a3c28f0c proper import of Main: BNF_Least_Fixpoint does not "contain pretty much everything", especially it lacks the 'value' command, which is defined *after* theory List;
wenzelm
parents: 58372
diff changeset
     2
imports Main
15136
1275417e3930 Adapted text to new theory header syntax.
nipkow
parents: 9541
diff changeset
     3
begin
8751
9ed0548177fb *** empty log message ***
nipkow
parents:
diff changeset
     4
58926
baf5a3c28f0c proper import of Main: BNF_Least_Fixpoint does not "contain pretty much everything", especially it lacks the 'value' command, which is defined *after* theory List;
wenzelm
parents: 58372
diff changeset
     5
no_notation Nil ("[]") and Cons (infixr "#" 65) and append (infixr "@" 65)
baf5a3c28f0c proper import of Main: BNF_Least_Fixpoint does not "contain pretty much everything", especially it lacks the 'value' command, which is defined *after* theory List;
wenzelm
parents: 58372
diff changeset
     6
hide_type list
baf5a3c28f0c proper import of Main: BNF_Least_Fixpoint does not "contain pretty much everything", especially it lacks the 'value' command, which is defined *after* theory List;
wenzelm
parents: 58372
diff changeset
     7
hide_const rev
baf5a3c28f0c proper import of Main: BNF_Least_Fixpoint does not "contain pretty much everything", especially it lacks the 'value' command, which is defined *after* theory List;
wenzelm
parents: 58372
diff changeset
     8
8751
9ed0548177fb *** empty log message ***
nipkow
parents:
diff changeset
     9
datatype 'a list = Nil                          ("[]")
9541
d17c0b34d5c8 *** empty log message ***
nipkow
parents: 8846
diff changeset
    10
                 | Cons 'a "'a list"            (infixr "#" 65)
8751
9ed0548177fb *** empty log message ***
nipkow
parents:
diff changeset
    11
38430
254a021ed66e tuned text about "value" and added note on comments.
nipkow
parents: 27015
diff changeset
    12
(* This is the append function: *)
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 26729
diff changeset
    13
primrec app :: "'a list => 'a list => 'a list"  (infixr "@" 65)
f8537d69f514 *** empty log message ***
nipkow
parents: 26729
diff changeset
    14
where
f8537d69f514 *** empty log message ***
nipkow
parents: 26729
diff changeset
    15
"[] @ ys       = ys" |
9541
d17c0b34d5c8 *** empty log message ***
nipkow
parents: 8846
diff changeset
    16
"(x # xs) @ ys = x # (xs @ ys)"
8751
9ed0548177fb *** empty log message ***
nipkow
parents:
diff changeset
    17
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 26729
diff changeset
    18
primrec rev :: "'a list => 'a list" where
f8537d69f514 *** empty log message ***
nipkow
parents: 26729
diff changeset
    19
"rev []        = []" |
9541
d17c0b34d5c8 *** empty log message ***
nipkow
parents: 8846
diff changeset
    20
"rev (x # xs)  = (rev xs) @ (x # [])"