src/HOLCF/Domain_Aux.thy
author huffman
Wed, 10 Nov 2010 18:15:21 -0800
changeset 40503 4094d788b904
parent 40502 8e92772bc0e8
permissions -rw-r--r--
move stuff from Domain.thy to Domain_Aux.thy
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35652
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
     1
(*  Title:      HOLCF/Domain_Aux.thy
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
     2
    Author:     Brian Huffman
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
     3
*)
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
     4
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
     5
header {* Domain package support *}
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
     6
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
     7
theory Domain_Aux
40502
8e92772bc0e8 move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents: 40327
diff changeset
     8
imports Map_Functions Fixrec
35652
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
     9
uses
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
    10
  ("Tools/Domain/domain_take_proofs.ML")
40503
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
    11
  ("Tools/cont_consts.ML")
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
    12
  ("Tools/cont_proc.ML")
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
    13
  ("Tools/Domain/domain_constructors.ML")
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
    14
  ("Tools/Domain/domain_induction.ML")
35652
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
    15
begin
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
    16
35653
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    17
subsection {* Continuous isomorphisms *}
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    18
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    19
text {* A locale for continuous isomorphisms *}
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    20
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    21
locale iso =
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    22
  fixes abs :: "'a \<rightarrow> 'b"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    23
  fixes rep :: "'b \<rightarrow> 'a"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    24
  assumes abs_iso [simp]: "rep\<cdot>(abs\<cdot>x) = x"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    25
  assumes rep_iso [simp]: "abs\<cdot>(rep\<cdot>y) = y"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    26
