src/HOL/BNF_Composition.thy
author wenzelm
Tue Oct 10 19:23:03 2017 +0200 (23 months ago)
changeset 66831 29ea2b900a05
parent 62777 596baa1a3251
child 67091 1393c2340eec
permissions -rw-r--r--
tuned: each session has at most one defining entry;
blanchet@58128
     1
(*  Title:      HOL/BNF_Composition.thy
blanchet@48975
     2
    Author:     Dmitriy Traytel, TU Muenchen
blanchet@57698
     3
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@57698
     4
    Copyright   2012, 2013, 2014
blanchet@48975
     5
blanchet@48975
     6
Composition of bounded natural functors.
blanchet@48975
     7
*)
blanchet@48975
     8
wenzelm@60758
     9
section \<open>Composition of Bounded Natural Functors\<close>
blanchet@48975
    10
blanchet@58128
    11
theory BNF_Composition
traytel@55936
    12
imports BNF_Def
traytel@60918
    13
keywords
traytel@60918
    14
  "copy_bnf" :: thy_decl and
traytel@60918
    15
  "lift_bnf" :: thy_goal
blanchet@48975
    16
begin
blanchet@48975
    17
traytel@60918
    18
lemma ssubst_mem: "\<lbrakk>t = s; s \<in> X\<rbrakk> \<Longrightarrow> t \<in> X"
traytel@60918
    19
  by simp
traytel@60918
    20
blanchet@49312
    21
lemma empty_natural: "(\<lambda>_. {}) o f = image g o (\<lambda>_. {})"
blanchet@58128
    22
  by (rule ext) simp
blanchet@49312
    23
blanchet@49312
    24
lemma Union_natural: "Union o image (image f) = image f o Union"
blanchet@58128
    25
  by (rule ext) (auto simp only: comp_apply)
blanchet@49312
    26
blanchet@49312
    27
lemma in_Union_o_assoc: "x \<in> (Union o gset o gmap) A \<Longrightarrow> x \<in> (Union o (gset o gmap)) A"
blanchet@58128
    28
  by (unfold comp_assoc)
blanchet@49312
    29
blanchet@49312
    30
lemma comp_single_set_bd:
blanchet@49312
    31
  assumes fbd_Card_order: "Card_order fbd" and
blanchet@49312
    32
    fset_bd: "\<And>x. |fset x| \<le>o fbd" and
blanchet@49312
    33
    gset_bd: "\<And>x. |gset x| \<le>o gbd"
haftmann@52141
    34
  shows "|\<Union>(fset ` gset x)| \<le>o gbd *c fbd"
blanchet@58128
    35
  apply simp
blanchet@58128
    36
  apply (rule ordLeq_transitive)
blanchet@58128
    37
  apply (rule card_of_UNION_Sigma)
blanchet@58128
    38
  apply (subst SIGMA_CSUM)
blanchet@58128
    39
  apply (rule ordLeq_transitive)
