author  wenzelm 
Wed, 14 Mar 2012 00:34:56 +0100  
changeset 46914  c2ca2c3d23a6 
parent 39246  9e58f0499f57 
child 58249  180f1b3508ed 
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 

46914  16 
primrec map_tree :: "('a => 'b) => 'a tree => 'b tree" 
35419  17 
where 
7018  18 
"map_tree f (Atom a) = Atom (f a)" 
35419  19 
 "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

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 

46914  24 
primrec exists_tree :: "('a => bool) => 'a tree => bool" 
35419  25 
where 
7018  26 
"exists_tree P (Atom a) = P a" 
35419  27 
 "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

28 

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

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

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

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

16078  34 

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

36 

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

38 

39 
text{*Addition of ordinals*} 

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

16078  45 

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

18242  47 
by (induct k) auto 
16078  48 

49 
text{*Multiplication of ordinals*} 

46914  50 
primrec mult :: "[brouwer,brouwer] => brouwer" 
35419  51 
where 
16078  52 
"mult i Zero = Zero" 
35419  53 
 "mult i (Succ j) = add (mult i j) i" 
54 
 "mult i (Lim f) = Lim (%n. mult i (f n))" 

16078  55 

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

18242  57 
by (induct k) (auto simp add: add_assoc) 
16078  58 

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

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

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

63 
the standard infix operators.*} 

64 

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

35439  67 
text{*To use the function package we need an ordering on the Brouwer 
16174  68 
ordinals. Start with a predecessor relation and form its transitive 
69 
closure. *} 

70 

46914  71 
definition brouwer_pred :: "(brouwer * brouwer) set" 
72 
where "brouwer_pred = (\<Union>i. {(m,n). n = Succ m \<or> (EX f. n = Lim f & m = f i)})" 

16174  73 

46914  74 
definition brouwer_order :: "(brouwer * brouwer) set" 
75 
where "brouwer_order = brouwer_pred^+" 

16174  76 

77 
lemma wf_brouwer_pred: "wf brouwer_pred" 

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

79 

35419  80 
lemma wf_brouwer_order[simp]: "wf brouwer_order" 
16174  81 
by(unfold brouwer_order_def, rule wf_trancl[OF wf_brouwer_pred]) 
82 

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

84 
by(auto simp add: brouwer_order_def brouwer_pred_def) 

85 

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

87 
by(auto simp add: brouwer_order_def brouwer_pred_def) 

88 

35419  89 
text{*Example of a general function*} 
90 

46914  91 
function add2 :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer" 
35419  92 
where 
39246  93 
"add2 i Zero = i" 
94 
 "add2 i (Succ j) = Succ (add2 i j)" 

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

35419  96 
by pat_completeness auto 
97 
termination by (relation "inv_image brouwer_order snd") auto 

16174  98 

39246  99 
lemma add2_assoc: "add2 (add2 i j) k = add2 i (add2 j k)" 
18242  100 
by (induct k) auto 
16174  101 

7018  102 
end 