src/HOLCF/Ffun.thy
author huffman
Wed, 02 Jan 2008 18:57:40 +0100
changeset 25786 6b3c79acac1f
parent 25758 89c7c22e64b4
child 25827 c2adeb1bae5c
permissions -rw-r--r--
move lemmas from Cont.thy to Ffun.thy; reorder dependency of Cont.thy and Ffun.thy; add dcpo instance proofs for function type
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
     1
(*  Title:      HOLCF/FunCpo.thy
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
     2
    ID:         $Id$
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
     3
    Author:     Franz Regensburger
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
Definition of the partial ordering for the type of all functions => (fun)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
     6
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
     7
Class instance of  => (fun) for class pcpo.
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
     8
*)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
     9
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    10
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
    11
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    12
theory Ffun
25786
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
    13
imports Cont
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    14
begin
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    15
18291
4afdf02d9831 changed section names
huffman
parents: 18092
diff changeset
    16
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
    17
25758
89c7c22e64b4 update instance proofs to new style
huffman
parents: 20523
diff changeset
    18
instantiation "fun"  :: (type, sq_ord) sq_ord
89c7c22e64b4 update instance proofs to new style
huffman
parents: 20523
diff changeset
    19
begin
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    20
25758
89c7c22e64b4 update instance proofs to new style
huffman
parents: 20523
diff changeset
    21
definition
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    22
  less_fun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)"  
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    23
25758
89c7c22e64b4 update instance proofs to new style
huffman
parents: 20523
diff changeset
    24
instance ..
89c7c22e64b4 update instance proofs to new style
huffman
parents: 20523
diff changeset
    25
end
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    26
25758
89c7c22e64b4 update instance proofs to new style
huffman
parents: 20523
diff changeset
    27
instance "fun" :: (type, po) po
89c7c22e64b4 update instance proofs to new style
huffman
parents: 20523
diff changeset
    28
proof
89c7c22e64b4 update instance proofs to new style
huffman
parents: 20523
diff changeset
    29
  fix f :: "'a \<Rightarrow> 'b"
89c7c22e64b4 update instance proofs to new style
huffman
parents: 20523
diff changeset
    30
  show "f \<sqsubseteq> f"
89c7c22e64b4 update instance proofs to new style
huffman
parents: 20523
diff changeset
    31
    by (simp add: less_fun_def)
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 :: "'a \<Rightarrow> 'b"
89c7c22e64b4 update instance proofs to new style
huffman
parents: 20523
diff changeset
    34
  assume "f \<sqsubseteq> g" and "g \<sqsubseteq> f" thus "f = g"
89c7c22e64b4 update instance proofs to new style
huffman
parents: 20523
diff changeset
    35
    by (simp add: less_fun_def expand_fun_eq antisym_less)
89c7c22e64b4 update instance proofs to new style
huffman
parents: 20523
diff changeset
    36
next
89c7c22e64b4 update instance proofs to new style
huffman
parents: 20523
diff changeset
    37
  fix f g h :: "'a \<Rightarrow> 'b"
89c7c22e64b4 update instance proofs to new style
huffman
parents: 20523
diff changeset
    38
  assume "f \<sqsubseteq> g" and "g \<sqsubseteq> h" thus "f \<sqsubseteq> h"
89c7c22e64b4 update instance proofs to new style
huffman
parents: 20523
diff changeset
    39
    unfolding less_fun_def by (fast elim: trans_less)
89c7c22e64b4 update instance proofs to new style
huffman
parents: 20523
diff changeset
    40
qed
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    41
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    42
text {* make the symbol @{text "<<"} accessible for type fun *}
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    43
17831
4a8c3f8b0a92 cleaned up; renamed less_fun to expand_fun_less
huffman
parents: 16202
diff changeset
    44
lemma expand_fun_less: "(f \<sqsubseteq> 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
    45
by (simp add: less_fun_def)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    46
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    47
lemma less_fun_ext: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    48
by (simp add: less_fun_def)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    49
18291
4afdf02d9831 changed section names
huffman
parents: 18092
diff changeset
    50
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
    51
25786
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
    52
text {* function application is monotone *}
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
    53
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
    54
