src/HOLCF/Ffun.thy
author huffman
Wed, 02 Jan 2008 01:20:18 +0100
changeset 25758 89c7c22e64b4
parent 20523 36a59e5d0039
child 25786 6b3c79acac1f
permissions -rw-r--r--
update instance proofs to new style
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
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    13
imports Pcpo
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
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    52
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
    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)"
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    55
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
    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"
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    58
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
    59
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    60
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    61
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
    62
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    63
lemma ub2ub_fun:
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    64
  "range (S::nat \<Rightarrow> 'a \<Rightarrow> 'b::po) <| u \<Longrightarrow> range (\<lambda>i. S i x) <| u x"
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    65
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
    66
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    67
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
    68
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    69
lemma lub_fun:
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    70
  "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
    71
    \<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
    72
apply (rule is_lubI)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    73
apply (rule ub_rangeI)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    74
apply (rule less_fun_ext)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    75
apply (rule is_ub_thelub)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    76
apply (erule ch2ch_fun)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    77
apply (rule less_fun_ext)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    78
apply (rule is_lub_thelub)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    79
apply (erule ch2ch_fun)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    80
apply (erule ub2ub_fun)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    81
done
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    82
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    83
lemma thelub_fun:
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    84
  "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
    85
    \<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
    86
by (rule lub_fun [THEN thelubI])
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    87
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    88
lemma cpo_fun:
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    89
  "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
    90
by (rule exI, erule lub_fun)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    91
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 18291
diff changeset
    92
instance "fun"  :: (type, cpo) cpo
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    93
by intro_classes (rule cpo_fun)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
    94
18291
4afdf02d9831 changed section names
huffman
parents: 18092
diff changeset
    95
subsection {* Full function space is pointed *}
17831
4a8c3f8b0a92 cleaned up; renamed less_fun to expand_fun_less
huffman
parents: 16202
diff changeset
    96
4a8c3f8b0a92 cleaned up; renamed less_fun to expand_fun_less
huffman
parents: 16202
diff changeset
    97
lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f"
4a8c3f8b0a92 cleaned up; renamed less_fun to expand_fun_less
huffman
parents: 16202
diff changeset
    98
by (simp add: less_fun_def)
4a8c3f8b0a92 cleaned up; renamed less_fun to expand_fun_less
huffman
parents: 16202
diff changeset
    99
4a8c3f8b0a92 cleaned up; renamed less_fun to expand_fun_less
huffman
parents: 16202
diff changeset
   100
lemma least_fun: "\<exists>x::'a \<Rightarrow> 'b::pcpo. \<forall>y. x \<sqsubseteq> y"
4a8c3f8b0a92 cleaned up; renamed less_fun to expand_fun_less
huffman
parents: 16202
diff changeset
   101
apply (rule_tac x = "\<lambda>x. \<bottom>" in exI)
4a8c3f8b0a92 cleaned up; renamed less_fun to expand_fun_less
huffman
parents: 16202
diff changeset
   102
apply (rule minimal_fun [THEN allI])
4a8c3f8b0a92 cleaned up; renamed less_fun to expand_fun_less
huffman
parents: 16202
diff changeset
   103
done
4a8c3f8b0a92 cleaned up; renamed less_fun to expand_fun_less
huffman
parents: 16202
diff changeset
   104
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 18291
diff changeset
   105
instance "fun"  :: (type, pcpo) pcpo
16202
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
   106
by intro_classes (rule least_fun)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
   107
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
   108
text {* for compatibility with old HOLCF-Version *}
17831
4a8c3f8b0a92 cleaned up; renamed less_fun to expand_fun_less
huffman
parents: 16202
diff changeset
   109
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
   110
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
   111
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
   112
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
   113
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
   114
by (simp add: inst_fun_pcpo)
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
   115
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
   116
end
61811f31ce5a renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff changeset
   117