src/HOL/Library/Old_Datatype.thy
author wenzelm
Tue May 15 13:57:39 2018 +0200 (16 months ago)
changeset 68189 6163c90694ef
parent 67613 ce654b0e6d69
child 69605 a96320074298
permissions -rw-r--r--
tuned headers;
blanchet@58372
     1
(*  Title:      HOL/Library/Old_Datatype.thy
wenzelm@20819
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@11954
     3
    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
berghofe@5181
     4
*)
berghofe@5181
     5
wenzelm@60500
     6
section \<open>Old Datatype package: constructing datatypes from Cartesian Products and Disjoint Sums\<close>
wenzelm@11954
     7
blanchet@58112
     8
theory Old_Datatype
wenzelm@65513
     9
imports Main
nipkow@15131
    10
begin
wenzelm@11954
    11
blanchet@58377
    12
wenzelm@60500
    13
subsection \<open>The datatype universe\<close>
haftmann@33959
    14
wenzelm@67091
    15
definition "Node = {p. \<exists>f x k. p = (f :: nat => 'b + nat, x ::'a + nat) \<and> f k = Inr 0}"
wenzelm@45694
    16
wenzelm@49834
    17
typedef ('a, 'b) node = "Node :: ((nat => 'b + nat) * ('a + nat)) set"
wenzelm@45694
    18
  morphisms Rep_Node Abs_Node
wenzelm@45694
    19
  unfolding Node_def by auto
wenzelm@20819
    20
wenzelm@61585
    21
text\<open>Datatypes will be represented by sets of type \<open>node\<close>\<close>
wenzelm@20819
    22
bulwahn@42163
    23
type_synonym 'a item        = "('a, unit) node set"
bulwahn@42163
    24
type_synonym ('a, 'b) dtree = "('a, 'b) node set"
wenzelm@20819
    25
wenzelm@62145
    26
definition Push :: "[('b + nat), nat => ('b + nat)] => (nat => ('b + nat))"
wenzelm@62145
    27
  (*crude "lists" of nats -- needed for the constructions*)
wenzelm@62145
    28
  where "Push == (%b h. case_nat b h)"
wenzelm@20819
    29
wenzelm@62145
    30
definition Push_Node :: "[('b + nat), ('a, 'b) node] => ('a, 'b) node"
wenzelm@62145
    31
  where "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
wenzelm@20819
    32
wenzelm@20819
    33
wenzelm@62145
    34
(** operations on S-expressions -- sets of nodes **)
wenzelm@20819
    35
wenzelm@62145
    36
(*S-expression constructors*)
wenzelm@62145
    37
definition Atom :: "('a + nat) => ('a, 'b) dtree"
wenzelm@62145
    38
  where "Atom == (%x. {Abs_Node((%k. Inr 0, x))})"
wenzelm@62145
    39
definition Scons :: "[('a, 'b) dtree, ('a, 'b) dtree] => ('a, 'b) dtree"
wenzelm@62145
    40
  where "Scons M N == (Push_Node (Inr 1) ` M) Un (Push_Node (Inr (Suc 1)) ` N)"
wenzelm@20819
    41
wenzelm@62145
    42
(*Leaf nodes, with arbitrary or nat labels*)
wenzelm@62145
    43
definition Leaf :: "'a => ('a, 'b) dtree"
wenzelm@67091
    44
  where "Leaf == Atom \<circ> Inl"
wenzelm@62145
    45
definition Numb :: "nat => ('a, 'b) dtree"
wenzelm@67091
    46
  where "Numb == Atom \<circ> Inr"
wenzelm@20819
    47
wenzelm@62145
    48
(*Injections of the "disjoint sum"*)
wenzelm@62145
    49
definition In0 :: "('a, 'b) dtree => ('a, 'b) dtree"
wenzelm@62145
    50
  where "In0(M) == Scons (Numb 0) M"
wenzelm@62145
    51
definition In1 :: "('a, 'b) dtree => ('a, 'b) dtree"
wenzelm@62145
    52
  where "In1(M) == Scons (Numb 1) M"
wenzelm@20819
    53
wenzelm@62145
    54
(*Function spaces*)
wenzelm@62145
    55
definition Lim :: "('b => ('a, 'b) dtree) => ('a, 'b) dtree"
wenzelm@67091
    56
  where "Lim f == \<Union>{z. \<exists>x. z = Push_Node (Inl x) ` (f x)}"
wenzelm@20819
    57
wenzelm@62145
    58
(*the set of nodes with depth less than k*)
wenzelm@62145
    59
