src/HOL/HOLCF/Tutorial/Fixrec_ex.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 42151 4da4fc77664b
child 58880 0baae4311a9f
permissions -rw-r--r--
Quotient_Info stores only relation maps
wenzelm@42151
     1
(*  Title:      HOL/HOLCF/Tutorial/Fixrec_ex.thy
huffman@16554
     2
    Author:     Brian Huffman
huffman@16554
     3
*)
huffman@16554
     4
huffman@16554
     5
header {* Fixrec package examples *}
huffman@16554
     6
huffman@16554
     7
theory Fixrec_ex
huffman@16554
     8
imports HOLCF
huffman@16554
     9
begin
huffman@16554
    10
huffman@31008
    11
subsection {* Basic @{text fixrec} examples *}
huffman@16554
    12
huffman@16554
    13
text {*
huffman@16554
    14
  Fixrec patterns can mention any constructor defined by the domain
huffman@16554
    15
  package, as well as any of the following built-in constructors:
huffman@35925
    16
  Pair, spair, sinl, sinr, up, ONE, TT, FF.
huffman@16554
    17
*}
huffman@16554
    18
huffman@31008
    19
text {* Typical usage is with lazy constructors. *}
huffman@16554
    20
huffman@30158
    21
fixrec down :: "'a u \<rightarrow> 'a"
huffman@30158
    22
where "down\<cdot>(up\<cdot>x) = x"
huffman@16554
    23
huffman@31008
    24
text {* With strict constructors, rewrite rules may require side conditions. *}
huffman@16554
    25
huffman@30158
    26
fixrec from_sinl :: "'a \<oplus> 'b \<rightarrow> 'a"
huffman@30158
    27
where "x \<noteq> \<bottom> \<Longrightarrow> from_sinl\<cdot>(sinl\<cdot>x) = x"
huffman@16554
    28
huffman@31008
    29
text {* Lifting can turn a strict constructor into a lazy one. *}
huffman@16554
    30
huffman@30158
    31
fixrec from_sinl_up :: "'a u \<oplus> 'b \<rightarrow> 'a"
huffman@30158
    32
where "from_sinl_up\<cdot>(sinl\<cdot>(up\<cdot>x)) = x"
huffman@16554
    33
huffman@33401
    34
text {* Fixrec also works with the HOL pair constructor. *}
huffman@33401
    35
huffman@33401
    36
fixrec down2 :: "'a u \<times> 'b u \<rightarrow> 'a \<times> 'b"
huffman@33401
    37
where "down2\<cdot>(up\<cdot>x, up\<cdot>y) = (x, y)"
huffman@33401
    38
huffman@16554
    39
huffman@33428
    40
subsection {* Examples using @{text fixrec_simp} *}
huffman@16554
    41
huffman@31008
    42
text {* A type of lazy lists. *}
huffman@16554
    43
huffman@16554
    44
domain 'a llist = lNil | lCons (lazy 'a) (lazy "'a llist")
huffman@16554
    45
huffman@31008
    46
text {* A zip function for lazy lists. *}
huffman@16554
    47
huffman@31008
    48
text {* Notice that the patterns are not exhaustive. *}
huffman@16554
    49
huffman@16554
    50
fixrec
huffman@30158
    51
  lzip :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
huffman@30158
    52
where
huffman@35925
    53
  "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip\<cdot>xs\<cdot>ys)"
huffman@30158
    54
| "lzip\<cdot>lNil\<cdot>lNil = lNil"
huffman@16554
    55
huffman@33428
    56
text {* @{text fixrec_simp} is useful for producing strictness theorems. *}
huffman@31008
    57
text {* Note that pattern matching is done in left-to-right order. *}
huffman@16554
    58
huffman@33428
    59
lemma lzip_stricts [simp]:
huffman@33428
    60
  "lzip\<cdot>\<bottom>\<cdot>ys = \<bottom>"
huffman@33428
    61
  "lzip\<cdot>lNil\<cdot>\<bottom> = \<bottom>"
huffman@33428
    62
  "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom> = \<bottom>"
huffman@33428
    63
by fixrec_simp+
huffman@16554
    64
huffman@33428
    65
text {* @{text fixrec_simp} can also produce rules for missing cases. *}
huffman@16554
    66
huffman@33428
    67
lemma lzip_undefs [simp]:
huffman@33428
    68
  "lzip\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys) = \<bottom>"
huffman@33428
    69
  "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil = \<bottom>"
huffman@33428
    70
by fixrec_simp+
huffman@16554
    71
huffman@16554
    72
huffman@31008
    73
subsection {* Pattern matching with bottoms *}
huffman@31008
    74
huffman@31008
    75
text {*
huffman@33428
    76
  As an alternative to using @{text fixrec_simp}, it is also possible
huffman@33428
    77
  to use bottom as a constructor pattern.  When using a bottom
huffman@33428
    78
  pattern, the right-hand-side must also be bottom; otherwise, @{text
huffman@33428
    79
  fixrec} will not be able to prove the equation.
huffman@31008
    80
*}
huffman@31008
    81
huffman@31008
    82
