--- a/src/HOL/Codatatype/Examples/TreeFI.thy Sat Sep 08 21:04:26 2012 +0200
+++ b/src/HOL/Codatatype/Examples/TreeFI.thy Sat Sep 08 21:04:27 2012 +0200
@@ -16,8 +16,8 @@
codata_raw treeFI: 'tree = "'a \<times> 'tree listF"
-lemma treeFIBNF_listF_set[simp]: "treeFIBNF_set2 (i, xs) = listF_set xs"
-unfolding treeFIBNF_set2_def collect_def[abs_def] prod_set_defs
+lemma pre_treeFI_listF_set[simp]: "pre_treeFI_set2 (i, xs) = listF_set xs"
+unfolding pre_treeFI_set2_def collect_def[abs_def] prod_set_defs
by (auto simp add: listF.set_natural')
(* selectors for trees *)
@@ -31,10 +31,10 @@
"f \<odot> g \<equiv> \<lambda>x. (f x, g x)"
lemma coiter_pair_fun_lab: "lab (treeFI_unf_coiter (f \<odot> g) t) = f t"
-unfolding lab_def pair_fun_def treeFI.unf_coiter treeFIBNF_map_def by simp
+unfolding lab_def pair_fun_def treeFI.unf_coiter pre_treeFI_map_def by simp
lemma coiter_pair_fun_sub: "sub (treeFI_unf_coiter (f \<odot> g) t) = listF_map (treeFI_unf_coiter (f \<odot> g)) (g t)"
-unfolding sub_def pair_fun_def treeFI.unf_coiter treeFIBNF_map_def by simp
+unfolding sub_def pair_fun_def treeFI.unf_coiter pre_treeFI_map_def by simp
(* Tree reverse:*)
definition "trev \<equiv> treeFI_unf_coiter (lab \<odot> lrev o sub)"
@@ -59,12 +59,12 @@
assume "phi a b"
with step have step': "lab a = lab b" "lengthh (sub a) = lengthh (sub b)"
"\<forall>i < lengthh (sub a). phi (nthh (sub a) i) (nthh (sub b) i)" by auto
- hence "treeFIBNF_map id fst ?z = treeFI_unf a" "treeFIBNF_map id snd ?z = treeFI_unf b"
- unfolding treeFIBNF_map_def by auto
- moreover have "\<forall>(x, y) \<in> treeFIBNF_set2 ?z. phi x y"
+ hence "pre_treeFI_map id fst ?z = treeFI_unf a" "pre_treeFI_map id snd ?z = treeFI_unf b"
+ unfolding pre_treeFI_map_def by auto
+ moreover have "\<forall>(x, y) \<in> pre_treeFI_set2 ?z. phi x y"
proof safe
fix z1 z2
- assume "(z1, z2) \<in> treeFIBNF_set2 ?z"
+ assume "(z1, z2) \<in> pre_treeFI_set2 ?z"
hence "(z1, z2) \<in> listF_set ?zs" by auto
hence "\<exists>i < lengthh ?zs. nthh ?zs i = (z1, z2)" by auto
with step'(2) obtain i where "i < lengthh (sub a)"
@@ -72,9 +72,9 @@
with step'(3) show "phi z1 z2" by auto
qed
ultimately show "\<exists>z.
- (treeFIBNF_map id fst z = treeFI_unf a \<and>
- treeFIBNF_map id snd z = treeFI_unf b) \<and>
- (\<forall>x y. (x, y) \<in> treeFIBNF_set2 z \<longrightarrow> phi x y)" by blast
+ (pre_treeFI_map id fst z = treeFI_unf a \<and>
+ pre_treeFI_map id snd z = treeFI_unf b) \<and>
+ (\<forall>x y. (x, y) \<in> pre_treeFI_set2 z \<longrightarrow> phi x y)" by blast
qed
lemma trev_trev: "trev (trev tr) = tr"