40 apply (rule_tac x = "1" in exI, simp) |
40 apply (rule_tac x = "1" in exI, simp) |
41 apply (rule_tac x = "abs c" in exI, auto) |
41 apply (rule_tac x = "abs c" in exI, auto) |
42 proof - |
42 proof - |
43 fix c :: 'a and x :: 'b |
43 fix c :: 'a and x :: 'b |
44 assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>" |
44 assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>" |
45 have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> \<bar>x\<^isub>1\<bar>" by (metis abs_ge_zero) |
45 have F1: "\<forall>x\<^sub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> \<bar>x\<^sub>1\<bar>" by (metis abs_ge_zero) |
46 have F2: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1) |
46 have F2: "\<forall>x\<^sub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^sub>1 = x\<^sub>1" by (metis mult_1) |
47 have F3: "\<forall>x\<^isub>1 x\<^isub>3. x\<^isub>3 \<le> \<bar>h x\<^isub>1\<bar> \<longrightarrow> x\<^isub>3 \<le> c * \<bar>f x\<^isub>1\<bar>" by (metis A1 order_trans) |
47 have F3: "\<forall>x\<^sub>1 x\<^sub>3. x\<^sub>3 \<le> \<bar>h x\<^sub>1\<bar> \<longrightarrow> x\<^sub>3 \<le> c * \<bar>f x\<^sub>1\<bar>" by (metis A1 order_trans) |
48 have F4: "\<forall>x\<^isub>2 x\<^isub>3\<Colon>'a\<Colon>linordered_idom. \<bar>x\<^isub>3\<bar> * \<bar>x\<^isub>2\<bar> = \<bar>x\<^isub>3 * x\<^isub>2\<bar>" |
48 have F4: "\<forall>x\<^sub>2 x\<^sub>3\<Colon>'a\<Colon>linordered_idom. \<bar>x\<^sub>3\<bar> * \<bar>x\<^sub>2\<bar> = \<bar>x\<^sub>3 * x\<^sub>2\<bar>" |
49 by (metis abs_mult) |
49 by (metis abs_mult) |
50 have F5: "\<forall>x\<^isub>3 x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> x\<^isub>1 \<longrightarrow> \<bar>x\<^isub>3 * x\<^isub>1\<bar> = \<bar>x\<^isub>3\<bar> * x\<^isub>1" |
50 have F5: "\<forall>x\<^sub>3 x\<^sub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> x\<^sub>1 \<longrightarrow> \<bar>x\<^sub>3 * x\<^sub>1\<bar> = \<bar>x\<^sub>3\<bar> * x\<^sub>1" |
51 by (metis abs_mult_pos) |
51 by (metis abs_mult_pos) |
52 hence "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = \<bar>1\<bar> * x\<^isub>1" by (metis F2) |
52 hence "\<forall>x\<^sub>1\<ge>0. \<bar>x\<^sub>1\<Colon>'a\<Colon>linordered_idom\<bar> = \<bar>1\<bar> * x\<^sub>1" by (metis F2) |
53 hence "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F2 abs_one) |
53 hence "\<forall>x\<^sub>1\<ge>0. \<bar>x\<^sub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^sub>1" by (metis F2 abs_one) |
54 hence "\<forall>x\<^isub>3. 0 \<le> \<bar>h x\<^isub>3\<bar> \<longrightarrow> \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>" by (metis F3) |
54 hence "\<forall>x\<^sub>3. 0 \<le> \<bar>h x\<^sub>3\<bar> \<longrightarrow> \<bar>c * \<bar>f x\<^sub>3\<bar>\<bar> = c * \<bar>f x\<^sub>3\<bar>" by (metis F3) |
55 hence "\<forall>x\<^isub>3. \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>" by (metis F1) |
55 hence "\<forall>x\<^sub>3. \<bar>c * \<bar>f x\<^sub>3\<bar>\<bar> = c * \<bar>f x\<^sub>3\<bar>" by (metis F1) |
56 hence "\<forall>x\<^isub>3. (0\<Colon>'a) \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c\<bar> * \<bar>f x\<^isub>3\<bar>" by (metis F5) |
56 hence "\<forall>x\<^sub>3. (0\<Colon>'a) \<le> \<bar>f x\<^sub>3\<bar> \<longrightarrow> c * \<bar>f x\<^sub>3\<bar> = \<bar>c\<bar> * \<bar>f x\<^sub>3\<bar>" by (metis F5) |
57 hence "\<forall>x\<^isub>3. (0\<Colon>'a) \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c * f x\<^isub>3\<bar>" by (metis F4) |
57 hence "\<forall>x\<^sub>3. (0\<Colon>'a) \<le> \<bar>f x\<^sub>3\<bar> \<longrightarrow> c * \<bar>f x\<^sub>3\<bar> = \<bar>c * f x\<^sub>3\<bar>" by (metis F4) |
58 hence "\<forall>x\<^isub>3. c * \<bar>f x\<^isub>3\<bar> = \<bar>c * f x\<^isub>3\<bar>" by (metis F1) |
58 hence "\<forall>x\<^sub>3. c * \<bar>f x\<^sub>3\<bar> = \<bar>c * f x\<^sub>3\<bar>" by (metis F1) |
59 hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1) |
59 hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1) |
60 thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F4) |
60 thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F4) |
61 qed |
61 qed |
62 |
62 |
63 sledgehammer_params [isar_proofs, isar_compress = 2] |
63 sledgehammer_params [isar_proofs, isar_compress = 2] |
71 apply (rule_tac x = "1" in exI, simp) |
71 apply (rule_tac x = "1" in exI, simp) |
72 apply (rule_tac x = "abs c" in exI, auto) |
72 apply (rule_tac x = "abs c" in exI, auto) |
73 proof - |
73 proof - |
74 fix c :: 'a and x :: 'b |
74 fix c :: 'a and x :: 'b |
75 assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>" |
75 assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>" |
76 have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1) |
76 have F1: "\<forall>x\<^sub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^sub>1 = x\<^sub>1" by (metis mult_1) |
77 have F2: "\<forall>x\<^isub>2 x\<^isub>3\<Colon>'a\<Colon>linordered_idom. \<bar>x\<^isub>3\<bar> * \<bar>x\<^isub>2\<bar> = \<bar>x\<^isub>3 * x\<^isub>2\<bar>" |
77 have F2: "\<forall>x\<^sub>2 x\<^sub>3\<Colon>'a\<Colon>linordered_idom. \<bar>x\<^sub>3\<bar> * \<bar>x\<^sub>2\<bar> = \<bar>x\<^sub>3 * x\<^sub>2\<bar>" |
78 by (metis abs_mult) |
78 by (metis abs_mult) |
79 have "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F1 abs_mult_pos abs_one) |
79 have "\<forall>x\<^sub>1\<ge>0. \<bar>x\<^sub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^sub>1" by (metis F1 abs_mult_pos abs_one) |
80 hence "\<forall>x\<^isub>3. \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>" by (metis A1 abs_ge_zero order_trans) |
80 hence "\<forall>x\<^sub>3. \<bar>c * \<bar>f x\<^sub>3\<bar>\<bar> = c * \<bar>f x\<^sub>3\<bar>" by (metis A1 abs_ge_zero order_trans) |
81 hence "\<forall>x\<^isub>3. 0 \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c * f x\<^isub>3\<bar>" by (metis F2 abs_mult_pos) |
81 hence "\<forall>x\<^sub>3. 0 \<le> \<bar>f x\<^sub>3\<bar> \<longrightarrow> c * \<bar>f x\<^sub>3\<bar> = \<bar>c * f x\<^sub>3\<bar>" by (metis F2 abs_mult_pos) |
82 hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1 abs_ge_zero) |
82 hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1 abs_ge_zero) |
83 thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F2) |
83 thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F2) |
84 qed |
84 qed |
85 |
85 |
86 sledgehammer_params [isar_proofs, isar_compress = 3] |
86 sledgehammer_params [isar_proofs, isar_compress = 3] |
94 apply (rule_tac x = "1" in exI, simp) |
94 apply (rule_tac x = "1" in exI, simp) |
95 apply (rule_tac x = "abs c" in exI, auto) |
95 apply (rule_tac x = "abs c" in exI, auto) |
96 proof - |
96 proof - |
97 fix c :: 'a and x :: 'b |
97 fix c :: 'a and x :: 'b |
98 assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>" |
98 assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>" |
99 have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1) |
99 have F1: "\<forall>x\<^sub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^sub>1 = x\<^sub>1" by (metis mult_1) |
100 have F2: "\<forall>x\<^isub>3 x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> x\<^isub>1 \<longrightarrow> \<bar>x\<^isub>3 * x\<^isub>1\<bar> = \<bar>x\<^isub>3\<bar> * x\<^isub>1" by (metis abs_mult_pos) |
100 have F2: "\<forall>x\<^sub>3 x\<^sub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> x\<^sub>1 \<longrightarrow> \<bar>x\<^sub>3 * x\<^sub>1\<bar> = \<bar>x\<^sub>3\<bar> * x\<^sub>1" by (metis abs_mult_pos) |
101 hence "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F1 abs_one) |
101 hence "\<forall>x\<^sub>1\<ge>0. \<bar>x\<^sub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^sub>1" by (metis F1 abs_one) |
102 hence "\<forall>x\<^isub>3. 0 \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c\<bar> * \<bar>f x\<^isub>3\<bar>" by (metis F2 A1 abs_ge_zero order_trans) |
102 hence "\<forall>x\<^sub>3. 0 \<le> \<bar>f x\<^sub>3\<bar> \<longrightarrow> c * \<bar>f x\<^sub>3\<bar> = \<bar>c\<bar> * \<bar>f x\<^sub>3\<bar>" by (metis F2 A1 abs_ge_zero order_trans) |
103 thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis A1 abs_ge_zero) |
103 thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis A1 abs_ge_zero) |
104 qed |
104 qed |
105 |
105 |
106 sledgehammer_params [isar_proofs, isar_compress = 4] |
106 sledgehammer_params [isar_proofs, isar_compress = 4] |
107 |
107 |
114 apply (rule_tac x = "1" in exI, simp) |
114 apply (rule_tac x = "1" in exI, simp) |
115 apply (rule_tac x = "abs c" in exI, auto) |
115 apply (rule_tac x = "abs c" in exI, auto) |
116 proof - |
116 proof - |
117 fix c :: 'a and x :: 'b |
117 fix c :: 'a and x :: 'b |
118 assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>" |
118 assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>" |
119 have "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis mult_1) |
119 have "\<forall>x\<^sub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^sub>1 = x\<^sub>1" by (metis mult_1) |
120 hence "\<forall>x\<^isub>3. \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>" |
120 hence "\<forall>x\<^sub>3. \<bar>c * \<bar>f x\<^sub>3\<bar>\<bar> = c * \<bar>f x\<^sub>3\<bar>" |
121 by (metis A1 abs_ge_zero order_trans abs_mult_pos abs_one) |
121 by (metis A1 abs_ge_zero order_trans abs_mult_pos abs_one) |
122 hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1 abs_ge_zero abs_mult_pos abs_mult) |
122 hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1 abs_ge_zero abs_mult_pos abs_mult) |
123 thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis abs_mult) |
123 thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis abs_mult) |
124 qed |
124 qed |
125 |
125 |
457 have F1: "inverse \<bar>c\<bar> = \<bar>inverse c\<bar>" using A1 by (metis nonzero_abs_inverse) |
457 have F1: "inverse \<bar>c\<bar> = \<bar>inverse c\<bar>" using A1 by (metis nonzero_abs_inverse) |
458 have F2: "(0\<Colon>'a) < \<bar>c\<bar>" using A1 by (metis zero_less_abs_iff) |
458 have F2: "(0\<Colon>'a) < \<bar>c\<bar>" using A1 by (metis zero_less_abs_iff) |
459 have "(0\<Colon>'a) < \<bar>c\<bar> \<longrightarrow> (0\<Colon>'a) < \<bar>inverse c\<bar>" using F1 by (metis positive_imp_inverse_positive) |
459 have "(0\<Colon>'a) < \<bar>c\<bar> \<longrightarrow> (0\<Colon>'a) < \<bar>inverse c\<bar>" using F1 by (metis positive_imp_inverse_positive) |
460 hence "(0\<Colon>'a) < \<bar>inverse c\<bar>" using F2 by metis |
460 hence "(0\<Colon>'a) < \<bar>inverse c\<bar>" using F2 by metis |
461 hence F3: "(0\<Colon>'a) \<le> \<bar>inverse c\<bar>" by (metis order_le_less) |
461 hence F3: "(0\<Colon>'a) \<le> \<bar>inverse c\<bar>" by (metis order_le_less) |
462 have "\<exists>(u\<Colon>'a) SKF\<^isub>7\<Colon>'a \<Rightarrow> 'b. \<bar>g (SKF\<^isub>7 (\<bar>inverse c\<bar> * u))\<bar> \<le> u * \<bar>f (SKF\<^isub>7 (\<bar>inverse c\<bar> * u))\<bar>" |
462 have "\<exists>(u\<Colon>'a) SKF\<^sub>7\<Colon>'a \<Rightarrow> 'b. \<bar>g (SKF\<^sub>7 (\<bar>inverse c\<bar> * u))\<bar> \<le> u * \<bar>f (SKF\<^sub>7 (\<bar>inverse c\<bar> * u))\<bar>" |
463 using A2 by metis |
463 using A2 by metis |
464 hence F4: "\<exists>(u\<Colon>'a) SKF\<^isub>7\<Colon>'a \<Rightarrow> 'b. \<bar>g (SKF\<^isub>7 (\<bar>inverse c\<bar> * u))\<bar> \<le> u * \<bar>f (SKF\<^isub>7 (\<bar>inverse c\<bar> * u))\<bar> \<and> (0\<Colon>'a) \<le> \<bar>inverse c\<bar>" |
464 hence F4: "\<exists>(u\<Colon>'a) SKF\<^sub>7\<Colon>'a \<Rightarrow> 'b. \<bar>g (SKF\<^sub>7 (\<bar>inverse c\<bar> * u))\<bar> \<le> u * \<bar>f (SKF\<^sub>7 (\<bar>inverse c\<bar> * u))\<bar> \<and> (0\<Colon>'a) \<le> \<bar>inverse c\<bar>" |
465 using F3 by metis |
465 using F3 by metis |
466 hence "\<exists>(v\<Colon>'a) (u\<Colon>'a) SKF\<^isub>7\<Colon>'a \<Rightarrow> 'b. \<bar>inverse c\<bar> * \<bar>g (SKF\<^isub>7 (u * v))\<bar> \<le> u * (v * \<bar>f (SKF\<^isub>7 (u * v))\<bar>)" |
466 hence "\<exists>(v\<Colon>'a) (u\<Colon>'a) SKF\<^sub>7\<Colon>'a \<Rightarrow> 'b. \<bar>inverse c\<bar> * \<bar>g (SKF\<^sub>7 (u * v))\<bar> \<le> u * (v * \<bar>f (SKF\<^sub>7 (u * v))\<bar>)" |
467 by (metis comm_mult_left_mono) |
467 by (metis comm_mult_left_mono) |
468 thus "\<exists>ca\<Colon>'a. \<forall>x\<Colon>'b. \<bar>inverse c\<bar> * \<bar>g x\<bar> \<le> ca * \<bar>f x\<bar>" |
468 thus "\<exists>ca\<Colon>'a. \<forall>x\<Colon>'b. \<bar>inverse c\<bar> * \<bar>g x\<bar> \<le> ca * \<bar>f x\<bar>" |
469 using A2 F4 by (metis ab_semigroup_mult_class.mult_ac(1) comm_mult_left_mono) |
469 using A2 F4 by (metis ab_semigroup_mult_class.mult_ac(1) comm_mult_left_mono) |
470 qed |
470 qed |
471 |
471 |