src/HOL/MicroJava/J/JBasis.ML
changeset 10042 7164dc0d24d8
parent 9969 4753185f1dd2
child 10138 412a3ced6efd
     1.1 --- a/src/HOL/MicroJava/J/JBasis.ML	Wed Sep 20 21:20:41 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/J/JBasis.ML	Thu Sep 21 10:42:49 2000 +0200
     1.3 @@ -7,25 +7,25 @@
     1.4  val strip_tac1 = SELECT_GOAL (safe_tac (HOL_cs delrules [conjI, disjE, impCE]));
     1.5  
     1.6  Goalw [image_def]
     1.7 -	"x \\<in> f``A \\<Longrightarrow> \\<exists>y. y \\<in> A \\<and>  x = f y";
     1.8 +	"x \\<in> f``A ==> \\<exists>y. y \\<in> A \\<and>  x = f y";
     1.9  by(Auto_tac);
    1.10  qed "image_rev";
    1.11  
    1.12  fun case_tac1 s i = EVERY [case_tac s i, rotate_tac ~1 i, rotate_tac ~1 (i+1)];
    1.13  
    1.14  val select_split = prove_goalw Prod.thy [split_def] 
    1.15 -	"(\\<epsilon>(x,y). P x y) = (\\<epsilon>xy. P (fst xy) (snd xy))" (K [rtac refl 1]);
    1.16 +	"(SOME (x,y). P x y) = (SOME xy. P (fst xy) (snd xy))" (K [rtac refl 1]);
    1.17  	 
    1.18  
    1.19  val split_beta = prove_goal Prod.thy "(\\<lambda>(x,y). P x y) z = P (fst z) (snd z)"
    1.20  	(fn _ => [stac surjective_pairing 1, stac split 1, rtac refl 1]);
    1.21  val split_beta2 = prove_goal Prod.thy "(\\<lambda>(x,y). P x y) (w,z) = P w z"
    1.22  	(fn _ => [Auto_tac]);
    1.23 -val splitE2 = prove_goal Prod.thy "\\<lbrakk>Q (split P z); \\<And>x y. \\<lbrakk>z = (x, y); Q (P x y)\\<rbrakk> \\<Longrightarrow> R\\<rbrakk> \\<Longrightarrow> R" (fn prems => [
    1.24 +val splitE2 = prove_goal Prod.thy "[|Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R|] ==> R" (fn prems => [
    1.25  	REPEAT (resolve_tac (prems@[surjective_pairing]) 1),
    1.26  	rtac (split_beta RS subst) 1,
    1.27  	rtac (hd prems) 1]);
    1.28 -val splitE2' = prove_goal Prod.thy "\\<lbrakk>((\\<lambda>(x,y). P x y) z) w; \\<And>x y. \\<lbrakk>z = (x, y); (P x y) w\\<rbrakk> \\<Longrightarrow> R\\<rbrakk> \\<Longrightarrow> R" (fn prems => [
    1.29 +val splitE2' = prove_goal Prod.thy "[|((\\<lambda>(x,y). P x y) z) w; !!x y. [|z = (x, y); (P x y) w|] ==> R|] ==> R" (fn prems => [
    1.30  	REPEAT (resolve_tac (prems@[surjective_pairing]) 1),
    1.31  	res_inst_tac [("P1","P")] (split_beta RS subst) 1,
    1.32  	rtac (hd prems) 1]);
    1.33 @@ -33,7 +33,7 @@
    1.34  
    1.35  fun pair_tac s = res_inst_tac [("p",s)] PairE THEN' hyp_subst_tac;
    1.36  
    1.37 -val BallE = prove_goal thy "\\<lbrakk>Ball A P; x \\<notin> A \\<Longrightarrow> Q; P x \\<Longrightarrow> Q \\<rbrakk> \\<Longrightarrow> Q"
    1.38 +val BallE = prove_goal thy "[|Ball A P; x \\<notin> A ==> Q; P x ==> Q |] ==> Q"
    1.39  	(fn prems => [rtac ballE 1, resolve_tac prems 1, 
    1.40  			eresolve_tac prems 1, eresolve_tac prems 1]);
    1.41  
    1.42 @@ -43,7 +43,7 @@
    1.43  
    1.44  (* To HOL.ML *)
    1.45  
    1.46 -val ex1_some_eq_trivial = prove_goal HOL.thy "\\<lbrakk> \\<exists>!x. P x; P y \\<rbrakk> \\<Longrightarrow> Eps P = y" 
    1.47 +val ex1_some_eq_trivial = prove_goal HOL.thy "[| \\<exists>!x. P x; P y |] ==> Eps P = y" 
    1.48  	(fn prems => [
    1.49  	cut_facts_tac prems 1,
    1.50  	rtac some_equality 1,
    1.51 @@ -74,7 +74,7 @@
    1.52    asm_full_simp_tac (simpset() delsimps [split_paired_All,split_paired_Ex])];
    1.53  
    1.54  val optionE = prove_goal thy 
    1.55 -       "\\<lbrakk> opt = None \\<Longrightarrow> P;  \\<And>x. opt = Some x \\<Longrightarrow> P \\<rbrakk> \\<Longrightarrow> P" 
    1.56 +       "[| opt = None ==> P;  !!x. opt = Some x ==> P |] ==> P" 
    1.57     (fn prems => [
    1.58  	case_tac "opt = None" 1,
    1.59  	 eresolve_tac prems 1,
    1.60 @@ -87,7 +87,7 @@
    1.61  	 rotate_tac ~1  i   , asm_full_simp_tac HOL_basic_ss i];
    1.62  
    1.63  val option_map_SomeD = prove_goalw thy [option_map_def]
    1.64 -	"\\<And>x. option_map f x = Some y \\<Longrightarrow> \\<exists>z. x = Some z \\<and> f z = y" (K [
    1.65 +	"!!x. option_map f x = Some y ==> \\<exists>z. x = Some z \\<and> f z = y" (K [
    1.66  	option_case_tac2 "x" 1,
    1.67  	 Auto_tac]);
    1.68  
    1.69 @@ -120,19 +120,19 @@
    1.70  by  (auto_tac (claset() addDs [fst_in_set_lemma],simpset()addsimps[inj_eq]));
    1.71  qed_spec_mp "unique_map_inj";
    1.72  
    1.73 -Goal "\\<And>l. unique l \\<Longrightarrow> unique (map (split (\\<lambda>k. Pair (k, C))) l)";
    1.74 +Goal "!!l. unique l ==> unique (map (split (\\<lambda>k. Pair (k, C))) l)";
    1.75  by(etac unique_map_inj 1);
    1.76  by(rtac injI 1);
    1.77  by Auto_tac;
    1.78  qed "unique_map_Pair";
    1.79  
    1.80 -Goal "\\<lbrakk>M = N; \\<And>x. x\\<in>N \\<Longrightarrow> f x = g x\\<rbrakk> \\<Longrightarrow> f``M = g``N";
    1.81 +Goal "[|M = N; !!x. x\\<in>N ==> f x = g x|] ==> f``M = g``N";
    1.82  by(rtac set_ext 1);
    1.83  by(simp_tac (simpset() addsimps image_def::premises()) 1);
    1.84  qed "image_cong";
    1.85  
    1.86  val split_Pair_eq = prove_goal Prod.thy 
    1.87 -"\\<And>X. ((x, y), z) \\<in> split (\\<lambda>x. Pair (x, Y)) `` A \\<Longrightarrow> y = Y" (K [
    1.88 +"!!X. ((x, y), z) \\<in> split (\\<lambda>x. Pair (x, Y)) `` A ==> y = Y" (K [
    1.89  	etac imageE 1,
    1.90  	split_all_tac 1,
    1.91  	auto_tac(claset_of Prod.thy,simpset_of Prod.thy)]);
    1.92 @@ -140,7 +140,7 @@
    1.93  
    1.94  (* More about Maps *)
    1.95  
    1.96 -val override_SomeD = prove_goalw thy [override_def] "(s \\<oplus> t) k = Some x \\<Longrightarrow> \
    1.97 +val override_SomeD = prove_goalw thy [override_def] "(s \\<oplus> t) k = Some x ==> \
    1.98  \ t k = Some x |  t k = None \\<and>  s k = Some x" (fn prems => [
    1.99  	cut_facts_tac prems 1,
   1.100  	case_tac "\\<exists>x. t k = Some x" 1,
   1.101 @@ -153,7 +153,7 @@
   1.102  
   1.103  Addsimps [fun_upd_same, fun_upd_other];
   1.104  
   1.105 -Goal "unique xys \\<longrightarrow> (map_of xys x = Some y) = ((x,y) \\<in> set xys)";
   1.106 +Goal "unique xys --> (map_of xys x = Some y) = ((x,y) \\<in> set xys)";
   1.107  by(induct_tac "xys" 1);
   1.108   by(Simp_tac 1);
   1.109  by(force_tac (claset(), simpset() addsimps [unique_Cons]) 1);
   1.110 @@ -162,7 +162,7 @@
   1.111  val in_set_get = unique_map_of_Some_conv RS iffD2;
   1.112  val get_in_set = unique_map_of_Some_conv RS iffD1;
   1.113  
   1.114 -Goal "(\\<forall>(x,y)\\<in>set l. P x y) \\<longrightarrow> (\\<forall>x. \\<forall>y. map_of l x = Some y \\<longrightarrow> P x y)";
   1.115 +Goal "(\\<forall>(x,y)\\<in>set l. P x y) --> (\\<forall>x. \\<forall>y. map_of l x = Some y --> P x y)";
   1.116  by(induct_tac "l" 1);
   1.117  by(ALLGOALS Simp_tac);
   1.118  by Safe_tac;
   1.119 @@ -170,37 +170,37 @@
   1.120  bind_thm("Ball_set_table",result() RS mp);
   1.121  
   1.122  val table_mono = prove_goal thy 
   1.123 -"unique l' \\<longrightarrow> (\\<forall>xy. (xy)\\<in>set l \\<longrightarrow> (xy)\\<in>set l') \\<longrightarrow>\
   1.124 -\ (\\<forall>k y. map_of l k = Some y \\<longrightarrow> map_of l' k = Some y)" (fn _ => [
   1.125 +"unique l' --> (\\<forall>xy. (xy)\\<in>set l --> (xy)\\<in>set l') -->\
   1.126 +\ (\\<forall>k y. map_of l k = Some y --> map_of l' k = Some y)" (fn _ => [
   1.127  	induct_tac "l" 1,
   1.128  	 Auto_tac,
   1.129   	 fast_tac (HOL_cs addSIs [in_set_get]) 1])
   1.130   RS mp RS mp RS spec RS spec RS mp;
   1.131  
   1.132 -val table_map_Some' = prove_goal thy "map_of t k = Some (k', x) \\<longrightarrow> \
   1.133 +val table_map_Some' = prove_goal thy "map_of t k = Some (k', x) --> \
   1.134  \ map_of (map (\\<lambda>u. ((fst u, fst (snd u)), snd (snd u))) t) (k, k') = Some x" (K [
   1.135  	induct_tac "t" 1,	
   1.136  	 ALLGOALS Simp_tac,
   1.137  	case_tac1 "k = fst a" 1,
   1.138  	 Auto_tac]) RS mp;
   1.139  val table_map_Some = prove_goal thy 
   1.140 -"map_of (map (\\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) \\<longrightarrow> \
   1.141 +"map_of (map (\\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) --> \
   1.142  \map_of t (k, k') = Some x" (K [
   1.143  	induct_tac "t" 1,	
   1.144  	Auto_tac]) RS mp;
   1.145  
   1.146  
   1.147 -val table_mapf_Some = prove_goal thy "\\<And>f. \\<forall>x y. f x = f y \\<longrightarrow> x = y \\<Longrightarrow> \
   1.148 -\ map_of (map (\\<lambda>(k,x). (k,f x)) t) k = Some (f x) \\<longrightarrow> map_of t k = Some x" (K [
   1.149 +val table_mapf_Some = prove_goal thy "!!f. \\<forall>x y. f x = f y --> x = y ==> \
   1.150 +\ map_of (map (\\<lambda>(k,x). (k,f x)) t) k = Some (f x) --> map_of t k = Some x" (K [
   1.151  	induct_tac "t" 1,	
   1.152  	Auto_tac]) RS mp;
   1.153  val table_mapf_SomeD = prove_goal thy 
   1.154 -"map_of (map (\\<lambda>(k,x). (k, f x)) t) k = Some z \\<longrightarrow> (\\<exists>y. (k,y)\\<in>set t \\<and>  z = f y)"(K [
   1.155 +"map_of (map (\\<lambda>(k,x). (k, f x)) t) k = Some z --> (\\<exists>y. (k,y)\\<in>set t \\<and>  z = f y)"(K [
   1.156  	induct_tac "t" 1,	
   1.157  	Auto_tac]) RS mp;
   1.158  
   1.159  val table_mapf_Some2 = prove_goal thy 
   1.160 -"\\<And>k. map_of (map (\\<lambda>(k,x). (k,C,x)) t) k = Some (D,x) \\<Longrightarrow> C = D \\<and> map_of t k = Some x" (K [
   1.161 +"!!k. map_of (map (\\<lambda>(k,x). (k,C,x)) t) k = Some (D,x) ==> C = D \\<and> map_of t k = Some x" (K [
   1.162  	forward_tac [table_mapf_SomeD] 1,
   1.163  	Auto_tac,
   1.164  	rtac table_mapf_Some 1,