src/HOL/BNF_Comp.thy
author blanchet
Mon, 20 Jan 2014 18:24:56 +0100
changeset 55059 ef2e0fb783c6
parent 55058 4e700eb471d4
child 55062 6d3fad6f01c9
permissions -rw-r--r--
tuned comments
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
55059
ef2e0fb783c6 tuned comments
blanchet
parents: 55058
diff changeset
     1
(*  Title:      HOL/BNF_Comp.thy
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     2
    Author:     Dmitriy Traytel, TU Muenchen
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     3
    Copyright   2012
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     4
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     5
Composition of bounded natural functors.
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     6
*)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     7
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     8
header {* Composition of Bounded Natural Functors *}
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     9
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    10
theory BNF_Comp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    11
imports Basic_BNFs
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    12
begin
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    13
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    14
lemma empty_natural: "(\<lambda>_. {}) o f = image g o (\<lambda>_. {})"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    15
by (rule ext) simp
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    16
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    17
lemma Union_natural: "Union o image (image f) = image f o Union"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    18
by (rule ext) (auto simp only: o_apply)
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    19
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    20
lemma in_Union_o_assoc: "x \<in> (Union o gset o gmap) A \<Longrightarrow> x \<in> (Union o (gset o gmap)) A"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    21
by (unfold o_assoc)
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    22
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    23
lemma comp_single_set_bd:
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    24
  assumes fbd_Card_order: "Card_order fbd" and
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    25
    fset_bd: "\<And>x. |fset x| \<le>o fbd" and
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    26
    gset_bd: "\<And>x. |gset x| \<le>o gbd"
52141
eff000cab70f weaker precendence of syntax for big intersection and union on sets
haftmann
parents: 51893
diff changeset
    27
  shows "|\<Union>(fset ` gset x)| \<le>o gbd *c fbd"
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    28
apply (subst sym[OF SUP_def])
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    29
apply (rule ordLeq_transitive)
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    30
apply (rule card_of_UNION_Sigma)
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    31
apply (subst SIGMA_CSUM)
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    32
apply (rule ordLeq_transitive)
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    33
apply (rule card_of_Csum_Times')
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    34
apply (rule fbd_Card_order)
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    35
apply (rule ballI)
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    36
apply (rule fset_bd)
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    37
apply (rule ordLeq_transitive)
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    38
apply (rule cprod_mono1)
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    39
apply (rule gset_bd)
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    40
apply (rule ordIso_imp_ordLeq)
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    41
apply (rule ordIso_refl)
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    42
apply (rule Card_order_cprod)
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    43
done
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    44
52141
eff000cab70f weaker precendence of syntax for big intersection and union on sets
haftmann
parents: 51893
diff changeset
    45
lemma Union_image_insert: "\<Union>(f ` insert a B) = f a \<union> \<Union>(f ` B)"
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    46
by simp
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    47
52141
eff000cab70f weaker precendence of syntax for big intersection and union on sets
haftmann
parents: 51893
diff changeset
    48
lemma Union_image_empty: "A \<union> \<Union>(f ` {}) = A"
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    49
by simp
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    50
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    51
lemma image_o_collect: "collect ((\<lambda>f. image g o f) ` F) = image g o collect F"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    52
by (rule ext) (auto simp add: collect_def)
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    53
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    54
lemma conj_subset_def: "A \<subseteq> {x. P x \<and> Q x} = (A \<subseteq> {x. P x} \<and> A \<subseteq> {x. Q x})"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    55
by blast
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    56
52141
eff000cab70f weaker precendence of syntax for big intersection and union on sets
haftmann
parents: 51893
diff changeset
    57
lemma UN_image_subset: "\<Union>(f ` g x) \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})"
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    58
by blast
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    59
52141
eff000cab70f weaker precendence of syntax for big intersection and union on sets
haftmann
parents: 51893
diff changeset
    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"
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    61
by (unfold o_apply collect_def SUP_def)
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    62
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    63
lemma wpull_cong:
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    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"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    65
by simp
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    66
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 49512
diff changeset
    67
lemma Grp_fst_snd: "(Grp (Collect (split R)) fst)^--1 OO Grp (Collect (split R)) snd = R"
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 49512
diff changeset
    68
unfolding Grp_def fun_eq_iff relcompp.simps by auto
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 49512
diff changeset
    69
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 49512
diff changeset
    70
lemma OO_Grp_cong: "A = B \<Longrightarrow> (Grp A f)^--1 OO Grp A g = (Grp B f)^--1 OO Grp B g"
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 49512
diff changeset
    71
by simp
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 49512
diff changeset
    72
49309
f20b24214ac2 split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents: 49308
diff changeset
    73
ML_file "Tools/bnf_comp_tactics.ML"
f20b24214ac2 split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents: 49308
diff changeset
    74
ML_file "Tools/bnf_comp.ML"
f20b24214ac2 split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents: 49308
diff changeset
    75
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    76
end