|
2570
|
1 |
(* Title: HOLCF/Dnat.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Franz Regensburger
|
|
12035
|
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE)
|
|
2570
|
5 |
|
|
|
6 |
Theory for the domain of natural numbers dnat = one ++ dnat
|
|
|
7 |
*)
|
|
|
8 |
|
|
12035
|
9 |
theory Dnat = HOLCF:
|
|
2570
|
10 |
|
|
|
11 |
domain dnat = dzero | dsucc (dpred :: dnat)
|
|
|
12 |
|
|
|
13 |
constdefs
|
|
12035
|
14 |
iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a"
|
|
|
15 |
"iterator == fix $ (LAM h n f x.
|
|
|
16 |
case n of dzero => x
|
|
|
17 |
| dsucc $ m => f $ (h $ m $ f $ x))"
|
|
2570
|
18 |
|
|
12035
|
19 |
text {*
|
|
|
20 |
\medskip Expand fixed point properties.
|
|
|
21 |
*}
|
|
|
22 |
|
|
|
23 |
ML_setup {*
|
|
|
24 |
bind_thm ("iterator_def2", fix_prover2 (the_context ()) (thm "iterator_def")
|
|
|
25 |
"iterator = (LAM n f x. case n of dzero => x | dsucc$m => f$(iterator$m$f$x))");
|
|
|
26 |
*}
|
|
|
27 |
|
|
|
28 |
text {*
|
|
|
29 |
\medskip Recursive properties.
|
|
|
30 |
*}
|
|
|
31 |
|
|
|
32 |
lemma iterator1: "iterator $ UU $ f $ x = UU"
|
|
|
33 |
apply (subst iterator_def2)
|
|
|
34 |
apply (simp add: dnat.rews)
|
|
|
35 |
done
|
|
|
36 |
|
|
|
37 |
lemma iterator2: "iterator $ dzero $ f $ x = x"
|
|
|
38 |
apply (subst iterator_def2)
|
|
|
39 |
apply (simp add: dnat.rews)
|
|
|
40 |
done
|
|
|
41 |
|
|
|
42 |
lemma iterator3: "n ~= UU ==> iterator $ (dsucc $ n) $ f $ x = f $ (iterator $ n $ f $ x)"
|
|
|
43 |
apply (rule trans)
|
|
|
44 |
apply (subst iterator_def2)
|
|
|
45 |
apply (simp add: dnat.rews)
|
|
|
46 |
apply (rule refl)
|
|
|
47 |
done
|
|
|
48 |
|
|
|
49 |
lemmas iterator_rews = iterator1 iterator2 iterator3
|
|
|
50 |
|
|
|
51 |
lemma dnat_flat: "ALL x y::dnat. x<<y --> x=UU | x=y"
|
|
|
52 |
apply (rule allI)
|
|
|
53 |
apply (induct_tac x rule: dnat.ind)
|
|
|
54 |
apply fast
|
|
|
55 |
apply (rule allI)
|
|
|
56 |
apply (rule_tac x = y in dnat.casedist)
|
|
|
57 |
apply (fast intro!: UU_I)
|
|
|
58 |
apply simp
|
|
|
59 |
apply (simp add: dnat.dist_les)
|
|
|
60 |
apply (rule allI)
|
|
|
61 |
apply (rule_tac x = y in dnat.casedist)
|
|
|
62 |
apply (fast intro!: UU_I)
|
|
|
63 |
apply (simp add: dnat.dist_les)
|
|
|
64 |
apply (simp (no_asm_simp) add: dnat.rews)
|
|
|
65 |
apply (intro strip)
|
|
|
66 |
apply (subgoal_tac "d << da")
|
|
|
67 |
apply (erule allE)
|
|
|
68 |
apply (drule mp)
|
|
|
69 |
apply assumption
|
|
|
70 |
apply (erule disjE)
|
|
|
71 |
apply (tactic "contr_tac 1")
|
|
|
72 |
apply simp
|
|
|
73 |
apply (erule (2) dnat.inverts)
|
|
|
74 |
done
|
|
2570
|
75 |
|
|
|
76 |
end
|