# HG changeset patch
# User traytel
# Date 1355409368 -3600
# Node ID 8f6c111038204c892729a7f8564d7ccec8b6a121
# Parent  ed6b40d15d1c9ad1b56c0c9f5cde04537264f73e
renamed theory

diff -r ed6b40d15d1c -r 8f6c11103820 src/HOL/BNF/Examples/Koenig.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF/Examples/Koenig.thy	Thu Dec 13 15:36:08 2012 +0100
@@ -0,0 +1,149 @@
+(*  Title:      HOL/BNF/Examples/Stream.thy
+    Author:     Dmitriy Traytel, TU Muenchen
+    Author:     Andrei Popescu, TU Muenchen
+    Copyright   2012
+
+Koenig's lemma.
+*)
+
+header {* Koenig's lemma *}
+
+theory Koenig
+imports TreeFI
+begin
+
+codata 'a stream = Stream (shd: 'a) (stl: "'a stream")
+
+(* selectors for streams *)
+lemma shd_def': "shd as = fst (stream_dtor as)"
+unfolding shd_def stream_case_def fst_def by (rule refl)
+
+lemma stl_def': "stl as = snd (stream_dtor as)"
+unfolding stl_def stream_case_def snd_def by (rule refl)
+
+lemma unfold_pair_fun_shd[simp]: "shd (stream_dtor_unfold (f \<odot> g) t) = f t"
+unfolding shd_def' pair_fun_def stream.dtor_unfold by simp
+
+lemma unfold_pair_fun_stl[simp]: "stl (stream_dtor_unfold (f \<odot> g) t) =
+ stream_dtor_unfold (f \<odot> g) (g t)"
+unfolding stl_def' pair_fun_def stream.dtor_unfold by simp
+
+(* infinite trees: *)
+coinductive infiniteTr where
+"\<lbrakk>tr' \<in> listF_set (sub tr); infiniteTr tr'\<rbrakk> \<Longrightarrow> infiniteTr tr"
+
+lemma infiniteTr_strong_coind[consumes 1, case_names sub]:
+assumes *: "phi tr" and
+**: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> listF_set (sub tr). phi tr' \<or> infiniteTr tr'"
+shows "infiniteTr tr"
+using assms by (elim infiniteTr.coinduct) blast
+
+lemma infiniteTr_coind[consumes 1, case_names sub, induct pred: infiniteTr]:
+assumes *: "phi tr" and
+**: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> listF_set (sub tr). phi tr'"
+shows "infiniteTr tr"
+using assms by (elim infiniteTr.coinduct) blast
+
+lemma infiniteTr_sub[simp]:
+"infiniteTr tr \<Longrightarrow> (\<exists> tr' \<in> listF_set (sub tr). infiniteTr tr')"
+by (erule infiniteTr.cases) blast
+
+definition "konigPath \<equiv> stream_dtor_unfold
+  (lab \<odot> (\<lambda>tr. SOME tr'. tr' \<in> listF_set (sub tr) \<and> infiniteTr tr'))"
+
+lemma konigPath_simps[simp]:
+"shd (konigPath t) = lab t"
+"stl (konigPath t) = konigPath (SOME tr. tr \<in> listF_set (sub t) \<and> infiniteTr tr)"
+unfolding konigPath_def by simp+
+
+(* proper paths in trees: *)
+coinductive properPath where
+"\<lbrakk>shd as = lab tr; tr' \<in> listF_set (sub tr); properPath (stl as) tr'\<rbrakk> \<Longrightarrow>
+ properPath as tr"
+
+lemma properPath_strong_coind[consumes 1, case_names shd_lab sub]:
+assumes *: "phi as tr" and
+**: "\<And> as tr. phi as tr \<Longrightarrow> shd as = lab tr" and
+***: "\<And> as tr.
+         phi as tr \<Longrightarrow>
+         \<exists> tr' \<in> listF_set (sub tr). phi (stl as) tr' \<or> properPath (stl as) tr'"
+shows "properPath as tr"
+using assms by (elim properPath.coinduct) blast
+
+lemma properPath_coind[consumes 1, case_names shd_lab sub, induct pred: properPath]:
+assumes *: "phi as tr" and
+**: "\<And> as tr. phi as tr \<Longrightarrow> shd as = lab tr" and
+***: "\<And> as tr.
+         phi as tr \<Longrightarrow>
+         \<exists> tr' \<in> listF_set (sub tr). phi (stl as) tr'"
+shows "properPath as tr"
+using properPath_strong_coind[of phi, OF * **] *** by blast
+
+lemma properPath_shd_lab:
+"properPath as tr \<Longrightarrow> shd as = lab tr"
+by (erule properPath.cases) blast
+
+lemma properPath_sub:
+"properPath as tr \<Longrightarrow>
+ \<exists> tr' \<in> listF_set (sub tr). phi (stl as) tr' \<or> properPath (stl as) tr'"
+by (erule properPath.cases) blast
+
+(* prove the following by coinduction *)
+theorem Konig:
+  assumes "infiniteTr tr"
+  shows "properPath (konigPath tr) tr"
+proof-
+  {fix as
+   assume "infiniteTr tr \<and> as = konigPath tr" hence "properPath as tr"
+   proof (induct rule: properPath_coind, safe)
+     fix t
+     let ?t = "SOME t'. t' \<in> listF_set (sub t) \<and> infiniteTr t'"
+     assume "infiniteTr t"
+     hence "\<exists>t' \<in> listF_set (sub t). infiniteTr t'" by simp
+     hence "\<exists>t'. t' \<in> listF_set (sub t) \<and> infiniteTr t'" by blast
+     hence "?t \<in> listF_set (sub t) \<and> infiniteTr ?t" by (elim someI_ex)
+     moreover have "stl (konigPath t) = konigPath ?t" by simp
+     ultimately show "\<exists>t' \<in> listF_set (sub t).
+             infiniteTr t' \<and> stl (konigPath t) = konigPath t'" by blast
+   qed simp
+  }
+  thus ?thesis using assms by blast
+qed
+
+(* some more stream theorems *)
+
+lemma stream_map[simp]: "stream_map f = stream_dtor_unfold (f o shd \<odot> stl)"
+unfolding stream_map_def pair_fun_def shd_def'[abs_def] stl_def'[abs_def]
+  map_pair_def o_def prod_case_beta by simp
+
+definition plus :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<oplus>" 66) where
+  [simp]: "plus xs ys =
+    stream_dtor_unfold ((%(xs, ys). shd xs + shd ys) \<odot> (%(xs, ys). (stl xs, stl ys))) (xs, ys)"
+
+definition scalar :: "nat \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<cdot>" 68) where
+  [simp]: "scalar n = stream_map (\<lambda>x. n * x)"
+
+definition ones :: "nat stream" where [simp]: "ones = stream_dtor_unfold ((%x. 1) \<odot> id) ()"
+definition twos :: "nat stream" where [simp]: "twos = stream_dtor_unfold ((%x. 2) \<odot> id) ()"
+definition ns :: "nat \<Rightarrow> nat stream" where [simp]: "ns n = scalar n ones"
+
+lemma "ones \<oplus> ones = twos"
+by (rule stream.coinduct[of "%x1 x2. \<exists>x. x1 = ones \<oplus> ones \<and> x2 = twos"]) auto
+
+lemma "n \<cdot> twos = ns (2 * n)"
+by (rule stream.coinduct[of "%x1 x2. \<exists>n. x1 = n \<cdot> twos \<and> x2 = ns (2 * n)"]) force+
+
+lemma prod_scalar: "(n * m) \<cdot> xs = n \<cdot> m \<cdot> xs"
+by (rule stream.coinduct[of "%x1 x2. \<exists>n m xs. x1 = (n * m) \<cdot> xs \<and> x2 = n \<cdot> m \<cdot> xs"]) force+
+
+lemma scalar_plus: "n \<cdot> (xs \<oplus> ys) = n \<cdot> xs \<oplus> n \<cdot> ys"
+by (rule stream.coinduct[of "%x1 x2. \<exists>n xs ys. x1 = n \<cdot> (xs \<oplus> ys) \<and> x2 = n \<cdot> xs \<oplus> n \<cdot> ys"])
+   (force simp: add_mult_distrib2)+
+
+lemma plus_comm: "xs \<oplus> ys = ys \<oplus> xs"
+by (rule stream.coinduct[of "%x1 x2. \<exists>xs ys. x1 = xs \<oplus> ys \<and> x2 = ys \<oplus> xs"]) force+
+
+lemma plus_assoc: "(xs \<oplus> ys) \<oplus> zs = xs \<oplus> ys \<oplus> zs"
+by (rule stream.coinduct[of "%x1 x2. \<exists>xs ys zs. x1 = (xs \<oplus> ys) \<oplus> zs \<and> x2 = xs \<oplus> ys \<oplus> zs"]) force+
+
+end
diff -r ed6b40d15d1c -r 8f6c11103820 src/HOL/BNF/Examples/Stream.thy
--- a/src/HOL/BNF/Examples/Stream.thy	Thu Dec 13 13:11:38 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,149 +0,0 @@
-(*  Title:      HOL/BNF/Examples/Stream.thy
-    Author:     Dmitriy Traytel, TU Muenchen
-    Author:     Andrei Popescu, TU Muenchen
-    Copyright   2012
-
-Infinite streams.
-*)
-
-header {* Infinite Streams *}
-
-theory Stream
-imports TreeFI
-begin
-
-codata 'a stream = Stream (hdd: 'a) (tll: "'a stream")
-
-(* selectors for streams *)
-lemma hdd_def': "hdd as = fst (stream_dtor as)"
-unfolding hdd_def stream_case_def fst_def by (rule refl)
-
-lemma tll_def': "tll as = snd (stream_dtor as)"
-unfolding tll_def stream_case_def snd_def by (rule refl)
-
-lemma unfold_pair_fun_hdd[simp]: "hdd (stream_dtor_unfold (f \<odot> g) t) = f t"
-unfolding hdd_def' pair_fun_def stream.dtor_unfold by simp
-
-lemma unfold_pair_fun_tll[simp]: "tll (stream_dtor_unfold (f \<odot> g) t) =
- stream_dtor_unfold (f \<odot> g) (g t)"
-unfolding tll_def' pair_fun_def stream.dtor_unfold by simp
-
-(* infinite trees: *)
-coinductive infiniteTr where
-"\<lbrakk>tr' \<in> listF_set (sub tr); infiniteTr tr'\<rbrakk> \<Longrightarrow> infiniteTr tr"
-
-lemma infiniteTr_strong_coind[consumes 1, case_names sub]:
-assumes *: "phi tr" and
-**: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> listF_set (sub tr). phi tr' \<or> infiniteTr tr'"
-shows "infiniteTr tr"
-using assms by (elim infiniteTr.coinduct) blast
-
-lemma infiniteTr_coind[consumes 1, case_names sub, induct pred: infiniteTr]:
-assumes *: "phi tr" and
-**: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> listF_set (sub tr). phi tr'"
-shows "infiniteTr tr"
-using assms by (elim infiniteTr.coinduct) blast
-
-lemma infiniteTr_sub[simp]:
-"infiniteTr tr \<Longrightarrow> (\<exists> tr' \<in> listF_set (sub tr). infiniteTr tr')"
-by (erule infiniteTr.cases) blast
-
-definition "konigPath \<equiv> stream_dtor_unfold
-  (lab \<odot> (\<lambda>tr. SOME tr'. tr' \<in> listF_set (sub tr) \<and> infiniteTr tr'))"
-
-lemma konigPath_simps[simp]:
-"hdd (konigPath t) = lab t"
-"tll (konigPath t) = konigPath (SOME tr. tr \<in> listF_set (sub t) \<and> infiniteTr tr)"
-unfolding konigPath_def by simp+
-
-(* proper paths in trees: *)
-coinductive properPath where
-"\<lbrakk>hdd as = lab tr; tr' \<in> listF_set (sub tr); properPath (tll as) tr'\<rbrakk> \<Longrightarrow>
- properPath as tr"
-
-lemma properPath_strong_coind[consumes 1, case_names hdd_lab sub]:
-assumes *: "phi as tr" and
-**: "\<And> as tr. phi as tr \<Longrightarrow> hdd as = lab tr" and
-***: "\<And> as tr.
-         phi as tr \<Longrightarrow>
-         \<exists> tr' \<in> listF_set (sub tr). phi (tll as) tr' \<or> properPath (tll as) tr'"
-shows "properPath as tr"
-using assms by (elim properPath.coinduct) blast
-
-lemma properPath_coind[consumes 1, case_names hdd_lab sub, induct pred: properPath]:
-assumes *: "phi as tr" and
-**: "\<And> as tr. phi as tr \<Longrightarrow> hdd as = lab tr" and
-***: "\<And> as tr.
-         phi as tr \<Longrightarrow>
-         \<exists> tr' \<in> listF_set (sub tr). phi (tll as) tr'"
-shows "properPath as tr"
-using properPath_strong_coind[of phi, OF * **] *** by blast
-
-lemma properPath_hdd_lab:
-"properPath as tr \<Longrightarrow> hdd as = lab tr"
-by (erule properPath.cases) blast
-
-lemma properPath_sub:
-"properPath as tr \<Longrightarrow>
- \<exists> tr' \<in> listF_set (sub tr). phi (tll as) tr' \<or> properPath (tll as) tr'"
-by (erule properPath.cases) blast
-
-(* prove the following by coinduction *)
-theorem Konig:
-  assumes "infiniteTr tr"
-  shows "properPath (konigPath tr) tr"
-proof-
-  {fix as
-   assume "infiniteTr tr \<and> as = konigPath tr" hence "properPath as tr"
-   proof (induct rule: properPath_coind, safe)
-     fix t
-     let ?t = "SOME t'. t' \<in> listF_set (sub t) \<and> infiniteTr t'"
-     assume "infiniteTr t"
-     hence "\<exists>t' \<in> listF_set (sub t). infiniteTr t'" by simp
-     hence "\<exists>t'. t' \<in> listF_set (sub t) \<and> infiniteTr t'" by blast
-     hence "?t \<in> listF_set (sub t) \<and> infiniteTr ?t" by (elim someI_ex)
-     moreover have "tll (konigPath t) = konigPath ?t" by simp
-     ultimately show "\<exists>t' \<in> listF_set (sub t).
-             infiniteTr t' \<and> tll (konigPath t) = konigPath t'" by blast
-   qed simp
-  }
-  thus ?thesis using assms by blast
-qed
-
-(* some more stream theorems *)
-
-lemma stream_map[simp]: "stream_map f = stream_dtor_unfold (f o hdd \<odot> tll)"
-unfolding stream_map_def pair_fun_def hdd_def'[abs_def] tll_def'[abs_def]
-  map_pair_def o_def prod_case_beta by simp
-
-definition plus :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<oplus>" 66) where
-  [simp]: "plus xs ys =
-    stream_dtor_unfold ((%(xs, ys). hdd xs + hdd ys) \<odot> (%(xs, ys). (tll xs, tll ys))) (xs, ys)"
-
-definition scalar :: "nat \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<cdot>" 68) where
-  [simp]: "scalar n = stream_map (\<lambda>x. n * x)"
-
-definition ones :: "nat stream" where [simp]: "ones = stream_dtor_unfold ((%x. 1) \<odot> id) ()"
-definition twos :: "nat stream" where [simp]: "twos = stream_dtor_unfold ((%x. 2) \<odot> id) ()"
-definition ns :: "nat \<Rightarrow> nat stream" where [simp]: "ns n = scalar n ones"
-
-lemma "ones \<oplus> ones = twos"
-by (rule stream.coinduct[of "%x1 x2. \<exists>x. x1 = ones \<oplus> ones \<and> x2 = twos"]) auto
-
-lemma "n \<cdot> twos = ns (2 * n)"
-by (rule stream.coinduct[of "%x1 x2. \<exists>n. x1 = n \<cdot> twos \<and> x2 = ns (2 * n)"]) force+
-
-lemma prod_scalar: "(n * m) \<cdot> xs = n \<cdot> m \<cdot> xs"
-by (rule stream.coinduct[of "%x1 x2. \<exists>n m xs. x1 = (n * m) \<cdot> xs \<and> x2 = n \<cdot> m \<cdot> xs"]) force+
-
-lemma scalar_plus: "n \<cdot> (xs \<oplus> ys) = n \<cdot> xs \<oplus> n \<cdot> ys"
-by (rule stream.coinduct[of "%x1 x2. \<exists>n xs ys. x1 = n \<cdot> (xs \<oplus> ys) \<and> x2 = n \<cdot> xs \<oplus> n \<cdot> ys"])
-   (force simp: add_mult_distrib2)+
-
-lemma plus_comm: "xs \<oplus> ys = ys \<oplus> xs"
-by (rule stream.coinduct[of "%x1 x2. \<exists>xs ys. x1 = xs \<oplus> ys \<and> x2 = ys \<oplus> xs"]) force+
-
-lemma plus_assoc: "(xs \<oplus> ys) \<oplus> zs = xs \<oplus> ys \<oplus> zs"
-by (rule stream.coinduct[of "%x1 x2. \<exists>xs ys zs. x1 = (xs \<oplus> ys) \<oplus> zs \<and> x2 = xs \<oplus> ys \<oplus> zs"]) force+
-
-end
diff -r ed6b40d15d1c -r 8f6c11103820 src/HOL/ROOT
--- a/src/HOL/ROOT	Thu Dec 13 13:11:38 2012 +0100
+++ b/src/HOL/ROOT	Thu Dec 13 15:36:08 2012 +0100
@@ -633,7 +633,7 @@
     TreeFsetI
     "Derivation_Trees/Gram_Lang"
     "Derivation_Trees/Parallel"
-    Stream
+    Koenig
   theories [condition = ISABELLE_FULL_TEST]
     Misc_Codata
     Misc_Data