author | wenzelm |
Sat, 03 Feb 2001 17:40:16 +0100 | |
changeset 11046 | b5f5942781a0 |
parent 9101 | b643f4d7b9e9 |
permissions | -rw-r--r-- |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/ex/Perm.thy |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
4 |
Copyright 1995 University of Cambridge |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
5 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
6 |
Permutations: example of an inductive definition |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
7 |
*) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
8 |
|
9101 | 9 |
Perm = Main + |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
10 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
11 |
consts perm :: "('a list * 'a list) set" |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
12 |
syntax "@perm" :: ['a list, 'a list] => bool ("_ <~~> _" [50,50] 50) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
13 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
14 |
translations |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
15 |
"x <~~> y" == "(x,y) : perm" |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
16 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
17 |
inductive perm |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
18 |
intrs |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
19 |
Nil "[] <~~> []" |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
20 |
swap "y#x#l <~~> x#y#l" |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
21 |
Cons "xs <~~> ys ==> z#xs <~~> z#ys" |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
22 |
trans "[| xs <~~> ys; ys <~~> zs |] ==> xs <~~> zs" |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
23 |
|
8354
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
3120
diff
changeset
|
24 |
|
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
3120
diff
changeset
|
25 |
consts |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
3120
diff
changeset
|
26 |
remove :: ['a, 'a list] => 'a list |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
3120
diff
changeset
|
27 |
|
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
3120
diff
changeset
|
28 |
primrec |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
3120
diff
changeset
|
29 |
"remove x [] = []" |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
3120
diff
changeset
|
30 |
"remove x (y#ys) = (if x=y then ys else y#remove x ys)" |
c02e3c131eca
function "remove" and new lemmas for Factorization
paulson
parents:
3120
diff
changeset
|
31 |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
32 |
end |