--- a/src/HOL/Codatatype/Examples/TreeFI.thy Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Examples/TreeFI.thy Fri Sep 21 15:53:29 2012 +0200
@@ -21,29 +21,29 @@
by (auto simp add: listF.set_natural')
(* selectors for trees *)
-definition "lab tr \<equiv> fst (treeFI_unf tr)"
-definition "sub tr \<equiv> snd (treeFI_unf tr)"
+definition "lab tr \<equiv> fst (treeFI_dtor tr)"
+definition "sub tr \<equiv> snd (treeFI_dtor tr)"
-lemma unf[simp]: "treeFI_unf tr = (lab tr, sub tr)"
+lemma dtor[simp]: "treeFI_dtor tr = (lab tr, sub tr)"
unfolding lab_def sub_def by simp
definition pair_fun (infixr "\<odot>" 50) where
"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_coiters pre_treeFI_map_def by simp
+lemma unfold_pair_fun_lab: "lab (treeFI_dtor_unfold (f \<odot> g) t) = f t"
+unfolding lab_def pair_fun_def treeFI.dtor_unfolds 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_coiters pre_treeFI_map_def by simp
+lemma unfold_pair_fun_sub: "sub (treeFI_dtor_unfold (f \<odot> g) t) = listF_map (treeFI_dtor_unfold (f \<odot> g)) (g t)"
+unfolding sub_def pair_fun_def treeFI.dtor_unfolds pre_treeFI_map_def by simp
(* Tree reverse:*)
-definition "trev \<equiv> treeFI_unf_coiter (lab \<odot> lrev o sub)"
+definition "trev \<equiv> treeFI_dtor_unfold (lab \<odot> lrev o sub)"
lemma trev_simps1[simp]: "lab (trev t) = lab t"
-unfolding trev_def by (simp add: coiter_pair_fun_lab)
+unfolding trev_def by (simp add: unfold_pair_fun_lab)
lemma trev_simps2[simp]: "sub (trev t) = listF_map trev (lrev (sub t))"
-unfolding trev_def by (simp add: coiter_pair_fun_sub)
+unfolding trev_def by (simp add: unfold_pair_fun_sub)
lemma treeFI_coinduct:
assumes *: "phi x y"
@@ -52,14 +52,14 @@
lengthh (sub a) = lengthh (sub b) \<and>
(\<forall>i < lengthh (sub a). phi (nthh (sub a) i) (nthh (sub b) i))"
shows "x = y"
-proof (rule mp[OF treeFI.unf_coinduct, of phi, OF _ *])
+proof (rule mp[OF treeFI.dtor_coinduct, of phi, OF _ *])
fix a b :: "'a treeFI"
let ?zs = "zipp (sub a) (sub b)"
let ?z = "(lab a, ?zs)"
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 "pre_treeFI_map id fst ?z = treeFI_unf a" "pre_treeFI_map id snd ?z = treeFI_unf b"
+ hence "pre_treeFI_map id fst ?z = treeFI_dtor a" "pre_treeFI_map id snd ?z = treeFI_dtor b"
unfolding pre_treeFI_map_def by auto
moreover have "\<forall>(x, y) \<in> pre_treeFI_set2 ?z. phi x y"
proof safe
@@ -72,8 +72,8 @@
with step'(3) show "phi z1 z2" by auto
qed
ultimately show "\<exists>z.
- (pre_treeFI_map id fst z = treeFI_unf a \<and>
- pre_treeFI_map id snd z = treeFI_unf b) \<and>
+ (pre_treeFI_map id fst z = treeFI_dtor a \<and>
+ pre_treeFI_map id snd z = treeFI_dtor b) \<and>
(\<forall>x y. (x, y) \<in> pre_treeFI_set2 z \<longrightarrow> phi x y)" by blast
qed