|
1 (* Title: HOL/ex/Term |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1992 University of Cambridge |
|
5 |
|
6 Terms over a given alphabet -- function applications; illustrates list functor |
|
7 (essentially the same type as in Trees & Forests) |
|
8 |
|
9 There is no constructor APP because it is simply cons ($) |
|
10 *) |
|
11 |
|
12 Term = SList + |
|
13 |
|
14 types 'a term |
|
15 |
|
16 arities term :: (term)term |
|
17 |
|
18 consts |
|
19 term :: "'a item set => 'a item set" |
|
20 Rep_term :: "'a term => 'a item" |
|
21 Abs_term :: "'a item => 'a term" |
|
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 |
|
28 inductive "term(A)" |
|
29 intrs |
|
30 APP_I "[| M: A; N : list(term(A)) |] ==> M$N : term(A)" |
|
31 monos "[list_mono]" |
|
32 |
|
33 defs |
|
34 (*defining abstraction/representation functions for term list...*) |
|
35 Rep_Tlist_def "Rep_Tlist == Rep_map(Rep_term)" |
|
36 Abs_Tlist_def "Abs_Tlist == Abs_map(Abs_term)" |
|
37 |
|
38 (*defining the abstract constants*) |
|
39 App_def "App a ts == Abs_term(Leaf(a) $ Rep_Tlist(ts))" |
|
40 |
|
41 (*list recursion*) |
|
42 Term_rec_def |
|
43 "Term_rec M d == wfrec (trancl pred_sexp) M \ |
|
44 \ (Split(%x y g. d x y (Abs_map g y)))" |
|
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 |