| author | wenzelm |
| Wed, 30 Aug 2000 17:54:26 +0200 | |
| changeset 9750 | 270cd9831e7b |
| parent 5738 | 0d8698c15439 |
| child 11046 | b5f5942781a0 |
| permissions | -rw-r--r-- |
|
5738
0d8698c15439
Terms are now defined using the new datatype package.
berghofe
parents:
5717
diff
changeset
|
1 |
(* Title: HOL/Induct/Term.thy |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
|
5738
0d8698c15439
Terms are now defined using the new datatype package.
berghofe
parents:
5717
diff
changeset
|
3 |
Author: Stefan Berghofer, TU Muenchen |
|
0d8698c15439
Terms are now defined using the new datatype package.
berghofe
parents:
5717
diff
changeset
|
4 |
Copyright 1998 TU Muenchen |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
5 |
|
|
5738
0d8698c15439
Terms are now defined using the new datatype package.
berghofe
parents:
5717
diff
changeset
|
6 |
Terms over a given alphabet -- function applications |
|
3120
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 |
|
|
5738
0d8698c15439
Terms are now defined using the new datatype package.
berghofe
parents:
5717
diff
changeset
|
9 |
Term = Main + |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
10 |
|
|
5738
0d8698c15439
Terms are now defined using the new datatype package.
berghofe
parents:
5717
diff
changeset
|
11 |
datatype |
|
0d8698c15439
Terms are now defined using the new datatype package.
berghofe
parents:
5717
diff
changeset
|
12 |
('a, 'b) term = Var 'a
|
|
0d8698c15439
Terms are now defined using the new datatype package.
berghofe
parents:
5717
diff
changeset
|
13 |
| App 'b ((('a, 'b) term) list)
|
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
14 |
|
|
5738
0d8698c15439
Terms are now defined using the new datatype package.
berghofe
parents:
5717
diff
changeset
|
15 |
|
|
0d8698c15439
Terms are now defined using the new datatype package.
berghofe
parents:
5717
diff
changeset
|
16 |
(** substitution function on terms **) |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
17 |
|
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
18 |
consts |
|
5738
0d8698c15439
Terms are now defined using the new datatype package.
berghofe
parents:
5717
diff
changeset
|
19 |
subst_term :: "['a => ('a, 'b) term, ('a, 'b) term] => ('a, 'b) term"
|
|
0d8698c15439
Terms are now defined using the new datatype package.
berghofe
parents:
5717
diff
changeset
|
20 |
subst_term_list :: |
|
0d8698c15439
Terms are now defined using the new datatype package.
berghofe
parents:
5717
diff
changeset
|
21 |
"['a => ('a, 'b) term, ('a, 'b) term list] => ('a, 'b) term list"
|
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
22 |
|
|
5738
0d8698c15439
Terms are now defined using the new datatype package.
berghofe
parents:
5717
diff
changeset
|
23 |
primrec |
|
0d8698c15439
Terms are now defined using the new datatype package.
berghofe
parents:
5717
diff
changeset
|
24 |
"subst_term f (Var a) = f a" |
|
0d8698c15439
Terms are now defined using the new datatype package.
berghofe
parents:
5717
diff
changeset
|
25 |
"subst_term f (App b ts) = App b (subst_term_list f ts)" |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
26 |
|
|
5738
0d8698c15439
Terms are now defined using the new datatype package.
berghofe
parents:
5717
diff
changeset
|
27 |
"subst_term_list f [] = []" |
|
0d8698c15439
Terms are now defined using the new datatype package.
berghofe
parents:
5717
diff
changeset
|
28 |
"subst_term_list f (t # ts) = |
|
0d8698c15439
Terms are now defined using the new datatype package.
berghofe
parents:
5717
diff
changeset
|
29 |
subst_term f t # subst_term_list f ts" |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
30 |
|
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
31 |
end |