src/HOL/BNF_Greatest_Fixpoint.thy
author wenzelm
Mon, 12 Apr 2021 14:14:47 +0200
changeset 73563 55b66a45bc94
parent 69913 ca515cf61651
child 75624 22d1c5f2b9f4
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58128
43a1ba26a8cb renamed BNF theories
blanchet
parents: 58104
diff changeset
     1
(*  Title:      HOL/BNF_Greatest_Fixpoint.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
55059
ef2e0fb783c6 tuned comments
blanchet
parents: 55058
diff changeset
     3
    Author:     Lorenz Panny, TU Muenchen
ef2e0fb783c6 tuned comments
blanchet
parents: 55058
diff changeset
     4
    Author:     Jasmin Blanchette, TU Muenchen
57698
afef6616cbae header tuning
blanchet
parents: 55966
diff changeset
     5
    Copyright   2012, 2013, 2014
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     6
58352
37745650a3f4 register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents: 58128
diff changeset
     7
Greatest fixpoint (codatatype) operation on 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
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
    10
section \<open>Greatest Fixpoint (Codatatype) Operation on Bounded Natural Functors\<close>
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    11
58128
43a1ba26a8cb renamed BNF theories
blanchet
parents: 58104
diff changeset
    12
theory BNF_Greatest_Fixpoint
43a1ba26a8cb renamed BNF theories
blanchet
parents: 58104
diff changeset
    13
imports BNF_Fixpoint_Base String
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    14
keywords
69913
ca515cf61651 more specific keyword kinds;
wenzelm
parents: 69605
diff changeset
    15
  "codatatype" :: thy_defn and
ca515cf61651 more specific keyword kinds;
wenzelm
parents: 69605
diff changeset
    16
  "primcorecursive" :: thy_goal_defn and
ca515cf61651 more specific keyword kinds;
wenzelm
parents: 69605
diff changeset
    17
  "primcorec" :: thy_defn
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
66248
df85956228c2 added command 'alias' and 'type_alias';
wenzelm
parents: 64413
diff changeset
    20
alias proj = Equiv_Relations.proj
55024
05cc0dbf3a50 hide short const name
blanchet
parents: 55022
diff changeset
    21
55966
972f0aa7091b balance tuples that represent curried functions
blanchet
parents: 55945
diff changeset
    22
lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
    23
  by simp
55966
972f0aa7091b balance tuples that represent curried functions
blanchet
parents: 55945
diff changeset
    24
972f0aa7091b balance tuples that represent curried functions
blanchet
parents: 55945
diff changeset
    25
lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
    26
  by (cases s) auto
55966
972f0aa7091b balance tuples that represent curried functions
blanchet
parents: 55945
diff changeset
    27
54485
b61b8c9e4cf7 killed more needless theorems
blanchet
parents: 54484
diff changeset
    28
lemma not_TrueE: "\<not> True \<Longrightarrow> P"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
    29
  by (erule notE, rule TrueI)
54485
b61b8c9e4cf7 killed more needless theorems
blanchet
parents: 54484
diff changeset
    30
b61b8c9e4cf7 killed more needless theorems
blanchet
parents: 54484
diff changeset
    31
lemma neq_eq_eq_contradict: "\<lbrakk>t \<noteq> u; s = t; s = u\<rbrakk> \<Longrightarrow> P"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
    32
  by fast
54485
b61b8c9e4cf7 killed more needless theorems
blanchet
parents: 54484
diff changeset
    33
67613
ce654b0e6d69 more symbols;
wenzelm
parents: 67091
diff changeset
    34
lemma converse_Times: "(A \<times> B)\<inverse> = B \<times> A"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
    35
  by fast
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    36
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    37
lemma equiv_proj:
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
    38
  assumes e: "equiv A R" and m: "z \<in> R"
67091
1393c2340eec more symbols;
wenzelm
parents: 66248
diff changeset
    39
  shows "(proj R \<circ> fst) z = (proj R \<circ> snd) z"
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    40
proof -
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
    41
  from m have z: "(fst z, snd z) \<in> R" by auto
53695
a66d211ab34e tuned proofs
traytel
parents: 53469
diff changeset
    42
  with e have "\<And>x. (fst z, x) \<in> R \<Longrightarrow> (snd z, x) \<in> R" "\<And>x. (snd z, x) \<in> R \<Longrightarrow> (fst z, x) \<in> R"
a66d211ab34e tuned proofs
traytel
parents: 53469
diff changeset
    43
    unfolding equiv_def sym_def trans_def by blast+
a66d211ab34e tuned proofs
traytel
parents: 53469
diff changeset
    44
  then show ?thesis unfolding proj_def[abs_def] by auto
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    45
qed
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    46
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    47
(* Operators: *)
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    48
definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    49
51447
a19e973fa2cf eliminate duplicated constant (diag vs. Id_on)
traytel
parents: 51446
diff changeset
    50
lemma Id_on_Gr: "Id_on A = Gr A id"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
    51
  unfolding Id_on_def Gr_def by auto
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    52
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    53
lemma image2_eqI: "\<lbrakk>b = f x; c = g x; x \<in> A\<rbrakk> \<Longrightarrow> (b, c) \<in> image2 A f g"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
    54
  unfolding image2_def by auto
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    55
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    56
lemma IdD: "(a, b) \<in> Id \<Longrightarrow> a = b"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
    57
  by auto
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    58
67613
ce654b0e6d69 more symbols;
wenzelm
parents: 67091
diff changeset
    59
lemma image2_Gr: "image2 A f g = (Gr A f)\<inverse> O (Gr A g)"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
    60
  unfolding image2_def Gr_def by auto
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    61
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    62
lemma GrD1: "(x, fx) \<in> Gr A f \<Longrightarrow> x \<in> A"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
    63
  unfolding Gr_def by simp
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    64
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    65
lemma GrD2: "(x, fx) \<in> Gr A f \<Longrightarrow> f x = fx"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
    66
  unfolding Gr_def by simp
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    67
61943
7fba644ed827 discontinued ASCII replacement syntax <*>;
wenzelm
parents: 61424
diff changeset
    68
lemma Gr_incl: "Gr A f \<subseteq> A \<times> B \<longleftrightarrow> f ` A \<subseteq> B"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
    69
  unfolding Gr_def by auto
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    70
54485
b61b8c9e4cf7 killed more needless theorems
blanchet
parents: 54484
diff changeset
    71
lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
    72
  by blast
54485
b61b8c9e4cf7 killed more needless theorems
blanchet
parents: 54484
diff changeset
    73
b61b8c9e4cf7 killed more needless theorems
blanchet
parents: 54484
diff changeset
    74
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})"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
    75
  by blast