definition ndepth :: "('a, 'b) node => nat"
wenzelm@62145
    60
  where "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)"
wenzelm@62145
    61
definition ntrunc :: "[nat, ('a, 'b) dtree] => ('a, 'b) dtree"
wenzelm@67613
    62
  where "ntrunc k N == {n. n\<in>N \<and> ndepth(n)<k}"
wenzelm@20819
    63
wenzelm@62145
    64
(*products and sums for the "universe"*)
wenzelm@62145
    65
definition uprod :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set"
wenzelm@62145
    66
  where "uprod A B == UN x:A. UN y:B. { Scons x y }"
wenzelm@62145
    67
definition usum :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set"
wenzelm@62145
    68
  where "usum A B == In0`A Un In1`B"
wenzelm@20819
    69
wenzelm@62145
    70
(*the corresponding eliminators*)
wenzelm@62145
    71
definition Split :: "[[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c"
wenzelm@67091
    72
  where "Split c M == THE u. \<exists>x y. M = Scons x y \<and> u = c x y"
wenzelm@20819
    73
wenzelm@62145
    74
definition Case :: "[[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c"
wenzelm@67091
    75
  where "Case c d M == THE u. (\<exists>x . M = In0(x) \<and> u = c(x)) \<or> (\<exists>y . M = In1(y) \<and> u = d(y))"
wenzelm@20819
    76
wenzelm@20819
    77
wenzelm@62145
    78
(** equality for the "universe" **)
wenzelm@20819
    79
wenzelm@62145
    80
definition dprod :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
wenzelm@62145
    81
      => (('a, 'b) dtree * ('a, 'b) dtree)set"
wenzelm@62145
    82
  where "dprod r s == UN (x,x'):r. UN (y,y'):s. {(Scons x y, Scons x' y')}"
wenzelm@20819
    83
wenzelm@62145
    84
definition dsum :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set]
wenzelm@62145
    85
      => (('a, 'b) dtree * ('a, 'b) dtree)set"
wenzelm@62145
    86
  where "dsum r s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un (UN (y,y'):s. {(In1(y),In1(y'))})"
wenzelm@20819
    87
wenzelm@20819
    88
wenzelm@20819
    89
lemma apfst_convE: 
wenzelm@20819
    90
    "[| q = apfst f p;  !!x y. [| p = (x,y);  q = (f(x),y) |] ==> R  
wenzelm@20819
    91
     |] ==> R"
wenzelm@20819
    92
by (force simp add: apfst_def)
wenzelm@20819
    93
wenzelm@20819
    94
(** Push -- an injection, analogous to Cons on lists **)
wenzelm@20819
    95
wenzelm@20819
    96
lemma Push_inject1: "Push i f = Push j g  ==> i=j"
nipkow@39302
    97
apply (simp add: Push_def fun_eq_iff) 
wenzelm@20819
    98
apply (drule_tac x=0 in spec, simp) 
wenzelm@20819
    99
done
wenzelm@20819
   100
wenzelm@20819
   101
lemma Push_inject2: "Push i f = Push j g  ==> f=g"
nipkow@39302
   102
apply (auto simp add: Push_def fun_eq_iff) 
wenzelm@20819
   103
apply (drule_tac x="Suc x" in spec, simp) 
wenzelm@20819
   104
done
wenzelm@20819
   105
wenzelm@20819
   106
lemma Push_inject:
wenzelm@20819
   107
    "[| Push i f =Push j g;  [| i=j;  f=g |] ==> P |] ==> P"
wenzelm@20819
   108
by (blast dest: Push_inject1 Push_inject2) 
wenzelm@20819
   109
wenzelm@20819
   110
lemma Push_neq_K0: "Push (Inr (Suc k)) f = (%z. Inr 0) ==> P"
nipkow@39302
   111
by (auto simp add: Push_def fun_eq_iff split: nat.split_asm)
wenzelm@20819
   112
wenzelm@45607
   113
lemmas Abs_Node_inj = Abs_Node_inject [THEN [2] rev_iffD1]
wenzelm@20819
   114
wenzelm@20819
   115
wenzelm@20819
   116
(*** Introduction rules for Node ***)
wenzelm@20819
   117
wenzelm@67613
   118
lemma Node_K0_I: "(\<lambda>k. Inr 0, a) \<in> Node"
wenzelm@20819
   119
by (simp add: Node_def)
wenzelm@20819
   120
wenzelm@67613
   121
lemma Node_Push_I: "p \<in> Node \<Longrightarrow> apfst (Push i) p \<in> Node"
wenzelm@20819
   122
