src/HOL/BNF_Comp.thy
author haftmann
Sun Mar 16 18:09:04 2014 +0100 (2014-03-16)
changeset 56166 9a241bc276cd
parent 56016 8875cdcfc85b
child 57698 afef6616cbae
permissions -rw-r--r--
normalising simp rules for compound operators
blanchet@55059
     1
(*  Title:      HOL/BNF_Comp.thy
blanchet@48975
     2
    Author:     Dmitriy Traytel, TU Muenchen
blanchet@48975
     3
    Copyright   2012
blanchet@48975
     4
blanchet@48975
     5
Composition of bounded natural functors.
blanchet@48975
     6
*)
blanchet@48975
     7
blanchet@48975
     8
header {* Composition of Bounded Natural Functors *}
blanchet@48975
     9
blanchet@48975
    10
theory BNF_Comp
traytel@55936
    11
imports BNF_Def
blanchet@48975
    12
begin
blanchet@48975
    13
blanchet@49312
    14
lemma empty_natural: "(\<lambda>_. {}) o f = image g o (\<lambda>_. {})"
blanchet@49312
    15
by (rule ext) simp
blanchet@49312
    16
blanchet@49312
    17
lemma Union_natural: "Union o image (image f) = image f o Union"
blanchet@55066
    18
by (rule ext) (auto simp only: comp_apply)
blanchet@49312
    19
blanchet@49312
    20
lemma in_Union_o_assoc: "x \<in> (Union o gset o gmap) A \<Longrightarrow> x \<in> (Union o (gset o gmap)) A"
blanchet@55066
    21
by (unfold comp_assoc)
blanchet@49312
    22
blanchet@49312
    23
lemma comp_single_set_bd:
blanchet@49312
    24
  assumes fbd_Card_order: "Card_order fbd" and
blanchet@49312
    25
    fset_bd: "\<And>x. |fset x| \<le>o fbd" and
blanchet@49312
    26
    gset_bd: "\<And>x. |gset x| \<le>o gbd"
haftmann@52141
    27
  shows "|\<Union>(fset ` gset x)| \<le>o gbd *c fbd"
haftmann@56166
    28
apply simp
blanchet@49312
    29
apply (rule ordLeq_transitive)
blanchet@49312
    30
apply (rule card_of_UNION_Sigma)
blanchet@49312
    31
apply (subst SIGMA_CSUM)
blanchet@49312
    32
apply (rule ordLeq_transitive)
blanchet@49312
    33
