src/HOL/MicroJava/J/TypeRel.ML
changeset 10042 7164dc0d24d8
parent 9581 b295382e1549
child 10613 78b1d6c3ee9c
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.ML	Wed Sep 20 21:20:41 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.ML	Thu Sep 21 10:42:49 2000 +0200
     1.3 @@ -4,11 +4,11 @@
     1.4      Copyright   1999 Technische Universitaet Muenchen
     1.5  *)
     1.6  
     1.7 -val subcls1D = prove_goalw thy [subcls1_def] "\\<And>G. G\\<turnstile>C\\<prec>C1D \\<Longrightarrow> \
     1.8 +val subcls1D = prove_goalw thy [subcls1_def] "!!G. G\\<turnstile>C\\<prec>C1D ==> \
     1.9  \ \\<exists>fs ms. class G C = Some (Some D,fs,ms)" (K [Auto_tac]);
    1.10  
    1.11  val subcls1I = prove_goalw  thy [subcls1_def] 
    1.12 -"\\<And>G. \\<lbrakk> class G C = Some (Some D,rest) \\<rbrakk> \\<Longrightarrow> G\\<turnstile>C\\<prec>C1D" (K [Auto_tac]);
    1.13 +"!!G. [| class G C = Some (Some D,rest) |] ==> G\\<turnstile>C\\<prec>C1D" (K [Auto_tac]);
    1.14  
    1.15  val subcls1_def2 = prove_goalw thy [subcls1_def,is_class_def]  "subcls1 G = \
    1.16  \ (SIGMA C:{C. is_class G C} . {D. fst (the (class G C)) = Some D})"
    1.17 @@ -32,7 +32,7 @@
    1.18  	auto_tac (claset() addDs lemmata, simpset())]);
    1.19  
    1.20  
    1.21 -Goalw [is_class_def] "(C,D) \\<in> (subcls1 G)^+ \\<Longrightarrow> is_class G C";
    1.22 +Goalw [is_class_def] "(C,D) \\<in> (subcls1 G)^+ ==> is_class G C";
    1.23  by(etac trancl_trans_induct 1);
    1.24  by (auto_tac (HOL_cs addSDs [subcls1D],simpset()));
    1.25  qed "subcls_is_class";
    1.26 @@ -81,16 +81,16 @@
    1.27  qed "widen_PrimT_RefT";
    1.28  AddIffs [widen_PrimT_RefT];
    1.29  
    1.30 -val widen_RefT = prove_typerel "G\\<turnstile>RefT R\\<preceq>T \\<Longrightarrow> \\<exists>t. T=RefT t" 
    1.31 -	[prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S=RefT R \\<longrightarrow> (\\<exists>t. T=RefT t)"];
    1.32 +val widen_RefT = prove_typerel "G\\<turnstile>RefT R\\<preceq>T ==> \\<exists>t. T=RefT t" 
    1.33 +	[prove_widen_lemma "G\\<turnstile>S\\<preceq>T ==> S=RefT R --> (\\<exists>t. T=RefT t)"];
    1.34  bind_thm ("widen_RefT", widen_RefT);
    1.35  
    1.36 -val widen_RefT2 = prove_typerel "G\\<turnstile>S\\<preceq>RefT R \\<Longrightarrow> \\<exists>t. S=RefT t" 
    1.37 -	[prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> T=RefT R \\<longrightarrow> (\\<exists>t. S=RefT t)"];
    1.38 +val widen_RefT2 = prove_typerel "G\\<turnstile>S\\<preceq>RefT R ==> \\<exists>t. S=RefT t" 
    1.39 +	[prove_widen_lemma "G\\<turnstile>S\\<preceq>T ==> T=RefT R --> (\\<exists>t. S=RefT t)"];
    1.40  bind_thm ("widen_RefT2", widen_RefT2);
    1.41  
    1.42 -val widen_Class = prove_typerel "G\\<turnstile>Class C\\<preceq>T \\<Longrightarrow> \\<exists>D. T=Class D"
    1.43 - [ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = Class C \\<longrightarrow> (\\<exists>D. T=Class D)"];
    1.44 +val widen_Class = prove_typerel "G\\<turnstile>Class C\\<preceq>T ==> \\<exists>D. T=Class D"
    1.45 + [ prove_widen_lemma "G\\<turnstile>S\\<preceq>T ==> S = Class C --> (\\<exists>D. T=Class D)"];
    1.46  bind_thm ("widen_Class", widen_Class);
    1.47  
    1.48  Goal "(G\\<turnstile>Class C\\<preceq>RefT NullT) = False"; 
    1.49 @@ -108,7 +108,7 @@
    1.50  qed "widen_Class_Class";
    1.51  AddIffs [widen_Class_Class];
    1.52  
    1.53 -Goal "G\\<turnstile>S\\<preceq>U \\<Longrightarrow> \\<forall>T. G\\<turnstile>U\\<preceq>T \\<longrightarrow> G\\<turnstile>S\\<preceq>T";
    1.54 +Goal "G\\<turnstile>S\\<preceq>U ==> \\<forall>T. G\\<turnstile>U\\<preceq>T --> G\\<turnstile>S\\<preceq>T";
    1.55  by( etac widen.induct 1);
    1.56  by   Safe_tac;
    1.57  by(  ALLGOALS (forward_tac [widen_Class, widen_RefT]));