apply (simp add: Node_def Push_def) 
blanchet@55642
   123
apply (fast intro!: apfst_conv nat.case(2)[THEN trans])
wenzelm@20819
   124
done
wenzelm@20819
   125
wenzelm@20819
   126
wenzelm@60500
   127
subsection\<open>Freeness: Distinctness of Constructors\<close>
wenzelm@20819
   128
wenzelm@20819
   129
(** Scons vs Atom **)
wenzelm@20819
   130
wenzelm@20819
   131
lemma Scons_not_Atom [iff]: "Scons M N \<noteq> Atom(a)"
huffman@35216
   132
unfolding Atom_def Scons_def Push_Node_def One_nat_def
huffman@35216
   133
by (blast intro: Node_K0_I Rep_Node [THEN Node_Push_I] 
wenzelm@20819
   134
         dest!: Abs_Node_inj 
wenzelm@20819
   135
         elim!: apfst_convE sym [THEN Push_neq_K0])  
wenzelm@20819
   136
wenzelm@45607
   137
lemmas Atom_not_Scons [iff] = Scons_not_Atom [THEN not_sym]
haftmann@21407
   138
wenzelm@20819
   139
wenzelm@20819
   140
(*** Injectiveness ***)
wenzelm@20819
   141
wenzelm@20819
   142
(** Atomic nodes **)
wenzelm@20819
   143
wenzelm@20819
   144
lemma inj_Atom: "inj(Atom)"
wenzelm@20819
   145
apply (simp add: Atom_def)
wenzelm@20819
   146
apply (blast intro!: inj_onI Node_K0_I dest!: Abs_Node_inj)
wenzelm@20819
   147
done
wenzelm@45607
   148
lemmas Atom_inject = inj_Atom [THEN injD]
wenzelm@20819
   149
wenzelm@20819
   150
lemma Atom_Atom_eq [iff]: "(Atom(a)=Atom(b)) = (a=b)"
wenzelm@20819
   151
by (blast dest!: Atom_inject)
wenzelm@20819
   152
wenzelm@20819
   153
lemma inj_Leaf: "inj(Leaf)"
wenzelm@20819
   154
apply (simp add: Leaf_def o_def)
wenzelm@20819
   155
apply (rule inj_onI)
wenzelm@20819
   156
apply (erule Atom_inject [THEN Inl_inject])
wenzelm@20819
   157
done
wenzelm@20819
   158
wenzelm@45607
   159
lemmas Leaf_inject [dest!] = inj_Leaf [THEN injD]
wenzelm@20819
   160
wenzelm@20819
   161
lemma inj_Numb: "inj(Numb)"
wenzelm@20819
   162
apply (simp add: Numb_def o_def)
wenzelm@20819
   163
apply (rule inj_onI)
wenzelm@20819
   164
apply (erule Atom_inject [THEN Inr_inject])
wenzelm@20819
   165
done
wenzelm@20819
   166
wenzelm@45607
   167
lemmas Numb_inject [dest!] = inj_Numb [THEN injD]
wenzelm@20819
   168
wenzelm@20819
   169
wenzelm@20819
   170
(** Injectiveness of Push_Node **)
wenzelm@20819
   171
wenzelm@20819
   172
lemma Push_Node_inject:
wenzelm@20819
   173
    "[| Push_Node i m =Push_Node j n;  [| i=j;  m=n |] ==> P  
wenzelm@20819
   174
     |] ==> P"
wenzelm@20819
   175
apply (simp add: Push_Node_def)
wenzelm@20819
   176
apply (erule Abs_Node_inj [THEN apfst_convE])
wenzelm@20819
   177
apply (rule Rep_Node [THEN Node_Push_I])+
wenzelm@20819
   178
apply (erule sym [THEN apfst_convE]) 
wenzelm@20819
   179
apply (blast intro: Rep_Node_inject [THEN iffD1] trans sym elim!: Push_inject)
wenzelm@20819
   180
done
wenzelm@20819
   181
wenzelm@20819
   182
wenzelm@20819
   183
(** Injectiveness of Scons **)
wenzelm@20819
   184
wenzelm@20819
   185
lemma Scons_inject_lemma1: "Scons M N <= Scons M' N' ==> M<=M'"
huffman@35216
   186
unfolding Scons_def One_nat_def
huffman@35216
   187
by (blast dest!: Push_Node_inject)
wenzelm@20819
   188
wenzelm@20819
   189
