author  haftmann 
Wed, 10 Jun 2009 15:04:31 +0200  
changeset 31602  59df8222c204 
parent 21404  eb85850d3eb7 
child 35419  d78659d1723e 
permissions  rwrr 
7018  1 
(* Title: HOL/Induct/Tree.thy 
2 
Author: Stefan Berghofer, TU Muenchen 

16078  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
7018  4 
*) 
5 

11046
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
7018
diff
changeset

6 
header {* Infinitely branching trees *} 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
7018
diff
changeset

7 

31602  8 
theory Tree 
9 
imports Main 

10 
begin 

7018  11 

11046
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
7018
diff
changeset

12 
datatype 'a tree = 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
7018
diff
changeset

13 
Atom 'a 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
7018
diff
changeset

14 
 Branch "nat => 'a tree" 
7018  15 

16 
consts 

17 
map_tree :: "('a => 'b) => 'a tree => 'b tree" 

18 
primrec 

19 
"map_tree f (Atom a) = Atom (f a)" 

11046
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
7018
diff
changeset

20 
"map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))" 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
7018
diff
changeset

21 

b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
7018
diff
changeset

22 
lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t" 
12171  23 
by (induct t) simp_all 
7018  24 

25 
consts 

26 
exists_tree :: "('a => bool) => 'a tree => bool" 

27 
primrec 

28 
"exists_tree P (Atom a) = P a" 

11046
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
7018
diff
changeset

29 
"exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))" 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
7018
diff
changeset

30 

b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
7018
diff
changeset

31 
lemma exists_map: 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
7018
diff
changeset

32 
"(!!x. P x ==> Q (f x)) ==> 
b5f5942781a0
Induct: converted some theories to newstyle format;
wenzelm
parents:
7018
diff
changeset

33 
exists_tree P ts ==> exists_tree Q (map_tree f ts)" 
12171  34 
by (induct ts) auto 
7018  35 

16078  36 

37 
subsection{*The Brouwer ordinals, as in ZF/Induct/Brouwer.thy.*} 

38 

39 
datatype brouwer = Zero  Succ "brouwer"  Lim "nat => brouwer" 

40 

41 
text{*Addition of ordinals*} 

42 
consts 

43 
add :: "[brouwer,brouwer] => brouwer" 

44 
primrec 

45 
"add i Zero = i" 

46 
"add i (Succ j) = Succ (add i j)" 

47 
"add i (Lim f) = Lim (%n. add i (f n))" 

48 

49 
lemma add_assoc: "add (add i j) k = add i (add j k)" 

18242  50 
by (induct k) auto 
16078  51 

52 
text{*Multiplication of ordinals*} 

53 
consts 

54 
mult :: "[brouwer,brouwer] => brouwer" 

55 
primrec 

56 
"mult i Zero = Zero" 

57 
"mult i (Succ j) = add (mult i j) i" 

58 
"mult i (Lim f) = Lim (%n. mult i (f n))" 

59 

60 
lemma add_mult_distrib: "mult i (add j k) = add (mult i j) (mult i k)" 

18242  61 
by (induct k) (auto simp add: add_assoc) 
16078  62 

63 
lemma mult_assoc: "mult (mult i j) k = mult i (mult j k)" 

18242  64 
by (induct k) (auto simp add: add_mult_distrib) 
16078  65 

66 
text{*We could probably instantiate some axiomatic type classes and use 

67 
the standard infix operators.*} 

68 

16174  69 
subsection{*A WF Ordering for The Brouwer ordinals (Michael Compton)*} 
70 

71 
text{*To define recdef style functions we need an ordering on the Brouwer 

72 
ordinals. Start with a predecessor relation and form its transitive 

73 
closure. *} 

74 

19736  75 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset

76 
brouwer_pred :: "(brouwer * brouwer) set" where 
19736  77 
"brouwer_pred = (\<Union>i. {(m,n). n = Succ m \<or> (EX f. n = Lim f & m = f i)})" 
16174  78 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset

79 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset

80 
brouwer_order :: "(brouwer * brouwer) set" where 
19736  81 
"brouwer_order = brouwer_pred^+" 
16174  82 

83 
lemma wf_brouwer_pred: "wf brouwer_pred" 

84 
by(unfold wf_def brouwer_pred_def, clarify, induct_tac x, blast+) 

85 

86 
lemma wf_brouwer_order: "wf brouwer_order" 

87 
by(unfold brouwer_order_def, rule wf_trancl[OF wf_brouwer_pred]) 

88 

89 
lemma [simp]: "(j, Succ j) : brouwer_order" 

90 
by(auto simp add: brouwer_order_def brouwer_pred_def) 

91 

92 
lemma [simp]: "(f n, Lim f) : brouwer_order" 

93 
by(auto simp add: brouwer_order_def brouwer_pred_def) 

94 

95 
text{*Example of a recdef*} 

96 
consts 

97 
add2 :: "(brouwer*brouwer) => brouwer" 

98 
recdef add2 "inv_image brouwer_order (\<lambda> (x,y). y)" 

99 
"add2 (i, Zero) = i" 

100 
"add2 (i, (Succ j)) = Succ (add2 (i, j))" 

101 
"add2 (i, (Lim f)) = Lim (\<lambda> n. add2 (i, (f n)))" 

102 
(hints recdef_wf: wf_brouwer_order) 

103 

104 
lemma add2_assoc: "add2 (add2 (i, j), k) = add2 (i, add2 (j, k))" 

18242  105 
by (induct k) auto 
16174  106 

7018  107 
end 