src/HOL/Induct/Tree.thy
author haftmann
Wed, 08 Sep 2010 19:21:46 +0200
changeset 39246 9e58f0499f57
parent 35439 888993948a1d
child 46914 c2ca2c3d23a6
permissions -rw-r--r--
modernized primrec
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
    Author:     Stefan Berghofer,  TU Muenchen
16078
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
7018
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
     4
*)
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
     5
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 7018
diff changeset
     6
header {* Infinitely branching trees *}
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 7018
diff changeset
     7
31602
59df8222c204 tuned header
haftmann
parents: 21404
diff changeset
     8
theory Tree
59df8222c204 tuned header
haftmann
parents: 21404
diff changeset
     9
imports Main
59df8222c204 tuned header
haftmann
parents: 21404
diff changeset
    10
begin
7018
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
    11
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 7018
diff changeset
    12
datatype 'a tree =
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 7018
diff changeset
    13
    Atom 'a
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 7018
diff changeset
    14
  | Branch "nat => 'a tree"
7018
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
    15
35419
d78659d1723e more recdef (and old primrec) hunting
krauss
parents: 31602
diff changeset
    16
primrec
7018
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
    17
  map_tree :: "('a => 'b) => 'a tree => 'b tree"
35419
d78659d1723e more recdef (and old primrec) hunting
krauss
parents: 31602
diff changeset
    18
where
7018
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
    19
  "map_tree f (Atom a) = Atom (f a)"
35419
d78659d1723e more recdef (and old primrec) hunting
krauss
parents: 31602
diff changeset
    20
| "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 7018
diff changeset
    21
b5f5942781a0 Induct: converted some theories to new-style 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
dc87f33db447 tuned inductions;
wenzelm
parents: 11649
diff changeset
    23
  by (induct t) simp_all
7018
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
    24
35419
d78659d1723e more recdef (and old primrec) hunting
krauss
parents: 31602
diff changeset
    25
primrec
7018
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
    26
  exists_tree :: "('a => bool) => 'a tree => bool"
35419
d78659d1723e more recdef (and old primrec) hunting
krauss
parents: 31602
diff changeset
    27
where
7018
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
    28
  "exists_tree P (Atom a) = P a"
35419
d78659d1723e more recdef (and old primrec) hunting
krauss
parents: 31602
diff changeset
    29
| "exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))"
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 7018
diff changeset
    30
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 7018
diff changeset
    31
lemma exists_map:
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 7018
diff changeset
    32
  "(!!x. P x ==> Q (f x)) ==>
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 7018
diff changeset
    33
    exists_tree P ts ==> exists_tree Q (map_tree f ts)"
12171
dc87f33db447 tuned inductions;
wenzelm
parents: 11649
diff changeset
    34
  by (induct ts) auto
7018
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
    35
16078
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    36
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    37
subsection{*The Brouwer ordinals, as in ZF/Induct/Brouwer.thy.*}
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    38
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    39
datatype brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer"
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    40
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    41
text{*Addition of ordinals*}
35419
d78659d1723e more recdef (and old primrec) hunting
krauss
parents: 31602
diff changeset
    42
primrec
16078
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    43
  add :: "[brouwer,brouwer] => brouwer"
35419
d78659d1723e more recdef (and old primrec) hunting
krauss
parents: 31602
diff changeset
    44
where
16078
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    45
  "add i Zero = i"
35419
d78659d1723e more recdef (and old primrec) hunting
krauss
parents: 31602
diff changeset
    46
| "add i (Succ j) = Succ (add i j)"
d78659d1723e more recdef (and old primrec) hunting
krauss
parents: 31602
diff changeset
    47
| "add i (Lim f) = Lim (%n. add i (f n))"
16078
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    48
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    49
lemma add_assoc: "add (add i j) k = add i (add j k)"
18242
2215049cd29c tuned induct proofs;
wenzelm
parents: 16417
diff changeset
    50
  by (induct k) auto
16078
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    51
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    52
text{*Multiplication of ordinals*}
35419
d78659d1723e more recdef (and old primrec) hunting
krauss
parents: 31602
diff changeset
    53
primrec
16078
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    54
  mult :: "[brouwer,brouwer] => brouwer"
35419
d78659d1723e more recdef (and old primrec) hunting
krauss
parents: 31602
diff changeset
    55
where
16078
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    56
  "mult i Zero = Zero"
35419
d78659d1723e more recdef (and old primrec) hunting
krauss
parents: 31602
diff changeset
    57
| "mult i (Succ j) = add (mult i j) i"
d78659d1723e more recdef (and old primrec) hunting
krauss
parents: 31602
diff changeset
    58
| "mult i (Lim f) = Lim (%n. mult i (f n))"
16078
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    59
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    60
lemma add_mult_distrib: "mult i (add j k) = add (mult i j) (mult i k)"
18242
2215049cd29c tuned induct proofs;
wenzelm
parents: 16417
diff changeset
    61
  by (induct k) (auto simp add: add_assoc)
16078
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    62
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    63
lemma mult_assoc: "mult (mult i j) k = mult i (mult j k)"
18242
2215049cd29c tuned induct proofs;
wenzelm
parents: 16417
diff changeset
    64
  by (induct k) (auto simp add: add_mult_distrib)
16078
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    65
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    66
text{*We could probably instantiate some axiomatic type classes and use
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    67
the standard infix operators.*}
e1364521a250 new Brouwer ordinal example
paulson
parents: 14981
diff changeset
    68
