src/HOL/Basic_BNFs.thy
author blanchet
Mon, 20 Jan 2014 20:21:12 +0100
changeset 55083 0a689157e3ce
parent 55075 b3d0a02a756d
child 55084 8ee9aabb2bca
permissions -rw-r--r--
move BNF_LFP up the dependency chain
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
55075
b3d0a02a756d dissolved BNF session
blanchet
parents: 55062
diff changeset
     1
(*  Title:      HOL/Basic_BNFs.thy
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     2
    Author:     Dmitriy Traytel, TU Muenchen
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     3
    Author:     Andrei Popescu, TU Muenchen
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     4
    Author:     Jasmin Blanchette, TU Muenchen
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     5
    Copyright   2012
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     6
49309
f20b24214ac2 split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents: 49236
diff changeset
     7
Registration of basic types as bounded natural functors.
48975
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
49309
f20b24214ac2 split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents: 49236
diff changeset
    10
header {* Registration of Basic Types as Bounded Natural Functors *}
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    11
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    12
theory Basic_BNFs
49310
6e30078de4f0 renamed "Ordinals_and_Cardinals" to "Cardinals"
blanchet
parents: 49309
diff changeset
    13
imports BNF_Def
54581
1502a1f707d9 eliminated dependence of Cardinals_FP on Set_Intervals, more precise imports
traytel
parents: 54578
diff changeset
    14
   (*FIXME: define relators here, reuse in Lifting_* once this theory is in HOL*)
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    15
begin
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    16
54421
632be352a5a3 more explicit syntax for defining a bnf
traytel
parents: 54191
diff changeset
    17
bnf ID: 'a
632be352a5a3 more explicit syntax for defining a bnf
traytel
parents: 54191
diff changeset
    18
  map: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
632be352a5a3 more explicit syntax for defining a bnf
traytel
parents: 54191
diff changeset
    19
  sets: "\<lambda>x. {x}"
632be352a5a3 more explicit syntax for defining a bnf
traytel
parents: 54191
diff changeset
    20
  bd: natLeq
632be352a5a3 more explicit syntax for defining a bnf
traytel
parents: 54191
diff changeset
    21
  rel: "id :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
    22
apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite)
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    23
apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
49453
ff0e540d8758 add rel as first-class citizen of BNF
blanchet
parents: 49451
diff changeset
    24
apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3]
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    25
done
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    26
54421
632be352a5a3 more explicit syntax for defining a bnf
traytel
parents: 54191
diff changeset
    27
bnf DEADID: 'a
632be352a5a3 more explicit syntax for defining a bnf
traytel
parents: 54191
diff changeset
    28
  map: "id :: 'a \<Rightarrow> 'a"
632be352a5a3 more explicit syntax for defining a bnf
traytel
parents: 54191
diff changeset
    29
  bd: "natLeq +c |UNIV :: 'a set|"
632be352a5a3 more explicit syntax for defining a bnf
traytel
parents: 54191
diff changeset
    30
  rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
54841
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54581
diff changeset
    31
by (auto simp add: Grp_def
51446
a6ebb12cc003 hide internal constants; tuned proofs
traytel
parents: 49510
diff changeset
    32
  card_order_csum natLeq_card_order card_of_card_order_on
a6ebb12cc003 hide internal constants; tuned proofs
traytel
parents: 49510
diff changeset
    33
  cinfinite_csum natLeq_cinfinite)
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    34
49451
7a28d22c33c6 renamed "sum_setl" to "setl" and similarly for r
blanchet
parents: 49450
diff changeset
    35
definition setl :: "'a + 'b \<Rightarrow> 'a set" where
7a28d22c33c6 renamed "sum_setl" to "setl" and similarly for r
blanchet
parents: 49450
diff changeset
    36
"setl x = (case x of Inl z => {z} | _ => {})"
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    37
49451
7a28d22c33c6 renamed "sum_setl" to "setl" and similarly for r
blanchet
parents: 49450
diff changeset
    38
definition setr :: "'a + 'b \<Rightarrow> 'b set" where
7a28d22c33c6 renamed "sum_setl" to "setl" and similarly for r
blanchet
parents: 49450
diff changeset
    39
"setr x = (case x of Inr z => {z} | _ => {})"
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    40
49451
7a28d22c33c6 renamed "sum_setl" to "setl" and similarly for r
blanchet
parents: 49450
diff changeset
    41
lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def]
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    42
55083
0a689157e3ce move BNF_LFP up the dependency chain
blanchet
parents: 55075
diff changeset
    43
definition
0a689157e3ce move BNF_LFP up the dependency chain
blanchet
parents: 55075
diff changeset
    44
   sum_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
0a689157e3ce move BNF_LFP up the dependency chain
blanchet
parents: 55075
diff changeset
    45
where
0a689157e3ce move BNF_LFP up the dependency chain
blanchet
parents: 55075
diff changeset
    46
   "sum_rel R1 R2 x y =
0a689157e3ce move BNF_LFP up the dependency chain
blanchet
parents: 55075
diff changeset
    47
     (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
0a689157e3ce move BNF_LFP up the dependency chain
blanchet
parents: 55075
diff changeset
    48
     | (Inr x, Inr y) \<Rightarrow> R2 x y
0a689157e3ce move BNF_LFP up the dependency chain
blanchet
parents: 55075
diff changeset
    49
     | _ \<Rightarrow> False)"
0a689157e3ce move BNF_LFP up the dependency chain
blanchet
parents: 55075
diff changeset
    50
0a689157e3ce move BNF_LFP up the dependency chain
blanchet
parents: 55075
diff changeset
    51
lemma sum_rel_simps[simp]:
0a689157e3ce move BNF_LFP up the dependency chain
blanchet
parents: 55075
diff changeset
    52
  "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
0a689157e3ce move BNF_LFP up the dependency chain
blanchet
parents: 55075
diff changeset
    53
  "sum_rel R1 R2 (Inl a1) (Inr b2) = False"
0a689157e3ce move BNF_LFP up the dependency chain
blanchet
parents: 55075
diff changeset
    54
  "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
0a689157e3ce move BNF_LFP up the dependency chain
blanchet
parents: 55075
diff changeset
    55
  "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
0a689157e3ce move BNF_LFP up the dependency chain
blanchet
parents: 55075
diff changeset
    56
  unfolding sum_rel_def by simp_all
0a689157e3ce move BNF_LFP up the dependency chain
blanchet
parents: 55075
diff changeset
    57
54421
632be352a5a3 more explicit syntax for defining a bnf
traytel
parents: 54191
diff changeset
    58
bnf "'a + 'b"
632be352a5a3 more explicit syntax for defining a bnf
traytel
parents: 54191
diff changeset
    59
  map: sum_map
632be352a5a3 more explicit syntax for defining a bnf
traytel
parents: 54191
diff changeset
    60
  sets: setl setr
632be352a5a3 more explicit syntax for defining a bnf
traytel
parents: 54191
diff changeset
    61
  bd: natLeq
632be352a5a3 more explicit syntax for defining a bnf
traytel
parents: 54191
diff changeset
    62
  wits: Inl Inr
632be352a5a3 more explicit syntax for defining a bnf
traytel
parents: 54191
diff changeset
    63
  rel: sum_rel
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    64
proof -
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    65
  show "sum_map id id = id" by (rule sum_map.id)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    66
next
54486
d8d276c922f2 tuned proofs
blanchet
parents: 54485
diff changeset
    67
  fix f1 :: "'o \<Rightarrow> 's" and f2 :: "'p \<Rightarrow> 't" and g1 :: "'s \<Rightarrow> 'q" and g2 :: "'t \<Rightarrow> 'r"
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    68
  show "sum_map (g1 o f1) (g2 o f2) = sum_map g1 g2 o sum_map f1 f2"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    69
    by (rule sum_map.comp[symmetric])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    70
next
54486
d8d276c922f2 tuned proofs
blanchet
parents: 54485
diff changeset
    71
  fix x and f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r" and g1 g2
49451
7a28d22c33c6 renamed "sum_setl" to "setl" and similarly for r
blanchet
parents: 49450
diff changeset
    72
  assume a1: "\<And>z. z \<in> setl x \<Longrightarrow> f1 z = g1 z" and
7a28d22c33c6 renamed "sum_setl" to "setl" and similarly for r
blanchet
parents: 49450
diff changeset
    73
         a2: "\<And>z. z \<in> setr x \<Longrightarrow> f2 z = g2 z"
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    74
  thus "sum_map f1 f2 x = sum_map g1 g2 x"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    75
  proof (cases x)
