1461
|
1 |
(* Title: ZF/Coind/Types.ML
|
916
|
2 |
ID: $Id$
|
1461
|
3 |
Author: Jacob Frost, Cambridge University Computer Laboratory
|
916
|
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);
|
2469
|
18 |
by (simp_tac (!simpset addsimps (rank_te_owr1::TyEnv.case_eqns)) 1);
|
916
|
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";
|
2469
|
29 |
by (simp_tac (!simpset addsimps [te_rec_emp]) 1);
|
916
|
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}";
|
2469
|
33 |
by (simp_tac (!simpset addsimps [te_rec_owr]) 1);
|
916
|
34 |
qed "te_dom_owr";
|
|
35 |
|
|
36 |
goalw Types.thy [te_app_def] "te_app(te_owr(te,x,t),x) = t";
|
2469
|
37 |
by (simp_tac (!simpset addsimps [te_rec_owr]) 1);
|
916
|
38 |
qed "te_app_owr1";
|
|
39 |
|
2469
|
40 |
goalw Types.thy [te_app_def]
|
|
41 |
"!!x y. x ~= y ==> te_app(te_owr(te,x,t),y) = te_app(te,y)";
|
|
42 |
by (asm_simp_tac (!simpset addsimps [te_rec_owr,(not_sym RS if_not_P)]) 1);
|
916
|
43 |
qed "te_app_owr2";
|
|
44 |
|
2469
|
45 |
goal Types.thy
|
|
46 |
"!!te. [| te:TyEnv; x:ExVar; x:te_dom(te) |] ==> te_app(te,x):Ty";
|
916
|
47 |
by (res_inst_tac [("P","x:te_dom(te)")] impE 1);
|
|
48 |
by (assume_tac 2);
|
|
49 |
by (assume_tac 2);
|
|
50 |
by (etac TyEnv.induct 1);
|
2469
|
51 |
by (simp_tac (!simpset addsimps [te_dom_emp]) 1);
|
916
|
52 |
by (rtac impI 1);
|
|
53 |
by (rtac (excluded_middle RS disjE) 1);
|
2034
|
54 |
by (stac te_app_owr2 1);
|
916
|
55 |
by (assume_tac 1);
|
2469
|
56 |
by (asm_full_simp_tac (!simpset addsimps [te_dom_owr]) 1);
|
|
57 |
by (Fast_tac 1);
|
|
58 |
by (asm_simp_tac (!simpset addsimps [te_app_owr1]) 1);
|
916
|
59 |
qed "te_appI";
|
|
60 |
|
|
61 |
|
|
62 |
|
|
63 |
|
|
64 |
|
|
65 |
|
|
66 |
|
|
67 |
|
|
68 |
|
|
69 |
|
|
70 |
|
|
71 |
|
|
72 |
|
|
73 |
|
|
74 |
|
|
75 |
|
|
76 |
|
|
77 |
|