|
1 (* Title: ZF/Coind/MT.ML |
|
2 ID: $Id$ |
|
3 Author: Jacob Frost, Cambridge University Computer Laboratory |
|
4 Copyright 1995 University of Cambridge |
|
5 *) |
|
6 |
|
7 open MT; |
|
8 |
|
9 |
|
10 (* ############################################################ *) |
|
11 (* The Consistency theorem *) |
|
12 (* ############################################################ *) |
|
13 |
|
14 val prems = goal MT.thy |
|
15 "[| c:Const; hastyenv(ve,te);<te,e_const(c),t>:ElabRel |] ==> \ |
|
16 \ <v_const(c), t> : HasTyRel"; |
|
17 by (cut_facts_tac prems 1); |
|
18 by (fast_tac htr_cs 1); |
|
19 qed "consistency_const"; |
|
20 |
|
21 |
|
22 val prems = goalw MT.thy [hastyenv_def] |
|
23 "[| x:ve_dom(ve); hastyenv(ve,te); <te,e_var(x),t>:ElabRel |] ==> \ |
|
24 \ <ve_app(ve,x),t>:HasTyRel"; |
|
25 by (cut_facts_tac prems 1); |
|
26 by (fast_tac static_cs 1); |
|
27 qed "consistency_var"; |
|
28 |
|
29 |
|
30 val prems = goalw MT.thy [hastyenv_def] |
|
31 "[| ve:ValEnv; x:ExVar; e:Exp; hastyenv(ve,te); \ |
|
32 \ <te,e_fn(x,e),t>:ElabRel \ |
|
33 \ |] ==> \ |
|
34 \ <v_clos(x, e, ve), t> : HasTyRel"; |
|
35 by (cut_facts_tac prems 1); |
|
36 by (best_tac htr_cs 1); |
|
37 qed "consistency_fn"; |
|
38 |
|
39 val MT_cs = ZF_cs |
|
40 addIs (Ty.intrs@TyEnv.intrs@Val_ValEnv.intrs) |
|
41 addDs [te_owrE,(ElabRel.dom_subset RS subsetD)]; |
|
42 |
|
43 val MT_ss = |
|
44 ZF_ss addsimps |
|
45 [ve_dom_owr,te_dom_owr,ve_app_owr1,ve_app_owr2,te_app_owr1,te_app_owr2]; |
|
46 |
|
47 val clean_tac = |
|
48 REPEAT_FIRST (fn i => |
|
49 (eq_assume_tac i) ORELSE |
|
50 (match_tac (Ty.intrs@TyEnv.intrs@Val_ValEnv.intrs) i) ORELSE |
|
51 (ematch_tac [te_owrE] i)); |
|
52 |
|
53 val prems = goalw MT.thy [hastyenv_def] |
|
54 "[| ve:ValEnv; x:ExVar; e:Exp; f:ExVar; cl:Val; \ |
|
55 \ v_clos(x,e,ve_owr(ve,f,cl)) = cl; \ |
|
56 \ hastyenv(ve,te); <te,e_fix(f,x,e),t>:ElabRel |] ==> \ |
|
57 \ <cl,t>:HasTyRel"; |
|
58 by (cut_facts_tac prems 1); |
|
59 by (etac elab_fixE 1); |
|
60 by (safe_tac ZF_cs); |
|
61 by (EVERY [forward_tac [subst] 1,atac 2,rtac htr_closCI 1]); |
|
62 by clean_tac; |
|
63 by (rtac ve_owrI 1); |
|
64 by clean_tac; |
|
65 by (dtac (ElabRel.dom_subset RS subsetD) 1); |
|
66 by ( eres_inst_tac |
|
67 [("Q","te_owr(te,f,t_fun(t1,t2)):TyEnv")] |
|
68 (SigmaD1 RS te_owrE) 1 |
|
69 ); |
|
70 by (assume_tac 1); |
|
71 by (rtac ElabRel.elab_fnI 1); |
|
72 by clean_tac; |
|
73 by (asm_simp_tac MT_ss 1); |
|
74 by (rtac (ve_dom_owr RS ssubst) 1); |
|
75 by (assume_tac 1); |
|
76 by (etac subst 1); |
|
77 by (rtac v_closNE 1); |
|
78 by (asm_simp_tac ZF_ss 1); |
|
79 |
|
80 by (rtac PowI 1); |
|
81 by (rtac (ve_dom_owr RS ssubst) 1); |
|
82 by (assume_tac 1); |
|
83 by (etac subst 1); |
|
84 by (rtac v_closNE 1); |
|
85 by (rtac subsetI 1); |
|
86 by (etac RepFunE 1); |
|
87 by (dtac lem_fix 1); |
|
88 by (etac UnE' 1); |
|
89 by (rtac UnI1 1); |
|
90 by (etac singletonE 1); |
|
91 by (asm_full_simp_tac MT_ss 1); |
|
92 by (rtac UnI2 1); |
|
93 by (etac notsingletonE 1); |
|
94 by (dtac not_sym 1); |
|
95 by (asm_full_simp_tac MT_ss 1); |
|
96 qed "consistency_fix"; |
|
97 |
|
98 |
|
99 val prems = goal MT.thy |
|
100 " [| ve:ValEnv; e1:Exp; e2:Exp; c1:Const; c2:Const; \ |
|
101 \ <ve,e1,v_const(c1)>:EvalRel; \ |
|
102 \ ALL t te. \ |
|
103 \ hastyenv(ve,te) --> <te,e1,t>:ElabRel --> <v_const(c1),t>:HasTyRel; \ |
|
104 \ <ve, e2, v_const(c2)> : EvalRel; \ |
|
105 \ ALL t te. \ |
|
106 \ hastyenv(ve,te) --> <te,e2,t>:ElabRel --> <v_const(c2),t>:HasTyRel; \ |
|
107 \ hastyenv(ve, te); \ |
|
108 \ <te,e_app(e1,e2),t>:ElabRel |] ==> \ |
|
109 \ <v_const(c_app(c1, c2)),t>:HasTyRel"; |
|
110 by (cut_facts_tac prems 1); |
|
111 by (etac elab_appE 1); |
|
112 by (fast_tac ((mk_htr_cs ZF_cs) addSIs [c_appI] addIs [isof_app]) 1); |
|
113 qed "consistency_app1"; |
|
114 |
|
115 val prems = goal MT.thy |
|
116 " [| ve:ValEnv; vem:ValEnv; e1:Exp; e2:Exp; em:Exp; xm:ExVar; v:Val; \ |
|
117 \ <ve,e1,v_clos(xm,em,vem)>:EvalRel; \ |
|
118 \ ALL t te. \ |
|
119 \ hastyenv(ve,te) --> \ |
|
120 \ <te,e1,t>:ElabRel --> \ |
|
121 \ <v_clos(xm,em,vem),t>:HasTyRel; \ |
|
122 \ <ve,e2,v2>:EvalRel; \ |
|
123 \ ALL t te. \ |
|
124 \ hastyenv(ve,te) --> \ |
|
125 \ <te,e2,t>:ElabRel --> \ |
|
126 \ <v2,t>:HasTyRel; \ |
|
127 \ <ve_owr(vem,xm,v2),em,v>:EvalRel; \ |
|
128 \ ALL t te. \ |
|
129 \ hastyenv(ve_owr(vem,xm,v2),te) --> \ |
|
130 \ <te,em,t>:ElabRel --> \ |
|
131 \ <v,t>:HasTyRel; \ |
|
132 \ hastyenv(ve,te); <te,e_app(e1,e2),t>:ElabRel |] ==> \ |
|
133 \ <v,t>:HasTyRel "; |
|
134 by (cut_facts_tac prems 1); |
|
135 by (etac elab_appE 1); |
|
136 by (dtac (spec RS spec RS mp RS mp) 1); |
|
137 by (assume_tac 1); |
|
138 by (assume_tac 1); |
|
139 by (dtac (spec RS spec RS mp RS mp) 1); |
|
140 by (assume_tac 1); |
|
141 by (assume_tac 1); |
|
142 by (etac htr_closE 1); |
|
143 by (etac elab_fnE 1); |
|
144 by (rewrite_tac Ty.con_defs); |
|
145 by (safe_tac sum_cs); |
|
146 by (dtac (spec RS spec RS mp RS mp) 1); |
|
147 by (assume_tac 3); |
|
148 by (assume_tac 2); |
|
149 by (rtac hastyenv_owr 1); |
|
150 by (assume_tac 1); |
|
151 by (assume_tac 1); |
|
152 by (assume_tac 2); |
|
153 by (rewrite_tac [hastyenv_def]); |
|
154 by (fast_tac ZF_cs 1); |
|
155 qed "consistency_app2"; |
|
156 |
|
157 fun mt_cases_tac t = ((rtac t 1) THEN (TRYALL assume_tac)); |
|
158 |
|
159 val prems = goal MT.thy |
|
160 "<ve,e,v>:EvalRel ==> \ |
|
161 \ (ALL t te. hastyenv(ve,te) --> <te,e,t>:ElabRel --> <v,t>:HasTyRel)"; |
|
162 by (rtac (EvalRel.mutual_induct RS spec RS spec RS spec RS impE) 1); |
|
163 by (resolve_tac prems 7 THEN assume_tac 7); |
|
164 by (safe_tac ZF_cs); |
|
165 by (mt_cases_tac consistency_const); |
|
166 by (mt_cases_tac consistency_var); |
|
167 by (mt_cases_tac consistency_fn); |
|
168 by (mt_cases_tac consistency_fix); |
|
169 by (mt_cases_tac consistency_app1); |
|
170 by (mt_cases_tac consistency_app2); |
|
171 qed "consistency"; |
|
172 |
|
173 |
|
174 val prems = goal MT.thy |
|
175 "[| ve:ValEnv; te:TyEnv; \ |
|
176 \ isofenv(ve,te); \ |
|
177 \ <ve,e,v_const(c)>:EvalRel; \ |
|
178 \ <te,e,t>:ElabRel \ |
|
179 \ |] ==> \ |
|
180 \ isof(c,t)"; |
|
181 by (cut_facts_tac prems 1); |
|
182 by (rtac (htr_constE) 1); |
|
183 by (dtac consistency 1); |
|
184 by (fast_tac (ZF_cs addSIs [basic_consistency_lem]) 1); |
|
185 by (assume_tac 1); |
|
186 qed "basic_consistency"; |
|
187 |
|
188 |
|
189 |
|
190 |