summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | huffman |

Mon, 08 Mar 2010 08:12:48 -0800 | |

changeset 35652 | 05ca920cd94b |

parent 35651 | 5dd352a85464 |

child 35653 | f87132febfac |

move take-proofs stuff into new theory Domain_Aux.thy

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Domain_Aux.thy Mon Mar 08 08:12:48 2010 -0800 @@ -0,0 +1,50 @@ +(* Title: HOLCF/Domain_Aux.thy + Author: Brian Huffman +*) + +header {* Domain package support *} + +theory Domain_Aux +imports Ssum Sprod Fixrec +uses + ("Tools/Domain/domain_take_proofs.ML") +begin + +subsection {* Proofs about take functions *} + +text {* + This section contains lemmas that are used in a module that supports + the domain isomorphism package; the module contains proofs related + to take functions and the finiteness predicate. +*} + +lemma deflation_abs_rep: + fixes abs and rep and d + assumes abs_iso: "\<And>x. rep\<cdot>(abs\<cdot>x) = x" + assumes rep_iso: "\<And>y. abs\<cdot>(rep\<cdot>y) = y" + shows "deflation d \<Longrightarrow> deflation (abs oo d oo rep)" +by (rule ep_pair.deflation_e_d_p) (simp add: ep_pair.intro assms) + +lemma deflation_chain_min: + assumes chain: "chain d" + assumes defl: "\<And>n. deflation (d n)" + shows "d m\<cdot>(d n\<cdot>x) = d (min m n)\<cdot>x" +proof (rule linorder_le_cases) + assume "m \<le> n" + with chain have "d m \<sqsubseteq> d n" by (rule chain_mono) + then have "d m\<cdot>(d n\<cdot>x) = d m\<cdot>x" + by (rule deflation_below_comp1 [OF defl defl]) + moreover from `m \<le> n` have "min m n = m" by simp + ultimately show ?thesis by simp +next + assume "n \<le> m" + with chain have "d n \<sqsubseteq> d m" by (rule chain_mono) + then have "d m\<cdot>(d n\<cdot>x) = d n\<cdot>x" + by (rule deflation_below_comp2 [OF defl defl]) + moreover from `n \<le> m` have "min m n = n" by simp + ultimately show ?thesis by simp +qed + +use "Tools/Domain/domain_take_proofs.ML" + +end

--- a/src/HOLCF/IsaMakefile Mon Mar 08 07:37:11 2010 -0800 +++ b/src/HOLCF/IsaMakefile Mon Mar 08 08:12:48 2010 -0800 @@ -39,6 +39,7 @@ Discrete.thy \ Deflation.thy \ Domain.thy \ + Domain_Aux.thy \ Eventual.thy \ Ffun.thy \ Fixrec.thy \

--- a/src/HOLCF/Representable.thy Mon Mar 08 07:37:11 2010 -0800 +++ b/src/HOLCF/Representable.thy Mon Mar 08 08:12:48 2010 -0800 @@ -5,51 +5,12 @@ header {* Representable Types *} theory Representable -imports Algebraic Universal Ssum Sprod One Fixrec +imports Algebraic Universal Ssum Sprod One Fixrec Domain_Aux uses ("Tools/repdef.ML") - ("Tools/Domain/domain_take_proofs.ML") ("Tools/Domain/domain_isomorphism.ML") begin -subsection {* Preliminaries: Take proofs *} - -text {* - This section contains lemmas that are used in a module that supports - the domain isomorphism package; the module contains proofs related - to take functions and the finiteness predicate. -*} - -lemma deflation_abs_rep: - fixes abs and rep and d - assumes abs_iso: "\<And>x. rep\<cdot>(abs\<cdot>x) = x" - assumes rep_iso: "\<And>y. abs\<cdot>(rep\<cdot>y) = y" - shows "deflation d \<Longrightarrow> deflation (abs oo d oo rep)" -by (rule ep_pair.deflation_e_d_p) (simp add: ep_pair.intro assms) - -lemma deflation_chain_min: - assumes chain: "chain d" - assumes defl: "\<And>n. deflation (d n)" - shows "d m\<cdot>(d n\<cdot>x) = d (min m n)\<cdot>x" -proof (rule linorder_le_cases) - assume "m \<le> n" - with chain have "d m \<sqsubseteq> d n" by (rule chain_mono) - then have "d m\<cdot>(d n\<cdot>x) = d m\<cdot>x" - by (rule deflation_below_comp1 [OF defl defl]) - moreover from `m \<le> n` have "min m n = m" by simp - ultimately show ?thesis by simp -next - assume "n \<le> m" - with chain have "d n \<sqsubseteq> d m" by (rule chain_mono) - then have "d m\<cdot>(d n\<cdot>x) = d n\<cdot>x" - by (rule deflation_below_comp2 [OF defl defl]) - moreover from `n \<le> m` have "min m n = n" by simp - ultimately show ?thesis by simp -qed - -use "Tools/Domain/domain_take_proofs.ML" - - subsection {* Class of representable types *} text "Overloaded embedding and projection functions between