src/HOLCF/ex/Fixrec_ex.thy
author huffman
Mon Nov 02 18:39:41 2009 -0800 (2009-11-02)
changeset 33401 fc43fa403a69
parent 31008 b8f4e351b5bf
child 33428 70ed971a79d1
permissions -rw-r--r--
add fixrec support for HOL pair constructor patterns
huffman@16554
     1
(*  Title:      HOLCF/ex/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@16554
    16
  cpair, 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@31008
    40
subsection {* Examples using @{text fixpat} *}
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@16554
    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@31008
    56
text {* @{text fixpat} 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@16554
    59
fixpat lzip_stricts [simp]:
huffman@16554
    60
  "lzip\<cdot>\<bottom>\<cdot>ys"
huffman@16554
    61
  "lzip\<cdot>lNil\<cdot>\<bottom>"
huffman@16554
    62
  "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom>"
huffman@16554
    63
huffman@31008
    64
text {* @{text fixpat} can also produce rules for missing cases. *}
huffman@16554
    65
huffman@16554
    66
fixpat lzip_undefs [simp]:
huffman@16554
    67
  "lzip\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys)"
huffman@16554
    68
  "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil"
huffman@16554
    69
huffman@16554
    70
huffman@31008
    71
subsection {* Pattern matching with bottoms *}
huffman@31008
    72
huffman@31008
    73
text {*
huffman@31008
    74
  As an alternative to using @{text fixpat}, it is also possible to
huffman@31008
    75
  use bottom as a constructor pattern.  When using a bottom pattern,
huffman@31008
    76
  the right-hand-side must also be bottom; otherwise, @{text fixrec}
huffman@31008
    77
  will not be able to prove the equation.
huffman@31008
    78
*}
huffman@31008
    79
huffman@31008
    80
fixrec
huffman@31008
    81
  from_sinr_up :: "'a \<oplus> 'b\<^sub>\<bottom> \<rightarrow> 'b"
huffman@31008
    82
where
huffman@31008
    83
  "from_sinr_up\<cdot>\<bottom> = \<bottom>"
huffman@31008
    84
| "from_sinr_up\<cdot>(sinr\<cdot>(up\<cdot>x)) = x"
huffman@16554
    85
huffman@31008
    86
text {*
huffman@31008
    87
  If the function is already strict in that argument, then the bottom
huffman@31008
    88
  pattern does not change the meaning of the function.  For example,
huffman@31008
    89
  in the definition of @{term from_sinr_up}, the first equation is
huffman@31008
    90
  actually redundant, and could have been proven separately by
huffman@31008
    91
  @{text fixpat}.
huffman@31008
    92
*}
huffman@31008
    93
huffman@31008
    94
text {*
huffman@31008
    95
  A bottom pattern can also be used to make a function strict in a
huffman@31008
    96
  certain argument, similar to a bang-pattern in Haskell.
huffman@31008
    97
*}
huffman@31008
    98
huffman@31008
    99
fixrec
huffman@31008
   100
  seq :: "'a \<rightarrow> 'b \<rightarrow> 'b"
huffman@31008
   101
where
huffman@31008
   102
  "seq\<cdot>\<bottom>\<cdot>y = \<bottom>"
huffman@31008
   103
| "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x\<cdot>y = y"
huffman@31008
   104
huffman@31008
   105
huffman@31008
   106
subsection {* Skipping proofs of rewrite rules *}
huffman@31008
   107
huffman@31008
   108
text {* Another zip function for lazy lists. *}
huffman@16554
   109
huffman@16554
   110
text {*
huffman@16554
   111
  Notice that this version has overlapping patterns.
huffman@16554
   112
  The second equation cannot be proved as a theorem
huffman@16554
   113
  because it only applies when the first pattern fails.
huffman@16554
   114
*}
huffman@16554
   115
huffman@16554
   116
fixrec (permissive)
huffman@30158
   117
  lzip2 :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
huffman@30158
   118
where
huffman@16554
   119
  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot><x,y>\<cdot>(lzip\<cdot>xs\<cdot>ys)"
huffman@30158
   120
| "lzip2\<cdot>xs\<cdot>ys = lNil"
huffman@16554
   121
huffman@16554
   122
text {*
huffman@16554
   123
  Usually fixrec tries to prove all equations as theorems.
huffman@16554
   124
  The "permissive" option overrides this behavior, so fixrec
huffman@16554
   125
  does not produce any simp rules.
huffman@16554
   126
*}
huffman@16554
   127
huffman@31008
   128
text {* Simp rules can be generated later using @{text fixpat}. *}
huffman@16554
   129
huffman@16554
   130
fixpat lzip2_simps [simp]:
huffman@16554
   131
  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys)"
huffman@16554
   132
  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil"
huffman@16554
   133
  "lzip2\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys)"
huffman@16554
   134
  "lzip2\<cdot>lNil\<cdot>lNil"
huffman@16554
   135
huffman@16554
   136
fixpat lzip2_stricts [simp]:
huffman@16554
   137
  "lzip2\<cdot>\<bottom>\<cdot>ys"
huffman@16554
   138
  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom>"
huffman@16554
   139
huffman@16554
   140
huffman@31008
   141
subsection {* Mutual recursion with @{text fixrec} *}
huffman@31008
   142
huffman@31008
   143
text {* Tree and forest types. *}
huffman@16554
   144
huffman@16554
   145
domain 'a tree = Leaf (lazy 'a) | Branch (lazy "'a forest")
huffman@16554
   146
and    'a forest = Empty | Trees (lazy "'a tree") "'a forest"
huffman@16554
   147
huffman@16554
   148
text {*
huffman@16554
   149
  To define mutually recursive functions, separate the equations
huffman@31008
   150
  for each function using the keyword @{text "and"}.
huffman@16554
   151
*}
huffman@16554
   152
huffman@16554
   153
fixrec
huffman@30158
   154
  map_tree :: "('a \<rightarrow> 'b) \<rightarrow> ('a tree \<rightarrow> 'b tree)"
huffman@16554
   155
and
huffman@30158
   156
  map_forest :: "('a \<rightarrow> 'b) \<rightarrow> ('a forest \<rightarrow> 'b forest)"
huffman@30158
   157
where
huffman@30158
   158
  "map_tree\<cdot>f\<cdot>(Leaf\<cdot>x) = Leaf\<cdot>(f\<cdot>x)"
huffman@30158
   159
| "map_tree\<cdot>f\<cdot>(Branch\<cdot>ts) = Branch\<cdot>(map_forest\<cdot>f\<cdot>ts)"
huffman@30158
   160
| "map_forest\<cdot>f\<cdot>Empty = Empty"
huffman@30158
   161
| "ts \<noteq> \<bottom> \<Longrightarrow>
huffman@16554
   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)"
huffman@16554
   163
huffman@16554
   164
fixpat map_tree_strict [simp]: "map_tree\<cdot>f\<cdot>\<bottom>"
huffman@16554
   165
fixpat map_forest_strict [simp]: "map_forest\<cdot>f\<cdot>\<bottom>"
huffman@16554
   166
huffman@16554
   167
text {*
huffman@16554
   168
  Theorems generated:
huffman@31008
   169
  @{text map_tree_def}
huffman@31008
   170
  @{text map_forest_def}
huffman@31008
   171
  @{text map_tree_unfold}
huffman@31008
   172
  @{text map_forest_unfold}
huffman@31008
   173
  @{text map_tree_simps}
huffman@31008
   174
  @{text map_forest_simps}
huffman@31008
   175
  @{text map_tree_map_forest_induct}
huffman@16554
   176
*}
huffman@16554
   177
huffman@16554
   178
end