# HG changeset patch # User huffman # Date 1290186443 28800 # Node ID 2df58ba31be7cfbd855b87a5ab62b51b98e96c99 # Parent dafba3a1dc5b4d65d98aaf424bf0a6538181a4c2# Parent 7202d63bfffefd789821d8fea76d5992011f1ad2 merged diff -r 7202d63bfffe -r 2df58ba31be7 NEWS --- a/NEWS Fri Nov 19 14:59:11 2010 +0000 +++ b/NEWS Fri Nov 19 09:07:23 2010 -0800 @@ -363,6 +363,121 @@ * Removed [split_format ... and ... and ...] version of [split_format]. Potential INCOMPATIBILITY. + +*** HOLCF *** + +* The domain package now runs in definitional mode by default: The +former command 'new_domain' is now called 'domain'. To use the domain +package in its original axiomatic mode, use 'domain (unsafe)'. +INCOMPATIBILITY. + +* The new class 'domain' is now the default sort; the definitional +domain package and the powerdomain theories both require this class. +The new class 'predomain' is an unpointed version of 'domain'. +Theories can be updated by replacing sort annotations as shown below. +INCOMPATIBILITY. + + 'a::type ~> 'a::countable + 'a::cpo ~> 'a::predomain + 'a::pcpo ~> 'a::domain + +* The old type class 'rep' has been superseded by class 'domain'. +Accordingly, users of the definitional package must remove any +'default_sort rep' declarations. INCOMPATIBILITY. + +* The old type classes 'profinite' and 'bifinite', along with the +overloaded constant 'approx' have been removed. INCOMPATIBILITY. + +* The type 'udom alg_defl' has been replaced by the non-parameterized +type 'defl'. HOLCF no longer defines an embedding of type defl into +udom by default; the instance proof defl :: domain is now available in +HOLCF/Library/Defl_Bifinite.thy. + +* The syntax 'REP('a)' has been replaced with 'DEFL('a)'. + +* The predicate 'directed' has been removed. INCOMPATIBILITY. + +* The type class 'finite_po' has been removed. INCOMPATIBILITY. + +* Renamed some theorems (the original names are also still available). + expand_fun_below ~> fun_below_iff + below_fun_ext ~> fun_belowI + expand_cfun_eq ~> cfun_eq_iff + ext_cfun ~> cfun_eqI + expand_cfun_below ~> cfun_below_iff + below_cfun_ext ~> cfun_belowI + cont2cont_Rep_CFun ~> cont2cont_APP + +* The Abs and Rep functions for various types have changed names. +Related theorem names have also changed to match. INCOMPATIBILITY. + Rep_CFun ~> Rep_cfun + Abs_CFun ~> Abs_cfun + Rep_Sprod ~> Rep_sprod + Abs_Sprod ~> Abs_sprod + Rep_Ssum ~> Rep_ssum + Abs_Ssum ~> Abs_ssum + +* Lemmas with names of the form *_defined_iff or *_strict_iff have +been renamed to *_bottom_iff. INCOMPATIBILITY. + +* Various changes to bisimulation/coinduction with domain package: + - Definitions of 'bisim' constants no longer mention definedness. + - With mutual recursion, 'bisim' predicate is now curried. + - With mutual recursion, each type gets a separate coind theorem. + - Variable names in bisim_def and coinduct rules have changed. +INCOMPATIBILITY. + +* Case combinators generated by the domain package for type 'foo' +are now named 'foo_case' instead of 'foo_when'. INCOMPATIBILITY. + +* Many legacy theorem names have been discontinued. INCOMPATIBILITY. + sq_ord_less_eq_trans ~> below_eq_trans + sq_ord_eq_less_trans ~> eq_below_trans + refl_less ~> below_refl + trans_less ~> below_trans + antisym_less ~> below_antisym + antisym_less_inverse ~> po_eq_conv [THEN iffD1] + box_less ~> box_below + rev_trans_less ~> rev_below_trans + not_less2not_eq ~> not_below2not_eq + less_UU_iff ~> below_UU_iff + flat_less_iff ~> flat_below_iff + adm_less ~> adm_below + adm_not_less ~> adm_not_below + adm_compact_not_less ~> adm_compact_not_below + less_fun_def ~> below_fun_def + expand_fun_less ~> fun_below_iff + less_fun_ext ~> fun_belowI + less_discr_def ~> below_discr_def + discr_less_eq ~> discr_below_eq + less_unit_def ~> below_unit_def + less_cprod_def ~> below_prod_def + prod_lessI ~> prod_belowI + Pair_less_iff ~> Pair_below_iff + fst_less_iff ~> fst_below_iff + snd_less_iff ~> snd_below_iff + expand_cfun_less ~> cfun_below_iff + less_cfun_ext ~> cfun_belowI + injection_less ~> injection_below + less_up_def ~> below_up_def + not_Iup_less ~> not_Iup_below + Iup_less ~> Iup_below + up_less ~> up_below + Def_inject_less_eq ~> Def_below_Def + Def_less_is_eq ~> Def_below_iff + spair_less_iff ~> spair_below_iff + less_sprod ~> below_sprod + spair_less ~> spair_below + sfst_less_iff ~> sfst_below_iff + ssnd_less_iff ~> ssnd_below_iff + fix_least_less ~> fix_least_below + dist_less_one ~> dist_below_one + less_ONE ~> below_ONE + ONE_less_iff ~> ONE_below_iff + less_sinlD ~> below_sinlD + less_sinrD ~> below_sinrD + + *** FOL *** * All constant names are now qualified. INCOMPATIBILITY. diff -r 7202d63bfffe -r 2df58ba31be7 src/HOL/Meson.thy --- a/src/HOL/Meson.thy Fri Nov 19 14:59:11 2010 +0000 +++ b/src/HOL/Meson.thy Fri Nov 19 09:07:23 2010 -0800 @@ -14,7 +14,7 @@ ("Tools/Meson/meson_tactic.ML") begin -section {* Negation Normal Form *} +subsection {* Negation Normal Form *} text {* de Morgan laws *} @@ -37,7 +37,7 @@ by fast+ -section {* Pulling out the existential quantifiers *} +subsection {* Pulling out the existential quantifiers *} text {* Conjunction *} @@ -95,7 +95,7 @@ by blast -section {* Lemmas for Forward Proof *} +subsection {* Lemmas for Forward Proof *} text{*There is a similarity to congruence rules*} @@ -120,7 +120,7 @@ by blast -section {* Clausification helper *} +subsection {* Clausification helper *} lemma TruepropI: "P \ Q \ Trueprop P \ Trueprop Q" by simp @@ -174,7 +174,7 @@ done -section {* Skolemization helpers *} +subsection {* Skolemization helpers *} definition skolem :: "'a \ 'a" where [no_atp]: "skolem = (\x. x)" @@ -186,7 +186,7 @@ lemmas skolem_COMBK_D = iffD2 [OF skolem_COMBK_iff] -section {* Meson package *} +subsection {* Meson package *} use "Tools/Meson/meson.ML" use "Tools/Meson/meson_clausify.ML" diff -r 7202d63bfffe -r 2df58ba31be7 src/HOL/Smallcheck.thy --- a/src/HOL/Smallcheck.thy Fri Nov 19 14:59:11 2010 +0000 +++ b/src/HOL/Smallcheck.thy Fri Nov 19 09:07:23 2010 -0800 @@ -8,7 +8,7 @@ begin -section {* small value generator type classes *} +subsection {* small value generator type classes *} class small = term_of + fixes small :: "('a \ term list option) \ code_numeral \ term list option" @@ -48,7 +48,7 @@ end -section {* Defining combinators for any first-order data type *} +subsection {* Defining combinators for any first-order data type *} definition catch_match :: "term list option => term list option => term list option" where diff -r 7202d63bfffe -r 2df58ba31be7 src/HOLCF/Adm.thy --- a/src/HOLCF/Adm.thy Fri Nov 19 14:59:11 2010 +0000 +++ b/src/HOLCF/Adm.thy Fri Nov 19 09:07:23 2010 -0800 @@ -31,9 +31,9 @@ subsection {* Admissibility on chain-finite types *} -text {* for chain-finite (easy) types every formula is admissible *} +text {* For chain-finite (easy) types every formula is admissible. *} -lemma adm_chfin: "adm (P::'a::chfin \ bool)" +lemma adm_chfin [simp]: "adm (P::'a::chfin \ bool)" by (rule admI, frule chfin, auto simp add: maxinch_is_thelub) subsection {* Admissibility of special formulae and propagation *} diff -r 7202d63bfffe -r 2df58ba31be7 src/HOLCF/Fun_Cpo.thy --- a/src/HOLCF/Fun_Cpo.thy Fri Nov 19 14:59:11 2010 +0000 +++ b/src/HOLCF/Fun_Cpo.thy Fri Nov 19 09:07:23 2010 -0800 @@ -46,11 +46,6 @@ subsection {* Full function space is chain complete *} -text {* Function application is monotone. *} - -lemma monofun_app: "monofun (\f. f x)" -by (rule monofunI, simp add: below_fun_def) - text {* Properties of chains of functions. *} lemma fun_chain_iff: "chain S \ (\x. chain (\i. S i x))" @@ -158,6 +153,9 @@ apply (simp add: cont2contlubE thelub_fun ch2ch_cont) done +lemma cont_fun: "cont (\f. f x)" +using cont_id by (rule cont2cont_fun) + text {* Lambda abstraction preserves monotonicity and continuity. (Note @{text "(\x. \y. f x y) = f"}.) diff -r 7202d63bfffe -r 2df58ba31be7 src/HOLCF/Product_Cpo.thy --- a/src/HOLCF/Product_Cpo.thy Fri Nov 19 14:59:11 2010 +0000 +++ b/src/HOLCF/Product_Cpo.thy Fri Nov 19 09:07:23 2010 -0800 @@ -276,6 +276,13 @@ shows "cont (\x. case p of (a, b) \ f x a b)" using assms by (cases p) auto +text {* Admissibility of predicates on product types. *} + +lemma adm_prod_case [simp]: + assumes "adm (\x. P x (fst (f x)) (snd (f x)))" + shows "adm (\x. case f x of (a, b) \ P x a b)" +unfolding prod_case_beta using assms . + subsection {* Compactness and chain-finiteness *} lemma fst_below_iff: "fst (x::'a \ 'b) \ y \ x \ (y, snd x)"