309 ML {* atomize_thm @{thm m1} *} |
309 ML {* atomize_thm @{thm m1} *} |
310 ML {* cterm_of @{theory} (atomize_goal @{theory} @{term "IN x EMPTY = False"}) *} |
310 ML {* cterm_of @{theory} (atomize_goal @{theory} @{term "IN x EMPTY = False"}) *} |
311 ML {* lift_thm_fset @{context} @{thm m1} *} |
311 ML {* lift_thm_fset @{context} @{thm m1} *} |
312 ML {* lift_thm_g_fset @{context} @{thm m1} @{term "IN x EMPTY = False"} *} |
312 ML {* lift_thm_g_fset @{context} @{thm m1} @{term "IN x EMPTY = False"} *} |
313 ML {* lift_thm_fset @{context} @{thm m2} *} |
313 ML {* lift_thm_fset @{context} @{thm m2} *} |
|
314 |
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_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_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_g_fset @{context} @{thm list_eq.intros(4)} @{term "INSERT a (INSERT a x) = INSERT a x"} *} |
|
318 |
317 ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *} |
319 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"} *} |
320 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} *} |
321 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"} *} |
322 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} *} |
323 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))"} *} |
324 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)} *} |
325 ML {* lift_thm_fset @{context} @{thm fold1.simps(2)} *} |
324 (* Doesn't work with 'a, 'b, but works with 'b, 'a *) |
326 (* Doesn't work with 'a, 'b, but works with 'b, 'a *) |
|
327 |
325 ML {* lift_thm_g_fset @{context} @{thm fold1.simps(2)} @{term "FOLD f g (z::'b) (INSERT a x) = |
328 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)"} *} |
329 (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 |
330 |
328 ML {* lift_thm_fset @{context} @{thm append_assoc} *} |
331 ML {* lift_thm_fset @{context} @{thm append_assoc} *} |
329 ML {* lift_thm_g_fset @{context} @{thm append_assoc} @{term "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"} *} |
332 ML {* lift_thm_g_fset @{context} @{thm append_assoc} @{term "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"} *} |
330 ML {* lift_thm_fset @{context} @{thm map_append} *} |
333 ML {* lift_thm_fset @{context} @{thm map_append} *} |
331 ML {* val gl = @{term "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"} *} |
334 ML {* val gl = @{term "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"} *} |
332 |
335 |
333 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
336 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
334 ML {* val rtrm = prop_of (atomize_thm @{thm map_append}) *} |
337 ML {* val rtrm = prop_of (atomize_thm @{thm map_append}) *} |
|
338 |
335 ML {* val qtrm = atomize_goal @{theory} gl *} |
339 ML {* val qtrm = atomize_goal @{theory} gl *} |
336 ML {* val a = (REGULARIZE_trm @{context} rtrm qtrm) *} |
340 ML {* val a = (REGULARIZE_trm @{context} rtrm qtrm) *} |
|
341 |
337 ML {* val a = Syntax.check_term @{context} a *} |
342 ML {* val a = Syntax.check_term @{context} a *} |
338 ML {* val t_r = regularize_goal @{context} (atomize_thm @{thm append_assoc}) rel_eqv rel_refl goal_a *} |
343 ML {* val t_r = regularize_goal @{context} (atomize_thm @{thm append_assoc}) rel_eqv rel_refl goal_a *} |
339 |
344 |
340 ML {* lift_thm_g_fset @{context} @{thm map_append} gl *} |
345 ML {* lift_thm_g_fset @{context} @{thm map_append} gl *} |
341 |
346 |