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
```