302 ML {* val rsp_thms = |
302 ML {* val rsp_thms = |
303 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} |
303 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} |
304 @ @{thms ho_all_prs ho_ex_prs} *} |
304 @ @{thms ho_all_prs ho_ex_prs} *} |
305 |
305 |
306 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *} |
306 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *} |
307 |
307 ML {* fun lift_thm_g_fset lthy t g = lift_thm_goal lthy qty "fset" rsp_thms defs t g *} |
308 thm m2 |
308 |
309 |
309 ML {* atomize_thm @{thm m1} *} |
310 thm neq_Nil_conv |
310 ML {* cterm_of @{theory} (atomize_goal @{theory} @{term "IN x EMPTY = False"}) *} |
311 term REP_fset |
311 ML {* lift_thm_fset @{context} @{thm m1} *} |
312 term "op --->" |
312 ML {* lift_thm_g_fset @{context} @{thm m1} @{term "IN x EMPTY = False"} *} |
313 thm INSERT_def |
313 ML {* lift_thm_fset @{context} @{thm m2} *} |
314 ML {* val defs_sym = flat (map (add_lower_defs @{context}) @{thms INSERT_def}) *} |
314 ML {* lift_thm_g_fset @{context} @{thm m2} @{term "IN x (INSERT y xa) = (x = y \<or> IN x xa)"} *} |
|
315 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *} |
|
316 ML {* lift_thm_g_fset @{context} @{thm list_eq.intros(4)} @{term "INSERT a (INSERT a x) = INSERT a x"} *} |
|
317 ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *} |
|
318 ML {* lift_thm_g_fset @{context} @{thm list_eq.intros(5)} @{term "x = xa \<Longrightarrow> INSERT a x = INSERT a xa"} *} |
|
319 ML {* lift_thm_fset @{context} @{thm card1_suc} *} |
|
320 ML {* lift_thm_g_fset @{context} @{thm card1_suc} @{term "CARD x = Suc n \<Longrightarrow> \<exists>a b. \<not> IN a b \<and> x = INSERT a b"} *} |
|
321 ML {* lift_thm_fset @{context} @{thm not_mem_card1} *} |
|
322 ML {* lift_thm_g_fset @{context} @{thm not_mem_card1} @{term "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))"} *} |
|
323 ML {* lift_thm_fset @{context} @{thm fold1.simps(2)} *} |
|
324 (* Doesn't work with 'a, 'b, but works with 'b, 'a *) |
|
325 ML {* lift_thm_g_fset @{context} @{thm fold1.simps(2)} @{term "FOLD f g (z::'b) (INSERT a x) = |
|
326 (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"} *} |
|
327 |
|
328 ML {* lift_thm_fset @{context} @{thm append_assoc} *} |
|
329 ML {* val goal_a = atomize_goal @{theory} @{term "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"} *} |
|
330 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
|
331 (* Fails *) |
|
332 ML {* val reg_trm = mk_REGULARIZE_goal @{context} (prop_of (atomize_thm @{thm append_assoc})) goal_a *} |
|
333 |
|
334 |
|
335 |
|
336 |
|
337 ML {* val t_r = regularize_goal @{context} (atomize_thm @{thm append_assoc}) rel_eqv rel_refl goal_a *} |
|
338 |
|
339 ML {* lift_thm_g_fset @{context} @{thm append_assoc} gl *} |
|
340 |
|
341 |
|
342 ML {* lift_thm_fset @{context} @{thm map_append} *} |
|
343 ML {* lift_thm_fset @{context} @{thm list.induct} *} |
|
344 ML {* lift_thm_g_fset @{context} @{thm list.induct} @{term "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"} *} |
|
345 |
315 (*ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *}*) |
346 (*ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *}*) |
316 ML {* lift_thm_fset @{context} @{thm m1} *} |
|
317 ML {* lift_thm_fset @{context} @{thm m2} *} |
|
318 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *} |
|
319 ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *} |
|
320 ML {* lift_thm_fset @{context} @{thm card1_suc} *} |
|
321 ML {* lift_thm_fset @{context} @{thm map_append} *} |
|
322 ML {* lift_thm_fset @{context} @{thm append_assoc} *} |
|
323 ML {* lift_thm_fset @{context} @{thm list.induct} *} |
|
324 ML {* lift_thm_fset @{context} @{thm fold1.simps(2)} *} |
|
325 ML {* lift_thm_fset @{context} @{thm not_mem_card1} *} |
|
326 |
347 |
327 quotient_def |
348 quotient_def |
328 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
349 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
329 where |
350 where |
330 "fset_rec \<equiv> list_rec" |
351 "fset_rec \<equiv> list_rec" |
354 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *} |
375 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *} |
355 |
376 |
356 |
377 |
357 ML {* map (lift_thm_fset @{context}) @{thms list.recs} *} |
378 ML {* map (lift_thm_fset @{context}) @{thms list.recs} *} |
358 ML {* map (lift_thm_fset @{context}) @{thms list.cases} *} |
379 ML {* map (lift_thm_fset @{context}) @{thms list.cases} *} |
|
380 |
|
381 ML {* atomize_thm @{thm m1} *} |
|
382 ML {* cterm_of @{theory} (atomize_goal @{theory} @{term "IN x EMPTY = False"}) *} |
|
383 ML {* lift_thm_fset @{context} @{thm m1} *} |
|
384 (* ML {* lift_thm_g_fset @{context} @{thm m1} @{term "IN x EMPTY = False"}) *} *) |
|
385 |
359 |
386 |
360 lemma list_induct_part: |
387 lemma list_induct_part: |
361 assumes a: "P (x :: 'a list) ([] :: 'a list)" |
388 assumes a: "P (x :: 'a list) ([] :: 'a list)" |
362 assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)" |
389 assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)" |
363 shows "P x l" |
390 shows "P x l" |