src/HOL/MicroJava/BV/Listn.thy
changeset 13006 51c5f3f11d16
parent 12911 704713ca07ea
child 13066 b57d926d1de2
     1.1 --- a/src/HOL/MicroJava/BV/Listn.thy	Sat Mar 02 12:09:23 2002 +0100
     1.2 +++ b/src/HOL/MicroJava/BV/Listn.thy	Sun Mar 03 16:59:08 2002 +0100
     1.3 @@ -12,41 +12,41 @@
     1.4  
     1.5  constdefs
     1.6  
     1.7 - list :: "nat => 'a set => 'a list set"
     1.8 + list :: "nat \<Rightarrow> 'a set \<Rightarrow> 'a list set"
     1.9  "list n A == {xs. length xs = n & set xs <= A}"
    1.10  
    1.11 - le :: "'a ord => ('a list)ord"
    1.12 + le :: "'a ord \<Rightarrow> ('a list)ord"
    1.13  "le r == list_all2 (%x y. x <=_r y)"
    1.14  
    1.15 -syntax "@lesublist" :: "'a list => 'a ord => 'a list => bool"
    1.16 +syntax "@lesublist" :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool"
    1.17         ("(_ /<=[_] _)" [50, 0, 51] 50)
    1.18 -syntax "@lesssublist" :: "'a list => 'a ord => 'a list => bool"
    1.19 +syntax "@lesssublist" :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool"
    1.20         ("(_ /<[_] _)" [50, 0, 51] 50)
    1.21  translations
    1.22   "x <=[r] y" == "x <=_(Listn.le r) y"
    1.23   "x <[r] y"  == "x <_(Listn.le r) y"
    1.24  
    1.25  constdefs
    1.26 - map2 :: "('a => 'b => 'c) => 'a list => 'b list => 'c list"
    1.27 + map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
    1.28  "map2 f == (%xs ys. map (split f) (zip xs ys))"
    1.29  
    1.30 -syntax "@plussublist" :: "'a list => ('a => 'b => 'c) => 'b list => 'c list"
    1.31 +syntax "@plussublist" :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b list \<Rightarrow> 'c list"
    1.32         ("(_ /+[_] _)" [65, 0, 66] 65)
    1.33  translations  "x +[f] y" == "x +_(map2 f) y"
    1.34  
    1.35 -consts coalesce :: "'a err list => 'a list err"
    1.36 +consts coalesce :: "'a err list \<Rightarrow> 'a list err"
    1.37  primrec
    1.38  "coalesce [] = OK[]"
    1.39  "coalesce (ex#exs) = Err.sup (op #) ex (coalesce exs)"
    1.40  
    1.41  constdefs
    1.42 - sl :: "nat => 'a sl => 'a list sl"
    1.43 + sl :: "nat \<Rightarrow> 'a sl \<Rightarrow> 'a list sl"
    1.44  "sl n == %(A,r,f). (list n A, le r, map2 f)"
    1.45  
    1.46 - sup :: "('a => 'b => 'c err) => 'a list => 'b list => 'c list err"
    1.47 + sup :: "('a \<Rightarrow> 'b \<Rightarrow> 'c err) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list err"
    1.48  "sup f == %xs ys. if size xs = size ys then coalesce(xs +[f] ys) else Err"
    1.49  
    1.50 - upto_esl :: "nat => 'a esl => 'a list esl"
    1.51 + upto_esl :: "nat \<Rightarrow> 'a esl \<Rightarrow> 'a list esl"
    1.52  "upto_esl m == %(A,r,f). (Union{list n A |n. n <= m}, le r, sup f)"
    1.53  
    1.54  lemmas [simp] = set_update_subsetI
    1.55 @@ -75,7 +75,7 @@
    1.56  done
    1.57  
    1.58  lemma Cons_less_Conss [simp]:
    1.59 -  "order r ==> 
    1.60 +  "order r \<Longrightarrow> 
    1.61    x#xs <_(Listn.le r) y#ys = 
    1.62    (x <_r y & xs <=[r] ys  |  x = y & xs <_(Listn.le r) ys)"
    1.63  apply (unfold lesssub_def)
    1.64 @@ -83,7 +83,7 @@
    1.65  done  
    1.66  
    1.67  lemma list_update_le_cong:
    1.68 -  "[| i<size xs; xs <=[r] ys; x <=_r y |] ==> xs[i:=x] <=[r] ys[i:=y]";
    1.69 +  "\<lbrakk> i<size xs; xs <=[r] ys; x <=_r y \<rbrakk> \<Longrightarrow> xs[i:=x] <=[r] ys[i:=y]";
    1.70  apply (unfold unfold_lesub_list)
    1.71  apply (unfold Listn.le_def)
    1.72  apply (simp add: list_all2_conv_all_nth nth_list_update)
    1.73 @@ -91,19 +91,19 @@
    1.74  
    1.75  
    1.76  lemma le_listD:
    1.77 -  "[| xs <=[r] ys; p < size xs |] ==> xs!p <=_r ys!p"
    1.78 +  "\<lbrakk> xs <=[r] ys; p < size xs \<rbrakk> \<Longrightarrow> xs!p <=_r ys!p"
    1.79  apply (unfold Listn.le_def lesub_def)
    1.80  apply (simp add: list_all2_conv_all_nth)
    1.81  done
    1.82  
    1.83  lemma le_list_refl:
    1.84 -  "!x. x <=_r x ==> xs <=[r] xs"
    1.85 +  "!x. x <=_r x \<Longrightarrow> xs <=[r] xs"
    1.86  apply (unfold unfold_lesub_list)
    1.87  apply (simp add: Listn.le_def list_all2_conv_all_nth)
    1.88  done
    1.89  
    1.90  lemma le_list_trans:
    1.91 -  "[| order r; xs <=[r] ys; ys <=[r] zs |] ==> xs <=[r] zs"
    1.92 +  "\<lbrakk> order r; xs <=[r] ys; ys <=[r] zs \<rbrakk> \<Longrightarrow> xs <=[r] zs"
    1.93  apply (unfold unfold_lesub_list)
    1.94  apply (simp add: Listn.le_def list_all2_conv_all_nth)
    1.95  apply clarify
    1.96 @@ -112,7 +112,7 @@
    1.97  done
    1.98  
    1.99  lemma le_list_antisym:
   1.100 -  "[| order r; xs <=[r] ys; ys <=[r] xs |] ==> xs = ys"
   1.101 +  "\<lbrakk> order r; xs <=[r] ys; ys <=[r] xs \<rbrakk> \<Longrightarrow> xs = ys"
   1.102  apply (unfold unfold_lesub_list)
   1.103  apply (simp add: Listn.le_def list_all2_conv_all_nth)
   1.104  apply (rule nth_equalityI)
   1.105 @@ -123,7 +123,7 @@
   1.106  done
   1.107  
   1.108  lemma order_listI [simp, intro!]:
   1.109 -  "order r ==> order(Listn.le r)"
   1.110 +  "order r \<Longrightarrow> order(Listn.le r)"
   1.111  apply (subst order_def)
   1.112  apply (blast intro: le_list_refl le_list_trans le_list_antisym
   1.113               dest: order_refl)
   1.114 @@ -131,35 +131,35 @@
   1.115  
   1.116  
   1.117  lemma lesub_list_impl_same_size [simp]:
   1.118 -  "xs <=[r] ys ==> size ys = size xs"  
   1.119 +  "xs <=[r] ys \<Longrightarrow> size ys = size xs"  
   1.120  apply (unfold Listn.le_def lesub_def)
   1.121  apply (simp add: list_all2_conv_all_nth)
   1.122  done 
   1.123  
   1.124  lemma lesssub_list_impl_same_size:
   1.125 -  "xs <_(Listn.le r) ys ==> size ys = size xs"
   1.126 +  "xs <_(Listn.le r) ys \<Longrightarrow> size ys = size xs"
   1.127  apply (unfold lesssub_def)
   1.128  apply auto
   1.129  done  
   1.130  
   1.131  lemma listI:
   1.132 -  "[| length xs = n; set xs <= A |] ==> xs : list n A"
   1.133 +  "\<lbrakk> length xs = n; set xs <= A \<rbrakk> \<Longrightarrow> xs : list n A"
   1.134  apply (unfold list_def)
   1.135  apply blast
   1.136  done
   1.137  
   1.138  lemma listE_length [simp]:
   1.139 -   "xs : list n A ==> length xs = n"
   1.140 +   "xs : list n A \<Longrightarrow> length xs = n"
   1.141  apply (unfold list_def)
   1.142  apply blast
   1.143  done 
   1.144  
   1.145  lemma less_lengthI:
   1.146 -  "[| xs : list n A; p < n |] ==> p < length xs"
   1.147 +  "\<lbrakk> xs : list n A; p < n \<rbrakk> \<Longrightarrow> p < length xs"
   1.148    by simp
   1.149  
   1.150  lemma listE_set [simp]:
   1.151 -  "xs : list n A ==> set xs <= A"
   1.152 +  "xs : list n A \<Longrightarrow> set xs <= A"
   1.153  apply (unfold list_def)
   1.154  apply blast
   1.155  done 
   1.156 @@ -183,7 +183,7 @@
   1.157  done 
   1.158  
   1.159  lemma list_not_empty:
   1.160 -  "? a. a:A ==> ? xs. xs : list n A";
   1.161 +  "? a. a:A \<Longrightarrow> ? xs. xs : list n A";
   1.162  apply (induct "n")
   1.163   apply simp
   1.164  apply (simp add: in_list_Suc_iff)
   1.165 @@ -192,18 +192,18 @@
   1.166  
   1.167  
   1.168  lemma nth_in [rule_format, simp]:
   1.169 -  "!i n. length xs = n --> set xs <= A --> i < n --> (xs!i) : A"
   1.170 +  "!i n. length xs = n \<longrightarrow> set xs <= A \<longrightarrow> i < n \<longrightarrow> (xs!i) : A"
   1.171  apply (induct "xs")
   1.172   apply simp
   1.173  apply (simp add: nth_Cons split: nat.split)
   1.174  done
   1.175  
   1.176  lemma listE_nth_in:
   1.177 -  "[| xs : list n A; i < n |] ==> (xs!i) : A"
   1.178 +  "\<lbrakk> xs : list n A; i < n \<rbrakk> \<Longrightarrow> (xs!i) : A"
   1.179    by auto
   1.180  
   1.181  lemma listt_update_in_list [simp, intro!]:
   1.182 -  "[| xs : list n A; x:A |] ==> xs[i := x] : list n A"
   1.183 +  "\<lbrakk> xs : list n A; x:A \<rbrakk> \<Longrightarrow> xs[i := x] : list n A"
   1.184  apply (unfold list_def)
   1.185  apply simp
   1.186  done 
   1.187 @@ -215,7 +215,7 @@
   1.188  done 
   1.189  
   1.190  lemma plus_list_Cons [simp]:
   1.191 -  "(x#xs) +[f] ys = (case ys of [] => [] | y#ys => (x +_f y)#(xs +[f] ys))"
   1.192 +  "(x#xs) +[f] ys = (case ys of [] \<Rightarrow> [] | y#ys \<Rightarrow> (x +_f y)#(xs +[f] ys))"
   1.193    by (simp add: plussub_def map2_def split: list.split)
   1.194  
   1.195  lemma length_plus_list [rule_format, simp]:
   1.196 @@ -227,7 +227,7 @@
   1.197  done
   1.198  
   1.199  lemma nth_plus_list [rule_format, simp]:
   1.200 -  "!xs ys i. length xs = n --> length ys = n --> i<n --> 
   1.201 +  "!xs ys i. length xs = n \<longrightarrow> length ys = n \<longrightarrow> i<n \<longrightarrow> 
   1.202    (xs +[f] ys)!i = (xs!i) +_f (ys!i)"
   1.203  apply (induct n)
   1.204   apply simp
   1.205 @@ -239,30 +239,30 @@
   1.206  
   1.207  
   1.208  lemma plus_list_ub1 [rule_format]:
   1.209 -  "[| semilat(A,r,f); set xs <= A; set ys <= A; size xs = size ys |] 
   1.210 -  ==> xs <=[r] xs +[f] ys"
   1.211 +  "\<lbrakk> semilat(A,r,f); set xs <= A; set ys <= A; size xs = size ys \<rbrakk> 
   1.212 +  \<Longrightarrow> xs <=[r] xs +[f] ys"
   1.213  apply (unfold unfold_lesub_list)
   1.214  apply (simp add: Listn.le_def list_all2_conv_all_nth)
   1.215  done
   1.216  
   1.217  lemma plus_list_ub2:
   1.218 -  "[| semilat(A,r,f); set xs <= A; set ys <= A; size xs = size ys |]
   1.219 -  ==> ys <=[r] xs +[f] ys"
   1.220 +  "\<lbrakk> semilat(A,r,f); set xs <= A; set ys <= A; size xs = size ys \<rbrakk>
   1.221 +  \<Longrightarrow> ys <=[r] xs +[f] ys"
   1.222  apply (unfold unfold_lesub_list)
   1.223  apply (simp add: Listn.le_def list_all2_conv_all_nth)
   1.224  done 
   1.225  
   1.226  lemma plus_list_lub [rule_format]:
   1.227 -  "semilat(A,r,f) ==> !xs ys zs. set xs <= A --> set ys <= A --> set zs <= A 
   1.228 -  --> size xs = n & size ys = n --> 
   1.229 -  xs <=[r] zs & ys <=[r] zs --> xs +[f] ys <=[r] zs"
   1.230 +  "semilat(A,r,f) \<Longrightarrow> !xs ys zs. set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> set zs <= A 
   1.231 +  \<longrightarrow> size xs = n & size ys = n \<longrightarrow> 
   1.232 +  xs <=[r] zs & ys <=[r] zs \<longrightarrow> xs +[f] ys <=[r] zs"
   1.233  apply (unfold unfold_lesub_list)
   1.234  apply (simp add: Listn.le_def list_all2_conv_all_nth)
   1.235  done 
   1.236  
   1.237  lemma list_update_incr [rule_format]:
   1.238 -  "[| semilat(A,r,f); x:A |] ==> set xs <= A --> 
   1.239 -  (!i. i<size xs --> xs <=[r] xs[i := x +_f xs!i])"
   1.240 +  "\<lbrakk> semilat(A,r,f); x:A \<rbrakk> \<Longrightarrow> set xs <= A \<longrightarrow> 
   1.241 +  (!i. i<size xs \<longrightarrow> xs <=[r] xs[i := x +_f xs!i])"
   1.242  apply (unfold unfold_lesub_list)
   1.243  apply (simp add: Listn.le_def list_all2_conv_all_nth)
   1.244  apply (induct xs)
   1.245 @@ -273,7 +273,7 @@
   1.246  done 
   1.247  
   1.248  lemma acc_le_listI [intro!]:
   1.249 -  "[| order r; acc r |] ==> acc(Listn.le r)"
   1.250 +  "\<lbrakk> order r; acc r \<rbrakk> \<Longrightarrow> acc(Listn.le r)"
   1.251  apply (unfold acc_def)
   1.252  apply (subgoal_tac
   1.253   "wf(UN n. {(ys,xs). size xs = n & size ys = n & xs <_(Listn.le r) ys})")
   1.254 @@ -323,7 +323,7 @@
   1.255  done 
   1.256  
   1.257  lemma closed_listI:
   1.258 -  "closed S f ==> closed (list n S) (map2 f)"
   1.259 +  "closed S f \<Longrightarrow> closed (list n S) (map2 f)"
   1.260  apply (unfold closed_def)
   1.261  apply (induct n)
   1.262   apply simp
   1.263 @@ -335,7 +335,7 @@
   1.264  
   1.265  
   1.266  lemma semilat_Listn_sl:
   1.267 -  "!!L. semilat L ==> semilat (Listn.sl n L)"
   1.268 +  "\<And>L. semilat L \<Longrightarrow> semilat (Listn.sl n L)"
   1.269  apply (unfold Listn.sl_def)
   1.270  apply (simp (no_asm_simp) only: split_tupled_all)
   1.271  apply (simp (no_asm) only: semilat_Def split_conv)
   1.272 @@ -349,7 +349,7 @@
   1.273  
   1.274  
   1.275  lemma coalesce_in_err_list [rule_format]:
   1.276 -  "!xes. xes : list n (err A) --> coalesce xes : err(list n A)"
   1.277 +  "!xes. xes : list n (err A) \<longrightarrow> coalesce xes : err(list n A)"
   1.278  apply (induct n)
   1.279   apply simp
   1.280  apply clarify
   1.281 @@ -359,13 +359,13 @@
   1.282  apply force
   1.283  done 
   1.284  
   1.285 -lemma lem: "!!x xs. x +_(op #) xs = x#xs"
   1.286 +lemma lem: "\<And>x xs. x +_(op #) xs = x#xs"
   1.287    by (simp add: plussub_def)
   1.288  
   1.289  lemma coalesce_eq_OK1_D [rule_format]:
   1.290 -  "semilat(err A, Err.le r, lift2 f) ==> 
   1.291 -  !xs. xs : list n A --> (!ys. ys : list n A --> 
   1.292 -  (!zs. coalesce (xs +[f] ys) = OK zs --> xs <=[r] zs))"
   1.293 +  "semilat(err A, Err.le r, lift2 f) \<Longrightarrow> 
   1.294 +  !xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow> 
   1.295 +  (!zs. coalesce (xs +[f] ys) = OK zs \<longrightarrow> xs <=[r] zs))"
   1.296  apply (induct n)
   1.297    apply simp
   1.298  apply clarify
   1.299 @@ -376,9 +376,9 @@
   1.300  done
   1.301  
   1.302  lemma coalesce_eq_OK2_D [rule_format]:
   1.303 -  "semilat(err A, Err.le r, lift2 f) ==> 
   1.304 -  !xs. xs : list n A --> (!ys. ys : list n A --> 
   1.305 -  (!zs. coalesce (xs +[f] ys) = OK zs --> ys <=[r] zs))"
   1.306 +  "semilat(err A, Err.le r, lift2 f) \<Longrightarrow> 
   1.307 +  !xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow> 
   1.308 +  (!zs. coalesce (xs +[f] ys) = OK zs \<longrightarrow> ys <=[r] zs))"
   1.309  apply (induct n)
   1.310   apply simp
   1.311  apply clarify
   1.312 @@ -389,8 +389,8 @@
   1.313  done 
   1.314  
   1.315  lemma lift2_le_ub:
   1.316 -  "[| semilat(err A, Err.le r, lift2 f); x:A; y:A; x +_f y = OK z; 
   1.317 -      u:A; x <=_r u; y <=_r u |] ==> z <=_r u"
   1.318 +  "\<lbrakk> semilat(err A, Err.le r, lift2 f); x:A; y:A; x +_f y = OK z; 
   1.319 +      u:A; x <=_r u; y <=_r u \<rbrakk> \<Longrightarrow> z <=_r u"
   1.320  apply (unfold semilat_Def plussub_def err_def)
   1.321  apply (simp add: lift2_def)
   1.322  apply clarify
   1.323 @@ -401,10 +401,10 @@
   1.324  done 
   1.325  
   1.326  lemma coalesce_eq_OK_ub_D [rule_format]:
   1.327 -  "semilat(err A, Err.le r, lift2 f) ==> 
   1.328 -  !xs. xs : list n A --> (!ys. ys : list n A --> 
   1.329 +  "semilat(err A, Err.le r, lift2 f) \<Longrightarrow> 
   1.330 +  !xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow> 
   1.331    (!zs us. coalesce (xs +[f] ys) = OK zs & xs <=[r] us & ys <=[r] us 
   1.332 -           & us : list n A --> zs <=[r] us))"
   1.333 +           & us : list n A \<longrightarrow> zs <=[r] us))"
   1.334  apply (induct n)
   1.335   apply simp
   1.336  apply clarify
   1.337 @@ -418,15 +418,15 @@
   1.338  done 
   1.339  
   1.340  lemma lift2_eq_ErrD:
   1.341 -  "[| x +_f y = Err; semilat(err A, Err.le r, lift2 f); x:A; y:A |] 
   1.342 -  ==> ~(? u:A. x <=_r u & y <=_r u)"
   1.343 +  "\<lbrakk> x +_f y = Err; semilat(err A, Err.le r, lift2 f); x:A; y:A \<rbrakk> 
   1.344 +  \<Longrightarrow> ~(? u:A. x <=_r u & y <=_r u)"
   1.345    by (simp add: OK_plus_OK_eq_Err_conv [THEN iffD1])
   1.346  
   1.347  
   1.348  lemma coalesce_eq_Err_D [rule_format]:
   1.349 -  "[| semilat(err A, Err.le r, lift2 f) |] 
   1.350 -  ==> !xs. xs:list n A --> (!ys. ys:list n A --> 
   1.351 -      coalesce (xs +[f] ys) = Err --> 
   1.352 +  "\<lbrakk> semilat(err A, Err.le r, lift2 f) \<rbrakk> 
   1.353 +  \<Longrightarrow> !xs. xs:list n A \<longrightarrow> (!ys. ys:list n A \<longrightarrow> 
   1.354 +      coalesce (xs +[f] ys) = Err \<longrightarrow> 
   1.355        ~(? zs:list n A. xs <=[r] zs & ys <=[r] zs))"
   1.356  apply (induct n)
   1.357   apply simp
   1.358 @@ -445,8 +445,8 @@
   1.359  done 
   1.360  
   1.361  lemma closed_map2_list [rule_format]:
   1.362 -  "closed (err A) (lift2 f) ==> 
   1.363 -  !xs. xs : list n A --> (!ys. ys : list n A --> 
   1.364 +  "closed (err A) (lift2 f) \<Longrightarrow> 
   1.365 +  !xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow> 
   1.366    map2 f xs ys : list n (err A))"
   1.367  apply (unfold map2_def)
   1.368  apply (induct n)
   1.369 @@ -458,14 +458,14 @@
   1.370  done 
   1.371  
   1.372  lemma closed_lift2_sup:
   1.373 -  "closed (err A) (lift2 f) ==> 
   1.374 +  "closed (err A) (lift2 f) \<Longrightarrow> 
   1.375    closed (err (list n A)) (lift2 (sup f))"
   1.376    by (fastsimp  simp add: closed_def plussub_def sup_def lift2_def
   1.377                            coalesce_in_err_list closed_map2_list
   1.378                  split: err.split)
   1.379  
   1.380  lemma err_semilat_sup:
   1.381 -  "err_semilat (A,r,f) ==> 
   1.382 +  "err_semilat (A,r,f) \<Longrightarrow> 
   1.383    err_semilat (list n A, Listn.le r, sup f)"
   1.384  apply (unfold Err.sl_def)
   1.385  apply (simp only: split_conv)
   1.386 @@ -480,7 +480,7 @@
   1.387  done 
   1.388  
   1.389  lemma err_semilat_upto_esl:
   1.390 -  "!!L. err_semilat L ==> err_semilat(upto_esl m L)"
   1.391 +  "\<And>L. err_semilat L \<Longrightarrow> err_semilat(upto_esl m L)"
   1.392  apply (unfold Listn.upto_esl_def)
   1.393  apply (simp (no_asm_simp) only: split_tupled_all)
   1.394  apply simp