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