|
1 (* Title: ZF/Coind/Types.ML |
|
2 ID: $Id$ |
|
3 Author: Jacob Frost, Cambridge University Computer Laboratory |
|
4 Copyright 1995 University of Cambridge |
|
5 *) |
|
6 |
|
7 open Types; |
|
8 |
|
9 val te_owrE = |
|
10 TyEnv.mk_cases TyEnv.con_defs "te_owr(te,f,t):TyEnv"; |
|
11 |
|
12 goalw Types.thy TyEnv.con_defs "rank(te) < rank(te_owr(te,x,t))"; |
|
13 by (simp_tac rank_ss 1); |
|
14 qed "rank_te_owr1"; |
|
15 |
|
16 goal Types.thy "te_rec(te_emp,c_te_emp,f_te_owr) = c_te_emp"; |
|
17 by (rtac (te_rec_def RS def_Vrec RS trans) 1); |
|
18 by (simp_tac (ZF_ss addsimps TyEnv.case_eqns) 1); |
|
19 qed "te_rec_emp"; |
|
20 |
|
21 goal Types.thy |
|
22 " te_rec(te_owr(te,x,t),c_te_emp,f_te_owr) = \ |
|
23 \ f_te_owr(te,x,t,te_rec(te,c_te_emp,f_te_owr))"; |
|
24 by (rtac (te_rec_def RS def_Vrec RS trans) 1); |
|
25 by (simp_tac (rank_ss addsimps (rank_te_owr1::TyEnv.case_eqns)) 1); |
|
26 qed "te_rec_owr"; |
|
27 |
|
28 goalw Types.thy [te_dom_def] "te_dom(te_emp) = 0"; |
|
29 by (simp_tac (ZF_ss addsimps [te_rec_emp]) 1); |
|
30 qed "te_dom_emp"; |
|
31 |
|
32 goalw Types.thy [te_dom_def] "te_dom(te_owr(te,x,v)) = te_dom(te) Un {x}"; |
|
33 by (simp_tac (ZF_ss addsimps [te_rec_owr]) 1); |
|
34 qed "te_dom_owr"; |
|
35 |
|
36 goalw Types.thy [te_app_def] "te_app(te_owr(te,x,t),x) = t"; |
|
37 by (simp_tac (ZF_ss addsimps [te_rec_owr]) 1); |
|
38 qed "te_app_owr1"; |
|
39 |
|
40 val prems = goalw Types.thy [te_app_def] |
|
41 "x ~= y ==> te_app(te_owr(te,x,t),y) = te_app(te,y)"; |
|
42 by (cut_facts_tac prems 1); |
|
43 by (asm_simp_tac (ZF_ss addsimps [te_rec_owr,(not_sym RS if_not_P)]) 1); |
|
44 qed "te_app_owr2"; |
|
45 |
|
46 val prems = goal Types.thy |
|
47 "[| te:TyEnv; x:ExVar; x:te_dom(te) |] ==> te_app(te,x):Ty"; |
|
48 by (cut_facts_tac prems 1); |
|
49 by (res_inst_tac [("P","x:te_dom(te)")] impE 1); |
|
50 by (assume_tac 2); |
|
51 by (assume_tac 2); |
|
52 by (etac TyEnv.induct 1); |
|
53 by (simp_tac (ZF_ss addsimps [te_dom_emp]) 1); |
|
54 by (rtac impI 1); |
|
55 by (rtac (excluded_middle RS disjE) 1); |
|
56 by (rtac (te_app_owr2 RS ssubst) 1); |
|
57 by (assume_tac 1); |
|
58 by (asm_full_simp_tac (ZF_ss addsimps [te_dom_owr]) 1); |
|
59 by (fast_tac ZF_cs 1); |
|
60 by (asm_simp_tac (ZF_ss addsimps [te_app_owr1]) 1); |
|
61 qed "te_appI"; |
|
62 |
|
63 |
|
64 |
|
65 |
|
66 |
|
67 |
|
68 |
|
69 |
|
70 |
|
71 |
|
72 |
|
73 |
|
74 |
|
75 |
|
76 |
|
77 |
|
78 |
|
79 |