8245
|
1 |
(* Title: HOL/MicroJava/BV/BVLightSpec.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Gerwin Klein
|
|
4 |
Copyright 1999 Technische Universitaet Muenchen
|
|
5 |
*)
|
|
6 |
|
|
7 |
Goal "\\<lbrakk>length a = n; length x = n; rev a @ b # c = rev x @ y # z\\<rbrakk> \\<Longrightarrow> a = x \\<and> b = y \\<and> c = z";
|
|
8 |
by Auto_tac;
|
|
9 |
qed "rev_eq";
|
|
10 |
|
|
11 |
|
|
12 |
Goal "\\<lbrakk>wtl_inst i G rT s0 s1 cert max_pc pc; \
|
|
13 |
\ wtl_inst i G rT s0 s1' cert max_pc pc\\<rbrakk> \\<Longrightarrow> s1 = s1'";
|
8423
|
14 |
by (cases_tac "i" 1);
|
|
15 |
by (cases_tac "branch" 8);
|
|
16 |
by (cases_tac "op_stack" 7);
|
|
17 |
by (cases_tac "meth_ret" 6);
|
|
18 |
by (cases_tac "meth_inv" 5);
|
|
19 |
by (cases_tac "check_object" 4);
|
|
20 |
by (cases_tac "manipulate_object" 3);
|
|
21 |
by (cases_tac "create_object" 2);
|
|
22 |
by (cases_tac "load_and_store" 1);
|
8245
|
23 |
by Auto_tac;
|
|
24 |
by (ALLGOALS (dtac rev_eq));
|
|
25 |
by (TRYALL atac);
|
|
26 |
by (ALLGOALS Asm_full_simp_tac);
|
|
27 |
qed "wtl_inst_unique";
|
|
28 |
|
|
29 |
|
|
30 |
Goal "\\<lbrakk>wtl_inst_option i G rT s0 s1 cert max_pc pc; \
|
|
31 |
\ wtl_inst_option i G rT s0 s1' cert max_pc pc\\<rbrakk> \\<Longrightarrow> s1 = s1'";
|
8423
|
32 |
by (cases_tac "cert!pc" 1);
|
8245
|
33 |
by (auto_tac (claset(), simpset() addsimps [wtl_inst_unique, wtl_inst_option_def]));
|
|
34 |
qed "wtl_inst_option_unique";
|
|
35 |
|
|
36 |
Goal "\\<forall> s0 pc. wtl_inst_list is G rT s0 s1 cert max_pc pc \\<longrightarrow> \
|
|
37 |
\ wtl_inst_list is G rT s0 s1' cert max_pc pc \\<longrightarrow> s1=s1'";
|
|
38 |
by (induct_tac "is" 1);
|
|
39 |
by Auto_tac;
|
|
40 |
by (datac wtl_inst_option_unique 1 1);
|
|
41 |
by (Asm_full_simp_tac 1);
|
|
42 |
qed "wtl_inst_list_unique";
|
|
43 |
|
|
44 |
Goal "\\<forall> pc' pc s. \
|
|
45 |
\ wtl_inst_list is G rT s s' cert mpc pc \\<longrightarrow> \
|
|
46 |
\ pc' < length is \\<longrightarrow> \
|
|
47 |
\ (\\<exists> a b s1. a @ b = is \\<and> length a = pc' \\<and> \
|
|
48 |
\ wtl_inst_list a G rT s s1 cert mpc pc \\<and> \
|
|
49 |
\ wtl_inst_list b G rT s1 s' cert mpc (pc+length a))";
|
|
50 |
by(induct_tac "is" 1);
|
|
51 |
by Auto_tac;
|
8423
|
52 |
by (cases_tac "pc'" 1);
|
8245
|
53 |
by (dres_inst_tac [("x","pc'")] spec 1);
|
|
54 |
by (smp_tac 3 1);
|
|
55 |
by (res_inst_tac [("x","[]")] exI 1);
|
|
56 |
by (Asm_full_simp_tac 1);
|
8423
|
57 |
by (cases_tac "cert!pc" 1);
|
8245
|
58 |
by (Force_tac 1);
|
|
59 |
by (force_tac (claset(), simpset() addsimps [wtl_inst_option_def]) 1);
|
|
60 |
by (dres_inst_tac [("x","nat")] spec 1);
|
|
61 |
by (smp_tac 3 1);
|
|
62 |
by Safe_tac;
|
|
63 |
by (res_inst_tac [("x","a#list")] exI 1);
|
|
64 |
by (Asm_full_simp_tac 1);
|
|
65 |
by (res_inst_tac [("x","a#ac")] exI 1);
|
|
66 |
by (Force_tac 1);
|
|
67 |
qed_spec_mp "wtl_partial";
|
|
68 |
|
|
69 |
|
|
70 |
Goal "\\<forall> s0 pc. wtl_inst_list a G rT s0 s1 cert (pc+length (a@i#b)) pc \\<longrightarrow> \
|
|
71 |
\ wtl_inst_option i G rT s1 s2 cert (pc+length (a@i#b)) (pc + length a) \\<longrightarrow> \
|
|
72 |
\ wtl_inst_list b G rT s2 s3 cert (pc+length (a@i#b)) (Suc (pc + length a)) \\<longrightarrow> \
|
|
73 |
\ wtl_inst_list (a@[i]) G rT s0 s2 cert (pc+length (a@i#b)) pc";
|
|
74 |
by (induct_tac "a" 1);
|
|
75 |
by (Clarify_tac 1);
|
|
76 |
by (Asm_full_simp_tac 1);
|
|
77 |
by (pair_tac "s2" 1);
|
|
78 |
by (Force_tac 1);
|
|
79 |
by (Clarify_tac 1);
|
|
80 |
by (Asm_full_simp_tac 1);
|
|
81 |
by (Clarify_tac 1);
|
|
82 |
by (eres_inst_tac [("x","ab")] allE 1);
|
|
83 |
by (eres_inst_tac [("x","baa")] allE 1);
|
|
84 |
by (eres_inst_tac [("x","Suc pc")] allE 1);
|
|
85 |
by (Force_tac 1);
|
|
86 |
bind_thm ("wtl_append_lemma", result() RS spec RS spec);
|
|
87 |
|
|
88 |
Goal "\\<lbrakk>wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0; \
|
|
89 |
\ wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a); \
|
|
90 |
\ wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))\\<rbrakk> \\<Longrightarrow> \
|
|
91 |
\ wtl_inst_list (a@[i]) G rT s0 s2 cert (length (a@i#b)) 0";
|
|
92 |
by (cut_inst_tac [("a","a"),("G","G"),("rT","rT"),("xa","s0"),("s1.0","s1"),("cert","cert"),("x","0"),("i","i"),("b","b"),("s2.0","s2"),("s3.0","s3")] wtl_append_lemma 1);
|
|
93 |
by (Asm_full_simp_tac 1);
|
|
94 |
qed "wtl_append";
|
|
95 |
|
|
96 |
|