# HG changeset patch
# User huffman
# Date 1109801716 -3600
# Node ID c899efea601fd0e4a932a83fec96b3024c659561
# Parent  9e125b67525345a39210b4431b8f41cfec60891f
converted to new-style theory

diff -r 9e125b675253 -r c899efea601f src/HOLCF/Fun1.ML
--- a/src/HOLCF/Fun1.ML	Wed Mar 02 22:57:08 2005 +0100
+++ b/src/HOLCF/Fun1.ML	Wed Mar 02 23:15:16 2005 +0100
@@ -1,31 +1,7 @@
-(*  Title:      HOLCF/Fun1.ML
-    ID:         $Id$
-    Author:     Franz Regensburger
 
-Definition of the partial ordering for the type of all functions => (fun)
-*)
-
-(* ------------------------------------------------------------------------ *)
-(* less_fun is a partial order on 'a => 'b                                  *)
-(* ------------------------------------------------------------------------ *)
-
-val prems = goalw thy [less_fun_def] "(f::'a::type =>'b::po) << f";
-by (fast_tac (HOL_cs addSIs [refl_less]) 1);
-qed "refl_less_fun";
+(* legacy ML bindings *)
 
-val prems = goalw Fun1.thy [less_fun_def] 
-        "[|(f1::'a::type =>'b::po) << f2; f2 << f1|] ==> f1 = f2";
-by (cut_facts_tac prems 1);
-by (stac expand_fun_eq 1);
-by (fast_tac (HOL_cs addSIs [antisym_less]) 1);
-qed "antisym_less_fun";
-
-val prems = goalw Fun1.thy [less_fun_def] 
-        "[|(f1::'a::type =>'b::po) << f2; f2 << f3 |] ==> f1 << f3";
-by (cut_facts_tac prems 1);
-by (strip_tac 1);
-by (rtac trans_less 1);
-by (etac allE 1);
-by (atac 1);
-by ((etac allE 1) THEN (atac 1));
-qed "trans_less_fun";
+val less_fun_def = thm "less_fun_def";
+val refl_less_fun = thm "refl_less_fun";
+val antisym_less_fun = thm "antisym_less_fun";
+val trans_less_fun = thm "trans_less_fun";
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<chfin (flat_imp_chfin)
+instance flat<chfin
+apply (intro_classes)
+apply (rule flat_imp_chfin)
+done
 
 (* to make << defineable: *)
