3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 2000 TUM |
4 Copyright 2000 TUM |
5 *) |
5 *) |
6 |
6 |
7 Goalw [lesub_def,subtype_def] "T [=_S T"; |
7 Goalw [lesub_def,subtype_def] "T [=_S T"; |
8 by(Simp_tac 1); |
8 by (Simp_tac 1); |
9 qed "subtype_refl"; |
9 qed "subtype_refl"; |
10 AddIffs [subtype_refl]; |
10 AddIffs [subtype_refl]; |
11 |
11 |
12 Goalw [lesub_def,subtype_def,is_Class_def] |
12 Goalw [lesub_def,subtype_def,is_Class_def] |
13 "(T [=_S Integer) = (T = Integer)"; |
13 "(T [=_S Integer) = (T = Integer)"; |
14 by(Simp_tac 1); |
14 by (Simp_tac 1); |
15 qed "subtype_Int_conv"; |
15 qed "subtype_Int_conv"; |
16 |
16 |
17 Goalw [lesub_def,subtype_def] "(Integer [=_S T) = (T = Integer)"; |
17 Goalw [lesub_def,subtype_def] "(Integer [=_S T) = (T = Integer)"; |
18 by(Blast_tac 1); |
18 by (Blast_tac 1); |
19 qed "Int_subtype_conv"; |
19 qed "Int_subtype_conv"; |
20 |
20 |
21 Goalw [lesub_def,subtype_def,is_Class_def] |
21 Goalw [lesub_def,subtype_def,is_Class_def] |
22 "(T [=_S Void) = (T = Void)"; |
22 "(T [=_S Void) = (T = Void)"; |
23 by(Simp_tac 1); |
23 by (Simp_tac 1); |
24 qed "subtype_Void_conv"; |
24 qed "subtype_Void_conv"; |
25 |
25 |
26 Goalw [lesub_def,subtype_def] "(Void [=_S T) = (T = Void)"; |
26 Goalw [lesub_def,subtype_def] "(Void [=_S T) = (T = Void)"; |
27 by(Blast_tac 1); |
27 by (Blast_tac 1); |
28 qed "Void_subtype_conv"; |
28 qed "Void_subtype_conv"; |
29 |
29 |
30 AddIffs [subtype_Int_conv,Int_subtype_conv, |
30 AddIffs [subtype_Int_conv,Int_subtype_conv, |
31 subtype_Void_conv,Void_subtype_conv]; |
31 subtype_Void_conv,Void_subtype_conv]; |
32 |
32 |
33 Goalw [lesub_def,subtype_def,is_Class_def] |
33 Goalw [lesub_def,subtype_def,is_Class_def] |
34 "T [=_S NullT = (T=NullT)"; |
34 "T [=_S NullT = (T=NullT)"; |
35 by(Simp_tac 1); |
35 by (Simp_tac 1); |
36 qed "subtype_NullT_conv"; |
36 qed "subtype_NullT_conv"; |
37 |
37 |
38 Goalw [lesub_def,subtype_def,is_Class_def] |
38 Goalw [lesub_def,subtype_def,is_Class_def] |
39 "NullT [=_S T = (T=NullT | (? C. T = Class C))"; |
39 "NullT [=_S T = (T=NullT | (? C. T = Class C))"; |
40 by(simp_tac (simpset() addsplits [ty.split]) 1); |
40 by (simp_tac (simpset() addsplits [ty.split]) 1); |
41 qed "NullT_subtype_conv"; |
41 qed "NullT_subtype_conv"; |
42 |
42 |
43 AddIffs [NullT_subtype_conv,subtype_NullT_conv]; |
43 AddIffs [NullT_subtype_conv,subtype_NullT_conv]; |
44 |
44 |
45 Goalw [lesub_def,subtype_def,is_Class_def] |
45 Goalw [lesub_def,subtype_def,is_Class_def] |
46 "T [=_S Class C = (T=NullT | (? D. T = Class D & (D,C) : S^*))"; |
46 "T [=_S Class C = (T=NullT | (? D. T = Class D & (D,C) : S^*))"; |
47 by(Simp_tac 1); |
47 by (Simp_tac 1); |
48 by(Blast_tac 1); |
48 by (Blast_tac 1); |
49 qed "subtype_Class_conv"; |
49 qed "subtype_Class_conv"; |
50 |
50 |
51 Goalw [lesub_def,subtype_def,refl_def] |
51 Goalw [lesub_def,subtype_def,refl_def] |
52 "Class D [=_S T = (? C. T = Class C & (D,C):S^*)"; |
52 "Class D [=_S T = (? C. T = Class C & (D,C):S^*)"; |
53 by(Blast_tac 1); |
53 by (Blast_tac 1); |
54 qed "Class_subtype_conv"; |
54 qed "Class_subtype_conv"; |
55 |
55 |
56 AddIffs [Class_subtype_conv,subtype_Class_conv]; |
56 AddIffs [Class_subtype_conv,subtype_Class_conv]; |
57 |
57 |
58 Goalw [lesub_def,subtype_def,is_Class_def] |
58 Goalw [lesub_def,subtype_def,is_Class_def] |
59 "[| A [=_S B; B [=_S C |] ==> A [=_S C"; |
59 "[| A [=_S B; B [=_S C |] ==> A [=_S C"; |
60 by(asm_full_simp_tac (simpset() addsplits [ty.split,ty.split_asm]) 1); |
60 by (asm_full_simp_tac (simpset() addsplits [ty.split,ty.split_asm]) 1); |
61 by(blast_tac (claset() addDs [transD] addIs [rtrancl_trans]) 1); |
61 by (blast_tac (claset() addDs [transD] addIs [rtrancl_trans]) 1); |
62 qed "subtype_transD"; |
62 qed "subtype_transD"; |
63 |
63 |
64 Goalw [order_def,subtype_def,lesub_def,is_Class_def] |
64 Goalw [order_def,subtype_def,lesub_def,is_Class_def] |
65 "acyclic S ==> order (subtype S)"; |
65 "acyclic S ==> order (subtype S)"; |
66 bd acyclic_impl_antisym_rtrancl 1; |
66 by (dtac acyclic_impl_antisym_rtrancl 1); |
67 by(auto_tac (claset() addIs [rtrancl_trans],simpset() addsimps [antisymD]) ); |
67 by (auto_tac (claset() addIs [rtrancl_trans],simpset() addsimps [antisymD]) ); |
68 qed "acyclic_impl_order_subtype"; |
68 qed "acyclic_impl_order_subtype"; |
69 |
69 |
70 Goalw [acc_def,lesssub_def] |
70 Goalw [acc_def,lesssub_def] |
71 "wf(S^-1) ==> acc(subtype S)"; |
71 "wf(S^-1) ==> acc(subtype S)"; |
72 by(dres_inst_tac [("p","S^-1 - Id")] wf_subset 1); |
72 by (dres_inst_tac [("p","S^-1 - Id")] wf_subset 1); |
73 by(Blast_tac 1); |
73 by (Blast_tac 1); |
74 bd wf_trancl 1; |
74 by (dtac wf_trancl 1); |
75 by (asm_full_simp_tac (simpset() addsimps [wf_eq_minimal]) 1); |
75 by (asm_full_simp_tac (simpset() addsimps [wf_eq_minimal]) 1); |
76 by (Clarify_tac 1); |
76 by (Clarify_tac 1); |
77 by(rename_tac "M T" 1); |
77 by (rename_tac "M T" 1); |
78 by(case_tac "EX C. Class C : M" 1); |
78 by (case_tac "EX C. Class C : M" 1); |
79 by(case_tac "T" 2); |
79 by (case_tac "T" 2); |
80 by(Blast_tac 2); |
80 by (Blast_tac 2); |
81 by(Blast_tac 2); |
81 by (Blast_tac 2); |
82 by(res_inst_tac [("x","T")] bexI 2); |
82 by (res_inst_tac [("x","T")] bexI 2); |
83 by(Blast_tac 2); |
83 by (Blast_tac 2); |
84 ba 2; |
84 by (assume_tac 2); |
85 by(Blast_tac 2); |
85 by (Blast_tac 2); |
86 by(eres_inst_tac [("x","{C. Class C : M}")] allE 1); |
86 by (eres_inst_tac [("x","{C. Class C : M}")] allE 1); |
87 by(Auto_tac); |
87 by (Auto_tac); |
88 by(rename_tac "D" 1); |
88 by (rename_tac "D" 1); |
89 by(res_inst_tac [("x","Class D")] bexI 1); |
89 by (res_inst_tac [("x","Class D")] bexI 1); |
90 by(atac 2); |
90 by (atac 2); |
91 by (Clarify_tac 1); |
91 by (Clarify_tac 1); |
92 by(cut_inst_tac [("r","S")] (standard(rtrancl_r_diff_Id RS sym)) 1); |
92 by (cut_inst_tac [("r","S")] (standard(rtrancl_r_diff_Id RS sym)) 1); |
93 by(Asm_full_simp_tac 1); |
93 by (Asm_full_simp_tac 1); |
94 be rtranclE 1; |
94 by (etac rtranclE 1); |
95 by(Blast_tac 1); |
95 by (Blast_tac 1); |
96 bd (converseI RS rtrancl_converseI) 1; |
96 by (dtac rtrancl_converseI 1); |
97 by(subgoal_tac "(S-Id)^-1 = (S^-1 - Id)" 1); |
97 by (subgoal_tac "(S-Id)^-1 = (S^-1 - Id)" 1); |
98 by(Blast_tac 2); |
98 by (Blast_tac 2); |
99 by(Asm_full_simp_tac 1); |
99 by (Asm_full_simp_tac 1); |
100 by(blast_tac (claset() addIs [rtrancl_into_trancl2]) 1); |
100 by (blast_tac (claset() addIs [rtrancl_into_trancl2]) 1); |
101 qed "wf_converse_subcls1_impl_acc_subtype"; |
101 qed "wf_converse_subcls1_impl_acc_subtype"; |
102 |
102 |
103 Addsimps [is_type_def]; |
103 Addsimps [is_type_def]; |
104 |
104 |
105 Goalw [closed_def,plussub_def,lift2_def,err_def,JType.sup_def] |
105 Goalw [closed_def,plussub_def,lift2_def,err_def,JType.sup_def] |
106 "[| univalent S; acyclic S |] ==> \ |
106 "[| univalent S; acyclic S |] ==> \ |
107 \ closed (err(types S)) (lift2 (JType.sup S))"; |
107 \ closed (err(types S)) (lift2 (JType.sup S))"; |
108 by(simp_tac (simpset() addsplits [err.split,ty.split]) 1); |
108 by (simp_tac (simpset() addsplits [err.split,ty.split]) 1); |
109 by(blast_tac (claset() addSDs [is_lub_some_lub,is_lubD,is_ubD] |
109 by (blast_tac (claset() addSDs [is_lub_some_lub,is_lubD,is_ubD] |
110 addSIs [is_ubI]) 1); |
110 addSIs [is_ubI]) 1); |
111 qed "closed_err_types"; |
111 qed "closed_err_types"; |
112 |
112 |
113 AddIffs [OK_le_conv]; |
113 AddIffs [OK_le_conv]; |
114 |
114 |
115 Goalw [semilat_def,split RS eq_reflection,JType.esl_def,Err.sl_def] |
115 Goalw [semilat_def,split RS eq_reflection,JType.esl_def,Err.sl_def] |
116 "[| univalent S; acyclic S |] ==> err_semilat (JType.esl S)"; |
116 "[| univalent S; acyclic S |] ==> err_semilat (JType.esl S)"; |
117 by(asm_full_simp_tac (simpset() addsimps [acyclic_impl_order_subtype,closed_err_types]) 1); |
117 by (asm_full_simp_tac (simpset() addsimps [acyclic_impl_order_subtype,closed_err_types]) 1); |
118 |
118 |
119 br conjI 1; |
119 by (rtac conjI 1); |
120 by(Clarify_tac 1); |
120 by (Clarify_tac 1); |
121 by(case_tac "x" 1); |
121 by (case_tac "x" 1); |
122 by(Clarify_tac 1); |
122 by (Clarify_tac 1); |
123 by(Simp_tac 1); |
123 by (Simp_tac 1); |
124 by(case_tac "y" 1); |
124 by (case_tac "y" 1); |
125 by(Clarify_tac 1); |
125 by (Clarify_tac 1); |
126 by(Simp_tac 1); |
126 by (Simp_tac 1); |
127 by(fast_tac (claset() addDs [is_lub_some_lub,is_lubD,is_ubD] addss |
127 by (fast_tac (claset() addDs [is_lub_some_lub,is_lubD,is_ubD] addss |
128 (simpset() addsimps [plussub_def,lift2_def,JType.sup_def] |
128 (simpset() addsimps [plussub_def,lift2_def,JType.sup_def] |
129 addsplits [ty.split])) 1); |
129 addsplits [ty.split])) 1); |
130 |
130 |
131 br conjI 1; |
131 by (rtac conjI 1); |
132 by(Clarify_tac 1); |
132 by (Clarify_tac 1); |
133 by(case_tac "x" 1); |
133 by (case_tac "x" 1); |
134 by(Clarify_tac 1); |
134 by (Clarify_tac 1); |
135 by(Simp_tac 1); |
135 by (Simp_tac 1); |
136 by(case_tac "y" 1); |
136 by (case_tac "y" 1); |
137 by(Clarify_tac 1); |
137 by (Clarify_tac 1); |
138 by(Simp_tac 1); |
138 by (Simp_tac 1); |
139 by(fast_tac (claset() addDs [is_lub_some_lub,is_lubD,is_ubD] addss |
139 by (fast_tac (claset() addDs [is_lub_some_lub,is_lubD,is_ubD] addss |
140 (simpset() addsimps [plussub_def,lift2_def,JType.sup_def] |
140 (simpset() addsimps [plussub_def,lift2_def,JType.sup_def] |
141 addsplits [ty.split])) 1); |
141 addsplits [ty.split])) 1); |
142 |
142 |
143 by(Clarify_tac 1); |
143 by (Clarify_tac 1); |
144 by(case_tac "x" 1); |
144 by (case_tac "x" 1); |
145 by(Clarify_tac 1); |
145 by (Clarify_tac 1); |
146 by(case_tac "y" 1); |
146 by (case_tac "y" 1); |
147 by(Clarify_tac 1); |
147 by (Clarify_tac 1); |
148 by(asm_simp_tac(simpset() addsimps [plussub_def,lift2_def,JType.sup_def] |
148 by (asm_simp_tac(simpset() addsimps [plussub_def,lift2_def,JType.sup_def] |
149 addsplits [ty.split]) 1); |
149 addsplits [ty.split]) 1); |
150 br conjI 1; |
150 by (rtac conjI 1); |
151 by(Blast_tac 1); |
151 by (Blast_tac 1); |
152 br conjI 1; |
152 by (rtac conjI 1); |
153 by(Blast_tac 1); |
153 by (Blast_tac 1); |
154 br conjI 1; |
154 by (rtac conjI 1); |
155 by(Blast_tac 1); |
155 by (Blast_tac 1); |
156 by(Clarify_tac 1); |
156 by (Clarify_tac 1); |
157 br conjI 1; |
157 by (rtac conjI 1); |
158 by(Clarify_tac 1); |
158 by (Clarify_tac 1); |
159 br conjI 1; |
159 by (rtac conjI 1); |
160 by(Clarify_tac 1); |
160 by (Clarify_tac 1); |
161 by(Asm_full_simp_tac 1); |
161 by (Asm_full_simp_tac 1); |
162 by(blast_tac (claset() addSDs [is_lub_some_lub,is_lubD,is_ubD] |
162 by (blast_tac (claset() addSDs [is_lub_some_lub,is_lubD,is_ubD] |
163 addSIs [is_ubI]) 1); |
163 addSIs [is_ubI]) 1); |
164 qed "err_semilat_JType_esl"; |
164 qed "err_semilat_JType_esl"; |
165 |
165 |
166 DelIffs [OK_le_conv]; |
166 DelIffs [OK_le_conv]; |