72 AddSIs [widen.refl]; |
72 AddSIs [widen.refl]; |
73 Addsimps [widen.refl]; |
73 Addsimps [widen.refl]; |
74 |
74 |
75 val prove_widen_lemma = prove_typerel_lemma [] widen.elim; |
75 val prove_widen_lemma = prove_typerel_lemma [] widen.elim; |
76 |
76 |
77 val widen_PrimT_RefT = prove_typerel "G\\<turnstile>PrimT x\\<preceq>RefT tname \\<Longrightarrow> R" |
77 Goal "(G\\<turnstile>PrimT pT\\<preceq>RefT rT) = False"; |
78 [ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = PrimT x \\<longrightarrow> T = RefT tname \\<longrightarrow> R"]; |
78 br iffI 1; |
79 |
79 be widen.elim 1; |
|
80 by(Auto_tac); |
|
81 qed "widen_PrimT_RefT"; |
|
82 AddIffs [widen_PrimT_RefT]; |
80 |
83 |
81 val widen_RefT = prove_typerel "G\\<turnstile>RefT R\\<preceq>T \\<Longrightarrow> \\<exists>t. T=RefT t" |
84 val widen_RefT = prove_typerel "G\\<turnstile>RefT R\\<preceq>T \\<Longrightarrow> \\<exists>t. T=RefT t" |
82 [prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S=RefT R \\<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)"]; |
83 |
86 |
84 val widen_RefT2 = prove_typerel "G\\<turnstile>S\\<preceq>RefT R \\<Longrightarrow> \\<exists>t. S=RefT t" |
87 val widen_RefT2 = prove_typerel "G\\<turnstile>S\\<preceq>RefT R \\<Longrightarrow> \\<exists>t. S=RefT t" |
85 [prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> T=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)"]; |
86 |
89 |
87 val widen_Class = prove_typerel "G\\<turnstile>Class C\\<preceq>T \\<Longrightarrow> \\<exists>D. T=Class D" |
90 val widen_Class = prove_typerel "G\\<turnstile>Class C\\<preceq>T \\<Longrightarrow> \\<exists>D. T=Class D" |
88 [ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = Class C \\<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)"]; |
89 |
92 |
90 val widen_Class_RefT = prove_typerel |
93 Goal "(G\\<turnstile>Class C\\<preceq>RefT NullT) = False"; |
91 "G\\<turnstile>Class C\\<preceq>RefT t \\<Longrightarrow> (\\<exists>tname. t=ClassT tname)" |
94 br iffI 1; |
92 [prove_widen_lemma |
95 be widen.elim 1; |
93 "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S=Class C \\<longrightarrow> T=RefT t \\<longrightarrow> (\\<exists>tname. t=ClassT tname)"]; |
96 by(Auto_tac); |
|
97 qed "widen_Class_NullT"; |
|
98 AddIffs [widen_Class_NullT]; |
94 |
99 |
95 val widen_Class_NullT = prove_typerel "G\\<turnstile>Class C\\<preceq>RefT NullT \\<Longrightarrow> R" |
100 Goal "(G\\<turnstile>Class C\\<preceq> Class D) = (G\\<turnstile>C\\<preceq>C D)"; |
96 [prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S=Class C \\<longrightarrow> T=RefT NullT \\<longrightarrow> R"]; |
101 br iffI 1; |
97 |
102 be widen.elim 1; |
98 val widen_Class_Class = prove_typerel "G\\<turnstile>Class C\\<preceq> Class cm \\<Longrightarrow> G\\<turnstile>C\\<preceq>C cm" |
103 by(Auto_tac); |
99 [ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = Class C \\<longrightarrow> T = Class cm \\<longrightarrow> G\\<turnstile>C\\<preceq>C cm"]; |
104 bes widen.intrs 1; |
|
105 qed "widen_Class_Class"; |
|
106 AddIffs [widen_Class_Class]; |
100 |
107 |
101 Goal "G\\<turnstile>S\\<preceq>U \\<Longrightarrow> \\<forall>T. G\\<turnstile>U\\<preceq>T \\<longrightarrow> G\\<turnstile>S\\<preceq>T"; |
108 Goal "G\\<turnstile>S\\<preceq>U \\<Longrightarrow> \\<forall>T. G\\<turnstile>U\\<preceq>T \\<longrightarrow> G\\<turnstile>S\\<preceq>T"; |
102 by( etac widen.induct 1); |
109 by( etac widen.induct 1); |
103 by Safe_tac; |
110 by Safe_tac; |
104 by( ALLGOALS (forward_tac [widen_Class, widen_RefT])); |
111 by( ALLGOALS (forward_tac [widen_Class, widen_RefT])); |
105 by Safe_tac; |
112 by Safe_tac; |
106 by( rtac widen.null 2); |
113 by( rtac widen.null 2); |
107 by(dtac widen_Class_Class 1); |
|
108 by(rtac widen.subcls 1); |
|
109 by(eatac rtrancl_trans 1 1); |
114 by(eatac rtrancl_trans 1 1); |
110 qed_spec_mp "widen_trans"; |
115 qed_spec_mp "widen_trans"; |
111 |
116 |
112 |
117 |
113 val prove_cast_lemma = prove_typerel_lemma [] cast.elim; |
118 val prove_cast_lemma = prove_typerel_lemma [] cast.elim; |