src/HOL/Library/Old_Datatype.thy
changeset 67613 ce654b0e6d69
parent 67319 07176d5b81d5
child 69605 a96320074298
     1.1 --- a/src/HOL/Library/Old_Datatype.thy	Tue Feb 13 14:24:50 2018 +0100
     1.2 +++ b/src/HOL/Library/Old_Datatype.thy	Thu Feb 15 12:11:00 2018 +0100
     1.3 @@ -59,7 +59,7 @@
     1.4  definition ndepth :: "('a, 'b) node => nat"
     1.5    where "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)"
     1.6  definition ntrunc :: "[nat, ('a, 'b) dtree] => ('a, 'b) dtree"
     1.7 -  where "ntrunc k N == {n. n:N \<and> ndepth(n)<k}"
     1.8 +  where "ntrunc k N == {n. n\<in>N \<and> ndepth(n)<k}"
     1.9  
    1.10  (*products and sums for the "universe"*)
    1.11  definition uprod :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set"
    1.12 @@ -115,10 +115,10 @@
    1.13  
    1.14  (*** Introduction rules for Node ***)
    1.15  
    1.16 -lemma Node_K0_I: "(%k. Inr 0, a) : Node"
    1.17 +lemma Node_K0_I: "(\<lambda>k. Inr 0, a) \<in> Node"
    1.18  by (simp add: Node_def)
    1.19  
    1.20 -lemma Node_Push_I: "p: Node ==> apfst (Push i) p : Node"
    1.21 +lemma Node_Push_I: "p \<in> Node \<Longrightarrow> apfst (Push i) p \<in> Node"
    1.22  apply (simp add: Node_def Push_def) 
    1.23  apply (fast intro!: apfst_conv nat.case(2)[THEN trans])
    1.24  done
    1.25 @@ -299,35 +299,35 @@
    1.26  
    1.27  (*** Cartesian Product ***)
    1.28  
    1.29 -lemma uprodI [intro!]: "[| M:A;  N:B |] ==> Scons M N : uprod A B"
    1.30 +lemma uprodI [intro!]: "\<lbrakk>M\<in>A; N\<in>B\<rbrakk> \<Longrightarrow> Scons M N \<in> uprod A B"
    1.31  by (simp add: uprod_def)
    1.32  
    1.33  (*The general elimination rule*)
    1.34  lemma uprodE [elim!]:
    1.35 -    "[| c : uprod A B;   
    1.36 -        !!x y. [| x:A;  y:B;  c = Scons x y |] ==> P  
    1.37 -     |] ==> P"
    1.38 +    "\<lbrakk>c \<in> uprod A B;   
    1.39 +        \<And>x y. \<lbrakk>x \<in> A; y \<in> B; c = Scons x y\<rbrakk> \<Longrightarrow> P  
    1.40 +     \<rbrakk> \<Longrightarrow> P"
    1.41  by (auto simp add: uprod_def) 
    1.42  
    1.43  
    1.44  (*Elimination of a pair -- introduces no eigenvariables*)
    1.45 -lemma uprodE2: "[| Scons M N : uprod A B;  [| M:A;  N:B |] ==> P |] ==> P"
    1.46 +lemma uprodE2: "\<lbrakk>Scons M N \<in> uprod A B; \<lbrakk>M \<in> A; N \<in> B\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    1.47  by (auto simp add: uprod_def)
    1.48  
    1.49  
    1.50  (*** Disjoint Sum ***)
    1.51  
    1.52 -lemma usum_In0I [intro]: "M:A ==> In0(M) : usum A B"
    1.53 +lemma usum_In0I [intro]: "M \<in> A \<Longrightarrow> In0(M) \<in> usum A B"
    1.54  by (simp add: usum_def)
    1.55  
    1.56 -lemma usum_In1I [intro]: "N:B ==> In1(N) : usum A B"
    1.57 +lemma usum_In1I [intro]: "N \<in> B \<Longrightarrow> In1(N) \<in> usum A B"
    1.58  by (simp add: usum_def)
    1.59  
    1.60  lemma usumE [elim!]: 
    1.61 -    "[| u : usum A B;   
    1.62 -        !!x. [| x:A;  u=In0(x) |] ==> P;  
    1.63 -        !!y. [| y:B;  u=In1(y) |] ==> P  
    1.64 -     |] ==> P"
    1.65 +    "\<lbrakk>u \<in> usum A B;   
    1.66 +        \<And>x. \<lbrakk>x \<in> A; u=In0(x)\<rbrakk> \<Longrightarrow> P;  
    1.67 +        \<And>y. \<lbrakk>y \<in> B; u=In1(y)\<rbrakk> \<Longrightarrow> P  
    1.68 +     \<rbrakk> \<Longrightarrow> P"
    1.69  by (auto simp add: usum_def)
    1.70  
    1.71  
    1.72 @@ -440,31 +440,31 @@
    1.73  (*** Equality for Cartesian Product ***)
    1.74  
    1.75  lemma dprodI [intro!]: 
    1.76 -    "[| (M,M'):r;  (N,N'):s |] ==> (Scons M N, Scons M' N') : dprod r s"
    1.77 +    "\<lbrakk>(M,M') \<in> r; (N,N') \<in> s\<rbrakk> \<Longrightarrow> (Scons M N, Scons M' N') \<in> dprod r s"
    1.78  by (auto simp add: dprod_def)
    1.79  
    1.80  (*The general elimination rule*)
    1.81  lemma dprodE [elim!]: 
    1.82 -    "[| c : dprod r s;   
    1.83 -        !!x y x' y'. [| (x,x') : r;  (y,y') : s;  
    1.84 -                        c = (Scons x y, Scons x' y') |] ==> P  
    1.85 -     |] ==> P"
    1.86 +    "\<lbrakk>c \<in> dprod r s;   
    1.87 +        \<And>x y x' y'. \<lbrakk>(x,x') \<in> r; (y,y') \<in> s;  
    1.88 +                        c = (Scons x y, Scons x' y')\<rbrakk> \<Longrightarrow> P  
    1.89 +     \<rbrakk> \<Longrightarrow> P"
    1.90  by (auto simp add: dprod_def)
    1.91  
    1.92  
    1.93  (*** Equality for Disjoint Sum ***)
    1.94  
    1.95 -lemma dsum_In0I [intro]: "(M,M'):r ==> (In0(M), In0(M')) : dsum r s"
    1.96 +lemma dsum_In0I [intro]: "(M,M') \<in> r \<Longrightarrow> (In0(M), In0(M')) \<in> dsum r s"
    1.97  by (auto simp add: dsum_def)
    1.98  
    1.99 -lemma dsum_In1I [intro]: "(N,N'):s ==> (In1(N), In1(N')) : dsum r s"
   1.100 +lemma dsum_In1I [intro]: "(N,N') \<in> s \<Longrightarrow> (In1(N), In1(N')) \<in> dsum r s"
   1.101  by (auto simp add: dsum_def)
   1.102  
   1.103  lemma dsumE [elim!]: 
   1.104 -    "[| w : dsum r s;   
   1.105 -        !!x x'. [| (x,x') : r;  w = (In0(x), In0(x')) |] ==> P;  
   1.106 -        !!y y'. [| (y,y') : s;  w = (In1(y), In1(y')) |] ==> P  
   1.107 -     |] ==> P"
   1.108 +    "\<lbrakk>w \<in> dsum r s;   
   1.109 +        \<And>x x'. \<lbrakk> (x,x') \<in> r;  w = (In0(x), In0(x')) \<rbrakk> \<Longrightarrow> P;  
   1.110 +        \<And>y y'. \<lbrakk> (y,y') \<in> s;  w = (In1(y), In1(y')) \<rbrakk> \<Longrightarrow> P  
   1.111 +     \<rbrakk> \<Longrightarrow> P"
   1.112  by (auto simp add: dsum_def)
   1.113  
   1.114