# HG changeset patch # User wenzelm # Date 1635457073 -7200 # Node ID 9af55a51e18536390a32957dbc449f5a01cce34a # Parent c496550dd2c26eed2edde2bd8a91a893b018c1f5 clarified antiquotations; diff -r c496550dd2c2 -r 9af55a51e185 src/HOL/Library/Sum_of_Squares/positivstellensatz.ML --- a/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML Thu Oct 28 21:28:52 2021 +0200 +++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML Thu Oct 28 23:37:53 2021 +0200 @@ -174,14 +174,9 @@ val pth = @{lemma "(((x::real) < y) \ (y - x > 0))" and "((x \ y) \ (y - x \ 0))" and "((x = y) \ (x - y = 0))" and "((\(x < y)) \ (x - y \ 0))" and - "((\(x \ y)) \ (x - y > 0))" and "((\(x = y)) \ (x - y > 0 \ -(x - y) > 0))" + "((\(x \ y)) \ (x - y > 0))" by (atomize (full), auto simp add: less_diff_eq le_diff_eq not_less)}; -fun neq_th x y = - \<^instantiate>\x and y in lemma \x \ y \ x - y > 0 \ - (x - y) > 0\ for x y :: real - by (atomize (full), auto simp add: less_diff_eq le_diff_eq not_less)\; - -val pth_final = @{lemma "(\p \ False) \ p" by blast} val pth_add = @{lemma "(x = (0::real) \ y = 0 \ x + y = 0 )" and "( x = 0 \ y \ 0 \ x + y \ 0)" and "(x = 0 \ y > 0 \ x + y > 0)" and "(x \ 0 \ y = 0 \ x + y \ 0)" and @@ -199,7 +194,6 @@ mult_strict_mono[where b="x" and d="y" and a="0" and c="0", simplified])}; val pth_emul = @{lemma "y = (0::real) \ x * y = 0" by simp}; -val pth_square = @{lemma "x * x \ (0::real)" by simp}; val weak_dnf_simps = List.take (@{thms simp_thms}, 34) @ @@ -384,7 +378,7 @@ in Thm.transitive th' (oprconv poly_conv (Thm.rhs_of th')) end val [real_lt_conv, real_le_conv, real_eq_conv, - real_not_lt_conv, real_not_le_conv, _] = + real_not_lt_conv, real_not_le_conv] = map real_ineq_conv pth fun match_mp_rule ths ths' = let @@ -398,7 +392,7 @@ fun emul_rule ct th = fconv_rule (arg_conv (oprconv poly_mul_conv)) (Thm.instantiate' [] [SOME ct] (th RS pth_emul)) fun square_rule t = fconv_rule (arg_conv (oprconv poly_conv)) - (Thm.instantiate' [] [SOME t] pth_square) + \<^instantiate>\x = t in lemma \x * x \ 0\ for x :: real by simp\ fun hol_of_positivstellensatz(eqs,les,lts) proof = let @@ -482,7 +476,9 @@ fun real_not_eq_conv ct = let val (l,r) = dest_eq (Thm.dest_arg ct) - val th = neq_th l r + val th = + \<^instantiate>\x = l and y = r in lemma \x \ y \ x - y > 0 \ - (x - y) > 0\ for x y :: real + by (atomize (full), auto simp add: less_diff_eq le_diff_eq not_less)\; val th_p = poly_conv(Thm.dest_arg(Thm.dest_arg1(Thm.rhs_of th))) val th_x = Drule.arg_cong_rule \<^cterm>\uminus :: real \ _\ th_p val th_n = fconv_rule (arg_conv poly_neg_conv) th_x @@ -578,7 +574,9 @@ (prove_hyp (Thm.equal_elim th1 (Thm.assume (Thm.apply \<^cterm>\Trueprop\ bod))) th2) in (Drule.implies_intr_hyps (prove_hyp (Thm.equal_elim th0 (Thm.assume nct)) th3), certs) end - in (Thm.implies_elim (Thm.instantiate' [] [SOME ct] pth_final) th, certificates) + in + (Thm.implies_elim \<^instantiate>\A = ct in lemma \(\ A \ False) \ A\ by blast\ th, + certificates) end in f end; diff -r c496550dd2c2 -r 9af55a51e185 src/HOL/Library/Sum_of_Squares/sum_of_squares.ML --- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Thu Oct 28 21:28:52 2021 +0200 +++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Thu Oct 28 23:37:53 2021 +0200 @@ -1018,12 +1018,14 @@ NONE => no_tac | SOME (d, ord) => let - val simp_ctxt = ctxt - |> Simplifier.put_simpset sos_ss + val simp_ctxt = ctxt |> Simplifier.put_simpset sos_ss; val th = - Thm.instantiate' [] [SOME d, SOME (Thm.dest_arg P)] - (if ord then @{lemma "(d=0 \ P) \ (d>0 \ P) \ (d<(0::real) \ P) \ P" by auto} - else @{lemma "(d=0 \ P) \ (d \ (0::real) \ P) \ P" by blast}) + if ord then + \<^instantiate>\d and P = \Thm.dest_arg P\ in + lemma \(d = 0 \ P) \ (d > 0 \ P) \ (d < 0 \ P) \ P\ for d :: real by auto\ + else + \<^instantiate>\d and P = \Thm.dest_arg P\ in + lemma \(d = 0 \ P) \ (d \ 0 \ P) \ P\ for d :: real by blast\ in resolve_tac ctxt [th] i THEN Simplifier.asm_full_simp_tac simp_ctxt i end)); fun elim_denom_tac ctxt i = REPEAT (elim_one_denom_tac ctxt i);