--- a/src/HOL/BNF_Examples/Koenig.thy Tue Jun 10 21:15:57 2014 +0200
+++ b/src/HOL/BNF_Examples/Koenig.thy Wed Jun 11 08:58:42 2014 +0200
@@ -14,31 +14,31 @@
(* infinite trees: *)
coinductive infiniteTr where
-"\<lbrakk>tr' \<in> set_listF (sub tr); infiniteTr tr'\<rbrakk> \<Longrightarrow> infiniteTr tr"
+"\<lbrakk>tr' \<in> 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> set_listF (sub tr). phi tr' \<or> infiniteTr tr'"
+**: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> 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> set_listF (sub tr). phi tr'"
+**: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> 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> set_listF (sub tr). infiniteTr tr')"
+"infiniteTr tr \<Longrightarrow> (\<exists> tr' \<in> set (sub tr). infiniteTr tr')"
by (erule infiniteTr.cases) blast
primcorec konigPath where
"shd (konigPath t) = lab t"
-| "stl (konigPath t) = konigPath (SOME tr. tr \<in> set_listF (sub t) \<and> infiniteTr tr)"
+| "stl (konigPath t) = konigPath (SOME tr. tr \<in> set (sub t) \<and> infiniteTr tr)"
(* proper paths in trees: *)
coinductive properPath where
-"\<lbrakk>shd as = lab tr; tr' \<in> set_listF (sub tr); properPath (stl as) tr'\<rbrakk> \<Longrightarrow>
+"\<lbrakk>shd as = lab tr; tr' \<in> set (sub tr); properPath (stl as) tr'\<rbrakk> \<Longrightarrow>
properPath as tr"
lemma properPath_strong_coind[consumes 1, case_names shd_lab sub]:
@@ -46,7 +46,7 @@
**: "\<And> as tr. phi as tr \<Longrightarrow> shd as = lab tr" and
***: "\<And> as tr.
phi as tr \<Longrightarrow>
- \<exists> tr' \<in> set_listF (sub tr). phi (stl as) tr' \<or> properPath (stl as) tr'"
+ \<exists> tr' \<in> set (sub tr). phi (stl as) tr' \<or> properPath (stl as) tr'"
shows "properPath as tr"
using assms by (elim properPath.coinduct) blast
@@ -55,7 +55,7 @@
**: "\<And> as tr. phi as tr \<Longrightarrow> shd as = lab tr" and
***: "\<And> as tr.
phi as tr \<Longrightarrow>
- \<exists> tr' \<in> set_listF (sub tr). phi (stl as) tr'"
+ \<exists> tr' \<in> set (sub tr). phi (stl as) tr'"
shows "properPath as tr"
using properPath_strong_coind[of phi, OF * **] *** by blast
@@ -65,7 +65,7 @@
lemma properPath_sub:
"properPath as tr \<Longrightarrow>
- \<exists> tr' \<in> set_listF (sub tr). phi (stl as) tr' \<or> properPath (stl as) tr'"
+ \<exists> tr' \<in> set (sub tr). phi (stl as) tr' \<or> properPath (stl as) tr'"
by (erule properPath.cases) blast
(* prove the following by coinduction *)
@@ -77,10 +77,10 @@
assume "infiniteTr tr \<and> as = konigPath tr" hence "properPath as tr"
proof (coinduction arbitrary: tr as rule: properPath_coind)
case (sub tr as)
- let ?t = "SOME t'. t' \<in> set_listF (sub tr) \<and> infiniteTr t'"
- from sub have "\<exists>t' \<in> set_listF (sub tr). infiniteTr t'" by simp
- then have "\<exists>t'. t' \<in> set_listF (sub tr) \<and> infiniteTr t'" by blast
- then have "?t \<in> set_listF (sub tr) \<and> infiniteTr ?t" by (rule someI_ex)
+ let ?t = "SOME t'. t' \<in> set (sub tr) \<and> infiniteTr t'"
+ from sub have "\<exists>t' \<in> set (sub tr). infiniteTr t'" by simp
+ then have "\<exists>t'. t' \<in> set (sub tr) \<and> infiniteTr t'" by blast
+ then have "?t \<in> set (sub tr) \<and> infiniteTr ?t" by (rule someI_ex)
moreover have "stl (konigPath tr) = konigPath ?t" by simp
ultimately show ?case using sub by blast
qed simp
--- a/src/HOL/BNF_Examples/ListF.thy Tue Jun 10 21:15:57 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,118 +0,0 @@
-(* Title: HOL/BNF_Examples/ListF.thy
- Author: Dmitriy Traytel, TU Muenchen
- Author: Andrei Popescu, TU Muenchen
- Copyright 2012
-
-Finite lists.
-*)
-
-header {* Finite Lists *}
-
-theory ListF
-imports Main
-begin
-
-datatype_new 'a listF =
- NilF
- | Conss (hdF: 'a) (tlF: "'a listF")
-for
- map: mapF
- rel: relF
-where
- "tlF NilF = NilF"
-
-datatype_compat listF
-
-definition Singll ("[[_]]") where
- [simp]: "Singll a \<equiv> Conss a NilF"
-
-primrec appendd (infixr "@@" 65) where
- "NilF @@ ys = ys"
-| "Conss x xs @@ ys = Conss x (xs @@ ys)"
-
-primrec lrev where
- "lrev NilF = NilF"
-| "lrev (Conss y ys) = lrev ys @@ [[y]]"
-
-lemma appendd_NilF[simp]: "xs @@ NilF = xs"
- by (induct xs) auto
-
-lemma appendd_assoc[simp]: "(xs @@ ys) @@ zs = xs @@ ys @@ zs"
- by (induct xs) auto
-
-lemma lrev_appendd[simp]: "lrev (xs @@ ys) = lrev ys @@ lrev xs"
- by (induct xs) auto
-
-lemma listF_map_appendd[simp]:
- "mapF f (xs @@ ys) = mapF f xs @@ mapF f ys"
- by (induct xs) auto
-
-lemma lrev_listF_map[simp]: "lrev (mapF f xs) = mapF f (lrev xs)"
- by (induct xs) auto
-
-lemma lrev_lrev[simp]: "lrev (lrev xs) = xs"
- by (induct xs) auto
-
-primrec lengthh where
- "lengthh NilF = 0"
-| "lengthh (Conss x xs) = Suc (lengthh xs)"
-
-fun nthh where
- "nthh (Conss x xs) 0 = x"
-| "nthh (Conss x xs) (Suc n) = nthh xs n"
-| "nthh xs i = undefined"
-
-lemma lengthh_listF_map[simp]: "lengthh (mapF f xs) = lengthh xs"
- by (induct xs) auto
-
-lemma nthh_listF_map[simp]:
- "i < lengthh xs \<Longrightarrow> nthh (mapF f xs) i = f (nthh xs i)"
- by (induct rule: nthh.induct) auto
-
-lemma nthh_listF_set[simp]: "i < lengthh xs \<Longrightarrow> nthh xs i \<in> set_listF xs"
- by (induct rule: nthh.induct) auto
-
-lemma NilF_iff[iff]: "(lengthh xs = 0) = (xs = NilF)"
- by (induct xs) auto
-
-lemma Conss_iff[iff]:
- "(lengthh xs = Suc n) = (\<exists>y ys. xs = Conss y ys \<and> lengthh ys = n)"
- by (induct xs) auto
-
-lemma Conss_iff'[iff]:
- "(Suc n = lengthh xs) = (\<exists>y ys. xs = Conss y ys \<and> lengthh ys = n)"
- by (induct xs) (simp, simp, blast)
-
-lemma listF_induct2[consumes 1, case_names NilF Conss]: "\<lbrakk>lengthh xs = lengthh ys; P NilF NilF;
- \<And>x xs y ys. P xs ys \<Longrightarrow> P (Conss x xs) (Conss y ys)\<rbrakk> \<Longrightarrow> P xs ys"
- by (induct xs arbitrary: ys) auto
-
-fun zipp where
- "zipp NilF NilF = NilF"
-| "zipp (Conss x xs) (Conss y ys) = Conss (x, y) (zipp xs ys)"
-| "zipp xs ys = undefined"
-
-lemma listF_map_fst_zip[simp]:
- "lengthh xs = lengthh ys \<Longrightarrow> mapF fst (zipp xs ys) = xs"
- by (induct rule: listF_induct2) auto
-
-lemma listF_map_snd_zip[simp]:
- "lengthh xs = lengthh ys \<Longrightarrow> mapF snd (zipp xs ys) = ys"
- by (induct rule: listF_induct2) auto
-
-lemma lengthh_zip[simp]:
- "lengthh xs = lengthh ys \<Longrightarrow> lengthh (zipp xs ys) = lengthh xs"
- by (induct rule: listF_induct2) auto
-
-lemma nthh_zip[simp]:
- assumes "lengthh xs = lengthh ys"
- shows "i < lengthh xs \<Longrightarrow> nthh (zipp xs ys) i = (nthh xs i, nthh ys i)"
-using assms proof (induct arbitrary: i rule: listF_induct2)
- case (Conss x xs y ys) thus ?case by (induct i) auto
-qed simp
-
-lemma list_set_nthh[simp]:
- "(x \<in> set_listF xs) \<Longrightarrow> (\<exists>i < lengthh xs. nthh xs i = x)"
- by (induct xs) (auto, induct rule: nthh.induct, auto)
-
-end
--- a/src/HOL/BNF_Examples/TreeFI.thy Tue Jun 10 21:15:57 2014 +0200
+++ b/src/HOL/BNF_Examples/TreeFI.thy Wed Jun 11 08:58:42 2014 +0200
@@ -9,31 +9,31 @@
header {* Finitely Branching Possibly Infinite Trees *}
theory TreeFI
-imports ListF
+imports Main
begin
-codatatype 'a treeFI = Tree (lab: 'a) (sub: "'a treeFI listF")
+codatatype 'a treeFI = Tree (lab: 'a) (sub: "'a treeFI list")
(* Tree reverse:*)
primcorec trev where
"lab (trev t) = lab t"
-| "sub (trev t) = mapF trev (lrev (sub t))"
+| "sub (trev t) = map trev (rev (sub t))"
lemma treeFI_coinduct:
assumes *: "phi x y"
and step: "\<And>a b. phi a b \<Longrightarrow>
lab a = lab b \<and>
- lengthh (sub a) = lengthh (sub b) \<and>
- (\<forall>i < lengthh (sub a). phi (nthh (sub a) i) (nthh (sub b) i))"
+ length (sub a) = length (sub b) \<and>
+ (\<forall>i < length (sub a). phi (nth (sub a) i) (nth (sub b) i))"
shows "x = y"
using * proof (coinduction arbitrary: x y)
case (Eq_treeFI t1 t2)
from conjunct1[OF conjunct2[OF step[OF Eq_treeFI]]] conjunct2[OF conjunct2[OF step[OF Eq_treeFI]]]
- have "relF phi (sub t1) (sub t2)"
- proof (induction "sub t1" "sub t2" arbitrary: t1 t2 rule: listF_induct2)
- case (Conss x xs y ys)
- note sub = Conss(2,3)[symmetric] and phi = mp[OF spec[OF Conss(4)], unfolded sub]
- and IH = Conss(1)[of "Tree (lab t1) (tlF (sub t1))" "Tree (lab t2) (tlF (sub t2))",
+ have "list_all2 phi (sub t1) (sub t2)"
+ proof (induction "sub t1" "sub t2" arbitrary: t1 t2 rule: list_induct2)
+ case (Cons x xs y ys)
+ note sub = Cons(3,4)[symmetric] and phi = mp[OF spec[OF Cons(5)], unfolded sub]
+ and IH = Cons(2)[of "Tree (lab t1) (tl (sub t1))" "Tree (lab t2) (tl (sub t2))",
unfolded sub, simplified]
from phi[of 0] show ?case unfolding sub by (auto intro!: IH dest: phi[simplified, OF Suc_mono])
qed simp
@@ -41,6 +41,6 @@
qed
lemma trev_trev: "trev (trev tr) = tr"
- by (coinduction arbitrary: tr rule: treeFI_coinduct) auto
+ by (coinduction arbitrary: tr rule: treeFI_coinduct) (auto simp add: rev_map)
end