Completely split rule eval_evals_exec.induct before applying it.
authorberghofe
Mon Jan 29 13:31:30 2001 +0100 (2001-01-29)
changeset 10990e7ffc23a05f6
parent 10989 87f8a7644f91
child 10991 2e59c831cf07
Completely split rule eval_evals_exec.induct before applying it.
src/HOL/MicroJava/J/Eval.ML
src/HOL/MicroJava/J/JTypeSafe.ML
     1.1 --- a/src/HOL/MicroJava/J/Eval.ML	Mon Jan 29 13:28:15 2001 +0100
     1.2 +++ b/src/HOL/MicroJava/J/Eval.ML	Mon Jan 29 13:31:30 2001 +0100
     1.3 @@ -4,6 +4,8 @@
     1.4      Copyright   1999 Technische Universitaet Muenchen
     1.5  *)
     1.6  
     1.7 +val eval_evals_exec_induct = complete_split_rule eval_evals_exec.induct;
     1.8 +
     1.9  Goal "[|new_Addr (heap s) = (a,x); \
    1.10  \      s' = c_hupd (heap s(a\\<mapsto>(C,init_vars (fields (G,C))))) (x,s)|] ==> \
    1.11  \      G\\<turnstile>Norm s -NewC C\\<succ>Addr a-> s'";
    1.12 @@ -16,7 +18,7 @@
    1.13  \             (G\\<turnstile>(x,s) -es[\\<succ>]vs-> (x',s') --> x'=None --> x=None) \\<and> \
    1.14  \             (G\\<turnstile>(x,s) -c       -> (x',s') --> x'=None --> x=None)";
    1.15  by(split_all_tac 1);
    1.16 -by(rtac eval_evals_exec.induct 1);
    1.17 +by(rtac eval_evals_exec_induct 1);
    1.18  by(rewtac c_hupd_def);
    1.19  by(ALLGOALS Asm_full_simp_tac);
    1.20  qed "eval_evals_exec_no_xcpt";
    1.21 @@ -36,7 +38,7 @@
    1.22  \        (G\\<turnstile>(x,s) -es[\\<succ>]vs-> (x',s') --> x=Some xc --> x'=Some xc \\<and> s'=s) \\<and> \
    1.23  \        (G\\<turnstile>(x,s) -c       -> (x',s') --> x=Some xc --> x'=Some xc \\<and> s'=s)";
    1.24  by (split_all_tac 1);
    1.25 -by (rtac eval_evals_exec.induct 1);
    1.26 +by (rtac eval_evals_exec_induct 1);
    1.27  by (rewtac c_hupd_def);
    1.28  by (ALLGOALS Asm_full_simp_tac);
    1.29  qed "eval_evals_exec_xcpt";
     2.1 --- a/src/HOL/MicroJava/J/JTypeSafe.ML	Mon Jan 29 13:28:15 2001 +0100
     2.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.ML	Mon Jan 29 13:31:30 2001 +0100
     2.3 @@ -173,7 +173,7 @@
     2.4  \ (G\\<turnstile>(x,(h,l)) -c       -> (x', (h',l')) --> \
     2.5  \     (\\<forall>lT.    (h ,l )::\\<preceq>(G,lT) -->       (G,lT)\\<turnstile>c  \\<surd> --> \
     2.6  \     h\\<le>|h' \\<and> (h',l')::\\<preceq>(G,lT)))";
     2.7 -by( rtac eval_evals_exec.induct 1);
     2.8 +by( rtac eval_evals_exec_induct 1);
     2.9  by( rewtac c_hupd_def);
    2.10  
    2.11  (* several simplifications, XcptE, XcptEs, XcptS, Skip, Nil?? *)