equal
deleted
inserted
replaced
6777 assumes [transfer_rule]: "bi_unique A" |
6777 assumes [transfer_rule]: "bi_unique A" |
6778 shows "(A ===> list_all2 A ===> list_all2 A) List.insert List.insert" |
6778 shows "(A ===> list_all2 A ===> list_all2 A) List.insert List.insert" |
6779 unfolding List.insert_def [abs_def] by transfer_prover |
6779 unfolding List.insert_def [abs_def] by transfer_prover |
6780 |
6780 |
6781 lemma find_transfer [transfer_rule]: |
6781 lemma find_transfer [transfer_rule]: |
6782 "((A ===> op =) ===> list_all2 A ===> option_rel A) List.find List.find" |
6782 "((A ===> op =) ===> list_all2 A ===> rel_option A) List.find List.find" |
6783 unfolding List.find_def by transfer_prover |
6783 unfolding List.find_def by transfer_prover |
6784 |
6784 |
6785 lemma remove1_transfer [transfer_rule]: |
6785 lemma remove1_transfer [transfer_rule]: |
6786 assumes [transfer_rule]: "bi_unique A" |
6786 assumes [transfer_rule]: "bi_unique A" |
6787 shows "(A ===> list_all2 A ===> list_all2 A) remove1 remove1" |
6787 shows "(A ===> list_all2 A ===> list_all2 A) remove1 remove1" |