author | kleing |
Fri, 27 May 2005 01:09:44 +0200 | |
changeset 16095 | f6af6b265d20 |
parent 16084 | 1aa809be1e82 |
permissions | -rw-r--r-- |
15600 | 1 |
(* Title: HOLCF/FunCpo.thy |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
2 |
ID: $Id$ |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
3 |
Author: Franz Regensburger |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
4 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
5 |
Definition of the partial ordering for the type of all functions => (fun) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
6 |
|
16070
4a83dd540b88
removed LICENCE note -- everything is subject to Isabelle licence as
wenzelm
parents:
15600
diff
changeset
|
7 |
Class instance of => (fun) for class pcpo. |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
8 |
*) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
9 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
10 |
header {* Class instances for the type of all functions *} |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
11 |
|
15577 | 12 |
theory FunCpo |
13 |
imports Pcpo |
|
14 |
begin |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
15 |
|
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
16 |
subsection {* Type @{typ "'a => 'b"} is a partial order *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
17 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
18 |
instance fun :: (type, sq_ord) sq_ord .. |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
19 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
20 |
defs (overloaded) |
16084
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
21 |
less_fun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)" |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
22 |
|
16084
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
23 |
lemma refl_less_fun: "(f::'a::type \<Rightarrow> 'b::po) \<sqsubseteq> f" |
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
24 |
by (simp add: less_fun_def) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
25 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
26 |
lemma antisym_less_fun: |
16084
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
27 |
"\<lbrakk>(f1::'a::type \<Rightarrow> 'b::po) \<sqsubseteq> f2; f2 \<sqsubseteq> f1\<rbrakk> \<Longrightarrow> f1 = f2" |
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
28 |
by (simp add: less_fun_def expand_fun_eq antisym_less) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
29 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
30 |
lemma trans_less_fun: |
16084
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
31 |
"\<lbrakk>(f1::'a::type \<Rightarrow> 'b::po) \<sqsubseteq> f2; f2 \<sqsubseteq> f3\<rbrakk> \<Longrightarrow> f1 \<sqsubseteq> f3" |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
32 |
apply (unfold less_fun_def) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
33 |
apply clarify |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
34 |
apply (rule trans_less) |
16084
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
35 |
apply (erule spec) |
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
36 |
apply (erule spec) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
37 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
38 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
39 |
instance fun :: (type, po) po |
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
40 |
by intro_classes |
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
41 |
(assumption | rule refl_less_fun antisym_less_fun trans_less_fun)+ |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
42 |
|
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
43 |
text {* make the symbol @{text "<<"} accessible for type fun *} |
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
44 |
|
16084
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
45 |
lemma less_fun: "(f \<sqsubseteq> g) = (\<forall>x. f x \<sqsubseteq> g x)" |
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
46 |
by (simp add: less_fun_def) |
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
47 |
|
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
48 |
lemma less_funI: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g" |
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
49 |
by (simp add: less_fun_def) |
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
50 |
|
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
51 |
subsection {* Type @{typ "'a::type => 'b::pcpo"} is pointed *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
52 |
|
16084
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
53 |
lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f" |
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
54 |
by (simp add: less_fun_def) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
55 |
|
16084
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
56 |
lemma least_fun: "\<exists>x::'a \<Rightarrow> 'b::pcpo. \<forall>y. x \<sqsubseteq> y" |
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
57 |
apply (rule_tac x = "\<lambda>x. \<bottom>" in exI) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
58 |
apply (rule minimal_fun [THEN allI]) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
59 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
60 |
|
16084
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
61 |
subsection {* Type @{typ "'a::type => 'b::cpo"} is chain complete *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
62 |
|
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
63 |
text {* chains of functions yield chains in the po range *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
64 |
|
16084
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
65 |
lemma ch2ch_fun: |
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
66 |
"chain (S::nat \<Rightarrow> 'a \<Rightarrow> 'b::po) \<Longrightarrow> chain (\<lambda>i. S i x)" |
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
67 |
by (simp add: chain_def less_fun_def) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
68 |
|
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
69 |
text {* upper bounds of function chains yield upper bound in the po range *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
70 |
|
16084
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
71 |
lemma ub2ub_fun: |
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
72 |
"range (S::nat \<Rightarrow> 'a \<Rightarrow> 'b::po) <| u \<Longrightarrow> range (\<lambda>i. S i x) <| u x" |
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
73 |
by (auto simp add: is_ub_def less_fun_def) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
74 |
|
16084
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
75 |
text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
76 |
|
16084
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
77 |
lemma lub_fun: |
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
78 |
"chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) |
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
79 |
\<Longrightarrow> range S <<| (\<lambda>x. \<Squnion>i. S i x)" |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
80 |
apply (rule is_lubI) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
81 |
apply (rule ub_rangeI) |
16084
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
82 |
apply (rule less_funI) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
83 |
apply (rule is_ub_thelub) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
84 |
apply (erule ch2ch_fun) |
16084
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
85 |
apply (rule less_funI) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
86 |
apply (rule is_lub_thelub) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
87 |
apply (erule ch2ch_fun) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
88 |
apply (erule ub2ub_fun) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
89 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
90 |
|
16084
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
91 |
lemma thelub_fun: |
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
92 |
"chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) |
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
93 |
\<Longrightarrow> lub (range S) = (\<lambda>x. \<Squnion>i. S i x)" |
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
94 |
by (rule lub_fun [THEN thelubI]) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
95 |
|
16084
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
96 |
lemma cpo_fun: |
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
97 |
"chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) \<Longrightarrow> \<exists>x. range S <<| x" |
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
98 |
by (rule exI, erule lub_fun) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
99 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
100 |
instance fun :: (type, cpo) cpo |
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
101 |
by intro_classes (rule cpo_fun) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
102 |
|
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
103 |
instance fun :: (type, pcpo) pcpo |
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
104 |
by intro_classes (rule least_fun) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
105 |
|
15588
14e3228f18cc
arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
106 |
text {* for compatibility with old HOLCF-Version *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
107 |
lemma inst_fun_pcpo: "UU = (%x. UU)" |
16084
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
108 |
by (rule minimal_fun [THEN UU_I, symmetric]) |
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
109 |
|
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
110 |
lemma UU_app [simp]: "\<bottom> x = \<bottom>" |
1aa809be1e82
cleaned up, added UU_app and less_funI, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
111 |
by (simp add: inst_fun_pcpo) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
112 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
113 |
end |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
114 |