src/HOLCF/ex/Fixrec_ex.thy
author huffman
Mon, 02 Nov 2009 18:39:41 -0800
changeset 33401 fc43fa403a69
parent 31008 b8f4e351b5bf
child 33428 70ed971a79d1
permissions -rw-r--r--
add fixrec support for HOL pair constructor patterns
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
     1
(*  Title:      HOLCF/ex/Fixrec_ex.thy
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
     2
    Author:     Brian Huffman
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
     3
*)
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
     4
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
     5
header {* Fixrec package examples *}
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
     6
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
     7
theory Fixrec_ex
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
     8
imports HOLCF
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
     9
begin
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    10
31008
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    11
subsection {* Basic @{text fixrec} examples *}
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    12
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    13
text {*
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    14
  Fixrec patterns can mention any constructor defined by the domain
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    15
  package, as well as any of the following built-in constructors:
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    16
  cpair, spair, sinl, sinr, up, ONE, TT, FF.
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    17
*}
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    18
31008
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    19
text {* Typical usage is with lazy constructors. *}
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    20
30158
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 16554
diff changeset
    21
fixrec down :: "'a u \<rightarrow> 'a"
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 16554
diff changeset
    22
where "down\<cdot>(up\<cdot>x) = x"
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    23
31008
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    24
text {* With strict constructors, rewrite rules may require side conditions. *}
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    25
30158
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 16554
diff changeset
    26
fixrec from_sinl :: "'a \<oplus> 'b \<rightarrow> 'a"
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 16554
diff changeset
    27
where "x \<noteq> \<bottom> \<Longrightarrow> from_sinl\<cdot>(sinl\<cdot>x) = x"
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    28
31008
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    29
text {* Lifting can turn a strict constructor into a lazy one. *}
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    30
30158
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 16554
diff changeset
    31
fixrec from_sinl_up :: "'a u \<oplus> 'b \<rightarrow> 'a"
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 16554
diff changeset
    32
where "from_sinl_up\<cdot>(sinl\<cdot>(up\<cdot>x)) = x"
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    33
33401
fc43fa403a69 add fixrec support for HOL pair constructor patterns
huffman
parents: 31008
diff changeset
    34
text {* Fixrec also works with the HOL pair constructor. *}
fc43fa403a69 add fixrec support for HOL pair constructor patterns
huffman
parents: 31008
diff changeset
    35
fc43fa403a69 add fixrec support for HOL pair constructor patterns
huffman
parents: 31008
diff changeset
    36
fixrec down2 :: "'a u \<times> 'b u \<rightarrow> 'a \<times> 'b"
fc43fa403a69 add fixrec support for HOL pair constructor patterns
huffman
parents: 31008
diff changeset
    37
where "down2\<cdot>(up\<cdot>x, up\<cdot>y) = (x, y)"
fc43fa403a69 add fixrec support for HOL pair constructor patterns
huffman
parents: 31008
diff changeset
    38
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    39
31008
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    40
subsection {* Examples using @{text fixpat} *}
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    41
31008
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    42
text {* A type of lazy lists. *}
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    43
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    44
domain 'a llist = lNil | lCons (lazy 'a) (lazy "'a llist")
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    45
31008
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    46
text {* A zip function for lazy lists. *}
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    47
31008
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    48
text {* Notice that the patterns are not exhaustive. *}
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    49
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    50
fixrec
30158
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 16554
diff changeset
    51
  lzip :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 16554
diff changeset
    52
where
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    53
  "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot><x,y>\<cdot>(lzip\<cdot>xs\<cdot>ys)"
30158
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 16554
diff changeset
    54
| "lzip\<cdot>lNil\<cdot>lNil = lNil"
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    55
31008
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    56
text {* @{text fixpat} is useful for producing strictness theorems. *}
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    57
text {* Note that pattern matching is done in left-to-right order. *}
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    58
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    59
fixpat lzip_stricts [simp]:
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    60
  "lzip\<cdot>\<bottom>\<cdot>ys"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    61
  "lzip\<cdot>lNil\<cdot>\<bottom>"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    62
  "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom>"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    63
