src/HOL/BNF_GFP.thy
author blanchet
Wed, 12 Feb 2014 08:35:57 +0100
changeset 55414 eab03e9cee8a
parent 55413 a8e96847523c
child 55415 05f5fdb8d093
permissions -rw-r--r--
renamed '{prod,sum,bool,unit}_case' to 'case_...'
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
55059
ef2e0fb783c6 tuned comments
blanchet
parents: 55058
diff changeset
     1
(*  Title:      HOL/BNF_GFP.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
ef2e0fb783c6 tuned comments
blanchet
parents: 55058
diff changeset
     5
    Copyright   2012, 2013
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     6
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
     7
Greatest fixed point operation on bounded natural functors.
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
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    10
header {* Greatest Fixed Point Operation on Bounded Natural Functors *}
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 BNF_GFP
55079
ec08a67e993b removed dependency of BNF package on Nitpick
blanchet
parents: 55062
diff changeset
    13
imports BNF_FP_Base List_Prefix String
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
    14
keywords
53310
8af01463b2d3 moved keywords down the hierarchy
blanchet
parents: 53105
diff changeset
    15
  "codatatype" :: thy_decl and
53822
6304b12c7627 add "primcorec" command (cf. ae7f50e70c09)
panny
parents: 53753
diff changeset
    16
  "primcorecursive" :: thy_goal and
6304b12c7627 add "primcorec" command (cf. ae7f50e70c09)
panny
parents: 53753
diff changeset
    17
  "primcorec" :: thy_decl
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
55024
05cc0dbf3a50 hide short const name
blanchet
parents: 55022
diff changeset
    20
setup {*
05cc0dbf3a50 hide short const name
blanchet
parents: 55022
diff changeset
    21
Sign.const_alias @{binding proj} @{const_name Equiv_Relations.proj}
05cc0dbf3a50 hide short const name
blanchet
parents: 55022
diff changeset
    22
*}
05cc0dbf3a50 hide short const name
blanchet
parents: 55022
diff changeset
    23
54485
b61b8c9e4cf7 killed more needless theorems
blanchet
parents: 54484
diff changeset
    24
lemma not_TrueE: "\<not> True \<Longrightarrow> P"
b61b8c9e4cf7 killed more needless theorems
blanchet
parents: 54484
diff changeset
    25
by (erule notE, rule TrueI)
b61b8c9e4cf7 killed more needless theorems
blanchet
parents: 54484
diff changeset
    26
b61b8c9e4cf7 killed more needless theorems
blanchet
parents: 54484
diff changeset
    27
lemma neq_eq_eq_contradict: "\<lbrakk>t \<noteq> u; s = t; s = u\<rbrakk> \<Longrightarrow> P"
b61b8c9e4cf7 killed more needless theorems
blanchet
parents: 54484
diff changeset
    28
by fast
b61b8c9e4cf7 killed more needless theorems
blanchet
parents: 54484
diff changeset
    29
55414
eab03e9cee8a renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents: 55413
diff changeset
    30
lemma case_sum_expand_Inr: "f o Inl = g \<Longrightarrow> f x = case_sum g (f o Inr) x"
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    31
by (auto split: sum.splits)
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    32
55414
eab03e9cee8a renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents: 55413
diff changeset
    33
lemma case_sum_expand_Inr': "f o Inl = g \<Longrightarrow> h = f o Inr \<longleftrightarrow> case_sum g h = f"
54488
b60f1fab408c more tuning for speed
blanchet
parents: 54485
diff changeset
    34
apply rule
b60f1fab408c more tuning for speed
blanchet
parents: 54485
diff changeset
    35
 apply (rule ext, force split: sum.split)
55414
eab03e9cee8a renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents: 55413
diff changeset
    36
by (rule ext, metis case_sum_o_inj(2))
51739
3514b90d0a8b (co)rec is (just as the (un)fold) the unique morphism;
traytel
parents: 51447
diff changeset
    37
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    38
lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A"
54488
b60f1fab408c more tuning for speed
blanchet
parents: 54485
diff changeset
    39
by fast
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    40
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    41
lemma equiv_proj:
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    42
  assumes e: "equiv A R" and "z \<in> R"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    43
  shows "(proj R o fst) z = (proj R o snd) z"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    44
proof -
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    45
  from assms(2) have z: "(fst z, snd z) \<in> R" by auto
53695
a66d211ab34e tuned proofs
traytel
parents: 53469
diff changeset
    46
  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
    47
    unfolding equiv_def sym_def trans_def by blast+
a66d211ab34e tuned proofs
traytel
parents: 53469
diff changeset
    48
  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
    49
qed
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    50
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    51
(* Operators: *)
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    52
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
    53
51447
a19e973fa2cf eliminate duplicated constant (diag vs. Id_on)
traytel
parents: 51446
diff changeset
    54
lemma Id_onD: "(a, b) \<in> Id_on A \<Longrightarrow> a = b"
a19e973fa2cf eliminate duplicated constant (diag vs. Id_on)
traytel
parents: 51446
diff changeset
    55
unfolding Id_on_def by simp
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    56
51447
a19e973fa2cf eliminate duplicated constant (diag vs. Id_on)
traytel
parents: 51446
diff changeset
    57
lemma Id_onD': "x \<in> Id_on A \<Longrightarrow> fst x = snd x"
a19e973fa2cf eliminate duplicated constant (diag vs. Id_on)
traytel
parents: 51446
diff changeset
    58
unfolding Id_on_def by auto
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    59
51447
a19e973fa2cf eliminate duplicated constant (diag vs. Id_on)
traytel
parents: 51446
diff changeset
    60
lemma Id_on_fst: "x \<in> Id_on A \<Longrightarrow> fst x \<in> A"
a19e973fa2cf eliminate duplicated constant (diag vs. Id_on)
traytel
parents: 51446
diff changeset
    61
unfolding Id_on_def by auto
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    62
51447
a19e973fa2cf eliminate duplicated constant (diag vs. Id_on)
traytel
parents: 51446
diff changeset
    63
lemma Id_on_UNIV: "Id_on UNIV = Id"
a19e973fa2cf eliminate duplicated constant (diag vs. Id_on)
traytel
parents: 51446
diff changeset
    64
unfolding Id_on_def by auto
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    65
51447
a19e973fa2cf eliminate duplicated constant (diag vs. Id_on)
traytel
parents: 51446
diff changeset
    66
lemma Id_on_Comp: "Id_on A = Id_on A O Id_on A"
a19e973fa2cf eliminate duplicated constant (diag vs. Id_on)
traytel
parents: 51446
diff changeset
    67
unfolding Id_on_def by auto
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    68
51447
a19e973fa2cf eliminate duplicated constant (diag vs. Id_on)
traytel
parents: 51446
diff changeset
    69
lemma Id_on_Gr: "Id_on A = Gr A id"
a19e973fa2cf eliminate duplicated constant (diag vs. Id_on)
traytel
parents: 51446
diff changeset
    70
unfolding Id_on_def Gr_def by auto
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    71
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    72
lemma image2_eqI: "\<lbrakk>b = f x; c = g x; x \<in> A\<rbrakk> \<Longrightarrow> (b, c) \<in> image2 A f g"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    73
unfolding image2_def by auto
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    74
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    75
lemma IdD: "(a, b) \<in> Id \<Longrightarrow> a = b"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    76
by auto
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    77
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    78
lemma image2_Gr: "image2 A f g = (Gr A f)^-1 O (Gr A g)"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    79
unfolding image2_def Gr_def by auto
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    80
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    81
lemma GrD1: "(x, fx) \<in> Gr A f \<Longrightarrow> x \<in> A"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    82
unfolding Gr_def by simp
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    83
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    84
lemma GrD2: "(x, fx) \<in> Gr A f \<Longrightarrow> f x = fx"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    85
unfolding Gr_def by simp
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    86
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    87
lemma Gr_incl: "Gr A f \<subseteq> A <*> B \<longleftrightarrow> f ` A \<subseteq> B"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    88
unfolding Gr_def by auto
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
    89
54485
b61b8c9e4cf7 killed more needless theorems
blanchet
parents: 54484
diff changeset
    90
lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
b61b8c9e4cf7 killed more needless theorems
blanchet
parents: 54484
diff changeset
    91
by blast
b61b8c9e4cf7 killed more needless theorems
blanchet
parents: 54484
diff changeset
    92
b61b8c9e4cf7 killed more needless theorems
blanchet
parents: 54484
diff changeset
    93
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})"
b61b8c9e4cf7 killed more needless theorems
blanchet
parents: 54484
diff changeset
    94
