Theory Fixrec

(*  Title:      HOL/HOLCF/Fixrec.thy
    Author:     Amber Telfer and Brian Huffman

section "Package for defining recursive functions in HOLCF"

theory Fixrec
imports Cprod Sprod Ssum Up One Tr Fix
keywords "fixrec" :: thy_defn

subsection ‹Pattern-match monad›

default_sort cpo

pcpodef 'a match = "UNIV::(one ++ 'a u) set"
by simp_all

  fail :: "'a match" where
  "fail = Abs_match (sinlONE)"

  succeed :: "'a  'a match" where
  "succeed = (Λ x. Abs_match (sinr(upx)))"

lemma matchE [case_names bottom fail succeed, cases type: match]:
  "p =   Q; p = fail  Q; x. p = succeedx  Q  Q"
unfolding fail_def succeed_def
apply (cases p, rename_tac r)
apply (rule_tac p=r in ssumE, simp add: Abs_match_strict)
apply (rule_tac p=x in oneE, simp, simp)
apply (rule_tac p=y in upE, simp, simp add: cont_Abs_match)

lemma succeed_defined [simp]: "succeedx  "
by (simp add: succeed_def cont_Abs_match Abs_match_bottom_iff)

lemma fail_defined [simp]: "fail  "
by (simp add: fail_def Abs_match_bottom_iff)

lemma succeed_eq [simp]: "(succeedx = succeedy) = (x = y)"
by (simp add: succeed_def cont_Abs_match Abs_match_inject)

lemma succeed_neq_fail [simp]:
  "succeedx  fail" "fail  succeedx"
by (simp_all add: succeed_def fail_def cont_Abs_match Abs_match_inject)

subsubsection ‹Run operator›

  run :: "'a match  'a::pcpo" where
  "run = (Λ m. sscase(fupID)(Rep_match m))"

text ‹rewrite rules for run›

lemma run_strict [simp]: "run = "
unfolding run_def
by (simp add: cont_Rep_match Rep_match_strict)

lemma run_fail [simp]: "runfail = "
unfolding run_def fail_def
by (simp add: cont_Rep_match Abs_match_inverse)

lemma run_succeed [simp]: "run(succeedx) = x"
unfolding run_def succeed_def
by (simp add: cont_Rep_match cont_Abs_match Abs_match_inverse)

subsubsection ‹Monad plus operator›

  mplus :: "'a match  'a match  'a match" where
  "mplus = (Λ m1 m2. sscase(Λ _. m2)(Λ _. m1)(Rep_match m1))"

  mplus_syn :: "['a match, 'a match]  'a match"  (infixr "+++" 65)  where
  "m1 +++ m2 == mplusm1m2"

text ‹rewrite rules for mplus›

lemma mplus_strict [simp]: " +++ m = "
unfolding mplus_def
by (simp add: cont_Rep_match Rep_match_strict)

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

lemma mplus_succeed [simp]: "succeedx +++ m = succeedx"
unfolding mplus_def succeed_def
by (simp add: cont_Rep_match cont_Abs_match Abs_match_inverse)

lemma mplus_fail2 [simp]: "m +++ fail = m"
by (cases m, simp_all)

lemma mplus_assoc: "(x +++ y) +++ z = x +++ (y +++ z)"
by (cases x, simp_all)

subsection ‹Match functions for built-in types›

default_sort pcpo

  match_bottom :: "'a  'c match  'c match"
  "match_bottom = (Λ x k. seqxfail)"

  match_Pair :: "'a::cpo × 'b::cpo  ('a  'b  'c match)  'c match"
  "match_Pair = (Λ x k. csplitkx)"

  match_spair :: "'a  'b  ('a  'b  'c match)  'c match"
  "match_spair = (Λ x k. ssplitkx)"

  match_sinl :: "'a  'b  ('a  'c match)  'c match"
  "match_sinl = (Λ x k. sscasek(Λ b. fail)x)"

  match_sinr :: "'a  'b  ('b  'c match)  'c match"
  "match_sinr = (Λ x k. sscase(Λ a. fail)kx)"

  match_up :: "'a::cpo u  ('a  'c match)  'c match"
  "match_up = (Λ x k. fupkx)"

  match_ONE :: "one  'c match  'c match"
  "match_ONE = (Λ ONE k. k)"

  match_TT :: "tr  'c match  'c match"
  "match_TT = (Λ x k. If x then k else fail)"

  match_FF :: "tr  'c match  'c match"
  "match_FF = (Λ x k. If x then fail else k)"

lemma match_bottom_simps [simp]:
  "match_bottomxk = (if x =  then  else fail)"
by (simp add: match_bottom_def)

lemma match_Pair_simps [simp]:
  "match_Pair(x, y)k = kxy"
by (simp_all add: match_Pair_def)

lemma match_spair_simps [simp]:
  "x  ; y    match_spair(:x, y:)k = kxy"
  "match_spairk = "
by (simp_all add: match_spair_def)

lemma match_sinl_simps [simp]:
  "x    match_sinl(sinlx)k = kx"
  "y    match_sinl(sinry)k = fail"
  "match_sinlk = "
by (simp_all add: match_sinl_def)

lemma match_sinr_simps [simp]:
  "x    match_sinr(sinlx)k = fail"
  "y    match_sinr(sinry)k = ky"
  "match_sinrk = "
by (simp_all add: match_sinr_def)

lemma match_up_simps [simp]:
  "match_up(upx)k = kx"
  "match_upk = "
by (simp_all add: match_up_def)

lemma match_ONE_simps [simp]:
  "match_ONEONEk = k"
  "match_ONEk = "
by (simp_all add: match_ONE_def)

lemma match_TT_simps [simp]:
  "match_TTTTk = k"
  "match_TTFFk = fail"
  "match_TTk = "
by (simp_all add: match_TT_def)

lemma match_FF_simps [simp]:
  "match_FFFFk = k"
  "match_FFTTk = fail"
  "match_FFk = "
by (simp_all add: 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 Pair_equalI: "x  fst p; y  snd p  (x, y)  p"
by simp

lemma Pair_eqD1: "(x, y) = (x', y')  x = x'"
by simp

lemma Pair_eqD2: "(x, y) = (x', y')  y = y'"
by simp

lemma def_cont_fix_eq:
  "f  fix(Abs_cfun F); cont F  f = F f"
by (simp, subst fix_eq, simp)

lemma def_cont_fix_ind:
  "f  fix(Abs_cfun F); cont F; adm P; P ; x. P x  P (F x)  P f"
by (simp add: fix_ind)

text ‹lemma for proving rewrite rules›

lemma ssubst_lhs: "t = s; P s = Q  P t = Q"
by simp

subsection ‹Initializing the fixrec package›

ML_file ‹Tools/holcf_library.ML›
ML_file ‹Tools/fixrec.ML›

method_setup fixrec_simp = Scan.succeed (SIMPLE_METHOD' o Fixrec.fixrec_simp_tac) "pattern prover for fixrec constants"

setup Fixrec.add_matchers
    [ (const_nameup, const_namematch_up),
      (const_namesinl, const_namematch_sinl),
      (const_namesinr, const_namematch_sinr),
      (const_namespair, const_namematch_spair),
      (const_namePair, const_namematch_Pair),
      (const_nameONE, const_namematch_ONE),
      (const_nameTT, const_namematch_TT),
      (const_nameFF, const_namematch_FF),
      (const_namebottom, const_namematch_bottom) ]

hide_const (open) succeed fail run