--- 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
--- 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";
-
--- 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