16174
a55c796b1f79 ordering for the ordinals
paulson
parents: 16078
diff changeset
    69
subsection{*A WF Ordering for The Brouwer ordinals (Michael Compton)*}
a55c796b1f79 ordering for the ordinals
paulson
parents: 16078
diff changeset
    70
35439
888993948a1d tuned comment
krauss
parents: 35419
diff changeset
    71
text{*To use the function package we need an ordering on the Brouwer
16174
a55c796b1f79 ordering for the ordinals
paulson
parents: 16078
diff changeset
    72
  ordinals.  Start with a predecessor relation and form its transitive 
a55c796b1f79 ordering for the ordinals
paulson
parents: 16078
diff changeset
    73
  closure. *} 
a55c796b1f79 ordering for the ordinals
paulson
parents: 16078
diff changeset
    74
19736
wenzelm
parents: 18242
diff changeset
    75
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 19736
diff changeset
    76
  brouwer_pred :: "(brouwer * brouwer) set" where
19736
wenzelm
parents: 18242
diff changeset
    77
  "brouwer_pred = (\<Union>i. {(m,n). n = Succ m \<or> (EX f. n = Lim f & m = f i)})"
16174
a55c796b1f79 ordering for the ordinals
paulson
parents: 16078
diff changeset
    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
wenzelm
parents: 18242
diff changeset
    81
  "brouwer_order = brouwer_pred^+"
16174
a55c796b1f79 ordering for the ordinals
paulson
parents: 16078
diff changeset
    82
a55c796b1f79 ordering for the ordinals
paulson
parents: 16078
diff changeset
    83
lemma wf_brouwer_pred: "wf brouwer_pred"
a55c796b1f79 ordering for the ordinals
paulson
parents: 16078
diff changeset
    84
  by(unfold wf_def brouwer_pred_def, clarify, induct_tac x, blast+)
a55c796b1f79 ordering for the ordinals
paulson
parents: 16078
diff changeset
    85
35419
d78659d1723e more recdef (and old primrec) hunting
krauss
parents: 31602
diff changeset
    86
lemma wf_brouwer_order[simp]: "wf brouwer_order"
16174
a55c796b1f79 ordering for the ordinals
paulson
parents: 16078
diff changeset
    87
  by(unfold brouwer_order_def, rule wf_trancl[OF wf_brouwer_pred])
a55c796b1f79 ordering for the ordinals
paulson
parents: 16078
diff changeset
    88
a55c796b1f79 ordering for the ordinals
paulson
parents: 16078
diff changeset
    89
lemma [simp]: "(j, Succ j) : brouwer_order"
a55c796b1f79 ordering for the ordinals
paulson
parents: 16078
diff changeset
    90
  by(auto simp add: brouwer_order_def brouwer_pred_def)
a55c796b1f79 ordering for the ordinals
paulson
parents: 16078
diff changeset
    91
a55c796b1f79 ordering for the ordinals
paulson
parents: 16078
diff changeset
    92
lemma [simp]: "(f n, Lim f) : brouwer_order"
a55c796b1f79 ordering for the ordinals
paulson
parents: 16078
diff changeset
    93
  by(auto simp add: brouwer_order_def brouwer_pred_def)
a55c796b1f79 ordering for the ordinals
paulson
parents: 16078
diff changeset
    94
35419
d78659d1723e more recdef (and old primrec) hunting
krauss
parents: 31602
diff changeset
    95
text{*Example of a general function*}
d78659d1723e more recdef (and old primrec) hunting
krauss
parents: 31602
diff changeset
    96
d78659d1723e more recdef (and old primrec) hunting
krauss
parents: 31602
diff changeset
    97
function
39246
9e58f0499f57 modernized primrec
haftmann
parents: 35439
diff changeset
    98
  add2 :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer"
35419
d78659d1723e more recdef (and old primrec) hunting
krauss
parents: 31602
diff changeset
    99
where
39246
9e58f0499f57 modernized primrec
haftmann
parents: 35439
diff changeset
   100
  "add2 i Zero = i"
9e58f0499f57 modernized primrec
haftmann
parents: 35439
diff changeset
   101
| "add2 i (Succ j) = Succ (add2 i j)"
9e58f0499f57 modernized primrec
haftmann
parents: 35439
diff changeset
   102
| "add2 i (Lim f) = Lim (\<lambda>n. add2 i (f n))"
35419
d78659d1723e more recdef (and old primrec) hunting
krauss
parents: 31602
diff changeset
   103
by pat_completeness auto
d78659d1723e more recdef (and old primrec) hunting
krauss
parents: 31602
diff changeset
   104
termination by (relation "inv_image brouwer_order snd") auto
16174
a55c796b1f79 ordering for the ordinals
paulson
parents: 16078
diff changeset
   105
39246
9e58f0499f57 modernized primrec
haftmann
parents: 35439
diff changeset
   106
lemma add2_assoc: "add2 (add2 i j) k = add2 i (add2 j k)"
18242
2215049cd29c tuned induct proofs;
wenzelm
parents: 16417
diff changeset
   107
  by (induct k) auto
16174
a55c796b1f79 ordering for the ordinals
paulson
parents: 16078
diff changeset
   108
7018
ae18bb3075c3 Infinitely branching trees.
berghofe
parents:
diff changeset
   109
end