author  haftmann 
Wed, 08 Sep 2010 19:21:46 +0200  
changeset 39246  9e58f0499f57 
parent 35439  888993948a1d 
child 46914  c2ca2c3d23a6 
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 

35419  16 
primrec 
7018  17 
map_tree :: "('a => 'b) => 'a tree => 'b tree" 
35419  18 
where 
7018  19 
"map_tree f (Atom a) = Atom (f a)" 
35419  20 
 "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))" 
11046
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 

35419  25 
primrec 
7018  26 
exists_tree :: "('a => bool) => 'a tree => bool" 
35419  27 
where 
7018  28 
"exists_tree P (Atom a) = P a" 
35419  29 
 "exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))" 
11046
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*} 

35419  42 
primrec 
16078  43 
add :: "[brouwer,brouwer] => brouwer" 
35419  44 
where 
16078  45 
"add i Zero = i" 
35419  46 
 "add i (Succ j) = Succ (add i j)" 
47 
 "add i (Lim f) = Lim (%n. add i (f n))" 

16078  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*} 

35419  53 
primrec 
16078  54 
mult :: "[brouwer,brouwer] => brouwer" 
35419  55 
where 
16078  56 
"mult i Zero = Zero" 
35419  57 
 "mult i (Succ j) = add (mult i j) i" 
58 
 "mult i (Lim f) = Lim (%n. mult i (f n))" 

16078  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 

35439  71 
text{*To use the function package we need an ordering on the Brouwer 
16174  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 

35419  86 
lemma wf_brouwer_order[simp]: "wf brouwer_order" 
16174  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 

35419  95 
text{*Example of a general function*} 
96 

97 
function 

39246  98 
add2 :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer" 
35419  99 
where 
39246  100 
"add2 i Zero = i" 
101 
 "add2 i (Succ j) = Succ (add2 i j)" 

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

35419  103 
by pat_completeness auto 
104 
termination by (relation "inv_image brouwer_order snd") auto 

16174  105 

39246  106 
lemma add2_assoc: "add2 (add2 i j) k = add2 i (add2 j k)" 
18242  107 
by (induct k) auto 
16174  108 

7018  109 
end 