src/HOL/Metis_Examples/BigO.thy
 changeset 37320 06c7a2f231fe parent 36925 ffad77bb3046 child 38622 86fc906dcd86
equal inserted replaced
37319:42268dc7d6c4 37320:06c7a2f231fe
`   878 (*sledgehammer*);  `
`   878 (*sledgehammer*);  `
`   879   apply (case_tac "0 <= k x - g x")`
`   879   apply (case_tac "0 <= k x - g x")`
`   880 (* apply (metis abs_le_iff add_le_imp_le_right diff_minus le_less`
`   880 (* apply (metis abs_le_iff add_le_imp_le_right diff_minus le_less`
`   881                 le_max_iff_disj min_max.le_supE min_max.sup_absorb2`
`   881                 le_max_iff_disj min_max.le_supE min_max.sup_absorb2`
`   882                 min_max.sup_commute) *)`
`   882                 min_max.sup_commute) *)`
`   883 proof (neg_clausify)`
`   883 proof -`
`   884 fix x`
`   884   fix x :: 'a`
`   885 assume 0: "\<And>A. k A \<le> f A"`
`   885   assume "\<forall>x\<Colon>'a. k x \<le> f x"`
`   886 have 1: "\<And>(X1\<Colon>'b\<Colon>linordered_idom) X2. \<not> max X1 X2 < X1"`
`   886   hence F1: "\<forall>x\<^isub>1\<Colon>'a. max (k x\<^isub>1) (f x\<^isub>1) = f x\<^isub>1" by (metis min_max.sup_absorb2)`
`   887   by (metis linorder_not_less le_maxI1)  (*sort inserted by hand*)`
`   887   assume "(0\<Colon>'b) \<le> k x - g x"`
`   888 assume 2: "(0\<Colon>'b) \<le> k x - g x"`
`   888   hence F2: "max (0\<Colon>'b) (k x - g x) = k x - g x" by (metis min_max.sup_absorb2)`
`   889 have 3: "\<not> k x - g x < (0\<Colon>'b)"`
`   889   have F3: "\<forall>x\<^isub>1\<Colon>'b. x\<^isub>1 \<le> \<bar>x\<^isub>1\<bar>" by (metis abs_le_iff le_less)`
`   890   by (metis 2 linorder_not_less)`
`   890   have "\<forall>(x\<^isub>2\<Colon>'b) x\<^isub>1\<Colon>'b. max x\<^isub>1 x\<^isub>2 \<le> x\<^isub>2 \<or> max x\<^isub>1 x\<^isub>2 \<le> x\<^isub>1" by (metis le_less le_max_iff_disj)`
`   891 have 4: "\<And>X1 X2. min X1 (k X2) \<le> f X2"`
`   891   hence "\<forall>(x\<^isub>3\<Colon>'b) (x\<^isub>2\<Colon>'b) x\<^isub>1\<Colon>'b. x\<^isub>1 - x\<^isub>2 \<le> x\<^isub>3 - x\<^isub>2 \<or> x\<^isub>3 \<le> x\<^isub>1" by (metis add_le_imp_le_right diff_minus min_max.le_supE)`
`   892   by (metis min_max.inf_le2 min_max.le_inf_iff min_max.le_iff_inf 0)`
`   892   hence "k x - g x \<le> f x - g x" by (metis F1 le_less min_max.sup_absorb2 min_max.sup_commute)`
`   893 have 5: "\<bar>g x - f x\<bar> = f x - g x"`
`   893   hence "k x - g x \<le> \<bar>f x - g x\<bar>" by (metis F3 le_max_iff_disj min_max.sup_absorb2)`
`   894   by (metis abs_minus_commute combine_common_factor mult_zero_right minus_add_cancel minus_zero abs_if diff_less_eq min_max.inf_commute 4 linorder_not_le min_max.le_iff_inf 3 diff_less_0_iff_less linorder_not_less)`
`   894   thus "max (k x - g x) (0\<Colon>'b) \<le> \<bar>f x - g x\<bar>" by (metis F2 min_max.sup_commute)`
`   895 have 6: "max (0\<Colon>'b) (k x - g x) = k x - g x"`
`       `
`   896   by (metis min_max.le_iff_sup 2)`
`       `
`   897 assume 7: "\<not> max (k x - g x) (0\<Colon>'b) \<le> \<bar>f x - g x\<bar>"`
`       `
`   898 have 8: "\<not> k x - g x \<le> f x - g x"`
`       `
`   899   by (metis 5 abs_minus_commute 7 min_max.sup_commute 6)`
`       `
`   900 show "False"`
`       `
`   901   by (metis min_max.sup_commute min_max.inf_commute min_max.sup_inf_absorb min_max.le_iff_inf 0 max_diff_distrib_left 1 linorder_not_le 8)`
`       `
`   902 next`
`   895 next`
`   903   show "\<And>x\<Colon>'a.`
`   896   show "\<And>x\<Colon>'a.`
`   904        \<lbrakk>\<forall>x\<Colon>'a. (0\<Colon>'b) \<le> k x; \<forall>x\<Colon>'a. k x \<le> f x; \<not> (0\<Colon>'b) \<le> k x - g x\<rbrakk>`
`   897        \<lbrakk>\<forall>x\<Colon>'a. (0\<Colon>'b) \<le> k x; \<forall>x\<Colon>'a. k x \<le> f x; \<not> (0\<Colon>'b) \<le> k x - g x\<rbrakk>`
`   905        \<Longrightarrow> max (k x - g x) (0\<Colon>'b) \<le> \<bar>f x - g x\<bar>"`
`   898        \<Longrightarrow> max (k x - g x) (0\<Colon>'b) \<le> \<bar>f x - g x\<bar>"`
`   906     by (metis abs_ge_zero le_cases min_max.sup_absorb2)`
`   899     by (metis abs_ge_zero le_cases min_max.sup_absorb2)`