fixrec
huffman@31008
    83
  from_sinr_up :: "'a \<oplus> 'b\<^sub>\<bottom> \<rightarrow> 'b"
huffman@31008
    84
where
huffman@31008
    85
  "from_sinr_up\<cdot>\<bottom> = \<bottom>"
huffman@31008
    86
| "from_sinr_up\<cdot>(sinr\<cdot>(up\<cdot>x)) = x"
huffman@16554
    87
huffman@31008
    88
text {*
huffman@31008
    89
  If the function is already strict in that argument, then the bottom
huffman@31008
    90
  pattern does not change the meaning of the function.  For example,
huffman@31008
    91
  in the definition of @{term from_sinr_up}, the first equation is
huffman@31008
    92
  actually redundant, and could have been proven separately by
huffman@33428
    93
  @{text fixrec_simp}.
huffman@31008
    94
*}
huffman@31008
    95
huffman@31008
    96
text {*
huffman@31008
    97
  A bottom pattern can also be used to make a function strict in a
huffman@31008
    98
  certain argument, similar to a bang-pattern in Haskell.
huffman@31008
    99
*}
huffman@31008
   100
huffman@31008
   101
fixrec
huffman@31008
   102
  seq :: "'a \<rightarrow> 'b \<rightarrow> 'b"
huffman@31008
   103
where
huffman@31008
   104
  "seq\<cdot>\<bottom>\<cdot>y = \<bottom>"
huffman@31008
   105
| "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x\<cdot>y = y"
huffman@31008
   106
huffman@31008
   107
huffman@31008
   108
subsection {* Skipping proofs of rewrite rules *}
huffman@31008
   109
huffman@31008
   110
text {* Another zip function for lazy lists. *}
huffman@16554
   111
huffman@16554
   112
text {*
huffman@16554
   113
  Notice that this version has overlapping patterns.
huffman@16554
   114
  The second equation cannot be proved as a theorem
huffman@16554
   115
  because it only applies when the first pattern fails.
huffman@16554
   116
*}
huffman@16554
   117
huffman@40041
   118
fixrec
huffman@30158
   119
  lzip2 :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
huffman@30158
   120
where
huffman@40041
   121
  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip2\<cdot>xs\<cdot>ys)"
huffman@40041
   122
| (unchecked) "lzip2\<cdot>xs\<cdot>ys = lNil"
huffman@16554
   123
huffman@16554
   124
text {*
huffman@16554
   125
  Usually fixrec tries to prove all equations as theorems.
huffman@40041
   126
  The "unchecked" option overrides this behavior, so fixrec
huffman@40041
   127
  does not attempt to prove that particular equation.
huffman@16554
   128
*}
huffman@16554
   129
huffman@33428
   130
text {* Simp rules can be generated later using @{text fixrec_simp}. *}
huffman@16554
   131
huffman@33428
   132
lemma lzip2_simps [simp]:
huffman@33428
   133
  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil = lNil"
huffman@33428
   134
  "lzip2\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys) = lNil"
huffman@33428
   135
  "lzip2\<cdot>lNil\<cdot>lNil = lNil"
huffman@33428
   136
by fixrec_simp+
huffman@16554
   137
huffman@33428
   138
lemma lzip2_stricts [simp]:
huffman@33428
   139
  "lzip2\<cdot>\<bottom>\<cdot>ys = \<bottom>"
huffman@33428
   140
  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom> = \<bottom>"
huffman@33428
   141
by fixrec_simp+
huffman@16554
   142
huffman@16554
   143
huffman@31008
   144
subsection {* Mutual recursion with @{text fixrec} *}
huffman@31008
   145
huffman@31008
   146
text {* Tree and forest types. *}
huffman@16554
   147
huffman@16554
   148
domain 'a tree = Leaf (lazy 'a) | Branch (lazy "'a forest")
huffman@16554
   149
and    'a forest = Empty | Trees (lazy "'a tree") "'a forest"
huffman@16554
   150
huffman@16554
   151
text {*
huffman@35770
   152
  To define mutually recursive functions, give multiple type signatures
huffman@35770
   153
  separated by the keyword @{text "and"}.
huffman@16554
   154
*}
huffman@16554
   155
huffman@16554
   156
fixrec
huffman@30158
   157
  map_tree :: "('a \<rightarrow> 'b) \<rightarrow> ('a tree \<rightarrow> 'b tree)"
huffman@16554
   158
and
huffman@30158
   159
  map_forest :: "('a \<rightarrow> 'b) \<rightarrow> ('a forest \<rightarrow> 'b forest)"
huffman@30158
   160
where
huffman@30158
   161
  "map_tree\<cdot>f\<cdot>(Leaf\<cdot>x) = Leaf\<cdot>(f\<cdot>x)"
huffman@30158
   162
| "map_tree\<cdot>f\<cdot>(Branch\<cdot>ts) = Branch\<cdot>(map_forest\<cdot>f\<cdot>ts)"
huffman@30158
   163
| "map_forest\<cdot>f\<cdot>Empty = Empty"
huffman@30158
   164
| "ts \<noteq> \<bottom> \<Longrightarrow>
huffman@16554
   165
    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)"
