# 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