author | wenzelm |
Mon, 25 Jul 2016 21:50:04 +0200 | |
changeset 63549 | b0d31c7def86 |
parent 62175 | 8ffc4d0e652d |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/ex/Dnat.thy |
2570 | 2 |
Author: Franz Regensburger |
3 |
||
4 |
Theory for the domain of natural numbers dnat = one ++ dnat |
|
5 |
*) |
|
6 |
||
27108 | 7 |
theory Dnat |
8 |
imports HOLCF |
|
9 |
begin |
|
2570 | 10 |
|
11 |
domain dnat = dzero | dsucc (dpred :: dnat) |
|
12 |
||
19763 | 13 |
definition |
63549 | 14 |
iterator :: "dnat \<rightarrow> ('a \<rightarrow> 'a) \<rightarrow> 'a \<rightarrow> 'a" where |
15 |
"iterator = fix\<cdot>(LAM h n f x. |
|
16 |
case n of dzero \<Rightarrow> x |
|
17 |
| dsucc\<cdot>m \<Rightarrow> f\<cdot>(h\<cdot>m\<cdot>f\<cdot>x))" |
|
2570 | 18 |
|
62175 | 19 |
text \<open> |
12035 | 20 |
\medskip Expand fixed point properties. |
62175 | 21 |
\<close> |
12035 | 22 |
|
19764 | 23 |
lemma iterator_def2: |
63549 | 24 |
"iterator = (LAM n f x. case n of dzero \<Rightarrow> x | dsucc\<cdot>m \<Rightarrow> f\<cdot>(iterator\<cdot>m\<cdot>f\<cdot>x))" |
19764 | 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 |
|
12035 | 31 |
|
62175 | 32 |
text \<open>\medskip Recursive properties.\<close> |
12035 | 33 |
|
63549 | 34 |
lemma iterator1: "iterator\<cdot>UU\<cdot>f\<cdot>x = UU" |
12035 | 35 |
apply (subst iterator_def2) |
35169 | 36 |
apply simp |
12035 | 37 |
done |
38 |
||
63549 | 39 |
lemma iterator2: "iterator\<cdot>dzero\<cdot>f\<cdot>x = x" |
12035 | 40 |
apply (subst iterator_def2) |
35169 | 41 |
apply simp |
12035 | 42 |
done |
43 |
||
63549 | 44 |
lemma iterator3: "n \<noteq> UU \<Longrightarrow> iterator\<cdot>(dsucc\<cdot>n)\<cdot>f\<cdot>x = f\<cdot>(iterator\<cdot>n\<cdot>f\<cdot>x)" |
12035 | 45 |
apply (rule trans) |
46 |
apply (subst iterator_def2) |
|
35169 | 47 |
apply simp |
12035 | 48 |
apply (rule refl) |
49 |
done |
|
50 |
||
51 |
lemmas iterator_rews = iterator1 iterator2 iterator3 |
|
52 |
||
63549 | 53 |
lemma dnat_flat: "\<forall>x y::dnat. x \<sqsubseteq> y \<longrightarrow> x = UU \<or> x = y" |
12035 | 54 |
apply (rule allI) |
35781
b7738ab762b1
renamed some lemmas generated by the domain package
huffman
parents:
35532
diff
changeset
|
55 |
apply (induct_tac x) |
12035 | 56 |
apply fast |
57 |
apply (rule allI) |
|
35532
60647586b173
adapt to changed variable name in casedist theorem
huffman
parents:
35443
diff
changeset
|
58 |
apply (case_tac y) |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
16417
diff
changeset
|
59 |
apply simp |
12035 | 60 |
apply simp |
35169 | 61 |
apply simp |
12035 | 62 |
apply (rule allI) |
35532
60647586b173
adapt to changed variable name in casedist theorem
huffman
parents:
35443
diff
changeset
|
63 |
apply (case_tac y) |
45049 | 64 |
apply (fast intro!: bottomI) |
63549 | 65 |
apply (thin_tac "\<forall>y. dnat \<sqsubseteq> y \<longrightarrow> dnat = UU \<or> dnat = y") |
35169 | 66 |
apply simp |
67 |
apply (simp (no_asm_simp)) |
|
35443
2e0f9516947e
change domain package's treatment of variable names in theorems to be like datatype package
huffman
parents:
35169
diff
changeset
|
68 |
apply (drule_tac x="dnata" in spec) |
19550
ae77a20f6995
update to reflect changes in inverts/injects lemmas
huffman
parents:
16417
diff
changeset
|
69 |
apply simp |
12035 | 70 |
done |
2570 | 71 |
|
72 |
end |