equal
deleted
inserted
replaced
73 "right_unique A \<Longrightarrow> right_unique (rel_set A)" |
73 "right_unique A \<Longrightarrow> right_unique (rel_set A)" |
74 unfolding right_unique_def rel_set_def by fast |
74 unfolding right_unique_def rel_set_def by fast |
75 |
75 |
76 lemma bi_total_rel_set [transfer_rule]: |
76 lemma bi_total_rel_set [transfer_rule]: |
77 "bi_total A \<Longrightarrow> bi_total (rel_set A)" |
77 "bi_total A \<Longrightarrow> bi_total (rel_set A)" |
78 by(simp add: bi_total_conv_left_right left_total_rel_set right_total_rel_set) |
78 by(simp add: bi_total_alt_def left_total_rel_set right_total_rel_set) |
79 |
79 |
80 lemma bi_unique_rel_set [transfer_rule]: |
80 lemma bi_unique_rel_set [transfer_rule]: |
81 "bi_unique A \<Longrightarrow> bi_unique (rel_set A)" |
81 "bi_unique A \<Longrightarrow> bi_unique (rel_set A)" |
82 unfolding bi_unique_def rel_set_def by fast |
82 unfolding bi_unique_def rel_set_def by fast |
83 |
83 |