huffman@35652

1 
(* Title: HOLCF/Domain_Aux.thy

huffman@35652

2 
Author: Brian Huffman

huffman@35652

3 
*)

huffman@35652

4 

huffman@35652

5 
header {* Domain package support *}

huffman@35652

6 

huffman@35652

7 
theory Domain_Aux

huffman@35652

8 
imports Ssum Sprod Fixrec

huffman@35652

9 
uses

huffman@35652

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

huffman@35652

11 
begin

huffman@35652

12 

huffman@35652

13 
subsection {* Proofs about take functions *}

huffman@35652

14 

huffman@35652

15 
text {*

huffman@35652

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

huffman@35652

17 
the domain isomorphism package; the module contains proofs related

huffman@35652

18 
to take functions and the finiteness predicate.

huffman@35652

19 
*}

huffman@35652

20 

huffman@35652

21 
lemma deflation_abs_rep:

huffman@35652

22 
fixes abs and rep and d

huffman@35652

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

huffman@35652

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

huffman@35652

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

huffman@35652

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

huffman@35652

27 

huffman@35652

28 
lemma deflation_chain_min:

huffman@35652

29 
assumes chain: "chain d"

huffman@35652

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

huffman@35652

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

huffman@35652

32 
proof (rule linorder_le_cases)

huffman@35652

33 
assume "m \<le> n"

huffman@35652

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

huffman@35652

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

huffman@35652

36 
by (rule deflation_below_comp1 [OF defl defl])

huffman@35652

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

huffman@35652

38 
ultimately show ?thesis by simp

huffman@35652

39 
next

huffman@35652

40 
assume "n \<le> m"

huffman@35652

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

huffman@35652

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

huffman@35652

43 
by (rule deflation_below_comp2 [OF defl defl])

huffman@35652

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

huffman@35652

45 
ultimately show ?thesis by simp

huffman@35652

46 
qed

huffman@35652

47 

huffman@35652

48 
use "Tools/Domain/domain_take_proofs.ML"

huffman@35652

49 

huffman@35652

50 
end
