author | paulson |
Tue, 19 Jan 1999 11:18:11 +0100 | |
changeset 6141 | a6922171b396 |
parent 6046 | 2c8a8be36c94 |
child 6154 | 6a00a5baef2b |
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 |
(* ############################################################ *) |
|
8 |
(* The Consistency theorem *) |
|
9 |
(* ############################################################ *) |
|
10 |
||
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5068
diff
changeset
|
11 |
Goal "[| c:Const; hastyenv(ve,te);<te,e_const(c),t>:ElabRel |] ==> \ |
2469 | 12 |
\ <v_const(c), t> : HasTyRel"; |
13 |
by (Fast_tac 1); |
|
915 | 14 |
qed "consistency_const"; |
15 |
||
16 |
||
5068 | 17 |
Goalw [hastyenv_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5068
diff
changeset
|
18 |
"[| x:ve_dom(ve); hastyenv(ve,te); <te,e_var(x),t>:ElabRel |] ==> \ |
915 | 19 |
\ <ve_app(ve,x),t>:HasTyRel"; |
2469 | 20 |
by (Fast_tac 1); |
915 | 21 |
qed "consistency_var"; |
22 |
||
23 |
||
5068 | 24 |
Goalw [hastyenv_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5068
diff
changeset
|
25 |
"[| ve:ValEnv; x:ExVar; e:Exp; hastyenv(ve,te); \ |
2469 | 26 |
\ <te,e_fn(x,e),t>:ElabRel \ |
27 |
\ |] ==> <v_clos(x, e, ve), t> : HasTyRel"; |
|
6046 | 28 |
by (Blast_tac 1); |
915 | 29 |
qed "consistency_fn"; |
30 |
||
2469 | 31 |
AddIs (Ty.intrs@TyEnv.intrs@Val_ValEnv.intrs); |
32 |
AddDs [te_owrE,(ElabRel.dom_subset RS subsetD)]; |
|
915 | 33 |
|
6046 | 34 |
Addsimps [ve_dom_owr, ve_app_owr1, ve_app_owr2, |
2493 | 35 |
te_app_owr1, te_app_owr2]; |
915 | 36 |
|
37 |
val clean_tac = |
|
38 |
REPEAT_FIRST (fn i => |
|
39 |
(eq_assume_tac i) ORELSE |
|
40 |
(match_tac (Ty.intrs@TyEnv.intrs@Val_ValEnv.intrs) i) ORELSE |
|
41 |
(ematch_tac [te_owrE] i)); |
|
42 |
||
6046 | 43 |
Goalw [hastyenv_def] |
1461 | 44 |
"[| ve:ValEnv; x:ExVar; e:Exp; f:ExVar; cl:Val; \ |
45 |
\ v_clos(x,e,ve_owr(ve,f,cl)) = cl; \ |
|
46 |
\ hastyenv(ve,te); <te,e_fix(f,x,e),t>:ElabRel |] ==> \ |
|
915 | 47 |
\ <cl,t>:HasTyRel"; |
48 |
by (etac elab_fixE 1); |
|
4152 | 49 |
by Safe_tac; |
915 | 50 |
by (EVERY [forward_tac [subst] 1,atac 2,rtac htr_closCI 1]); |
51 |
by clean_tac; |
|
52 |
by (rtac ve_owrI 1); |
|
53 |
by clean_tac; |
|
54 |
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
|
55 |
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
|
56 |
(SigmaD1 RS te_owrE) 1); |
915 | 57 |
by (assume_tac 1); |
6141 | 58 |
by (rtac ElabRel.fnI 1); |
915 | 59 |
by clean_tac; |
2469 | 60 |
by (Asm_simp_tac 1); |
2034 | 61 |
by (stac ve_dom_owr 1); |
915 | 62 |
by (assume_tac 1); |
63 |
by (etac subst 1); |
|
64 |
by (rtac v_closNE 1); |
|
2469 | 65 |
by (Asm_simp_tac 1); |
915 | 66 |
|
67 |
by (rtac PowI 1); |
|
2034 | 68 |
by (stac ve_dom_owr 1); |
915 | 69 |
by (assume_tac 1); |
70 |
by (etac subst 1); |
|
71 |
by (rtac v_closNE 1); |
|
72 |
by (rtac subsetI 1); |
|
73 |
by (etac RepFunE 1); |
|
2469 | 74 |
by (excluded_middle_tac "f=y" 1); |
2885
8d229dc0cfe2
Two extra commands shorten the proof time by 800 seconds...
paulson
parents:
2493
diff
changeset
|
75 |
by (rtac UnI1 2); |
8d229dc0cfe2
Two extra commands shorten the proof time by 800 seconds...
paulson
parents:
2493
diff
changeset
|
76 |
by (rtac UnI2 1); |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4152
diff
changeset
|
77 |
by Auto_tac; |
915 | 78 |
qed "consistency_fix"; |
79 |
||
80 |
||
6141 | 81 |
Goal "[| ve:ValEnv; e1:Exp; e2:Exp; c1:Const; c2:Const; \ |
1461 | 82 |
\ <ve,e1,v_const(c1)>:EvalRel; \ |
83 |
\ ALL t te. \ |
|
915 | 84 |
\ hastyenv(ve,te) --> <te,e1,t>:ElabRel --> <v_const(c1),t>:HasTyRel; \ |
1461 | 85 |
\ <ve, e2, v_const(c2)> : EvalRel; \ |
86 |
\ ALL t te. \ |
|
915 | 87 |
\ hastyenv(ve,te) --> <te,e2,t>:ElabRel --> <v_const(c2),t>:HasTyRel; \ |
1461 | 88 |
\ hastyenv(ve, te); \ |
89 |
\ <te,e_app(e1,e2),t>:ElabRel |] ==> \ |
|
915 | 90 |
\ <v_const(c_app(c1, c2)),t>:HasTyRel"; |
91 |
by (etac elab_appE 1); |
|
92 |
by (fast_tac ((mk_htr_cs ZF_cs) addSIs [c_appI] addIs [isof_app]) 1); |
|
93 |
qed "consistency_app1"; |
|
94 |
||
6141 | 95 |
Goal "[| ve:ValEnv; vem:ValEnv; e1:Exp; e2:Exp; em:Exp; xm:ExVar; v:Val; \ |
96 |
\ <ve,e1,v_clos(xm,em,vem)>:EvalRel; \ |
|
97 |
\ ALL t te. \ |
|
98 |
\ hastyenv(ve,te) --> \ |
|
99 |
\ <te,e1,t>:ElabRel --> \ |
|
100 |
\ <v_clos(xm,em,vem),t>:HasTyRel; \ |
|
101 |
\ <ve,e2,v2>:EvalRel; \ |
|
102 |
\ ALL t te. \ |
|
103 |
\ hastyenv(ve,te) --> \ |
|
104 |
\ <te,e2,t>:ElabRel --> \ |
|
105 |
\ <v2,t>:HasTyRel; \ |
|
106 |
\ <ve_owr(vem,xm,v2),em,v>:EvalRel; \ |
|
107 |
\ ALL t te. \ |
|
108 |
\ hastyenv(ve_owr(vem,xm,v2),te) --> \ |
|
109 |
\ <te,em,t>:ElabRel --> \ |
|
110 |
\ <v,t>:HasTyRel; \ |
|
111 |
\ hastyenv(ve,te); <te,e_app(e1,e2),t>:ElabRel |] ==> \ |
|
112 |
\ <v,t>:HasTyRel "; |
|
915 | 113 |
by (etac elab_appE 1); |
114 |
by (dtac (spec RS spec RS mp RS mp) 1); |
|
115 |
by (assume_tac 1); |
|
116 |
by (assume_tac 1); |
|
117 |
by (dtac (spec RS spec RS mp RS mp) 1); |
|
118 |
by (assume_tac 1); |
|
119 |
by (assume_tac 1); |
|
120 |
by (etac htr_closE 1); |
|
121 |
by (etac elab_fnE 1); |
|
6141 | 122 |
by (Full_simp_tac 1); |
123 |
by (Clarify_tac 1); |
|
915 | 124 |
by (dtac (spec RS spec RS mp RS mp) 1); |
125 |
by (assume_tac 3); |
|
126 |
by (assume_tac 2); |
|
127 |
by (rtac hastyenv_owr 1); |
|
128 |
by (assume_tac 1); |
|
129 |
by (assume_tac 1); |
|
130 |
by (assume_tac 2); |
|
6141 | 131 |
by (asm_simp_tac (simpset() addsimps [hastyenv_def]) 1); |
2469 | 132 |
by (Fast_tac 1); |
915 | 133 |
qed "consistency_app2"; |
134 |
||
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5068
diff
changeset
|
135 |
Goal "<ve,e,v>:EvalRel ==> \ |
1740 | 136 |
\ (ALL t te. hastyenv(ve,te) --> <te,e,t>:ElabRel --> <v,t>:HasTyRel)"; |
137 |
by (etac EvalRel.induct 1); |
|
6141 | 138 |
by (blast_tac (claset() addIs [consistency_app2]) 6); |
139 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [consistency_const, consistency_var, consistency_fn, consistency_fix, consistency_app1]))); |
|
915 | 140 |
qed "consistency"; |
141 |
||
142 |
||
6141 | 143 |
Goal "[| ve:ValEnv; te:TyEnv; \ |
144 |
\ isofenv(ve,te); \ |
|
145 |
\ <ve,e,v_const(c)>:EvalRel; \ |
|
146 |
\ <te,e,t>:ElabRel \ |
|
147 |
\ |] ==> isof(c,t)"; |
|
148 |
by (rtac htr_constE 1); |
|
915 | 149 |
by (dtac consistency 1); |
4091 | 150 |
by (fast_tac (claset() addSIs [basic_consistency_lem]) 1); |
915 | 151 |
by (assume_tac 1); |
152 |
qed "basic_consistency"; |