(* Title: HOL/LList.thy ID: $Id: LFilter.thy,v 1.7 2005/06/17 14:13:07 haftmann Exp $ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1997 University of Cambridge *) header {*The "filter" functional for coinductive lists --defined by a combination of induction and coinduction*} theory LFilter imports LList begin consts findRel :: "('a => bool) => ('a llist * 'a llist)set" inductive "findRel p" intros found: "p x ==> (LCons x l, LCons x l) ∈ findRel p" seek: "[| ~p x; (l,l') ∈ findRel p |] ==> (LCons x l, l') ∈ findRel p" declare findRel.intros [intro] constdefs find :: "['a => bool, 'a llist] => 'a llist" "find p l == @l'. (l,l'): findRel p | (l' = LNil & l ~: Domain(findRel p))" lfilter :: "['a => bool, 'a llist] => 'a llist" "lfilter p l == llist_corec l (%l. case find p l of LNil => None | LCons y z => Some(y,z))" subsection {* @{text findRel}: basic laws *} inductive_cases findRel_LConsE [elim!]: "(LCons x l, l'') ∈ findRel p" lemma findRel_functional [rule_format]: "(l,l'): findRel p ==> (l,l''): findRel p --> l'' = l'" by (erule findRel.induct, auto) lemma findRel_imp_LCons [rule_format]: "(l,l'): findRel p ==> ∃x l''. l' = LCons x l'' & p x" by (erule findRel.induct, auto) lemma findRel_LNil [elim!]: "(LNil,l): findRel p ==> R" by (blast elim: findRel.cases) subsection {* Properties of @{text "Domain (findRel p)"} *} lemma LCons_Domain_findRel [simp]: "LCons x l ∈ Domain(findRel p) = (p x | l ∈ Domain(findRel p))" by auto lemma Domain_findRel_iff: "(l ∈ Domain (findRel p)) = (∃x l'. (l, LCons x l') ∈ findRel p & p x)" by (blast dest: findRel_imp_LCons) lemma Domain_findRel_mono: "[| !!x. p x ==> q x |] ==> Domain (findRel p) <= Domain (findRel q)" apply clarify apply (erule findRel.induct, blast+) done subsection {* @{text find}: basic equations *} lemma find_LNil [simp]: "find p LNil = LNil" by (unfold find_def, blast) lemma findRel_imp_find [simp]: "(l,l') ∈ findRel p ==> find p l = l'" apply (unfold find_def) apply (blast dest: findRel_functional) done lemma find_LCons_found: "p x ==> find p (LCons x l) = LCons x l" by (blast intro: findRel_imp_find) lemma diverge_find_LNil [simp]: "l ~: Domain(findRel p) ==> find p l = LNil" by (unfold find_def, blast) lemma find_LCons_seek: "~ (p x) ==> find p (LCons x l) = find p l" apply (case_tac "LCons x l ∈ Domain (findRel p) ") apply auto apply (blast intro: findRel_imp_find) done lemma find_LCons [simp]: "find p (LCons x l) = (if p x then LCons x l else find p l)" by (simp add: find_LCons_seek find_LCons_found) subsection {* @{text lfilter}: basic equations *} lemma lfilter_LNil [simp]: "lfilter p LNil = LNil" by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp) lemma diverge_lfilter_LNil [simp]: "l ~: Domain(findRel p) ==> lfilter p l = LNil" by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp) lemma lfilter_LCons_found: "p x ==> lfilter p (LCons x l) = LCons x (lfilter p l)" by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp) lemma findRel_imp_lfilter [simp]: "(l, LCons x l') ∈ findRel p ==> lfilter p l = LCons x (lfilter p l')" by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp) lemma lfilter_LCons_seek: "~ (p x) ==> lfilter p (LCons x l) = lfilter p l" apply (rule lfilter_def [THEN def_llist_corec, THEN trans], simp) apply (case_tac "LCons x l ∈ Domain (findRel p) ") apply (simp add: Domain_findRel_iff, auto) done lemma lfilter_LCons [simp]: "lfilter p (LCons x l) = (if p x then LCons x (lfilter p l) else lfilter p l)" by (simp add: lfilter_LCons_found lfilter_LCons_seek) declare llistD_Fun_LNil_I [intro!] llistD_Fun_LCons_I [intro!] lemma lfilter_eq_LNil: "lfilter p l = LNil ==> l ~: Domain(findRel p)" apply (auto iff: Domain_findRel_iff) done lemma lfilter_eq_LCons [rule_format]: "lfilter p l = LCons x l' --> (∃l''. l' = lfilter p l'' & (l, LCons x l'') ∈ findRel p)" apply (subst lfilter_def [THEN def_llist_corec]) apply (case_tac "l ∈ Domain (findRel p) ") apply (auto iff: Domain_findRel_iff) done lemma lfilter_cases: "lfilter p l = LNil | (∃y l'. lfilter p l = LCons y (lfilter p l') & p y)" apply (case_tac "l ∈ Domain (findRel p) ") apply (auto iff: Domain_findRel_iff) done subsection {* @{text lfilter}: simple facts by coinduction *} lemma lfilter_K_True: "lfilter (%x. True) l = l" by (rule_tac l = "l" in llist_fun_equalityI, simp_all) lemma lfilter_idem: "lfilter p (lfilter p l) = lfilter p l" apply (rule_tac l = "l" in llist_fun_equalityI, simp_all) apply safe txt{*Cases: @{text "p x"} is true or false*} apply (rule lfilter_cases [THEN disjE]) apply (erule ssubst, auto) done subsection {* Numerous lemmas required to prove @{text lfilter_conj} *} lemma findRel_conj_lemma [rule_format]: "(l,l') ∈ findRel q ==> l' = LCons x l'' --> p x --> (l,l') ∈ findRel (%x. p x & q x)" by (erule findRel.induct, auto) lemmas findRel_conj = findRel_conj_lemma [OF _ refl] lemma findRel_not_conj_Domain [rule_format]: "(l,l'') ∈ findRel (%x. p x & q x) ==> (l, LCons x l') ∈ findRel q --> ~ p x --> l' ∈ Domain (findRel (%x. p x & q x))" by (erule findRel.induct, auto) lemma findRel_conj2 [rule_format]: "(l,lxx) ∈ findRel q ==> lxx = LCons x lx --> (lx,lz) ∈ findRel(%x. p x & q x) --> ~ p x --> (l,lz) ∈ findRel (%x. p x & q x)" by (erule findRel.induct, auto) lemma findRel_lfilter_Domain_conj [rule_format]: "(lx,ly) ∈ findRel p ==> ∀l. lx = lfilter q l --> l ∈ Domain (findRel(%x. p x & q x))" apply (erule findRel.induct) apply (blast dest!: sym [THEN lfilter_eq_LCons] intro: findRel_conj, auto) apply (drule sym [THEN lfilter_eq_LCons], auto) apply (drule spec) apply (drule refl [THEN rev_mp]) apply (blast intro: findRel_conj2) done lemma findRel_conj_lfilter [rule_format]: "(l,l'') ∈ findRel(%x. p x & q x) ==> l'' = LCons y l' --> (lfilter q l, LCons y (lfilter q l')) ∈ findRel p" by (erule findRel.induct, auto) lemma lfilter_conj_lemma: "(lfilter p (lfilter q l), lfilter (%x. p x & q x) l) ∈ llistD_Fun (range (%u. (lfilter p (lfilter q u), lfilter (%x. p x & q x) u)))" apply (case_tac "l ∈ Domain (findRel q)") apply (subgoal_tac [2] "l ~: Domain (findRel (%x. p x & q x))") prefer 3 apply (blast intro: rev_subsetD [OF _ Domain_findRel_mono]) txt{*There are no @{text qs} in @{text l}: both lists are @{text LNil}*} apply (simp_all add: Domain_findRel_iff, clarify) txt{*case @{text "q x"}*} apply (case_tac "p x") apply (simp_all add: findRel_conj [THEN findRel_imp_lfilter]) txt{*case @{text "q x"} and @{text "~(p x)"} *} apply (case_tac "l' ∈ Domain (findRel (%x. p x & q x))") txt{*subcase: there is no @{text "p & q"} in @{text l'} and therefore none in @{text l}*} apply (subgoal_tac [2] "l ~: Domain (findRel (%x. p x & q x))") prefer 3 apply (blast intro: findRel_not_conj_Domain) apply (subgoal_tac [2] "lfilter q l' ~: Domain (findRel p) ") prefer 3 apply (blast intro: findRel_lfilter_Domain_conj) txt{* {\dots} and therefore too, no @{text p} in @{text "lfilter q l'"}. Both results are @{text LNil}*} apply (simp_all add: Domain_findRel_iff, clarify) txt{*subcase: there is a @{text "p & q"} in @{text l'} and therefore also one in @{text l} *} apply (subgoal_tac " (l, LCons xa l'a) ∈ findRel (%x. p x & q x) ") prefer 2 apply (blast intro: findRel_conj2) apply (subgoal_tac " (lfilter q l', LCons xa (lfilter q l'a)) ∈ findRel p") apply simp apply (blast intro: findRel_conj_lfilter) done lemma lfilter_conj: "lfilter p (lfilter q l) = lfilter (%x. p x & q x) l" apply (rule_tac l = "l" in llist_fun_equalityI, simp_all) apply (blast intro: lfilter_conj_lemma rev_subsetD [OF _ llistD_Fun_mono]) done subsection {* Numerous lemmas required to prove ??: @{text "lfilter p (lmap f l) = lmap f (lfilter (%x. p(f x)) l)"} *} lemma findRel_lmap_Domain: "(l,l') ∈ findRel(%x. p (f x)) ==> lmap f l ∈ Domain(findRel p)" by (erule findRel.induct, auto) lemma lmap_eq_LCons [rule_format]: "lmap f l = LCons x l' --> (∃y l''. x = f y & l' = lmap f l'' & l = LCons y l'')" apply (subst lmap_def [THEN def_llist_corec]) apply (rule_tac l = "l" in llistE, auto) done lemma lmap_LCons_findRel_lemma [rule_format]: "(lx,ly) ∈ findRel p ==> ∀l. lmap f l = lx --> ly = LCons x l' --> (∃y l''. x = f y & l' = lmap f l'' & (l, LCons y l'') ∈ findRel(%x. p(f x)))" apply (erule findRel.induct, simp_all) apply (blast dest!: lmap_eq_LCons)+ done lemmas lmap_LCons_findRel = lmap_LCons_findRel_lemma [OF _ refl refl] lemma lfilter_lmap: "lfilter p (lmap f l) = lmap f (lfilter (p o f) l)" apply (rule_tac l = "l" in llist_fun_equalityI, simp_all) apply safe apply (case_tac "lmap f l ∈ Domain (findRel p)") apply (simp add: Domain_findRel_iff, clarify) apply (frule lmap_LCons_findRel, force) apply (subgoal_tac "l ~: Domain (findRel (%x. p (f x)))", simp) apply (blast intro: findRel_lmap_Domain) done end
lemmas findRel_LConsE:
[| (LCons x l, l'') ∈ findRel p; [| p x; l'' = LCons x l |] ==> P; [| ¬ p x; (l, l'') ∈ findRel p |] ==> P |] ==> P
lemma findRel_functional:
[| (l, l') ∈ findRel p; (l, l'') ∈ findRel p |] ==> l'' = l'
lemma findRel_imp_LCons:
(l, l') ∈ findRel p ==> ∃x l''. l' = LCons x l'' ∧ p x
lemma findRel_LNil:
(LNil, l) ∈ findRel p ==> R
lemma LCons_Domain_findRel:
(LCons x l ∈ Domain (findRel p)) = (p x ∨ l ∈ Domain (findRel p))
lemma Domain_findRel_iff:
(l ∈ Domain (findRel p)) = (∃x l'. (l, LCons x l') ∈ findRel p ∧ p x)
lemma Domain_findRel_mono:
(!!x. p x ==> q x) ==> Domain (findRel p) ⊆ Domain (findRel q)
lemma find_LNil:
find p LNil = LNil
lemma findRel_imp_find:
(l, l') ∈ findRel p ==> find p l = l'
lemma find_LCons_found:
p x ==> find p (LCons x l) = LCons x l
lemma diverge_find_LNil:
l ∉ Domain (findRel p) ==> find p l = LNil
lemma find_LCons_seek:
¬ p x ==> find p (LCons x l) = find p l
lemma find_LCons:
find p (LCons x l) = (if p x then LCons x l else find p l)
lemma lfilter_LNil:
lfilter p LNil = LNil
lemma diverge_lfilter_LNil:
l ∉ Domain (findRel p) ==> lfilter p l = LNil
lemma lfilter_LCons_found:
p x ==> lfilter p (LCons x l) = LCons x (lfilter p l)
lemma findRel_imp_lfilter:
(l, LCons x l') ∈ findRel p ==> lfilter p l = LCons x (lfilter p l')
lemma lfilter_LCons_seek:
¬ p x ==> lfilter p (LCons x l) = lfilter p l
lemma lfilter_LCons:
lfilter p (LCons x l) = (if p x then LCons x (lfilter p l) else lfilter p l)
lemma lfilter_eq_LNil:
lfilter p l = LNil ==> l ∉ Domain (findRel p)
lemma lfilter_eq_LCons:
lfilter p l = LCons x l' ==> ∃l''. l' = lfilter p l'' ∧ (l, LCons x l'') ∈ findRel p
lemma lfilter_cases:
lfilter p l = LNil ∨ (∃y l'. lfilter p l = LCons y (lfilter p l') ∧ p y)
lemma lfilter_K_True:
lfilter (%x. True) l = l
lemma lfilter_idem:
lfilter p (lfilter p l) = lfilter p l
lemma findRel_conj_lemma:
[| (l, l') ∈ findRel q; l' = LCons x l''; p x |] ==> (l, l') ∈ findRel (%x. p x ∧ q x)
lemmas findRel_conj:
[| (l, LCons x l'') ∈ findRel q; p x |] ==> (l, LCons x l'') ∈ findRel (%x. p x ∧ q x)
lemmas findRel_conj:
[| (l, LCons x l'') ∈ findRel q; p x |] ==> (l, LCons x l'') ∈ findRel (%x. p x ∧ q x)
lemma findRel_not_conj_Domain:
[| (l, l'') ∈ findRel (%x. p x ∧ q x); (l, LCons x l') ∈ findRel q; ¬ p x |] ==> l' ∈ Domain (findRel (%x. p x ∧ q x))
lemma findRel_conj2:
[| (l, lxx) ∈ findRel q; lxx = LCons x lx; (lx, lz) ∈ findRel (%x. p x ∧ q x); ¬ p x |] ==> (l, lz) ∈ findRel (%x. p x ∧ q x)
lemma findRel_lfilter_Domain_conj:
[| (lx, ly) ∈ findRel p; lx = lfilter q l |] ==> l ∈ Domain (findRel (%x. p x ∧ q x))
lemma findRel_conj_lfilter:
[| (l, l'') ∈ findRel (%x. p x ∧ q x); l'' = LCons y l' |] ==> (lfilter q l, LCons y (lfilter q l')) ∈ findRel p
lemma lfilter_conj_lemma:
(lfilter p (lfilter q l), lfilter (%x. p x ∧ q x) l) ∈ llistD_Fun (range (%u. (lfilter p (lfilter q u), lfilter (%x. p x ∧ q x) u)))
lemma lfilter_conj:
lfilter p (lfilter q l) = lfilter (%x. p x ∧ q x) l
lemma findRel_lmap_Domain:
(l, l') ∈ findRel (%x. p (f x)) ==> lmap f l ∈ Domain (findRel p)
lemma lmap_eq_LCons:
lmap f l = LCons x l' ==> ∃y l''. x = f y ∧ l' = lmap f l'' ∧ l = LCons y l''
lemma lmap_LCons_findRel_lemma:
[| (lx, ly) ∈ findRel p; lmap f l = lx; ly = LCons x l' |] ==> ∃y l''. x = f y ∧ l' = lmap f l'' ∧ (l, LCons y l'') ∈ findRel (%x. p (f x))
lemmas lmap_LCons_findRel:
(lmap f l, LCons x l') ∈ findRel p ==> ∃y l''. x = f y ∧ l' = lmap f l'' ∧ (l, LCons y l'') ∈ findRel (%x. p (f x))
lemmas lmap_LCons_findRel:
(lmap f l, LCons x l') ∈ findRel p ==> ∃y l''. x = f y ∧ l' = lmap f l'' ∧ (l, LCons y l'') ∈ findRel (%x. p (f x))
lemma lfilter_lmap:
lfilter p (lmap f l) = lmap f (lfilter (p o f) l)