src/HOLCF/Ffun.thy
author huffman
Fri Jun 03 22:07:30 2005 +0200 (2005-06-03)
changeset 16202 61811f31ce5a
child 17831 4a8c3f8b0a92
permissions -rw-r--r--
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman@16202
     1
(*  Title:      HOLCF/FunCpo.thy
huffman@16202
     2
    ID:         $Id$
huffman@16202
     3
    Author:     Franz Regensburger
huffman@16202
     4
huffman@16202
     5
Definition of the partial ordering for the type of all functions => (fun)
huffman@16202
     6
huffman@16202
     7
Class instance of  => (fun) for class pcpo.
huffman@16202
     8
*)
huffman@16202
     9
huffman@16202
    10
header {* Class instances for the full function space *}
huffman@16202
    11
huffman@16202
    12
theory Ffun
huffman@16202
    13
imports Pcpo
huffman@16202
    14
begin
huffman@16202
    15
huffman@16202
    16
subsection {* Type @{typ "'a => 'b"} is a partial order *}
huffman@16202
    17
huffman@16202
    18
instance fun  :: (type, sq_ord) sq_ord ..
huffman@16202
    19
huffman@16202
    20
defs (overloaded)
huffman@16202
    21
  less_fun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)"  
huffman@16202
    22
huffman@16202
    23
lemma refl_less_fun: "(f::'a::type \<Rightarrow> 'b::po) \<sqsubseteq> f"
huffman@16202
    24
by (simp add: less_fun_def)
huffman@16202
    25
huffman@16202
    26
lemma antisym_less_fun:
huffman@16202
    27
  "\<lbrakk>(f1::'a::type \<Rightarrow> 'b::po) \<sqsubseteq> f2; f2 \<sqsubseteq> f1\<rbrakk> \<Longrightarrow> f1 = f2"
huffman@16202
    28
by (simp add: less_fun_def expand_fun_eq antisym_less)
huffman@16202
    29
huffman@16202
    30
lemma trans_less_fun:
huffman@16202
    31
  "\<lbrakk>(f1::'a::type \<Rightarrow> 'b::po) \<sqsubseteq> f2; f2 \<sqsubseteq> f3\<rbrakk> \<Longrightarrow> f1 \<sqsubseteq> f3"
huffman@16202
    32
apply (unfold less_fun_def)
huffman@16202
    33
apply clarify
huffman@16202
    34
apply (rule trans_less)
huffman@16202
    35
apply (erule spec)
huffman@16202
    36
apply (erule spec)
huffman@16202
    37
done
huffman@16202
    38
huffman@16202
    39
instance fun  :: (type, po) po
huffman@16202
    40
by intro_classes
huffman@16202
    41
  (assumption | rule refl_less_fun antisym_less_fun trans_less_fun)+
huffman@16202
    42
huffman@16202
    43
text {* make the symbol @{text "<<"} accessible for type fun *}
huffman@16202
    44
huffman@16202
    45
lemma less_fun: "(f \<sqsubseteq> g) = (\<forall>x. f x \<sqsubseteq> g x)"
huffman@16202
    46
by (simp add: less_fun_def)
huffman@16202
    47
huffman@16202
    48
lemma less_fun_ext: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
huffman@16202
    49
by (simp add: less_fun_def)
huffman@16202
    50
huffman@16202
    51
subsection {* Type @{typ "'a::type => 'b::pcpo"} is pointed *}
huffman@16202
    52
huffman@16202
    53
lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f"
huffman@16202
    54
by (simp add: less_fun_def)
huffman@16202
    55
huffman@16202
    56
lemma least_fun: "\<exists>x::'a \<Rightarrow> 'b::pcpo. \<forall>y. x \<sqsubseteq> y"
huffman@16202
    57
apply (rule_tac x = "\<lambda>x. \<bottom>" in exI)
huffman@16202
    58
apply (rule minimal_fun [THEN allI])
huffman@16202
    59
done
huffman@16202
    60
huffman@16202
    61
subsection {* Type @{typ "'a::type => 'b::cpo"} is chain complete *}
huffman@16202
    62
huffman@16202
    63
text {* chains of functions yield chains in the po range *}
huffman@16202
    64
huffman@16202
    65
lemma ch2ch_fun: "chain S \<Longrightarrow> chain (\<lambda>i. S i x)"
huffman@16202
    66
by (simp add: chain_def less_fun_def)
huffman@16202
    67
huffman@16202
    68
lemma ch2ch_fun_rev: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> chain S"
huffman@16202
    69
by (simp add: chain_def less_fun_def)
huffman@16202
    70
huffman@16202
    71
huffman@16202
    72
text {* upper bounds of function chains yield upper bound in the po range *}
huffman@16202
    73
huffman@16202
    74
lemma ub2ub_fun:
huffman@16202
    75
  "range (S::nat \<Rightarrow> 'a \<Rightarrow> 'b::po) <| u \<Longrightarrow> range (\<lambda>i. S i x) <| u x"
huffman@16202
    76
by (auto simp add: is_ub_def less_fun_def)
huffman@16202
    77
huffman@16202
    78
text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *}
huffman@16202
    79
huffman@16202
    80
lemma lub_fun:
huffman@16202
    81
  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
huffman@16202
    82
    \<Longrightarrow> range S <<| (\<lambda>x. \<Squnion>i. S i x)"
huffman@16202
    83
apply (rule is_lubI)
huffman@16202
    84
apply (rule ub_rangeI)
huffman@16202
    85
apply (rule less_fun_ext)
huffman@16202
    86
apply (rule is_ub_thelub)
huffman@16202
    87
apply (erule ch2ch_fun)
huffman@16202
    88
apply (rule less_fun_ext)
huffman@16202
    89
apply (rule is_lub_thelub)
huffman@16202
    90
apply (erule ch2ch_fun)
huffman@16202
    91
apply (erule ub2ub_fun)
huffman@16202
    92
done
huffman@16202
    93
huffman@16202
    94
lemma thelub_fun:
huffman@16202
    95
  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
huffman@16202
    96
    \<Longrightarrow> lub (range S) = (\<lambda>x. \<Squnion>i. S i x)"
huffman@16202
    97
by (rule lub_fun [THEN thelubI])
huffman@16202
    98
huffman@16202
    99
lemma cpo_fun:
huffman@16202
   100
  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) \<Longrightarrow> \<exists>x. range S <<| x"
huffman@16202
   101
by (rule exI, erule lub_fun)
huffman@16202
   102
huffman@16202
   103
instance fun  :: (type, cpo) cpo
huffman@16202
   104
by intro_classes (rule cpo_fun)
huffman@16202
   105
huffman@16202
   106
instance fun  :: (type, pcpo) pcpo
huffman@16202
   107
by intro_classes (rule least_fun)
huffman@16202
   108
huffman@16202
   109
text {* for compatibility with old HOLCF-Version *}
huffman@16202
   110
lemma inst_fun_pcpo: "UU = (%x. UU)"
huffman@16202
   111
by (rule minimal_fun [THEN UU_I, symmetric])
huffman@16202
   112
huffman@16202
   113
text {* function application is strict in the left argument *}
huffman@16202
   114
lemma app_strict [simp]: "\<bottom> x = \<bottom>"
huffman@16202
   115
by (simp add: inst_fun_pcpo)
huffman@16202
   116
huffman@16202
   117
end
huffman@16202
   118