author  berghofe 
Fri, 24 Jul 1998 13:39:47 +0200  
changeset 5191  8ceaa19f7717 
parent 5143  b94cd208f073 
child 5223  4cb05273f764 
permissions  rwrr 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

1 
(* Title: HOL/ex/LFilter 
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 1997 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 
The "filter" functional for coinductive lists 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

7 
defined by a combination of induction and coinduction 
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 

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

10 
open LFilter; 
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 
(*** findRel: basic laws ****) 
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 
val findRel_LConsE = 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

16 
findRel.mk_cases [LCons_LCons_eq] "(LCons x l, l'') : findRel p"; 
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 
AddSEs [findRel_LConsE]; 
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 

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

21 
Goal "(l,l'): findRel p ==> (l,l''): findRel p > l'' = l'"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

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

25 
qed_spec_mp "findRel_functional"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

26 

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

27 
Goal "(l,l'): findRel p ==> EX x l''. l' = LCons x l'' & p x"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

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

31 
qed_spec_mp "findRel_imp_LCons"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

32 

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

33 
Goal "(LNil,l): findRel p ==> R"; 
4090  34 
by (blast_tac (claset() addEs [findRel.elim]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

36 

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

37 
AddSEs [findRel_LNil]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

38 

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

39 

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

40 
(*** Properties of Domain (findRel p) ***) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

41 

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

42 
Goal "LCons x l : Domain(findRel p) = (p x  l : Domain(findRel p))"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

43 
by (case_tac "p x" 1); 
4090  44 
by (ALLGOALS (blast_tac (claset() addIs findRel.intrs))); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

46 

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

47 
Addsimps [LCons_Domain_findRel]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

48 

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

49 
val major::prems = 
5069  50 
Goal "[ l: Domain (findRel p); \ 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

51 
\ !!x l'. [ (l, LCons x l') : findRel p; p x ] ==> Q \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

52 
\ ] ==> Q"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

