src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
 changeset 35028 108662d50512 parent 34974 18b41bba42b5 child 35033 e47934673b74
```     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Feb 05 14:33:31 2010 +0100
1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Feb 05 14:33:50 2010 +0100
1.3 @@ -447,7 +447,7 @@
1.4  by (induct p rule: fmsize.induct) simp_all
1.5
1.6    (* Semantics of formulae (fm) *)
1.7 -consts Ifm ::"'a::{division_by_zero,ordered_field} list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool"
1.8 +consts Ifm ::"'a::{division_by_zero,linordered_field} list \<Rightarrow> 'a list \<Rightarrow> fm \<Rightarrow> bool"
1.9  primrec
1.10    "Ifm vs bs T = True"
1.11    "Ifm vs bs F = False"
1.12 @@ -1833,16 +1833,16 @@
1.13    ultimately show ?case by blast
1.14  qed (auto simp add: nth_pos2 tmbound0_I[where vs=vs and bs="bs" and b="y" and b'="x"] bound0_I[where vs=vs and bs="bs" and b="y" and b'="x"])
1.15
1.16 -lemma one_plus_one_pos[simp]: "(1::'a::{ordered_field}) + 1 > 0"
1.17 +lemma one_plus_one_pos[simp]: "(1::'a::{linordered_field}) + 1 > 0"
1.18  proof-
1.19    have op: "(1::'a) > 0" by simp
1.20    from add_pos_pos[OF op op] show ?thesis .
1.21  qed
1.22
1.23 -lemma one_plus_one_nonzero[simp]: "(1::'a::{ordered_field}) + 1 \<noteq> 0"
1.24 +lemma one_plus_one_nonzero[simp]: "(1::'a::{linordered_field}) + 1 \<noteq> 0"
1.25    using one_plus_one_pos[where ?'a = 'a] by (simp add: less_le)
1.26
1.27 -lemma half_sum_eq: "(u + u) / (1+1) = (u::'a::{ordered_field})"
1.28 +lemma half_sum_eq: "(u + u) / (1+1) = (u::'a::{linordered_field})"
1.29  proof-
1.30    have "(u + u) = (1 + 1) * u" by (simp add: ring_simps)
1.31    hence "(u + u) / (1+1) = (1 + 1)*u / (1 + 1)" by simp
1.32 @@ -3172,54 +3172,54 @@
1.33  *} "Parametric QE for linear Arithmetic over fields, Version 2"
1.34
1.35
1.36 -lemma "\<exists>(x::'a::{division_by_zero,ordered_field,number_ring}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
1.37 -  apply (frpar type: "'a::{division_by_zero,ordered_field,number_ring}" pars: "y::'a::{division_by_zero,ordered_field,number_ring}")
1.38 +lemma "\<exists>(x::'a::{division_by_zero,linordered_field,number_ring}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
1.39 +  apply (frpar type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "y::'a::{division_by_zero,linordered_field,number_ring}")
1.41    apply (rule spec[where x=y])
1.42 -  apply (frpar type: "'a::{division_by_zero,ordered_field,number_ring}" pars: "z::'a::{division_by_zero,ordered_field,number_ring}")
1.43 +  apply (frpar type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "z::'a::{division_by_zero,linordered_field,number_ring}")
1.44    by simp
1.45
1.46  text{* Collins/Jones Problem *}
1.47  (*
1.48 -lemma "\<exists>(r::'a::{division_by_zero,ordered_field,number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0"
1.49 +lemma "\<exists>(r::'a::{division_by_zero,linordered_field,number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0"
1.50  proof-
1.51 -  have "(\<exists>(r::'a::{division_by_zero,ordered_field,number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \<longleftrightarrow> (\<exists>(r::'a::{division_by_zero,ordered_field,number_ring}). 0 < r \<and> r < 1 \<and> 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \<and> 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \<longleftrightarrow> ?rhs")
1.52 +  have "(\<exists>(r::'a::{division_by_zero,linordered_field,number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \<longleftrightarrow> (\<exists>(r::'a::{division_by_zero,linordered_field,number_ring}). 0 < r \<and> r < 1 \<and> 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \<and> 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \<longleftrightarrow> ?rhs")
1.54  have "?rhs"
1.55
1.56 -  apply (frpar type: "'a::{division_by_zero,ordered_field,number_ring}" pars: "a::'a::{division_by_zero,ordered_field,number_ring}" "b::'a::{division_by_zero,ordered_field,number_ring}")
1.57 +  apply (frpar type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "a::'a::{division_by_zero,linordered_field,number_ring}" "b::'a::{division_by_zero,linordered_field,number_ring}")
1.59  oops
1.60  *)
1.61  (*
1.62 -lemma "ALL (x::'a::{division_by_zero,ordered_field,number_ring}) y. (1 - t)*x \<le> (1+t)*y \<and> (1 - t)*y \<le> (1+t)*x --> 0 \<le> y"
1.63 -apply (frpar type: "'a::{division_by_zero,ordered_field,number_ring}" pars: "t::'a::{division_by_zero,ordered_field,number_ring}")
1.64 +lemma "ALL (x::'a::{division_by_zero,linordered_field,number_ring}) y. (1 - t)*x \<le> (1+t)*y \<and> (1 - t)*y \<le> (1+t)*x --> 0 \<le> y"
1.65 +apply (frpar type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "t::'a::{division_by_zero,linordered_field,number_ring}")
1.66  oops
1.67  *)
1.68
1.69 -lemma "\<exists>(x::'a::{division_by_zero,ordered_field,number_ring}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
1.70 -  apply (frpar2 type: "'a::{division_by_zero,ordered_field,number_ring}" pars: "y::'a::{division_by_zero,ordered_field,number_ring}")
1.71 +lemma "\<exists>(x::'a::{division_by_zero,linordered_field,number_ring}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
1.72 +  apply (frpar2 type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "y::'a::{division_by_zero,linordered_field,number_ring}")
1.74    apply (rule spec[where x=y])
1.75 -  apply (frpar2 type: "'a::{division_by_zero,ordered_field,number_ring}" pars: "z::'a::{division_by_zero,ordered_field,number_ring}")
1.76 +  apply (frpar2 type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "z::'a::{division_by_zero,linordered_field,number_ring}")
1.77    by simp
1.78
1.79  text{* Collins/Jones Problem *}
1.80
1.81  (*
1.82 -lemma "\<exists>(r::'a::{division_by_zero,ordered_field,number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0"
1.83 +lemma "\<exists>(r::'a::{division_by_zero,linordered_field,number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0"
1.84  proof-
1.85 -  have "(\<exists>(r::'a::{division_by_zero,ordered_field,number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \<longleftrightarrow> (\<exists>(r::'a::{division_by_zero,ordered_field,number_ring}). 0 < r \<and> r < 1 \<and> 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \<and> 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \<longleftrightarrow> ?rhs")
1.86 +  have "(\<exists>(r::'a::{division_by_zero,linordered_field,number_ring}). 0 < r \<and> r < 1 \<and> 0 < (2 - 3*r) *(a^2 + b^2) + (2*a)*r \<and> (2 - 3*r) *(a^2 + b^2) + 4*a*r - 2*a - r < 0) \<longleftrightarrow> (\<exists>(r::'a::{division_by_zero,linordered_field,number_ring}). 0 < r \<and> r < 1 \<and> 0 < 2 *(a^2 + b^2) - (3*(a^2 + b^2)) * r + (2*a)*r \<and> 2*(a^2 + b^2) - (3*(a^2 + b^2) - 4*a + 1)*r - 2*a < 0)" (is "?lhs \<longleftrightarrow> ?rhs")
1.88  have "?rhs"
1.89 -  apply (frpar2 type: "'a::{division_by_zero,ordered_field,number_ring}" pars: "a::'a::{division_by_zero,ordered_field,number_ring}" "b::'a::{division_by_zero,ordered_field,number_ring}")
1.90 +  apply (frpar2 type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "a::'a::{division_by_zero,linordered_field,number_ring}" "b::'a::{division_by_zero,linordered_field,number_ring}")
1.91    apply simp
1.92  oops
1.93  *)
1.94
1.95  (*
1.96 -lemma "ALL (x::'a::{division_by_zero,ordered_field,number_ring}) y. (1 - t)*x \<le> (1+t)*y \<and> (1 - t)*y \<le> (1+t)*x --> 0 \<le> y"
1.97 -apply (frpar2 type: "'a::{division_by_zero,ordered_field,number_ring}" pars: "t::'a::{division_by_zero,ordered_field,number_ring}")
1.98 +lemma "ALL (x::'a::{division_by_zero,linordered_field,number_ring}) y. (1 - t)*x \<le> (1+t)*y \<and> (1 - t)*y \<le> (1+t)*x --> 0 \<le> y"
1.99 +apply (frpar2 type: "'a::{division_by_zero,linordered_field,number_ring}" pars: "t::'a::{division_by_zero,linordered_field,number_ring}")
1.100  apply (simp add: field_simps linorder_neq_iff[symmetric])
1.101  apply ferrack
1.102  oops
```