apply (rule card_of_Csum_Times')
blanchet@49312
    34
apply (rule fbd_Card_order)
blanchet@49312
    35
apply (rule ballI)
blanchet@49312
    36
apply (rule fset_bd)
blanchet@49312
    37
apply (rule ordLeq_transitive)
blanchet@49312
    38
apply (rule cprod_mono1)
blanchet@49312
    39
apply (rule gset_bd)
blanchet@49312
    40
apply (rule ordIso_imp_ordLeq)
blanchet@49312
    41
apply (rule ordIso_refl)
blanchet@49312
    42
apply (rule Card_order_cprod)
blanchet@49312
    43
done
blanchet@49312
    44
traytel@55935
    45
lemma csum_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p +c p' =o r +c r \<Longrightarrow> p +c p' =o r"
traytel@55935
    46
apply (erule ordIso_transitive)
traytel@55935
    47
apply (frule csum_absorb2')
traytel@55935
    48
apply (erule ordLeq_refl)
traytel@55935
    49
by simp
traytel@55935
    50
traytel@55935
    51
lemma cprod_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p *c p' =o r *c r \<Longrightarrow> p *c p' =o r"
traytel@55935
    52
apply (erule ordIso_transitive)
traytel@55935
    53
apply (rule cprod_infinite)
traytel@55935
    54
by simp
traytel@55935
    55
haftmann@52141
    56
lemma Union_image_insert: "\<Union>(f ` insert a B) = f a \<union> \<Union>(f ` B)"
blanchet@49312
    57
by simp
blanchet@49312
    58
haftmann@52141
    59
lemma Union_image_empty: "A \<union> \<Union>(f ` {}) = A"
blanchet@49312
    60
by simp
blanchet@49312
    61
blanchet@49312
    62
lemma image_o_collect: "collect ((\<lambda>f. image g o f) ` F) = image g o collect F"
blanchet@49312
    63
by (rule ext) (auto simp add: collect_def)
blanchet@49312
    64
blanchet@49312
    65
lemma conj_subset_def: "A \<subseteq> {x. P x \<and> Q x} = (A \<subseteq> {x. P x} \<and> A \<subseteq> {x. Q x})"
blanchet@49312
    66
by blast
blanchet@49312
    67
haftmann@52141
    68
lemma UN_image_subset: "\<Union>(f ` g x) \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})"
blanchet@49312
    69
by blast
blanchet@49312
    70
haftmann@52141
    71
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"
haftmann@56166
    72
by (unfold comp_apply collect_def) simp
blanchet@49312
    73
blanchet@49312
    74
lemma wpull_cong:
blanchet@49312
    75
"\<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"
blanchet@49312
    76
by simp
blanchet@49312
    77
traytel@51893
    78
lemma Grp_fst_snd: "(Grp (Collect (split R)) fst)^--1 OO Grp (Collect (split R)) snd = R"
traytel@51893
    79
unfolding Grp_def fun_eq_iff relcompp.simps by auto
traytel@51893
    80
traytel@51893
    81
lemma OO_Grp_cong: "A = B \<Longrightarrow> (Grp A f)^--1 OO Grp A g = (Grp B f)^--1 OO Grp B g"
blanchet@55705
    82
by (rule arg_cong)
traytel@51893
    83
traytel@55803
    84
lemma vimage2p_relcompp_mono: "R OO S \<le> T \<Longrightarrow>
traytel@55803
    85
  vimage2p f g R OO vimage2p g h S \<le> vimage2p f h T"
traytel@55803
    86
  unfolding vimage2p_def by auto
traytel@55803
    87
traytel@55803
    88
lemma type_copy_map_cong0: "M (g x) = N (h x) \<Longrightarrow> (f o M o g) x = (f o N o h) x"
traytel@55803
    89
  by auto
traytel@55803
    90
traytel@55803
    91
lemma type_copy_set_bd: "(\<And>y. |S y| \<le>o bd) \<Longrightarrow> |(S o Rep) x| \<le>o bd"
traytel@55803
    92
  by auto
traytel@55803
    93
traytel@55803
    94
lemma vimage2p_cong: "R = S \<Longrightarrow> vimage2p f g R = vimage2p f g S"
traytel@55803
    95
  by simp
traytel@55803
    96
traytel@55803
    97
context
traytel@55803
    98
fixes Rep Abs
traytel@55803
    99
assumes type_copy: "type_definition Rep Abs UNIV"
traytel@55803
   100
begin
traytel@55803
   101
traytel@55803
   102
lemma type_copy_map_id0: "M = id \<Longrightarrow> Abs o M o Rep = id"
traytel@55803
   103
  using type_definition.Rep_inverse[OF type_copy] by auto
traytel@55811
   104
traytel@55803
   105
lemma type_copy_map_comp0: "M = M1 o M2 \<Longrightarrow> f o M o g = (f o M1 o Rep) o (Abs o M2 o g)"
traytel@55803
   106
  using type_definition.Abs_inverse[OF type_copy UNIV_I] by auto
traytel@55811
   107
traytel@55803
   108
lemma type_copy_set_map0: "S o M = image f o S' \<Longrightarrow> (S o Rep) o (Abs o M o g) = image f o (S' o g)"
traytel@55803
   109
  using type_definition.Abs_inverse[OF type_copy UNIV_I] by (auto simp: o_def fun_eq_iff)
traytel@55811
   110
traytel@55803
   111
lemma type_copy_wit: "x \<in> (S o Rep) (Abs y) \<Longrightarrow> x \<in> S y"
traytel@55803
   112
  using type_definition.Abs_inverse[OF type_copy UNIV_I] by auto
traytel@55811
   113
traytel@55803
   114
lemma type_copy_vimage2p_Grp_Rep: "vimage2p f Rep (Grp (Collect P) h) =
traytel@55803
   115
    Grp (Collect (\<lambda>x. P (f x))) (Abs o h o f)"
traytel@55803
   116
  unfolding vimage2p_def Grp_def fun_eq_iff
traytel@55803
   117
  by (auto simp: type_definition.Abs_inverse[OF type_copy UNIV_I]
traytel@55803
   118
   type_definition.Rep_inverse[OF type_copy] dest: sym)
traytel@55811
   119
traytel@55803
   120
lemma type_copy_vimage2p_Grp_Abs:
traytel@55803
   121
  "\<And>h. vimage2p g Abs (Grp (Collect P) h) = Grp (Collect (\<lambda>x. P (g x))) (Rep o h o g)"
traytel@55803
   122
  unfolding vimage2p_def Grp_def fun_eq_iff
traytel@55803
   123
  by (auto simp: type_definition.Abs_inverse[OF type_copy UNIV_I]
traytel@55803
   124
   type_definition.Rep_inverse[OF type_copy] dest: sym)
traytel@55811
   125
traytel@55811
   126
lemma type_copy_ex_RepI: "(\<exists>b. F b) = (\<exists>b. F (Rep b))"
traytel@55811
   127
proof safe
traytel@55811
   128
  fix b assume "F b"
traytel@55811
   129
  show "\<exists>b'. F (Rep b')"
traytel@55811
   130
  proof (rule exI)
traytel@55811
   131
    from `F b` show "F (Rep (Abs b))" using type_definition.Abs_inverse[OF type_copy] by auto
traytel@55811
   132
  qed
traytel@55811
   133
qed blast
traytel@55811
   134
traytel@55803
   135
lemma vimage2p_relcompp_converse:
traytel@55803
   136
  "vimage2p f g (R^--1 OO S) = (vimage2p Rep f R)^--1 OO vimage2p Rep g S"
traytel@55803
   137
  unfolding vimage2p_def relcompp.simps conversep.simps fun_eq_iff image_def
traytel@55811
   138
  by (auto simp: type_copy_ex_RepI)
traytel@55803
   139
traytel@55803
   140
end
traytel@55803
   141
traytel@55935
   142
bnf DEADID: 'a
traytel@55935
   143
  map: "id :: 'a \<Rightarrow> 'a"
traytel@55935
   144
  bd: natLeq
traytel@55935
   145
  rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
traytel@55935
   146
by (auto simp add: Grp_def natLeq_card_order natLeq_cinfinite)
traytel@55935
   147
traytel@55935
   148
definition id_bnf_comp :: "'a \<Rightarrow> 'a" where "id_bnf_comp \<equiv> (\<lambda>x. x)"
traytel@55935
   149
traytel@56016
   150
lemma id_bnf_comp_apply: "id_bnf_comp x = x"
traytel@56016
   151
  unfolding id_bnf_comp_def by simp
traytel@56016
   152
traytel@55935
   153
bnf ID: 'a
traytel@55935
   154
  map: "id_bnf_comp :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
traytel@55935
   155
  sets: "\<lambda>x. {x}"
traytel@55935
   156
  bd: natLeq
traytel@55935
   157
  rel: "id_bnf_comp :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
traytel@55935
   158
unfolding id_bnf_comp_def
traytel@55935
   159
apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite)
traytel@55935
   160
apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
traytel@55935
   161
apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3]
traytel@55935
   162
done
blanchet@55854
   163
blanchet@55855
   164
lemma type_definition_id_bnf_comp_UNIV: "type_definition id_bnf_comp id_bnf_comp UNIV"
blanchet@55855
   165
  unfolding id_bnf_comp_def by unfold_locales auto
blanchet@55854
   166
blanchet@55062
   167
ML_file "Tools/BNF/bnf_comp_tactics.ML"
blanchet@55062
   168
ML_file "Tools/BNF/bnf_comp.ML"
blanchet@49309
   169
blanchet@55873
   170
hide_const (open) id_bnf_comp
blanchet@55873
   171
hide_fact (open) id_bnf_comp_def type_definition_id_bnf_comp_UNIV
blanchet@55854
   172
blanchet@48975
   173
end