35652

1 
(* Title: HOLCF/Domain_Aux.thy


2 
Author: Brian Huffman


3 
*)


4 


5 
header {* Domain package support *}


6 


7 
theory Domain_Aux


8 
imports Ssum Sprod Fixrec


9 
uses


10 
("Tools/Domain/domain_take_proofs.ML")


11 
begin


12 


13 
subsection {* Proofs about take functions *}


14 


15 
text {*


16 
This section contains lemmas that are used in a module that supports


17 
the domain isomorphism package; the module contains proofs related


18 
to take functions and the finiteness predicate.


19 
*}


20 


21 
lemma deflation_abs_rep:


22 
fixes abs and rep and d


23 
assumes abs_iso: "\<And>x. rep\<cdot>(abs\<cdot>x) = x"


24 
assumes rep_iso: "\<And>y. abs\<cdot>(rep\<cdot>y) = y"


25 
shows "deflation d \<Longrightarrow> deflation (abs oo d oo rep)"


26 
by (rule ep_pair.deflation_e_d_p) (simp add: ep_pair.intro assms)


27 


28 
lemma deflation_chain_min:


29 
assumes chain: "chain d"


30 
assumes defl: "\<And>n. deflation (d n)"


31 
shows "d m\<cdot>(d n\<cdot>x) = d (min m n)\<cdot>x"


32 
proof (rule linorder_le_cases)


33 
assume "m \<le> n"


34 
with chain have "d m \<sqsubseteq> d n" by (rule chain_mono)


35 
then have "d m\<cdot>(d n\<cdot>x) = d m\<cdot>x"


36 
by (rule deflation_below_comp1 [OF defl defl])


37 
moreover from `m \<le> n` have "min m n = m" by simp


38 
ultimately show ?thesis by simp


39 
next


40 
assume "n \<le> m"


41 
with chain have "d n \<sqsubseteq> d m" by (rule chain_mono)


42 
then have "d m\<cdot>(d n\<cdot>x) = d n\<cdot>x"


43 
by (rule deflation_below_comp2 [OF defl defl])


44 
moreover from `n \<le> m` have "min m n = n" by simp


45 
ultimately show ?thesis by simp


46 
qed


47 


48 
use "Tools/Domain/domain_take_proofs.ML"


49 


50 
end
