src/HOL/Library/Old_Datatype.thy
 changeset 67091 1393c2340eec parent 65513 587433a18053 child 67318 0ee38196509e
```     1.1 --- a/src/HOL/Library/Old_Datatype.thy	Sun Nov 26 13:19:52 2017 +0100
1.2 +++ b/src/HOL/Library/Old_Datatype.thy	Sun Nov 26 21:08:32 2017 +0100
1.3 @@ -15,7 +15,7 @@
1.4
1.5  subsection \<open>The datatype universe\<close>
1.6
1.7 -definition "Node = {p. EX f x k. p = (f :: nat => 'b + nat, x ::'a + nat) & f k = Inr 0}"
1.8 +definition "Node = {p. \<exists>f x k. p = (f :: nat => 'b + nat, x ::'a + nat) \<and> f k = Inr 0}"
1.9
1.10  typedef ('a, 'b) node = "Node :: ((nat => 'b + nat) * ('a + nat)) set"
1.11    morphisms Rep_Node Abs_Node
1.12 @@ -44,9 +44,9 @@
1.13
1.14  (*Leaf nodes, with arbitrary or nat labels*)
1.15  definition Leaf :: "'a => ('a, 'b) dtree"
1.16 -  where "Leaf == Atom o Inl"
1.17 +  where "Leaf == Atom \<circ> Inl"
1.18  definition Numb :: "nat => ('a, 'b) dtree"
1.19 -  where "Numb == Atom o Inr"
1.20 +  where "Numb == Atom \<circ> Inr"
1.21
1.22  (*Injections of the "disjoint sum"*)
1.23  definition In0 :: "('a, 'b) dtree => ('a, 'b) dtree"
1.24 @@ -56,13 +56,13 @@
1.25
1.26  (*Function spaces*)
1.27  definition Lim :: "('b => ('a, 'b) dtree) => ('a, 'b) dtree"
1.28 -  where "Lim f == \<Union>{z. ? x. z = Push_Node (Inl x) ` (f x)}"
1.29 +  where "Lim f == \<Union>{z. \<exists>x. z = Push_Node (Inl x) ` (f x)}"
1.30
1.31  (*the set of nodes with depth less than k*)
1.32  definition ndepth :: "('a, 'b) node => nat"
1.33    where "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)"
1.34  definition ntrunc :: "[nat, ('a, 'b) dtree] => ('a, 'b) dtree"
1.35 -  where "ntrunc k N == {n. n:N & ndepth(n)<k}"
1.36 +  where "ntrunc k N == {n. n:N \<and> ndepth(n)<k}"
1.37
1.38  (*products and sums for the "universe"*)
1.39  definition uprod :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set"
1.40 @@ -72,10 +72,10 @@
1.41
1.42  (*the corresponding eliminators*)
1.43  definition Split :: "[[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c"
1.44 -  where "Split c M == THE u. EX x y. M = Scons x y & u = c x y"
1.45 +  where "Split c M == THE u. \<exists>x y. M = Scons x y \<and> u = c x y"
1.46
1.47  definition Case :: "[[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c"
1.48 -  where "Case c d M == THE u. (EX x . M = In0(x) & u = c(x)) | (EX y . M = In1(y) & u = d(y))"
1.49 +  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))"
1.50
1.51
1.52  (** equality for the "universe" **)
1.53 @@ -207,7 +207,7 @@
1.54      "[| Scons M N = Scons M' N';  [| M=M';  N=N' |] ==> P |] ==> P"
1.55  by (iprover dest: Scons_inject1 Scons_inject2)
1.56
1.57 -lemma Scons_Scons_eq [iff]: "(Scons M N = Scons M' N') = (M=M' & N=N')"
1.58 +lemma Scons_Scons_eq [iff]: "(Scons M N = Scons M' N') = (M=M' \<and> N=N')"
1.59  by (blast elim!: Scons_inject)
1.60
1.61  (*** Distinctness involving Leaf and Numb ***)
1.62 @@ -241,7 +241,7 @@
1.63  by (simp add: ndepth_def  Node_K0_I [THEN Abs_Node_inverse] Least_equality)
1.64
1.65  lemma ndepth_Push_Node_aux:
1.66 -     "case_nat (Inr (Suc i)) f k = Inr 0 --> Suc(LEAST x. f x = Inr 0) <= k"
1.67 +     "case_nat (Inr (Suc i)) f k = Inr 0 \<longrightarrow> Suc(LEAST x. f x = Inr 0) \<le> k"
1.68  apply (induct_tac "k", auto)
1.69  apply (erule Least_le)
1.70  done
1.71 @@ -385,7 +385,7 @@
1.72  done
1.73
1.74  lemma ntrunc_o_equality:
1.75 -    "[| !!k. (ntrunc(k) o h1) = (ntrunc(k) o h2) |] ==> h1=h2"
1.76 +    "[| !!k. (ntrunc(k) \<circ> h1) = (ntrunc(k) \<circ> h2) |] ==> h1=h2"
1.77  apply (rule ntrunc_equality [THEN ext])