54485
b61b8c9e4cf7 killed more needless theorems
blanchet
parents: 54484
diff changeset
    76
61424
c3658c18b7bc prod_case as canonical name for product type eliminator
haftmann
parents: 61032
diff changeset
    77
lemma in_rel_Collect_case_prod_eq: "in_rel (Collect (case_prod X)) = X"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
    78
  unfolding fun_eq_iff by auto
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
    79
61424
c3658c18b7bc prod_case as canonical name for product type eliminator
haftmann
parents: 61032
diff changeset
    80
lemma Collect_case_prod_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (case_prod (in_rel Y))"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
    81
  by auto
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
    82
61424
c3658c18b7bc prod_case as canonical name for product type eliminator
haftmann
parents: 61032
diff changeset
    83
lemma Collect_case_prod_in_rel_leE: "X \<subseteq> Collect (case_prod (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
    84
  by force
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
    85
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
    86
lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
    87
  unfolding fun_eq_iff by auto
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
    88
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
    89
lemma relcompp_in_rel: "in_rel R OO in_rel S = in_rel (R O S)"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
    90
  unfolding fun_eq_iff by auto
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
    91
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
    92
lemma in_rel_Gr: "in_rel (Gr A f) = Grp A f"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
    93
  unfolding Gr_def Grp_def fun_eq_iff by auto
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
    94
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    95
definition relImage where
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
    96
  "relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}"
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    97
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    98
definition relInvImage where
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
    99
  "relInvImage A R f \<equiv> {(a1, a2) | a1 a2. a1 \<in> A \<and> a2 \<in> A \<and> (f a1, f a2) \<in> R}"
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   100
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   101
lemma relImage_Gr:
67613
ce654b0e6d69 more symbols;
wenzelm
parents: 67091
diff changeset
   102
  "\<lbrakk>R \<subseteq> A \<times> A\<rbrakk> \<Longrightarrow> relImage R f = (Gr A f)\<inverse> O R O Gr A f"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   103
  unfolding relImage_def Gr_def relcomp_def by auto
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   104
67613
ce654b0e6d69 more symbols;
wenzelm
parents: 67091
diff changeset
   105
