13 where |
13 where |
14 "list_eq xs ys = (\<forall>x. x \<in> set xs \<longleftrightarrow> x \<in> set ys)" |
14 "list_eq xs ys = (\<forall>x. x \<in> set xs \<longleftrightarrow> x \<in> set ys)" |
15 |
15 |
16 lemma list_eq_equivp: |
16 lemma list_eq_equivp: |
17 shows "equivp list_eq" |
17 shows "equivp list_eq" |
18 unfolding equivp_reflp_symp_transp |
18 unfolding equivp_reflp_symp_transp |
19 unfolding reflp_def symp_def transp_def |
19 unfolding reflp_def symp_def transp_def |
20 by auto |
20 by auto |
|
21 |
|
22 definition |
|
23 memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" |
|
24 where |
|
25 "memb x xs \<equiv> x \<in> set xs" |
|
26 |
|
27 definition |
|
28 sub_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
|
29 where |
|
30 "sub_list xs ys \<equiv> (\<forall>x. x \<in> set xs \<longrightarrow> x \<in> set ys)" |
|
31 |
|
32 lemma sub_list_cons: |
|
33 "sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)" |
|
34 by (auto simp add: memb_def sub_list_def) |
|
35 |
|
36 lemma nil_not_cons: |
|
37 shows "\<not> ([] \<approx> x # xs)" |
|
38 and "\<not> (x # xs \<approx> [])" |
|
39 by auto |
|
40 |
|
41 lemma sub_list_rsp1: "\<lbrakk>xs \<approx> ys\<rbrakk> \<Longrightarrow> sub_list xs zs = sub_list ys zs" |
|
42 by (simp add: sub_list_def) |
|
43 |
|
44 lemma sub_list_rsp2: "\<lbrakk>xs \<approx> ys\<rbrakk> \<Longrightarrow> sub_list zs xs = sub_list zs ys" |
|
45 by (simp add: sub_list_def) |
|
46 |
|
47 lemma [quot_respect]: |
|
48 "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list" |
|
49 by (auto simp only: fun_rel_def sub_list_rsp1 sub_list_rsp2) |
21 |
50 |
22 quotient_type |
51 quotient_type |
23 'a fset = "'a list" / "list_eq" |
52 'a fset = "'a list" / "list_eq" |
24 by (rule list_eq_equivp) |
53 by (rule list_eq_equivp) |
25 |
54 |
349 apply (simp) |
368 apply (simp) |
350 apply (simp add: memb_cons_iff memb_def) |
369 apply (simp add: memb_cons_iff memb_def) |
351 apply auto |
370 apply auto |
352 apply (drule_tac x="e" in spec) |
371 apply (drule_tac x="e" in spec) |
353 apply blast |
372 apply blast |
354 apply (simp add: memb_cons_iff) |
373 apply (case_tac b) |
355 apply (metis Nitpick.list_size_simp(2) ffold_raw.simps(2) |
374 apply simp_all |
356 length_Suc_conv memb_absorb nil_not_cons(2)) |
|
357 apply (subgoal_tac "ffold_raw f z b = f a1 (ffold_raw f z (delete_raw b a1))") |
375 apply (subgoal_tac "ffold_raw f z b = f a1 (ffold_raw f z (delete_raw b a1))") |
358 apply (simp only:) |
376 apply (simp only:) |
359 apply (rule_tac f="f a1" in arg_cong) |
377 apply (rule_tac f="f a1" in arg_cong) |
360 apply (subgoal_tac "\<forall>e. memb e a2 = memb e (delete_raw b a1)") |
378 apply (subgoal_tac "\<forall>e. memb e a2 = memb e (delete_raw b a1)") |
361 apply simp |
379 apply simp |
362 apply (simp add: memb_delete_raw) |
380 apply (simp add: memb_delete_raw) |
363 apply (auto simp add: memb_cons_iff)[1] |
381 apply (auto simp add: memb_cons_iff)[1] |
364 apply (erule memb_commute_ffold_raw) |
382 apply (erule memb_commute_ffold_raw) |
365 apply (drule_tac x="a1" in spec) |
383 apply (drule_tac x="a1" in spec) |
366 apply (simp add: memb_cons_iff) |
384 apply (simp add: memb_cons_iff) |
367 apply (metis Nitpick.list_size_simp(2) ffold_raw.simps(2) |
385 apply (simp add: memb_cons_iff) |
368 length_Suc_conv memb_absorb memb_cons_iff nil_not_cons(2)) |
386 apply (case_tac b) |
|
387 apply simp_all |
369 done |
388 done |
370 |
389 |
371 lemma [quot_respect]: |
390 lemma [quot_respect]: |
372 "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw" |
391 "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw" |
373 by (simp add: memb_def[symmetric] ffold_raw_rsp_pre) |
392 by (simp add: memb_def[symmetric] ffold_raw_rsp_pre) |
439 |
458 |
440 lemma list_equiv_rsp[quot_respect]: |
459 lemma list_equiv_rsp[quot_respect]: |
441 shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>" |
460 shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>" |
442 by auto |
461 by auto |
443 |
462 |
|
463 text {* alternate formulation with a different decomposition principle |
|
464 and a proof of equivalence *} |
|
465 |
|
466 inductive |
|
467 list_eq2 |
|
468 where |
|
469 "list_eq2 (a # b # xs) (b # a # xs)" |
|
470 | "list_eq2 [] []" |
|
471 | "list_eq2 xs ys \<Longrightarrow> list_eq2 ys xs" |
|
472 | "list_eq2 (a # a # xs) (a # xs)" |
|
473 | "list_eq2 xs ys \<Longrightarrow> list_eq2 (a # xs) (a # ys)" |
|
474 | "\<lbrakk>list_eq2 xs1 xs2; list_eq2 xs2 xs3\<rbrakk> \<Longrightarrow> list_eq2 xs1 xs3" |
|
475 |
|
476 lemma list_eq2_refl: |
|
477 shows "list_eq2 xs xs" |
|
478 by (induct xs) (auto intro: list_eq2.intros) |
|
479 |
|
480 lemma cons_delete_list_eq2: |
|
481 shows "list_eq2 (a # (delete_raw A a)) (if memb a A then A else a # A)" |
|
482 apply (induct A) |
|
483 apply (simp add: memb_def list_eq2_refl) |
|
484 apply (case_tac "memb a (aa # A)") |
|
485 apply (simp_all only: memb_cons_iff) |
|
486 apply (case_tac [!] "a = aa") |
|
487 apply (simp_all add: delete_raw.simps) |
|
488 apply (case_tac "memb a A") |
|
489 apply (auto simp add: memb_def)[2] |
|
490 apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6)) |
|
491 apply (metis delete_raw.simps(2) list_eq2.intros(1) list_eq2.intros(5) list_eq2.intros(6)) |
|
492 apply (auto simp add: list_eq2_refl not_memb_delete_raw_ident) |
|
493 done |
|
494 |
|
495 lemma memb_delete_list_eq2: |
|
496 assumes a: "memb e r" |
|
497 shows "list_eq2 (e # delete_raw r e) r" |
|
498 using a cons_delete_list_eq2[of e r] |
|
499 by simp |
|
500 |
|
501 lemma list_eq2_equiv_aux: |
|
502 assumes a: "fcard_raw l = n" |
|
503 and b: "l \<approx> r" |
|
504 shows "list_eq2 l r" |
|
505 using a b |
|
506 proof (induct n arbitrary: l r) |
|
507 case 0 |
|
508 have "fcard_raw l = 0" by fact |
|
509 then have "\<forall>x. \<not> memb x l" using memb_card_not_0[of _ l] by auto |
|
510 then have z: "l = []" using no_memb_nil by auto |
|
511 then have "r = []" sorry |
|
512 then show ?case using z list_eq2_refl by simp |
|
513 next |
|
514 case (Suc m) |
|
515 have b: "l \<approx> r" by fact |
|
516 have d: "fcard_raw l = Suc m" by fact |
|
517 have "\<exists>a. memb a l" by (rule fcard_raw_suc_memb[OF d]) |
|
518 then obtain a where e: "memb a l" by auto |
|
519 then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b by auto |
|
520 have f: "fcard_raw (delete_raw l a) = m" using fcard_raw_delete[of l a] e d by simp |
|
521 have g: "delete_raw l a \<approx> delete_raw r a" using delete_raw_rsp[OF b] by simp |
|
522 have g': "list_eq2 (delete_raw l a) (delete_raw r a)" by (rule Suc.hyps[OF f g]) |
|
523 have h: "list_eq2 (a # delete_raw l a) (a # delete_raw r a)" by (rule list_eq2.intros(5)[OF g']) |
|
524 have i: "list_eq2 l (a # delete_raw l a)" by (rule list_eq2.intros(3)[OF memb_delete_list_eq2[OF e]]) |
|
525 have "list_eq2 l (a # delete_raw r a)" by (rule list_eq2.intros(6)[OF i h]) |
|
526 then show ?case using list_eq2.intros(6)[OF _ memb_delete_list_eq2[OF e']] by simp |
|
527 qed |
|
528 |
|
529 lemma list_eq2_equiv: |
|
530 "(l \<approx> r) \<longleftrightarrow> (list_eq2 l r)" |
|
531 proof |
|
532 show "list_eq2 l r \<Longrightarrow> l \<approx> r" by (induct rule: list_eq2.induct) auto |
|
533 show "l \<approx> r \<Longrightarrow> list_eq2 l r" using list_eq2_equiv_aux by blast |
|
534 qed |
|
535 |
444 section {* lifted part *} |
536 section {* lifted part *} |
445 |
537 |
446 lemma not_fin_fnil: "x |\<notin>| {||}" |
538 lemma not_fin_fnil: "x |\<notin>| {||}" |
447 by (lifting not_memb_nil) |
539 by (lifting not_memb_nil) |
448 |
540 |
529 |
621 |
530 lemma fcard_suc_memb: "fcard A = Suc n \<Longrightarrow> \<exists>a. a |\<in>| A" |
622 lemma fcard_suc_memb: "fcard A = Suc n \<Longrightarrow> \<exists>a. a |\<in>| A" |
531 by (lifting fcard_raw_suc_memb) |
623 by (lifting fcard_raw_suc_memb) |
532 |
624 |
533 lemma fin_fcard_not_0: "a |\<in>| A \<Longrightarrow> fcard A \<noteq> 0" |
625 lemma fin_fcard_not_0: "a |\<in>| A \<Longrightarrow> fcard A \<noteq> 0" |
534 by (lifting mem_card_not_0) |
626 by (lifting memb_card_not_0) |
535 |
627 |
536 text {* funion *} |
628 text {* funion *} |
537 |
629 |
538 lemma funion_simps[simp]: |
630 lemma funion_simps[simp]: |
539 shows "{||} |\<union>| S = S" |
631 shows "{||} |\<union>| S = S" |
540 and "finsert x S |\<union>| T = finsert x (S |\<union>| T)" |
632 and "finsert x S |\<union>| T = finsert x (S |\<union>| T)" |
541 by (lifting append.simps) |
633 by (lifting append.simps) |
542 |
634 |
|
635 lemma funion_empty[simp]: |
|
636 shows "S |\<union>| {||} = S" |
|
637 by (lifting append_Nil2) |
|
638 |
543 lemma funion_sym: |
639 lemma funion_sym: |
544 shows "S |\<union>| T = T |\<union>| S" |
640 shows "S |\<union>| T = T |\<union>| S" |
545 by (lifting funion_sym_pre) |
641 by (lifting funion_sym_pre) |
546 |
642 |
547 lemma funion_assoc: |
643 lemma funion_assoc: |
548 shows "S |\<union>| T |\<union>| U = S |\<union>| (T |\<union>| U)" |
644 shows "S |\<union>| T |\<union>| U = S |\<union>| (T |\<union>| U)" |
549 by (lifting append_assoc) |
645 by (lifting append_assoc) |
|
646 |
|
647 lemma singleton_union_left: |
|
648 "{|a|} |\<union>| S = finsert a S" |
|
649 by simp |
|
650 |
|
651 lemma singleton_union_right: |
|
652 "S |\<union>| {|a|} = finsert a S" |
|
653 by (subst funion_sym) simp |
550 |
654 |
551 section {* Induction and Cases rules for finite sets *} |
655 section {* Induction and Cases rules for finite sets *} |
552 |
656 |
553 lemma fset_strong_cases: |
657 lemma fset_strong_cases: |
554 "S = {||} \<or> (\<exists>x T. x |\<notin>| T \<and> S = finsert x T)" |
658 "S = {||} \<or> (\<exists>x T. x |\<notin>| T \<and> S = finsert x T)" |
668 |
772 |
669 lemma expand_fset_eq: |
773 lemma expand_fset_eq: |
670 "(S = T) = (\<forall>x. (x |\<in>| S) = (x |\<in>| T))" |
774 "(S = T) = (\<forall>x. (x |\<in>| S) = (x |\<in>| T))" |
671 by (lifting list_eq.simps[simplified memb_def[symmetric]]) |
775 by (lifting list_eq.simps[simplified memb_def[symmetric]]) |
672 |
776 |
|
777 (* We cannot write it as "assumes .. shows" since Isabelle changes |
|
778 the quantifiers to schematic variables and reintroduces them in |
|
779 a different order *) |
|
780 lemma fset_eq_cases: |
|
781 "\<lbrakk>a1 = a2; |
|
782 \<And>a b xs. \<lbrakk>a1 = finsert a (finsert b xs); a2 = finsert b (finsert a xs)\<rbrakk> \<Longrightarrow> P; |
|
783 \<lbrakk>a1 = {||}; a2 = {||}\<rbrakk> \<Longrightarrow> P; \<And>xs ys. \<lbrakk>a1 = ys; a2 = xs; xs = ys\<rbrakk> \<Longrightarrow> P; |
|
784 \<And>a xs. \<lbrakk>a1 = finsert a (finsert a xs); a2 = finsert a xs\<rbrakk> \<Longrightarrow> P; |
|
785 \<And>xs ys a. \<lbrakk>a1 = finsert a xs; a2 = finsert a ys; xs = ys\<rbrakk> \<Longrightarrow> P; |
|
786 \<And>xs1 xs2 xs3. \<lbrakk>a1 = xs1; a2 = xs3; xs1 = xs2; xs2 = xs3\<rbrakk> \<Longrightarrow> P\<rbrakk> |
|
787 \<Longrightarrow> P" |
|
788 by (lifting list_eq2.cases[simplified list_eq2_equiv[symmetric]]) |
|
789 |
|
790 lemma fset_eq_induct: |
|
791 assumes "x1 = x2" |
|
792 and "\<And>a b xs. P (finsert a (finsert b xs)) (finsert b (finsert a xs))" |
|
793 and "P {||} {||}" |
|
794 and "\<And>xs ys. \<lbrakk>xs = ys; P xs ys\<rbrakk> \<Longrightarrow> P ys xs" |
|
795 and "\<And>a xs. P (finsert a (finsert a xs)) (finsert a xs)" |
|
796 and "\<And>xs ys a. \<lbrakk>xs = ys; P xs ys\<rbrakk> \<Longrightarrow> P (finsert a xs) (finsert a ys)" |
|
797 and "\<And>xs1 xs2 xs3. \<lbrakk>xs1 = xs2; P xs1 xs2; xs2 = xs3; P xs2 xs3\<rbrakk> \<Longrightarrow> P xs1 xs3" |
|
798 shows "P x1 x2" |
|
799 using assms |
|
800 by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]]) |
673 |
801 |
674 ML {* |
802 ML {* |
675 fun dest_fsetT (Type ("FSet.fset", [T])) = T |
803 fun dest_fsetT (Type ("FSet.fset", [T])) = T |
676 | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); |
804 | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); |
677 *} |
805 *} |