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