Theory Fixrec

Up to index of Isabelle/HOLCF

theory Fixrec
imports Sprod Ssum Up One Tr Fix
uses (fixrec_package.ML)
begin

(*  Title:      HOLCF/Fixrec.thy
    ID:         $Id: Fixrec.thy,v 1.11 2005/07/12 16:44:32 huffman Exp $
    Author:     Amber Telfer and Brian Huffman
*)

header "Package for defining recursive functions in HOLCF"

theory Fixrec
imports Sprod Ssum Up One Tr Fix
uses ("fixrec_package.ML")
begin

subsection {* Maybe monad type *}

defaultsort cpo

types 'a maybe = "one ++ 'a u"

constdefs
  fail :: "'a maybe"
  "fail ≡ sinl·ONE"

  return :: "'a -> 'a maybe"
  "return ≡ sinr oo up"

lemma maybeE:
  "[|p = ⊥ ==> Q; p = fail ==> Q; !!x. p = return·x ==> Q|] ==> Q"
apply (unfold fail_def return_def)
apply (rule_tac p=p in ssumE, simp)
apply (rule_tac p=x in oneE, simp, simp)
apply (rule_tac p=y in upE, simp, simp)
done

subsection {* Monadic bind operator *}

constdefs
  bind :: "'a maybe -> ('a -> 'b maybe) -> 'b maybe"
  "bind ≡ Λ m f. sscase·sinl·(fup·f)·m"

syntax
  "_bind" :: "'a maybe => ('a -> 'b maybe) => 'b maybe"
    ("(_ >>= _)" [50, 51] 50)

translations "m >>= k" == "bind·m·k"

nonterminals
  maybebind maybebinds

syntax 
  "_MBIND"  :: "pttrn => 'a maybe => maybebind"         ("(2_ <-/ _)" 10)
  ""        :: "maybebind => maybebinds"                ("_")

  "_MBINDS" :: "[maybebind, maybebinds] => maybebinds"  ("_;/ _")
  "_MDO"    :: "[maybebinds, 'a maybe] => 'a maybe"     ("(do _;/ (_))" 10)

translations
  "_MDO (_MBINDS b bs) e" == "_MDO b (_MDO bs e)"
  "do (x,y) <- m; e" == "m >>= (LAM <x,y>. e)" 
  "do x <- m; e"            == "m >>= (LAM x. e)"

text {* monad laws *}

lemma bind_strict [simp]: "UU >>= f = UU"
by (simp add: bind_def)

lemma bind_fail [simp]: "fail >>= f = fail"
by (simp add: bind_def fail_def)

lemma left_unit [simp]: "(return·a) >>= k = k·a"
by (simp add: bind_def return_def)

lemma right_unit [simp]: "m >>= return = m"
by (rule_tac p=m in maybeE, simp_all)

lemma bind_assoc [simp]:
 "(do b <- (do a <- m; k·a); h·b) = (do a <- m; b <- k·a; h·b)"
by (rule_tac p=m in maybeE, simp_all)

subsection {* Run operator *}

constdefs
  run:: "'a::pcpo maybe -> 'a"
  "run ≡ sscase·⊥·(fup·ID)"

text {* rewrite rules for run *}

lemma run_strict [simp]: "run·⊥ = ⊥"
by (simp add: run_def)

lemma run_fail [simp]: "run·fail = ⊥"
by (simp add: run_def fail_def)

lemma run_return [simp]: "run·(return·x) = x"
by (simp add: run_def return_def)

subsection {* Monad plus operator *}

constdefs
  mplus :: "'a maybe -> 'a maybe -> 'a maybe"
  "mplus ≡ Λ m1 m2. sscase·(Λ x. m2)·(fup·return)·m1"

syntax "+++" :: "'a maybe => 'a maybe => 'a maybe" (infixr 65)
translations "x +++ y" == "mplus·x·y"

text {* rewrite rules for mplus *}

lemma mplus_strict [simp]: "⊥ +++ m = ⊥"
by (simp add: mplus_def)

lemma mplus_fail [simp]: "fail +++ m = m"
by (simp add: mplus_def fail_def)

lemma mplus_return [simp]: "return·x +++ m = return·x"
by (simp add: mplus_def return_def)

lemma mplus_fail2 [simp]: "m +++ fail = m"
by (rule_tac p=m in maybeE, simp_all)

lemma mplus_assoc: "(x +++ y) +++ z = x +++ (y +++ z)"
by (rule_tac p=x in maybeE, simp_all)

subsection {* Match functions for built-in types *}

defaultsort pcpo

constdefs
  match_UU :: "'a -> unit maybe"
  "match_UU ≡ Λ x. fail"

  match_cpair :: "'a::cpo × 'b::cpo -> ('a × 'b) maybe"
  "match_cpair ≡ csplit·(Λ x y. return·<x,y>)"

  match_spair :: "'a ⊗ 'b -> ('a × 'b) maybe"
  "match_spair ≡ ssplit·(Λ x y. return·<x,y>)"

  match_sinl :: "'a ⊕ 'b -> 'a maybe"
  "match_sinl ≡ sscase·return·(Λ y. fail)"

  match_sinr :: "'a ⊕ 'b -> 'b maybe"
  "match_sinr ≡ sscase·(Λ x. fail)·return"

  match_up :: "'a::cpo u -> 'a maybe"
  "match_up ≡ fup·return"

  match_ONE :: "one -> unit maybe"
  "match_ONE ≡ flift1 (λu. return·())"

  match_TT :: "tr -> unit maybe"
  "match_TT ≡ flift1 (λb. if b then return·() else fail)"

  match_FF :: "tr -> unit maybe"
  "match_FF ≡ flift1 (λb. if b then fail else return·())"

