author  paulson 
Wed, 07 May 1997 12:50:26 +0200  
changeset 3120  c58423c20740 
child 5191  8ceaa19f7717 
permissions  rwrr 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

1 
(* Title: HOL/ex/Term 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

2 
ID: $Id$ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

4 
Copyright 1992 University of Cambridge 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

5 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

6 
Terms over a given alphabet  function applications; illustrates list functor 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

7 
(essentially the same type as in Trees & Forests) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

8 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

9 
There is no constructor APP because it is simply cons ($) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

10 
*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

11 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

12 
Term = SList + 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

13 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

14 
types 'a term 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

15 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

16 
arities term :: (term)term 
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 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

19 
term :: 'a item set => 'a item set 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

20 
Rep_term :: 'a term => 'a item 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

21 
Abs_term :: 'a item => 'a term 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

22 
Rep_Tlist :: 'a term list => 'a item 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

23 
Abs_Tlist :: 'a item => 'a term list 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

24 
App :: ['a, ('a term)list] => 'a term 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

25 
Term_rec :: ['a item, ['a item , 'a item, 'b list]=>'b] => 'b 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

26 
term_rec :: ['a term, ['a ,'a term list, 'b list]=>'b] => 'b 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

27 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

28 
inductive "term(A)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

29 
intrs 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

30 
APP_I "[ M: A; N : list(term(A)) ] ==> M$N : term(A)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

31 
monos "[list_mono]" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

32 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

33 
defs 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

34 
(*defining abstraction/representation functions for term list...*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

35 
Rep_Tlist_def "Rep_Tlist == Rep_map(Rep_term)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

36 
Abs_Tlist_def "Abs_Tlist == Abs_map(Abs_term)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

37 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

38 
(*defining the abstract constants*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

39 
App_def "App a ts == Abs_term(Leaf(a) $ Rep_Tlist(ts))" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

40 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

41 
(*list recursion*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

42 
Term_rec_def 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

43 
"Term_rec M d == wfrec (trancl pred_sexp) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

44 
(%g. Split(%x y. d x y (Abs_map g y))) M" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

45 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

46 
term_rec_def 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

47 
"term_rec t d == 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

48 
Term_rec (Rep_term t) (%x y r. d (inv Leaf x) (Abs_Tlist(y)) r)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

49 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

50 
rules 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

51 
(*faking a type definition for term...*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

52 
Rep_term "Rep_term(n): term(range(Leaf))" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

53 
Rep_term_inverse "Abs_term(Rep_term(t)) = t" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

54 
Abs_term_inverse "M: term(range(Leaf)) ==> Rep_term(Abs_term(M)) = M" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

55 
end 