src/HOLCF/Fixrec.thy
 author haftmann Fri Jun 17 16:12:49 2005 +0200 (2005-06-17) changeset 16417 9bc16273c2d4 parent 16401 57c35ede00b9 child 16460 72a08d509d62 permissions -rw-r--r--
migrated theory headers to new format
```     1 (*  Title:      HOLCF/Fixrec.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Amber Telfer and Brian Huffman
```
```     4 *)
```
```     5
```
```     6 header "Package for defining recursive functions in HOLCF"
```
```     7
```
```     8 theory Fixrec
```
```     9 imports Ssum One Up Fix
```
```    10 uses ("fixrec_package.ML")
```
```    11 begin
```
```    12
```
```    13 subsection {* Maybe monad type *}
```
```    14
```
```    15 types 'a maybe = "one ++ 'a u"
```
```    16
```
```    17 constdefs
```
```    18   fail :: "'a maybe"
```
```    19   "fail \<equiv> sinl\<cdot>ONE"
```
```    20
```
```    21   return :: "'a \<rightarrow> 'a maybe"
```
```    22   "return \<equiv> sinr oo up"
```
```    23
```
```    24 lemma maybeE:
```
```    25   "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = fail \<Longrightarrow> Q; \<And>x. p = return\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
```
```    26 apply (unfold fail_def return_def)
```
```    27 apply (rule_tac p=p in ssumE, simp)
```
```    28 apply (rule_tac p=x in oneE, simp, simp)
```
```    29 apply (rule_tac p=y in upE1, simp, simp)
```
```    30 done
```
```    31
```
```    32 subsection {* Monadic bind operator *}
```
```    33
```
```    34 constdefs
```
```    35   bind :: "'a maybe \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> 'b maybe"
```
```    36   "bind \<equiv> \<Lambda> m f. sscase\<cdot>sinl\<cdot>(fup\<cdot>f)\<cdot>m"
```
```    37
```
```    38 syntax
```
```    39   "_bind" :: "'a maybe \<Rightarrow> ('a \<rightarrow> 'b maybe) \<Rightarrow> 'b maybe"
```
```    40     ("(_ >>= _)" [50, 51] 50)
```
```    41
```
```    42 translations "m >>= k" == "bind\<cdot>m\<cdot>k"
```
```    43
```
```    44 nonterminals
```
```    45   maybebind maybebinds
```
```    46
```
```    47 syntax
```
```    48   "_MBIND"  :: "pttrn \<Rightarrow> 'a maybe \<Rightarrow> maybebind"         ("(2_ <-/ _)" 10)
```
```    49   ""        :: "maybebind \<Rightarrow> maybebinds"                ("_")
```
```    50
```
```    51   "_MBINDS" :: "[maybebind, maybebinds] \<Rightarrow> maybebinds"  ("_;/ _")
```
```    52   "_MDO"    :: "[maybebinds, 'a maybe] \<Rightarrow> 'a maybe"     ("(do _;/ (_))" 10)
```
```    53
```
```    54 translations
```
```    55   "_MDO (_MBINDS b bs) e" == "_MDO b (_MDO bs e)"
```
```    56   "do (x,y) <- m; e" == "m >>= (LAM <x,y>. e)"
```
```    57   "do x <- m; e"            == "m >>= (LAM x. e)"
```
```    58
```
```    59 text {* monad laws *}
```
```    60
```
```    61 lemma bind_strict [simp]: "UU >>= f = UU"
```
```    62 by (simp add: bind_def)
```
```    63
```
```    64 lemma bind_fail [simp]: "fail >>= f = fail"
```
```    65 by (simp add: bind_def fail_def)
```
```    66
```
```    67 lemma left_unit [simp]: "(return\<cdot>a) >>= k = k\<cdot>a"
```
```    68 by (simp add: bind_def return_def)
```
```    69
```
```    70 lemma right_unit [simp]: "m >>= return = m"
```
```    71 by (rule_tac p=m in maybeE, simp_all)
```
```    72
```
```    73 lemma bind_assoc [simp]:
```
```    74  "(do a <- m; b <- k\<cdot>a; h\<cdot>b) = (do b <- (do a <- m; k\<cdot>a); h\<cdot>b)"
```
```    75 by (rule_tac p=m in maybeE, simp_all)
```
```    76
```
```    77 subsection {* Run operator *}
```
```    78
```
```    79 constdefs
```
```    80   run:: "'a maybe \<rightarrow> 'a"
```
```    81   "run \<equiv> sscase\<cdot>\<bottom>\<cdot>(fup\<cdot>ID)"
```
```    82
```
```    83 text {* rewrite rules for run *}
```
```    84
```
```    85 lemma run_strict [simp]: "run\<cdot>\<bottom> = \<bottom>"
```
```    86 by (simp add: run_def)
```
```    87
```
```    88 lemma run_fail [simp]: "run\<cdot>fail = \<bottom>"
```
```    89 by (simp add: run_def fail_def)
```
```    90
```
```    91 lemma run_return [simp]: "run\<cdot>(return\<cdot>x) = x"
```
```    92 by (simp add: run_def return_def)
```
```    93
```
```    94 subsection {* Monad plus operator *}
```
```    95
```
```    96 constdefs
```
```    97   mplus :: "'a maybe \<rightarrow> 'a maybe \<rightarrow> 'a maybe"
```
```    98   "mplus \<equiv> \<Lambda> m1 m2. sscase\<cdot>(\<Lambda> x. m2)\<cdot>(fup\<cdot>return)\<cdot>m1"
```
```    99
```
```   100 syntax "+++" :: "'a maybe \<Rightarrow> 'a maybe \<Rightarrow> 'a maybe" (infixr 65)
```
```   101 translations "x +++ y" == "mplus\<cdot>x\<cdot>y"
```
```   102
```
```   103 text {* rewrite rules for mplus *}
```
```   104
```
```   105 lemma mplus_strict [simp]: "\<bottom> +++ m = \<bottom>"
```
```   106 by (simp add: mplus_def)
```
```   107
```
```   108 lemma mplus_fail [simp]: "fail +++ m = m"
```
```   109 by (simp add: mplus_def fail_def)
```
```   110
```
```   111 lemma mplus_return [simp]: "return\<cdot>x +++ m = return\<cdot>x"
```
```   112 by (simp add: mplus_def return_def)
```
```   113
```
```   114 lemma mplus_assoc: "(x +++ y) +++ z = x +++ (y +++ z)"
```
```   115 by (rule_tac p=x in maybeE, simp_all)
```
```   116
```
```   117 subsection {* Match functions for built-in types *}
```
```   118
```
```   119 text {* Currently the package only supports lazy constructors *}
```
```   120
```
```   121 constdefs
```
```   122   match_cpair :: "'a \<times> 'b \<rightarrow> ('a \<times> 'b) maybe"
```
```   123   "match_cpair \<equiv> csplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
```
```   124
```
```   125   match_up :: "'a u \<rightarrow> 'a maybe"
```
```   126   "match_up \<equiv> fup\<cdot>return"
```
```   127
```
```   128 lemma match_cpair_simps [simp]:
```
```   129   "match_cpair\<cdot><x,y> = return\<cdot><x,y>"
```
```   130 by (simp add: match_cpair_def)
```
```   131
```
```   132 lemma match_up_simps [simp]:
```
```   133   "match_up\<cdot>(up\<cdot>x) = return\<cdot>x"
```
```   134   "match_up\<cdot>\<bottom> = \<bottom>"
```
```   135 by (simp_all add: match_up_def)
```
```   136
```
```   137 subsection {* Mutual recursion *}
```
```   138
```
```   139 text {*
```
```   140   The following rules are used to prove unfolding theorems from
```
```   141   fixed-point definitions of mutually recursive functions.
```
```   142 *}
```
```   143
```
```   144 lemma cpair_equalI: "\<lbrakk>x \<equiv> cfst\<cdot>p; y \<equiv> csnd\<cdot>p\<rbrakk> \<Longrightarrow> <x,y> \<equiv> p"
```
```   145 by (simp add: surjective_pairing_Cprod2)
```
```   146
```
```   147 lemma cpair_eqD1: "<x,y> = <x',y'> \<Longrightarrow> x = x'"
```
```   148 by simp
```
```   149
```
```   150 lemma cpair_eqD2: "<x,y> = <x',y'> \<Longrightarrow> y = y'"
```
```   151 by simp
```
```   152
```
```   153 ML {*
```
```   154 val cpair_equalI = thm "cpair_equalI";
```
```   155 val cpair_eqD1 = thm "cpair_eqD1";
```
```   156 val cpair_eqD2 = thm "cpair_eqD2";
```
```   157 *}
```
```   158
```
```   159 subsection {* Intitializing the fixrec package *}
```
```   160
```
```   161 use "fixrec_package.ML"
```
```   162
```
```   163 end
```