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