src/HOLCF/Fixrec.thy
author huffman
Wed Nov 30 01:01:15 2005 +0100 (2005-11-30)
changeset 18293 4eaa654c92f2
parent 18112 dc1d6f588204
child 19092 e32cf29f01fc
permissions -rw-r--r--
reimplement Case expression pattern matching to support lazy patterns
huffman@16221
     1
(*  Title:      HOLCF/Fixrec.thy
huffman@16221
     2
    ID:         $Id$
huffman@16221
     3
    Author:     Amber Telfer and Brian Huffman
huffman@16221
     4
*)
huffman@16221
     5
huffman@16221
     6
header "Package for defining recursive functions in HOLCF"
huffman@16221
     7
huffman@16221
     8
theory Fixrec
huffman@16551
     9
imports Sprod Ssum Up One Tr Fix
haftmann@16417
    10
uses ("fixrec_package.ML")
huffman@16221
    11
begin
huffman@16221
    12
huffman@16221
    13
subsection {* Maybe monad type *}
huffman@16221
    14
huffman@16776
    15
defaultsort cpo
huffman@16776
    16
huffman@16221
    17
types 'a maybe = "one ++ 'a u"
huffman@16221
    18
huffman@16221
    19
constdefs
huffman@16221
    20
  fail :: "'a maybe"
huffman@16221
    21
  "fail \<equiv> sinl\<cdot>ONE"
huffman@16221
    22
huffman@16221
    23
  return :: "'a \<rightarrow> 'a maybe"
huffman@16221
    24
  "return \<equiv> sinr oo up"
huffman@16221
    25
huffman@16221
    26
lemma maybeE:
huffman@16221
    27
  "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = fail \<Longrightarrow> Q; \<And>x. p = return\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
huffman@16221
    28
apply (unfold fail_def return_def)
huffman@16221
    29
apply (rule_tac p=p in ssumE, simp)
huffman@16221
    30
apply (rule_tac p=x in oneE, simp, simp)
huffman@16754
    31
apply (rule_tac p=y in upE, simp, simp)
huffman@16221
    32
done
huffman@16221
    33
huffman@18293
    34
lemma return_defined [simp]: "return\<cdot>x \<noteq> \<bottom>"
huffman@18293
    35
by (simp add: return_def)
huffman@18293
    36
huffman@18293
    37
lemma fail_defined [simp]: "fail \<noteq> \<bottom>"
huffman@18293
    38
by (simp add: fail_def)
huffman@18293
    39
huffman@18293
    40
lemma return_eq [simp]: "(return\<cdot>x = return\<cdot>y) = (x = y)"
huffman@18293
    41
by (simp add: return_def)
huffman@18293
    42
huffman@18293
    43
lemma return_neq_fail [simp]:
huffman@18293
    44
  "return\<cdot>x \<noteq> fail" "fail \<noteq> return\<cdot>x"
huffman@18293
    45
by (simp_all add: return_def fail_def)
huffman@18293
    46
huffman@18293
    47
huffman@18097
    48
subsubsection {* Monadic bind operator *}
huffman@16221
    49
huffman@18097
    50
constdefs
huffman@18097
    51
  bind :: "'a maybe \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> 'b maybe"
huffman@18097
    52
  "bind \<equiv> \<Lambda> m f. sscase\<cdot>sinl\<cdot>(fup\<cdot>f)\<cdot>m"
huffman@18097
    53
huffman@18097
    54
syntax ">>=" :: "['a maybe, 'a \<rightarrow> 'b maybe] \<Rightarrow> 'b maybe" (infixl ">>=" 50)
huffman@18097
    55
translations "m >>= f" == "bind\<cdot>m\<cdot>f"
huffman@16221
    56
huffman@16221
    57
nonterminals
huffman@16221
    58
  maybebind maybebinds
huffman@16221
    59
huffman@16221
    60
syntax 
huffman@16221
    61
  "_MBIND"  :: "pttrn \<Rightarrow> 'a maybe \<Rightarrow> maybebind"         ("(2_ <-/ _)" 10)
huffman@16221
    62
  ""        :: "maybebind \<Rightarrow> maybebinds"                ("_")
huffman@16221
    63
huffman@16221
    64
  "_MBINDS" :: "[maybebind, maybebinds] \<Rightarrow> maybebinds"  ("_;/ _")
huffman@16221
    65
  "_MDO"    :: "[maybebinds, 'a maybe] \<Rightarrow> 'a maybe"     ("(do _;/ (_))" 10)
huffman@16221
    66
huffman@16221
    67
translations
huffman@16221
    68
  "_MDO (_MBINDS b bs) e" == "_MDO b (_MDO bs e)"
huffman@16221
    69
  "do (x,y) <- m; e" == "m >>= (LAM <x,y>. e)" 
huffman@16221
    70
  "do x <- m; e"            == "m >>= (LAM x. e)"
huffman@16221
    71
huffman@16221
    72
text {* monad laws *}
huffman@16221
    73
huffman@16221
    74
lemma bind_strict [simp]: "UU >>= f = UU"
huffman@16221
    75