by blast
b61b8c9e4cf7 killed more needless theorems
blanchet
parents: 54484
diff changeset
    95
51893
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
    96
lemma in_rel_Collect_split_eq: "in_rel (Collect (split X)) = X"
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
    97
unfolding fun_eq_iff by auto
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
    98
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
    99
lemma Collect_split_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (split (in_rel Y))"
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
   100
by auto
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
   101
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
   102
lemma Collect_split_in_rel_leE: "X \<subseteq> Collect (split (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
   103
by force
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
   104
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
   105
lemma Collect_split_in_relI: "x \<in> X \<Longrightarrow> x \<in> Collect (split (in_rel X))"
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
   106
by auto
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
   107
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
   108
lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)"
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
   109
unfolding fun_eq_iff by auto
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
   110
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
   111
lemma relcompp_in_rel: "in_rel R OO in_rel S = in_rel (R O S)"
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
   112
unfolding fun_eq_iff by auto
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
   113
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
   114
lemma in_rel_Gr: "in_rel (Gr A f) = Grp A f"
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
   115
unfolding Gr_def Grp_def fun_eq_iff by auto
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
   116
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
   117
lemma in_rel_Id_on_UNIV: "in_rel (Id_on UNIV) = op ="
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
   118
unfolding fun_eq_iff by auto
596baae88a88 got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents: 51850
diff changeset
   119
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   120
definition relImage where
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   121
"relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   122
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   123
definition relInvImage where
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   124
"relInvImage A R f \<equiv> {(a1, a2) | a1 a2. a1 \<in> A \<and> a2 \<in> A \<and> (f a1, f a2) \<in> R}"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   125
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   126
lemma relImage_Gr:
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   127
"\<lbrakk>R \<subseteq> A \<times> A\<rbrakk> \<Longrightarrow> relImage R f = (Gr A f)^-1 O R O Gr A f"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   128
unfolding relImage_def Gr_def relcomp_def by auto
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   129
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   130
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"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   131
unfolding Gr_def relcomp_def image_def relInvImage_def by auto
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   132
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   133
lemma relImage_mono:
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   134
"R1 \<subseteq> R2 \<Longrightarrow> relImage R1 f \<subseteq> relImage R2 f"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   135
unfolding relImage_def by auto
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   136
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   137
lemma relInvImage_mono:
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   138
"R1 \<subseteq> R2 \<Longrightarrow> relInvImage A R1 f \<subseteq> relInvImage A R2 f"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   139
unfolding relInvImage_def by auto
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   140
51447
a19e973fa2cf eliminate duplicated constant (diag vs. Id_on)
traytel
parents: 51446
diff changeset
   141