lemma Scons_inject_lemma2: "Scons M N <= Scons M' N' ==> N<=N'"
huffman@35216
   190
unfolding Scons_def One_nat_def
huffman@35216
   191
by (blast dest!: Push_Node_inject)
wenzelm@20819
   192
wenzelm@20819
   193
lemma Scons_inject1: "Scons M N = Scons M' N' ==> M=M'"
wenzelm@20819
   194
apply (erule equalityE)
wenzelm@20819
   195
apply (iprover intro: equalityI Scons_inject_lemma1)
wenzelm@20819
   196
done
wenzelm@20819
   197
wenzelm@20819
   198
lemma Scons_inject2: "Scons M N = Scons M' N' ==> N=N'"
wenzelm@20819
   199
apply (erule equalityE)
wenzelm@20819
   200
apply (iprover intro: equalityI Scons_inject_lemma2)
wenzelm@20819
   201
done
wenzelm@20819
   202
wenzelm@20819
   203
lemma Scons_inject:
wenzelm@20819
   204
    "[| Scons M N = Scons M' N';  [| M=M';  N=N' |] ==> P |] ==> P"
wenzelm@20819
   205
by (iprover dest: Scons_inject1 Scons_inject2)
wenzelm@20819
   206
wenzelm@67091
   207
lemma Scons_Scons_eq [iff]: "(Scons M N = Scons M' N') = (M=M' \<and> N=N')"
wenzelm@20819
   208
by (blast elim!: Scons_inject)
wenzelm@20819
   209
wenzelm@20819
   210
(*** Distinctness involving Leaf and Numb ***)
wenzelm@20819
   211
wenzelm@20819
   212
(** Scons vs Leaf **)
wenzelm@20819
   213
wenzelm@20819
   214
lemma Scons_not_Leaf [iff]: "Scons M N \<noteq> Leaf(a)"
huffman@35216
   215
unfolding Leaf_def o_def by (rule Scons_not_Atom)
wenzelm@20819
   216
wenzelm@45607
   217
lemmas Leaf_not_Scons  [iff] = Scons_not_Leaf [THEN not_sym]
wenzelm@20819
   218
wenzelm@20819
   219
(** Scons vs Numb **)
wenzelm@20819
   220
wenzelm@20819
   221
lemma Scons_not_Numb [iff]: "Scons M N \<noteq> Numb(k)"
huffman@35216
   222
unfolding Numb_def o_def by (rule Scons_not_Atom)
wenzelm@20819
   223
wenzelm@45607
   224
lemmas Numb_not_Scons [iff] = Scons_not_Numb [THEN not_sym]
wenzelm@20819
   225
wenzelm@20819
   226
wenzelm@20819
   227
(** Leaf vs Numb **)
wenzelm@20819
   228
wenzelm@20819
   229
lemma Leaf_not_Numb [iff]: "Leaf(a) \<noteq> Numb(k)"
wenzelm@20819
   230
by (simp add: Leaf_def Numb_def)
wenzelm@20819
   231
wenzelm@45607
   232
lemmas Numb_not_Leaf [iff] = Leaf_not_Numb [THEN not_sym]
wenzelm@20819
   233
wenzelm@20819
   234
wenzelm@20819
   235
(*** ndepth -- the depth of a node ***)
wenzelm@20819
   236
wenzelm@20819
   237
lemma ndepth_K0: "ndepth (Abs_Node(%k. Inr 0, x)) = 0"
wenzelm@20819
   238
by (simp add: ndepth_def  Node_K0_I [THEN Abs_Node_inverse] Least_equality)
wenzelm@20819
   239
wenzelm@20819
   240
lemma ndepth_Push_Node_aux:
wenzelm@67091
   241
     "case_nat (Inr (Suc i)) f k = Inr 0 \<longrightarrow> Suc(LEAST x. f x = Inr 0) \<le> k"
wenzelm@20819
   242
apply (induct_tac "k", auto)
wenzelm@20819
   243
apply (erule Least_le)
wenzelm@20819
   244
done
wenzelm@20819
   245
wenzelm@20819
   246
lemma ndepth_Push_Node: 
wenzelm@20819
   247
    "ndepth (Push_Node (Inr (Suc i)) n) = Suc(ndepth(n))"
wenzelm@20819
   248
apply (insert Rep_Node [of n, unfolded Node_def])
wenzelm@20819
   249
apply (auto simp add: ndepth_def Push_Node_def
wenzelm@20819
   250
                 Rep_Node [THEN Node_Push_I, THEN Abs_Node_inverse])
wenzelm@20819
   251
