--- 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.
--- 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 \<equiv> Q \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
by simp
@@ -174,7 +174,7 @@
done
-section {* Skolemization helpers *}
+subsection {* Skolemization helpers *}
definition skolem :: "'a \<Rightarrow> 'a" where
[no_atp]: "skolem = (\<lambda>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"
--- 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 \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> 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
--- 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 \<Rightarrow> bool)"
+lemma adm_chfin [simp]: "adm (P::'a::chfin \<Rightarrow> bool)"
by (rule admI, frule chfin, auto simp add: maxinch_is_thelub)
subsection {* Admissibility of special formulae and propagation *}
--- 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 (\<lambda>f. f x)"
-by (rule monofunI, simp add: below_fun_def)
-
text {* Properties of chains of functions. *}
lemma fun_chain_iff: "chain S \<longleftrightarrow> (\<forall>x. chain (\<lambda>i. S i x))"
@@ -158,6 +153,9 @@
apply (simp add: cont2contlubE thelub_fun ch2ch_cont)
done
+lemma cont_fun: "cont (\<lambda>f. f x)"
+using cont_id by (rule cont2cont_fun)
+
text {*
Lambda abstraction preserves monotonicity and continuity.
(Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"}.)
--- 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 (\<lambda>x. case p of (a, b) \<Rightarrow> f x a b)"
using assms by (cases p) auto
+text {* Admissibility of predicates on product types. *}
+
+lemma adm_prod_case [simp]:
+ assumes "adm (\<lambda>x. P x (fst (f x)) (snd (f x)))"
+ shows "adm (\<lambda>x. case f x of (a, b) \<Rightarrow> P x a b)"
+unfolding prod_case_beta using assms .
+
subsection {* Compactness and chain-finiteness *}
lemma fst_below_iff: "fst (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (y, snd x)"