src/HOL/Codatatype/BNF_Comp.thy
author blanchet
Mon Sep 17 21:33:12 2012 +0200 (2012-09-17)
changeset 49430 6df729c6a1a6
parent 49312 c874ff5658dc
child 49463 83ac281bcdc2
permissions -rw-r--r--
tuned simpset
     1 (*  Title:      HOL/Codatatype/BNF_Comp.thy
     2     Author:     Dmitriy Traytel, TU Muenchen
     3     Copyright   2012
     4 
     5 Composition of bounded natural functors.
     6 *)
     7 
     8 header {* Composition of Bounded Natural Functors *}
     9 
    10 theory BNF_Comp
    11 imports Basic_BNFs
    12 begin
    13 
    14 lemma empty_natural: "(\<lambda>_. {}) o f = image g o (\<lambda>_. {})"
    15 by (rule ext) simp
    16 
    17 lemma Union_natural: "Union o image (image f) = image f o Union"
    18 by (rule ext) (auto simp only: o_apply)
    19 
    20 lemma in_Union_o_assoc: "x \<in> (Union o gset o gmap) A \<Longrightarrow> x \<in> (Union o (gset o gmap)) A"
    21 by (unfold o_assoc)
    22 
    23 lemma comp_single_set_bd:
    24   assumes fbd_Card_order: "Card_order fbd" and
    25     fset_bd: "\<And>x. |fset x| \<le>o fbd" and
    26     gset_bd: "\<And>x. |gset x| \<le>o gbd"
    27   shows "|\<Union>fset ` gset x| \<le>o gbd *c fbd"
    28 apply (subst sym[OF SUP_def])
    29 apply (rule ordLeq_transitive)
    30 apply (rule card_of_UNION_Sigma)
    31 apply (subst SIGMA_CSUM)
    32 apply (rule ordLeq_transitive)
    33 apply (rule card_of_Csum_Times')
    34 apply (rule fbd_Card_order)
    35 apply (rule ballI)
    36 apply (rule fset_bd)
    37 apply (rule ordLeq_transitive)
    38 apply (rule cprod_mono1)
    39 apply (rule gset_bd)
    40 apply (rule ordIso_imp_ordLeq)
    41 apply (rule ordIso_refl)
    42 apply (rule Card_order_cprod)
    43 done
    44 
    45 lemma Union_image_insert: "\<Union>f ` insert a B = f a \<union> \<Union>f ` B"
    46 by simp
    47 
    48 lemma Union_image_empty: "A \<union> \<Union>f ` {} = A"
    49 by simp
    50 
    51 lemma image_o_collect: "collect ((\<lambda>f. image g o f) ` F) = image g o collect F"
    52 by (rule ext) (auto simp add: collect_def)
    53 
    54 lemma conj_subset_def: "A \<subseteq> {x. P x \<and> Q x} = (A \<subseteq> {x. P x} \<and> A \<subseteq> {x. Q x})"
    55 by blast
    56 
    57 lemma UN_image_subset: "\<Union>f ` g x \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})"
    58 by blast
    59 
    60 lemma comp_set_bd_Union_o_collect: "|\<Union>\<Union>(\<lambda>f. f x) ` X| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd"
    61 by (unfold o_apply collect_def SUP_def)
    62 
    63 lemma wpull_cong:
    64 "\<lbrakk>A' = A; B1' = B1; B2' = B2; wpull A B1 B2 f1 f2 p1 p2\<rbrakk> \<Longrightarrow> wpull A' B1' B2' f1 f2 p1 p2"
    65 by simp
    66 
    67 lemma Id_def': "Id = {(a,b). a = b}"
    68 by auto
    69 
    70 lemma Gr_fst_snd: "(Gr R fst)^-1 O Gr R snd = R"
    71 unfolding Gr_def by auto
    72 
    73 lemma subst_rel_def: "A = B \<Longrightarrow> (Gr A f)^-1 O Gr A g = (Gr B f)^-1 O Gr B g"
    74 by simp
    75 
    76 lemma abs_pred_def: "\<lbrakk>\<And>x y. (x, y) \<in> rel = pred x y\<rbrakk> \<Longrightarrow> rel = Collect (split pred)"
    77 by auto
    78 
    79 lemma Collect_split_cong: "Collect (split pred) = Collect (split pred') \<Longrightarrow> pred = pred'"
    80 by blast
    81 
    82 lemma pred_def_abs: "rel = Collect (split pred) \<Longrightarrow> pred = (\<lambda>x y. (x, y) \<in> rel)"
    83 by auto
    84 
    85 ML_file "Tools/bnf_comp_tactics.ML"
    86 ML_file "Tools/bnf_comp.ML"
    87 
    88 end