src/HOL/Induct/Tree.thy
author paulson
Wed, 25 May 2005 16:14:40 +0200
changeset 16078 e1364521a250
parent 14981 e73f8140af78
child 16174 a55c796b1f79
permissions -rw-r--r--
new Brouwer ordinal example
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7018
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
     1
(*  Title:      HOL/Induct/Tree.thy
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
     2
    ID:         $Id$
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
     3
    Author:     Stefan Berghofer,  TU Muenchen
16078
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
     4
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
7018
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
     5
*)
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
     6
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 7018
diff changeset
     7
header {* Infinitely branching trees *}
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 7018
diff changeset
     8
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 7018
diff changeset
     9
theory Tree = Main:
7018
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
    10
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 7018
diff changeset
    11
datatype 'a tree =
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 7018
diff changeset
    12
    Atom 'a
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 7018
diff changeset
    13
  | Branch "nat => 'a tree"
7018
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
    14
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
    15
consts
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
    16
  map_tree :: "('a => 'b) => 'a tree => 'b tree"
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
    17
primrec
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
    18
  "map_tree f (Atom a) = Atom (f a)"
11046
b5f5942781a0 Induct: converted some theories to new-style 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 new-style format;
wenzelm
parents: 7018
diff changeset
    20
b5f5942781a0 Induct: converted some theories to new-style 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
dc87f33db447 tuned inductions;
wenzelm
parents: 11649
diff changeset
    22
  by (induct t) simp_all
7018
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
    23
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
    24
consts
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
    25
  exists_tree :: "('a => bool) => 'a tree => bool"
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
    26
primrec
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
    27
  "exists_tree P (Atom a) = P a"
11046
b5f5942781a0 Induct: converted some theories to new-style 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 new-style format;
wenzelm
parents: 7018
diff changeset
    29
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 7018
diff changeset
    30
lemma exists_map:
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 7018
diff changeset
    31
  "(!!x. P x ==> Q (f x)) ==>
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 7018
diff changeset
    32
    exists_tree P ts ==> exists_tree Q (map_tree f ts)"
12171
dc87f33db447 tuned inductions;
wenzelm
parents: 11649
diff changeset
    33
  by (induct ts) auto
7018
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
    34
16078
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    35
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    36
subsection{*The Brouwer ordinals, as in ZF/Induct/Brouwer.thy.*}
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    37
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    38
datatype brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer"
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    39
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    40
text{*Addition of ordinals*}
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    41
consts
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    42
  add :: "[brouwer,brouwer] => brouwer"
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    43
primrec
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    44
  "add i Zero = i"
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    45
  "add i (Succ j) = Succ (add i j)"
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    46
  "add i (Lim f) = Lim (%n. add i (f n))"
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    47
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    48
lemma add_assoc: "add (add i j) k = add i (add j k)"
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    49
by (induct k, auto)
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    50
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    51
text{*Multiplication of ordinals*}
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    52
consts
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    53
  mult :: "[brouwer,brouwer] => brouwer"
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    54
primrec
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    55
  "mult i Zero = Zero"
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    56
  "mult i (Succ j) = add (mult i j) i"
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    57
  "mult i (Lim f) = Lim (%n. mult i (f n))"
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    58
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    59
lemma add_mult_distrib: "mult i (add j k) = add (mult i j) (mult i k)"
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    60
apply (induct k) 
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    61
apply (auto simp add: add_assoc) 
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    62
done
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    63
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    64
lemma mult_assoc: "mult (mult i j) k = mult i (mult j k)"
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    65
apply (induct k) 
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    66
apply (auto simp add: add_mult_distrib) 
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    67
done
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    68
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    69
text{*We could probably instantiate some axiomatic type classes and use
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    70
the standard infix operators.*}
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    71
7018
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
    72
end