lemma relInvImage_Id_on:
a19e973fa2cf eliminate duplicated constant (diag vs. Id_on)
traytel
parents: 51446
diff changeset
   142
"(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (Id_on B) f \<subseteq> Id"
a19e973fa2cf eliminate duplicated constant (diag vs. Id_on)
traytel
parents: 51446
diff changeset
   143
unfolding relInvImage_def Id_on_def by auto
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   144
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   145
lemma relInvImage_UNIV_relImage:
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   146
"R \<subseteq> relInvImage UNIV (relImage R f) f"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   147
unfolding relInvImage_def relImage_def by auto
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   148
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   149
lemma relImage_proj:
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   150
assumes "equiv A R"
51447
a19e973fa2cf eliminate duplicated constant (diag vs. Id_on)
traytel
parents: 51446
diff changeset
   151
shows "relImage R (proj R) \<subseteq> Id_on (A//R)"
a19e973fa2cf eliminate duplicated constant (diag vs. Id_on)
traytel
parents: 51446
diff changeset
   152
unfolding relImage_def Id_on_def
a19e973fa2cf eliminate duplicated constant (diag vs. Id_on)
traytel
parents: 51446
diff changeset
   153
using proj_iff[OF assms] equiv_class_eq_iff[OF assms]
a19e973fa2cf eliminate duplicated constant (diag vs. Id_on)
traytel
parents: 51446
diff changeset
   154
by (auto simp: proj_preserves)
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   155
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   156
lemma relImage_relInvImage:
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   157
assumes "R \<subseteq> f ` A <*> f ` A"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   158
shows "relImage (relInvImage A R f) f = R"
54488
b60f1fab408c more tuning for speed
blanchet
parents: 54485
diff changeset
   159
