src/HOLCF/ex/Fixrec_ex.thy
author huffman
Thu, 23 Jun 2005 22:08:24 +0200
changeset 16554 5841e7f9eef5
child 30158 83c50c62cf23
permissions -rw-r--r--
add new file to test fixrec package
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
    ID:         $Id$
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
     3
    Author:     Brian Huffman
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
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
     6
header {* Fixrec package examples *}
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
     7
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
     8
theory Fixrec_ex
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
     9
imports HOLCF
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    10
begin
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    11
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    12
subsection {* basic fixrec examples *}
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    13
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    14
text {*
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    15
  Fixrec patterns can mention any constructor defined by the domain
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    16
  package, as well as any of the following built-in constructors:
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    17
  cpair, spair, sinl, sinr, up, ONE, TT, FF.
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    18
*}
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    19
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    20
text {* typical usage is with lazy constructors *}
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    21
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    22
consts down :: "'a u \<rightarrow> 'a"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    23
fixrec "down\<cdot>(up\<cdot>x) = x"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    24
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    25
text {* with strict constructors, rewrite rules may require side conditions *}
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    26
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    27
consts from_sinl :: "'a \<oplus> 'b \<rightarrow> 'a"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    28
fixrec "x \<noteq> \<bottom> \<Longrightarrow> from_sinl\<cdot>(sinl\<cdot>x) = x"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    29
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    30
text {* lifting can turn a strict constructor into a lazy one *}
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    31
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    32
consts from_sinl_up :: "'a u \<oplus> 'b \<rightarrow> 'a"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    33
fixrec "from_sinl_up\<cdot>(sinl\<cdot>(up\<cdot>x)) = x"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    34
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    35
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    36
subsection {* fixpat examples *}
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    37
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    38
text {* a type of lazy lists *}
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    39
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    40
domain 'a llist = lNil | lCons (lazy 'a) (lazy "'a llist")
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    41
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    42
text {* zip function for lazy lists *}
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
consts lzip :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    45
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    46
text {* notice that the patterns are not exhaustive *}
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    47
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    48
fixrec
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    49
  "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot><x,y>\<cdot>(lzip\<cdot>xs\<cdot>ys)"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    50
  "lzip\<cdot>lNil\<cdot>lNil = lNil"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    51
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    52
text {* fixpat is useful for producing strictness theorems *}
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    53
text {* note that pattern matching is done in left-to-right order *}
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    54
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    55
fixpat lzip_stricts [simp]:
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    56
  "lzip\<cdot>\<bottom>\<cdot>ys"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    57
  "lzip\<cdot>lNil\<cdot>\<bottom>"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    58
  "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom>"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    59
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    60
text {* fixpat can also produce rules for missing cases *}
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    61
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    62
fixpat lzip_undefs [simp]:
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    63
  "lzip\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys)"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    64
  "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil"
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
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    67
subsection {* skipping proofs of rewrite rules *}
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    68
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    69
text {* another zip function for lazy lists *}
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    70
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    71
consts lzip2 :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    72
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    73
text {*
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    74
  Notice that this version has overlapping patterns.
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    75
  The second equation cannot be proved as a theorem
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    76
  because it only applies when the first pattern fails.
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    77
*}
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    78
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    79
fixrec (permissive)
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    80
  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot><x,y>\<cdot>(lzip\<cdot>xs\<cdot>ys)"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    81
  "lzip2\<cdot>xs\<cdot>ys = lNil"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    82
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    83
text {*
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    84
  Usually fixrec tries to prove all equations as theorems.
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    85
  The "permissive" option overrides this behavior, so fixrec
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    86
  does not produce any simp rules.
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    87
*}
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    88
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    89
text {* simp rules can be generated later using fixpat *}
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    90
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    91
fixpat lzip2_simps [simp]:
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    92
  "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
    93
  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    94
  "lzip2\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys)"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    95
  "lzip2\<cdot>lNil\<cdot>lNil"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    96
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    97
fixpat lzip2_stricts [simp]:
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    98
  "lzip2\<cdot>\<bottom>\<cdot>ys"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
    99
  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom>"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   100
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   101
subsection {* mutual recursion with fixrec *}
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   102
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   103
text {* tree and forest types *}
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   104
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   105
domain 'a tree = Leaf (lazy 'a) | Branch (lazy "'a forest")
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   106
and    'a forest = Empty | Trees (lazy "'a tree") "'a forest"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   107
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   108
consts
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   109
  map_tree :: "('a \<rightarrow> 'b) \<rightarrow> ('a tree \<rightarrow> 'b tree)"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   110
  map_forest :: "('a \<rightarrow> 'b) \<rightarrow> ('a forest \<rightarrow> 'b forest)"
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
  To define mutually recursive functions, separate the equations
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   114
  for each function using the keyword "and".
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
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   117
fixrec
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   118
  "map_tree\<cdot>f\<cdot>(Leaf\<cdot>x) = Leaf\<cdot>(f\<cdot>x)"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   119
  "map_tree\<cdot>f\<cdot>(Branch\<cdot>ts) = Branch\<cdot>(map_forest\<cdot>f\<cdot>ts)"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   120
and
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   121
  "map_forest\<cdot>f\<cdot>Empty = Empty"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   122
  "ts \<noteq> \<bottom> \<Longrightarrow>
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   123
    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
   124
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   125
fixpat map_tree_strict [simp]: "map_tree\<cdot>f\<cdot>\<bottom>"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   126
fixpat map_forest_strict [simp]: "map_forest\<cdot>f\<cdot>\<bottom>"
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   127
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   128
text {*
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   129
  Theorems generated:
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   130
  map_tree_def map_forest_def
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   131
  map_tree_unfold map_forest_unfold
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   132
  map_tree_simps map_forest_simps
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   133
  map_tree_map_forest_induct
5841e7f9eef5 add new file to test fixrec package
huffman
parents:
diff changeset
   134
*}
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
end