author | wenzelm |
Wed, 25 Mar 2015 11:39:52 +0100 | |
changeset 59809 | 87641097d0f3 |
parent 58926 | baf5a3c28f0c |
permissions | -rw-r--r-- |
15136 | 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 | 3 |
begin |
8751 | 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 | 9 |
datatype 'a list = Nil ("[]") |
9541 | 10 |
| Cons 'a "'a list" (infixr "#" 65) |
8751 | 11 |
|
38430
254a021ed66e
tuned text about "value" and added note on comments.
nipkow
parents:
27015
diff
changeset
|
12 |
(* This is the append function: *) |
27015 | 13 |
primrec app :: "'a list => 'a list => 'a list" (infixr "@" 65) |
14 |
where |
|
15 |
"[] @ ys = ys" | |
|
9541 | 16 |
"(x # xs) @ ys = x # (xs @ ys)" |
8751 | 17 |
|
27015 | 18 |
primrec rev :: "'a list => 'a list" where |
19 |
"rev [] = []" | |
|
9541 | 20 |
"rev (x # xs) = (rev xs) @ (x # [])" |