author | oheimb |
Wed, 05 Jul 2000 10:28:29 +0200 | |
changeset 9246 | 91423cd08c6f |
parent 8185 | 59b62e8804b4 |
child 9348 | f495dba0cb07 |
permissions | -rw-r--r-- |
8011 | 1 |
(* Title: HOL/MicroJava/J/TypeRel.ML |
2 |
ID: $Id$ |
|
3 |
Author: David von Oheimb |
|
4 |
Copyright 1999 Technische Universitaet Muenchen |
|
5 |
*) |
|
6 |
||
7 |
val subcls1D = prove_goalw thy [subcls1_def] "\\<And>G. G\\<turnstile>C\\<prec>C1D \\<Longrightarrow> \ |
|
8 |
\ \\<exists>fs ms. class G C = Some (Some D,fs,ms)" (K [Auto_tac]); |
|
9 |
||
10 |
val subcls1I = prove_goalw thy [subcls1_def] |
|
11 |
"\\<And>G. \\<lbrakk> class G C = Some (Some D,rest) \\<rbrakk> \\<Longrightarrow> G\\<turnstile>C\\<prec>C1D" (K [Auto_tac]); |
|
12 |
||
13 |
val subcls1_def2 = prove_goalw thy [subcls1_def,is_class_def] "subcls1 G = \ |
|
14 |
\ (SIGMA C:{C. is_class G C} . {D. fst (the (class G C)) = Some D})" |
|
15 |
(K [Auto_tac]); |
|
16 |
||
17 |
Goal "finite (subcls1 G)"; |
|
18 |
by(stac subcls1_def2 1); |
|
19 |
by( rtac finite_SigmaI 1); |
|
20 |
by( rtac finite_is_class 1); |
|
21 |
by( rtac finite_subset 1); |
|
22 |
by( rtac some_subset_the 1); |
|
23 |
by( Simp_tac 1); |
|
24 |
qed "finite_subcls1"; |
|
25 |
||
26 |
fun prove_typerel_lemma drules indrule s = prove_goal thy s (fn prems => [ |
|
27 |
rtac (hd prems RS indrule) 1, |
|
28 |
auto_tac (claset() addDs drules, simpset())]); |
|
29 |
||
30 |
fun prove_typerel s lemmata = prove_goal thy s (fn prems => [ |
|
31 |
cut_facts_tac prems 1, |
|
32 |
auto_tac (claset() addDs lemmata, simpset())]); |
|
33 |
||
34 |
||
8082 | 35 |
Goalw [is_class_def] "(C,D) \\<in> (subcls1 G)^+ \\<Longrightarrow> is_class G C"; |
8011 | 36 |
by(etac trancl_trans_induct 1); |
37 |
by (auto_tac (HOL_cs addSDs [subcls1D],simpset())); |
|
38 |
qed "subcls_is_class"; |
|
39 |
||
40 |
(* A particular thm about wf; |
|
41 |
looks like it is an odd instance of something more general |
|
42 |
*) |
|
43 |
Goalw [wf_def] "wf{((A,x),(B,y)) . A=B \\<and> wf(R(A)) \\<and> (x,y)\\<in>R(A)}"; |
|
44 |
by(full_simp_tac (simpset() delcongs [imp_cong] addsimps [split_paired_All]) 1); |
|
45 |
by(strip_tac 1); |
|
46 |
by(rename_tac "A x" 1); |
|
47 |
by(case_tac "wf(R A)" 1); |
|
48 |
by (eres_inst_tac [("a","x")] wf_induct 1); |
|
49 |
by (EVERY1[etac allE, etac allE, etac mp, rtac allI, rtac allI]); |
|
50 |
by (Fast_tac 1); |
|
51 |
by(rewrite_goals_tac [wf_def]); |
|
52 |
by(Blast_tac 1); |
|
8082 | 53 |
qed "wf_rel_lemma"; |
8011 | 54 |
|
55 |
||
56 |
(* Proving the termination conditions *) |
|
57 |
||
58 |
goalw thy [subcls1_rel_def] "wf subcls1_rel"; |
|
59 |
by(rtac (wf_rel_lemma RS wf_subset) 1); |
|
60 |
by(Force_tac 1); |
|
8082 | 61 |
qed "wf_subcls1_rel"; |
8011 | 62 |
|
8034
6fc37b5c5e98
Various little changes like cmethd -> method and cfield -> field.
nipkow
parents:
8011
diff
changeset
|
63 |
val method_TC = prove_goalw_cterm [subcls1_rel_def] |
6fc37b5c5e98
Various little changes like cmethd -> method and cfield -> field.
nipkow
parents:
8011
diff
changeset
|
64 |
(cterm_of (sign_of thy) (HOLogic.mk_Trueprop (hd (tl (method.tcs))))) |
8011 | 65 |
(K [auto_tac (claset() addIs [subcls1I], simpset())]); |
66 |
||
67 |
val fields_TC = prove_goalw_cterm [subcls1_rel_def] |
|
68 |
(cterm_of (sign_of thy) (HOLogic.mk_Trueprop (hd (tl (fields.tcs))))) |
|
69 |
(K [auto_tac (claset() addIs [subcls1I], simpset())]); |
|
70 |
||
71 |
||
72 |
AddSIs [widen.refl]; |
|
73 |
Addsimps [widen.refl]; |
|
74 |
||
75 |
val prove_widen_lemma = prove_typerel_lemma [] widen.elim; |
|
76 |
||
8185 | 77 |
Goal "(G\\<turnstile>PrimT pT\\<preceq>RefT rT) = False"; |
78 |
br iffI 1; |
|
79 |
be widen.elim 1; |
|
80 |
by(Auto_tac); |
|
81 |
qed "widen_PrimT_RefT"; |
|
82 |
AddIffs [widen_PrimT_RefT]; |
|
8011 | 83 |
|
84 |
val widen_RefT = prove_typerel "G\\<turnstile>RefT R\\<preceq>T \\<Longrightarrow> \\<exists>t. T=RefT t" |
|
85 |
[prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S=RefT R \\<longrightarrow> (\\<exists>t. T=RefT t)"]; |
|
86 |
||
87 |
val widen_RefT2 = prove_typerel "G\\<turnstile>S\\<preceq>RefT R \\<Longrightarrow> \\<exists>t. S=RefT t" |
|
88 |
[prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> T=RefT R \\<longrightarrow> (\\<exists>t. S=RefT t)"]; |
|
89 |
||
90 |
val widen_Class = prove_typerel "G\\<turnstile>Class C\\<preceq>T \\<Longrightarrow> \\<exists>D. T=Class D" |
|
91 |
[ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = Class C \\<longrightarrow> (\\<exists>D. T=Class D)"]; |
|
92 |
||
8185 | 93 |
Goal "(G\\<turnstile>Class C\\<preceq>RefT NullT) = False"; |
94 |
br iffI 1; |
|
95 |
be widen.elim 1; |
|
96 |
by(Auto_tac); |
|
97 |
qed "widen_Class_NullT"; |
|
98 |
AddIffs [widen_Class_NullT]; |
|
8011 | 99 |
|
8185 | 100 |
Goal "(G\\<turnstile>Class C\\<preceq> Class D) = (G\\<turnstile>C\\<preceq>C D)"; |
101 |
br iffI 1; |
|
102 |
be widen.elim 1; |
|
103 |
by(Auto_tac); |
|
104 |
bes widen.intrs 1; |
|
105 |
qed "widen_Class_Class"; |
|
106 |
AddIffs [widen_Class_Class]; |
|
8011 | 107 |
|
8082 | 108 |
Goal "G\\<turnstile>S\\<preceq>U \\<Longrightarrow> \\<forall>T. G\\<turnstile>U\\<preceq>T \\<longrightarrow> G\\<turnstile>S\\<preceq>T"; |
8011 | 109 |
by( etac widen.induct 1); |
110 |
by Safe_tac; |
|
111 |
by( ALLGOALS (forward_tac [widen_Class, widen_RefT])); |
|
112 |
by Safe_tac; |
|
113 |
by( rtac widen.null 2); |
|
8082 | 114 |
by(eatac rtrancl_trans 1 1); |
115 |
qed_spec_mp "widen_trans"; |
|
8011 | 116 |
|
117 |
||
118 |
val prove_cast_lemma = prove_typerel_lemma [] cast.elim; |
|
119 |
||
9246 | 120 |
val cast_RefT = prove_typerel "G\\<turnstile>RefT R\\<preceq>? T \\<Longrightarrow> \\<exists>t. T=RefT t" |
8011 | 121 |
[prove_typerel_lemma [widen_RefT] cast.elim |
9246 | 122 |
"G\\<turnstile>S\\<preceq>? T \\<Longrightarrow> S=RefT R \\<longrightarrow> (\\<exists>t. T=RefT t)"]; |
8011 | 123 |
|
9246 | 124 |
val cast_RefT2 = prove_typerel "G\\<turnstile>S\\<preceq>? RefT R \\<Longrightarrow> \\<exists>t. S=RefT t" |
8011 | 125 |
[prove_typerel_lemma [widen_RefT2] cast.elim |
9246 | 126 |
"G\\<turnstile>S\\<preceq>? T \\<Longrightarrow> T=RefT R \\<longrightarrow> (\\<exists>t. S=RefT t)"]; |
8011 | 127 |
|
9246 | 128 |
val cast_PrimT2 = prove_typerel "G\\<turnstile>S\\<preceq>? PrimT pt \\<Longrightarrow> G\\<turnstile>S\\<preceq>PrimT pt" |
129 |
[prove_cast_lemma "G\\<turnstile>S\\<preceq>? T \\<Longrightarrow> T=PrimT pt \\<longrightarrow> G\\<turnstile>S\\<preceq>PrimT pt"]; |
|
8011 | 130 |