src/HOL/Codatatype/Examples/TreeFsetI.thy
changeset 49508 1e205327f059
parent 49463 83ac281bcdc2
child 49509 163914705f8d
--- a/src/HOL/Codatatype/Examples/TreeFsetI.thy	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Examples/TreeFsetI.thy	Fri Sep 21 15:53:29 2012 +0200
@@ -13,7 +13,7 @@
 begin
 
 hide_const (open) Sublist.sub
-hide_fact (open) Quotient_Product.prod_pred_def
+hide_fact (open) Quotient_Product.prod_rel_def
 
 definition pair_fun (infixr "\<odot>" 50) where
   "f \<odot> g \<equiv> \<lambda>x. (f x, g x)"
@@ -21,36 +21,36 @@
 codata_raw treeFsetI: 't = "'a \<times> 't fset"
 
 (* selectors for trees *)
-definition "lab t \<equiv> fst (treeFsetI_unf t)"
-definition "sub t \<equiv> snd (treeFsetI_unf t)"
+definition "lab t \<equiv> fst (treeFsetI_dtor t)"
+definition "sub t \<equiv> snd (treeFsetI_dtor t)"
 
-lemma unf[simp]: "treeFsetI_unf t = (lab t, sub t)"
+lemma dtor[simp]: "treeFsetI_dtor t = (lab t, sub t)"
 unfolding lab_def sub_def by simp
 
-lemma coiter_pair_fun_lab: "lab (treeFsetI_unf_coiter (f \<odot> g) t) = f t"
-unfolding lab_def pair_fun_def treeFsetI.unf_coiters pre_treeFsetI_map_def by simp
+lemma unfold_pair_fun_lab: "lab (treeFsetI_dtor_unfold (f \<odot> g) t) = f t"
+unfolding lab_def pair_fun_def treeFsetI.dtor_unfolds pre_treeFsetI_map_def by simp
 
-lemma coiter_pair_fun_sub: "sub (treeFsetI_unf_coiter (f \<odot> g) t) = map_fset (treeFsetI_unf_coiter (f \<odot> g)) (g t)"
-unfolding sub_def pair_fun_def treeFsetI.unf_coiters pre_treeFsetI_map_def by simp
+lemma unfold_pair_fun_sub: "sub (treeFsetI_dtor_unfold (f \<odot> g) t) = map_fset (treeFsetI_dtor_unfold (f \<odot> g)) (g t)"
+unfolding sub_def pair_fun_def treeFsetI.dtor_unfolds pre_treeFsetI_map_def by simp
 
 (* tree map (contrived example): *)
-definition "tmap f \<equiv> treeFsetI_unf_coiter (f o lab \<odot> sub)"
+definition "tmap f \<equiv> treeFsetI_dtor_unfold (f o lab \<odot> sub)"
 
 lemma tmap_simps1[simp]: "lab (tmap f t) = f (lab t)"
-unfolding tmap_def by (simp add: coiter_pair_fun_lab)
+unfolding tmap_def by (simp add: unfold_pair_fun_lab)
 
 lemma trev_simps2[simp]: "sub (tmap f t) = map_fset (tmap f) (sub t)"
-unfolding tmap_def by (simp add: coiter_pair_fun_sub)
+unfolding tmap_def by (simp add: unfold_pair_fun_sub)
 
-lemma pre_treeFsetI_pred[simp]: "pre_treeFsetI_pred R1 R2 a b = (R1 (fst a) (fst b) \<and>
+lemma pre_treeFsetI_rel[simp]: "pre_treeFsetI_rel R1 R2 a b = (R1 (fst a) (fst b) \<and>
   (\<forall>t \<in> fset (snd a). (\<exists>u \<in> fset (snd b). R2 t u)) \<and>
   (\<forall>t \<in> fset (snd b). (\<exists>u \<in> fset (snd a). R2 u t)))"
 apply (cases a)
 apply (cases b)
-apply (simp add: pre_treeFsetI_pred_def prod_pred_def fset_pred_def)
+apply (simp add: pre_treeFsetI_rel_def prod_rel_def fset_rel_def)
 done
 
-lemmas treeFsetI_coind = mp[OF treeFsetI.pred_coinduct]
+lemmas treeFsetI_coind = mp[OF treeFsetI.rel_coinduct]
 
 lemma "tmap (f o g) x = tmap f (tmap g x)"
 by (intro treeFsetI_coind[where P="%x1 x2. \<exists>x. x1 = tmap (f o g) x \<and> x2 = tmap f (tmap g x)"])