# HG changeset patch
# User wenzelm
# Date 1004809273 -3600
# Node ID f2ee4b5d02f249a0cfb02b71ef88c05e270b2314
# Parent  4471077c4d4fb4a6d05b0c19c0b01f3fc9efec42
converted theory Dnat;

diff -r 4471077c4d4f -r f2ee4b5d02f2 src/HOLCF/IsaMakefile
--- a/src/HOLCF/IsaMakefile	Sat Nov 03 18:40:21 2001 +0100
+++ b/src/HOLCF/IsaMakefile	Sat Nov 03 18:41:13 2001 +0100
@@ -56,7 +56,7 @@
 HOLCF-ex: HOLCF $(LOG)/HOLCF-ex.gz
 
 $(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF ex/Dagstuhl.ML ex/Dagstuhl.thy \
-  ex/Dnat.ML ex/Dnat.thy ex/Fix2.ML ex/Fix2.thy ex/Focus_ex.ML \
+  ex/Dnat.thy ex/Fix2.ML ex/Fix2.thy ex/Focus_ex.ML \
   ex/Focus_ex.thy ex/Hoare.ML ex/Hoare.thy ex/Loop.ML ex/Loop.thy \
   ex/ROOT.ML ex/Stream.ML ex/Stream.thy ex/loeckx.ML \
   ../HOL/Library/Nat_Infinity.thy 
diff -r 4471077c4d4f -r f2ee4b5d02f2 src/HOLCF/ex/Dnat.ML
--- a/src/HOLCF/ex/Dnat.ML	Sat Nov 03 18:40:21 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,67 +0,0 @@
-(*  Title:      HOLCF/Dnat.ML
-    ID:         $Id$
-    Author:     Franz Regensburger
-    Copyright   1993, 1995 Technische Universitaet Muenchen
-
-*)
-
-open Dnat;
-
-(* ------------------------------------------------------------------------- *)
-(* expand fixed point properties                                             *)
-(* ------------------------------------------------------------------------- *)
-
-bind_thm ("iterator_def2", fix_prover2 Dnat.thy iterator_def 
-	"iterator = (LAM n f x. case n of dzero => x | \
-\                                     dsucc$m => f$(iterator$m$f$x))");
-
-(* ------------------------------------------------------------------------- *)
-(* recursive  properties                                                     *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "iterator$UU$f$x = UU";
-by (stac iterator_def2 1);
-by (simp_tac (HOLCF_ss addsimps dnat.rews) 1);
-qed "iterator1";
-
-Goal "iterator$dzero$f$x = x";
-by (stac iterator_def2 1);
-by (simp_tac (HOLCF_ss addsimps dnat.rews) 1);
-qed "iterator2";
-
-Goal "n~=UU ==> iterator$(dsucc$n)$f$x = f$(iterator$n$f$x)";
-by (rtac trans 1);
-by (stac iterator_def2 1);
-by (asm_simp_tac (HOLCF_ss addsimps dnat.rews) 1);
-by (rtac refl 1);
-qed "iterator3";
-
-val iterator_rews = 
-	[iterator1, iterator2, iterator3];
-
-Goal "ALL x y::dnat. x<<y --> x=UU | x=y";
-by (rtac allI 1);
-by (res_inst_tac [("x","x")] dnat.ind 1);
-by (fast_tac HOL_cs 1);
-by (rtac allI 1);
-by (res_inst_tac [("x","y")] dnat.casedist 1);
-by (fast_tac (HOL_cs addSIs [UU_I]) 1);
-by (Asm_simp_tac 1);
-by (asm_simp_tac (simpset() addsimps dnat.dist_les) 1);
-by (rtac allI 1);
-by (res_inst_tac [("x","y")] dnat.casedist 1);
-by (fast_tac (HOL_cs addSIs [UU_I]) 1);
-by (asm_simp_tac (simpset() addsimps dnat.dist_les) 1);
-by (asm_simp_tac (simpset() addsimps dnat.rews) 1);
-by (strip_tac 1);
-by (subgoal_tac "d<<da" 1);
-by (etac allE 1);
-by (dtac mp 1);
-by (atac 1);
-by (etac disjE 1);
-by (contr_tac 1);
-by (Asm_simp_tac 1);
-by (resolve_tac  dnat.inverts 1);
-by (REPEAT (atac 1));
-qed "dnat_flat";
-
diff -r 4471077c4d4f -r f2ee4b5d02f2 src/HOLCF/ex/Dnat.thy
--- a/src/HOLCF/ex/Dnat.thy	Sat Nov 03 18:40:21 2001 +0100
+++ b/src/HOLCF/ex/Dnat.thy	Sat Nov 03 18:41:13 2001 +0100
@@ -1,19 +1,76 @@
 (*  Title:      HOLCF/Dnat.thy
     ID:         $Id$
     Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Theory for the domain of natural numbers  dnat = one ++ dnat
 *)
 
-Dnat = HOLCF +
+theory Dnat = HOLCF:
 
 domain dnat = dzero | dsucc (dpred :: dnat)
 
 constdefs
+  iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a"
+  "iterator == fix $ (LAM h n f x.
+    case n of dzero => x
+      | dsucc $ m => f $ (h $ m $ f $ x))"
 
-iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a"
-            "iterator == fix$(LAM h n f x . case n of dzero   => x
-                                                    | dsucc$m => f$(h$m$f$x))"
+text {*
+  \medskip Expand fixed point properties.
+*}
+
+ML_setup {*
+bind_thm ("iterator_def2", fix_prover2 (the_context ()) (thm "iterator_def")
+        "iterator = (LAM n f x. case n of dzero => x | dsucc$m => f$(iterator$m$f$x))");
+*}
+
+text {*
+  \medskip Recursive properties.
+*}
+
+lemma iterator1: "iterator $ UU $ f $ x = UU"
+  apply (subst iterator_def2)
+  apply (simp add: dnat.rews)
+  done
+
+lemma iterator2: "iterator $ dzero $ f $ x = x"
+  apply (subst iterator_def2)
+  apply (simp add: dnat.rews)
+  done
+
+lemma iterator3: "n ~= UU ==> iterator $ (dsucc $ n) $ f $ x = f $ (iterator $ n $ f $ x)"
+  apply (rule trans)
+   apply (subst iterator_def2)
+   apply (simp add: dnat.rews)
+  apply (rule refl)
+  done
+
+lemmas iterator_rews = iterator1 iterator2 iterator3
+
+lemma dnat_flat: "ALL x y::dnat. x<<y --> x=UU | x=y"
+  apply (rule allI)
+  apply (induct_tac x rule: dnat.ind)
+    apply fast
+   apply (rule allI)
+   apply (rule_tac x = y in dnat.casedist)
+     apply (fast intro!: UU_I)
+    apply simp
+   apply (simp add: dnat.dist_les)
+  apply (rule allI)
+  apply (rule_tac x = y in dnat.casedist)
+    apply (fast intro!: UU_I)
+   apply (simp add: dnat.dist_les)
+  apply (simp (no_asm_simp) add: dnat.rews)
+  apply (intro strip)
+  apply (subgoal_tac "d << da")
+   apply (erule allE)
+   apply (drule mp)
+    apply assumption
+   apply (erule disjE)
+    apply (tactic "contr_tac 1")
+   apply simp
+  apply (erule (2) dnat.inverts)
+  done
 
 end