src/HOL/Induct/LFilter.thy
author urbanc
Tue Jun 05 09:56:19 2007 +0200 (2007-06-05)
changeset 23243 a37d3e6e8323
parent 21404 eb85850d3eb7
child 23746 a455e69c31cc
permissions -rw-r--r--
included Class.thy in the compiling process for Nominal/Examples
     1 (*  Title:      HOL/LList.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1997  University of Cambridge
     5 *)
     6 
     7 header {*The "filter" functional for coinductive lists
     8   --defined by a combination of induction and coinduction*}
     9 
    10 theory LFilter imports LList begin
    11 
    12 consts
    13   findRel	:: "('a => bool) => ('a llist * 'a llist)set"
    14 
    15 inductive "findRel p"
    16   intros
    17     found:  "p x ==> (LCons x l, LCons x l) \<in> findRel p"
    18     seek:   "[| ~p x;  (l,l') \<in> findRel p |] ==> (LCons x l, l') \<in> findRel p"
    19 
    20 declare findRel.intros [intro]
    21 
    22 definition
    23   find    :: "['a => bool, 'a llist] => 'a llist" where
    24   "find p l = (SOME l'. (l,l'): findRel p | (l' = LNil & l ~: Domain(findRel p)))"
    25 
    26 definition
    27   lfilter :: "['a => bool, 'a llist] => 'a llist" where
    28   "lfilter p l = llist_corec l (%l. case find p l of
    29                                             LNil => None
    30                                           | LCons y z => Some(y,z))"
    31 
    32 
    33 subsection {* @{text findRel}: basic laws *}
    34 
    35 inductive_cases
    36   findRel_LConsE [elim!]: "(LCons x l, l'') \<in> findRel p"
    37 
    38 
    39 lemma findRel_functional [rule_format]:
    40      "(l,l'): findRel p ==> (l,l''): findRel p --> l'' = l'"
    41 by (erule findRel.induct, auto)
    42 
    43 lemma findRel_imp_LCons [rule_format]:
    44      "(l,l'): findRel p ==> \<exists>x l''. l' = LCons x l'' & p x"
    45 by (erule findRel.induct, auto)
    46 
    47 lemma findRel_LNil [elim!]: "(LNil,l): findRel p ==> R"
    48 by (blast elim: findRel.cases)
    49 
    50 
    51 subsection {* Properties of @{text "Domain (findRel p)"} *}
    52 
    53 lemma LCons_Domain_findRel [simp]:
    54      "LCons x l \<in> Domain(findRel p) = (p x | l \<in> Domain(findRel p))"
    55 by auto
    56 
    57 lemma Domain_findRel_iff:
    58      "(l \<in> Domain (findRel p)) = (\<exists>x l'. (l, LCons x l') \<in> findRel p &  p x)" 
    59 by (blast dest: findRel_imp_LCons) 
    60 
    61 lemma Domain_findRel_mono:
    62     "[| !!x. p x ==> q x |] ==> Domain (findRel p) <= Domain (findRel q)"
    63 apply clarify
    64 apply (erule findRel.induct, blast+)
    65 done
    66 
    67 
    68 subsection {* @{text find}: basic equations *}
    69 
    70 lemma find_LNil [simp]: "find p LNil = LNil"
    71 by (unfold find_def, blast)
    72 
    73 lemma findRel_imp_find [simp]: "(l,l') \<in> findRel p ==> find p l = l'"
    74 apply (unfold find_def)
    75 apply (blast dest: findRel_functional)
    76 done
    77 
    78 lemma find_LCons_found: "p x ==> find p (LCons x l) = LCons x l"
    79 by (blast intro: findRel_imp_find)
    80 
    81 lemma diverge_find_LNil [simp]: "l ~: Domain(findRel p) ==> find p l = LNil"
    82 by (unfold find_def, blast)
    83 
    84 lemma find_LCons_seek: "~ (p x) ==> find p (LCons x l) = find p l"
    85 apply (case_tac "LCons x l \<in> Domain (findRel p) ")
    86  apply auto 
    87 apply (blast intro: findRel_imp_find)
    88 done
    89 
    90 lemma find_LCons [simp]:
    91      "find p (LCons x l) = (if p x then LCons x l else find p l)"
    92 by (simp add: find_LCons_seek find_LCons_found)
    93 
    94 
    95 
    96 subsection {* @{text lfilter}: basic equations *}
    97 
    98 lemma lfilter_LNil [simp]: "lfilter p LNil = LNil"
    99 by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp)
   100 
   101 lemma diverge_lfilter_LNil [simp]:
   102      "l ~: Domain(findRel p) ==> lfilter p l = LNil"
   103 by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp)
   104 
   105 lemma lfilter_LCons_found:
   106      "p x ==> lfilter p (LCons x l) = LCons x (lfilter p l)"
   107 by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp)
   108 
   109 lemma findRel_imp_lfilter [simp]:
   110      "(l, LCons x l') \<in> findRel p ==> lfilter p l = LCons x (lfilter p l')"
   111 by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp)
   112 
   113 lemma lfilter_LCons_seek: "~ (p x) ==> lfilter p (LCons x l) = lfilter p l"
   114 apply (rule lfilter_def [THEN def_llist_corec, THEN trans], simp)
   115 apply (case_tac "LCons x l \<in> Domain (findRel p) ")
   116  apply (simp add: Domain_findRel_iff, auto) 
   117 done
   118 
   119 lemma lfilter_LCons [simp]:
   120      "lfilter p (LCons x l) =  
   121           (if p x then LCons x (lfilter p l) else lfilter p l)"
   122 by (simp add: lfilter_LCons_found lfilter_LCons_seek)
   123 
   124 declare llistD_Fun_LNil_I [intro!] llistD_Fun_LCons_I [intro!]
   125 
   126 
   127 lemma lfilter_eq_LNil: "lfilter p l = LNil ==> l ~: Domain(findRel p)" 
   128 apply (auto iff: Domain_findRel_iff)
   129 done
   130 
   131 lemma lfilter_eq_LCons [rule_format]:
   132      "lfilter p l = LCons x l' -->      
   133                (\<exists>l''. l' = lfilter p l'' & (l, LCons x l'') \<in> findRel p)"
   134 apply (subst lfilter_def [THEN def_llist_corec])
   135 apply (case_tac "l \<in> Domain (findRel p) ")
   136  apply (auto iff: Domain_findRel_iff)
   137 done
   138 
   139 
   140 lemma lfilter_cases: "lfilter p l = LNil  |   
   141           (\<exists>y l'. lfilter p l = LCons y (lfilter p l') & p y)"
   142 apply (case_tac "l \<in> Domain (findRel p) ")
   143 apply (auto iff: Domain_findRel_iff)
   144 done
   145 
   146 
   147 subsection {* @{text lfilter}: simple facts by coinduction *}
   148 
   149 lemma lfilter_K_True: "lfilter (%x. True) l = l"
   150 by (rule_tac l = "l" in llist_fun_equalityI, simp_all)
   151 
   152 lemma lfilter_idem: "lfilter p (lfilter p l) = lfilter p l"
   153 apply (rule_tac l = "l" in llist_fun_equalityI, simp_all)
   154 apply safe
   155 txt{*Cases: @{text "p x"} is true or false*}
   156 apply (rule lfilter_cases [THEN disjE])
   157  apply (erule ssubst, auto)
   158 done
   159 
   160 
   161 subsection {* Numerous lemmas required to prove @{text lfilter_conj} *}
   162 
   163 lemma findRel_conj_lemma [rule_format]:
   164      "(l,l') \<in> findRel q  
   165       ==> l' = LCons x l'' --> p x --> (l,l') \<in> findRel (%x. p x & q x)"
   166 by (erule findRel.induct, auto)
   167 
   168 lemmas findRel_conj = findRel_conj_lemma [OF _ refl]
   169 
   170 lemma findRel_not_conj_Domain [rule_format]:
   171      "(l,l'') \<in> findRel (%x. p x & q x)  
   172       ==> (l, LCons x l') \<in> findRel q --> ~ p x --> 
   173           l' \<in> Domain (findRel (%x. p x & q x))"
   174 by (erule findRel.induct, auto)
   175 
   176 lemma findRel_conj2 [rule_format]:
   177      "(l,lxx) \<in> findRel q 
   178       ==> lxx = LCons x lx --> (lx,lz) \<in> findRel(%x. p x & q x) --> ~ p x  
   179           --> (l,lz) \<in> findRel (%x. p x & q x)"
   180 by (erule findRel.induct, auto)
   181 
   182 lemma findRel_lfilter_Domain_conj [rule_format]:
   183      "(lx,ly) \<in> findRel p  
   184       ==> \<forall>l. lx = lfilter q l --> l \<in> Domain (findRel(%x. p x & q x))"
   185 apply (erule findRel.induct)
   186  apply (blast dest!: sym [THEN lfilter_eq_LCons] intro: findRel_conj, auto)
   187 apply (drule sym [THEN lfilter_eq_LCons], auto)
   188 apply (drule spec)
   189 apply (drule refl [THEN rev_mp])
   190 apply (blast intro: findRel_conj2)
   191 done
   192 
   193 
   194 lemma findRel_conj_lfilter [rule_format]:
   195      "(l,l'') \<in> findRel(%x. p x & q x)  
   196       ==> l'' = LCons y l' --> 
   197           (lfilter q l, LCons y (lfilter q l')) \<in> findRel p"
   198 by (erule findRel.induct, auto)
   199 
   200 lemma lfilter_conj_lemma:
   201      "(lfilter p (lfilter q l), lfilter (%x. p x & q x) l)   
   202       \<in> llistD_Fun (range (%u. (lfilter p (lfilter q u),           
   203                                 lfilter (%x. p x & q x) u)))"
   204 apply (case_tac "l \<in> Domain (findRel q)")
   205  apply (subgoal_tac [2] "l ~: Domain (findRel (%x. p x & q x))")
   206   prefer 3 apply (blast intro: rev_subsetD [OF _ Domain_findRel_mono])
   207  txt{*There are no @{text qs} in @{text l}: both lists are @{text LNil}*}
   208  apply (simp_all add: Domain_findRel_iff, clarify) 
   209 txt{*case @{text "q x"}*}
   210 apply (case_tac "p x")
   211  apply (simp_all add: findRel_conj [THEN findRel_imp_lfilter])
   212  txt{*case @{text "q x"} and @{text "~(p x)"} *}
   213 apply (case_tac "l' \<in> Domain (findRel (%x. p x & q x))")
   214  txt{*subcase: there is no @{text "p & q"} in @{text l'} and therefore none in @{text l}*}
   215  apply (subgoal_tac [2] "l ~: Domain (findRel (%x. p x & q x))")
   216   prefer 3 apply (blast intro: findRel_not_conj_Domain)
   217  apply (subgoal_tac [2] "lfilter q l' ~: Domain (findRel p) ")
   218   prefer 3 apply (blast intro: findRel_lfilter_Domain_conj)
   219  txt{*    {\dots} and therefore too, no @{text p} in @{text "lfilter q l'"}.
   220    Both results are @{text LNil}*}
   221  apply (simp_all add: Domain_findRel_iff, clarify) 
   222 txt{*subcase: there is a @{text "p & q"} in @{text l'} and therefore also one in @{text l} *}
   223 apply (subgoal_tac " (l, LCons xa l'a) \<in> findRel (%x. p x & q x) ")
   224  prefer 2 apply (blast intro: findRel_conj2)
   225 apply (subgoal_tac " (lfilter q l', LCons xa (lfilter q l'a)) \<in> findRel p")
   226  apply simp 
   227 apply (blast intro: findRel_conj_lfilter)
   228 done
   229 
   230 
   231 lemma lfilter_conj: "lfilter p (lfilter q l) = lfilter (%x. p x & q x) l"
   232 apply (rule_tac l = "l" in llist_fun_equalityI, simp_all)
   233 apply (blast intro: lfilter_conj_lemma rev_subsetD [OF _ llistD_Fun_mono])
   234 done
   235 
   236 
   237 subsection {* Numerous lemmas required to prove ??:
   238      @{text "lfilter p (lmap f l) = lmap f (lfilter (%x. p(f x)) l)"}
   239  *}
   240 
   241 lemma findRel_lmap_Domain:
   242      "(l,l') \<in> findRel(%x. p (f x)) ==> lmap f l \<in> Domain(findRel p)"
   243 by (erule findRel.induct, auto)
   244 
   245 lemma lmap_eq_LCons [rule_format]: "lmap f l = LCons x l' -->      
   246                (\<exists>y l''. x = f y & l' = lmap f l'' & l = LCons y l'')"
   247 apply (subst lmap_def [THEN def_llist_corec])
   248 apply (rule_tac l = "l" in llistE, auto)
   249 done
   250 
   251 
   252 lemma lmap_LCons_findRel_lemma [rule_format]:
   253      "(lx,ly) \<in> findRel p
   254       ==> \<forall>l. lmap f l = lx --> ly = LCons x l' -->  
   255           (\<exists>y l''. x = f y & l' = lmap f l'' &        
   256           (l, LCons y l'') \<in> findRel(%x. p(f x)))"
   257 apply (erule findRel.induct, simp_all)
   258 apply (blast dest!: lmap_eq_LCons)+
   259 done
   260 
   261 lemmas lmap_LCons_findRel = lmap_LCons_findRel_lemma [OF _ refl refl]
   262 
   263 lemma lfilter_lmap: "lfilter p (lmap f l) = lmap f (lfilter (p o f) l)"
   264 apply (rule_tac l = "l" in llist_fun_equalityI, simp_all)
   265 apply safe
   266 apply (case_tac "lmap f l \<in> Domain (findRel p)")
   267  apply (simp add: Domain_findRel_iff, clarify)
   268  apply (frule lmap_LCons_findRel, force) 
   269 apply (subgoal_tac "l ~: Domain (findRel (%x. p (f x)))", simp)
   270 apply (blast intro: findRel_lmap_Domain)
   271 done
   272 
   273 end