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])
    1.78  apply (simp add: fun_eq_iff) 
    1.79  done