--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Corec_Examples/LFilter.thy Tue Mar 22 12:39:37 2016 +0100
@@ -0,0 +1,102 @@
+(* Title: HOL/Corec_Examples/LFilter.thy
+ Author: Andreas Lochbihler, ETH Zuerich
+ Author: Dmitriy Traytel, ETH Zuerich
+ Author: Andrei Popescu, TU Muenchen
+ Copyright 2014, 2016
+
+The filter function on lazy lists.
+*)
+
+section {* The Filter Function on Lazy Lists *}
+
+theory LFilter
+imports "~~/src/HOL/Library/BNF_Corec"
+begin
+
+codatatype (lset: 'a) llist =
+ LNil
+| LCons (lhd: 'a) (ltl: "'a llist")
+
+corecursive lfilter where
+ "lfilter P xs = (if \<forall>x \<in> lset xs. \<not> P x then
+ LNil
+ else if P (lhd xs) then
+ LCons (lhd xs) (lfilter P (ltl xs))
+ else
+ lfilter P (ltl xs))"
+proof (relation "measure (\<lambda>(P, xs). LEAST n. P (lhd ((ltl ^^ n) xs)))", rule wf_measure, clarsimp)
+ fix P xs x
+ assume "x \<in> lset xs" "P x" "\<not> P (lhd xs)"
+ from this(1,2) obtain a where "P (lhd ((ltl ^^ a) xs))"
+ by (atomize_elim, induct x xs rule: llist.set_induct)
+ (auto simp: funpow_Suc_right simp del: funpow.simps(2) intro: exI[of _ 0] exI[of _ "Suc i" for i])
+ moreover
+ with \<open>\<not> P (lhd xs)\<close>
+ have "(LEAST n. P (lhd ((ltl ^^ n) xs))) = Suc (LEAST n. P (lhd ((ltl ^^ Suc n) xs)))"
+ by (intro Least_Suc) auto
+ then show "(LEAST n. P (lhd ((ltl ^^ n) (ltl xs)))) < (LEAST n. P (lhd ((ltl ^^ n) xs)))"
+ by (simp add: funpow_swap1[of ltl])
+qed
+
+lemma lfilter_LNil [simp]: "lfilter P LNil = LNil"
+ by(simp add: lfilter.code)
+
+lemma lnull_lfilter [simp]: "lfilter P xs = LNil \<longleftrightarrow> (\<forall>x \<in> lset xs. \<not> P x)"
+proof(rule iffI ballI)+
+ show "\<not> P x" if "x \<in> lset xs" "lfilter P xs = LNil" for x using that
+ by(induction rule: llist.set_induct)(subst (asm) lfilter.code; auto split: if_split_asm; fail)+
+qed(simp add: lfilter.code)
+
+lemma lfilter_LCons [simp]: "lfilter P (LCons x xs) = (if P x then LCons x (lfilter P xs) else lfilter P xs)"
+ by(subst lfilter.code)(auto intro: sym)
+
+lemma llist_in_lfilter [simp]: "lset (lfilter P xs) = lset xs \<inter> {x. P x}"
+proof(intro set_eqI iffI)
+ show "x \<in> lset xs \<inter> {x. P x}" if "x \<in> lset (lfilter P xs)" for x using that
+ proof(induction ys\<equiv>"lfilter P xs" arbitrary: xs rule: llist.set_induct)
+ case (LCons1 x xs ys)
+ from this show ?case
+ apply(induction arg\<equiv>"(P, ys)" arbitrary: ys rule: lfilter.inner_induct)
+ subgoal by(subst (asm) (2) lfilter.code)(auto split: if_split_asm elim: llist.set_cases)
+ done
+ next
+ case (LCons2 xs y x ys)
+ from LCons2(3) LCons2(1) show ?case
+ apply(induction arg\<equiv>"(P, ys)" arbitrary: ys rule: lfilter.inner_induct)
+ subgoal using LCons2(2) by(subst (asm) (2) lfilter.code)(auto split: if_split_asm elim: llist.set_cases)
+ done
+ qed
+ show "x \<in> lset (lfilter P xs)" if "x \<in> lset xs \<inter> {x. P x}" for x
+ using that[THEN IntD1] that[THEN IntD2] by(induction) auto
+qed
+
+lemma lfilter_unique_weak:
+ "(\<And>xs. f xs = (if \<forall>x \<in> lset xs. \<not> P x then LNil
+ else if P (lhd xs) then LCons (lhd xs) (f (ltl xs))
+ else lfilter P (ltl xs)))
+ \<Longrightarrow> f = lfilter P"
+ by(corec_unique)(rule ext lfilter.code)+
+
+lemma lfilter_unique:
+ assumes "\<And>xs. f xs = (if \<forall>x\<in>lset xs. \<not> P x then LNil
+ else if P (lhd xs) then LCons (lhd xs) (f (ltl xs))
+ else f (ltl xs))"
+ shows "f = lfilter P"
+-- \<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>
+proof(rule ext)
+ show "f xs = lfilter P xs" for xs
+ proof(coinduction arbitrary: xs)
+ case (Eq_llist xs)
+ show ?case
+ apply(induction arg\<equiv>"(P, xs)" arbitrary: xs rule: lfilter.inner_induct)
+ apply(subst (1 2 3 4) assms)
+ apply(subst (1 2 3 4) lfilter.code)
+ apply auto
+ done
+ qed
+qed
+
+lemma lfilter_lfilter: "lfilter P \<circ> lfilter Q = lfilter (\<lambda>x. P x \<and> Q x)"
+ by(rule lfilter_unique)(auto elim: llist.set_cases)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Corec_Examples/Stream_Processor.thy Tue Mar 22 12:39:37 2016 +0100
@@ -0,0 +1,77 @@
+(* Title: HOL/Corec_Examples/Stream_Processor.thy
+ Author: Andreas Lochbihler, ETH Zuerich
+ Author: Dmitriy Traytel, ETH Zuerich
+ Author: Andrei Popescu, TU Muenchen
+ Copyright 2014, 2016
+
+Stream processors---a syntactic representation of continuous functions on streams.
+*)
+
+section {* Stream Processors---A Syntactic Representation of Continuous Functions on Streams *}
+
+theory Stream_Processor
+imports "~~/src/HOL/Library/BNF_Corec" "~~/src/HOL/Library/Stream"
+begin
+
+datatype (discs_sels) ('a, 'b, 'c) sp\<^sub>\<mu> =
+ Get "'a \<Rightarrow> ('a, 'b, 'c) sp\<^sub>\<mu>"
+| Put "'b" "'c"
+
+codatatype ('a, 'b) sp\<^sub>\<nu> =
+ In (out: "('a, 'b, ('a, 'b) sp\<^sub>\<nu>) sp\<^sub>\<mu>")
+
+definition "sub \<equiv> {(f a, Get f) | a f. True}"
+
+lemma subI[intro]: "(f a, Get f) \<in> sub"
+ unfolding sub_def by blast
+
+lemma wf_sub[simp, intro]: "wf sub"
+proof (rule wfUNIVI)
+ fix P :: "('a, 'b, 'c) sp\<^sub>\<mu> \<Rightarrow> bool" and x
+ assume "\<forall>x. (\<forall>y. (y, x) \<in> sub \<longrightarrow> P y) \<longrightarrow> P x"
+ hence I: "\<And>x. (\<forall>y. (\<exists>a f. y = f a \<and> x = Get f) \<longrightarrow> P y) \<Longrightarrow> P x" unfolding sub_def by blast
+ show "P x" by (induct x) (auto intro: I)
+qed
+
+definition get where
+ "get f = In (Get (\<lambda>a. out (f a)))"
+
+corecursive run :: "('a, 'b) sp\<^sub>\<nu> \<Rightarrow> 'a stream \<Rightarrow> 'b stream" where
+ "run sp s = (case out sp of
+ Get f \<Rightarrow> run (In (f (shd s))) (stl s)
+ | Put b sp \<Rightarrow> b ## run sp s)"
+ by (relation "map_prod In In ` sub <*lex*> {}")
+ (auto simp: inj_on_def out_def split: sp\<^sub>\<nu>.splits intro: wf_map_prod_image)
+
+corec copy where
+ "copy = In (Get (\<lambda>a. Put a copy))"
+
+friend_of_corec get where
+ "get f = In (Get (\<lambda>a. out (f a)))"
+ by (auto simp: rel_fun_def get_def sp\<^sub>\<mu>.rel_map rel_prod.simps, metis sndI)
+
+lemma run_simps [simp]:
+ "run (In (Get f)) s = run (In (f (shd s))) (stl s)"
+ "run (In (Put b sp)) s = b ## run sp s"
+by(subst run.code; simp; fail)+
+
+lemma copy_sel[simp]: "out copy = Get (\<lambda>a. Put a copy)"
+ by (subst copy.code; simp)
+
+corecursive sp_comp (infixl "oo" 65) where
+ "sp oo sp' = (case (out sp, out sp') of
+ (Put b sp, _) \<Rightarrow> In (Put b (sp oo sp'))
+ | (Get f, Put b sp) \<Rightarrow> In (f b) oo sp
+ | (_, Get g) \<Rightarrow> get (\<lambda>a. (sp oo In (g a))))"
+ by (relation "map_prod In In ` sub <*lex*> map_prod In In ` sub")
+ (auto simp: inj_on_def out_def split: sp\<^sub>\<nu>.splits intro: wf_map_prod_image)
+
+lemma run_copy_unique:
+ "(\<And>s. h s = shd s ## h (stl s)) \<Longrightarrow> h = run copy"
+apply corec_unique
+apply(rule ext)
+apply(subst copy.code)
+apply simp
+done
+
+end
--- a/src/HOL/Datatype_Examples/Stream_Processor.thy Tue Mar 22 12:39:37 2016 +0100
+++ b/src/HOL/Datatype_Examples/Stream_Processor.thy Tue Mar 22 12:39:37 2016 +0100
@@ -17,8 +17,12 @@
section {* Continuous Functions on Streams *}
-datatype ('a, 'b, 'c) sp\<^sub>\<mu> = Get "'a \<Rightarrow> ('a, 'b, 'c) sp\<^sub>\<mu>" | Put "'b" "'c"
-codatatype ('a, 'b) sp\<^sub>\<nu> = In (out: "('a, 'b, ('a, 'b) sp\<^sub>\<nu>) sp\<^sub>\<mu>")
+datatype ('a, 'b, 'c) sp\<^sub>\<mu> =
+ Get "'a \<Rightarrow> ('a, 'b, 'c) sp\<^sub>\<mu>"
+| Put "'b" "'c"
+
+codatatype ('a, 'b) sp\<^sub>\<nu> =
+ In (out: "('a, 'b, ('a, 'b) sp\<^sub>\<nu>) sp\<^sub>\<mu>")
primrec run\<^sub>\<mu> :: "('a, 'b, 'c) sp\<^sub>\<mu> \<Rightarrow> 'a stream \<Rightarrow> ('b \<times> 'c) \<times> 'a stream" where
"run\<^sub>\<mu> (Get f) s = run\<^sub>\<mu> (f (shd s)) (stl s)"
--- a/src/HOL/ROOT Tue Mar 22 12:39:37 2016 +0100
+++ b/src/HOL/ROOT Tue Mar 22 12:39:37 2016 +0100
@@ -792,7 +792,6 @@
*}
options [document = false]
theories
- "~~/src/HOL/Library/Old_Datatype"
Compat
Lambda_Term
Process
@@ -808,6 +807,15 @@
Misc_Primcorec
Misc_Primrec
+session "HOL-Corec_Examples" in Corec_Examples = HOL +
+ description {*
+ Corecursion Examples.
+ *}
+ options [document = false]
+ theories
+ LFilter
+ Stream_Processor
+
session "HOL-Word" (main) in Word = HOL +
theories Word
document_files "root.bib" "root.tex"