4 Copyright 1996 TU Muenchen |
4 Copyright 1996 TU Muenchen |
5 *) |
5 *) |
6 |
6 |
7 AddSEs [equalityE]; |
7 AddSEs [equalityE]; |
8 |
8 |
9 goal thy "!!A B. free_tv A = free_tv B ==> gen A t = gen B t"; |
9 Goal "!!A B. free_tv A = free_tv B ==> gen A t = gen B t"; |
10 by (typ.induct_tac "t" 1); |
10 by (typ.induct_tac "t" 1); |
11 by (ALLGOALS Asm_simp_tac); |
11 by (ALLGOALS Asm_simp_tac); |
12 qed "gen_eq_on_free_tv"; |
12 qed "gen_eq_on_free_tv"; |
13 |
13 |
14 goal thy "!!t.(free_tv t) <= (free_tv sch) --> gen sch t = (mk_scheme t)"; |
14 Goal "!!t.(free_tv t) <= (free_tv sch) --> gen sch t = (mk_scheme t)"; |
15 by (typ.induct_tac "t" 1); |
15 by (typ.induct_tac "t" 1); |
16 by (Asm_simp_tac 1); |
16 by (Asm_simp_tac 1); |
17 by (Simp_tac 1); |
17 by (Simp_tac 1); |
18 by (Fast_tac 1); |
18 by (Fast_tac 1); |
19 qed_spec_mp "gen_without_effect"; |
19 qed_spec_mp "gen_without_effect"; |
20 |
20 |
21 Addsimps [gen_without_effect]; |
21 Addsimps [gen_without_effect]; |
22 |
22 |
23 goal thy "!!A. free_tv (gen ($ S A) t) = free_tv t Int free_tv ($ S A)"; |
23 Goal "!!A. free_tv (gen ($ S A) t) = free_tv t Int free_tv ($ S A)"; |
24 by (typ.induct_tac "t" 1); |
24 by (typ.induct_tac "t" 1); |
25 by (Simp_tac 1); |
25 by (Simp_tac 1); |
26 by (case_tac "nat : free_tv ($ S A)" 1); |
26 by (case_tac "nat : free_tv ($ S A)" 1); |
27 by (Asm_simp_tac 1); |
27 by (Asm_simp_tac 1); |
28 by (Fast_tac 1); |
28 by (Fast_tac 1); |
32 by (Fast_tac 1); |
32 by (Fast_tac 1); |
33 qed "free_tv_gen"; |
33 qed "free_tv_gen"; |
34 |
34 |
35 Addsimps [free_tv_gen]; |
35 Addsimps [free_tv_gen]; |
36 |
36 |
37 goal thy "!!A. free_tv (gen ($ S A) t # $ S A) = free_tv ($ S A)"; |
37 Goal "!!A. free_tv (gen ($ S A) t # $ S A) = free_tv ($ S A)"; |
38 by (Simp_tac 1); |
38 by (Simp_tac 1); |
39 by (Fast_tac 1); |
39 by (Fast_tac 1); |
40 qed "free_tv_gen_cons"; |
40 qed "free_tv_gen_cons"; |
41 |
41 |
42 Addsimps [free_tv_gen_cons]; |
42 Addsimps [free_tv_gen_cons]; |
43 |
43 |
44 goal thy "!!A. bound_tv (gen A t1) = (free_tv t1) - (free_tv A)"; |
44 Goal "!!A. bound_tv (gen A t1) = (free_tv t1) - (free_tv A)"; |
45 by (typ.induct_tac "t1" 1); |
45 by (typ.induct_tac "t1" 1); |
46 by (Simp_tac 1); |
46 by (Simp_tac 1); |
47 by (case_tac "nat : free_tv A" 1); |
47 by (case_tac "nat : free_tv A" 1); |
48 by (Asm_simp_tac 1); |
48 by (Asm_simp_tac 1); |
49 by (Asm_simp_tac 1); |
49 by (Asm_simp_tac 1); |
52 by (Fast_tac 1); |
52 by (Fast_tac 1); |
53 qed "bound_tv_gen"; |
53 qed "bound_tv_gen"; |
54 |
54 |
55 Addsimps [bound_tv_gen]; |
55 Addsimps [bound_tv_gen]; |
56 |
56 |
57 goal thy "!!A. new_tv n t --> new_tv n (gen A t)"; |
57 Goal "!!A. new_tv n t --> new_tv n (gen A t)"; |
58 by (typ.induct_tac "t" 1); |
58 by (typ.induct_tac "t" 1); |
59 by (Simp_tac 1); |
59 by (Simp_tac 1); |
60 by (case_tac "nat : free_tv A" 1); |
60 by (case_tac "nat : free_tv A" 1); |
61 by (Asm_simp_tac 1); |
61 by (Asm_simp_tac 1); |
62 by (Asm_simp_tac 1); |
62 by (Asm_simp_tac 1); |
63 qed_spec_mp "new_tv_compatible_gen"; |
63 qed_spec_mp "new_tv_compatible_gen"; |
64 |
64 |
65 goalw thy [gen_ML_def] "!!A. gen A t = gen_ML A t"; |
65 Goalw [gen_ML_def] "!!A. gen A t = gen_ML A t"; |
66 by (typ.induct_tac "t" 1); |
66 by (typ.induct_tac "t" 1); |
67 by (simp_tac (simpset() addsimps [free_tv_ML_scheme_list]) 1); |
67 by (simp_tac (simpset() addsimps [free_tv_ML_scheme_list]) 1); |
68 by (asm_simp_tac (simpset() addsimps [free_tv_ML_scheme_list]) 1); |
68 by (asm_simp_tac (simpset() addsimps [free_tv_ML_scheme_list]) 1); |
69 qed "gen_eq_gen_ML"; |
69 qed "gen_eq_gen_ML"; |
70 |
70 |
71 goal thy "!!S. (free_tv S) Int ((free_tv t) - (free_tv A)) = {} \ |
71 Goal "!!S. (free_tv S) Int ((free_tv t) - (free_tv A)) = {} \ |
72 \ --> gen ($ S A) ($ S t) = $ S (gen A t)"; |
72 \ --> gen ($ S A) ($ S t) = $ S (gen A t)"; |
73 by (induct_tac "t" 1); |
73 by (induct_tac "t" 1); |
74 by (strip_tac 1); |
74 by (strip_tac 1); |
75 by (case_tac "nat:(free_tv A)" 1); |
75 by (case_tac "nat:(free_tv A)" 1); |
76 by (Asm_simp_tac 1); |
76 by (Asm_simp_tac 1); |
82 by (Fast_tac 1); |
82 by (Fast_tac 1); |
83 by (Asm_simp_tac 1); |
83 by (Asm_simp_tac 1); |
84 by (Blast_tac 1); |
84 by (Blast_tac 1); |
85 qed_spec_mp "gen_subst_commutes"; |
85 qed_spec_mp "gen_subst_commutes"; |
86 |
86 |
87 goal Generalize.thy "free_tv(t::typ) <= free_tv(A) --> bound_typ_inst S (gen A t) = t"; |
87 Goal "free_tv(t::typ) <= free_tv(A) --> bound_typ_inst S (gen A t) = t"; |
88 by (typ.induct_tac "t" 1); |
88 by (typ.induct_tac "t" 1); |
89 by (ALLGOALS Asm_simp_tac); |
89 by (ALLGOALS Asm_simp_tac); |
90 by (Fast_tac 1); |
90 by (Fast_tac 1); |
91 qed_spec_mp "bound_typ_inst_gen"; |
91 qed_spec_mp "bound_typ_inst_gen"; |
92 Addsimps [bound_typ_inst_gen]; |
92 Addsimps [bound_typ_inst_gen]; |
93 |
93 |
94 goalw Generalize.thy [le_type_scheme_def,is_bound_typ_instance] |
94 Goalw [le_type_scheme_def,is_bound_typ_instance] |
95 "gen ($ S A) ($ S t) <= $ S (gen A t)"; |
95 "gen ($ S A) ($ S t) <= $ S (gen A t)"; |
96 by Safe_tac; |
96 by Safe_tac; |
97 by (rename_tac "R" 1); |
97 by (rename_tac "R" 1); |
98 by (res_inst_tac [("x", "(%a. bound_typ_inst R (gen ($S A) (S a)))")] exI 1); |
98 by (res_inst_tac [("x", "(%a. bound_typ_inst R (gen ($S A) (S a)))")] exI 1); |
99 by (typ.induct_tac "t" 1); |
99 by (typ.induct_tac "t" 1); |
100 by (Simp_tac 1); |
100 by (Simp_tac 1); |
101 by (Asm_simp_tac 1); |
101 by (Asm_simp_tac 1); |
102 qed "gen_bound_typ_instance"; |
102 qed "gen_bound_typ_instance"; |
103 |
103 |
104 goalw Generalize.thy [le_type_scheme_def,is_bound_typ_instance] |
104 Goalw [le_type_scheme_def,is_bound_typ_instance] |
105 "!!A B. free_tv B <= free_tv A ==> gen A t <= gen B t"; |
105 "!!A B. free_tv B <= free_tv A ==> gen A t <= gen B t"; |
106 by Safe_tac; |
106 by Safe_tac; |
107 by (rename_tac "S" 1); |
107 by (rename_tac "S" 1); |
108 by (res_inst_tac [("x","%b. if b:free_tv A then TVar b else S b")] exI 1); |
108 by (res_inst_tac [("x","%b. if b:free_tv A then TVar b else S b")] exI 1); |
109 by (typ.induct_tac "t" 1); |
109 by (typ.induct_tac "t" 1); |
110 by (Asm_simp_tac 1); |
110 by (Asm_simp_tac 1); |
111 by (Fast_tac 1); |
111 by (Fast_tac 1); |
112 by (Asm_simp_tac 1); |
112 by (Asm_simp_tac 1); |
113 qed "free_tv_subset_gen_le"; |
113 qed "free_tv_subset_gen_le"; |
114 |
114 |
115 goalw thy [le_type_scheme_def,is_bound_typ_instance] |
115 Goalw [le_type_scheme_def,is_bound_typ_instance] |
116 "!!A. new_tv n A --> gen A t <= gen A ($ (%x. TVar (if x : free_tv A then x else n + x)) t)"; |
116 "!!A. new_tv n A --> gen A t <= gen A ($ (%x. TVar (if x : free_tv A then x else n + x)) t)"; |
117 by (strip_tac 1); |
117 by (strip_tac 1); |
118 by (etac exE 1); |
118 by (etac exE 1); |
119 by (hyp_subst_tac 1); |
119 by (hyp_subst_tac 1); |
120 by (res_inst_tac [("x","(%x. S (if n <= x then x - n else x))")] exI 1); |
120 by (res_inst_tac [("x","(%x. S (if n <= x then x - n else x))")] exI 1); |