author | haftmann |
Tue, 10 Jun 2008 15:30:59 +0200 | |
changeset 27108 | e447b3107696 |
parent 21404 | eb85850d3eb7 |
child 35169 | 31cbcb019003 |
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 |
||
27108 | 8 |
theory Dnat |
9 |
imports HOLCF |
|
10 |
begin |
|
2570 | 11 |
|
12 |
domain dnat = dzero | dsucc (dpred :: dnat) |
|
13 |
||
19763 | 14 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19764
diff
changeset
|
15 |
iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a" where |
19763 | 16 |
"iterator = fix $ (LAM h n f x. |
12035 | 17 |
case n of dzero => x |
18 |
| dsucc $ m => f $ (h $ m $ f $ x))" |
|
2570 | 19 |
|
12035 | 20 |
text {* |
21 |
\medskip Expand fixed point properties. |
|
22 |
*} |
|
23 |
||
19764 | 24 |
lemma iterator_def2: |
25 |
"iterator = (LAM n f x. case n of dzero => x | dsucc$m => f$(iterator$m$f$x))" |
|
26 |
apply (rule trans) |
|
27 |
apply (rule fix_eq2) |
|
28 |
apply (rule iterator_def [THEN eq_reflection]) |
|
29 |
apply (rule beta_cfun) |
|
30 |
apply simp |
|
31 |
done |
|
12035 | 32 |
|
19764 | 33 |
text {* \medskip Recursive properties. *} |
12035 | 34 |
|
35 |
lemma iterator1: "iterator $ UU $ f $ x = UU" |
|
36 |
apply (subst iterator_def2) |
|
37 |
apply (simp add: dnat.rews) |
|
38 |
done |
|
39 |
||
40 |
lemma iterator2: "iterator $ dzero $ f $ x = x" |
|
41 |
apply (subst iterator_def2) |
|
42 |
apply (simp add: dnat.rews) |
|
43 |
done |
|
44 |
||
45 |
lemma iterator3: "n ~= UU ==> iterator $ (dsucc $ n) $ f $ x = f $ (iterator $ n $ f $ x)" |
|
46 |
apply (rule trans) |
|
47 |
apply (subst iterator_def2) |
|
48 |
apply (simp add: dnat.rews) |
|
49 |
apply (rule refl) |
|
50 |
done |
|
51 |
||
52 |
lemmas iterator_rews = iterator1 iterator2 iterator3 |
|
53 |
||
54 |
lemma dnat_flat: "ALL x y::dnat. x<<y --> x=UU | x=y" |
|
55 |
apply (rule allI) |
|
56 |
apply (induct_tac x rule: dnat.ind) |
|
57 |
apply fast |
|
58 |
apply (rule allI) |
|
59 |
apply (rule_tac x = y in dnat.casedist) |
|
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
16417
diff
changeset
|
60 |
apply simp |
12035 | 61 |
apply simp |
62 |
apply (simp add: dnat.dist_les) |
|
63 |
apply (rule allI) |
|
64 |
apply (rule_tac x = y in dnat.casedist) |
|
65 |
apply (fast intro!: UU_I) |
|
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
16417
diff
changeset
|
66 |
apply (thin_tac "ALL y. d << y --> d = UU | d = y") |
12035 | 67 |
apply (simp add: dnat.dist_les) |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
16417
diff
changeset
|
68 |
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
|
69 |
apply (drule_tac x="da" in spec) |
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
16417
diff
changeset
|
70 |
apply simp |
12035 | 71 |
done |
2570 | 72 |
|
73 |
end |