blanchet@58128
    40
  apply (rule card_of_Csum_Times')
blanchet@58128
    41
  apply (rule fbd_Card_order)
blanchet@58128
    42
  apply (rule ballI)
blanchet@58128
    43
  apply (rule fset_bd)
blanchet@58128
    44
  apply (rule ordLeq_transitive)
blanchet@58128
    45
  apply (rule cprod_mono1)
blanchet@58128
    46
  apply (rule gset_bd)
blanchet@58128
    47
  apply (rule ordIso_imp_ordLeq)
blanchet@58128
    48
  apply (rule ordIso_refl)
blanchet@58128
    49
  apply (rule Card_order_cprod)
blanchet@58128
    50
  done
blanchet@49312
    51
traytel@55935
    52
lemma csum_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p +c p' =o r +c r \<Longrightarrow> p +c p' =o r"
blanchet@58128
    53
  apply (erule ordIso_transitive)
blanchet@58128
    54
  apply (frule csum_absorb2')
blanchet@58128
    55
  apply (erule ordLeq_refl)
blanchet@58128
    56
  by simp
traytel@55935
    57
traytel@55935
    58
lemma cprod_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p *c p' =o r *c r \<Longrightarrow> p *c p' =o r"
blanchet@58128
    59
  apply (erule ordIso_transitive)
blanchet@58128
    60
  apply (rule cprod_infinite)
blanchet@58128
    61
  by simp
traytel@55935
    62
haftmann@52141
    63
lemma Union_image_insert: "\<Union>(f ` insert a B) = f a \<union> \<Union>(f ` B)"
blanchet@58128
    64
  by simp
blanchet@49312
    65
haftmann@52141
    66
lemma Union_image_empty: "A \<union> \<Union>(f ` {}) = A"
blanchet@58128
    67
  by simp
blanchet@49312
    68
blanchet@49312
    69
lemma image_o_collect: "collect ((\<lambda>f. image g o f) ` F) = image g o collect F"
blanchet@58128
    70
  by (rule ext) (auto simp add: collect_def)
blanchet@49312
    71
blanchet@49312
    72
lemma conj_subset_def: "A \<subseteq> {x. P x \<and> Q x} = (A \<subseteq> {x. P x} \<and> A \<subseteq> {x. Q x})"
blanchet@58128
    73
  by blast
blanchet@49312
    74
haftmann@52141
    75
lemma UN_image_subset: "\<Union>(f ` g x) \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})"
blanchet@58128
    76
  by blast
blanchet@49312
    77
haftmann@52141
    78
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"
blanchet@58128
    79
  by (unfold comp_apply collect_def) simp
blanchet@49312
    80
traytel@62324
    81
lemma Collect_inj: "Collect P = Collect Q \<Longrightarrow> P = Q"
traytel@62324
    82
  by blast
traytel@62324
    83
haftmann@61032
    84
lemma Grp_fst_snd: "(Grp (Collect (case_prod R)) fst)^--1 OO Grp (Collect (case_prod R)) snd = R"
blanchet@58128
    85
  unfolding Grp_def fun_eq_iff relcompp.simps by auto
traytel@51893
    86
traytel@51893
    87
lemma OO_Grp_cong: "A = B \<Longrightarrow> (Grp A f)^--1 OO Grp A g = (Grp B f)^--1 OO Grp B g"
blanchet@58128
    88
  by (rule arg_cong)
traytel@51893
    89
traytel@55803
    90
lemma vimage2p_relcompp_mono: "R OO S \<le> T \<Longrightarrow>
traytel@55803
    91
  vimage2p f g R OO vimage2p g h S \<le> vimage2p f h T"
traytel@55803
    92
  unfolding vimage2p_def by auto
traytel@55803
    93
traytel@55803
    94
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
    95
  by auto
traytel@55803
    96
traytel@55803
    97
lemma type_copy_set_bd: "(\<And>y. |S y| \<le>o bd) \<Longrightarrow> |(S o Rep) x| \<le>o bd"
traytel@55803
    98
  by auto
traytel@55803
    99
traytel@55803
   100
lemma vimage2p_cong: "R = S \<Longrightarrow> vimage2p f g R = vimage2p f g S"
traytel@55803
   101
  by simp
traytel@55803
   102
traytel@62324
   103
lemma Ball_comp_iff: "(\<lambda>x. Ball (A x) f) o g = (\<lambda>x. Ball ((A o g) x) f)"
traytel@62324
   104
  unfolding o_def by auto
traytel@62324
   105
traytel@62324
   106
lemma conj_comp_iff: "(\<lambda>x. P x \<and> Q x) o g = (\<lambda>x. (P o g) x \<and> (Q o g) x)"
traytel@62324
   107
  unfolding o_def by auto
traytel@62324
   108
traytel@55803
   109
context
blanchet@58128
   110
  fixes Rep Abs
blanchet@58128
   111
  assumes type_copy: "type_definition Rep Abs UNIV"
traytel@55803
   112
begin
traytel@55803
   113
traytel@55803
   114
lemma type_copy_map_id0: "M = id \<Longrightarrow> Abs o M o Rep = id"
traytel@55803
   115
  using type_definition.Rep_inverse[OF type_copy] by auto
traytel@55811
   116
traytel@55803
   117
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
   118
  using type_definition.Abs_inverse[OF type_copy UNIV_I] by auto
traytel@55811
   119
traytel@55803
   120
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
   121
  using type_definition.Abs_inverse[OF type_copy UNIV_I] by (auto simp: o_def fun_eq_iff)
traytel@55811
   122
traytel@55803
   123
lemma type_copy_wit: "x \<in> (S o Rep) (Abs y) \<Longrightarrow> x \<in> S y"
traytel@55803
   124
  using type_definition.Abs_inverse[OF type_copy UNIV_I] by auto
traytel@55811
   125
traytel@55803
   126
lemma type_copy_vimage2p_Grp_Rep: "vimage2p f Rep (Grp (Collect P) h) =
traytel@55803
   127
    Grp (Collect (\<lambda>x. P (f x))) (Abs o h o f)"
traytel@55803
   128
  unfolding vimage2p_def Grp_def fun_eq_iff
traytel@55803
   129
  by (auto simp: type_definition.Abs_inverse[OF type_copy UNIV_I]
traytel@55803
   130
   type_definition.Rep_inverse[OF type_copy] dest: sym)
traytel@55811
   131
traytel@55803
   132
lemma type_copy_vimage2p_Grp_Abs:
traytel@55803
   133
  "\<And>h. vimage2p g Abs (Grp (Collect P) h) = Grp (Collect (\<lambda>x. P (g x))) (Rep o h o g)"
traytel@55803
   134
  unfolding vimage2p_def Grp_def fun_eq_iff
traytel@55803
   135
  by (auto simp: type_definition.Abs_inverse[OF type_copy UNIV_I]
traytel@55803
   136
   type_definition.Rep_inverse[OF type_copy] dest: sym)
traytel@55811
   137
traytel@55811
   138
lemma type_copy_ex_RepI: "(\<exists>b. F b) = (\<exists>b. F (Rep b))"
traytel@55811
   139
proof safe
traytel@55811
   140
  fix b assume "F b"
traytel@55811
   141
  show "\<exists>b'. F (Rep b')"
traytel@55811
   142
  proof (rule exI)
wenzelm@60758
   143
    from \<open>F b\<close> show "F (Rep (Abs b))" using type_definition.Abs_inverse[OF type_copy] by auto
traytel@55811
   144
  qed
traytel@55811
   145
qed blast
traytel@55811
   146
traytel@55803
   147
lemma vimage2p_relcompp_converse:
traytel@55803
   148
  "vimage2p f g (R^--1 OO S) = (vimage2p Rep f R)^--1 OO vimage2p Rep g S"
traytel@55803
   149
  unfolding vimage2p_def relcompp.simps conversep.simps fun_eq_iff image_def
traytel@55811
   150
  by (auto simp: type_copy_ex_RepI)
traytel@55803
   151
traytel@55803
   152
end
traytel@55803
   153
traytel@55935
   154
bnf DEADID: 'a
traytel@55935
   155
  map: "id :: 'a \<Rightarrow> 'a"
traytel@55935
   156
  bd: natLeq
traytel@55935
   157
  rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
traytel@62324
   158
  by (auto simp add: natLeq_card_order natLeq_cinfinite)
traytel@55935
   159
blanchet@58353
   160
definition id_bnf :: "'a \<Rightarrow> 'a" where
blanchet@58353
   161
  "id_bnf \<equiv> (\<lambda>x. x)"
traytel@55935
   162
blanchet@58181
   163
lemma id_bnf_apply: "id_bnf x = x"
blanchet@58181
   164
  unfolding id_bnf_def by simp
traytel@56016
   165
traytel@55935
   166
bnf ID: 'a
blanchet@58181
   167
  map: "id_bnf :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
traytel@55935
   168
  sets: "\<lambda>x. {x}"
traytel@55935
   169
  bd: natLeq
blanchet@58181
   170
  rel: "id_bnf :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
traytel@62324
   171
  pred: "id_bnf :: ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
blanchet@58181
   172
  unfolding id_bnf_def
blanchet@58128
   173
  apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite)
blanchet@58128
   174
  apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
blanchet@58128
   175
  apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3]