begin
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    27
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    28
lemma swap: "iso rep abs"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    29
  by (rule iso.intro [OF rep_iso abs_iso])
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    30
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    31
lemma abs_below: "(abs\<cdot>x \<sqsubseteq> abs\<cdot>y) = (x \<sqsubseteq> y)"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    32
proof
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    33
  assume "abs\<cdot>x \<sqsubseteq> abs\<cdot>y"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    34
  then have "rep\<cdot>(abs\<cdot>x) \<sqsubseteq> rep\<cdot>(abs\<cdot>y)" by (rule monofun_cfun_arg)
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    35
  then show "x \<sqsubseteq> y" by simp
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    36
next
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    37
  assume "x \<sqsubseteq> y"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    38
  then show "abs\<cdot>x \<sqsubseteq> abs\<cdot>y" by (rule monofun_cfun_arg)
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    39
qed
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    40
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    41
lemma rep_below: "(rep\<cdot>x \<sqsubseteq> rep\<cdot>y) = (x \<sqsubseteq> y)"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    42
  by (rule iso.abs_below [OF swap])
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    43
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    44
lemma abs_eq: "(abs\<cdot>x = abs\<cdot>y) = (x = y)"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    45
  by (simp add: po_eq_conv abs_below)
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    46
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    47
lemma rep_eq: "(rep\<cdot>x = rep\<cdot>y) = (x = y)"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    48
  by (rule iso.abs_eq [OF swap])
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    49
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    50
lemma abs_strict: "abs\<cdot>\<bottom> = \<bottom>"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    51
proof -
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    52
  have "\<bottom> \<sqsubseteq> rep\<cdot>\<bottom>" ..
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    53
  then have "abs\<cdot>\<bottom> \<sqsubseteq> abs\<cdot>(rep\<cdot>\<bottom>)" by (rule monofun_cfun_arg)
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    54
  then have "abs\<cdot>\<bottom> \<sqsubseteq> \<bottom>" by simp
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    55
  then show ?thesis by (rule UU_I)
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    56
qed
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    57
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    58
lemma rep_strict: "rep\<cdot>\<bottom> = \<bottom>"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    59
  by (rule iso.abs_strict [OF swap])
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    60
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    61
lemma abs_defin': "abs\<cdot>x = \<bottom> \<Longrightarrow> x = \<bottom>"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    62
proof -
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    63
  have "x = rep\<cdot>(abs\<cdot>x)" by simp
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    64
  also assume "abs\<cdot>x = \<bottom>"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    65
  also note rep_strict
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    66
  finally show "x = \<bottom>" .
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    67
qed
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    68
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    69
lemma rep_defin': "rep\<cdot>z = \<bottom> \<Longrightarrow> z = \<bottom>"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    70
  by (rule iso.abs_defin' [OF swap])
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    71
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    72
lemma abs_defined: "z \<noteq> \<bottom> \<Longrightarrow> abs\<cdot>z \<noteq> \<bottom>"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    73
  by (erule contrapos_nn, erule abs_defin')
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    74
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    75
lemma rep_defined: "z \<noteq> \<bottom> \<Longrightarrow> rep\<cdot>z \<noteq> \<bottom>"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    76
  by (rule iso.abs_defined [OF iso.swap]) (rule iso_axioms)
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    77
40321
d065b195ec89 rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents: 40216
diff changeset
    78
lemma abs_bottom_iff: "(abs\<cdot>x = \<bottom>) = (x = \<bottom>)"
35653
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    79
  by (auto elim: abs_defin' intro: abs_strict)
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    80
40321
d065b195ec89 rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents: 40216
diff changeset
    81
lemma rep_bottom_iff: "(rep\<cdot>x = \<bottom>) = (x = \<bottom>)"
d065b195ec89 rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents: 40216
diff changeset
    82
  by (rule iso.abs_bottom_iff [OF iso.swap]) (rule iso_axioms)
35653
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    83
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    84
lemma casedist_rule: "rep\<cdot>x = \<bottom> \<or> P \<Longrightarrow> x = \<bottom> \<or> P"
40321
d065b195ec89 rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents: 40216
diff changeset
    85
  by (simp add: rep_bottom_iff)
35653
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    86
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    87
lemma compact_abs_rev: "compact (abs\<cdot>x) \<Longrightarrow> compact x"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    88
proof (unfold compact_def)
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    89
  assume "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> y)"
40327
1dfdbd66093a renamed {Rep,Abs}_CFun to {Rep,Abs}_cfun
huffman
parents: 40321
diff changeset
    90
  with cont_Rep_cfun2
35653
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    91
  have "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> abs\<cdot>y)" by (rule adm_subst)
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    92
  then show "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" using abs_below by simp
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    93
qed
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    94
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    95
lemma compact_rep_rev: "compact (rep\<cdot>x) \<Longrightarrow> compact x"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    96
  by (rule iso.compact_abs_rev [OF iso.swap]) (rule iso_axioms)
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    97
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    98
lemma compact_abs: "compact x \<Longrightarrow> compact (abs\<cdot>x)"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
    99
  by (rule compact_rep_rev) simp
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   100
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   101
lemma compact_rep: "compact x \<Longrightarrow> compact (rep\<cdot>x)"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   102
  by (rule iso.compact_abs [OF iso.swap]) (rule iso_axioms)
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   103
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   104
lemma iso_swap: "(x = abs\<cdot>y) = (rep\<cdot>x = y)"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   105
proof
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   106
  assume "x = abs\<cdot>y"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   107
  then have "rep\<cdot>x = rep\<cdot>(abs\<cdot>y)" by simp
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   108
  then show "rep\<cdot>x = y" by simp
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   109
next
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   110
  assume "rep\<cdot>x = y"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   111
  then have "abs\<cdot>(rep\<cdot>x) = abs\<cdot>y" by simp
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   112
  then show "x = abs\<cdot>y" by simp
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   113
qed
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   114
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   115
end
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   116
35652
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   117
subsection {* Proofs about take functions *}
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   118
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   119
text {*
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   120
  This section contains lemmas that are used in a module that supports
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   121
  the domain isomorphism package; the module contains proofs related
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   122
  to take functions and the finiteness predicate.
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   123
*}
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   124
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   125
lemma deflation_abs_rep:
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   126
  fixes abs and rep and d
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   127
  assumes abs_iso: "\<And>x. rep\<cdot>(abs\<cdot>x) = x"
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   128
  assumes rep_iso: "\<And>y. abs\<cdot>(rep\<cdot>y) = y"
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   129
  shows "deflation d \<Longrightarrow> deflation (abs oo d oo rep)"
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   130
by (rule ep_pair.deflation_e_d_p) (simp add: ep_pair.intro assms)
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   131
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   132
lemma deflation_chain_min:
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   133
  assumes chain: "chain d"
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   134
  assumes defl: "\<And>n. deflation (d n)"
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   135
  shows "d m\<cdot>(d n\<cdot>x) = d (min m n)\<cdot>x"
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   136
proof (rule linorder_le_cases)
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   137
  assume "m \<le> n"
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   138
  with chain have "d m \<sqsubseteq> d n" by (rule chain_mono)
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   139
  then have "d m\<cdot>(d n\<cdot>x) = d m\<cdot>x"
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   140
    by (rule deflation_below_comp1 [OF defl defl])
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   141
  moreover from `m \<le> n` have "min m n = m" by simp
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   142
  ultimately show ?thesis by simp
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   143
next
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   144
  assume "n \<le> m"
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   145
  with chain have "d n \<sqsubseteq> d m" by (rule chain_mono)
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   146
  then have "d m\<cdot>(d n\<cdot>x) = d n\<cdot>x"
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   147
    by (rule deflation_below_comp2 [OF defl defl])
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   148
  moreover from `n \<le> m` have "min m n = n" by simp
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   149
  ultimately show ?thesis by simp
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   150
qed
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   151
35653
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   152
lemma lub_ID_take_lemma:
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   153
  assumes "chain t" and "(\<Squnion>n. t n) = ID"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   154
  assumes "\<And>n. t n\<cdot>x = t n\<cdot>y" shows "x = y"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   155
proof -
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   156
  have "(\<Squnion>n. t n\<cdot>x) = (\<Squnion>n. t n\<cdot>y)"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   157
    using assms(3) by simp
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   158
  then have "(\<Squnion>n. t n)\<cdot>x = (\<Squnion>n. t n)\<cdot>y"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   159
    using assms(1) by (simp add: lub_distribs)
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   160
  then show "x = y"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   161
    using assms(2) by simp
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   162
qed
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   163
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   164
lemma lub_ID_reach:
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   165
  assumes "chain t" and "(\<Squnion>n. t n) = ID"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   166
  shows "(\<Squnion>n. t n\<cdot>x) = x"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   167
using assms by (simp add: lub_distribs)
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   168
35655
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35653
diff changeset
   169
lemma lub_ID_take_induct:
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35653
diff changeset
   170
  assumes "chain t" and "(\<Squnion>n. t n) = ID"
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35653
diff changeset
   171
  assumes "adm P" and "\<And>n. P (t n\<cdot>x)" shows "P x"
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35653
diff changeset
   172
proof -
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35653
diff changeset
   173
  from `chain t` have "chain (\<lambda>n. t n\<cdot>x)" by simp
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35653
diff changeset
   174
  from `adm P` this `\<And>n. P (t n\<cdot>x)` have "P (\<Squnion>n. t n\<cdot>x)" by (rule admD)
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35653
diff changeset
   175
  with `chain t` `(\<Squnion>n. t n) = ID` show "P x" by (simp add: lub_distribs)
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35653
diff changeset
   176
qed
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35653
diff changeset
   177
35653
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   178
subsection {* Finiteness *}
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   179
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   180
text {*
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   181
  Let a ``decisive'' function be a deflation that maps every input to
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   182
  either itself or bottom.  Then if a domain's take functions are all
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   183
  decisive, then all values in the domain are finite.
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   184
*}
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   185
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   186
definition
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   187
  decisive :: "('a::pcpo \<rightarrow> 'a) \<Rightarrow> bool"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   188
where
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   189
  "decisive d \<longleftrightarrow> (\<forall>x. d\<cdot>x = x \<or> d\<cdot>x = \<bottom>)"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   190
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   191
lemma decisiveI: "(\<And>x. d\<cdot>x = x \<or> d\<cdot>x = \<bottom>) \<Longrightarrow> decisive d"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   192
  unfolding decisive_def by simp
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   193
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   194
lemma decisive_cases:
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   195
  assumes "decisive d" obtains "d\<cdot>x = x" | "d\<cdot>x = \<bottom>"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   196
using assms unfolding decisive_def by auto
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   197
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   198
lemma decisive_bottom: "decisive \<bottom>"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   199
  unfolding decisive_def by simp
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   200
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   201
lemma decisive_ID: "decisive ID"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   202
  unfolding decisive_def by simp
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   203
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   204
lemma decisive_ssum_map:
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   205
  assumes f: "decisive f"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   206
  assumes g: "decisive g"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   207
  shows "decisive (ssum_map\<cdot>f\<cdot>g)"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   208
apply (rule decisiveI, rename_tac s)
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   209
apply (case_tac s, simp_all)
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   210
apply (rule_tac x=x in decisive_cases [OF f], simp_all)
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   211
apply (rule_tac x=y in decisive_cases [OF g], simp_all)
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   212
done
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   213
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   214
lemma decisive_sprod_map:
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   215
  assumes f: "decisive f"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   216
  assumes g: "decisive g"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   217
  shows "decisive (sprod_map\<cdot>f\<cdot>g)"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   218
apply (rule decisiveI, rename_tac s)
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   219
apply (case_tac s, simp_all)
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   220
apply (rule_tac x=x in decisive_cases [OF f], simp_all)
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   221
apply (rule_tac x=y in decisive_cases [OF g], simp_all)
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   222
done
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   223
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   224
lemma decisive_abs_rep:
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   225
  fixes abs rep
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   226
  assumes iso: "iso abs rep"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   227
  assumes d: "decisive d"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   228
  shows "decisive (abs oo d oo rep)"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   229
apply (rule decisiveI)
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   230
apply (rule_tac x="rep\<cdot>x" in decisive_cases [OF d])
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   231
apply (simp add: iso.rep_iso [OF iso])
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   232
apply (simp add: iso.abs_strict [OF iso])
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   233
done
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   234
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   235
lemma lub_ID_finite:
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   236
  assumes chain: "chain d"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   237
  assumes lub: "(\<Squnion>n. d n) = ID"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   238
  assumes decisive: "\<And>n. decisive (d n)"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   239
  shows "\<exists>n. d n\<cdot>x = x"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   240
proof -
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   241
  have 1: "chain (\<lambda>n. d n\<cdot>x)" using chain by simp
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   242
  have 2: "(\<Squnion>n. d n\<cdot>x) = x" using chain lub by (rule lub_ID_reach)
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   243
  have "\<forall>n. d n\<cdot>x = x \<or> d n\<cdot>x = \<bottom>"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   244
    using decisive unfolding decisive_def by simp
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   245
  hence "range (\<lambda>n. d n\<cdot>x) \<subseteq> {x, \<bottom>}"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   246
    by auto
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   247
  hence "finite (range (\<lambda>n. d n\<cdot>x))"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   248
    by (rule finite_subset, simp)
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   249
  with 1 have "finite_chain (\<lambda>n. d n\<cdot>x)"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   250
    by (rule finite_range_imp_finch)
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   251
  then have "\<exists>n. (\<Squnion>n. d n\<cdot>x) = d n\<cdot>x"
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   252
    unfolding finite_chain_def by (auto simp add: maxinch_is_thelub)
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   253
  with 2 show "\<exists>n. d n\<cdot>x = x" by (auto elim: sym)
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   254
qed
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   255
35655
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35653
diff changeset
   256
lemma lub_ID_finite_take_induct:
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35653
diff changeset
   257
  assumes "chain d" and "(\<Squnion>n. d n) = ID" and "\<And>n. decisive (d n)"
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35653
diff changeset
   258
  shows "(\<And>n. P (d n\<cdot>x)) \<Longrightarrow> P x"
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35653
diff changeset
   259
using lub_ID_finite [OF assms] by metis
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35653
diff changeset
   260
40503
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   261
subsection {* Proofs about constructor functions *}
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   262
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   263
text {* Lemmas for proving nchotomy rule: *}
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   264
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   265
lemma ex_one_bottom_iff:
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   266
  "(\<exists>x. P x \<and> x \<noteq> \<bottom>) = P ONE"
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   267
by simp
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   268
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   269
lemma ex_up_bottom_iff:
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   270
  "(\<exists>x. P x \<and> x \<noteq> \<bottom>) = (\<exists>x. P (up\<cdot>x))"
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   271
by (safe, case_tac x, auto)
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   272
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   273
lemma ex_sprod_bottom_iff:
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   274
 "(\<exists>y. P y \<and> y \<noteq> \<bottom>) =
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   275
  (\<exists>x y. (P (:x, y:) \<and> x \<noteq> \<bottom>) \<and> y \<noteq> \<bottom>)"
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   276
by (safe, case_tac y, auto)
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   277
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   278
lemma ex_sprod_up_bottom_iff:
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   279
 "(\<exists>y. P y \<and> y \<noteq> \<bottom>) =
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   280
  (\<exists>x y. P (:up\<cdot>x, y:) \<and> y \<noteq> \<bottom>)"
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   281
by (safe, case_tac y, simp, case_tac x, auto)
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   282
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   283
lemma ex_ssum_bottom_iff:
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   284
 "(\<exists>x. P x \<and> x \<noteq> \<bottom>) =
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   285
 ((\<exists>x. P (sinl\<cdot>x) \<and> x \<noteq> \<bottom>) \<or>
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   286
  (\<exists>x. P (sinr\<cdot>x) \<and> x \<noteq> \<bottom>))"
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   287
by (safe, case_tac x, auto)
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   288
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   289
lemma exh_start: "p = \<bottom> \<or> (\<exists>x. p = x \<and> x \<noteq> \<bottom>)"
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   290
  by auto
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   291
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   292
lemmas ex_bottom_iffs =
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   293
   ex_ssum_bottom_iff
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   294
   ex_sprod_up_bottom_iff
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   295
   ex_sprod_bottom_iff
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   296
   ex_up_bottom_iff
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   297
   ex_one_bottom_iff
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   298
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   299
text {* Rules for turning nchotomy into exhaust: *}
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   300
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   301
lemma exh_casedist0: "\<lbrakk>R; R \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" (* like make_elim *)
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   302
  by auto
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   303
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   304
lemma exh_casedist1: "((P \<or> Q \<Longrightarrow> R) \<Longrightarrow> S) \<equiv> (\<lbrakk>P \<Longrightarrow> R; Q \<Longrightarrow> R\<rbrakk> \<Longrightarrow> S)"
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   305
  by rule auto
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   306
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   307
lemma exh_casedist2: "(\<exists>x. P x \<Longrightarrow> Q) \<equiv> (\<And>x. P x \<Longrightarrow> Q)"
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   308
  by rule auto
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   309
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   310
lemma exh_casedist3: "(P \<and> Q \<Longrightarrow> R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> R)"
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   311
  by rule auto
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   312
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   313
lemmas exh_casedists = exh_casedist1 exh_casedist2 exh_casedist3
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   314
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   315
text {* Rules for proving constructor properties *}
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   316
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   317
lemmas con_strict_rules =
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   318
  sinl_strict sinr_strict spair_strict1 spair_strict2
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   319
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   320
lemmas con_bottom_iff_rules =
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   321
  sinl_bottom_iff sinr_bottom_iff spair_bottom_iff up_defined ONE_defined
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   322
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   323
lemmas con_below_iff_rules =
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   324
  sinl_below sinr_below sinl_below_sinr sinr_below_sinl con_bottom_iff_rules
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   325
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   326
lemmas con_eq_iff_rules =
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   327
  sinl_eq sinr_eq sinl_eq_sinr sinr_eq_sinl con_bottom_iff_rules
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   328
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   329
lemmas sel_strict_rules =
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   330
  cfcomp2 sscase1 sfst_strict ssnd_strict fup1
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   331
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   332
lemma sel_app_extra_rules:
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   333
  "sscase\<cdot>ID\<cdot>\<bottom>\<cdot>(sinr\<cdot>x) = \<bottom>"
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   334
  "sscase\<cdot>ID\<cdot>\<bottom>\<cdot>(sinl\<cdot>x) = x"
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   335
  "sscase\<cdot>\<bottom>\<cdot>ID\<cdot>(sinl\<cdot>x) = \<bottom>"
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   336
  "sscase\<cdot>\<bottom>\<cdot>ID\<cdot>(sinr\<cdot>x) = x"
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   337
  "fup\<cdot>ID\<cdot>(up\<cdot>x) = x"
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   338
by (cases "x = \<bottom>", simp, simp)+
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   339
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   340
lemmas sel_app_rules =
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   341
  sel_strict_rules sel_app_extra_rules
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   342
  ssnd_spair sfst_spair up_defined spair_defined
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   343
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   344
lemmas sel_bottom_iff_rules =
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   345
  cfcomp2 sfst_bottom_iff ssnd_bottom_iff
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   346
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   347
lemmas take_con_rules =
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   348
  ssum_map_sinl' ssum_map_sinr' sprod_map_spair' u_map_up
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   349
  deflation_strict deflation_ID ID1 cfcomp2
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   350
35653
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   351
subsection {* ML setup *}
f87132febfac move lemmas from Domain.thy to Domain_Aux.thy
huffman
parents: 35652
diff changeset
   352
35652
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   353
use "Tools/Domain/domain_take_proofs.ML"
40503
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   354
use "Tools/cont_consts.ML"
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   355
use "Tools/cont_proc.ML"
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   356
use "Tools/Domain/domain_constructors.ML"
4094d788b904 move stuff from Domain.thy to Domain_Aux.thy
huffman
parents: 40502
diff changeset
   357
use "Tools/Domain/domain_induction.ML"
35652
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   358
40216
366309dfaf60 use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents: 35655
diff changeset
   359
setup Domain_Take_Proofs.setup
366309dfaf60 use Named_Thms instead of Theory_Data for some domain package theorems
huffman
parents: 35655
diff changeset
   360
35652
05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy
huffman
parents:
diff changeset
   361
end