318 |
318 |
319 lemma "INSERT a (INSERT a x) = INSERT a x" |
319 lemma "INSERT a (INSERT a x) = INSERT a x" |
320 apply (tactic {* lift_tac_fset @{context} @{thm list_eq.intros(4)} 1 *}) |
320 apply (tactic {* lift_tac_fset @{context} @{thm list_eq.intros(4)} 1 *}) |
321 done |
321 done |
322 |
322 |
323 lemma "x = xa \<longrightarrow> INSERT a x = INSERT a xa" |
323 lemma "x = xa \<Longrightarrow> INSERT a x = INSERT a xa" |
324 apply (tactic {* lift_tac_fset @{context} @{thm list_eq.intros(5)} 1 *}) |
324 apply (tactic {* lift_tac_fset @{context} @{thm list_eq.intros(5)} 1 *}) |
325 done |
325 done |
326 |
326 |
327 lemma "CARD x = Suc n \<longrightarrow> (\<exists>a b. \<not> IN a b & x = INSERT a b)" |
327 lemma "CARD x = Suc n \<Longrightarrow> (\<exists>a b. \<not> IN a b & x = INSERT a b)" |
328 apply (tactic {* lift_tac_fset @{context} @{thm card1_suc} 1 *}) |
328 apply (tactic {* lift_tac_fset @{context} @{thm card1_suc} 1 *}) |
329 done |
329 done |
330 |
330 |
331 lemma "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))" |
331 lemma "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))" |
332 apply (tactic {* lift_tac_fset @{context} @{thm not_mem_card1} 1 *}) |
332 apply (tactic {* lift_tac_fset @{context} @{thm not_mem_card1} 1 *}) |
|
333 done |
|
334 |
|
335 lemma "\<forall>f g z a x. FOLD f g (z::'b) (INSERT a x) = |
|
336 (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)" |
|
337 apply (tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) |
|
338 done |
|
339 |
|
340 (* |
|
341 ML {* |
|
342 fun lambda_prs_conv ctxt ctrm = |
|
343 case (Thm.term_of ctrm) of |
|
344 (@{term "op --->"} $ x $ y) $ (Abs (_, T, x)) => |
|
345 let |
|
346 val lty = T; |
|
347 val rty = fastype_of x; |
|
348 val thy = ProofContext.theory_of ctxt; |
|
349 val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty) |
|
350 val inst = [SOME lcty, NONE, SOME rcty]; |
|
351 val lpi = Drule.instantiate' inst [] thm; |
|
352 |
|
353 (Conv.all_conv ctrm) |
|
354 | _ $ _ => Conv.comb_conv (lambda_prs_conv ctxt) ctrm |
|
355 | Abs _ => Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt) ctxt ctrm |
|
356 | _ => Conv.all_conv ctrm |
|
357 *} |
|
358 |
|
359 |
|
360 ML {* |
|
361 fun lambda_prs_tac ctxt = CSUBGOAL (fn (goal, i) => |
|
362 CONVERSION |
|
363 (Conv.params_conv ~1 (fn ctxt => |
|
364 (Conv.prems_conv ~1 (lambda_prs_conv ctxt) then_conv |
|
365 Conv.concl_conv ~1 (lambda_prs_conv ctxt))) ctxt) i) |
|
366 *} |
|
367 *) |
|
368 |
|
369 thm map_append |
|
370 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" |
|
371 apply(tactic {* procedure_tac @{thm map_append} @{context} 1 *}) |
|
372 apply(tactic {* prepare_tac 1 *}) |
|
373 thm map_append |
|
374 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *}) |
|
375 done |
|
376 |
|
377 |
|
378 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
|
379 apply(tactic {* procedure_tac @{thm list.induct} @{context} 1 *}) |
|
380 apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) |
|
381 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *}) |
|
382 apply(tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *}) |
|
383 thm LAMBDA_PRS |
|
384 apply(tactic {* EqSubst.eqsubst_tac @{context} [0] @{thms LAMBDA_PRS} 1 *}) |
|
385 |
|
386 apply(tactic {* (lambda_prs_tac @{context} quot) 1 *}) |
|
387 |
|
388 apply(tactic {* REPEAT_ALL_NEW (lambda_prs_tac @{context} quot) 1 *}) |
|
389 |
|
390 apply(tactic {* clean_tac @{context} quot defs reps_same 1 *}) |
|
391 apply (tactic {* lift_tac_fset @{context} @{thm list.induct} 1 *}) |
|
392 ML {* lift_thm_fset @{context} @{thm list.induct} *} |
|
393 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"} *} |
|
394 |
|
395 lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)" |
|
396 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *}) |
333 done |
397 done |
334 |
398 |
335 ML {* atomize_thm @{thm fold1.simps(2)} *} |
399 ML {* atomize_thm @{thm fold1.simps(2)} *} |
336 (*ML {* lift_thm_g_fset @{context} @{thm fold1.simps(2)} @{term "FOLD f g (z::'b) (INSERT a x) = |
400 (*ML {* lift_thm_g_fset @{context} @{thm fold1.simps(2)} @{term "FOLD f g (z::'b) (INSERT a x) = |
337 (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)"} *}*) |
401 (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)"} *}*) |
338 |
402 |
339 lemma "\<forall>f g z a x. FOLD f g (z::'b) (INSERT a x) = |
403 |
340 (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)" |
404 |
341 apply (tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) |
405 ML {* lift_thm_g_fset @{context} @{thm map_append} @{term "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"} *} |
342 done |
406 |
343 |
407 |
344 ML {* cterm_of @{theory} (atomize_goal @{theory} @{term "\<forall>x xa a. x = xa \<Longrightarrow> INSERT a x = INSERT a xa"}) *} |
408 ML {* cterm_of @{theory} (atomize_goal @{theory} @{term "\<forall>x xa a. x = xa \<Longrightarrow> INSERT a x = INSERT a xa"}) *} |
345 |
409 |
346 (* Doesn't work with 'a, 'b, but works with 'b, 'a *) |
|
347 ML {* lift_thm_g_fset @{context} @{thm fold1.simps(2)} |
|
348 |
|
349 ML {* lift_thm_fset @{context} @{thm append_assoc} *} |
|
350 ML {* lift_thm_g_fset @{context} @{thm append_assoc} @{term "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"} *} |
|
351 |
410 |
352 ML {* lift_thm_fset @{context} @{thm map_append} *} |
411 ML {* lift_thm_fset @{context} @{thm map_append} *} |
353 ML {* lift_thm_g_fset @{context} @{thm map_append} @{term "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"} *} |
|
354 ML {* lift_thm_fset @{context} @{thm list.induct} *} |
|
355 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"} *} |
|
356 |
412 |
357 |
413 |
358 |
414 |
359 apply(tactic {* procedure_tac @{thm m1} @{context} 1 *}) |
415 apply(tactic {* procedure_tac @{thm m1} @{context} 1 *}) |
360 apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) |
416 apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) |