# HG changeset patch
# User paulson
# Date 1189090443 -7200
# Node ID f406a57447562fe8e0b565dab51f0e4fce91c6a6
# Parent  da7de38392df7f755e296f53467a7280cdb7bf57
new proofs found

diff -r da7de38392df -r f406a5744756 src/HOL/MetisExamples/BigO.thy
--- a/src/HOL/MetisExamples/BigO.thy	Thu Sep 06 16:28:42 2007 +0200
+++ b/src/HOL/MetisExamples/BigO.thy	Thu Sep 06 16:54:03 2007 +0200
@@ -409,8 +409,45 @@
 
 
 ML{*ResReconstruct.modulus:=1*}
+
+(*Vampire finds this structured proof*)
+lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom). 
+    ALL x. (abs (h x)) <= (c * (abs (f x))))
+      = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
+  apply auto
+  apply (case_tac "c = 0", simp)
+  apply (rule_tac x = "1" in exI, simp)
+  apply (rule_tac x = "abs c" in exI, auto);
+proof (neg_clausify)
+fix c x  (*sort/type constraint inserted by hand!*)
+have 0: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2. \<bar>X1 * \<bar>X2\<bar>\<bar> = \<bar>X1 * X2\<bar>"
+  by (metis abs_ge_zero abs_mult_pos abs_mult)
+assume 1: "\<And>A. \<bar>h A\<bar> \<le> c * \<bar>f A\<bar>"
+have 2: "\<And>X1 X2. \<not> \<bar>X1\<bar> \<le> X2 \<or> (0\<Colon>'a) \<le> X2"
+  by (metis abs_ge_zero order_trans)
+have 3: "\<And>X1. (0\<Colon>'a) \<le> c * \<bar>f X1\<bar>"
+  by (metis 1 2)
+have 4: "\<And>X1. c * \<bar>f X1\<bar> = \<bar>c * f X1\<bar>"
+  by (metis 0 abs_of_nonneg 3)
+have 5: "\<And>X1. - h X1 \<le> c * \<bar>f X1\<bar>"
+  by (metis 1 abs_le_D2)
+have 6: "\<And>X1. - h X1 \<le> \<bar>c * f X1\<bar>"
+  by (metis 4 5)
+have 7: "\<And>X1. h X1 \<le> c * \<bar>f X1\<bar>"
+  by (metis 1 abs_le_D1)
+have 8: "\<And>X1. h X1 \<le> \<bar>c * f X1\<bar>"
+  by (metis 4 7)
+assume 9: "\<not> \<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>"
+have 10: "\<not> \<bar>h x\<bar> \<le> \<bar>c * f x\<bar>"
+  by (metis abs_mult 9)
+show "False"
+  by (metis 6 8 10 abs_leI)
+qed
+
+
 ML{*ResReconstruct.recon_sorts:=true*}
 
+
 lemma bigo_alt_def: "O(f) = 
     {h. EX c. (0 < c & (ALL x. abs (h x) <= c * abs (f x)))}"
 by (auto simp add: bigo_def bigo_pos_const)
@@ -1433,26 +1470,28 @@
 apply (erule thin_rl)
 (*sledgehammer*);  
   apply (case_tac "0 <= k x - g x")
