src/HOL/MicroJava/DFA/Listn.thy
changeset 67613 ce654b0e6d69
parent 67399 eab6ce8368fa
child 68646 7dc9fe795dae
     1.1 --- a/src/HOL/MicroJava/DFA/Listn.thy	Tue Feb 13 14:24:50 2018 +0100
     1.2 +++ b/src/HOL/MicroJava/DFA/Listn.thy	Thu Feb 15 12:11:00 2018 +0100
     1.3 @@ -94,7 +94,7 @@
     1.4  done
     1.5  
     1.6  lemma le_list_refl:
     1.7 -  "!x. x <=_r x \<Longrightarrow> xs <=[r] xs"
     1.8 +  "\<forall>x. x <=_r x \<Longrightarrow> xs <=[r] xs"
     1.9  apply (unfold unfold_lesub_list)
    1.10  apply (simp add: Listn.le_def list_all2_conv_all_nth)
    1.11  done
    1.12 @@ -154,23 +154,23 @@
    1.13    done
    1.14  
    1.15  lemma listI:
    1.16 -  "\<lbrakk> length xs = n; set xs <= A \<rbrakk> \<Longrightarrow> xs : list n A"
    1.17 +  "\<lbrakk> length xs = n; set xs <= A \<rbrakk> \<Longrightarrow> xs \<in> list n A"
    1.18  apply (unfold list_def)
    1.19  apply blast
    1.20  done
    1.21  
    1.22  lemma listE_length [simp]:
    1.23 -   "xs : list n A \<Longrightarrow> length xs = n"
    1.24 +   "xs \<in> list n A \<Longrightarrow> length xs = n"
    1.25  apply (unfold list_def)
    1.26  apply blast
    1.27  done 
    1.28  
    1.29  lemma less_lengthI:
    1.30 -  "\<lbrakk> xs : list n A; p < n \<rbrakk> \<Longrightarrow> p < length xs"
    1.31 +  "\<lbrakk> xs \<in> list n A; p < n \<rbrakk> \<Longrightarrow> p < length xs"
    1.32    by simp
    1.33  
    1.34  lemma listE_set [simp]:
    1.35 -  "xs : list n A \<Longrightarrow> set xs <= A"
    1.36 +  "xs \<in> list n A \<Longrightarrow> set xs <= A"
    1.37  apply (unfold list_def)
    1.38  apply blast
    1.39  done 
    1.40 @@ -182,19 +182,19 @@
    1.41  done 
    1.42  
    1.43  lemma in_list_Suc_iff: 
    1.44 -  "(xs : list (Suc n) A) = (\<exists>y\<in> A. \<exists>ys\<in> list n A. xs = y#ys)"
    1.45 +  "(xs \<in> list (Suc n) A) = (\<exists>y\<in> A. \<exists>ys\<in> list n A. xs = y#ys)"
    1.46  apply (unfold list_def)
    1.47  apply (case_tac "xs")
    1.48  apply auto
    1.49  done 
    1.50  
    1.51  lemma Cons_in_list_Suc [iff]:
    1.52 -  "(x#xs : list (Suc n) A) = (x\<in> A & xs : list n A)"
    1.53 +  "(x#xs \<in> list (Suc n) A) = (x\<in> A & xs \<in> list n A)"
    1.54  apply (simp add: in_list_Suc_iff)
    1.55  done 
    1.56  
    1.57  lemma list_not_empty:
    1.58 -  "\<exists>a. a\<in> A \<Longrightarrow> \<exists>xs. xs : list n A"
    1.59 +  "\<exists>a. a\<in> A \<Longrightarrow> \<exists>xs. xs \<in> list n A"
    1.60  apply (induct "n")
    1.61   apply simp
    1.62  apply (simp add: in_list_Suc_iff)
    1.63 @@ -203,14 +203,14 @@
    1.64  
    1.65  
    1.66  lemma nth_in [rule_format, simp]:
    1.67 -  "!i n. length xs = n \<longrightarrow> set xs <= A \<longrightarrow> i < n \<longrightarrow> (xs!i) : A"
    1.68 +  "\<forall>i n. length xs = n \<longrightarrow> set xs <= A \<longrightarrow> i < n \<longrightarrow> (xs!i) \<in> A"
    1.69  apply (induct "xs")
    1.70   apply simp
    1.71  apply (simp add: nth_Cons split: nat.split)
    1.72  done
    1.73  
    1.74  lemma listE_nth_in:
    1.75 -  "\<lbrakk> xs : list n A; i < n \<rbrakk> \<Longrightarrow> (xs!i) : A"
    1.76 +  "\<lbrakk> xs \<in> list n A; i < n \<rbrakk> \<Longrightarrow> (xs!i) \<in> A"
    1.77    by auto
    1.78  
    1.79  
    1.80 @@ -245,7 +245,7 @@
    1.81  
    1.82  
    1.83  lemma listt_update_in_list [simp, intro!]:
    1.84 -  "\<lbrakk> xs : list n A; x\<in> A \<rbrakk> \<Longrightarrow> xs[i := x] : list n A"
    1.85 +  "\<lbrakk> xs \<in> list n A; x\<in> A \<rbrakk> \<Longrightarrow> xs[i := x] \<in> list n A"
    1.86  apply (unfold list_def)
    1.87  apply simp
    1.88  done 
    1.89 @@ -261,7 +261,7 @@
    1.90    by (simp add: plussub_def map2_def split: list.split)
    1.91  
    1.92  lemma length_plus_list [rule_format, simp]:
    1.93 -  "!ys. length(xs +[f] ys) = min(length xs) (length ys)"
    1.94 +  "\<forall>ys. length(xs +[f] ys) = min(length xs) (length ys)"
    1.95  apply (induct xs)
    1.96   apply simp
    1.97  apply clarify
    1.98 @@ -269,7 +269,7 @@
    1.99  done
   1.100  
   1.101  lemma nth_plus_list [rule_format, simp]:
   1.102 -  "!xs ys i. length xs = n \<longrightarrow> length ys = n \<longrightarrow> i<n \<longrightarrow> 
   1.103 +  "\<forall>xs ys i. length xs = n \<longrightarrow> length ys = n \<longrightarrow> i<n \<longrightarrow> 
   1.104    (xs +[f] ys)!i = (xs!i) +_f (ys!i)"
   1.105  apply (induct n)
   1.106   apply simp
   1.107 @@ -295,7 +295,7 @@
   1.108  done
   1.109  
   1.110  lemma (in Semilat) plus_list_lub [rule_format]:
   1.111 -shows "!xs ys zs. set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> set zs <= A 
   1.112 +shows "\<forall>xs ys zs. set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> set zs <= A 
   1.113    \<longrightarrow> size xs = n & size ys = n \<longrightarrow> 
   1.114    xs <=[r] zs & ys <=[r] zs \<longrightarrow> xs +[f] ys <=[r] zs"
   1.115  apply (unfold unfold_lesub_list)
   1.116 @@ -304,7 +304,7 @@
   1.117  
   1.118  lemma (in Semilat) list_update_incr [rule_format]:
   1.119   "x\<in> A \<Longrightarrow> set xs <= A \<longrightarrow> 
   1.120 -  (!i. i<size xs \<longrightarrow> xs <=[r] xs[i := x +_f xs!i])"
   1.121 +  (\<forall>i. i<size xs \<longrightarrow> xs <=[r] xs[i := x +_f xs!i])"
   1.122  apply (unfold unfold_lesub_list)
   1.123  apply (simp add: Listn.le_def list_all2_conv_all_nth)
   1.124  apply (induct xs)
   1.125 @@ -342,7 +342,7 @@
   1.126   apply (erule thin_rl)
   1.127   apply (erule thin_rl)
   1.128   apply blast
   1.129 -apply (erule_tac x = "{a. \<exists>xs. size xs = k \<and> a#xs:M}" in allE)
   1.130 +apply (erule_tac x = "{a. \<exists>xs. size xs = k \<and> a#xs \<in> M}" in allE)
   1.131  apply (erule impE)
   1.132   apply blast
   1.133  apply (thin_tac "\<exists>x xs. P x xs" for P)
   1.134 @@ -394,7 +394,7 @@
   1.135   by(simp add: Listn_sl_aux split_tupled_all)
   1.136  
   1.137  lemma coalesce_in_err_list [rule_format]:
   1.138 -  "!xes. xes : list n (err A) \<longrightarrow> coalesce xes : err(list n A)"
   1.139 +  "\<forall>xes. xes \<in> list n (err A) \<longrightarrow> coalesce xes \<in> err(list n A)"
   1.140  apply (induct n)
   1.141   apply simp
   1.142  apply clarify
   1.143 @@ -409,8 +409,8 @@
   1.144  
   1.145  lemma coalesce_eq_OK1_D [rule_format]:
   1.146    "semilat(err A, Err.le r, lift2 f) \<Longrightarrow> 
   1.147 -  !xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow> 
   1.148 -  (!zs. coalesce (xs +[f] ys) = OK zs \<longrightarrow> xs <=[r] zs))"
   1.149 +  \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> 
   1.150 +  (\<forall>zs. coalesce (xs +[f] ys) = OK zs \<longrightarrow> xs <=[r] zs))"
   1.151  apply (induct n)
   1.152    apply simp
   1.153  apply clarify
   1.154 @@ -422,8 +422,8 @@
   1.155  
   1.156  lemma coalesce_eq_OK2_D [rule_format]:
   1.157    "semilat(err A, Err.le r, lift2 f) \<Longrightarrow> 
   1.158 -  !xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow> 
   1.159 -  (!zs. coalesce (xs +[f] ys) = OK zs \<longrightarrow> ys <=[r] zs))"
   1.160 +  \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> 
   1.161 +  (\<forall>zs. coalesce (xs +[f] ys) = OK zs \<longrightarrow> ys <=[r] zs))"
   1.162  apply (induct n)
   1.163   apply simp
   1.164  apply clarify
   1.165 @@ -447,9 +447,9 @@
   1.166  
   1.167  lemma coalesce_eq_OK_ub_D [rule_format]:
   1.168    "semilat(err A, Err.le r, lift2 f) \<Longrightarrow> 
   1.169 -  !xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow> 
   1.170 -  (!zs us. coalesce (xs +[f] ys) = OK zs & xs <=[r] us & ys <=[r] us 
   1.171 -           & us : list n A \<longrightarrow> zs <=[r] us))"
   1.172 +  \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> 
   1.173 +  (\<forall>zs us. coalesce (xs +[f] ys) = OK zs \<and> xs <=[r] us \<and> ys <=[r] us 
   1.174 +           \<and> us \<in> list n A \<longrightarrow> zs <=[r] us))"
   1.175  apply (induct n)
   1.176   apply simp
   1.177  apply clarify
   1.178 @@ -470,9 +470,9 @@
   1.179  
   1.180  lemma coalesce_eq_Err_D [rule_format]:
   1.181    "\<lbrakk> semilat(err A, Err.le r, lift2 f) \<rbrakk> 
   1.182 -  \<Longrightarrow> !xs. xs\<in> list n A \<longrightarrow> (!ys. ys\<in> list n A \<longrightarrow> 
   1.183 +  \<Longrightarrow> \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> 
   1.184        coalesce (xs +[f] ys) = Err \<longrightarrow> 
   1.185 -      ~(\<exists>zs\<in> list n A. xs <=[r] zs & ys <=[r] zs))"
   1.186 +      \<not>(\<exists>zs\<in> list n A. xs <=[r] zs \<and> ys <=[r] zs))"
   1.187  apply (induct n)
   1.188   apply simp
   1.189  apply clarify
   1.190 @@ -483,15 +483,15 @@
   1.191  done 
   1.192  
   1.193  lemma closed_err_lift2_conv:
   1.194 -  "closed (err A) (lift2 f) = (\<forall>x\<in> A. \<forall>y\<in> A. x +_f y : err A)"
   1.195 +  "closed (err A) (lift2 f) = (\<forall>x\<in> A. \<forall>y\<in> A. x +_f y \<in> err A)"
   1.196  apply (unfold closed_def)
   1.197  apply (simp add: err_def)
   1.198  done 
   1.199  
   1.200  lemma closed_map2_list [rule_format]:
   1.201    "closed (err A) (lift2 f) \<Longrightarrow> 
   1.202 -  \<forall>xs. xs : list n A \<longrightarrow> (\<forall>ys. ys : list n A \<longrightarrow> 
   1.203 -  map2 f xs ys : list n (err A))"
   1.204 +  \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> 
   1.205 +  map2 f xs ys \<in> list n (err A))"
   1.206  apply (unfold map2_def)
   1.207  apply (induct n)
   1.208   apply simp