49451
7a28d22c33c6 renamed "sum_setl" to "setl" and similarly for r
blanchet
parents: 49450
diff changeset
    76
    case Inl thus ?thesis using a1 by (clarsimp simp: setl_def)
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    77
  next
49451
7a28d22c33c6 renamed "sum_setl" to "setl" and similarly for r
blanchet
parents: 49450
diff changeset
    78
    case Inr thus ?thesis using a2 by (clarsimp simp: setr_def)
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    79
  qed
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    80
next
54486
d8d276c922f2 tuned proofs
blanchet
parents: 54485
diff changeset
    81
  fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
49451
7a28d22c33c6 renamed "sum_setl" to "setl" and similarly for r
blanchet
parents: 49450
diff changeset
    82
  show "setl o sum_map f1 f2 = image f1 o setl"
7a28d22c33c6 renamed "sum_setl" to "setl" and similarly for r
blanchet
parents: 49450
diff changeset
    83
    by (rule ext, unfold o_apply) (simp add: setl_def split: sum.split)
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    84
next
54486
d8d276c922f2 tuned proofs
blanchet
parents: 54485
diff changeset
    85
  fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
49451
7a28d22c33c6 renamed "sum_setl" to "setl" and similarly for r
blanchet
parents: 49450
diff changeset
    86
  show "setr o sum_map f1 f2 = image f2 o setr"
7a28d22c33c6 renamed "sum_setl" to "setl" and similarly for r
blanchet
parents: 49450
diff changeset
    87
    by (rule ext, unfold o_apply) (simp add: setr_def split: sum.split)
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    88
next
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    89
  show "card_order natLeq" by (rule natLeq_card_order)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    90
next
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    91
  show "cinfinite natLeq" by (rule natLeq_cinfinite)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    92
next
54486
d8d276c922f2 tuned proofs
blanchet
parents: 54485
diff changeset
    93
  fix x :: "'o + 'p"
49451
7a28d22c33c6 renamed "sum_setl" to "setl" and similarly for r
blanchet
parents: 49450
diff changeset
    94
  show "|setl x| \<le>o natLeq"
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    95
    apply (rule ordLess_imp_ordLeq)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    96
    apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
49451
7a28d22c33c6 renamed "sum_setl" to "setl" and similarly for r
blanchet
parents: 49450
diff changeset
    97
    by (simp add: setl_def split: sum.split)
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    98
next
54486
d8d276c922f2 tuned proofs
blanchet
parents: 54485
diff changeset
    99
  fix x :: "'o + 'p"
49451
7a28d22c33c6 renamed "sum_setl" to "setl" and similarly for r
blanchet
parents: 49450
diff changeset
   100
  show "|setr x| \<le>o natLeq"
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   101
    apply (rule ordLess_imp_ordLeq)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   102
    apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
49451
7a28d22c33c6 renamed "sum_setl" to "setl" and similarly for r
blanchet
parents: 49450
diff changeset
   103
    by (simp add: setr_def split: sum.split)
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   104
next
54841
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54581
diff changeset
   105
  fix R1 R2 S1 S2
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54581
diff changeset
   106
  show "sum_rel R1 R2 OO sum_rel S1 S2 \<le> sum_rel (R1 OO S1) (R2 OO S2)"
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54581
diff changeset
   107
    by (auto simp: sum_rel_def split: sum.splits)
49453
ff0e540d8758 add rel as first-class citizen of BNF
blanchet
parents: 49451
diff changeset
   108
next
ff0e540d8758 add rel as first-class citizen of BNF
blanchet
parents: 49451
diff changeset
   109
  fix R S
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   110
  show "sum_rel R S =
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   111
        (Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (sum_map fst fst))\<inverse>\<inverse> OO
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   112
        Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (sum_map snd snd)"
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   113
  unfolding setl_def setr_def sum_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff
49453
ff0e540d8758 add rel as first-class citizen of BNF
blanchet
parents: 49451
diff changeset
   114
  by (fastforce split: sum.splits)
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   115
qed (auto simp: sum_set_defs)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   116
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   117
definition fsts :: "'a \<times> 'b \<Rightarrow> 'a set" where
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   118
"fsts x = {fst x}"
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
definition snds :: "'a \<times> 'b \<Rightarrow> 'b set" where
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   121
"snds x = {snd x}"
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
lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def]
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   124
55083
0a689157e3ce move BNF_LFP up the dependency chain
blanchet
parents: 55075
diff changeset
   125