blanchet@58128
   176
  done
blanchet@55854
   177
blanchet@58181
   178
lemma type_definition_id_bnf_UNIV: "type_definition id_bnf id_bnf UNIV"
blanchet@58181
   179
  unfolding id_bnf_def by unfold_locales auto
blanchet@55854
   180
blanchet@55062
   181
ML_file "Tools/BNF/bnf_comp_tactics.ML"
blanchet@55062
   182
ML_file "Tools/BNF/bnf_comp.ML"
traytel@60918
   183
ML_file "Tools/BNF/bnf_lift.ML"
blanchet@49309
   184
blanchet@58282
   185
hide_fact
blanchet@58282
   186
  DEADID.inj_map DEADID.inj_map_strong DEADID.map_comp DEADID.map_cong DEADID.map_cong0
blanchet@58282
   187
  DEADID.map_cong_simp DEADID.map_id DEADID.map_id0 DEADID.map_ident DEADID.map_transfer
blanchet@58282
   188
  DEADID.rel_Grp DEADID.rel_compp DEADID.rel_compp_Grp DEADID.rel_conversep DEADID.rel_eq
blanchet@58282
   189
  DEADID.rel_flip DEADID.rel_map DEADID.rel_mono DEADID.rel_transfer
blanchet@58282
   190
  ID.inj_map ID.inj_map_strong ID.map_comp ID.map_cong ID.map_cong0 ID.map_cong_simp ID.map_id
blanchet@58282
   191
  ID.map_id0 ID.map_ident ID.map_transfer ID.rel_Grp ID.rel_compp ID.rel_compp_Grp ID.rel_conversep
blanchet@58282
   192
  ID.rel_eq ID.rel_flip ID.rel_map ID.rel_mono ID.rel_transfer ID.set_map ID.set_transfer
blanchet@58282
   193
blanchet@48975
   194
end