merged
authorhaftmann
Fri Mar 27 10:12:55 2009 +0100 (2009-03-27)
changeset 307419e23e3ea7edd
parent 30736 f5d9cc53f4c8
parent 30740 2d3ae5a7edb2
child 30742 3e89ac3905b9
merged
NEWS
src/HOL/Decision_Procs/Dense_Linear_Order.thy
src/HOL/Library/SetsAndFunctions.thy
src/HOL/ex/Code_Antiq.thy
     1.1 --- a/NEWS	Fri Mar 27 09:58:48 2009 +0100
     1.2 +++ b/NEWS	Fri Mar 27 10:12:55 2009 +0100
     1.3 @@ -502,10 +502,9 @@
     1.4  resulting ML value/function/datatype constructor binding in place.
     1.5  All occurrences of @{code} with a single ML block are generated
     1.6  simultaneously.  Provides a generic and safe interface for
     1.7 -instrumentalizing code generation.  See HOL/ex/Code_Antiq for a toy
     1.8 -example, or HOL/Complex/ex/ReflectedFerrack for a more ambitious
     1.9 -application.  In future you ought refrain from ad-hoc compiling
    1.10 -generated SML code on the ML toplevel.  Note that (for technical
    1.11 +instrumentalizing code generation.  See HOL/Decision_Procs/Ferrack for
    1.12 +a more ambitious application.  In future you ought refrain from ad-hoc
    1.13 +compiling generated SML code on the ML toplevel.  Note that (for technical
    1.14  reasons) @{code} cannot refer to constants for which user-defined
    1.15  serializations are set.  Refer to the corresponding ML counterpart
    1.16  directly in that cases.
     2.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Fri Mar 27 09:58:48 2009 +0100
     2.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Fri Mar 27 10:12:55 2009 +0100
     2.3 @@ -6,7 +6,7 @@
     2.4    and a quantifier elimination procedure in Ferrante and Rackoff style *}
     2.5  
     2.6  theory Dense_Linear_Order
     2.7 -imports Plain Groebner_Basis Main
     2.8 +imports Main
     2.9  uses
    2.10    "~~/src/HOL/Tools/Qelim/langford_data.ML"
    2.11    "~~/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML"
     3.1 --- a/src/HOL/GCD.thy	Fri Mar 27 09:58:48 2009 +0100
     3.2 +++ b/src/HOL/GCD.thy	Fri Mar 27 10:12:55 2009 +0100
     3.3 @@ -6,7 +6,7 @@
     3.4  header {* The Greatest Common Divisor *}
     3.5  
     3.6  theory GCD
     3.7 -imports Plain Presburger Main
     3.8 +imports Main
     3.9  begin
    3.10  
    3.11  text {*
     4.1 --- a/src/HOL/Imperative_HOL/Heap.thy	Fri Mar 27 09:58:48 2009 +0100
     4.2 +++ b/src/HOL/Imperative_HOL/Heap.thy	Fri Mar 27 10:12:55 2009 +0100
     4.3 @@ -1,12 +1,11 @@
     4.4  (*  Title:      HOL/Library/Heap.thy
     4.5 -    ID:         $Id$
     4.6      Author:     John Matthews, Galois Connections; Alexander Krauss, TU Muenchen
     4.7  *)
     4.8  
     4.9  header {* A polymorphic heap based on cantor encodings *}
    4.10  
    4.11  theory Heap
    4.12 -imports Plain "~~/src/HOL/List" Countable Typerep
    4.13 +imports Main Countable
    4.14  begin
    4.15  
    4.16  subsection {* Representable types *}
     5.1 --- a/src/HOL/Library/Permutation.thy	Fri Mar 27 09:58:48 2009 +0100
     5.2 +++ b/src/HOL/Library/Permutation.thy	Fri Mar 27 10:12:55 2009 +0100
     5.3 @@ -5,7 +5,7 @@
     5.4  header {* Permutations *}
     5.5  
     5.6  theory Permutation
     5.7 -imports Plain Multiset
     5.8 +imports Main Multiset
     5.9  begin
    5.10  
    5.11  inductive
     6.1 --- a/src/HOL/Library/Pocklington.thy	Fri Mar 27 09:58:48 2009 +0100
     6.2 +++ b/src/HOL/Library/Pocklington.thy	Fri Mar 27 10:12:55 2009 +0100
     6.3 @@ -1,13 +1,11 @@
     6.4  (*  Title:      HOL/Library/Pocklington.thy
     6.5 -    ID:         $Id$
     6.6      Author:     Amine Chaieb
     6.7  *)
     6.8  
     6.9  header {* Pocklington's Theorem for Primes *}
    6.10  
    6.11 -
    6.12  theory Pocklington
    6.13 -imports Plain "~~/src/HOL/List" "~~/src/HOL/Primes"
    6.14 +imports Main Primes
    6.15  begin
    6.16  
    6.17  definition modeq:: "nat => nat => nat => bool"    ("(1[_ = _] '(mod _'))")
     7.1 --- a/src/HOL/Library/Polynomial.thy	Fri Mar 27 09:58:48 2009 +0100
     7.2 +++ b/src/HOL/Library/Polynomial.thy	Fri Mar 27 10:12:55 2009 +0100
     7.3 @@ -6,7 +6,7 @@
     7.4  header {* Univariate Polynomials *}
     7.5  
     7.6  theory Polynomial
     7.7 -imports Plain SetInterval Main
     7.8 +imports Main
     7.9  begin
    7.10  
    7.11  subsection {* Definition of type @{text poly} *}
     8.1 --- a/src/HOL/Library/Primes.thy	Fri Mar 27 09:58:48 2009 +0100
     8.2 +++ b/src/HOL/Library/Primes.thy	Fri Mar 27 10:12:55 2009 +0100
     8.3 @@ -6,7 +6,7 @@
     8.4  header {* Primality on nat *}
     8.5  
     8.6  theory Primes
     8.7 -imports Plain "~~/src/HOL/ATP_Linkup" "~~/src/HOL/GCD" "~~/src/HOL/Parity"
     8.8 +imports Complex_Main
     8.9  begin
    8.10  
    8.11  definition
     9.1 --- a/src/HOL/Library/Product_ord.thy	Fri Mar 27 09:58:48 2009 +0100
     9.2 +++ b/src/HOL/Library/Product_ord.thy	Fri Mar 27 10:12:55 2009 +0100
     9.3 @@ -1,12 +1,11 @@
     9.4  (*  Title:      HOL/Library/Product_ord.thy
     9.5 -    ID:         $Id$
     9.6      Author:     Norbert Voelker
     9.7  *)
     9.8  
     9.9  header {* Order on product types *}
    9.10  
    9.11  theory Product_ord
    9.12 -imports Plain
    9.13 +imports Main
    9.14  begin
    9.15  
    9.16  instantiation "*" :: (ord, ord) ord
    10.1 --- a/src/HOL/Library/Quicksort.thy	Fri Mar 27 09:58:48 2009 +0100
    10.2 +++ b/src/HOL/Library/Quicksort.thy	Fri Mar 27 10:12:55 2009 +0100
    10.3 @@ -1,12 +1,11 @@
    10.4 -(*  ID:         $Id$
    10.5 -    Author:     Tobias Nipkow
    10.6 +(*  Author:     Tobias Nipkow
    10.7      Copyright   1994 TU Muenchen
    10.8  *)
    10.9  
   10.10  header{*Quicksort*}
   10.11  
   10.12  theory Quicksort
   10.13 -imports Plain Multiset
   10.14 +imports Main Multiset
   10.15  begin
   10.16  
   10.17  context linorder
    11.1 --- a/src/HOL/Library/Quotient.thy	Fri Mar 27 09:58:48 2009 +0100
    11.2 +++ b/src/HOL/Library/Quotient.thy	Fri Mar 27 10:12:55 2009 +0100
    11.3 @@ -1,12 +1,11 @@
    11.4  (*  Title:      HOL/Library/Quotient.thy
    11.5 -    ID:         $Id$
    11.6      Author:     Markus Wenzel, TU Muenchen
    11.7  *)
    11.8  
    11.9  header {* Quotient types *}
   11.10  
   11.11  theory Quotient
   11.12 -imports Plain "~~/src/HOL/Hilbert_Choice"
   11.13 +imports Main
   11.14  begin
   11.15  
   11.16  text {*
    12.1 --- a/src/HOL/Library/RBT.thy	Fri Mar 27 09:58:48 2009 +0100
    12.2 +++ b/src/HOL/Library/RBT.thy	Fri Mar 27 10:12:55 2009 +0100
    12.3 @@ -1,5 +1,4 @@
    12.4  (*  Title:      RBT.thy
    12.5 -    ID:         $Id$
    12.6      Author:     Markus Reiter, TU Muenchen
    12.7      Author:     Alexander Krauss, TU Muenchen
    12.8  *)
    12.9 @@ -8,7 +7,7 @@
   12.10  
   12.11  (*<*)
   12.12  theory RBT
   12.13 -imports Plain AssocList
   12.14 +imports Main AssocList
   12.15  begin
   12.16  
   12.17  datatype color = R | B
    13.1 --- a/src/HOL/Library/Ramsey.thy	Fri Mar 27 09:58:48 2009 +0100
    13.2 +++ b/src/HOL/Library/Ramsey.thy	Fri Mar 27 10:12:55 2009 +0100
    13.3 @@ -1,12 +1,11 @@
    13.4  (*  Title:      HOL/Library/Ramsey.thy
    13.5 -    ID:         $Id$
    13.6      Author:     Tom Ridge. Converted to structured Isar by L C Paulson
    13.7  *)
    13.8  
    13.9  header "Ramsey's Theorem"
   13.10  
   13.11  theory Ramsey
   13.12 -imports Plain "~~/src/HOL/Presburger" Infinite_Set
   13.13 +imports Main Infinite_Set
   13.14  begin
   13.15  
   13.16  subsection {* Preliminaries *}
    14.1 --- a/src/HOL/Library/SetsAndFunctions.thy	Fri Mar 27 09:58:48 2009 +0100
    14.2 +++ b/src/HOL/Library/SetsAndFunctions.thy	Fri Mar 27 10:12:55 2009 +0100
    14.3 @@ -5,7 +5,7 @@
    14.4  header {* Operations on sets and functions *}
    14.5  
    14.6  theory SetsAndFunctions
    14.7 -imports Plain
    14.8 +imports Main
    14.9  begin
   14.10  
   14.11  text {*
    15.1 --- a/src/HOL/Library/State_Monad.thy	Fri Mar 27 09:58:48 2009 +0100
    15.2 +++ b/src/HOL/Library/State_Monad.thy	Fri Mar 27 10:12:55 2009 +0100
    15.3 @@ -5,7 +5,7 @@
    15.4  header {* Combinator syntax for generic, open state monads (single threaded monads) *}
    15.5  
    15.6  theory State_Monad
    15.7 -imports Plain "~~/src/HOL/List"
    15.8 +imports Main
    15.9  begin
   15.10  
   15.11  subsection {* Motivation *}
    16.1 --- a/src/HOL/Library/Sublist_Order.thy	Fri Mar 27 09:58:48 2009 +0100
    16.2 +++ b/src/HOL/Library/Sublist_Order.thy	Fri Mar 27 10:12:55 2009 +0100
    16.3 @@ -1,13 +1,12 @@
    16.4  (*  Title:      HOL/Library/Sublist_Order.thy
    16.5 -    ID:         $Id$
    16.6      Authors:    Peter Lammich, Uni Muenster <peter.lammich@uni-muenster.de>
    16.7 -                Florian Haftmann, TU M√ľnchen
    16.8 +                Florian Haftmann, TU Muenchen
    16.9  *)
   16.10  
   16.11  header {* Sublist Ordering *}
   16.12  
   16.13  theory Sublist_Order
   16.14 -imports Plain "~~/src/HOL/List"
   16.15 +imports Main
   16.16  begin
   16.17  
   16.18  text {*
    17.1 --- a/src/HOL/Library/Univ_Poly.thy	Fri Mar 27 09:58:48 2009 +0100
    17.2 +++ b/src/HOL/Library/Univ_Poly.thy	Fri Mar 27 10:12:55 2009 +0100
    17.3 @@ -5,7 +5,7 @@
    17.4  header {* Univariate Polynomials *}
    17.5  
    17.6  theory Univ_Poly
    17.7 -imports Plain List
    17.8 +imports Main
    17.9  begin
   17.10  
   17.11  text{* Application of polynomial as a function. *}
    18.1 --- a/src/HOL/Library/While_Combinator.thy	Fri Mar 27 09:58:48 2009 +0100
    18.2 +++ b/src/HOL/Library/While_Combinator.thy	Fri Mar 27 10:12:55 2009 +0100
    18.3 @@ -1,5 +1,4 @@
    18.4  (*  Title:      HOL/Library/While_Combinator.thy
    18.5 -    ID:         $Id$
    18.6      Author:     Tobias Nipkow
    18.7      Copyright   2000 TU Muenchen
    18.8  *)
    18.9 @@ -7,7 +6,7 @@
   18.10  header {* A general ``while'' combinator *}
   18.11  
   18.12  theory While_Combinator
   18.13 -imports Plain "~~/src/HOL/Presburger"
   18.14 +imports Main
   18.15  begin
   18.16  
   18.17  text {* 
    19.1 --- a/src/HOL/Lubs.thy	Fri Mar 27 09:58:48 2009 +0100
    19.2 +++ b/src/HOL/Lubs.thy	Fri Mar 27 10:12:55 2009 +0100
    19.3 @@ -6,7 +6,7 @@
    19.4  header{*Definitions of Upper Bounds and Least Upper Bounds*}
    19.5  
    19.6  theory Lubs
    19.7 -imports Plain Main
    19.8 +imports Main
    19.9  begin
   19.10  
   19.11  text{*Thanks to suggestions by James Margetson*}
    20.1 --- a/src/HOL/Map.thy	Fri Mar 27 09:58:48 2009 +0100
    20.2 +++ b/src/HOL/Map.thy	Fri Mar 27 10:12:55 2009 +0100
    20.3 @@ -1,5 +1,4 @@
    20.4  (*  Title:      HOL/Map.thy
    20.5 -    ID:         $Id$
    20.6      Author:     Tobias Nipkow, based on a theory by David von Oheimb
    20.7      Copyright   1997-2003 TU Muenchen
    20.8  
    21.1 --- a/src/HOL/Parity.thy	Fri Mar 27 09:58:48 2009 +0100
    21.2 +++ b/src/HOL/Parity.thy	Fri Mar 27 10:12:55 2009 +0100
    21.3 @@ -5,7 +5,7 @@
    21.4  header {* Even and Odd for int and nat *}
    21.5  
    21.6  theory Parity
    21.7 -imports Plain Presburger Main
    21.8 +imports Main
    21.9  begin
   21.10  
   21.11  class even_odd = 
    22.1 --- a/src/HOL/Tools/TFL/post.ML	Fri Mar 27 09:58:48 2009 +0100
    22.2 +++ b/src/HOL/Tools/TFL/post.ML	Fri Mar 27 10:12:55 2009 +0100
    22.3 @@ -79,10 +79,7 @@
    22.4     in lhs aconv rhs end
    22.5     handle U.ERR _ => false;
    22.6     
    22.7 -
    22.8 -fun prover s = prove_goal @{theory HOL} s (fn _ => [fast_tac HOL_cs 1]);
    22.9 -val P_imp_P_iff_True = prover "P --> (P= True)" RS mp;
   22.10 -val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection;
   22.11 +val P_imp_P_eq_True = @{thm eqTrueI} RS eq_reflection;
   22.12  fun mk_meta_eq r = case concl_of r of
   22.13       Const("==",_)$_$_ => r
   22.14    |   _ $(Const("op =",_)$_$_) => r RS eq_reflection
    23.1 --- a/src/HOL/ex/Code_Antiq.thy	Fri Mar 27 09:58:48 2009 +0100
    23.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    23.3 @@ -1,84 +0,0 @@
    23.4 -(*  Title:      HOL/ex/Code_Antiq.thy
    23.5 -    ID:         $Id$
    23.6 -    Author:     Florian Haftmann
    23.7 -*)
    23.8 -
    23.9 -header {* A simple certificate check as toy example for the code antiquotation *}
   23.10 -
   23.11 -theory Code_Antiq
   23.12 -imports Plain
   23.13 -begin
   23.14 -
   23.15 -lemma div_cert1:
   23.16 -  fixes n m q r :: nat
   23.17 -  assumes "r < m"
   23.18 -    and "0 < m"
   23.19 -    and "n = m * q + r"
   23.20 -  shows "n div m = q"
   23.21 -using assms by (simp add: div_mult_self2 add_commute)
   23.22 -
   23.23 -lemma div_cert2:
   23.24 -  fixes n :: nat
   23.25 -  shows "n div 0 = 0"
   23.26 -by simp
   23.27 -
   23.28 -ML {*
   23.29 -local
   23.30 -
   23.31 -fun code_of_val k = if k <= 0 then @{code "0::nat"}
   23.32 -  else @{code Suc} (code_of_val (k - 1));
   23.33 -
   23.34 -fun val_of_code @{code "0::nat"} = 0
   23.35 -  | val_of_code (@{code Suc} n) = val_of_code n + 1;
   23.36 -
   23.37 -val term_of_code = HOLogic.mk_nat o val_of_code;
   23.38 -
   23.39 -infix 9 &$;
   23.40 -val op &$ = uncurry Thm.capply;
   23.41 -
   23.42 -val simpset = HOL_ss addsimps
   23.43 -  @{thms plus_nat.simps add_0_right add_Suc_right times_nat.simps mult_0_right mult_Suc_right  less_nat_zero_code le_simps(2) less_eq_nat.simps(1) le_simps(3)}
   23.44 -
   23.45 -fun prove prop = Goal.prove_internal [] (@{cterm Trueprop} &$ prop)
   23.46 -  (K (ALLGOALS (Simplifier.simp_tac simpset))); (*FIXME*)
   23.47 -
   23.48 -in
   23.49 -
   23.50 -fun simp_div ctxt ct_n ct_m =
   23.51 -  let
   23.52 -    val m = HOLogic.dest_nat (Thm.term_of ct_m);
   23.53 -  in if m = 0 then Drule.instantiate'[] [SOME ct_n] @{thm div_cert2} else
   23.54 -    let
   23.55 -      val thy = ProofContext.theory_of ctxt;
   23.56 -      val n = HOLogic.dest_nat (Thm.term_of ct_n);
   23.57 -      val c_n = code_of_val n;
   23.58 -      val c_m = code_of_val m;
   23.59 -      val (c_q, c_r) = @{code divmod} c_n c_m;
   23.60 -      val t_q = term_of_code c_q;
   23.61 -      val t_r = term_of_code c_r;
   23.62 -      val ct_q = Thm.cterm_of thy t_q;
   23.63 -      val ct_r = Thm.cterm_of thy t_r;
   23.64 -      val thm_r = prove (@{cterm "op < \<Colon> nat \<Rightarrow> _"} &$ ct_r &$ ct_m);
   23.65 -      val thm_m = prove (@{cterm "(op < \<Colon> nat \<Rightarrow> _) 0"} &$ ct_m);
   23.66 -      val thm_n = prove (@{cterm "(op = \<Colon> nat \<Rightarrow> _)"} &$ ct_n
   23.67 -        &$ (@{cterm "(op + \<Colon> nat \<Rightarrow> _)"}
   23.68 -          &$ (@{cterm "(op * \<Colon> nat \<Rightarrow> _)"} &$ ct_m &$ ct_q) &$ ct_r));
   23.69 -    in @{thm div_cert1} OF [thm_r, thm_m, thm_n] end
   23.70 -  end;
   23.71 -
   23.72 -end;
   23.73 -*}
   23.74 -
   23.75 -ML_val {*
   23.76 -  simp_div @{context}
   23.77 -    @{cterm "Suc (Suc (Suc (Suc (Suc 0))))"}
   23.78 -    @{cterm "(Suc (Suc 0))"}
   23.79 -*}
   23.80 -
   23.81 -ML_val {*
   23.82 -  simp_div @{context}
   23.83 -    (Thm.cterm_of @{theory} (HOLogic.mk_nat 170))
   23.84 -    (Thm.cterm_of @{theory} (HOLogic.mk_nat 42))
   23.85 -*}
   23.86 -
   23.87 -end
   23.88 \ No newline at end of file
    24.1 --- a/src/HOL/ex/ROOT.ML	Fri Mar 27 09:58:48 2009 +0100
    24.2 +++ b/src/HOL/ex/ROOT.ML	Fri Mar 27 10:12:55 2009 +0100
    24.3 @@ -56,7 +56,6 @@
    24.4    "Classical",
    24.5    "set",
    24.6    "Meson_Test",
    24.7 -  "Code_Antiq",
    24.8    "Termination",
    24.9    "Coherent",
   24.10    "PresburgerEx",
    25.1 --- a/src/Pure/Isar/code_unit.ML	Fri Mar 27 09:58:48 2009 +0100
    25.2 +++ b/src/Pure/Isar/code_unit.ML	Fri Mar 27 10:12:55 2009 +0100
    25.3 @@ -215,9 +215,10 @@
    25.4            |> Conjunction.elim_balanced (length thms)
    25.5    in
    25.6      thms
    25.7 -    |> burrow_thms (canonical_tvars thy purify_tvar)
    25.8      |> map (canonical_vars thy purify_var)
    25.9      |> map (canonical_absvars purify_var)
   25.10 +    |> map Drule.zero_var_indexes
   25.11 +    |> burrow_thms (canonical_tvars thy purify_tvar)
   25.12      |> Drule.zero_var_indexes_list
   25.13    end;
   25.14