huffman@16554
   166
huffman@33428
   167
lemma map_tree_strict [simp]: "map_tree\<cdot>f\<cdot>\<bottom> = \<bottom>"
huffman@33428
   168
by fixrec_simp
huffman@33428
   169
huffman@33428
   170
lemma map_forest_strict [simp]: "map_forest\<cdot>f\<cdot>\<bottom> = \<bottom>"
huffman@33428
   171
by fixrec_simp
huffman@16554
   172
huffman@37000
   173
(*
huffman@16554
   174
  Theorems generated:
huffman@35770
   175
  @{text map_tree_def}  @{thm map_tree_def}
huffman@35770
   176
  @{text map_forest_def}  @{thm map_forest_def}
huffman@35770
   177
  @{text map_tree.unfold}  @{thm map_tree.unfold}
huffman@35770
   178
  @{text map_forest.unfold}  @{thm map_forest.unfold}
huffman@35770
   179
  @{text map_tree.simps}  @{thm map_tree.simps}
huffman@35770
   180
  @{text map_forest.simps}  @{thm map_forest.simps}
huffman@35770
   181
  @{text map_tree_map_forest.induct}  @{thm map_tree_map_forest.induct}
huffman@37000
   182
*)
huffman@16554
   183
huffman@35770
   184
huffman@36997
   185
subsection {* Looping simp rules *}
huffman@36997
   186
huffman@36997
   187
text {*
huffman@36997
   188
  The defining equations of a fixrec definition are declared as simp
huffman@36997
   189
  rules by default.  In some cases, especially for constants with no
huffman@36997
   190
  arguments or functions with variable patterns, the defining
huffman@36997
   191
  equations may cause the simplifier to loop.  In these cases it will
huffman@36997
   192
  be necessary to use a @{text "[simp del]"} declaration.
huffman@36997
   193
*}
huffman@36997
   194
huffman@36997
   195
fixrec
huffman@36997
   196
  repeat :: "'a \<rightarrow> 'a llist"
huffman@36997
   197
where
huffman@36997
   198
  [simp del]: "repeat\<cdot>x = lCons\<cdot>x\<cdot>(repeat\<cdot>x)"
huffman@36997
   199
huffman@36997
   200
text {*
huffman@36997
   201
  We can derive other non-looping simp rules for @{const repeat} by
huffman@36997
   202
  using the @{text subst} method with the @{text repeat.simps} rule.
huffman@36997
   203
*}
huffman@36997
   204
huffman@36997
   205
lemma repeat_simps [simp]:
huffman@36997
   206
  "repeat\<cdot>x \<noteq> \<bottom>"
huffman@36997
   207
  "repeat\<cdot>x \<noteq> lNil"
huffman@36997
   208
  "repeat\<cdot>x = lCons\<cdot>y\<cdot>ys \<longleftrightarrow> x = y \<and> repeat\<cdot>x = ys"
huffman@36997
   209
by (subst repeat.simps, simp)+
huffman@36997
   210
huffman@40213
   211
lemma llist_case_repeat [simp]:
huffman@40213
   212
  "llist_case\<cdot>z\<cdot>f\<cdot>(repeat\<cdot>x) = f\<cdot>x\<cdot>(repeat\<cdot>x)"
huffman@36997
   213
by (subst repeat.simps, simp)
huffman@36997
   214
huffman@36997
   215
text {*
huffman@36997
   216
  For mutually-recursive constants, looping might only occur if all
huffman@36997
   217
  equations are in the simpset at the same time.  In such cases it may
huffman@36997
   218
  only be necessary to declare @{text "[simp del]"} on one equation.
huffman@36997
   219
*}
huffman@36997
   220
huffman@36997
   221
fixrec
huffman@36997
   222
  inf_tree :: "'a tree" and inf_forest :: "'a forest"
huffman@36997
   223
where
huffman@36997
   224
  [simp del]: "inf_tree = Branch\<cdot>inf_forest"
huffman@36997
   225
| "inf_forest = Trees\<cdot>inf_tree\<cdot>(Trees\<cdot>inf_tree\<cdot>Empty)"
huffman@36997
   226
huffman@36997
   227
huffman@35770
   228
subsection {* Using @{text fixrec} inside locales *}
huffman@35770
   229
huffman@35770
   230
locale test =
huffman@35770
   231
  fixes foo :: "'a \<rightarrow> 'a"
huffman@35770
   232
  assumes foo_strict: "foo\<cdot>\<bottom> = \<bottom>"
huffman@35770
   233
begin
huffman@35770
   234
huffman@35770
   235
fixrec
huffman@35770
   236
  bar :: "'a u \<rightarrow> 'a"
huffman@35770
   237
where
huffman@35770
   238
  "bar\<cdot>(up\<cdot>x) = foo\<cdot>x"
huffman@35770
   239
huffman@35770
   240
lemma bar_strict: "bar\<cdot>\<bottom> = \<bottom>"
huffman@35770
   241
by fixrec_simp
huffman@35770
   242
huffman@16554
   243
end
huffman@35770
   244
huffman@35770
   245
end