196 val case_ns = |
196 val case_ns = |
197 "bottom" :: map (fn (b,_,_) => Binding.name_of b) spec; |
197 "bottom" :: map (fn (b,_,_) => Binding.name_of b) spec; |
198 |
198 |
199 fun qualified name = Binding.qualified true name dbind; |
199 fun qualified name = Binding.qualified true name dbind; |
200 val simp = Simplifier.simp_add; |
200 val simp = Simplifier.simp_add; |
201 val fixrec_simp = Fixrec.fixrec_simp_add; |
|
202 |
201 |
203 in |
202 in |
204 thy |
203 thy |
205 |> PureThy.add_thmss [ |
204 |> PureThy.add_thmss [ |
206 ((qualified "iso_rews" , iso_rews ), [simp]), |
205 ((qualified "iso_rews" , iso_rews ), [simp]), |
207 ((qualified "nchotomy" , [nchotomy] ), []), |
206 ((qualified "nchotomy" , [nchotomy] ), []), |
208 ((qualified "exhaust" , [exhaust] ), |
207 ((qualified "exhaust" , [exhaust] ), |
209 [Rule_Cases.case_names case_ns, Induct.cases_type dname]), |
208 [Rule_Cases.case_names case_ns, Induct.cases_type dname]), |
210 ((qualified "when_rews" , when_rews ), [simp]), |
209 ((qualified "when_rews" , when_rews ), [simp]), |
211 ((qualified "compacts" , compacts ), [simp]), |
210 ((qualified "compacts" , compacts ), [simp]), |
212 ((qualified "con_rews" , con_rews ), [simp, fixrec_simp]), |
211 ((qualified "con_rews" , con_rews ), [simp]), |
213 ((qualified "sel_rews" , sel_rews ), [simp]), |
212 ((qualified "sel_rews" , sel_rews ), [simp]), |
214 ((qualified "dis_rews" , dis_rews ), [simp]), |
213 ((qualified "dis_rews" , dis_rews ), [simp]), |
215 ((qualified "pat_rews" , pat_rews ), [simp]), |
214 ((qualified "pat_rews" , pat_rews ), [simp]), |
216 ((qualified "dist_les" , dist_les ), [simp]), |
215 ((qualified "dist_les" , dist_les ), [simp]), |
217 ((qualified "dist_eqs" , dist_eqs ), [simp]), |
216 ((qualified "dist_eqs" , dist_eqs ), [simp]), |
218 ((qualified "inverts" , inverts ), [simp]), |
217 ((qualified "inverts" , inverts ), [simp]), |
219 ((qualified "injects" , injects ), [simp]), |
218 ((qualified "injects" , injects ), [simp]), |
220 ((qualified "take_rews" , take_rews ), [simp]), |
219 ((qualified "take_rews" , take_rews ), [simp]), |
221 ((qualified "match_rews", mat_rews ), [simp, fixrec_simp])] |
220 ((qualified "match_rews", mat_rews ), [simp])] |
222 |> snd |
221 |> snd |
223 |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @ |
222 |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @ |
224 pat_rews @ dist_les @ dist_eqs) |
223 pat_rews @ dist_les @ dist_eqs) |
225 end; (* let *) |
224 end; (* let *) |
226 |
225 |