equal
deleted
inserted
replaced
3763 by (cases "x = y") (auto intro: insort_key_left_comm) |
3763 by (cases "x = y") (auto intro: insort_key_left_comm) |
3764 |
3764 |
3765 lemma fun_left_comm_insort: |
3765 lemma fun_left_comm_insort: |
3766 "fun_left_comm insort" |
3766 "fun_left_comm insort" |
3767 proof |
3767 proof |
3768 qed (fact insort_left_comm) |
3768 qed (simp add: insort_left_comm fun_eq_iff) |
3769 |
3769 |
3770 lemma sort_key_simps [simp]: |
3770 lemma sort_key_simps [simp]: |
3771 "sort_key f [] = []" |
3771 "sort_key f [] = []" |
3772 "sort_key f (x#xs) = insort_key f x (sort_key f xs)" |
3772 "sort_key f (x#xs) = insort_key f x (sort_key f xs)" |
3773 by (simp_all add: sort_key_def) |
3773 by (simp_all add: sort_key_def) |