src/HOL/BNF/Examples/TreeFsetI.thy
changeset 49631 9ce0c2cbadb8
parent 49594 55e798614c45
child 50516 ed6b40d15d1c
equal deleted inserted replaced
49629:99700c4e0b33 49631:9ce0c2cbadb8
    13 begin
    13 begin
    14 
    14 
    15 hide_const (open) Sublist.sub
    15 hide_const (open) Sublist.sub
    16 hide_fact (open) Quotient_Product.prod_rel_def
    16 hide_fact (open) Quotient_Product.prod_rel_def
    17 
    17 
       
    18 codata 'a treeFsetI = Tree (lab: 'a) (sub: "'a treeFsetI fset")
       
    19 
    18 definition pair_fun (infixr "\<odot>" 50) where
    20 definition pair_fun (infixr "\<odot>" 50) where
    19   "f \<odot> g \<equiv> \<lambda>x. (f x, g x)"
    21   "f \<odot> g \<equiv> \<lambda>x. (f x, g x)"
    20 
    22 
    21 codata_raw treeFsetI: 't = "'a \<times> 't fset"
    23 (* tree map (contrived example): *)
       
    24 definition tmap where
       
    25 "tmap f = treeFsetI_unfold (f o lab) sub"
    22 
    26 
    23 (* selectors for trees *)
    27 lemma tmap_simps[simp]:
    24 definition "lab t \<equiv> fst (treeFsetI_dtor t)"
    28 "lab (tmap f t) = f (lab t)"
    25 definition "sub t \<equiv> snd (treeFsetI_dtor t)"
    29 "sub (tmap f t) = map_fset (tmap f) (sub t)"
    26 
    30 unfolding tmap_def treeFsetI.sel_unfold by simp+
    27 lemma dtor[simp]: "treeFsetI_dtor t = (lab t, sub t)"
       
    28 unfolding lab_def sub_def by simp
       
    29 
       
    30 lemma unfold_pair_fun_lab: "lab (treeFsetI_dtor_unfold (f \<odot> g) t) = f t"
       
    31 unfolding lab_def pair_fun_def treeFsetI.dtor_unfold pre_treeFsetI_map_def by simp
       
    32 
       
    33 lemma unfold_pair_fun_sub: "sub (treeFsetI_dtor_unfold (f \<odot> g) t) = map_fset (treeFsetI_dtor_unfold (f \<odot> g)) (g t)"
       
    34 unfolding sub_def pair_fun_def treeFsetI.dtor_unfold pre_treeFsetI_map_def by simp
       
    35 
       
    36 (* tree map (contrived example): *)
       
    37 definition "tmap f \<equiv> treeFsetI_dtor_unfold (f o lab \<odot> sub)"
       
    38 
       
    39 lemma tmap_simps1[simp]: "lab (tmap f t) = f (lab t)"
       
    40 unfolding tmap_def by (simp add: unfold_pair_fun_lab)
       
    41 
       
    42 lemma trev_simps2[simp]: "sub (tmap f t) = map_fset (tmap f) (sub t)"
       
    43 unfolding tmap_def by (simp add: unfold_pair_fun_sub)
       
    44 
       
    45 lemma pre_treeFsetI_rel[simp]: "pre_treeFsetI_rel R1 R2 a b = (R1 (fst a) (fst b) \<and>
       
    46   (\<forall>t \<in> fset (snd a). (\<exists>u \<in> fset (snd b). R2 t u)) \<and>
       
    47   (\<forall>t \<in> fset (snd b). (\<exists>u \<in> fset (snd a). R2 u t)))"
       
    48 apply (cases a)
       
    49 apply (cases b)
       
    50 apply (simp add: pre_treeFsetI_rel_def prod_rel_def fset_rel_def)
       
    51 done
       
    52 
       
    53 lemmas treeFsetI_coind = mp[OF treeFsetI.dtor_coinduct]
       
    54 
    31 
    55 lemma "tmap (f o g) x = tmap f (tmap g x)"
    32 lemma "tmap (f o g) x = tmap f (tmap g x)"
    56 by (intro treeFsetI_coind[where P="%x1 x2. \<exists>x. x1 = tmap (f o g) x \<and> x2 = tmap f (tmap g x)"])
    33 apply (rule treeFsetI.coinduct[of "%x1 x2. \<exists>x. x1 = tmap (f o g) x \<and> x2 = tmap f (tmap g x)"])
    57    force+
    34 apply auto
       
    35 apply (unfold fset_rel_def)
       
    36 by auto
    58 
    37 
    59 end
    38 end