src/HOL/MicroJava/J/WellType.ML
changeset 10042 7164dc0d24d8
parent 8185 59b62e8804b4
child 10613 78b1d6c3ee9c
     1.1 --- a/src/HOL/MicroJava/J/WellType.ML	Wed Sep 20 21:20:41 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/J/WellType.ML	Thu Sep 21 10:42:49 2000 +0200
     1.3 @@ -5,15 +5,15 @@
     1.4  *)
     1.5  
     1.6  Goal
     1.7 -"\\<lbrakk> method (G,C) sig = Some (md,rT,b); wf_prog wf_mb G; G\\<turnstile>T''\\<preceq>C C\\<rbrakk>\
     1.8 -\ \\<Longrightarrow> \\<exists>md' rT' b'. method (G,T'') sig = Some (md',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
     1.9 +"[| method (G,C) sig = Some (md,rT,b); wf_prog wf_mb G; G\\<turnstile>T''\\<preceq>C C|]\
    1.10 +\ ==> \\<exists>md' rT' b'. method (G,T'') sig = Some (md',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
    1.11  by( dtac subcls_widen_methd 1);
    1.12  by   Auto_tac;
    1.13  qed "widen_methd";
    1.14  
    1.15  
    1.16  Goal
    1.17 -"\\<lbrakk>method (G,C) sig = Some (md,rT,b); G\\<turnstile>T''\\<preceq>C C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
    1.18 +"[|method (G,C) sig = Some (md,rT,b); G\\<turnstile>T''\\<preceq>C C; wf_prog wf_mb G|] ==> \
    1.19  \ \\<exists>T' rT' b. method (G,T'') sig = Some (T',rT',b) \\<and> \
    1.20  \ G\\<turnstile>rT'\\<preceq>rT \\<and> G\\<turnstile>T''\\<preceq>C T' \\<and> wf_mhead G sig rT' \\<and> wf_mb G T' (sig,rT',b)";
    1.21  by( datac widen_methd 2 1);
    1.22 @@ -25,25 +25,25 @@
    1.23  qed "Call_lemma";
    1.24  
    1.25  
    1.26 -Goal "wf_prog wf_mb G \\<Longrightarrow> method (G,Object) sig = None";
    1.27 +Goal "wf_prog wf_mb G ==> method (G,Object) sig = None";
    1.28  by (Asm_simp_tac 1);
    1.29  qed "method_Object";
    1.30  Addsimps [method_Object];
    1.31  
    1.32  Goalw [max_spec_def] 
    1.33 -  "x \\<in> max_spec G C sig \\<Longrightarrow> x \\<in> appl_methds G C sig";
    1.34 +  "x \\<in> max_spec G C sig ==> x \\<in> appl_methds G C sig";
    1.35  by (Fast_tac 1);
    1.36  qed"max_spec2appl_meths";
    1.37  
    1.38  Goalw [appl_methds_def] 
    1.39 -"((md,rT),pTs')\\<in>appl_methds G C (mn, pTs) \\<Longrightarrow> \
    1.40 +"((md,rT),pTs')\\<in>appl_methds G C (mn, pTs) ==> \
    1.41  \ \\<exists>D b. md = Class D \\<and> method (G,C) (mn, pTs') = Some (D,rT,b) \
    1.42  \ \\<and> list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'";
    1.43  by (Fast_tac 1);
    1.44  qed "appl_methsD";
    1.45  
    1.46  val is_type_typeof = prove_goal thy 
    1.47 -	"(\\<forall>a. v \\<noteq> Addr a) \\<longrightarrow> (\\<exists>T. typeof t v = Some T \\<and>  is_type G T)" (K [
    1.48 +	"(\\<forall>a. v \\<noteq> Addr a) --> (\\<exists>T. typeof t v = Some T \\<and>  is_type G T)" (K [
    1.49  	rtac val_.induct 1,
    1.50  	    Fast_tac 5,
    1.51  	   ALLGOALS Simp_tac]) RS mp;