324 (* Doesn't work with 'a, 'b, but works with 'b, 'a *) |
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) = |
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)"} *} |
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 |
327 |
328 ML {* lift_thm_fset @{context} @{thm append_assoc} *} |
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)"} *} |
329 ML {* lift_thm_g_fset @{context} @{thm append_assoc} @{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} *} |
330 ML {* lift_thm_fset @{context} @{thm map_append} *} |
|
331 ML {* lift_thm_g_fset @{context} @{thm map_append} @{term "fmap f (FUNION x xa) = FUNION (fmap f x) (fmap f xa)"} *} |
|
332 |
343 ML {* lift_thm_fset @{context} @{thm list.induct} *} |
333 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"} *} |
334 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"} *} |
|
335 |
|
336 |
|
337 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
|
338 ML {* val rtrm = prop_of (atomize_thm @{thm append_assoc}) *} |
|
339 ML {* val qtrm = goal_a *} |
|
340 ML {* val a = (REGULARIZE_trm @{context} rtrm qtrm) *} |
|
341 ML {* val a = Syntax.check_term @{context} a *} |
|
342 ML {* val t_r = regularize_goal @{context} (atomize_thm @{thm append_assoc}) rel_eqv rel_refl goal_a *} |
|
343 |
|
344 ML {* lift_thm_g_fset @{context} @{thm append_assoc} gl *} |
|
345 |
|
346 |
345 |
347 |
346 (*ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *}*) |
348 (*ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *}*) |
347 |
349 |
348 quotient_def |
350 quotient_def |
349 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
351 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |