src/HOL/HOLCF/Fun_Cpo.thy
author huffman
Mon, 06 Dec 2010 10:08:33 -0800
changeset 41030 ff7d177128ef
parent 40774 0437dbc127b3
child 41032 75b4ff66781c
permissions -rw-r--r--
rename lub_fun -> is_lub_fun, thelub_fun -> lub_fun
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
40001
666c3751227c rename Ffun.thy to Fun_Cpo.thy
huffman
parents: 39302
diff changeset
     1
(*  Title:      HOLCF/Fun_Cpo.thy
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
     2
    Author:     Franz Regensburger
40001
666c3751227c rename Ffun.thy to Fun_Cpo.thy
huffman
parents: 39302
diff changeset
     3
    Author:     Brian Huffman
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
     4
*)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
     5
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
     6
header {* Class instances for the full function space *}
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
     7
40001
666c3751227c rename Ffun.thy to Fun_Cpo.thy
huffman
parents: 39302
diff changeset
     8
theory Fun_Cpo
40011
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
     9
imports Adm
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    10
begin
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    11
18291
4afdf02d9831 changed section names
huffman
parents: 18092
diff changeset
    12
subsection {* Full function space is a partial order *}
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    13
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29138
diff changeset
    14
instantiation "fun"  :: (type, below) below
25758
89c7c22e64b4 update instance proofs to new style
huffman
parents: 20523
diff changeset
    15
begin
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    16
25758
89c7c22e64b4 update instance proofs to new style
huffman
parents: 20523
diff changeset
    17
definition
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29138
diff changeset
    18
  below_fun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)"
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    19
25758
89c7c22e64b4 update instance proofs to new style
huffman
parents: 20523
diff changeset
    20
instance ..
89c7c22e64b4 update instance proofs to new style
huffman
parents: 20523
diff changeset
    21
end
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    22
25758
89c7c22e64b4 update instance proofs to new style
huffman
parents: 20523
diff changeset
    23
instance "fun" :: (type, po) po
89c7c22e64b4 update instance proofs to new style
huffman
parents: 20523
diff changeset
    24
proof
89c7c22e64b4 update instance proofs to new style
huffman
parents: 20523
diff changeset
    25
  fix f :: "'a \<Rightarrow> 'b"
89c7c22e64b4 update instance proofs to new style
huffman
parents: 20523
diff changeset
    26
  show "f \<sqsubseteq> f"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29138
diff changeset
    27
    by (simp add: below_fun_def)
25758
89c7c22e64b4 update instance proofs to new style
huffman
parents: 20523
diff changeset
    28
next
89c7c22e64b4 update instance proofs to new style
huffman
parents: 20523
diff changeset
    29
  fix f g :: "'a \<Rightarrow> 'b"
89c7c22e64b4 update instance proofs to new style
huffman
parents: 20523
diff changeset
    30
  assume "f \<sqsubseteq> g" and "g \<sqsubseteq> f" thus "f = g"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39199
diff changeset
    31
    by (simp add: below_fun_def fun_eq_iff below_antisym)
25758
89c7c22e64b4 update instance proofs to new style
huffman
parents: 20523
diff changeset
    32
next
89c7c22e64b4 update instance proofs to new style
huffman
parents: 20523
diff changeset
    33
  fix f g h :: "'a \<Rightarrow> 'b"
89c7c22e64b4 update instance proofs to new style
huffman
parents: 20523
diff changeset
    34
  assume "f \<sqsubseteq> g" and "g \<sqsubseteq> h" thus "f \<sqsubseteq> h"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29138
diff changeset
    35
    unfolding below_fun_def by (fast elim: below_trans)
25758
89c7c22e64b4 update instance proofs to new style
huffman
parents: 20523
diff changeset
    36
qed
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    37
40002
c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents: 40001
diff changeset
    38
lemma fun_below_iff: "f \<sqsubseteq> g \<longleftrightarrow> (\<forall>x. f x \<sqsubseteq> g x)"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29138
diff changeset
    39
by (simp add: below_fun_def)
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    40
40002
c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents: 40001
diff changeset
    41
lemma fun_belowI: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29138
diff changeset
    42
by (simp add: below_fun_def)
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    43
40011
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
    44
lemma fun_belowD: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
    45
by (simp add: below_fun_def)
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
    46
18291
4afdf02d9831 changed section names
huffman
parents: 18092
diff changeset
    47
subsection {* Full function space is chain complete *}
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    48
40011
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
    49
text {* Properties of chains of functions. *}
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
    50
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
    51
lemma fun_chain_iff: "chain S \<longleftrightarrow> (\<forall>x. chain (\<lambda>i. S i x))"
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
    52
unfolding chain_def fun_below_iff by auto
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    53
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    54
lemma ch2ch_fun: "chain S \<Longrightarrow> chain (\<lambda>i. S i x)"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29138
diff changeset
    55
by (simp add: chain_def below_fun_def)
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    56
18092
2c5d5da79a1e renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
huffman
parents: 17831
diff changeset
    57
lemma ch2ch_lambda: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> chain S"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29138
diff changeset
    58
by (simp add: chain_def below_fun_def)
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    59
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    60
text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *}
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    61
26028
74668c3a8f70 add lemma is_lub_lambda
huffman
parents: 26025
diff changeset
    62
lemma is_lub_lambda:
40011
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
    63
  "(\<And>x. range (\<lambda>i. Y i x) <<| f x) \<Longrightarrow> range Y <<| f"
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
    64
unfolding is_lub_def is_ub_def below_fun_def by simp
26028
74668c3a8f70 add lemma is_lub_lambda
huffman
parents: 26025
diff changeset
    65
41030
ff7d177128ef rename lub_fun -> is_lub_fun, thelub_fun -> lub_fun
huffman
parents: 40774
diff changeset
    66
lemma is_lub_fun:
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    67
  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    68
    \<Longrightarrow> range S <<| (\<lambda>x. \<Squnion>i. S i x)"
26028
74668c3a8f70 add lemma is_lub_lambda
huffman
parents: 26025
diff changeset
    69
apply (rule is_lub_lambda)
74668c3a8f70 add lemma is_lub_lambda
huffman
parents: 26025
diff changeset
    70
apply (rule cpo_lubI)
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    71
apply (erule ch2ch_fun)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    72
done
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    73
41030
ff7d177128ef rename lub_fun -> is_lub_fun, thelub_fun -> lub_fun
huffman
parents: 40774
diff changeset
    74
lemma lub_fun:
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    75
  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
27413
3154f3765cc7 replace lub (range Y) with (LUB i. Y i)
huffman
parents: 26452
diff changeset
    76
    \<Longrightarrow> (\<Squnion>i. S i) = (\<lambda>x. \<Squnion>i. S i x)"
41030
ff7d177128ef rename lub_fun -> is_lub_fun, thelub_fun -> lub_fun
huffman
parents: 40774
diff changeset
    77
by (rule is_lub_fun [THEN lub_eqI])
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    78
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 18291
diff changeset
    79
instance "fun"  :: (type, cpo) cpo
41030
ff7d177128ef rename lub_fun -> is_lub_fun, thelub_fun -> lub_fun
huffman
parents: 40774
diff changeset
    80
by intro_classes (rule exI, erule is_lub_fun)
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    81
40011
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
    82
subsection {* Chain-finiteness of function space *}
25827
c2adeb1bae5c new instance proofs for classes finite_po, chfin, flat
huffman
parents: 25786
diff changeset
    83
c2adeb1bae5c new instance proofs for classes finite_po, chfin, flat
huffman
parents: 25786
diff changeset
    84
lemma maxinch2maxinch_lambda:
c2adeb1bae5c new instance proofs for classes finite_po, chfin, flat
huffman
parents: 25786
diff changeset
    85
  "(\<And>x. max_in_chain n (\<lambda>i. S i x)) \<Longrightarrow> max_in_chain n S"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39199
diff changeset
    86
unfolding max_in_chain_def fun_eq_iff by simp
25827
c2adeb1bae5c new instance proofs for classes finite_po, chfin, flat
huffman
parents: 25786
diff changeset
    87
c2adeb1bae5c new instance proofs for classes finite_po, chfin, flat
huffman
parents: 25786
diff changeset
    88
