author  wenzelm 
Fri, 17 Nov 2006 02:20:03 +0100  
changeset 21404  eb85850d3eb7 
parent 19736  d8d0f8f51d69 
child 31602  59df8222c204 
permissions  rwrr 
7018  1 
(* Title: HOL/Induct/Tree.thy 
2 
ID: $Id$ 

3 
Author: Stefan Berghofer, TU Muenchen 

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

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

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

8 

16417  9 
theory Tree imports Main begin 
7018  10 

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

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

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

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

15 
consts 

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

17 
primrec 

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

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

19 
"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

20 

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

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

24 
consts 

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

26 
primrec 

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

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

28 
"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

29 

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

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

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

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

16078  35 

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

37 

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

39 

40 
text{*Addition of ordinals*} 

41 
consts 

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

43 
primrec 

44 
"add i Zero = i" 

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

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

47 

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

18242  49 
by (induct k) auto 
16078  50 

51 
text{*Multiplication of ordinals*} 

52 
consts 

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

54 
primrec 

55 
"mult i Zero = Zero" 

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

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

58 

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

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

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

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

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

66 
the standard infix operators.*} 

67 

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

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

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

72 
closure. *} 

73 

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

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

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

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

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

82 
lemma wf_brouwer_pred: "wf brouwer_pred" 

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

84 

85 
lemma wf_brouwer_order: "wf brouwer_order" 

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

87 

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

89 
by(auto simp add: brouwer_order_def brouwer_pred_def) 

90 

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

92 
by(auto simp add: brouwer_order_def brouwer_pred_def) 

93 

94 
text{*Example of a recdef*} 

95 
consts 

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

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

98 
"add2 (i, Zero) = i" 

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

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

101 
(hints recdef_wf: wf_brouwer_order) 

102 

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

18242  104 
by (induct k) auto 
16174  105 

7018  106 
end 