31008
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    64
text {* @{text fixpat} can also produce rules for missing cases. *}
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    65
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    66
fixpat lzip_undefs [simp]:
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    67
  "lzip\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys)"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    68
  "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    69
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    70
31008
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    71
subsection {* Pattern matching with bottoms *}
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    72
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    73
text {*
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    74
  As an alternative to using @{text fixpat}, it is also possible to
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    75
  use bottom as a constructor pattern.  When using a bottom pattern,
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    76
  the right-hand-side must also be bottom; otherwise, @{text fixrec}
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    77
  will not be able to prove the equation.
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    78
*}
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    79
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    80
fixrec
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    81
  from_sinr_up :: "'a \<oplus> 'b\<^sub>\<bottom> \<rightarrow> 'b"
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    82
where
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    83
  "from_sinr_up\<cdot>\<bottom> = \<bottom>"
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    84
| "from_sinr_up\<cdot>(sinr\<cdot>(up\<cdot>x)) = x"
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    85
31008
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    86
text {*
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    87
  If the function is already strict in that argument, then the bottom
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    88
  pattern does not change the meaning of the function.  For example,
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    89
  in the definition of @{term from_sinr_up}, the first equation is
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    90
  actually redundant, and could have been proven separately by
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    91
  @{text fixpat}.
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    92
*}
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    93
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    94
text {*
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    95
  A bottom pattern can also be used to make a function strict in a
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    96
  certain argument, similar to a bang-pattern in Haskell.
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    97
*}
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    98
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    99
fixrec
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
   100
  seq :: "'a \<rightarrow> 'b \<rightarrow> 'b"
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
   101
where
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
   102
  "seq\<cdot>\<bottom>\<cdot>y = \<bottom>"
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
   103
| "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x\<cdot>y = y"
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
   104
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
   105
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
   106
subsection {* Skipping proofs of rewrite rules *}
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
   107
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
   108
text {* Another zip function for lazy lists. *}
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   109
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   110
text {*
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   111
  Notice that this version has overlapping patterns.
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   112
  The second equation cannot be proved as a theorem
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   113
  because it only applies when the first pattern fails.
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   114
*}
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   115
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   116
fixrec (permissive)
30158
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 16554
diff changeset
   117
  lzip2 :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 16554
diff changeset
   118
where
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   119
  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot><x,y>\<cdot>(lzip\<cdot>xs\<cdot>ys)"
30158
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 16554
diff changeset
   120
| "lzip2\<cdot>xs\<cdot>ys = lNil"
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   121
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   122
text {*
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   123
  Usually fixrec tries to prove all equations as theorems.
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   124
  The "permissive" option overrides this behavior, so fixrec
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   125
  does not produce any simp rules.
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   126
*}
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   127
31008
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
   128
text {* Simp rules can be generated later using @{text fixpat}. *}
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   129
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   130
fixpat lzip2_simps [simp]:
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   131
  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys)"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   132
  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   133
  "lzip2\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys)"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   134
  "lzip2\<cdot>lNil\<cdot>lNil"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   135
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   136
fixpat lzip2_stricts [simp]:
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   137
  "lzip2\<cdot>\<bottom>\<cdot>ys"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   138
  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom>"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   139
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   140
31008
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
   141
subsection {* Mutual recursion with @{text fixrec} *}
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
   142
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
   143
text {* Tree and forest types. *}
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   144
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   145
domain 'a tree = Leaf (lazy 'a) | Branch (lazy "'a forest")
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   146
and    'a forest = Empty | Trees (lazy "'a tree") "'a forest"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   147
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   148
text {*
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   149
  To define mutually recursive functions, separate the equations
31008
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
   150
  for each function using the keyword @{text "and"}.
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   151
*}
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   152
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   153
fixrec
30158
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 16554
diff changeset
   154
  map_tree :: "('a \<rightarrow> 'b) \<rightarrow> ('a tree \<rightarrow> 'b tree)"
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   155
and
30158
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 16554
diff changeset
   156
  map_forest :: "('a \<rightarrow> 'b) \<rightarrow> ('a forest \<rightarrow> 'b forest)"
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 16554
diff changeset
   157
where
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 16554
diff changeset
   158
  "map_tree\<cdot>f\<cdot>(Leaf\<cdot>x) = Leaf\<cdot>(f\<cdot>x)"
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 16554
diff changeset
   159
| "map_tree\<cdot>f\<cdot>(Branch\<cdot>ts) = Branch\<cdot>(map_forest\<cdot>f\<cdot>ts)"
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 16554
diff changeset
   160
| "map_forest\<cdot>f\<cdot>Empty = Empty"
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 16554
diff changeset
   161
| "ts \<noteq> \<bottom> \<Longrightarrow>
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   162
    map_forest\<cdot>f\<cdot>(Trees\<cdot>t\<cdot>ts) = Trees\<cdot>(map_tree\<cdot>f\<cdot>t)\<cdot>(map_forest\<cdot>f\<cdot>ts)"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   163
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   164
fixpat map_tree_strict [simp]: "map_tree\<cdot>f\<cdot>\<bottom>"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   165
fixpat map_forest_strict [simp]: "map_forest\<cdot>f\<cdot>\<bottom>"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   166
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   167
text {*
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   168
  Theorems generated:
31008
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
   169
  @{text map_tree_def}
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
   170
  @{text map_forest_def}
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
   171
  @{text map_tree_unfold}
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
   172
  @{text map_forest_unfold}
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
   173
  @{text map_tree_simps}
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
   174
  @{text map_forest_simps}
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
   175
  @{text map_tree_map_forest_induct}
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   176
*}
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   177
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   178
end