equal
deleted
inserted
replaced
43 | fine_Cons: |
43 | fine_Cons: |
44 "\<lbrakk>fine \<delta> (b, c) D; a < b; a \<le> x; x \<le> b; b - a < \<delta> x\<rbrakk> |
44 "\<lbrakk>fine \<delta> (b, c) D; a < b; a \<le> x; x \<le> b; b - a < \<delta> x\<rbrakk> |
45 \<Longrightarrow> fine \<delta> (a, c) ((a, x, b) # D)" |
45 \<Longrightarrow> fine \<delta> (a, c) ((a, x, b) # D)" |
46 |
46 |
47 lemmas fine_induct [induct set: fine] = |
47 lemmas fine_induct [induct set: fine] = |
48 fine.induct [of "\<delta>" "(a,b)" "D" "split P", unfolded split_conv, standard] |
48 fine.induct [of "\<delta>" "(a,b)" "D" "split P", unfolded split_conv] for \<delta> a b D P |
49 |
49 |
50 lemma fine_single: |
50 lemma fine_single: |
51 "\<lbrakk>a < b; a \<le> x; x \<le> b; b - a < \<delta> x\<rbrakk> \<Longrightarrow> fine \<delta> (a, b) [(a, x, b)]" |
51 "\<lbrakk>a < b; a \<le> x; x \<le> b; b - a < \<delta> x\<rbrakk> \<Longrightarrow> fine \<delta> (a, b) [(a, x, b)]" |
52 by (rule fine_Cons [OF fine_Nil]) |
52 by (rule fine_Cons [OF fine_Nil]) |
53 |
53 |