using assms unfolding relImage_def relInvImage_def by fast
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   160
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   161
lemma subst_Pair: "P x y \<Longrightarrow> a = (x, y) \<Longrightarrow> P (fst a) (snd a)"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   162
by simp
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   163
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   164
lemma fst_diag_id: "(fst \<circ> (%x. (x, x))) z = id z"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   165
by simp
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   166
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   167
lemma snd_diag_id: "(snd \<circ> (%x. (x, x))) z = id z"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   168
by simp
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   169
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   170
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"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   171
unfolding convol_def by auto
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   172
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   173
(*Extended Sublist*)
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   174
54581
1502a1f707d9 eliminated dependence of Cardinals_FP on Set_Intervals, more precise imports
traytel
parents: 54538
diff changeset
   175
definition clists where "clists r = |lists (Field r)|"
1502a1f707d9 eliminated dependence of Cardinals_FP on Set_Intervals, more precise imports
traytel
parents: 54538
diff changeset
   176
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   177
definition prefCl where
50058
bb1fadeba35e import Sublist rather than PrefixOrder to avoid unnecessary class instantiation
traytel
parents: 49635
diff changeset
   178
  "prefCl Kl = (\<forall> kl1 kl2. prefixeq kl1 kl2 \<and> kl2 \<in> Kl \<longrightarrow> kl1 \<in> Kl)"
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   179
definition PrefCl where
50058
bb1fadeba35e import Sublist rather than PrefixOrder to avoid unnecessary class instantiation
traytel
parents: 49635
diff changeset
   180
  "PrefCl A n = (\<forall>kl kl'. kl \<in> A n \<and> prefixeq kl' kl \<longrightarrow> (\<exists>m\<le>n. kl' \<in> A m))"
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   181
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   182
lemma prefCl_UN:
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   183
  "\<lbrakk>\<And>n. PrefCl A n\<rbrakk> \<Longrightarrow> prefCl (\<Union>n. A n)"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   184
unfolding prefCl_def PrefCl_def by fastforce
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   185
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   186
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
   187
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
   188
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
   189
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   190
lemma empty_Shift: "\<lbrakk>[] \<in> Kl; k \<in> Succ Kl []\<rbrakk> \<Longrightarrow> [] \<in> Shift Kl k"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   191
unfolding Shift_def Succ_def by simp
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   192
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   193
lemma Shift_clists: "Kl \<subseteq> Field (clists r) \<Longrightarrow> Shift Kl k \<subseteq> Field (clists r)"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   194
unfolding Shift_def clists_def Field_card_of by auto
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   195
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   196
lemma Shift_prefCl: "prefCl Kl \<Longrightarrow> prefCl (Shift Kl k)"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   197
unfolding prefCl_def Shift_def
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   198
proof safe
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   199
  fix kl1 kl2
50058
bb1fadeba35e import Sublist rather than PrefixOrder to avoid unnecessary class instantiation
traytel
parents: 49635
diff changeset
   200
  assume "\<forall>kl1 kl2. prefixeq kl1 kl2 \<and> kl2 \<in> Kl \<longrightarrow> kl1 \<in> Kl"
bb1fadeba35e import Sublist rather than PrefixOrder to avoid unnecessary class instantiation
traytel
parents: 49635
diff changeset
   201
    "prefixeq kl1 kl2" "k # kl2 \<in> Kl"
bb1fadeba35e import Sublist rather than PrefixOrder to avoid unnecessary class instantiation
traytel
parents: 49635
diff changeset
   202
  thus "k # kl1 \<in> Kl" using Cons_prefixeq_Cons[of k kl1 k kl2] by blast
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   203
qed
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   204
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   205
lemma not_in_Shift: "kl \<notin> Shift Kl x \<Longrightarrow> x # kl \<notin> Kl"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   206
unfolding Shift_def by simp
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   207
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   208
lemma SuccD: "k \<in> Succ Kl kl \<Longrightarrow> kl @ [k] \<in> Kl"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   209
unfolding Succ_def by simp
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   210
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   211
lemmas SuccE = SuccD[elim_format]
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   212
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   213
lemma SuccI: "kl @ [k] \<in> Kl \<Longrightarrow> k \<in> Succ Kl kl"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   214
unfolding Succ_def by simp
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 ShiftD: "kl \<in> Shift Kl k \<Longrightarrow> k # kl \<in> Kl"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   217
unfolding Shift_def by simp
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   218
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   219
lemma Succ_Shift: "Succ (Shift Kl k) kl = Succ Kl (k # kl)"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   220
unfolding Succ_def Shift_def by auto
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   221
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   222
lemma Nil_clists: "{[]} \<subseteq> Field (clists r)"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   223
unfolding clists_def Field_card_of by auto
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   224
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   225
lemma Cons_clists:
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   226
  "\<lbrakk>x \<in> Field r; xs \<in> Field (clists r)\<rbrakk> \<Longrightarrow> x # xs \<in> Field (clists r)"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   227