apply (rule Least_equality)
wenzelm@20819
   252
apply (auto simp add: Push_def ndepth_Push_Node_aux)
wenzelm@20819
   253
apply (erule LeastI)
wenzelm@20819
   254
done
wenzelm@20819
   255
wenzelm@20819
   256
wenzelm@20819
   257
(*** ntrunc applied to the various node sets ***)
wenzelm@20819
   258
wenzelm@20819
   259
lemma ntrunc_0 [simp]: "ntrunc 0 M = {}"
wenzelm@20819
   260
by (simp add: ntrunc_def)
wenzelm@20819
   261
wenzelm@20819
   262
lemma ntrunc_Atom [simp]: "ntrunc (Suc k) (Atom a) = Atom(a)"
wenzelm@20819
   263
by (auto simp add: Atom_def ntrunc_def ndepth_K0)
wenzelm@20819
   264
wenzelm@20819
   265
lemma ntrunc_Leaf [simp]: "ntrunc (Suc k) (Leaf a) = Leaf(a)"
huffman@35216
   266
unfolding Leaf_def o_def by (rule ntrunc_Atom)
wenzelm@20819
   267
wenzelm@20819
   268
lemma ntrunc_Numb [simp]: "ntrunc (Suc k) (Numb i) = Numb(i)"
huffman@35216
   269
unfolding Numb_def o_def by (rule ntrunc_Atom)
wenzelm@20819
   270
wenzelm@20819
   271
lemma ntrunc_Scons [simp]: 
wenzelm@20819
   272
    "ntrunc (Suc k) (Scons M N) = Scons (ntrunc k M) (ntrunc k N)"
huffman@35216
   273
unfolding Scons_def ntrunc_def One_nat_def
huffman@35216
   274
by (auto simp add: ndepth_Push_Node)
wenzelm@20819
   275
wenzelm@20819
   276
wenzelm@20819
   277
wenzelm@20819
   278
(** Injection nodes **)
wenzelm@20819
   279
wenzelm@20819
   280
lemma ntrunc_one_In0 [simp]: "ntrunc (Suc 0) (In0 M) = {}"
wenzelm@20819
   281
apply (simp add: In0_def)
wenzelm@20819
   282
apply (simp add: Scons_def)
wenzelm@20819
   283
done
wenzelm@20819
   284
wenzelm@20819
   285
lemma ntrunc_In0 [simp]: "ntrunc (Suc(Suc k)) (In0 M) = In0 (ntrunc (Suc k) M)"
wenzelm@20819
   286
by (simp add: In0_def)
wenzelm@20819
   287
wenzelm@20819
   288
lemma ntrunc_one_In1 [simp]: "ntrunc (Suc 0) (In1 M) = {}"
wenzelm@20819
   289
apply (simp add: In1_def)
wenzelm@20819
   290
apply (simp add: Scons_def)
wenzelm@20819
   291
done
wenzelm@20819
   292
wenzelm@20819
   293
lemma ntrunc_In1 [simp]: "ntrunc (Suc(Suc k)) (In1 M) = In1 (ntrunc (Suc k) M)"
wenzelm@20819
   294
by (simp add: In1_def)
wenzelm@20819
   295
wenzelm@20819
   296
wenzelm@60500
   297
subsection\<open>Set Constructions\<close>
wenzelm@20819
   298
wenzelm@20819
   299
wenzelm@20819
   300
(*** Cartesian Product ***)
wenzelm@20819
   301
wenzelm@67613
   302
lemma uprodI [intro!]: "\<lbrakk>M\<in>A; N\<in>B\<rbrakk> \<Longrightarrow> Scons M N \<in> uprod A B"
wenzelm@20819
   303
by (simp add: uprod_def)
wenzelm@20819
   304
wenzelm@20819
   305
(*The general elimination rule*)
wenzelm@20819
   306
lemma uprodE [elim!]:
wenzelm@67613
   307
    "\<lbrakk>c \<in> uprod A B;   
wenzelm@67613
   308
        \<And>x y. \<lbrakk>x \<in> A; y \<in> B; c = Scons x y\<rbrakk> \<Longrightarrow> P  
wenzelm@67613
   309
     \<rbrakk> \<Longrightarrow> P"
wenzelm@20819
   310
by (auto simp add: uprod_def) 
wenzelm@20819
   311
wenzelm@20819
   312
wenzelm@20819
   313
(*Elimination of a pair -- introduces no eigenvariables*)
wenzelm@67613
   314
