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 


14 
val prems = goal MT.thy

1461

15 
"[ c:Const; hastyenv(ve,te);<te,e_const(c),t>:ElabRel ] ==> \

915

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]

1461

23 
"[ x:ve_dom(ve); hastyenv(ve,te); <te,e_var(x),t>:ElabRel ] ==> \

915

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]

1461

31 
"[ ve:ValEnv; x:ExVar; e:Exp; hastyenv(ve,te); \


32 
\ <te,e_fn(x,e),t>:ElabRel \


33 
\ ] ==> \

915

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]

1461

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 ] ==> \

915

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

1461

100 
" [ ve:ValEnv; e1:Exp; e2:Exp; c1:Const; c2:Const; \


101 
\ <ve,e1,v_const(c1)>:EvalRel; \


102 
\ ALL t te. \

915

103 
\ hastyenv(ve,te) > <te,e1,t>:ElabRel > <v_const(c1),t>:HasTyRel; \

1461

104 
\ <ve, e2, v_const(c2)> : EvalRel; \


105 
\ ALL t te. \

915

106 
\ hastyenv(ve,te) > <te,e2,t>:ElabRel > <v_const(c2),t>:HasTyRel; \

1461

107 
\ hastyenv(ve, te); \


108 
\ <te,e_app(e1,e2),t>:ElabRel ] ==> \

915

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

1461

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 ] ==> \

915

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

1461

160 
"<ve,e,v>:EvalRel ==> \

915

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

1461

175 
"[ ve:ValEnv; te:TyEnv; \


176 
\ isofenv(ve,te); \


177 
\ <ve,e,v_const(c)>:EvalRel; \


178 
\ <te,e,t>:ElabRel \


179 
\ ] ==> \

915

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 