lemma relInvImage_Gr: "\<lbrakk>R \<subseteq> B \<times> B\<rbrakk> \<Longrightarrow> relInvImage A R f = Gr A f O R O (Gr A f)\<inverse>"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   106
  unfolding Gr_def relcomp_def image_def relInvImage_def by auto
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   107
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   108
lemma relImage_mono:
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   109
  "R1 \<subseteq> R2 \<Longrightarrow> relImage R1 f \<subseteq> relImage R2 f"
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   110
  unfolding relImage_def by auto
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   111
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   112
lemma relInvImage_mono:
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   113
  "R1 \<subseteq> R2 \<Longrightarrow> relInvImage A R1 f \<subseteq> relInvImage A R2 f"
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   114
  unfolding relInvImage_def by auto
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   115
51447
a19e973fa2cf eliminate duplicated constant (diag vs. Id_on)
traytel
parents: 51446
diff changeset
   116
lemma relInvImage_Id_on:
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   117
  "(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (Id_on B) f \<subseteq> Id"
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   118
  unfolding relInvImage_def Id_on_def by auto
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   119
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   120
lemma relInvImage_UNIV_relImage:
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   121
  "R \<subseteq> relInvImage UNIV (relImage R f) f"
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   122
  unfolding relInvImage_def relImage_def by auto
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   123
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   124
lemma relImage_proj:
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   125
  assumes "equiv A R"
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   126
  shows "relImage R (proj R) \<subseteq> Id_on (A//R)"
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   127
  unfolding relImage_def Id_on_def
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   128
  using proj_iff[OF assms] equiv_class_eq_iff[OF assms]
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   129
  by (auto simp: proj_preserves)
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   130
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   131
lemma relImage_relInvImage:
61943
7fba644ed827 discontinued ASCII replacement syntax <*>;
wenzelm
parents: 61424
diff changeset
   132
  assumes "R \<subseteq> f ` A \<times> f ` A"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   133
  shows "relImage (relInvImage A R f) f = R"
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   134
  using assms unfolding relImage_def relInvImage_def by fast
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   135
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   136
lemma subst_Pair: "P x y \<Longrightarrow> a = (x, y) \<Longrightarrow> P (fst a) (snd a)"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   137
  by simp
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   138
64413
blanchet
parents: 62905
diff changeset
   139
lemma fst_diag_id: "(fst \<circ> (\<lambda>x. (x, x))) z = id z" by simp
blanchet
parents: 62905
diff changeset
   140
lemma snd_diag_id: "(snd \<circ> (\<lambda>x. (x, x))) z = id z" by simp
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   141
67091
1393c2340eec more symbols;
wenzelm
parents: 66248
diff changeset
   142
lemma fst_diag_fst: "fst \<circ> ((\<lambda>x. (x, x)) \<circ> fst) = fst" by auto
1393c2340eec more symbols;
wenzelm
parents: 66248
diff changeset
   143
lemma snd_diag_fst: "snd \<circ> ((\<lambda>x. (x, x)) \<circ> fst) = fst" by auto
1393c2340eec more symbols;
wenzelm
parents: 66248
diff changeset
   144
lemma fst_diag_snd: "fst \<circ> ((\<lambda>x. (x, x)) \<circ> snd) = snd" by auto
1393c2340eec more symbols;
wenzelm
parents: 66248
diff changeset
   145
