author  paulson 
Wed, 15 Jul 1998 10:15:13 +0200  
changeset 5143  b94cd208f073 
parent 5069  3ea049f7979d 
child 5148  74919e8f221c 
permissions  rwrr 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

1 
(* Title: HOL/ex/SList.ML 
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 
4521  4 
Copyright 1998 University of Cambridge 
3120
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 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 

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

9 
open SList; 
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 
val list_con_defs = [NIL_def, CONS_def]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

12 

5069  13 
Goal "list(A) = {Numb(0)} <+> (A <*> list(A))"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

14 
let val rew = rewrite_rule list_con_defs in 
4089  15 
by (fast_tac (claset() addSIs (equalityI :: map rew list.intrs) 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

16 
addEs [rew list.elim]) 1) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

18 
qed "list_unfold"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

19 

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

20 
(*This justifies using list in other recursive type definitions*) 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

21 
Goalw list.defs "A<=B ==> list(A) <= list(B)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

22 
by (rtac lfp_mono 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

23 
by (REPEAT (ares_tac basic_monos 1)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

24 
qed "list_mono"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

25 

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

26 
(*Type checking  list creates wellfounded sets*) 
5069  27 
Goalw (list_con_defs @ list.defs) "list(sexp) <= sexp"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

28 
by (rtac lfp_lowerbound 1); 
4089  29 
by (fast_tac (claset() addIs sexp.intrs@[sexp_In0I,sexp_In1I]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

30 
qed "list_sexp"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

31 

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

32 
(* A <= sexp ==> list(A) <= sexp *) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

33 
bind_thm ("list_subset_sexp", ([list_mono, list_sexp] MRS subset_trans)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

34 

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

35 
(*Induction for the type 'a list *) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

36 
val prems = goalw SList.thy [Nil_def,Cons_def] 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

37 
"[ P(Nil); \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

38 
\ !!x xs. P(xs) ==> P(x # xs) ] ==> P(l)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

39 
by (rtac (Rep_list_inverse RS subst) 1); (*types force good instantiation*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

40 
by (rtac (Rep_list RS list.induct) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

41 
by (REPEAT (ares_tac prems 1 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

42 
ORELSE eresolve_tac [rangeE, ssubst, Abs_list_inverse RS subst] 1)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

43 
qed "list_induct2"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

44 

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

45 
(*Perform induction on xs. *) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

46 
fun list_ind_tac a M = 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

47 
EVERY [res_inst_tac [("l",a)] list_induct2 M, 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

48 
rename_last_tac a ["1"] (M+1)]; 
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 
(*** Isomorphisms ***) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

51 

5069  52 
Goal "inj(Rep_list)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

53 
by (rtac inj_inverseI 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

54 
by (rtac Rep_list_inverse 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

55 
qed "inj_Rep_list"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

56 

5069  57 
Goal "inj_on Abs_list (list(range Leaf))"; 
4831  58 
by (rtac inj_on_inverseI 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

59 
by (etac Abs_list_inverse 1); 
4831  60 
qed "inj_on_Abs_list"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

61 

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

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

63 

5069  64 
Goalw list_con_defs "CONS M N ~= NIL"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

65 
by (rtac In1_not_In0 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

66 
qed "CONS_not_NIL"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

67 
bind_thm ("NIL_not_CONS", (CONS_not_NIL RS not_sym)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

68 

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

69 
bind_thm ("CONS_neq_NIL", (CONS_not_NIL RS notE)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

70 
val NIL_neq_CONS = sym RS CONS_neq_NIL; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

71 

5069  72 
Goalw [Nil_def,Cons_def] "x # xs ~= Nil"; 
4831  73 
by (rtac (CONS_not_NIL RS (inj_on_Abs_list RS inj_on_contraD)) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

74 
by (REPEAT (resolve_tac (list.intrs @ [rangeI, Rep_list]) 1)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

75 
qed "Cons_not_Nil"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

76 

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

77 
bind_thm ("Nil_not_Cons", Cons_not_Nil RS not_sym); 
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 
(** Injectiveness of CONS and Cons **) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

80 

5069  81 
Goalw [CONS_def] "(CONS K M=CONS L N) = (K=L & M=N)"; 
4089  82 
by (fast_tac (claset() addSEs [Scons_inject, make_elim In1_inject]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

83 
qed "CONS_CONS_eq"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

84 

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

85 
(*For reasoning about abstract list constructors*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

86 
AddIs ([Rep_list] @ list.intrs); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

87 

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

88 
AddIffs [CONS_not_NIL, NIL_not_CONS, CONS_CONS_eq]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

89 

4831  90 
AddSDs [inj_on_Abs_list RS inj_onD, 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

91 
inj_Rep_list RS injD, Leaf_inject]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

92 

5069  93 
Goalw [Cons_def] "(x#xs=y#ys) = (x=y & xs=ys)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

94 
by (Fast_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

95 
qed "Cons_Cons_eq"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

96 
bind_thm ("Cons_inject2", (Cons_Cons_eq RS iffD1 RS conjE)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

97 

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

98 
val [major] = goal SList.thy "CONS M N: list(A) ==> M: A & N: list(A)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

99 
by (rtac (major RS setup_induction) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

100 
by (etac list.induct 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

101 
by (ALLGOALS (Fast_tac)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

102 
qed "CONS_D"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

103 

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

104 
val prems = goalw SList.thy [CONS_def,In1_def] 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

105 
"CONS M N: sexp ==> M: sexp & N: sexp"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

106 
by (cut_facts_tac prems 1); 
4089  107 
by (fast_tac (claset() addSDs [Scons_D]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

108 
qed "sexp_CONS_D"; 
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 

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

111 
(*Reasoning about constructors and their freeness*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

112 
Addsimps list.intrs; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

113 

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

114 
AddIffs [Cons_not_Nil, Nil_not_Cons, Cons_Cons_eq]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

115 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

116 
Goal "N: list(A) ==> !M. N ~= CONS M N"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

117 
by (etac list.induct 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

118 
by (ALLGOALS Asm_simp_tac); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

119 
qed "not_CONS_self"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

120 

5069  121 
Goal "!x. l ~= x#l"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

122 
by (list_ind_tac "l" 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

123 
by (ALLGOALS Asm_simp_tac); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

124 
qed "not_Cons_self2"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

125 

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

126 

5069  127 
Goal "(xs ~= []) = (? y ys. xs = y#ys)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

128 
by (list_ind_tac "xs" 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

129 
by (Simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

130 
by (Asm_simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

131 
by (REPEAT(resolve_tac [exI,refl,conjI] 1)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

132 
qed "neq_Nil_conv2"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

133 

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

134 
(** Conversion rules for List_case: case analysis operator **) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

135 

5069  136 
Goalw [List_case_def,NIL_def] "List_case c h NIL = c"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

137 
by (rtac Case_In0 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

138 
qed "List_case_NIL"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

139 

5069  140 
Goalw [List_case_def,CONS_def] "List_case c h (CONS M N) = h M N"; 
4521  141 
by (Simp_tac 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

142 
qed "List_case_CONS"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

143 

4521  144 
Addsimps [List_case_NIL, List_case_CONS]; 
145 

146 

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

147 
(*** List_rec  by wf recursion on pred_sexp ***) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

148 

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

149 
(* The trancl(pred_sexp) is essential because pred_sexp_CONS_I1,2 would not 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

150 
hold if pred_sexp^+ were changed to pred_sexp. *) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

151 

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

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

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

155 
by (simp_tac (HOL_ss addsimps [List_rec_def]) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

156 
val List_rec_unfold = standard 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

157 
((wf_pred_sexp RS wf_trancl) RS ((result() RS eq_reflection) RS def_wfrec)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

158 

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

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

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

161 
* val List_rec_unfold = [List_rec_def,wf_pred_sexp RS wf_trancl] MRS def_wfrec 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

162 
* > standard; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

164 

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

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

166 

5069  167 
Goalw [CONS_def,In1_def] 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

168 
"!!M. [ M: sexp; N: sexp ] ==> (M, CONS M N) : pred_sexp^+"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

169 
by (Asm_simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

170 
qed "pred_sexp_CONS_I1"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

171 

5069  172 
Goalw [CONS_def,In1_def] 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

173 
"!!M. [ M: sexp; N: sexp ] ==> (N, CONS M N) : pred_sexp^+"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

174 
by (Asm_simp_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

175 
qed "pred_sexp_CONS_I2"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

176 

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

177 
val [prem] = goal SList.thy 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

178 
"(CONS M1 M2, N) : pred_sexp^+ ==> \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

179 
\ (M1,N) : pred_sexp^+ & (M2,N) : pred_sexp^+"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

180 
by (rtac (prem RS (pred_sexp_subset_Sigma RS trancl_subset_Sigma RS 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

181 
subsetD RS SigmaE2)) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

182 
by (etac (sexp_CONS_D RS conjE) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

183 
by (REPEAT (ares_tac [conjI, pred_sexp_CONS_I1, pred_sexp_CONS_I2, 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

184 
prem RSN (2, trans_trancl RS transD)] 1)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

185 
qed "pred_sexp_CONS_D"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

186 

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

187 
(** Conversion rules for List_rec **) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

188 

5069  189 
Goal "List_rec NIL c h = c"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

190 
by (rtac (List_rec_unfold RS trans) 1); 
4521  191 
by (Simp_tac 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

192 
qed "List_rec_NIL"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

193 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

194 
Goal "[ M: sexp; N: sexp ] ==> \ 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

195 
\ List_rec (CONS M N) c h = h M N (List_rec N c h)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

196 
by (rtac (List_rec_unfold RS trans) 1); 
4521  197 
by (asm_simp_tac (simpset() addsimps [pred_sexp_CONS_I2]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

198 
qed "List_rec_CONS"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

199 

4521  200 
Addsimps [List_rec_NIL, List_rec_CONS]; 
201 

202 

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

203 
(*** list_rec  by List_rec ***) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

204 

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

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

206 
[range_Leaf_subset_sexp RS list_subset_sexp, Rep_list] MRS subsetD; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

207 

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

208 
local 
4521  209 
val list_rec_simps = [Abs_list_inverse, Rep_list_inverse, 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

210 
Rep_list, rangeI, inj_Leaf, inv_f_f, 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

211 
sexp.LeafI, Rep_list_in_sexp] 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

213 
val list_rec_Nil = prove_goalw SList.thy [list_rec_def, Nil_def] 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

214 
"list_rec Nil c h = c" 
4089  215 
(fn _=> [simp_tac (simpset() addsimps list_rec_simps) 1]); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

216 

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

217 
val list_rec_Cons = prove_goalw SList.thy [list_rec_def, Cons_def] 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

218 
"list_rec (a#l) c h = h a l (list_rec l c h)" 
4089  219 
(fn _=> [simp_tac (simpset() addsimps list_rec_simps) 1]); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

221 

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

222 
Addsimps [List_rec_NIL, List_rec_CONS, list_rec_Nil, list_rec_Cons]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

223 

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

224 

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

225 
(*Type checking. Useful?*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

226 
val major::A_subset_sexp::prems = goal SList.thy 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

227 
"[ M: list(A); \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

228 
\ A<=sexp; \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

229 
\ c: C(NIL); \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

230 
\ !!x y r. [ x: A; y: list(A); r: C(y) ] ==> h x y r: C(CONS x y) \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

231 
\ ] ==> List_rec M c h : C(M :: 'a item)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

232 
val sexp_ListA_I = A_subset_sexp RS list_subset_sexp RS subsetD; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

233 
val sexp_A_I = A_subset_sexp RS subsetD; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

234 
by (rtac (major RS list.induct) 1); 
4089  235 
by (ALLGOALS(asm_simp_tac (simpset() addsimps ([sexp_A_I,sexp_ListA_I]@prems)))); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

236 
qed "List_rec_type"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

237 

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

238 
(** Generalized map functionals **) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

239 

5069  240 
Goalw [Rep_map_def] "Rep_map f Nil = NIL"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

241 
by (rtac list_rec_Nil 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

242 
qed "Rep_map_Nil"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

243 

5069  244 
Goalw [Rep_map_def] 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

245 
"Rep_map f (x#xs) = CONS (f x) (Rep_map f xs)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

246 
by (rtac list_rec_Cons 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

247 
qed "Rep_map_Cons"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

248 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

249 
val prems = Goalw [Rep_map_def] "(!!x. f(x): A) ==> Rep_map f xs: list(A)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

250 
by (rtac list_induct2 1); 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

251 
by (ALLGOALS (asm_simp_tac (simpset() addsimps prems))); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

252 
qed "Rep_map_type"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

253 

5069  254 
Goalw [Abs_map_def] "Abs_map g NIL = Nil"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

255 
by (rtac List_rec_NIL 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

256 
qed "Abs_map_NIL"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

257 

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

258 
val prems = goalw SList.thy [Abs_map_def] 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

259 
"[ M: sexp; N: sexp ] ==> \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

260 
\ Abs_map g (CONS M N) = g(M) # Abs_map g N"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

261 
by (REPEAT (resolve_tac (List_rec_CONS::prems) 1)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

262 
qed "Abs_map_CONS"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

263 

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

264 
(*These 2 rules ease the use of primitive recursion. NOTE USE OF == *) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

265 
val [rew] = goal SList.thy 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

266 
"[ !!xs. f(xs) == list_rec xs c h ] ==> f([]) = c"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

267 
by (rewtac rew); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

268 
by (rtac list_rec_Nil 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

269 
qed "def_list_rec_Nil"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

270 

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

271 
val [rew] = goal SList.thy 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

272 
"[ !!xs. f(xs) == list_rec xs c h ] ==> f(x#xs) = h x xs (f xs)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

273 
by (rewtac rew); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

274 
by (rtac list_rec_Cons 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

275 
qed "def_list_rec_Cons"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

276 

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

277 
fun list_recs def = 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

278 
[standard (def RS def_list_rec_Nil), 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

279 
standard (def RS def_list_rec_Cons)]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

280 

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

281 
(*** Unfolding the basic combinators ***) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

282 

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

283 
val [null_Nil, null_Cons] = list_recs null_def; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

284 
val [_, hd_Cons] = list_recs hd_def; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

285 
val [_, tl_Cons] = list_recs tl_def; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

286 
val [ttl_Nil, ttl_Cons] = list_recs ttl_def; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

287 
val [append_Nil3, append_Cons] = list_recs append_def; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

288 
val [mem_Nil, mem_Cons] = list_recs mem_def; 
3649
e530286d4847
Renamed set_of_list to set, and relevant theorems too
paulson
parents:
3120
diff
changeset

289 
val [set_Nil, set_Cons] = list_recs set_def; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

290 
val [map_Nil, map_Cons] = list_recs map_def; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

291 
val [list_case_Nil, list_case_Cons] = list_recs list_case_def; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

292 
val [filter_Nil, filter_Cons] = list_recs filter_def; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

293 

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

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

295 
[null_Nil, ttl_Nil, 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

298 
append_Nil3, append_Cons, 
3649
e530286d4847
Renamed set_of_list to set, and relevant theorems too
paulson
parents:
3120
diff
changeset

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

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

301 
filter_Nil, filter_Cons]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

302 

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

303 

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

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

305 

5069  306 
Goal "(xs@ys)@zs = xs@(ys@zs)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

307 
by (list_ind_tac "xs" 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

308 
by (ALLGOALS Asm_simp_tac); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

309 
qed "append_assoc2"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

310 

5069  311 
Goal "xs @ [] = xs"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

312 
by (list_ind_tac "xs" 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

313 
by (ALLGOALS Asm_simp_tac); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

314 
qed "append_Nil4"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

315 

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

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

317 

5069  318 
Goal "x mem (xs@ys) = (x mem xs  x mem ys)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

319 
by (list_ind_tac "xs" 1); 
4686  320 
by (ALLGOALS Asm_simp_tac); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

321 
qed "mem_append2"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

322 

5069  323 
Goal "x mem [x:xs. P(x)] = (x mem xs & P(x))"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

324 
by (list_ind_tac "xs" 1); 
4686  325 
by (ALLGOALS Asm_simp_tac); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

326 
qed "mem_filter2"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

327 

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

328 

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

329 
(** The functional "map" **) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

330 

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

331 
Addsimps [Rep_map_Nil, Rep_map_Cons, Abs_map_NIL, Abs_map_CONS]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

332 

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

333 
val [major,A_subset_sexp,minor] = goal SList.thy 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

334 
"[ M: list(A); A<=sexp; !!z. z: A ==> f(g(z)) = z ] \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

335 
\ ==> Rep_map f (Abs_map g M) = M"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

336 
by (rtac (major RS list.induct) 1); 
4089  337 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [sexp_A_I,sexp_ListA_I,minor]))); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

338 
qed "Abs_map_inverse"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

339 

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

340 
(*Rep_map_inverse is obtained via Abs_Rep_map and map_ident*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

341 

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

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

343 

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

345 
"P(list_case a f xs) = ((xs=[] > P(a)) & \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

346 
\ (!y ys. xs=y#ys > P(f y ys)))"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

347 
by (list_ind_tac "xs" 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

348 
by (ALLGOALS Asm_simp_tac); 
4831  349 
qed "split_list_case2"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

350 

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

351 

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

352 
(** Additional mapping lemmas **) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

353 

5069  354 
Goal "map (%x. x) xs = xs"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

355 
by (list_ind_tac "xs" 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

356 
by (ALLGOALS Asm_simp_tac); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

357 
qed "map_ident2"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

358 

5069  359 
Goal "map f (xs@ys) = map f xs @ map f ys"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

360 
by (list_ind_tac "xs" 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

361 
by (ALLGOALS Asm_simp_tac); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

362 
qed "map_append2"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

363 

5069  364 
Goalw [o_def] "map (f o g) xs = map f (map g xs)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

365 
by (list_ind_tac "xs" 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

366 
by (ALLGOALS Asm_simp_tac); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

367 
qed "map_compose2"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

368 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

369 
val prems = 
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

370 
Goal "(!!x. f(x): sexp) ==> \ 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

371 
\ Abs_map g (Rep_map f xs) = map (%t. g(f(t))) xs"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

372 
by (list_ind_tac "xs" 1); 
4521  373 
by (ALLGOALS (asm_simp_tac(simpset() addsimps 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

374 
(prems@[Rep_map_type, list_sexp RS subsetD])))); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

375 
qed "Abs_Rep_map"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

376 

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

377 
Addsimps [append_Nil4, map_ident2]; 