# HG changeset patch
# User huffman
# Date 1117067188 -7200
# Node ID 1aa809be1e82fdf406d26632780b871e14abe842
# Parent  fca38c55c8fa0f1b3d99c11487c335d774e677a0
cleaned up, added UU_app and less_funI, removed some obsolete stuff

diff -r fca38c55c8fa -r 1aa809be1e82 src/HOLCF/FunCpo.ML
--- a/src/HOLCF/FunCpo.ML	Thu May 26 02:24:41 2005 +0200
+++ b/src/HOLCF/FunCpo.ML	Thu May 26 02:26:28 2005 +0200
@@ -5,9 +5,7 @@
 val refl_less_fun = thm "refl_less_fun";
 val antisym_less_fun = thm "antisym_less_fun";
 val trans_less_fun = thm "trans_less_fun";
-val inst_fun_po = thm "inst_fun_po";
 val minimal_fun = thm "minimal_fun";
-val UU_fun_def = thm "UU_fun_def";
 val least_fun = thm "least_fun";
 val less_fun = thm "less_fun";
 val ch2ch_fun = thm "ch2ch_fun";
diff -r fca38c55c8fa -r 1aa809be1e82 src/HOLCF/FunCpo.thy
--- a/src/HOLCF/FunCpo.thy	Thu May 26 02:24:41 2005 +0200
+++ b/src/HOLCF/FunCpo.thy	Thu May 26 02:26:28 2005 +0200
@@ -4,8 +4,6 @@
 
 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 !!
-
 Class instance of  => (fun) for class pcpo.
 *)
 
@@ -20,105 +18,84 @@
 instance fun  :: (type, sq_ord) sq_ord ..
 
 defs (overloaded)
-  less_fun_def: "(op <<) == (%f1 f2.!x. f1 x << f2 x)"  
+  less_fun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)"  
 
-lemma refl_less_fun: "(f::'a::type =>'b::po) << f"
-apply (unfold less_fun_def)
-apply (fast intro!: refl_less)
-done
+lemma refl_less_fun: "(f::'a::type \<Rightarrow> 'b::po) \<sqsubseteq> f"
+by (simp add: less_fun_def)
 
 lemma antisym_less_fun:
-        "[|(f1::'a::type =>'b::po) << f2; f2 << f1|] ==> f1 = f2"
-apply (unfold less_fun_def)
-apply (rule ext)
-apply (fast intro!: antisym_less)
-done
+  "\<lbrakk>(f1::'a::type \<Rightarrow> 'b::po) \<sqsubseteq> f2; f2 \<sqsubseteq> f1\<rbrakk> \<Longrightarrow> f1 = f2"
+by (simp add: less_fun_def expand_fun_eq antisym_less)
 
 lemma trans_less_fun:
-        "[|(f1::'a::type =>'b::po) << f2; f2 << f3 |] ==> f1 << f3"
+  "\<lbrakk>(f1::'a::type \<Rightarrow> 'b::po) \<sqsubseteq> f2; f2 \<sqsubseteq> f3\<rbrakk> \<Longrightarrow> f1 \<sqsubseteq> f3"
 apply (unfold less_fun_def)
 apply clarify
 apply (rule trans_less)
-apply (erule allE, assumption)
-apply (erule allE, assumption)
+apply (erule spec)
+apply (erule spec)
 done
 
-text {* default class is still type! *}
-
 instance fun  :: (type, po) po
 by intro_classes
   (assumption | rule refl_less_fun antisym_less_fun trans_less_fun)+
 
-text {* for compatibility with old HOLCF-Version *}
-lemma inst_fun_po: "(op <<)=(%f g.!x. f x << g x)"
-apply (fold less_fun_def)
-apply (rule refl)
-done
-
 text {* make the symbol @{text "<<"} accessible for type fun *}
 
-lemma less_fun: "(f1 << f2) = (! x. f1(x) << f2(x))"
-apply (subst inst_fun_po)
-apply (rule refl)
-done
+lemma less_fun: "(f \<sqsubseteq> g) = (\<forall>x. f x \<sqsubseteq> g x)"
+by (simp add: less_fun_def)
+
+lemma less_funI: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
+by (simp add: less_fun_def)
 
 subsection {* Type @{typ "'a::type => 'b::pcpo"} is pointed *}
 