lemma monofun_app: "monofun (\<lambda>f. f x)"
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
    55
by (rule monofunI, simp add: less_fun_def)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
    56
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    57
text {* chains of functions yield chains in the po range *}
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    58
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    59
lemma ch2ch_fun: "chain S \<Longrightarrow> chain (\<lambda>i. S i x)"
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    60
by (simp add: chain_def less_fun_def)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    61
18092
2c5d5da79a1e renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
huffman
parents: 17831
diff changeset
    62
lemma ch2ch_lambda: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> chain S"
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    63
by (simp add: chain_def less_fun_def)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    64
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    65
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    66
text {* upper bounds of function chains yield upper bound in the po range *}
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    67
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    68
lemma ub2ub_fun:
25786
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
    69
  "range (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::po) <| u \<Longrightarrow> range (\<lambda>i. S i x) <| u x"
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    70
by (auto simp add: is_ub_def less_fun_def)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    71
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    72
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
    73
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    74
lemma lub_fun:
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)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    76
    \<Longrightarrow> range S <<| (\<lambda>x. \<Squnion>i. S i x)"
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    77
apply (rule is_lubI)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    78
apply (rule ub_rangeI)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    79
apply (rule less_fun_ext)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    80
apply (rule is_ub_thelub)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    81
apply (erule ch2ch_fun)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    82
apply (rule less_fun_ext)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    83
apply (rule is_lub_thelub)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    84
apply (erule ch2ch_fun)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    85
apply (erule ub2ub_fun)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    86
done
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    87
25786
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
    88
lemma lub_fun':
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
    89
  fixes S :: "('a::type \<Rightarrow> 'b::dcpo) set"
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
    90
  assumes S: "directed S"
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
    91
  shows "S <<| (\<lambda>x. \<Squnion>f\<in>S. f x)"
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
    92
apply (rule is_lubI)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
    93
apply (rule is_ubI)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
    94
apply (rule less_fun_ext)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
    95
