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 |
309 ML {* atomize_thm @{thm m1} *} |
|
310 ML {* cterm_of @{theory} (atomize_goal @{theory} @{term "IN x EMPTY = False"}) *} |
|
311 ML {* lift_thm_fset @{context} @{thm m1} *} |
309 ML {* lift_thm_fset @{context} @{thm m1} *} |
312 ML {* lift_thm_g_fset @{context} @{thm m1} @{term "IN x EMPTY = False"} *} |
310 ML {* lift_thm_g_fset @{context} @{thm m1} @{term "IN x EMPTY = False"} *} |
|
311 |
313 ML {* lift_thm_fset @{context} @{thm m2} *} |
312 ML {* lift_thm_fset @{context} @{thm m2} *} |
314 |
|
315 ML {* lift_thm_g_fset @{context} @{thm m2} @{term "IN x (INSERT y xa) = (x = y \<or> IN x xa)"} *} |
313 ML {* lift_thm_g_fset @{context} @{thm m2} @{term "IN x (INSERT y xa) = (x = y \<or> IN x xa)"} *} |
|
314 |
316 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *} |
315 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *} |
317 ML {* lift_thm_g_fset @{context} @{thm list_eq.intros(4)} @{term "INSERT a (INSERT a x) = INSERT a x"} *} |
316 ML {* lift_thm_g_fset @{context} @{thm list_eq.intros(4)} @{term "INSERT a (INSERT a x) = INSERT a x"} *} |
318 |
317 |
319 ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *} |
318 ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *} |
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_g_fset @{context} @{thm list_eq.intros(5)} @{term "x = xa \<Longrightarrow> INSERT a x = INSERT a xa"} *} |
|
320 |
321 ML {* lift_thm_fset @{context} @{thm card1_suc} *} |
321 ML {* lift_thm_fset @{context} @{thm card1_suc} *} |
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 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"} *} |
|
323 |
323 ML {* lift_thm_fset @{context} @{thm not_mem_card1} *} |
324 ML {* lift_thm_fset @{context} @{thm not_mem_card1} *} |
324 ML {* lift_thm_g_fset @{context} @{thm not_mem_card1} @{term "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))"} *} |
325 ML {* lift_thm_g_fset @{context} @{thm not_mem_card1} @{term "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))"} *} |
|
326 |
325 ML {* lift_thm_fset @{context} @{thm fold1.simps(2)} *} |
327 ML {* lift_thm_fset @{context} @{thm fold1.simps(2)} *} |
|
328 |
326 (* Doesn't work with 'a, 'b, but works with 'b, 'a *) |
329 (* Doesn't work with 'a, 'b, but works with 'b, 'a *) |
327 |
|
328 ML {* lift_thm_g_fset @{context} @{thm fold1.simps(2)} @{term "FOLD f g (z::'b) (INSERT a x) = |
330 ML {* lift_thm_g_fset @{context} @{thm fold1.simps(2)} @{term "FOLD f g (z::'b) (INSERT a x) = |
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)"} *} |
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)"} *} |
330 |
332 |
331 ML {* lift_thm_fset @{context} @{thm append_assoc} *} |
333 ML {* lift_thm_fset @{context} @{thm append_assoc} *} |
332 ML {* lift_thm_g_fset @{context} @{thm append_assoc} @{term "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"} *} |
334 ML {* lift_thm_g_fset @{context} @{thm append_assoc} @{term "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"} *} |
|
335 |
333 ML {* lift_thm_fset @{context} @{thm map_append} *} |
336 ML {* lift_thm_fset @{context} @{thm map_append} *} |
334 ML {* val gl = @{term "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"} *} |
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)"} *} |
335 |
|
336 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
|
337 ML {* val rtrm = prop_of (atomize_thm @{thm map_append}) *} |
|
338 |
|
339 ML {* val qtrm = atomize_goal @{theory} gl *} |
|
340 ML {* val a = (REGULARIZE_trm @{context} rtrm qtrm) *} |
|
341 |
|
342 ML {* val a = Syntax.check_term @{context} a *} |
|
343 ML {* val t_r = regularize_goal @{context} (atomize_thm @{thm append_assoc}) rel_eqv rel_refl goal_a *} |
|
344 |
|
345 ML {* lift_thm_g_fset @{context} @{thm map_append} gl *} |
|
346 |
|
347 |
|
348 ML {* lift_thm_fset @{context} @{thm list.induct} *} |
338 ML {* lift_thm_fset @{context} @{thm list.induct} *} |
349 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"} *} |
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"} *} |
350 |
|
351 |
|
352 |
|
353 |
340 |
354 (*ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *}*) |
341 (*ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *}*) |
355 |
342 |
356 quotient_def |
343 quotient_def |
357 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
344 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
379 |
366 |
380 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *} |
367 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *} |
381 ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *} |
368 ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *} |
382 |
369 |
383 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *} |
370 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *} |
384 |
371 ML {* fun lift_thm_g_fset lthy t g = lift_thm_goal lthy qty "fset" rsp_thms defs t g *} |
385 |
372 |
386 ML {* map (lift_thm_fset @{context}) @{thms list.recs} *} |
373 thm list.recs(2) |
|
374 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)"} *} |
|
376 |
|
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 |
|
381 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)} *} |
|
383 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)) *} |
|
385 ML {* val rg2 = cterm_of @{theory}(my_reg @{context} rel rty (prop_of t_a)) *} |
|
386 |
|
387 ML {* val t_r = regularize_goal @{context} t_a rel_eqv rel_refl qtrm *} |
|
388 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *} |
|
389 |
|
390 ML {* val rg = cterm_of @{theory}(Syntax.check_term @{context} (inj_REPABS @{context} ((prop_of t_r), qtrm))) *} |
|
391 ML {* val rg2 = cterm_of @{theory} (build_repabs_term @{context} t_r consts rty qty) *} |
|
392 ML {* val t_t = repabs_goal @{context} t_r rty quot rel_refl trans2 rsp_thms qtrm *} |
|
393 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} |
|
394 ML {* |
|
395 val lthy = @{context} |
|
396 val (alls, exs) = findallex lthy rty qty (prop_of t_a); |
|
397 val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls |
|
398 val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs |
|
399 val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t |
|
400 val abs = findabs rty (prop_of t_a); |
|
401 val aps = findaps rty (prop_of t_a); |
|
402 val app_prs_thms = map (applic_prs lthy rty qty absrep) aps; |
|
403 val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs; |
|
404 val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a; |
|
405 val defs_sym = flat (map (add_lower_defs lthy) defs); |
|
406 val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym; |
|
407 val t_id = simp_ids lthy t_l; |
|
408 val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id; |
|
409 val t_d = repeat_eqsubst_thm lthy defs_sym t_d0; |
|
410 val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; |
|
411 val t_rv = ObjectLogic.rulify t_r |
|
412 |
|
413 *} |
|
414 |
|
415 |
|
416 |
|
417 |
|
418 |
|
419 |
387 ML {* map (lift_thm_fset @{context}) @{thms list.cases} *} |
420 ML {* map (lift_thm_fset @{context}) @{thms list.cases} *} |
|
421 |
|
422 |
|
423 |
388 |
424 |
389 ML {* atomize_thm @{thm m1} *} |
425 ML {* atomize_thm @{thm m1} *} |
390 ML {* cterm_of @{theory} (atomize_goal @{theory} @{term "IN x EMPTY = False"}) *} |
426 ML {* cterm_of @{theory} (atomize_goal @{theory} @{term "IN x EMPTY = False"}) *} |
391 ML {* lift_thm_fset @{context} @{thm m1} *} |
427 ML {* lift_thm_fset @{context} @{thm m1} *} |
392 (* ML {* lift_thm_g_fset @{context} @{thm m1} @{term "IN x EMPTY = False"}) *} *) |
428 (* ML {* lift_thm_g_fset @{context} @{thm m1} @{term "IN x EMPTY = False"}) *} *) |