diff -r 9e125b675253 -r c899efea601f src/HOLCF/Fun1.thy --- a/src/HOLCF/Fun1.thy Wed Mar 02 22:57:08 2005 +0100 +++ b/src/HOLCF/Fun1.thy Wed Mar 02 23:15:16 2005 +0100 @@ -1,21 +1,63 @@ (* Title: HOLCF/Fun1.thy ID: $Id$ Author: Franz Regensburger + License: GPL (GNU GENERAL PUBLIC LICENSE) Definition of the partial ordering for the type of all functions => (fun) REMARK: The ordering on 'a => 'b is only defined if 'b is in class po !! *) -Fun1 = Pcpo + +theory Fun1 = Pcpo: -instance flat (fun) +*) + +(* ------------------------------------------------------------------------ *) +(* less_fun is a partial order on 'a => 'b *) +(* ------------------------------------------------------------------------ *) -defs - less_fun_def "(op <<) == (%f1 f2.!x. f1 x << f2 x)" +lemma refl_less_fun: "(f::'a::type =>'b::po) << f" +apply (unfold less_fun_def) +apply (fast intro!: refl_less) +done + +lemma antisym_less_fun: + "[|(f1::'a::type =>'b::po) << f2; f2 << f1|] ==> f1 = f2" +apply (unfold less_fun_def) +(* apply (cut_tac prems) *) +apply (subst expand_fun_eq) +apply (fast intro!: antisym_less) +done + +lemma trans_less_fun: + "[|(f1::'a::type =>'b::po) << f2; f2 << f3 |] ==> f1 << f3" +apply (unfold less_fun_def) +(* apply (cut_tac prems) *) +apply clarify +apply (rule trans_less) +apply (erule allE) +apply assumption +apply (erule allE, assumption) +done + end