merged
authorberghofe
Tue Jun 02 10:04:03 2009 +0200 (2009-06-02)
changeset 31362edf74583715a
parent 31358 3e640334a1b3
parent 31361 3e900a2acaed
child 31363 7493b571b37d
child 31371 75f38cfcf9d6
child 31375 815426e7dd3b
merged
src/HOL/IsaMakefile
src/HOL/Library/Convex_Euclidean_Space.thy
     1.1 --- a/src/HOL/IsaMakefile	Tue Jun 02 08:56:19 2009 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Jun 02 10:04:03 2009 +0200
     1.3 @@ -316,6 +316,7 @@
     1.4    Library/Abstract_Rat.thy \
     1.5    Library/BigO.thy Library/ContNotDenum.thy Library/Efficient_Nat.thy	\
     1.6    Library/Euclidean_Space.thy Library/Sum_Of_Squares.thy Library/positivstellensatz.ML	\
     1.7 +  Library/Convex_Euclidean_Space.thy \
     1.8    Library/sum_of_squares.ML Library/Glbs.thy Library/normarith.ML \
     1.9    Library/Executable_Set.thy Library/Infinite_Set.thy			\
    1.10    Library/FuncSet.thy Library/Permutations.thy Library/Determinants.thy\
     2.1 --- a/src/HOL/Library/Convex_Euclidean_Space.thy	Tue Jun 02 08:56:19 2009 +0200
     2.2 +++ b/src/HOL/Library/Convex_Euclidean_Space.thy	Tue Jun 02 10:04:03 2009 +0200
     2.3 @@ -1,6 +1,6 @@
     2.4 -(* Title:      Convex
     2.5 -   ID:         $Id: 
     2.6 -   Author:     Robert Himmelmann, TU Muenchen*)
     2.7 +(*  Title:      HOL/Library/Convex_Euclidean_Space.thy
     2.8 +    Author:     Robert Himmelmann, TU Muenchen
     2.9 +*)
    2.10  
    2.11  header {* Convex sets, functions and related things. *}
    2.12  
    2.13 @@ -2194,7 +2194,7 @@
    2.14  lemma convex_interval: "convex {a .. b}" "convex {a<..<b::real^'n::finite}"
    2.15    apply(rule_tac[!] is_interval_convex) using is_interval_interval by auto
    2.16  
    2.17 -subsection {* On real^1, is_interval, convex and connected are all equivalent. *}
    2.18 +subsection {* On @{text "real^1"}, @{text "is_interval"}, @{text "convex"} and @{text "connected"} are all equivalent. *}
    2.19  
    2.20  lemma is_interval_1:
    2.21    "is_interval s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b \<longrightarrow> x \<in> s)"
     3.1 --- a/src/HOL/Library/Library.thy	Tue Jun 02 08:56:19 2009 +0200
     3.2 +++ b/src/HOL/Library/Library.thy	Tue Jun 02 10:04:03 2009 +0200
     3.3 @@ -14,6 +14,7 @@
     3.4    Commutative_Ring
     3.5    Continuity
     3.6    ContNotDenum
     3.7 +  Convex_Euclidean_Space
     3.8    Countable
     3.9    Determinants
    3.10    Diagonalize
     4.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Jun 02 08:56:19 2009 +0200
     4.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Jun 02 10:04:03 2009 +0200
     4.3 @@ -386,7 +386,8 @@
     4.4      val (weak_case_congs, thy10) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
     4.5        descr sorts thy9;
     4.6  
     4.7 -    val dt_infos = map (make_dt_info NONE (flat descr) sorts induct reccomb_names rec_thms)
     4.8 +    val dt_infos = map
     4.9 +      (make_dt_info (SOME new_type_names) (flat descr) sorts induct reccomb_names rec_thms)
    4.10        ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~
    4.11          casedist_thms ~~ simproc_dists ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
    4.12  
    4.13 @@ -586,7 +587,7 @@
    4.14      val _ = (case duplicates (op =) (map fst new_dts) @ duplicates (op =) new_type_names of
    4.15        [] => () | dups => error ("Duplicate datatypes: " ^ commas dups));
    4.16  
    4.17 -    fun prep_dt_spec (tvs, tname, mx, constrs) (dts', constr_syntax, sorts, i) =
    4.18 +    fun prep_dt_spec ((tvs, tname, mx, constrs), tname') (dts', constr_syntax, sorts, i) =
    4.19        let
    4.20          fun prep_constr (cname, cargs, mx') (constrs, constr_syntax', sorts') =
    4.21            let
    4.22 @@ -595,7 +596,7 @@
    4.23                  [] => ()
    4.24                | vs => error ("Extra type variables on rhs: " ^ commas vs))
    4.25            in (constrs @ [((if flat_names then Sign.full_name tmp_thy else
    4.26 -                Sign.full_name_path tmp_thy (Binding.name_of tname))
    4.27 +                Sign.full_name_path tmp_thy tname')
    4.28                    (Binding.map_name (Syntax.const_name mx') cname),
    4.29                     map (dtyp_of_typ new_dts) cargs')],
    4.30                constr_syntax' @ [(cname, mx')], sorts'')
    4.31 @@ -616,7 +617,8 @@
    4.32               " in datatype " ^ quote (Binding.str_of tname))
    4.33        end;
    4.34  
    4.35 -    val (dts', constr_syntax, sorts', i) = fold prep_dt_spec dts ([], [], [], 0);
    4.36 +    val (dts', constr_syntax, sorts', i) =
    4.37 +      fold prep_dt_spec (dts ~~ new_type_names) ([], [], [], 0);
    4.38      val sorts = sorts' @ (map (rpair (Sign.defaultS tmp_thy)) (tyvars \\ map fst sorts'));
    4.39      val dt_info = get_datatypes thy;
    4.40      val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i;