renamed theory
authortraytel
Thu Dec 13 15:36:08 2012 +0100 (2012-12-13)
changeset 505178f6c11103820
parent 50516 ed6b40d15d1c
child 50518 d4fdda801e19
renamed theory
src/HOL/BNF/Examples/Koenig.thy
src/HOL/BNF/Examples/Stream.thy
src/HOL/ROOT
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/BNF/Examples/Koenig.thy	Thu Dec 13 15:36:08 2012 +0100
     1.3 @@ -0,0 +1,149 @@
     1.4 +(*  Title:      HOL/BNF/Examples/Stream.thy
     1.5 +    Author:     Dmitriy Traytel, TU Muenchen
     1.6 +    Author:     Andrei Popescu, TU Muenchen
     1.7 +    Copyright   2012
     1.8 +
     1.9 +Koenig's lemma.
    1.10 +*)
    1.11 +
    1.12 +header {* Koenig's lemma *}
    1.13 +
    1.14 +theory Koenig
    1.15 +imports TreeFI
    1.16 +begin
    1.17 +
    1.18 +codata 'a stream = Stream (shd: 'a) (stl: "'a stream")
    1.19 +
    1.20 +(* selectors for streams *)
    1.21 +lemma shd_def': "shd as = fst (stream_dtor as)"
    1.22 +unfolding shd_def stream_case_def fst_def by (rule refl)
    1.23 +
    1.24 +lemma stl_def': "stl as = snd (stream_dtor as)"
    1.25 +unfolding stl_def stream_case_def snd_def by (rule refl)
    1.26 +
    1.27 +lemma unfold_pair_fun_shd[simp]: "shd (stream_dtor_unfold (f \<odot> g) t) = f t"
    1.28 +unfolding shd_def' pair_fun_def stream.dtor_unfold by simp
    1.29 +
    1.30 +lemma unfold_pair_fun_stl[simp]: "stl (stream_dtor_unfold (f \<odot> g) t) =
    1.31 + stream_dtor_unfold (f \<odot> g) (g t)"
    1.32 +unfolding stl_def' pair_fun_def stream.dtor_unfold by simp
    1.33 +
    1.34 +(* infinite trees: *)
    1.35 +coinductive infiniteTr where
    1.36 +"\<lbrakk>tr' \<in> listF_set (sub tr); infiniteTr tr'\<rbrakk> \<Longrightarrow> infiniteTr tr"
    1.37 +
    1.38 +lemma infiniteTr_strong_coind[consumes 1, case_names sub]:
    1.39 +assumes *: "phi tr" and
    1.40 +**: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> listF_set (sub tr). phi tr' \<or> infiniteTr tr'"
    1.41 +shows "infiniteTr tr"
    1.42 +using assms by (elim infiniteTr.coinduct) blast
    1.43 +
    1.44 +lemma infiniteTr_coind[consumes 1, case_names sub, induct pred: infiniteTr]:
    1.45 +assumes *: "phi tr" and
    1.46 +**: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> listF_set (sub tr). phi tr'"
    1.47 +shows "infiniteTr tr"
    1.48 +using assms by (elim infiniteTr.coinduct) blast
    1.49 +
    1.50 +lemma infiniteTr_sub[simp]:
    1.51 +"infiniteTr tr \<Longrightarrow> (\<exists> tr' \<in> listF_set (sub tr). infiniteTr tr')"
    1.52 +by (erule infiniteTr.cases) blast
    1.53 +
    1.54 +definition "konigPath \<equiv> stream_dtor_unfold
    1.55 +  (lab \<odot> (\<lambda>tr. SOME tr'. tr' \<in> listF_set (sub tr) \<and> infiniteTr tr'))"
    1.56 +
    1.57 +lemma konigPath_simps[simp]:
    1.58 +"shd (konigPath t) = lab t"
    1.59 +"stl (konigPath t) = konigPath (SOME tr. tr \<in> listF_set (sub t) \<and> infiniteTr tr)"
    1.60 +unfolding konigPath_def by simp+
    1.61 +
    1.62 +(* proper paths in trees: *)
    1.63 +coinductive properPath where
    1.64 +"\<lbrakk>shd as = lab tr; tr' \<in> listF_set (sub tr); properPath (stl as) tr'\<rbrakk> \<Longrightarrow>
    1.65 + properPath as tr"
    1.66 +
    1.67 +lemma properPath_strong_coind[consumes 1, case_names shd_lab sub]:
    1.68 +assumes *: "phi as tr" and
    1.69 +**: "\<And> as tr. phi as tr \<Longrightarrow> shd as = lab tr" and
    1.70 +***: "\<And> as tr.
    1.71 +         phi as tr \<Longrightarrow>
    1.72 +         \<exists> tr' \<in> listF_set (sub tr). phi (stl as) tr' \<or> properPath (stl as) tr'"
    1.73 +shows "properPath as tr"
    1.74 +using assms by (elim properPath.coinduct) blast
    1.75 +
    1.76 +lemma properPath_coind[consumes 1, case_names shd_lab sub, induct pred: properPath]:
    1.77 +assumes *: "phi as tr" and
    1.78 +**: "\<And> as tr. phi as tr \<Longrightarrow> shd as = lab tr" and
    1.79 +***: "\<And> as tr.
    1.80 +         phi as tr \<Longrightarrow>
    1.81 +         \<exists> tr' \<in> listF_set (sub tr). phi (stl as) tr'"
    1.82 +shows "properPath as tr"
    1.83 +using properPath_strong_coind[of phi, OF * **] *** by blast
    1.84 +
    1.85 +lemma properPath_shd_lab:
    1.86 +"properPath as tr \<Longrightarrow> shd as = lab tr"
    1.87 +by (erule properPath.cases) blast
    1.88 +
    1.89 +lemma properPath_sub:
    1.90 +"properPath as tr \<Longrightarrow>
    1.91 + \<exists> tr' \<in> listF_set (sub tr). phi (stl as) tr' \<or> properPath (stl as) tr'"
    1.92 +by (erule properPath.cases) blast
    1.93 +
    1.94 +(* prove the following by coinduction *)
    1.95 +theorem Konig:
    1.96 +  assumes "infiniteTr tr"
    1.97 +  shows "properPath (konigPath tr) tr"
    1.98 +proof-
    1.99 +  {fix as
   1.100 +   assume "infiniteTr tr \<and> as = konigPath tr" hence "properPath as tr"
   1.101 +   proof (induct rule: properPath_coind, safe)
   1.102 +     fix t
   1.103 +     let ?t = "SOME t'. t' \<in> listF_set (sub t) \<and> infiniteTr t'"
   1.104 +     assume "infiniteTr t"
   1.105 +     hence "\<exists>t' \<in> listF_set (sub t). infiniteTr t'" by simp
   1.106 +     hence "\<exists>t'. t' \<in> listF_set (sub t) \<and> infiniteTr t'" by blast
   1.107 +     hence "?t \<in> listF_set (sub t) \<and> infiniteTr ?t" by (elim someI_ex)
   1.108 +     moreover have "stl (konigPath t) = konigPath ?t" by simp
   1.109 +     ultimately show "\<exists>t' \<in> listF_set (sub t).
   1.110 +             infiniteTr t' \<and> stl (konigPath t) = konigPath t'" by blast
   1.111 +   qed simp
   1.112 +  }
   1.113 +  thus ?thesis using assms by blast
   1.114 +qed
   1.115 +
   1.116 +(* some more stream theorems *)
   1.117 +
   1.118 +lemma stream_map[simp]: "stream_map f = stream_dtor_unfold (f o shd \<odot> stl)"
   1.119 +unfolding stream_map_def pair_fun_def shd_def'[abs_def] stl_def'[abs_def]
   1.120 +  map_pair_def o_def prod_case_beta by simp
   1.121 +
   1.122 +definition plus :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<oplus>" 66) where
   1.123 +  [simp]: "plus xs ys =
   1.124 +    stream_dtor_unfold ((%(xs, ys). shd xs + shd ys) \<odot> (%(xs, ys). (stl xs, stl ys))) (xs, ys)"
   1.125 +
   1.126 +definition scalar :: "nat \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<cdot>" 68) where
   1.127 +  [simp]: "scalar n = stream_map (\<lambda>x. n * x)"
   1.128 +
   1.129 +definition ones :: "nat stream" where [simp]: "ones = stream_dtor_unfold ((%x. 1) \<odot> id) ()"
   1.130 +definition twos :: "nat stream" where [simp]: "twos = stream_dtor_unfold ((%x. 2) \<odot> id) ()"
   1.131 +definition ns :: "nat \<Rightarrow> nat stream" where [simp]: "ns n = scalar n ones"
   1.132 +
   1.133 +lemma "ones \<oplus> ones = twos"
   1.134 +by (rule stream.coinduct[of "%x1 x2. \<exists>x. x1 = ones \<oplus> ones \<and> x2 = twos"]) auto
   1.135 +
   1.136 +lemma "n \<cdot> twos = ns (2 * n)"
   1.137 +by (rule stream.coinduct[of "%x1 x2. \<exists>n. x1 = n \<cdot> twos \<and> x2 = ns (2 * n)"]) force+
   1.138 +
   1.139 +lemma prod_scalar: "(n * m) \<cdot> xs = n \<cdot> m \<cdot> xs"
   1.140 +by (rule stream.coinduct[of "%x1 x2. \<exists>n m xs. x1 = (n * m) \<cdot> xs \<and> x2 = n \<cdot> m \<cdot> xs"]) force+
   1.141 +
   1.142 +lemma scalar_plus: "n \<cdot> (xs \<oplus> ys) = n \<cdot> xs \<oplus> n \<cdot> ys"
   1.143 +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"])
   1.144 +   (force simp: add_mult_distrib2)+
   1.145 +
   1.146 +lemma plus_comm: "xs \<oplus> ys = ys \<oplus> xs"
   1.147 +by (rule stream.coinduct[of "%x1 x2. \<exists>xs ys. x1 = xs \<oplus> ys \<and> x2 = ys \<oplus> xs"]) force+
   1.148 +
   1.149 +lemma plus_assoc: "(xs \<oplus> ys) \<oplus> zs = xs \<oplus> ys \<oplus> zs"
   1.150 +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+
   1.151 +
   1.152 +end
     2.1 --- a/src/HOL/BNF/Examples/Stream.thy	Thu Dec 13 13:11:38 2012 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,149 +0,0 @@
     2.4 -(*  Title:      HOL/BNF/Examples/Stream.thy
     2.5 -    Author:     Dmitriy Traytel, TU Muenchen
     2.6 -    Author:     Andrei Popescu, TU Muenchen
     2.7 -    Copyright   2012
     2.8 -
     2.9 -Infinite streams.
    2.10 -*)
    2.11 -
    2.12 -header {* Infinite Streams *}
    2.13 -
    2.14 -theory Stream
    2.15 -imports TreeFI
    2.16 -begin
    2.17 -
    2.18 -codata 'a stream = Stream (hdd: 'a) (tll: "'a stream")
    2.19 -
    2.20 -(* selectors for streams *)
    2.21 -lemma hdd_def': "hdd as = fst (stream_dtor as)"
    2.22 -unfolding hdd_def stream_case_def fst_def by (rule refl)
    2.23 -
    2.24 -lemma tll_def': "tll as = snd (stream_dtor as)"
    2.25 -unfolding tll_def stream_case_def snd_def by (rule refl)
    2.26 -
    2.27 -lemma unfold_pair_fun_hdd[simp]: "hdd (stream_dtor_unfold (f \<odot> g) t) = f t"
    2.28 -unfolding hdd_def' pair_fun_def stream.dtor_unfold by simp
    2.29 -
    2.30 -lemma unfold_pair_fun_tll[simp]: "tll (stream_dtor_unfold (f \<odot> g) t) =
    2.31 - stream_dtor_unfold (f \<odot> g) (g t)"
    2.32 -unfolding tll_def' pair_fun_def stream.dtor_unfold by simp
    2.33 -
    2.34 -(* infinite trees: *)
    2.35 -coinductive infiniteTr where
    2.36 -"\<lbrakk>tr' \<in> listF_set (sub tr); infiniteTr tr'\<rbrakk> \<Longrightarrow> infiniteTr tr"
    2.37 -
    2.38 -lemma infiniteTr_strong_coind[consumes 1, case_names sub]:
    2.39 -assumes *: "phi tr" and
    2.40 -**: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> listF_set (sub tr). phi tr' \<or> infiniteTr tr'"
    2.41 -shows "infiniteTr tr"
    2.42 -using assms by (elim infiniteTr.coinduct) blast
    2.43 -
    2.44 -lemma infiniteTr_coind[consumes 1, case_names sub, induct pred: infiniteTr]:
    2.45 -assumes *: "phi tr" and
    2.46 -**: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> listF_set (sub tr). phi tr'"
    2.47 -shows "infiniteTr tr"
    2.48 -using assms by (elim infiniteTr.coinduct) blast
    2.49 -
    2.50 -lemma infiniteTr_sub[simp]:
    2.51 -"infiniteTr tr \<Longrightarrow> (\<exists> tr' \<in> listF_set (sub tr). infiniteTr tr')"
    2.52 -by (erule infiniteTr.cases) blast
    2.53 -
    2.54 -definition "konigPath \<equiv> stream_dtor_unfold
    2.55 -  (lab \<odot> (\<lambda>tr. SOME tr'. tr' \<in> listF_set (sub tr) \<and> infiniteTr tr'))"
    2.56 -
    2.57 -lemma konigPath_simps[simp]:
    2.58 -"hdd (konigPath t) = lab t"
    2.59 -"tll (konigPath t) = konigPath (SOME tr. tr \<in> listF_set (sub t) \<and> infiniteTr tr)"
    2.60 -unfolding konigPath_def by simp+
    2.61 -
    2.62 -(* proper paths in trees: *)
    2.63 -coinductive properPath where
    2.64 -"\<lbrakk>hdd as = lab tr; tr' \<in> listF_set (sub tr); properPath (tll as) tr'\<rbrakk> \<Longrightarrow>
    2.65 - properPath as tr"
    2.66 -
    2.67 -lemma properPath_strong_coind[consumes 1, case_names hdd_lab sub]:
    2.68 -assumes *: "phi as tr" and
    2.69 -**: "\<And> as tr. phi as tr \<Longrightarrow> hdd as = lab tr" and
    2.70 -***: "\<And> as tr.
    2.71 -         phi as tr \<Longrightarrow>
    2.72 -         \<exists> tr' \<in> listF_set (sub tr). phi (tll as) tr' \<or> properPath (tll as) tr'"
    2.73 -shows "properPath as tr"
    2.74 -using assms by (elim properPath.coinduct) blast
    2.75 -
    2.76 -lemma properPath_coind[consumes 1, case_names hdd_lab sub, induct pred: properPath]:
    2.77 -assumes *: "phi as tr" and
    2.78 -**: "\<And> as tr. phi as tr \<Longrightarrow> hdd as = lab tr" and
    2.79 -***: "\<And> as tr.
    2.80 -         phi as tr \<Longrightarrow>
    2.81 -         \<exists> tr' \<in> listF_set (sub tr). phi (tll as) tr'"
    2.82 -shows "properPath as tr"
    2.83 -using properPath_strong_coind[of phi, OF * **] *** by blast
    2.84 -
    2.85 -lemma properPath_hdd_lab:
    2.86 -"properPath as tr \<Longrightarrow> hdd as = lab tr"
    2.87 -by (erule properPath.cases) blast
    2.88 -
    2.89 -lemma properPath_sub:
    2.90 -"properPath as tr \<Longrightarrow>
    2.91 - \<exists> tr' \<in> listF_set (sub tr). phi (tll as) tr' \<or> properPath (tll as) tr'"
    2.92 -by (erule properPath.cases) blast
    2.93 -
    2.94 -(* prove the following by coinduction *)
    2.95 -theorem Konig:
    2.96 -  assumes "infiniteTr tr"
    2.97 -  shows "properPath (konigPath tr) tr"
    2.98 -proof-
    2.99 -  {fix as
   2.100 -   assume "infiniteTr tr \<and> as = konigPath tr" hence "properPath as tr"
   2.101 -   proof (induct rule: properPath_coind, safe)
   2.102 -     fix t
   2.103 -     let ?t = "SOME t'. t' \<in> listF_set (sub t) \<and> infiniteTr t'"
   2.104 -     assume "infiniteTr t"
   2.105 -     hence "\<exists>t' \<in> listF_set (sub t). infiniteTr t'" by simp
   2.106 -     hence "\<exists>t'. t' \<in> listF_set (sub t) \<and> infiniteTr t'" by blast
   2.107 -     hence "?t \<in> listF_set (sub t) \<and> infiniteTr ?t" by (elim someI_ex)
   2.108 -     moreover have "tll (konigPath t) = konigPath ?t" by simp
   2.109 -     ultimately show "\<exists>t' \<in> listF_set (sub t).
   2.110 -             infiniteTr t' \<and> tll (konigPath t) = konigPath t'" by blast
   2.111 -   qed simp
   2.112 -  }
   2.113 -  thus ?thesis using assms by blast
   2.114 -qed
   2.115 -
   2.116 -(* some more stream theorems *)
   2.117 -
   2.118 -lemma stream_map[simp]: "stream_map f = stream_dtor_unfold (f o hdd \<odot> tll)"
   2.119 -unfolding stream_map_def pair_fun_def hdd_def'[abs_def] tll_def'[abs_def]
   2.120 -  map_pair_def o_def prod_case_beta by simp
   2.121 -
   2.122 -definition plus :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<oplus>" 66) where
   2.123 -  [simp]: "plus xs ys =
   2.124 -    stream_dtor_unfold ((%(xs, ys). hdd xs + hdd ys) \<odot> (%(xs, ys). (tll xs, tll ys))) (xs, ys)"
   2.125 -
   2.126 -definition scalar :: "nat \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<cdot>" 68) where
   2.127 -  [simp]: "scalar n = stream_map (\<lambda>x. n * x)"
   2.128 -
   2.129 -definition ones :: "nat stream" where [simp]: "ones = stream_dtor_unfold ((%x. 1) \<odot> id) ()"
   2.130 -definition twos :: "nat stream" where [simp]: "twos = stream_dtor_unfold ((%x. 2) \<odot> id) ()"
   2.131 -definition ns :: "nat \<Rightarrow> nat stream" where [simp]: "ns n = scalar n ones"
   2.132 -
   2.133 -lemma "ones \<oplus> ones = twos"
   2.134 -by (rule stream.coinduct[of "%x1 x2. \<exists>x. x1 = ones \<oplus> ones \<and> x2 = twos"]) auto
   2.135 -
   2.136 -lemma "n \<cdot> twos = ns (2 * n)"
   2.137 -by (rule stream.coinduct[of "%x1 x2. \<exists>n. x1 = n \<cdot> twos \<and> x2 = ns (2 * n)"]) force+
   2.138 -
   2.139 -lemma prod_scalar: "(n * m) \<cdot> xs = n \<cdot> m \<cdot> xs"
   2.140 -by (rule stream.coinduct[of "%x1 x2. \<exists>n m xs. x1 = (n * m) \<cdot> xs \<and> x2 = n \<cdot> m \<cdot> xs"]) force+
   2.141 -
   2.142 -lemma scalar_plus: "n \<cdot> (xs \<oplus> ys) = n \<cdot> xs \<oplus> n \<cdot> ys"
   2.143 -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"])
   2.144 -   (force simp: add_mult_distrib2)+
   2.145 -
   2.146 -lemma plus_comm: "xs \<oplus> ys = ys \<oplus> xs"
   2.147 -by (rule stream.coinduct[of "%x1 x2. \<exists>xs ys. x1 = xs \<oplus> ys \<and> x2 = ys \<oplus> xs"]) force+
   2.148 -
   2.149 -lemma plus_assoc: "(xs \<oplus> ys) \<oplus> zs = xs \<oplus> ys \<oplus> zs"
   2.150 -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+
   2.151 -
   2.152 -end
     3.1 --- a/src/HOL/ROOT	Thu Dec 13 13:11:38 2012 +0100
     3.2 +++ b/src/HOL/ROOT	Thu Dec 13 15:36:08 2012 +0100
     3.3 @@ -633,7 +633,7 @@
     3.4      TreeFsetI
     3.5      "Derivation_Trees/Gram_Lang"
     3.6      "Derivation_Trees/Parallel"
     3.7 -    Stream
     3.8 +    Koenig
     3.9    theories [condition = ISABELLE_FULL_TEST]
    3.10      Misc_Codata
    3.11      Misc_Data