1 (* Title: HOL/ex/Term |
1 (* Title: HOL/Induct/Term.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Stefan Berghofer, TU Muenchen |
4 Copyright 1992 University of Cambridge |
4 Copyright 1998 TU Muenchen |
5 |
5 |
6 Terms over a given alphabet -- function applications; illustrates list functor |
6 Terms over a given alphabet -- function applications |
7 (essentially the same type as in Trees & Forests) |
|
8 |
|
9 There is no constructor APP because it is simply Scons |
|
10 *) |
7 *) |
11 |
8 |
12 Term = SList + |
9 Term = Main + |
13 |
10 |
14 types 'a term |
11 datatype |
|
12 ('a, 'b) term = Var 'a |
|
13 | App 'b ((('a, 'b) term) list) |
15 |
14 |
16 arities term :: (term)term |
15 |
|
16 (** substitution function on terms **) |
17 |
17 |
18 consts |
18 consts |
19 term :: 'a item set => 'a item set |
19 subst_term :: "['a => ('a, 'b) term, ('a, 'b) term] => ('a, 'b) term" |
20 Rep_term :: 'a term => 'a item |
20 subst_term_list :: |
21 Abs_term :: 'a item => 'a term |
21 "['a => ('a, 'b) term, ('a, 'b) term list] => ('a, 'b) term list" |
22 Rep_Tlist :: 'a term list => 'a item |
|
23 Abs_Tlist :: 'a item => 'a term list |
|
24 App :: ['a, ('a term)list] => 'a term |
|
25 Term_rec :: ['a item, ['a item , 'a item, 'b list]=>'b] => 'b |
|
26 term_rec :: ['a term, ['a ,'a term list, 'b list]=>'b] => 'b |
|
27 |
22 |
28 inductive "term(A)" |
23 primrec |
29 intrs |
24 "subst_term f (Var a) = f a" |
30 APP_I "[| M: A; N : list(term(A)) |] ==> Scons M N : term(A)" |
25 "subst_term f (App b ts) = App b (subst_term_list f ts)" |
31 monos list_mono |
|
32 |
26 |
33 defs |
27 "subst_term_list f [] = []" |
34 (*defining abstraction/representation functions for term list...*) |
28 "subst_term_list f (t # ts) = |
35 Rep_Tlist_def "Rep_Tlist == Rep_map(Rep_term)" |
29 subst_term f t # subst_term_list f ts" |
36 Abs_Tlist_def "Abs_Tlist == Abs_map(Abs_term)" |
|
37 |
30 |
38 (*defining the abstract constants*) |
|
39 App_def "App a ts == Abs_term(Scons (Leaf a) (Rep_Tlist ts))" |
|
40 |
|
41 (*list recursion*) |
|
42 Term_rec_def |
|
43 "Term_rec M d == wfrec (trancl pred_sexp) |
|
44 (%g. Split(%x y. d x y (Abs_map g y))) M" |
|
45 |
|
46 term_rec_def |
|
47 "term_rec t d == |
|
48 Term_rec (Rep_term t) (%x y r. d (inv Leaf x) (Abs_Tlist(y)) r)" |
|
49 |
|
50 rules |
|
51 (*faking a type definition for term...*) |
|
52 Rep_term "Rep_term(n): term(range(Leaf))" |
|
53 Rep_term_inverse "Abs_term(Rep_term(t)) = t" |
|
54 Abs_term_inverse "M: term(range(Leaf)) ==> Rep_term(Abs_term(M)) = M" |
|
55 end |
31 end |