src/HOLCF/Domain_Aux.thy
author huffman
Mon Mar 08 08:12:48 2010 -0800 (2010-03-08)
changeset 35652 05ca920cd94b
child 35653 f87132febfac
permissions -rw-r--r--
move take-proofs stuff into new theory Domain_Aux.thy
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