--- 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"
--- 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
--- 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
--- 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
--- 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
--- 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 *}
--- 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)
--- 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}"
--- 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
--- 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 *}
--- 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 \<le> 1" "4*y^2 \<le> 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 \<le> 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 \<le> 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) \<le> 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 \<noteq> 0"
using s pne by auto
{assume ds0: "degree s = 0"
- from ds0 have "\<exists>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 \<noteq> 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: "\<And>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 \<noteq> 0"
{assume dp: "degree p = 0"
then obtain k where k: "p = [:k:]" "k\<noteq>0" using pe
- by (cases p, simp split: if_splits)
+ by (cases p) (simp split: if_splits)
hence th1: "\<forall>x. poly p x \<noteq> 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 \<equiv> ?rhs" by - (atomize(full), blast)
@@ -1056,7 +1051,7 @@
proof-
have "p = 0 \<longleftrightarrow> poly p = poly 0"
by (simp add: poly_zero)
- also have "\<dots> \<longleftrightarrow> (\<not> (\<exists>x. poly p x \<noteq> 0))" by (auto intro: ext)
+ also have "\<dots> \<longleftrightarrow> (\<not> (\<exists>x. poly p x \<noteq> 0))" by auto
finally show "(\<exists>x. poly p x \<noteq> (0::complex)) \<equiv> p \<noteq> 0"
by - (atomize (full), blast)
qed
@@ -1078,7 +1073,7 @@
assumes h: "\<And>x. poly (q ^ n) x \<equiv> poly r x"
shows "p dvd (q ^ n) \<equiv> 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) \<equiv> p dvd r" by simp
qed
--- 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
--- 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:
--- 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
--- 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
--- 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 *}
--- 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 *}
--- 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 *}
--- 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