merged
authorwenzelm
Tue Mar 26 20:55:21 2013 +0100 (2013-03-26)
changeset 515456f6012f430fc
parent 51540 eea5c4ca4a0e
parent 51544 8c58fbbc1d5a
child 51546 2e26df807dc7
child 51549 37211c7c2894
merged
src/HOL/Library/Saturated.thy
     1.1 --- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Tue Mar 26 20:49:57 2013 +0100
     1.2 +++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Tue Mar 26 20:55:21 2013 +0100
     1.3 @@ -3046,7 +3046,7 @@
     1.4              by auto
     1.5            with nrm_C_C' nrm_C' A
     1.6            have "?NormalAssigned s3 A"
     1.7 -            by fastforce
     1.8 +            by auto
     1.9            moreover
    1.10            from eq_s3_s2 brk_C_C' brk_C' normal_s1 A
    1.11            have "?BreakAssigned (Norm s0) s3 A"
     2.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Tue Mar 26 20:49:57 2013 +0100
     2.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Tue Mar 26 20:55:21 2013 +0100
     2.3 @@ -8,7 +8,7 @@
     2.4    Complex_Main
     2.5    "~~/src/HOL/Library/Float"
     2.6    "~~/src/HOL/Library/Reflection"
     2.7 -  "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
     2.8 +  Dense_Linear_Order
     2.9    "~~/src/HOL/Library/Code_Target_Numeral"
    2.10  begin
    2.11  
     3.1 --- a/src/HOL/Decision_Procs/Decision_Procs.thy	Tue Mar 26 20:49:57 2013 +0100
     3.2 +++ b/src/HOL/Decision_Procs/Decision_Procs.thy	Tue Mar 26 20:55:21 2013 +0100
     3.3 @@ -1,11 +1,16 @@
     3.4 -header {* Various decision procedures, typically involving reflection *}
     3.5 -
     3.6  theory Decision_Procs
     3.7  imports
     3.8 -  Commutative_Ring Cooper Ferrack MIR Approximation Dense_Linear_Order
     3.9 +  Commutative_Ring
    3.10 +  Cooper
    3.11 +  Ferrack
    3.12 +  MIR
    3.13 +  Approximation
    3.14 +  Dense_Linear_Order
    3.15    Parametric_Ferrante_Rackoff
    3.16    Commutative_Ring_Complete
    3.17 -  "ex/Commutative_Ring_Ex" "ex/Approximation_Ex" "ex/Dense_Linear_Order_Ex"
    3.18 +  "ex/Commutative_Ring_Ex"
    3.19 +  "ex/Approximation_Ex"
    3.20 +  "ex/Dense_Linear_Order_Ex"
    3.21  begin
    3.22  
    3.23  end
     4.1 --- a/src/HOL/Library/Code_Char.thy	Tue Mar 26 20:49:57 2013 +0100
     4.2 +++ b/src/HOL/Library/Code_Char.thy	Tue Mar 26 20:55:21 2013 +0100
     4.3 @@ -5,7 +5,7 @@
     4.4  header {* Code generation of pretty characters (and strings) *}
     4.5  
     4.6  theory Code_Char
     4.7 -imports Main "~~/src/HOL/Library/Char_ord"
     4.8 +imports Main Char_ord
     4.9  begin
    4.10  
    4.11  code_type char
     5.1 --- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Tue Mar 26 20:49:57 2013 +0100
     5.2 +++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Tue Mar 26 20:55:21 2013 +0100
     5.3 @@ -1,7 +1,7 @@
     5.4  (* Authors: Florian Haftmann, Johannes Hölzl, Tobias Nipkow *)
     5.5  
     5.6  theory Code_Real_Approx_By_Float
     5.7 -imports Complex_Main "~~/src/HOL/Library/Code_Target_Int"
     5.8 +imports Complex_Main Code_Target_Int
     5.9  begin
    5.10  
    5.11  text{* \textbf{WARNING} This theory implements mathematical reals by machine
     6.1 --- a/src/HOL/Library/Countable_Set.thy	Tue Mar 26 20:49:57 2013 +0100
     6.2 +++ b/src/HOL/Library/Countable_Set.thy	Tue Mar 26 20:55:21 2013 +0100
     6.3 @@ -6,7 +6,7 @@
     6.4  header {* Countable sets *}
     6.5  
     6.6  theory Countable_Set
     6.7 -  imports "~~/src/HOL/Library/Countable" "~~/src/HOL/Library/Infinite_Set"
     6.8 +imports Countable Infinite_Set
     6.9  begin
    6.10  
    6.11  subsection {* Predicate for countable sets *}
     7.1 --- a/src/HOL/Library/FinFun_Syntax.thy	Tue Mar 26 20:49:57 2013 +0100
     7.2 +++ b/src/HOL/Library/FinFun_Syntax.thy	Tue Mar 26 20:55:21 2013 +0100
     7.3 @@ -2,7 +2,9 @@
     7.4  
     7.5  header {* Pretty syntax for almost everywhere constant functions *}
     7.6  
     7.7 -theory FinFun_Syntax imports FinFun begin
     7.8 +theory FinFun_Syntax
     7.9 +imports FinFun
    7.10 +begin
    7.11  
    7.12  type_notation
    7.13    finfun ("(_ =>f /_)" [22, 21] 21)
     8.1 --- a/src/HOL/Library/Float.thy	Tue Mar 26 20:49:57 2013 +0100
     8.2 +++ b/src/HOL/Library/Float.thy	Tue Mar 26 20:55:21 2013 +0100
     8.3 @@ -6,7 +6,7 @@
     8.4  header {* Floating-Point Numbers *}
     8.5  
     8.6  theory Float
     8.7 -imports Complex_Main "~~/src/HOL/Library/Lattice_Algebras"
     8.8 +imports Complex_Main Lattice_Algebras
     8.9  begin
    8.10  
    8.11  definition "float = {m * 2 powr e | (m :: int) (e :: int). True}"
     9.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Tue Mar 26 20:49:57 2013 +0100
     9.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Tue Mar 26 20:55:21 2013 +0100
     9.3 @@ -5,7 +5,7 @@
     9.4  header{* A formalization of formal power series *}
     9.5  
     9.6  theory Formal_Power_Series
     9.7 -imports Complex_Main Binomial
     9.8 +imports Binomial
     9.9  begin
    9.10  
    9.11  
    10.1 --- a/src/HOL/Library/Function_Growth.thy	Tue Mar 26 20:49:57 2013 +0100
    10.2 +++ b/src/HOL/Library/Function_Growth.thy	Tue Mar 26 20:55:21 2013 +0100
    10.3 @@ -4,7 +4,7 @@
    10.4  header {* Comparing growth of functions on natural numbers by a preorder relation *}
    10.5  
    10.6  theory Function_Growth
    10.7 -imports Main "~~/src/HOL/Library/Preorder" "~~/src/HOL/Library/Discrete"
    10.8 +imports Main Preorder Discrete
    10.9  begin
   10.10  
   10.11  subsection {* Motivation *}
    11.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Mar 26 20:49:57 2013 +0100
    11.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Mar 26 20:55:21 2013 +0100
    11.3 @@ -191,7 +191,7 @@
    11.4      hence "(abs (2 * x))^2 <= 1^2" "(abs (2 * y)) ^2 <= 1^2"
    11.5        by - (rule power_mono, simp, simp)+
    11.6      hence th0: "4*x^2 \<le> 1" "4*y^2 \<le> 1"
    11.7 -      by (simp_all  add: power2_abs power_mult_distrib)
    11.8 +      by (simp_all add: power_mult_distrib)
    11.9      from add_mono[OF th0] xy have False by simp }
   11.10    thus ?thesis unfolding linorder_not_le[symmetric] by blast
   11.11  qed
   11.12 @@ -490,7 +490,7 @@
   11.13          unfolding norm_mult by (simp add: algebra_simps)
   11.14        from complex_mod_triangle_sub[of "z * poly (pCons c cs) z" a]
   11.15        have th2: "cmod(z * poly (pCons c cs) z) - cmod a \<le> cmod (poly (pCons a (pCons c cs)) z)"
   11.16 -        by (simp add: diff_le_eq algebra_simps)
   11.17 +        by (simp add: algebra_simps)
   11.18        from th1 th2 have "d \<le> cmod (poly (pCons a (pCons c cs)) z)"  by arith}
   11.19      hence ?case by blast}
   11.20    moreover
   11.21 @@ -601,7 +601,6 @@
   11.22      apply (rule_tac x="a" in exI)
   11.23      apply simp
   11.24      apply (rule_tac x="q" in exI)
   11.25 -    apply (auto simp add: power_Suc)
   11.26      apply (auto simp add: psize_def split: if_splits)
   11.27      done
   11.28  qed
   11.29 @@ -718,7 +717,7 @@
   11.30        have th30: "t^k * (t* (cmod w ^ (k + 1) * m)) < t^k * 1"
   11.31          apply - apply (rule mult_strict_left_mono) by simp_all
   11.32        have "cmod (?w^k * ?w * poly s ?w) = t^k * (t* (cmod w ^ (k+1) * cmod (poly s ?w)))"  using w0 t(1)
   11.33 -        by (simp add: algebra_simps power_mult_distrib norm_of_real norm_power norm_mult)
   11.34 +        by (simp add: algebra_simps power_mult_distrib norm_power norm_mult)
   11.35        then have "cmod (?w^k * ?w * poly s ?w) \<le> t^k * (t* (cmod w ^ (k + 1) * m))"
   11.36          using t(1,2) m(2)[rule_format, OF tw] w0
   11.37          apply (simp only: )
   11.38 @@ -819,9 +818,8 @@
   11.39          have sne: "s \<noteq> 0"
   11.40            using s pne by auto
   11.41          {assume ds0: "degree s = 0"
   11.42 -          from ds0 have "\<exists>k. s = [:k:]"
   11.43 -            by (cases s, simp split: if_splits)
   11.44 -          then obtain k where kpn: "s = [:k:]" by blast
   11.45 +          from ds0 obtain k where kpn: "s = [:k:]"
   11.46 +            by (cases s) (auto split: if_splits)
   11.47            from sne kpn have k: "k \<noteq> 0" by simp
   11.48            let ?w = "([:1/k:] * ([:-a,1:] ^ (n - ?op))) * (r ^ n)"
   11.49            from k oop [of a] have "q ^ n = p * ?w"
   11.50 @@ -878,9 +876,7 @@
   11.51  
   11.52      then have pp: "\<And>x. poly p x =  c" by simp
   11.53      let ?w = "[:1/c:] * (q ^ n)"
   11.54 -    from ccs
   11.55 -    have "(q ^ n) = (p * ?w) "
   11.56 -      by (simp add: smult_smult)
   11.57 +    from ccs have "(q ^ n) = (p * ?w)" by simp
   11.58      hence ?ths unfolding dvd_def by blast}
   11.59    ultimately show ?ths by blast
   11.60  qed
   11.61 @@ -902,7 +898,7 @@
   11.62    {assume pe: "p \<noteq> 0"
   11.63      {assume dp: "degree p = 0"
   11.64        then obtain k where k: "p = [:k:]" "k\<noteq>0" using pe
   11.65 -        by (cases p, simp split: if_splits)
   11.66 +        by (cases p) (simp split: if_splits)
   11.67        hence th1: "\<forall>x. poly p x \<noteq> 0" by simp
   11.68        from k dp have "q ^ (degree p) = p * [:1/k:]"
   11.69          by (simp add: one_poly_def)
   11.70 @@ -937,7 +933,7 @@
   11.71  next
   11.72    assume r: ?rhs
   11.73    then obtain k where "p = [:k:]"
   11.74 -    by (cases p, simp split: if_splits)
   11.75 +    by (cases p) (simp split: if_splits)
   11.76    then show ?lhs unfolding constant_def by auto
   11.77  qed
   11.78  
   11.79 @@ -1019,14 +1015,13 @@
   11.80    {assume l: ?lhs
   11.81      then obtain u where u: "q = p * u" ..
   11.82       have "r = p * (smult a u - t)"
   11.83 -       using u qrp' [symmetric] t by (simp add: algebra_simps mult_smult_right)
   11.84 +       using u qrp' [symmetric] t by (simp add: algebra_simps)
   11.85       then have ?rhs ..}
   11.86    moreover
   11.87    {assume r: ?rhs
   11.88      then obtain u where u: "r = p * u" ..
   11.89      from u [symmetric] t qrp' [symmetric] a0
   11.90 -    have "q = p * smult (1/a) (u + t)"
   11.91 -      by (simp add: algebra_simps mult_smult_right smult_smult)
   11.92 +    have "q = p * smult (1/a) (u + t)" by (simp add: algebra_simps)
   11.93      hence ?lhs ..}
   11.94    ultimately have "?lhs = ?rhs" by blast }
   11.95  thus "?lhs \<equiv> ?rhs"  by - (atomize(full), blast)
   11.96 @@ -1056,7 +1051,7 @@
   11.97  proof-
   11.98    have "p = 0 \<longleftrightarrow> poly p = poly 0"
   11.99      by (simp add: poly_zero)
  11.100 -  also have "\<dots> \<longleftrightarrow> (\<not> (\<exists>x. poly p x \<noteq> 0))" by (auto intro: ext)
  11.101 +  also have "\<dots> \<longleftrightarrow> (\<not> (\<exists>x. poly p x \<noteq> 0))" by auto
  11.102    finally show "(\<exists>x. poly p x \<noteq> (0::complex)) \<equiv> p \<noteq> 0"
  11.103      by - (atomize (full), blast)
  11.104  qed
  11.105 @@ -1078,7 +1073,7 @@
  11.106    assumes h: "\<And>x. poly (q ^ n) x \<equiv> poly r x"
  11.107    shows "p dvd (q ^ n) \<equiv> p dvd r"
  11.108  proof-
  11.109 -  from h have "poly (q ^ n) = poly r" by (auto intro: ext)
  11.110 +  from h have "poly (q ^ n) = poly r" by auto
  11.111    then have "(q ^ n) = r" by (simp add: poly_eq_iff)
  11.112    thus "p dvd (q ^ n) \<equiv> p dvd r" by simp
  11.113  qed
    12.1 --- a/src/HOL/Library/Library.thy	Tue Mar 26 20:49:57 2013 +0100
    12.2 +++ b/src/HOL/Library/Library.thy	Tue Mar 26 20:55:21 2013 +0100
    12.3 @@ -16,7 +16,9 @@
    12.4    Debug
    12.5    Diagonal_Subsequence
    12.6    Dlist
    12.7 -  Extended Extended_Nat Extended_Real
    12.8 +  Extended
    12.9 +  Extended_Nat
   12.10 +  Extended_Real
   12.11    FinFun
   12.12    Float
   12.13    Formal_Power_Series
    13.1 --- a/src/HOL/Library/Liminf_Limsup.thy	Tue Mar 26 20:49:57 2013 +0100
    13.2 +++ b/src/HOL/Library/Liminf_Limsup.thy	Tue Mar 26 20:55:21 2013 +0100
    13.3 @@ -5,7 +5,7 @@
    13.4  header {* Liminf and Limsup on complete lattices *}
    13.5  
    13.6  theory Liminf_Limsup
    13.7 -imports "~~/src/HOL/Complex_Main"
    13.8 +imports Complex_Main
    13.9  begin
   13.10  
   13.11  lemma le_Sup_iff_less:
    14.1 --- a/src/HOL/Library/Permutation.thy	Tue Mar 26 20:49:57 2013 +0100
    14.2 +++ b/src/HOL/Library/Permutation.thy	Tue Mar 26 20:55:21 2013 +0100
    14.3 @@ -5,7 +5,7 @@
    14.4  header {* Permutations *}
    14.5  
    14.6  theory Permutation
    14.7 -imports Main Multiset
    14.8 +imports Multiset
    14.9  begin
   14.10  
   14.11  inductive
    15.1 --- a/src/HOL/Library/Phantom_Type.thy	Tue Mar 26 20:49:57 2013 +0100
    15.2 +++ b/src/HOL/Library/Phantom_Type.thy	Tue Mar 26 20:55:21 2013 +0100
    15.3 @@ -4,7 +4,9 @@
    15.4  
    15.5  header {* A generic phantom type *}
    15.6  
    15.7 -theory Phantom_Type imports Main begin
    15.8 +theory Phantom_Type
    15.9 +imports Main
   15.10 +begin
   15.11  
   15.12  datatype ('a, 'b) phantom = phantom 'b
   15.13  
    16.1 --- a/src/HOL/Library/Product_Order.thy	Tue Mar 26 20:49:57 2013 +0100
    16.2 +++ b/src/HOL/Library/Product_Order.thy	Tue Mar 26 20:55:21 2013 +0100
    16.3 @@ -5,7 +5,7 @@
    16.4  header {* Pointwise order on product types *}
    16.5  
    16.6  theory Product_Order
    16.7 -imports "~~/src/HOL/Library/Product_plus"
    16.8 +imports Product_plus
    16.9  begin
   16.10  
   16.11  subsection {* Pointwise ordering *}
    17.1 --- a/src/HOL/Library/Reflection.thy	Tue Mar 26 20:49:57 2013 +0100
    17.2 +++ b/src/HOL/Library/Reflection.thy	Tue Mar 26 20:55:21 2013 +0100
    17.3 @@ -8,8 +8,8 @@
    17.4  imports Main
    17.5  begin
    17.6  
    17.7 -ML_file "~~/src/HOL/Library/reify_data.ML"
    17.8 -ML_file "~~/src/HOL/Library/reflection.ML"
    17.9 +ML_file "reify_data.ML"
   17.10 +ML_file "reflection.ML"
   17.11  
   17.12  setup {* Reify_Data.setup *}
   17.13  
    18.1 --- a/src/HOL/Library/Saturated.thy	Tue Mar 26 20:49:57 2013 +0100
    18.2 +++ b/src/HOL/Library/Saturated.thy	Tue Mar 26 20:55:21 2013 +0100
    18.3 @@ -7,7 +7,7 @@
    18.4  header {* Saturated arithmetic *}
    18.5  
    18.6  theory Saturated
    18.7 -imports Main "~~/src/HOL/Library/Numeral_Type" "~~/src/HOL/Word/Type_Length"
    18.8 +imports Numeral_Type "~~/src/HOL/Word/Type_Length"
    18.9  begin
   18.10  
   18.11  subsection {* The type of saturated naturals *}
    19.1 --- a/src/HOL/ROOT	Tue Mar 26 20:49:57 2013 +0100
    19.2 +++ b/src/HOL/ROOT	Tue Mar 26 20:55:21 2013 +0100
    19.3 @@ -347,6 +347,9 @@
    19.4    files "document/root.bib" "document/root.tex"
    19.5  
    19.6  session "HOL-Decision_Procs" in Decision_Procs = HOL +
    19.7 +  description {*
    19.8 +    Various decision procedures, typically involving reflection.
    19.9 +  *}
   19.10    options [condition = ISABELLE_POLYML, document = false]
   19.11    theories Decision_Procs
   19.12