lemma maxinch_mono:
c2adeb1bae5c new instance proofs for classes finite_po, chfin, flat
huffman
parents: 25786
diff changeset
    89
  "\<lbrakk>max_in_chain i Y; i \<le> j\<rbrakk> \<Longrightarrow> max_in_chain j Y"
c2adeb1bae5c new instance proofs for classes finite_po, chfin, flat
huffman
parents: 25786
diff changeset
    90
unfolding max_in_chain_def
c2adeb1bae5c new instance proofs for classes finite_po, chfin, flat
huffman
parents: 25786
diff changeset
    91
proof (intro allI impI)
c2adeb1bae5c new instance proofs for classes finite_po, chfin, flat
huffman
parents: 25786
diff changeset
    92
  fix k
c2adeb1bae5c new instance proofs for classes finite_po, chfin, flat
huffman
parents: 25786
diff changeset
    93
  assume Y: "\<forall>n\<ge>i. Y i = Y n"
c2adeb1bae5c new instance proofs for classes finite_po, chfin, flat
huffman
parents: 25786
diff changeset
    94
  assume ij: "i \<le> j"
c2adeb1bae5c new instance proofs for classes finite_po, chfin, flat
huffman
parents: 25786
diff changeset
    95
  assume jk: "j \<le> k"
c2adeb1bae5c new instance proofs for classes finite_po, chfin, flat
huffman
parents: 25786
diff changeset
    96
  from ij jk have ik: "i \<le> k" by simp
c2adeb1bae5c new instance proofs for classes finite_po, chfin, flat
huffman
parents: 25786
diff changeset
    97
  from Y ij have Yij: "Y i = Y j" by simp
c2adeb1bae5c new instance proofs for classes finite_po, chfin, flat
huffman
parents: 25786
diff changeset
    98
  from Y ik have Yik: "Y i = Y k" by simp
c2adeb1bae5c new instance proofs for classes finite_po, chfin, flat
huffman
parents: 25786
diff changeset
    99
  from Yij Yik show "Y j = Y k" by auto
c2adeb1bae5c new instance proofs for classes finite_po, chfin, flat
huffman
parents: 25786
diff changeset
   100
qed
c2adeb1bae5c new instance proofs for classes finite_po, chfin, flat
huffman
parents: 25786
diff changeset
   101
40011
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
   102
instance "fun" :: (type, discrete_cpo) discrete_cpo
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
   103
proof
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
   104
  fix f g :: "'a \<Rightarrow> 'b"
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
   105
  show "f \<sqsubseteq> g \<longleftrightarrow> f = g" 
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
   106
    unfolding fun_below_iff fun_eq_iff
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
   107
    by simp
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
   108
qed
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
   109
18291
4afdf02d9831 changed section names
huffman
parents: 18092
diff changeset
   110
subsection {* Full function space is pointed *}
17831
4a8c3f8b0a92 cleaned up; renamed less_fun to expand_fun_less
huffman
parents: 16202
diff changeset
   111
4a8c3f8b0a92 cleaned up; renamed less_fun to expand_fun_less
huffman
parents: 16202
diff changeset
   112
lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f"
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 29138
diff changeset
   113
by (simp add: below_fun_def)
17831
4a8c3f8b0a92 cleaned up; renamed less_fun to expand_fun_less
huffman
parents: 16202
diff changeset
   114
40011
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
   115
instance "fun"  :: (type, pcpo) pcpo
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
   116
by default (fast intro: minimal_fun)
17831
4a8c3f8b0a92 cleaned up; renamed less_fun to expand_fun_less
huffman
parents: 16202
diff changeset
   117
4a8c3f8b0a92 cleaned up; renamed less_fun to expand_fun_less
huffman
parents: 16202
diff changeset
   118
lemma inst_fun_pcpo: "\<bottom> = (\<lambda>x. \<bottom>)"
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
   119
by (rule minimal_fun [THEN UU_I, symmetric])
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
   120
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
   121
lemma app_strict [simp]: "\<bottom> x = \<bottom>"
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
   122
by (simp add: inst_fun_pcpo)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
   123
40011
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
   124
lemma lambda_strict: "(\<lambda>x. \<bottom>) = \<bottom>"
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
   125