lemma snd_diag_snd: "snd \<circ> ((\<lambda>x. (x, x)) \<circ> snd) = snd" by auto
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   146
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   147
definition Succ where "Succ Kl kl = {k . kl @ [k] \<in> Kl}"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   148
definition Shift where "Shift Kl k = {kl. k # kl \<in> Kl}"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   149
definition shift where "shift lab k = (\<lambda>kl. lab (k # kl))"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   150
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   151
lemma empty_Shift: "\<lbrakk>[] \<in> Kl; k \<in> Succ Kl []\<rbrakk> \<Longrightarrow> [] \<in> Shift Kl k"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   152
  unfolding Shift_def Succ_def by simp
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   153
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   154
lemma SuccD: "k \<in> Succ Kl kl \<Longrightarrow> kl @ [k] \<in> Kl"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   155
  unfolding Succ_def by simp
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   156
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   157
lemmas SuccE = SuccD[elim_format]
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   158
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   159
lemma SuccI: "kl @ [k] \<in> Kl \<Longrightarrow> k \<in> Succ Kl kl"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   160
  unfolding Succ_def by simp
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   161
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   162
lemma ShiftD: "kl \<in> Shift Kl k \<Longrightarrow> k # kl \<in> Kl"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   163
  unfolding Shift_def by simp
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   164
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   165
lemma Succ_Shift: "Succ (Shift Kl k) kl = Succ Kl (k # kl)"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   166
  unfolding Succ_def Shift_def by auto
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   167
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   168
lemma length_Cons: "length (x # xs) = Suc (length xs)"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   169
  by simp
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   170
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   171
lemma length_append_singleton: "length (xs @ [x]) = Suc (length xs)"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   172
  by simp
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   173
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   174
(*injection into the field of a cardinal*)
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   175
definition "toCard_pred A r f \<equiv> inj_on f A \<and> f ` A \<subseteq> Field r \<and> Card_order r"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   176
definition "toCard A r \<equiv> SOME f. toCard_pred A r f"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   177
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   178
lemma ex_toCard_pred:
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   179
  "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> \<exists> f. toCard_pred A r f"
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   180
  unfolding toCard_pred_def
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   181
  using card_of_ordLeq[of A "Field r"]
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   182
    ordLeq_ordIso_trans[OF _ card_of_unique[of "Field r" r], of "|A|"]
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   183
  by blast
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   184
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   185
lemma toCard_pred_toCard:
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   186
  "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> toCard_pred A r (toCard A r)"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   187
  unfolding toCard_def using someI_ex[OF ex_toCard_pred] .
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   188
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   189
lemma toCard_inj: "\<lbrakk>|A| \<le>o r; Card_order r; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> toCard A r x = toCard A r y \<longleftrightarrow> x = y"
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   190
  using toCard_pred_toCard unfolding inj_on_def toCard_pred_def by blast
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   191
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   192
definition "fromCard A r k \<equiv> SOME b. b \<in> A \<and> toCard A r b = k"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   193
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   194
lemma fromCard_toCard:
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   195
  "\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> fromCard A r (toCard A r b) = b"
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   196
  unfolding fromCard_def by (rule some_equality) (auto simp add: toCard_inj)
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   197
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   198
lemma Inl_Field_csum: "a \<in> Field r \<Longrightarrow> Inl a \<in> Field (r +c s)"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   199
  unfolding Field_card_of csum_def by auto
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   200
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   201
lemma Inr_Field_csum: "a \<in> Field s \<Longrightarrow> Inr a \<in> Field (r +c s)"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   202
  unfolding Field_card_of csum_def by auto
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   203
64413
blanchet
parents: 62905
diff changeset
   204
lemma rec_nat_0_imp: "f = rec_nat f1 (\<lambda>n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   205
  by auto
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   206
64413
blanchet
parents: 62905
diff changeset
   207
lemma rec_nat_Suc_imp: "f = rec_nat f1 (\<lambda>n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   208
  by auto
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   209
64413
blanchet
parents: 62905
diff changeset
   210
lemma rec_list_Nil_imp: "f = rec_list f1 (\<lambda>x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   211
  by auto
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   212
64413
blanchet
parents: 62905
diff changeset
   213
lemma rec_list_Cons_imp: "f = rec_list f1 (\<lambda>x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   214
  by auto
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   215
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   216
lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   217
  by simp
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   218
52731
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52660
diff changeset
   219
definition image2p where
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52660
diff changeset
   220
  "image2p f g R = (\<lambda>x y. \<exists>x' y'. R x' y' \<and> f x' = x \<and> g y' = y)"
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52660
diff changeset
   221
55463
942c2153b5b4 register 'Spec_Rules' for new-style (co)datatypes
blanchet
parents: 55415
diff changeset
   222
lemma image2pI: "R x y \<Longrightarrow> image2p f g R (f x) (g y)"
52731
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52660
diff changeset
   223
  unfolding image2p_def by blast
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52660
diff changeset
   224
55463
942c2153b5b4 register 'Spec_Rules' for new-style (co)datatypes
blanchet
parents: 55415
diff changeset
   225
lemma image2pE: "\<lbrakk>image2p f g R fx gy; (\<And>x y. fx = f x \<Longrightarrow> gy = g y \<Longrightarrow> R x y \<Longrightarrow> P)\<rbrakk> \<Longrightarrow> P"
52731
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52660
diff changeset
   226
  unfolding image2p_def by blast
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52660
diff changeset
   227
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55644
diff changeset
   228
lemma rel_fun_iff_geq_image2p: "rel_fun R S f g = (image2p f g R \<le> S)"
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55644
diff changeset
   229
  unfolding rel_fun_def image2p_def by auto
52731
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52660
diff changeset
   230
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55644
diff changeset
   231
lemma rel_fun_image2p: "rel_fun R (image2p f g R) f g"
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 55644
diff changeset
   232
  unfolding rel_fun_def image2p_def by auto
52731
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52660
diff changeset
   233
55022
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   234
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   235
subsection \<open>Equivalence relations, quotients, and Hilbert's choice\<close>
55022
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   236
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   237
lemma equiv_Eps_in:
64413
blanchet
parents: 62905
diff changeset
   238
