author | paulson |
Tue, 22 Sep 1998 13:50:57 +0200 | |
changeset 5529 | 4a54acae6a15 |
parent 5268 | 59ef39008514 |
child 6046 | 2c8a8be36c94 |
permissions | -rw-r--r-- |
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 |
||
5068 | 12 |
Goalw TyEnv.con_defs "rank(te) < rank(te_owr(te,x,t))"; |
916 | 13 |
by (simp_tac rank_ss 1); |
14 |
qed "rank_te_owr1"; |
|
15 |
||
5068 | 16 |
Goal "te_rec(te_emp,c_te_emp,f_te_owr) = c_te_emp"; |
916 | 17 |
by (rtac (te_rec_def RS def_Vrec RS trans) 1); |
5529 | 18 |
by (simp_tac (simpset() addsimps rank_te_owr1::TyEnv.case_eqns) 1); |
916 | 19 |
qed "te_rec_emp"; |
20 |
||
5268 | 21 |
Goal " te_rec(te_owr(te,x,t),c_te_emp,f_te_owr) = \ |
916 | 22 |
\ f_te_owr(te,x,t,te_rec(te,c_te_emp,f_te_owr))"; |
23 |
by (rtac (te_rec_def RS def_Vrec RS trans) 1); |
|
5529 | 24 |
by (simp_tac (rank_ss addsimps rank_te_owr1::TyEnv.case_eqns) 1); |
916 | 25 |
qed "te_rec_owr"; |
26 |
||
5068 | 27 |
Goalw [te_dom_def] "te_dom(te_emp) = 0"; |
4091 | 28 |
by (simp_tac (simpset() addsimps [te_rec_emp]) 1); |
916 | 29 |
qed "te_dom_emp"; |
30 |
||
5068 | 31 |
Goalw [te_dom_def] "te_dom(te_owr(te,x,v)) = te_dom(te) Un {x}"; |
4091 | 32 |
by (simp_tac (simpset() addsimps [te_rec_owr]) 1); |
916 | 33 |
qed "te_dom_owr"; |
34 |
||
5068 | 35 |
Goalw [te_app_def] "te_app(te_owr(te,x,t),x) = t"; |
4091 | 36 |
by (simp_tac (simpset() addsimps [te_rec_owr]) 1); |
916 | 37 |
qed "te_app_owr1"; |
38 |
||
5068 | 39 |
Goalw [te_app_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5068
diff
changeset
|
40 |
"x ~= y ==> te_app(te_owr(te,x,t),y) = te_app(te,y)"; |
4091 | 41 |
by (asm_simp_tac (simpset() addsimps [te_rec_owr,(not_sym RS if_not_P)]) 1); |
916 | 42 |
qed "te_app_owr2"; |
43 |
||
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5068
diff
changeset
|
44 |
Goal "[| te:TyEnv; x:ExVar; x:te_dom(te) |] ==> te_app(te,x):Ty"; |
916 | 45 |
by (res_inst_tac [("P","x:te_dom(te)")] impE 1); |
46 |
by (assume_tac 2); |
|
47 |
by (assume_tac 2); |
|
48 |
by (etac TyEnv.induct 1); |
|
4091 | 49 |
by (simp_tac (simpset() addsimps [te_dom_emp]) 1); |
916 | 50 |
by (rtac impI 1); |
51 |
by (rtac (excluded_middle RS disjE) 1); |
|
2034 | 52 |
by (stac te_app_owr2 1); |
916 | 53 |
by (assume_tac 1); |
4091 | 54 |
by (asm_full_simp_tac (simpset() addsimps [te_dom_owr]) 1); |
2469 | 55 |
by (Fast_tac 1); |
4091 | 56 |
by (asm_simp_tac (simpset() addsimps [te_app_owr1]) 1); |
916 | 57 |
qed "te_appI"; |
58 |
||
59 |
||
60 |
||
61 |
||
62 |
||
63 |
||
64 |
||
65 |
||
66 |
||
67 |
||
68 |
||
69 |
||
70 |
||
71 |
||
72 |
||
73 |
||
74 |
||
75 |