src/HOL/MicroJava/J/Conform.ML
changeset 10042 7164dc0d24d8
parent 9758 88366d7332ff
child 10613 78b1d6c3ee9c
     1.1 --- a/src/HOL/MicroJava/J/Conform.ML	Wed Sep 20 21:20:41 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/J/Conform.ML	Thu Sep 21 10:42:49 2000 +0200
     1.3 @@ -6,25 +6,25 @@
     1.4  
     1.5  section "hext";
     1.6  
     1.7 -val hextI = prove_goalw thy [hext_def] "\\<And>h. \
     1.8 -\ \\<forall>a C fs . h  a = Some (C,fs) \\<longrightarrow>  \
     1.9 -\     (\\<exists>fs'. h' a = Some (C,fs')) \\<Longrightarrow> h\\<le>|h'" (K [Auto_tac ]);
    1.10 +val hextI = prove_goalw thy [hext_def] "!!h. \
    1.11 +\ \\<forall>a C fs . h  a = Some (C,fs) -->  \
    1.12 +\     (\\<exists>fs'. h' a = Some (C,fs')) ==> h\\<le>|h'" (K [Auto_tac ]);
    1.13  
    1.14  val hext_objD = prove_goalw thy [hext_def] 
    1.15 -"\\<And>h. \\<lbrakk>h\\<le>|h'; h a = Some (C,fs) \\<rbrakk> \\<Longrightarrow> \\<exists>fs'. h' a = Some (C,fs')" 
    1.16 +"!!h. [|h\\<le>|h'; h a = Some (C,fs) |] ==> \\<exists>fs'. h' a = Some (C,fs')" 
    1.17  	(K [Force_tac 1]);
    1.18  
    1.19  val hext_refl = prove_goal thy "h\\<le>|h" (K [
    1.20  	rtac hextI 1,
    1.21  	Fast_tac 1]);
    1.22  
    1.23 -val hext_new = prove_goal thy "\\<And>h. h a = None \\<Longrightarrow> h\\<le>|h(a\\<mapsto>x)" (K [
    1.24 +val hext_new = prove_goal thy "!!h. h a = None ==> h\\<le>|h(a\\<mapsto>x)" (K [
    1.25  	rtac hextI 1,
    1.26  	safe_tac HOL_cs,
    1.27  	 ALLGOALS (case_tac "aa = a"),
    1.28  	   Auto_tac]);
    1.29  
    1.30 -val hext_trans = prove_goal thy "\\<And>h. \\<lbrakk>h\\<le>|h'; h'\\<le>|h''\\<rbrakk> \\<Longrightarrow> h\\<le>|h''" (K [
    1.31 +val hext_trans = prove_goal thy "!!h. [|h\\<le>|h'; h'\\<le>|h''|] ==> h\\<le>|h''" (K [
    1.32  	rtac hextI 1,
    1.33  	safe_tac HOL_cs,
    1.34  	 fast_tac (HOL_cs addDs [hext_objD]) 1]);
    1.35 @@ -32,7 +32,7 @@
    1.36  Addsimps [hext_refl, hext_new];
    1.37  
    1.38  val hext_upd_obj = prove_goal thy 
    1.39 -"\\<And>h. h a = Some (C,fs) \\<Longrightarrow> h\\<le>|h(a\\<mapsto>(C,fs'))" (K [
    1.40 +"!!h. h a = Some (C,fs) ==> h\\<le>|h(a\\<mapsto>(C,fs'))" (K [
    1.41  	rtac hextI 1,
    1.42  	safe_tac HOL_cs,
    1.43  	 ALLGOALS (case_tac "aa = a"),
    1.44 @@ -42,37 +42,37 @@
    1.45  section "conf";
    1.46  
    1.47  val conf_Null = prove_goalw thy [conf_def] 
    1.48 -"G,h\\<turnstile>Null\\<Colon>\\<preceq>T = G\\<turnstile>RefT NullT\\<preceq>T" (K [Simp_tac 1]);
    1.49 +"G,h\\<turnstile>Null::\\<preceq>T = G\\<turnstile>RefT NullT\\<preceq>T" (K [Simp_tac 1]);
    1.50  Addsimps [conf_Null];
    1.51  
    1.52  val conf_litval = prove_goalw thy [conf_def] 
    1.53 -"typeof (\\<lambda>v. None) v = Some T \\<longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>T" (K [
    1.54 +"typeof (\\<lambda>v. None) v = Some T --> G,h\\<turnstile>v::\\<preceq>T" (K [
    1.55  	rtac val_.induct 1,
    1.56  	    Auto_tac]) RS mp;
    1.57  
    1.58 -Goalw [conf_def] "G,s\\<turnstile>Unit\\<Colon>\\<preceq>PrimT Void";
    1.59 +Goalw [conf_def] "G,s\\<turnstile>Unit::\\<preceq>PrimT Void";
    1.60  by( Simp_tac 1);
    1.61  qed "conf_VoidI";
    1.62  
    1.63 -Goalw [conf_def] "G,s\\<turnstile>Bool b\\<Colon>\\<preceq>PrimT Boolean";
    1.64 +Goalw [conf_def] "G,s\\<turnstile>Bool b::\\<preceq>PrimT Boolean";
    1.65  by( Simp_tac 1);
    1.66  qed "conf_BooleanI";
    1.67  
    1.68 -Goalw [conf_def] "G,s\\<turnstile>Intg i\\<Colon>\\<preceq>PrimT Integer";
    1.69 +Goalw [conf_def] "G,s\\<turnstile>Intg i::\\<preceq>PrimT Integer";
    1.70  by( Simp_tac 1);
    1.71  qed "conf_IntegerI";
    1.72  
    1.73  Addsimps [conf_VoidI, conf_BooleanI, conf_IntegerI];
    1.74  
    1.75  val conf_AddrI = prove_goalw thy [conf_def] 
    1.76 -"\\<And>G. \\<lbrakk>h a = Some obj; G\\<turnstile>obj_ty obj\\<preceq>T\\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>Addr a\\<Colon>\\<preceq>T"
    1.77 +"!!G. [|h a = Some obj; G\\<turnstile>obj_ty obj\\<preceq>T|] ==> G,h\\<turnstile>Addr a::\\<preceq>T"
    1.78  (K [Asm_full_simp_tac 1]);
    1.79  
    1.80  val conf_obj_AddrI = prove_goalw thy [conf_def]
    1.81 - "\\<And>G. \\<lbrakk>h a = Some (C,fs); G\\<turnstile>C\\<preceq>C D\\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>Addr a\\<Colon>\\<preceq> Class D" 
    1.82 + "!!G. [|h a = Some (C,fs); G\\<turnstile>C\\<preceq>C D|] ==> G,h\\<turnstile>Addr a::\\<preceq> Class D" 
    1.83  (K [Asm_full_simp_tac 1]);
    1.84  
    1.85 -Goalw [conf_def] "is_type G T \\<longrightarrow> G,h\\<turnstile>default_val T\\<Colon>\\<preceq>T";
    1.86 +Goalw [conf_def] "is_type G T --> G,h\\<turnstile>default_val T::\\<preceq>T";
    1.87  by (res_inst_tac [("y","T")] ty.exhaust 1);
    1.88  by  (etac ssubst 1);
    1.89  by  (res_inst_tac [("y","prim_ty")] prim_ty.exhaust 1);
    1.90 @@ -80,7 +80,7 @@
    1.91  qed_spec_mp "defval_conf";
    1.92  
    1.93  val conf_upd_obj = prove_goalw thy [conf_def] 
    1.94 -"h a = Some (C,fs) \\<longrightarrow> (G,h(a\\<mapsto>(C,fs'))\\<turnstile>x\\<Colon>\\<preceq>T) = (G,h\\<turnstile>x\\<Colon>\\<preceq>T)" (fn _ => [
    1.95 +"h a = Some (C,fs) --> (G,h(a\\<mapsto>(C,fs'))\\<turnstile>x::\\<preceq>T) = (G,h\\<turnstile>x::\\<preceq>T)" (fn _ => [
    1.96  	rtac impI 1,
    1.97  	rtac val_.induct 1,
    1.98  	 ALLGOALS Simp_tac,
    1.99 @@ -88,14 +88,14 @@
   1.100  	 ALLGOALS Asm_simp_tac]) RS mp;
   1.101  
   1.102  val conf_widen = prove_goalw thy [conf_def] 
   1.103 -"\\<And>G. wf_prog wf_mb G \\<Longrightarrow> G,h\\<turnstile>x\\<Colon>\\<preceq>T \\<longrightarrow> G\\<turnstile>T\\<preceq>T' \\<longrightarrow> G,h\\<turnstile>x\\<Colon>\\<preceq>T'" (K [
   1.104 +"!!G. wf_prog wf_mb G ==> G,h\\<turnstile>x::\\<preceq>T --> G\\<turnstile>T\\<preceq>T' --> G,h\\<turnstile>x::\\<preceq>T'" (K [
   1.105  	rtac val_.induct 1,
   1.106  	    ALLGOALS Simp_tac,
   1.107  	    ALLGOALS (fast_tac (HOL_cs addIs [widen_trans]))]) RS mp RS mp;
   1.108  bind_thm ("conf_widen", conf_widen);
   1.109  
   1.110  val conf_hext' = prove_goalw thy [conf_def] 
   1.111 -	"\\<And>h. h\\<le>|h' \\<Longrightarrow> (\\<forall>v T. G,h\\<turnstile>v\\<Colon>\\<preceq>T \\<longrightarrow> G,h'\\<turnstile>v\\<Colon>\\<preceq>T)" (K [
   1.112 +	"!!h. h\\<le>|h' ==> (\\<forall>v T. G,h\\<turnstile>v::\\<preceq>T --> G,h'\\<turnstile>v::\\<preceq>T)" (K [
   1.113  	REPEAT (rtac allI 1),
   1.114  	rtac val_.induct 1,
   1.115  	 ALLGOALS Simp_tac,
   1.116 @@ -107,36 +107,36 @@
   1.117  bind_thm ("conf_hext", conf_hext);
   1.118  
   1.119  val new_locD = prove_goalw thy [conf_def] 
   1.120 -	"\\<lbrakk>h a = None; G,h\\<turnstile>Addr t\\<Colon>\\<preceq>T\\<rbrakk> \\<Longrightarrow> t\\<noteq>a" (fn prems => [
   1.121 +	"[|h a = None; G,h\\<turnstile>Addr t::\\<preceq>T|] ==> t\\<noteq>a" (fn prems => [
   1.122  	cut_facts_tac prems 1,
   1.123  	Full_simp_tac 1,
   1.124  	safe_tac HOL_cs,
   1.125  	Asm_full_simp_tac 1]);
   1.126  
   1.127  Goalw [conf_def]
   1.128 - "G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT T \\<longrightarrow> a' = Null |  \
   1.129 + "G,h\\<turnstile>a'::\\<preceq>RefT T --> a' = Null |  \
   1.130  \ (\\<exists>a obj T'. a' = Addr a \\<and>  h a = Some obj \\<and>  obj_ty obj = T' \\<and>  G\\<turnstile>T'\\<preceq>RefT T)";
   1.131  by(induct_tac "a'" 1);
   1.132  by(Auto_tac);
   1.133  qed_spec_mp "conf_RefTD";
   1.134  
   1.135 -val conf_NullTD = prove_goal thy "\\<And>G. G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT NullT \\<Longrightarrow> a' = Null" (K [
   1.136 +val conf_NullTD = prove_goal thy "!!G. G,h\\<turnstile>a'::\\<preceq>RefT NullT ==> a' = Null" (K [
   1.137  	dtac conf_RefTD 1,
   1.138  	Step_tac 1,
   1.139  	 Auto_tac]);
   1.140  
   1.141 -val non_npD = prove_goal thy "\\<And>G. \\<lbrakk>a' \\<noteq> Null; G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT t\\<rbrakk> \\<Longrightarrow> \
   1.142 +val non_npD = prove_goal thy "!!G. [|a' \\<noteq> Null; G,h\\<turnstile>a'::\\<preceq>RefT t|] ==> \
   1.143  \ \\<exists>a C fs. a' = Addr a \\<and>  h a = Some (C,fs) \\<and>  G\\<turnstile>Class C\\<preceq>RefT t" (K [
   1.144  	dtac conf_RefTD 1,
   1.145  	Step_tac 1,
   1.146  	 Auto_tac]);
   1.147  
   1.148 -val non_np_objD = prove_goal thy "\\<And>G. \\<lbrakk>a' \\<noteq> Null; G,h\\<turnstile>a'\\<Colon>\\<preceq> Class C; C \\<noteq> Object\\<rbrakk> \\<Longrightarrow> \
   1.149 +val non_np_objD = prove_goal thy "!!G. [|a' \\<noteq> Null; G,h\\<turnstile>a'::\\<preceq> Class C; C \\<noteq> Object|] ==> \
   1.150  \ (\\<exists>a C' fs. a' = Addr a \\<and>  h a = Some (C',fs) \\<and>  G\\<turnstile>C'\\<preceq>C C)" 
   1.151  	(K[fast_tac (claset() addDs [non_npD]) 1]);
   1.152  
   1.153 -Goal "a' \\<noteq> Null \\<longrightarrow> wf_prog wf_mb G \\<longrightarrow> G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT t \\<longrightarrow>\
   1.154 -\ (\\<forall>C. t = ClassT C \\<longrightarrow> C \\<noteq> Object) \\<longrightarrow> \
   1.155 +Goal "a' \\<noteq> Null --> wf_prog wf_mb G --> G,h\\<turnstile>a'::\\<preceq>RefT t -->\
   1.156 +\ (\\<forall>C. t = ClassT C --> C \\<noteq> Object) --> \
   1.157  \ (\\<exists>a C fs. a' = Addr a \\<and>  h a = Some (C,fs) \\<and>  G\\<turnstile>Class C\\<preceq>RefT t)";
   1.158  by(rtac impI 1);
   1.159  by(rtac impI 1);
   1.160 @@ -150,7 +150,7 @@
   1.161  by(Fast_tac 1);
   1.162  qed_spec_mp "non_np_objD'";
   1.163  
   1.164 -Goal "wf_prog wf_mb G \\<Longrightarrow> \\<forall>Ts Ts'. list_all2 (conf G h) vs Ts \\<longrightarrow> list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') Ts Ts' \\<longrightarrow>  list_all2 (conf G h) vs Ts'";
   1.165 +Goal "wf_prog wf_mb G ==> \\<forall>Ts Ts'. list_all2 (conf G h) vs Ts --> list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') Ts Ts' -->  list_all2 (conf G h) vs Ts'";
   1.166  by(induct_tac "vs" 1);
   1.167   by(ALLGOALS Clarsimp_tac);
   1.168  by(forward_tac [list_all2_lengthD RS sym] 1);
   1.169 @@ -166,30 +166,30 @@
   1.170  section "lconf";
   1.171  
   1.172  val lconfD = prove_goalw thy [lconf_def] 
   1.173 -   "\\<And>X. \\<lbrakk> G,h\\<turnstile>vs[\\<Colon>\\<preceq>]Ts; Ts n = Some T \\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>(the (vs n))\\<Colon>\\<preceq>T"
   1.174 +   "!!X. [| G,h\\<turnstile>vs[::\\<preceq>]Ts; Ts n = Some T |] ==> G,h\\<turnstile>(the (vs n))::\\<preceq>T"
   1.175   (K [Force_tac 1]);
   1.176  
   1.177  val lconf_hext = prove_goalw thy [lconf_def] 
   1.178 -	"\\<And>X. \\<lbrakk> G,h\\<turnstile>l[\\<Colon>\\<preceq>]L; h\\<le>|h' \\<rbrakk> \\<Longrightarrow> G,h'\\<turnstile>l[\\<Colon>\\<preceq>]L" (K [
   1.179 +	"!!X. [| G,h\\<turnstile>l[::\\<preceq>]L; h\\<le>|h' |] ==> G,h'\\<turnstile>l[::\\<preceq>]L" (K [
   1.180  		fast_tac (claset() addEs [conf_hext]) 1]);
   1.181  AddEs [lconf_hext];
   1.182  
   1.183 -Goalw [lconf_def] "\\<And>X. \\<lbrakk> G,h\\<turnstile>l[\\<Colon>\\<preceq>]lT; \
   1.184 -\ G,h\\<turnstile>v\\<Colon>\\<preceq>T; lT va = Some T \\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>l(va\\<mapsto>v)[\\<Colon>\\<preceq>]lT";
   1.185 +Goalw [lconf_def] "!!X. [| G,h\\<turnstile>l[::\\<preceq>]lT; \
   1.186 +\ G,h\\<turnstile>v::\\<preceq>T; lT va = Some T |] ==> G,h\\<turnstile>l(va\\<mapsto>v)[::\\<preceq>]lT";
   1.187  by( Clarify_tac 1);
   1.188  by( case_tac "n = va" 1);
   1.189   by Auto_tac;
   1.190  qed "lconf_upd";
   1.191  
   1.192 -Goal "\\<forall>x. P x \\<longrightarrow> R (dv x) x \\<Longrightarrow> (\\<forall>x. map_of fs f = Some x \\<longrightarrow> P x) \\<longrightarrow> \
   1.193 -\ (\\<forall>T. map_of fs f = Some T \\<longrightarrow> \
   1.194 +Goal "\\<forall>x. P x --> R (dv x) x ==> (\\<forall>x. map_of fs f = Some x --> P x) --> \
   1.195 +\ (\\<forall>T. map_of fs f = Some T --> \
   1.196  \ (\\<exists>v. map_of (map (\\<lambda>(f,ft). (f, dv ft)) fs) f = Some v \\<and>  R v T))";
   1.197  by( induct_tac "fs" 1);
   1.198  by Auto_tac;
   1.199  qed_spec_mp "lconf_init_vars_lemma";
   1.200  
   1.201  Goalw [lconf_def, init_vars_def] 
   1.202 -"\\<forall>n. \\<forall>T. map_of fs n = Some T \\<longrightarrow> is_type G T \\<Longrightarrow> G,h\\<turnstile>init_vars fs[\\<Colon>\\<preceq>]map_of fs";
   1.203 +"\\<forall>n. \\<forall>T. map_of fs n = Some T --> is_type G T ==> G,h\\<turnstile>init_vars fs[::\\<preceq>]map_of fs";
   1.204  by Auto_tac;
   1.205  by( rtac lconf_init_vars_lemma 1);
   1.206  by(   atac 3);
   1.207 @@ -200,10 +200,10 @@
   1.208  AddSIs [lconf_init_vars];
   1.209  
   1.210  val lconf_ext = prove_goalw thy [lconf_def] 
   1.211 -"\\<And>X. \\<lbrakk>G,s\\<turnstile>l[\\<Colon>\\<preceq>]L; G,s\\<turnstile>v\\<Colon>\\<preceq>T\\<rbrakk> \\<Longrightarrow> G,s\\<turnstile>l(vn\\<mapsto>v)[\\<Colon>\\<preceq>]L(vn\\<mapsto>T)" 
   1.212 +"!!X. [|G,s\\<turnstile>l[::\\<preceq>]L; G,s\\<turnstile>v::\\<preceq>T|] ==> G,s\\<turnstile>l(vn\\<mapsto>v)[::\\<preceq>]L(vn\\<mapsto>T)" 
   1.213  	(K [Auto_tac]);
   1.214  
   1.215 -Goalw [lconf_def] "G,h\\<turnstile>l[\\<Colon>\\<preceq>]L \\<Longrightarrow> \\<forall>vs Ts. nodups vns \\<longrightarrow> length Ts = length vns \\<longrightarrow> list_all2 (\\<lambda>v T. G,h\\<turnstile>v\\<Colon>\\<preceq>T) vs Ts \\<longrightarrow> G,h\\<turnstile>l(vns[\\<mapsto>]vs)[\\<Colon>\\<preceq>]L(vns[\\<mapsto>]Ts)";
   1.216 +Goalw [lconf_def] "G,h\\<turnstile>l[::\\<preceq>]L ==> \\<forall>vs Ts. nodups vns --> length Ts = length vns --> list_all2 (\\<lambda>v T. G,h\\<turnstile>v::\\<preceq>T) vs Ts --> G,h\\<turnstile>l(vns[\\<mapsto>]vs)[::\\<preceq>]L(vns[\\<mapsto>]Ts)";
   1.217  by( induct_tac "vns" 1);
   1.218  by(  ALLGOALS Clarsimp_tac);
   1.219  by( forward_tac [list_all2_lengthD] 1);
   1.220 @@ -214,10 +214,10 @@
   1.221  section "oconf";
   1.222  
   1.223  val oconf_hext = prove_goalw thy [oconf_def] 
   1.224 -"\\<And>X. G,h\\<turnstile>obj\\<surd> \\<Longrightarrow> h\\<le>|h' \\<Longrightarrow> G,h'\\<turnstile>obj\\<surd>" (K [Fast_tac 1]);
   1.225 +"!!X. G,h\\<turnstile>obj\\<surd> ==> h\\<le>|h' ==> G,h'\\<turnstile>obj\\<surd>" (K [Fast_tac 1]);
   1.226  
   1.227  val oconf_obj = prove_goalw thy [oconf_def,lconf_def] "G,h\\<turnstile>(C,fs)\\<surd> = \
   1.228 -\ (\\<forall>T f. map_of(fields (G,C)) f = Some T \\<longrightarrow> (\\<exists>v. fs f = Some v \\<and>  G,h\\<turnstile>v\\<Colon>\\<preceq>T))"(K [
   1.229 +\ (\\<forall>T f. map_of(fields (G,C)) f = Some T --> (\\<exists>v. fs f = Some v \\<and>  G,h\\<turnstile>v::\\<preceq>T))"(K [
   1.230  	Auto_tac]);
   1.231  
   1.232  val oconf_objD = oconf_obj RS iffD1 RS spec RS spec RS mp;
   1.233 @@ -225,11 +225,11 @@
   1.234  
   1.235  section "hconf";
   1.236  
   1.237 -Goalw [hconf_def] "\\<lbrakk>G\\<turnstile>h h\\<surd>; h a = Some obj\\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>obj\\<surd>";
   1.238 +Goalw [hconf_def] "[|G\\<turnstile>h h\\<surd>; h a = Some obj|] ==> G,h\\<turnstile>obj\\<surd>";
   1.239  by (Fast_tac 1);
   1.240  qed "hconfD";
   1.241  
   1.242 -Goalw [hconf_def] "\\<forall>a obj. h a=Some obj \\<longrightarrow> G,h\\<turnstile>obj\\<surd> \\<Longrightarrow> G\\<turnstile>h h\\<surd>";
   1.243 +Goalw [hconf_def] "\\<forall>a obj. h a=Some obj --> G,h\\<turnstile>obj\\<surd> ==> G\\<turnstile>h h\\<surd>";
   1.244  by (Fast_tac 1);
   1.245  qed "hconfI";
   1.246  
   1.247 @@ -237,25 +237,25 @@
   1.248  section "conforms";
   1.249  
   1.250  val conforms_heapD = prove_goalw thy [conforms_def]
   1.251 -	"(h, l)\\<Colon>\\<preceq>(G, lT) \\<Longrightarrow> G\\<turnstile>h h\\<surd>"
   1.252 +	"(h, l)::\\<preceq>(G, lT) ==> G\\<turnstile>h h\\<surd>"
   1.253  	(fn prems => [cut_facts_tac prems 1, Asm_full_simp_tac 1]);
   1.254  
   1.255  val conforms_localD = prove_goalw thy [conforms_def]
   1.256 -	 "(h, l)\\<Colon>\\<preceq>(G, lT) \\<Longrightarrow> G,h\\<turnstile>l[\\<Colon>\\<preceq>]lT" (fn prems => [
   1.257 +	 "(h, l)::\\<preceq>(G, lT) ==> G,h\\<turnstile>l[::\\<preceq>]lT" (fn prems => [
   1.258  	cut_facts_tac prems 1, Asm_full_simp_tac 1]);
   1.259  
   1.260  val conformsI = prove_goalw thy [conforms_def] 
   1.261 -"\\<lbrakk>G\\<turnstile>h h\\<surd>; G,h\\<turnstile>l[\\<Colon>\\<preceq>]lT\\<rbrakk> \\<Longrightarrow> (h, l)\\<Colon>\\<preceq>(G, lT)" (fn prems => [
   1.262 +"[|G\\<turnstile>h h\\<surd>; G,h\\<turnstile>l[::\\<preceq>]lT|] ==> (h, l)::\\<preceq>(G, lT)" (fn prems => [
   1.263  	cut_facts_tac prems 1,
   1.264  	Simp_tac 1,
   1.265  	Auto_tac]);
   1.266  
   1.267 -Goal "\\<lbrakk>(h,l)\\<Colon>\\<preceq>(G,lT); h\\<le>|h'; G\\<turnstile>h h'\\<surd> \\<rbrakk> \\<Longrightarrow> (h',l)\\<Colon>\\<preceq>(G,lT)";
   1.268 +Goal "[|(h,l)::\\<preceq>(G,lT); h\\<le>|h'; G\\<turnstile>h h'\\<surd> |] ==> (h',l)::\\<preceq>(G,lT)";
   1.269  by( fast_tac (HOL_cs addDs [conforms_localD] 
   1.270    addSEs [conformsI, lconf_hext]) 1);
   1.271  qed "conforms_hext";
   1.272  
   1.273 -Goal "\\<lbrakk>(h,l)\\<Colon>\\<preceq>(G, lT); G,h(a\\<mapsto>obj)\\<turnstile>obj\\<surd>; h\\<le>|h(a\\<mapsto>obj)\\<rbrakk> \\<Longrightarrow> (h(a\\<mapsto>obj),l)\\<Colon>\\<preceq>(G, lT)";
   1.274 +Goal "[|(h,l)::\\<preceq>(G, lT); G,h(a\\<mapsto>obj)\\<turnstile>obj\\<surd>; h\\<le>|h(a\\<mapsto>obj)|] ==> (h(a\\<mapsto>obj),l)::\\<preceq>(G, lT)";
   1.275  by( rtac conforms_hext 1);
   1.276  by   Auto_tac;
   1.277  by( rtac hconfI 1);
   1.278 @@ -265,7 +265,7 @@
   1.279  qed "conforms_upd_obj";
   1.280  
   1.281  Goalw [conforms_def] 
   1.282 -"\\<lbrakk>(h, l)\\<Colon>\\<preceq>(G, lT); G,h\\<turnstile>v\\<Colon>\\<preceq>T; lT va = Some T\\<rbrakk> \\<Longrightarrow> \
   1.283 -\ (h, l(va\\<mapsto>v))\\<Colon>\\<preceq>(G, lT)";
   1.284 +"[|(h, l)::\\<preceq>(G, lT); G,h\\<turnstile>v::\\<preceq>T; lT va = Some T|] ==> \
   1.285 +\ (h, l(va\\<mapsto>v))::\\<preceq>(G, lT)";
   1.286  by( auto_tac (claset() addEs [lconf_upd], simpset()));
   1.287  qed "conforms_upd_local";