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