author | paulson <lp15@cam.ac.uk> |
Mon, 30 Nov 2020 11:06:01 +0000 | |
changeset 72794 | 3757e64e75bb |
parent 66453 | cc19f7ca2ed6 |
permissions | -rw-r--r-- |
62694 | 1 |
(* Title: HOL/Corec_Examples/LFilter.thy |
2 |
Author: Andreas Lochbihler, ETH Zuerich |
|
3 |
Author: Dmitriy Traytel, ETH Zuerich |
|
4 |
Author: Andrei Popescu, TU Muenchen |
|
5 |
Copyright 2014, 2016 |
|
6 |
||
7 |
The filter function on lazy lists. |
|
8 |
*) |
|
9 |
||
62726 | 10 |
section \<open>The Filter Function on Lazy Lists\<close> |
62694 | 11 |
|
12 |
theory LFilter |
|
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
63540
diff
changeset
|
13 |
imports "HOL-Library.BNF_Corec" |
62694 | 14 |
begin |
15 |
||
16 |
codatatype (lset: 'a) llist = |
|
17 |
LNil |
|
18 |
| LCons (lhd: 'a) (ltl: "'a llist") |
|
19 |
||
20 |
corecursive lfilter where |
|
21 |
"lfilter P xs = (if \<forall>x \<in> lset xs. \<not> P x then |
|
22 |
LNil |
|
23 |
else if P (lhd xs) then |
|
24 |
LCons (lhd xs) (lfilter P (ltl xs)) |
|
25 |
else |
|
26 |
lfilter P (ltl xs))" |
|
27 |
proof (relation "measure (\<lambda>(P, xs). LEAST n. P (lhd ((ltl ^^ n) xs)))", rule wf_measure, clarsimp) |
|
28 |
fix P xs x |
|
29 |
assume "x \<in> lset xs" "P x" "\<not> P (lhd xs)" |
|
30 |
from this(1,2) obtain a where "P (lhd ((ltl ^^ a) xs))" |
|
31 |
by (atomize_elim, induct x xs rule: llist.set_induct) |
|
32 |
(auto simp: funpow_Suc_right simp del: funpow.simps(2) intro: exI[of _ 0] exI[of _ "Suc i" for i]) |
|
33 |
with \<open>\<not> P (lhd xs)\<close> |
|
34 |
have "(LEAST n. P (lhd ((ltl ^^ n) xs))) = Suc (LEAST n. P (lhd ((ltl ^^ Suc n) xs)))" |
|
35 |
by (intro Least_Suc) auto |
|
36 |
then show "(LEAST n. P (lhd ((ltl ^^ n) (ltl xs)))) < (LEAST n. P (lhd ((ltl ^^ n) xs)))" |
|
37 |
by (simp add: funpow_swap1[of ltl]) |
|
38 |
qed |
|
39 |
||
40 |
lemma lfilter_LNil [simp]: "lfilter P LNil = LNil" |
|
41 |
by(simp add: lfilter.code) |
|
42 |
||
43 |
lemma lnull_lfilter [simp]: "lfilter P xs = LNil \<longleftrightarrow> (\<forall>x \<in> lset xs. \<not> P x)" |
|
44 |
proof(rule iffI ballI)+ |
|
45 |
show "\<not> P x" if "x \<in> lset xs" "lfilter P xs = LNil" for x using that |
|
46 |
by(induction rule: llist.set_induct)(subst (asm) lfilter.code; auto split: if_split_asm; fail)+ |
|
47 |
qed(simp add: lfilter.code) |
|
48 |
||
49 |
lemma lfilter_LCons [simp]: "lfilter P (LCons x xs) = (if P x then LCons x (lfilter P xs) else lfilter P xs)" |
|
50 |
by(subst lfilter.code)(auto intro: sym) |
|
51 |
||
52 |
lemma llist_in_lfilter [simp]: "lset (lfilter P xs) = lset xs \<inter> {x. P x}" |
|
53 |
proof(intro set_eqI iffI) |
|
54 |
show "x \<in> lset xs \<inter> {x. P x}" if "x \<in> lset (lfilter P xs)" for x using that |
|
55 |
proof(induction ys\<equiv>"lfilter P xs" arbitrary: xs rule: llist.set_induct) |
|
56 |
case (LCons1 x xs ys) |
|
62698 | 57 |
from this show ?case |
62694 | 58 |
apply(induction arg\<equiv>"(P, ys)" arbitrary: ys rule: lfilter.inner_induct) |
59 |
subgoal by(subst (asm) (2) lfilter.code)(auto split: if_split_asm elim: llist.set_cases) |
|
60 |
done |
|
61 |
next |
|
62 |
case (LCons2 xs y x ys) |
|
63 |
from LCons2(3) LCons2(1) show ?case |
|
64 |
apply(induction arg\<equiv>"(P, ys)" arbitrary: ys rule: lfilter.inner_induct) |
|
65 |
subgoal using LCons2(2) by(subst (asm) (2) lfilter.code)(auto split: if_split_asm elim: llist.set_cases) |
|
66 |
done |
|
67 |
qed |
|
68 |
show "x \<in> lset (lfilter P xs)" if "x \<in> lset xs \<inter> {x. P x}" for x |
|
69 |
using that[THEN IntD1] that[THEN IntD2] by(induction) auto |
|
70 |
qed |
|
71 |
||
72 |
lemma lfilter_unique_weak: |
|
73 |
"(\<And>xs. f xs = (if \<forall>x \<in> lset xs. \<not> P x then LNil |
|
74 |
else if P (lhd xs) then LCons (lhd xs) (f (ltl xs)) |
|
75 |
else lfilter P (ltl xs))) |
|
76 |
\<Longrightarrow> f = lfilter P" |
|
77 |
by(corec_unique)(rule ext lfilter.code)+ |
|
78 |
||
79 |
lemma lfilter_unique: |
|
80 |
assumes "\<And>xs. f xs = (if \<forall>x\<in>lset xs. \<not> P x then LNil |
|
81 |
else if P (lhd xs) then LCons (lhd xs) (f (ltl xs)) |
|
82 |
else f (ltl xs))" |
|
83 |
shows "f = lfilter P" |
|
63167 | 84 |
\<comment> \<open>It seems as if we cannot use @{thm lfilter_unique_weak} for showing this as the induction and the coinduction must be nested\<close> |
62694 | 85 |
proof(rule ext) |
86 |
show "f xs = lfilter P xs" for xs |
|
87 |
proof(coinduction arbitrary: xs) |
|
88 |
case (Eq_llist xs) |
|
89 |
show ?case |
|
90 |
apply(induction arg\<equiv>"(P, xs)" arbitrary: xs rule: lfilter.inner_induct) |
|
91 |
apply(subst (1 2 3 4) assms) |
|
92 |
apply(subst (1 2 3 4) lfilter.code) |
|
93 |
apply auto |
|
94 |
done |
|
95 |
qed |
|
62698 | 96 |
qed |
62694 | 97 |
|
98 |
lemma lfilter_lfilter: "lfilter P \<circ> lfilter Q = lfilter (\<lambda>x. P x \<and> Q x)" |
|
99 |
by(rule lfilter_unique)(auto elim: llist.set_cases) |
|
100 |
||
101 |
end |