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