"\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> Eps (\<lambda>x. x \<in> X) \<in> X"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   239
  apply (rule someI2_ex)
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   240
  using in_quotient_imp_non_empty by blast
55022
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   241
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   242
lemma equiv_Eps_preserves:
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   243
  assumes ECH: "equiv A r" and X: "X \<in> A//r"
64413
blanchet
parents: 62905
diff changeset
   244
  shows "Eps (\<lambda>x. x \<in> X) \<in> A"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   245
  apply (rule in_mono[rule_format])
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   246
   using assms apply (rule in_quotient_imp_subset)
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   247
  by (rule equiv_Eps_in) (rule assms)+
55022
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   248
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   249
lemma proj_Eps:
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   250
  assumes "equiv A r" and "X \<in> A//r"
64413
blanchet
parents: 62905
diff changeset
   251
  shows "proj r (Eps (\<lambda>x. x \<in> X)) = X"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   252
unfolding proj_def
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   253
proof auto
55022
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   254
  fix x assume x: "x \<in> X"
64413
blanchet
parents: 62905
diff changeset
   255
  thus "(Eps (\<lambda>x. x \<in> X), x) \<in> r" using assms equiv_Eps_in in_quotient_imp_in_rel by fast
55022
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   256
next
64413
blanchet
parents: 62905
diff changeset
   257
  fix x assume "(Eps (\<lambda>x. x \<in> X),x) \<in> r"
55022
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   258
  thus "x \<in> X" using in_quotient_imp_closed[OF assms equiv_Eps_in[OF assms]] by fast
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   259
qed
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   260
64413
blanchet
parents: 62905
diff changeset
   261
definition univ where "univ f X == f (Eps (\<lambda>x. x \<in> X))"
55022
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   262
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   263
lemma univ_commute:
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   264
assumes ECH: "equiv A r" and RES: "f respects r" and x: "x \<in> A"
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   265
shows "(univ f) (proj r x) = f x"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   266
proof (unfold univ_def)
55022
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   267
  have prj: "proj r x \<in> A//r" using x proj_preserves by fast
64413
blanchet
parents: 62905
diff changeset
   268
  hence "Eps (\<lambda>y. y \<in> proj r x) \<in> A" using ECH equiv_Eps_preserves by fast
blanchet
parents: 62905
diff changeset
   269
  moreover have "proj r (Eps (\<lambda>y. y \<in> proj r x)) = proj r x" using ECH prj proj_Eps by fast
blanchet
parents: 62905
diff changeset
   270
  ultimately have "(x, Eps (\<lambda>y. y \<in> proj r x)) \<in> r" using x ECH proj_iff by fast
blanchet
parents: 62905
diff changeset
   271
  thus "f (Eps (\<lambda>y. y \<in> proj r x)) = f x" using RES unfolding congruent_def by fastforce
55022
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   272
qed
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   273
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   274
lemma univ_preserves:
57991
f50b3726266f don't note low-level (co)datatype theorems, unless 'bnf_note_all' is set
blanchet
parents: 57896
diff changeset
   275
  assumes ECH: "equiv A r" and RES: "f respects r" and PRES: "\<forall>x \<in> A. f x \<in> B"
57896
2d037f8dc4d5 tuned whitespace
blanchet
parents: 57698
diff changeset
   276
  shows "\<forall>X \<in> A//r. univ f X \<in> B"
55022
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   277
proof
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   278
  fix X assume "X \<in> A//r"
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   279
  then obtain x where x: "x \<in> A" and X: "X = proj r x" using ECH proj_image[of r A] by blast
57991
f50b3726266f don't note low-level (co)datatype theorems, unless 'bnf_note_all' is set
blanchet
parents: 57896
diff changeset
   280
  hence "univ f X = f x" using ECH RES univ_commute by fastforce
55022
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   281
  thus "univ f X \<in> B" using x PRES by simp
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   282
qed
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   283
69605
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 67613
diff changeset
   284
ML_file \<open>Tools/BNF/bnf_gfp_util.ML\<close>
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 67613
diff changeset
   285
ML_file \<open>Tools/BNF/bnf_gfp_tactics.ML\<close>
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 67613
diff changeset
   286
ML_file \<open>Tools/BNF/bnf_gfp.ML\<close>
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 67613
diff changeset
   287
ML_file \<open>Tools/BNF/bnf_gfp_rec_sugar_tactics.ML\<close>
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 67613
diff changeset
   288
ML_file \<open>Tools/BNF/bnf_gfp_rec_sugar.ML\<close>
49309
f20b24214ac2 split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents: 49308
diff changeset
   289
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   290
end