unfolding clists_def Field_card_of by auto
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   228
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   229
lemma length_Cons: "length (x # xs) = Suc (length xs)"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   230
by simp
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   231
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   232
lemma length_append_singleton: "length (xs @ [x]) = Suc (length xs)"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   233
by simp
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   234
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   235
(*injection into the field of a cardinal*)
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   236
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
   237
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
   238
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   239
lemma ex_toCard_pred:
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   240
"\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> \<exists> f. toCard_pred A r f"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   241
unfolding toCard_pred_def
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   242
using card_of_ordLeq[of A "Field r"]
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   243
      ordLeq_ordIso_trans[OF _ card_of_unique[of "Field r" r], of "|A|"]
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   244
by blast
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   245
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   246
lemma toCard_pred_toCard:
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   247
  "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> toCard_pred A r (toCard A r)"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   248
unfolding toCard_def using someI_ex[OF ex_toCard_pred] .
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   249
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   250
lemma toCard_inj: "\<lbrakk>|A| \<le>o r; Card_order r; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow>
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   251
  toCard A r x = toCard A r y \<longleftrightarrow> x = y"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   252
using toCard_pred_toCard unfolding inj_on_def toCard_pred_def by blast
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   253
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   254
lemma toCard: "\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> toCard A r b \<in> Field r"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   255
using toCard_pred_toCard unfolding toCard_pred_def by blast
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   256
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   257
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
   258
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   259
lemma fromCard_toCard:
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   260
"\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> fromCard A r (toCard A r b) = b"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   261
unfolding fromCard_def by (rule some_equality) (auto simp add: toCard_inj)
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   262
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   263
lemma Inl_Field_csum: "a \<in> Field r \<Longrightarrow> Inl a \<in> Field (r +c s)"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   264
unfolding Field_card_of csum_def by auto
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   265
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   266
lemma Inr_Field_csum: "a \<in> Field s \<Longrightarrow> Inr a \<in> Field (r +c s)"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   267
unfolding Field_card_of csum_def by auto
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   268
55062
6d3fad6f01c9 made BNF compile after move to HOL
blanchet
parents: 55059
diff changeset
   269
lemma nat_rec_0_imp: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   270
by auto
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   271
55062
6d3fad6f01c9 made BNF compile after move to HOL
blanchet
parents: 55059
diff changeset
   272
lemma nat_rec_Suc_imp: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   273
by auto
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   274
55413
a8e96847523c adapted theories to '{case,rec}_{list,option}' names
blanchet
parents: 55079
diff changeset
   275
lemma rec_list_Nil_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   276
by auto
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   277
55413
a8e96847523c adapted theories to '{case,rec}_{list,option}' names
blanchet
parents: 55079
diff changeset
   278
lemma rec_list_Cons_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)"
49312
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   279
by auto
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   280
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   281
lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   282
by simp
c874ff5658dc moved theorems closer to where they are used
blanchet
parents: 49309
diff changeset
   283
51925
e3b7917186f1 relator coinduction for codatatypes
traytel
parents: 51909
diff changeset
   284
lemma Collect_splitD: "x \<in> Collect (split A) \<Longrightarrow> A (fst x) (snd x)"
e3b7917186f1 relator coinduction for codatatypes
traytel
parents: 51909
diff changeset
   285
by auto
e3b7917186f1 relator coinduction for codatatypes
traytel
parents: 51909
diff changeset
   286
52731
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52660
diff changeset
   287
definition image2p where
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52660
diff changeset
   288
  "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
   289
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52660
diff changeset
   290
lemma image2pI: "R x y \<Longrightarrow> (image2p f g R) (f x) (g y)"
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52660
diff changeset
   291
  unfolding image2p_def by blast
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52660
diff changeset
   292
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52660
diff changeset
   293
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"
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52660
diff changeset
   294
  unfolding image2p_def by blast
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52660
diff changeset
   295
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52660
diff changeset
   296
