author | paulson |
Tue, 19 Jan 1999 11:18:11 +0100 | |
changeset 6141 | a6922171b396 |
parent 5618 | 721671c68324 |
child 7499 | 23e090051cb8 |
permissions | -rw-r--r-- |
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 |
(*** findRel: basic laws ****) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
11 |
|
6141 | 12 |
val findRel_LConsE = findRel.mk_cases "(LCons x l, l'') : findRel p"; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
13 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
14 |
AddSEs [findRel_LConsE]; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
15 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
16 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
17 |
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
|
18 |
by (etac findRel.induct 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
19 |
by (Blast_tac 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
20 |
by (Blast_tac 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
21 |
qed_spec_mp "findRel_functional"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
22 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
23 |
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
|
24 |
by (etac findRel.induct 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
25 |
by (Blast_tac 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
26 |
by (Blast_tac 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
27 |
qed_spec_mp "findRel_imp_LCons"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
28 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
29 |
Goal "(LNil,l): findRel p ==> R"; |
4090 | 30 |
by (blast_tac (claset() addEs [findRel.elim]) 1); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
31 |
qed "findRel_LNil"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
32 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
33 |
AddSEs [findRel_LNil]; |
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 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
36 |
(*** Properties of Domain (findRel p) ***) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
37 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
38 |
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
|
39 |
by (case_tac "p x" 1); |
4090 | 40 |
by (ALLGOALS (blast_tac (claset() addIs findRel.intrs))); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
41 |
qed "LCons_Domain_findRel"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
42 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
43 |
Addsimps [LCons_Domain_findRel]; |
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 |
val major::prems = |
5069 | 46 |
Goal "[| l: Domain (findRel p); \ |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
47 |
\ !!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
|
48 |
\ |] ==> Q"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
49 |
by (rtac (major RS DomainE) 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
50 |
by (forward_tac [findRel_imp_LCons] 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
51 |
by (REPEAT (eresolve_tac [exE,conjE] 1)); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
52 |
by (hyp_subst_tac 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
53 |
by (REPEAT (ares_tac prems 1)); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
54 |
qed "Domain_findRelE"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
55 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
56 |
val prems = goal thy |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
57 |
"[| !!x. p x ==> q x |] ==> Domain (findRel p) <= Domain (findRel q)"; |
3718 | 58 |
by (Clarify_tac 1); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
59 |
by (etac findRel.induct 1); |
5618 | 60 |
by (blast_tac (claset() addIs findRel.intrs @ prems) 1); |
4090 | 61 |
by (blast_tac (claset() addIs findRel.intrs) 1); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
62 |
qed "Domain_findRel_mono"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
63 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
64 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
65 |
(*** find: basic equations ***) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
66 |
|
5069 | 67 |
Goalw [find_def] "find p LNil = LNil"; |
4535 | 68 |
by (Blast_tac 1); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
69 |
qed "find_LNil"; |
4521 | 70 |
Addsimps [find_LNil]; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
71 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
72 |
Goalw [find_def] "(l,l') : findRel p ==> find p l = l'"; |
4535 | 73 |
by (blast_tac (claset() addDs [findRel_functional]) 1); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
74 |
qed "findRel_imp_find"; |
4521 | 75 |
Addsimps [findRel_imp_find]; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
76 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
77 |
Goal "p x ==> find p (LCons x l) = LCons x l"; |
4090 | 78 |
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
|
79 |
qed "find_LCons_found"; |
4521 | 80 |
Addsimps [find_LCons_found]; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
81 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
82 |
Goalw [find_def] "l ~: Domain(findRel p) ==> find p l = LNil"; |
4535 | 83 |
by (Blast_tac 1); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
84 |
qed "diverge_find_LNil"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
85 |
Addsimps [diverge_find_LNil]; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
86 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
87 |
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
|
88 |
by (case_tac "LCons x l : Domain(findRel p)" 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
89 |
by (Asm_full_simp_tac 2); |
3718 | 90 |
by (Clarify_tac 1); |
4521 | 91 |
by (Asm_simp_tac 1); |
4090 | 92 |
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
|
93 |
qed "find_LCons_seek"; |
4521 | 94 |
Addsimps [find_LCons_seek]; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
95 |
|
5069 | 96 |
Goal "find p (LCons x l) = (if p x then LCons x l else find p l)"; |
4686 | 97 |
by (Asm_simp_tac 1); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
98 |
qed "find_LCons"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
99 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
100 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
101 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
102 |
(*** lfilter: basic equations ***) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
103 |
|
5069 | 104 |
Goal "lfilter p LNil = LNil"; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
105 |
by (rtac (lfilter_def RS def_llist_corec RS trans) 1); |
4521 | 106 |
by (Simp_tac 1); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
107 |
qed "lfilter_LNil"; |
4521 | 108 |
Addsimps [lfilter_LNil]; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
109 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
110 |
Goal "l ~: Domain(findRel p) ==> lfilter p l = LNil"; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
111 |
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
|
112 |
by (Asm_simp_tac 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
113 |
qed "diverge_lfilter_LNil"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
114 |
|
4521 | 115 |
Addsimps [diverge_lfilter_LNil]; |
116 |
||
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
117 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
118 |
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
|
119 |
by (rtac (lfilter_def RS def_llist_corec RS trans) 1); |
4521 | 120 |
by (Asm_simp_tac 1); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
121 |
qed "lfilter_LCons_found"; |
4521 | 122 |
(*This rewrite and lfilter_LCons_seek are NOT added because lfilter_LCons |
123 |
subsumes both*) |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
124 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
125 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
126 |
Goal "(l, LCons x l') : findRel p \ |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
127 |
\ ==> lfilter p l = LCons x (lfilter p l')"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
128 |
by (rtac (lfilter_def RS def_llist_corec RS trans) 1); |
4521 | 129 |
by (Asm_simp_tac 1); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
130 |
qed "findRel_imp_lfilter"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
131 |
|
4521 | 132 |
Addsimps [findRel_imp_lfilter]; |
133 |
||
134 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
135 |
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
|
136 |
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
|
137 |
by (case_tac "LCons x l : Domain(findRel p)" 1); |
4521 | 138 |
by (Asm_full_simp_tac 2); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
139 |
by (etac Domain_findRelE 1); |
4090 | 140 |
by (safe_tac (claset() delrules [conjI])); |
4521 | 141 |
by (Asm_full_simp_tac 1); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
142 |
qed "lfilter_LCons_seek"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
143 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
144 |
|
5069 | 145 |
Goal "lfilter p (LCons x l) = \ |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
146 |
\ (if p x then LCons x (lfilter p l) else lfilter p l)"; |
4686 | 147 |
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
|
148 |
qed "lfilter_LCons"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
149 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
150 |
AddSIs [llistD_Fun_LNil_I, llistD_Fun_LCons_I]; |
4521 | 151 |
Addsimps [lfilter_LCons]; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
152 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
153 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
154 |
Goal "lfilter p l = LNil ==> l ~: Domain(findRel p)"; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
155 |
by (rtac notI 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
156 |
by (etac Domain_findRelE 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
157 |
by (etac rev_mp 1); |
4521 | 158 |
by (Asm_simp_tac 1); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
159 |
qed "lfilter_eq_LNil"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
160 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
161 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
162 |
Goal "lfilter p l = LCons x l' --> \ |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
163 |
\ (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
|
164 |
by (stac (lfilter_def RS def_llist_corec) 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
165 |
by (case_tac "l : Domain(findRel p)" 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
166 |
by (etac Domain_findRelE 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
167 |
by (Asm_simp_tac 2); |
4521 | 168 |
by (Asm_simp_tac 1); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
169 |
by (Blast_tac 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
170 |
qed_spec_mp "lfilter_eq_LCons"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
171 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
172 |
|
5069 | 173 |
Goal "lfilter p l = LNil | \ |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
174 |
\ (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
|
175 |
by (case_tac "l : Domain(findRel p)" 1); |
4521 | 176 |
by (Asm_simp_tac 2); |
4090 | 177 |
by (blast_tac (claset() addSEs [Domain_findRelE] |
4521 | 178 |
addIs [findRel_imp_lfilter]) 1); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
179 |
qed "lfilter_cases"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
180 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
181 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
182 |
(*** lfilter: simple facts by coinduction ***) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
183 |
|
5069 | 184 |
Goal "lfilter (%x. True) l = l"; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
185 |
by (res_inst_tac [("l","l")] llist_fun_equalityI 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
186 |
by (ALLGOALS Simp_tac); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
187 |
qed "lfilter_K_True"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
188 |
|
5069 | 189 |
Goal "lfilter p (lfilter p l) = lfilter p l"; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
190 |
by (res_inst_tac [("l","l")] llist_fun_equalityI 1); |
4686 | 191 |
by (ALLGOALS Simp_tac); |
3724 | 192 |
by Safe_tac; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
193 |
(*Cases: p x is true or false*) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
194 |
by (rtac (lfilter_cases RS disjE) 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
195 |
by (etac ssubst 1); |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4090
diff
changeset
|
196 |
by Auto_tac; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
197 |
qed "lfilter_idem"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
198 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
199 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
200 |
(*** Numerous lemmas required to prove lfilter_conj: |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
201 |
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
|
202 |
***) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
203 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
204 |
Goal "(l,l') : findRel q \ |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
205 |
\ ==> 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
|
206 |
by (etac findRel.induct 1); |
4090 | 207 |
by (blast_tac (claset() addIs findRel.intrs) 1); |
208 |
by (blast_tac (claset() addIs findRel.intrs) 1); |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
209 |
qed_spec_mp "findRel_conj_lemma"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
210 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
211 |
val findRel_conj = refl RSN (2, findRel_conj_lemma); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
212 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
213 |
Goal "(l,l'') : findRel (%x. p x & q x) \ |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
214 |
\ ==> (l, LCons x l') : findRel q --> ~ p x \ |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
215 |
\ --> l' : Domain (findRel (%x. p x & q x))"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
216 |
by (etac findRel.induct 1); |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4090
diff
changeset
|
217 |
by Auto_tac; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
218 |
qed_spec_mp "findRel_not_conj_Domain"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
219 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
220 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
221 |
Goal "(l,lxx) : findRel q ==> \ |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
222 |
\ 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
|
223 |
\ --> (l,lz) : findRel (%x. p x & q x)"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
224 |
by (etac findRel.induct 1); |
4090 | 225 |
by (ALLGOALS (blast_tac (claset() addIs findRel.intrs))); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
226 |
qed_spec_mp "findRel_conj2"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
227 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
228 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
229 |
Goal "(lx,ly) : findRel p \ |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
230 |
\ ==> ALL l. lx = lfilter q l \ |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
231 |
\ --> l : Domain (findRel(%x. p x & q x))"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
232 |
by (etac findRel.induct 1); |
4090 | 233 |
by (blast_tac (claset() addSDs [sym RS lfilter_eq_LCons] |
4521 | 234 |
addIs [findRel_conj]) 1); |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4090
diff
changeset
|
235 |
by Auto_tac; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
236 |
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
|
237 |
by Auto_tac; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
238 |
by (dtac spec 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
239 |
by (dtac (refl RS rev_mp) 1); |
4090 | 240 |
by (blast_tac (claset() addIs [findRel_conj2]) 1); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
241 |
qed_spec_mp "findRel_lfilter_Domain_conj"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
242 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
243 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
244 |
Goal "(l,l'') : findRel(%x. p x & q x) \ |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
245 |
\ ==> l'' = LCons y l' --> \ |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
246 |
\ (lfilter q l, LCons y (lfilter q l')) : findRel p"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
247 |
by (etac findRel.induct 1); |
4686 | 248 |
by (ALLGOALS Asm_simp_tac); |
4090 | 249 |
by (ALLGOALS (blast_tac (claset() addIs findRel.intrs))); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
250 |
qed_spec_mp "findRel_conj_lfilter"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
251 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
252 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
253 |
|
5069 | 254 |
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
|
255 |
\ : llistD_Fun (range \ |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
256 |
\ (%u. (lfilter p (lfilter q u), \ |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
257 |
\ lfilter (%x. p x & q x) u)))"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
258 |
by (case_tac "l : Domain(findRel q)" 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
259 |
by (subgoal_tac "l ~: Domain (findRel (%x. p x & q x))" 2); |
4090 | 260 |
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
|
261 |
(*There are no qs in l: both lists are LNil*) |
4521 | 262 |
by (Asm_simp_tac 2); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
263 |
by (etac Domain_findRelE 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
264 |
(*case q x*) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
265 |
by (case_tac "p x" 1); |
4521 | 266 |
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
|
267 |
(*case q x and ~(p x) *) |
4521 | 268 |
by (Asm_simp_tac 1); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
269 |
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
|
270 |
(*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
|
271 |
by (subgoal_tac "l ~: Domain (findRel (%x. p x & q x))" 2); |
4090 | 272 |
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
|
273 |
by (subgoal_tac "lfilter q l' ~: Domain(findRel p)" 2); |
4090 | 274 |
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
|
275 |
(* ...and therefore too, no p in lfilter q l'. Both results are Lnil*) |
4521 | 276 |
by (Asm_simp_tac 2); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
277 |
(*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
|
278 |
by (etac Domain_findRelE 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
279 |
by (subgoal_tac "(l, LCons xa l'a) : findRel(%x. p x & q x)" 1); |
4090 | 280 |
by (blast_tac (claset() addIs [findRel_conj2]) 2); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
281 |
by (subgoal_tac "(lfilter q l', LCons xa (lfilter q l'a)) : findRel p" 1); |
4090 | 282 |
by (blast_tac (claset() addIs [findRel_conj_lfilter]) 2); |
4521 | 283 |
by (Asm_simp_tac 1); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
284 |
val lemma = result(); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
285 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
286 |
|
5069 | 287 |
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
|
288 |
by (res_inst_tac [("l","l")] llist_fun_equalityI 1); |
4686 | 289 |
by (ALLGOALS Simp_tac); |
4090 | 290 |
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
|
291 |
qed "lfilter_conj"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
292 |
|
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 |
(*** Numerous lemmas required to prove ??: |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
295 |
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
|
296 |
***) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
297 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
298 |
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
|
299 |
by (etac findRel.induct 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
300 |
by (ALLGOALS Asm_full_simp_tac); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
301 |
qed "findRel_lmap_Domain"; |
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 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
304 |
Goal "lmap f l = LCons x l' --> \ |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
305 |
\ (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
|
306 |
by (stac (lmap_def RS def_llist_corec) 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
307 |
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
|
308 |
by Auto_tac; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
309 |
qed_spec_mp "lmap_eq_LCons"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
310 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
311 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
312 |
Goal "(lx,ly) : findRel p ==> \ |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
313 |
\ ALL l. lmap f l = lx --> ly = LCons x l' --> \ |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
314 |
\ (EX y l''. x = f y & l' = lmap f l'' & \ |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
315 |
\ (l, LCons y l'') : findRel(%x. p(f x)))"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
316 |
by (etac findRel.induct 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
317 |
by (ALLGOALS Asm_simp_tac); |
4090 | 318 |
by (safe_tac (claset() addSDs [lmap_eq_LCons])); |
319 |
by (blast_tac (claset() addIs findRel.intrs) 1); |
|
320 |
by (blast_tac (claset() addIs findRel.intrs) 1); |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
321 |
qed_spec_mp "lmap_LCons_findRel_lemma"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
322 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
323 |
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
|
324 |
|
5069 | 325 |
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
|
326 |
by (res_inst_tac [("l","l")] llist_fun_equalityI 1); |
4686 | 327 |
by (ALLGOALS Simp_tac); |
3724 | 328 |
by Safe_tac; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
329 |
by (case_tac "lmap f l : Domain (findRel p)" 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
330 |
by (subgoal_tac "l ~: Domain (findRel(%x. p (f x)))" 2); |
4090 | 331 |
by (blast_tac (claset() addIs [findRel_lmap_Domain]) 3); |
4521 | 332 |
by (Asm_simp_tac 2); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
333 |
by (etac Domain_findRelE 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
334 |
by (forward_tac [lmap_LCons_findRel] 1); |
3718 | 335 |
by (Clarify_tac 1); |
4521 | 336 |
by (Asm_simp_tac 1); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
337 |
qed "lfilter_lmap"; |