18 subsection {* Type @{typ "'a => 'b"} is a partial order *} |
16 subsection {* Type @{typ "'a => 'b"} is a partial order *} |
19 |
17 |
20 instance fun :: (type, sq_ord) sq_ord .. |
18 instance fun :: (type, sq_ord) sq_ord .. |
21 |
19 |
22 defs (overloaded) |
20 defs (overloaded) |
23 less_fun_def: "(op <<) == (%f1 f2.!x. f1 x << f2 x)" |
21 less_fun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)" |
24 |
22 |
25 lemma refl_less_fun: "(f::'a::type =>'b::po) << f" |
23 lemma refl_less_fun: "(f::'a::type \<Rightarrow> 'b::po) \<sqsubseteq> f" |
26 apply (unfold less_fun_def) |
24 by (simp add: less_fun_def) |
27 apply (fast intro!: refl_less) |
|
28 done |
|
29 |
25 |
30 lemma antisym_less_fun: |
26 lemma antisym_less_fun: |
31 "[|(f1::'a::type =>'b::po) << f2; f2 << f1|] ==> f1 = f2" |
27 "\<lbrakk>(f1::'a::type \<Rightarrow> 'b::po) \<sqsubseteq> f2; f2 \<sqsubseteq> f1\<rbrakk> \<Longrightarrow> f1 = f2" |
32 apply (unfold less_fun_def) |
28 by (simp add: less_fun_def expand_fun_eq antisym_less) |
33 apply (rule ext) |
|
34 apply (fast intro!: antisym_less) |
|
35 done |
|
36 |
29 |
37 lemma trans_less_fun: |
30 lemma trans_less_fun: |
38 "[|(f1::'a::type =>'b::po) << f2; f2 << f3 |] ==> f1 << f3" |
31 "\<lbrakk>(f1::'a::type \<Rightarrow> 'b::po) \<sqsubseteq> f2; f2 \<sqsubseteq> f3\<rbrakk> \<Longrightarrow> f1 \<sqsubseteq> f3" |
39 apply (unfold less_fun_def) |
32 apply (unfold less_fun_def) |
40 apply clarify |
33 apply clarify |
41 apply (rule trans_less) |
34 apply (rule trans_less) |
42 apply (erule allE, assumption) |
35 apply (erule spec) |
43 apply (erule allE, assumption) |
36 apply (erule spec) |
44 done |
37 done |
45 |
|
46 text {* default class is still type! *} |
|
47 |
38 |
48 instance fun :: (type, po) po |
39 instance fun :: (type, po) po |
49 by intro_classes |
40 by intro_classes |
50 (assumption | rule refl_less_fun antisym_less_fun trans_less_fun)+ |
41 (assumption | rule refl_less_fun antisym_less_fun trans_less_fun)+ |
51 |
42 |
52 text {* for compatibility with old HOLCF-Version *} |
|
53 lemma inst_fun_po: "(op <<)=(%f g.!x. f x << g x)" |
|
54 apply (fold less_fun_def) |
|
55 apply (rule refl) |
|
56 done |
|
57 |
|
58 text {* make the symbol @{text "<<"} accessible for type fun *} |
43 text {* make the symbol @{text "<<"} accessible for type fun *} |
59 |
44 |
60 lemma less_fun: "(f1 << f2) = (! x. f1(x) << f2(x))" |
45 lemma less_fun: "(f \<sqsubseteq> g) = (\<forall>x. f x \<sqsubseteq> g x)" |
61 apply (subst inst_fun_po) |
46 by (simp add: less_fun_def) |
62 apply (rule refl) |
47 |
63 done |
48 lemma less_funI: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g" |
|
49 by (simp add: less_fun_def) |
64 |
50 |
65 subsection {* Type @{typ "'a::type => 'b::pcpo"} is pointed *} |
51 subsection {* Type @{typ "'a::type => 'b::pcpo"} is pointed *} |
66 |
52 |
67 lemma minimal_fun: "(%z. UU) << x" |
53 lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f" |
68 apply (simp (no_asm) add: inst_fun_po minimal) |
54 by (simp add: less_fun_def) |
69 done |
|
70 |
55 |
71 lemmas UU_fun_def = minimal_fun [THEN minimal2UU, symmetric, standard] |
56 lemma least_fun: "\<exists>x::'a \<Rightarrow> 'b::pcpo. \<forall>y. x \<sqsubseteq> y" |
72 |
57 apply (rule_tac x = "\<lambda>x. \<bottom>" in exI) |
73 lemma least_fun: "? x::'a=>'b::pcpo.!y. x<<y" |
|
74 apply (rule_tac x = " (%z. UU) " in exI) |
|
75 apply (rule minimal_fun [THEN allI]) |
58 apply (rule minimal_fun [THEN allI]) |
76 done |
59 done |
77 |
60 |
78 subsection {* Type @{typ "'a::type => 'b::pcpo"} is chain complete *} |
61 subsection {* Type @{typ "'a::type => 'b::cpo"} is chain complete *} |
79 |
62 |
80 text {* chains of functions yield chains in the po range *} |
63 text {* chains of functions yield chains in the po range *} |
81 |
64 |
82 lemma ch2ch_fun: "chain (S::nat=>('a=>'b::po)) ==> chain (%i. S i x)" |
65 lemma ch2ch_fun: |
83 apply (unfold chain_def) |
66 "chain (S::nat \<Rightarrow> 'a \<Rightarrow> 'b::po) \<Longrightarrow> chain (\<lambda>i. S i x)" |
84 apply (simp add: less_fun) |
67 by (simp add: chain_def less_fun_def) |
85 done |
|
86 |
68 |
87 text {* upper bounds of function chains yield upper bound in the po range *} |
69 text {* upper bounds of function chains yield upper bound in the po range *} |
88 |
70 |
89 lemma ub2ub_fun: "range(S::nat=>('a::type => 'b::po)) <| u ==> range(%i. S i x) <| u(x)" |
71 lemma ub2ub_fun: |
90 apply (rule ub_rangeI) |
72 "range (S::nat \<Rightarrow> 'a \<Rightarrow> 'b::po) <| u \<Longrightarrow> range (\<lambda>i. S i x) <| u x" |
91 apply (drule ub_rangeD) |
73 by (auto simp add: is_ub_def less_fun_def) |
92 apply (simp add: less_fun) |
|
93 apply auto |
|
94 done |
|
95 |
74 |
96 text {* Type @{typ "'a::type => 'b::pcpo"} is chain complete *} |
75 text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *} |
97 |
76 |
98 lemma lub_fun: "chain(S::nat=>('a::type => 'b::cpo)) ==> |
77 lemma lub_fun: |
99 range(S) <<| (% x. lub(range(% i. S(i)(x))))" |
78 "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) |
|
79 \<Longrightarrow> range S <<| (\<lambda>x. \<Squnion>i. S i x)" |
100 apply (rule is_lubI) |
80 apply (rule is_lubI) |
101 apply (rule ub_rangeI) |
81 apply (rule ub_rangeI) |
102 apply (subst less_fun) |
82 apply (rule less_funI) |
103 apply (rule allI) |
|
104 apply (rule is_ub_thelub) |
83 apply (rule is_ub_thelub) |
105 apply (erule ch2ch_fun) |
84 apply (erule ch2ch_fun) |
106 apply (subst less_fun) |
85 apply (rule less_funI) |
107 apply (rule allI) |
|
108 apply (rule is_lub_thelub) |
86 apply (rule is_lub_thelub) |
109 apply (erule ch2ch_fun) |
87 apply (erule ch2ch_fun) |
110 apply (erule ub2ub_fun) |
88 apply (erule ub2ub_fun) |
111 done |
89 done |
112 |
90 |
113 lemmas thelub_fun = lub_fun [THEN thelubI, standard] |
91 lemma thelub_fun: |
114 (* chain ?S1 ==> lub (range ?S1) = (%x. lub (range (%i. ?S1 i x))) *) |
92 "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) |
|
93 \<Longrightarrow> lub (range S) = (\<lambda>x. \<Squnion>i. S i x)" |
|
94 by (rule lub_fun [THEN thelubI]) |
115 |
95 |
116 lemma cpo_fun: "chain(S::nat=>('a::type => 'b::cpo)) ==> ? x. range(S) <<| x" |
96 lemma cpo_fun: |
117 apply (rule exI) |
97 "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) \<Longrightarrow> \<exists>x. range S <<| x" |
118 apply (erule lub_fun) |
98 by (rule exI, erule lub_fun) |
119 done |
|
120 |
|
121 text {* default class is still type *} |
|
122 |
99 |
123 instance fun :: (type, cpo) cpo |
100 instance fun :: (type, cpo) cpo |
124 by intro_classes (rule cpo_fun) |
101 by intro_classes (rule cpo_fun) |
125 |
102 |
126 instance fun :: (type, pcpo) pcpo |
103 instance fun :: (type, pcpo) pcpo |
127 by intro_classes (rule least_fun) |
104 by intro_classes (rule least_fun) |
128 |
105 |
129 text {* for compatibility with old HOLCF-Version *} |
106 text {* for compatibility with old HOLCF-Version *} |
130 lemma inst_fun_pcpo: "UU = (%x. UU)" |
107 lemma inst_fun_pcpo: "UU = (%x. UU)" |
131 by (simp add: UU_def UU_fun_def) |
108 by (rule minimal_fun [THEN UU_I, symmetric]) |
|
109 |
|
110 lemma UU_app [simp]: "\<bottom> x = \<bottom>" |
|
111 by (simp add: inst_fun_pcpo) |
132 |
112 |
133 end |
113 end |
134 |
114 |