1 (* Title: HOLCF/Dnat.ML |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993, 1995 Technische Universitaet Muenchen |
|
5 |
|
6 *) |
|
7 |
|
8 open Dnat; |
|
9 |
|
10 (* ------------------------------------------------------------------------- *) |
|
11 (* expand fixed point properties *) |
|
12 (* ------------------------------------------------------------------------- *) |
|
13 |
|
14 bind_thm ("iterator_def2", fix_prover2 Dnat.thy iterator_def |
|
15 "iterator = (LAM n f x. case n of dzero => x | \ |
|
16 \ dsucc$m => f$(iterator$m$f$x))"); |
|
17 |
|
18 (* ------------------------------------------------------------------------- *) |
|
19 (* recursive properties *) |
|
20 (* ------------------------------------------------------------------------- *) |
|
21 |
|
22 Goal "iterator$UU$f$x = UU"; |
|
23 by (stac iterator_def2 1); |
|
24 by (simp_tac (HOLCF_ss addsimps dnat.rews) 1); |
|
25 qed "iterator1"; |
|
26 |
|
27 Goal "iterator$dzero$f$x = x"; |
|
28 by (stac iterator_def2 1); |
|
29 by (simp_tac (HOLCF_ss addsimps dnat.rews) 1); |
|
30 qed "iterator2"; |
|
31 |
|
32 Goal "n~=UU ==> iterator$(dsucc$n)$f$x = f$(iterator$n$f$x)"; |
|
33 by (rtac trans 1); |
|
34 by (stac iterator_def2 1); |
|
35 by (asm_simp_tac (HOLCF_ss addsimps dnat.rews) 1); |
|
36 by (rtac refl 1); |
|
37 qed "iterator3"; |
|
38 |
|
39 val iterator_rews = |
|
40 [iterator1, iterator2, iterator3]; |
|
41 |
|
42 Goal "ALL x y::dnat. x<<y --> x=UU | x=y"; |
|
43 by (rtac allI 1); |
|
44 by (res_inst_tac [("x","x")] dnat.ind 1); |
|
45 by (fast_tac HOL_cs 1); |
|
46 by (rtac allI 1); |
|
47 by (res_inst_tac [("x","y")] dnat.casedist 1); |
|
48 by (fast_tac (HOL_cs addSIs [UU_I]) 1); |
|
49 by (Asm_simp_tac 1); |
|
50 by (asm_simp_tac (simpset() addsimps dnat.dist_les) 1); |
|
51 by (rtac allI 1); |
|
52 by (res_inst_tac [("x","y")] dnat.casedist 1); |
|
53 by (fast_tac (HOL_cs addSIs [UU_I]) 1); |
|
54 by (asm_simp_tac (simpset() addsimps dnat.dist_les) 1); |
|
55 by (asm_simp_tac (simpset() addsimps dnat.rews) 1); |
|
56 by (strip_tac 1); |
|
57 by (subgoal_tac "d<<da" 1); |
|
58 by (etac allE 1); |
|
59 by (dtac mp 1); |
|
60 by (atac 1); |
|
61 by (etac disjE 1); |
|
62 by (contr_tac 1); |
|
63 by (Asm_simp_tac 1); |
|
64 by (resolve_tac dnat.inverts 1); |
|
65 by (REPEAT (atac 1)); |
|
66 qed "dnat_flat"; |
|
67 |
|