7 open Types; |
7 open Types; |
8 |
8 |
9 val te_owrE = |
9 val te_owrE = |
10 TyEnv.mk_cases TyEnv.con_defs "te_owr(te,f,t):TyEnv"; |
10 TyEnv.mk_cases TyEnv.con_defs "te_owr(te,f,t):TyEnv"; |
11 |
11 |
12 goalw Types.thy TyEnv.con_defs "rank(te) < rank(te_owr(te,x,t))"; |
12 Goalw TyEnv.con_defs "rank(te) < rank(te_owr(te,x,t))"; |
13 by (simp_tac rank_ss 1); |
13 by (simp_tac rank_ss 1); |
14 qed "rank_te_owr1"; |
14 qed "rank_te_owr1"; |
15 |
15 |
16 goal Types.thy "te_rec(te_emp,c_te_emp,f_te_owr) = c_te_emp"; |
16 Goal "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); |
17 by (rtac (te_rec_def RS def_Vrec RS trans) 1); |
18 by (simp_tac (simpset() addsimps (rank_te_owr1::TyEnv.case_eqns)) 1); |
18 by (simp_tac (simpset() addsimps (rank_te_owr1::TyEnv.case_eqns)) 1); |
19 qed "te_rec_emp"; |
19 qed "te_rec_emp"; |
20 |
20 |
21 goal Types.thy |
21 Goal |
22 " te_rec(te_owr(te,x,t),c_te_emp,f_te_owr) = \ |
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))"; |
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); |
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); |
25 by (simp_tac (rank_ss addsimps (rank_te_owr1::TyEnv.case_eqns)) 1); |
26 qed "te_rec_owr"; |
26 qed "te_rec_owr"; |
27 |
27 |
28 goalw Types.thy [te_dom_def] "te_dom(te_emp) = 0"; |
28 Goalw [te_dom_def] "te_dom(te_emp) = 0"; |
29 by (simp_tac (simpset() addsimps [te_rec_emp]) 1); |
29 by (simp_tac (simpset() addsimps [te_rec_emp]) 1); |
30 qed "te_dom_emp"; |
30 qed "te_dom_emp"; |
31 |
31 |
32 goalw Types.thy [te_dom_def] "te_dom(te_owr(te,x,v)) = te_dom(te) Un {x}"; |
32 Goalw [te_dom_def] "te_dom(te_owr(te,x,v)) = te_dom(te) Un {x}"; |
33 by (simp_tac (simpset() addsimps [te_rec_owr]) 1); |
33 by (simp_tac (simpset() addsimps [te_rec_owr]) 1); |
34 qed "te_dom_owr"; |
34 qed "te_dom_owr"; |
35 |
35 |
36 goalw Types.thy [te_app_def] "te_app(te_owr(te,x,t),x) = t"; |
36 Goalw [te_app_def] "te_app(te_owr(te,x,t),x) = t"; |
37 by (simp_tac (simpset() addsimps [te_rec_owr]) 1); |
37 by (simp_tac (simpset() addsimps [te_rec_owr]) 1); |
38 qed "te_app_owr1"; |
38 qed "te_app_owr1"; |
39 |
39 |
40 goalw Types.thy [te_app_def] |
40 Goalw [te_app_def] |
41 "!!x y. x ~= y ==> te_app(te_owr(te,x,t),y) = te_app(te,y)"; |
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); |
42 by (asm_simp_tac (simpset() addsimps [te_rec_owr,(not_sym RS if_not_P)]) 1); |
43 qed "te_app_owr2"; |
43 qed "te_app_owr2"; |
44 |
44 |
45 goal Types.thy |
45 Goal |
46 "!!te. [| te:TyEnv; x:ExVar; x:te_dom(te) |] ==> te_app(te,x):Ty"; |
46 "!!te. [| te:TyEnv; x:ExVar; x:te_dom(te) |] ==> te_app(te,x):Ty"; |
47 by (res_inst_tac [("P","x:te_dom(te)")] impE 1); |
47 by (res_inst_tac [("P","x:te_dom(te)")] impE 1); |
48 by (assume_tac 2); |
48 by (assume_tac 2); |
49 by (assume_tac 2); |
49 by (assume_tac 2); |
50 by (etac TyEnv.induct 1); |
50 by (etac TyEnv.induct 1); |