src/HOL/Codatatype/BNF_Util.thy
author blanchet
Tue, 11 Sep 2012 17:14:49 +0200
changeset 49283 97809ae5f7bb
parent 49282 c057e1b39f16
child 49309 f20b24214ac2
permissions -rw-r--r--
move "bnf_util.ML" to "BNF_Util.thy"
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
49282
c057e1b39f16 renamed "BNF_Library" to "BNF_Util"
blanchet
parents: 49276
diff changeset
     1
(*  Title:      HOL/Codatatype/BNF_Util.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
49282
c057e1b39f16 renamed "BNF_Library" to "BNF_Util"
blanchet
parents: 49276
diff changeset
     3
    Author:     Jasmin Blanchette, TU Muenchen
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     4
    Copyright   2012
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     5
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     6
Library for bounded natural functors.
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
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     9
header {* Library for Bounded Natural Functors *}
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    10
49282
c057e1b39f16 renamed "BNF_Library" to "BNF_Util"
blanchet
parents: 49276
diff changeset
    11
theory BNF_Util
49090
6be57c7d84f8 reverted (accidentally commited) changes from changeset fd4aef9bc7a9
Christian Sternagel
parents: 49086
diff changeset
    12
imports
6be57c7d84f8 reverted (accidentally commited) changes from changeset fd4aef9bc7a9
Christian Sternagel
parents: 49086
diff changeset
    13
  "../Ordinals_and_Cardinals/Cardinal_Arithmetic"
6be57c7d84f8 reverted (accidentally commited) changes from changeset fd4aef9bc7a9
Christian Sternagel
parents: 49086
diff changeset
    14
  "~~/src/HOL/Library/Prefix_Order"
48979
b62d14275b89 fixed import paths
blanchet
parents: 48975
diff changeset
    15
  Equiv_Relations_More
49283
97809ae5f7bb move "bnf_util.ML" to "BNF_Util.thy"
blanchet
parents: 49282
diff changeset
    16
uses
97809ae5f7bb move "bnf_util.ML" to "BNF_Util.thy"
blanchet
parents: 49282
diff changeset
    17
  ("Tools/bnf_util.ML")
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    18
begin
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    19
49116
3d520eec2746 allow pseudo-definition of is_Cons in terms of is_Nil (and similarly for other two-constructor datatypes)
blanchet
parents: 49090
diff changeset
    20
lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
3d520eec2746 allow pseudo-definition of is_Cons in terms of is_Nil (and similarly for other two-constructor datatypes)
blanchet
parents: 49090
diff changeset
    21
by (erule iffI) (erule contrapos_pn)
3d520eec2746 allow pseudo-definition of is_Cons in terms of is_Nil (and similarly for other two-constructor datatypes)
blanchet
parents: 49090
diff changeset
    22
49125
5fc5211cf104 implemented "mk_exhaust_tac"
blanchet
parents: 49116
diff changeset
    23
lemma all_unit_eq: "(\<And>x. PROP P x) \<equiv> PROP P ()" by simp
5fc5211cf104 implemented "mk_exhaust_tac"
blanchet
parents: 49116
diff changeset
    24
49255
2ecc533d6697 use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents: 49125
diff changeset
    25
lemma all_prod_eq: "(\<And>x. PROP P x) \<equiv> (\<And>a b. PROP P (a, b))" by clarsimp
49125
5fc5211cf104 implemented "mk_exhaust_tac"
blanchet
parents: 49116
diff changeset
    26
5fc5211cf104 implemented "mk_exhaust_tac"
blanchet
parents: 49116
diff changeset
    27
lemma False_imp_eq: "(False \<Longrightarrow> P) \<equiv> Trueprop True"
5fc5211cf104 implemented "mk_exhaust_tac"
blanchet
parents: 49116
diff changeset
    28
by presburger
5fc5211cf104 implemented "mk_exhaust_tac"
blanchet
parents: 49116
diff changeset
    29
5fc5211cf104 implemented "mk_exhaust_tac"
blanchet
parents: 49116
diff changeset
    30
lemma case_unit: "(case u of () => f) = f"
5fc5211cf104 implemented "mk_exhaust_tac"
blanchet
parents: 49116
diff changeset
    31
by (cases u) (hypsubst, rule unit.cases)
5fc5211cf104 implemented "mk_exhaust_tac"
blanchet
parents: 49116
diff changeset
    32
5fc5211cf104 implemented "mk_exhaust_tac"
blanchet
parents: 49116
diff changeset
    33
lemma All_point_1: "(\<And>z. z = b \<Longrightarrow> phi z) \<equiv> Trueprop (phi b)"
5fc5211cf104 implemented "mk_exhaust_tac"
blanchet
parents: 49116
diff changeset
    34
by presburger
5fc5211cf104 implemented "mk_exhaust_tac"
blanchet
parents: 49116
diff changeset
    35
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    36
lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    37
by blast
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    38
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    39
lemma subset_CollectI: "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> Q x \<Longrightarrow> P x) \<Longrightarrow> ({x \<in> B. Q x} \<subseteq> {x \<in> A. P x})"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    40
by blast
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    41
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    42
lemma mem_Collect_eq_split: "{(x, y). (x, y) \<in> X} = X"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    43
by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    44
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    45
lemma image_comp: "image (f o g) = image f o image g"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    46
by (rule ext) (auto simp only: o_apply image_def)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    47
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    48
lemma empty_natural: "(\<lambda>_. {}) o f = image g o (\<lambda>_. {})"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    49
by (rule ext) simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    50
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    51
lemma Union_natural: "Union o image (image f) = image f o Union"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    52
by (rule ext) (auto simp only: o_apply)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    53
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    54
lemma in_Union_o_assoc: "x \<in> (Union o gset o gmap) A \<Longrightarrow> x \<in> (Union o (gset o gmap)) A"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    55
by (unfold o_assoc)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    56
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    57
lemma comp_single_set_bd:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    58
  assumes fbd_Card_order: "Card_order fbd" and
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    59
    fset_bd: "\<And>x. |fset x| \<le>o fbd" and
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    60
    gset_bd: "\<And>x. |gset x| \<le>o gbd"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    61
  shows "|\<Union>fset ` gset x| \<le>o gbd *c fbd"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    62
apply (subst sym[OF SUP_def])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    63
apply (rule ordLeq_transitive)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    64
apply (rule card_of_UNION_Sigma)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    65
apply (subst SIGMA_CSUM)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    66
apply (rule ordLeq_transitive)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    67
apply (rule card_of_Csum_Times')
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    68
apply (rule fbd_Card_order)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    69
apply (rule ballI)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    70
apply (rule fset_bd)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    71
apply (rule ordLeq_transitive)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    72
apply (rule cprod_mono1)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    73
apply (rule gset_bd)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    74
apply (rule ordIso_imp_ordLeq)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    75
apply (rule ordIso_refl)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    76
apply (rule Card_order_cprod)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    77
done
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    78
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    79
lemma Union_image_insert: "\<Union>f ` insert a B = f a \<union> \<Union>f ` B"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    80
by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    81
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    82
lemma Union_image_empty: "A \<union> \<Union>f ` {} = A"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    83
by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    84
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    85
definition collect where
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    86
  "collect F x = (\<Union>f \<in> F. f x)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    87
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    88
lemma collect_o: "collect F o g = collect ((\<lambda>f. f o g) ` F)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    89
by (rule ext) (auto simp only: o_apply collect_def)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    90
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    91
lemma image_o_collect: "collect ((\<lambda>f. image g o f) ` F) = image g o collect F"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    92
by (rule ext) (auto simp add: collect_def)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    93
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    94
lemma conj_subset_def: "A \<subseteq> {x. P x \<and> Q x} = (A \<subseteq> {x. P x} \<and> A \<subseteq> {x. Q x})"
49255
2ecc533d6697 use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents: 49125
diff changeset
    95
by blast
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    96
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    97
lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"
49255
2ecc533d6697 use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents: 49125
diff changeset
    98
by blast
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    99
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   100
lemma rev_bspec: "a \<in> A \<Longrightarrow> \<forall>z \<in> A. P z \<Longrightarrow> P a"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   101
by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   102
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   103
lemma Un_cong: "\<lbrakk>A = B; C = D\<rbrakk> \<Longrightarrow> A \<union> C = B \<union> D"
49255
2ecc533d6697 use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents: 49125
diff changeset
   104
by simp
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   105
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   106
lemma UN_image_subset: "\<Union>f ` g x \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})"
49255
2ecc533d6697 use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents: 49125
diff changeset
   107
by blast
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   108
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   109
lemma image_Collect_subsetI:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   110
  "(\<And>x. P x \<Longrightarrow> f x \<in> B) \<Longrightarrow> f ` {x. P x} \<subseteq> B"
49255
2ecc533d6697 use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents: 49125
diff changeset
   111
by blast
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   112
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   113
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"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   114
by (unfold o_apply collect_def SUP_def)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   115
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   116
lemma sum_case_comp_Inl:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   117
"sum_case f g \<circ> Inl = f"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   118
unfolding comp_def by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   119
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   120
lemma sum_case_expand_Inr: "f o Inl = g \<Longrightarrow> f x = sum_case g (f o Inr) x"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   121
by (auto split: sum.splits)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   122
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   123
lemma converse_mono:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   124
"R1 ^-1 \<subseteq> R2 ^-1 \<longleftrightarrow> R1 \<subseteq> R2"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   125
unfolding converse_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   126
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   127
lemma converse_shift:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   128
"R1 \<subseteq> R2 ^-1 \<Longrightarrow> R1 ^-1 \<subseteq> R2"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   129
unfolding converse_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   130
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   131
lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   132
by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   133
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   134
lemma equiv_triv1:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   135
assumes "equiv A R" and "(a, b) \<in> R" and "(a, c) \<in> R"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   136
shows "(b, c) \<in> R"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   137
using assms unfolding equiv_def sym_def trans_def by blast
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   138
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   139
lemma equiv_triv2:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   140
assumes "equiv A R" and "(a, b) \<in> R" and "(b, c) \<in> R"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   141
shows "(a, c) \<in> R"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   142
using assms unfolding equiv_def trans_def by blast
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   143
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   144
lemma equiv_proj:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   145
  assumes e: "equiv A R" and "z \<in> R"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   146
  shows "(proj R o fst) z = (proj R o snd) z"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   147
proof -
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   148
  from assms(2) have z: "(fst z, snd z) \<in> R" by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   149
  have P: "\<And>x. (fst z, x) \<in> R \<Longrightarrow> (snd z, x) \<in> R" by (erule equiv_triv1[OF e z])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   150
  have "\<And>x. (snd z, x) \<in> R \<Longrightarrow> (fst z, x) \<in> R" by (erule equiv_triv2[OF e z])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   151
  with P show ?thesis unfolding proj_def[abs_def] by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   152
qed
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   153
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   154
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   155
section{* Weak pullbacks: *}
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   156
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   157
definition csquare where
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   158
"csquare A f1 f2 p1 p2 \<longleftrightarrow> (\<forall> a \<in> A. f1 (p1 a) = f2 (p2 a))"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   159
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   160
definition wpull where
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   161
"wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   162
 (\<forall> b1 b2. b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2 \<longrightarrow> (\<exists> a \<in> A. p1 a = b1 \<and> p2 a = b2))"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   163
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   164
lemma wpull_cong:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   165
"\<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"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   166
by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   167
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   168
lemma wpull_id: "wpull UNIV B1 B2 id id id id"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   169
unfolding wpull_def by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   170
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   171
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   172
(* Weak pseudo-pullbacks *)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   173
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   174
definition wppull where
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   175
"wppull A B1 B2 f1 f2 e1 e2 p1 p2 \<longleftrightarrow>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   176
 (\<forall> b1 b2. b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2 \<longrightarrow>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   177
           (\<exists> a \<in> A. e1 (p1 a) = e1 b1 \<and> e2 (p2 a) = e2 b2))"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   178
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   179
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   180
(* The pullback of sets *)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   181
definition thePull where
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   182
"thePull B1 B2 f1 f2 = {(b1,b2). b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2}"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   183
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   184
lemma wpull_thePull:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   185
"wpull (thePull B1 B2 f1 f2) B1 B2 f1 f2 fst snd"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   186
unfolding wpull_def thePull_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   187
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   188
lemma wppull_thePull:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   189
assumes "wppull A B1 B2 f1 f2 e1 e2 p1 p2"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   190
shows
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   191
"\<exists> j. \<forall> a' \<in> thePull B1 B2 f1 f2.
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   192
   j a' \<in> A \<and>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   193
   e1 (p1 (j a')) = e1 (fst a') \<and> e2 (p2 (j a')) = e2 (snd a')"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   194
(is "\<exists> j. \<forall> a' \<in> ?A'. ?phi a' (j a')")
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   195
proof(rule bchoice[of ?A' ?phi], default)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   196
  fix a' assume a': "a' \<in> ?A'"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   197
  hence "fst a' \<in> B1" unfolding thePull_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   198
  moreover
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   199
  from a' have "snd a' \<in> B2" unfolding thePull_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   200
  moreover have "f1 (fst a') = f2 (snd a')"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   201
  using a' unfolding csquare_def thePull_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   202
  ultimately show "\<exists> ja'. ?phi a' ja'"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   203
  using assms unfolding wppull_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   204
qed
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   205
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   206
lemma wpull_wppull:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   207
assumes wp: "wpull A' B1 B2 f1 f2 p1' p2'" and
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   208
1: "\<forall> a' \<in> A'. j a' \<in> A \<and> e1 (p1 (j a')) = e1 (p1' a') \<and> e2 (p2 (j a')) = e2 (p2' a')"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   209
shows "wppull A B1 B2 f1 f2 e1 e2 p1 p2"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   210
unfolding wppull_def proof safe
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   211
  fix b1 b2
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   212
  assume b1: "b1 \<in> B1" and b2: "b2 \<in> B2" and f: "f1 b1 = f2 b2"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   213
  then obtain a' where a': "a' \<in> A'" and b1: "b1 = p1' a'" and b2: "b2 = p2' a'"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   214
  using wp unfolding wpull_def by blast
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   215
  show "\<exists>a\<in>A. e1 (p1 a) = e1 b1 \<and> e2 (p2 a) = e2 b2"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   216
  apply(rule bexI[of _ "j a'"]) unfolding b1 b2 using a' 1 by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   217
qed
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   218
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   219
lemma wppull_id: "\<lbrakk>wpull UNIV UNIV UNIV f1 f2 p1 p2; e1 = id; e2 = id\<rbrakk> \<Longrightarrow>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   220
   wppull UNIV UNIV UNIV f1 f2 e1 e2 p1 p2"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   221
by (erule wpull_wppull) auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   222
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   223
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   224
(* Operators: *)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   225
definition diag where "diag A \<equiv> {(a,a) | a. a \<in> A}"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   226
definition "Gr A f = {(a,f a) | a. a \<in> A}"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   227
definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   228
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   229
lemma diagI: "x \<in> A \<Longrightarrow> (x, x) \<in> diag A"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   230
unfolding diag_def by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   231
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   232
lemma diagE: "(a, b) \<in> diag A \<Longrightarrow> a = b"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   233
unfolding diag_def by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   234
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   235
lemma diagE': "x \<in> diag A \<Longrightarrow> fst x = snd x"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   236
unfolding diag_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   237
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   238
lemma diag_fst: "x \<in> diag A \<Longrightarrow> fst x \<in> A"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   239
unfolding diag_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   240
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   241
lemma diag_UNIV: "diag UNIV = Id"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   242
unfolding diag_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   243
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   244
lemma diag_converse: "diag A = (diag A) ^-1"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   245
unfolding diag_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   246
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   247
lemma diag_Comp: "diag A = diag A O diag A"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   248
unfolding diag_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   249
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   250
lemma diag_Gr: "diag A = Gr A id"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   251
unfolding diag_def Gr_def by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   252
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   253
lemma diag_UNIV_I: "x = y \<Longrightarrow> (x, y) \<in> diag UNIV"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   254
unfolding diag_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   255
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   256
lemma image2_eqI: "\<lbrakk>b = f x; c = g x; x \<in> A\<rbrakk> \<Longrightarrow> (b, c) \<in> image2 A f g"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   257
unfolding image2_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   258
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   259
lemma Id_def': "Id = {(a,b). a = b}"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   260
by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   261
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   262
lemma Id_alt: "Id = Gr UNIV id"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   263
unfolding Gr_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   264
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   265
lemma Id_subset: "Id \<subseteq> {(a, b). P a b \<or> a = b}"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   266
by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   267
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   268
lemma IdD: "(a, b) \<in> Id \<Longrightarrow> a = b"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   269
by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   270
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   271
lemma image2_Gr: "image2 A f g = (Gr A f)^-1 O (Gr A g)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   272
unfolding image2_def Gr_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   273
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   274
lemma GrI: "\<lbrakk>x \<in> A; f x = fx\<rbrakk> \<Longrightarrow> (x, fx) \<in> Gr A f"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   275
unfolding Gr_def by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   276
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   277
lemma GrE: "(x, fx) \<in> Gr A f \<Longrightarrow> (x \<in> A \<Longrightarrow> f x = fx \<Longrightarrow> P) \<Longrightarrow> P"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   278
unfolding Gr_def by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   279
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   280
lemma GrD1: "(x, fx) \<in> Gr A f \<Longrightarrow> x \<in> A"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   281
unfolding Gr_def by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   282
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   283
lemma GrD2: "(x, fx) \<in> Gr A f \<Longrightarrow> f x = fx"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   284
unfolding Gr_def by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   285
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   286
lemma Gr_UNIV_id: "f = id \<Longrightarrow> (Gr UNIV f)^-1 O Gr UNIV f = Gr UNIV f"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   287
unfolding Gr_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   288
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   289
lemma Gr_fst_snd: "(Gr R fst)^-1 O Gr R snd = R"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   290
unfolding Gr_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   291
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   292
lemma Gr_mono: "A \<subseteq> B \<Longrightarrow> Gr A f \<subseteq> Gr B f"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   293
unfolding Gr_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   294
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   295
lemma subst_rel_def: "A = B \<Longrightarrow> (Gr A f)^-1 O Gr A g = (Gr B f)^-1 O Gr B g"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   296
by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   297
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   298
lemma abs_pred_def: "\<lbrakk>\<And>x y. (x, y) \<in> rel = pred x y\<rbrakk> \<Longrightarrow> rel = Collect (split pred)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   299
by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   300
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   301
lemma Collect_split_cong: "Collect (split pred) = Collect (split pred') \<Longrightarrow> pred = pred'"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   302
by blast
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   303
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   304
lemma pred_def_abs: "rel = Collect (split pred) \<Longrightarrow> pred = (\<lambda>x y. (x, y) \<in> rel)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   305
by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   306
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   307
lemma wpull_Gr:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   308
"wpull (Gr A f) A (f ` A) f id fst snd"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   309
unfolding wpull_def Gr_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   310
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   311
lemma Gr_incl: "Gr A f \<subseteq> A <*> B \<longleftrightarrow> f ` A \<subseteq> B"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   312
unfolding Gr_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   313
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   314
lemma equiv_Image: "equiv A R \<Longrightarrow> (\<And>a b. (a, b) \<in> R \<Longrightarrow> a \<in> A \<and> b \<in> A \<and> R `` {a} = R `` {b})"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   315
unfolding equiv_def refl_on_def Image_def by (auto intro: transD symD)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   316
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   317
definition relImage where
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   318
"relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   319
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   320
definition relInvImage where
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   321
"relInvImage A R f \<equiv> {(a1, a2) | a1 a2. a1 \<in> A \<and> a2 \<in> A \<and> (f a1, f a2) \<in> R}"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   322
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   323
lemma relImage_Gr:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   324
"\<lbrakk>R \<subseteq> A \<times> A\<rbrakk> \<Longrightarrow> relImage R f = (Gr A f)^-1 O R O Gr A f"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   325
unfolding relImage_def Gr_def relcomp_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   326
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   327
lemma relInvImage_Gr: "\<lbrakk>R \<subseteq> B \<times> B\<rbrakk> \<Longrightarrow> relInvImage A R f = Gr A f O R O (Gr A f)^-1"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   328
unfolding Gr_def relcomp_def image_def relInvImage_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   329
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   330
lemma relImage_mono:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   331
"R1 \<subseteq> R2 \<Longrightarrow> relImage R1 f \<subseteq> relImage R2 f"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   332
unfolding relImage_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   333
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   334
lemma relInvImage_mono:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   335
"R1 \<subseteq> R2 \<Longrightarrow> relInvImage A R1 f \<subseteq> relInvImage A R2 f"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   336
unfolding relInvImage_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   337
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   338
lemma relInvImage_diag:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   339
"(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (diag B) f \<subseteq> Id"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   340
unfolding relInvImage_def diag_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   341
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   342
lemma relInvImage_UNIV_relImage:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   343
"R \<subseteq> relInvImage UNIV (relImage R f) f"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   344
unfolding relInvImage_def relImage_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   345
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   346
lemma relImage_proj:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   347
assumes "equiv A R"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   348
shows "relImage R (proj R) \<subseteq> diag (A//R)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   349
unfolding relImage_def diag_def apply safe
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   350
using proj_iff[OF assms]
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   351
by (metis assms equiv_Image proj_def proj_preserves)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   352
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   353
lemma relImage_relInvImage:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   354
assumes "R \<subseteq> f ` A <*> f ` A"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   355
shows "relImage (relInvImage A R f) f = R"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   356
using assms unfolding relImage_def relInvImage_def by fastforce
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   357
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   358
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   359
(* Relation composition as a weak pseudo-pullback *)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   360
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   361
(* pick middle *)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   362
definition "pickM P Q a c = (SOME b. (a,b) \<in> P \<and> (b,c) \<in> Q)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   363
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   364
lemma pickM:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   365
assumes "(a,c) \<in> P O Q"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   366
shows "(a, pickM P Q a c) \<in> P \<and> (pickM P Q a c, c) \<in> Q"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   367
unfolding pickM_def apply(rule someI_ex)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   368
using assms unfolding relcomp_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   369
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   370
definition fstO where "fstO P Q ac = (fst ac, pickM P Q (fst ac) (snd ac))"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   371
definition sndO where "sndO P Q ac = (pickM P Q (fst ac) (snd ac), snd ac)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   372
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   373
lemma fstO_in: "ac \<in> P O Q \<Longrightarrow> fstO P Q ac \<in> P"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   374
by (metis assms fstO_def pickM surjective_pairing)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   375
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   376
lemma fst_fstO: "fst bc = (fst \<circ> fstO P Q) bc"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   377
unfolding comp_def fstO_def by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   378
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   379
lemma snd_sndO: "snd bc = (snd \<circ> sndO P Q) bc"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   380
unfolding comp_def sndO_def by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   381
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   382
lemma sndO_in: "ac \<in> P O Q \<Longrightarrow> sndO P Q ac \<in> Q"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   383
by (metis assms sndO_def pickM surjective_pairing)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   384
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   385
lemma csquare_fstO_sndO:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   386
"csquare (P O Q) snd fst (fstO P Q) (sndO P Q)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   387
unfolding csquare_def fstO_def sndO_def using pickM by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   388
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   389
lemma wppull_fstO_sndO:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   390
shows "wppull (P O Q) P Q snd fst fst snd (fstO P Q) (sndO P Q)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   391
using pickM unfolding wppull_def fstO_def sndO_def relcomp_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   392
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   393
lemma subst_Pair: "P x y \<Longrightarrow> a = (x, y) \<Longrightarrow> P (fst a) (snd a)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   394
by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   395
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   396
lemma snd_fst_flip: "snd xy = (fst o (%(x, y). (y, x))) xy"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   397
by (simp split: prod.split)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   398
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   399
lemma fst_snd_flip: "fst xy = (snd o (%(x, y). (y, x))) xy"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   400
by (simp split: prod.split)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   401
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   402
lemma flip_rel: "A \<subseteq> (R ^-1) \<Longrightarrow> (%(x, y). (y, x)) ` A \<subseteq> R"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   403
by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   404
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   405
lemma fst_diag_id: "(fst \<circ> (%x. (x, x))) z = id z"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   406
by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   407
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   408
lemma snd_diag_id: "(snd \<circ> (%x. (x, x))) z = id z"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   409
by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   410
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   411
lemma fst_snd: "\<lbrakk>snd x = (y, z)\<rbrakk> \<Longrightarrow> fst (snd x) = y"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   412
by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   413
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   414
lemma snd_snd: "\<lbrakk>snd x = (y, z)\<rbrakk> \<Longrightarrow> snd (snd x) = z"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   415
by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   416
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   417
lemma fstI: "x = (y, z) \<Longrightarrow> fst x = y"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   418
by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   419
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   420
lemma sndI: "x = (y, z) \<Longrightarrow> snd x = z"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   421
by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   422
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   423
lemma Collect_restrict: "{x. x \<in> X \<and> P x} \<subseteq> X"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   424
by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   425
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   426
lemma Collect_restrict': "{(x, y) | x y. phi x y \<and> P x y} \<subseteq> {(x, y) | x y. phi x y}"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   427
by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   428
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   429
lemma prop_restrict: "\<lbrakk>x \<in> Z; Z \<subseteq> {x. x \<in> X \<and> P x}\<rbrakk> \<Longrightarrow> P x"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   430
by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   431
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   432
lemma underS_I: "\<lbrakk>i \<noteq> j; (i, j) \<in> R\<rbrakk> \<Longrightarrow> i \<in> rel.underS R j"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   433
unfolding rel.underS_def by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   434
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   435
lemma underS_E: "i \<in> rel.underS R j \<Longrightarrow> i \<noteq> j \<and> (i, j) \<in> R"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   436
unfolding rel.underS_def by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   437
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   438
lemma underS_Field: "i \<in> rel.underS R j \<Longrightarrow> i \<in> Field R"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   439
unfolding rel.underS_def Field_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   440
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   441
lemma FieldI2: "(i, j) \<in> R \<Longrightarrow> j \<in> Field R"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   442
unfolding Field_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   443
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   444
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   445
subsection {* Convolution product *}
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   446
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   447
definition convol ("<_ , _>") where
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   448
"<f , g> \<equiv> %a. (f a, g a)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   449
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   450
lemma fst_convol:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   451
"fst o <f , g> = f"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   452
apply(rule ext)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   453
unfolding convol_def by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   454
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   455
lemma snd_convol:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   456
"snd o <f , g> = g"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   457
apply(rule ext)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   458
unfolding convol_def by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   459
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   460
lemma fst_convol': "fst (<f, g> x) = f x"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   461
using fst_convol unfolding convol_def by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   462
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   463
lemma snd_convol': "snd (<f, g> x) = g x"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   464
using snd_convol unfolding convol_def by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   465
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   466
lemma image_convolD: "\<lbrakk>(a, b) \<in> <f, g> ` X\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> X \<and> a = f x \<and> b = g x"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   467
unfolding convol_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   468
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   469
lemma convol_expand_snd: "fst o f = g \<Longrightarrow>  <g, snd o f> = f"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   470
unfolding convol_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   471
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   472
subsection{* Facts about functions *}
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   473
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   474
lemma pointfreeE: "f o g = f' o g' \<Longrightarrow> f (g x) = f' (g' x)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   475
unfolding o_def fun_eq_iff by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   476
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   477
lemma pointfree_idE: "f o g = id \<Longrightarrow> f (g x) = x"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   478
unfolding o_def fun_eq_iff by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   479
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   480
definition inver where
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   481
  "inver g f A = (ALL a : A. g (f a) = a)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   482
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   483
lemma bij_betw_iff_ex:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   484
  "bij_betw f A B = (EX g. g ` B = A \<and> inver g f A \<and> inver f g B)" (is "?L = ?R")
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   485
proof (rule iffI)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   486
  assume ?L
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   487
  hence f: "f ` A = B" and inj_f: "inj_on f A" unfolding bij_betw_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   488
  let ?phi = "% b a. a : A \<and> f a = b"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   489
  have "ALL b : B. EX a. ?phi b a" using f by blast
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   490
  then obtain g where g: "ALL b : B. g b : A \<and> f (g b) = b"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   491
    using bchoice[of B ?phi] by blast
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   492
  hence gg: "ALL b : f ` A. g b : A \<and> f (g b) = b" using f by blast
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   493
  have gf: "inver g f A" unfolding inver_def by (metis gg imageI inj_f the_inv_into_f_f)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   494
  moreover have "g ` B \<le> A \<and> inver f g B" using g unfolding inver_def by blast
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   495
  moreover have "A \<le> g ` B"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   496
  proof safe
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   497
    fix a assume a: "a : A"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   498
    hence "f a : B" using f by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   499
    moreover have "a = g (f a)" using a gf unfolding inver_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   500
    ultimately show "a : g ` B" by blast
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   501
  qed
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   502
  ultimately show ?R by blast
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   503
next
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   504
  assume ?R
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   505
  then obtain g where g: "g ` B = A \<and> inver g f A \<and> inver f g B" by blast
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   506
  show ?L unfolding bij_betw_def
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   507
  proof safe
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   508
    show "inj_on f A" unfolding inj_on_def
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   509
    proof safe
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   510
      fix a1 a2 assume a: "a1 : A"  "a2 : A" and "f a1 = f a2"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   511
      hence "g (f a1) = g (f a2)" by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   512
      thus "a1 = a2" using a g unfolding inver_def by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   513
    qed
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   514
  next
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   515
    fix a assume "a : A"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   516
    then obtain b where b: "b : B" and a: "a = g b" using g by blast
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   517
    hence "b = f (g b)" using g unfolding inver_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   518
    thus "f a : B" unfolding a using b by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   519
  next
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   520
    fix b assume "b : B"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   521
    hence "g b : A \<and> b = f (g b)" using g unfolding inver_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   522
    thus "b : f ` A" by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   523
  qed
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   524
qed
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   525
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   526
lemma bijI: "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   527
unfolding bij_def inj_on_def by auto blast
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   528
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   529
lemma bij_betw_ex_weakE:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   530
  "\<lbrakk>bij_betw f A B\<rbrakk> \<Longrightarrow> \<exists>g. g ` B \<subseteq> A \<and> inver g f A \<and> inver f g B"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   531
by (auto simp only: bij_betw_iff_ex)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   532
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   533
lemma inver_surj: "\<lbrakk>g ` B \<subseteq> A; f ` A \<subseteq> B; inver g f A\<rbrakk> \<Longrightarrow> g ` B = A"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   534
unfolding inver_def by auto (rule rev_image_eqI, auto)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   535
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   536
lemma inver_mono: "\<lbrakk>A \<subseteq> B; inver f g B\<rbrakk> \<Longrightarrow> inver f g A"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   537
unfolding inver_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   538
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   539
lemma inver_pointfree: "inver f g A = (\<forall>a \<in> A. (f o g) a = a)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   540
unfolding inver_def by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   541
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   542
lemma bij_betwE: "bij_betw f A B \<Longrightarrow> \<forall>a\<in>A. f a \<in> B"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   543
unfolding bij_betw_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   544
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   545
lemma bij_betw_imageE: "bij_betw f A B \<Longrightarrow> f ` A = B"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   546
unfolding bij_betw_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   547
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   548
lemma inverE: "\<lbrakk>inver f f' A; x \<in> A\<rbrakk> \<Longrightarrow> f (f' x) = x"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   549
unfolding inver_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   550
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   551
lemma bij_betw_inver1: "bij_betw f A B \<Longrightarrow> inver (inv_into A f) f A"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   552
unfolding bij_betw_def inver_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   553
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   554
lemma bij_betw_inver2: "bij_betw f A B \<Longrightarrow> inver f (inv_into A f) B"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   555
unfolding bij_betw_def inver_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   556
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   557
lemma bij_betwI: "\<lbrakk>bij_betw g B A; inver g f A; inver f g B\<rbrakk> \<Longrightarrow> bij_betw f A B"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   558
by (metis bij_betw_iff_ex bij_betw_imageE)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   559
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   560
lemma bij_betwI':
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   561
  "\<lbrakk>\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> (f x = f y) = (x = y);
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   562
    \<And>x. x \<in> X \<Longrightarrow> f x \<in> Y;
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   563
    \<And>y. y \<in> Y \<Longrightarrow> \<exists>x \<in> X. y = f x\<rbrakk> \<Longrightarrow> bij_betw f X Y"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   564
unfolding bij_betw_def inj_on_def by auto (metis rev_image_eqI)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   565
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   566
lemma o_bij:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   567
  assumes gf: "g o f = id" and fg: "f o g = id"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   568
  shows "bij f"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   569
unfolding bij_def inj_on_def surj_def proof safe
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   570
  fix a1 a2 assume "f a1 = f a2"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   571
  hence "g ( f a1) = g (f a2)" by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   572
  thus "a1 = a2" using gf unfolding fun_eq_iff by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   573
next
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   574
  fix b
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   575
  have "b = f (g b)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   576
  using fg unfolding fun_eq_iff by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   577
  thus "EX a. b = f a" by blast
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   578
qed
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   579
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   580
lemma surj_fun_eq:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   581
  assumes surj_on: "f ` X = UNIV" and eq_on: "\<forall>x \<in> X. (g1 o f) x = (g2 o f) x"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   582
  shows "g1 = g2"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   583
proof (rule ext)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   584
  fix y
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   585
  from surj_on obtain x where "x \<in> X" and "y = f x" by blast
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   586
  thus "g1 y = g2 y" using eq_on by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   587
qed
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   588
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   589
lemma Card_order_wo_rel: "Card_order r \<Longrightarrow> wo_rel r"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   590
unfolding wo_rel_def card_order_on_def by blast 
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   591
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   592
lemma Cinfinite_limit: "\<lbrakk>x \<in> Field r; Cinfinite r\<rbrakk> \<Longrightarrow>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   593
  \<exists>y \<in> Field r. x \<noteq> y \<and> (x, y) \<in> r"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   594
unfolding cinfinite_def by (auto simp add: infinite_Card_order_limit)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   595
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   596
lemma Card_order_trans:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   597
  "\<lbrakk>Card_order r; x \<noteq> y; (x, y) \<in> r; y \<noteq> z; (y, z) \<in> r\<rbrakk> \<Longrightarrow> x \<noteq> z \<and> (x, z) \<in> r"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   598
unfolding card_order_on_def well_order_on_def linear_order_on_def
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   599
  partial_order_on_def preorder_on_def trans_def antisym_def by blast
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   600
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   601
lemma Cinfinite_limit2:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   602
 assumes x1: "x1 \<in> Field r" and x2: "x2 \<in> Field r" and r: "Cinfinite r"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   603
 shows "\<exists>y \<in> Field r. (x1 \<noteq> y \<and> (x1, y) \<in> r) \<and> (x2 \<noteq> y \<and> (x2, y) \<in> r)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   604
proof -
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   605
  from r have trans: "trans r" and total: "Total r" and antisym: "antisym r"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   606
    unfolding card_order_on_def well_order_on_def linear_order_on_def
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   607
      partial_order_on_def preorder_on_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   608
  obtain y1 where y1: "y1 \<in> Field r" "x1 \<noteq> y1" "(x1, y1) \<in> r"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   609
    using Cinfinite_limit[OF x1 r] by blast
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   610
  obtain y2 where y2: "y2 \<in> Field r" "x2 \<noteq> y2" "(x2, y2) \<in> r"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   611
    using Cinfinite_limit[OF x2 r] by blast
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   612
  show ?thesis
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   613
  proof (cases "y1 = y2")
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   614
    case True with y1 y2 show ?thesis by blast
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   615
  next
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   616
    case False
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   617
    with y1(1) y2(1) total have "(y1, y2) \<in> r \<or> (y2, y1) \<in> r"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   618
      unfolding total_on_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   619
    thus ?thesis
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   620
    proof
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   621
      assume *: "(y1, y2) \<in> r"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   622
      with trans y1(3) have "(x1, y2) \<in> r" unfolding trans_def by blast
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   623
      with False y1 y2 * antisym show ?thesis by (cases "x1 = y2") (auto simp: antisym_def)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   624
    next
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   625
      assume *: "(y2, y1) \<in> r"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   626
      with trans y2(3) have "(x2, y1) \<in> r" unfolding trans_def by blast
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   627
      with False y1 y2 * antisym show ?thesis by (cases "x2 = y1") (auto simp: antisym_def)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   628
    qed
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   629
  qed
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   630
qed
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   631
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   632
lemma Cinfinite_limit_finite: "\<lbrakk>finite X; X \<subseteq> Field r; Cinfinite r\<rbrakk>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   633
 \<Longrightarrow> \<exists>y \<in> Field r. \<forall>x \<in> X. (x \<noteq> y \<and> (x, y) \<in> r)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   634
proof (induct X rule: finite_induct)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   635
  case empty thus ?case unfolding cinfinite_def using ex_in_conv[of "Field r"] finite.emptyI by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   636
next
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   637
  case (insert x X)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   638
  then obtain y where y: "y \<in> Field r" "\<forall>x \<in> X. (x \<noteq> y \<and> (x, y) \<in> r)" by blast
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   639
  then obtain z where z: "z \<in> Field r" "x \<noteq> z \<and> (x, z) \<in> r" "y \<noteq> z \<and> (y, z) \<in> r"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   640
    using Cinfinite_limit2[OF _ y(1) insert(5), of x] insert(4) by blast
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   641
  show ?case by (metis Card_order_trans insert(5) insertE y(2) z)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   642
qed
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   643
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   644
lemma insert_subsetI: "\<lbrakk>x \<in> A; X \<subseteq> A\<rbrakk> \<Longrightarrow> insert x X \<subseteq> A"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   645
by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   646
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   647
(*helps resolution*)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   648
lemma well_order_induct_imp:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   649
  "wo_rel r \<Longrightarrow> (\<And>x. \<forall>y. y \<noteq> x \<and> (y, x) \<in> r \<longrightarrow> y \<in> Field r \<longrightarrow> P y \<Longrightarrow> x \<in> Field r \<longrightarrow> P x) \<Longrightarrow>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   650
     x \<in> Field r \<longrightarrow> P x"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   651
by (erule wo_rel.well_order_induct)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   652
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   653
lemma meta_spec2:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   654
  assumes "(\<And>x y. PROP P x y)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   655
  shows "PROP P x y"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   656
by (rule `(\<And>x y. PROP P x y)`)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   657
49077
154f25a162e3 renamed theory List_Prefix into Sublist (since it is not only about prefixes)
Christian Sternagel
parents: 48979
diff changeset
   658
(*Extended Sublist*)
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   659
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   660
definition prefCl where
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   661
  "prefCl Kl = (\<forall> kl1 kl2. kl1 \<le> kl2 \<and> kl2 \<in> Kl \<longrightarrow> kl1 \<in> Kl)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   662
definition PrefCl where
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   663
  "PrefCl A n = (\<forall>kl kl'. kl \<in> A n \<and> kl' \<le> kl \<longrightarrow> (\<exists>m\<le>n. kl' \<in> A m))"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   664
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   665
lemma prefCl_UN:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   666
  "\<lbrakk>\<And>n. PrefCl A n\<rbrakk> \<Longrightarrow> prefCl (\<Union>n. A n)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   667
unfolding prefCl_def PrefCl_def by fastforce
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   668
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   669
definition Succ where "Succ Kl kl = {k . kl @ [k] \<in> Kl}"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   670
definition Shift where "Shift Kl k = {kl. k # kl \<in> Kl}"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   671
definition shift where "shift lab k = (\<lambda>kl. lab (k # kl))"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   672
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   673
lemmas sh_def = Shift_def shift_def
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   674
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   675
lemma empty_Shift: "\<lbrakk>[] \<in> Kl; k \<in> Succ Kl []\<rbrakk> \<Longrightarrow> [] \<in> Shift Kl k"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   676
unfolding Shift_def Succ_def by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   677
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   678
lemma Shift_clists: "Kl \<subseteq> Field (clists r) \<Longrightarrow> Shift Kl k \<subseteq> Field (clists r)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   679
unfolding Shift_def clists_def Field_card_of by auto
49090
6be57c7d84f8 reverted (accidentally commited) changes from changeset fd4aef9bc7a9
Christian Sternagel
parents: 49086
diff changeset
   680
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   681
lemma Shift_prefCl: "prefCl Kl \<Longrightarrow> prefCl (Shift Kl k)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   682
unfolding prefCl_def Shift_def
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   683
proof safe
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   684
  fix kl1 kl2
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   685
  assume "\<forall>kl1 kl2. kl1 \<le> kl2 \<and> kl2 \<in> Kl \<longrightarrow> kl1 \<in> Kl"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   686
    "kl1 \<le> kl2" "k # kl2 \<in> Kl"
49090
6be57c7d84f8 reverted (accidentally commited) changes from changeset fd4aef9bc7a9
Christian Sternagel
parents: 49086
diff changeset
   687
  thus "k # kl1 \<in> Kl" using Cons_prefix_Cons[of k kl1 k kl2] by blast
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   688
qed
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   689
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   690
lemma not_in_Shift: "kl \<notin> Shift Kl x \<Longrightarrow> x # kl \<notin> Kl"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   691
unfolding Shift_def by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   692
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   693
lemma prefCl_Succ: "\<lbrakk>prefCl Kl; k # kl \<in> Kl\<rbrakk> \<Longrightarrow> k \<in> Succ Kl []"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   694
unfolding Succ_def proof
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   695
  assume "prefCl Kl" "k # kl \<in> Kl"
49090
6be57c7d84f8 reverted (accidentally commited) changes from changeset fd4aef9bc7a9
Christian Sternagel
parents: 49086
diff changeset
   696
  moreover have "k # [] \<le> k # kl" by auto
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   697
  ultimately have "k # [] \<in> Kl" unfolding prefCl_def by blast
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   698
  thus "[] @ [k] \<in> Kl" by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   699
qed
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   700
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   701
lemma SuccD: "k \<in> Succ Kl kl \<Longrightarrow> kl @ [k] \<in> Kl"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   702
unfolding Succ_def by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   703
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   704
lemmas SuccE = SuccD[elim_format]
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   705
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   706
lemma SuccI: "kl @ [k] \<in> Kl \<Longrightarrow> k \<in> Succ Kl kl"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   707
unfolding Succ_def by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   708
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   709
lemma ShiftD: "kl \<in> Shift Kl k \<Longrightarrow> k # kl \<in> Kl"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   710
unfolding Shift_def by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   711
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   712
lemma Succ_Shift: "Succ (Shift Kl k) kl = Succ Kl (k # kl)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   713
unfolding Succ_def Shift_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   714
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   715
lemma ShiftI: "k # kl \<in> Kl \<Longrightarrow> kl \<in> Shift Kl k"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   716
unfolding Shift_def by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   717
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   718
lemma Func_cexp: "|Func A B| =o |B| ^c |A|"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   719
unfolding cexp_def Field_card_of by (simp only: card_of_refl)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   720
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   721
lemma clists_bound: "A \<in> Field (cpow (clists r)) - {{}} \<Longrightarrow> |A| \<le>o clists r"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   722
unfolding cpow_def clists_def Field_card_of by (auto simp: card_of_mono1)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   723
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   724
lemma cpow_clists_czero: "\<lbrakk>A \<in> Field (cpow (clists r)) - {{}}; |A| =o czero\<rbrakk> \<Longrightarrow> False"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   725
unfolding cpow_def clists_def
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   726
by (auto simp add: card_of_ordIso_czero_iff_empty[symmetric])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   727
   (erule notE, erule ordIso_transitive, rule czero_ordIso)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   728
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   729
lemma incl_UNION_I:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   730
assumes "i \<in> I" and "A \<subseteq> F i"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   731
shows "A \<subseteq> UNION I F"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   732
using assms by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   733
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   734
lemma Nil_clists: "{[]} \<subseteq> Field (clists r)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   735
unfolding clists_def Field_card_of by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   736
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   737
lemma Cons_clists:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   738
  "\<lbrakk>x \<in> Field r; xs \<in> Field (clists r)\<rbrakk> \<Longrightarrow> x # xs \<in> Field (clists r)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   739
unfolding clists_def Field_card_of by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   740
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   741
lemma length_Cons: "length (x#xs) = Suc (length xs)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   742
by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   743
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   744
lemma length_append_singleton: "length (xs @ [x]) = Suc (length xs)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   745
by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   746
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   747
(*injection into the field of a cardinal*)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   748
definition "toCard_pred A r f \<equiv> inj_on f A \<and> f ` A \<subseteq> Field r \<and> Card_order r"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   749
definition "toCard A r \<equiv> SOME f. toCard_pred A r f"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   750
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   751
lemma ex_toCard_pred:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   752
"\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> \<exists> f. toCard_pred A r f"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   753
unfolding toCard_pred_def
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   754
using card_of_ordLeq[of A "Field r"]
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   755
      ordLeq_ordIso_trans[OF _ card_of_unique[of "Field r" r], of "|A|"]
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   756
by blast
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   757
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   758
lemma toCard_pred_toCard:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   759
  "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> toCard_pred A r (toCard A r)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   760
unfolding toCard_def using someI_ex[OF ex_toCard_pred] .
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   761
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   762
lemma toCard_inj: "\<lbrakk>|A| \<le>o r; Card_order r; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   763
  toCard A r x = toCard A r y \<longleftrightarrow> x = y"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   764
using toCard_pred_toCard unfolding inj_on_def toCard_pred_def by blast
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   765
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   766
lemma toCard: "\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> toCard A r b \<in> Field r"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   767
using toCard_pred_toCard unfolding toCard_pred_def by blast
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   768
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   769
definition "fromCard A r k \<equiv> SOME b. b \<in> A \<and> toCard A r b = k"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   770
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   771
lemma fromCard_toCard:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   772
"\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> fromCard A r (toCard A r b) = b"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   773
unfolding fromCard_def by (rule some_equality) (auto simp add: toCard_inj)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   774
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   775
(* pick according to the weak pullback *)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   776
definition pickWP_pred where
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   777
"pickWP_pred A p1 p2 b1 b2 a \<equiv>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   778
 a \<in> A \<and> p1 a = b1 \<and> p2 a = b2"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   779
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   780
definition pickWP where
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   781
"pickWP A p1 p2 b1 b2 \<equiv>
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   782
 SOME a. pickWP_pred A p1 p2 b1 b2 a"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   783
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   784
lemma pickWP_pred:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   785
assumes "wpull A B1 B2 f1 f2 p1 p2" and
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   786
"b1 \<in> B1" and "b2 \<in> B2" and "f1 b1 = f2 b2"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   787
shows "\<exists> a. pickWP_pred A p1 p2 b1 b2 a"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   788
using assms unfolding wpull_def pickWP_pred_def by blast
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   789
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   790
lemma pickWP_pred_pickWP:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   791
assumes "wpull A B1 B2 f1 f2 p1 p2" and
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   792
"b1 \<in> B1" and "b2 \<in> B2" and "f1 b1 = f2 b2"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   793
shows "pickWP_pred A p1 p2 b1 b2 (pickWP A p1 p2 b1 b2)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   794
unfolding pickWP_def using assms by(rule someI_ex[OF pickWP_pred])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   795
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   796
lemma pickWP:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   797
assumes "wpull A B1 B2 f1 f2 p1 p2" and
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   798
"b1 \<in> B1" and "b2 \<in> B2" and "f1 b1 = f2 b2"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   799
shows "pickWP A p1 p2 b1 b2 \<in> A"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   800
      "p1 (pickWP A p1 p2 b1 b2) = b1"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   801
      "p2 (pickWP A p1 p2 b1 b2) = b2"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   802
using assms pickWP_pred_pickWP unfolding pickWP_pred_def by fastforce+
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   803
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   804
lemma ssubst_mem: "\<lbrakk>t = s; s \<in> X\<rbrakk> \<Longrightarrow> t \<in> X" by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   805
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   806
lemma Inl_Field_csum: "a \<in> Field r \<Longrightarrow> Inl a \<in> Field (r +c s)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   807
unfolding Field_card_of csum_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   808
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   809
lemma Inr_Field_csum: "a \<in> Field s \<Longrightarrow> Inr a \<in> Field (r +c s)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   810
unfolding Field_card_of csum_def by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   811
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   812
lemma nat_rec_0: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   813
by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   814
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   815
lemma nat_rec_Suc: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   816
by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   817
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   818
lemma list_rec_Nil: "f = list_rec f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   819
by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   820
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   821
lemma list_rec_Cons: "f = list_rec f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   822
by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   823
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   824
lemma sum_case_cong: "p = q \<Longrightarrow> sum_case f g p = sum_case f g q"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   825
by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   826
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   827
lemma sum_case_step:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   828
  "sum_case (sum_case f' g') g (Inl p) = sum_case f' g' p"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   829
  "sum_case f (sum_case f' g') (Inr p) = sum_case f' g' p"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   830
by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   831
49255
2ecc533d6697 use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents: 49125
diff changeset
   832
lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
2ecc533d6697 use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents: 49125
diff changeset
   833
by simp
2ecc533d6697 use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents: 49125
diff changeset
   834
49263
669a820ef213 fixed general case of "mk_sumEN_balanced"
blanchet
parents: 49255
diff changeset
   835
lemma obj_one_pointE: "\<forall>x. s = x \<longrightarrow> P \<Longrightarrow> P"
669a820ef213 fixed general case of "mk_sumEN_balanced"
blanchet
parents: 49255
diff changeset
   836
by blast
669a820ef213 fixed general case of "mk_sumEN_balanced"
blanchet
parents: 49255
diff changeset
   837
49255
2ecc533d6697 use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents: 49125
diff changeset
   838
lemma obj_sumE_f:
2ecc533d6697 use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents: 49125
diff changeset
   839
"\<lbrakk>\<forall>x. s = f (Inl x) \<longrightarrow> P; \<forall>x. s = f (Inr x) \<longrightarrow> P\<rbrakk> \<Longrightarrow> \<forall>x. s = f x \<longrightarrow> P"
2ecc533d6697 use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents: 49125
diff changeset
   840
by (metis sum.exhaust)
2ecc533d6697 use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents: 49125
diff changeset
   841
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   842
lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   843
by (cases s) auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   844
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   845
lemma obj_sum_step:
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   846
  "\<lbrakk>\<forall>x. s = f (Inr (Inl x)) \<longrightarrow> P; \<forall>x. s = f (Inr (Inr x)) \<longrightarrow> P\<rbrakk> \<Longrightarrow> \<forall>x. s = f (Inr x) \<longrightarrow> P"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   847
by (metis obj_sumE)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   848
49274
ddd606ec45b9 first step towards splitting corecursor function arguments into (p, g, h) triples
blanchet
parents: 49263
diff changeset
   849
lemma sum_case_if:
ddd606ec45b9 first step towards splitting corecursor function arguments into (p, g, h) triples
blanchet
parents: 49263
diff changeset
   850
"sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)"
ddd606ec45b9 first step towards splitting corecursor function arguments into (p, g, h) triples
blanchet
parents: 49263
diff changeset
   851
by simp
ddd606ec45b9 first step towards splitting corecursor function arguments into (p, g, h) triples
blanchet
parents: 49263
diff changeset
   852
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   853
lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
49255
2ecc533d6697 use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents: 49125
diff changeset
   854
by simp
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   855
49283
97809ae5f7bb move "bnf_util.ML" to "BNF_Util.thy"
blanchet
parents: 49282
diff changeset
   856
ML_file "Tools/bnf_util.ML"
97809ae5f7bb move "bnf_util.ML" to "BNF_Util.thy"
blanchet
parents: 49282
diff changeset
   857
ML_file "Tools/bnf_tactics.ML"
97809ae5f7bb move "bnf_util.ML" to "BNF_Util.thy"
blanchet
parents: 49282
diff changeset
   858
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   859
end