-  apply (simp del: compare_rls diff_minus);
-  apply (subst abs_of_nonneg)
-  apply (drule_tac x = x in spec) back
-ML{*ResAtp.problem_name := "BigO__bigo_lesso2_simpler"*}
-(*sledgehammer*);  
-  apply (simp add: compare_rls del: diff_minus)
-  apply (subst diff_minus)+
-  apply (rule add_right_mono)
-  apply (erule spec)
-  apply (rule order_trans) 
-  prefer 2
-  apply (rule abs_ge_zero)
-(*
-  apply (simp only: compare_rls min_max.below_sup.above_sup_conv 
-             linorder_not_le order_less_imp_le)
-*)
-  apply (simp add: compare_rls del: diff_minus)
-done
-
-
+  prefer 2 (*re-order subgoals because I don't know what to put after a structured proof*)
+   apply (metis abs_ge_zero abs_minus_commute linorder_linear min_max.less_eq_less_sup.sup_absorb1 min_max.less_eq_less_sup.sup_commute)
+proof (neg_clausify)
+fix x
+assume 0: "\<And>A. k A \<le> f A"
+have 1: "\<And>(X1\<Colon>'b\<Colon>ordered_idom) X2. \<not> max X1 X2 < X1"
+  by (metis linorder_not_less le_maxI1)  (*sort inserted by hand*)
+assume 2: "(0\<Colon>'b) \<le> k x - g x"
+have 3: "\<not> k x - g x < (0\<Colon>'b)"
+  by (metis 2 linorder_not_less)
+have 4: "\<And>X1 X2. min X1 (k X2) \<le> f X2"
+  by (metis min_max.less_eq_less_inf.inf_le2 min_max.less_eq_less_inf.le_inf_iff min_max.less_eq_less_inf.le_iff_inf 0)
+have 5: "\<bar>g x - f x\<bar> = f x - g x"
+  by (metis abs_minus_commute combine_common_factor mult_zero_right minus_add_cancel minus_zero abs_if diff_less_eq min_max.less_eq_less_inf.inf_commute 4 linorder_not_le min_max.less_eq_less_inf.le_iff_inf 3 diff_less_0_iff_less linorder_not_less)
+have 6: "max (0\<Colon>'b) (k x - g x) = k x - g x"
+  by (metis min_max.less_eq_less_sup.le_iff_sup 2)
+assume 7: "\<not> max (k x - g x) (0\<Colon>'b) \<le> \<bar>f x - g x\<bar>"
+have 8: "\<not> k x - g x \<le> f x - g x"
+  by (metis 5 abs_minus_commute 7 min_max.less_eq_less_sup.sup_commute 6)
+show "False"
+  by (metis min_max.less_eq_less_sup.sup_commute min_max.less_eq_less_inf.inf_commute min_max.less_eq_less_inf_sup.sup_inf_absorb min_max.less_eq_less_inf.le_iff_inf 0 max_diff_distrib_left 1 linorder_not_le 8)
+qed
 
 ML{*ResAtp.problem_name := "BigO__bigo_lesso3"*}
 lemma bigo_lesso3: "f =o g +o O(h) ==>
@@ -1472,16 +1511,9 @@
   apply (subst abs_of_nonneg)
   apply (drule_tac x = x in spec) back
 ML{*ResAtp.problem_name := "BigO__bigo_lesso3_simpler"*}
-(*sledgehammer*);  
-  apply (simp del: diff_minus)
-  apply (subst diff_minus)+
-  apply (rule add_left_mono)
-  apply (rule le_imp_neg_le)
-  apply (erule spec)
-  apply (rule order_trans) 
-  prefer 2
-  apply (rule abs_ge_zero)
-  apply (simp del: diff_minus)
+apply (metis diff_less_0_iff_less linorder_not_le not_leE uminus_add_conv_diff xt1(12) xt1(6))
+apply (metis add_minus_cancel diff_le_eq le_diff_eq uminus_add_conv_diff)
+apply (metis abs_ge_zero linorder_linear min_max.less_eq_less_sup.sup_absorb1 min_max.less_eq_less_sup.sup_commute)
 done
 
 lemma bigo_lesso4: "f <o g =o O(k::'a=>'b::ordered_field) ==>
@@ -1503,8 +1535,7 @@
     EX C. ALL x. f x <= g x + C * abs(h x)"
   apply (simp only: lesso_def bigo_alt_def)
   apply clarsimp
-(*sledgehammer*);  
-apply (auto simp add: compare_rls add_ac) 
+  apply (metis abs_if abs_mult add_commute diff_le_eq less_not_permute mult_commute)  
 done
 
 end
diff -r da7de38392df -r f406a5744756 src/HOL/MetisExamples/Tarski.thy
--- a/src/HOL/MetisExamples/Tarski.thy	Thu Sep 06 16:28:42 2007 +0200
+++ b/src/HOL/MetisExamples/Tarski.thy	Thu Sep 06 16:54:03 2007 +0200
@@ -1018,12 +1018,7 @@
 ML{*ResAtp.problem_name:="Tarski__fz_in_int_rel"*}  (*ALL THEOREMS*)
 lemma (in Tarski) f'z_in_int_rel: "[| z \<in> P; \<forall>y\<in>Y. (y, z) \<in> induced P r |]
       ==> ((%x: intY1. f x) z, z) \<in> induced intY1 r" 
-(*
-  apply (metis P_def UnE Un_absorb contra_subsetD equalityE fix_imp_eq indI intY1_elem intY1_f_closed monotoneE monotone_f reflE rel_imp_elem restrict_apply z_in_interval)
-??unsound??*)
-apply (simp add: induced_def  intY1_f_closed z_in_interval P_def)
-apply (simp add: fix_imp_eq [of _ f A] fix_subset [of f A, THEN subsetD]
-                 reflE)
+apply (metis P_def acc_def fix_imp_eq fix_subset indI reflE restrict_apply subset_def z_in_interval)
 done
 
 (*never proved, 2007-01-22*)