|
1 (* Title: ZF/Coind/ECR.ML |
|
2 ID: $Id$ |
|
3 Author: Jacob Frost, Cambridge University Computer Laboratory |
|
4 Copyright 1995 University of Cambridge |
|
5 *) |
|
6 |
|
7 open Dynamic ECR; |
|
8 |
|
9 (* Specialised co-induction rule *) |
|
10 |
|
11 goal ECR.thy |
|
12 "!!x.[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv; \ |
|
13 \ <te, e_fn(x, e), t>:ElabRel; ve_dom(ve) = te_dom(te); \ |
|
14 \ {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}: \ |
|
15 \ Pow({<v_clos(x,e,ve),t>} Un HasTyRel) |] ==> \ |
|
16 \ <v_clos(x, e, ve),t>:HasTyRel"; |
|
17 by (rtac HasTyRel.coinduct 1); |
|
18 by (rtac singletonI 1); |
|
19 by (fast_tac (ZF_cs addIs Val_ValEnv.intrs) 1); |
|
20 by (rtac disjI2 1); |
|
21 by (etac singletonE 1); |
|
22 by (REPEAT_FIRST (resolve_tac [conjI,exI])); |
|
23 by (REPEAT (atac 1)); |
|
24 qed "htr_closCI"; |
|
25 |
|
26 (* Specialised elimination rules *) |
|
27 |
|
28 val htr_constE = |
|
29 (HasTyRel.mk_cases Val_ValEnv.con_defs "<v_const(c),t>:HasTyRel"); |
|
30 |
|
31 val htr_closE = |
|
32 (HasTyRel.mk_cases Val_ValEnv.con_defs "<v_clos(x,e,ve),t>:HasTyRel"); |
|
33 |
|
34 (* Classical reasoning sets *) |
|
35 |
|
36 fun mk_htr_cs cs = |
|
37 let open HasTyRel in |
|
38 ( cs |
|
39 addSIs [htr_constI] |
|
40 addSEs [htr_constE] |
|
41 addIs [htr_closI,htr_closCI] |
|
42 addEs [htr_closE]) |
|
43 end; |
|
44 |
|
45 val htr_cs = mk_htr_cs(static_cs); |
|
46 |
|
47 (* Properties of the pointwise extension to environments *) |
|
48 |
|
49 goalw ECR.thy [hastyenv_def] |
|
50 "!!ve.[| ve:ValEnv; te:TyEnv; hastyenv(ve,te); <v,t>:HasTyRel |] ==> \ |
|
51 \ hastyenv(ve_owr(ve,x,v),te_owr(te,x,t))"; |
|
52 by (safe_tac ZF_cs); |
|
53 by (rtac (ve_dom_owr RS ssubst) 1); |
|
54 by (assume_tac 1); |
|
55 by (etac (HasTyRel.dom_subset RS subsetD RS SigmaD1 RS ValNEE) 1); |
|
56 by (rtac (te_dom_owr RS ssubst) 1); |
|
57 by (asm_simp_tac ZF_ss 1); |
|
58 by (rtac (excluded_middle RS disjE) 1); |
|
59 by (rtac (ve_app_owr2 RS ssubst) 1); |
|
60 by (assume_tac 1); |
|
61 by (assume_tac 1); |
|
62 by (rtac (te_app_owr2 RS ssubst) 1); |
|
63 by (assume_tac 1); |
|
64 by (dtac (ve_dom_owr RS subst) 1); |
|
65 by (etac (HasTyRel.dom_subset RS subsetD RS SigmaD1 RS ValNEE) 1); |
|
66 by ((fast_tac ZF_cs 1) THEN (fast_tac ZF_cs 1)); |
|
67 by (asm_simp_tac (ZF_ss addsimps [ve_app_owr1,te_app_owr1]) 1); |
|
68 qed "hastyenv_owr"; |
|
69 |
|
70 goalw ECR.thy [isofenv_def,hastyenv_def] |
|
71 "!!ve.[| ve:ValEnv; te:TyEnv; isofenv(ve,te) |] ==> hastyenv(ve,te)"; |
|
72 by (safe_tac ZF_cs); |
|
73 by (dtac bspec 1); |
|
74 by (assume_tac 1); |
|
75 by (safe_tac ZF_cs); |
|
76 by (dtac HasTyRel.htr_constI 1); |
|
77 by (assume_tac 2); |
|
78 by (etac te_appI 1); |
|
79 by (etac ve_domI 1); |
|
80 by (ALLGOALS (asm_full_simp_tac ZF_ss)); |
|
81 qed "basic_consistency_lem"; |
|
82 |
|
83 |
|
84 |