apply (rule is_ub_thelub')
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
    96
apply (rule dir2dir_monofun [OF monofun_app S])
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
    97
apply (erule imageI)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
    98
apply (rule less_fun_ext)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
    99
apply (rule is_lub_thelub')
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   100
apply (rule dir2dir_monofun [OF monofun_app S])
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   101
apply (erule ub2ub_monofun' [OF monofun_app])
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   102
done
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   103
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
   104
lemma thelub_fun:
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
   105
  "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
   106
    \<Longrightarrow> lub (range S) = (\<lambda>x. \<Squnion>i. S i x)"
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
   107
by (rule lub_fun [THEN thelubI])
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
   108
25786
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   109
lemma thelub_fun':
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   110
  "directed (S::('a::type \<Rightarrow> 'b::dcpo) set)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   111
    \<Longrightarrow> lub S = (\<lambda>x. \<Squnion>f\<in>S. f x)"
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   112
by (rule lub_fun' [THEN thelubI])
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   113
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
   114
lemma cpo_fun:
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
   115
  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) \<Longrightarrow> \<exists>x. range S <<| x"
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
   116
by (rule exI, erule lub_fun)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
   117
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 18291
diff changeset
   118
instance "fun"  :: (type, cpo) cpo
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
   119
by intro_classes (rule cpo_fun)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
   120
25786
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   121
lemma dcpo_fun:
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   122
  "directed (S::('a::type \<Rightarrow> 'b::dcpo) set) \<Longrightarrow> \<exists>x. S <<| x"
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   123
by (rule exI, erule lub_fun')
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   124
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   125
instance "fun" :: (type, dcpo) dcpo
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   126
by intro_classes (rule dcpo_fun)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   127
18291
4afdf02d9831 changed section names
huffman
parents: 18092
diff changeset
   128
subsection {* Full function space is pointed *}
17831
4a8c3f8b0a92 cleaned up; renamed less_fun to expand_fun_less
huffman
parents: 16202
diff changeset
   129
4a8c3f8b0a92 cleaned up; renamed less_fun to expand_fun_less
huffman
parents: 16202
diff changeset
   130
lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f"
4a8c3f8b0a92 cleaned up; renamed less_fun to expand_fun_less
huffman
parents: 16202
diff changeset
   131
by (simp add: less_fun_def)
4a8c3f8b0a92 cleaned up; renamed less_fun to expand_fun_less
huffman
parents: 16202
diff changeset
   132
25786
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   133
lemma least_fun: "\<exists>x::'a::type \<Rightarrow> 'b::pcpo. \<forall>y. x \<sqsubseteq> y"
17831
4a8c3f8b0a92 cleaned up; renamed less_fun to expand_fun_less
huffman
parents: 16202
diff changeset
   134
apply (rule_tac x = "\<lambda>x. \<bottom>" in exI)
4a8c3f8b0a92 cleaned up; renamed less_fun to expand_fun_less
huffman
parents: 16202
diff changeset
   135
apply (rule minimal_fun [THEN allI])
4a8c3f8b0a92 cleaned up; renamed less_fun to expand_fun_less
huffman
parents: 16202
diff changeset
   136
done
4a8c3f8b0a92 cleaned up; renamed less_fun to expand_fun_less
huffman
parents: 16202
diff changeset
   137
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 18291
diff changeset
   138
instance "fun"  :: (type, pcpo) pcpo
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
   139
by intro_classes (rule least_fun)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
   140
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
   141
text {* for compatibility with old HOLCF-Version *}
17831
4a8c3f8b0a92 cleaned up; renamed less_fun to expand_fun_less
huffman
parents: 16202
diff changeset
   142
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
   143
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
   144
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
   145
text {* function application is strict in the left argument *}
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
   146
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
   147
by (simp add: inst_fun_pcpo)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
   148
25786
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   149
text {*
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   150
  The following results are about application for functions in @{typ "'a=>'b"}
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   151
*}
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   152
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   153
lemma monofun_fun_fun: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   154
by (simp add: less_fun_def)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   155
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   156
lemma monofun_fun_arg: "\<lbrakk>monofun f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y"
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   157
by (rule monofunE)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   158
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   159
lemma monofun_fun: "\<lbrakk>monofun f; monofun g; f \<sqsubseteq> g; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> g y"
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   160
by (rule trans_less [OF monofun_fun_arg monofun_fun_fun])
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   161
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   162
subsection {* Propagation of monotonicity and continuity *}
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   163
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   164
text {* the lub of a chain of monotone functions is monotone *}
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
lemma monofun_lub_fun:
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   167
  "\<lbrakk>chain (F::nat \<Rightarrow> 'a \<Rightarrow> 'b::cpo); \<forall>i. monofun (F i)\<rbrakk>
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   168
    \<Longrightarrow> monofun (\<Squnion>i. F i)"
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   169
apply (rule monofunI)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   170
apply (simp add: thelub_fun)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   171
apply (rule lub_mono [rule_format])
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   172
apply (erule ch2ch_fun)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   173
apply (erule ch2ch_fun)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   174
apply (simp add: monofunE)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   175
done
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   176
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   177
text {* the lub of a chain of continuous functions is continuous *}
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   178
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   179
declare range_composition [simp del]
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   180
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   181
lemma contlub_lub_fun:
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   182
  "\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> contlub (\<Squnion>i. F i)"
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   183
apply (rule contlubI)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   184
apply (simp add: thelub_fun)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   185
apply (simp add: cont2contlubE)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   186
apply (rule ex_lub)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   187
apply (erule ch2ch_fun)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   188
apply (simp add: ch2ch_cont)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   189
done
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   190
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   191
lemma cont_lub_fun:
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   192
  "\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<Squnion>i. F i)"
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   193
apply (rule monocontlub2cont)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   194
apply (erule monofun_lub_fun)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   195
apply (simp add: cont2mono)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   196
apply (erule (1) contlub_lub_fun)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   197
done
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   198
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   199
lemma cont2cont_lub:
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   200
  "\<lbrakk>chain F; \<And>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. \<Squnion>i. F i x)"
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   201
by (simp add: thelub_fun [symmetric] cont_lub_fun)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   202
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   203
lemma mono2mono_fun: "monofun f \<Longrightarrow> monofun (\<lambda>x. f x y)"
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   204
apply (rule monofunI)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   205
apply (erule (1) monofun_fun_arg [THEN monofun_fun_fun])
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   206
done
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   207
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   208
lemma cont2cont_fun: "cont f \<Longrightarrow> cont (\<lambda>x. f x y)"
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   209
apply (rule monocontlub2cont)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   210
apply (erule cont2mono [THEN mono2mono_fun])
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   211
apply (rule contlubI)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   212
apply (simp add: cont2contlubE)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   213
apply (simp add: thelub_fun ch2ch_cont)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   214
done
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   215
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   216
text {* Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"} *}
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   217
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   218
lemma mono2mono_lambda: "(\<And>y. monofun (\<lambda>x. f x y)) \<Longrightarrow> monofun f"
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   219
apply (rule monofunI)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   220
apply (rule less_fun_ext)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   221
apply (blast dest: monofunE)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   222
done
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   223
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   224
lemma cont2cont_lambda: "(\<And>y. cont (\<lambda>x. f x y)) \<Longrightarrow> cont f"
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   225
apply (subgoal_tac "monofun f")
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   226
apply (rule monocontlub2cont)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   227
apply assumption
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   228
apply (rule contlubI)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   229
apply (rule ext)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   230
apply (simp add: thelub_fun ch2ch_monofun)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   231
apply (blast dest: cont2contlubE)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   232
apply (simp add: mono2mono_lambda cont2mono)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   233
done
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   234
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   235
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
   236
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   237
lemma contlub_lambda:
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   238
  "(\<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
   239
    \<Longrightarrow> (\<lambda>x. \<Squnion>i. S i x) = (\<Squnion>i. (\<lambda>x. S i x))"
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   240
by (simp add: thelub_fun ch2ch_lambda)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   241
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   242
lemma contlub_abstraction:
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   243
  "\<lbrakk>chain Y; \<forall>y. cont (\<lambda>x.(c::'a::cpo\<Rightarrow>'b::type\<Rightarrow>'c::cpo) x y)\<rbrakk> \<Longrightarrow>
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   244
    (\<lambda>y. \<Squnion>i. c (Y i) y) = (\<Squnion>i. (\<lambda>y. c (Y i) y))"
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   245
apply (rule thelub_fun [symmetric])
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   246
apply (rule ch2ch_cont)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   247
apply (simp add: cont2cont_lambda)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   248
apply assumption
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   249
done
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   250
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   251
lemma mono2mono_app:
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   252
  "\<lbrakk>monofun f; \<forall>x. monofun (f x); monofun t\<rbrakk> \<Longrightarrow> monofun (\<lambda>x. (f x) (t x))"
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   253
apply (rule monofunI)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   254
apply (simp add: monofun_fun monofunE)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   255
done
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   256
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   257
lemma cont2contlub_app:
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   258
  "\<lbrakk>cont f; \<forall>x. cont (f x); cont t\<rbrakk> \<Longrightarrow> contlub (\<lambda>x. (f x) (t x))"
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   259
apply (rule contlubI)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   260
apply (subgoal_tac "chain (\<lambda>i. f (Y i))")
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   261
apply (subgoal_tac "chain (\<lambda>i. t (Y i))")
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   262
apply (simp add: cont2contlubE thelub_fun)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   263
apply (rule diag_lub)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   264
apply (erule ch2ch_fun)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   265
apply (drule spec)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   266
apply (erule (1) ch2ch_cont)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   267
apply (erule (1) ch2ch_cont)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   268
apply (erule (1) ch2ch_cont)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   269
done
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   270
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   271
lemma cont2cont_app:
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   272
  "\<lbrakk>cont f; \<forall>x. cont (f x); cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. (f x) (t x))"
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   273
by (blast intro: monocontlub2cont mono2mono_app cont2mono cont2contlub_app)
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   274
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   275
lemmas cont2cont_app2 = cont2cont_app [rule_format]
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   276
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   277
lemma cont2cont_app3: "\<lbrakk>cont f; cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. f (t x))"
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   278
by (rule cont2cont_app2 [OF cont_const])
6b3c79acac1f move lemmas from Cont.thy to Ffun.thy;
huffman
parents: 25758
diff changeset
   279
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
   280
end
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
   281