src/HOLCF/ex/Fixrec_ex.thy
author huffman
Wed, 19 May 2010 14:38:25 -0700
changeset 36997 ca3172dbde8b
parent 35925 3da8db225c93
permissions -rw-r--r--
add section about fixrec definitions with looping simp rules
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:
35925
3da8db225c93 use Pair instead of cpair in Fixrec_ex.thy
huffman
parents: 35770
diff changeset
    16
  Pair, spair, sinl, sinr, up, ONE, TT, FF.
16554
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
33428
70ed971a79d1 fixrec examples use fixrec_simp instead of fixpat
huffman
parents: 33401
diff changeset
    40
subsection {* Examples using @{text fixrec_simp} *}
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
35925
3da8db225c93 use Pair instead of cpair in Fixrec_ex.thy
huffman
parents: 35770
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
33428
70ed971a79d1 fixrec examples use fixrec_simp instead of fixpat
huffman
parents: 33401
diff changeset
    56
text {* @{text fixrec_simp} is useful for producing strictness theorems. *}
31008
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
33428
70ed971a79d1 fixrec examples use fixrec_simp instead of fixpat
huffman
parents: 33401
diff changeset
    59
lemma lzip_stricts [simp]:
70ed971a79d1 fixrec examples use fixrec_simp instead of fixpat
huffman
parents: 33401
diff changeset
    60
  "lzip\<cdot>\<bottom>\<cdot>ys = \<bottom>"
70ed971a79d1 fixrec examples use fixrec_simp instead of fixpat
huffman
parents: 33401
diff changeset
    61
  "lzip\<cdot>lNil\<cdot>\<bottom> = \<bottom>"
70ed971a79d1 fixrec examples use fixrec_simp instead of fixpat
huffman
parents: 33401
diff changeset
    62
  "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom> = \<bottom>"
70ed971a79d1 fixrec examples use fixrec_simp instead of fixpat
huffman
parents: 33401
diff changeset
    63
by fixrec_simp+
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    64
33428
70ed971a79d1 fixrec examples use fixrec_simp instead of fixpat
huffman
parents: 33401
diff changeset
    65
text {* @{text fixrec_simp} can also produce rules for missing cases. *}
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    66
33428
70ed971a79d1 fixrec examples use fixrec_simp instead of fixpat
huffman
parents: 33401
diff changeset
    67
lemma lzip_undefs [simp]:
70ed971a79d1 fixrec examples use fixrec_simp instead of fixpat
huffman
parents: 33401
diff changeset
    68
  "lzip\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys) = \<bottom>"
70ed971a79d1 fixrec examples use fixrec_simp instead of fixpat
huffman
parents: 33401
diff changeset
    69
  "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil = \<bottom>"
70ed971a79d1 fixrec examples use fixrec_simp instead of fixpat
huffman
parents: 33401
diff changeset
    70
by fixrec_simp+
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    71
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    72
31008
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    73
subsection {* Pattern matching with bottoms *}
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    74
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    75
text {*
33428
70ed971a79d1 fixrec examples use fixrec_simp instead of fixpat
huffman
parents: 33401
diff changeset
    76
  As an alternative to using @{text fixrec_simp}, it is also possible
70ed971a79d1 fixrec examples use fixrec_simp instead of fixpat
huffman
parents: 33401
diff changeset
    77
  to use bottom as a constructor pattern.  When using a bottom
70ed971a79d1 fixrec examples use fixrec_simp instead of fixpat
huffman
parents: 33401
diff changeset
    78
  pattern, the right-hand-side must also be bottom; otherwise, @{text
70ed971a79d1 fixrec examples use fixrec_simp instead of fixpat
huffman
parents: 33401
diff changeset
    79
  fixrec} will not be able to prove the equation.
31008
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    80
*}
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    81
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    82
fixrec
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    83
  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
    84
where
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    85
  "from_sinr_up\<cdot>\<bottom> = \<bottom>"
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    86
| "from_sinr_up\<cdot>(sinr\<cdot>(up\<cdot>x)) = x"
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    87
31008
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    88
text {*
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    89
  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
    90
  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
    91
  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
    92
  actually redundant, and could have been proven separately by
33428
70ed971a79d1 fixrec examples use fixrec_simp instead of fixpat
huffman
parents: 33401
diff changeset
    93
  @{text fixrec_simp}.
31008
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    94
*}
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    95
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    96
text {*
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    97
  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
    98
  certain argument, similar to a bang-pattern in Haskell.
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
    99
*}
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
   100
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
   101
fixrec
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
   102
  seq :: "'a \<rightarrow> 'b \<rightarrow> 'b"
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
   103
where
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
   104
  "seq\<cdot>\<bottom>\<cdot>y = \<bottom>"
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
   105
| "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
   106
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
subsection {* Skipping proofs of rewrite rules *}
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
   109
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
   110
text {* Another zip function for lazy lists. *}
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   111
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   112
text {*
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   113
  Notice that this version has overlapping patterns.
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   114
  The second equation cannot be proved as a theorem
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   115
  because it only applies when the first pattern fails.
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   116
*}
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   117
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   118
fixrec (permissive)
30158
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 16554
diff changeset
   119
  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
   120
