author | berghofe |
Fri, 23 Oct 1998 12:56:13 +0200 | |
changeset 5738 | 0d8698c15439 |
parent 5717 | 0d28dbe484b6 |
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 |