97 by (ALLGOALS (asm_simp_tac (simpset() addsimps prems))); |
97 by (ALLGOALS (asm_simp_tac (simpset() addsimps prems))); |
98 qed "list_rec_type"; |
98 qed "list_rec_type"; |
99 |
99 |
100 (** map **) |
100 (** map **) |
101 |
101 |
102 val prems = Goalw [get_def (the_context ()) "map_list"] |
102 val prems = Goalw [thm "map_list_def"] |
103 "[| l: list(A); !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)"; |
103 "[| l: list(A); !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)"; |
104 by (REPEAT (ares_tac (prems @ list.intrs @ [list_rec_type]) 1)); |
104 by (REPEAT (ares_tac (prems @ list.intrs @ [list_rec_type]) 1)); |
105 qed "map_type"; |
105 qed "map_type"; |
106 |
106 |
107 Goal "l: list(A) ==> map(h,l) : list({h(u). u:A})"; |
107 Goal "l: list(A) ==> map(h,l) : list({h(u). u:A})"; |
109 by (etac RepFunI 1); |
109 by (etac RepFunI 1); |
110 qed "map_type2"; |
110 qed "map_type2"; |
111 |
111 |
112 (** length **) |
112 (** length **) |
113 |
113 |
114 Goalw [get_def (the_context ()) "length_list"] |
114 Goalw [thm "length_list_def"] |
115 "l: list(A) ==> length(l) : nat"; |
115 "l: list(A) ==> length(l) : nat"; |
116 by (REPEAT (ares_tac [list_rec_type, nat_0I, nat_succI] 1)); |
116 by (REPEAT (ares_tac [list_rec_type, nat_0I, nat_succI] 1)); |
117 qed "length_type"; |
117 qed "length_type"; |
118 |
118 |
119 (** app **) |
119 (** app **) |
120 |
120 |
121 Goalw [get_def (the_context ()) "op @_list"] |
121 Goalw [thm "op @_list_def"] |
122 "[| xs: list(A); ys: list(A) |] ==> xs@ys : list(A)"; |
122 "[| xs: list(A); ys: list(A) |] ==> xs@ys : list(A)"; |
123 by (REPEAT (ares_tac [list_rec_type, list.Cons_I] 1)); |
123 by (REPEAT (ares_tac [list_rec_type, list.Cons_I] 1)); |
124 qed "app_type"; |
124 qed "app_type"; |
125 |
125 |
126 (** rev **) |
126 (** rev **) |
127 |
127 |
128 Goalw [get_def (the_context ()) "rev_list"] |
128 Goalw [thm "rev_list_def"] |
129 "xs: list(A) ==> rev(xs) : list(A)"; |
129 "xs: list(A) ==> rev(xs) : list(A)"; |
130 by (REPEAT (ares_tac (list.intrs @ [list_rec_type, app_type]) 1)); |
130 by (REPEAT (ares_tac (list.intrs @ [list_rec_type, app_type]) 1)); |
131 qed "rev_type"; |
131 qed "rev_type"; |
132 |
132 |
133 |
133 |
134 (** flat **) |
134 (** flat **) |
135 |
135 |
136 Goalw [get_def (the_context ()) "flat_list"] |
136 Goalw [thm "flat_list_def"] |
137 "ls: list(list(A)) ==> flat(ls) : list(A)"; |
137 "ls: list(list(A)) ==> flat(ls) : list(A)"; |
138 by (REPEAT (ares_tac (list.intrs @ [list_rec_type, app_type]) 1)); |
138 by (REPEAT (ares_tac (list.intrs @ [list_rec_type, app_type]) 1)); |
139 qed "flat_type"; |
139 qed "flat_type"; |
140 |
140 |
141 |
141 |
142 (** set_of_list **) |
142 (** set_of_list **) |
143 |
143 |
144 Goalw [get_def (the_context ()) "set_of_list_list"] |
144 Goalw [thm "set_of_list_list_def"] |
145 "l: list(A) ==> set_of_list(l) : Pow(A)"; |
145 "l: list(A) ==> set_of_list(l) : Pow(A)"; |
146 by (etac list_rec_type 1); |
146 by (etac list_rec_type 1); |
147 by (ALLGOALS (Blast_tac)); |
147 by (ALLGOALS (Blast_tac)); |
148 qed "set_of_list_type"; |
148 qed "set_of_list_type"; |
149 |
149 |
154 qed "set_of_list_append"; |
154 qed "set_of_list_append"; |
155 |
155 |
156 |
156 |
157 (** list_add **) |
157 (** list_add **) |
158 |
158 |
159 Goalw [get_def (the_context ()) "list_add_list"] |
159 Goalw [thm "list_add_list_def"] |
160 "xs: list(nat) ==> list_add(xs) : nat"; |
160 "xs: list(nat) ==> list_add(xs) : nat"; |
161 by (REPEAT (ares_tac [list_rec_type, nat_0I, add_type] 1)); |
161 by (REPEAT (ares_tac [list_rec_type, nat_0I, add_type] 1)); |
162 qed "list_add_type"; |
162 qed "list_add_type"; |
163 |
163 |
164 bind_thms ("list_typechecks", |
164 bind_thms ("list_typechecks", |