src/HOL/MicroJava/BV/Listn.thy
changeset 15341 254f6f00b60e
parent 13601 fd3e3d6b37b2
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/MicroJava/BV/Listn.thy	Mon Nov 29 11:25:32 2004 +0100
     1.2 +++ b/src/HOL/MicroJava/BV/Listn.thy	Mon Nov 29 14:02:55 2004 +0100
     1.3 @@ -185,19 +185,19 @@
     1.4  done 
     1.5  
     1.6  lemma in_list_Suc_iff: 
     1.7 -  "(xs : list (Suc n) A) = (? y:A. ? ys:list n A. xs = y#ys)"
     1.8 +  "(xs : list (Suc n) A) = (\<exists>y\<in> A. \<exists>ys\<in> list n A. xs = y#ys)"
     1.9  apply (unfold list_def)
    1.10  apply (case_tac "xs")
    1.11  apply auto
    1.12  done 
    1.13  
    1.14  lemma Cons_in_list_Suc [iff]:
    1.15 -  "(x#xs : list (Suc n) A) = (x:A & xs : list n A)";
    1.16 +  "(x#xs : list (Suc n) A) = (x\<in> A & xs : list n A)";
    1.17  apply (simp add: in_list_Suc_iff)
    1.18  done 
    1.19  
    1.20  lemma list_not_empty:
    1.21 -  "? a. a:A \<Longrightarrow> ? xs. xs : list n A";
    1.22 +  "\<exists>a. a\<in> A \<Longrightarrow> \<exists>xs. xs : list n A";
    1.23  apply (induct "n")
    1.24   apply simp
    1.25  apply (simp add: in_list_Suc_iff)
    1.26 @@ -248,7 +248,7 @@
    1.27  
    1.28  
    1.29  lemma listt_update_in_list [simp, intro!]:
    1.30 -  "\<lbrakk> xs : list n A; x:A \<rbrakk> \<Longrightarrow> xs[i := x] : list n A"
    1.31 +  "\<lbrakk> xs : list n A; x\<in> A \<rbrakk> \<Longrightarrow> xs[i := x] : list n A"
    1.32  apply (unfold list_def)
    1.33  apply simp
    1.34  done 
    1.35 @@ -306,7 +306,7 @@
    1.36  done
    1.37  
    1.38  lemma (in semilat) list_update_incr [rule_format]:
    1.39 - "x:A \<Longrightarrow> set xs <= A \<longrightarrow> 
    1.40 + "x\<in> A \<Longrightarrow> set xs <= A \<longrightarrow> 
    1.41    (!i. i<size xs \<longrightarrow> xs <=[r] xs[i := x +_f xs!i])"
    1.42  apply (unfold unfold_lesub_list)
    1.43  apply (simp add: Listn.le_def list_all2_conv_all_nth)
    1.44 @@ -330,8 +330,6 @@
    1.45   apply (rename_tac m n)
    1.46   apply (case_tac "m=n")
    1.47    apply simp
    1.48 - apply (rule conjI)
    1.49 -  apply (fast intro!: equals0I dest: not_sym)
    1.50   apply (fast intro!: equals0I dest: not_sym)
    1.51  apply clarify
    1.52  apply (rename_tac n)
    1.53 @@ -342,15 +340,15 @@
    1.54  apply (simp (no_asm) add: length_Suc_conv cong: conj_cong)
    1.55  apply clarify
    1.56  apply (rename_tac M m)
    1.57 -apply (case_tac "? x xs. size xs = k & x#xs : M")
    1.58 +apply (case_tac "\<exists>x xs. size xs = k & x#xs : M")
    1.59   prefer 2
    1.60   apply (erule thin_rl)
    1.61   apply (erule thin_rl)
    1.62   apply blast
    1.63 -apply (erule_tac x = "{a. ? xs. size xs = k & a#xs:M}" in allE)
    1.64 +apply (erule_tac x = "{a. \<exists>xs. size xs = k & a#xs:M}" in allE)
    1.65  apply (erule impE)
    1.66   apply blast
    1.67 -apply (thin_tac "? x xs. ?P x xs")
    1.68 +apply (thin_tac "\<exists>x xs. ?P x xs")
    1.69  apply clarify
    1.70  apply (rename_tac maxA xs)
    1.71  apply (erule_tac x = "{ys. size ys = size xs & maxA#ys : M}" in allE)
    1.72 @@ -435,8 +433,8 @@
    1.73  done 
    1.74  
    1.75  lemma lift2_le_ub:
    1.76 -  "\<lbrakk> semilat(err A, Err.le r, lift2 f); x:A; y:A; x +_f y = OK z; 
    1.77 -      u:A; x <=_r u; y <=_r u \<rbrakk> \<Longrightarrow> z <=_r u"
    1.78 +  "\<lbrakk> semilat(err A, Err.le r, lift2 f); x\<in> A; y\<in> A; x +_f y = OK z; 
    1.79 +      u\<in> A; x <=_r u; y <=_r u \<rbrakk> \<Longrightarrow> z <=_r u"
    1.80  apply (unfold semilat_Def plussub_def err_def)
    1.81  apply (simp add: lift2_def)
    1.82  apply clarify
    1.83 @@ -464,16 +462,16 @@
    1.84  done 
    1.85  
    1.86  lemma lift2_eq_ErrD:
    1.87 -  "\<lbrakk> x +_f y = Err; semilat(err A, Err.le r, lift2 f); x:A; y:A \<rbrakk> 
    1.88 -  \<Longrightarrow> ~(? u:A. x <=_r u & y <=_r u)"
    1.89 +  "\<lbrakk> x +_f y = Err; semilat(err A, Err.le r, lift2 f); x\<in> A; y\<in> A \<rbrakk> 
    1.90 +  \<Longrightarrow> ~(\<exists>u\<in> A. x <=_r u & y <=_r u)"
    1.91    by (simp add: OK_plus_OK_eq_Err_conv [THEN iffD1])
    1.92  
    1.93  
    1.94  lemma coalesce_eq_Err_D [rule_format]:
    1.95    "\<lbrakk> semilat(err A, Err.le r, lift2 f) \<rbrakk> 
    1.96 -  \<Longrightarrow> !xs. xs:list n A \<longrightarrow> (!ys. ys:list n A \<longrightarrow> 
    1.97 +  \<Longrightarrow> !xs. xs\<in> list n A \<longrightarrow> (!ys. ys\<in> list n A \<longrightarrow> 
    1.98        coalesce (xs +[f] ys) = Err \<longrightarrow> 
    1.99 -      ~(? zs:list n A. xs <=[r] zs & ys <=[r] zs))"
   1.100 +      ~(\<exists>zs\<in> list n A. xs <=[r] zs & ys <=[r] zs))"
   1.101  apply (induct n)
   1.102   apply simp
   1.103  apply clarify
   1.104 @@ -484,14 +482,14 @@
   1.105  done 
   1.106  
   1.107  lemma closed_err_lift2_conv:
   1.108 -  "closed (err A) (lift2 f) = (!x:A. !y:A. x +_f y : err A)"
   1.109 +  "closed (err A) (lift2 f) = (\<forall>x\<in> A. \<forall>y\<in> A. x +_f y : err A)"
   1.110  apply (unfold closed_def)
   1.111  apply (simp add: err_def)
   1.112  done 
   1.113  
   1.114  lemma closed_map2_list [rule_format]:
   1.115    "closed (err A) (lift2 f) \<Longrightarrow> 
   1.116 -  !xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow> 
   1.117 +  \<forall>xs. xs : list n A \<longrightarrow> (\<forall>ys. ys : list n A \<longrightarrow> 
   1.118    map2 f xs ys : list n (err A))"
   1.119  apply (unfold map2_def)
   1.120  apply (induct n)