equal
deleted
inserted
replaced
2506 using left_total_rel_filter[of "A\<inverse>\<inverse>"] by simp |
2506 using left_total_rel_filter[of "A\<inverse>\<inverse>"] by simp |
2507 |
2507 |
2508 lemma bi_total_rel_filter [transfer_rule]: |
2508 lemma bi_total_rel_filter [transfer_rule]: |
2509 assumes "bi_total A" "bi_unique A" |
2509 assumes "bi_total A" "bi_unique A" |
2510 shows "bi_total (rel_filter A)" |
2510 shows "bi_total (rel_filter A)" |
2511 unfolding bi_total_conv_left_right using assms |
2511 unfolding bi_total_alt_def using assms |
2512 by(simp add: left_total_rel_filter right_total_rel_filter) |
2512 by(simp add: left_total_rel_filter right_total_rel_filter) |
2513 |
2513 |
2514 lemma left_unique_rel_filter [transfer_rule]: |
2514 lemma left_unique_rel_filter [transfer_rule]: |
2515 assumes "left_unique A" |
2515 assumes "left_unique A" |
2516 shows "left_unique (rel_filter A)" |
2516 shows "left_unique (rel_filter A)" |
2533 "right_unique A \<Longrightarrow> right_unique (rel_filter A)" |
2533 "right_unique A \<Longrightarrow> right_unique (rel_filter A)" |
2534 using left_unique_rel_filter[of "A\<inverse>\<inverse>"] by simp |
2534 using left_unique_rel_filter[of "A\<inverse>\<inverse>"] by simp |
2535 |
2535 |
2536 lemma bi_unique_rel_filter [transfer_rule]: |
2536 lemma bi_unique_rel_filter [transfer_rule]: |
2537 "bi_unique A \<Longrightarrow> bi_unique (rel_filter A)" |
2537 "bi_unique A \<Longrightarrow> bi_unique (rel_filter A)" |
2538 by(simp add: bi_unique_conv_left_right left_unique_rel_filter right_unique_rel_filter) |
2538 by(simp add: bi_unique_alt_def left_unique_rel_filter right_unique_rel_filter) |
2539 |
2539 |
2540 lemma top_filter_parametric [transfer_rule]: |
2540 lemma top_filter_parametric [transfer_rule]: |
2541 "bi_total A \<Longrightarrow> (rel_filter A) top top" |
2541 "bi_total A \<Longrightarrow> (rel_filter A) top top" |
2542 by(simp add: rel_filter_eventually All_transfer) |
2542 by(simp add: rel_filter_eventually All_transfer) |
2543 |
2543 |