# HG changeset patch
# User blanchet
# Date 1402469922 -7200
# Node ID df0f8ad7cc30c027a0fc1fb36ed066026ef7fe22
# Parent  d9be905d62833944df1ac5929bb6cfe4063198f3
got rid of 'listF' example, which is now subsumed by the real 'list' type

diff -r d9be905d6283 -r df0f8ad7cc30 src/HOL/BNF_Examples/Koenig.thy
--- 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
diff -r d9be905d6283 -r df0f8ad7cc30 src/HOL/BNF_Examples/ListF.thy
--- 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
diff -r d9be905d6283 -r df0f8ad7cc30 src/HOL/BNF_Examples/TreeFI.thy
--- 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