lemma uprodE2: "\<lbrakk>Scons M N \<in> uprod A B; \<lbrakk>M \<in> A; N \<in> B\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
wenzelm@20819
   315
by (auto simp add: uprod_def)
wenzelm@20819
   316
wenzelm@20819
   317
wenzelm@20819
   318
(*** Disjoint Sum ***)
wenzelm@20819
   319
wenzelm@67613
   320
lemma usum_In0I [intro]: "M \<in> A \<Longrightarrow> In0(M) \<in> usum A B"
wenzelm@20819
   321
by (simp add: usum_def)
wenzelm@20819
   322
wenzelm@67613
   323
lemma usum_In1I [intro]: "N \<in> B \<Longrightarrow> In1(N) \<in> usum A B"
wenzelm@20819
   324
by (simp add: usum_def)
wenzelm@20819
   325
wenzelm@20819
   326
lemma usumE [elim!]: 
wenzelm@67613
   327
    "\<lbrakk>u \<in> usum A B;   
wenzelm@67613
   328
        \<And>x. \<lbrakk>x \<in> A; u=In0(x)\<rbrakk> \<Longrightarrow> P;  
wenzelm@67613
   329
        \<And>y. \<lbrakk>y \<in> B; u=In1(y)\<rbrakk> \<Longrightarrow> P  
wenzelm@67613
   330
     \<rbrakk> \<Longrightarrow> P"
wenzelm@20819
   331
by (auto simp add: usum_def)
wenzelm@20819
   332
wenzelm@20819
   333
wenzelm@20819
   334
(** Injection **)
wenzelm@20819
   335
wenzelm@20819
   336
lemma In0_not_In1 [iff]: "In0(M) \<noteq> In1(N)"
huffman@35216
   337
unfolding In0_def In1_def One_nat_def by auto
wenzelm@20819
   338
wenzelm@45607
   339
lemmas In1_not_In0 [iff] = In0_not_In1 [THEN not_sym]
wenzelm@20819
   340
wenzelm@20819
   341
lemma In0_inject: "In0(M) = In0(N) ==>  M=N"
wenzelm@20819
   342
by (simp add: In0_def)
wenzelm@20819
   343
wenzelm@20819
   344
lemma In1_inject: "In1(M) = In1(N) ==>  M=N"
wenzelm@20819
   345
by (simp add: In1_def)
wenzelm@20819
   346
wenzelm@20819
   347
lemma In0_eq [iff]: "(In0 M = In0 N) = (M=N)"
wenzelm@20819
   348
by (blast dest!: In0_inject)
wenzelm@20819
   349
wenzelm@20819
   350
lemma In1_eq [iff]: "(In1 M = In1 N) = (M=N)"
wenzelm@20819
   351
by (blast dest!: In1_inject)
wenzelm@20819
   352
wenzelm@20819
   353
lemma inj_In0: "inj In0"
wenzelm@20819
   354
by (blast intro!: inj_onI)
wenzelm@20819
   355
wenzelm@20819
   356
lemma inj_In1: "inj In1"
wenzelm@20819
   357
by (blast intro!: inj_onI)
wenzelm@20819
   358
wenzelm@20819
   359
wenzelm@20819
   360
(*** Function spaces ***)
wenzelm@20819
   361
wenzelm@20819
   362
lemma Lim_inject: "Lim f = Lim g ==> f = g"
wenzelm@20819
   363
apply (simp add: Lim_def)
wenzelm@20819
   364
apply (rule ext)
wenzelm@20819
   365
apply (blast elim!: Push_Node_inject)
wenzelm@20819
   366
done
wenzelm@20819
   367
wenzelm@20819
   368
wenzelm@20819
   369
(*** proving equality of sets and functions using ntrunc ***)
wenzelm@20819
   370
wenzelm@20819
   371
lemma ntrunc_subsetI: "ntrunc k M <= M"
wenzelm@20819
   372
by (auto simp add: ntrunc_def)
wenzelm@20819
   373
wenzelm@20819
   374
lemma ntrunc_subsetD: "(!!k. ntrunc k M <= N) ==> M<=N"
wenzelm@20819
   375
by (auto simp add: ntrunc_def)
wenzelm@20819
   376
wenzelm@20819
   377
(*A generalized form of the take-lemma*)
wenzelm@20819
   378
lemma ntrunc_equality: "(!!k. ntrunc k M = ntrunc k N) ==> M=N"
wenzelm@20819
   379
apply (rule equalityI)
wenzelm@20819
   380
apply (rule_tac [!] ntrunc_subsetD)
wenzelm@20819
   381