by (simp add: bind_def)
huffman@16221
    76
huffman@16221
    77
lemma bind_fail [simp]: "fail >>= f = fail"
huffman@16221
    78
by (simp add: bind_def fail_def)
huffman@16221
    79
huffman@16221
    80
lemma left_unit [simp]: "(return\<cdot>a) >>= k = k\<cdot>a"
huffman@16221
    81
by (simp add: bind_def return_def)
huffman@16221
    82
huffman@16221
    83
lemma right_unit [simp]: "m >>= return = m"
huffman@16221
    84
by (rule_tac p=m in maybeE, simp_all)
huffman@16221
    85
huffman@16221
    86
lemma bind_assoc [simp]:
huffman@16779
    87
 "(do b <- (do a <- m; k\<cdot>a); h\<cdot>b) = (do a <- m; b <- k\<cdot>a; h\<cdot>b)"
huffman@16221
    88
by (rule_tac p=m in maybeE, simp_all)
huffman@16221
    89
huffman@18097
    90
subsubsection {* Run operator *}
huffman@16221
    91
huffman@16221
    92
constdefs
huffman@16776
    93
  run:: "'a::pcpo maybe \<rightarrow> 'a"
huffman@16221
    94
  "run \<equiv> sscase\<cdot>\<bottom>\<cdot>(fup\<cdot>ID)"
huffman@16221
    95
huffman@16221
    96
text {* rewrite rules for run *}
huffman@16221
    97
huffman@16221
    98
lemma run_strict [simp]: "run\<cdot>\<bottom> = \<bottom>"
huffman@16221
    99
by (simp add: run_def)
huffman@16221
   100
huffman@16221
   101
lemma run_fail [simp]: "run\<cdot>fail = \<bottom>"
huffman@16221
   102
by (simp add: run_def fail_def)
huffman@16221
   103
huffman@16221
   104
lemma run_return [simp]: "run\<cdot>(return\<cdot>x) = x"
huffman@16221
   105
by (simp add: run_def return_def)
huffman@16221
   106
huffman@18097
   107
subsubsection {* Monad plus operator *}
huffman@16221
   108
huffman@18097
   109
constdefs
huffman@18097
   110
  mplus :: "'a maybe \<rightarrow> 'a maybe \<rightarrow> 'a maybe"
huffman@18097
   111
  "mplus \<equiv> \<Lambda> m1 m2. sscase\<cdot>(\<Lambda> x. m2)\<cdot>(fup\<cdot>return)\<cdot>m1"
huffman@18097
   112
huffman@18097
   113
syntax "+++" :: "['a maybe, 'a maybe] \<Rightarrow> 'a maybe" (infixr "+++" 65)
huffman@18097
   114
translations "m1 +++ m2" == "mplus\<cdot>m1\<cdot>m2"
huffman@16221
   115
huffman@16221
   116
text {* rewrite rules for mplus *}
huffman@16221
   117
huffman@16221
   118
lemma mplus_strict [simp]: "\<bottom> +++ m = \<bottom>"
huffman@16221
   119
by (simp add: mplus_def)
huffman@16221
   120
huffman@16221
   121
lemma mplus_fail [simp]: "fail +++ m = m"
huffman@16221
   122
by (simp add: mplus_def fail_def)
huffman@16221
   123
huffman@16221
   124
lemma mplus_return [simp]: "return\<cdot>x +++ m = return\<cdot>x"
huffman@16221
   125
by (simp add: mplus_def return_def)
huffman@16221
   126
huffman@16460
   127
lemma mplus_fail2 [simp]: "m +++ fail = m"
huffman@16460
   128
by (rule_tac p=m in maybeE, simp_all)
huffman@16460
   129
huffman@16221
   130
lemma mplus_assoc: "(x +++ y) +++ z = x +++ (y +++ z)"
huffman@16221
   131
by (rule_tac p=x in maybeE, simp_all)
huffman@16221
   132
huffman@18097
   133
subsubsection {* Fatbar combinator *}
huffman@18097
   134
huffman@18097
   135
constdefs
huffman@18097
   136
  fatbar :: "('a \<rightarrow> 'b maybe) \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> ('a \<rightarrow> 'b maybe)"
huffman@18097
   137
  "fatbar \<equiv> \<Lambda> a b x. a\<cdot>x +++ b\<cdot>x"
huffman@18097
   138
huffman@18097
   139
syntax
huffman@18097
   140
  "\<parallel>" :: "['a \<rightarrow> 'b maybe, 'a \<rightarrow> 'b maybe] \<Rightarrow> 'a \<rightarrow> 'b maybe" (infixr "\<parallel>" 60)
huffman@18097
   141
translations
huffman@18097
   142
  "m1 \<parallel> m2" == "fatbar\<cdot>m1\<cdot>m2"
huffman@18097
   143
huffman@18097
   144
lemma fatbar1: "m\<cdot>x = \<bottom> \<Longrightarrow> (m \<parallel> ms)\<cdot>x = \<bottom>"
huffman@18097
   145
