author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45049  13efaee97111 
child 62175  8ffc4d0e652d 
permissions  rwrr 
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 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19764
diff
changeset

14 
iterator :: "dnat > ('a > 'a) > 'a > 'a" where 
19763  15 
"iterator = fix $ (LAM h n f x. 
12035  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 

19764  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 

12035  31 

19764  32 
text {* \medskip Recursive properties. *} 
12035  33 

34 
lemma iterator1: "iterator $ UU $ f $ x = UU" 

35 
apply (subst iterator_def2) 

35169  36 
apply simp 
12035  37 
done 
38 

39 
lemma iterator2: "iterator $ dzero $ f $ x = x" 

40 
apply (subst iterator_def2) 

35169  41 
apply simp 
12035  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) 

35169  47 
apply simp 
12035  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) 

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) 
35443
2e0f9516947e
change domain package's treatment of variable names in theorems to be like datatype package
huffman
parents:
35169
diff
changeset

65 
apply (thin_tac "ALL y. dnat << y > dnat = UU  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 