where
35925
3da8db225c93 use Pair instead of cpair in Fixrec_ex.thy
huffman
parents: 35770
diff changeset
   121
  "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
   122
| "lzip2\<cdot>xs\<cdot>ys = lNil"
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   123
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   124
text {*
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   125
  Usually fixrec tries to prove all equations as theorems.
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   126
  The "permissive" option overrides this behavior, so fixrec
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   127
  does not produce any simp rules.
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   128
*}
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   129
33428
70ed971a79d1 fixrec examples use fixrec_simp instead of fixpat
huffman
parents: 33401
diff changeset
   130
text {* Simp rules can be generated later using @{text fixrec_simp}. *}
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   131
33428
70ed971a79d1 fixrec examples use fixrec_simp instead of fixpat
huffman
parents: 33401
diff changeset
   132
lemma lzip2_simps [simp]:
35925
3da8db225c93 use Pair instead of cpair in Fixrec_ex.thy
huffman
parents: 35770
diff changeset
   133
  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip\<cdot>xs\<cdot>ys)"
33428
70ed971a79d1 fixrec examples use fixrec_simp instead of fixpat
huffman
parents: 33401
diff changeset
   134
  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil = lNil"
70ed971a79d1 fixrec examples use fixrec_simp instead of fixpat
huffman
parents: 33401
diff changeset
   135
  "lzip2\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys) = lNil"
70ed971a79d1 fixrec examples use fixrec_simp instead of fixpat
huffman
parents: 33401
diff changeset
   136
  "lzip2\<cdot>lNil\<cdot>lNil = lNil"
70ed971a79d1 fixrec examples use fixrec_simp instead of fixpat
huffman
parents: 33401
diff changeset
   137
by fixrec_simp+
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   138
33428
70ed971a79d1 fixrec examples use fixrec_simp instead of fixpat
huffman
parents: 33401
diff changeset
   139
lemma lzip2_stricts [simp]:
70ed971a79d1 fixrec examples use fixrec_simp instead of fixpat
huffman
parents: 33401
diff changeset
   140
  "lzip2\<cdot>\<bottom>\<cdot>ys = \<bottom>"
70ed971a79d1 fixrec examples use fixrec_simp instead of fixpat
huffman
parents: 33401
diff changeset
   141
  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom> = \<bottom>"
70ed971a79d1 fixrec examples use fixrec_simp instead of fixpat
huffman
parents: 33401
diff changeset
   142
by fixrec_simp+
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   143
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   144
31008
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
   145
subsection {* Mutual recursion with @{text fixrec} *}
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
   146
b8f4e351b5bf add proper support for bottom-patterns in fixrec package
huffman
parents: 30158
diff changeset
   147
text {* Tree and forest types. *}
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   148
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   149
domain 'a tree = Leaf (lazy 'a) | Branch (lazy "'a forest")
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   150
and    'a forest = Empty | Trees (lazy "'a tree") "'a forest"
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
text {*
35770
a57ab2c01369 fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents: 33428
diff changeset
   153
  To define mutually recursive functions, give multiple type signatures
a57ab2c01369 fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents: 33428
diff changeset
   154
  separated by the keyword @{text "and"}.
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   155
*}
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   156
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   157
fixrec
30158
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 16554
diff changeset
   158
  map_tree :: "('a \<rightarrow> 'b) \<rightarrow> ('a tree \<rightarrow> 'b tree)"
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   159
and
30158
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 16554
diff changeset
   160
  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
   161
where
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 16554
diff changeset
   162
  "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
   163
| "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
   164
| "map_forest\<cdot>f\<cdot>Empty = Empty"
83c50c62cf23 fixrec package uses new-style syntax and local-theory interface
huffman
parents: 16554
diff changeset
   165
| "ts \<noteq> \<bottom> \<Longrightarrow>
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   166
    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
   167
33428
70ed971a79d1 fixrec examples use fixrec_simp instead of fixpat
huffman
parents: 33401
diff changeset
   168
lemma map_tree_strict [simp]: "map_tree\<cdot>f\<cdot>\<bottom> = \<bottom>"
70ed971a79d1 fixrec examples use fixrec_simp instead of fixpat
huffman
parents: 33401
diff changeset
   169
by fixrec_simp
70ed971a79d1 fixrec examples use fixrec_simp instead of fixpat
huffman
parents: 33401
diff changeset
   170
70ed971a79d1 fixrec examples use fixrec_simp instead of fixpat
huffman
parents: 33401
diff changeset
   171
lemma map_forest_strict [simp]: "map_forest\<cdot>f\<cdot>\<bottom> = \<bottom>"
70ed971a79d1 fixrec examples use fixrec_simp instead of fixpat
huffman
parents: 33401
diff changeset
   172