definition
0a689157e3ce move BNF_LFP up the dependency chain
blanchet
parents: 55075
diff changeset
   126
  prod_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool"
0a689157e3ce move BNF_LFP up the dependency chain
blanchet
parents: 55075
diff changeset
   127
where
0a689157e3ce move BNF_LFP up the dependency chain
blanchet
parents: 55075
diff changeset
   128
  "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
0a689157e3ce move BNF_LFP up the dependency chain
blanchet
parents: 55075
diff changeset
   129
0a689157e3ce move BNF_LFP up the dependency chain
blanchet
parents: 55075
diff changeset
   130
lemma prod_rel_apply [simp]:
0a689157e3ce move BNF_LFP up the dependency chain
blanchet
parents: 55075
diff changeset
   131
  "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
0a689157e3ce move BNF_LFP up the dependency chain
blanchet
parents: 55075
diff changeset
   132
  by (simp add: prod_rel_def)
0a689157e3ce move BNF_LFP up the dependency chain
blanchet
parents: 55075
diff changeset
   133
54421
632be352a5a3 more explicit syntax for defining a bnf
traytel
parents: 54191
diff changeset
   134
bnf "'a \<times> 'b"
632be352a5a3 more explicit syntax for defining a bnf
traytel
parents: 54191
diff changeset
   135
  map: map_pair
632be352a5a3 more explicit syntax for defining a bnf
traytel
parents: 54191
diff changeset
   136
  sets: fsts snds
632be352a5a3 more explicit syntax for defining a bnf
traytel
parents: 54191
diff changeset
   137
  bd: natLeq
632be352a5a3 more explicit syntax for defining a bnf
traytel
parents: 54191
diff changeset
   138
  rel: prod_rel
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   139
proof (unfold prod_set_defs)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   140
  show "map_pair id id = id" by (rule map_pair.id)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   141
next
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   142
  fix f1 f2 g1 g2
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   143
  show "map_pair (g1 o f1) (g2 o f2) = map_pair g1 g2 o map_pair f1 f2"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   144
    by (rule map_pair.comp[symmetric])
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   145
next
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   146
  fix x f1 f2 g1 g2
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   147
  assume "\<And>z. z \<in> {fst x} \<Longrightarrow> f1 z = g1 z" "\<And>z. z \<in> {snd x} \<Longrightarrow> f2 z = g2 z"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   148
  thus "map_pair f1 f2 x = map_pair g1 g2 x" by (cases x) simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   149
next
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   150
  fix f1 f2
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   151
  show "(\<lambda>x. {fst x}) o map_pair f1 f2 = image f1 o (\<lambda>x. {fst x})"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   152
    by (rule ext, unfold o_apply) simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   153
next
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   154
  fix f1 f2
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   155
  show "(\<lambda>x. {snd x}) o map_pair f1 f2 = image f2 o (\<lambda>x. {snd x})"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   156
    by (rule ext, unfold o_apply) simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   157
next
52635
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 52545
diff changeset
   158
  show "card_order natLeq" by (rule natLeq_card_order)
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   159
next
52635
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 52545
diff changeset
   160
  show "cinfinite natLeq" by (rule natLeq_cinfinite)
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   161
next
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   162
  fix x
52635
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 52545
diff changeset
   163
  show "|{fst x}| \<le>o natLeq"
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 52545
diff changeset
   164
    by (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq finite.emptyI finite_insert)
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   165
next
52635
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 52545
diff changeset
   166
  fix x
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 52545
diff changeset
   167
  show "|{snd x}| \<le>o natLeq"
4f84b730c489 got rid of in_bd BNF property (derivable from set_bd+map_cong+map_comp+map_id)
traytel
parents: 52545
diff changeset
   168
    by (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq finite.emptyI finite_insert)
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   169
next
54841
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54581
diff changeset
   170
  fix R1 R2 S1 S2
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54581
diff changeset
   171
  show "prod_rel R1 R2 OO prod_rel S1 S2 \<le> prod_rel (R1 OO S1) (R2 OO S2)" by auto
49453
ff0e540d8758 add rel as first-class citizen of BNF
blanchet
parents: 49451
diff changeset
   172
