equal
deleted
inserted
replaced
1 (* Title: HOL/MicroJava/BV/Convert.ML |
1 (* Title: HOL/MicroJava/BV/Convert.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Cornelia Pusch |
3 Author: Cornelia Pusch |
4 Copyright 1999 Technische Universitaet Muenchen |
4 Copyright 1999 Technische Universitaet Muenchen |
5 *) |
5 *) |
|
6 |
|
7 |
|
8 Goalw[sup_ty_opt_def] "G \\<turnstile> t <=o t"; |
|
9 by (exhaust_tac "t" 1); |
|
10 by Auto_tac; |
|
11 qed "sup_ty_opt_refl"; |
|
12 Addsimps [sup_ty_opt_refl]; |
|
13 |
|
14 Goalw[sup_loc_def] "G \\<turnstile> t <=l t"; |
|
15 by (induct_tac "t" 1); |
|
16 by Auto_tac; |
|
17 qed "sup_loc_refl"; |
|
18 Addsimps [sup_loc_refl]; |
|
19 |
|
20 Goalw[sup_state_def] "G \\<turnstile> s <=s s"; |
|
21 by Auto_tac; |
|
22 qed "sup_state_refl"; |
|
23 Addsimps [sup_state_refl]; |
6 |
24 |
7 val widen_PrimT_conv1 = |
25 val widen_PrimT_conv1 = |
8 prove_typerel "(G \\<turnstile> PrimT x \\<preceq> T) = (T = PrimT x)" |
26 prove_typerel "(G \\<turnstile> PrimT x \\<preceq> T) = (T = PrimT x)" |
9 [ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = PrimT x \\<longrightarrow> T = PrimT x"]; |
27 [ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = PrimT x \\<longrightarrow> T = PrimT x"]; |
10 Addsimps [widen_PrimT_conv1]; |
28 Addsimps [widen_PrimT_conv1]; |
35 Goalw [sup_loc_def] |
53 Goalw [sup_loc_def] |
36 "CFS \\<turnstile> (Y#YT) <=l XT = (\\<exists>X XT'. XT=X#XT' \\<and> CFS \\<turnstile> Y <=o X \\<and> CFS \\<turnstile> YT <=l XT')"; |
54 "CFS \\<turnstile> (Y#YT) <=l XT = (\\<exists>X XT'. XT=X#XT' \\<and> CFS \\<turnstile> Y <=o X \\<and> CFS \\<turnstile> YT <=l XT')"; |
37 by(simp_tac (simpset() addsimps [list_all2_Cons1]) 1); |
55 by(simp_tac (simpset() addsimps [list_all2_Cons1]) 1); |
38 qed "sup_loc_Cons"; |
56 qed "sup_loc_Cons"; |
39 AddIffs [sup_loc_Cons]; |
57 AddIffs [sup_loc_Cons]; |
|
58 |