# HG changeset patch
# User blanchet
# Date 1458646777 -3600
# Node ID f50d7efc8fe35fb8505d244b11afc7117ddd4562
# Parent  0ae225877b684b9d87359e35d73ee79a6a741f2d
added two 'corec' examples

diff -r 0ae225877b68 -r f50d7efc8fe3 src/HOL/Corec_Examples/LFilter.thy
--- /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
diff -r 0ae225877b68 -r f50d7efc8fe3 src/HOL/Corec_Examples/Stream_Processor.thy
--- /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
diff -r 0ae225877b68 -r f50d7efc8fe3 src/HOL/Datatype_Examples/Stream_Processor.thy
--- 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)"
diff -r 0ae225877b68 -r f50d7efc8fe3 src/HOL/ROOT
--- 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"