54 
by (forward_tac [findRel_imp_LCons] 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

55 
by (REPEAT (eresolve_tac [exE,conjE] 1)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

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

59 

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

60 
val prems = goal thy 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

61 
"[ !!x. p x ==> q x ] ==> Domain (findRel p) <= Domain (findRel q)"; 
3718  62 
by (Clarify_tac 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

63 
by (etac findRel.induct 1); 
4090  64 
by (blast_tac (claset() addIs (findRel.intrs@prems)) 1); 
65 
by (blast_tac (claset() addIs findRel.intrs) 1); 

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

66 
qed "Domain_findRel_mono"; 
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 

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

69 
(*** find: basic equations ***) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

70 

5069  71 
Goalw [find_def] "find p LNil = LNil"; 
4535  72 
by (Blast_tac 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

73 
qed "find_LNil"; 
4521  74 
Addsimps [find_LNil]; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

75 

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

76 
Goalw [find_def] "(l,l') : findRel p ==> find p l = l'"; 
4535  77 
by (blast_tac (claset() addDs [findRel_functional]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

78 
qed "findRel_imp_find"; 
4521  79 
Addsimps [findRel_imp_find]; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

80 

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

81 
Goal "p x ==> find p (LCons x l) = LCons x l"; 
4090  82 
by (blast_tac (claset() addIs (findRel_imp_find::findRel.intrs)) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

83 
qed "find_LCons_found"; 
4521  84 
Addsimps [find_LCons_found]; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

85 

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

86 
Goalw [find_def] "l ~: Domain(findRel p) ==> find p l = LNil"; 
4535  87 
by (Blast_tac 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

89 
Addsimps [diverge_find_LNil]; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

90 

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

91 
Goal "~ (p x) ==> find p (LCons x l) = find p l"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

92 
by (case_tac "LCons x l : Domain(findRel p)" 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

93 
by (Asm_full_simp_tac 2); 
3718  94 
by (Clarify_tac 1); 
4521  95 
by (Asm_simp_tac 1); 
4090  96 
by (blast_tac (claset() addIs (findRel_imp_find::findRel.intrs)) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

97 
qed "find_LCons_seek"; 
4521  98 
Addsimps [find_LCons_seek]; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

99 

5069  100 
Goal "find p (LCons x l) = (if p x then LCons x l else find p l)"; 
4686  101 
by (Asm_simp_tac 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

102 
qed "find_LCons"; 
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 

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

105 

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

106 
(*** lfilter: basic equations ***) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

107 

5069  108 
Goal "lfilter p LNil = LNil"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

109 
by (rtac (lfilter_def RS def_llist_corec RS trans) 1); 
4521  110 
by (Simp_tac 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

111 
qed "lfilter_LNil"; 
4521  112 
Addsimps [lfilter_LNil]; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

113 

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

114 
Goal "l ~: Domain(findRel p) ==> lfilter p l = LNil"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

115 
by (rtac (lfilter_def RS def_llist_corec RS trans) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

118 

4521  119 
Addsimps [diverge_lfilter_LNil]; 
120 

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

121 

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

122 
Goal "p x ==> lfilter p (LCons x l) = LCons x (lfilter p l)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

123 
by (rtac (lfilter_def RS def_llist_corec RS trans) 1); 
4521  124 
by (Asm_simp_tac 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

125 
qed "lfilter_LCons_found"; 
4521  126 
(*This rewrite and lfilter_LCons_seek are NOT added because lfilter_LCons 
127 
subsumes both*) 

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

128 

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

129 

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

130 
Goal "(l, LCons x l') : findRel p \ 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

131 
\ ==> lfilter p l = LCons x (lfilter p l')"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

132 
by (rtac (lfilter_def RS def_llist_corec RS trans) 1); 
4521  133 
by (Asm_simp_tac 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

135 

4521  136 
Addsimps [findRel_imp_lfilter]; 
137 

138 

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

139 
Goal "~ (p x) ==> lfilter p (LCons x l) = lfilter p l"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

140 
by (rtac (lfilter_def RS def_llist_corec RS trans) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

141 
by (case_tac "LCons x l : Domain(findRel p)" 1); 
4521  142 
by (Asm_full_simp_tac 2); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

143 
by (etac Domain_findRelE 1); 
4090  144 
by (safe_tac (claset() delrules [conjI])); 
4521  145 
by (Asm_full_simp_tac 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

147 

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

148 

5069  149 
Goal "lfilter p (LCons x l) = \ 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

150 
\ (if p x then LCons x (lfilter p l) else lfilter p l)"; 
4686  151 
by (asm_simp_tac (simpset() addsimps [lfilter_LCons_found, lfilter_LCons_seek]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

153 

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

154 
AddSIs [llistD_Fun_LNil_I, llistD_Fun_LCons_I]; 
4521  155 
Addsimps [lfilter_LCons]; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

156 

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

157 

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

158 
Goal "lfilter p l = LNil ==> l ~: Domain(findRel p)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

161 
by (etac rev_mp 1); 
4521  162 
by (Asm_simp_tac 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

163 
qed "lfilter_eq_LNil"; 
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 

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

166 
Goal "lfilter p l = LCons x l' > \ 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

167 
\ (EX l''. l' = lfilter p l'' & (l, LCons x l'') : findRel p)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

168 
by (stac (lfilter_def RS def_llist_corec) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

169 
by (case_tac "l : Domain(findRel p)" 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

171 
by (Asm_simp_tac 2); 
4521  172 
by (Asm_simp_tac 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

174 
qed_spec_mp "lfilter_eq_LCons"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

175 

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

176 

5069  177 
Goal "lfilter p l = LNil  \ 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

178 
\ (EX y l'. lfilter p l = LCons y (lfilter p l') & p y)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

179 
by (case_tac "l : Domain(findRel p)" 1); 
4521  180 
by (Asm_simp_tac 2); 
4090  181 
by (blast_tac (claset() addSEs [Domain_findRelE] 
4521  182 
addIs [findRel_imp_lfilter]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

184 

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

185 

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

186 
(*** lfilter: simple facts by coinduction ***) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

187 

5069  188 
Goal "lfilter (%x. True) l = l"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

189 
by (res_inst_tac [("l","l")] llist_fun_equalityI 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

192 

5069  193 
Goal "lfilter p (lfilter p l) = lfilter p l"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

194 
by (res_inst_tac [("l","l")] llist_fun_equalityI 1); 
4686  195 
by (ALLGOALS Simp_tac); 
3724  196 
by Safe_tac; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

197 
(*Cases: p x is true or false*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

198 
by (rtac (lfilter_cases RS disjE) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

199 
by (etac ssubst 1); 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4090
diff
changeset

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

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

202 

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

203 

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

204 
(*** Numerous lemmas required to prove lfilter_conj: 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

205 
lfilter p (lfilter q l) = lfilter (%x. p x & q x) l 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

207 

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

208 
Goal "(l,l') : findRel q \ 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

209 
\ ==> l' = LCons x l'' > p x > (l,l') : findRel (%x. p x & q x)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

210 
by (etac findRel.induct 1); 
4090  211 
by (blast_tac (claset() addIs findRel.intrs) 1); 
212 
by (blast_tac (claset() addIs findRel.intrs) 1); 

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

213 
qed_spec_mp "findRel_conj_lemma"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

214 

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

215 
val findRel_conj = refl RSN (2, findRel_conj_lemma); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

216 

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

217 
Goal "(l,l'') : findRel (%x. p x & q x) \ 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

218 
\ ==> (l, LCons x l') : findRel q > ~ p x \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

219 
\ > l' : Domain (findRel (%x. p x & q x))"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

220 
by (etac findRel.induct 1); 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4090
diff
changeset

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

222 
qed_spec_mp "findRel_not_conj_Domain"; 
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 

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

225 
Goal "(l,lxx) : findRel q ==> \ 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

226 
\ lxx = LCons x lx > (lx,lz) : findRel(%x. p x & q x) > ~ p x \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

227 
\ > (l,lz) : findRel (%x. p x & q x)"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

228 
by (etac findRel.induct 1); 
4090  229 
by (ALLGOALS (blast_tac (claset() addIs findRel.intrs))); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

230 
qed_spec_mp "findRel_conj2"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

231 

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

232 

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

233 
Goal "(lx,ly) : findRel p \ 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

234 
\ ==> ALL l. lx = lfilter q l \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

235 
\ > l : Domain (findRel(%x. p x & q x))"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

236 
by (etac findRel.induct 1); 
4090  237 
by (blast_tac (claset() addSDs [sym RS lfilter_eq_LCons] 
4521  238 
addIs [findRel_conj]) 1); 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4090
diff
changeset

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

240 
by (dtac (sym RS lfilter_eq_LCons) 1); 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4090
diff
changeset

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

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

243 
by (dtac (refl RS rev_mp) 1); 
4090  244 
by (blast_tac (claset() addIs [findRel_conj2]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

245 
qed_spec_mp "findRel_lfilter_Domain_conj"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

246 

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

247 

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

248 
Goal "(l,l'') : findRel(%x. p x & q x) \ 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

249 
\ ==> l'' = LCons y l' > \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

250 
\ (lfilter q l, LCons y (lfilter q l')) : findRel p"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

251 
by (etac findRel.induct 1); 
4686  252 
by (ALLGOALS Asm_simp_tac); 
4090  253 
by (ALLGOALS (blast_tac (claset() addIs findRel.intrs))); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

254 
qed_spec_mp "findRel_conj_lfilter"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

255 

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

256 

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

257 

5069  258 
Goal "(lfilter p (lfilter q l), lfilter (%x. p x & q x) l) \ 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

260 
\ (%u. (lfilter p (lfilter q u), \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

261 
\ lfilter (%x. p x & q x) u)))"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

262 
by (case_tac "l : Domain(findRel q)" 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

263 
by (subgoal_tac "l ~: Domain (findRel (%x. p x & q x))" 2); 
4090  264 
by (blast_tac (claset() addIs [impOfSubs Domain_findRel_mono]) 3); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

265 
(*There are no qs in l: both lists are LNil*) 
4521  266 
by (Asm_simp_tac 2); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

268 
(*case q x*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

269 
by (case_tac "p x" 1); 
4521  270 
by (asm_simp_tac (simpset() addsimps [findRel_conj RS findRel_imp_lfilter]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

271 
(*case q x and ~(p x) *) 
4521  272 
by (Asm_simp_tac 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

273 
by (case_tac "l' : Domain (findRel (%x. p x & q x))" 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

274 
(*subcase: there is no p&q in l' and therefore none in l*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

275 
by (subgoal_tac "l ~: Domain (findRel (%x. p x & q x))" 2); 
4090  276 
by (blast_tac (claset() addIs [findRel_not_conj_Domain]) 3); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

277 
by (subgoal_tac "lfilter q l' ~: Domain(findRel p)" 2); 
4090  278 
by (blast_tac (claset() addIs [findRel_lfilter_Domain_conj]) 3); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

279 
(* ...and therefore too, no p in lfilter q l'. Both results are Lnil*) 
4521  280 
by (Asm_simp_tac 2); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

281 
(*subcase: there is a p&q in l' and therefore also one in l*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

283 
by (subgoal_tac "(l, LCons xa l'a) : findRel(%x. p x & q x)" 1); 
4090  284 
by (blast_tac (claset() addIs [findRel_conj2]) 2); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

285 
by (subgoal_tac "(lfilter q l', LCons xa (lfilter q l'a)) : findRel p" 1); 
4090  286 
by (blast_tac (claset() addIs [findRel_conj_lfilter]) 2); 
4521  287 
by (Asm_simp_tac 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

288 
val lemma = result(); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

289 

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

290 

5069  291 
Goal "lfilter p (lfilter q l) = lfilter (%x. p x & q x) l"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

292 
by (res_inst_tac [("l","l")] llist_fun_equalityI 1); 
4686  293 
by (ALLGOALS Simp_tac); 
4090  294 
by (blast_tac (claset() addIs [lemma, impOfSubs llistD_Fun_mono]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

296 

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

297 

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

298 
(*** Numerous lemmas required to prove ??: 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

299 
lfilter p (lmap f l) = lmap f (lfilter (%x. p(f x)) l) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

301 

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

302 
Goal "(l,l') : findRel(%x. p (f x)) ==> lmap f l : Domain(findRel p)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

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

306 

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

307 

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

308 
Goal "lmap f l = LCons x l' > \ 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

309 
\ (EX y l''. x = f y & l' = lmap f l'' & l = LCons y l'')"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

310 
by (stac (lmap_def RS def_llist_corec) 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

311 
by (res_inst_tac [("l", "l")] llistE 1); 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4090
diff
changeset

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

313 
qed_spec_mp "lmap_eq_LCons"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

314 

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

315 

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

316 
Goal "(lx,ly) : findRel p ==> \ 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

317 
\ ALL l. lmap f l = lx > ly = LCons x l' > \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

318 
\ (EX y l''. x = f y & l' = lmap f l'' & \ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

319 
\ (l, LCons y l'') : findRel(%x. p(f x)))"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

321 
by (ALLGOALS Asm_simp_tac); 
4090  322 
by (safe_tac (claset() addSDs [lmap_eq_LCons])); 
323 
by (blast_tac (claset() addIs findRel.intrs) 1); 

324 
by (blast_tac (claset() addIs findRel.intrs) 1); 

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

325 
qed_spec_mp "lmap_LCons_findRel_lemma"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

326 

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

327 
val lmap_LCons_findRel = refl RSN (2, refl RSN (2, lmap_LCons_findRel_lemma)); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

328 

5069  329 
Goal "lfilter p (lmap f l) = lmap f (lfilter (p o f) l)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

330 
by (res_inst_tac [("l","l")] llist_fun_equalityI 1); 
4686  331 
by (ALLGOALS Simp_tac); 
3724  332 
by Safe_tac; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

333 
by (case_tac "lmap f l : Domain (findRel p)" 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

334 
by (subgoal_tac "l ~: Domain (findRel(%x. p (f x)))" 2); 
4090  335 
by (blast_tac (claset() addIs [findRel_lmap_Domain]) 3); 
4521  336 
by (Asm_simp_tac 2); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

338 
by (forward_tac [lmap_LCons_findRel] 1); 
3718  339 
by (Clarify_tac 1); 
4521  340 
by (Asm_simp_tac 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

341 
qed "lfilter_lmap"; 