by (simp add: fatbar_def)
huffman@18097
   146
huffman@18097
   147
lemma fatbar2: "m\<cdot>x = fail \<Longrightarrow> (m \<parallel> ms)\<cdot>x = ms\<cdot>x"
huffman@18097
   148
by (simp add: fatbar_def)
huffman@18097
   149
huffman@18097
   150
lemma fatbar3: "m\<cdot>x = return\<cdot>y \<Longrightarrow> (m \<parallel> ms)\<cdot>x = return\<cdot>y"
huffman@18097
   151
by (simp add: fatbar_def)
huffman@18097
   152
huffman@18097
   153
lemmas fatbar_simps = fatbar1 fatbar2 fatbar3
huffman@18097
   154
huffman@18112
   155
lemma run_fatbar1: "m\<cdot>x = \<bottom> \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = \<bottom>"
huffman@18112
   156
by (simp add: fatbar_def)
huffman@18112
   157
huffman@18112
   158
lemma run_fatbar2: "m\<cdot>x = fail \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = run\<cdot>(ms\<cdot>x)"
huffman@18112
   159
by (simp add: fatbar_def)
huffman@18112
   160
huffman@18112
   161
lemma run_fatbar3: "m\<cdot>x = return\<cdot>y \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = y"
huffman@18112
   162
by (simp add: fatbar_def)
huffman@18112
   163
huffman@18112
   164
lemmas run_fatbar_simps [simp] = run_fatbar1 run_fatbar2 run_fatbar3
huffman@18112
   165
huffman@18293
   166
subsection {* Case branch combinator *}
huffman@18097
   167
huffman@18097
   168
constdefs
huffman@18293
   169
  branch :: "('a \<rightarrow> 'b maybe) \<Rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'c maybe)"
huffman@18293
   170
  "branch p \<equiv> \<Lambda> r x. bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> y. return\<cdot>(r\<cdot>y))"
huffman@18097
   171
huffman@18293
   172
lemma branch_rews:
huffman@18293
   173
  "p\<cdot>x = \<bottom> \<Longrightarrow> branch p\<cdot>r\<cdot>x = \<bottom>"
huffman@18293
   174
  "p\<cdot>x = fail \<Longrightarrow> branch p\<cdot>r\<cdot>x = fail"
huffman@18293
   175
  "p\<cdot>x = return\<cdot>y \<Longrightarrow> branch p\<cdot>r\<cdot>x = return\<cdot>(r\<cdot>y)"
huffman@18293
   176
by (simp_all add: branch_def)
huffman@18097
   177
huffman@18293
   178
lemma branch_return [simp]: "branch return\<cdot>r\<cdot>x = return\<cdot>(r\<cdot>x)"
huffman@18293
   179
by (simp add: branch_def)
huffman@18293
   180
huffman@18097
   181
huffman@18097
   182
subsection {* Case syntax *}
huffman@18097
   183
huffman@18097
   184
nonterminals
huffman@18097
   185
  Case_syn  Cases_syn
huffman@18097
   186
huffman@18097
   187
syntax
huffman@18097
   188
  "_Case_syntax":: "['a, Cases_syn] => 'b"               ("(Case _ of/ _)" 10)
huffman@18097
   189
  "_Case1"      :: "['a, 'b] => Case_syn"                ("(2_ =>/ _)" 10)
huffman@18097
   190
  ""            :: "Case_syn => Cases_syn"               ("_")
huffman@18097
   191
  "_Case2"      :: "[Case_syn, Cases_syn] => Cases_syn"  ("_/ | _")
huffman@18097
   192
huffman@18097
   193
syntax (xsymbols)
huffman@18097
   194
  "_Case1"      :: "['a, 'b] => Case_syn"                ("(2_ \<Rightarrow>/ _)" 10)
huffman@18097
   195
huffman@18293
   196
translations
huffman@18293
   197
  "_Case_syntax x ms" == "run\<cdot>(ms\<cdot>x)"
huffman@18293
   198
  "_Case2 m ms" == "m \<parallel> ms"
huffman@18112
   199
huffman@18112
   200
text {* Parsing Case expressions *}
huffman@18097
   201
huffman@18293
   202
syntax
huffman@18293
   203
  "_pat" :: "'a"
huffman@18293
   204
  "_var" :: "'a"
huffman@18293
   205
huffman@18097
   206
translations
huffman@18293
   207
  "_Case1 p r" => "branch (_pat p)\<cdot>(_var p r)"
huffman@18293
   208
  "_var (_args x y) r" => "csplit\<cdot>(_var x (_var y r))"
huffman@18293
   209
  "_var () r" => "unit_when\<cdot>r"
huffman@18112
   210
huffman@18112
   211
parse_translation {*
huffman@18293
   212
(* rewrites (_pat x) => (return) *)
huffman@18293
   213
(* rewrites (_var x t) => (Abs_CFun (%x. t)) *)
huffman@18293
   214
  [("_pat", K (Syntax.const "return")),
huffman@18293
   215
   mk_binder_tr ("_var", "Abs_CFun")];
huffman@18112
   216
*}
huffman@18112
   217
