equal
deleted
inserted
replaced
727 assumes "\<And>I. split I \<noteq> []" |
727 assumes "\<And>I. split I \<noteq> []" |
728 shows "split_domain split I \<noteq> []" |
728 shows "split_domain split I \<noteq> []" |
729 using last_in_set assms |
729 using last_in_set assms |
730 by (induction I, auto) |
730 by (induction I, auto) |
731 |
731 |
|
732 lemma lower_split_interval1: "lower (fst (split_interval X m)) = min (lower X) m" |
|
733 and lower_split_interval2: "lower (snd (split_interval X m)) = min (upper X) m" |
|
734 and upper_split_interval1: "upper (fst (split_interval X m)) = max (lower X) m" |
|
735 and upper_split_interval2: "upper (snd (split_interval X m)) = max (upper X) m" |
|
736 subgoal by transfer auto |
|
737 subgoal by transfer (auto simp: min.commute) |
|
738 subgoal by transfer (auto simp: ) |
|
739 subgoal by transfer (auto simp: ) |
|
740 done |
732 |
741 |
733 lemma split_intervalD: "split_interval X x = (A, B) \<Longrightarrow> set_of X \<subseteq> set_of A \<union> set_of B" |
742 lemma split_intervalD: "split_interval X x = (A, B) \<Longrightarrow> set_of X \<subseteq> set_of A \<union> set_of B" |
734 unfolding set_of_eq |
743 unfolding set_of_eq |
735 by transfer (auto simp: min_def max_def split: if_splits) |
744 by transfer (auto simp: min_def max_def split: if_splits) |
736 |
745 |