2525
|
1 |
(* Title: HOL/MiniML/Generalize.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Wolfgang Naraschewski and Tobias Nipkow
|
|
4 |
Copyright 1996 TU Muenchen
|
|
5 |
*)
|
|
6 |
|
|
7 |
AddSEs [equalityE];
|
|
8 |
|
|
9 |
goal thy "!!A B. free_tv A = free_tv B ==> gen A t = gen B t";
|
|
10 |
by (typ.induct_tac "t" 1);
|
|
11 |
by (ALLGOALS Asm_simp_tac);
|
|
12 |
qed "gen_eq_on_free_tv";
|
|
13 |
|
|
14 |
goal thy "!!t.(free_tv t) <= (free_tv sch) --> gen sch t = (mk_scheme t)";
|
|
15 |
by (typ.induct_tac "t" 1);
|
|
16 |
by (Asm_simp_tac 1);
|
|
17 |
by (Simp_tac 1);
|
|
18 |
by (Fast_tac 1);
|
|
19 |
qed_spec_mp "gen_without_effect";
|
|
20 |
|
|
21 |
Addsimps [gen_without_effect];
|
|
22 |
|
|
23 |
goal thy "!!A. free_tv (gen ($ S A) t) = free_tv t Int free_tv ($ S A)";
|
|
24 |
by (typ.induct_tac "t" 1);
|
|
25 |
by (Simp_tac 1);
|
|
26 |
by (case_tac "nat : free_tv ($ S A)" 1);
|
|
27 |
by (Asm_simp_tac 1);
|
|
28 |
by (Fast_tac 1);
|
|
29 |
by (Asm_simp_tac 1);
|
|
30 |
by (Fast_tac 1);
|
|
31 |
by (Asm_full_simp_tac 1);
|
|
32 |
by (Fast_tac 1);
|
|
33 |
qed "free_tv_gen";
|
|
34 |
|
|
35 |
Addsimps [free_tv_gen];
|
|
36 |
|
|
37 |
goal thy "!!A. free_tv (gen ($ S A) t # $ S A) = free_tv ($ S A)";
|
|
38 |
by (Simp_tac 1);
|
|
39 |
by (Fast_tac 1);
|
|
40 |
qed "free_tv_gen_cons";
|
|
41 |
|
|
42 |
Addsimps [free_tv_gen_cons];
|
|
43 |
|
|
44 |
goal thy "!!A. bound_tv (gen A t1) = (free_tv t1) - (free_tv A)";
|
|
45 |
by (typ.induct_tac "t1" 1);
|
|
46 |
by (Simp_tac 1);
|
|
47 |
by (case_tac "nat : free_tv A" 1);
|
|
48 |
by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
|
|
49 |
by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
|
|
50 |
by (Fast_tac 1);
|
|
51 |
by (Asm_simp_tac 1);
|
|
52 |
by (Fast_tac 1);
|
|
53 |
qed "bound_tv_gen";
|
|
54 |
|
|
55 |
Addsimps [bound_tv_gen];
|
|
56 |
|
|
57 |
goal thy "!!A. new_tv n t --> new_tv n (gen A t)";
|
|
58 |
by (typ.induct_tac "t" 1);
|
|
59 |
by (Simp_tac 1);
|
|
60 |
by (case_tac "nat : free_tv A" 1);
|
|
61 |
by (Asm_simp_tac 1);
|
|
62 |
by (Asm_simp_tac 1);
|
|
63 |
by (Asm_full_simp_tac 1);
|
|
64 |
qed_spec_mp "new_tv_compatible_gen";
|
|
65 |
|
|
66 |
goalw thy [gen_ML_def] "!!A. gen A t = gen_ML A t";
|
|
67 |
by (typ.induct_tac "t" 1);
|
|
68 |
by (simp_tac (!simpset addsimps [free_tv_ML_scheme_list]) 1);
|
|
69 |
by (asm_simp_tac (!simpset addsimps [free_tv_ML_scheme_list]) 1);
|
|
70 |
qed "gen_eq_gen_ML";
|
|
71 |
|
|
72 |
goal thy "!!S. (free_tv S) Int ((free_tv t) - (free_tv A)) = {} \
|
|
73 |
\ --> gen ($ S A) ($ S t) = $ S (gen A t)";
|
|
74 |
by (typ.induct_tac "t" 1);
|
|
75 |
by (strip_tac 1);
|
|
76 |
by (case_tac "nat:(free_tv A)" 1);
|
|
77 |
by (Asm_simp_tac 1);
|
|
78 |
by (Asm_full_simp_tac 1);
|
|
79 |
by (subgoal_tac "nat ~: free_tv S" 1);
|
|
80 |
by (Fast_tac 2);
|
|
81 |
by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def,de_Morgan_disj]) 1);
|
|
82 |
by (split_tac [expand_if] 1);
|
|
83 |
by (cut_facts_tac [free_tv_app_subst_scheme_list] 1);
|
|
84 |
by (Fast_tac 1);
|
|
85 |
by (Asm_simp_tac 1);
|
|
86 |
by (Best_tac 1);
|
|
87 |
qed_spec_mp "gen_subst_commutes";
|
|
88 |
|
|
89 |
goal Generalize.thy "free_tv(t::typ) <= free_tv(A) --> bound_typ_inst S (gen A t) = t";
|
|
90 |
by(typ.induct_tac "t" 1);
|
|
91 |
by(ALLGOALS Asm_simp_tac);
|
|
92 |
by(Fast_tac 1);
|
|
93 |
qed_spec_mp "bound_typ_inst_gen";
|
|
94 |
Addsimps [bound_typ_inst_gen];
|
|
95 |
|
|
96 |
goalw Generalize.thy [le_type_scheme_def,is_bound_typ_instance]
|
|
97 |
"gen ($ S A) ($ S t) <= $ S (gen A t)";
|
|
98 |
by(safe_tac (!claset));
|
|
99 |
by(rename_tac "R" 1);
|
|
100 |
by(res_inst_tac [("x", "(%a. bound_typ_inst R (gen ($S A) (S a)))")] exI 1);
|
|
101 |
by(typ.induct_tac "t" 1);
|
|
102 |
by(simp_tac (!simpset setloop (split_tac[expand_if])) 1);
|
|
103 |
by(Asm_simp_tac 1);
|
|
104 |
qed "gen_bound_typ_instance";
|
|
105 |
|
|
106 |
goalw Generalize.thy [le_type_scheme_def,is_bound_typ_instance]
|
|
107 |
"!!A B. free_tv B <= free_tv A ==> gen A t <= gen B t";
|
|
108 |
by(safe_tac (!claset));
|
|
109 |
by(rename_tac "S" 1);
|
|
110 |
by(res_inst_tac [("x","%b. if b:free_tv A then TVar b else S b")] exI 1);
|
|
111 |
by (typ.induct_tac "t" 1);
|
|
112 |
by(asm_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
|
|
113 |
by(Fast_tac 1);
|
|
114 |
by(Asm_simp_tac 1);
|
|
115 |
qed "free_tv_subset_gen_le";
|
|
116 |
|
|
117 |
goalw thy [le_type_scheme_def,is_bound_typ_instance]
|
|
118 |
"!!A. new_tv n A --> gen A t <= gen A ($ (%x. TVar (if x : free_tv A then x else n + x)) t)";
|
|
119 |
by (strip_tac 1);
|
|
120 |
by (etac exE 1);
|
|
121 |
by (hyp_subst_tac 1);
|
|
122 |
by (res_inst_tac [("x","(%x. S (if n <= x then x - n else x))")] exI 1);
|
|
123 |
by (typ.induct_tac "t" 1);
|
|
124 |
by (Simp_tac 1);
|
|
125 |
by (case_tac "nat : free_tv A" 1);
|
|
126 |
by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
|
|
127 |
by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
|
|
128 |
by (subgoal_tac "n <= n + nat" 1);
|
|
129 |
by (forw_inst_tac [("t","A")] new_tv_le 1);
|
|
130 |
ba 1;
|
|
131 |
by (dtac new_tv_not_free_tv 1);
|
|
132 |
by (dtac new_tv_not_free_tv 1);
|
|
133 |
by (asm_simp_tac (!simpset addsimps [diff_add_inverse]) 1);
|
|
134 |
by (simp_tac (!simpset addsimps [le_add1]) 1);
|
|
135 |
by (Asm_simp_tac 1);
|
|
136 |
qed_spec_mp "gen_t_le_gen_alpha_t";
|
|
137 |
|
|
138 |
Addsimps [gen_t_le_gen_alpha_t];
|