(* Title: HOL/HOLCF/Fixrec.thy Author: Amber Telfer and Brian Huffman *) header "Package for defining recursive functions in HOLCF" theory Fixrec imports Plain_HOLCF keywords "fixrec" :: thy_decl uses ("Tools/holcf_library.ML") ("Tools/fixrec.ML") begin subsection {* Pattern-match monad *} default_sort cpo pcpodef (open) 'a match = "UNIV::(one ++ 'a u) set" by simp_all definition fail :: "'a match" where "fail = Abs_match (sinl\ONE)" definition succeed :: "'a \ 'a match" where "succeed = (\ x. Abs_match (sinr\(up\x)))" lemma matchE [case_names bottom fail succeed, cases type: match]: "\p = \ \ Q; p = fail \ Q; \x. p = succeed\x \ 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) done lemma succeed_defined [simp]: "succeed\x \ \" 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]: "(succeed\x = succeed\y) = (x = y)" by (simp add: succeed_def cont_Abs_match Abs_match_inject) lemma succeed_neq_fail [simp]: "succeed\x \ fail" "fail \ succeed\x" by (simp_all add: succeed_def fail_def cont_Abs_match Abs_match_inject) subsubsection {* Run operator *} definition run :: "'a match \ 'a::pcpo" where "run = (\ m. sscase\\\(fup\ID)\(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]: "run\fail = \" unfolding run_def fail_def by (simp add: cont_Rep_match Abs_match_inverse) lemma run_succeed [simp]: "run\(succeed\x) = x" unfolding run_def succeed_def by (simp add: cont_Rep_match cont_Abs_match Abs_match_inverse) subsubsection {* Monad plus operator *} definition mplus :: "'a match \ 'a match \ 'a match" where "mplus = (\ m1 m2. sscase\(\ _. m2)\(\ _. m1)\(Rep_match m1))" abbreviation mplus_syn :: "['a match, 'a match] \ 'a match" (infixr "+++" 65) where "m1 +++ m2 == mplus\m1\m2" 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]: "succeed\x +++ m = succeed\x" 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 definition match_bottom :: "'a \ 'c match \ 'c match" where "match_bottom = (\ x k. seq\x\fail)" definition match_Pair :: "'a::cpo \ 'b::cpo \ ('a \ 'b \ 'c match) \ 'c match" where "match_Pair = (\ x k. csplit\k\x)" definition match_spair :: "'a \ 'b \ ('a \ 'b \ 'c match) \ 'c match" where "match_spair = (\ x k. ssplit\k\x)" definition match_sinl :: "'a \ 'b \ ('a \ 'c match) \ 'c match" where "match_sinl = (\ x k. sscase\k\(\ b. fail)\x)" definition match_sinr :: "'a \ 'b \ ('b \ 'c match) \ 'c match" where "match_sinr = (\ x k. sscase\(\ a. fail)\k\x)" definition match_up :: "'a::cpo u \ ('a \ 'c match) \ 'c match" where "match_up = (\ x k. fup\k\x)" definition match_ONE :: "one \ 'c match \ 'c match" where "match_ONE = (\ ONE k. k)" definition match_TT :: "tr \ 'c match \ 'c match" where "match_TT = (\ x k. If x then k else fail)" definition match_FF :: "tr \ 'c match \ 'c match" where "match_FF = (\ x k. If x then fail else k)" lemma match_bottom_simps [simp]: "match_bottom\x\k = (if x = \ then \ else fail)" by (simp add: match_bottom_def) lemma match_Pair_simps [simp]: "match_Pair\(x, y)\k = k\x\y" by (simp_all add: match_Pair_def) lemma match_spair_simps [simp]: "\x \ \; y \ \\ \ match_spair\(:x, y:)\k = k\x\y" "match_spair\\\k = \" by (simp_all add: match_spair_def) lemma match_sinl_simps [simp]: "x \ \ \ match_sinl\(sinl\x)\k = k\x" "y \ \ \ match_sinl\(sinr\y)\k = fail" "match_sinl\\\k = \" by (simp_all add: match_sinl_def) lemma match_sinr_simps [simp]: "x \ \ \ match_sinr\(sinl\x)\k = fail" "y \ \ \ match_sinr\(sinr\y)\k = k\y" "match_sinr\\\k = \" by (simp_all add: match_sinr_def) lemma match_up_simps [simp]: "match_up\(up\x)\k = k\x" "match_up\\\k = \" by (simp_all add: match_up_def) lemma match_ONE_simps [simp]: "match_ONE\ONE\k = k" "match_ONE\\\k = \" by (simp_all add: match_ONE_def) lemma match_TT_simps [simp]: "match_TT\TT\k = k" "match_TT\FF\k = fail" "match_TT\\\k = \" by (simp_all add: match_TT_def) lemma match_FF_simps [simp]: "match_FF\FF\k = k" "match_FF\TT\k = fail" "match_FF\\\k = \" 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 *} use "Tools/holcf_library.ML" use "Tools/fixrec.ML" setup {* Fixrec.setup *} setup {* Fixrec.add_matchers [ (@{const_name up}, @{const_name match_up}), (@{const_name sinl}, @{const_name match_sinl}), (@{const_name sinr}, @{const_name match_sinr}), (@{const_name spair}, @{const_name match_spair}), (@{const_name Pair}, @{const_name match_Pair}), (@{const_name ONE}, @{const_name match_ONE}), (@{const_name TT}, @{const_name match_TT}), (@{const_name FF}, @{const_name match_FF}), (@{const_name bottom}, @{const_name match_bottom}) ] *} hide_const (open) succeed fail run end