next
ff0e540d8758 add rel as first-class citizen of BNF
blanchet
parents: 49451
diff changeset
   173
  fix R S
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   174
  show "prod_rel R S =
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   175
        (Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_pair fst fst))\<inverse>\<inverse> OO
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   176
        Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_pair snd snd)"
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   177
  unfolding prod_set_defs prod_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff
49453
ff0e540d8758 add rel as first-class citizen of BNF
blanchet
parents: 49451
diff changeset
   178
  by auto
54189
c0186a0d8cb3 define a trivial nonemptiness witness if none is provided
traytel
parents: 53026
diff changeset
   179
qed
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   180
54421
632be352a5a3 more explicit syntax for defining a bnf
traytel
parents: 54191
diff changeset
   181
bnf "'a \<Rightarrow> 'b"
632be352a5a3 more explicit syntax for defining a bnf
traytel
parents: 54191
diff changeset
   182
  map: "op \<circ>"
632be352a5a3 more explicit syntax for defining a bnf
traytel
parents: 54191
diff changeset
   183
  sets: range
632be352a5a3 more explicit syntax for defining a bnf
traytel
parents: 54191
diff changeset
   184
  bd: "natLeq +c |UNIV :: 'a set|"
632be352a5a3 more explicit syntax for defining a bnf
traytel
parents: 54191
diff changeset
   185
  rel: "fun_rel op ="
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   186
proof
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   187
  fix f show "id \<circ> f = id f" by simp
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   188
next
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   189
  fix f g show "op \<circ> (g \<circ> f) = op \<circ> g \<circ> op \<circ> f"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   190
  unfolding comp_def[abs_def] ..
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   191
next
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   192
  fix x f g
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   193
  assume "\<And>z. z \<in> range x \<Longrightarrow> f z = g z"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   194
  thus "f \<circ> x = g \<circ> x" by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   195
next
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   196
  fix f show "range \<circ> op \<circ> f = op ` f \<circ> range"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   197
  unfolding image_def comp_def[abs_def] by auto
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   198
next
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   199
  show "card_order (natLeq +c |UNIV| )" (is "_ (_ +c ?U)")
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   200
  apply (rule card_order_csum)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   201
  apply (rule natLeq_card_order)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   202
  by (rule card_of_card_order_on)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   203
(*  *)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   204
  show "cinfinite (natLeq +c ?U)"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   205
    apply (rule cinfinite_csum)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   206
    apply (rule disjI1)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   207
    by (rule natLeq_cinfinite)
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   208
next
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   209
  fix f :: "'d => 'a"
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   210
  have "|range f| \<le>o | (UNIV::'d set) |" (is "_ \<le>o ?U") by (rule card_of_image)
54486
d8d276c922f2 tuned proofs
blanchet
parents: 54485
diff changeset
   211
  also have "?U \<le>o natLeq +c ?U" by (rule ordLeq_csum2) (rule card_of_Card_order)
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   212
  finally show "|range f| \<le>o natLeq +c ?U" .
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   213
next
54841
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54581
diff changeset
   214
  fix R S
af71b753c459 express weak pullback property of bnfs only in terms of the relator
traytel
parents: 54581
diff changeset
   215
  show "fun_rel op = R OO fun_rel op = S \<le> fun_rel op = (R OO S)" by (auto simp: fun_rel_def)
49453
ff0e540d8758 add rel as first-class citizen of BNF
blanchet
parents: 49451
diff changeset
   216
next
49463
83ac281bcdc2 provide predicator, define relator
blanchet
parents: 49455
diff changeset
   217
  fix R
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   218
  show "fun_rel op = R =
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   219
        (Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> fst))\<inverse>\<inverse> OO
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   220
         Grp {x. range x \<subseteq> Collect (split R)} (op \<circ> snd)"
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51836
diff changeset
   221
  unfolding fun_rel_def Grp_def fun_eq_iff relcompp.simps conversep.simps  subset_iff image_iff
54486
d8d276c922f2 tuned proofs
blanchet
parents: 54485
diff changeset
   222
  by auto (force, metis (no_types) pair_collapse)
54189
c0186a0d8cb3 define a trivial nonemptiness witness if none is provided
traytel
parents: 53026
diff changeset
   223
qed
54191
7fba375a7e7d removed junk
traytel
parents: 54189
diff changeset
   224
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   225
end