1 (* Title: HOLCF/Fun1.thy |
1 (* Title: HOLCF/Fun1.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Franz Regensburger |
3 Author: Franz Regensburger |
|
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
4 |
5 |
5 Definition of the partial ordering for the type of all functions => (fun) |
6 Definition of the partial ordering for the type of all functions => (fun) |
6 |
7 |
7 REMARK: The ordering on 'a => 'b is only defined if 'b is in class po !! |
8 REMARK: The ordering on 'a => 'b is only defined if 'b is in class po !! |
8 *) |
9 *) |
9 |
10 |
10 Fun1 = Pcpo + |
11 theory Fun1 = Pcpo: |
11 |
12 |
12 instance flat<chfin (flat_imp_chfin) |
13 instance flat<chfin |
|
14 apply (intro_classes) |
|
15 apply (rule flat_imp_chfin) |
|
16 done |
13 |
17 |
14 (* to make << defineable: *) |
18 (* to make << defineable: *) |
15 instance fun :: (type, sq_ord) sq_ord |
|
16 |
19 |
17 defs |
20 instance fun :: (type, sq_ord) sq_ord .. |
18 less_fun_def "(op <<) == (%f1 f2.!x. f1 x << f2 x)" |
21 |
|
22 defs (overloaded) |
|
23 less_fun_def: "(op <<) == (%f1 f2.!x. f1 x << f2 x)" |
|
24 |
|
25 (* Title: HOLCF/Fun1.ML |
|
26 ID: $Id$ |
|
27 Author: Franz Regensburger |
|
28 License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
29 |
|
30 Definition of the partial ordering for the type of all functions => (fun) |
|
31 *) |
|
32 |
|
33 (* ------------------------------------------------------------------------ *) |
|
34 (* less_fun is a partial order on 'a => 'b *) |
|
35 (* ------------------------------------------------------------------------ *) |
|
36 |
|
37 lemma refl_less_fun: "(f::'a::type =>'b::po) << f" |
|
38 apply (unfold less_fun_def) |
|
39 apply (fast intro!: refl_less) |
|
40 done |
|
41 |
|
42 lemma antisym_less_fun: |
|
43 "[|(f1::'a::type =>'b::po) << f2; f2 << f1|] ==> f1 = f2" |
|
44 apply (unfold less_fun_def) |
|
45 (* apply (cut_tac prems) *) |
|
46 apply (subst expand_fun_eq) |
|
47 apply (fast intro!: antisym_less) |
|
48 done |
|
49 |
|
50 lemma trans_less_fun: |
|
51 "[|(f1::'a::type =>'b::po) << f2; f2 << f3 |] ==> f1 << f3" |
|
52 apply (unfold less_fun_def) |
|
53 (* apply (cut_tac prems) *) |
|
54 apply clarify |
|
55 apply (rule trans_less) |
|
56 apply (erule allE) |
|
57 apply assumption |
|
58 apply (erule allE, assumption) |
|
59 done |
|
60 |
19 end |
61 end |
20 |
62 |
21 |
63 |
22 |
64 |
23 |
65 |