huffman@18112
   218
text {* Printing Case expressions *}
huffman@18112
   219
huffman@18293
   220
syntax
huffman@18293
   221
  "_match" :: "'a"
huffman@18097
   222
huffman@18112
   223
print_translation {*
huffman@18112
   224
  let
huffman@18293
   225
    fun dest_LAM (Const ("Rep_CFun",_) $ Const ("unit_when",_) $ t) =
huffman@18293
   226
          (Syntax.const "Unity", t)
huffman@18293
   227
    |   dest_LAM (Const ("Rep_CFun",_) $ Const ("csplit",_) $ t) =
huffman@18293
   228
          let
huffman@18293
   229
            val (v1, t1) = dest_LAM t;
huffman@18293
   230
            val (v2, t2) = dest_LAM t1;
huffman@18293
   231
          in (Syntax.const "_args" $ v1 $ v2, t2) end 
huffman@18293
   232
    |   dest_LAM (Const ("Abs_CFun",_) $ t) =
huffman@18112
   233
          let
huffman@18293
   234
            val abs = case t of Abs abs => abs
huffman@18293
   235
                | _ => ("x", dummyT, incr_boundvars 1 t $ Bound 0);
huffman@18293
   236
            val (x, t') = atomic_abs_tr' abs;
huffman@18293
   237
          in (Syntax.const "_var" $ x, t') end
huffman@18293
   238
    |   dest_LAM _ = raise Match; (* too few vars: abort translation *)
huffman@18097
   239
huffman@18293
   240
    fun Case1_tr' [Const("branch",_) $ p, r] =
huffman@18293
   241
          let val (v, t) = dest_LAM r;
huffman@18293
   242
          in Syntax.const "_Case1" $ (Syntax.const "_match" $ p $ v) $ t end;
huffman@18112
   243
huffman@18293
   244
  in [("Rep_CFun", Case1_tr')] end;
huffman@18112
   245
*}
huffman@18097
   246
huffman@18293
   247
translations
huffman@18293
   248
  "x" <= "_match return (_var x)"
huffman@18293
   249
huffman@18293
   250
huffman@18293
   251
subsection {* Pattern combinators for data constructors *}
huffman@18293
   252
huffman@18293
   253
types ('a, 'b) pat = "'a \<rightarrow> 'b maybe"
huffman@18097
   254
huffman@18097
   255
constdefs
huffman@18293
   256
  cpair_pat :: "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a \<times> 'b, 'c \<times> 'd) pat"
huffman@18293
   257
  "cpair_pat p1 p2 \<equiv> \<Lambda>\<langle>x, y\<rangle>. do a <- p1\<cdot>x; b <- p2\<cdot>y; return\<cdot>\<langle>a, b\<rangle>"
huffman@18097
   258
huffman@18293
   259
  spair_pat ::
huffman@18293
   260
  "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a::pcpo \<otimes> 'b::pcpo, 'c \<times> 'd) pat"
huffman@18293
   261
  "spair_pat p1 p2 \<equiv> \<Lambda>(:x, y:). cpair_pat p1 p2\<cdot>\<langle>x, y\<rangle>"
huffman@18097
   262
huffman@18293
   263
  sinl_pat :: "('a, 'c) pat \<Rightarrow> ('a::pcpo \<oplus> 'b::pcpo, 'c) pat"
huffman@18293
   264
  "sinl_pat p \<equiv> sscase\<cdot>p\<cdot>(\<Lambda> x. fail)"
huffman@18097
   265
huffman@18293
   266
  sinr_pat :: "('b, 'c) pat \<Rightarrow> ('a::pcpo \<oplus> 'b::pcpo, 'c) pat"
huffman@18293
   267
  "sinr_pat p \<equiv> sscase\<cdot>(\<Lambda> x. fail)\<cdot>p"
huffman@18293
   268
huffman@18293
   269
  up_pat :: "('a, 'b) pat \<Rightarrow> ('a u, 'b) pat"
huffman@18293
   270
  "up_pat p \<equiv> fup\<cdot>p"
huffman@18097
   271
huffman@18293
   272
  TT_pat :: "(tr, unit) pat"
huffman@18293
   273
  "TT_pat \<equiv> \<Lambda> b. If b then return\<cdot>() else fail fi"
huffman@18097
   274
huffman@18293
   275
  FF_pat :: "(tr, unit) pat"
huffman@18293
   276
  "FF_pat \<equiv> \<Lambda> b. If b then fail else return\<cdot>() fi"
huffman@18097
   277
huffman@18293
   278
  ONE_pat :: "(one, unit) pat"
huffman@18293
   279
  "ONE_pat \<equiv> \<Lambda> ONE. return\<cdot>()"
huffman@18097
   280
huffman@18293
   281
text {* Parse translations (patterns) *}
huffman@18097
   282
translations
huffman@18293
   283
  "_pat (cpair\<cdot>x\<cdot>y)" => "cpair_pat (_pat x) (_pat y)"
huffman@18293
   284
  "_pat (spair\<cdot>x\<cdot>y)" => "spair_pat (_pat x) (_pat y)"
huffman@18293
   285
  "_pat (sinl\<cdot>x)" => "sinl_pat (_pat x)"
huffman@18293
   286
  "_pat (sinr\<cdot>x)" => "sinr_pat (_pat x)"
huffman@18293
   287
  "_pat (up\<cdot>x)" => "up_pat (_pat x)"
huffman@18293
   288
  "_pat TT" => "TT_pat"
huffman@18293
   289
  "_pat FF" => "FF_pat"
huffman@18293
   290
  "_pat ONE" => "ONE_pat"
huffman@18293
   291
huffman@18293
   292
text {* Parse translations (variables) *}
huffman@18293
   293
translations
huffman@18293
   294
  "_var (cpair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
huffman@18293
   295
  "_var (spair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
huffman@18293
   296
  "_var (sinl\<cdot>x) r" => "_var x r"
huffman@18293
   297
  "_var (sinr\<cdot>x) r" => "_var x r"
huffman@18293
   298
  "_var (up\<cdot>x) r" => "_var x r"
huffman@18293
   299
  "_var TT r" => "_var () r"
huffman@18293
   300
  "_var FF r" => "_var () r"
huffman@18293
   301
  "_var ONE r" => "_var () r"
huffman@18097
   302
huffman@18112
   303
text {* Print translations *}
huffman@18097
   304
translations
huffman@18293
   305
  "cpair\<cdot>(_match p1 v1)\<cdot>(_match p2 v2)"
huffman@18293
   306
      <= "_match (cpair_pat p1 p2) (_args v1 v2)"
huffman@18293
   307
  "spair\<cdot>(_match p1 v1)\<cdot>(_match p2 v2)"
huffman@18293
   308
      <= "_match (spair_pat p1 p2) (_args v1 v2)"
huffman@18293
   309
  "sinl\<cdot>(_match p1 v1)" <= "_match (sinl_pat p1) v1"
huffman@18293
   310
  "sinr\<cdot>(_match p1 v1)" <= "_match (sinr_pat p1) v1"
huffman@18293
   311
  "up\<cdot>(_match p1 v1)" <= "_match (up_pat p1) v1"
huffman@18293
   312
  "TT" <= "_match TT_pat ()"
huffman@18293
   313
  "FF" <= "_match FF_pat ()"
huffman@18293
   314
  "ONE" <= "_match ONE_pat ()"
huffman@18293
   315
huffman@18293
   316
lemma cpair_pat1:
huffman@18293
   317
  "branch p\<cdot>r\<cdot>x = \<bottom> \<Longrightarrow> branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>\<langle>x, y\<rangle> = \<bottom>"
huffman@18293
   318
apply (simp add: branch_def cpair_pat_def)
huffman@18293
   319
apply (rule_tac p="p\<cdot>x" in maybeE, simp_all)
huffman@18293
   320
done
huffman@18097
   321
huffman@18293
   322
lemma cpair_pat2:
huffman@18293
   323
  "branch p\<cdot>r\<cdot>x = fail \<Longrightarrow> branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>\<langle>x, y\<rangle> = fail"
huffman@18293
   324
apply (simp add: branch_def cpair_pat_def)
huffman@18293
   325
apply (rule_tac p="p\<cdot>x" in maybeE, simp_all)
huffman@18293
   326
done
huffman@18097
   327
huffman@18293
   328
lemma cpair_pat3:
huffman@18293
   329
  "branch p\<cdot>r\<cdot>x = return\<cdot>s \<Longrightarrow>
huffman@18293
   330
   branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>\<langle>x, y\<rangle> = branch q\<cdot>s\<cdot>y"
huffman@18293
   331
apply (simp add: branch_def cpair_pat_def)
huffman@18293
   332
apply (rule_tac p="p\<cdot>x" in maybeE, simp_all)
huffman@18293
   333
apply (rule_tac p="q\<cdot>y" in maybeE, simp_all)
huffman@18293
   334
done
huffman@18097
   335
huffman@18293
   336
lemmas cpair_pat [simp] =
huffman@18293
   337
  cpair_pat1 cpair_pat2 cpair_pat3
huffman@18097
   338
huffman@18293
   339
lemma spair_pat [simp]:
huffman@18293
   340
  "branch (spair_pat p1 p2)\<cdot>r\<cdot>\<bottom> = \<bottom>"
huffman@18293
   341
  "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk>
huffman@18293
   342
     \<Longrightarrow> branch (spair_pat p1 p2)\<cdot>r\<cdot>(:x, y:) =
huffman@18293
   343
         branch (cpair_pat p1 p2)\<cdot>r\<cdot>\<langle>x, y\<rangle>"
huffman@18293
   344
by (simp_all add: branch_def spair_pat_def)
huffman@18097
   345
huffman@18293
   346
lemma sinl_pat [simp]:
huffman@18293
   347
  "branch (sinl_pat p)\<cdot>r\<cdot>\<bottom> = \<bottom>"
huffman@18293
   348
  "x \<noteq> \<bottom> \<Longrightarrow> branch (sinl_pat p)\<cdot>r\<cdot>(sinl\<cdot>x) = branch p\<cdot>r\<cdot>x"
huffman@18293
   349
  "y \<noteq> \<bottom> \<Longrightarrow> branch (sinl_pat p)\<cdot>r\<cdot>(sinr\<cdot>y) = fail"
huffman@18293
   350
by (simp_all add: branch_def sinl_pat_def)
huffman@18097
   351
huffman@18293
   352
lemma sinr_pat [simp]:
huffman@18293
   353
  "branch (sinr_pat p)\<cdot>r\<cdot>\<bottom> = \<bottom>"
huffman@18293
   354
  "x \<noteq> \<bottom> \<Longrightarrow> branch (sinr_pat p)\<cdot>r\<cdot>(sinl\<cdot>x) = fail"
huffman@18293
   355
  "y \<noteq> \<bottom> \<Longrightarrow> branch (sinr_pat p)\<cdot>r\<cdot>(sinr\<cdot>y) = branch p\<cdot>r\<cdot>y"
huffman@18293
   356
by (simp_all add: branch_def sinr_pat_def)
huffman@18097
   357
huffman@18293
   358
lemma up_pat [simp]:
huffman@18293
   359
  "branch (up_pat p)\<cdot>r\<cdot>\<bottom> = \<bottom>"
huffman@18293
   360
  "branch (up_pat p)\<cdot>r\<cdot>(up\<cdot>x) = branch p\<cdot>r\<cdot>x"
huffman@18293
   361
by (simp_all add: branch_def up_pat_def)
huffman@18293
   362
huffman@18293
   363
lemma TT_pat [simp]:
huffman@18293
   364
  "branch TT_pat\<cdot>(unit_when\<cdot>r)\<cdot>\<bottom> = \<bottom>"
huffman@18293
   365
  "branch TT_pat\<cdot>(unit_when\<cdot>r)\<cdot>TT = return\<cdot>r"
huffman@18293
   366
  "branch TT_pat\<cdot>(unit_when\<cdot>r)\<cdot>FF = fail"
huffman@18293
   367
by (simp_all add: branch_def TT_pat_def)
huffman@18097
   368
huffman@18293
   369
lemma FF_pat [simp]:
huffman@18293
   370
  "branch FF_pat\<cdot>(unit_when\<cdot>r)\<cdot>\<bottom> = \<bottom>"
huffman@18293
   371
  "branch FF_pat\<cdot>(unit_when\<cdot>r)\<cdot>TT = fail"
huffman@18293
   372
  "branch FF_pat\<cdot>(unit_when\<cdot>r)\<cdot>FF = return\<cdot>r"
huffman@18293
   373
by (simp_all add: branch_def FF_pat_def)
huffman@18097
   374
huffman@18293
   375
lemma ONE_pat [simp]:
huffman@18293
   376
  "branch ONE_pat\<cdot>(unit_when\<cdot>r)\<cdot>\<bottom> = \<bottom>"
huffman@18293
   377
  "branch ONE_pat\<cdot>(unit_when\<cdot>r)\<cdot>ONE = return\<cdot>r"
huffman@18293
   378
by (simp_all add: branch_def ONE_pat_def)
huffman@18097
   379
huffman@18293
   380
huffman@18293
   381
subsection {* Wildcards, as-patterns, and lazy patterns *}
huffman@18112
   382
huffman@18112
   383
syntax
huffman@18293
   384
  "_as_pat" :: "[idt, 'a] \<Rightarrow> 'a" (infixr "\<as>" 10)
huffman@18293
   385
  "_lazy_pat" :: "'a \<Rightarrow> 'a" ("\<lazy> _" [1000] 1000)
huffman@18112
   386
huffman@18112
   387
constdefs
huffman@18293
   388
  wild_pat :: "'a \<rightarrow> unit maybe"
huffman@18293
   389
  "wild_pat \<equiv> \<Lambda> x. return\<cdot>()"
huffman@18293
   390
huffman@18293
   391
  as_pat :: "('a \<rightarrow> 'b maybe) \<Rightarrow> 'a \<rightarrow> ('a \<times> 'b) maybe"
huffman@18293
   392
  "as_pat p \<equiv> \<Lambda> x. do a <- p\<cdot>x; return\<cdot>\<langle>x, a\<rangle>"
huffman@18112
   393
huffman@18293
   394
  lazy_pat :: "('a \<rightarrow> 'b::pcpo maybe) \<Rightarrow> ('a \<rightarrow> 'b maybe)"
huffman@18293
   395
  "lazy_pat p \<equiv> \<Lambda> x. return\<cdot>(run\<cdot>(p\<cdot>x))"
huffman@18293
   396
huffman@18293
   397
text {* Parse translations (patterns) *}
huffman@18293
   398
translations
huffman@18293
   399
  "_pat _" => "wild_pat"
huffman@18293
   400
  "_pat (_as_pat x y)" => "as_pat (_pat y)"
huffman@18293
   401
  "_pat (_lazy_pat x)" => "lazy_pat (_pat x)"
huffman@18293
   402
huffman@18293
   403
text {* Parse translations (variables) *}
huffman@18112
   404
translations
huffman@18293
   405
  "_var _ r" => "_var () r"
huffman@18293
   406
  "_var (_as_pat x y) r" => "_var (_args x y) r"
huffman@18293
   407
  "_var (_lazy_pat x) r" => "_var x r"
huffman@18293
   408
huffman@18293
   409
text {* Print translations *}
huffman@18293
   410
translations
huffman@18293
   411
  "_" <= "_match wild_pat ()"
huffman@18293
   412
  "_as_pat x (_match p v)" <= "_match (as_pat p) (_args (_var x) v)"
huffman@18293
   413
  "_lazy_pat (_match p v)" <= "_match (lazy_pat p) v"
huffman@18293
   414
huffman@18293
   415
lemma wild_pat [simp]: "branch wild_pat\<cdot>(unit_when\<cdot>r)\<cdot>x = return\<cdot>r"
huffman@18293
   416
by (simp add: branch_def wild_pat_def)
huffman@18112
   417
huffman@18293
   418
lemma as_pat [simp]:
huffman@18293
   419
  "branch (as_pat p)\<cdot>(csplit\<cdot>r)\<cdot>x = branch p\<cdot>(r\<cdot>x)\<cdot>x"
huffman@18293
   420
apply (simp add: branch_def as_pat_def)
huffman@18293
   421
apply (rule_tac p="p\<cdot>x" in maybeE, simp_all)
huffman@18293
   422
done
huffman@18293
   423
huffman@18293
   424
lemma lazy_pat [simp]:
huffman@18293
   425
  "branch p\<cdot>r\<cdot>x = \<bottom> \<Longrightarrow> branch (lazy_pat p)\<cdot>r\<cdot>x = return\<cdot>(r\<cdot>\<bottom>)"
huffman@18293
   426
  "branch p\<cdot>r\<cdot>x = fail \<Longrightarrow> branch (lazy_pat p)\<cdot>r\<cdot>x = return\<cdot>(r\<cdot>\<bottom>)"
huffman@18293
   427
  "branch p\<cdot>r\<cdot>x = return\<cdot>s \<Longrightarrow> branch (lazy_pat p)\<cdot>r\<cdot>x = return\<cdot>s"
huffman@18293
   428
apply (simp_all add: branch_def lazy_pat_def)
huffman@18293
   429
apply (rule_tac [!] p="p\<cdot>x" in maybeE, simp_all)
huffman@18293
   430
done
huffman@18293
   431
huffman@18112
   432
huffman@16221
   433
subsection {* Match functions for built-in types *}
huffman@16221
   434
huffman@16776
   435
defaultsort pcpo
huffman@16776
   436
huffman@16221
   437
constdefs
huffman@16776
   438
  match_UU :: "'a \<rightarrow> unit maybe"
huffman@16776
   439
  "match_UU \<equiv> \<Lambda> x. fail"
huffman@16776
   440
huffman@16776
   441
  match_cpair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<times> 'b) maybe"
huffman@16221
   442
  "match_cpair \<equiv> csplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
huffman@16221
   443
huffman@16551
   444
  match_spair :: "'a \<otimes> 'b \<rightarrow> ('a \<times> 'b) maybe"
huffman@16551
   445
  "match_spair \<equiv> ssplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)"
huffman@16551
   446
huffman@16551
   447
  match_sinl :: "'a \<oplus> 'b \<rightarrow> 'a maybe"
huffman@16551
   448
  "match_sinl \<equiv> sscase\<cdot>return\<cdot>(\<Lambda> y. fail)"
huffman@16551
   449
huffman@16551
   450
  match_sinr :: "'a \<oplus> 'b \<rightarrow> 'b maybe"
huffman@16551
   451
  "match_sinr \<equiv> sscase\<cdot>(\<Lambda> x. fail)\<cdot>return"
huffman@16551
   452
huffman@16776
   453
  match_up :: "'a::cpo u \<rightarrow> 'a maybe"
huffman@16221
   454
  "match_up \<equiv> fup\<cdot>return"
huffman@16221
   455
huffman@16460
   456
  match_ONE :: "one \<rightarrow> unit maybe"
huffman@18094
   457
  "match_ONE \<equiv> \<Lambda> ONE. return\<cdot>()"
huffman@18094
   458
 
huffman@16460
   459
  match_TT :: "tr \<rightarrow> unit maybe"
huffman@18094
   460
  "match_TT \<equiv> \<Lambda> b. If b then return\<cdot>() else fail fi"
huffman@18094
   461
 
huffman@16460
   462
  match_FF :: "tr \<rightarrow> unit maybe"
huffman@18094
   463
  "match_FF \<equiv> \<Lambda> b. If b then fail else return\<cdot>() fi"
huffman@16460
   464
huffman@16776
   465
lemma match_UU_simps [simp]:
huffman@16776
   466
  "match_UU\<cdot>x = fail"
huffman@16776
   467
by (simp add: match_UU_def)
huffman@16776
   468
huffman@16221
   469
lemma match_cpair_simps [simp]:
huffman@16221
   470
  "match_cpair\<cdot><x,y> = return\<cdot><x,y>"
huffman@16221
   471
by (simp add: match_cpair_def)
huffman@16221
   472
huffman@16551
   473
lemma match_spair_simps [simp]:
huffman@16551
   474
  "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> match_spair\<cdot>(:x,y:) = return\<cdot><x,y>"
huffman@16551
   475
  "match_spair\<cdot>\<bottom> = \<bottom>"
huffman@16551
   476
by (simp_all add: match_spair_def)
huffman@16551
   477
huffman@16551
   478
lemma match_sinl_simps [simp]:
huffman@16551
   479
  "x \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinl\<cdot>x) = return\<cdot>x"
huffman@16551
   480
  "x \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinr\<cdot>x) = fail"
huffman@16551
   481
  "match_sinl\<cdot>\<bottom> = \<bottom>"
huffman@16551
   482
by (simp_all add: match_sinl_def)
huffman@16551
   483
huffman@16551
   484
lemma match_sinr_simps [simp]:
huffman@16551
   485
  "x \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinr\<cdot>x) = return\<cdot>x"
huffman@16551
   486
  "x \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinl\<cdot>x) = fail"
huffman@16551
   487
  "match_sinr\<cdot>\<bottom> = \<bottom>"
huffman@16551
   488
by (simp_all add: match_sinr_def)
huffman@16551
   489
huffman@16221
   490
lemma match_up_simps [simp]:
huffman@16221
   491
  "match_up\<cdot>(up\<cdot>x) = return\<cdot>x"
huffman@16221
   492
  "match_up\<cdot>\<bottom> = \<bottom>"
huffman@16221
   493
by (simp_all add: match_up_def)
huffman@16221
   494
huffman@16460
   495
lemma match_ONE_simps [simp]:
huffman@16460
   496
  "match_ONE\<cdot>ONE = return\<cdot>()"
huffman@16460
   497
  "match_ONE\<cdot>\<bottom> = \<bottom>"
huffman@18094
   498
by (simp_all add: match_ONE_def)
huffman@16460
   499
huffman@16460
   500
lemma match_TT_simps [simp]:
huffman@16460
   501
  "match_TT\<cdot>TT = return\<cdot>()"
huffman@16460
   502
  "match_TT\<cdot>FF = fail"
huffman@16460
   503
  "match_TT\<cdot>\<bottom> = \<bottom>"
huffman@18094
   504
by (simp_all add: match_TT_def)
huffman@16460
   505
huffman@16460
   506
lemma match_FF_simps [simp]:
huffman@16460
   507
  "match_FF\<cdot>FF = return\<cdot>()"
huffman@16460
   508
  "match_FF\<cdot>TT = fail"
huffman@16460
   509
  "match_FF\<cdot>\<bottom> = \<bottom>"
huffman@18094
   510
by (simp_all add: match_FF_def)
huffman@16460
   511
huffman@16401
   512
subsection {* Mutual recursion *}
huffman@16401
   513
huffman@16401
   514
text {*
huffman@16401
   515
  The following rules are used to prove unfolding theorems from
huffman@16401
   516
  fixed-point definitions of mutually recursive functions.
huffman@16401
   517
*}
huffman@16401
   518
huffman@16401
   519
lemma cpair_equalI: "\<lbrakk>x \<equiv> cfst\<cdot>p; y \<equiv> csnd\<cdot>p\<rbrakk> \<Longrightarrow> <x,y> \<equiv> p"
huffman@16401
   520
by (simp add: surjective_pairing_Cprod2)
huffman@16401
   521
huffman@16401
   522
lemma cpair_eqD1: "<x,y> = <x',y'> \<Longrightarrow> x = x'"
huffman@16401
   523
by simp
huffman@16401
   524
huffman@16401
   525
lemma cpair_eqD2: "<x,y> = <x',y'> \<Longrightarrow> y = y'"
huffman@16401
   526
by simp
huffman@16401
   527
huffman@16463
   528
text {* lemma for proving rewrite rules *}
huffman@16463
   529
huffman@16463
   530
lemma ssubst_lhs: "\<lbrakk>t = s; P s = Q\<rbrakk> \<Longrightarrow> P t = Q"
huffman@16463
   531
by simp
huffman@16463
   532
huffman@16401
   533
ML {*
huffman@16401
   534
val cpair_equalI = thm "cpair_equalI";
huffman@16401
   535
val cpair_eqD1 = thm "cpair_eqD1";
huffman@16401
   536
val cpair_eqD2 = thm "cpair_eqD2";
huffman@16463
   537
val ssubst_lhs = thm "ssubst_lhs";
huffman@18293
   538
val branch_def = thm "branch_def";
huffman@16401
   539
*}
huffman@16221
   540
huffman@16758
   541
subsection {* Initializing the fixrec package *}
huffman@16221
   542
huffman@16229
   543
use "fixrec_package.ML"
huffman@16221
   544
huffman@16221
   545
end