author  paulson 
Wed, 25 May 2005 16:14:40 +0200  
changeset 16078  e1364521a250 
parent 14981  e73f8140af78 
child 16174  a55c796b1f79 
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 

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

9 
theory Tree = Main: 
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)" 

49 
by (induct k, auto) 

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

60 
apply (induct k) 

61 
apply (auto simp add: add_assoc) 

62 
done 

63 

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

65 
apply (induct k) 

66 
apply (auto simp add: add_mult_distrib) 

67 
done 

68 

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

70 
the standard infix operators.*} 

71 

7018  72 
end 