1 (* Title: HOLCF/Fun1.thy |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
5 |
|
6 Definition of the partial ordering for the type of all functions => (fun) |
|
7 |
|
8 REMARK: The ordering on 'a => 'b is only defined if 'b is in class po !! |
|
9 *) |
|
10 |
|
11 theory Fun1 = Pcpo: |
|
12 |
|
13 instance flat<chfin |
|
14 apply (intro_classes) |
|
15 apply (rule flat_imp_chfin) |
|
16 done |
|
17 |
|
18 (* to make << defineable: *) |
|
19 |
|
20 instance fun :: (type, sq_ord) sq_ord .. |
|
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 |
|
61 end |
|
62 |
|
63 |
|
64 |
|
65 |
|