by (rule UU_I, rule minimal_fun)
25786
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   126
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   127
subsection {* Propagation of monotonicity and continuity *}
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   128
40011
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
   129
text {* The lub of a chain of monotone functions is monotone. *}
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
   130
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
   131
lemma adm_monofun: "adm monofun"
41030
ff7d177128ef rename lub_fun -> is_lub_fun, thelub_fun -> lub_fun
huffman
parents: 40774
diff changeset
   132
by (rule admI, simp add: lub_fun fun_chain_iff monofun_def lub_mono)
25786
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   133
40011
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
   134
text {* The lub of a chain of continuous functions is continuous. *}
25786
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   135
40011
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
   136
lemma adm_cont: "adm cont"
41030
ff7d177128ef rename lub_fun -> is_lub_fun, thelub_fun -> lub_fun
huffman
parents: 40774
diff changeset
   137
by (rule admI, simp add: lub_fun fun_chain_iff)
25786
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   138
40011
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
   139
text {* Function application preserves monotonicity and continuity. *}
25786
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   140
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   141
lemma mono2mono_fun: "monofun f \<Longrightarrow> monofun (\<lambda>x. f x y)"
40011
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
   142
by (simp add: monofun_def fun_below_iff)
25786
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   143
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   144
lemma cont2cont_fun: "cont f \<Longrightarrow> cont (\<lambda>x. f x y)"
35914
91a7311177c4 remove contlub predicate
huffman
parents: 31076
diff changeset
   145
apply (rule contI2)
25786
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   146
apply (erule cont2mono [THEN mono2mono_fun])
41030
ff7d177128ef rename lub_fun -> is_lub_fun, thelub_fun -> lub_fun
huffman
parents: 40774
diff changeset
   147
apply (simp add: cont2contlubE lub_fun ch2ch_cont)
25786
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   148
done
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   149
40622
e40e9e9769f4 add lemma cont_fun; remove unused lemma monofun_app
huffman
parents: 40091
diff changeset
   150
lemma cont_fun: "cont (\<lambda>f. f x)"
e40e9e9769f4 add lemma cont_fun; remove unused lemma monofun_app
huffman
parents: 40091
diff changeset
   151
using cont_id by (rule cont2cont_fun)
e40e9e9769f4 add lemma cont_fun; remove unused lemma monofun_app
huffman
parents: 40091
diff changeset
   152
40011
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
   153
text {*
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
   154
  Lambda abstraction preserves monotonicity and continuity.
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
   155
  (Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"}.)
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
   156
*}
25786
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   157
26452
ed657432b8b9 declare cont_lemmas_ext as simp rules individually
huffman
parents: 26028
diff changeset
   158
lemma mono2mono_lambda:
ed657432b8b9 declare cont_lemmas_ext as simp rules individually
huffman
parents: 26028
diff changeset
   159
  assumes f: "\<And>y. monofun (\<lambda>x. f x y)" shows "monofun f"
40011
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
   160
using f by (simp add: monofun_def fun_below_iff)
25786
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   161
26452
ed657432b8b9 declare cont_lemmas_ext as simp rules individually
huffman
parents: 26028
diff changeset
   162
lemma cont2cont_lambda [simp]:
ed657432b8b9 declare cont_lemmas_ext as simp rules individually
huffman
parents: 26028
diff changeset
   163
  assumes f: "\<And>y. cont (\<lambda>x. f x y)" shows "cont f"
40011
b974cf829099 cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents: 40006
diff changeset
   164
by (rule contI, rule is_lub_lambda, rule contE [OF f])
25786
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   165
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   166
text {* What D.A.Schmidt calls continuity of abstraction; never used here *}
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   167
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   168
lemma contlub_lambda:
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   169
  "(\<And>x::'a::type. chain (\<lambda>i. S i x::'b::cpo))
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   170
    \<Longrightarrow> (\<lambda>x. \<Squnion>i. S i x) = (\<Squnion>i. (\<lambda>x. S i x))"
41030
ff7d177128ef rename lub_fun -> is_lub_fun, thelub_fun -> lub_fun
huffman
parents: 40774
diff changeset
   171
by (simp add: lub_fun ch2ch_lambda)
25786
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   172
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
   173
end