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