-lemma minimal_fun: "(%z. UU) << x"
-apply (simp (no_asm) add: inst_fun_po minimal)
-done
+lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f"
+by (simp add: less_fun_def)
 
-lemmas UU_fun_def = minimal_fun [THEN minimal2UU, symmetric, standard]
-
-lemma least_fun: "? x::'a=>'b::pcpo.!y. x<<y"
-apply (rule_tac x = " (%z. UU) " in exI)
+lemma least_fun: "\<exists>x::'a \<Rightarrow> 'b::pcpo. \<forall>y. x \<sqsubseteq> y"
+apply (rule_tac x = "\<lambda>x. \<bottom>" in exI)
 apply (rule minimal_fun [THEN allI])
 done
 
-subsection {* Type @{typ "'a::type => 'b::pcpo"} is chain complete *}
+subsection {* Type @{typ "'a::type => 'b::cpo"} is chain complete *}
 
 text {* chains of functions yield chains in the po range *}
 
-lemma ch2ch_fun: "chain (S::nat=>('a=>'b::po)) ==> chain (%i. S i x)"
-apply (unfold chain_def)
-apply (simp add: less_fun)
-done
+lemma ch2ch_fun:
+  "chain (S::nat \<Rightarrow> 'a \<Rightarrow> 'b::po) \<Longrightarrow> chain (\<lambda>i. S i x)"
+by (simp add: chain_def less_fun_def)
 
 text {* upper bounds of function chains yield upper bound in the po range *}
 
-lemma ub2ub_fun: "range(S::nat=>('a::type => 'b::po)) <| u ==> range(%i. S i x) <| u(x)"
-apply (rule ub_rangeI)
-apply (drule ub_rangeD)
-apply (simp add: less_fun)
-apply auto
-done
+lemma ub2ub_fun:
+  "range (S::nat \<Rightarrow> 'a \<Rightarrow> 'b::po) <| u \<Longrightarrow> range (\<lambda>i. S i x) <| u x"
+by (auto simp add: is_ub_def less_fun_def)
 
-text {* Type @{typ "'a::type => 'b::pcpo"} is chain complete *}
+text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *}
 
-lemma lub_fun: "chain(S::nat=>('a::type => 'b::cpo)) ==>  
-         range(S) <<| (% x. lub(range(% i. S(i)(x))))"
+lemma lub_fun:
+  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
+    \<Longrightarrow> range S <<| (\<lambda>x. \<Squnion>i. S i x)"
 apply (rule is_lubI)
 apply (rule ub_rangeI)
-apply (subst less_fun)
-apply (rule allI)
+apply (rule less_funI)
 apply (rule is_ub_thelub)
 apply (erule ch2ch_fun)
-apply (subst less_fun)
-apply (rule allI)
+apply (rule less_funI)
 apply (rule is_lub_thelub)
 apply (erule ch2ch_fun)
 apply (erule ub2ub_fun)
 done
 
-lemmas thelub_fun = lub_fun [THEN thelubI, standard]
-(* chain ?S1 ==> lub (range ?S1) = (%x. lub (range (%i. ?S1 i x))) *)
+lemma thelub_fun:
+  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
+    \<Longrightarrow> lub (range S) = (\<lambda>x. \<Squnion>i. S i x)"
+by (rule lub_fun [THEN thelubI])
 
-lemma cpo_fun: "chain(S::nat=>('a::type => 'b::cpo)) ==> ? x. range(S) <<| x"
-apply (rule exI)
-apply (erule lub_fun)
-done
-
-text {* default class is still type *}
+lemma cpo_fun:
+  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) \<Longrightarrow> \<exists>x. range S <<| x"
+by (rule exI, erule lub_fun)
 
 instance fun  :: (type, cpo) cpo
 by intro_classes (rule cpo_fun)
@@ -128,7 +105,10 @@
 
 text {* for compatibility with old HOLCF-Version *}
 lemma inst_fun_pcpo: "UU = (%x. UU)"
-by (simp add: UU_def UU_fun_def)
+by (rule minimal_fun [THEN UU_I, symmetric])
+
+lemma UU_app [simp]: "\<bottom> x = \<bottom>"
+by (simp add: inst_fun_pcpo)
 
 end