author  berghofe 
Fri, 24 Jul 1998 13:39:47 +0200  
changeset 5191  8ceaa19f7717 
parent 3842  b55686a7b22c 
child 5977  9f0c8869cf71 
permissions  rwrr 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

1 
(* Title: HOL/ex/SList.thy 
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 1993 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 
Definition of type 'a list (strict lists) by a least fixed point 
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 
We use list(A) == lfp(%Z. {NUMB(0)} <+> A <*> Z) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

9 
and not list == lfp(%Z. {NUMB(0)} <+> range(Leaf) <*> Z) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

10 
so that list can serve as a "functor" for defining other recursive types 
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 

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

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

14 

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

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

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

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

20 

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

21 

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

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

23 

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

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

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

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

27 
NIL :: 'a item 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

29 
Nil :: 'a list 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

30 
"#" :: ['a, 'a list] => 'a list (infixr 65) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

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

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

35 
Rep_map :: ('b => 'a item) => ('b list => 'a item) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

36 
Abs_map :: ('a item => 'b) => 'a item => 'b list 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

37 
null :: 'a list => bool 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

38 
hd :: 'a list => 'a 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

39 
tl,ttl :: 'a list => 'a list 
3649
e530286d4847
Renamed set_of_list to set, and relevant theorems too
paulson
parents:
3320
diff
changeset

40 
set :: ('a list => 'a set) 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

41 
mem :: ['a, 'a list] => bool (infixl 55) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

42 
map :: ('a=>'b) => ('a list => 'b list) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

43 
"@" :: ['a list, 'a list] => 'a list (infixr 65) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

44 
filter :: ['a => bool, 'a list] => 'a list 
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 
(* list Enumeration *) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

47 

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

48 
"[]" :: 'a list ("[]") 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

49 
"@list" :: args => 'a list ("[(_)]") 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

50 

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

51 
(* Special syntax for filter *) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

52 
"@filter" :: [idt, 'a list, bool] => 'a list ("(1[_:_ ./ _])") 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

53 

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

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

55 
"[x, xs]" == "x#[xs]" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

56 
"[x]" == "x#[]" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

57 
"[]" == "Nil" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

58 

3842  59 
"case xs of Nil => a  y#ys => b" == "list_case a (%y ys. b) xs" 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

60 

3842  61 
"[x:xs . P]" == "filter (%x. P) xs" 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

62 

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

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

64 
(* Defining the Concrete Constructors *) 
5191
8ceaa19f7717
Renamed '$' to 'Scons' because of clashes with constants of the same
berghofe
parents:
3842
diff
changeset

65 
NIL_def "NIL == In0 (Numb 0)" 
8ceaa19f7717
Renamed '$' to 'Scons' because of clashes with constants of the same
berghofe
parents:
3842
diff
changeset

66 
CONS_def "CONS M N == In1 (Scons M N)" 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

67 

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

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

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

70 
NIL_I "NIL: list(A)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

71 
CONS_I "[ a: A; M: list(A) ] ==> CONS a M : list(A)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

72 

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

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

74 
(* Faking a Type Definition ... *) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

75 
Rep_list "Rep_list(xs): list(range(Leaf))" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

76 
Rep_list_inverse "Abs_list(Rep_list(xs)) = xs" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

77 
Abs_list_inverse "M: list(range(Leaf)) ==> Rep_list(Abs_list(M)) = M" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

78 

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

79 

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

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

81 
(* Defining the Abstract Constructors *) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

82 
Nil_def "Nil == Abs_list(NIL)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

83 
Cons_def "x#xs == Abs_list(CONS (Leaf x) (Rep_list xs))" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

84 

3842  85 
List_case_def "List_case c d == Case (%x. c) (Split d)" 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

86 

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

87 
(* list Recursion  the trancl is Essential; see list.ML *) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

88 

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

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

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

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

92 

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

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

94 
"list_rec l c d == 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

95 
List_rec (Rep_list l) c (%x y r. d (inv Leaf x) (Abs_list y) r)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

96 

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

97 
(* Generalized Map Functionals *) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

98 

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

99 
Rep_map_def "Rep_map f xs == list_rec xs NIL (%x l r. CONS (f x) r)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

100 
Abs_map_def "Abs_map g M == List_rec M Nil (%N L r. g(N)#r)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

101 

3842  102 
null_def "null(xs) == list_rec xs True (%x xs r. False)" 
103 
hd_def "hd(xs) == list_rec xs arbitrary (%x xs r. x)" 

104 
tl_def "tl(xs) == list_rec xs arbitrary (%x xs r. xs)" 

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

105 
(* a total version of tl: *) 
3842  106 
ttl_def "ttl(xs) == list_rec xs [] (%x xs r. xs)" 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

107 

3649
e530286d4847
Renamed set_of_list to set, and relevant theorems too
paulson
parents:
3320
diff
changeset

108 
set_def "set xs == list_rec xs {} (%x l r. insert x r)" 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

109 

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

110 
mem_def "x mem xs == 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

111 
list_rec xs False (%y ys r. if y=x then True else r)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

112 
map_def "map f xs == list_rec xs [] (%x l r. f(x)#r)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

113 
append_def "xs@ys == list_rec xs ys (%x l r. x#r)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

114 
filter_def "filter P xs == 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

115 
list_rec xs [] (%x xs r. if P(x) then x#r else r)" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

116 

3842  117 
list_case_def "list_case a f xs == list_rec xs a (%x xs r. f x xs)" 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

118 

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

119 
end 