established Plain theory and image
authorhaftmann
Thu Jun 26 10:07:01 2008 +0200 (2008-06-26)
changeset 273689f90ac19e32b
parent 27367 a75d71c73362
child 27369 7f242009f7b4
established Plain theory and image
src/HOL/ATP_Linkup.thy
src/HOL/Complex/Complex_Main.thy
src/HOL/Complex/ex/MIR.thy
src/HOL/Complex/ex/ReflectedFerrack.thy
src/HOL/Dense_Linear_Order.thy
src/HOL/Hyperreal/Poly.thy
src/HOL/IsaMakefile
src/HOL/Library/Abstract_Rat.thy
src/HOL/Library/AssocList.thy
src/HOL/Library/BigO.thy
src/HOL/Library/Binomial.thy
src/HOL/Library/Boolean_Algebra.thy
src/HOL/Library/Char_nat.thy
src/HOL/Library/Char_ord.thy
src/HOL/Library/Code_Char.thy
src/HOL/Library/Code_Char_chr.thy
src/HOL/Library/Code_Index.thy
src/HOL/Library/Code_Integer.thy
src/HOL/Library/Code_Message.thy
src/HOL/Library/Coinductive_List.thy
src/HOL/Library/Commutative_Ring.thy
src/HOL/Library/Continuity.thy
src/HOL/Library/Countable.thy
src/HOL/Library/Dense_Linear_Order.thy
src/HOL/Library/Efficient_Nat.thy
src/HOL/Library/Enum.thy
src/HOL/Library/Eval.thy
src/HOL/Library/Eval_Witness.thy
src/HOL/Library/Executable_Set.thy
src/HOL/Library/FuncSet.thy
src/HOL/Library/GCD.thy
src/HOL/Library/Heap.thy
src/HOL/Library/Infinite_Set.thy
src/HOL/Library/LaTeXsugar.thy
src/HOL/Library/Library.thy
src/HOL/Library/ListVector.thy
src/HOL/Library/List_Prefix.thy
src/HOL/Library/List_lexord.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/NatPair.thy
src/HOL/Library/Nat_Infinity.thy
src/HOL/Library/Nested_Environment.thy
src/HOL/Library/Numeral_Type.thy
src/HOL/Library/Option_ord.thy
src/HOL/Library/Order_Relation.thy
src/HOL/Library/Parity.thy
src/HOL/Library/Permutation.thy
src/HOL/Library/Pocklington.thy
src/HOL/Library/Primes.thy
src/HOL/Library/Product_ord.thy
src/HOL/Library/Quicksort.thy
src/HOL/Library/Quotient.thy
src/HOL/Library/RBT.thy
src/HOL/Library/RType.thy
src/HOL/Library/Ramsey.thy
src/HOL/Library/SetsAndFunctions.thy
src/HOL/Library/State_Monad.thy
src/HOL/Library/Sublist_Order.thy
src/HOL/Library/Univ_Poly.thy
src/HOL/Library/While_Combinator.thy
src/HOL/Library/Word.thy
src/HOL/List.thy
src/HOL/MetisExamples/Abstraction.thy
src/HOL/MetisExamples/Tarski.thy
src/HOL/NumberTheory/Factorization.thy
src/HOL/NumberTheory/IntPrimes.thy
src/HOL/Plain.thy
src/HOL/ROOT.ML
src/HOL/Real/ContNotDenum.thy
src/HOL/Real/Lubs.thy
src/HOL/plain.ML
     1.1 --- a/src/HOL/ATP_Linkup.thy	Thu Jun 26 10:06:54 2008 +0200
     1.2 +++ b/src/HOL/ATP_Linkup.thy	Thu Jun 26 10:07:01 2008 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  header{* The Isabelle-ATP Linkup *}
     1.5  
     1.6  theory ATP_Linkup
     1.7 -imports Record Presburger SAT Recdef Extraction Relation_Power Hilbert_Choice
     1.8 +imports Record Hilbert_Choice
     1.9  uses
    1.10    "Tools/polyhash.ML"
    1.11    "Tools/res_clause.ML"
    1.12 @@ -88,6 +88,9 @@
    1.13  apply (simp add: COMBC_def) 
    1.14  done
    1.15  
    1.16 +
    1.17 +subsection {* Setup of Vampire, E prover and SPASS *}
    1.18 +
    1.19  use "Tools/res_axioms.ML"      --{*requires the combinators declared above*}
    1.20  setup ResAxioms.setup
    1.21  
    1.22 @@ -96,9 +99,6 @@
    1.23  use "Tools/watcher.ML"
    1.24  use "Tools/res_atp.ML"
    1.25  
    1.26 -
    1.27 -subsection {* Setup for Vampire, E prover and SPASS *}
    1.28 -
    1.29  use "Tools/res_atp_provers.ML"
    1.30  
    1.31  oracle vampire_oracle ("string * int") = {* ResAtpProvers.vampire_o *}
     2.1 --- a/src/HOL/Complex/Complex_Main.thy	Thu Jun 26 10:06:54 2008 +0200
     2.2 +++ b/src/HOL/Complex/Complex_Main.thy	Thu Jun 26 10:07:01 2008 +0200
     2.3 @@ -7,7 +7,7 @@
     2.4  header{*Comprehensive Complex Theory*}
     2.5  
     2.6  theory Complex_Main
     2.7 -imports Fundamental_Theorem_Algebra CLim "../Hyperreal/Hyperreal"
     2.8 +imports Main Fundamental_Theorem_Algebra CLim "../Hyperreal/Hyperreal"
     2.9  begin
    2.10  
    2.11  end
     3.1 --- a/src/HOL/Complex/ex/MIR.thy	Thu Jun 26 10:06:54 2008 +0200
     3.2 +++ b/src/HOL/Complex/ex/MIR.thy	Thu Jun 26 10:07:01 2008 +0200
     3.3 @@ -5,9 +5,9 @@
     3.4  header {* Quatifier elimination for R(0,1,+,floor,<) *}
     3.5  
     3.6  theory MIR
     3.7 -  imports Real GCD Code_Integer
     3.8 -  uses ("mireif.ML") ("mirtac.ML")
     3.9 -  begin
    3.10 +imports List Real Code_Integer
    3.11 +uses ("mireif.ML") ("mirtac.ML")
    3.12 +begin
    3.13  
    3.14  declare real_of_int_floor_cancel [simp del]
    3.15  
     4.1 --- a/src/HOL/Complex/ex/ReflectedFerrack.thy	Thu Jun 26 10:06:54 2008 +0200
     4.2 +++ b/src/HOL/Complex/ex/ReflectedFerrack.thy	Thu Jun 26 10:07:01 2008 +0200
     4.3 @@ -5,8 +5,8 @@
     4.4  header {* Quatifier elimination for R(0,1,+,<) *}
     4.5  
     4.6  theory ReflectedFerrack
     4.7 -  imports GCD Real Efficient_Nat
     4.8 -  uses ("linreif.ML") ("linrtac.ML")
     4.9 +imports Main GCD Real Efficient_Nat
    4.10 +uses ("linreif.ML") ("linrtac.ML")
    4.11  begin
    4.12  
    4.13  
     5.1 --- a/src/HOL/Dense_Linear_Order.thy	Thu Jun 26 10:06:54 2008 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,553 +0,0 @@
     5.4 -(*
     5.5 -    ID:         $Id$
     5.6 -    Author:     Amine Chaieb, TU Muenchen
     5.7 -*)
     5.8 -
     5.9 -header {* Dense linear order without endpoints
    5.10 -  and a quantifier elimination procedure in Ferrante and Rackoff style *}
    5.11 -
    5.12 -theory Dense_Linear_Order
    5.13 -imports Finite_Set
    5.14 -uses
    5.15 -  "Tools/Qelim/qelim.ML"
    5.16 -  "Tools/Qelim/langford_data.ML"
    5.17 -  "Tools/Qelim/ferrante_rackoff_data.ML"
    5.18 -  ("Tools/Qelim/langford.ML")
    5.19 -  ("Tools/Qelim/ferrante_rackoff.ML")
    5.20 -begin
    5.21 -
    5.22 -setup Langford_Data.setup
    5.23 -setup Ferrante_Rackoff_Data.setup
    5.24 -
    5.25 -context linorder
    5.26 -begin
    5.27 -
    5.28 -lemma less_not_permute: "\<not> (x < y \<and> y < x)" by (simp add: not_less linear)
    5.29 -
    5.30 -lemma gather_simps: 
    5.31 -  shows 
    5.32 -  "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y) \<and> x < u \<and> P x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> (insert u U). x < y) \<and> P x)"
    5.33 -  and "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y) \<and> l < x \<and> P x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> (insert l L). y < x) \<and> (\<forall>y \<in> U. x < y) \<and> P x)"
    5.34 -  "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y) \<and> x < u) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> (insert u U). x < y))"
    5.35 -  and "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y) \<and> l < x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> (insert l L). y < x) \<and> (\<forall>y \<in> U. x < y))"  by auto
    5.36 -
    5.37 -lemma 
    5.38 -  gather_start: "(\<exists>x. P x) \<equiv> (\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y\<in> {}. x < y) \<and> P x)" 
    5.39 -  by simp
    5.40 -
    5.41 -text{* Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"}*}
    5.42 -lemma minf_lt:  "\<exists>z . \<forall>x. x < z \<longrightarrow> (x < t \<longleftrightarrow> True)" by auto
    5.43 -lemma minf_gt: "\<exists>z . \<forall>x. x < z \<longrightarrow>  (t < x \<longleftrightarrow>  False)"
    5.44 -  by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le)
    5.45 -
    5.46 -lemma minf_le: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<le> t \<longleftrightarrow> True)" by (auto simp add: less_le)
    5.47 -lemma minf_ge: "\<exists>z. \<forall>x. x < z \<longrightarrow> (t \<le> x \<longleftrightarrow> False)"
    5.48 -  by (auto simp add: less_le not_less not_le)
    5.49 -lemma minf_eq: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
    5.50 -lemma minf_neq: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
    5.51 -lemma minf_P: "\<exists>z. \<forall>x. x < z \<longrightarrow> (P \<longleftrightarrow> P)" by blast
    5.52 -
    5.53 -text{* Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"}*}
    5.54 -lemma pinf_gt:  "\<exists>z . \<forall>x. z < x \<longrightarrow> (t < x \<longleftrightarrow> True)" by auto
    5.55 -lemma pinf_lt: "\<exists>z . \<forall>x. z < x \<longrightarrow>  (x < t \<longleftrightarrow>  False)"
    5.56 -  by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le)
    5.57 -
    5.58 -lemma pinf_ge: "\<exists>z. \<forall>x. z < x \<longrightarrow> (t \<le> x \<longleftrightarrow> True)" by (auto simp add: less_le)
    5.59 -lemma pinf_le: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x \<le> t \<longleftrightarrow> False)"
    5.60 -  by (auto simp add: less_le not_less not_le)
    5.61 -lemma pinf_eq: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
    5.62 -lemma pinf_neq: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
    5.63 -lemma pinf_P: "\<exists>z. \<forall>x. z < x \<longrightarrow> (P \<longleftrightarrow> P)" by blast
    5.64 -
    5.65 -lemma nmi_lt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x < t \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
    5.66 -lemma nmi_gt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t < x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)"
    5.67 -  by (auto simp add: le_less)
    5.68 -lemma  nmi_le: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x\<le> t \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
    5.69 -lemma  nmi_ge: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t\<le> x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
    5.70 -lemma  nmi_eq: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  x = t \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
    5.71 -lemma  nmi_neq: "t \<in> U \<Longrightarrow>\<forall>x. \<not>True \<and> x \<noteq> t \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
    5.72 -lemma  nmi_P: "\<forall> x. ~P \<and> P \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
    5.73 -lemma  nmi_conj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x) ;
    5.74 -  \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)\<rbrakk> \<Longrightarrow>
    5.75 -  \<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
    5.76 -lemma  nmi_disj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x) ;
    5.77 -  \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)\<rbrakk> \<Longrightarrow>
    5.78 -  \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
    5.79 -
    5.80 -lemma  npi_lt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  x < t \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by (auto simp add: le_less)
    5.81 -lemma  npi_gt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> t < x \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
    5.82 -lemma  npi_le: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  x \<le> t \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
    5.83 -lemma  npi_ge: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> t \<le> x \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
    5.84 -lemma  npi_eq: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  x = t \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
    5.85 -lemma  npi_neq: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x \<noteq> t \<longrightarrow>  (\<exists> u\<in> U. x \<le> u )" by auto
    5.86 -lemma  npi_P: "\<forall> x. ~P \<and> P \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
    5.87 -lemma  npi_conj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. x \<le> u) ;  \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)\<rbrakk>
    5.88 -  \<Longrightarrow>  \<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
    5.89 -lemma  npi_disj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. x \<le> u) ; \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)\<rbrakk>
    5.90 -  \<Longrightarrow> \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
    5.91 -
    5.92 -lemma lin_dense_lt: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t < u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> x < t \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y < t)"
    5.93 -proof(clarsimp)
    5.94 -  fix x l u y  assume tU: "t \<in> U" and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x"
    5.95 -    and xu: "x<u"  and px: "x < t" and ly: "l<y" and yu:"y < u"
    5.96 -  from tU noU ly yu have tny: "t\<noteq>y" by auto
    5.97 -  {assume H: "t < y"
    5.98 -    from less_trans[OF lx px] less_trans[OF H yu]
    5.99 -    have "l < t \<and> t < u"  by simp
   5.100 -    with tU noU have "False" by auto}
   5.101 -  hence "\<not> t < y"  by auto hence "y \<le> t" by (simp add: not_less)
   5.102 -  thus "y < t" using tny by (simp add: less_le)
   5.103 -qed
   5.104 -
   5.105 -lemma lin_dense_gt: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l < x \<and> x < u \<and> t < x \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> t < y)"
   5.106 -proof(clarsimp)
   5.107 -  fix x l u y
   5.108 -  assume tU: "t \<in> U" and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x" and xu: "x<u"
   5.109 -  and px: "t < x" and ly: "l<y" and yu:"y < u"
   5.110 -  from tU noU ly yu have tny: "t\<noteq>y" by auto
   5.111 -  {assume H: "y< t"
   5.112 -    from less_trans[OF ly H] less_trans[OF px xu] have "l < t \<and> t < u" by simp
   5.113 -    with tU noU have "False" by auto}
   5.114 -  hence "\<not> y<t"  by auto hence "t \<le> y" by (auto simp add: not_less)
   5.115 -  thus "t < y" using tny by (simp add:less_le)
   5.116 -qed
   5.117 -
   5.118 -lemma lin_dense_le: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> x \<le> t \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y\<le> t)"
   5.119 -proof(clarsimp)
   5.120 -  fix x l u y
   5.121 -  assume tU: "t \<in> U" and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x" and xu: "x<u"
   5.122 -  and px: "x \<le> t" and ly: "l<y" and yu:"y < u"
   5.123 -  from tU noU ly yu have tny: "t\<noteq>y" by auto
   5.124 -  {assume H: "t < y"
   5.125 -    from less_le_trans[OF lx px] less_trans[OF H yu]
   5.126 -    have "l < t \<and> t < u" by simp
   5.127 -    with tU noU have "False" by auto}
   5.128 -  hence "\<not> t < y"  by auto thus "y \<le> t" by (simp add: not_less)
   5.129 -qed
   5.130 -
   5.131 -lemma lin_dense_ge: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> t \<le> x \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> t \<le> y)"
   5.132 -proof(clarsimp)
   5.133 -  fix x l u y
   5.134 -  assume tU: "t \<in> U" and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x" and xu: "x<u"
   5.135 -  and px: "t \<le> x" and ly: "l<y" and yu:"y < u"
   5.136 -  from tU noU ly yu have tny: "t\<noteq>y" by auto
   5.137 -  {assume H: "y< t"
   5.138 -    from less_trans[OF ly H] le_less_trans[OF px xu]
   5.139 -    have "l < t \<and> t < u" by simp
   5.140 -    with tU noU have "False" by auto}
   5.141 -  hence "\<not> y<t"  by auto thus "t \<le> y" by (simp add: not_less)
   5.142 -qed
   5.143 -lemma lin_dense_eq: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> x = t   \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y= t)"  by auto
   5.144 -lemma lin_dense_neq: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> x \<noteq> t   \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y\<noteq> t)"  by auto
   5.145 -lemma lin_dense_P: "\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P   \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P)"  by auto
   5.146 -
   5.147 -lemma lin_dense_conj:
   5.148 -  "\<lbrakk>\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P1 x
   5.149 -  \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P1 y) ;
   5.150 -  \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P2 x
   5.151 -  \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow>
   5.152 -  \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> (P1 x \<and> P2 x)
   5.153 -  \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> (P1 y \<and> P2 y))"
   5.154 -  by blast
   5.155 -lemma lin_dense_disj:
   5.156 -  "\<lbrakk>\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P1 x
   5.157 -  \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P1 y) ;
   5.158 -  \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P2 x
   5.159 -  \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow>
   5.160 -  \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> (P1 x \<or> P2 x)
   5.161 -  \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> (P1 y \<or> P2 y))"
   5.162 -  by blast
   5.163 -
   5.164 -lemma npmibnd: "\<lbrakk>\<forall>x. \<not> MP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<le> x); \<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. x \<le> u)\<rbrakk>
   5.165 -  \<Longrightarrow> \<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<le> x \<and> x \<le> u')"
   5.166 -by auto
   5.167 -
   5.168 -lemma finite_set_intervals:
   5.169 -  assumes px: "P x" and lx: "l \<le> x" and xu: "x \<le> u" and linS: "l\<in> S"
   5.170 -  and uinS: "u \<in> S" and fS:"finite S" and lS: "\<forall> x\<in> S. l \<le> x" and Su: "\<forall> x\<in> S. x \<le> u"
   5.171 -  shows "\<exists> a \<in> S. \<exists> b \<in> S. (\<forall> y. a < y \<and> y < b \<longrightarrow> y \<notin> S) \<and> a \<le> x \<and> x \<le> b \<and> P x"
   5.172 -proof-
   5.173 -  let ?Mx = "{y. y\<in> S \<and> y \<le> x}"
   5.174 -  let ?xM = "{y. y\<in> S \<and> x \<le> y}"
   5.175 -  let ?a = "Max ?Mx"
   5.176 -  let ?b = "Min ?xM"
   5.177 -  have MxS: "?Mx \<subseteq> S" by blast
   5.178 -  hence fMx: "finite ?Mx" using fS finite_subset by auto
   5.179 -  from lx linS have linMx: "l \<in> ?Mx" by blast
   5.180 -  hence Mxne: "?Mx \<noteq> {}" by blast
   5.181 -  have xMS: "?xM \<subseteq> S" by blast
   5.182 -  hence fxM: "finite ?xM" using fS finite_subset by auto
   5.183 -  from xu uinS have linxM: "u \<in> ?xM" by blast
   5.184 -  hence xMne: "?xM \<noteq> {}" by blast
   5.185 -  have ax:"?a \<le> x" using Mxne fMx by auto
   5.186 -  have xb:"x \<le> ?b" using xMne fxM by auto
   5.187 -  have "?a \<in> ?Mx" using Max_in[OF fMx Mxne] by simp hence ainS: "?a \<in> S" using MxS by blast
   5.188 -  have "?b \<in> ?xM" using Min_in[OF fxM xMne] by simp hence binS: "?b \<in> S" using xMS by blast
   5.189 -  have noy:"\<forall> y. ?a < y \<and> y < ?b \<longrightarrow> y \<notin> S"
   5.190 -  proof(clarsimp)
   5.191 -    fix y   assume ay: "?a < y" and yb: "y < ?b" and yS: "y \<in> S"
   5.192 -    from yS have "y\<in> ?Mx \<or> y\<in> ?xM" by (auto simp add: linear)
   5.193 -    moreover {assume "y \<in> ?Mx" hence "y \<le> ?a" using Mxne fMx by auto with ay have "False" by (simp add: not_le[symmetric])}
   5.194 -    moreover {assume "y \<in> ?xM" hence "?b \<le> y" using xMne fxM by auto with yb have "False" by (simp add: not_le[symmetric])}
   5.195 -    ultimately show "False" by blast
   5.196 -  qed
   5.197 -  from ainS binS noy ax xb px show ?thesis by blast
   5.198 -qed
   5.199 -
   5.200 -lemma finite_set_intervals2:
   5.201 -  assumes px: "P x" and lx: "l \<le> x" and xu: "x \<le> u" and linS: "l\<in> S"
   5.202 -  and uinS: "u \<in> S" and fS:"finite S" and lS: "\<forall> x\<in> S. l \<le> x" and Su: "\<forall> x\<in> S. x \<le> u"
   5.203 -  shows "(\<exists> s\<in> S. P s) \<or> (\<exists> a \<in> S. \<exists> b \<in> S. (\<forall> y. a < y \<and> y < b \<longrightarrow> y \<notin> S) \<and> a < x \<and> x < b \<and> P x)"
   5.204 -proof-
   5.205 -  from finite_set_intervals[where P="P", OF px lx xu linS uinS fS lS Su]
   5.206 -  obtain a and b where
   5.207 -    as: "a\<in> S" and bs: "b\<in> S" and noS:"\<forall>y. a < y \<and> y < b \<longrightarrow> y \<notin> S"
   5.208 -    and axb: "a \<le> x \<and> x \<le> b \<and> P x"  by auto
   5.209 -  from axb have "x= a \<or> x= b \<or> (a < x \<and> x < b)" by (auto simp add: le_less)
   5.210 -  thus ?thesis using px as bs noS by blast
   5.211 -qed
   5.212 -
   5.213 -end
   5.214 -
   5.215 -section {* The classical QE after Langford for dense linear orders *}
   5.216 -
   5.217 -context dense_linear_order
   5.218 -begin
   5.219 -
   5.220 -lemma dlo_qe_bnds: 
   5.221 -  assumes ne: "L \<noteq> {}" and neU: "U \<noteq> {}" and fL: "finite L" and fU: "finite U"
   5.222 -  shows "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y)) \<equiv> (\<forall> l \<in> L. \<forall>u \<in> U. l < u)"
   5.223 -proof (simp only: atomize_eq, rule iffI)
   5.224 -  assume H: "\<exists>x. (\<forall>y\<in>L. y < x) \<and> (\<forall>y\<in>U. x < y)"
   5.225 -  then obtain x where xL: "\<forall>y\<in>L. y < x" and xU: "\<forall>y\<in>U. x < y" by blast
   5.226 -  {fix l u assume l: "l \<in> L" and u: "u \<in> U"
   5.227 -    have "l < x" using xL l by blast
   5.228 -    also have "x < u" using xU u by blast
   5.229 -    finally (less_trans) have "l < u" .}
   5.230 -  thus "\<forall>l\<in>L. \<forall>u\<in>U. l < u" by blast
   5.231 -next
   5.232 -  assume H: "\<forall>l\<in>L. \<forall>u\<in>U. l < u"
   5.233 -  let ?ML = "Max L"
   5.234 -  let ?MU = "Min U"  
   5.235 -  from fL ne have th1: "?ML \<in> L" and th1': "\<forall>l\<in>L. l \<le> ?ML" by auto
   5.236 -  from fU neU have th2: "?MU \<in> U" and th2': "\<forall>u\<in>U. ?MU \<le> u" by auto
   5.237 -  from th1 th2 H have "?ML < ?MU" by auto
   5.238 -  with dense obtain w where th3: "?ML < w" and th4: "w < ?MU" by blast
   5.239 -  from th3 th1' have "\<forall>l \<in> L. l < w" by auto
   5.240 -  moreover from th4 th2' have "\<forall>u \<in> U. w < u" by auto
   5.241 -  ultimately show "\<exists>x. (\<forall>y\<in>L. y < x) \<and> (\<forall>y\<in>U. x < y)" by auto
   5.242 -qed
   5.243 -
   5.244 -lemma dlo_qe_noub: 
   5.245 -  assumes ne: "L \<noteq> {}" and fL: "finite L"
   5.246 -  shows "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> {}. x < y)) \<equiv> True"
   5.247 -proof(simp add: atomize_eq)
   5.248 -  from gt_ex[of "Max L"] obtain M where M: "Max L < M" by blast
   5.249 -  from ne fL have "\<forall>x \<in> L. x \<le> Max L" by simp
   5.250 -  with M have "\<forall>x\<in>L. x < M" by (auto intro: le_less_trans)
   5.251 -  thus "\<exists>x. \<forall>y\<in>L. y < x" by blast
   5.252 -qed
   5.253 -
   5.254 -lemma dlo_qe_nolb: 
   5.255 -  assumes ne: "U \<noteq> {}" and fU: "finite U"
   5.256 -  shows "(\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y \<in> U. x < y)) \<equiv> True"
   5.257 -proof(simp add: atomize_eq)
   5.258 -  from lt_ex[of "Min U"] obtain M where M: "M < Min U" by blast
   5.259 -  from ne fU have "\<forall>x \<in> U. Min U \<le> x" by simp
   5.260 -  with M have "\<forall>x\<in>U. M < x" by (auto intro: less_le_trans)
   5.261 -  thus "\<exists>x. \<forall>y\<in>U. x < y" by blast
   5.262 -qed
   5.263 -
   5.264 -lemma exists_neq: "\<exists>(x::'a). x \<noteq> t" "\<exists>(x::'a). t \<noteq> x" 
   5.265 -  using gt_ex[of t] by auto
   5.266 -
   5.267 -lemmas dlo_simps = order_refl less_irrefl not_less not_le exists_neq 
   5.268 -  le_less neq_iff linear less_not_permute
   5.269 -
   5.270 -lemma axiom: "dense_linear_order (op \<le>) (op <)" by (rule dense_linear_order_axioms)
   5.271 -lemma atoms:
   5.272 -  includes meta_term_syntax
   5.273 -  shows "TERM (less :: 'a \<Rightarrow> _)"
   5.274 -    and "TERM (less_eq :: 'a \<Rightarrow> _)"
   5.275 -    and "TERM (op = :: 'a \<Rightarrow> _)" .
   5.276 -
   5.277 -declare axiom[langford qe: dlo_qe_bnds dlo_qe_nolb dlo_qe_noub gather: gather_start gather_simps atoms: atoms]
   5.278 -declare dlo_simps[langfordsimp]
   5.279 -
   5.280 -end
   5.281 -
   5.282 -(* FIXME: Move to HOL -- together with the conj_aci_rule in langford.ML *)
   5.283 -lemma dnf:
   5.284 -  "(P & (Q | R)) = ((P&Q) | (P&R))" 
   5.285 -  "((Q | R) & P) = ((Q&P) | (R&P))"
   5.286 -  by blast+
   5.287 -
   5.288 -lemmas weak_dnf_simps = simp_thms dnf
   5.289 -
   5.290 -lemma nnf_simps:
   5.291 -    "(\<not>(P \<and> Q)) = (\<not>P \<or> \<not>Q)" "(\<not>(P \<or> Q)) = (\<not>P \<and> \<not>Q)" "(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
   5.292 -    "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"
   5.293 -  by blast+
   5.294 -
   5.295 -lemma ex_distrib: "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> ((\<exists>x. P x) \<or> (\<exists>x. Q x))" by blast
   5.296 -
   5.297 -lemmas dnf_simps = weak_dnf_simps nnf_simps ex_distrib
   5.298 -
   5.299 -use "Tools/Qelim/langford.ML"
   5.300 -method_setup dlo = {*
   5.301 -  Method.ctxt_args (Method.SIMPLE_METHOD' o LangfordQE.dlo_tac)
   5.302 -*} "Langford's algorithm for quantifier elimination in dense linear orders"
   5.303 -
   5.304 -
   5.305 -section {* Contructive dense linear orders yield QE for linear arithmetic over ordered Fields -- see @{text "Arith_Tools.thy"} *}
   5.306 -
   5.307 -text {* Linear order without upper bounds *}
   5.308 -
   5.309 -locale linorder_stupid_syntax = linorder
   5.310 -begin
   5.311 -notation
   5.312 -  less_eq  ("op \<sqsubseteq>") and
   5.313 -  less_eq  ("(_/ \<sqsubseteq> _)" [51, 51] 50) and
   5.314 -  less  ("op \<sqsubset>") and
   5.315 -  less  ("(_/ \<sqsubset> _)"  [51, 51] 50)
   5.316 -
   5.317 -end
   5.318 -
   5.319 -locale linorder_no_ub = linorder_stupid_syntax +
   5.320 -  assumes gt_ex: "\<exists>y. less x y"
   5.321 -begin
   5.322 -lemma ge_ex: "\<exists>y. x \<sqsubseteq> y" using gt_ex by auto
   5.323 -
   5.324 -text {* Theorems for @{text "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"} *}
   5.325 -lemma pinf_conj:
   5.326 -  assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
   5.327 -  and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
   5.328 -  shows "\<exists>z. \<forall>x. z \<sqsubset>  x \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
   5.329 -proof-
   5.330 -  from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
   5.331 -     and z2: "\<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
   5.332 -  from gt_ex obtain z where z:"ord.max less_eq z1 z2 \<sqsubset> z" by blast
   5.333 -  from z have zz1: "z1 \<sqsubset> z" and zz2: "z2 \<sqsubset> z" by simp_all
   5.334 -  {fix x assume H: "z \<sqsubset> x"
   5.335 -    from less_trans[OF zz1 H] less_trans[OF zz2 H]
   5.336 -    have "(P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2')"  using z1 zz1 z2 zz2 by auto
   5.337 -  }
   5.338 -  thus ?thesis by blast
   5.339 -qed
   5.340 -
   5.341 -lemma pinf_disj:
   5.342 -  assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
   5.343 -  and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
   5.344 -  shows "\<exists>z. \<forall>x. z \<sqsubset>  x \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
   5.345 -proof-
   5.346 -  from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
   5.347 -     and z2: "\<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
   5.348 -  from gt_ex obtain z where z:"ord.max less_eq z1 z2 \<sqsubset> z" by blast
   5.349 -  from z have zz1: "z1 \<sqsubset> z" and zz2: "z2 \<sqsubset> z" by simp_all
   5.350 -  {fix x assume H: "z \<sqsubset> x"
   5.351 -    from less_trans[OF zz1 H] less_trans[OF zz2 H]
   5.352 -    have "(P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2')"  using z1 zz1 z2 zz2 by auto
   5.353 -  }
   5.354 -  thus ?thesis by blast
   5.355 -qed
   5.356 -
   5.357 -lemma pinf_ex: assumes ex:"\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x"
   5.358 -proof-
   5.359 -  from ex obtain z where z: "\<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast
   5.360 -  from gt_ex obtain x where x: "z \<sqsubset> x" by blast
   5.361 -  from z x p1 show ?thesis by blast
   5.362 -qed
   5.363 -
   5.364 -end
   5.365 -
   5.366 -text {* Linear order without upper bounds *}
   5.367 -
   5.368 -locale linorder_no_lb = linorder_stupid_syntax +
   5.369 -  assumes lt_ex: "\<exists>y. less y x"
   5.370 -begin
   5.371 -lemma le_ex: "\<exists>y. y \<sqsubseteq> x" using lt_ex by auto
   5.372 -
   5.373 -
   5.374 -text {* Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"} *}
   5.375 -lemma minf_conj:
   5.376 -  assumes ex1: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
   5.377 -  and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
   5.378 -  shows "\<exists>z. \<forall>x. x \<sqsubset>  z \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
   5.379 -proof-
   5.380 -  from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"and z2: "\<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
   5.381 -  from lt_ex obtain z where z:"z \<sqsubset> ord.min less_eq z1 z2" by blast
   5.382 -  from z have zz1: "z \<sqsubset> z1" and zz2: "z \<sqsubset> z2" by simp_all
   5.383 -  {fix x assume H: "x \<sqsubset> z"
   5.384 -    from less_trans[OF H zz1] less_trans[OF H zz2]
   5.385 -    have "(P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2')"  using z1 zz1 z2 zz2 by auto
   5.386 -  }
   5.387 -  thus ?thesis by blast
   5.388 -qed
   5.389 -
   5.390 -lemma minf_disj:
   5.391 -  assumes ex1: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
   5.392 -  and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
   5.393 -  shows "\<exists>z. \<forall>x. x \<sqsubset>  z \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
   5.394 -proof-
   5.395 -  from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"and z2: "\<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
   5.396 -  from lt_ex obtain z where z:"z \<sqsubset> ord.min less_eq z1 z2" by blast
   5.397 -  from z have zz1: "z \<sqsubset> z1" and zz2: "z \<sqsubset> z2" by simp_all
   5.398 -  {fix x assume H: "x \<sqsubset> z"
   5.399 -    from less_trans[OF H zz1] less_trans[OF H zz2]
   5.400 -    have "(P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2')"  using z1 zz1 z2 zz2 by auto
   5.401 -  }
   5.402 -  thus ?thesis by blast
   5.403 -qed
   5.404 -
   5.405 -lemma minf_ex: assumes ex:"\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x"
   5.406 -proof-
   5.407 -  from ex obtain z where z: "\<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast
   5.408 -  from lt_ex obtain x where x: "x \<sqsubset> z" by blast
   5.409 -  from z x p1 show ?thesis by blast
   5.410 -qed
   5.411 -
   5.412 -end
   5.413 -
   5.414 -
   5.415 -locale constr_dense_linear_order = linorder_no_lb + linorder_no_ub +
   5.416 -  fixes between
   5.417 -  assumes between_less: "less x y \<Longrightarrow> less x (between x y) \<and> less (between x y) y"
   5.418 -     and  between_same: "between x x = x"
   5.419 -
   5.420 -interpretation  constr_dense_linear_order < dense_linear_order 
   5.421 -  apply unfold_locales
   5.422 -  using gt_ex lt_ex between_less
   5.423 -    by (auto, rule_tac x="between x y" in exI, simp)
   5.424 -
   5.425 -context  constr_dense_linear_order
   5.426 -begin
   5.427 -
   5.428 -lemma rinf_U:
   5.429 -  assumes fU: "finite U"
   5.430 -  and lin_dense: "\<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> P x
   5.431 -  \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P y )"
   5.432 -  and nmpiU: "\<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<sqsubseteq> x \<and> x \<sqsubseteq> u')"
   5.433 -  and nmi: "\<not> MP"  and npi: "\<not> PP"  and ex: "\<exists> x.  P x"
   5.434 -  shows "\<exists> u\<in> U. \<exists> u' \<in> U. P (between u u')"
   5.435 -proof-
   5.436 -  from ex obtain x where px: "P x" by blast
   5.437 -  from px nmi npi nmpiU have "\<exists> u\<in> U. \<exists> u' \<in> U. u \<sqsubseteq> x \<and> x \<sqsubseteq> u'" by auto
   5.438 -  then obtain u and u' where uU:"u\<in> U" and uU': "u' \<in> U" and ux:"u \<sqsubseteq> x" and xu':"x \<sqsubseteq> u'" by auto
   5.439 -  from uU have Une: "U \<noteq> {}" by auto
   5.440 -  term "linorder.Min less_eq"
   5.441 -  let ?l = "linorder.Min less_eq U"
   5.442 -  let ?u = "linorder.Max less_eq U"
   5.443 -  have linM: "?l \<in> U" using fU Une by simp
   5.444 -  have uinM: "?u \<in> U" using fU Une by simp
   5.445 -  have lM: "\<forall> t\<in> U. ?l \<sqsubseteq> t" using Une fU by auto
   5.446 -  have Mu: "\<forall> t\<in> U. t \<sqsubseteq> ?u" using Une fU by auto
   5.447 -  have th:"?l \<sqsubseteq> u" using uU Une lM by auto
   5.448 -  from order_trans[OF th ux] have lx: "?l \<sqsubseteq> x" .
   5.449 -  have th: "u' \<sqsubseteq> ?u" using uU' Une Mu by simp
   5.450 -  from order_trans[OF xu' th] have xu: "x \<sqsubseteq> ?u" .
   5.451 -  from finite_set_intervals2[where P="P",OF px lx xu linM uinM fU lM Mu]
   5.452 -  have "(\<exists> s\<in> U. P s) \<or>
   5.453 -      (\<exists> t1\<in> U. \<exists> t2 \<in> U. (\<forall> y. t1 \<sqsubset> y \<and> y \<sqsubset> t2 \<longrightarrow> y \<notin> U) \<and> t1 \<sqsubset> x \<and> x \<sqsubset> t2 \<and> P x)" .
   5.454 -  moreover { fix u assume um: "u\<in>U" and pu: "P u"
   5.455 -    have "between u u = u" by (simp add: between_same)
   5.456 -    with um pu have "P (between u u)" by simp
   5.457 -    with um have ?thesis by blast}
   5.458 -  moreover{
   5.459 -    assume "\<exists> t1\<in> U. \<exists> t2 \<in> U. (\<forall> y. t1 \<sqsubset> y \<and> y \<sqsubset> t2 \<longrightarrow> y \<notin> U) \<and> t1 \<sqsubset> x \<and> x \<sqsubset> t2 \<and> P x"
   5.460 -      then obtain t1 and t2 where t1M: "t1 \<in> U" and t2M: "t2\<in> U"
   5.461 -        and noM: "\<forall> y. t1 \<sqsubset> y \<and> y \<sqsubset> t2 \<longrightarrow> y \<notin> U" and t1x: "t1 \<sqsubset> x" and xt2: "x \<sqsubset> t2" and px: "P x"
   5.462 -        by blast
   5.463 -      from less_trans[OF t1x xt2] have t1t2: "t1 \<sqsubset> t2" .
   5.464 -      let ?u = "between t1 t2"
   5.465 -      from between_less t1t2 have t1lu: "t1 \<sqsubset> ?u" and ut2: "?u \<sqsubset> t2" by auto
   5.466 -      from lin_dense noM t1x xt2 px t1lu ut2 have "P ?u" by blast
   5.467 -      with t1M t2M have ?thesis by blast}
   5.468 -    ultimately show ?thesis by blast
   5.469 -  qed
   5.470 -
   5.471 -theorem fr_eq:
   5.472 -  assumes fU: "finite U"
   5.473 -  and lin_dense: "\<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> P x
   5.474 -   \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P y )"
   5.475 -  and nmibnd: "\<forall>x. \<not> MP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<sqsubseteq> x)"
   5.476 -  and npibnd: "\<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. x \<sqsubseteq> u)"
   5.477 -  and mi: "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x = MP)"  and pi: "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x = PP)"
   5.478 -  shows "(\<exists> x. P x) \<equiv> (MP \<or> PP \<or> (\<exists> u \<in> U. \<exists> u'\<in> U. P (between u u')))"
   5.479 -  (is "_ \<equiv> (_ \<or> _ \<or> ?F)" is "?E \<equiv> ?D")
   5.480 -proof-
   5.481 - {
   5.482 -   assume px: "\<exists> x. P x"
   5.483 -   have "MP \<or> PP \<or> (\<not> MP \<and> \<not> PP)" by blast
   5.484 -   moreover {assume "MP \<or> PP" hence "?D" by blast}
   5.485 -   moreover {assume nmi: "\<not> MP" and npi: "\<not> PP"
   5.486 -     from npmibnd[OF nmibnd npibnd]
   5.487 -     have nmpiU: "\<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<sqsubseteq> x \<and> x \<sqsubseteq> u')" .
   5.488 -     from rinf_U[OF fU lin_dense nmpiU nmi npi px] have "?D" by blast}
   5.489 -   ultimately have "?D" by blast}
   5.490 - moreover
   5.491 - { assume "?D"
   5.492 -   moreover {assume m:"MP" from minf_ex[OF mi m] have "?E" .}
   5.493 -   moreover {assume p: "PP" from pinf_ex[OF pi p] have "?E" . }
   5.494 -   moreover {assume f:"?F" hence "?E" by blast}
   5.495 -   ultimately have "?E" by blast}
   5.496 - ultimately have "?E = ?D" by blast thus "?E \<equiv> ?D" by simp
   5.497 -qed
   5.498 -
   5.499 -lemmas minf_thms = minf_conj minf_disj minf_eq minf_neq minf_lt minf_le minf_gt minf_ge minf_P
   5.500 -lemmas pinf_thms = pinf_conj pinf_disj pinf_eq pinf_neq pinf_lt pinf_le pinf_gt pinf_ge pinf_P
   5.501 -
   5.502 -lemmas nmi_thms = nmi_conj nmi_disj nmi_eq nmi_neq nmi_lt nmi_le nmi_gt nmi_ge nmi_P
   5.503 -lemmas npi_thms = npi_conj npi_disj npi_eq npi_neq npi_lt npi_le npi_gt npi_ge npi_P
   5.504 -lemmas lin_dense_thms = lin_dense_conj lin_dense_disj lin_dense_eq lin_dense_neq lin_dense_lt lin_dense_le lin_dense_gt lin_dense_ge lin_dense_P
   5.505 -
   5.506 -lemma ferrack_axiom: "constr_dense_linear_order less_eq less between"
   5.507 -  by (rule constr_dense_linear_order_axioms)
   5.508 -lemma atoms:
   5.509 -  includes meta_term_syntax
   5.510 -  shows "TERM (less :: 'a \<Rightarrow> _)"
   5.511 -    and "TERM (less_eq :: 'a \<Rightarrow> _)"
   5.512 -    and "TERM (op = :: 'a \<Rightarrow> _)" .
   5.513 -
   5.514 -declare ferrack_axiom [ferrack minf: minf_thms pinf: pinf_thms
   5.515 -    nmi: nmi_thms npi: npi_thms lindense:
   5.516 -    lin_dense_thms qe: fr_eq atoms: atoms]
   5.517 -
   5.518 -declaration {*
   5.519 -let
   5.520 -fun simps phi = map (Morphism.thm phi) [@{thm "not_less"}, @{thm "not_le"}]
   5.521 -fun generic_whatis phi =
   5.522 - let
   5.523 -  val [lt, le] = map (Morphism.term phi) [@{term "op \<sqsubset>"}, @{term "op \<sqsubseteq>"}]
   5.524 -  fun h x t =
   5.525 -   case term_of t of
   5.526 -     Const("op =", _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
   5.527 -                            else Ferrante_Rackoff_Data.Nox
   5.528 -   | @{term "Not"}$(Const("op =", _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
   5.529 -                            else Ferrante_Rackoff_Data.Nox
   5.530 -   | b$y$z => if Term.could_unify (b, lt) then
   5.531 -                 if term_of x aconv y then Ferrante_Rackoff_Data.Lt
   5.532 -                 else if term_of x aconv z then Ferrante_Rackoff_Data.Gt
   5.533 -                 else Ferrante_Rackoff_Data.Nox
   5.534 -             else if Term.could_unify (b, le) then
   5.535 -                 if term_of x aconv y then Ferrante_Rackoff_Data.Le
   5.536 -                 else if term_of x aconv z then Ferrante_Rackoff_Data.Ge
   5.537 -                 else Ferrante_Rackoff_Data.Nox
   5.538 -             else Ferrante_Rackoff_Data.Nox
   5.539 -   | _ => Ferrante_Rackoff_Data.Nox
   5.540 - in h end
   5.541 - fun ss phi = HOL_ss addsimps (simps phi)
   5.542 -in
   5.543 - Ferrante_Rackoff_Data.funs  @{thm "ferrack_axiom"}
   5.544 -  {isolate_conv = K (K (K Thm.reflexive)), whatis = generic_whatis, simpset = ss}
   5.545 -end
   5.546 -*}
   5.547 -
   5.548 -end
   5.549 -
   5.550 -use "Tools/Qelim/ferrante_rackoff.ML"
   5.551 -
   5.552 -method_setup ferrack = {*
   5.553 -  Method.ctxt_args (Method.SIMPLE_METHOD' o FerranteRackoff.dlo_tac)
   5.554 -*} "Ferrante and Rackoff's algorithm for quantifier elimination in dense linear orders"
   5.555 -
   5.556 -end 
     6.1 --- a/src/HOL/Hyperreal/Poly.thy	Thu Jun 26 10:06:54 2008 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,1054 +0,0 @@
     6.4 -(*  Title:       Poly.thy
     6.5 -    ID:         $Id$
     6.6 -    Author:      Jacques D. Fleuriot
     6.7 -    Copyright:   2000 University of Edinburgh
     6.8 -
     6.9 -    Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
    6.10 -*)
    6.11 -
    6.12 -header{*Univariate Real Polynomials*}
    6.13 -
    6.14 -theory Poly
    6.15 -imports Deriv
    6.16 -begin
    6.17 -
    6.18 -text{*Application of polynomial as a real function.*}
    6.19 -
    6.20 -consts poly :: "real list => real => real"
    6.21 -primrec
    6.22 -  poly_Nil:  "poly [] x = 0"
    6.23 -  poly_Cons: "poly (h#t) x = h + x * poly t x"
    6.24 -
    6.25 -
    6.26 -subsection{*Arithmetic Operations on Polynomials*}
    6.27 -
    6.28 -text{*addition*}
    6.29 -consts padd :: "[real list, real list] => real list"  (infixl "+++" 65)
    6.30 -primrec
    6.31 -  padd_Nil:  "[] +++ l2 = l2"
    6.32 -  padd_Cons: "(h#t) +++ l2 = (if l2 = [] then h#t
    6.33 -                            else (h + hd l2)#(t +++ tl l2))"
    6.34 -
    6.35 -text{*Multiplication by a constant*}
    6.36 -consts cmult :: "[real, real list] => real list"  (infixl "%*" 70)
    6.37 -primrec
    6.38 -   cmult_Nil:  "c %* [] = []"
    6.39 -   cmult_Cons: "c %* (h#t) = (c * h)#(c %* t)"
    6.40 -
    6.41 -text{*Multiplication by a polynomial*}
    6.42 -consts pmult :: "[real list, real list] => real list"  (infixl "***" 70)
    6.43 -primrec
    6.44 -   pmult_Nil:  "[] *** l2 = []"
    6.45 -   pmult_Cons: "(h#t) *** l2 = (if t = [] then h %* l2
    6.46 -                              else (h %* l2) +++ ((0) # (t *** l2)))"
    6.47 -
    6.48 -text{*Repeated multiplication by a polynomial*}
    6.49 -consts mulexp :: "[nat, real list, real list] => real list"
    6.50 -primrec
    6.51 -   mulexp_zero:  "mulexp 0 p q = q"
    6.52 -   mulexp_Suc:   "mulexp (Suc n) p q = p *** mulexp n p q"
    6.53 -
    6.54 -text{*Exponential*}
    6.55 -consts pexp :: "[real list, nat] => real list"  (infixl "%^" 80)
    6.56 -primrec
    6.57 -   pexp_0:   "p %^ 0 = [1]"
    6.58 -   pexp_Suc: "p %^ (Suc n) = p *** (p %^ n)"
    6.59 -
    6.60 -text{*Quotient related value of dividing a polynomial by x + a*}
    6.61 -(* Useful for divisor properties in inductive proofs *)
    6.62 -consts "pquot" :: "[real list, real] => real list"
    6.63 -primrec
    6.64 -   pquot_Nil:  "pquot [] a= []"
    6.65 -   pquot_Cons: "pquot (h#t) a = (if t = [] then [h]
    6.66 -                   else (inverse(a) * (h - hd( pquot t a)))#(pquot t a))"
    6.67 -
    6.68 -text{*Differentiation of polynomials (needs an auxiliary function).*}
    6.69 -consts pderiv_aux :: "nat => real list => real list"
    6.70 -primrec
    6.71 -   pderiv_aux_Nil:  "pderiv_aux n [] = []"
    6.72 -   pderiv_aux_Cons: "pderiv_aux n (h#t) =
    6.73 -                     (real n * h)#(pderiv_aux (Suc n) t)"
    6.74 -
    6.75 -text{*normalization of polynomials (remove extra 0 coeff)*}
    6.76 -consts pnormalize :: "real list => real list"
    6.77 -primrec
    6.78 -   pnormalize_Nil:  "pnormalize [] = []"
    6.79 -   pnormalize_Cons: "pnormalize (h#p) = (if ( (pnormalize p) = [])
    6.80 -                                     then (if (h = 0) then [] else [h])
    6.81 -                                     else (h#(pnormalize p)))"
    6.82 -
    6.83 -definition "pnormal p = ((pnormalize p = p) \<and> p \<noteq> [])"
    6.84 -definition "nonconstant p = (pnormal p \<and> (\<forall>x. p \<noteq> [x]))"
    6.85 -text{*Other definitions*}
    6.86 -
    6.87 -definition
    6.88 -  poly_minus :: "real list => real list"      ("-- _" [80] 80) where
    6.89 -  "-- p = (- 1) %* p"
    6.90 -
    6.91 -definition
    6.92 -  pderiv :: "real list => real list" where
    6.93 -  "pderiv p = (if p = [] then [] else pderiv_aux 1 (tl p))"
    6.94 -
    6.95 -definition
    6.96 -  divides :: "[real list,real list] => bool"  (infixl "divides" 70) where
    6.97 -  "p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))"
    6.98 -
    6.99 -definition
   6.100 -  order :: "real => real list => nat" where
   6.101 -    --{*order of a polynomial*}
   6.102 -  "order a p = (SOME n. ([-a, 1] %^ n) divides p &
   6.103 -                      ~ (([-a, 1] %^ (Suc n)) divides p))"
   6.104 -
   6.105 -definition
   6.106 -  degree :: "real list => nat" where
   6.107 -     --{*degree of a polynomial*}
   6.108 -  "degree p = length (pnormalize p) - 1"
   6.109 -
   6.110 -definition
   6.111 -  rsquarefree :: "real list => bool" where
   6.112 -     --{*squarefree polynomials --- NB with respect to real roots only.*}
   6.113 -  "rsquarefree p = (poly p \<noteq> poly [] &
   6.114 -                     (\<forall>a. (order a p = 0) | (order a p = 1)))"
   6.115 -
   6.116 -
   6.117 -
   6.118 -lemma padd_Nil2: "p +++ [] = p"
   6.119 -by (induct p) auto
   6.120 -declare padd_Nil2 [simp]
   6.121 -
   6.122 -lemma padd_Cons_Cons: "(h1 # p1) +++ (h2 # p2) = (h1 + h2) # (p1 +++ p2)"
   6.123 -by auto
   6.124 -
   6.125 -lemma pminus_Nil: "-- [] = []"
   6.126 -by (simp add: poly_minus_def)
   6.127 -declare pminus_Nil [simp]
   6.128 -
   6.129 -lemma pmult_singleton: "[h1] *** p1 = h1 %* p1"
   6.130 -by simp
   6.131 -
   6.132 -lemma poly_ident_mult: "1 %* t = t"
   6.133 -by (induct "t", auto)
   6.134 -declare poly_ident_mult [simp]
   6.135 -
   6.136 -lemma poly_simple_add_Cons: "[a] +++ ((0)#t) = (a#t)"
   6.137 -by simp
   6.138 -declare poly_simple_add_Cons [simp]
   6.139 -
   6.140 -text{*Handy general properties*}
   6.141 -
   6.142 -lemma padd_commut: "b +++ a = a +++ b"
   6.143 -apply (subgoal_tac "\<forall>a. b +++ a = a +++ b")
   6.144 -apply (induct_tac [2] "b", auto)
   6.145 -apply (rule padd_Cons [THEN ssubst])
   6.146 -apply (case_tac "aa", auto)
   6.147 -done
   6.148 -
   6.149 -lemma padd_assoc [rule_format]: "\<forall>b c. (a +++ b) +++ c = a +++ (b +++ c)"
   6.150 -apply (induct "a", simp, clarify)
   6.151 -apply (case_tac b, simp_all)
   6.152 -done
   6.153 -
   6.154 -lemma poly_cmult_distr [rule_format]:
   6.155 -     "\<forall>q. a %* ( p +++ q) = (a %* p +++ a %* q)"
   6.156 -apply (induct "p", simp, clarify) 
   6.157 -apply (case_tac "q")
   6.158 -apply (simp_all add: right_distrib)
   6.159 -done
   6.160 -
   6.161 -lemma pmult_by_x: "[0, 1] *** t = ((0)#t)"
   6.162 -apply (induct "t", simp)
   6.163 -apply (auto simp add: poly_ident_mult padd_commut)
   6.164 -done
   6.165 -declare pmult_by_x [simp]
   6.166 -
   6.167 -
   6.168 -text{*properties of evaluation of polynomials.*}
   6.169 -
   6.170 -lemma poly_add: "poly (p1 +++ p2) x = poly p1 x + poly p2 x"
   6.171 -apply (subgoal_tac "\<forall>p2. poly (p1 +++ p2) x = poly (p1) x + poly (p2) x")
   6.172 -apply (induct_tac [2] "p1", auto)
   6.173 -apply (case_tac "p2")
   6.174 -apply (auto simp add: right_distrib)
   6.175 -done
   6.176 -
   6.177 -lemma poly_cmult: "poly (c %* p) x = c * poly p x"
   6.178 -apply (induct "p") 
   6.179 -apply (case_tac [2] "x=0")
   6.180 -apply (auto simp add: right_distrib mult_ac)
   6.181 -done
   6.182 -
   6.183 -lemma poly_minus: "poly (-- p) x = - (poly p x)"
   6.184 -apply (simp add: poly_minus_def)
   6.185 -apply (auto simp add: poly_cmult)
   6.186 -done
   6.187 -
   6.188 -lemma poly_mult: "poly (p1 *** p2) x = poly p1 x * poly p2 x"
   6.189 -apply (subgoal_tac "\<forall>p2. poly (p1 *** p2) x = poly p1 x * poly p2 x")
   6.190 -apply (simp (no_asm_simp))
   6.191 -apply (induct "p1")
   6.192 -apply (auto simp add: poly_cmult)
   6.193 -apply (case_tac p1)
   6.194 -apply (auto simp add: poly_cmult poly_add left_distrib right_distrib mult_ac)
   6.195 -done
   6.196 -
   6.197 -lemma poly_exp: "poly (p %^ n) x = (poly p x) ^ n"
   6.198 -apply (induct "n")
   6.199 -apply (auto simp add: poly_cmult poly_mult)
   6.200 -done
   6.201 -
   6.202 -text{*More Polynomial Evaluation Lemmas*}
   6.203 -
   6.204 -lemma poly_add_rzero: "poly (a +++ []) x = poly a x"
   6.205 -by simp
   6.206 -declare poly_add_rzero [simp]
   6.207 -
   6.208 -lemma poly_mult_assoc: "poly ((a *** b) *** c) x = poly (a *** (b *** c)) x"
   6.209 -by (simp add: poly_mult real_mult_assoc)
   6.210 -
   6.211 -lemma poly_mult_Nil2: "poly (p *** []) x = 0"
   6.212 -by (induct "p", auto)
   6.213 -declare poly_mult_Nil2 [simp]
   6.214 -
   6.215 -lemma poly_exp_add: "poly (p %^ (n + d)) x = poly( p %^ n *** p %^ d) x"
   6.216 -apply (induct "n")
   6.217 -apply (auto simp add: poly_mult real_mult_assoc)
   6.218 -done
   6.219 -
   6.220 -text{*The derivative*}
   6.221 -
   6.222 -lemma pderiv_Nil: "pderiv [] = []"
   6.223 -
   6.224 -apply (simp add: pderiv_def)
   6.225 -done
   6.226 -declare pderiv_Nil [simp]
   6.227 -
   6.228 -lemma pderiv_singleton: "pderiv [c] = []"
   6.229 -by (simp add: pderiv_def)
   6.230 -declare pderiv_singleton [simp]
   6.231 -
   6.232 -lemma pderiv_Cons: "pderiv (h#t) = pderiv_aux 1 t"
   6.233 -by (simp add: pderiv_def)
   6.234 -
   6.235 -lemma DERIV_cmult2: "DERIV f x :> D ==> DERIV (%x. (f x) * c :: real) x :> D * c"
   6.236 -by (simp add: DERIV_cmult mult_commute [of _ c])
   6.237 -
   6.238 -lemma DERIV_pow2: "DERIV (%x. x ^ Suc n) x :> real (Suc n) * (x ^ n)"
   6.239 -by (rule lemma_DERIV_subst, rule DERIV_pow, simp)
   6.240 -declare DERIV_pow2 [simp] DERIV_pow [simp]
   6.241 -
   6.242 -lemma lemma_DERIV_poly1: "\<forall>n. DERIV (%x. (x ^ (Suc n) * poly p x)) x :>
   6.243 -        x ^ n * poly (pderiv_aux (Suc n) p) x "
   6.244 -apply (induct "p")
   6.245 -apply (auto intro!: DERIV_add DERIV_cmult2 
   6.246 -            simp add: pderiv_def right_distrib real_mult_assoc [symmetric] 
   6.247 -            simp del: realpow_Suc)
   6.248 -apply (subst mult_commute) 
   6.249 -apply (simp del: realpow_Suc) 
   6.250 -apply (simp add: mult_commute realpow_Suc [symmetric] del: realpow_Suc)
   6.251 -done
   6.252 -
   6.253 -lemma lemma_DERIV_poly: "DERIV (%x. (x ^ (Suc n) * poly p x)) x :>
   6.254 -        x ^ n * poly (pderiv_aux (Suc n) p) x "
   6.255 -by (simp add: lemma_DERIV_poly1 del: realpow_Suc)
   6.256 -
   6.257 -lemma DERIV_add_const: "DERIV f x :> D ==>  DERIV (%x. a + f x :: real) x :> D"
   6.258 -by (rule lemma_DERIV_subst, rule DERIV_add, auto)
   6.259 -
   6.260 -lemma poly_DERIV: "DERIV (%x. poly p x) x :> poly (pderiv p) x"
   6.261 -apply (induct "p")
   6.262 -apply (auto simp add: pderiv_Cons)
   6.263 -apply (rule DERIV_add_const)
   6.264 -apply (rule lemma_DERIV_subst)
   6.265 -apply (rule lemma_DERIV_poly [where n=0, simplified], simp) 
   6.266 -done
   6.267 -declare poly_DERIV [simp]
   6.268 -
   6.269 -
   6.270 -text{* Consequences of the derivative theorem above*}
   6.271 -
   6.272 -lemma poly_differentiable: "(%x. poly p x) differentiable x"
   6.273 -
   6.274 -apply (simp add: differentiable_def)
   6.275 -apply (blast intro: poly_DERIV)
   6.276 -done
   6.277 -declare poly_differentiable [simp]
   6.278 -
   6.279 -lemma poly_isCont: "isCont (%x. poly p x) x"
   6.280 -by (rule poly_DERIV [THEN DERIV_isCont])
   6.281 -declare poly_isCont [simp]
   6.282 -
   6.283 -lemma poly_IVT_pos: "[| a < b; poly p a < 0; 0 < poly p b |]
   6.284 -      ==> \<exists>x. a < x & x < b & (poly p x = 0)"
   6.285 -apply (cut_tac f = "%x. poly p x" and a = a and b = b and y = 0 in IVT_objl)
   6.286 -apply (auto simp add: order_le_less)
   6.287 -done
   6.288 -
   6.289 -lemma poly_IVT_neg: "[| a < b; 0 < poly p a; poly p b < 0 |]
   6.290 -      ==> \<exists>x. a < x & x < b & (poly p x = 0)"
   6.291 -apply (insert poly_IVT_pos [where p = "-- p" ]) 
   6.292 -apply (simp add: poly_minus neg_less_0_iff_less) 
   6.293 -done
   6.294 -
   6.295 -lemma poly_MVT: "a < b ==>
   6.296 -     \<exists>x. a < x & x < b & (poly p b - poly p a = (b - a) * poly (pderiv p) x)"
   6.297 -apply (drule_tac f = "poly p" in MVT, auto)
   6.298 -apply (rule_tac x = z in exI)
   6.299 -apply (auto simp add: real_mult_left_cancel poly_DERIV [THEN DERIV_unique])
   6.300 -done
   6.301 -
   6.302 -text{*Lemmas for Derivatives*}
   6.303 -
   6.304 -lemma lemma_poly_pderiv_aux_add: "\<forall>p2 n. poly (pderiv_aux n (p1 +++ p2)) x =
   6.305 -                poly (pderiv_aux n p1 +++ pderiv_aux n p2) x"
   6.306 -apply (induct "p1", simp, clarify) 
   6.307 -apply (case_tac "p2")
   6.308 -apply (auto simp add: right_distrib)
   6.309 -done
   6.310 -
   6.311 -lemma poly_pderiv_aux_add: "poly (pderiv_aux n (p1 +++ p2)) x =
   6.312 -      poly (pderiv_aux n p1 +++ pderiv_aux n p2) x"
   6.313 -apply (simp add: lemma_poly_pderiv_aux_add)
   6.314 -done
   6.315 -
   6.316 -lemma lemma_poly_pderiv_aux_cmult: "\<forall>n. poly (pderiv_aux n (c %* p)) x = poly (c %* pderiv_aux n p) x"
   6.317 -apply (induct "p")
   6.318 -apply (auto simp add: poly_cmult mult_ac)
   6.319 -done
   6.320 -
   6.321 -lemma poly_pderiv_aux_cmult: "poly (pderiv_aux n (c %* p)) x = poly (c %* pderiv_aux n p) x"
   6.322 -by (simp add: lemma_poly_pderiv_aux_cmult)
   6.323 -
   6.324 -lemma poly_pderiv_aux_minus:
   6.325 -   "poly (pderiv_aux n (-- p)) x = poly (-- pderiv_aux n p) x"
   6.326 -apply (simp add: poly_minus_def poly_pderiv_aux_cmult)
   6.327 -done
   6.328 -
   6.329 -lemma lemma_poly_pderiv_aux_mult1: "\<forall>n. poly (pderiv_aux (Suc n) p) x = poly ((pderiv_aux n p) +++ p) x"
   6.330 -apply (induct "p")
   6.331 -apply (auto simp add: real_of_nat_Suc left_distrib)
   6.332 -done
   6.333 -
   6.334 -lemma lemma_poly_pderiv_aux_mult: "poly (pderiv_aux (Suc n) p) x = poly ((pderiv_aux n p) +++ p) x"
   6.335 -by (simp add: lemma_poly_pderiv_aux_mult1)
   6.336 -
   6.337 -lemma lemma_poly_pderiv_add: "\<forall>q. poly (pderiv (p +++ q)) x = poly (pderiv p +++ pderiv q) x"
   6.338 -apply (induct "p", simp, clarify) 
   6.339 -apply (case_tac "q")
   6.340 -apply (auto simp add: poly_pderiv_aux_add poly_add pderiv_def)
   6.341 -done
   6.342 -
   6.343 -lemma poly_pderiv_add: "poly (pderiv (p +++ q)) x = poly (pderiv p +++ pderiv q) x"
   6.344 -by (simp add: lemma_poly_pderiv_add)
   6.345 -
   6.346 -lemma poly_pderiv_cmult: "poly (pderiv (c %* p)) x = poly (c %* (pderiv p)) x"
   6.347 -apply (induct "p")
   6.348 -apply (auto simp add: poly_pderiv_aux_cmult poly_cmult pderiv_def)
   6.349 -done
   6.350 -
   6.351 -lemma poly_pderiv_minus: "poly (pderiv (--p)) x = poly (--(pderiv p)) x"
   6.352 -by (simp add: poly_minus_def poly_pderiv_cmult)
   6.353 -
   6.354 -lemma lemma_poly_mult_pderiv:
   6.355 -   "poly (pderiv (h#t)) x = poly ((0 # (pderiv t)) +++ t) x"
   6.356 -apply (simp add: pderiv_def)
   6.357 -apply (induct "t")
   6.358 -apply (auto simp add: poly_add lemma_poly_pderiv_aux_mult)
   6.359 -done
   6.360 -
   6.361 -lemma poly_pderiv_mult: "\<forall>q. poly (pderiv (p *** q)) x =
   6.362 -      poly (p *** (pderiv q) +++ q *** (pderiv p)) x"
   6.363 -apply (induct "p")
   6.364 -apply (auto simp add: poly_add poly_cmult poly_pderiv_cmult poly_pderiv_add poly_mult)
   6.365 -apply (rule lemma_poly_mult_pderiv [THEN ssubst])
   6.366 -apply (rule lemma_poly_mult_pderiv [THEN ssubst])
   6.367 -apply (rule poly_add [THEN ssubst])
   6.368 -apply (rule poly_add [THEN ssubst])
   6.369 -apply (simp (no_asm_simp) add: poly_mult right_distrib add_ac mult_ac)
   6.370 -done
   6.371 -
   6.372 -lemma poly_pderiv_exp: "poly (pderiv (p %^ (Suc n))) x =
   6.373 -         poly ((real (Suc n)) %* (p %^ n) *** pderiv p) x"
   6.374 -apply (induct "n")
   6.375 -apply (auto simp add: poly_add poly_pderiv_cmult poly_cmult poly_pderiv_mult
   6.376 -                      real_of_nat_zero poly_mult real_of_nat_Suc 
   6.377 -                      right_distrib left_distrib mult_ac)
   6.378 -done
   6.379 -
   6.380 -lemma poly_pderiv_exp_prime: "poly (pderiv ([-a, 1] %^ (Suc n))) x =
   6.381 -      poly (real (Suc n) %* ([-a, 1] %^ n)) x"
   6.382 -apply (simp add: poly_pderiv_exp poly_mult del: pexp_Suc)
   6.383 -apply (simp add: poly_cmult pderiv_def)
   6.384 -done
   6.385 -
   6.386 -subsection{*Key Property: if @{term "f(a) = 0"} then @{term "(x - a)"} divides
   6.387 - @{term "p(x)"} *}
   6.388 -
   6.389 -lemma lemma_poly_linear_rem: "\<forall>h. \<exists>q r. h#t = [r] +++ [-a, 1] *** q"
   6.390 -apply (induct "t", safe)
   6.391 -apply (rule_tac x = "[]" in exI)
   6.392 -apply (rule_tac x = h in exI, simp)
   6.393 -apply (drule_tac x = aa in spec, safe)
   6.394 -apply (rule_tac x = "r#q" in exI)
   6.395 -apply (rule_tac x = "a*r + h" in exI)
   6.396 -apply (case_tac "q", auto)
   6.397 -done
   6.398 -
   6.399 -lemma poly_linear_rem: "\<exists>q r. h#t = [r] +++ [-a, 1] *** q"
   6.400 -by (cut_tac t = t and a = a in lemma_poly_linear_rem, auto)
   6.401 -
   6.402 -
   6.403 -lemma poly_linear_divides: "(poly p a = 0) = ((p = []) | (\<exists>q. p = [-a, 1] *** q))"
   6.404 -apply (auto simp add: poly_add poly_cmult right_distrib)
   6.405 -apply (case_tac "p", simp) 
   6.406 -apply (cut_tac h = aa and t = list and a = a in poly_linear_rem, safe)
   6.407 -apply (case_tac "q", auto)
   6.408 -apply (drule_tac x = "[]" in spec, simp)
   6.409 -apply (auto simp add: poly_add poly_cmult add_assoc)
   6.410 -apply (drule_tac x = "aa#lista" in spec, auto)
   6.411 -done
   6.412 -
   6.413 -lemma lemma_poly_length_mult: "\<forall>h k a. length (k %* p +++  (h # (a %* p))) = Suc (length p)"
   6.414 -by (induct "p", auto)
   6.415 -declare lemma_poly_length_mult [simp]
   6.416 -
   6.417 -lemma lemma_poly_length_mult2: "\<forall>h k. length (k %* p +++  (h # p)) = Suc (length p)"
   6.418 -by (induct "p", auto)
   6.419 -declare lemma_poly_length_mult2 [simp]
   6.420 -
   6.421 -lemma poly_length_mult: "length([-a,1] *** q) = Suc (length q)"
   6.422 -by auto
   6.423 -declare poly_length_mult [simp]
   6.424 -
   6.425 -
   6.426 -subsection{*Polynomial length*}
   6.427 -
   6.428 -lemma poly_cmult_length: "length (a %* p) = length p"
   6.429 -by (induct "p", auto)
   6.430 -declare poly_cmult_length [simp]
   6.431 -
   6.432 -lemma poly_add_length [rule_format]:
   6.433 -     "\<forall>p2. length (p1 +++ p2) =
   6.434 -             (if (length p1 < length p2) then length p2 else length p1)"
   6.435 -apply (induct "p1", simp_all)
   6.436 -apply arith
   6.437 -done
   6.438 -
   6.439 -lemma poly_root_mult_length: "length([a,b] *** p) = Suc (length p)"
   6.440 -by (simp add: poly_cmult_length poly_add_length)
   6.441 -declare poly_root_mult_length [simp]
   6.442 -
   6.443 -lemma poly_mult_not_eq_poly_Nil: "(poly (p *** q) x \<noteq> poly [] x) =
   6.444 -      (poly p x \<noteq> poly [] x & poly q x \<noteq> poly [] x)"
   6.445 -apply (auto simp add: poly_mult)
   6.446 -done
   6.447 -declare poly_mult_not_eq_poly_Nil [simp]
   6.448 -
   6.449 -lemma poly_mult_eq_zero_disj: "(poly (p *** q) x = 0) = (poly p x = 0 | poly q x = 0)"
   6.450 -by (auto simp add: poly_mult)
   6.451 -
   6.452 -text{*Normalisation Properties*}
   6.453 -
   6.454 -lemma poly_normalized_nil: "(pnormalize p = []) --> (poly p x = 0)"
   6.455 -by (induct "p", auto)
   6.456 -
   6.457 -text{*A nontrivial polynomial of degree n has no more than n roots*}
   6.458 -
   6.459 -lemma poly_roots_index_lemma [rule_format]:
   6.460 -   "\<forall>p x. poly p x \<noteq> poly [] x & length p = n
   6.461 -    --> (\<exists>i. \<forall>x. (poly p x = (0::real)) --> (\<exists>m. (m \<le> n & x = i m)))"
   6.462 -apply (induct "n", safe)
   6.463 -apply (rule ccontr)
   6.464 -apply (subgoal_tac "\<exists>a. poly p a = 0", safe)
   6.465 -apply (drule poly_linear_divides [THEN iffD1], safe)
   6.466 -apply (drule_tac x = q in spec)
   6.467 -apply (drule_tac x = x in spec)
   6.468 -apply (simp del: poly_Nil pmult_Cons)
   6.469 -apply (erule exE)
   6.470 -apply (drule_tac x = "%m. if m = Suc n then a else i m" in spec, safe)
   6.471 -apply (drule poly_mult_eq_zero_disj [THEN iffD1], safe)
   6.472 -apply (drule_tac x = "Suc (length q)" in spec)
   6.473 -apply simp
   6.474 -apply (drule_tac x = xa in spec, safe)
   6.475 -apply (drule_tac x = m in spec, simp, blast)
   6.476 -done
   6.477 -lemmas poly_roots_index_lemma2 = conjI [THEN poly_roots_index_lemma, standard]
   6.478 -
   6.479 -lemma poly_roots_index_length: "poly p x \<noteq> poly [] x ==>
   6.480 -      \<exists>i. \<forall>x. (poly p x = 0) --> (\<exists>n. n \<le> length p & x = i n)"
   6.481 -by (blast intro: poly_roots_index_lemma2)
   6.482 -
   6.483 -lemma poly_roots_finite_lemma: "poly p x \<noteq> poly [] x ==>
   6.484 -      \<exists>N i. \<forall>x. (poly p x = 0) --> (\<exists>n. (n::nat) < N & x = i n)"
   6.485 -apply (drule poly_roots_index_length, safe)
   6.486 -apply (rule_tac x = "Suc (length p)" in exI)
   6.487 -apply (rule_tac x = i in exI) 
   6.488 -apply (simp add: less_Suc_eq_le)
   6.489 -done
   6.490 -
   6.491 -(* annoying proof *)
   6.492 -lemma real_finite_lemma [rule_format (no_asm)]:
   6.493 -     "\<forall>P. (\<forall>x. P x --> (\<exists>n. n < N & x = (j::nat=>real) n))
   6.494 -      --> (\<exists>a. \<forall>x. P x --> x < a)"
   6.495 -apply (induct "N", simp, safe)
   6.496 -apply (drule_tac x = "%z. P z & (z \<noteq> j N)" in spec)
   6.497 -apply (auto simp add: less_Suc_eq)
   6.498 -apply (rename_tac N P a) 
   6.499 -apply (rule_tac x = "abs a + abs (j N) + 1" in exI)
   6.500 -apply safe
   6.501 -apply (drule_tac x = x in spec, safe) 
   6.502 -apply (drule_tac x = "j n" in spec)
   6.503 -apply arith
   6.504 -apply arith
   6.505 -done
   6.506 -
   6.507 -lemma poly_roots_finite: "(poly p \<noteq> poly []) =
   6.508 -      (\<exists>N j. \<forall>x. poly p x = 0 --> (\<exists>n. (n::nat) < N & x = j n))"
   6.509 -apply safe
   6.510 -apply (erule contrapos_np, rule ext)
   6.511 -apply (rule ccontr)
   6.512 -apply (clarify dest!: poly_roots_finite_lemma)
   6.513 -apply (clarify dest!: real_finite_lemma)
   6.514 -apply (drule_tac x = a in fun_cong, auto)
   6.515 -done
   6.516 -
   6.517 -text{*Entirety and Cancellation for polynomials*}
   6.518 -
   6.519 -lemma poly_entire_lemma: "[| poly p \<noteq> poly [] ; poly q \<noteq> poly [] |]
   6.520 -      ==>  poly (p *** q) \<noteq> poly []"
   6.521 -apply (auto simp add: poly_roots_finite)
   6.522 -apply (rule_tac x = "N + Na" in exI)
   6.523 -apply (rule_tac x = "%n. if n < N then j n else ja (n - N)" in exI)
   6.524 -apply (auto simp add: poly_mult_eq_zero_disj, force) 
   6.525 -done
   6.526 -
   6.527 -lemma poly_entire: "(poly (p *** q) = poly []) = ((poly p = poly []) | (poly q = poly []))"
   6.528 -apply (auto intro: ext dest: fun_cong simp add: poly_entire_lemma poly_mult)
   6.529 -apply (blast intro: ccontr dest: poly_entire_lemma poly_mult [THEN subst])
   6.530 -done
   6.531 -
   6.532 -lemma poly_entire_neg: "(poly (p *** q) \<noteq> poly []) = ((poly p \<noteq> poly []) & (poly q \<noteq> poly []))"
   6.533 -by (simp add: poly_entire)
   6.534 -
   6.535 -lemma fun_eq: " (f = g) = (\<forall>x. f x = g x)"
   6.536 -by (auto intro!: ext)
   6.537 -
   6.538 -lemma poly_add_minus_zero_iff: "(poly (p +++ -- q) = poly []) = (poly p = poly q)"
   6.539 -by (auto simp add: poly_add poly_minus_def fun_eq poly_cmult)
   6.540 -
   6.541 -lemma poly_add_minus_mult_eq: "poly (p *** q +++ --(p *** r)) = poly (p *** (q +++ -- r))"
   6.542 -by (auto simp add: poly_add poly_minus_def fun_eq poly_mult poly_cmult right_distrib)
   6.543 -
   6.544 -lemma poly_mult_left_cancel: "(poly (p *** q) = poly (p *** r)) = (poly p = poly [] | poly q = poly r)"
   6.545 -apply (rule_tac p1 = "p *** q" in poly_add_minus_zero_iff [THEN subst])
   6.546 -apply (auto intro: ext simp add: poly_add_minus_mult_eq poly_entire poly_add_minus_zero_iff)
   6.547 -done
   6.548 -
   6.549 -lemma real_mult_zero_disj_iff: "(x * y = 0) = (x = (0::real) | y = 0)"
   6.550 -by simp
   6.551 -
   6.552 -lemma poly_exp_eq_zero:
   6.553 -     "(poly (p %^ n) = poly []) = (poly p = poly [] & n \<noteq> 0)"
   6.554 -apply (simp only: fun_eq add: all_simps [symmetric]) 
   6.555 -apply (rule arg_cong [where f = All]) 
   6.556 -apply (rule ext)
   6.557 -apply (induct_tac "n")
   6.558 -apply (auto simp add: poly_mult real_mult_zero_disj_iff)
   6.559 -done
   6.560 -declare poly_exp_eq_zero [simp]
   6.561 -
   6.562 -lemma poly_prime_eq_zero: "poly [a,1] \<noteq> poly []"
   6.563 -apply (simp add: fun_eq)
   6.564 -apply (rule_tac x = "1 - a" in exI, simp)
   6.565 -done
   6.566 -declare poly_prime_eq_zero [simp]
   6.567 -
   6.568 -lemma poly_exp_prime_eq_zero: "(poly ([a, 1] %^ n) \<noteq> poly [])"
   6.569 -by auto
   6.570 -declare poly_exp_prime_eq_zero [simp]
   6.571 -
   6.572 -text{*A more constructive notion of polynomials being trivial*}
   6.573 -
   6.574 -lemma poly_zero_lemma: "poly (h # t) = poly [] ==> h = 0 & poly t = poly []"
   6.575 -apply (simp add: fun_eq)
   6.576 -apply (case_tac "h = 0")
   6.577 -apply (drule_tac [2] x = 0 in spec, auto) 
   6.578 -apply (case_tac "poly t = poly []", simp) 
   6.579 -apply (auto simp add: poly_roots_finite real_mult_zero_disj_iff)
   6.580 -apply (drule real_finite_lemma, safe)
   6.581 -apply (drule_tac x = "abs a + 1" in spec)+
   6.582 -apply arith
   6.583 -done
   6.584 -
   6.585 -
   6.586 -lemma poly_zero: "(poly p = poly []) = list_all (%c. c = 0) p"
   6.587 -apply (induct "p", simp)
   6.588 -apply (rule iffI)
   6.589 -apply (drule poly_zero_lemma, auto)
   6.590 -done
   6.591 -
   6.592 -declare real_mult_zero_disj_iff [simp]
   6.593 -
   6.594 -lemma pderiv_aux_iszero [rule_format, simp]:
   6.595 -  "\<forall>n. list_all (%c. c = 0) (pderiv_aux (Suc n) p) = list_all (%c. c = 0) p"
   6.596 -by (induct "p", auto)
   6.597 -
   6.598 -lemma pderiv_aux_iszero_num: "(number_of n :: nat) \<noteq> 0
   6.599 -  ==> (list_all (%c. c = 0) (pderiv_aux (number_of n) p) =
   6.600 -      list_all (%c. c = 0) p)"
   6.601 -apply(drule  not0_implies_Suc, clarify)
   6.602 -apply (rule_tac n1 = "m" in pderiv_aux_iszero [THEN subst])
   6.603 -apply (simp (no_asm_simp) del: pderiv_aux_iszero)
   6.604 -done
   6.605 -
   6.606 -lemma pderiv_iszero [rule_format]:
   6.607 -     "poly (pderiv p) = poly [] --> (\<exists>h. poly p = poly [h])"
   6.608 -apply (simp add: poly_zero)
   6.609 -apply (induct "p", force)
   6.610 -apply (simp add: pderiv_Cons pderiv_aux_iszero_num del: poly_Cons)
   6.611 -apply (auto simp add: poly_zero [symmetric])
   6.612 -done
   6.613 -
   6.614 -lemma pderiv_zero_obj: "poly p = poly [] --> (poly (pderiv p) = poly [])"
   6.615 -apply (simp add: poly_zero)
   6.616 -apply (induct "p", force)
   6.617 -apply (simp add: pderiv_Cons pderiv_aux_iszero_num del: poly_Cons)
   6.618 -done
   6.619 -
   6.620 -lemma pderiv_zero: "poly p = poly [] ==> (poly (pderiv p) = poly [])"
   6.621 -by (blast elim: pderiv_zero_obj [THEN impE])
   6.622 -declare pderiv_zero [simp]
   6.623 -
   6.624 -lemma poly_pderiv_welldef: "poly p = poly q ==> (poly (pderiv p) = poly (pderiv q))"
   6.625 -apply (cut_tac p = "p +++ --q" in pderiv_zero_obj)
   6.626 -apply (simp add: fun_eq poly_add poly_minus poly_pderiv_add poly_pderiv_minus del: pderiv_zero)
   6.627 -done
   6.628 -
   6.629 -text{*Basics of divisibility.*}
   6.630 -
   6.631 -lemma poly_primes: "([a, 1] divides (p *** q)) = ([a, 1] divides p | [a, 1] divides q)"
   6.632 -apply (auto simp add: divides_def fun_eq poly_mult poly_add poly_cmult left_distrib [symmetric])
   6.633 -apply (drule_tac x = "-a" in spec)
   6.634 -apply (auto simp add: poly_linear_divides poly_add poly_cmult left_distrib [symmetric])
   6.635 -apply (rule_tac x = "qa *** q" in exI)
   6.636 -apply (rule_tac [2] x = "p *** qa" in exI)
   6.637 -apply (auto simp add: poly_add poly_mult poly_cmult mult_ac)
   6.638 -done
   6.639 -
   6.640 -lemma poly_divides_refl: "p divides p"
   6.641 -apply (simp add: divides_def)
   6.642 -apply (rule_tac x = "[1]" in exI)
   6.643 -apply (auto simp add: poly_mult fun_eq)
   6.644 -done
   6.645 -declare poly_divides_refl [simp]
   6.646 -
   6.647 -lemma poly_divides_trans: "[| p divides q; q divides r |] ==> p divides r"
   6.648 -apply (simp add: divides_def, safe)
   6.649 -apply (rule_tac x = "qa *** qaa" in exI)
   6.650 -apply (auto simp add: poly_mult fun_eq real_mult_assoc)
   6.651 -done
   6.652 -
   6.653 -lemma poly_divides_exp: "m \<le> n ==> (p %^ m) divides (p %^ n)"
   6.654 -apply (auto simp add: le_iff_add)
   6.655 -apply (induct_tac k)
   6.656 -apply (rule_tac [2] poly_divides_trans)
   6.657 -apply (auto simp add: divides_def)
   6.658 -apply (rule_tac x = p in exI)
   6.659 -apply (auto simp add: poly_mult fun_eq mult_ac)
   6.660 -done
   6.661 -
   6.662 -lemma poly_exp_divides: "[| (p %^ n) divides q;  m\<le>n |] ==> (p %^ m) divides q"
   6.663 -by (blast intro: poly_divides_exp poly_divides_trans)
   6.664 -
   6.665 -lemma poly_divides_add:
   6.666 -   "[| p divides q; p divides r |] ==> p divides (q +++ r)"
   6.667 -apply (simp add: divides_def, auto)
   6.668 -apply (rule_tac x = "qa +++ qaa" in exI)
   6.669 -apply (auto simp add: poly_add fun_eq poly_mult right_distrib)
   6.670 -done
   6.671 -
   6.672 -lemma poly_divides_diff:
   6.673 -   "[| p divides q; p divides (q +++ r) |] ==> p divides r"
   6.674 -apply (simp add: divides_def, auto)
   6.675 -apply (rule_tac x = "qaa +++ -- qa" in exI)
   6.676 -apply (auto simp add: poly_add fun_eq poly_mult poly_minus right_diff_distrib compare_rls add_ac)
   6.677 -done
   6.678 -
   6.679 -lemma poly_divides_diff2: "[| p divides r; p divides (q +++ r) |] ==> p divides q"
   6.680 -apply (erule poly_divides_diff)
   6.681 -apply (auto simp add: poly_add fun_eq poly_mult divides_def add_ac)
   6.682 -done
   6.683 -
   6.684 -lemma poly_divides_zero: "poly p = poly [] ==> q divides p"
   6.685 -apply (simp add: divides_def)
   6.686 -apply (auto simp add: fun_eq poly_mult)
   6.687 -done
   6.688 -
   6.689 -lemma poly_divides_zero2: "q divides []"
   6.690 -apply (simp add: divides_def)
   6.691 -apply (rule_tac x = "[]" in exI)
   6.692 -apply (auto simp add: fun_eq)
   6.693 -done
   6.694 -declare poly_divides_zero2 [simp]
   6.695 -
   6.696 -text{*At last, we can consider the order of a root.*}
   6.697 -
   6.698 -
   6.699 -lemma poly_order_exists_lemma [rule_format]:
   6.700 -     "\<forall>p. length p = d --> poly p \<noteq> poly [] 
   6.701 -             --> (\<exists>n q. p = mulexp n [-a, 1] q & poly q a \<noteq> 0)"
   6.702 -apply (induct "d")
   6.703 -apply (simp add: fun_eq, safe)
   6.704 -apply (case_tac "poly p a = 0")
   6.705 -apply (drule_tac poly_linear_divides [THEN iffD1], safe)
   6.706 -apply (drule_tac x = q in spec)
   6.707 -apply (drule_tac poly_entire_neg [THEN iffD1], safe, force, blast) 
   6.708 -apply (rule_tac x = "Suc n" in exI)
   6.709 -apply (rule_tac x = qa in exI)
   6.710 -apply (simp del: pmult_Cons)
   6.711 -apply (rule_tac x = 0 in exI, force) 
   6.712 -done
   6.713 -
   6.714 -(* FIXME: Tidy up *)
   6.715 -lemma poly_order_exists:
   6.716 -     "[| length p = d; poly p \<noteq> poly [] |]
   6.717 -      ==> \<exists>n. ([-a, 1] %^ n) divides p &
   6.718 -                ~(([-a, 1] %^ (Suc n)) divides p)"
   6.719 -apply (drule poly_order_exists_lemma [where a=a], assumption, clarify)  
   6.720 -apply (rule_tac x = n in exI, safe)
   6.721 -apply (unfold divides_def)
   6.722 -apply (rule_tac x = q in exI)
   6.723 -apply (induct_tac "n", simp)
   6.724 -apply (simp (no_asm_simp) add: poly_add poly_cmult poly_mult right_distrib mult_ac)
   6.725 -apply safe
   6.726 -apply (subgoal_tac "poly (mulexp n [- a, 1] q) \<noteq> poly ([- a, 1] %^ Suc n *** qa)") 
   6.727 -apply simp 
   6.728 -apply (induct_tac "n")
   6.729 -apply (simp del: pmult_Cons pexp_Suc)
   6.730 -apply (erule_tac Q = "poly q a = 0" in contrapos_np)
   6.731 -apply (simp add: poly_add poly_cmult)
   6.732 -apply (rule pexp_Suc [THEN ssubst])
   6.733 -apply (rule ccontr)
   6.734 -apply (simp add: poly_mult_left_cancel poly_mult_assoc del: pmult_Cons pexp_Suc)
   6.735 -done
   6.736 -
   6.737 -lemma poly_one_divides: "[1] divides p"
   6.738 -by (simp add: divides_def, auto)
   6.739 -declare poly_one_divides [simp]
   6.740 -
   6.741 -lemma poly_order: "poly p \<noteq> poly []
   6.742 -      ==> EX! n. ([-a, 1] %^ n) divides p &
   6.743 -                 ~(([-a, 1] %^ (Suc n)) divides p)"
   6.744 -apply (auto intro: poly_order_exists simp add: less_linear simp del: pmult_Cons pexp_Suc)
   6.745 -apply (metis Suc_leI less_linear poly_exp_divides)
   6.746 -done
   6.747 -
   6.748 -text{*Order*}
   6.749 -
   6.750 -lemma some1_equalityD: "[| n = (@n. P n); EX! n. P n |] ==> P n"
   6.751 -by (blast intro: someI2)
   6.752 -
   6.753 -lemma order:
   6.754 -      "(([-a, 1] %^ n) divides p &
   6.755 -        ~(([-a, 1] %^ (Suc n)) divides p)) =
   6.756 -        ((n = order a p) & ~(poly p = poly []))"
   6.757 -apply (unfold order_def)
   6.758 -apply (rule iffI)
   6.759 -apply (blast dest: poly_divides_zero intro!: some1_equality [symmetric] poly_order)
   6.760 -apply (blast intro!: poly_order [THEN [2] some1_equalityD])
   6.761 -done
   6.762 -
   6.763 -lemma order2: "[| poly p \<noteq> poly [] |]
   6.764 -      ==> ([-a, 1] %^ (order a p)) divides p &
   6.765 -              ~(([-a, 1] %^ (Suc(order a p))) divides p)"
   6.766 -by (simp add: order del: pexp_Suc)
   6.767 -
   6.768 -lemma order_unique: "[| poly p \<noteq> poly []; ([-a, 1] %^ n) divides p;
   6.769 -         ~(([-a, 1] %^ (Suc n)) divides p)
   6.770 -      |] ==> (n = order a p)"
   6.771 -by (insert order [of a n p], auto) 
   6.772 -
   6.773 -lemma order_unique_lemma: "(poly p \<noteq> poly [] & ([-a, 1] %^ n) divides p &
   6.774 -         ~(([-a, 1] %^ (Suc n)) divides p))
   6.775 -      ==> (n = order a p)"
   6.776 -by (blast intro: order_unique)
   6.777 -
   6.778 -lemma order_poly: "poly p = poly q ==> order a p = order a q"
   6.779 -by (auto simp add: fun_eq divides_def poly_mult order_def)
   6.780 -
   6.781 -lemma pexp_one: "p %^ (Suc 0) = p"
   6.782 -apply (induct "p")
   6.783 -apply (auto simp add: numeral_1_eq_1)
   6.784 -done
   6.785 -declare pexp_one [simp]
   6.786 -
   6.787 -lemma lemma_order_root [rule_format]:
   6.788 -     "\<forall>p a. n > 0 & [- a, 1] %^ n divides p & ~ [- a, 1] %^ (Suc n) divides p
   6.789 -             --> poly p a = 0"
   6.790 -apply (induct "n", blast)
   6.791 -apply (auto simp add: divides_def poly_mult simp del: pmult_Cons)
   6.792 -done
   6.793 -
   6.794 -lemma order_root: "(poly p a = 0) = ((poly p = poly []) | order a p \<noteq> 0)"
   6.795 -apply (case_tac "poly p = poly []", auto)
   6.796 -apply (simp add: poly_linear_divides del: pmult_Cons, safe)
   6.797 -apply (drule_tac [!] a = a in order2)
   6.798 -apply (rule ccontr)
   6.799 -apply (simp add: divides_def poly_mult fun_eq del: pmult_Cons, blast)
   6.800 -apply (blast intro: lemma_order_root)
   6.801 -done
   6.802 -
   6.803 -lemma order_divides: "(([-a, 1] %^ n) divides p) = ((poly p = poly []) | n \<le> order a p)"
   6.804 -apply (case_tac "poly p = poly []", auto)
   6.805 -apply (simp add: divides_def fun_eq poly_mult)
   6.806 -apply (rule_tac x = "[]" in exI)
   6.807 -apply (auto dest!: order2 [where a=a]
   6.808 -	    intro: poly_exp_divides simp del: pexp_Suc)
   6.809 -done
   6.810 -
   6.811 -lemma order_decomp:
   6.812 -     "poly p \<noteq> poly []
   6.813 -      ==> \<exists>q. (poly p = poly (([-a, 1] %^ (order a p)) *** q)) &
   6.814 -                ~([-a, 1] divides q)"
   6.815 -apply (unfold divides_def)
   6.816 -apply (drule order2 [where a = a])
   6.817 -apply (simp add: divides_def del: pexp_Suc pmult_Cons, safe)
   6.818 -apply (rule_tac x = q in exI, safe)
   6.819 -apply (drule_tac x = qa in spec)
   6.820 -apply (auto simp add: poly_mult fun_eq poly_exp mult_ac simp del: pmult_Cons)
   6.821 -done
   6.822 -
   6.823 -text{*Important composition properties of orders.*}
   6.824 -
   6.825 -lemma order_mult: "poly (p *** q) \<noteq> poly []
   6.826 -      ==> order a (p *** q) = order a p + order a q"
   6.827 -apply (cut_tac a = a and p = "p***q" and n = "order a p + order a q" in order)
   6.828 -apply (auto simp add: poly_entire simp del: pmult_Cons)
   6.829 -apply (drule_tac a = a in order2)+
   6.830 -apply safe
   6.831 -apply (simp add: divides_def fun_eq poly_exp_add poly_mult del: pmult_Cons, safe)
   6.832 -apply (rule_tac x = "qa *** qaa" in exI)
   6.833 -apply (simp add: poly_mult mult_ac del: pmult_Cons)
   6.834 -apply (drule_tac a = a in order_decomp)+
   6.835 -apply safe
   6.836 -apply (subgoal_tac "[-a,1] divides (qa *** qaa) ")
   6.837 -apply (simp add: poly_primes del: pmult_Cons)
   6.838 -apply (auto simp add: divides_def simp del: pmult_Cons)
   6.839 -apply (rule_tac x = qb in exI)
   6.840 -apply (subgoal_tac "poly ([-a, 1] %^ (order a p) *** (qa *** qaa)) = poly ([-a, 1] %^ (order a p) *** ([-a, 1] *** qb))")
   6.841 -apply (drule poly_mult_left_cancel [THEN iffD1], force)
   6.842 -apply (subgoal_tac "poly ([-a, 1] %^ (order a q) *** ([-a, 1] %^ (order a p) *** (qa *** qaa))) = poly ([-a, 1] %^ (order a q) *** ([-a, 1] %^ (order a p) *** ([-a, 1] *** qb))) ")
   6.843 -apply (drule poly_mult_left_cancel [THEN iffD1], force)
   6.844 -apply (simp add: fun_eq poly_exp_add poly_mult mult_ac del: pmult_Cons)
   6.845 -done
   6.846 -
   6.847 -(* FIXME: too too long! *)
   6.848 -lemma lemma_order_pderiv [rule_format]:
   6.849 -     "\<forall>p q a. n > 0 &
   6.850 -       poly (pderiv p) \<noteq> poly [] &
   6.851 -       poly p = poly ([- a, 1] %^ n *** q) & ~ [- a, 1] divides q
   6.852 -       --> n = Suc (order a (pderiv p))"
   6.853 -apply (induct "n", safe)
   6.854 -apply (rule order_unique_lemma, rule conjI, assumption)
   6.855 -apply (subgoal_tac "\<forall>r. r divides (pderiv p) = r divides (pderiv ([-a, 1] %^ Suc n *** q))")
   6.856 -apply (drule_tac [2] poly_pderiv_welldef)
   6.857 - prefer 2 apply (simp add: divides_def del: pmult_Cons pexp_Suc) 
   6.858 -apply (simp del: pmult_Cons pexp_Suc) 
   6.859 -apply (rule conjI)
   6.860 -apply (simp add: divides_def fun_eq del: pmult_Cons pexp_Suc)
   6.861 -apply (rule_tac x = "[-a, 1] *** (pderiv q) +++ real (Suc n) %* q" in exI)
   6.862 -apply (simp add: poly_pderiv_mult poly_pderiv_exp_prime poly_add poly_mult poly_cmult right_distrib mult_ac del: pmult_Cons pexp_Suc)
   6.863 -apply (simp add: poly_mult right_distrib left_distrib mult_ac del: pmult_Cons)
   6.864 -apply (erule_tac V = "\<forall>r. r divides pderiv p = r divides pderiv ([- a, 1] %^ Suc n *** q)" in thin_rl)
   6.865 -apply (unfold divides_def)
   6.866 -apply (simp (no_asm) add: poly_pderiv_mult poly_pderiv_exp_prime fun_eq poly_add poly_mult del: pmult_Cons pexp_Suc)
   6.867 -apply (rule contrapos_np, assumption)
   6.868 -apply (rotate_tac 3, erule contrapos_np)
   6.869 -apply (simp del: pmult_Cons pexp_Suc, safe)
   6.870 -apply (rule_tac x = "inverse (real (Suc n)) %* (qa +++ -- (pderiv q))" in exI)
   6.871 -apply (subgoal_tac "poly ([-a, 1] %^ n *** q) = poly ([-a, 1] %^ n *** ([-a, 1] *** (inverse (real (Suc n)) %* (qa +++ -- (pderiv q))))) ")
   6.872 -apply (drule poly_mult_left_cancel [THEN iffD1], simp)
   6.873 -apply (simp add: fun_eq poly_mult poly_add poly_cmult poly_minus del: pmult_Cons mult_cancel_left, safe)
   6.874 -apply (rule_tac c1 = "real (Suc n)" in real_mult_left_cancel [THEN iffD1])
   6.875 -apply (simp (no_asm))
   6.876 -apply (subgoal_tac "real (Suc n) * (poly ([- a, 1] %^ n) xa * poly q xa) =
   6.877 -          (poly qa xa + - poly (pderiv q) xa) *
   6.878 -          (poly ([- a, 1] %^ n) xa *
   6.879 -           ((- a + xa) * (inverse (real (Suc n)) * real (Suc n))))")
   6.880 -apply (simp only: mult_ac)
   6.881 -apply (rotate_tac 2)
   6.882 -apply (drule_tac x = xa in spec)
   6.883 -apply (simp add: left_distrib mult_ac del: pmult_Cons)
   6.884 -done
   6.885 -
   6.886 -lemma order_pderiv: "[| poly (pderiv p) \<noteq> poly []; order a p \<noteq> 0 |]
   6.887 -      ==> (order a p = Suc (order a (pderiv p)))"
   6.888 -apply (case_tac "poly p = poly []")
   6.889 -apply (auto dest: pderiv_zero)
   6.890 -apply (drule_tac a = a and p = p in order_decomp)
   6.891 -apply (metis lemma_order_pderiv length_0_conv length_greater_0_conv)
   6.892 -done
   6.893 -
   6.894 -text{*Now justify the standard squarefree decomposition, i.e. f / gcd(f,f').    *)
   6.895 -(* `a la Harrison*}
   6.896 -
   6.897 -lemma poly_squarefree_decomp_order: "[| poly (pderiv p) \<noteq> poly [];
   6.898 -         poly p = poly (q *** d);
   6.899 -         poly (pderiv p) = poly (e *** d);
   6.900 -         poly d = poly (r *** p +++ s *** pderiv p)
   6.901 -      |] ==> order a q = (if order a p = 0 then 0 else 1)"
   6.902 -apply (subgoal_tac "order a p = order a q + order a d")
   6.903 -apply (rule_tac [2] s = "order a (q *** d)" in trans)
   6.904 -prefer 2 apply (blast intro: order_poly)
   6.905 -apply (rule_tac [2] order_mult)
   6.906 - prefer 2 apply force
   6.907 -apply (case_tac "order a p = 0", simp)
   6.908 -apply (subgoal_tac "order a (pderiv p) = order a e + order a d")
   6.909 -apply (rule_tac [2] s = "order a (e *** d)" in trans)
   6.910 -prefer 2 apply (blast intro: order_poly)
   6.911 -apply (rule_tac [2] order_mult)
   6.912 - prefer 2 apply force
   6.913 -apply (case_tac "poly p = poly []")
   6.914 -apply (drule_tac p = p in pderiv_zero, simp)
   6.915 -apply (drule order_pderiv, assumption)
   6.916 -apply (subgoal_tac "order a (pderiv p) \<le> order a d")
   6.917 -apply (subgoal_tac [2] " ([-a, 1] %^ (order a (pderiv p))) divides d")
   6.918 - prefer 2 apply (simp add: poly_entire order_divides)
   6.919 -apply (subgoal_tac [2] " ([-a, 1] %^ (order a (pderiv p))) divides p & ([-a, 1] %^ (order a (pderiv p))) divides (pderiv p) ")
   6.920 - prefer 3 apply (simp add: order_divides)
   6.921 - prefer 2 apply (simp add: divides_def del: pexp_Suc pmult_Cons, safe)
   6.922 -apply (rule_tac x = "r *** qa +++ s *** qaa" in exI)
   6.923 -apply (simp add: fun_eq poly_add poly_mult left_distrib right_distrib mult_ac del: pexp_Suc pmult_Cons, auto)
   6.924 -done
   6.925 -
   6.926 -
   6.927 -lemma poly_squarefree_decomp_order2: "[| poly (pderiv p) \<noteq> poly [];
   6.928 -         poly p = poly (q *** d);
   6.929 -         poly (pderiv p) = poly (e *** d);
   6.930 -         poly d = poly (r *** p +++ s *** pderiv p)
   6.931 -      |] ==> \<forall>a. order a q = (if order a p = 0 then 0 else 1)"
   6.932 -apply (blast intro: poly_squarefree_decomp_order)
   6.933 -done
   6.934 -
   6.935 -lemma order_root2: "poly p \<noteq> poly [] ==> (poly p a = 0) = (order a p \<noteq> 0)"
   6.936 -by (rule order_root [THEN ssubst], auto)
   6.937 -
   6.938 -lemma order_pderiv2: "[| poly (pderiv p) \<noteq> poly []; order a p \<noteq> 0 |]
   6.939 -      ==> (order a (pderiv p) = n) = (order a p = Suc n)"
   6.940 -by (metis Suc_Suc_eq order_pderiv)
   6.941 -
   6.942 -lemma rsquarefree_roots:
   6.943 -  "rsquarefree p = (\<forall>a. ~(poly p a = 0 & poly (pderiv p) a = 0))"
   6.944 -apply (simp add: rsquarefree_def)
   6.945 -apply (case_tac "poly p = poly []", simp, simp)
   6.946 -apply (case_tac "poly (pderiv p) = poly []")
   6.947 -apply simp
   6.948 -apply (drule pderiv_iszero, clarify)
   6.949 -apply (subgoal_tac "\<forall>a. order a p = order a [h]")
   6.950 -apply (simp add: fun_eq)
   6.951 -apply (rule allI)
   6.952 -apply (cut_tac p = "[h]" and a = a in order_root)
   6.953 -apply (simp add: fun_eq)
   6.954 -apply (blast intro: order_poly)
   6.955 -apply (metis One_nat_def order_pderiv2 order_root rsquarefree_def)
   6.956 -done
   6.957 -
   6.958 -lemma pmult_one: "[1] *** p = p"
   6.959 -by auto
   6.960 -declare pmult_one [simp]
   6.961 -
   6.962 -lemma poly_Nil_zero: "poly [] = poly [0]"
   6.963 -by (simp add: fun_eq)
   6.964 -
   6.965 -lemma rsquarefree_decomp:
   6.966 -     "[| rsquarefree p; poly p a = 0 |]
   6.967 -      ==> \<exists>q. (poly p = poly ([-a, 1] *** q)) & poly q a \<noteq> 0"
   6.968 -apply (simp add: rsquarefree_def, safe)
   6.969 -apply (frule_tac a = a in order_decomp)
   6.970 -apply (drule_tac x = a in spec)
   6.971 -apply (drule_tac a = a in order_root2 [symmetric])
   6.972 -apply (auto simp del: pmult_Cons)
   6.973 -apply (rule_tac x = q in exI, safe)
   6.974 -apply (simp add: poly_mult fun_eq)
   6.975 -apply (drule_tac p1 = q in poly_linear_divides [THEN iffD1])
   6.976 -apply (simp add: divides_def del: pmult_Cons, safe)
   6.977 -apply (drule_tac x = "[]" in spec)
   6.978 -apply (auto simp add: fun_eq)
   6.979 -done
   6.980 -
   6.981 -lemma poly_squarefree_decomp: "[| poly (pderiv p) \<noteq> poly [];
   6.982 -         poly p = poly (q *** d);
   6.983 -         poly (pderiv p) = poly (e *** d);
   6.984 -         poly d = poly (r *** p +++ s *** pderiv p)
   6.985 -      |] ==> rsquarefree q & (\<forall>a. (poly q a = 0) = (poly p a = 0))"
   6.986 -apply (frule poly_squarefree_decomp_order2, assumption+) 
   6.987 -apply (case_tac "poly p = poly []")
   6.988 -apply (blast dest: pderiv_zero)
   6.989 -apply (simp (no_asm) add: rsquarefree_def order_root del: pmult_Cons)
   6.990 -apply (simp add: poly_entire del: pmult_Cons)
   6.991 -done
   6.992 -
   6.993 -
   6.994 -text{*Normalization of a polynomial.*}
   6.995 -
   6.996 -lemma poly_normalize: "poly (pnormalize p) = poly p"
   6.997 -apply (induct "p")
   6.998 -apply (auto simp add: fun_eq)
   6.999 -done
  6.1000 -declare poly_normalize [simp]
  6.1001 -
  6.1002 -
  6.1003 -text{*The degree of a polynomial.*}
  6.1004 -
  6.1005 -lemma lemma_degree_zero:
  6.1006 -     "list_all (%c. c = 0) p \<longleftrightarrow>  pnormalize p = []"
  6.1007 -by (induct "p", auto)
  6.1008 -
  6.1009 -lemma degree_zero: "(poly p = poly []) \<Longrightarrow> (degree p = 0)"
  6.1010 -apply (simp add: degree_def)
  6.1011 -apply (case_tac "pnormalize p = []")
  6.1012 -apply (auto simp add: poly_zero lemma_degree_zero )
  6.1013 -done
  6.1014 -
  6.1015 -lemma pnormalize_sing: "(pnormalize [x] = [x]) \<longleftrightarrow> x \<noteq> 0" by simp
  6.1016 -lemma pnormalize_pair: "y \<noteq> 0 \<longleftrightarrow> (pnormalize [x, y] = [x, y])" by simp
  6.1017 -lemma pnormal_cons: "pnormal p \<Longrightarrow> pnormal (c#p)" 
  6.1018 -  unfolding pnormal_def by simp
  6.1019 -lemma pnormal_tail: "p\<noteq>[] \<Longrightarrow> pnormal (c#p) \<Longrightarrow> pnormal p"
  6.1020 -  unfolding pnormal_def 
  6.1021 -  apply (cases "pnormalize p = []", auto)
  6.1022 -  by (cases "c = 0", auto)
  6.1023 -lemma pnormal_last_nonzero: "pnormal p ==> last p \<noteq> 0"
  6.1024 -  apply (induct p, auto simp add: pnormal_def)
  6.1025 -  apply (case_tac "pnormalize p = []", auto)
  6.1026 -  by (case_tac "a=0", auto)
  6.1027 -lemma  pnormal_length: "pnormal p \<Longrightarrow> 0 < length p"
  6.1028 -  unfolding pnormal_def length_greater_0_conv by blast
  6.1029 -lemma pnormal_last_length: "\<lbrakk>0 < length p ; last p \<noteq> 0\<rbrakk> \<Longrightarrow> pnormal p"
  6.1030 -  apply (induct p, auto)
  6.1031 -  apply (case_tac "p = []", auto)
  6.1032 -  apply (simp add: pnormal_def)
  6.1033 -  by (rule pnormal_cons, auto)
  6.1034 -lemma pnormal_id: "pnormal p \<longleftrightarrow> (0 < length p \<and> last p \<noteq> 0)"
  6.1035 -  using pnormal_last_length pnormal_length pnormal_last_nonzero by blast
  6.1036 -
  6.1037 -text{*Tidier versions of finiteness of roots.*}
  6.1038 -
  6.1039 -lemma poly_roots_finite_set: "poly p \<noteq> poly [] ==> finite {x. poly p x = 0}"
  6.1040 -apply (auto simp add: poly_roots_finite)
  6.1041 -apply (rule_tac B = "{x::real. \<exists>n. (n::nat) < N & (x = j n) }" in finite_subset)
  6.1042 -apply (induct_tac [2] "N", auto)
  6.1043 -apply (subgoal_tac "{x::real. \<exists>na. na < Suc n & (x = j na) } = { (j n) } Un {x. \<exists>na. na < n & (x = j na) }") 
  6.1044 -apply (auto simp add: less_Suc_eq)
  6.1045 -done
  6.1046 -
  6.1047 -text{*bound for polynomial.*}
  6.1048 -
  6.1049 -lemma poly_mono: "abs(x) \<le> k ==> abs(poly p x) \<le> poly (map abs p) k"
  6.1050 -apply (induct "p", auto)
  6.1051 -apply (rule_tac j = "abs a + abs (x * poly p x)" in real_le_trans)
  6.1052 -apply (rule abs_triangle_ineq)
  6.1053 -apply (auto intro!: mult_mono simp add: abs_mult)
  6.1054 -done
  6.1055 -
  6.1056 -lemma poly_Sing: "poly [c] x = c" by simp
  6.1057 -end
     7.1 --- a/src/HOL/IsaMakefile	Thu Jun 26 10:06:54 2008 +0200
     7.2 +++ b/src/HOL/IsaMakefile	Thu Jun 26 10:07:01 2008 +0200
     7.3 @@ -6,7 +6,7 @@
     7.4  
     7.5  default: HOL
     7.6  generate: HOL-Complex-Generate-HOL HOL-Complex-Generate-HOLLight
     7.7 -images: HOL HOL-Algebra HOL-Complex HOL-Complex-Matrix HOL-Nominal \
     7.8 +images: HOL-Plain HOL HOL-Algebra HOL-Complex HOL-Complex-Matrix HOL-Nominal \
     7.9          HOL-Word TLA HOL4
    7.10  
    7.11  #Note: keep targets sorted (except for HOL-Library and HOL-ex)
    7.12 @@ -64,86 +64,180 @@
    7.13  
    7.14  ## HOL
    7.15  
    7.16 -HOL: Pure $(OUT)/HOL
    7.17 +HOL: HOL-Plain $(OUT)/HOL
    7.18 +
    7.19 +HOL-Plain: Pure $(OUT)/HOL-Plain
    7.20  
    7.21  Pure:
    7.22  	@cd $(SRC)/Pure; $(ISATOOL) make Pure
    7.23  
    7.24 -$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML		\
    7.25 -  $(SRC)/Provers/Arith/assoc_fold.ML					\
    7.26 -  $(SRC)/Provers/Arith/cancel_div_mod.ML				\
    7.27 -  $(SRC)/Provers/Arith/cancel_numeral_factor.ML				\
    7.28 -  $(SRC)/Provers/Arith/cancel_numerals.ML				\
    7.29 -  $(SRC)/Provers/Arith/cancel_sums.ML					\
    7.30 -  $(SRC)/Provers/Arith/combine_numerals.ML				\
    7.31 -  $(SRC)/Provers/Arith/extract_common_term.ML				\
    7.32 -  $(SRC)/Provers/Arith/fast_lin_arith.ML				\
    7.33 -  $(SRC)/Tools/IsaPlanner/isand.ML $(SRC)/Tools/IsaPlanner/rw_inst.ML	\
    7.34 -  $(SRC)/Tools/IsaPlanner/rw_tools.ML					\
    7.35 -  $(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Tools/induct.ML		\
    7.36 -  $(SRC)/Tools/induct_tacs.ML $(SRC)/Provers/blast.ML			\
    7.37 -  $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML			\
    7.38 -  $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML			\
    7.39 -  $(SRC)/Provers/order.ML $(SRC)/Provers/project_rule.ML		\
    7.40 -  $(SRC)/Provers/quantifier1.ML $(SRC)/Provers/quasi.ML			\
    7.41 -  $(SRC)/Provers/splitter.ML $(SRC)/Provers/trancl.ML			\
    7.42 -  $(SRC)/Tools/Metis/metis.ML $(SRC)/Tools/code/code_funcgr.ML		\
    7.43 -  $(SRC)/Tools/code/code_name.ML $(SRC)/Tools/code/code_target.ML	\
    7.44 -  $(SRC)/Tools/code/code_thingol.ML $(SRC)/Tools/nbe.ML			\
    7.45 -  $(SRC)/Tools/atomize_elim.ML $(SRC)/Tools/random_word.ML		\
    7.46 -  $(SRC)/Tools/rat.ML Tools/TFL/casesplit.ML ATP_Linkup.thy		\
    7.47 -  Arith_Tools.thy Code_Setup.thy Datatype.thy Divides.thy		\
    7.48 -  Equiv_Relations.thy Extraction.thy Finite_Set.thy Fun.thy FunDef.thy	\
    7.49 -  HOL.thy Hilbert_Choice.thy Inductive.thy Int.thy IntDiv.thy		\
    7.50 -  Lattices.thy List.thy Main.thy Map.thy Nat.thy NatBin.thy		\
    7.51 -  OrderedGroup.thy Orderings.thy Power.thy Predicate.thy		\
    7.52 -  Product_Type.thy ROOT.ML Recdef.thy Record.thy Refute.thy		\
    7.53 -  Relation.thy Relation_Power.thy Ring_and_Field.thy SAT.thy Set.thy	\
    7.54 -  SetInterval.thy Sum_Type.thy Groebner_Basis.thy Tools/watcher.ML	\
    7.55 -  Tools/Groebner_Basis/groebner.ML Tools/Groebner_Basis/misc.ML		\
    7.56 -  Tools/Groebner_Basis/normalizer.ML					\
    7.57 -  Tools/Groebner_Basis/normalizer_data.ML Tools/Qelim/cooper.ML		\
    7.58 -  Tools/Qelim/langford_data.ML Tools/Qelim/langford.ML			\
    7.59 -  Tools/Qelim/cooper_data.ML Tools/Qelim/ferrante_rackoff.ML		\
    7.60 -  Tools/Qelim/ferrante_rackoff_data.ML Tools/Qelim/generated_cooper.ML	\
    7.61 -  Tools/Qelim/presburger.ML Tools/Qelim/qelim.ML Tools/TFL/dcterm.ML	\
    7.62 -  Tools/TFL/post.ML Tools/TFL/rules.ML Tools/TFL/tfl.ML			\
    7.63 -  Tools/TFL/thms.ML Tools/TFL/thry.ML Tools/TFL/usyntax.ML		\
    7.64 -  Tools/TFL/utils.ML Tools/cnf_funcs.ML Tools/datatype_abs_proofs.ML	\
    7.65 -  Tools/datatype_aux.ML Tools/datatype_case.ML				\
    7.66 -  Tools/datatype_codegen.ML Tools/datatype_package.ML			\
    7.67 -  Tools/datatype_prop.ML Tools/datatype_realizer.ML			\
    7.68 -  Tools/datatype_rep_proofs.ML Tools/dseq.ML				\
    7.69 -  Tools/function_package/auto_term.ML					\
    7.70 -  Tools/function_package/context_tree.ML				\
    7.71 -  Tools/function_package/fundef_common.ML				\
    7.72 -  Tools/function_package/fundef_core.ML					\
    7.73 -  Tools/function_package/fundef_datatype.ML				\
    7.74 -  Tools/function_package/fundef_lib.ML					\
    7.75 -  Tools/function_package/fundef_package.ML				\
    7.76 -  Tools/function_package/inductive_wrap.ML				\
    7.77 -  Tools/function_package/lexicographic_order.ML				\
    7.78 -  Tools/function_package/measure_functions.ML				\
    7.79 -  Tools/function_package/mutual.ML					\
    7.80 -  Tools/function_package/pattern_split.ML				\
    7.81 -  Tools/function_package/size.ML Tools/inductive_codegen.ML		\
    7.82 -  Tools/inductive_package.ML Tools/inductive_realizer.ML		\
    7.83 -  Tools/inductive_set_package.ML Tools/lin_arith.ML Tools/meson.ML	\
    7.84 -  Tools/metis_tools.ML Tools/numeral.ML Tools/numeral_syntax.ML		\
    7.85 -  Tools/old_primrec_package.ML Tools/polyhash.ML			\
    7.86 -  Tools/primrec_package.ML Tools/prop_logic.ML Tools/recdef_package.ML	\
    7.87 -  Tools/recfun_codegen.ML Tools/record_package.ML Tools/refute.ML	\
    7.88 -  Tools/refute_isar.ML Tools/res_atp.ML Tools/res_atp_methods.ML	\
    7.89 -  Tools/res_atp_provers.ML Tools/res_axioms.ML Tools/res_clause.ML	\
    7.90 -  Tools/res_hol_clause.ML Tools/res_reconstruct.ML			\
    7.91 -  Tools/rewrite_hol_proof.ML Tools/sat_funcs.ML Tools/sat_solver.ML	\
    7.92 -  Tools/specification_package.ML Tools/split_rule.ML			\
    7.93 -  Tools/string_syntax.ML Tools/typecopy_package.ML			\
    7.94 -  Tools/typedef_codegen.ML Tools/typedef_package.ML			\
    7.95 -  Transitive_Closure.thy Typedef.thy Wellfounded.thy arith_data.ML	\
    7.96 -  document/root.tex hologic.ML int_arith1.ML int_factor_simprocs.ML	\
    7.97 -  nat_simprocs.ML simpdata.ML
    7.98 -	@$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL
    7.99 +$(OUT)/HOL-Plain: $(OUT)/Pure \
   7.100 +  plain.ML \
   7.101 +  Code_Setup.thy \
   7.102 +  Datatype.thy \
   7.103 +  Divides.thy \
   7.104 +  Extraction.thy \
   7.105 +  Finite_Set.thy \
   7.106 +  Fun.thy \
   7.107 +  FunDef.thy \
   7.108 +  HOL.thy \
   7.109 +  Inductive.thy \
   7.110 +  Lattices.thy \
   7.111 +  Nat.thy \
   7.112 +  OrderedGroup.thy \
   7.113 +  Orderings.thy \
   7.114 +  Plain.thy \
   7.115 +  Power.thy \
   7.116 +  Predicate.thy \
   7.117 +  Product_Type.thy \
   7.118 +  Record.thy \
   7.119 +  Refute.thy \
   7.120 +  Relation.thy \
   7.121 +  Ring_and_Field.thy \
   7.122 +  SAT.thy \
   7.123 +  Set.thy \
   7.124 +  Sum_Type.thy \
   7.125 +  Tools/cnf_funcs.ML \
   7.126 +  Tools/datatype_abs_proofs.ML \
   7.127 +  Tools/datatype_aux.ML \
   7.128 +  Tools/datatype_case.ML \
   7.129 +  Tools/datatype_codegen.ML \
   7.130 +  Tools/datatype_package.ML \
   7.131 +  Tools/datatype_prop.ML \
   7.132 +  Tools/datatype_realizer.ML \
   7.133 +  Tools/datatype_rep_proofs.ML \
   7.134 +  Tools/dseq.ML \
   7.135 +  Tools/function_package/auto_term.ML \
   7.136 +  Tools/function_package/context_tree.ML \
   7.137 +  Tools/function_package/fundef_common.ML \
   7.138 +  Tools/function_package/fundef_core.ML \
   7.139 +  Tools/function_package/fundef_datatype.ML \
   7.140 +  Tools/function_package/fundef_lib.ML \
   7.141 +  Tools/function_package/fundef_package.ML \
   7.142 +  Tools/function_package/induction_scheme.ML \
   7.143 +  Tools/function_package/inductive_wrap.ML \
   7.144 +  Tools/function_package/lexicographic_order.ML \
   7.145 +  Tools/function_package/measure_functions.ML \
   7.146 +  Tools/function_package/mutual.ML \
   7.147 +  Tools/function_package/pattern_split.ML \
   7.148 +  Tools/function_package/size.ML \
   7.149 +  Tools/function_package/sum_tree.ML \
   7.150 +  Tools/inductive_codegen.ML \
   7.151 +  Tools/inductive_package.ML \
   7.152 +  Tools/inductive_realizer.ML \
   7.153 +  Tools/inductive_set_package.ML \
   7.154 +  Tools/lin_arith.ML \
   7.155 +  Tools/old_primrec_package.ML \
   7.156 +  Tools/primrec_package.ML \
   7.157 +  Tools/prop_logic.ML \
   7.158 +  Tools/recfun_codegen.ML \
   7.159 +  Tools/record_package.ML \
   7.160 +  Tools/refute.ML \
   7.161 +  Tools/refute_isar.ML \
   7.162 +  Tools/rewrite_hol_proof.ML \
   7.163 +  Tools/sat_funcs.ML \
   7.164 +  Tools/sat_solver.ML \
   7.165 +  Tools/split_rule.ML \
   7.166 +  Tools/typecopy_package.ML \
   7.167 +  Tools/typedef_codegen.ML \
   7.168 +  Tools/typedef_package.ML \
   7.169 +  Transitive_Closure.thy \
   7.170 +  Typedef.thy \
   7.171 +  Wellfounded.thy \
   7.172 +  arith_data.ML \
   7.173 +  hologic.ML \
   7.174 +  simpdata.ML \
   7.175 +  $(SRC)/Provers/Arith/abel_cancel.ML \
   7.176 +  $(SRC)/Provers/Arith/cancel_div_mod.ML \
   7.177 +  $(SRC)/Provers/Arith/cancel_sums.ML \
   7.178 +  $(SRC)/Provers/Arith/fast_lin_arith.ML \
   7.179 +  $(SRC)/Provers/blast.ML \
   7.180 +  $(SRC)/Provers/clasimp.ML \
   7.181 +  $(SRC)/Provers/classical.ML \
   7.182 +  $(SRC)/Provers/eqsubst.ML \
   7.183 +  $(SRC)/Provers/hypsubst.ML \
   7.184 +  $(SRC)/Provers/order.ML \
   7.185 +  $(SRC)/Provers/project_rule.ML \
   7.186 +  $(SRC)/Provers/quantifier1.ML \
   7.187 +  $(SRC)/Provers/splitter.ML \
   7.188 +  $(SRC)/Provers/trancl.ML \
   7.189 +  $(SRC)/Tools/IsaPlanner/isand.ML \
   7.190 +  $(SRC)/Tools/IsaPlanner/rw_inst.ML \
   7.191 +  $(SRC)/Tools/IsaPlanner/rw_tools.ML \
   7.192 +  $(SRC)/Tools/IsaPlanner/zipper.ML \
   7.193 +  $(SRC)/Tools/atomize_elim.ML \
   7.194 +  $(SRC)/Tools/code/code_funcgr.ML \
   7.195 +  $(SRC)/Tools/code/code_name.ML \
   7.196 +  $(SRC)/Tools/code/code_target.ML \
   7.197 +  $(SRC)/Tools/code/code_thingol.ML \
   7.198 +  $(SRC)/Tools/induct.ML \
   7.199 +  $(SRC)/Tools/induct_tacs.ML \
   7.200 +  $(SRC)/Tools/nbe.ML \
   7.201 +  $(SRC)/Tools/random_word.ML \
   7.202 +  $(SRC)/Tools/rat.ML
   7.203 +	@$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -f plain.ML -g true $(OUT)/Pure HOL-Plain
   7.204 +
   7.205 +$(OUT)/HOL: $(OUT)/HOL-Plain \
   7.206 +  ROOT.ML \
   7.207 +  ATP_Linkup.thy \
   7.208 +  Arith_Tools.thy \
   7.209 +  Equiv_Relations.thy \
   7.210 +  Groebner_Basis.thy \
   7.211 +  Hilbert_Choice.thy \
   7.212 +  Int.thy \
   7.213 +  IntDiv.thy \
   7.214 +  List.thy \
   7.215 +  Main.thy \
   7.216 +  Map.thy \
   7.217 +  NatBin.thy \
   7.218 +  Presburger.thy \
   7.219 +  Recdef.thy \
   7.220 +  Relation_Power.thy \
   7.221 +  SetInterval.thy \
   7.222 +  Tools/Groebner_Basis/groebner.ML \
   7.223 +  Tools/Groebner_Basis/misc.ML \
   7.224 +  Tools/Groebner_Basis/normalizer.ML \
   7.225 +  Tools/Groebner_Basis/normalizer_data.ML \
   7.226 +  Tools/Qelim/cooper.ML \
   7.227 +  Tools/Qelim/cooper_data.ML \
   7.228 +  Tools/Qelim/generated_cooper.ML \
   7.229 +  Tools/Qelim/presburger.ML \
   7.230 +  Tools/Qelim/qelim.ML \
   7.231 +  Tools/TFL/casesplit.ML \
   7.232 +  Tools/TFL/dcterm.ML \
   7.233 +  Tools/TFL/post.ML \
   7.234 +  Tools/TFL/rules.ML \
   7.235 +  Tools/TFL/tfl.ML \
   7.236 +  Tools/TFL/thms.ML \
   7.237 +  Tools/TFL/thry.ML \
   7.238 +  Tools/TFL/usyntax.ML \
   7.239 +  Tools/TFL/utils.ML \
   7.240 +  Tools/meson.ML \
   7.241 +  Tools/metis_tools.ML \
   7.242 +  Tools/numeral.ML \
   7.243 +  Tools/numeral_syntax.ML \
   7.244 +  Tools/polyhash.ML \
   7.245 +  Tools/recdef_package.ML \
   7.246 +  Tools/res_atp.ML \
   7.247 +  Tools/res_atp_methods.ML \
   7.248 +  Tools/res_atp_provers.ML \
   7.249 +  Tools/res_axioms.ML \
   7.250 +  Tools/res_clause.ML \
   7.251 +  Tools/res_hol_clause.ML \
   7.252 +  Tools/res_reconstruct.ML \
   7.253 +  Tools/specification_package.ML \
   7.254 +  Tools/string_syntax.ML \
   7.255 +  Tools/watcher.ML \
   7.256 +  int_arith1.ML \
   7.257 +  int_factor_simprocs.ML \
   7.258 +  nat_simprocs.ML \
   7.259 +  $(SRC)/Provers/Arith/assoc_fold.ML \
   7.260 +  $(SRC)/Provers/Arith/cancel_numeral_factor.ML \
   7.261 +  $(SRC)/Provers/Arith/cancel_numerals.ML \
   7.262 +  $(SRC)/Provers/Arith/combine_numerals.ML \
   7.263 +  $(SRC)/Provers/Arith/extract_common_term.ML \
   7.264 +  $(SRC)/Tools/Metis/metis.ML
   7.265 +	@$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/HOL-Plain HOL
   7.266  
   7.267  
   7.268  ## HOL-Complex-HahnBanach
   7.269 @@ -167,27 +261,66 @@
   7.270  
   7.271  HOL-Complex: HOL $(OUT)/HOL-Complex
   7.272  
   7.273 -$(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML                          \
   7.274 -  Library/Zorn.thy Library/Order_Relation.thy Real/ContNotDenum.thy	\
   7.275 -  Real/float_arith.ML Real/Lubs.thy Real/PReal.thy                      \
   7.276 -  Real/RComplete.thy Real/Rational.thy Real/Real.thy Real/RealDef.thy	\
   7.277 -  Real/RealPow.thy Real/RealVector.thy Real/rat_arith.ML		\
   7.278 -  Real/real_arith.ML Hyperreal/StarDef.thy Hyperreal/Fact.thy		\
   7.279 -  Hyperreal/HLog.thy Hyperreal/Filter.thy Hyperreal/HSeries.thy		\
   7.280 -  Hyperreal/transfer.ML Hyperreal/HLim.thy Hyperreal/HSEQ.thy		\
   7.281 -  Hyperreal/HTranscendental.thy Hyperreal/HDeriv.thy			\
   7.282 -  Hyperreal/HyperDef.thy Hyperreal/HyperNat.thy				\
   7.283 -  Hyperreal/Hyperreal.thy Hyperreal/Integration.thy Hyperreal/Lim.thy	\
   7.284 -  Hyperreal/Log.thy Hyperreal/Ln.thy Hyperreal/MacLaurin.thy		\
   7.285 -  Hyperreal/NatStar.thy Hyperreal/NSA.thy Hyperreal/NthRoot.thy		\
   7.286 -  Library/Univ_Poly.thy Hyperreal/SEQ.thy Hyperreal/Series.thy		\
   7.287 -  Hyperreal/Star.thy Hyperreal/Taylor.thy Hyperreal/FrechetDeriv.thy	\
   7.288 -  Hyperreal/Deriv.thy Hyperreal/Transcendental.thy			\
   7.289 -  Hyperreal/hypreal_arith.ML Complex/Complex_Main.thy			\
   7.290 -  Complex/Fundamental_Theorem_Algebra.thy Complex/CLim.thy		\
   7.291 -  Complex/CStar.thy Complex/Complex.thy Complex/NSCA.thy		\
   7.292 -  Complex/NSComplex.thy Complex/document/root.tex			\
   7.293 -  Library/Infinite_Set.thy Library/Parity.thy
   7.294 +$(OUT)/HOL-Complex: $(OUT)/HOL \
   7.295 +  Complex/ROOT.ML \
   7.296 +  Complex/CLim.thy \
   7.297 +  Complex/CStar.thy \
   7.298 +  Complex/Complex.thy \
   7.299 +  Complex/Complex_Main.thy \
   7.300 +  Complex/Fundamental_Theorem_Algebra.thy \
   7.301 +  Complex/NSCA.thy \
   7.302 +  Complex/NSComplex.thy \
   7.303 +  Hyperreal/Deriv.thy \
   7.304 +  Hyperreal/Fact.thy \
   7.305 +  Hyperreal/Filter.thy \
   7.306 +  Hyperreal/HDeriv.thy \
   7.307 +  Hyperreal/HLim.thy \
   7.308 +  Hyperreal/HLog.thy \
   7.309 +  Hyperreal/HSEQ.thy \
   7.310 +  Hyperreal/HSeries.thy \
   7.311 +  Hyperreal/HTranscendental.thy \
   7.312 +  Hyperreal/HyperDef.thy \
   7.313 +  Hyperreal/HyperNat.thy \
   7.314 +  Hyperreal/Hyperreal.thy \
   7.315 +  Hyperreal/Integration.thy \
   7.316 +  Hyperreal/Lim.thy \
   7.317 +  Hyperreal/Ln.thy \
   7.318 +  Hyperreal/Log.thy \
   7.319 +  Hyperreal/MacLaurin.thy \
   7.320 +  Hyperreal/NSA.thy \
   7.321 +  Hyperreal/NatStar.thy \
   7.322 +  Hyperreal/NthRoot.thy \
   7.323 +  Hyperreal/SEQ.thy \
   7.324 +  Hyperreal/Series.thy \
   7.325 +  Hyperreal/Star.thy \
   7.326 +  Hyperreal/StarDef.thy \
   7.327 +  Hyperreal/Taylor.thy \
   7.328 +  Hyperreal/Transcendental.thy \
   7.329 +  Hyperreal/hypreal_arith.ML \
   7.330 +  Hyperreal/transfer.ML \
   7.331 +  Library/Abstract_Rat.thy \
   7.332 +  Library/Dense_Linear_Order.thy \
   7.333 +  Library/GCD.thy \
   7.334 +  Library/Infinite_Set.thy \
   7.335 +  Library/Order_Relation.thy \
   7.336 +  Library/Parity.thy \
   7.337 +  Library/Univ_Poly.thy \
   7.338 +  Library/Zorn.thy \
   7.339 +  Real/ContNotDenum.thy \
   7.340 +  Real/Lubs.thy \
   7.341 +  Real/PReal.thy \
   7.342 +  Real/RComplete.thy \
   7.343 +  Real/Rational.thy \
   7.344 +  Real/Real.thy \
   7.345 +  Real/RealDef.thy \
   7.346 +  Real/RealPow.thy \
   7.347 +  Real/RealVector.thy \
   7.348 +  Real/rat_arith.ML \
   7.349 +  Real/real_arith.ML \
   7.350 +  Tools/Qelim/ferrante_rackoff.ML \
   7.351 +  Tools/Qelim/ferrante_rackoff_data.ML \
   7.352 +  Tools/Qelim/langford.ML \
   7.353 +  Tools/Qelim/langford_data.ML
   7.354  	@cd Complex; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Complex
   7.355  
   7.356  
   7.357 @@ -211,26 +344,26 @@
   7.358  
   7.359  $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/SetsAndFunctions.thy		\
   7.360    Library/BigO.thy Library/Ramsey.thy Library/Efficient_Nat.thy		\
   7.361 -  Library/Executable_Set.thy Library/Infinite_Set.thy			\
   7.362 -  Library/Dense_Linear_Order.thy Library/FuncSet.thy			\
   7.363 +  Library/Executable_Set.thy 			\
   7.364 +  Library/FuncSet.thy			\
   7.365    Library/Library.thy Library/List_Prefix.thy Library/State_Monad.thy	\
   7.366    Library/Multiset.thy Library/NatPair.thy Library/Permutation.thy	\
   7.367    Library/Primes.thy Library/Pocklington.thy Library/Quotient.thy	\
   7.368    Library/Quicksort.thy Library/Nat_Infinity.thy Library/Word.thy	\
   7.369    Library/README.html Library/Continuity.thy				\
   7.370 -  Library/Nested_Environment.thy Library/Zorn.thy			\
   7.371 +  Library/Nested_Environment.thy			\
   7.372    Library/Library/ROOT.ML Library/Library/document/root.tex		\
   7.373    Library/Library/document/root.bib Library/While_Combinator.thy	\
   7.374    Library/Product_ord.thy Library/Char_nat.thy Library/Char_ord.thy	\
   7.375    Library/Option_ord.thy Library/Sublist_Order.thy			\
   7.376    Library/List_lexord.thy Library/Commutative_Ring.thy			\
   7.377    Library/comm_ring.ML Library/Coinductive_List.thy			\
   7.378 -  Library/AssocList.thy Library/Parity.thy Library/GCD.thy		\
   7.379 +  Library/AssocList.thy		\
   7.380    Library/Binomial.thy Library/Eval.thy Library/Eval_Witness.thy	\
   7.381    Library/Code_Index.thy Library/Code_Char.thy				\
   7.382    Library/Code_Char_chr.thy Library/Code_Integer.thy			\
   7.383 -  Library/Code_Message.thy Library/Abstract_Rat.thy			\
   7.384 -  Library/Univ_Poly.thy Library/Numeral_Type.thy			\
   7.385 +  Library/Code_Message.thy			\
   7.386 +  Library/Numeral_Type.thy			\
   7.387    Library/Boolean_Algebra.thy Library/Countable.thy Library/RType.thy	\
   7.388    Library/Heap.thy Library/Heap_Monad.thy Library/Array.thy		\
   7.389    Library/Ref.thy Library/Imperative_HOL.thy Library/RBT.thy		\
     8.1 --- a/src/HOL/Library/Abstract_Rat.thy	Thu Jun 26 10:06:54 2008 +0200
     8.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Thu Jun 26 10:07:01 2008 +0200
     8.3 @@ -6,7 +6,7 @@
     8.4  header {* Abstract rational numbers *}
     8.5  
     8.6  theory Abstract_Rat
     8.7 -imports GCD
     8.8 +imports Plain GCD
     8.9  begin
    8.10  
    8.11  types Num = "int \<times> int"
     9.1 --- a/src/HOL/Library/AssocList.thy	Thu Jun 26 10:06:54 2008 +0200
     9.2 +++ b/src/HOL/Library/AssocList.thy	Thu Jun 26 10:07:01 2008 +0200
     9.3 @@ -6,7 +6,7 @@
     9.4  header {* Map operations implemented on association lists*}
     9.5  
     9.6  theory AssocList 
     9.7 -imports Map
     9.8 +imports Plain Map
     9.9  begin
    9.10  
    9.11  text {*
    10.1 --- a/src/HOL/Library/BigO.thy	Thu Jun 26 10:06:54 2008 +0200
    10.2 +++ b/src/HOL/Library/BigO.thy	Thu Jun 26 10:07:01 2008 +0200
    10.3 @@ -6,7 +6,7 @@
    10.4  header {* Big O notation *}
    10.5  
    10.6  theory BigO
    10.7 -imports Main SetsAndFunctions
    10.8 +imports Plain Presburger SetsAndFunctions
    10.9  begin
   10.10  
   10.11  text {*
    11.1 --- a/src/HOL/Library/Binomial.thy	Thu Jun 26 10:06:54 2008 +0200
    11.2 +++ b/src/HOL/Library/Binomial.thy	Thu Jun 26 10:07:01 2008 +0200
    11.3 @@ -7,7 +7,7 @@
    11.4  header {* Binomial Coefficients *}
    11.5  
    11.6  theory Binomial
    11.7 -imports ATP_Linkup
    11.8 +imports Plain SetInterval
    11.9  begin
   11.10  
   11.11  text {* This development is based on the work of Andy Gordon and
    12.1 --- a/src/HOL/Library/Boolean_Algebra.thy	Thu Jun 26 10:06:54 2008 +0200
    12.2 +++ b/src/HOL/Library/Boolean_Algebra.thy	Thu Jun 26 10:07:01 2008 +0200
    12.3 @@ -8,7 +8,7 @@
    12.4  header {* Boolean Algebras *}
    12.5  
    12.6  theory Boolean_Algebra
    12.7 -imports ATP_Linkup
    12.8 +imports Plain
    12.9  begin
   12.10  
   12.11  locale boolean =
    13.1 --- a/src/HOL/Library/Char_nat.thy	Thu Jun 26 10:06:54 2008 +0200
    13.2 +++ b/src/HOL/Library/Char_nat.thy	Thu Jun 26 10:07:01 2008 +0200
    13.3 @@ -6,7 +6,7 @@
    13.4  header {* Mapping between characters and natural numbers *}
    13.5  
    13.6  theory Char_nat
    13.7 -imports List
    13.8 +imports Plain List
    13.9  begin
   13.10  
   13.11  text {* Conversions between nibbles and natural numbers in [0..15]. *}
    14.1 --- a/src/HOL/Library/Char_ord.thy	Thu Jun 26 10:06:54 2008 +0200
    14.2 +++ b/src/HOL/Library/Char_ord.thy	Thu Jun 26 10:07:01 2008 +0200
    14.3 @@ -6,7 +6,7 @@
    14.4  header {* Order on characters *}
    14.5  
    14.6  theory Char_ord
    14.7 -imports Product_ord Char_nat
    14.8 +imports Plain Product_ord Char_nat
    14.9  begin
   14.10  
   14.11  instantiation nibble :: linorder
    15.1 --- a/src/HOL/Library/Code_Char.thy	Thu Jun 26 10:06:54 2008 +0200
    15.2 +++ b/src/HOL/Library/Code_Char.thy	Thu Jun 26 10:07:01 2008 +0200
    15.3 @@ -6,7 +6,7 @@
    15.4  header {* Code generation of pretty characters (and strings) *}
    15.5  
    15.6  theory Code_Char
    15.7 -imports List
    15.8 +imports Plain List
    15.9  begin
   15.10  
   15.11  declare char.recs [code func del] char.cases [code func del]
    16.1 --- a/src/HOL/Library/Code_Char_chr.thy	Thu Jun 26 10:06:54 2008 +0200
    16.2 +++ b/src/HOL/Library/Code_Char_chr.thy	Thu Jun 26 10:07:01 2008 +0200
    16.3 @@ -6,7 +6,7 @@
    16.4  header {* Code generation of pretty characters with character codes *}
    16.5  
    16.6  theory Code_Char_chr
    16.7 -imports Char_nat Code_Char Code_Integer
    16.8 +imports Plain Char_nat Code_Char Code_Integer
    16.9  begin
   16.10  
   16.11  definition
    17.1 --- a/src/HOL/Library/Code_Index.thy	Thu Jun 26 10:06:54 2008 +0200
    17.2 +++ b/src/HOL/Library/Code_Index.thy	Thu Jun 26 10:07:01 2008 +0200
    17.3 @@ -5,7 +5,7 @@
    17.4  header {* Type of indices *}
    17.5  
    17.6  theory Code_Index
    17.7 -imports ATP_Linkup
    17.8 +imports Plain Presburger
    17.9  begin
   17.10  
   17.11  text {*
    18.1 --- a/src/HOL/Library/Code_Integer.thy	Thu Jun 26 10:06:54 2008 +0200
    18.2 +++ b/src/HOL/Library/Code_Integer.thy	Thu Jun 26 10:07:01 2008 +0200
    18.3 @@ -6,7 +6,7 @@
    18.4  header {* Pretty integer literals for code generation *}
    18.5  
    18.6  theory Code_Integer
    18.7 -imports ATP_Linkup
    18.8 +imports Plain Presburger
    18.9  begin
   18.10  
   18.11  text {*
    19.1 --- a/src/HOL/Library/Code_Message.thy	Thu Jun 26 10:06:54 2008 +0200
    19.2 +++ b/src/HOL/Library/Code_Message.thy	Thu Jun 26 10:07:01 2008 +0200
    19.3 @@ -5,7 +5,7 @@
    19.4  header {* Monolithic strings (message strings) for code generation *}
    19.5  
    19.6  theory Code_Message
    19.7 -imports List
    19.8 +imports Plain List
    19.9  begin
   19.10  
   19.11  subsection {* Datatype of messages *}
    20.1 --- a/src/HOL/Library/Coinductive_List.thy	Thu Jun 26 10:06:54 2008 +0200
    20.2 +++ b/src/HOL/Library/Coinductive_List.thy	Thu Jun 26 10:07:01 2008 +0200
    20.3 @@ -6,7 +6,7 @@
    20.4  header {* Potentially infinite lists as greatest fixed-point *}
    20.5  
    20.6  theory Coinductive_List
    20.7 -imports List
    20.8 +imports Plain List
    20.9  begin
   20.10  
   20.11  subsection {* List constructors over the datatype universe *}
    21.1 --- a/src/HOL/Library/Commutative_Ring.thy	Thu Jun 26 10:06:54 2008 +0200
    21.2 +++ b/src/HOL/Library/Commutative_Ring.thy	Thu Jun 26 10:07:01 2008 +0200
    21.3 @@ -7,7 +7,7 @@
    21.4  header {* Proving equalities in commutative rings *}
    21.5  
    21.6  theory Commutative_Ring
    21.7 -imports List Parity
    21.8 +imports Plain List Parity
    21.9  uses ("comm_ring.ML")
   21.10  begin
   21.11  
    22.1 --- a/src/HOL/Library/Continuity.thy	Thu Jun 26 10:06:54 2008 +0200
    22.2 +++ b/src/HOL/Library/Continuity.thy	Thu Jun 26 10:07:01 2008 +0200
    22.3 @@ -6,7 +6,7 @@
    22.4  header {* Continuity and iterations (of set transformers) *}
    22.5  
    22.6  theory Continuity
    22.7 -imports ATP_Linkup
    22.8 +imports Plain Relation_Power
    22.9  begin
   22.10  
   22.11  subsection {* Continuity for complete lattices *}
    23.1 --- a/src/HOL/Library/Countable.thy	Thu Jun 26 10:06:54 2008 +0200
    23.2 +++ b/src/HOL/Library/Countable.thy	Thu Jun 26 10:07:01 2008 +0200
    23.3 @@ -6,7 +6,7 @@
    23.4  header {* Encoding (almost) everything into natural numbers *}
    23.5  
    23.6  theory Countable
    23.7 -imports Finite_Set List Hilbert_Choice
    23.8 +imports Plain List Hilbert_Choice
    23.9  begin
   23.10  
   23.11  subsection {* The class of countable types *}
    24.1 --- a/src/HOL/Library/Dense_Linear_Order.thy	Thu Jun 26 10:06:54 2008 +0200
    24.2 +++ b/src/HOL/Library/Dense_Linear_Order.thy	Thu Jun 26 10:07:01 2008 +0200
    24.3 @@ -7,7 +7,7 @@
    24.4    and a quantifier elimination procedure in Ferrante and Rackoff style *}
    24.5  
    24.6  theory Dense_Linear_Order
    24.7 -imports Arith_Tools
    24.8 +imports Plain Presburger
    24.9  uses
   24.10    "~~/src/HOL/Tools/Qelim/qelim.ML"
   24.11    "~~/src/HOL/Tools/Qelim/langford_data.ML"
    25.1 --- a/src/HOL/Library/Efficient_Nat.thy	Thu Jun 26 10:06:54 2008 +0200
    25.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Thu Jun 26 10:07:01 2008 +0200
    25.3 @@ -6,7 +6,7 @@
    25.4  header {* Implementation of natural numbers by target-language integers *}
    25.5  
    25.6  theory Efficient_Nat
    25.7 -imports Code_Integer Code_Index
    25.8 +imports Plain Code_Integer Code_Index
    25.9  begin
   25.10  
   25.11  text {*
    26.1 --- a/src/HOL/Library/Enum.thy	Thu Jun 26 10:06:54 2008 +0200
    26.2 +++ b/src/HOL/Library/Enum.thy	Thu Jun 26 10:07:01 2008 +0200
    26.3 @@ -6,7 +6,7 @@
    26.4  header {* Finite types as explicit enumerations *}
    26.5  
    26.6  theory Enum
    26.7 -imports Main
    26.8 +imports Plain Map
    26.9  begin
   26.10  
   26.11  subsection {* Class @{text enum} *}
    27.1 --- a/src/HOL/Library/Eval.thy	Thu Jun 26 10:06:54 2008 +0200
    27.2 +++ b/src/HOL/Library/Eval.thy	Thu Jun 26 10:07:01 2008 +0200
    27.3 @@ -7,6 +7,7 @@
    27.4  
    27.5  theory Eval
    27.6  imports
    27.7 +  Plain
    27.8    RType
    27.9    Code_Index (* this theory is just imported for a term_of setup *)
   27.10  begin
    28.1 --- a/src/HOL/Library/Eval_Witness.thy	Thu Jun 26 10:06:54 2008 +0200
    28.2 +++ b/src/HOL/Library/Eval_Witness.thy	Thu Jun 26 10:07:01 2008 +0200
    28.3 @@ -7,7 +7,7 @@
    28.4  header {* Evaluation Oracle with ML witnesses *}
    28.5  
    28.6  theory Eval_Witness
    28.7 -imports List
    28.8 +imports Plain List
    28.9  begin
   28.10  
   28.11  text {* 
    29.1 --- a/src/HOL/Library/Executable_Set.thy	Thu Jun 26 10:06:54 2008 +0200
    29.2 +++ b/src/HOL/Library/Executable_Set.thy	Thu Jun 26 10:07:01 2008 +0200
    29.3 @@ -6,7 +6,7 @@
    29.4  header {* Implementation of finite sets by lists *}
    29.5  
    29.6  theory Executable_Set
    29.7 -imports List
    29.8 +imports Plain List
    29.9  begin
   29.10  
   29.11  subsection {* Definitional rewrites *}
    30.1 --- a/src/HOL/Library/FuncSet.thy	Thu Jun 26 10:06:54 2008 +0200
    30.2 +++ b/src/HOL/Library/FuncSet.thy	Thu Jun 26 10:07:01 2008 +0200
    30.3 @@ -6,7 +6,7 @@
    30.4  header {* Pi and Function Sets *}
    30.5  
    30.6  theory FuncSet
    30.7 -imports Main
    30.8 +imports Plain Hilbert_Choice
    30.9  begin
   30.10  
   30.11  definition
    31.1 --- a/src/HOL/Library/GCD.thy	Thu Jun 26 10:06:54 2008 +0200
    31.2 +++ b/src/HOL/Library/GCD.thy	Thu Jun 26 10:07:01 2008 +0200
    31.3 @@ -7,7 +7,7 @@
    31.4  header {* The Greatest Common Divisor *}
    31.5  
    31.6  theory GCD
    31.7 -imports ATP_Linkup
    31.8 +imports Plain Presburger
    31.9  begin
   31.10  
   31.11  text {*
    32.1 --- a/src/HOL/Library/Heap.thy	Thu Jun 26 10:06:54 2008 +0200
    32.2 +++ b/src/HOL/Library/Heap.thy	Thu Jun 26 10:07:01 2008 +0200
    32.3 @@ -6,7 +6,7 @@
    32.4  header {* A polymorphic heap based on cantor encodings *}
    32.5  
    32.6  theory Heap
    32.7 -imports Main Countable RType
    32.8 +imports Plain List Countable RType
    32.9  begin
   32.10  
   32.11  subsection {* Representable types *}
    33.1 --- a/src/HOL/Library/Infinite_Set.thy	Thu Jun 26 10:06:54 2008 +0200
    33.2 +++ b/src/HOL/Library/Infinite_Set.thy	Thu Jun 26 10:07:01 2008 +0200
    33.3 @@ -6,9 +6,10 @@
    33.4  header {* Infinite Sets and Related Concepts *}
    33.5  
    33.6  theory Infinite_Set
    33.7 -imports ATP_Linkup
    33.8 +imports Plain SetInterval Hilbert_Choice
    33.9  begin
   33.10  
   33.11 +
   33.12  subsection "Infinite Sets"
   33.13  
   33.14  text {*
    34.1 --- a/src/HOL/Library/LaTeXsugar.thy	Thu Jun 26 10:06:54 2008 +0200
    34.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Thu Jun 26 10:07:01 2008 +0200
    34.3 @@ -6,7 +6,7 @@
    34.4  
    34.5  (*<*)
    34.6  theory LaTeXsugar
    34.7 -imports List
    34.8 +imports Plain List
    34.9  begin
   34.10  
   34.11  (* LOGIC *)
    35.1 --- a/src/HOL/Library/Library.thy	Thu Jun 26 10:06:54 2008 +0200
    35.2 +++ b/src/HOL/Library/Library.thy	Thu Jun 26 10:07:01 2008 +0200
    35.3 @@ -2,7 +2,6 @@
    35.4  (*<*)
    35.5  theory Library
    35.6  imports
    35.7 -  Abstract_Rat
    35.8    AssocList
    35.9    BigO
   35.10    Binomial
   35.11 @@ -24,9 +23,7 @@
   35.12    Executable_Set
   35.13    "../Real/Float"
   35.14    FuncSet
   35.15 -  GCD
   35.16    Imperative_HOL
   35.17 -  Infinite_Set
   35.18    ListVector
   35.19    Multiset
   35.20    NatPair
   35.21 @@ -35,8 +32,6 @@
   35.22    Numeral_Type
   35.23    OptionalSugar
   35.24    Option_ord
   35.25 -  Order_Relation
   35.26 -  Parity
   35.27    Permutation
   35.28    Primes
   35.29    Quicksort
   35.30 @@ -44,10 +39,8 @@
   35.31    Ramsey
   35.32    RBT
   35.33    State_Monad
   35.34 -  Univ_Poly
   35.35    While_Combinator
   35.36    Word
   35.37 -  Zorn
   35.38  begin
   35.39  end
   35.40  (*>*)
    36.1 --- a/src/HOL/Library/ListVector.thy	Thu Jun 26 10:06:54 2008 +0200
    36.2 +++ b/src/HOL/Library/ListVector.thy	Thu Jun 26 10:07:01 2008 +0200
    36.3 @@ -5,7 +5,7 @@
    36.4  header "Lists as vectors"
    36.5  
    36.6  theory ListVector
    36.7 -imports Main
    36.8 +imports Plain List
    36.9  begin
   36.10  
   36.11  text{* \noindent
    37.1 --- a/src/HOL/Library/List_Prefix.thy	Thu Jun 26 10:06:54 2008 +0200
    37.2 +++ b/src/HOL/Library/List_Prefix.thy	Thu Jun 26 10:07:01 2008 +0200
    37.3 @@ -6,7 +6,7 @@
    37.4  header {* List prefixes and postfixes *}
    37.5  
    37.6  theory List_Prefix
    37.7 -imports List
    37.8 +imports Plain List
    37.9  begin
   37.10  
   37.11  subsection {* Prefix order on lists *}
    38.1 --- a/src/HOL/Library/List_lexord.thy	Thu Jun 26 10:06:54 2008 +0200
    38.2 +++ b/src/HOL/Library/List_lexord.thy	Thu Jun 26 10:07:01 2008 +0200
    38.3 @@ -6,7 +6,7 @@
    38.4  header {* Lexicographic order on lists *}
    38.5  
    38.6  theory List_lexord
    38.7 -imports List
    38.8 +imports Plain List
    38.9  begin
   38.10  
   38.11  instantiation list :: (ord) ord
    39.1 --- a/src/HOL/Library/Multiset.thy	Thu Jun 26 10:06:54 2008 +0200
    39.2 +++ b/src/HOL/Library/Multiset.thy	Thu Jun 26 10:07:01 2008 +0200
    39.3 @@ -6,7 +6,7 @@
    39.4  header {* Multisets *}
    39.5  
    39.6  theory Multiset
    39.7 -imports List
    39.8 +imports Plain List
    39.9  begin
   39.10  
   39.11  subsection {* The type of multisets *}
    40.1 --- a/src/HOL/Library/NatPair.thy	Thu Jun 26 10:06:54 2008 +0200
    40.2 +++ b/src/HOL/Library/NatPair.thy	Thu Jun 26 10:07:01 2008 +0200
    40.3 @@ -7,7 +7,7 @@
    40.4  header {* Pairs of Natural Numbers *}
    40.5  
    40.6  theory NatPair
    40.7 -imports ATP_Linkup
    40.8 +imports Plain Presburger
    40.9  begin
   40.10  
   40.11  text{*
    41.1 --- a/src/HOL/Library/Nat_Infinity.thy	Thu Jun 26 10:06:54 2008 +0200
    41.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Thu Jun 26 10:07:01 2008 +0200
    41.3 @@ -6,7 +6,7 @@
    41.4  header {* Natural numbers with infinity *}
    41.5  
    41.6  theory Nat_Infinity
    41.7 -imports ATP_Linkup
    41.8 +imports Plain Presburger
    41.9  begin
   41.10  
   41.11  subsection {* Type definition *}
    42.1 --- a/src/HOL/Library/Nested_Environment.thy	Thu Jun 26 10:06:54 2008 +0200
    42.2 +++ b/src/HOL/Library/Nested_Environment.thy	Thu Jun 26 10:07:01 2008 +0200
    42.3 @@ -6,7 +6,7 @@
    42.4  header {* Nested environments *}
    42.5  
    42.6  theory Nested_Environment
    42.7 -imports List
    42.8 +imports Plain List
    42.9  begin
   42.10  
   42.11  text {*
    43.1 --- a/src/HOL/Library/Numeral_Type.thy	Thu Jun 26 10:06:54 2008 +0200
    43.2 +++ b/src/HOL/Library/Numeral_Type.thy	Thu Jun 26 10:07:01 2008 +0200
    43.3 @@ -8,7 +8,7 @@
    43.4  header "Numeral Syntax for Types"
    43.5  
    43.6  theory Numeral_Type
    43.7 -  imports ATP_Linkup
    43.8 +imports Plain Presburger
    43.9  begin
   43.10  
   43.11  subsection {* Preliminary lemmas *}
    44.1 --- a/src/HOL/Library/Option_ord.thy	Thu Jun 26 10:06:54 2008 +0200
    44.2 +++ b/src/HOL/Library/Option_ord.thy	Thu Jun 26 10:07:01 2008 +0200
    44.3 @@ -6,7 +6,7 @@
    44.4  header {* Canonical order on option type *}
    44.5  
    44.6  theory Option_ord
    44.7 -imports ATP_Linkup
    44.8 +imports Plain
    44.9  begin
   44.10  
   44.11  instantiation option :: (order) order
    45.1 --- a/src/HOL/Library/Order_Relation.thy	Thu Jun 26 10:06:54 2008 +0200
    45.2 +++ b/src/HOL/Library/Order_Relation.thy	Thu Jun 26 10:07:01 2008 +0200
    45.3 @@ -5,7 +5,7 @@
    45.4  header {* Orders as Relations *}
    45.5  
    45.6  theory Order_Relation
    45.7 -imports ATP_Linkup Hilbert_Choice
    45.8 +imports Plain Hilbert_Choice ATP_Linkup
    45.9  begin
   45.10  
   45.11  text{* This prelude could be moved to theory Relation: *}
    46.1 --- a/src/HOL/Library/Parity.thy	Thu Jun 26 10:06:54 2008 +0200
    46.2 +++ b/src/HOL/Library/Parity.thy	Thu Jun 26 10:07:01 2008 +0200
    46.3 @@ -6,7 +6,7 @@
    46.4  header {* Even and Odd for int and nat *}
    46.5  
    46.6  theory Parity
    46.7 -imports ATP_Linkup
    46.8 +imports Plain Presburger
    46.9  begin
   46.10  
   46.11  class even_odd = type + 
    47.1 --- a/src/HOL/Library/Permutation.thy	Thu Jun 26 10:06:54 2008 +0200
    47.2 +++ b/src/HOL/Library/Permutation.thy	Thu Jun 26 10:07:01 2008 +0200
    47.3 @@ -5,7 +5,7 @@
    47.4  header {* Permutations *}
    47.5  
    47.6  theory Permutation
    47.7 -imports Multiset
    47.8 +imports Plain Multiset
    47.9  begin
   47.10  
   47.11  inductive
    48.1 --- a/src/HOL/Library/Pocklington.thy	Thu Jun 26 10:06:54 2008 +0200
    48.2 +++ b/src/HOL/Library/Pocklington.thy	Thu Jun 26 10:07:01 2008 +0200
    48.3 @@ -1,5 +1,5 @@
    48.4  (*  Title:      HOL/Library/Pocklington.thy
    48.5 -    ID:         $Id: 
    48.6 +    ID:         $Id$
    48.7      Author:     Amine Chaieb 
    48.8  *)
    48.9  
   48.10 @@ -7,7 +7,7 @@
   48.11  
   48.12  
   48.13  theory Pocklington
   48.14 -imports List Primes
   48.15 +imports Plain List Primes
   48.16  begin
   48.17  
   48.18  definition modeq:: "nat => nat => nat => bool"    ("(1[_ = _] '(mod _'))")
   48.19 @@ -596,9 +596,7 @@
   48.20    and Rop: "\<forall>x1 y1 x2 y2. R x1 x2 \<and> R y1 y2 \<longrightarrow> R (x1 * y1) (x2 * y2)" 
   48.21    and fS: "finite S" and Rfg: "\<forall>x\<in>S. R (h x) (g x)"
   48.22    shows "R (fold (op *) h e S) (fold (op *) g e S)"
   48.23 -  using prems
   48.24 -  by -(rule finite_subset_induct,auto)
   48.25 -
   48.26 +  using fS by (rule finite_subset_induct) (insert assms, auto)
   48.27  
   48.28  lemma nproduct_mod:
   48.29    assumes fS: "finite S" and n0: "n \<noteq> 0"
   48.30 @@ -621,11 +619,8 @@
   48.31  lemma coprime_nproduct:
   48.32    assumes fS: "finite S" and Sn: "\<forall>x\<in>S. coprime n (a x)"
   48.33    shows "coprime n (setprod a S)"
   48.34 -  using fS Sn
   48.35 -unfolding setprod_def
   48.36 -apply -
   48.37 -apply (rule finite_subset_induct)
   48.38 -by (auto simp add: coprime_mul)
   48.39 +  using fS unfolding setprod_def by (rule finite_subset_induct)
   48.40 +    (insert Sn, auto simp add: coprime_mul)
   48.41  
   48.42  lemma (in comm_monoid_mult) 
   48.43    fold_eq_general:
    49.1 --- a/src/HOL/Library/Primes.thy	Thu Jun 26 10:06:54 2008 +0200
    49.2 +++ b/src/HOL/Library/Primes.thy	Thu Jun 26 10:07:01 2008 +0200
    49.3 @@ -7,7 +7,7 @@
    49.4  header {* Primality on nat *}
    49.5  
    49.6  theory Primes
    49.7 -imports GCD Parity
    49.8 +imports Plain ATP_Linkup GCD Parity
    49.9  begin
   49.10  
   49.11  definition
    50.1 --- a/src/HOL/Library/Product_ord.thy	Thu Jun 26 10:06:54 2008 +0200
    50.2 +++ b/src/HOL/Library/Product_ord.thy	Thu Jun 26 10:07:01 2008 +0200
    50.3 @@ -6,7 +6,7 @@
    50.4  header {* Order on product types *}
    50.5  
    50.6  theory Product_ord
    50.7 -imports ATP_Linkup
    50.8 +imports Plain
    50.9  begin
   50.10  
   50.11  instantiation "*" :: (ord, ord) ord
    51.1 --- a/src/HOL/Library/Quicksort.thy	Thu Jun 26 10:06:54 2008 +0200
    51.2 +++ b/src/HOL/Library/Quicksort.thy	Thu Jun 26 10:07:01 2008 +0200
    51.3 @@ -6,7 +6,7 @@
    51.4  header{*Quicksort*}
    51.5  
    51.6  theory Quicksort
    51.7 -imports Multiset
    51.8 +imports Plain Multiset
    51.9  begin
   51.10  
   51.11  context linorder
    52.1 --- a/src/HOL/Library/Quotient.thy	Thu Jun 26 10:06:54 2008 +0200
    52.2 +++ b/src/HOL/Library/Quotient.thy	Thu Jun 26 10:07:01 2008 +0200
    52.3 @@ -6,7 +6,7 @@
    52.4  header {* Quotient types *}
    52.5  
    52.6  theory Quotient
    52.7 -imports ATP_Linkup Hilbert_Choice
    52.8 +imports Plain Hilbert_Choice
    52.9  begin
   52.10  
   52.11  text {*
    53.1 --- a/src/HOL/Library/RBT.thy	Thu Jun 26 10:06:54 2008 +0200
    53.2 +++ b/src/HOL/Library/RBT.thy	Thu Jun 26 10:07:01 2008 +0200
    53.3 @@ -8,7 +8,7 @@
    53.4  
    53.5  (*<*)
    53.6  theory RBT
    53.7 -imports Main AssocList
    53.8 +imports Plain AssocList
    53.9  begin
   53.10  
   53.11  datatype color = R | B
    54.1 --- a/src/HOL/Library/RType.thy	Thu Jun 26 10:06:54 2008 +0200
    54.2 +++ b/src/HOL/Library/RType.thy	Thu Jun 26 10:07:01 2008 +0200
    54.3 @@ -6,7 +6,7 @@
    54.4  header {* Reflecting Pure types into HOL *}
    54.5  
    54.6  theory RType
    54.7 -imports Main Code_Message Code_Index (* import all 'special code' types *)
    54.8 +imports Plain List Code_Message Code_Index (* import all 'special code' types *)
    54.9  begin
   54.10  
   54.11  datatype "rtype" = RType message_string "rtype list"
    55.1 --- a/src/HOL/Library/Ramsey.thy	Thu Jun 26 10:06:54 2008 +0200
    55.2 +++ b/src/HOL/Library/Ramsey.thy	Thu Jun 26 10:07:01 2008 +0200
    55.3 @@ -6,7 +6,7 @@
    55.4  header "Ramsey's Theorem"
    55.5  
    55.6  theory Ramsey
    55.7 -imports ATP_Linkup Infinite_Set
    55.8 +imports Plain Presburger Infinite_Set
    55.9  begin
   55.10  
   55.11  subsection {* Preliminaries *}
    56.1 --- a/src/HOL/Library/SetsAndFunctions.thy	Thu Jun 26 10:06:54 2008 +0200
    56.2 +++ b/src/HOL/Library/SetsAndFunctions.thy	Thu Jun 26 10:07:01 2008 +0200
    56.3 @@ -6,7 +6,7 @@
    56.4  header {* Operations on sets and functions *}
    56.5  
    56.6  theory SetsAndFunctions
    56.7 -imports ATP_Linkup
    56.8 +imports Plain
    56.9  begin
   56.10  
   56.11  text {*
    57.1 --- a/src/HOL/Library/State_Monad.thy	Thu Jun 26 10:06:54 2008 +0200
    57.2 +++ b/src/HOL/Library/State_Monad.thy	Thu Jun 26 10:07:01 2008 +0200
    57.3 @@ -6,7 +6,7 @@
    57.4  header {* Combinators syntax for generic, open state monads (single threaded monads) *}
    57.5  
    57.6  theory State_Monad
    57.7 -imports List
    57.8 +imports Plain List
    57.9  begin
   57.10  
   57.11  subsection {* Motivation *}
    58.1 --- a/src/HOL/Library/Sublist_Order.thy	Thu Jun 26 10:06:54 2008 +0200
    58.2 +++ b/src/HOL/Library/Sublist_Order.thy	Thu Jun 26 10:07:01 2008 +0200
    58.3 @@ -7,7 +7,7 @@
    58.4  header {* Sublist Ordering *}
    58.5  
    58.6  theory Sublist_Order
    58.7 -imports Main
    58.8 +imports Plain List
    58.9  begin
   58.10  
   58.11  text {*
    59.1 --- a/src/HOL/Library/Univ_Poly.thy	Thu Jun 26 10:06:54 2008 +0200
    59.2 +++ b/src/HOL/Library/Univ_Poly.thy	Thu Jun 26 10:07:01 2008 +0200
    59.3 @@ -6,7 +6,7 @@
    59.4  header{*Univariate Polynomials*}
    59.5  
    59.6  theory Univ_Poly
    59.7 -imports Main
    59.8 +imports Plain "../List"
    59.9  begin
   59.10  
   59.11  text{* Application of polynomial as a function. *}
    60.1 --- a/src/HOL/Library/While_Combinator.thy	Thu Jun 26 10:06:54 2008 +0200
    60.2 +++ b/src/HOL/Library/While_Combinator.thy	Thu Jun 26 10:07:01 2008 +0200
    60.3 @@ -7,7 +7,7 @@
    60.4  header {* A general ``while'' combinator *}
    60.5  
    60.6  theory While_Combinator
    60.7 -imports Main
    60.8 +imports Plain Presburger
    60.9  begin
   60.10  
   60.11  text {* 
    61.1 --- a/src/HOL/Library/Word.thy	Thu Jun 26 10:06:54 2008 +0200
    61.2 +++ b/src/HOL/Library/Word.thy	Thu Jun 26 10:07:01 2008 +0200
    61.3 @@ -6,7 +6,7 @@
    61.4  header {* Binary Words *}
    61.5  
    61.6  theory Word
    61.7 -imports List
    61.8 +imports Main
    61.9  begin
   61.10  
   61.11  subsection {* Auxilary Lemmas *}
   61.12 @@ -430,13 +430,13 @@
   61.13    "bv_to_nat (l1 @ l2) = bv_to_nat l1 * 2 ^ length l2 + bv_to_nat l2"
   61.14  proof -
   61.15    have "\<forall>l2. bv_to_nat (l1 @ l2) = bv_to_nat l1 * 2 ^ length l2 + bv_to_nat l2"
   61.16 -  proof (induct l1,simp_all)
   61.17 +  proof (induct l1, simp_all)
   61.18      fix x xs
   61.19      assume ind: "\<forall>l2. bv_to_nat (xs @ l2) = bv_to_nat xs * 2 ^ length l2 + bv_to_nat l2"
   61.20 -    show "\<forall>l2. bv_to_nat xs * 2 ^ length l2 + bitval x * 2 ^ (length xs + length l2) = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2"
   61.21 +    show "\<forall>l2::bit list. bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2"
   61.22      proof
   61.23        fix l2
   61.24 -      show "bv_to_nat xs * 2 ^ length l2 + bitval x * 2 ^ (length xs + length l2) = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2"
   61.25 +      show "bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2"
   61.26        proof -
   61.27          have "(2::nat) ^ (length xs + length l2) = 2 ^ length xs * 2 ^ length l2"
   61.28            by (induct "length xs",simp_all)
    62.1 --- a/src/HOL/List.thy	Thu Jun 26 10:06:54 2008 +0200
    62.2 +++ b/src/HOL/List.thy	Thu Jun 26 10:07:01 2008 +0200
    62.3 @@ -6,7 +6,7 @@
    62.4  header {* The datatype of finite lists *}
    62.5  
    62.6  theory List
    62.7 -imports ATP_Linkup
    62.8 +imports Plain Relation_Power Presburger Recdef ATP_Linkup
    62.9  uses "Tools/string_syntax.ML"
   62.10  begin
   62.11  
    63.1 --- a/src/HOL/MetisExamples/Abstraction.thy	Thu Jun 26 10:06:54 2008 +0200
    63.2 +++ b/src/HOL/MetisExamples/Abstraction.thy	Thu Jun 26 10:07:01 2008 +0200
    63.3 @@ -5,7 +5,8 @@
    63.4  Testing the metis method
    63.5  *)
    63.6  
    63.7 -theory Abstraction imports FuncSet
    63.8 +theory Abstraction
    63.9 +imports Main FuncSet
   63.10  begin
   63.11  
   63.12  (*For Christoph Benzmueller*)
   63.13 @@ -180,9 +181,10 @@
   63.14     CLF \<subseteq> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
   63.15     f \<in> pset cl \<inter> cl"
   63.16  by auto
   63.17 +
   63.18  (*??no longer terminates, with combinators
   63.19  by (metis Collect_mem_eq Int_def SigmaD2 UnCI Un_absorb1)
   63.20 -  --{*@{text Int_def} is redundant}
   63.21 +  --{*@{text Int_def} is redundant*}
   63.22  *)
   63.23  
   63.24  ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Int"*}
    64.1 --- a/src/HOL/MetisExamples/Tarski.thy	Thu Jun 26 10:06:54 2008 +0200
    64.2 +++ b/src/HOL/MetisExamples/Tarski.thy	Thu Jun 26 10:07:01 2008 +0200
    64.3 @@ -7,7 +7,9 @@
    64.4  
    64.5  header {* The Full Theorem of Tarski *}
    64.6  
    64.7 -theory Tarski imports FuncSet begin
    64.8 +theory Tarski
    64.9 +imports Main FuncSet
   64.10 +begin
   64.11  
   64.12  (*Many of these higher-order problems appear to be impossible using the
   64.13  current linkup. They often seem to need either higher-order unification
   64.14 @@ -961,8 +963,10 @@
   64.15  done
   64.16  
   64.17  ML_command{*ResAtp.problem_name:="Tarski__intY1_func"*}  (*ALL THEOREMS*)
   64.18 -lemma (in Tarski) intY1_func: "(%x: intY1. f x) \<in> intY1 -> intY1" 
   64.19 -by (metis intY1_f_closed restrict_in_funcset)
   64.20 +lemma (in Tarski) intY1_func: "(%x: intY1. f x) \<in> intY1 -> intY1"
   64.21 +apply (rule restrict_in_funcset)
   64.22 +apply (metis intY1_f_closed restrict_in_funcset)
   64.23 +done
   64.24  
   64.25  ML_command{*ResAtp.problem_name:="Tarski__intY1_mono"*}  (*ALL THEOREMS*)
   64.26  lemma (in Tarski) intY1_mono:
    65.1 --- a/src/HOL/NumberTheory/Factorization.thy	Thu Jun 26 10:06:54 2008 +0200
    65.2 +++ b/src/HOL/NumberTheory/Factorization.thy	Thu Jun 26 10:07:01 2008 +0200
    65.3 @@ -6,7 +6,9 @@
    65.4  
    65.5  header {* Fundamental Theorem of Arithmetic (unique factorization into primes) *}
    65.6  
    65.7 -theory Factorization imports Primes Permutation begin
    65.8 +theory Factorization
    65.9 +imports Main Primes Permutation
   65.10 +begin
   65.11  
   65.12  
   65.13  subsection {* Definitions *}
    66.1 --- a/src/HOL/NumberTheory/IntPrimes.thy	Thu Jun 26 10:06:54 2008 +0200
    66.2 +++ b/src/HOL/NumberTheory/IntPrimes.thy	Thu Jun 26 10:07:01 2008 +0200
    66.3 @@ -7,7 +7,7 @@
    66.4  header {* Divisibility and prime numbers (on integers) *}
    66.5  
    66.6  theory IntPrimes
    66.7 -imports Primes
    66.8 +imports Main Primes
    66.9  begin
   66.10  
   66.11  text {*
    67.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    67.2 +++ b/src/HOL/Plain.thy	Thu Jun 26 10:07:01 2008 +0200
    67.3 @@ -0,0 +1,15 @@
    67.4 +(*  Title:      HOL/Plain.thy
    67.5 +    ID:         $Id$
    67.6 +
    67.7 +Contains fundamental HOL tools and packages.  Does not include Hilbert_Choice.
    67.8 +*)
    67.9 +
   67.10 +header {* Plain HOL *}
   67.11 +
   67.12 +theory Plain
   67.13 +imports Datatype FunDef Record SAT Extraction
   67.14 +begin
   67.15 +
   67.16 +ML {* path_add "~~/src/HOL/Library" *}
   67.17 +
   67.18 +end
    68.1 --- a/src/HOL/ROOT.ML	Thu Jun 26 10:06:54 2008 +0200
    68.2 +++ b/src/HOL/ROOT.ML	Thu Jun 26 10:07:01 2008 +0200
    68.3 @@ -1,7 +1,7 @@
    68.4  (*  Title:      HOL/ROOT.ML
    68.5      ID:         $Id$
    68.6   
    68.7 -Classical Higher-order Logic.
    68.8 +Classical Higher-order Logic -- batteries included.
    68.9  *)
   68.10  
   68.11  use_thy "Main";
    69.1 --- a/src/HOL/Real/ContNotDenum.thy	Thu Jun 26 10:06:54 2008 +0200
    69.2 +++ b/src/HOL/Real/ContNotDenum.thy	Thu Jun 26 10:07:01 2008 +0200
    69.3 @@ -6,7 +6,7 @@
    69.4  header {* Non-denumerability of the Continuum. *}
    69.5  
    69.6  theory ContNotDenum
    69.7 -imports RComplete
    69.8 +imports RComplete "../Hilbert_Choice"
    69.9  begin
   69.10  
   69.11  subsection {* Abstract *}
    70.1 --- a/src/HOL/Real/Lubs.thy	Thu Jun 26 10:06:54 2008 +0200
    70.2 +++ b/src/HOL/Real/Lubs.thy	Thu Jun 26 10:07:01 2008 +0200
    70.3 @@ -7,7 +7,7 @@
    70.4  header{*Definitions of Upper Bounds and Least Upper Bounds*}
    70.5  
    70.6  theory Lubs
    70.7 -imports Main
    70.8 +imports Plain
    70.9  begin
   70.10  
   70.11  text{*Thanks to suggestions by James Margetson*}
    71.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    71.2 +++ b/src/HOL/plain.ML	Thu Jun 26 10:07:01 2008 +0200
    71.3 @@ -0,0 +1,7 @@
    71.4 +(*  Title:      HOL/plain.ML
    71.5 +    ID:         $Id$
    71.6 + 
    71.7 +Classical Higher-order Logic -- plain Tool bootstrap.
    71.8 +*)
    71.9 +
   71.10 +use_thy "Plain";