equal
deleted
inserted
replaced
1 (* Title: HOLCF/Dnat.thy |
|
2 Author: Franz Regensburger |
|
3 |
|
4 Theory for the domain of natural numbers dnat = one ++ dnat |
|
5 *) |
|
6 |
|
7 theory Dnat |
|
8 imports HOLCF |
|
9 begin |
|
10 |
|
11 domain dnat = dzero | dsucc (dpred :: dnat) |
|
12 |
|
13 definition |
|
14 iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a" where |
|
15 "iterator = fix $ (LAM h n f x. |
|
16 case n of dzero => x |
|
17 | dsucc $ m => f $ (h $ m $ f $ x))" |
|
18 |
|
19 text {* |
|
20 \medskip Expand fixed point properties. |
|
21 *} |
|
22 |
|
23 lemma iterator_def2: |
|
24 "iterator = (LAM n f x. case n of dzero => x | dsucc$m => f$(iterator$m$f$x))" |
|
25 apply (rule trans) |
|
26 apply (rule fix_eq2) |
|
27 apply (rule iterator_def [THEN eq_reflection]) |
|
28 apply (rule beta_cfun) |
|
29 apply simp |
|
30 done |
|
31 |
|
32 text {* \medskip Recursive properties. *} |
|
33 |
|
34 lemma iterator1: "iterator $ UU $ f $ x = UU" |
|
35 apply (subst iterator_def2) |
|
36 apply simp |
|
37 done |
|
38 |
|
39 lemma iterator2: "iterator $ dzero $ f $ x = x" |
|
40 apply (subst iterator_def2) |
|
41 apply simp |
|
42 done |
|
43 |
|
44 lemma iterator3: "n ~= UU ==> iterator $ (dsucc $ n) $ f $ x = f $ (iterator $ n $ f $ x)" |
|
45 apply (rule trans) |
|
46 apply (subst iterator_def2) |
|
47 apply simp |
|
48 apply (rule refl) |
|
49 done |
|
50 |
|
51 lemmas iterator_rews = iterator1 iterator2 iterator3 |
|
52 |
|
53 lemma dnat_flat: "ALL x y::dnat. x<<y --> x=UU | x=y" |
|
54 apply (rule allI) |
|
55 apply (induct_tac x) |
|
56 apply fast |
|
57 apply (rule allI) |
|
58 apply (case_tac y) |
|
59 apply simp |
|
60 apply simp |
|
61 apply simp |
|
62 apply (rule allI) |
|
63 apply (case_tac y) |
|
64 apply (fast intro!: UU_I) |
|
65 apply (thin_tac "ALL y. dnat << y --> dnat = UU | dnat = y") |
|
66 apply simp |
|
67 apply (simp (no_asm_simp)) |
|
68 apply (drule_tac x="dnata" in spec) |
|
69 apply simp |
|
70 done |
|
71 |
|
72 end |
|