apply (rule_tac [!] ntrunc_subsetI [THEN [2] subset_trans], auto) 
wenzelm@20819
   382
done
wenzelm@20819
   383
wenzelm@20819
   384
lemma ntrunc_o_equality: 
wenzelm@67091
   385
    "[| !!k. (ntrunc(k) \<circ> h1) = (ntrunc(k) \<circ> h2) |] ==> h1=h2"
wenzelm@20819
   386
apply (rule ntrunc_equality [THEN ext])
nipkow@39302
   387
apply (simp add: fun_eq_iff) 
wenzelm@20819
   388
done
wenzelm@20819
   389
wenzelm@20819
   390
wenzelm@20819
   391
(*** Monotonicity ***)
wenzelm@20819
   392
wenzelm@20819
   393
lemma uprod_mono: "[| A<=A';  B<=B' |] ==> uprod A B <= uprod A' B'"
wenzelm@20819
   394
by (simp add: uprod_def, blast)
wenzelm@20819
   395
wenzelm@20819
   396
lemma usum_mono: "[| A<=A';  B<=B' |] ==> usum A B <= usum A' B'"
wenzelm@20819
   397
by (simp add: usum_def, blast)
wenzelm@20819
   398
wenzelm@20819
   399
lemma Scons_mono: "[| M<=M';  N<=N' |] ==> Scons M N <= Scons M' N'"
wenzelm@20819
   400
by (simp add: Scons_def, blast)
wenzelm@20819
   401
wenzelm@20819
   402
lemma In0_mono: "M<=N ==> In0(M) <= In0(N)"
huffman@35216
   403
by (simp add: In0_def Scons_mono)
wenzelm@20819
   404
wenzelm@20819
   405
lemma In1_mono: "M<=N ==> In1(M) <= In1(N)"
huffman@35216
   406
by (simp add: In1_def Scons_mono)
wenzelm@20819
   407
wenzelm@20819
   408
wenzelm@20819
   409
(*** Split and Case ***)
wenzelm@20819
   410
wenzelm@20819
   411
lemma Split [simp]: "Split c (Scons M N) = c M N"
wenzelm@20819
   412
by (simp add: Split_def)
wenzelm@20819
   413
wenzelm@20819
   414
lemma Case_In0 [simp]: "Case c d (In0 M) = c(M)"
wenzelm@20819
   415
by (simp add: Case_def)
wenzelm@20819
   416
wenzelm@20819
   417
lemma Case_In1 [simp]: "Case c d (In1 N) = d(N)"
wenzelm@20819
   418
by (simp add: Case_def)
wenzelm@20819
   419
wenzelm@20819
   420
wenzelm@20819
   421
wenzelm@20819
   422
(**** UN x. B(x) rules ****)
wenzelm@20819
   423
wenzelm@20819
   424
lemma ntrunc_UN1: "ntrunc k (UN x. f(x)) = (UN x. ntrunc k (f x))"
wenzelm@20819
   425
by (simp add: ntrunc_def, blast)
wenzelm@20819
   426
wenzelm@20819
   427
lemma Scons_UN1_x: "Scons (UN x. f x) M = (UN x. Scons (f x) M)"
wenzelm@20819
   428
by (simp add: Scons_def, blast)
wenzelm@20819
   429
wenzelm@20819
   430
lemma Scons_UN1_y: "Scons M (UN x. f x) = (UN x. Scons M (f x))"
wenzelm@20819
   431
by (simp add: Scons_def, blast)
wenzelm@20819
   432
wenzelm@20819
   433
lemma In0_UN1: "In0(UN x. f(x)) = (UN x. In0(f(x)))"
wenzelm@20819
   434
by (simp add: In0_def Scons_UN1_y)
wenzelm@20819
   435
wenzelm@20819
   436
lemma In1_UN1: "In1(UN x. f(x)) = (UN x. In1(f(x)))"
wenzelm@20819
   437
by (simp add: In1_def Scons_UN1_y)
wenzelm@20819
   438
wenzelm@20819
   439
wenzelm@20819
   440
(*** Equality for Cartesian Product ***)
wenzelm@20819
   441
wenzelm@20819
   442
lemma dprodI [intro!]: 
wenzelm@67613
   443
    "\<lbrakk>(M,M') \<in> r; (N,N') \<in> s\<rbrakk> \<Longrightarrow> (Scons M N, Scons M' N') \<in> dprod r s"
wenzelm@20819
   444
by (auto simp add: dprod_def)
wenzelm@20819
   445
wenzelm@20819
   446
