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.40    apply (simp add: ring_simps)
    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.53  by (simp add: ring_simps)
    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.58    apply (simp add: ring_simps)
    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.73    apply (simp add: ring_simps)
    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.87  by (simp add: ring_simps)
    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