lemma match_UU_simps [simp]:
  "match_UU·x = fail"
by (simp add: match_UU_def)

lemma match_cpair_simps [simp]:
  "match_cpair·<x,y> = return·<x,y>"
by (simp add: match_cpair_def)

lemma match_spair_simps [simp]:
  "[|x ≠ ⊥; y ≠ ⊥|] ==> match_spair·(:x,y:) = return·<x,y>"
  "match_spair·⊥ = ⊥"
by (simp_all add: match_spair_def)

lemma match_sinl_simps [simp]:
  "x ≠ ⊥ ==> match_sinl·(sinl·x) = return·x"
  "x ≠ ⊥ ==> match_sinl·(sinr·x) = fail"
  "match_sinl·⊥ = ⊥"
by (simp_all add: match_sinl_def)

lemma match_sinr_simps [simp]:
  "x ≠ ⊥ ==> match_sinr·(sinr·x) = return·x"
  "x ≠ ⊥ ==> match_sinr·(sinl·x) = fail"
  "match_sinr·⊥ = ⊥"
by (simp_all add: match_sinr_def)

lemma match_up_simps [simp]:
  "match_up·(up·x) = return·x"
  "match_up·⊥ = ⊥"
by (simp_all add: match_up_def)

lemma match_ONE_simps [simp]:
  "match_ONE·ONE = return·()"
  "match_ONE·⊥ = ⊥"
by (simp_all add: ONE_def match_ONE_def)

lemma match_TT_simps [simp]:
  "match_TT·TT = return·()"
  "match_TT·FF = fail"
  "match_TT·⊥ = ⊥"
by (simp_all add: TT_def FF_def match_TT_def)

lemma match_FF_simps [simp]:
  "match_FF·FF = return·()"
  "match_FF·TT = fail"
  "match_FF·⊥ = ⊥"
by (simp_all add: TT_def FF_def match_FF_def)

subsection {* Mutual recursion *}

text {*
  The following rules are used to prove unfolding theorems from
  fixed-point definitions of mutually recursive functions.
*}

lemma cpair_equalI: "[|x ≡ cfst·p; y ≡ csnd·p|] ==> <x,y> ≡ p"
by (simp add: surjective_pairing_Cprod2)

lemma cpair_eqD1: "<x,y> = <x',y'> ==> x = x'"
by simp

lemma cpair_eqD2: "<x,y> = <x',y'> ==> y = y'"
by simp

text {* lemma for proving rewrite rules *}

lemma ssubst_lhs: "[|t = s; P s = Q|] ==> P t = Q"
by simp

ML {*
val cpair_equalI = thm "cpair_equalI";
val cpair_eqD1 = thm "cpair_eqD1";
val cpair_eqD2 = thm "cpair_eqD2";
val ssubst_lhs = thm "ssubst_lhs";
*}

subsection {* Initializing the fixrec package *}

use "fixrec_package.ML"

end

Maybe monad type

lemma maybeE:

  [| p = UU ==> Q; p = fail ==> Q; !!x. p = return·x ==> Q |] ==> Q

Monadic bind operator

lemma bind_strict:

  (UU >>= f) = UU

lemma bind_fail:

  (fail >>= f) = fail

lemma left_unit:

  (return·a >>= k) = k·a

lemma right_unit:

  (m >>= return) = m

lemma bind_assoc:

  (do b <- do a <- m; k·a; h·b) = (do a <- m; b <- k·a; h·b)

Run operator

lemma run_strict:

  run·UU = UU

lemma run_fail:

  run·fail = UU

lemma run_return:

  run·(return·x) = x

Monad plus operator

lemma mplus_strict:

  UU +++ m = UU

lemma mplus_fail:

  fail +++ m = m

lemma mplus_return:

  return·x +++ m = return·x

lemma mplus_fail2:

  m +++ fail = m

lemma mplus_assoc:

  (x +++ y) +++ z = x +++ y +++ z

Match functions for built-in types

lemma match_UU_simps:

  match_UU·x = fail

lemma match_cpair_simps:

  match_cpair·<x, y> = return·<x, y>

lemma match_spair_simps:

  [| x ≠ UU; y ≠ UU |] ==> match_spair·(:x, y:) = return·<x, y>
  match_spair·UU = UU

lemma match_sinl_simps:

  x ≠ UU ==> match_sinl·(sinl·x) = return·x
  x ≠ UU ==> match_sinl·(sinr·x) = fail
  match_sinl·UU = UU

lemma match_sinr_simps:

  x ≠ UU ==> match_sinr·(sinr·x) = return·x
  x ≠ UU ==> match_sinr·(sinl·x) = fail
  match_sinr·UU = UU

lemma match_up_simps:

  match_up·(up·x) = return·x
  match_up·UU = UU

lemma match_ONE_simps:

  match_ONE·ONE = return·()
  match_ONE·UU = UU

lemma match_TT_simps:

  match_TT·TT = return·()
  match_TT·FF = fail
  match_TT·UU = UU

lemma match_FF_simps:

  match_FF·FF = return·()
  match_FF·TT = fail
  match_FF·UU = UU

Mutual recursion

lemma cpair_equalI:

  [| x == cfst·p; y == csnd·p |] ==> <x, y> == p

lemma cpair_eqD1:

  <x, y> = <x', y'> ==> x = x'

lemma cpair_eqD2:

  <x, y> = <x', y'> ==> y = y'

lemma ssubst_lhs:

  [| t = s; P s = Q |] ==> P t = Q

Initializing the fixrec package