by fixrec_simp
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   173
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   174
text {*
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   175
  Theorems generated:
35770
a57ab2c01369 fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents: 33428
diff changeset
   176
  @{text map_tree_def}  @{thm map_tree_def}
a57ab2c01369 fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents: 33428
diff changeset
   177
  @{text map_forest_def}  @{thm map_forest_def}
a57ab2c01369 fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents: 33428
diff changeset
   178
  @{text map_tree.unfold}  @{thm map_tree.unfold}
a57ab2c01369 fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents: 33428
diff changeset
   179
  @{text map_forest.unfold}  @{thm map_forest.unfold}
a57ab2c01369 fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents: 33428
diff changeset
   180
  @{text map_tree.simps}  @{thm map_tree.simps}
a57ab2c01369 fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents: 33428
diff changeset
   181
  @{text map_forest.simps}  @{thm map_forest.simps}
a57ab2c01369 fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents: 33428
diff changeset
   182
  @{text map_tree_map_forest.induct}  @{thm map_tree_map_forest.induct}
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   183
*}
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   184
35770
a57ab2c01369 fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents: 33428
diff changeset
   185
36997
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   186
subsection {* Looping simp rules *}
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   187
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   188
text {*
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   189
  The defining equations of a fixrec definition are declared as simp
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   190
  rules by default.  In some cases, especially for constants with no
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   191
  arguments or functions with variable patterns, the defining
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   192
  equations may cause the simplifier to loop.  In these cases it will
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   193
  be necessary to use a @{text "[simp del]"} declaration.
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   194
*}
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   195
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   196
fixrec
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   197
  repeat :: "'a \<rightarrow> 'a llist"
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   198
where
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   199
  [simp del]: "repeat\<cdot>x = lCons\<cdot>x\<cdot>(repeat\<cdot>x)"
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   200
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   201
text {*
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   202
  We can derive other non-looping simp rules for @{const repeat} by
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   203
  using the @{text subst} method with the @{text repeat.simps} rule.
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   204
*}
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   205
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   206
lemma repeat_simps [simp]:
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   207
  "repeat\<cdot>x \<noteq> \<bottom>"
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   208
  "repeat\<cdot>x \<noteq> lNil"
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   209
  "repeat\<cdot>x = lCons\<cdot>y\<cdot>ys \<longleftrightarrow> x = y \<and> repeat\<cdot>x = ys"
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   210
by (subst repeat.simps, simp)+
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   211
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   212
lemma llist_when_repeat [simp]:
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   213
  "llist_when\<cdot>z\<cdot>f\<cdot>(repeat\<cdot>x) = f\<cdot>x\<cdot>(repeat\<cdot>x)"
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   214
by (subst repeat.simps, simp)
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   215
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   216
text {*
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   217
  For mutually-recursive constants, looping might only occur if all
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   218
  equations are in the simpset at the same time.  In such cases it may
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   219
  only be necessary to declare @{text "[simp del]"} on one equation.
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   220
*}
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   221
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   222
fixrec
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   223
  inf_tree :: "'a tree" and inf_forest :: "'a forest"
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   224
where
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   225
  [simp del]: "inf_tree = Branch\<cdot>inf_forest"
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   226
| "inf_forest = Trees\<cdot>inf_tree\<cdot>(Trees\<cdot>inf_tree\<cdot>Empty)"
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   227
ca3172dbde8b add section about fixrec definitions with looping simp rules
huffman
parents: 35925
diff changeset
   228
35770
a57ab2c01369 fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents: 33428
diff changeset
   229
subsection {* Using @{text fixrec} inside locales *}
a57ab2c01369 fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents: 33428
diff changeset
   230
a57ab2c01369 fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents: 33428
diff changeset
   231
locale test =
a57ab2c01369 fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents: 33428
diff changeset
   232
  fixes foo :: "'a \<rightarrow> 'a"
a57ab2c01369 fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents: 33428
diff changeset
   233
  assumes foo_strict: "foo\<cdot>\<bottom> = \<bottom>"
a57ab2c01369 fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents: 33428
diff changeset
   234
begin
a57ab2c01369 fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents: 33428
diff changeset
   235
a57ab2c01369 fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents: 33428
diff changeset
   236
fixrec
a57ab2c01369 fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents: 33428
diff changeset
   237
  bar :: "'a u \<rightarrow> 'a"
a57ab2c01369 fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents: 33428
diff changeset
   238
where
a57ab2c01369 fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents: 33428
diff changeset
   239
  "bar\<cdot>(up\<cdot>x) = foo\<cdot>x"
a57ab2c01369 fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents: 33428
diff changeset
   240
a57ab2c01369 fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents: 33428
diff changeset
   241
lemma bar_strict: "bar\<cdot>\<bottom> = \<bottom>"
a57ab2c01369 fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents: 33428
diff changeset
   242
by fixrec_simp
a57ab2c01369 fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents: 33428
diff changeset
   243
16554
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   244
end
35770
a57ab2c01369 fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents: 33428
diff changeset
   245
a57ab2c01369 fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents: 33428
diff changeset
   246
end