author | wenzelm |
Fri, 02 Jun 2006 20:12:59 +0200 | |
changeset 19764 | 372065f34795 |
parent 19763 | ec18656a2c10 |
child 21404 | eb85850d3eb7 |
permissions | -rw-r--r-- |
2570 | 1 |
(* Title: HOLCF/Dnat.thy |
2 |
ID: $Id$ |
|
3 |
Author: Franz Regensburger |
|
4 |
||
5 |
Theory for the domain of natural numbers dnat = one ++ dnat |
|
6 |
*) |
|
7 |
||
16417 | 8 |
theory Dnat imports HOLCF begin |
2570 | 9 |
|
10 |
domain dnat = dzero | dsucc (dpred :: dnat) |
|
11 |
||
19763 | 12 |
definition |
12035 | 13 |
iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a" |
19763 | 14 |
"iterator = fix $ (LAM h n f x. |
12035 | 15 |
case n of dzero => x |
16 |
| dsucc $ m => f $ (h $ m $ f $ x))" |
|
2570 | 17 |
|
12035 | 18 |
text {* |
19 |
\medskip Expand fixed point properties. |
|
20 |
*} |
|
21 |
||
19764 | 22 |
lemma iterator_def2: |
23 |
"iterator = (LAM n f x. case n of dzero => x | dsucc$m => f$(iterator$m$f$x))" |
|
24 |
apply (rule trans) |
|
25 |
apply (rule fix_eq2) |
|
26 |
apply (rule iterator_def [THEN eq_reflection]) |
|
27 |
apply (rule beta_cfun) |
|
28 |
apply simp |
|
29 |
done |
|
12035 | 30 |
|
19764 | 31 |
text {* \medskip Recursive properties. *} |
12035 | 32 |
|
33 |
lemma iterator1: "iterator $ UU $ f $ x = UU" |
|
34 |
apply (subst iterator_def2) |
|
35 |
apply (simp add: dnat.rews) |
|
36 |
done |
|
37 |
||
38 |
lemma iterator2: "iterator $ dzero $ f $ x = x" |
|
39 |
apply (subst iterator_def2) |
|
40 |
apply (simp add: dnat.rews) |
|
41 |
done |
|
42 |
||
43 |
lemma iterator3: "n ~= UU ==> iterator $ (dsucc $ n) $ f $ x = f $ (iterator $ n $ f $ x)" |
|
44 |
apply (rule trans) |
|
45 |
apply (subst iterator_def2) |
|
46 |
apply (simp add: dnat.rews) |
|
47 |
apply (rule refl) |
|
48 |
done |
|
49 |
||
50 |
lemmas iterator_rews = iterator1 iterator2 iterator3 |
|
51 |
||
52 |
lemma dnat_flat: "ALL x y::dnat. x<<y --> x=UU | x=y" |
|
53 |
apply (rule allI) |
|
54 |
apply (induct_tac x rule: dnat.ind) |
|
55 |
apply fast |
|
56 |
apply (rule allI) |
|
57 |
apply (rule_tac x = y in dnat.casedist) |
|
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
16417
diff
changeset
|
58 |
apply simp |
12035 | 59 |
apply simp |
60 |
apply (simp add: dnat.dist_les) |
|
61 |
apply (rule allI) |
|
62 |
apply (rule_tac x = y in dnat.casedist) |
|
63 |
apply (fast intro!: UU_I) |
|
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
16417
diff
changeset
|
64 |
apply (thin_tac "ALL y. d << y --> d = UU | d = y") |
12035 | 65 |
apply (simp add: dnat.dist_les) |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
16417
diff
changeset
|
66 |
apply (simp (no_asm_simp) add: dnat.rews dnat.injects dnat.inverts) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
16417
diff
changeset
|
67 |
apply (drule_tac x="da" in spec) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
16417
diff
changeset
|
68 |
apply simp |
12035 | 69 |
done |
2570 | 70 |
|
71 |
end |