# HG changeset patch # User wenzelm # Date 1364327721 -3600 # Node ID 6f6012f430fca7715294e84aac015d522cf4d2ae # Parent eea5c4ca4a0ee533b319d6414cf6a965b66abbef# Parent 8c58fbbc1d5a265c6fb3427a03f71254067aaf9f merged diff -r eea5c4ca4a0e -r 6f6012f430fc src/HOL/Bali/DefiniteAssignmentCorrect.thy --- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy Tue Mar 26 20:49:57 2013 +0100 +++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy Tue Mar 26 20:55:21 2013 +0100 @@ -3046,7 +3046,7 @@ by auto with nrm_C_C' nrm_C' A have "?NormalAssigned s3 A" - by fastforce + by auto moreover from eq_s3_s2 brk_C_C' brk_C' normal_s1 A have "?BreakAssigned (Norm s0) s3 A" diff -r eea5c4ca4a0e -r 6f6012f430fc src/HOL/Decision_Procs/Approximation.thy --- a/src/HOL/Decision_Procs/Approximation.thy Tue Mar 26 20:49:57 2013 +0100 +++ b/src/HOL/Decision_Procs/Approximation.thy Tue Mar 26 20:55:21 2013 +0100 @@ -8,7 +8,7 @@ Complex_Main "~~/src/HOL/Library/Float" "~~/src/HOL/Library/Reflection" - "~~/src/HOL/Decision_Procs/Dense_Linear_Order" + Dense_Linear_Order "~~/src/HOL/Library/Code_Target_Numeral" begin diff -r eea5c4ca4a0e -r 6f6012f430fc src/HOL/Decision_Procs/Decision_Procs.thy --- a/src/HOL/Decision_Procs/Decision_Procs.thy Tue Mar 26 20:49:57 2013 +0100 +++ b/src/HOL/Decision_Procs/Decision_Procs.thy Tue Mar 26 20:55:21 2013 +0100 @@ -1,11 +1,16 @@ -header {* Various decision procedures, typically involving reflection *} - theory Decision_Procs imports - Commutative_Ring Cooper Ferrack MIR Approximation Dense_Linear_Order + Commutative_Ring + Cooper + Ferrack + MIR + Approximation + Dense_Linear_Order Parametric_Ferrante_Rackoff Commutative_Ring_Complete - "ex/Commutative_Ring_Ex" "ex/Approximation_Ex" "ex/Dense_Linear_Order_Ex" + "ex/Commutative_Ring_Ex" + "ex/Approximation_Ex" + "ex/Dense_Linear_Order_Ex" begin end diff -r eea5c4ca4a0e -r 6f6012f430fc src/HOL/Library/Code_Char.thy --- a/src/HOL/Library/Code_Char.thy Tue Mar 26 20:49:57 2013 +0100 +++ b/src/HOL/Library/Code_Char.thy Tue Mar 26 20:55:21 2013 +0100 @@ -5,7 +5,7 @@ header {* Code generation of pretty characters (and strings) *} theory Code_Char -imports Main "~~/src/HOL/Library/Char_ord" +imports Main Char_ord begin code_type char diff -r eea5c4ca4a0e -r 6f6012f430fc src/HOL/Library/Code_Real_Approx_By_Float.thy --- a/src/HOL/Library/Code_Real_Approx_By_Float.thy Tue Mar 26 20:49:57 2013 +0100 +++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy Tue Mar 26 20:55:21 2013 +0100 @@ -1,7 +1,7 @@ (* Authors: Florian Haftmann, Johannes Hölzl, Tobias Nipkow *) theory Code_Real_Approx_By_Float -imports Complex_Main "~~/src/HOL/Library/Code_Target_Int" +imports Complex_Main Code_Target_Int begin text{* \textbf{WARNING} This theory implements mathematical reals by machine diff -r eea5c4ca4a0e -r 6f6012f430fc src/HOL/Library/Countable_Set.thy --- a/src/HOL/Library/Countable_Set.thy Tue Mar 26 20:49:57 2013 +0100 +++ b/src/HOL/Library/Countable_Set.thy Tue Mar 26 20:55:21 2013 +0100 @@ -6,7 +6,7 @@ header {* Countable sets *} theory Countable_Set - imports "~~/src/HOL/Library/Countable" "~~/src/HOL/Library/Infinite_Set" +imports Countable Infinite_Set begin subsection {* Predicate for countable sets *} diff -r eea5c4ca4a0e -r 6f6012f430fc src/HOL/Library/FinFun_Syntax.thy --- a/src/HOL/Library/FinFun_Syntax.thy Tue Mar 26 20:49:57 2013 +0100 +++ b/src/HOL/Library/FinFun_Syntax.thy Tue Mar 26 20:55:21 2013 +0100 @@ -2,7 +2,9 @@ header {* Pretty syntax for almost everywhere constant functions *} -theory FinFun_Syntax imports FinFun begin +theory FinFun_Syntax +imports FinFun +begin type_notation finfun ("(_ =>f /_)" [22, 21] 21) diff -r eea5c4ca4a0e -r 6f6012f430fc src/HOL/Library/Float.thy --- a/src/HOL/Library/Float.thy Tue Mar 26 20:49:57 2013 +0100 +++ b/src/HOL/Library/Float.thy Tue Mar 26 20:55:21 2013 +0100 @@ -6,7 +6,7 @@ header {* Floating-Point Numbers *} theory Float -imports Complex_Main "~~/src/HOL/Library/Lattice_Algebras" +imports Complex_Main Lattice_Algebras begin definition "float = {m * 2 powr e | (m :: int) (e :: int). True}" diff -r eea5c4ca4a0e -r 6f6012f430fc src/HOL/Library/Formal_Power_Series.thy --- a/src/HOL/Library/Formal_Power_Series.thy Tue Mar 26 20:49:57 2013 +0100 +++ b/src/HOL/Library/Formal_Power_Series.thy Tue Mar 26 20:55:21 2013 +0100 @@ -5,7 +5,7 @@ header{* A formalization of formal power series *} theory Formal_Power_Series -imports Complex_Main Binomial +imports Binomial begin diff -r eea5c4ca4a0e -r 6f6012f430fc src/HOL/Library/Function_Growth.thy --- a/src/HOL/Library/Function_Growth.thy Tue Mar 26 20:49:57 2013 +0100 +++ b/src/HOL/Library/Function_Growth.thy Tue Mar 26 20:55:21 2013 +0100 @@ -4,7 +4,7 @@ header {* Comparing growth of functions on natural numbers by a preorder relation *} theory Function_Growth -imports Main "~~/src/HOL/Library/Preorder" "~~/src/HOL/Library/Discrete" +imports Main Preorder Discrete begin subsection {* Motivation *} diff -r eea5c4ca4a0e -r 6f6012f430fc src/HOL/Library/Fundamental_Theorem_Algebra.thy --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Tue Mar 26 20:49:57 2013 +0100 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Tue Mar 26 20:55:21 2013 +0100 @@ -191,7 +191,7 @@ hence "(abs (2 * x))^2 <= 1^2" "(abs (2 * y)) ^2 <= 1^2" by - (rule power_mono, simp, simp)+ hence th0: "4*x^2 \ 1" "4*y^2 \ 1" - by (simp_all add: power2_abs power_mult_distrib) + by (simp_all add: power_mult_distrib) from add_mono[OF th0] xy have False by simp } thus ?thesis unfolding linorder_not_le[symmetric] by blast qed @@ -490,7 +490,7 @@ unfolding norm_mult by (simp add: algebra_simps) from complex_mod_triangle_sub[of "z * poly (pCons c cs) z" a] have th2: "cmod(z * poly (pCons c cs) z) - cmod a \ cmod (poly (pCons a (pCons c cs)) z)" - by (simp add: diff_le_eq algebra_simps) + by (simp add: algebra_simps) from th1 th2 have "d \ cmod (poly (pCons a (pCons c cs)) z)" by arith} hence ?case by blast} moreover @@ -601,7 +601,6 @@ apply (rule_tac x="a" in exI) apply simp apply (rule_tac x="q" in exI) - apply (auto simp add: power_Suc) apply (auto simp add: psize_def split: if_splits) done qed @@ -718,7 +717,7 @@ have th30: "t^k * (t* (cmod w ^ (k + 1) * m)) < t^k * 1" apply - apply (rule mult_strict_left_mono) by simp_all have "cmod (?w^k * ?w * poly s ?w) = t^k * (t* (cmod w ^ (k+1) * cmod (poly s ?w)))" using w0 t(1) - by (simp add: algebra_simps power_mult_distrib norm_of_real norm_power norm_mult) + by (simp add: algebra_simps power_mult_distrib norm_power norm_mult) then have "cmod (?w^k * ?w * poly s ?w) \ t^k * (t* (cmod w ^ (k + 1) * m))" using t(1,2) m(2)[rule_format, OF tw] w0 apply (simp only: ) @@ -819,9 +818,8 @@ have sne: "s \ 0" using s pne by auto {assume ds0: "degree s = 0" - from ds0 have "\k. s = [:k:]" - by (cases s, simp split: if_splits) - then obtain k where kpn: "s = [:k:]" by blast + from ds0 obtain k where kpn: "s = [:k:]" + by (cases s) (auto split: if_splits) from sne kpn have k: "k \ 0" by simp let ?w = "([:1/k:] * ([:-a,1:] ^ (n - ?op))) * (r ^ n)" from k oop [of a] have "q ^ n = p * ?w" @@ -878,9 +876,7 @@ then have pp: "\x. poly p x = c" by simp let ?w = "[:1/c:] * (q ^ n)" - from ccs - have "(q ^ n) = (p * ?w) " - by (simp add: smult_smult) + from ccs have "(q ^ n) = (p * ?w)" by simp hence ?ths unfolding dvd_def by blast} ultimately show ?ths by blast qed @@ -902,7 +898,7 @@ {assume pe: "p \ 0" {assume dp: "degree p = 0" then obtain k where k: "p = [:k:]" "k\0" using pe - by (cases p, simp split: if_splits) + by (cases p) (simp split: if_splits) hence th1: "\x. poly p x \ 0" by simp from k dp have "q ^ (degree p) = p * [:1/k:]" by (simp add: one_poly_def) @@ -937,7 +933,7 @@ next assume r: ?rhs then obtain k where "p = [:k:]" - by (cases p, simp split: if_splits) + by (cases p) (simp split: if_splits) then show ?lhs unfolding constant_def by auto qed @@ -1019,14 +1015,13 @@ {assume l: ?lhs then obtain u where u: "q = p * u" .. have "r = p * (smult a u - t)" - using u qrp' [symmetric] t by (simp add: algebra_simps mult_smult_right) + using u qrp' [symmetric] t by (simp add: algebra_simps) then have ?rhs ..} moreover {assume r: ?rhs then obtain u where u: "r = p * u" .. from u [symmetric] t qrp' [symmetric] a0 - have "q = p * smult (1/a) (u + t)" - by (simp add: algebra_simps mult_smult_right smult_smult) + have "q = p * smult (1/a) (u + t)" by (simp add: algebra_simps) hence ?lhs ..} ultimately have "?lhs = ?rhs" by blast } thus "?lhs \ ?rhs" by - (atomize(full), blast) @@ -1056,7 +1051,7 @@ proof- have "p = 0 \ poly p = poly 0" by (simp add: poly_zero) - also have "\ \ (\ (\x. poly p x \ 0))" by (auto intro: ext) + also have "\ \ (\ (\x. poly p x \ 0))" by auto finally show "(\x. poly p x \ (0::complex)) \ p \ 0" by - (atomize (full), blast) qed @@ -1078,7 +1073,7 @@ assumes h: "\x. poly (q ^ n) x \ poly r x" shows "p dvd (q ^ n) \ p dvd r" proof- - from h have "poly (q ^ n) = poly r" by (auto intro: ext) + from h have "poly (q ^ n) = poly r" by auto then have "(q ^ n) = r" by (simp add: poly_eq_iff) thus "p dvd (q ^ n) \ p dvd r" by simp qed diff -r eea5c4ca4a0e -r 6f6012f430fc src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Tue Mar 26 20:49:57 2013 +0100 +++ b/src/HOL/Library/Library.thy Tue Mar 26 20:55:21 2013 +0100 @@ -16,7 +16,9 @@ Debug Diagonal_Subsequence Dlist - Extended Extended_Nat Extended_Real + Extended + Extended_Nat + Extended_Real FinFun Float Formal_Power_Series diff -r eea5c4ca4a0e -r 6f6012f430fc src/HOL/Library/Liminf_Limsup.thy --- a/src/HOL/Library/Liminf_Limsup.thy Tue Mar 26 20:49:57 2013 +0100 +++ b/src/HOL/Library/Liminf_Limsup.thy Tue Mar 26 20:55:21 2013 +0100 @@ -5,7 +5,7 @@ header {* Liminf and Limsup on complete lattices *} theory Liminf_Limsup -imports "~~/src/HOL/Complex_Main" +imports Complex_Main begin lemma le_Sup_iff_less: diff -r eea5c4ca4a0e -r 6f6012f430fc src/HOL/Library/Permutation.thy --- a/src/HOL/Library/Permutation.thy Tue Mar 26 20:49:57 2013 +0100 +++ b/src/HOL/Library/Permutation.thy Tue Mar 26 20:55:21 2013 +0100 @@ -5,7 +5,7 @@ header {* Permutations *} theory Permutation -imports Main Multiset +imports Multiset begin inductive diff -r eea5c4ca4a0e -r 6f6012f430fc src/HOL/Library/Phantom_Type.thy --- a/src/HOL/Library/Phantom_Type.thy Tue Mar 26 20:49:57 2013 +0100 +++ b/src/HOL/Library/Phantom_Type.thy Tue Mar 26 20:55:21 2013 +0100 @@ -4,7 +4,9 @@ header {* A generic phantom type *} -theory Phantom_Type imports Main begin +theory Phantom_Type +imports Main +begin datatype ('a, 'b) phantom = phantom 'b diff -r eea5c4ca4a0e -r 6f6012f430fc src/HOL/Library/Product_Order.thy --- a/src/HOL/Library/Product_Order.thy Tue Mar 26 20:49:57 2013 +0100 +++ b/src/HOL/Library/Product_Order.thy Tue Mar 26 20:55:21 2013 +0100 @@ -5,7 +5,7 @@ header {* Pointwise order on product types *} theory Product_Order -imports "~~/src/HOL/Library/Product_plus" +imports Product_plus begin subsection {* Pointwise ordering *} diff -r eea5c4ca4a0e -r 6f6012f430fc src/HOL/Library/Reflection.thy --- a/src/HOL/Library/Reflection.thy Tue Mar 26 20:49:57 2013 +0100 +++ b/src/HOL/Library/Reflection.thy Tue Mar 26 20:55:21 2013 +0100 @@ -8,8 +8,8 @@ imports Main begin -ML_file "~~/src/HOL/Library/reify_data.ML" -ML_file "~~/src/HOL/Library/reflection.ML" +ML_file "reify_data.ML" +ML_file "reflection.ML" setup {* Reify_Data.setup *} diff -r eea5c4ca4a0e -r 6f6012f430fc src/HOL/Library/Saturated.thy --- a/src/HOL/Library/Saturated.thy Tue Mar 26 20:49:57 2013 +0100 +++ b/src/HOL/Library/Saturated.thy Tue Mar 26 20:55:21 2013 +0100 @@ -7,7 +7,7 @@ header {* Saturated arithmetic *} theory Saturated -imports Main "~~/src/HOL/Library/Numeral_Type" "~~/src/HOL/Word/Type_Length" +imports Numeral_Type "~~/src/HOL/Word/Type_Length" begin subsection {* The type of saturated naturals *} diff -r eea5c4ca4a0e -r 6f6012f430fc src/HOL/ROOT --- a/src/HOL/ROOT Tue Mar 26 20:49:57 2013 +0100 +++ b/src/HOL/ROOT Tue Mar 26 20:55:21 2013 +0100 @@ -347,6 +347,9 @@ files "document/root.bib" "document/root.tex" session "HOL-Decision_Procs" in Decision_Procs = HOL + + description {* + Various decision procedures, typically involving reflection. + *} options [condition = ISABELLE_POLYML, document = false] theories Decision_Procs