equal
deleted
inserted
replaced
6 imports |
6 imports |
7 Derivative |
7 Derivative |
8 "~~/src/HOL/Library/Indicator_Function" |
8 "~~/src/HOL/Library/Indicator_Function" |
9 begin |
9 begin |
10 |
10 |
11 declare [[smt_certificates="Integration.certs"]] |
11 declare [[smt_certificates = "Integration.certs"]] |
12 declare [[smt_fixed=true]] |
12 declare [[smt_read_only_certificates = true]] |
13 declare [[smt_oracle=false]] |
13 declare [[smt_oracle = false]] |
14 |
14 |
15 (*declare not_less[simp] not_le[simp]*) |
15 (*declare not_less[simp] not_le[simp]*) |
16 |
16 |
17 lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib |
17 lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib |
18 scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff |
18 scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff |
5581 fix x assume x:"x \<in> s" |
5581 fix x assume x:"x \<in> s" |
5582 show "f n x \<le> Sup {f j x |j. n \<le> j}" apply(rule Sup_upper[where z="h x"]) defer |
5582 show "f n x \<le> Sup {f j x |j. n \<le> j}" apply(rule Sup_upper[where z="h x"]) defer |
5583 using assms(3)[rule_format,OF x] unfolding real_norm_def abs_le_iff by auto |
5583 using assms(3)[rule_format,OF x] unfolding real_norm_def abs_le_iff by auto |
5584 qed qed(insert n,auto) qed qed qed |
5584 qed qed(insert n,auto) qed qed qed |
5585 |
5585 |
5586 declare [[smt_certificates=""]] |
5586 declare [[smt_certificates = ""]] |
5587 declare [[smt_fixed=false]] |
5587 declare [[smt_read_only_certificates = false]] |
5588 |
5588 |
5589 end |
5589 end |