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