lemma fun_rel_iff_geq_image2p: "(fun_rel R S) f g = (image2p f g R \<le> S)"
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52660
diff changeset
   297
  unfolding fun_rel_def image2p_def by auto
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52660
diff changeset
   298
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52660
diff changeset
   299
lemma fun_rel_image2p: "(fun_rel R (image2p f g R)) f g"
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52660
diff changeset
   300
  unfolding fun_rel_def image2p_def by auto
dacd47a0633f transfer rule for {c,d}tor_{,un}fold
traytel
parents: 52660
diff changeset
   301
55022
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   302
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   303
subsection {* Equivalence relations, quotients, and Hilbert's choice *}
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   304
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   305
lemma equiv_Eps_in:
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   306
"\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> Eps (%x. x \<in> X) \<in> X"
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   307
apply (rule someI2_ex)
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   308
using in_quotient_imp_non_empty by blast
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   309
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   310
lemma equiv_Eps_preserves:
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   311
assumes ECH: "equiv A r" and X: "X \<in> A//r"
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   312
shows "Eps (%x. x \<in> X) \<in> A"
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   313
apply (rule in_mono[rule_format])
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   314
 using assms apply (rule in_quotient_imp_subset)
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   315
by (rule equiv_Eps_in) (rule assms)+
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   316
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   317
lemma proj_Eps:
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   318
assumes "equiv A r" and "X \<in> A//r"
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   319
shows "proj r (Eps (%x. x \<in> X)) = X"
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   320
unfolding proj_def proof auto
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   321
  fix x assume x: "x \<in> X"
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   322
  thus "(Eps (%x. x \<in> X), x) \<in> r" using assms equiv_Eps_in in_quotient_imp_in_rel by fast
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   323
next
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   324
  fix x assume "(Eps (%x. x \<in> X),x) \<in> r"
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   325
  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
   326
qed
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   327
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   328
definition univ where "univ f X == f (Eps (%x. x \<in> X))"
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   329
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   330
lemma univ_commute:
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   331
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
   332
shows "(univ f) (proj r x) = f x"
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   333
unfolding univ_def proof -
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   334
  have prj: "proj r x \<in> A//r" using x proj_preserves by fast
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   335
  hence "Eps (%y. y \<in> proj r x) \<in> A" using ECH equiv_Eps_preserves by fast
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   336
  moreover have "proj r (Eps (%y. y \<in> proj r x)) = proj r x" using ECH prj proj_Eps by fast
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   337
  ultimately have "(x, Eps (%y. y \<in> proj r x)) \<in> r" using x ECH proj_iff by fast
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   338
  thus "f (Eps (%y. y \<in> proj r x)) = f x" using RES unfolding congruent_def by fastforce
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   339
qed
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   340
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   341
lemma univ_preserves:
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   342
assumes ECH: "equiv A r" and RES: "f respects r" and
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   343
        PRES: "\<forall> x \<in> A. f x \<in> B"
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   344
shows "\<forall> X \<in> A//r. univ f X \<in> B"
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   345
proof
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   346
  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
   347
  then obtain x where x: "x \<in> A" and X: "X = proj r x" using ECH proj_image[of r A] by blast
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   348
  hence "univ f X = f x" using assms univ_commute by fastforce
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   349
  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
   350
qed
eeba3ba73486 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
blanchet
parents: 54841
diff changeset
   351
55062
6d3fad6f01c9 made BNF compile after move to HOL
blanchet
parents: 55059
diff changeset
   352
ML_file "Tools/BNF/bnf_gfp_rec_sugar_tactics.ML"
6d3fad6f01c9 made BNF compile after move to HOL
blanchet
parents: 55059
diff changeset
   353
ML_file "Tools/BNF/bnf_gfp_rec_sugar.ML"
6d3fad6f01c9 made BNF compile after move to HOL
blanchet
parents: 55059
diff changeset
   354
ML_file "Tools/BNF/bnf_gfp_util.ML"
6d3fad6f01c9 made BNF compile after move to HOL
blanchet
parents: 55059
diff changeset
   355
ML_file "Tools/BNF/bnf_gfp_tactics.ML"
6d3fad6f01c9 made BNF compile after move to HOL
blanchet
parents: 55059
diff changeset
   356
ML_file "Tools/BNF/bnf_gfp.ML"
49309
f20b24214ac2 split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents: 49308
diff changeset
   357
48975
7f79f94a432c added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff changeset
   358
end