|
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 {* Type @{typ "'a => 'b"} 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 less_fun: "(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 {* Type @{typ "'a::type => 'b::pcpo"} is pointed *} |
|
52 |
|
53 lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f" |
|
54 by (simp add: less_fun_def) |
|
55 |
|
56 lemma least_fun: "\<exists>x::'a \<Rightarrow> 'b::pcpo. \<forall>y. x \<sqsubseteq> y" |
|
57 apply (rule_tac x = "\<lambda>x. \<bottom>" in exI) |
|
58 apply (rule minimal_fun [THEN allI]) |
|
59 done |
|
60 |
|
61 subsection {* Type @{typ "'a::type => 'b::cpo"} is chain complete *} |
|
62 |
|
63 text {* chains of functions yield chains in the po range *} |
|
64 |
|
65 lemma ch2ch_fun: "chain S \<Longrightarrow> chain (\<lambda>i. S i x)" |
|
66 by (simp add: chain_def less_fun_def) |
|
67 |
|
68 lemma ch2ch_fun_rev: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> chain S" |
|
69 by (simp add: chain_def less_fun_def) |
|
70 |
|
71 |
|
72 text {* upper bounds of function chains yield upper bound in the po range *} |
|
73 |
|
74 lemma ub2ub_fun: |
|
75 "range (S::nat \<Rightarrow> 'a \<Rightarrow> 'b::po) <| u \<Longrightarrow> range (\<lambda>i. S i x) <| u x" |
|
76 by (auto simp add: is_ub_def less_fun_def) |
|
77 |
|
78 text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *} |
|
79 |
|
80 lemma lub_fun: |
|
81 "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) |
|
82 \<Longrightarrow> range S <<| (\<lambda>x. \<Squnion>i. S i x)" |
|
83 apply (rule is_lubI) |
|
84 apply (rule ub_rangeI) |
|
85 apply (rule less_fun_ext) |
|
86 apply (rule is_ub_thelub) |
|
87 apply (erule ch2ch_fun) |
|
88 apply (rule less_fun_ext) |
|
89 apply (rule is_lub_thelub) |
|
90 apply (erule ch2ch_fun) |
|
91 apply (erule ub2ub_fun) |
|
92 done |
|
93 |
|
94 lemma thelub_fun: |
|
95 "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) |
|
96 \<Longrightarrow> lub (range S) = (\<lambda>x. \<Squnion>i. S i x)" |
|
97 by (rule lub_fun [THEN thelubI]) |
|
98 |
|
99 lemma cpo_fun: |
|
100 "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) \<Longrightarrow> \<exists>x. range S <<| x" |
|
101 by (rule exI, erule lub_fun) |
|
102 |
|
103 instance fun :: (type, cpo) cpo |
|
104 by intro_classes (rule cpo_fun) |
|
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: "UU = (%x. UU)" |
|
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 |