equal
deleted
inserted
replaced
6580 then show ?thesis |
6580 then show ?thesis |
6581 unfolding Domainp_iff[abs_def] |
6581 unfolding Domainp_iff[abs_def] |
6582 by (auto iff: fun_eq_iff) |
6582 by (auto iff: fun_eq_iff) |
6583 qed |
6583 qed |
6584 |
6584 |
6585 lemma reflp_list_all2[reflexivity_rule]: |
|
6586 assumes "reflp R" |
|
6587 shows "reflp (list_all2 R)" |
|
6588 proof (rule reflpI) |
|
6589 from assms have *: "\<And>xs. R xs xs" by (rule reflpE) |
|
6590 fix xs |
|
6591 show "list_all2 R xs xs" |
|
6592 by (induct xs) (simp_all add: *) |
|
6593 qed |
|
6594 |
|
6595 lemma left_total_list_all2[reflexivity_rule]: |
6585 lemma left_total_list_all2[reflexivity_rule]: |
6596 "left_total R \<Longrightarrow> left_total (list_all2 R)" |
6586 "left_total R \<Longrightarrow> left_total (list_all2 R)" |
6597 unfolding left_total_def |
6587 unfolding left_total_def |
6598 apply safe |
6588 apply safe |
6599 apply (rename_tac xs, induct_tac xs, simp, simp add: list_all2_Cons1) |
6589 apply (rename_tac xs, induct_tac xs, simp, simp add: list_all2_Cons1) |