-instance fun  :: (type, sq_ord) sq_ord
+
+instance fun  :: (type, sq_ord) sq_ord ..
+
+defs (overloaded)
+  less_fun_def: "(op <<) == (%f1 f2.!x. f1 x << f2 x)"  
+
+(*  Title:      HOLCF/Fun1.ML
+    ID:         $Id$
+    Author:     Franz Regensburger
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
+
+Definition of the partial ordering for the type of all functions => (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
 
 
diff -r 9e125b675253 -r c899efea601f src/HOLCF/Fun2.ML
--- a/src/HOLCF/Fun2.ML	Wed Mar 02 22:57:08 2005 +0100
+++ b/src/HOLCF/Fun2.ML	Wed Mar 02 23:15:16 2005 +0100
@@ -1,81 +1,13 @@
-(*  Title:      HOLCF/Fun2.ML
-    ID:         $Id$
-    Author:     Franz Regensburger
-*)
 
-(* for compatibility with old HOLCF-Version *)
-Goal "(op <<)=(%f g.!x. f x << g x)";
-by (fold_goals_tac [less_fun_def]);
-by (rtac refl 1);
-qed "inst_fun_po";
-
-(* ------------------------------------------------------------------------ *)
-(* Type 'a::type => 'b::pcpo is pointed                                     *)
-(* ------------------------------------------------------------------------ *)
-
-Goal "(%z. UU) << x";
-by (simp_tac (simpset() addsimps [inst_fun_po,minimal]) 1);
-qed "minimal_fun";
-
-bind_thm ("UU_fun_def",minimal_fun RS minimal2UU RS sym);
-
-Goal "? x::'a=>'b::pcpo.!y. x<<y";
-by (res_inst_tac [("x","(%z. UU)")] exI 1);
-by (rtac (minimal_fun RS allI) 1);
-qed "least_fun";
-
-(* ------------------------------------------------------------------------ *)
-(* make the symbol << accessible for type fun                               *)
-(* ------------------------------------------------------------------------ *)
-
-Goal "(f1 << f2) = (! x. f1(x) << f2(x))";
-by (stac inst_fun_po 1);
-by (rtac refl 1);
-qed "less_fun";
-
-(* ------------------------------------------------------------------------ *)
-(* chains of functions yield chains in the po range                         *)
-(* ------------------------------------------------------------------------ *)
+(* legacy ML bindings *)
 
-Goalw [chain_def] "chain (S::nat=>('a=>'b::po)) ==> chain (%i. S i x)";
-by (asm_full_simp_tac (simpset() addsimps [less_fun]) 1);
-qed "ch2ch_fun";
-
-(* ------------------------------------------------------------------------ *)
-(* upper bounds of function chains yield upper bound in the po range        *)
-(* ------------------------------------------------------------------------ *)
-
-Goal "range(S::nat=>('a::type => 'b::po)) <| u ==> range(%i. S i x) <| u(x)";
-by (rtac ub_rangeI 1);
-by (dtac ub_rangeD 1);
-by (asm_full_simp_tac (simpset() addsimps [less_fun]) 1);
-by Auto_tac; 	
-qed "ub2ub_fun";
-
-(* ------------------------------------------------------------------------ *)
-(* Type 'a::type => 'b::pcpo is chain complete                              *)
-(* ------------------------------------------------------------------------ *)
-
-Goal "chain(S::nat=>('a::type => 'b::cpo)) ==> \
-\        range(S) <<| (% x. lub(range(% i. S(i)(x))))";
-by (rtac is_lubI 1);
-by (rtac ub_rangeI 1);
-by (stac less_fun 1);
-by (rtac allI 1);
-by (rtac is_ub_thelub 1);
-by (etac ch2ch_fun 1);
-by (strip_tac 1);
-by (stac less_fun 1);
-by (rtac allI 1);
-by (rtac is_lub_thelub 1);
-by (etac ch2ch_fun 1);
-by (etac ub2ub_fun 1);
-qed "lub_fun";
-
-bind_thm ("thelub_fun", lub_fun RS thelubI);
-(* chain ?S1 ==> lub (range ?S1) = (%x. lub (range (%i. ?S1 i x))) *)
-
-Goal "chain(S::nat=>('a::type => 'b::cpo)) ==> ? x. range(S) <<| x";
-by (rtac exI 1);
-by (etac lub_fun 1);
-qed "cpo_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";
+val ub2ub_fun = thm "ub2ub_fun";
+val lub_fun = thm "lub_fun";
+val thelub_fun = thm "thelub_fun";
+val cpo_fun = thm "cpo_fun";
diff -r 9e125b675253 -r c899efea601f src/HOLCF/Fun2.thy
--- a/src/HOLCF/Fun2.thy	Wed Mar 02 22:57:08 2005 +0100
+++ b/src/HOLCF/Fun2.thy	Wed Mar 02 23:15:16 2005 +0100
@@ -1,13 +1,104 @@
 (*  Title:      HOLCF/Fun2.thy
     ID:         $Id$
     Author:     Franz Regensburger
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
-Fun2 = Fun1 + 
+theory Fun2 = Fun1:
 
 (* default class is still type!*)
 
-instance fun  :: (type, po) po (refl_less_fun,antisym_less_fun,trans_less_fun)
+instance fun  :: (type, po) po
+apply (intro_classes)
+apply (rule refl_less_fun)
+apply (rule antisym_less_fun, assumption+)
+apply (rule trans_less_fun, assumption+)
+done
+
+(*  Title:      HOLCF/Fun2.ML
+    ID:         $Id$
+    Author:     Franz Regensburger
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
+*)
+
+(* 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
+
+(* ------------------------------------------------------------------------ *)
+(* Type 'a::type => 'b::pcpo is pointed                                     *)
+(* ------------------------------------------------------------------------ *)
+
+lemma minimal_fun: "(%z. UU) << x"
+apply (simp (no_asm) add: inst_fun_po minimal)
+done
+
+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)
+apply (rule minimal_fun [THEN allI])
+done
+
+(* ------------------------------------------------------------------------ *)
+(* make the symbol << accessible for type fun                               *)
+(* ------------------------------------------------------------------------ *)
+
+lemma less_fun: "(f1 << f2) = (! x. f1(x) << f2(x))"
+apply (subst inst_fun_po)
+apply (rule refl)
+done
+
+(* ------------------------------------------------------------------------ *)
+(* 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
+
+(* ------------------------------------------------------------------------ *)
+(* 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
+
+(* ------------------------------------------------------------------------ *)
+(* Type 'a::type => 'b::pcpo is chain complete                              *)
+(* ------------------------------------------------------------------------ *)
+
+lemma lub_fun: "chain(S::nat=>('a::type => 'b::cpo)) ==>  
+         range(S) <<| (% x. lub(range(% i. S(i)(x))))"
+apply (rule is_lubI)
+apply (rule ub_rangeI)
+apply (subst less_fun)
+apply (rule allI)
+apply (rule is_ub_thelub)
+apply (erule ch2ch_fun)
+(* apply (intro strip) *)
+apply (subst less_fun)
+apply (rule allI)
+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 cpo_fun: "chain(S::nat=>('a::type => 'b::cpo)) ==> ? x. range(S) <<| x"
+apply (rule exI)
+apply (erule lub_fun)
+done
 
 end
 
diff -r 9e125b675253 -r c899efea601f src/HOLCF/Fun3.ML
--- a/src/HOLCF/Fun3.ML	Wed Mar 02 22:57:08 2005 +0100
+++ b/src/HOLCF/Fun3.ML	Wed Mar 02 23:15:16 2005 +0100
@@ -1,9 +1,4 @@
-(*  Title:      HOLCF/Fun3.ML
-    ID:         $Id$
-    Author:     Franz Regensburger
-*)
 
-(* for compatibility with old HOLCF-Version *)
-Goal "UU = (%x. UU)";
-by (simp_tac (HOL_ss addsimps [UU_def,UU_fun_def]) 1);
-qed "inst_fun_pcpo";
+(* legacy ML bindings *)
+
+val inst_fun_pcpo = thm "inst_fun_pcpo";
diff -r 9e125b675253 -r c899efea601f src/HOLCF/Fun3.thy
--- a/src/HOLCF/Fun3.thy	Wed Mar 02 22:57:08 2005 +0100
+++ b/src/HOLCF/Fun3.thy	Wed Mar 02 23:15:16 2005 +0100
@@ -1,16 +1,35 @@
 (*  Title:      HOLCF/Fun3.thy
     ID:         $Id$
     Author:     Franz Regensburger
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Class instance of  => (fun) for class pcpo
 *)
 
-Fun3 = Fun2 +
+theory Fun3 = Fun2:
 
 (* default class is still type *)
 
-instance fun  :: (type, cpo) cpo         (cpo_fun)
-instance fun  :: (type, pcpo)pcpo       (least_fun)
+instance fun  :: (type, cpo) cpo
+apply (intro_classes)
+apply (erule cpo_fun)
+done
+
+instance fun  :: (type, pcpo)pcpo
+apply (intro_classes)
+apply (rule least_fun)
+done
+
+(*  Title:      HOLCF/Fun3.ML
+    ID:         $Id$
+    Author:     Franz Regensburger
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
+*)
+
+(* for compatibility with old HOLCF-Version *)
+lemma inst_fun_pcpo: "UU = (%x. UU)"
+apply (simp add: UU_def UU_fun_def)
+done
 
 end