converted theory Dnat;
authorwenzelm
Sat Nov 03 18:41:13 2001 +0100 (2001-11-03)
changeset 12035f2ee4b5d02f2
parent 12034 4471077c4d4f
child 12036 49f6c49454c2
converted theory Dnat;
src/HOLCF/IsaMakefile
src/HOLCF/ex/Dnat.ML
src/HOLCF/ex/Dnat.thy
     1.1 --- a/src/HOLCF/IsaMakefile	Sat Nov 03 18:40:21 2001 +0100
     1.2 +++ b/src/HOLCF/IsaMakefile	Sat Nov 03 18:41:13 2001 +0100
     1.3 @@ -56,7 +56,7 @@
     1.4  HOLCF-ex: HOLCF $(LOG)/HOLCF-ex.gz
     1.5  
     1.6  $(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF ex/Dagstuhl.ML ex/Dagstuhl.thy \
     1.7 -  ex/Dnat.ML ex/Dnat.thy ex/Fix2.ML ex/Fix2.thy ex/Focus_ex.ML \
     1.8 +  ex/Dnat.thy ex/Fix2.ML ex/Fix2.thy ex/Focus_ex.ML \
     1.9    ex/Focus_ex.thy ex/Hoare.ML ex/Hoare.thy ex/Loop.ML ex/Loop.thy \
    1.10    ex/ROOT.ML ex/Stream.ML ex/Stream.thy ex/loeckx.ML \
    1.11    ../HOL/Library/Nat_Infinity.thy 
     2.1 --- a/src/HOLCF/ex/Dnat.ML	Sat Nov 03 18:40:21 2001 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,67 +0,0 @@
     2.4 -(*  Title:      HOLCF/Dnat.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Franz Regensburger
     2.7 -    Copyright   1993, 1995 Technische Universitaet Muenchen
     2.8 -
     2.9 -*)
    2.10 -
    2.11 -open Dnat;
    2.12 -
    2.13 -(* ------------------------------------------------------------------------- *)
    2.14 -(* expand fixed point properties                                             *)
    2.15 -(* ------------------------------------------------------------------------- *)
    2.16 -
    2.17 -bind_thm ("iterator_def2", fix_prover2 Dnat.thy iterator_def 
    2.18 -	"iterator = (LAM n f x. case n of dzero => x | \
    2.19 -\                                     dsucc$m => f$(iterator$m$f$x))");
    2.20 -
    2.21 -(* ------------------------------------------------------------------------- *)
    2.22 -(* recursive  properties                                                     *)
    2.23 -(* ------------------------------------------------------------------------- *)
    2.24 -
    2.25 -Goal "iterator$UU$f$x = UU";
    2.26 -by (stac iterator_def2 1);
    2.27 -by (simp_tac (HOLCF_ss addsimps dnat.rews) 1);
    2.28 -qed "iterator1";
    2.29 -
    2.30 -Goal "iterator$dzero$f$x = x";
    2.31 -by (stac iterator_def2 1);
    2.32 -by (simp_tac (HOLCF_ss addsimps dnat.rews) 1);
    2.33 -qed "iterator2";
    2.34 -
    2.35 -Goal "n~=UU ==> iterator$(dsucc$n)$f$x = f$(iterator$n$f$x)";
    2.36 -by (rtac trans 1);
    2.37 -by (stac iterator_def2 1);
    2.38 -by (asm_simp_tac (HOLCF_ss addsimps dnat.rews) 1);
    2.39 -by (rtac refl 1);
    2.40 -qed "iterator3";
    2.41 -
    2.42 -val iterator_rews = 
    2.43 -	[iterator1, iterator2, iterator3];
    2.44 -
    2.45 -Goal "ALL x y::dnat. x<<y --> x=UU | x=y";
    2.46 -by (rtac allI 1);
    2.47 -by (res_inst_tac [("x","x")] dnat.ind 1);
    2.48 -by (fast_tac HOL_cs 1);
    2.49 -by (rtac allI 1);
    2.50 -by (res_inst_tac [("x","y")] dnat.casedist 1);
    2.51 -by (fast_tac (HOL_cs addSIs [UU_I]) 1);
    2.52 -by (Asm_simp_tac 1);
    2.53 -by (asm_simp_tac (simpset() addsimps dnat.dist_les) 1);
    2.54 -by (rtac allI 1);
    2.55 -by (res_inst_tac [("x","y")] dnat.casedist 1);
    2.56 -by (fast_tac (HOL_cs addSIs [UU_I]) 1);
    2.57 -by (asm_simp_tac (simpset() addsimps dnat.dist_les) 1);
    2.58 -by (asm_simp_tac (simpset() addsimps dnat.rews) 1);
    2.59 -by (strip_tac 1);
    2.60 -by (subgoal_tac "d<<da" 1);
    2.61 -by (etac allE 1);
    2.62 -by (dtac mp 1);
    2.63 -by (atac 1);
    2.64 -by (etac disjE 1);
    2.65 -by (contr_tac 1);
    2.66 -by (Asm_simp_tac 1);
    2.67 -by (resolve_tac  dnat.inverts 1);
    2.68 -by (REPEAT (atac 1));
    2.69 -qed "dnat_flat";
    2.70 -
     3.1 --- a/src/HOLCF/ex/Dnat.thy	Sat Nov 03 18:40:21 2001 +0100
     3.2 +++ b/src/HOLCF/ex/Dnat.thy	Sat Nov 03 18:41:13 2001 +0100
     3.3 @@ -1,19 +1,76 @@
     3.4  (*  Title:      HOLCF/Dnat.thy
     3.5      ID:         $Id$
     3.6      Author:     Franz Regensburger
     3.7 -    Copyright   1993 Technische Universitaet Muenchen
     3.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     3.9  
    3.10  Theory for the domain of natural numbers  dnat = one ++ dnat
    3.11  *)
    3.12  
    3.13 -Dnat = HOLCF +
    3.14 +theory Dnat = HOLCF:
    3.15  
    3.16  domain dnat = dzero | dsucc (dpred :: dnat)
    3.17  
    3.18  constdefs
    3.19 +  iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a"
    3.20 +  "iterator == fix $ (LAM h n f x.
    3.21 +    case n of dzero => x
    3.22 +      | dsucc $ m => f $ (h $ m $ f $ x))"
    3.23  
    3.24 -iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a"
    3.25 -            "iterator == fix$(LAM h n f x . case n of dzero   => x
    3.26 -                                                    | dsucc$m => f$(h$m$f$x))"
    3.27 +text {*
    3.28 +  \medskip Expand fixed point properties.
    3.29 +*}
    3.30 +
    3.31 +ML_setup {*
    3.32 +bind_thm ("iterator_def2", fix_prover2 (the_context ()) (thm "iterator_def")
    3.33 +        "iterator = (LAM n f x. case n of dzero => x | dsucc$m => f$(iterator$m$f$x))");
    3.34 +*}
    3.35 +
    3.36 +text {*
    3.37 +  \medskip Recursive properties.
    3.38 +*}
    3.39 +
    3.40 +lemma iterator1: "iterator $ UU $ f $ x = UU"
    3.41 +  apply (subst iterator_def2)
    3.42 +  apply (simp add: dnat.rews)
    3.43 +  done
    3.44 +
    3.45 +lemma iterator2: "iterator $ dzero $ f $ x = x"
    3.46 +  apply (subst iterator_def2)
    3.47 +  apply (simp add: dnat.rews)
    3.48 +  done
    3.49 +
    3.50 +lemma iterator3: "n ~= UU ==> iterator $ (dsucc $ n) $ f $ x = f $ (iterator $ n $ f $ x)"
    3.51 +  apply (rule trans)
    3.52 +   apply (subst iterator_def2)
    3.53 +   apply (simp add: dnat.rews)
    3.54 +  apply (rule refl)
    3.55 +  done
    3.56 +
    3.57 +lemmas iterator_rews = iterator1 iterator2 iterator3
    3.58 +
    3.59 +lemma dnat_flat: "ALL x y::dnat. x<<y --> x=UU | x=y"
    3.60 +  apply (rule allI)
    3.61 +  apply (induct_tac x rule: dnat.ind)
    3.62 +    apply fast
    3.63 +   apply (rule allI)
    3.64 +   apply (rule_tac x = y in dnat.casedist)
    3.65 +     apply (fast intro!: UU_I)
    3.66 +    apply simp
    3.67 +   apply (simp add: dnat.dist_les)
    3.68 +  apply (rule allI)
    3.69 +  apply (rule_tac x = y in dnat.casedist)
    3.70 +    apply (fast intro!: UU_I)
    3.71 +   apply (simp add: dnat.dist_les)
    3.72 +  apply (simp (no_asm_simp) add: dnat.rews)
    3.73 +  apply (intro strip)
    3.74 +  apply (subgoal_tac "d << da")
    3.75 +   apply (erule allE)
    3.76 +   apply (drule mp)
    3.77 +    apply assumption
    3.78 +   apply (erule disjE)
    3.79 +    apply (tactic "contr_tac 1")
    3.80 +   apply simp
    3.81 +  apply (erule (2) dnat.inverts)
    3.82 +  done
    3.83  
    3.84  end