(*The general elimination rule*)
wenzelm@20819
   447
lemma dprodE [elim!]: 
wenzelm@67613
   448
    "\<lbrakk>c \<in> dprod r s;   
wenzelm@67613
   449
        \<And>x y x' y'. \<lbrakk>(x,x') \<in> r; (y,y') \<in> s;  
wenzelm@67613
   450
                        c = (Scons x y, Scons x' y')\<rbrakk> \<Longrightarrow> P  
wenzelm@67613
   451
     \<rbrakk> \<Longrightarrow> P"
wenzelm@20819
   452
by (auto simp add: dprod_def)
wenzelm@20819
   453
wenzelm@20819
   454
wenzelm@20819
   455
(*** Equality for Disjoint Sum ***)
wenzelm@20819
   456
wenzelm@67613
   457
lemma dsum_In0I [intro]: "(M,M') \<in> r \<Longrightarrow> (In0(M), In0(M')) \<in> dsum r s"
wenzelm@20819
   458
by (auto simp add: dsum_def)
wenzelm@20819
   459
wenzelm@67613
   460
lemma dsum_In1I [intro]: "(N,N') \<in> s \<Longrightarrow> (In1(N), In1(N')) \<in> dsum r s"
wenzelm@20819
   461
by (auto simp add: dsum_def)
wenzelm@20819
   462
wenzelm@20819
   463
lemma dsumE [elim!]: 
wenzelm@67613
   464
    "\<lbrakk>w \<in> dsum r s;   
wenzelm@67613
   465
        \<And>x x'. \<lbrakk> (x,x') \<in> r;  w = (In0(x), In0(x')) \<rbrakk> \<Longrightarrow> P;  
wenzelm@67613
   466
        \<And>y y'. \<lbrakk> (y,y') \<in> s;  w = (In1(y), In1(y')) \<rbrakk> \<Longrightarrow> P  
wenzelm@67613
   467
     \<rbrakk> \<Longrightarrow> P"
wenzelm@20819
   468
by (auto simp add: dsum_def)
wenzelm@20819
   469
wenzelm@20819
   470
wenzelm@20819
   471
(*** Monotonicity ***)
wenzelm@20819
   472
wenzelm@20819
   473
lemma dprod_mono: "[| r<=r';  s<=s' |] ==> dprod r s <= dprod r' s'"
wenzelm@20819
   474
by blast
wenzelm@20819
   475
wenzelm@20819
   476
lemma dsum_mono: "[| r<=r';  s<=s' |] ==> dsum r s <= dsum r' s'"
wenzelm@20819
   477
by blast
wenzelm@20819
   478
wenzelm@20819
   479
wenzelm@20819
   480
(*** Bounding theorems ***)
wenzelm@20819
   481
wenzelm@61943
   482
lemma dprod_Sigma: "(dprod (A \<times> B) (C \<times> D)) <= (uprod A C) \<times> (uprod B D)"
wenzelm@20819
   483
by blast
wenzelm@20819
   484
wenzelm@45607
   485
lemmas dprod_subset_Sigma = subset_trans [OF dprod_mono dprod_Sigma]
wenzelm@20819
   486
wenzelm@20819
   487
(*Dependent version*)
wenzelm@20819
   488
lemma dprod_subset_Sigma2:
blanchet@58112
   489
    "(dprod (Sigma A B) (Sigma C D)) <= Sigma (uprod A C) (Split (%x y. uprod (B x) (D y)))"
wenzelm@20819
   490
by auto
wenzelm@20819
   491
wenzelm@61943
   492
lemma dsum_Sigma: "(dsum (A \<times> B) (C \<times> D)) <= (usum A C) \<times> (usum B D)"
wenzelm@20819
   493
by blast
wenzelm@20819
   494
wenzelm@45607
   495
lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma]
wenzelm@20819
   496
wenzelm@20819
   497
blanchet@58157
   498
(*** Domain theorems ***)
blanchet@58157
   499
blanchet@58157
   500
lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
blanchet@58157
   501
  by auto
blanchet@58157
   502
blanchet@58157
   503
lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)"
blanchet@58157
   504
  by auto
blanchet@58157
   505
blanchet@58157
   506
wenzelm@60500
   507
text \<open>hides popular names\<close>
wenzelm@36176
   508
hide_type (open) node item
wenzelm@36176
   509
hide_const (open) Push Node Atom Leaf Numb Lim Split Case
wenzelm@20819
   510
blanchet@58372
   511
ML_file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
berghofe@13635
   512
berghofe@5181
   513
end