merged
authorhuffman
Fri, 19 Nov 2010 09:07:23 -0800
changeset 40624 2df58ba31be7
parent 40623 dafba3a1dc5b (diff)
parent 40618 7202d63bfffe (current diff)
child 40625 2d9222a2239d
merged
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.
--- 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)"