equal
deleted
inserted
replaced
301 ML {* fun lift_tac_fset lthy t = lift_tac lthy t *} |
301 ML {* fun lift_tac_fset lthy t = lift_tac lthy t *} |
302 |
302 |
303 lemma "IN x EMPTY = False" |
303 lemma "IN x EMPTY = False" |
304 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *}) |
304 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *}) |
305 apply(tactic {* regularize_tac @{context} 1 *}) |
305 apply(tactic {* regularize_tac @{context} 1 *}) |
306 apply(tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
306 apply(tactic {* all_inj_repabs_tac @{context} 1 *}) |
307 apply(tactic {* clean_tac @{context} 1*}) |
307 apply(tactic {* clean_tac @{context} 1*}) |
308 done |
308 done |
309 |
309 |
310 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)" |
310 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)" |
311 by (tactic {* lift_tac_fset @{context} @{thm m2} 1 *}) |
311 by (tactic {* lift_tac_fset @{context} @{thm m2} 1 *}) |
328 |
328 |
329 lemma "FOLD f g (z::'b) (INSERT a x) = |
329 lemma "FOLD f g (z::'b) (INSERT a x) = |
330 (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 (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 apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) |
331 apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) |
332 done |
332 done |
333 |
|
334 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *} |
|
335 |
333 |
336 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" |
334 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" |
337 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *}) |
335 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *}) |
338 done |
336 done |
339 |
337 |
346 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) |
344 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) |
347 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) |
345 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) |
348 apply(tactic {* regularize_tac @{context} 1 *}) |
346 apply(tactic {* regularize_tac @{context} 1 *}) |
349 defer |
347 defer |
350 apply(tactic {* clean_tac @{context} 1 *}) |
348 apply(tactic {* clean_tac @{context} 1 *}) |
351 apply(tactic {* inj_repabs_tac_fset @{context} 1*})+ |
349 apply(tactic {* inj_repabs_tac @{context} 1*})+ |
352 done |
350 done |
353 |
351 |
354 lemma list_induct_part: |
352 lemma list_induct_part: |
355 assumes a: "P (x :: 'a list) ([] :: 'c list)" |
353 assumes a: "P (x :: 'a list) ([] :: 'c list)" |
356 assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)" |
354 assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)" |
388 quotient_def |
386 quotient_def |
389 INSERT2 :: "'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2" |
387 INSERT2 :: "'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2" |
390 where |
388 where |
391 "INSERT2 \<equiv> op #" |
389 "INSERT2 \<equiv> op #" |
392 |
390 |
393 ML {* val quot = @{thms Quotient_fset Quotient_fset2} *} |
|
394 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *} |
|
395 ML {* fun lift_tac_fset lthy t = lift_tac lthy t *} |
|
396 |
|
397 lemma "P (x :: 'a fset2) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l" |
391 lemma "P (x :: 'a fset2) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l" |
398 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) |
392 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) |
399 done |
393 done |
400 |
394 |
401 lemma "P (x :: 'a fset) (EMPTY2 :: 'c fset2) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT2 e t)) \<Longrightarrow> P x l" |
395 lemma "P (x :: 'a fset) (EMPTY2 :: 'c fset2) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT2 e t)) \<Longrightarrow> P x l" |
423 lemma list_case_rsp[quotient_rsp]: |
417 lemma list_case_rsp[quotient_rsp]: |
424 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case" |
418 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case" |
425 apply (auto) |
419 apply (auto) |
426 sorry |
420 sorry |
427 |
421 |
428 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *} |
|
429 ML {* fun lift_tac_fset lthy t = lift_tac lthy t *} |
|
430 |
|
431 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)" |
422 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)" |
432 apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *}) |
423 apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *}) |
433 done |
424 done |
434 |
425 |
435 lemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa" |
426 lemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa" |