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 ML {* fun lift_thm_g_fset lthy t g = lift_thm_goal lthy qty "fset" rsp_thms defs t g *} |
307 ML {* fun lift_thm_g_fset lthy t g = lift_thm_goal lthy qty "fset" rsp_thms defs t g *} |
308 |
308 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
309 ML {* lift_thm_fset @{context} @{thm m1} *} |
309 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *} |
310 ML {* lift_thm_g_fset @{context} @{thm m1} @{term "IN x EMPTY = False"} *} |
310 ML {* val consts = lookup_quot_consts defs *} |
311 |
311 ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *} |
312 ML {* lift_thm_fset @{context} @{thm m2} *} |
312 |
313 ML {* lift_thm_g_fset @{context} @{thm m2} @{term "IN x (INSERT y xa) = (x = y \<or> IN x xa)"} *} |
313 lemma "IN x EMPTY = False" |
314 |
314 by (tactic {* lift_tac_fset @{context} @{thm m1} 1 *}) |
315 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *} |
315 |
316 ML {* lift_thm_g_fset @{context} @{thm list_eq.intros(4)} @{term "INSERT a (INSERT a x) = INSERT a x"} *} |
316 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)" |
317 |
317 by (tactic {* lift_tac_fset @{context} @{thm m2} 1 *}) |
318 ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *} |
318 |
319 ML {* lift_thm_g_fset @{context} @{thm list_eq.intros(5)} @{term "x = xa \<Longrightarrow> INSERT a x = INSERT a xa"} *} |
319 lemma "INSERT a (INSERT a x) = INSERT a x" |
320 |
320 apply (tactic {* lift_tac_fset @{context} @{thm list_eq.intros(4)} 1 *}) |
321 ML {* lift_thm_fset @{context} @{thm card1_suc} *} |
321 done |
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"} *} |
322 |
323 |
323 lemma "x = xa \<longrightarrow> INSERT a x = INSERT a xa" |
324 ML {* lift_thm_fset @{context} @{thm not_mem_card1} *} |
324 apply (tactic {* lift_tac_fset @{context} @{thm list_eq.intros(5)} 1 *}) |
325 ML {* lift_thm_g_fset @{context} @{thm not_mem_card1} @{term "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))"} *} |
325 done |
326 |
326 |
327 ML {* lift_thm_fset @{context} @{thm fold1.simps(2)} *} |
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 *}) |
|
329 done |
|
330 |
|
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 *}) |
|
333 done |
|
334 |
|
335 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) = |
|
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)"} *}*) |
|
338 |
|
339 lemma "\<forall>f g z a x. FOLD f g (z::'b) (INSERT a x) = |
|
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)" |
|
341 apply (tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) |
|
342 done |
|
343 |
|
344 ML {* cterm_of @{theory} (atomize_goal @{theory} @{term "\<forall>x xa a. x = xa \<Longrightarrow> INSERT a x = INSERT a xa"}) *} |
328 |
345 |
329 (* Doesn't work with 'a, 'b, but works with 'b, 'a *) |
346 (* Doesn't work with 'a, 'b, but works with 'b, 'a *) |
330 ML {* lift_thm_g_fset @{context} @{thm fold1.simps(2)} @{term "FOLD f g (z::'b) (INSERT a x) = |
347 ML {* lift_thm_g_fset @{context} @{thm fold1.simps(2)} |
331 (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)"} *} |
|
332 |
348 |
333 ML {* lift_thm_fset @{context} @{thm append_assoc} *} |
349 ML {* lift_thm_fset @{context} @{thm append_assoc} *} |
334 ML {* lift_thm_g_fset @{context} @{thm append_assoc} @{term "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"} *} |
350 ML {* lift_thm_g_fset @{context} @{thm append_assoc} @{term "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"} *} |
335 |
351 |
336 ML {* lift_thm_fset @{context} @{thm map_append} *} |
352 ML {* lift_thm_fset @{context} @{thm map_append} *} |
337 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)"} *} |
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)"} *} |
338 ML {* lift_thm_fset @{context} @{thm list.induct} *} |
354 ML {* lift_thm_fset @{context} @{thm list.induct} *} |
339 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"} *} |
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 |
|
357 |
|
358 |
|
359 apply(tactic {* procedure_tac @{thm m1} @{context} 1 *}) |
|
360 apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) |
|
361 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *}) |
|
362 apply(tactic {* clean_tac @{context} quot defs reps_same 1 *}) |
|
363 apply(tactic {* TRY' (REPEAT_ALL_NEW (allex_prs_tac @{context} quot)) 1 *}) |
|
364 apply(tactic {* TRY' (REPEAT_ALL_NEW (lambda_prs_tac @{context} quot)) 1 *}) |
|
365 ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *} |
|
366 apply(tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1*}) |
|
367 apply(tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *}) |
|
368 |
|
369 |
|
370 |
340 |
371 |
341 (*ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *}*) |
372 (*ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *}*) |
342 |
373 |
343 quotient_def |
374 quotient_def |
344 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
375 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
372 |
403 |
373 thm list.recs(2) |
404 thm list.recs(2) |
374 ML {* lift_thm_fset @{context} @{thm list.recs(2)} *} |
405 ML {* lift_thm_fset @{context} @{thm list.recs(2)} *} |
375 ML {* lift_thm_g_fset @{context} @{thm list.recs(2)} @{term "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"} *} |
406 ML {* lift_thm_g_fset @{context} @{thm list.recs(2)} @{term "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"} *} |
376 |
407 |
377 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
|
378 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *} |
|
379 ML {* val consts = lookup_quot_consts defs *} |
|
380 |
408 |
381 ML {* val gl = @{term "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"} *} |
409 ML {* val gl = @{term "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"} *} |
382 ML {* val t_a = atomize_thm @{thm list.recs(2)} *} |
410 ML {* val t_a = atomize_thm @{thm list.recs(2)} *} |
383 ML {* val qtrm = atomize_goal @{theory} gl *} |
411 ML {* val qtrm = atomize_goal @{theory} gl *} |
384 ML {* val rg = cterm_of @{theory}(Syntax.check_term @{context} (REGULARIZE_trm @{context} (prop_of t_a) qtrm)) *} |
412 ML {* val rg = cterm_of @{theory}(Syntax.check_term @{context} (REGULARIZE_trm @{context} (prop_of t_a) qtrm)) *} |